diff --git a/Complexity.lean b/Complexity.lean index 43d3104b91..3a3eab508c 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2949,6 +2949,7 @@ 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.Alloc public import Complexity.DataStructure.Memory.Field public import Complexity.DataStructure.Memory.Frame public import Complexity.DataStructure.Memory.Spec diff --git a/Complexity/Algorithms/Lean/Dijkstra/Memory.lean b/Complexity/Algorithms/Lean/Dijkstra/Memory.lean index 62e06022a5..8a9081023f 100644 --- a/Complexity/Algorithms/Lean/Dijkstra/Memory.lean +++ b/Complexity/Algorithms/Lean/Dijkstra/Memory.lean @@ -176,12 +176,14 @@ theorem holds_inputGraph (G : ListInstance) : /-- **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. -/ +graph. The structures share memory only while its frontier fits a word (`Memory.Framed.Apart`). -/ 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) : + (hA : (inputGraph G.n G.m).Valid G.n) + (hfit : Fits w ((Memory.State.init G.encode).frontier + G.n + 1 + + PriorityQueue.WordRAM.BinaryHeap.space 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⟩ ∧ @@ -202,13 +204,15 @@ theorem inv_input (G : ListInstance) {w K V : ℕ} ⟨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] + · refine ⟨?_, hfit⟩ + 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, + · refine ⟨?_, hfit⟩ + 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 @@ -300,6 +304,7 @@ theorem run_triple (G : ListInstance) {w : ℕ} 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 + (hfit.of_le (by simp only [PriorityQueue.WordRAM.BinaryHeap.space]; nlinarith)) 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 diff --git a/Complexity/DataStructure/AdjacencyList/Memory.lean b/Complexity/DataStructure/AdjacencyList/Memory.lean index 04c3ae9a8f..f87b81bddc 100644 --- a/Complexity/DataStructure/AdjacencyList/Memory.lean +++ b/Complexity/DataStructure/AdjacencyList/Memory.lean @@ -210,6 +210,10 @@ def framed (hL : L.Valid n) : Memory.Framed (AdjacencyList.spec n) w := obtain ⟨-, -, -, hs'⟩ := ops_run (w := w) hL hs o hv change ((Memory.spec w).clientState _ (ops L o)).mem b = _ rw [hs']) + (fun o hs hv => by + obtain ⟨-, -, -, hs'⟩ := ops_run (w := w) hL hs o hv + change ((Memory.spec w).clientState _ (ops L o)).frontier = _ + rw [hs']) /-- The footprint of the arrays is their two fields. -/ @[simp] theorem framed_footprint (hL : L.Valid n) (s : Memory.State) : diff --git a/Complexity/DataStructure/Dictionary/Memory.lean b/Complexity/DataStructure/Dictionary/Memory.lean index 433b139bc6..9d175ebd81 100644 --- a/Complexity/DataStructure/Dictionary/Memory.lean +++ b/Complexity/DataStructure/Dictionary/Memory.lean @@ -164,6 +164,9 @@ def framed (hT : Valid T w U V) : Memory.Framed (Dictionary.spec U V n_max) w := (fun o hs hv b _ hb => by obtain ⟨-, -, -, -, -, h⟩ := ops_run hT hs o hv exact h b hb) + (fun o hs hv => by + obtain ⟨-, -, -, -, h, -⟩ := ops_run hT hs o hv + exact h) /-- The footprint of a table is its field. -/ @[simp] theorem framed_footprint (hT : Valid T w U V) (s : Memory.State) : diff --git a/Complexity/DataStructure/Memory/Alloc.lean b/Complexity/DataStructure/Memory/Alloc.lean new file mode 100644 index 0000000000..1d2d11b11c --- /dev/null +++ b/Complexity/DataStructure/Memory/Alloc.lean @@ -0,0 +1,584 @@ +/- +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.Memory.Frame +public import Complexity.Foundations.Analysis.Asymptotics.CostBound + +/-! +# Allocating data structures over the memory oracle + +A program that uses data structures over `Memory.spec w` first allocates their storage, then runs +a client of their specification through their methods. A `Memory.Allocator D w` packages the +first half for a specification `D`: + +* the allocation program, which returns a handle such as a layout of named fields; +* the methods, given the handle; +* the abstract state the allocation sets up, the room it needs, and a bound on its cost; +* for each memory with that room, the framed refinement it sets up (`Allocator.framed`), with the + proof that the allocation sets it up (`Memory.Allocates`). + +The structure's footprint lies in fresh cells, which the allocation and later operations take +from the frontier, and in the allocated cells `Allocator.owned` that it takes over. A structure +allocated from scratch takes over none. One that the input already holds, such as a graph given +as adjacency arrays, takes over the cells holding it, and its precondition `Allocator.Pre` says +that they do. `Allocator.resident` is the allocator of a framed structure already in memory, +whose allocation does nothing. + +`Allocator.run` allocates and then runs a client. `Allocator.run_correct` and +`Allocator.run_cost` hold for every allocator and every client: a client admissible for the +specification issues only admissible memory operations, answers as the specification does, and +costs at most the allocation's cost, the potential once allocated, and the upper charges of its +operations. A certificate `Allocator.Amortized` carries the cost side. `Allocator.run_cost_isBigO` +exports a constant per-operation charge as `O(m)` in the number `m` of operations. + +Allocators combine as their structures do. + +* `Allocator.prod` allocates two structures one after the other, and sets up their product over + one memory (`Memory.Framed.prod`). Its room is the sum of the rooms, so it reserves both + structures' growth. Iterated, `A₁.prod (A₂.prod A₃)` allocates the three structures of a client + such as Dijkstra's algorithm, which runs over `product PQ (product Dict Adj)`. +* `Allocator.comp` puts a refinement on top, such as a queue over the pair of its stacks, with + `Memory.Framed.comp`. + +Certificates combine along with them (`Allocator.Amortized.prod`, `Allocator.Amortized.comp`, +`Allocator.Amortized.resident`). An allocation changes no allocated cell, and being admissible, +no cell beyond its new frontier either (`Memory.mem_clientState_of_frontier_le`). So it keeps the +other structures' preconditions, such as that the memory beyond the frontier is zero, and the +cells they take over (`Allocator.pre_fresh`, `Allocator.owned_fresh`). The product's +precondition (`Allocator.ProdPre`) asks in addition that the cells the two structures take over +be disjoint. So `A₁.prod (A₂.prod A₃)` may combine structures allocated from scratch with +structures that the input holds. + +## Main definitions + +* `Memory.Allocates`: what an allocation program establishes for the structure it sets up. +* `Memory.Allocator`: an allocation program, the methods it sets up, and their framed refinement. +* `Memory.Allocator.run`: allocate, then run a client. +* `Memory.Allocator.prod`, `Memory.Allocator.comp`: products and refinements on top. +* `Memory.Allocator.ProdPre`: the precondition of a product. +* `Memory.Allocator.resident`: a structure already in memory. +* `Memory.Allocator.Amortized`: an amortized cost certificate of an allocator. + +## Main results + +* `Memory.Allocator.run_correct`: the run is admissible and answers as the specification. +* `Memory.Allocator.run_cost`, `Memory.Allocator.run_cost_le`: its memory cost. +* `Memory.Allocator.run_cost_isBigO`: the cost as `O(m)` for constant per-operation charges. +* `Memory.Allocator.Amortized.prod`, `Memory.Allocator.Amortized.comp`, + `Memory.Allocator.Amortized.resident`: certificates combine, and carry over to structures + already in memory. +-/ + +@[expose] public section + +namespace Cslib.DataStructure.Memory + +open Cslib.WordRAM + +variable {w : ℕ} + +/-- What running the allocation program `alloc` from the memory `s` establishes for the framed +refinement `M`: its operations are admissible and cost at most `cost`, it changes no allocated +cell, and it sets up `M` with the methods of the handle it returns, holding at the abstract state +`init`. The footprint lies in the allocated cells `owned` that the structure takes over and in +fresh cells, and the frontier plus `M`'s room is at most `room` beyond the old frontier. -/ +structure Allocates {D : StateTransitionSpec.{0, 0, 0}} {H : Type} (alloc : Prog H) + (methods : H → Methods D (spec w)) (init : D.State) (owned : Finset ℕ) (room cost : ℕ) + (s : State) (M : Framed D w) : Prop where + /-- The allocation's operations are admissible. -/ + validHistory : (spec w).ValidHistory s ((spec w).clientHistory s alloc) + /-- The allocation costs at most `cost`. -/ + cost_le : (spec w).totalCost charge s ((spec w).clientHistory s alloc) ≤ cost + /-- The allocation changes no allocated cell. -/ + mem_eq : ∀ a < s.frontier, ((spec w).clientState s alloc).mem a = s.mem a + /-- The structure runs the methods of the returned handle. -/ + methods_eq : M.methods = methods ((spec w).clientResult s alloc) + /-- The structure holds after the allocation. -/ + inv : M.inv ((spec w).clientState s alloc) + /-- It represents `init`. -/ + abs_eq : M.abs ((spec w).clientState s alloc) = init + /-- Its footprint lies in the cells it takes over and in fresh cells. -/ + of_mem_footprint : ∀ a ∈ M.footprint ((spec w).clientState s alloc), a ∈ owned ∨ s.frontier ≤ a + /-- The allocation and the structure's reserved room take at most `room` cells. -/ + room_le : ((spec w).clientState s alloc).frontier + M.room ((spec w).clientState s alloc) ≤ + s.frontier + room + +/-- **Allocators.** A memory program `alloc` that allocates a structure implementing `D`, and +the structure's methods, given the handle that `alloc` returns. From a memory satisfying `Pre` in +which `room` cells beyond the frontier fit a word, the allocation sets up the framed refinement +`framed s`, which represents `init`, at a memory cost of at most `cost`. Its footprint lies in +fresh cells and in the allocated cells `owned s` that it takes over, such as an input that holds +the structure already. -/ +structure Allocator (D : StateTransitionSpec.{0, 0, 0}) (w : ℕ) where + /-- What the allocation returns, such as a layout of named fields. -/ + Handle : Type + /-- The allocation program. -/ + alloc : Prog Handle + /-- The structure's methods, given the handle. -/ + methods : Handle → Methods D (spec w) + /-- The abstract state the allocation sets up. -/ + init : D.State + /-- The cells the allocation takes and the room it reserves for growth. -/ + room : ℕ + /-- A bound on the memory cost of the allocation. -/ + cost : ℕ + /-- What the allocation needs of the memory besides room, such as the structure it takes + over. -/ + Pre : State → Prop := fun _ => True + /-- The allocated cells that the structure takes over instead of allocating them. -/ + owned : State → Finset ℕ := fun _ => ∅ + /-- The cells taken over are allocated. -/ + owned_lt : ∀ {s a}, Pre s → a ∈ owned s → a < s.frontier := by intros; simp_all + /-- Runs that keep every allocated cell and every cell beyond the new frontier and leave the + room fitting, such as other allocations, keep the precondition. -/ + pre_fresh : ∀ {s s' : State}, Pre s → (∀ a < s.frontier, s'.mem a = s.mem a) → + (∀ a, s'.frontier ≤ a → s'.mem a = s.mem a) → s.frontier ≤ s'.frontier → + Fits w (s'.frontier + room) → Pre s' := by intros; trivial + /-- Such runs keep the cells taken over. -/ + owned_fresh : ∀ {s s' : State}, Pre s → (∀ a < s.frontier, s'.mem a = s.mem a) → + (∀ a, s'.frontier ≤ a → s'.mem a = s.mem a) → s.frontier ≤ s'.frontier → + Fits w (s'.frontier + room) → owned s' = owned s := by intros; rfl + /-- The framed refinement that allocating from `s` sets up. -/ + framed : (s : State) → Pre s → Fits w (s.frontier + room) → Framed D w + /-- Allocating from `s` sets it up. -/ + allocates : ∀ s (hs : Pre s) (hroom : Fits w (s.frontier + room)), + Allocates alloc methods init (owned s) room cost s (framed s hs hroom) + +namespace Allocator + +variable {D D₁ D₂ E : StateTransitionSpec.{0, 0, 0}} + +/-! ## Runs -/ + +section Run + +variable (A : Allocator D w) + +/-- Allocate the structure, then run a client of its specification through its methods. -/ +def run {β : Type} (p : D.Client β) : Prog β := A.alloc >>= fun h => link (A.methods h) p + +/-- The history of a run: the allocation's, then the linked client's. -/ +theorem clientHistory_run {β : Type} (p : D.Client β) (s : State) : + (spec w).clientHistory s (A.run p) = (spec w).clientHistory s A.alloc ++ + (spec w).clientHistory ((spec w).clientState s A.alloc) + (link (A.methods ((spec w).clientResult s A.alloc)) p) := + (spec w).clientHistory_bind _ _ s + +/-- The answer of a run is the linked client's. -/ +theorem clientResult_run {β : Type} (p : D.Client β) (s : State) : + (spec w).clientResult s (A.run p) = + (spec w).clientResult ((spec w).clientState s A.alloc) + (link (A.methods ((spec w).clientResult s A.alloc)) p) := + (spec w).clientResult_bind _ _ s + +/-- A run ends where the linked client ends. -/ +theorem clientState_run {β : Type} (p : D.Client β) (s : State) : + (spec w).clientState s (A.run p) = + (spec w).clientState ((spec w).clientState s A.alloc) + (link (A.methods ((spec w).clientResult s A.alloc)) p) := + (spec w).clientState_bind _ _ s + +variable {fD : (s : D.State) → (o : D.Op) → D.State × D.Result o} [D.HasStepFn fD] + +/-- **Correctness of a run.** From a memory with the allocator's precondition and room, a client +admissible for the specification issues only admissible memory operations and answers as the +specification does from `A.init`; the structure then holds at the specified final state. -/ +theorem run_correct {β : Type} (p : D.Client β) {s : State} (hs : A.Pre s) + (hroom : Fits w (s.frontier + A.room)) (hv : D.ValidHistory A.init (D.clientHistory A.init p)) : + (spec w).ValidHistory s ((spec w).clientHistory s (A.run p)) ∧ + (spec w).clientResult s (A.run p) = D.clientResult A.init p ∧ + (A.framed s hs hroom).inv ((spec w).clientState s (A.run p)) ∧ + (A.framed s hs hroom).abs ((spec w).clientState s (A.run p)) = D.clientState A.init p := by + have hA := A.allocates s hs hroom + obtain ⟨hvE, hres, habs, hinv⟩ := + (A.framed s hs hroom).simulates_client p hA.inv (by rw [hA.abs_eq]; exact hv) + rw [hA.methods_eq] at hvE hres habs hinv + rw [hA.abs_eq] at hres habs + rw [clientHistory_run, clientResult_run, clientState_run, + StateTransitionSpec.validHistory_append, StateTransitionSpec.run_runClient] + exact ⟨⟨hA.validHistory, hvE⟩, hres, hinv, habs⟩ + +end Run + +/-! ## Cost certificates -/ + +/-- **An amortized cost certificate of an allocator.** From every memory it can allocate from, +the structure it sets up is amortized against `upper` with a potential that reads only its +footprint and is at most `Φ₀` once allocated. -/ +def Amortized (A : Allocator D w) (upper : D.State → D.Op → ℕ) (Φ₀ : ℕ) : Prop := + ∀ s (hs : A.Pre s) (hroom : Fits w (s.frontier + A.room)), ∃ Φ : State → ℕ, + (A.framed s hs hroom).Amortized charge upper Φ ∧ (A.framed s hs hroom).Local Φ ∧ + Φ ((spec w).clientState s A.alloc) ≤ Φ₀ + +section Cost + +variable {A : Allocator D w} {fD : (s : D.State) → (o : D.Op) → D.State × D.Result o} + [D.HasStepFn fD] + +/-- **The cost of a run.** A client admissible for the specification costs at most the +allocation's cost, the potential once allocated, and the upper charges of its operations. -/ +theorem run_cost {upper : D.State → D.Op → ℕ} {Φ₀ : ℕ} (hA : A.Amortized upper Φ₀) {β : Type} + (p : D.Client β) {s : State} (hs : A.Pre s) (hroom : Fits w (s.frontier + A.room)) + (hv : D.ValidHistory A.init (D.clientHistory A.init p)) : + (spec w).totalCost charge s ((spec w).clientHistory s (A.run p)) ≤ + A.cost + Φ₀ + D.totalCost upper A.init (D.clientHistory A.init p) := by + have hal := A.allocates s hs hroom + obtain ⟨Φ, hc, -, hΦ⟩ := hA s hs hroom + have h := hc.client p hal.inv (by rw [hal.abs_eq]; exact hv) + rw [hal.methods_eq, hal.abs_eq] at h + rw [clientHistory_run, StateTransitionSpec.totalCost_append, StateTransitionSpec.run_runClient] + have := hal.cost_le + omega + +/-- The cost of a run for a constant charge `K` per operation: at most the allocation's cost, +the potential once allocated, and `K` per operation. -/ +theorem run_cost_le {K Φ₀ : ℕ} (hA : A.Amortized (fun _ _ => K) Φ₀) {β : Type} + (p : D.Client β) {s : State} (hs : A.Pre s) (hroom : Fits w (s.frontier + A.room)) + (hv : D.ValidHistory A.init (D.clientHistory A.init p)) : + (spec w).totalCost charge s ((spec w).clientHistory s (A.run p)) ≤ + A.cost + Φ₀ + K * (D.clientHistory A.init p).length := by + have h := run_cost hA p hs hroom hv + rw [StateTransitionSpec.totalCost_const, Nat.mul_comm] at h + exact h + +/-- **The exported form.** For a constant charge per operation, the memory cost of a run is +`O(m)` in the number `m` of operations, over admissible clients. -/ +theorem run_cost_isBigO {K Φ₀ : ℕ} (hA : A.Amortized (fun _ _ => K) Φ₀) {β : Type} {s : State} + (hs : A.Pre s) (hroom : Fits w (s.frontier + A.room)) : + CostIsBigO Filter.atTop (fun m : ℕ => (m : ℝ)) + (fun p : {p : D.Client β // D.ValidHistory A.init (D.clientHistory A.init p)} => + (D.clientHistory A.init p.1).length) + (fun p => (spec w).totalCost charge s ((spec w).clientHistory s (A.run p.1))) := + CostIsBigO.of_le_add_mul (A.cost + Φ₀) K fun p => run_cost_le hA p.1 hs hroom p.2 + +end Cost + +/-! ## Refinements on top -/ + +/-- **A refinement on top of an allocated structure.** The same allocation sets up the +composite `Memory.Framed.comp R M`, whose methods link `R`'s methods through the structure's, +provided `R`'s invariant holds of the allocated abstract state. -/ +def comp (R : Refinement D E) (A : Allocator E w) (hinit : R.inv A.init) : Allocator D w where + Handle := A.Handle + alloc := A.alloc + methods h o := link (A.methods h) (R.methods o) + init := R.abs A.init + room := A.room + cost := A.cost + Pre := A.Pre + owned := A.owned + owned_lt := A.owned_lt + pre_fresh := A.pre_fresh + owned_fresh := A.owned_fresh + framed s hs hroom := Framed.comp R (A.framed s hs hroom) + allocates s hs hroom := + have h := A.allocates s hs hroom + { validHistory := h.validHistory + cost_le := h.cost_le + mem_eq := h.mem_eq + methods_eq := by rw [Framed.comp_methods, h.methods_eq] + inv := ⟨h.inv, by rw [h.abs_eq]; exact hinit⟩ + abs_eq := by rw [Framed.comp_abs, h.abs_eq] + of_mem_footprint := h.of_mem_footprint + room_le := h.room_le } + +/-- **Potentials stack through a refinement on top.** A certificate of `R` against the middle +charges and one of the allocator against them give a certificate of the composite, with `R`'s +potential at the allocated state added. -/ +theorem Amortized.comp {R : Refinement D E} {A : Allocator E w} {hinit : R.inv A.init} + {middle : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} {Φ : E.State → ℕ} {Ψ₀ : ℕ} + (hR : R.Amortized middle upper Φ) (hA : A.Amortized middle Ψ₀) : + (A.comp R hinit).Amortized upper (Φ A.init + Ψ₀) := by + intro s hs hroom + obtain ⟨Ψ, hc, hl, hΨ⟩ := hA s hs hroom + have hal := A.allocates s hs hroom + refine ⟨fun s' => Φ ((A.framed s hs hroom).abs s') + Ψ s', Framed.amortized_comp hR hc, + Framed.Local.add (Framed.Local.comp (Framed.Local.comp_abs _ Φ)) (Framed.Local.comp hl), ?_⟩ + change Φ ((A.framed s hs hroom).abs ((spec w).clientState s A.alloc)) + + Ψ ((spec w).clientState s A.alloc) ≤ Φ A.init + Ψ₀ + rw [hal.abs_eq] + omega + +/-! ## Products -/ + +section Prod + +variable (A₁ : Allocator D₁ w) (A₂ : Allocator D₂ w) + +/-- Allocate both structures, one after the other. -/ +def allocPair : Prog (A₁.Handle × A₂.Handle) := do + let h₁ ← A₁.alloc + let h₂ ← A₂.alloc + pure (h₁, h₂) + +/-- Both allocations' histories, one after the other. -/ +theorem clientHistory_allocPair (s : State) : + (spec w).clientHistory s (allocPair A₁ A₂) = (spec w).clientHistory s A₁.alloc ++ + (spec w).clientHistory ((spec w).clientState s A₁.alloc) A₂.alloc := by + rw [allocPair, (spec w).clientHistory_bind, (spec w).clientHistory_bind] + exact congrArg (_ ++ ·) (List.append_nil _) + +/-- The memory after both allocations. -/ +theorem clientState_allocPair (s : State) : + (spec w).clientState s (allocPair A₁ A₂) = + (spec w).clientState ((spec w).clientState s A₁.alloc) A₂.alloc := by + rw [allocPair, (spec w).clientState_bind, (spec w).clientState_bind] + rfl + +/-- Both handles. -/ +theorem clientResult_allocPair (s : State) : + (spec w).clientResult s (allocPair A₁ A₂) = + ((spec w).clientResult s A₁.alloc, + (spec w).clientResult ((spec w).clientState s A₁.alloc) A₂.alloc) := by + rw [allocPair, (spec w).clientResult_bind, (spec w).clientResult_bind] + rfl + +variable {A₁} + +/-- After allocating the first structure, room for both leaves room for the second. -/ +theorem room_after {s : State} (hs₁ : A₁.Pre s) {r : ℕ} + (hroom : Fits w (s.frontier + (A₁.room + r))) : + Fits w (((spec w).clientState s A₁.alloc).frontier + r) := + hroom.of_le (by + have := (A₁.allocates s hs₁ (hroom.of_le (by omega))).room_le + omega) + +/-- After allocating the first structure, the second one's precondition still holds. -/ +theorem pre_after {s : State} (hs₁ : A₁.Pre s) + (hroom : Fits w (s.frontier + (A₁.room + A₂.room))) (hs₂ : A₂.Pre s) : + A₂.Pre ((spec w).clientState s A₁.alloc) := + have h₁ := A₁.allocates s hs₁ (hroom.of_le (by omega)) + A₂.pre_fresh hs₂ h₁.mem_eq (fun _ => mem_clientState_of_frontier_le s _ h₁.validHistory) + (frontier_le_clientState s _) (room_after hs₁ hroom) + +/-- After allocating the first structure, the second one takes over the same cells. -/ +theorem owned_after {s : State} (hs₁ : A₁.Pre s) + (hroom : Fits w (s.frontier + (A₁.room + A₂.room))) (hs₂ : A₂.Pre s) : + A₂.owned ((spec w).clientState s A₁.alloc) = A₂.owned s := + have h₁ := A₁.allocates s hs₁ (hroom.of_le (by omega)) + A₂.owned_fresh hs₂ h₁.mem_eq (fun _ => mem_clientState_of_frontier_le s _ h₁.validHistory) + (frontier_le_clientState s _) (room_after hs₁ hroom) + +variable (A₁) + +/-- The precondition of a product of allocators: both preconditions, and the cells that the two +structures take over are disjoint. -/ +structure ProdPre (s : State) : Prop where + /-- The first allocator's precondition. -/ + left : A₁.Pre s + /-- The second allocator's precondition. -/ + right : A₂.Pre s + /-- The two structures take over disjoint cells. -/ + disjoint : Disjoint (A₁.owned s) (A₂.owned s) + +/-- **Products of allocators.** Allocate the two structures one after the other, and set up +their product over one memory. The room and the cost add, and the product takes over the cells +that either structure takes over. -/ +def prod : Allocator (product D₁ D₂) w where + Handle := A₁.Handle × A₂.Handle + alloc := allocPair A₁ A₂ + methods := fun (h₁, h₂) => Methods.prod (A₁.methods h₁) (A₂.methods h₂) + init := (A₁.init, A₂.init) + room := A₁.room + A₂.room + cost := A₁.cost + A₂.cost + Pre := ProdPre A₁ A₂ + owned s := A₁.owned s ∪ A₂.owned s + owned_lt hs ha := (Finset.mem_union.mp ha).elim (A₁.owned_lt hs.left) (A₂.owned_lt hs.right) + pre_fresh hs hmem habove hf hr := + have hr₁ := hr.of_le (Nat.add_le_add_left (Nat.le_add_right A₁.room A₂.room) _) + have hr₂ := hr.of_le (Nat.add_le_add_left (Nat.le_add_left A₂.room A₁.room) _) + { left := A₁.pre_fresh hs.left hmem habove hf hr₁ + right := A₂.pre_fresh hs.right hmem habove hf hr₂ + disjoint := by + rw [A₁.owned_fresh hs.left hmem habove hf hr₁, A₂.owned_fresh hs.right hmem habove hf hr₂] + exact hs.disjoint } + owned_fresh hs hmem habove hf hr := by + rw [A₁.owned_fresh hs.left hmem habove hf + (hr.of_le (Nat.add_le_add_left (Nat.le_add_right A₁.room A₂.room) _)), + A₂.owned_fresh hs.right hmem habove hf + (hr.of_le (Nat.add_le_add_left (Nat.le_add_left A₂.room A₁.room) _))] + framed s hs hroom := + (A₁.framed s hs.left (hroom.of_le (by omega))).prod + (A₂.framed ((spec w).clientState s A₁.alloc) (pre_after A₂ hs.left hroom hs.right) + (room_after hs.left hroom)) + allocates s hs hroom := by + -- The two allocations, from `s` to `s₁` and from `s₁` to `s₂`. + obtain ⟨hs₁, hs₂, hd⟩ := hs + have hroom₁ : Fits w (s.frontier + A₁.room) := hroom.of_le (by omega) + have h₁ := A₁.allocates s hs₁ hroom₁ + have h₂ := A₂.allocates _ (pre_after A₂ hs₁ hroom hs₂) (room_after hs₁ hroom) + have ho₂ := owned_after A₂ hs₁ hroom hs₂ + have hf₁ := frontier_le_clientState (w := w) s A₁.alloc + have hfit := h₁.room_le + have hfit₂ := h₂.room_le + -- The second footprint lies in cells taken over, which are allocated and apart from the + -- first structure's, and in cells fresh after the first allocation. + obtain ⟨hinv, habs, hfp, hr⟩ := Framed.prod_of_fresh h₁.inv h₂.mem_eq + (frontier_le_clientState _ _) h₂.inv + (Finset.disjoint_left.mpr fun a ha ha' => by + have hlt := (A₁.framed s hs₁ hroom₁).lt_frontier h₁.inv ha + rcases h₂.of_mem_footprint a ha' with ha' | ha' + · rw [ho₂] at ha' + have := A₂.owned_lt hs₂ ha' + rcases h₁.of_mem_footprint a ha with ha | ha + · exact Finset.disjoint_left.mp hd ha ha' + · omega + · omega) + (hroom.of_le (by omega)) + refine + { validHistory := ?_, cost_le := ?_, mem_eq := ?_, methods_eq := ?_, inv := ?_, + abs_eq := ?_, of_mem_footprint := ?_, room_le := ?_ } + · rw [clientHistory_allocPair, StateTransitionSpec.validHistory_append, + StateTransitionSpec.run_runClient] + exact ⟨h₁.validHistory, h₂.validHistory⟩ + · rw [clientHistory_allocPair, StateTransitionSpec.totalCost_append, + StateTransitionSpec.run_runClient] + have := h₁.cost_le + have := h₂.cost_le + omega + · intro a ha + rw [clientState_allocPair, h₂.mem_eq a (ha.trans_le hf₁), h₁.mem_eq a ha] + · rw [clientResult_allocPair, Framed.prod_methods, h₁.methods_eq, h₂.methods_eq] + · rw [clientState_allocPair] + exact hinv + · rw [clientState_allocPair, habs, h₁.abs_eq, h₂.abs_eq] + · intro a ha + rw [clientState_allocPair, hfp] at ha + rcases Finset.mem_union.mp ha with ha | ha + · exact (h₁.of_mem_footprint a ha).imp_left (Finset.mem_union_left _) + · rcases h₂.of_mem_footprint a ha with ha | ha + · rw [ho₂] at ha + exact .inl (Finset.mem_union_right _ ha) + · exact .inr (hf₁.trans ha) + · rw [clientState_allocPair, hr] + omega + +/-- The product's methods run each side's methods with its own handle. -/ +@[simp] theorem prod_methods (h₁ : A₁.Handle) (h₂ : A₂.Handle) : + (A₁.prod A₂).methods (h₁, h₂) = Methods.prod (A₁.methods h₁) (A₂.methods h₂) := rfl + +/-- The product sets up both abstract states. -/ +@[simp] theorem prod_init : (A₁.prod A₂).init = (A₁.init, A₂.init) := rfl + +/-- The product's room is the sum of the rooms. -/ +@[simp] theorem prod_room : (A₁.prod A₂).room = A₁.room + A₂.room := rfl + +/-- The product's allocation costs at most the sum of the costs. -/ +@[simp] theorem prod_cost : (A₁.prod A₂).cost = A₁.cost + A₂.cost := rfl + +/-- The product takes over the cells that either structure takes over. -/ +@[simp] theorem prod_owned (s : State) : + (A₁.prod A₂).owned s = A₁.owned s ∪ A₂.owned s := rfl + +/-- The product's precondition. -/ +theorem prod_pre_iff (s : State) : (A₁.prod A₂).Pre s ↔ ProdPre A₁ A₂ s := Iff.rfl + +variable {A₁ A₂} + +/-- **Certificates add across a product of allocators**: the charges componentwise, the +potentials once allocated by sum. -/ +theorem Amortized.prod {upper₁ : D₁.State → D₁.Op → ℕ} {upper₂ : D₂.State → D₂.Op → ℕ} + {Φ₁ Φ₂ : ℕ} (hA₁ : A₁.Amortized upper₁ Φ₁) (hA₂ : A₂.Amortized upper₂ Φ₂) : + (A₁.prod A₂).Amortized (productCharge upper₁ upper₂) (Φ₁ + Φ₂) := by + intro s hs hroom + obtain ⟨hs₁, hs₂, -⟩ := hs + have hroom₁ : Fits w (s.frontier + A₁.room) := hroom.of_le (by simp only [prod_room]; omega) + have hs₂' := pre_after A₂ hs₁ hroom hs₂ + have hroom₂ := room_after hs₁ hroom + obtain ⟨Ψ₁, hc₁, hl₁, hΨ₁⟩ := hA₁ s hs₁ hroom₁ + obtain ⟨Ψ₂, hc₂, hl₂, hΨ₂⟩ := hA₂ _ hs₂' hroom₂ + refine ⟨fun s' => Ψ₁ s' + Ψ₂ s', Framed.amortized_prod hc₁ hc₂ hl₁ hl₂, + Framed.Local.add hl₁.prod_left hl₂.prod_right, ?_⟩ + -- The first potential is unchanged by the second allocation. + have h₁ := A₁.allocates s hs₁ hroom₁ + have h₂ := A₂.allocates _ hs₂' hroom₂ + have hfit := h₁.room_le + have hfit₂ := h₂.room_le + have hkeep := hl₁ h₁.inv + (fun a ha => h₂.mem_eq a ((A₁.framed s hs₁ hroom₁).lt_frontier h₁.inv ha)) + (frontier_le_clientState _ _) (hroom.of_le (by simp only [prod_room]; omega)) + change Ψ₁ ((spec w).clientState s (allocPair A₁ A₂)) + + Ψ₂ ((spec w).clientState s (allocPair A₁ A₂)) ≤ Φ₁ + Φ₂ + rw [clientState_allocPair, hkeep] + omega + +end Prod + +/-! ## Structures already in memory -/ + +section Resident + +variable (M : Framed D w) (init : D.State) (room : ℕ) + +/-- **A structure already in memory**, such as a graph that the input holds as adjacency arrays. +Its allocation does nothing. It takes over the footprint of `M`, and needs `M` to hold, to +represent `init` and to have at most `room` cells of room. -/ +def resident : Allocator D w where + Handle := Unit + alloc := pure () + methods _ := M.methods + init := init + room := room + cost := 0 + Pre s := M.inv s ∧ M.abs s = init ∧ M.room s ≤ room + owned := M.footprint + owned_lt hs ha := M.lt_frontier hs.1 ha + pre_fresh {s _} hs hmem _ hf hr := by + obtain ⟨hinv, habs, hle⟩ := hs + obtain ⟨hinv', habs', -, hroom'⟩ := M.of_fresh hinv hmem hf (hr.of_le (by omega)) + exact ⟨hinv', habs'.trans habs, hroom' ▸ hle⟩ + owned_fresh {s _} hs hmem _ hf hr := by + obtain ⟨hinv, -, hle⟩ := hs + obtain ⟨-, -, hfp, -⟩ := M.of_fresh hinv hmem hf (hr.of_le (by omega)) + exact hfp + framed _ _ _ := M + allocates s hs _ := by + obtain ⟨hinv, habs, hle⟩ := hs + exact + { validHistory := trivial + cost_le := le_rfl + mem_eq := fun _ _ => rfl + methods_eq := rfl + inv := hinv + abs_eq := habs + of_mem_footprint := fun _ ha => .inl ha + room_le := Nat.add_le_add_left hle s.frontier } + +/-- A structure already in memory runs `M`'s methods. -/ +@[simp] theorem resident_methods (h : Unit) : (resident M init room).methods h = M.methods := rfl + +/-- It represents `init`. -/ +@[simp] theorem resident_init : (resident M init room).init = init := rfl + +/-- It takes over `M`'s footprint. -/ +@[simp] theorem resident_owned (s : State) : (resident M init room).owned s = M.footprint s := rfl + +/-- Its allocation costs nothing. -/ +@[simp] theorem resident_cost : (resident M init room).cost = 0 := rfl + +/-- Its precondition: `M` holds, represents `init` and has at most `room` cells of room. -/ +theorem resident_pre_iff (s : State) : + (resident M init room).Pre s ↔ M.inv s ∧ M.abs s = init ∧ M.room s ≤ room := Iff.rfl + +variable {M init room} + +/-- **The certificate of a structure already in memory** is the structure's own: a potential +that reads only its footprint and is at most `Φ₀` wherever the structure represents `init`. -/ +theorem Amortized.resident {upper : D.State → D.Op → ℕ} {Φ : State → ℕ} {Φ₀ : ℕ} + (hc : M.Amortized charge upper Φ) (hl : M.Local Φ) + (hΦ : ∀ s, M.inv s → M.abs s = init → Φ s ≤ Φ₀) : + (resident M init room).Amortized upper Φ₀ := fun s hs _ => by + obtain ⟨hinv, habs, -⟩ := hs + exact ⟨Φ, hc, hl, hΦ s hinv habs⟩ + +end Resident + +end Allocator + +end Cslib.DataStructure.Memory diff --git a/Complexity/DataStructure/Memory/Frame.lean b/Complexity/DataStructure/Memory/Frame.lean index 9c41b35613..9992941dbc 100644 --- a/Complexity/DataStructure/Memory/Frame.lean +++ b/Complexity/DataStructure/Memory/Frame.lean @@ -11,54 +11,66 @@ public import Complexity.DataStructure.Memory.Spec public import Complexity.DataStructure.StateTransition.Refinement /-! -# Footprints, and products of data structures sharing one memory - -A `Memory.Framed D w` is a refinement of `D` over `Memory.spec w` together with a footprint: the -finite set of allocated cells that holds the representation of each memory state. Three -obligations make the footprint honest. - -* `congr`: the invariant, the abstraction and the footprint itself read only the footprint's - cells, and survive a growing frontier. -* `modifies`: a method run changes no allocated cell outside the footprint, and the footprint - grows only into cells that the run allocated. +# Footprints, room, and products of data structures sharing one memory + +A `Memory.Framed D w` is a refinement of `D` over `Memory.spec w` together with a footprint, the +finite set of allocated cells that holds the representation of each memory state, and a room, +the number of cells the structure has reserved for its future allocations. Three obligations make +them honest. + +* `congr`: the invariant, the abstraction, the footprint and the room read only the footprint's + cells, and survive a growing frontier that leaves the reserved room fitting a word. +* `modifies`: a method run changes no allocated cell outside the footprint, the footprint grows + only into cells that the run allocated, and the frontier advances by at most the room the run + gives up. * `lt_frontier`: the footprint is allocated. -Footprints may change from state to state, so that a structure can grow into cells it allocates -inside its operations. A structure laid out in fixed blocks has a constant footprint, and -`Framed.ofStatic` asks for less. Allocating inside an operation also needs room, since -`Memory.valid` asks the new frontier to fit a word. Neither the abstract state nor the structure's -own cells determine the frontier, and the other side of a product moves it, so such a structure -needs a shared budget of room, which this file does not provide. The structures built so far -allocate their storage once, up front. - -Two framed refinements implement the product of their specifications over one shared memory, -as long as their footprints are disjoint (`Framed.prod`). Disjointness is part of the product's -invariant. It holds after each method run because a run of one side writes only its own cells -and fresh ones, and the other side's footprint is allocated, hence not fresh. The product is -framed again, with the union of the footprints, so products iterate: -`(M₁.prod M₂).prod M₃` implements three structures in one memory. A potential that reads only the -footprint (`Framed.Local`) is left unchanged by the other side's methods, so amortized +A structure laid out in fixed blocks has a constant footprint and no room, and `Framed.ofStatic` +asks for less. A structure that allocates inside its operations, such as a growing array, +reserves room for all of its future growth. Its invariant may then ask that the frontier plus its +room fit a word, which is what `Memory.valid` needs of each allocation. That fact is not +preserved by other structures' allocations on its own, so the product keeps it for everybody. + +**Products.** Two framed refinements implement the product of their specifications over one +shared memory (`Framed.prod`). The product's invariant asks that the footprints be disjoint and +that the frontier plus both rooms fit a word. This is the shared room budget: a method run of one +side writes only its own cells and fresh ones, and advances the frontier by at most the room it +gives up, so the other side keeps its cells and its room, and the budget still fits. The product +is framed again, with the union of the footprints and the sum of the rooms, so products iterate: +`(M₁.prod M₂).prod M₃` implements three structures in one memory. A potential that reads only +the footprint (`Framed.Local`) is left unchanged by the other side's methods, so amortized certificates add across the product (`Framed.amortized_prod`), and so do worst-case `Module.ChargeBound`s, as the case of zero potentials. -Allocation is a memory program like any other. A run that leaves every allocated cell unchanged, -such as the allocation of a further structure, preserves a framed refinement (`Framed.of_fresh`), -and `Framed.prod_of_fresh` sets up a product from structures allocated one after the other. +**Composition.** A refinement of `D` over `E` composed with a framed refinement of `E` is framed +by the same footprint and room (`Framed.comp`), since a whole linked client keeps the frame of its +calls (`Framed.modifies_demonic`). So a structure built on others, such as a queue over two +stacks, joins a product like any other. + +**Allocation** is a memory program like any other. A run that leaves every allocated cell +unchanged and leaves the room fitting, such as the allocation of a further structure, preserves a +framed refinement (`Framed.of_fresh`), and `Framed.prod_of_fresh` sets up a product from +structures allocated one after the other. `Memory.Allocator` packages this. ## Main definitions -* `Memory.Framed`: a refinement over memory with a footprint. -* `Memory.Framed.ofStatic`: the constructor for a constant footprint. +* `Memory.Framed`: a refinement over memory with a footprint and a room. +* `Memory.Framed.ofStatic`: the constructor for a constant footprint and no room. * `Memory.Framed.Local`: a function of memory that reads only the footprint. * `Memory.Framed.prod`: two framed refinements with disjoint footprints implement the product. +* `Memory.Framed.comp`: a refinement over a framed refinement is framed. ## Main results -* `Memory.frontier_le_of_clientRun`: a run never lowers the frontier. +* `Memory.frontier_le_of_clientRun`, `Memory.frontier_le_clientState`: a run never lowers the + frontier. * `Memory.mem_run_of_lt_frontier`, `Memory.mem_clientState_of_lt_frontier`: a run changes an allocated cell only by writing it. +* `Memory.mem_run_of_frontier_le`, `Memory.mem_clientState_of_frontier_le`: an admissible run + changes no cell at or above its final frontier. +* `Memory.Framed.modifies_demonic`: a linked client keeps the frame of its calls. * `Memory.Framed.frame`: a method run of one structure leaves a structure with a disjoint - footprint unchanged. + footprint unchanged, and the shared room budget fitting. * `Memory.Framed.prod_methods`: the product's methods are the two sides' methods. * `Memory.Framed.amortized_prod`: potentials and charges add across the product. * `Memory.Framed.of_fresh`, `Memory.Framed.prod_of_fresh`: allocation preserves structures and @@ -75,6 +87,8 @@ explicit finite footprints as in `Cslib.WordRAM.HeapAssertion`; see namespace Cslib.DataStructure.Memory +open Cslib.WordRAM + variable {w : ℕ} /-! ## Runs and allocated cells -/ @@ -87,6 +101,12 @@ theorem frontier_le_of_clientRun {α : Type} {s s' : State} {p : Prog α} {a : rw [← (spec w).run_runClient] exact frontier_le_run s _ +/-- No memory program lowers the frontier. -/ +theorem frontier_le_clientState {α : Type} (s : State) (p : Prog α) : + s.frontier ≤ ((spec w).clientState s p).frontier := by + rw [← (spec w).run_runClient] + exact frontier_le_run s _ + /-- A sequence of operations changes an allocated cell only by writing it. -/ theorem mem_run_of_lt_frontier (s : State) (os : List Op) {a : ℕ} (ha : a < s.frontier) (hw : ∀ v, Op.write a v ∉ os) : ((spec w).run s os).1.mem a = s.mem a := by @@ -105,76 +125,219 @@ theorem mem_clientState_of_lt_frontier {α : Type} (s : State) (p : Prog α) {a rw [← (spec w).run_runClient] exact mem_run_of_lt_frontier s _ ha hw +/-- An admissible sequence of operations changes no cell at or above its final frontier: writes +go below the frontier, and an allocation clears only the block that it hands out. -/ +theorem mem_run_of_frontier_le {s : State} {os : List Op} (hv : (spec w).ValidHistory s os) + {a : ℕ} (ha : ((spec w).run s os).1.frontier ≤ a) : ((spec w).run s os).1.mem a = s.mem a := by + induction os generalizing s with + | nil => rfl + | cons o os ih => + obtain ⟨hvo, hvs⟩ := hv + change ((spec w).run (step s o).1 os).1.frontier ≤ a at ha + change ((spec w).run (step s o).1 os).1.mem a = s.mem a + rw [ih hvs ha] + have hf : (step s o).1.frontier ≤ a := (frontier_le_run _ os).trans ha + cases o with + | read => rfl + | write b v => + have hb : b < s.frontier := hvo.1 + simp only [step_write] at hf + have hab : a ≠ b := by omega + exact Function.update_of_ne hab v s.mem + | alloc k => + simp only [step_alloc] at hf + exact clear_of_not_owns (by simp only [Block.Owns]; omega) + | allocDirty => rfl + +/-- An admissible memory program changes no cell at or above its final frontier. -/ +theorem mem_clientState_of_frontier_le {α : Type} (s : State) (p : Prog α) + (hv : (spec w).ValidHistory s ((spec w).clientHistory s p)) {a : ℕ} + (ha : ((spec w).clientState s p).frontier ≤ a) : + ((spec w).clientState s p).mem a = s.mem a := by + rw [← (spec w).run_runClient] at ha ⊢ + exact mem_run_of_frontier_le hv ha + /-! ## Framed refinements -/ -/-- A refinement of `D` over memory whose representation lives in a footprint of allocated -cells. The invariant, the abstraction and the footprint read only the footprint's cells; a -method run changes no allocated cell outside the footprint; and the footprint grows only into -cells at or above the old frontier, which the run allocated. -/ +/-- A refinement of `D` over memory whose representation lives in a footprint of allocated cells, +with room reserved for its growth. The invariant, the abstraction, the footprint and the room +read only the footprint's cells; a method run changes no allocated cell outside the footprint; +the footprint grows only into cells at or above the old frontier, which the run allocated; and +the frontier advances by at most the room the run gives up. -/ structure Framed (D : StateTransitionSpec.{0, 0, 0}) (w : ℕ) extends Refinement D (spec w) where /-- The cells holding the representation. -/ footprint : State → Finset ℕ + /-- The cells reserved for the structure's future allocations. -/ + room : State → ℕ /-- The footprint is allocated. -/ lt_frontier : ∀ {s a}, inv s → a ∈ footprint s → a < s.frontier - /-- The invariant, the abstraction and the footprint read only the footprint's cells, and - survive a growing frontier. -/ + /-- The invariant, the abstraction, the footprint and the room read only the footprint's + cells, and survive a growing frontier that leaves the room fitting a word. -/ congr : ∀ {s s'}, inv s → (∀ a ∈ footprint s, s'.mem a = s.mem a) → - s.frontier ≤ s'.frontier → inv s' ∧ abs s' = abs s ∧ footprint s' = footprint s - /-- A method run changes no allocated cell outside the footprint, and the footprint grows - only into fresh cells. -/ + s.frontier ≤ s'.frontier → Fits w (s'.frontier + room s) → + inv s' ∧ abs s' = abs s ∧ footprint s' = footprint s ∧ room s' = room s + /-- A method run changes no allocated cell outside the footprint, the footprint grows only + into fresh cells, and the frontier advances by at most the room given up. -/ modifies : ∀ {s} o {a s' tr}, inv s → D.valid (abs s) o → (spec w).ClientRun s (methods o) a s' tr → (∀ b < s.frontier, b ∉ footprint s → s'.mem b = s.mem b) ∧ - ∀ b ∈ footprint s', b ∈ footprint s ∨ s.frontier ≤ b + (∀ b ∈ footprint s', b ∈ footprint s ∨ s.frontier ≤ b) ∧ + s'.frontier + room s' ≤ s.frontier + room s namespace Framed -variable {D D₁ D₂ : StateTransitionSpec.{0, 0, 0}} +variable {D D₁ D₂ E : StateTransitionSpec.{0, 0, 0}} -/-- The constructor for a constant footprint `fp`: the invariant and abstraction read only `fp`, -and each method's final state agrees with its initial state on the allocated cells outside -`fp`. -/ +/-- The constructor for a constant footprint `fp` and no room: the invariant and abstraction read +only `fp`, and each method's final state agrees with its initial state on the allocated cells +outside `fp` and has the same frontier. -/ def ofStatic (M : Refinement D (spec w)) (fp : Finset ℕ) (lt_frontier : ∀ {s a}, M.inv s → a ∈ fp → a < s.frontier) (congr : ∀ {s s'}, M.inv s → (∀ a ∈ fp, s'.mem a = s.mem a) → s.frontier ≤ s'.frontier → M.inv s' ∧ M.abs s' = M.abs s) (modifies : ∀ {s} o, M.inv s → D.valid (M.abs s) o → ∀ b < s.frontier, b ∉ fp → - ((spec w).clientState s (M.methods o)).mem b = s.mem b) : + ((spec w).clientState s (M.methods o)).mem b = s.mem b) + (frontier_eq : ∀ {s} o, M.inv s → D.valid (M.abs s) o → + ((spec w).clientState s (M.methods o)).frontier = s.frontier) : Framed D w where toRefinement := M footprint _ := fp + room _ := 0 lt_frontier := lt_frontier - congr hs h hf := ⟨(congr hs h hf).1, (congr hs h hf).2, rfl⟩ + congr hs h hf _ := ⟨(congr hs h hf).1, (congr hs h hf).2, rfl, rfl⟩ modifies {s} o {a s' tr} hs hv hrun := by obtain ⟨_, _, rfl, _⟩ := ((spec w).clientRun_iff_runClient _ _ _ _ _).mp hrun - exact ⟨modifies o hs hv, fun b hb => .inl hb⟩ + exact ⟨modifies o hs hv, fun b hb => .inl hb, (frontier_eq o hs hv).le⟩ variable (M : Framed D w) /-- A function of memory reads only the footprint: it is unchanged when the footprint's cells -are and the frontier grows. The abstraction is one (`Local.abs`); so are potentials that a -product must keep apart. -/ +are and the frontier grows, leaving the room fitting a word. The abstraction is one +(`Local.abs`), and so is the room (`Local.room`); so are potentials that a product must keep +apart. -/ def Local {β : Type*} (f : State → β) : Prop := ∀ {s s'}, M.inv s → (∀ a ∈ M.footprint s, s'.mem a = s.mem a) → - s.frontier ≤ s'.frontier → f s' = f s + s.frontier ≤ s'.frontier → Fits w (s'.frontier + M.room s) → f s' = f s /-- The abstraction reads only the footprint. -/ -theorem Local.abs : M.Local M.abs := fun hs h hf => (M.congr hs h hf).2.1 +theorem Local.abs : M.Local M.abs := fun hs h hf hr => by + obtain ⟨-, habs, -⟩ := M.congr hs h hf hr + exact habs + +/-- The room reads only the footprint. -/ +theorem Local.room : M.Local M.room := fun hs h hf hr => by + obtain ⟨-, -, -, hroom⟩ := M.congr hs h hf hr + exact hroom /-- A constant reads no cell. -/ -theorem Local.const {β : Type*} (b : β) : M.Local fun _ => b := fun _ _ _ => rfl +theorem Local.const {β : Type*} (b : β) : M.Local fun _ => b := fun _ _ _ _ => rfl /-- Sums of local functions are local. -/ -theorem Local.add {f g : State → ℕ} (hf : M.Local f) (hg : M.Local g) : - M.Local fun s => f s + g s := fun hs h hfr => - congrArg₂ (· + ·) (hf hs h hfr) (hg hs h hfr) +theorem Local.add {M : Framed D w} {f g : State → ℕ} (hf : M.Local f) (hg : M.Local g) : + M.Local fun s => f s + g s := fun hs h hfr hr => + congrArg₂ (· + ·) (hf hs h hfr hr) (hg hs h hfr hr) -/-- A run that leaves every allocated cell unchanged preserves a framed refinement. Allocating -another structure is such a run. -/ +/-- A function of the abstract state is local. -/ +theorem Local.comp_abs {β : Type*} (f : D.State → β) : M.Local fun s => f (M.abs s) := + fun hs h hfr hr => congrArg f (Local.abs M hs h hfr hr) + +/-- A run that leaves every allocated cell unchanged and leaves the room fitting preserves a +framed refinement. Allocating another structure is such a run. -/ theorem of_fresh {s s' : State} (hs : M.inv s) - (hmem : ∀ a < s.frontier, s'.mem a = s.mem a) (hf : s.frontier ≤ s'.frontier) : - M.inv s' ∧ M.abs s' = M.abs s ∧ M.footprint s' = M.footprint s := - M.congr hs (fun a ha => hmem a (M.lt_frontier hs ha)) hf + (hmem : ∀ a < s.frontier, s'.mem a = s.mem a) (hf : s.frontier ≤ s'.frontier) + (hroom : Fits w (s'.frontier + M.room s)) : + M.inv s' ∧ M.abs s' = M.abs s ∧ M.footprint s' = M.footprint s ∧ M.room s' = M.room s := + M.congr hs (fun a ha => hmem a (M.lt_frontier hs ha)) hf hroom + +/-- **The frame of a client.** A run of a linked admissible client changes no cell outside the +footprint that was allocated before it, grows the footprint only into fresh cells, and advances +the frontier by at most the room it gives up, as each method run does. -/ +theorem modifies_demonic {α : Type} (p : D.Client α) {s s' : State} {a : α} + {tr : (spec w).Transcript} (hs : M.inv s) (hv : D.DemonicValid (M.abs s) p) + (hrun : (spec w).ClientRun s (link M.methods p) a s' tr) : + (∀ b < s.frontier, b ∉ M.footprint s → s'.mem b = s.mem b) ∧ + (∀ b ∈ M.footprint s', b ∈ M.footprint s ∨ s.frontier ≤ b) ∧ + s'.frontier + M.room s' ≤ s.frontier + M.room s := by + induction p generalizing s tr with + | pure b => + obtain ⟨-, rfl, -⟩ := ((spec w).clientRun_pure_iff _ _ _ _ _).mp hrun + exact ⟨fun _ _ _ => rfl, fun _ hb => .inl hb, le_rfl⟩ + | liftBind o k ih => + obtain ⟨hv_o, hv_k⟩ := (D.demonicValid_liftBind_iff _ o k).mp hv + have heq : link M.methods (.liftBind o k) = + (M.methods o).bind (fun r => link M.methods (k r)) := rfl + rw [heq] at hrun + obtain ⟨r, s₁, tr₁, tr₂, hrun₁, hrun₂, rfl⟩ := (spec w).clientRun_bind_iff.mp hrun + obtain ⟨hstep, hs₁⟩ := M.correct o hs hv_o hrun₁ + obtain ⟨hmod₁, hgrow₁, hroom₁⟩ := M.modifies o hs hv_o hrun₁ + obtain ⟨hmod₂, hgrow₂, hroom₂⟩ := ih r hs₁ (hv_k _ r hstep) hrun₂ + have hf₁ := frontier_le_of_clientRun hrun₁ + refine ⟨fun b hb hb' => ?_, fun b hb => ?_, by omega⟩ + · have hb₁ : b ∉ M.footprint s₁ := fun h => + (hgrow₁ b h).elim hb' fun h' => absurd hb (Nat.not_lt.mpr h') + rw [hmod₂ b (hb.trans_le hf₁) hb₁, hmod₁ b hb hb'] + · rcases hgrow₂ b hb with h | h + · exact hgrow₁ b h + · exact .inr (hf₁.trans h) + +/-! ## Composition -/ + +/-- **A refinement over a framed refinement is framed**, by the same footprint and room: the +upper invariant and abstraction read the lower state only through its abstraction, and each +upper method is a linked client of the lower methods. -/ +def comp (R : Refinement D E) (M : Framed E w) : Framed D w where + toRefinement := R.comp M.toRefinement + footprint := M.footprint + room := M.room + lt_frontier hs ha := M.lt_frontier hs.1 ha + congr {s _} hs h hf hr := by + obtain ⟨hM, hR⟩ := hs + obtain ⟨hM', habs, hfp, hroom⟩ := M.congr hM h hf hr + refine ⟨⟨hM', ?_⟩, ?_, hfp, hroom⟩ + · rwa [habs] + · change R.abs (M.abs _) = R.abs (M.abs s) + rw [habs] + modifies {_} o {_ _ _} hs hv hrun := + M.modifies_demonic (R.methods o) hs.1 (R.valid o hs.2 hv) hrun + +/-- The composite's methods link the upper methods through the lower ones. -/ +theorem comp_methods (R : Refinement D E) (M : Framed E w) : + (comp R M).methods = fun o => link M.methods (R.methods o) := rfl + +/-- The composite is the composition of the refinements. -/ +theorem comp_toRefinement (R : Refinement D E) (M : Framed E w) : + (comp R M).toRefinement = R.comp M.toRefinement := rfl + +/-- The composite's invariant: the lower invariant, and the upper invariant of the lower +abstraction. -/ +theorem comp_inv_iff (R : Refinement D E) (M : Framed E w) (s : State) : + (comp R M).inv s ↔ M.inv s ∧ R.inv (M.abs s) := Iff.rfl + +/-- The composite represents a memory state by the upper abstraction of the lower one. -/ +@[simp] theorem comp_abs (R : Refinement D E) (M : Framed E w) (s : State) : + (comp R M).abs s = R.abs (M.abs s) := rfl + +/-- The composite's footprint is the lower footprint. -/ +@[simp] theorem comp_footprint (R : Refinement D E) (M : Framed E w) (s : State) : + (comp R M).footprint s = M.footprint s := rfl + +/-- The composite's room is the lower room. -/ +@[simp] theorem comp_room (R : Refinement D E) (M : Framed E w) (s : State) : + (comp R M).room s = M.room s := rfl + +/-- A function local to the lower framed refinement is local to the composite. -/ +theorem Local.comp {R : Refinement D E} {M : Framed E w} {β : Type*} {f : State → β} + (hf : M.Local f) : (comp R M).Local f := fun hs h hfr hr => hf hs.1 h hfr hr + +/-- **Potentials stack across composition** with a framed refinement, as for refinements +(`Refinement.Amortized.comp`). -/ +theorem amortized_comp {R : Refinement D E} {M : Framed E w} {lower : State → Op → ℕ} + {middle : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} {Φ : E.State → ℕ} + {Ψ : State → ℕ} (A : R.Amortized middle upper Φ) (B : M.Amortized lower middle Ψ) : + (comp R M).Amortized lower upper fun s => Φ (M.abs s) + Ψ s := + A.comp B + +/-! ## Frames of disjoint structures -/ variable {M} (N : Framed D₂ w) @@ -186,96 +349,122 @@ theorem agree_of_run {s : State} (o : D.Op) {a : D.Result o} {s' : State} ∀ b ∈ N.footprint s, s'.mem b = s.mem b := fun b hb => (M.modifies o hM hv hrun).1 b (N.lt_frontier hN hb) (Finset.disjoint_right.mp hd hb) +/-- A method run of `M` leaves room for `N` when both rooms fitted before. -/ +theorem room_of_run {s : State} (o : D.Op) {a : D.Result o} {s' : State} + {tr : (spec w).Transcript} (hM : M.inv s) (hv : D.valid (M.abs s) o) + (hrun : (spec w).ClientRun s (M.methods o) a s' tr) {r : ℕ} + (hroom : Fits w (s.frontier + (M.room s + r))) : Fits w (s'.frontier + (M.room s' + r)) := + hroom.of_le (by obtain ⟨-, -, h⟩ := M.modifies o hM hv hrun; omega) + /-- **The frame of a framed refinement.** A method run of `M` leaves a framed refinement with a -disjoint footprint unchanged, and the footprints stay disjoint. -/ +disjoint footprint unchanged, and the footprints disjoint and the shared room budget fitting. -/ theorem frame {s : State} (o : D.Op) {a : D.Result o} {s' : State} {tr : (spec w).Transcript} (hM : M.inv s) (hN : N.inv s) - (hd : Disjoint (M.footprint s) (N.footprint s)) (hv : D.valid (M.abs s) o) + (hd : Disjoint (M.footprint s) (N.footprint s)) + (hroom : Fits w (s.frontier + (M.room s + N.room s))) (hv : D.valid (M.abs s) o) (hrun : (spec w).ClientRun s (M.methods o) a s' tr) : - N.abs s' = N.abs s ∧ N.inv s' ∧ N.footprint s' = N.footprint s ∧ - Disjoint (M.footprint s') (N.footprint s') := by + N.abs s' = N.abs s ∧ N.inv s' ∧ N.footprint s' = N.footprint s ∧ N.room s' = N.room s ∧ + Disjoint (M.footprint s') (N.footprint s') ∧ + Fits w (s'.frontier + (M.room s' + N.room s')) := by have hf := frontier_le_of_clientRun hrun - obtain ⟨hN', habs, hfp⟩ := N.congr hN (agree_of_run N o hM hN hd hv hrun) hf - refine ⟨habs, hN', hfp, Finset.disjoint_left.mpr fun b hb hb' => ?_⟩ + have hroom' := room_of_run o hM hv hrun hroom + obtain ⟨hN', habs, hfp, hr⟩ := N.congr hN (agree_of_run N o hM hN hd hv hrun) hf + (hroom'.of_le (by omega)) + refine ⟨habs, hN', hfp, hr, Finset.disjoint_left.mpr fun b hb hb' => ?_, hr ▸ hroom'⟩ rw [hfp] at hb' - rcases (M.modifies o hM hv hrun).2 b hb with hb | hb + obtain ⟨-, hgrow, -⟩ := M.modifies o hM hv hrun + rcases hgrow b hb with hb | hb · exact Finset.disjoint_left.mp hd hb hb' · exact absurd (N.lt_frontier hN hb') (Nat.not_lt.mpr hb) /-- A method run of `M` leaves unchanged every function that reads only a disjoint footprint. -/ theorem Local.frame {β : Type*} {f : State → β} (hf : N.Local f) {s : State} (o : D.Op) {a : D.Result o} {s' : State} {tr : (spec w).Transcript} (hM : M.inv s) (hN : N.inv s) - (hd : Disjoint (M.footprint s) (N.footprint s)) (hv : D.valid (M.abs s) o) + (hd : Disjoint (M.footprint s) (N.footprint s)) + (hroom : Fits w (s.frontier + (M.room s + N.room s))) (hv : D.valid (M.abs s) o) (hrun : (spec w).ClientRun s (M.methods o) a s' tr) : f s' = f s := hf hN (agree_of_run N o hM hN hd hv hrun) (frontier_le_of_clientRun hrun) + ((room_of_run o hM hv hrun hroom).of_le (by omega)) /-! ## Products -/ variable (M₁ : Framed D₁ w) (M₂ : Framed D₂ w) -/-- A method run of the left side keeps the right side and the disjointness of the footprints. -/ +/-- What keeps two framed refinements apart in one memory: disjoint footprints, and room for +both. -/ +def Apart (s : State) : Prop := + Disjoint (M₁.footprint s) (M₂.footprint s) ∧ Fits w (s.frontier + (M₁.room s + M₂.room s)) + +/-- A method run of the left side keeps the right side and keeps the two apart. -/ theorem prod_frame_left {s : State} (o : D₁.Op) {a : D₁.Result o} {s' : State} - {tr : (spec w).Transcript} (h₁ : M₁.inv s) (h₂ : M₂.inv s) - (hd : Disjoint (M₁.footprint s) (M₂.footprint s)) (hv : D₁.valid (M₁.abs s) o) - (hrun : (spec w).ClientRun s (M₁.methods o) a s' tr) : - M₂.abs s' = M₂.abs s ∧ M₂.inv s' ∧ Disjoint (M₁.footprint s') (M₂.footprint s') := - have h := frame M₂ o h₁ h₂ hd hv hrun - ⟨h.1, h.2.1, h.2.2.2⟩ - -/-- A method run of the right side keeps the left side and the disjointness of the footprints. -/ + {tr : (spec w).Transcript} (h₁ : M₁.inv s) (h₂ : M₂.inv s) (hJ : Apart M₁ M₂ s) + (hv : D₁.valid (M₁.abs s) o) (hrun : (spec w).ClientRun s (M₁.methods o) a s' tr) : + M₂.abs s' = M₂.abs s ∧ M₂.inv s' ∧ Apart M₁ M₂ s' := by + obtain ⟨habs, hinv, -, -, hapart⟩ := frame M₂ o h₁ h₂ hJ.1 hJ.2 hv hrun + exact ⟨habs, hinv, hapart⟩ + +/-- A method run of the right side keeps the left side and keeps the two apart. -/ theorem prod_frame_right {s : State} (o : D₂.Op) {a : D₂.Result o} {s' : State} - {tr : (spec w).Transcript} (h₁ : M₁.inv s) (h₂ : M₂.inv s) - (hd : Disjoint (M₁.footprint s) (M₂.footprint s)) (hv : D₂.valid (M₂.abs s) o) - (hrun : (spec w).ClientRun s (M₂.methods o) a s' tr) : - M₁.abs s' = M₁.abs s ∧ M₁.inv s' ∧ Disjoint (M₁.footprint s') (M₂.footprint s') := - have h := frame M₁ o h₂ h₁ hd.symm hv hrun - ⟨h.1, h.2.1, h.2.2.2.symm⟩ + {tr : (spec w).Transcript} (h₁ : M₁.inv s) (h₂ : M₂.inv s) (hJ : Apart M₁ M₂ s) + (hv : D₂.valid (M₂.abs s) o) (hrun : (spec w).ClientRun s (M₂.methods o) a s' tr) : + M₁.abs s' = M₁.abs s ∧ M₁.inv s' ∧ Apart M₁ M₂ s' := by + obtain ⟨habs, hinv, -, -, hd, hroom⟩ := + frame M₁ o h₂ h₁ hJ.1.symm (by rw [Nat.add_comm (M₂.room s)]; exact hJ.2) hv hrun + exact ⟨habs, hinv, hd.symm, by rw [Nat.add_comm (M₁.room s')]; exact hroom⟩ /-- **Products over one memory.** Two framed refinements implement the product of their -specifications over one memory, with the union of their footprints, while the footprints are -disjoint. Disjointness is part of the product's invariant. -/ +specifications over one memory, with the union of their footprints and the sum of their rooms, +while they are apart: their footprints are disjoint and the frontier plus both rooms fits a word. +Being apart is part of the product's invariant. -/ def prod : Framed (product D₁ D₂) w where - toRefinement := M₁.toRefinement.prod M₂.toRefinement - (fun s => Disjoint (M₁.footprint s) (M₂.footprint s)) + toRefinement := M₁.toRefinement.prod M₂.toRefinement (Apart M₁ M₂) (prod_frame_left M₁ M₂) (prod_frame_right M₁ M₂) footprint s := M₁.footprint s ∪ M₂.footprint s + room s := M₁.room s + M₂.room s lt_frontier {_ _} hs ha := by + obtain ⟨h₁, h₂, -⟩ := hs rcases Finset.mem_union.mp ha with ha | ha - · exact M₁.lt_frontier hs.1 ha - · exact M₂.lt_frontier hs.2.1 ha - congr {_ _} hs h hf := by - obtain ⟨h₁, h₂, hd⟩ := hs - obtain ⟨h₁', habs₁, hfp₁⟩ := M₁.congr h₁ (fun a ha => h a (Finset.mem_union_left _ ha)) hf - obtain ⟨h₂', habs₂, hfp₂⟩ := M₂.congr h₂ (fun a ha => h a (Finset.mem_union_right _ ha)) hf - refine ⟨⟨h₁', h₂', ?_⟩, ?_, ?_⟩ - · change Disjoint (M₁.footprint _) (M₂.footprint _) - rwa [hfp₁, hfp₂] + · exact M₁.lt_frontier h₁ ha + · exact M₂.lt_frontier h₂ ha + congr {_ _} hs h hf hr := by + obtain ⟨h₁, h₂, hd, -⟩ := hs + obtain ⟨h₁', habs₁, hfp₁, hr₁⟩ := M₁.congr h₁ + (fun a ha => h a (Finset.mem_union_left _ ha)) hf (hr.of_le (by omega)) + obtain ⟨h₂', habs₂, hfp₂, hr₂⟩ := M₂.congr h₂ + (fun a ha => h a (Finset.mem_union_right _ ha)) hf (hr.of_le (by omega)) + refine ⟨⟨h₁', h₂', ?_, ?_⟩, ?_, ?_, ?_⟩ + · rwa [hfp₁, hfp₂] + · rwa [hr₁, hr₂] · change (M₁.abs _, M₂.abs _) = (M₁.abs _, M₂.abs _) rw [habs₁, habs₂] · rw [hfp₁, hfp₂] + · rw [hr₁, hr₂] modifies {s} o {a s' tr} hs hv hrun := by - obtain ⟨h₁, h₂, hd⟩ := hs + obtain ⟨h₁, h₂, hd, hroom⟩ := hs cases o with | inl o => - obtain ⟨hmod, hgrow⟩ := M₁.modifies o h₁ hv hrun - obtain ⟨-, -, hfp₂, -⟩ := frame M₂ o h₁ h₂ hd hv hrun + obtain ⟨hmod, hgrow, hr⟩ := M₁.modifies o h₁ hv hrun + obtain ⟨-, -, hfp₂, hr₂, -⟩ := frame M₂ o h₁ h₂ hd hroom hv hrun refine ⟨fun b hb hb' => hmod b hb fun h => hb' (Finset.mem_union_left _ h), - fun b hb => ?_⟩ - change b ∈ M₁.footprint s' ∪ M₂.footprint s' at hb - rw [hfp₂] at hb - rcases Finset.mem_union.mp hb with hb | hb - · exact (hgrow b hb).imp_left (Finset.mem_union_left _) - · exact .inl (Finset.mem_union_right _ hb) + fun b hb => ?_, ?_⟩ + · change b ∈ M₁.footprint s' ∪ M₂.footprint s' at hb + rw [hfp₂] at hb + rcases Finset.mem_union.mp hb with hb | hb + · exact (hgrow b hb).imp_left (Finset.mem_union_left _) + · exact .inl (Finset.mem_union_right _ hb) + · omega | inr o => - obtain ⟨hmod, hgrow⟩ := M₂.modifies o h₂ hv hrun - obtain ⟨-, -, hfp₁, -⟩ := frame M₁ o h₂ h₁ hd.symm hv hrun + obtain ⟨hmod, hgrow, hr⟩ := M₂.modifies o h₂ hv hrun + obtain ⟨-, -, hfp₁, hr₁, -⟩ := frame M₁ o h₂ h₁ hd.symm + (by rw [Nat.add_comm (M₂.room s)]; exact hroom) hv hrun refine ⟨fun b hb hb' => hmod b hb fun h => hb' (Finset.mem_union_right _ h), - fun b hb => ?_⟩ - change b ∈ M₁.footprint s' ∪ M₂.footprint s' at hb - rw [hfp₁] at hb - rcases Finset.mem_union.mp hb with hb | hb - · exact .inl (Finset.mem_union_left _ hb) - · exact (hgrow b hb).imp_left (Finset.mem_union_right _) + fun b hb => ?_, ?_⟩ + · change b ∈ M₁.footprint s' ∪ M₂.footprint s' at hb + rw [hfp₁] at hb + rcases Finset.mem_union.mp hb with hb | hb + · exact .inl (Finset.mem_union_left _ hb) + · exact (hgrow b hb).imp_left (Finset.mem_union_right _) + · omega /-- The product's methods run each side's methods. They do not depend on the proofs. -/ theorem prod_methods : (M₁.prod M₂).methods = Methods.prod M₁.methods M₂.methods := rfl @@ -283,26 +472,30 @@ theorem prod_methods : (M₁.prod M₂).methods = Methods.prod M₁.methods M₂ /-- The product represents each side by its own abstraction. -/ @[simp] theorem prod_abs (s : State) : (M₁.prod M₂).abs s = (M₁.abs s, M₂.abs s) := rfl -/-- The product's invariant: both sides' invariants, and disjoint footprints. -/ +/-- The product's invariant: both sides' invariants, and the two sides apart. -/ theorem prod_inv_iff (s : State) : - (M₁.prod M₂).inv s ↔ - M₁.inv s ∧ M₂.inv s ∧ Disjoint (M₁.footprint s) (M₂.footprint s) := Iff.rfl + (M₁.prod M₂).inv s ↔ M₁.inv s ∧ M₂.inv s ∧ Apart M₁ M₂ s := Iff.rfl /-- The product's footprint is the union of the footprints. -/ @[simp] theorem prod_footprint (s : State) : (M₁.prod M₂).footprint s = M₁.footprint s ∪ M₂.footprint s := rfl +/-- The product's room is the sum of the rooms. -/ +@[simp] theorem prod_room (s : State) : (M₁.prod M₂).room s = M₁.room s + M₂.room s := rfl + variable {M₁ M₂} /-- A function local to the left side is local to the product. -/ theorem Local.prod_left {β : Type*} {f : State → β} (hf : M₁.Local f) : - (M₁.prod M₂).Local f := fun hs h hfr => - hf hs.1 (fun a ha => h a (Finset.mem_union_left _ ha)) hfr + (M₁.prod M₂).Local f := fun ⟨h₁, _, _⟩ h hfr hr => + hf h₁ (fun a ha => h a (Finset.mem_union_left _ ha)) hfr + (hr.of_le (Nat.add_le_add_left (Nat.le_add_right _ _) _)) /-- A function local to the right side is local to the product. -/ theorem Local.prod_right {β : Type*} {f : State → β} (hf : M₂.Local f) : - (M₁.prod M₂).Local f := fun hs h hfr => - hf hs.2.1 (fun a ha => h a (Finset.mem_union_right _ ha)) hfr + (M₁.prod M₂).Local f := fun ⟨_, h₂, _⟩ h hfr hr => + hf h₂ (fun a ha => h a (Finset.mem_union_right _ ha)) hfr + (hr.of_le (Nat.add_le_add_left (Nat.le_add_left _ _) _)) /-- **Potentials add across a product over one memory.** Certificates of the two sides against one lower charge, with potentials that read only their own footprints, give a certificate of @@ -313,21 +506,25 @@ theorem amortized_prod {lower : State → Op → ℕ} {upper₁ : D₁.State → (hΦ₁ : M₁.Local Φ₁) (hΦ₂ : M₂.Local Φ₂) : (M₁.prod M₂).Amortized lower (productCharge upper₁ upper₂) fun s => Φ₁ s + Φ₂ s := Refinement.Amortized.prod (frame₁ := prod_frame_left M₁ M₂) (frame₂ := prod_frame_right M₁ M₂) - A₁ A₂ (fun {_} o {_ _ _} h₁ h₂ hd hv hrun => hΦ₂.frame M₂ o h₁ h₂ hd hv hrun) - (fun {_} o {_ _ _} h₁ h₂ hd hv hrun => hΦ₁.frame M₁ o h₂ h₁ hd.symm hv hrun) + A₁ A₂ (fun {_} o {_ _ _} h₁ h₂ hJ hv hrun => hΦ₂.frame M₂ o h₁ h₂ hJ.1 hJ.2 hv hrun) + (fun {_} o {_ _ _} h₁ h₂ hJ hv hrun => hΦ₁.frame M₁ o h₂ h₁ hJ.1.symm + (by rw [Nat.add_comm (M₂.room _)]; exact hJ.2) hv hrun) /-- Setting up a product from structures allocated one after the other: `M₁` holds at `s`; a -run from `s` to `s'` leaves the cells below `s.frontier` unchanged; and `M₂` holds at `s'` on a -footprint at or above `s.frontier`. Then the product holds at `s'`, with `M₁`'s abstraction +run from `s` to `s'` leaves the cells below `s.frontier` unchanged; `M₂` holds at `s'` on a +footprint disjoint from `M₁`'s, such as one at or above `s.frontier`; and the frontier plus both +rooms fits. Then the product holds at `s'`, with `M₁`'s abstraction, footprint and room unchanged. -/ theorem prod_of_fresh {s s' : State} (h₁ : M₁.inv s) (hmem : ∀ a < s.frontier, s'.mem a = s.mem a) (hf : s.frontier ≤ s'.frontier) - (h₂ : M₂.inv s') (hfp : ∀ a ∈ M₂.footprint s', s.frontier ≤ a) : - (M₁.prod M₂).inv s' ∧ (M₁.prod M₂).abs s' = (M₁.abs s, M₂.abs s') := by - obtain ⟨h₁', habs, hfp₁⟩ := M₁.of_fresh h₁ hmem hf - refine ⟨⟨h₁', h₂, Finset.disjoint_left.mpr fun a ha ha' => ?_⟩, by rw [prod_abs, habs]⟩ - rw [hfp₁] at ha - exact absurd (M₁.lt_frontier h₁ ha) (Nat.not_lt.mpr (hfp a ha')) + (h₂ : M₂.inv s') (hd : Disjoint (M₁.footprint s) (M₂.footprint s')) + (hroom : Fits w (s'.frontier + (M₁.room s + M₂.room s'))) : + (M₁.prod M₂).inv s' ∧ (M₁.prod M₂).abs s' = (M₁.abs s, M₂.abs s') ∧ + (M₁.prod M₂).footprint s' = M₁.footprint s ∪ M₂.footprint s' ∧ + (M₁.prod M₂).room s' = M₁.room s + M₂.room s' := by + obtain ⟨h₁', habs, hfp₁, hr₁⟩ := M₁.of_fresh h₁ hmem hf (hroom.of_le (by omega)) + exact ⟨⟨h₁', h₂, by rwa [hfp₁], by rwa [hr₁]⟩, by rw [prod_abs, habs], + by rw [prod_footprint, hfp₁], by rw [prod_room, hr₁]⟩ end Framed diff --git a/Complexity/DataStructure/PriorityQueue/BinaryHeap/Memory.lean b/Complexity/DataStructure/PriorityQueue/BinaryHeap/Memory.lean index 0cb6b26d3e..82a58259e1 100644 --- a/Complexity/DataStructure/PriorityQueue/BinaryHeap/Memory.lean +++ b/Complexity/DataStructure/PriorityQueue/BinaryHeap/Memory.lean @@ -722,6 +722,13 @@ theorem methods_frame (hL : L.Valid w K) {s : Memory.State} (hs : Inv L s) obtain ⟨-, -, -, -, -, h⟩ := methods_run hL hs o hv exact h +/-- An operation leaves the frontier where it was. -/ +theorem methods_frontier (hL : L.Valid w K) {s : Memory.State} (hs : Inv L s) + (o : IndexedMinPQ.Op n) (hv : IndexedMinPQ.valid K (abs L s) o) : + ((Memory.spec w).clientState s (ops L o)).frontier = s.frontier := by + obtain ⟨-, -, -, -, h, -⟩ := methods_run hL hs o hv + exact h + /-! ## The refinement and its frame -/ /-- The binary heap implements the indexed min-priority queue with keys at most `K`. -/ @@ -764,6 +771,7 @@ def framed (hL : L.Valid w K) : Memory.Framed (indexedMinPQSpec n K) w := .ofStatic (refinement hL) L.footprint (fun hs ha => hs.lt_frontier hL ha) (fun hs h hf => ⟨hs.congr hL h hf, abs_congr h⟩) (fun o hs hv b _ hb => methods_frame hL hs o hv b hb) + (fun o hs hv => methods_frontier hL hs o hv) /-- The footprint of a heap is its layout's cells. -/ @[simp] theorem framed_footprint (hL : L.Valid w K) (s : Memory.State) : diff --git a/Complexity/DataStructure/Queue/Memory.lean b/Complexity/DataStructure/Queue/Memory.lean index 89acafde8b..e3845a1645 100644 --- a/Complexity/DataStructure/Queue/Memory.lean +++ b/Complexity/DataStructure/Queue/Memory.lean @@ -22,16 +22,18 @@ proved once: (`Queue.potential_step`); only the capacity and word-fit admissibility of the bounded stacks is new. Each queue operation costs at most three stack calls, amortized, with two credits per rear element. -2. `pair`: two array stacks with disjoint layouts in one memory, as the generic product - `Memory.Framed.prod` of two framed stacks, each stack call costing at most three memory +2. Two array stacks allocated one after the other, as the generic product + `Memory.Allocator.prod` of two stack allocators, each stack call costing at most three memory units. -`memRefinement` composes them, and `mem_amortized` stacks the potentials across the composition -(`Refinement.Amortized.comp`): every queue operation costs at most nine memory units, amortized, -with six credits per rear element. `run` allocates the two stacks and then runs a queue client. -From any memory with room for both stacks, `run_correct` gives its answer and the admissibility of -its memory operations, `run_cost` bounds its memory cost by `6 + 9 m` for `m` queue operations, -and `run_cost_isBigO` exports that bound as `O(m)`. +`allocator` puts the first step on top of the second (`Memory.Allocator.comp`), and +`amortized_allocator` stacks the potentials across the composition: every queue operation costs +at most nine memory units, amortized, with six credits per rear element. `run` allocates the two +stacks and then runs a queue client. From any memory with room for both stacks, `run_correct` +gives its answer and the admissibility of its memory operations, `run_cost` bounds its memory +cost by `6 + 9 m` for `m` queue operations, and `run_cost_isBigO` exports that bound as `O(m)`. +All three are instances of the generic theorems of `Memory.Allocator`, so this file has no setup +proof of its own. The machine-level counterpart is `Queue.WordRAM`, whose dispatcher is hand-stepped instruction by instruction. Here the proofs mention neither registers nor instructions. Executing the memory @@ -43,16 +45,15 @@ provide. * `boundedStacks`: the pair of bounded stacks. * `Inv`: a FIFO list within capacity holding words. * `refinement`: the two-stack queue over the pair of bounded stacks. -* `pair`: the two stacks in one memory. -* `memRefinement`, `memMethods`: the queue over two array stacks over memory, and its methods as - plain memory programs. +* `allocator`: the queue over two array stacks, allocated in memory. * `run`: allocate the stacks, then run a queue client. ## Main results * `runClient_boundedStacks`: bounded stacks run clients exactly as unbounded ones. * `amortized`: three stack calls per queue operation, with two credits per rear element. -* `mem_amortized`: nine memory units per queue operation, with six credits per rear element. +* `amortized_allocator`: nine memory units per queue operation, with six credits per rear + element. * `run_correct`, `run_cost`: the allocated queue answers like the specification and costs at most `6 + 9 m` memory units for `m` queue operations. * `run_cost_glue`: with glue charged per memory operation, at most `(2 K + 1) (6 + 9 m)`. @@ -191,100 +192,37 @@ theorem amortized : /-! ## Over memory -/ -/-- The two stacks over one memory, in disjoint layouts. -/ -abbrev pair {L₁ L₂ : Stack.Memory.Layout} (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) : - Memory.Framed (boundedStacks w C) w := - (Stack.Memory.framed h₁).prod (Stack.Memory.framed h₂) +/-- The queue over two array stacks of capacity `C`: allocate the stacks one after the other, +and run the two-stack queue on their product. -/ +def allocator (w C : ℕ) : Allocator (Queue.WordRAM.spec w C) w := + ((Stack.Memory.allocator w C).prod (Stack.Memory.allocator w C)).comp (refinement w C) + (show Inv w C [] from ⟨Nat.zero_le C, fun _ h => absurd h List.not_mem_nil⟩) -/-- The queue over two array stacks over memory. -/ -def memRefinement {L₁ L₂ : Stack.Memory.Layout} (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) : - Refinement (Queue.WordRAM.spec w C) (Memory.spec w) := - (refinement w C).comp (pair h₁ h₂).toRefinement +/-- The allocated queue is empty. -/ +@[simp] theorem init_allocator : (allocator w C).init = [] := rfl + +/-- The two stacks take `2 (C + 1)` cells. -/ +@[simp] theorem room_allocator : (allocator w C).room = 2 * (C + 1) := by + change (C + 1) + (C + 1) = _ + omega + +/-- The two stacks are allocated from scratch, so the allocation needs nothing of the memory +besides room. -/ +theorem pre_allocator (s : Memory.State) : (allocator w C).Pre s := + ⟨trivial, trivial, Finset.disjoint_empty_left _⟩ /-- **Stacked potentials.** Every queue operation costs at most nine memory units, amortized, with six credits per element of the rear stack: the queue's potential, at three memory units per -stack call, read through the stacks' abstraction. -/ -theorem mem_amortized {L₁ L₂ : Stack.Memory.Layout} (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) : - (memRefinement h₁ h₂).Amortized charge (fun _ _ => 9) - fun s => 6 * (Stack.Memory.abs L₂ s).length := by - have hpair := Memory.Framed.amortized_prod (Stack.Memory.amortized h₁) - (Stack.Memory.amortized h₂) (Memory.Framed.Local.const _ 0) (Memory.Framed.Local.const _ 0) +stack call, read through the stacks' abstraction. Allocation leaves no potential. -/ +theorem amortized_allocator : (allocator w C).Amortized (fun _ _ => 9) 0 := by + have hpair := (Stack.Memory.amortized_allocator (w := w) (C := C)).prod + (Stack.Memory.amortized_allocator (w := w) (C := C)) rw [productCharge_const] at hpair - have h := (amortized.mul_left 3).comp hpair - have hΦ : (fun s : Memory.State => - 3 * (2 * (Stack.Memory.abs L₂ s).length) + (0 + 0)) = - fun s => 6 * (Stack.Memory.abs L₂ s).length := by - funext s - omega - exact hΦ ▸ h - -/-! ## Allocation and a whole run -/ - -/-- The queue methods over two array stacks, as plain memory programs. -/ -def memMethods (L₁ L₂ : Stack.Memory.Layout) (w C : ℕ) : - Methods (Queue.WordRAM.spec w C) (Memory.spec w) := - fun o => link (Methods.prod (Stack.Memory.methods L₁ w C) (Stack.Memory.methods L₂ w C)) - (methods o) - -/-- The composite's methods are `memMethods`, whatever the proofs about the layouts. -/ -theorem memRefinement_methods {L₁ L₂ : Stack.Memory.Layout} (h₁ : L₁.Valid w C) - (h₂ : L₂.Valid w C) : (memRefinement h₁ h₂).methods = memMethods L₁ L₂ w C := rfl + exact Allocator.Amortized.comp (amortized.mul_left 3) hpair /-- Allocate two empty stacks of capacity `C`, then run a queue client on them. -/ -def run (w C : ℕ) {β : Type} (p : (Queue.WordRAM.spec w C).Client β) : Prog β := do - let L₁ ← Stack.Memory.allocLayout C - let L₂ ← Stack.Memory.allocLayout C - link (memMethods L₁ L₂ w C) p - -/-- The first stack allocated from `s`. -/ -abbrev frontLayout (s : Memory.State) (C : ℕ) : Stack.Memory.Layout := - ⟨⟨s.frontier, 1⟩, ⟨s.frontier + 1, C⟩⟩ - -/-- The second stack allocated from `s`. -/ -abbrev rearLayout (s : Memory.State) (C : ℕ) : Stack.Memory.Layout := - ⟨⟨s.frontier + 1 + C, 1⟩, ⟨s.frontier + 1 + C + 1, C⟩⟩ - -/-- The memory after both allocations. -/ -abbrev allocated (s : Memory.State) (C : ℕ) : Memory.State := - ⟨clear (clear s.mem s.frontier 1) (s.frontier + 1 + C) 1, s.frontier + 1 + C + 1 + C⟩ - -/-- A run allocates both stacks, then runs the linked client from the allocated memory. -/ -theorem runClient_run {β : Type} (p : (Queue.WordRAM.spec w C).Client β) (s : Memory.State) : - (Memory.spec w).runClient s (run w C p) = - let (v, s', os) := (Memory.spec w).runClient (allocated s C) - (link (memMethods (frontLayout s C) (rearLayout s C) w C) p) - (v, s', .alloc 1 :: .allocDirty C :: .alloc 1 :: .allocDirty C :: os) := rfl - -/-- The facts that start the refinement after allocation. -/ -private theorem setup (s : Memory.State) (hfit : Fits w (s.frontier + 2 * (C + 1))) : - ∃ (h₁ : (frontLayout s C).Valid w C) (h₂ : (rearLayout s C).Valid w C), - (memRefinement h₁ h₂).inv (allocated s C) ∧ - (memRefinement h₁ h₂).abs (allocated s C) = [] ∧ - Stack.Memory.abs (rearLayout s C) (allocated s C) = [] := by - have h₁ : (frontLayout s C).Valid w C := Stack.Memory.valid_allocLayout (hfit.of_le (by omega)) - have h₂ : (rearLayout s C).Valid w C := Stack.Memory.valid_allocLayout (hfit.of_le (by omega)) - -- Each stack is empty once allocated, the second one from the state after the first. - obtain ⟨hi₁, ha₁⟩ := Stack.Memory.inv_allocLayout (C := C) s - obtain ⟨hi₂, ha₂⟩ := Stack.Memory.inv_allocLayout (C := C) - ⟨clear s.mem s.frontier 1, s.frontier + 1 + C⟩ - -- The second allocation is fresh, so the stacks form a product. - obtain ⟨hinv, habs⟩ := Memory.Framed.prod_of_fresh (M₁ := Stack.Memory.framed h₁) - (M₂ := Stack.Memory.framed h₂) hi₁ - (fun a ha => clear_of_not_owns (by simp only [Block.Owns] at ha ⊢; omega)) (by simp only; omega) - hi₂ - (fun a ha => by - simp only [Stack.Memory.framed_footprint, Stack.Memory.Layout.footprint, Finset.mem_union, - Block.mem_footprint, Block.Owns] at ha - simp only - omega) - have hempty : (pair h₁ h₂).abs (allocated s C) = ([], []) := habs.trans (Prod.ext ha₁ ha₂) - refine ⟨h₁, h₂, ⟨hinv, ?_⟩, ?_, ha₂⟩ - · change Inv w C (Queue.WordRAM.contents ((pair h₁ h₂).abs (allocated s C))) - rw [hempty] - exact ⟨by simp [Queue.WordRAM.contents], by simp [Queue.WordRAM.contents]⟩ - · change Queue.WordRAM.contents ((pair h₁ h₂).abs (allocated s C)) = [] - rw [hempty] - rfl +def run (w C : ℕ) {β : Type} (p : (Queue.WordRAM.spec w C).Client β) : Prog β := + (allocator w C).run p /-- **Correctness.** From any memory with room for both stacks, an admissible queue client run over two freshly allocated array stacks issues only admissible memory operations and returns the @@ -293,17 +231,9 @@ theorem run_correct {β : Type} (p : (Queue.WordRAM.spec w C).Client β) {s : Me (hfit : Fits w (s.frontier + 2 * (C + 1))) (hv : (Queue.WordRAM.spec w C).ValidHistory [] ((Queue.WordRAM.spec w C).clientHistory [] p)) : (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (run w C p)) ∧ - (Memory.spec w).clientResult s (run w C p) = (Queue.WordRAM.spec w C).clientResult [] p := by - obtain ⟨h₁, h₂, hinv, habs, -⟩ := setup s hfit - obtain ⟨hvE, hres, -, -⟩ := - (memRefinement h₁ h₂).simulates_client p hinv (by rw [habs]; exact hv) - rw [memRefinement_methods] at hvE hres - simp only [StateTransitionSpec.clientHistory, StateTransitionSpec.clientResult, - runClient_run] at hvE hres ⊢ - simp only [StateTransitionSpec.validHistory_cons, StateTransitionSpec.stepFn, step_alloc, - step_allocDirty, valid_alloc, valid_allocDirty] - refine ⟨⟨hfit.of_le (by omega), hfit.of_le (by omega), hfit.of_le (by omega), - hfit.of_le (by omega), hvE⟩, hres.trans (by rw [habs])⟩ + (Memory.spec w).clientResult s (run w C p) = (Queue.WordRAM.spec w C).clientResult [] p := + have ⟨hvE, hres, _⟩ := (allocator w C).run_correct p (pre_allocator s) (room_allocator ▸ hfit) hv + ⟨hvE, hres⟩ /-- **Cost.** The same run costs at most `6 + 9 m` memory units for a client of `m` queue operations: six for the two allocations and nine per operation, amortized. -/ @@ -311,15 +241,8 @@ theorem run_cost {β : Type} (p : (Queue.WordRAM.spec w C).Client β) {s : Memor (hfit : Fits w (s.frontier + 2 * (C + 1))) (hv : (Queue.WordRAM.spec w C).ValidHistory [] ((Queue.WordRAM.spec w C).clientHistory [] p)) : (Memory.spec w).totalCost charge s ((Memory.spec w).clientHistory s (run w C p)) ≤ - 6 + 9 * ((Queue.WordRAM.spec w C).clientHistory [] p).length := by - obtain ⟨h₁, h₂, hinv, habs, hrear⟩ := setup s hfit - have h := (mem_amortized h₁ h₂).client p hinv (by rw [habs]; exact hv) - rw [memRefinement_methods, habs, StateTransitionSpec.totalCost_const, hrear] at h - simp only [StateTransitionSpec.clientHistory, runClient_run, - StateTransitionSpec.totalCost_cons, charge_alloc, charge_allocDirty, - StateTransitionSpec.stepFn, step_alloc, step_allocDirty] at h ⊢ - simp only [List.length_nil, Nat.mul_zero, Nat.add_zero, allocated] at h ⊢ - omega + 6 + 9 * ((Queue.WordRAM.spec w C).clientHistory [] p).length := + Allocator.run_cost_le amortized_allocator p (pre_allocator s) (room_allocator ▸ hfit) hv /-- **Cost with glue.** A realization also charges the glue that runs after each memory operation. If that glue costs at most `K` times the operation's charge plus `K`, the run costs at most @@ -345,6 +268,6 @@ theorem run_cost_isBigO (s : Memory.State) (hfit : Fits w (s.frontier + 2 * (C + ((Queue.WordRAM.spec w C).clientHistory [] p.1).length) (fun p => (Memory.spec w).totalCost charge s ((Memory.spec w).clientHistory s (run w C p.1))) := - CostIsBigO.of_le_add_mul 6 9 fun p => run_cost p.1 hfit p.2 + Allocator.run_cost_isBigO amortized_allocator (pre_allocator s) (room_allocator ▸ hfit) end Cslib.DataStructure.Queue.Memory diff --git a/Complexity/DataStructure/Stack/Memory.lean b/Complexity/DataStructure/Stack/Memory.lean index 5fb09e09e6..4db5ea5025 100644 --- a/Complexity/DataStructure/Stack/Memory.lean +++ b/Complexity/DataStructure/Stack/Memory.lean @@ -8,7 +8,7 @@ module -- upstream: candidate public import Complexity.DataStructure.Memory.Field -public import Complexity.DataStructure.Memory.Frame +public import Complexity.DataStructure.Memory.Alloc public import Complexity.DataStructure.Stack.WordRAM.Basic /-! @@ -25,7 +25,8 @@ Every operation costs at most three memory units, with no potential (`amortized` write only the layout's cells and never allocate (`modifies_methods`), and the abstraction and invariant depend only on those cells (`abs_congr`, `Inv.congr`). So the stack is framed by its layout (`framed`), and stacks with disjoint layouts share one memory through the generic product -`Memory.Framed.prod`. +`Memory.Framed.prod`. `allocator` packages the allocation of an empty stack (`allocLayout`) with +the framed stack it sets up, so that clients allocate stacks through `Memory.Allocator`. This is the same specification that `Stack.WordRAM` implements by a hand-stepped nine-register dispatcher. Here no register or instruction count appears. Word fit enters only through the @@ -40,6 +41,7 @@ admissibility of `Memory.spec w` and one static fact of the layout, that the cap * `refinement`: the array stack as a `Refinement` of the bounded stack. * `framed`: the same refinement, framed by the layout's cells. * `allocLayout`: allocate an empty stack. +* `allocator`: allocation and the framed stack, as a `Memory.Allocator`. ## Main results @@ -47,8 +49,9 @@ admissibility of `Memory.spec w` and one static fact of the layout, that the cap * `runClient_push`, `runClient_pop_of_eq_zero`, `runClient_pop_of_pos`, `runClient_size`: the operations evaluate definitionally. * `modifies_methods`, `abs_congr`, `Inv.congr`, `Inv.lt_frontier`: the frame of a stack. -* `runClient_allocLayout_bind`, `valid_allocLayout`, `inv_allocLayout`: allocation yields a - well-formed empty stack in three memory units. +* `runClient_allocLayout_bind`, `runClient_allocLayout`, `valid_allocLayout`, + `inv_allocLayout`: allocation yields a well-formed empty stack in three memory units. +* `amortized_allocator`: the allocator's cost certificate, three units per operation. ## References @@ -318,6 +321,7 @@ def framed (hL : L.Valid w C) : Memory.Framed (Stack.WordRAM.spec w C) w := .ofStatic (refinement hL) L.footprint (fun hs ha => Inv.lt_frontier hs ha) (fun hs h hf => ⟨hs.congr hL h hf, abs_congr hL hs h⟩) (fun o _ hv b _ hb => (modifies_methods hL o hv).1 b hb) + (fun o _ hv => (modifies_methods hL o hv).2) /-- Every operation costs at most three memory units, so the stack needs no potential. -/ theorem amortized (hL : L.Valid w C) : @@ -385,4 +389,51 @@ theorem inv_allocLayout (s : Memory.State) : exact Nat.zero_le C · simp [abs, h0] +/-- Allocation returns the layout at the frontier, clears the count cell, and advances the +frontier past the items. -/ +theorem runClient_allocLayout (C : ℕ) (s : Memory.State) : + (Memory.spec w).runClient s (allocLayout C) = + (⟨⟨s.frontier, 1⟩, ⟨s.frontier + 1, C⟩⟩, ⟨clear s.mem s.frontier 1, s.frontier + 1 + C⟩, + [.alloc 1, .allocDirty C]) := rfl + +/-- **The array stack as an allocator**: allocate an empty stack of capacity `C` in `C + 1` +cells, at a memory cost of three units. -/ +def allocator (w C : ℕ) : Allocator (Stack.WordRAM.spec w C) w where + Handle := Layout + alloc := allocLayout C + methods L := methods L w C + init := [] + room := C + 1 + cost := 3 + framed s _ hroom := framed (valid_allocLayout (f := s.frontier) (hroom.of_le (by omega))) + allocates s _ hroom := by + obtain ⟨hinv, habs⟩ := inv_allocLayout (C := C) s + refine + { validHistory := ?_, cost_le := ?_, mem_eq := ?_, methods_eq := rfl, inv := ?_, + abs_eq := ?_, of_mem_footprint := ?_, room_le := ?_ } <;> + simp only [StateTransitionSpec.clientHistory, StateTransitionSpec.clientState, + runClient_allocLayout] + · simp only [StateTransitionSpec.validHistory_cons, StateTransitionSpec.stepFn, step_alloc, + valid_alloc, valid_allocDirty] + exact ⟨hroom.of_le (by omega), hroom.of_le (by omega), trivial⟩ + · simp + · exact fun a ha => clear_of_not_owns (by simp only [Block.Owns]; omega) + · exact hinv + · exact habs + · intro a ha + simp only [framed_footprint, Layout.footprint, Finset.mem_union, Block.mem_footprint, + Block.Owns] at ha + right + omega + · simp only [framed, Memory.Framed.ofStatic] + omega + +/-- The allocated stack is empty. -/ +@[simp] theorem init_allocator (w C : ℕ) : (allocator w C).init = [] := rfl + +/-- Every stack operation costs at most three memory units, and allocation leaves no +potential. -/ +theorem amortized_allocator : (allocator w C).Amortized (fun _ _ => 3) 0 := + fun _ _ _ => ⟨fun _ => 0, amortized _, Memory.Framed.Local.const _ 0, le_rfl⟩ + end Cslib.DataStructure.Stack.Memory diff --git a/Complexity/DataStructure/StateTransition.lean b/Complexity/DataStructure/StateTransition.lean index 623ad75564..032f4dac9f 100644 --- a/Complexity/DataStructure/StateTransition.lean +++ b/Complexity/DataStructure/StateTransition.lean @@ -71,8 +71,10 @@ The relational semantics is **demonic** for callers and **angelic** for implemen under `[StateTransitionSpec.HasStepFn]`. * `StateTransitionSpec.fst_run_eq_toFLTS_mtr`, `StateTransitionSpec.run_append`, `StateTransitionSpec.validHistory_append`, `StateTransitionSpec.totalCost_append`, - `StateTransitionSpec.run_runClient`, `StateTransitionSpec.runClient_bind`, `eval_bind`, - `eval_eq_liftM`: functional history and client laws under `[StateTransitionSpec.HasStepFn]`. + `StateTransitionSpec.run_runClient`, `StateTransitionSpec.runClient_bind`, + `StateTransitionSpec.clientResult_bind`, `StateTransitionSpec.clientState_bind`, + `StateTransitionSpec.clientHistory_bind`, `eval_bind`, `eval_eq_liftM`: functional history and + client laws under `[StateTransitionSpec.HasStepFn]`. ## References @@ -870,6 +872,26 @@ theorem runClient_bind (p : D.Client α) (k : α → D.Client β) (s : D.State) exact congrArg (fun r : β × D.State × List D.Op => (r.1, r.2.1, o :: r.2.2)) (ih (D.stepFn s o).2 (D.stepFn s o).1) +/-- A sequential client answers as its continuation, run from where the first client stopped. -/ +theorem clientResult_bind (p : D.Client α) (k : α → D.Client β) (s : D.State) : + D.clientResult s (p >>= k) = D.clientResult (D.clientState s p) (k (D.clientResult s p)) := by + change D.clientResult s (p.bind k) = _ + rw [clientResult, runClient_bind] + +/-- A sequential client stops where its continuation, run from where the first client stopped, +stops. -/ +theorem clientState_bind (p : D.Client α) (k : α → D.Client β) (s : D.State) : + D.clientState s (p >>= k) = D.clientState (D.clientState s p) (k (D.clientResult s p)) := by + change D.clientState s (p.bind k) = _ + rw [clientState, runClient_bind] + +/-- The history of a sequential client is the first client's history, then its continuation's. -/ +theorem clientHistory_bind (p : D.Client α) (k : α → D.Client β) (s : D.State) : + D.clientHistory s (p >>= k) = + D.clientHistory s p ++ D.clientHistory (D.clientState s p) (k (D.clientResult s p)) := by + change D.clientHistory s (p.bind k) = _ + rw [clientHistory, runClient_bind] + /-- On a deterministic specification (`[D.HasStepFn f]`), demonic operation-sequence admissibility `ValidOpSeq` coincides with `D.ValidHistory`. -/ @[simp] diff --git a/ComplexityTests/DataStructureMemoryAlloc.lean b/ComplexityTests/DataStructureMemoryAlloc.lean new file mode 100644 index 0000000000..292ff6f507 --- /dev/null +++ b/ComplexityTests/DataStructureMemoryAlloc.lean @@ -0,0 +1,592 @@ +/- +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.Stack.Memory + +/-! +# Allocation inside operations, and structures already in memory + +Two checks of the allocator contract of `Memory.Allocator`, at word size `8`. + +**Room consumed inside operations.** A write-once cell reserves one cell of room when it is +allocated, and allocates that cell inside its first `set`. Its header is taken without clearing, +so its allocator needs the memory beyond the frontier to be zero, which the other cell's +allocation keeps. Two such cells share one memory as `cells`, the product of their allocators. +A client sets them alternately, so each `set` allocates above the other structure's newest cell. +The tests check: + +* the answers and the admissibility of the whole run, by the generic `Allocator.run_correct`; +* the allocations inside the operations, in the run's memory history; +* after each step, the footprints, the abstractions and the frontier plus the remaining room, + which stays at the frontier the allocation reserved up to; +* the boundary: from frontier `251`, where `251 + 4` fits a byte, the run is admissible. From + `252` it is not, and only the right `set` fails: its allocation, of the last of the four + reserved cells, would leave the frontier at `256`; +* that the precondition is needed: over a nonzero cell, an unset cell reads as set. + +**Structures already in memory.** A stack that the input holds is taken over by +`Allocator.resident`, in the shape of Dijkstra's algorithm: two stacks are allocated from +scratch above the input, and the input's stack is used in place. The generic theorems give the +run's answer and cost. Two stacks that the input holds in disjoint cells combine too. Taking +over the same cells twice is excluded by the product's precondition. +-/ + +@[expose] public section + +namespace ComplexityTests.DataStructureMemoryAlloc + +open Cslib.WordRAM Cslib.DataStructure Cslib.DataStructure.Memory + +/-! ## A write-once cell that allocates on its first `set` -/ + +/-- The operations of a write-once cell: set it once, and get its value. -/ +inductive CellOp where + /-- Set the cell to a value. -/ + | set (v : ℕ) + /-- Get the value, if set. -/ + | get + deriving DecidableEq + +/-- Setting answers nothing; getting answers the value, if set. -/ +abbrev CellOp.Result : CellOp → Type + | .set _ => Unit + | .get => Option ℕ + +/-- Setting stores the value, and getting returns it. -/ +def cellStep (c : Option ℕ) : (o : CellOp) → Option ℕ × o.Result + | .set v => (some v, ()) + | .get => (c, c) + +/-- A cell is set once, to a word. -/ +def cellValid (w : ℕ) (c : Option ℕ) : CellOp → Prop + | .set v => c = none ∧ Fits w v + | .get => True + +instance (w : ℕ) (c : Option ℕ) (o : CellOp) : Decidable (cellValid w c o) := by + cases o <;> unfold cellValid <;> infer_instance + +/-- The write-once cell at word size `w`. -/ +abbrev Cell (w : ℕ) : StateTransitionSpec := + StateTransitionSpec.ofFn (State := Option ℕ) (Op := CellOp) (Result := CellOp.Result) cellStep + (cellValid w) + +/-- Admissibility of a concrete history of cell operations is decidable. -/ +instance (w : ℕ) (c : Option ℕ) (os : List CellOp) : Decidable ((Cell w).ValidHistory c os) := by + induction os generalizing c with + | nil => exact isTrue trivial + | cons o os ih => + exact decidable_of_iff (cellValid w c o ∧ (Cell w).ValidHistory (cellStep c o).1 os) Iff.rfl + +variable (h w : ℕ) + +/-- Set: allocate the value cell, write the value there, and point the header `h` at it. -/ +def cellSet (v : ℕ) : Prog Unit := do + let p ← allocDirty 1 + write p v + write h p + +/-- Get: a zero header means unset; otherwise read the cell that it points to. -/ +def cellGet : Prog (Option ℕ) := do + let p ← read h + if p = 0 then pure none else do + let v ← read p + pure (some v) + +/-- The cell's operations as memory programs, with header `h`. -/ +def cellMethods : Methods (Cell w) (spec w) + | .set v => cellSet h v + | .get => cellGet h + +/-- The value cell, if the header points to one. -/ +def cellAbs (s : State) : Option ℕ := if s.mem h = 0 then none else some (s.mem (s.mem h)) + +/-- The header, and the value cell once set. -/ +def cellFootprint (s : State) : Finset ℕ := if s.mem h = 0 then {h} else {h, s.mem h} + +/-- One cell of room until the cell is set. -/ +def cellRoom (s : State) : ℕ := if s.mem h = 0 then 1 else 0 + +/-- The header and the value cell are allocated, and the frontier plus the room fits a word, so +that the first `set` may allocate. -/ +structure CellInv (s : State) : Prop where + /-- The header is allocated. -/ + header_lt : h < s.frontier + /-- The value cell is allocated. -/ + value_lt : s.mem h ≠ 0 → s.mem h < s.frontier + /-- The reserved cell fits. -/ + fits_room : Fits w (s.frontier + cellRoom h s) + +/-- A set allocates one cell at the frontier, writes the value there and points the header at +it. -/ +theorem runClient_cellSet (s : State) (v : ℕ) : + (spec w).runClient s (cellSet h v) = + ((), ⟨Function.update (Function.update s.mem s.frontier v) h s.frontier, s.frontier + 1⟩, + [.allocDirty 1, .write s.frontier v, .write h s.frontier]) := rfl + +/-- A get of an unset cell reads the header. -/ +theorem runClient_cellGet_of_eq_zero (s : State) (h0 : s.mem h = 0) : + (spec w).runClient s (cellGet h) = (none, s, [.read h]) := by + simp [cellGet, h0] + +/-- A get of a set cell reads the header and the value cell. -/ +theorem runClient_cellGet_of_ne_zero (s : State) (h0 : s.mem h ≠ 0) : + (spec w).runClient s (cellGet h) = (some (s.mem (s.mem h)), s, [.read h, .read (s.mem h)]) := by + unfold cellGet + simp only [StateTransitionSpec.runClient_lift_bind', StateTransitionSpec.stepFn, step_read, h0, + ↓reduceIte] + rfl + +/-- Allocating a header takes one cell at the frontier, without clearing it. -/ +theorem runClient_allocDirty_one (s : State) : + (spec w).runClient s (allocDirty 1) = (s.frontier, ⟨s.mem, s.frontier + 1⟩, [.allocDirty 1]) := + rfl + +variable {h w} + +/-- A cell is unset exactly when its header is zero. -/ +theorem cellAbs_eq_none {s : State} : cellAbs h s = none ↔ s.mem h = 0 := by + unfold cellAbs + split <;> simp_all + +variable (h w) + +/-- The write-once cell with header `h` implements its specification. -/ +def cellRefinement : Refinement (Cell w) (spec w) := + Refinement.ofFn (cellMethods h w) (CellInv h w) (cellAbs h) + (by + intro s o hs hv + have hh := CellInv.header_lt hs + cases o with + | set v => + obtain ⟨hnone, hfit⟩ := hv + have h0 := cellAbs_eq_none.mp hnone + have hr := CellInv.fits_room hs + simp only [cellRoom, h0, ↓reduceIte] at hr + simp only [cellMethods, StateTransitionSpec.clientHistory, runClient_cellSet, + StateTransitionSpec.validHistory_cons, StateTransitionSpec.stepFn, step_allocDirty, + step_write, valid_allocDirty, valid_write] + exact ⟨hr, ⟨Nat.lt_add_one _, hfit⟩, ⟨by omega, hr.of_le (by omega)⟩, trivial⟩ + | get => + by_cases h0 : s.mem h = 0 + · simp only [cellMethods, StateTransitionSpec.clientHistory, + runClient_cellGet_of_eq_zero h w s h0] + exact ⟨hh, trivial⟩ + · simp only [cellMethods, StateTransitionSpec.clientHistory, + runClient_cellGet_of_ne_zero h w s h0] + exact ⟨hh, CellInv.value_lt hs h0, trivial⟩) + (by + intro s o hs hv + have hh := CellInv.header_lt hs + cases o with + | set v => + obtain ⟨hnone, -⟩ := hv + have h0 := cellAbs_eq_none.mp hnone + have hr := CellInv.fits_room hs + simp only [cellRoom, h0, ↓reduceIte] at hr + have hne : s.frontier ≠ h := by omega + have hf0 : s.frontier ≠ 0 := by omega + simp only [cellMethods, StateTransitionSpec.clientState, StateTransitionSpec.clientResult, + runClient_cellSet] + refine ⟨?_, ⟨by simp only; omega, fun _ => ?_, ?_⟩⟩ + · simp [cellAbs, cellStep, hne, hf0] + · simp only [Function.update_self] + omega + · simpa [cellRoom, hf0] using hr + | get => + by_cases h0 : s.mem h = 0 + · simp only [cellMethods, StateTransitionSpec.clientState, + StateTransitionSpec.clientResult, runClient_cellGet_of_eq_zero h w s h0] + exact ⟨by simp [cellAbs, h0, cellStep], hs⟩ + · simp only [cellMethods, StateTransitionSpec.clientState, + StateTransitionSpec.clientResult, runClient_cellGet_of_ne_zero h w s h0] + exact ⟨by simp [cellAbs, h0, cellStep], hs⟩) + +/-- The refinement runs the cell's methods. -/ +@[simp] theorem cellRefinement_methods : (cellRefinement h w).methods = cellMethods h w := rfl + +/-- The refinement's abstraction. -/ +@[simp] theorem cellRefinement_abs : (cellRefinement h w).abs = cellAbs h := rfl + +/-- The refinement's invariant. -/ +@[simp] theorem cellRefinement_inv : (cellRefinement h w).inv = CellInv h w := rfl + +/-- The header belongs to the footprint. -/ +theorem header_mem_cellFootprint (s : State) : h ∈ cellFootprint h s := by + unfold cellFootprint + split <;> simp + +/-- **The write-once cell, framed with room.** Its footprint grows into the cell that its first +`set` allocates, and that `set` gives up the one cell of room it advances the frontier by. -/ +def cellFramed : Framed (Cell w) w where + toRefinement := cellRefinement h w + footprint := cellFootprint h + room := cellRoom h + lt_frontier {s a} hs ha := by + have hh := CellInv.header_lt hs + unfold cellFootprint at ha + split at ha + · rw [Finset.mem_singleton] at ha + omega + · rcases Finset.mem_insert.mp ha with ha | ha + · omega + · rw [Finset.mem_singleton] at ha + rw [ha] + exact CellInv.value_lt hs (by assumption) + congr {s s'} hs hmem hf hr := by + have hh : s'.mem h = s.mem h := hmem h (header_mem_cellFootprint h s) + have hroom : cellRoom h s' = cellRoom h s := by simp only [cellRoom, hh] + have hfp : cellFootprint h s' = cellFootprint h s := by simp only [cellFootprint, hh] + refine ⟨⟨(CellInv.header_lt hs).trans_le hf, fun h0 => ?_, hroom ▸ hr⟩, ?_, hfp, hroom⟩ + · rw [hh] at h0 ⊢ + exact (CellInv.value_lt hs h0).trans_le hf + · change cellAbs h s' = cellAbs h s + unfold cellAbs + by_cases h0 : s.mem h = 0 + · simp [hh, h0] + · have hv : s'.mem (s.mem h) = s.mem (s.mem h) := hmem _ (by simp [cellFootprint, h0]) + simp [hh, h0, hv] + modifies {s} o {a s' tr} hs hv hrun := by + obtain ⟨_, _, rfl, _⟩ := ((spec w).clientRun_iff_runClient _ _ _ _ _).mp hrun + simp only [cellRefinement_inv, cellRefinement_abs] at hs hv + have hh := CellInv.header_lt hs + cases o with + | set v => + obtain ⟨hnone, -⟩ := hv + have h0 := cellAbs_eq_none.mp hnone + have hne : s.frontier ≠ h := by omega + simp only [cellRefinement_methods, cellMethods, StateTransitionSpec.clientState, + runClient_cellSet] + refine ⟨fun b hb hb' => ?_, fun b hb => ?_, ?_⟩ + · have hbh : b ≠ h := fun e => hb' (e ▸ header_mem_cellFootprint h s) + change Function.update (Function.update s.mem s.frontier v) h s.frontier b = s.mem b + rw [Function.update_of_ne hbh, Function.update_of_ne (by omega)] + · have hf0 : s.frontier ≠ 0 := by omega + simp only [cellFootprint, Function.update_self, hf0, ↓reduceIte, Finset.mem_insert, + Finset.mem_singleton] at hb + rcases hb with hb | hb + · exact .inl (hb ▸ header_mem_cellFootprint h s) + · exact .inr hb.ge + · have hf0 : s.frontier ≠ 0 := by omega + simp [cellRoom, h0, hf0] + | get => + by_cases h0 : s.mem h = 0 + · simp only [cellRefinement_methods, cellMethods, StateTransitionSpec.clientState, + runClient_cellGet_of_eq_zero h w s h0] + exact ⟨fun _ _ _ => trivial, fun _ hb => .inl hb, le_rfl⟩ + · simp only [cellRefinement_methods, cellMethods, StateTransitionSpec.clientState, + runClient_cellGet_of_ne_zero h w s h0] + exact ⟨fun _ _ _ => trivial, fun _ hb => .inl hb, le_rfl⟩ + +/-- A set costs three memory units, a get at most two, with no potential. -/ +theorem cellAmortized : (cellFramed h w).Amortized charge (fun _ _ => 3) fun _ => 0 := by + apply Refinement.Amortized.ofFn + intro s o _ _ + change (spec w).totalCost charge s ((spec w).clientHistory s (cellMethods h w o)) + 0 ≤ 3 + 0 + cases o with + | set v => simp [cellMethods, StateTransitionSpec.clientHistory, runClient_cellSet] + | get => + by_cases h0 : s.mem h = 0 + · simp [cellMethods, StateTransitionSpec.clientHistory, runClient_cellGet_of_eq_zero h w s h0] + · simp [cellMethods, StateTransitionSpec.clientHistory, runClient_cellGet_of_ne_zero h w s h0] + +/-- **The write-once cell as an allocator**: take a header at the frontier without clearing it, +since the memory beyond the frontier is zero, and reserve one more cell for the first `set`. +Another structure's allocation keeps the memory beyond the new frontier zero. -/ +def cellAllocator : Allocator (Cell w) w where + Handle := ℕ + alloc := allocDirty 1 + methods h := cellMethods h w + init := none + room := 2 + cost := 1 + Pre s := ∀ a, s.frontier ≤ a → s.mem a = 0 + pre_fresh hs _ habove hf _ a ha := (habove a ha).trans (hs a (hf.trans ha)) + framed s _ _ := cellFramed s.frontier w + allocates s hs hroom := by + have h0 : s.mem s.frontier = 0 := hs _ le_rfl + refine + { validHistory := ?_, cost_le := ?_, mem_eq := ?_, methods_eq := rfl, inv := ?_, + abs_eq := ?_, of_mem_footprint := ?_, room_le := ?_ } <;> + simp only [StateTransitionSpec.clientHistory, StateTransitionSpec.clientState, + runClient_allocDirty_one] + · exact ⟨hroom.of_le (by omega), trivial⟩ + · simp + · exact fun _ _ => trivial + · refine ⟨Nat.lt_add_one _, fun h => absurd h0 h, ?_⟩ + change Fits w (s.frontier + 1 + cellRoom s.frontier ⟨s.mem, _⟩) + simp only [cellRoom, h0, ↓reduceIte] + exact hroom.of_le (by omega) + · change cellAbs s.frontier ⟨s.mem, _⟩ = none + simp [cellAbs, h0] + · intro a ha + change a ∈ cellFootprint s.frontier ⟨s.mem, _⟩ at ha + simp only [cellFootprint, h0, ↓reduceIte, Finset.mem_singleton] at ha + exact .inr ha.ge + · change s.frontier + 1 + cellRoom s.frontier ⟨s.mem, _⟩ ≤ _ + simp only [cellRoom, h0, ↓reduceIte] + omega + +/-- Each cell costs three memory units per operation, and allocation leaves no potential. -/ +theorem cellAllocator_amortized : (cellAllocator w).Amortized (fun _ _ => 3) 0 := + fun s _ _ => ⟨fun _ => 0, cellAmortized s.frontier w, Framed.Local.const _ 0, le_rfl⟩ + +/-! ## Two cells that allocate inside their operations -/ + +/-- Two write-once cells in one memory, each with one cell of room for its `set`. -/ +abbrev cells : Allocator (product (Cell 8) (Cell 8)) 8 := (cellAllocator 8).prod (cellAllocator 8) + +/-- The two cells reserve four cells: two headers and two value cells. -/ +example : cells.room = 4 := rfl + +/-- Set the left cell. -/ +def setLeft : (product (Cell 8) (Cell 8)).Client Unit := + (product (Cell 8) (Cell 8)).call (.inl (.set 5)) + +/-- Set the left cell, then the right one. -/ +def setBoth : (product (Cell 8) (Cell 8)).Client Unit := do + let _ ← (product (Cell 8) (Cell 8)).call (.inl (.set 5)) + let _ ← (product (Cell 8) (Cell 8)).call (.inr (.set 7)) + pure () + +/-- Set both cells, then get both. -/ +def client : (product (Cell 8) (Cell 8)).Client (Option ℕ × Option ℕ) := do + setBoth + let a ← (product (Cell 8) (Cell 8)).call (.inl .get) + let b ← (product (Cell 8) (Cell 8)).call (.inr .get) + pure (a, b) + +/-- Memory with nothing allocated. -/ +def nothing : State := ⟨fun _ => 0, 0⟩ + +/-- Besides room, the two cells need the memory beyond the frontier to be zero, as the input +convention leaves it. The second cell's need survives the first cell's allocation. -/ +theorem pre {s : State} (hs : ∀ a, s.frontier ≤ a → s.mem a = 0) : cells.Pre s := + ⟨hs, hs, Finset.disjoint_empty_left _⟩ + +/-- The four reserved cells fit a byte. -/ +theorem fits : Fits 8 (nothing.frontier + cells.room) := by decide + +/-- The two cells, as set up by the allocation from `nothing`. -/ +abbrev framed : Framed (product (Cell 8) (Cell 8)) 8 := + cells.framed nothing (pre fun _ _ => rfl) fits + +/-- The client is admissible: each cell is set once, to a byte. -/ +theorem client_valid : (product (Cell 8) (Cell 8)).ValidHistory cells.init + ((product (Cell 8) (Cell 8)).clientHistory cells.init client) := + ⟨⟨rfl, by decide⟩, ⟨rfl, by decide⟩, trivial, trivial, trivial⟩ + +/-- **The run is admissible and answers as the specification does**, by the generic theorem: no +proof about this client or this product. -/ +theorem run_correct : + (spec 8).ValidHistory nothing ((spec 8).clientHistory nothing (cells.run client)) ∧ + (spec 8).clientResult nothing (cells.run client) = (some 5, some 7) ∧ + framed.abs ((spec 8).clientState nothing (cells.run client)) = (some 5, some 7) := by + obtain ⟨hv, hres, -, habs⟩ := cells.run_correct client (pre fun _ _ => rfl) fits client_valid + exact ⟨hv, hres, habs⟩ + +/-- The same answer, by evaluation. -/ +example : (spec 8).clientResult nothing (cells.run client) = (some 5, some 7) := by decide + +/-- **Each `set` allocates inside the operation**: the headers at `0` and `1`, then the left +value cell at `2` and the right one at `3`, above the other structure's newest cell. -/ +example : (spec 8).clientHistory nothing (cells.run client) = + [.allocDirty 1, .allocDirty 1, .allocDirty 1, .write 2 5, .write 0 2, .allocDirty 1, + .write 3 7, .write 1 3, .read 0, .read 2, .read 1, .read 3] := by + decide + +/-- After allocation: both headers, both cells unset, and two cells of room up to frontier +`4`. -/ +example : let s := (spec 8).clientState nothing (cells.run (pure ())) + framed.footprint s = {0, 1} ∧ framed.abs s = (none, none) ∧ s.frontier = 2 ∧ + framed.room s = 2 := by + decide + +/-- After the left `set`: the left cell has taken its reserved cell `2`, and the right cell keeps +its value, its footprint and its reservation. The frontier plus the room is still `4`. -/ +example : let s := (spec 8).clientState nothing (cells.run setLeft) + framed.footprint s = {0, 2, 1} ∧ framed.abs s = (some 5, none) ∧ s.frontier = 3 ∧ + framed.room s = 1 := by + decide + +/-- After both `set`s: all four reserved cells are used and no room is left. -/ +example : let s := (spec 8).clientState nothing (cells.run setBoth) + framed.footprint s = {0, 2, 1, 3} ∧ framed.abs s = (some 5, some 7) ∧ s.frontier = 4 ∧ + framed.room s = 0 := by + decide + +/-- It costs one unit per header, three per `set` and two per `get`. -/ +example : (spec 8).totalCost charge nothing ((spec 8).clientHistory nothing (cells.run client)) = + 12 := by + decide + +/-- The generic cost theorem: two units to allocate, and three per operation. -/ +example : (spec 8).totalCost charge nothing ((spec 8).clientHistory nothing (cells.run client)) ≤ + 2 + 0 + 3 * 4 := by + have h := Allocator.Amortized.prod (cellAllocator_amortized (w := 8)) + (cellAllocator_amortized (w := 8)) + simp only [productCharge_const] at h + exact Allocator.run_cost_le h client (pre fun _ _ => rfl) fits client_valid + +/-- Get the left cell. -/ +def getLeft : (product (Cell 8) (Cell 8)).Client (Option ℕ) := + (product (Cell 8) (Cell 8)).call (.inl .get) + +/-- A memory with a nonzero cell beyond the frontier, where the left header will be taken. -/ +def dirty : State := ⟨fun a => if a = 0 then 9 else 0, 0⟩ + +/-- **The precondition is needed**: from `dirty` it fails, and the left cell, never set, reads as +set, since its header was taken without clearing. -/ +example : ¬cells.Pre dirty ∧ (spec 8).clientResult dirty (cells.run getLeft) = some 0 := by + refine ⟨fun hs => absurd (Allocator.ProdPre.left hs 0 le_rfl) (by decide), by decide⟩ + +/-! ### The boundary of the reservation -/ + +/-- The highest frontier with room for both cells at word size `8`: `251 + 4 = 255`. -/ +def high : State := ⟨fun _ => 0, 251⟩ + +/-- One cell higher: `252 + 4 = 256` does not fit a byte. -/ +def tooHigh : State := ⟨fun _ => 0, 252⟩ + +example : Fits 8 (high.frontier + cells.room) ∧ ¬Fits 8 (tooHigh.frontier + cells.room) := by + decide + +/-- From the highest frontier with room, the generic theorem gives an admissible run. -/ +example : (spec 8).ValidHistory high ((spec 8).clientHistory high (cells.run client)) := + (cells.run_correct client (pre fun _ _ => rfl) (by decide) client_valid).1 + +/-- One cell higher, the run is not admissible. -/ +example : ¬(spec 8).ValidHistory tooHigh ((spec 8).clientHistory tooHigh (cells.run client)) := by + decide + +/-- Only the right `set` fails, when it allocates the last of the four reserved cells: the +allocations and the left `set` are admissible. -/ +example : (spec 8).ValidHistory tooHigh ((spec 8).clientHistory tooHigh (cells.run setLeft)) ∧ + ¬(spec 8).ValidHistory tooHigh ((spec 8).clientHistory tooHigh (cells.run setBoth)) := by + decide + +/-! ## Stacks already in memory -/ + +/-- A bounded stack of capacity `2` at word size `8`. -/ +abbrev S : StateTransitionSpec := Stack.WordRAM.spec 8 2 + +/-- The layout of stack `i`: its count cell at `3 i`, its items at `3 i + 1` and `3 i + 2`. -/ +def layout (i : ℕ) : Stack.Memory.Layout := ⟨⟨3 * i, 1⟩, ⟨3 * i + 1, 2⟩⟩ + +/-- The layouts are well formed. -/ +theorem valid (i : ℕ) (hi : i < 3) : (layout i).Valid 8 2 := + Stack.Memory.valid_allocLayout (f := 3 * i) (Fits.of_le (show Fits 8 9 by decide) (by omega)) + +/-- The stack at layout `i`, taken over as it is in memory, holding `xs`. -/ +abbrev inputStack (i : ℕ) (hi : i < 3) (xs : List ℕ) : Allocator S 8 := + Allocator.resident (Stack.Memory.framed (valid i hi)) xs 0 + +/-- The input: stack `0` holds `7` on top of `5`, and stack `1` holds `4`. -/ +def input : State := + ⟨fun a => if a = 0 then 2 else if a = 1 then 5 else if a = 2 then 7 else if a = 3 then 1 + else if a = 4 then 4 else 0, 6⟩ + +/-- Stack `i` holds in the input. -/ +theorem inv_input (i : ℕ) (hi : i < 2) : Stack.Memory.Inv (layout i) input where + count_allocated := by simp only [Block.Allocated, layout, input]; omega + items_allocated := by simp only [Block.Allocated, layout, input]; omega + count_le := by + obtain _ | _ | i := i + · decide + · decide + · omega + +/-- **The Dijkstra shape**: two stacks allocated from scratch above the input, and the input's +stack `0` taken over in place, as Dijkstra's algorithm takes over its input graph. -/ +abbrev dijkstraShape : Allocator (product S (product S S)) 8 := + (Stack.Memory.allocator 8 2).prod ((Stack.Memory.allocator 8 2).prod (inputStack 0 (by decide) + [7, 5])) + +/-- The input holds the stack that the third structure takes over. -/ +theorem pre_dijkstraShape : dijkstraShape.Pre input := + ⟨trivial, ⟨trivial, ⟨inv_input 0 (by decide), by decide, le_rfl⟩, Finset.disjoint_empty_left _⟩, + Finset.disjoint_empty_left _⟩ + +/-- Pop the input's stack, push `1` on the first fresh stack and `2` on the second, then pop +all three. -/ +def dijkstraClient : (product S (product S S)).Client (List (Option ℕ)) := do + let a ← (product S (product S S)).call (.inr (.inr .pop)) + let _ ← (product S (product S S)).call (.inl (.push 1)) + let _ ← (product S (product S S)).call (.inr (.inl (.push 2))) + let b ← (product S (product S S)).call (.inl .pop) + let c ← (product S (product S S)).call (.inr (.inl .pop)) + let d ← (product S (product S S)).call (.inr (.inr .pop)) + pure [a, b, c, d] + +/-- The client is admissible from the allocated states. -/ +theorem dijkstraClient_valid : (product S (product S S)).ValidHistory dijkstraShape.init + ((product S (product S S)).clientHistory dijkstraShape.init dijkstraClient) := + ⟨trivial, ⟨by decide, by decide⟩, ⟨by decide, by decide⟩, trivial, trivial, trivial, trivial⟩ + +/-- **The generic correctness theorem**: the run answers as the specification does from the +input's stack and two empty ones. -/ +example : (spec 8).clientResult input (dijkstraShape.run dijkstraClient) = + [some 7, some 1, some 2, some 5] := by + obtain ⟨-, hres, -⟩ := + dijkstraShape.run_correct dijkstraClient pre_dijkstraShape (by decide) dijkstraClient_valid + rw [hres] + decide + +/-- The same answer, by evaluation. The fresh stacks take the six cells above the input, and +the input's stack is popped in place: its count cell, at address `0`, ends at `0`. -/ +example : (spec 8).clientResult input (dijkstraShape.run dijkstraClient) = + [some 7, some 1, some 2, some 5] ∧ + ((spec 8).clientState input (dijkstraShape.run dijkstraClient)).frontier = 12 ∧ + ((spec 8).clientState input (dijkstraShape.run dijkstraClient)).mem 0 = 0 := by + decide + +/-- The generic cost theorem: six units to allocate the fresh stacks, none for the input's, and +three per operation. -/ +example : (spec 8).totalCost charge input ((spec 8).clientHistory input + (dijkstraShape.run dijkstraClient)) ≤ 6 + 0 + 3 * 6 := by + have hres : (inputStack 0 (by decide) [7, 5]).Amortized (fun _ _ => 3) 0 := + Allocator.Amortized.resident (Stack.Memory.amortized _) (Framed.Local.const _ 0) + fun _ _ _ => le_rfl + have h := Allocator.Amortized.prod (Stack.Memory.amortized_allocator (w := 8) (C := 2)) + (Allocator.Amortized.prod (Stack.Memory.amortized_allocator (w := 8) (C := 2)) hres) + simp only [productCharge_const] at h + exact Allocator.run_cost_le h dijkstraClient pre_dijkstraShape (by decide) dijkstraClient_valid + +/-- Two stacks that the input holds in disjoint cells. -/ +abbrev bothInputs : Allocator (product S S) 8 := + (inputStack 0 (by decide) [7, 5]).prod (inputStack 1 (by decide) [4]) + +/-- Pop both input stacks twice. -/ +def popBoth : (product S S).Client (List (Option ℕ)) := do + let a ← (product S S).call (.inl .pop) + let b ← (product S S).call (.inr .pop) + let c ← (product S S).call (.inl .pop) + let d ← (product S S).call (.inr .pop) + pure [a, b, c, d] + +/-- Both stacks hold in the input, in disjoint cells. -/ +theorem pre_bothInputs : bothInputs.Pre input := + ⟨⟨inv_input 0 (by decide), by decide, le_rfl⟩, ⟨inv_input 1 (by decide), by decide, le_rfl⟩, + by decide⟩ + +/-- The generic correctness theorem for two structures taken over in place. -/ +example : (spec 8).clientResult input (bothInputs.run popBoth) = + [some 7, some 4, some 5, none] := by + obtain ⟨-, hres, -⟩ := bothInputs.run_correct popBoth pre_bothInputs (by decide) + ⟨trivial, trivial, trivial, trivial, trivial⟩ + rw [hres] + decide + +/-- **The same cells cannot be taken over twice**: the product's precondition asks for disjoint +cells, so no memory satisfies it for one stack taken over twice. -/ +example (s : State) : ¬((inputStack 0 (by decide) [7, 5]).prod + (inputStack 0 (by decide) [7, 5])).Pre s := fun hs => by + have hd : Disjoint (layout 0).footprint (layout 0).footprint := Allocator.ProdPre.disjoint hs + exact absurd hd (by decide) + +end ComplexityTests.DataStructureMemoryAlloc diff --git a/ComplexityTests/DataStructureMemoryProduct.lean b/ComplexityTests/DataStructureMemoryProduct.lean index 52d5e75184..2ad73fad46 100644 --- a/ComplexityTests/DataStructureMemoryProduct.lean +++ b/ComplexityTests/DataStructureMemoryProduct.lean @@ -99,15 +99,16 @@ theorem inv_layout (i : ℕ) (hi : i < 3) : Stack.Memory.Inv (layout i) empty wh /-- The three stacks hold in the empty memory, with disjoint footprints. -/ theorem inv_empty : triple.inv empty := - ⟨⟨inv_layout 0 (by decide), inv_layout 1 (by decide), by decide⟩, inv_layout 2 (by decide), - by decide⟩ + ⟨⟨inv_layout 0 (by decide), inv_layout 1 (by decide), by decide, by decide⟩, + inv_layout 2 (by decide), by decide, by decide⟩ /-- The specification's answer, transported to the memory run by the iterated product. -/ example : (spec 8).clientResult empty (link triple.methods client) = (product (product S S) S).clientResult (triple.abs empty) client := - (triple.simulates_client client inv_empty + have ⟨_, hres, _⟩ := triple.simulates_client client inv_empty ⟨⟨by decide, by decide⟩, ⟨by decide, by decide⟩, ⟨by decide, by decide⟩, trivial, trivial, - trivial, trivial, trivial⟩).2.1 + trivial, trivial, trivial⟩ + hres /-- Every operation of the three stacks costs at most three memory units, amortized with zero potential: the stacks' certificates add across both products. -/ @@ -117,11 +118,78 @@ theorem amortized : triple.Amortized charge (fun _ _ => 3) fun _ => 0 := by (Framed.Local.const _ 0) rw [productCharge_const] at h₀₁ have h := Framed.amortized_prod h₀₁ (Stack.Memory.amortized (valid 2 (by decide))) - (fun _ _ _ => rfl) (Framed.Local.const _ 0) + (fun _ _ _ _ => rfl) (Framed.Local.const _ 0) rwa [productCharge_const] at h /-- With zero potential, the same certificate is a worst-case charge bound. -/ example : triple.toModule.ChargeBound charge fun _ _ => 3 := amortized.chargeBound +/-! ## Allocated one after the other + +The same three stacks, allocated by a program rather than laid out by hand, in the shape of a +client of three structures such as Dijkstra's algorithm over `product PQ (product Dict Adj)`. +The generic theorems of `Memory.Allocator` give the run's admissibility, answer and cost, with no +setup proof for this client. -/ + +/-- Three stacks of capacity `2`, allocated one after the other. -/ +abbrev allocated : Allocator (product S (product S S)) 8 := + (Stack.Memory.allocator 8 2).prod + ((Stack.Memory.allocator 8 2).prod (Stack.Memory.allocator 8 2)) + +/-- The client above, on the right-nested product. -/ +def client' : (product S (product S S)).Client (List (Option ℕ) × List ℕ) := do + let _ ← (product S (product S S)).call (.inl (.push 1)) + let _ ← (product S (product S S)).call (.inl (.push 2)) + let _ ← (product S (product S S)).call (.inr (.inr (.push 3))) + let a ← (product S (product S S)).call (.inl .pop) + let b ← (product S (product S S)).call (.inl .pop) + let m ← (product S (product S S)).call (.inr (.inl .size)) + let n ← (product S (product S S)).call (.inr (.inr .size)) + pure ([a, b], [m, n]) + +/-- Memory with nothing allocated. -/ +def nothing : State := ⟨fun _ => 0, 0⟩ + +/-- The allocated run answers as the linked client on hand-placed stacks. -/ +example : (spec 8).clientResult nothing (allocated.run client') = ([some 2, some 1], [0, 1]) := by + decide + +/-- It costs the 17 units of the client and three units per allocated stack. -/ +example : (spec 8).totalCost charge nothing ((spec 8).clientHistory nothing + (allocated.run client')) = 9 + 17 := by + decide + +/-- The three stacks are allocated from scratch, so nothing is needed of the memory besides +room. -/ +theorem pre_allocated (s : State) : allocated.Pre s := + ⟨trivial, ⟨trivial, trivial, Finset.disjoint_empty_left _⟩, Finset.disjoint_empty_left _⟩ + +/-- The client is admissible for the three bounded stacks. -/ +theorem client'_valid : (product S (product S S)).ValidHistory allocated.init + ((product S (product S S)).clientHistory allocated.init client') := + ⟨⟨by decide, by decide⟩, ⟨by decide, by decide⟩, ⟨by decide, by decide⟩, trivial, trivial, + trivial, trivial, trivial⟩ + +/-- The stacks' certificates add across both products of allocators. -/ +theorem amortized_allocated : allocated.Amortized (fun _ _ => 3) 0 := by + have h := Allocator.Amortized.prod (Stack.Memory.amortized_allocator (w := 8) (C := 2)) + (Allocator.Amortized.prod (Stack.Memory.amortized_allocator (w := 8) (C := 2)) + (Stack.Memory.amortized_allocator (w := 8) (C := 2))) + simp only [productCharge_const] at h + exact h + +/-- The generic correctness theorem gives the specification's answer. -/ +example : (spec 8).clientResult nothing (allocated.run client') = + (product S (product S S)).clientResult allocated.init client' := + have ⟨_, hres, _⟩ := + allocated.run_correct client' (pre_allocated _) (by decide) client'_valid + hres + +/-- The generic cost theorem: nine units to allocate, and three per operation. -/ +example : (spec 8).totalCost charge nothing ((spec 8).clientHistory nothing + (allocated.run client')) ≤ 9 + 0 + 3 * 7 := + Allocator.run_cost_le amortized_allocated client' (pre_allocated _) (by decide) + client'_valid + end ComplexityTests.DataStructureMemoryProduct