feat(wordram): implement the complete native convolution host

Complexity.lean

@@ -102,6 +102,9 @@ public import Complexity.Algorithms.WordRAM.Karger.FastCut
 public import Complexity.Algorithms.WordRAM.Karger.Graph
 public import Complexity.Algorithms.WordRAM.KargerMinCut
 public import Complexity.Algorithms.WordRAM.KargerStein
+public import Complexity.Algorithms.WordRAM.NatClog
+public import Complexity.Algorithms.WordRAM.NatLog
+public import Complexity.Algorithms.WordRAM.NatSqrt
 public import Complexity.Algorithms.WordRAM.PrefixSums.Dynamic
 public import Complexity.Algorithms.WordRAM.PrefixSums.Query
 public import Complexity.Algorithms.WordRAM.PrefixSums.Tree
@@ -134,8 +137,13 @@ public import Complexity.Algorithms.WordRAM.Stack.Controller
 public import Complexity.Algorithms.WordRAM.ThreeSum.Cell
 public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Collisions
 public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Count
+public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Parameters
 public import Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Residues
 public import Complexity.Algorithms.WordRAM.ThreeSum.Fill
+public import Complexity.Algorithms.WordRAM.ThreeSum.Host.Loop
+public import Complexity.Algorithms.WordRAM.ThreeSum.Host.Prepare
+public import Complexity.Algorithms.WordRAM.ThreeSum.Host.Program
+public import Complexity.Algorithms.WordRAM.ThreeSum.Host.Width
 public import Complexity.Algorithms.WordRAM.ThreeSum.Memory
 public import Complexity.Algorithms.WordRAM.ThreeSum.Weight
 public import Complexity.Algorithms.WordRAM.VanEmdeBoas.Call
@@ -1698,6 +1706,7 @@ public import Complexity.Computability.WordRAM.Randomized.Defs
 public import Complexity.Computability.WordRAM.Randomized.Expected
 public import Complexity.Computability.WordRAM.Randomized.LoopSegment
 public import Complexity.Computability.WordRAM.Randomized.Structured
+public import Complexity.Computability.WordRAM.RegisterFrame
 public import Complexity.Computability.WordRAM.Signed.Arithmetic
 public import Complexity.Computability.WordRAM.Signed.Comparison
 public import Complexity.Computability.WordRAM.Signed.Compile

Complexity/Algorithms/WordRAM/FusionTree/Node/Registers.lean

@@ -9,6 +9,7 @@ module
 
 public import Complexity.Algorithms.WordRAM.FusionTree.Parameters
 public import Complexity.Algorithms.WordRAM.FusionTree.ReadHeader
+public import Complexity.Computability.WordRAM.RegisterFrame
 
 /-!
 # Register banks for fusion-node queries
@@ -75,25 +76,12 @@ theorem bank_injective {k offset : ℕ} (hk : offset + k ≤ registers) :
   dsimp only [bank] at this
   omega
 
-/-- A renamed subroutine cannot write a register outside its embedding. This proof treats
-the subroutine structurally and does not expand its instruction graph. -/
-private theorem preserves_rename {k : ℕ} {f : Fin k → Fin registers} (c : Code .standard k)
-    (i : Fin registers) (hi : ∀ j, f j ≠ i) : (c.rename f).Preserves i := by
-  induction c with
-  | op o =>
-    cases o <;> simp only [Code.rename, Code.Preserves, Op.rename, Op.dest,
-      ne_eq, Option.some.injEq, reduceCtorEq, not_false_eq_true] <;> apply hi
-  | seq a b iha ihb => exact ⟨iha, ihb⟩
-  | branch cond pos neg ihp ihn => exact ⟨ihp, ihn⟩
-  | loop cond body ih => exact ih
-  | rand dst src => simpa only [Code.rename, Code.Preserves] using hi dst
-
 /-- In particular, a contiguous bank frames every physical register outside its interval. -/
 theorem preserves_bank {k offset : ℕ} (hk : offset + k ≤ registers)
     (c : Code .standard k) (i : Fin registers)
     (hi : i.val < offset ∨ offset + k ≤ i.val) :
     (c.rename (bank offset hk)).Preserves i := by
-  apply preserves_rename
+  apply Code.preserves_rename_of_forall_ne
   intro j he
   have := congrArg Fin.val he
   dsimp only [bank] at this

Complexity/Algorithms/WordRAM/NatClog.lean

