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.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.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 ((fun (i : Fin (inputCount + gateCount)) => Fin.addCases inputs gates i) ∘ 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), (fun (i : Fin (targetInputCount + targetGateCount)) => Fin.addCases newInputs newGates i) (wireMap wire) = (fun (i : Fin (sourceInputCount + sourceGateCount)) => Fin.addCases oldInputs oldGates i) 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), (fun (i : Fin (inputCount + targetGateCount)) => Fin.addCases inputs newGates i) (ρ.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)) => 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

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

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 i = Fin.addCases (fun (x : Fin inputCount) => 0) p.depths i

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) => 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) : Fin (inputCount + gateCount) → U

The input values followed by all gate values, in program order.

Equations

• p.trace i✝ x i = Fin.addCases x (p.eval i✝ x) i

@[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 (Fin.castSucc wire) = program.trace interpretation input wire

@[simp]

theorem Cslib.Circuits.Program.trace_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).trace interpretation input (Fin.last (inputCount + gateCount)) = line.eval interpretation input (program.eval interpretation input)

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.