Local evaluation on a closed wire graph

The graph has no extra edges for observed sinks. Gate values are computed directly from their incident argument slots, including nullary gates. Inputs use their first outgoing edge; the compiler therefore assumes that the selected inputs have positive fanout.

def Algebraic.Cutwidth.Aggregate.Wiring.InputsHaveFanout {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) : Prop

Every selected primary input has an ordinary outgoing slot.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Cutwidth.Aggregate.Wiring.signal_eq_of_fst_eq_inl {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) {e : MultiOutput.Internal.WireGraph.Edge K} {w : MultiOutput.Internal.WireGraph.Signal K} (h : MultiOutput.Internal.WireGraph.fst K e = Sum.inl w) : MultiOutput.Internal.WireGraph.signal K e = w

The signal carried by an edge leaving a signal vertex.

theorem Algebraic.Cutwidth.Aggregate.Wiring.signal_eq_of_fst_eq_inr {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) {e : MultiOutput.Internal.WireGraph.Edge K} {c : MultiOutput.Internal.WireGraph.Copy K} (h : MultiOutput.Internal.WireGraph.fst K e = Sum.inr c) : MultiOutput.Internal.WireGraph.signal K e = c.fst

The signal carried by an edge leaving a copy vertex.

theorem Algebraic.Cutwidth.Aggregate.Wiring.exists_outgoing {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) (w : MultiOutput.Internal.WireGraph.Signal K) (hpos : 0 < MultiOutput.Internal.WireGraph.fanout K w) : ∃ (e : MultiOutput.Internal.WireGraph.Edge K), MultiOutput.Internal.WireGraph.fst K e = Sum.inl w

A signal with positive fanout has an outgoing edge at its signal vertex.

noncomputable def Algebraic.Cutwidth.Aggregate.Wiring.firstOut {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (w : MultiOutput.Internal.WireGraph.Signal K) : MultiOutput.Internal.WireGraph.Edge K

An outgoing edge, with an irrelevant default for sinks.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Cutwidth.Aggregate.Wiring.fst_firstOut {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (w : MultiOutput.Internal.WireGraph.Signal K) (h : 0 < MultiOutput.Internal.WireGraph.fanout K w) : MultiOutput.Internal.WireGraph.fst K (firstOut K w) = Sum.inl w

theorem Algebraic.Cutwidth.Aggregate.Wiring.signal_firstOut {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (w : MultiOutput.Internal.WireGraph.Signal K) (h : 0 < MultiOutput.Internal.WireGraph.fanout K w) : MultiOutput.Internal.WireGraph.signal K (firstOut K w) = w

theorem Algebraic.Cutwidth.Aggregate.Wiring.eq_firstOut_of_fst_eq_inl {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] {w : MultiOutput.Internal.WireGraph.Signal K} {e : MultiOutput.Internal.WireGraph.Edge K} (h : MultiOutput.Internal.WireGraph.fst K e = Sum.inl w) (hpos : 0 < MultiOutput.Internal.WireGraph.fanout K w) : e = firstOut K w

At most one outgoing edge at a signal vertex identifies its chosen edge.

def Algebraic.Cutwidth.Aggregate.Wiring.opValue {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) (I : Interpretation σ Bool) (g : Fin s) (h : Wire.gate g ∈ K.carrier) (α : MultiOutput.Internal.WireGraph.Edge K → Bool) : Bool

The value of a gate, computed from its incident argument slots.

Equations

• Algebraic.Cutwidth.Aggregate.Wiring.opValue K I g h α = I (p.lines g).op fun (a : Fin (σ.Arity (p.lines g).op)) => α (Sum.inl ⟨⟨g, a⟩, h⟩)

noncomputable def Algebraic.Cutwidth.Aggregate.Wiring.localValue {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (I : Interpretation σ Bool) (α : MultiOutput.Internal.WireGraph.Edge K → Bool) : MultiOutput.Internal.WireGraph.Signal K → Bool

The value observed at a signal vertex, including gates without outgoing edges.

Equations

• Algebraic.Cutwidth.Aggregate.Wiring.localValue K I α ⟨Cslib.Circuits.Wire.input j, h⟩ = α (Algebraic.Cutwidth.Aggregate.Wiring.firstOut K ⟨Cslib.Circuits.Wire.input j, h⟩)
• Algebraic.Cutwidth.Aggregate.Wiring.localValue K I α ⟨Cslib.Circuits.Wire.gate g, h⟩ = Algebraic.Cutwidth.Aggregate.Wiring.opValue K I g h α

noncomputable def Algebraic.Cutwidth.Aggregate.Wiring.Check {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (I : Interpretation σ Bool) : MultiOutput.Internal.WireGraph.Vertex K → (MultiOutput.Internal.WireGraph.Edge K → Bool) → Prop

Every outgoing edge agrees with its local signal or incoming copy edge.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.Aggregate.Wiring.portVertex {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (j : Fin n) : MultiOutput.Internal.WireGraph.Vertex K

Each selected input is read at its signal vertex.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.Aggregate.Wiring.portEdge {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (j : Fin n) : MultiOutput.Internal.WireGraph.Edge K

The chosen outgoing edge carries a selected input.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Cutwidth.Aggregate.Wiring.localValue_congr {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (hinput : InputsHaveFanout K) (I : Interpretation σ Bool) (w : MultiOutput.Internal.WireGraph.Signal K) (α β : MultiOutput.Internal.WireGraph.Edge K → Bool) (h : ∀ (e : MultiOutput.Internal.WireGraph.Edge K), MultiOutput.Internal.WireGraph.fst K e = Sum.inl w ∨ MultiOutput.Internal.WireGraph.snd K e = Sum.inl w → α e = β e) : localValue K I α w = localValue K I β w

Local values depend only on incident edge bits.

noncomputable def Algebraic.Cutwidth.Aggregate.Wiring.network {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (hinput : InputsHaveFanout K) (I : Interpretation σ Bool) : Network n (MultiOutput.Internal.WireGraph.Vertex K) (MultiOutput.Internal.WireGraph.Edge K)

The unchanged wire graph equipped with local evaluation checks and input ports.

Equations

• One or more equations did not get rendered due to their size.