From 37de6254904e5a29fa4521b8c06c11830c42d2a7 Mon Sep 17 00:00:00 2001 From: Erik Demaine Date: Sun, 1 Nov 2026 00:42:29 -0400 Subject: [PATCH 1/4] feat(ExactTriangle): implement dirty-memory fixed-prime caller Source/MCP checkpoint for #2125 on pinned bc2. Complete actual640-register caller execution, original-array copy/sum, computed source width and memory-window translation, exact +/- ET/witness/global scans and caller/selector frames are proved. Aggregate actual source/copy/setup/return/halt charge and original initialization14 are checked. All owned source modules and concrete signed/dirty/frame/cost tests have clean targeted diagnostics; no local all-six/static/import audit claim. Original producer admission/locality proof is reused through narrow public seams; old initialized statement and all existing native source program bodies are retained. This is a partial source checkpoint, not completion/publication: full initialized same-y Runs/halt, original-regime logarithmic width/polynomial prefixes, fully admitted clients and final audit/review remain under2125. Root retains sole audit slot and full1394/global parameter/prime/ordinary-host/asymptotic scope. No new agents or PR. AI assistance: OpenAI Codex; original source credit preserved. --- .../CallableFixedPrime/Adapt.lean | 193 +++++++++++++++++ .../CallableFixedPrime/Admission.lean | 76 +++++++ .../CallableFixedPrime/Copy.lean | 134 ++++++++++++ .../CallableFixedPrime/Core.lean | 106 +++++++++ .../CallableFixedPrime/Exec.lean | 153 +++++++++++++ .../CallableFixedPrime/Header.lean | 71 +++++++ .../CallableFixedPrime/Input.lean | 108 ++++++++++ .../CallableFixedPrime/InputSpec.lean | 172 +++++++++++++++ .../CallableFixedPrime/Parameters.lean | 103 +++++++++ .../CallableFixedPrime/Program.lean | 173 +++++++++++++++ .../CallableFixedPrime/Properties.lean | 111 ++++++++++ .../CallableFixedPrime/Receive.lean | 46 ++++ .../CallableFixedPrime/Setup.lean | 201 ++++++++++++++++++ .../CallableFixedPrime/Source.lean | 158 ++++++++++++++ .../CallableFixedPrime/TimeBound.lean | 56 +++++ .../ExactTriangle/FixedPrime/Program.lean | 18 +- .../ExactTriangle/PreparationInput.lean | 46 ++-- .../ExactTriangle/PreparationLocality.lean | 48 +++++ Complexity/Computability/WordRAM/CopySum.lean | 135 ++++++++++++ .../WordRAM/MemoryWindow/Normalization.lean | 47 ++++ .../WordRAMCallableFixedPrime.lean | 58 +++++ 21 files changed, 2193 insertions(+), 20 deletions(-) create mode 100755 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Adapt.lean create mode 100755 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Admission.lean create mode 100755 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Copy.lean create mode 100755 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Core.lean create mode 100755 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Exec.lean create mode 100755 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Header.lean create mode 100755 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Input.lean create mode 100755 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/InputSpec.lean create mode 100755 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Parameters.lean create mode 100755 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Program.lean create mode 100755 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Properties.lean create mode 100755 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Receive.lean create mode 100755 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Setup.lean create mode 100755 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Source.lean create mode 100755 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/TimeBound.lean create mode 100755 Complexity/Computability/WordRAM/CopySum.lean create mode 100755 Complexity/Computability/WordRAM/MemoryWindow/Normalization.lean create mode 100755 ComplexityTests/WordRAMCallableFixedPrime.lean diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Adapt.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Adapt.lean new file mode 100755 index 0000000000..7d3386f5b2 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Adapt.lean @@ -0,0 +1,193 @@ +/- +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.CallableFixedPrime.Copy +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.InputSpec + +/-! +# Complete original-array adaptation and actual word accumulation + +All three real copy calls operate only on original squares. Their sum and memory effects +are composed without a clean destination, a supplied list of words or a layout certificate. +The implementation interfaces here retain numerical fits; the complete caller derives them +from original input bounds and the computed virtual-window threshold. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM + +/-- Original raw-word sum computed while copying the three source squares. -/ +@[expose] def matrixWordSum (mem : ℕ → ℕ) (n ab bc ac : ℕ) : ℕ := + ArrayCopySum.wordSum mem ab (n * n) + ArrayCopySum.wordSum mem bc (n * n) + + ArrayCopySum.wordSum mem ac (n * n) + +/-- Original canonical source words identify the actual native sum with the original list +sum used by source-width admission. No additional matrix traversal is performed. -/ +theorem matrixWordSum_eq_rawTotal {n ab bc ac : ℕ} (mem : ℕ → ℕ) (values : List ℤ) + (vab : ∀ q < n * n, mem (ab + q) = Signed.encode (values.getD q 0)) + (vbc : ∀ q < n * n, mem (bc + q) = Signed.encode (values.getD (n * n + q) 0)) + (vac : ∀ q < n * n, mem (ac + q) = Signed.encode (values.getD (2 * (n * n) + q) 0)) : + matrixWordSum mem n ab bc ac = rawTotal n values := by + have ha : ArrayCopySum.wordSum mem ab (n * n) = + ∑ q ∈ Finset.range (n * n), Signed.encode (values.getD q 0) := + Finset.sum_congr rfl (fun q hq => vab q (Finset.mem_range.mp hq)) + have hb : ArrayCopySum.wordSum mem bc (n * n) = + ∑ q ∈ Finset.range (n * n), Signed.encode (values.getD (n * n + q) 0) := + Finset.sum_congr rfl (fun q hq => vbc q (Finset.mem_range.mp hq)) + have hc : ArrayCopySum.wordSum mem ac (n * n) = + ∑ q ∈ Finset.range (n * n), Signed.encode (values.getD (2 * (n * n) + q) 0) := + Finset.sum_congr rfl (fun q hq => vac q (Finset.mem_range.mp hq)) + rw [matrixWordSum, ha, hb, hc, rawTotal_split] + +/-- Actual stores/copies and their complete linear charge. The three sources may alias each +other, but precede workspace. Only original source/end/sum quantities occur in the fits. -/ +theorem exec_adapt {W : ℕ} (x : Data 640) + (hab : x.regs Reg.ab + x.regs Reg.n * x.regs Reg.n ≤ x.regs Reg.base) + (hbc : x.regs Reg.bc + x.regs Reg.n * x.regs Reg.n ≤ x.regs Reg.base) + (hac : x.regs Reg.ac + x.regs Reg.n * x.regs Reg.n ≤ x.regs Reg.base) + (hfit : Fits W (x.regs Reg.base + 4 * (x.regs Reg.n * x.regs Reg.n) + + matrixWordSum x.mem (x.regs Reg.n) (x.regs Reg.ab) (x.regs Reg.bc) (x.regs Reg.ac) + + 1024)) : + ∃ y, ExecWithin W adapt x y (24 * (x.regs Reg.n * x.regs Reg.n) + 38) ∧ + y.mem = copyMemory x.mem (x.regs Reg.base) (x.regs Reg.n) (x.regs Reg.dimension) + (x.regs Reg.groups) (x.regs Reg.prime) (x.regs Reg.ab) (x.regs Reg.bc) (x.regs Reg.ac) ∧ + y.regs Reg.total = matrixWordSum x.mem (x.regs Reg.n) + (x.regs Reg.ab) (x.regs Reg.bc) (x.regs Reg.ac) ∧ + ∀ j : Fin 640, j.val < 608 → y.regs j = x.regs j := by + let n := x.regs Reg.n + let N := n * n + let b := x.regs Reg.base + let ab := x.regs Reg.ab + let bc := x.regs Reg.bc + let ac := x.regs Reg.ac + let Sa := ArrayCopySum.wordSum x.mem ab N + let Sb := ArrayCopySum.wordSum x.mem bc N + let Sc := ArrayCopySum.wordSum x.mem ac N + let T := Sa + Sb + Sc + have fit : Fits W (b + 4 * N + T + 1024) := hfit + have h1 : Fits W 1 := fit.of_le (by omega) + have sum_eq (mem : ℕ → ℕ) (hmem : ∀ q < b, mem q = x.mem q) + (src : ℕ) (hsrc : src + N ≤ b) : + ArrayCopySum.wordSum mem src N = ArrayCopySum.wordSum x.mem src N := by + apply Finset.sum_congr rfl + intro q hq + exact hmem _ (by have := Finset.mem_range.mp hq; omega) + obtain ⟨h, hh, harea, hconstant, hmem, hregs⟩ := exec_header x (fit.of_le (by + change b + 4 * N + 1024 ≤ b + 4 * N + T + 1024 + omega)) + have hbelow (q : ℕ) (hq : q < b) : h.mem q = x.mem q := by + rw [hmem] + exact headerMemory_below _ _ _ _ _ _ _ hq + obtain ⟨a, ha, amem, asrc, adst, alen, atotal, aregs⟩ := exec_firstCopy h hconstant + (by rw [hregs Reg.base (by decide)]; exact fit.of_le (by omega)) + have a_src : a.regs (copyBank 0) = ab := asrc.trans (hregs Reg.ab (by decide)) + have a_dst : a.regs (copyBank 1) = b + 5 := by rw [adst, hregs Reg.base (by decide)] + have a_len : a.regs (copyBank 2) = N := alen.trans harea + have a_total : a.regs (copyBank 7) = 0 := atotal + have a_meta (j : Fin 640) (hj : j.val < 608) : a.regs j = x.regs j := + (aregs j (by omega)).trans (hregs j (by omega)) + have a_below (q : ℕ) (hq : q < b) : a.mem q = x.mem q := by rw [amem]; exact hbelow q hq + have a_sum : ArrayCopySum.wordSum a.mem ab N = Sa := sum_eq a.mem a_below ab hab + obtain ⟨c₁, hc₁, c₁mem, c₁src, c₁dst, c₁len, c₁total, c₁regs⟩ := exec_copy a h1 + (by rw [a_src, a_len]; exact fit.of_le (by omega)) + (by rw [a_dst, a_len]; exact fit.of_le (by omega)) + (by rw [a_total, a_src, a_len, a_sum]; exact fit.of_le (by omega)) + (by rw [a_src, a_dst, a_len]; omega) + have hc₁' : ExecWithin W (ArrayCopySum.program.rename copyBank) a c₁ (8 * N + 4) := by + simpa only [a_len] using hc₁ + have c₁_dst : c₁.regs (copyBank 1) = b + 5 := c₁dst.trans a_dst + have c₁_len : c₁.regs (copyBank 2) = N := c₁len.trans a_len + have c₁_total : c₁.regs (copyBank 7) = Sa := by + simpa only [a_total, a_src, a_len, a_sum, Nat.zero_add] using c₁total + have c₁_meta (j : Fin 640) (hj : j.val < 608) : c₁.regs j = x.regs j := + (c₁regs j (Or.inl (by omega))).trans (a_meta j hj) + have cm₁ : c₁.mem = ArrayCopy.copyPrefix + (headerMemory x.mem b n (x.regs Reg.dimension) (x.regs Reg.groups) (x.regs Reg.prime)) + ab (b + 5) N := by rw [c₁mem, a_src, a_dst, a_len, amem, hmem] + have c₁_below (q : ℕ) (hq : q < b) : c₁.mem q = x.mem q := by + rw [c₁mem, a_dst, ArrayCopy.copyPrefix_outside (by omega)] + exact a_below q hq + obtain ⟨d₂, hd₂, d₂mem, d₂src, d₂dst, d₂len, d₂total, d₂regs⟩ := + exec_nextCopy Reg.bc c₁ (by rw [c₁_dst, c₁_len]; exact fit.of_le (by omega)) + have d₂_src : d₂.regs (copyBank 0) = bc := d₂src.trans (c₁_meta Reg.bc (by decide)) + have d₂_dst : d₂.regs (copyBank 1) = b + 5 + N := by rw [d₂dst, c₁_dst, c₁_len] + have d₂_len : d₂.regs (copyBank 2) = N := d₂len.trans c₁_len + have d₂_total : d₂.regs (copyBank 7) = Sa := d₂total.trans c₁_total + have d₂_meta (j : Fin 640) (hj : j.val < 608) : d₂.regs j = x.regs j := + (d₂regs j (by omega)).trans (c₁_meta j hj) + have d₂_below (q : ℕ) (hq : q < b) : d₂.mem q = x.mem q := by + rw [d₂mem]; exact c₁_below q hq + have d₂_sum : ArrayCopySum.wordSum d₂.mem bc N = Sb := sum_eq d₂.mem d₂_below bc hbc + obtain ⟨c₂, hc₂, c₂mem, c₂src, c₂dst, c₂len, c₂total, c₂regs⟩ := exec_copy d₂ h1 + (by rw [d₂_src, d₂_len]; exact fit.of_le (by omega)) + (by rw [d₂_dst, d₂_len]; exact fit.of_le (by omega)) + (by rw [d₂_total, d₂_src, d₂_len, d₂_sum]; exact fit.of_le (by omega)) + (by rw [d₂_src, d₂_dst, d₂_len]; omega) + have hc₂' : ExecWithin W (ArrayCopySum.program.rename copyBank) d₂ c₂ (8 * N + 4) := by + simpa only [d₂_len] using hc₂ + have c₂_dst : c₂.regs (copyBank 1) = b + 5 + N := c₂dst.trans d₂_dst + have c₂_len : c₂.regs (copyBank 2) = N := c₂len.trans d₂_len + have c₂_total : c₂.regs (copyBank 7) = Sa + Sb := by + simpa only [d₂_total, d₂_src, d₂_len, d₂_sum] using c₂total + have c₂_meta (j : Fin 640) (hj : j.val < 608) : c₂.regs j = x.regs j := + (c₂regs j (Or.inl (by omega))).trans (d₂_meta j hj) + have cm₂ : c₂.mem = ArrayCopy.copyPrefix c₁.mem bc (b + 5 + N) N := by + rw [c₂mem, d₂_src, d₂_dst, d₂_len, d₂mem] + have c₂_below (q : ℕ) (hq : q < b) : c₂.mem q = x.mem q := by + rw [c₂mem, d₂_dst, ArrayCopy.copyPrefix_outside (by omega)] + exact d₂_below q hq + obtain ⟨d₃, hd₃, d₃mem, d₃src, d₃dst, d₃len, d₃total, d₃regs⟩ := + exec_nextCopy Reg.ac c₂ (by rw [c₂_dst, c₂_len]; exact fit.of_le (by omega)) + have d₃_src : d₃.regs (copyBank 0) = ac := d₃src.trans (c₂_meta Reg.ac (by decide)) + have d₃_dst : d₃.regs (copyBank 1) = b + 5 + N + N := by rw [d₃dst, c₂_dst, c₂_len] + have d₃_len : d₃.regs (copyBank 2) = N := d₃len.trans c₂_len + have d₃_total : d₃.regs (copyBank 7) = Sa + Sb := d₃total.trans c₂_total + have d₃_meta (j : Fin 640) (hj : j.val < 608) : d₃.regs j = x.regs j := + (d₃regs j (by omega)).trans (c₂_meta j hj) + have d₃_below (q : ℕ) (hq : q < b) : d₃.mem q = x.mem q := by + rw [d₃mem]; exact c₂_below q hq + have d₃_sum : ArrayCopySum.wordSum d₃.mem ac N = Sc := sum_eq d₃.mem d₃_below ac hac + obtain ⟨c₃, hc₃, c₃mem, c₃src, c₃dst, c₃len, c₃total, c₃regs⟩ := exec_copy d₃ h1 + (by rw [d₃_src, d₃_len]; exact fit.of_le (by omega)) + (by rw [d₃_dst, d₃_len]; exact fit.of_le (by omega)) + (by rw [d₃_total, d₃_src, d₃_len, d₃_sum]; exact fit.of_le (by omega)) + (by rw [d₃_src, d₃_dst, d₃_len]; omega) + have hc₃' : ExecWithin W (ArrayCopySum.program.rename copyBank) d₃ c₃ (8 * N + 4) := by + simpa only [d₃_len] using hc₃ + have c₃_total : c₃.regs (copyBank 7) = T := by + simpa only [d₃_total, d₃_src, d₃_len, d₃_sum] using c₃total + have c₃_meta (j : Fin 640) (hj : j.val < 608) : c₃.regs j = x.regs j := + (c₃regs j (Or.inl (by omega))).trans (d₃_meta j hj) + have cm₃ : c₃.mem = ArrayCopy.copyPrefix c₂.mem ac (b + 5 + N + N) N := by + rw [c₃mem, d₃_src, d₃_dst, d₃_len, d₃mem] + let y := c₃.set Reg.total T + have hsave : ExecWithin (B := .standard) W (.op (.copy Reg.total (copyBank 7))) c₃ y 1 := by + simpa only [y, c₃_total] using + (ExecWithin.copy (B := .standard) (w := W) (d := Reg.total) (s := copyBank 7) (x := c₃)) + refine ⟨y, (hh.seq (ha.seq (hc₁'.seq (hd₂.seq (hc₂'.seq (hd₃.seq (hc₃'.seq hsave))))))).mono + (by change 17 + (4 + (8 * N + 4 + (2 + (8 * N + 4 + (2 + (8 * N + 4 + 1)))))) ≤ + 24 * N + 38 + omega), ?_, ?_, ?_⟩ + · change c₃.mem = _ + rw [cm₃, cm₂, cm₁] + rfl + · change (c₃.set Reg.total T).regs Reg.total = T + exact Function.update_self Reg.total T c₃.regs + · intro j hj + have hne : j ≠ Reg.total := by + intro he + have hv := congrArg Fin.val he + change j.val = 608 at hv + omega + simpa only [y, Data.set_regs, Function.update_of_ne hne] using c₃_meta j hj + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Admission.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Admission.lean new file mode 100755 index 0000000000..5067048048 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Admission.lean @@ -0,0 +1,76 @@ +/- +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.CallableFixedPrime.Core +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.InputSpec +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Setup +import Complexity.Foundations.Data.Nat.Log + +/-! +# Original-parameter caller admission + +The physical threshold includes the caller's raw old-word bound P, so dirty words before +their actual remainder instructions fit the physical machine. P is a bound on original +caller data, not a computed layout, source execution or algorithm argument. Source width +and its actual runtime modulus depend only on original scalars and the copied word sum. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM +open Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- Positive physical width for original caller words, source addresses and every setup fit. -/ +@[expose] def admissionWidth (n D g p total b P : ℕ) : ℕ := + Nat.clog 2 (b + 4 * windowSize n D g p total + P + 1024) + 1 + +/-- A physical-width-independent bound for prefix words and new address support. -/ +@[expose] def wordBound (n D g p total b P : ℕ) : ℕ := + 4 * (b + 4 * windowSize n D g p total + P + 1024) + +/-- Caller admission is positive even without geometric assumptions. -/ +theorem admissionWidth_pos (n D g p total b P : ℕ) : 0 < admissionWidth n D g p total b P := by + unfold admissionWidth + omega + +/-- Every wider width contains the caller's raw dirty words and the actual source reservation. -/ +theorem admission_fits {W n D g p total b P : ℕ} + (hW : admissionWidth n D g p total b P ≤ W) : + Fits W (b + 4 * windowSize n D g p total + P + 1024) := by + have hw : Nat.clog 2 (b + 4 * windowSize n D g p total + P + 1024) < W := by + unfold admissionWidth at hW + omega + exact (Nat.le_pow_clog (by decide : 1 < (2 : ℕ)) _).trans_lt + (Nat.pow_lt_pow_right (by decide : 1 < (2 : ℕ)) hw) + +/-- The real copied input span fits the computed source window before the solver begins. -/ +theorem inputEnd_le_window {m n g p : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) : + 5 + 3 * (n * n) ≤ windowSize n (D m) g p (rawTotal n values) := by + have hi := input_fits_source (m := m) (g := g) (p := p) values hlen + (natAbs_le_rawTotal values hlen) + have h := hi.1 + simp only [PreparationInput.input, List.length_append, List.length_cons, List.length_nil, + List.length_map, hlen, Nat.reduceAdd] at h + change _ < windowSize n (D m) g p (rawTotal n values) at h + omega + +/-- The width's power of two is bounded by a fixed original-input numerical envelope. -/ +theorem pow_admissionWidth_le (n D g p total b P : ℕ) : + 2 ^ admissionWidth n D g p total b P ≤ wordBound n D g p total b P := by + let E := b + 4 * windowSize n D g p total + P + 1024 + have he : E ≠ 0 := by dsimp only [E]; omega + have hp := Nat.pow_clog_le_mul (by decide : 1 < (2 : ℕ)) he + change 2 ^ (Nat.clog 2 E + 1) ≤ 4 * E + rw [pow_succ] + omega + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Copy.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Copy.lean new file mode 100755 index 0000000000..278c5252a3 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Copy.lean @@ -0,0 +1,134 @@ +/- +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.CallableFixedPrime.Header + +/-! +# Charged copies in the caller's high register bank + +This internal call rule embeds the actual eight-register copy/sum loop. Only the source, +destination and sum bounds are needed; the caller metadata and low selector bank are framed +without unfolding the loop. The full adapter discharges these bounds from original inputs. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM + +private theorem copyBank_injective : Function.Injective copyBank := by + intro i j h + have hv := congrArg Fin.val h + exact Fin.ext (by simpa only [copyBank] using Nat.add_left_cancel hv) + +/-- Deliver the original AB arguments and zero accumulator after the real header. -/ +theorem exec_firstCopy {W : ℕ} (x : Data 640) (hc : x.regs Reg.constant = 5) + (hfit : Fits W (x.regs Reg.base + 5)) : + ∃ y, ExecWithin W firstCopy x y 4 ∧ y.mem = x.mem ∧ + y.regs (copyBank 0) = x.regs Reg.ab ∧ + y.regs (copyBank 1) = x.regs Reg.base + 5 ∧ + y.regs (copyBank 2) = x.regs Reg.area ∧ y.regs (copyBank 7) = 0 ∧ + ∀ j : Fin 640, j.val < 620 → y.regs j = x.regs j := by + let y := (((x.set (copyBank 0) (x.regs Reg.ab)).set (copyBank 1) + (x.regs Reg.base + 5)).set (copyBank 2) (x.regs Reg.area)).set (copyBank 7) 0 + have he : ExecWithin W firstCopy x y 4 := by + ram_eval [firstCopy, y, copyBank, hc, hfit, Reg.ab, Reg.base, Reg.area, + Reg.constant, Fin.mk.injEq] + refine ⟨y, he, rfl, ?_, ?_, ?_, ?_, ?_⟩ + · simp [y, copyBank] + · simp [y, copyBank] + · simp [y, copyBank] + · simp [y, copyBank] + · intro j hj + apply he.regs_eq + have hn (i : Fin 8) : copyBank i ≠ j := by + intro h + have hv := congrArg Fin.val h + change 620 + i.val = j.val at hv + omega + simp [firstCopy, Code.Preserves, Op.dest, Op.bin, hn] + +/-- Deliver a subsequent matrix pointer and advance only the destination span. -/ +theorem exec_nextCopy {W : ℕ} (src : Fin 640) (x : Data 640) + (hfit : Fits W (x.regs (copyBank 1) + x.regs (copyBank 2))) : + ∃ y, ExecWithin W (nextCopy src) x y 2 ∧ y.mem = x.mem ∧ + y.regs (copyBank 0) = x.regs src ∧ + y.regs (copyBank 1) = x.regs (copyBank 1) + x.regs (copyBank 2) ∧ + y.regs (copyBank 2) = x.regs (copyBank 2) ∧ + y.regs (copyBank 7) = x.regs (copyBank 7) ∧ + ∀ j : Fin 640, j.val < 620 → y.regs j = x.regs j := by + let a := x.set (copyBank 0) (x.regs src) + let y := a.set (copyBank 1) (x.regs (copyBank 1) + x.regs (copyBank 2)) + have hfirst : ExecWithin (B := .standard) W (.op (.copy (copyBank 0) src)) x a 1 := + ExecWithin.copy + have hsecond : ExecWithin W + (.op (.bin .add (copyBank 1) (copyBank 1) (copyBank 2))) a y 1 := by + simpa [a, y, copyBank, BinOp.eval] using + (ExecWithin.bin (w := W) (f := .add) (d := copyBank 1) (i := copyBank 1) + (j := copyBank 2) (x := a) + (by simpa [a, copyBank] using hfit)) + have he : ExecWithin W (nextCopy src) x y 2 := hfirst.seq hsecond + refine ⟨y, he, rfl, ?_, ?_, ?_, ?_, ?_⟩ + · simp [y, a, copyBank] + · simp [y, a, copyBank] + · simp [y, a, copyBank] + · simp [y, a, copyBank] + · intro j hj + apply he.regs_eq + have hn (i : Fin 8) : copyBank i ≠ j := by + intro h + have hv := congrArg Fin.val h + change 620 + i.val = j.val at hv + omega + simp [nextCopy, Code.Preserves, Op.dest, Op.bin, hn] + +/-- Actual copied words and running sum, with all caller registers outside the eight scratch +registers unchanged. This stage theorem is an implementation interface. -/ +theorem exec_copy {W : ℕ} (x : Data 640) (h1 : Fits W 1) + (hs : Fits W (x.regs (copyBank ArrayCopySum.Reg.src) + + x.regs (copyBank ArrayCopySum.Reg.len))) + (hd : Fits W (x.regs (copyBank ArrayCopySum.Reg.dst) + + x.regs (copyBank ArrayCopySum.Reg.len))) + (ht : Fits W (x.regs (copyBank ArrayCopySum.Reg.total) + + ArrayCopySum.wordSum x.mem (x.regs (copyBank ArrayCopySum.Reg.src)) + (x.regs (copyBank ArrayCopySum.Reg.len)))) + (hsep : x.regs (copyBank ArrayCopySum.Reg.src) + + x.regs (copyBank ArrayCopySum.Reg.len) ≤ x.regs (copyBank ArrayCopySum.Reg.dst)) : + ∃ y, ExecWithin W (ArrayCopySum.program.rename copyBank) x y + (8 * x.regs (copyBank ArrayCopySum.Reg.len) + 4) ∧ + y.mem = ArrayCopy.copyPrefix x.mem (x.regs (copyBank ArrayCopySum.Reg.src)) + (x.regs (copyBank ArrayCopySum.Reg.dst)) (x.regs (copyBank ArrayCopySum.Reg.len)) ∧ + y.regs (copyBank ArrayCopySum.Reg.src) = x.regs (copyBank ArrayCopySum.Reg.src) ∧ + y.regs (copyBank ArrayCopySum.Reg.dst) = x.regs (copyBank ArrayCopySum.Reg.dst) ∧ + y.regs (copyBank ArrayCopySum.Reg.len) = x.regs (copyBank ArrayCopySum.Reg.len) ∧ + y.regs (copyBank ArrayCopySum.Reg.total) = x.regs (copyBank ArrayCopySum.Reg.total) + + ArrayCopySum.wordSum x.mem (x.regs (copyBank ArrayCopySum.Reg.src)) + (x.regs (copyBank ArrayCopySum.Reg.len)) ∧ + ∀ j : Fin 640, j.val < 620 ∨ 628 ≤ j.val → y.regs j = x.regs j := by + obtain ⟨a, ha, hm, hs', hd', hl, ht'⟩ := ArrayCopySum.exec (x.comap copyBank) + h1 hs hd ht hsep + let y := a.extend copyBank x + have hy : ExecWithin W (ArrayCopySum.program.rename copyBank) x y + (8 * x.regs (copyBank ArrayCopySum.Reg.len) + 4) := ha.rename copyBank_injective + refine ⟨y, hy, hm, + (copyBank_injective.extend_apply _ _ _).trans hs', + (copyBank_injective.extend_apply _ _ _).trans hd', + (copyBank_injective.extend_apply _ _ _).trans hl, + (copyBank_injective.extend_apply _ _ _).trans ht', ?_⟩ + intro j hj + apply hy.regs_eq + apply Code.preserves_rename_of_forall_ne + intro i he + have hv := congrArg Fin.val he + have hi := i.isLt + change 620 + i.val = j.val at hv + rcases hj with h | h <;> omega + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Core.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Core.lean new file mode 100755 index 0000000000..eae62d4ea2 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Core.lean @@ -0,0 +1,106 @@ +/- +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.CallableFixedPrime.Source +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Parameters +public import Complexity.Computability.WordRAM.MemoryWindow + +/-! +# Actual translated fixed-prime solver execution + +This internal stage composes the proved original-input source execution with the existing +memory-window compiler. The caller's real setup supplies normalized source registers and the +computed modulus. No source execution, list of records, readback, solver or time contract is +a premise. Dirty physical memory is clipped by each translated load itself. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle +open Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- Canonical original inputs fit the width computed from a bounding raw-word sum. -/ +theorem input_fits_source {m n g p total : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hv : ∀ z ∈ values, z.natAbs ≤ total) : + InputFits (sourceWidth n (D m) g p total) + (PreparationInput.input n (D m) g p values) := by + have hr := FixedPrime.record_admitted (source_admission n (D m) g p total) + have hprep : PreparationInput.width n (D m) g p total ≤ sourceWidth n (D m) g p total := by + unfold RecordWitness.admissionWidth RecordProduct.admissionWidth at hr + omega + exact (PreparationInput.input_fits values hlen hv).mono hprep + +/-- Translate the actual complete source computation into its dirty physical window. Source +register fits here are an internal setup postcondition, not a final caller admission premise. +The one global scan allowance and both positive/negative decisions are preserved exactly. -/ +theorem exec_compiled {W b m n g p total : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hD : 16 ≤ D m) + (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D m)) (hN : D m ^ 18 ≤ n) + (hv : ∀ z ∈ values, z.natAbs ≤ total) + (x : Data 419) (hb : x.regs MemoryWindow.Reg.base = b) + (hm : x.regs MemoryWindow.Reg.modulus = windowSize n (D m) g p total) + (hregs : ∀ i : Fin 416, Fits (sourceWidth n (D m) g p total) (x.regs (i.castAdd 3))) + (hinput : ∀ q < 5 + 3 * (n * n), x.mem (b + q) = + (Data.init (PreparationInput.input n (D m) g p values) : Data 64).mem q) + (hw : sourceWidth n (D m) g p total ≤ W) + (hfit : Fits W (b + windowSize n (D m) g p total)) : + let V := fun q => values.getD q 0 + let wAB := fun u v : Fin n => V (pairIndex (u, v)) + let wBC := fun b c : Fin n => V (n * n + pairIndex (b, c)) + let wAC := fun u c : Fin n => V (2 * (n * n) + pairIndex (u, c)) + 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, + Instances.Output n (D m) g p V + (.init (PreparationInput.input n (D m) g p values)) a ∧ + ∃ y, ExecWithin W (MemoryWindow.compile FixedPrime.program) x y + (3 * FixedPrime.timeBound (m := m) hn g p values a.mem) ∧ + (y.regs (FixedPrime.Reg.found.castAdd 3) = 0 ∨ + y.regs (FixedPrime.Reg.found.castAdd 3) = 1) ∧ + y.regs (FixedPrime.Reg.scans.castAdd 3) ≤ falsePositiveCount wAB wBC wAC p + + y.regs (FixedPrime.Reg.found.castAdd 3) ∧ + (y.regs (FixedPrime.Reg.found.castAdd 3) = 1 ↔ HasZeroTriangle wAB wBC wAC) ∧ + (y.regs (FixedPrime.Reg.found.castAdd 3) = 1 → + y.regs ((FixedPrime.recordBank RecordWitness.Reg.witnessA).castAdd 3) < n ∧ + y.regs ((FixedPrime.recordBank RecordWitness.Reg.witnessB).castAdd 3) < n ∧ + y.regs ((FixedPrime.recordBank RecordWitness.Reg.witnessC).castAdd 3) < n ∧ + V (y.regs ((FixedPrime.recordBank RecordWitness.Reg.witnessA).castAdd 3) * n + + y.regs ((FixedPrime.recordBank RecordWitness.Reg.witnessB).castAdd 3)) + + V (n * n + (y.regs ((FixedPrime.recordBank RecordWitness.Reg.witnessB).castAdd 3) * n + + y.regs ((FixedPrime.recordBank RecordWitness.Reg.witnessC).castAdd 3))) + + V (2 * (n * n) + + (y.regs ((FixedPrime.recordBank RecordWitness.Reg.witnessA).castAdd 3) * n + + y.regs ((FixedPrime.recordBank RecordWitness.Reg.witnessC).castAdd 3))) = 0) ∧ + ∀ q, q < b ∨ b + windowSize n (D m) g p total ≤ q → y.mem q = x.mem q := by + let v := MemoryWindow.view (sourceWidth n (D m) g p total) b x + have vb := MemoryWindow.view_bounded (sourceWidth n (D m) g p total) b x hregs + have hi := Data.Bounded.init (r := 64) + (input_fits_source (m := m) (g := g) (p := p) values hlen hv) + have vi (q : ℕ) (hq : q < 5 + 3 * (n * n)) : v.mem q = + (Data.init (PreparationInput.input n (D m) g p values) : Data 64).mem q := by + change x.mem (b + q) % 2 ^ sourceWidth n (D m) g p total = _ + rw [hinput q hq, Nat.mod_eq_of_lt (hi.2 q)] + have htwo : sourceWidth n (D m) g p total - 2 + 2 = sourceWidth n (D m) g p total := + Nat.sub_add_cancel (by have := sourceWidth_two_lt n (D m) g p total; omega) + have hs := exec_source (w := sourceWidth n (D m) g p total - 2) values hlen hD hg hp hN hv + (by simpa only [htwo] using source_admission n (D m) g p total) v vi + rw [htwo] at hs + obtain ⟨a, hout, z, hz, zf, zs, ziff, zw, -⟩ := hs + obtain ⟨y, hy, hm', hf⟩ := MemoryWindow.execWithin hz FixedPrime.program_not_readsWidth + vb (show MemoryWindow.Matches (sourceWidth n (D m) g p total) b v x from + ⟨rfl, hb, hm⟩) hw hfit + refine ⟨a, hout, y, hy, ?_, ?_, ?_, ?_, hf⟩ + · simpa only [hm'.regs] using zf + · simpa only [hm'.regs] using zs + · simpa only [hm'.regs] using ziff + · simpa only [hm'.regs] using zw + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Exec.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Exec.lean new file mode 100755 index 0000000000..d9840278fd --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Exec.lean @@ -0,0 +1,153 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +module +-- upstream: candidate + +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Adapt +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Admission +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Receive + +/-! +# Complete caller-safe fixed-prime solver execution + +Only runtime original scalars, canonical signed arrays and caller workspace are inputs. The +program copies those arrays once, computes its width, runs the real one-time producer and +all-record solver, and returns its actual original-coordinate witness. The proof's reference +prepared state is an output of the derivation, never a layout/run/time certificate supplied +by the caller. Raw old-word bounds include dirty words before any normalization. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle +open Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- All adaptation, computed modulus, translated source and five return copies, before halt. +The reference memory only indexes existing finite charges; it is not an algorithm input. -/ +@[expose] noncomputable def timeBound {m n : ℕ} (hn : 0 < n) (g p : ℕ) + (values : List ℤ) (mem : ℕ → ℕ) : ℕ := + 24 * (n * n) + 24669 * Nat.clog 2 (n + D m + g + p + rawTotal n values + 4) + 482 + + 3 * FixedPrime.timeBound (m := m) hn g p values mem + +/-- Complete actual native caller execution, with the selector bank and original call arguments +protected. The original source spans may alias each other and all remaining memory may be dirty. +No source execution, catalogue, order, solver, witness or time bound is supplied as a premise. -/ +theorem exec {W m n g p b : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hD : 16 ≤ D m) + (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D m)) (hN : D m ^ 18 ≤ n) + (x : Data 640) (xn : x.regs Reg.n = n) (xD : x.regs Reg.dimension = D m) + (xg : x.regs Reg.groups = g) (xp : x.regs Reg.prime = p) (xb : x.regs Reg.base = b) + (hab : x.regs Reg.ab + n * n ≤ b) (hbc : x.regs Reg.bc + n * n ≤ b) + (hac : x.regs Reg.ac + n * n ≤ b) + (vab : ∀ q < n * n, x.mem (x.regs Reg.ab + q) = Signed.encode (values.getD q 0)) + (vbc : ∀ q < n * n, x.mem (x.regs Reg.bc + q) = Signed.encode (values.getD (n * n + q) 0)) + (vac : ∀ q < n * n, x.mem (x.regs Reg.ac + q) = + Signed.encode (values.getD (2 * (n * n) + q) 0)) + (hx : x.Bounded W) + (hfit : Fits W (b + 4 * windowSize n (D m) g p (rawTotal n values) + 1024)) : + let V := fun q => values.getD q 0 + let wAB := fun u v : Fin n => V (pairIndex (u, v)) + let wBC := fun u v : Fin n => V (n * n + pairIndex (u, v)) + let wAC := fun u v : Fin n => V (2 * (n * n) + pairIndex (u, v)) + 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, + Instances.Output n (D m) g p V + (.init (PreparationInput.input n (D m) g p values)) a ∧ + ∃ y, ExecWithin W program x y (timeBound (m := m) hn g p values a.mem) ∧ + y.Bounded W ∧ (y.regs Reg.found = 0 ∨ y.regs Reg.found = 1) ∧ + y.regs Reg.scans ≤ falsePositiveCount wAB wBC wAC p + y.regs Reg.found ∧ + (y.regs Reg.found = 1 ↔ HasZeroTriangle wAB wBC wAC) ∧ + (y.regs Reg.found = 1 → + y.regs Reg.witnessA < n ∧ y.regs Reg.witnessB < n ∧ y.regs Reg.witnessC < n ∧ + V (y.regs Reg.witnessA * n + y.regs Reg.witnessB) + + V (n * n + (y.regs Reg.witnessB * n + y.regs Reg.witnessC)) + + V (2 * (n * n) + (y.regs Reg.witnessA * n + y.regs Reg.witnessC)) = 0) ∧ + (∀ q, q < b ∨ b + windowSize n (D m) g p (rawTotal n values) ≤ q → + y.mem q = x.mem q) ∧ + ∀ j : Fin 640, j.val < 160 ∨ (600 ≤ j.val ∧ j.val < 608) → y.regs j = x.regs j := by + let T := rawTotal n values + have fit : Fits W (b + 4 * windowSize n (D m) g p T + 1024) := hfit + have window_fit : Fits W (b + windowSize n (D m) g p T) := fit.of_le (by omega) + obtain ⟨hw, hS, -, -⟩ := setup_fits fit + have hT : T ≤ windowSize n (D m) g p T := by omega + have hI : 5 + 3 * (n * n) ≤ windowSize n (D m) g p T := + inputEnd_le_window (m := m) (g := g) (p := p) values hlen + have hsum : matrixWordSum x.mem n (x.regs Reg.ab) (x.regs Reg.bc) (x.regs Reg.ac) = T := + matrixWordSum_eq_rawTotal x.mem values vab vbc vac + obtain ⟨a, ha, amem, atotal, ameta⟩ := exec_adapt x + (by simpa only [xn, xb] using hab) (by simpa only [xn, xb] using hbc) + (by simpa only [xn, xb] using hac) + (by rw [xn, xb, hsum]; exact fit.of_le (by omega)) + have ha' : ExecWithin W adapt x a (24 * (n * n) + 38) := by simpa only [xn] using ha + have an : a.regs Reg.n = n := (ameta _ (by decide)).trans xn + have aD : a.regs Reg.dimension = D m := (ameta _ (by decide)).trans xD + have ag : a.regs Reg.groups = g := (ameta _ (by decide)).trans xg + have ap : a.regs Reg.prime = p := (ameta _ (by decide)).trans xp + have ab : a.regs Reg.base = b := (ameta _ (by decide)).trans xb + have asum : a.regs Reg.total = T := by simpa only [xn, hsum] using atotal + have ai (q : ℕ) (hq : q < 5 + 3 * (n * n)) : a.mem (b + q) = + (Data.init (PreparationInput.input n (D m) g p values) : Data 64).mem q := by + rw [amem, xn, xD, xg, xp, xb] + exact copyMemory_input x.mem values hlen hab hbc hac vab vbc vac q hq + have af (q : ℕ) (hq : q < b ∨ b + windowSize n (D m) g p T ≤ q) : a.mem q = x.mem q := by + rw [amem, xn, xD, xg, xp, xb] + exact copyMemory_outside _ _ _ _ _ _ _ _ _ _ (by omega) + obtain ⟨s, hs, smem, sb, sM, sr, -⟩ := exec_setup a + (by simpa only [an, aD, ag, ap, asum, ab] using fit) + have hs' : ExecWithin W setup a s + (24669 * Nat.clog 2 (n + D m + g + p + T + 4) + 439) := by + simpa only [an, aD, ag, ap, asum] using hs + have sb' : s.regs (sourceBank MemoryWindow.Reg.base) = b := sb.trans ab + have sM' : s.regs (sourceBank MemoryWindow.Reg.modulus) = windowSize n (D m) g p T := by + simpa only [an, aD, ag, ap, asum] using sM + have sr' (i : Fin 416) : Fits (sourceWidth n (D m) g p T) (s.regs (sourceReg i)) := by + simpa only [an, aD, ag, ap, asum] using sr i + have si (q : ℕ) (hq : q < 5 + 3 * (n * n)) : s.mem (b + q) = + (Data.init (PreparationInput.input n (D m) g p values) : Data 64).mem q := by + rw [smem]; exact ai q hq + obtain ⟨reference, hout, z, hz, zf, zs, ziff, zw, zframe⟩ := exec_compiled values hlen + hD hg hp hN (natAbs_le_rawTotal values hlen) (s.comap sourceBank) sb' sM' sr' si hw window_fit + let z' := z.extend sourceBank s + have hsolve : ExecWithin W solve s z' + (3 * FixedPrime.timeBound (m := m) + (lt_of_lt_of_le (by omega : 0 < D m) + ((Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN)) + g p values reference.mem) := hz.rename sourceBank_injective + obtain ⟨y, hy, ymem, yf, ya, yb, yc, ys⟩ := exec_receive (W := W) z' + have zreg (i : Fin 416) : z'.regs (sourceReg i) = z.regs (i.castAdd 3) := + sourceBank_injective.extend_apply _ _ _ + have yF : y.regs Reg.found = z.regs (FixedPrime.Reg.found.castAdd 3) := yf.trans (zreg _) + have yA : y.regs Reg.witnessA = + z.regs ((FixedPrime.recordBank RecordWitness.Reg.witnessA).castAdd 3) := ya.trans (zreg _) + have yB : y.regs Reg.witnessB = + z.regs ((FixedPrime.recordBank RecordWitness.Reg.witnessB).castAdd 3) := yb.trans (zreg _) + have yC : y.regs Reg.witnessC = + z.regs ((FixedPrime.recordBank RecordWitness.Reg.witnessC).castAdd 3) := yc.trans (zreg _) + have yS : y.regs Reg.scans = z.regs (FixedPrime.Reg.scans.castAdd 3) := ys.trans (zreg _) + have he : ExecWithin W program x y + (timeBound (m := m) + (lt_of_lt_of_le (by omega : 0 < D m) + ((Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN)) + g p values reference.mem) := by + apply (ha'.seq (hs'.seq (hsolve.seq hy))).mono + dsimp only [timeBound, T] + exact le_of_eq (by ring) + refine ⟨reference, hout, y, he, he.bounded hx, ?_, ?_, ?_, ?_, ?_, ?_⟩ + · simpa only [yF] using zf + · simpa only [yS, yF] using zs + · simpa only [yF] using ziff + · simpa only [yF, yA, yB, yC] using zw + · intro q hq + have hf : z'.mem q = s.mem q := zframe q hq + exact (congrFun ymem q).trans (hf.trans ((congrFun smem q).trans (af q hq))) + · intro j hj + exact he.regs_eq (program_preserves j hj) + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Header.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Header.lean new file mode 100755 index 0000000000..05e95bbfc0 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Header.lean @@ -0,0 +1,71 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +module +-- upstream: candidate + +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Program + +/-! +# Real scalar-header stores for the caller adapter + +The five stores create the existing preparation input convention in caller workspace. This +is only a fixed-size header, with no array/table initialization hidden in its specification. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM + +/-- The memory after the five actual scalar-header stores. -/ +@[expose] def headerMemory (mem : ℕ → ℕ) (base n D g p : ℕ) : ℕ → ℕ := + Function.update (Function.update (Function.update (Function.update (Function.update mem + base (n * n * 3 + 4)) (base + 1) D) (base + 2) g) (base + 3) n) (base + 4) p + +/-- The unchanged original scalar registers supply every header store and length computation. -/ +theorem exec_header {W : ℕ} (x : Data 640) + (hfit : Fits W (x.regs Reg.base + 4 * (x.regs Reg.n * x.regs Reg.n) + 1024)) : + ∃ y, ExecWithin W header x y 17 ∧ + y.regs Reg.area = x.regs Reg.n * x.regs Reg.n ∧ y.regs Reg.constant = 5 ∧ + y.mem = headerMemory x.mem (x.regs Reg.base) (x.regs Reg.n) + (x.regs Reg.dimension) (x.regs Reg.groups) (x.regs Reg.prime) ∧ + ∀ j : Fin 640, j.val < 609 → y.regs j = x.regs j := by + let n := x.regs Reg.n + let b := x.regs Reg.base + have h1 : Fits W 1 := 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 h5 : Fits W 5 := hfit.of_le (by omega) + have ha : Fits W (n * n) := hfit.of_le (by dsimp only [n]; omega) + have hat : Fits W (n * n * 3) := hfit.of_le (by dsimp only [n]; omega) + have hal : Fits W (n * n * 3 + 4) := hfit.of_le (by dsimp only [n]; omega) + have hb1 : Fits W (b + 1) := hfit.of_le (by dsimp only [b]; omega) + have hb2 : Fits W (b + 2) := hfit.of_le (by dsimp only [b]; omega) + have hb3 : Fits W (b + 3) := hfit.of_le (by dsimp only [b]; omega) + have hb4 : Fits W (b + 4) := hfit.of_le (by dsimp only [b]; omega) + refine ⟨?y, ?run, ?area, ?constant, ?memory, ?regs⟩ + case run => ram_eval [header, n, b, h1, h3, h4, h5, ha, hat, hal, hb1, hb2, hb3, hb4, + Reg.n, Reg.dimension, Reg.groups, Reg.prime, Reg.base, Reg.area, Reg.length, + Reg.address, Reg.one, Reg.constant, Fin.mk.injEq] + case area => simp +decide + case constant => simp +decide + case memory => rfl + case regs => + intro j hj + have hn (i : Fin 640) (hi : 609 ≤ i.val) : j ≠ i := by + intro he + have hv := congrArg Fin.val he + omega + simp only [Data.set_regs, Data.write_regs, + Function.update_of_ne (hn Reg.area (by decide)), + Function.update_of_ne (hn Reg.length (by decide)), + Function.update_of_ne (hn Reg.address (by decide)), + Function.update_of_ne (hn Reg.one (by decide)), + Function.update_of_ne (hn Reg.constant (by decide))] + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Input.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Input.lean new file mode 100755 index 0000000000..7892f4f1fc --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Input.lean @@ -0,0 +1,108 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +module +-- upstream: candidate + +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Exec + +/-! +# Actual initialized entry for the callable fixed-prime solver + +The input convention is exactly `PreparationInput.input`: four raw scalar headers followed +by three canonical signed squares. Four actual loads and native pointer arithmetic deliver +the high-bank caller arguments. Workspace starts immediately after the original input; +the subsequent adapter leaves the entire original block intact. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM + +/-- Workspace after the original input's length word, four headers and three squares. -/ +@[expose] def workspaceBase (n : ℕ) : ℕ := 5 + 3 * (n * n) + +/-- An original-input bound for the initialized caller's words. No scan or clearing of this +reservation is performed; the actual copy loop computes the source modulus later. -/ +@[expose] def inputWordBound (n D g p : ℕ) (values : List ℤ) : ℕ := + 4 * windowSize n D g p (rawTotal n values) + +/-- Positive initialized physical threshold, independent of a larger chosen width. -/ +@[expose] def inputWidth (n D g p : ℕ) (values : List ℤ) : ℕ := + admissionWidth n D g p (rawTotal n values) (workspaceBase n) (inputWordBound n D g p values) + +open Reg in +/-- Read the original raw headers and compute all actual caller pointers. -/ +@[expose] def entryHeader : Code .standard 640 := ram[ + one ← #1; address ← #1; dimension ← *address; + address ← address + one; groups ← *address; + address ← address + one; n ← *address; + address ← address + one; prime ← *address; + area ← n * n; ab ← #5; bc ← ab + area; ac ← bc + area; base ← ac + area ] + +/-- The same complete solver, with original-input argument delivery. -/ +@[expose] def entryProgram : Code .standard 640 := .seq entryHeader program + +/-- Fixed original-input setup, with every load, addition and multiplication charged. -/ +theorem entryHeader_fixed : entryHeader.size = 14 ∧ ¬entryHeader.ReadsWidth := by decide +kernel + +/-- The initialized program also has fixed code and no reads of physical width. -/ +theorem entryProgram_fixed : (entryProgram.program Reg.found).length ≤ 400014 ∧ + ¬(entryProgram.program Reg.found).ReadsWidth := by + have hno : ¬entryProgram.ReadsWidth := + not_or.mpr ⟨entryHeader_fixed.2, program_not_readsWidth⟩ + refine ⟨?_, Code.not_readsWidth_program hno _⟩ + have h := program_fixed.1 + simp only [Code.program, List.length_append, Code.length_assemble, + List.length_singleton, entryProgram, Code.size, entryHeader_fixed.1] at h ⊢ + omega + +/-- The real initialized setup provides actual runtime pointers and preserves every original +memory cell. Its only numerical premise concerns the original scalar/address arithmetic. -/ +theorem exec_entryHeader {W n D g p : ℕ} (values : List ℤ) + (hfit : Fits W (n + D + g + p + 5 + 3 * (n * n) + 1024)) : + ∃ x : Data 640, ExecWithin W entryHeader + (.init (PreparationInput.input n D g p values)) x 14 ∧ + x.mem = (Data.init (PreparationInput.input n D g p values) : Data 640).mem ∧ + x.regs Reg.n = n ∧ x.regs Reg.dimension = D ∧ + x.regs Reg.groups = g ∧ x.regs Reg.prime = p ∧ x.regs Reg.ab = 5 ∧ + x.regs Reg.bc = 5 + n * n ∧ x.regs Reg.ac = 5 + n * n + n * n ∧ + x.regs Reg.base = workspaceBase n := by + 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 h5 : Fits W 5 := hfit.of_le (by omega) + have ha : Fits W (n * n) := hfit.of_le (by omega) + have hab : Fits W (5 + n * n) := hfit.of_le (by omega) + have hac : Fits W (5 + n * n + n * n) := hfit.of_le (by omega) + have hb : Fits W (5 + n * n + n * n + n * n) := hfit.of_le (by omega) + generalize hstart : (Data.init (PreparationInput.input n D g p values) : Data 640) = initial + have hDread : initial.mem 1 = D := by rw [← hstart]; simp [Data.init, PreparationInput.input] + have hgread : initial.mem 2 = g := by rw [← hstart]; simp [Data.init, PreparationInput.input] + have hnread : initial.mem 3 = n := by rw [← hstart]; simp [Data.init, PreparationInput.input] + have hpread : initial.mem 4 = p := by rw [← hstart]; simp [Data.init, PreparationInput.input] + refine ⟨?x, ?run, ?mem, ?sizeValue, ?dimensionValue, ?groupsValue, ?primeValue, + ?ab, ?bc, ?ac, ?base⟩ + case run => ram_eval [entryHeader, hDread, hgread, hnread, hpread, + h1, h2, h3, h4, h5, ha, hab, hac, hb, Reg.one, Reg.address, + Reg.dimension, Reg.groups, Reg.n, Reg.prime, Reg.area, Reg.ab, Reg.bc, Reg.ac, Reg.base, + Fin.mk.injEq] + case mem => rfl + case sizeValue => simp +decide + case dimensionValue => simp +decide + case groupsValue => simp +decide + case primeValue => simp +decide + case ab => simp +decide + case bc => simp +decide + case ac => simp +decide + case base => + simpa +decide [workspaceBase] using + (show 5 + n * n + n * n + n * n = 5 + 3 * (n * n) by omega) + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/InputSpec.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/InputSpec.lean new file mode 100755 index 0000000000..f3428007a5 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/InputSpec.lean @@ -0,0 +1,172 @@ +/- +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.CallableFixedPrime.Header +import Mathlib.Data.List.GetD +import Mathlib.Tactic.IntervalCases + +/-! +# Original-word sum and copied-input meaning + +The runtime copy loop computes the sum of exactly the three original matrix spans. That sum +bounds every signed input magnitude and is polynomial under the original weight hypothesis. +It is not supplied as a certificate or computed by an uncharged preprocessing operation. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM + +/-- Sum accumulated by the three native matrix copies, in original row-major order. -/ +@[expose] def rawTotal (n : ℕ) (values : List ℤ) : ℕ := + ∑ q ∈ Finset.range (3 * (n * n)), Signed.encode (values.getD q 0) + +/-- No additional scan of the matrices is needed: the three copy accumulators concatenate. -/ +theorem rawTotal_split (n : ℕ) (values : List ℤ) : + rawTotal n values = + (∑ q ∈ Finset.range (n * n), Signed.encode (values.getD q 0)) + + (∑ q ∈ Finset.range (n * n), Signed.encode (values.getD (n * n + q) 0)) + + (∑ q ∈ Finset.range (n * n), Signed.encode (values.getD (2 * (n * n) + q) 0)) := by + unfold rawTotal + rw [show 3 * (n * n) = (n * n + n * n) + n * n by omega, + Finset.sum_range_add, Finset.sum_range_add] + simp only [two_mul] + +/-- Every original integer fits the magnitude supplied by the actual word accumulator. -/ +theorem natAbs_le_rawTotal {n : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (z : ℤ) (hz : z ∈ values) : + z.natAbs ≤ rawTotal n values := by + obtain ⟨q, hq, he⟩ := List.mem_iff_getElem.mp hz + have henc : z.natAbs ≤ Signed.encode z := by unfold Signed.encode; omega + apply henc.trans + have hs : Signed.encode (values.getD q 0) ≤ rawTotal n values := by + unfold rawTotal + exact Finset.single_le_sum (f := fun q : ℕ => Signed.encode (values.getD q 0)) + (fun _ _ => Nat.zero_le _) + (show q ∈ Finset.range (3 * (n * n)) from Finset.mem_range.mpr (by omega)) + simpa only [List.getD_eq_getElem _ _ hq, he] using hs + +/-- Original polynomial weight bounds also bound the computed runtime word sum. -/ +theorem rawTotal_le {n A : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hv : ∀ z ∈ values, z.natAbs ≤ A) : + rawTotal n values ≤ 3 * (n * n) * (2 * A + 1) := by + calc + _ ≤ ∑ _q ∈ Finset.range (3 * (n * n)), (2 * A + 1) := by + apply Finset.sum_le_sum + intro q hq + have hql : q < values.length := by have := Finset.mem_range.mp hq; omega + have hmem : values.getD q 0 ∈ values := by + rw [List.getD_eq_getElem _ _ hql] + exact List.getElem_mem _ + have hb := hv _ hmem + unfold Signed.encode + split_ifs <;> omega + _ = _ := by simp + +/-- Scalar stores do not change the caller prefix. -/ +theorem headerMemory_below (mem : ℕ → ℕ) (b n D g p q : ℕ) (hq : q < b) : + headerMemory mem b n D g p q = mem q := by + simp only [headerMemory, Function.update_of_ne (by omega : q ≠ b + 4), + Function.update_of_ne (by omega : q ≠ b + 3), + Function.update_of_ne (by omega : q ≠ b + 2), + Function.update_of_ne (by omega : q ≠ b + 1), + Function.update_of_ne (by omega : q ≠ b)] + +/-- The scalar header writes exactly five cells. -/ +theorem headerMemory_outside (mem : ℕ → ℕ) (b n D g p q : ℕ) + (hq : q < b ∨ b + 5 ≤ q) : headerMemory mem b n D g p q = mem q := by + simp only [headerMemory, Function.update_of_ne (by omega : q ≠ b + 4), + Function.update_of_ne (by omega : q ≠ b + 3), + Function.update_of_ne (by omega : q ≠ b + 2), + Function.update_of_ne (by omega : q ≠ b + 1), + Function.update_of_ne (by omega : q ≠ b)] + +/-- Memory after the actual five header stores and three square copies. -/ +@[expose] def copyMemory (mem : ℕ → ℕ) (b n D g p ab bc ac : ℕ) : ℕ → ℕ := + ArrayCopy.copyPrefix (ArrayCopy.copyPrefix (ArrayCopy.copyPrefix + (headerMemory mem b n D g p) ab (b + 5) (n * n)) + bc (b + 5 + n * n) (n * n)) ac (b + 5 + n * n + n * n) (n * n) + +/-- The actual copied spans never change the original caller prefix. -/ +theorem copyMemory_below (mem : ℕ → ℕ) (b n D g p ab bc ac q : ℕ) (hq : q < b) : + copyMemory mem b n D g p ab bc ac q = mem q := by + unfold copyMemory + rw [ArrayCopy.copyPrefix_outside (by omega), ArrayCopy.copyPrefix_outside (by omega), + ArrayCopy.copyPrefix_outside (by omega), headerMemory_below _ _ _ _ _ _ _ hq] + +/-- Input adaptation touches only its five header words and three original squares. -/ +theorem copyMemory_outside (mem : ℕ → ℕ) (b n D g p ab bc ac q : ℕ) + (hq : q < b ∨ b + 5 + 3 * (n * n) ≤ q) : + copyMemory mem b n D g p ab bc ac q = mem q := by + unfold copyMemory + rw [ArrayCopy.copyPrefix_outside (by omega), ArrayCopy.copyPrefix_outside (by omega), + ArrayCopy.copyPrefix_outside (by omega), headerMemory_outside _ _ _ _ _ _ _ (by omega)] + +/-- The three real copies preserve canonical signed encoding and original matrix order. +Their source arrays may alias one another; every source span precedes caller workspace. -/ +theorem copyMemory_payload {n b D g p ab bc ac : ℕ} (mem : ℕ → ℕ) (values : List ℤ) + (hab : ab + n * n ≤ b) (hbc : bc + n * n ≤ b) (hac : ac + n * n ≤ b) + (vab : ∀ q < n * n, mem (ab + q) = Signed.encode (values.getD q 0)) + (vbc : ∀ q < n * n, mem (bc + q) = Signed.encode (values.getD (n * n + q) 0)) + (vac : ∀ q < n * n, mem (ac + q) = Signed.encode (values.getD (2 * (n * n) + q) 0)) + (q : ℕ) (hq : q < 3 * (n * n)) : + copyMemory mem b n D g p ab bc ac (b + 5 + q) = Signed.encode (values.getD q 0) := by + by_cases hfirst : q < n * n + · unfold copyMemory + rw [ArrayCopy.copyPrefix_outside (by omega), ArrayCopy.copyPrefix_outside (by omega), + ArrayCopy.copyPrefix_read hfirst, headerMemory_below _ _ _ _ _ _ _ (by omega)] + exact vab q hfirst + · by_cases hsecond : q < 2 * (n * n) + · have hj : q - n * n < n * n := by omega + have he : b + 5 + q = b + 5 + n * n + (q - n * n) := by omega + unfold copyMemory + rw [ArrayCopy.copyPrefix_outside (by omega), he, + ArrayCopy.copyPrefix_read hj, ArrayCopy.copyPrefix_outside (by omega), + headerMemory_below _ _ _ _ _ _ _ (by omega)] + have hv := vbc (q - n * n) hj + simpa only [show n * n + (q - n * n) = q by omega] using hv + · have hj : q - 2 * (n * n) < n * n := by omega + have he : b + 5 + q = b + 5 + n * n + n * n + (q - 2 * (n * n)) := by omega + unfold copyMemory + rw [he, ArrayCopy.copyPrefix_read hj, + ArrayCopy.copyPrefix_outside (by omega), ArrayCopy.copyPrefix_outside (by omega), + headerMemory_below _ _ _ _ _ _ _ (by omega)] + have hv := vac (q - 2 * (n * n)) hj + simpa only [show 2 * (n * n) + (q - 2 * (n * n)) = q by omega] using hv + +/-- The copied words form exactly the existing initialized input block. This is readback of +actual stores and copies, not an input layout supplied to the algorithm. -/ +theorem copyMemory_input {n b D g p ab bc ac : ℕ} (mem : ℕ → ℕ) (values : List ℤ) + (hlen : values.length = 3 * (n * n)) + (hab : ab + n * n ≤ b) (hbc : bc + n * n ≤ b) (hac : ac + n * n ≤ b) + (vab : ∀ q < n * n, mem (ab + q) = Signed.encode (values.getD q 0)) + (vbc : ∀ q < n * n, mem (bc + q) = Signed.encode (values.getD (n * n + q) 0)) + (vac : ∀ q < n * n, mem (ac + q) = Signed.encode (values.getD (2 * (n * n) + q) 0)) + (q : ℕ) (hq : q < 5 + 3 * (n * n)) : + copyMemory mem b n D g p ab bc ac (b + q) = + (Data.init (PreparationInput.input n D g p values) : Data 64).mem q := by + by_cases hh : q < 5 + · have hhead : copyMemory mem b n D g p ab bc ac (b + q) = + headerMemory mem b n D g p (b + q) := by + unfold copyMemory + rw [ArrayCopy.copyPrefix_outside (by omega), ArrayCopy.copyPrefix_outside (by omega), + ArrayCopy.copyPrefix_outside (by omega)] + rw [hhead] + interval_cases q <;> + simp [headerMemory, Data.init, PreparationInput.input, hlen, Nat.mul_comm, Nat.add_comm, + ← Nat.add_assoc] + · have hr : q - 5 < 3 * (n * n) := by omega + rw [show b + q = b + 5 + (q - 5) by omega, + copyMemory_payload mem values hab hbc hac vab vbc vac (q - 5) hr] + have hv := PreparationInput.input_word n D g p values (q - 5) + simpa only [show 5 + (q - 5) = q by omega] using hv.symm + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Parameters.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Parameters.lean new file mode 100755 index 0000000000..656d5d73dd --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Parameters.lean @@ -0,0 +1,103 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +module +-- upstream: candidate + +public import Complexity.Algorithms.WordRAM.ExactTriangle.FixedPrime + +/-! +# Computable source width for the callable fixed-prime solver + +The adapter accumulates the actual unsigned input words while copying the three original +matrices. Its source width depends on that sum and the original scalar arguments, without +a supplied exponent, logarithm, intermediate layout or execution certificate. The large +constant is a conservative width bound, not an additional charged polynomial computation. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM +open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage + +/-- Width computed from the original scalars and the actual copied raw-word sum. -/ +@[expose] def sourceWidth (n D g p total : ℕ) : ℕ := + 6166 * Nat.clog 2 (n + D + g + p + total + 4) + +/-- A virtual address reservation; the program never clears or snapshots this interval. -/ +@[expose] def windowSize (n D g p total : ℕ) : ℕ := 2 ^ sourceWidth n D g p total + +private theorem admission_mono {n D g p A B : ℕ} + (hn : n ≤ B) (hD : D ≤ B) (hg : g ≤ B) (hp : p ≤ B) (hA : A ≤ B) : + FixedPrime.admissionWidth n D g p A ≤ FixedPrime.admissionWidth B B B B B := by + have henv : PreparationInput.envelope n D g p A ≤ PreparationInput.envelope B B B B B := by + dsimp only [PreparationInput.envelope, Instances.budget, Catalogue.budget] + gcongr + have hw : PreparationInput.width n D g p A ≤ PreparationInput.width B B B B B := + Nat.add_le_add_right (Nat.clog_mono_right 2 henv) 3 + have hP : PreparationInput.wordBound n D g p A ≤ PreparationInput.wordBound B B B B B := + Nat.mul_le_mul_left 16 henv + have hn2 := Nat.pow_le_pow_left hn 2 + have harg : 2 * PreparationInput.wordBound n D g p A + n + n ^ 2 + 5 ≤ + 2 * PreparationInput.wordBound B B B B B + B + B ^ 2 + 5 := by omega + have hr : RecordProduct.admissionWidth n D g p A ≤ + RecordProduct.admissionWidth B B B B B := + Nat.add_le_add hw (Nat.mul_le_mul_left 256 (Nat.clog_mono_right 2 harg)) + have hM : CallableProduct.windowSize n (n ^ 2) ≤ CallableProduct.windowSize B (B ^ 2) := by + unfold CallableProduct.windowSize CallableProduct.sourceWidth + apply Nat.pow_le_pow_right (by decide) + exact Nat.mul_le_mul_left 128 (Nat.clog_mono_right 2 (by omega)) + have henv' : RecordWitness.envelope n D g p A ≤ RecordWitness.envelope B B B B B := by + unfold RecordWitness.envelope + gcongr + have hr' : RecordWitness.admissionWidth n D g p A ≤ + RecordWitness.admissionWidth B B B B B := by + unfold RecordWitness.admissionWidth + exact Nat.add_le_add_right (max_le_max hr (Nat.clog_mono_right 2 henv')) 3 + have hC : FixedPrime.counterEnvelope n p ≤ FixedPrime.counterEnvelope B B := by + unfold FixedPrime.counterEnvelope + gcongr + exact max_le_max hr' (Nat.add_le_add_right (Nat.clog_mono_right 2 hC) 1) + +/-- A word sum bounding every original integer's magnitude guarantees the whole source +admission. This is a numerical theorem; the adapter computes the sum and logarithm itself. -/ +theorem source_admission (n D g p total : ℕ) : + FixedPrime.admissionWidth n D g p total ≤ sourceWidth n D g p total := by + let B := n + D + g + p + total + 2 + have hm : FixedPrime.admissionWidth n D g p total ≤ + FixedPrime.admissionWidth B B B B B := admission_mono (by omega) (by omega) + (by omega) (by omega) (by omega) + have hl := FixedPrime.admissionWidth_le_log (κ := 1) (A := B) (by omega : 1 ≤ B) + (le_refl B) (le_refl B) (le_refl B) (by simp) + exact hm.trans (by simpa only [sourceWidth, B, Nat.reduceMul, Nat.reduceAdd] using hl) + +/-- The computed source is wide enough for the two-bit signed-kernel extension. -/ +theorem sourceWidth_two_lt (n D g p total : ℕ) : 2 < sourceWidth n D g p total := by + have hc : 1 ≤ Nat.clog 2 (n + D + g + p + total + 4) := Nat.clog_pos + (by decide) (by omega) + unfold sourceWidth + omega + +/-- The computed modulus covers the original scalar sum, exponent and native coefficient. +These are original-parameter facts, independent of the physical width or any execution. -/ +theorem source_bounds (n D g p total : ℕ) : + n + D + g + p + total + 4 ≤ windowSize n D g p total ∧ + sourceWidth n D g p total < windowSize n D g p total ∧ + 6166 ≤ windowSize n D g p total := by + have hlog : Nat.clog 2 (n + D + g + p + total + 4) ≤ sourceWidth n D g p total := by + unfold sourceWidth + omega + have hsize : n + D + g + p + total + 4 ≤ windowSize n D g p total := + (Nat.le_pow_clog (by decide) _).trans (Nat.pow_le_pow_right (by decide) hlog) + have hwidth : sourceWidth n D g p total < windowSize n D g p total := Nat.lt_two_pow_self + have hc : 1 ≤ Nat.clog 2 (n + D + g + p + total + 4) := + Nat.clog_pos (by decide) (by omega) + have h6166 : 6166 ≤ sourceWidth n D g p total := by unfold sourceWidth; omega + exact ⟨hsize, hwidth, h6166.trans hwidth.le⟩ + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Program.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Program.lean new file mode 100755 index 0000000000..7b9da7fce9 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Program.lean @@ -0,0 +1,173 @@ +/- +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.CallableFixedPrime.Parameters +public import Complexity.Computability.WordRAM.CopySum +public import Complexity.Computability.WordRAM.MemoryWindow +public import Complexity.Computability.WordRAM.Power +public import Complexity.Computability.WordRAM.RegisterFrame +public import Complexity.Algorithms.WordRAM.NatClog + +/-! +# Caller-safe fixed-prime native code + +The fixed 640-register standard program protects the selector's entire low 160-register bank. +Arguments 600–607 are raw n,D,g,p, signed AB/BC/AC pointers and workspace base. They survive. +Raw verdict/witness/scans return in 632–636. Registers 160–578 embed the complete translated +416-register fixed-prime solver and its three memory-window registers. + +The adapter copies exactly the three original arrays into its workspace, accumulating their +actual raw words. It writes five original-input headers and computes its own source modulus +with native ceiling-logarithm and power loops. No caller catalogue or reserved window is +cleared or copied. The real one-time producer and all-record traversal remain unchanged. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM + +namespace Reg + +/-- Original side length. -/ +abbrev n : Fin 640 := 600 +/-- Runtime inner dimension, required to be a power of four by the correctness theorem. -/ +abbrev dimension : Fin 640 := 601 +/-- Runtime piece parameter. -/ +abbrev groups : Fin 640 := 602 +/-- Runtime fixed prime. -/ +abbrev prime : Fin 640 := 603 +/-- Canonical signed AB source pointer. -/ +abbrev ab : Fin 640 := 604 +/-- Canonical signed BC source pointer. -/ +abbrev bc : Fin 640 := 605 +/-- Canonical signed AC source pointer. -/ +abbrev ac : Fin 640 := 606 +/-- Caller-owned base of the dirty working interval. -/ +abbrev base : Fin 640 := 607 +/-- Computed raw-word sum of all three original matrices. -/ +abbrev total : Fin 640 := 608 +/-- Computed square side length. -/ +abbrev area : Fin 640 := 609 +/-- Header word count. -/ +abbrev length : Fin 640 := 611 +/-- Header store address. -/ +abbrev address : Fin 640 := 612 +/-- Constant one used for the five header stores. -/ +abbrev one : Fin 640 := 615 +/-- Header constant, finally five. -/ +abbrev constant : Fin 640 := 619 +/-- Raw zero/one original ET verdict. -/ +abbrev found : Fin 640 := 632 +/-- Original AB-row coordinate on success. -/ +abbrev witnessA : Fin 640 := 633 +/-- Original middle coordinate on success. -/ +abbrev witnessB : Fin 640 := 634 +/-- Original AC-column coordinate on success. -/ +abbrev witnessC : Fin 640 := 635 +/-- Total actual original-weight scans over all visited records. -/ +abbrev scans : Fin 640 := 636 + +end Reg + +/-- The complete solver and its compiler registers move as one bank, above the selector. -/ +@[expose] def sourceBank (i : Fin 419) : Fin 640 := ⟨160 + i.val, by omega⟩ + +/-- An unchanged source register in the high physical bank. -/ +@[expose] def sourceReg (i : Fin 416) : Fin 640 := sourceBank (i.castAdd 3) + +/-- The copy/sum loop uses eight disjoint setup registers. -/ +@[expose] def copyBank (i : Fin 8) : Fin 640 := ⟨620 + i.val, by omega⟩ + +/-- Ceiling-logarithm setup uses the first four copy temporaries. -/ +@[expose] def clogBank (i : Fin 4) : Fin 640 := ⟨620 + i.val, by omega⟩ + +/-- Power setup uses the first five copy temporaries. -/ +@[expose] def powerBank (i : Fin 5) : Fin 640 := ⟨620 + i.val, by omega⟩ + +open Reg in +/-- Write the actual original-input length and four raw scalar headers. -/ +@[expose] def header : Code .standard 640 := ram[ + one ← #1; area ← n * n; constant ← #3; length ← area * constant; + constant ← #4; length ← length + constant; address ← base; *address ← length; + address ← address + one; *address ← dimension; + address ← address + one; *address ← groups; + address ← address + one; *address ← n; + address ← address + one; *address ← prime; constant ← #5 ] + +/-- Prepare the first original matrix and initialize its actual raw-word accumulator. -/ +@[expose] def firstCopy : Code .standard 640 := + let src := copyBank 0 + let dst := copyBank 1 + let len := copyBank 2 + let total := copyBank 7 + ram[ src ← Reg.ab; dst ← Reg.base + Reg.constant; len ← Reg.area; total ← #0 ] + +/-- Advance the destination by one copied square, retaining the actual running word sum. -/ +@[expose] def nextCopy (src : Fin 640) : Code .standard 640 := + let source := copyBank 0 + let dst := copyBank 1 + let len := copyBank 2 + ram[ source ← src; dst ← dst + len ] + +/-- Only the original matrix spans are copied. Every loaded word also contributes to the +computed source-width argument; no external magnitude/exponent certificate is read. -/ +@[expose] def adapt : Code .standard 640 := + .seq header <| .seq firstCopy <| .seq (ArrayCopySum.program.rename copyBank) <| + .seq (nextCopy Reg.bc) <| .seq (ArrayCopySum.program.rename copyBank) <| + .seq (nextCopy Reg.ac) <| .seq (ArrayCopySum.program.rename copyBank) + (.op (.copy Reg.total (copyBank 7))) + +/-- Form the actual argument of the ceiling logarithm. -/ +@[expose] def sizeArgument : Code .standard 640 := + let arg := clogBank 0 + let constant := clogBank 2 + ram[ arg ← Reg.n; arg ← arg + Reg.dimension; arg ← arg + Reg.groups; + arg ← arg + Reg.prime; arg ← arg + Reg.total; constant ← #4; arg ← arg + constant ] + +/-- Deliver the computed exponent and base to the actual power routine. -/ +@[expose] def powerArguments : Code .standard 640 := + let logarithm := clogBank 1 + let coefficient := powerBank 2 + let exponent := powerBank 3 + ram[ coefficient ← #6166; exponent ← logarithm * coefficient; coefficient ← #2 ] + +/-- Deliver the computed power and runtime base to the memory-window compiler bank. -/ +@[expose] def windowArguments : Code .standard 640 := + let base := sourceBank MemoryWindow.Reg.base + let modulus := sourceBank MemoryWindow.Reg.modulus + let value := powerBank 0 + ram[ base ← Reg.base; modulus ← value ] + +/-- Compute the actual source modulus and normalize the fixed source register bank. +Neither the dirty memory window nor the caller's register bank is cleared. -/ +@[expose] def setup : Code .standard 640 := + .seq sizeArgument <| .seq (NatClog.program.rename clogBank) <| + .seq powerArguments <| .seq (Power.program.rename powerBank) <| + .seq windowArguments ((MemoryWindow.normalizeRegisters 416).rename sourceBank) + +/-- Every original solver load/store has actual runtime address translation and normalization. -/ +@[expose] def solve : Code .standard 640 := + (MemoryWindow.compile FixedPrime.program).rename sourceBank + +/-- Return raw verdict, original coordinates and the single accumulated scan counter. -/ +@[expose] def receive : Code .standard 640 := + let found := sourceReg FixedPrime.Reg.found + let a := sourceReg (FixedPrime.recordBank RecordWitness.Reg.witnessA) + let b := sourceReg (FixedPrime.recordBank RecordWitness.Reg.witnessB) + let c := sourceReg (FixedPrime.recordBank RecordWitness.Reg.witnessC) + let scans := sourceReg FixedPrime.Reg.scans + ram[ Reg.found ← found; Reg.witnessA ← a; Reg.witnessB ← b; + Reg.witnessC ← c; Reg.scans ← scans ] + +/-- One uniform callable solver; all copies, setup, invocation and return instructions are real. -/ +@[expose] def program : Code .standard 640 := .seq adapt (.seq setup (.seq solve receive)) + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Properties.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Properties.lean new file mode 100755 index 0000000000..fd9b22425f --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Properties.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.CallableFixedPrime.Program +public import Complexity.Computability.WordRAM.MemoryWindow.Normalization + +/-! +# Fixed code and selector-register frame + +The complete translated solver moves as one bank. Register framing uses its embedding, +without expanding the product or verifier instruction graph. The selector bank and the eight +original caller arguments survive every actual call. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM + +/-- The entire source bank is embedded injectively, including all compiler temporaries. -/ +theorem sourceBank_injective : Function.Injective sourceBank := by + intro i j h + have hv := congrArg Fin.val h + exact Fin.ext (by simpa only [sourceBank] using Nat.add_left_cancel hv) + +private theorem small_preserves : ∀ i : Fin 640, + i.val < 160 ∨ (600 ≤ i.val ∧ i.val < 608) → + header.Preserves i ∧ firstCopy.Preserves i ∧ + (nextCopy Reg.bc).Preserves i ∧ (nextCopy Reg.ac).Preserves i ∧ + sizeArgument.Preserves i ∧ + powerArguments.Preserves i ∧ windowArguments.Preserves i ∧ + receive.Preserves i ∧ (.op (.copy Reg.total (copyBank 7)) : Code .standard 640).Preserves i := + by decide +kernel + +/-- Both the selector's low 160 registers and the actual original call arguments are preserved +syntactically, for all executions and every physical word width. -/ +theorem program_preserves (i : Fin 640) + (hi : i.val < 160 ∨ (600 ≤ i.val ∧ i.val < 608)) : program.Preserves i := by + have src_ne (j : Fin 419) : sourceBank j ≠ i := by + intro h + have hv := congrArg Fin.val h + have hj := j.isLt + change 160 + j.val = i.val at hv + rcases hi with h | h <;> omega + have copy_ne (j : Fin 8) : copyBank j ≠ i := by + intro h + have hv := congrArg Fin.val h + change 620 + j.val = i.val at hv + rcases hi with h | h <;> omega + have clog_ne (j : Fin 4) : clogBank j ≠ i := by + intro h + have hv := congrArg Fin.val h + change 620 + j.val = i.val at hv + rcases hi with h | h <;> omega + have power_ne (j : Fin 5) : powerBank j ≠ i := by + intro h + have hv := congrArg Fin.val h + change 620 + j.val = i.val at hv + rcases hi with h | h <;> omega + obtain ⟨hh, hf, hb, ha, hs, hp, hm, hr, ht⟩ := small_preserves i hi + have hc := Code.preserves_rename_of_forall_ne ArrayCopySum.program copyBank i copy_ne + have hl := Code.preserves_rename_of_forall_ne NatClog.program clogBank i clog_ne + have hpow := Code.preserves_rename_of_forall_ne Power.program powerBank i power_ne + have hn := Code.preserves_rename_of_forall_ne (MemoryWindow.normalizeRegisters 416) + sourceBank i src_ne + have hsolve := Code.preserves_rename_of_forall_ne (MemoryWindow.compile FixedPrime.program) + sourceBank i src_ne + have hadapt : adapt.Preserves i := ⟨hh, hf, hc, hb, hc, ha, hc, ht⟩ + have hsetup : setup.Preserves i := ⟨hs, hl, hp, hpow, hm, hn⟩ + exact ⟨hadapt, hsetup, hsolve, hr⟩ + +private theorem adapt_size : adapt.size = 59 := by decide +kernel + +private theorem setup_size : setup.size = 446 := by + simp only [setup, Code.size, Code.size_rename, MemoryWindow.size_normalizeRegisters] + decide +kernel + +/-- Runtime modulus computation, translation and input adaptation never read physical width. -/ +theorem program_not_readsWidth : ¬program.ReadsWidth := by + have hc : ¬solve.ReadsWidth := by + simpa only [solve, Code.readsWidth_rename, MemoryWindow.readsWidth_compile] using + FixedPrime.program_not_readsWidth + have ha : ¬adapt.ReadsWidth := by decide +kernel + have hs : ¬setup.ReadsWidth := by + simp only [setup, Code.ReadsWidth, Code.readsWidth_rename, + MemoryWindow.normalizeRegisters_not_readsWidth, or_false] + decide +kernel + have hr : ¬receive.ReadsWidth := by decide +kernel + exact not_or.mpr ⟨ha, not_or.mpr ⟨hs, not_or.mpr ⟨hc, hr⟩⟩⟩ + +/-- One fixed standard program with 640 registers, at most 400000 slots including halt, +and no reads of the physical width. -/ +theorem program_fixed : (program.program Reg.found).length ≤ 400000 ∧ + ¬(program.program Reg.found).ReadsWidth := by + refine ⟨?_, Code.not_readsWidth_program program_not_readsWidth _⟩ + have hsource := FixedPrime.program_fixed.1 + simp only [Code.program, List.length_append, Code.length_assemble, + List.length_singleton] at hsource ⊢ + have hcompile := MemoryWindow.size_compile FixedPrime.program + simp only [program, Code.size, adapt_size, setup_size, solve, Code.size_rename] + have hreceive : receive.size = 5 := by decide +kernel + omega + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Receive.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Receive.lean new file mode 100755 index 0000000000..14f076f907 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Receive.lean @@ -0,0 +1,46 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +module +-- upstream: candidate + +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Properties + +/-! +# Actual raw verdict, witness and scan-counter return + +Five real copies return the values from the complete translated solver bank. The Boolean and +original-coordinate meaning are supplied by its proved execution, not assumed by this stage. +No answer span needs copying or normalization: the returned source registers already agree +exactly with the compiled native computation. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM + +/-- Charge all actual return copies, including coordinates in unsuccessful calls. -/ +theorem exec_receive {W : ℕ} (x : Data 640) : + ∃ y, ExecWithin W receive x y 5 ∧ y.mem = x.mem ∧ + y.regs Reg.found = x.regs (sourceReg FixedPrime.Reg.found) ∧ + y.regs Reg.witnessA = x.regs (sourceReg (FixedPrime.recordBank RecordWitness.Reg.witnessA)) ∧ + y.regs Reg.witnessB = x.regs (sourceReg (FixedPrime.recordBank RecordWitness.Reg.witnessB)) ∧ + y.regs Reg.witnessC = x.regs (sourceReg (FixedPrime.recordBank RecordWitness.Reg.witnessC)) ∧ + y.regs Reg.scans = x.regs (sourceReg FixedPrime.Reg.scans) := by + refine ⟨?y, ?run, ?mem, ?found, ?a, ?b, ?c, ?scans⟩ + case run => ram_eval [receive, sourceReg, sourceBank, FixedPrime.recordBank, + FixedPrime.Reg.found, FixedPrime.Reg.scans, RecordWitness.Reg.witnessA, + RecordWitness.Reg.witnessB, RecordWitness.Reg.witnessC, + Reg.found, Reg.witnessA, Reg.witnessB, Reg.witnessC, Reg.scans, Fin.mk.injEq] + case mem => rfl + all_goals simp +decide [sourceReg, sourceBank, FixedPrime.recordBank, + Reg.found, Reg.witnessA, Reg.witnessB, Reg.witnessC, Reg.scans, + FixedPrime.Reg.found, FixedPrime.Reg.scans, RecordWitness.Reg.witnessA, + RecordWitness.Reg.witnessB, RecordWitness.Reg.witnessC] + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Setup.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Setup.lean new file mode 100755 index 0000000000..42708fe90d --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Setup.lean @@ -0,0 +1,201 @@ +/- +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.CallableFixedPrime.Properties + +/-! +# Computed modulus and normalized source bank + +The native setup executes the ceiling logarithm and power loops on the actual copied-word +sum. It normalizes only the fixed source register bank. Every memory word, original argument +and selector register is preserved; no clean window or precomputed modulus is supplied. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM + +/-- The explicit physical margin covers the source width, scalar-size sum and power setup. -/ +theorem setup_fits {W b n D g p total : ℕ} + (hfit : Fits W (b + 4 * windowSize n D g p total + 1024)) : + sourceWidth n D g p total ≤ W ∧ + n + D + g + p + total + 4 ≤ windowSize n D g p total ∧ + sourceWidth n D g p total < windowSize n D g p total ∧ + 6166 ≤ windowSize n D g p total := by + obtain ⟨hsize, hwidth, h6166⟩ := source_bounds n D g p total + refine ⟨?_, hsize, hwidth, h6166⟩ + by_contra h + have hW : W ≤ sourceWidth n D g p total := by omega + have he := Nat.pow_le_pow_right (by decide : 1 ≤ (2 : ℕ)) hW + unfold Fits windowSize at hfit + omega + +private theorem clogBank_injective : Function.Injective clogBank := by + intro i j h + have hv := congrArg Fin.val h + exact Fin.ext (by simpa only [clogBank] using Nat.add_left_cancel hv) + +private theorem powerBank_injective : Function.Injective powerBank := by + intro i j h + have hv := congrArg Fin.val h + exact Fin.ext (by simpa only [powerBank] using Nat.add_left_cancel hv) + +/-- Actual computed setup at every admitted physical width. Register normalization is charged +and source fits are postconditions of that code, not final caller assumptions. -/ +theorem exec_setup {W : ℕ} (x : Data 640) + (hfit : Fits W (x.regs Reg.base + + 4 * windowSize (x.regs Reg.n) (x.regs Reg.dimension) (x.regs Reg.groups) + (x.regs Reg.prime) (x.regs Reg.total) + 1024)) : + let n := x.regs Reg.n + let D := x.regs Reg.dimension + let g := x.regs Reg.groups + let p := x.regs Reg.prime + let total := x.regs Reg.total + ∃ y, ExecWithin W setup x y + (24669 * Nat.clog 2 (n + D + g + p + total + 4) + 439) ∧ + y.mem = x.mem ∧ + y.regs (sourceBank MemoryWindow.Reg.base) = x.regs Reg.base ∧ + y.regs (sourceBank MemoryWindow.Reg.modulus) = windowSize n D g p total ∧ + (∀ i : Fin 416, Fits (sourceWidth n D g p total) (y.regs (sourceReg i))) ∧ + ∀ j : Fin 640, j.val < 160 ∨ (600 ≤ j.val ∧ j.val < 608) → y.regs j = x.regs j := by + let n := x.regs Reg.n + let D := x.regs Reg.dimension + let g := x.regs Reg.groups + let p := x.regs Reg.prime + let total := x.regs Reg.total + let b := x.regs Reg.base + let S := n + D + g + p + total + 4 + have fit : Fits W (b + 4 * windowSize n D g p total + 1024) := hfit + obtain ⟨hw, hS, hwidth, h6166⟩ := setup_fits fit + have h2 : Fits W 2 := fit.of_le (by omega) + have h4 : Fits W 4 := fit.of_le (by omega) + have hc : Fits W 6166 := fit.of_le (by omega) + have hsize : Fits W S := fit.of_le (by omega) + have hsize' : Fits W (S + 1) := fit.of_le (by omega) + have hlog : Nat.clog 2 S ≤ sourceWidth n D g p total := by dsimp only [sourceWidth, S]; omega + have hlog' : Fits W (Nat.clog 2 S + 1) := fit.of_le (by omega) + have hexp : Fits W (Nat.clog 2 S * 6166) := fit.of_le (by + have he : Nat.clog 2 S * 6166 = sourceWidth n D g p total := by + dsimp only [sourceWidth, S] + omega + rw [he] + omega) + have hpfit : Fits W (2 ^ sourceWidth n D g p total + sourceWidth n D g p total + 2) := + fit.of_le (by change windowSize n D g p total + _ + 2 ≤ _; omega) + have hND : Fits W (n + D) := hsize.of_le (by dsimp only [S]; omega) + have hNDg : Fits W (n + D + g) := hsize.of_le (by dsimp only [S]; omega) + have hNDgp : Fits W (n + D + g + p) := hsize.of_le (by dsimp only [S]; omega) + have hNDgpt : Fits W (n + D + g + p + total) := hsize.of_le (by dsimp only [S]; omega) + obtain ⟨s, hs, sval, smem, sbase⟩ : + ∃ s, ExecWithin W sizeArgument x s 7 ∧ s.regs (clogBank 0) = S ∧ + s.mem = x.mem ∧ s.regs Reg.base = b := by + refine ⟨?s, ?run, ?value, ?mem, ?base⟩ + case run => ram_eval [sizeArgument, clogBank, n, D, g, p, total, S, h4, hND, hNDg, + hNDgp, hNDgpt, hsize, Reg.n, Reg.dimension, Reg.groups, Reg.prime, Reg.total, + Fin.mk.injEq] + case value => simp +decide [S, n, D, g, p, total, clogBank] + case mem => rfl + case base => simp +decide [b, Reg.base] + obtain ⟨l, hl, lval, lmem, -, -⟩ := NatClog.exec_rename clogBank clogBank_injective s h2 + (by change Fits W (s.regs (clogBank 0) + 1); rw [sval]; exact hsize') + (by change Fits W (Nat.clog 2 (s.regs (clogBank 0)) + 1); rw [sval]; exact hlog') + have hl' : ExecWithin W (NatClog.program.rename clogBank) s l + (5 * Nat.clog 2 S + 5) := by simpa only [sval] using hl + have lc : l.regs (clogBank 1) = Nat.clog 2 S := by simpa only [sval] using lval + have lb : l.regs Reg.base = b := (hl.regs_eq (by + apply Code.preserves_rename_of_forall_ne + intro i he + have hv := congrArg Fin.val he + change 620 + i.val = 607 at hv + omega)).trans sbase + let a := ((l.set (powerBank 2) 6166).set (powerBank 3) + (Nat.clog 2 S * 6166)).set (powerBank 2) 2 + have ha : ExecWithin W powerArguments l a 3 := by + let a₁ := l.set (powerBank 2) 6166 + have hconst : ExecWithin (B := .standard) W + (.op (.const (powerBank 2) 6166)) l a₁ 1 := ExecWithin.const hc + have hv₁ : a₁.regs (clogBank 1) = Nat.clog 2 S := by + simpa [a₁, powerBank, clogBank] using lc + have hc₁ : a₁.regs (powerBank 2) = 6166 := + Function.update_self (powerBank 2) 6166 l.regs + have hmul : ExecWithin W + (.op (.bin .mul (powerBank 3) (clogBank 1) (powerBank 2))) a₁ + (a₁.set (powerBank 3) (Nat.clog 2 S * 6166)) 1 := by + simpa only [BinOp.eval, hv₁, hc₁] using + (ExecWithin.bin (w := W) (f := .mul) (d := powerBank 3) + (i := clogBank 1) (j := powerBank 2) (x := a₁) + (by simpa only [BinOp.eval, hv₁, hc₁] using hexp)) + exact hconst.seq (hmul.seq (ExecWithin.const h2)) + have ab : a.regs Reg.base = b := by + simpa [a, powerBank, Reg.base, Function.update_apply] using lb + obtain ⟨v, hv, vv, -, -, vm, -, -⟩ := Power.exec (w := W) 2 + (sourceWidth n D g p total) (by decide) (a.comap powerBank) + (by simp [a, powerBank, Power.base]) + (by simp [a, powerBank, Power.exponent, sourceWidth, S, Nat.mul_comm]) hpfit + let z := v.extend powerBank a + have hz : ExecWithin W (Power.program.rename powerBank) a z + (4 * sourceWidth n D g p total + 5) := hv.rename powerBank_injective + have zv : z.regs (powerBank 0) = windowSize n D g p total := + (powerBank_injective.extend_apply _ _ _).trans vv + have zb : z.regs Reg.base = b := (hz.regs_eq (by + apply Code.preserves_rename_of_forall_ne + intro i he + have hval := congrArg Fin.val he + change 620 + i.val = 607 at hval + omega)).trans ab + let c := (z.set (sourceBank MemoryWindow.Reg.base) b).set + (sourceBank MemoryWindow.Reg.modulus) (windowSize n D g p total) + have hc' : ExecWithin W windowArguments z c 2 := by + have hbase : ExecWithin (B := .standard) W + (.op (.copy (sourceBank MemoryWindow.Reg.base) Reg.base)) z + (z.set (sourceBank MemoryWindow.Reg.base) b) 1 := by + simpa only [zb] using + (ExecWithin.copy (B := .standard) (w := W) (x := z) + (d := sourceBank MemoryWindow.Reg.base) (s := Reg.base)) + have hvalue : (z.set (sourceBank MemoryWindow.Reg.base) b).regs (powerBank 0) = + windowSize n D g p total := by + rw [Data.set_regs, Function.update_of_ne (by decide)] + exact zv + have hmodulus : ExecWithin (B := .standard) W + (.op (.copy (sourceBank MemoryWindow.Reg.modulus) (powerBank 0))) + (z.set (sourceBank MemoryWindow.Reg.base) b) c 1 := by + simpa only [hvalue] using + (ExecWithin.copy (B := .standard) (w := W) + (x := z.set (sourceBank MemoryWindow.Reg.base) b) + (d := sourceBank MemoryWindow.Reg.modulus) (s := powerBank 0)) + exact hbase.seq hmodulus + have cb : c.regs (sourceBank MemoryWindow.Reg.base) = b := by + simp +decide [c, sourceBank, MemoryWindow.Reg.base, MemoryWindow.Reg.modulus] + have cM : c.regs (sourceBank MemoryWindow.Reg.modulus) = windowSize n D g p total := by + simp [c] + obtain ⟨v', hv', v'mem, v'match, v'bound, -⟩ := MemoryWindow.exec_normalizeRegisters + (w := sourceWidth n D g p total) (W := W) (b := b) (c.comap sourceBank) cb cM hw + let y := v'.extend sourceBank c + have hy : ExecWithin W ((MemoryWindow.normalizeRegisters 416).rename sourceBank) c y 417 := + hv'.rename sourceBank_injective + have he : ExecWithin W setup x y (24669 * Nat.clog 2 S + 439) := by + apply (hs.seq (hl'.seq (ha.seq (hz.seq (hc'.seq hy))))).mono + dsimp only [sourceWidth, S] + exact le_of_eq (by ring) + refine ⟨y, he, ?_, ?_, ?_, ?_, ?_⟩ + · exact v'mem.trans (vm.trans (lmem.trans smem)) + · exact (sourceBank_injective.extend_apply _ _ _).trans v'match.base_eq + · exact (sourceBank_injective.extend_apply _ _ _).trans v'match.modulus_eq + · intro i + change Fits (sourceWidth n D g p total) (y.regs (sourceBank (i.castAdd 3))) + rw [show y.regs (sourceBank (i.castAdd 3)) = v'.regs (i.castAdd 3) from + sourceBank_injective.extend_apply _ _ _] + exact v'bound.1 i + · intro j hj + obtain ⟨-, hj', -, -⟩ := program_preserves j hj + exact he.regs_eq hj' + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Source.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Source.lean new file mode 100755 index 0000000000..fd4f0774ba --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Source.lean @@ -0,0 +1,158 @@ +/- +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.FixedPrime + +/-! +# Complete fixed-prime execution with dirty source memory + +The unchanged producer runs on arbitrary old registers and dirty remaining memory. Its actual +prepared prefix supplies the all-record controller. A proof-only reference state frames that +prefix against the canonical original input; it does not assert a zero external frame for the +real computation. Neither the reference state nor its readback is an algorithm input. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle +open Cslib.Algorithms.MatrixMultiplication.Schonhage +open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage + +/-- Actual complete source execution from only the original input prefix. Old registers and +all remaining memory may be dirty. The reference prepared state is derived from the executed +producer, rather than supplied as a layout, run, answer or time certificate. -/ +theorem exec_source {w m n g p A : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hD : 16 ≤ D m) + (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D m)) (hN : D m ^ 18 ≤ n) + (hv : ∀ z ∈ values, z.natAbs ≤ A) + (hW : FixedPrime.admissionWidth n (D m) g p A ≤ w + 2) + (initial : Data 416) + (hinput : ∀ q < 5 + 3 * (n * n), initial.mem q = + (Data.init (PreparationInput.input n (D m) g p values) : Data 64).mem q) : + let V := fun q => values.getD q 0 + let wAB := fun u v : Fin n => V (pairIndex (u, v)) + let wBC := fun b c : Fin n => V (n * n + pairIndex (b, c)) + let wAC := fun u c : Fin n => V (2 * (n * n) + pairIndex (u, c)) + 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, + Instances.Output n (D m) g p V + (.init (PreparationInput.input n (D m) g p values)) a ∧ + ∃ y, ExecWithin (w + 2) FixedPrime.program initial y + (FixedPrime.timeBound (m := m) hn g p values a.mem) ∧ + (y.regs FixedPrime.Reg.found = 0 ∨ y.regs FixedPrime.Reg.found = 1) ∧ + y.regs FixedPrime.Reg.scans ≤ falsePositiveCount wAB wBC wAC p + + y.regs FixedPrime.Reg.found ∧ + (y.regs FixedPrime.Reg.found = 1 ↔ HasZeroTriangle wAB wBC wAC) ∧ + (y.regs FixedPrime.Reg.found = 1 → + y.regs (FixedPrime.recordBank RecordWitness.Reg.witnessA) < n ∧ + y.regs (FixedPrime.recordBank RecordWitness.Reg.witnessB) < n ∧ + y.regs (FixedPrime.recordBank RecordWitness.Reg.witnessC) < n ∧ + V (y.regs (FixedPrime.recordBank RecordWitness.Reg.witnessA) * n + + y.regs (FixedPrime.recordBank RecordWitness.Reg.witnessB)) + + V (n * n + (y.regs (FixedPrime.recordBank RecordWitness.Reg.witnessB) * n + + y.regs (FixedPrime.recordBank RecordWitness.Reg.witnessC))) + + V (2 * (n * n) + (y.regs (FixedPrime.recordBank RecordWitness.Reg.witnessA) * n + + y.regs (FixedPrime.recordBank RecordWitness.Reg.witnessC))) = 0) ∧ + ∀ q, q < 5 + 3 * (n * n) ∨ + a.regs Instances.heap + CallableProduct.windowSize n (n * n) ≤ q → + y.mem q = initial.mem q := by + let V := fun q => values.getD q 0 + let canonical : Data 64 := .init (PreparationInput.input n (D m) g p values) + have hDn : D m ≤ n := (Nat.le_self_pow (by decide : 18 ≠ 0) (D m)).trans hN + have hp0 := (Nat.mem_sqrtPrimeWindow_iff_sq.mp hp).1.pos + have hw : PreparationInput.width n (D m) g p A ≤ w + 2 := by + have hr := FixedPrime.record_admitted hW + unfold RecordWitness.admissionWidth RecordProduct.admissionWidth at hr + omega + have header (q : ℕ) (hq : q < 5 + 3 * (n * n)) : initial.mem q = canonical.mem q := + hinput q hq + have hf : Function.Injective RecordProduct.producerBank := by + intro i j h + exact Fin.ext (congrArg (fun k : Fin 320 => k.val) h) + have hf' : Function.Injective RecordWitness.productBank := by + intro i j h + exact Fin.ext (congrArg (fun k : Fin 400 => k.val) h) + have hf'' : Function.Injective FixedPrime.recordBank := by + intro i j h + exact Fin.ext (congrArg (fun k : Fin 416 => k.val) h) + let c₀ := initial.comap FixedPrime.recordBank + let b₀ := c₀.comap RecordWitness.productBank + let a₀ := b₀.comap RecordProduct.producerBank + obtain ⟨a, ha, hout⟩ := PreparationInput.exec_at values hlen a₀ + (by change initial.mem 1 = D m + simpa [canonical, PreparationInput.input, Data.init] using header 1 (by omega)) + (by change initial.mem 2 = g + simpa [canonical, PreparationInput.input, Data.init] using header 2 (by omega)) + (by change initial.mem 3 = n + simpa [canonical, PreparationInput.input, Data.init] using header 3 (by omega)) + (by change initial.mem 4 = p + simpa [canonical, PreparationInput.input, Data.init] using header 4 (by omega)) + (fun q hq => (header (5 + q) (by omega)).trans + (PreparationInput.input_word n (D m) g p values q)) + (by omega) hDn hg hp0 hv hw + have hend := hout.inputEnd_le_heap + have haframe (q : ℕ) (hq : q < 5 + 3 * (n * n) ∨ a.regs Instances.heap ≤ q) : + a.mem q = initial.mem q := by + obtain ⟨-, -, -, -, -, hh, -, -, -, -, -, hframe⟩ := hout + exact hframe q (by simpa only [hh] using hq) + let reference : Data 64 := ⟨a.regs, + fun q => if q < a.regs Instances.heap then a.mem q else canonical.mem q⟩ + have reference_mem (q : ℕ) (hq : q < a.regs Instances.heap) : reference.mem q = a.mem q := + ite_eq_left hq + have reference_out : Instances.Output n (D m) g p V canonical reference := + hout.transfer V rfl (fun q hq => reference_mem q hq) (by + intro q hq + change (if q < a.regs Instances.heap then a.mem q else canonical.mem q) = canonical.mem q + by_cases h : q < a.regs Instances.heap + · rw [ite_eq_left h] + have hin : q < 5 + 3 * (n * n) := by + change _ ∨ a.regs Instances.heap ≤ q at hq + omega + exact (haframe q (Or.inl hin)).trans (header q hin) + · rw [ite_eq_right h]) + have heap : reference.regs Instances.heap ≤ PreparationInput.wordBound n (D m) g p A := by + have hh := hout.heap_le_budget V (by omega) hDn hg + change a.regs Instances.heap ≤ _ + unfold PreparationInput.wordBound PreparationInput.envelope + omega + let b := a.extend RecordProduct.producerBank b₀ + have hb : ExecWithin (w + 2) RecordProduct.produce b₀ b + (RecordProduct.preparationTime n (D m) g p values - 1) := ha.rename hf + let c := b.extend RecordWitness.productBank c₀ + have hc : ExecWithin (w + 2) RecordWitness.produce c₀ c + (RecordProduct.preparationTime n (D m) g p values - 1) := hb.rename hf' + let x := c.extend FixedPrime.recordBank initial + have hx : ExecWithin (w + 2) FixedPrime.produce initial x + (RecordProduct.preparationTime n (D m) g p values - 1) := hc.rename hf'' + have bank (j : Fin 64) : x.regs + (FixedPrime.recordBank (RecordWitness.productBank (RecordProduct.producerBank j))) = + reference.regs j := + (hf''.extend_apply _ _ _).trans ((hf'.extend_apply _ _ _).trans (hf.extend_apply _ _ _)) + have hmem : Set.EqOn x.mem reference.mem (Set.Iio (reference.regs Instances.heap)) := by + intro q hq + exact (reference_mem q hq).symm + obtain ⟨y, hy, yf, ys, yiff, yw, frame, -⟩ := FixedPrime.exec_traverse values hlen + hD hg hp hN hv hW reference x reference_out bank hmem heap + refine ⟨reference, reference_out, y, (hx.seq hy).mono ?_, yf, ys, yiff, yw, ?_⟩ + · dsimp only [FixedPrime.timeBound, V] + omega + · intro q hq + have houtside : q < reference.regs Instances.heap ∨ + reference.regs Instances.heap + CallableProduct.windowSize n (n * n) ≤ q := + hq.elim (fun h => Or.inl (h.trans_le hend)) Or.inr + apply (frame q houtside).trans + apply haframe q + change q < 5 + 3 * (n * n) ∨ + a.regs Instances.heap + CallableProduct.windowSize n (n * n) ≤ q at hq + omega + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/TimeBound.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/TimeBound.lean new file mode 100755 index 0000000000..f88486a452 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/TimeBound.lean @@ -0,0 +1,56 @@ +/- +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.CallableFixedPrime.Exec + +/-! +# Aggregate callable fixed-prime charge + +The memory-window compiler multiplies the actual complete source charge by at most three. +Only the original input adaptation and computed-modulus/return overhead are added. The source +producer and all-product saving remain explicit, as does the single global false-positive +reserve. This does not choose parameters or prove the final ExactTriangle/3SUM exponent. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle +open Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- Halt-inclusive complete caller bound. It includes all copies, setup, source instructions, +recursion, index/dispatch, normalization, return copies and exactly one final halt. The old +source's own halt-inclusive bound is retained conservatively inside the factor-three term. -/ +theorem timeBound_le {m n g p : ℕ} (hn : 0 < n) (values : List ℤ) (mem : ℕ → ℕ) + (hD : 16 ≤ D m) (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D m)) (hN : D m ^ 18 ≤ n) : + let V := fun q => values.getD q 0 + let F := falsePositiveCount (fun u v : Fin n => V (pairIndex (u, v))) + (fun u v => V (n * n + pairIndex (u, v))) + (fun u v => V (2 * (n * n) + pairIndex (u, v))) p + ((timeBound (m := m) hn g p values mem + 1 : ℕ) : ℝ) ≤ + 24 * (n : ℝ) ^ 2 + + 24669 * (Nat.clog 2 (n + D m + g + p + rawTotal n values + 4) : ℕ) + 483 + + 3 * (690 * (n : ℝ) ^ 2 * D m * g + + 138412032 * ((19 * m + 1 : ℕ) : ℝ) * (n : ℝ) ^ 3 * g / + (D m : ℝ) ^ (1 / 18 : ℝ) + + (4 * (n : ℝ) * g) * + ((5 * Nat.sqrt (D m) + 8 * queryCap n (D m) + 61 : ℕ) : ℝ) + + (((42 * pieceSize (D m) g + 28) * (F + 1) + 7 : ℕ) : ℝ)) := by + have h := mul_le_mul_of_nonneg_left + (FixedPrime.timeBound_le hn values mem hD hg hp hN) (by norm_num : (0 : ℝ) ≤ 3) + calc + _ = 24 * (n : ℝ) ^ 2 + + 24669 * (Nat.clog 2 (n + D m + g + p + rawTotal n values + 4) : ℕ) + 483 + + 3 * (FixedPrime.timeBound (m := m) hn g p values mem : ℝ) := by + simp only [timeBound, Nat.cast_add, Nat.cast_mul, Nat.cast_ofNat, pow_two] + ring + _ ≤ _ := add_le_add (le_refl _) h + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Program.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Program.lean index 062e519445..5f931f0fa5 100644 --- a/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Program.lean +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/FixedPrime/Program.lean @@ -83,6 +83,16 @@ open Reg in /-- Complete original-input fixed-prime solver: one preparation and the actual native loop. -/ @[expose] def program : Code .standard 416 := .seq produce traverse +/-- The complete structured solver never reads the physical word width. This form is used +by actual memory-window compilation as well as by the flat initialized client. -/ +theorem program_not_readsWidth : ¬program.ReadsWidth := by + simp only [program, produce, traverse, setup, step, select, record, receive, + RecordWitness.produce, RecordProduct.produce, RecordWitness.program, + Code.ReadsWidth, Code.readsWidth_rename, Op.ReadsWidth, Op.bin, reduceCtorEq, + false_or, or_false] + exact not_or.mpr ⟨Instances.program_fixed.2, + not_or.mpr ⟨RecordProduct.program_fixed.2, RecordWitness.consume_fixed.2⟩⟩ + /-- The whole fixed-prime controller is one standard-native program, with a fixed register bank and at most 133152 flat slots including halt. It never reads the physical word width. -/ theorem program_fixed : (program.program Reg.found).length ≤ 133152 ∧ @@ -96,12 +106,6 @@ theorem program_fixed : (program.program Reg.found).length ≤ 133152 ∧ have hr := RecordProduct.program_fixed.1 have hc := RecordWitness.consume_fixed.1 omega - · apply Code.not_readsWidth_program - simp only [program, produce, traverse, setup, step, select, record, receive, - RecordWitness.produce, RecordProduct.produce, RecordWitness.program, - Code.ReadsWidth, Code.readsWidth_rename, Op.ReadsWidth, Op.bin, reduceCtorEq, - false_or, or_false] - exact not_or.mpr ⟨Instances.program_fixed.2, - not_or.mpr ⟨RecordProduct.program_fixed.2, RecordWitness.consume_fixed.2⟩⟩ + · exact Code.not_readsWidth_program program_not_readsWidth _ end Cslib.Algorithms.WordRAM.ExactTriangle.FixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationInput.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationInput.lean index f126a6eb98..92a263379b 100644 --- a/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationInput.lean +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationInput.lean @@ -194,7 +194,9 @@ private theorem fits_at_width (n D g p A : ℕ) : · simp only [Nat.add_sub_cancel] exact_mod_cast hmag -private theorem input_fits {n D g p A : ℕ} (values : List ℤ) +/-- Original scalar headers and canonical signed words fit at the derived preparation width. +Caller-side memory-window translations reuse this bound before normalizing their source view. -/ +theorem input_fits {n D g p A : ℕ} (values : List ℤ) (hlen : values.length = 3 * (n * n)) (hv : ∀ z ∈ values, z.natAbs ≤ A) : InputFits (width n D g p A) (input n D g p values) := by obtain ⟨hmag, hbudget⟩ := fits_at_width n D g p A @@ -214,20 +216,21 @@ 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) -/-- 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)) +/-- Execute preparation from actual scalar headers and original signed array words, with +arbitrary old registers and dirty remaining memory. Admission is derived from original +parameters using the same proof as the initialized client. No intermediate fit is supplied. -/ +theorem exec_at {n D g p A W : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (initial : Data 64) + (hDHeader : initial.mem 1 = D) (hgHeader : initial.mem 2 = g) + (hnHeader : initial.mem 3 = n) (hpHeader : initial.mem 4 = p) + (hinput : ∀ q < 3 * (n * n), initial.mem (5 + q) = Signed.encode (values.getD q 0)) (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, ExecWithin W Instances.program (.init (input n D g p values)) y + ∃ y, ExecWithin W Instances.program initial 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 + Instances.Output n D g p (fun q => values.getD q 0) initial y := by obtain ⟨hmag, hbudget⟩ := fits_at_width n D g p A have hmod : GenericRAM.Signed.Fits (Nat.clog 2 (envelope n D g p A) + 1) (p : ℤ) := hmag.of_natAbs_le (by simp only [Int.natAbs_natCast]; omega) @@ -239,12 +242,29 @@ theorem exec_input {n D g p A W : ℕ} (values : List ℤ) exact List.getElem_mem hq' exact hmag.of_natAbs_le ((hv _ hmem).trans (by omega : A ≤ A + p + 1)) obtain ⟨y, hy, hout⟩ := Instances.exec_at n D g p (fun q => values.getD q 0) - (.init (input n D g p values)) rfl rfl rfl rfl (fun q _ => input_word n D g p values q) + initial hDHeader hgHeader hnHeader hpHeader hinput hD hDn hg hp hmod hvalues hbudget have hew := ExecWithin.mono_width Instances.program_fixed.2 hy hw + exact ⟨y, hew, hout⟩ + +/-- 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, 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 + obtain ⟨y, hew, hout⟩ := exec_at values hlen (.init (input n D g p values)) + rfl rfl rfl rfl (fun q _ => input_word n D g p values q) hD hDn hg hp hv hw have hi := (input_fits values hlen hv).mono hw - have hybounded := hew.bounded (Data.Bounded.init hi) - exact ⟨y, hew, hout, hi, hybounded⟩ + exact ⟨y, hew, hout, hi, hew.bounded (Data.Bounded.init hi)⟩ /-- 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. -/ diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationLocality.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationLocality.lean index 8b1b5611b5..b97c3d26b9 100644 --- a/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationLocality.lean +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationLocality.lean @@ -111,4 +111,52 @@ theorem Output.reframe {n D g p : ℕ} (values : ℕ → ℤ) {initial y z : Dat rw [mem_eq _ (by have hj : j.val < n * D := j.isLt; omega)] exact hright j +/-- Transport prepared readback to a protected-prefix-equivalent state with its own explicit +external frame. The prefix premise covers only genuine prepared words; the external frame +is relative to the chosen initial state, and no new execution is asserted. -/ +theorem Output.transfer {n D g p : ℕ} (values : ℕ → ℤ) {initial y initial' z : Data 64} + (h : Output n D g p values initial y) (hregs : z.regs = y.regs) + (hmem : Set.EqOn z.mem y.mem (Set.Iio (y.regs heap))) + (hframe : ∀ q, q < 5 + 3 * (n * n) ∨ z.regs heap ≤ q → z.mem q = initial'.mem q) : + Output n D g p values initial' z := by + obtain ⟨hn, hD, hp, ho, hc, hh, hr, hcounts, hqueries, hdesc, hblocks, -⟩ := + h.reframe values hregs hmem + exact ⟨hn, hD, hp, ho, hc, hh, hr, hcounts, hqueries, hdesc, hblocks, + by simpa only [hh] using hframe⟩ + +/-- Original headers and signed matrices precede every prepared record and its workspace. -/ +theorem Output.inputEnd_le_heap {n D g p : ℕ} {values : ℕ → ℤ} {initial y : Data 64} + (h : Output n D g p values initial y) : 5 + 3 * (n * n) ≤ y.regs heap := by + obtain ⟨-, -, -, -, -, hh, -⟩ := h + dsimp only at hh + omega + +/-- The computed heap fits the original preparation budget, independently of old registers +or dirty memory outside the original arrays. -/ +theorem Output.heap_le_budget {n D g p : ℕ} (values : ℕ → ℤ) {initial y : Data 64} + (h : Output n D g p values initial y) (hD : 1 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) : + y.regs heap ≤ budget n D g p := by + let C := fun rho => Nat.count (fun q => (values q % (p : ℤ)).toNat = rho) (n * n) + let K := ChunkCatalogue.before C (queryCap n D) p + let H := numPieces n D g + have hK : K ≤ p * (n * n) := ChunkCatalogue.before_le + (one_le_queryCap hD hDn) (fun _ _ => Nat.count_le _) le_rfl + have hB : 0 < pieceSize D g := by + have hs : 0 < sOf D := Nat.sqrt_pos.mpr hD + have hc := Nat.le_ceilDiv_mul (a := sOf D) (by omega : 0 < g) + change sOf D ≤ pieceSize D g * g at hc + by_contra hz + have : pieceSize D g = 0 := by omega + rw [this, Nat.zero_mul] at hc + omega + have hH : H ≤ n := (Nat.ceilDiv_le_iff hB).mpr + (Nat.le_mul_of_pos_right n hB) + have hKH := Nat.mul_le_mul hK hH + have hprod := Nat.mul_le_mul_right (6 + 2 * (n * D)) hKH + obtain ⟨-, -, -, -, -, hh, -⟩ := h + change y.regs heap = 5 + 6 * (n * n) + p + 2 * (n * n) * p + 3 * K + + (K * H) * (6 + 2 * (n * D)) at hh + dsimp only [budget] + omega + end Cslib.Algorithms.WordRAM.ExactTriangle.Instances diff --git a/Complexity/Computability/WordRAM/CopySum.lean b/Complexity/Computability/WordRAM/CopySum.lean new file mode 100755 index 0000000000..d3a0b23e26 --- /dev/null +++ b/Complexity/Computability/WordRAM/CopySum.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 +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.WordRAM.Copy +public import Mathlib.Algebra.Order.BigOperators.Group.Finset + +/-! +# Copying an array while accumulating its original words + +The fixed eight-register program performs the same forward stores as `ArrayCopy.program`, +with one additional addition per word. The running sum can carry across successive arrays. +Its sum is computed by the program, rather than supplied as an input magnitude certificate. +All memory outside the destination remains unchanged, including dirty caller memory. +-/ + +public section + +namespace Cslib.WordRAM.ArrayCopySum + +namespace Reg + +/-- Source pointer. -/ +abbrev src : Fin 8 := 0 +/-- Destination pointer. -/ +abbrev dst : Fin 8 := 1 +/-- Number of words. -/ +abbrev len : Fin 8 := 2 +/-- Current offset. -/ +abbrev idx : Fin 8 := 3 +/-- Address temporary. -/ +abbrev addr : Fin 8 := 4 +/-- Loaded original word. -/ +abbrev value : Fin 8 := 5 +/-- Constant one. -/ +abbrev one : Fin 8 := 6 +/-- Accumulator, supplied and returned in the same register. -/ +abbrev total : Fin 8 := 7 + +end Reg + +open Reg + +/-- The mathematical sum of the original source span. -/ +@[expose] def wordSum (mem : ℕ → ℕ) (base length : ℕ) : ℕ := + ∑ j ∈ Finset.range length, mem (base + j) + +/-- One actual copy and accumulation, including both address computations. -/ +@[expose] def body : Code .standard 8 := ram[ + addr ← src + idx; value ← *addr; addr ← dst + idx; *addr ← value; + total ← total + value; idx ← idx + one ] + +/-- Copy and sum a runtime span, retaining the old accumulator for zero-length spans. -/ +@[expose] def program : Code .standard 8 := + ram[ idx ← #0; one ← #1; while idx < len do [ ⟪body⟫ ] ] + +/-- Copy a separated source span and accumulate its original words. Every loop test, load, +store and sum is charged; only actual source/destination and total-sum numerical fits are +premises. This does not require a clean destination. -/ +theorem exec {w : ℕ} (x : Data 8) (h1 : Fits w 1) + (hs : Fits w (x.regs src + x.regs len)) + (hd : Fits w (x.regs dst + x.regs len)) + (ht : Fits w (x.regs total + wordSum x.mem (x.regs src) (x.regs len))) + (hsep : x.regs src + x.regs len ≤ x.regs dst) : + ∃ y, ExecWithin w program x y (8 * x.regs len + 4) ∧ + y.mem = ArrayCopy.copyPrefix x.mem (x.regs src) (x.regs dst) (x.regs len) ∧ + y.regs src = x.regs src ∧ y.regs dst = x.regs dst ∧ y.regs len = x.regs len ∧ + y.regs total = x.regs total + wordSum x.mem (x.regs src) (x.regs len) := by + let I (y : Data 8) : Prop := + y.regs src = x.regs src ∧ y.regs dst = x.regs dst ∧ y.regs len = x.regs len ∧ + y.regs one = 1 ∧ y.regs idx ≤ x.regs len ∧ + y.mem = ArrayCopy.copyPrefix x.mem (x.regs src) (x.regs dst) (y.regs idx) ∧ + y.regs total = x.regs total + wordSum x.mem (x.regs src) (y.regs idx) + have hbody (y : Data 8) (hy : I y) (hc : (Cond.lt idx len).Holds y) : + ∃ z, ExecWithin w body y z 6 ∧ I z ∧ + x.regs len - z.regs idx < x.regs len - y.regs idx := by + obtain ⟨hys, hyd, hyl, hyo, hyi, hym, hyt⟩ := hy + have hi : y.regs idx < x.regs len := by simpa only [Cond.holds_lt, hyl] using hc + have hsrc : Fits w (y.regs src + y.regs idx) := by + rw [hys]; exact hs.of_le (by omega) + have hdst : Fits w (y.regs dst + y.regs idx) := by + rw [hyd]; exact hd.of_le (by omega) + have hinc : Fits w (y.regs idx + 1) := hs.of_le (by omega) + have hread : y.mem (y.regs src + y.regs idx) = x.mem (x.regs src + y.regs idx) := by + rw [hym, hys] + exact ArrayCopy.copyPrefix_outside (by omega) + have hsum : Fits w (y.regs total + y.mem (y.regs src + y.regs idx)) := by + rw [hyt, hread] + have hle : wordSum x.mem (x.regs src) (y.regs idx + 1) ≤ + wordSum x.mem (x.regs src) (x.regs len) := + Finset.sum_le_sum_of_subset_of_nonneg (Finset.range_mono (by omega)) + (fun _ _ _ => Nat.zero_le _) + apply ht.of_le + simpa only [wordSum, Finset.sum_range_succ, Nat.add_assoc] using + Nat.add_le_add_left hle (x.regs total) + refine ⟨?z, ?run, ?inv, ?decrease⟩ + case run => ram_eval [body, hsrc, hdst, hinc, hsum, hyo] + case inv => + refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ + · simpa +decide [Function.update_apply] using hys + · simpa +decide [Function.update_apply] using hyd + · simpa +decide [Function.update_apply] using hyl + · simpa +decide [Function.update_apply] using hyo + · simpa [hyo] using Nat.succ_le_of_lt hi + · simp only [Data.set_mem, Data.write_mem, Data.set_regs, Function.update_apply] + rw [hread, hym, hyd, ← ArrayCopy.copyPrefix_succ] + rfl + · simp only [Data.set_regs, Function.update_apply] + simp only [show (total : Fin 8) ≠ idx by decide, ↓reduceIte] + rw [hyt, hread] + simp only [wordSum, Finset.sum_range_succ, Nat.add_assoc] + case decrease => simp only [Data.set_regs, Function.update_self]; omega + let x₀ := (x.set idx 0).set one 1 + have hx₀ : I x₀ := by simp +decide [I, x₀, wordSum] + obtain ⟨y, he, hy, hc⟩ := ExecWithin.loop_invariant I + (fun y => x.regs len - y.regs idx) hbody hx₀ + obtain ⟨hys, hyd, hyl, hyo, hyi, hym, hyt⟩ := hy + have hend : y.regs idx = x.regs len := by + simp only [Cond.holds_lt, hyl] at hc + omega + refine ⟨y, ?_, by simpa only [hend] using hym, hys, hyd, hyl, + by simpa only [hend] using hyt⟩ + have hinit := (ExecWithin.const (d := idx) (x := x) (fits_zero w)).seq + ((ExecWithin.const (d := one) h1).seq he) + convert hinit using 1 + · rfl + · simp +decide only [x₀, Data.set_regs, Function.update_apply, ↓reduceIte, Nat.sub_zero] + omega + +end Cslib.WordRAM.ArrayCopySum diff --git a/Complexity/Computability/WordRAM/MemoryWindow/Normalization.lean b/Complexity/Computability/WordRAM/MemoryWindow/Normalization.lean new file mode 100755 index 0000000000..65d24275c9 --- /dev/null +++ b/Complexity/Computability/WordRAM/MemoryWindow/Normalization.lean @@ -0,0 +1,47 @@ +/- +Copyright (c) 2026 Erik Demaine. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Erik Demaine +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.WordRAM.MemoryWindow + +/-! +# Static properties of memory-window register normalization + +The normalizer has exactly one remainder per source register and one closing self-copy. +These properties let callers account for a whole fixed register bank without unfolding the +finite register enumeration, and preserve width-independent execution. +-/ + +public section + +namespace Cslib.WordRAM.MemoryWindow + +private theorem size_normalizeBankList {r : ℕ} (is : List (Fin r)) : + (normalizeBankList is).size = is.length + 1 := by + induction is with + | nil => rfl + | cons i is ih => simp only [normalizeBankList, Code.size, List.length_cons, ih]; omega + +/-- The fixed register normalizer uses one real operation per source register, plus one. -/ +theorem size_normalizeRegisters (r : ℕ) : (normalizeRegisters r).size = r + 1 := by + simpa only [normalizeRegisters, List.length_finRange] using + size_normalizeBankList (List.finRange r) + +private theorem normalizeBankList_not_readsWidth {r : ℕ} (is : List (Fin r)) : + ¬(normalizeBankList is).ReadsWidth := by + induction is with + | nil => simp [normalizeBankList, Code.ReadsWidth, Op.ReadsWidth] + | cons i is ih => + simpa only [normalizeBankList, Code.ReadsWidth, Op.ReadsWidth, Op.bin, + reduceCtorEq, false_or] using ih + +/-- Register normalization uses the runtime modulus and never reads the physical width. -/ +theorem normalizeRegisters_not_readsWidth (r : ℕ) : ¬(normalizeRegisters r).ReadsWidth := + normalizeBankList_not_readsWidth _ + +end Cslib.WordRAM.MemoryWindow diff --git a/ComplexityTests/WordRAMCallableFixedPrime.lean b/ComplexityTests/WordRAMCallableFixedPrime.lean new file mode 100755 index 0000000000..30d2054048 --- /dev/null +++ b/ComplexityTests/WordRAMCallableFixedPrime.lean @@ -0,0 +1,58 @@ +/- +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.CallableFixedPrime.Program + +/-! +# Actual caller adaptation regressions + +These small interpreter runs test the copies, accumulated raw-word sum, scalar headers and +the protected low register bank. Their small dimensions do not satisfy the full thin solver's +geometry, and no complete solver execution at those dimensions is claimed. +-/ + +set_option linter.hashCommand false + +namespace ComplexityTests.WordRAMCallableFixedPrime + +open Cslib.WordRAM +open Cslib.Algorithms.WordRAM.ExactTriangle + +private def copyInput : Data 8 := + ⟨![1, 10, 3, 99, 99, 99, 99, 5], fun q => + if q = 1 then 5 else if q = 2 then 2 else if q = 3 then 8 else 99⟩ + +-- Signed encodings of -2, 1, 4 are copied unchanged and added to the old accumulator five. +example : ∃ y, ExecWithin 8 ArrayCopySum.program copyInput y 28 ∧ + y.regs ArrayCopySum.Reg.total = 20 ∧ y.mem 10 = 5 ∧ y.mem 11 = 2 ∧ y.mem 12 = 8 ∧ + y.mem 1 = 5 ∧ y.mem 9 = 99 ∧ y.mem 13 = 99 := by + refine ⟨?y, ?run, ?values⟩ + case run => + apply ExecWithin.of_eval (fuel := 3) (n := 28) + · rfl + · decide + case values => decide +kernel + +example : Fits 5 20 ∧ ¬Fits 4 20 := by decide +kernel + +private def caller : Data 640 := + { regs := fun j => + if j.val = 600 then 1 else if j.val = 601 then 16 else if j.val = 602 then 1 + else if j.val = 603 then 3 else if j.val = 604 then 1 else if j.val = 605 then 2 + else if j.val = 606 then 3 else if j.val = 607 then 16 else 777 + mem := copyInput.mem } + +private def adapted : Option (List ℕ × ℕ) := + (CallableFixedPrime.adapt.eval 16 4 caller).map fun (y, t) => + ([y.mem 16, y.mem 17, y.mem 18, y.mem 19, y.mem 20, y.mem 21, y.mem 22, y.mem 23, + y.regs CallableFixedPrime.Reg.total, y.regs 0, y.regs 159, y.regs 600, + y.mem 1, y.mem 15, y.mem 24], t) + +#guard adapted == some ([7, 16, 1, 1, 3, 5, 2, 8, 15, 777, 777, 1, 5, 99, 99], 62) + +end ComplexityTests.WordRAMCallableFixedPrime From 69495f23b6325d2ff629e92f73edda03de1316c7 Mon Sep 17 00:00:00 2001 From: Erik Demaine Date: Sun, 1 Nov 2026 01:01:08 -0400 Subject: [PATCH 2/4] feat(ExactTriangle): complete callable fixed-prime execution and bounds Source-ready checkpoint for #2125 on pinned main bc2e6c2599e53b7ea8b2b8088fbc15cdc02e17bc. Complete fixed640 standard Code caller and initialized entry: real original-array copies/sum, native ceiling-log/power/modulus/normalization, actual complete one-time producer and all-record solver, original signed witness verification, raw Boolean/witness/global scans. Caller preserves low160 and arguments600..607, with outside-window/source frame and dirty scratch. Actual initialized same-y prefix and halt prove positive and negative ET iff, and global S<=F(p)+actualFlag. No run/layout/list/witness/solver/time oracle. New Width/Prefix/SourceBounds prove original-parameter positive admission, raw dirty words before reduction, every-wide-width native prefixes and independent-W polynomial words/new-support. Separate caller placement/raw-word exponent is explicit. Initialized log-width coefficient24664*(kappa+9)+19 and polynomial prefix exponent24664*(kappa+9)+20. Actual caller cost24n^2+24669*clog2(n+D+g+p+T+4)+482+3*oldSourceTime pre-halt, T actual raw copied sum. Initialized header14 and halt1 are charged. Complete source aggregate terms retained, including one global false-positive reserve; parameter/prime choice, uniform selected-prime performance and full1394/1.9992 remain OPEN. Targeted Lean MCP clean: new umbrella and all source through its imports; three owned test modules WordRAMCallableFixedPrime, WordRAMCallableFixedPrimeInput, WordRAMCallableFixedPrimeCaller; existing WordRAMExactTriangleFixedPrimeInput client. Tests include fully admitted initialized +/- valid thin geometry, complete actual dirty caller with aliased inputs/nonzero low160, and small native signed/header/return/frame/cost regressions. Earlier source files checked serially; bootstrap was warm. No local all-six, canonical aggregate generation or final hygiene/name/static audit claimed: root retains that slot, required fresh whole-layer review/publication still pending. Original source checkpoint37de retained. Own new-file executable modes corrected to0644; no unrelated checkout/cache/process/source change. Public producer exec_at/input_fits and Output transfer/heap lemmas reuse original private admission/locality proofs; old initialized statements and existing native program bodies retained. FixedPrime noReads property extracted once and reused. Generic ArrayCopySum/MemoryWindow normalization API additions have concrete clients. Abstract catalogue/rendering unaffected; no headline promotion. AI assistance: OpenAI Codex; existing mathematical/source credit retained. --- .../ExactTriangle/CallableFixedPrime.lean | 47 ++++++ .../CallableFixedPrime/Adapt.lean | 0 .../CallableFixedPrime/Admission.lean | 0 .../CallableFixedPrime/Copy.lean | 0 .../CallableFixedPrime/Core.lean | 0 .../CallableFixedPrime/Exec.lean | 0 .../CallableFixedPrime/Flat.lean | 135 ++++++++++++++++ .../CallableFixedPrime/Header.lean | 0 .../CallableFixedPrime/Input.lean | 8 + .../CallableFixedPrime/InputSpec.lean | 0 .../CallableFixedPrime/Parameters.lean | 0 .../CallableFixedPrime/Prefix.lean | 106 +++++++++++++ .../CallableFixedPrime/Program.lean | 0 .../CallableFixedPrime/Properties.lean | 0 .../CallableFixedPrime/Receive.lean | 0 .../CallableFixedPrime/Setup.lean | 0 .../CallableFixedPrime/Source.lean | 0 .../CallableFixedPrime/SourceBounds.lean | 73 +++++++++ .../CallableFixedPrime/TimeBound.lean | 0 .../CallableFixedPrime/Width.lean | 150 ++++++++++++++++++ .../ExactTriangle/PreparationInput.lean | 3 +- Complexity/Computability/WordRAM/CopySum.lean | 0 .../WordRAM/MemoryWindow/Normalization.lean | 0 .../WordRAMCallableFixedPrime.lean | 25 ++- .../WordRAMCallableFixedPrimeCaller.lean | 146 +++++++++++++++++ .../WordRAMCallableFixedPrimeInput.lean | 148 +++++++++++++++++ 26 files changed, 839 insertions(+), 2 deletions(-) create mode 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime.lean mode change 100755 => 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Adapt.lean mode change 100755 => 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Admission.lean mode change 100755 => 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Copy.lean mode change 100755 => 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Core.lean mode change 100755 => 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Exec.lean create mode 100755 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Flat.lean mode change 100755 => 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Header.lean mode change 100755 => 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Input.lean mode change 100755 => 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/InputSpec.lean mode change 100755 => 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Parameters.lean create mode 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Prefix.lean mode change 100755 => 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Program.lean mode change 100755 => 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Properties.lean mode change 100755 => 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Receive.lean mode change 100755 => 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Setup.lean mode change 100755 => 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Source.lean create mode 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/SourceBounds.lean mode change 100755 => 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/TimeBound.lean create mode 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Width.lean mode change 100755 => 100644 Complexity/Computability/WordRAM/CopySum.lean mode change 100755 => 100644 Complexity/Computability/WordRAM/MemoryWindow/Normalization.lean mode change 100755 => 100644 ComplexityTests/WordRAMCallableFixedPrime.lean create mode 100644 ComplexityTests/WordRAMCallableFixedPrimeCaller.lean create mode 100644 ComplexityTests/WordRAMCallableFixedPrimeInput.lean diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime.lean new file mode 100644 index 0000000000..ef7b06340d --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime.lean @@ -0,0 +1,47 @@ +/- +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.CallableFixedPrime.SourceBounds +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.TimeBound + +/-! +# Caller-safe complete fixed-prime ExactTriangle solver + +The fixed 640-register standard program consumes runtime n,D,g,p, canonical-signed original +matrix pointers and a dirty workspace base. It preserves the selector's entire low 160-register +bank, its argument bank and original memory outside its computed working interval. It copies +only the original three arrays, computes its own virtual word modulus, and invokes the actual +one-time producer and all-record product/witness controller through the memory-window compiler. +No catalogue, layout, solver, witness, execution or time certificate is an algorithm input. + +## Main definitions + +* `CallableFixedPrime.program`: caller code; arguments 600–607, raw verdict/witness/scans 632–636. +* `CallableFixedPrime.entryProgram`: initialized original-input header delivery and caller code. +* `CallableFixedPrime.admissionWidth`: original-caller threshold including raw dirty words + before remainder instructions. + +## Main results + +* `CallableFixedPrime.exec`: complete caller execution, exact original positive/negative decision, + witness coordinates, caller frames and the single global scan bound S ≤ F(p) + returnedFlag. +* `CallableFixedPrime.runs_input`: actual initialized same-state prefix and charged halt. +* `CallableFixedPrime.timeBound_le`: aggregate charged source work plus real adaptation overhead. +* `CallableFixedPrime.bounded_reachable_caller`: width-independent word/support envelope from + original caller words, including arbitrary original outside memory. +* `CallableFixedPrime.inputWidth_le_log`, `CallableFixedPrime.prefixBound_le_pow`: positive + logarithmic initialized admission and polynomial envelope for every wider native prefix. + +Correctness requires D=4^m ≥16, g≥1, p in the stated prime window and n≥D^18. Width bounds also +state original scalar, weight, placement and raw-word hypotheses explicitly. The initialized +clients use the original producer input encoding. The wrapper/compiler work is original; +underlying finite source identities and the concrete source solver retain their own credit. +Global parameter/prime choice, the outer ordinary-input host and the complete subquadratic 3SUM +bound remain separate. This module is not a complete solution to that broader objective. +-/ diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Adapt.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Adapt.lean old mode 100755 new mode 100644 diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Admission.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Admission.lean old mode 100755 new mode 100644 diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Copy.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Copy.lean old mode 100755 new mode 100644 diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Core.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Core.lean old mode 100755 new mode 100644 diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Exec.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Exec.lean old mode 100755 new mode 100644 diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Flat.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Flat.lean new file mode 100755 index 0000000000..28ccd87b79 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Flat.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 +-/ + +module +-- upstream: candidate + +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Input + +/-! +# Initialized halting caller-safe fixed-prime computation + +The same final state witnesses the actual initialized prefix, halt, verdict, original +coordinates and global failed-scan accounting. Fourteen real header/pointer instructions +precede the complete caller program, and the final halt is charged. This remains a fixed-prime +component with explicit thin geometry, not parameter/prime selection or the 3SUM endpoint. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle +open Cslib.Algorithms.MatrixMultiplication.Schonhage + +private theorem pow_sourceWidth_add_two (n D g p T : ℕ) : + 2 ^ (sourceWidth n D g p T + 2) = 4 * windowSize n D g p T := by + simp [windowSize, pow_add, Nat.mul_comm] + +private theorem input_low_admission {m n g p : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) : + InputFits (sourceWidth n (D m) g p (rawTotal n values) + 2) + (PreparationInput.input n (D m) g p values) ∧ + Fits (sourceWidth n (D m) g p (rawTotal n values) + 2) + (n + D m + g + p + 5 + 3 * (n * n) + 1024) := by + have hi := input_fits_source (m := m) (g := g) (p := p) values hlen + (natAbs_le_rawTotal values hlen) + have hI := inputEnd_le_window (m := m) (g := g) (p := p) values hlen + obtain ⟨hS, -, hc⟩ := source_bounds n (D m) g p (rawTotal n values) + refine ⟨hi.mono (by omega), ?_⟩ + change _ < 2 ^ (sourceWidth n (D m) g p (rawTotal n values) + 2) + rw [pow_sourceWidth_add_two] + omega + +/-- Fully initialized same-state prefix and halt. The width guarantee also establishes original +input fit; no producer state, prepared catalogue, layout, solver or run law is an input. -/ +theorem runs_input {W m n g p : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hD : 16 ≤ D m) + (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D m)) (hN : D m ^ 18 ≤ n) + (hW : inputWidth n (D m) g p values ≤ W) : + let V := fun q => values.getD q 0 + let wAB := fun u v : Fin n => V (pairIndex (u, v)) + let wBC := fun u v : Fin n => V (n * n + pairIndex (u, v)) + let wAC := fun u v : Fin n => V (2 * (n * n) + pairIndex (u, v)) + 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) + InputFits W (PreparationInput.input n (D m) g p values) ∧ + ∃ a : Data 64, + Instances.Output n (D m) g p V + (.init (PreparationInput.input n (D m) g p values)) a ∧ + ∃ y t, t + 1 ≤ timeBound (m := m) hn g p values a.mem + 15 ∧ + Runs W (entryProgram.program Reg.found) + (State.init (PreparationInput.input n (D m) g p values)) ⟨entryProgram.size, y⟩ t ∧ + Executes W (entryProgram.program Reg.found) + (State.init (PreparationInput.input n (D m) g p values)) (y.regs Reg.found) (t + 1) ∧ + y.Bounded W ∧ (y.regs Reg.found = 0 ∨ y.regs Reg.found = 1) ∧ + y.regs Reg.scans ≤ falsePositiveCount wAB wBC wAC p + y.regs Reg.found ∧ + (y.regs Reg.found = 1 ↔ HasZeroTriangle wAB wBC wAC) ∧ + (y.regs Reg.found = 1 → ∃ u v c : Fin n, + y.regs Reg.witnessA = u.val ∧ y.regs Reg.witnessB = v.val ∧ + y.regs Reg.witnessC = c.val ∧ weightSum wAB wBC wAC u v c = 0) ∧ + (∀ q, q < workspaceBase n ∨ + workspaceBase n + windowSize n (D m) g p (rawTotal n values) ≤ q → + y.mem q = (Data.init (PreparationInput.input n (D m) g p values) : Data 640).mem q) ∧ + ∀ j : Fin 640, j.val < 160 → y.regs j = 0 := by + let T := rawTotal n values + let M := windowSize n (D m) g p T + let b := workspaceBase n + let w₀ := sourceWidth n (D m) g p T + 2 + have fit : Fits W (b + 4 * M + 4 * M + 1024) := admission_fits hW + have hw₀ : w₀ ≤ W := by + have h4M : Fits W (4 * M) := fit.of_le (by omega) + change 4 * M < 2 ^ W at h4M + have hpw : 2 ^ w₀ = 4 * M := pow_sourceWidth_add_two n (D m) g p T + by_contra h + have hpow := Nat.pow_le_pow_right (by decide : 1 ≤ (2 : ℕ)) (by omega : W ≤ w₀) + rw [hpw] at hpow + omega + obtain ⟨hi₀, hinitfit⟩ := input_low_admission (m := m) (g := g) (p := p) values hlen + obtain ⟨x, hinit, xmem, xn, xD, xg, xp, xab, xbc, xac, xb⟩ := exec_entryHeader values hinitfit + have hi : InputFits W (PreparationInput.input n (D m) g p values) := hi₀.mono hw₀ + have hx₀ : x.Bounded w₀ := hinit.bounded (Data.Bounded.init hi₀) + have hx : x.Bounded W := ⟨fun i => (hx₀.1 i).mono hw₀, fun q => (hx₀.2 q).mono hw₀⟩ + have hinitial : ExecWithin W entryHeader + (.init (PreparationInput.input n (D m) g p values)) x 14 := + ExecWithin.mono_width entryHeader_fixed.2 hinit hw₀ + have vab (q : ℕ) (hq : q < n * n) : + x.mem (x.regs Reg.ab + q) = Signed.encode (values.getD q 0) := by + rw [xab, xmem] + exact PreparationInput.input_word n (D m) g p values q + have vbc (q : ℕ) (hq : q < n * n) : + x.mem (x.regs Reg.bc + q) = Signed.encode (values.getD (n * n + q) 0) := by + rw [xbc, xmem] + simpa only [Data.init, Nat.add_assoc] using + PreparationInput.input_word n (D m) g p values (n * n + q) + have vac (q : ℕ) (hq : q < n * n) : x.mem (x.regs Reg.ac + q) = + Signed.encode (values.getD (2 * (n * n) + q) 0) := by + rw [xac, xmem] + simpa only [Data.init, two_mul, Nat.add_assoc] using + PreparationInput.input_word n (D m) g p values (2 * (n * n) + q) + obtain ⟨a, hout, y, hy, ybound, yf, ys, yiff, yw, yframe, -⟩ := exec values hlen hD hg hp hN + x xn xD xg xp xb (by rw [xab]; dsimp only [workspaceBase]; omega) + (by rw [xbc]; dsimp only [workspaceBase]; omega) + (by rw [xac]; dsimp only [workspaceBase]; omega) vab vbc vac hx + (fit.of_le (by dsimp only [b, M, T] at *; omega)) + have he : ExecWithin W entryProgram + (.init (PreparationInput.input n (D m) g p values)) y + (14 + timeBound (m := m) _ g p values a.mem) := hinitial.seq hy + obtain ⟨t, ht, hex⟩ := he + refine ⟨hi, a, hout, y, t, ?_, ?_, ?_, ybound, yf, ys, yiff, ?_, ?_, ?_⟩ + · exact (Nat.add_le_add_right ht 1).trans_eq (by ring) + · simpa only [Nat.zero_add, State.init] using hex.runs (pc := 0) + (p := entryProgram.program Reg.found) (Program.Contains.self _).append_left + · simpa only [State.init] using hex.executes Reg.found + · intro hf + obtain ⟨ha, hb, hc, hz⟩ := yw hf + exact ⟨⟨_, ha⟩, ⟨_, hb⟩, ⟨_, hc⟩, rfl, rfl, rfl, hz⟩ + · intro q hq + exact (yframe q hq).trans (congrFun xmem q) + · intro j hj + exact hex.regs_eq (entryProgram_preserves_selector j hj) + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Header.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Header.lean old mode 100755 new mode 100644 diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Input.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Input.lean old mode 100755 new mode 100644 index 7892f4f1fc..7e0b2bdb2d --- a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Input.lean +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Input.lean @@ -62,6 +62,14 @@ theorem entryProgram_fixed : (entryProgram.program Reg.found).length ≤ 400014 List.length_singleton, entryProgram, Code.size, entryHeader_fixed.1] at h ⊢ omega +private theorem entryHeader_selector_frame : ∀ j : Fin 640, j.val < 160 → + entryHeader.Preserves j := by decide +kernel + +/-- Original-input header delivery also retains the selector/parameter bank. -/ +theorem entryProgram_preserves_selector (j : Fin 640) (hj : j.val < 160) : + entryProgram.Preserves j := + ⟨entryHeader_selector_frame j hj, program_preserves j (Or.inl hj)⟩ + /-- The real initialized setup provides actual runtime pointers and preserves every original memory cell. Its only numerical premise concerns the original scalar/address arithmetic. -/ theorem exec_entryHeader {W n D g p : ℕ} (values : List ℤ) diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/InputSpec.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/InputSpec.lean old mode 100755 new mode 100644 diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Parameters.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Parameters.lean old mode 100755 new mode 100644 diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Prefix.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Prefix.lean new file mode 100644 index 0000000000..facad79bed --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Prefix.lean @@ -0,0 +1,106 @@ +/- +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.CallableFixedPrime.Flat +public import Complexity.Computability.WordRAM.Width + +/-! +# Physical-width-independent prefixes of the caller-safe fixed-prime program + +The actual minimum-width solver execution controls every prefix at every larger admitted width. +The initial raw dirty-word bound P applies before any remainder instruction. It is a hypothesis +about the original caller data, not a supplied execution certificate or an algorithm argument. +New address support is bounded independently of physical width; original outside memory is kept. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM +open Cslib.Algorithms.MatrixMultiplication.Schonhage + +/-- Original raw words fit at every admitted width, including dirty loads before reduction. -/ +theorem original_bounded {W n d g p T b P : ℕ} (x : Data 640) + (hregs : ∀ i, x.regs i ≤ P) (hmem : ∀ q, x.mem q ≤ P) + (hW : admissionWidth n d g p T b P ≤ W) : x.Bounded W := by + have fit : Fits W P := (admission_fits hW).of_le (by omega) + exact ⟨fun i => fit.of_le (hregs i), fun q => fit.of_le (hmem q)⟩ + +/-- Every actual caller prefix has an original-input envelope. The complete concrete solver +supplies the comparison run; no run, layout, witness or resource certificate is a premise. -/ +theorem bounded_reachable_caller {W m n g p b P k : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hD : 16 ≤ D m) + (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D m)) (hN : D m ^ 18 ≤ n) + (x : Data 640) (xn : x.regs Reg.n = n) (xD : x.regs Reg.dimension = D m) + (xg : x.regs Reg.groups = g) (xp : x.regs Reg.prime = p) (xb : x.regs Reg.base = b) + (hab : x.regs Reg.ab + n * n ≤ b) (hbc : x.regs Reg.bc + n * n ≤ b) + (hac : x.regs Reg.ac + n * n ≤ b) + (vab : ∀ q < n * n, x.mem (x.regs Reg.ab + q) = Signed.encode (values.getD q 0)) + (vbc : ∀ q < n * n, x.mem (x.regs Reg.bc + q) = Signed.encode (values.getD (n * n + q) 0)) + (vac : ∀ q < n * n, x.mem (x.regs Reg.ac + q) = + Signed.encode (values.getD (2 * (n * n) + q) 0)) + (hregs : ∀ i, x.regs i ≤ P) (hmem : ∀ q, x.mem q ≤ P) + (hW : admissionWidth n (D m) g p (rawTotal n values) b P ≤ W) + {s : State 640} (hr : Runs W (program.program Reg.found) ⟨0, x⟩ s k) : + (∀ i, s.data.regs i < wordBound n (D m) g p (rawTotal n values) b P) ∧ + (∀ q, s.data.mem q < wordBound n (D m) g p (rawTotal n values) b P) ∧ + ∀ q, wordBound n (D m) g p (rawTotal n values) b P ≤ q → s.data.mem q = x.mem q := by + let w := admissionWidth n (D m) g p (rawTotal n values) b P + have hx : x.Bounded w := original_bounded x hregs hmem le_rfl + have fit : Fits w (b + 4 * windowSize n (D m) g p (rawTotal n values) + 1024) := + (admission_fits (le_refl w)).of_le (by omega) + obtain ⟨a, hout, y, he, -⟩ := exec values hlen hD hg hp hN + x xn xD xg xp xb hab hbc hac vab vbc vac hx fit + obtain ⟨t, ht, hex⟩ := he + have hlow := Runs.prefix_at_smaller_width program_fixed.2 hW hr + (hex.executes Reg.found) + have hs := hlow.bounded hx + have hpow := pow_admissionWidth_le n (D m) g p (rawTotal n values) b P + refine ⟨fun i => (hs.1 i).trans_le hpow, fun q => (hs.2 q).trans_le hpow, ?_⟩ + exact fun q hq => hlow.mem_above hx (hpow.trans hq) + +/-- Numerical envelope for initialized prefix words and newly written addresses. -/ +@[expose] def prefixBound (n d g p : ℕ) (values : List ℤ) : ℕ := + wordBound n d g p (rawTotal n values) (workspaceBase n) (inputWordBound n d g p values) + +/-- Initialized execution, including every reused dirty workspace prefix, has finite support +independent of physical width. The concrete minimum-width run supplies the comparison. -/ +theorem bounded_reachable_input {W m n g p k : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hD : 16 ≤ D m) + (hg : 1 ≤ g) (hp : p ∈ Nat.sqrtPrimeWindow (D m)) (hN : D m ^ 18 ≤ n) + (hW : inputWidth n (D m) g p values ≤ W) + {s : State 640} (hr : Runs W (entryProgram.program Reg.found) + (State.init (PreparationInput.input n (D m) g p values)) s k) : + (∀ i, s.data.regs i < prefixBound n (D m) g p values) ∧ + (∀ q, s.data.mem q < prefixBound n (D m) g p values) ∧ + ∀ q, prefixBound n (D m) g p values ≤ q → s.data.mem q = 0 := by + obtain ⟨hi, a, hout, y, t, ht, hpref, he, -⟩ := + runs_input values hlen hD hg hp hN le_rfl + have hlow := Runs.prefix_at_smaller_width entryProgram_fixed.2 hW hr he + have hx := Data.Bounded.init (r := 640) hi + have hs := hlow.bounded hx + have hpow := pow_admissionWidth_le n (D m) g p (rawTotal n values) (workspaceBase n) + (inputWordBound n (D m) g p values) + refine ⟨fun i => (hs.1 i).trans_le hpow, fun q => (hs.2 q).trans_le hpow, ?_⟩ + intro q hq + have hq' : 2 ^ inputWidth n (D m) g p values ≤ q := hpow.trans hq + rw [hlow.mem_above hx hq'] + cases q with + | zero => + have := Nat.two_pow_pos (inputWidth n (D m) g p values) + omega + | succ q => + change (PreparationInput.input n (D m) g p values).getD q 0 = 0 + apply List.getD_eq_default + have hlen := hi.1 + dsimp only [Fits] at hlen + omega + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Program.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Program.lean old mode 100755 new mode 100644 diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Properties.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Properties.lean old mode 100755 new mode 100644 diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Receive.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Receive.lean old mode 100755 new mode 100644 diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Setup.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Setup.lean old mode 100755 new mode 100644 diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Source.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Source.lean old mode 100755 new mode 100644 diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/SourceBounds.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/SourceBounds.lean new file mode 100644 index 0000000000..e08ab59bc4 --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/SourceBounds.lean @@ -0,0 +1,73 @@ +/- +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.CallableFixedPrime.Prefix +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Width + +/-! +# Initialized logarithmic admission and polynomial prefix support + +The explicit positive logarithmic constant depends only on the original weight exponent. +Every wider native prefix has the same polynomial numerical/support envelope. These coarse +bounds cover the real computed modulus; the program does not allocate by clearing this envelope. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +private theorem input_placement {n d g p A κ : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hv : ∀ z ∈ values, z.natAbs ≤ A) + (hd : d ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) : + workspaceBase n ≤ (n + 2) ^ (12332 * (κ + 9) + 5) ∧ + inputWordBound n d g p values ≤ (n + 2) ^ (12332 * (κ + 9) + 5) := by + let B := n + 2 + have hb : 2 ≤ B := by dsimp only [B]; omega + have hb1 : 1 ≤ B := by omega + have hn : n ≤ B := by dsimp only [B]; omega + have hn2 : n * n ≤ B ^ 2 := (Nat.mul_le_mul hn hn).trans_eq (by ring) + have h2 : 1 ≤ B ^ 2 := Nat.one_le_pow _ _ hb1 + have h8 : 8 ≤ B ^ 3 := + (by decide : 8 ≤ (2 : ℕ) ^ 3).trans (Nat.pow_le_pow_left hb 3) + have hbase : workspaceBase n ≤ B ^ 5 := by + calc + _ ≤ 8 * B ^ 2 := by dsimp only [workspaceBase]; omega + _ ≤ B ^ 3 * B ^ 2 := Nat.mul_le_mul_right _ h8 + _ = _ := by ring + refine ⟨hbase.trans (Nat.pow_le_pow_right hb1 (by omega)), ?_⟩ + have hM := windowSize_le_pow values hlen hv hd hg hp hA + have h4 : 4 ≤ B ^ 2 := (by decide : 4 ≤ (2 : ℕ) ^ 2).trans (Nat.pow_le_pow_left hb 2) + calc + _ ≤ B ^ 2 * B ^ (12332 * (κ + 9)) := Nat.mul_le_mul h4 hM + _ = B ^ (12332 * (κ + 9) + 2) := by rw [← pow_add, Nat.add_comm] + _ ≤ _ := Nat.pow_le_pow_right hb1 (by omega) + +/-- All physical widths beyond a positive constant times log(n+2) admit the actual initialized +program. No weight exponent or width certificate is passed to the program. -/ +theorem inputWidth_le_log {n d g p A κ : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hv : ∀ z ∈ values, z.natAbs ≤ A) + (hd : d ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) : + inputWidth n d g p values ≤ + (24664 * (κ + 9) + 19) * Nat.clog 2 (n + 2) := by + obtain ⟨hb, hP⟩ := input_placement values hlen hv hd hg hp hA + have h := admissionWidth_le_log values hlen hv hd hg hp hA hb hP + simpa only [inputWidth, show 12332 * (κ + 9) + (12332 * (κ + 9) + 5) + 14 = + 24664 * (κ + 9) + 19 by omega] using h + +/-- Polynomial bound on the width-independent envelope that controls every initialized prefix. -/ +theorem prefixBound_le_pow {n d g p A κ : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hv : ∀ z ∈ values, z.natAbs ≤ A) + (hd : d ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) : + prefixBound n d g p values ≤ (n + 2) ^ (24664 * (κ + 9) + 20) := by + obtain ⟨hb, hP⟩ := input_placement values hlen hv hd hg hp hA + have h := wordBound_le_pow values hlen hv hd hg hp hA hb hP + simpa only [prefixBound, show 12332 * (κ + 9) + (12332 * (κ + 9) + 5) + 15 = + 24664 * (κ + 9) + 20 by omega] using h + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/TimeBound.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/TimeBound.lean old mode 100755 new mode 100644 diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Width.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Width.lean new file mode 100644 index 0000000000..1fd585005a --- /dev/null +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Width.lean @@ -0,0 +1,150 @@ +/- +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.CallableFixedPrime.Input +import Complexity.Foundations.Data.Nat.Log + +/-! +# Original-input logarithmic width of the callable solver + +The computed raw-word sum has a polynomial bound from the original integer weights. Consequently +both the computed virtual modulus and the physical admission have bounds independent of the +physical width. The caller's original placement and raw dirty-word exponent is explicit and may +be different from its integer-weight exponent. These are resource bounds, not algorithm inputs. +-/ + +public section + +namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime + +open Cslib.WordRAM + +private theorem scalarSum_le_pow {n d g p A κ : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hv : ∀ z ∈ values, z.natAbs ≤ A) + (hd : d ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) : + n + d + g + p + rawTotal n values + 4 ≤ (n + 2) ^ (κ + 9) := by + let B := n + 2 + have hb : 2 ≤ B := by dsimp only [B]; omega + have hb1 : 1 ≤ B := by omega + have hnB : n ≤ B := by dsimp only [B]; omega + have h3 : 3 ≤ B ^ 2 := (by decide : 3 ≤ (2 : ℕ) ^ 2).trans (Nat.pow_le_pow_left hb 2) + have hA' : A ≤ B ^ κ := hA + have hκ : 1 ≤ B ^ κ := Nat.one_le_pow _ _ hb1 + have ha : 2 * A + 1 ≤ B ^ (κ + 2) := by + calc + _ ≤ 3 * B ^ κ := by omega + _ ≤ B ^ 2 * B ^ κ := Nat.mul_le_mul_right _ h3 + _ = _ := by ring + have hn2 : n * n ≤ B ^ 2 := (Nat.mul_le_mul hnB hnB).trans_eq (by ring) + have ht : rawTotal n values ≤ B ^ (κ + 6) := by + calc + _ ≤ 3 * (n * n) * (2 * A + 1) := rawTotal_le values hlen hv + _ ≤ B ^ 2 * B ^ 2 * B ^ (κ + 2) := + Nat.mul_le_mul (Nat.mul_le_mul h3 hn2) ha + _ = _ := by ring + have hnE : n ≤ B ^ (κ + 6) := hnB.trans (Nat.le_self_pow (by omega) B) + have h4 : 4 ≤ B ^ (κ + 6) := + (by decide : 4 ≤ (2 : ℕ) ^ 6).trans ((Nat.pow_le_pow_left hb 6).trans + (Nat.pow_le_pow_right hb1 (by omega))) + calc + _ ≤ 6 * B ^ (κ + 6) := by omega + _ ≤ B ^ 3 * B ^ (κ + 6) := Nat.mul_le_mul_right _ + ((by decide : 6 ≤ (2 : ℕ) ^ 3).trans (Nat.pow_le_pow_left hb 3)) + _ = _ := by ring + +/-- Width actually computed by the program, from polynomial original weights and scalar headers. -/ +theorem sourceWidth_le_log {n d g p A κ : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hv : ∀ z ∈ values, z.natAbs ≤ A) + (hd : d ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) : + sourceWidth n d g p (rawTotal n values) ≤ + (6166 * (κ + 9)) * Nat.clog 2 (n + 2) := by + have he := scalarSum_le_pow values hlen hv hd hg hp hA + have he' := he.trans (Nat.pow_le_pow_left + (Nat.le_pow_clog (by decide : 1 < (2 : ℕ)) (n + 2)) (κ + 9)) + rw [← Nat.pow_mul] at he' + have hl := Nat.clog_le_of_le_pow he' + unfold sourceWidth + nlinarith only [hl] + +/-- The real runtime reservation is polynomial, without any physical-width parameter. -/ +theorem windowSize_le_pow {n d g p A κ : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hv : ∀ z ∈ values, z.natAbs ≤ A) + (hd : d ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) : + windowSize n d g p (rawTotal n values) ≤ (n + 2) ^ (12332 * (κ + 9)) := by + have hb : 2 ≤ n + 2 := by omega + have hbase : 2 ^ Nat.clog 2 (n + 2) ≤ (n + 2) ^ 2 := + (Nat.pow_clog_le_mul (by decide : 1 < (2 : ℕ)) (by omega : n + 2 ≠ 0)).trans + (by nlinarith only [hb]) + calc + _ ≤ 2 ^ ((6166 * (κ + 9)) * Nat.clog 2 (n + 2)) := + Nat.pow_le_pow_right (by decide) (sourceWidth_le_log values hlen hv hd hg hp hA) + _ = (2 ^ Nat.clog 2 (n + 2)) ^ (6166 * (κ + 9)) := by + rw [← Nat.pow_mul, Nat.mul_comm] + _ ≤ ((n + 2) ^ 2) ^ (6166 * (κ + 9)) := Nat.pow_le_pow_left hbase _ + _ = _ := by + rw [← Nat.pow_mul] + exact congrArg (fun e : ℕ => (n + 2) ^ e) + (by omega : 2 * (6166 * (κ + 9)) = 12332 * (κ + 9)) + +private theorem envelope_le_pow {n d g p A κ β b P : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hv : ∀ z ∈ values, z.natAbs ≤ A) + (hd : d ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) + (hb : b ≤ (n + 2) ^ β) (hP : P ≤ (n + 2) ^ β) : + b + 4 * windowSize n d g p (rawTotal n values) + P + 1024 ≤ + (n + 2) ^ (12332 * (κ + 9) + β + 13) := by + let B := n + 2 + let e := 12332 * (κ + 9) + β + 10 + have hb1 : 1 ≤ B := by dsimp only [B]; omega + have hb2 : 2 ≤ B := by dsimp only [B]; omega + have hm := (windowSize_le_pow values hlen hv hd hg hp hA).trans + (Nat.pow_le_pow_right hb1 (show 12332 * (κ + 9) ≤ e by dsimp only [e]; omega)) + have hb' := hb.trans (Nat.pow_le_pow_right hb1 (show β ≤ e by dsimp only [e]; omega)) + have hP' := hP.trans (Nat.pow_le_pow_right hb1 (show β ≤ e by dsimp only [e]; omega)) + have hc : 1024 ≤ B ^ e := (by decide : 1024 ≤ (2 : ℕ) ^ 10).trans + ((Nat.pow_le_pow_left hb2 10).trans + (Nat.pow_le_pow_right hb1 (show 10 ≤ e by dsimp only [e]; omega))) + calc + _ ≤ 7 * B ^ e := by omega + _ ≤ B ^ 3 * B ^ e := Nat.mul_le_mul_right _ + ((by decide : 7 ≤ (2 : ℕ) ^ 3).trans (Nat.pow_le_pow_left hb2 3)) + _ = _ := by rw [← pow_add]; congr 1; dsimp only [e]; omega + +/-- Positive logarithmic physical threshold. The original caller's placement/dirty-word +exponent β is separate from its original integer-weight exponent κ. -/ +theorem admissionWidth_le_log {n d g p A κ β b P : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hv : ∀ z ∈ values, z.natAbs ≤ A) + (hd : d ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) + (hb : b ≤ (n + 2) ^ β) (hP : P ≤ (n + 2) ^ β) : + admissionWidth n d g p (rawTotal n values) b P ≤ + (12332 * (κ + 9) + β + 14) * Nat.clog 2 (n + 2) := by + have he := envelope_le_pow values hlen hv hd hg hp hA hb hP + have he' := he.trans (Nat.pow_le_pow_left + (Nat.le_pow_clog (by decide : 1 < (2 : ℕ)) (n + 2)) _) + rw [← Nat.pow_mul] at he' + have hl := Nat.clog_le_of_le_pow he' + have hpos : 1 ≤ Nat.clog 2 (n + 2) := Nat.clog_pos (by decide) (by omega) + unfold admissionWidth + nlinarith only [hl, hpos] + +/-- All admitted prefixes use a polynomial numerical envelope in the original input size. -/ +theorem wordBound_le_pow {n d g p A κ β b P : ℕ} (values : List ℤ) + (hlen : values.length = 3 * (n * n)) (hv : ∀ z ∈ values, z.natAbs ≤ A) + (hd : d ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) + (hb : b ≤ (n + 2) ^ β) (hP : P ≤ (n + 2) ^ β) : + wordBound n d g p (rawTotal n values) b P ≤ + (n + 2) ^ (12332 * (κ + 9) + β + 15) := by + have he := envelope_le_pow values hlen hv hd hg hp hA hb hP + have hc : 4 ≤ (n + 2) ^ 2 := + (by decide : 4 ≤ (2 : ℕ) ^ 2).trans (Nat.pow_le_pow_left (by omega : 2 ≤ n + 2) 2) + calc + _ ≤ 4 * (n + 2) ^ (12332 * (κ + 9) + β + 13) := Nat.mul_le_mul_left _ he + _ ≤ (n + 2) ^ 2 * (n + 2) ^ (12332 * (κ + 9) + β + 13) := Nat.mul_le_mul_right _ hc + _ = _ := by rw [← pow_add]; congr 1; omega + +end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationInput.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationInput.lean index 92a263379b..84d6554ada 100644 --- a/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationInput.lean +++ b/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationInput.lean @@ -29,7 +29,8 @@ pre-halt state and the final halt charged. ## Main results -* `PreparationInput.exec_input`: structured execution for composition, without the final halt. +* `PreparationInput.exec_at`: structured execution from arbitrary registers and dirty memory. +* `PreparationInput.exec_input`: initialized structured execution, 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 diff --git a/Complexity/Computability/WordRAM/CopySum.lean b/Complexity/Computability/WordRAM/CopySum.lean old mode 100755 new mode 100644 diff --git a/Complexity/Computability/WordRAM/MemoryWindow/Normalization.lean b/Complexity/Computability/WordRAM/MemoryWindow/Normalization.lean old mode 100755 new mode 100644 diff --git a/ComplexityTests/WordRAMCallableFixedPrime.lean b/ComplexityTests/WordRAMCallableFixedPrime.lean old mode 100755 new mode 100644 index 30d2054048..27e107ef60 --- a/ComplexityTests/WordRAMCallableFixedPrime.lean +++ b/ComplexityTests/WordRAMCallableFixedPrime.lean @@ -6,7 +6,7 @@ Authors: Erik Demaine -- upstream: local-only (tests) -import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Program +import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Input /-! # Actual caller adaptation regressions @@ -55,4 +55,27 @@ private def adapted : Option (List ℕ × ℕ) := #guard adapted == some ([7, 16, 1, 1, 3, 5, 2, 8, 15, 777, 777, 1, 5, 99, 99], 62) +private def returned (flag : ℕ) : Option (List ℕ × ℕ) := + let x : Data 640 := + { regs := fun j => + if j = CallableFixedPrime.sourceReg FixedPrime.Reg.found then flag + else if j = CallableFixedPrime.sourceReg FixedPrime.Reg.scans then 3 + else 717 + mem := fun _ => 99 } + (CallableFixedPrime.receive.eval 16 1 x).map fun (y, t) => + ([y.regs CallableFixedPrime.Reg.found, y.regs CallableFixedPrime.Reg.scans, + y.regs CallableFixedPrime.Reg.witnessA, y.regs CallableFixedPrime.Reg.witnessB, + y.regs CallableFixedPrime.Reg.witnessC, y.regs 0, y.regs 159, y.mem 77], t) + +#guard returned 1 == some ([1, 3, 717, 717, 717, 717, 717, 99], 5) +#guard returned 0 == some ([0, 3, 717, 717, 717, 717, 717, 99], 5) + +private def initialized : Option (List ℕ × ℕ) := + let x : Data 640 := .init (PreparationInput.input 1 16 1 3 [-2, 1, 4]) + (CallableFixedPrime.entryHeader.eval 16 1 x).map fun (y, t) => + ([y.regs 600, y.regs 601, y.regs 602, y.regs 603, y.regs 604, y.regs 605, + y.regs 606, y.regs 607, y.regs 0, y.regs 159, y.mem 6, y.mem 7, y.mem 8], t) + +#guard initialized == some ([1, 16, 1, 3, 5, 6, 7, 8, 0, 0, 2, 8, 0], 14) + end ComplexityTests.WordRAMCallableFixedPrime diff --git a/ComplexityTests/WordRAMCallableFixedPrimeCaller.lean b/ComplexityTests/WordRAMCallableFixedPrimeCaller.lean new file mode 100644 index 0000000000..ff794d0f83 --- /dev/null +++ b/ComplexityTests/WordRAMCallableFixedPrimeCaller.lean @@ -0,0 +1,146 @@ +/- +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.CallableFixedPrime.SourceBounds +import Mathlib.Data.List.GetD + +/-! +# Admitted dirty caller with aliased original matrices + +The complete solver is called at valid geometry. All three original spans alias, its workspace +contains nonzero dirty words, and the selector bank contains 717. The proof connects the same +actual final state to the prefix, halt, verdict, global scan bound and protected caller frame. +No enormous complete interpreter evaluation or supplied source execution is used. +-/ + +namespace ComplexityTests.WordRAMCallableFixedPrimeCaller + +open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle +open Cslib.Algorithms.WordRAM.ExactTriangle +open Cslib.Algorithms.MatrixMultiplication.Schonhage + +private def base (N : ℕ) : ℕ := N * N + 1024 +private def oldBound (N : ℕ) : ℕ := base N + 4096 +private def zeros (N : ℕ) : List ℤ := List.replicate (3 * (N * N)) 0 +private def caller (N : ℕ) : Data 640 := + { regs := fun j => + if j.val = 600 then N else if j.val = 601 then 16 else if j.val = 602 then 1 + else if j.val = 603 then 3 else if j.val = 604 then 1 else if j.val = 605 then 1 + else if j.val = 606 then 1 else if j.val = 607 then base N else 717 + mem := fun q => if q < base N then 0 else 99 } +private def width (N : ℕ) : ℕ := + CallableFixedPrime.admissionWidth N (D 2) 1 3 (CallableFixedPrime.rawTotal N (zeros N)) + (base N) (oldBound N) + +private theorem caller_reg_bound (N : ℕ) (i : Fin 640) : (caller N).regs i ≤ oldBound N := by + have hn : N ≤ N * N + 1024 := by nlinarith + dsimp only [caller, oldBound, base] + split_ifs <;> omega + +private theorem caller_mem_bound (N q : ℕ) : (caller N).mem q ≤ oldBound N := by + change (if q < base N then 0 else 99) ≤ oldBound N + split <;> dsimp only [oldBound, base] <;> omega + +/-- A fully admitted dirty caller; original arrays may alias and low selector registers survive. -/ +private theorem dirty_alias (N : ℕ) (hgeo : D 2 ^ 18 ≤ N) : + ∃ y : Data 640, ∃ t : ℕ, + Runs (width N) (CallableFixedPrime.program.program CallableFixedPrime.Reg.found) + ⟨0, caller N⟩ ⟨CallableFixedPrime.program.size, y⟩ t ∧ + Executes (width N) (CallableFixedPrime.program.program CallableFixedPrime.Reg.found) + ⟨0, caller N⟩ 1 (t + 1) ∧ + y.regs CallableFixedPrime.Reg.found = 1 ∧ + y.regs CallableFixedPrime.Reg.scans ≤ 1 ∧ + y.regs 0 = 717 ∧ y.regs 159 = 717 ∧ y.regs CallableFixedPrime.Reg.ab = 1 ∧ + ∀ q, q < base N ∨ + base N + CallableFixedPrime.windowSize N (D 2) 1 3 + (CallableFixedPrime.rawTotal N (zeros N)) ≤ q → y.mem q = (caller N).mem q := by + have hp : 3 ∈ Nat.sqrtPrimeWindow (D 2) := + Nat.mem_sqrtPrimeWindow_iff_sq.mpr ⟨by decide, by decide, by decide⟩ + have hregs := caller_reg_bound N + have hmem := caller_mem_bound N + have hbounded : (caller N).Bounded (width N) := + CallableFixedPrime.original_bounded (caller N) hregs hmem le_rfl + have hfit : Fits (width N) (base N + + 4 * CallableFixedPrime.windowSize N (D 2) 1 3 + (CallableFixedPrime.rawTotal N (zeros N)) + 1024) := + (CallableFixedPrime.admission_fits (le_refl (width N))).of_le (by omega) + have hval0 (q : ℕ) : (zeros N).getD q 0 = 0 := + List.getElem?_getD_replicate_default_eq _ _ _ + have hread (q : ℕ) (hq : q < N * N) : (caller N).mem (1 + q) = + Signed.encode ((zeros N).getD q 0) := by + have hq' : 1 + q < base N := by dsimp only [base]; omega + rw [hval0] + change (if 1 + q < base N then 0 else 99) = Signed.encode 0 + simp only [ite_eq_left hq', Signed.encode, Int.natAbs_zero, + lt_self_iff_false, ite_eq_right (not_false)] + have hread' (q : ℕ) (hq : q < N * N) : (caller N).mem (1 + q) = + Signed.encode ((zeros N).getD (N * N + q) 0) := by + simpa only [hval0] using hread q hq + have hread'' (q : ℕ) (hq : q < N * N) : (caller N).mem (1 + q) = + Signed.encode ((zeros N).getD (2 * (N * N) + q) 0) := by + simpa only [hval0] using hread q hq + have hargs : (caller N).regs CallableFixedPrime.Reg.n = N ∧ + (caller N).regs CallableFixedPrime.Reg.dimension = D 2 ∧ + (caller N).regs CallableFixedPrime.Reg.groups = 1 ∧ + (caller N).regs CallableFixedPrime.Reg.prime = 3 ∧ + (caller N).regs CallableFixedPrime.Reg.base = base N ∧ + (caller N).regs CallableFixedPrime.Reg.ab = 1 ∧ + (caller N).regs CallableFixedPrime.Reg.bc = 1 ∧ + (caller N).regs CallableFixedPrime.Reg.ac = 1 := by + simp +decide [caller, CallableFixedPrime.Reg.n, CallableFixedPrime.Reg.dimension, + CallableFixedPrime.Reg.groups, CallableFixedPrime.Reg.prime, CallableFixedPrime.Reg.base, + CallableFixedPrime.Reg.ab, CallableFixedPrime.Reg.bc, CallableFixedPrime.Reg.ac, D] + obtain ⟨hn, hd, hg, hp', hb, hab, hbc, hac⟩ := hargs + obtain ⟨a, hout, y, he, yb, yf, ys, yiff, yw, frame, regs⟩ := + CallableFixedPrime.exec (m := 2) (zeros N) (by simp only [zeros, List.length_replicate]) + (by decide) (by decide) hp hgeo (caller N) hn hd hg hp' hb + (by rw [hab]; dsimp only [base]; omega) + (by rw [hbc]; dsimp only [base]; omega) + (by rw [hac]; dsimp only [base]; omega) + (by simpa only [hab] using hread) (by simpa only [hbc] using hread') + (by simpa only [hac] using hread'') hbounded hfit + let V := fun q => (zeros N).getD q 0 + have hval (q : ℕ) : V q = 0 := List.getElem?_getD_replicate_default_eq _ _ _ + have hzero : HasZeroTriangle (fun u v : Fin N => V (pairIndex (u, v))) + (fun b c => V (N * N + pairIndex (b, c))) + (fun u c => V (2 * (N * N) + pairIndex (u, c))) := by + let v : Fin N := ⟨0, lt_of_lt_of_le (by decide : 0 < D 2 ^ 18) hgeo⟩ + exact ⟨v, v, v, by simp only [hval, zero_add]⟩ + have hf : y.regs CallableFixedPrime.Reg.found = 1 := yiff.mpr hzero + have hF : falsePositiveCount (fun u v : Fin N => V (pairIndex (u, v))) + (fun b c => V (N * N + pairIndex (b, c))) + (fun u c => V (2 * (N * N) + pairIndex (u, c))) 3 = 0 := by + simp only [falsePositiveCount, IsFalsePositive, weightSum, hval, zero_add, + ne_eq, not_true_eq_false, false_and, Finset.filter_false, Finset.card_empty] + obtain ⟨t, ht, hex⟩ := he + refine ⟨y, t, ?_, ?_, hf, ?_, ?_, ?_, ?_, frame⟩ + · simpa only [Nat.zero_add] using hex.runs (pc := 0) + (p := CallableFixedPrime.program.program CallableFixedPrime.Reg.found) + (Program.Contains.self _).append_left + · simpa only [hf] using hex.executes CallableFixedPrime.Reg.found + · have hs : y.regs CallableFixedPrime.Reg.scans ≤ + falsePositiveCount (fun u v : Fin N => V (pairIndex (u, v))) + (fun b c => V (N * N + pairIndex (b, c))) + (fun u c => V (2 * (N * N) + pairIndex (u, c))) 3 + + y.regs CallableFixedPrime.Reg.found := ys + simpa only [hF, hf, zero_add] using hs + · exact (regs 0 (Or.inl (by decide))).trans rfl + · exact (regs 159 (Or.inl (by decide))).trans rfl + · exact (regs CallableFixedPrime.Reg.ab (Or.inr ⟨by decide, by decide⟩)).trans hab + +example : ∃ y : Data 640, ∃ t : ℕ, + Runs (width (16 ^ 18)) + (CallableFixedPrime.program.program CallableFixedPrime.Reg.found) + ⟨0, caller (16 ^ 18)⟩ ⟨CallableFixedPrime.program.size, y⟩ t ∧ + Executes (width (16 ^ 18)) + (CallableFixedPrime.program.program CallableFixedPrime.Reg.found) + ⟨0, caller (16 ^ 18)⟩ 1 (t + 1) := by + obtain ⟨y, t, hr, he, -⟩ := dirty_alias (16 ^ 18) (by decide) + exact ⟨y, t, hr, he⟩ + +end ComplexityTests.WordRAMCallableFixedPrimeCaller diff --git a/ComplexityTests/WordRAMCallableFixedPrimeInput.lean b/ComplexityTests/WordRAMCallableFixedPrimeInput.lean new file mode 100644 index 0000000000..5aabe62236 --- /dev/null +++ b/ComplexityTests/WordRAMCallableFixedPrimeInput.lean @@ -0,0 +1,148 @@ +/- +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.CallableFixedPrime.SourceBounds +import Mathlib.Data.List.GetD + +/-! +# Fully admitted caller-safe initialized fixed-prime decisions + +Both clients use actual header delivery, signed copies, computed source width, the memory-window +compiler and real solver from State.init, at valid positive thin geometry. +The all-one negative input has modular false positives at prime three, but no original zero; +its unsuccessful records collectively receive no additive successful-scan allowance. These +kernel proofs do not evaluate the enormous catalogue or encoder through the interpreter. +-/ + +namespace ComplexityTests.WordRAMCallableFixedPrimeInput + +open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle +open Cslib.Algorithms.WordRAM.ExactTriangle +open Cslib.Algorithms.MatrixMultiplication.Schonhage + +private def side : ℕ := 16 ^ 18 +private def weights (N : ℕ) (z : ℤ) : List ℤ := List.replicate (3 * (N * N)) z +private def width (N : ℕ) (z : ℤ) : ℕ := + CallableFixedPrime.inputWidth N (D 2) 1 3 (weights N z) + +private theorem prime : 3 ∈ Nat.sqrtPrimeWindow (D 2) := + Nat.mem_sqrtPrimeWindow_iff_sq.mpr ⟨by decide, by decide, by decide⟩ + +/-- The complete actual program returns one and an original witness on all-zero input. -/ +private theorem initialized_zero (N : ℕ) (hgeo : D 2 ^ 18 ≤ N) : ∃ y : Data 640, ∃ t : ℕ, + Runs (width N 0) (CallableFixedPrime.entryProgram.program CallableFixedPrime.Reg.found) + (State.init (PreparationInput.input N (D 2) 1 3 (weights N 0))) + ⟨CallableFixedPrime.entryProgram.size, y⟩ t ∧ + Executes (width N 0) (CallableFixedPrime.entryProgram.program CallableFixedPrime.Reg.found) + (State.init (PreparationInput.input N (D 2) 1 3 (weights N 0))) 1 (t + 1) ∧ + y.regs CallableFixedPrime.Reg.found = 1 ∧ y.regs CallableFixedPrime.Reg.scans ≤ 1 ∧ + ∃ u v c : Fin N, + y.regs CallableFixedPrime.Reg.witnessA = u.val ∧ + y.regs CallableFixedPrime.Reg.witnessB = v.val ∧ + y.regs CallableFixedPrime.Reg.witnessC = c.val := by + obtain ⟨hi, a, hout, y, t, ht, hr, he, yb, yf, ys, yiff, yw, frame, regs⟩ := + CallableFixedPrime.runs_input (m := 2) (n := N) (g := 1) (p := 3) + (W := width N 0) (weights N 0) (by simp only [weights, List.length_replicate]) + (by decide) (by decide) prime hgeo le_rfl + let V := fun q => (weights N 0).getD q 0 + have hval (q : ℕ) : V q = 0 := List.getElem?_getD_replicate_default_eq _ _ _ + have hzero : HasZeroTriangle (fun u v : Fin N => V (pairIndex (u, v))) + (fun b c => V (N * N + pairIndex (b, c))) + (fun u c => V (2 * (N * N) + pairIndex (u, c))) := by + let v : Fin N := ⟨0, lt_of_lt_of_le (by decide : 0 < D 2 ^ 18) hgeo⟩ + exact ⟨v, v, v, by simp only [hval, zero_add]⟩ + have hf : y.regs CallableFixedPrime.Reg.found = 1 := yiff.mpr hzero + have hF : falsePositiveCount (fun u v : Fin N => V (pairIndex (u, v))) + (fun b c => V (N * N + pairIndex (b, c))) + (fun u c => V (2 * (N * N) + pairIndex (u, c))) 3 = 0 := by + simp only [falsePositiveCount, IsFalsePositive, weightSum, hval, zero_add, + ne_eq, not_true_eq_false, false_and, Finset.filter_false, Finset.card_empty] + obtain ⟨u, v, c, hu, hv, hc, _⟩ := yw hf + refine ⟨y, t, hr, ?_, hf, ?_, u, v, c, hu, hv, hc⟩ + · simpa only [hf] using he + · have hs : y.regs CallableFixedPrime.Reg.scans ≤ + falsePositiveCount (fun u v : Fin N => V (pairIndex (u, v))) + (fun b c => V (N * N + pairIndex (b, c))) + (fun u c => V (2 * (N * N) + pairIndex (u, c))) 3 + + y.regs CallableFixedPrime.Reg.found := ys + simpa only [hF, hf, zero_add] using hs + +/-- Even with nonzero modular candidates, exhaustion of every actual record returns zero +exactly. The total scan bound is the single global false-positive count, with no extra one. -/ +private theorem initialized_one (N : ℕ) (hgeo : D 2 ^ 18 ≤ N) : + let V := fun q => (weights N 1).getD q 0 + let F := falsePositiveCount (fun u v : Fin N => V (pairIndex (u, v))) + (fun b c => V (N * N + pairIndex (b, c))) + (fun u c => V (2 * (N * N) + pairIndex (u, c))) 3 + ∃ y : Data 640, ∃ t : ℕ, + Runs (width N 1) (CallableFixedPrime.entryProgram.program CallableFixedPrime.Reg.found) + (State.init (PreparationInput.input N (D 2) 1 3 (weights N 1))) + ⟨CallableFixedPrime.entryProgram.size, y⟩ t ∧ + Executes (width N 1) (CallableFixedPrime.entryProgram.program CallableFixedPrime.Reg.found) + (State.init (PreparationInput.input N (D 2) 1 3 (weights N 1))) 0 (t + 1) ∧ + y.regs CallableFixedPrime.Reg.found = 0 ∧ y.regs CallableFixedPrime.Reg.scans ≤ F := by + obtain ⟨hi, a, hout, y, t, ht, hr, he, yb, yf, ys, yiff, yw, frame, regs⟩ := + CallableFixedPrime.runs_input (m := 2) (n := N) (g := 1) (p := 3) + (W := width N 1) (weights N 1) (by simp only [weights, List.length_replicate]) + (by decide) (by decide) prime hgeo le_rfl + let V := fun q => (weights N 1).getD q 0 + have hval (q : ℕ) (hq : q < 3 * (N * N)) : V q = 1 := + List.getD_replicate (1 : ℤ) hq + have pair_bound (u v : Fin N) : pairIndex (u, v) < N * N := by + have hu := Nat.mul_le_mul_right N (Nat.succ_le_of_lt u.isLt) + rw [Nat.succ_mul] at hu + change u.val * N + v.val < N * N + have hv := v.isLt + omega + have hn : ¬ HasZeroTriangle (fun u v : Fin N => V (pairIndex (u, v))) + (fun b c => V (N * N + pairIndex (b, c))) + (fun u c => V (2 * (N * N) + pairIndex (u, c))) := by + rintro ⟨u, v, c, hz⟩ + change V (pairIndex (u, v)) + V (N * N + pairIndex (v, c)) + + V (2 * (N * N) + pairIndex (u, c)) = 0 at hz + rw [hval (pairIndex (u, v)) (by have := pair_bound u v; omega), + hval (N * N + pairIndex (v, c)) (by have := pair_bound v c; omega), + hval (2 * (N * N) + pairIndex (u, c)) (by have := pair_bound u c; omega)] at hz + norm_num at hz + have hf : y.regs CallableFixedPrime.Reg.found = 0 := by + rcases yf with h | h + · exact h + · exact False.elim (hn (yiff.mp h)) + refine ⟨y, t, hr, ?_, hf, ?_⟩ + · simpa only [hf] using he + · simpa only [hf, Nat.add_zero] using ys + + +example : ∃ y : Data 640, ∃ t : ℕ, + Runs (width side 0) (CallableFixedPrime.entryProgram.program CallableFixedPrime.Reg.found) + (State.init (PreparationInput.input side (D 2) 1 3 (weights side 0))) + ⟨CallableFixedPrime.entryProgram.size, y⟩ t ∧ + Executes (width side 0) (CallableFixedPrime.entryProgram.program CallableFixedPrime.Reg.found) + (State.init (PreparationInput.input side (D 2) 1 3 (weights side 0))) 1 (t + 1) ∧ + y.regs CallableFixedPrime.Reg.found = 1 ∧ y.regs CallableFixedPrime.Reg.scans ≤ 1 ∧ + ∃ u v c : Fin side, + y.regs CallableFixedPrime.Reg.witnessA = u.val ∧ + y.regs CallableFixedPrime.Reg.witnessB = v.val ∧ + y.regs CallableFixedPrime.Reg.witnessC = c.val := + initialized_zero side (by decide) + +example : + let V := fun q => (weights side 1).getD q 0 + let F := falsePositiveCount (fun u v : Fin side => V (pairIndex (u, v))) + (fun b c => V (side * side + pairIndex (b, c))) + (fun u c => V (2 * (side * side) + pairIndex (u, c))) 3 + ∃ y : Data 640, ∃ t : ℕ, + Runs (width side 1) (CallableFixedPrime.entryProgram.program CallableFixedPrime.Reg.found) + (State.init (PreparationInput.input side (D 2) 1 3 (weights side 1))) + ⟨CallableFixedPrime.entryProgram.size, y⟩ t ∧ + Executes (width side 1) (CallableFixedPrime.entryProgram.program CallableFixedPrime.Reg.found) + (State.init (PreparationInput.input side (D 2) 1 3 (weights side 1))) 0 (t + 1) ∧ + y.regs CallableFixedPrime.Reg.found = 0 ∧ y.regs CallableFixedPrime.Reg.scans ≤ F := + initialized_one side (by decide) + +end ComplexityTests.WordRAMCallableFixedPrimeInput From 61fec43436dd0b2b605e19565cce9db7eba490b4 Mon Sep 17 00:00:00 2001 From: Erik Demaine Date: Sun, 1 Nov 2026 01:01:17 -0400 Subject: [PATCH 3/4] chore(ExactTriangle): normalize initialized caller file mode Only mode100755 to100644; source bytes and targeted Lean evidence from69495f23b unchanged. Source-ready2125 still awaits coordinated canonical imports/static and fresh whole-layer review; no all-six claim. --- .../Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Flat.lean | 0 1 file changed, 0 insertions(+), 0 deletions(-) mode change 100755 => 100644 Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Flat.lean diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Flat.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/Flat.lean old mode 100755 new mode 100644 From dc92727dc2744d3f1420d5b1ddd9144603d9c207 Mon Sep 17 00:00:00 2001 From: Erik Demaine Date: Sun, 1 Nov 2026 01:12:34 -0400 Subject: [PATCH 4/4] feat(ExactTriangle): finalize callable fixed-prime imports and validation Final #2125 candidate on one normal compatibility merge of pinned main b4678e2063c4de73cd39b02d1af26045e5ac6289. All28 source-ready owned source blobs and modes are identical to61fec4343, all inherited main blobs preserved, and only22 canonical imports added. No source/proof/program repair during this final audit. Frozen validated source tree ff0dd30bd22eecb962c199c873d76609e1084840. Strict cache-disabled scoped build PASS for new CallableFixedPrime umbrella, all3 owned tests (WordRAMCallableFixedPrime, WordRAMCallableFixedPrimeInput, WordRAMCallableFixedPrimeCaller) and existing WordRAMExactTriangleFixedPrimeInput. Canonical mk_all check PASS; full hygiene --check-simp PASS; changed25-library environment lint PASS (538 local declarations, imported-environment nonlocal linters too); fresh scoped compiled doc-name/3-new-test audits PASS; strict PR body declaration names PASS; whole pinned-base/staged/unstaged diff --check PASS. One compiler thread, downloads disabled. Exact own/supplier/main/native-code/statement/private-fit and primary-pin/blob/locator identities PASS. All audit processes finished. Scope limitation: NO local whole-library/all-six claim. Standard changed-file CLI first rejected missing whole-library freshness/root artifacts, including unrelated WordRAMUniformProbing. Its unchanged repository doc/test lint functions passed on fresh strictly built scoped25lib/3test artifacts instead; full standard CLI and all six gates require hosted exact-head CI before integration. Initial mk_all generation exit1 denoted one updated aggregate; subsequent check0. Initial lake lint argument parsing fixed by direct existing Batteries script; no source workaround. Preserved raw logs/summary/validation and reproducible audit helpers under tmp/callable-fixed-prime-3dda8289/final. Code/model: fixed640 standard caller protects low160 and args600..607, returns raw632 flag/633..635 original witness/636 global scans; actual signed copying+sum/native modulus/dirty normalization/one producer/all-record execution, initialized same-y prefix+halt, exact positive AND negative ET iff, global S<=F(p)+actualFlag and caller frame. Original D4^m>=16, n>=D^18,g>=1,p-window and raw old-word/address bounds explicit. Complete charged preparation/product/query/control/scan/compiler/copy/setup/return/halt bounds, positive source-regime log admission and independent-W polynomial prefix/support proved. Full parameter/prime/outer host/asymptotic1394/1.9992 remains OPEN; no selected-prime/uniform fast endpoint claimed. Fresh whole-layer nonauthoring review remains REQUIRED before publication, covering CopySum, normalization, producer exec_at/input_fits/locality, dirty source derivation, actual640 caller/init, every-wide prefix and costs. Unchanged supplier reviews are not approval of new reasoning. No PR/watch/merge by child. Abstract/catalogue/rendering no impact. AI assistance: OpenAI Codex; existing source credit retained. Canonical imports are the only source delta from the source-ready checkpoint plus pinned-main compatibility. --- Complexity.lean | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/Complexity.lean b/Complexity.lean index d3be46c9a8..423bc6cbda 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -147,6 +147,26 @@ public import Complexity.Algorithms.WordRAM.DynamicArray public import Complexity.Algorithms.WordRAM.ElementDistinctness public import Complexity.Algorithms.WordRAM.ElementDistinctnessRAM public import Complexity.Algorithms.WordRAM.ExactLog +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Adapt +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Admission +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Copy +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Core +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Exec +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Flat +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Header +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Input +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.InputSpec +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Parameters +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Prefix +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Program +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Properties +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Receive +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Setup +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Source +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.SourceBounds +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.TimeBound +public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Width public import Complexity.Algorithms.WordRAM.ExactTriangle.Catalogue public import Complexity.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue public import Complexity.Algorithms.WordRAM.ExactTriangle.Chunks @@ -2418,6 +2438,7 @@ public import Complexity.Computability.WordRAM.Basis public import Complexity.Computability.WordRAM.Compile public import Complexity.Computability.WordRAM.Controller public import Complexity.Computability.WordRAM.Copy +public import Complexity.Computability.WordRAM.CopySum public import Complexity.Computability.WordRAM.Defs public import Complexity.Computability.WordRAM.Dynamic public import Complexity.Computability.WordRAM.ExactNotation @@ -2430,6 +2451,7 @@ public import Complexity.Computability.WordRAM.ListArray public import Complexity.Computability.WordRAM.ListOutput public import Complexity.Computability.WordRAM.MapOp public import Complexity.Computability.WordRAM.MemoryWindow +public import Complexity.Computability.WordRAM.MemoryWindow.Normalization public import Complexity.Computability.WordRAM.Multiword public import Complexity.Computability.WordRAM.Multiword.Arithmetic public import Complexity.Computability.WordRAM.Multiword.Bank