One streaming raw-gate step

This definitions layer couples raw-gate code emission with incrementing the binary counter that records the first unused circuit wire. It is the atomic append operation used by circuit serializers.

structure Complexity.CircuitCode.Machine.RawGateStepDistinct {n : ℕ} (emitCounterIdx availableIdx input₀Idx input₁Idx : Fin n) : Prop

Separation conditions for the mutable first-unused-wire counter, the emitter's zero scratch, and its two preserved reference tapes. The two references may coincide, which is useful for copy and constant gates.

• emitCounter_ne_available : emitCounterIdx ≠ availableIdx

  The emitter scratch is not the first-unused-wire counter.

• emitCounter_ne_input₀ : emitCounterIdx ≠ input₀Idx

  The emitter scratch is not the first reference.

• emitCounter_ne_input₁ : emitCounterIdx ≠ input₁Idx

  The emitter scratch is not the second reference.

• available_ne_input₀ : availableIdx ≠ input₀Idx

  The mutable wire counter is not the first preserved reference.

• available_ne_input₁ : availableIdx ≠ input₁Idx

  The mutable wire counter is not the second preserved reference.

def Complexity.CircuitCode.Machine.emitRawGateStepTM {n : ℕ} (op : AndOrOp) (negated₀ negated₁ : Bool) (emitCounterIdx availableIdx input₀Idx input₁Idx : Fin n) : TM n

Emit one raw gate from two binary reference tapes, then increment the canonical binary first-unused-wire counter.

Equations

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

def Complexity.CircuitCode.Machine.emitRawGateStepTime (available input₀ input₁ : ℕ) : ℕ

Compositional running-time bound for one streaming gate step.

Equations

• Complexity.CircuitCode.Machine.emitRawGateStepTime available input₀ input₁ = Complexity.CircuitCode.Machine.emitRawGateTime input₀ input₁ + 1 + Complexity.TM.binarySuccTime available

def Complexity.CircuitCode.Machine.emitRawGateStepSpace (initialSpace available input₀ input₁ : ℕ) : ℕ

All-prefix space bound for one streaming gate step.

Equations

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