Straight-line programs

A program is a topologically ordered sequence of gates. Each Line records an operation and its argument wires. The gate-count index ensures that wires refer only to original inputs or earlier gates.

This file defines

• lines, their evaluation and depth, and Line.mapWires together with the transport lemmas Line.eval_mapWires and Line.eval_mapRenaming;
• programs, their evaluation Program.eval, the input-and-gate valuation Program.trace, gate depths, and the bounded-fan-in predicate Program.FanInAtMost;
• folds over program lines in execution order (Program.foldl) and reverse execution order (Program.foldr), with Program.foldl_rel and Program.foldr_rel for proving that the steps preserve a relation between accumulators;
• the scalar views Program.gateFunction and Program.wireFunction, and the widened line collection Program.lines with Program.lines_eval.

Evaluation of lines and programs commutes with homomorphisms (Line.map_eval, Program.map_eval, Program.map_trace).

structure Cslib.Circuits.Line (σ : Signature) (inputCount gateCount : ℕ) : Type u_1

One gate together with the wires supplying its arguments.

• op : σ.Op

  The operation performed by the gate.

• wires : Fin (σ.Arity self.op) → Wire inputCount gateCount

  The wire supplying each argument of the operation.

def Cslib.Circuits.Line.equiv (σ : Signature) (inputCount gateCount : ℕ) : Line σ inputCount gateCount ≃ (op : σ.Op) × (Fin (σ.Arity op) → Wire inputCount gateCount)

A line is an operation symbol together with a tuple of argument wires.

def Cslib.Circuits.Line.mapWires {σ : Signature} {sourceInputCount targetInputCount sourceGateCount targetGateCount : ℕ} (line : Line σ sourceInputCount sourceGateCount) (wireMap : Wire sourceInputCount sourceGateCount → Wire targetInputCount targetGateCount) : Line σ targetInputCount targetGateCount

Apply a function to every wire read by a line.

@[simp]

theorem Cslib.Circuits.Line.mapWires_op {σ : Signature} {sourceInputCount targetInputCount sourceGateCount targetGateCount : ℕ} (line : Line σ sourceInputCount sourceGateCount) (wireMap : Wire sourceInputCount sourceGateCount → Wire targetInputCount targetGateCount) : (line.mapWires wireMap).op = line.op

@[simp]

theorem Cslib.Circuits.Line.mapWires_wires {σ : Signature} {sourceInputCount targetInputCount sourceGateCount targetGateCount : ℕ} (line : Line σ sourceInputCount sourceGateCount) (wireMap : Wire sourceInputCount sourceGateCount → Wire targetInputCount targetGateCount) (argument : Fin (σ.Arity line.op)) : (line.mapWires wireMap).wires argument = wireMap (line.wires argument)

inductive Cslib.Circuits.Program (σ : Signature) (inputCount : ℕ) : ℕ → Type v

A topologically ordered straight-line program, indexed by its gate count.

• empty {σ : Signature} {inputCount : ℕ} : Program σ inputCount 0
• gate {σ : Signature} {inputCount gateCount : ℕ} : Program σ inputCount gateCount → Line σ inputCount gateCount → Program σ inputCount (gateCount + 1)

def Cslib.Circuits.Program.emptyEquiv (σ : Signature) (inputCount : ℕ) : Program σ inputCount 0 ≃ PUnit.{1}

The empty program is the only program with no gates.

def Cslib.Circuits.Program.gateEquiv (σ : Signature) (inputCount gateCount : ℕ) : Program σ inputCount (gateCount + 1) ≃ Program σ inputCount gateCount × Line σ inputCount gateCount

A nonempty program is a prefix followed by its last gate.

def Cslib.Circuits.Program.foldl {σ : Signature} {inputCount : ℕ} {α : Type u₁} {gateCount : ℕ} (p : Program σ inputCount gateCount) (f : {k : ℕ} → α → Line σ inputCount k → α) (init : α) : α

