Sequential fixed-width evaluation semantics

Compiled encoded-evaluation prefixes run successfully on valid descriptions and agree, slot output by slot output, with direct evaluation of the padded raw circuit on the same sample input.

noncomputable def Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.prefixResult {inputWidth gateBound : ℕ} {description : Description inputWidth gateBound} (hdescription : description.WellFormed) (input : BitString inputWidth) (count : ℕ) (hcount : count ≤ gateBound) : PrefixResult description input count hcount

A valid description's compiled prefix and padded raw prefix evaluate in lockstep with corresponding gate outputs.

Equations

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