From 5909d1bae7648600e86ab49730835ce9d336ca95 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 1 Nov 2026 17:07:14 -0500 Subject: [PATCH 1/9] feat(DataStructure/Memory): word-addressed memory oracle and named field arrays Memory.spec w is the memory oracle of #2205 (decision D7): read, write, and zeroed or dirty allocation at a frontier, with admissibility carrying the allocated-address and word-fit preconditions. Field arrays are WordRAM Blocks accessed by Block.get/Block.set programs over the oracle. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 2 + Complexity/DataStructure/Memory/Field.lean | 183 +++++++++++++++ Complexity/DataStructure/Memory/Spec.lean | 258 +++++++++++++++++++++ ComplexityTests/DataStructureMemory.lean | 117 ++++++++++ 4 files changed, 560 insertions(+) create mode 100644 Complexity/DataStructure/Memory/Field.lean create mode 100644 Complexity/DataStructure/Memory/Spec.lean create mode 100644 ComplexityTests/DataStructureMemory.lean diff --git a/Complexity.lean b/Complexity.lean index 7f9a77746d..00f4bf2faf 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2873,6 +2873,8 @@ public import Complexity.DataStructure.HashFamily.WordRAM.DoubleTabulation public import Complexity.DataStructure.HashFamily.WordRAM.KWise public import Complexity.DataStructure.HashFamily.WordRAM.MultiplyShift public import Complexity.DataStructure.HashFamily.WordRAM.Tabulation +public import Complexity.DataStructure.Memory.Field +public import Complexity.DataStructure.Memory.Spec public import Complexity.DataStructure.ObliviousSequence public import Complexity.DataStructure.Online.Basic public import Complexity.DataStructure.OrderedSet.Basic diff --git a/Complexity/DataStructure/Memory/Field.lean b/Complexity/DataStructure/Memory/Field.lean new file mode 100644 index 0000000000..f065798d88 --- /dev/null +++ b/Complexity/DataStructure/Memory/Field.lean @@ -0,0 +1,183 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.WordRAM.ListArray +public import Complexity.DataStructure.Memory.Spec + +/-! +# Named field arrays over the memory oracle + +A field array is a `Cslib.WordRAM.Block`: a base address and a length. A data structure lays out +its storage as a structure whose fields are blocks (a struct of arrays) and accesses entry `i` of +a field `f` with the programs `f.get i` and `f.set i v` over `Memory.spec w`. Addresses are thus +named (`par.get v`) rather than computed by hand (`base + n + v`), while computed indices, pointer +chasing (`do let p ← next.get v; key.get p`) and reuse of a block across operations remain +ordinary programs. + +The lemmas here evaluate these programs, discharge their admissibility from `Block.Allocated`, +and describe their frame: a write to a field leaves every other address unchanged. +`Block.entries` reads the first `n` entries of a field as a list, which is how an abstraction +function usually sees an array. It realizes `Block.HoldsList`. + +## Main definitions + +* `Cslib.WordRAM.Block.get`, `Cslib.WordRAM.Block.set`: entry access through the oracle. +* `Cslib.WordRAM.Block.Allocated`: the block lies below the frontier. +* `Cslib.WordRAM.Block.entries`: the first `n` entries of a field in index order. +* `Cslib.DataStructure.Memory.allocBlock`, `Cslib.DataStructure.Memory.allocBlockDirty`: + allocate a field. + +## Main results + +* `Cslib.WordRAM.Block.runClient_get_bind`, `Cslib.WordRAM.Block.runClient_set_bind`: one-step + evaluation of field accesses. +* `Cslib.WordRAM.Block.Allocated.lt_frontier`, `Cslib.WordRAM.Block.Allocated.mono`: allocated + entries are admissible addresses, and stay allocated. +* `Cslib.WordRAM.Block.entries_succ`, `Cslib.WordRAM.Block.entries_congr`, + `Cslib.WordRAM.Block.entries_update_of_le`, `Cslib.WordRAM.Block.entries_update_of_not_owns`: + the list view under appends and writes. +* `Cslib.WordRAM.Block.holdsList_entries`: the list view realizes `Block.HoldsList`. +* `Cslib.DataStructure.Memory.runClient_allocBlock_bind`: allocation hands out a zeroed, + allocated block at the frontier. +-/ + +@[expose] public section + +namespace Cslib.WordRAM.Block + +open Cslib.DataStructure + +/-- Read entry `i` of the field `b` through the memory oracle. -/ +abbrev get (b : Block) (i : ℕ) : Memory.Prog ℕ := Memory.read (b.base + i) + +/-- Write `v` to entry `i` of the field `b` through the memory oracle. -/ +abbrev set (b : Block) (i v : ℕ) : Memory.Prog Unit := Memory.write (b.base + i) v + +/-- The block lies below the frontier, so all of its entries are allocated. -/ +def Allocated (b : Block) (s : Memory.State) : Prop := b.base + b.length ≤ s.frontier + +/-- An entry of an allocated block is an allocated address. -/ +theorem Allocated.lt_frontier {b : Block} {s : Memory.State} (h : b.Allocated s) {i : ℕ} + (hi : i < b.length) : b.base + i < s.frontier := by + unfold Allocated at h + omega + +/-- A block stays allocated as the frontier grows. -/ +theorem Allocated.mono {b : Block} {s s' : Memory.State} (h : b.Allocated s) + (hs : s.frontier ≤ s'.frontier) : b.Allocated s' := + le_trans h hs + +/-- A block owns the address of each of its entries. -/ +theorem owns_add {b : Block} {i : ℕ} (hi : i < b.length) : b.Owns (b.base + i) := + ⟨Nat.le_add_right _ _, Nat.add_lt_add_left hi _⟩ + +/-- Reading an entry returns the cell and leaves memory unchanged. -/ +@[simp] theorem runClient_get_bind {w : ℕ} {α : Type} (b : Block) (i : ℕ) (k : ℕ → Memory.Prog α) + (s : Memory.State) : + (Memory.spec w).runClient s (b.get i >>= k) = + let (v, s', os) := (Memory.spec w).runClient s (k (s.mem (b.base + i))) + (v, s', .read (b.base + i) :: os) := rfl + +/-- Writing an entry updates its cell. -/ +@[simp] theorem runClient_set_bind {w : ℕ} {α : Type} (b : Block) (i v : ℕ) + (k : Unit → Memory.Prog α) (s : Memory.State) : + (Memory.spec w).runClient s (b.set i v >>= k) = + let (r, s', os) := (Memory.spec w).runClient + ⟨Function.update s.mem (b.base + i) v, s.frontier⟩ (k ()) + (r, s', .write (b.base + i) v :: os) := rfl + +/-! ## The list of entries -/ + +/-- The first `n` entries of the field `b` in memory `m`, in index order. -/ +def entries (b : Block) (n : ℕ) (m : ℕ → ℕ) : List ℕ := + (List.range n).map fun i => m (b.base + i) + +@[simp] theorem length_entries (b : Block) (n : ℕ) (m : ℕ → ℕ) : (b.entries n m).length = n := by + simp [entries] + +@[simp] theorem entries_zero (b : Block) (m : ℕ → ℕ) : b.entries 0 m = [] := rfl + +/-- Entry `i` of the list view is the cell at `b.base + i`. -/ +@[simp] theorem getElem_entries (b : Block) (n : ℕ) (m : ℕ → ℕ) (i : ℕ) + (hi : i < (b.entries n m).length) : (b.entries n m)[i] = m (b.base + i) := by + simp [entries] + +/-- One more entry appends its cell. -/ +theorem entries_succ (b : Block) (n : ℕ) (m : ℕ → ℕ) : + b.entries (n + 1) m = b.entries n m ++ [m (b.base + n)] := by + simp [entries, List.range_succ] + +/-- The list view depends only on the cells of its entries. -/ +theorem entries_congr (b : Block) (n : ℕ) {m m' : ℕ → ℕ} + (h : ∀ i < n, m' (b.base + i) = m (b.base + i)) : b.entries n m' = b.entries n m := + List.map_congr_left fun i hi => h i (List.mem_range.mp hi) + +/-- Writing at or beyond entry `n` leaves the first `n` entries unchanged. -/ +theorem entries_update_of_le (b : Block) {n i : ℕ} (hi : n ≤ i) (m : ℕ → ℕ) (v : ℕ) : + b.entries n (Function.update m (b.base + i) v) = b.entries n m := + b.entries_congr n fun j hj => Function.update_of_ne (by omega) v m + +/-- Writing outside the block leaves every entry unchanged. -/ +theorem entries_update_of_not_owns (b : Block) {n : ℕ} (hn : n ≤ b.length) {a : ℕ} + (ha : ¬b.Owns a) (m : ℕ → ℕ) (v : ℕ) : + b.entries n (Function.update m a v) = b.entries n m := + b.entries_congr n fun j hj => + Function.update_of_ne (fun h => ha (by rw [← h]; exact owns_add (by omega))) v m + +/-- The list view of `n` entries realizes the list at the block's base. -/ +theorem holdsList_entries (b : Block) (n : ℕ) (m : ℕ → ℕ) : + HoldsList b.base (b.entries n m) m := fun i => by + simp [Block.read] + +end Cslib.WordRAM.Block + +namespace Cslib.DataStructure.Memory + +open Cslib.WordRAM + +/-- Allocate a zeroed field of `k` cells. -/ +def allocBlock (k : ℕ) : Prog Block := do + let base ← alloc k + pure ⟨base, k⟩ + +/-- Allocate a field of `k` cells without clearing it. -/ +def allocBlockDirty (k : ℕ) : Prog Block := do + let base ← allocDirty k + pure ⟨base, k⟩ + +/-- A zeroed allocation hands out the block at the frontier, clears it, and advances the +frontier past it. -/ +@[simp] theorem runClient_allocBlock_bind {w : ℕ} {α : Type} (k : ℕ) (next : Block → Prog α) + (s : State) : + (spec w).runClient s (allocBlock k >>= next) = + let (v, s', os) := (spec w).runClient + ⟨clear s.mem s.frontier k, s.frontier + k⟩ (next ⟨s.frontier, k⟩) + (v, s', .alloc k :: os) := rfl + +/-- A dirty allocation hands out the block at the frontier without changing memory. -/ +@[simp] theorem runClient_allocBlockDirty_bind {w : ℕ} {α : Type} (k : ℕ) + (next : Block → Prog α) (s : State) : + (spec w).runClient s (allocBlockDirty k >>= next) = + let (v, s', os) := (spec w).runClient ⟨s.mem, s.frontier + k⟩ (next ⟨s.frontier, k⟩) + (v, s', .allocDirty k :: os) := rfl + +/-- A freshly allocated block is allocated in the new state. -/ +theorem allocated_alloc (s : State) (k : ℕ) : + (Block.mk s.frontier k).Allocated ⟨clear s.mem s.frontier k, s.frontier + k⟩ := + le_rfl + +/-- A freshly allocated zeroed block holds zeros. -/ +theorem entries_alloc (s : State) (k : ℕ) {n : ℕ} (hn : n ≤ k) : + (Block.mk s.frontier k).entries n (clear s.mem s.frontier k) = List.replicate n 0 := by + refine List.ext_getElem (by simp) fun i hi _ => ?_ + simp only [Block.length_entries] at hi + simp only [Block.getElem_entries, List.getElem_replicate] + exact clear_of_owns (Block.owns_add (b := ⟨s.frontier, k⟩) (by simp only; omega)) + +end Cslib.DataStructure.Memory diff --git a/Complexity/DataStructure/Memory/Spec.lean b/Complexity/DataStructure/Memory/Spec.lean new file mode 100644 index 0000000000..3507072aee --- /dev/null +++ b/Complexity/DataStructure/Memory/Spec.lean @@ -0,0 +1,258 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.WordRAM.Heap +public import Complexity.DataStructure.StateTransition + +/-! +# Word-addressed memory as a state-transition specification + +`Memory.spec w` is a memory oracle: the interface through which a data-structure implementation +reaches storage. Its state is the contents of every cell together with an allocation frontier. +Every address below the frontier is allocated, and allocation hands out the block that starts at +the frontier. The operations read a cell, write a cell, and allocate a block, either zeroed +(`alloc`, charged per cell) or with its old contents (`allocDirty`, charged one unit). + +Admissibility carries the preconditions a word RAM needs. Accessed addresses must be allocated, +written values must fit a `w`-bit word, and the frontier after an allocation must fit. Under +these preconditions the frontier and every cell keep fitting a word (`WellFormed.step`), so an +allocated address fits too (`WellFormed.fits_of_lt_frontier`). + +An implementation over this interface is an ordinary `Memory.Prog` program. Its correctness and +its operation charges are proved against `step` and `charge`, without registers or instruction +counts. `charge` is the memory-level currency; executing such a program on the word RAM is a +separate step that exchanges it into instructions. Allocation never reuses addresses, as in +`Cslib.WordRAM.alloc`, so blocks allocated at different times are disjoint +(`Cslib.WordRAM.Block.disjoint_of_le`). A program reuses memory by keeping a block it allocated. + +## Main definitions + +* `Memory.State`, `Memory.Op`, `Memory.step`, `Memory.valid`: cells and frontier, operations + with their answers, the transition function and the admissibility preconditions. +* `Memory.spec`: the deterministic specification at word size `w`. +* `Memory.charge`: one unit per read, write and dirty allocation; `k + 1` for a zeroed block of + `k` cells. +* `Memory.Prog`, `Memory.read`, `Memory.write`, `Memory.alloc`, `Memory.allocDirty`: programs + over the oracle and its four one-call programs. +* `Memory.WellFormed`: the frontier and all cell contents fit a `w`-bit word. +* `Memory.State.init`: the word RAM's input convention as a memory state. + +## Main results + +* `Memory.WellFormed.step`, `Memory.WellFormed.run`: admissible operations preserve + well-formedness. +* `Memory.WellFormed.fits_of_lt_frontier`: allocated addresses fit a word. +* `Memory.frontier_le_step`, `Memory.frontier_le_run`: the frontier never decreases. +* `Memory.mem_step_of_lt_frontier`: an operation changes an allocated cell only by writing it. +* `Memory.wellFormed_init`: the input convention is well formed. +-/ + +@[expose] public section + +namespace Cslib.DataStructure.Memory + +open Cslib.WordRAM + +/-- Memory: the contents of every cell, and the frontier below which cells are allocated. -/ +@[ext] +structure State where + /-- The contents of the cell at each address. -/ + mem : ℕ → ℕ + /-- Every address below the frontier is allocated; the next block starts here. -/ + frontier : ℕ + +/-- Operations on memory. Addresses are words computed by the caller. -/ +inductive Op where + /-- Read the cell at an address. -/ + | read (addr : ℕ) + /-- Write a value to the cell at an address. -/ + | write (addr value : ℕ) + /-- Allocate `count` zeroed cells at the frontier and return their base address. -/ + | alloc (count : ℕ) + /-- Allocate `count` cells at the frontier without clearing them and return their base + address. -/ + | allocDirty (count : ℕ) + deriving DecidableEq + +/-- The answer type of each operation: a read and an allocation return a word. -/ +abbrev Op.Result : Op → Type + | .read _ => ℕ + | .write _ _ => Unit + | .alloc _ => ℕ + | .allocDirty _ => ℕ + +/-- The transition of each operation. An allocation returns the old frontier. -/ +def step (s : State) : (o : Op) → State × o.Result + | .read a => (s, s.mem a) + | .write a v => (⟨Function.update s.mem a v, s.frontier⟩, ()) + | .alloc k => (⟨clear s.mem s.frontier k, s.frontier + k⟩, s.frontier) + | .allocDirty k => (⟨s.mem, s.frontier + k⟩, s.frontier) + +/-- Admissibility at word size `w`: accessed addresses are allocated, written values fit a word, +and an allocation leaves a fitting frontier. -/ +def valid (w : ℕ) (s : State) : Op → Prop + | .read a => a < s.frontier + | .write a v => a < s.frontier ∧ Fits w v + | .alloc k => Fits w (s.frontier + k) + | .allocDirty k => Fits w (s.frontier + k) + +instance (w : ℕ) (s : State) (o : Op) : Decidable (valid w s o) := by + cases o <;> unfold valid <;> infer_instance + +/-- Word-addressed memory at word size `w`. -/ +abbrev spec (w : ℕ) : StateTransitionSpec := + StateTransitionSpec.ofFn (State := State) (Op := Op) (Result := Op.Result) step (valid w) + +/-- The memory-level currency: one unit per read, write and dirty allocation, and `k + 1` units +for a zeroed block of `k` cells. -/ +def charge (_ : State) : Op → ℕ + | .alloc k => k + 1 + | _ => 1 + +/-- Programs over the memory oracle. They are the clients of `Memory.spec w` at every word size. -/ +abbrev Prog (α : Type) : Type := PFunctor.FreeM ⟨Op, Op.Result⟩ α + +/-- Read the cell at address `a`. -/ +abbrev read (a : ℕ) : Prog ℕ := PFunctor.FreeM.lift (P := ⟨Op, Op.Result⟩) (.read a) + +/-- Write `v` to the cell at address `a`. -/ +abbrev write (a v : ℕ) : Prog Unit := PFunctor.FreeM.lift (P := ⟨Op, Op.Result⟩) (.write a v) + +/-- Allocate `k` zeroed cells and return their base address. -/ +abbrev alloc (k : ℕ) : Prog ℕ := PFunctor.FreeM.lift (P := ⟨Op, Op.Result⟩) (.alloc k) + +/-- Allocate `k` cells without clearing them and return their base address. -/ +abbrev allocDirty (k : ℕ) : Prog ℕ := + PFunctor.FreeM.lift (P := ⟨Op, Op.Result⟩) (.allocDirty k) + +@[simp] theorem step_read (s : State) (a : ℕ) : step s (.read a) = (s, s.mem a) := rfl + +@[simp] theorem step_write (s : State) (a v : ℕ) : + step s (.write a v) = (⟨Function.update s.mem a v, s.frontier⟩, ()) := rfl + +@[simp] theorem step_alloc (s : State) (k : ℕ) : + step s (.alloc k) = (⟨clear s.mem s.frontier k, s.frontier + k⟩, s.frontier) := rfl + +@[simp] theorem step_allocDirty (s : State) (k : ℕ) : + step s (.allocDirty k) = (⟨s.mem, s.frontier + k⟩, s.frontier) := rfl + +@[simp] theorem valid_read (w : ℕ) (s : State) (a : ℕ) : valid w s (.read a) ↔ a < s.frontier := + Iff.rfl + +@[simp] theorem valid_write (w : ℕ) (s : State) (a v : ℕ) : + valid w s (.write a v) ↔ a < s.frontier ∧ Fits w v := Iff.rfl + +@[simp] theorem valid_alloc (w : ℕ) (s : State) (k : ℕ) : + valid w s (.alloc k) ↔ Fits w (s.frontier + k) := Iff.rfl + +@[simp] theorem valid_allocDirty (w : ℕ) (s : State) (k : ℕ) : + valid w s (.allocDirty k) ↔ Fits w (s.frontier + k) := Iff.rfl + +@[simp] theorem charge_read (s : State) (a : ℕ) : charge s (.read a) = 1 := rfl + +@[simp] theorem charge_write (s : State) (a v : ℕ) : charge s (.write a v) = 1 := rfl + +@[simp] theorem charge_alloc (s : State) (k : ℕ) : charge s (.alloc k) = k + 1 := rfl + +@[simp] theorem charge_allocDirty (s : State) (k : ℕ) : charge s (.allocDirty k) = 1 := rfl + +/-- Admissibility of a concrete history is decidable. -/ +instance decidableValidHistory (w : ℕ) (s : State) (os : List Op) : + Decidable ((spec w).ValidHistory s os) := by + induction os generalizing s with + | nil => exact isTrue trivial + | cons o os ih => + exact decidable_of_iff (valid w s o ∧ (spec w).ValidHistory (step s o).1 os) Iff.rfl + +/-! ## Frontier and frame -/ + +/-- No operation lowers the frontier. -/ +theorem frontier_le_step (s : State) (o : Op) : s.frontier ≤ (step s o).1.frontier := by + cases o <;> simp + +/-- No sequence of operations lowers the frontier. -/ +theorem frontier_le_run {w : ℕ} (s : State) (os : List Op) : + s.frontier ≤ ((spec w).run s os).1.frontier := by + induction os generalizing s with + | nil => exact le_rfl + | cons o os ih => exact (frontier_le_step s o).trans (ih _) + +/-- An operation changes an allocated cell only by writing to it. Allocation clears cells at or +above the frontier only. -/ +theorem mem_step_of_lt_frontier (s : State) (o : Op) {a : ℕ} (ha : a < s.frontier) + (hw : ∀ v, o ≠ .write a v) : (step s o).1.mem a = s.mem a := by + cases o with + | read => rfl + | write b v => + have hab : a ≠ b := fun h => hw v (h ▸ rfl) + exact Function.update_of_ne hab v s.mem + | alloc k => exact clear_of_not_owns (by simp only [Block.Owns]; omega) + | allocDirty => rfl + +/-! ## Word fit -/ + +/-- The frontier and every cell fit a `w`-bit word. Admissible operations preserve this. -/ +structure WellFormed (w : ℕ) (s : State) : Prop where + /-- The frontier fits a word, hence so does every allocated address. -/ + frontier_fits : Fits w s.frontier + /-- Every cell holds a word. -/ + mem_fits : ∀ a, Fits w (s.mem a) + +/-- Allocated addresses fit a word. -/ +theorem WellFormed.fits_of_lt_frontier {w : ℕ} {s : State} (h : WellFormed w s) {a : ℕ} + (ha : a < s.frontier) : Fits w a := + h.frontier_fits.of_le ha.le + +/-- Admissible operations preserve well-formedness. -/ +theorem WellFormed.step {w : ℕ} {s : State} (h : WellFormed w s) {o : Op} (hv : valid w s o) : + WellFormed w (Memory.step s o).1 := by + cases o with + | read => exact h + | write a v => + refine ⟨h.frontier_fits, fun b => ?_⟩ + by_cases hb : b = a + · subst hb + simpa using hv.2 + · simpa [Function.update_of_ne hb] using h.mem_fits b + | alloc k => + refine ⟨hv, fun b => ?_⟩ + simp only [step_alloc, clear] + split + · exact fits_zero w + · exact h.mem_fits b + | allocDirty k => exact ⟨hv, h.mem_fits⟩ + +/-- Admissible histories preserve well-formedness. -/ +theorem WellFormed.run {w : ℕ} {s : State} (h : WellFormed w s) {os : List Op} + (hv : (spec w).ValidHistory s os) : WellFormed w ((spec w).run s os).1 := by + induction os generalizing s with + | nil => exact h + | cons o os ih => exact ih (h.step hv.1) hv.2 + +/-! ## The input convention -/ + +/-- The word RAM's input convention (`Cslib.WordRAM.Data.init`) as a memory state: the input +length at address `0`, the input words at addresses `1, …, n`, and everything up to the input +allocated. -/ +def State.init (input : List ℕ) : State := + ⟨(Data.init (r := 0) input).mem, input.length + 1⟩ + +/-- The input convention is well formed when the input and its frontier fit a word. -/ +theorem wellFormed_init {w : ℕ} {input : List ℕ} (hin : InputFits w input) + (hf : Fits w (input.length + 1)) : WellFormed w (State.init input) := by + refine ⟨hf, fun a => ?_⟩ + change Fits w (if a = 0 then input.length else input.getD (a - 1) 0) + split + · exact hin.1 + · rw [List.getD_eq_getElem?_getD] + cases hi : input[a - 1]? with + | none => exact fits_zero w + | some v => exact hin.2 v (List.mem_of_getElem? hi) + +end Cslib.DataStructure.Memory diff --git a/ComplexityTests/DataStructureMemory.lean b/ComplexityTests/DataStructureMemory.lean new file mode 100644 index 0000000000..01791c6332 --- /dev/null +++ b/ComplexityTests/DataStructureMemory.lean @@ -0,0 +1,117 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: local-only (test driver) + +public import Complexity.DataStructure.Memory.Field + +/-! +# Memory-oracle programs: named fields, pointer chasing and block reuse + +A singly linked list is stored as a struct of arrays with a `key` field and a `next` field; +pointers are indices, with `0` as null. The tests allocate the layout, build a two-node list, +chase pointers to sum the keys, and reuse one scratch block across two rounds. They check the +answers, the operation histories and charges, admissibility at an 8-bit word size, and two +rejected operations: a read above the frontier and a write of an oversized value. +-/ + +@[expose] public section + +namespace ComplexityTests.DataStructureMemory + +open Cslib.WordRAM Cslib.DataStructure Cslib.DataStructure.Memory + +/-- A linked-list node store as a struct of arrays. -/ +structure Nodes where + /-- The key of each node. -/ + key : Block + /-- The successor of each node, as an index; `0` is null. -/ + next : Block + +/-- Allocate both fields for `n` nodes. -/ +def Nodes.alloc (n : ℕ) : Prog Nodes := do + let key ← allocBlock n + let next ← allocBlock n + pure ⟨key, next⟩ + +/-- Follow at most `fuel` successors from node `v`, summing keys. Every address is computed from +an answer: the next node is read from memory. -/ +def Nodes.sumFrom (L : Nodes) : ℕ → ℕ → Prog ℕ + | 0, _ => pure 0 + | fuel + 1, v => do + let k ← L.key.get v + let nxt ← L.next.get v + if nxt = 0 then pure k else do + let rest ← L.sumFrom fuel nxt + pure (k + rest) + +/-- Build the list `1 → 2` with keys `5` and `7` (node `0` is reserved as null), then sum it. -/ +def linkedSum : Prog ℕ := do + let L ← Nodes.alloc 3 + L.key.set 1 5 + L.key.set 2 7 + L.next.set 1 2 + L.sumFrom 3 1 + +/-- The empty memory with nothing allocated. -/ +def empty : State := ⟨fun _ => 0, 0⟩ + +example : (spec 8).clientResult empty linkedSum = 12 := by decide + +/-- The history: two zeroed allocations, three writes and four reads by pointer chasing. -/ +example : (spec 8).clientHistory empty linkedSum = + [.alloc 3, .alloc 3, .write 1 5, .write 2 7, .write 4 2, + .read 1, .read 4, .read 2, .read 5] := by decide + +/-- The two zeroed allocations of three cells cost four each; seven unit operations follow. -/ +example : (spec 8).totalCost charge empty ((spec 8).clientHistory empty linkedSum) = 15 := by + decide + +/-- Every operation is admissible at an 8-bit word size. -/ +example : (spec 8).ValidHistory empty ((spec 8).clientHistory empty linkedSum) := by decide + +/-- One scratch block, allocated without clearing, is reused across two rounds. -/ +def reuse : Prog (ℕ × ℕ) := do + let scratch ← allocBlockDirty 1 + scratch.set 0 3 + let first ← scratch.get 0 + scratch.set 0 (first + 4) + let second ← scratch.get 0 + pure (first, second) + +example : (spec 8).clientResult empty reuse = (3, 7) := by decide + +example : ((spec 8).clientState empty reuse).frontier = 1 := by decide + +example : (spec 8).totalCost charge empty ((spec 8).clientHistory empty reuse) = 5 := by decide + +/-- A read above the frontier is rejected. -/ +example : ¬(spec 8).ValidHistory empty [.read 0] := by decide + +/-- A write of a value wider than the word is rejected, even at an allocated address. -/ +example : ¬(spec 8).ValidHistory ⟨fun _ => 0, 1⟩ [.write 0 256] := by decide + +/-- An allocation whose end does not fit the word is rejected. -/ +example : ¬(spec 8).ValidHistory empty [.alloc 256] := by decide + +/-- Well-formedness survives the pointer-chasing program. -/ +example : WellFormed 8 ((spec 8).clientState empty linkedSum) := by + have h : WellFormed 8 empty := ⟨by decide, fun _ => fits_zero 8⟩ + rw [← (spec 8).run_runClient] + exact h.run (by decide) + +/-- The input convention: the length at address `0`, the words from address `1`, and the +frontier just past them. -/ +example : (spec 8).clientResult (State.init [4, 9]) (do + let n ← read 0 + let x ← read 2 + pure (n, x)) = (2, 9) := by decide + +/-- The list view reads the live prefix of a field. -/ +example : (Block.mk 1 3).entries 2 (fun a => a * 10) = [10, 20] := by decide + +end ComplexityTests.DataStructureMemory From 4283b8fb714450e78ba170865bcb54ce8563bce3 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 1 Nov 2026 17:51:55 -0500 Subject: [PATCH 2/9] feat(WordRAM): certify compositional register-word glue Add one framed register-word certificate over existing Code, with visible admissibility and fit envelopes, uniform costs, finite computed-argument substitution, and lazy selection. Keep exact-basis definedness explicit. Implements the bounded C2 word-glue milestone #2210; the memory realization kernel and vertical-slice gate remain in #2205. Validation: final staged tree a1b88e3fd1cc5e72a9a105865df17fa04295710e passed scripts/check.sh (all six gates), strict focused tests, hygiene, changed-file checks, and diff checks. No selected abstract/PDF impact. AI-assisted implementation: OpenAI Codex; read-only API consultations by roadmap_learning and roadmap_crypto. Independent outside review pending. --- Complexity.lean | 1 + Complexity/Computability/WordRAM/Glue.lean | 724 +++++++++++++++++++++ ComplexityTests/WordRAMGlue.lean | 172 +++++ ComplexityTests/WordRAMGlueNamed.lean | 43 ++ 4 files changed, 940 insertions(+) create mode 100644 Complexity/Computability/WordRAM/Glue.lean create mode 100644 ComplexityTests/WordRAMGlue.lean create mode 100644 ComplexityTests/WordRAMGlueNamed.lean diff --git a/Complexity.lean b/Complexity.lean index 7f9a77746d..53856ab81b 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2517,6 +2517,7 @@ public import Complexity.Computability.WordRAM.Dynamic public import Complexity.Computability.WordRAM.ExactNotation public import Complexity.Computability.WordRAM.Function public import Complexity.Computability.WordRAM.GhostLoop +public import Complexity.Computability.WordRAM.Glue public import Complexity.Computability.WordRAM.Heap public import Complexity.Computability.WordRAM.InputArray public import Complexity.Computability.WordRAM.Invariance diff --git a/Complexity/Computability/WordRAM/Glue.lean b/Complexity/Computability/WordRAM/Glue.lean new file mode 100644 index 0000000000..f022c95b6b --- /dev/null +++ b/Complexity/Computability/WordRAM/Glue.lean @@ -0,0 +1,724 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.WordRAM.Structured +import Mathlib.Data.Fintype.EquivFin +import Mathlib.Data.List.FinRange + +/-! +# Compositional certificates for register-word glue + +This module certifies finite, memory-independent glue in the existing `WordRAM.Code` language. +An emitter takes possibly repeated input registers and a disjoint fresh scratch bank. Its code +and instruction budget are chosen before the input values and word width. This is the +emit-and-frame interface used by `Multiword.Circuit`, specialized to physical words; it does not +use that compiler's standard-basis wide-arithmetic semantics for exact-basis operations. + +The admissible-input predicate and one envelope for executed values remain explicit. In +particular, increasing the width does not justify exact subtraction below zero or a zero +divisor. Selection runs only its chosen alternative. Width reads, memory instructions, loops +and random sampling are excluded. This is the word-glue component of realization, not a +compiler for memory clients or algorithms. The certificate asserts successful execution on its +stated domain; it does not assert a converse about executions outside that domain. + +Inputs are already in the supplied registers. Their installation, scratch reservation and a +final halt are not charged here; the surrounding realization must charge them. Constants, +copies, ALU instructions and branch overhead inside the emitted code are charged normally. +The interface and closure results are original; the underlying model is `WordRAM.Structured`. + +## Main definitions + +* `Code.IsGlue`: the memory-independent, width-independent finite fragment of existing code. +* `GlueComputes`: a framed scalar computation with an explicit uniform instruction budget. +* `GlueComputable`: the same contract with only the instruction budget existentially hidden. + +## Main results + +* `GlueComputes.proj`, `GlueComputes.const`: register projections and constants. +* `GlueComputes.binary`, `GlueComputes.comp_many`, `GlueComputes.select`: compositional emission. +* `GlueComputes.realize`: instantiate the emitter with a concrete finite register layout. +* `GlueComputes.mono`: explicit weakening of the value envelope and instruction budget. +-/ + +public section + +namespace Cslib.WordRAM + +variable {B : Basis} {k r : ℕ} + +/-- The register-only finite fragment of `Code`. Conditions may select a branch, but no loop, +memory access, random choice or word-width read is permitted. This is a predicate on the +existing language, not a second program syntax. -/ +@[expose] def Code.IsGlue : Code B r → Prop + | .op (.const _ _) | .op (.copy _ _) => True + | .op (.alu f _ _) => ¬B.ReadsWidth f + | .seq a b | .branch _ a b => a.IsGlue ∧ b.IsGlue + | _ => False + +/-- Register glue does not read the word width, so existing execution monotonicity applies. -/ +theorem Code.IsGlue.not_readsWidth {c : Code B r} (h : c.IsGlue) : ¬c.ReadsWidth := by + induction c with + | op o => cases o <;> simp_all [Code.IsGlue, Code.ReadsWidth, Op.ReadsWidth] + | seq a b ha hb | branch cond a b ha hb => + exact fun hc => hc.elim (ha h.1) (hb h.2) + | loop | rand => exact h.elim + +/-- A scalar register function has a fixed emitter and instruction budget. `bound` is one +top-level value envelope, and `P` is the fixed admissibility predicate. The scratch bank is +fresh and injectively placed; input registers may repeat. Output is in scratch slot zero, +memory is unchanged, and registers outside scratch retain their initial contents. Neither the +emitter nor the budget may depend on run-time values or the word width. -/ +@[expose] def GlueComputes (B : Basis) (P : (Fin k → ℕ) → Prop) + (f bound : (Fin k → ℕ) → ℕ) + (time : ℕ) : Prop := + (∀ v, P v → f v ≤ bound v) ∧ + ∃ n, ∃ emit : ∀ {r : ℕ}, (Fin k → Fin r) → (Fin (n + 1) → Fin r) → Code B r, + ∀ {r : ℕ} (src : Fin k → Fin r) (tmp : Fin (n + 1) → Fin r), + Function.Injective tmp → (∀ i j, src i ≠ tmp j) → + (emit src tmp).IsGlue ∧ + ∀ (w : ℕ) (x : Data r), P (x.regs ∘ src) → Fits w (bound (x.regs ∘ src)) → + ∃ y, ExecWithin w (emit src tmp) x y time ∧ + y.regs (tmp 0) = f (x.regs ∘ src) ∧ y.mem = x.mem ∧ + ∀ i, (∀ j, tmp j ≠ i) → y.regs i = x.regs i + +/-- Syntax-directed automation hides only the uniform budget and emitter witness. The basis, +admissibility predicate, scalar function and value envelope remain visible parameters. -/ +@[expose, fun_prop] +def GlueComputable (B : Basis) (f : (Fin k → ℕ) → ℕ) (P : (Fin k → ℕ) → Prop) + (bound : (Fin k → ℕ) → ℕ) : Prop := + ∃ time, GlueComputes B P f bound time + +namespace GlueComputes + +variable {P : (Fin k → ℕ) → Prop} {f bound bound' : (Fin k → ℕ) → ℕ} {time time' : ℕ} + +/-- A checked explicit budget supplies the automation facade. -/ +theorem computable (h : GlueComputes B P f bound time) : GlueComputable B f P bound := + ⟨time, h⟩ + +/-- A canonical finite register layout puts inputs first and fresh scratch after them. The +same code and register count work for every valid input and width, and every initial memory +is framed. The budget excludes a final halt; a later flat-program export must charge it. -/ +theorem realize (h : GlueComputes B P f bound time) : + ∃ n, ∃ code : Code B (k + (n + 1)), code.IsGlue ∧ + ∀ (w : ℕ) (v : Fin k → ℕ) (mem : ℕ → ℕ), P v → Fits w (bound v) → + ∃ y, ExecWithin w code ⟨Fin.addCases v (fun _ => 0), mem⟩ y time ∧ + y.regs (Fin.natAdd k 0) = f v ∧ y.mem = mem ∧ + ∀ i, y.regs (Fin.castAdd (n + 1) i) = v i := by + obtain ⟨_, n, emit, he⟩ := h + have hi : Function.Injective (Fin.natAdd k : Fin (n + 1) → Fin (k + (n + 1))) := by + intro i j h + apply Fin.ext + have := congrArg Fin.val h + simp only [Fin.val_natAdd] at this + omega + have hd (i : Fin k) (j : Fin (n + 1)) : Fin.castAdd (n + 1) i ≠ Fin.natAdd k j := by + intro h + have := congrArg Fin.val h + simp only [Fin.val_castAdd, Fin.val_natAdd] at this + omega + obtain ⟨hg, hrun⟩ := he (Fin.castAdd (n + 1)) (Fin.natAdd k) hi hd + refine ⟨n, emit (Fin.castAdd (n + 1)) (Fin.natAdd k), hg, ?_⟩ + intro w v mem hv hw + let x : Data (k + (n + 1)) := ⟨Fin.addCases v (fun _ => 0), mem⟩ + have hxs : x.regs ∘ Fin.castAdd (n + 1) = v := by + funext i + change Fin.addCases v (fun _ : Fin (n + 1) => 0) (Fin.castAdd (n + 1) i) = v i + exact Fin.addCases_left i + obtain ⟨y, hy, hyo, hym, hyf⟩ := hrun w x (hxs.symm ▸ hv) (hxs.symm ▸ hw) + refine ⟨y, hy, hxs ▸ hyo, hym, ?_⟩ + intro i + exact (hyf _ (fun j => (hd i j).symm)).trans (congrFun hxs i) + +/-- Weaken the envelope and instruction budget explicitly, outside syntax-directed search. -/ +theorem mono (h : GlueComputes B P f bound time) + (hb : ∀ v, P v → bound v ≤ bound' v) (ht : time ≤ time') : + GlueComputes B P f bound' time' := by + obtain ⟨hf, n, emit, he⟩ := h + refine ⟨fun v hv => (hf v hv).trans (hb v hv), n, emit, ?_⟩ + intro r src tmp hi hd + obtain ⟨hg, hrun⟩ := he src tmp hi hd + refine ⟨hg, ?_⟩ + intro w x hx hw + obtain ⟨y, hy, ho, hm, hf⟩ := hrun w x hx (hw.of_le (hb _ hx)) + exact ⟨y, hy.mono ht, ho, hm, hf⟩ + +/-- Copy one input register. Its bound is checked against the common visible envelope. -/ +theorem proj (i : Fin k) (hb : ∀ v, P v → v i ≤ bound v) : + GlueComputes B P (fun v => v i) bound 1 := by + refine ⟨hb, 0, fun src tmp => .op (.copy (tmp 0) (src i)), ?_⟩ + intro r src tmp hi hd + refine ⟨trivial, ?_⟩ + intro w x hx hw + refine ⟨x.set (tmp 0) (x.regs (src i)), ExecWithin.copy, ?_, rfl, ?_⟩ + · simp [Data.set] + · intro j hj + exact Function.update_of_ne (hj 0).symm _ _ + +/-- Write a fitting constant. -/ +theorem const (z : ℕ) (hb : ∀ v, P v → z ≤ bound v) : + GlueComputes B P (fun _ => z) bound 1 := by + refine ⟨hb, 0, fun _ tmp => .op (.const (tmp 0) z), ?_⟩ + intro r src tmp hi hd + refine ⟨trivial, ?_⟩ + intro w x hx hw + refine ⟨x.set (tmp 0) z, ExecWithin.const (hw.of_le (hb _ hx)), ?_, rfl, ?_⟩ + · simp [Data.set] + · intro j hj + exact Function.update_of_ne (hj 0).symm _ _ + +private def left {a b : ℕ} (j : Fin (a + 1)) : Fin (a + b + 3) := + ⟨j.val + 1, by omega⟩ + +private def right {a b : ℕ} (j : Fin (b + 1)) : Fin (a + b + 3) := + ⟨j.val + a + 2, by omega⟩ + +private theorem left_injective {a b : ℕ} : Function.Injective (@left a b) := by + intro i j h + apply Fin.ext + have := congrArg Fin.val h + simp only [left] at this + omega + +private theorem right_injective {a b : ℕ} : Function.Injective (@right a b) := by + intro i j h + apply Fin.ext + have := congrArg Fin.val h + simp only [right] at this + omega + +private theorem left_ne_right {a b : ℕ} (i : Fin (a + 1)) (j : Fin (b + 1)) : + left i ≠ right j := by + intro h + have := congrArg Fin.val h + simp only [left, right] at this + omega + +/-- Apply a basis operation to two computed words. The operation may repeat or ignore either +word in its argument vector. Its interpretation and domain are checked explicitly, at every +width; no totalization of a partial basis operation is used. Intermediate executions share the +same envelope, and their instruction costs are added without bound search. -/ +theorem binary {f g h : (Fin k → ℕ) → ℕ} {tf tg : ℕ} + (hf : GlueComputes B P f bound tf) (hg : GlueComputes B P g bound tg) + (op : B.Op) (args : Fin (B.Arity op) → Fin 2) (hop : ¬B.ReadsWidth op) + (heval : ∀ v, P v → ∀ w, B.interp w op (fun i => ![f v, g v] (args i)) = some (h v)) + (hb : ∀ v, P v → h v ≤ bound v) : + GlueComputes B P h bound (tf + tg + 1) := by + obtain ⟨_, a, ea, ha⟩ := hf + obtain ⟨_, b, eb, hg⟩ := hg + let emit : ∀ {r : ℕ}, (Fin k → Fin r) → (Fin (a + b + 2 + 1) → Fin r) → Code B r := + fun src tmp => .seq (ea src (tmp ∘ left)) + (.seq (eb src (tmp ∘ right)) + (.op (.alu op (tmp 0) (fun i => if args i = 0 then tmp (left 0) else tmp (right 0))))) + refine ⟨hb, a + b + 2, emit, ?_⟩ + intro r src tmp hi hd + obtain ⟨hga, hra⟩ := ha src (tmp ∘ left) (hi.comp left_injective) + (fun i j => hd i (left j)) + obtain ⟨hgb, hrb⟩ := hg src (tmp ∘ right) (hi.comp right_injective) + (fun i j => hd i (right j)) + refine ⟨⟨hga, hgb, hop⟩, ?_⟩ + intro w x hx hw + obtain ⟨y, hy, hyo, hym, hyf⟩ := hra w x hx hw + have hys : y.regs ∘ src = x.regs ∘ src := by + funext i + exact hyf (src i) (fun j => (hd i (left j)).symm) + obtain ⟨z, hz, hzo, hzm, hzf⟩ := hrb w y (hys.symm ▸ hx) (hys.symm ▸ hw) + have hleft : z.regs (tmp (left 0)) = f (x.regs ∘ src) := + (hzf _ (fun j h => left_ne_right (0 : Fin (a + 1)) j (hi h).symm)).trans hyo + have hright : z.regs (tmp (right 0)) = g (x.regs ∘ src) := by + change z.regs (tmp (right 0)) = g (y.regs ∘ src) at hzo + exact hys ▸ hzo + have hargs : (z.regs ∘ (fun i => if args i = 0 then tmp (left 0) else tmp (right 0))) = + (fun i => ![f (x.regs ∘ src), g (x.regs ∘ src)] (args i)) := by + funext i + by_cases h : args i = 0 + · simp [h, hleft] + · have h' : args i = 1 := by apply Fin.ext; have := (args i).isLt; omega + simp [h', hright] + have he : ExecWithin w (.op (.alu op (tmp 0) + (fun i => if args i = 0 then tmp (left 0) else tmp (right 0)))) z + (z.set (tmp 0) (h (x.regs ∘ src))) 1 := by + apply ExecWithin.alu _ (hw.of_le (hb _ hx)) + rw [hargs] + exact heval _ hx w + refine ⟨z.set (tmp 0) (h (x.regs ∘ src)), hy.seq (hz.seq he), ?_, hzm.trans hym, ?_⟩ + · simp [Data.set] + · intro i hne + change Function.update z.regs (tmp 0) (h (x.regs ∘ src)) i = x.regs i + rw [Function.update_of_ne (hne 0).symm] + exact (hzf i (fun j => hne (right j))).trans (hyf i (fun j => hne (left j))) + +/-- Substitute a register map, including a map with repeated inputs. The emitter accepts +arbitrary input layouts, so this substitution needs no staging copies or injectivity premise. -/ +theorem reindex {m : ℕ} {Q : (Fin m → ℕ) → Prop} {b : (Fin m → ℕ) → ℕ} + (h : GlueComputes B P f bound time) (ρ : Fin k → Fin m) + (hP : ∀ v, Q v → P (v ∘ ρ)) (hb : ∀ v, Q v → bound (v ∘ ρ) ≤ b v) : + GlueComputes B Q (fun v => f (v ∘ ρ)) b time := by + obtain ⟨hf, n, emit, he⟩ := h + refine ⟨fun v hv => (hf _ (hP v hv)).trans (hb v hv), n, + fun src tmp => emit (src ∘ ρ) tmp, ?_⟩ + intro r src tmp hi hd + obtain ⟨hg, hrun⟩ := he (src ∘ ρ) tmp hi (fun i j => hd (ρ i) j) + refine ⟨hg, ?_⟩ + intro w x hx hw + exact hrun w x (hP _ hx) (hw.of_le (hb _ hx)) + +/-- Substitute any finite vector of computed arguments into a routine. All component emitters, +scratch banks and budgets are fixed before runtime inputs or widths. The forest runs in index +order, preserving inputs and earlier results, and then runs the outer routine in its own bank. +The one common envelope covers all components and dominates the outer envelope. -/ +theorem comp_many {m : ℕ} {Q : (Fin m → ℕ) → Prop} {h b : (Fin m → ℕ) → ℕ} + {g : (Fin k → ℕ) → Fin m → ℕ} {tf : ℕ} {t : Fin m → ℕ} + (hf : GlueComputes B Q h b tf) + (hg : ∀ i, GlueComputes B P (fun v => g v i) bound (t i)) + (hQ : ∀ v, P v → Q (g v)) (hb : ∀ v, P v → b (g v) ≤ bound v) : + GlueComputes B P (fun v => h (g v)) bound ((List.ofFn t).sum + tf) := by + classical + obtain ⟨hfo, a, ef, hef⟩ := hf + choose ns es hes using fun i => (hg i).2 + let S := (i : Fin m) × Fin (ns i + 1) + let N := Fintype.card S + let idx : S ≃ Fin N := Fintype.equivFin S + let inner (i : Fin m) (j : Fin (ns i + 1)) : Fin (N + a + 1) := + ⟨a + 1 + (idx ⟨i, j⟩).val, by have := (idx ⟨i, j⟩).isLt; omega⟩ + let outer (j : Fin (a + 1)) : Fin (N + a + 1) := ⟨j.val, by omega⟩ + have hindex {i j : Fin m} {p : Fin (ns i + 1)} {q : Fin (ns j + 1)} + (he : inner i p = inner j q) : (⟨i, p⟩ : S) = ⟨j, q⟩ := by + apply idx.injective + apply Fin.ext + have := congrArg Fin.val he + dsimp only [inner] at this + omega + have hinj (i : Fin m) : Function.Injective (inner i) := by + intro p q he + exact Fin.ext (congrArg (fun s : S => s.2.val) (hindex he)) + have hsep (i j : Fin m) (p : Fin (ns i + 1)) (q : Fin (ns j + 1)) + (he : inner i p = inner j q) : i = j := congrArg Sigma.fst (hindex he) + have hout : Function.Injective outer := by + intro p q he + apply Fin.ext + have hv := congrArg (fun j : Fin (N + a + 1) => j.val) he + exact hv + have hio (i : Fin m) (p : Fin (ns i + 1)) (q : Fin (a + 1)) : + inner i p ≠ outer q := by + intro he + have := congrArg Fin.val he + dsimp only [inner, outer] at this + omega + let emit : ∀ {r : ℕ}, (Fin k → Fin r) → (Fin (N + a + 1) → Fin r) → Code B r := + fun src tmp => (List.finRange m).foldr + (fun i rest => .seq (es i src (tmp ∘ inner i)) rest) + (ef (fun i => tmp (inner i 0)) (tmp ∘ outer)) + refine ⟨fun v hv => (hfo _ (hQ v hv)).trans (hb v hv), N + a, emit, ?_⟩ + intro r src tmp hi hd + have hc (i : Fin m) := hes i src (tmp ∘ inner i) (hi.comp (hinj i)) + (fun j q => hd j (inner i q)) + obtain ⟨hfg, hfrun⟩ := hef (fun i => tmp (inner i 0)) (tmp ∘ outer) + (hi.comp hout) (fun i q he => hio i 0 q (hi he)) + refine ⟨?_, ?_⟩ + · dsimp only [emit] + generalize List.finRange m = L + induction L with + | nil => exact hfg + | cons i L ih => exact ⟨(hc i).1, ih⟩ + intro w x hx hw + let v := x.regs ∘ src + have run (L : List (Fin m)) (z : Data r) (hz : z.regs ∘ src = v) + (hvals : ∀ i, i ∉ L → z.regs (tmp (inner i 0)) = g v i) : + ∃ y, ExecWithin w + (L.foldr (fun i rest => .seq (es i src (tmp ∘ inner i)) rest) + (ef (fun i => tmp (inner i 0)) (tmp ∘ outer))) z y ((L.map t).sum + tf) ∧ + y.regs (tmp 0) = h (g v) ∧ y.mem = z.mem ∧ + ∀ j, (∀ q, tmp q ≠ j) → y.regs j = z.regs j := by + induction L generalizing z with + | nil => + have hargs : z.regs ∘ (fun i => tmp (inner i 0)) = g v := by + funext i + exact hvals i (by simp) + obtain ⟨y, hy, ho, hm, hf⟩ := hfrun w z (hargs.symm ▸ hQ v hx) + (hargs.symm ▸ hw.of_le (hb v hx)) + refine ⟨y, ?_, ?_, hm, ?_⟩ + · simpa only [List.foldr_nil, List.map_nil, List.sum_nil, Nat.zero_add] using hy + · change y.regs (tmp 0) = h (z.regs ∘ (fun i => tmp (inner i 0))) at ho + exact hargs ▸ ho + · intro j hj + exact hf j (fun q => hj (outer q)) + | cons i L ih => + obtain ⟨z', he, ho, hm, hframe⟩ := (hc i).2 w z (hz.symm ▸ hx) (hz.symm ▸ hw) + have hz' : z'.regs ∘ src = v := by + funext j + exact (hframe (src j) (fun q => (hd j (inner i q)).symm)).trans (congrFun hz j) + have hvals' (j : Fin m) (hj : j ∉ L) : z'.regs (tmp (inner j 0)) = g v j := by + by_cases hji : j = i + · subst j + change z'.regs (tmp (inner i 0)) = g (z.regs ∘ src) i at ho + exact hz ▸ ho + · have hreg := hframe (tmp (inner j 0)) + (fun q heq => hji (hsep i j q 0 (hi heq)).symm) + exact hreg.trans (hvals j (by simpa only [List.mem_cons, not_or] using And.intro hji hj)) + obtain ⟨y, hy, hyo, hym, hyf⟩ := ih z' hz' hvals' + refine ⟨y, ?_, hyo, hym.trans hm, ?_⟩ + · simpa only [List.foldr_cons, List.map_cons, List.sum_cons, Nat.add_assoc] using he.seq hy + · intro j hj + exact (hyf j hj).trans (hframe j (fun q => hj (inner i q))) + obtain ⟨y, hy, ho, hm, hf⟩ := run (List.finRange m) x rfl + (fun i hi => False.elim (hi (by simp))) + refine ⟨y, ?_, ho, hm, hf⟩ + simpa only [List.ofFn_eq_map] using hy + +/-- Compose two scalar computations, passing the first result as the second computation's +single input. Each stage keeps its own explicit domain and envelope; the caller proves the +domain implication and envelope domination once. -/ +theorem comp {g b : (Fin 1 → ℕ) → ℕ} {Q : (Fin 1 → ℕ) → Prop} {tf tg : ℕ} + (hf : GlueComputes B P f bound tf) (hg : GlueComputes B Q g b tg) + (hQ : ∀ v, P v → Q (fun _ => f v)) + (hb : ∀ v, P v → b (fun _ => f v) ≤ bound v) : + GlueComputes B P (fun v => g (fun _ => f v)) bound (tf + tg + 1) := by + have hc := hg.comp_many (g := fun v _ => f v) (t := fun _ : Fin 1 => tf) + (fun _ => hf) hQ hb + have hc' : GlueComputes B P (fun v => g (fun _ => f v)) bound (tf + tg) := by + simpa [List.ofFn_succ] using hc + exact hc'.mono (fun _ _ => le_rfl) (by omega) + +/-- Select between two computations by an existing register condition. Only the selected +branch must satisfy its domain; the inactive branch may fault if executed. -/ +theorem select (cond : Cond k) {f g : (Fin k → ℕ) → ℕ} {tf tg : ℕ} + (hf : GlueComputes B (fun v => P v ∧ cond.Holds ⟨v, fun _ => 0⟩) f bound tf) + (hg : GlueComputes B (fun v => P v ∧ ¬cond.Holds ⟨v, fun _ => 0⟩) g bound tg) : + GlueComputes B P (fun v => if cond.Holds ⟨v, fun _ => 0⟩ then f v else g v) + bound (max tf tg + 3) := by + obtain ⟨hfo, a, ea, ha⟩ := hf + obtain ⟨hgo, b, eb, hg⟩ := hg + let emit : ∀ {r : ℕ}, (Fin k → Fin r) → (Fin (a + b + 2 + 1) → Fin r) → Code B r := + fun src tmp => .branch (cond.rename src) + (.seq (ea src (tmp ∘ left)) (.op (.copy (tmp 0) (tmp (left 0))))) + (.seq (eb src (tmp ∘ right)) (.op (.copy (tmp 0) (tmp (right 0))))) + refine ⟨?_, a + b + 2, emit, ?_⟩ + · intro v hv + dsimp only + split + · exact hfo v ⟨hv, by assumption⟩ + · exact hgo v ⟨hv, by assumption⟩ + intro r src tmp hi hd + obtain ⟨hga, hra⟩ := ha src (tmp ∘ left) (hi.comp left_injective) + (fun i j => hd i (left j)) + obtain ⟨hgb, hrb⟩ := hg src (tmp ∘ right) (hi.comp right_injective) + (fun i j => hd i (right j)) + refine ⟨⟨⟨hga, trivial⟩, hgb, trivial⟩, ?_⟩ + intro w x hx hw + have hc : (cond.rename src).Holds x ↔ cond.Holds ⟨x.regs ∘ src, fun _ => 0⟩ := by + cases cond <;> rfl + by_cases h : cond.Holds ⟨x.regs ∘ src, fun _ => 0⟩ + · obtain ⟨y, hy, hyo, hym, hyf⟩ := hra w x ⟨hx, h⟩ hw + refine ⟨y.set (tmp 0) (y.regs (tmp (left 0))), + ((hy.seq ExecWithin.copy).branch_pos (hc.mpr h)).mono (by omega), ?_, hym, ?_⟩ + · simpa [Data.set, h] using hyo + · intro i hne + change Function.update y.regs (tmp 0) _ i = x.regs i + rw [Function.update_of_ne (hne 0).symm] + exact hyf i (fun j => hne (left j)) + · obtain ⟨y, hy, hyo, hym, hyf⟩ := hrb w x ⟨hx, h⟩ hw + refine ⟨y.set (tmp 0) (y.regs (tmp (right 0))), + ((hy.seq ExecWithin.copy).branch_neg (fun h' => h (hc.mp h'))).mono (by omega), + ?_, hym, ?_⟩ + · simpa [Data.set, h] using hyo + · intro i hne + change Function.update y.regs (tmp 0) _ i = x.regs i + rw [Function.update_of_ne (hne 0).symm] + exact hyf i (fun j => hne (right j)) + +/-- Standard binary operations use the basis's documented total natural-number semantics. -/ +theorem bin_standard {f g : (Fin k → ℕ) → ℕ} {tf tg : ℕ} + (hf : GlueComputes .standard P f bound tf) (hg : GlueComputes .standard P g bound tg) + (op : BinOp) (hb : ∀ v, P v → op.eval (f v) (g v) ≤ bound v) : + GlueComputes .standard P (fun v => op.eval (f v) (g v)) bound (tf + tg + 1) := + binary hf hg (.bin op) id (by simp) (fun _ _ _ => rfl) hb + +/-- Exact binary operations require their interpretation to be defined on the fixed domain. +Output fit alone cannot discharge underflow or a zero divisor. -/ +theorem bin_exact {f g : (Fin k → ℕ) → ℕ} {tf tg : ℕ} + (hf : GlueComputes .exact P f bound tf) (hg : GlueComputes .exact P g bound tg) + (op : BinOp) (hv : ∀ v, P v → op.evalExact (f v) (g v) = some (op.eval (f v) (g v))) + (hb : ∀ v, P v → op.eval (f v) (g v) ≤ bound v) : + GlueComputes .exact P (fun v => op.eval (f v) (g v)) bound (tf + tg + 1) := + binary hf hg (.bin op) id (by simp) (fun v hp _ => hv v hp) hb + +end GlueComputes + +namespace GlueComputable + +variable {P : (Fin k → ℕ) → Prop} {bound : (Fin k → ℕ) → ℕ} + +/-- Register projections are found without searching for a budget. -/ +@[fun_prop] +theorem proj (i : Fin k) (hb : ∀ v, P v → v i ≤ bound v) : + GlueComputable B (fun v => v i) P bound := (GlueComputes.proj i hb).computable + +/-- Constants are found without searching for a budget. -/ +@[fun_prop] +theorem const (z : ℕ) (hb : ∀ v, P v → z ≤ bound v) : + GlueComputable B (fun _ => z) P bound := (GlueComputes.const z hb).computable + +variable {f g : (Fin k → ℕ) → ℕ} + +/-- Reuse a named scalar computation after another computation, with explicit domain and +envelope implications. This rule searches for the two functions, never for a budget. -/ +@[fun_prop] +theorem comp {h : ℕ → ℕ} {b : (Fin 1 → ℕ) → ℕ} {Q : (Fin 1 → ℕ) → Prop} + (hf : GlueComputable B f P bound) + (hh : GlueComputable B (fun v => h (v 0)) Q b) + (hQ : ∀ v, P v → Q (fun _ => f v)) + (hb : ∀ v, P v → b (fun _ => f v) ≤ bound v) : + GlueComputable B (fun v => h (f v)) P bound := by + obtain ⟨tf, hf⟩ := hf + obtain ⟨th, hh⟩ := hh + exact (hf.comp hh hQ hb).computable + +/-- Apply an opaque routine to any finite vector of computed local words. The component +budgets are chosen uniformly, before the input/width quantifiers, and then summed explicitly. -/ +@[fun_prop] +theorem comp_many {m : ℕ} {Q : (Fin m → ℕ) → Prop} {h b : (Fin m → ℕ) → ℕ} + {g : (Fin k → ℕ) → Fin m → ℕ} + (hh : GlueComputable B h Q b) + (hg : ∀ i, GlueComputable B (fun v => g v i) P bound) + (hQ : ∀ v, P v → Q (g v)) (hb : ∀ v, P v → b (g v) ≤ bound v) : + GlueComputable B (fun v => h (g v)) P bound := by + classical + obtain ⟨tf, hf⟩ := hh + choose t ht using hg + exact (hf.comp_many ht hQ hb).computable + +/-- Indexing a finite tuple is compile-time routing, so it adds no runtime instruction. -/ +@[fun_prop] +theorem vec_cons {m : ℕ} {g : (Fin k → ℕ) → Fin m → ℕ} + (hf : GlueComputable B f P bound) + (hg : ∀ i, GlueComputable B (fun v => g v i) P bound) (i : Fin (m + 1)) : + GlueComputable B (fun v => Matrix.vecCons (f v) (g v) i) P bound := by + refine Fin.cases ?_ (fun j => ?_) i + · exact hf + · exact hg j + +/-- A singleton tuple has just its computed head; there is no empty-tail obligation. -/ +@[fun_prop] +theorem vec_single (hf : GlueComputable B f P bound) (i : Fin 1) : + GlueComputable B (fun v => ![f v] i) P bound := by + have hi : i = 0 := Subsingleton.elim _ _ + subst i + exact hf + +/-- Register-condition selection retains branch-specific domains. -/ +theorem select (cond : Cond k) + (hf : GlueComputable B f (fun v => P v ∧ cond.Holds ⟨v, fun _ => 0⟩) bound) + (hg : GlueComputable B g (fun v => P v ∧ ¬cond.Holds ⟨v, fun _ => 0⟩) bound) : + GlueComputable B (fun v => if cond.Holds ⟨v, fun _ => 0⟩ then f v else g v) P bound := by + obtain ⟨tf, hf⟩ := hf + obtain ⟨tg, hg⟩ := hg + exact (GlueComputes.select cond hf hg).computable + +/-- Select by equality of input words, without evaluating the unchosen computation. -/ +@[fun_prop] +theorem ite_eq (i j : Fin k) + (hf : GlueComputable B f (fun v => P v ∧ v i = v j) bound) + (hg : GlueComputable B g (fun v => P v ∧ ¬v i = v j) bound) : + GlueComputable B (fun v => if v i = v j then f v else g v) P bound := + select (.eq i j) hf hg + +/-- Select by unsigned comparison of input words. -/ +@[fun_prop] +theorem ite_lt (i j : Fin k) + (hf : GlueComputable B f (fun v => P v ∧ v i < v j) bound) + (hg : GlueComputable B g (fun v => P v ∧ ¬v i < v j) bound) : + GlueComputable B (fun v => if v i < v j then f v else g v) P bound := + select (.lt i j) hf hg + +/-- The standard basis's binary operation rule. -/ +theorem bin_standard (hf : GlueComputable .standard f P bound) + (hg : GlueComputable .standard g P bound) (op : BinOp) + (hb : ∀ v, P v → op.eval (f v) (g v) ≤ bound v) : + GlueComputable .standard (fun v => op.eval (f v) (g v)) P bound := by + obtain ⟨tf, hf⟩ := hf + obtain ⟨tg, hg⟩ := hg + exact (hf.bin_standard hg op hb).computable + +/-- The exact basis's binary operation rule keeps its domain premise explicit. -/ +theorem bin_exact (hf : GlueComputable .exact f P bound) + (hg : GlueComputable .exact g P bound) (op : BinOp) + (hv : ∀ v, P v → op.evalExact (f v) (g v) = some (op.eval (f v) (g v))) + (hb : ∀ v, P v → op.eval (f v) (g v) ≤ bound v) : + GlueComputable .exact (fun v => op.eval (f v) (g v)) P bound := by + obtain ⟨tf, hf⟩ := hf + obtain ⟨tg, hg⟩ := hg + exact (hf.bin_exact hg op hv hb).computable + +/-- Closure under exact-basis `add`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem add (hf : GlueComputable .exact f P bound) + (hg : GlueComputable .exact g P bound) + (hb : ∀ v, P v → f v + g v ≤ bound v) : + GlueComputable .exact (fun v => f v + g v) P bound := + bin_exact hf hg .add (fun _ _ => rfl) hb + +/-- Closure under exact-basis `sub`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem sub (hf : GlueComputable .exact f P bound) + (hg : GlueComputable .exact g P bound) + (hv : ∀ v, P v → g v ≤ f v) + (hb : ∀ v, P v → f v - g v ≤ bound v) : + GlueComputable .exact (fun v => f v - g v) P bound := + bin_exact hf hg .sub (fun v hp => by simp [hv v hp]) hb + +/-- Closure under exact-basis `mul`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem mul (hf : GlueComputable .exact f P bound) + (hg : GlueComputable .exact g P bound) + (hb : ∀ v, P v → f v * g v ≤ bound v) : + GlueComputable .exact (fun v => f v * g v) P bound := + bin_exact hf hg .mul (fun _ _ => rfl) hb + +/-- Closure under exact-basis `div`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem div (hf : GlueComputable .exact f P bound) + (hg : GlueComputable .exact g P bound) + (hv : ∀ v, P v → g v ≠ 0) + (hb : ∀ v, P v → f v / g v ≤ bound v) : + GlueComputable .exact (fun v => f v / g v) P bound := + bin_exact hf hg .div (fun v hp => by simp [hv v hp]) hb + +/-- Closure under exact-basis `mod`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem mod (hf : GlueComputable .exact f P bound) + (hg : GlueComputable .exact g P bound) + (hv : ∀ v, P v → g v ≠ 0) + (hb : ∀ v, P v → f v % g v ≤ bound v) : + GlueComputable .exact (fun v => f v % g v) P bound := + bin_exact hf hg .mod (fun v hp => by simp [hv v hp]) hb + +/-- Closure under exact-basis `and`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem and (hf : GlueComputable .exact f P bound) + (hg : GlueComputable .exact g P bound) + (hb : ∀ v, P v → f v &&& g v ≤ bound v) : + GlueComputable .exact (fun v => f v &&& g v) P bound := + bin_exact hf hg .and (fun _ _ => rfl) hb + +/-- Closure under exact-basis `or`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem or (hf : GlueComputable .exact f P bound) + (hg : GlueComputable .exact g P bound) + (hb : ∀ v, P v → f v ||| g v ≤ bound v) : + GlueComputable .exact (fun v => f v ||| g v) P bound := + bin_exact hf hg .or (fun _ _ => rfl) hb + +/-- Closure under exact-basis `xor`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem xor (hf : GlueComputable .exact f P bound) + (hg : GlueComputable .exact g P bound) + (hb : ∀ v, P v → f v ^^^ g v ≤ bound v) : + GlueComputable .exact (fun v => f v ^^^ g v) P bound := + bin_exact hf hg .xor (fun _ _ => rfl) hb + +/-- Closure under exact-basis `shiftLeft`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem shiftLeft (hf : GlueComputable .exact f P bound) + (hg : GlueComputable .exact g P bound) + (hb : ∀ v, P v → f v <<< g v ≤ bound v) : + GlueComputable .exact (fun v => f v <<< g v) P bound := + bin_exact hf hg .shiftLeft (fun _ _ => rfl) hb + +/-- Closure under exact-basis `shiftRight`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem shiftRight (hf : GlueComputable .exact f P bound) + (hg : GlueComputable .exact g P bound) + (hb : ∀ v, P v → f v >>> g v ≤ bound v) : + GlueComputable .exact (fun v => f v >>> g v) P bound := + bin_exact hf hg .shiftRight (fun _ _ => rfl) hb + +/-- Closure under standard-basis `add`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem add_standard (hf : GlueComputable .standard f P bound) + (hg : GlueComputable .standard g P bound) + (hb : ∀ v, P v → f v + g v ≤ bound v) : + GlueComputable .standard (fun v => f v + g v) P bound := + bin_standard hf hg .add hb + +/-- Closure under standard-basis `sub`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem sub_standard (hf : GlueComputable .standard f P bound) + (hg : GlueComputable .standard g P bound) + (hb : ∀ v, P v → f v - g v ≤ bound v) : + GlueComputable .standard (fun v => f v - g v) P bound := + bin_standard hf hg .sub hb + +/-- Closure under standard-basis `mul`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem mul_standard (hf : GlueComputable .standard f P bound) + (hg : GlueComputable .standard g P bound) + (hb : ∀ v, P v → f v * g v ≤ bound v) : + GlueComputable .standard (fun v => f v * g v) P bound := + bin_standard hf hg .mul hb + +/-- Closure under standard-basis `div`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem div_standard (hf : GlueComputable .standard f P bound) + (hg : GlueComputable .standard g P bound) + (hb : ∀ v, P v → f v / g v ≤ bound v) : + GlueComputable .standard (fun v => f v / g v) P bound := + bin_standard hf hg .div hb + +/-- Closure under standard-basis `mod`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem mod_standard (hf : GlueComputable .standard f P bound) + (hg : GlueComputable .standard g P bound) + (hb : ∀ v, P v → f v % g v ≤ bound v) : + GlueComputable .standard (fun v => f v % g v) P bound := + bin_standard hf hg .mod hb + +/-- Closure under standard-basis `and`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem and_standard (hf : GlueComputable .standard f P bound) + (hg : GlueComputable .standard g P bound) + (hb : ∀ v, P v → f v &&& g v ≤ bound v) : + GlueComputable .standard (fun v => f v &&& g v) P bound := + bin_standard hf hg .and hb + +/-- Closure under standard-basis `or`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem or_standard (hf : GlueComputable .standard f P bound) + (hg : GlueComputable .standard g P bound) + (hb : ∀ v, P v → f v ||| g v ≤ bound v) : + GlueComputable .standard (fun v => f v ||| g v) P bound := + bin_standard hf hg .or hb + +/-- Closure under standard-basis `xor`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem xor_standard (hf : GlueComputable .standard f P bound) + (hg : GlueComputable .standard g P bound) + (hb : ∀ v, P v → f v ^^^ g v ≤ bound v) : + GlueComputable .standard (fun v => f v ^^^ g v) P bound := + bin_standard hf hg .xor hb + +/-- Closure under standard-basis `shiftLeft`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem shiftLeft_standard (hf : GlueComputable .standard f P bound) + (hg : GlueComputable .standard g P bound) + (hb : ∀ v, P v → f v <<< g v ≤ bound v) : + GlueComputable .standard (fun v => f v <<< g v) P bound := + bin_standard hf hg .shiftLeft hb + +/-- Closure under standard-basis `shiftRight`; the common envelope also bounds this result. -/ +@[fun_prop] +theorem shiftRight_standard (hf : GlueComputable .standard f P bound) + (hg : GlueComputable .standard g P bound) + (hb : ∀ v, P v → f v >>> g v ≤ bound v) : + GlueComputable .standard (fun v => f v >>> g v) P bound := + bin_standard hf hg .shiftRight hb + +end GlueComputable + +end Cslib.WordRAM diff --git a/ComplexityTests/WordRAMGlue.lean b/ComplexityTests/WordRAMGlue.lean new file mode 100644 index 0000000000..e1b2663e7a --- /dev/null +++ b/ComplexityTests/WordRAMGlue.lean @@ -0,0 +1,172 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: local-only (tests) + +public import Complexity.Computability.WordRAM.Glue +import ComplexityTests.WordRAMGlueNamed +meta import Mathlib.Tactic.FunProp.Decl + +/-! Concrete word-glue clients. `WordRAMBasis` separately pins the underlying basis semantics. -/ + +public section + +namespace ComplexityTests.WordRAMGlue + +open Cslib.WordRAM + +-- The property must be indexed by the scalar function, not the admissibility predicate. +run_cmd Lean.Elab.Command.liftTermElabM do + let goal ← Lean.Elab.Term.elabTerm (← `(GlueComputable .exact + (fun v : Fin 1 → ℕ => v 0 + 1) (fun v => v 0 ≤ 10) (fun _ => 11))) none + let some decl ← Mathlib.Meta.FunProp.getFunPropDecl? goal + | throwError "GlueComputable was not registered" + unless decl.funArgId == 2 do throwError "wrong GlueComputable function index" + let some f ← Mathlib.Meta.FunProp.getFunPropFun? goal + | throwError "GlueComputable function was not found" + let expected ← Lean.Elab.Term.elabTerm (← `(fun v : Fin 1 → ℕ => v 0 + 1)) none + unless ← Lean.Meta.isDefEq f expected do throwError "indexed P or the bound instead of f" + +-- Costs are explicit and separate from the automation facade: two copies and one addition. +example : GlueComputes .exact (fun v : Fin 2 → ℕ => v 0 + v 1 ≤ 100) + (fun v => v 0 + v 1) (fun _ => 100) 3 := by + apply GlueComputes.bin_exact (GlueComputes.proj 0 ?_) (GlueComputes.proj 1 ?_) .add + · intros; rfl + all_goals intros; (try dsimp [BinOp.eval, Function.comp_def] at *); omega + +-- A larger advertised bound is discharged once, outside fun_prop's rule search. +example : GlueComputes .exact (fun v : Fin 2 → ℕ => v 0 + v 1 ≤ 100) + (fun v => v 0 + v 1) (fun _ => 200) 10 := by + have h : GlueComputes .exact (fun v : Fin 2 → ℕ => v 0 + v 1 ≤ 100) + (fun v => v 0 + v 1) (fun _ => 100) 3 := by + apply GlueComputes.bin_exact (GlueComputes.proj 0 ?_) (GlueComputes.proj 1 ?_) .add + · intros; rfl + all_goals intros; (try dsimp [BinOp.eval, Function.comp_def] at *); omega + exact h.mono (by intros; omega) (by omega) + +-- Ordinary arithmetic closure needs no intermediate machine assertions or cost metavariables. +example : GlueComputable .exact (fun v => (v 0 + v 1) + v 2) + (fun v : Fin 3 → ℕ => v 0 + v 1 + v 2 ≤ 100) + (fun _ => 100) := by + fun_prop (disch := intros; (try dsimp [BinOp.eval, Function.comp_def] at *); omega) + +example : GlueComputable .standard (fun v => v 0 + v 1) + (fun v : Fin 2 → ℕ => v 0 + v 1 ≤ 100) + (fun _ => 100) := by + fun_prop (disch := intros; (try dsimp [BinOp.eval, Function.comp_def] at *); omega) + +-- Exact subtraction uses the domain, rather than totalizing an underflow. +example : GlueComputable .exact (fun v => (v 0 - v 1) / 2) + (fun v : Fin 2 → ℕ => v 1 ≤ v 0 ∧ v 0 ≤ 100) + (fun _ => 100) := by + fun_prop (disch := intros; (try dsimp [BinOp.eval, Function.comp_def] at *); omega) + +-- The nonselected branch is allowed to be invalid on the other branch's input domain. +example : GlueComputable .exact (fun v => if v 0 < v 1 then v 1 - v 0 else v 0 - v 1) + (fun v : Fin 2 → ℕ => v 0 ≤ 100 ∧ v 1 ≤ 100) + (fun _ => 100) := by + fun_prop (disch := intros; (try dsimp [BinOp.eval, Function.comp_def] at *); omega) + +-- At zero, division is not evaluated. The other branch's domain supplies a nonzero divisor. +example : GlueComputable .exact (fun v => if v 0 = v 1 then 0 else 7 / v 0) + (fun v : Fin 2 → ℕ => v 0 ≤ 100 ∧ v 1 = 0) (fun _ => 100) := by + fun_prop (disch := intro v hv; have := Nat.div_le_self 7 (v 0); omega) + +-- Repeated source registers are supported by layout substitution, without injectivity of ρ. +example : GlueComputes .exact (fun v : Fin 1 → ℕ => 2 * v 0 ≤ 100) + (fun v => v 0 + v 0) (fun _ => 100) 3 := by + have h : GlueComputes .exact (fun v : Fin 2 → ℕ => v 0 + v 1 ≤ 100) + (fun v => v 0 + v 1) (fun _ => 100) 3 := by + apply GlueComputes.bin_exact (GlueComputes.proj 0 ?_) (GlueComputes.proj 1 ?_) .add + · intros; rfl + all_goals intros; (try dsimp [BinOp.eval, Function.comp_def] at *); omega + exact h.reindex (fun _ => 0) + (by intros; (try dsimp [BinOp.eval, Function.comp_def] at *); omega) (by intros; rfl) + +-- This function's body is opaque in this importing module. Composition reuses its certificate. +example : GlueComputable .exact (fun v => WordRAMGlueNamed.twice (v 0 + v 1)) + (fun v : Fin 2 → ℕ => 2 * (v 0 + v 1) ≤ 100) + (fun _ => 100) := by + have ht := WordRAMGlueNamed.twice_glue + fun_prop (disch := intros; omega) + +-- Both arguments are computed locals. The outer two-input routine is opaque here; the +-- forest rule must stage both values and preserve the input/frame automatically. +example : GlueComputable .exact + (fun v => WordRAMGlueNamed.weighted ![v 0 + 1, v 1 + v 1]) + (fun v : Fin 2 → ℕ => v 0 + 1 + 4 * v 1 ≤ 100) (fun _ => 100) := by + have hw := WordRAMGlueNamed.weighted_glue + fun_prop (disch := intros; (try dsimp at *); omega) + +example : WordRAMGlueNamed.weighted ![(2 : ℕ) + 1, 3 + 3] = 15 := + WordRAMGlueNamed.weighted_three_six + +-- Empty substitution executes only the outer constant routine, with no staging overhead. +example : GlueComputes .exact (fun _ : Fin 1 → ℕ => True) + (fun _ => 7) (fun _ => 7) 1 := by + have hf : GlueComputes .exact (fun _ : Fin 0 → ℕ => True) + (fun _ => 7) (fun _ => 7) 1 := GlueComputes.const 7 (by intros; rfl) + have hg : ∀ i : Fin 0, GlueComputes .exact (fun _ : Fin 1 → ℕ => True) + (fun _ => Fin.elim0 i) (fun _ => 7) (Fin.elim0 i) := fun i => Fin.elim0 i + exact hf.comp_many hg (by intros; trivial) (by intros; rfl) + +/-- The certificate supplies one actual finite code before the initial memory is chosen. -/ +theorem concrete_code : ∃ n, ∃ code : Code .exact (2 + (n + 1)), code.IsGlue ∧ + ∀ mem : ℕ → ℕ, ∃ y, + ExecWithin 4 code ⟨Fin.addCases ![2, 3] (fun _ => 0), mem⟩ y 3 ∧ + y.regs (Fin.natAdd 2 0) = 5 ∧ y.mem = mem ∧ + y.regs (Fin.castAdd (n + 1) 0) = 2 ∧ y.regs (Fin.castAdd (n + 1) 1) = 3 := by + have h : GlueComputes .exact (fun v : Fin 2 → ℕ => v 0 + v 1 ≤ 10) + (fun v => v 0 + v 1) (fun _ => 10) 3 := by + apply GlueComputes.bin_exact (GlueComputes.proj 0 ?_) (GlueComputes.proj 1 ?_) .add + · intros; rfl + all_goals intros; (try dsimp [BinOp.eval] at *); omega + obtain ⟨n, code, hg, hrun⟩ := h.realize + refine ⟨n, code, hg, ?_⟩ + intro mem + obtain ⟨y, hy, ho, hm, hi⟩ := hrun 4 ![2, 3] mem (by decide) (by decide) + exact ⟨y, hy, ho, hm, hi 0, hi 1⟩ + +-- A zero envelope cannot hide a positive returned word, including at width zero. +example : ¬GlueComputable .exact (fun _ => 1) (fun _ : Fin 0 → ℕ => True) (fun _ => 0) := by + rintro ⟨_, h⟩ + have hh := h.1 Fin.elim0 trivial + exact Nat.not_succ_le_zero 0 hh + +-- Existing Code.eval makes failure independent of fuel exhaustion for this loop-free code. +private def sample (a b : ℕ) : Data 4 := ⟨![a, b, 0, 0], fun _ => 17⟩ + +example : (Code.op (Op.const (B := .exact) (2 : Fin 4) 0)).eval 0 0 (sample 0 0) = + some ((sample 0 0).set 2 0, 1) := rfl + +example : (Code.op (Op.const (B := .exact) (2 : Fin 4) 1)).eval 0 0 (sample 0 0) = + none := by decide + +example : (Code.op (Op.exactBin .sub (2 : Fin 4) 0 1)).eval 4 0 (sample 3 5) = + none := by decide + +example : (Code.op (Op.exactBin .div (2 : Fin 4) 0 1)).eval 4 0 (sample 7 0) = + none := by decide + +example : (Code.op (Op.exactBin .mod (2 : Fin 4) 0 1)).eval 4 0 (sample 7 0) = + none := by decide + +-- Fitting inputs and fitting final mathematical value do not imply intermediate fit. +example : (Code.seq (.op (.exactBin .add (2 : Fin 4) 0 1)) + (.op (.exactBin .sub 2 2 1))).eval 3 0 (sample 7 1) = none := by decide + +-- A lazy branch avoids an exact zero-divisor fault and charges the actual branch overhead. +private def lazyDivide : Code .exact 4 := + .branch (.eq 0 1) (.op (.const 2 0)) (.op (.exactBin .div 2 3 0)) + +example : lazyDivide.eval 3 0 ⟨![0, 0, 0, 7], fun _ => 17⟩ = + some ((⟨![0, 0, 0, 7], fun _ => 17⟩ : Data 4).set 2 0, 2) := rfl + +example : lazyDivide.eval 3 0 ⟨![2, 0, 0, 7], fun _ => 17⟩ = + some ((⟨![2, 0, 0, 7], fun _ => 17⟩ : Data 4).set 2 3, 3) := rfl + +end ComplexityTests.WordRAMGlue diff --git a/ComplexityTests/WordRAMGlueNamed.lean b/ComplexityTests/WordRAMGlueNamed.lean new file mode 100644 index 0000000000..3f09a068d3 --- /dev/null +++ b/ComplexityTests/WordRAMGlueNamed.lean @@ -0,0 +1,43 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: local-only (tests) + +public import Complexity.Computability.WordRAM.Glue + +/-! An imported, unexposed named routine for word-glue composition regressions. -/ + +public section + +namespace ComplexityTests.WordRAMGlueNamed + +open Cslib.WordRAM + +/-- The body is deliberately not exposed to importing clients. -/ +def twice (n : ℕ) : ℕ := n + n + +/-- A named certificate can be reused without unfolding its function. -/ +theorem twice_glue : GlueComputable .exact (fun v => twice (v 0)) + (fun v : Fin 1 → ℕ => 2 * v 0 ≤ 100) (fun _ => 100) := by + unfold twice + fun_prop (disch := intros; omega) + +/-- A two-input routine whose definition is also hidden across this module boundary. -/ +def weighted (v : Fin 2 → ℕ) : ℕ := v 0 + 2 * v 1 + +/-- The fixed domain and envelope make the named routine safe independently of its callers. -/ +theorem weighted_glue : GlueComputable .exact weighted + (fun v => v 0 + 2 * v 1 ≤ 100) (fun _ => 100) := by + unfold weighted + fun_prop (disch := intros; omega) + +/-- A concrete value pins the opaque routine's ordinary natural-number meaning. -/ +theorem weighted_three_six : weighted ![3, 6] = 15 := by + unfold weighted + decide + +end ComplexityTests.WordRAMGlueNamed From 45dd18424e29ae6a3136f0d0944fbc60354f1b44 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 1 Nov 2026 18:22:17 -0500 Subject: [PATCH 3/9] feat(WordRAM): realize memory queries with uniform bind and glue Add one graded certificate over existing Memory.Prog and native Code. Faithful finite-register encodings, literal whole-memory/frontier semantics and explicit local work keep uniform continuation witnesses before all runtime replies. This is the foundational milestone of #2213 under #2205. Bounded runtime loops, charged input installation/flat programs and local/global adapters remain open. No curated abstract or headline scope changes. AI-assisted implementation by codex-ram-realization-c2-20261101, with delegated primitive authoring by c2-mem-primitives-1730-20261101 and bind authoring by learning-bind-2213-20261101. Memory5909 and Glue4283 prerequisites are preserved. --- Complexity.lean | 5 + .../WordRAM/Realization/Basic.lean | 182 +++++++++++++++ .../WordRAM/Realization/Bind.lean | 189 +++++++++++++++ .../WordRAM/Realization/Branch.lean | 129 +++++++++++ .../WordRAM/Realization/Glue.lean | 70 ++++++ .../WordRAM/Realization/Primitive.lean | 206 +++++++++++++++++ ComplexityTests/WordRAMRealizationBind.lean | 61 +++++ ComplexityTests/WordRAMRealizationBranch.lean | 52 +++++ .../WordRAMRealizationPrimitive.lean | 215 ++++++++++++++++++ ROADMAP.md | 10 + UPSTREAM.md | 6 + 11 files changed, 1125 insertions(+) create mode 100644 Complexity/Computability/WordRAM/Realization/Basic.lean create mode 100644 Complexity/Computability/WordRAM/Realization/Bind.lean create mode 100644 Complexity/Computability/WordRAM/Realization/Branch.lean create mode 100644 Complexity/Computability/WordRAM/Realization/Glue.lean create mode 100644 Complexity/Computability/WordRAM/Realization/Primitive.lean create mode 100644 ComplexityTests/WordRAMRealizationBind.lean create mode 100644 ComplexityTests/WordRAMRealizationBranch.lean create mode 100644 ComplexityTests/WordRAMRealizationPrimitive.lean diff --git a/Complexity.lean b/Complexity.lean index b1759ffebf..b58e9959ef 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2556,6 +2556,11 @@ public import Complexity.Computability.WordRAM.Randomized.Law public import Complexity.Computability.WordRAM.Randomized.LoopSegment public import Complexity.Computability.WordRAM.Randomized.Structured public import Complexity.Computability.WordRAM.Randomized.UniformLoopExit +public import Complexity.Computability.WordRAM.Realization.Basic +public import Complexity.Computability.WordRAM.Realization.Bind +public import Complexity.Computability.WordRAM.Realization.Branch +public import Complexity.Computability.WordRAM.Realization.Glue +public import Complexity.Computability.WordRAM.Realization.Primitive public import Complexity.Computability.WordRAM.RegisterFrame public import Complexity.Computability.WordRAM.Sequence public import Complexity.Computability.WordRAM.Signed.Arithmetic diff --git a/Complexity/Computability/WordRAM/Realization/Basic.lean b/Complexity/Computability/WordRAM/Realization/Basic.lean new file mode 100644 index 0000000000..12c4ef7608 --- /dev/null +++ b/Complexity/Computability/WordRAM/Realization/Basic.lean @@ -0,0 +1,182 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.WordRAM.Controller +public import Complexity.Computability.WordRAM.MapOp +public import Complexity.DataStructure.Memory.Spec + +/-! +# Graded realization of memory-oracle clients + +`Realization.Realizes` certifies one uniform native emitter for an existing `Memory.Prog` +family. Arguments and results have explicit faithful finite-register encodings. Its memory +abstraction is the entire memory function together with one frontier register; scratch consists +only of fresh registers. The entry predicate and local-work charge are visible parameters. + +The charged currency adds certified local computation and control work to `Memory.charge`. +In particular, a query-free loop cannot acquire a constant instruction bound merely because its +memory history is empty. The emitter, scratch size and exchange constant precede every runtime +argument, word width and initial memory. `Refines` is a semantic projection of this certificate, +not a competing execution semantics or a second client language. + +## Main definitions + +* `memoryState`: the functional whole-memory/frontier abstraction. +* `memoryCost`: the memory-level charge of the client's actual deterministic history. +* `Realizes`: uniform native realization with a combined instruction currency and register frame. + +## Main results + +* `Realizes.exists_refines`: forget the fresh-register frame to the existing `Refines` API. + +The realization certificate and its grading are original infrastructure. The memory interface, +free-monad interpreter and native execution rules are reused unchanged. +-/ + +@[expose] public section + +namespace Cslib.WordRAM.Realization + +open Cslib.DataStructure + +variable {B : Basis} {r k l : ℕ} {δ α : Type} + +/-- The abstraction retains every cell, including unallocated and inaccessible cells. -/ +def memoryState (frontier : Fin r) (x : Data r) : Memory.State := + ⟨x.mem, x.regs frontier⟩ + +/-- Bounded native data supplies the memory invariant, independently of any scratch layout. -/ +theorem wellFormed_memoryState {w : ℕ} {frontier : Fin r} {x : Data r} (hx : x.Bounded w) : + Memory.WellFormed w (memoryState frontier x) := + ⟨hx.1 frontier, hx.2⟩ + +/-- The memory-level instruction currency uses the existing deterministic interpreter. Its +transition function does not depend on the word width; admissibility is a separate premise. -/ +def memoryCost (p : Memory.Prog α) (s : Memory.State) : ℕ := + (Memory.spec 0).totalCost Memory.charge s ((Memory.spec 0).clientHistory s p) + +/-- Uniformity of the mathematical interpreter across widths: only `valid` depends on `w`. -/ +theorem runClient_width (w : ℕ) (p : Memory.Prog α) (s : Memory.State) : + (Memory.spec w).runClient s p = (Memory.spec 0).runClient s p := by + induction p generalizing s with + | pure a => rfl + | liftBind o cont ih => + exact congrArg (fun t : α × Memory.State × List Memory.Op => (t.1, t.2.1, o :: t.2.2)) + (ih (Memory.step s o).2 (Memory.step s o).1) + +/-- A semantic return issues no memory operation. Its native glue is charged separately. -/ +@[simp] theorem memoryCost_pure (a : α) (s : Memory.State) : + memoryCost (.pure a) s = 0 := rfl + +/-- Memory charges add at the actual intermediate state; the local bind charge is separate. -/ +theorem memoryCost_bind {β : Type} (p : Memory.Prog α) (q : α → Memory.Prog β) + (s : Memory.State) : + memoryCost (p.bind q) s = memoryCost p s + + memoryCost (q ((Memory.spec 0).clientResult s p)) ((Memory.spec 0).clientState s p) := by + unfold memoryCost + simp only [StateTransitionSpec.clientHistory, StateTransitionSpec.runClient_bind] + rw [StateTransitionSpec.totalCost_append, StateTransitionSpec.run_runClient] + +/-- Existing `Memory.Prog` clients have a fixed emitter and a combined charge. The explicit +`safe` predicate may contain glue domains and fit envelopes; it is never existentially chosen. +The existing valid-history premise supplies memory admissibility. The extra one pays uniform +entry/exit overhead, so the native bound is `C * charged + C` with one fixed `C`. + +Input registers may alias each other. The injective scratch bank is disjoint from all inputs and +the frontier; its first `l` registers hold the faithfully encoded result. Every other register, +except the frontier, is framed. All native registers and memory are bounded at entry, separately +from the functional representation. -/ +def Realizes (B : Basis) (p : δ → Memory.Prog α) + (input : δ ↪ (Fin k → ℕ)) (output : α ↪ (Fin l → ℕ)) + (safe : ℕ → δ → Memory.State → Prop) (work : δ → Memory.State → ℕ) : Prop := + ∃ n C : ℕ, + ∃ emit : ∀ {r : ℕ}, (frontier : Fin r) → (Fin k → Fin r) → + (Fin (l + n + 1) → Fin r) → Code B r, + ∀ {r : ℕ} (frontier : Fin r) (src : Fin k → Fin r) + (tmp : Fin (l + n + 1) → Fin r), + Function.Injective tmp → (∀ i j, src i ≠ tmp j) → + (∀ j, tmp j ≠ frontier) → (∀ i, src i ≠ frontier) → + ¬(emit frontier src tmp).ReadsWidth ∧ + ∀ (w : ℕ) (d : δ) (x : Data r), x.Bounded w → x.regs ∘ src = input d → + safe w d (memoryState frontier x) → + (Memory.spec w).ValidHistory (memoryState frontier x) + ((Memory.spec w).clientHistory (memoryState frontier x) (p d)) → + ∃ y, ExecWithin w (emit frontier src tmp) x y + (C * (memoryCost (p d) (memoryState frontier x) + + work d (memoryState frontier x) + 1)) ∧ + memoryState frontier y = (Memory.spec w).clientState (memoryState frontier x) (p d) ∧ + (∀ i : Fin l, y.regs (tmp (Fin.castAdd (n + 1) i)) = + output ((Memory.spec w).clientResult (memoryState frontier x) (p d)) i) ∧ + ∀ i, i ≠ frontier → (∀ j, tmp j ≠ i) → y.regs i = x.regs i + +namespace Realizes + +variable {p : δ → Memory.Prog α} {input : δ ↪ (Fin k → ℕ)} + {output : α ↪ (Fin l → ℕ)} {safe : ℕ → δ → Memory.State → Prop} + {work : δ → Memory.State → ℕ} + +/-- Strengthen the visible entry domain or enlarge the local-work charge. The entry word and +memory bounds may discharge fit conditions; no executable code or domain is hidden by this rule. -/ +theorem consequence {safe' : ℕ → δ → Memory.State → Prop} {work' : δ → Memory.State → ℕ} + (h : Realizes B p input output safe work) + (hsafe : ∀ w d s, (∀ i, Fits w (input d i)) → Memory.WellFormed w s → + safe' w d s → safe w d s) + (hwork : ∀ d s, work d s ≤ work' d s) : Realizes B p input output safe' work' := by + obtain ⟨n, C, emit, he⟩ := h + refine ⟨n, C, emit, ?_⟩ + intro r frontier src tmp hi hd hf hs + obtain ⟨hnw, hrun⟩ := he frontier src tmp hi hd hf hs + refine ⟨hnw, ?_⟩ + intro w d x hx hin hsafe' hv + have hwords (i : Fin k) : Fits w (input d i) := congrFun hin i ▸ hx.1 (src i) + obtain ⟨y, hy, hm, hout, hframe⟩ := + hrun w d x hx hin (hsafe w d _ hwords (wellFormed_memoryState hx) hsafe') hv + exact ⟨y, hy.mono (Nat.mul_le_mul_left C (by have := hwork d (memoryState frontier x); omega)), + hm, hout, hframe⟩ + +/-- Existing defined-evaluation basis simulation preserves the complete realization certificate. -/ +theorem mapSimulates {B' : Basis} (h : Realizes B p input output safe work) + (φ : B.Simulates B') : Realizes B' p input output safe work := by + obtain ⟨n, C, emit, he⟩ := h + refine ⟨n, C, fun frontier src tmp => (emit frontier src tmp).mapSimulates φ, ?_⟩ + intro r frontier src tmp hi hd hf hs + obtain ⟨hnw, hrun⟩ := he frontier src tmp hi hd hf hs + refine ⟨fun h => hnw (Code.readsWidth_of_mapSimulates φ h), ?_⟩ + intro w d x hx hin hsafe hv + obtain ⟨y, hy, hm, hout, hframe⟩ := hrun w d x hx hin hsafe hv + exact ⟨y, hy.mapSimulates φ, hm, hout, hframe⟩ + +/-- The same witness derives the existing semantic `Refines` judgment. The intermediate +representation is fixed by the functional memory abstraction and argument/result registers. -/ +theorem exists_refines (h : Realizes B p input output safe work) : + ∃ n C : ℕ, + ∃ emit : ∀ {r : ℕ}, (frontier : Fin r) → (Fin k → Fin r) → + (Fin (l + n + 1) → Fin r) → Code B r, + ∀ {r : ℕ} (frontier : Fin r) (src : Fin k → Fin r) + (tmp : Fin (l + n + 1) → Fin r), + Function.Injective tmp → (∀ i j, src i ≠ tmp j) → + (∀ j, tmp j ≠ frontier) → (∀ i, src i ≠ frontier) → + ∀ (w : ℕ) (d : δ), + Refines (D := Memory.spec w) w + (fun s x => s = memoryState frontier x ∧ x.Bounded w ∧ x.regs ∘ src = input d ∧ + safe w d s ∧ (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (p d))) + (p d) + (fun a s y => memoryState frontier y = s ∧ + ∀ i : Fin l, y.regs (tmp (Fin.castAdd (n + 1) i)) = output a i) + (fun s _ => C * (memoryCost (p d) s + work d s + 1)) (emit frontier src tmp) := by + obtain ⟨n, C, emit, he⟩ := h + refine ⟨n, C, emit, fun frontier src tmp hi hd hf hs w d => ?_⟩ + apply Refines.ofFn + rintro s x ⟨rfl, hx, hin, hsafe, hv⟩ + obtain ⟨y, hy, hm, hout, _⟩ := (he frontier src tmp hi hd hf hs).2 w d x hx hin hsafe hv + exact ⟨hv, y, hy, hm, hout⟩ + +end Realizes + +end Cslib.WordRAM.Realization diff --git a/Complexity/Computability/WordRAM/Realization/Bind.lean b/Complexity/Computability/WordRAM/Realization/Bind.lean new file mode 100644 index 0000000000..51d75154ea --- /dev/null +++ b/Complexity/Computability/WordRAM/Realization/Bind.lean @@ -0,0 +1,189 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.WordRAM.Realization.Basic +public import Mathlib.Logic.Equiv.Fin.Basic + +/-! +# Uniform sequential realization of memory clients + +The continuation has one realization for the environment paired with its runtime answer. +Its source registers append the first computation's answer slots to the original inputs. +Two disjoint static scratch banks preserve that environment without client-written intermediate +assertions. The continuation's bank already contains the final output slots, so no copy is needed. + +## Main results + +* `Realizes.bind`: sequential realization with additive memory and local-work charges. +-/ + +@[expose] public section + +namespace Cslib.WordRAM.Realization + +open Cslib.DataStructure + +private def bindLeft {m n₂ l n₁ : ℕ} (i : Fin (m + n₂ + 1)) : + Fin (m + (n₂ + l + n₁ + 1) + 1) := ⟨i.val, by omega⟩ + +private def bindRight {m n₂ l n₁ : ℕ} (i : Fin (l + n₁ + 1)) : + Fin (m + (n₂ + l + n₁ + 1) + 1) := ⟨m + n₂ + 1 + i.val, by omega⟩ + +private theorem validHistory_bind {α β : Type} (w : ℕ) (s : Memory.State) + (p : Memory.Prog α) (q : α → Memory.Prog β) : + (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (p.bind q)) ↔ + (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s p) ∧ + (Memory.spec w).ValidHistory ((Memory.spec w).clientState s p) + ((Memory.spec w).clientHistory ((Memory.spec w).clientState s p) + (q ((Memory.spec w).clientResult s p))) := by + have hh : (Memory.spec w).clientHistory s (p.bind q) = + (Memory.spec w).clientHistory s p ++ + (Memory.spec w).clientHistory ((Memory.spec w).clientState s p) + (q ((Memory.spec w).clientResult s p)) := by + simp only [StateTransitionSpec.clientHistory, StateTransitionSpec.clientState, + StateTransitionSpec.clientResult, StateTransitionSpec.runClient_bind] + rw [hh, StateTransitionSpec.validHistory_append, StateTransitionSpec.run_runClient] + +namespace Realizes + +variable {B : Basis} {δ α β : Type} {k l m : ℕ} + {p : δ → Memory.Prog α} {q : δ × α → Memory.Prog β} + {input : δ ↪ (Fin k → ℕ)} {answer : α ↪ (Fin l → ℕ)} + {output : β ↪ (Fin m → ℕ)} + {safeP : ℕ → δ → Memory.State → Prop} {safeQ : ℕ → δ × α → Memory.State → Prop} + {workP : δ → Memory.State → ℕ} {workQ : δ × α → Memory.State → ℕ} + +/-- One uniform continuation emitter consumes the original environment and the first runtime +answer. Its domain and work charge are evaluated at the deterministic intermediate state. +All emitted code, register banks and the exchange constant precede runtime answers. -/ +theorem bind (hP : Realizes B p input answer safeP workP) + (hQ : Realizes B q ((input.prodMap answer).trans (Fin.appendEquiv k l).toEmbedding) + output safeQ workQ) : + Realizes B (fun d => (p d).bind (fun a => q (d, a))) input output + (fun w d s => safeP w d s ∧ + safeQ w (d, (Memory.spec 0).clientResult s (p d)) + ((Memory.spec 0).clientState s (p d))) + (fun d s => workP d s + + workQ (d, (Memory.spec 0).clientResult s (p d)) + ((Memory.spec 0).clientState s (p d)) + 1) := by + obtain ⟨n₁, C₁, emitP, heP⟩ := hP + obtain ⟨n₂, C₂, emitQ, heQ⟩ := hQ + let N := n₂ + l + n₁ + 1 + let C := max C₁ C₂ + let left : Fin (m + n₂ + 1) → Fin (m + N + 1) := bindLeft + let right : Fin (l + n₁ + 1) → Fin (m + N + 1) := bindRight + let emit : ∀ {r : ℕ}, (frontier : Fin r) → (Fin k → Fin r) → + (Fin (m + N + 1) → Fin r) → Code B r := fun frontier src tmp => + .seq (emitP frontier src (tmp ∘ right)) + (emitQ frontier + (Fin.append src (fun i => tmp (right (Fin.castAdd (n₁ + 1) i)))) (tmp ∘ left)) + refine ⟨N, C, emit, ?_⟩ + intro r frontier src tmp hi hd hf hs + have hleft : Function.Injective (tmp ∘ left) := by + intro a b hab + apply Fin.ext + have h := congrArg Fin.val (hi hab) + exact h + have hright : Function.Injective (tmp ∘ right) := by + intro a b hab + apply Fin.ext + have := congrArg Fin.val (hi hab) + change m + n₂ + 1 + a.val = m + n₂ + 1 + b.val at this + omega + have hdisjoint (a : Fin (l + n₁ + 1)) (b : Fin (m + n₂ + 1)) : + tmp (right a) ≠ tmp (left b) := by + intro hab + have := congrArg Fin.val (hi hab) + change m + n₂ + 1 + a.val = b.val at this + omega + let nextSrc : Fin (k + l) → Fin r := + Fin.append src (fun i => tmp (right (Fin.castAdd (n₁ + 1) i))) + have hnextDisjoint (i : Fin (k + l)) (j : Fin (m + n₂ + 1)) : + nextSrc i ≠ (tmp ∘ left) j := by + refine Fin.addCases (fun a => ?_) (fun b => ?_) i + · simpa only [nextSrc, Fin.append_left, Function.comp_apply] using hd a (left j) + · simpa only [nextSrc, Fin.append_right, Function.comp_apply] using + hdisjoint (Fin.castAdd (n₁ + 1) b) j + have hnextFrontier (i : Fin (k + l)) : nextSrc i ≠ frontier := by + refine Fin.addCases (fun a => ?_) (fun b => ?_) i + · simpa only [nextSrc, Fin.append_left] using hs a + · simpa only [nextSrc, Fin.append_right] using hf (right (Fin.castAdd (n₁ + 1) b)) + obtain ⟨hnwP, hrunP⟩ := heP frontier src (tmp ∘ right) hright + (fun i j => hd i (right j)) (fun j => hf (right j)) hs + obtain ⟨hnwQ, hrunQ⟩ := heQ frontier nextSrc (tmp ∘ left) hleft hnextDisjoint + (fun j => hf (left j)) hnextFrontier + refine ⟨fun h => h.elim hnwP hnwQ, ?_⟩ + intro w d x hx hin hsafe hv + let s := memoryState frontier x + let a := (Memory.spec 0).clientResult s (p d) + let s' := (Memory.spec 0).clientState s (p d) + have hresult : (Memory.spec w).clientResult s (p d) = a := + congrArg Prod.fst (runClient_width w (p d) s) + have hstate : (Memory.spec w).clientState s (p d) = s' := + congrArg (fun z => z.2.1) (runClient_width w (p d) s) + obtain ⟨hvP, hvQ⟩ := (validHistory_bind w s (p d) (fun a => q (d, a))).mp hv + obtain ⟨z, hz, hmP, houtP, hframeP⟩ := hrunP w d x hx hin hsafe.1 hvP + change memoryState frontier z = (Memory.spec w).clientState s (p d) at hmP + rw [hstate] at hmP + change ∀ i : Fin l, z.regs ((tmp ∘ right) (Fin.castAdd (n₁ + 1) i)) = + answer ((Memory.spec w).clientResult s (p d)) i at houtP + rw [hresult] at houtP + have hinQ : z.regs ∘ nextSrc = + ((input.prodMap answer).trans (Fin.appendEquiv k l).toEmbedding) (d, a) := by + funext i + refine Fin.addCases (fun j => ?_) (fun j => ?_) i + · change z.regs (nextSrc (Fin.castAdd l j)) = + Fin.append (input d) (answer a) (Fin.castAdd l j) + simp only [nextSrc, Fin.append_left] + exact (hframeP (src j) (hs j) (fun t => (hd j (right t)).symm)).trans (congrFun hin j) + · change z.regs (nextSrc (Fin.natAdd k j)) = + Fin.append (input d) (answer a) (Fin.natAdd k j) + simpa only [nextSrc, Fin.append_right, Function.comp_apply] using houtP j + have hsafeQ : safeQ w (d, a) (memoryState frontier z) := by + rw [hmP] + exact hsafe.2 + have hvalidQ : (Memory.spec w).ValidHistory (memoryState frontier z) + ((Memory.spec w).clientHistory (memoryState frontier z) (q (d, a))) := by + rw [hmP] + simpa only [hstate, hresult] using hvQ + obtain ⟨y, hy, hmQ, houtQ, hframeQ⟩ := + hrunQ w (d, a) z (hz.bounded hx) hinQ hsafeQ hvalidQ + refine ⟨y, (hz.seq hy).mono ?_, ?_, ?_, ?_⟩ + · change C₁ * (memoryCost (p d) s + workP d s + 1) + + C₂ * (memoryCost (q (d, a)) (memoryState frontier z) + + workQ (d, a) (memoryState frontier z) + 1) ≤ + C * (memoryCost ((p d).bind (fun a => q (d, a))) s + + (workP d s + workQ (d, a) s' + 1) + 1) + rw [hmP, memoryCost_bind] + calc + _ ≤ C * (memoryCost (p d) s + workP d s + 1) + + C * (memoryCost (q (d, a)) s' + workQ (d, a) s' + 1) := + Nat.add_le_add (Nat.mul_le_mul_right _ (Nat.le_max_left _ _)) + (Nat.mul_le_mul_right _ (Nat.le_max_right _ _)) + _ = _ := by + rw [← Nat.mul_add] + congr 1 + dsimp only [a, s'] + omega + · rw [hmP] at hmQ + exact hmQ.trans (by + simp only [StateTransitionSpec.clientState, StateTransitionSpec.runClient_bind] + rw [runClient_width w (p d) s]) + · intro i + have hslot : left (Fin.castAdd (n₂ + 1) i) = Fin.castAdd (N + 1) i := rfl + rw [hmP] at houtQ + simpa only [hslot, Function.comp_apply, StateTransitionSpec.clientResult, + StateTransitionSpec.runClient_bind, runClient_width] using houtQ i + · intro i hif htmp + exact (hframeQ i hif (fun j => htmp (left j))).trans + (hframeP i hif (fun j => htmp (right j))) + +end Realizes + +end Cslib.WordRAM.Realization diff --git a/Complexity/Computability/WordRAM/Realization/Branch.lean b/Complexity/Computability/WordRAM/Realization/Branch.lean new file mode 100644 index 0000000000..3d55738f1e --- /dev/null +++ b/Complexity/Computability/WordRAM/Realization/Branch.lean @@ -0,0 +1,129 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.WordRAM.Realization.Basic + +/-! +# Native branching in memory-client realizations + +The branch test reads only the encoded live words. Both alternatives have uniform emitters; +only the selected alternative's domain, fit obligations and local work are required at runtime. +The two-instruction allowance includes the jump on the negative path. + +## Main definitions + +* `test`: interpret an existing native condition on a word-vector environment. + +## Main results + +* `Realizes.branch`: compose two realizations using an actual native conditional. +-/ + +@[expose] public section + +namespace Cslib.WordRAM.Realization + +open Cslib.DataStructure + +variable {B : Basis} {δ α : Type} {k l : ℕ} + +/-- The existing native condition observes the encoded words, without inspecting memory. -/ +def test (c : Cond k) (v : Fin k → ℕ) : Prop := c.Holds ⟨v, fun _ => 0⟩ + +instance (c : Cond k) (v : Fin k → ℕ) : Decidable (test c v) := by + unfold test + infer_instance + +private theorem test_rename {r : ℕ} (c : Cond k) (src : Fin k → Fin r) + (x : Data r) (v : Fin k → ℕ) (h : x.regs ∘ src = v) : + (c.rename src).Holds x ↔ test c v := by + cases c <;> simp only [Cond.rename, Cond.Holds, test] <;> + simp only [← h, Function.comp_apply] + +namespace Realizes + +/-- Both branch emitters precede all runtime values. Shared result slots and disjointness from +live inputs are synthesized internally; the entry domain and work charge select the actual path. -/ +theorem branch {pos neg : δ → Memory.Prog α} + {input : δ ↪ (Fin k → ℕ)} {output : α ↪ (Fin l → ℕ)} + {safePos safeNeg : ℕ → δ → Memory.State → Prop} + {workPos workNeg : δ → Memory.State → ℕ} (c : Cond k) + (hp : Realizes B pos input output safePos workPos) + (hn : Realizes B neg input output safeNeg workNeg) : + Realizes B (fun d => if test c (input d) then pos d else neg d) input output + (fun w d s => if test c (input d) then safePos w d s else safeNeg w d s) + (fun d s => (if test c (input d) then workPos d s else workNeg d s) + 2) := by + obtain ⟨np, Cp, ep, hep⟩ := hp + obtain ⟨nn, Cn, en, hen⟩ := hn + let ip : Fin (l + np + 1) → Fin (l + (np + nn) + 1) := Fin.castLE (by omega) + let ineg : Fin (l + nn + 1) → Fin (l + (np + nn) + 1) := Fin.castLE (by omega) + refine ⟨np + nn, max Cp Cn + 2, fun frontier src tmp => + .branch (c.rename src) (ep frontier src (tmp ∘ ip)) + (en frontier src (tmp ∘ ineg)), ?_⟩ + intro r frontier src tmp hi hd hf hs + have hip : Function.Injective (tmp ∘ ip) := by + intro a b hab + apply Fin.ext + exact congrArg (fun z : Fin (l + (np + nn) + 1) => z.val) (hi hab) + have hin : Function.Injective (tmp ∘ ineg) := by + intro a b hab + apply Fin.ext + exact congrArg (fun z : Fin (l + (np + nn) + 1) => z.val) (hi hab) + obtain ⟨hnp, hrp⟩ := hep frontier src (tmp ∘ ip) hip + (fun i j => hd i (ip j)) (fun j => hf (ip j)) hs + obtain ⟨hnn, hrn⟩ := hen frontier src (tmp ∘ ineg) hin + (fun i j => hd i (ineg j)) (fun j => hf (ineg j)) hs + refine ⟨fun h => h.elim hnp hnn, ?_⟩ + intro w d x hx hin hsafe hv + have hc := test_rename c src x (input d) hin + by_cases ht : test c (input d) + · simp only [ite_eq_left ht] at hsafe hv ⊢ + obtain ⟨y, hy, hm, hout, hframe⟩ := hrp w d x hx hin hsafe hv + refine ⟨y, (hy.branch_pos (hc.mpr ht)).mono ?_, hm, ?_, ?_⟩ + · have hC : Cp ≤ max Cp Cn + 2 := by omega + have hmul := Nat.mul_le_mul_right + (memoryCost (pos d) (memoryState frontier x) + workPos d (memoryState frontier x) + 1) hC + calc + _ ≤ (max Cp Cn + 2) * + (memoryCost (pos d) (memoryState frontier x) + + workPos d (memoryState frontier x) + 1) + 2 := by omega + _ ≤ (max Cp Cn + 2) * + (memoryCost (pos d) (memoryState frontier x) + workPos d (memoryState frontier x) + 1) + + (max Cp Cn + 2) * 2 := by omega + _ = _ := by ring + · intro i + have heq : Fin.castAdd (np + nn + 1) i = ip (Fin.castAdd (np + 1) i) := Fin.ext rfl + rw [heq] + exact hout i + · intro i hif htmp + exact hframe i hif (fun j => htmp (ip j)) + · simp only [ite_eq_right ht] at hsafe hv ⊢ + obtain ⟨y, hy, hm, hout, hframe⟩ := hrn w d x hx hin hsafe hv + refine ⟨y, (hy.branch_neg (fun h => ht (hc.mp h))).mono ?_, hm, ?_, ?_⟩ + · have hC : Cn ≤ max Cp Cn + 2 := by omega + have hmul := Nat.mul_le_mul_right + (memoryCost (neg d) (memoryState frontier x) + workNeg d (memoryState frontier x) + 1) hC + calc + _ ≤ (max Cp Cn + 2) * + (memoryCost (neg d) (memoryState frontier x) + + workNeg d (memoryState frontier x) + 1) + 2 := by omega + _ ≤ (max Cp Cn + 2) * + (memoryCost (neg d) (memoryState frontier x) + workNeg d (memoryState frontier x) + 1) + + (max Cp Cn + 2) * 2 := by omega + _ = _ := by ring + · intro i + have heq : Fin.castAdd (np + nn + 1) i = ineg (Fin.castAdd (nn + 1) i) := Fin.ext rfl + rw [heq] + exact hout i + · intro i hif htmp + exact hframe i hif (fun j => htmp (ineg j)) + +end Realizes + +end Cslib.WordRAM.Realization diff --git a/Complexity/Computability/WordRAM/Realization/Glue.lean b/Complexity/Computability/WordRAM/Realization/Glue.lean new file mode 100644 index 0000000000..faac0fa3e3 --- /dev/null +++ b/Complexity/Computability/WordRAM/Realization/Glue.lean @@ -0,0 +1,70 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.WordRAM.Realization.Basic +public import Complexity.Computability.WordRAM.Glue + +/-! +# Certified local computation in memory clients + +The source computation is an ordinary `pure` in `Memory.Prog`, but its native cost is the +certified word-glue budget. The input domain and top-level fit envelope remain visible. +Uniform emitter witnesses are chosen before the runtime environment, width or memory, including +when this rule supplies the continuation of a previous memory read. + +## Main results + +* `Realizes.glue`: reuse a `GlueComputes` emitter, preserving the entire memory and frontier. +-/ + +@[expose] public section + +namespace Cslib.WordRAM.Realization.Realizes + +open Cslib.DataStructure + +variable {B : Basis} {δ : Type} {k : ℕ} {P : (Fin k → ℕ) → Prop} + {f bound : (Fin k → ℕ) → ℕ} {time : ℕ} + +private def glueSlot {n : ℕ} (j : Fin (n + 1)) : Fin (1 + n + 1) := ⟨j.val, by omega⟩ + +/-- Certified scalar computation returns its word, frames memory/frontier/live registers, and +charges its instruction budget even though its source memory-operation history is empty. -/ +theorem glue (input : δ ↪ (Fin k → ℕ)) (h : GlueComputes B P f bound time) : + Realizes B (fun d => pure (f (input d))) input + (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding + (fun w d _ => P (input d) ∧ Fits w (bound (input d))) (fun _ _ => time) := by + obtain ⟨_, n, emit, he⟩ := h + refine ⟨n, 1, fun _ src tmp => emit src (fun j => tmp (glueSlot j)), ?_⟩ + intro r frontier src tmp hi hd hf hs + have htmp : Function.Injective (fun j : Fin (n + 1) => tmp (glueSlot j)) := by + intro a b h + apply Fin.ext + exact congrArg (fun z : Fin (1 + n + 1) => z.val) (hi h) + obtain ⟨hg, hrun⟩ := he src (fun j => tmp (glueSlot j)) htmp + (fun i j => hd i (glueSlot j)) + refine ⟨hg.not_readsWidth, ?_⟩ + intro w d x hx hin hsafe hv + obtain ⟨y, hy, hout, hm, hframe⟩ := hrun w x (hin.symm ▸ hsafe.1) (hin.symm ▸ hsafe.2) + refine ⟨y, hy.mono (by change time ≤ 1 * (0 + time + 1); omega), ?_, ?_, ?_⟩ + · apply Memory.State.ext + · exact hm + · exact hframe frontier (fun j => hf (glueSlot j)) + · intro i + have hi : i = 0 := Fin.eq_zero i + subst i + change y.regs (tmp 0) = f (input d) + have hzero : glueSlot (0 : Fin (n + 1)) = 0 := by + apply Fin.ext + simp [glueSlot] + simpa only [hzero, hin] using hout + · intro i hif htmp + exact hframe i (fun j => htmp (glueSlot j)) + +end Cslib.WordRAM.Realization.Realizes diff --git a/Complexity/Computability/WordRAM/Realization/Primitive.lean b/Complexity/Computability/WordRAM/Realization/Primitive.lean new file mode 100644 index 0000000000..cc15b5c64c --- /dev/null +++ b/Complexity/Computability/WordRAM/Realization/Primitive.lean @@ -0,0 +1,206 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.WordRAM.Realization.Basic +public import Complexity.Computability.WordRAM.Subroutine + +/-! +# Native memory-query realizations + +The native query arguments are already in the caller's live register environment. Loads and +stores reuse the basis-generic execution rules. Allocation uses exact arithmetic and the +existing generic zero-fill subroutine; it changes the full memory abstraction exactly as the +memory oracle specifies. Argument computation, binds and the final halt are charged by the +surrounding realization rules rather than hidden in these primitives. + +## Main results + +* `Realizes.read`, `Realizes.write`: one-instruction memory operations with live-register frames. +* `Realizes.allocDirty`: exact two-instruction bump allocation, including zero-width empty blocks. +* `Realizes.alloc`: zeroed allocation via the existing basis-generic zero-fill code. +-/ + +@[expose] public section + +namespace Cslib.WordRAM.Realization.Realizes + +open Cslib.DataStructure + +variable {B : Basis} {δ : Type} {k : ℕ} + +local notation "word" => Equiv.toEmbedding (Equiv.symm (Equiv.funUnique (Fin 1) ℕ)) +local notation "unitWords" => Equiv.toEmbedding (Equiv.ofUnique Unit (Fin 0 → ℕ)) + +/-- A read returns a word without changing the frontier or any memory cell. Its address is a +live word; memory admissibility additionally states that the address is allocated. -/ +theorem read (input : δ ↪ (Fin k → ℕ)) (i : Fin k) : + Realizes B (fun d => Memory.read (input d i)) input word + (fun _ _ _ => True) (fun _ _ => 0) := by + refine ⟨0, 1, fun _ src tmp => .op (.load (tmp 0) (src i)), ?_⟩ + intro r frontier src tmp hi hd hf hs + refine ⟨by simp [Code.ReadsWidth, Op.ReadsWidth], ?_⟩ + intro w d x hx hin hsafe hv + have harg : x.regs (src i) = input d i := congrFun hin i + let y := x.set (tmp 0) (x.mem (input d i)) + refine ⟨y, ?_, ?_, ?_, ?_⟩ + · have he := ExecWithin.load (B := B) (w := w) (d := tmp 0) (a := src i) (x := x) + rw [harg] at he + exact he.mono (by change 1 ≤ 1 * (1 + 0 + 1); omega) + · apply Memory.State.ext + · rfl + · change (x.set (tmp 0) _).regs frontier = x.regs frontier + simp [Data.set, Function.update_of_ne (hf 0).symm] + · intro j + have hj : j = 0 := Fin.eq_zero j + subst j + change (x.set (tmp 0) _).regs (tmp 0) = x.mem (input d i) + simp [Data.set] + · intro j hj htmp + exact Function.update_of_ne (htmp 0).symm _ _ + +/-- A store returns unit, updates precisely the selected memory cell and preserves all registers. +The value and allocated-address hypotheses remain in the existing memory valid-history premise. -/ +theorem write (input : δ ↪ (Fin k → ℕ)) (i j : Fin k) : + Realizes B (fun d => Memory.write (input d i) (input d j)) input unitWords + (fun _ _ _ => True) (fun _ _ => 0) := by + refine ⟨0, 1, fun _ src _ => .op (.store (src i) (src j)), ?_⟩ + intro r frontier src tmp hi hd hf hs + refine ⟨by simp [Code.ReadsWidth, Op.ReadsWidth], ?_⟩ + intro w d x hx hin hsafe hv + have hi' : x.regs (src i) = input d i := congrFun hin i + have hj' : x.regs (src j) = input d j := congrFun hin j + let y := x.write (input d i) (input d j) + refine ⟨y, ?_, ?_, ?_, fun _ _ _ => rfl⟩ + · have he := ExecWithin.store (B := B) (w := w) (a := src i) (s := src j) (x := x) + rw [hi', hj'] at he + exact he.mono (by change 1 ≤ 1 * (1 + 0 + 1); omega) + · rfl + · exact fun i => Fin.elim0 i + +/-- Dirty allocation returns the old frontier and adds the count exactly, without touching memory. +No constant `1` is materialized, so a zero-width empty allocation is included. -/ +theorem allocDirty (input : δ ↪ (Fin k → ℕ)) (i : Fin k) : + Realizes .exact (fun d => Memory.allocDirty (input d i)) input word + (fun _ _ _ => True) (fun _ _ => 0) := by + refine ⟨0, 1, fun frontier src tmp => + .seq (.op (.copy (tmp 0) frontier)) (.op (.exactBin .add frontier frontier (src i))), ?_⟩ + intro r frontier src tmp hi hd hf hs + refine ⟨by simp [Code.ReadsWidth, Op.ReadsWidth, Op.exactBin, Basis.exact], ?_⟩ + intro w d x hx hin hsafe hv + have harg : x.regs (src i) = input d i := congrFun hin i + have hfit : Fits w (x.regs frontier + input d i) := hv.1 + let a := x.set (tmp 0) (x.regs frontier) + let y := a.set frontier (x.regs frontier + input d i) + have ha : a.regs frontier = x.regs frontier := + Function.update_of_ne (hf 0).symm _ _ + have hai : a.regs (src i) = input d i := + (Function.update_of_ne (hd i 0) _ _).trans harg + have hcopy : ExecWithin (B := .exact) w (.op (.copy (tmp 0) frontier)) x a 1 := + ExecWithin.copy + have hadd : ExecWithin w (.op (.exactBin .add frontier frontier (src i))) a y 1 := by + apply ExecWithin.op + rw [Op.eval_exactBin, ha, hai] + exact Data.put_of_fits hfit + refine ⟨y, (hcopy.seq hadd).mono (by change 1 + 1 ≤ 1 * (1 + 0 + 1); omega), ?_, ?_, ?_⟩ + · apply Memory.State.ext + · rfl + · change (a.set frontier _).regs frontier = x.regs frontier + input d i + simp [Data.set] + · intro j + have hj : j = 0 := Fin.eq_zero j + subst j + change y.regs (tmp 0) = x.regs frontier + simp [y, a, Data.set, Function.update_of_ne (hf 0)] + · intro j hj htmp + simp [y, a, Data.set, Function.update_of_ne hj, + Function.update_of_ne (htmp 0).symm] + +private def clearPackage {r : ℕ} (frontier base cur zero one : Fin r) : + SubroutineCode .exact r 0 where + allocSpan := .op (.copy base base) + initSetup := .op (.copy base base) + code := .op (.copy base base) + frontierReg := frontier + baseReg := base + initParams := Fin.elim0 + curReg := cur + zeroReg := zero + oneReg := one + incCur := .exactBin .add cur cur one + input := fun _ => false + output := base + +/-- Zeroed allocation realizes the full oracle memory update on arbitrary old scratch contents. +The reused clear code materializes `1` only in the positive-size branch. -/ +theorem alloc (input : δ ↪ (Fin k → ℕ)) (i : Fin k) : + Realizes .exact (fun d => Memory.alloc (input d i)) input word + (fun _ _ _ => True) (fun _ _ => 0) := by + refine ⟨2, 4, fun frontier src tmp => + .seq (.op (.copy (tmp 0) frontier)) <| + .seq (.op (.exactBin .add frontier frontier (src i))) + (clearPackage frontier (tmp 0) (tmp 1) (tmp 2) (tmp 3)).zeroFillCode, ?_⟩ + intro r frontier src tmp hi hd hf hs + refine ⟨by simp [Code.ReadsWidth, Op.ReadsWidth, Op.exactBin, Basis.exact, + clearPackage, SubroutineCode.zeroFillCode], ?_⟩ + intro w d x hx hin hsafe hv + have harg : x.regs (src i) = input d i := congrFun hin i + have hfit : Fits w (x.regs frontier + input d i) := hv.1 + let a := x.set (tmp 0) (x.regs frontier) + let b := a.set frontier (x.regs frontier + input d i) + let P := clearPackage frontier (tmp 0) (tmp 1) (tmp 2) (tmp 3) + have ha : a.regs frontier = x.regs frontier := Function.update_of_ne (hf 0).symm _ _ + have hai : a.regs (src i) = input d i := + (Function.update_of_ne (hd i 0) _ _).trans harg + have hcopy : ExecWithin (B := .exact) w (.op (.copy (tmp 0) frontier)) x a 1 := + ExecWithin.copy + have hadd : ExecWithin w (.op (.exactBin .add frontier frontier (src i))) a b 1 := by + apply ExecWithin.op + rw [Op.eval_exactBin, ha, hai] + exact Data.put_of_fits hfit + have hclear : [P.curReg, P.zeroReg, P.oneReg, P.baseReg, P.frontierReg].Nodup := by + simp [P, clearPackage, hi.eq_iff, hf] + have hinc {z : Data r} (hz : z.regs P.oneReg = 1) (hfit : Fits w (z.regs P.curReg + 1)) : + P.incCur.eval w z = some (z.set P.curReg (z.regs P.curReg + 1)) := by + change z.regs (tmp 3) = 1 at hz + change Fits w (z.regs (tmp 1) + 1) at hfit + change (Op.exactBin .add (tmp 1) (tmp 1) (tmp 3)).eval w z = + some (z.set (tmp 1) (z.regs (tmp 1) + 1)) + rw [Op.eval_exactBin, hz] + exact Data.put_of_fits hfit + have hbbase : b.regs P.baseReg = x.regs frontier := by + simp [P, clearPackage, b, a, Data.set, Function.update_of_ne (hf 0)] + have hbfront : b.regs P.frontierReg = x.regs frontier + input d i := by + simp [P, clearPackage, b, Data.set] + obtain ⟨y, hy, hby, hbase, hfront, _, hzero, hmod⟩ := + P.zeroFillCode_exec (params := Fin.elim0) hclear (fun j => Fin.elim0 j) hinc + ((hcopy.seq hadd).bounded hx) + hbbase hbfront (fun j => Fin.elim0 j) + have hmem : y.mem = clear x.mem (x.regs frontier) (input d i) := by + funext addr + by_cases ha : (Block.mk (x.regs frontier) (input d i)).Owns addr + · rw [clear_of_owns ha] + exact hzero addr (Block.mem_footprint.mpr ha) + · rw [clear_of_not_owns ha] + exact hmod addr (fun h => ha (Block.mem_footprint.mp h)) + have hwhole := hcopy.seq (hadd.seq hy) + refine ⟨y, hwhole.mono (by change 1 + (1 + (4 * input d i + 6)) ≤ + 4 * ((input d i + 1) + 0 + 1); omega), ?_, ?_, ?_⟩ + · apply Memory.State.ext + · exact hmem + · exact hfront + · intro j + have hj : j = 0 := Fin.eq_zero j + subst j + exact hbase + · intro j hj htmp + apply hwhole.regs_eq + simp [Code.Preserves, Op.dest, Op.exactBin, P, clearPackage, + SubroutineCode.zeroFillCode, Ne.symm hj, htmp] + +end Cslib.WordRAM.Realization.Realizes diff --git a/ComplexityTests/WordRAMRealizationBind.lean b/ComplexityTests/WordRAMRealizationBind.lean new file mode 100644 index 0000000000..8667ae3a17 --- /dev/null +++ b/ComplexityTests/WordRAMRealizationBind.lean @@ -0,0 +1,61 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.WordRAM.Realization.Bind +import Complexity.Computability.WordRAM.Realization.Primitive + +/-! A uniform continuation reads the address returned by allocation, not a statically fixed cell. -/ + +namespace ComplexityTests.WordRAMRealizationBind + +open Cslib.DataStructure Cslib.WordRAM Cslib.WordRAM.Realization + +private def word : ℕ ↪ (Fin 1 → ℕ) := (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding + +private def environment : ℕ × ℕ ↪ (Fin 2 → ℕ) := + (word.prodMap word).trans (Fin.appendEquiv 1 1).toEmbedding + +private def allocatedRead (count : ℕ) : Memory.Prog ℕ := + (Memory.alloc count).bind Memory.read + +-- The two source emitters are uniform over all initial counts and all returned addresses. +-- Only their existing primitive certificates are supplied: no intermediate assertion or +-- manually chosen register layout is needed by the bind client. +example : Realizes .exact allocatedRead word word + (fun _ _ _ => True) (fun _ _ => 1) := by + have hp : Realizes .exact (fun count => Memory.alloc count) word word + (fun _ _ _ => True) (fun _ _ => 0) := Realizes.alloc word 0 + have hq : Realizes .exact (fun da : ℕ × ℕ => Memory.read da.2) environment word + (fun _ _ _ => True) (fun _ _ => 0) := Realizes.read environment 1 + have h := Realizes.bind hp hq + exact h.consequence (fun _ _ _ _ _ _ => ⟨trivial, trivial⟩) (fun _ _ => le_rfl) + +private def initial : Memory.State := ⟨fun _ => 7, 3⟩ + +-- This is a nonempty admissible instance; the allocated base is 3 while the input count is 2. +example : Memory.WellFormed 4 initial := by + constructor + · decide + · intro address + change Fits 4 7 + decide + +example : (Memory.spec 4).ValidHistory initial + ((Memory.spec 4).clientHistory initial (allocatedRead 2)) := by decide + +example : (Memory.spec 4).clientResult initial (allocatedRead 2) = 0 := by decide + +example : ((Memory.spec 4).clientState initial (allocatedRead 2)).frontier = 5 := by decide + +-- The abstraction retains cells outside the allocated block, including inaccessible cells. +example : ((Memory.spec 4).clientState initial (allocatedRead 2)).mem 10 = 7 := by decide + +-- Empty allocation cannot justify reading its returned frontier: the existing memory domain +-- remains a genuine obligation of the composed realization. +example : ¬(Memory.spec 4).ValidHistory initial + ((Memory.spec 4).clientHistory initial (allocatedRead 0)) := by decide + +end ComplexityTests.WordRAMRealizationBind diff --git a/ComplexityTests/WordRAMRealizationBranch.lean b/ComplexityTests/WordRAMRealizationBranch.lean new file mode 100644 index 0000000000..9b027819f9 --- /dev/null +++ b/ComplexityTests/WordRAMRealizationBranch.lean @@ -0,0 +1,52 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: local-only (tests of realization branching) + +public import Complexity.Computability.WordRAM.Realization.Branch +public import Complexity.Computability.WordRAM.Realization.Glue + +/-! The branch that needs `1` is taken only when an input word is positive. Thus the same fixed +program also works at width zero on two zero inputs, without requiring `Fits 0 1`. -/ + +public section + +open Cslib.WordRAM Cslib.WordRAM.Realization + +namespace WordRAMRealizationBranchTests + +@[expose] def input : (Fin 2 → ℕ) ↪ (Fin 2 → ℕ) := Function.Embedding.refl _ + +@[expose] def output : ℕ ↪ (Fin 1 → ℕ) := (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding + +theorem branch_fits_on_selected_path : Realizes .exact + (fun v => if v 0 < v 1 then pure 1 else pure 0) input output + (fun _ _ _ => True) (fun _ _ => 3) := by + have hp := Realizes.glue input + (GlueComputes.const (B := .exact) (P := fun _ : Fin 2 → ℕ => True) + (bound := fun _ => 1) 1 (fun _ _ => le_rfl)) + have hn := Realizes.glue input + (GlueComputes.const (B := .exact) (P := fun _ : Fin 2 → ℕ => True) + (bound := fun _ => 0) 0 (fun _ _ => le_rfl)) + have h := Realizes.branch (.lt 0 1) hp hn + apply h.consequence + · intro w d s hwords hmem hs + by_cases hd : d 0 < d 1 + · simp only [test, Cond.Holds, input, Function.Embedding.refl_apply, + ite_eq_left hd] + exact ⟨trivial, (hwords 1).of_le (by change 1 ≤ d 1; omega)⟩ + · simp only [test, Cond.Holds, input, Function.Embedding.refl_apply, + ite_eq_right hd] + exact ⟨trivial, fits_zero w⟩ + · intro d s + split <;> exact le_rfl + +example : ¬ Fits 0 1 := by decide + +example : ¬ test (.lt 0 1) (fun _ : Fin 2 => 0) := by decide + +end WordRAMRealizationBranchTests diff --git a/ComplexityTests/WordRAMRealizationPrimitive.lean b/ComplexityTests/WordRAMRealizationPrimitive.lean new file mode 100644 index 0000000000..fd02aca415 --- /dev/null +++ b/ComplexityTests/WordRAMRealizationPrimitive.lean @@ -0,0 +1,215 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.WordRAM.Realization.Primitive + +/-! +# Concrete clients of native memory-query realization + +The clients instantiate the emitted native code on dirty memory, retain an unrelated live word, +and inspect the returned word, frontier and entire resulting memory. Empty zeroed allocation is +also instantiated at word width zero, where the constant `1` cannot be written. +-/ + +namespace ComplexityTests.WordRAMRealizationPrimitive + +open Cslib.WordRAM Cslib.WordRAM.Realization Cslib.DataStructure + +private abbrev wordWords : ℕ ↪ (Fin 1 → ℕ) := + Equiv.toEmbedding (Equiv.symm (Equiv.funUnique (Fin 1) ℕ)) + +private def initial {r : ℕ} (frontier arg marker : ℕ) (mem : ℕ → ℕ) : Data r := + ⟨fun j => if j.val = 0 then frontier else if j.val = 1 then arg + else if j.val = 2 then marker else 0, mem⟩ + +/-- A canonical layout keeps the frontier, argument and a live marker before the fresh bank. -/ +private theorem word_query {B : Basis} (p : ℕ → Memory.Prog ℕ) + (h : Realizes B p wordWords wordWords (fun _ _ _ => True) (fun _ _ => 0)) + (w frontier arg marker : ℕ) (mem : ℕ → ℕ) + (hf : Fits w frontier) (ha : Fits w arg) (hm : ∀ a, Fits w (mem a)) + (hmarker : Fits w marker) + (hv : (Memory.spec w).ValidHistory ⟨mem, frontier⟩ + ((Memory.spec w).clientHistory ⟨mem, frontier⟩ (p arg))) : + ∃ n C, ∃ code : Code B (3 + (1 + n + 1)), ∃ y : Data (3 + (1 + n + 1)), + ExecWithin w code (initial frontier arg marker mem) y + (C * (memoryCost (p arg) ⟨mem, frontier⟩ + 1)) ∧ + memoryState ⟨0, by omega⟩ y = (Memory.spec w).clientState ⟨mem, frontier⟩ (p arg) ∧ + y.regs ⟨3, by omega⟩ = (Memory.spec w).clientResult ⟨mem, frontier⟩ (p arg) ∧ + y.regs ⟨1, by omega⟩ = arg ∧ y.regs ⟨2, by omega⟩ = marker := by + obtain ⟨n, C, emit, he⟩ := h + let f : Fin (3 + (1 + n + 1)) := ⟨0, by omega⟩ + let src : Fin 1 → Fin (3 + (1 + n + 1)) := fun _ => ⟨1, by omega⟩ + let tmp : Fin (1 + n + 1) → Fin (3 + (1 + n + 1)) := Fin.natAdd 3 + have hi : Function.Injective tmp := by + intro a b hab + apply Fin.ext + have hval := congrArg Fin.val hab + change 3 + a.val = 3 + b.val at hval + omega + have hd (i : Fin 1) (j : Fin (1 + n + 1)) : src i ≠ tmp j := by + intro hij + have hval := congrArg Fin.val hij + change 1 = 3 + j.val at hval + omega + have htf (j : Fin (1 + n + 1)) : tmp j ≠ f := by + intro hj + have hval := congrArg Fin.val hj + change 3 + j.val = 0 at hval + omega + have hsf (i : Fin 1) : src i ≠ f := by + intro hi + have hval := congrArg Fin.val hi + change 1 = 0 at hval + omega + let x : Data (3 + (1 + n + 1)) := initial frontier arg marker mem + have hx : x.Bounded w := by + refine ⟨fun j => ?_, hm⟩ + change Fits w (if j.val = 0 then frontier else if j.val = 1 then arg + else if j.val = 2 then marker else 0) + split_ifs <;> first | exact hf | exact ha | exact hmarker | exact fits_zero w + have hin : x.regs ∘ src = wordWords arg := by + funext i + rfl + obtain ⟨y, hy, hstate, hout, hframe⟩ := (he f src tmp hi hd htf hsf).2 w arg x hx hin + trivial hv + have hxs : memoryState f x = ⟨mem, frontier⟩ := rfl + rw [hxs] at hy hstate hout + have ho := hout 0 + change y.regs ⟨3, by omega⟩ = (Memory.spec w).clientResult ⟨mem, frontier⟩ (p arg) at ho + have harg := hframe ⟨1, by omega⟩ + (by intro h; have hval := congrArg Fin.val h; change 1 = 0 at hval; omega) + (fun j h => by have hval := congrArg Fin.val h; change 3 + j.val = 1 at hval; omega) + have hmark := hframe ⟨2, by omega⟩ + (by intro h; have hval := congrArg Fin.val h; change 2 = 0 at hval; omega) + (fun j h => by have hval := congrArg Fin.val h; change 3 + j.val = 2 at hval; omega) + refine ⟨n, C, emit f src tmp, y, ?_, hstate, ho, harg, hmark⟩ + simpa only [Nat.add_zero] using hy + +-- Clearing a dirty block preserves both the allocated prefix and inaccessible high cells. +example : + ∃ n C, ∃ code : Code .exact (3 + (1 + n + 1)), ∃ y : Data (3 + (1 + n + 1)), + ExecWithin 4 code (initial 3 2 9 (fun _ => 7)) y (C * 4) ∧ + y.regs ⟨0, by omega⟩ = 5 ∧ y.regs ⟨3, by omega⟩ = 3 ∧ + y.regs ⟨1, by omega⟩ = 2 ∧ y.regs ⟨2, by omega⟩ = 9 ∧ + y.mem 3 = 0 ∧ y.mem 4 = 0 ∧ y.mem 2 = 7 ∧ y.mem 100 = 7 := by + obtain ⟨n, C, code, y, he, hs, ho, ha, hl⟩ := + word_query Memory.alloc (Realizes.alloc wordWords 0) 4 3 2 9 (fun _ => 7) + (by norm_num [Fits]) (by norm_num [Fits]) (fun _ => by norm_num [Fits]) + (by norm_num [Fits]) (by change Fits 4 (3 + 2) ∧ True; norm_num [Fits]) + have hf := congrArg Memory.State.frontier hs + have hm := congrArg Memory.State.mem hs + change y.mem = clear (fun _ => 7) 3 2 at hm + refine ⟨n, C, code, y, he, hf, ho, ha, hl, ?_⟩ + rw [hm] + norm_num [clear] + +-- At width zero only zero fits, but allocating an empty block still has a native realization. +example : + ∃ n C, ∃ code : Code .exact (3 + (1 + n + 1)), ∃ y : Data (3 + (1 + n + 1)), + ExecWithin 0 code (initial 0 0 0 (fun _ => 0)) y (C * 2) ∧ + y.regs ⟨0, by omega⟩ = 0 ∧ y.regs ⟨3, by omega⟩ = 0 ∧ + y.mem = (fun _ => 0) ∧ y.regs ⟨2, by omega⟩ = 0 := by + obtain ⟨n, C, code, y, he, hs, ho, _, hl⟩ := + word_query Memory.alloc (Realizes.alloc wordWords 0) 0 0 0 0 (fun _ => 0) + (fits_zero 0) (fits_zero 0) (fun _ => fits_zero 0) (fits_zero 0) + (by change Fits 0 (0 + 0) ∧ True; exact ⟨fits_zero 0, trivial⟩) + have hf := congrArg Memory.State.frontier hs + have hm := congrArg Memory.State.mem hs + change y.mem = clear (fun _ => 0) 0 0 at hm + rw [clear_zero] at hm + exact ⟨n, C, code, y, he, hf, ho, hm, hl⟩ + +-- Dirty allocation retains every old memory value while returning the old frontier. +example : + ∃ n C, ∃ code : Code .exact (3 + (1 + n + 1)), ∃ y : Data (3 + (1 + n + 1)), + ExecWithin 4 code (initial 3 2 9 (fun _ => 7)) y (C * 2) ∧ + y.regs ⟨0, by omega⟩ = 5 ∧ y.regs ⟨3, by omega⟩ = 3 ∧ + y.mem = (fun _ => 7) ∧ y.regs ⟨2, by omega⟩ = 9 := by + obtain ⟨n, C, code, y, he, hs, ho, _, hl⟩ := + word_query Memory.allocDirty (Realizes.allocDirty wordWords 0) 4 3 2 9 (fun _ => 7) + (by norm_num [Fits]) (by norm_num [Fits]) (fun _ => by norm_num [Fits]) + (by norm_num [Fits]) (by change Fits 4 (3 + 2) ∧ True; norm_num [Fits]) + exact ⟨n, C, code, y, he, congrArg Memory.State.frontier hs, ho, + congrArg Memory.State.mem hs, hl⟩ + +-- Reading an allocated word keeps the entire dirty memory and an unrelated live register. +example : + ∃ n C, ∃ code : Code .exact (3 + (1 + n + 1)), ∃ y : Data (3 + (1 + n + 1)), + ExecWithin 4 code (initial 3 2 9 (fun _ => 7)) y (C * 2) ∧ + y.regs ⟨0, by omega⟩ = 3 ∧ y.regs ⟨3, by omega⟩ = 7 ∧ + y.mem = (fun _ => 7) ∧ y.regs ⟨2, by omega⟩ = 9 := by + obtain ⟨n, C, code, y, he, hs, ho, _, hl⟩ := + word_query Memory.read (Realizes.read (B := .exact) wordWords 0) 4 3 2 9 (fun _ => 7) + (by norm_num [Fits]) (by norm_num [Fits]) (fun _ => by norm_num [Fits]) + (by norm_num [Fits]) (by change 2 < 3 ∧ True; norm_num) + exact ⟨n, C, code, y, he, congrArg Memory.State.frontier hs, ho, + congrArg Memory.State.mem hs, hl⟩ + +private def pairWords : ℕ × ℕ ↪ (Fin 2 → ℕ) where + toFun x := ![x.1, x.2] + inj' := by + intro a b h + apply Prod.ext + · exact congrFun h 0 + · exact congrFun h 1 + +private def writeInitial {r : ℕ} : Data r := + ⟨fun j => if j.val = 0 then 3 else if j.val = 1 then 2 else if j.val = 2 then 12 else 9, + fun _ => 7⟩ + +-- A store changes its allocated cell while preserving low/high memory and a live register. +example : + ∃ n C, ∃ code : Code .exact (4 + (0 + n + 1)), ∃ y : Data (4 + (0 + n + 1)), + ExecWithin 4 code writeInitial y (C * 2) ∧ + y.regs ⟨0, by omega⟩ = 3 ∧ y.mem 2 = 12 ∧ y.mem 0 = 7 ∧ y.mem 100 = 7 ∧ + y.regs ⟨3, by omega⟩ = 9 := by + obtain ⟨n, C, emit, he⟩ := Realizes.write (B := .exact) pairWords 0 1 + let f : Fin (4 + (0 + n + 1)) := ⟨0, by omega⟩ + let src : Fin 2 → Fin (4 + (0 + n + 1)) := fun i => ⟨1 + i.val, by omega⟩ + let tmp : Fin (0 + n + 1) → Fin (4 + (0 + n + 1)) := Fin.natAdd 4 + have hi : Function.Injective tmp := by + intro a b hab + apply Fin.ext + have hval := congrArg Fin.val hab + change 4 + a.val = 4 + b.val at hval + omega + have hd (i : Fin 2) (j : Fin (0 + n + 1)) : src i ≠ tmp j := by + intro hij + have hval := congrArg Fin.val hij + change 1 + i.val = 4 + j.val at hval + omega + have htf (j : Fin (0 + n + 1)) : tmp j ≠ f := by + intro hj + have hval := congrArg Fin.val hj + change 4 + j.val = 0 at hval + omega + have hsf (i : Fin 2) : src i ≠ f := by + intro hi + have hval := congrArg Fin.val hi + change 1 + i.val = 0 at hval + omega + let x : Data (4 + (0 + n + 1)) := writeInitial + have hx : x.Bounded 4 := by + refine ⟨fun j => ?_, fun _ => by change Fits 4 7; norm_num [Fits]⟩ + change Fits 4 (if j.val = 0 then 3 else if j.val = 1 then 2 else if j.val = 2 then 12 else 9) + split_ifs <;> norm_num [Fits] + have hin : x.regs ∘ src = pairWords (2, 12) := by + funext i + fin_cases i <;> rfl + have hv : (Memory.spec 4).ValidHistory (memoryState f x) + ((Memory.spec 4).clientHistory (memoryState f x) (Memory.write 2 12)) := by + change (2 < 3 ∧ Fits 4 12) ∧ True + norm_num [Fits] + obtain ⟨y, hy, hs, _, hframe⟩ := (he f src tmp hi hd htf hsf).2 4 (2, 12) x hx hin trivial hv + have hm := congrArg Memory.State.mem hs + change y.mem = Function.update (fun _ => 7) 2 12 at hm + have hf := congrArg Memory.State.frontier hs + have hl := hframe ⟨3, by omega⟩ + (by intro h; have hval := congrArg Fin.val h; change 3 = 0 at hval; omega) + (fun j h => by have hval := congrArg Fin.val h; change 4 + j.val = 3 at hval; omega) + refine ⟨n, C, emit f src tmp, y, hy, hf, ?_, ?_, ?_, hl⟩ <;> rw [hm] <;> norm_num + +end ComplexityTests.WordRAMRealizationPrimitive diff --git a/ROADMAP.md b/ROADMAP.md index 11d44c8c06..678d8e30d8 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -631,6 +631,14 @@ reusing graph and matroid foundations and the shared data-structure interfaces. `3704*(p+1)²*(n+1)^2.81` instructions including halt. Its source-regime admission and width-independent prefix bounds are proved; selecting the actual minimum-count prime and the global endpoint remain separate. +- **Memory-oracle realization** ([#2205], [#2213]): the foundational graded kernel certifies + all four memory queries, register-word glue, native branches and binds with one fixed + continuation emitter for all runtime replies. Its functional representation retains the + complete memory and frontier, and its instruction currency adds local work to memory charges. + Remaining: bounded runtime loops, charged input installation and flat programs, operation-level + memory implementation and framed upper-ADT adapters. The full C2/M1b and queue transfer + objectives remain open; this foundation does not turn arbitrary host continuations into + machine-time certificates. - **Stateful algorithms and data structures:** Word-RAM controllers for larger adaptive and iterative clients, including the two-stack queue and timeline-editing controllers; reusable allocation and deallocation, shrinking, and live and peak space accounting; ownership and @@ -774,3 +782,5 @@ not planned, not as proved. [#2019]: https://github.com/cslib-community/complexitylib/issues/2019 [#2062]: https://github.com/cslib-community/complexitylib/issues/2062 [#2063]: https://github.com/cslib-community/complexitylib/issues/2063 +[#2205]: https://github.com/cslib-community/complexitylib/issues/2205 +[#2213]: https://github.com/cslib-community/complexitylib/issues/2213 diff --git a/UPSTREAM.md b/UPSTREAM.md index 0aebe288d0..7a8ebc36cb 100644 --- a/UPSTREAM.md +++ b/UPSTREAM.md @@ -510,6 +510,12 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he representation from the standard input. `WordRAM/Function` gives separate nonuniform and uniform RAM function-time predicates, with named-certificate reuse by `polytime`. Arbitrary continuation synthesis, iterative clients and a Turing-machine simulation remain open. + The bounded `WordRAM/Realization` foundation (#2213, under #2205) reuses the memory + oracle and the same native `Code`/`ExecWithin` semantics. Its explicit faithful register + encodings support all four memory queries, certified word glue, branches and uniform + reply-dependent bind, charging local work as well as memory operations. Query arguments are + already in live registers; whole-input installation, final halt, bounded-loop and local-ADT + adapter endpoints remain separate work. This adds no abstract-catalogue headline. `DataStructure/OrderedSet` and `DataStructure/OrderedSet/*` provide neutral optional-minimum contracts, a typed finite-set interface including deletion, and adaptive minimum extraction, with no tree or cost dependency. Bounded-key implementations may specialize From d8f6bea19d10e824d0045e4ed832fbc70d182177 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 1 Nov 2026 18:27:47 -0500 Subject: [PATCH 4/9] fix(WordRAM): normalize the memory return simp rule --- Complexity/Computability/WordRAM/Realization/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Complexity/Computability/WordRAM/Realization/Basic.lean b/Complexity/Computability/WordRAM/Realization/Basic.lean index 12c4ef7608..07f59ad67b 100644 --- a/Complexity/Computability/WordRAM/Realization/Basic.lean +++ b/Complexity/Computability/WordRAM/Realization/Basic.lean @@ -72,7 +72,7 @@ theorem runClient_width (w : ℕ) (p : Memory.Prog α) (s : Memory.State) : /-- A semantic return issues no memory operation. Its native glue is charged separately. -/ @[simp] theorem memoryCost_pure (a : α) (s : Memory.State) : - memoryCost (.pure a) s = 0 := rfl + memoryCost (pure a) s = 0 := rfl /-- Memory charges add at the actual intermediate state; the local bind charge is separate. -/ theorem memoryCost_bind {β : Type} (p : Memory.Prog α) (q : α → Memory.Prog β) From 4977e9bf3c417ebb33a2d39a73f17d169a463863 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 1 Nov 2026 18:46:48 -0500 Subject: [PATCH 5/9] feat(WordRAM): realize bounded loops and initialized client programs Reuse one body certificate for runtime fuel, charging every iteration and all local work even without memory queries. Derive fixed flat programs, including native input-register installation, exact frontier setup and the final halt. Unit observations execute an additional real zero instruction. This is the loop/whole-program milestone under #2213 and #2205. Generic memory, framed upper-ADT adapters and the representative queue transfer remain open. Existing selected abstracts and headline scope are unchanged. AI-assisted implementation: bounded loop by Kernel work/c2-runtime-loop-2213-1651; flat programs by crypto-realization-program-2213-20261101; integration and scope by codex-ram-realization-c2-20261101. Prior foundational source remains unchanged. --- Complexity.lean | 2 + .../WordRAM/Realization/Loop.lean | 509 ++++++++++++++++++ .../WordRAM/Realization/Program.lean | 345 ++++++++++++ ComplexityTests/WordRAMRealizationLoop.lean | 193 +++++++ .../WordRAMRealizationProgram.lean | 294 ++++++++++ ROADMAP.md | 9 +- UPSTREAM.md | 9 +- 7 files changed, 1354 insertions(+), 7 deletions(-) create mode 100644 Complexity/Computability/WordRAM/Realization/Loop.lean create mode 100644 Complexity/Computability/WordRAM/Realization/Program.lean create mode 100644 ComplexityTests/WordRAMRealizationLoop.lean create mode 100644 ComplexityTests/WordRAMRealizationProgram.lean diff --git a/Complexity.lean b/Complexity.lean index b58e9959ef..25721a3ac3 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2560,7 +2560,9 @@ public import Complexity.Computability.WordRAM.Realization.Basic public import Complexity.Computability.WordRAM.Realization.Bind public import Complexity.Computability.WordRAM.Realization.Branch public import Complexity.Computability.WordRAM.Realization.Glue +public import Complexity.Computability.WordRAM.Realization.Loop public import Complexity.Computability.WordRAM.Realization.Primitive +public import Complexity.Computability.WordRAM.Realization.Program public import Complexity.Computability.WordRAM.RegisterFrame public import Complexity.Computability.WordRAM.Sequence public import Complexity.Computability.WordRAM.Signed.Arithmetic diff --git a/Complexity/Computability/WordRAM/Realization/Loop.lean b/Complexity/Computability/WordRAM/Realization/Loop.lean new file mode 100644 index 0000000000..9081953bdc --- /dev/null +++ b/Complexity/Computability/WordRAM/Realization/Loop.lean @@ -0,0 +1,509 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.WordRAM.Realization.Basic + +/-! +# Bounded memory-client loops + +Bounded iteration remains an ordinary `Memory.Prog` term. The local-work currency counts body +work and every iteration, including iterations issuing no memory query. The native realization +uses one fixed body emitter and static registers for the mutable state and countdown counter. + +## Main definitions + +* `iterate`: bounded iteration in the existing memory-client monad. +* `iterationWork`, `iterationSafe`: local work and domains along the actual semantic states. + +## Main results + +* `copyBank_exec`: a static register-bank copy with memory and live-register frames. +* `loop_invariant_state_charged`: bounded native loops charge local work and control. +* `Realizes.iterateRuntime`: one uniform body certificate realizes a runtime-bounded loop. + +The iteration grading and realization are original infrastructure over the existing free monad +and structured Word-RAM code. No additional program syntax or memory model is introduced. +-/ + +@[expose] public section + +namespace Cslib.WordRAM.Realization + +open Cslib.DataStructure + +variable {δ σ : Type} {B : Basis} {r k l : ℕ} + +/-- Execute one fixed body family a runtime-bounded number of times. -/ +def iterate (body : δ × σ → Memory.Prog σ) (d : δ) : ℕ → σ → Memory.Prog σ + | 0, s => pure s + | n + 1, s => do + let s' ← body (d, s) + iterate body d n s' + +/-- Local computation and one control-work unit per iteration, along actual semantic states. -/ +def iterationWork (body : δ × σ → Memory.Prog σ) (work : (δ × σ) → Memory.State → ℕ) + (d : δ) : ℕ → σ → Memory.State → ℕ + | 0, _, _ => 0 + | n + 1, a, s => + work (d, a) s + iterationWork body work d n + ((Memory.spec 0).clientResult s (body (d, a))) + ((Memory.spec 0).clientState s (body (d, a))) + 1 + +/-- Every executed body must satisfy its explicit domain at the reached state. -/ +def iterationSafe (body : δ × σ → Memory.Prog σ) + (safe : ℕ → (δ × σ) → Memory.State → Prop) (w : ℕ) (d : δ) : + ℕ → σ → Memory.State → Prop + | 0, _, _ => True + | n + 1, a, s => safe w (d, a) s ∧ iterationSafe body safe w d n + ((Memory.spec 0).clientResult s (body (d, a))) + ((Memory.spec 0).clientState s (body (d, a))) + +/-- Native register copies need no word-size or arithmetic side condition. -/ +def copyBank : {k : ℕ} → (Fin k → Fin r) → (Fin k → Fin r) → Fin r → Code B r + | 0, _, _, idle => .op (.copy idle idle) + | n + 1, src, dst, idle => .seq (.op (.copy (dst 0) (src 0))) + (copyBank (fun i : Fin n => src i.succ) (fun i => dst i.succ) idle) + +/-- Copying a finite bank does not inspect the word width. -/ +theorem copyBank_not_readsWidth (src dst : Fin k → Fin r) (idle : Fin r) : + ¬(copyBank (B := B) src dst idle).ReadsWidth := by + induction k with + | zero => simp [copyBank, Code.ReadsWidth, Op.ReadsWidth] + | succ n ih => simp [copyBank, Code.ReadsWidth, Op.ReadsWidth, ih] + +/-- Copy disjoint source words into an injective destination bank, leaving the entire memory and +all other registers unchanged. A neutral copy supplies the zero-length code case. -/ +theorem copyBank_exec (src dst : Fin k → Fin r) (idle : Fin r) + (hi : Function.Injective dst) (hd : ∀ i j, src i ≠ dst j) (w : ℕ) (x : Data r) : + ∃ y, ExecWithin w (copyBank (B := B) src dst idle) x y (k + 1) ∧ + y.mem = x.mem ∧ (∀ i, y.regs (dst i) = x.regs (src i)) ∧ + ∀ j, (∀ i, dst i ≠ j) → y.regs j = x.regs j := by + induction k generalizing x with + | zero => + have he : ExecWithin (B := B) w (.op (.copy idle idle)) x x 1 := by + convert (ExecWithin.copy (B := B) (w := w) (d := idle) (s := idle) (x := x)) using 1 + apply Data.ext <;> simp [Data.set] + exact ⟨x, he, rfl, fun i => Fin.elim0 i, fun _ _ => rfl⟩ + | succ n ih => + let a := x.set (dst 0) (x.regs (src 0)) + obtain ⟨y, hy, hm, hout, hframe⟩ := ih + (fun i : Fin n => src i.succ) (fun i => dst i.succ) + (fun i j h => Fin.succ_injective _ (hi h)) + (fun i j => hd i.succ j.succ) a + have he : ExecWithin (B := B) w (.op (.copy (dst 0) (src 0))) x a 1 := + ExecWithin.copy + refine ⟨y, ?_, hm, ?_, ?_⟩ + · simpa only [copyBank, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] using he.seq hy + · intro i + refine Fin.cases ?_ (fun j => ?_) i + · rw [hframe (dst 0) (fun j h => Fin.succ_ne_zero _ (hi h))] + simp [a, Data.set] + · rw [hout] + exact Function.update_of_ne (hd j.succ 0) _ _ + · intro j hj + rw [hframe j (fun i => hj i.succ)] + exact Function.update_of_ne (hj 0).symm _ _ + +/-- The result of the memory interpreter is independent of the admissibility width. -/ +theorem clientResult_width (w : ℕ) (p : Memory.Prog σ) (s : Memory.State) : + (Memory.spec w).clientResult s p = (Memory.spec 0).clientResult s p := + congrArg Prod.fst (runClient_width w p s) + +/-- The final memory/frontier state is independent of the admissibility width. -/ +theorem clientState_width (w : ℕ) (p : Memory.Prog σ) (s : Memory.State) : + (Memory.spec w).clientState s p = (Memory.spec 0).clientState s p := + congrArg (fun t => t.2.1) (runClient_width w p s) + +/-- Admissible sequential histories split at the actual returned value and memory state. -/ +theorem validHistory_bind (w : ℕ) {α β : Type} (p : Memory.Prog α) + (q : α → Memory.Prog β) (s : Memory.State) : + (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (p.bind q)) ↔ + (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s p) ∧ + (Memory.spec w).ValidHistory ((Memory.spec w).clientState s p) + ((Memory.spec w).clientHistory ((Memory.spec w).clientState s p) + (q ((Memory.spec w).clientResult s p))) := by + simp only [StateTransitionSpec.clientHistory, StateTransitionSpec.runClient_bind] + rw [StateTransitionSpec.validHistory_append, StateTransitionSpec.run_runClient] + +/-- Memory cost and certified local work decompose at each actual iteration. -/ +theorem iteration_charge_succ (body : δ × σ → Memory.Prog σ) + (work : (δ × σ) → Memory.State → ℕ) (d : δ) (n : ℕ) (a : σ) (s : Memory.State) : + memoryCost (iterate body d (n + 1) a) s + iterationWork body work d (n + 1) a s = + memoryCost (body (d, a)) s + work (d, a) s + + (memoryCost (iterate body d n ((Memory.spec 0).clientResult s (body (d, a)))) + ((Memory.spec 0).clientState s (body (d, a))) + + iterationWork body work d n ((Memory.spec 0).clientResult s (body (d, a))) + ((Memory.spec 0).clientState s (body (d, a)))) + 1 := by + rw [show iterate body d (n + 1) a = + (body (d, a)).bind (iterate body d n) from rfl, memoryCost_bind] + simp only [iterationWork] + omega + +/-- Sum a state-dependent charge along a fixed semantic transition. -/ +def iterationSum (next : σ → σ) (charge : σ → ℕ) : ℕ → σ → ℕ + | 0, _ => 0 + | n + 1, s => charge s + iterationSum next charge n (next s) + +/-- A bounded native loop may charge variable body work and one unit per iteration without +issuing a memory query. Its body, register bank and exchange constants are fixed before fuel. +The remaining-fuel relation also carries arbitrary semantic proof state. -/ +theorem loop_invariant_state_charged {cond : Cond r} {code : Code B r} {w C D : ℕ} + (I : ℕ → σ → Data r → Prop) (next : σ → σ) (charge : σ → ℕ) + (hexit : ∀ s x, I 0 s x → ¬cond.Holds x) + (hbody : ∀ n s x, I (n + 1) s x → + cond.Holds x ∧ ∃ y, ExecWithin w code x y (C * (charge s + 1) + D) ∧ + I n (next s) y) + {n : ℕ} {s : σ} {x : Data r} (hx : I n s x) : + ∃ y, ExecWithin w (.loop cond code) x y + ((C + D + 2) * (iterationSum next charge n s + n + 1)) ∧ + I 0 ((next^[n]) s) y := by + induction n generalizing s x with + | zero => + refine ⟨x, (ExecWithin.loop_exit (hexit s x hx)).mono ?_, hx⟩ + simp only [iterationSum, Nat.zero_add, Nat.mul_one] + omega + | succ n ih => + obtain ⟨hc, a, ha, hI⟩ := hbody n s x hx + obtain ⟨y, hy, hIy⟩ := ih hI + refine ⟨y, (ExecWithin.loop_iter hc ha hy).mono ?_, ?_⟩ + · simp only [iterationSum] + nlinarith + · simpa only [Function.iterate_succ_apply] using hIy + +/-- One semantic iteration updates both the mutable value and the complete memory state. -/ +def iterationStep (body : δ × σ → Memory.Prog σ) (d : δ) (a : σ × Memory.State) : + σ × Memory.State := + ((Memory.spec 0).clientResult a.2 (body (d, a.1)), + (Memory.spec 0).clientState a.2 (body (d, a.1))) + +/-- The interpreter follows precisely the bounded semantic transition, not an arbitrary state. -/ +theorem iterate_result_state (body : δ × σ → Memory.Prog σ) (d : δ) (n : ℕ) (a : σ) + (s : Memory.State) : + ((Memory.spec 0).clientResult s (iterate body d n a), + (Memory.spec 0).clientState s (iterate body d n a)) = + (iterationStep body d)^[n] (a, s) := by + induction n generalizing a s with + | zero => rfl + | succ n ih => + rw [show iterate body d (n + 1) a = + (body (d, a)).bind (iterate body d n) from rfl] + simpa only [StateTransitionSpec.clientResult, StateTransitionSpec.clientState, + StateTransitionSpec.runClient_bind, Function.iterate_succ_apply, iterationStep] using + ih ((Memory.spec 0).clientResult s (body (d, a))) + ((Memory.spec 0).clientState s (body (d, a))) + +/-- The native grading rule's semantic sum is exactly memory charge plus local iteration work. -/ +theorem iterationSum_eq (body : δ × σ → Memory.Prog σ) + (work : (δ × σ) → Memory.State → ℕ) (d : δ) (n : ℕ) (a : σ) (s : Memory.State) : + iterationSum (iterationStep body d) + (fun q => memoryCost (body (d, q.1)) q.2 + work (d, q.1) q.2) n (a, s) + n = + memoryCost (iterate body d n a) s + iterationWork body work d n a s := by + induction n generalizing a s with + | zero => rfl + | succ n ih => + rw [iterationSum, iteration_charge_succ] + have h := ih ((Memory.spec 0).clientResult s (body (d, a))) + ((Memory.spec 0).clientState s (body (d, a))) + dsimp only [iterationStep] at * + omega + +private def stateSlot {l n : ℕ} (i : Fin l) : Fin (l + (l + n + 3) + 1) := + ⟨i.val, by omega⟩ + +private def counterSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1) := ⟨l, by omega⟩ +private def zeroSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1) := ⟨l + 1, by omega⟩ +private def oneSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1) := ⟨l + 2, by omega⟩ + +private def bodySlot {l n : ℕ} (i : Fin (l + n + 1)) : Fin (l + (l + n + 3) + 1) := + ⟨l + 3 + i.val, by omega⟩ + +private def loopBody {n : ℕ} (emit : ∀ {r : ℕ}, Fin r → (Fin (k + l) → Fin r) → + (Fin (l + n + 1) → Fin r) → Code .exact r) + (frontier : Fin r) (src : Fin (k + l + 1) → Fin r) + (tmp : Fin (l + (l + n + 3) + 1) → Fin r) : Code .exact r := + .seq (emit frontier (Fin.append (fun i : Fin k => src ⟨i.val, by omega⟩) + (fun i => tmp (stateSlot i))) (fun i => tmp (bodySlot i))) <| + .seq (copyBank (fun i : Fin l => tmp (bodySlot (Fin.castAdd (n + 1) i))) + (fun i => tmp (stateSlot i)) (tmp (zeroSlot l n))) <| + .seq (.op (.const (tmp (oneSlot l n)) 1)) + (.op (.exactBin .sub (tmp (counterSlot l n)) + (tmp (counterSlot l n)) (tmp (oneSlot l n)))) + +private def loopEmit {n : ℕ} (emit : ∀ {r : ℕ}, Fin r → (Fin (k + l) → Fin r) → + (Fin (l + n + 1) → Fin r) → Code .exact r) + (frontier : Fin r) (src : Fin (k + l + 1) → Fin r) + (tmp : Fin (l + (l + n + 3) + 1) → Fin r) : Code .exact r := + .seq (copyBank (fun i : Fin l => src ⟨k + i.val, by omega⟩) + (fun i => tmp (stateSlot i)) (tmp (zeroSlot l n))) <| + .seq (.op (.copy (tmp (counterSlot l n)) (src ⟨k + l, by omega⟩))) <| + .seq (.op (.const (tmp (zeroSlot l n)) 0)) + (.loop (.lt (tmp (zeroSlot l n)) (tmp (counterSlot l n))) + (loopBody emit frontier src tmp)) + +namespace Realizes + +/-- A runtime-bounded loop reuses one fixed body emitter, including iterations without queries. +The visible domain is precisely the body domains along the actual semantic states. -/ +theorem iterateRuntime (input : δ ↪ (Fin k → ℕ)) (output : σ ↪ (Fin l → ℕ)) + {body : δ × σ → Memory.Prog σ} + {safe : ℕ → (δ × σ) → Memory.State → Prop} + {work : (δ × σ) → Memory.State → ℕ} + (h : Realizes .exact body + ((input.prodMap output).trans (Fin.appendEquiv k l).toEmbedding) output safe work) : + Realizes .exact (fun d : (δ × σ) × ℕ => iterate body d.1.1 d.2 d.1.2) + ((((input.prodMap output).trans (Fin.appendEquiv k l).toEmbedding).prodMap + (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding).trans + (Fin.appendEquiv (k + l) 1).toEmbedding) output + (fun w d s => iterationSafe body safe w d.1.1 d.2 d.1.2 s) + (fun d s => iterationWork body work d.1.1 d.2 d.1.2 s) := by + obtain ⟨n, C, emit, he⟩ := h + refine ⟨l + n + 3, C + 2 * l + 8, loopEmit emit, ?_⟩ + intro r frontier src tmp hi hd hf hs + let st : Fin l → Fin r := fun i => tmp (stateSlot i) + let ctr := tmp (counterSlot l n) + let zero := tmp (zeroSlot l n) + let one := tmp (oneSlot l n) + let bt : Fin (l + n + 1) → Fin r := fun i => tmp (bodySlot i) + let env : Fin k → Fin r := fun i => src ⟨i.val, by omega⟩ + let bs := Fin.append env st + have hst : Function.Injective st := by + intro i j hij + apply Fin.ext + exact congrArg (fun j : Fin (l + (l + n + 3) + 1) => j.val) (hi hij) + have hbt : Function.Injective bt := by + intro i j hij + apply Fin.ext + have hh := congrArg Fin.val (hi hij) + dsimp only [bodySlot] at hh + omega + have hbdis : ∀ i j, bs i ≠ bt j := by + intro i j + refine Fin.addCases (fun i => ?_) (fun i => ?_) i + · simpa only [bs, Fin.append_left] using hd (⟨i.val, by omega⟩ : Fin (k + l + 1)) (bodySlot j) + · simp only [bs, Fin.append_right] + intro hij + have hh := congrArg Fin.val (hi hij) + dsimp only [stateSlot, bodySlot] at hh + omega + have hbf : ∀ j, bt j ≠ frontier := fun j => hf _ + have hbs : ∀ i, bs i ≠ frontier := by + intro i + refine Fin.addCases (fun i => ?_) (fun i => ?_) i + · simpa only [bs, Fin.append_left] using hs (⟨i.val, by omega⟩ : Fin (k + l + 1)) + · simpa only [bs, Fin.append_right] using hf (stateSlot i) + obtain ⟨hnw, hrun⟩ := he frontier bs bt hbt hbdis hbf hbs + have houtdis : ∀ i j : Fin l, bt (Fin.castAdd (n + 1) i) ≠ st j := by + intro i j hij + have hh := congrArg Fin.val (hi hij) + dsimp only [bodySlot, stateSlot] at hh + omega + have hct : ctr ≠ zero := by + intro hij + have := congrArg Fin.val (hi hij) + simp [counterSlot, zeroSlot] at this + have hco : ctr ≠ one := by + intro hij + have := congrArg Fin.val (hi hij) + simp [counterSlot, oneSlot] at this + have hzo : zero ≠ one := by + intro hij + have := congrArg Fin.val (hi hij) + simp [zeroSlot, oneSlot] at this + have hregbt (a : Fin (l + (l + n + 3) + 1)) (ha : a.val < l + 3) : + ∀ j, bt j ≠ tmp a := by + intro j hij + have hh := congrArg Fin.val (hi hij) + dsimp only [bodySlot] at hh + omega + have hregst (a : Fin (l + (l + n + 3) + 1)) (ha : l ≤ a.val) : + ∀ i, st i ≠ tmp a := by + intro i hij + have hh := congrArg Fin.val (hi hij) + dsimp only [stateSlot] at hh + omega + refine ⟨?_, ?_⟩ + · change ¬(loopEmit emit frontier src tmp).ReadsWidth + simpa [loopEmit, loopBody, Code.ReadsWidth, Op.ReadsWidth, Op.exactBin, + copyBank_not_readsWidth] using hnw + · intro w d x hx hin hsafe hv + let a₀ := d.1.2 + let d₀ := d.1.1 + let fuel := d.2 + let s₀ := memoryState frontier x + have henv (i : Fin k) : x.regs (env i) = input d₀ i := by + have hh : x.regs (src (Fin.castAdd 1 (Fin.castAdd l i))) = input d₀ i := by + simpa [d₀, Fin.appendEquiv] using congrFun hin (Fin.castAdd 1 (Fin.castAdd l i)) + have hidx : Fin.castAdd 1 (Fin.castAdd l i) = (⟨i.val, by omega⟩ : Fin (k + l + 1)) := by + apply Fin.ext + rfl + rw [hidx] at hh + exact hh + have hstate (i : Fin l) : x.regs (src ⟨k + i.val, by omega⟩) = output a₀ i := by + have hh : x.regs (src (Fin.castAdd 1 (Fin.natAdd k i))) = output a₀ i := by + simpa [a₀, Fin.appendEquiv] using congrFun hin (Fin.castAdd 1 (Fin.natAdd k i)) + have hidx : Fin.castAdd 1 (Fin.natAdd k i) = + (⟨k + i.val, by omega⟩ : Fin (k + l + 1)) := by + apply Fin.ext + rfl + rw [hidx] at hh + exact hh + have hfuel : x.regs (src ⟨k + l, by omega⟩) = fuel := by + have hh : x.regs (src (Fin.natAdd (k + l) 0)) = fuel := by + simpa [fuel, Fin.appendEquiv] using congrFun hin (Fin.natAdd (k + l) 0) + have hidx : Fin.natAdd (k + l) 0 = (⟨k + l, by omega⟩ : Fin (k + l + 1)) := by + apply Fin.ext + simp + rw [hidx] at hh + exact hh + obtain ⟨a, ha, ham, has, haf⟩ := copyBank_exec + (fun i : Fin l => src ⟨k + i.val, by omega⟩) st zero hst + (fun _ _ => hd _ _) w x + let b := a.set ctr fuel + let z := b.set zero 0 + have hafuel : a.regs (src ⟨k + l, by omega⟩) = fuel := by + rw [haf _ (fun _ => (hd _ _).symm)] + exact hfuel + have hc : ExecWithin (B := .exact) w (.op (.copy ctr (src ⟨k + l, by omega⟩))) a b 1 := by + simpa only [hafuel] using + (ExecWithin.copy (B := .exact) (w := w) (d := ctr) + (s := src ⟨k + l, by omega⟩) (x := a)) + have hz : ExecWithin (B := .exact) w (.op (.const zero 0)) b z 1 := + ExecWithin.const (fits_zero w) + let I : ℕ → (σ × Memory.State) → Data r → Prop := fun j q y => + y.Bounded w ∧ memoryState frontier y = q.2 ∧ + (∀ i, y.regs (env i) = input d₀ i) ∧ (∀ i, y.regs (st i) = output q.1 i) ∧ + y.regs ctr = j ∧ y.regs zero = 0 ∧ iterationSafe body safe w d₀ j q.1 q.2 ∧ + (Memory.spec w).ValidHistory q.2 + ((Memory.spec w).clientHistory q.2 (iterate body d₀ j q.1)) ∧ + ∀ i, i ≠ frontier → (∀ j, tmp j ≠ i) → y.regs i = x.regs i + have hIz : I fuel (a₀, s₀) z := by + refine ⟨(ha.seq (hc.seq hz)).bounded hx, ?_, ?_, ?_, ?_, ?_, hsafe, hv, ?_⟩ + · apply Memory.State.ext + · exact ham + · change (b.set zero 0).regs frontier = x.regs frontier + rw [show (b.set zero 0).regs frontier = b.regs frontier from + Function.update_of_ne (hf (zeroSlot l n)).symm _ _, + show b.regs frontier = a.regs frontier from + Function.update_of_ne (hf (counterSlot l n)).symm _ _, + haf frontier (fun i => hf _)] + · intro i + simp only [z, b, Data.set] + rw [Function.update_of_ne (hd _ _), Function.update_of_ne (hd _ _), + haf _ (fun _ => (hd _ _).symm)] + exact henv i + · intro i + simp only [z, b, Data.set] + rw [Function.update_of_ne (hregst _ (by simp [zeroSlot]) i), + Function.update_of_ne (hregst _ (by simp [counterSlot]) i), has] + exact hstate i + · simp [z, b, Data.set, hct] + · simp [z, Data.set] + · intro i hif htmp + simp only [z, b, Data.set] + rw [Function.update_of_ne (htmp _).symm, + Function.update_of_ne (htmp _).symm, haf _ (fun _ => htmp _)] + have hbody : ∀ j q y, I (j + 1) q y → + (Cond.lt zero ctr).Holds y ∧ ∃ y', + ExecWithin w (loopBody emit frontier src tmp) y y' + (C * (memoryCost (body (d₀, q.1)) q.2 + work (d₀, q.1) q.2 + 1) + (l + 3)) ∧ + I j (iterationStep body d₀ q) y' := by + intro j q y hIy + obtain ⟨hyb, hym, hye, hys, hyc, hyz, hysafe, hyv, hyframe⟩ := hIy + refine ⟨by simp [Cond.Holds, hyz, hyc], ?_⟩ + have hvparts := (validHistory_bind w (body (d₀, q.1)) + (iterate body d₀ j) q.2).mp hyv + have hinbody : y.regs ∘ bs = + ((input.prodMap output).trans (Fin.appendEquiv k l).toEmbedding) (d₀, q.1) := by + funext i + refine Fin.addCases (fun i => ?_) (fun i => ?_) i + · simpa [bs, Fin.appendEquiv] using hye i + · simpa [bs, Fin.appendEquiv] using hys i + obtain ⟨u, hu, hum, huo, huf⟩ := hrun w (d₀, q.1) y hyb hinbody + (hym ▸ hysafe.1) (hym ▸ hvparts.1) + rw [hym] at hu hum huo + rw [clientState_width] at hum + simp only [clientResult_width] at huo + obtain ⟨v, hv', hvm, hvs, hvf⟩ := copyBank_exec + (fun i : Fin l => bt (Fin.castAdd (n + 1) i)) st zero hst houtdis w u + have hvctr : v.regs ctr = j + 1 := by + rw [hvf _ (hregst _ (by simp [counterSlot])), + huf _ (hf _) (hregbt _ (by simp [counterSlot]))] + exact hyc + have hvzero : v.regs zero = 0 := by + rw [hvf _ (hregst _ (by simp [zeroSlot])), + huf _ (hf _) (hregbt _ (by simp [zeroSlot]))] + exact hyz + have h1 : Fits w 1 := (hyb.1 ctr).of_le (by omega) + let t := v.set one 1 + let y' := t.set ctr j + have ht : ExecWithin (B := .exact) w (.op (.const one 1)) v t 1 := + ExecWithin.const h1 + have htc : t.regs ctr = j + 1 := by + rw [show t.regs ctr = v.regs ctr from Function.update_of_ne hco _ _] + exact hvctr + have htone : t.regs one = 1 := by simp [t, Data.set] + have hjfit : Fits w j := (hyb.1 ctr).of_le (by omega) + have hdec : ExecWithin w (.op (.exactBin .sub ctr ctr one)) t y' 1 := by + apply ExecWithin.op + rw [Op.eval_exactBin, htc, htone] + simp only [BinOp.evalExact, Nat.le_add_left, ↓reduceIte, Nat.add_sub_cancel, + Option.bind_some] + exact Data.put_of_fits hjfit + refine ⟨y', ?_, ?_⟩ + · exact (hu.seq (hv'.seq (ht.seq hdec))).mono (by omega) + · refine ⟨(hu.seq (hv'.seq (ht.seq hdec))).bounded hyb, ?_, ?_, ?_, ?_, ?_, + hysafe.2, ?_, ?_⟩ + · apply Memory.State.ext + · exact hvm.trans (congrArg Memory.State.mem hum) + · change (t.set ctr j).regs frontier = _ + rw [show (t.set ctr j).regs frontier = t.regs frontier from + Function.update_of_ne (hf (counterSlot l n)).symm _ _, + show t.regs frontier = v.regs frontier from + Function.update_of_ne (hf (oneSlot l n)).symm _ _, + hvf frontier (fun i => hf _)] + exact congrArg Memory.State.frontier hum + · intro i + simp only [y', t, Data.set] + rw [Function.update_of_ne (hd _ _), Function.update_of_ne (hd _ _), + hvf _ (fun _ => (hd _ _).symm), huf _ (hs _) (fun _ => (hd _ _).symm)] + exact hye i + · intro i + simp only [y', t, Data.set] + rw [Function.update_of_ne (hregst _ (by simp [counterSlot]) i), + Function.update_of_ne (hregst _ (by simp [oneSlot]) i), hvs, huo] + rfl + · simp [y', Data.set] + · simp [y', t, Data.set, hct.symm, hzo, hvzero] + · have hrest := hvparts.2 + rw [clientState_width w, clientResult_width w] at hrest + exact hrest + · intro i hif htmp + simp only [y', t, Data.set] + rw [Function.update_of_ne (htmp _).symm, Function.update_of_ne (htmp _).symm, + hvf _ (fun _ => htmp _), huf _ hif (fun _ => htmp _)] + exact hyframe i hif htmp + obtain ⟨y, hy, hIy⟩ := loop_invariant_state_charged I (iterationStep body d₀) + (fun q => memoryCost (body (d₀, q.1)) q.2 + work (d₀, q.1) q.2) + (fun q y hI => by simp [Cond.Holds, hI.2.2.2.2.1, hI.2.2.2.2.2.1]) hbody hIz + rw [iterationSum_eq] at hy + have hfinal := iterate_result_state body d₀ fuel a₀ s₀ + rw [← hfinal] at hIy + obtain ⟨_, hym, _, hys, _, _, _, _, hyf⟩ := hIy + refine ⟨y, (ha.seq (hc.seq (hz.seq hy))).mono ?_, ?_, ?_, hyf⟩ + · nlinarith + · change memoryState frontier y = (Memory.spec w).clientState s₀ (iterate body d₀ fuel a₀) + rw [clientState_width w] + exact hym + · intro i + change y.regs (st i) = output ((Memory.spec w).clientResult s₀ (iterate body d₀ fuel a₀)) i + rw [clientResult_width w] + exact hys i + +end Realizes +end Cslib.WordRAM.Realization diff --git a/Complexity/Computability/WordRAM/Realization/Program.lean b/Complexity/Computability/WordRAM/Realization/Program.lean new file mode 100644 index 0000000000..5bd3f46df6 --- /dev/null +++ b/Complexity/Computability/WordRAM/Realization/Program.lean @@ -0,0 +1,345 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.WordRAM.Realization.Basic + +/-! +# Flat programs from graded memory-client realizations + +`Realizes.exists_program` projects the existing realization certificate through +`Refines.executes`. One emitter, scratch size and exchange constant precede every runtime +argument, word width and initial memory. A statically selected coordinate of the faithful result +encoding is observed by the existing `Code.program`; its final halt costs one instruction. +The emitted body is shared by all coordinate observations. + +`Realizes.exists_program` takes already installed arguments and frontier. +`Realizes.exists_init_program` instead executes `inputPrefix` from `Data.init`, charging +`2 * k + 5` instructions to install the first `k` input words and frontier. Its explicit layout, +input-word and frontier-fit premises exclude free preparation and address overflow. The initial +memory is retained in full. The whole-memory postcondition and register frame remain available +through `Realizes.exists_refines`; no new execution judgment is introduced here. + +## Main definitions + +* `inputLoads`: a fixed sequence loading consecutive cells into source registers. +* `inputPrefix`: the native register and frontier installation prefix. +* `inputState`: the functional memory state of the native list-input convention. + +## Main results + +* `Realizes.exists_program`: a uniform flat program for every static output coordinate, with + bound `C * (memoryCost + work + 1) + 1`, including the trailing halt. +* `inputPrefix_exec`: a charged, memory-preserving native list-input prefix. +* `Realizes.exists_init_program`: the same uniform flat-program bound from `Data.init`, + absorbing the actual prefix into its exchange constant. +* `Realizes.exists_unit_program`, `Realizes.exists_init_unit_program`: zero-output clients + execute a zero write and halt, charging both instructions at every word width. + +## References + +This semantic projection is original infrastructure over the existing flat compiler. +-/ + +@[expose] public section + +namespace Cslib.WordRAM.Realization + +open Cslib.DataStructure + +/-- Install consecutive input cells in the given source registers. The terminal self-copy +provides the empty case without adding a skip instruction to the native language. -/ +def inputLoads {r : ℕ} (ptr : Fin r) : + {k : ℕ} → (Fin k → Fin r) → ℕ → Code .exact r + | 0, _, _ => .op (.copy ptr ptr) + | _ + 1, src, offset => + .seq (.op (.const ptr (offset + 1))) + (.seq (.op (.load (src 0) ptr)) (inputLoads ptr (fun i => src i.succ) (offset + 1))) + +private theorem inputLoads_exec {r k w : ℕ} (ptr : Fin r) (src : Fin k → Fin r) + (offset : ℕ) (x : Data r) (hi : Function.Injective src) + (hd : ∀ i, src i ≠ ptr) (hfit : ∀ i : Fin k, Fits w (offset + i.val + 1)) : + ∃ y, ExecWithin w (inputLoads ptr src offset) x y (2 * k + 1) ∧ + y.mem = x.mem ∧ (∀ i, y.regs (src i) = x.mem (offset + i.val + 1)) ∧ + ∀ j, j ≠ ptr → (∀ i, src i ≠ j) → y.regs j = x.regs j := by + induction k generalizing offset x with + | zero => + refine ⟨x, ?_, rfl, (fun i => Fin.elim0 i), ?_⟩ + · simpa [inputLoads, Data.set] using + (ExecWithin.copy (B := .exact) (w := w) (x := x) (d := ptr) (s := ptr)) + · intro j _ _ + rfl + | succ k ih => + let x₁ := x.set ptr (offset + 1) + let x₂ := x₁.set (src 0) (x.mem (offset + 1)) + have e₁ : ExecWithin (B := .exact) w (.op (.const ptr (offset + 1))) x x₁ 1 := + ExecWithin.const (by simpa using hfit 0) + have e₂ : ExecWithin (B := .exact) w (.op (.load (src 0) ptr)) x₁ x₂ 1 := by + simpa [x₂, x₁] using + (ExecWithin.load (B := .exact) (w := w) (x := x₁) (d := src 0) (a := ptr)) + obtain ⟨y, ey, hm, ho, hf⟩ := ih (fun i => src i.succ) (offset + 1) x₂ + (hi.comp (Fin.succ_injective _)) (fun i => hd i.succ) + (fun i => by simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using hfit i.succ) + refine ⟨y, ?_, hm, ?_, ?_⟩ + · exact (e₁.seq (e₂.seq ey)).mono (by omega) + · intro i + refine Fin.cases ?_ (fun j => ?_) i + · rw [hf (src 0) (hd 0) (fun j h => by + have := hi h + exact Fin.succ_ne_zero j this)] + simp [x₂] + · simpa [x₂, x₁, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using ho j + · intro j hj hs + rw [hf j hj (fun i => hs i.succ)] + simp [x₂, x₁, (hs 0).symm, hj] + +/-- A native entry prefix installs the frontier and the first `k` input words. All data starts +from the existing `Data.init` convention; register installation is charged. -/ +def inputPrefix {r k : ℕ} (frontier ptr : Fin r) (src : Fin k → Fin r) : Code .exact r := + .seq (.op (.const ptr 0)) + (.seq (.op (.load frontier ptr)) + (.seq (.op (.const ptr 1)) + (.seq (.op (.exactBin .add frontier frontier ptr)) (inputLoads ptr src 0)))) + +/-- The whole input memory, with the first free address immediately after its last word. -/ +def inputState (words : List ℕ) : Memory.State := + ⟨(Data.init words : Data 0).mem, words.length + 1⟩ + +/-- Argument installation takes at most `2 * k + 5` native instructions. Its memory is unchanged; +only the frontier, pointer and source registers can change. The frontier-fit premise also pays +for the constant one and every input address. -/ +theorem inputPrefix_exec {r k w : ℕ} (frontier ptr : Fin r) (src : Fin k → Fin r) + (words : List ℕ) (hi : Function.Injective src) (hp : ptr ≠ frontier) + (hd : ∀ i, src i ≠ ptr) (hf : ∀ i, src i ≠ frontier) + (hk : k ≤ words.length) (hw : Fits w (words.length + 1)) (hin : InputFits w words) : + ∃ y, ExecWithin w (inputPrefix frontier ptr src) (Data.init words) y (2 * k + 5) ∧ + y.Bounded w ∧ memoryState frontier y = inputState words ∧ + (∀ i, y.regs (src i) = words.getD i.val 0) ∧ + ∀ j, j ≠ frontier → j ≠ ptr → (∀ i, src i ≠ j) → y.regs j = 0 := by + let x : Data r := Data.init words + let x₁ := x.set ptr 0 + let x₂ := x₁.set frontier words.length + let x₃ := x₂.set ptr 1 + let x₄ := x₃.set frontier (words.length + 1) + have h1 : Fits w 1 := hw.of_le (by omega) + have e₁ : ExecWithin (B := .exact) w (.op (.const ptr 0)) x x₁ 1 := ExecWithin.const (fits_zero w) + have e₂ : ExecWithin (B := .exact) w (.op (.load frontier ptr)) x₁ x₂ 1 := by + simpa [x₂, x₁, x] using + (ExecWithin.load (B := .exact) (w := w) (x := x₁) (d := frontier) (a := ptr)) + have e₃ : ExecWithin (B := .exact) w (.op (.const ptr 1)) x₂ x₃ 1 := ExecWithin.const h1 + have e₄ : ExecWithin w (.op (.exactBin .add frontier frontier ptr)) x₃ x₄ 1 := by + apply ExecWithin.op + simp [Op.eval_exactBin, BinOp.evalExact, x₄, x₃, x₂, hp.symm, Data.put_of_fits hw] + obtain ⟨y, ey, hm, ho, hframe⟩ := inputLoads_exec ptr src 0 x₄ hi hd + (fun i => hw.of_le (by omega)) + have he : ExecWithin w (inputPrefix frontier ptr src) x y (2 * k + 5) := by + exact (e₁.seq (e₂.seq (e₃.seq (e₄.seq ey)))).mono (by omega) + refine ⟨y, he, he.bounded (Data.Bounded.init hin), ?_, ?_, ?_⟩ + · apply Memory.State.ext + · exact hm + · change y.regs frontier = words.length + 1 + rw [hframe frontier hp.symm hf] + simp [x₄] + · intro i + simpa [x₄, x₃, x₂, x₁, x] using ho i + · intro j hj hptr hs + rw [hframe j hptr hs] + simp [x₄, x₃, x₂, x₁, x, hj, hptr] + +end Cslib.WordRAM.Realization + +namespace Cslib.WordRAM.Realization.Realizes + +open Cslib.DataStructure + +variable {B : Basis} {k l : ℕ} {δ α : Type} + {p : δ → Memory.Prog α} {input : δ ↪ (Fin k → ℕ)} + {output : α ↪ (Fin l → ℕ)} {safe : ℕ → δ → Memory.State → Prop} + {work : δ → Memory.State → ℕ} + +/-- Each static coordinate of a faithfully encoded result has one flat program, independent of +the runtime input, width and memory. The selected halt observes an output register of the same +emitted body; the clock includes that halt. Arguments and frontier are explicit entry premises. +For an empty result register vector this makes no scalar observation. -/ +theorem exists_program (h : Realizes B p input output safe work) : + ∃ n C : ℕ, + ∃ emit : ∀ {r : ℕ}, (frontier : Fin r) → (Fin k → Fin r) → + (Fin (l + n + 1) → Fin r) → Code B r, + ∀ {r : ℕ} (frontier : Fin r) (src : Fin k → Fin r) + (tmp : Fin (l + n + 1) → Fin r), + Function.Injective tmp → (∀ i j, src i ≠ tmp j) → + (∀ j, tmp j ≠ frontier) → (∀ i, src i ≠ frontier) → + ∀ (i : Fin l) (w : ℕ) (d : δ) (x : Data r), + x.Bounded w → x.regs ∘ src = input d → safe w d (memoryState frontier x) → + (Memory.spec w).ValidHistory (memoryState frontier x) + ((Memory.spec w).clientHistory (memoryState frontier x) (p d)) → + ∃ t, Executes w ((emit frontier src tmp).program (tmp (Fin.castAdd (n + 1) i))) + ⟨0, x⟩ (output ((Memory.spec w).clientResult (memoryState frontier x) (p d)) i) t ∧ + t ≤ C * (memoryCost (p d) (memoryState frontier x) + + work d (memoryState frontier x) + 1) + 1 := by + obtain ⟨n, C, emit, he⟩ := h.exists_refines + refine ⟨n, C, emit, ?_⟩ + intro r frontier src tmp hi hd hf hs i w d x hx hin hsafe hv + exact (he frontier src tmp hi hd hf hs w d).executes + (tmp (Fin.castAdd (n + 1) i)) (fun a => output a i) (fun _ _ _ hout => hout.2 i) + ⟨rfl, hx, hin, hsafe, hv⟩ + +/-- A flat exact-basis program starts from the native list-input convention and charges both +argument installation and its trailing halt. The first `k` cells encode the argument; the whole +input memory and its frontier are passed to the client. The fixed installation cost is absorbed +into one exchange constant before every width and runtime argument. -/ +theorem exists_init_program (h : Realizes .exact p input output safe work) + (raw : δ → List ℕ) (hlayout : ∀ d (i : Fin k), (raw d).getD i.val 0 = input d i) : + ∃ n C : ℕ, + ∃ emit : ∀ {r : ℕ}, (frontier : Fin r) → (Fin k → Fin r) → + (Fin (l + n + 1) → Fin r) → Code .exact r, + ∀ {r : ℕ} (frontier : Fin r) (src : Fin k → Fin r) + (tmp : Fin (l + n + 1) → Fin r), + Function.Injective src → Function.Injective tmp → (∀ i j, src i ≠ tmp j) → + (∀ j, tmp j ≠ frontier) → (∀ i, src i ≠ frontier) → + ∀ (i : Fin l) (w : ℕ) (d : δ), + k ≤ (raw d).length → Fits w ((raw d).length + 1) → InputFits w (raw d) → + safe w d (inputState (raw d)) → + (Memory.spec w).ValidHistory (inputState (raw d)) + ((Memory.spec w).clientHistory (inputState (raw d)) (p d)) → + ∃ t, Executes w + ((Code.seq (inputPrefix frontier (tmp (Fin.last (l + n))) src) + (emit frontier src tmp)).program (tmp (Fin.castAdd (n + 1) i))) + (State.init (raw d)) + (output ((Memory.spec w).clientResult (inputState (raw d)) (p d)) i) t ∧ + t ≤ C * (memoryCost (p d) (inputState (raw d)) + + work d (inputState (raw d)) + 1) + 1 := by + obtain ⟨n, C, emit, he⟩ := h + refine ⟨n, C + (2 * k + 5), emit, ?_⟩ + intro r frontier src tmp hsrc htmp hd hf hs i w d hk hw hin hsafe hv + obtain ⟨x, ex, hx, hm, hwords, _⟩ := + inputPrefix_exec frontier (tmp (Fin.last (l + n))) src (raw d) hsrc + (hf _) (fun j => hd j _) hs hk hw hin + have harg : x.regs ∘ src = input d := by + funext j + exact (hwords j).trans (hlayout d j) + obtain ⟨y, ey, _, hout, _⟩ := (he frontier src tmp htmp hd hf hs).2 w d x hx harg + (hm.symm ▸ hsafe) (hm.symm ▸ hv) + rw [hm] at ey hout + obtain ⟨t, ht, et⟩ := ex.seq ey + refine ⟨t + 1, ?_, ?_⟩ + · simpa only [State.init, hout i] using et.executes (tmp (Fin.castAdd (n + 1) i)) + · have hpos : 1 ≤ memoryCost (p d) (inputState (raw d)) + + work d (inputState (raw d)) + 1 := by omega + have hover := Nat.mul_le_mul_left (2 * k + 5) hpos + simp only [Nat.mul_one] at hover + rw [Nat.add_mul] + omega + +/-- A Unit-returning client needs no output coordinate. Execute an actual zero constant after +its body to obtain a scalar observation, preserving the entire represented client state. +The extra instruction fits every width, including zero. -/ +theorem exists_unit_refines {p : δ → Memory.Prog Unit} {output : Unit ↪ (Fin 0 → ℕ)} + (h : Realizes B p input output safe work) : + ∃ n C : ℕ, + ∃ emit : ∀ {r : ℕ}, (frontier : Fin r) → (Fin k → Fin r) → + (Fin (0 + n + 1) → Fin r) → Code B r, + ∀ {r : ℕ} (frontier : Fin r) (src : Fin k → Fin r) + (tmp : Fin (0 + n + 1) → Fin r), + Function.Injective tmp → (∀ i j, src i ≠ tmp j) → + (∀ j, tmp j ≠ frontier) → (∀ i, src i ≠ frontier) → + ∀ (w : ℕ) (d : δ), + Refines (D := Memory.spec w) w + (fun s x => s = memoryState frontier x ∧ x.Bounded w ∧ x.regs ∘ src = input d ∧ + safe w d s ∧ (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (p d))) + (p d) + (fun _ s y => memoryState frontier y = s ∧ y.regs (tmp 0) = 0) + (fun s _ => C * (memoryCost (p d) s + work d s + 1) + 1) + (.seq (emit frontier src tmp) (.op (.const (tmp 0) 0))) := by + obtain ⟨n, C, emit, he⟩ := h.exists_refines + refine ⟨n, C, emit, ?_⟩ + intro r frontier src tmp hi hd hf hs w d + apply Refines.ofFn + intro s x hx + obtain ⟨hv, y, ey, hm, _⟩ := (he frontier src tmp hi hd hf hs w d).toOfFn hx + refine ⟨hv, y.set (tmp 0) 0, ey.seq (ExecWithin.const (fits_zero w)), ?_, ?_⟩ + · apply Eq.trans ?_ hm + apply Memory.State.ext + · rfl + · exact Function.update_of_ne (hf 0).symm _ _ + · simp + +/-- A zero-output Unit client has a uniform flat scalar observation after a charged zero write +and halt. Both instructions are included, without a positive-width premise. -/ +theorem exists_unit_program {p : δ → Memory.Prog Unit} {output : Unit ↪ (Fin 0 → ℕ)} + (h : Realizes B p input output safe work) : + ∃ n C : ℕ, + ∃ emit : ∀ {r : ℕ}, (frontier : Fin r) → (Fin k → Fin r) → + (Fin (0 + n + 1) → Fin r) → Code B r, + ∀ {r : ℕ} (frontier : Fin r) (src : Fin k → Fin r) + (tmp : Fin (0 + n + 1) → Fin r), + Function.Injective tmp → (∀ i j, src i ≠ tmp j) → + (∀ j, tmp j ≠ frontier) → (∀ i, src i ≠ frontier) → + ∀ (w : ℕ) (d : δ) (x : Data r), + x.Bounded w → x.regs ∘ src = input d → safe w d (memoryState frontier x) → + (Memory.spec w).ValidHistory (memoryState frontier x) + ((Memory.spec w).clientHistory (memoryState frontier x) (p d)) → + ∃ t, Executes w + ((Code.seq (emit frontier src tmp) (.op (.const (tmp 0) 0))).program (tmp 0)) + ⟨0, x⟩ 0 t ∧ + t ≤ C * (memoryCost (p d) (memoryState frontier x) + + work d (memoryState frontier x) + 1) + 2 := by + obtain ⟨n, C, emit, he⟩ := h.exists_unit_refines + refine ⟨n, C, emit, ?_⟩ + intro r frontier src tmp hi hd hf hs w d x hx hin hsafe hv + simpa only [Nat.add_assoc] using + (he frontier src tmp hi hd hf hs w d).executes (tmp 0) (fun _ => 0) + (fun _ _ _ hout => hout.2) ⟨rfl, hx, hin, hsafe, hv⟩ + +/-- Unit-returning clients can start from `Data.init` too. Argument installation is charged and +absorbed into the uniform exchange constant; the real zero write and trailing halt cost two +further instructions. -/ +theorem exists_init_unit_program {p : δ → Memory.Prog Unit} {output : Unit ↪ (Fin 0 → ℕ)} + (h : Realizes .exact p input output safe work) + (raw : δ → List ℕ) (hlayout : ∀ d (i : Fin k), (raw d).getD i.val 0 = input d i) : + ∃ n C : ℕ, + ∃ emit : ∀ {r : ℕ}, (frontier : Fin r) → (Fin k → Fin r) → + (Fin (0 + n + 1) → Fin r) → Code .exact r, + ∀ {r : ℕ} (frontier : Fin r) (src : Fin k → Fin r) + (tmp : Fin (0 + n + 1) → Fin r), + Function.Injective src → Function.Injective tmp → (∀ i j, src i ≠ tmp j) → + (∀ j, tmp j ≠ frontier) → (∀ i, src i ≠ frontier) → + ∀ (w : ℕ) (d : δ), + k ≤ (raw d).length → Fits w ((raw d).length + 1) → InputFits w (raw d) → + safe w d (inputState (raw d)) → + (Memory.spec w).ValidHistory (inputState (raw d)) + ((Memory.spec w).clientHistory (inputState (raw d)) (p d)) → + ∃ t, Executes w + ((Code.seq (inputPrefix frontier (tmp (Fin.last (0 + n))) src) + (.seq (emit frontier src tmp) (.op (.const (tmp 0) 0)))).program (tmp 0)) + (State.init (raw d)) 0 t ∧ + t ≤ C * (memoryCost (p d) (inputState (raw d)) + + work d (inputState (raw d)) + 1) + 2 := by + obtain ⟨n, C, emit, he⟩ := h.exists_unit_refines + refine ⟨n, C + (2 * k + 5), emit, ?_⟩ + intro r frontier src tmp hsrc htmp hd hf hs w d hk hw hin hsafe hv + obtain ⟨x, ex, hx, hm, hwords, _⟩ := + inputPrefix_exec frontier (tmp (Fin.last (0 + n))) src (raw d) hsrc + (hf _) (fun j => hd j _) hs hk hw hin + have harg : x.regs ∘ src = input d := by + funext j + exact (hwords j).trans (hlayout d j) + obtain ⟨_, y, ey, _, hout⟩ := (he frontier src tmp htmp hd hf hs w d).toOfFn + ⟨rfl, hx, harg, hm.symm ▸ hsafe, hm.symm ▸ hv⟩ + rw [hm] at ey + obtain ⟨t, ht, et⟩ := ex.seq ey + refine ⟨t + 1, ?_, ?_⟩ + · simpa only [State.init, hout] using et.executes (tmp 0) + · have hpos : 1 ≤ memoryCost (p d) (inputState (raw d)) + + work d (inputState (raw d)) + 1 := by omega + have hover := Nat.mul_le_mul_left (2 * k + 5) hpos + simp only [Nat.mul_one] at hover + rw [Nat.add_mul] + omega + +end Cslib.WordRAM.Realization.Realizes diff --git a/ComplexityTests/WordRAMRealizationLoop.lean b/ComplexityTests/WordRAMRealizationLoop.lean new file mode 100644 index 0000000000..cc9fdb205f --- /dev/null +++ b/ComplexityTests/WordRAMRealizationLoop.lean @@ -0,0 +1,193 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: local-only (regression tests for realization loop infrastructure) + +public import Complexity.Computability.WordRAM.Realization.Loop +import Complexity.Computability.WordRAM.Realization.Glue +import Complexity.Computability.WordRAM.Realization.Primitive + +/-! +# Runtime-loop regression clients + +A query-free identity loop has zero memory charge but a local-work charge growing with runtime +fuel. Its uniform native witness also executes at zero word width when the state and fuel are +zero, so materializing the decrement constant in the positive body cannot break the empty case. +-/ + +public section + +namespace Cslib.WordRAM.Realization.Tests + +open Cslib.DataStructure + +private def unitInput : Unit ↪ (Fin 0 → ℕ) := + (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding + +private def wordOutput : ℕ ↪ (Fin 1 → ℕ) := + (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding + +private def bodyInput : Unit × ℕ ↪ (Fin (0 + 1) → ℕ) := + (unitInput.prodMap wordOutput).trans (Fin.appendEquiv 0 1).toEmbedding + +/-- A certified word copy performs local work without any memory query. -/ +@[expose] def identityBody (d : Unit × ℕ) : Memory.Prog ℕ := pure d.2 + +private theorem identityBody_realizes : + Realizes .exact identityBody bodyInput wordOutput + (fun w d _ => Fits w d.2) (fun _ _ => 1) := by + unfold identityBody + have h : GlueComputes .exact (fun _ : Fin 1 → ℕ => True) + (fun v => v 0) (fun v => v 0) 1 := GlueComputes.proj 0 (fun _ _ => le_rfl) + simpa [identityBody, bodyInput, unitInput, wordOutput, Fin.appendEquiv, + Fin.append, Fin.addCases] using Realizes.glue bodyInput h + +/-- A single body certificate is reused before all runtime fuel and data choices. -/ +private theorem identityLoop_realizes : + Realizes .exact (fun d : (Unit × ℕ) × ℕ => iterate identityBody d.1.1 d.2 d.1.2) + ((bodyInput.prodMap wordOutput).trans (Fin.appendEquiv (0 + 1) 1).toEmbedding) + wordOutput (fun w d s => iterationSafe identityBody (fun w d _ => Fits w d.2) + w d.1.1 d.2 d.1.2 s) + (fun d s => iterationWork identityBody (fun _ _ => 1) d.1.1 d.2 d.1.2 s) := + Realizes.iterateRuntime unitInput wordOutput identityBody_realizes + +private theorem identity_iterate (n a : ℕ) : iterate identityBody () n a = pure a := by + induction n with + | zero => rfl + | succ n ih => simpa only [iterate, identityBody, pure_bind] using ih + +example (n a : ℕ) (s : Memory.State) : memoryCost (iterate identityBody () n a) s = 0 := by + rw [identity_iterate] + rfl + +private theorem identity_work (n a : ℕ) (s : Memory.State) : + iterationWork identityBody (fun _ _ => 1) () n a s = 2 * n := by + induction n generalizing a s with + | zero => rfl + | succ n ih => + simp only [iterationWork, ih] + omega + +/-- Query-free iteration still has increasing certified local work. -/ +theorem queryFree_work_grows (n m a : ℕ) (s : Memory.State) (h : n < m) : + iterationWork identityBody (fun _ _ => 1) () n a s < + iterationWork identityBody (fun _ _ => 1) () m a s := by + rw [identity_work, identity_work] + omega + +/-- The uniform loop witness has a genuine zero-width, zero-fuel flat execution. -/ +example : ∃ r, ∃ p : Program .exact r, ∃ steps, + Executes 0 p ⟨0, ⟨fun _ => 0, fun _ => 0⟩⟩ 0 steps := by + obtain ⟨n, C, emit, he⟩ := identityLoop_realizes + let r := 2 + (1 + n + 1) + 1 + let frontier : Fin r := ⟨r - 1, by omega⟩ + let src : Fin 2 → Fin r := fun i => ⟨i.val, by omega⟩ + let tmp : Fin (1 + n + 1) → Fin r := fun i => ⟨2 + i.val, by omega⟩ + have hi : Function.Injective tmp := by + intro i j h + apply Fin.ext + have hh := congrArg (fun a : Fin r => a.val) h + dsimp only [tmp] at hh + omega + have hd (i : Fin 2) (j : Fin (1 + n + 1)) : src i ≠ tmp j := by + intro h + have hh := congrArg (fun a : Fin r => a.val) h + dsimp only [src, tmp] at hh + omega + have hf (j : Fin (1 + n + 1)) : tmp j ≠ frontier := by + intro h + have hh := congrArg (fun a : Fin r => a.val) h + dsimp only [tmp, frontier, r] at hh + omega + have hs (i : Fin 2) : src i ≠ frontier := by + intro h + have hh := congrArg (fun a : Fin r => a.val) h + dsimp only [src, frontier, r] at hh + omega + let x : Data r := ⟨fun _ => 0, fun _ => 0⟩ + have hx : x.Bounded 0 := ⟨fun _ => fits_zero 0, fun _ => fits_zero 0⟩ + have hin : x.regs ∘ src = + ((bodyInput.prodMap wordOutput).trans (Fin.appendEquiv (0 + 1) 1).toEmbedding) + (((), 0), 0) := by + funext i + fin_cases i <;> rfl + obtain ⟨y, ⟨steps, _, hy⟩, _, hout, _⟩ := + (he frontier src tmp hi hd hf hs).2 0 (((), 0), 0) x hx hin trivial trivial + have ho : y.regs (tmp 0) = 0 := hout 0 + refine ⟨r, (emit frontier src tmp).program (tmp 0), steps + 1, ?_⟩ + simpa only [ho] using hy.executes (tmp 0) + +private def decrementBody (d : Unit × ℕ) : Memory.Prog ℕ := pure (d.2 - 1) + +private theorem decrementBody_realizes : + Realizes .exact decrementBody bodyInput wordOutput + (fun w d _ => 1 ≤ d.2 ∧ Fits w d.2) (fun _ _ => 3) := by + unfold decrementBody + have hp : GlueComputes .exact (fun v : Fin 1 → ℕ => 1 ≤ v 0) + (fun v => v 0) (fun v => v 0) 1 := GlueComputes.proj 0 (fun _ _ => le_rfl) + have hc : GlueComputes .exact (fun v : Fin 1 → ℕ => 1 ≤ v 0) + (fun _ => 1) (fun v => v 0) 1 := GlueComputes.const 1 (fun _ h => h) + have h := GlueComputes.bin_exact hp hc .sub + (fun v hv => by simp [BinOp.evalExact, hv, BinOp.eval]) + (fun v _ => Nat.sub_le (v 0) 1) + simpa [bodyInput, unitInput, wordOutput, Fin.appendEquiv, + Fin.append, Fin.addCases, BinOp.eval] using Realizes.glue bodyInput h + +private theorem decrementLoop_realizes : + Realizes .exact (fun d : (Unit × ℕ) × ℕ => iterate decrementBody d.1.1 d.2 d.1.2) + ((bodyInput.prodMap wordOutput).trans (Fin.appendEquiv (0 + 1) 1).toEmbedding) + wordOutput (fun w d s => iterationSafe decrementBody + (fun w d _ => 1 ≤ d.2 ∧ Fits w d.2) w d.1.1 d.2 d.1.2 s) + (fun d s => iterationWork decrementBody (fun _ _ => 3) d.1.1 d.2 d.1.2 s) := + Realizes.iterateRuntime unitInput wordOutput decrementBody_realizes + +example (s : Memory.State) : (Memory.spec 4).clientResult s + (iterate decrementBody () 3 7) = 4 := rfl + +example (s : Memory.State) : iterationSafe decrementBody + (fun w d _ => 1 ≤ d.2 ∧ Fits w d.2) 4 () 3 7 s := by + change (1 ≤ 7 ∧ Fits 4 7) ∧ (1 ≤ 6 ∧ Fits 4 6) ∧ (1 ≤ 5 ∧ Fits 4 5) ∧ True + decide + +example (s : Memory.State) : iterationSafe decrementBody + (fun w d _ => 1 ≤ d.2 ∧ Fits w d.2) 0 () 0 0 s := trivial + +private def pointerBody (d : Unit × ℕ) : Memory.Prog ℕ := Memory.read d.2 + +private theorem pointerBody_realizes : + Realizes .exact pointerBody bodyInput wordOutput + (fun _ _ _ => True) (fun _ _ => 0) := by + unfold pointerBody + simpa [bodyInput, unitInput, wordOutput, Fin.appendEquiv, Fin.append, Fin.addCases] using + Realizes.read (B := .exact) bodyInput (0 : Fin 1) + +/-- The mutable state supplies each next address; the loop is not repeated at its first address. -/ +private theorem pointerLoop_realizes : + Realizes .exact (fun d : (Unit × ℕ) × ℕ => iterate pointerBody d.1.1 d.2 d.1.2) + ((bodyInput.prodMap wordOutput).trans (Fin.appendEquiv (0 + 1) 1).toEmbedding) + wordOutput (fun w d s => iterationSafe pointerBody (fun _ _ _ => True) + w d.1.1 d.2 d.1.2 s) + (fun d s => iterationWork pointerBody (fun _ _ => 0) d.1.1 d.2 d.1.2 s) := + Realizes.iterateRuntime unitInput wordOutput pointerBody_realizes + +private def linkedMemory : Memory.State := + ⟨fun a => if a = 0 then 1 else if a = 1 then 2 else 0, 3⟩ + +example : (Memory.spec 2).clientResult linkedMemory (iterate pointerBody () 2 0) = 2 := rfl + +example : (Memory.spec 2).clientHistory linkedMemory (iterate pointerBody () 2 0) = + [.read 0, .read 1] := rfl + +example : (Memory.spec 2).ValidHistory linkedMemory + ((Memory.spec 2).clientHistory linkedMemory (iterate pointerBody () 2 0)) := by decide + +example : Memory.WellFormed 2 linkedMemory := by + refine ⟨by decide, fun a => ?_⟩ + change Fits 2 (if a = 0 then 1 else if a = 1 then 2 else 0) + split_ifs <;> decide + +end Cslib.WordRAM.Realization.Tests diff --git a/ComplexityTests/WordRAMRealizationProgram.lean b/ComplexityTests/WordRAMRealizationProgram.lean new file mode 100644 index 0000000000..808b775985 --- /dev/null +++ b/ComplexityTests/WordRAMRealizationProgram.lean @@ -0,0 +1,294 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Computability.WordRAM.Realization.Program + +/-! Nonvacuous flat-program projections with uniform code and clock constants, for both +already installed arguments and an actually charged native list-input prefix. The former +includes width zero; the latter explicitly checks frontier overflow and the empty-input case. -/ + +namespace ComplexityTests.WordRAMRealizationProgram + +open Cslib.WordRAM Cslib.WordRAM.Realization Cslib.DataStructure + +private def word : ℕ ↪ (Fin 1 → ℕ) := + ⟨fun d _ => d, fun _ _ h => congrFun h 0⟩ + +private theorem copy_realizes : + Realizes .exact (fun d : ℕ => (pure d : Memory.Prog ℕ)) word word + (fun _ _ _ => True) (fun _ _ => 0) := by + refine ⟨0, 1, fun _ src tmp => .op (.copy (tmp 0) (src 0)), ?_⟩ + intro r frontier src tmp _ _ hf _ + refine ⟨by simp [Code.ReadsWidth, Op.ReadsWidth], ?_⟩ + intro w d x _ hin _ _ + have harg : x.regs (src 0) = d := congrFun hin 0 + refine ⟨x.set (tmp 0) d, ?_, ?_, ?_, ?_⟩ + · change ExecWithin _ _ _ _ 1 + simpa [harg] using + (ExecWithin.copy (B := .exact) (w := w) (x := x) (d := tmp 0) (s := src 0)) + · apply Memory.State.ext + · rfl + · exact Function.update_of_ne (hf 0).symm _ _ + · intro i + have hi : i = 0 := Fin.eq_zero i + subst i + change (x.set (tmp 0) d).regs (tmp 0) = d + simp [Data.set] + · intro i _ htmp + exact Function.update_of_ne (htmp 0).symm _ _ + +private def entry (r d : ℕ) : Data r := + ⟨fun i => if i.val = 0 then d else 0, fun _ => 0⟩ + +-- The register count, program and exchange constant precede every width and argument. +example : ∃ (r C : ℕ) (p : Program .exact r), + ∀ w d, Fits w d → + ∃ t, Executes w p ⟨0, entry r d⟩ d t ∧ t ≤ C + 1 := by + obtain ⟨n, C, emit, he⟩ := copy_realizes.exists_program + let m := 1 + n + 1 + let r := m + 2 + let frontier : Fin r := ⟨1, by dsimp [r, m]; omega⟩ + let src : Fin 1 → Fin r := fun _ => ⟨0, by dsimp [r, m]; omega⟩ + let tmp : Fin (1 + n + 1) → Fin r := fun j => ⟨j.val + 2, by dsimp [r, m]; omega⟩ + have hi : Function.Injective tmp := by + intro a b h + apply Fin.ext + have := congrArg Fin.val h + dsimp [tmp] at this + omega + have hd : ∀ i j, src i ≠ tmp j := by + intro i j h + have := congrArg Fin.val h + change 0 = j.val + 2 at this + omega + have hf : ∀ j, tmp j ≠ frontier := by + intro j h + have := congrArg Fin.val h + change j.val + 2 = 1 at this + omega + have hs : ∀ i, src i ≠ frontier := by + intro i h + have := congrArg Fin.val h + change 0 = 1 at this + omega + refine ⟨r, C, (emit frontier src tmp).program (tmp (Fin.castAdd (n + 1) (0 : Fin 1))), ?_⟩ + intro w d hfit + have hx : (entry r d).Bounded w := by + constructor + · intro i + by_cases h : i.val = 0 + · change Fits w (if i.val = 0 then d else 0) + rwa [ite_eq_left h] + · change Fits w (if i.val = 0 then d else 0) + rw [ite_eq_right h] + exact fits_zero w + · intro a + exact fits_zero w + have hin : (entry r d).regs ∘ src = word d := by + funext i + rfl + obtain ⟨t, ht, htime⟩ := he frontier src tmp hi hd hf hs 0 w d (entry r d) hx hin + trivial (by trivial) + change t ≤ C * (0 + 0 + 1) + 1 at htime + exact ⟨t, ht, by simpa using htime⟩ + +-- One fixed flat program now includes actual argument and frontier installation. +example : ∃ (r C : ℕ) (p : Program .exact r), + ∀ w d, Fits w 2 → Fits w d → + ∃ t, Executes w p (State.init [d]) d t ∧ t ≤ C + 1 := by + obtain ⟨n, C, emit, he⟩ := copy_realizes.exists_init_program (fun d => [d]) (by + intro d i + have hi : i = 0 := Fin.eq_zero i + subst i + rfl) + let m := 1 + n + 1 + let r := m + 2 + let frontier : Fin r := ⟨1, by dsimp [r, m]; omega⟩ + let src : Fin 1 → Fin r := fun _ => ⟨0, by dsimp [r, m]; omega⟩ + let tmp : Fin (1 + n + 1) → Fin r := fun j => ⟨j.val + 2, by dsimp [r, m]; omega⟩ + have hi : Function.Injective tmp := by + intro a b h + apply Fin.ext + have := congrArg Fin.val h + dsimp [tmp] at this + omega + have hd : ∀ i j, src i ≠ tmp j := by + intro i j h + have := congrArg Fin.val h + change 0 = j.val + 2 at this + omega + have hf : ∀ j, tmp j ≠ frontier := by + intro j h + have := congrArg Fin.val h + change j.val + 2 = 1 at this + omega + have hs : ∀ i, src i ≠ frontier := by + intro i h + have := congrArg Fin.val h + change 0 = 1 at this + omega + refine ⟨r, C, (Code.seq (inputPrefix frontier (tmp (Fin.last (1 + n))) src) + (emit frontier src tmp)).program (tmp (Fin.castAdd (n + 1) (0 : Fin 1))), ?_⟩ + intro w d h2 hfit + have hin : InputFits w [d] := by + refine ⟨h2.of_le (by simp), ?_⟩ + intro v hv + simp only [List.mem_singleton] at hv + exact hv.symm ▸ hfit + obtain ⟨t, ht, htime⟩ := he frontier src tmp (fun _ _ _ => Subsingleton.elim _ _) hi + hd hf hs 0 w d (by simp) h2 hin trivial (by trivial) + change t ≤ C * (0 + 0 + 1) + 1 at htime + exact ⟨t, ht, by simpa using htime⟩ + +private def unitWords : Unit ↪ (Fin 0 → ℕ) := + (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding + +private def storeZero {r : ℕ} (src ptr : Fin r) : Code .exact r := + .seq (.op (.const ptr 0)) (.op (.store ptr src)) + +-- The client really writes a cell and returns Unit with zero output coordinates. +private theorem write_realizes : + Realizes .exact (fun d : ℕ => Memory.write 0 d) word unitWords + (fun _ _ _ => True) (fun _ _ => 0) := by + refine ⟨0, 1, fun _ src tmp => storeZero (src 0) (tmp 0), ?_⟩ + intro r frontier src tmp _ hd hf _ + refine ⟨by simp [storeZero, Code.ReadsWidth, Op.ReadsWidth], ?_⟩ + intro w d x _ hin _ _ + have harg : x.regs (src 0) = d := congrFun hin 0 + let y := (x.set (tmp 0) 0).write 0 d + refine ⟨y, ?_, ?_, (fun i => Fin.elim0 i), ?_⟩ + · have e₁ := ExecWithin.const (B := .exact) (x := x) (d := tmp 0) (fits_zero w) + have e₂ := ExecWithin.store (B := .exact) (w := w) (x := x.set (tmp 0) 0) + (a := tmp 0) (s := src 0) + have hs : (x.set (tmp 0) 0).regs (src 0) = d := by + simpa [hd 0 0] using harg + rw [hs] at e₂ + change ExecWithin w (storeZero (src 0) (tmp 0)) x y (1 * (1 + 0 + 1)) + simpa [storeZero] using e₁.seq e₂ + · apply Memory.State.ext + · rfl + · exact Function.update_of_ne (hf 0).symm _ _ + · intro j _ htmp + exact Function.update_of_ne (htmp 0).symm _ _ + +-- The flat Unit write starts at Data.init, not a preinstalled register environment. +example : ∃ (r C : ℕ) (p : Program .exact r), + ∀ w d, Fits w 2 → Fits w d → + ∃ t, Executes w p (State.init [d]) 0 t ∧ t ≤ C * 2 + 2 := by + obtain ⟨n, C, emit, he⟩ := write_realizes.exists_init_unit_program (fun d => [d]) (by + intro d i + have hi : i = 0 := Fin.eq_zero i + subst i + rfl) + let r := (0 + n + 1) + 2 + let frontier : Fin r := ⟨1, by dsimp [r]; omega⟩ + let src : Fin 1 → Fin r := fun _ => ⟨0, by dsimp [r]; omega⟩ + let tmp : Fin (0 + n + 1) → Fin r := fun j => ⟨j.val + 2, by dsimp [r]; omega⟩ + have hi : Function.Injective tmp := by + intro a b h + apply Fin.ext + have := congrArg Fin.val h + dsimp [tmp] at this + omega + have hd : ∀ i j, src i ≠ tmp j := by + intro i j h + have := congrArg Fin.val h + change 0 = j.val + 2 at this + omega + have hf : ∀ j, tmp j ≠ frontier := by + intro j h + have := congrArg Fin.val h + change j.val + 2 = 1 at this + omega + have hs : ∀ i, src i ≠ frontier := by + intro i h + have := congrArg Fin.val h + change 0 = 1 at this + omega + refine ⟨r, C, (Code.seq (inputPrefix frontier (tmp (Fin.last (0 + n))) src) + (.seq (emit frontier src tmp) (.op (.const (tmp 0) 0)))).program (tmp 0), ?_⟩ + intro w d h2 hfit + have hin : InputFits w [d] := by + refine ⟨h2.of_le (by simp), ?_⟩ + intro v hv + simp only [List.mem_singleton] at hv + exact hv.symm ▸ hfit + have hv : (Memory.spec w).ValidHistory (inputState [d]) + ((Memory.spec w).clientHistory (inputState [d]) (Memory.write 0 d)) := by + exact ⟨⟨by simp [inputState], hfit⟩, trivial⟩ + obtain ⟨t, ht, htime⟩ := he frontier src tmp (fun _ _ _ => Subsingleton.elim _ _) hi + hd hf hs w d (by simp) h2 hin trivial hv + change t ≤ C * (1 + 0 + 1) + 2 at htime + exact ⟨t, ht, by simpa using htime⟩ + +-- The same Unit observation supports all widths, including zero, for a pure Unit client. +private theorem pure_unit_realizes : + Realizes .exact (fun _ : Unit => (pure () : Memory.Prog Unit)) unitWords unitWords + (fun _ _ _ => True) (fun _ _ => 0) := by + refine ⟨0, 1, fun _ _ tmp => .op (.copy (tmp 0) (tmp 0)), ?_⟩ + intro r frontier src tmp _ _ _ _ + refine ⟨by simp [Code.ReadsWidth, Op.ReadsWidth], ?_⟩ + intro w d x _ _ _ _ + refine ⟨x, ?_, rfl, (fun i => Fin.elim0 i), fun _ _ _ => rfl⟩ + change ExecWithin w (.op (.copy (tmp 0) (tmp 0))) x x 1 + simpa [Data.set] using + (ExecWithin.copy (B := .exact) (w := w) (x := x) (d := tmp 0) (s := tmp 0)) + +example : ∃ (r C : ℕ) (p : Program .exact r), + ∀ w, ∃ t, Executes w p (State.init []) 0 t ∧ t ≤ C + 2 := by + obtain ⟨n, C, emit, he⟩ := pure_unit_realizes.exists_unit_program + let r := (0 + n + 1) + 1 + let frontier : Fin r := ⟨0, by dsimp [r]; omega⟩ + let src : Fin 0 → Fin r := Fin.elim0 + let tmp : Fin (0 + n + 1) → Fin r := fun j => ⟨j.val + 1, by dsimp [r]; omega⟩ + have hi : Function.Injective tmp := by + intro a b h + apply Fin.ext + have := congrArg Fin.val h + dsimp [tmp] at this + omega + have hf : ∀ j, tmp j ≠ frontier := by + intro j h + have := congrArg Fin.val h + change j.val + 1 = 0 at this + omega + refine ⟨r, C, (Code.seq (emit frontier src tmp) (.op (.const (tmp 0) 0))).program + (tmp 0), ?_⟩ + intro w + have hx : (Data.init [] : Data r).Bounded w := + Data.Bounded.init ⟨fits_zero w, by simp⟩ + obtain ⟨t, ht, htime⟩ := he frontier src tmp hi (fun i => Fin.elim0 i) hf + (fun i => Fin.elim0 i) w () (Data.init []) hx (by funext i; exact Fin.elim0 i) + trivial (by trivial) + change t ≤ C * (0 + 0 + 1) + 2 at htime + exact ⟨t, ht, by simpa [State.init] using htime⟩ + +-- The actual prefix, Unit store and scalar-observation instruction preserve the write. +example : ((Code.seq (inputPrefix (r := 4) 1 2 (fun _ : Fin 1 => 0)) + (.seq (storeZero 0 2) (.op (.const 2 0)))).eval 2 30 (Data.init [3])).map + (fun z => (z.1.mem 0, z.1.regs 1, z.1.regs 2, z.2)) = some (3, 2, 0, 10) := by + decide + +-- The charged prefix really reads memory and installs the frontier before its body. +example : ((inputPrefix (r := 4) 1 2 (fun _ : Fin 1 => 0)).eval 2 20 (Data.init [3])).map + (fun z => (z.1.regs 0, z.1.regs 1, z.2)) = some (3, 2, 7) := by + decide + +-- With no arguments the real empty-case copy still costs one instruction. +example : ((inputPrefix (r := 2) 0 1 (Fin.elim0 : Fin 0 → Fin 2)).eval 1 20 + (Data.init [])).map (fun z => (z.1.regs 0, z.2)) = some (1, 5) := by + decide + +-- A fitting input word alone is insufficient: the next free address must also fit. +example : (inputPrefix (r := 4) 1 2 (fun _ : Fin 1 => 0)).eval 1 20 (Data.init [1]) = none := by + decide + +-- The frontier cannot fit at width zero, even for empty input. +example : (inputPrefix (r := 2) 0 1 (Fin.elim0 : Fin 0 → Fin 2)).eval 0 20 + (Data.init []) = none := by + decide + +end ComplexityTests.WordRAMRealizationProgram diff --git a/ROADMAP.md b/ROADMAP.md index 678d8e30d8..134291d41d 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -635,10 +635,11 @@ reusing graph and matroid foundations and the shared data-structure interfaces. all four memory queries, register-word glue, native branches and binds with one fixed continuation emitter for all runtime replies. Its functional representation retains the complete memory and frontier, and its instruction currency adds local work to memory charges. - Remaining: bounded runtime loops, charged input installation and flat programs, operation-level - memory implementation and framed upper-ADT adapters. The full C2/M1b and queue transfer - objectives remain open; this foundation does not turn arbitrary host continuations into - machine-time certificates. + Bounded runtime loops also charge local computation and every iteration, including query-free + iterations. Fixed flat programs include the actual input-installation prefix and final halt, + with explicit input layout, fits and safe-domain hypotheses. Remaining: operation-level memory + implementation, framed upper-ADT adapters and the representative queue transfer. The full + C2/M1b objective remains open; arbitrary host continuations do not acquire machine-time bounds. - **Stateful algorithms and data structures:** Word-RAM controllers for larger adaptive and iterative clients, including the two-stack queue and timeline-editing controllers; reusable allocation and deallocation, shrinking, and live and peak space accounting; ownership and diff --git a/UPSTREAM.md b/UPSTREAM.md index 7a8ebc36cb..299a193948 100644 --- a/UPSTREAM.md +++ b/UPSTREAM.md @@ -513,9 +513,12 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he The bounded `WordRAM/Realization` foundation (#2213, under #2205) reuses the memory oracle and the same native `Code`/`ExecWithin` semantics. Its explicit faithful register encodings support all four memory queries, certified word glue, branches and uniform - reply-dependent bind, charging local work as well as memory operations. Query arguments are - already in live registers; whole-input installation, final halt, bounded-loop and local-ADT - adapter endpoints remain separate work. This adds no abstract-catalogue headline. + reply-dependent bind, charging local work as well as memory operations. Bounded native loops + charge iterations even without a query. The initialized flat-program projection installs + live inputs in `2*k+5` instructions and includes the final halt; Unit observation additionally + writes a real zero word. Input layout, bounded words and safe domains remain explicit. + Generic memory and local-ADT adapter endpoints remain separate work. This adds no + abstract-catalogue headline. `DataStructure/OrderedSet` and `DataStructure/OrderedSet/*` provide neutral optional-minimum contracts, a typed finite-set interface including deletion, and adaptive minimum extraction, with no tree or cost dependency. Bounded-key implementations may specialize From a929a76f23194a8e94428973bca2a317f9f23755 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 1 Nov 2026 20:59:29 -0500 Subject: [PATCH 6/9] refactor(WordRAM): centralize realization history and word encodings Address outside review5731255619: move the existing public width/history lemmas into Basic and use them from Bind/Loop; remove the private duplicate. Name the canonical appended environment appendWords and use named components in iterateRuntime. Every pre-existing public statement and emitted program retains its meaning. Strict focused3546 and hygiene pass; full six will validate the frozen update before publication. Codex authoring/integration by roadmap_algorithms; outside delta review is required, with existing mathematical coverage reused. No selected abstract impact. --- .../WordRAM/Realization/Basic.lean | 27 ++++++++++++ .../WordRAM/Realization/Bind.lean | 25 +++-------- .../WordRAM/Realization/Loop.lean | 43 ++++++------------- 3 files changed, 44 insertions(+), 51 deletions(-) diff --git a/Complexity/Computability/WordRAM/Realization/Basic.lean b/Complexity/Computability/WordRAM/Realization/Basic.lean index 07f59ad67b..59be6c2b0d 100644 --- a/Complexity/Computability/WordRAM/Realization/Basic.lean +++ b/Complexity/Computability/WordRAM/Realization/Basic.lean @@ -70,6 +70,33 @@ theorem runClient_width (w : ℕ) (p : Memory.Prog α) (s : Memory.State) : exact congrArg (fun t : α × Memory.State × List Memory.Op => (t.1, t.2.1, o :: t.2.2)) (ih (Memory.step s o).2 (Memory.step s o).1) +/-- The result of the memory interpreter is independent of the admissibility width. -/ +theorem clientResult_width (w : ℕ) (p : Memory.Prog α) (s : Memory.State) : + (Memory.spec w).clientResult s p = (Memory.spec 0).clientResult s p := + congrArg Prod.fst (runClient_width w p s) + +/-- The final memory/frontier state is independent of the admissibility width. -/ +theorem clientState_width (w : ℕ) (p : Memory.Prog α) (s : Memory.State) : + (Memory.spec w).clientState s p = (Memory.spec 0).clientState s p := + congrArg (fun t => t.2.1) (runClient_width w p s) + +/-- Admissible sequential histories split at the actual returned value and memory state. -/ +theorem validHistory_bind (w : ℕ) {α β : Type} (p : Memory.Prog α) + (q : α → Memory.Prog β) (s : Memory.State) : + (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (p.bind q)) ↔ + (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s p) ∧ + (Memory.spec w).ValidHistory ((Memory.spec w).clientState s p) + ((Memory.spec w).clientHistory ((Memory.spec w).clientState s p) + (q ((Memory.spec w).clientResult s p))) := by + simp only [StateTransitionSpec.clientHistory, StateTransitionSpec.runClient_bind] + rw [StateTransitionSpec.validHistory_append, StateTransitionSpec.run_runClient] + +/-- Faithfully append a returned word vector to the original input environment. +This is static register wiring; it performs no native computation or copies. -/ +def appendWords (input : δ ↪ (Fin k → ℕ)) (output : α ↪ (Fin l → ℕ)) : + δ × α ↪ (Fin (k + l) → ℕ) := + (input.prodMap output).trans (Fin.appendEquiv k l).toEmbedding + /-- A semantic return issues no memory operation. Its native glue is charged separately. -/ @[simp] theorem memoryCost_pure (a : α) (s : Memory.State) : memoryCost (pure a) s = 0 := rfl diff --git a/Complexity/Computability/WordRAM/Realization/Bind.lean b/Complexity/Computability/WordRAM/Realization/Bind.lean index 51d75154ea..9858fb81ce 100644 --- a/Complexity/Computability/WordRAM/Realization/Bind.lean +++ b/Complexity/Computability/WordRAM/Realization/Bind.lean @@ -35,21 +35,6 @@ private def bindLeft {m n₂ l n₁ : ℕ} (i : Fin (m + n₂ + 1)) : private def bindRight {m n₂ l n₁ : ℕ} (i : Fin (l + n₁ + 1)) : Fin (m + (n₂ + l + n₁ + 1) + 1) := ⟨m + n₂ + 1 + i.val, by omega⟩ -private theorem validHistory_bind {α β : Type} (w : ℕ) (s : Memory.State) - (p : Memory.Prog α) (q : α → Memory.Prog β) : - (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (p.bind q)) ↔ - (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s p) ∧ - (Memory.spec w).ValidHistory ((Memory.spec w).clientState s p) - ((Memory.spec w).clientHistory ((Memory.spec w).clientState s p) - (q ((Memory.spec w).clientResult s p))) := by - have hh : (Memory.spec w).clientHistory s (p.bind q) = - (Memory.spec w).clientHistory s p ++ - (Memory.spec w).clientHistory ((Memory.spec w).clientState s p) - (q ((Memory.spec w).clientResult s p)) := by - simp only [StateTransitionSpec.clientHistory, StateTransitionSpec.clientState, - StateTransitionSpec.clientResult, StateTransitionSpec.runClient_bind] - rw [hh, StateTransitionSpec.validHistory_append, StateTransitionSpec.run_runClient] - namespace Realizes variable {B : Basis} {δ α β : Type} {k l m : ℕ} @@ -63,7 +48,7 @@ variable {B : Basis} {δ α β : Type} {k l m : ℕ} answer. Its domain and work charge are evaluated at the deterministic intermediate state. All emitted code, register banks and the exchange constant precede runtime answers. -/ theorem bind (hP : Realizes B p input answer safeP workP) - (hQ : Realizes B q ((input.prodMap answer).trans (Fin.appendEquiv k l).toEmbedding) + (hQ : Realizes B q (appendWords input answer) output safeQ workQ) : Realizes B (fun d => (p d).bind (fun a => q (d, a))) input output (fun w d s => safeP w d s ∧ @@ -124,10 +109,10 @@ theorem bind (hP : Realizes B p input answer safeP workP) let a := (Memory.spec 0).clientResult s (p d) let s' := (Memory.spec 0).clientState s (p d) have hresult : (Memory.spec w).clientResult s (p d) = a := - congrArg Prod.fst (runClient_width w (p d) s) + clientResult_width w (p d) s have hstate : (Memory.spec w).clientState s (p d) = s' := - congrArg (fun z => z.2.1) (runClient_width w (p d) s) - obtain ⟨hvP, hvQ⟩ := (validHistory_bind w s (p d) (fun a => q (d, a))).mp hv + clientState_width w (p d) s + obtain ⟨hvP, hvQ⟩ := (validHistory_bind w (p d) (fun a => q (d, a)) s).mp hv obtain ⟨z, hz, hmP, houtP, hframeP⟩ := hrunP w d x hx hin hsafe.1 hvP change memoryState frontier z = (Memory.spec w).clientState s (p d) at hmP rw [hstate] at hmP @@ -135,7 +120,7 @@ theorem bind (hP : Realizes B p input answer safeP workP) answer ((Memory.spec w).clientResult s (p d)) i at houtP rw [hresult] at houtP have hinQ : z.regs ∘ nextSrc = - ((input.prodMap answer).trans (Fin.appendEquiv k l).toEmbedding) (d, a) := by + (appendWords input answer) (d, a) := by funext i refine Fin.addCases (fun j => ?_) (fun j => ?_) i · change z.regs (nextSrc (Fin.castAdd l j)) = diff --git a/Complexity/Computability/WordRAM/Realization/Loop.lean b/Complexity/Computability/WordRAM/Realization/Loop.lean index 9081953bdc..893fbe6260 100644 --- a/Complexity/Computability/WordRAM/Realization/Loop.lean +++ b/Complexity/Computability/WordRAM/Realization/Loop.lean @@ -110,27 +110,6 @@ theorem copyBank_exec (src dst : Fin k → Fin r) (idle : Fin r) rw [hframe j (fun i => hj i.succ)] exact Function.update_of_ne (hj 0).symm _ _ -/-- The result of the memory interpreter is independent of the admissibility width. -/ -theorem clientResult_width (w : ℕ) (p : Memory.Prog σ) (s : Memory.State) : - (Memory.spec w).clientResult s p = (Memory.spec 0).clientResult s p := - congrArg Prod.fst (runClient_width w p s) - -/-- The final memory/frontier state is independent of the admissibility width. -/ -theorem clientState_width (w : ℕ) (p : Memory.Prog σ) (s : Memory.State) : - (Memory.spec w).clientState s p = (Memory.spec 0).clientState s p := - congrArg (fun t => t.2.1) (runClient_width w p s) - -/-- Admissible sequential histories split at the actual returned value and memory state. -/ -theorem validHistory_bind (w : ℕ) {α β : Type} (p : Memory.Prog α) - (q : α → Memory.Prog β) (s : Memory.State) : - (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (p.bind q)) ↔ - (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s p) ∧ - (Memory.spec w).ValidHistory ((Memory.spec w).clientState s p) - ((Memory.spec w).clientHistory ((Memory.spec w).clientState s p) - (q ((Memory.spec w).clientResult s p))) := by - simp only [StateTransitionSpec.clientHistory, StateTransitionSpec.runClient_bind] - rw [StateTransitionSpec.validHistory_append, StateTransitionSpec.run_runClient] - /-- Memory cost and certified local work decompose at each actual iteration. -/ theorem iteration_charge_succ (body : δ × σ → Memory.Prog σ) (work : (δ × σ) → Memory.State → ℕ) (d : δ) (n : ℕ) (a : σ) (s : Memory.State) : @@ -255,13 +234,13 @@ theorem iterateRuntime (input : δ ↪ (Fin k → ℕ)) (output : σ ↪ (Fin l {safe : ℕ → (δ × σ) → Memory.State → Prop} {work : (δ × σ) → Memory.State → ℕ} (h : Realizes .exact body - ((input.prodMap output).trans (Fin.appendEquiv k l).toEmbedding) output safe work) : - Realizes .exact (fun d : (δ × σ) × ℕ => iterate body d.1.1 d.2 d.1.2) - ((((input.prodMap output).trans (Fin.appendEquiv k l).toEmbedding).prodMap + (appendWords input output) output safe work) : + Realizes .exact (fun ((d, a), fuel) => iterate body d fuel a) + (((appendWords input output).prodMap (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding).trans (Fin.appendEquiv (k + l) 1).toEmbedding) output - (fun w d s => iterationSafe body safe w d.1.1 d.2 d.1.2 s) - (fun d s => iterationWork body work d.1.1 d.2 d.1.2 s) := by + (fun w ((d, a), fuel) s => iterationSafe body safe w d fuel a s) + (fun ((d, a), fuel) s => iterationWork body work d fuel a s) := by obtain ⟨n, C, emit, he⟩ := h refine ⟨l + n + 3, C + 2 * l + 8, loopEmit emit, ?_⟩ intro r frontier src tmp hi hd hf hs @@ -338,7 +317,8 @@ theorem iterateRuntime (input : δ ↪ (Fin k → ℕ)) (output : σ ↪ (Fin l let s₀ := memoryState frontier x have henv (i : Fin k) : x.regs (env i) = input d₀ i := by have hh : x.regs (src (Fin.castAdd 1 (Fin.castAdd l i))) = input d₀ i := by - simpa [d₀, Fin.appendEquiv] using congrFun hin (Fin.castAdd 1 (Fin.castAdd l i)) + simpa [d₀, appendWords, Fin.appendEquiv] using + congrFun hin (Fin.castAdd 1 (Fin.castAdd l i)) have hidx : Fin.castAdd 1 (Fin.castAdd l i) = (⟨i.val, by omega⟩ : Fin (k + l + 1)) := by apply Fin.ext rfl @@ -346,7 +326,8 @@ theorem iterateRuntime (input : δ ↪ (Fin k → ℕ)) (output : σ ↪ (Fin l exact hh have hstate (i : Fin l) : x.regs (src ⟨k + i.val, by omega⟩) = output a₀ i := by have hh : x.regs (src (Fin.castAdd 1 (Fin.natAdd k i))) = output a₀ i := by - simpa [a₀, Fin.appendEquiv] using congrFun hin (Fin.castAdd 1 (Fin.natAdd k i)) + simpa [a₀, appendWords, Fin.appendEquiv] using + congrFun hin (Fin.castAdd 1 (Fin.natAdd k i)) have hidx : Fin.castAdd 1 (Fin.natAdd k i) = (⟨k + i.val, by omega⟩ : Fin (k + l + 1)) := by apply Fin.ext @@ -419,11 +400,11 @@ theorem iterateRuntime (input : δ ↪ (Fin k → ℕ)) (output : σ ↪ (Fin l have hvparts := (validHistory_bind w (body (d₀, q.1)) (iterate body d₀ j) q.2).mp hyv have hinbody : y.regs ∘ bs = - ((input.prodMap output).trans (Fin.appendEquiv k l).toEmbedding) (d₀, q.1) := by + (appendWords input output) (d₀, q.1) := by funext i refine Fin.addCases (fun i => ?_) (fun i => ?_) i - · simpa [bs, Fin.appendEquiv] using hye i - · simpa [bs, Fin.appendEquiv] using hys i + · simpa [bs, appendWords, Fin.appendEquiv] using hye i + · simpa [bs, appendWords, Fin.appendEquiv] using hys i obtain ⟨u, hu, hum, huo, huf⟩ := hrun w (d₀, q.1) y hyb hinbody (hym ▸ hysafe.1) (hym ▸ hvparts.1) rw [hym] at hu hum huo From 53b120bd220e8488fa3e2f58fa36274f59583e56 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 1 Nov 2026 23:15:59 -0500 Subject: [PATCH 7/9] feat(WordRAM): export initialized flat programs with a standard layout Choose private canonical frontier/input/scratch banks once and project an existing Realizes certificate through the actual charged Data.init prefix, Code.program and halt. The stateful export retains the actual flat Runs, full source memory/frontier and every encoded result word; the scalar Executes corollary removes caller register-layout proofs. Its fixed code, output placement, halt PC and factor precede every runtime width/input. Keep the same raw-layout, length, fit, safe-domain and admissibility premises and C*(memoryCost+work+1)+1 bound. Empty input still requires frontier one to fit; no initialized width-zero case is claimed. The checked initialized-copy client block drops48 to20 lines with its statement unchanged. An actual write/read client checks full post-memory and maximum payload15; the empty-input case retains positive frontier fit. The original Program.lean and all its public interfaces remain exact SHAeeb7346b2d483bede91259eb6f03f50b7b494a735c264a2293e993bf0d800db2. Existing Program/native-prefix source credit remains unchanged. Worker codex-c5-canonical-program-learning-20261102 under root/Algorithms #2279, #2205/#2213, fixed published2230/a929a76f. This is a bounded C5 usability milestone, not a new compiler/language/model or broad completion. Static Fin l observation retains the existing scalar-output scope; zero-output Unit exports remain separate. No selected abstract impact. All six default scripts/check.sh gates PASS,2threads, exact frozen source; strict focused3546, hygiene/check-simp/whitespace and source/pin guards PASS. Fresh outside-author-fleet correctness/API review is required. No own approval or parent source/ref changes. AI assistance: OpenAI Codex. --- Complexity.lean | 1 + .../WordRAM/Realization/Program/Standard.lean | 164 ++++++++++++++++++ .../WordRAMRealizationProgram.lean | 38 +--- .../WordRAMRealizationStandardProgram.lean | 101 +++++++++++ 4 files changed, 271 insertions(+), 33 deletions(-) create mode 100644 Complexity/Computability/WordRAM/Realization/Program/Standard.lean create mode 100644 ComplexityTests/WordRAMRealizationStandardProgram.lean diff --git a/Complexity.lean b/Complexity.lean index 25721a3ac3..b110a8715a 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2563,6 +2563,7 @@ public import Complexity.Computability.WordRAM.Realization.Glue public import Complexity.Computability.WordRAM.Realization.Loop public import Complexity.Computability.WordRAM.Realization.Primitive public import Complexity.Computability.WordRAM.Realization.Program +public import Complexity.Computability.WordRAM.Realization.Program.Standard public import Complexity.Computability.WordRAM.RegisterFrame public import Complexity.Computability.WordRAM.Sequence public import Complexity.Computability.WordRAM.Signed.Arithmetic diff --git a/Complexity/Computability/WordRAM/Realization/Program/Standard.lean b/Complexity/Computability/WordRAM/Realization/Program/Standard.lean new file mode 100644 index 0000000000..db14dc1f85 --- /dev/null +++ b/Complexity/Computability/WordRAM/Realization/Program/Standard.lean @@ -0,0 +1,164 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.WordRAM.Realization.Program + +/-! +# Initialized flat programs with a fixed register layout + +Choose the frontier, input bank and fresh scratch bank once, before every runtime width and +argument. Clients supply the same encoded-input, fit, domain and memory-history premises as +`Realizes.exists_init_program`, without proving register-placement conditions themselves. +The real `Data.init` prefix, native body and trailing halt are all charged. Its positive +next-free address must fit even for an empty input; this is not a width-zero initialization. + +## Main results + +* `Realizes.exists_standard_init_program_state`: one flat program with the exact whole-memory, + frontier and all encoded result words at its fixed halting location. +* `Realizes.exists_standard_init_program`: the scalar `Executes` projection of that same run. + +The observed coordinate is static, as in the existing scalar export. Zero-output Unit clients +continue to use the separate charged Unit-observation API. + +## References + +This is original infrastructure over the existing realization certificate, charged input prefix +and native `Code.program` compiler. It introduces no execution model or client language. +-/ + +@[expose] public section + +namespace Cslib.WordRAM.Realization + +open Cslib.DataStructure + +private abbrev registers (k l n : ℕ) : ℕ := 1 + (k + (l + n + 1)) + +private def standardFrontier {k l n : ℕ} : Fin (registers k l n) := + ⟨0, by unfold registers; omega⟩ + +private def standardInput {k l n : ℕ} (i : Fin k) : Fin (registers k l n) := + Fin.natAdd 1 (Fin.castAdd (l + n + 1) i) + +private def standardScratch {k l n : ℕ} (i : Fin (l + n + 1)) : Fin (registers k l n) := + Fin.natAdd 1 (Fin.natAdd k i) + +private theorem standardPlacement (k l n : ℕ) : + Function.Injective (standardInput (k := k) (l := l) (n := n)) ∧ + Function.Injective (standardScratch (k := k) (l := l) (n := n)) ∧ + (∀ i j, standardInput (l := l) (n := n) i ≠ standardScratch (k := k) j) ∧ + (∀ j, standardScratch (k := k) (l := l) (n := n) j ≠ standardFrontier) ∧ + (∀ i, standardInput (k := k) (l := l) (n := n) i ≠ standardFrontier) := by + refine ⟨?_, ?_, ?_, ?_, ?_⟩ + · intro i j h + apply Fin.ext + have := congrArg Fin.val h + simpa only [standardInput, Fin.val_natAdd, Fin.val_castAdd, + Nat.add_left_cancel_iff] using this + · intro i j h + apply Fin.ext + have := congrArg Fin.val h + simp only [standardScratch, Fin.val_natAdd] at this + omega + · intro i j h + have := congrArg Fin.val h + simp only [standardInput, standardScratch, Fin.val_natAdd, Fin.val_castAdd] at this + have := i.isLt + omega + · intro i h + have := congrArg Fin.val h + simp only [standardScratch, standardFrontier, Fin.val_natAdd] at this + omega + · intro i h + have := congrArg Fin.val h + simp only [standardInput, standardFrontier, Fin.val_natAdd, Fin.val_castAdd] at this + omega + +namespace Realizes + +variable {k l : ℕ} {δ α : Type} {p : δ → Memory.Prog α} + {input : δ ↪ (Fin k → ℕ)} {output : α ↪ (Fin l → ℕ)} + {safe : ℕ → δ → Memory.State → Prop} {work : δ → Memory.State → ℕ} + +/-- One statically laid-out flat program includes charged input installation and its halt. +The witnessed native state is the actual final state of the flat run, retaining the entire +source memory and frontier and every result coordinate. All witnesses precede runtime data. -/ +theorem exists_standard_init_program_state (h : Realizes .exact p input output safe work) + (raw : δ → List ℕ) (hlayout : ∀ d (i : Fin k), (raw d).getD i.val 0 = input d i) + (i : Fin l) : + ∃ r C pc : ℕ, ∃ prog : Program .exact r, + ∃ frontier : Fin r, ∃ out : Fin l → Fin r, + ∀ w d, k ≤ (raw d).length → Fits w ((raw d).length + 1) → InputFits w (raw d) → + safe w d (inputState (raw d)) → + (Memory.spec w).ValidHistory (inputState (raw d)) + ((Memory.spec w).clientHistory (inputState (raw d)) (p d)) → + ∃ y n, Runs w prog (State.init (raw d)) ⟨pc, y⟩ n ∧ + step w prog ⟨pc, y⟩ = + .halt (output ((Memory.spec w).clientResult (inputState (raw d)) (p d)) i) ∧ + memoryState frontier y = (Memory.spec w).clientState (inputState (raw d)) (p d) ∧ + (∀ j, y.regs (out j) = + output ((Memory.spec w).clientResult (inputState (raw d)) (p d)) j) ∧ + n + 1 ≤ C * (memoryCost (p d) (inputState (raw d)) + + work d (inputState (raw d)) + 1) + 1 := by + obtain ⟨n, C, emit, he⟩ := h + let r := registers k l n + let frontier : Fin r := standardFrontier + let src : Fin k → Fin r := standardInput + let tmp : Fin (l + n + 1) → Fin r := standardScratch + obtain ⟨hsrc, htmp, hd, hf, hs⟩ := standardPlacement k l n + let code := Code.seq (inputPrefix frontier (tmp (Fin.last (l + n))) src) + (emit frontier src tmp) + let prog := code.program (tmp (Fin.castAdd (n + 1) i)) + refine ⟨r, C + (2 * k + 5), code.size, prog, frontier, + (fun j => tmp (Fin.castAdd (n + 1) j)), ?_⟩ + intro w d hk hw hin hsafe hv + obtain ⟨x, ex, hx, hm, hwords, _⟩ := inputPrefix_exec frontier (tmp (Fin.last (l + n))) + src (raw d) hsrc (hf _) (fun j => hd j _) hs hk hw hin + have harg : x.regs ∘ src = input d := by + funext j + exact (hwords j).trans (hlayout d j) + obtain ⟨y, ey, hmem, hout, _⟩ := (he frontier src tmp htmp hd hf hs).2 w d x hx harg + (hm.symm ▸ hsafe) (hm.symm ▸ hv) + rw [hm] at ey hmem hout + obtain ⟨steps, hsteps, erun⟩ := ex.seq ey + have hr := erun.runs (pc := 0) (p := prog) (Program.Contains.self _).append_left + refine ⟨y, steps, ?_, ?_, hmem, hout, ?_⟩ + · simpa only [Nat.zero_add, State.init, code] using hr + · rw [← hout i] + exact step_halt (by simp [prog, Code.program]) + · have hpos : 1 ≤ memoryCost (p d) (inputState (raw d)) + + work d (inputState (raw d)) + 1 := by omega + have hover := Nat.mul_le_mul_left (2 * k + 5) hpos + simp only [Nat.mul_one] at hover + rw [Nat.add_mul] + omega + +/-- The canonical initialized export requires no caller-written register layout. Its bound +includes the actual prefix, body and final halt, with code fixed before every width and input. -/ +theorem exists_standard_init_program (h : Realizes .exact p input output safe work) + (raw : δ → List ℕ) (hlayout : ∀ d (i : Fin k), (raw d).getD i.val 0 = input d i) + (i : Fin l) : + ∃ r C : ℕ, ∃ prog : Program .exact r, + ∀ w d, k ≤ (raw d).length → Fits w ((raw d).length + 1) → InputFits w (raw d) → + safe w d (inputState (raw d)) → + (Memory.spec w).ValidHistory (inputState (raw d)) + ((Memory.spec w).clientHistory (inputState (raw d)) (p d)) → + ∃ t, Executes w prog (State.init (raw d)) + (output ((Memory.spec w).clientResult (inputState (raw d)) (p d)) i) t ∧ + t ≤ C * (memoryCost (p d) (inputState (raw d)) + + work d (inputState (raw d)) + 1) + 1 := by + obtain ⟨r, C, pc, prog, _, _, he⟩ := h.exists_standard_init_program_state raw hlayout i + refine ⟨r, C, prog, ?_⟩ + intro w d hk hw hin hsafe hv + obtain ⟨y, n, hr, hh, _, _, hn⟩ := he w d hk hw hin hsafe hv + exact ⟨n + 1, ⟨⟨pc, y⟩, n, hr, hh, rfl⟩, hn⟩ + +end Realizes +end Cslib.WordRAM.Realization diff --git a/ComplexityTests/WordRAMRealizationProgram.lean b/ComplexityTests/WordRAMRealizationProgram.lean index 808b775985..abc00e6d03 100644 --- a/ComplexityTests/WordRAMRealizationProgram.lean +++ b/ComplexityTests/WordRAMRealizationProgram.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Samuel Schlesinger -/ -import Complexity.Computability.WordRAM.Realization.Program +import Complexity.Computability.WordRAM.Realization.Program.Standard /-! Nonvacuous flat-program projections with uniform code and clock constants, for both already installed arguments and an actually charged native list-input prefix. The former @@ -99,47 +99,19 @@ example : ∃ (r C : ℕ) (p : Program .exact r), example : ∃ (r C : ℕ) (p : Program .exact r), ∀ w d, Fits w 2 → Fits w d → ∃ t, Executes w p (State.init [d]) d t ∧ t ≤ C + 1 := by - obtain ⟨n, C, emit, he⟩ := copy_realizes.exists_init_program (fun d => [d]) (by + obtain ⟨r, C, prog, he⟩ := copy_realizes.exists_standard_init_program (fun d => [d]) (by intro d i have hi : i = 0 := Fin.eq_zero i subst i - rfl) - let m := 1 + n + 1 - let r := m + 2 - let frontier : Fin r := ⟨1, by dsimp [r, m]; omega⟩ - let src : Fin 1 → Fin r := fun _ => ⟨0, by dsimp [r, m]; omega⟩ - let tmp : Fin (1 + n + 1) → Fin r := fun j => ⟨j.val + 2, by dsimp [r, m]; omega⟩ - have hi : Function.Injective tmp := by - intro a b h - apply Fin.ext - have := congrArg Fin.val h - dsimp [tmp] at this - omega - have hd : ∀ i j, src i ≠ tmp j := by - intro i j h - have := congrArg Fin.val h - change 0 = j.val + 2 at this - omega - have hf : ∀ j, tmp j ≠ frontier := by - intro j h - have := congrArg Fin.val h - change j.val + 2 = 1 at this - omega - have hs : ∀ i, src i ≠ frontier := by - intro i h - have := congrArg Fin.val h - change 0 = 1 at this - omega - refine ⟨r, C, (Code.seq (inputPrefix frontier (tmp (Fin.last (1 + n))) src) - (emit frontier src tmp)).program (tmp (Fin.castAdd (n + 1) (0 : Fin 1))), ?_⟩ + rfl) 0 + refine ⟨r, C, prog, ?_⟩ intro w d h2 hfit have hin : InputFits w [d] := by refine ⟨h2.of_le (by simp), ?_⟩ intro v hv simp only [List.mem_singleton] at hv exact hv.symm ▸ hfit - obtain ⟨t, ht, htime⟩ := he frontier src tmp (fun _ _ _ => Subsingleton.elim _ _) hi - hd hf hs 0 w d (by simp) h2 hin trivial (by trivial) + obtain ⟨t, ht, htime⟩ := he w d (by simp) h2 hin trivial (by trivial) change t ≤ C * (0 + 0 + 1) + 1 at htime exact ⟨t, ht, by simpa using htime⟩ diff --git a/ComplexityTests/WordRAMRealizationStandardProgram.lean b/ComplexityTests/WordRAMRealizationStandardProgram.lean new file mode 100644 index 0000000000..6517ac04c7 --- /dev/null +++ b/ComplexityTests/WordRAMRealizationStandardProgram.lean @@ -0,0 +1,101 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: local-only (canonical initialized flat-program clients) + +public import Complexity.Computability.WordRAM.Realization.Bind +public import Complexity.Computability.WordRAM.Realization.Glue +public import Complexity.Computability.WordRAM.Realization.Primitive +public import Complexity.Computability.WordRAM.Realization.Program.Standard + +/-! +# Canonical flat programs for an actual memory client + +One fixed program writes a runtime word to an input-memory cell and reads it back. The complete +native post-memory, frontier and encoded result are checked without any register-bank proof in +the client. The empty-input case keeps the actual positive next-free-address premise. +-/ + +public section + +namespace Cslib.WordRAM.Realization.Tests.StandardProgram + +open Cslib.DataStructure + +private abbrev word : ℕ ↪ (Fin 1 → ℕ) := (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding +private abbrev unitWords : Unit ↪ (Fin 0 → ℕ) := (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding +private abbrev arguments : ℕ × ℕ ↪ (Fin 2 → ℕ) := appendWords word word + +private def writeRead (d : ℕ × ℕ) : Memory.Prog ℕ := do + Memory.write d.1 d.2 + Memory.read d.1 + +private theorem writeRead_realizes : + Realizes .exact writeRead arguments word (fun _ _ _ => True) (fun _ _ => 1) := by + have h := (Realizes.write (B := .exact) arguments 0 1).bind + (Realizes.read (appendWords arguments unitWords) 0) + exact h.consequence (fun _ _ _ _ _ _ => ⟨trivial, trivial⟩) (fun _ _ => le_rfl) + +/-- A uniform flat program preserves the actual final data of a write followed by a read. +There are no caller-written register indices, disjointness conditions or intermediate states. -/ +theorem writeRead_native : ∃ r C pc : ℕ, ∃ prog : Program .exact r, + ∃ frontier result : Fin r, ∀ w v, Fits w 3 → Fits w v → + ∃ y n, Runs w prog (State.init [1, v]) ⟨pc, y⟩ n ∧ + step w prog ⟨pc, y⟩ = .halt v ∧ + y.mem 1 = v ∧ y.mem 2 = v ∧ y.mem 100 = 0 ∧ + y.regs frontier = 3 ∧ y.regs result = v ∧ n + 1 ≤ C * 4 + 1 := by + obtain ⟨r, C, pc, prog, frontier, out, he⟩ := + writeRead_realizes.exists_standard_init_program_state (fun d => [d.1, d.2]) + (by intro d i; fin_cases i <;> rfl) 0 + refine ⟨r, C, pc, prog, frontier, out 0, ?_⟩ + intro w v h3 hv + have hin : InputFits w [1, v] := by + refine ⟨h3.of_le (by change 2 ≤ 3; decide), ?_⟩ + intro a ha + simp only [List.mem_cons, List.not_mem_nil, or_false] at ha + rcases ha with rfl | rfl + · exact h3.of_le (by decide) + · exact hv + have hvalid : (Memory.spec w).ValidHistory (inputState [1, v]) + ((Memory.spec w).clientHistory (inputState [1, v]) (writeRead (1, v))) := by + change (1 < 3 ∧ Fits w v) ∧ 1 < 3 ∧ True + exact ⟨⟨by decide, hv⟩, by decide, trivial⟩ + obtain ⟨y, n, hr, hh, hm, hout, hn⟩ := he w (1, v) + (by change 2 ≤ 2; exact le_rfl) h3 hin trivial hvalid + exact ⟨y, n, hr, hh, congrArg (fun s : Memory.State => s.mem 1) hm, + congrArg (fun s : Memory.State => s.mem 2) hm, + congrArg (fun s : Memory.State => s.mem 100) hm, + congrArg Memory.State.frontier hm, hout 0, hn⟩ + +-- A concrete maximum-width payload inhabits the uniform memory-client endpoint. +example : ∃ r : ℕ, ∃ prog : Program .exact r, ∃ y : Data r, ∃ pc n : ℕ, + Runs 4 prog (State.init [1, 15]) ⟨pc, y⟩ n ∧ + step 4 prog ⟨pc, y⟩ = .halt 15 ∧ y.mem 1 = 15 ∧ y.mem 100 = 0 := by + obtain ⟨r, _, pc, prog, _, _, he⟩ := writeRead_native + obtain ⟨y, n, hr, hh, hm, _, ht, _⟩ := he 4 15 (by decide) (by decide) + exact ⟨r, prog, y, pc, n, hr, hh, hm, ht⟩ + +private theorem zero_realizes : + Realizes .exact (fun _ : Unit => (pure 0 : Memory.Prog ℕ)) unitWords word + (fun _ _ _ => True) (fun _ _ => 1) := by + have h := Realizes.glue unitWords (GlueComputes.const (B := .exact) (P := fun _ => True) + (bound := fun _ => 0) 0 (fun _ _ => le_rfl)) + exact h.consequence (fun w _ _ _ _ _ => ⟨trivial, fits_zero w⟩) (fun _ _ => le_rfl) + +/-- Empty input still installs frontier one, with its neutral copy and halt charged. -/ +theorem emptyInput_native : ∃ r C : ℕ, ∃ prog : Program .exact r, + ∀ w, Fits w 1 → ∃ t, Executes w prog (State.init []) 0 t ∧ t ≤ C * 2 + 1 := by + obtain ⟨r, C, prog, he⟩ := zero_realizes.exists_standard_init_program (fun _ => []) + (fun _ i => Fin.elim0 i) 0 + refine ⟨r, C, prog, ?_⟩ + intro w h1 + exact he w () (by decide) h1 ⟨fits_zero w, by simp⟩ trivial (by trivial) + +-- No initialized width-zero instance is claimed, even on empty input. +example : ¬Fits 0 (([] : List ℕ).length + 1) := by decide + +end Cslib.WordRAM.Realization.Tests.StandardProgram From 1e77082f2fab7cc80a00a0e7a2b40690c9d66811 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Mon, 2 Nov 2026 01:27:35 -0500 Subject: [PATCH 8/9] feat(WordRAM): export fixed programs over independent raw memory Generalize the existing canonical initialized whole-state export so raw input words vary after the program, register layout and exchange factor are chosen. The pointwise input-prefix equation relates them to the faithfully encoded argument. Preserve both existing theorem statements as wrappers. The Dijkstra consumer checks one program over every adjacency-list encode with Unit register arguments, plus two different graph memories and a maximum fitting edge weight. Original Program.lean, dependency pins and abstract catalogue are unchanged. All six default scripts/check.sh gates pass at exact tree36ae8037ff716ea9e1c58187285caf3848e0127e (2 threads); focused3572 and hygiene pass. AI assistance: OpenAI Codex, session codex-dijkstra-native-learning-20261102. Refs #2281, #2288. --- .../WordRAM/Realization/Program/Standard.lean | 70 +++++++++++++------ .../WordRAMRealizationStandardProgram.lean | 53 ++++++++++++++ 2 files changed, 102 insertions(+), 21 deletions(-) diff --git a/Complexity/Computability/WordRAM/Realization/Program/Standard.lean b/Complexity/Computability/WordRAM/Realization/Program/Standard.lean index db14dc1f85..7053543fb4 100644 --- a/Complexity/Computability/WordRAM/Realization/Program/Standard.lean +++ b/Complexity/Computability/WordRAM/Realization/Program/Standard.lean @@ -20,8 +20,10 @@ next-free address must fit even for an empty input; this is not a width-zero ini ## Main results -* `Realizes.exists_standard_init_program_state`: one flat program with the exact whole-memory, - frontier and all encoded result words at its fixed halting location. +* `Realizes.exists_standard_init_program_state_from_words`: one flat program for independent + raw memory and register arguments, related by their input prefix. +* `Realizes.exists_standard_init_program_state`: the argument-indexed specialization, retaining + the exact whole-memory, frontier and all encoded result words at its fixed halting location. * `Realizes.exists_standard_init_program`: the scalar `Executes` projection of that same run. The observed coordinate is static, as in the existing scalar export. Zero-output Unit clients @@ -89,24 +91,26 @@ variable {k l : ℕ} {δ α : Type} {p : δ → Memory.Prog α} /-- One statically laid-out flat program includes charged input installation and its halt. The witnessed native state is the actual final state of the flat run, retaining the entire -source memory and frontier and every result coordinate. All witnesses precede runtime data. -/ -theorem exists_standard_init_program_state (h : Realizes .exact p input output safe work) - (raw : δ → List ℕ) (hlayout : ∀ d (i : Fin k), (raw d).getD i.val 0 = input d i) - (i : Fin l) : +source memory and frontier and every result coordinate. The raw input words vary independently +of the register-encoded argument: only their input prefix must agree. All witnesses precede +both kinds of runtime data. -/ +theorem exists_standard_init_program_state_from_words + (h : Realizes .exact p input output safe work) (i : Fin l) : ∃ r C pc : ℕ, ∃ prog : Program .exact r, ∃ frontier : Fin r, ∃ out : Fin l → Fin r, - ∀ w d, k ≤ (raw d).length → Fits w ((raw d).length + 1) → InputFits w (raw d) → - safe w d (inputState (raw d)) → - (Memory.spec w).ValidHistory (inputState (raw d)) - ((Memory.spec w).clientHistory (inputState (raw d)) (p d)) → - ∃ y n, Runs w prog (State.init (raw d)) ⟨pc, y⟩ n ∧ + ∀ w d words, (∀ j : Fin k, words.getD j.val 0 = input d j) → + k ≤ words.length → Fits w (words.length + 1) → InputFits w words → + safe w d (inputState words) → + (Memory.spec w).ValidHistory (inputState words) + ((Memory.spec w).clientHistory (inputState words) (p d)) → + ∃ y n, Runs w prog (State.init words) ⟨pc, y⟩ n ∧ step w prog ⟨pc, y⟩ = - .halt (output ((Memory.spec w).clientResult (inputState (raw d)) (p d)) i) ∧ - memoryState frontier y = (Memory.spec w).clientState (inputState (raw d)) (p d) ∧ + .halt (output ((Memory.spec w).clientResult (inputState words) (p d)) i) ∧ + memoryState frontier y = (Memory.spec w).clientState (inputState words) (p d) ∧ (∀ j, y.regs (out j) = - output ((Memory.spec w).clientResult (inputState (raw d)) (p d)) j) ∧ - n + 1 ≤ C * (memoryCost (p d) (inputState (raw d)) + - work d (inputState (raw d)) + 1) + 1 := by + output ((Memory.spec w).clientResult (inputState words) (p d)) j) ∧ + n + 1 ≤ C * (memoryCost (p d) (inputState words) + + work d (inputState words) + 1) + 1 := by obtain ⟨n, C, emit, he⟩ := h let r := registers k l n let frontier : Fin r := standardFrontier @@ -118,12 +122,12 @@ theorem exists_standard_init_program_state (h : Realizes .exact p input output s let prog := code.program (tmp (Fin.castAdd (n + 1) i)) refine ⟨r, C + (2 * k + 5), code.size, prog, frontier, (fun j => tmp (Fin.castAdd (n + 1) j)), ?_⟩ - intro w d hk hw hin hsafe hv + intro w d words hlayout hk hw hin hsafe hv obtain ⟨x, ex, hx, hm, hwords, _⟩ := inputPrefix_exec frontier (tmp (Fin.last (l + n))) - src (raw d) hsrc (hf _) (fun j => hd j _) hs hk hw hin + src words hsrc (hf _) (fun j => hd j _) hs hk hw hin have harg : x.regs ∘ src = input d := by funext j - exact (hwords j).trans (hlayout d j) + exact (hwords j).trans (hlayout j) obtain ⟨y, ey, hmem, hout, _⟩ := (he frontier src tmp htmp hd hf hs).2 w d x hx harg (hm.symm ▸ hsafe) (hm.symm ▸ hv) rw [hm] at ey hmem hout @@ -133,13 +137,37 @@ theorem exists_standard_init_program_state (h : Realizes .exact p input output s · simpa only [Nat.zero_add, State.init, code] using hr · rw [← hout i] exact step_halt (by simp [prog, Code.program]) - · have hpos : 1 ≤ memoryCost (p d) (inputState (raw d)) + - work d (inputState (raw d)) + 1 := by omega + · have hpos : 1 ≤ memoryCost (p d) (inputState words) + + work d (inputState words) + 1 := by omega have hover := Nat.mul_le_mul_left (2 * k + 5) hpos simp only [Nat.mul_one] at hover rw [Nat.add_mul] omega +/-- One statically laid-out flat program includes charged input installation and its halt. +The witnessed native state is the actual final state of the flat run, retaining the entire +source memory and frontier and every result coordinate. All witnesses precede runtime data. -/ +theorem exists_standard_init_program_state (h : Realizes .exact p input output safe work) + (raw : δ → List ℕ) (hlayout : ∀ d (i : Fin k), (raw d).getD i.val 0 = input d i) + (i : Fin l) : + ∃ r C pc : ℕ, ∃ prog : Program .exact r, + ∃ frontier : Fin r, ∃ out : Fin l → Fin r, + ∀ w d, k ≤ (raw d).length → Fits w ((raw d).length + 1) → InputFits w (raw d) → + safe w d (inputState (raw d)) → + (Memory.spec w).ValidHistory (inputState (raw d)) + ((Memory.spec w).clientHistory (inputState (raw d)) (p d)) → + ∃ y n, Runs w prog (State.init (raw d)) ⟨pc, y⟩ n ∧ + step w prog ⟨pc, y⟩ = + .halt (output ((Memory.spec w).clientResult (inputState (raw d)) (p d)) i) ∧ + memoryState frontier y = (Memory.spec w).clientState (inputState (raw d)) (p d) ∧ + (∀ j, y.regs (out j) = + output ((Memory.spec w).clientResult (inputState (raw d)) (p d)) j) ∧ + n + 1 ≤ C * (memoryCost (p d) (inputState (raw d)) + + work d (inputState (raw d)) + 1) + 1 := by + obtain ⟨r, C, pc, prog, frontier, out, he⟩ := + h.exists_standard_init_program_state_from_words i + exact ⟨r, C, pc, prog, frontier, out, fun w d => he w d (raw d) (hlayout d)⟩ + /-- The canonical initialized export requires no caller-written register layout. Its bound includes the actual prefix, body and final halt, with code fixed before every width and input. -/ theorem exists_standard_init_program (h : Realizes .exact p input output safe work) diff --git a/ComplexityTests/WordRAMRealizationStandardProgram.lean b/ComplexityTests/WordRAMRealizationStandardProgram.lean index 6517ac04c7..20ed5e4f22 100644 --- a/ComplexityTests/WordRAMRealizationStandardProgram.lean +++ b/ComplexityTests/WordRAMRealizationStandardProgram.lean @@ -7,6 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: local-only (canonical initialized flat-program clients) +public import Complexity.Algorithms.WordRAM.Dijkstra.ListEncode public import Complexity.Computability.WordRAM.Realization.Bind public import Complexity.Computability.WordRAM.Realization.Glue public import Complexity.Computability.WordRAM.Realization.Primitive @@ -95,6 +96,58 @@ theorem emptyInput_native : ∃ r C : ℕ, ∃ prog : Program .exact r, intro w h1 exact he w () (by decide) h1 ⟨fits_zero w, by simp⟩ trivial (by trivial) +private theorem readHeader_realizes : + Realizes .exact (fun _ : Unit => Memory.read 1) unitWords word + (fun w _ _ => Fits w 1) (fun _ _ => 2) := by + have h := (Realizes.glue unitWords (GlueComputes.const (B := .exact) + (P := fun _ => True) (bound := fun _ => 1) 1 (fun _ _ => le_rfl))).bind + (Realizes.read (appendWords unitWords word) 0) + exact h.consequence (fun _ _ _ _ _ hfit => ⟨⟨trivial, hfit⟩, trivial⟩) + (fun _ _ => le_rfl) + +/-- The graph is runtime memory, while the register argument is only Unit. One fixed program +reads its first header word for every adjacency-list instance, preserving all input memory. -/ +theorem graphHeader_native : ∃ r C pc : ℕ, ∃ prog : Program .exact r, + ∃ frontier result : Fin r, + ∀ w (G : Cslib.Algorithms.WordRAM.Dijkstra.ListInstance), + Fits w (G.encode.length + 1) → InputFits w G.encode → + ∃ y n, Runs w prog (State.init G.encode) ⟨pc, y⟩ n ∧ + step w prog ⟨pc, y⟩ = .halt G.n ∧ + y.mem = (Data.init G.encode : Data 0).mem ∧ + y.regs frontier = G.encode.length + 1 ∧ y.regs result = G.n ∧ + n + 1 ≤ C * 4 + 1 := by + obtain ⟨r, C, pc, prog, frontier, out, he⟩ := + readHeader_realizes.exists_standard_init_program_state_from_words 0 + refine ⟨r, C, pc, prog, frontier, out 0, ?_⟩ + intro w G hw hin + have hvalid : (Memory.spec w).ValidHistory (inputState G.encode) + ((Memory.spec w).clientHistory (inputState G.encode) (Memory.read 1)) := by + change 1 < G.encode.length + 1 ∧ True + rw [G.encode_length] + exact ⟨by omega, trivial⟩ + obtain ⟨y, n, hr, hh, hm, hout, hn⟩ := he w () G.encode + (fun j => Fin.elim0 j) (Nat.zero_le _) hw hin (hw.of_le (by omega)) hvalid + exact ⟨y, n, hr, hh, congrArg Memory.State.mem hm, + congrArg Memory.State.frontier hm, hout 0, hn⟩ + +private def isolatedVertex : Cslib.Algorithms.WordRAM.Dijkstra.ListInstance := + ⟨1, fun _ => [], 0⟩ + +private def maximumEdge : Cslib.Algorithms.WordRAM.Dijkstra.ListInstance := + ⟨2, fun u => if u.val = 0 then [(1, 15)] else [], 0⟩ + +-- Two different graph memories share one program; the maximum fitting edge weight survives. +example : ∃ r pc : ℕ, ∃ prog : Program .exact r, ∃ y₁ y₂ : Data r, ∃ n₁ n₂ : ℕ, + Runs 4 prog (State.init isolatedVertex.encode) ⟨pc, y₁⟩ n₁ ∧ + Runs 4 prog (State.init maximumEdge.encode) ⟨pc, y₂⟩ n₂ ∧ + step 4 prog ⟨pc, y₁⟩ = .halt 1 ∧ step 4 prog ⟨pc, y₂⟩ = .halt 2 ∧ + y₂.mem 7 = 15 := by + obtain ⟨r, _, pc, prog, _, _, he⟩ := graphHeader_native + obtain ⟨y₁, n₁, hr₁, hh₁, _⟩ := he 4 isolatedVertex (by decide) (by decide) + obtain ⟨y₂, n₂, hr₂, hh₂, hm₂, _⟩ := he 4 maximumEdge (by decide) (by decide) + exact ⟨r, pc, prog, y₁, y₂, n₁, n₂, hr₁, hr₂, hh₁, hh₂, + congrFun hm₂ 7⟩ + -- No initialized width-zero instance is claimed, even on empty input. example : ¬Fits 0 (([] : List ℕ).length + 1) := by decide From 4b3e205c887c1a48b17940c28b3ebff4c976d938 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Mon, 2 Nov 2026 13:17:59 -0500 Subject: [PATCH 9/9] doc(WordRAM): explain canonical initialized program exports Address PR2281 outside review6583587280 beside the Realizes discussion. Give the exact import, raw-words/state/scalar choices, preserved prefix, fit/domain/history premises and complete checked clients. Distinguish uncharged Data.init raw placement from the charged 2*k+5 register/frontier prefix, body and halt. The graph client only reads its header and preserves memory; no Dijkstra runtime endpoint is claimed. Manual impact: update the Algorithm/Operator's Manual API reference. No Agent Operator's Manual edit: roles, delegation, human direction and handoff procedures are unchanged. No selected abstract/catalogue impact. Validation: documented Python manual checker and all37 controls pass; whitespace passes. Inspect the affected GitHub-Markdown/Chrome page render and exact approved source links. Full XeLaTeX book generation unavailable because Pandoc, XeLaTeX and Graphviz are not installed; no book-PDF claim. No Lean source, test, dependency pin or proof changes in this child. Independent source/API review6583587280 remains the source coverage; independent documentation/current-context review still follows. AI assistance: OpenAI Codex, codex-2281-manual-bpl-20261102, authored this bounded documentation repair under LogsQ. Samuel Schlesinger/Learning source credit and all approved payloads are unchanged. --- .../memory-specifications.md | 49 +++++++++++++++++++ 1 file changed, 49 insertions(+) diff --git a/manual/algorithms-and-memory/memory-specifications.md b/manual/algorithms-and-memory/memory-specifications.md index 1b01af2993..c2f11311a5 100644 --- a/manual/algorithms-and-memory/memory-specifications.md +++ b/manual/algorithms-and-memory/memory-specifications.md @@ -28,6 +28,55 @@ The native allocation library [Complexity/Computability/WordRAM/Allocation.lean] [Realizes](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/WordRAM/Realization/Basic.lean#L95) is a graded realization interface. It chooses scratch registers, a constant and a uniform code emitter **before** arguments, width and memory. It requires faithful register encodings, a whole-memory/frontier abstraction, register framing and explicit safety/work bounds. Its instruction allowance is proportional to `memoryCost + work + 1`. The `work` term is necessary because pure/control code can take time without making memory queries. `Realizes.exists_refines` connects it to the native controller layer. Primitive, bind and branch modules provide a compositional foundation, not a compiler for every arbitrary Lean function. +### Export a canonical initialized flat program + +Import `Complexity.Computability.WordRAM.Realization.Program.Standard` when you have a +`Realizes .exact` certificate and want one flat program with a fixed register layout. +The [canonical exports](../../Complexity/Computability/WordRAM/Realization/Program/Standard.lean) +choose the program, frontier register, result bank, halt location and constant factor before +runtime word width and input. You supply the encoding and admissibility proofs; the exports +supply the register placement and disjointness proofs. + +Choose the conclusion your client needs: + +- `Realizes.exists_standard_init_program_state_from_words` lets the raw memory list vary + independently of the register-encoded argument. Use it when a small argument controls an + operation on a larger input already in memory. The first `k` raw words must agree pointwise + with the `k` encoded argument words. +- `Realizes.exists_standard_init_program_state` specializes that rule to a chosen `raw d` + list for each argument `d`. It retains the actual final native state, complete memory and + frontier, every encoded result word, and the fixed halting location. +- `Realizes.exists_standard_init_program` projects the same run to scalar `Executes` at a + fixed result coordinate `i : Fin l`. Use the state variant when a later proof needs memory + or other result coordinates. Zero-output Unit clients use the separate Unit-observation + exports in [Program](../../Complexity/Computability/WordRAM/Realization/Program.lean). + +For each runtime input, prove `k ≤ words.length`, `Fits w (words.length + 1)`, +`InputFits w words`, the certificate's `safe w d (inputState words)` condition, and +`Memory.spec`'s `ValidHistory` for that client from `inputState words`. The raw-words rule +also requires the prefix equality described above; the other two take that equality for +`raw d` when choosing the program. The resulting instruction bound is +`C * (memoryCost + work + 1) + 1`, including the executed prefix, body and halt. +If an application fails, check the prefix, fit, safe-domain and history obligations before +changing the program or dropping a premise. Even an empty input needs `Fits w 1`; these +exports do not initialize at word width zero. + +`Data.init` places the raw input list in memory by the existing **uncharged calling +convention**. The charged native prefix takes at most `2*k+5` instructions to install the +frontier and the first `k` argument registers while preserving memory. It does not construct +or copy the whole graph or other raw-memory input. Work used to obtain that initial input +requires a separate bound if the surrounding application charges it. + +Open the complete checked +[StandardProgram clients](../../ComplexityTests/WordRAMRealizationStandardProgram.lean), +including their imports, encodings and premises, for a starting point. +`writeRead_native` uses the state export for a write followed by a read, with a concrete +maximum-fitting payload `15`; `emptyInput_native` uses the scalar export and exposes the +positive frontier-fit premise. `graphHeader_native` uses the raw-words export with a Unit +register argument and actual Dijkstra adjacency-list encodings. One program handles two +different graphs, reads their first header word and preserves the entire input memory. +This client is a header-read demonstration, not a Dijkstra execution or shortest-path bound. + ## Footprints, traces, and memory windows [HeapAssertion](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/WordRAM/Heap.lean#L62) records a finite support and a predicate on total memory. Separating conjunction uses disjoint supports; `Modifies` records agreement outside an allowed write set. This is an explicit-footprint frame calculus inspired by separation logic, not a replacement semantics in which inaccessible cells disappear [reynolds02][reynolds02].