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;
• 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.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
• (prior.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
• (prior.gate line).eval i x = fun (i_1 : Fin (gateCount_2 + 1)) => Fin.lastCases (line.eval i x (prior.eval i x)) (prior.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
• (prior.gate line).depths = fun (i : Fin (gateCount_2 + 1)) => Fin.lastCases (line.depth (Cslib.Circuits.Wire.elim (fun (x : Fin inputCount) => 0) prior.depths)) prior.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_wires_lt {σ : Signature} {n g : ℕ} (p : Program σ n g) (gate : Fin g) (argument : Fin (σ.Arity (p.lines gate).op)) : ↑((p.lines gate).wires argument).index < n + ↑gate

Every argument of a widened line is an input or an earlier gate.

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.