diff --git a/Complexity.lean b/Complexity.lean index 7e19236855..68af37ea5b 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -325,6 +325,30 @@ public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandR public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandSplit public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandTables public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandThin +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Bounds +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.CatalogueLoop +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.CatalogueState +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.CatalogueWrite +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Children +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Constructor +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.DigitScan +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Digits +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Flat +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Geometry +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Index +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Initialize +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Input +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.InputLayout +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Lookup +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.LookupDigits +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.LookupLoop +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.LookupStep +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Program +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Tile +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.TileChildren +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.TileKernels +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Values public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Bounds public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Core @@ -3489,6 +3513,7 @@ public import Complexity.Foundations.Data.Finset.Finpartition public import Complexity.Foundations.Data.Finset.KthLargest public import Complexity.Foundations.Data.Finset.KthLargest.Truncation public import Complexity.Foundations.Data.Finset.Lowest +public import Complexity.Foundations.Data.Finset.LowestMax public import Complexity.Foundations.Data.Finset.Markov public import Complexity.Foundations.Data.Finset.OrderGlue public import Complexity.Foundations.Data.Finset.OrderedFilter @@ -3582,6 +3607,7 @@ public import Complexity.Foundations.Data.Nat.Prime public import Complexity.Foundations.Data.Nat.Primrec public import Complexity.Foundations.Data.Nat.Radix public import Complexity.Foundations.Data.Nat.Radix.Measurement +public import Complexity.Foundations.Data.Nat.RadixUpdate public import Complexity.Foundations.Data.Nat.RecursionTree public import Complexity.Foundations.Data.Nat.ResidueSum public import Complexity.Foundations.Data.Nat.SqrtLog diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable.lean new file mode 100644 index 0000000000..d406108c2a --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable.lean @@ -0,0 +1,46 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Constructor +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Flat + +/-! +# Native shared geometry and compact signed box tables + +The existing finite boxes are now computed as a shared native directory and compact +catalogue. Each tile fills one value per actual box from the two canonical signed +leaf arrays, and lookup reads the actual stored signed word for a valid raw cube. +The caller routines permit dirty scratch and preserve the original arrays and outside memory. + +## Main definitions + +* `BoxTable.geometry`: compute the shared directory and descriptor catalogue once. +* `BoxTable.tile`: reuse that geometry to fill one compact value table. +* `BoxTable.lookup`: read a valid raw cube's actual stored value. +* `BoxTable.program`: complete initialized-input constructor with a fixed 64-register bank. + +## Main results + +* `BoxTable.runs_wide`: original-input admission, actual initialized prefix and charged halt, + with the same final witness for the computed ranks, values and frame. +* `BoxTable.exec_lookup`: actual valid-box lookup, within `18*L+32` native instructions. +* `BoxTable.geometryTime_le`: shared geometry within `64*(L+1)^2*10^L` when `m ≤ L`. +* `BoxTable.tileTime_le`: per-tile work bounded using the existing finite box-count law. + +## References + +The finite boxes and recurrence are adapted from [AlmanWilliams2026, Section 4.2]. +The shared directory and compact native representation are original alternatives to the +per-tile trie in the primary formal source at +[anthropics/formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5](https://github.com/anthropics/formal-math/tree/16a5ce41304fcdaea4e0be7c132e1c361dc26da5/3sum-apsp/ThreeSumApsp/Programs/Sec4/Theorem30). +Both use the existing tensor terms and signed leaf-product sum, but the memory layout, +digit order and charged costs differ. Shared setup and retained tile storage remain explicit; +no global all-tile amortization, wanted-query program, Corollary 26 or tuned 1.9992 bound +is claimed. +-/ diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Bounds.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Bounds.lean new file mode 100644 index 0000000000..8fe5aededd --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Bounds.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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.InputLayout +import Mathlib.Data.Nat.Log + +/-! +# Original-input bounds for native compact box tables + +The actual shared geometry and one tile have separate charged terms. A positive +logarithmic width threshold follows from the original depth, scalar headers, and +leaf magnitude envelopes. Neither the program nor its input reads a width certificate. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- Shared scalar/directory/descriptor setup; this cost is paid once across tiles. -/ +@[expose] def geometryTime (L m t : ℕ) : ℕ := + 4 * L + 20 + (11 * L + 28) * ((m - t + 1) * 10 ^ L) + +/-- One compact value-table construction, with dirty-memory-safe scalar setup. -/ +@[expose] def tileTime (L m t : ℕ) : ℕ := 328 * (boxes L m t).card + 8 + +/-- Original input adaptation, shared setup, one tile, and the final halt are charged. -/ +@[expose] def timeBound (L m t : ℕ) : ℕ := 4 * L + 19 + geometryTime L m t + tileTime L m t + 1 + +/-- The physical width threshold uses only original scalar and magnitude parameters. -/ +@[expose] def admissionWidth (L m t A B : ℕ) : ℕ := + Nat.clog 2 (magnitudeBound L A B + addressBound L m t + 1) + 3 + +/-- Width admission remains positive at zero depth and zero operands. -/ +theorem admissionWidth_pos (L m t A B : ℕ) : 0 < admissionWidth L m t A B := by + unfold admissionWidth + omega + +/-- The same original-input threshold derives unsigned addresses and signed operand bounds. -/ +theorem admission_bounds {W L m t A B : ℕ} (hW : admissionWidth L m t A B ≤ W) : + 0 < W - 2 ∧ Fits W (addressBound L m t) ∧ + GenericRAM.Signed.Fits (W - 2) (magnitudeBound L A B : ℕ) := by + have hlog := Nat.le_pow_clog (by decide : 1 < (2 : ℕ)) + (magnitudeBound L A B + addressBound L m t + 1) + have hs : Nat.clog 2 (magnitudeBound L A B + addressBound L m t + 1) ≤ (W - 2) - 1 := by + unfold admissionWidth at hW + omega + have hp := Nat.pow_le_pow_right (by decide : 1 ≤ (2 : ℕ)) hs + have hmag : magnitudeBound L A B < 2 ^ ((W - 2) - 1) := by omega + have hw : 0 < W - 2 := by unfold admissionWidth at hW; omega + refine ⟨hw, ?_, hw, ?_, ?_⟩ + · change addressBound L m t < 2 ^ W + have hp' := Nat.pow_le_pow_right (by decide : 1 ≤ (2 : ℕ)) (by omega : + Nat.clog 2 (magnitudeBound L A B + addressBound L m t + 1) ≤ W) + omega + · have hnonneg : 0 ≤ (magnitudeBound L A B : ℤ) := Int.natCast_nonneg _ + have hpow : 0 ≤ (2 : ℤ) ^ ((W - 2) - 1) := by positivity + omega + · exact_mod_cast hmag + +/-- The existing finite cardinality law controls the per-tile memoization cost. -/ +theorem tileTime_le (L m t : ℕ) (hm : m ≤ L) (ht : t ≤ m) : + tileTime L m t ≤ 328 * (m + 1) * ∑ d ∈ Finset.Icc t m, beta L m d + 8 := by + have hb := card_boxes_le L m t hm ht + unfold tileTime + nlinarith only [hb] + +/-- Under the usual depth bound, shared geometry is polynomial-depth times the existing +encoding-array length. This setup is independent of the number of tiles. -/ +theorem geometryTime_le (L m t : ℕ) (hm : m ≤ L) : + geometryTime L m t ≤ 64 * (L + 1) ^ 2 * 10 ^ L := by + have hp : 1 ≤ 10 ^ L := Nat.one_le_pow L _ (by decide) + have hh : m - t + 1 ≤ L + 1 := by omega + have hs := Nat.mul_le_mul_right (10 ^ L) hh + have hc := Nat.mul_le_mul_left (11 * L + 28) hs + have hsmall : 4 * L + 20 ≤ (4 * L + 20) * 10 ^ L := by + simpa only [Nat.mul_one] using Nat.mul_le_mul_left (4 * L + 20) hp + calc + geometryTime L m t ≤ (4 * L + 20) * 10 ^ L + + (11 * L + 28) * ((L + 1) * 10 ^ L) := Nat.add_le_add hsmall hc + _ = (4 * L + 20 + (11 * L + 28) * (L + 1)) * 10 ^ L := by ring + _ ≤ 64 * (L + 1) ^ 2 * 10 ^ L := Nat.mul_le_mul_right _ (by nlinarith) + +/-- The directory and descriptors are shared; a retained tile adds exactly one word per box. -/ +theorem allocation_le (L m t : ℕ) : + memoryEnd L m t - directoryBase L ≤ 5 * ((m - t + 1) * 10 ^ L) := by + have hk := Nat.count_le (Eligible L (m - t)) (n := (m - t + 1) * 10 ^ L) + rw [count_eligible_eq_card_boxes] at hk + unfold memoryEnd valueBase recordBase + omega + +/-- A fixed constructor bank and constant flat code bound, including its final halt. -/ +theorem program_size_le : program.size + 1 ≤ 1024 := by decide + +/-- Lookup uses the same fixed bank and bounded code, independently of the depth. -/ +theorem lookup_size_le : lookup.size + 1 ≤ 256 := by decide + +/-- Construction never inspects the physical width. -/ +theorem not_readsWidth : ¬program.ReadsWidth := by decide + +/-- Lookup never inspects the physical width. -/ +theorem lookup_not_readsWidth : ¬lookup.ReadsWidth := by decide + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/CatalogueLoop.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/CatalogueLoop.lean new file mode 100644 index 0000000000..2579c1cee2 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/CatalogueLoop.lean @@ -0,0 +1,153 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.CatalogueWrite + +/-! +# Complete native shared-catalogue scan + +The actual outer loop visits every directory slot once. Its digit scans and all +directory/record stores are charged; the compact count is Mathlib's count of the +computed eligibility predicate. Dirty memory outside the written prefixes survives. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Cslib.WordRAM + +/-- Persistent scalar contents used by the native catalogue loop, with no run or cost fields. -/ +structure CatalogueParameters (L H D R : ℕ) (x : Data registers) : Prop where + /-- Original depth. -/ + levels : x.regs Reg.levels = L + /-- Computed P0/star limit. -/ + height : x.regs Reg.height = H + /-- Computed decimal capacity. -/ + span : x.regs Reg.span = 10 ^ L + /-- Caller directory base. -/ + directory : x.regs Reg.directory = D + /-- Computed compact-record base. -/ + records : x.regs Reg.records = R + /-- Computed complete slot count. -/ + slots : x.regs Reg.slots = (H + 1) * 10 ^ L + /-- Scalar one. -/ + one : x.regs Reg.one = 1 + /-- Scalar radix. -/ + ten : x.regs Reg.ten = 10 + /-- Scalar P0 digit. -/ + nine : x.regs Reg.nine = 9 + /-- Scalar record width. -/ + three : x.regs Reg.three = 3 + /-- Scalar zero outside signed arithmetic. -/ + nil : x.regs Reg.nil = 0 + +private def parameterRegisters : Finset (Fin registers) := + {Reg.levels, Reg.height, Reg.span, Reg.directory, Reg.records, Reg.slots, + Reg.one, Reg.ten, Reg.nine, Reg.three, Reg.nil} + +private theorem CatalogueParameters.of_eq {L H D R : ℕ} {x y : Data registers} + (hx : CatalogueParameters L H D R x) + (h : ∀ i ∈ parameterRegisters, y.regs i = x.regs i) : + CatalogueParameters L H D R y := + ⟨(h _ (by decide)).trans hx.levels, (h _ (by decide)).trans hx.height, + (h _ (by decide)).trans hx.span, (h _ (by decide)).trans hx.directory, + (h _ (by decide)).trans hx.records, (h _ (by decide)).trans hx.slots, + (h _ (by decide)).trans hx.one, (h _ (by decide)).trans hx.ten, + (h _ (by decide)).trans hx.nine, (h _ (by decide)).trans hx.three, + (h _ (by decide)).trans hx.nil⟩ + +/-- Scalar registers changed by a complete catalogue iteration. -/ +@[expose] def CatalogueLocal (i : Fin registers) : Prop := InspectLocal i ∨ WriteLocal i + +instance (i : Fin registers) : Decidable (CatalogueLocal i) := + inferInstanceAs (Decidable (InspectLocal i ∨ WriteLocal i)) + +private theorem catalogueStep_preserves (i : Fin registers) : + ¬CatalogueLocal i → catalogueStep.Preserves i := by decide +revert + +private theorem parameter_not_local : + ∀ i ∈ parameterRegisters, ¬CatalogueLocal i := by decide + +/-- Compose the complete native digit scan with the real compact stores. -/ +theorem exec_catalogueStep {w L H D R s : ℕ} (x : Data registers) + (hx : CatalogueParameters L H D R x) (hs : x.regs Reg.slot = s) + (hc : x.regs Reg.count = Nat.count (Eligible L H) s) + (hslt : s < (H + 1) * 10 ^ L) + (hfit : Fits w (D + R + 6 * ((H + 1) * 10 ^ L) + 10 ^ L + L + 12)) : + ∃ y, ExecWithin w catalogueStep x y (11 * L + 26) ∧ + y.mem = catalogueWrite L H D R s x.mem ∧ y.regs Reg.slot = s + 1 ∧ + y.regs Reg.count = Nat.count (Eligible L H) (s + 1) ∧ + CatalogueParameters L H D R y ∧ + (∀ i, ¬CatalogueLocal i → y.regs i = x.regs i) := by + have hscan : Fits w (s + 10 ^ L + L + 12) := hfit.of_le (by omega) + have hwrite : Fits w (D + R + 6 * (s + 1) + 12) := hfit.of_le + (Nat.add_le_add_right ((Nat.add_le_add_left + (Nat.mul_le_mul_left 6 (Nat.succ_le_of_lt hslt)) (D + R)).trans + ((Nat.le_add_right _ (10 ^ L)).trans (Nat.le_add_right _ L))) 12) + obtain ⟨u, hu, he, hcode, hpop, hstride, hmem, hframe⟩ := + exec_inspect x hx.levels hx.span hs hx.one hx.ten hx.nine hscan + have hf (i : Fin registers) (hi : ¬InspectLocal i) : u.regs i = x.regs i := hframe i hi + obtain ⟨y, hy, hym, hys, hyc, _⟩ := exec_writeSlot u + ((hf _ (by decide)).trans hx.directory) ((hf _ (by decide)).trans hx.records) + ((hf _ (by decide)).trans hs) ((hf _ (by decide)).trans hx.height) + ((hf _ (by decide)).trans hc) hcode he hpop hstride + ((hf _ (by decide)).trans hx.one) ((hf _ (by decide)).trans hx.three) + ((hf _ (by decide)).trans hx.nil) hwrite + have hwhole : ExecWithin w catalogueStep x y (11 * L + 26) := + (hu.seq hy).mono (by omega) + have hregs (i : Fin registers) (hi : ¬CatalogueLocal i) : y.regs i = x.regs i := + hwhole.regs_eq (catalogueStep_preserves i hi) + refine ⟨y, hwhole, ?_, hys, hyc, hx.of_eq (fun i hi => + hregs i (parameter_not_local i hi)), hregs⟩ + simpa only [hmem] using hym + +/-- The actual scan fills every directory word and emits every eligible compact record once. -/ +theorem exec_catalogueLoop {w L H D R : ℕ} (x : Data registers) + (hx : CatalogueParameters L H D R x) + (hslot : x.regs Reg.slot = 0) (hcount : x.regs Reg.count = 0) + (hsep : D + (H + 1) * 10 ^ L ≤ R) + (hfit : Fits w (D + R + 6 * ((H + 1) * 10 ^ L) + 10 ^ L + L + 12)) : + ∃ y, ExecWithin w (.loop (.lt Reg.slot Reg.slots) catalogueStep) x y + ((11 * L + 28) * ((H + 1) * 10 ^ L) + 2) ∧ + CatalogueParameters L H D R y ∧ y.regs Reg.slot = (H + 1) * 10 ^ L ∧ + y.regs Reg.count = Nat.count (Eligible L H) ((H + 1) * 10 ^ L) ∧ + CataloguePrefix L H D R ((H + 1) * 10 ^ L) x.mem y.mem := by + let S := (H + 1) * 10 ^ L + let I (y : Data registers) : Prop := + CatalogueParameters L H D R y ∧ y.regs Reg.slot ≤ S ∧ + y.regs Reg.count = Nat.count (Eligible L H) (y.regs Reg.slot) ∧ + CataloguePrefix L H D R (y.regs Reg.slot) x.mem y.mem + have hi : I x := by + refine ⟨hx, by simp [hslot, S], by simp [hslot, hcount], ?_⟩ + simpa only [hslot] using CataloguePrefix.zero L H D R x.mem + have hb (y : Data registers) (hy : I y) (hg : (Cond.lt Reg.slot Reg.slots).Holds y) : + ∃ z, ExecWithin w catalogueStep y z (11 * L + 26) ∧ I z ∧ + S - z.regs Reg.slot < S - y.regs Reg.slot := by + obtain ⟨hp, hle, hc, hprefix⟩ := hy + have hlt : y.regs Reg.slot < S := by + simpa only [Cond.holds_lt, hp.slots, S] using hg + obtain ⟨z, hz, hzm, hzs, hzc, hzp, _⟩ := + exec_catalogueStep y hp rfl hc hlt hfit + refine ⟨z, hz, ⟨hzp, by omega, ?_, ?_⟩, by omega⟩ + · simpa only [hzs] using hzc + · rw [hzs, hzm] + exact hprefix.step hlt hsep + obtain ⟨y, hy, hIy, hstop⟩ := ExecWithin.loop_invariant I + (fun y => S - y.regs Reg.slot) hb hi + obtain ⟨hp, hle, hc, hprefix⟩ := hIy + have hdone : y.regs Reg.slot = S := by + simp only [Cond.holds_lt, hp.slots, not_lt] at hstop + exact Nat.le_antisymm hle hstop + refine ⟨y, ?_, hp, hdone, ?_, ?_⟩ + · simpa only [hslot, Nat.sub_zero, S, Nat.mul_comm, Nat.add_assoc] using hy + · simpa only [hdone] using hc + · simpa only [hdone] using hprefix + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/CatalogueState.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/CatalogueState.lean new file mode 100644 index 0000000000..096e571bdc --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/CatalogueState.lean @@ -0,0 +1,161 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Digits + +/-! +# Readback invariants for computed box geometry + +Every slot is assigned its actual prefix-count rank plus one, or zero when invalid. +Valid slots also append their three scalar descriptors. These are memory predicates +and descriptions of actual stores, not execution or time certificates. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +/-- A slot denotes a canonical box when its star count fits its completion's P0 population. -/ +@[expose] def Eligible (L H s : ℕ) : Prop := + s / 10 ^ L ≤ population (s % 10 ^ L) L ∧ population (s % 10 ^ L) L ≤ H + +instance (L H s : ℕ) : Decidable (Eligible L H s) := + inferInstanceAs (Decidable (s / 10 ^ L ≤ population (s % 10 ^ L) L ∧ + population (s % 10 ^ L) L ≤ H)) + +/-- Offset-one compact index, leaving zero for invalid slots. -/ +@[expose] def directoryWord (L H s : ℕ) : ℕ := + if Eligible L H s then Nat.count (Eligible L H) s + 1 else 0 + +/-- The completed leaf code stored in a compact record. -/ +@[expose] def recordCode (L s : ℕ) : ℕ := s % 10 ^ L + +/-- The exact star count stored in a compact record. -/ +@[expose] def recordStars (L s : ℕ) : ℕ := s / 10 ^ L + +/-- The place value used by actual ten-child native lookups. -/ +@[expose] def recordStride (L s : ℕ) : ℕ := + starStride (recordCode L s) (recordStars L s) L + +/-- The four stores made for a valid slot, or the one zero store for an invalid slot. -/ +@[expose] def catalogueWrite (L H D R s : ℕ) (μ : ℕ → ℕ) : ℕ → ℕ := + let ν := Function.update μ (D + s) (directoryWord L H s) + if Eligible L H s then + let p := R + 3 * Nat.count (Eligible L H) s + Function.update (Function.update (Function.update ν p (recordCode L s)) + (p + 1) (recordStars L s)) (p + 2) (recordStride L s) + else ν + +/-- Readback of every completed slot and compact record, with the exact written-prefix frame. -/ +structure CataloguePrefix (L H D R s : ℕ) (initial current : ℕ → ℕ) : Prop where + /-- All visited directory slots have been assigned, even when invalid. -/ + directory : ∀ i < s, current (D + i) = directoryWord L H i + /-- Every emitted record contains the original completed leaf index. -/ + code : ∀ i < s, Eligible L H i → + current (R + 3 * Nat.count (Eligible L H) i) = recordCode L i + /-- Every emitted record contains its exact star count. -/ + stars : ∀ i < s, Eligible L H i → + current (R + 3 * Nat.count (Eligible L H) i + 1) = recordStars L i + /-- Every emitted record contains the computed highest-star place value. -/ + stride : ∀ i < s, Eligible L H i → + current (R + 3 * Nat.count (Eligible L H) i + 2) = recordStride L i + /-- No word outside the actually written prefixes has changed. -/ + frame : ∀ a, ¬(D ≤ a ∧ a < D + s) → + ¬(R ≤ a ∧ a < R + 3 * Nat.count (Eligible L H) s) → current a = initial a + +/-- No initial zero-memory premise is needed at the empty prefix. -/ +theorem CataloguePrefix.zero (L H D R : ℕ) (μ : ℕ → ℕ) : + CataloguePrefix L H D R 0 μ μ := by + constructor <;> simp + +/-- The actual slot and descriptor writes extend the readback invariant by one slot. -/ +theorem CataloguePrefix.step {L H D R s : ℕ} {μ ν : ℕ → ℕ} + (h : CataloguePrefix L H D R s μ ν) + (hs : s < (H + 1) * 10 ^ L) (hsep : D + (H + 1) * 10 ^ L ≤ R) : + CataloguePrefix L H D R (s + 1) μ (catalogueWrite L H D R s ν) := by + have hcount : Nat.count (Eligible L H) s ≤ s := Nat.count_le _ + have hold (i : ℕ) (hi : i < s) (hp : Eligible L H i) : + Nat.count (Eligible L H) i < Nat.count (Eligible L H) s := + Nat.count_strict_mono hp hi + by_cases hv : Eligible L H s + · have hn := Nat.count_succ_eq_succ_count hv + constructor + · intro i hi + by_cases his : i = s + · subst i + simp [catalogueWrite, hv, Function.update_of_ne (by omega : D + s ≠ + R + 3 * Nat.count (Eligible L H) s), + Function.update_of_ne (by omega : D + s ≠ R + 3 * Nat.count (Eligible L H) s + 1), + Function.update_of_ne (by omega : D + s ≠ R + 3 * Nat.count (Eligible L H) s + 2)] + · have hiold : i < s := by omega + simp only [catalogueWrite, hv, ↓reduceIte] + rw [Function.update_of_ne (by omega), Function.update_of_ne (by omega), + Function.update_of_ne (by omega), Function.update_of_ne (by omega)] + exact h.directory i hiold + · intro i hi hp + by_cases his : i = s + · subst i + simp [catalogueWrite, hv] + · have hr := hold i (by omega) hp + simp only [catalogueWrite, hv, ↓reduceIte] + rw [Function.update_of_ne (by omega), Function.update_of_ne (by omega), + Function.update_of_ne (by omega), Function.update_of_ne (by omega)] + exact h.code i (by omega) hp + · intro i hi hp + by_cases his : i = s + · subst i + simp [catalogueWrite, hv] + · have hr := hold i (by omega) hp + simp only [catalogueWrite, hv, ↓reduceIte] + rw [Function.update_of_ne (by omega), Function.update_of_ne (by omega), + Function.update_of_ne (by omega), Function.update_of_ne (by omega)] + exact h.stars i (by omega) hp + · intro i hi hp + by_cases his : i = s + · subst i + simp [catalogueWrite, hv] + · have hr := hold i (by omega) hp + simp only [catalogueWrite, hv, ↓reduceIte] + rw [Function.update_of_ne (by omega), Function.update_of_ne (by omega), + Function.update_of_ne (by omega), Function.update_of_ne (by omega)] + exact h.stride i (by omega) hp + · intro a hd hr + simp only [hn] at hr + simp only [catalogueWrite, hv, ↓reduceIte] + rw [Function.update_of_ne (by omega), Function.update_of_ne (by omega), + Function.update_of_ne (by omega), Function.update_of_ne (by omega)] + exact h.frame a (by omega) (by omega) + · have hn := Nat.count_succ_eq_count hv + constructor + · intro i hi + by_cases his : i = s + · subst i + simp [catalogueWrite, hv] + · rw [catalogueWrite, ite_eq_right hv, Function.update_of_ne (by omega)] + exact h.directory i (by omega) + · intro i hi hp + have hne : i ≠ s := fun heq => hv (heq ▸ hp) + have hiold : i < s := by omega + rw [catalogueWrite, ite_eq_right hv, Function.update_of_ne (by omega)] + exact h.code i hiold hp + · intro i hi hp + have hne : i ≠ s := fun heq => hv (heq ▸ hp) + have hiold : i < s := by omega + rw [catalogueWrite, ite_eq_right hv, Function.update_of_ne (by omega)] + exact h.stars i hiold hp + · intro i hi hp + have hne : i ≠ s := fun heq => hv (heq ▸ hp) + have hiold : i < s := by omega + rw [catalogueWrite, ite_eq_right hv, Function.update_of_ne (by omega)] + exact h.stride i hiold hp + · intro a hd hr + rw [catalogueWrite, ite_eq_right hv, Function.update_of_ne (by omega)] + exact h.frame a (by omega) (by simpa only [hn] using hr) + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/CatalogueWrite.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/CatalogueWrite.lean new file mode 100644 index 0000000000..a206f63544 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/CatalogueWrite.lean @@ -0,0 +1,105 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.DigitScan +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.CatalogueState + +/-! +# Charged native stores of box geometry + +Both rejected and accepted slots execute a real directory store. Accepted slots also +write their three descriptor words at the actual computed compact rank. No zeroed +directory or precomputed compact-rank certificate is used by the program. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Cslib.WordRAM + +/-- Scalar registers changed by the native stores and counter updates. -/ +@[expose] def WriteLocal (i : Fin registers) : Prop := + i = Reg.address ∨ i = Reg.temporary ∨ i = Reg.count ∨ i = Reg.slot + +instance (i : Fin registers) : Decidable (WriteLocal i) := + inferInstanceAs (Decidable (i = Reg.address ∨ i = Reg.temporary ∨ + i = Reg.count ∨ i = Reg.slot)) + +private theorem writeSlot_preserves (i : Fin registers) : + ¬WriteLocal i → writeSlot.Preserves i := by decide +revert + +/-- Execute the exact stores after the actual digit scan. -/ +theorem exec_writeSlot {w L H D R s : ℕ} (x : Data registers) + (hd : x.regs Reg.directory = D) (hr : x.regs Reg.records = R) + (hs : x.regs Reg.slot = s) (hh : x.regs Reg.height = H) + (hc : x.regs Reg.count = Nat.count (Eligible L H) s) + (hcode : x.regs Reg.completion = recordCode L s) + (he : x.regs Reg.stars = recordStars L s) + (hp : x.regs Reg.population = population (recordCode L s) L) + (hstride : x.regs Reg.starPower = recordStride L s) + (h1 : x.regs Reg.one = 1) (h3 : x.regs Reg.three = 3) (h0 : x.regs Reg.nil = 0) + (hfit : Fits w (D + R + 6 * (s + 1) + 12)) : + ∃ y, ExecWithin w writeSlot x y 17 ∧ + y.mem = catalogueWrite L H D R s x.mem ∧ y.regs Reg.slot = s + 1 ∧ + y.regs Reg.count = Nat.count (Eligible L H) (s + 1) ∧ + (∀ i, ¬WriteLocal i → y.regs i = x.regs i) := by + let r := Nat.count (Eligible L H) s + have hrc : r ≤ s := Nat.count_le _ + have hfds : Fits w (D + s) := hfit.of_le (by omega) + have hfr : Fits w (r + 1) := hfit.of_le (by omega) + have hf3r : Fits w (r * 3) := hfit.of_le (by omega) + have hfra : Fits w (R + r * 3) := hfit.of_le (by omega) + have hfra1 : Fits w (R + r * 3 + 1) := hfit.of_le (by omega) + have hfra2 : Fits w (R + r * 3 + 1 + 1) := hfit.of_le (by omega) + have hfs : Fits w (s + 1) := hfit.of_le (by omega) + let bad := (((x.set Reg.address (D + s)).write (D + s) 0).set + Reg.temporary (x.regs Reg.temporary)).set Reg.slot (s + 1) + let good := ((((((((((((x.set Reg.address (D + s)).write (D + s) 0).set + Reg.temporary (r + 1)).write (D + s) (r + 1)).set Reg.address (r * 3)).set + Reg.address (R + r * 3)).write (R + r * 3) (recordCode L s)).set + Reg.address (R + r * 3 + 1)).write (R + r * 3 + 1) (recordStars L s)).set + Reg.address (R + r * 3 + 1 + 1)).write (R + r * 3 + 1 + 1) (recordStride L s)).set + Reg.count (r + 1)).set Reg.slot (s + 1) + by_cases hlarge : H < population (recordCode L s) L + · have hv : ¬Eligible L H s := fun h => (Nat.not_lt_of_ge h.2) hlarge + have hy : ExecWithin w writeSlot x bad 17 := by + ram_eval [writeSlot, bad, hd, hr, hs, hh, hp, h1, h0, hlarge, hfds, hfs, + Reg.address, Reg.directory, Reg.records, Reg.slot, Reg.height, Reg.population, + Reg.temporary, Reg.one, Reg.nil, Fin.mk.injEq] + refine ⟨bad, hy, ?_, ?_, ?_, fun i hi => hy.regs_eq (writeSlot_preserves i hi)⟩ + · simp [bad, catalogueWrite, hv, directoryWord, Data.write, Data.set] + · simp [bad, Reg.slot] + · simpa [bad, Reg.count, Reg.slot, Reg.temporary, Reg.address, + Nat.count_succ_eq_count hv] using hc + · by_cases hsmall : population (recordCode L s) L < recordStars L s + · have hv : ¬Eligible L H s := fun h => (Nat.not_lt_of_ge h.1) hsmall + have hy : ExecWithin w writeSlot x bad 17 := by + ram_eval [writeSlot, bad, hd, hr, hs, hh, hp, he, h1, h0, + hlarge, hsmall, hfds, hfs, Reg.address, Reg.directory, Reg.records, Reg.slot, + Reg.height, Reg.population, Reg.stars, Reg.temporary, Reg.one, Reg.nil, Fin.mk.injEq] + refine ⟨bad, hy, ?_, ?_, ?_, fun i hi => hy.regs_eq (writeSlot_preserves i hi)⟩ + · simp [bad, catalogueWrite, hv, directoryWord, Data.write, Data.set] + · simp [bad, Reg.slot] + · simpa [bad, Reg.count, Reg.slot, Reg.temporary, Reg.address, + Nat.count_succ_eq_count hv] using hc + · have hv : Eligible L H s := ⟨Nat.le_of_not_lt hsmall, Nat.le_of_not_lt hlarge⟩ + have hy : ExecWithin w writeSlot x good 17 := by + ram_eval [writeSlot, emit, good, r, hd, hr, hs, hh, hc, hcode, he, hp, + hstride, h1, h3, h0, hlarge, hsmall, hfds, hfr, hf3r, hfra, hfra1, hfra2, hfs, + Reg.address, Reg.directory, Reg.records, Reg.slot, Reg.height, Reg.population, + Reg.stars, Reg.completion, Reg.starPower, Reg.temporary, Reg.count, + Reg.one, Reg.three, Reg.nil, Fin.mk.injEq] + refine ⟨good, hy, ?_, ?_, ?_, fun i hi => hy.regs_eq (writeSlot_preserves i hi)⟩ + · simp [good, catalogueWrite, hv, directoryWord, r, Data.write, Data.set, + Function.update_idem, Nat.mul_comm, Nat.add_assoc] + · simp [good, Reg.slot] + · simp [good, Reg.count, Reg.slot, r, Nat.count_succ_eq_succ_count hv] + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Children.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Children.lean new file mode 100644 index 0000000000..f8d9bcfd00 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Children.lean @@ -0,0 +1,170 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Index +import Complexity.Foundations.Data.Finset.LowestMax + +/-! +# Earlier native entries for a box's ten children + +The computed e-th P0 stride selects the highest star of the existing canonical box. +The actual subtraction and directory-slot arithmetic therefore identify its ten +replacement boxes, all strictly earlier in the e-major catalogue. These finite facts +justify native memoization without supplying a geometry or lookup oracle. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Finset Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- An eligible slot with a positive star count has a highest star. -/ +theorem slotCube_stars_nonempty {L H s : ℕ} (hv : Eligible L H s) + (he : 0 < recordStars L s) : (slotCube L s).starLevels.Nonempty := by + apply card_pos.mp + rw [slotCube_star_count hv] + exact he + +/-- The native child completion code obtained by replacing the selected P0 digit. -/ +@[expose] def childCode (L s : ℕ) (d : Fin 10) : ℕ := + recordCode L s - (9 - d.val) * recordStride L s + +/-- The actual child directory address before adding the directory base. -/ +@[expose] def childSlot (L s : ℕ) (d : Fin 10) : ℕ := + (recordStars L s - 1) * 10 ^ L + childCode L s d + +/-- The recorded place value is exactly that of the highest starred coordinate. -/ +theorem recordStride_eq_pow_highest {L H s : ℕ} (hv : Eligible L H s) + (he : 0 < recordStars L s) : + recordStride L s = 10 ^ ((slotCube L s).starLevels.max' + (slotCube_stars_nonempty hv he)).val := by + let τ := completionAt L s + let e := recordStars L s + have hpop : e ≤ (P0Levels τ).card := by + change recordStars L s ≤ (P0Levels (leafAt + ⟨recordCode L s, Nat.mod_lt _ (pow_pos (by decide) L)⟩)).card + rw [← population_eq_card_P0Levels] + exact hv.1 + have hne : (lowest e (P0Levels τ)).Nonempty := by + simpa only [slotCube, starLevels_starLowest] using slotCube_stars_nonempty hv he + let q := (lowest e (P0Levels τ)).max' hne + have hq : q ∈ P0Levels τ := lowest_subset _ _ (max'_mem _ hne) + have hd : digitAt (recordCode L s) q.val = 9 := + (leafAt_eq_P0_iff _ q).mp (mem_P0Levels.mp hq) + have hrank : population (recordCode L s) (q.val + 1) = e := by + rw [population_succ, hd, ite_eq_left rfl] + have hp := population_eq_card_P0Levels_filter + (⟨recordCode L s, Nat.mod_lt _ (pow_pos (by decide) L)⟩ : Fin (10 ^ L)) + (Nat.le_of_lt q.isLt) + have hc := card_filter_lt_max_lowest hpop hne + have hf : ((P0Levels τ).filter fun ℓ => ℓ.val < q.val) = + (P0Levels τ).filter fun ℓ => ℓ < q := by rfl + rw [hp] + change ((P0Levels τ).filter fun ℓ => ℓ.val < q.val).card + 1 = e + rw [hf] + exact hc + have hs := starStride_of_rank q.isLt hd hrank + change starStride (recordCode L s) (recordStars L s) L = _ + simpa only [slotCube, starLevels_starLowest] using hs + +/-- Completion of a replacement changes exactly that completed-leaf coordinate. -/ +theorem starsToP0_replace {L : ℕ} (π : Cube L) (q : Fin L) + (lam : Term) : (π.replace q lam).starsToP0 = Function.update π.starsToP0 q lam := by + funext ℓ + by_cases h : ℓ = q + · subst ℓ + simp [Cube.replace, Cube.starsToP0] + · simp [Cube.replace, Cube.starsToP0, Function.update_of_ne h] + +/-- Native child arithmetic computes the exact canonical key of the replacement box. -/ +theorem childSlot_eq_cubeSlot_replace {L H s : ℕ} (hv : Eligible L H s) + (he : 0 < recordStars L s) (d : Fin 10) : + childSlot L s d = cubeSlot ((slotCube L s).replace + ((slotCube L s).starLevels.max' (slotCube_stars_nonempty hv he)) + (Encoding.termDigits d)) := by + let π := slotCube L s + let q := π.starLevels.max' (slotCube_stars_nonempty hv he) + have hq : π q = .star := Cube.mem_starLevels.mp (max'_mem _ _) + have hτ : π.starsToP0 q = .P0 := by simp [Cube.starsToP0, hq] + have hc : π.starLevels.card = recordStars L s := slotCube_star_count hv + have hpow : recordStride L s = 10 ^ q.val := recordStride_eq_pow_highest hv he + have hchild : (π.replace q (Encoding.termDigits d)).starLevels.card = + recordStars L s - 1 := by + rw [Cube.starLevels_replace, card_erase_of_mem (max'_mem _ _), hc] + change childSlot L s d = cubeSlot (π.replace q (Encoding.termDigits d)) + rw [cubeSlot, hchild, starsToP0_replace, leafIndex_update_P0 _ _ _ hτ, + ← hpow] + simp only [π, starsToP0_slotCube, completionAt, leafIndex_leafAt, childSlot, childCode] + +/-- A child is a genuine finite box with exactly one fewer star. -/ +theorem replace_mem_boxesWithStars {L H s : ℕ} (hv : Eligible L H s) + (he : 0 < recordStars L s) (d : Fin 10) : + (slotCube L s).replace ((slotCube L s).starLevels.max' + (slotCube_stars_nonempty hv he)) (Encoding.termDigits d) ∈ + boxesWithStars L H 0 (recordStars L s - 1) := by + apply replace_highest_mem_boxesWithStars + refine mem_boxesWithStars.mpr ⟨?_, ?_⟩ + · exact slotCube_isBox (by simpa using hv) + · rw [slotCube_star_count hv] + omega + +/-- Child directory lookups always address valid emitted entries. -/ +theorem eligible_childSlot {L H s : ℕ} (hv : Eligible L H s) + (he : 0 < recordStars L s) (d : Fin 10) : Eligible L H (childSlot L s d) := by + rw [childSlot_eq_cubeSlot_replace hv he d] + simpa using eligible_cubeSlot (mem_boxesWithStars.mp (replace_mem_boxesWithStars hv he d)).1 + +/-- The directory decoder returns the exact replacement cube required by the finite recurrence. -/ +theorem slotCube_childSlot {L H s : ℕ} (hv : Eligible L H s) + (he : 0 < recordStars L s) (d : Fin 10) : + slotCube L (childSlot L s d) = (slotCube L s).replace + ((slotCube L s).starLevels.max' (slotCube_stars_nonempty hv he)) + (Encoding.termDigits d) := by + rw [childSlot_eq_cubeSlot_replace hv he d] + exact slotCube_cubeSlot (mem_boxesWithStars.mp (replace_mem_boxesWithStars hv he d)).1 + +/-- The native replacement code remains an actual original encoding-array index. -/ +theorem childCode_lt {L H s : ℕ} (hv : Eligible L H s) + (he : 0 < recordStars L s) (d : Fin 10) : childCode L s d < 10 ^ L := by + have hkey := childSlot_eq_cubeSlot_replace hv he d + have hc := (mem_boxesWithStars.mp (replace_mem_boxesWithStars hv he d)).2 + rw [childSlot, cubeSlot, hc] at hkey + have heq := Nat.add_left_cancel hkey + exact heq ▸ (Encoding.leafIndex _).isLt + +/-- Decreasing the exact star count puts every child before its parent in the raw catalogue. -/ +theorem childSlot_lt {L H s : ℕ} (hv : Eligible L H s) + (he : 0 < recordStars L s) (d : Fin 10) : childSlot L s d < s := by + calc + childSlot L s d < (recordStars L s - 1) * 10 ^ L + 10 ^ L := + Nat.add_lt_add_left (childCode_lt hv he d) _ + _ = recordStars L s * 10 ^ L := by + rw [← Nat.add_one_mul, Nat.sub_add_cancel he] + _ ≤ s := Nat.div_mul_le_self _ _ + +/-- Offset-one directory ranks point to values already written by the native e-major loop. -/ +theorem child_rank_lt {L H s : ℕ} (hv : Eligible L H s) + (he : 0 < recordStars L s) (d : Fin 10) : + Nat.count (Eligible L H) (childSlot L s d) < Nat.count (Eligible L H) s := + Nat.count_strict_mono (eligible_childSlot hv he d) (childSlot_lt hv he d) + +/-- The finite box-value recurrence reads precisely the ten earlier native child slots. -/ +theorem boxValue_eq_sum_childSlots {L H s : ℕ} (hv : Eligible L H s) + (he : 0 < recordStars L s) (encA encB : Leaf L → ℤ) : + boxValue encA encB (recordStars L s) (slotCube L s) = + ∑ d : Fin 10, boxValue encA encB (recordStars L s - 1) + (slotCube L (childSlot L s d)) := by + have heq : recordStars L s = (recordStars L s - 1) + 1 := by omega + conv_lhs => rw [heq] + rw [boxValue, dite_eq_left (slotCube_stars_nonempty hv he)] + rw [← Encoding.termDigits.sum_comp] + exact sum_congr rfl fun d _ => by rw [slotCube_childSlot hv he d] + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Constructor.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Constructor.lean new file mode 100644 index 0000000000..2ce076412c --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Constructor.lean @@ -0,0 +1,108 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Tile +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Bounds + +/-! +# Caller-safe shared geometry and compact value construction + +The actual geometry and tile code compose on arbitrary caller data. Both original leaf +arrays lie before the caller's directory pointer; they may otherwise overlap. Scratch +contents need not be zero. Directory ranks, catalogue cardinality and every signed table +word are computed from the original scalar parameters and input words, with a complete +outside-allocation frame. Shared setup and per-tile work remain separately charged. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- Complete actual caller construction, with no assumed catalogue or table geometry. -/ +theorem exec_constructor {w L m t D AA BB A B : ℕ} (x : Data registers) + (a b : Leaf L → ℤ) + (ha : ∀ τ, (a τ).natAbs ≤ A) (hb : ∀ τ, (b τ).natAbs ≤ B) + (hL : x.regs Reg.levels = L) (hm : x.regs Reg.inner = m) + (ht : x.regs Reg.threshold = t) (hD : x.regs Reg.directory = D) + (hAA : x.regs Reg.arrayA = AA) (hBB : x.regs Reg.arrayB = BB) + (hAD : AA + 10 ^ L ≤ D) (hBD : BB + 10 ^ L ≤ D) + (hleft : ∀ c : Fin (10 ^ L), x.mem (AA + c.val) = Signed.encode (a (leafAt c))) + (hright : ∀ c : Fin (10 ^ L), x.mem (BB + c.val) = Signed.encode (b (leafAt c))) + (haddr : Fits (w + 2) (100 * (D + AA + BB + L + m + t + + (m - t + 1) * 10 ^ L + 10))) + (hmag : GenericRAM.Signed.Fits w (A + B + 10 ^ L * (A * B) : ℕ)) : + ∃ y, ExecWithin (w + 2) (.seq geometry tile) x y + (geometryTime L m t + 328 * (boxes L m t).card + 8) ∧ + y.regs Reg.levels = L ∧ y.regs Reg.inner = m ∧ y.regs Reg.threshold = t ∧ + y.regs Reg.height = m - t ∧ y.regs Reg.span = 10 ^ L ∧ + y.regs Reg.directory = D ∧ + y.regs Reg.records = D + (m - t + 1) * 10 ^ L ∧ + y.regs Reg.values = D + (m - t + 1) * 10 ^ L + 3 * (boxes L m t).card ∧ + y.regs Reg.count = (boxes L m t).card ∧ + y.regs Reg.arrayA = AA ∧ y.regs Reg.arrayB = BB ∧ + (∀ s < (m - t + 1) * 10 ^ L, + y.mem (D + s) = directoryWord L (m - t) s) ∧ + (∀ s < (m - t + 1) * 10 ^ L, Eligible L (m - t) s → + y.mem (D + (m - t + 1) * 10 ^ L + 3 * (boxes L m t).card + + Nat.count (Eligible L (m - t)) s) = Signed.encode (slotValue a b s)) ∧ + (∀ q, ¬(D ≤ q ∧ q < D + (m - t + 1) * 10 ^ L + 4 * (boxes L m t).card) → + y.mem q = x.mem q) := by + let S := (m - t + 1) * 10 ^ L + let K := (boxes L m t).card + let V := D + S + 3 * K + have hK : K = Nat.count (Eligible L (m - t)) S := + (count_eligible_eq_card_boxes L m t).symm + have hKS : K ≤ S := hK ▸ Nat.count_le _ + have hTS : 10 ^ L ≤ S := Nat.le_mul_of_pos_left _ (by omega) + obtain ⟨v, hv, vp, vK, vV, vcat⟩ := exec_geometry x hL hm ht hD + (haddr.of_le (by dsimp only [S] at hTS; omega)) + have vA : v.regs Reg.arrayA = AA := + (hv.regs_eq (by decide : geometry.Preserves Reg.arrayA)).trans hAA + have vB : v.regs Reg.arrayB = BB := + (hv.regs_eq (by decide : geometry.Preserves Reg.arrayB)).trans hBB + have vV' : v.regs Reg.values = V := vV + have vleft (c : Fin (10 ^ L)) : v.mem (AA + c.val) = Signed.encode (a (leafAt c)) := by + rw [vcat.frame _ (by have := c.isLt; omega) (by have := c.isLt; omega)] + exact hleft c + have vright (c : Fin (10 ^ L)) : v.mem (BB + c.val) = Signed.encode (b (leafAt c)) := by + rw [vcat.frame _ (by have := c.isLt; omega) (by have := c.isLt; omega)] + exact hright c + obtain ⟨y, hy, yvalues, yframe, yregs⟩ := exec_tile v a b ha hb vp vV' vA vB + (vK.trans hK) vcat (Nat.le_refl _) (by rw [← hK]) + (by dsimp only [V]; omega) (by dsimp only [V]; omega) vleft vright + (haddr.of_le (by dsimp only [S, K] at hKS hTS; dsimp only [V, S, K]; omega)) hmag + have he : ExecWithin (w + 2) (.seq geometry tile) x y + (geometryTime L m t + 328 * K + 8) := by + exact (hv.seq hy).mono (by dsimp only [geometryTime]; rw [← hK]; omega) + refine ⟨y, he, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, yvalues, ?_⟩ + · exact (hy.regs_eq (by decide : tile.Preserves Reg.levels)).trans vp.levels + · exact (hy.regs_eq (by decide : tile.Preserves Reg.inner)).trans + ((hv.regs_eq (by decide : geometry.Preserves Reg.inner)).trans hm) + · exact (hy.regs_eq (by decide : tile.Preserves Reg.threshold)).trans + ((hv.regs_eq (by decide : geometry.Preserves Reg.threshold)).trans ht) + · exact (hy.regs_eq (by decide : tile.Preserves Reg.height)).trans vp.height + · exact (hy.regs_eq (by decide : tile.Preserves Reg.span)).trans vp.span + · exact (hy.regs_eq (by decide : tile.Preserves Reg.directory)).trans vp.directory + · exact (hy.regs_eq (by decide : tile.Preserves Reg.records)).trans vp.records + · exact (yregs _ (by decide)).trans vV' + · exact (yregs _ (by decide)).trans vK + · exact (yregs _ (by decide)).trans vA + · exact (yregs _ (by decide)).trans vB + · intro s hs + rw [yframe _ (by dsimp only [V, S]; omega)] + exact vcat.directory s hs + · intro q hq + change ¬(D ≤ q ∧ q < D + S + 4 * K) at hq + rw [yframe _ (by rw [← hK]; dsimp only [V]; omega)] + rw [vcat.frame _ (by change ¬(D ≤ q ∧ q < D + S); omega) + (by rw [← hK]; change ¬(D + S ≤ q ∧ q < D + S + 3 * K); omega)] + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/DigitScan.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/DigitScan.lean new file mode 100644 index 0000000000..cd0406269a --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/DigitScan.lean @@ -0,0 +1,222 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Program +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Digits + +/-! +# Execution of the box-geometry digit scan + +The native remainder/division loop counts P0 digits and records the place value of +the requested P0 occurrence. Every scalar fit follows from the original code, depth +and final power. The memory is preserved, including dirty caller scratch. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Cslib.WordRAM + +/-- Registers changed by a native digit step. -/ +@[expose] def DigitLocal (i : Fin registers) : Prop := + i = Reg.digit ∨ i = Reg.suffix ∨ i = Reg.population ∨ i = Reg.starPower ∨ + i = Reg.power ∨ i = Reg.level ∨ i = Reg.temporary + +instance (i : Fin registers) : Decidable (DigitLocal i) := + inferInstanceAs (Decidable (i = Reg.digit ∨ i = Reg.suffix ∨ i = Reg.population ∨ + i = Reg.starPower ∨ i = Reg.power ∨ i = Reg.level ∨ i = Reg.temporary)) + +private theorem countDigit_preserves (i : Fin registers) : + ¬DigitLocal i → countDigit.Preserves i := by decide +revert + +/-- One charged step of the real native scan, with its original-input-derived fits. -/ +theorem exec_countDigit {w L c e k : ℕ} (x : Data registers) (hk : k < L) + (h10 : x.regs Reg.ten = 10) (h9 : x.regs Reg.nine = 9) + (h1 : x.regs Reg.one = 1) (he : x.regs Reg.stars = e) + (hl : x.regs Reg.level = k) (hq : x.regs Reg.suffix = c / 10 ^ k) + (hp : x.regs Reg.population = population c k) + (hpow : x.regs Reg.power = 10 ^ k) + (hs : x.regs Reg.starPower = starStride c e k) + (hfit : Fits w (c + 10 ^ L + L + 12)) : + ∃ y, ExecWithin w countDigit x y 9 ∧ y.regs Reg.level = k + 1 ∧ + y.regs Reg.suffix = c / 10 ^ (k + 1) ∧ + y.regs Reg.population = population c (k + 1) ∧ + y.regs Reg.power = 10 ^ (k + 1) ∧ + y.regs Reg.starPower = starStride c e (k + 1) ∧ y.mem = x.mem ∧ + (∀ i, ¬DigitLocal i → y.regs i = x.regs i) := by + have hp0 := population_le c k + have hcBound : c ≤ c + 10 ^ L + L + 12 := + ((Nat.le_add_right c (10 ^ L)).trans (Nat.le_add_right _ L)).trans + (Nat.le_add_right _ 12) + have hLBound : L ≤ c + 10 ^ L + L + 12 := + (Nat.le_add_left L (c + 10 ^ L)).trans (Nat.le_add_right _ 12) + have hPBound : 10 ^ L ≤ c + 10 ^ L + L + 12 := + ((Nat.le_add_left (10 ^ L) c).trans (Nat.le_add_right _ L)).trans + (Nat.le_add_right _ 12) + have h12Bound : 12 ≤ c + 10 ^ L + L + 12 := Nat.le_add_left _ _ + have hfpop : Fits w (population c k + 1) := + hfit.of_le ((Nat.succ_le_of_lt (hp0.trans_lt hk)).trans hLBound) + have hfk : Fits w (k + 1) := hfit.of_le ((Nat.succ_le_of_lt hk).trans hLBound) + have hfd : Fits w (digitAt c k) := hfit.of_le + ((Nat.le_of_lt (Nat.mod_lt _ (by decide : 0 < 10))).trans + ((by decide : 10 ≤ 12).trans h12Bound)) + have hfq : Fits w (c / 10 ^ k / 10) := hfit.of_le + ((Nat.div_le_self _ _).trans ((Nat.div_le_self _ _).trans hcBound)) + have hpowle : 10 ^ (k + 1) ≤ 10 ^ L := + Nat.pow_le_pow_right (by decide) (Nat.succ_le_of_lt hk) + have hfpow : Fits w (10 ^ k * 10) := by + simpa only [pow_succ] using hfit.of_le (hpowle.trans hPBound) + have hpowq : c / 10 ^ k / 10 = c / 10 ^ (k + 1) := by + rw [Nat.div_div_eq_div_mul, pow_succ] + let base := (x.set Reg.digit (digitAt c k)).set Reg.suffix (c / 10 ^ k / 10) + let changed := if digitAt c k = 9 then + if population c k + 1 = e then + (base.set Reg.population (population c k + 1)).set Reg.starPower (10 ^ k) + else (base.set Reg.population (population c k + 1)).set Reg.temporary + (x.regs Reg.temporary) + else base.set Reg.temporary (x.regs Reg.temporary) + let y := (changed.set Reg.power (10 ^ k * 10)).set Reg.level (k + 1) + have hy : ExecWithin w countDigit x y 9 := by + dsimp only [digitAt] at hfd + by_cases hd : c / 10 ^ k % 10 = 9 <;> by_cases hm : population c k + 1 = e + all_goals + have hf9 : Fits w 9 := hfit.of_le ((by decide : 9 ≤ 12).trans h12Bound) + have hfn := hfpop + try rw [hm] at hfn + ram_eval [countDigit, y, changed, base, hd, hm, h10, h9, h1, he, hl, hq, hp, + hpow, hs, hfd, hfq, hfpop, hfn, hf9, hfpow, hfk, digitAt, + Reg.digit, Reg.suffix, Reg.population, Reg.starPower, Reg.power, Reg.level, + Reg.temporary, Reg.ten, Reg.nine, Reg.one, Reg.stars, Fin.mk.injEq] + refine ⟨y, hy, ?_, ?_, ?_, ?_, ?_, ?_, fun i hi => hy.regs_eq + (countDigit_preserves i hi)⟩ + all_goals + by_cases hd : digitAt c k = 9 <;> by_cases hm : population c k + 1 = e <;> + simp [y, changed, base, hd, hm, hp, hs, population_succ, starStride, + hpowq, pow_succ, Reg.level, Reg.power, Reg.population, Reg.suffix, + Reg.starPower, Reg.digit, Reg.temporary] + +/-- Registers changed by the scan, including its descriptor initialization. -/ +@[expose] def InspectLocal (i : Fin registers) : Prop := + DigitLocal i ∨ i = Reg.stars ∨ i = Reg.completion + +instance (i : Fin registers) : Decidable (InspectLocal i) := + inferInstanceAs (Decidable (DigitLocal i ∨ i = Reg.stars ∨ i = Reg.completion)) + +private theorem inspect_preserves (i : Fin registers) : + ¬InspectLocal i → inspect.Preserves i := by decide +revert + +/-- The complete digit loop computes the population and highest-star stride from a raw slot. -/ +theorem exec_inspect {w L s : ℕ} (x : Data registers) + (hL : x.regs Reg.levels = L) (hT : x.regs Reg.span = 10 ^ L) + (hslot : x.regs Reg.slot = s) (h1 : x.regs Reg.one = 1) + (h10 : x.regs Reg.ten = 10) (h9 : x.regs Reg.nine = 9) + (hfit : Fits w (s + 10 ^ L + L + 12)) : + ∃ y, ExecWithin w inspect x y (11 * L + 9) ∧ + y.regs Reg.stars = s / 10 ^ L ∧ y.regs Reg.completion = s % 10 ^ L ∧ + y.regs Reg.population = population (s % 10 ^ L) L ∧ + y.regs Reg.starPower = starStride (s % 10 ^ L) (s / 10 ^ L) L ∧ + y.mem = x.mem ∧ (∀ i, ¬InspectLocal i → y.regs i = x.regs i) := by + let e := s / 10 ^ L + let c := s % 10 ^ L + have hc : c ≤ s := Nat.mod_le _ _ + have he : e ≤ s := Nat.div_le_self _ _ + have hscalar : s ≤ s + 10 ^ L + L + 12 := + ((Nat.le_add_right _ _).trans (Nat.le_add_right _ _)).trans (Nat.le_add_right _ _) + have hfe : Fits w e := hfit.of_le (he.trans hscalar) + have hfc : Fits w c := hfit.of_le (hc.trans hscalar) + have hfitc : Fits w (c + 10 ^ L + L + 12) := hfit.of_le + (Nat.add_le_add_right (Nat.add_le_add_right (Nat.add_le_add_right hc _) _) _) + have hf1 : Fits w 1 := hfit.of_le ((by decide : 1 ≤ 12).trans (Nat.le_add_left _ _)) + let start := ((((((x.set Reg.stars e).set Reg.completion c).set Reg.suffix c).set + Reg.level 0).set Reg.population 0).set Reg.power 1).set Reg.starPower 0 + have hs : ExecWithin w (ram[ + Reg.stars ← Reg.slot / Reg.span; Reg.completion ← Reg.slot % Reg.span; + Reg.suffix ← Reg.completion; Reg.level ← #0; Reg.population ← #0; + Reg.power ← #1; Reg.starPower ← #0 ]) x start 7 := by + ram_eval [start, e, c, hslot, hT, hfe, hfc, hf1, + Reg.stars, Reg.slot, Reg.span, Reg.completion, Reg.suffix, Reg.level, + Reg.population, Reg.power, Reg.starPower, Fin.mk.injEq] + let I (y : Data registers) : Prop := + y.regs Reg.level ≤ L ∧ + y.regs Reg.suffix = c / 10 ^ y.regs Reg.level ∧ + y.regs Reg.population = population c (y.regs Reg.level) ∧ + y.regs Reg.power = 10 ^ y.regs Reg.level ∧ + y.regs Reg.starPower = starStride c e (y.regs Reg.level) ∧ + y.mem = x.mem ∧ (∀ i, ¬DigitLocal i → y.regs i = start.regs i) + have hi : I start := by + simp [I, start, Reg.level, Reg.starPower, Reg.power, Reg.population, Reg.suffix, + Reg.completion, Reg.stars, population_zero, starStride] + have hb (y : Data registers) (hy : I y) (hg : (Cond.lt Reg.level Reg.levels).Holds y) : + ∃ z, ExecWithin w countDigit y z 9 ∧ I z ∧ + L - z.regs Reg.level < L - y.regs Reg.level := by + obtain ⟨hle, hq, hp, hpow, hstar, hm, hframe⟩ := hy + have hlevels : y.regs Reg.levels = L := by + simpa [start, Reg.levels, Reg.stars, Reg.completion, Reg.suffix, Reg.level, + Reg.population, Reg.power, Reg.starPower] using + (hframe Reg.levels (by decide)).trans (by + simpa [start, Reg.levels, Reg.stars, Reg.completion, Reg.suffix, Reg.level, + Reg.population, Reg.power, Reg.starPower] using hL) + have hconst1 : y.regs Reg.one = 1 := by + simpa [start, Reg.one, Reg.stars, Reg.completion, Reg.suffix, Reg.level, + Reg.population, Reg.power, Reg.starPower] using + (hframe Reg.one (by decide)).trans (by + simpa [start, Reg.one, Reg.stars, Reg.completion, Reg.suffix, Reg.level, + Reg.population, Reg.power, Reg.starPower] using h1) + have hconst10 : y.regs Reg.ten = 10 := by + simpa [start, Reg.ten, Reg.stars, Reg.completion, Reg.suffix, Reg.level, + Reg.population, Reg.power, Reg.starPower] using + (hframe Reg.ten (by decide)).trans (by + simpa [start, Reg.ten, Reg.stars, Reg.completion, Reg.suffix, Reg.level, + Reg.population, Reg.power, Reg.starPower] using h10) + have hconst9 : y.regs Reg.nine = 9 := by + simpa [start, Reg.nine, Reg.stars, Reg.completion, Reg.suffix, Reg.level, + Reg.population, Reg.power, Reg.starPower] using + (hframe Reg.nine (by decide)).trans (by + simpa [start, Reg.nine, Reg.stars, Reg.completion, Reg.suffix, Reg.level, + Reg.population, Reg.power, Reg.starPower] using h9) + have hstars : y.regs Reg.stars = e := by + simpa [start, Reg.stars, Reg.completion, Reg.suffix, Reg.level, + Reg.population, Reg.power, Reg.starPower] using hframe Reg.stars (by decide) + have hk : y.regs Reg.level < L := by simpa only [Cond.holds_lt, hlevels] using hg + obtain ⟨z, hz, hzl, hzq, hzp, hzpow, hzs, hzm, hzf⟩ := + exec_countDigit y hk hconst10 hconst9 hconst1 hstars rfl hq hp hpow hstar hfitc + refine ⟨z, hz, ⟨by omega, ?_, ?_, ?_, ?_, hzm.trans hm, + fun i h => (hzf i h).trans (hframe i h)⟩, by omega⟩ + · simpa only [hzl] using hzq + · simpa only [hzl] using hzp + · simpa only [hzl] using hzpow + · simpa only [hzl] using hzs + obtain ⟨y, hloop, hy, hstop⟩ := ExecWithin.loop_invariant I + (fun y => L - y.regs Reg.level) hb hi + have hlevels : y.regs Reg.levels = L := by + simpa [start, Reg.levels, Reg.stars, Reg.completion, Reg.suffix, Reg.level, + Reg.population, Reg.power, Reg.starPower] using + (hy.2.2.2.2.2.2 Reg.levels (by decide)).trans (by + simpa [start, Reg.levels, Reg.stars, Reg.completion, Reg.suffix, Reg.level, + Reg.population, Reg.power, Reg.starPower] using hL) + have hdone : y.regs Reg.level = L := by + simp only [Cond.holds_lt, hlevels, not_lt] at hstop + exact Nat.le_antisymm hy.1 hstop + have hwhole : ExecWithin w inspect x y (11 * L + 9) := by + apply (hs.seq hloop).mono + simp only [start, Data.set_regs, Reg.level, Reg.population, Reg.power, Reg.starPower, + Function.update_apply, Fin.reduceEq, ↓reduceIte, Nat.sub_zero] + omega + refine ⟨y, hwhole, ?_, ?_, ?_, ?_, hy.2.2.2.2.2.1, + fun i hi => hwhole.regs_eq (inspect_preserves i hi)⟩ + · simpa [start, Reg.stars, Reg.completion, Reg.suffix, Reg.level, + Reg.population, Reg.power, Reg.starPower] using hy.2.2.2.2.2.2 Reg.stars (by decide) + · simpa [start, Reg.stars, Reg.completion, Reg.suffix, Reg.level, + Reg.population, Reg.power, Reg.starPower] using + hy.2.2.2.2.2.2 Reg.completion (by decide) + · simpa only [hdone] using hy.2.2.1 + · simpa only [hdone] using hy.2.2.2.2.1 + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Digits.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Digits.lean new file mode 100644 index 0000000000..36558af5a8 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Digits.lean @@ -0,0 +1,147 @@ +/- +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.Algorithms.MatrixMultiplication.Schonhage.BoxValues +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Meaning +public import Mathlib.Data.Nat.Count + +/-! +# Geometry digits for the shared native box table + +The flat leaf numbering is exactly the existing native encoder's numbering, with +level zero least significant and P0 digit nine. `population` and `starStride` describe +the scalar results of the native digit loop. Neither definition contains execution, +time, rank, layout or table hypotheses. + +The canonical boxes are those of [AlmanWilliams2026, Section 4.2], already adapted in +`BoxValues`. The shared dense directory and compact enumeration are a new native +representation; their one-time setup is distinct from the source's per-tile trie. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Finset Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- Decode a complete leaf using the existing native encoder's finite digit dictionary. -/ +@[expose] def leafAt {L : ℕ} (c : Fin (10 ^ L)) : Leaf L := + fun ℓ => Encoding.termDigits (finFunctionFinEquiv.symm c ℓ) + +/-- Decoding and re-encoding uses the same actual flat array position. -/ +@[simp] theorem leafIndex_leafAt {L : ℕ} (c : Fin (10 ^ L)) : + Encoding.leafIndex (leafAt c) = c := by + simp [Encoding.leafIndex, leafAt] + +/-- Decoding an existing leaf index recovers every original term. -/ +@[simp] theorem leafAt_leafIndex {L : ℕ} (τ : Leaf L) : + leafAt (Encoding.leafIndex τ) = τ := by + funext ℓ + simp [leafAt, Encoding.leafIndex] + +/-- The raw decimal digit at a level, in the existing least-significant-first layout. -/ +@[expose] def digitAt (c k : ℕ) : ℕ := c / 10 ^ k % 10 + +/-- Number of P0 digits in the first `k` levels. -/ +@[expose] def population (c k : ℕ) : ℕ := Nat.count (fun i => digitAt c i = 9) k + +/-- The e-th P0 place value found by the scan; zero until that occurrence has been found. -/ +@[expose] def starStride (c e : ℕ) : ℕ → ℕ + | 0 => 0 + | k + 1 => + if digitAt c k = 9 ∧ population c k + 1 = e then 10 ^ k else starStride c e k + +/-- A leaf uses P0 at a level precisely when the actual native digit is nine. -/ +theorem leafAt_eq_P0_iff {L : ℕ} (c : Fin (10 ^ L)) (ℓ : Fin L) : + leafAt c ℓ = .P0 ↔ digitAt c.val ℓ.val = 9 := by + have hd := finFunctionFinEquiv_symm_apply_val c ℓ + constructor + · intro h + have h' := congrArg Encoding.termDigits.symm h + simp only [leafAt, Equiv.symm_apply_apply] at h' + change (finFunctionFinEquiv.symm c ℓ) = 9 at h' + simp [digitAt, ← hd, h'] + · intro h + have h' : finFunctionFinEquiv.symm c ℓ = 9 := Fin.ext (hd.trans h) + simp [leafAt, h', Encoding.termDigits, Encoding.termAt] + +/-- The scan's population is the existing finite P0-coordinate cardinality. -/ +theorem population_eq_card_P0Levels {L : ℕ} (c : Fin (10 ^ L)) : + population c.val L = (P0Levels (leafAt c)).card := by + rw [population, Nat.count_eq_card_filter_range] + symm + refine card_bij (fun ℓ _ => ℓ.val) ?_ ?_ ?_ + · intro ℓ hℓ + exact mem_filter.mpr ⟨mem_range.mpr ℓ.isLt, + (leafAt_eq_P0_iff c ℓ).mp (mem_P0Levels.mp hℓ)⟩ + · intro ℓ _ ℓ' _ h + exact Fin.ext h + · intro k hk + obtain ⟨hkL, hkd⟩ := mem_filter.mp hk + exact ⟨⟨k, mem_range.mp hkL⟩, + mem_P0Levels.mpr ((leafAt_eq_P0_iff c _).mpr hkd), rfl⟩ + +/-- A prefix scan counts precisely the P0 coordinates below its native level. -/ +theorem population_eq_card_P0Levels_filter {L k : ℕ} (c : Fin (10 ^ L)) (hk : k ≤ L) : + population c.val k = ((P0Levels (leafAt c)).filter fun ℓ => ℓ.val < k).card := by + rw [population, Nat.count_eq_card_filter_range] + symm + refine card_bij (fun ℓ _ => ℓ.val) ?_ ?_ ?_ + · intro ℓ hℓ + obtain ⟨hp, hlt⟩ := mem_filter.mp hℓ + exact mem_filter.mpr ⟨mem_range.mpr hlt, + (leafAt_eq_P0_iff c ℓ).mp (mem_P0Levels.mp hp)⟩ + · intro ℓ _ ℓ' _ h + exact Fin.ext h + · intro i hi + obtain ⟨hilt, hid⟩ := mem_filter.mp hi + have hiL : i < L := (mem_range.mp hilt).trans_le hk + exact ⟨⟨i, hiL⟩, mem_filter.mpr + ⟨mem_P0Levels.mpr ((leafAt_eq_P0_iff c _).mpr hid), mem_range.mp hilt⟩, rfl⟩ + +/-- No scan prefix contains more P0 digits than scanned levels. -/ +theorem population_le (c k : ℕ) : population c k ≤ k := Nat.count_le _ + +@[simp] theorem population_zero (c : ℕ) : population c 0 = 0 := rfl + +/-- Extend the ordinary Mathlib count by the next native digit test. -/ +theorem population_succ (c k : ℕ) : + population c (k + 1) = population c k + if digitAt c k = 9 then 1 else 0 := by + simp [population, Nat.count_succ] + +/-- A recorded stride fits below the final power used by the scan. -/ +theorem starStride_le (c e k : ℕ) : starStride c e k ≤ 10 ^ k := by + induction k with + | zero => simp [starStride] + | succ k ih => + rw [starStride] + split + · exact Nat.pow_le_pow_right (by decide) (by omega) + · exact ih.trans (Nat.pow_le_pow_right (by decide) (by omega)) + +/-- Once the e-th P0 coordinate is reached, later digits preserve its exact place value. -/ +theorem starStride_of_rank {c e j k : ℕ} (hjk : j < k) + (hd : digitAt c j = 9) (hrank : population c (j + 1) = e) : + starStride c e k = 10 ^ j := by + induction k with + | zero => omega + | succ k ih => + by_cases hj : j = k + · subst j + rw [starStride] + have hr : population c k + 1 = e := by simpa [population_succ, hd] using hrank + simp [hd, hr] + · have hjk' : j < k := by omega + have hmono : e ≤ population c k := by + rw [← hrank] + exact Nat.count_monotone _ (by omega) + rw [starStride, ite_eq_right (by omega : ¬(digitAt c k = 9 ∧ population c k + 1 = e))] + exact ih hjk' + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Flat.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Flat.lean new file mode 100644 index 0000000000..f4b6aa4f07 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Flat.lean @@ -0,0 +1,71 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Input +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Lookup + +/-! +# Initialized flat box-table construction and actual lookup + +One fixed 64-register program computes the shared catalogue and a complete tile from +the original arrays. The exact pre-halt state is the same witness used for all table +readbacks and the charged final halt. Physical admission is an original-input logarithm. +The lookup theorem remains separately callable, so geometry is not rebuilt per query. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- The standard compiler gives a real initialized prefix and charged halt with the same data. -/ +theorem runs_wide {W L m t A B : ℕ} (a b : Fin (10 ^ L) → ℤ) + (ha : ∀ i, (a i).natAbs ≤ A) (hb : ∀ i, (b i).natAbs ≤ B) + (hW : admissionWidth L m t A B ≤ W) : + InputFits W (input L m t a b) ∧ + ∃ y n, n + 1 ≤ timeBound L m t ∧ + Runs W (program.program Reg.values) (State.init (input L m t a b)) + ⟨program.size, y⟩ n ∧ + Executes W (program.program Reg.values) (State.init (input L m t a b)) + (valueBase L m t) (n + 1) ∧ y.Bounded W ∧ + y.regs Reg.levels = L ∧ y.regs Reg.height = m - t ∧ + y.regs Reg.span = 10 ^ L ∧ y.regs Reg.directory = directoryBase L ∧ + y.regs Reg.values = valueBase L m t ∧ + y.regs Reg.count = (boxes L m t).card ∧ + (∀ s < (m - t + 1) * 10 ^ L, + y.mem (directoryBase L + s) = directoryWord L (m - t) s) ∧ + (∀ s < (m - t + 1) * 10 ^ L, Eligible L (m - t) s → + y.mem (valueBase L m t + Nat.count (Eligible L (m - t)) s) = + Signed.encode (slotValue (fun τ => a (Encoding.leafIndex τ)) + (fun τ => b (Encoding.leafIndex τ)) s)) ∧ + (∀ q, ¬(directoryBase L ≤ q ∧ q < memoryEnd L m t) → + y.mem q = (State.init (input L m t a b) : State registers).data.mem q) := by + obtain ⟨hw, haddr, hmag⟩ := admission_bounds hW + have hwidth : W - 2 + 2 = W := by unfold admissionWidth at hW; omega + obtain ⟨hi, y, ⟨n, hn, he⟩, hy, hL, hH, hT, hD, hV, hK, hd, hv, hf⟩ := + exec_input a b ha hb (by simpa only [hwidth] using haddr) hmag + refine ⟨by simpa only [hwidth] using hi, y, n, ?_, ?_, ?_, + by simpa only [hwidth] using hy, hL, hH, hT, hD, hV, hK, hd, hv, hf⟩ + · have ht : 0 < timeBound L m t := by unfold timeBound; omega + omega + · simpa only [hwidth, Nat.zero_add, State.init] using he.runs (pc := 0) + (p := program.program Reg.values) (Program.Contains.self _).append_left + · simpa only [hwidth, hV, State.init] using he.executes Reg.values + +/-- Every reachable initialized prefix has fitting native words under the same admission. -/ +theorem bounded_reachable {W L m t A B n : ℕ} (a b : Fin (10 ^ L) → ℤ) + (ha : ∀ i, (a i).natAbs ≤ A) (hb : ∀ i, (b i).natAbs ≤ B) + (hW : admissionWidth L m t A B ≤ W) {y : State registers} + (hy : Runs W (program.program Reg.values) (State.init (input L m t a b)) y n) : + y.data.Bounded W := by + have hi := (runs_wide a b ha hb hW).1 + exact hy.bounded_init hi + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Geometry.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Geometry.lean new file mode 100644 index 0000000000..2d604584e2 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Geometry.lean @@ -0,0 +1,177 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.CatalogueLoop +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Index + +/-! +# Complete shared native box geometry + +The actual program computes its power, directory extent, compact count and value-table +base from the original scalar parameters. It assigns every directory slot and writes +exactly the catalogue records counted by the existing finite box family. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Cslib.WordRAM + +private theorem powerRegisters_injective : Function.Injective powerRegisters := by decide + +/-- The existing power routine computes the actual native span with unchanged memory. -/ +theorem exec_span {w L : ℕ} (x : Data registers) + (hL : x.regs Reg.levels = L) (h10 : x.regs Reg.ten = 10) + (hfit : Fits w (10 ^ L + L + 2)) : + ∃ y, ExecWithin w (Power.program.rename powerRegisters) x y (4 * L + 5) ∧ + y.regs Reg.span = 10 ^ L ∧ y.regs Reg.one = 1 ∧ y.mem = x.mem ∧ + (∀ i, i ≠ Reg.span → i ≠ Reg.level → i ≠ Reg.one → y.regs i = x.regs i) := by + obtain ⟨z, hz, hv, _, ho, hm, _, _⟩ := + Power.exec 10 L (by decide) (x.comap powerRegisters) h10 hL hfit + have he := hz.rename powerRegisters_injective + refine ⟨z.extend powerRegisters x, he, ?_, ?_, hm, ?_⟩ + · have h := congrArg (fun d : Data 5 => d.regs Power.value) + (Data.comap_extend powerRegisters_injective z x) + exact h.trans hv + · have h := congrArg (fun d : Data 5 => d.regs Power.one) + (Data.comap_extend powerRegisters_injective z x) + exact h.trans ho + · intro i hv hc ho + apply he.regs_eq + simp [Power.program, Power.body, Code.rename, Code.Preserves, Op.rename, Op.dest, + Op.bin, powerRegisters, Power.value, Power.counter, Power.base, Power.exponent, + Power.one, Ne.symm hv, Ne.symm hc, Ne.symm ho] + +/-- Explicit scalar initialization, also valid when every old temporary is dirty. -/ +theorem exec_constants {w : ℕ} (x : Data registers) (hfit : Fits w 10) : + ∃ y, ExecWithin w constants x y 5 ∧ y.regs Reg.nil = 0 ∧ + y.regs Reg.one = 1 ∧ y.regs Reg.ten = 10 ∧ y.regs Reg.nine = 9 ∧ + y.regs Reg.three = 3 ∧ y.mem = x.mem ∧ + (∀ i, i ≠ Reg.nil → i ≠ Reg.one → i ≠ Reg.ten → i ≠ Reg.nine → + i ≠ Reg.three → y.regs i = x.regs i) := by + have h0 := hfit.of_le (by decide : 0 ≤ 10) + have h1 := hfit.of_le (by decide : 1 ≤ 10) + have h3 := hfit.of_le (by decide : 3 ≤ 10) + have h9 := hfit.of_le (by decide : 9 ≤ 10) + let y := ((((x.set Reg.nil 0).set Reg.one 1).set Reg.ten 10).set Reg.nine 9).set Reg.three 3 + have he : ExecWithin w constants x y 5 := by + ram_eval [constants, y, h0, h1, h3, h9, hfit, Reg.nil, Reg.one, Reg.ten, + Reg.nine, Reg.three, Fin.mk.injEq] + refine ⟨y, he, by simp [y, Reg.nil, Reg.one, Reg.ten, Reg.nine, Reg.three], + by simp [y, Reg.nil, Reg.one, Reg.ten, Reg.nine, Reg.three], + by simp [y, Reg.nil, Reg.one, Reg.ten, Reg.nine, Reg.three], + by simp [y, Reg.nil, Reg.one, Reg.ten, Reg.nine, Reg.three], + by simp [y, Reg.nil, Reg.one, Reg.ten, Reg.nine, Reg.three], rfl, ?_⟩ + intro i hi0 hi1 hi10 hi9 hi3 + exact he.regs_eq (by simp [constants, Code.Preserves, Op.dest, + Ne.symm hi0, Ne.symm hi1, Ne.symm hi10, Ne.symm hi9, Ne.symm hi3]) + +/-- Actual extent setup and its complete persistent parameter readback. -/ +theorem exec_geometrySetup {w L m t D : ℕ} (x : Data registers) + (hL : x.regs Reg.levels = L) (hm : x.regs Reg.inner = m) + (ht : x.regs Reg.threshold = t) (hD : x.regs Reg.directory = D) + (hT : x.regs Reg.span = 10 ^ L) (h1 : x.regs Reg.one = 1) + (h10 : x.regs Reg.ten = 10) (h9 : x.regs Reg.nine = 9) + (h3 : x.regs Reg.three = 3) (h0 : x.regs Reg.nil = 0) + (hfit : Fits w (D + (m - t + 1) * 10 ^ L + m + 12)) : + ∃ y, ExecWithin w geometrySetup x y 6 ∧ + CatalogueParameters L (m - t) D (D + (m - t + 1) * 10 ^ L) y ∧ + y.regs Reg.slot = 0 ∧ y.regs Reg.count = 0 ∧ y.mem = x.mem := by + let S := (m - t + 1) * 10 ^ L + have hp : 0 < 10 ^ L := by positivity + have hh : Fits w (m - t) := hfit.of_le (by omega) + have hh1 : Fits w (m - t + 1) := hfit.of_le (by omega) + have hS : Fits w S := hfit.of_le (by omega) + have hR : Fits w (D + S) := hfit.of_le (by omega) + have hf0 : Fits w 0 := hfit.of_le (Nat.zero_le _) + let a := ((x.set Reg.height (m - t)).set Reg.slots (m - t + 1)).set Reg.slots S + let y := ((a.set Reg.records (D + S)).set Reg.slot 0).set Reg.count 0 + have he : ExecWithin w geometrySetup x y 6 := by + ram_eval [geometrySetup, y, a, S, hm, ht, hD, hT, h1, hh, hh1, hS, hR, hf0, + Reg.height, Reg.slots, Reg.records, Reg.slot, Reg.count, Reg.inner, Reg.threshold, + Reg.directory, Reg.span, Reg.one, Fin.mk.injEq] + refine ⟨y, he, ?_, ?_, ?_, rfl⟩ + · constructor <;> simp [y, a, S, hL, hD, hT, h1, h10, h9, h3, h0, + Reg.height, Reg.slots, Reg.records, Reg.slot, Reg.count, Reg.levels, + Reg.directory, Reg.span, Reg.one, Reg.ten, Reg.nine, Reg.three, Reg.nil] + · simp [y, a, Reg.count, Reg.slot] + · simp [y, a] + +/-- Actual shared setup, including all digit scans and descriptor writes. -/ +theorem exec_geometry {w L m t D : ℕ} (x : Data registers) + (hL : x.regs Reg.levels = L) (hm : x.regs Reg.inner = m) + (ht : x.regs Reg.threshold = t) (hD : x.regs Reg.directory = D) + (hfit : Fits w (D + (D + (m - t + 1) * 10 ^ L) + + 6 * ((m - t + 1) * 10 ^ L) + 10 ^ L + L + m + 12)) : + ∃ y, ExecWithin w geometry x y + (4 * L + 20 + (11 * L + 28) * ((m - t + 1) * 10 ^ L)) ∧ + CatalogueParameters L (m - t) D (D + (m - t + 1) * 10 ^ L) y ∧ + y.regs Reg.count = (Cslib.Algorithms.MatrixMultiplication.Schonhage.boxes L m t).card ∧ + y.regs Reg.values = D + (m - t + 1) * 10 ^ L + + 3 * (Cslib.Algorithms.MatrixMultiplication.Schonhage.boxes L m t).card ∧ + CataloguePrefix L (m - t) D (D + (m - t + 1) * 10 ^ L) + ((m - t + 1) * 10 ^ L) x.mem y.mem := by + let S := (m - t + 1) * 10 ^ L + let R := D + S + let B := Nat.count (Eligible L (m - t)) S + have hS : Nat.count (Eligible L (m - t)) S ≤ S := Nat.count_le _ + have h10 : Fits w 10 := hfit.of_le ((by decide : 10 ≤ 12).trans (Nat.le_add_left _ _)) + obtain ⟨a, ha, a0, a1, a10, a9, a3, am, af⟩ := exec_constants x h10 + have aL : a.regs Reg.levels = L := (af _ (by decide) (by decide) + (by decide) (by decide) (by decide)).trans hL + obtain ⟨b, hb, bT, b1, bm, bf⟩ := exec_span a aL a10 (hfit.of_le (by omega)) + have bL : b.regs Reg.levels = L := (bf _ (by decide) (by decide) (by decide)).trans aL + have bD : b.regs Reg.directory = D := + (bf _ (by decide) (by decide) (by decide)).trans + ((af _ (by decide) (by decide) (by decide) (by decide) (by decide)).trans hD) + have bm' : b.regs Reg.inner = m := + (bf _ (by decide) (by decide) (by decide)).trans + ((af _ (by decide) (by decide) (by decide) (by decide) (by decide)).trans hm) + have bt : b.regs Reg.threshold = t := + (bf _ (by decide) (by decide) (by decide)).trans + ((af _ (by decide) (by decide) (by decide) (by decide) (by decide)).trans ht) + have b0 : b.regs Reg.nil = 0 := (bf _ (by decide) (by decide) (by decide)).trans a0 + have b10 : b.regs Reg.ten = 10 := (bf _ (by decide) (by decide) (by decide)).trans a10 + have b9 : b.regs Reg.nine = 9 := (bf _ (by decide) (by decide) (by decide)).trans a9 + have b3 : b.regs Reg.three = 3 := (bf _ (by decide) (by decide) (by decide)).trans a3 + obtain ⟨c, hc, cp, cs, cc, cm⟩ := exec_geometrySetup b bL bm' bt bD bT b1 b10 b9 b3 b0 + (hfit.of_le (by omega)) + obtain ⟨d, hd, dp, ds, dc, dmem⟩ := exec_catalogueLoop c cp cs cc + (Nat.le_refl _) (hfit.of_le (by omega)) + have hf3 : Fits w (B * 3) := hfit.of_le (by dsimp only [B]; omega) + have hfV : Fits w (R + B * 3) := hfit.of_le (by dsimp only [B, R]; omega) + let y := (d.set Reg.temporary (B * 3)).set Reg.values (R + B * 3) + have he : ExecWithin w geometryFinish d y 2 := by + ram_eval [geometryFinish, y, dc, dp.three, dp.records, hf3, hfV, B, R, S, + Reg.temporary, Reg.values, Reg.count, Reg.three, Reg.records, Fin.mk.injEq] + have hy : ExecWithin w geometry x y + (4 * L + 20 + (11 * L + 28) * ((m - t + 1) * 10 ^ L)) := by + exact (ha.seq (hb.seq (hc.seq (hd.seq he)))).mono (by omega) + have hycount : y.regs Reg.count = B := by + simpa [y, Reg.temporary, Reg.values, Reg.count, B, S] using dc + have hB : B = (Cslib.Algorithms.MatrixMultiplication.Schonhage.boxes L m t).card := + count_eligible_eq_card_boxes L m t + refine ⟨y, hy, ?_, hycount.trans hB, ?_, ?_⟩ + · constructor + · simpa [y, Reg.temporary, Reg.values, Reg.levels] using dp.levels + · simpa [y, Reg.temporary, Reg.values, Reg.height] using dp.height + · simpa [y, Reg.temporary, Reg.values, Reg.span] using dp.span + · simpa [y, Reg.temporary, Reg.values, Reg.directory] using dp.directory + · simpa [y, Reg.temporary, Reg.values, Reg.records] using dp.records + · simpa [y, Reg.temporary, Reg.values, Reg.slots] using dp.slots + · simpa [y, Reg.temporary, Reg.values, Reg.one] using dp.one + · simpa [y, Reg.temporary, Reg.values, Reg.ten] using dp.ten + · simpa [y, Reg.temporary, Reg.values, Reg.nine] using dp.nine + · simpa [y, Reg.temporary, Reg.values, Reg.three] using dp.three + · simpa [y, Reg.temporary, Reg.values, Reg.nil] using dp.nil + · simp [y, R, S, hB, Nat.mul_comm] + · simpa only [y, Data.set_mem, cm, bm, am] using dmem + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Index.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Index.lean new file mode 100644 index 0000000000..36d6199589 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Index.lean @@ -0,0 +1,137 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.CatalogueState +import Complexity.Foundations.Data.Nat.RadixUpdate + +/-! +# Exact canonical-box indexing of the native directory + +Valid directory slots and the existing finite boxes are in bijection. The computed +compact count is therefore the actual box cardinality, not a supplied catalogue size. +The digit-update identity also gives the real child encoding-array index directly. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Finset Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- Completed leaf represented by a raw directory slot. -/ +@[expose] def completionAt (L s : ℕ) : Leaf L := + leafAt ⟨recordCode L s, Nat.mod_lt _ (pow_pos (by decide) L)⟩ + +/-- Canonical cube represented by the slot's star count and completed leaf. -/ +@[expose] def slotCube (L s : ℕ) : Cube L := starLowest (recordStars L s) (completionAt L s) + +/-- Recover the unique raw directory slot of a canonical box. -/ +@[expose] def cubeSlot {L : ℕ} (π : Cube L) : ℕ := + π.starLevels.card * 10 ^ L + (Encoding.leafIndex π.starsToP0).val + +@[simp] theorem recordCode_slot {L : ℕ} (e : ℕ) (c : Fin (10 ^ L)) : + recordCode L (e * 10 ^ L + c.val) = c.val := by + simp [recordCode, Nat.add_mod, Nat.mod_eq_of_lt c.isLt] + +@[simp] theorem recordStars_slot {L : ℕ} (e : ℕ) (c : Fin (10 ^ L)) : + recordStars L (e * 10 ^ L + c.val) = e := by + rw [recordStars, Nat.mul_comm e (10 ^ L), Nat.add_comm, + Nat.add_mul_div_left _ _ (pow_pos (by decide) L), + Nat.div_eq_of_lt c.isLt, Nat.zero_add] + +@[simp] theorem completionAt_slot {L : ℕ} (e : ℕ) (c : Fin (10 ^ L)) : + completionAt L (e * 10 ^ L + c.val) = leafAt c := by + simp [completionAt] + +private theorem completion_population (L s : ℕ) : + (P0Levels (completionAt L s)).card = population (recordCode L s) L := + (population_eq_card_P0Levels ⟨recordCode L s, Nat.mod_lt _ (pow_pos (by decide) L)⟩).symm + +/-- An eligible slot denotes a box with the original finite box predicate. -/ +theorem slotCube_isBox {L m t s : ℕ} (h : Eligible L (m - t) s) : + IsBox m t (slotCube L s) := by + apply isBox_starLowest + rw [completion_population] + exact h.2 + +/-- Eligibility ensures that starring does not saturate before its supplied star count. -/ +theorem slotCube_star_count {L H s : ℕ} (h : Eligible L H s) : + (slotCube L s).starLevels.card = recordStars L s := by + rw [slotCube, starLevels_starLowest, card_lowest, completion_population] + exact min_eq_left h.1 + +/-- Completing a slot cube recovers its original completed leaf. -/ +@[simp] theorem starsToP0_slotCube (L s : ℕ) : + (slotCube L s).starsToP0 = completionAt L s := starsToP0_starLowest _ _ + +/-- Recovering an eligible slot's key returns that exact slot. -/ +theorem cubeSlot_slotCube {L H s : ℕ} (h : Eligible L H s) : + cubeSlot (slotCube L s) = s := by + rw [cubeSlot, slotCube_star_count h, starsToP0_slotCube, completionAt, leafIndex_leafAt] + simpa only [recordStars, recordCode, Nat.mul_comm] using Nat.div_add_mod s (10 ^ L) + +/-- Every finite box has a raw slot in the allocated directory. -/ +theorem cubeSlot_lt {L m t : ℕ} {π : Cube L} (hπ : IsBox m t π) : + cubeSlot π < (m - t + 1) * 10 ^ L := by + have he : π.starLevels.card ≤ m - t := (Nat.le_add_right _ _).trans hπ.1 + calc + cubeSlot π < π.starLevels.card * 10 ^ L + 10 ^ L := + Nat.add_lt_add_left (Encoding.leafIndex π.starsToP0).isLt _ + _ = (π.starLevels.card + 1) * 10 ^ L := by rw [Nat.add_mul, Nat.one_mul] + _ ≤ (m - t + 1) * 10 ^ L := Nat.mul_le_mul_right _ (Nat.succ_le_succ he) + +/-- A box's recovered slot satisfies both actual digit-loop eligibility tests. -/ +theorem eligible_cubeSlot {L m t : ℕ} {π : Cube L} (hπ : IsBox m t π) : + Eligible L (m - t) (cubeSlot π) := by + change recordStars L (cubeSlot π) ≤ population (recordCode L (cubeSlot π)) L ∧ + population (recordCode L (cubeSlot π)) L ≤ m - t + rw [cubeSlot, recordStars_slot, recordCode_slot, population_eq_card_P0Levels, + leafAt_leafIndex, card_P0Levels_starsToP0] + exact ⟨Nat.le_add_right _ _, hπ.1⟩ + +/-- A recovered key denotes precisely the original box. -/ +theorem slotCube_cubeSlot {L m t : ℕ} {π : Cube L} (hπ : IsBox m t π) : + slotCube L (cubeSlot π) = π := by + rw [slotCube, cubeSlot, recordStars_slot, completionAt_slot, leafAt_leafIndex] + exact (eq_starLowest_starsToP0 π hπ.2).symm + +/-- The computed compact count is exactly the existing finite box-set cardinality. -/ +theorem count_eligible_eq_card_boxes (L m t : ℕ) : + Nat.count (Eligible L (m - t)) ((m - t + 1) * 10 ^ L) = (boxes L m t).card := by + rw [Nat.count_eq_card_filter_range] + refine card_bij (fun s _ => slotCube L s) ?_ ?_ ?_ + · intro s hs + exact mem_boxes.mpr (slotCube_isBox (mem_filter.mp hs).2) + · intro s hs s' hs' heq + have hkeys := congrArg cubeSlot heq + simpa only [cubeSlot_slotCube (mem_filter.mp hs).2, + cubeSlot_slotCube (mem_filter.mp hs').2] using hkeys + · intro π hπ + have hp := mem_boxes.mp hπ + exact ⟨cubeSlot π, mem_filter.mpr ⟨mem_range.mpr (cubeSlot_lt hp), + eligible_cubeSlot hp⟩, slotCube_cubeSlot hp⟩ + +/-- The native subtraction computes a replacement leaf's existing decimal index exactly. -/ +theorem leafIndex_update_P0 {L : ℕ} (τ : Leaf L) (ℓ : Fin L) (d : Fin 10) + (hτ : τ ℓ = .P0) : + (Encoding.leafIndex (Function.update τ ℓ (Encoding.termDigits d))).val = + (Encoding.leafIndex τ).val - (9 - d.val) * 10 ^ ℓ.val := by + have hfun : (fun j => Encoding.termDigits.symm + (Function.update τ ℓ (Encoding.termDigits d) j)) = + Function.update (fun j => Encoding.termDigits.symm (τ j)) ℓ d := by + funext j + by_cases h : j = ℓ <;> simp [h] + unfold Encoding.leafIndex + rw [hfun] + have hd : d.val ≤ (Encoding.termDigits.symm (τ ℓ)).val := by + simpa [hτ, Encoding.termDigits] using (Nat.le_of_lt_succ d.isLt) + simpa [hτ, Encoding.termDigits] using Nat.finFunctionFinEquiv_update_of_le + (fun j => Encoding.termDigits.symm (τ j)) ℓ d hd + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Initialize.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Initialize.lean new file mode 100644 index 0000000000..70b02bc7cf --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Initialize.lean @@ -0,0 +1,80 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.InputLayout + +/-! +# Native box-table input adaptation + +The actual header loads, reused power code and pointer arithmetic locate the original +two leaf arrays and the first writable word. No array or workspace is copied or cleared. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Cslib.WordRAM + +/-- Actual scalar header loads with unchanged memory. -/ +theorem exec_inputHeaders {w L m t : ℕ} (x : Data registers) + (hL : x.mem 1 = L) (hm : x.mem 2 = m) (ht : x.mem 3 = t) + (hfit : Fits w 3) : + ∃ y, ExecWithin w inputHeaders x y 6 ∧ y.regs Reg.levels = L ∧ + y.regs Reg.inner = m ∧ y.regs Reg.threshold = t ∧ y.mem = x.mem := by + have h1 : Fits w 1 := hfit.of_le (by decide) + have h2 : Fits w 2 := hfit.of_le (by decide) + let y := (((((x.set Reg.address 1).set Reg.levels L).set Reg.address 2).set + Reg.inner m).set Reg.address 3).set Reg.threshold t + have he : ExecWithin w inputHeaders x y 6 := by + ram_eval [inputHeaders, y, hL, hm, ht, h1, h2, hfit, + Reg.address, Reg.levels, Reg.inner, Reg.threshold, Fin.mk.injEq] + exact ⟨y, he, by simp [y, Reg.levels, Reg.inner, Reg.threshold, Reg.address], + by simp [y, Reg.inner, Reg.threshold, Reg.address], by simp [y], rfl⟩ + +/-- Complete native initialization from the three actual input header words. -/ +theorem exec_loadInput {w L m t : ℕ} (x : Data registers) + (hL : x.mem 1 = L) (hm : x.mem 2 = m) (ht : x.mem 3 = t) + (hfit : Fits w (2 * 10 ^ L + L + 12)) : + ∃ y, ExecWithin w loadInput x y (4 * L + 19) ∧ + y.regs Reg.levels = L ∧ y.regs Reg.inner = m ∧ y.regs Reg.threshold = t ∧ + y.regs Reg.arrayA = 4 ∧ y.regs Reg.arrayB = 4 + 10 ^ L ∧ + y.regs Reg.directory = directoryBase L ∧ y.mem = x.mem := by + obtain ⟨a, ha, aL, am, ath, haμ⟩ := exec_inputHeaders x hL hm ht + (hfit.of_le (by omega)) + obtain ⟨b, hb, _, _, b10, _, _, hbμ, bf⟩ := exec_constants a + (hfit.of_le ((by decide : 10 ≤ 12).trans (Nat.le_add_left _ _))) + have bL : b.regs Reg.levels = L := + (bf _ (by decide) (by decide) (by decide) (by decide) (by decide)).trans aL + obtain ⟨c, hc, cT, _, hcμ, cf⟩ := exec_span b bL b10 (hfit.of_le (by omega)) + have cL : c.regs Reg.levels = L := (cf _ (by decide) (by decide) (by decide)).trans bL + have cm : c.regs Reg.inner = m := + (cf _ (by decide) (by decide) (by decide)).trans + ((bf _ (by decide) (by decide) (by decide) (by decide) (by decide)).trans am) + have ct : c.regs Reg.threshold = t := + (cf _ (by decide) (by decide) (by decide)).trans + ((bf _ (by decide) (by decide) (by decide) (by decide) (by decide)).trans ath) + have hf4 : Fits w 4 := hfit.of_le (by omega) + have hfB : Fits w (4 + 10 ^ L) := hfit.of_le (by omega) + have hfD : Fits w (4 + 10 ^ L + 10 ^ L) := hfit.of_le (by omega) + let y := ((c.set Reg.arrayA 4).set Reg.arrayB (4 + 10 ^ L)).set + Reg.directory (4 + 10 ^ L + 10 ^ L) + have hd : ExecWithin w inputPointers c y 3 := by + ram_eval [inputPointers, y, cT, hf4, hfB, hfD, Reg.arrayA, Reg.arrayB, + Reg.directory, Reg.span, Fin.mk.injEq] + refine ⟨y, (ha.seq (hb.seq (hc.seq hd))).mono (by omega), ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ + · simpa [y, Reg.levels, Reg.arrayA, Reg.arrayB, Reg.directory] using cL + · simpa [y, Reg.inner, Reg.arrayA, Reg.arrayB, Reg.directory] using cm + · simpa [y, Reg.threshold, Reg.arrayA, Reg.arrayB, Reg.directory] using ct + · simp [y, Reg.arrayA, Reg.arrayB, Reg.directory] + · simp [y, Reg.arrayB, Reg.directory] + · simp [y, directoryBase]; omega + · exact hcμ.trans (hbμ.trans haμ) + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Input.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Input.lean new file mode 100644 index 0000000000..6e796ee4f6 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Input.lean @@ -0,0 +1,110 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Initialize +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Tile +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Bounds + +/-! +# Complete initialized native box-table constructor + +The actual fixed program constructs its shared geometry and one compact signed value +table from ordinary headers and encoded leaf arrays. Computed directory ranks, descriptors, +values, frame and charged time refer to the same final data witness. The geometry charge +remains separate from the linear-in-box-count cost of another tile. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- Actual initialized construction, with all geometry and value work discharged. -/ +theorem exec_input {w L m t A B : ℕ} (a b : Fin (10 ^ L) → ℤ) + (ha : ∀ i, (a i).natAbs ≤ A) (hb : ∀ i, (b i).natAbs ≤ B) + (haddr : Fits (w + 2) (addressBound L m t)) + (hmag : GenericRAM.Signed.Fits w (magnitudeBound L A B : ℕ)) : + InputFits (w + 2) (input L m t a b) ∧ + ∃ y, ExecWithin (w + 2) program (State.init (input L m t a b)).data y + (timeBound L m t - 1) ∧ y.Bounded (w + 2) ∧ + y.regs Reg.levels = L ∧ y.regs Reg.height = m - t ∧ + y.regs Reg.span = 10 ^ L ∧ y.regs Reg.directory = directoryBase L ∧ + y.regs Reg.values = valueBase L m t ∧ + y.regs Reg.count = (boxes L m t).card ∧ + (∀ s < (m - t + 1) * 10 ^ L, + y.mem (directoryBase L + s) = directoryWord L (m - t) s) ∧ + (∀ s < (m - t + 1) * 10 ^ L, Eligible L (m - t) s → + y.mem (valueBase L m t + Nat.count (Eligible L (m - t)) s) = + Signed.encode (slotValue (fun τ => a (Encoding.leafIndex τ)) + (fun τ => b (Encoding.leafIndex τ)) s)) ∧ + (∀ q, ¬(directoryBase L ≤ q ∧ q < memoryEnd L m t) → + y.mem q = (State.init (input L m t a b) : State registers).data.mem q) := by + have hi := input_fits a b ha hb haddr hmag + let x : Data registers := (State.init (input L m t a b)).data + let S := (m - t + 1) * 10 ^ L + let K := (boxes L m t).card + have hK : K = Nat.count (Eligible L (m - t)) S := + (count_eligible_eq_card_boxes L m t).symm + have hKS : K ≤ S := hK ▸ Nat.count_le _ + have hT : 10 ^ L ≤ S := Nat.le_mul_of_pos_left _ (by omega) + have hA : 4 + 10 ^ L ≤ directoryBase L := by unfold directoryBase; omega + have hB : 4 + 10 ^ L + 10 ^ L = directoryBase L := by unfold directoryBase; omega + obtain ⟨xL, xm, xt, xA, xB⟩ := input_readback L m t a b + obtain ⟨u, hu, uL, um, ut, uA, uB, uD, uμ⟩ := exec_loadInput (L := L) (m := m) (t := t) x xL xm xt + (haddr.of_le (by unfold addressBound; dsimp only [S] at hT; omega)) + obtain ⟨v, hv, vp, vK, vV, vcat⟩ := exec_geometry + (L := L) (m := m) (t := t) (D := directoryBase L) u uL um ut uD + (haddr.of_le (by unfold addressBound directoryBase; dsimp only [S] at hKS hT; omega)) + have vA : v.regs Reg.arrayA = 4 := + (hv.regs_eq (by decide : geometry.Preserves Reg.arrayA)).trans uA + have vB : v.regs Reg.arrayB = 4 + 10 ^ L := + (hv.regs_eq (by decide : geometry.Preserves Reg.arrayB)).trans uB + have vV' : v.regs Reg.values = valueBase L m t := vV + have vleft (i : Fin (10 ^ L)) : v.mem (4 + i.val) = Signed.encode (a i) := by + rw [vcat.frame _ (by have := i.isLt; omega) (by + unfold directoryBase; have := i.isLt; omega), uμ] + exact xA i + have vright (i : Fin (10 ^ L)) : v.mem (4 + 10 ^ L + i.val) = Signed.encode (b i) := by + rw [vcat.frame _ (by have := i.isLt; omega) (by + unfold directoryBase; have := i.isLt; omega), uμ] + exact xB i + obtain ⟨y, hy, yvalues, yframe, yregs⟩ := exec_tile v + (fun τ => a (Encoding.leafIndex τ)) (fun τ => b (Encoding.leafIndex τ)) + (fun τ => ha _) (fun τ => hb _) vp vV' vA vB (vK.trans hK) + vcat (Nat.le_refl _) (by rw [← hK]; exact Nat.le_refl _) + (by unfold valueBase recordBase; omega) + (by unfold valueBase recordBase; omega) + (fun i => by simpa only [leafIndex_leafAt] using vleft i) + (fun i => by simpa only [leafIndex_leafAt] using vright i) + (haddr.of_le (by + unfold addressBound valueBase recordBase directoryBase + dsimp only [K, S] at hKS hT + omega)) hmag + have he : ExecWithin (w + 2) program x y (timeBound L m t - 1) := by + apply (hu.seq (hv.seq hy)).mono + simp only [timeBound, geometryTime, tileTime, count_eligible_eq_card_boxes] + omega + refine ⟨hi, y, he, he.bounded (Data.Bounded.init hi), ?_, ?_, ?_, ?_, + ?_, ?_, ?_, yvalues, ?_⟩ + · exact (hy.regs_eq (by decide : tile.Preserves Reg.levels)).trans vp.levels + · exact (hy.regs_eq (by decide : tile.Preserves Reg.height)).trans vp.height + · exact (hy.regs_eq (by decide : tile.Preserves Reg.span)).trans vp.span + · exact (hy.regs_eq (by decide : tile.Preserves Reg.directory)).trans vp.directory + · exact (yregs _ (by decide)).trans vV' + · exact (yregs _ (by decide)).trans vK + · intro s hs + rw [yframe _ (by unfold valueBase recordBase; omega)] + exact vcat.directory s hs + · intro q hq + rw [yframe _ (by unfold memoryEnd at hq; rw [← hK]; omega)] + rw [vcat.frame _ (by unfold memoryEnd valueBase recordBase at hq; omega) + (by unfold memoryEnd valueBase recordBase at hq; rw [← hK]; omega), uμ] + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/InputLayout.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/InputLayout.lean new file mode 100644 index 0000000000..aa41d3a984 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/InputLayout.lean @@ -0,0 +1,103 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Geometry +public import Complexity.Computability.WordRAM.InputArray +public import Complexity.Computability.GenericRAM.Signed.Fits + +/-! +# Original input and native box-table layout + +Three raw headers are followed by the two canonical signed leaf arrays. The directory, +compact descriptors and values are allocated after those original arrays. Their extents +are computed from the depth and finite box cardinality; no layout is an input certificate. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- Ordinary scalar headers and two actual canonical signed encoding arrays. -/ +@[expose] def input (L m t : ℕ) (a b : Fin (10 ^ L) → ℤ) : List ℕ := + [L, m, t] ++ List.ofFn (fun i => Signed.encode (a i)) ++ + List.ofFn (fun i => Signed.encode (b i)) + +/-- The directory starts immediately after the original input. -/ +@[expose] def directoryBase (L : ℕ) : ℕ := 4 + 2 * 10 ^ L + +/-- The compact descriptors follow the complete shared directory. -/ +@[expose] def recordBase (L m t : ℕ) : ℕ := + directoryBase L + (m - t + 1) * 10 ^ L + +/-- The actual value array follows three words per emitted record. -/ +@[expose] def valueBase (L m t : ℕ) : ℕ := recordBase L m t + 3 * (boxes L m t).card + +/-- End of the shared directory, compact descriptors and one complete value table. -/ +@[expose] def memoryEnd (L m t : ℕ) : ℕ := valueBase L m t + (boxes L m t).card + +/-- One original-input scalar envelope covers all address arithmetic of construction. -/ +@[expose] def addressBound (L m t : ℕ) : ℕ := + 100 * (L + m + t + (m - t + 1) * 10 ^ L + 10) + +/-- One signed envelope covers operands even when their opposite array is identically zero. -/ +@[expose] def magnitudeBound (L A B : ℕ) : ℕ := A + B + 10 ^ L * (A * B) + +@[simp] theorem length_input (L m t : ℕ) (a b : Fin (10 ^ L) → ℤ) : + (input L m t a b).length = 3 + 2 * 10 ^ L := by simp [input]; omega + +/-- The actual input fits under the same original scalar and signed envelopes as execution. -/ +theorem input_fits {w L m t A B : ℕ} (a b : Fin (10 ^ L) → ℤ) + (ha : ∀ i, (a i).natAbs ≤ A) (hb : ∀ i, (b i).natAbs ≤ B) + (haddr : Fits (w + 2) (addressBound L m t)) + (hmag : GenericRAM.Signed.Fits w (magnitudeBound L A B : ℕ)) : + InputFits (w + 2) (input L m t a b) := by + have hp : 1 ≤ 10 ^ L := Nat.one_le_pow L _ (by decide) + have hS : 10 ^ L ≤ (m - t + 1) * 10 ^ L := Nat.le_mul_of_pos_left _ (by omega) + constructor + · rw [length_input] + exact haddr.of_le (by unfold addressBound; omega) + · intro v hv + simp only [input, List.mem_append, List.mem_cons, List.not_mem_nil, or_false] at hv + rcases hv with ((rfl | rfl | rfl) | hv) | hv + · exact haddr.of_le (by unfold addressBound; omega) + · exact haddr.of_le (by unfold addressBound; omega) + · exact haddr.of_le (by unfold addressBound; omega) + · obtain ⟨i, rfl⟩ := List.mem_ofFn.mp hv + exact (Signed.encode_fits (hmag.of_natAbs_le ((ha i).trans + (by unfold magnitudeBound; omega)))).mono (by omega) + · obtain ⟨i, rfl⟩ := List.mem_ofFn.mp hv + exact (Signed.encode_fits (hmag.of_natAbs_le ((hb i).trans + (by unfold magnitudeBound; omega)))).mono (by omega) + +/-- Actual initialized words contain the two original signed arrays at their computed bases. -/ +theorem input_readback (L m t : ℕ) (a b : Fin (10 ^ L) → ℤ) : + let x : Data registers := (State.init (input L m t a b)).data + x.mem 1 = L ∧ x.mem 2 = m ∧ x.mem 3 = t ∧ + (∀ i : Fin (10 ^ L), x.mem (4 + i.val) = Signed.encode (a i)) ∧ + (∀ i : Fin (10 ^ L), x.mem (4 + 10 ^ L + i.val) = Signed.encode (b i)) := by + dsimp only + refine ⟨by simp [State.init, Data.init, input], by simp [State.init, Data.init, input], + by simp [State.init, Data.init, input], ?_, ?_⟩ + · intro i + have h := Data.init_realizes_append (r := registers) [L, m, t] + (List.ofFn (fun j => Signed.encode (a j))) (List.ofFn (fun j => Signed.encode (b j))) + have hr := h ⟨i.val, by simp⟩ + simpa [State.init, input, Block.read, List.append_assoc] using hr + · intro i + have hfour (n : ℕ) : 1 + (1 + (1 + (1 + n))) = 4 + n := by omega + have h := Data.init_realizes_append (r := registers) + ([L, m, t] ++ List.ofFn (fun j => Signed.encode (a j))) + (List.ofFn (fun j => Signed.encode (b j))) [] + have hr := h ⟨i.val, by simp⟩ + simpa [State.init, input, Block.read, List.append_assoc, Nat.add_assoc, + Nat.add_comm, Nat.add_left_comm, hfour] using hr + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Lookup.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Lookup.lean new file mode 100644 index 0000000000..7bd8a5886a --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Lookup.lean @@ -0,0 +1,142 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.LookupLoop +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Values + +/-! +# Native lookup in the computed compact box table + +The real code scans the original cube digits and reads its computed directory rank +and signed table word. The caller supplies ordinary memory readback, as obtained from +the native catalogue and value constructors. All scan and address arithmetic is charged; +the lookup preserves all memory and registers outside its documented scalar workspace. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- The complete scalar workspace modified by native lookup, including returned fields. -/ +@[expose] def LookupWholeLocal (i : Fin registers) : Prop := + LookupLocal i ∨ i = Reg.nil ∨ i = Reg.one ∨ i = Reg.ten ∨ i = Reg.nine ∨ + i = Reg.three ∨ i = Reg.found ∨ i = Reg.answer ∨ i = Reg.childSlot ∨ i = Reg.childRank + +instance (i : Fin registers) : Decidable (LookupWholeLocal i) := + inferInstanceAs (Decidable (LookupLocal i ∨ i = Reg.nil ∨ i = Reg.one ∨ i = Reg.ten ∨ + i = Reg.nine ∨ i = Reg.three ∨ i = Reg.found ∨ i = Reg.answer ∨ + i = Reg.childSlot ∨ i = Reg.childRank)) + +private theorem lookup_preserves (i : Fin registers) : + ¬LookupWholeLocal i → lookup.Preserves i := by decide +revert + +private theorem lookupSetup_preserves (i : Fin registers) : + ¬LookupWholeLocal i → lookupSetup.Preserves i := by decide +revert + +private theorem exec_lookupSetup {w L C : ℕ} (x : Data registers) + (hL : x.regs Reg.levels = L) (hC : x.regs Reg.cube = C) (hfit : Fits w 10) : + ∃ y, ExecWithin w lookupSetup x y 14 ∧ y.mem = x.mem ∧ LookupParameters L C y ∧ + y.regs Reg.level = 0 ∧ y.regs Reg.power = 1 ∧ y.regs Reg.completion = 0 ∧ + y.regs Reg.stars = 0 ∧ y.regs Reg.population = 0 ∧ + y.regs Reg.fixedSeen = 0 ∧ y.regs Reg.invalid = 0 ∧ + (∀ i, ¬LookupWholeLocal i → y.regs i = x.regs i) := by + have hf0 : Fits w 0 := hfit.of_le (by decide) + have hf1 : Fits w 1 := hfit.of_le (by decide) + have hf3 : Fits w 3 := hfit.of_le (by decide) + have hf9 : Fits w 9 := hfit.of_le (by decide) + let y := ((((((((((((((x.set Reg.nil 0).set Reg.one 1).set Reg.ten 10).set Reg.nine 9).set + Reg.three 3).set Reg.level 0).set Reg.stars 0).set Reg.population 0).set + Reg.fixedSeen 0).set Reg.invalid 0).set Reg.completion 0).set Reg.power 1).set + Reg.found 0).set Reg.answer 0) + have hy : ExecWithin w lookupSetup x y 14 := by + ram_eval [lookupSetup, constants, y, hfit, hf0, hf1, hf3, hf9, + Reg.nil, Reg.one, Reg.ten, Reg.nine, Reg.three, Reg.level, Reg.stars, + Reg.population, Reg.fixedSeen, Reg.invalid, Reg.completion, Reg.power, + Reg.found, Reg.answer, Fin.mk.injEq] + refine ⟨y, hy, rfl, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, + fun i hi => hy.regs_eq (lookupSetup_preserves i hi)⟩ + · constructor <;> simp [y, hL, hC, Reg.nil, Reg.one, Reg.ten, Reg.nine, Reg.three, + Reg.level, Reg.stars, Reg.population, Reg.fixedSeen, Reg.invalid, Reg.completion, + Reg.power, Reg.found, Reg.answer, Reg.levels, Reg.cube] + all_goals simp [y, Reg.nil, Reg.one, Reg.ten, Reg.nine, Reg.three, + Reg.level, Reg.stars, Reg.population, Reg.fixedSeen, Reg.invalid, Reg.completion, + Reg.power, Reg.found, Reg.answer] + +/-- Read the genuine signed word at a valid box's computed compact rank. -/ +theorem exec_lookup {w L m t C D V : ℕ} (x : Data registers) (π : Cube L) + (a b : Leaf L → ℤ) (hπ : IsBox m t π) + (hL : x.regs Reg.levels = L) (hH : x.regs Reg.height = m - t) + (hT : x.regs Reg.span = 10 ^ L) (hC : x.regs Reg.cube = C) + (hD : x.regs Reg.directory = D) (hV : x.regs Reg.values = V) + (hread : ∀ i < L, x.mem (C + i) = rawCubeDigit π i) + (hdir : ∀ s < (m - t + 1) * 10 ^ L, x.mem (D + s) = directoryWord L (m - t) s) + (hvalues : ∀ s < (m - t + 1) * 10 ^ L, Eligible L (m - t) s → + x.mem (V + Nat.count (Eligible L (m - t)) s) = Signed.encode (slotValue a b s)) + (hfit : Fits w (C + D + V + (m - t + 1) * 10 ^ L + 10 ^ L + L + 30)) : + ∃ y, ExecWithin w lookup x y (18 * L + 32) ∧ y.mem = x.mem ∧ + y.regs Reg.found = 1 ∧ + y.regs Reg.answer = Signed.encode (boxValue a b π.starLevels.card π) ∧ + (∀ i, ¬LookupWholeLocal i → y.regs i = x.regs i) := by + obtain ⟨u, hu, hum, hup, hul, hupow, huc, hus, huf, huv, hui, hframeu⟩ := + exec_lookupSetup x hL hC (hfit.of_le (by omega)) + obtain ⟨z, hz, hzm, hzp, hzl, hzpow, hzc, hzs, hzf, hzi, hframez⟩ := + exec_lookupLoop u π hπ hup (by simpa only [hum] using hread) + hul hupow huc hus huf huv hui (hfit.of_le (by omega)) + have hmem : z.mem = x.mem := hzm.trans hum + have hpres (i : Fin registers) (hi : ¬LookupWholeLocal i) : z.regs i = x.regs i := + (hframez i (fun h => hi (Or.inl h))).trans (hframeu i hi) + have zH : z.regs Reg.height = m - t := (hpres _ (by decide)).trans hH + have zT : z.regs Reg.span = 10 ^ L := (hpres _ (by decide)).trans hT + have zD : z.regs Reg.directory = D := (hpres _ (by decide)).trans hD + have zV : z.regs Reg.values = V := (hpres _ (by decide)).trans hV + let s := cubeSlot π + let r := Nat.count (Eligible L (m - t)) s + have hs : s < (m - t + 1) * 10 ^ L := cubeSlot_lt hπ + have hv : Eligible L (m - t) s := eligible_cubeSlot hπ + have hr : r ≤ s := Nat.count_le _ + have hslot : π.starLevels.card * 10 ^ L + + (Encoding.leafIndex π.starsToP0).val = s := rfl + have hword : z.mem (D + s) = r + 1 := by + rw [hmem, hdir s hs, directoryWord, ite_eq_left hv] + have hvalue : z.mem (V + r) = Signed.encode (slotValue a b s) := by + rw [hmem] + exact hvalues s hs hv + have hfprod : Fits w (π.starLevels.card * 10 ^ L) := hfit.of_le (by omega) + have hfs : Fits w s := hfit.of_le (by omega) + have hfD : Fits w (D + s) := hfit.of_le (by omega) + have hfr : Fits w r := hfit.of_le (by omega) + have hfV : Fits w (V + r) := hfit.of_le (by omega) + have hf1 : Fits w 1 := hfit.of_le (by omega) + have hnH : ¬m - t < π.starLevels.card + π.P0Levels.card := not_lt.mpr hπ.1 + have hnr : ¬r + 1 = 0 := by omega + let z' := z.set Reg.temporary (z.regs Reg.temporary) + let y := ((((((((z'.set Reg.childSlot (π.starLevels.card * 10 ^ L)).set Reg.childSlot s).set + Reg.address (D + s)).set Reg.childRank (r + 1)).set Reg.childRank r).set + Reg.address (V + r)).set Reg.answer (Signed.encode (slotValue a b s))).set Reg.found 1) + have hy : ExecWithin w lookupFinish z y 16 := by + ram_eval [lookupFinish, y, z', zH, zT, zD, zV, hzs, hzc, hzf, hzi, + hzp.nil, hzp.one, hnH, hslot, hword, hvalue, hnr, + hfprod, hfs, hfD, hfr, hfV, hf1, Nat.add_sub_cancel, + Reg.height, Reg.population, Reg.invalid, Reg.nil, Reg.temporary, + Reg.childSlot, Reg.stars, Reg.span, Reg.completion, Reg.address, Reg.directory, + Reg.childRank, Reg.one, Reg.values, Reg.answer, Reg.found, Fin.mk.injEq] + have he : ExecWithin w lookup x y (18 * L + 32) := + (hu.seq (hz.seq hy)).mono (by omega) + refine ⟨y, he, hmem, ?_, ?_, fun i hi => he.regs_eq (lookup_preserves i hi)⟩ + · simp [y, Reg.found, Reg.answer] + · have hval : slotValue a b s = boxValue a b π.starLevels.card π := by + have hstars : recordStars L s = π.starLevels.card := by + dsimp only [s, cubeSlot] + rw [recordStars_slot] + rw [slotValue, hstars, slotCube_cubeSlot hπ] + simpa [y, Reg.found, Reg.answer] using congrArg Signed.encode hval + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/LookupDigits.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/LookupDigits.lean new file mode 100644 index 0000000000..99f7783c31 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/LookupDigits.lean @@ -0,0 +1,187 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Digits +import Complexity.Foundations.Data.Nat.Radix + +/-! +# Raw cube digits for native box-table lookup + +Terms use the existing encoder's ten digits; a star uses eleven-symbol digit ten. +`lookupCompletion` is the prefix value actually accumulated by the native lookup, +replacing stars by P0 digit nine. The full readback and order lemmas use the existing +cube and box notions, without introducing another membership or ordering predicate. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Finset Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- A raw cube digit uses ten for a star and the existing native digit for a term. -/ +@[expose] def cubeDigit {L : ℕ} (π : Cube L) (k : Fin L) : ℕ := + match π k with + | .star => 10 + | .term lam => (Encoding.termDigits.symm lam).val + +/-- Extend the real cube digits by zero outside its finite input span. -/ +@[expose] def rawCubeDigit {L : ℕ} (π : Cube L) (k : ℕ) : ℕ := + if h : k < L then cubeDigit π ⟨k, h⟩ else 0 + +/-- The completion code accumulated in the first `k` native lookup iterations. -/ +@[expose] def lookupCompletion (raw : ℕ → ℕ) : ℕ → ℕ + | 0 => 0 + | k + 1 => lookupCompletion raw k + (if raw k = 10 then 9 else raw k) * 10 ^ k + +/-- Every actual cube symbol fits the eleven-symbol input alphabet. -/ +theorem cubeDigit_le_ten {L : ℕ} (π : Cube L) (k : Fin L) : cubeDigit π k ≤ 10 := by + cases h : π k with + | star => simp [cubeDigit, h] + | term lam => simpa only [cubeDigit, h] using (Encoding.termDigits.symm lam).isLt.le + +@[simp] theorem rawCubeDigit_fin {L : ℕ} (π : Cube L) (k : Fin L) : + rawCubeDigit π k.val = cubeDigit π k := by simp [rawCubeDigit, k.isLt] + +/-- The zero extension obeys the same digit bound at every natural index. -/ +theorem rawCubeDigit_le_ten {L : ℕ} (π : Cube L) (k : ℕ) : rawCubeDigit π k ≤ 10 := by + by_cases h : k < L + · simpa only [rawCubeDigit, dite_eq_left h] using cubeDigit_le_ten π ⟨k, h⟩ + · simp [rawCubeDigit, h] + +/-- Ten denotes precisely a star. -/ +@[simp] theorem cubeDigit_eq_ten_iff {L : ℕ} (π : Cube L) (k : Fin L) : + cubeDigit π k = 10 ↔ π k = .star := by + cases h : π k with + | star => simp [cubeDigit, h] + | term lam => + have hlt := (Encoding.termDigits.symm lam).isLt + simp [cubeDigit, h, Nat.ne_of_lt hlt] + +/-- Nine denotes precisely a fixed P0 term. -/ +@[simp] theorem cubeDigit_eq_nine_iff {L : ℕ} (π : Cube L) (k : Fin L) : + cubeDigit π k = 9 ↔ π k = .term .P0 := by + cases h : π k with + | star => simp [cubeDigit, h] + | term lam => + have he : (Encoding.termDigits.symm lam).val = 9 ↔ lam = .P0 := by + constructor + · intro hh + have hf : Encoding.termDigits.symm lam = 9 := Fin.ext hh + calc + lam = Encoding.termDigits (Encoding.termDigits.symm lam) := + (Encoding.termDigits.apply_symm_apply lam).symm + _ = Encoding.termDigits 9 := congrArg Encoding.termDigits hf + _ = .P0 := by decide + · intro hh + simp [hh, Encoding.termDigits] + simpa [cubeDigit, h] using he + +/-- Native prefix completion is the ordinary little-endian weighted digit sum. -/ +theorem lookupCompletion_eq_sum (raw : ℕ → ℕ) (k : ℕ) : + lookupCompletion raw k = + ∑ i ∈ range k, (if raw i = 10 then 9 else raw i) * 10 ^ i := by + induction k with + | zero => simp [lookupCompletion] + | succ k ih => rw [lookupCompletion, sum_range_succ, ih] + +/-- Every completed prefix is a genuine decimal code, including empty input. -/ +theorem lookupCompletion_lt {raw : ℕ → ℕ} {k : ℕ} (hraw : ∀ i < k, raw i ≤ 10) : + lookupCompletion raw k < 10 ^ k := by + induction k with + | zero => simp [lookupCompletion] + | succ k ih => + have hk := ih (fun i hi => hraw i (by omega)) + have hd : (if raw k = 10 then 9 else raw k) ≤ 9 := by + split <;> have h := hraw k (by omega) <;> omega + calc + lookupCompletion raw (k + 1) < + 10 ^ k + (if raw k = 10 then 9 else raw k) * 10 ^ k := + Nat.add_lt_add_right hk _ + _ ≤ 10 ^ k + 9 * 10 ^ k := Nat.add_le_add_left (Nat.mul_le_mul_right _ hd) _ + _ = 10 ^ (k + 1) := by rw [pow_succ]; omega + +/-- Actual completion of all input digits is exactly the encoder's existing leaf index. -/ +theorem lookupCompletion_rawCubeDigit {L : ℕ} (π : Cube L) : + lookupCompletion (rawCubeDigit π) L = (Encoding.leafIndex π.starsToP0).val := by + rw [lookupCompletion_eq_sum, ← Fin.sum_univ_eq_sum_range, Encoding.leafIndex, + finFunctionFinEquiv_apply] + apply sum_congr rfl + intro k _ + rw [rawCubeDigit_fin] + cases h : π k with + | star => simp [cubeDigit, Cube.starsToP0, h, Encoding.termDigits] + | term lam => + have hn : (Encoding.termDigits.symm lam).val ≠ 10 := + Nat.ne_of_lt (Encoding.termDigits.symm lam).isLt + simp [cubeDigit, Cube.starsToP0, h, hn] + +private theorem count_rawCubeDigit {L : ℕ} (π : Cube L) (p : ℕ → Prop) [DecidablePred p] : + Nat.count (fun i => p (rawCubeDigit π i)) L = + (univ.filter fun k : Fin L => p (cubeDigit π k)).card := by + rw [Nat.count_eq_card_filter_range] + symm + refine card_bij (fun k _ => k.val) ?_ ?_ ?_ + · intro k hk + exact mem_filter.mpr ⟨mem_range.mpr k.isLt, by + simpa only [rawCubeDigit_fin] using (mem_filter.mp hk).2⟩ + · intro k _ k' _ hh + exact Fin.ext hh + · intro i hi + obtain ⟨hiL, hp⟩ := mem_filter.mp hi + refine ⟨⟨i, mem_range.mp hiL⟩, mem_filter.mpr ⟨mem_univ _, ?_⟩, rfl⟩ + simpa only [rawCubeDigit, dite_eq_left (mem_range.mp hiL)] using hp + +/-- The native star counter reads the actual finite cube's star count. -/ +theorem count_rawCubeDigit_stars {L : ℕ} (π : Cube L) : + Nat.count (fun i => rawCubeDigit π i = 10) L = π.starLevels.card := by + rw [count_rawCubeDigit π (fun d => d = 10)] + congr 1 + ext k + simp + +/-- The native population counter reads fixed P0 terms plus stars completed with P0. -/ +theorem count_rawCubeDigit_population {L : ℕ} (π : Cube L) : + Nat.count (fun i => rawCubeDigit π i = 9 ∨ rawCubeDigit π i = 10) L = + π.starLevels.card + π.P0Levels.card := by + rw [count_rawCubeDigit π (fun d => d = 9 ∨ d = 10)] + have hf : (univ.filter fun k : Fin L => cubeDigit π k = 9 ∨ cubeDigit π k = 10) = + π.starLevels ∪ π.P0Levels := by + ext k + simp [or_comm] + rw [hf, card_union_of_disjoint π.disjoint_starLevels_P0Levels] + +/-- Completing stars preserves the population counted by the native lookup scan. -/ +theorem population_lookupCompletion {L : ℕ} (π : Cube L) : + population (lookupCompletion (rawCubeDigit π) L) L = + π.starLevels.card + π.P0Levels.card := by + rw [lookupCompletion_rawCubeDigit] + simpa only [leafAt_leafIndex, card_P0Levels_starsToP0] using + population_eq_card_P0Levels (Encoding.leafIndex π.starsToP0) + +/-- A canonical box never has a fixed P0 before a later starred coordinate. -/ +theorem no_fixed_before_star {L m t : ℕ} {π : Cube L} (hπ : IsBox m t π) + (k : Fin L) (hk : π k = .star) : + ¬ ∃ i : Fin L, i < k ∧ cubeDigit π i = 9 := by + rintro ⟨i, hik, hi⟩ + have hki := hπ.2 k (Cube.mem_starLevels.mpr hk) i + (Cube.mem_P0Levels.mpr ((cubeDigit_eq_nine_iff π i).mp hi)) + exact lt_asymm hik hki + +/-- Natural-index form of the order invariant consumed by the native lookup scan. -/ +theorem rawCubeDigit_no_fixed_before_star {L m t : ℕ} {π : Cube L} (hπ : IsBox m t π) + {k : ℕ} (hk : k < L) (hs : rawCubeDigit π k = 10) : + ¬ ∃ i < k, rawCubeDigit π i = 9 := by + rintro ⟨i, hik, hi⟩ + have hiL : i < L := hik.trans hk + apply no_fixed_before_star hπ ⟨k, hk⟩ + ((cubeDigit_eq_ten_iff π _).mp (by simpa only [rawCubeDigit, dite_eq_left hk] using hs)) + exact ⟨⟨i, hiL⟩, hik, by simpa only [rawCubeDigit, dite_eq_left hiL] using hi⟩ + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/LookupLoop.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/LookupLoop.lean new file mode 100644 index 0000000000..e9ffbefec9 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/LookupLoop.lean @@ -0,0 +1,122 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.LookupStep +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.LookupDigits + +/-! +# Complete native cube-digit lookup scan + +The actual loop reads every original cube word once and returns the existing completed +leaf index, exact star/P0 counts and a valid order flag. Its invariant counts fixed P0 +occurrences with Mathlib's count, so no precomputed order or index certificate is needed. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Cslib.WordRAM Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- Persistent actual register contents used by a raw cube lookup scan. -/ +structure LookupParameters (L C : ℕ) (x : Data registers) : Prop where + /-- Original depth. -/ + levels : x.regs Reg.levels = L + /-- Real input cube pointer. -/ + cube : x.regs Reg.cube = C + /-- Constant zero. -/ + nil : x.regs Reg.nil = 0 + /-- Constant one. -/ + one : x.regs Reg.one = 1 + /-- Constant P0 digit. -/ + nine : x.regs Reg.nine = 9 + /-- Constant radix and star digit. -/ + ten : x.regs Reg.ten = 10 + +private theorem lookupLoop_preserves (i : Fin registers) : + ¬LookupLocal i → (Code.loop (.lt Reg.level Reg.levels) lookupDigit).Preserves i := by + decide +revert + +/-- The native loop computes every final lookup scalar from the actual cube words. -/ +theorem exec_lookupLoop {w L m t C : ℕ} (x : Data registers) (π : Cube L) + (hπ : IsBox m t π) (hx : LookupParameters L C x) + (hread : ∀ i < L, x.mem (C + i) = rawCubeDigit π i) + (hlevel : x.regs Reg.level = 0) (hpow : x.regs Reg.power = 1) + (hcode : x.regs Reg.completion = 0) (hstars : x.regs Reg.stars = 0) + (hpop : x.regs Reg.population = 0) (hseen : x.regs Reg.fixedSeen = 0) + (hinvalid : x.regs Reg.invalid = 0) + (hfit : Fits w (C + 10 ^ L + L + 20)) : + ∃ y, ExecWithin w (.loop (.lt Reg.level Reg.levels) lookupDigit) x y (18 * L + 2) ∧ + y.mem = x.mem ∧ LookupParameters L C y ∧ y.regs Reg.level = L ∧ + y.regs Reg.power = 10 ^ L ∧ + y.regs Reg.completion = (Encoding.leafIndex π.starsToP0).val ∧ + y.regs Reg.stars = π.starLevels.card ∧ + y.regs Reg.population = π.starLevels.card + π.P0Levels.card ∧ + y.regs Reg.invalid = 0 ∧ + (∀ i, ¬LookupLocal i → y.regs i = x.regs i) := by + let raw := rawCubeDigit π + let I (y : Data registers) : Prop := + LookupParameters L C y ∧ y.mem = x.mem ∧ y.regs Reg.level ≤ L ∧ + y.regs Reg.power = 10 ^ y.regs Reg.level ∧ + y.regs Reg.completion = lookupCompletion raw (y.regs Reg.level) ∧ + y.regs Reg.stars = Nat.count (fun i => raw i = 10) (y.regs Reg.level) ∧ + y.regs Reg.population = Nat.count (fun i => raw i = 9 ∨ raw i = 10) (y.regs Reg.level) ∧ + y.regs Reg.fixedSeen = (if Nat.count (fun i => raw i = 9) (y.regs Reg.level) = 0 + then 0 else 1) ∧ y.regs Reg.invalid = 0 + have hi : I x := by + refine ⟨hx, rfl, by omega, ?_, ?_, ?_, ?_, ?_, hinvalid⟩ + all_goals simp [hlevel, hpow, hcode, hstars, hpop, hseen, lookupCompletion] + have hb (y : Data registers) (hy : I y) + (hg : (Cond.lt Reg.level Reg.levels).Holds y) : + ∃ z, ExecWithin w lookupDigit y z 16 ∧ I z ∧ + L - z.regs Reg.level < L - y.regs Reg.level := by + obtain ⟨hp, hm, hle, hpower, hc, hs, hf, hv, hinv⟩ := hy + have hk : y.regs Reg.level < L := by simpa only [Cond.holds_lt, hp.levels] using hg + have hseenle : (if Nat.count (fun i => raw i = 9) (y.regs Reg.level) = 0 + then 0 else 1) ≤ 1 := by split <;> omega + have horder : raw (y.regs Reg.level) = 10 → + (if Nat.count (fun i => raw i = 9) (y.regs Reg.level) = 0 then 0 else 1) = 0 := by + intro hstar + have hn := rawCubeDigit_no_fixed_before_star hπ hk hstar + have hz : Nat.count (fun i => raw i = 9) (y.regs Reg.level) = 0 := + Nat.count_of_forall_not (fun i hi hh => hn ⟨i, hi, hh⟩) + rw [hz] + rfl + obtain ⟨z, hz, hzm, hzl, hzp, hzc, hzs, hzf, hzv, hzi, hframe⟩ := + exec_lookupDigit y hk (rawCubeDigit_le_ten π _) (Nat.count_le _) + (Nat.count_le _) (lookupCompletion_lt (fun i _ => rawCubeDigit_le_ten π i)) + hseenle horder hp.cube (by rw [hm]; exact hread _ hk) rfl hs hf hc hv hinv + hpower hp.nil hp.one hp.nine hp.ten hfit + have hpz : LookupParameters L C z := + ⟨(hframe _ (by decide)).trans hp.levels, (hframe _ (by decide)).trans hp.cube, + (hframe _ (by decide)).trans hp.nil, (hframe _ (by decide)).trans hp.one, + (hframe _ (by decide)).trans hp.nine, (hframe _ (by decide)).trans hp.ten⟩ + refine ⟨z, hz, ⟨hpz, hzm.trans hm, by omega, ?_, ?_, ?_, ?_, ?_, hzi⟩, by omega⟩ + · simpa only [hzl] using hzp + · simpa only [hzl, lookupCompletion] using hzc + · simpa only [hzl, Nat.count_succ] using hzs + · simpa only [hzl, Nat.count_succ] using hzf + · rw [hzl, hzv, Nat.count_succ] + by_cases hd : raw (y.regs Reg.level) = 9 + all_goals dsimp only [raw] at hd ⊢; simp [hd] + obtain ⟨y, hy, hIy, hstop⟩ := ExecWithin.loop_invariant I + (fun y => L - y.regs Reg.level) hb hi + obtain ⟨hp, hm, hle, hpower, hc, hs, hf, _, hinv⟩ := hIy + have hdone : y.regs Reg.level = L := by + simp only [Cond.holds_lt, hp.levels, not_lt] at hstop + omega + refine ⟨y, ?_, hm, hp, hdone, ?_, ?_, ?_, ?_, hinv, + fun i hi => hy.regs_eq (lookupLoop_preserves i hi)⟩ + · simpa only [hlevel, Nat.sub_zero, Nat.mul_comm] using hy + · simpa only [hdone] using hpower + · simpa only [hdone, raw, lookupCompletion_rawCubeDigit] using hc + · simpa only [hdone, raw, count_rawCubeDigit_stars] using hs + · simpa only [hdone, raw, count_rawCubeDigit_population] using hf + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/LookupStep.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/LookupStep.lean new file mode 100644 index 0000000000..c1875f1461 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/LookupStep.lean @@ -0,0 +1,110 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Program + +/-! +# Actual cube-digit lookup step + +The native scan reads a real cube digit, checks its alphabet and order, and updates +the completed-leaf code and star/P0 counts. The step theorem consumes ordinary scalar +and memory readback, with all intermediate fits derived from one address/depth envelope. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Cslib.WordRAM + +/-- Registers modified by the actual lookup digit scan. -/ +@[expose] def LookupLocal (i : Fin registers) : Prop := + i = Reg.address ∨ i = Reg.digit ∨ i = Reg.invalid ∨ i = Reg.fixedSeen ∨ + i = Reg.stars ∨ i = Reg.population ∨ i = Reg.temporary ∨ i = Reg.completion ∨ + i = Reg.power ∨ i = Reg.level + +instance (i : Fin registers) : Decidable (LookupLocal i) := + inferInstanceAs (Decidable (i = Reg.address ∨ i = Reg.digit ∨ i = Reg.invalid ∨ + i = Reg.fixedSeen ∨ i = Reg.stars ∨ i = Reg.population ∨ i = Reg.temporary ∨ + i = Reg.completion ∨ i = Reg.power ∨ i = Reg.level)) + +private theorem lookupDigit_preserves (i : Fin registers) : + ¬LookupLocal i → lookupDigit.Preserves i := by decide +revert + +/-- The real scan preserves a valid prefix and charges both failed branch instructions. -/ +theorem exec_lookupDigit {w L k C d s f c v : ℕ} (x : Data registers) + (hk : k < L) (hd : d ≤ 10) (hs : s ≤ k) (hf : f ≤ k) + (hc : c < 10 ^ k) (_hv : v ≤ 1) (horder : d = 10 → v = 0) + (hC : x.regs Reg.cube = C) (hread : x.mem (C + k) = d) + (hlevel : x.regs Reg.level = k) (hstars : x.regs Reg.stars = s) + (hpop : x.regs Reg.population = f) (hcode : x.regs Reg.completion = c) + (hseen : x.regs Reg.fixedSeen = v) (hinvalid : x.regs Reg.invalid = 0) + (hpow : x.regs Reg.power = 10 ^ k) (h0 : x.regs Reg.nil = 0) + (h1 : x.regs Reg.one = 1) (h9 : x.regs Reg.nine = 9) + (h10 : x.regs Reg.ten = 10) + (hfit : Fits w (C + 10 ^ L + L + 20)) : + ∃ y, ExecWithin w lookupDigit x y 16 ∧ y.mem = x.mem ∧ + y.regs Reg.level = k + 1 ∧ y.regs Reg.power = 10 ^ (k + 1) ∧ + y.regs Reg.completion = c + (if d = 10 then 9 else d) * 10 ^ k ∧ + y.regs Reg.stars = s + (if d = 10 then 1 else 0) ∧ + y.regs Reg.population = f + (if d = 9 ∨ d = 10 then 1 else 0) ∧ + y.regs Reg.fixedSeen = (if d = 9 then 1 else v) ∧ y.regs Reg.invalid = 0 ∧ + (∀ i, ¬LookupLocal i → y.regs i = x.regs i) := by + let digit := if d = 10 then 9 else d + have hdn : digit ≤ 9 := by dsimp only [digit]; split <;> omega + have hpowle : 10 ^ (k + 1) ≤ 10 ^ L := + Nat.pow_le_pow_right (by decide) (Nat.succ_le_of_lt hk) + have hcnext : c + digit * 10 ^ k < 10 ^ (k + 1) := by + rw [pow_succ] + have := Nat.mul_le_mul_right (10 ^ k) hdn + omega + have hfa : Fits w (C + k) := hfit.of_le (by omega) + have hfl : Fits w (k + 1) := hfit.of_le (by omega) + have hfs : Fits w (s + 1) := hfit.of_le (by omega) + have hff : Fits w (f + 1) := hfit.of_le (by omega) + have hf0 : Fits w 0 := hfit.of_le (Nat.zero_le _) + have hf1 : Fits w 1 := hfit.of_le (by omega) + have hfm : Fits w (digit * 10 ^ k) := hfit.of_le (by omega) + have hfc : Fits w (c + digit * 10 ^ k) := hfit.of_le (by omega) + have hfp : Fits w (10 ^ k * 10) := by + rw [← pow_succ] + exact hfit.of_le (by omega) + let loaded := (x.set Reg.address (C + k)).set Reg.digit d + let checked := loaded.set Reg.temporary (x.regs Reg.temporary) + let starred := (((checked.set Reg.temporary (x.regs Reg.temporary)).set + Reg.stars (s + 1)).set Reg.population (f + 1)).set Reg.digit 9 + let counted := if d = 10 then starred + else if d = 9 then (checked.set Reg.fixedSeen 1).set Reg.population (f + 1) + else checked.set Reg.temporary (x.regs Reg.temporary) + let y := (((counted.set Reg.temporary (digit * 10 ^ k)).set + Reg.completion (c + digit * 10 ^ k)).set Reg.power (10 ^ k * 10)).set Reg.level (k + 1) + have he : ExecWithin w lookupDigit x y 16 := by + by_cases hd10 : d = 10 <;> by_cases hd9 : d = 9 + all_goals + try omega + all_goals + simp +decide only [digit, hd10, hd9, ite_true, ite_false] at hfm hfc + have hn10 : ¬10 < d := by omega + have hv0 : d = 10 → ¬0 < v := by intro h; rw [horder h]; omega + ram_eval [lookupDigit, y, counted, starred, checked, loaded, digit, hd10, hd9, hn10, + hv0, horder, hC, hread, hlevel, hstars, hpop, hcode, hseen, hinvalid, hpow, + h0, h1, h9, h10, hfa, hfl, hfs, hff, hf0, hf1, hfm, hfc, hfp, + Reg.address, Reg.digit, Reg.invalid, Reg.fixedSeen, Reg.stars, Reg.population, + Reg.temporary, Reg.completion, Reg.power, Reg.level, Reg.cube, Reg.nil, + Reg.one, Reg.nine, Reg.ten, Fin.mk.injEq] + refine ⟨y, he, by dsimp only [y, counted]; split <;> first | rfl | (split <;> rfl), + ?_, ?_, ?_, ?_, ?_, ?_, ?_, + fun i hi => he.regs_eq (lookupDigit_preserves i hi)⟩ + all_goals + by_cases hd10 : d = 10 <;> by_cases hd9 : d = 9 + all_goals simp_all [y, counted, starred, checked, loaded, digit, + Reg.address, Reg.digit, Reg.invalid, Reg.fixedSeen, Reg.stars, Reg.population, + Reg.temporary, Reg.completion, Reg.power, Reg.level, pow_succ] + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Program.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Program.lean new file mode 100644 index 0000000000..229656cb47 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Program.lean @@ -0,0 +1,298 @@ +/- +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.Power +public import Complexity.Computability.WordRAM.Signed.Arithmetic + +/-! +# Native shared box geometry and compact value tables + +The geometry stage assigns every slot of a shared `(m-t+1) * 10^L` directory, +including invalid slots. It emits only valid canonical boxes into a compact three-word +catalogue: completed leaf code, number of stars, and highest-star place value. +The catalogue is ordered by star count. Each tile writes one signed value per catalogue +entry, reading only values for smaller star counts. No scratch region must start zero. + +Level zero is the least significant decimal digit, as in the existing native encodings; +the P0 digit is nine. The per-tile stage does not rebuild or clear the geometry. +This is an original representation alternative to the trie in [AlmanWilliams2026, Section 4.3]. +Its one-time geometry charge and allocation must remain separate from per-tile work. +Definitions here are code only; execution and resource proofs belong to the stage modules. + +## Main definitions + +* `BoxTable.geometry`: compute the shared directory and compact catalogue. +* `BoxTable.tile`: compute the compact value table from two encoded leaf arrays. +* `BoxTable.lookup`: read a cube's actual stored value after checking its raw digit form. +* `BoxTable.program`: ordinary initialized-input constructor for one tile. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Cslib.WordRAM + +/-- A fixed bank containing the existing nine-register signed-arithmetic workspace. -/ +abbrev registers : ℕ := 64 + +namespace Reg + +/-- Original depth. -/ +abbrev levels : Fin registers := 9 +/-- Original inner-level count. -/ +abbrev inner : Fin registers := 10 +/-- Original order threshold. -/ +abbrev threshold : Fin registers := 11 +/-- Computed maximum combined P0/star count. -/ +abbrev height : Fin registers := 12 +/-- Computed encoding length, ten to the depth. -/ +abbrev span : Fin registers := 13 +/-- Shared directory base. -/ +abbrev directory : Fin registers := 14 +/-- Three-word catalogue base. -/ +abbrev records : Fin registers := 15 +/-- Compact signed value-table base. -/ +abbrev values : Fin registers := 16 +/-- Left canonical signed encoding-array base. -/ +abbrev arrayA : Fin registers := 17 +/-- Right canonical signed encoding-array base. -/ +abbrev arrayB : Fin registers := 18 +/-- Number of directory slots. -/ +abbrev slots : Fin registers := 19 +/-- Current directory slot. -/ +abbrev slot : Fin registers := 20 +/-- Number of emitted catalogue records. -/ +abbrev count : Fin registers := 21 +/-- Star count of the current record. -/ +abbrev stars : Fin registers := 22 +/-- Completed leaf code of the current record. -/ +abbrev completion : Fin registers := 23 +/-- Unprocessed decimal suffix. -/ +abbrev suffix : Fin registers := 24 +/-- Current level in a digit scan. -/ +abbrev level : Fin registers := 25 +/-- P0 population of the processed prefix. -/ +abbrev population : Fin registers := 26 +/-- Place value of the current level. -/ +abbrev power : Fin registers := 27 +/-- Place value of the highest star, or zero when there are no stars. -/ +abbrev starPower : Fin registers := 28 +/-- Raw digit temporary. -/ +abbrev digit : Fin registers := 29 +/-- Load/store address temporary. -/ +abbrev address : Fin registers := 30 +/-- Scalar arithmetic temporary. -/ +abbrev temporary : Fin registers := 31 +/-- Constant one. -/ +abbrev one : Fin registers := 32 +/-- Constant ten. -/ +abbrev ten : Fin registers := 33 +/-- Constant nine, the P0 digit. -/ +abbrev nine : Fin registers := 34 +/-- Constant three, the catalogue record width. -/ +abbrev three : Fin registers := 35 +/-- Current compact record index. -/ +abbrev current : Fin registers := 36 +/-- Canonical signed partial sum. -/ +abbrev accumulator : Fin registers := 37 +/-- Current replacement term, from zero through nine. -/ +abbrev term : Fin registers := 38 +/-- Completed leaf code after replacing the highest star. -/ +abbrev childCode : Fin registers := 39 +/-- Child's shared directory slot. -/ +abbrev childSlot : Fin registers := 40 +/-- Child's compact value-table index, initially stored with offset one. -/ +abbrev childRank : Fin registers := 41 +/-- Constant zero outside the signed workspace. -/ +abbrev nil : Fin registers := 42 +/-- Input pointer to a raw cube's digits for lookup. -/ +abbrev cube : Fin registers := 43 +/-- Lookup-invalid flag. -/ +abbrev invalid : Fin registers := 44 +/-- A fixed P0 term has already appeared below this level. -/ +abbrev fixedSeen : Fin registers := 45 +/-- Lookup-found flag. -/ +abbrev found : Fin registers := 46 +/-- Lookup's canonical signed returned value. -/ +abbrev answer : Fin registers := 47 + +end Reg + +open Reg + +/-- Initialize every reused scalar constant explicitly. -/ +@[expose] def constants : Code .standard registers := ram[ + nil ← #0; one ← #1; ten ← #10; nine ← #9; three ← #3 ] + +/-- Reuse the existing power routine without introducing a second exponentiation loop. -/ +@[expose] def powerRegisters : Fin 5 → Fin registers := ![span, level, ten, levels, one] + +/-- Count a P0 digit and remember precisely the requested occurrence's place value. -/ +@[expose] def countDigit : Code .standard registers := ram[ + digit ← suffix % ten; suffix ← suffix / ten; + if digit = nine then [ + population ← population + one; + if population = stars then [ starPower ← power ] else [ temporary ← temporary ] + ] else [ temporary ← temporary ]; + power ← power * ten; level ← level + one ] + +/-- Initialize a scan from the current raw directory slot. -/ +@[expose] def inspectSetup : Code .standard registers := ram[ + stars ← slot / span; completion ← slot % span; suffix ← completion; + level ← #0; population ← #0; power ← #1; starPower ← #0 ] + +/-- Complete one actual digit scan; the loop is over the original depth. -/ +@[expose] def inspect : Code .standard registers := + .seq inspectSetup (.loop (.lt level levels) countDigit) + +/-- Write one compact record and its offset-one directory entry. -/ +@[expose] def emit : Code .standard registers := ram[ + temporary ← count + one; *address ← temporary; + address ← count * three; address ← records + address; *address ← completion; + address ← address + one; *address ← stars; + address ← address + one; *address ← starPower; + count ← count + one ] + +/-- Assign one directory slot and emit a compact record when both tests succeed. -/ +@[expose] def writeSlot : Code .standard registers := ram[ + address ← directory + slot; *address ← nil; + if height < population then [ temporary ← temporary ] else [ + if population < stars then [ temporary ← temporary ] else [ ⟪emit⟫ ] ]; + slot ← slot + one ] + +/-- Every directory slot is assigned, including slots rejected by either population test. -/ +@[expose] def catalogueStep : Code .standard registers := .seq inspect writeSlot + +/-- Compute the slot range and initialize the actual compact count. -/ +@[expose] def geometrySetup : Code .standard registers := ram[ + height ← inner - threshold; slots ← height + one; slots ← slots * span; + records ← directory + slots; slot ← #0; count ← #0 ] + +/-- Place the value table immediately after the actual compact records. -/ +@[expose] def geometryFinish : Code .standard registers := ram[ + temporary ← count * three; values ← records + temporary ] + +/-- Compute the shared geometry, returning its actual compact count and value-table base. -/ +@[expose] def geometry : Code .standard registers := + .seq constants <| .seq (Power.program.rename powerRegisters) <| + .seq geometrySetup <| .seq (.loop (.lt slot slots) catalogueStep) geometryFinish + +/-- Load the three actual catalogue words. -/ +@[expose] def loadRecord : Code .standard registers := ram[ + address ← current * three; address ← records + address; completion ← *address; + address ← address + one; stars ← *address; + address ← address + one; starPower ← *address ] + +/-- Read both encoded leaf operands from their actual array positions. -/ +@[expose] def leafLoad : Code .standard registers := ram[ + address ← arrayA + completion; Signed.left ← *address; + address ← arrayB + completion; Signed.right ← *address ] + +/-- Retain the actual signed arithmetic result outside its scratch bank. -/ +@[expose] def leafFinish : Code .standard registers := ram[ accumulator ← Signed.result ] + +/-- Multiply the two encoded words of a fully fixed cube. -/ +@[expose] def leafProduct : Code .standard registers := + .seq leafLoad (.seq Signed.multiply leafFinish) + +/-- Compute a child's directory index and load its already written signed value. -/ +@[expose] def childLoad : Code .standard registers := ram[ + temporary ← nine - term; temporary ← temporary * starPower; + childCode ← completion - temporary; + childSlot ← stars - one; childSlot ← childSlot * span; childSlot ← childSlot + childCode; + address ← directory + childSlot; childRank ← *address; childRank ← childRank - one; + address ← values + childRank; Signed.right ← *address; Signed.left ← accumulator ] + +/-- Save the signed partial sum and advance the actual ten-child loop. -/ +@[expose] def childFinish : Code .standard registers := ram[ + accumulator ← Signed.result; term ← term + one ] + +/-- Compute one child's actual directory index, read its stored value, and add it. -/ +@[expose] def addChild : Code .standard registers := + .seq childLoad (.seq Signed.add childFinish) + +/-- Reset the accumulator and term counter before the ten-child loop. -/ +@[expose] def childrenStart : Code .standard registers := ram[ + accumulator ← #0; term ← #0 ] + +/-- Accumulate all ten earlier child values. -/ +@[expose] def children : Code .standard registers := + .seq childrenStart (.loop (.lt term ten) addChild) + +/-- Evaluate a leaf product or the sum of its ten earlier children. -/ +@[expose] def tileValue : Code .standard registers := + .branch (.eq stars nil) leafProduct children + +/-- Store the completed signed value and advance its compact index. -/ +@[expose] def tileStore : Code .standard registers := ram[ + address ← values + current; *address ← accumulator; current ← current + one ] + +/-- Evaluate one compact box and store it before advancing the compact index. -/ +@[expose] def tileStep : Code .standard registers := + .seq loadRecord (.seq tileValue tileStore) + +/-- Initialize every per-tile scalar that is read before being written. -/ +@[expose] def tileSetup : Code .standard registers := ram[ ⟪constants⟫; current ← #0 ] + +/-- Fill exactly one compact value table, reusing the shared geometry. -/ +@[expose] def tile : Code .standard registers := + .seq tileSetup (.loop (.lt current count) tileStep) + +/-- Read one cube digit, rejecting out-of-alphabet and star-after-fixed-P0 forms. -/ +@[expose] def lookupDigit : Code .standard registers := ram[ + address ← cube + level; digit ← *address; + if ten < digit then [ invalid ← #1; digit ← #0 ] else [ temporary ← temporary ]; + if digit = ten then [ + if nil < fixedSeen then [ invalid ← #1 ] else [ temporary ← temporary ]; + stars ← stars + one; population ← population + one; digit ← nine + ] else [ + if digit = nine then [ fixedSeen ← #1; population ← population + one ] + else [ temporary ← temporary ] ]; + temporary ← digit * power; completion ← completion + temporary; + power ← power * ten; level ← level + one ] + +/-- Initialize the raw lookup prefix and both returned flags explicitly. -/ +@[expose] def lookupSetup : Code .standard registers := ram[ + ⟪constants⟫; level ← #0; stars ← #0; population ← #0; fixedSeen ← #0; + invalid ← #0; completion ← #0; power ← #1; found ← #0; answer ← #0 ] + +/-- Validate the completed population and read the actual compact-table word. -/ +@[expose] def lookupFinish : Code .standard registers := ram[ + if height < population then [ invalid ← #1 ] else [ temporary ← temporary ]; + if invalid = nil then [ + childSlot ← stars * span; childSlot ← childSlot + completion; + address ← directory + childSlot; childRank ← *address; + if childRank = nil then [ temporary ← temporary ] else [ + childRank ← childRank - one; address ← values + childRank; + answer ← *address; found ← #1 ] + ] else [ temporary ← temporary ] ] + +/-- Read the actual table entry for a valid canonical cube; return raw found and signed answer. -/ +@[expose] def lookup : Code .standard registers := + .seq lookupSetup (.seq (.loop (.lt level levels) lookupDigit) lookupFinish) + +/-- Read the three original scalar input headers. -/ +@[expose] def inputHeaders : Code .standard registers := ram[ + address ← #1; levels ← *address; address ← #2; inner ← *address; + address ← #3; threshold ← *address ] + +/-- Locate both leaf arrays and the shared directory after the original input. -/ +@[expose] def inputPointers : Code .standard registers := ram[ + arrayA ← #4; arrayB ← arrayA + span; directory ← arrayB + span ] + +/-- Original scalar headers followed by both leaf arrays; address zero is State.init's header. -/ +@[expose] def loadInput : Code .standard registers := + .seq inputHeaders (.seq constants (.seq (Power.program.rename powerRegisters) inputPointers)) + +/-- Complete one-tile constructor, retaining separate shared-geometry and per-tile routines. -/ +@[expose] def program : Code .standard registers := ram[ + ⟪loadInput⟫; ⟪geometry⟫; ⟪tile⟫ ] + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Tile.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Tile.lean new file mode 100644 index 0000000000..63c2761a1e --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Tile.lean @@ -0,0 +1,419 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.TileChildren +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Values +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Geometry +import Mathlib.Algebra.BigOperators.Fin + +/-! +# Complete native compact box-value table + +The native e-major loop writes one signed value per computed catalogue record. Its +children have smaller actual compact ranks, so no value-table clearing or assumed +table construction is used. Original encoding-array bounds cover all signed partials. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Cslib.WordRAM Finset Cslib.Algorithms.MatrixMultiplication.Schonhage +open scoped BigOperators + +private theorem exists_count_rank (p : ℕ → Prop) [DecidablePred p] {S j : ℕ} + (hj : j < Nat.count p S) : ∃ s < S, p s ∧ Nat.count p s = j := by + induction S with + | zero => simp at hj + | succ S ih => + by_cases hp : p S + · rw [Nat.count_succ_eq_succ_count hp] at hj + by_cases hlt : j < Nat.count p S + · obtain ⟨s, hs, hps, hr⟩ := ih hlt + exact ⟨s, by omega, hps, hr⟩ + · exact ⟨S, by omega, hp, by omega⟩ + · rw [Nat.count_succ_eq_count hp] at hj + obtain ⟨s, hs, hps, hr⟩ := ih hj + exact ⟨s, by omega, hps, hr⟩ + +private theorem child_stars {L H s : ℕ} (hv : Eligible L H s) + (he : 0 < recordStars L s) (d : Fin 10) : + recordStars L (childSlot L s d) = recordStars L s - 1 := by + simpa only [childSlot] using recordStars_slot (recordStars L s - 1) + (⟨childCode L s d, childCode_lt hv he d⟩ : Fin (10 ^ L)) + +private theorem slotValue_children {L H s : ℕ} (hv : Eligible L H s) + (he : 0 < recordStars L s) (a b : Leaf L → ℤ) : + slotValue a b s = ∑ d : Fin 10, slotValue a b (childSlot L s d) := by + rw [slotValue, boxValue_eq_sum_childSlots hv he] + exact sum_congr rfl fun d _ => by rw [slotValue, child_stars hv he] + +/-- Registers that may change while constructing one tile's compact values. -/ +@[expose] def TileLocal (i : Fin registers) : Prop := + RecordLocal i ∨ ProductLocal i ∨ ChildLocal i ∨ i = Reg.current ∨ + i = Reg.nil ∨ i = Reg.one ∨ i = Reg.ten ∨ i = Reg.nine ∨ i = Reg.three + +instance (i : Fin registers) : Decidable (TileLocal i) := + inferInstanceAs (Decidable (RecordLocal i ∨ ProductLocal i ∨ ChildLocal i ∨ + i = Reg.current ∨ i = Reg.nil ∨ i = Reg.one ∨ i = Reg.ten ∨ + i = Reg.nine ∨ i = Reg.three)) + +private theorem tile_preserves (i : Fin registers) : + ¬TileLocal i → tile.Preserves i := by decide +revert + +private theorem tileValue_preserves (i : Fin registers) : + ¬(ProductLocal i ∨ ChildLocal i) → tileValue.Preserves i := by decide +revert + +/-- Evaluate one actual descriptor using the stored earlier children or two actual leaf words. -/ +theorem exec_tileValue {w L H D V AA BB A B s : ℕ} (x : Data registers) + (a b : Leaf L → ℤ) (hv : Eligible L H s) + (ha : ∀ τ, (a τ).natAbs ≤ A) (hb : ∀ τ, (b τ).natAbs ≤ B) + (hD : x.regs Reg.directory = D) (hV : x.regs Reg.values = V) + (hAA : x.regs Reg.arrayA = AA) (hBB : x.regs Reg.arrayB = BB) + (hc : x.regs Reg.completion = recordCode L s) + (he : x.regs Reg.stars = recordStars L s) + (hT : x.regs Reg.span = 10 ^ L) (hp : x.regs Reg.starPower = recordStride L s) + (h0 : x.regs Reg.nil = 0) (h9 : x.regs Reg.nine = 9) + (h1 : x.regs Reg.one = 1) (h10 : x.regs Reg.ten = 10) + (hleft : x.mem (AA + recordCode L s) = Signed.encode (a (completionAt L s))) + (hright : x.mem (BB + recordCode L s) = Signed.encode (b (completionAt L s))) + (hrank : 0 < recordStars L s → ∀ d : Fin 10, + x.mem (D + childSlot L s d) = Nat.count (Eligible L H) (childSlot L s d) + 1) + (hvalue : 0 < recordStars L s → ∀ d : Fin 10, x.mem + (V + Nat.count (Eligible L H) (childSlot L s d)) = + Signed.encode (slotValue a b (childSlot L s d))) + (hfit : Fits (w + 2) + (D + V + AA + BB + 20 * ((H + 1) * 10 ^ L) + 20 * 10 ^ L + 30)) + (hsigned : GenericRAM.Signed.Fits w (A + B + 10 ^ L * (A * B) : ℕ)) : + ∃ y, ExecWithin (w + 2) tileValue x y 316 ∧ + y.regs Reg.accumulator = Signed.encode (slotValue a b s) ∧ y.mem = x.mem ∧ + (∀ i, ¬(ProductLocal i ∨ ChildLocal i) → y.regs i = x.regs i) := by + have hTpos : 0 < 10 ^ L := by positivity + have hcode : recordCode L s < 10 ^ L := Nat.mod_lt _ hTpos + have heL : recordStars L s ≤ L := hv.1.trans (population_le _ _) + have hAB : A * B ≤ 10 ^ L * (A * B) := by + exact Nat.le_mul_of_pos_left _ hTpos + by_cases he0 : recordStars L s = 0 + · have ha0 : GenericRAM.Signed.Fits w (a (completionAt L s)) := + hsigned.of_natAbs_le ((ha _).trans (by omega)) + have hb0 : GenericRAM.Signed.Fits w (b (completionAt L s)) := + hsigned.of_natAbs_le ((hb _).trans (by omega)) + have hp0 : GenericRAM.Signed.Fits w + (a (completionAt L s) * b (completionAt L s)) := by + apply hsigned.of_natAbs_le + rw [Int.natAbs_mul] + exact (Nat.mul_le_mul (ha _) (hb _)).trans (hAB.trans (by omega)) + obtain ⟨y, hy, hyr, hym, _⟩ := exec_leafProduct ha0 hb0 hp0 x + (by simpa only [hAA, hc] using hleft) (by simpa only [hBB, hc] using hright) + (hfit.of_le (by rw [hAA, hc]; omega)) (hfit.of_le (by rw [hBB, hc]; omega)) + have hy' : ExecWithin (w + 2) tileValue x y 316 := + (hy.branch_pos (by simp [Cond.holds_eq, he, h0, he0])).mono (by decide) + refine ⟨y, hy', ?_, hym, fun i hi => hy'.regs_eq (tileValue_preserves i hi)⟩ + simpa only [slotValue, he0, boxValue, starsToP0_slotCube] using hyr + · have hepos : 0 < recordStars L s := Nat.pos_of_ne_zero he0 + let val (d : ℕ) := slotValue a b (childSlot L s ⟨d % 10, Nat.mod_lt _ (by decide)⟩) + let rank (d : ℕ) := Nat.count (Eligible L H) + (childSlot L s ⟨d % 10, Nat.mod_lt _ (by decide)⟩) + let C := 10 ^ (recordStars L s - 1) * (A * B) + have hC : 10 * C ≤ 10 ^ L * (A * B) := by + calc + _ = 10 ^ (recordStars L s - 1 + 1) * (A * B) := by + dsimp only [C] + rw [pow_succ] + ring + _ = 10 ^ recordStars L s * (A * B) := by rw [Nat.sub_add_cancel hepos] + _ ≤ _ := Nat.mul_le_mul_right _ (Nat.pow_le_pow_right (by decide) heL) + let u := (x.set Reg.accumulator 0).set Reg.term 0 + have hf0 : Fits (w + 2) 0 := hfit.of_le (Nat.zero_le _) + have hstart : ExecWithin (w + 2) childrenStart x u 2 := by + ram_eval [childrenStart, u, hf0, Reg.accumulator, Reg.term, Fin.mk.injEq] + have uf (i : Fin registers) (hi : i ≠ Reg.accumulator) (ht : i ≠ Reg.term) : + u.regs i = x.regs i := by simp [u, hi, ht] + have hrange (d : ℕ) (hd : d < 10) : rank d ≤ (H + 1) * 10 ^ L := by + have hslt : childSlot L s ⟨d % 10, Nat.mod_lt _ (by decide)⟩ < (H + 1) * 10 ^ L := by + have hh := eligible_childSlot hv hepos ⟨d % 10, Nat.mod_lt _ (by decide)⟩ + have hc' := childCode_lt hv hepos ⟨d % 10, Nat.mod_lt _ (by decide)⟩ + have hstar : recordStars L s ≤ H := hv.1.trans hv.2 + dsimp only [childSlot] + have hm := Nat.mul_le_mul_right (10 ^ L) (show recordStars L s - 1 + 1 ≤ H + 1 by omega) + rw [Nat.add_one_mul] at hm + omega + exact (Nat.count_le _).trans hslt.le + obtain ⟨y, hy, hyd, hya, hym, _⟩ := exec_childLoop (R := (H + 1) * 10 ^ L) (C := C) u val rank + ((uf _ (by decide) (by decide)).trans hD) ((uf _ (by decide) (by decide)).trans hV) + ((uf _ (by decide) (by decide)).trans hc) ((uf _ (by decide) (by decide)).trans he) + ((uf _ (by decide) (by decide)).trans hT) hTpos + ((uf _ (by decide) (by decide)).trans hp) (by simp [u]) + (by simp [u, Reg.accumulator, Reg.term]) + ((uf _ (by decide) (by decide)).trans h9) ((uf _ (by decide) (by decide)).trans h1) + ((uf _ (by decide) (by decide)).trans h10) + (fun d hd => by + simpa only [u, Data.set_mem, childSlot, childCode, rank, Nat.mod_eq_of_lt hd] + using hrank hepos ⟨d, hd⟩) + (fun d hd => by + simpa only [u, Data.set_mem, val, rank, Nat.mod_eq_of_lt hd] + using hvalue hepos (⟨d, hd⟩ : Fin 10)) hrange + (fun d _ => by + dsimp only [val, slotValue] + rw [child_stars hv hepos] + exact natAbs_boxValue_le a b ha hb _ _) + (hsigned.of_natAbs_le (by + simpa only [Int.natAbs_natCast] using hC.trans + (show 10 ^ L * (A * B) ≤ A + B + 10 ^ L * (A * B) by omega))) + (hfit.of_le (by + have hc' := hcode + have hp' := starStride_le (recordCode L s) (recordStars L s) L + have heH : recordStars L s ≤ H := hv.1.trans hv.2 + have hes : recordStars L s * 10 ^ L ≤ (H + 1) * 10 ^ L := + Nat.mul_le_mul_right _ (by omega) + dsimp only [recordStride] at * + omega)) + have hy' : ExecWithin (w + 2) tileValue x y 316 := + ((hstart.seq hy).branch_neg (by simp [Cond.holds_eq, he, h0, he0])).mono (by decide) + refine ⟨y, hy', ?_, hym, fun i hi => hy'.regs_eq (tileValue_preserves i hi)⟩ + have hsum : (∑ d ∈ range 10, val d) = + ∑ d : Fin 10, slotValue a b (childSlot L s d) := by + rw [← Fin.sum_univ_eq_sum_range] + exact sum_congr rfl fun d _ => by simp [val, Nat.mod_eq_of_lt d.isLt] + rw [slotValue_children hv hepos a b] + exact hya.trans (congrArg Signed.encode hsum) + +/-- Load, evaluate and store one compact record with all native control and address work. -/ +theorem exec_tileStep {w L H D R V AA BB A B s : ℕ} (x : Data registers) + (a b : Leaf L → ℤ) (hv : Eligible L H s) (hs : s < (H + 1) * 10 ^ L) + (ha : ∀ τ, (a τ).natAbs ≤ A) (hb : ∀ τ, (b τ).natAbs ≤ B) + (hx : CatalogueParameters L H D R x) + (hV : x.regs Reg.values = V) (hAA : x.regs Reg.arrayA = AA) + (hBB : x.regs Reg.arrayB = BB) + (hj : x.regs Reg.current = Nat.count (Eligible L H) s) + (hcode : x.mem (R + 3 * Nat.count (Eligible L H) s) = recordCode L s) + (hstars : x.mem (R + 3 * Nat.count (Eligible L H) s + 1) = recordStars L s) + (hstride : x.mem (R + 3 * Nat.count (Eligible L H) s + 2) = recordStride L s) + (hleft : x.mem (AA + recordCode L s) = Signed.encode (a (completionAt L s))) + (hright : x.mem (BB + recordCode L s) = Signed.encode (b (completionAt L s))) + (hrank : 0 < recordStars L s → ∀ d : Fin 10, + x.mem (D + childSlot L s d) = Nat.count (Eligible L H) (childSlot L s d) + 1) + (hvalue : 0 < recordStars L s → ∀ d : Fin 10, + x.mem (V + Nat.count (Eligible L H) (childSlot L s d)) = + Signed.encode (slotValue a b (childSlot L s d))) + (hfit : Fits (w + 2) + (D + R + V + AA + BB + 20 * ((H + 1) * 10 ^ L) + 20 * 10 ^ L + 30)) + (hsigned : GenericRAM.Signed.Fits w (A + B + 10 ^ L * (A * B) : ℕ)) : + ∃ y, ExecWithin (w + 2) tileStep x y 326 ∧ + y.regs Reg.current = Nat.count (Eligible L H) s + 1 ∧ + y.mem = Function.update x.mem (V + Nat.count (Eligible L H) s) + (Signed.encode (slotValue a b s)) := by + have hjlt : Nat.count (Eligible L H) s < (H + 1) * 10 ^ L := + (Nat.count_le _).trans_lt hs + obtain ⟨u, hu, uc, ue, up, um, uf⟩ := exec_loadRecord x hx.records hj hx.one hx.three + (by simpa only [Nat.mul_comm] using hcode) + (by simpa only [Nat.mul_comm] using hstars) + (by simpa only [Nat.mul_comm] using hstride) (hfit.of_le (by omega)) + obtain ⟨v, hvexec, vacc, vm, vf⟩ := exec_tileValue u a b hv ha hb + ((uf _ (by decide)).trans hx.directory) ((uf _ (by decide)).trans hV) + ((uf _ (by decide)).trans hAA) ((uf _ (by decide)).trans hBB) + uc ue ((uf _ (by decide)).trans hx.span) up + ((uf _ (by decide)).trans hx.nil) ((uf _ (by decide)).trans hx.nine) + ((uf _ (by decide)).trans hx.one) ((uf _ (by decide)).trans hx.ten) + (by simpa only [um] using hleft) (by simpa only [um] using hright) + (fun he d => by simpa only [um] using hrank he d) + (fun he d => by simpa only [um] using hvalue he d) + (hfit.of_le (by omega)) hsigned + have vV : v.regs Reg.values = V := + (vf _ (by decide)).trans ((uf _ (by decide)).trans hV) + have vj : v.regs Reg.current = Nat.count (Eligible L H) s := + (vf _ (by decide)).trans ((uf _ (by decide)).trans hj) + have v1 : v.regs Reg.one = 1 := + (vf _ (by decide)).trans ((uf _ (by decide)).trans hx.one) + have haddr : Fits (w + 2) (V + Nat.count (Eligible L H) s) := hfit.of_le (by omega) + have hinc : Fits (w + 2) (Nat.count (Eligible L H) s + 1) := hfit.of_le (by omega) + let y := ((v.set Reg.address (V + Nat.count (Eligible L H) s)).write + (V + Nat.count (Eligible L H) s) (Signed.encode (slotValue a b s))).set + Reg.current (Nat.count (Eligible L H) s + 1) + have hstore : ExecWithin (w + 2) tileStore v y 3 := by + ram_eval [tileStore, y, vV, vj, v1, vacc, haddr, hinc, + Reg.address, Reg.values, Reg.current, Reg.accumulator, Reg.one, Fin.mk.injEq] + have hy : ExecWithin (w + 2) tileStep x y 326 := hu.seq (hvexec.seq hstore) + exact ⟨y, hy, by simp [y], by simp only [y, Data.set_mem, Data.write_mem, vm, um]⟩ + +/-- The native compact loop computes every eligible slot, preserving the catalogue and inputs. -/ +theorem exec_tileLoop {w L H D R V AA BB A B : ℕ} {μ : ℕ → ℕ} (x : Data registers) + (a b : Leaf L → ℤ) + (ha : ∀ τ, (a τ).natAbs ≤ A) (hb : ∀ τ, (b τ).natAbs ≤ B) + (hx : CatalogueParameters L H D R x) + (hV : x.regs Reg.values = V) (hAA : x.regs Reg.arrayA = AA) + (hBB : x.regs Reg.arrayB = BB) + (hcount : x.regs Reg.count = Nat.count (Eligible L H) ((H + 1) * 10 ^ L)) + (hcurrent : x.regs Reg.current = 0) + (hcat : CataloguePrefix L H D R ((H + 1) * 10 ^ L) μ x.mem) + (hDR : D + (H + 1) * 10 ^ L ≤ R) + (hRV : R + 3 * Nat.count (Eligible L H) ((H + 1) * 10 ^ L) ≤ V) + (hAV : AA + 10 ^ L ≤ V) (hBV : BB + 10 ^ L ≤ V) + (hleft : ∀ c : Fin (10 ^ L), x.mem (AA + c.val) = Signed.encode (a (leafAt c))) + (hright : ∀ c : Fin (10 ^ L), x.mem (BB + c.val) = Signed.encode (b (leafAt c))) + (hfit : Fits (w + 2) + (D + R + V + AA + BB + 20 * ((H + 1) * 10 ^ L) + 20 * 10 ^ L + 30)) + (hsigned : GenericRAM.Signed.Fits w (A + B + 10 ^ L * (A * B) : ℕ)) : + ∃ y, ExecWithin (w + 2) (.loop (.lt Reg.current Reg.count) tileStep) x y + (328 * Nat.count (Eligible L H) ((H + 1) * 10 ^ L) + 2) ∧ + (∀ s < (H + 1) * 10 ^ L, Eligible L H s → + y.mem (V + Nat.count (Eligible L H) s) = Signed.encode (slotValue a b s)) ∧ + (∀ q, ¬(V ≤ q ∧ q < V + Nat.count (Eligible L H) ((H + 1) * 10 ^ L)) → + y.mem q = x.mem q) := by + let S := (H + 1) * 10 ^ L + let K := Nat.count (Eligible L H) S + let I (y : Data registers) : Prop := + CatalogueParameters L H D R y ∧ y.regs Reg.values = V ∧ + y.regs Reg.arrayA = AA ∧ y.regs Reg.arrayB = BB ∧ y.regs Reg.count = K ∧ + y.regs Reg.current ≤ K ∧ + (∀ s < S, Eligible L H s → Nat.count (Eligible L H) s < y.regs Reg.current → + y.mem (V + Nat.count (Eligible L H) s) = Signed.encode (slotValue a b s)) ∧ + (∀ q, ¬(V ≤ q ∧ q < V + y.regs Reg.current) → y.mem q = x.mem q) + have hi : I x := by + refine ⟨hx, hV, hAA, hBB, hcount, by simp [hcurrent], ?_, fun _ _ => rfl⟩ + simp only [hcurrent, not_lt_zero, IsEmpty.forall_iff, implies_true] + have hbody (y : Data registers) (hy : I y) + (hg : (Cond.lt Reg.current Reg.count).Holds y) : + ∃ z, ExecWithin (w + 2) tileStep y z 326 ∧ I z ∧ + K - z.regs Reg.current < K - y.regs Reg.current := by + obtain ⟨yp, yV, yA, yB, yK, yj, yvalues, yframe⟩ := hy + have hjlt : y.regs Reg.current < K := by + simpa only [Cond.holds_lt, yK] using hg + obtain ⟨s, hs, hvs, hsj⟩ := exists_count_rank (Eligible L H) hjlt + have hlow (q : ℕ) (hq : q < V) : y.mem q = x.mem q := yframe q (by omega) + have hsK : Nat.count (Eligible L H) s < K := Nat.count_strict_mono hvs hs + have hrec : R + 3 * Nat.count (Eligible L H) s + 2 < V := by + dsimp only [K] at hsK + omega + have hcode : recordCode L s < 10 ^ L := Nat.mod_lt _ (by positivity) + obtain ⟨z, hz, hzj, hzm⟩ := exec_tileStep y a b hvs hs ha hb yp yV yA yB hsj.symm + ((hlow _ (by omega)).trans (hcat.code s hs hvs)) + ((hlow _ (by omega)).trans (hcat.stars s hs hvs)) + ((hlow _ hrec).trans (hcat.stride s hs hvs)) + ((hlow _ (by omega)).trans (hleft ⟨recordCode L s, hcode⟩)) + ((hlow _ (by omega)).trans (hright ⟨recordCode L s, hcode⟩)) + (fun he d => by + have hchild : childSlot L s d < S := (childSlot_lt hvs he d).trans hs + rw [hlow _ (by dsimp only [S] at hchild; omega), hcat.directory _ hchild, + directoryWord, ite_eq_left (eligible_childSlot hvs he d)]) + (fun he d => yvalues _ ((childSlot_lt hvs he d).trans hs) + (eligible_childSlot hvs he d) ((child_rank_lt hvs he d).trans_eq hsj)) + hfit hsigned + have zregs (i : Fin registers) (h : tileStep.Preserves i) : z.regs i = y.regs i := + hz.regs_eq h + have zp : CatalogueParameters L H D R z := by + constructor + · exact (zregs _ (by decide)).trans yp.levels + · exact (zregs _ (by decide)).trans yp.height + · exact (zregs _ (by decide)).trans yp.span + · exact (zregs _ (by decide)).trans yp.directory + · exact (zregs _ (by decide)).trans yp.records + · exact (zregs _ (by decide)).trans yp.slots + · exact (zregs _ (by decide)).trans yp.one + · exact (zregs _ (by decide)).trans yp.ten + · exact (zregs _ (by decide)).trans yp.nine + · exact (zregs _ (by decide)).trans yp.three + · exact (zregs _ (by decide)).trans yp.nil + refine ⟨z, hz, ⟨zp, (zregs _ (by decide)).trans yV, + (zregs _ (by decide)).trans yA, (zregs _ (by decide)).trans yB, + (zregs _ (by decide)).trans yK, by omega, ?_, ?_⟩, by omega⟩ + · intro i hi hvi hji + rw [hzm] + by_cases hij : Nat.count (Eligible L H) i = Nat.count (Eligible L H) s + · have his : i = s := Nat.count_injective hvi hvs hij + subst i + simp + · rw [Function.update_of_ne (by omega)] + exact yvalues i hi hvi (by omega) + · intro q hq + rw [hzm, Function.update_of_ne (by omega)] + exact yframe q (by omega) + obtain ⟨y, hy, hIy, hstop⟩ := ExecWithin.loop_invariant I + (fun y => K - y.regs Reg.current) hbody hi + obtain ⟨yp, yV, yA, yB, yK, yj, yvalues, yframe⟩ := hIy + have hdone : y.regs Reg.current = K := by + simp only [Cond.holds_lt, yK, not_lt] at hstop + omega + refine ⟨y, ?_, ?_, ?_⟩ + · simpa only [hcurrent, Nat.sub_zero, K, S, Nat.reduceAdd, Nat.mul_comm] using hy + · intro s hs hv + exact yvalues s hs hv ((Nat.count_strict_mono hv hs).trans_eq hdone.symm) + · simpa only [hdone, K, S] using yframe + +/-- Complete one-tile execution, including actual constant/counter setup, with no dirty-memory +restriction. The catalogue and both input arrays lie below the value-table base. -/ +theorem exec_tile {w L H D R V AA BB A B : ℕ} {μ : ℕ → ℕ} (x : Data registers) + (a b : Leaf L → ℤ) + (ha : ∀ τ, (a τ).natAbs ≤ A) (hb : ∀ τ, (b τ).natAbs ≤ B) + (hx : CatalogueParameters L H D R x) + (hV : x.regs Reg.values = V) (hAA : x.regs Reg.arrayA = AA) + (hBB : x.regs Reg.arrayB = BB) + (hcount : x.regs Reg.count = Nat.count (Eligible L H) ((H + 1) * 10 ^ L)) + (hcat : CataloguePrefix L H D R ((H + 1) * 10 ^ L) μ x.mem) + (hDR : D + (H + 1) * 10 ^ L ≤ R) + (hRV : R + 3 * Nat.count (Eligible L H) ((H + 1) * 10 ^ L) ≤ V) + (hAV : AA + 10 ^ L ≤ V) (hBV : BB + 10 ^ L ≤ V) + (hleft : ∀ c : Fin (10 ^ L), x.mem (AA + c.val) = Signed.encode (a (leafAt c))) + (hright : ∀ c : Fin (10 ^ L), x.mem (BB + c.val) = Signed.encode (b (leafAt c))) + (hfit : Fits (w + 2) + (D + R + V + AA + BB + 20 * ((H + 1) * 10 ^ L) + 20 * 10 ^ L + 30)) + (hsigned : GenericRAM.Signed.Fits w (A + B + 10 ^ L * (A * B) : ℕ)) : + ∃ y, ExecWithin (w + 2) tile x y + (328 * Nat.count (Eligible L H) ((H + 1) * 10 ^ L) + 8) ∧ + (∀ s < (H + 1) * 10 ^ L, Eligible L H s → + y.mem (V + Nat.count (Eligible L H) s) = Signed.encode (slotValue a b s)) ∧ + (∀ q, ¬(V ≤ q ∧ q < V + Nat.count (Eligible L H) ((H + 1) * 10 ^ L)) → + y.mem q = x.mem q) ∧ (∀ i, ¬TileLocal i → y.regs i = x.regs i) := by + obtain ⟨u, hu, u0, u1, u10, u9, u3, um, uf⟩ := exec_constants x + (hfit.of_le (by omega)) + have hf0 : Fits (w + 2) 0 := hfit.of_le (Nat.zero_le _) + let v := u.set Reg.current 0 + have hv : ExecWithin (B := .standard) (w + 2) (ram[ Reg.current ← #0 ]) u v 1 := by + ram_eval [v, hf0] + have vf0 (i : Fin registers) (hi : i ≠ Reg.current) : v.regs i = u.regs i := by + simp only [v, Data.set_regs, Function.update_of_ne hi] + have vp : CatalogueParameters L H D R v := by + constructor + · exact (vf0 _ (by decide)).trans + ((uf _ (by decide) (by decide) (by decide) (by decide) (by decide)).trans hx.levels) + · exact (vf0 _ (by decide)).trans + ((uf _ (by decide) (by decide) (by decide) (by decide) (by decide)).trans hx.height) + · exact (vf0 _ (by decide)).trans + ((uf _ (by decide) (by decide) (by decide) (by decide) (by decide)).trans hx.span) + · exact (vf0 _ (by decide)).trans + ((uf _ (by decide) (by decide) (by decide) (by decide) (by decide)).trans hx.directory) + · exact (vf0 _ (by decide)).trans + ((uf _ (by decide) (by decide) (by decide) (by decide) (by decide)).trans hx.records) + · exact (vf0 _ (by decide)).trans + ((uf _ (by decide) (by decide) (by decide) (by decide) (by decide)).trans hx.slots) + · exact (vf0 _ (by decide)).trans u1 + · exact (vf0 _ (by decide)).trans u10 + · exact (vf0 _ (by decide)).trans u9 + · exact (vf0 _ (by decide)).trans u3 + · exact (vf0 _ (by decide)).trans u0 + have vf (i : Fin registers) (hi : i ≠ Reg.current) (h0 : i ≠ Reg.nil) + (h1 : i ≠ Reg.one) (h10 : i ≠ Reg.ten) (h9 : i ≠ Reg.nine) (h3 : i ≠ Reg.three) : + v.regs i = x.regs i := by + simpa only [v, Data.set_regs, Function.update_of_ne hi] using uf i h0 h1 h10 h9 h3 + have vm : v.mem = x.mem := um + obtain ⟨y, hy, hvalues, hframe⟩ := exec_tileLoop v a b ha hb vp + ((vf _ (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans hV) + ((vf _ (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans hAA) + ((vf _ (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans hBB) + ((vf _ (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans hcount) + (by simp [v]) (by simpa only [vm] using hcat) hDR hRV hAV hBV + (fun c => by simpa only [vm] using hleft c) + (fun c => by simpa only [vm] using hright c) hfit hsigned + have he : ExecWithin (w + 2) tile x y + (328 * Nat.count (Eligible L H) ((H + 1) * 10 ^ L) + 8) := by + exact ((hu.seq hv).seq hy).mono (by omega) + refine ⟨y, he, hvalues, ?_, fun i hi => he.regs_eq (tile_preserves i hi)⟩ + simpa only [vm] using hframe + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/TileChildren.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/TileChildren.lean new file mode 100644 index 0000000000..c5588a5df0 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/TileChildren.lean @@ -0,0 +1,98 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.TileKernels +public import Complexity.Computability.GenericRAM.Signed.Fits +import Mathlib.Algebra.BigOperators.Group.Finset.Basic + +/-! +# Complete native ten-child accumulation + +The actual child loop reads each directory rank and signed child value once. Every +intermediate signed sum fits by one mathematical bound on the ten child magnitudes; +there is no separate intermediate-fit or execution certificate among the inputs. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Cslib.WordRAM +open scoped BigOperators + +/-- All ten actual child additions, including loop tests and the final exit, cost at most 312. -/ +theorem exec_childLoop {w D V c e T p R C : ℕ} (x : Data registers) + (b : ℕ → ℤ) (rank : ℕ → ℕ) + (hD : x.regs Reg.directory = D) (hV : x.regs Reg.values = V) + (hc : x.regs Reg.completion = c) (he : x.regs Reg.stars = e) + (hT : x.regs Reg.span = T) (hTpos : 0 < T) (hp : x.regs Reg.starPower = p) + (hd : x.regs Reg.term = 0) (hacc : x.regs Reg.accumulator = 0) + (h9 : x.regs Reg.nine = 9) (h1 : x.regs Reg.one = 1) + (h10 : x.regs Reg.ten = 10) + (hrank : ∀ d < 10, + x.mem (D + ((e - 1) * T + (c - (9 - d) * p))) = rank d + 1) + (hvalue : ∀ d < 10, x.mem (V + rank d) = Signed.encode (b d)) + (hrange : ∀ d < 10, rank d ≤ R) + (hmag : ∀ d < 10, (b d).natAbs ≤ C) + (hsigned : GenericRAM.Signed.Fits w (10 * C : ℕ)) + (hfit : Fits (w + 2) (D + V + c + e * T + 10 * p + R + 30)) : + ∃ y, ExecWithin (w + 2) (.loop (.lt Reg.term Reg.ten) addChild) x y 312 ∧ + y.regs Reg.term = 10 ∧ + y.regs Reg.accumulator = Signed.encode (∑ d ∈ Finset.range 10, b d) ∧ + y.mem = x.mem ∧ (∀ i, ¬ChildLocal i → y.regs i = x.regs i) := by + have hsum (k : ℕ) (hk : k ≤ 10) : + (∑ d ∈ Finset.range k, b d).natAbs ≤ 10 * C := by + calc + _ ≤ ∑ d ∈ Finset.range k, (b d).natAbs := Int.natAbs_sum_le _ _ + _ ≤ ∑ _d ∈ Finset.range k, C := Finset.sum_le_sum fun d hd => + hmag d ((Finset.mem_range.mp hd).trans_le hk) + _ = k * C := by simp + _ ≤ 10 * C := Nat.mul_le_mul_right C hk + let I (y : Data registers) : Prop := + y.regs Reg.term ≤ 10 ∧ + y.regs Reg.accumulator = Signed.encode (∑ d ∈ Finset.range (y.regs Reg.term), b d) ∧ + y.mem = x.mem ∧ (∀ i, ¬ChildLocal i → y.regs i = x.regs i) + have hi : I x := by + refine ⟨by simp [hd], ?_, rfl, fun _ _ => rfl⟩ + simp [hd, hacc, Signed.encode] + have hb (y : Data registers) (hy : I y) + (hg : (Cond.lt Reg.term Reg.ten).Holds y) : + ∃ z, ExecWithin (w + 2) addChild y z 29 ∧ I z ∧ + 10 - z.regs Reg.term < 10 - y.regs Reg.term := by + obtain ⟨hle, hsumy, hmem, hregs⟩ := hy + have hy10 : y.regs Reg.ten = 10 := (hregs _ (by decide)).trans h10 + have hlt : y.regs Reg.term < 10 := by + simpa only [Cond.holds_lt, hy10] using hg + have hchildmag : (b (y.regs Reg.term)).natAbs ≤ 10 * C := + (hmag _ hlt).trans (by omega) + have hchildrank := hrange _ hlt + obtain ⟨z, hz, hza, hzd, hzm, hzf⟩ := exec_addChild + (hsigned.of_natAbs_le (hsum _ hle)) (hsigned.of_natAbs_le hchildmag) y + ((hregs _ (by decide)).trans hD) ((hregs _ (by decide)).trans hV) + ((hregs _ (by decide)).trans hc) ((hregs _ (by decide)).trans he) + ((hregs _ (by decide)).trans hT) hTpos ((hregs _ (by decide)).trans hp) + rfl hsumy ((hregs _ (by decide)).trans h9) ((hregs _ (by decide)).trans h1) + (by simpa only [hmem] using hrank _ hlt) + (by simpa only [hmem] using hvalue _ hlt) + (hfit.of_le (by omega)) + refine ⟨z, hz, ⟨by omega, ?_, hzm.trans hmem, + fun i hi => (hzf i hi).trans (hregs i hi)⟩, by omega⟩ + simpa only [hzd, Finset.sum_range_succ] using hza + obtain ⟨y, hy, hIy, hstop⟩ := ExecWithin.loop_invariant I + (fun y => 10 - y.regs Reg.term) hb hi + obtain ⟨hle, hya, hym, hyf⟩ := hIy + have hy10 : y.regs Reg.ten = 10 := (hyf _ (by decide)).trans h10 + have hdone : y.regs Reg.term = 10 := by + simp only [Cond.holds_lt, hy10, not_lt] at hstop + omega + refine ⟨y, ?_, hdone, ?_, hym, hyf⟩ + · simpa only [hd] using hy + · simpa only [hdone] using hya + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/TileKernels.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/TileKernels.lean new file mode 100644 index 0000000000..b40f3b1ba3 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/TileKernels.lean @@ -0,0 +1,177 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Program + +/-! +# Native compact-table reads and signed arithmetic + +The descriptor loads, leaf multiplication and child accumulation execute the actual +fixed-register program. The bounds include address arithmetic and operand loads as +well as the existing signed kernels. None of these routines changes memory. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Cslib.WordRAM + +/-- Registers written while loading one three-word descriptor. -/ +@[expose] def RecordLocal (i : Fin registers) : Prop := + i = Reg.address ∨ i = Reg.completion ∨ i = Reg.stars ∨ i = Reg.starPower + +instance (i : Fin registers) : Decidable (RecordLocal i) := + inferInstanceAs (Decidable (i = Reg.address ∨ i = Reg.completion ∨ + i = Reg.stars ∨ i = Reg.starPower)) + +private theorem loadRecord_preserves (i : Fin registers) : + ¬RecordLocal i → loadRecord.Preserves i := by decide +revert + +/-- Read the three actual descriptor cells within seven native instructions. -/ +theorem exec_loadRecord {w R j c e p : ℕ} (x : Data registers) + (hR : x.regs Reg.records = R) (hj : x.regs Reg.current = j) + (h1 : x.regs Reg.one = 1) (h3 : x.regs Reg.three = 3) + (hc : x.mem (R + j * 3) = c) (he : x.mem (R + j * 3 + 1) = e) + (hp : x.mem (R + j * 3 + 2) = p) (hfit : Fits w (R + j * 3 + 2)) : + ∃ y, ExecWithin w loadRecord x y 7 ∧ y.regs Reg.completion = c ∧ + y.regs Reg.stars = e ∧ y.regs Reg.starPower = p ∧ y.mem = x.mem ∧ + (∀ i, ¬RecordLocal i → y.regs i = x.regs i) := by + have hf0 : Fits w (j * 3) := hfit.of_le (by omega) + have hf1 : Fits w (R + j * 3) := hfit.of_le (by omega) + have hf2 : Fits w (R + j * 3 + 1) := hfit.of_le (by omega) + have hf3 : Fits w (R + j * 3 + 1 + 1) := by simpa only [Nat.add_assoc] using hfit + have hp' : x.mem (R + j * 3 + 1 + 1) = p := by simpa only [Nat.add_assoc] using hp + let y := (((((((x.set Reg.address (j * 3)).set Reg.address (R + j * 3)).set + Reg.completion c).set Reg.address (R + j * 3 + 1)).set Reg.stars e).set + Reg.address (R + j * 3 + 1 + 1)).set Reg.starPower p) + have hy : ExecWithin w loadRecord x y 7 := by + ram_eval [loadRecord, y, hR, hj, h1, h3, hc, he, hp', hf0, hf1, hf2, hf3, + Reg.address, Reg.records, Reg.current, Reg.one, Reg.three, Reg.completion, + Reg.stars, Reg.starPower, Fin.mk.injEq] + exact ⟨y, hy, by simp [y, Reg.completion, Reg.starPower, Reg.stars, Reg.address], + by simp [y, Reg.stars, Reg.starPower, Reg.address], by simp [y], rfl, + fun i hi => hy.regs_eq (loadRecord_preserves i hi)⟩ + +/-- The signed workspace, indexed address and returned accumulator. -/ +@[expose] def ProductLocal (i : Fin registers) : Prop := + i.val < 9 ∨ i = Reg.address ∨ i = Reg.accumulator + +instance (i : Fin registers) : Decidable (ProductLocal i) := + inferInstanceAs (Decidable (i.val < 9 ∨ i = Reg.address ∨ i = Reg.accumulator)) + +private theorem leafProduct_preserves (i : Fin registers) : + ¬ProductLocal i → leafProduct.Preserves i := by decide +revert + +/-- Actual encoded leaf loads, signed multiplication and result delivery cost nineteen. -/ +theorem exec_leafProduct {w : ℕ} {a b : ℤ} (ha : GenericRAM.Signed.Fits w a) + (hb : GenericRAM.Signed.Fits w b) (hab : GenericRAM.Signed.Fits w (a * b)) + (x : Data registers) + (hleft : x.mem (x.regs Reg.arrayA + x.regs Reg.completion) = Signed.encode a) + (hright : x.mem (x.regs Reg.arrayB + x.regs Reg.completion) = Signed.encode b) + (hp : Fits (w + 2) (x.regs Reg.arrayA + x.regs Reg.completion)) + (hq : Fits (w + 2) (x.regs Reg.arrayB + x.regs Reg.completion)) : + ∃ y, ExecWithin (w + 2) leafProduct x y 19 ∧ + y.regs Reg.accumulator = Signed.encode (a * b) ∧ y.mem = x.mem ∧ + (∀ i, ¬ProductLocal i → y.regs i = x.regs i) := by + let z := ((((x.set Reg.address (x.regs Reg.arrayA + x.regs Reg.completion)).set + Signed.left (Signed.encode a)).set Reg.address + (x.regs Reg.arrayB + x.regs Reg.completion)).set Signed.right (Signed.encode b)) + have hload : ExecWithin (w + 2) leafLoad x z 4 := by + ram_eval [leafLoad, z, hleft, hright, hp, hq, Reg.address, Reg.arrayA, + Reg.arrayB, Reg.completion, Signed.left, Signed.right, Fin.mk.injEq] + obtain ⟨u, hu, hproduct, hframe⟩ := Signed.exec_multiply (r := 55) ha hb hab z + (by simp +decide [z, Signed.left, Signed.right, Reg.address]) (by simp [z]) + have hproduct' : u.regs Signed.result = Signed.encode (a * b) := hproduct + let y := u.set Reg.accumulator (Signed.encode (a * b)) + have hfinish : ExecWithin (w + 2) leafFinish u y 1 := by + ram_eval [leafFinish, y, hproduct'] + have hy : ExecWithin (w + 2) leafProduct x y 19 := hload.seq (hu.seq hfinish) + exact ⟨y, hy, by simp [y], hframe.1, + fun i hi => hy.regs_eq (leafProduct_preserves i hi)⟩ + +/-- The signed workspace and native directory/value-address temporaries of one child. -/ +@[expose] def ChildLocal (i : Fin registers) : Prop := + i.val < 9 ∨ i = Reg.temporary ∨ i = Reg.childCode ∨ i = Reg.childSlot ∨ + i = Reg.address ∨ i = Reg.childRank ∨ i = Reg.accumulator ∨ i = Reg.term + +instance (i : Fin registers) : Decidable (ChildLocal i) := + inferInstanceAs (Decidable (i.val < 9 ∨ i = Reg.temporary ∨ i = Reg.childCode ∨ + i = Reg.childSlot ∨ i = Reg.address ∨ i = Reg.childRank ∨ + i = Reg.accumulator ∨ i = Reg.term)) + +private theorem addChild_preserves (i : Fin registers) : + ¬ChildLocal i → addChild.Preserves i := by decide +revert + +/-- Read the actual offset-one directory rank and child value, add it, and advance the term. +The caller supplies mathematical readback equalities, not an execution or time contract. -/ +theorem exec_addChild {w D V c e T p d r : ℕ} {a b : ℤ} + (ha : GenericRAM.Signed.Fits w a) (hb : GenericRAM.Signed.Fits w b) + (x : Data registers) + (hD : x.regs Reg.directory = D) (hV : x.regs Reg.values = V) + (hc : x.regs Reg.completion = c) (he : x.regs Reg.stars = e) + (hT : x.regs Reg.span = T) (hTpos : 0 < T) (hp : x.regs Reg.starPower = p) + (hd : x.regs Reg.term = d) (hacc : x.regs Reg.accumulator = Signed.encode a) + (h9 : x.regs Reg.nine = 9) (h1 : x.regs Reg.one = 1) + (hrank : x.mem (D + ((e - 1) * T + (c - (9 - d) * p))) = r + 1) + (hvalue : x.mem (V + r) = Signed.encode b) + (hfit : Fits (w + 2) (D + V + c + e * T + 10 * p + r + d + 20)) : + ∃ y, ExecWithin (w + 2) addChild x y 29 ∧ + y.regs Reg.accumulator = Signed.encode (a + b) ∧ y.regs Reg.term = d + 1 ∧ + y.mem = x.mem ∧ (∀ i, ¬ChildLocal i → y.regs i = x.regs i) := by + let cc := c - (9 - d) * p + let cs := (e - 1) * T + cc + have hmp : (9 - d) * p ≤ 10 * p := Nat.mul_le_mul_right p (by omega) + have hmt : (e - 1) * T ≤ e * T := Nat.mul_le_mul_right T (Nat.sub_le ..) + have heT : e ≤ e * T := by simpa only [Nat.mul_one] using + (Nat.mul_le_mul_left e hTpos) + have hcc : cc ≤ c := Nat.sub_le .. + have hcs : cs ≤ e * T + c := Nat.add_le_add hmt hcc + have hf9 : Fits (w + 2) (9 - d) := hfit.of_le (by omega) + have hfmp : Fits (w + 2) ((9 - d) * p) := hfit.of_le (by omega) + have hfcc : Fits (w + 2) cc := hfit.of_le (by omega) + have hfe : Fits (w + 2) (e - 1) := hfit.of_le (by omega) + have hfmt : Fits (w + 2) ((e - 1) * T) := hfit.of_le (by omega) + have hfcs : Fits (w + 2) cs := hfit.of_le (by omega) + have hfD : Fits (w + 2) (D + cs) := hfit.of_le (by omega) + have hfr : Fits (w + 2) r := hfit.of_le (by omega) + have hfV : Fits (w + 2) (V + r) := hfit.of_le (by omega) + have hfd : Fits (w + 2) (d + 1) := hfit.of_le (by omega) + let z := ((((((((((((x.set Reg.temporary (9 - d)).set Reg.temporary ((9 - d) * p)).set + Reg.childCode cc).set Reg.childSlot (e - 1)).set Reg.childSlot ((e - 1) * T)).set + Reg.childSlot cs).set Reg.address (D + cs)).set Reg.childRank (r + 1)).set + Reg.childRank r).set Reg.address (V + r)).set Signed.right (Signed.encode b)).set + Signed.left (Signed.encode a)) + have hload : ExecWithin (w + 2) childLoad x z 12 := by + ram_eval [childLoad, z, cc, cs, hD, hV, hc, he, hT, hp, hd, hacc, h9, h1, + hrank, hvalue, hf9, hfmp, hfcc, hfe, hfmt, hfcs, hfD, hfr, hfV, + Reg.temporary, Reg.childCode, Reg.childSlot, Reg.address, Reg.childRank, + Reg.completion, Reg.stars, Reg.span, Reg.starPower, Reg.directory, Reg.values, + Reg.term, Reg.accumulator, Reg.nine, Reg.one, Signed.left, Signed.right, + Fin.mk.injEq, Nat.add_sub_cancel] + obtain ⟨u, hu, hsum, hframe⟩ := Signed.exec_add (r := 55) ha hb z + (by simp [z]) (by simp +decide [z, Signed.left, Signed.right]) + have hsum' : u.regs Signed.result = Signed.encode (a + b) := hsum + have hud : u.regs Reg.term = d := by + rw [hframe.2 _ (Or.inr (by decide))] + simpa +decide [z, Reg.term, Reg.temporary, Reg.childCode, Reg.childSlot, + Reg.address, Reg.childRank, Signed.left, Signed.right] using hd + have hu1 : u.regs Reg.one = 1 := by + rw [hframe.2 _ (Or.inr (by decide))] + simpa +decide [z, Reg.one, Reg.temporary, Reg.childCode, Reg.childSlot, + Reg.address, Reg.childRank, Signed.left, Signed.right] using h1 + let y := (u.set Reg.accumulator (Signed.encode (a + b))).set Reg.term (d + 1) + have hfinish : ExecWithin (w + 2) childFinish u y 2 := by + ram_eval [childFinish, y, hud, hu1, hsum', hfd, Reg.term, Reg.accumulator, + Reg.one, Fin.mk.injEq] + have hy : ExecWithin (w + 2) addChild x y 29 := hload.seq (hu.seq hfinish) + exact ⟨y, hy, by simp [y, Reg.accumulator, Reg.term], by simp [y], hframe.1, + fun i hi => hy.regs_eq (addChild_preserves i hi)⟩ + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Values.lean b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Values.lean new file mode 100644 index 0000000000..7200a2a7c1 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/MatrixMultiplication/Schonhage/BoxTable/Values.lean @@ -0,0 +1,65 @@ +/- +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.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Children + +/-! +# Compact box values and original-array magnitude bounds + +The stored value uses the existing finite `boxValue` recurrence. Its magnitude +bound covers every child partial sum as well as the final value, including cancellation. +The input arrays are arbitrary signed leaf functions, so encoded matrix arrays specialize +the same construction without changing its machine semantics. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +open Finset Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- The existing finite value associated to one actual directory slot. -/ +@[expose] def slotValue {L : ℕ} (a b : Leaf L → ℤ) (s : ℕ) : ℤ := + boxValue a b (recordStars L s) (slotCube L s) + +/-- Original-array bounds cover the complete finite recurrence at every cube. -/ +theorem natAbs_boxValue_le {L A B : ℕ} (a b : Leaf L → ℤ) + (ha : ∀ τ, (a τ).natAbs ≤ A) (hb : ∀ τ, (b τ).natAbs ≤ B) + (e : ℕ) (π : Cube L) : (boxValue a b e π).natAbs ≤ 10 ^ e * (A * B) := by + induction e generalizing π with + | zero => + simpa only [boxValue, pow_zero, one_mul, Int.natAbs_mul] using + Nat.mul_le_mul (ha π.starsToP0) (hb π.starsToP0) + | succ e ih => + rw [boxValue] + split + · calc + _ ≤ ∑ lam : Term, (boxValue a b e (π.replace _ lam)).natAbs := Int.natAbs_sum_le _ _ + _ ≤ ∑ _lam : Term, 10 ^ e * (A * B) := sum_le_sum fun _ _ => ih _ + _ = 10 ^ (e + 1) * (A * B) := by + simp only [sum_const, card_univ, card_term, smul_eq_mul] + ring + · simp + +/-- Every eligible slot's value fits the original full-depth magnitude envelope. -/ +theorem natAbs_slotValue_le {L H A B s : ℕ} (a b : Leaf L → ℤ) + (ha : ∀ τ, (a τ).natAbs ≤ A) (hb : ∀ τ, (b τ).natAbs ≤ B) + (hs : Eligible L H s) : (slotValue a b s).natAbs ≤ 10 ^ L * (A * B) := by + have he : recordStars L s ≤ L := hs.1.trans (population_le _ _) + exact (natAbs_boxValue_le a b ha hb _ _).trans + (Nat.mul_le_mul_right _ (Nat.pow_le_pow_right (by decide) he)) + +/-- With the existing tensor encodings, the stored recurrence is the original signed cube sum. -/ +theorem slotValue_encoding {L m t s : ℕ} (a : LeftStr L → ℤ) (b : RightStr L → ℤ) + (hs : Eligible L (m - t) s) : + slotValue (encodingL a) (encodingR b) s = Cube.val a b (slotCube L s) := by + apply boxValue_eq_val + exact mem_boxesWithStars.mpr ⟨slotCube_isBox hs, slotCube_star_count hs⟩ + +end Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable diff --git a/Complexity/Foundations/Data/Finset/LowestMax.lean b/Complexity/Foundations/Data/Finset/LowestMax.lean new file mode 100644 index 0000000000..0457b2ec58 --- /dev/null +++ b/Complexity/Foundations/Data/Finset/LowestMax.lean @@ -0,0 +1,90 @@ +/- +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.Foundations.Data.Finset.Lowest +public import Mathlib.Data.Finset.Max + +/-! +# The last element of a finite initial subset + +These initial-subset facts identify the highest starred coordinate of a canonical +tensor box and the remaining star set after replacing it. They use the existing +rank-filter initial subset rather than adding a second ordering or rank convention. +-/ + +public section + +namespace Finset + +variable {α : Type*} [LinearOrder α] + +/-- Membership of a finite initial subset is downward closed inside the original set. -/ +theorem mem_lowest_of_le {S : Finset α} {k : ℕ} {x y : α} + (hy : y ∈ lowest k S) (hx : x ∈ S) (hxy : x ≤ y) : x ∈ lowest k S := by + refine mem_lowest.mpr ⟨hx, ?_⟩ + apply lt_of_le_of_lt (card_le_card ?_) (mem_lowest.mp hy).2 + intro z hz + exact mem_filter.mpr ⟨(mem_filter.mp hz).1, (mem_filter.mp hz).2.trans_le hxy⟩ + +/-- The last of the first `k` elements has precisely `k - 1` predecessors in the original set. -/ +theorem card_filter_lt_max_lowest {S : Finset α} {k : ℕ} (hk : k ≤ S.card) + (hne : (lowest k S).Nonempty) : + (S.filter fun x => x < (lowest k S).max' hne).card + 1 = k := by + have hc : (lowest k S).card = k := by rw [card_lowest, min_eq_left hk] + have hf : (S.filter fun x => x < (lowest k S).max' hne) = + (lowest k S).erase ((lowest k S).max' hne) := by + ext x + constructor + · intro hx + obtain ⟨hxs, hlt⟩ := mem_filter.mp hx + exact mem_erase.mpr ⟨hlt.ne, + mem_lowest_of_le (max'_mem _ hne) hxs hlt.le⟩ + · intro hx + obtain ⟨hne', hx⟩ := mem_erase.mp hx + exact mem_filter.mpr ⟨lowest_subset _ _ hx, + lt_of_le_of_ne (le_max' _ x hx) hne'⟩ + rw [hf, card_erase_of_mem (max'_mem _ hne), hc] + have hpos : 0 < k := by simpa only [hc] using hne.card_pos + omega + +/-- Removing the last selected element leaves the shorter initial subset. -/ +theorem erase_max_lowest {S : Finset α} {k : ℕ} (hk : k ≤ S.card) + (hne : (lowest k S).Nonempty) : + (lowest k S).erase ((lowest k S).max' hne) = lowest (k - 1) S := by + have hsub : (lowest k S).erase ((lowest k S).max' hne) ⊆ S := + (erase_subset _ _).trans (lowest_subset _ _) + have hinit := eq_lowest_of_lt hsub (fun x hx y hy => by + obtain ⟨hxn, hx⟩ := mem_erase.mp hx + by_cases hyq : y ∈ lowest k S + · have hymax : y = (lowest k S).max' hne := by + by_contra hn + exact (mem_sdiff.mp hy).2 (mem_erase.mpr ⟨hn, hyq⟩) + rw [hymax] + exact lt_of_le_of_ne (le_max' _ x hx) hxn + · exact lowest_lt hx (mem_sdiff.mpr ⟨(mem_sdiff.mp hy).1, hyq⟩)) + simpa only [card_erase_of_mem (max'_mem _ hne), card_lowest, min_eq_left hk] using hinit + +/-- Removing that coordinate from the ambient set leaves the same shorter initial subset. -/ +theorem erase_max_lowest_erase {S : Finset α} {k : ℕ} (hk : k ≤ S.card) + (hne : (lowest k S).Nonempty) : + (lowest k S).erase ((lowest k S).max' hne) = + lowest (k - 1) (S.erase ((lowest k S).max' hne)) := by + have hsub : (lowest k S).erase ((lowest k S).max' hne) ⊆ + S.erase ((lowest k S).max' hne) := erase_subset_erase _ (lowest_subset _ _) + have hinit := eq_lowest_of_lt hsub (fun x hx y hy => by + have hxs := (mem_erase.mp hx).2 + have hyS := (mem_erase.mp (mem_sdiff.mp hy).1).2 + have hnot : y ∉ lowest k S := by + intro hyq + exact (mem_sdiff.mp hy).2 + (mem_erase.mpr ⟨(mem_erase.mp (mem_sdiff.mp hy).1).1, hyq⟩) + exact lowest_lt hxs (mem_sdiff.mpr ⟨hyS, hnot⟩)) + simpa only [card_erase_of_mem (max'_mem _ hne), card_lowest, min_eq_left hk] using hinit + +end Finset diff --git a/Complexity/Foundations/Data/Nat/RadixUpdate.lean b/Complexity/Foundations/Data/Nat/RadixUpdate.lean new file mode 100644 index 0000000000..1ae50026f9 --- /dev/null +++ b/Complexity/Foundations/Data/Nat/RadixUpdate.lean @@ -0,0 +1,51 @@ +/- +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.Foundations.Data.Nat.Radix +import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise + +/-! +# Updating one digit of a finite-function radix code + +These weighted-digit identities reuse Mathlib's finite-function enumeration and sum +updates. The concrete client computes a child box's native encoding-array index by +replacing a P0 digit with one of the ten term digits, without rebuilding the string. +-/ + +public section + +namespace Nat + +open Finset + +/-- Replacing one digit changes exactly its weighted contribution to the code. -/ +theorem finFunctionFinEquiv_update_add {b L : ℕ} (f : Fin L → Fin b) (i : Fin L) + (d : Fin b) : + (finFunctionFinEquiv (Function.update f i d)).val + (f i).val * b ^ i.val = + (finFunctionFinEquiv f).val + d.val * b ^ i.val := by + have hfun : (fun j => (Function.update f i d j).val * b ^ j.val) = + Function.update (fun j => (f j).val * b ^ j.val) i (d.val * b ^ i.val) := by + funext j + by_cases h : j = i <;> simp [h] + rw [finFunctionFinEquiv_apply, finFunctionFinEquiv_apply, hfun, + sum_update_of_mem (mem_univ i), sdiff_singleton_eq_erase, + ← add_sum_erase univ (fun j => (f j).val * b ^ j.val) (mem_univ i)] + ac_rfl + +/-- Decreasing one digit computes its new code by a single exact natural subtraction. -/ +theorem finFunctionFinEquiv_update_of_le {b L : ℕ} (f : Fin L → Fin b) (i : Fin L) + (d : Fin b) (hd : d.val ≤ (f i).val) : + (finFunctionFinEquiv (Function.update f i d)).val = + (finFunctionFinEquiv f).val - ((f i).val - d.val) * b ^ i.val := by + have h := finFunctionFinEquiv_update_add f i d + have hm := Nat.mul_le_mul_right (b ^ i.val) hd + rw [Nat.sub_mul] + omega + +end Nat diff --git a/ComplexityTests/WordRAMSchonhageBoxTable.lean b/ComplexityTests/WordRAMSchonhageBoxTable.lean new file mode 100644 index 0000000000..5112bda35e --- /dev/null +++ b/ComplexityTests/WordRAMSchonhageBoxTable.lean @@ -0,0 +1,202 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable.Flat + +/-! +Actual native constructor/lookup regressions. These execute code from State.init and +check observable words, including dirty scratch and invalid directory slots. They do +not replace the general execution, finite-meaning, frame or resource proofs. +-/ + +set_option linter.hashCommand false + +namespace ComplexityTests.WordRAMSchonhageBoxTable + +open Cslib.WordRAM Cslib.WordRAM.Signed +open Cslib.Algorithms.MatrixMultiplication.Schonhage +open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BoxTable + +private def a (u : LeftStr 1) : ℤ := + match u 0 with + | .x i => ![1, 2, -1] i + | .p i j => !![-3, 2; 0, 5] i j + +private def b (u : RightStr 1) : ℤ := + match u 0 with + | .y j => ![3, -2, 1] j + | .q i j => !![2, -1; 4, 0] i j + +private def leftValues (i : Fin 10) : ℤ := encodeLeft (fun _ : Fin 1 => + Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.termDigits i) a + +private def rightValues (i : Fin 10) : ℤ := encodeRight (fun _ : Fin 1 => + Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.termDigits i) b + +-- The only depth-zero cube is a fully fixed empty leaf; both signed reads are real. +#guard match program.eval 12 100 ((State.init (input 0 0 0 (fun _ => 2) (fun _ => -3))).data) with + | some (y, _) => y.regs Reg.count == 1 && y.mem (y.regs Reg.values) == encode (-6) + | none => false + +-- Complete memoized construction, with one shared starred box after ten fixed leaves. +private def signedState : Data registers := + let x := (State.init (input 1 1 0 leftValues rightValues) : State registers).data + { x with mem := fun a => if 24 ≤ a ∧ a < 88 then 99 else if a = 88 then 777 else x.mem a } + +#guard match program.eval 16 10000 signedState with + | some (y, _) => y.regs Reg.count == 11 && y.regs Reg.values == 77 && + y.mem 86 == encode (-4) && y.mem 87 == encode (-8) && y.mem 88 == 777 && + (List.range 24).all (fun a => y.mem a == signedState.mem a) && + (List.range 9).all (fun i => y.mem (34 + i) == 0) + | none => false + +private def request : Code .standard registers := + .seq program (.seq (ram[ Reg.cube ← #100 ]) lookup) + +private def queryState (digits : List ℕ) : Data registers := + { signedState with mem := fun a => + if 100 ≤ a then digits[a - 100]?.getD 0 else signedState.mem a } + +-- Real lookup reads the computed compact table, including the digit-nine child of the sum. +#guard match request.eval 16 10000 (queryState [10]) with + | some (y, _) => y.regs Reg.found == 1 && y.regs Reg.answer == encode (-8) && y.mem 88 == 777 + | none => false + +-- Out-of-alphabet words are rejected by actual code before digit multiplication. +#guard match request.eval 16 10000 (queryState [999]) with + | some (y, _) => y.regs Reg.found == 0 && y.regs Reg.answer == 0 + | none => false + +-- At threshold m, only the nine non-P0 fixed leaves remain; a star is rejected. +#guard match program.eval 16 10000 + ((State.init (input 1 1 1 leftValues rightValues)).data) with + | some (y, _) => y.regs Reg.count == 9 && y.regs Reg.values == 61 && y.mem 33 == 0 + | none => false + +#guard match request.eval 16 10000 ((queryState [10]).write 3 1) with + | some (y, _) => y.regs Reg.found == 0 && y.regs Reg.answer == 0 + | none => false + +private def depthTwoState (digits : List ℕ) : Data registers := + let x := (State.init (input 2 2 0 (fun _ => 1) (fun _ => 1)) : State registers).data + { x with mem := fun p => if 204 ≤ p ∧ p < 984 then 99 else + if p = 1050 then 777 else if 1100 ≤ p then digits[p - 1100]?.getD 0 else x.mem p } + +private def depthTwoRequest : Code .standard registers := + .seq program (.seq (ram[ Reg.cube ← #1100 ]) lookup) + +-- Both star layers use real earlier ranks; the full two-star cube sums 100 leaf products. +#guard match depthTwoRequest.eval 20 10000 (depthTwoState [10, 10]) with + | some (y, _) => y.regs Reg.count == 120 && y.regs Reg.values == 864 && + y.regs Reg.found == 1 && y.regs Reg.answer == encode 100 && y.mem 1050 == 777 + | none => false + +#guard match depthTwoRequest.eval 20 10000 (depthTwoState [10, 9]) with + | some (y, _) => y.regs Reg.found == 1 && y.regs Reg.answer == encode 10 + | none => false + +-- Reversing those symbols puts a fixed P0 below a star and is not a canonical box. +#guard match depthTwoRequest.eval 20 10000 (depthTwoState [9, 10]) with + | some (y, _) => y.regs Reg.found == 0 && y.regs Reg.answer == 0 && y.mem 1050 == 777 + | none => false + +-- Fully admitted compilation client: the observed word belongs to the same native +-- pre-halt witness as the initialized prefix and charged halt. +example : ∃ y n, + Runs 20 (program.program Reg.values) (State.init (input 0 0 0 (fun _ => 2) (fun _ => -3))) + ⟨program.size, y⟩ n ∧ + Executes 20 (program.program Reg.values) + (State.init (input 0 0 0 (fun _ => 2) (fun _ => -3))) (valueBase 0 0 0) (n + 1) ∧ + n + 1 ≤ timeBound 0 0 0 ∧ y.mem (y.regs Reg.values) = encode (-6) := by + obtain ⟨_, y, n, hn, hr, he, _, _, _, _, _, hV, _, _, hvalues, _⟩ := + runs_wide (A := 2) (B := 3) (fun _ : Fin 1 => (2 : ℤ)) (fun _ => (-3 : ℤ)) + (by decide) (by decide) (by decide : admissionWidth 0 0 0 2 3 ≤ 20) + refine ⟨y, n, hr, he, hn, ?_⟩ + have hv := hvalues 0 (by decide) (by decide) + have hvalue : slotValue (fun _ : Leaf 0 => (2 : ℤ)) (fun _ => (-3 : ℤ)) 0 = -6 := + by decide + rw [hV] + simpa only [Nat.count_zero, Nat.add_zero, hvalue] using hv + +private theorem left_magnitude : ∀ i, (leftValues i).natAbs ≤ 20 := by decide +private theorem right_magnitude : ∀ i, (rightValues i).natAbs ≤ 20 := by decide + +-- Positive depth has a real ten-child sum. All hypotheses of the general native +-- constructor are discharged, including the original-array bounds and width. +example : ∃ y n, + Runs 20 (program.program Reg.values) (State.init (input 1 1 0 leftValues rightValues)) + ⟨program.size, y⟩ n ∧ + Executes 20 (program.program Reg.values) (State.init (input 1 1 0 leftValues rightValues)) + 77 (n + 1) ∧ n + 1 ≤ timeBound 1 1 0 ∧ + y.regs Reg.count = 11 ∧ y.regs Reg.values = 77 ∧ y.mem 87 = encode (-8) := by + obtain ⟨_, y, n, hn, hr, he, _, _, _, _, _, hV, hK, _, hvalues, _⟩ := + runs_wide leftValues rightValues left_magnitude right_magnitude + (by decide : admissionWidth 1 1 0 20 20 ≤ 20) + have hbase : valueBase 1 1 0 = 77 := by decide + have hcard : (boxes 1 1 0).card = 11 := by decide + have hv := hvalues 19 (by decide) (by decide) + have hindex : valueBase 1 1 0 + Nat.count (Eligible 1 1) 19 = 87 := by decide + have hvalue : slotValue + (fun τ : Leaf 1 => leftValues + (Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.leafIndex τ)) + (fun τ : Leaf 1 => rightValues + (Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.leafIndex τ)) 19 = -8 := + by decide + refine ⟨y, n, hr, by simpa only [hbase] using he, hn, + hK.trans hcard, hV.trans hbase, ?_⟩ + simpa only [hindex, hvalue] using hv + +private def lookupCaller (y : Data registers) : Data registers := + (y.set Reg.cube 100).write 100 10 + +-- A genuine callable lookup consumes the table produced by the same initialized +-- constructor witness. Only the new query word and its pointer are supplied by the caller. +example : ∃ y n z, + Runs 20 (program.program Reg.values) (State.init (input 1 1 0 leftValues rightValues)) + ⟨program.size, y⟩ n ∧ + Executes 20 (program.program Reg.values) (State.init (input 1 1 0 leftValues rightValues)) + 77 (n + 1) ∧ + ExecWithin 20 lookup (lookupCaller y) z 50 ∧ z.regs Reg.found = 1 ∧ + z.regs Reg.answer = encode (-8) ∧ z.mem = (lookupCaller y).mem := by + obtain ⟨_, y, n, _, hr, he, _, yL, yH, yT, yD, yV, _, hdir, hvalues, _⟩ := + runs_wide leftValues rightValues left_magnitude right_magnitude + (by decide : admissionWidth 1 1 0 20 20 ≤ 20) + let π : Cube 1 := fun _ => .star + let encA (τ : Leaf 1) := leftValues + (Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.leafIndex τ) + let encB (τ : Leaf 1) := rightValues + (Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.leafIndex τ) + have hbase : valueBase 1 1 0 = 77 := by decide + have hmem (q : ℕ) (hq : q ≠ 100) : (lookupCaller y).mem q = y.mem q := by + simp only [lookupCaller, Data.write_mem, Data.set_mem, Function.update_of_ne hq] + obtain ⟨z, hz, hzm, hfound, hanswer, _⟩ := exec_lookup (lookupCaller y) π encA encB + (by decide : IsBox 1 0 π) + (by simpa [lookupCaller, Reg.levels, Reg.cube] using yL) + (by simpa [lookupCaller, Reg.height, Reg.cube] using yH) + (by simpa [lookupCaller, Reg.span, Reg.cube] using yT) + (by simp [lookupCaller]) + (by simpa [lookupCaller, Reg.directory, Reg.cube, directoryBase] using yD) + (by simpa [lookupCaller, Reg.values, Reg.cube, hbase] using yV) + (fun i hi => by + have hi0 : i = 0 := by omega + subst i + simp [lookupCaller, rawCubeDigit, cubeDigit, π]) + (fun s hs => by + rw [hmem _ (by omega)] + simpa [directoryBase] using hdir s hs) + (fun s hs hv => by + have hc : Nat.count (Eligible 1 1) s ≤ s := Nat.count_le _ + rw [hmem _ (by + change 77 + Nat.count (Eligible 1 1) s ≠ 100 + change s < 20 at hs + omega)] + simpa only [hbase, encA, encB] using hvalues s hs hv) + (by decide : Fits 20 (100 + 24 + 77 + (1 - 0 + 1) * 10 ^ 1 + 10 ^ 1 + 1 + 30)) + have hvalue : boxValue encA encB π.starLevels.card π = -8 := by decide + exact ⟨y, n, z, hr, by simpa only [hbase] using he, hz, hfound, + by simpa only [hvalue] using hanswer, hzm⟩ + +end ComplexityTests.WordRAMSchonhageBoxTable diff --git a/UPSTREAM.md b/UPSTREAM.md index c88bd0fdb6..e7c62a733f 100644 --- a/UPSTREAM.md +++ b/UPSTREAM.md @@ -414,6 +414,20 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he Mathlib-intended `Foundations/Data/Finset/Lowest` topic module, used by the canonical boxes. Native box enumeration/trie construction/query costs and the tuned 1.9992 route remain #1394. No curated abstract or rendering changes are needed for this finite prerequisite. +* **Native shared box tables.** The original native representation in + [#2176](https://github.com/cslib-community/complexitylib/issues/2176) reuses the finite boxes + and value recurrence above. A one-time directory over `(m-t+1)*10^L` slots computes compact + ranks and three-word descriptors. Per-tile code writes one signed value per box, reading + only earlier child ranks; lookup reads those stored words. This replaces the primary + source's per-tile relative-pointer trie, not its mathematical box notion. Native level zero + remains least significant, matching the existing encoders; the source's Horner numbering + must not be substituted silently. Shared setup is at most `64*(L+1)^2*10^L` for `m ≤ L`, + each tile costs at most `328*B+8`, and valid lookup at most `18*L+32`, with the actual box + count `B`. Setup, resident geometry and retained tile storage must all be charged in future + global composition; no Corollary 26 or tuned 1.9992 endpoint follows from this component. + `Foundations/Data/{Finset/LowestMax,Nat/RadixUpdate}` hold the small general ordered-subset + and radix-update facts used by these concrete clients. No curated abstract or rendering + changes are needed for this native data-structure prerequisite. * **Native pruned-query evaluator.** The explicit-stack pruned-query evaluator ([#1526](https://github.com/cslib-community/complexitylib/issues/1526)) is original native code, reusing the finite `Pruned.result`, `childSet` and trace/leaf quantities from `Sec2/Lemma10.lean`. `PrunedQuery.queryIndex` directly applies the existing