Circuit dependencies

The consumers of a wire are the gates that read it. Equality of two evaluations propagates through the program outside a boundary when the gates crossing that boundary have equal values.

def Cslib.Circuits.Program.Reads {σ : Signature} {n g : ℕ} (p : Program σ n g) (gate : Fin g) (wire : Wire n g) : Prop

A gate reads a wire as one of its arguments.

Equations

• p.Reads gate wire = ∃ (argument : Fin (σ.Arity (p.lines gate).op)), (p.lines gate).wires argument = wire

@[instance_reducible]

instance Cslib.Circuits.Program.instDecidableReads {σ : Signature} {n g : ℕ} (p : Program σ n g) (gate : Fin g) (wire : Wire n g) : Decidable (p.Reads gate wire)

Equations

• p.instDecidableReads gate wire = id inferInstance

def Cslib.Circuits.Program.consumers {σ : Signature} {n g : ℕ} (p : Program σ n g) (wire : Wire n g) : Finset (Fin g)

All gates that read a given wire.

Equations

• p.consumers wire = {gate : Fin g | p.Reads gate wire}

@[simp]

theorem Cslib.Circuits.Program.mem_consumers {σ : Signature} {n g : ℕ} (p : Program σ n g) (wire : Wire n g) (gate : Fin g) : gate ∈ p.consumers wire ↔ p.Reads gate wire

theorem Cslib.Circuits.Program.Reads.lt {σ : Signature} {n g : ℕ} {p : Program σ n g} {gate : Fin g} {wire : Wire n g} (h : p.Reads gate wire) : ↑wire.index < n + ↑gate

A gate can only read input wires and earlier gate wires.

theorem Cslib.Circuits.Program.trace_eq_of_boundary {σ : Signature} {n g : ℕ} {U : Type u_1} (p : Program σ n g) (I : Interpretation σ U) (x y : Fin n → U) (boundary : Set (Wire n g)) (limit : ℕ) (hinput : ∀ (i : Fin n), Wire.input i ∉ boundary → x i = y i) (hgate : ∀ (j : Fin g), n + ↑j < limit → Wire.gate j ∉ boundary → (∃ (a : Fin (σ.Arity (p.lines j).op)), (p.lines j).wires a ∈ boundary) → p.eval I x j = p.eval I y j) (wire : Wire n g) (hwire : wire ∉ boundary) (hlimit : ↑wire.index < limit) : p.trace I x wire = p.trace I y wire

Equality propagates away from a boundary if every gate crossing it agrees.