Feedback around a straight-line circuit program

A native program may read external inputs and proposed state values. Connecting the latter to selected internal gates produces a cyclic circuit without adding or duplicating operations. The selected gates are its outputs; they may be shared and other gates may be unused.

For monotone interpretations, the cyclic output is the least state satisfying the program's feedback equations. Thus clients can build one ordinary straight-line update program, prove its functional behavior, and close the loop using the existing least-fixed-point semantics. This construction does not assert a finite iteration bound.

Main definitions

• Cslib.Circuits.Program.feedback: connect state inputs to selected internal gates.
• Cslib.Circuits.Circuit.feedback: close a native circuit whose outputs are internal gates.

Main results

• Cslib.Circuits.Program.cost_feedback: feedback preserves every operation weight.
• Cslib.Circuits.Program.eval_feedback_fixed: the outputs satisfy the update equations.
• Cslib.Circuits.Program.eval_feedback_le: leastness among pre-fixed states.
• Cslib.Circuits.Circuit.eval_feedback_eq_lfp: a functional update determines the least output.

References

The construction uses CSLib's native wire mapping and program evaluation and Mathlib's Knaster–Tarski fixed-point API.

def Cslib.Circuits.Program.feedbackWire {n k g : ℕ} (feed : Fin k → Fin g) : Wire (n + k) g → Wire n g

Replace state inputs by their selected feedback gates, leaving other wires unchanged.

theorem Cslib.Circuits.Program.elim_feedbackWire {U : Type v} {n k g : ℕ} (feed : Fin k → Fin g) (input : Fin n → U) (state : Fin g → U) (wire : Wire (n + k) g) : Wire.elim input state (feedbackWire feed wire) = Wire.elim (Fin.append input (state ∘ feed)) state wire

Reading a feedback wire is reading the original wire with the selected gate values as state.

def Cslib.Circuits.Program.feedback {σ : Signature} {n k g : ℕ} (p : Program σ (n + k) g) (feed : Fin k → Fin g) : CyclicCircuit σ n k

Close the last inputs of a program through selected gates, retaining all operation costs.

@[simp]

theorem Cslib.Circuits.Program.cost_feedback {σ : Signature} {n k g : ℕ} (p : Program σ (n + k) g) (feed : Fin k → Fin g) (weight : σ.Op → ℕ) : (p.feedback feed).cost weight = p.cost weight

Feedback does not add, remove or duplicate any weighted gate.

theorem Cslib.Circuits.Program.evalGates_feedback {σ : Signature} {U : Type v} {n k g : ℕ} [CompleteLattice U] (p : Program σ (n + k) g) (feed : Fin k → Fin g) (I : Interpretation σ U) (hI : ∀ (op : σ.Op), Monotone (I op)) (input : Fin n → U) : (p.feedback feed).evalGates I hI input = p.eval I (Fin.append input ((p.feedback feed).eval I hI input))

The solved internal gates are the ordinary evaluation at the solved feedback inputs.

theorem Cslib.Circuits.Program.eval_feedback_fixed {σ : Signature} {U : Type v} {n k g : ℕ} [CompleteLattice U] (p : Program σ (n + k) g) (feed : Fin k → Fin g) (I : Interpretation σ U) (hI : ∀ (op : σ.Op), Monotone (I op)) (input : Fin n → U) : p.eval I (Fin.append input ((p.feedback feed).eval I hI input)) ∘ feed = (p.feedback feed).eval I hI input

Feedback outputs satisfy the program's state-update equations.

theorem Cslib.Circuits.Program.eval_feedback_le {σ : Signature} {U : Type v} {n k g : ℕ} [CompleteLattice U] (p : Program σ (n + k) g) (feed : Fin k → Fin g) (I : Interpretation σ U) (hI : ∀ (op : σ.Op), Monotone (I op)) (input : Fin n → U) {state : Fin k → U} (hstate : p.eval I (Fin.append input state) ∘ feed ≤ state) : (p.feedback feed).eval I hI input ≤ state

