Circuit input support

This file computes the original inputs that can affect each wire and proves that circuit evaluation depends only on those inputs. An input on which a function depends essentially (EssentialAt) therefore reaches an output of every circuit computing it.

Main definitions

• Cslib.Circuits.EssentialAt: coordinates whose change can change a function.
• Cslib.Circuits.Program.wireSupport, Cslib.Circuits.Circuit.inputSupport.

Main results

• Cslib.Circuits.Circuit.dependsOn_eval: a circuit depends only on its input support.

def Cslib.Circuits.EssentialAt {U : Type u_1} {V : Type u_2} {n : ℕ} (f : (Fin n → U) → V) (i : Fin n) : Prop

Changing only coordinate i can change the value of f.

theorem Cslib.Circuits.EssentialAt.mem_support {U : Type u_1} {V : Type u_2} {n : ℕ} {f : (Fin n → U) → V} {support : Finset (Fin n)} {i : Fin n} (h : EssentialAt f i) (hf : DependsOn f ↑support) : i ∈ support

Every essential coordinate belongs to any support of the function.

theorem Cslib.Circuits.essentialAt_iff_not_dependsOn {U : Type u_1} {V : Type u_2} {n : ℕ} {f : (Fin n → U) → V} {i : Fin n} : EssentialAt f i ↔ ¬DependsOn f {i}ᶜ

A coordinate is essential exactly when the function does not depend only on the others.

def Cslib.Circuits.supportInterpretation (σ : Signature) (n : ℕ) : Interpretation σ (Finset (Fin n))

The support interpretation unions the supports of a gate's argument wires.

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.

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

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.

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

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.

@[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.trace_congr {σ : Signature} {U : Type u_1} {n g : ℕ} (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.Program.eval_congr {σ : Signature} {U : Type u_1} {n g : ℕ} (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.Circuit.dependsOn_eval {σ : Signature} {U : Type u_1} {n m : ℕ} (c : Circuit σ n m) (interpretation : Interpretation σ U) : DependsOn (c.eval interpretation) ↑c.inputSupport

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

theorem Cslib.Circuits.Circuit.Computes.dependsOn {σ : Signature} {U : Type u_1} {n m : ℕ} {c : Circuit σ n m} {interpretation : Interpretation σ U} {target : (Fin n → U) → Fin m → U} (computes : c.Computes interpretation target) : DependsOn target ↑c.inputSupport

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