Evaluating a designated circuit output

Main results

• Cslib.Circuits.Circuit.eval_of_output_eq_gate: an output selecting a gate reads that gate's value in the program evaluation.

theorem Cslib.Circuits.Circuit.eval_of_output_eq_gate {σ : Signature} {U : Type u} {n m : ℕ} {c : Circuit σ n m} {j : Fin m} {gate : Fin c.size} (h : c.outputs j = Wire.gate gate) (I : Interpretation σ U) (x : Fin n → U) : c.eval I x j = c.program.eval I x gate

A designated gate output reads its value from the program evaluation.