Derived register arithmetic

Addition, copying, and multiply-accumulate over unary registers, composed from forRegTM, incRegTM, and clearRegTM — no new hand-rolled machines. Each spec is one application of forRegTM_hoareTime with an iteration-indexed ghost family, plus Function.update bookkeeping.

Time bounds are deliberately loose (rounded up via HoareTime.mono_bound); only their polynomial shape matters downstream.

def Complexity.TM.addIntoTM {n : ℕ} (src dst : Fin n) : TM n

dst += src (repeat-increment, fueled by src).

Equations

• Complexity.TM.addIntoTM src dst = (Complexity.TM.incRegTM dst).forRegTM src

theorem Complexity.TM.addIntoTM_hoareTime {n : ℕ} (src dst : Fin n) (hne : src ≠ dst) (a b : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), i ≠ src → Parked (work₀ i)) (hsrc : work₀ src = regTape a) (hdst : work₀ dst = regTape b) : (addIntoTM src dst).HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ (Function.update work₀ dst (regTape (b + a))) ys) (a * (2 * (b + a) + 4 + 2) + (a + 2))

addIntoTM Hoare specification. From regTape a in src and regTape b in dst, reach regTape (b + a) in dst; src and everything else untouched.

def Complexity.TM.copyIntoTM {n : ℕ} (src dst : Fin n) : TM n

dst := src (clear then add).

Equations

• Complexity.TM.copyIntoTM src dst = (Complexity.TM.clearRegTM dst).seqTM (Complexity.TM.addIntoTM src dst)

theorem Complexity.TM.copyIntoTM_hoareTime {n : ℕ} (src dst : Fin n) (hne : src ≠ dst) (a b : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), i ≠ src → Parked (work₀ i)) (hsrc : work₀ src = regTape a) (hdst : work₀ dst = regTape b) : (copyIntoTM src dst).HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ (Function.update work₀ dst (regTape a)) ys) (2 * b + 4 + 1 + (a * (2 * (0 + a) + 4 + 2) + (a + 2)))

copyIntoTM Hoare specification.

def Complexity.TM.mulAddIntoTM {n : ℕ} (src₁ src₂ dst : Fin n) : TM n

dst += src₁ * src₂ (repeat-add, fueled by src₁).

Equations

• Complexity.TM.mulAddIntoTM src₁ src₂ dst = (Complexity.TM.addIntoTM src₂ dst).forRegTM src₁

def Complexity.TM.mulAddBound (a b d : ℕ) : ℕ

The (loose) per-iteration budget of mulAddIntoTM.

Equations

• Complexity.TM.mulAddBound a b d = b * (2 * (d + a * b + b) + 4 + 2) + (b + 2)

theorem Complexity.TM.mulAddIntoTM_hoareTime {n : ℕ} (src₁ src₂ dst : Fin n) (h12 : src₁ ≠ src₂) (h1d : src₁ ≠ dst) (h2d : src₂ ≠ dst) (a b d : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), i ≠ src₁ → Parked (work₀ i)) (h1 : work₀ src₁ = regTape a) (h2 : work₀ src₂ = regTape b) (hd : work₀ dst = regTape d) : (mulAddIntoTM src₁ src₂ dst).HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ (Function.update work₀ dst (regTape (d + a * b))) ys) (a * (mulAddBound a b d + 2) + (a + 2))

mulAddIntoTM Hoare specification. From regTape a, regTape b, regTape d in src₁, src₂, dst, reach regTape (d + a·b) in dst.

def Complexity.TM.iterTM {n : ℕ} (m : TM n) : ℕ → TM n

Run m in sequence c times.

Equations

• m.iterTM 0 = Complexity.TM.skipTM
• m.iterTM c.succ = m.seqTM (m.iterTM c)

theorem Complexity.TM.iterTM_incRegTM_hoareTime {n : ℕ} (q : Fin n) (c d : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) : Parked inp₀ → (∀ (i : Fin n), Parked (work₀ i)) → work₀ q = regTape d → ((incRegTM q).iterTM c).HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ (Function.update work₀ q (regTape (d + c))) ys) (c * (2 * (d + c) + 5) + 1)

Iterated increment: add the constant c to register q.