Fold the lines from the first gate to the last. The step accepts a line at any gate count, retaining its original bound on references to previous gates.

@[simp]

theorem Cslib.Circuits.Program.foldl_empty {σ : Signature} {inputCount : ℕ} {α : Type u₁} (f : {k : ℕ} → α → Line σ inputCount k → α) (init : α) : empty.foldl (fun {k : ℕ} => f) init = init

@[simp]

theorem Cslib.Circuits.Program.foldl_gate {σ : Signature} {inputCount gateCount : ℕ} {α : Type u₁} (p : Program σ inputCount gateCount) (line : Line σ inputCount gateCount) (f : {k : ℕ} → α → Line σ inputCount k → α) (init : α) : (p.gate line).foldl (fun {k : ℕ} => f) init = f (p.foldl (fun {k : ℕ} => f) init) line

theorem Cslib.Circuits.Program.foldl_rel {σ : Signature} {inputCount gateCount : ℕ} {α : Type u₁} {β : Type u₂} (p : Program σ inputCount gateCount) (R : α → β → Prop) {f : {k : ℕ} → α → Line σ inputCount k → α} {f' : {k : ℕ} → β → Line σ inputCount k → β} {a : α} {b : β} (hinit : R a b) (hstep : ∀ {k : ℕ} {a : α} {b : β} (line : Line σ inputCount k), R a b → R (f a line) (f' b line)) : R (p.foldl (fun {k : ℕ} => f) a) (p.foldl (fun {k : ℕ} => f') b)

Two left folds preserve a relation if their initial accumulators are related and each pair of steps preserves it. For example, use equality or an order relation.

def Cslib.Circuits.Program.foldr {σ : Signature} {inputCount : ℕ} {α : Type u₁} {gateCount : ℕ} (p : Program σ inputCount gateCount) (f : {k : ℕ} → Line σ inputCount k → α → α) (init : α) : α

Fold the lines from the last gate to the first. Each line retains its original bound on references to previous gates, and the step receives the line before the accumulator.

@[simp]

theorem Cslib.Circuits.Program.foldr_empty {σ : Signature} {inputCount : ℕ} {α : Type u₁} (f : {k : ℕ} → Line σ inputCount k → α → α) (init : α) : empty.foldr (fun {k : ℕ} => f) init = init

@[simp]

theorem Cslib.Circuits.Program.foldr_gate {σ : Signature} {inputCount gateCount : ℕ} {α : Type u₁} (p : Program σ inputCount gateCount) (line : Line σ inputCount gateCount) (f : {k : ℕ} → Line σ inputCount k → α → α) (init : α) : (p.gate line).foldr (fun {k : ℕ} => f) init = p.foldr (fun {k : ℕ} => f) (f line init)

theorem Cslib.Circuits.Program.foldr_rel {σ : Signature} {inputCount gateCount : ℕ} {α : Type u₁} {β : Type u₂} (p : Program σ inputCount gateCount) (R : α → β → Prop) {f : {k : ℕ} → Line σ inputCount k → α → α} {f' : {k : ℕ} → Line σ inputCount k → β → β} {a : α} {b : β} (hinit : R a b) (hstep : ∀ {k : ℕ} {a : α} {b : β} (line : Line σ inputCount k), R a b → R (f line a) (f' line b)) : R (p.foldr (fun {k : ℕ} => f) a) (p.foldr (fun {k : ℕ} => f') b)

Two right folds preserve a relation if their initial accumulators are related and each pair of steps preserves it.

def Cslib.Circuits.Program.FanInAtMost {σ : Signature} {inputCount gateCount : ℕ} (program : Program σ inputCount gateCount) : ℕ → Prop

Every gate in a program has at most r arguments.

@[instance_reducible]

instance Cslib.Circuits.Program.instDecidableFanInAtMost {σ : Signature} {inputCount gateCount : ℕ} (program : Program σ inputCount gateCount) (r : ℕ) : Decidable (program.FanInAtMost r)

Bounded fan-in is decidable for every concrete program.

def Cslib.Circuits.Line.eval {σ : Signature} {inputCount gateCount : ℕ} {U : Type u} (line : Line σ inputCount gateCount) (i : Interpretation σ U) (inputs : Fin inputCount → U) (gates : Fin gateCount → U) : U

Evaluate a line from the values of the inputs and preceding gates.

theorem Cslib.Circuits.Line.eval_mapWires {σ : Signature} {sourceInputCount targetInputCount sourceGateCount targetGateCount : ℕ} {U : Type u} (line : Line σ sourceInputCount sourceGateCount) (wireMap : Wire sourceInputCount sourceGateCount → Wire targetInputCount targetGateCount) (interpretation : Interpretation σ U) (oldInputs : Fin sourceInputCount → U) (newInputs : Fin targetInputCount → U) (oldGates : Fin sourceGateCount → U) (newGates : Fin targetGateCount → U) (preserves : ∀ (wire : Wire sourceInputCount sourceGateCount), Wire.elim newInputs newGates (wireMap wire) = Wire.elim oldInputs oldGates wire) : (line.mapWires wireMap).eval interpretation newInputs newGates = line.eval interpretation oldInputs oldGates

Mapping a line's wires preserves evaluation when the new valuation agrees with the old valuation along the map. The source and target input namespaces may differ.

theorem Cslib.Circuits.Line.eval_mapRenaming {σ : Signature} {inputCount sourceGateCount targetGateCount : ℕ} {U : Type u} (line : Line σ inputCount sourceGateCount) (ρ : Wire.Renaming inputCount sourceGateCount targetGateCount) (interpretation : Interpretation σ U) (inputs : Fin inputCount → U) (oldGates : Fin sourceGateCount → U) (newGates : Fin targetGateCount → U) (preservesGates : ∀ (gate : Fin sourceGateCount), Wire.elim inputs newGates (ρ.gates gate) = oldGates gate) : (line.mapWires ρ.apply).eval interpretation inputs newGates = line.eval interpretation inputs oldGates

Specialization of Line.eval_mapWires to an input-fixing wire renaming.

def Cslib.Circuits.Line.depth {σ : Signature} {inputCount gateCount : ℕ} (line : Line σ inputCount gateCount) (wireDepths : Wire inputCount gateCount → ℕ) : ℕ

The depth of a line, given the depth of every wire it may read.

theorem Cslib.Circuits.Line.map_eval {σ : Signature} {inputCount gateCount : ℕ} {U₁ : Type u₁} {U₂ : Type u₂} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} (line : Line σ inputCount gateCount) (h : Homomorphism i₁ i₂) (inputs : Fin inputCount → U₁) (gates : Fin gateCount → U₁) : h.map (line.eval i₁ inputs gates) = line.eval i₂ (h.map ∘ inputs) (h.map ∘ gates)

Evaluating a line commutes with a homomorphism.

def Cslib.Circuits.Program.eval {σ : Signature} {inputCount : ℕ} {U : Type u} {gateCount : ℕ} (p : Program σ inputCount gateCount) (i : Interpretation σ U) (x : Fin inputCount → U) : Fin gateCount → U

Evaluate every gate in a program, in program order.

@[simp]

theorem Cslib.Circuits.Program.eval_gate_last {σ : Signature} {inputCount gateCount : ℕ} {U : Type u} (program : Program σ inputCount gateCount) (line : Line σ inputCount gateCount) (interpretation : Interpretation σ U) (input : Fin inputCount → U) : (program.gate line).eval interpretation input (Fin.last gateCount) = line.eval interpretation input (program.eval interpretation input)

@[simp]

theorem Cslib.Circuits.Program.eval_gate_castSucc {σ : Signature} {inputCount gateCount : ℕ} {U : Type u} (program : Program σ inputCount gateCount) (line : Line σ inputCount gateCount) (interpretation : Interpretation σ U) (input : Fin inputCount → U) (gate : Fin gateCount) : (program.gate line).eval interpretation input gate.castSucc = program.eval interpretation input gate

def Cslib.Circuits.Program.depths {σ : Signature} {inputCount gateCount : ℕ} (p : Program σ inputCount gateCount) : Fin gateCount → ℕ

The depth of every gate in a program. Inputs have implicit depth zero.

def Cslib.Circuits.Program.wireDepths {σ : Signature} {inputCount gateCount : ℕ} (p : Program σ inputCount gateCount) : Wire inputCount gateCount → ℕ

The depth of every input or gate wire in a program.

def Cslib.Circuits.Program.depth {σ : Signature} {inputCount gateCount : ℕ} (p : Program σ inputCount gateCount) : ℕ

The maximum depth of any gate in a program.

theorem Cslib.Circuits.Program.map_eval {σ : Signature} {inputCount gateCount : ℕ} {U₁ : Type u₁} {U₂ : Type u₂} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} (p : Program σ inputCount gateCount) (h : Homomorphism i₁ i₂) (x : Fin inputCount → U₁) : h.map ∘ p.eval i₁ x = p.eval i₂ (h.map ∘ x)

Evaluating a program commutes with a homomorphism.

def Cslib.Circuits.Program.trace {σ : Signature} {inputCount gateCount : ℕ} {U : Type u} (p : Program σ inputCount gateCount) (i : Interpretation σ U) (x : Fin inputCount → U) : Wire inputCount gateCount → U

The value of every input and gate wire.

@[simp]

theorem Cslib.Circuits.Program.trace_input {σ : Signature} {inputCount gateCount : ℕ} {U : Type u} (program : Program σ inputCount gateCount) (interpretation : Interpretation σ U) (input : Fin inputCount → U) (sourceInput : Fin inputCount) : program.trace interpretation input (Wire.input sourceInput) = input sourceInput

@[simp]

theorem Cslib.Circuits.Program.trace_gate_castSucc {σ : Signature} {inputCount gateCount : ℕ} {U : Type u} (program : Program σ inputCount gateCount) (line : Line σ inputCount gateCount) (interpretation : Interpretation σ U) (input : Fin inputCount → U) (wire : Wire inputCount gateCount) : (program.gate line).trace interpretation input wire.castSucc = program.trace interpretation input wire

theorem Cslib.Circuits.Program.map_trace {σ : Signature} {inputCount gateCount : ℕ} {U₁ : Type u₁} {U₂ : Type u₂} {i₁ : Interpretation σ U₁} {i₂ : Interpretation σ U₂} (p : Program σ inputCount gateCount) (h : Homomorphism i₁ i₂) (x : Fin inputCount → U₁) : h.map ∘ p.trace i₁ x = p.trace i₂ (h.map ∘ x)

Evaluating every input and gate wire commutes with a homomorphism.

def Cslib.Circuits.Program.gateFunction {σ : Signature} {inputCount gateCount : ℕ} {U : Type u} (program : Program σ inputCount gateCount) (interpretation : Interpretation σ U) (gate : Fin gateCount) (input : Fin inputCount → U) : U

The scalar function computed by an internal gate.

def Cslib.Circuits.Program.wireFunction {σ : Signature} {inputCount gateCount : ℕ} {U : Type u} (program : Program σ inputCount gateCount) (interpretation : Interpretation σ U) (wire : Wire inputCount gateCount) (input : Fin inputCount → U) : U

The scalar function carried by an input or internal-gate wire.

@[simp]

theorem Cslib.Circuits.Program.gateFunction_apply {σ : Signature} {inputCount gateCount : ℕ} {U : Type u} (program : Program σ inputCount gateCount) (interpretation : Interpretation σ U) (gate : Fin gateCount) (input : Fin inputCount → U) : program.gateFunction interpretation gate input = program.eval interpretation input gate

@[simp]

theorem Cslib.Circuits.Program.wireFunction_input {σ : Signature} {inputCount gateCount : ℕ} {U : Type u} (program : Program σ inputCount gateCount) (interpretation : Interpretation σ U) (inputWire : Fin inputCount) : program.wireFunction interpretation (Wire.input inputWire) = fun (input : Fin inputCount → U) => input inputWire

@[simp]

theorem Cslib.Circuits.Program.wireFunction_gate {σ : Signature} {inputCount gateCount : ℕ} {U : Type u} (program : Program σ inputCount gateCount) (interpretation : Interpretation σ U) (gate : Fin gateCount) : program.wireFunction interpretation (Wire.gate gate) = program.gateFunction interpretation gate

@[simp]

theorem Cslib.Circuits.Program.gateFunction_gate_last {σ : Signature} {inputCount gateCount : ℕ} {U : Type u} (program : Program σ inputCount gateCount) (line : Line σ inputCount gateCount) (interpretation : Interpretation σ U) : (program.gate line).gateFunction interpretation (Fin.last gateCount) = fun (input : Fin inputCount → U) => line.eval interpretation input (program.eval interpretation input)

@[simp]

theorem Cslib.Circuits.Program.gateFunction_gate_castSucc {σ : Signature} {inputCount gateCount : ℕ} {U : Type u} (program : Program σ inputCount gateCount) (line : Line σ inputCount gateCount) (interpretation : Interpretation σ U) (gate : Fin gateCount) : (program.gate line).gateFunction interpretation gate.castSucc = program.gateFunction interpretation gate

@[simp]

theorem Cslib.Circuits.Program.trace_gateWire {σ : Signature} {inputCount gateCount : ℕ} {U : Type u} (program : Program σ inputCount gateCount) (interpretation : Interpretation σ U) (input : Fin inputCount → U) (gate : Fin gateCount) : program.trace interpretation input (Wire.gate gate) = program.gateFunction interpretation gate input

def Cslib.Circuits.Program.lines {σ : Signature} {inputCount gateCount : ℕ} (program : Program σ inputCount gateCount) : Fin gateCount → Line σ inputCount gateCount

The program's lines, each widened to the final wire namespace.

@[simp]

theorem Cslib.Circuits.Program.lines_gate_last {σ : Signature} {inputCount gateCount : ℕ} (program : Program σ inputCount gateCount) (line : Line σ inputCount gateCount) : (program.gate line).lines (Fin.last gateCount) = line.mapWires Wire.Renaming.castSucc.apply

@[simp]

theorem Cslib.Circuits.Program.lines_gate_castSucc {σ : Signature} {inputCount gateCount : ℕ} (program : Program σ inputCount gateCount) (line : Line σ inputCount gateCount) (gate : Fin gateCount) : (program.gate line).lines gate.castSucc = (program.lines gate).mapWires Wire.Renaming.castSucc.apply

theorem Cslib.Circuits.Program.lines_eval {σ : Signature} {inputCount gateCount : ℕ} {U : Type u} (program : Program σ inputCount gateCount) (interpretation : Interpretation σ U) (input : Fin inputCount → U) (gate : Fin gateCount) : (program.lines gate).eval interpretation input (program.eval interpretation input) = program.eval interpretation input gate

A widened line evaluates to the value of its corresponding program gate.

theorem Cslib.Circuits.Program.eq_eval_of_forall_lines_eval {σ : Signature} {inputCount gateCount : ℕ} {U : Type u} (p : Program σ inputCount gateCount) (i : Interpretation σ U) (x : Fin inputCount → U) (values : Fin gateCount → U) (h : ∀ (gate : Fin gateCount), (p.lines gate).eval i x values = values gate) : values = p.eval i x

A valuation satisfying every gate equation is the program's evaluation.