The counting loop's test

⚠️ Unreviewed by Bolton

TM.loopTM stops when its test machine leaves 1 in the output tape's verdict cell. The counting loop stops when its counter reaches the horizon, so its test compares the counter against a register holding that horizon and publishes the answer.

The comparison itself is TM.binaryEqTM, which deposits its verdict as a bit on a scratch work tape and leaves the output alone; the remaining three stages move that bit where the loop can see it. Two of them exist only because of where heads end up: TM.binaryEqTM leaves its operands' heads wherever the scan stopped, and TM.writeOutputBitTM publishes whatever is under a head, so the operands must be rewound before the verdict can be read off.

Main results

• TM.testTailTM — rewind, publish the verdict, clear the scratch bit
• TM.testTailTM_hoareTime — its contract, through fully pinned tape states
• TM.tallyTestTM, TM.tallyTestTM_hoareTime — the whole test, leaving its bank as it found it
• NTM.tallyTestTM_hoareTime_tallyPost — the same contract in the shape NTM.tallyLoop_hoareTime_of_hoare asks for
• TM.Parked.write_ne_start — a frame fact the assembly needs

def Complexity.TM.testTargets {n : ℕ} (cIdx nIdx resIdx : Fin n) : List (Fin n)

The three tapes the comparison touches, in the order the rewind visits them.

Equations

• Complexity.TM.testTargets cIdx nIdx resIdx = [cIdx, nIdx, resIdx]

def Complexity.TM.rewoundBank {n : ℕ} (cIdx nIdx resIdx : Fin n) (W : Fin n → Tape) : Fin n → Tape

The work bank after every compared tape has been rewound to cell one.

Equations

• Complexity.TM.rewoundBank cIdx nIdx resIdx W j = if j ∈ Complexity.TM.testTargets cIdx nIdx resIdx then { head := 1, cells := (W j).cells } else W j

def Complexity.TM.testTailTM {n : ℕ} (cIdx nIdx resIdx : Fin n) : TM n

The tail of the counting loop's test. Rewind the compared tapes, publish the scratch bit onto the output, then clear the scratch tape for the next iteration.

Equations

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

theorem Complexity.TM.rewoundBank_parked {n : ℕ} {cIdx nIdx resIdx : Fin n} {W : Fin n → Tape} (hW : ∀ (j : Fin n), Parked (W j)) (j : Fin n) : Parked (rewoundBank cIdx nIdx resIdx W j)

theorem Complexity.TM.Parked.write_ne_start {t : Tape} (h : Parked t) {s : Γ} (hs : s ≠ Γ.start) : Parked (t.write s)

Writing a non-marker symbol keeps a parked tape parked.

theorem Complexity.TM.testTailTM_hoareTime {n : ℕ} (cIdx nIdx resIdx : Fin n) (hd : BinaryEqDistinct cIdx nIdx resIdx) (b : Bool) (B : ℕ) (hB : 1 ≤ B) (I : Tape) (W : Fin n → Tape) (O : Tape) (hI : Parked I) (hO : Parked O) (hW : ∀ (j : Fin n), Parked (W j)) (hstart : ∀ j ∈ testTargets cIdx nIdx resIdx, (W j).cells 0 = Γ.start ∧ (W j).head ≤ B) (hres : (W resIdx).cells 1 = Γ.ofBool b) (hresBlank : ∀ (i : ℕ), 2 ≤ i → (W resIdx).cells i = Γ.blank) : (testTailTM cIdx nIdx resIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I ∧ work = W ∧ out = O) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I ∧ work = Function.update (rewoundBank cIdx nIdx resIdx W) resIdx ((Tape.init []).move Dir3.right) ∧ out = O.write (Γ.ofBool b)) (3 * (max (3 * (B + 3) + 1) (resetBinaryWorkTime B 1) + 1) + 1)

The contract of the test's tail. From a bank in which the compared tapes carry their markers and the scratch tape carries the verdict bit, the three stages land on a fully named bank — every compared tape at cell one, the scratch tape blank — with the verdict on the output.

def Complexity.TM.tallyTestTM {n : ℕ} (cIdx nIdx resIdx : Fin n) : TM n

The counting loop's test. Compare the counter against the horizon register, then move the verdict where TM.loopTM looks for it.

Equations

• Complexity.TM.tallyTestTM cIdx nIdx resIdx = (Complexity.TM.binaryEqTM cIdx nIdx resIdx).seqTM (Complexity.TM.testTailTM cIdx nIdx resIdx)

