The loop invariant, relative to the initial state `s0`

The loop invariant, relative to the initial state s0. -/ def expInv (N K : ℕ) (X Y : ℤ) (s0 : IState HS) (k : ℕ) (t : IState HS) : Prop := t.G 30 = .int X :: s0.G 30 ∧ t.G 31 = .int Y :: s0.G 31 ∧ t.G 32 = .int (2 ^ N) :: s0.G 32 ∧ t.G 33 = .int k :: s0.G 33 ∧ t.G 34 = .int (expTerm N X Y k).1 :: s0.G 34 ∧ t.G 35 = .int (expTerm N X Y k).2 :: s0.G 35 ∧ t.G 36 = .int (expApprox N k X Y).1 :: s0.G 36 ∧ t.G 37 = .int (expApprox N k X Y).2 :: s0.G 37 ∧ t.G 38 = .int (expTerm N X Y k).1 :: s0.G 38 ∧ t.G 39 = .int ((K : ℤ) - k) :: s0.G 39 ∧ ∀ j : Fin HS, j.val < 30 ∨ 39 < j.val → t.G j = s0.G j theorem exp_body (N K : ℕ) (X Y : ℤ) (s0 t : IState HS) (k : ℕ) (h : expInv N K X Y s0 k t) : expBody.ok t ∧ expInv N K X Y s0 (k + 1) (decSt 39 (expBody.run t)) := by obtain ⟨h30, h31, h32, h33, h34, h35, h36, h37, h38, h39, hj⟩ := h have hpos : (0 : ℤ) < ((k : ℤ) + 1) * 2 ^ N := by positivity refine ⟨?, ?⟩ · simp only [expBody, seqL, RS.ok, run_seq] refine ⟨?, ?, ?, ?, ?, ?⟩ all_goals simp (config := {decide := true}) [Ex.eval, Ex.ok, IState.top, IState.IsInt, Ex.Clean, Ex.regs, Ex.fdiv_regs, zX_all, dvE, nu1E, nu2E, h30, h31, h32, h33, h34, h35, h36, h37, h38, h39] all_goals (apply Ex.fdiv_ok) <;> simp (config := {decide := true}) [Ex.eval, Ex.ok, IState.top, IState.IsInt, Ex.fdiv_eval, h30, h31, h32, h33, h34, h35, h36, h37, h38, h39, hpos] simp only [expBody, seqL, run_seq] refine ⟨?, ?, ?, ?, ?, ?, ?, ?, ?, ?, ?⟩ all_goals simp (config := {decide := true}) [Ex.eval, IState.top, Ex.fdiv_eval, dvE, nu1E, nu2E, h30, h31, h32, h33, h34, h35, h36, h37, h38, h39, hpos, expTerm, sub_eq_add_neg, expApprox_succ] · ring · intro j hj' have : j ≠ 33 ∧ j ≠ 34 ∧ j ≠ 35 ∧ j ≠ 36 ∧ j ≠ 37 ∧ j ≠ 38 ∧ j ≠ 39 := by refine ⟨?, ?, ?, ?, ?, ?, ?⟩ <;> (rintro rfl; revert hj'; decide) simp [this, hj j hj'] theorem exp_pre (n : ℕ) (x y : ℤ) (s : IState HS) (L5 L6 L7 : List Item) (h5 : s.G 5 = .int n :: L5) (h6 : s.G 6 = .int x :: L6) (h7 : s.G 7 = .int y :: L7) : expPre.ok s ∧ (expPre.run s).G 30 = .int (x * 2 ^ (n + 9)) :: s.G 30 ∧ (expPre.run s).G 31 = .int (y * 2 ^ (n + 9)) :: s.G 31 ∧ (expPre.run s).G 32 = .int (2 ^ (2 * n + 9)) :: s.G 32 ∧ (expPre.run s).G 33 = .int 0 :: s.G 33 ∧ (expPre.run s).G 34 = .int (2 ^ (2 * n + 9)) :: s.G 34 ∧ (expPre.run s).G 35 = .int 0 :: s.G 35 ∧ (expPre.run s).G 36 = .int 0 :: s.G 36 ∧ (expPre.run s).G 37 = .int 0 :: s.G 37 ∧ (expPre.run s).G 38 = .int (2 ^ (2 * n + 9)) :: s.G 38 ∧ ∀ j : Fin HS, j.val < 30 ∨ 38 < j.val → (expPre.run s).G j = s.G j := by have e9 : ((n : ℤ) + 9).toNat = n + 9 := by omega have eN : ((n : ℤ) + n + 9).toNat = 2 * n + 9 := by omega refine ⟨?, ?, ?, ?, ?, ?, ?, ?, ?, ?, ?⟩ all_goals simp (config := {decide := true}) [expPre, seqL, run_seq, RS.ok, Ex.eval, Ex.ok, IState.top, IState.IsInt, Ex.Clean, Ex.regs, zX_all, eXE, eYE, ePE, h5, h6, h7, e9, eN] · omega · intro j hj have : j ≠ 30 ∧ j ≠ 31 ∧ j ≠ 32 ∧ j ≠ 33 ∧ j ≠ 34 ∧ j ≠ 35 ∧ j ≠ 36 ∧ j ≠ 37 ∧ j ≠ 38 := by refine ⟨?, ?, ?, ?, ?, ?, ?, ?, ?⟩ <;> (rintro rfl; revert hj; decide) simp [this] theorem exp_K (n : ℕ) (x y : ℤ) (s : IState HS) (L5 L6 L7 : List Item) (h5 : s.G 5 = .int n :: L5) (h6 : s.G 6 = .int x :: L6) (h7 : s.G 7 = .int y :: L7) : eKE.eval (expPre.run s) = ((2 * n + 13 : ℕ) : ℤ) := by obtain ⟨-, -, -, -, -, -, -, -, -, -, gj⟩ := exp_pre n x y s L5 L6 L7 h5 h6 h7 simp (config := {decide := true}) [eKE, Ex.eval, IState.top, gj 5 (by decide), h5] ring theorem exp_inv_all (n : ℕ) (x y : ℤ) (s : IState HS) (L5 L6 L7 : List Item) (h5 : s.G 5 = .int n :: L5) (h6 : s.G 6 = .int x :: L6) (h7 : s.G 7 = .int y :: L7) : ∀ k ≤ 2 * n + 13, expInv (2 * n + 9) (2 * n + 13) (x * 2 ^ (n + 9)) (y * 2 ^ (n + 9)) s k (repSt 39 eKE expBody (expPre.run s) k) := by obtain ⟨-, g30, g31, g32, g33, g34, g35, g36, g37, g38, gj⟩ := exp_pre n x y s L5 L6 L7 h5 h6 h7 have hK := exp_K n x y s L5 L6 L7 h5 h6 h7 have hinv := repSt_inv 39 eKE expBody (expPre.run s) (expInv (2 * n + 9) (2 * n + 13) (x * 2 ^ (n + 9)) (y * 2 ^ (n + 9)) s) (by refine ⟨?, ?, ?, ?, ?, ?, ?, ?, ?, ?, ?⟩ <;> simp (config := {decide := true}) [g30, g31, g32, g33, g34, g35, g36, g37, g38, gj 39 (by decide), hK, expTerm, expApprox] intro j hj have : j ≠ 39 := by rintro rfl; revert hj; decide simp [this, gj j (by omega)]) (fun k _ hI => (exp_body _ _ _ _ s _ k hI).2) rw [hK, Int.toNat_natCast] at hinv exact hinv theorem exp_loop (n : ℕ) (x y : ℤ) (s : IState HS) (L5 L6 L7 : List Item) (h5 : s.G 5 = .int n :: L5) (h6 : s.G 6 = .int x :: L6) (h7 : s.G 7 = .int y :: L7) : (rep 39 eKE expBody).ok (expPre.run s) ∧ (rep 39 eKE expBody).run (expPre.run s) = (repSt 39 eKE expBody (expPre.run s) (2 * n + 13)).upd 39 (s.G 39) := by obtain ⟨-, -, -, -, -, -, -, -, -, -, gj⟩ := exp_pre n x y s L5 L6 L7 h5 h6 h7 have hK := exp_K n x y s L5 L6 L7 h5 h6 h7 have hinv := exp_inv_all n x y s L5 L6 L7 h5 h6 h7 have hw : (39 : Fin HS) ∉ expBody.writes := by simp [expBody, seqL, RS.writes] refine ⟨⟨by decide, ?, ?, ?, hw, ?⟩, ?⟩ · simp (config := {decide := true}) [eKE, Ex.Clean, Ex.regs, zX_all] · simp (config := {decide := true}) [eKE, Ex.ok, IState.IsInt, IState.top, gj 5 (by decide), h5] · rw [hK]; positivity · intro k hk rw [hK, Int.toNat_natCast] at hk exact (exp_body _ _ _ _ s _ k (hinv k hk.le)).1 · rw [run_rep 39 _ _ _ hw (by rw [hK]; positivity), hK, Int.toNat_natCast, gj 39 (by decide)] theorem expP_spec (n : ℕ) (x y : ℤ) (s : IState HS) (L5 L6 L7 : List Item) (h5 : s.G 5 = .int n :: L5) (h6 : s.G 6 = .int x :: L6) (h7 : s.G 7 = .int y :: L7) : expP.ok s ∧ expP.run s = (s.upd 8 (.int (expBits n x y).1 :: s.G 8)).upd 9 (.int (expBits n x y).2 :: s.G 9) := by obtain ⟨hpre, -⟩ := exp_pre n x y s L5 L6 L7 h5 h6 h7 obtain ⟨hlok, hrun⟩ := exp_loop n x y s L5 L6 L7 h5 h6 h7 obtain ⟨f30, f31, f32, f33, f34, f35, f36, f37, f38, -, fj⟩ := exp_inv_all n x y s L5 L6 L7 h5 h6 h7 (2 * n + 13) le_rfl have e8 : ((n : ℤ) + 8).toNat = n + 8 := by omega have e9 : ((n : ℤ) + 9).toNat = n + 9 := by omega have f5 := fj 5 (by decide) rw [h5] at f5 refine ⟨⟨hpre, hlok, ?⟩, ?⟩ · rw [hrun] simp (config := {decide := true}) only [expPost, seqL, RS.ok, run_seq, RS.run_push_G, RS.run_pop_G, IState.upd_G, IState.IsInt, IState.top, if_true, if_false, List.tail_cons, f30, f31, f32, f33, f34, f35, f36, f37, f38, rndE, Ex.Clean, Ex.fdiv_regs, Ex.regs, zX_all] refine ⟨⟨trivial, trivial, ?⟩, ⟨trivial, trivial, ?⟩, by simp⟩ all_goals (apply Ex.fdiv_ok) <;> simp (config := {decide := true}) [Ex.ok, Ex.eval, IState.IsInt, IState.top, IState.upd_G, f5, f36, f37, RS.run_push_G] <;> omega · show expPost.run ((rep 39 eKE expBody).run (expPre.run s)) = _ rw [hrun] refine run_ext ?_ ?_ ?_ rotate_left · simp only [IState.upd_ip] exact (repSt_ip_out _ _ _ _ ).1.trans (run_ip_out _ s).1 · simp only [IState.upd_out] exact (repSt_ip_out _ _ _ _ ).2.trans (run_ip_out _ s).2 intro j by_cases hj8 : j = 8 · subst hj8 simp (config := {decide := true}) [expPost, seqL, run_seq, rndE, Ex.eval, IState.top, IState.upd_G, f36, f5, fj 8 (by decide), e8, e9, expBits] by_cases hj9 : j = 9 · subst hj9 simp (config := {decide := true}) [expPost, seqL, run_seq, rndE, Ex.eval, IState.top, IState.upd_G, f37, f5, fj 9 (by decide), e8, e9, expBits] by_cases hlo : j.val < 30 ∨ 39 < j.val · have : j ≠ 30 ∧ j ≠ 31 ∧ j ≠ 32 ∧ j ≠ 33 ∧ j ≠ 34 ∧ j ≠ 35 ∧ j ≠ 36 ∧ j ≠ 37 ∧ j ≠ 38 ∧ j ≠ 39 := by refine ⟨?, ?, ?, ?, ?, ?, ?, ?, ?, ?⟩ <;> (rintro rfl; revert hlo; decide) simp [expPost, seqL, run_seq, IState.upd_G, hj8, hj9, this, fj j hlo] · have : j = 30 ∨ j = 31 ∨ j = 32 ∨ j = 33 ∨ j = 34 ∨ j = 35 ∨ j = 36 ∨ j = 37 ∨ j = 38 ∨ j = 39 := by revert hlo; revert j; decide rcases this with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> simp (config := {decide := true}) [expPost, seqL, run_seq, IState.upd_G, f30, f31, f32, f33, f34, f35, f36, f37, f38] /-! ## Cost

The following holds (Lean statement, in the scope of module NLogN.HNumExp):

theorem NLogN.exp_body_cost (N K : ℕ) (X Y : ℤ) (s0 t : IState HS) (k : ℕ)
    (h : expInv N K X Y s0 k t) (hk : k < K) (M : ℤ) (B : ℕ)
    (hM : ((K : ℤ) + 1) * (2 ^ N * (|X| + |Y| + 1) ^ K) ≤ M)
    (big : ∀ z : ℤ, |z| ≤ M → zsz z ≤ B) :
    expBody.cost t + asgCost 39 (decE 39) (expBody.run t) ≤ 1000 * 10 ^ 7 * (B + 4) ^ 2

Context. The lemma belongs to the part expBits as a register program: Inputs n on register 5, x on 6, y on 7; the two components of expBits n x y are pushed on registers 8 and 9. Scratch registers 30 … 39.

Formalization Note. This is a lemma of the Lean development NLogN, a multitape-Turing-machine implementation of the Harvey–van der Hoeven $O(n\log n)$ integer multiplication algorithm, used in the proof of NLogN.FIN.theorem_1_1_nlogn : IntMul.MulTimeBound fun n => n * Real.log n. All names refer to the definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8 (namespace NLogN), built on the platform model Def_IntMul_MultitapeModel and the published reference Def_IntMul_HvdH_MachineRef. The machine layer: IState HS is a state of 64 item stacks; RM programs have a semantics p.run s, a definedness predicate p.ok M s and a cost p.cost M s relative to a multiplication spec M : MulSpec; zsz z is the bit length of $|z|$.