Every pre-fixed state bounds the solved feedback outputs.

theorem Cslib.Circuits.Program.eval_feedback_eq_lfp {σ : Signature} {U : Type v} {n k g : ℕ} [CompleteLattice U] (p : Program σ (n + k) g) (feed : Fin k → Fin g) (I : Interpretation σ U) (hI : ∀ (op : σ.Op), Monotone (I op)) (input : Fin n → U) (step : (Fin k → U) →o Fin k → U) (hstep : ∀ (state : Fin k → U), p.eval I (Fin.append input state) ∘ feed = step state) : (p.feedback feed).eval I hI input = OrderHom.lfp step

A proved functional update identifies the feedback output with its least fixed point.

def Cslib.Circuits.Circuit.feedbackGate {σ : Signature} {n k : ℕ} (c : Circuit σ (n + k) k) (h : ∀ (i : Fin k), ∃ (j : Fin c.size), c.outputs i = Wire.gate j) (i : Fin k) : Fin c.size

Extract a circuit's internal output gate, using its structural witness only in proofs.

def Cslib.Circuits.Circuit.feedback {σ : Signature} {n k : ℕ} (c : Circuit σ (n + k) k) (h : ∀ (i : Fin k), ∃ (j : Fin c.size), c.outputs i = Wire.gate j) : CyclicCircuit σ n k

Feed the outputs of a native circuit back into its final input block. Outputs must be internal gates; this excludes direct aliases between state inputs without an operation.

@[simp]

theorem Cslib.Circuits.Circuit.cost_feedback {σ : Signature} {n k : ℕ} (c : Circuit σ (n + k) k) (h : ∀ (i : Fin k), ∃ (j : Fin c.size), c.outputs i = Wire.gate j) (weight : σ.Op → ℕ) : (c.feedback h).cost weight = c.program.cost weight

Closing the feedback block leaves every operation cost unchanged.

theorem Cslib.Circuits.Circuit.eval_feedback_fixed {σ : Signature} {U : Type v} {n k : ℕ} [CompleteLattice U] (c : Circuit σ (n + k) k) (h : ∀ (i : Fin k), ∃ (j : Fin c.size), c.outputs i = Wire.gate j) (I : Interpretation σ U) (hI : ∀ (op : σ.Op), Monotone (I op)) (input : Fin n → U) : c.eval I (Fin.append input ((c.feedback h).eval I hI input)) = (c.feedback h).eval I hI input

The feedback outputs satisfy the ordinary circuit's update equations.

theorem Cslib.Circuits.Circuit.eval_feedback_le {σ : Signature} {U : Type v} {n k : ℕ} [CompleteLattice U] (c : Circuit σ (n + k) k) (h : ∀ (i : Fin k), ∃ (j : Fin c.size), c.outputs i = Wire.gate j) (I : Interpretation σ U) (hI : ∀ (op : σ.Op), Monotone (I op)) (input : Fin n → U) {state : Fin k → U} (hstate : c.eval I (Fin.append input state) ≤ state) : (c.feedback h).eval I hI input ≤ state

Every pre-fixed state bounds the circuit's feedback outputs.

theorem Cslib.Circuits.Circuit.eval_feedback_eq_lfp {σ : Signature} {U : Type v} {n k : ℕ} [CompleteLattice U] (c : Circuit σ (n + k) k) (h : ∀ (i : Fin k), ∃ (j : Fin c.size), c.outputs i = Wire.gate j) (I : Interpretation σ U) (hI : ∀ (op : σ.Op), Monotone (I op)) (input : Fin n → U) (step : (Fin k → U) →o Fin k → U) (hstep : ∀ (state : Fin k → U), c.eval I (Fin.append input state) = step state) : (c.feedback h).eval I hI input = OrderHom.lfp step

A functional description of the circuit update identifies its least feedback solution.