Proof-carrying binary stream routines -- definitions

A binary routine operates on a vector of natural numbers represented by canonical rewound Nat.bits tapes. It may update that pure vector and append a value-dependent word to an output accumulator. A value-level precondition supports honest partial leaves such as positive predecessor and zero-scratch copying without weakening the canonical state model.

@[reducible, inline]

abbrev Complexity.BinaryValues (n : ℕ) : Type

Pure values represented by all work tapes of a binary routine.

Equations

• Complexity.BinaryValues n = (Fin n → ℕ)

def Complexity.BinaryRoutine.natTape (value : ℕ) : Tape

Canonical rewound tape representation of one natural number.

Equations

• Complexity.BinaryRoutine.natTape value = (Complexity.Tape.init (List.map Complexity.Γ.ofBool value.bits)).move Complexity.Dir3.right

def Complexity.BinaryRoutine.workTapes {n : ℕ} (values : BinaryValues n) : Fin n → Tape

Canonical work-tape vector corresponding to values.

Equations

• Complexity.BinaryRoutine.workTapes values i = Complexity.BinaryRoutine.natTape (values i)

def Complexity.BinaryRoutine.CanonicalPred {n : ℕ} (inp₀ : Tape) (values : BinaryValues n) (ys : List Bool) : TapePred n

A fixed parked input, canonical binary work vector, and append accumulator.

Equations

• Complexity.BinaryRoutine.CanonicalPred inp₀ values ys = Complexity.TM.EmitPred inp₀ (Complexity.BinaryRoutine.workTapes values) ys

structure Complexity.BinaryRoutine (n : ℕ) : Type 1

A concrete streaming machine paired with its pure value effect, emitted word, domain, and explicit time/all-prefix-space bounds.

• machine : TM n

  Concrete machine implementing the routine.

• requires : BinaryValues n → Prop

  Pure value-level domain on which the routine contract holds.

• effect : BinaryValues n → BinaryValues n

  Exact pure work-vector effect.

• emitted : BinaryValues n → List Bool

  Exact word appended from each starting value vector.

• timeBound : BinaryValues n → ℕ

  Time bound from each starting value vector.

• spaceBound : ℕ → BinaryValues n → ℕ

  All-prefix auxiliary-space bound from an initial work budget.

structure Complexity.BinaryRoutine.Sound {n : ℕ} (routine : BinaryRoutine n) : Prop

Soundness of a proof-carrying routine on every canonical state in its value-level domain. The input tape is fixed and parked for each invocation; initialSpace ≥ 1 covers the canonical work heads at cell one.

• hoareTimeSpace (values : BinaryValues n) (inp₀ : Tape) (ys : List Bool) (inputLength initialSpace : ℕ) : routine.requires values → TM.Parked inp₀ → 1 ≤ initialSpace → inp₀.head ≤ inputLength + initialSpace + 1 → routine.machine.HoareTimeSpace (CanonicalPred inp₀ values ys) (CanonicalPred inp₀ (routine.effect values) (ys ++ routine.emitted values)) (routine.timeBound values) inputLength (routine.spaceBound initialSpace values)

  Exact endpoint, time, and all-reachable space contract.

• isTransducer : routine.machine.IsTransducer

  The routine never moves its output head left.

def Complexity.BinaryRoutine.emitBits {n : ℕ} (word : List Bool) : BinaryRoutine n

Append a fixed word without changing the binary work vector.

Equations

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

def Complexity.BinaryRoutine.identity {n : ℕ} : BinaryRoutine n

Empty fixed-word emission is the canonical routine identity.

Equations

• Complexity.BinaryRoutine.identity = Complexity.BinaryRoutine.emitBits []

def Complexity.BinaryRoutine.seq {n : ℕ} (first second : BinaryRoutine n) : BinaryRoutine n

Sequential composition, including the concrete seqTM seam step.

Equations

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

def Complexity.BinaryRoutine.restrict {n : ℕ} (routine : BinaryRoutine n) (requires : BinaryValues n → Prop) : BinaryRoutine n

Replace a routine's public pure precondition while preserving its concrete machine, effect, emitted word, and resource bounds exactly. Soundness requires the replacement precondition to imply the original one.

Equations

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

def Complexity.BinaryRoutine.binarySucc {n : ℕ} (idx : Fin n) : BinaryRoutine n

Increment one canonical binary work value.

Equations

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

def Complexity.BinaryRoutine.binaryPred {n : ℕ} (idx : Fin n) : BinaryRoutine n

Decrement one positive canonical binary work value.

Equations

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

def Complexity.BinaryRoutine.binaryCopy {n : ℕ} (srcIdx dstIdx counterIdx : Fin n) : BinaryRoutine n

Copy one canonical binary value into another using a zero scratch counter.

Equations

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

def Complexity.BinaryRoutine.emitRawGateStep {n : ℕ} (op : AndOrOp) (negated₀ negated₁ : Bool) (emitCounterIdx availableIdx input₀Idx input₁Idx : Fin n) : BinaryRoutine n

Emit one raw gate and advance the first-unused-wire value.

Equations

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