Canonical binary count-up loops — Hoare-style driver, internal proofs

BinaryForLoopSpec asks a client for a canonical configuration at every loop index, which presumes a body whose tape effect is available in closed form. Bodies assembled from Hoare triples do not have that shape: their contracts only assert that some halting run exists. This module closes the gap by running the loop composition directly on existential contracts, so a client needs nothing but a per-index triple for its body.

theorem Complexity.TM.Parked.of_hasBinaryNat {t : Tape} {value : ℕ} (h : t.HasBinaryNat value) : Parked t

A canonical binary tape is parked: its head sits off the left marker and no cell to the right of cell zero holds ▷.

theorem Complexity.TM.binaryForTM_hoareTime_internal {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. A body that carries the loop frame from value to the pre-successor postcondition at every index runs the whole loop, from counter zero to the limit, within the advertised time.

def Complexity.TM.binaryForAdv {k : ℕ} {body : TM (k + 1)} (Adv : body.Q → Bool) (counterIdx limitIdx : Fin (k + 1)) : (body.binaryForTM counterIdx limitIdx).Q → Bool

The advancing states of a count-up loop are the body's, taken inside the composite iteration. The driver and the counter's successor never consult the guess tape.

Equations

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

theorem Complexity.TM.guessProtocol_binarySuccTM {k : ℕ} (idx : Fin (k + 1)) (hidx : idx ≠ Fin.last k) : (binarySuccTM idx).GuessProtocol fun (x : (binarySuccTM idx).Q) => false

Canonical successor never consults the guess tape.

theorem Complexity.TM.guessProtocol_binaryForTM_internal {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 reads and rewrites only the counter, the limit, and whatever the body touches, so a body that consumes its guesses in the advancing states keeps doing so inside the loop.