Prove2Me

Round-six κ development, definitions part 11

Definition
IntMul_Kappa_R6_Defs11

by xuanji · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplicationkappa-improvement

Definition bundle IntMul_Kappa_R6_Defs11 of the round-six κ-improvement development. It collects the definitions (data types, parameter maps, network and program structures, and the few lemmas that these definitions need) of the Lean modules NLogN.HExprPf, NLogN.HExprPow, NLogN.HExprDiv, NLogN.HExprRun, NLogN.HExprCost, NLogN.HExprLin, NLogN.HReg, NLogN.HList, NLogN.HRM, NLogN.HLinCost, NLogN.HRen, Solutions.ButterflyGuard, Solutions.ButterflyPacked, Solutions.KIL6Den, extracted by skeleton subtraction from the source files with their namespaces, variable declarations and opens unchanged.

The theorems about these objects are published as separate platform nodes that import this bundle.

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).

Definition code
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_R6_Defs10
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_HvdH_M_Defs2
import Definitions.Def_IntMul_HvdH_M_Defs1
import Definitions.Def_IntMul_Kappa_R6_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs10
import Definitions.Def_IntMul_Kappa_K_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs1

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: NLogN.HExprPf
/-!
# Correctness of expression code
-/

namespace NLogN

open IntMul

variable {S P : ℕ} {I : List Sym} {iprog : Fin P → IStmt S P}

theorem IState.top_upd_ne (s : IState S) {i j : Fin S} (h : i ≠ j) (L : List Item) :
    (s.upd j L).top i = s.top i := by
  simp [IState.top, IState.upd_G, h]

theorem IState.isInt_upd_ne (s : IState S) {i j : Fin S} (h : i ≠ j) (L : List Item) :
    (s.upd j L).IsInt i ↔ s.IsInt i := by
  simp [IState.IsInt, IState.top_upd_ne s h, IState.upd_G, h]

theorem IState.isInt_of_r6c {s : IState S} {i : Fin S} {a : ℤ} {L : List Item}
    (h : s.G i = .int a :: L) : s.IsInt i := ⟨L, by rw [IState.top_eq_r6c h, h]⟩

namespace Ex

theorem eval_upd (s : IState S) (j : Fin S) (L : List Item) :
    ∀ e : Ex S, j ∉ e.regs → e.eval (s.upd j L) = e.eval s
  | reg i, h => by simp only [regs, List.mem_singleton] at h; exact IState.top_upd_ne s (Ne.symm h) L
  | lit _, _ => rfl
  | add a b, h | mul a b, h | shl a b, h | quo a b, h | rem a b, h | ndiv a b, h | nmod a b, h => by
    simp only [regs, List.mem_append, not_or] at h
    simp only [eval, eval_upd s j L a h.1, eval_upd s j L b h.2]
  | neg a, h | pow2 a, h => by
    simp only [regs] at h; simp only [eval, eval_upd s j L a h]
  | sel c x y, h => by
    simp only [regs, List.mem_append, not_or] at h
    simp only [eval, eval_upd s j L c h.1.1, eval_upd s j L x h.1.2, eval_upd s j L y h.2]

theorem ok_upd (s : IState S) (j : Fin S) (L : List Item) :
    ∀ e : Ex S, j ∉ e.regs → (e.ok (s.upd j L) ↔ e.ok s)
  | reg i, h => by
    simp only [regs, List.mem_singleton] at h; exact IState.isInt_upd_ne s (Ne.symm h) L
  | lit _, _ => Iff.rfl
  | add a b, h | mul a b, h => by
    simp only [regs, List.mem_append, not_or] at h
    simp only [ok, ok_upd s j L a h.1, ok_upd s j L b h.2]
  | shl a b, h | quo a b, h | rem a b, h => by
    simp only [regs, List.mem_append, not_or] at h
    simp only [ok, ok_upd s j L a h.1, ok_upd s j L b h.2, eval_upd s j L b h.2]
  | ndiv a b, h | nmod a b, h => by
    simp only [regs, List.mem_append, not_or] at h
    simp only [ok, ok_upd s j L a h.1, ok_upd s j L b h.2, eval_upd s j L a h.1,
      eval_upd s j L b h.2]
  | neg a, h => by simp only [regs] at h; simp only [ok, ok_upd s j L a h]
  | pow2 a, h => by simp only [regs] at h; simp only [ok, ok_upd s j L a h, eval_upd s j L a h]
  | sel c x y, h => by
    simp only [regs, List.mem_append, not_or] at h
    simp only [ok, ok_upd s j L c h.1.1, ok_upd s j L x h.1.2, ok_upd s j L y h.2,
      eval_upd s j L c h.1.1]

theorem cost_upd (s : IState S) (j : Fin S) (L : List Item) :
    ∀ e : Ex S, j ∉ e.regs → e.cost (s.upd j L) = e.cost s
  | reg i, h => by
    simp only [regs, List.mem_singleton] at h; simp only [cost, IState.top_upd_ne s (Ne.symm h) L]
  | lit _, _ => rfl
  | add a b, h | mul a b, h | shl a b, h | quo a b, h | rem a b, h | ndiv a b, h | nmod a b, h => by
    simp only [regs, List.mem_append, not_or] at h
    simp only [cost, cost_upd s j L a h.1, cost_upd s j L b h.2, eval_upd s j L a h.1,
      eval_upd s j L b h.2]
  | neg a, h => by simp only [regs] at h; simp only [cost, cost_upd s j L a h]
  | pow2 a, h => by
    simp only [regs] at h; simp only [cost, cost_upd s j L a h, eval_upd s j L a h]
  | sel c x y, h => by
    simp only [regs, List.mem_append, not_or] at h
    simp only [cost, cost_upd s j L c h.1.1, cost_upd s j L x h.1.2, cost_upd s j L y h.2,
      eval_upd s j L c h.1.1]

end Ex

end NLogN

end

section
-- Source module: NLogN.HExprPow
/-!
# `2^a` by doubling
-/

namespace NLogN

open IntMul

variable {S P : ℕ} {I : List Sym} {iprog : Fin P → IStmt S P}

theorem zsz_neg_one' : zsz (-1) = 1 := by rw [zsz_neg_r6c, zsz_one_r6c]
theorem zsz_two' : zsz (2 : ℤ) = 2 := by rw [show (2 : ℤ) = 2 ^ 1 by norm_num, zsz_two_pow_r6c]

theorem zsz_natCast_sub_le (a k : ℕ) (h : k ≤ a) : zsz ((a : ℤ) - k) ≤ zsz (a : ℤ) :=
  zsz_mono_r6c (by omega)