@@ -0,0 +1,116 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.WordRAM.Notation
+public import Mathlib.Data.Nat.Log
+
+/-!
+# A charged native ceiling binary logarithm
+
+## Main definitions
+
+* `NatClog.program`: successive ceiling division by two.
+
+## Main results
+
+* `NatClog.exec`: the ceiling logarithm with a logarithmic charged instruction bound.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.NatClog
+
+open Cslib.WordRAM
+
+/-- Quotient, initially the input. -/
+abbrev arg : Fin 4 := 0
+/-- Ceiling logarithm output. -/
+abbrev result : Fin 4 := 1
+/-- Constant one. -/
+abbrev one : Fin 4 := 2
+/-- Constant two. -/
+abbrev two : Fin 4 := 3
+
+/-- Divide the quotient by two and increment the answer. -/
+def body : Code .standard 4 := ram[ arg ← arg + one; arg ← arg / two; result ← result + one ]
+
+/-- Fixed code for `Nat.clog 2`, including its value zero at input zero. -/
+def program : Code .standard 4 :=
+  .seq (ram[ result ← #0; one ← #1; two ← #2 ]) (.loop (.lt one arg) body)
+
+/-- Compute the ceiling binary logarithm in at most `5 ⌈log₂ n⌉ + 5` instructions.
+Memory is untouched and the input quotient is consumed. -/
+theorem exec {w : ℕ} (x : Data 4) (h2 : Fits w 2) (hn : Fits w (x.regs arg + 1))
+    (hout : Fits w (Nat.clog 2 (x.regs arg) + 1)) :
+    ∃ y, ExecWithin w program x y (5 * Nat.clog 2 (x.regs arg) + 5) ∧
+      y.regs result = Nat.clog 2 (x.regs arg) ∧ y.mem = x.mem ∧
+      y.regs one = 1 ∧ y.regs two = 2 := by
+  let I (y : Data 4) : Prop := y.regs one = 1 ∧ y.regs two = 2 ∧
+    y.regs arg ≤ x.regs arg ∧
+    y.regs result + Nat.clog 2 (y.regs arg) = Nat.clog 2 (x.regs arg) ∧ y.mem = x.mem
+  have hbody (y : Data 4) (hy : I y) (hc : (Cond.lt one arg).Holds y) :
+      ∃ z, ExecWithin w body y z 3 ∧ I z ∧
+        Nat.clog 2 (z.regs arg) < Nat.clog 2 (y.regs arg) := by
+    obtain ⟨ho, ht, harg, hsum, hm⟩ := hy
+    have hgt : 1 < y.regs arg := by simpa only [Cond.holds_lt, ho] using hc
+    have hpos : 0 < Nat.clog 2 (y.regs arg) := Nat.clog_pos (by decide) (by omega)
+    have hadd : Fits w (y.regs arg + 1) := hn.of_le (by omega)
+    have hdiv : Fits w ((y.regs arg + 1) / 2) :=
+      hn.of_le ((Nat.div_le_self _ _).trans (by omega))
+    have hinc : Fits w (y.regs result + 1) := hout.of_le (by omega)
+    refine ⟨?z, ?run, ?inv, ?decrease⟩
+    case run => ram_eval [body, ho, ht, hadd, hdiv, hinc, arg, result, one, two, Fin.mk.injEq]
+    case inv =>
+      refine ⟨?_, ?_, ?_, ?_, ?_⟩
+      · simpa +decide [Function.update_apply] using ho
+      · simpa +decide [Function.update_apply] using ht
+      · simpa +decide [Function.update_apply] using
+          (show (y.regs arg + 1) / 2 ≤ x.regs arg from by omega)
+      · change y.regs result + 1 + Nat.clog 2 ((y.regs arg + 1) / 2) = Nat.clog 2 (x.regs arg)
+        have h := Nat.clog_of_two_le (b := 2) (by decide) (by omega : 2 ≤ y.regs arg)
+        simp only [show y.regs arg + 2 - 1 = y.regs arg + 1 by omega] at h
+        omega
+      · exact hm
+    case decrease =>
+      change Nat.clog 2 ((y.regs arg + 1) / 2) < Nat.clog 2 (y.regs arg)
+      have h := Nat.clog_of_two_le (b := 2) (by decide) (by omega : 2 ≤ y.regs arg)
+      simp only [show y.regs arg + 2 - 1 = y.regs arg + 1 by omega] at h
+      omega
+  let x₀ := ((x.set result 0).set one 1).set two 2
+  have hx₀ : I x₀ := by simp +decide [I, x₀, arg, result, one, two]
+  obtain ⟨y, he, hy, hc⟩ := ExecWithin.loop_invariant I
+    (fun y => Nat.clog 2 (y.regs arg)) hbody hx₀
+  obtain ⟨ho, ht, harg, hsum, hm⟩ := hy
+  have hzero : Nat.clog 2 (y.regs arg) = 0 := by
+    have hle : y.regs arg ≤ 1 := by simpa only [Cond.holds_lt, ho, not_lt] using hc
+    exact Nat.clog_of_right_le_one hle 2
+  refine ⟨y, ?_, by omega, hm, ho, ht⟩
+  have h1 : Fits w 1 := h2.of_le (by decide)
+  have hinit : ExecWithin (B := .standard) w (ram[ result ← #0; one ← #1; two ← #2 ]) x x₀ 3 := by
+    ram_eval [x₀, h1, h2]
+  convert hinit.seq he using 1
+  · rfl
+  · simp +decide only [x₀, Data.set_regs, Function.update_apply, arg, result, one, two,
+      ↓reduceIte]
+    omega
+
+/-- Run the routine on any injectively chosen registers. -/
+theorem exec_rename {r w : ℕ} (f : Fin 4 → Fin r) (hf : f.Injective) (x : Data r)
+    (h2 : Fits w 2) (hn : Fits w (x.regs (f arg) + 1))
+    (hout : Fits w (Nat.clog 2 (x.regs (f arg)) + 1)) :
+    ∃ y, ExecWithin w (program.rename f) x y (5 * Nat.clog 2 (x.regs (f arg)) + 5) ∧
+      y.regs (f result) = Nat.clog 2 (x.regs (f arg)) ∧ y.mem = x.mem ∧
+      y.regs (f one) = 1 ∧ y.regs (f two) = 2 := by
+  obtain ⟨a, ha, hr, hm, ho, ht⟩ := exec (x.comap f) h2 hn hout
+  refine ⟨a.extend f x, ha.rename hf, ?_, hm, ?_, ?_⟩
+  · exact (hf.extend_apply _ _ result).trans hr
+  · exact (hf.extend_apply _ _ one).trans ho
+  · exact (hf.extend_apply _ _ two).trans ht
+
+end Cslib.Algorithms.WordRAM.NatClog

Complexity/Algorithms/WordRAM/NatLog.lean

@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.WordRAM.Notation
+public import Mathlib.Data.Nat.Log
+
+/-!
+# A charged native binary logarithm
+
+## Main definitions
+
+* `NatLog.program`: successive division by two.
+
+## Main results
+
+* `NatLog.exec`: the floor logarithm with a logarithmic charged instruction bound.
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.WordRAM.NatLog
+
+open Cslib.WordRAM
+
+/-- Quotient, initially the input. -/
+abbrev arg : Fin 4 := 0
+/-- Floor logarithm output. -/
+abbrev result : Fin 4 := 1
+/-- Constant one. -/
+abbrev one : Fin 4 := 2
+/-- Constant two. -/
+abbrev two : Fin 4 := 3
+
+/-- Divide the quotient by two and increment the answer. -/
+def body : Code .standard 4 := ram[ arg ← arg / two; result ← result + one ]
+
+/-- Fixed code for `Nat.log 2`, including its value zero at input zero. -/
+def program : Code .standard 4 :=
+  .seq (ram[ result ← #0; one ← #1; two ← #2 ]) (.loop (.lt one arg) body)
+
+/-- Compute the floor binary logarithm in at most `4 log₂ n + 5` instructions.
+Memory is untouched and the input quotient is consumed. -/
+theorem exec {w : ℕ} (x : Data 4) (h2 : Fits w 2) (hn : Fits w (x.regs arg))
+    (hout : Fits w (Nat.log 2 (x.regs arg) + 1)) :
+    ∃ y, ExecWithin w program x y (4 * Nat.log 2 (x.regs arg) + 5) ∧
+      y.regs result = Nat.log 2 (x.regs arg) ∧ y.mem = x.mem ∧
+      y.regs one = 1 ∧ y.regs two = 2 := by
+  let I (y : Data 4) : Prop := y.regs one = 1 ∧ y.regs two = 2 ∧
+    y.regs arg ≤ x.regs arg ∧
+    y.regs result + Nat.log 2 (y.regs arg) = Nat.log 2 (x.regs arg) ∧ y.mem = x.mem
+  have hbody (y : Data 4) (hy : I y) (hc : (Cond.lt one arg).Holds y) :
+      ∃ z, ExecWithin w body y z 2 ∧ I z ∧
+        Nat.log 2 (z.regs arg) < Nat.log 2 (y.regs arg) := by
+    obtain ⟨ho, ht, harg, hsum, hm⟩ := hy
+    have hgt : 1 < y.regs arg := by simpa only [Cond.holds_lt, ho] using hc
+    have hpos : 0 < Nat.log 2 (y.regs arg) := Nat.log_pos (by decide) (by omega)
+    have hdiv : Fits w (y.regs arg / 2) := hn.of_le ((Nat.div_le_self _ _).trans harg)
+    have hinc : Fits w (y.regs result + 1) := hout.of_le (by omega)
+    refine ⟨?z, ?run, ?inv, ?decrease⟩
+    case run => ram_eval [body, ho, ht, hdiv, hinc, arg, result, one, two, Fin.mk.injEq]
+    case inv =>
+      refine ⟨?_, ?_, ?_, ?_, ?_⟩
+      · simpa +decide [Function.update_apply] using ho
+      · simpa +decide [Function.update_apply] using ht
+      · simpa +decide [Function.update_apply] using (Nat.div_le_self (y.regs arg) 2).trans harg
+      · change y.regs result + 1 + Nat.log 2 (y.regs arg / 2) = Nat.log 2 (x.regs arg)
+        rw [Nat.log_div_base]
+        omega
+      · exact hm
+    case decrease =>
+      change Nat.log 2 (y.regs arg / 2) < Nat.log 2 (y.regs arg)
+      rw [Nat.log_div_base]
+      omega
+  let x₀ := ((x.set result 0).set one 1).set two 2
+  have hx₀ : I x₀ := by simp +decide [I, x₀, arg, result, one, two]
+  obtain ⟨y, he, hy, hc⟩ := ExecWithin.loop_invariant I
+    (fun y => Nat.log 2 (y.regs arg)) hbody hx₀
+  obtain ⟨ho, ht, harg, hsum, hm⟩ := hy
+  have hzero : Nat.log 2 (y.regs arg) = 0 := by
+    have hle : y.regs arg ≤ 1 := by simpa only [Cond.holds_lt, ho, not_lt] using hc
+    exact Nat.log_eq_zero_iff.mpr (Or.inl (by omega))
+  refine ⟨y, ?_, by omega, hm, ho, ht⟩
+  have h1 : Fits w 1 := h2.of_le (by decide)
+  have hinit : ExecWithin (B := .standard) w (ram[ result ← #0; one ← #1; two ← #2 ]) x x₀ 3 := by
+    ram_eval [x₀, h1, h2]
+  convert hinit.seq he using 1
+  · rfl
+  · simp +decide only [x₀, Data.set_regs, Function.update_apply, arg, result, one, two,
+      ↓reduceIte]
+    omega
+
+/-- Run the routine on any injectively chosen registers. -/
+theorem exec_rename {r w : ℕ} (f : Fin 4 → Fin r) (hf : f.Injective) (x : Data r)
+    (h2 : Fits w 2) (hn : Fits w (x.regs (f arg)))
+    (hout : Fits w (Nat.log 2 (x.regs (f arg)) + 1)) :
+    ∃ y, ExecWithin w (program.rename f) x y (4 * Nat.log 2 (x.regs (f arg)) + 5) ∧
+      y.regs (f result) = Nat.log 2 (x.regs (f arg)) ∧ y.mem = x.mem ∧
+      y.regs (f one) = 1 ∧ y.regs (f two) = 2 := by
+  obtain ⟨a, ha, hr, hm, ho, ht⟩ := exec (x.comap f) h2 hn hout
+  refine ⟨a.extend f x, ha.rename hf, ?_, hm, ?_, ?_⟩
+  · exact (hf.extend_apply _ _ result).trans hr
+  · exact (hf.extend_apply _ _ one).trans ho
+  · exact (hf.extend_apply _ _ two).trans ht
+
+end Cslib.Algorithms.WordRAM.NatLog