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