theorem pow2Code_runs (z : ExSt S) (hz : z.Good) (s : IState S) (a : ℕ) (L : List Item)
    (hV : s.G z.V = .int a :: L) :
    IRuns I iprog (pow2Code z) s (s.upd z.V (.int (2 ^ a) :: L)) (pow2Cost a) := by
  obtain ⟨hVA, hVB, hVC, hVD, hVE, hVF, hVG, hAB, hAC, hAD, hAE, hAF, hAG, hBC, hBD, hBE, hBF, hBG,
    hCD, hCE, hCF, hCG, hDE, hDF, hDG, hEF, hEG, hFG⟩ := hz
  have hVA' := Ne.symm hVA; have hVB' := Ne.symm hVB; have hVC' := Ne.symm hVC; have hVD' := Ne.symm hVD; have hVE' := Ne.symm hVE; have hVF' := Ne.symm hVF; have hVG' := Ne.symm hVG; have hAB' := Ne.symm hAB; have hAC' := Ne.symm hAC; have hAD' := Ne.symm hAD; have hAE' := Ne.symm hAE; have hAF' := Ne.symm hAF; have hAG' := Ne.symm hAG; have hBC' := Ne.symm hBC; have hBD' := Ne.symm hBD; have hBE' := Ne.symm hBE; have hBF' := Ne.symm hBF; have hBG' := Ne.symm hBG; have hCD' := Ne.symm hCD; have hCE' := Ne.symm hCE; have hCF' := Ne.symm hCF; have hCG' := Ne.symm hCG; have hDE' := Ne.symm hDE; have hDF' := Ne.symm hDF; have hDG' := Ne.symm hDG; have hEF' := Ne.symm hEF; have hEG' := Ne.symm hEG; have hFG' := Ne.symm hFG
  have h1 := IRuns.mv_r6c (I := I) (iprog := iprog) hVC hV
  set s1 := (s.upd z.V L).upd z.C (.int a :: s.G z.C)
  have h2 := IRuns.const_r6c (I := I) (iprog := iprog) (s := s1) z.V 1
  set s2 := s1.upd z.V (.int 1 :: s1.G z.V)
  have h3 := IRuns.const_r6c (I := I) (iprog := iprog) (s := s2) z.A 2
  set s3 := s2.upd z.A (.int 2 :: s2.G z.A)
  let ss : ℕ → IState S := fun k =>
    (s3.upd z.V (.int (2 ^ k) :: L)).upd z.C (.int ((a : ℤ) - k) :: s.G z.C)
  have hb : ∀ k < a, IRuns I iprog
      (.seq (.op (.shl z.V z.A)) (.seq (.op (.const z.B (-1))) (.op (.add z.B z.C z.C))))
      (ss k) (ss (k + 1)) (shlCost 1 + 3 + addIntCost (1 + zsz (a : ℤ))) := by
    intro k hk
    have g1 := IRuns.shl (I := I) (iprog := iprog) (s := ss k) (i := z.V) (j := z.A) (a := 2 ^ k)
      (m := 1) (Li := L) (Lj := s.G z.A) hVA (by simp [ss, s3, s2, s1, hVC, hVA, hAC, hAC'])
      (by simp [ss, s3, s2, s1, hAC, hVA', hAC'])
    set t1 := (ss k).upd z.V (.int (2 ^ k * 2 ^ 1) :: L)
    have g2 := IRuns.const_r6c (I := I) (iprog := iprog) (s := t1) z.B (-1)
    set t2 := t1.upd z.B (.int (-1) :: t1.G z.B)
    have g3 := IRuns.add (I := I) (iprog := iprog) (s := t2) (i := z.B) (j := z.C) (k := z.C)
      (a := -1) (b := (a : ℤ) - k) (Li := s.G z.B) (Lj := s.G z.C) hBC
      (by simp [t2, t1, ss, s3, s2, s1, hBC, hVB', hAB', hBC', hVB, hAB])
      (by simp [t2, t1, ss, s3, s2, s1, hBC', hVC', hBC, hVC])
    refine (g1.seq_r6c (g2.seq_r6c g3)).mono' ?_ ?_
    · simp only [t2, t1, ss, s3, s2, s1]; ((apply IState.ext' <;> intros <;> simp only [IState.upd_G, IState.upd_ip, IState.upd_out] <;> split_ifs <;> simp_all)) <;> ring
    · have := addIntCost_mono (show 1 + zsz ((a : ℤ) - k) ≤ 1 + zsz (a : ℤ) by
        have := zsz_natCast_sub_le a k hk.le; omega)
      simp only [zsz_neg_one']; omega
  have hloop := IRuns.loop' (I := I) (iprog := iprog) (i := z.C) (f := fun c => c != .zero)
    (p := .seq (.op (.shl z.V z.A)) (.seq (.op (.const z.B (-1))) (.op (.add z.B z.C z.C))))
    ss _ a (fun k hk => by
      rw [cl_int (ss k) z.C ((a : ℤ) - k) (s.G z.C) (by simp [ss])]
      have : (a : ℤ) - k ≠ 0 := by omega
      simp [this]; split_ifs <;> simp)
    (by rw [cl_int (ss a) z.C ((a : ℤ) - a) (s.G z.C) (by simp [ss])]; simp) hb
  have e0 : s3 = ss 0 := by simp only [ss, s3, s2, s1]; ((apply IState.ext' <;> intros <;> simp only [IState.upd_G, IState.upd_ip, IState.upd_out] <;> split_ifs <;> simp_all))
  have h4 := IRuns.drop_r6c (I := I) (iprog := iprog) (s := ss a) (i := z.A) (a := 2)
    (L := s.G z.A) (by simp [ss, s3, s2, s1, hAC, hVA', hAC'])
  have h5 := IRuns.drop_r6c (I := I) (iprog := iprog) (s := (ss a).upd z.A (s.G z.A)) (i := z.C)
    (a := (a : ℤ) - a) (L := s.G z.C) (by simp [ss, hAC'])
  rw [e0] at h3
  refine (h1.seq_r6c (h2.seq_r6c (h3.seq_r6c (hloop.seq_r6c (h4.seq_r6c h5))))).mono' ?_ ?_
  · simp only [ss, s3, s2, s1]; ((apply IState.ext' <;> intros <;> simp only [IState.upd_G, IState.upd_ip, IState.upd_out] <;> split_ifs <;> simp_all))
  · simp only [pow2Cost, zsz_two', sub_self, zsz_zero_r6c, zsz_one_r6c]
    have hm : 2 * moveCost (zsz (a : ℤ)) + 19 ≤ addIntCost (zsz (a : ℤ) + 1) := by
      simp only [moveCost, addIntCost, addMagCost, subMagCost, zipCost]; nlinarith
    have hs : shlCost 1 = 223 := by simp [shlCost, moveCost, zipCost]
    rw [hs, show 1 + zsz (a : ℤ) = zsz (a : ℤ) + 1 by omega]
    generalize addIntCost (zsz (a : ℤ) + 1) = X at hm ⊢
    generalize 2 * moveCost (zsz (a : ℤ)) = Y at hm ⊢
    nlinarith

end NLogN

end

section
-- Source module: NLogN.HExprDiv
/-!
# Long division
-/

set_option linter.unusedSimpArgs false

namespace NLogN

open IntMul

variable {S P : ℕ} {I : List Sym} {iprog : Fin P → IStmt S P}

theorem zX_good : zX.Good := by constructor <;> decide

variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P}

@[simp] theorem rulerExp_two : rulerExp 2 = some 1 := by
  have := rulerExp_two_pow 1; simpa using this

theorem zsz_le_two_mul (a : ℤ) : zsz a ≤ zsz (2 * a) := zsz_mono_r6c (by rw [Int.natAbs_mul]; simp; omega)

theorem zsz_add_le' (a b : ℤ) : zsz (a + b) ≤ zsz a + zsz b + 1 := by
  have := zsz_add_le a b; omega

theorem ldUp_runs (s : IState HS) (L : List Item) (a b c d f : ℤ) :
    IRuns I iprog (ldUp zX) (ldSt s L a b c d (some f)) (ldSt s L (a * 2) b c (d + 1) (some (b - a * 2)))
      (2 * zsz f + 2 + shlCost 1 + 3 + addIntCost (1 + zsz d) +
        (dupCost (zsz b) + 17 + (dupCost (zsz (a * 2)) + 17) + 20 + addIntCost (zsz (a * 2) + zsz b))) := by
  apply IRuns.of_runsTo_r6c 0
  simp +decide [IStmt.run, IOp.run, ldUp, ldFlag, ldSt]
  refine ⟨?_, by rw [zsz_neg_r6c]; simp only [zsz_one_r6c]; omega⟩
  rw [show -(a * 2) + b = b - a * 2 by ring, show 1 + d = d + 1 by ring]; ((apply IState.ext' <;> intros <;> simp +decide only [IState.upd_G, IState.upd_ip, IState.upd_out] <;> split_ifs <;> simp_all +decide))

theorem ldDown_lt (s : IState HS) (L : List Item) (a r q d : ℤ) (h0 : 0 < a) (h : r < a) :
    IRuns I iprog (ldDown zX) (ldSt s L (2 * a) r q d none) (ldSt s L a r (q * 2) (d - 1) none)
      (10000 * (zsz (2 * a) + zsz r + zsz q + zsz d + 10)) := by
  apply IRuns.of_runsTo_r6c 0
  have h1 : ¬ 2 * a < 0 := by omega
  have h2 : |a| = a := abs_of_pos h0
  have h3 : (2 * a).natAbs / 2 = a.natAbs := by omega
  have h4 : (2 * a).natAbs % 2 = 0 := by omega
  simp +decide [IStmt.run, IOp.run, ldDown, ldFlag, ldSt, h, sg, h1, h2, h3, h4]
  refine ⟨by rw [show -1 + d = d - 1 by ring]; ((apply IState.ext' <;> intros <;> simp +decide only [IState.upd_G, IState.upd_ip, IState.upd_out] <;> split_ifs <;> simp_all +decide)), ?_⟩
  have := zsz_le_two_mul a
  have := zsz_add_le' (-a) r
  ((simp only [addIntCost, addMagCost, subMagCost, dupCost, moveCost, zipCost, shlCost, splitCost, takeCost, zsz_neg_r6c, zsz_one_r6c, zsz_zero_r6c, zsz_neg_one', zsz_two'] at *)); omega

theorem ldDown_ge (s : IState HS) (L : List Item) (a r q d : ℤ) (h0 : 0 < a) (h : a ≤ r) :
    IRuns I iprog (ldDown zX) (ldSt s L (2 * a) r q d none)
      (ldSt s L a (r - a) (q * 2 + 1) (d - 1) none)
      (10000 * (zsz (2 * a) + zsz r + zsz q + zsz d + 10)) := by
  apply IRuns.of_runsTo_r6c 0
  have h1 : ¬ 2 * a < 0 := by omega
  have h2 : |a| = a := abs_of_pos h0
  have h3 : (2 * a).natAbs / 2 = a.natAbs := by omega
  have h4 : (2 * a).natAbs % 2 = 0 := by omega
  have h5 : ¬ -a + r < 0 := by omega
  simp +decide [IStmt.run, IOp.run, ldDown, ldFlag, ldSt, h5, sg, h1, h2, h3, h4]
  refine ⟨by rw [show -1 + d = d - 1 by ring, show 1 + q * 2 = q * 2 + 1 by ring,
    show -a + r = r - a by ring]; ((apply IState.ext' <;> intros <;> simp +decide only [IState.upd_G, IState.upd_ip, IState.upd_out] <;> split_ifs <;> simp_all +decide)), ?_⟩
  have := zsz_le_two_mul a
  have := zsz_add_le' (-a) r
  have := zsz_mul_le q 2
  have : zsz (2 : ℤ) = 2 := zsz_two'
  ((simp only [addIntCost, addMagCost, subMagCost, dupCost, moveCost, zipCost, shlCost, splitCost, takeCost, zsz_neg_r6c, zsz_one_r6c, zsz_zero_r6c, zsz_neg_one', zsz_two'] at *)); omega

theorem ldiv_arith (a D : ℕ) (hD : 0 < D) :
    (a % (2 * D) < D → a / D = a / (2 * D) * 2 ∧ a % D = a % (2 * D)) ∧
    (D ≤ a % (2 * D) → a / D = a / (2 * D) * 2 + 1 ∧ a % D = a % (2 * D) - D) := by
  have e := Nat.div_add_mod a (2 * D)
  have hr := Nat.mod_lt a (show 0 < 2 * D by omega)
  constructor
  · intro h
    exact (Nat.div_mod_unique hD).2 ⟨by linarith, h⟩
  · intro h
    refine (Nat.div_mod_unique hD).2 ⟨?_, by omega⟩
    have : a % (2 * D) - D + D = a % (2 * D) := Nat.sub_add_cancel h
    zify [h] at *
    linarith

theorem zsz_natCast_mul_two_pow (b k : ℕ) : zsz (((b * 2 ^ k : ℕ)) : ℤ) ≤ zsz (b : ℤ) + k + 1 := by
  have := zsz_mul_le (b : ℤ) (2 ^ k)
  rw [zsz_two_pow_r6c] at this
  push_cast; omega

theorem zsz_natCast_le' {x y : ℕ} (h : x ≤ y) : zsz (x : ℤ) ≤ zsz (y : ℤ) := zsz_mono_r6c (by simpa)

theorem lt_two_pow_zsz (a : ℕ) : a < 2 ^ zsz (a : ℤ) := by
  have := (zsz_le_iff (z := (a : ℤ)) (m := zsz (a : ℤ))).1 le_rfl; simpa using this

theorem zsz_natCast_le_self' (k : ℕ) : zsz (k : ℤ) ≤ k :=
  zsz_le_of_lt (by simpa using Nat.lt_two_pow_self)

theorem ldivCode_runs (s : IState HS) (a b : ℕ) (hb : 0 < b) (L : List Item)
    (hV : s.G 56 = .int b :: .int a :: L) :
    IRuns I iprog (ldivCode zX) s
      ((s.upd 56 (.int ((a / b : ℕ) : ℤ) :: L)).upd 63 (.int ((a % b : ℕ) : ℤ) :: s.G 63))
      (ldivCost (zsz (a : ℤ) + zsz (b : ℤ))) := by
  set n := zsz (a : ℤ) + zsz (b : ℤ) with hn
  have hex : ∃ k, a < b * 2 ^ k := ⟨a, lt_of_lt_of_le Nat.lt_two_pow_self
    (Nat.le_mul_of_pos_left _ hb)⟩
  obtain ⟨k0, hk0, hlt, hk0n⟩ : ∃ k0, a < b * 2 ^ k0 ∧ (∀ k < k0, b * 2 ^ k ≤ a) ∧
      k0 ≤ zsz (a : ℤ) :=
    ⟨Nat.find hex, Nat.find_spec hex, fun k hk => by have := Nat.find_min hex hk; omega,
      Nat.find_min' hex (lt_of_lt_of_le (lt_two_pow_zsz a) (Nat.le_mul_of_pos_left _ hb))⟩
  -- prologue
  have h0 : IRuns I iprog
      (.seq (.op (.mv zX.V zX.A)) (.seq (.op (.mv zX.V zX.B)) (.seq (.op (.const zX.C 0))
        (.seq (.op (.const zX.D 0)) (.seq (.op (.const zX.E 2)) (ldFlag zX))))))
      s (ldSt s L ((b * 2 ^ 0 : ℕ) : ℤ) a 0 ((0 : ℕ) : ℤ) (some ((a : ℤ) - ((b * 2 ^ 0 : ℕ) : ℤ))))
      (20 * moveCost n + 1000 + dupCost (zsz (a : ℤ)) + dupCost (zsz (b : ℤ)) +
        addIntCost (zsz (b : ℤ) + zsz (a : ℤ))) := by
    apply IRuns.of_runsTo_r6c 0
    simp +decide [IStmt.run, IOp.run, ldFlag, ldSt, hV]
    refine ⟨by rw [show -(b : ℤ) + a = a - b by ring]; ((apply IState.ext' <;> intros <;> simp +decide only [IState.upd_G, IState.upd_ip, IState.upd_out] <;> split_ifs <;> simp_all +decide)), ?_⟩
    ((simp only [addIntCost, addMagCost, subMagCost, dupCost, moveCost, zipCost, shlCost, splitCost, takeCost, zsz_neg_r6c, zsz_one_r6c, zsz_zero_r6c, zsz_neg_one', zsz_two'] at *)); omega
  -- phase 1
  have hbk : ∀ k ≤ k0, zsz (((b * 2 ^ k : ℕ)) : ℤ) ≤ n + 1 := by
    intro k hk; have := zsz_natCast_mul_two_pow b k; omega
  let ss : ℕ → IState HS := fun k =>
    ldSt s L ((b * 2 ^ k : ℕ) : ℤ) a 0 ((k : ℕ) : ℤ) (some ((a : ℤ) - ((b * 2 ^ k : ℕ) : ℤ)))
  have c1 : ∀ k < k0, IRuns I iprog (ldUp zX) (ss k) (ss (k + 1)) (10000 * (n + 10)) := by
    intro k hk
    have g := ldUp_runs (I := I) (iprog := iprog) s L ((b * 2 ^ k : ℕ) : ℤ) a 0 (k : ℤ)
      ((a : ℤ) - ((b * 2 ^ k : ℕ) : ℤ))
    have e2 : ((b * 2 ^ k : ℕ) : ℤ) * 2 = ((b * 2 ^ (k + 1) : ℕ) : ℤ) := by push_cast; ring
    refine g.mono' (by simp only [ss, e2]; push_cast; ring_nf) ?_
    have := hbk (k + 1) (by omega)
    have := hbk k (by omega)
    have := hlt k hk
    have hf : zsz ((a : ℤ) - ((b * 2 ^ k : ℕ) : ℤ)) ≤ zsz (a : ℤ) := zsz_mono_r6c (by omega)
    have hd : zsz ((k : ℕ) : ℤ) ≤ n := by have := zsz_natCast_le_self' k; omega
    rw [e2]
    ((simp only [addIntCost, addMagCost, subMagCost, dupCost, moveCost, zipCost, shlCost, splitCost, takeCost, zsz_neg_r6c, zsz_one_r6c, zsz_zero_r6c, zsz_neg_one', zsz_two'] at *)); omega
  have hL1 := IRuns.loop' (I := I) (iprog := iprog) (i := zX.F) (f := fun c => c != .neg)
    (p := ldUp zX) ss _ k0 (fun k hk => by
      have h1 : ((b * 2 ^ k : ℕ) : ℤ) ≤ a := by exact_mod_cast hlt k hk
      rw [cl_int (ss k) zX.F ((a : ℤ) - ((b * 2 ^ k : ℕ) : ℤ)) (s.G 62) (by simp [ss, ldSt])]
      have : ¬ ((a : ℤ) - ((b * 2 ^ k : ℕ) : ℤ) < 0) := by omega
      simp only [this, if_false]; split_ifs <;> simp)
    (by
      have h1 : (a : ℤ) < ((b * 2 ^ k0 : ℕ) : ℤ) := by exact_mod_cast hk0
      rw [cl_int (ss k0) zX.F ((a : ℤ) - ((b * 2 ^ k0 : ℕ) : ℤ)) (s.G 62) (by simp [ss, ldSt])]
      have : ((a : ℤ) - ((b * 2 ^ k0 : ℕ) : ℤ) < 0) := by omega
      have : ((a : ℤ) - ((b * 2 ^ k0 : ℕ) : ℤ) ≠ 0) := by omega
      rw [if_neg (by assumption), if_pos (by assumption)]; rfl) c1
  -- drop the flag
  have hdr := IRuns.drop_r6c (I := I) (iprog := iprog) (s := ss k0) (i := zX.F)
    (a := (a : ℤ) - ((b * 2 ^ k0 : ℕ) : ℤ)) (L := s.G 62) (by simp [ss, ldSt])
  -- phase 2
  let tt : ℕ → IState HS := fun j =>
    ldSt s L ((b * 2 ^ (k0 - j) : ℕ) : ℤ) ((a % (b * 2 ^ (k0 - j)) : ℕ) : ℤ)
      ((a / (b * 2 ^ (k0 - j)) : ℕ) : ℤ) ((k0 - j : ℕ) : ℤ) none
  have et : (ss k0).upd zX.F (s.G 62) = tt 0 := by
    simp only [ss, tt, Nat.sub_zero, Nat.mod_eq_of_lt hk0, Nat.div_eq_of_lt hk0]
    simp [ldSt]
  have c2 : ∀ j < k0, IRuns I iprog (ldDown zX) (tt j) (tt (j + 1)) (10000 * (4 * n + 20)) := by
    intro j hj
    set D := b * 2 ^ (k0 - (j + 1)) with hD
    have hD0 : 0 < D := by positivity
    have e2 : b * 2 ^ (k0 - j) = 2 * D := by
      rw [hD, show k0 - j = k0 - (j + 1) + 1 by omega, pow_succ]; ring
    have hq : zsz ((a / (2 * D) : ℕ) : ℤ) ≤ n := by
      have := zsz_natCast_le' (Nat.div_le_self a (2 * D)); omega
    have h2D : zsz ((2 * D : ℕ) : ℤ) ≤ n + 1 := by rw [← e2]; exact hbk _ (by omega)
    have hr : zsz ((a % (2 * D) : ℕ) : ℤ) ≤ n + 1 := by
      have := zsz_natCast_le' (Nat.mod_lt a (show 0 < 2 * D by omega)).le; omega
    have hdk : zsz (((k0 - j : ℕ)) : ℤ) ≤ n := by have := zsz_natCast_le_self' (k0 - j); omega
    have ar := ldiv_arith a D hD0
    have htj : tt j = ldSt s L (2 * (D : ℤ)) ((a % (2 * D) : ℕ) : ℤ) ((a / (2 * D) : ℕ) : ℤ)
        ((k0 - j : ℕ) : ℤ) none := by simp only [tt, e2]; push_cast; rfl
    rw [htj]
    by_cases hc : a % (2 * D) < D
    · have g := ldDown_lt (I := I) (iprog := iprog) s L (D : ℤ) ((a % (2 * D) : ℕ) : ℤ)
        ((a / (2 * D) : ℕ) : ℤ) ((k0 - j : ℕ) : ℤ) (by positivity) (by exact_mod_cast hc)
      refine g.mono' ?_ ?_
      · simp only [tt, ← hD, (ar.1 hc).1, (ar.1 hc).2]; push_cast
        rw [show ((k0 - j : ℕ) : ℤ) - 1 = ((k0 - (j + 1) : ℕ) : ℤ) by omega]
      · push_cast at h2D; omega
    · have g := ldDown_ge (I := I) (iprog := iprog) s L (D : ℤ) ((a % (2 * D) : ℕ) : ℤ)
        ((a / (2 * D) : ℕ) : ℤ) ((k0 - j : ℕ) : ℤ) (by positivity) (by exact_mod_cast (show D ≤ a % (2 * D) by omega))
      refine g.mono' ?_ ?_
      · simp only [tt, ← hD, (ar.2 (by omega)).1, (ar.2 (by omega)).2]
        rw [show ((k0 - j : ℕ) : ℤ) - 1 = ((k0 - (j + 1) : ℕ) : ℤ) by omega]
        push_cast [Nat.cast_sub (show D ≤ a % (2 * D) by omega)]; rfl
      · push_cast at h2D; omega
  have hL2 := IRuns.loop' (I := I) (iprog := iprog) (i := zX.D) (f := fun c => c != .zero)
    (p := ldDown zX) tt _ k0 (fun j hj => by
      rw [cl_int (tt j) zX.D ((k0 - j : ℕ) : ℤ) (s.G 60) (by simp [tt, ldSt])]
      have : ((k0 - j : ℕ) : ℤ) ≠ 0 := by omega
      rw [if_neg this]; split_ifs <;> rfl)
    (by rw [cl_int (tt k0) zX.D ((k0 - k0 : ℕ) : ℤ) (s.G 60) (by simp [tt, ldSt])]; simp) c2
  -- epilogue
  have h3 : IRuns I iprog (.seq (.op (.drop zX.E)) (.seq (.op (.drop zX.D)) (.seq (.op (.drop zX.A))
      (.seq (.op (.mv zX.C zX.V)) (.op (.mv zX.B zX.G)))))) (tt k0)
      ((s.upd 56 (.int ((a / b : ℕ) : ℤ) :: L)).upd 63 (.int ((a % b : ℕ) : ℤ) :: s.G 63))
      (100 * moveCost (n + 1) + 1000) := by
    apply IRuns.of_runsTo_r6c 0
    simp +decide [IStmt.run, IOp.run, tt, ldSt]
    refine ⟨by ((apply IState.ext' <;> intros <;> simp +decide only [IState.upd_G, IState.upd_ip, IState.upd_out] <;> split_ifs <;> simp_all +decide)), ?_⟩
    have h1 := zsz_natCast_le' (Nat.div_le_self a b)
    have h2 := zsz_natCast_le' (Nat.mod_le a b)
    push_cast at h1 h2
    ((simp only [addIntCost, addMagCost, subMagCost, dupCost, moveCost, zipCost, shlCost, splitCost, takeCost, zsz_neg_r6c, zsz_one_r6c, zsz_zero_r6c, zsz_neg_one', zsz_two'] at *)); omega
  rw [et] at hdr
  refine (h0.seq_r6c (hL1.seq_r6c (hdr.seq_r6c (hL2.seq_r6c h3)))).mono_r6c ?_
  have hf : zsz ((a : ℤ) - ((b * 2 ^ k0 : ℕ) : ℤ)) ≤ 2 * n + 2 := by
    have := zsz_add_le' (a : ℤ) (-((b * 2 ^ k0 : ℕ) : ℤ)); rw [zsz_neg_r6c] at this
    have := hbk k0 le_rfl; rw [sub_eq_add_neg]; omega
  simp only [ldivCost]
  have hk : k0 ≤ n := by omega
  ((simp only [addIntCost, addMagCost, subMagCost, dupCost, moveCost, zipCost, shlCost, splitCost, takeCost, zsz_neg_r6c, zsz_one_r6c, zsz_zero_r6c, zsz_neg_one', zsz_two'] at *))
  nlinarith

end NLogN

end

section
-- Source module: NLogN.HExprRun
/-!
# Expression code runs (on the HvdH stacks)
-/

set_option linter.unusedSimpArgs false

namespace NLogN

open IntMul

variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P}

theorem sg_tdiv (a : ℤ) (m : ℕ) : sg a (a.natAbs / 2 ^ m) = a.tdiv (2 ^ m) := by
  unfold sg
  split_ifs with h
  · obtain ⟨k, rfl⟩ : ∃ k : ℕ, a = -k := ⟨a.natAbs, by omega⟩
    rw [Int.neg_tdiv]
    simp only [Int.natAbs_neg, Int.natAbs_natCast, neg_inj]
    rw [show ((2 : ℤ) ^ m) = ((2 ^ m : ℕ) : ℤ) by push_cast; rfl, ← Int.ofNat_tdiv]
  · obtain ⟨k, rfl⟩ : ∃ k : ℕ, a = k := ⟨a.natAbs, by omega⟩
    simp only [Int.natAbs_natCast]
    rw [show ((2 : ℤ) ^ m) = ((2 ^ m : ℕ) : ℤ) by push_cast; rfl, ← Int.ofNat_tdiv]

theorem sg_tmod (a : ℤ) (m : ℕ) : sg a (a.natAbs % 2 ^ m) = a.tmod (2 ^ m) := by
  unfold sg
  split_ifs with h
  · obtain ⟨k, rfl⟩ : ∃ k : ℕ, a = -k := ⟨a.natAbs, by omega⟩
    rw [Int.neg_tmod]
    simp only [Int.natAbs_neg, Int.natAbs_natCast, neg_inj]
    rw [show ((2 : ℤ) ^ m) = ((2 ^ m : ℕ) : ℤ) by push_cast; rfl, ← Int.ofNat_tmod]
  · obtain ⟨k, rfl⟩ : ∃ k : ℕ, a = k := ⟨a.natAbs, by omega⟩
    simp only [Int.natAbs_natCast]
    rw [show ((2 : ℤ) ^ m) = ((2 ^ m : ℕ) : ℤ) by push_cast; rfl, ← Int.ofNat_tmod]

theorem zX_all : zX.all = [56, 57, 58, 59, 60, 61, 62, 63] := rfl

theorem zsz_sg_div_le (a : ℤ) (m : ℕ) : zsz (sg a (a.natAbs / 2 ^ m)) ≤ zsz a :=
  zsz_mono_r6c (by rw [natAbs_sg]; exact Nat.div_le_self _ _)

theorem zsz_sg_mod_le (a : ℤ) (m : ℕ) : zsz (sg a (a.natAbs % 2 ^ m)) ≤ zsz a :=
  zsz_mono_r6c (by rw [natAbs_sg]; exact Nat.mod_le _ _)

namespace Ex

theorem Clean.not56 {e : Ex HS} (h : e.Clean) : (56 : Fin HS) ∉ e.regs := fun hm =>
  h _ hm (by simp [zX_all])

theorem code_runs_r6c : ∀ (e : Ex HS) (s : IState HS), e.Clean → e.ok s →
    IRuns I iprog (e.code zX) s (s.upd 56 (.int (e.eval s) :: s.G 56)) (e.cost s)
  | reg i, s, hc, hok => by
    obtain ⟨L, hL⟩ := hok
    have hi : i ≠ 56 := fun h => hc i (by simp [regs]) (by simp [h, zX_all])
    exact (IRuns.dup_r6c (I := I) (iprog := iprog) hi hL).mono' (by simp [eval]) (by simp [cost])
  | lit c, s, _, _ => (IRuns.const_r6c (I := I) (iprog := iprog) (s := s) 56 c).mono' rfl le_rfl
  | add a b, s, hc, hok => by
    have hca : a.Clean := fun i hi => hc i (by simp [regs, hi])
    have hcb : b.Clean := fun i hi => hc i (by simp [regs, hi])
    have ha := code_runs_r6c a s hca hok.1
    set s1 := s.upd 56 (.int (a.eval s) :: s.G 56)
    have hb := code_runs_r6c b s1 hcb ((ok_upd s 56 _ b hcb.not56).2 hok.2)
    rw [eval_upd s 56 _ b hcb.not56, cost_upd s 56 _ b hcb.not56] at hb
    have hr : IRuns I iprog (.seq (.op (.mv zX.V zX.A)) (.seq (.op (.mv zX.V zX.B))
        (.op (.add zX.A zX.B zX.V)))) (s1.upd 56 (.int (b.eval s) :: s1.G 56))
        (s.upd 56 (.int (a.eval s + b.eval s) :: s.G 56))
        (2 * moveCost (zsz (b.eval s)) + 2 * moveCost (zsz (a.eval s)) + 38 +
          addIntCost (zsz (b.eval s) + zsz (a.eval s))) := by
      apply IRuns.of_runsTo_r6c 0
      simp +decide [IStmt.run, IOp.run, s1]
      refine ⟨by rw [add_comm]; ((apply IState.ext' <;> intros <;> simp +decide only [IState.upd_G, IState.upd_ip, IState.upd_out] <;> split_ifs <;> simp_all +decide)), by omega⟩
    exact (ha.seq_r6c (hb.seq_r6c hr)).mono' rfl (by simp only [cost]; omega)
  | neg a, s, hc, hok => by
    have hca : a.Clean := fun i hi => hc i (by simp [regs, hi])
    have ha := code_runs_r6c a s hca hok
    have hr := IRuns.neg (I := I) (iprog := iprog) (s := s.upd 56 (.int (a.eval s) :: s.G 56))
      (i := 56) (a := a.eval s) (L := s.G 56) (by simp)
    exact (ha.seq_r6c hr).mono' (by simp [eval]) (by simp only [cost]; omega)
  | mul a b, s, hc, hok => by
    have hca : a.Clean := fun i hi => hc i (by simp [regs, hi])
    have hcb : b.Clean := fun i hi => hc i (by simp [regs, hi])
    have ha := code_runs_r6c a s hca hok.1
    set s1 := s.upd 56 (.int (a.eval s) :: s.G 56)
    have hb := code_runs_r6c b s1 hcb ((ok_upd s 56 _ b hcb.not56).2 hok.2)
    rw [eval_upd s 56 _ b hcb.not56, cost_upd s 56 _ b hcb.not56] at hb
    have hr := smul_runs (I := I) (iprog := iprog) (A := zX.V) (X := zX.A) (Y := zX.B) (W := zX.C)
      (Q := zX.D) (R := zX.E) (T := zX.F) (by decide) (s1.upd 56 (.int (b.eval s) :: s1.G 56))
      (b.eval s) (a.eval s) (s.G 56) (by simp [s1])
    exact (ha.seq_r6c (hb.seq_r6c hr)).mono' (by simp [s1, eval, mul_comm]) (by simp only [cost]; omega)
  | shl a r, s, hc, hok => by
    have hca : a.Clean := fun i hi => hc i (by simp [regs, hi])
    have hcb : r.Clean := fun i hi => hc i (by simp [regs, hi])
    obtain ⟨hoa, hor, m, hm⟩ := hok
    have ha := code_runs_r6c a s hca hoa
    set s1 := s.upd 56 (.int (a.eval s) :: s.G 56)
    have hb := code_runs_r6c r s1 hcb ((ok_upd s 56 _ r hcb.not56).2 hor)
    rw [eval_upd s 56 _ r hcb.not56, cost_upd s 56 _ r hcb.not56, hm] at hb
    have hr : IRuns I iprog (.seq (.op (.mv zX.V zX.A)) (.seq (.op (.shl zX.V zX.A))
        (.op (.drop zX.A)))) (s1.upd 56 (.int (2 ^ m) :: s1.G 56))
        (s.upd 56 (.int (a.eval s * 2 ^ m) :: s.G 56))
        (2 * moveCost (zsz ((2 : ℤ) ^ m)) + 19 + shlCost m + (2 * zsz ((2 : ℤ) ^ m) + 2)) := by
      apply IRuns.of_runsTo_r6c 0
      simp +decide [IStmt.run, IOp.run, s1]
      refine ⟨by ((apply IState.ext' <;> intros <;> simp +decide only [IState.upd_G, IState.upd_ip, IState.upd_out] <;> split_ifs <;> simp_all +decide)), by omega⟩
    refine (ha.seq_r6c (hb.seq_r6c hr)).mono' (by simp [eval, hm]) ?_
    simp only [cost, hm, zsz_two_pow_r6c]
    have : shlCost m ≤ shlCost (m + 1) := by simp only [shlCost, moveCost, zipCost]; omega
    omega
  | quo a r, s, hc, hok => by
    have hca : a.Clean := fun i hi => hc i (by simp [regs, hi])
    have hcb : r.Clean := fun i hi => hc i (by simp [regs, hi])
    obtain ⟨hoa, hor, m, hm⟩ := hok
    have ha := code_runs_r6c a s hca hoa
    set s1 := s.upd 56 (.int (a.eval s) :: s.G 56)
    have hb := code_runs_r6c r s1 hcb ((ok_upd s 56 _ r hcb.not56).2 hor)
    rw [eval_upd s 56 _ r hcb.not56, cost_upd s 56 _ r hcb.not56, hm] at hb
    have hr : IRuns I iprog (.seq (.op (.mv zX.V zX.A)) (.seq (.op (.split zX.V zX.A zX.B))
        (.seq (.op (.drop zX.B)) (.op (.drop zX.A))))) (s1.upd 56 (.int (2 ^ m) :: s1.G 56))
        (s.upd 56 (.int (sg (a.eval s) ((a.eval s).natAbs / 2 ^ m)) :: s.G 56))
        (2 * moveCost (zsz ((2 : ℤ) ^ m)) + 19 + (splitCost m + 17) +
          (2 * zsz (sg (a.eval s) ((a.eval s).natAbs % 2 ^ m)) + 2) + (2 * zsz ((2 : ℤ) ^ m) + 2)) := by
      apply IRuns.of_runsTo_r6c 0
      simp +decide [IStmt.run, IOp.run, s1]
      refine ⟨by ((apply IState.ext' <;> intros <;> simp +decide only [IState.upd_G, IState.upd_ip, IState.upd_out] <;> split_ifs <;> simp_all +decide)), by omega⟩
    refine (ha.seq_r6c (hb.seq_r6c hr)).mono' (by simp [eval, hm, sg_tdiv]) ?_
    simp only [cost, hm, zsz_two_pow_r6c]
    have : splitCost m ≤ splitCost (m + 1) := by
      simp only [splitCost, moveCost, takeCost]; omega
    have := zsz_sg_mod_le (a.eval s) m
    omega
  | rem a r, s, hc, hok => by
    have hca : a.Clean := fun i hi => hc i (by simp [regs, hi])
    have hcb : r.Clean := fun i hi => hc i (by simp [regs, hi])
    obtain ⟨hoa, hor, m, hm⟩ := hok
    have ha := code_runs_r6c a s hca hoa
    set s1 := s.upd 56 (.int (a.eval s) :: s.G 56)
    have hb := code_runs_r6c r s1 hcb ((ok_upd s 56 _ r hcb.not56).2 hor)
    rw [eval_upd s 56 _ r hcb.not56, cost_upd s 56 _ r hcb.not56, hm] at hb
    have hr : IRuns I iprog (.seq (.op (.mv zX.V zX.A)) (.seq (.op (.split zX.V zX.A zX.B))
        (.seq (.op (.drop zX.V)) (.seq (.op (.mv zX.B zX.V)) (.op (.drop zX.A))))))
        (s1.upd 56 (.int (2 ^ m) :: s1.G 56))
        (s.upd 56 (.int (sg (a.eval s) ((a.eval s).natAbs % 2 ^ m)) :: s.G 56))
        (2 * moveCost (zsz ((2 : ℤ) ^ m)) + 19 + (splitCost m + 17) +
          (2 * zsz (sg (a.eval s) ((a.eval s).natAbs / 2 ^ m)) + 2) +
          (2 * moveCost (zsz (sg (a.eval s) ((a.eval s).natAbs % 2 ^ m))) + 19) +
          (2 * zsz ((2 : ℤ) ^ m) + 2)) := by
      apply IRuns.of_runsTo_r6c 0
      simp +decide [IStmt.run, IOp.run, s1]
      refine ⟨by ((apply IState.ext' <;> intros <;> simp +decide only [IState.upd_G, IState.upd_ip, IState.upd_out] <;> split_ifs <;> simp_all +decide)), by omega⟩
    refine (ha.seq_r6c (hb.seq_r6c hr)).mono' (by simp [eval, hm, sg_tmod]) ?_
    simp only [cost, hm, zsz_two_pow_r6c]
    have : splitCost m ≤ splitCost (m + 1) := by
      simp only [splitCost, moveCost, takeCost]; omega
    have h1 := zsz_sg_mod_le (a.eval s) m
    have h2 := zsz_sg_div_le (a.eval s) m
    have : moveCost (zsz (sg (a.eval s) ((a.eval s).natAbs % 2 ^ m))) ≤ moveCost (zsz (a.eval s)) := by
      simp only [moveCost]; nlinarith
    omega
  | pow2 a, s, hc, hok => by
    have hca : a.Clean := fun i hi => hc i (by simp [regs, hi])
    obtain ⟨hoa, h0⟩ := hok
    have ha := code_runs_r6c a s hca hoa
    obtain ⟨k, hk⟩ : ∃ k : ℕ, a.eval s = k := ⟨(a.eval s).toNat, by omega⟩
    rw [hk] at ha
    have hr := pow2Code_runs (I := I) (iprog := iprog) zX zX_good
      (s.upd 56 (.int k :: s.G 56)) k (s.G 56) (by simp)
    refine (ha.seq_r6c hr).mono' (by simp [eval, hk]) ?_
    simp only [cost, hk, Int.toNat_natCast]
    omega
  | sel c x y, s, hc, hok => by
    have hcc : c.Clean := fun i hi => hc i (by simp [regs, hi])
    have hcx : x.Clean := fun i hi => hc i (by simp [regs, hi])
    have hcy : y.Clean := fun i hi => hc i (by simp [regs, hi])
    obtain ⟨hoc, hoxy⟩ := hok
    have h1 := code_runs_r6c c s hcc hoc
    have h2 := IRuns.mv_r6c (I := I) (iprog := iprog) (s := s.upd 56 (.int (c.eval s) :: s.G 56))
      (i := zX.V) (j := zX.A) (a := c.eval s) (L := s.G 56) (by decide) (by simp)
    set s2 := ((s.upd 56 (.int (c.eval s) :: s.G 56)).upd zX.V (s.G 56)).upd zX.A
      (.int (c.eval s) :: (s.upd 56 (.int (c.eval s) :: s.G 56)).G zX.A)
    have hd := IRuns.drop_r6c (I := I) (iprog := iprog) (s := s2) (i := zX.A) (a := c.eval s)
      (L := s.G 57) (by simp [s2])
    have e3 : s2.upd zX.A (s.G 57) = s := by simp only [s2]; ((apply IState.ext' <;> intros <;> simp +decide only [IState.upd_G, IState.upd_ip, IState.upd_out] <;> split_ifs <;> simp_all +decide))
    rw [e3] at hd
    by_cases hneg : c.eval s < 0
    · have hx := code_runs_r6c x s hcx (by simpa [hneg] using hoxy)
      have hi := IRuns.iteT (I := I) (iprog := iprog) (i := zX.A) (f := fun k => k == .neg)
        (q := .seq (.op (.drop zX.A)) (y.code zX))
        (by rw [cl_int s2 zX.A (c.eval s) (s.G 57) (by simp [s2])]; simp [hneg]; omega)
        (hd.seq_r6c hx)
      refine (h1.seq_r6c (h2.seq_r6c hi)).mono' (by simp [eval, hneg]) ?_
      simp only [cost, if_pos hneg]; omega
    · have hy := code_runs_r6c y s hcy (by simpa [hneg] using hoxy)
      have hi := IRuns.iteF (I := I) (iprog := iprog) (i := zX.A) (f := fun k => k == .neg)
        (p := .seq (.op (.drop zX.A)) (x.code zX))
        (by rw [cl_int s2 zX.A (c.eval s) (s.G 57) (by simp [s2])]; simp [hneg]; split_ifs <;> simp)
        (hd.seq_r6c hy)
      refine (h1.seq_r6c (h2.seq_r6c hi)).mono' (by simp [eval, hneg]) ?_
      simp only [cost, if_neg hneg]; omega
  | ndiv a b, s, hc, hok => by
    have hca : a.Clean := fun i hi => hc i (by simp [regs, hi])
    have hcb : b.Clean := fun i hi => hc i (by simp [regs, hi])
    obtain ⟨hoa, hob, ha0, hb0⟩ := hok
    have ha := code_runs_r6c a s hca hoa
    set s1 := s.upd 56 (.int (a.eval s) :: s.G 56)
    have hb := code_runs_r6c b s1 hcb ((ok_upd s 56 _ b hcb.not56).2 hob)
    rw [eval_upd s 56 _ b hcb.not56, cost_upd s 56 _ b hcb.not56] at hb
    obtain ⟨u, hu⟩ : ∃ u : ℕ, a.eval s = u := ⟨(a.eval s).toNat, by omega⟩
    obtain ⟨v, hv⟩ : ∃ v : ℕ, b.eval s = v := ⟨(b.eval s).toNat, by omega⟩
    have hv0 : 0 < v := by omega
    rw [hv] at hb
    have hd := ldivCode_runs (I := I) (iprog := iprog) (s1.upd 56 (.int v :: s1.G 56)) u v hv0
      (s.G 56) (by simp [s1, hu])
    have ht : IRuns I iprog (.op (.drop zX.G))
        (((s1.upd 56 (.int v :: s1.G 56)).upd 56 (.int ((u / v : ℕ) : ℤ) :: s.G 56)).upd 63
          (.int ((u % v : ℕ) : ℤ) :: (s1.upd 56 (.int v :: s1.G 56)).G 63))
        (s.upd 56 (.int ((u / v : ℕ) : ℤ) :: s.G 56)) (2 * zsz ((u % v : ℕ) : ℤ) + 2) := by
      apply IRuns.of_runsTo_r6c 0
      simp +decide [IStmt.run, IOp.run, s1]
      try refine ⟨?_, ?_⟩
      all_goals first | ((apply IState.ext' <;> intros <;> simp +decide only [IState.upd_G, IState.upd_ip, IState.upd_out] <;> split_ifs <;> simp_all +decide)) | omega
    refine (ha.seq_r6c (hb.seq_r6c (hd.seq_r6c ht))).mono' (by simp [eval, hu, hv]) ?_
    simp only [cost, hu, hv]
    have : zsz ((u % v : ℕ) : ℤ) ≤ zsz (v : ℤ) :=
      zsz_mono_r6c (by simp; exact (Nat.mod_lt _ hv0).le)
    have : 2 * zsz (v : ℤ) + 2 ≤ ldivCost (zsz (u : ℤ) + zsz (v : ℤ)) := by
      have := Nat.le_self_pow (n := 2) (by norm_num) (zsz (u : ℤ) + zsz (v : ℤ) + 2)
      simp only [ldivCost]; omega
    omega
  | nmod a b, s, hc, hok => by
    have hca : a.Clean := fun i hi => hc i (by simp [regs, hi])
    have hcb : b.Clean := fun i hi => hc i (by simp [regs, hi])
    obtain ⟨hoa, hob, ha0, hb0⟩ := hok
    have ha := code_runs_r6c a s hca hoa
    set s1 := s.upd 56 (.int (a.eval s) :: s.G 56)
    have hb := code_runs_r6c b s1 hcb ((ok_upd s 56 _ b hcb.not56).2 hob)
    rw [eval_upd s 56 _ b hcb.not56, cost_upd s 56 _ b hcb.not56] at hb
    obtain ⟨u, hu⟩ : ∃ u : ℕ, a.eval s = u := ⟨(a.eval s).toNat, by omega⟩
    obtain ⟨v, hv⟩ : ∃ v : ℕ, b.eval s = v := ⟨(b.eval s).toNat, by omega⟩
    have hv0 : 0 < v := by omega
    rw [hv] at hb
    have hd := ldivCode_runs (I := I) (iprog := iprog) (s1.upd 56 (.int v :: s1.G 56)) u v hv0
      (s.G 56) (by simp [s1, hu])
    have ht : IRuns I iprog (.seq (.op (.drop zX.V)) (.op (.mv zX.G zX.V)))
        (((s1.upd 56 (.int v :: s1.G 56)).upd 56 (.int ((u / v : ℕ) : ℤ) :: s.G 56)).upd 63
          (.int ((u % v : ℕ) : ℤ) :: (s1.upd 56 (.int v :: s1.G 56)).G 63))
        (s.upd 56 (.int ((u % v : ℕ) : ℤ) :: s.G 56))
        (2 * zsz ((u / v : ℕ) : ℤ) + 2 + (2 * moveCost (zsz ((u % v : ℕ) : ℤ)) + 19)) := by
      apply IRuns.of_runsTo_r6c 0
      simp +decide [IStmt.run, IOp.run, s1]
      try refine ⟨?_, ?_⟩
      all_goals first | ((apply IState.ext' <;> intros <;> simp +decide only [IState.upd_G, IState.upd_ip, IState.upd_out] <;> split_ifs <;> simp_all +decide)) | omega
    refine (ha.seq_r6c (hb.seq_r6c (hd.seq_r6c ht))).mono' (by simp [eval, hu, hv]) ?_
    simp only [cost, hu, hv]
    have h1 : zsz ((u % v : ℕ) : ℤ) ≤ zsz (v : ℤ) :=
      zsz_mono_r6c (by simp; exact (Nat.mod_lt _ hv0).le)
    have h2 : zsz ((u / v : ℕ) : ℤ) ≤ zsz (u : ℤ) :=
      zsz_mono_r6c (by simp; exact Nat.div_le_self _ _)
    have : 2 * zsz (u : ℤ) + 2 + (2 * moveCost (zsz (v : ℤ)) + 19) ≤
        ldivCost (zsz (u : ℤ) + zsz (v : ℤ)) := by
      have := Nat.le_self_pow (n := 2) (by norm_num) (zsz (u : ℤ) + zsz (v : ℤ) + 2)
      simp only [ldivCost, moveCost]; omega
    have : moveCost (zsz ((u % v : ℕ) : ℤ)) ≤ moveCost (zsz (v : ℤ)) := by
      simp only [moveCost]; omega
    omega

end Ex

end NLogN

end

section
-- Source module: NLogN.HExprCost
/-!
# A uniform cost bound for expressions

If every value an expression computes (and every register it reads) has at most `B` bits, its
code costs at most `size · 10^7 · (B+2)^2`.
-/

namespace NLogN

open IntMul

variable {S : ℕ}

namespace Ex

theorem zsz_eval_le (s : IState S) (B : ℕ) : ∀ e : Ex S, e.Bnd s B → zsz (e.eval s) ≤ B
  | reg _, h | lit _, h => h
  | add _ _, h | mul _ _, h | shl _ _, h | ndiv _ _, h | nmod _ _, h => h.2.2
  | neg a, h => by simp only [eval, zsz_neg_r6c]; exact zsz_eval_le s B a h
  | quo a r, h => by
    simp only [eval]
    exact le_trans (zsz_mono_r6c (by rw [Int.natAbs_tdiv]; exact Nat.div_le_self _ _))
      (zsz_eval_le s B a h.1)
  | rem a r, h => by
    simp only [eval]
    exact le_trans (zsz_mono_r6c (by rw [Int.natAbs_tmod]; exact Nat.mod_le _ _))
      (zsz_eval_le s B a h.1)
  | pow2 a, h => by
    simp only [eval]; rw [zsz_two_pow_r6c]; have := h.2; omega
  | sel c x y, h => by
    simp only [eval]; split_ifs with hc
    · exact zsz_eval_le s B x (by simpa [hc] using h.2)
    · exact zsz_eval_le s B y (by simpa [hc] using h.2)

theorem cost_le_r6c (s : IState S) (B : ℕ) : ∀ e : Ex S, e.Bnd s B →
    e.cost s ≤ e.size * 10 ^ 7 * (B + 2) ^ 2
  | reg i, h => by
    simp only [cost, size, Bnd] at h ⊢; (simp only [dupCost, moveCost, zipCost, addIntCost, addMagCost, subMagCost, smulCost, shlCost, splitCost, takeCost, ldivCost, pow2Cost] at *); nlinarith
  | lit c, h => by
    simp only [cost, size, Bnd] at h ⊢; nlinarith
  | add a b, h => by
    have ha := cost_le_r6c s B a h.1; have hb := cost_le_r6c s B b h.2.1
    have za := zsz_eval_le s B a h.1; have zb := zsz_eval_le s B b h.2.1
    simp only [cost, size]; (simp only [dupCost, moveCost, zipCost, addIntCost, addMagCost, subMagCost, smulCost, shlCost, splitCost, takeCost, ldivCost, pow2Cost] at *); nlinarith
  | mul a b, h => by
    have ha := cost_le_r6c s B a h.1; have hb := cost_le_r6c s B b h.2.1
    have za := zsz_eval_le s B a h.1; have zb := zsz_eval_le s B b h.2.1
    simp only [cost, size]; (simp only [dupCost, moveCost, zipCost, addIntCost, addMagCost, subMagCost, smulCost, shlCost, splitCost, takeCost, ldivCost, pow2Cost] at *); nlinarith
  | shl a b, h => by
    have ha := cost_le_r6c s B a h.1; have hb := cost_le_r6c s B b h.2.1
    have za := zsz_eval_le s B a h.1; have zb := zsz_eval_le s B b h.2.1
    simp only [cost, size]; (simp only [dupCost, moveCost, zipCost, addIntCost, addMagCost, subMagCost, smulCost, shlCost, splitCost, takeCost, ldivCost, pow2Cost] at *); nlinarith
  | quo a b, h | rem a b, h => by
    have ha := cost_le_r6c s B a h.1; have hb := cost_le_r6c s B b h.2
    have za := zsz_eval_le s B a h.1; have zb := zsz_eval_le s B b h.2
    simp only [cost, size]; (simp only [dupCost, moveCost, zipCost, addIntCost, addMagCost, subMagCost, smulCost, shlCost, splitCost, takeCost, ldivCost, pow2Cost] at *); nlinarith
  | ndiv a b, h | nmod a b, h => by
    have ha := cost_le_r6c s B a h.1; have hb := cost_le_r6c s B b h.2.1
    have za := zsz_eval_le s B a h.1; have zb := zsz_eval_le s B b h.2.1
    simp only [cost, size]; (simp only [dupCost, moveCost, zipCost, addIntCost, addMagCost, subMagCost, smulCost, shlCost, splitCost, takeCost, ldivCost, pow2Cost] at *); nlinarith
  | neg a, h => by
    have ha := cost_le_r6c s B a h
    have : 1 ≤ (B + 2) ^ 2 := Nat.one_le_pow _ _ (by omega)
    simp only [cost, size]; nlinarith
  | pow2 a, h => by
    have ha := cost_le_r6c s B a h.1
    have za := zsz_eval_le s B a h.1
    have ht := h.2
    have zt : zsz (((a.eval s).toNat : ℕ) : ℤ) ≤ B := by
      have := zsz_natCast_le_self' (a.eval s).toNat; omega
    simp only [cost, size]; (simp only [dupCost, moveCost, zipCost, addIntCost, addMagCost, subMagCost, smulCost, shlCost, splitCost, takeCost, ldivCost, pow2Cost] at *); nlinarith
  | sel c x y, h => by
    have hc := cost_le_r6c s B c h.1
    have zc := zsz_eval_le s B c h.1
    simp only [cost, size]
    split_ifs with hn
    · have hx := cost_le_r6c s B x (by simpa [hn] using h.2)
      (simp only [dupCost, moveCost, zipCost, addIntCost, addMagCost, subMagCost, smulCost, shlCost, splitCost, takeCost, ldivCost, pow2Cost] at *); nlinarith
    · have hy := cost_le_r6c s B y (by simpa [hn] using h.2)
      (simp only [dupCost, moveCost, zipCost, addIntCost, addMagCost, subMagCost, smulCost, shlCost, splitCost, takeCost, ldivCost, pow2Cost] at *); nlinarith

end Ex

end NLogN

end

section
-- Source module: NLogN.HExprLin
/-!
# Linear cost bound for multiplication-free expressions

Expressions built from registers, literals, `add`, `neg`, `shl`, `quo`, `rem` and `sel` cost at
most `size · 2000 · (B + 2)` when every value has at most `B` bits.  This is what per-element
list operations use; products of large numbers go through the multiplication procedure instead.
-/

namespace NLogN

open IntMul

variable {S : ℕ}

namespace Ex

theorem cost_le_lin (s : IState S) (B : ℕ) : ∀ e : Ex S, e.Lin → e.Bnd s B →
    e.cost s ≤ e.size * 2000 * (B + 2)
  | reg i, _, h => by
    simp only [cost, size, Bnd] at h ⊢; (simp only [dupCost, moveCost, zipCost, addIntCost, addMagCost, subMagCost, smulCost, shlCost, splitCost, takeCost, ldivCost, pow2Cost] at *); nlinarith
  | lit c, _, h => by
    simp only [cost, size, Bnd] at h ⊢; nlinarith
  | add a b, hl, h => by
    have ha := cost_le_lin s B a hl.1 h.1; have hb := cost_le_lin s B b hl.2 h.2.1
    have za := zsz_eval_le s B a h.1; have zb := zsz_eval_le s B b h.2.1
    simp only [cost, size]; (simp only [dupCost, moveCost, zipCost, addIntCost, addMagCost, subMagCost, smulCost, shlCost, splitCost, takeCost, ldivCost, pow2Cost] at *); nlinarith
  | shl a b, hl, h => by
    have ha := cost_le_lin s B a hl.1 h.1; have hb := cost_le_lin s B b hl.2 h.2.1
    have za := zsz_eval_le s B a h.1; have zb := zsz_eval_le s B b h.2.1
    simp only [cost, size]; (simp only [dupCost, moveCost, zipCost, addIntCost, addMagCost, subMagCost, smulCost, shlCost, splitCost, takeCost, ldivCost, pow2Cost] at *); nlinarith
  | quo a b, hl, h | rem a b, hl, h => by
    have ha := cost_le_lin s B a hl.1 h.1; have hb := cost_le_lin s B b hl.2 h.2
    have za := zsz_eval_le s B a h.1; have zb := zsz_eval_le s B b h.2
    simp only [cost, size]; (simp only [dupCost, moveCost, zipCost, addIntCost, addMagCost, subMagCost, smulCost, shlCost, splitCost, takeCost, ldivCost, pow2Cost] at *); nlinarith
  | neg a, hl, h => by
    have ha := cost_le_lin s B a hl h
    simp only [cost, size]; nlinarith
  | sel c x y, hl, h => by
    have hc := cost_le_lin s B c hl.1 h.1
    have zc := zsz_eval_le s B c h.1
    simp only [cost, size]
    split_ifs with hn
    · have hx := cost_le_lin s B x hl.2.1 (by simpa [hn] using h.2)
      (simp only [dupCost, moveCost, zipCost, addIntCost, addMagCost, subMagCost, smulCost, shlCost, splitCost, takeCost, ldivCost, pow2Cost] at *); nlinarith
    · have hy := cost_le_lin s B y hl.2.2 (by simpa [hn] using h.2)
      (simp only [dupCost, moveCost, zipCost, addIntCost, addMagCost, subMagCost, smulCost, shlCost, splitCost, takeCost, ldivCost, pow2Cost] at *); nlinarith
  | mul _ _, hl, _ | pow2 _, hl, _ | ndiv _ _, hl, _ | nmod _ _, hl, _ => hl.elim

end Ex

end NLogN

end

section
-- Source module: NLogN.HReg
/-!
# Register programs

`RS` is a small structured language over the register stacks `0 … 55`: assignments of
expressions, pushes and pops, conditionals and counted loops.  `RS.run` is its functional
semantics on `IState`s, and `RS.code_runs` shows that the compiled `IStmt` realises it with cost
`RS.cost`.
-/

set_option linter.unusedSimpArgs false

namespace NLogN

open IntMul

variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P}

namespace RS

/-! ## Frame -/

theorem run_G_of_not_mem : ∀ (p : RS) (s : IState HS) (j : Fin HS), j ∉ p.writes →
    (p.run s).G j = s.G j
  | skip, s, j, _ => rfl
  | asg i e, s, j, h | push i e, s, j, h | pop i, s, j, h => by
    simp only [writes, List.mem_singleton] at h; simp [run, IState.upd_G, h]
  | seq a b, s, j, h => by
    simp only [writes, List.mem_append, not_or] at h
    simp only [run]; rw [run_G_of_not_mem b _ j h.2, run_G_of_not_mem a _ j h.1]
  | ite c a b, s, j, h => by
    simp only [writes, List.mem_append, not_or] at h
    simp only [run]; split_ifs
    · exact run_G_of_not_mem a _ j h.1
    · exact run_G_of_not_mem b _ j h.2
  | rep i n b, s, j, h => by
    simp only [writes, List.mem_cons, not_or] at h
    simp only [run, IState.upd_G, if_neg h.1]
    suffices H : ∀ k (t : IState HS), ((fun t => decSt i (b.run t))^[k] t).G j = t.G j by
      rw [H]; simp [IState.upd_G, h.1]
    intro k; induction k with
    | zero => intro t; rfl
    | succ k ih =>
      intro t
      rw [Function.iterate_succ_apply']
      have e := ih t
      generalize ((fun t => decSt i (b.run t))^[k] t) = X at e ⊢
      simp only [decSt, IState.upd_G, if_neg h.1]
      rw [run_G_of_not_mem b _ j h.2, e]

theorem repSt_G (i : Fin HS) (n : Ex HS) (b : RS) (s : IState HS) (hi : i ∉ b.writes) :
    ∀ k, (repSt i n b s k).G i = .int (n.eval s - k) :: s.G i := by
  intro k; induction k with
  | zero => simp [repSt, IState.upd_G]
  | succ k ih =>
    simp only [repSt] at ih ⊢
    rw [Function.iterate_succ_apply']
    generalize ((fun t => decSt i (b.run t))^[k] (s.upd i (.int (n.eval s) :: s.G i))) = X at ih ⊢
    have h1 := run_G_of_not_mem b X i hi
    rw [ih] at h1
    simp only [decSt, IState.upd_G, if_pos rfl, IState.top, h1, List.tail_cons]
    push_cast; ring_nf

/-! ## Compilation -/

theorem ne56 {i : Fin HS} (hi : i.val < 56) : (56 : Fin HS) ≠ i := by
  intro h; rw [← h] at hi; exact absurd hi (by decide)

theorem clean_of_lt {i : Fin HS} (hi : i.val < 56) : (Ex.reg i).Clean := by
  intro j hj
  simp only [Ex.regs, List.mem_singleton] at hj
  subst hj; simp only [zX_all, List.mem_cons, List.not_mem_nil, or_false]
  intro h; rcases h with h | h | h | h | h | h | h | h <;> (subst h; exact absurd hi (by decide))

theorem asg_runs (i : Fin HS) (e : Ex HS) (s : IState HS) (hi : i.val < 56) (hc : e.Clean)
    (hok : e.ok s) (hint : s.IsInt i) :
    IRuns I iprog (.seq (e.code zX) (.seq (.op (.drop i)) (.op (.mv zX.V i)))) s
      (s.upd i (.int (e.eval s) :: (s.G i).tail)) (asgCost i e s) := by
  have hne := ne56 hi
  have h1 := Ex.code_runs_r6c (I := I) (iprog := iprog) e s hc hok
  obtain ⟨L, hL⟩ := hint
  have h2 := IRuns.drop_r6c (I := I) (iprog := iprog) (s := s.upd 56 (.int (e.eval s) :: s.G 56))
    (i := i) (a := s.top i) (L := L) (by simp [IState.upd_G, Ne.symm hne, hL])
  have h3 := IRuns.mv_r6c (I := I) (iprog := iprog)
    (s := (s.upd 56 (.int (e.eval s) :: s.G 56)).upd i L) (i := zX.V) (j := i) (a := e.eval s)
    (L := s.G 56) (by simpa using hne) (by simp [IState.upd_G, hne])
  refine (h1.seq_r6c (h2.seq_r6c h3)).mono' ?_ (by simp only [asgCost]; omega)
  have hne' := Ne.symm hne
  apply IState.ext' <;> intros <;> simp only [IState.upd_G, IState.upd_ip, IState.upd_out] <;>
    split_ifs <;> simp_all

theorem code_runs : ∀ (p : RS) (s : IState HS), p.ok s →
    IRuns I iprog (p.code) s (p.run s) (p.cost s)
  | skip, s, _ => IRuns.skip_r6c s
  | asg i e, s, ⟨hi, hc, hok, hint⟩ => asg_runs i e s hi hc hok hint
  | push i e, s, ⟨hi, hc, hok⟩ => by
    have hne := ne56 hi
    have h1 := Ex.code_runs_r6c (I := I) (iprog := iprog) e s hc hok
    have h3 := IRuns.mv_r6c (I := I) (iprog := iprog)
      (s := s.upd 56 (.int (e.eval s) :: s.G 56)) (i := zX.V) (j := i) (a := e.eval s)
      (L := s.G 56) (by simpa using hne) (by simp [IState.upd_G])
    refine (h1.seq_r6c h3).mono' ?_ (by simp only [cost]; exact le_rfl)
    have hne' := Ne.symm hne
    simp only [run]
    apply IState.ext' <;> intros <;> simp only [IState.upd_G, IState.upd_ip, IState.upd_out] <;>
      split_ifs <;> simp_all
  | pop i, s, ⟨hi, L, hL⟩ => by
    have := IRuns.drop_r6c (I := I) (iprog := iprog) (s := s) (i := i) (a := s.top i) (L := L) hL
    exact this.mono' (by simp [run, hL]) (by simp [cost])
  | seq a b, s, ⟨ha, hb⟩ => by
    exact ((code_runs a s ha).seq_r6c (code_runs b _ hb)).mono' rfl (by simp [cost])
  | ite c a b, s, ⟨hcc, hoc, hab⟩ => by
    have h1 := Ex.code_runs_r6c (I := I) (iprog := iprog) c s hcc hoc
    have h2 := IRuns.mv_r6c (I := I) (iprog := iprog) (s := s.upd 56 (.int (c.eval s) :: s.G 56))
      (i := zX.V) (j := zX.A) (a := c.eval s) (L := s.G 56) (by decide) (by simp)
    set s2 := ((s.upd 56 (.int (c.eval s) :: s.G 56)).upd zX.V (s.G 56)).upd zX.A
      (.int (c.eval s) :: (s.upd 56 (.int (c.eval s) :: s.G 56)).G zX.A)
    have hd := IRuns.drop_r6c (I := I) (iprog := iprog) (s := s2) (i := zX.A) (a := c.eval s)
      (L := s.G 57) (by simp [s2])
    have e3 : s2.upd zX.A (s.G 57) = s := by simp only [s2]; ((apply IState.ext' <;> intros <;> simp +decide only [IState.upd_G, IState.upd_ip, IState.upd_out] <;> split_ifs <;> simp_all +decide))
    rw [e3] at hd
    by_cases hneg : c.eval s < 0
    · have hx := code_runs a s (by simpa [hneg] using hab)
      have hi := IRuns.iteT (I := I) (iprog := iprog) (i := zX.A) (f := fun k => k == .neg)
        (q := .seq (.op (.drop zX.A)) b.code)
        (by rw [cl_int s2 zX.A (c.eval s) (s.G 57) (by simp [s2])]; simp [hneg]; omega)
        (hd.seq_r6c hx)
      refine (h1.seq_r6c (h2.seq_r6c hi)).mono' (by simp [run, hneg]) ?_
      simp only [cost, if_pos hneg]; omega
    · have hy := code_runs b s (by simpa [hneg] using hab)
      have hi := IRuns.iteF (I := I) (iprog := iprog) (i := zX.A) (f := fun k => k == .neg)
        (p := .seq (.op (.drop zX.A)) a.code)
        (by rw [cl_int s2 zX.A (c.eval s) (s.G 57) (by simp [s2])]; simp [hneg]; split_ifs <;> simp)
        (hd.seq_r6c hy)
      refine (h1.seq_r6c (h2.seq_r6c hi)).mono' (by simp [run, hneg]) ?_
      simp only [cost, if_neg hneg]; omega
  | rep i n b, s, ⟨hi, hc, hok, hn0, hw, hb⟩ => by
    have hne := ne56 hi
    have hne' := Ne.symm hne
    have h1 := Ex.code_runs_r6c (I := I) (iprog := iprog) n s hc hok
    have h2 := IRuns.mv_r6c (I := I) (iprog := iprog)
      (s := s.upd 56 (.int (n.eval s) :: s.G 56)) (i := zX.V) (j := i) (a := n.eval s)
      (L := s.G 56) (by simpa using hne) (by simp [IState.upd_G])
    have e0 : ((s.upd 56 (.int (n.eval s) :: s.G 56)).upd zX.V (s.G 56)).upd i
        (.int (n.eval s) :: (s.upd 56 (.int (n.eval s) :: s.G 56)).G i) = repSt i n b s 0 := by
      simp only [repSt, Function.iterate_zero, id]
      apply IState.ext' <;> intros <;> simp only [IState.upd_G, IState.upd_ip, IState.upd_out] <;>
        split_ifs <;> simp_all
    rw [e0] at h2
    set N := (n.eval s).toNat with hN
    have hNv : n.eval s = N := by omega
    have hG := repSt_G i n b s hw
    have hloop := IRuns.loop (I := I) (iprog := iprog) (i := i) (f := fun c => c != .zero)
      (p := .seq b.code (.seq ((decE i).code zX) (.seq (.op (.drop i)) (.op (.mv zX.V i)))))
      (repSt i n b s)
      (fun k => b.cost (repSt i n b s k) + asgCost i (decE i) (b.run (repSt i n b s k))) N
      (fun k hk => by
        rw [cl_int _ i _ _ (hG k)]
        have : n.eval s - k ≠ 0 := by omega
        simp [this]; split_ifs <;> simp)
      (by rw [cl_int _ i _ _ (hG N)]; simp [hNv])
      (fun k hk => by
        have hbk := code_runs b (repSt i n b s k) (hb k hk)
        have hGb := run_G_of_not_mem b (repSt i n b s k) i hw
        rw [hG k] at hGb
        have hd := asg_runs (I := I) (iprog := iprog) i (decE i) (b.run (repSt i n b s k)) hi
          (by intro j hj; simp only [decE, Ex.regs, List.append_nil] at hj; exact clean_of_lt hi j hj)
          (by simp only [decE, Ex.ok, and_true]; exact IState.isInt_of_r6c hGb)
          (IState.isInt_of_r6c hGb)
        refine (hbk.seq_r6c hd).mono' ?_ le_rfl
        simp only [repSt, Function.iterate_succ_apply']
        simp only [repSt] at hGb
        simp only [decSt, decE, Ex.eval, sub_eq_add_neg])
    have hdrop := IRuns.drop_r6c (I := I) (iprog := iprog) (s := repSt i n b s N) (i := i)
      (a := n.eval s - N) (L := s.G i) (hG N)
    refine ((h1.seq_r6c h2).seq_r6c (hloop.seq_r6c hdrop)).mono' ?_ ?_
    · have hGN := hG N
      simp only [repSt] at hGN
      simp only [run, repSt, ← hN]
      rw [hGN]; rfl
    · have hz : zsz (n.eval s - N) = 0 := by rw [hNv, sub_self, zsz_zero_r6c]
      rw [hz]
      simp only [cost, ← hN]
      omega

/-! ## Sequences and reasoning lemmas -/

/-! ## Cost bounds -/

theorem pushCost_le_r6c (e : Ex HS) (s : IState HS) (B : ℕ) (h : e.Bnd s B) :
    e.cost s + (2 * moveCost (zsz (e.eval s)) + 19) ≤ (e.size + 1) * 10 ^ 7 * (B + 2) ^ 2 := by
  have h1 := Ex.cost_le_r6c s B e h
  have h2 := Ex.zsz_eval_le s B e h
  simp only [moveCost]; nlinarith

theorem run_rep (i : Fin HS) (n : Ex HS) (b : RS) (s : IState HS) (hw : i ∉ b.writes)
    (h0 : 0 ≤ n.eval s) :
    (rep i n b).run s = (repSt i n b s (n.eval s).toNat).upd i (s.G i) := by
  have := repSt_G i n b s hw (n.eval s).toNat
  simp only [repSt] at this
  simp only [run, repSt, this]; rfl

end RS

end NLogN

end

section
-- Source module: NLogN.HList
/-!
# Counted loops through a family of states

`rep_states`: if the body maps the `k`-th logical state (with the counter on top of `i`) to the
`(k+1)`-st, the loop computes the last one.  This is the interface used for list processing.
-/

set_option linter.unusedSimpArgs false

namespace NLogN

open IntMul RS

theorem decSt_withCtr (i : Fin HS) (s t : IState HS) (N k : ℕ) :
    decSt i (withCtr i s N k t) = withCtr i s N (k + 1) t := by
  have e : ((N : ℤ) - k - 1) = (N : ℤ) - (k + 1 : ℕ) := by push_cast; ring
  simp only [decSt, withCtr, IState.upd_upd_same, IState.top, IState.upd_G, if_true,
    List.tail_cons, e]

theorem RepStates.repSt {i : Fin HS} {n : Ex HS} {b : RS} {s : IState HS} {S : ℕ → IState HS}
    (h : RepStates i n b s S) :
    ∀ k ≤ (n.eval s).toNat, repSt i n b s k = withCtr i s (n.eval s).toNat k (S k) := by
  intro k
  induction k with
  | zero =>
    intro _
    have := h.nonneg
    have e : n.eval s = (((n.eval s).toNat : ℕ) : ℤ) - ((0 : ℕ) : ℤ) := by push_cast; omega
    simp only [RS.repSt, Function.iterate_zero, id, withCtr, h.h0]
    rw [← e]
  | succ k ih =>
    intro hk
    rw [RS.repSt, Function.iterate_succ_apply', ← RS.repSt, ih (by omega), h.step k (by omega)]
    exact decSt_withCtr i s _ _ _

theorem RepStates.run {i : Fin HS} {n : Ex HS} {b : RS} {s : IState HS} {S : ℕ → IState HS}
    (h : RepStates i n b s S) : (rep i n b).run s = S (n.eval s).toNat := by
  rw [run_rep i n b s h.hw h.nonneg, h.repSt _ le_rfl]
  simp only [withCtr, IState.upd_upd_same]
  rw [← h.hG (n.eval s).toNat, IState.upd_self]

theorem RepStates.ok {i : Fin HS} {n : Ex HS} {b : RS} {s : IState HS} {S : ℕ → IState HS}
    (h : RepStates i n b s S) (hi : i.val < 56) (hc : n.Clean) (hn : n.ok s)
    (hb : ∀ k < (n.eval s).toNat, b.ok (withCtr i s (n.eval s).toNat k (S k))) :
    (rep i n b).ok s :=
  ⟨hi, hc, hn, h.nonneg, h.hw, fun k hk => by rw [h.repSt k hk.le]; exact hb k hk⟩

end NLogN

end

section
-- Source module: NLogN.HRM
/-!
# Register programs with multiplication calls

`RM` extends the register programs `RS` by `mul k i j`, which pushes `top j * top i` onto `k`
by calling the multiplication procedure `pM` with the calling convention

  `ARG = 55 : a :: b :: L  ↦  (a * b) :: L`,

all other stacks unchanged.  The cost of a call and the inputs on which it may be used are a
parameter `M : MulSpec`; `RM.code_runs` holds whenever the procedure meets `MulOK M`.
-/

set_option linter.unusedSimpArgs false

namespace NLogN

open IntMul

variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P}

theorem IOp.run_frame {o : IOp HS} {s s' : IState HS} {c : ℕ} (h : o.run s = some (s', c))
    (j : Fin HS) (hj : j ∉ o.stks) : s'.G j = s.G j := by
  cases o <;> simp only [IOp.stks, List.mem_cons, List.not_mem_nil, or_false, not_or] at hj <;>
    simp only [IOp.run] at h <;> (repeat' split at h) <;> (try simp at h) <;>
    (try split_ifs at h) <;> (try simp at h) <;>
    (try (obtain ⟨rfl, rfl⟩ := h)) <;> (try (obtain ⟨_, rfl, rfl⟩ := h)) <;>
    simp_all [IState.upd_G]

namespace RM

open RS (decSt decE asgCost)

/-! ## Frame -/

theorem run_G_of_not_mem : ∀ (p : RM) (s : IState HS) (j : Fin HS), j ∉ p.writes →
    (p.run s).G j = s.G j
  | rs p, s, j, h => RS.run_G_of_not_mem p s j h
  | mul k i i', s, j, h => by
    simp only [writes, List.mem_singleton] at h; simp [run, IState.upd_G, h]
  | seq a b, s, j, h => by
    simp only [writes, List.mem_append, not_or] at h
    simp only [run]; rw [run_G_of_not_mem b _ j h.2, run_G_of_not_mem a _ j h.1]
  | ite c a b, s, j, h => by
    simp only [writes, List.mem_append, not_or] at h
    simp only [run]; split_ifs
    · exact run_G_of_not_mem a _ j h.1
    · exact run_G_of_not_mem b _ j h.2
  | rep i n b, s, j, h => by
    simp only [writes, List.mem_cons, not_or] at h
    simp only [run, IState.upd_G, if_neg h.1]
    suffices H : ∀ k (t : IState HS), ((fun t => decSt i (b.run t))^[k] t).G j = t.G j by
      rw [H]; simp [IState.upd_G, h.1]
    intro k; induction k with
    | zero => intro t; rfl
    | succ k ih =>
      intro t
      rw [Function.iterate_succ_apply']
      have e := ih t
      generalize ((fun t => decSt i (b.run t))^[k] t) = X at e ⊢
      simp only [decSt, IState.upd_G, if_neg h.1]
      rw [run_G_of_not_mem b _ j h.2, e]
  | op o, s, j, h => by
    simp only [run]; split
    · rename_i r hr; exact IOp.run_frame hr j h
    · rfl
  | prc _ f _ _ w hf _, s, j, h => hf s j h

theorem repSt_G (i : Fin HS) (n : Ex HS) (b : RM) (s : IState HS) (hi : i ∉ b.writes) :
    ∀ k, (repSt i n b s k).G i = .int (n.eval s - k) :: s.G i := by
  intro k; induction k with
  | zero => simp [repSt, IState.upd_G]
  | succ k ih =>
    simp only [repSt, Function.iterate_succ_apply'] at ih ⊢
    generalize ((fun t => decSt i (b.run t))^[k] (s.upd i (.int (n.eval s) :: s.G i))) = X at ih ⊢
    have := run_G_of_not_mem b X i hi
    simp only [decSt, IState.upd_G, if_true, IState.top, this, ih, List.tail_cons]
    push_cast; ring_nf

/-! ## Reasoning lemmas -/

theorem run_rep (i : Fin HS) (n : Ex HS) (b : RM) (s : IState HS) (hw : i ∉ b.writes)
    (h0 : 0 ≤ n.eval s) :
    (rep i n b).run s = (repSt i n b s (n.eval s).toNat).upd i (s.G i) := by
  have := repSt_G i n b s hw (n.eval s).toNat
  simp only [repSt] at this
  simp only [run, repSt, this]; rfl

/-! ## Counted loops through a family of states -/

theorem RepStates.repSt' {i : Fin HS} {n : Ex HS} {b : RM} {s : IState HS} {S : ℕ → IState HS}
    (h : RepStates i n b s S) :
    ∀ k ≤ (n.eval s).toNat, repSt i n b s k = withCtr i s (n.eval s).toNat k (S k) := by
  intro k
  induction k with
  | zero =>
    intro _
    have := h.nonneg
    have e : n.eval s = (((n.eval s).toNat : ℕ) : ℤ) - ((0 : ℕ) : ℤ) := by push_cast; omega
    simp only [RM.repSt, Function.iterate_zero, id, withCtr, h.h0]
    rw [← e]
  | succ k ih =>
    intro hk
    rw [RM.repSt, Function.iterate_succ_apply', ← RM.repSt, ih (by omega), h.step k (by omega)]
    exact decSt_withCtr i s _ _ _

theorem RepStates.run {i : Fin HS} {n : Ex HS} {b : RM} {s : IState HS} {S : ℕ → IState HS}
    (h : RepStates i n b s S) : (rep i n b).run s = S (n.eval s).toNat := by
  rw [run_rep i n b s h.hw h.nonneg, h.repSt' _ le_rfl]
  simp only [withCtr, IState.upd_upd_same]
  rw [← h.hG (n.eval s).toNat, IState.upd_self]

theorem RepStates.ok {M : MulSpec} {i : Fin HS} {n : Ex HS} {b : RM} {s : IState HS}
    {S : ℕ → IState HS}
    (h : RepStates i n b s S) (hi : i.val < 56) (hc : n.Clean) (hn : n.ok s)
    (hb : ∀ k < (n.eval s).toNat, b.ok M (withCtr i s (n.eval s).toNat k (S k))) :
    (rep i n b).ok M s :=
  ⟨hi, hc, hn, h.nonneg, h.hw, fun k hk => by rw [h.repSt' k hk.le]; exact hb k hk⟩

end RM

end NLogN

end

section
-- Source module: NLogN.HLinCost
/-!
# Linear cost bounds for assignments, pushes and counted loops

Loop overhead is linear in the size of the counter, so a pass over `n` elements costs
`O(n · (C + log n))` rather than `O(n · log² n)`.
-/

namespace NLogN

open IntMul

namespace RS

theorem asgCost_le_lin (i : Fin HS) (e : Ex HS) (s : IState HS) (B : ℕ) (hl : e.Lin)
    (h : e.Bnd s B) (hi : zsz (s.top i) ≤ B) :
    asgCost i e s ≤ (e.size + 1) * 2000 * (B + 2) := by
  have h1 := Ex.cost_le_lin s B e hl h
  have h2 := Ex.zsz_eval_le s B e h
  simp only [asgCost, moveCost]; nlinarith

theorem pushCost_le_lin (e : Ex HS) (s : IState HS) (B : ℕ) (hl : e.Lin) (h : e.Bnd s B) :
    e.cost s + (2 * moveCost (zsz (e.eval s)) + 19) ≤ (e.size + 1) * 2000 * (B + 2) := by
  have h1 := Ex.cost_le_lin s B e hl h
  have h2 := Ex.zsz_eval_le s B e h
  simp only [moveCost]; nlinarith

theorem decCost_le (i : Fin HS) (t : IState HS) (B : ℕ) (h1 : zsz (t.top i) ≤ B)
    (h2 : zsz (t.top i + -1) ≤ B) (hB : 1 ≤ B) : asgCost i (decE i) t ≤ 8000 * (B + 2) := by
  have := asgCost_le_lin i (decE i) t B (by simp [decE, Ex.Lin])
    (by simp only [decE, Ex.Bnd, Ex.eval]; refine ⟨h1, ?_, h2⟩; rw [zsz_neg_r6c, zsz_one_r6c]; omega) h1
  have hs : (decE i).size = 3 := rfl
  rw [hs] at this; omega

end RS

/-- Shared step of the loop cost bounds: the decrement in iteration `k` reads `N - k`. -/
theorem withCtr_dec_le {B : ℕ} (i : Fin HS) (s t : IState HS) (n : Ex HS) (k : ℕ)
    (hk : k < (n.eval s).toNat) (hB : zsz (n.eval s) ≤ B) :
    RS.asgCost i (RS.decE i) (withCtr i s (n.eval s).toNat k t) ≤ 8000 * (B + 2) := by
  have hv : zsz (((n.eval s).toNat : ℤ) - k) ≤ B := le_trans (zsz_mono_r6c (by omega)) hB
  have hv' : zsz (((n.eval s).toNat : ℤ) - k + -1) ≤ B := le_trans (zsz_mono_r6c (by omega)) hB
  have h1 : 1 ≤ B := by
    by_contra hc
    have := (zsz_le_iff (z := n.eval s) (m := 0)).1 (by omega); simp at this; omega
  apply RS.decCost_le
  · simpa [IState.top, withCtr] using hv
  · simpa [IState.top, withCtr] using hv'
  · exact h1

theorem RepStates.cost_le_lin {i : Fin HS} {n : Ex HS} {b : RS} {s : IState HS}
    {S : ℕ → IState HS}
    (h : RepStates i n b s S) (B C : ℕ) (hl : n.Lin) (hn : n.Bnd s B)
    (hb : ∀ k < (n.eval s).toNat, b.cost (withCtr i s (n.eval s).toNat k (S k)) ≤ C) :
    (RS.rep i n b).cost s ≤ (n.size + 1) * 2000 * (B + 2) +
      (n.eval s).toNat * (C + 8000 * (B + 2) + 30) + 32 := by
  have hB := Ex.zsz_eval_le s B n hn
  have h1 := RS.pushCost_le_lin n s B hl hn
  have h2 : ∑ k ∈ Finset.range (n.eval s).toNat, (b.cost (RS.repSt i n b s k) +
      RS.asgCost i (RS.decE i) (b.run (RS.repSt i n b s k)) + 30) ≤
      (n.eval s).toNat * (C + 8000 * (B + 2) + 30) := by
    have := Finset.sum_le_sum (s := Finset.range (n.eval s).toNat)
      (f := fun k => b.cost (RS.repSt i n b s k) +
        RS.asgCost i (RS.decE i) (b.run (RS.repSt i n b s k)) + 30)
      (g := fun _ => C + 8000 * (B + 2) + 30) (fun k hk => by
        have hk' := Finset.mem_range.1 hk
        rw [h.repSt k hk'.le]
        have := hb k hk'
        rw [h.step k hk']
        have := withCtr_dec_le i s (S (k + 1)) n k hk' hB
        omega)
    simpa using this
  simp only [RS.cost]; omega

end NLogN

end

section
-- Source module: NLogN.HRen
/-!
# Renaming stacks and procedures of item-language programs

Given a map of stacks `f : Fin S → Fin S'` and a map of procedure indices `g : Fin P → Fin P'`,
`IStmt.ren f g` renames every stack `i` to `f i` and every call `j` to `g j`.  For injective `f`,
executions are simulated: a run from `s` to `s'` becomes a run from `embed f s t` to `embed f s' t`,
where `IState.embed f s t` is `t` with the stacks in the image of `f` overwritten by those of `s`
(and `ip`, `out` taken from `s`).  Stacks outside the image of `f` are untouched.
-/

namespace NLogN

open IntMul

variable {S S' P P' : ℕ}

section Inj

variable {f : Fin S → Fin S'} (hf : Function.Injective f)
include hf

theorem IState.embed_G (s : IState S) (t : IState S') (x : Fin S) :
    (IState.embed f s t).G (f x) = s.G x := hf.extend_apply _ _ _

omit hf in
theorem IState.embed_G_of_not (s : IState S) (t : IState S') (y : Fin S') (hy : ∀ x, f x ≠ y) :
    (IState.embed f s t).G y = t.G y :=
  Function.extend_apply' _ _ _ (by rintro ⟨x, hx⟩; exact hy x hx)

theorem IState.embed_upd (s : IState S) (t : IState S') (i : Fin S) (L : List Item) :
    IState.embed f (s.upd i L) t = (IState.embed f s t).upd (f i) L := by
  refine IState.ext' (fun y => ?_) rfl rfl
  by_cases hy : ∃ x, f x = y
  · obtain ⟨x, rfl⟩ := hy
    rw [IState.embed_G hf, IState.upd_G, IState.upd_G, IState.embed_G hf]
    by_cases h : x = i
    · simp [h]
    · simp [h, hf.ne h]
  · push Not at hy
    rw [IState.embed_G_of_not _ _ _ hy, IState.upd_G, if_neg (hy i).symm,
      IState.embed_G_of_not _ _ _ hy]

theorem IState.embed_cl (s : IState S) (t : IState S') (i : Fin S) :
    (IState.embed f s t).cl (f i) = s.cl i := by
  simp only [IState.cl, IState.embed_G hf]

variable {I : List Sym}

theorem IOp.Step.ren {o : IOp S} {s s' : IState S} {c : ℕ} (h : o.Step I s s' c)
    (t : IState S') : (o.ren f).Step I (IState.embed f s t) (IState.embed f s' t) c := by
  cases h with
  | add hij hi hj =>
    rename_i i j k a b Li Lj
    have := IOp.Step.add (I := I) (s := IState.embed f s t) (k := f k) (hf.ne hij)
      (by rw [IState.embed_G hf, hi]) (by rw [IState.embed_G hf, hj])
    simp only [← IState.embed_upd hf, IState.embed_G hf] at this
    exact this
  | neg hi =>
    have := IOp.Step.neg (I := I) (s := IState.embed f s t) (by rw [IState.embed_G hf, hi])
    simp only [← IState.embed_upd hf] at this
    exact this
  | dup hij hi =>
    have := IOp.Step.dup (I := I) (s := IState.embed f s t) (hf.ne hij)
      (by rw [IState.embed_G hf, hi])
    simp only [← IState.embed_upd hf, IState.embed_G hf] at this
    exact this
  | drop hi =>
    have := IOp.Step.drop (I := I) (s := IState.embed f s t) (by rw [IState.embed_G hf, hi])
    simp only [← IState.embed_upd hf] at this
    exact this
  | mv hij hi =>
    have := IOp.Step.mv (I := I) (s := IState.embed f s t) (hf.ne hij)
      (by rw [IState.embed_G hf, hi])
    simp only [← IState.embed_upd hf, IState.embed_G hf] at this
    exact this
  | const c =>
    rename_i i
    have := IOp.Step.const (I := I) (s := IState.embed f s t) (i := f i) c
    simp only [← IState.embed_upd hf, IState.embed_G hf] at this
    exact this
  | mark =>
    rename_i i
    have := IOp.Step.mark (I := I) (s := IState.embed f s t) (i := f i)
    simp only [← IState.embed_upd hf, IState.embed_G hf] at this
    exact this
  | unmark hi =>
    have := IOp.Step.unmark (I := I) (s := IState.embed f s t) (by rw [IState.embed_G hf, hi])
    simp only [← IState.embed_upd hf] at this
    exact this
  | shl hij hi hj =>
    have := IOp.Step.shl (I := I) (s := IState.embed f s t) (hf.ne hij)
      (by rw [IState.embed_G hf, hi]) (by rw [IState.embed_G hf, hj])
    simp only [← IState.embed_upd hf] at this
    exact this
  | split hij hik hjk hi hj =>
    have := IOp.Step.split (I := I) (s := IState.embed f s t) (hf.ne hij) (hf.ne hik)
      (hf.ne hjk) (by rw [IState.embed_G hf, hi]) (by rw [IState.embed_G hf, hj])
    simp only [← IState.embed_upd hf, IState.embed_G hf] at this
    exact this
  | read W hij hs0 hs1 hk hstop =>
    have := IOp.Step.read (I := I) (s := IState.embed f s t) W (hf.ne hij) hs0 hs1 hk hstop
    simp only [← IState.embed_upd hf, IState.embed_G hf] at this
    exact this
  | write hij hn hi hj =>
    have := IOp.Step.write (I := I) (s := IState.embed f s t) (hf.ne hij) hn
      (by rw [IState.embed_G hf, hi]) (by rw [IState.embed_G hf, hj])
    simp only [← IState.embed_upd hf] at this
    exact this
  | cat hij hik hjk ha hb hi hj hk =>
    have := IOp.Step.cat (I := I) (s := IState.embed f s t) (hf.ne hij) (hf.ne hik) (hf.ne hjk)
      ha hb (by rw [IState.embed_G hf, hi]) (by rw [IState.embed_G hf, hj])
      (by rw [IState.embed_G hf, hk])
    simp only [← IState.embed_upd hf] at this
    exact this

/-- **Simulation**: a renamed program runs on the embedded states, with the same cost. -/
theorem IExec.ren {iprog : Fin P → IStmt S P} {iprog' : Fin P' → IStmt S' P'} {g : Fin P → Fin P'}
    (hprog : ∀ j, iprog' (g j) = (iprog j).ren f g) {p : IStmt S P} {s s' : IState S} {c : ℕ}
    (h : IExec I iprog p s s' c) (t : IState S') :
    IExec I iprog' (p.ren f g) (IState.embed f s t) (IState.embed f s' t) c := by
  induction h with
  | skip s => exact .skip _
  | op h => exact .op (h.ren hf t)
  | seq _ _ ih₁ ih₂ => exact .seq ih₁ ih₂
  | iteT hc _ ih => exact .iteT (by rw [IState.embed_cl hf]; exact hc) ih
  | iteF hc _ ih => exact .iteF (by rw [IState.embed_cl hf]; exact hc) ih
  | loopT hc _ _ ih₁ ih₂ => exact .loopT (by rw [IState.embed_cl hf]; exact hc) ih₁ ih₂
  | loopF hc => exact .loopF (by rw [IState.embed_cl hf]; exact hc)
  | call _ ih => exact .call (by rw [hprog]; exact ih)

theorem IRuns.ren {iprog : Fin P → IStmt S P} {iprog' : Fin P' → IStmt S' P'} {g : Fin P → Fin P'}
    (hprog : ∀ j, iprog' (g j) = (iprog j).ren f g) {p : IStmt S P} {s s' : IState S} {c : ℕ}
    (h : IRuns I iprog p s s' c) (t : IState S') :
    IRuns I iprog' (p.ren f g) (IState.embed f s t) (IState.embed f s' t) c := by
  obtain ⟨c', hc, h⟩ := h
  exact ⟨c', hc, IExec.ren hf hprog h t⟩

end Inj

end NLogN

end

section
-- Source module: Solutions.ButterflyGuard
/-!
# §5.4 An explicit guard-width bound (and the numeric parts of Proposition 14)

1. The constants `E = 64(W+m+1)³`, `B = s+E`, `ν = min{j ≥ 1 : m^j ≥ B}`, `C1 = max{20, ν+3}`,
   `C0 = 128 m B²` for the complex network `m = 10⁶`, `W_c`, `s_c`: `m^10 < B < m^11`, `ν = 11`,
   `C1 = 20`.
2. The depth recurrence `A(e) ≤ s A(e/m) + E`, `A ≤ 8e` at leaves, gives `A ≤ 8 d B^{k+1}
   ≤ 8 B² d^{ν+1}`, and the final chain `8mB²d^{ν+2}+8d+t+9 ≤ … < 128mB²d^{ν+3} ≤ C0 d^{C1}`.
3. Dyadic growth: a value at arithmetic depth `ℓ` (add, sub, halve, negate, multiply by `i`)
   lies in `2^{-(p+ℓ)} ℤ[i]` with modulus `≤ 2^ℓ`; hence `p+Δ` fractional and `Δ+3` integer and
   sign bits represent it exactly.
4. The final truncation `Q_p` toward zero: `|Q_p z| ≤ |z|`, `|Q_p z - z| < √2 · 2^{-p}`.
5. The width bookkeeping of the proof of Proposition 14.
-/

namespace Butterfly

open Complex

/-! ## 1. The constants -/

/-- The constants of the complex network (Proposition 8). -/
def mc : ℕ := 1000000
def Wc : ℕ := 1873807244643542670000
def sc : ℕ := 1873807244636671267308000000

/-! ## 2. Depth recurrence and the chain -/

/-! ## 3. Dyadic depth invariant -/

lemma DyGood.mono {p ℓ ℓ' : ℕ} {z : ℂ} (h : DyGood p ℓ z) (hl : ℓ ≤ ℓ') : DyGood p ℓ' z := by
  obtain ⟨⟨a, b, rfl⟩, hn⟩ := h
  refine ⟨⟨a * 2 ^ (ℓ' - ℓ), b * 2 ^ (ℓ' - ℓ), ?_⟩, hn.trans (pow_le_pow_right₀ (by norm_num) hl)⟩
  have : (2 : ℂ) ^ (p + ℓ') = 2 ^ (p + ℓ) * 2 ^ (ℓ' - ℓ) := by
    rw [← pow_add]; congr 1; omega
  rw [this]; push_cast
  field_simp

lemma DyGood.add {p ℓ ℓ' : ℕ} {z w : ℂ} (hz : DyGood p ℓ z) (hw : DyGood p ℓ' w) :
    DyGood p (max ℓ ℓ' + 1) (z + w) := by
  obtain ⟨⟨a, b, ha⟩, hz'⟩ := hz.mono (le_max_left ℓ ℓ')
  obtain ⟨⟨c, e, hc⟩, hw'⟩ := hw.mono (le_max_right ℓ ℓ')
  refine ⟨⟨(a + c) * 2, (b + e) * 2, ?_⟩, ?_⟩
  · rw [ha, hc, ← add_assoc p, pow_succ]; push_cast; field_simp; ring
  · calc ‖z + w‖ ≤ ‖z‖ + ‖w‖ := norm_add_le _ _
      _ ≤ 2 ^ max ℓ ℓ' + 2 ^ max ℓ ℓ' := add_le_add hz' hw'
      _ = 2 ^ (max ℓ ℓ' + 1) := by ring

/-! ## 4. Final truncation toward zero -/

/-! ## 5. Width bookkeeping in the proof of Proposition 14 -/

end Butterfly

end

section
-- Source module: Solutions.ButterflyPacked
/-!
# §5.2 Lemma 13: packed selected-bit addition on one rectangle

1. (20)/(21): eight controlled `±1` updates of `(u, w)` give `(u + c(1 - 2(u mod 2)), w)`.
2. The packed lines (22) on `L = fK`-bit chunks `y, z` (mod `2^L`), with the `f - 1` segments
   at `j_i = ρ + iK` and controls `c_i = x_{j_i}`: outside the guard set `B` (23), their
   composite `S0` equals the ideal map `T0` (flip `y_{j_i}` where `c_i = 1`, fix `x, z`).
3. Bijections agreeing off `B` with `T0(B) = B` satisfy `S0(B) = B` (the repair permutes `B`).
4. (24): the guard count `|B| · 2^K ≤ 80 (f-1) · 2^{3L}`.
-/

namespace Butterfly

open Finset

/-! ## 1. The eight scalar updates (20) -/

/-! ## 2. Segment packing -/

variable (K : ℕ)

/-! ## 3. The packed lines (22) -/

variable (ρ f : ℕ)

/-- Packed segment state: both chunks packed with segments in a safe range. -/
structure SegState (y z : ℤ) where
  loy : ℤ
  loz : ℤ
  hy : ℤ
  hz : ℤ
  u : ℕ → ℤ
  w : ℕ → ℤ
  hloy : 0 ≤ loy ∧ loy < 2 ^ ρ
  hloz : 0 ≤ loz ∧ loz < 2 ^ ρ
  hhy : 0 ≤ hy ∧ hy < 2 ^ (K - ρ)
  hhz : 0 ≤ hz ∧ hz < 2 ^ (K - ρ)
  ey : y = packed K ρ (f - 1) loy u hy
  ez : z = packed K ρ (f - 1) loz w hz

variable {K ρ f}

/-! ## 4. Address form: guards and the ideal map -/

variable (K ρ f)

variable {K ρ f}

/-! ## 5. The repair permutes `B` -/

/-! ## 6. The guard count (24) -/

end Butterfly

end

section
-- Source module: Solutions.KIL6Den
/-!
# KIL6: Lemma 12 as a uniform IL program — the list denotations

The IL program of KIL6 realises the Lemma 12 interchange with the following data flow (array
model, `AModelL12`):

1. **binary padding** `binShape … (2^u) → binShape … (q^e)`: two one-field paddings
   (`padL`, `embed_binShape`);
2. **high swaps**: `r = min ρ e` single-digit interchanges (`highSwaps`);
3. if `n = e - r > 0`, the **middle part** `l12mid`: the row field is the prefix
   `Pre ++ [q]^r` (volume `vol Pre · q^r`), padded to `padRows W Kp (q^r)` rows (`padL`); the
   Prop. 11 oracle runs on the pieces (`runPieces … pieceLevels`), with the gap
   `G ++ [q]^r` (the already interchanged high digits of the second chunk belong to the gap);
   the padding is scanned away (`unpadL`);
4. **binary extraction** (two `unpadL`).

Compared with `AModelL12.l12q` this variant needs no joining rotation: the interchanged high
digits `d⁺` simply stay inside the gap.  `l12v_correct` proves that it is the interchange
`swapPos` of the two `[2^u]` fields, from the same oracle specification `OracleSpec`.

The list functions `padL` / `unpadL` are the one-field embeddings / extractions in the chunk
form the IL loops produce (`embed_eq_padL`, `extract_eq_unpadL`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN.KIL

open AModel AModelL12

/-! ## One-field padding and extraction in chunk form -/

section Pad

variable {α : Type*}

/-! ## Composing embeddings and extractions -/

theorem ShapeLE.trans {S T U : Shape} (h1 : ShapeLE S T) (h2 : ShapeLE T U) : ShapeLE S U :=
  ⟨h1.1.trans h2.1, fun k a b => le_trans (h1.2 k a (by rw [← h1.1]; exact a)) (h2.2 k _ b)⟩

end Pad

/-! ## The binary and row paddings in chunk form -/

/-! ## The variant procedure and its correctness -/

/-! ## Auxiliary facts: pieces, digits, maps -/

end NLogN.KIL

end
Source
S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean modules Solutions/HExprPf.lean, Solutions/HExprPow.lean, Solutions/HExprDiv.lean, Solutions/HExprRun.lean, Solutions/HExprCost.lean, Solutions/HExprLin.lean, Solutions/HReg.lean, Solutions/HList.lean, Solutions/HRM.lean, Solutions/HLinCost.lean, Solutions/HRen.lean, Solutions/ButterflyGuard.lean, Solutions/ButterflyPacked.lean, Solutions/KIL6Den.lean.

View graph