Exact semantics of local evaluation checks

Copy chains carry precisely the value computed at their signal vertex. Induction in program order then identifies every locally computed value with the ordinary program trace, including observed sinks, which need no additional outgoing edge.

theorem Algebraic.Cutwidth.Aggregate.Wiring.trace_eq_of_inputs_agree {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) (I : Interpretation σ Bool) {x y : Fin n → Bool} (hxy : ∀ j ∈ SingleCut.inputsIn K.carrier, x j = y j) (w : Wire n s) (hw : w ∈ K.carrier) : p.trace I x w = p.trace I y w

A closed component's trace depends only on its own primary inputs.

theorem Algebraic.Cutwidth.Aggregate.Wiring.trace_eq_of_outside_inputs_agree {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) (I : Interpretation σ Bool) {x y : Fin n → Bool} (hxy : ∀ j ∉ SingleCut.inputsIn K.carrier, x j = y j) (w : Wire n s) (hw : w ∉ K.carrier) : p.trace I x w = p.trace I y w

The complementary trace depends only on inputs outside the component.

theorem Algebraic.Cutwidth.Aggregate.Wiring.copy_eq_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} (hα : ∀ (v : MultiOutput.Internal.WireGraph.Vertex K), Check K I v α) (w : MultiOutput.Internal.WireGraph.Signal K) (m : ℕ) (hm : m < MultiOutput.Internal.WireGraph.fanout K w - 1) : α (Sum.inr ⟨w, ⟨m, hm⟩⟩) = localValue K I α w

Copy chains propagate their signal's locally computed value.

theorem Algebraic.Cutwidth.Aggregate.Wiring.edge_eq_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} (hα : ∀ (v : MultiOutput.Internal.WireGraph.Vertex K), Check K I v α) (e : MultiOutput.Internal.WireGraph.Edge K) : α e = localValue K I α (MultiOutput.Internal.WireGraph.signal K e)

Every edge carries the local value of its signal.

theorem Algebraic.Cutwidth.Aggregate.Wiring.localValue_eq_trace_of_satisfies {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (hinput : InputsHaveFanout K) (I : Interpretation σ Bool) {x : Fin n → Bool} {α : MultiOutput.Internal.WireGraph.Edge K → Bool} (hα : (network K hinput I).Satisfies x α) (w : MultiOutput.Internal.WireGraph.Signal K) : localValue K I α w = p.trace I x ↑w

A satisfying edge assignment computes the program trace at every selected signal.

theorem Algebraic.Cutwidth.Aggregate.Wiring.edge_eq_trace_of_satisfies {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (hinput : InputsHaveFanout K) (I : Interpretation σ Bool) {x : Fin n → Bool} {α : MultiOutput.Internal.WireGraph.Edge K → Bool} (hα : (network K hinput I).Satisfies x α) (e : MultiOutput.Internal.WireGraph.Edge K) : α e = p.trace I x ↑(MultiOutput.Internal.WireGraph.signal K e)

A satisfying assignment puts the trace value on every edge.

def Algebraic.Cutwidth.Aggregate.Wiring.traceAssignment {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) (I : Interpretation σ Bool) (x : Fin n → Bool) (e : MultiOutput.Internal.WireGraph.Edge K) : Bool

The canonical edge assignment induced by the program evaluation.

Equations

• Algebraic.Cutwidth.Aggregate.Wiring.traceAssignment K I x e = p.trace I x ↑(Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.signal K e)

theorem Algebraic.Cutwidth.Aggregate.Wiring.localValue_traceAssignment {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (hinput : InputsHaveFanout K) (I : Interpretation σ Bool) (x : Fin n → Bool) (w : MultiOutput.Internal.WireGraph.Signal K) : localValue K I (traceAssignment K I x) w = p.trace I x ↑w

Local evaluation of the canonical assignment recovers even an unobserved sink.

theorem Algebraic.Cutwidth.Aggregate.Wiring.traceAssignment_satisfies {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (hinput : InputsHaveFanout K) (I : Interpretation σ Bool) (x : Fin n → Bool) : (network K hinput I).Satisfies x (traceAssignment K I x)

Every program input induces a satisfying edge assignment.