forRegTM: the register-fueled loop combinator

forRegTM body r runs body once per mark of register r. The fuel is the head position on r: the register's cells are never written; the test reads the cell under the head — a mark means "iterate" (consume = move right, run the body), the first blank means "exit" (rewind r to cell 1 and halt). The body must leave r untouched (our ghost-style specs guarantee this for free, since bodies preserve every non-target tape literally).

This is the only loop mechanism of the reduction emitter (docs/A5-ReductionEmitter.md): unlike loopTM, its test reads a work tape, so the output tape remains an append-only accumulator throughout.

The Hoare rule forRegTM_hoareTime threads an iteration-indexed family of ghost work-tape functions and output words through the loop.

inductive Complexity.TM.ForPhase : Type

Driver phases of forRegTM: test reads the fuel register's cell (mark = iterate, blank = exit), rewind returns the register head to cell 1, done is the halt state.

• test : ForPhase
• rewind : ForPhase
• done : ForPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqForPhase : DecidableEq ForPhase

Equations

• Complexity.TM.instDecidableEqForPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypeForPhase : Fintype ForPhase

ForPhase is a finite type (it has exactly three constructors).

Equations

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

def Complexity.TM.forRegTM {n : ℕ} (body : TM n) (r : Fin n) : TM n

Register-fueled loop: run body once per mark of register r. States: the driver phases on the left, the body's states on the right.

Equations

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

theorem Complexity.TM.forRegTM_hoareTime {n : ℕ} (body : TM n) (r : Fin n) (v : ℕ) (inp₀ : Tape) (w : ℕ → Fin n → Tape) (ys : ℕ → List Bool) (b_iter : ℕ) (hinp₀ : Parked inp₀) (hwreg : ∀ (i : ℕ), w i r = regTape v) (hwP : ∀ (i : ℕ) (j : Fin n), j ≠ r → Parked (w i j)) (hbody : ∀ i < v, body.HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = Function.update (w i) r { head := i + 2, cells := regCells v } ∧ OutAcc (ys i) out) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = Function.update (w (i + 1)) r { head := i + 2, cells := regCells v } ∧ OutAcc (ys (i + 1)) out) b_iter) : (body.forRegTM r).HoareTime (EmitPred inp₀ (w 0) (ys 0)) (EmitPred inp₀ (w v) (ys v)) (v * (b_iter + 2) + (v + 2))

forRegTM Hoare rule. Given a fuel register holding v (whose tape the iteration-indexed ghost family w never changes) and a body spec carrying w i / ys i to w (i+1) / ys (i+1), the loop carries w 0 / ys 0 to w v / ys v in at most v·(b_iter + 2) + v + 3 steps.