theorem Complexity.TM.tallyTestTM_hoareTime {n : ℕ} (cIdx nIdx resIdx : Fin n) (hd : BinaryEqDistinct cIdx nIdx resIdx) (v N B : ℕ) (I : Tape) (W : Fin n → Tape) (O : Tape) (hI : Parked I) (hIz : I.cells 0 = Γ.start) (hO : Parked O) (hOz : O.cells 0 = Γ.start) (hW : ∀ (j : Fin n), Parked (W j)) (hWz : ∀ (j : Fin n), (W j).cells 0 = Γ.start) (hc : W cIdx = natTape v) (hnn : W nIdx = natTape N) (hres : W resIdx = (Tape.init []).move Dir3.right) (hB : ∀ (j : Fin n), (W j).head + binaryEqTime v.bits N.bits ≤ B) : (tallyTestTM cIdx nIdx resIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I ∧ work = W ∧ out = O) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I ∧ work = W ∧ out = O.write (Γ.ofBool (decide (v = N)))) (binaryEqTime v.bits N.bits + 1 + (3 * (max (3 * (B + 3) + 1) (resetBinaryWorkTime B 1) + 1) + 1))

The test's contract. The bank comes back exactly as it went in — the comparison is non-destructive and the scratch tape is cleared — and the output gains the verdict bit.

theorem Complexity.NTM.outSlot_write (s s' : Γw) : (outSlot s).write s'.toΓ = outSlot s'

Writing into the verdict slot replaces its symbol. The slot's head never leaves cell one, so a write lands exactly on the cell TM.loopTM inspects.

theorem Complexity.NTM.outSlot_blank_write (b : Bool) : (outSlot Γw.blank).write (Γ.ofBool b) = outSlot (if b = true then Γw.one else Γw.zero)

Writing the verdict into a blank slot produces the slot holding that verdict.

theorem Complexity.NTM.outSlot_blank_eq_blankTape : outSlot Γw.blank = TM.blankTape

The blank verdict slot is the blank tape — the same object under two names, which is what lets the wipe's precondition and the loop's invariant meet.

theorem Complexity.NTM.readBackWrite_eq_one_iff (s : Γ) : TM.readBackWrite s = Γw.one ↔ s = Γ.one

Reading a cell back as a writable symbol turns it into 1 exactly when it was 1.

theorem Complexity.NTM.publish_hoareTime {n : ℕ} (idx : Fin n) (I : Tape) (W : Fin n → Tape) (hI : TM.Parked I) (hW : ∀ (j : Fin n), TM.Parked (W j)) (hv : (W idx).head = 1) : (TM.writeOutputBitTM idx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I ∧ work = W ∧ out = TM.blankTape) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I ∧ work = W ∧ out = outSlot (TM.readBackWrite ((W idx).cells 1))) 1

The body's publishing stage. With the verdict tape rewound to cell one, its symbol is copied into the output slot, where TM.ifTM can branch on it.

theorem Complexity.NTM.natTape_cells_zero (v : ℕ) : (natTape v).cells 0 = Γ.start

The marker sits at cell zero of a counter tape.

theorem Complexity.NTM.tallyTestTM_hoareTime_tallyPost {n : ℕ} (cIdx aIdx rIdx nIdx resIdx : Fin n) (hd : TM.BinaryEqDistinct cIdx nIdx resIdx) (hnc : nIdx ≠ cIdx) (hna : nIdx ≠ aIdx) (hnr : nIdx ≠ rIdx) (hsc : resIdx ≠ cIdx) (hsa : resIdx ≠ aIdx) (hsr : resIdx ≠ rIdx) (I : Tape) (rest : Fin n → Tape) (P : ℕ → Bool) (N w B Hr : ℕ) (hI : TM.Parked I) (hIz : I.cells 0 = Γ.start) (hrest : ∀ (j : Fin n), TM.Parked (rest j)) (hrestz : ∀ (j : Fin n), (rest j).cells 0 = Γ.start) (hresth : ∀ (j : Fin n), (rest j).head ≤ Hr) (hn : rest nIdx = natTape N) (hr : rest resIdx = (Tape.init []).move Dir3.right) (hB : Hr + 1 + TM.binaryEqTime w.bits N.bits ≤ B) : (TM.tallyTestTM cIdx nIdx resIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I ∧ work = tallyWork cIdx aIdx rIdx rest (w, tally P w, tally (fun (u : ℕ) => !P u) w) ∧ out = outSlot Γw.blank) (tallyPost cIdx aIdx rIdx I rest P N w) (TM.binaryEqTime w.bits N.bits + 1 + (3 * (max (3 * (B + 3) + 1) (TM.resetBinaryWorkTime B 1) + 1) + 1))

The counting loop's test meets its obligation. With the horizon parked on nIdx and a blank scratch tape on resIdx, TM.tallyTestTM carries the state the body leaves — the bank at index w and a blank verdict slot — to NTM.tallyPost at that index.