Proof-carrying binary stream routines

BinaryRoutine is an experimental composition layer for append-only machines whose complete work state is a vector of canonical rewound binary naturals. Each routine carries a pure domain, exact value-vector effect, exact emitted word, and explicit time/all-prefix-space bounds. BinaryRoutine.Sound ties those fields to one HoareTimeSpace contract and transducer proof on every canonical state in the domain.

The pure domain is deliberate: predecessor honestly requires a positive value, while copying and gate emission honestly require their reusable scratch value to be zero. Sequential composition conjoins those obligations at the correct intermediate value vector. Loop, branch, and polynomial adapters are outside this initial layer.

Main results

• BinaryRoutine.Sound.seq composes proofs across seqTM.
• BinaryRoutine.identity_sound proves the empty-emission identity.
• BinaryRoutine.emitBits_sound adapts fixed-word emission.
• BinaryRoutine.binarySucc_sound and binaryPred_sound adapt arithmetic.
• BinaryRoutine.binaryCopy_sound adapts framed canonical copying.
• BinaryRoutine.emitRawGateStep_sound adapts one streaming raw gate.

theorem Complexity.BinaryRoutine.natTape_hasBinaryNat (value : ℕ) : (natTape value).HasBinaryNat value

The canonical tape realizes its advertised natural value.

theorem Complexity.BinaryRoutine.natTape_parked (value : ℕ) : TM.Parked (natTape value)

Every canonical binary natural tape is parked.

theorem Complexity.BinaryRoutine.workTapes_hasBinaryNat {n : ℕ} (values : BinaryValues n) (i : Fin n) : (workTapes values i).HasBinaryNat (values i)

Each tape in a canonical work vector realizes its corresponding value.

theorem Complexity.BinaryRoutine.workTapes_parked {n : ℕ} (values : BinaryValues n) (i : Fin n) : TM.Parked (workTapes values i)

Every tape in a canonical work vector is parked.

theorem Complexity.BinaryRoutine.workTapes_update {n : ℕ} (values : BinaryValues n) (idx : Fin n) (value : ℕ) : workTapes (Function.update values idx value) = Function.update (workTapes values) idx (natTape value)

Updating one pure value is exactly a literal update of its canonical tape.

theorem Complexity.BinaryRoutine.Sound.seq {n : ℕ} {first second : BinaryRoutine n} (hfirst : first.Sound) (hsecond : second.Sound) : (first.seq second).Sound

Sound routines compose, with second-phase obligations and bounds evaluated at the first routine's exact value effect.

theorem Complexity.BinaryRoutine.Sound.restrict {n : ℕ} {routine : BinaryRoutine n} (hsound : routine.Sound) (requires : BinaryValues n → Prop) (hrequires : ∀ (values : BinaryValues n), requires values → routine.requires values) : (routine.restrict requires).Sound

Strengthening a routine's pure precondition preserves soundness without changing its concrete behavior or resource bounds.

theorem Complexity.BinaryRoutine.emitBits_sound {n : ℕ} (word : List Bool) : (emitBits word).Sound

Fixed-word emission is sound; its all-prefix bound is obtained honestly from its exact running time.

theorem Complexity.BinaryRoutine.identity_sound {n : ℕ} : identity.Sound

Empty fixed-word emission is a sound routine identity.

theorem Complexity.BinaryRoutine.binarySucc_sound {n : ℕ} (idx : Fin n) : (binarySucc idx).Sound

Canonical binary successor is a sound value-vector leaf.

theorem Complexity.BinaryRoutine.binaryPred_sound {n : ℕ} (idx : Fin n) : (binaryPred idx).Sound

Canonical positive binary predecessor is a sound value-vector leaf. Its routine domain is exactly 0 < values idx.

theorem Complexity.BinaryRoutine.binaryCopy_sound {n : ℕ} (srcIdx dstIdx counterIdx : Fin n) : (binaryCopy srcIdx dstIdx counterIdx).Sound

Framed canonical binary copying is sound when the three indices are distinct; its routine domain records that the private counter value is zero.

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

One raw-gate stream step is a sound routine leaf. Its pure effect advances only availableIdx, and its emitted word is exactly RawGate.encode.