Machine emission of raw circuit gates — definitions

A serialized raw gate consists of a fixed three-bit header followed by two terminated-unary wire references. The header is baked into finite control; the references are read from preserved canonical binary work tapes. One reusable zero scratch tape drives both natural-code emitters.

def Complexity.CircuitCode.Machine.rawGateHeader (op : AndOrOp) (negated₀ negated₁ : Bool) : List Bool

The fixed operation-and-negation prefix of a serialized raw gate.

Equations

• Complexity.CircuitCode.Machine.rawGateHeader Complexity.AndOrOp.and negated₀ negated₁ = [true, negated₀, negated₁]
• Complexity.CircuitCode.Machine.rawGateHeader Complexity.AndOrOp.or negated₀ negated₁ = [false, negated₀, negated₁]

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

Emit one raw gate from two canonical binary wire-reference tapes.

The scratch tape is restored to zero by each emitNatCodeTM call, so it can be reused for the second reference and by the surrounding stream generator.

Equations

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

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

Concrete time bound for one serialized raw gate.

Equations

• Complexity.CircuitCode.Machine.emitRawGateTime input₀ input₁ = Complexity.CircuitCode.Machine.emitNatCodeTime input₀ + Complexity.CircuitCode.Machine.emitNatCodeTime input₁ + 5

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

All-prefix auxiliary-space bound for one serialized raw gate.

Equations

• Complexity.CircuitCode.Machine.emitRawGateSpace initialSpace input₀ input₁ = initialSpace + 2 * max input₀.size input₁.size + 5