diff --git a/Complexity.lean b/Complexity.lean
index 5b587273b8..78d237d5fe 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -14,6 +14,7 @@ public import Complexity.Algorithms.ExactTriangle.Weights
 public import Complexity.Algorithms.ExactTriangle.Witnesses
 public import Complexity.Algorithms.Lean.Dijkstra.Client
 public import Complexity.Algorithms.Lean.Dijkstra.Cost
+public import Complexity.Algorithms.Lean.Dijkstra.Memory
 public import Complexity.Algorithms.Lean.Huffman.Basic
 public import Complexity.Algorithms.Lean.Huffman.Kraft
 public import Complexity.Algorithms.Lean.Huffman.Optimality
@@ -2878,6 +2879,7 @@ public import Complexity.Crypto.Protocols.Signature.RandomOracle
 public import Complexity.DataStructure.AVLTree.Basic
 public import Complexity.DataStructure.AVLTree.Erase
 public import Complexity.DataStructure.AVLTree.Impl
+public import Complexity.DataStructure.AdjacencyList.Memory
 public import Complexity.DataStructure.AdjacencyList.Spec
 public import Complexity.DataStructure.CountMin.Basic
 public import Complexity.DataStructure.CountMin.LinearHash
@@ -2885,6 +2887,7 @@ public import Complexity.DataStructure.CountMin.Probability
 public import Complexity.DataStructure.CountMin.Program
 public import Complexity.DataStructure.Dictionary.CuckooHashing
 public import Complexity.DataStructure.Dictionary.DoubleHashing
+public import Complexity.DataStructure.Dictionary.Memory
 public import Complexity.DataStructure.Dictionary.Spec
 public import Complexity.DataStructure.Dictionary.UniformProbing
 public import Complexity.DataStructure.Dictionary.WordRAM.ChainedHash
