The counting loop's body

⚠️ Unreviewed by Bolton

The body of the counting loop advances the count and one of the two tallies. Which tally it advances is decided by the simulated path's verdict, and TM.ifTM is the combinator that reads a verdict and branches — but it reads the output tape, so the verdict must already have been published there, which is what TM.writeOutputBitTM is for.

This file builds the arithmetic end of the body: given the verdict in the output tape's slot, bump the chosen tally, bump the count, and blank the slot again for the next pass.

Main results

• TM.binarySuccTM_hoareTime_pinned, TM.binaryRippleSubTM_hoareTime_pinned — the successor and truncated subtraction, with fully named result banks
• TM.condBumpTM, TM.condBumpTM_hoareTime — bump one of two registers according to the published verdict
• TM.tallyBumpTM, TM.tallyBumpTM_hoareTime — that bump, the count's bump, and the blanking of the verdict slot, chained through named banks

theorem Complexity.TM.binarySuccTM_hoareTime_pinned {n : ℕ} (idx : Fin n) (value : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hvalue : work₀ idx = natTape value) (hinp : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ idx → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : (binarySuccTM idx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = Function.update work₀ idx (natTape (value + 1)) ∧ out = out₀) (binarySuccTime value)

The canonical successor, with the result bank named. Tape.HasBinaryNat determines a tape outright, so the library's contract — which reports the new value rather than the new tape — can be sharpened to a pinned one, which is what the chaining rules consume.

def Complexity.TM.condBumpTM {n : ℕ} (aIdx rIdx : Fin n) : TM n

Bump one of two registers, according to the verdict already in the output slot. The test stage is TM.skipTM: the verdict is published before the branch is reached, so the conditional has nothing left to compute.

Equations

• Complexity.TM.condBumpTM aIdx rIdx = Complexity.TM.skipTM.ifTM (Complexity.TM.binarySuccTM aIdx) (Complexity.TM.binarySuccTM rIdx)

theorem Complexity.TM.condBumpTM_hoareTime {n : ℕ} (aIdx rIdx : Fin n) (a r : ℕ) (b : Bool) (s : Γw) (hb : s = Γw.one ↔ b = true) (I : Tape) (W : Fin n → Tape) (hI : Parked I) (hIz : I.cells 0 = Γ.start) (hW : ∀ (j : Fin n), Parked (W j)) (hWz : ∀ (j : Fin n), (W j).cells 0 = Γ.start) (ha : W aIdx = natTape a) (hr : W rIdx = natTape r) : (condBumpTM aIdx rIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I ∧ work = W ∧ out = NTM.outSlot s) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I ∧ (work = if b = true then Function.update W aIdx (natTape (a + 1)) else Function.update W rIdx (natTape (r + 1))) ∧ out = NTM.outSlot s) (1 + 1 + max (binarySuccTime a) (binarySuccTime r) + 5)

The conditional bump's contract. The verdict b sitting in the output slot selects which register grows; the slot itself is untouched, since the branch reads it and nothing writes it.

def Complexity.TM.tallyBumpTM {n : ℕ} (cIdx aIdx rIdx zIdx : Fin n) : TM n

The arithmetic end of the loop body. Bump the selected tally, bump the count, and blank the verdict slot so the next pass starts from the state the loop's invariant describes.

Equations

• Complexity.TM.tallyBumpTM cIdx aIdx rIdx zIdx = Complexity.TM.bigSeqTM [Complexity.TM.condBumpTM aIdx rIdx, Complexity.TM.binarySuccTM cIdx, Complexity.TM.writeOutputBitTM zIdx]

theorem Complexity.TM.tallyBumpTM_hoareTime {n : ℕ} (cIdx aIdx rIdx zIdx : Fin n) (hca : cIdx ≠ aIdx) (hcr : cIdx ≠ rIdx) (hzc : zIdx ≠ cIdx) (hza : zIdx ≠ aIdx) (hzr : zIdx ≠ rIdx) (v a r : ℕ) (b : Bool) (s : Γw) (hb : s = Γw.one ↔ b = true) (I : Tape) (W : Fin n → Tape) (hI : Parked I) (hIz : I.cells 0 = Γ.start) (hW : ∀ (j : Fin n), Parked (W j)) (hWz : ∀ (j : Fin n), (W j).cells 0 = Γ.start) (hcv : W cIdx = natTape v) (ha : W aIdx = natTape a) (hr : W rIdx = natTape r) (hz : (W zIdx).read = Γ.blank) : (tallyBumpTM cIdx aIdx rIdx zIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I ∧ work = W ∧ out = NTM.outSlot s) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = I ∧ work = Function.update (if b = true then Function.update W aIdx (natTape (a + 1)) else Function.update W rIdx (natTape (r + 1))) cIdx (natTape (v + 1)) ∧ out = NTM.outSlot Γw.blank) (3 * (max (1 + 1 + max (binarySuccTime a) (binarySuccTime r) + 5) (binarySuccTime v) + 1) + 1)

The arithmetic end of the loop body, contracted. Every intermediate bank is named, so the three stages chain through TM.bigSeqTM_hoareTime_pinned with no existential in sight.

theorem Complexity.TM.binaryRippleSubTM_hoareTime_pinned {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) (hdistinct : BinaryRippleSubDistinct lhsIdx rhsIdx resultIdx) (lhs rhs : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hlhs : work₀ lhsIdx = natTape lhs) (hrhs : work₀ rhsIdx = natTape rhs) (hres : (work₀ resultIdx).HasBinaryNat 0) (hinput : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ lhsIdx → i ≠ rhsIdx → i ≠ resultIdx → Parked (work₀ i)) (houtput : Parked out₀) : (binaryRippleSubTM lhsIdx rhsIdx resultIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = Function.update work₀ resultIdx (natTape (lhs - rhs)) ∧ out = out₀) (binaryRippleSubTime lhs rhs)

Truncated subtraction, with the result bank named. As with the successor, the library reports the new values; since Tape.HasBinaryNat determines a tape, the operands come back literally unchanged and only the result register moves.