Verified serialized-circuit evaluator

This module exposes audited staged-core and end-to-end contracts for the executable three-work-tape circuit-family evaluator. The total machine validates its outer pair, defaults every malformed encoding to zero, and runs within a concrete quadratic bound.

Main results

• evalFamilyCoreTM_hoareTime proves total defaulted-verdict agreement in time 20 * (|code| + |input| + 1)^2.
• evalFamilyTM_hoareTime proves agreement with evalFamilyPair? on every raw input.
• evalFamilyTM_decidesInTime packages the machine as a decider for circuitEvalLanguage.
• evalFamilyTime_bigO_quadratic proves the end-to-end budget is O(n^2).

theorem Complexity.CircuitCode.Machine.evalFamilyCoreTM_hoareTime (codeBits inputBits : List Bool) (initialInput : Tape) : evalFamilyCoreTM.HoareTime (FamilyCorePre codeBits inputBits initialInput) (FamilyCorePost codeBits inputBits initialInput) (evalFamilyCoreTime codeBits.length inputBits.length)

The streaming core evaluates every staged tagged-family code within the uniform quadratic budget. Malformed codes halt with the explicit zero verdict.

theorem Complexity.CircuitCode.Machine.evalFamilyTM_hoareTime (bits : List Bool) : evalFamilyTM.HoareTime (PairStagePre bits) (EvalFamilyPost bits) (evalFamilyTime bits.length)

The total evaluator validates, stages, and evaluates every raw input within the concrete end-to-end budget. Malformed outer pairs and malformed inner codes both halt with the default zero verdict.

theorem Complexity.CircuitCode.Machine.evalFamilyTM_decidesInTime : evalFamilyTM.DecidesInTime circuitEvalLanguage evalFamilyTime

The total serialized evaluator decides exactly the language of successful paired family-code evaluations.

theorem Complexity.CircuitCode.Machine.evalFamilyTime_bigO_quadratic : BigO evalFamilyTime fun (x : ℕ) => x ^ 2

The concrete end-to-end evaluator budget is quadratic in the raw serialized input length.