Canonical binary count-up loops

This module exposes an output-safe bounded loop whose counter and preserved limit use canonical little-endian binary work tapes. Under the certified invariant counter ≤ limit, every test scans the full limit width, so a comparison has the value-independent exact time 2 * limit.size + 2. A nonterminal test runs the supplied body, increments the counter, and returns to a fresh test; equality halts with both binary tapes rewound.

The generic certificates keep body-specific facts explicit. In particular, the loop driver does not assume that an arbitrary body preserves its counter, limit, or tape frames. Clients record those endpoint facts in BinaryForLoopSpec and the corresponding prefix-space facts in BinaryForLoopSpaceSpec.

Main results

• binaryForTM_compare_reachesIn_frame gives the exact framed comparison.
• BinaryForLoopSpec.reachesIn composes a certified loop exactly.
• BinaryForLoopSpaceSpec.prefix_withinAuxSpace covers every run prefix.
• IsTransducer.binaryForTM preserves one-way output safety.
• binaryForTM_hoareTime runs the loop from a per-index contract for its body, for clients whose bodies come as Hoare triples rather than closed forms.
• guessProtocol_binaryForTM carries a body's guess-tape discipline through the loop, so a nondeterministic body may be driven by one.

theorem Complexity.TM.binaryForTM_compare_reachesIn_frame_of_eq {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) (hne : counterIdx ≠ limitIdx) (value : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hcounter : (work₀ counterIdx).HasBinaryNat value) (hlimit : (work₀ limitIdx).HasBinaryNat value) (hinp : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ counterIdx → i ≠ limitIdx → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : (body.binaryForTM counterIdx limitIdx).reachesIn (binaryForCompareTime value) { state := Sum.inl (BinaryForPhase.scan true), input := inp₀, work := work₀, output := out₀ } { state := Sum.inl BinaryForPhase.done, input := inp₀, work := work₀, output := out₀ }

At equality, one full-width comparison preserves every tape and reaches the final driver configuration in exact time.

theorem Complexity.TM.binaryForTM_compare_reachesIn_frame_of_lt {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) (hne : counterIdx ≠ limitIdx) (value limitValue : ℕ) (hlt : value < limitValue) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hcounter : (work₀ counterIdx).HasBinaryNat value) (hlimit : (work₀ limitIdx).HasBinaryNat limitValue) (hinp : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ counterIdx → i ≠ limitIdx → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : (body.binaryForTM counterIdx limitIdx).reachesIn (binaryForCompareTime limitValue) { state := Sum.inl (BinaryForPhase.scan true), input := inp₀, work := work₀, output := out₀ } { state := Sum.inr (body.binaryForIterationTM counterIdx).qstart, input := inp₀, work := work₀, output := out₀ }

Strictly below the limit, one full-width comparison preserves every tape and reaches the composite iteration start in exact time.

theorem Complexity.TM.binaryForTM_compare_reachesIn_frame {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) (hne : counterIdx ≠ limitIdx) (value limitValue : ℕ) (hle : value ≤ limitValue) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hcounter : (work₀ counterIdx).HasBinaryNat value) (hlimit : (work₀ limitIdx).HasBinaryNat limitValue) (hinp : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ counterIdx → i ≠ limitIdx → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : ∃ (c' : Cfg n (body.binaryForTM counterIdx limitIdx).Q), (body.binaryForTM counterIdx limitIdx).reachesIn (binaryForCompareTime limitValue) { state := Sum.inl (BinaryForPhase.scan true), input := inp₀, work := work₀, output := out₀ } c' ∧ c'.input = inp₀ ∧ c'.work = work₀ ∧ c'.output = out₀ ∧ (c'.state = Sum.inr (body.binaryForIterationTM counterIdx).qstart ↔ value < limitValue) ∧ (c'.state = Sum.inl BinaryForPhase.done ↔ value = limitValue)

A bounded canonical comparison has one exact, fully framed endpoint. It enters the composite iteration exactly below the limit and halts exactly at equality.

theorem Complexity.TM.BinaryForLoopSpec.reachesIn {n : ℕ} {body : TM n} {counterIdx limitIdx : Fin n} {bodyTime : ℕ → ℕ} {limitValue : ℕ} (spec : body.BinaryForLoopSpec counterIdx limitIdx bodyTime limitValue) (count value : ℕ) (hlimit : value + count = limitValue) : (body.binaryForTM counterIdx limitIdx).reachesIn (binaryForLoopTime bodyTime limitValue value count) (spec.scanCfg value) spec.doneCfg

A certified count-up loop has its advertised exact remaining run.

theorem Complexity.TM.BinaryForLoopSpaceSpec.scanWithin {n : ℕ} {body : TM n} {counterIdx limitIdx : Fin n} {bodyTime : ℕ → ℕ} {limitValue inputLength spaceBound value : ℕ} {spec : body.BinaryForLoopSpec counterIdx limitIdx bodyTime limitValue} (spaceSpec : BinaryForLoopSpaceSpec spec inputLength spaceBound) (hvalue : value ≤ limitValue) : (spec.scanCfg value).WithinAuxSpace inputLength spaceBound

Every canonical scanner configuration in a certified range satisfies the declared auxiliary-space budget.

theorem Complexity.TM.BinaryForLoopSpaceSpec.doneWithin {n : ℕ} {body : TM n} {counterIdx limitIdx : Fin n} {bodyTime : ℕ → ℕ} {limitValue inputLength spaceBound : ℕ} {spec : body.BinaryForLoopSpec counterIdx limitIdx bodyTime limitValue} (spaceSpec : BinaryForLoopSpaceSpec spec inputLength spaceBound) : spec.doneCfg.WithinAuxSpace inputLength spaceBound

The final configuration of a space-certified loop satisfies its declared auxiliary-space budget.

theorem Complexity.TM.BinaryForLoopSpaceSpec.prefix_withinAuxSpace {n : ℕ} {body : TM n} {counterIdx limitIdx : Fin n} {bodyTime : ℕ → ℕ} {limitValue inputLength spaceBound : ℕ} {spec : body.BinaryForLoopSpec counterIdx limitIdx bodyTime limitValue} (spaceSpec : BinaryForLoopSpaceSpec spec inputLength spaceBound) (count value t : ℕ) (c : Cfg n (body.binaryForTM counterIdx limitIdx).Q) (hlimit : value + count = limitValue) (hreach : (body.binaryForTM counterIdx limitIdx).reachesIn t (spec.scanCfg value) c) (htime : t ≤ binaryForLoopTime bodyTime limitValue value count) : c.WithinAuxSpace inputLength spaceBound

Every prefix of a certified binary count-up loop respects its declared auxiliary-space budget.

theorem Complexity.TM.binaryForTM_hoareTime {n : ℕ} {body : TM n} {counterIdx limitIdx : Fin n} (hne : counterIdx ≠ limitIdx) (limitValue : ℕ) (bodyTime : ℕ → ℕ) (P : ℕ → TapePred n) (hbody : ∀ value < limitValue, body.HoareTime (BinaryForFrame counterIdx limitIdx limitValue P value) (BinaryForBodyPost counterIdx limitIdx limitValue P value) (bodyTime value)) : (body.binaryForTM counterIdx limitIdx).HoareTime (BinaryForFrame counterIdx limitIdx limitValue P 0) (BinaryForFrame counterIdx limitIdx limitValue P limitValue) (binaryForLoopTime bodyTime limitValue 0 limitValue)

A count-up loop from a contract for its body.

BinaryForLoopSpec asks for a canonical configuration at every loop index, which presumes a body whose tape effect is known in closed form. A body assembled from Hoare triples has no such form — its contract only asserts that some halting run exists — so this rule takes the per-index triple directly: if the body carries BinaryForFrame at value to BinaryForBodyPost at value, the driver runs the whole loop from counter zero to limitValue.

theorem Complexity.TM.IsTransducer.binaryForTM {n : ℕ} {body : TM n} (hbody : body.IsTransducer) (counterIdx limitIdx : Fin n) : (body.binaryForTM counterIdx limitIdx).IsTransducer

A binary count-up loop preserves the body's one-way-output discipline.

theorem Complexity.TM.guessProtocol_binaryForTM {k : ℕ} {body : TM (k + 1)} {Adv : body.Q → Bool} (hbody : body.GuessProtocol Adv) (counterIdx limitIdx : Fin (k + 1)) (hcounter : counterIdx ≠ Fin.last k) (hlimit : limitIdx ≠ Fin.last k) : (body.binaryForTM counterIdx limitIdx).GuessProtocol (binaryForAdv Adv counterIdx limitIdx)

The guess protocol survives a count-up loop. The driver rewrites every tape it does not own and holds their heads still, so a body that consumes its guesses only in its advancing states keeps doing so inside the loop. The counter and the limit must not be the guess tape itself.