diff --git a/Complexity/Algorithms/Lean/Dijkstra/Memory.lean b/Complexity/Algorithms/Lean/Dijkstra/Memory.lean
new file mode 100644
index 0000000000..62e06022a5
--- /dev/null
+++ b/Complexity/Algorithms/Lean/Dijkstra/Memory.lean
@@ -0,0 +1,380 @@
+/-
+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.Algorithms.Lean.Dijkstra.Cost
+public import Complexity.DataStructure.AdjacencyList.Memory
+public import Complexity.DataStructure.Dictionary.Memory
+public import Complexity.DataStructure.PriorityQueue.BinaryHeap.Memory
+import Complexity.Algorithms.WordRAM.Dijkstra.ListEncode
+
+/-!
+# Dijkstra's algorithm with a binary heap, over the memory oracle
+
+The client `Cslib.Algorithms.Lean.Dijkstra.dijkstra` runs over three structures in one memory
+(`framed`, a `Memory.Framed.prod`): the indexed binary heap
+`Cslib.DataStructure.PriorityQueue.BinaryHeap.Memory.framed`, a direct-address table for the
+tentative distances, and the adjacency arrays of the graph. `run` is one memory program for every
+graph. It reads the word RAM's input convention (`ListInstance.encode`): it reads `n`, the source
+and the number `m` of edges, allocates the distance table and the heap just past the input, where
+memory is zero, and runs the linked client on the adjacency arrays of the input.
+
+`run_spec` is the memory-level counterpart of `Cslib.Algorithms.WordRAM.Dijkstra.LogLinearSpec`:
+at every word size that holds `8 (n + m + 2) (W + 2)`, every memory operation of `run` is
+admissible, the cell `G.outAddr v` then holds the encoded distance from the source to `v`, and the
+run costs at most `52 (m + 1) (⌊log₂ n⌋ + 1)` memory units. `exists_run_logLinear` exports the
+bound as `O((m + 1) log n)`. Correctness is `dijkstra_correct` transported through the refinement
+(`Refinement.simulates_client`); the cost is the client's operation count
+(`totalCost_dijkstra_le`) at the structures' charges, transported by their amortized
+certificates (`Refinement.Amortized.client`). The proofs here mention no register, instruction
+or address beyond the layout of the input.
+
+Executing memory programs on the word RAM is a separate, generic realization step, which this
+file does not provide.
+
+## Main definitions
+
+* `memMethods`, `opCharge`: the methods of the three structures, and their charges.
+* `inputGraph`: the adjacency arrays of the input convention.
+* `framed`: the three structures as one framed refinement of `Dijkstra.spec`.
+* `run`: read the input, allocate, and run Dijkstra's algorithm.
+
+## Main results
+
+* `dijkstra_eq`: the client does not depend on the key and value bounds of its interfaces.
+* `holds_inputGraph`: the input holds the graph in the adjacency arrays.
+* `inv_input`: after allocation, the structures represent the initial state.
+* `run_spec`: admissibility, distances and memory cost of `run`.
+* `exists_run_logLinear`: the same with an `O((m + 1) log n)` cost function.
+
+## References
+
+* [E. W. Dijkstra, *A note on two problems in connexion with graphs*][Dijkstra1959]
+* [T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, *Introduction to
+  Algorithms*][CLRS2009]
+-/
+
+@[expose] public section
+
+namespace Cslib.Algorithms.Lean.Dijkstra.Memory
+
+open Cslib.WordRAM Cslib.DataStructure Cslib.DataStructure.Memory Cslib.DataStructure.PriorityQueue
+open Cslib.Algorithms.WordRAM.Dijkstra (ListInstance encodeDist)
+
+/-! ## The client does not depend on its bounds -/
+
+/-- The main loop does not depend on the key and value bounds `K` and `V`, which only restrict
+admissibility. -/
+theorem loop_eq (n K V K' V' k : ℕ) : @loop n K V k = @loop n K' V' k := by
+  induction k with
+  | zero => rfl
+  | succ k ih =>
+    simp only [loop, ih]
+    rfl
+
+/-- The client does not depend on the key and value bounds `K` and `V`. -/
+theorem dijkstra_eq {n : ℕ} (K V K' V' : ℕ) (src : Fin n) :
+    @dijkstra n K V src = @dijkstra n K' V' src := by
+  simp only [dijkstra, loop_eq n K V K' V']
+
+/-! ## The structures -/
+
+/-- The methods of the heap `H`, the distance table `T` and the adjacency arrays `A`. -/
+def memMethods (n K V w : ℕ) (H : BinaryHeap.Memory.Layout n) (T : Block)
+    (A : AdjacencyList.Memory.Layout) : Methods (spec n K V) (Memory.spec w) :=
+  Methods.prod (BinaryHeap.Memory.ops H)
+    (Methods.prod (Dictionary.Memory.ops T) (AdjacencyList.Memory.ops A))
+
+/-- The adjacency arrays of the input convention: the `n + 1` offsets at address `3`, and the `m`
+edges from address `n + 4`. -/
+def inputGraph (n m : ℕ) : AdjacencyList.Memory.Layout := ⟨⟨3, n + 1⟩, ⟨n + 4, 2 * m⟩⟩
+
+variable {n K V w : ℕ} {H : BinaryHeap.Memory.Layout n} {T : Block}
+  {A : AdjacencyList.Memory.Layout}
+
+/-- The heap, the distance table and the adjacency arrays of the graph `adj`, as one framed
+refinement of the interfaces of Dijkstra's algorithm. -/
+def framed (hH : H.Valid w K) (hT : Dictionary.Memory.Valid T w n V) (hA : A.Valid n)
+    (adj : AdjacencyList.State n) : Memory.Framed (spec n K V) w :=
+  (BinaryHeap.Memory.framed hH).prod
+    ((Dictionary.Memory.framed (n_max := n) hT).prod (AdjacencyList.Memory.framed adj hA))
+
+/-- The composite's methods are `memMethods`. -/
+theorem framed_methods (hH : H.Valid w K) (hT : Dictionary.Memory.Valid T w n V)
+    (hA : A.Valid n) (adj : AdjacencyList.State n) :
+    (framed hH hT hA adj).methods = memMethods n K V w H T A := rfl
+
+/-- The methods do not depend on the bounds and the word size in their type. -/
+theorem memMethods_eq (n K V w K' V' w' : ℕ) (H : BinaryHeap.Memory.Layout n) (T : Block)
+    (A : AdjacencyList.Memory.Layout) : memMethods n K V w H T A = memMethods n K' V' w' H T A := by
+  funext o
+  rcases o with o | o | o <;> rfl
+
+/-- The charge of the composite: a heap operation costs `opCost n`, a distance-table operation
+one unit and a graph query three units. -/
+abbrev opCharge (n K V : ℕ) : (spec n K V).State → (spec n K V).Op → ℕ :=
+  productCharge (fun _ _ => BinaryHeap.Memory.opCost n) (productCharge (fun _ _ => 1)
+    fun _ _ => 3)
+
+/-- Every operation of the composite costs at most its `charge`, with no potential. -/
+theorem amortized (hH : H.Valid w K) (hT : Dictionary.Memory.Valid T w n V) (hA : A.Valid n)
+    (adj : AdjacencyList.State n) :
+    (framed hH hT hA adj).Amortized Memory.charge (opCharge n K V) fun _ => 0 :=
+  Memory.Framed.amortized_prod (BinaryHeap.Memory.amortized hH)
+    (Memory.Framed.amortized_prod (Dictionary.Memory.amortized hT)
+      (AdjacencyList.Memory.amortized hA) (Memory.Framed.Local.const _ 0)
+      (Memory.Framed.Local.const _ 0))
+    (Memory.Framed.Local.const _ 0)
+    (Memory.Framed.Local.const _ 0)
+
+/-! ## The program -/
+
+/-- **Dijkstra's algorithm over memory** on the word RAM's input convention: read `n`, the source
+and the number `m` of edges, allocate the distance table and the heap past the input, and run the
+client through the three structures. The key bound, value bound and word size in the types of
+`memMethods` and `dijkstra` are `0`: they only restrict admissibility, and the program does not
+depend on them (`dijkstra_eq`). -/
+def run : Prog Unit := do
+  let n ← read 1
+  let src ← read 2
+  let m ← read (n + 3)
+  let T ← allocBlockDirty n
+  let H ← BinaryHeap.Memory.allocLayout n
+  if h : src < n then
+    link (memMethods n 0 0 0 H T (inputGraph n m)) (dijkstra (K := 0) (V := 0) ⟨src, h⟩)
+  else pure ()
+
+/-! ## The input -/
+
+/-- The input convention holds the graph in the adjacency arrays `inputGraph`. -/
+theorem holds_inputGraph (G : ListInstance) :
+    AdjacencyList.Memory.Holds (inputGraph G.n G.m) G.adj (Memory.State.init G.encode).mem := by
+  set m := (Memory.State.init G.encode).mem with hm
+  have hoff : ∀ j ≤ G.n, m (3 + j) = G.offset j := fun j hj => by
+    rw [Nat.add_comm]
+    exact G.init_offset (r := 0) hj
+  refine ⟨fun u => ?_, fun u => ?_, fun u i hi => ?_, fun u i hi => ?_⟩
+  · change m (3 + (u + 1)) = m (3 + u) + _
+    rw [hoff _ u.isLt, hoff _ u.isLt.le, G.offset_succ u.isLt]
+  · change 2 * m (3 + (u + 1)) ≤ 2 * G.m
+    rw [hoff _ u.isLt, ← G.offset_n]
+    exact Nat.mul_le_mul_left 2 (G.offset_mono u.isLt)
+  · change m (G.n + 4 + 2 * (m (3 + u) + i)) = _
+    rw [hoff _ u.isLt.le, show G.n + 4 + 2 * (G.offset u + i) = 2 * (G.offset u + i) + G.n + 4 by
+      omega]
+    exact G.init_target (r := 0) u hi
+  · change m (G.n + 4 + (2 * (m (3 + u) + i) + 1)) = _
+    rw [hoff _ u.isLt.le, show G.n + 4 + (2 * (G.offset u + i) + 1) =
+      2 * (G.offset u + i) + G.n + 5 by omega]
+    exact G.init_weight (r := 0) u hi
+
+/-- **The structures after allocation.** Past the input of `G`, a distance table and then a heap,
+allocated without clearing, together with the adjacency arrays of the input, represent the
+initial state of Dijkstra's algorithm on `G`: an empty queue, an empty distance map and the
+graph. -/
+theorem inv_input (G : ListInstance) {w K V : ℕ}
+    (hH : (BinaryHeap.Memory.allocated G.n ((Memory.State.init G.encode).frontier + G.n)).Valid
+      w K)
+    (hT : Dictionary.Memory.Valid ⟨(Memory.State.init G.encode).frontier, G.n⟩ w G.n V)
+    (hA : (inputGraph G.n G.m).Valid G.n) :
+    (framed hH hT hA G.adj).inv ⟨(Memory.State.init G.encode).mem,
+        (Memory.State.init G.encode).frontier + G.n + 1 +
+          PriorityQueue.WordRAM.BinaryHeap.space G.n⟩ ∧
+      (framed hH hT hA G.adj).abs ⟨(Memory.State.init G.encode).mem,
+        (Memory.State.init G.encode).frontier + G.n + 1 +
+          PriorityQueue.WordRAM.BinaryHeap.space G.n⟩ = init G := by
+  set s₀ := Memory.State.init G.encode with hs₀
+  have hf₀ : s₀.frontier = G.n + 2 * G.m + 4 := by
+    simp only [s₀, Memory.State.init, G.encode_length]
+  have hz : ZeroAbove s₀ := zeroAbove_init _
+  set f := s₀.frontier with hf
+  have hf₁ : (Memory.State.init G.encode).frontier = G.n + 2 * G.m + 4 := hf₀
+  obtain ⟨hHinv, hHabs⟩ := BinaryHeap.Memory.inv_allocated (s := ⟨s₀.mem, f + G.n⟩)
+    (hz.allocDirty G.n)
+  obtain ⟨hTinv, hTabs⟩ := Dictionary.Memory.inv_alloc (U := G.n) hz
+  have hsp : PriorityQueue.WordRAM.BinaryHeap.space G.n = 3 * G.n + 1 := rfl
+  refine ⟨⟨hHinv, ⟨Block.Allocated.mono hTinv (by simp only; omega),
+    ⟨by simp only [inputGraph, Block.Allocated]; omega,
+      by simp only [inputGraph, Block.Allocated]; omega, holds_inputGraph G⟩, ?_⟩, ?_⟩,
+    Prod.ext hHabs (Prod.ext hTabs rfl)⟩
+  · simp only [Dictionary.Memory.framed_footprint, AdjacencyList.Memory.framed_footprint]
+    rw [Finset.disjoint_left]
+    intro a ha hb
+    simp only [Block.mem_footprint, Block.Owns, AdjacencyList.Memory.Layout.footprint,
+      inputGraph, Finset.mem_union] at ha hb
+    omega
+  · simp only [Memory.Framed.prod_footprint, BinaryHeap.Memory.framed_footprint,
+      Dictionary.Memory.framed_footprint, AdjacencyList.Memory.framed_footprint]
+    rw [Finset.disjoint_left]
+    intro a ha hb
+    simp only [Block.mem_footprint, Block.Owns, AdjacencyList.Memory.Layout.footprint,
+      BinaryHeap.Memory.Layout.footprint, inputGraph, Finset.mem_union, hsp] at ha hb
+    omega
+
+/-- A cell whose decoded value is `some d` exactly when the distance `D` is `d` holds the encoded
+distance. -/
+private theorem eq_encodeDist {x : ℕ} {D : ℕ∞}
+    (h : ∀ d : ℕ, Dictionary.Memory.decode x = some d ↔ D = d) : x = encodeDist D := by
+  cases x with
+  | zero =>
+    have hD : D = ⊤ := by
+      by_contra hD
+      obtain ⟨d, rfl⟩ := ENat.ne_top_iff_exists.mp hD
+      simpa using (h d).mpr rfl
+    simp [hD, encodeDist]
+  | succ x =>
+    have hD := (h x).mp rfl
+    simp [hD, encodeDist]
+
+
+/-! ## Correctness and cost -/
+
+/-- The cost of Dijkstra's algorithm over memory, at most: `52 (m + 1) (⌊log₂ n⌋ + 1)`. -/
+def memCost (n m : ℕ) : ℕ := 52 * (m + 1) * (Nat.log 2 n + 1)
+
+/-- The client's operations, at the charges of the three structures, cost at most
+`3 (m + 1) opCost n + 8 m + 4`, which with the six units of reading and allocating is within
+`memCost`. -/
+private theorem budget_le (n m : ℕ) :
+    6 + (3 * (m + 1) * BinaryHeap.Memory.opCost n + 8 * m + 4) ≤ memCost n m := by
+  unfold memCost BinaryHeap.Memory.opCost
+  generalize Nat.log 2 n = L
+  nlinarith
+
+/-- **Dijkstra's algorithm over memory.** On the input words of a graph `G`, at every word size
+`w` that holds `8 (n + m + 2) (W + 2)`, every memory operation of `run` is admissible, it costs at
+most `memCost n m` memory units, and the cell `G.outAddr v` then holds the encoded distance from
+the source to `v`, for every vertex `v`. -/
+theorem run_triple (G : ListInstance) {w : ℕ}
+    (hfit : Fits w (8 * (G.n + G.m + 2) * (G.maxWeight + 2))) :
+    Triple w (Memory.State.init G.encode) run (memCost G.n G.m)
+      fun _ s' => ∀ v : Fin G.n, s'.mem (G.outAddr v) = encodeDist (G.dist G.source v) := by
+  set s₀ := Memory.State.init G.encode with hs₀
+  have hf₀ : s₀.frontier = G.n + 2 * G.m + 4 := by
+    simp only [s₀, Memory.State.init, G.encode_length]
+  have hz : ZeroAbove s₀ := zeroAbove_init _
+  have hn1 : s₀.mem 1 = G.n := rfl
+  have hsrc : s₀.mem 2 = G.source := rfl
+  have hm : s₀.mem (G.n + 3) = G.m := by
+    rw [← G.offset_n]
+    exact G.init_offset (r := 0) le_rfl
+  -- The bounds of the interfaces and the facts that fit a word.
+  set K := G.n * G.maxWeight with hK
+  have hW : 2 ≤ G.maxWeight + 2 := by omega
+  have hbig : 2 * (G.n + G.m + 2) ≤ 8 * (G.n + G.m + 2) * (G.maxWeight + 2) := by nlinarith
+  have hn : Fits w G.n := hfit.of_le (by nlinarith)
+  have hKf : Fits w K := hfit.of_le (by nlinarith)
+  have hVf : Fits w (K + 1) := hfit.of_le (by nlinarith)
+  -- The rate of each kind of operation.
+  let rate : OpKind → ℕ
+    | .insert => BinaryHeap.Memory.opCost G.n
+    | .extractMin => BinaryHeap.Memory.opCost G.n
+    | .decreaseKey => BinaryHeap.Memory.opCost G.n
+    | .inspect => 0
+    | .distance => 1
+    | .graph => 3
+  have hrate : rateBound rate G.n G.m ≤
+      3 * (G.m + 1) * BinaryHeap.Memory.opCost G.n + 8 * G.m + 4 :=
+    (min_le_right _ _).trans (by simp only [rate]; nlinarith)
+  refine Triple.mono (c := rateBound rate G.n G.m + 6) ?_
+    (by have := budget_le G.n G.m; omega) fun _ _ h => h
+  refine Triple.read_bind (by omega) <| Triple.read_bind (by omega) ?_
+  rw [hn1, hsrc]
+  refine Triple.read_bind (by omega) ?_
+  rw [hm]
+  refine Triple.allocBlockDirty_bind (hfit.of_le (by nlinarith)) ?_
+  refine BinaryHeap.Memory.allocLayout_bind
+    (hfit.of_le (by simp only [PriorityQueue.WordRAM.BinaryHeap.space]; nlinarith)) ?_
+  rw [dite_eq_left G.source.isLt]
+  dsimp only
+  -- The three structures, at the bounds `K` and `K + 1`, on the memory after allocation.
+  set f := s₀.frontier with hf
+  have hH : (BinaryHeap.Memory.allocated G.n (f + G.n)).Valid w K :=
+    BinaryHeap.Memory.valid_allocated hn hKf
+  have hT : Dictionary.Memory.Valid ⟨f, G.n⟩ w G.n (K + 1) := ⟨rfl, hVf⟩
+  have hA : (inputGraph G.n G.m).Valid G.n := ⟨rfl⟩
+  set M := framed hH hT hA G.adj with hM
+  obtain ⟨hinv, habs⟩ := inv_input G hH hT hA
+  obtain ⟨hvalid, hdist⟩ := dijkstra_correct (K := K) (V := K + 1) G le_rfl (by omega)
+  rw [← habs] at hvalid hdist
+  obtain ⟨hvE, -, hstate, -⟩ := M.simulates_client (dijkstra G.source) hinv hvalid
+  have hcost := (amortized hH hT hA G.adj).client (dijkstra G.source) hinv hvalid
+  have hcost' := totalCost_dijkstra_le (K := K) (V := K + 1) G le_rfl (by omega)
+    (opCharge G.n K (K + 1)) rate fun s o ho => by
+      rcases o with (_ | _ | _ | _ | _) | (_ | _) | (_ | _) <;>
+        first | exact absurd rfl ho | simp [rate, kind, opCharge, productCharge]
+  rw [← habs] at hcost'
+  have hprog : link (memMethods G.n 0 0 0 (BinaryHeap.Memory.allocated G.n (f + G.n)) ⟨f, G.n⟩
+      (inputGraph G.n G.m)) (dijkstra (K := 0) (V := 0) ⟨G.source, G.source.isLt⟩) =
+      link M.methods (dijkstra (K := K) (V := K + 1) G.source) := by
+    rw [hM, framed_methods, dijkstra_eq K (K + 1) 0 0, memMethods_eq G.n K (K + 1) w 0 0 0]
+    rfl
+  rw [hprog]
+  refine triple_iff.mpr ⟨hvE, ?_, fun v => ?_⟩
+  · exact (Nat.le_add_right _ _).trans (hcost.trans (Nat.add_le_add_right hcost' 0))
+  obtain ⟨dist, hds, hdv⟩ := hdist
+  rw [← hstate] at hds
+  have hcell := congrArg (fun x => x.2.1 v) hds
+  simp only [M, framed, Memory.Framed.prod_abs] at hcell
+  refine eq_encodeDist fun d => ?_
+  rw [show G.outAddr v = f + v by simp only [ListInstance.outAddr]; omega, ← hdv v d, ← hcell]
+  exact Iff.rfl
+
+/-- **Dijkstra's algorithm over memory, unpacked.** On the input words of a graph `G`, at every
+word size that holds `8 (n + m + 2) (W + 2)`, every memory operation of `run` is admissible, the
+cell `G.outAddr v` then holds the encoded distance from the source to `v`, and the run costs at
+most `52 (m + 1) (⌊log₂ n⌋ + 1)` memory units. -/
+theorem run_spec (G : ListInstance) {w : ℕ}
+    (hfit : Fits w (8 * (G.n + G.m + 2) * (G.maxWeight + 2))) :
+    (Memory.spec w).ValidHistory (Memory.State.init G.encode)
+        ((Memory.spec w).clientHistory (Memory.State.init G.encode) run) ∧
+      (∀ v : Fin G.n, ((Memory.spec w).clientState (Memory.State.init G.encode) run).mem
+        (G.outAddr v) = encodeDist (G.dist G.source v)) ∧
+      (Memory.spec w).totalCost Memory.charge (Memory.State.init G.encode)
+        ((Memory.spec w).clientHistory (Memory.State.init G.encode) run) ≤ memCost G.n G.m := by
+  obtain ⟨hv, hc, hd⟩ := triple_iff.mp (run_triple G hfit)
+  exact ⟨hv, hd, hc⟩
+
+/-- `memCost` grows with the graph. -/
+theorem memCost_mono {n m n' m' : ℕ} (hn : n ≤ n') (hm : m ≤ m') : memCost n m ≤ memCost n' m' := by
+  unfold memCost
+  have := Nat.log_mono_right (b := 2) hn
+  gcongr
+
+/-- **The exported form: `O((m + 1) log n)` memory units.** One memory program computes the
+distances from the source of every graph, at every word size that holds `8 (n + m + 2) (W + 2)`,
+admissibly and within `f (n, m)` memory units, for a monotone `f = O((m + 1) log n)` as `n` grows,
+uniformly in `m`. Since `m + 1 ≤ n + m`, this is also `O((n + m) log n)`. -/
+theorem exists_run_logLinear :
+    ∃ f : ℕ × ℕ → ℕ, Monotone f ∧
+      (fun p => (f p : ℝ)) =O[Filter.comap Prod.fst Filter.atTop]
+        (fun ((n, m) : ℕ × ℕ) => ((m + 1) * Nat.log 2 n : ℝ)) ∧
+      ∀ (G : ListInstance) (w : ℕ), Fits w (8 * (G.n + G.m + 2) * (G.maxWeight + 2)) →
+        (Memory.spec w).ValidHistory (Memory.State.init G.encode)
+            ((Memory.spec w).clientHistory (Memory.State.init G.encode) run) ∧
+          (∀ v : Fin G.n, ((Memory.spec w).clientState (Memory.State.init G.encode) run).mem
+            (G.outAddr v) = encodeDist (G.dist G.source v)) ∧
+          (Memory.spec w).totalCost Memory.charge (Memory.State.init G.encode)
+            ((Memory.spec w).clientHistory (Memory.State.init G.encode) run) ≤ f (G.n, G.m) := by
+  refine ⟨fun (n, m) => memCost n m, fun ⟨_, _⟩ ⟨_, _⟩ ⟨hn, hm⟩ => memCost_mono hn hm, ?_,
+    fun G _ hfit => run_spec G hfit⟩
+  refine Asymptotics.IsBigO.of_bound 104 ?_
+  rw [Filter.eventually_comap]
+  filter_upwards [Filter.eventually_ge_atTop 2] with b hb p hp
+  obtain ⟨n, m⟩ := p
+  simp only at hp
+  subst hp
+  have hL : 1 ≤ Nat.log 2 n := Nat.le_log_of_pow_le (by norm_num) (by simpa using hb)
+  have h : memCost n m ≤ 104 * ((m + 1) * Nat.log 2 n) := by
+    unfold memCost
+    nlinarith
+  simp only [Real.norm_natCast, norm_mul]
+  rw [Real.norm_of_nonneg (by positivity)]
+  exact_mod_cast h
+
+end Cslib.Algorithms.Lean.Dijkstra.Memory
diff --git a/Complexity/DataStructure/AdjacencyList/Memory.lean b/Complexity/DataStructure/AdjacencyList/Memory.lean
new file mode 100644
index 0000000000..04c3ae9a8f
--- /dev/null
+++ b/Complexity/DataStructure/AdjacencyList/Memory.lean
@@ -0,0 +1,225 @@
+/-
+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.DataStructure.AdjacencyList.Spec
+public import Complexity.DataStructure.Memory.Frame
+public import Complexity.DataStructure.Memory.Triple
+
+/-!
+# Adjacency arrays over the memory oracle
+
+The read-only adjacency-list interface `AdjacencyList.spec n` is implemented over
+`Memory.spec w` by compressed adjacency arrays: a field `offsets` whose cell `u` holds the start
+of the list of `u` in the edge array, so that the out-degree of `u` is the difference of two
+consecutive offsets, and a field `edges` holding each edge as two cells, its target and its
+weight. This is the layout in which a word RAM receives a graph as input. A degree query reads
+two offsets, and an edge query reads an offset and the edge's two cells (`amortized`).
+
+The interface never changes its state, so a refinement represents one graph `adj`: its invariant
+says that the arrays hold `adj` (`Holds`), and its abstraction function is constant. The methods
+write nothing (`ops_triple`), and the invariant reads only the two fields, so the arrays are
+framed by their fields and share memory with other structures (`framed`).
+
+## Main definitions
+
+* `Layout`, `Layout.footprint`, `Layout.Valid`: the two fields, their cells, and the length of the
+  offset field.
+* `degree`, `edge`, `ops`, `methods`: the queries as memory programs.
+* `Holds`, `Inv`: the arrays hold a graph, and the implementation invariant.
+* `refinement`, `framed`: the arrays as a refinement of the interface for the graph they hold,
+  framed by their fields.
+
+## Main results
+
+* `ops_triple`: each query returns the specified answer within three memory units, and writes
+  nothing.
+* `amortized`: every query costs at most three memory units.
+
+## References
+
+* [T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, *Introduction to Algorithms*,
+  Section 22.1][CLRS2009]
+-/
+
+@[expose] public section
+
+namespace Cslib.DataStructure.AdjacencyList.Memory
+
+open Cslib.WordRAM Cslib.DataStructure Cslib.DataStructure.Memory
+
+/-- Adjacency arrays: the offset of each vertex's list, and the edges, two cells each. -/
+structure Layout where
+  /-- Cell `u` holds the position of the first edge out of `u`; cell `n` the number of edges. -/
+  offsets : Block
+  /-- Edge `j` occupies cells `2 j` (its target) and `2 j + 1` (its weight). -/
+  edges : Block
+
+namespace Layout
+
+/-- The cells of both fields. -/
+def footprint (L : Layout) : Finset ℕ := L.offsets.footprint ∪ L.edges.footprint
+
+/-- The offset field of a graph on `n` vertices has `n + 1` cells. -/
+structure Valid (L : Layout) (n : ℕ) : Prop where
+  /-- One offset per vertex, and the end of the last list. -/
+  offsets_length : L.offsets.length = n + 1
+
+end Layout
+
+variable {n : ℕ} (L : Layout)
+
+/-- The out-degree of `u`: the difference of two consecutive offsets. -/
+def degree (u : Fin n) : Prog ℕ := do
+  let a ← L.offsets.get u
+  let b ← L.offsets.get (u + 1)
+  pure (b - a)
+
+/-- The `i`-th edge out of `u`: its target and weight, from the edge at the offset of `u` plus
+`i`. A target that is not a vertex cannot occur for an admissible query; the answer is then the
+spec's placeholder `(u, 0)`. -/
+def edge (u : Fin n) (i : ℕ) : Prog (Fin n × ℕ) := do
+  let a ← L.offsets.get u
+  let t ← L.edges.get (2 * (a + i))
+  let c ← L.edges.get (2 * (a + i) + 1)
+  pure (if h : t < n then (⟨t, h⟩, c) else (u, 0))
+
+/-- The queries as memory programs. -/
+def ops : (o : AdjacencyList.Op n) → Prog o.Result
+  | .degree u => degree L u
+  | .edge u i => edge L u i
+
+/-- The queries as methods of `AdjacencyList.spec n` over `Memory.spec w`. -/
+abbrev methods (w : ℕ) : Methods (AdjacencyList.spec n) (Memory.spec w) := ops L
+
+/-- The memory `m` holds the graph `adj` in the layout: consecutive offsets differ by the
+out-degrees, the edges out of `u` follow its offset in order, and every list ends within the edge
+field. -/
+structure Holds (adj : AdjacencyList.State n) (m : ℕ → ℕ) : Prop where
+  /-- The list of `u` ends where the list of `u + 1` starts. -/
+  offset_succ : ∀ u : Fin n,
+    m (L.offsets.base + (u + 1)) = m (L.offsets.base + u) + (adj u).length
+  /-- Every list ends within the edge field. -/
+  end_le : ∀ u : Fin n, 2 * m (L.offsets.base + (u + 1)) ≤ L.edges.length
+  /-- The target of each edge. -/
+  target : ∀ (u : Fin n) (i : ℕ) (hi : i < (adj u).length),
+    m (L.edges.base + 2 * (m (L.offsets.base + u) + i)) = (adj u)[i].1
+  /-- The weight of each edge. -/
+  weight : ∀ (u : Fin n) (i : ℕ) (hi : i < (adj u).length),
+    m (L.edges.base + (2 * (m (L.offsets.base + u) + i) + 1)) = (adj u)[i].2
+
+/-- The implementation invariant for the graph `adj`: both fields are allocated and hold it. -/
+structure Inv (adj : AdjacencyList.State n) (s : Memory.State) : Prop where
+  /-- The offset field is allocated. -/
+  offsets_allocated : L.offsets.Allocated s
+  /-- The edge field is allocated. -/
+  edges_allocated : L.edges.Allocated s
+  /-- The fields hold the graph. -/
+  holds : Holds L adj s.mem
+
+variable {L} {w : ℕ} {adj : AdjacencyList.State n}
+
+/-- The cells an edge query reads lie in the edge field. -/
+theorem Holds.edge_lt {m : ℕ → ℕ} (h : Holds L adj m) (u : Fin n) {i : ℕ}
+    (hi : i < (adj u).length) : 2 * (m (L.offsets.base + u) + i) + 1 < L.edges.length := by
+  have h₁ := h.offset_succ u
+  have h₂ := h.end_le u
+  omega
+
+/-- **Each query returns the specified answer** within three memory units, and writes nothing. -/
+theorem ops_triple (hL : L.Valid n) {s : Memory.State} (hs : Inv L adj s)
+    (o : AdjacencyList.Op n) (hv : AdjacencyList.valid adj o) :
+    Triple w s (ops L o) 3 fun r s' => AdjacencyList.step adj o = (adj, r) ∧ s' = s := by
+  have hoff : ∀ j ≤ n, L.offsets.base + j < s.frontier := fun j hj =>
+    hs.offsets_allocated.lt_frontier (by rw [hL.offsets_length]; omega)
+  cases o with
+  | degree u =>
+    refine Triple.read_bind (hoff u u.isLt.le) <| Triple.read_bind (hoff (u + 1) u.isLt) <|
+      Triple.pure ⟨?_, rfl⟩
+    rw [AdjacencyList.step_degree, hs.holds.offset_succ u]
+    simp
+  | edge u i =>
+    have hlt := hs.holds.edge_lt u hv
+    refine Triple.read_bind (hoff u u.isLt.le) <|
+      Triple.read_bind (hs.edges_allocated.lt_frontier (by omega)) <|
+      Triple.read_bind (hs.edges_allocated.lt_frontier hlt) <| Triple.pure ⟨?_, rfl⟩
+    rw [AdjacencyList.step_edge _ _ hv, hs.holds.target u i hv, hs.holds.weight u i hv]
+    simp
+
+/-- The run of a query, by `ops_triple`. -/
+theorem ops_run (hL : L.Valid n) {s : Memory.State} (hs : Inv L adj s) (o : AdjacencyList.Op n)
+    (hv : AdjacencyList.valid adj o) :
+    (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (ops L o)) ∧
+      (Memory.spec w).totalCost charge s ((Memory.spec w).clientHistory s (ops L o)) ≤ 3 ∧
+      AdjacencyList.step adj o = (adj, (Memory.spec w).clientResult s (ops L o)) ∧
+        (Memory.spec w).clientState s (ops L o) = s :=
+  triple_iff.mp (ops_triple hL hs o hv)
+
+variable (adj) in
+/-- The adjacency arrays implement the interface for the graph `adj` they hold. -/
+def refinement (hL : L.Valid n) : Refinement (AdjacencyList.spec n) (Memory.spec w) :=
+  Refinement.ofFn (methods L w) (Inv L adj) (fun _ => adj)
+    (fun o hs hv => (ops_run hL hs o hv).1)
+    (fun o hs hv => by
+      obtain ⟨-, -, hstep, hs'⟩ := ops_run hL hs o hv
+      exact ⟨hstep, (congrArg (Inv L adj) hs').mpr hs⟩)
+
+/-- The fields are allocated. -/
+theorem Inv.lt_frontier {s : Memory.State} (hs : Inv L adj s) {a : ℕ} (ha : a ∈ L.footprint) :
+    a < s.frontier := by
+  have h₁ := hs.offsets_allocated
+  have h₂ := hs.edges_allocated
+  simp only [Layout.footprint, Finset.mem_union, Block.mem_footprint, Block.Owns] at ha
+  unfold Block.Allocated at h₁ h₂
+  omega
+
+/-- The invariant reads only the two fields and survives a growing frontier. -/
+theorem Inv.congr (hL : L.Valid n) {s s' : Memory.State} (hs : Inv L adj s)
+    (h : ∀ a ∈ L.footprint, s'.mem a = s.mem a) (hf : s.frontier ≤ s'.frontier) :
+    Inv L adj s' := by
+  have hoff : ∀ j ≤ n, s'.mem (L.offsets.base + j) = s.mem (L.offsets.base + j) := fun j hj =>
+    h _ (Finset.mem_union_left _ (Block.mem_footprint.mpr
+      (Block.owns_add (by rw [hL.offsets_length]; omega))))
+  have hedge : ∀ j < L.edges.length, s'.mem (L.edges.base + j) = s.mem (L.edges.base + j) :=
+    fun j hj => h _ (Finset.mem_union_right _ (Block.mem_footprint.mpr (Block.owns_add hj)))
+  have H := hs.holds
+  refine ⟨hs.offsets_allocated.mono hf, hs.edges_allocated.mono hf, ⟨fun u => ?_, fun u => ?_,
+    fun u i hi => ?_, fun u i hi => ?_⟩⟩
+  · rw [hoff _ u.isLt, hoff _ u.isLt.le]
+    exact H.offset_succ u
+  · rw [hoff _ u.isLt]
+    exact H.end_le u
+  · have := H.edge_lt u hi
+    rw [hoff _ u.isLt.le, hedge _ (by omega)]
+    exact H.target u i hi
+  · have := H.edge_lt u hi
+    rw [hoff _ u.isLt.le, hedge _ this]
+    exact H.weight u i hi
+
+variable (adj) in
+/-- The adjacency arrays, framed by their two fields. -/
+def framed (hL : L.Valid n) : Memory.Framed (AdjacencyList.spec n) w :=
+  .ofStatic (refinement adj hL) L.footprint (fun hs ha => Inv.lt_frontier hs ha)
+    (fun hs h hf => ⟨hs.congr hL h hf, rfl⟩)
+    (fun o hs hv b _ _ => by
+      obtain ⟨-, -, -, hs'⟩ := ops_run (w := w) hL hs o hv
+      change ((Memory.spec w).clientState _ (ops L o)).mem b = _
+      rw [hs'])
+
+/-- The footprint of the arrays is their two fields. -/
+@[simp] theorem framed_footprint (hL : L.Valid n) (s : Memory.State) :
+    (framed (w := w) adj hL).footprint s = L.footprint := rfl
+
+/-- **Every query costs at most three memory units.** -/
+theorem amortized (hL : L.Valid n) :
+    (framed (w := w) adj hL).Amortized charge (fun _ _ => 3) fun _ => 0 :=
+  Refinement.Amortized.ofFn fun {_} o hs hv => by
+    obtain ⟨-, hc, -⟩ := ops_run (w := w) hL hs o hv
+    exact Nat.add_le_add_right hc 0
+
+end Cslib.DataStructure.AdjacencyList.Memory
diff --git a/Complexity/DataStructure/Dictionary/Memory.lean b/Complexity/DataStructure/Dictionary/Memory.lean
new file mode 100644
index 0000000000..433b139bc6
--- /dev/null
+++ b/Complexity/DataStructure/Dictionary/Memory.lean
@@ -0,0 +1,188 @@
+/-
+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.DataStructure.Dictionary.Spec
+public import Complexity.DataStructure.Memory.Frame
+public import Complexity.DataStructure.Memory.Triple
+
+/-!
+# A direct-address table over the memory oracle
+
+The dictionary `Dictionary.spec U V n_max` on the keys `Fin U` is implemented as a direct-address
+table: a field `T` of `U` cells, one per key, holding `0` for an absent key and `v + 1` for the
+value `v` (`decode`). A lookup reads the key's cell and an insertion writes it, one memory unit
+each (`amortized`). The table has a cell for every key, so the capacity `n_max` never binds.
+Values below `V` are stored, so `V` must fit a word.
+
+The table is framed by its field (`framed`), so it shares memory with other structures. Allocated
+in memory that is zero above the frontier, it starts empty at the cost of one memory unit
+(`inv_alloc`).
+
+## Main definitions
+
+* `decode`: the value of a cell, `0` for absent.
+* `get`, `insert`, `ops`, `methods`: the operations as memory programs.
+* `abs`, `Inv`, `Valid`: the abstraction function, the implementation invariant and the static
+  well-formedness of the field.
+* `refinement`, `framed`: the table as a refinement of the dictionary, framed by its field.
+
+## Main results
+
+* `amortized`: every operation costs one memory unit.
+* `inv_alloc`: a field allocated in memory that is zero above the frontier is an empty table.
+
+## References
+
+* [T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, *Introduction to Algorithms*,
+  Section 11.1][CLRS2009]
+-/
+
+@[expose] public section
+
+namespace Cslib.DataStructure.Dictionary.Memory
+
+open Cslib.WordRAM Cslib.DataStructure Cslib.DataStructure.Memory
+
+/-- The value stored in a cell: `0` is an absent key, and `v + 1` the value `v`. This is the
+word encoding of `Option ℕ` that the word-RAM dictionaries use. -/
+def decode : ℕ → Option ℕ
+  | 0 => none
+  | v + 1 => some v
+
+@[simp] theorem decode_zero : decode 0 = none := rfl
+
+@[simp] theorem decode_succ (v : ℕ) : decode (v + 1) = some v := rfl
+
+variable {U : ℕ} (T : Block)
+
+/-- Look up a key: read its cell. -/
+def get (u : Fin U) : Prog (Option ℕ) := do
+  let x ← T.get u
+  pure (decode x)
+
+/-- Store the value `v` for a key: write `v + 1` to its cell. -/
+def insert (u : Fin U) (v : ℕ) : Prog Unit := T.set u (v + 1)
+
+/-- The dictionary operations as memory programs. -/
+def ops : (o : Dictionary.Op U) → Prog o.Result
+  | .get u => get T u
+  | .insert u v => insert T u v
+
+/-- The operations as methods of `Dictionary.spec U V n_max` over `Memory.spec w`. -/
+abbrev methods (w V n_max : ℕ) : Methods (Dictionary.spec U V n_max) (Memory.spec w) := ops T
+
+/-- The represented dictionary: the decoded cell of each key. -/
+def abs (s : Memory.State) : Dictionary.State U := fun u => decode (s.mem (T.base + u))
+
+/-- The implementation invariant: the field is allocated. -/
+abbrev Inv (s : Memory.State) : Prop := T.Allocated s
+
+/-- Static well-formedness for `U` keys and values below `V` at word size `w`: one cell per key,
+and `V` fits a word, so every stored `v + 1` does. -/
+structure Valid (T : Block) (w U V : ℕ) : Prop where
+  /-- One cell per key. -/
+  length_eq : T.length = U
+  /-- The value bound fits a word. -/
+  value_fits : Fits w V
+
+variable {T} {w V n_max : ℕ}
+
+/-- The cell of a key is allocated. -/
+theorem cell_lt (hT : Valid T w U V) {s : Memory.State} (hs : Inv T s) (u : Fin U) :
+    T.base + u < s.frontier :=
+  Block.Allocated.lt_frontier hs (by rw [hT.length_eq]; exact u.isLt)
+
+/-- The cell of a key belongs to the field. -/
+theorem mem_footprint (hT : Valid T w U V) (u : Fin U) : T.base + u ∈ T.footprint :=
+  Block.mem_footprint.mpr (Block.owns_add (by rw [hT.length_eq]; exact u.isLt))
+
+/-- An owned cell of an allocated field is allocated. -/
+theorem lt_of_owns {s : Memory.State} (hs : Inv T s) {a : ℕ} (ha : T.Owns a) : a < s.frontier := by
+  unfold Block.Owns at ha
+  unfold Inv Block.Allocated at hs
+  omega
+
+variable (T) in
+/-- What a run of the operation `o` from `s` establishes: the specified step, the invariant, and
+no change to the frontier or to any cell outside the field. -/
+def Post (s : Memory.State) (o : Dictionary.Op U) (r : o.Result) (s' : Memory.State) : Prop :=
+  Dictionary.step (abs T s) o = (abs T s', r) ∧ Inv T s' ∧ s'.frontier = s.frontier ∧
+    ∀ a ∉ T.footprint, s'.mem a = s.mem a
+
+/-- **Each operation realizes the specified step** with one memory operation. -/
+theorem ops_triple (hT : Valid T w U V) {s : Memory.State} (hs : Inv T s) (o : Dictionary.Op U)
+    (hv : (Dictionary.spec U V n_max).valid (abs T s) o) : Triple w s (ops T o) 1 (Post T s o) := by
+  cases o with
+  | get u =>
+    exact Triple.read_bind (cell_lt hT hs u)
+      (Triple.pure ⟨rfl, hs, rfl, fun _ _ => rfl⟩)
+  | insert u v =>
+    refine Triple.write_bind (cell_lt hT hs u) (hT.value_fits.of_le hv.2) <|
+      Triple.pure ⟨?_, hs, rfl, fun a ha => Function.update_of_ne
+        (fun h => ha (by rw [h]; exact mem_footprint hT u)) _ _⟩
+    refine Prod.ext (funext fun u' => ?_) rfl
+    by_cases hu : u' = u
+    · subst hu
+      simp [abs]
+    · have : (T.base + u' : ℕ) ≠ T.base + u := by
+        have := Fin.val_ne_of_ne hu
+        omega
+      simp [abs, hu, Function.update_of_ne this]
+
+/-- The run of an operation, by `ops_triple`. -/
+theorem ops_run (hT : Valid T w U V) {s : Memory.State} (hs : Inv T s) (o : Dictionary.Op U)
+    (hv : (Dictionary.spec U V n_max).valid (abs T s) o) :
+    (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (ops T o)) ∧
+      (Memory.spec w).totalCost charge s ((Memory.spec w).clientHistory s (ops T o)) ≤ 1 ∧
+      Post T s o ((Memory.spec w).clientResult s (ops T o))
+        ((Memory.spec w).clientState s (ops T o)) :=
+  triple_iff.mp (ops_triple hT hs o hv)
+
+/-- The direct-address table implements the dictionary. -/
+def refinement (hT : Valid T w U V) : Refinement (Dictionary.spec U V n_max) (Memory.spec w) :=
+  Refinement.ofFn (methods T w V n_max) (Inv T) (abs T)
+    (fun o hs hv => (ops_run hT hs o hv).1)
+    (fun o hs hv => by
+      obtain ⟨-, -, hstep, hinv, -⟩ := ops_run hT hs o hv
+      exact ⟨hstep, hinv⟩)
+
+/-- The abstraction reads only the field. -/
+theorem abs_congr (hT : Valid T w U V) {s s' : Memory.State}
+    (h : ∀ a ∈ T.footprint, s'.mem a = s.mem a) : abs (U := U) T s' = abs T s :=
+  funext fun u => by simp only [abs, h _ (mem_footprint hT u)]
+
+/-- The table, framed by its field. -/
+def framed (hT : Valid T w U V) : Memory.Framed (Dictionary.spec U V n_max) w :=
+  .ofStatic (refinement hT) T.footprint (fun hs ha => lt_of_owns hs (Block.mem_footprint.mp ha))
+    (fun hs h hf => ⟨Block.Allocated.mono hs hf, abs_congr hT h⟩)
+    (fun o hs hv b _ hb => by
+      obtain ⟨-, -, -, -, -, h⟩ := ops_run hT hs o hv
+      exact h b hb)
+
+/-- The footprint of a table is its field. -/
+@[simp] theorem framed_footprint (hT : Valid T w U V) (s : Memory.State) :
+    (framed (n_max := n_max) hT).footprint s = T.footprint := rfl
+
+/-- **Every operation costs one memory unit.** -/
+theorem amortized (hT : Valid T w U V) :
+    (framed (n_max := n_max) hT).Amortized charge (fun _ _ => 1) fun _ => 0 :=
+  Refinement.Amortized.ofFn fun {_} o hs hv => by
+    obtain ⟨-, hc, -⟩ := ops_run (w := w) hT hs o hv
+    exact Nat.add_le_add_right hc 0
+
+/-- A field allocated without clearing in memory that is zero above the frontier is an empty
+table. -/
+theorem inv_alloc {s : Memory.State} (hz : ZeroAbove s) :
+    Inv ⟨s.frontier, U⟩ ⟨s.mem, s.frontier + U⟩ ∧
+      abs ⟨s.frontier, U⟩ ⟨s.mem, s.frontier + U⟩ = Dictionary.empty U := by
+  refine ⟨le_rfl, funext fun u => ?_⟩
+  change decode (s.mem (s.frontier + u)) = none
+  rw [hz _ (Nat.le_add_right _ _), decode_zero]
+
+end Cslib.DataStructure.Dictionary.Memory
diff --git a/ComplexityTests/DijkstraMemory.lean b/ComplexityTests/DijkstraMemory.lean
new file mode 100644
index 0000000000..f1210426c9
--- /dev/null
+++ b/ComplexityTests/DijkstraMemory.lean
@@ -0,0 +1,63 @@
+/-
+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.Algorithms.Lean.Dijkstra.Memory
+
+/-!
+# Dijkstra's algorithm with a binary heap, run on the word RAM's input convention
+
+The graph of `ComplexityTests/Dijkstra.lean`, with a parallel edge and a shorter path through a
+third vertex, is written in the input convention and given to `Dijkstra.Memory.run` at word size
+`16`. The tests check the distances it leaves past the input, the admissibility of every memory
+operation, its exact memory cost against the proved bound `memCost 3 4 = 520`, and that
+`run_spec` applies to this graph.
+-/
+
+open Cslib.WordRAM Cslib.DataStructure
+open Cslib.Algorithms.WordRAM.Dijkstra (ListInstance encodeDist)
+open Cslib.Algorithms.Lean.Dijkstra.Memory
+
+set_option linter.hashCommand false
+
+namespace DijkstraMemoryTests
+
+/-- Edges `0 → 1` of weights `4` and `5`, `0 → 2` of weight `1`, and `2 → 1` of weight `2`, from
+source `0`. The distances are `0`, `3` and `1`. -/
+def graph : ListInstance where
+  n := 3
+  adj := ![[(1, 4), (2, 1), (1, 5)], [], [(1, 2)]]
+  source := 0
+
+/-- The input words: `n`, the source, four offsets and four edges. -/
+example : graph.encode = [3, 0, 0, 3, 3, 4, 1, 4, 2, 1, 1, 5, 1, 2] := by decide
+
+/-- The memory of the input convention. -/
+def input : Memory.State := Memory.State.init graph.encode
+
+-- The cells just past the input hold the encoded distances `0 + 1`, `3 + 1` and `1 + 1`.
+#guard (List.finRange 3).map (fun v =>
+  ((Memory.spec 16).clientState input run).mem (graph.outAddr v)) = [1, 4, 2]
+
+-- Every memory operation of the run is admissible at word size `16`.
+#guard decide ((Memory.spec 16).ValidHistory input ((Memory.spec 16).clientHistory input run))
+
+-- Its exact memory cost, within `memCost 3 4 = 520`.
+#guard (Memory.spec 16).totalCost Memory.charge input
+  ((Memory.spec 16).clientHistory input run) = 75
+
+example : memCost 3 4 = 520 := by decide
+
+/-- The word size `16` holds `8 (n + m + 2) (W + 2) = 504`, so `run_spec` applies. -/
+theorem fits : Fits 16 (8 * (graph.n + graph.m + 2) * (graph.maxWeight + 2)) := by decide
+
+/-- By `run_spec`, the cell of vertex `1` holds its encoded distance. -/
+example : ((Memory.spec 16).clientState input run).mem (graph.outAddr ⟨1, by decide⟩) =
+    encodeDist (graph.dist graph.source ⟨1, by decide⟩) :=
+  (run_spec graph fits).2.1 _
+
+/-- A word size too small for the input: `504` does not fit eight bits. -/
+example : ¬Fits 8 (8 * (graph.n + graph.m + 2) * (graph.maxWeight + 2)) := by decide
+
+end DijkstraMemoryTests