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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• line.mapWires wireMap = { op := line.op, wires := wireMap ∘ line.wires }

@[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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Cslib.Circuits.Program.empty.foldl f init = init
• (q.gate line).foldl f init = f (q.foldl (fun {k : ℕ} => f) init) line

@[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.

Equations

• Cslib.Circuits.Program.empty.foldr f init = init
• (q.gate line).foldr f init = q.foldr (fun {k : ℕ} => f) (f line init)

@[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.

Equations

• Cslib.Circuits.Program.empty.FanInAtMost x✝ = True
• (program.gate line).FanInAtMost x✝ = (program.FanInAtMost x✝ ∧ σ.Arity line.op ≤ x✝)

@[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.

Equations

• Cslib.Circuits.Program.empty.instDecidableFanInAtMost r = isTrue trivial
• (q.gate line).instDecidableFanInAtMost r = instDecidableAnd

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.

Equations

• line.eval i inputs gates = i line.op (Cslib.Circuits.Wire.elim inputs gates ∘ line.wires)

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.

Equations

• line.depth wireDepths = (Fin.foldl (σ.Arity line.op) (fun (depth : ℕ) (k : Fin (σ.Arity line.op)) => max depth (wireDepths (line.wires k))) 0).succ

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.

Equations

• Cslib.Circuits.Program.empty.eval i x = Fin.elim0
• (q.gate line).eval i x = fun (i_1 : Fin (gateCount_2 + 1)) => Fin.lastCases (line.eval i x (q.eval i x)) (q.eval i x) i_1

@[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.

Equations

• Cslib.Circuits.Program.empty.depths = Fin.elim0
• (q.gate line).depths = fun (i : Fin (gateCount_2 + 1)) => Fin.lastCases (line.depth (Cslib.Circuits.Wire.elim (fun (x : Fin inputCount) => 0) q.depths)) q.depths i

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.

Equations

• p.wireDepths = Cslib.Circuits.Wire.elim (fun (x : Fin inputCount) => 0) p.depths

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

The maximum depth of any gate in a program.

Equations

• p.depth = Fin.foldl gateCount (fun (depth : ℕ) (k : Fin gateCount) => max depth (p.depths k)) 0

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.

Equations

• p.trace i x = Cslib.Circuits.Wire.elim x (p.eval i x)

@[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.

Equations

• program.gateFunction interpretation gate input = program.eval interpretation input 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.

Equations

• program.wireFunction interpretation wire input = program.trace interpretation input 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.

Equations

• One or more equations did not get rendered due to their size.
• Cslib.Circuits.Program.empty.lines = Fin.elim0

@[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.