diff --git a/Complexity.lean b/Complexity.lean index d40ce892bf..1cb1498b1c 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2928,6 +2928,7 @@ public import Complexity.DataStructure.HashFamily.WordRAM.KWise public import Complexity.DataStructure.HashFamily.WordRAM.MultiplyShift public import Complexity.DataStructure.HashFamily.WordRAM.Tabulation public import Complexity.DataStructure.Memory.Field +public import Complexity.DataStructure.Memory.Frame public import Complexity.DataStructure.Memory.Spec public import Complexity.DataStructure.ObliviousSequence public import Complexity.DataStructure.Online.Basic @@ -2979,6 +2980,7 @@ public import Complexity.DataStructure.StateTransition.CostHoare public import Complexity.DataStructure.StateTransition.Hoare public import Complexity.DataStructure.StateTransition.Impl public import Complexity.DataStructure.StateTransition.Module +public import Complexity.DataStructure.StateTransition.Oracle public import Complexity.DataStructure.StateTransition.Refinement public import Complexity.DataStructure.StateTransition.Resource public import Complexity.DataStructure.VanEmdeBoas.Basic diff --git a/Complexity/DataStructure/Memory/Frame.lean b/Complexity/DataStructure/Memory/Frame.lean new file mode 100644 index 0000000000..9c41b35613 --- /dev/null +++ b/Complexity/DataStructure/Memory/Frame.lean @@ -0,0 +1,334 @@ +/- +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.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. +* `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 +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. + +## Main definitions + +* `Memory.Framed`: a refinement over memory with a footprint. +* `Memory.Framed.ofStatic`: the constructor for a constant footprint. +* `Memory.Framed.Local`: a function of memory that reads only the footprint. +* `Memory.Framed.prod`: two framed refinements with disjoint footprints implement the product. + +## Main results + +* `Memory.frontier_le_of_clientRun`: 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.Framed.frame`: a method run of one structure leaves a structure with a disjoint + footprint unchanged. +* `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 + sets up products. + +## References + +The footprint and frame discipline is the locality principle of separation logic, here with +explicit finite footprints as in `Cslib.WordRAM.HeapAssertion`; see +[J. C. Reynolds, *Separation Logic: A Logic for Shared Mutable Data Structures*][Reynolds2002]. +-/ + +@[expose] public section + +namespace Cslib.DataStructure.Memory + +variable {w : ℕ} + +/-! ## Runs and allocated cells -/ + +/-- No run of a memory program lowers the frontier. -/ +theorem frontier_le_of_clientRun {α : Type} {s s' : State} {p : Prog α} {a : α} + {tr : (spec w).Transcript} (h : (spec w).ClientRun s p a s' tr) : + s.frontier ≤ s'.frontier := by + obtain ⟨_, _, rfl, _⟩ := ((spec w).clientRun_iff_runClient _ _ _ _ _).mp h + 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 + induction os generalizing s with + | nil => rfl + | cons o os ih => + have hw' : ∀ v, Op.write a v ∉ os := fun v hv => hw v (List.mem_cons_of_mem o hv) + change ((spec w).run (step s o).1 os).1.mem a = s.mem a + rw [ih _ (ha.trans_le (frontier_le_step s o)) hw'] + exact mem_step_of_lt_frontier s o ha fun v h => hw v (h ▸ List.mem_cons_self) + +/-- A memory program changes an allocated cell only by writing it. -/ +theorem mem_clientState_of_lt_frontier {α : Type} (s : State) (p : Prog α) {a : ℕ} + (ha : a < s.frontier) (hw : ∀ v, Op.write a v ∉ (spec w).clientHistory s p) : + ((spec w).clientState s p).mem a = s.mem a := by + rw [← (spec w).run_runClient] + exact mem_run_of_lt_frontier s _ ha hw + +/-! ## 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. -/ +structure Framed (D : StateTransitionSpec.{0, 0, 0}) (w : ℕ) extends Refinement D (spec w) where + /-- The cells holding the representation. -/ + footprint : State → Finset ℕ + /-- 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. -/ + 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. -/ + 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 + +namespace Framed + +variable {D D₁ D₂ : 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`. -/ +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) : + Framed D w where + toRefinement := M + footprint _ := fp + lt_frontier := lt_frontier + congr hs h hf := ⟨(congr hs h hf).1, (congr hs h hf).2, 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⟩ + +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. -/ +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 + +/-- The abstraction reads only the footprint. -/ +theorem Local.abs : M.Local M.abs := fun hs h hf => (M.congr hs h hf).2.1 + +/-- A constant reads no cell. -/ +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) + +/-- A run that leaves every allocated cell unchanged 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 + +variable {M} (N : Framed D₂ w) + +/-- A method run of `M` keeps every cell of a disjoint, allocated footprint. -/ +theorem agree_of_run {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) + (hrun : (spec w).ClientRun s (M.methods o) a s' tr) : + ∀ 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) + +/-- **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. -/ +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) + (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 + 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' => ?_⟩ + rw [hfp] at hb' + rcases (M.modifies o hM hv hrun).2 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) + (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) + +/-! ## 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. -/ +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. -/ +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⟩ + +/-- **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. -/ +def prod : Framed (product D₁ D₂) w where + toRefinement := M₁.toRefinement.prod M₂.toRefinement + (fun s => Disjoint (M₁.footprint s) (M₂.footprint s)) + (prod_frame_left M₁ M₂) (prod_frame_right M₁ M₂) + footprint s := M₁.footprint s ∪ M₂.footprint s + lt_frontier {_ _} hs ha := by + 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₂] + · change (M₁.abs _, M₂.abs _) = (M₁.abs _, M₂.abs _) + rw [habs₁, habs₂] + · rw [hfp₁, hfp₂] + modifies {s} o {a s' tr} hs hv hrun := by + obtain ⟨h₁, h₂, hd⟩ := 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 + 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) + | inr o => + obtain ⟨hmod, hgrow⟩ := M₂.modifies o h₂ hv hrun + obtain ⟨-, -, hfp₁, -⟩ := frame M₁ o h₂ h₁ hd.symm 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 _) + +/-- 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 + +/-- 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. -/ +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 + +/-- 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 + +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 + +/-- 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 + +/-- **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 +the product with componentwise upper charges and the sum of the potentials. -/ +theorem amortized_prod {lower : State → Op → ℕ} {upper₁ : D₁.State → D₁.Op → ℕ} + {upper₂ : D₂.State → D₂.Op → ℕ} {Φ₁ Φ₂ : State → ℕ} + (A₁ : M₁.Amortized lower upper₁ Φ₁) (A₂ : M₂.Amortized lower upper₂ Φ₂) + (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) + +/-- 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 +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')) + +end Framed + +end Cslib.DataStructure.Memory diff --git a/Complexity/DataStructure/Memory/Spec.lean b/Complexity/DataStructure/Memory/Spec.lean index 3507072aee..f61e0fda4e 100644 --- a/Complexity/DataStructure/Memory/Spec.lean +++ b/Complexity/DataStructure/Memory/Spec.lean @@ -48,6 +48,7 @@ separate step that exchanges it into instructions. Allocation never reuses addre * `Memory.WellFormed.step`, `Memory.WellFormed.run`: admissible operations preserve well-formedness. * `Memory.WellFormed.fits_of_lt_frontier`: allocated addresses fit a word. +* `Memory.one_le_charge`: every operation costs at least one unit. * `Memory.frontier_le_step`, `Memory.frontier_le_run`: the frontier never decreases. * `Memory.mem_step_of_lt_frontier`: an operation changes an allocated cell only by writing it. * `Memory.wellFormed_init`: the input convention is well formed. @@ -162,6 +163,11 @@ abbrev allocDirty (k : ℕ) : Prog ℕ := @[simp] theorem charge_allocDirty (s : State) (k : ℕ) : charge s (.allocDirty k) = 1 := rfl +/-- Every memory operation costs at least one unit, so the number of operations, hence the +glue run after them, is paid for by their charges. -/ +theorem one_le_charge (s : State) (o : Op) : 1 ≤ charge s o := by + cases o <;> simp + /-- Admissibility of a concrete history is decidable. -/ instance decidableValidHistory (w : ℕ) (s : State) (os : List Op) : Decidable ((spec w).ValidHistory s os) := by diff --git a/Complexity/DataStructure/Queue/Memory.lean b/Complexity/DataStructure/Queue/Memory.lean index d3fa6805cf..89acafde8b 100644 --- a/Complexity/DataStructure/Queue/Memory.lean +++ b/Complexity/DataStructure/Queue/Memory.lean @@ -22,8 +22,9 @@ 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. `Stack.Memory.pairRefinement`: two array stacks with disjoint layouts over `Memory.spec w`, - each stack call costing at most three memory units. +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 + 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, @@ -42,6 +43,7 @@ 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. * `run`: allocate the stacks, then run a queue client. @@ -53,6 +55,7 @@ provide. * `mem_amortized`: 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)`. * `run_cost_isBigO`: the same cost as `O(m)`. ## References @@ -188,22 +191,28 @@ 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 over memory. -/ -def memRefinement {L₁ L₂ : Stack.Memory.Layout} (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) - (hd : Disjoint L₁.footprint L₂.footprint) : +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 (Stack.Memory.pairRefinement h₁ h₂ hd) + (refinement w C).comp (pair h₁ h₂).toRefinement /-- **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) - (hd : Disjoint L₁.footprint L₂.footprint) : - (memRefinement h₁ h₂ hd).Amortized charge (fun _ _ => 9) +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 h := (amortized.mul_left 3).comp (Stack.Memory.pair_amortized h₁ h₂ hd) + have hpair := Memory.Framed.amortized_prod (Stack.Memory.amortized h₁) + (Stack.Memory.amortized h₂) (Memory.Framed.Local.const _ 0) (Memory.Framed.Local.const _ 0) + 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) = + 3 * (2 * (Stack.Memory.abs L₂ s).length) + (0 + 0)) = fun s => 6 * (Stack.Memory.abs L₂ s).length := by funext s omega @@ -214,16 +223,12 @@ theorem mem_amortized {L₁ L₂ : Stack.Memory.Layout} (h₁ : L₁.Valid w C) /-- 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 (Stack.Memory.pairMethods L₁ L₂ w C) (methods o) + 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) (hd : Disjoint L₁.footprint L₂.footprint) : - (memRefinement h₁ h₂ hd).methods = memMethods L₁ L₂ w C := by - funext o - change link (Stack.Memory.pairRefinement h₁ h₂ hd).methods (methods o) = _ - rw [Stack.Memory.pairRefinement_methods] - rfl + (h₂ : L₂.Valid w C) : (memRefinement h₁ h₂).methods = memMethods L₁ L₂ w C := rfl /-- 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 @@ -252,43 +257,33 @@ theorem runClient_run {β : Type} (p : (Queue.WordRAM.spec w C).Client β) (s : /-- 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) - (hd : Disjoint (frontLayout s C).footprint (rearLayout s C).footprint), - (memRefinement h₁ h₂ hd).inv (allocated s C) ∧ - (memRefinement h₁ h₂ hd).abs (allocated s C) = [] ∧ + ∃ (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)) - have hd : Disjoint (frontLayout s C).footprint (rearLayout s C).footprint := by - rw [Finset.disjoint_left] - intro a ha hb - simp only [Stack.Memory.Layout.footprint, Finset.mem_union, Block.mem_footprint, - Block.Owns] at ha hb - omega - -- The first stack, as allocated, before the second allocation. + -- 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 - -- The second stack, allocated from the state after the first. obtain ⟨hi₂, ha₂⟩ := Stack.Memory.inv_allocLayout (C := C) ⟨clear s.mem s.frontier 1, s.frontier + 1 + C⟩ - -- The second allocation leaves the first stack's cells alone. - have hframe : ∀ a ∈ (frontLayout s C).footprint, - (allocated s C).mem a = clear s.mem s.frontier 1 a := by - intro a ha - simp only [Stack.Memory.Layout.footprint, Finset.mem_union, Block.mem_footprint, - Block.Owns] at ha - exact clear_of_not_owns (by simp only [Block.Owns]; omega) - have hi₁' := hi₁.congr h₁ hframe (by simp only; omega) - have ha₁' := (Stack.Memory.abs_congr h₁ hi₁ hframe).trans ha₁ - refine ⟨h₁, h₂, hd, ⟨⟨hi₁', hi₂⟩, ?_⟩, ?_, ha₂⟩ - · change Inv w C (Queue.WordRAM.contents - (Stack.Memory.abs (frontLayout s C) (allocated s C), - Stack.Memory.abs (rearLayout s C) (allocated s C))) - rw [ha₁', ha₂] + -- 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 - (Stack.Memory.abs (frontLayout s C) (allocated s C), - Stack.Memory.abs (rearLayout s C) (allocated s C)) = [] - rw [ha₁', ha₂] + · change Queue.WordRAM.contents ((pair h₁ h₂).abs (allocated s C)) = [] + rw [hempty] rfl /-- **Correctness.** From any memory with room for both stacks, an admissible queue client run @@ -299,9 +294,9 @@ theorem run_correct {β : Type} (p : (Queue.WordRAM.spec w C).Client β) {s : Me (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₂, hd, hinv, habs, -⟩ := setup s hfit + obtain ⟨h₁, h₂, hinv, habs, -⟩ := setup s hfit obtain ⟨hvE, hres, -, -⟩ := - (memRefinement h₁ h₂ hd).simulates_client p hinv (by rw [habs]; exact hv) + (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 ⊢ @@ -317,8 +312,8 @@ theorem run_cost {β : Type} (p : (Queue.WordRAM.spec w C).Client β) {s : Memor (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₂, hd, hinv, habs, hrear⟩ := setup s hfit - have h := (mem_amortized h₁ h₂ hd).client p hinv (by rw [habs]; exact hv) + 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, @@ -326,6 +321,21 @@ theorem run_cost {β : Type} (p : (Queue.WordRAM.spec w C).Client β) {s : Memor simp only [List.length_nil, Nat.mul_zero, Nat.add_zero, allocated] at h ⊢ omega +/-- **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 +`(2 K + 1) (6 + 9 m)` in memory charges and glue together. The queue's and the stacks' methods +are straight-line code between memory operations, so their glue is of this form. -/ +theorem run_cost_glue {β : Type} (p : (Queue.WordRAM.spec w C).Client β) {s : Memory.State} + (hfit : Fits w (s.frontier + 2 * (C + 1))) + (hv : (Queue.WordRAM.spec w C).ValidHistory [] ((Queue.WordRAM.spec w C).clientHistory [] p)) + {glue : Memory.State → Memory.Op → ℕ} {K : ℕ} + (hglue : ∀ s o, glue s o ≤ K * (charge s o + 1)) : + (Memory.spec w).totalCost (fun s o => charge s o + glue s o) s + ((Memory.spec w).clientHistory s (run w C p)) ≤ + (2 * K + 1) * (6 + 9 * ((Queue.WordRAM.spec w C).clientHistory [] p).length) := + ((Memory.spec w).totalCost_glue_le one_le_charge hglue s _).trans + (Nat.mul_le_mul_left _ (run_cost p hfit hv)) + /-- **The exported form.** Over admissible clients, the memory cost of a run is `O(m)` in the number `m` of queue operations. -/ theorem run_cost_isBigO (s : Memory.State) (hfit : Fits w (s.frontier + 2 * (C + 1))) : diff --git a/Complexity/DataStructure/Stack/Memory.lean b/Complexity/DataStructure/Stack/Memory.lean index cf79d42258..5fb09e09e6 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.StateTransition.Refinement +public import Complexity.DataStructure.Memory.Frame public import Complexity.DataStructure.Stack.WordRAM.Basic /-! @@ -23,8 +23,9 @@ refinement obligations follow from those equations and the list view of the arra Every operation costs at most three memory units, with no potential (`amortized`). The methods 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`). Two stacks with disjoint -layouts therefore implement the product of two stacks (`pairRefinement`). +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`. 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 @@ -37,18 +38,15 @@ admissibility of `Memory.spec w` and one static fact of the layout, that the cap * `push`, `pop`, `size`, `methods`: the operations as memory programs. * `abs`, `Inv`: the abstraction function and the implementation invariant. * `refinement`: the array stack as a `Refinement` of the bounded stack. -* `pairMethods`, `pairRefinement`: two array stacks with disjoint layouts implement the pair of - stacks. +* `framed`: the same refinement, framed by the layout's cells. * `allocLayout`: allocate an empty stack. ## Main results * `amortized`: every operation costs at most three memory units. -* `pair_amortized`: so does every operation of the pair. -* `pairRefinement_methods`: the pair's methods do not depend on the proofs about its layouts. * `runClient_push`, `runClient_pop_of_eq_zero`, `runClient_pop_of_pos`, `runClient_size`: the operations evaluate definitionally. -* `modifies_methods`, `abs_congr`, `Inv.congr`, `frame`: the frame of a stack. +* `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. @@ -278,20 +276,6 @@ def refinement (hL : L.Valid w C) : Refinement (Stack.WordRAM.spec w C) (Memory. runClient_size] exact ⟨by simp, hs⟩) -/-- Every operation costs at most three memory units, so the stack needs no potential. -/ -theorem amortized (hL : L.Valid w C) : - (refinement hL).Amortized charge (fun _ _ => 3) fun _ => 0 := by - apply Refinement.Amortized.ofFn - intro s o _ _ - cases o with - | push v => simp [refinement, methods, StateTransitionSpec.clientHistory, runClient_push] - | pop => - by_cases h0 : s.mem L.count.base = 0 - · simp [refinement, methods, StateTransitionSpec.clientHistory, - runClient_pop_of_eq_zero L s h0] - · simp [refinement, methods, StateTransitionSpec.clientHistory, runClient_pop_of_pos L s h0] - | size => simp [refinement, methods, StateTransitionSpec.clientHistory, runClient_size] - /-! ## The frame of a stack -/ /-- Each admissible operation writes only the layout's cells and never allocates. -/ @@ -319,54 +303,44 @@ theorem modifies_methods (hL : L.Valid w C) {s : Memory.State} (o : StackOp ℕ) exact ⟨fun a ha => Function.update_of_ne (ne_of_mem_of_not_mem hc ha).symm _ _, trivial⟩ | size => exact ⟨fun _ _ => rfl, rfl⟩ -/-- A stack's operations leave a stack with a disjoint layout unchanged. -/ -theorem frame {L' : Layout} (hL : L.Valid w C) (hL' : L'.Valid w C) - (hd : Disjoint L.footprint L'.footprint) {s : Memory.State} (hs' : Inv L' s) - (o : StackOp ℕ) (hv : (Stack.WordRAM.spec w C).valid (abs L s) o) : - abs L' ((Memory.spec w).clientState s (methods L w C o)) = abs L' s ∧ - Inv L' ((Memory.spec w).clientState s (methods L w C o)) := by - obtain ⟨hm, hf⟩ := modifies_methods hL o hv - have h : ∀ a ∈ L'.footprint, - ((Memory.spec w).clientState s (methods L w C o)).mem a = s.mem a := - fun a ha => hm a (Finset.disjoint_right.mp hd ha) - exact ⟨abs_congr hL' hs' h, hs'.congr hL' h hf.ge⟩ - -/-! ## Two stacks in one memory -/ - -/-- The operations of two stacks, each on its own layout. -/ -def pairMethods (L₁ L₂ : Layout) (w C : ℕ) : - Methods (product (Stack.WordRAM.spec w C) (Stack.WordRAM.spec w C)) (Memory.spec w) - | .inl o => methods L₁ w C o - | .inr o => methods L₂ w C o - -/-- Two array stacks with disjoint layouts implement a pair of bounded stacks. -/ -def pairRefinement {L₁ L₂ : Layout} (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) - (hd : Disjoint L₁.footprint L₂.footprint) : - Refinement (product (Stack.WordRAM.spec w C) (Stack.WordRAM.spec w C)) (Memory.spec w) := - (refinement h₁).prod (refinement h₂) - (fun {s} o {a s' tr} hs₁ hs₂ hv hrun => by - obtain ⟨_, _, rfl, _⟩ := ((Memory.spec w).clientRun_iff_runClient _ _ _ _ _).mp hrun - exact frame h₁ h₂ hd hs₂ o hv) - (fun {s} o {a s' tr} hs₁ hs₂ hv hrun => by - obtain ⟨_, _, rfl, _⟩ := ((Memory.spec w).clientRun_iff_runClient _ _ _ _ _).mp hrun - exact frame h₂ h₁ hd.symm hs₁ o hv) - -/-- The pair's methods are `pairMethods`, whatever the proofs about the layouts. -/ -theorem pairRefinement_methods {L₁ L₂ : Layout} (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) - (hd : Disjoint L₁.footprint L₂.footprint) : - (pairRefinement h₁ h₂ hd).methods = pairMethods L₁ L₂ w C := by - funext o - cases o <;> rfl - -/-- Every operation of the pair costs at most three memory units. -/ -theorem pair_amortized {L₁ L₂ : Layout} (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) - (hd : Disjoint L₁.footprint L₂.footprint) : - (pairRefinement h₁ h₂ hd).Amortized charge (fun _ _ => 3) fun _ => 0 := by - have h : (pairRefinement h₁ h₂ hd).Amortized charge - (productCharge (fun _ _ => 3) (fun _ _ => 3)) fun _ => 0 := - (amortized h₁).prod (amortized h₂) (fun _ _ _ _ _ _ _ _ => rfl) - (fun _ _ _ _ _ _ _ _ => rfl) - rwa [productCharge_const] at h +/-- The layout's cells are allocated. -/ +theorem Inv.lt_frontier {s : Memory.State} (hs : Inv L s) {a : ℕ} (ha : a ∈ L.footprint) : + a < s.frontier := by + have h₁ := hs.count_allocated + have h₂ := hs.items_allocated + simp only [Layout.footprint, Finset.mem_union, Block.mem_footprint, Block.Owns] at ha + unfold Block.Allocated at h₁ h₂ + omega + +/-- The array stack, with its layout's cells as a constant footprint. Stacks with disjoint +layouts therefore share one memory as a product of stacks (`Memory.Framed.prod`). -/ +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) + +/-- Every operation costs at most three memory units, so the stack needs no potential. -/ +theorem amortized (hL : L.Valid w C) : + (framed hL).Amortized charge (fun _ _ => 3) fun _ => 0 := by + apply Refinement.Amortized.ofFn + intro s o _ _ + cases o with + | push v => + simp [framed, Memory.Framed.ofStatic, refinement, methods, + StateTransitionSpec.clientHistory, runClient_push] + | pop => + by_cases h0 : s.mem L.count.base = 0 + · simp [framed, Memory.Framed.ofStatic, refinement, methods, + StateTransitionSpec.clientHistory, runClient_pop_of_eq_zero L s h0] + · simp [framed, Memory.Framed.ofStatic, refinement, methods, + StateTransitionSpec.clientHistory, runClient_pop_of_pos L s h0] + | size => + simp [framed, Memory.Framed.ofStatic, refinement, methods, + StateTransitionSpec.clientHistory, runClient_size] + +/-- The footprint of a stack is its layout's cells. -/ +@[simp] theorem framed_footprint (hL : L.Valid w C) (s : Memory.State) : + (framed hL).footprint s = L.footprint := rfl /-! ## Allocation -/ diff --git a/Complexity/DataStructure/StateTransition/Oracle.lean b/Complexity/DataStructure/StateTransition/Oracle.lean new file mode 100644 index 0000000000..5cb3deff99 --- /dev/null +++ b/Complexity/DataStructure/StateTransition/Oracle.lean @@ -0,0 +1,44 @@ +/- +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.StateTransition.Module +public import Complexity.Languages.Probabilistic.Basic + +/-! +# Linking is oracle interpretation + +A client of a state-transition specification is an oracle program over the specification's +signature: both are `PFunctor.FreeM` over the operations and their answer types. Linking a client +through methods over a lower interface is interpreting the program in the lower interface's client +monad, answering each call with its method (`link_eq_interpret`). The lemmas about +`OracleComp.interpret` (sequencing, composition of interpretations, interpretation into `PMF` +and state monads) therefore apply to linked clients, and refinement and cost results about `link` +apply to interpreted programs. + +This bridge is its own module so that the state-transition layer does not import probability. + +## Main results + +* `link_eq_interpret`: linking is interpretation by the methods. +-/ + +@[expose] public section + +namespace Cslib.DataStructure + +universe u v w + +variable {D E : StateTransitionSpec.{u, v, w}} {α : Type w} + +/-- Linking a client through methods is interpreting it as an oracle program, answering each +call with its method. -/ +theorem link_eq_interpret (methods : Methods D E) (p : D.Client α) : + link methods p = OracleComp.interpret (spec := D.Result) (m := E.Client) methods p := rfl + +end Cslib.DataStructure diff --git a/Complexity/DataStructure/StateTransition/Refinement.lean b/Complexity/DataStructure/StateTransition/Refinement.lean index e6d94e5d59..794f512032 100644 --- a/Complexity/DataStructure/StateTransition/Refinement.lean +++ b/Complexity/DataStructure/StateTransition/Refinement.lean @@ -30,7 +30,16 @@ representation is functional yields an `Amortized` certificate of the realized m (`Refinement.Amortized.realize`). Products of refinements over one lower interface (`Refinement.prod`) need non-interference: the -methods of each side leave the other side's abstraction, invariant and potential unchanged. +methods of each side leave the other side's abstraction, invariant and potential unchanged. A +joint invariant, such as the disjointness of the memory the two sides use, may be part of the +product's invariant. `Memory.Framed.prod` discharges these obligations from footprints. + +**Glue.** A realization charges, besides each lower call, the glue code that consumes its answer. +In a free-monad program every bind follows exactly one call, so glue charged per bind is a +further charge per lower call, and `Refinement.Amortized.glue` absorbs it at a constant rate when +it is at most proportional to the call's charge plus one. Work not attached to a lower call, such +as a loop iteration that makes no call, is charged per call one level up and added with +`Refinement.Amortized.add`. ## Main definitions @@ -40,12 +49,13 @@ methods of each side leave the other side's abstraction, invariant and potential * `Refinement.toModule`: the underlying relational module. * `Refinement.id`, `Refinement.comp`, `Refinement.prod`: identity, composition, and products under non-interference. +* `Methods.prod`: the methods of both sides of a product. * `Refinement.Amortized`: per-method amortized cost refinement with a potential on lower states. * `productCharge`: componentwise charges of a product specification. -The two transcript-cost lemmas `StateTransitionSpec.totalCostTranscript_mono` and -`StateTransitionSpec.totalCostTranscript_mul_left` sit here, beside their only clients, rather -than in the widely imported `StateTransition` module. +The transcript-cost lemmas `StateTransitionSpec.totalCostTranscript_mono`, +`StateTransitionSpec.totalCostTranscript_mul_left` and `StateTransitionSpec.totalCostTranscript_add` +sit here, beside their only clients, rather than in the widely imported `StateTransition` module. ## Main results @@ -58,12 +68,15 @@ than in the widely imported `StateTransition` module. * `Refinement.Amortized.prod`: potentials add across non-interfering products. * `Refinement.Amortized.realize`: an amortized certificate for the realized module. * `Refinement.Amortized.id`: the identity refinement passes charges through. -* `Refinement.Amortized.mono`, `Refinement.Amortized.mul_left`: weaken charges, and exchange - both currencies at a constant rate. +* `Refinement.Amortized.mono`, `Refinement.Amortized.mul_left`, `Refinement.Amortized.add`: + weaken charges, exchange both currencies at a constant rate, and add certificates. +* `Refinement.Amortized.glue`, `Refinement.Amortized.glue_of_one_le`: absorb glue charged per + lower call. +* `StateTransitionSpec.totalCost_glue_le`: the same on a history. * `productCharge_const`: equal constant charges on a product. * `StateTransitionSpec.totalCostTranscript_mono`, - `StateTransitionSpec.totalCostTranscript_mul_left`: monotonicity and scaling of transcript - costs. + `StateTransitionSpec.totalCostTranscript_mul_left`, `StateTransitionSpec.totalCostTranscript_add`: + monotonicity, scaling and additivity of transcript costs. * `Refinement.Amortized.chargeBound`, `Refinement.Amortized.of_chargeBound`: with zero potential, the existing worst-case `Module.ChargeBound`. @@ -96,6 +109,11 @@ structure Refinement (D E : StateTransitionSpec.{u, v, w}) where correct : ∀ {e} o {a e' tr}, inv e → D.valid (abs e) o → E.ClientRun e (methods o) a e' tr → D.step (abs e) o (abs e') a ∧ inv e' +/-- The methods of both sides of a product, over one lower interface. -/ +def Methods.prod (m₁ : Methods D₁ E) (m₂ : Methods D₂ E) : Methods (product D₁ D₂) E + | .inl o => m₁ o + | .inr o => m₂ o + /-- Componentwise charges of a product specification. -/ def productCharge (c₁ : D₁.State → D₁.Op → ℕ) (c₂ : D₂.State → D₂.Op → ℕ) : (product D₁ D₂).State → (product D₁ D₂).Op → ℕ @@ -127,6 +145,36 @@ theorem StateTransitionSpec.totalCostTranscript_mul_left (K : ℕ) (c : D.State | cons st tr ih => simp only [StateTransitionSpec.totalCostTranscript_cons, ih, Nat.mul_add] +/-- Charges add along a transcript. -/ +theorem StateTransitionSpec.totalCostTranscript_add (c c' : D.State → D.Op → ℕ) (s : D.State) + (tr : D.Transcript) : + D.totalCostTranscript (fun s o => c s o + c' s o) s tr = + D.totalCostTranscript c s tr + D.totalCostTranscript c' s tr := by + induction tr generalizing s with + | nil => simp + | cons st tr ih => + simp only [StateTransitionSpec.totalCostTranscript_cons, ih] + omega + +/-- **Glue on a history.** Glue charged with each operation at most `K` times its charge plus `K` +costs, together with the charges, at most `2 K + 1` times the charges, when every operation +costs at least one unit. -/ +theorem StateTransitionSpec.totalCost_glue_le + {fD : (s : D.State) → (o : D.Op) → D.State × D.Result o} [D.HasStepFn fD] + {lower glue : D.State → D.Op → ℕ} {K : ℕ} (hone : ∀ s o, 1 ≤ lower s o) + (hglue : ∀ s o, glue s o ≤ K * (lower s o + 1)) (s : D.State) (os : List D.Op) : + D.totalCost (fun s o => lower s o + glue s o) s os ≤ (2 * K + 1) * D.totalCost lower s os := by + induction os generalizing s with + | nil => simp + | cons o os ih => + simp only [StateTransitionSpec.totalCost_cons] + have h := ih (D.stepFn s o).1 + have hg := hglue s o + have h1 := Nat.mul_le_mul_left K (hone s o) + rw [Nat.mul_add] at hg ⊢ + rw [Nat.add_mul, Nat.mul_assoc, Nat.one_mul] at ⊢ + omega + namespace Refinement /-- The constructor for deterministic specifications: each method's history is admissible, and @@ -230,32 +278,33 @@ theorem link_comp (M : Refinement D E) (N : Refinement E F) (p : D.Client α) : (DataStructure.link_comp M.methods N.methods p).symm /-- Two refinements over one lower interface implement the product of their specifications, -provided the methods of each leave the other's abstraction and invariant unchanged. -/ -def prod (M₁ : Refinement D₁ E) (M₂ : Refinement D₂ E) - (frame₁ : ∀ {e} o {a e' tr}, M₁.inv e → M₂.inv e → D₁.valid (M₁.abs e) o → - E.ClientRun e (M₁.methods o) a e' tr → M₂.abs e' = M₂.abs e ∧ M₂.inv e') - (frame₂ : ∀ {e} o {a e' tr}, M₁.inv e → M₂.inv e → D₂.valid (M₂.abs e) o → - E.ClientRun e (M₂.methods o) a e' tr → M₁.abs e' = M₁.abs e ∧ M₁.inv e') : +provided the methods of each leave the other's abstraction and invariant unchanged. The joint +invariant `J` holds of the shared lower state and is preserved by both sides; it records what +keeps them apart, such as the disjointness of the memory each one uses. -/ +def prod (M₁ : Refinement D₁ E) (M₂ : Refinement D₂ E) (J : E.State → Prop) + (frame₁ : ∀ {e} o {a e' tr}, M₁.inv e → M₂.inv e → J e → D₁.valid (M₁.abs e) o → + E.ClientRun e (M₁.methods o) a e' tr → M₂.abs e' = M₂.abs e ∧ M₂.inv e' ∧ J e') + (frame₂ : ∀ {e} o {a e' tr}, M₁.inv e → M₂.inv e → J e → D₂.valid (M₂.abs e) o → + E.ClientRun e (M₂.methods o) a e' tr → M₁.abs e' = M₁.abs e ∧ M₁.inv e' ∧ J e') : Refinement (product D₁ D₂) E where - methods - | .inl o => M₁.methods o - | .inr o => M₂.methods o - inv e := M₁.inv e ∧ M₂.inv e + methods := Methods.prod M₁.methods M₂.methods + inv e := M₁.inv e ∧ M₂.inv e ∧ J e abs e := (M₁.abs e, M₂.abs e) valid {_} o hi hv := by cases o with | inl o => exact M₁.valid o hi.1 hv - | inr o => exact M₂.valid o hi.2 hv + | inr o => exact M₂.valid o hi.2.1 hv correct {_} o {_ _ _} hi hv hrun := by + obtain ⟨hi₁, hi₂, hJ⟩ := hi cases o with | inl o => - obtain ⟨hstep, hi₁⟩ := M₁.correct o hi.1 hv hrun - obtain ⟨habs, hi₂⟩ := frame₁ o hi.1 hi.2 hv hrun - exact ⟨⟨hstep, habs⟩, hi₁, hi₂⟩ + obtain ⟨hstep, hi₁'⟩ := M₁.correct o hi₁ hv hrun + obtain ⟨habs, hi₂', hJ'⟩ := frame₁ o hi₁ hi₂ hJ hv hrun + exact ⟨⟨hstep, habs⟩, hi₁', hi₂', hJ'⟩ | inr o => - obtain ⟨hstep, hi₂⟩ := M₂.correct o hi.2 hv hrun - obtain ⟨habs, hi₁⟩ := frame₂ o hi.1 hi.2 hv hrun - exact ⟨⟨habs, hstep⟩, hi₁, hi₂⟩ + obtain ⟨hstep, hi₂'⟩ := M₂.correct o hi₂ hv hrun + obtain ⟨habs, hi₁', hJ'⟩ := frame₂ o hi₁ hi₂ hJ hv hrun + exact ⟨⟨habs, hstep⟩, hi₁', hi₂', hJ'⟩ /-! ## Amortized costs -/ @@ -308,6 +357,58 @@ theorem Amortized.mul_left (A : M.Amortized lower upper potential) (K : ℕ) : rw [E.totalCostTranscript_mul_left, ← Nat.mul_add, ← Nat.mul_add] exact Nat.mul_le_mul_left K (A.step o hi hv hrun) +/-- Two certificates of one refinement add: their lower charges, upper charges and potentials. -/ +theorem Amortized.add (A : M.Amortized lower upper potential) + {lower' : E.State → E.Op → ℕ} {upper' : D.State → D.Op → ℕ} {potential' : E.State → ℕ} + (B : M.Amortized lower' upper' potential') : + M.Amortized (fun e o => lower e o + lower' e o) (fun s o => upper s o + upper' s o) + (fun e => potential e + potential' e) := by + refine ⟨fun {e} o {a e' tr} hi hv hrun => ?_⟩ + have h := A.step o hi hv hrun + have h' := B.step o hi hv hrun + rw [E.totalCostTranscript_add] + omega + +/-- **Glue charges.** A realization of the lower interface charges, besides each lower call, the +glue that consumes its answer: in a free-monad program every bind follows exactly one call. If +the glue charged with a call is at most `K` times the call's charge plus `K`, a certificate for +the charges and one for the number of calls give a certificate for the combined charge. Work that +is not attached to a lower call, such as the iterations of a loop that makes no call, is a +further per-call charge of the upper interface, added with `Amortized.add` one level up. -/ +theorem Amortized.glue (A : M.Amortized lower upper potential) + {calls : D.State → D.Op → ℕ} {Ψ : E.State → ℕ} (B : M.Amortized (fun _ _ => 1) calls Ψ) + {glue : E.State → E.Op → ℕ} {K : ℕ} (hglue : ∀ e o, glue e o ≤ K * (lower e o + 1)) : + M.Amortized (fun e o => lower e o + glue e o) + (fun s o => (K + 1) * upper s o + K * calls s o) + (fun e => (K + 1) * potential e + K * Ψ e) := + ((A.mul_left (K + 1)).add (B.mul_left K)).mono + (fun e o => calc + lower e o + glue e o ≤ lower e o + K * (lower e o + 1) := Nat.add_le_add_left (hglue e o) _ + _ = (K + 1) * lower e o + K * 1 := by rw [Nat.mul_add, Nat.add_mul]; omega) + fun _ _ _ => le_rfl + +/-- **Glue charges, when every call costs at least one unit**, as every memory operation does: +then the calls are paid for by their charges, and the combined charge is amortized at `2 K + 1` +times the upper charge. -/ +theorem Amortized.glue_of_one_le (A : M.Amortized lower upper potential) + (hone : ∀ e o, 1 ≤ lower e o) {glue : E.State → E.Op → ℕ} {K : ℕ} + (hglue : ∀ e o, glue e o ≤ K * (lower e o + 1)) : + M.Amortized (fun e o => lower e o + glue e o) (fun s o => (2 * K + 1) * upper s o) + (fun e => (2 * K + 1) * potential e) := by + have h := A.glue (A.mono hone fun _ _ _ => le_rfl) hglue + have hu : (fun s o => (K + 1) * upper s o + K * upper s o) = + fun s o => (2 * K + 1) * upper s o := by + funext s o + rw [Nat.add_mul, Nat.add_mul, Nat.mul_assoc] + omega + have hp : (fun e => (K + 1) * potential e + K * potential e) = + fun e => (2 * K + 1) * potential e := by + funext e + rw [Nat.add_mul, Nat.add_mul, Nat.mul_assoc] + omega + rw [hu, hp] at h + exact h + /-- Potentials telescope along any run of a linked admissible client. -/ theorem Amortized.demonic (A : M.Amortized lower upper potential) (p : D.Client α) {e e' : E.State} {a : α} {tr_E : E.Transcript} (he : M.inv e) @@ -366,31 +467,32 @@ theorem Amortized.comp {N : Refinement E F} {lower : F.State → F.Op → ℕ} /-- **Potentials add across non-interfering products**, provided the methods of each side leave the other side's potential unchanged. -/ -theorem Amortized.prod {M₁ : Refinement D₁ E} {M₂ : Refinement D₂ E} - {frame₁ : ∀ {e} o {a e' tr}, M₁.inv e → M₂.inv e → D₁.valid (M₁.abs e) o → - E.ClientRun e (M₁.methods o) a e' tr → M₂.abs e' = M₂.abs e ∧ M₂.inv e'} - {frame₂ : ∀ {e} o {a e' tr}, M₁.inv e → M₂.inv e → D₂.valid (M₂.abs e) o → - E.ClientRun e (M₂.methods o) a e' tr → M₁.abs e' = M₁.abs e ∧ M₁.inv e'} +theorem Amortized.prod {M₁ : Refinement D₁ E} {M₂ : Refinement D₂ E} {J : E.State → Prop} + {frame₁ : ∀ {e} o {a e' tr}, M₁.inv e → M₂.inv e → J e → D₁.valid (M₁.abs e) o → + E.ClientRun e (M₁.methods o) a e' tr → M₂.abs e' = M₂.abs e ∧ M₂.inv e' ∧ J e'} + {frame₂ : ∀ {e} o {a e' tr}, M₁.inv e → M₂.inv e → J e → D₂.valid (M₂.abs e) o → + E.ClientRun e (M₂.methods o) a e' tr → M₁.abs e' = M₁.abs e ∧ M₁.inv e' ∧ J e'} {upper₁ : D₁.State → D₁.Op → ℕ} {upper₂ : D₂.State → D₂.Op → ℕ} {Φ₁ Φ₂ : E.State → ℕ} (A₁ : M₁.Amortized lower upper₁ Φ₁) (A₂ : M₂.Amortized lower upper₂ Φ₂) - (potential₁ : ∀ {e} o {a e' tr}, M₁.inv e → M₂.inv e → D₁.valid (M₁.abs e) o → + (potential₁ : ∀ {e} o {a e' tr}, M₁.inv e → M₂.inv e → J e → D₁.valid (M₁.abs e) o → E.ClientRun e (M₁.methods o) a e' tr → Φ₂ e' = Φ₂ e) - (potential₂ : ∀ {e} o {a e' tr}, M₁.inv e → M₂.inv e → D₂.valid (M₂.abs e) o → + (potential₂ : ∀ {e} o {a e' tr}, M₁.inv e → M₂.inv e → J e → D₂.valid (M₂.abs e) o → E.ClientRun e (M₂.methods o) a e' tr → Φ₁ e' = Φ₁ e) : - (M₁.prod M₂ frame₁ frame₂).Amortized lower (productCharge upper₁ upper₂) + (M₁.prod M₂ J frame₁ frame₂).Amortized lower (productCharge upper₁ upper₂) (fun e => Φ₁ e + Φ₂ e) := by refine ⟨fun {e} o {a e' tr} hi hv hrun => ?_⟩ + obtain ⟨hi₁, hi₂, hJ⟩ := hi cases o with | inl o => - have h := A₁.step o hi.1 hv hrun - have hΦ := potential₁ o hi.1 hi.2 hv hrun + have h := A₁.step o hi₁ hv hrun + have hΦ := potential₁ o hi₁ hi₂ hJ hv hrun change E.totalCostTranscript lower e tr + (Φ₁ e' + Φ₂ e') ≤ upper₁ (M₁.abs e) o + (Φ₁ e + Φ₂ e) omega | inr o => - have h := A₂.step o hi.2 hv hrun - have hΦ := potential₂ o hi.1 hi.2 hv hrun + have h := A₂.step o hi₂ hv hrun + have hΦ := potential₂ o hi₁ hi₂ hJ hv hrun change E.totalCostTranscript lower e tr + (Φ₁ e' + Φ₂ e') ≤ upper₂ (M₂.abs e) o + (Φ₁ e + Φ₂ e) omega diff --git a/ComplexityTests/DataStructureMemoryProduct.lean b/ComplexityTests/DataStructureMemoryProduct.lean new file mode 100644 index 0000000000..22244481b9 --- /dev/null +++ b/ComplexityTests/DataStructureMemoryProduct.lean @@ -0,0 +1,110 @@ +/- +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 + +/-! +# Three stacks in one memory + +Three array stacks of capacity `2` sit side by side in one memory at word size `8`. The iterated +product `(S₀.prod S₁).prod S₂` of their framed refinements implements the product of three stack +specifications. The tests run one linked client against concrete memory, transport the +specification's answer to it with `Refinement.simulates_client`, and check that the amortized +certificates add across both products to three memory units per operation, which also gives a +worst-case `Module.ChargeBound`. +-/ + +@[expose] public section + +namespace ComplexityTests.DataStructureMemoryProduct + +open Cslib.WordRAM Cslib.DataStructure Cslib.DataStructure.Memory Cslib.DataStructure.Queue + +/-- 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 three 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)) + +/-- Nested products need their transition function named. -/ +instance : (product (product S S) S).HasStepFn + (productStepFn _ _ (productStepFn S S (stack ℕ).stepFn (stack ℕ).stepFn) (stack ℕ).stepFn) := + instHasStepFnProduct _ _ + +/-- Stack `i`, framed by its layout. -/ +abbrev stackAt (i : ℕ) (hi : i < 3) : Framed S 8 := Stack.Memory.framed (valid i hi) + +/-- The three stacks in one memory. -/ +abbrev triple : Framed (product (product S S) S) 8 := + ((stackAt 0 (by decide)).prod (stackAt 1 (by decide))).prod (stackAt 2 (by decide)) + +/-- Push `1` and `2` on the first stack and `3` on the third, then pop the first stack twice and +read the sizes. -/ +def client : (product (product S S) S).Client (List (Option ℕ) × List ℕ) := do + let _ ← (product (product S S) S).call (.inl (.inl (.push 1))) + let _ ← (product (product S S) S).call (.inl (.inl (.push 2))) + let _ ← (product (product S S) S).call (.inr (.push 3)) + let a ← (product (product S S) S).call (.inl (.inl .pop)) + let b ← (product (product S S) S).call (.inl (.inl .pop)) + let m ← (product (product S S) S).call (.inl (.inr .size)) + let n ← (product (product S S) S).call (.inr .size) + pure ([a, b], [m, n]) + +/-- Nine allocated zero cells: three empty stacks. -/ +def empty : State := ⟨fun _ => 0, 9⟩ + +/-- The linked client answers last in, first out, on each stack separately. -/ +example : (spec 8).clientResult empty (link triple.methods client) = + ([some 2, some 1], [0, 1]) := by + decide + +/-- It issues `4 · 3 + 1 + 1` memory operations, three per push and per nonempty pop, one per +size. -/ +example : (spec 8).totalCost charge empty ((spec 8).clientHistory empty + (link triple.methods client)) = 17 := by + decide + +/-- Each stack holds in the empty memory. -/ +theorem inv_layout (i : ℕ) (hi : i < 3) : Stack.Memory.Inv (layout i) empty where + count_allocated := by simp only [Block.Allocated, layout, empty]; omega + items_allocated := by simp only [Block.Allocated, layout, empty]; omega + count_le := by simp [layout, empty] + +/-- 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⟩ + +/-- 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 + ⟨⟨by decide, by decide⟩, ⟨by decide, by decide⟩, ⟨by decide, by decide⟩, trivial, trivial, + trivial, trivial, trivial⟩).2.1 + +/-- Every operation of the three stacks costs at most three memory units, amortized with zero +potential: the stacks' certificates add across both products. -/ +theorem amortized : triple.Amortized charge (fun _ _ => 3) fun _ => 0 := by + have h₀₁ := Framed.amortized_prod (Stack.Memory.amortized (valid 0 (by decide))) + (Stack.Memory.amortized (valid 1 (by decide))) (Framed.Local.const _ 0) + (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) + 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 + +end ComplexityTests.DataStructureMemoryProduct diff --git a/ComplexityTests/DataStructureQueueMemory.lean b/ComplexityTests/DataStructureQueueMemory.lean index 93a8793360..78d4631f2f 100644 --- a/ComplexityTests/DataStructureQueueMemory.lean +++ b/ComplexityTests/DataStructureQueueMemory.lean @@ -73,6 +73,18 @@ example : (spec 8).clientResult empty (run 8 3 client) = example : (spec 8).totalCost charge empty ((spec 8).clientHistory empty (run 8 3 client)) ≤ 69 := run_cost client room client_valid +/-- Glue of two units after each memory operation: the 47 operations add 94 units to the 49 +memory units, within the bound `(2 · 1 + 1) · 69` for `K = 1`. -/ +example : (spec 8).totalCost (fun s o => charge s o + 2) empty + ((spec 8).clientHistory empty (run 8 3 client)) = 143 := by + decide + +example : (spec 8).totalCost (fun s o => charge s o + 2) empty + ((spec 8).clientHistory empty (run 8 3 client)) ≤ 3 * 69 := + run_cost_glue client room client_valid (K := 1) fun s o => by + have := one_le_charge s o + omega + /-- A memory with too little room: the second stack would end past the 4-bit word range. -/ example : ¬Fits 4 (empty.frontier + 2 * (7 + 1)) := by decide