From 82735f7c11529319ecfff8271ae0724e23142762 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 1 Nov 2026 20:17:53 -0500 Subject: [PATCH 1/2] test(DataStructure): run a Fibonacci heap client over memory ComplexityTests/FibonacciHeapMemory runs an indexed priority-queue client (four inserts, an extraction that consolidates, a key decrease that cuts, two more extractions) over memory through memRefinement, and checks the answers, the exact memory cost (213), the amortized bound of charge (920), and that simulates_client and Amortized.client with mem_amortized apply. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- ComplexityTests/FibonacciHeapMemory.lean | 133 +++++++++++++++++++++++ 1 file changed, 133 insertions(+) create mode 100644 ComplexityTests/FibonacciHeapMemory.lean diff --git a/ComplexityTests/FibonacciHeapMemory.lean b/ComplexityTests/FibonacciHeapMemory.lean new file mode 100644 index 0000000000..7f48c6535b --- /dev/null +++ b/ComplexityTests/FibonacciHeapMemory.lean @@ -0,0 +1,133 @@ +/- +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.PriorityQueue.FibonacciHeap.Memory + +/-! +# The Fibonacci heap over memory, on a concrete client + +A client of the indexed priority queue on four handles inserts four keys, extracts the minimum +(which consolidates the other three), decreases a key below its parent's (which cuts it), and +extracts the minimum twice more. It runs over memory through `memRefinement`, with the heap's +`9 · 4 + 5 = 41` cells zeroed at addresses `0, …, 40`, at word size `6`. + +The tests check the answers against the specification, the exact memory cost of the run, the +amortized bound `4 · 43 + 104 + 276 + 2 · 184 = 920` of `charge`, and that the general theorems +apply: `simulates_client` gives the answers and admissibility, and `Amortized.client` with +`mem_amortized` gives the bound. +-/ + +@[expose] public section + +namespace ComplexityTests.FibonacciHeapMemory + +open Cslib.WordRAM Cslib.DataStructure Cslib.DataStructure.PriorityQueue + Cslib.DataStructure.PriorityQueue.FibonacciHeap + +/-- The indexed priority queue on four handles with keys at most `9`. -/ +abbrev pq : StateTransitionSpec := indexedMinPQSpec 4 9 + +/-- Insert keys `5, 3, 8, 6` at handles `0, 1, 2, 3`; extract the minimum; lower the key of `2` +to `1`; extract the minimum twice. -/ +def client : pq.Client (List (Option (Fin 4 × ℕ))) := do + pq.call (.insert 0 5) + pq.call (.insert 1 3) + pq.call (.insert 2 8) + pq.call (.insert 3 6) + let a ← pq.call .extractMin + pq.call (.decreaseKey 2 1) + let b ← pq.call .extractMin + let c ← pq.call .extractMin + pure [a, b, c] + +/-- The specification's answers: `(1, 3)`, then the lowered `(2, 1)`, then `(0, 5)`. -/ +example : + pq.clientResult (IndexedMinPQ.empty 4) client = [some (1, 3), some (2, 1), some (0, 5)] := by + decide + +/-- The client is admissible: handles are fresh on insertion, and the key decrease lowers a +present key. -/ +theorem client_valid : pq.ValidHistory (IndexedMinPQ.empty 4) + (pq.clientHistory (IndexedMinPQ.empty 4) client) := + ⟨⟨by decide, by decide⟩, ⟨by decide, by decide⟩, ⟨by decide, by decide⟩, ⟨by decide, by decide⟩, + trivial, ⟨⟨8, by decide, by decide⟩, by decide⟩, trivial, trivial, trivial⟩ + +/-- Word size `6` fits the handle count and the key bound. -/ +theorem hn : Fits 6 4 := by decide + +theorem hK : Fits 6 9 := by decide + +/-- The heap over memory at base address `0`. -/ +abbrev heap : Refinement pq (Memory.spec 6) := memRefinement hn hK 0 + +/-- Memory with the heap's 41 cells allocated and zeroed. -/ +def mem : Memory.State := ⟨fun _ => 0, 41⟩ + +/-- The zeroed cells hold the empty heap. -/ +theorem mem_inv : heap.inv mem := by + refine ⟨fun i hi => ?_, ?_⟩ + · cases i <;> simp only [Cell.ok, layout, mem] at hi ⊢ <;> omega + · have hzero : (layout 4 0).abs mem = fun _ => 0 := by + funext i + simp [Record.Layout.abs, mem] + change Inv 4 9 ((layout 4 0).abs mem) + rw [hzero] + exact (inv_of_fibRawInv (WordRAM.FibonacciHeap.FibRawInv.empty (fun _ => rfl) + (fun _ _ => rfl) rfl rfl rfl rfl)).1 + +theorem abs_mem : heap.abs mem = IndexedMinPQ.empty 4 := by + funext v + fin_cases v <;> decide + +set_option maxRecDepth 20000 in +/-- The run over memory gives the same answers. -/ +example : (Memory.spec 6).clientResult mem (link heap.methods client) = + [some (1, 3), some (2, 1), some (0, 5)] := by + decide + +set_option maxRecDepth 20000 in +/-- Its exact cost: `213` memory units, one per record operation. -/ +example : (Memory.spec 6).totalCost Memory.charge mem + ((Memory.spec 6).clientHistory mem (link heap.methods client)) = 213 := by + decide + +/-- The amortized bound: `43` per insertion, `104` for the key decrease, and +`92 · (log₂ m + 1)` for an extraction from `m` handles: `276` from four, `184` from three and +from two. -/ +example : pq.totalCost (charge 4) (IndexedMinPQ.empty 4) + (pq.clientHistory (IndexedMinPQ.empty 4) client) = 920 := by + decide + +set_option maxRecDepth 20000 in +/-- **The refinement theorem applies**: the memory run is admissible and answers as the +specification. -/ +example : (Memory.spec 6).ValidHistory mem + ((Memory.spec 6).clientHistory mem (link heap.methods client)) ∧ + (Memory.spec 6).clientResult mem (link heap.methods client) = + pq.clientResult (IndexedMinPQ.empty 4) client := by + obtain ⟨hv, hres, -⟩ := + heap.simulates_client client mem_inv (by rw [abs_mem]; exact client_valid) + rw [abs_mem] at hres + exact ⟨hv, hres⟩ + +set_option maxRecDepth 20000 in +/-- **The amortized bound applies**: the memory cost and the final potential are at most `920`, +the empty heap's potential being `0`. -/ +example : (Memory.spec 6).totalCost Memory.charge mem + ((Memory.spec 6).clientHistory mem (link heap.methods client)) ≤ 920 := by + have h := (mem_amortized hn hK 0).client client mem_inv (by rw [abs_mem]; exact client_valid) + have hΦ : potential 4 ((layout 4 0).abs mem) + 0 = 0 := by decide + have hcharge : pq.totalCost (charge 4) (heap.abs mem) (pq.clientHistory (heap.abs mem) client) = + 920 := by + rw [abs_mem] + decide + rw [hcharge, hΦ] at h + exact (Nat.le_add_right _ _).trans h + +end ComplexityTests.FibonacciHeapMemory From 3ea2c8cdf3ee10f457c101db8b6769184bb6f250 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 6 Nov 2026 02:53:19 +0000 Subject: [PATCH 2/2] test(DataStructure): import fin_cases in the Fibonacci heap memory test main no longer provides Mathlib.Tactic.FinCases transitively through FibonacciHeap.Memory; import it directly. No statement or proof changes. Session: restack-a-jetski-fd1a2b3c --- ComplexityTests/FibonacciHeapMemory.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/ComplexityTests/FibonacciHeapMemory.lean b/ComplexityTests/FibonacciHeapMemory.lean index 7f48c6535b..2fbb617ae0 100644 --- a/ComplexityTests/FibonacciHeapMemory.lean +++ b/ComplexityTests/FibonacciHeapMemory.lean @@ -8,6 +8,7 @@ module -- upstream: local-only (test driver) public import Complexity.DataStructure.PriorityQueue.FibonacciHeap.Memory +import Mathlib.Tactic.FinCases /-! # The Fibonacci heap over memory, on a concrete client