Pure semantics for the streaming circuit evaluator

The machine controller parses and evaluates one gate before moving to the next. The public codec first decodes the complete gate list and then evaluates it. This file supplies a verdict-level streaming evaluator and proves that the two orders produce the same result. A controller-ordered one-gate step additionally exposes the ref0-before-ref1 dependency order needed by execution proofs while retaining evalFamilyCode as their external specification; it is not a transition-level trace model.

def Complexity.CircuitCode.Machine.Internal.gateStream? : ℕ → List Bool → List Bool → Option Bool → Option Bool

Parse and evaluate exactly count gates. The memo list begins with the primary inputs and grows by one value per gate; last is the most recently appended gate value. Successful termination also requires exact code consumption.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitCode.Machine.Internal.gateStream? 0 x✝² x✝¹ x✝ = if x✝² = [] then x✝ else none

structure Complexity.CircuitCode.Machine.Internal.GateStepResult : Type

The semantic result of one controller-ordered gate evaluation.

• rest : List Bool

  The unconsumed circuit code after both references.

• wires : List Bool

  The wire memo after appending the new gate value.

• value : Bool

  The newly computed gate value.

def Complexity.CircuitCode.Machine.Internal.gateStep? (code wires : List Bool) : Option GateStepResult

Parse and evaluate one gate in the controller's reference dependency order: parse the first reference, read its wire, parse the second reference, and read its wire.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitCode.Machine.Internal.gateStep? code wires = none

theorem Complexity.CircuitCode.Machine.Internal.rawGate_eval_opOfBit (op negated₀ negated₁ value₀ value₁ : Bool) (input₀ input₁ : ℕ) : { op := RawGate.opOfBit op, input₀ := input₀, input₁ := input₁, negated₀ := negated₀, negated₁ := negated₁ }.eval value₀ value₁ = evalOpBit op (negated₀ ^^ value₀) (negated₁ ^^ value₁)

Decoding an operation bit and evaluating the resulting raw gate agrees with the controller's Boolean operation.

theorem Complexity.CircuitCode.Machine.Internal.gateStream?_succ_eq_gateStep? (count : ℕ) (code wires : List Bool) (last : Option Bool) : gateStream? (count + 1) code wires last = (gateStep? code wires).bind fun (step : GateStepResult) => gateStream? count step.rest step.wires (some step.value)

A positive gate-stream step is exactly one controller-ordered gate step followed by the remaining stream.

def Complexity.CircuitCode.Machine.Internal.positiveStream? (code input : List Bool) : Option Bool

Parse a circuit's unary gate count and evaluate its gate stream.

Equations

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

theorem Complexity.CircuitCode.Machine.Internal.positiveStream?_eq_evalCode (code input : List Bool) : positiveStream? code input = evalCode input.length code input

The streaming specification agrees with the library's public exact codec and memoized evaluator.

def Complexity.CircuitCode.Machine.Internal.familyStream? (code input : List Bool) : Option Bool

Pure semantics of the complete tagged-family stream consumed by the machine core.

Equations

• Complexity.CircuitCode.Machine.Internal.familyStream? [false, answer] input = if input.isEmpty = true then some answer else none
• Complexity.CircuitCode.Machine.Internal.familyStream? (true :: circuitCode) input = if input.isEmpty = true then none else Complexity.CircuitCode.Machine.Internal.positiveStream? circuitCode input
• Complexity.CircuitCode.Machine.Internal.familyStream? code input = if input.isEmpty = true then none else none

theorem Complexity.CircuitCode.Machine.Internal.familyStream?_eq_evalFamilyCode (code input : List Bool) : familyStream? code input = evalFamilyCode code input

The controller-shaped pure stream retains evalFamilyCode as its exact external specification.