Circuit input support

This file computes the original inputs that can affect each wire and proves that circuit evaluation depends only on those inputs.

def Cslib.Circuits.Line.inputSupport {σ : Signature} {n g : ℕ} (line : Line σ n g) (wireSupport : Wire n g → Finset (Fin n)) : Finset (Fin n)

The original inputs supporting a line, given the support of each wire.

Equations

• line.inputSupport wireSupport = Finset.univ.biUnion fun (k : Fin (σ.Arity line.op)) => wireSupport (line.wires k)

@[simp]

theorem Cslib.Circuits.Line.mem_inputSupport {σ : Signature} {n g : ℕ} {line : Line σ n g} {wireSupport : Wire n g → Finset (Fin n)} {input : Fin n} : input ∈ line.inputSupport wireSupport ↔ ∃ (argument : Fin (σ.Arity line.op)), input ∈ wireSupport (line.wires argument)

Membership in a line's input support comes from one of its arguments.

def Cslib.Circuits.Program.gateSupport {σ : Signature} {n g : ℕ} (program : Program σ n g) : Fin g → Finset (Fin n)

The input support of every gate in a program.

Equations

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

def Cslib.Circuits.Program.wireSupport {σ : Signature} {n g : ℕ} (program : Program σ n g) : Wire n g → Finset (Fin n)

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

Equations

• program.wireSupport = Cslib.Circuits.Wire.elim (fun (k : Fin n) => {k}) program.gateSupport

@[simp]

theorem Cslib.Circuits.Program.wireSupport_input {σ : Signature} {n g : ℕ} (program : Program σ n g) (input : Fin n) : program.wireSupport (Wire.input input) = {input}

An input wire is supported only by that input.

@[simp]

theorem Cslib.Circuits.Program.wireSupport_gate {σ : Signature} {n g : ℕ} (program : Program σ n g) (gate : Fin g) : program.wireSupport (Wire.gate gate) = program.gateSupport gate

A gate-output wire has the support of that gate.

@[simp]

theorem Cslib.Circuits.Program.wireSupport_gate_castSucc {σ : Signature} {n g : ℕ} (program : Program σ n g) (line : Line σ n g) (wire : Wire n g) : (program.gate line).wireSupport wire.castSucc = program.wireSupport wire

Adding a gate preserves the support of every earlier wire.

@[simp]

theorem Cslib.Circuits.Program.gateSupport_gate_last {σ : Signature} {n g : ℕ} (program : Program σ n g) (line : Line σ n g) : (program.gate line).gateSupport (Fin.last g) = line.inputSupport program.wireSupport

The new gate is supported by precisely the inputs supporting the new line.

theorem Cslib.Circuits.Program.wireSupport_gate_last {σ : Signature} {n g : ℕ} (program : Program σ n g) (line : Line σ n g) : (program.gate line).wireSupport (Wire.gate (Fin.last g)) = line.inputSupport program.wireSupport

The new wire is supported by precisely the inputs supporting the new line.

def Cslib.Circuits.Circuit.outputSupport {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : Fin m → Finset (Fin n)

The input support of every designated output wire in a circuit.

Equations

• c.outputSupport = c.program.wireSupport ∘ c.outputs

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

The union of the input supports of a circuit's outputs.

Equations

• c.inputSupport = Finset.univ.biUnion c.outputSupport

@[simp]

theorem Cslib.Circuits.Circuit.mem_inputSupport {σ : Signature} {n m : ℕ} {c : Circuit σ n m} {input : Fin n} : input ∈ c.inputSupport ↔ ∃ (output : Fin m), input ∈ c.program.wireSupport (c.outputs output)

An input supports a circuit exactly when it supports a designated output wire.

theorem Cslib.Circuits.Program.eval_congr {σ : Signature} {n g : ℕ} {U : Type u_2} (program : Program σ n g) (interpretation : Interpretation σ U) (left right : Fin n → U) (k : Fin g) (agree : ∀ i ∈ program.gateSupport k, left i = right i) : program.eval interpretation left k = program.eval interpretation right k

Program gates agree whenever their supporting inputs agree.

theorem Cslib.Circuits.Program.trace_congr {σ : Signature} {n g : ℕ} {U : Type u_2} (program : Program σ n g) (interpretation : Interpretation σ U) (left right : Fin n → U) (wire : Wire n g) (agree : ∀ i ∈ program.wireSupport wire, left i = right i) : program.trace interpretation left wire = program.trace interpretation right wire

Program traces agree on any wire whose supporting inputs agree.

theorem Cslib.Circuits.Circuit.eval_dependsOnlyOn {σ : Signature} {n m : ℕ} {U : Type u_2} (c : Circuit σ n m) (interpretation : Interpretation σ U) : Algebraic.DependsOnlyOn (c.eval interpretation) c.inputSupport

Circuit evaluation depends only on the circuit's structural input support.

theorem Cslib.Circuits.Circuit.ComputesWith.dependsOnlyOn {σ : Signature} {n m : ℕ} {U : Type u_2} {c : Circuit σ n m} {interpretation : Interpretation σ U} {target : (Fin n → U) → Fin m → U} (computes : c.ComputesWith interpretation target) : Algebraic.DependsOnlyOn target c.inputSupport

A computed function depends only on the circuit's structural input support.

theorem Algebraic.Circuit.Computes.dependsOnlyOn {σ : Signature} {n m : ℕ} {U : Type u_2} {circuit : Circuit σ n m} {interpretation : Interpretation σ U} {target : Target U n m} (computes : Computes circuit interpretation target) : DependsOnlyOn target circuit.inputSupport

Legacy qualified name for structural support of a computed function.