Facts about straight-line programs

Upstreaming candidates for Cslib.Computability.Circuit.Program:

• Program.lines_wires_eq_gate_lt: a gate reads only earlier gates.
• Program.FanInAtMost.arity_le: under a fan-in bound, every line has bounded arity.
• Program.trace_gate: the value of a gate is its operation applied to the values of its arguments.
• Program.Upstream and Program.trace_congr_of_upstream: the value of a wire depends only on the inputs upstream of it.
• Circuit.innerSize: the number of gates of positive arity. Gates of arity zero are constants, leaves of the circuit like its inputs.

theorem Cslib.Circuits.Program.lt_of_gate_mem_range_wires {σ : Signature} {n s : ℕ} (p : Program σ n s) (g : Fin s) {g' : Fin s} (h : Wire.gate g' ∈ Set.range (p.lines g).wires) : g' < g

The argument wires of a gate are original inputs or earlier gates.

theorem Cslib.Circuits.Program.lines_wires_eq_gate_lt {σ : Signature} {n s : ℕ} (p : Program σ n s) (g : Fin s) (a : Fin (σ.Arity (p.lines g).op)) {g' : Fin s} (h : (p.lines g).wires a = Wire.gate g') : g' < g

A gate reads only original inputs and earlier gates.

theorem Cslib.Circuits.Program.FanInAtMost.arity_le {σ : Signature} {n s : ℕ} {p : Program σ n s} {r : ℕ} (h : p.FanInAtMost r) (g : Fin s) : σ.Arity (p.lines g).op ≤ r

Under a fan-in bound, every line of a program has bounded arity.

theorem Cslib.Circuits.Program.trace_gate {σ : Signature} {n s : ℕ} {U : Type u_1} (p : Program σ n s) (I : Interpretation σ U) (x : Fin n → U) (g : Fin s) : p.trace I x (Wire.gate g) = I (p.lines g).op fun (a : Fin (σ.Arity (p.lines g).op)) => p.trace I x ((p.lines g).wires a)

The value of a gate is its operation applied to the values of its argument wires.

inductive Cslib.Circuits.Program.Upstream {σ : Signature} {n s : ℕ} (p : Program σ n s) (w : Wire n s) : Wire n s → Prop

p.Upstream w v: the wire v is w itself or an argument of a gate upstream of w. The value of w can depend only on the wires upstream of it.

• refl {σ : Signature} {n s : ℕ} {p : Program σ n s} {w : Wire n s} : p.Upstream w w

  Every wire is upstream of itself.

• arg {σ : Signature} {n s : ℕ} {p : Program σ n s} {w : Wire n s} {g : Fin s} (a : Fin (σ.Arity (p.lines g).op)) : p.Upstream w (Wire.gate g) → p.Upstream w ((p.lines g).wires a)

  The arguments of a gate upstream of w are upstream of w.

theorem Cslib.Circuits.Program.Upstream.trans {σ : Signature} {n s : ℕ} {p : Program σ n s} {u v w : Wire n s} (huv : p.Upstream u v) (hvw : p.Upstream v w) : p.Upstream u w

theorem Cslib.Circuits.Program.trace_congr_of_upstream {σ : Signature} {n s : ℕ} {U : Type u_1} (p : Program σ n s) (I : Interpretation σ U) {x y : Fin n → U} {w : Wire n s} (h : ∀ (i : Fin n), p.Upstream w (Wire.input i) → x i = y i) (v : Wire n s) : p.Upstream w v → p.trace I x v = p.trace I y v

The value of a wire depends only on the inputs upstream of it.

def Cslib.Circuits.Program.innerGates {σ : Signature} {n s : ℕ} (p : Program σ n s) : Finset (Fin s)

The inner gates of a program: those of positive arity. A gate of arity zero is a constant, a leaf of the circuit like an input.

Equations

• p.innerGates = {g : Fin s | σ.Arity (p.lines g).op ≠ 0}

def Cslib.Circuits.Circuit.innerSize {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : ℕ

The number of inner gates of a circuit: its size, with constant gates free. For arithmetic circuits this counts additions and multiplications.

Equations

• c.innerSize = c.program.innerGates.card

theorem Cslib.Circuits.Circuit.innerSize_le_size {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : c.innerSize ≤ c.size