Sequential fixed-width evaluation semantics -- proof internals #
noncomputable def
Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.prefixResultInternal
{inputWidth gateBound : ℕ}
{description : Description inputWidth gateBound}
(hdescription : description.WellFormed)
(input : BitString inputWidth)
(count : ℕ)
(hcount : count ≤ gateBound)
:
PrefixResult description input count hcount
Construct the lockstep evaluation witness for a prefix of the padded gate sequence.
Equations
- One or more equations did not get rendered due to their size.