diff --git a/Complexity.lean b/Complexity.lean index 227ff8d31a..6f3915c1fb 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -102,6 +102,23 @@ public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationInput public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationSpec public import Complexity.Algorithms.WordRAM.ExactTriangle.QueryScan public import Complexity.Algorithms.WordRAM.ExactTriangle.QuerySpec +public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct +public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Bounds +public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Copy +public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Decode +public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Entry +public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Exec +public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.First +public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Flat +public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Header +public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.InputSpec +public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Kernel +public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Prepare +public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Producer +public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.ProducerQueries +public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Program +public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.RawInput +public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.SourceBounds public import Complexity.Algorithms.WordRAM.ExactTriangle.ResidueClasses public import Complexity.Algorithms.WordRAM.ExactTriangle.WriteMatrices public import Complexity.Algorithms.WordRAM.FusionTree.Binary diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationInput.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationInput.lean index 876bc8d8da..f126a6eb98 100644 --- a/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationInput.lean +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationInput.lean @@ -29,6 +29,7 @@ pre-halt state and the final halt charged. ## Main results +* `PreparationInput.exec_input`: structured execution for composition, without the final halt. * `PreparationInput.runs_input`: initialized execution, exact readback, fits and charged halt. * `PreparationInput.bounded_reachable`: input-derived word and address bounds at every prefix. * `PreparationInput.width_le_log`, `PreparationInput.wordBound_le_pow`: logarithmic physical @@ -213,18 +214,17 @@ private theorem input_fits {n D g p A : ℕ} (values : List ℤ) have hs := hmag.of_natAbs_le ((hv z hz).trans (by omega : A ≤ A + p + 1)) exact (Signed.encode_fits hs).mono (by dsimp only [width]; omega) -/-- Complete initialized execution at every admitted physical width. The prefix witness and -the output predicate use the same actual pre-halt memory, and the bound includes the halt. -/ -theorem runs_input {n D g p A W : ℕ} (values : List ℤ) +/-- Structured initialized execution for real native caller composition. The budget excludes +only the final halt; all existing original-input, width and exact readback hypotheses remain. +This does not accept an execution, layout or intermediate-fit certificate. -/ +theorem exec_input {n D g p A W : ℕ} (values : List ℤ) (hlen : values.length = 3 * (n * n)) (hD : 1 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : 0 < p) (hv : ∀ z ∈ values, z.natAbs ≤ A) (hw : width n D g p A ≤ W) : let C := fun rho => Nat.count (fun q => (values.getD q 0 % (p : ℤ)).toNat = rho) (n * n) let K := ChunkCatalogue.before C (queryCap n D) p - ∃ y t, t ≤ Instances.timeBound n D p K (numPieces n D g) ∧ - Runs W flatProgram (State.init (input n D g p values)) ⟨Instances.program.size, y⟩ - (t - 1) ∧ - Executes W flatProgram (State.init (input n D g p values)) (y.regs Instances.output) t ∧ + ∃ y, ExecWithin W Instances.program (.init (input n D g p values)) y + (Instances.timeBound n D p K (numPieces n D g) - 1) ∧ Instances.Output n D g p (fun q => values.getD q 0) (.init (input n D g p values)) y ∧ InputFits W (input n D g p values) ∧ y.Bounded W := by @@ -244,6 +244,24 @@ theorem runs_input {n D g p A W : ℕ} (values : List ℤ) have hew := ExecWithin.mono_width Instances.program_fixed.2 hy hw have hi := (input_fits values hlen hv).mono hw have hybounded := hew.bounded (Data.Bounded.init hi) + exact ⟨y, hew, hout, hi, hybounded⟩ + +/-- Complete initialized execution at every admitted physical width. The prefix witness and +the output predicate use the same actual pre-halt memory, and the bound includes the halt. -/ +theorem runs_input {n D g p A W : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) + (hD : 1 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : 0 < p) + (hv : ∀ z ∈ values, z.natAbs ≤ A) (hw : width n D g p A ≤ W) : + let C := fun rho => Nat.count (fun q => (values.getD q 0 % (p : ℤ)).toNat = rho) (n * n) + let K := ChunkCatalogue.before C (queryCap n D) p + ∃ y t, t ≤ Instances.timeBound n D p K (numPieces n D g) ∧ + Runs W flatProgram (State.init (input n D g p values)) ⟨Instances.program.size, y⟩ + (t - 1) ∧ + Executes W flatProgram (State.init (input n D g p values)) (y.regs Instances.output) t ∧ + Instances.Output n D g p (fun q => values.getD q 0) + (.init (input n D g p values)) y ∧ + InputFits W (input n D g p values) ∧ y.Bounded W := by + obtain ⟨y, hew, hout, hi, hybounded⟩ := exec_input values hlen hD hDn hg hp hv hw obtain ⟨t, ht, he⟩ := hew have hr := he.runs (pc := 0) (p := flatProgram) (Program.Contains.self _).append_left refine ⟨y, t + 1, ?_, ?_, ?_, hout, hi, hybounded⟩ diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct.lean new file mode 100644 index 0000000000..6d0ca12997 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct.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.ExactTriangle.RecordProduct.SourceBounds + +/-! +# Native ExactTriangle record-to-product adapter + +## Main definitions + +* `RecordProduct.program`: fixed 320-register consumer of any occupied producer record ordinal. +* `RecordProduct.entryProgram`: actual original-input producer followed by ordinal-zero selection + and that consumer; original geometry proves the first record exists. +* `RecordProduct.leftMatrix`, `RecordProduct.rightMatrix`: the unchanged native writer's actual + raw zero/one matrices, read in their respective row-major orders. +* `RecordProduct.admissionWidth`, `RecordProduct.wordBound`: original-header/weight bounds for + every sufficiently wide physical execution and its complete prefix words/address support. + +## Main results + +* `RecordProduct.exec_of_output`: actual producer readback derives all six record words, every + matrix/query pointer and separation, the coordinate occurrences and their sparsity; the actual + callee returns all requested product values and preserves the producer catalogue and registers. +* `RecordProduct.runs_input`: complete native `State.init`, same-data prefix `Runs`, returned + pointer, charged halt, exact product words, caller frame and occurrence sparsity. This fixed + initialized client selects the first record, rather than solving all prepared instances. +* `RecordProduct.timeBound_le`: actual callee work plus `O(nD+Q)` descriptor/log/header/copy/ + invocation overhead. There is no whole-window/catalogue initialization or snapshot. +* `RecordProduct.thin_timeBound_sparse`: under `D=4^m`, `L=19m`, `D^18≤n` and `Q·2^m≤n²`, the + per-record bound including halt is `34603008·(19m+1)·n²/D^(1/18)`. The actual chunk derives + its occurrence bound; a mere distinct-set bound instead retains the additive occurrence term. +* `RecordProduct.admissionWidth_le_log`: original polynomial header/weight envelopes give the + positive logarithmic threshold `(257κ+5906)·clog₂(n+2)` as a sufficient upper envelope. +* `RecordProduct.bounded_reachable_original`, `RecordProduct.wordBound_le_pow`: all wider native + prefixes have polynomial words/support independent of the chosen physical width. + +The native code computes the record stride/address, reads every descriptor word, recovers `m` +with the existing binary-logarithm program and division by two, writes original local headers, +and copies raw X/Y and all interleaved coordinate occurrences above the actual producer heap. +The entire 163-register callable bank is renamed together. Memory rebasing is performed by its +actual compiler; register renaming alone is not a memory relocation. Raw matrix entries remain +zero/one during adapter copying: the actual callee already charges their canonical-signed doubling. + +`PreparationInput.exec_input` exposes the existing structured initialized producer execution, +and `PreparationInput.runs_input` reuses it without changing its statement or cost. Stage lemmas +in the submodules are internal implementation interfaces. No intermediate fits, layouts, routing +tables, run/time/solver or sparse-bound certificate is an original input hypothesis. + +This is per-record composition, not an aggregate subcubic ExactTriangle solver. Global parameter +and prime selection, the outer instance loop, backend/witness reconstruction, the full ordinary +distinct-position 3SUM composition and the improved 1.9992 endpoint remain open under #1394. + +## References + +The existing matrix writer and queried-product mathematics retain their pinned +[AlmanWilliams2026] / Anthropic source mapping. This adapter, register framing, initialized +composition and charged native proofs are original work; they do not transfer source Light +semantics or instruction constants. The value-only matrix wrappers reuse `WriteMatrices.entry`. +-/ diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Bounds.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Bounds.lean new file mode 100644 index 0000000000..97df3f2d40 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Bounds.lean @@ -0,0 +1,154 @@ +/- +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.ExactTriangle.RecordProduct.Producer +public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationInput + +/-! +# Input-derived admission and charged adapter overhead + +The actual producer supplies a polynomial bound for every pre-adapter word and address. +Its existing `wordBound` determines a sufficient positive logarithmic physical width for the +selected product's computed window. Adaptation is linear in `nD+Q`; this per-record statement +does not sum an ExactTriangle solver or establish its aggregate subcubic bound. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct + +open Cslib.WordRAM Cslib.Algorithms.ExactTriangle +open Cslib.Algorithms.MatrixMultiplication.Schonhage +open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage + +/-- Original-input physical width covering the actual producer, every dirty producer word +before normalization, and all relocated product addresses. -/ +@[expose] def admissionWidth (n D g p A : ℕ) : ℕ := + PreparationInput.width n D g p A + + 256 * Nat.clog 2 (2 * PreparationInput.wordBound n D g p A + n + n ^ 2 + 5) + +/-- Physical admission is positive, including parameter boundary cases. -/ +theorem admissionWidth_pos (n D g p A : ℕ) : 0 < admissionWidth n D g p A := by + unfold admissionWidth PreparationInput.width + omega + +/-- Actual producer word/address bounds and the computed chunk size discharge the physical +fit numerically; neither a window nor an intermediate arithmetic certificate is an input. -/ +theorem physical_fits {W n D g p A b Q : ℕ} + (hb : b ≤ PreparationInput.wordBound n D g p A) (hQ : Q ≤ n ^ 2) + (hW : admissionWidth n D g p A ≤ W) : + Fits W (2 * b + 4 * CallableProduct.windowSize n Q + 1024) := by + have hw : 256 * Nat.clog 2 (2 * PreparationInput.wordBound n D g p A + n + n ^ 2 + 5) ≤ W := + by unfold admissionWidth at hW; omega + have hfit := CallableProduct.physical_fits hw + have hM : CallableProduct.windowSize n Q ≤ CallableProduct.windowSize n (n ^ 2) := by + apply Nat.pow_le_pow_right (by decide) + exact Nat.mul_le_mul_left 128 (Nat.clog_mono_right 2 (by omega)) + exact hfit.of_le (by omega) + +/-- The final threshold is logarithmic in the original outer dimension under the producer's +standard polynomial original-header/weight hypotheses. The constant is positive for every κ. -/ +theorem admissionWidth_le_log {n D g p A κ : ℕ} (hn : 1 ≤ n) + (hD : D ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) : + admissionWidth n D g p A ≤ (257 * κ + 5906) * Nat.clog 2 (n + 2) := by + let b := n + 2 + have hb : 2 ≤ b := by dsimp only [b]; omega + have hP := PreparationInput.wordBound_le_pow hn hD hg hp hA + change PreparationInput.wordBound n D g p A ≤ b ^ (κ + 19) at hP + have hunit : 1 ≤ b ^ (κ + 19) := Nat.one_le_pow _ _ (by omega) + have hnpow : n ≤ b ^ (κ + 19) := (show n ≤ b by dsimp only [b]; omega).trans + (Nat.le_self_pow (by omega) b) + have hn2 : n ^ 2 ≤ b ^ (κ + 19) := + (Nat.pow_le_pow_left (by dsimp only [b]; omega : n ≤ b) 2).trans + (Nat.pow_le_pow_right (by omega : 1 ≤ b) (by omega : 2 ≤ κ + 19)) + have harg : 2 * PreparationInput.wordBound n D g p A + n + n ^ 2 + 5 ≤ b ^ (κ + 23) := by + have hsum : 2 * PreparationInput.wordBound n D g p A + n + n ^ 2 + 5 ≤ + 9 * b ^ (κ + 19) := by omega + have hc : 9 ≤ b ^ 4 := (show 9 ≤ 2 ^ 4 by decide).trans (Nat.pow_le_pow_left hb 4) + calc + _ ≤ 9 * b ^ (κ + 19) := hsum + _ ≤ b ^ 4 * b ^ (κ + 19) := Nat.mul_le_mul_right _ hc + _ = b ^ (κ + 23) := by rw [← Nat.pow_add]; congr 1; omega + have hbase := Nat.le_pow_clog (by decide : 1 < (2 : ℕ)) b + have hlogBound := harg.trans (Nat.pow_le_pow_left hbase (κ + 23)) + rw [← Nat.pow_mul] at hlogBound + have hlog := Nat.clog_le_of_le_pow hlogBound + have hprep := PreparationInput.width_le_log hn hD hg hp hA + change Nat.clog 2 (2 * PreparationInput.wordBound n D g p A + n + n ^ 2 + 5) ≤ + Nat.clog 2 b * (κ + 23) at hlog + unfold admissionWidth + dsimp only [b] at hlog + nlinarith only [hlog, hprep] + +/-- All real descriptor/log/header/copy/invocation work is linear in original matrices and +occurrences. This includes standalone halt, but not another execution of the producer. -/ +theorem timeBound_le {m n : ℕ} (qs : List (Fin n × Fin n)) (hN : D m ^ 18 ≤ n) : + timeBound (m := m) qs + 1 ≤ + 3 * (QueriedProduct.timeBound (show m ≤ 19 * m by omega) qs + 1) + + 4096 * (n * D m + qs.length + 1) := by + have hn : 1 ≤ n := Nat.pow_pos (Nat.pow_pos (by decide : 0 < (4 : ℕ))) |>.trans_le hN + have hm : m ≤ D m := by + have hlog := Nat.log_le_self 2 (4 ^ m) + rw [log_two_four_pow] at hlog + change m ≤ 4 ^ m + omega + have hND : D m ≤ n * D m := Nat.le_mul_of_pos_left _ hn + have ht := CallableProduct.timeBound_le (m := m) qs + unfold timeBound + omega + +/-- The actual callee envelope already dominates a second copy of this linear adaptation. +This comparison reuses its established sparse bounds without a separate polylog oracle. -/ +theorem timeBound_le_twice_callable {m n : ℕ} (qs : List (Fin n × Fin n)) + (hN : D m ^ 18 ≤ n) : + timeBound (m := m) qs + 1 ≤ 2 * (CallableProduct.timeBound (m := m) qs + 3) := by + have hn : 1 ≤ n := Nat.pow_pos (Nat.pow_pos (by decide : 0 < (4 : ℕ))) |>.trans_le hN + have hm : m ≤ n * D m := by + have hlog := Nat.log_le_self 2 (4 ^ m) + rw [log_two_four_pow] at hlog + have hmul : D m ≤ n * D m := Nat.le_mul_of_pos_left _ hn + change 4 ^ m ≤ n * D m at hmul + omega + unfold timeBound CallableProduct.timeBound CallableProduct.coreTime QueriedProduct.timeBound + QueriedProduct.inputEnd + omega + +/-- Distinct-set sparsity retains the actual list-occurrence charge. -/ +theorem thin_timeBound {m n : ℕ} (qs : List (Fin n × Fin n)) (hN : D m ^ 18 ≤ n) + (hQ : qs.toFinset.card * 2 ^ m ≤ n ^ 2) : + ((timeBound (m := m) qs + 1 : ℕ) : ℝ) ≤ + 524288 * ((19 * m + 1 : ℕ) : ℝ) * + (65 * ((D m : ℝ) ^ (-(1 / 18 : ℝ)) * (n : ℝ) ^ 2) + qs.length) := by + have ht : ((timeBound (m := m) qs + 1 : ℕ) : ℝ) ≤ + 2 * ((CallableProduct.timeBound (m := m) qs + 3 : ℕ) : ℝ) := by + exact_mod_cast timeBound_le_twice_callable qs hN + have h := CallableProduct.thin_timeBound qs hN hQ + calc + _ ≤ 2 * ((CallableProduct.timeBound (m := m) qs + 3 : ℕ) : ℝ) := ht + _ ≤ 2 * (262144 * ((19 * m + 1 : ℕ) : ℝ) * + (65 * ((D m : ℝ) ^ (-(1 / 18 : ℝ)) * (n : ℝ) ^ 2) + qs.length)) := by linarith + _ = _ := by ring + +/-- Occurrence sparsity, which actual producer chunks supply, absorbs every occurrence charge. +The bound includes the adapter's standalone halt; producer execution is charged separately. -/ +theorem thin_timeBound_sparse {m n : ℕ} (qs : List (Fin n × Fin n)) + (hN : D m ^ 18 ≤ n) (hQ : qs.length * 2 ^ m ≤ n ^ 2) : + ((timeBound (m := m) qs + 1 : ℕ) : ℝ) ≤ + 34603008 * ((19 * m + 1 : ℕ) : ℝ) * (n : ℝ) ^ 2 / (D m : ℝ) ^ (1 / 18 : ℝ) := by + have ht : ((timeBound (m := m) qs + 1 : ℕ) : ℝ) ≤ + 2 * ((CallableProduct.timeBound (m := m) qs + 3 : ℕ) : ℝ) := by + exact_mod_cast timeBound_le_twice_callable qs hN + have h := CallableProduct.thin_timeBound_sparse qs hN hQ + calc + _ ≤ 2 * ((CallableProduct.timeBound (m := m) qs + 3 : ℕ) : ℝ) := ht + _ ≤ 2 * (17301504 * ((19 * m + 1 : ℕ) : ℝ) * (n : ℝ) ^ 2 / + (D m : ℝ) ^ (1 / 18 : ℝ)) := by linarith + _ = _ := by ring + +end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Copy.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Copy.lean new file mode 100644 index 0000000000..aa2ca1f2c2 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Copy.lean @@ -0,0 +1,129 @@ +/- +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.ExactTriangle.RecordProduct.Header + +/-! +# Three charged original-input copies + +The left and right raw matrices and every interleaved query occurrence are copied separately. +Sources lie below the actual producer heap end. Only the destination spans are written; no +caller catalogue, virtual window or unrelated allocation is cleared or copied. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct + +open Cslib.WordRAM + +/-- All three original arrays are copied with native loops, at fourteen instructions per +matrix cell/query pair plus constant argument and loop overhead. -/ +theorem exec_copyInputs {W b A Q s t q : ℕ} (x : Data 320) + (hb : x.regs Reg.base = b) (hA : x.regs Reg.area = A) + (hQ : x.regs Reg.count = Q) (hs : x.regs Reg.left = s) + (ht : x.regs Reg.right = t) (hq : x.regs Reg.queries = q) + (hsb : s + A ≤ b) (htb : t + A ≤ b) (hqb : q + 2 * Q ≤ b) + (hfit : Fits W (2 * b + 2 * A + 2 * Q + 64)) : + ∃ y, ExecWithin W copyInputs x y (14 * A + 14 * Q + 21) ∧ + (∀ a < A, y.mem (b + 5 + a) = x.mem (s + a)) ∧ + (∀ a < A, y.mem (b + 5 + A + a) = x.mem (t + a)) ∧ + (∀ a < 2 * Q, y.mem (b + 5 + 2 * A + a) = x.mem (q + a)) ∧ + (∀ a, a < b + 5 ∨ b + 5 + 2 * A + 2 * Q ≤ a → y.mem a = x.mem a) ∧ + ∀ i : Fin 320, i.val < 96 → i ≠ Reg.address → y.regs i = x.regs i := by + have h5 : Fits W 5 := hfit.of_le (by omega) + have hb5 : Fits W (b + 5) := hfit.of_le (by omega) + have hbA : Fits W (b + 5 + A) := hfit.of_le (by omega) + have hbAA : Fits W (b + 5 + A + A) := hfit.of_le (by omega) + have hQQ : Fits W (Q + Q) := hfit.of_le (by omega) + let l := x.set Reg.source s |>.set Reg.address 5 |>.set Reg.destination (b + 5) + |>.set Reg.length A + have hl : ExecWithin W deliverLeft x l 4 := by + ram_eval [deliverLeft, l, hs, hb, hA, h5, hb5, Reg.source, Reg.left, Reg.address, + Reg.destination, Reg.base, Reg.length, Reg.area] + have lmeta (i : Fin 320) (hi : i.val < 96) (hne : i ≠ Reg.address) : + l.regs i = x.regs i := by + have hsource : i ≠ Reg.source := by intro h; subst i; simp [Reg.source] at hi + have hdest : i ≠ Reg.destination := by intro h; subst i; simp [Reg.destination] at hi + have hlen : i ≠ Reg.length := by intro h; subst i; simp [Reg.length] at hi + simp only [l, Data.set_regs, Function.update_of_ne hsource, Function.update_of_ne hdest, + Function.update_of_ne hlen, Function.update_of_ne hne] + obtain ⟨a, ha, am, asrc, adst, alen, ar⟩ := exec_copy l + (by simp +decide [l, Reg.source, Reg.address, Reg.destination, Reg.length]) + (by simp +decide [l, Reg.destination, Reg.length]) (by simp [l]) + (by omega : s + A ≤ b + 5) (hfit.of_le (by omega)) + have aA : a.regs Reg.area = A := + (ar _ (by decide)).trans ((lmeta _ (by decide) (by decide)).trans hA) + have aRight : a.regs Reg.right = t := + (ar _ (by decide)).trans ((lmeta _ (by decide) (by decide)).trans ht) + let r := a.set Reg.source t |>.set Reg.destination (b + 5 + A) + have hr : ExecWithin W deliverRight a r 2 := by + ram_eval [deliverRight, r, aRight, adst, aA, hbA, Reg.source, Reg.right, + Reg.destination, Reg.area] + obtain ⟨c, hc, cm, csrc, cdst, clen, cr⟩ := exec_copy r + (by simp +decide [r, Reg.source, Reg.destination]) (by simp [r]) + (by simpa +decide [r, Reg.length, Reg.source, Reg.destination] using alen) + (by omega : t + A ≤ b + 5 + A) + (hfit.of_le (by omega)) + have rmeta (i : Fin 320) (hi : i.val < 96) : r.regs i = a.regs i := by + have hsource : i ≠ Reg.source := by intro h; subst i; simp [Reg.source] at hi + have hdest : i ≠ Reg.destination := by intro h; subst i; simp [Reg.destination] at hi + simp only [r, Data.set_regs, Function.update_of_ne hsource, Function.update_of_ne hdest] + have cA : c.regs Reg.area = A := + (cr _ (by decide)).trans ((rmeta _ (by decide)).trans aA) + have cq : c.regs Reg.queries = q := (cr _ (by decide)).trans + ((rmeta _ (by decide)).trans + ((ar _ (by decide)).trans ((lmeta _ (by decide) (by decide)).trans hq))) + have cQ : c.regs Reg.count = Q := (cr _ (by decide)).trans + ((rmeta _ (by decide)).trans + ((ar _ (by decide)).trans ((lmeta _ (by decide) (by decide)).trans hQ))) + let z := c.set Reg.source q |>.set Reg.destination (b + 5 + A + A) + |>.set Reg.length (Q + Q) + have hz : ExecWithin W deliverQueries c z 3 := by + ram_eval [deliverQueries, z, cq, cdst, cA, cQ, hbAA, hQQ, Reg.source, + Reg.queries, Reg.destination, Reg.area, Reg.length, Reg.count] + obtain ⟨y, hy, ym, ysrc, ydst, ylen, yr⟩ := exec_copy z + (by simp +decide [z, Reg.source, Reg.destination, Reg.length]) + (by simp +decide [z, Reg.destination, Reg.length]) (by simp [z]) + (by omega : q + (Q + Q) ≤ b + 5 + A + A) (hfit.of_le (by omega)) + have arMem : a.mem = ArrayCopy.copyPrefix x.mem s (b + 5) A := am + have crMem : c.mem = ArrayCopy.copyPrefix a.mem t (b + 5 + A) A := cm + have yrMem : y.mem = ArrayCopy.copyPrefix c.mem q (b + 5 + A + A) (Q + Q) := ym + refine ⟨y, ?_, ?_, ?_, ?_, ?_, ?_⟩ + · exact (hl.seq (ha.seq (hr.seq (hc.seq (hz.seq hy))))).mono (by omega) + · intro j hj + rw [yrMem, ArrayCopy.copyPrefix_outside (by omega), crMem, + ArrayCopy.copyPrefix_outside (by omega), arMem, ArrayCopy.copyPrefix_read hj] + · intro j hj + rw [yrMem, ArrayCopy.copyPrefix_outside (by omega), crMem, ArrayCopy.copyPrefix_read hj, + arMem, ArrayCopy.copyPrefix_outside (by omega)] + · intro j hj + have hj' : j < Q + Q := by omega + rw [show b + 5 + 2 * A + j = b + 5 + A + A + j by omega, + yrMem, ArrayCopy.copyPrefix_read hj', crMem, + ArrayCopy.copyPrefix_outside (by omega), arMem, + ArrayCopy.copyPrefix_outside (by omega)] + · intro j hj + rw [yrMem, ArrayCopy.copyPrefix_outside (by omega), crMem, + ArrayCopy.copyPrefix_outside (by omega), arMem, + ArrayCopy.copyPrefix_outside (by omega)] + · intro i hi hne + have hsource : i ≠ Reg.source := by intro h; subst i; simp [Reg.source] at hi + have hdest : i ≠ Reg.destination := by intro h; subst i; simp [Reg.destination] at hi + have hlen : i ≠ Reg.length := by intro h; subst i; simp [Reg.length] at hi + rw [yr i (Or.inl hi)] + simp only [z, Data.set_regs, Function.update_of_ne hsource, + Function.update_of_ne hdest, Function.update_of_ne hlen] + rw [cr i (Or.inl hi)] + simp only [r, Data.set_regs, Function.update_of_ne hsource, Function.update_of_ne hdest] + rw [ar i (Or.inl hi)] + simp only [l, Data.set_regs, Function.update_of_ne hsource, Function.update_of_ne hdest, + Function.update_of_ne hlen, Function.update_of_ne hne] + +end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Decode.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Decode.lean new file mode 100644 index 0000000000..a539d34bb9 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Decode.lean @@ -0,0 +1,128 @@ +/- +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.ExactTriangle.RecordProduct.Kernel + +/-! +# Actual record selection and depth recovery + +These internal lemmas account for the actual original-header and six descriptor loads, every +stride/address calculation, and the existing floor-logarithm loop. The final producer client +derives each loaded word from its actual readback theorem. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct + +open Cslib.WordRAM + +/-- The actual binary logarithm recovers twice the power-of-four exponent. -/ +theorem log_two_four_pow (m : ℕ) : Nat.log 2 (4 ^ m) = 2 * m := by + rw [show 4 ^ m = 2 ^ (2 * m) by rw [Nat.pow_mul], Nat.log_pow (by decide)] + +private theorem logBank_injective : Function.Injective logBank := by + intro i j h + apply Fin.ext + simpa only [logBank, Nat.add_left_cancel_iff] using congrArg Fin.val h + +-- This closed preservation test enumerates the finite relocated register bank. +set_option maxRecDepth 4096 in +private theorem log_preserves : ∀ i : Fin 320, + i.val < 96 ∨ 100 ≤ i.val → logarithm.Preserves i := by decide + +/-- The computed logarithm is read from the actual existing loop, with no logarithm input +certificate. Its charge is `8m+5` at a power of four. -/ +theorem exec_logarithm {W m : ℕ} (x : Data 320) + (hD : x.regs Reg.source = 4 ^ m) (hfit : Fits W (4 ^ m + 2 * m + 3)) : + ∃ y, ExecWithin W logarithm x y (8 * m + 5) ∧ + y.regs Reg.destination = 2 * m ∧ y.mem = x.mem ∧ + ∀ i : Fin 320, i.val < 96 ∨ 100 ≤ i.val → y.regs i = x.regs i := by + have harg : x.regs (logBank NatLog.arg) = 4 ^ m := hD + obtain ⟨y, hy, hr, hm, -, -⟩ := NatLog.exec_rename logBank logBank_injective x + (hfit.of_le (by omega)) (by rw [harg]; exact hfit.of_le (by omega)) + (by rw [harg, log_two_four_pow]; exact hfit.of_le (by omega)) + refine ⟨y, ?_, ?_, hm, fun i hi => hy.regs_eq (log_preserves i hi)⟩ + · have he : 4 * Nat.log 2 (x.regs (logBank NatLog.arg)) + 5 = 8 * m + 5 := by + rw [harg, log_two_four_pow]; omega + simpa only [logarithm, he] using hy + · rw [harg, log_two_four_pow] at hr + exact hr + +/-- Read an actual six-word producer record at its computed ordinal. The input memory is +unchanged; arbitrary source words are loaded, rather than supplied as predecoded registers. -/ +theorem exec_readRecord {W n D i out b : ℕ} (x : Data 320) (v : Fin 6 → ℕ) + (hD : x.mem 1 = D) (hn : x.mem 3 = n) + (hi : x.regs Reg.ordinal = i) (hout : x.regs 39 = out) (hb : x.regs 42 = b) + (hrec : out + i * (6 + 2 * (n * D)) + 6 ≤ b) + (hv : ∀ k : Fin 6, x.mem (out + i * (6 + 2 * (n * D)) + k.val) = v k) + (hfit : Fits W (b + 2 * (n * D) + D + n + 128)) : + ∃ y, ExecWithin W readRecord x y 28 ∧ y.mem = x.mem ∧ + y.regs Reg.dimension = D ∧ y.regs Reg.size = n ∧ + y.regs Reg.area = n * D ∧ y.regs Reg.twiceArea = 2 * (n * D) ∧ + y.regs Reg.base = b ∧ y.regs Reg.record = out + i * (6 + 2 * (n * D)) ∧ + y.regs Reg.rho = v 0 ∧ y.regs Reg.piece = v 1 ∧ y.regs Reg.queries = v 2 ∧ + y.regs Reg.count = v 3 ∧ y.regs Reg.left = v 4 ∧ y.regs Reg.right = v 5 ∧ + y.regs Reg.source = D ∧ y.regs Reg.one = 1 ∧ y.regs Reg.two = 2 ∧ + y.regs Reg.nineteen = 19 ∧ y.regs Reg.four = 4 := by + let r := out + i * (n * D + n * D + 6) + have hmul : n * D + n * D + 6 = 6 + 2 * (n * D) := by omega + have hrec' : r + 6 ≤ b := by simpa only [r, hmul] using hrec + have h1 : Fits W 1 := hfit.of_le (by omega) + have h2 : Fits W 2 := hfit.of_le (by omega) + have h3 : Fits W 3 := hfit.of_le (by omega) + have h4 : Fits W 4 := hfit.of_le (by omega) + have h6 : Fits W 6 := hfit.of_le (by omega) + have h19 : Fits W 19 := hfit.of_le (by omega) + have hA : Fits W (n * D) := hfit.of_le (by omega) + have hAA : Fits W (n * D + n * D) := hfit.of_le (by omega) + have hstride : Fits W (n * D + n * D + 6) := hfit.of_le (by omega) + have his : Fits W (i * (n * D + n * D + 6)) := by + rw [hmul]; exact hfit.of_le (by omega) + have hr : Fits W r := hfit.of_le (by dsimp only [r]; omega) + have hr1 : Fits W (r + 1) := hfit.of_le (by dsimp only [r]; omega) + have hr2 : Fits W (r + 1 + 1) := hfit.of_le (by dsimp only [r]; omega) + have hr3 : Fits W (r + 1 + 1 + 1) := hfit.of_le (by dsimp only [r]; omega) + have hr4 : Fits W (r + 1 + 1 + 1 + 1) := hfit.of_le (by dsimp only [r]; omega) + have hr5 : Fits W (r + 1 + 1 + 1 + 1 + 1) := hfit.of_le (by dsimp only [r]; omega) + have hv0 : x.mem r = v 0 := by simpa only [r, hmul, Fin.val_zero, Nat.add_zero] using hv 0 + have hv1 : x.mem (r + 1) = v 1 := by simpa +decide [r, hmul] using hv ⟨1, by decide⟩ + have hv2 : x.mem (r + 1 + 1) = v 2 := by + change x.mem (r + 2) = v 2 + simpa +decide [r, hmul] using hv ⟨2, by decide⟩ + have hv3 : x.mem (r + 1 + 1 + 1) = v 3 := by + change x.mem (r + 3) = v 3 + simpa +decide [r, hmul] using hv ⟨3, by decide⟩ + have hv4 : x.mem (r + 1 + 1 + 1 + 1) = v 4 := by + change x.mem (r + 4) = v 4 + simpa +decide [r, hmul] using hv ⟨4, by decide⟩ + have hv5 : x.mem (r + 1 + 1 + 1 + 1 + 1) = v 5 := by + change x.mem (r + 5) = v 5 + simpa +decide [r, hmul] using hv ⟨5, by decide⟩ + let y := x.set Reg.one 1 |>.set Reg.two 2 |>.set Reg.six 6 |>.set Reg.nineteen 19 + |>.set Reg.four 4 |>.set Reg.address 1 |>.set Reg.dimension D |>.set Reg.address 3 + |>.set Reg.size n |>.set Reg.area (n * D) |>.set Reg.twiceArea (n * D + n * D) + |>.set Reg.address (n * D + n * D + 6) + |>.set Reg.address (i * (n * D + n * D + 6)) |>.set Reg.record r |>.set Reg.base b + |>.set Reg.address r |>.set Reg.rho (v 0) |>.set Reg.address (r + 1) + |>.set Reg.piece (v 1) |>.set Reg.address (r + 1 + 1) |>.set Reg.queries (v 2) + |>.set Reg.address (r + 1 + 1 + 1) |>.set Reg.count (v 3) + |>.set Reg.address (r + 1 + 1 + 1 + 1) |>.set Reg.left (v 4) + |>.set Reg.address (r + 1 + 1 + 1 + 1 + 1) |>.set Reg.right (v 5) |>.set Reg.source D + refine ⟨y, ?run, ?post⟩ + case run => + ram_eval [readRecord, y, hi, hout, hb, hD, hn, h1, h2, h3, h4, h6, h19, hA, hAA, + hstride, his, hr, hr1, hr2, hr3, hr4, hr5, r, hv0, hv1, hv2, hv3, hv4, hv5, + Reg.one, Reg.two, Reg.six, Reg.nineteen, Reg.four, Reg.address, Reg.dimension, + Reg.size, Reg.area, Reg.twiceArea, Reg.ordinal, Reg.record, Reg.base, Reg.rho, + Reg.piece, Reg.queries, Reg.count, Reg.left, Reg.right, Reg.source] + case post => + simp +decide [y, r, two_mul, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc] + +end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Entry.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Entry.lean new file mode 100644 index 0000000000..c39594b239 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Entry.lean @@ -0,0 +1,145 @@ +/- +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.ExactTriangle.RecordProduct.First + +/-! +# Initialized producer-to-adapter composition + +One fixed native program runs the complete producer from its original four headers and three +signed weight arrays, selects actual ordinal zero and invokes the actual record consumer. +The general caller interface handles any occupied ordinal; the initialized client here chooses +the first one with real code. Its existence follows from the original positive geometry. + +The producer's pre-halt native witness and polynomial word bound derive every source pointer, +coordinate, caller base and dirty-word bound used by the record consumer. No producer layout, +run, solver or time certificate is an input hypothesis. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct + +open Cslib.WordRAM Cslib.Algorithms.ExactTriangle Cslib.Matrix +open Cslib.Algorithms.MatrixMultiplication.Schonhage +open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage + +/-- The complete real producer, using its original low bank. -/ +@[expose] def produce : Code .standard 320 := Instances.program.rename producerBank + +/-- One fixed initialized composition; selecting the first record costs one actual instruction. -/ +@[expose] def entryProgram : Code .standard 320 := + .seq produce (.seq (.op (.const Reg.ordinal 0)) program) + +/-- The unchanged producer's original-header budget, including its standalone halt. -/ +@[expose] def preparationTime (n D g p : ℕ) (values : List ℤ) : ℕ := + let C := fun rho => Nat.count (fun q => (values.getD q 0 % (p : ℤ)).toNat = rho) (n * n) + Instances.timeBound n D p (ChunkCatalogue.before C (queryCap n D) p) (numPieces n D g) + +private theorem producerBank_injective : Function.Injective producerBank := by + intro i j h + apply Fin.ext + exact congrArg (fun k : Fin 320 => k.val) h + +/-- Complete initialized structured execution. The actual producer execution is a conclusion, +and its same native memory supplies the coordinate list consumed by the composed adapter. -/ +theorem exec_input {W m n g p A : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hD : 16 ≤ D m) + (hg : 1 ≤ g) (hp : 0 < p) (hN : D m ^ 18 ≤ n) + (hv : ∀ z ∈ values, z.natAbs ≤ A) (hW : admissionWidth n (D m) g p A ≤ W) : + InputFits W (PreparationInput.input n (D m) g p values) ∧ + let hn : 0 < n := lt_of_lt_of_le (by omega : 0 < D m) + ((Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN) + ∃ a : Data 64, ∃ idx : InstanceIndex p, + ExecWithin W Instances.program (.init (PreparationInput.input n (D m) g p values)) a + (preparationTime n (D m) g p values - 1) ∧ + idx ∈ instanceIndices (fun a b : Fin n => values.getD (pairIndex (a, b)) 0) (D m) g p ∧ + recordOrdinal n (D m) g p (fun q => values.getD q 0) idx = 0 ∧ + let qs := decodedQueries hn a.mem (recordQueries n (D m) p idx) + (recordQueryCount n (D m) p (fun q => values.getD q 0) idx) + ∃ y, ExecWithin W entryProgram (.init (PreparationInput.input n (D m) g p values)) y + (preparationTime n (D m) g p values + timeBound (m := m) qs) ∧ + y.regs Reg.result = a.regs Instances.heap + + QueriedProduct.outputBase (19 * m) m n qs.length ∧ + (∀ j : Fin qs.length, + y.mem (a.regs Instances.heap + + (QueriedProduct.outputBase (19 * m) m n qs.length + j.val)) = + Signed.encode ((leftMatrix m n g p (fun q => values.getD q 0) idx * + rightMatrix m n g p (fun q => values.getD q 0) idx) (qs.get j).1 (qs.get j).2)) ∧ + (∀ u, u < a.regs Instances.heap ∨ + a.regs Instances.heap + CallableProduct.windowSize n qs.length ≤ u → + y.mem u = a.mem u) ∧ + (∀ j : Fin 64, y.regs (producerBank j) = a.regs j) ∧ + qs.length * 2 ^ m ≤ n ^ 2 := by + have hDn : D m ≤ n := (Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN + have hw : PreparationInput.width n (D m) g p A ≤ W := by + unfold admissionWidth at hW + omega + obtain ⟨a, ha, houtput, hinput, abound⟩ := PreparationInput.exec_input values hlen + (by omega) hDn hg hp hv hw + have ha' : ExecWithin W Instances.program (.init (PreparationInput.input n (D m) g p values)) a + (preparationTime n (D m) g p values - 1) := ha + let x₀ : Data 320 := .init (PreparationInput.input n (D m) g p values) + let x := a.extend producerBank x₀ + have hx : ExecWithin W produce x₀ x (preparationTime n (D m) g p values - 1) := + ha'.rename producerBank_injective + obtain ⟨t, ht, he⟩ := ha' + have hr : Runs W PreparationInput.flatProgram + (State.init (PreparationInput.input n (D m) g p values)) + ⟨Instances.program.size, a⟩ t := by + simpa only [Nat.zero_add, State.init] using he.runs (pc := 0) + (p := PreparationInput.flatProgram) (Program.Contains.self _).append_left + have hwords := PreparationInput.bounded_reachable values hlen (by omega) hDn hg hp hv hw + ⟨Instances.program.size, a⟩ t hr + obtain ⟨idx, hidx, hord⟩ := first_index (n := n) (D := D m) (g := g) (p := p) + (fun q => values.getD q 0) hD hDn hg (by omega) + let z := x.set Reg.ordinal 0 + have hz : ExecWithin (B := .standard) W (.op (.const Reg.ordinal 0)) x z 1 := + ExecWithin.const (fits_zero W) + have zmap : z.comap producerBank = a := by + ext j + · change Function.update x.regs Reg.ordinal 0 (producerBank j) = a.regs j + have hne : producerBank j ≠ Reg.ordinal := by + intro heq + have hh := congrArg Fin.val heq + change j.val = 64 at hh + omega + rw [Function.update_of_ne hne] + exact producerBank_injective.extend_apply _ _ j + · rfl + have hheap : z.regs 42 = a.regs Instances.heap := by + exact congrArg (fun d : Data 64 => d.regs Instances.heap) zmap + have hQ : recordQueryCount n (D m) p (fun q => values.getD q 0) idx ≤ n ^ 2 := by + unfold recordQueryCount + rw [pow_two] + exact (min_le_right _ _).trans ((Nat.sub_le _ _).trans (Nat.count_le _)) + have hfit := physical_fits (b := z.regs 42) (n := n) (D := D m) (g := g) (p := p) (A := A) + (Q := recordQueryCount n (D m) p (fun q => values.getD q 0) idx) + (by rw [hheap]; exact (hwords.1 Instances.heap).le) hQ hW + have zout : Instances.Output n (D m) g p (fun q => values.getD q 0) + (.init (PreparationInput.input n (D m) g p values)) (z.comap producerBank) := by + rw [zmap] + exact houtput + obtain ⟨y, hy, yr, yv, yf, yg, yQ⟩ := exec_of_output (fun q => values.getD q 0) + (.init (PreparationInput.input n (D m) g p values)) z zout hD hg (by omega) hN + rfl rfl idx hidx (by + simpa only [z, Data.set_regs, Function.update_self] using hord.symm) hfit + have hmem : z.mem = a.mem := rfl + simp only [hheap, hmem] at hy yr yv yf yQ + refine ⟨hinput, a, idx, ⟨t, ht, he⟩, hidx, hord, y, ?_, yr, yv, yf, ?_, yQ⟩ + · have hpos : 1 ≤ preparationTime n (D m) g p values := by + dsimp only [preparationTime, Instances.timeBound] + omega + exact (hx.seq (hz.seq hy)).mono (by omega) + · intro j + have hj : j.val < 64 := j.isLt + rw [yg (producerBank j) (by change j.val < 65; omega)] + exact congrArg (fun d : Data 64 => d.regs j) zmap + +end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Exec.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Exec.lean new file mode 100644 index 0000000000..bc0f824b11 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Exec.lean @@ -0,0 +1,88 @@ +/- +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.ExactTriangle.RecordProduct.Prepare + +/-! +# Complete native per-record product execution + +The native preparation is followed by the complete existing callable product. Every returned +word answers its original occurrence; the whole producer catalogue remains below the owned +window and is preserved. These are internal readback composition rules; the producer client +discharges their descriptor and source-span assertions from its actual initialized execution. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct + +open Cslib.WordRAM +open Cslib.Algorithms.MatrixMultiplication.Schonhage +open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage + +/-- The complete per-record charge includes actual decoding, copying and callee invocation. -/ +@[expose] def timeBound {m n : ℕ} (qs : List (Fin n × Fin n)) : ℕ := + CallableProduct.timeBound (m := m) qs + 8 * m + 14 * (n * D m) + 14 * qs.length + 71 + +/-- All preparation arithmetic and the original input lie below the already computed virtual +window. This follows from the existing actual product admission, rather than an input fit table. -/ +theorem preparation_margin {m n Q : ℕ} (hN : D m ^ 18 ≤ n) : + 2 * (n * D m) + 2 * Q + 20 * m + D m + n + 256 < CallableProduct.windowSize n Q := by + have hD : D m ≤ n := (Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN + have hbudget := (CallableProduct.source_admission (Q := Q) hN).2.2 + change QueriedProduct.wordBudget (19 * m) m n Q < CallableProduct.windowSize n Q at hbudget + unfold QueriedProduct.wordBudget QueriedProduct.inputEnd at hbudget + omega + +/-- Actual record-to-product execution, with only original input/readback premises and no +solver/run/time oracle. The final initialized client derives these premises from the producer. -/ +theorem exec {W b m n i out rho piece s t q : ℕ} + (X : Matrix (Fin n) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin n) ℤ) + (qs : List (Fin n × Fin n)) (x : Data 320) + (hD : x.mem 1 = D m) (hn : x.mem 3 = n) + (hi : x.regs Reg.ordinal = i) (hout : x.regs 39 = out) (hb : x.regs 42 = b) + (hrec : out + i * (6 + 2 * (n * D m)) + 6 ≤ b) + (hrecord : (Block.mk (out + i * (6 + 2 * (n * D m))) 6).Realizes x.mem + ![rho, piece, q, qs.length, s, t]) + (hsb : s + n * D m ≤ b) (htb : t + n * D m ≤ b) + (hqb : q + 2 * qs.length ≤ b) + (hleft : ∀ a < n * D m, x.mem (s + a) = + (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem (5 + a)) + (hright : ∀ a < n * D m, x.mem (t + a) = + (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem + (5 + n * D m + a)) + (hqueries : ∀ a < 2 * qs.length, x.mem (q + a) = + (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem + (5 + 2 * (n * D m) + a)) + (hX : ∀ a k, 0 ≤ X a k ∧ X a k ≤ 1) (hY : ∀ k a, 0 ≤ Y k a ∧ Y k a ≤ 1) + (hN : D m ^ 18 ≤ n) + (hfit : Fits W (2 * b + 4 * CallableProduct.windowSize n qs.length + 1024)) : + ∃ y, ExecWithin W program x y (timeBound (m := m) qs) ∧ + y.regs Reg.result = b + QueriedProduct.outputBase (19 * m) m n qs.length ∧ + (∀ j : Fin qs.length, + y.mem (b + (QueriedProduct.outputBase (19 * m) m n qs.length + j.val)) = + Signed.encode ((X * Y) (qs.get j).1 (qs.get j).2)) ∧ + (∀ a, a < b ∨ b + CallableProduct.windowSize n qs.length ≤ a → y.mem a = x.mem a) ∧ + ∀ j : Fin 320, j.val < 65 → y.regs j = x.regs j := by + have hmargin := preparation_margin (Q := qs.length) hN + obtain ⟨a, ha, ab, ain, af, ar⟩ := exec_prepare X Y qs x hD hn hi hout hb hrec hrecord + hsb htb hqb hleft hright hqueries (hfit.of_le (by omega)) + obtain ⟨y, hy, yr, yv, yi, yf, yg⟩ := exec_invoke X Y qs a ab ain hX hY hN + (hfit.of_le (by omega)) + refine ⟨y, (ha.seq hy).mono (by unfold timeBound; omega), yr, yv, ?_, ?_⟩ + · intro j hj + rw [yf j hj] + apply af j + unfold QueriedProduct.inputEnd + omega + · intro j hj + have hne : j ≠ Reg.result := by intro h; subst j; simp [Reg.result] at hj + exact (yg j (by omega) hne).trans (ar j hj) + +end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/First.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/First.lean new file mode 100644 index 0000000000..b3828cd256 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/First.lean @@ -0,0 +1,67 @@ +/- +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.ExactTriangle.RecordProduct.Bounds + +/-! +# The actual first prepared record exists + +The fixed initialized composition selects ordinal zero. An original vertex pair belongs to +one existing residue class, so that class has a chunk and the vertex set has a piece. The native +ordinal characterization then supplies the unique existing finite index of the first record. +No nonempty catalogue or index certificate is an extra runtime input. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct + +open Cslib.WordRAM Cslib.Algorithms.ExactTriangle Cslib.Matrix + +/-- Under the real producer geometry, ordinal zero always names an existing finite instance. -/ +theorem first_index {n D g p : ℕ} (values : ℕ → ℤ) + (hD : 16 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : p ≠ 0) : + ∃ idx : InstanceIndex p, + idx ∈ instanceIndices (fun a b : Fin n => values (pairIndex (a, b))) D g p ∧ + recordOrdinal n D g p values idx = 0 := by + let wAB := fun a b : Fin n => values (pairIndex (a, b)) + let R := fun q => (values q % (p : ℤ)).toNat + let C := fun rho => Nat.count (fun q => R q = rho) (n * n) + have hn : 0 < n := by omega + let a : Fin n := ⟨0, hn⟩ + let rho := resFin hp (wAB a a) + have hmem : (a, a) ∈ residueClass wAB p rho := + (mem_residueClass wAB hp rho (a, a)).mpr rfl + have hcard : 0 < (residueClass wAB p rho).card := Finset.card_pos.mpr ⟨_, hmem⟩ + have hcap : 0 < queryCap n D := one_le_queryCap (by omega) hDn + have hchunks : 0 < numChunks (residueClass wAB p rho) (queryCap n D) := by + have hc : (residueClass wAB p rho).card ≤ + numChunks (residueClass wAB p rho) (queryCap n D) * queryCap n D := + Nat.le_ceilDiv_mul hcap + by_contra h + have he : numChunks (residueClass wAB p rho) (queryCap n D) = 0 := by omega + rw [he, Nat.zero_mul] at hc + omega + have hpieces : 0 < numPieces n D g := by + have hc : n ≤ numPieces n D g * pieceSize D g := + Nat.le_ceilDiv_mul (pieceSize_pos hD hg) + by_contra h + have he : numPieces n D g = 0 := by omega + rw [he, Nat.zero_mul] at hc + omega + have hnonempty : (instanceIndices wAB D g p).Nonempty := by + refine ⟨(rho, 0, 0), (mem_instanceIndices wAB _).mpr ⟨hchunks, hpieces⟩⟩ + have hcount : 0 < ChunkCatalogue.before C (queryCap n D) p * numPieces n D g := by + rw [QuerySpec.before_mul_numPieces wAB hp R (by intro q; rfl)] + exact Finset.card_pos.mpr hnonempty + obtain ⟨idx, ⟨hidx, hzero⟩, -⟩ := PreparationSpec.index_unique values wAB hp + (by intro a b; rfl) hD hDn hg 0 hcount + exact ⟨idx, hidx, hzero.symm⟩ + +end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Flat.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Flat.lean new file mode 100644 index 0000000000..ebf559ed3b --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Flat.lean @@ -0,0 +1,99 @@ +/- +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.ExactTriangle.RecordProduct.Entry + +/-! +# Initialized flat native producer and product runs + +The original four scalar headers and three signed weight arrays initialize one fixed native +program. Prefix `Runs`, the charged final halt, exact answer words and the caller frame all +refer to the same actual final data. The initialized client selects the first actual record; +the caller interface `exec_of_output` supports every occupied ordinal. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct + +open Cslib.WordRAM Cslib.Algorithms.ExactTriangle Cslib.Matrix +open Cslib.Algorithms.MatrixMultiplication.Schonhage +open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage + +/-- Fixed register count, instruction bound including halt, and physical-width independence. -/ +theorem entryProgram_fixed : (entryProgram.program Reg.result).length ≤ 132352 ∧ + ¬(entryProgram.program Reg.result).ReadsWidth := by + constructor + · simp only [Code.program, List.length_append, Code.length_assemble, + List.length_singleton, entryProgram, Code.size, produce, Code.size_rename] + have hc := program_fixed.1 + have hp := Instances.program_fixed.1 + omega + · apply Code.not_readsWidth_program + simp only [entryProgram, Code.ReadsWidth, produce, Code.readsWidth_rename, Op.ReadsWidth, + false_or] + exact not_or.mpr ⟨Instances.program_fixed.2, program_fixed.2⟩ + +/-- Every sufficiently wide physical execution starts from the actual original input and +returns the first prepared record's exact requested product values. There is no supplied +layout, run, time, sparse-count or solver certificate. Source prime selection and the outer +instance loop are separate; this theorem alone is not an aggregate ExactTriangle bound. -/ +theorem runs_input {W m n g p A : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hD : 16 ≤ D m) + (hg : 1 ≤ g) (hp : 0 < p) (hN : D m ^ 18 ≤ n) + (hv : ∀ z ∈ values, z.natAbs ≤ A) (hW : admissionWidth n (D m) g p A ≤ W) : + InputFits W (PreparationInput.input n (D m) g p values) ∧ + let hn : 0 < n := lt_of_lt_of_le (by omega : 0 < D m) + ((Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN) + ∃ a : Data 64, ∃ idx : InstanceIndex p, + ExecWithin W Instances.program (.init (PreparationInput.input n (D m) g p values)) a + (preparationTime n (D m) g p values - 1) ∧ + idx ∈ instanceIndices (fun a b : Fin n => values.getD (pairIndex (a, b)) 0) (D m) g p ∧ + recordOrdinal n (D m) g p (fun q => values.getD q 0) idx = 0 ∧ + let qs := decodedQueries hn a.mem (recordQueries n (D m) p idx) + (recordQueryCount n (D m) p (fun q => values.getD q 0) idx) + ∃ y t, t + 1 ≤ preparationTime n (D m) g p values + timeBound (m := m) qs + 1 ∧ + Runs W (entryProgram.program Reg.result) + (State.init (PreparationInput.input n (D m) g p values)) ⟨entryProgram.size, y⟩ t ∧ + Executes W (entryProgram.program Reg.result) + (State.init (PreparationInput.input n (D m) g p values)) + (a.regs Instances.heap + QueriedProduct.outputBase (19 * m) m n qs.length) (t + 1) ∧ + y.Bounded W ∧ + y.regs Reg.result = a.regs Instances.heap + + QueriedProduct.outputBase (19 * m) m n qs.length ∧ + (∀ j : Fin qs.length, + y.mem (a.regs Instances.heap + + (QueriedProduct.outputBase (19 * m) m n qs.length + j.val)) = + Signed.encode ((leftMatrix m n g p (fun q => values.getD q 0) idx * + rightMatrix m n g p (fun q => values.getD q 0) idx) (qs.get j).1 (qs.get j).2)) ∧ + (∀ u, u < a.regs Instances.heap ∨ + a.regs Instances.heap + CallableProduct.windowSize n qs.length ≤ u → + y.mem u = a.mem u) ∧ + (∀ j : Fin 64, y.regs (producerBank j) = a.regs j) ∧ qs.length * 2 ^ m ≤ n ^ 2 := by + obtain ⟨hi, a, idx, ha, hidx, hord, y, hy, yr, yv, yf, yg, hQ⟩ := + exec_input values hlen hD hg hp hN hv hW + have ybound := hy.bounded (Data.Bounded.init hi) + obtain ⟨t, ht, he⟩ := hy + refine ⟨hi, a, idx, ha, hidx, hord, y, t, by omega, ?_, ?_, ybound, yr, yv, yf, yg, hQ⟩ + · simpa only [Nat.zero_add, State.init] using he.runs (pc := 0) + (p := entryProgram.program Reg.result) (Program.Contains.self _).append_left + · simpa only [yr, State.init] using he.executes Reg.result + +/-- Every native prefix is physically word-bounded from the actual admitted original input. +In particular this includes dirty loads before the callable compiler's remainder instruction. -/ +theorem bounded_reachable {W m n g p A k : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hD : 16 ≤ D m) + (hg : 1 ≤ g) (hp : 0 < p) (hN : D m ^ 18 ≤ n) + (hv : ∀ z ∈ values, z.natAbs ≤ A) (hW : admissionWidth n (D m) g p A ≤ W) + {s : State 320} (hr : Runs W (entryProgram.program Reg.result) + (State.init (PreparationInput.input n (D m) g p values)) s k) : s.data.Bounded W := by + have hi := (exec_input values hlen hD hg hp hN hv hW).1 + exact hr.bounded_init hi + +end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Header.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Header.lean new file mode 100644 index 0000000000..3cb3f2ec3d --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Header.lean @@ -0,0 +1,83 @@ +/- +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.ExactTriangle.RecordProduct.Decode + +/-! +# Original callee header stores + +The native stores place the payload length, computed tensor level and recovered inner depth, +outer dimension and actual occurrence count above the producer's heap. No encoded matrix or +query table is supplied by this header. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct + +open Cslib.WordRAM + +/-- Fifteen actual arithmetic/copy/store instructions write the five original header words. +All metadata below register 78, including the complete producer bank, is preserved. -/ +theorem exec_writeHeader {W b m n A Q : ℕ} (x : Data 320) + (hb : x.regs Reg.base = b) (hm : x.regs Reg.destination = 2 * m) + (hA : x.regs Reg.twiceArea = 2 * A) (hQ : x.regs Reg.count = Q) + (hn : x.regs Reg.size = n) (h1 : x.regs Reg.one = 1) (h2 : x.regs Reg.two = 2) + (h19 : x.regs Reg.nineteen = 19) (h4 : x.regs Reg.four = 4) + (hfit : Fits W (b + 19 * m + 2 * A + 2 * Q + 64)) : + ∃ y, ExecWithin W writeHeader x y 15 ∧ + (Block.mk b 5).Realizes y.mem ![4 + 2 * A + 2 * Q, 19 * m, m, n, Q] ∧ + (∀ a, a < b ∨ b + 5 ≤ a → y.mem a = x.mem a) ∧ + ∀ i : Fin 320, i.val < 78 → y.regs i = x.regs i := by + have hdepth : Fits W m := hfit.of_le (by omega) + have hlevel : Fits W (m * 19) := hfit.of_le (by omega) + have hAQ : Fits W (2 * A + Q) := hfit.of_le (by omega) + have hAQQ : Fits W (2 * A + Q + Q) := hfit.of_le (by omega) + have hlen : Fits W (2 * A + Q + Q + 4) := hfit.of_le (by omega) + have hb1 : Fits W (b + 1) := hfit.of_le (by omega) + have hb2 : Fits W (b + 1 + 1) := hfit.of_le (by omega) + have hb3 : Fits W (b + 1 + 1 + 1) := hfit.of_le (by omega) + have hb4 : Fits W (b + 1 + 1 + 1 + 1) := hfit.of_le (by omega) + have hquot : 2 * m / 2 = m := by omega + let y := x.set Reg.depth m |>.set Reg.level (m * 19) + |>.set Reg.payloadLength (2 * A + Q) |>.set Reg.payloadLength (2 * A + Q + Q) + |>.set Reg.payloadLength (2 * A + Q + Q + 4) |>.set Reg.address b + |>.write b (2 * A + Q + Q + 4) |>.set Reg.address (b + 1) |>.write (b + 1) (m * 19) + |>.set Reg.address (b + 1 + 1) |>.write (b + 1 + 1) m + |>.set Reg.address (b + 1 + 1 + 1) |>.write (b + 1 + 1 + 1) n + |>.set Reg.address (b + 1 + 1 + 1 + 1) |>.write (b + 1 + 1 + 1 + 1) Q + have he : ExecWithin W writeHeader x y 15 := by + ram_eval [writeHeader, y, hb, hm, hA, hQ, hn, h1, h2, h19, h4, hquot, hdepth, hlevel, + hAQ, hAQQ, hlen, hb1, hb2, hb3, hb4, Reg.depth, Reg.destination, Reg.two, + Reg.level, Reg.nineteen, Reg.payloadLength, Reg.twiceArea, Reg.count, Reg.four, + Reg.address, Reg.base, Reg.one, Reg.size] + refine ⟨y, he, ?_, ?_, ?_⟩ + · intro j + change y.mem (b + j.val) = _ + fin_cases j <;> simp +decide [y, two_mul, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm, + Nat.mul_comm] + · intro a ha + have h0 : a ≠ b := by omega + have h1 : a ≠ b + 1 := by omega + have h2 : a ≠ b + 1 + 1 := by omega + have h3 : a ≠ b + 1 + 1 + 1 := by omega + have h4 : a ≠ b + 1 + 1 + 1 + 1 := by omega + simp only [y, Data.write_mem, Data.set_mem, Function.update_of_ne h0, + Function.update_of_ne h1, Function.update_of_ne h2, Function.update_of_ne h3, + Function.update_of_ne h4] + · intro i hi + have hdepth : i ≠ Reg.depth := by intro h; subst i; simp [Reg.depth] at hi + have hlevel : i ≠ Reg.level := by intro h; subst i; simp [Reg.level] at hi + have hlen : i ≠ Reg.payloadLength := by + intro h; subst i; simp [Reg.payloadLength] at hi + have haddr : i ≠ Reg.address := by intro h; subst i; simp [Reg.address] at hi + simp only [y, Data.write_regs, Data.set_regs, Function.update_of_ne hdepth, + Function.update_of_ne hlevel, Function.update_of_ne hlen, Function.update_of_ne haddr] + +end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/InputSpec.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/InputSpec.lean new file mode 100644 index 0000000000..3a7c842154 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/InputSpec.lean @@ -0,0 +1,87 @@ +/- +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.ExactTriangle.RecordProduct.Copy + +/-! +# Composing the actual copied spans with the original product input + +The local input meaning uses the unchanged queried-product `State.init` convention. Matrix +and coordinate readback is separated by the three actual source spans; no encoded bands, +routing data or precomputed execution contract is present in these assertions. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct + +open Cslib.WordRAM +open Cslib.Algorithms.MatrixMultiplication.Schonhage +open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage + +/-- The original product's first five memory words, including its actual payload length. -/ +theorem original_header {m n : ℕ} + (X : Matrix (Fin n) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin n) ℤ) + (qs : List (Fin n × Fin n)) : + (Block.mk 0 5).Realizes + (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem + ![4 + 2 * (n * D m) + 2 * qs.length, 19 * m, m, n, qs.length] := by + intro j + change (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem + (0 + j.val) = _ + fin_cases j + · change (QueriedProduct.input true (19 * m) X Y qs).length = _ + have h := QueriedProduct.input_length true (19 * m) X Y qs + unfold QueriedProduct.inputEnd at h + simpa only [Matrix.cons_val_zero'] using + (show (QueriedProduct.input true (19 * m) X Y qs).length = + 4 + 2 * (n * D m) + 2 * qs.length by omega) + · rfl + · rfl + · rfl + · rfl + +/-- Exact readback of the five header words and three copied spans identifies the entire +unchanged original input. This is a pure consequence of those native stores and copies. -/ +theorem local_input {m n b : ℕ} + (X : Matrix (Fin n) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin n) ℤ) + (qs : List (Fin n × Fin n)) (mem : ℕ → ℕ) + (hhead : (Block.mk b 5).Realizes mem + ![4 + 2 * (n * D m) + 2 * qs.length, 19 * m, m, n, qs.length]) + (hleft : ∀ a < n * D m, mem (b + 5 + a) = + (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem (5 + a)) + (hright : ∀ a < n * D m, mem (b + 5 + n * D m + a) = + (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem + (5 + n * D m + a)) + (hqueries : ∀ a < 2 * qs.length, mem (b + 5 + 2 * (n * D m) + a) = + (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem + (5 + 2 * (n * D m) + a)) : + ∀ a, a < QueriedProduct.inputEnd m n qs.length → mem (b + a) = + (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem a := by + intro a ha + unfold QueriedProduct.inputEnd at ha + by_cases h5 : a < 5 + · have hh := hhead ⟨a, h5⟩ + have hs := original_header X Y qs ⟨a, h5⟩ + change mem (b + a) = _ at hh + change (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem + (0 + a) = _ at hs + exact hh.trans (by simpa only [Nat.zero_add] using hs.symm) + by_cases hl : a < 5 + n * D m + · have h := hleft (a - 5) (by omega) + simpa only [Nat.add_assoc, Nat.add_sub_of_le (by omega : 5 ≤ a)] using h + by_cases hr : a < 5 + 2 * (n * D m) + · have h := hright (a - (5 + n * D m)) (by omega) + have he : 5 + n * D m + (a - (5 + n * D m)) = a := by omega + simpa only [Nat.add_assoc, ← Nat.add_assoc 5 (n * D m), he] using h + · have h := hqueries (a - (5 + 2 * (n * D m))) (by omega) + have he : 5 + 2 * (n * D m) + (a - (5 + 2 * (n * D m))) = a := by omega + simpa only [Nat.add_assoc, ← Nat.add_assoc 5 (2 * (n * D m)), he] using h + +end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Kernel.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Kernel.lean new file mode 100644 index 0000000000..2c916b38d8 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Kernel.lean @@ -0,0 +1,119 @@ +/- +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.ExactTriangle.RecordProduct.Program + +/-! +# Relocated native copy and queried-product calls + +All registers of each existing native program are renamed together. Memory relocation is +performed by the callable product's actual address compiler, not by register renaming. +These internal execution rules preserve the low producer bank and full outside-memory frame. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct + +open Cslib.WordRAM +open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage +open Cslib.Algorithms.MatrixMultiplication.Schonhage + +theorem copyBank_injective : Function.Injective copyBank := by + intro i j h + apply Fin.ext + simpa only [copyBank, Nat.add_left_cancel_iff] using congrArg Fin.val h + +theorem calleeBank_injective : Function.Injective calleeBank := by + intro i j h + apply Fin.ext + simpa only [calleeBank, Nat.add_left_cancel_iff] using congrArg Fin.val h + +/-- The real copy loop preserves all adapter metadata and the complete producer register bank. -/ +theorem exec_copy {W s d n : ℕ} (x : Data 320) + (hs : x.regs Reg.source = s) (hd : x.regs Reg.destination = d) + (hn : x.regs Reg.length = n) (hsep : s + n ≤ d) + (hfit : Fits W (s + d + n + 2)) : + ∃ y, ExecWithin W copy x y (7 * n + 4) ∧ + y.mem = ArrayCopy.copyPrefix x.mem s d n ∧ + y.regs Reg.source = s ∧ y.regs Reg.destination = d ∧ y.regs Reg.length = n ∧ + ∀ i : Fin 320, i.val < 96 ∨ 103 ≤ i.val → y.regs i = x.regs i := by + have hs' : (x.comap copyBank).regs ArrayCopy.src = s := hs + have hd' : (x.comap copyBank).regs ArrayCopy.dst = d := hd + have hn' : (x.comap copyBank).regs ArrayCopy.len = n := hn + obtain ⟨a, ha, am, asrc, adst, alen⟩ := ArrayCopy.exec (x.comap copyBank) + (hfit.of_le (by omega)) + (by rw [hs', hn']; exact hfit.of_le (by omega)) + (by rw [hd', hn']; exact hfit.of_le (by omega)) (by simpa only [hs', hd', hn'] using hsep) + refine ⟨a.extend copyBank x, ?_, ?_, ?_, ?_, ?_, ?_⟩ + · simpa only [copy, hn'] using ha.rename copyBank_injective + · simpa only [Data.extend, Data.comap_mem, hs', hd', hn'] using am + · exact (copyBank_injective.extend_apply _ _ ArrayCopy.src).trans (asrc.trans hs') + · exact (copyBank_injective.extend_apply _ _ ArrayCopy.dst).trans (adst.trans hd') + · exact (copyBank_injective.extend_apply _ _ ArrayCopy.len).trans (alen.trans hn') + · intro i hi + apply Function.extend_apply' + rintro ⟨j, hj⟩ + have h := congrArg Fin.val hj + change 96 + j.val = i.val at h + omega + +/-- The concrete original-input callee derives its execution from the matrices and coordinate +occurrences. No execution or time certificate is accepted by this invocation rule. -/ +theorem exec_invoke {W b m N : ℕ} + (X : Matrix (Fin N) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin N) ℤ) + (qs : List (Fin N × Fin N)) (x : Data 320) (hb : x.regs Reg.base = b) + (hinput : ∀ a, a < QueriedProduct.inputEnd m N qs.length → + x.mem (b + a) = + (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem a) + (hX : ∀ i k, 0 ≤ X i k ∧ X i k ≤ 1) (hY : ∀ k j, 0 ≤ Y k j ∧ Y k j ≤ 1) + (hN : D m ^ 18 ≤ N) (hfit : Fits W (b + 4 * CallableProduct.windowSize N qs.length + 1024)) : + ∃ y, ExecWithin W invoke x y (CallableProduct.timeBound (m := m) qs + 2) ∧ + y.regs Reg.result = b + QueriedProduct.outputBase (19 * m) m N qs.length ∧ + (∀ i : Fin qs.length, + y.mem (b + (QueriedProduct.outputBase (19 * m) m N qs.length + i.val)) = + Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧ + (∀ a, a < QueriedProduct.inputEnd m N qs.length → y.mem (b + a) = x.mem (b + a)) ∧ + (∀ a, a < b ∨ b + CallableProduct.windowSize N qs.length ≤ a → y.mem a = x.mem a) ∧ + ∀ i : Fin 320, i.val < 128 → i ≠ Reg.result → y.regs i = x.regs i := by + let z := x.set (calleeBank CallableProduct.Reg.base) b + have hz : ExecWithin (B := .standard) W + (.op (.copy (calleeBank CallableProduct.Reg.base) Reg.base)) x z 1 := by + simpa only [z, hb] using + (ExecWithin.copy (w := W) (x := x) (d := calleeBank CallableProduct.Reg.base) + (s := Reg.base)) + have zb : (z.comap calleeBank).regs CallableProduct.Reg.base = b := by simp [z] + obtain ⟨a, ha, ar, ab, aM, av, ai, af⟩ := + CallableProduct.exec X Y qs (z.comap calleeBank) zb hinput hX hY hN hfit + let c := a.extend calleeBank z + have hc : ExecWithin W (CallableProduct.program.rename calleeBank) z c + (CallableProduct.timeBound (m := m) qs) := ha.rename calleeBank_injective + have cr : c.regs (calleeBank CallableProduct.Reg.result) = + b + QueriedProduct.outputBase (19 * m) m N qs.length := + (calleeBank_injective.extend_apply _ _ _).trans ar + let y := c.set Reg.result (b + QueriedProduct.outputBase (19 * m) m N qs.length) + have hy : ExecWithin (B := .standard) W + (.op (.copy Reg.result (calleeBank CallableProduct.Reg.result))) c y 1 := by + simpa only [y, cr] using (ExecWithin.copy (w := W) (x := c) (d := Reg.result) + (s := calleeBank CallableProduct.Reg.result)) + refine ⟨y, ?_, by simp [y], av, ai, af, ?_⟩ + · exact (hz.seq (hc.seq hy)).mono (by omega) + · intro i hi hne + have hbank : ¬∃ j, calleeBank j = i := by + rintro ⟨j, hj⟩ + have h := congrArg Fin.val hj + change 128 + j.val = i.val at h + omega + have hiz : i ≠ calleeBank CallableProduct.Reg.base := by + intro h + exact hbank ⟨_, h.symm⟩ + simp only [y, Data.set_regs, Function.update_of_ne hne, c, Data.extend, + Function.extend_apply' _ _ _ hbank, z, Function.update_of_ne hiz] + +end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Prepare.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Prepare.lean new file mode 100644 index 0000000000..769a2ae087 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Prepare.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.ExactTriangle.RecordProduct.InputSpec + +/-! +# Complete record-to-original-input preparation + +All runtime metadata is read by the real descriptor code. The logarithm, five original-header +stores and three native array copies compose to linear preparation work. The readback premises +here are internal; the producer client derives them from the actual prepared instance. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct + +open Cslib.WordRAM +open Cslib.Algorithms.MatrixMultiplication.Schonhage +open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage + +-- The finite preservation test traverses the relocated 320-register code. +set_option maxRecDepth 4096 in +private theorem read_preserves : ∀ i : Fin 320, i.val < 65 → readRecord.Preserves i := by decide + +/-- Complete native preparation from a selected record and its actual three source spans. +No source execution, encoded matrix or routing table is supplied. -/ +theorem exec_prepare {W b m n i out rho piece s t q : ℕ} + (X : Matrix (Fin n) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin n) ℤ) + (qs : List (Fin n × Fin n)) (x : Data 320) + (hD : x.mem 1 = D m) (hn : x.mem 3 = n) + (hi : x.regs Reg.ordinal = i) (hout : x.regs 39 = out) (hb : x.regs 42 = b) + (hrec : out + i * (6 + 2 * (n * D m)) + 6 ≤ b) + (hrecord : (Block.mk (out + i * (6 + 2 * (n * D m))) 6).Realizes x.mem + ![rho, piece, q, qs.length, s, t]) + (hsb : s + n * D m ≤ b) (htb : t + n * D m ≤ b) + (hqb : q + 2 * qs.length ≤ b) + (hleft : ∀ a < n * D m, x.mem (s + a) = + (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem (5 + a)) + (hright : ∀ a < n * D m, x.mem (t + a) = + (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem + (5 + n * D m + a)) + (hqueries : ∀ a < 2 * qs.length, x.mem (q + a) = + (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem + (5 + 2 * (n * D m) + a)) + (hfit : Fits W (2 * b + 2 * (n * D m) + 2 * qs.length + 20 * m + D m + n + 256)) : + ∃ y, ExecWithin W prepare x y (8 * m + 14 * (n * D m) + 14 * qs.length + 69) ∧ + y.regs Reg.base = b ∧ + (∀ a, a < QueriedProduct.inputEnd m n qs.length → y.mem (b + a) = + (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem a) ∧ + (∀ a, a < b ∨ b + QueriedProduct.inputEnd m n qs.length ≤ a → y.mem a = x.mem a) ∧ + ∀ j : Fin 320, j.val < 65 → y.regs j = x.regs j := by + obtain ⟨r, hr, rm, rD, rn, rA, rAA, rb, rrec, rrho, rpiece, rq, rQ, rs, rt, + rarg, r1, r2, r19, r4⟩ := exec_readRecord x ![rho, piece, q, qs.length, s, t] + hD hn hi hout hb hrec hrecord (hfit.of_le (by omega)) + have rq' : r.regs Reg.queries = q := by simpa +decide using rq + have rQ' : r.regs Reg.count = qs.length := by simpa +decide using rQ + have rs' : r.regs Reg.left = s := by simpa +decide using rs + have rt' : r.regs Reg.right = t := by simpa +decide using rt + obtain ⟨l, hl, lmDepth, lm, lr⟩ := exec_logarithm r rarg (hfit.of_le (by + change D m + 2 * m + 3 ≤ _ + omega)) + have lb : l.regs Reg.base = b := (lr _ (by decide)).trans rb + obtain ⟨h, hh, hhead, hframe, hregs⟩ := exec_writeHeader l lb lmDepth + ((lr _ (by decide)).trans rAA) ((lr _ (by decide)).trans rQ') + ((lr _ (by decide)).trans rn) ((lr _ (by decide)).trans r1) + ((lr _ (by decide)).trans r2) ((lr _ (by decide)).trans r19) + ((lr _ (by decide)).trans r4) (hfit.of_le (by omega)) + have hb' : h.regs Reg.base = b := (hregs _ (by decide)).trans lb + obtain ⟨y, hy, yleft, yright, yqueries, yframe, yregs⟩ := exec_copyInputs h hb' + ((hregs _ (by decide)).trans ((lr _ (by decide)).trans rA)) + ((hregs _ (by decide)).trans ((lr _ (by decide)).trans rQ')) + ((hregs _ (by decide)).trans ((lr _ (by decide)).trans rs')) + ((hregs _ (by decide)).trans ((lr _ (by decide)).trans rt')) + ((hregs _ (by decide)).trans ((lr _ (by decide)).trans rq')) + hsb htb hqb (hfit.of_le (by omega)) + have hread (a : ℕ) (ha : a < b) : h.mem a = x.mem a := + (hframe a (Or.inl ha)).trans (congrFun lm a |>.trans (congrFun rm a)) + refine ⟨y, (hr.seq (hl.seq (hh.seq hy))).mono (by omega), + (yregs _ (by decide) (by decide)).trans hb', ?_, ?_, ?_⟩ + · apply local_input X Y qs y.mem + · intro j + have hj : j.val < 5 := j.isLt + change y.mem (b + j.val) = _ + rw [yframe _ (Or.inl (by omega))] + exact hhead j + · intro a ha + rw [yleft a ha, hread _ (by omega)] + exact hleft a ha + · intro a ha + rw [yright a ha, hread _ (by omega)] + exact hright a ha + · intro a ha + rw [yqueries a ha, hread _ (by omega)] + exact hqueries a ha + · intro a ha + have hI : QueriedProduct.inputEnd m n qs.length = + 5 + 2 * (n * D m) + 2 * qs.length := rfl + rw [yframe _ (by rw [hI] at ha; omega), hframe _ (by rw [hI] at ha; omega), lm, rm] + · intro j hj + have jne : j ≠ Reg.address := by intro h; subst j; simp [Reg.address] at hj + rw [yregs _ (by omega) jne, hregs _ (by omega), lr _ (Or.inl (by omega))] + exact hr.regs_eq (read_preserves j hj) + +end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Producer.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Producer.lean new file mode 100644 index 0000000000..0876048cd6 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Producer.lean @@ -0,0 +1,238 @@ +/- +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.ExactTriangle.RecordProduct.ProducerQueries + +/-! +# Applying the adapter to the actual native producer + +The record, source pointers, original zero/one matrices and ordered coordinate occurrences +are derived from `Instances.Output` and the existing native readback theorems. The initialized +client obtains that output from the actual producer execution, not from an algorithm oracle. +Prime selection, global parameters and the outer ExactTriangle host are separate components. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct + +open Cslib.WordRAM Cslib.Algorithms.ExactTriangle Cslib.Matrix +open Cslib.Algorithms.MatrixMultiplication.Schonhage +open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage + +/-- The unchanged complete producer occupies the original low register bank. -/ +@[expose] def producerBank (i : Fin 64) : Fin 320 := i.castLE (by decide) + +/-- Existing native writer arguments, with pointer fields omitted from the value-only view. -/ +@[expose] def matrixArgs (n D g p rho piece : ℕ) : WriteMatrices.Args := + ⟨0, 0, n, D, p, piece * pieceSize D g, + min (pieceSize D g) (n - piece * pieceSize D g), rho⟩ + +/-- Exact raw left adjacency matrix written by the actual producer. -/ +@[expose] def leftMatrix (m n g p : ℕ) (values : ℕ → ℤ) (idx : InstanceIndex p) : + Matrix (Fin n) (Fin (D m)) ℤ := fun a k => + (WriteMatrices.entry false (matrixArgs n (D m) g p idx.1.val idx.2.2) + (fun q => (values (2 * (n * n) + q) % (p : ℤ)).toNat) (a.val * D m + k.val) : ℤ) + +/-- Exact raw right adjacency matrix, in its actual `D×n` storage order. -/ +@[expose] def rightMatrix (m n g p : ℕ) (values : ℕ → ℤ) (idx : InstanceIndex p) : + Matrix (Fin (D m)) (Fin n) ℤ := fun k a => + (WriteMatrices.entry true (matrixArgs n (D m) g p idx.1.val idx.2.2) + (fun q => (values (n * n + q) % (p : ℤ)).toNat) (k.val * n + a.val) : ℤ) + +/-- Both native writer value functions are raw zero/one words at every index. -/ +theorem entry_le_one (side : Bool) (A : WriteMatrices.Args) (R : ℕ → ℕ) (a : ℕ) : + WriteMatrices.entry side A R a ≤ 1 := by + cases side <;> dsimp only [WriteMatrices.entry] <;> split_ifs <;> omega + +/-- The readback matrices satisfy the raw callee's original-entry hypotheses. -/ +theorem matrices_zero_one (m n g p : ℕ) (values : ℕ → ℤ) (idx : InstanceIndex p) : + (∀ a k, 0 ≤ leftMatrix m n g p values idx a k ∧ + leftMatrix m n g p values idx a k ≤ 1) ∧ + (∀ k a, 0 ≤ rightMatrix m n g p values idx k a ∧ + rightMatrix m n g p values idx k a ≤ 1) := by + constructor <;> intro a k + · exact ⟨Int.natCast_nonneg _, by + dsimp only [leftMatrix] + exact_mod_cast entry_le_one false _ _ _⟩ + · exact ⟨Int.natCast_nonneg _, by + dsimp only [rightMatrix] + exact_mod_cast entry_le_one true _ _ _⟩ + +/-- The actual computed ordinal of an existing finite class/chunk/piece. This is a value +specification for the caller's selection register, not a table supplied to the adapter. -/ +@[expose] def recordOrdinal (n D g p : ℕ) (values : ℕ → ℤ) (idx : InstanceIndex p) : ℕ := + let C := fun rho => Nat.count (fun q => (values q % (p : ℤ)).toNat = rho) (n * n) + (ChunkCatalogue.before C (queryCap n D) idx.1.val + idx.2.1) * numPieces n D g + idx.2.2 + +/-- Actual descriptor occurrence count, rather than an assumed sparse set size. -/ +@[expose] def recordQueryCount (n D p : ℕ) (values : ℕ → ℤ) (idx : InstanceIndex p) : ℕ := + min (queryCap n D) + (Nat.count (fun q => (values q % (p : ℤ)).toNat = idx.1.val) (n * n) - + idx.2.1 * queryCap n D) + +/-- Every occupied finite instance has a nonempty actual descriptor query slice. -/ +theorem recordQueryCount_pos {n D g p : ℕ} (values : ℕ → ℤ) (hp : p ≠ 0) + (hD : 1 ≤ D) (hDn : D ≤ n) (idx : InstanceIndex p) + (hidx : idx ∈ instanceIndices (fun a b : Fin n => values (pairIndex (a, b))) D g p) : + 0 < recordQueryCount n D p values idx := by + let wAB := fun a b : Fin n => values (pairIndex (a, b)) + let R := fun q => (values q % (p : ℤ)).toNat + have hk := ((mem_instanceIndices wAB idx).mp hidx).1 + have hcard := QuerySpec.card_residueClass wAB hp R (by intro q; rfl) idx.1 + have hcap : 0 < queryCap n D := one_le_queryCap hD hDn + have hkcard : idx.2.1 * queryCap n D < (residueClass wAB p idx.1).card := by + by_contra h + have hc := (Nat.ceilDiv_le_iff hcap).mpr + (by omega : (residueClass wAB p idx.1).card ≤ idx.2.1 * queryCap n D) + change idx.2.1 < (residueClass wAB p idx.1).card ⌈/⌉ queryCap n D at hk + omega + rw [hcard] at hkcard + unfold recordQueryCount + change 0 < min (queryCap n D) (Nat.count (fun q => R q = idx.1.val) (n * n) - + idx.2.1 * queryCap n D) + omega + +/-- Actual query pointer into the protected producer catalogue. -/ +@[expose] def recordQueries (n D p : ℕ) (idx : InstanceIndex p) : ℕ := + 5 + 6 * (n * n) + p + 2 * idx.1.val * (n * n) + 2 * (idx.2.1 * queryCap n D) + +-- The composed readback contains nested finite writer-argument structures and vector fields. +set_option maxRecDepth 4096 in +/-- Full adapter execution over a genuine producer output. Every descriptor and source-span +premise of `exec` is derived here from the actual output; none remains an independent caller +certificate. A following initialized client obtains this output by executing the producer. -/ +theorem exec_of_output {W m n g p : ℕ} (values : ℕ → ℤ) + (initial : Data 64) (x : Data 320) + (h : Instances.Output n (D m) g p values initial (x.comap producerBank)) + (hD : 16 ≤ D m) (hg : 1 ≤ g) (hp : p ≠ 0) (hN : D m ^ 18 ≤ n) + (hheaderD : initial.mem 1 = D m) (hheaderN : initial.mem 3 = n) + (idx : InstanceIndex p) + (hidx : idx ∈ instanceIndices (fun a b : Fin n => values (pairIndex (a, b))) (D m) g p) + (hi : x.regs Reg.ordinal = recordOrdinal n (D m) g p values idx) + (hfit : Fits W (2 * x.regs 42 + + 4 * CallableProduct.windowSize n (recordQueryCount n (D m) p values idx) + 1024)) : + let hn : 0 < n := lt_of_lt_of_le (by omega : 0 < D m) + ((Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN) + let qs := decodedQueries hn x.mem (recordQueries n (D m) p idx) + (recordQueryCount n (D m) p values idx) + ∃ y, ExecWithin W program x y (timeBound (m := m) qs) ∧ + y.regs Reg.result = x.regs 42 + QueriedProduct.outputBase (19 * m) m n qs.length ∧ + (∀ j : Fin qs.length, + y.mem (x.regs 42 + (QueriedProduct.outputBase (19 * m) m n qs.length + j.val)) = + Signed.encode ((leftMatrix m n g p values idx * rightMatrix m n g p values idx) + (qs.get j).1 (qs.get j).2)) ∧ + (∀ a, a < x.regs 42 ∨ x.regs 42 + CallableProduct.windowSize n qs.length ≤ a → + y.mem a = x.mem a) ∧ + (∀ j : Fin 320, j.val < 65 → y.regs j = x.regs j) ∧ + qs.length * 2 ^ m ≤ n ^ 2 := by + let wAB := fun a b : Fin n => values (pairIndex (a, b)) + let N := n * n + let R := fun q => (values q % (p : ℤ)).toNat + let C := fun rho => Nat.count (fun q => R q = rho) N + let H := numPieces n (D m) g + let K := ChunkCatalogue.before C (queryCap n (D m)) p + let out := 5 + 6 * N + p + 2 * N * p + 3 * K + let ord := recordOrdinal n (D m) g p values idx + let recordBase := out + ord * (6 + 2 * (n * D m)) + let q := recordQueries n (D m) p idx + let Q := recordQueryCount n (D m) p values idx + have hDn : D m ≤ n := (Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN + have hn : 0 < n := lt_of_lt_of_le (by omega) hDn + let qs := decodedQueries hn x.mem q Q + have hlen : qs.length = Q := decodedQueries_length hn x.mem q Q + obtain ⟨hk, hj⟩ := (mem_instanceIndices wAB idx).mp hidx + have hcard : (residueClass wAB p idx.1).card = C idx.1.val := + QuerySpec.card_residueClass wAB hp R (by intro pair; rfl) idx.1 + have hchunk : idx.2.1 < C idx.1.val ⌈/⌉ queryCap n (D m) := by + simpa only [numChunks, hcard] using hk + have hord := ChunkCatalogue.before_add_lt C (queryCap n (D m)) idx.1.isLt hchunk + have hiCount : ord < K * H := by + have hh := Nat.mul_le_mul_right H (Nat.succ_le_of_lt hord) + change (ChunkCatalogue.before C (queryCap n (D m)) idx.1.val + idx.2.1) * H + + idx.2.2 < K * H + change (ChunkCatalogue.before C (queryCap n (D m)) idx.1.val + idx.2.1 + 1) * H ≤ + K * H at hh + change idx.2.2 < H at hj + rw [Nat.add_mul, Nat.one_mul] at hh + omega + have hfull := h + obtain ⟨yn, yD, yp, yo, yc, yb, yres, ycnt, yscan, ydesc, yblocks, yframe⟩ := h + change x.regs 39 = out at yo + change x.regs 42 = out + (K * H) * (6 + 2 * (n * D m)) at yb + have hrecEnd : recordBase + 6 + 2 * (n * D m) ≤ x.regs 42 := by + have ht := Nat.mul_le_mul_right (6 + 2 * (n * D m)) (Nat.succ_le_of_lt hiCount) + dsimp only [recordBase] + rw [yb] + nlinarith only [ht] + have hcap : 0 < queryCap n (D m) := one_le_queryCap (by omega) hDn + have hkcard : idx.2.1 * queryCap n (D m) < C idx.1.val := by + have hpositive := recordQueryCount_pos values hp (by omega) hDn idx hidx + change 0 < min (queryCap n (D m)) (C idx.1.val - idx.2.1 * queryCap n (D m)) at hpositive + omega + have hQ : idx.2.1 * queryCap n (D m) + Q ≤ N := by + have hc : C idx.1.val ≤ N := Nat.count_le _ + dsimp only [Q, recordQueryCount] + change idx.2.1 * queryCap n (D m) + + min (queryCap n (D m)) (C idx.1.val - idx.2.1 * queryCap n (D m)) ≤ N + omega + have hqEnd : q + 2 * Q ≤ x.regs 42 := by + have hrho := Nat.mul_le_mul_right (2 * N) (Nat.succ_le_of_lt idx.1.isLt) + dsimp only [q, recordQueries] + change 5 + 6 * N + p + 2 * idx.1.val * N + 2 * (idx.2.1 * queryCap n (D m)) + + 2 * Q ≤ _ + rw [yb] + dsimp only [out] + nlinarith only [hQ, hrho, Nat.zero_le (3 * K), + Nat.zero_le (K * H * (6 + 2 * (n * D m)))] + obtain ⟨hdr, hleft, hright⟩ := PreparationSpec.instance_readback values wAB hp + (by intro a b; rfl) hD hDn hg hfull idx hidx + have hcoord := (output_query_coordinates values wAB hp (by intro a b; rfl) + (by omega) hDn hfull idx.1 idx.2.1 hk).1 + rw [hcard] at hcoord + have hc : ∀ j < Q, x.mem (q + 2 * j) < n ∧ x.mem (q + 2 * j + 1) < n := hcoord + have hvalues := matrices_zero_one m n g p values idx + obtain ⟨y, hy, yr, yv, yf, yg⟩ := exec (b := x.regs 42) (i := ord) (out := out) + (rho := idx.1.val) (piece := idx.2.2) (s := recordBase + 6) + (t := recordBase + 6 + n * D m) (q := q) (leftMatrix m n g p values idx) + (rightMatrix m n g p values idx) qs x + ((yframe 1 (Or.inl (by omega))).trans hheaderD) + ((yframe 3 (Or.inl (by omega))).trans hheaderN) hi yo rfl + (by change recordBase + 6 ≤ _; omega) + (by simpa only [hlen, hcard, recordBase, out, ord, recordOrdinal, C, R, N, K, Q, + recordQueryCount, q, recordQueries, Data.comap_mem] using hdr) + (by omega) (by omega) + (by simpa only [hlen] using hqEnd) + (raw_left_words x.mem _ _ qs (by + intro a k + have hflat : a.val * D m + k.val < n * D m := by + have ht := Nat.mul_le_mul_right (D m) a.isLt + rw [Nat.succ_mul] at ht + have := k.isLt + omega + simpa +decide only [leftMatrix, matrixArgs, WriteMatrices.entry, Int.toNat_natCast, + Block.read, Data.comap_mem, recordBase, out, ord, recordOrdinal, K, C, R, N] using + hleft ⟨a.val * D m + k.val, hflat⟩)) + (raw_right_words hn x.mem _ _ qs (by + intro k a + have hflat : k.val * n + a.val < n * D m := by + have ht := Nat.mul_le_mul_right n k.isLt + rw [Nat.succ_mul, Nat.mul_comm (D m) n] at ht + have := a.isLt + omega + simpa only [rightMatrix, matrixArgs, WriteMatrices.entry, Int.toNat_natCast, + Block.read, Data.comap_mem, recordBase, out, ord, recordOrdinal, K, C, R, N] using + hright ⟨k.val * n + a.val, hflat⟩)) + (by simpa only [hlen] using decodedQueries_words hn x.mem _ _ hc) + hvalues.1 hvalues.2 hN (by simpa only [hlen] using hfit) + refine ⟨y, hy, yr, yv, yf, yg, ?_⟩ + rw [hlen] + exact (Nat.mul_le_mul_right (2 ^ m) (min_le_left _ _)).trans (queryCap_mul_two_pow_le n m) + +end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/ProducerQueries.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/ProducerQueries.lean new file mode 100644 index 0000000000..5115fc21f2 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/ProducerQueries.lean @@ -0,0 +1,91 @@ +/- +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.ExactTriangle.RecordProduct.RawInput + +/-! +# Actual producer chunks admit the native query copies + +The class scanner's real coordinate stores and the existing finite chunk theorem derive +in-range query words. Their original occurrence count is the descriptor's computed minimum. +The power-of-four query-capacity bound supplies occurrence sparsity without assuming a sparse +execution or replacing a list length by a set cardinality. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct + +open Cslib.WordRAM Cslib.Algorithms.ExactTriangle Cslib.Matrix +open Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- The existing computed chunk capacity supplies the stronger occurrence bound at `4^m`. -/ +theorem queryCap_mul_two_pow_le (n m : ℕ) : queryCap n (D m) * 2 ^ m ≤ n ^ 2 := by + have hroot := Nat.sqrt_le ((n ^ 2) ^ 2 / D m) + have hmul := (Nat.mul_le_mul_right (D m) hroot).trans + (Nat.div_mul_le_self ((n ^ 2) ^ 2) (D m)) + have hD : D m = (2 ^ m) ^ 2 := by + change 4 ^ m = (2 ^ m) ^ 2 + rw [← Nat.pow_mul, Nat.mul_comm m 2, Nat.pow_mul] + have hs : (queryCap n (D m) * 2 ^ m) ^ 2 ≤ (n ^ 2) ^ 2 := by + change (Nat.sqrt ((n ^ 2) ^ 2 / D m) * 2 ^ m) ^ 2 ≤ _ + rw [mul_pow, ← hD] + simpa only [pow_two] using hmul + nlinarith only [hs, Nat.zero_le (queryCap n (D m) * 2 ^ m), Nat.zero_le (n ^ 2)] + +/-- The producer's actual scanner stores identify every local chunk occurrence with its +unique existing finite pair. Thus neither coordinate range nor the query count is supplied +as an independent adapter certificate. -/ +theorem output_query_coordinates {n D g p : ℕ} (values : ℕ → ℤ) + (wAB : Fin n → Fin n → ℤ) (hp : p ≠ 0) + (hAB : ∀ a b, values (pairIndex (a, b)) = wAB a b) + (hD : 1 ≤ D) (hDn : D ≤ n) + {initial y : Data 64} (h : Instances.Output n D g p values initial y) + (rho : Fin p) (k : ℕ) + (hk : k < numChunks (residueClass wAB p rho) (queryCap n D)) : + let q := 5 + 6 * (n * n) + p + 2 * rho.val * (n * n) + 2 * (k * queryCap n D) + let Q := min (queryCap n D) ((residueClass wAB p rho).card - k * queryCap n D) + (∀ i < Q, y.mem (q + 2 * i) < n ∧ y.mem (q + 2 * i + 1) < n) ∧ + (∀ i < Q, ∃! pair : Fin n × Fin n, + pair ∈ chunkOf wAB D p rho k ∧ + rankIn (residueClass wAB p rho) pair = k * queryCap n D + i ∧ + y.mem (q + 2 * i) = pair.1.val ∧ y.mem (q + 2 * i + 1) = pair.2.val) := by + let R := fun q => (values q % (p : ℤ)).toNat + have hR (pair : Fin n × Fin n) : R (pairIndex pair) = (resFin hp (wAB pair.1 pair.2)).val := by + dsimp only [R] + rw [hAB] + rfl + have hscan := h.2.2.2.2.2.2.2.2.1 + have hread (q : ℕ) (hq : q < n * n) (hrho : R q = rho.val) : + y.mem (5 + 6 * (n * n) + p + 2 * rho.val * (n * n) + + 2 * Nat.count (fun j => R j = rho.val) q) = q / n ∧ + y.mem (5 + 6 * (n * n) + p + 2 * rho.val * (n * n) + + 2 * Nat.count (fun j => R j = rho.val) q + 1) = q % n := by + simpa only [R, Nat.mul_right_comm 2 (n * n) rho.val] using + hscan rho.val rho.isLt q hq hrho + have hcap : 0 < queryCap n D := one_le_queryCap hD hDn + have hpair (i : ℕ) (hi : i < min (queryCap n D) + ((residueClass wAB p rho).card - k * queryCap n D)) := + QuerySpec.chunk_readback wAB hp R hR D rho y.mem + (5 + 6 * (n * n) + p + 2 * rho.val * (n * n)) hread hcap k hk i hi + have haddr (i : ℕ) : + 5 + 6 * (n * n) + p + 2 * rho.val * (n * n) + 2 * (k * queryCap n D + i) = + 5 + 6 * (n * n) + p + 2 * rho.val * (n * n) + 2 * (k * queryCap n D) + 2 * i := by + omega + dsimp only + constructor + · intro i hi + obtain ⟨pair, hpair, -⟩ := hpair i hi + rw [haddr i] at hpair + rw [hpair.2.2.1, hpair.2.2.2] + exact ⟨pair.1.isLt, pair.2.isLt⟩ + · intro i hi + simpa only [haddr i] using hpair i hi + +end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Program.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Program.lean new file mode 100644 index 0000000000..6368cd58a4 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Program.lean @@ -0,0 +1,174 @@ +/- +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.ExactTriangle.PreparationAdjacency +public import Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Callable.Width +public import Complexity.Algorithms.WordRAM.NatLog +public import Complexity.Computability.WordRAM.Copy + +/-! +# Calling a queried product from an actual prepared record + +The low 64 producer registers are retained. Register 64 selects an actual record ordinal; +the native code computes its stride, reads its six words and places the original raw matrices +and interleaved query coordinates at the actual producer heap end. The complete callable +product occupies a separate 163-register bank. Its existing matrix-input code, not this adapter, +performs raw-zero/one to canonical-signed doubling. + +The logarithm is computed by `NatLog.program`. Under `D=4^m`, dividing its binary result by two +recovers `m` exactly. No layout, logarithm, execution or solver certificate is a runtime input. +These definitions are internal stages of the complete record consumer. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct + +open Cslib.WordRAM +open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage + +namespace Reg + +/-- Actual record ordinal supplied by the outer caller. -/ +abbrev ordinal : Fin 320 := 64 +/-- Absolute result pointer. -/ +abbrev result : Fin 320 := 65 +/-- Actual producer heap end, and the callee's local-memory base. -/ +abbrev base : Fin 320 := 66 +/-- Original padded middle dimension. -/ +abbrev dimension : Fin 320 := 67 +/-- Original outer dimension. -/ +abbrev size : Fin 320 := 68 +/-- Computed selected record pointer. -/ +abbrev record : Fin 320 := 69 +/-- Loaded residue and piece metadata, retained without reinterpreting them. -/ +abbrev rho : Fin 320 := 70 +/-- Loaded piece index. -/ +abbrev piece : Fin 320 := 71 +/-- Loaded interleaved query pointer. -/ +abbrev queries : Fin 320 := 72 +/-- Loaded number of query occurrences. -/ +abbrev count : Fin 320 := 73 +/-- Loaded left-matrix pointer. -/ +abbrev left : Fin 320 := 74 +/-- Loaded right-matrix pointer. -/ +abbrev right : Fin 320 := 75 +/-- Computed size of either matrix block. -/ +abbrev area : Fin 320 := 76 +/-- Computed combined matrix-block length. -/ +abbrev twiceArea : Fin 320 := 77 +/-- Recovered inner depth. -/ +abbrev depth : Fin 320 := 78 +/-- Computed tensor level, nineteen times the inner depth. -/ +abbrev level : Fin 320 := 79 +/-- Computed original callee payload length. -/ +abbrev payloadLength : Fin 320 := 80 +/-- Constant one. -/ +abbrev one : Fin 320 := 81 +/-- Constant two. -/ +abbrev two : Fin 320 := 82 +/-- Record header length. -/ +abbrev six : Fin 320 := 83 +/-- Tensor-level multiplier. -/ +abbrev nineteen : Fin 320 := 84 +/-- Original callee scalar header length. -/ +abbrev four : Fin 320 := 85 +/-- Adapter address scratch. -/ +abbrev address : Fin 320 := 86 +/-- Temporary source pointer, also the logarithm input. -/ +abbrev source : Fin 320 := 96 +/-- Temporary destination pointer, also the logarithm result. -/ +abbrev destination : Fin 320 := 97 +/-- Temporary copy length. -/ +abbrev length : Fin 320 := 98 + +end Reg + +/-- The logarithm and copy routines share an adapter-local temporary register bank. -/ +@[expose] def logBank (i : Fin 4) : Fin 320 := ⟨96 + i.val, by omega⟩ +/-- All seven registers of the real array-copy routine are relocated together. -/ +@[expose] def copyBank (i : Fin 7) : Fin 320 := ⟨96 + i.val, by omega⟩ +/-- The complete callable product bank is disjoint from producer and adapter registers. -/ +@[expose] def calleeBank (i : Fin 163) : Fin 320 := ⟨128 + i.val, by omega⟩ + +/-- Compute the record pointer and read every actual descriptor field. -/ +@[expose] def readRecord : Code .standard 320 := + let output : Fin 320 := 39 + let heap : Fin 320 := 42 + ram[ Reg.one ← #1; Reg.two ← #2; Reg.six ← #6; Reg.nineteen ← #19; Reg.four ← #4; + Reg.address ← #1; Reg.dimension ← *Reg.address; + Reg.address ← #3; Reg.size ← *Reg.address; + Reg.area ← Reg.size * Reg.dimension; Reg.twiceArea ← Reg.area + Reg.area; + Reg.address ← Reg.twiceArea + Reg.six; Reg.address ← Reg.ordinal * Reg.address; + Reg.record ← output + Reg.address; Reg.base ← heap; + Reg.address ← Reg.record; Reg.rho ← *Reg.address; + Reg.address ← Reg.address + Reg.one; Reg.piece ← *Reg.address; + Reg.address ← Reg.address + Reg.one; Reg.queries ← *Reg.address; + Reg.address ← Reg.address + Reg.one; Reg.count ← *Reg.address; + Reg.address ← Reg.address + Reg.one; Reg.left ← *Reg.address; + Reg.address ← Reg.address + Reg.one; Reg.right ← *Reg.address; + Reg.source ← Reg.dimension ] + +/-- Recover the exact power-of-four exponent with the existing charged binary logarithm. -/ +@[expose] def logarithm : Code .standard 320 := NatLog.program.rename logBank + +/-- Write the complete original local input header, including its length word. -/ +@[expose] def writeHeader : Code .standard 320 := ram[ + Reg.depth ← Reg.destination / Reg.two; + Reg.level ← Reg.depth * Reg.nineteen; + Reg.payloadLength ← Reg.twiceArea + Reg.count; + Reg.payloadLength ← Reg.payloadLength + Reg.count; + Reg.payloadLength ← Reg.payloadLength + Reg.four; + Reg.address ← Reg.base; *Reg.address ← Reg.payloadLength; + Reg.address ← Reg.address + Reg.one; *Reg.address ← Reg.level; + Reg.address ← Reg.address + Reg.one; *Reg.address ← Reg.depth; + Reg.address ← Reg.address + Reg.one; *Reg.address ← Reg.size; + Reg.address ← Reg.address + Reg.one; *Reg.address ← Reg.count ] + +/-- Deliver real source and destination pointers for the left-matrix copy. -/ +@[expose] def deliverLeft : Code .standard 320 := ram[ + Reg.source ← Reg.left; Reg.address ← #5; + Reg.destination ← Reg.base + Reg.address; Reg.length ← Reg.area ] + +/-- The right block follows the left destination block. -/ +@[expose] def deliverRight : Code .standard 320 := ram[ + Reg.source ← Reg.right; Reg.destination ← Reg.destination + Reg.area ] + +/-- Preserve each query occurrence's two original raw coordinates, in its original order. -/ +@[expose] def deliverQueries : Code .standard 320 := ram[ + Reg.source ← Reg.queries; Reg.destination ← Reg.destination + Reg.area; + Reg.length ← Reg.count + Reg.count ] + +/-- Real copying, with every address calculation, load/store and loop instruction charged. -/ +@[expose] def copy : Code .standard 320 := ArrayCopy.program.rename copyBank + +/-- Three actual copies; no catalogue or virtual-window snapshot is made. -/ +@[expose] def copyInputs : Code .standard 320 := + .seq deliverLeft <| .seq copy <| .seq deliverRight <| .seq copy <| + .seq deliverQueries copy + +/-- Runtime memory rebasing is provided by the callee; renaming moves only its registers. -/ +@[expose] def invoke : Code .standard 320 := + .seq (.op (.copy (calleeBank CallableProduct.Reg.base) Reg.base)) <| + .seq (CallableProduct.program.rename calleeBank) + (.op (.copy Reg.result (calleeBank CallableProduct.Reg.result))) + +/-- Runtime preparation prefix, useful for admitted decoder/copy tests without the full solver. -/ +@[expose] def prepare : Code .standard 320 := + .seq readRecord <| .seq logarithm <| .seq writeHeader copyInputs + +/-- One selected actual producer record, including all copying and the complete native callee. -/ +@[expose] def program : Code .standard 320 := .seq prepare invoke + +-- The closed syntactic traversal includes the complete existing large callee. +set_option maxRecDepth 4096 in +/-- One fixed finite native program, independent of dimensions, record ordinal and word width. -/ +theorem program_fixed : program.size ≤ 131584 ∧ ¬program.ReadsWidth := by decide + +end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/RawInput.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/RawInput.lean new file mode 100644 index 0000000000..bd86b23f73 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/RawInput.lean @@ -0,0 +1,114 @@ +/- +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.ExactTriangle.RecordProduct.Exec + +/-! +# Original raw matrix and coordinate spans + +These readback lemmas use the existing original product input and row-major numbering. +The query list is the finite mathematical reading of actual native coordinate words; the +adapter copies those words unchanged, and performs no uncharged query decoding operation. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct + +open Cslib.WordRAM +open Cslib.Algorithms.MatrixMultiplication.Schonhage +open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage + +/-- Mathematical reading of an existing interleaved native query block. The modulo is only +a total specification; actual producer coordinates are proved in range before using it. -/ +@[expose] def decodedQueries {n : ℕ} (hn : 0 < n) (mem : ℕ → ℕ) (q Q : ℕ) : + List (Fin n × Fin n) := + List.ofFn fun i : Fin Q => + (⟨mem (q + 2 * i.val) % n, Nat.mod_lt _ hn⟩, + ⟨mem (q + 2 * i.val + 1) % n, Nat.mod_lt _ hn⟩) + +/-- Decoding retains exactly the original occurrence count. -/ +theorem decodedQueries_length {n : ℕ} (hn : 0 < n) (mem : ℕ → ℕ) (q Q : ℕ) : + (decodedQueries hn mem q Q).length = Q := List.length_ofFn + +/-- Every actual in-range coordinate word reappears unchanged in the ordinary callee input. -/ +theorem decodedQueries_words {m n q Q : ℕ} (hn : 0 < n) (mem : ℕ → ℕ) + (X : Matrix (Fin n) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin n) ℤ) + (hcoord : ∀ i < Q, mem (q + 2 * i) < n ∧ mem (q + 2 * i + 1) < n) : + ∀ a < 2 * Q, mem (q + a) = + (State.init (QueriedProduct.input true (19 * m) X Y + (decodedQueries hn mem q Q)) : State 160).data.mem (5 + 2 * (n * D m) + a) := by + intro a ha + have hi : a / 2 < Q := (Nat.div_lt_iff_lt_mul (by decide : 0 < 2)).mpr (by omega) + let i : Fin (decodedQueries hn mem q Q).length := ⟨a / 2, by + rw [decodedQueries_length]; exact hi⟩ + let s : Fin 2 := ⟨a % 2, Nat.mod_lt _ (by decide)⟩ + have hw := QueriedProduct.input_query_word true (19 * m) X Y + (decodedQueries hn mem q Q) i s + have hsplit : 2 * (a / 2) + a % 2 = a := by omega + change (State.init (QueriedProduct.input true (19 * m) X Y + (decodedQueries hn mem q Q)) : State 160).data.mem + (QueriedProduct.queryInputBase m n + 2 * (a / 2) + a % 2) = _ at hw + rw [show QueriedProduct.queryInputBase m n + 2 * (a / 2) + a % 2 = + 5 + 2 * (n * D m) + a by unfold QueriedProduct.queryInputBase; omega] at hw + rw [hw] + have hc := hcoord (a / 2) hi + simp only [decodedQueries, List.get_ofFn, i, Fin.val_cast] + by_cases hzero : a % 2 = 0 + · have he : s = 0 := Fin.ext hzero + simp only [he, ↓reduceIte] + rw [Nat.mod_eq_of_lt hc.1] + congr 1 + omega + · have hone : a % 2 = 1 := by have := Nat.mod_lt a (by decide : 0 < 2); omega + have he : s ≠ 0 := by intro h; exact hzero (congrArg Fin.val h) + simp only [he, ↓reduceIte] + rw [Nat.mod_eq_of_lt hc.2] + congr 1 + omega + +/-- A native left-matrix span reads exactly as the ordinary product's original raw input. -/ +theorem raw_left_words {m n s : ℕ} (mem : ℕ → ℕ) + (X : Matrix (Fin n) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin n) ℤ) + (qs : List (Fin n × Fin n)) + (hX : ∀ (i : Fin n) (k : Fin (D m)), mem (s + (i.val * D m + k.val)) = (X i k).toNat) : + ∀ a < n * D m, mem (s + a) = + (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem (5 + a) := by + intro a ha + have hd : 0 < D m := by change 0 < 4 ^ m; positivity + have hi : a / D m < n := (Nat.div_lt_iff_lt_mul hd).mpr ha + have hk : a % D m < D m := Nat.mod_lt _ hd + have hw := QueriedProduct.input_matrix_word (L := 19 * m) true X Y qs false + (a / D m) (a % D m) hi hk + have he : a / D m * D m + a % D m = a := Nat.div_add_mod' a (D m) + simp only [BandPreparation.matrixOffset, Bool.false_eq_true, ↓reduceIte, he, + BandPreparation.matrixValues, QueriedProduct.entryWord, hi, hk, ↓reduceDIte] at hw + rw [show 5 + a = a + 5 by omega, hw] + simpa only [he] using hX ⟨a / D m, hi⟩ ⟨a % D m, hk⟩ + +/-- The right original block retains its `D×n` row-major order. -/ +theorem raw_right_words {m n t : ℕ} (hn : 0 < n) (mem : ℕ → ℕ) + (X : Matrix (Fin n) (Fin (D m)) ℤ) (Y : Matrix (Fin (D m)) (Fin n) ℤ) + (qs : List (Fin n × Fin n)) + (hY : ∀ (k : Fin (D m)) (i : Fin n), mem (t + (k.val * n + i.val)) = (Y k i).toNat) : + ∀ a < n * D m, mem (t + a) = + (State.init (QueriedProduct.input true (19 * m) X Y qs) : State 160).data.mem + (5 + n * D m + a) := by + intro a ha + have hi : a % n < n := Nat.mod_lt _ hn + have hk : a / n < D m := (Nat.div_lt_iff_lt_mul hn).mpr (by simpa only [Nat.mul_comm] using ha) + have hw := QueriedProduct.input_matrix_word (L := 19 * m) true X Y qs true + (a % n) (a / n) hi hk + have he : a / n * n + a % n = a := Nat.div_add_mod' a n + simp only [BandPreparation.matrixOffset, ↓reduceIte, he, + BandPreparation.matrixValues, QueriedProduct.entryWord, hi, hk, ↓reduceDIte] at hw + rw [show 5 + n * D m + a = a + n * D m + 5 by omega, hw] + simpa only [he] using hY ⟨a / n, hk⟩ ⟨a % n, hi⟩ + +end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/SourceBounds.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/SourceBounds.lean new file mode 100644 index 0000000000..bc1d61eeaa --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/SourceBounds.lean @@ -0,0 +1,109 @@ +/- +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.ExactTriangle.RecordProduct.Flat +public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationBounds + +/-! +# Original-size prefix bounds and the per-record thin saving + +The initialized code has physical-width-independent polynomial words and memory support at +every admitted wider width. Its charge is the actual producer preparation plus the selected +record's actual thin product. Summing all products, solving ExactTriangle and reconstructing +witnesses remain separate; no aggregate subcubic claim is made here. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct + +open Cslib.WordRAM Cslib.Algorithms.ExactTriangle +open Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- Explicit input-derived bound for all prefix words and the address support, independent +of any larger admitted physical width. This is a reservation, not a bulk initialization. -/ +@[expose] def wordBound (n D g p A : ℕ) : ℕ := 2 ^ admissionWidth n D g p A + +/-- The prefix bound is polynomial in original size for the usual original scalar/weight +envelopes, with an explicit fixed exponent for each magnitude exponent κ. -/ +theorem wordBound_le_pow {n D g p A κ : ℕ} (hn : 1 ≤ n) + (hD : D ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) : + wordBound n D g p A ≤ (n + 2) ^ (514 * κ + 11812) := by + let b := n + 2 + have hb : 1 < b := by dsimp only [b]; omega + have hc := Nat.clog_pos (by decide : 1 < (2 : ℕ)) hb + have hp2 := Nat.pow_pred_clog_lt_self (by decide : 1 < (2 : ℕ)) hb + have he : Nat.clog 2 b = (Nat.clog 2 b).pred + 1 := (Nat.succ_pred_eq_of_pos hc).symm + have hbase : 2 ^ Nat.clog 2 b ≤ b ^ 2 := by + rw [he, pow_succ] + nlinarith only [hp2, show 2 ≤ b by omega] + have hw := admissionWidth_le_log hn hD hg hp hA + have hpow := Nat.pow_le_pow_right (by decide : 1 ≤ (2 : ℕ)) hw + change 2 ^ admissionWidth n D g p A ≤ _ + calc + _ ≤ 2 ^ ((257 * κ + 5906) * Nat.clog 2 b) := hpow + _ = (2 ^ Nat.clog 2 b) ^ (257 * κ + 5906) := by rw [← Nat.pow_mul, Nat.mul_comm] + _ ≤ (b ^ 2) ^ (257 * κ + 5906) := Nat.pow_le_pow_left hbase _ + _ = b ^ (514 * κ + 11812) := by + rw [← Nat.pow_mul] + exact congrArg (fun k : ℕ => b ^ k) (by omega : 2 * (257 * κ + 5906) = 514 * κ + 11812) + +/-- Every actual native prefix at every admitted width has input-derived bounded words and +zero memory beyond the same bound. The real halting run at the minimum admitted width and +the existing width-independent prefix theorem derive the result. -/ +theorem bounded_reachable_original {W m n g p A k : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hD : 16 ≤ D m) + (hg : 1 ≤ g) (hp : 0 < p) (hN : D m ^ 18 ≤ n) + (hv : ∀ z ∈ values, z.natAbs ≤ A) (hW : admissionWidth n (D m) g p A ≤ W) + {s : State 320} (hr : Runs W (entryProgram.program Reg.result) + (State.init (PreparationInput.input n (D m) g p values)) s k) : + (∀ i, s.data.regs i < wordBound n (D m) g p A) ∧ + (∀ a, s.data.mem a < wordBound n (D m) g p A) ∧ + ∀ a, wordBound n (D m) g p A ≤ a → s.data.mem a = 0 := by + obtain ⟨hi, a, idx, ha, hidx, hord, y, t, ht, hpref, he, hy, yr, hv', hf, hreg, hQ⟩ := + runs_input values hlen hD hg hp hN hv le_rfl + have hlow := Runs.prefix_at_smaller_width entryProgram_fixed.2 hW hr he + have hs := hlow.bounded (Data.Bounded.init hi) + refine ⟨hs.1, hs.2, ?_⟩ + intro a ha + rw [hlow.mem_above (Data.Bounded.init hi) ha] + cases a with + | zero => + change 2 ^ admissionWidth n (D m) g p A ≤ 0 at ha + have := Nat.two_pow_pos (admissionWidth n (D m) g p A) + omega + | succ a => + change (PreparationInput.input n (D m) g p values).getD a 0 = 0 + apply List.getD_eq_default + have hlen := hi.1 + dsimp only [Fits] at hlen + change 2 ^ admissionWidth n (D m) g p A ≤ a + 1 at ha + omega + +/-- Complete producer preparation plus one actual record product, including the final halt. +The per-record sparsity is supplied by its actual native chunk, not an aggregate solver oracle. -/ +theorem initialized_time_le {m n g p : ℕ} (values : List ℤ) (qs : List (Fin n × Fin n)) + (hD : 16 ≤ D m) (hN : D m ^ 18 ≤ n) (hg : 1 ≤ g) + (hp : p ∈ Nat.sqrtPrimeWindow (D m)) (hQ : qs.length * 2 ^ m ≤ n ^ 2) : + ((preparationTime n (D m) g p values + timeBound (m := m) qs + 1 : ℕ) : ℝ) ≤ + 690 * (n : ℝ) ^ 2 * D m * g + + 34603008 * ((19 * m + 1 : ℕ) : ℝ) * (n : ℝ) ^ 2 / (D m : ℝ) ^ (1 / 18 : ℝ) := by + have hDn : D m ≤ n := (Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN + have hpTime := PreparationBounds.computed_timeBound_le values hD hDn hg hp + have hpReal : (preparationTime n (D m) g p values : ℝ) ≤ + 690 * (n : ℝ) ^ 2 * D m * g := by + have hpNat : preparationTime n (D m) g p values ≤ 690 * n ^ 2 * D m * g := by + simpa only [preparationTime, pow_two] using hpTime + exact_mod_cast hpNat + have ht := thin_timeBound_sparse qs hN hQ + push_cast + push_cast at ht + linarith only [hpReal, ht] + +end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct diff --git a/ComplexityTests/WordRAMExactTriangleRecordProduct.lean b/ComplexityTests/WordRAMExactTriangleRecordProduct.lean new file mode 100644 index 0000000000..4c1fed3b66 --- /dev/null +++ b/ComplexityTests/WordRAMExactTriangleRecordProduct.lean @@ -0,0 +1,135 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +-- upstream: local-only (tests) + +import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.SourceBounds + +/-! +# Real record-decoder prefixes at admitted positive-depth geometry + +Full positive-depth multiplication is too large for a concrete VM regression: its smallest +producer middle dimension is sixteen and the thin geometry requires `n≥16^18`. These tests +execute actual descriptor/log/header code at that valid geometry, without allocating matrices +or claiming a complete producer run for the fixture. General initialized composition is +checked separately by the library execution theorem. +-/ + +set_option linter.hashCommand false + +namespace ComplexityTests.WordRAMExactTriangleRecordProduct + +open Cslib.WordRAM Cslib.Algorithms.WordRAM.ExactTriangle +open Cslib.Algorithms.ExactTriangle Cslib.Algorithms.MatrixMultiplication.Schonhage +open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage + +private def side : ℕ := 16 ^ 18 +private def area : ℕ := side * 16 +private def stride : ℕ := 6 + 2 * area +private def record : ℕ := 100 + stride +private def heap : ℕ := 100 + 2 * stride + +private def fixture : Data 320 := + { regs := fun i => if i.val = 39 then 100 else if i.val = 42 then heap + else if i.val = 64 then 1 else 73 + mem := fun a => if a = 1 then 16 else if a = 3 then side + else if record ≤ a && a < record + 6 then + [3, 1, 50, 2, record + 6, record + 6 + area].getD (a - record) 0 + else if a = 50 then side - 1 else if a = 51 then 7 + else if a = 52 then 8 else if a = 53 then side - 2 else 0 } + +private def decodePrefix : Code .standard 320 := + .seq RecordProduct.readRecord (.seq RecordProduct.logarithm RecordProduct.writeHeader) + +private def observe : Option (List ℕ × List ℕ × Bool × ℕ) := + (decodePrefix.eval 32768 512 fixture).map fun (y, steps) => + ((List.range 5).map (fun i => y.mem (heap + i)), + (List.range 4).map (fun i => y.mem (50 + i)), + decide (∀ i : Fin 64, y.regs (RecordProduct.producerBank i) = + fixture.regs (RecordProduct.producerBank i)), steps) + +-- Actual nonzero ordinal selects the second six-word record, recovers m=2 and writes L=38. +#guard observe == some ([4 + 2 * area + 4, 38, 2, side, 2], + [side - 1, 7, 8, side - 2], true, 64) + +-- Geometry is fully admitted; the smaller tempting VM dimension would violate it. +#guard side ≥ 16 ^ 18 +#guard ¬(16 ≥ 16 ^ 18) + +-- Actual source words are not doubled by the adapter's copy routine. +private def copyFixture : Data 320 := + { regs := fun i => if i.val = 96 then 10 else if i.val = 97 then 30 + else if i.val = 98 then 2 else 91 + mem := fun a => if a = 10 then 1 else if a = 11 then 0 else 77 } + +#guard (RecordProduct.copy.eval 16 8 copyFixture).map (fun (y, steps) => + (y.mem 30, y.mem 31, y.mem 29, y.mem 32, y.regs 39, steps)) == + some (1, 0, 77, 77, 91, 18) + +private def zeroWeights (n : ℕ) : List ℤ := List.replicate (3 * (n * n)) 0 +private def physicalWidth (n : ℕ) : ℕ := RecordProduct.admissionWidth n (D 2) 1 3 0 + +/-- A fully admitted, nonempty producer→adapter run at positive inner depth. The list is kept +symbolic: this kernel proof uses the general actual execution theorem, not VM enumeration of +the enormous matrix family. Its observed answer and charged halt use the same final memory. -/ +private theorem initialized_zero (N : ℕ) (hgeo : D 2 ^ 18 ≤ N) : + ∃ a : Data 64, ∃ idx : InstanceIndex 3, ∃ y : Data 320, ∃ steps : ℕ, + Runs (physicalWidth N) (RecordProduct.entryProgram.program RecordProduct.Reg.result) + (State.init (PreparationInput.input N (D 2) 1 3 (zeroWeights N))) + ⟨RecordProduct.entryProgram.size, y⟩ steps ∧ + Executes (physicalWidth N) (RecordProduct.entryProgram.program RecordProduct.Reg.result) + (State.init (PreparationInput.input N (D 2) 1 3 (zeroWeights N))) + (y.regs RecordProduct.Reg.result) (steps + 1) ∧ + let qs := RecordProduct.decodedQueries + ((Nat.pow_pos (by decide : 0 < D 2) (n := 18)).trans_le hgeo) a.mem + (RecordProduct.recordQueries N (D 2) 3 idx) + (RecordProduct.recordQueryCount N (D 2) 3 (fun q => (zeroWeights N).getD q 0) idx) + ∃ first : Fin qs.length, + y.mem (y.regs RecordProduct.Reg.result) = Signed.encode + ((RecordProduct.leftMatrix 2 N 1 3 (fun q => (zeroWeights N).getD q 0) idx * + RecordProduct.rightMatrix 2 N 1 3 (fun q => (zeroWeights N).getD q 0) idx) + (qs.get first).1 (qs.get first).2) := by + have hv : ∀ z ∈ (zeroWeights N), z.natAbs ≤ 0 := by + intro z hz + have he : z = 0 := List.eq_of_mem_replicate hz + subst z + decide + obtain ⟨hi, a, idx, ha, hidx, hord, y, steps, ht, hr, he, hb, yr, hvals, hf, hg, hQ⟩ := + RecordProduct.runs_input (m := 2) (n := N) (g := 1) (p := 3) (A := 0) + (W := (physicalWidth N)) (zeroWeights N) (by simp [zeroWeights]) + (by decide) (by decide) (by decide) hgeo hv le_rfl + have hpos := RecordProduct.recordQueryCount_pos (n := N) (D := D 2) (g := 1) (p := 3) + (fun q => (zeroWeights N).getD q 0) + (by decide : (3 : ℕ) ≠ 0) (by decide : 1 ≤ D 2) + ((Nat.le_self_pow (by decide : 18 ≠ 0) (D 2)).trans hgeo) idx hidx + let qs := RecordProduct.decodedQueries + ((Nat.pow_pos (by decide : 0 < D 2) (n := 18)).trans_le hgeo) a.mem + (RecordProduct.recordQueries N (D 2) 3 idx) + (RecordProduct.recordQueryCount N (D 2) 3 (fun q => (zeroWeights N).getD q 0) idx) + have hlen : 0 < qs.length := by rw [RecordProduct.decodedQueries_length]; exact hpos + let first : Fin qs.length := ⟨0, hlen⟩ + have hv0 := hvals first + refine ⟨a, idx, y, steps, hr, ?_, first, ?_⟩ + · simpa only [yr] using he + · simpa only [first, Fin.val_mk, Nat.add_zero, ← yr] using hv0 + +example : ∃ a : Data 64, ∃ idx : InstanceIndex 3, ∃ y : Data 320, ∃ steps : ℕ, + Runs (physicalWidth side) (RecordProduct.entryProgram.program RecordProduct.Reg.result) + (State.init (PreparationInput.input side (D 2) 1 3 (zeroWeights side))) + ⟨RecordProduct.entryProgram.size, y⟩ steps ∧ + Executes (physicalWidth side) (RecordProduct.entryProgram.program RecordProduct.Reg.result) + (State.init (PreparationInput.input side (D 2) 1 3 (zeroWeights side))) + (y.regs RecordProduct.Reg.result) (steps + 1) ∧ + let qs := RecordProduct.decodedQueries (by dsimp [side]; positivity : 0 < side) a.mem + (RecordProduct.recordQueries side (D 2) 3 idx) + (RecordProduct.recordQueryCount side (D 2) 3 (fun q => (zeroWeights side).getD q 0) idx) + ∃ first : Fin qs.length, + y.mem (y.regs RecordProduct.Reg.result) = Signed.encode + ((RecordProduct.leftMatrix 2 side 1 3 (fun q => (zeroWeights side).getD q 0) idx * + RecordProduct.rightMatrix 2 side 1 3 (fun q => (zeroWeights side).getD q 0) idx) + (qs.get first).1 (qs.get first).2) := initialized_zero side le_rfl + +end ComplexityTests.WordRAMExactTriangleRecordProduct diff --git a/ROADMAP.md b/ROADMAP.md index d80448735e..a6be60a66e 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -526,9 +526,19 @@ each statement against the numbered result. Organize modules by subject, not cha `D=4^m`, `L=19m`, `D^18≤N` and `Q*2^m≤N²`, the full charge including halt is at most `17301504*(19m+1)*N²/D^(1/18)`. Distinct-set sparsity retains an additive occurrence charge. Every width at least `256*clog₂(base+N+Q+P+5)` suffices for initialized caller-word bound `P`. - The reserved window is at most `(2*(N+Q+3))^128` and is not bulk-initialized. Actual ET-record - reads, matrix/query placement, producer-readback composition and the full [#1394] endpoint - remain open. + The reserved window is at most `(2*(N+Q+3))^128` and is not bulk-initialized. +- **Prepared ET-record product calls** ([#1626](https://github.com/cslib-community/complexitylib/issues/1626)): + the native adapter reads the computed six-word record, recovers the depth with actual binary + logarithm code, and copies raw matrices and query occurrences above the producer's heap. + It invokes the complete callable product in a separate register bank and preserves the + catalogue, sources and producer registers. The fixed 320-register initialized client runs + the producer and consumes its first record; the caller interface supports every occupied + ordinal. Original polynomial headers/weights give positive logarithmic admission and + polynomial words/address support at every wider width. Adaptation costs `O(nD+Q)` beyond + the actual callee; actual chunks derive `Q*2^m≤n²`, giving the per-record halt-inclusive bound + `34603008*(19m+1)*n²/D^(1/18)` at `D=4^m`, `L=19m`, `D^18≤n`. + The outer instance loop, aggregate subcubic ET bound, backend/witness reconstruction and + the full [#1394] ordinary-3SUM 1.9992 endpoint remain open. - **Conditional Convolution-3SUM host** ([#1524]): the charged native host initializes from the ordinary input and runs every generated instance, conditional on a concrete solver's execution, correctness and frame theorem. This completes the conditional host milestone. Integrating the diff --git a/UPSTREAM.md b/UPSTREAM.md index e55fed516e..7f5575c79e 100644 --- a/UPSTREAM.md +++ b/UPSTREAM.md @@ -384,7 +384,26 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he from that derived physical admission. Initialized scratch is zero, so its `P` only needs to bound the protected caller prefix. The generic compiler theorem remains separate from the concrete thin-geometry admission and saving. - The real ET-record/matrix/query adapter and whole solver remain subsequent work under #1394. + The real ET-record/matrix/query adapter is tracked in + [#1626](https://github.com/cslib-community/complexitylib/issues/1626). Its fixed 320-register + native code computes the selected record address, reads all six fields, recovers the exact + `4^m` exponent with existing `NatLog`, stores local original headers and copies the two raw + matrices and interleaved occurrence coordinates above the actual producer heap. Raw zero/one + words are copied unchanged; the callee's existing loop performs charged signed doubling. + The complete 163-register callable bank is renamed together, preserving the producer's low + 64 registers. Memory relocation uses the real callable compiler, never register renaming alone. + `PreparationInput.exec_input` exposes the existing structured initialized derivation so real + caller code can compose it. Its private fit proof stays private; existing `runs_input` reuses + the new rule with unchanged statement, assumptions, exact readback and halt-inclusive budget. + The first-record initialized client supplies no layout/run/time/fit/solver certificate; + actual producer readback derives all source pointer ranges and coordinate meanings, and + actual chunk counts derive occurrence sparsity. The general caller supports every occupied + record ordinal. The per-record charge including halt is at most three times the original + product plus `4096*(nD+Q+1)`, or `34603008*(19m+1)*n²/D^(1/18)` under the admitted geometry. + The original producer word bound supplies caller `P` and heap placement; the complete wider + initialized prefixes have a positive logarithmic width threshold and polynomial words/support + independent of the physical width. Outer parameter/prime selection and instance iteration, + aggregate solving/witness reconstruction and the whole #1394 endpoint remain separate. Stage `exec_*` lemmas are internal implementation APIs exported across proof modules; callers use the flat initialized runs, width theorem or pointer/epoch kernel. The narrow `WordRAM.ArrayAppend` and `WordRAM.InputArray` topic modules keep append/input dependencies