From 9656b28f36ba7b4a21f36665e76a5ec03dacb333 Mon Sep 17 00:00:00 2001 From: TankTechnology <2541826291@qq.com> Date: Wed, 12 Aug 2026 18:11:47 +0800 Subject: [PATCH 01/11] feat(ch15): add legal cache traces and policy equivalence --- .../Dev/Trace/A1_LegalTrace.lean | 114 ++++++++++++++++++ Tests/Chapter_15_4_Interface.lean | 15 +++ 2 files changed, 129 insertions(+) create mode 100644 CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A1_LegalTrace.lean create mode 100644 Tests/Chapter_15_4_Interface.lean diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A1_LegalTrace.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A1_LegalTrace.lean new file mode 100644 index 00000000..c23a068a --- /dev/null +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A1_LegalTrace.lean @@ -0,0 +1,114 @@ +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S2_Farthest_In_Future + +/-! +# Chapter 15.4 development: legal cache traces + +This file separates the semantic notion of a legal cache execution from the +`Policy` representation. It is the first layer of the trace-coupling proof of +farthest-in-future optimality. +-/ + +namespace CLRS + +open Finset +open scoped BigOperators + +namespace Caching + +/-- A legal cache execution on `σ`, with cache states at request boundaries. -/ +structure LegalTrace (C₀ : Finset Page) (σ : List Page) where + cache : ℕ → Finset Page + evict : ℕ → Page + init : cache 0 = C₀ + step : ∀ t, t < σ.length → + cache (t + 1) = + if σ.getD t 0 ∈ cache t then cache t + else insert (σ.getD t 0) ((cache t).erase (evict t)) + evict_mem : ∀ t, t < σ.length → + σ.getD t 0 ∉ cache t → evict t ∈ cache t + +/-- The miss indicator of a legal trace at request position `t`. -/ +def traceFaultAt (T : LegalTrace C₀ σ) (t : ℕ) : ℕ := + if σ.getD t 0 ∈ T.cache t then 0 else 1 + +/-- The total number of misses of a legal trace over the request sequence. -/ +def traceMisses (T : LegalTrace C₀ σ) : ℕ := + ∑ t ∈ Finset.range σ.length, traceFaultAt T t + +/-- On a hit, a legal trace leaves the cache unchanged. -/ +lemma LegalTrace.cache_succ_of_mem (T : LegalTrace C₀ σ) + (t : ℕ) (ht : t < σ.length) (hrequest : σ.getD t 0 ∈ T.cache t) : + T.cache (t + 1) = T.cache t := by + rw [T.step t ht, if_pos hrequest] + +/-- On a fault, a legal trace evicts its recorded resident and loads the request. -/ +lemma LegalTrace.cache_succ_of_not_mem (T : LegalTrace C₀ σ) + (t : ℕ) (ht : t < σ.length) (hrequest : σ.getD t 0 ∉ T.cache t) : + T.cache (t + 1) = + insert (σ.getD t 0) ((T.cache t).erase (T.evict t)) := by + rw [T.step t ht, if_neg hrequest] + +/-- The legal trace generated by an eviction policy. -/ +def policyTrace (π : Policy) (C₀ : Finset Page) (σ : List Page) + (hC₀ : C₀.Nonempty) : LegalTrace C₀ σ where + cache := cacheSeq π C₀ σ + evict := fun t => π.evict t (cacheSeq π C₀ σ t) (σ.getD t 0) + init := rfl + step := by + intro t _ht + rfl + evict_mem := by + intro t _ht hmiss + exact π.evict_mem t (cacheSeq π C₀ σ t) (σ.getD t 0) hmiss + (cacheSeq_nonempty π C₀ σ t hC₀) + +/-- The legal trace generated by farthest-in-future. -/ +noncomputable def fifoTrace (C₀ : Finset Page) (σ : List Page) + (hC₀ : C₀.Nonempty) : LegalTrace C₀ σ := + policyTrace (fifoPolicy σ) C₀ σ hC₀ + +/-- A policy trace has the same pointwise miss indicator as the policy run. -/ +lemma traceFaultAt_policyTrace (π : Policy) (C₀ : Finset Page) + (σ : List Page) (hC₀ : C₀.Nonempty) (t : ℕ) : + traceFaultAt (policyTrace π C₀ σ hC₀) t = faultAt π C₀ σ t := by + rfl + +/-- A policy trace has exactly the policy's miss count. -/ +lemma traceMisses_policyTrace (π : Policy) (C₀ : Finset Page) + (σ : List Page) (hC₀ : C₀.Nonempty) : + traceMisses (policyTrace π C₀ σ hC₀) = misses π C₀ σ := by + rfl + +/-- The farthest-in-future trace has exactly the policy-level FIF miss count. -/ +lemma traceMisses_fifoTrace (C₀ : Finset Page) (σ : List Page) + (hC₀ : C₀.Nonempty) : + traceMisses (fifoTrace C₀ σ hC₀) = misses (fifoPolicy σ) C₀ σ := by + rfl + +/-- Every reachable cache boundary in a legal trace preserves cache size. -/ +lemma legalTrace_card (T : LegalTrace C₀ σ) (hC₀ : C₀.Nonempty) + (t : ℕ) (ht : t ≤ σ.length) : + (T.cache t).card = C₀.card := by + induction t with + | zero => simpa using congrArg Finset.card T.init + | succ t ih => + have htlt : t < σ.length := Nat.lt_of_succ_le ht + have htprev : t ≤ σ.length := Nat.le_trans (Nat.le_succ t) ht + rw [T.step t htlt] + by_cases hrequest : σ.getD t 0 ∈ T.cache t + · rw [if_pos hrequest] + exact ih htprev + · rw [if_neg hrequest] + have hevict : T.evict t ∈ T.cache t := T.evict_mem t htlt hrequest + have hnotmem : σ.getD t 0 ∉ (T.cache t).erase (T.evict t) := by + intro hmem + exact hrequest (Finset.mem_erase.mp hmem).2 + rw [Finset.card_insert_of_notMem hnotmem] + rw [Finset.card_erase_of_mem hevict] + rw [ih htprev] + have hpos : 0 < C₀.card := Finset.card_pos.mpr hC₀ + omega + +end Caching + +end CLRS diff --git a/Tests/Chapter_15_4_Interface.lean b/Tests/Chapter_15_4_Interface.lean new file mode 100644 index 00000000..a3529be5 --- /dev/null +++ b/Tests/Chapter_15_4_Interface.lean @@ -0,0 +1,15 @@ +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching + +open Finset + +namespace CLRS.Caching + +#check fifo_optimal +#print axioms fifo_optimal + +example (π : Policy) (C₀ : Finset Page) (σ : List Page) + (hC₀ : C₀.Nonempty) : + misses (fifoPolicy σ) C₀ σ ≤ misses π C₀ σ := by + exact fifo_optimal π C₀ σ hC₀ + +end CLRS.Caching From 8c63681908448bb5eafbb7cda9c6fc853700348d Mon Sep 17 00:00:00 2001 From: TankTechnology <2541826291@qq.com> Date: Wed, 12 Aug 2026 18:14:14 +0800 Subject: [PATCH 02/11] feat(ch15): formalize one-page cache difference algebra --- .../Dev/Trace/A2_OnePageDiff.lean | 115 ++++++++++++++++++ 1 file changed, 115 insertions(+) create mode 100644 CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A2_OnePageDiff.lean diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A2_OnePageDiff.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A2_OnePageDiff.lean new file mode 100644 index 00000000..0eea5ce0 --- /dev/null +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A2_OnePageDiff.lean @@ -0,0 +1,115 @@ +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Trace.A1_LegalTrace + +/-! +# Chapter 15.4 development: exact one-page cache difference + +The exchange proof needs a precise relation for two equal-size caches that +differ in exactly one resident page on each side. +-/ + +namespace CLRS + +open Finset + +namespace Caching + +/-- `A` contains only `a`, `B` contains only `b`, and their common cores agree. -/ +def OnePageDiff (A B : Finset Page) (a b : Page) : Prop := + a ∈ A ∧ a ∉ B ∧ b ∉ A ∧ b ∈ B ∧ A.erase a = B.erase b + +namespace OnePageDiff + +lemma left_mem (h : OnePageDiff A B a b) : a ∈ A := h.1 + +lemma left_not_mem_right (h : OnePageDiff A B a b) : a ∉ B := h.2.1 + +lemma right_not_mem_left (h : OnePageDiff A B a b) : b ∉ A := h.2.2.1 + +lemma right_mem (h : OnePageDiff A B a b) : b ∈ B := h.2.2.2.1 + +lemma erase_eq (h : OnePageDiff A B a b) : A.erase a = B.erase b := h.2.2.2.2 + +/-- The two distinguished pages of an exact one-page difference are distinct. -/ +lemma ne (h : OnePageDiff A B a b) : a ≠ b := by + intro hab + subst b + exact h.right_not_mem_left h.left_mem + +/-- Reversing the caches reverses the two distinguished pages. -/ +lemma symm (h : OnePageDiff A B a b) : OnePageDiff B A b a := by + exact ⟨h.right_mem, h.right_not_mem_left, h.left_not_mem_right, + h.left_mem, h.erase_eq.symm⟩ + +/-- Membership agrees away from the two distinguished pages. -/ +lemma mem_iff (h : OnePageDiff A B a b) + (hxa : x ≠ a) (hxb : x ≠ b) : x ∈ A ↔ x ∈ B := by + constructor + · intro hx + have hxe : x ∈ A.erase a := Finset.mem_erase.mpr ⟨hxa, hx⟩ + rw [h.erase_eq] at hxe + exact (Finset.mem_erase.mp hxe).2 + · intro hx + have hxe : x ∈ B.erase b := Finset.mem_erase.mpr ⟨hxb, hx⟩ + rw [← h.erase_eq] at hxe + exact (Finset.mem_erase.mp hxe).2 + +/-- Exact one-page-different caches have equal cardinality. -/ +lemma card_eq (h : OnePageDiff A B a b) : A.card = B.card := by + calc + A.card = (A.erase a).card + 1 := (Finset.card_erase_add_one h.left_mem).symm + _ = (B.erase b).card + 1 := + congrArg (fun S : Finset Page => S.card + 1) h.erase_eq + _ = B.card := Finset.card_erase_add_one h.right_mem + +/-- Removing the unique page on each side and loading the same request merges caches. -/ +lemma merge (h : OnePageDiff A B a b) (r : Page) : + insert r (A.erase a) = insert r (B.erase b) := by + rw [h.erase_eq] + +/-- Erasing the same non-distinguished page preserves the exact difference. -/ +lemma erase_common (h : OnePageDiff A B a b) (x : Page) + (hxa : x ≠ a) (hxb : x ≠ b) : + OnePageDiff (A.erase x) (B.erase x) a b := by + refine ⟨?_, ?_, ?_, ?_, ?_⟩ + · exact Finset.mem_erase.mpr ⟨hxa.symm, h.left_mem⟩ + · intro ha + exact h.left_not_mem_right (Finset.mem_erase.mp ha).2 + · intro hb + exact h.right_not_mem_left (Finset.mem_erase.mp hb).2 + · exact Finset.mem_erase.mpr ⟨hxb.symm, h.right_mem⟩ + · rw [Finset.erase_right_comm, h.erase_eq, Finset.erase_right_comm] + +/-- Inserting a page absent from both caches preserves their exact difference. -/ +lemma insert_common (h : OnePageDiff A B a b) (r : Page) + (hrA : r ∉ A) (hrB : r ∉ B) : + OnePageDiff (insert r A) (insert r B) a b := by + have hra : r ≠ a := by + intro hra + subst a + exact hrA h.left_mem + have hrb : r ≠ b := by + intro hrb + subst b + exact hrB h.right_mem + refine ⟨?_, ?_, ?_, ?_, ?_⟩ + · exact Finset.mem_insert_of_mem h.left_mem + · simpa [hra.symm] using h.left_not_mem_right + · simpa [hrb.symm] using h.right_not_mem_left + · exact Finset.mem_insert_of_mem h.right_mem + · rw [Finset.erase_insert_of_ne hra, Finset.erase_insert_of_ne hrb, h.erase_eq] + +/-- Mirroring a common fault preserves the exact one-page difference. -/ +lemma fault_common (h : OnePageDiff A B a b) (x r : Page) + (hxa : x ≠ a) (hxb : x ≠ b) (hrA : r ∉ A) (hrB : r ∉ B) : + OnePageDiff (insert r (A.erase x)) (insert r (B.erase x)) a b := by + apply (h.erase_common x hxa hxb).insert_common r + · intro hr + exact hrA (Finset.mem_erase.mp hr).2 + · intro hr + exact hrB (Finset.mem_erase.mp hr).2 + +end OnePageDiff + +end Caching + +end CLRS From 5a96b2805625b3bffef0653e23d224e6cd7ef1ed Mon Sep 17 00:00:00 2001 From: TankTechnology <2541826291@qq.com> Date: Wed, 12 Aug 2026 18:16:26 +0800 Subject: [PATCH 03/11] feat(ch15): add recursive one-page coupling core --- .../Dev/Trace/A3_CouplingCore.lean | 122 ++++++++++++++++++ 1 file changed, 122 insertions(+) create mode 100644 CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A3_CouplingCore.lean diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A3_CouplingCore.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A3_CouplingCore.lean new file mode 100644 index 00000000..a00572c2 --- /dev/null +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A3_CouplingCore.lean @@ -0,0 +1,122 @@ +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Trace.A2_OnePageDiff + +/-! +# Chapter 15.4 development: recursive coupling core + +This file defines the transformed execution used by the local exchange. The +definitions are total; their legality and miss accounting are proved in A4. +-/ + +namespace CLRS + +open Finset + +namespace Caching + +/-- The phase of the one-page coupling. -/ +inductive CouplingMode where + | same + | ordered (a b : Page) + | credited (a b : Page) +deriving DecidableEq, Repr + +/-- Apply one recorded eviction decision to a cache request. -/ +def traceStepCache (C : Finset Page) (evict request : Page) : Finset Page := + if request ∈ C then C else insert request (C.erase evict) + +/-- +Choose the transformed eviction while mirroring the source. If the source +hits its unique page, or evicts its unique page, the transformed side removes +its own unique page so that the caches merge. +-/ +def coupledEvict (mode : CouplingMode) (A B : Finset Page) + (sourceEvict request : Page) : Page := + match mode with + | .same => sourceEvict + | .ordered a b => + if request ∈ B ∧ request ∉ A then a + else if sourceEvict = b then a else sourceEvict + | .credited a b => + if request ∈ B ∧ request ∉ A then a + else if sourceEvict = b then a else sourceEvict + +/-- Update the coupling phase after both caches take one step. -/ +def nextCouplingMode (mode : CouplingMode) (request sourceEvict : Page) + (transformedNext sourceNext : Finset Page) : CouplingMode := + if transformedNext = sourceNext then .same + else + match mode with + | .same => .same + | .ordered a b => + if request = a then .credited sourceEvict b else .ordered a b + | .credited a b => + if request = a then .credited sourceEvict b else .credited a b + +/-- State of the transformed execution at one request boundary. -/ +structure CouplingState where + cache : Finset Page + evict : Page + mode : CouplingMode + +/-- +The transformed suffix at relative boundary `n`; absolute request positions +are `start + n`. +-/ +def couplingCore (source : LegalTrace C₀ σ) (start : ℕ) + (initialCache : Finset Page) (initialMode : CouplingMode) : + ℕ → CouplingState + | 0 => + let sourceCache := source.cache start + let request := σ.getD start 0 + let evict := coupledEvict initialMode initialCache sourceCache + (source.evict start) request + ⟨initialCache, evict, initialMode⟩ + | n + 1 => + let previous := couplingCore source start initialCache initialMode n + let absolute := start + n + let request := σ.getD absolute 0 + let transformedNext := traceStepCache previous.cache previous.evict request + let sourceNext := source.cache (absolute + 1) + let modeNext := nextCouplingMode previous.mode request (source.evict absolute) + transformedNext sourceNext + let nextAbsolute := absolute + 1 + let nextRequest := σ.getD nextAbsolute 0 + let nextEvict := coupledEvict modeNext transformedNext sourceNext + (source.evict nextAbsolute) nextRequest + ⟨transformedNext, nextEvict, modeNext⟩ + +@[simp] lemma couplingCore_zero (source : LegalTrace C₀ σ) (start : ℕ) + (A : Finset Page) (mode : CouplingMode) : + (couplingCore source start A mode 0).cache = A := by + rfl + +/-- Cache states of the full trace splice: source prefix, transformed suffix. -/ +def coupledCache (source : LegalTrace C₀ σ) (start : ℕ) + (A : Finset Page) (mode : CouplingMode) (s : ℕ) : Finset Page := + if s < start then source.cache s + else (couplingCore source start A mode (s - start)).cache + +/-- +Evictions of the full trace splice. The replacement boundary decision is at +`start - 1`; core decisions begin at `start`. +-/ +def coupledTraceEvict (source : LegalTrace C₀ σ) (start : ℕ) + (boundaryEvict : Page) (A : Finset Page) (mode : CouplingMode) + (s : ℕ) : Page := + if s + 1 < start then source.evict s + else if s + 1 = start then boundaryEvict + else (couplingCore source start A mode (s - start)).evict + +@[simp] lemma coupledCache_of_lt (source : LegalTrace C₀ σ) (start : ℕ) + (A : Finset Page) (mode : CouplingMode) (s : ℕ) (hs : s < start) : + coupledCache source start A mode s = source.cache s := by + simp [coupledCache, hs] + +@[simp] lemma coupledCache_start (source : LegalTrace C₀ σ) (start : ℕ) + (A : Finset Page) (mode : CouplingMode) : + coupledCache source start A mode start = A := by + simp [coupledCache] + +end Caching + +end CLRS From bb92f2b453989da25273230922eae73c879fc0d3 Mon Sep 17 00:00:00 2001 From: TankTechnology <2541826291@qq.com> Date: Wed, 12 Aug 2026 18:37:31 +0800 Subject: [PATCH 04/11] feat(ch15): prove ordered and credited trace coupling --- .../Dev/Trace/A2_OnePageDiff.lean | 41 + .../Dev/Trace/A4_CouplingCorrect.lean | 850 ++++++++++++++++++ 2 files changed, 891 insertions(+) create mode 100644 CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A4_CouplingCorrect.lean diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A2_OnePageDiff.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A2_OnePageDiff.lean index 0eea5ce0..de461bdd 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A2_OnePageDiff.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A2_OnePageDiff.lean @@ -35,6 +35,12 @@ lemma ne (h : OnePageDiff A B a b) : a ≠ b := by subst b exact h.right_not_mem_left h.left_mem +/-- Exact one-page-different caches are not equal. -/ +lemma cache_ne (h : OnePageDiff A B a b) : A ≠ B := by + intro hAB + subst B + exact h.left_not_mem_right h.left_mem + /-- Reversing the caches reverses the two distinguished pages. -/ lemma symm (h : OnePageDiff A B a b) : OnePageDiff B A b a := by exact ⟨h.right_mem, h.right_not_mem_left, h.left_not_mem_right, @@ -66,6 +72,41 @@ lemma merge (h : OnePageDiff A B a b) (r : Page) : insert r (A.erase a) = insert r (B.erase b) := by rw [h.erase_eq] +/-- Loading A's unique page after removing B's unique page recovers A. -/ +lemma insert_left_erase_right (h : OnePageDiff A B a b) : + insert a (B.erase b) = A := by + rw [← h.erase_eq, Finset.insert_erase h.left_mem] + +/-- Loading B's unique page after removing A's unique page recovers B. -/ +lemma insert_right_erase_left (h : OnePageDiff A B a b) : + insert b (A.erase a) = B := by + rw [h.erase_eq, Finset.insert_erase h.right_mem] + +/-- +If A hits its unique page while B faults and evicts a common page `y`, the +new exact difference is `y` on A's side and the old `b` on B's side. +-/ +lemma hit_left_fault (h : OnePageDiff A B a b) (y : Page) + (hyB : y ∈ B) (hyb : y ≠ b) : + OnePageDiff A (insert a (B.erase y)) y b := by + have hya : y ≠ a := by + intro hya + subst y + exact h.left_not_mem_right hyB + have hyA : y ∈ A := (h.mem_iff hya hyb).2 hyB + refine ⟨hyA, ?_, h.right_not_mem_left, ?_, ?_⟩ + · simp [hya] + · exact Finset.mem_insert_of_mem (Finset.mem_erase.mpr ⟨hyb.symm, h.right_mem⟩) + · calc + A.erase y = (insert a (A.erase a)).erase y := by + rw [Finset.insert_erase h.left_mem] + _ = insert a ((A.erase a).erase y) := by + rw [Finset.erase_insert_of_ne hya.symm] + _ = insert a ((B.erase b).erase y) := by rw [h.erase_eq] + _ = insert a ((B.erase y).erase b) := by rw [Finset.erase_right_comm] + _ = (insert a (B.erase y)).erase b := by + rw [Finset.erase_insert_of_ne h.ne] + /-- Erasing the same non-distinguished page preserves the exact difference. -/ lemma erase_common (h : OnePageDiff A B a b) (x : Page) (hxa : x ≠ a) (hxb : x ≠ b) : diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A4_CouplingCorrect.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A4_CouplingCorrect.lean new file mode 100644 index 00000000..b8f1c88a --- /dev/null +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A4_CouplingCorrect.lean @@ -0,0 +1,850 @@ +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Trace.A3_CouplingCore + +/-! +# Chapter 15.4 development: coupling correctness + +This file proves that the recursive coupling is legal, preserves the exact +cache relation, and never spends more misses than the local credit permits. +-/ + +namespace CLRS + +open Finset +open scoped BigOperators + +namespace Caching + +/-- Cache relation represented by each coupling phase. -/ +def ModeRel : CouplingMode → Finset Page → Finset Page → Prop + | .same, A, B => A = B + | .ordered a b, A, B => OnePageDiff A B a b + | .credited a b, A, B => OnePageDiff A B a b + +/-- The miss indicator of one request against one cache. -/ +def faultInCache (C : Finset Page) (request : Page) : ℕ := + if request ∈ C then 0 else 1 + +/-- A cache-only miss indicator used while the transformed trace is unpackaged. -/ +def cacheFaultAt (cache : ℕ → Finset Page) (σ : List Page) (t : ℕ) : ℕ := + faultInCache (cache t) (σ.getD t 0) + +/-- Misses of a cache sequence on a finite interval starting at `start`. -/ +def cacheMissesFrom (cache : ℕ → Finset Page) (σ : List Page) + (start count : ℕ) : ℕ := + ∑ n ∈ Finset.range count, cacheFaultAt cache σ (start + n) + +/-- Ordered mode has no credit; credited mode has one saved source miss. -/ +def AccountingRel : CouplingMode → ℕ → ℕ → Prop + | .same, transformed, source => transformed ≤ source + | .ordered _ _, transformed, source => transformed ≤ source + | .credited _ _, transformed, source => transformed + 1 ≤ source + +/-- Ordered mode is safe only while the source-only page is not requested. -/ +def OrderedSafe : CouplingMode → Page → Prop + | .ordered _ b, request => request ≠ b + | _, _ => True + +lemma faultInCache_le_one (C : Finset Page) (request : Page) : + faultInCache C request ≤ 1 := by + unfold faultInCache + split <;> omega + +lemma OnePageDiff.fault_eq_of_ne (h : OnePageDiff A B a b) + (request : Page) (hrequesta : request ≠ a) (hrequestb : request ≠ b) : + faultInCache A request = faultInCache B request := by + have hmem := h.mem_iff hrequesta hrequestb + unfold faultInCache + by_cases hrequestA : request ∈ A + · have hrequestB := hmem.mp hrequestA + simp [hrequestA, hrequestB] + · have hrequestB : request ∉ B := by + intro hmemB + exact hrequestA (hmem.mpr hmemB) + simp [hrequestA, hrequestB] + +lemma OnePageDiff.fault_le_of_ne_right (h : OnePageDiff A B a b) + (request : Page) (hrequestb : request ≠ b) : + faultInCache A request ≤ faultInCache B request := by + by_cases hrequesta : request = a + · subst request + simp [faultInCache, h.left_mem, h.left_not_mem_right] + · rw [h.fault_eq_of_ne request hrequesta hrequestb] + +lemma faultInCache_le_add_one (A B : Finset Page) (request : Page) : + faultInCache A request ≤ faultInCache B request + 1 := by + have hA := faultInCache_le_one A request + omega + +/-- The common eviction rule used by both one-page-difference modes. -/ +private def diffCoupledEvict (A B : Finset Page) (a b sourceEvict request : Page) : Page := + if request ∈ B ∧ request ∉ A then a + else if sourceEvict = b then a else sourceEvict + +/-- A transformed fault always removes a transformed resident. -/ +lemma coupledEvict_mem (mode : CouplingMode) (A B : Finset Page) + (sourceEvict request : Page) (hrel : ModeRel mode A B) + (hsource : request ∉ B → sourceEvict ∈ B) + (htransformed : request ∉ A) : + coupledEvict mode A B sourceEvict request ∈ A := by + cases mode with + | same => + simp only [ModeRel] at hrel + subst B + simpa [coupledEvict] using hsource htransformed + | ordered a b => + simp only [ModeRel] at hrel + by_cases hunique : request ∈ B ∧ request ∉ A + · simp [coupledEvict, hunique, hrel.left_mem] + · have hrequestB : request ∉ B := by + intro hmem + exact hunique ⟨hmem, htransformed⟩ + have hsourceB : sourceEvict ∈ B := hsource hrequestB + by_cases hsb : sourceEvict = b + · simp [coupledEvict, hunique, hsb, hrel.left_mem] + · have hsa : sourceEvict ≠ a := by + intro hsa + subst sourceEvict + exact hrel.left_not_mem_right hsourceB + have hsourceA : sourceEvict ∈ A := (hrel.mem_iff hsa hsb).2 hsourceB + simpa [coupledEvict, hunique, hsb] using hsourceA + | credited a b => + simp only [ModeRel] at hrel + by_cases hunique : request ∈ B ∧ request ∉ A + · simp [coupledEvict, hunique, hrel.left_mem] + · have hrequestB : request ∉ B := by + intro hmem + exact hunique ⟨hmem, htransformed⟩ + have hsourceB : sourceEvict ∈ B := hsource hrequestB + by_cases hsb : sourceEvict = b + · simp [coupledEvict, hunique, hsb, hrel.left_mem] + · have hsa : sourceEvict ≠ a := by + intro hsa + subst sourceEvict + exact hrel.left_not_mem_right hsourceB + have hsourceA : sourceEvict ∈ A := (hrel.mem_iff hsa hsb).2 hsourceB + simpa [coupledEvict, hunique, hsb] using hsourceA + +/-- Complete transition classification for exact one-page-different caches. -/ +lemma onePageDiff_step_cases (h : OnePageDiff A B a b) + (sourceEvict request : Page) + (hsource : request ∉ B → sourceEvict ∈ B) : + let evict := diffCoupledEvict A B a b sourceEvict request + let transformedNext := traceStepCache A evict request + let sourceNext := traceStepCache B sourceEvict request + transformedNext = sourceNext ∨ + (request = a ∧ sourceEvict ≠ b ∧ + OnePageDiff transformedNext sourceNext sourceEvict b) ∨ + (request ≠ a ∧ OnePageDiff transformedNext sourceNext a b) := by + dsimp only + by_cases hrequestA : request ∈ A + · by_cases hrequestB : request ∈ B + · have hrequesta : request ≠ a := by + intro hrequesta + subst request + exact h.left_not_mem_right hrequestB + right + right + refine ⟨hrequesta, ?_⟩ + simpa [traceStepCache, hrequestA, hrequestB] + · have hrequestb : request ≠ b := by + intro hrequestb + subst request + exact h.right_not_mem_left hrequestA + have hrequesta : request = a := by + by_contra hne + exact hrequestB ((h.mem_iff hne hrequestb).1 hrequestA) + subst request + have hsourceB : sourceEvict ∈ B := hsource h.left_not_mem_right + by_cases hsourceb : sourceEvict = b + · subst sourceEvict + left + simpa [traceStepCache, h.left_mem, h.left_not_mem_right] using + h.insert_left_erase_right.symm + · right + left + refine ⟨rfl, hsourceb, ?_⟩ + simpa [traceStepCache, h.left_mem, h.left_not_mem_right] using + h.hit_left_fault sourceEvict hsourceB hsourceb + · by_cases hrequestB : request ∈ B + · have hrequesta : request ≠ a := by + intro hrequesta + subst request + exact hrequestA h.left_mem + have hrequestb : request = b := by + by_contra hne + exact hrequestA ((h.mem_iff hrequesta hne).2 hrequestB) + subst request + left + simpa [diffCoupledEvict, traceStepCache, h.right_not_mem_left, + h.right_mem] using h.insert_right_erase_left + · have hsourceB : sourceEvict ∈ B := hsource hrequestB + by_cases hsourceb : sourceEvict = b + · subst sourceEvict + left + simpa [diffCoupledEvict, traceStepCache, hrequestA, hrequestB] using + h.merge request + · have hsourcea : sourceEvict ≠ a := by + intro hsourcea + subst sourceEvict + exact h.left_not_mem_right hsourceB + have hrequesta : request ≠ a := by + intro hrequesta + subst request + exact hrequestA h.left_mem + right + right + refine ⟨hrequesta, ?_⟩ + simpa [diffCoupledEvict, traceStepCache, hrequestA, hrequestB, + hsourceb] using + h.fault_common sourceEvict request hsourcea hsourceb hrequestA hrequestB + +/-- One coupling step preserves the relation represented by the next mode. -/ +lemma modeRel_step (mode : CouplingMode) (A B : Finset Page) + (sourceEvict request : Page) (hrel : ModeRel mode A B) + (hsource : request ∉ B → sourceEvict ∈ B) : + let transformedNext := + traceStepCache A (coupledEvict mode A B sourceEvict request) request + let sourceNext := traceStepCache B sourceEvict request + ModeRel (nextCouplingMode mode request sourceEvict transformedNext sourceNext) + transformedNext sourceNext := by + dsimp only + cases mode with + | same => + simp only [ModeRel] at hrel + subst B + simp [coupledEvict, nextCouplingMode, ModeRel] + | ordered a b => + simp only [ModeRel] at hrel + have hcases := onePageDiff_step_cases hrel sourceEvict request hsource + simp only [diffCoupledEvict] at hcases + rcases hcases with hequal | hchanged | hstable + · have hequal' : + traceStepCache A (coupledEvict (.ordered a b) A B sourceEvict request) request = + traceStepCache B sourceEvict request := by + simpa [coupledEvict] using hequal + simp [nextCouplingMode, hequal', ModeRel] + · rcases hchanged with ⟨hrequest, hsourceb, hdiff⟩ + subst request + have hdiff' : OnePageDiff + (traceStepCache A (coupledEvict (.ordered a b) A B sourceEvict a) a) + (traceStepCache B sourceEvict a) sourceEvict b := by + simpa [coupledEvict] using hdiff + have hne := hdiff'.cache_ne + simpa [nextCouplingMode, hne, ModeRel] using hdiff' + · rcases hstable with ⟨hrequest, hdiff⟩ + have hdiff' : OnePageDiff + (traceStepCache A (coupledEvict (.ordered a b) A B sourceEvict request) request) + (traceStepCache B sourceEvict request) a b := by + simpa [coupledEvict] using hdiff + have hne := hdiff'.cache_ne + simpa [nextCouplingMode, hne, hrequest, ModeRel] using hdiff' + | credited a b => + simp only [ModeRel] at hrel + have hcases := onePageDiff_step_cases hrel sourceEvict request hsource + simp only [diffCoupledEvict] at hcases + rcases hcases with hequal | hchanged | hstable + · have hequal' : + traceStepCache A (coupledEvict (.credited a b) A B sourceEvict request) request = + traceStepCache B sourceEvict request := by + simpa [coupledEvict] using hequal + simp [nextCouplingMode, hequal', ModeRel] + · rcases hchanged with ⟨hrequest, hsourceb, hdiff⟩ + subst request + have hdiff' : OnePageDiff + (traceStepCache A (coupledEvict (.credited a b) A B sourceEvict a) a) + (traceStepCache B sourceEvict a) sourceEvict b := by + simpa [coupledEvict] using hdiff + have hne := hdiff'.cache_ne + simpa [nextCouplingMode, hne, ModeRel] using hdiff' + · rcases hstable with ⟨hrequest, hdiff⟩ + have hdiff' : OnePageDiff + (traceStepCache A (coupledEvict (.credited a b) A B sourceEvict request) request) + (traceStepCache B sourceEvict request) a b := by + simpa [coupledEvict] using hdiff + have hne := hdiff'.cache_ne + simpa [nextCouplingMode, hne, hrequest, ModeRel] using hdiff' + +/-- One request preserves the local miss-accounting invariant. -/ +lemma accounting_step (mode : CouplingMode) (A B : Finset Page) + (sourceEvict request : Page) (transformedMisses sourceMisses : ℕ) + (hrel : ModeRel mode A B) + (hsource : request ∉ B → sourceEvict ∈ B) + (hsafe : OrderedSafe mode request) + (haccount : AccountingRel mode transformedMisses sourceMisses) : + let transformedNext := + traceStepCache A (coupledEvict mode A B sourceEvict request) request + let sourceNext := traceStepCache B sourceEvict request + AccountingRel + (nextCouplingMode mode request sourceEvict transformedNext sourceNext) + (transformedMisses + faultInCache A request) + (sourceMisses + faultInCache B request) := by + dsimp only + cases mode with + | same => + simp only [ModeRel] at hrel + simp only [AccountingRel] at haccount + subst B + simp [coupledEvict, nextCouplingMode, AccountingRel] + omega + | ordered a b => + simp only [ModeRel] at hrel + simp only [OrderedSafe] at hsafe + simp only [AccountingRel] at haccount + have hcases := onePageDiff_step_cases hrel sourceEvict request hsource + simp only [diffCoupledEvict] at hcases + rcases hcases with hequal | hchanged | hstable + · have hequal' : + traceStepCache A (coupledEvict (.ordered a b) A B sourceEvict request) request = + traceStepCache B sourceEvict request := by + simpa [coupledEvict] using hequal + have hfault := hrel.fault_le_of_ne_right request hsafe + simp [nextCouplingMode, hequal', AccountingRel] + omega + · rcases hchanged with ⟨hrequest, hsourceb, hdiff⟩ + subst request + have hdiff' : OnePageDiff + (traceStepCache A (coupledEvict (.ordered a b) A B sourceEvict a) a) + (traceStepCache B sourceEvict a) sourceEvict b := by + simpa [coupledEvict] using hdiff + have hne := hdiff'.cache_ne + simp [nextCouplingMode, hne, AccountingRel, faultInCache, + hrel.left_mem, hrel.left_not_mem_right] + omega + · rcases hstable with ⟨hrequesta, hdiff⟩ + have hdiff' : OnePageDiff + (traceStepCache A (coupledEvict (.ordered a b) A B sourceEvict request) request) + (traceStepCache B sourceEvict request) a b := by + simpa [coupledEvict] using hdiff + have hne := hdiff'.cache_ne + have hfault := hrel.fault_eq_of_ne request hrequesta hsafe + simp [nextCouplingMode, hne, hrequesta, AccountingRel] + omega + | credited a b => + simp only [ModeRel] at hrel + simp only [AccountingRel] at haccount + have hcases := onePageDiff_step_cases hrel sourceEvict request hsource + simp only [diffCoupledEvict] at hcases + rcases hcases with hequal | hchanged | hstable + · have hequal' : + traceStepCache A (coupledEvict (.credited a b) A B sourceEvict request) request = + traceStepCache B sourceEvict request := by + simpa [coupledEvict] using hequal + have hfault := faultInCache_le_add_one A B request + simp [nextCouplingMode, hequal', AccountingRel] + omega + · rcases hchanged with ⟨hrequest, hsourceb, hdiff⟩ + subst request + have hdiff' : OnePageDiff + (traceStepCache A (coupledEvict (.credited a b) A B sourceEvict a) a) + (traceStepCache B sourceEvict a) sourceEvict b := by + simpa [coupledEvict] using hdiff + have hne := hdiff'.cache_ne + simp [nextCouplingMode, hne, AccountingRel, faultInCache, + hrel.left_mem, hrel.left_not_mem_right] + omega + · rcases hstable with ⟨hrequesta, hdiff⟩ + have hdiff' : OnePageDiff + (traceStepCache A (coupledEvict (.credited a b) A B sourceEvict request) request) + (traceStepCache B sourceEvict request) a b := by + simpa [coupledEvict] using hdiff + have hrequestb : request ≠ b := by + intro hrequestb + subst request + have hequal' : + traceStepCache A (coupledEvict (.credited a b) A B sourceEvict b) b = + traceStepCache B sourceEvict b := by + simpa [coupledEvict, traceStepCache, hrel.right_not_mem_left, + hrel.right_mem] using hrel.insert_right_erase_left + exact hdiff'.cache_ne hequal' + have hne := hdiff'.cache_ne + have hfault := hrel.fault_eq_of_ne request hrequesta hrequestb + simp [nextCouplingMode, hne, hrequesta, AccountingRel] + omega +/-- For distinct pages, non-strict `Farther` yields a strict first-use order. -/ +lemma farther_distinct_order {σ : List Page} {start : ℕ} {a b : Page} + (hab : a ≠ b) + (hfarther : Farther (nextUse σ start b) (nextUse σ start a)) : + nextUse σ start b = none ∨ + ∃ ja jb, nextUse σ start a = some ja ∧ + nextUse σ start b = some jb ∧ ja < jb := by + rcases farther_cases hfarther with hnone | ⟨jb, ja, hb, ha, hle⟩ + · exact Or.inl hnone + · right + refine ⟨ja, jb, ha, hb, ?_⟩ + have hne : ja ≠ jb := by + intro heq + subst jb + have hgeta := getD_eq_nextUse ha + have hgetb := getD_eq_nextUse hb + exact hab (hgeta.symm.trans hgetb) + omega + +/-- No request of the farther page occurs up to the first nearer-page request. -/ +lemma getD_ne_farther_until {σ : List Page} {start n : ℕ} {a b : Page} + (hab : a ≠ b) + (hfarther : Farther (nextUse σ start b) (nextUse σ start a)) + (hlen : start + n < σ.length) + (hdeadline : ∀ j, nextUse σ start a = some j → n ≤ j) : + σ.getD (start + n) 0 ≠ b := by + rcases farther_distinct_order hab hfarther with hnone | ⟨ja, jb, ha, hb, hjlt⟩ + · have hnone' := nextUse_eq_none_iff.mp hnone + apply hnone' (σ.getD (start + n) 0) + have hnDrop : n < (σ.drop start).length := by + rw [List.length_drop] + omega + have hget : (σ.drop start).getD n 0 = σ.getD (start + n) 0 := by + rw [getD_drop] + rw [← hget] + rw [List.getD_eq_getElem _ 0 hnDrop] + exact List.getElem_mem hnDrop + · exact getD_ne_nextUse hb (by omega) (by + have hnle := hdeadline ja ha + omega) + +/-- An ordered next mode can only come from the same ordered pair before `a`. -/ +lemma nextCouplingMode_eq_ordered {mode : CouplingMode} {request sourceEvict a b : Page} + {transformedNext sourceNext : Finset Page} + (hnext : nextCouplingMode mode request sourceEvict transformedNext sourceNext = + .ordered a b) : + mode = .ordered a b ∧ request ≠ a := by + by_cases hequal : transformedNext = sourceNext + · simp [nextCouplingMode, hequal] at hnext + · cases mode with + | same => simp [nextCouplingMode, hequal] at hnext + | ordered x y => + by_cases hrequest : request = x + · simp [nextCouplingMode, hequal, hrequest] at hnext + · simp [nextCouplingMode, hequal, hrequest] at hnext + rcases hnext with ⟨rfl, rfl⟩ + exact ⟨rfl, hrequest⟩ + | credited x y => + by_cases hrequest : request = x <;> + simp [nextCouplingMode, hequal, hrequest] at hnext + +/-- Source misses over a suffix, expressed with the legal trace cache. -/ +def traceMissesFrom (T : LegalTrace C₀ σ) (start count : ℕ) : ℕ := + cacheMissesFrom T.cache σ start count + +/-- Misses of the unpackaged recursive transformed suffix. -/ +def couplingMisses (source : LegalTrace C₀ σ) (start : ℕ) + (A : Finset Page) (mode : CouplingMode) (count : ℕ) : ℕ := + ∑ n ∈ Finset.range count, + faultInCache (couplingCore source start A mode n).cache (σ.getD (start + n) 0) + +@[simp] lemma couplingCore_cache_succ (source : LegalTrace C₀ σ) (start : ℕ) + (A : Finset Page) (mode : CouplingMode) (n : ℕ) : + (couplingCore source start A mode (n + 1)).cache = + traceStepCache (couplingCore source start A mode n).cache + (couplingCore source start A mode n).evict (σ.getD (start + n) 0) := by + rfl + +@[simp] lemma couplingCore_mode_succ (source : LegalTrace C₀ σ) (start : ℕ) + (A : Finset Page) (mode : CouplingMode) (n : ℕ) : + (couplingCore source start A mode (n + 1)).mode = + nextCouplingMode (couplingCore source start A mode n).mode + (σ.getD (start + n) 0) (source.evict (start + n)) + (couplingCore source start A mode (n + 1)).cache + (source.cache (start + n + 1)) := by + rfl + +lemma couplingCore_evict_eq (source : LegalTrace C₀ σ) (start : ℕ) + (A : Finset Page) (mode : CouplingMode) (n : ℕ) : + (couplingCore source start A mode n).evict = + coupledEvict (couplingCore source start A mode n).mode + (couplingCore source start A mode n).cache (source.cache (start + n)) + (source.evict (start + n)) (σ.getD (start + n) 0) := by + cases n <;> rfl + +/-- The recursive core preserves the cache relation at every in-range boundary. -/ +lemma couplingCore_modeRel (source : LegalTrace C₀ σ) (start : ℕ) + (A : Finset Page) (a b : Page) (hdiff : OnePageDiff A (source.cache start) a b) + (n : ℕ) (hbound : start + n ≤ σ.length) : + ModeRel (couplingCore source start A (.ordered a b) n).mode + (couplingCore source start A (.ordered a b) n).cache + (source.cache (start + n)) := by + induction n with + | zero => simpa [couplingCore, ModeRel] using hdiff + | succ n ih => + have hlt : start + n < σ.length := by omega + have hprev : start + n ≤ σ.length := by omega + have hrel := ih hprev + have hsource : σ.getD (start + n) 0 ∉ source.cache (start + n) → + source.evict (start + n) ∈ source.cache (start + n) := + source.evict_mem (start + n) hlt + have hstep := modeRel_step + (couplingCore source start A (.ordered a b) n).mode + (couplingCore source start A (.ordered a b) n).cache + (source.cache (start + n)) (source.evict (start + n)) + (σ.getD (start + n) 0) hrel hsource + have hsourceStep : source.cache (start + n + 1) = + traceStepCache (source.cache (start + n)) (source.evict (start + n)) + (σ.getD (start + n) 0) := by + simpa [traceStepCache] using source.step (start + n) hlt + have hsourceStep' : source.cache (start + (n + 1)) = + traceStepCache (source.cache (start + n)) (source.evict (start + n)) + (σ.getD (start + n) 0) := by + simpa [Nat.add_assoc] using hsourceStep + rw [couplingCore_mode_succ, couplingCore_cache_succ] + rw [hsourceStep, hsourceStep'] + rw [couplingCore_evict_eq] + exact hstep + +/-- Every transformed core fault evicts a transformed resident. -/ +lemma couplingCore_evict_mem (source : LegalTrace C₀ σ) (start : ℕ) + (A : Finset Page) (a b : Page) (hdiff : OnePageDiff A (source.cache start) a b) + (n : ℕ) (hbound : start + n < σ.length) + (hmiss : σ.getD (start + n) 0 ∉ + (couplingCore source start A (.ordered a b) n).cache) : + (couplingCore source start A (.ordered a b) n).evict ∈ + (couplingCore source start A (.ordered a b) n).cache := by + rw [couplingCore_evict_eq] + apply coupledEvict_mem + · exact couplingCore_modeRel source start A a b hdiff n (by omega) + · exact source.evict_mem (start + n) hbound + · exact hmiss + +/-- Ordered mode can only persist for the original pair and through `a`'s deadline. -/ +lemma couplingCore_ordered_deadline (source : LegalTrace C₀ σ) (start : ℕ) + (A : Finset Page) (a b : Page) (n : ℕ) : + ∀ x y, (couplingCore source start A (.ordered a b) n).mode = .ordered x y → + x = a ∧ y = b ∧ + ∀ j, nextUse σ start a = some j → n ≤ j := by + induction n with + | zero => + intro x y hmode + simp [couplingCore] at hmode + rcases hmode with ⟨rfl, rfl⟩ + exact ⟨rfl, rfl, by intro j hj; omega⟩ + | succ n ih => + intro x y hmode + have hnext : + nextCouplingMode (couplingCore source start A (.ordered a b) n).mode + (σ.getD (start + n) 0) (source.evict (start + n)) + (couplingCore source start A (.ordered a b) (n + 1)).cache + (source.cache (start + n + 1)) = .ordered x y := by + simpa using hmode + rcases nextCouplingMode_eq_ordered hnext with ⟨hprev, hrequest⟩ + rcases ih x y hprev with ⟨hx, hy, hdeadline⟩ + refine ⟨hx, hy, ?_⟩ + intro j hj + have hnle := hdeadline j hj + by_contra hnot + have hnj : n = j := by omega + subst j + have hgeta := getD_eq_nextUse hj + exact hrequest (hgeta.trans hx.symm) + +/-- At every in-range ordered step, the source-only page is not requested. -/ +lemma couplingCore_ordered_safe (source : LegalTrace C₀ σ) (start : ℕ) + (A : Finset Page) (a b : Page) (hdiff : OnePageDiff A (source.cache start) a b) + (hfarther : Farther (nextUse σ start b) (nextUse σ start a)) + (n : ℕ) (hbound : start + n < σ.length) : + OrderedSafe (couplingCore source start A (.ordered a b) n).mode + (σ.getD (start + n) 0) := by + cases hmode : (couplingCore source start A (.ordered a b) n).mode with + | same => simp [OrderedSafe] + | credited x y => simp [OrderedSafe] + | ordered x y => + rcases couplingCore_ordered_deadline source start A a b n x y hmode with + ⟨hx, hy, hdeadline⟩ + subst x + subst y + simpa [OrderedSafe, hmode] using + getD_ne_farther_until hdiff.ne hfarther hbound hdeadline + +@[simp] lemma couplingMisses_zero (source : LegalTrace C₀ σ) (start : ℕ) + (A : Finset Page) (mode : CouplingMode) : + couplingMisses source start A mode 0 = 0 := by + simp [couplingMisses] + +lemma couplingMisses_succ (source : LegalTrace C₀ σ) (start : ℕ) + (A : Finset Page) (mode : CouplingMode) (n : ℕ) : + couplingMisses source start A mode (n + 1) = + couplingMisses source start A mode n + + faultInCache (couplingCore source start A mode n).cache + (σ.getD (start + n) 0) := by + simp [couplingMisses, Finset.sum_range_succ] + +@[simp] lemma traceMissesFrom_zero (T : LegalTrace C₀ σ) (start : ℕ) : + traceMissesFrom T start 0 = 0 := by + simp [traceMissesFrom, cacheMissesFrom] + +lemma traceMissesFrom_succ (T : LegalTrace C₀ σ) (start n : ℕ) : + traceMissesFrom T start (n + 1) = + traceMissesFrom T start n + + faultInCache (T.cache (start + n)) (σ.getD (start + n) 0) := by + simp [traceMissesFrom, cacheMissesFrom, cacheFaultAt, Finset.sum_range_succ] + +/-- The recursive suffix maintains the local miss-accounting invariant. -/ +lemma couplingCore_accounting (source : LegalTrace C₀ σ) (start : ℕ) + (A : Finset Page) (a b : Page) (hdiff : OnePageDiff A (source.cache start) a b) + (hfarther : Farther (nextUse σ start b) (nextUse σ start a)) + (n : ℕ) (hbound : start + n ≤ σ.length) : + AccountingRel (couplingCore source start A (.ordered a b) n).mode + (couplingMisses source start A (.ordered a b) n) + (traceMissesFrom source start n) := by + induction n with + | zero => simp [couplingCore, AccountingRel] + | succ n ih => + have hlt : start + n < σ.length := by omega + have hprev : start + n ≤ σ.length := by omega + have haccount := ih hprev + have hrel := couplingCore_modeRel source start A a b hdiff n hprev + have hsource : σ.getD (start + n) 0 ∉ source.cache (start + n) → + source.evict (start + n) ∈ source.cache (start + n) := + source.evict_mem (start + n) hlt + have hsafe := couplingCore_ordered_safe source start A a b hdiff hfarther n hlt + have hstep := accounting_step + (couplingCore source start A (.ordered a b) n).mode + (couplingCore source start A (.ordered a b) n).cache + (source.cache (start + n)) (source.evict (start + n)) + (σ.getD (start + n) 0) + (couplingMisses source start A (.ordered a b) n) + (traceMissesFrom source start n) hrel hsource hsafe haccount + have hsourceStep : source.cache (start + n + 1) = + traceStepCache (source.cache (start + n)) (source.evict (start + n)) + (σ.getD (start + n) 0) := by + simpa [traceStepCache] using source.step (start + n) hlt + rw [couplingMisses_succ, traceMissesFrom_succ] + rw [couplingCore_mode_succ, couplingCore_cache_succ] + rw [hsourceStep, couplingCore_evict_eq] + exact hstep + +lemma AccountingRel.le {mode : CouplingMode} {transformed source : ℕ} + (h : AccountingRel mode transformed source) : transformed ≤ source := by + cases mode <;> simp only [AccountingRel] at h <;> omega + +/-- The recursive transformed suffix has no more misses than the source suffix. -/ +lemma couplingMisses_le (source : LegalTrace C₀ σ) (start : ℕ) + (A : Finset Page) (a b : Page) (hdiff : OnePageDiff A (source.cache start) a b) + (hfarther : Farther (nextUse σ start b) (nextUse σ start a)) + (count : ℕ) (hbound : start + count ≤ σ.length) : + couplingMisses source start A (.ordered a b) count ≤ + traceMissesFrom source start count := + (couplingCore_accounting source start A a b hdiff hfarther count hbound).le + +/-! Focused executable checks for the three critical coupling branches. -/ + +example : + traceStepCache ({1, 3} : Finset Page) + (coupledEvict (.ordered 1 2) {1, 3} {2, 3} 2 4) 4 = + traceStepCache ({2, 3} : Finset Page) 2 4 := by + have hdiff : OnePageDiff ({1, 3} : Finset Page) {2, 3} 1 2 := by + simp [OnePageDiff] + simp [coupledEvict, traceStepCache, hdiff.erase_eq] + +example : OnePageDiff + ({1, 3} : Finset Page) + (traceStepCache ({2, 3} : Finset Page) 3 1) 3 2 := by + have hdiff : OnePageDiff ({1, 3} : Finset Page) {2, 3} 1 2 := by + simp [OnePageDiff] + simpa [traceStepCache] using hdiff.hit_left_fault 3 (by decide) (by decide) + +example : + traceStepCache ({1, 3} : Finset Page) + (coupledEvict (.credited 1 2) {1, 3} {2, 3} 0 2) 2 = + ({2, 3} : Finset Page) := by + have hdiff : OnePageDiff ({1, 3} : Finset Page) {2, 3} 1 2 := by + simp [OnePageDiff] + change insert 2 (({1, 3} : Finset Page).erase 1) = ({2, 3} : Finset Page) + exact hdiff.insert_right_erase_left + +lemma coupledCache_of_le (source : LegalTrace C₀ σ) (start : ℕ) + (A : Finset Page) (mode : CouplingMode) (s : ℕ) (hs : start ≤ s) : + coupledCache source start A mode s = + (couplingCore source start A mode (s - start)).cache := by + simp [coupledCache, Nat.not_lt.mpr hs] + +/-- Package the boundary-aware splice as a legal trace. -/ +def coupledLegalTrace (source : LegalTrace C₀ σ) (start : ℕ) + (hstartPos : 0 < start) (_hstart : start ≤ σ.length) + (A : Finset Page) (boundaryEvict a b : Page) + (hboundaryMem : + σ.getD (start - 1) 0 ∉ source.cache (start - 1) → + boundaryEvict ∈ source.cache (start - 1)) + (hboundaryStep : + A = traceStepCache (source.cache (start - 1)) boundaryEvict + (σ.getD (start - 1) 0)) + (hdiff : OnePageDiff A (source.cache start) a b) : + LegalTrace C₀ σ where + cache := coupledCache source start A (.ordered a b) + evict := coupledTraceEvict source start boundaryEvict A (.ordered a b) + init := by + rw [coupledCache_of_lt source start A (.ordered a b) 0 hstartPos] + exact source.init + step := by + intro t ht + change coupledCache source start A (.ordered a b) (t + 1) = + traceStepCache (coupledCache source start A (.ordered a b) t) + (coupledTraceEvict source start boundaryEvict A (.ordered a b) t) + (σ.getD t 0) + by_cases hprefix : t + 1 < start + · have htstart : t < start := by omega + simpa [coupledCache, coupledTraceEvict, hprefix, htstart, traceStepCache] using + source.step t ht + · by_cases hboundary : t + 1 = start + · have htEq : t = start - 1 := by omega + subst t + have hminus : start - 1 + 1 = start := by omega + have hltprev : start - 1 < start := by omega + simpa [coupledCache, coupledTraceEvict, hminus, hltprev] using hboundaryStep + · have htge : start ≤ t := by omega + have hsuccge : start ≤ t + 1 := by omega + have hsubsucc : (t + 1) - start = (t - start) + 1 := by omega + have habsolute : start + (t - start) = t := by omega + rw [coupledCache_of_le source start A (.ordered a b) t htge] + rw [coupledCache_of_le source start A (.ordered a b) (t + 1) hsuccge] + have hevict : + coupledTraceEvict source start boundaryEvict A (.ordered a b) t = + (couplingCore source start A (.ordered a b) (t - start)).evict := by + simp [coupledTraceEvict, hprefix, hboundary] + rw [hevict, hsubsucc, couplingCore_cache_succ, habsolute] + evict_mem := by + intro t ht hmiss + by_cases hprefix : t + 1 < start + · have htstart : t < start := by omega + have hmissSource : σ.getD t 0 ∉ source.cache t := by + simpa [coupledCache, htstart] using hmiss + simpa [coupledCache, coupledTraceEvict, hprefix, htstart] using + source.evict_mem t ht hmissSource + · by_cases hboundary : t + 1 = start + · have htEq : t = start - 1 := by omega + subst t + have hminus : start - 1 + 1 = start := by omega + have hltprev : start - 1 < start := by omega + have hmissSource : + σ.getD (start - 1) 0 ∉ source.cache (start - 1) := by + simpa [coupledCache, hltprev] using hmiss + simpa [coupledCache, coupledTraceEvict, hminus, hltprev] using + hboundaryMem hmissSource + · have htge : start ≤ t := by omega + have habsolute : start + (t - start) = t := by omega + have hmissCore : σ.getD (start + (t - start)) 0 ∉ + (couplingCore source start A (.ordered a b) (t - start)).cache := by + simpa [habsolute, coupledCache, Nat.not_lt.mpr htge] using hmiss + have hcore := couplingCore_evict_mem source start A a b hdiff (t - start) + (by simpa [habsolute] using ht) hmissCore + simpa [coupledCache, coupledTraceEvict, Nat.not_lt.mpr htge, + hprefix, hboundary] using hcore + +/-- Split a legal trace's total misses into a prefix and a shifted suffix. -/ +lemma traceMisses_split (T : LegalTrace C₀ σ) (start : ℕ) + (hstart : start ≤ σ.length) : + traceMisses T = + traceMissesFrom T 0 start + + traceMissesFrom T start (σ.length - start) := by + unfold traceMisses traceMissesFrom cacheMissesFrom cacheFaultAt traceFaultAt + rw [show σ.length = start + (σ.length - start) by omega] + rw [Finset.sum_range_add] + simp [faultInCache] + +/-- Suffix miss counts agree when the boundary caches agree pointwise. -/ +lemma traceMissesFrom_congr (T U : LegalTrace C₀ σ) (start count : ℕ) + (hcache : ∀ n, n < count → T.cache (start + n) = U.cache (start + n)) : + traceMissesFrom T start count = traceMissesFrom U start count := by + unfold traceMissesFrom cacheMissesFrom + apply Finset.sum_congr rfl + intro n hn + unfold cacheFaultAt + rw [hcache n (Finset.mem_range.mp hn)] + +/-- The splice has the same strict-prefix miss count as the source. -/ +lemma coupledLegalTrace_prefix_misses + (source : LegalTrace C₀ σ) (start : ℕ) + (hstartPos : 0 < start) (hstart : start ≤ σ.length) + (A : Finset Page) (boundaryEvict a b : Page) + (hboundaryMem : + σ.getD (start - 1) 0 ∉ source.cache (start - 1) → + boundaryEvict ∈ source.cache (start - 1)) + (hboundaryStep : + A = traceStepCache (source.cache (start - 1)) boundaryEvict + (σ.getD (start - 1) 0)) + (hdiff : OnePageDiff A (source.cache start) a b) : + traceMissesFrom + (coupledLegalTrace source start hstartPos hstart A boundaryEvict a b + hboundaryMem hboundaryStep hdiff) + 0 start = + traceMissesFrom source 0 start := by + apply traceMissesFrom_congr + intro n hn + change coupledCache source start A (.ordered a b) (0 + n) = source.cache (0 + n) + simpa using coupledCache_of_lt source start A (.ordered a b) n hn + +/-- The splice's shifted suffix miss count is the recursive core miss count. -/ +lemma coupledLegalTrace_suffix_misses + (source : LegalTrace C₀ σ) (start : ℕ) + (hstartPos : 0 < start) (hstart : start ≤ σ.length) + (A : Finset Page) (boundaryEvict a b : Page) + (hboundaryMem : + σ.getD (start - 1) 0 ∉ source.cache (start - 1) → + boundaryEvict ∈ source.cache (start - 1)) + (hboundaryStep : + A = traceStepCache (source.cache (start - 1)) boundaryEvict + (σ.getD (start - 1) 0)) + (hdiff : OnePageDiff A (source.cache start) a b) + (count : ℕ) : + traceMissesFrom + (coupledLegalTrace source start hstartPos hstart A boundaryEvict a b + hboundaryMem hboundaryStep hdiff) + start count = + couplingMisses source start A (.ordered a b) count := by + unfold traceMissesFrom cacheMissesFrom couplingMisses + apply Finset.sum_congr rfl + intro n hn + unfold cacheFaultAt + change faultInCache (coupledCache source start A (.ordered a b) (start + n)) + (σ.getD (start + n) 0) = + faultInCache (couplingCore source start A (.ordered a b) n).cache + (σ.getD (start + n) 0) + rw [coupledCache_of_le source start A (.ordered a b) (start + n) (by omega)] + simp + +/-- +Boundary-aware ordered/credited coupling constructs a legal full trace and +does not increase total misses. +-/ +theorem exists_coupled_suffix + (source : LegalTrace C₀ σ) (start : ℕ) + (hstartPos : 0 < start) (hstart : start ≤ σ.length) + (A : Finset Page) (boundaryEvict a b : Page) + (hboundaryMem : + σ.getD (start - 1) 0 ∉ source.cache (start - 1) → + boundaryEvict ∈ source.cache (start - 1)) + (hboundaryStep : + A = traceStepCache (source.cache (start - 1)) boundaryEvict + (σ.getD (start - 1) 0)) + (hdiff : OnePageDiff A (source.cache start) a b) + (hfarther : Farther (nextUse σ start b) (nextUse σ start a)) : + ∃ transformed : LegalTrace C₀ σ, + (∀ s, s < start → transformed.cache s = source.cache s) ∧ + transformed.cache start = A ∧ + traceMisses transformed ≤ traceMisses source := by + let transformed := coupledLegalTrace source start hstartPos hstart A boundaryEvict a b + hboundaryMem hboundaryStep hdiff + refine ⟨transformed, ?_, ?_, ?_⟩ + · intro s hs + exact coupledCache_of_lt source start A (.ordered a b) s hs + · exact coupledCache_start source start A (.ordered a b) + · have hprefix := coupledLegalTrace_prefix_misses source start hstartPos hstart + A boundaryEvict a b hboundaryMem hboundaryStep hdiff + have hsuffixEq := coupledLegalTrace_suffix_misses source start hstartPos hstart + A boundaryEvict a b hboundaryMem hboundaryStep hdiff (σ.length - start) + have hbound : start + (σ.length - start) ≤ σ.length := by omega + have hsuffix := couplingMisses_le source start A a b hdiff hfarther + (σ.length - start) hbound + calc + traceMisses transformed = + traceMissesFrom transformed 0 start + + traceMissesFrom transformed start (σ.length - start) := + traceMisses_split transformed start hstart + _ = traceMissesFrom source 0 start + + couplingMisses source start A (.ordered a b) (σ.length - start) := by + rw [hprefix, hsuffixEq] + _ ≤ traceMissesFrom source 0 start + + traceMissesFrom source start (σ.length - start) := + Nat.add_le_add_left hsuffix _ + _ = traceMisses source := (traceMisses_split source start hstart).symm + +end Caching + +end CLRS From bf9ce6a0b242e42e2cbda2b494d7177a143307dd Mon Sep 17 00:00:00 2001 From: TankTechnology <2541826291@qq.com> Date: Wed, 12 Aug 2026 18:40:23 +0800 Subject: [PATCH 05/11] feat(ch15): prove one-step FIF trace exchange --- .../Dev/Trace/A2_OnePageDiff.lean | 23 ++++ .../Dev/Trace/A5_Exchange.lean | 101 ++++++++++++++++++ 2 files changed, 124 insertions(+) create mode 100644 CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A5_Exchange.lean diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A2_OnePageDiff.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A2_OnePageDiff.lean index de461bdd..41d32542 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A2_OnePageDiff.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A2_OnePageDiff.lean @@ -149,6 +149,29 @@ lemma fault_common (h : OnePageDiff A B a b) (x r : Page) · intro hr exact hrB (Finset.mem_erase.mp hr).2 +/-- +Loading the same absent request after evicting distinct residents produces an +exact one-page difference: the first cache keeps `q`, the second keeps `p`. +-/ +lemma of_common_fault {C : Finset Page} {request p q : Page} + (hrequest : request ∉ C) (hp : p ∈ C) (hq : q ∈ C) (hqp : q ≠ p) : + OnePageDiff (insert request (C.erase p)) (insert request (C.erase q)) q p := by + have hqr : q ≠ request := by + intro h + subst q + exact hrequest hq + have hpr : p ≠ request := by + intro h + subst p + exact hrequest hp + refine ⟨?_, ?_, ?_, ?_, ?_⟩ + · exact Finset.mem_insert_of_mem (Finset.mem_erase.mpr ⟨hqp, hq⟩) + · simp [hqr] + · simp [hpr] + · exact Finset.mem_insert_of_mem (Finset.mem_erase.mpr ⟨hqp.symm, hp⟩) + · rw [Finset.erase_insert_of_ne hqr.symm, Finset.erase_insert_of_ne hpr.symm] + rw [Finset.erase_right_comm] + end OnePageDiff end Caching diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A5_Exchange.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A5_Exchange.lean new file mode 100644 index 00000000..5c703d90 --- /dev/null +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A5_Exchange.lean @@ -0,0 +1,101 @@ +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Trace.A4_CouplingCorrect + +/-! +# Chapter 15.4 development: one-step FIF exchange + +At the first transition where a legal trace differs from farthest-in-future, +replace that eviction and couple the remaining suffix without increasing +misses. +-/ + +namespace CLRS + +open Finset + +namespace Caching + +/-- Agreement of cache boundaries with farthest-in-future through `n`. -/ +def TraceAgreesWithFIF (T : LegalTrace C₀ σ) (n : ℕ) : Prop := + ∀ s, s ≤ n → T.cache s = cacheSeq (fifoPolicy σ) C₀ σ s + +/-- One local exchange extends FIF agreement by one boundary without more misses. -/ +theorem exchange_trace + (T : LegalTrace C₀ σ) (t : ℕ) (ht : t < σ.length) + (hagree : TraceAgreesWithFIF T t) + (hdis : T.cache (t + 1) ≠ cacheSeq (fifoPolicy σ) C₀ σ (t + 1)) : + ∃ T' : LegalTrace C₀ σ, + TraceAgreesWithFIF T' (t + 1) ∧ + traceMisses T' ≤ traceMisses T := by + have hpre : T.cache t = cacheSeq (fifoPolicy σ) C₀ σ t := hagree t (by omega) + have hmiss : σ.getD t 0 ∉ T.cache t := by + intro hmem + have hTnext := T.cache_succ_of_mem t ht hmem + have hFmem : σ.getD t 0 ∈ cacheSeq (fifoPolicy σ) C₀ σ t := by + rw [← hpre] + exact hmem + have hFnext : cacheSeq (fifoPolicy σ) C₀ σ (t + 1) = + cacheSeq (fifoPolicy σ) C₀ σ t := by + change (fifoPolicy σ).step t (cacheSeq (fifoPolicy σ) C₀ σ t) + (σ.getD t 0) = cacheSeq (fifoPolicy σ) C₀ σ t + exact fifo_step_of_mem σ t _ _ hFmem + apply hdis + calc + T.cache (t + 1) = T.cache t := hTnext + _ = cacheSeq (fifoPolicy σ) C₀ σ t := hpre + _ = cacheSeq (fifoPolicy σ) C₀ σ (t + 1) := hFnext.symm + + let q : Page := T.evict t + let p : Page := farthestInFuture (T.cache t) σ t + have hq : q ∈ T.cache t := T.evict_mem t ht hmiss + have hnonempty : (T.cache t).Nonempty := ⟨q, hq⟩ + have hp : p ∈ T.cache t := mem_farthestInFuture hnonempty + have hTnext : T.cache (t + 1) = + insert (σ.getD t 0) ((T.cache t).erase q) := by + simpa [q] using T.cache_succ_of_not_mem t ht hmiss + have hFnext : cacheSeq (fifoPolicy σ) C₀ σ (t + 1) = + insert (σ.getD t 0) ((T.cache t).erase p) := by + change (fifoPolicy σ).step t (cacheSeq (fifoPolicy σ) C₀ σ t) + (σ.getD t 0) = _ + rw [← hpre] + simpa [p] using fifo_step_fault σ t (T.cache t) (σ.getD t 0) hmiss + have hqp : q ≠ p := by + intro hqp + apply hdis + rw [hTnext, hFnext, hqp] + have hdiff : OnePageDiff + (cacheSeq (fifoPolicy σ) C₀ σ (t + 1)) (T.cache (t + 1)) q p := by + rw [hFnext, hTnext] + exact OnePageDiff.of_common_fault hmiss hp hq hqp + have hfarther : + Farther (nextUse σ (t + 1) p) (nextUse σ (t + 1) q) := by + simpa [p] using farthestInFuture_max (σ := σ) (i := t) (p := q) hq + have hsub : t + 1 - 1 = t := by omega + have hboundaryMem : + σ.getD (t + 1 - 1) 0 ∉ T.cache (t + 1 - 1) → + p ∈ T.cache (t + 1 - 1) := by + simpa [hsub] using fun _ : σ.getD t 0 ∉ T.cache t => hp + have hboundaryStep : + cacheSeq (fifoPolicy σ) C₀ σ (t + 1) = + traceStepCache (T.cache (t + 1 - 1)) p (σ.getD (t + 1 - 1) 0) := by + rw [hsub, hFnext] + unfold traceStepCache + split + · contradiction + · rfl + rcases exists_coupled_suffix T (t + 1) (by omega) (by omega) + (cacheSeq (fifoPolicy σ) C₀ σ (t + 1)) p q p + hboundaryMem hboundaryStep hdiff hfarther with + ⟨T', hprefix, hstartCache, hmisses⟩ + refine ⟨T', ?_, hmisses⟩ + intro s hs + by_cases hsend : s = t + 1 + · subst s + exact hstartCache + · have hslt : s < t + 1 := by omega + calc + T'.cache s = T.cache s := hprefix s hslt + _ = cacheSeq (fifoPolicy σ) C₀ σ s := hagree s (by omega) + +end Caching + +end CLRS From 1d6500a13b3e5ec235802f7c42488cc07b729d47 Mon Sep 17 00:00:00 2001 From: TankTechnology <2541826291@qq.com> Date: Wed, 12 Aug 2026 18:42:21 +0800 Subject: [PATCH 06/11] feat(ch15): close FIF optimality via finite trace exchange --- .../Dev/Trace/A6_Iteration.lean | 86 +++++++++++++++++++ 1 file changed, 86 insertions(+) create mode 100644 CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A6_Iteration.lean diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A6_Iteration.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A6_Iteration.lean new file mode 100644 index 00000000..b922d7e0 --- /dev/null +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A6_Iteration.lean @@ -0,0 +1,86 @@ +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Trace.A5_Exchange + +/-! +# Chapter 15.4 development: finite exchange iteration + +Repeatedly extend agreement by one request boundary. The remaining number of +boundaries is the sole termination measure. +-/ + +namespace CLRS + +open Finset +open scoped BigOperators + +namespace Caching + +/-- Full cache-boundary agreement with FIF gives exactly the FIF miss count. -/ +lemma traceMisses_eq_fifo_of_agree + (T : LegalTrace C₀ σ) + (hagree : TraceAgreesWithFIF T σ.length) : + traceMisses T = misses (fifoPolicy σ) C₀ σ := by + unfold traceMisses misses traceFaultAt faultAt + apply Finset.sum_congr rfl + intro t ht + rw [hagree t (by + have := Finset.mem_range.mp ht + omega)] + +/-- Complete FIF agreement when `k` request boundaries remain. -/ +lemma exists_fully_agreeing_trace_aux + (k n : ℕ) (hkn : n + k = σ.length) + (T : LegalTrace C₀ σ) (hagree : TraceAgreesWithFIF T n) : + ∃ T' : LegalTrace C₀ σ, + TraceAgreesWithFIF T' σ.length ∧ + traceMisses T' ≤ traceMisses T := by + induction k generalizing n T with + | zero => + have hn : n = σ.length := by omega + refine ⟨T, ?_, le_rfl⟩ + simpa [hn] using hagree + | succ k ih => + have hnlt : n < σ.length := by omega + by_cases hnext : + T.cache (n + 1) = cacheSeq (fifoPolicy σ) C₀ σ (n + 1) + · have hagreeNext : TraceAgreesWithFIF T (n + 1) := by + intro s hs + by_cases hsn : s = n + 1 + · subst s + exact hnext + · exact hagree s (by omega) + exact ih (n + 1) (by omega) T hagreeNext + · rcases exchange_trace T n hnlt hagree hnext with + ⟨T₁, hagree₁, hmiss₁⟩ + rcases ih (n + 1) (by omega) T₁ hagree₁ with + ⟨T₂, hagree₂, hmiss₂⟩ + exact ⟨T₂, hagree₂, Nat.le_trans hmiss₂ hmiss₁⟩ + +/-- Every legal trace can be exchanged into a fully FIF-agreeing trace. -/ +theorem exists_fully_agreeing_trace (T : LegalTrace C₀ σ) : + ∃ T' : LegalTrace C₀ σ, + TraceAgreesWithFIF T' σ.length ∧ + traceMisses T' ≤ traceMisses T := by + have hagreeZero : TraceAgreesWithFIF T 0 := by + intro s hs + have hs0 : s = 0 := by omega + subst s + change T.cache 0 = C₀ + exact T.init + exact exists_fully_agreeing_trace_aux σ.length 0 (by simp) T hagreeZero + +/-- Development theorem: farthest-in-future is optimal among all policies. -/ +theorem fifo_optimal_trace + (π : Policy) (C₀ : Finset Page) (σ : List Page) + (hC₀ : C₀.Nonempty) : + misses (fifoPolicy σ) C₀ σ ≤ misses π C₀ σ := by + rcases exists_fully_agreeing_trace (policyTrace π C₀ σ hC₀) with + ⟨T, hagree, hmisses⟩ + calc + misses (fifoPolicy σ) C₀ σ = traceMisses T := + (traceMisses_eq_fifo_of_agree T hagree).symm + _ ≤ traceMisses (policyTrace π C₀ σ hC₀) := hmisses + _ = misses π C₀ σ := traceMisses_policyTrace π C₀ σ hC₀ + +end Caching + +end CLRS From f3c3ca10d20444a49b1602dc3b91f86006b1b289 Mon Sep 17 00:00:00 2001 From: TankTechnology <2541826291@qq.com> Date: Wed, 12 Aug 2026 18:46:51 +0800 Subject: [PATCH 07/11] feat(ch15): publish unconditional FIF optimality theorem --- .../Trace/A1_LegalTrace.lean | 0 .../Trace/A2_OnePageDiff.lean | 2 +- .../Trace/A3_CouplingCore.lean | 2 +- .../Trace/A4_CouplingCorrect.lean | 2 +- .../Trace/A5_Exchange.lean | 2 +- .../Trace/A6_Iteration.lean | 2 +- .../S3_Optimality.lean | 35 ++++++++----------- 7 files changed, 19 insertions(+), 26 deletions(-) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/{Dev => Optimality}/Trace/A1_LegalTrace.lean (100%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/{Dev => Optimality}/Trace/A2_OnePageDiff.lean (99%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/{Dev => Optimality}/Trace/A3_CouplingCore.lean (99%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/{Dev => Optimality}/Trace/A4_CouplingCorrect.lean (99%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/{Dev => Optimality}/Trace/A5_Exchange.lean (98%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/{Dev => Optimality}/Trace/A6_Iteration.lean (98%) diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A1_LegalTrace.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A1_LegalTrace.lean similarity index 100% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A1_LegalTrace.lean rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A1_LegalTrace.lean diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A2_OnePageDiff.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A2_OnePageDiff.lean similarity index 99% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A2_OnePageDiff.lean rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A2_OnePageDiff.lean index 41d32542..384ee68f 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A2_OnePageDiff.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A2_OnePageDiff.lean @@ -1,4 +1,4 @@ -import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Trace.A1_LegalTrace +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A1_LegalTrace /-! # Chapter 15.4 development: exact one-page cache difference diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A3_CouplingCore.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A3_CouplingCore.lean similarity index 99% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A3_CouplingCore.lean rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A3_CouplingCore.lean index a00572c2..ece7d73a 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A3_CouplingCore.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A3_CouplingCore.lean @@ -1,4 +1,4 @@ -import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Trace.A2_OnePageDiff +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A2_OnePageDiff /-! # Chapter 15.4 development: recursive coupling core diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A4_CouplingCorrect.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A4_CouplingCorrect.lean similarity index 99% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A4_CouplingCorrect.lean rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A4_CouplingCorrect.lean index b8f1c88a..91c09e26 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A4_CouplingCorrect.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A4_CouplingCorrect.lean @@ -1,4 +1,4 @@ -import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Trace.A3_CouplingCore +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A3_CouplingCore /-! # Chapter 15.4 development: coupling correctness diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A5_Exchange.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A5_Exchange.lean similarity index 98% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A5_Exchange.lean rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A5_Exchange.lean index 5c703d90..69f07cde 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A5_Exchange.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A5_Exchange.lean @@ -1,4 +1,4 @@ -import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Trace.A4_CouplingCorrect +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A4_CouplingCorrect /-! # Chapter 15.4 development: one-step FIF exchange diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A6_Iteration.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A6_Iteration.lean similarity index 98% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A6_Iteration.lean rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A6_Iteration.lean index b922d7e0..9a38bc18 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Trace/A6_Iteration.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A6_Iteration.lean @@ -1,4 +1,4 @@ -import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Trace.A5_Exchange +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A5_Exchange /-! # Chapter 15.4 development: finite exchange iteration diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality.lean index fa78ba4e..8ea69884 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality.lean @@ -1,5 +1,6 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S1_Cache_Model import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S2_Farthest_In_Future +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A6_Iteration /-! # S3. Optimality of the farthest-in-future policy @@ -11,6 +12,7 @@ the cache size. Main results: +- `fifo_optimal`: no offline eviction policy incurs fewer misses than FIF - `fifo_evicts_resident`: the FIF policy evicts a resident page - `fifo_step_size`: a FIF step preserves the cache size - `schedCache` / `schedMisses`: the run and miss count of an arbitrary @@ -57,27 +59,8 @@ Main results: Current gaps: -- The optimality theorem (`fifo_optimal`: no eviction policy — even offline — - has fewer misses than the farthest-in-future policy, CLRS Theorem 15.5) - remains to be formalized. The iteration machinery is in place: - `exchange_step` shows that exchanging the first disagreement of a schedule - reduced from that position on never increases misses and extends agreement - with the farthest-in-future policy by one position, and - `exchangeSchedule_reduced_after` shows the reducedness state (reduced at - every fault after a bound `hnb`) is preserved by the exchange (with the - bound growing to `max hnb J'`). The remaining work is the iteration - assembly: repeatedly exchanging at the first disagreement while the - schedule is reduced from there on produces a schedule agreeing with the - policy everywhere with no more misses. The pieces are in place — - `exchange_step` (never increases misses, extends agreement), the slack - lemma `exchangeSchedule_misses_le_plus_one` (spare miss when the bad event - did not occur), and the repair step `repair_step` (replacing a no-op - eviction at or before the reducedness bound by the policy's choice costs - at most one extra miss, paid by the slack) — so the remaining work is the - iteration state machine: tracking the reducedness bound, the previous - `q'`/`J'` and the accumulated slack, choosing between the exchange and the - repair at each first disagreement, and the boundary case where the first - disagreement lands exactly on the previous `q'` request. +- None for optimality in the mathematical cache model. Low-level RAM/cache + implementation refinement is outside this section's current model. -/ namespace CLRS @@ -2980,6 +2963,16 @@ lemma repairSchedule_window_swap' (e : ℕ → Page) (σ : List Page) (C₀ : Fi · exact repairSchedule_step_swap' e σ C₀ hC₀ ht hagree hdis hqin hq' hq hj hj' hjj' s ih (by omega) (by omega) +/-- +The farthest-in-future policy is optimal among all offline eviction policies +for a nonempty initial cache (CLRS Theorem 15.5). +-/ +theorem fifo_optimal + (π : Policy) (C₀ : Finset Page) (σ : List Page) + (hC₀ : C₀.Nonempty) : + misses (fifoPolicy σ) C₀ σ ≤ misses π C₀ σ := by + exact fifo_optimal_trace π C₀ σ hC₀ + end Caching end CLRS From d4bfa74602cd700a16307e18d494a1b2cbfc73c6 Mon Sep 17 00:00:00 2001 From: TankTechnology <2541826291@qq.com> Date: Wed, 12 Aug 2026 18:55:37 +0800 Subject: [PATCH 08/11] docs(ch15): archive failed optimality proof routes --- .../Dev/Legacy/FAILED_APPROACHES.md | 152 ++++++++++++++++++ .../StateMachine}/B10_CaseOne_Hdred.lean | 2 +- .../StateMachine}/B11_CaseOne_B1.lean | 2 +- .../StateMachine}/B12_CaseOne_NoWindowB1.lean | 2 +- .../StateMachine}/B13_PerPageCredit.lean | 2 +- .../StateMachine}/B14_PerPageHQ.lean | 2 +- .../StateMachine}/B7_Iteration.lean | 8 +- .../{ => Legacy/StateMachine}/B8_HnotE.lean | 2 +- .../StateMachine}/B9_Assembly.lean | 2 +- .../Dev/{ => Legacy/StateMachine}/DESIGN.md | 0 .../{ => Legacy/StateMachine}/search_b2.py | 0 .../StateMachine}/search_caseone.py | 0 .../{ => Legacy/StateMachine}/search_ehit.py | 0 .../{ => Legacy/StateMachine}/search_hnot.py | 0 .../{ => Legacy/StateMachine}/search_hq.py | 0 .../{ => Legacy/StateMachine}/search_iter.py | 0 .../StateMachine}/search_noevict.py | 0 .../{ => Legacy/StateMachine}/search_slack.py | 0 18 files changed, 165 insertions(+), 9 deletions(-) create mode 100644 CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/FAILED_APPROACHES.md rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/{ => Legacy/StateMachine}/B10_CaseOne_Hdred.lean (99%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/{ => Legacy/StateMachine}/B11_CaseOne_B1.lean (99%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/{ => Legacy/StateMachine}/B12_CaseOne_NoWindowB1.lean (99%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/{ => Legacy/StateMachine}/B13_PerPageCredit.lean (99%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/{ => Legacy/StateMachine}/B14_PerPageHQ.lean (99%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/{ => Legacy/StateMachine}/B7_Iteration.lean (99%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/{ => Legacy/StateMachine}/B8_HnotE.lean (99%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/{ => Legacy/StateMachine}/B9_Assembly.lean (99%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/{ => Legacy/StateMachine}/DESIGN.md (100%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/{ => Legacy/StateMachine}/search_b2.py (100%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/{ => Legacy/StateMachine}/search_caseone.py (100%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/{ => Legacy/StateMachine}/search_ehit.py (100%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/{ => Legacy/StateMachine}/search_hnot.py (100%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/{ => Legacy/StateMachine}/search_hq.py (100%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/{ => Legacy/StateMachine}/search_iter.py (100%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/{ => Legacy/StateMachine}/search_noevict.py (100%) rename CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/{ => Legacy/StateMachine}/search_slack.py (100%) diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/FAILED_APPROACHES.md b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/FAILED_APPROACHES.md new file mode 100644 index 00000000..874df0db --- /dev/null +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/FAILED_APPROACHES.md @@ -0,0 +1,152 @@ +# Failed approaches to the Chapter 15.4 optimality proof + +This file is the negative-results ledger for the abandoned schedule-state-machine +proof of farthest-in-future optimality. The archived sources are under +`StateMachine/`; the accepted public proof instead uses legal cache traces and +a local one-page coupling under `Optimality/Trace/`. + +The search counts below refute the stated invariant designs. They are not +claims that every enumerated state is reachable. Explicit theorem interfaces, +concrete counterexamples, and Lean proofs remain the authoritative evidence. + +## 1. Conditional final wrapper (`hB1` / `hB2` / `hAone`) + +- **Attempted invariant.** `IterateState` tracked agreement, reducedness, + natural-number slack, historical page pairs, and repair windows. The B7 + iteration theorem delegated its remaining transitions to three supply + hypotheses `hB1`, `hB2`, and `hAone`. +- **Failure evidence.** The private theorem originally named `fifo_optimal` + (renamed `fifo_optimal_conditional_legacy` during archival) in + `StateMachine/B7_Iteration.lean` accepts all three supplies as arguments. + Kernel checking therefore establishes only a conditional implication, not + CLRS Theorem 15.5. B8--B14 refine pieces of the supplies but never eliminate + the conditional public boundary. +- **Reusable results.** The schedule/cache algebra in S3, first-disagreement + lemmas, exchange/repair transition calculations, exact miss accounting, and + next-use lemmas remain useful mathematical facts. They informed the trace + proof's statement shaping and local transition split. +- **Recurrence-prevention rule.** Completion requires an interface test that + instantiates `CLRS.Caching.fifo_optimal` at the approved unconditional type. + A theorem with any state-machine supply hypothesis cannot pass G4. + +## 2. Full-history `hQ` + +- **Attempted invariant.** Store every historical repair pair in `Q` and + require every live pair's first future request (its nop position) to remain + strictly after the current disagreement. The reverse-difference chain was + then bounded by `Q.image`. +- **Failure evidence.** Once a pair's nop has passed, the strict bound is + arithmetically impossible. `search_hq.py` found 10,236 B1 and 688 B2 steps + with an old nop at or before the step, 212 B1 and 312 B2 boundary cases with + the nop exactly at `t₂ + 1`, and **988 B2 steps entered from an already + broken-`hQ` state**. Pruning expired pairs also loses pages needed by the + reverse-difference chain. +- **Reusable results.** `b2_ehit_ne_per_page`, `last_pair_page_stays`, + `creditedPage`, and `HQPerPageHyp` in `StateMachine/B14_PerPageHQ.lean` + isolate valid consulted-pair and page-stays facts. The reverse-difference + lemmas remain valid with their explicit premises. +- **Recurrence-prevention rule.** Never quantify a future-position bound over + unpruned full history without proving preservation across the boundary where + each stored position expires. Test the extension step, not only consumers + of the invariant. + +## 3. Plain natural-number slack + +- **Attempted invariant.** Maintain + `schedMisses d + slack ≤ initialMisses`, credit an exchange by one when its + bad event does not occur, and pay each B1 repair from the same scalar slack; + the key supply was `bad ≤ slack`. +- **Failure evidence.** Exact enumeration in `search_slack.py` found + **492 negative-slack executions**. A minimal recorded counterexample is + `σ = [1,1,3,2,4,1,2,4]`, `C₀ = {1,2}`, with the largest-resident source: + an A step at 2 produces no credit, a free B2 step occurs at 4, then a real + B1 bad at 5 requires one unit while slack is zero. Of 3,836 B1 bads, 1,040 + are outside the directly covered `q₀'` case and 492 of those have zero + slack. +- **Reusable results.** `b1_exchange_no_bad_q0` and + `b1_bad_le_slack_q0` correctly cover the `d t₂ = q₀'` subcase. + `repair_step_swap_exact_net` and the exact B2 good/bad accounting are also + sound local results. +- **Recurrence-prevention rule.** A global natural-number potential must be + proved nonnegative at every consumer. Aggregate miss inequalities and a + handful of locally credited cases do not establish a supply theorem. + +## 4. Per-page credit and candidate-C credit + +- **Attempted invariant.** Replace scalar slack by pending-good balances per + page, drawing a B1 bad first from the repaired page's balance; a candidate-C + variant sends alive-alive B2 net savings to a global pool. +- **Failure evidence.** The per-page design reduces the 492 failures only to + 336; candidate-C reduces them to **164**, not zero. All 164 residual cases + contain two consecutive B1 bads in one window. The second required page has + no pending good under any identified credit, so the proposed balance can go + negative and no closed global invariant results. +- **Reusable results.** The arithmetic lemmas + `b1_bad_le_slack_credit`, `b1_draw_credit`, `b1_draw_slack`, and + `b2_good_accrues` in `StateMachine/B13_PerPageCredit.lean` are correct under + their explicit supply premises. They document how a future proof could + consume a genuinely established page credit. +- **Recurrence-prevention rule.** A refined credit system is not accepted + until exhaustive transition preservation closes every producer/consumer + case and the initial/final potentials are connected to misses. Reducing a + counterexample count is diagnostic progress, not a proof. + +## 5. Skipping the case-one branch-1 position with `hnb` + +- **Attempted invariant.** After a case-one exchange, raise the reducedness + boundary `hnb'` past the unique branch-1 no-op position, expecting the next + disagreement to occur after that boundary and return to case A. +- **Failure evidence.** `search_caseone.py` found 7,384 branch-1 spots and + zero multiple spots, but in every applicable trace the next disagreement + lands **exactly at the branch-1 spot**, hence below `hnb' = s₁ + 1`. + Example: `σ = [1,1,3,4,1]`, `C₀ = {1,2}`, exchange at 2, spot and next + disagreement at 3. Raising `hnb` relabels the required transition as case + B; it does not remove it. Unbounded junk positions also forced a vacuous + `σ.length + 2` boundary rather than a finite reduced tail. +- **Reusable results.** `case_one_D_minus_E_subset_q'`, + `case_one_exchange_fault_imp_d_fault`, `case_one_branch1_once`, and the + no-window B1 construction in B10--B12 are kernel-checked and precisely + describe this exceptional transition. +- **Recurrence-prevention rule.** A boundary shift is valid only after proving + the next disagreement is on the permitted side. Always test equality at + the proposed boundary; do not infer progress from at-most-once alone. + +## 6. Build-based false completion + +- **Attempted criterion.** Treat absence of `sorry`, kernel checking of every + local file, or a successful repository build as evidence that §15.4 is + complete. +- **Failure evidence.** The legacy tree compiled while the only final wrapper + was private and conditional on `hB1`, `hB2`, and `hAone`; the public section + did not export an unconditional `fifo_optimal`. A build checks declarations + that exist, not the intended theorem that is missing. +- **Reusable results.** Kernel checking and unfinished-marker scans remain + necessary lower-level gates. They become meaningful when combined with a + public interface typecheck and `#print axioms`. +- **Recurrence-prevention rule.** Completion is conjunctive: exact public + theorem type, public import reachability, acceptable axiom report, focused + interface instantiation, and repository checks must all pass freshly. + +## 7. Third-/fourth-edition migration ledger collision + +- **Attempted criterion.** Reuse the existing `Chapter 15` progress row for + the newly migrated §15.4 work without distinguishing editions or source + paths. +- **Failure evidence.** In CLRS third edition, Chapter 15 is Dynamic + Programming; in the fourth edition, Chapter 15 is Greedy Algorithms and + contains offline caching. FIF progress was written into the legacy Dynamic + Programming row, making a status claim that referred to the wrong chapter. +- **Reusable results.** The compatibility map and explicit fourth-edition + module hierarchy provide stable identities during migration. +- **Recurrence-prevention rule.** Every progress entry must name the edition, + chapter title, and canonical source path. Never join migration ledgers by + chapter number alone. + +## Non-mathematical implementation incident + +Deriving `Repr` for a coupling state containing `Finset` triggered a Lean +compiler panic on the project's release-candidate toolchain. The instance was +unused, so removing the derivation restored compilation without changing any +definition or theorem. This was a toolchain/diagnostic-surface issue, not a +failed mathematical route; avoid deriving runtime representations for proof +states unless a test actually needs them. diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B10_CaseOne_Hdred.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B10_CaseOne_Hdred.lean similarity index 99% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B10_CaseOne_Hdred.lean rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B10_CaseOne_Hdred.lean index e65fe814..acf43786 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B10_CaseOne_Hdred.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B10_CaseOne_Hdred.lean @@ -1,4 +1,4 @@ -import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B9_Assembly +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Legacy.StateMachine.B9_Assembly /- # Dev B10: case-one hdred supply diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B11_CaseOne_B1.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B11_CaseOne_B1.lean similarity index 99% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B11_CaseOne_B1.lean rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B11_CaseOne_B1.lean index 30e01f5f..8a8d3b7b 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B11_CaseOne_B1.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B11_CaseOne_B1.lean @@ -1,4 +1,4 @@ -import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B9_Assembly +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Legacy.StateMachine.B9_Assembly /- # Dev B11: the case-one no-window B1 step diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B12_CaseOne_NoWindowB1.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B12_CaseOne_NoWindowB1.lean similarity index 99% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B12_CaseOne_NoWindowB1.lean rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B12_CaseOne_NoWindowB1.lean index ff78027f..0c987343 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B12_CaseOne_NoWindowB1.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B12_CaseOne_NoWindowB1.lean @@ -1,4 +1,4 @@ -import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B11_CaseOne_B1 +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Legacy.StateMachine.B11_CaseOne_B1 /- # Dev B12: the no-window B1 step (case-one assembly) diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B13_PerPageCredit.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B13_PerPageCredit.lean similarity index 99% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B13_PerPageCredit.lean rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B13_PerPageCredit.lean index 78f31dd1..7bad8b43 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B13_PerPageCredit.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B13_PerPageCredit.lean @@ -1,4 +1,4 @@ -import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B12_CaseOne_NoWindowB1 +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Legacy.StateMachine.B12_CaseOne_NoWindowB1 /- # Dev B13: the per-page credit invariant (non-q₀' B1 slack) diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B14_PerPageHQ.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B14_PerPageHQ.lean similarity index 99% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B14_PerPageHQ.lean rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B14_PerPageHQ.lean index 3b7efc35..30ea93cc 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B14_PerPageHQ.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B14_PerPageHQ.lean @@ -1,4 +1,4 @@ -import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B13_PerPageCredit +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Legacy.StateMachine.B13_PerPageCredit /- # Dev B14: the per-page credit invariant — hQ replacement diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B7_Iteration.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B7_Iteration.lean similarity index 99% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B7_Iteration.lean rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B7_Iteration.lean index 9b9172eb..00730f08 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B7_Iteration.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B7_Iteration.lean @@ -3464,8 +3464,12 @@ private lemma iterate_main (σ : List Page) (C₀ : Finset Page) (hC₀ : C₀.N ∃ d' slack', agreeWithFIF d' C₀ σ σ.length ∧ schedMisses d' C₀ σ + slack' ≤ M) (σ.length - st.t0) hmain st rfl - /-- fifo_optimal: CLRS Theorem 15.5 via iterate_main from the initial state (d0, t0=0, slack=0, hnb=0, Q=P=empty, win=none); the hB1/hB2/hAone supplies are hypotheses. -/ - private lemma fifo_optimal (π : Policy) (C₀ : Finset Page) (σ : List Page) + /-- Legacy conditional candidate for CLRS Theorem 15.5 via `iterate_main` from + the initial state. This is deliberately not named `fifo_optimal`: the public + theorem is unconditional, while this archived route still assumes the + `hB1`/`hB2`/`hAone` supplies. -/ + private lemma fifo_optimal_conditional_legacy + (π : Policy) (C₀ : Finset Page) (σ : List Page) (hC₀ : C₀.Nonempty) (hB1 : ∀ (M : ℕ) (st : IterateState σ C₀ M) (t₂ : ℕ) (ht₂ : t₂ < σ.length) (ht₂hnb : t₂ < st.hnb), agreeWithFIF st.d C₀ σ t₂ → diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B8_HnotE.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B8_HnotE.lean similarity index 99% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B8_HnotE.lean rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B8_HnotE.lean index 05d6442e..4245a24f 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B8_HnotE.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B8_HnotE.lean @@ -1,4 +1,4 @@ -import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B7_Iteration +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Legacy.StateMachine.B7_Iteration /-! # Dev B8: the hnotE derivation (Q''-exclusion at window faults) diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B9_Assembly.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B9_Assembly.lean similarity index 99% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B9_Assembly.lean rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B9_Assembly.lean index cf1bd013..ee5b0b5c 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B9_Assembly.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B9_Assembly.lean @@ -1,4 +1,4 @@ -import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B8_HnotE +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Legacy.StateMachine.B8_HnotE /- # Dev B9: the iterate_main assembly (checkpoint) diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/DESIGN.md b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/DESIGN.md similarity index 100% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/DESIGN.md rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/DESIGN.md diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/search_b2.py b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/search_b2.py similarity index 100% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/search_b2.py rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/search_b2.py diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/search_caseone.py b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/search_caseone.py similarity index 100% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/search_caseone.py rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/search_caseone.py diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/search_ehit.py b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/search_ehit.py similarity index 100% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/search_ehit.py rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/search_ehit.py diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/search_hnot.py b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/search_hnot.py similarity index 100% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/search_hnot.py rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/search_hnot.py diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/search_hq.py b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/search_hq.py similarity index 100% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/search_hq.py rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/search_hq.py diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/search_iter.py b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/search_iter.py similarity index 100% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/search_iter.py rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/search_iter.py diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/search_noevict.py b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/search_noevict.py similarity index 100% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/search_noevict.py rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/search_noevict.py diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/search_slack.py b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/search_slack.py similarity index 100% rename from CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/search_slack.py rename to CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/search_slack.py From e95af73a217dd2808959db7a2ea028744e9e1bea Mon Sep 17 00:00:00 2001 From: TankTechnology <2541826291@qq.com> Date: Wed, 12 Aug 2026 19:04:02 +0800 Subject: [PATCH 09/11] docs(ch15): keep proof-marker scan unambiguous --- .../Dev/Legacy/StateMachine/B9_Assembly.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B9_Assembly.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B9_Assembly.lean index ee5b0b5c..f2152ada 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B9_Assembly.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B9_Assembly.lean @@ -7,7 +7,7 @@ The concrete instantiation of `iterate_main`'s abstract case-step supplies `hB1`/`hB2`/`hAone` with the kernel-checked case-step lemmas and the extension glue. The checkpoint wires everything that is proved and leaves the genuinely open pieces as **documented -hypotheses** (referencing `Dev/DESIGN.md`) — no `sorry` (the +hypotheses** (referencing `Dev/DESIGN.md`) — with no unfinished proof placeholder (the repository checker forbids them on `main`): 1. `hQ_open`: the hQ-strictness/extension — the state's `hQ` field From c14b059ddbebf2561e2d20fc261aec84dee5a331 Mon Sep 17 00:00:00 2001 From: TankTechnology <2541826291@qq.com> Date: Wed, 12 Aug 2026 19:06:56 +0800 Subject: [PATCH 10/11] test(ch15): lock the public trace exchange contract --- .../Section_15_4_Offline_Caching/S3_Optimality.lean | 11 ++++++++++- Tests/Chapter_15_4_Interface.lean | 10 ++++++++++ 2 files changed, 20 insertions(+), 1 deletion(-) diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality.lean index 8ea69884..fb7d4ced 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality.lean @@ -8,11 +8,20 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality The exchange-schedule machinery for the optimality proof of the farthest-in-future (Belady) eviction policy of CLRS §15.4, plus basic sanity lemmas for the policy itself: it always evicts a resident page and preserves -the cache size. +the cache size. The unconditional theorem is closed through a separate +policy-independent legal-trace argument: one-page cache differences are +coupled across the suffix, the first disagreement is exchanged without adding +misses, and finite iteration yields a trace that agrees with FIF everywhere. Main results: - `fifo_optimal`: no offline eviction policy incurs fewer misses than FIF +- `LegalTrace` / `traceOfPolicy`: policy-independent legal cache executions and + the trace induced by any policy +- `exchange_trace`: one local exchange extends agreement with FIF by one cache + boundary without increasing total misses +- `exists_fully_agreeing_trace` / `fifo_optimal_trace`: finite iteration of the + exchange and its trace-level optimality consequence - `fifo_evicts_resident`: the FIF policy evicts a resident page - `fifo_step_size`: a FIF step preserves the cache size - `schedCache` / `schedMisses`: the run and miss count of an arbitrary diff --git a/Tests/Chapter_15_4_Interface.lean b/Tests/Chapter_15_4_Interface.lean index a3529be5..1df01df2 100644 --- a/Tests/Chapter_15_4_Interface.lean +++ b/Tests/Chapter_15_4_Interface.lean @@ -6,6 +6,16 @@ namespace CLRS.Caching #check fifo_optimal #print axioms fifo_optimal +#check exchange_trace +#print axioms exchange_trace + +example (T : LegalTrace C₀ σ) (t : ℕ) (ht : t < σ.length) + (hagree : TraceAgreesWithFIF T t) + (hdis : T.cache (t + 1) ≠ cacheSeq (fifoPolicy σ) C₀ σ (t + 1)) : + ∃ T' : LegalTrace C₀ σ, + TraceAgreesWithFIF T' (t + 1) ∧ + traceMisses T' ≤ traceMisses T := by + exact exchange_trace T t ht hagree hdis example (π : Policy) (C₀ : Finset Page) (σ : List Page) (hC₀ : C₀.Nonempty) : From 06cf2985618020b891c894082b73c888c56fb49e Mon Sep 17 00:00:00 2001 From: TankTechnology <2541826291@qq.com> Date: Fri, 14 Aug 2026 10:12:21 +0800 Subject: [PATCH 11/11] docs(ch15): reconcile trace optimality completion --- CLRSLean/FourthEdition/Chapter_15.lean | 10 ++- .../Section_15_4_Offline_Caching.lean | 24 +++++-- .../Dev/B3_AfterJ_Window.lean | 3 +- .../Dev/B4_Repair_Swap_Count.lean | 2 +- .../Dev/B5_Iteration.lean | 2 +- .../Dev/B6_Strong_Repair.lean | 2 +- .../Dev/Legacy/StateMachine/B7_Iteration.lean | 8 +-- .../Dev/Legacy/StateMachine/B9_Assembly.lean | 2 +- .../Optimality.lean | 13 ++++ .../Optimality/Trace.lean | 18 +++++ .../Optimality/Trace/A1_LegalTrace.lean | 2 +- .../Optimality/Trace/A2_OnePageDiff.lean | 2 +- .../Optimality/Trace/A3_CouplingCore.lean | 2 +- .../Optimality/Trace/A4_CouplingCorrect.lean | 2 +- .../Optimality/Trace/A5_Exchange.lean | 2 +- .../Optimality/Trace/A6_Iteration.lean | 2 +- .../S3_Optimality.lean | 4 +- CLRSLean/Progress.lean | 8 +-- CLRSLean/Status.lean | 5 +- README.md | 2 +- docs/clrs-fourth-edition-map.csv | 8 +-- docs/clrs-proof-progress.csv | 3 +- docs/index.md | 8 +++ docs/migrations/clrs4.md | 2 +- docs/proof-map.md | 70 ++++++++----------- .../2026-08-08-fifo-optimality-design.md | 7 +- ...026-08-12-ch15-4-fifo-optimality-design.md | 7 ++ literate.toml | 36 ++++++++++ 28 files changed, 175 insertions(+), 81 deletions(-) create mode 100644 CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality.lean create mode 100644 CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace.lean diff --git a/CLRSLean/FourthEdition/Chapter_15.lean b/CLRSLean/FourthEdition/Chapter_15.lean index 27b07c2b..bc3f89a2 100644 --- a/CLRSLean/FourthEdition/Chapter_15.lean +++ b/CLRSLean/FourthEdition/Chapter_15.lean @@ -26,8 +26,10 @@ these sources during the compatibility period. ## Coverage boundary -Section 15.4 (offline caching) is a native fourth-edition section (the -farthest-in-future eviction policy; the optimality theorem remains a gap), +Section 15.4 (offline caching) is a native fourth-edition section. Its finite +cache model, farthest-in-future policy, legal-trace exchange construction, and +public optimality theorem `CLRS.Caching.fifo_optimal` complete CLRS Theorem +15.5 for every nonempty initial cache and finite request sequence. It is imported through [Section 15.4](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/). The section is split into the sub-modules: @@ -36,6 +38,10 @@ The section is split into the sub-modules: * [Farthest-In-Future Eviction](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S2_Farthest_In_Future/) * [Optimality](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality/) +This completion is at the mathematical cache-policy level. Pointer/RAM +implementations and hardware caching costs remain optional refinements outside +the advertised theorem boundary. + The third-edition Sections 16.4 (matroids) and 16.5 (task scheduling) are retained as supplementary online material (reachable through {lit}`CLRSLean.OnlineMaterial`). diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching.lean index d2981419..2b395c8e 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching.lean @@ -9,7 +9,7 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S3_Optimal This section formalizes the offline caching problem of CLRS §15.4 and the farthest-in-future (Belady) eviction policy: the cache model with policies, hits and misses, the next-use function, the farthest-in-future selection, and -basic sanity lemmas for the policy. +the finite-trace exchange proof that the policy is optimal. Main results: @@ -19,13 +19,17 @@ Main results: - `farthestInFuture cache σ i`: the resident page whose next use is farthest - `fifoPolicy σ`: the farthest-in-future eviction policy - `fifo_step_of_mem` / `fifo_step_fault`: the policy's cache transitions +- `LegalTrace`: a policy-independent certificate for a legal cache execution +- `fifo_optimal`: for every nonempty initial cache and finite request sequence, + the farthest-in-future policy incurs no more misses than any policy (CLRS + Theorem 15.5) -Current gaps: +Completion boundary: -- The optimality theorem (`fifo_optimal`: no eviction policy has fewer - misses than the farthest-in-future policy, CLRS Theorem 15.5) remains to - be formalized; the classical exchange argument over request suffixes is - deferred. +- The mathematical offline-caching optimality theorem is complete. The result + is stated for finite request lists and a nonempty finite initial cache. + Pointer-level cache mutation, RAM costs, and hardware caching behavior are + separate implementation refinements and are not claimed here. Notation conventions used in this section: @@ -41,4 +45,12 @@ The section is split into the following sub-modules: * [Cache Model](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S1_Cache_Model/) * [Farthest-In-Future Eviction](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S2_Farthest_In_Future/) * [Optimality](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality/) +* [Optimality proof overview](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/) +* [Trace-coupling proof](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/) +* [Legal cache traces](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A1_LegalTrace/) +* [Exact one-page cache difference](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A2_OnePageDiff/) +* [Recursive coupling core](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A3_CouplingCore/) +* [Coupling correctness](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A4_CouplingCorrect/) +* [One-step FIF exchange](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A5_Exchange/) +* [Finite exchange iteration](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A6_Iteration/) -/ diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B3_AfterJ_Window.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B3_AfterJ_Window.lean index 7e6f76f4..ecfc5388 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B3_AfterJ_Window.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B3_AfterJ_Window.lean @@ -16,7 +16,8 @@ Main results: - `repairSchedule_after_J_window`: the `(J, J']` window relation, by induction from `repairSchedule_after_J` -This file is part of the `fifo_optimal` iteration (see `Dev/DESIGN.md`); it +This file is part of the archived `fifo_optimal` iteration (see +`Dev/Legacy/StateMachine/DESIGN.md`); it will be merged into `S3_Optimality.lean` once the proof is complete. -/ diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B4_Repair_Swap_Count.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B4_Repair_Swap_Count.lean index cabaf63a..ec8747ce 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B4_Repair_Swap_Count.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B4_Repair_Swap_Count.lean @@ -4,7 +4,7 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B3_Aft # Dev B4: the resident (B2) repair counting lemma Development file for the resident-case repair step of the `fifo_optimal` -iteration (see `Dev/DESIGN.md`): when `q = e t` is resident, replacing the +iteration (see `Dev/Legacy/StateMachine/DESIGN.md`): when `q = e t` is resident, replacing the eviction at the first disagreement by the policy's choice (`q'`, evicted again at its first request) costs at most one extra miss and extends agreement by one position — the B2 analogue of `repair_step`. diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B5_Iteration.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B5_Iteration.lean index d4d1f3d2..50d35a52 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B5_Iteration.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B5_Iteration.lean @@ -4,7 +4,7 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B4_Rep # Dev B5: the iteration to `fifo_optimal` Development file for the final assembly of the optimality proof (see -`Dev/DESIGN.md`): starting from an arbitrary reduced schedule, repeatedly +`Dev/Legacy/StateMachine/DESIGN.md`): starting from an arbitrary reduced schedule, repeatedly repair or exchange at the first disagreement with the FIF schedule, tracking the reducedness bound and the accumulated slack, until the schedule agrees with the policy everywhere; the miss count never increases overall. diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B6_Strong_Repair.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B6_Strong_Repair.lean index 1b44f125..e2080e1f 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B6_Strong_Repair.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B6_Strong_Repair.lean @@ -4,7 +4,7 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B5_Ite # Dev B6: the strong B2 repair (no slack needed) Development file for the resident (B2) repair step of the `fifo_optimal` -iteration (see `Dev/DESIGN.md`): when `q = e t` is resident at a case-B +iteration (see `Dev/Legacy/StateMachine/DESIGN.md`): when `q = e t` is resident at a case-B position, the repair `r = repairSchedule e t q'' (t+1+j'')` costs **no slack** — the good event at `J = t+1+j` (the repair hits where `e` faults) offsets the bad event at `J'' = t+1+j''`. This is the "strong version" of diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B7_Iteration.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B7_Iteration.lean index 00730f08..cca8d9bb 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B7_Iteration.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B7_Iteration.lean @@ -4,7 +4,7 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B6_Str # Dev B7: the iteration assembly (repair diff invariants) Development file for the iteration assembly of the `fifo_optimal` proof (see -`Dev/DESIGN.md`): the reverse-diff invariants of a B2 repair. At a B2 +`Dev/Legacy/StateMachine/DESIGN.md`): the reverse-diff invariants of a B2 repair. At a B2 position `t` (inside the window of the last case-A exchange), with `q = e t` resident and `q'' = fifoSchedule σ C₀ t` both alive (`j < j''`), the repair `r = repairSchedule e t q'' (t + 1 + j'')` evicts `q''` at `t` @@ -73,7 +73,7 @@ Main results: `Q' = insert (t₂, q'') Q`, `P'`, `r` from the old state's invariants plus the step's facts (`r t₂ = q''`, `r nop = q''`, `r s = d s` off `{t₂, nop}`, caches agree up to `t₂`, `σ[t₂]` fault, `q''` resident); - hQ's extension is the open design question (see `Dev/DESIGN.md`) + hQ's extension is the open design question (see `Dev/Legacy/StateMachine/DESIGN.md`) - `iterate_main_case_b2_alive`: the case-B2 step (alive-alive) — the repair at a resident disagreement: agreement to `t₂ + 1`, misses not increased, chain extended by `q''`, `hd_eq` extended to @@ -100,7 +100,7 @@ Main results: is reduced from `t + 1` on except the branch-1 positions (`d s = q'` — the exchange evicts `q'` as a no-op, not resident; at most one such fault); the q-dead sub-case's final agreement is attainable (the - DESIGN's "unattainable" claim is stale — see `Dev/DESIGN.md`) + DESIGN's "unattainable" claim is stale — see `Dev/Legacy/StateMachine/DESIGN.md`) - the q₀'-B1 slack supply: `exchangeSchedule_eq_q'_imp_d_eq_q'` (the branch-1 reverse — the exchange evicts `q₀'` at `s > t₀` iff the source does), `b1_exchange_no_bad_q0` (at a B1 with `d t₂ = q₀'`, `t₂ ∉ P`, @@ -111,7 +111,7 @@ Main results: gives `q₀' ∉ D₀_{J'₀}` — the exchange's bad event did not occur) and `b1_bad_le_slack_q0` (`bad ≤ slack` for the q₀'-B1 given `1 ≤ slack`) — the q₀' half of the slack accounting; the non-q₀' B1s are the open - design question (see `Dev/DESIGN.md`) + design question (see `Dev/Legacy/StateMachine/DESIGN.md`) This file is part of the `fifo_optimal` iteration; it will be merged into `S3_Optimality.lean` once the proof is complete. diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B9_Assembly.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B9_Assembly.lean index f2152ada..147c4a6e 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B9_Assembly.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/StateMachine/B9_Assembly.lean @@ -7,7 +7,7 @@ The concrete instantiation of `iterate_main`'s abstract case-step supplies `hB1`/`hB2`/`hAone` with the kernel-checked case-step lemmas and the extension glue. The checkpoint wires everything that is proved and leaves the genuinely open pieces as **documented -hypotheses** (referencing `Dev/DESIGN.md`) — with no unfinished proof placeholder (the +hypotheses** (referencing `Dev/Legacy/StateMachine/DESIGN.md`) — with no unfinished proof placeholder (the repository checker forbids them on `main`): 1. `hQ_open`: the hQ-strictness/extension — the state's `hQ` field diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality.lean new file mode 100644 index 00000000..165745a3 --- /dev/null +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality.lean @@ -0,0 +1,13 @@ +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace + +/-! +# Section 15.4 optimality proof + +This module is the reader-facing entry point for the legal-trace coupling proof +of farthest-in-future optimality. The trace submodule packages the six proof +layers from policy semantics through finite exchange iteration. + +Implementation details: + +* [Trace-coupling proof](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/) +-/ diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace.lean new file mode 100644 index 00000000..09ba0189 --- /dev/null +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace.lean @@ -0,0 +1,18 @@ +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A6_Iteration + +/-! +# Section 15.4 trace-coupling proof + +The optimality proof proceeds through legal cache traces, exact one-page cache +differences, a recursive ordered/credited suffix coupling, one-step exchange, +and finite iteration. + +Proof layers: + +* [Legal cache traces](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A1_LegalTrace/) +* [Exact one-page cache difference](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A2_OnePageDiff/) +* [Recursive coupling core](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A3_CouplingCore/) +* [Coupling correctness](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A4_CouplingCorrect/) +* [One-step FIF exchange](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A5_Exchange/) +* [Finite exchange iteration](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A6_Iteration/) +-/ diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A1_LegalTrace.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A1_LegalTrace.lean index c23a068a..2a7dd758 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A1_LegalTrace.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A1_LegalTrace.lean @@ -1,7 +1,7 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S2_Farthest_In_Future /-! -# Chapter 15.4 development: legal cache traces +# Section 15.4 optimality: legal cache traces This file separates the semantic notion of a legal cache execution from the `Policy` representation. It is the first layer of the trace-coupling proof of diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A2_OnePageDiff.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A2_OnePageDiff.lean index 384ee68f..82744913 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A2_OnePageDiff.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A2_OnePageDiff.lean @@ -1,7 +1,7 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A1_LegalTrace /-! -# Chapter 15.4 development: exact one-page cache difference +# Section 15.4 optimality: exact one-page cache difference The exchange proof needs a precise relation for two equal-size caches that differ in exactly one resident page on each side. diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A3_CouplingCore.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A3_CouplingCore.lean index ece7d73a..b8aa1e94 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A3_CouplingCore.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A3_CouplingCore.lean @@ -1,7 +1,7 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A2_OnePageDiff /-! -# Chapter 15.4 development: recursive coupling core +# Section 15.4 optimality: recursive coupling core This file defines the transformed execution used by the local exchange. The definitions are total; their legality and miss accounting are proved in A4. diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A4_CouplingCorrect.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A4_CouplingCorrect.lean index 91c09e26..5bcdf807 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A4_CouplingCorrect.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A4_CouplingCorrect.lean @@ -1,7 +1,7 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A3_CouplingCore /-! -# Chapter 15.4 development: coupling correctness +# Section 15.4 optimality: coupling correctness This file proves that the recursive coupling is legal, preserves the exact cache relation, and never spends more misses than the local credit permits. diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A5_Exchange.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A5_Exchange.lean index 69f07cde..64c1464c 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A5_Exchange.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A5_Exchange.lean @@ -1,7 +1,7 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A4_CouplingCorrect /-! -# Chapter 15.4 development: one-step FIF exchange +# Section 15.4 optimality: one-step FIF exchange At the first transition where a legal trace differs from farthest-in-future, replace that eviction and couple the remaining suffix without increasing diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A6_Iteration.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A6_Iteration.lean index 9a38bc18..cb6e0959 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A6_Iteration.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A6_Iteration.lean @@ -1,7 +1,7 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A5_Exchange /-! -# Chapter 15.4 development: finite exchange iteration +# Section 15.4 optimality: finite exchange iteration Repeatedly extend agreement by one request boundary. The remaining number of boundaries is the sole termination measure. diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality.lean index fb7d4ced..8da4b006 100644 --- a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality.lean +++ b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality.lean @@ -1,6 +1,6 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S1_Cache_Model import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S2_Farthest_In_Future -import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A6_Iteration +import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality /-! # S3. Optimality of the farthest-in-future policy @@ -16,7 +16,7 @@ misses, and finite iteration yields a trace that agrees with FIF everywhere. Main results: - `fifo_optimal`: no offline eviction policy incurs fewer misses than FIF -- `LegalTrace` / `traceOfPolicy`: policy-independent legal cache executions and +- `LegalTrace` / `policyTrace`: policy-independent legal cache executions and the trace induced by any policy - `exchange_trace`: one local exchange extends agreement with FIF by one cache boundary without increasing total misses diff --git a/CLRSLean/Progress.lean b/CLRSLean/Progress.lean index c59e56b7..3594b659 100644 --- a/CLRSLean/Progress.lean +++ b/CLRSLean/Progress.lean @@ -19,7 +19,7 @@ least six months; removal is possible only in 2.0 or later. * Tracked reader-facing theorem entries: 1,510. * Proved tracked theorem entries: 1,510. * Online/supplementary theorem entries: 464. -* Remaining edition-coverage units: 2. +* Remaining edition-coverage units: 1. Tracked theorem entries form a selected proof inventory of reviewed groups mapped to represented fourth-edition sections. A complete proved/tracked count does not @@ -34,10 +34,10 @@ every theorem already selected for that chapter is proved. ## Status Counts -* {lit}`main-proof-complete`: 22 chapters. +* {lit}`main-proof-complete`: 23 chapters. * {lit}`main-proof-complete-for-correctness`: 6 chapters. * {lit}`selected-section-complete`: 4 chapters. -* {lit}`partial`: 2 chapters. +* {lit}`partial`: 1 chapter. * {lit}`expository`: 1 chapter. ## Chapter Matrix @@ -59,7 +59,7 @@ Ch Chapter Status 12 12. Binary Search Trees main-proof-complete-for-correctness 12.1;12.2;12.3 40 0 13 13. Red-Black Trees main-proof-complete 13.1;13.2;13.3;13.4 40 0 14 14. Dynamic Programming main-proof-complete 14.1;14.2;14.3;14.4;14.5 90 0 -15 15. Greedy Algorithms partial (edition coverage) 15.1;15.2;15.3;15.4 27 1 +15 15. Greedy Algorithms main-proof-complete 15.1;15.2;15.3;15.4 27 0 16 16. Amortized Analysis selected-section-complete 16.1;16.2;16.3;16.4 66 0 17 17. Augmenting Data Structures main-proof-complete 17.1;17.2;17.3 79 0 18 18. B-Trees main-proof-complete-for-correctness 18.1;18.2;18.3 134 0 diff --git a/CLRSLean/Status.lean b/CLRSLean/Status.lean index 1cb8ef0e..ca6e4ef0 100644 --- a/CLRSLean/Status.lean +++ b/CLRSLean/Status.lean @@ -44,7 +44,6 @@ prose does not freeze a completed-prefix milestone. The edition map currently records these fourth-edition gaps: * **Chapter 10, Elementary Data Structures:** Section 10.1 remains partial. -* **Chapter 15, Greedy Algorithms:** Section 15.4 (offline caching) is a native section with the farthest-in-future policy; the optimality theorem remains. * **Chapter 29, Linear Programming:** Sections 29.1--29.3 remain partial for general-form normalization, finite formulation bridges, and canonical declaration ownership; detailed SIMPLEX material remains available online. @@ -60,6 +59,10 @@ progress ledger. Such a label applies only to the advertised Lean model and represented fourth-edition sections, never automatically to exercises, chapter-end Problems, pointer/RAM models, or floating-point implementations. +Chapter 15 is no longer an edition-map gap: the native §15.4 finite-cache model +now exposes `CLRS.Caching.fifo_optimal`, the unconditional farthest-in-future +optimality theorem for nonempty initial caches and finite request sequences. + ## Not-Started Chapters * **Chapters 34--35, NP-Completeness and Approximation Algorithms:** guide-only, diff --git a/README.md b/README.md index 6b412e3f..abca1bca 100644 --- a/README.md +++ b/README.md @@ -69,7 +69,7 @@ selected. Edition-level gaps determine the status and **Edition gaps** column. | 12 | Binary Search Trees | 🟢 correctness | 40 / 40 | — | | 13 | Red-Black Trees | 🟢 complete | 40 / 40 | — | | 14 | Dynamic Programming | 🟢 complete | 90 / 90 | — | -| 15 | Greedy Algorithms | 🟠 partial coverage | 27 / 27 | Section 15.4 (Offline caching): the exchange step the slack… | +| 15 | Greedy Algorithms | 🟢 complete | 27 / 27 | — | | 16 | Amortized Analysis | 🟡 sections | 66 / 66 | — | | 17 | Augmenting Data Structures | 🟢 complete | 79 / 79 | — | | 18 | B-Trees | 🟢 correctness | 134 / 134 | — | diff --git a/docs/clrs-fourth-edition-map.csv b/docs/clrs-fourth-edition-map.csv index c9c892e7..ea2488ea 100644 --- a/docs/clrs-fourth-edition-map.csv +++ b/docs/clrs-fourth-edition-map.csv @@ -54,10 +54,10 @@ chapter_no,section_no,chapter_title,section_title,migration_state,source_modules 14,14.3,Dynamic Programming,Elements of dynamic programming,native,CLRSLean.FourthEdition.Chapter_14.Section_14_3_Elements_Of_Dynamic_Programming,none,Native fourth-edition §14.3 Elements of dynamic programming: the reusable memo-cache consistency invariant and the distinct-state cost bridge. 14,14.4,Dynamic Programming,Longest common subsequence,native,CLRSLean.FourthEdition.Chapter_14.Section_14_4_Longest_Common_Subsequence,none,Native fourth-edition §14.4 Longest common subsequence: the tabulated Θ(mn) table bound for the bottom-up length and reconstruction. 14,14.5,Dynamic Programming,Optimal binary search trees,native,CLRSLean.FourthEdition.Chapter_14.Section_14_5_Optimal_Binary_Search_Trees,none,"Native fourth-edition §14.5 Optimal binary search trees: the public e/w/root tables, a public reconstruction interface, and the Θ(n³) time / Θ(n²) space bounds." -15,15.1,Greedy Algorithms,An activity-selection problem,facade,CLRSLean.Chapter_16,CLRS third edition Chapter 16,The current Chapter 16 guide supplies the represented proof interface during the compatibility period. -15,15.2,Greedy Algorithms,Elements of the greedy strategy,facade,CLRSLean.Chapter_16,CLRS third edition Chapter 16,The current Chapter 16 guide supplies the represented proof interface during the compatibility period. -15,15.3,Greedy Algorithms,Huffman codes,facade,CLRSLean.Chapter_16,CLRS third edition Chapter 16,The current Chapter 16 guide supplies the represented proof interface during the compatibility period. -15,15.4,Greedy Algorithms,Offline caching,partial,CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching;CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S1_Cache_Model;CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S2_Farthest_In_Future;CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S3_Optimality,none,"Native fourth-edition source: offline-caching model, farthest-in-future selection, and the FIF policy; the exchange-schedule machinery with the weakened reducedness hypothesis, the one-step exchange, the slack lemma, and the repair step are proved; the iteration state machine to CLRS Theorem 15.5 remains BLOCKED by two documented design blockers (the slack-accounting invariant is empirically false, and the hQ state field does not hold over the full-history pair set) recorded in Dev/DESIGN.md — completing it needs original research on a correct accounting scheme, not a final proof pass." +15,15.1,Greedy Algorithms,An activity-selection problem,native,CLRSLean.FourthEdition.Chapter_15.Section_15_1_Activity_Selection,CLRS third edition Section 16.1,"Native fourth-edition source: sorted-list activity-selection optimality (greedy exchange certificate, recursive tail optimality, maximum-cardinality bundles). Legacy Section 16.1 forwards to it during the compatibility period." +15,15.2,Greedy Algorithms,Elements of the greedy strategy,native,CLRSLean.FourthEdition.Chapter_15.Section_15_2_Greedy_Meta,CLRS third edition Section 16.2,Native fourth-edition source: the abstract greedy-choice property (Lemma 15.1) and optimal substructure (Lemma 15.2) meta-theorems. Legacy Section 16.2 forwards to it during the compatibility period. +15,15.3,Greedy Algorithms,Huffman codes,native,CLRSLean.FourthEdition.Chapter_15.Section_15_3_Huffman_Codes,CLRS third edition Section 16.3,"Native fourth-edition source: the self-contained Huffman optimality proof (split-leaf transformation, forest V2 optimality, frequency-table interface). Legacy Section 16.3 forwards to it during the compatibility period." +15,15.4,Greedy Algorithms,Offline caching,native,CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching;CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S1_Cache_Model;CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S2_Farthest_In_Future;CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S3_Optimality,none,"Native fourth-edition source: the offline-caching model, farthest-in-future policy, legal cache traces, finite-trace exchange/coupling construction, and the unconditional fifo_optimal theorem (CLRS Theorem 15.5) for nonempty initial caches and finite request sequences." 16,16.1,Amortized Analysis,Aggregate analysis,facade,CLRSLean.Chapter_17,CLRS third edition Chapter 17,The current Chapter 17 guide supplies the represented proof interface during the compatibility period. 16,16.2,Amortized Analysis,The accounting method,facade,CLRSLean.Chapter_17,CLRS third edition Chapter 17,The current Chapter 17 guide supplies the represented proof interface during the compatibility period. 16,16.3,Amortized Analysis,The potential method,facade,CLRSLean.Chapter_17,CLRS third edition Chapter 17,The current Chapter 17 guide supplies the represented proof interface during the compatibility period. diff --git a/docs/clrs-proof-progress.csv b/docs/clrs-proof-progress.csv index 06ad4e11..0e02a93e 100644 --- a/docs/clrs-proof-progress.csv +++ b/docs/clrs-proof-progress.csv @@ -13,7 +13,7 @@ chapter_no,chapter_title,repo_status,represented_sections,tracked_key_theorems,p 12,Binary Search Trees,main-proof-complete-for-correctness,12.1;12.2;12.3,40,40,0,The fourth-edition facade reuses 40 proved tracked theorem entries from legacy Chapter 12 across represented Sections 12.1;12.2;12.3,Search; min/max; insertion; complete successor/predecessor specifications; functional delete membership and ordering; search and neighbor queries after updates; faithful zipper reconstruction; iterative search equivalence; transplant ordering preservation; deletion-via-transplant equivalence; parent-ascent successor/predecessor equivalence; imperative pointer-heap node/store model; heap-to-tree abstraction faithfulness; pointer frame rules; in-place TRANSPLANT refinement; pointer TREE-INSERT leaf-attachment refinement,None,CLRSLean/FourthEdition/Chapter_12.lean; CLRSLean/Chapter_12.lean; CLRSLean/Chapter_12/Section_12_1_Binary_Search_Trees.lean; CLRSLean/Status.lean; Tests/Chapter_12_Interface.lean,Canonical fourth-edition Chapter 12 currently reuses its legacy source through a compatibility facade. Legacy source note: The represented mathematical and refinement interfaces are complete; lower-level pointer deletion and RAM accounting do not block the correctness milestone. Non-blocking scope note: pointer-level in-place delete and explicit RAM costs are optional low-level refinements. 13,Red-Black Trees,main-proof-complete,13.1;13.2;13.3;13.4,40,40,0,"All 40 tracked theorem entries are proved: the color/black-height and functional key-set/shape layers, the §13.2/§13.3 pointer/sentinel store with BST-preserving rotations and insertion, and the §13.4 deletion with logarithmic pointer cost and BST ordering preservation",Rotation membership; repaint membership; no-red-red; black-height; local red-black shape preservation; insertion-fixup certificates; executable insert and redBlackShape_insert; height_log_bound (Lemma 13.1); executable baldL/baldR/splitMin/join/del/delete; inTree_delete_iff; local delete-fixup membership and shape certificates; deficit-absorbing rebalancer certificates baldL_shape and baldR_shape; splitMin_invariant; del_invariant; redBlackShape_delete; BST ordering preservation of deletion (bst_delete) via the keys sublist pipeline (keys_baldL/keys_baldR/keys_splitMin_cons/keys_join/keys_del_sublist/bst_del),None,CLRSLean/FourthEdition/Chapter_13.lean; CLRSLean/Chapter_13.lean; CLRSLean/Chapter_13/Section_13_1_Red_Black_Trees.lean; CLRSLean/Status.lean,"redBlackShape_delete and exact delete membership are proved; §13.2/§13.3 add the pointer/sentinel store, BST/inorder rotation preservation, bst_insert, and logarithmic insert/delete costs; §13.4 adds bst_delete (BST-preserving deletion), so deletion is a complete red-black search-tree theorem." 14,Dynamic Programming,main-proof-complete,14.1;14.2;14.3;14.4;14.5,90,90,0,The fourth-edition facade maps 90 proved tracked theorem groups; native sections 14.1-14.5 complete the algorithm/table/cost and generic-DP boundary,Bellman rod-cutting recurrence and bottom-up value; mutable-Array bottom-up rod-cutting refinement; optimal-cut reconstruction and top-down memoization; rod-cutting O(n^2) step count; matrix-chain lower bound pure optimum split reconstruction and correctness; tabulated MATRIX-CHAIN-ORDER time/space bounds; LCS recurrence pure length/reconstruction and correctness; tabulated Theta(mn) LCS bound; optimal-BST recurrence evaluator and existential optimal-plan correctness; public OBST e/w/root tables and cost bounds; reusable memo-cache invariant and distinct-state cost bridge,None,CLRSLean/FourthEdition/Chapter_14.lean; CLRSLean/Chapter_15.lean; CLRSLean/Chapter_15/Section_15_1_Rod_Cutting.lean; CLRSLean/Chapter_15/Section_15_2_Matrix_Chain_Multiplication.lean; CLRSLean/Chapter_15/Section_15_4_Longest_Common_Subsequence.lean; CLRSLean/Chapter_15/Section_15_5_Optimal_Binary_Search_Trees.lean; CLRSLean/FourthEdition/Chapter_14/Section_14_1_Rod_Cutting.lean; CLRSLean/FourthEdition/Chapter_14/Section_14_2_Matrix_Chain_Multiplication.lean; CLRSLean/FourthEdition/Chapter_14/Section_14_3_Elements_Of_Dynamic_Programming.lean; CLRSLean/FourthEdition/Chapter_14/Section_14_4_Longest_Common_Subsequence.lean; CLRSLean/FourthEdition/Chapter_14/Section_14_5_Optimal_Binary_Search_Trees.lean; Tests/FourthEdition_Chapter_14_Interface.lean; CLRSLean/Status.lean,"The represented examples now have tabulated/memoized fourth-edition algorithms with cost bounds, plus the generic Elements-of-DP interface. An explicit RAM execution cost semantics remains a future target." -15,Greedy Algorithms,partial,15.1;15.2;15.3;15.4,27,27,1,The fourth-edition facade maps 23 proved tracked theorem groups after excluding moved material to the online ledger; the edition map records exact represented sections and gaps,Activity-selection greedy optimality; Huffman V2 frequency-table optimality and minimum-cost wrappers; GreedyProblem meta-theorem and gsolve_optimal (CLRS §16.2 greedy-choice property and optimal substructure),Section 15.4 (Offline caching): the exchange step the slack lemma and the repair step are proved; the FIF optimality iteration state machine is BLOCKED by two documented design blockers (slack-accounting invariant empirically false; hQ field does not hold over the full-history pair set) recorded in Dev/DESIGN.md,CLRSLean/FourthEdition/Chapter_15.lean; CLRSLean/Chapter_16.lean; CLRSLean/Chapter_16/Section_16_2_Greedy_Meta.lean; CLRSLean/Status.lean,The canonical fourth-edition ledger excludes 9 matroid and task-scheduling groups recorded in the online-material ledger. Canonical fourth-edition Chapter 15 currently reuses legacy Chapter 16 through a compatibility facade. Legacy source note: The represented Sections 16.1-16.5 cover the core chapter theorem groups; exercises remain an optional second track. +15,Greedy Algorithms,main-proof-complete,15.1;15.2;15.3;15.4,27,27,0,All 27 selected fourth-edition theorem groups are proved; the native Sections 15.1-15.4 include the complete mathematical offline-caching optimality stack,Activity-selection greedy optimality; GreedyProblem meta-theorem and gsolve_optimal (CLRS §15.2 greedy-choice property and optimal substructure); Huffman V2 frequency-table optimality and minimum-cost wrappers; legal cache traces and policy equivalence; finite-trace exchange and coupling; fifo_optimal (CLRS Theorem 15.5),None,CLRSLean/FourthEdition/Chapter_15.lean; CLRSLean/FourthEdition/Chapter_15/Section_15_1_Activity_Selection.lean; CLRSLean/FourthEdition/Chapter_15/Section_15_2_Greedy_Meta.lean; CLRSLean/FourthEdition/Chapter_15/Section_15_3_Huffman_Codes.lean; CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality.lean; CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A6_Iteration.lean; Tests/Chapter_15_4_Interface.lean; CLRSLean/Status.lean,The canonical fourth-edition ledger excludes 9 third-edition matroid and task-scheduling groups recorded in the online-material ledger. Sections 15.1-15.4 are native fourth-edition sources; legacy Sections 16.1-16.3 forward to the first three during the compatibility period. The FIF theorem covers finite request lists and nonempty finite initial caches; pointer/RAM cache implementations and hardware caching costs are outside the advertised mathematical boundary. 16,Amortized Analysis,selected-section-complete,16.1;16.2;16.3;16.4,66,66,0,The fourth-edition facade reuses 66 proved tracked theorem entries from legacy Chapter 17 across represented Sections 16.1;16.2;16.3;16.4,Aggregate/accounting/potential telescoping; MULTIPOP; executable binary-counter one-step and multi-step trace bounds; dynamic-table potential nonnegativity; concrete amortized-cost unfoldings and transition/capacity wrappers,None,CLRSLean/FourthEdition/Chapter_16.lean; CLRSLean/Chapter_17.lean; CLRSLean/Chapter_17/Section_17_1_Amortized_Framework.lean; CLRSLean/Chapter_17/Section_17_1_Amortized_Framework/Section_17_2_Stack_And_Counter.lean; CLRSLean/Chapter_17/Section_17_4_Dynamic_Tables.lean; Tests/Chapter_17_Interface.lean,Canonical fourth-edition Chapter 16 currently reuses legacy Chapter 17 through a compatibility facade. Legacy source note: No sorry/admit/axiom in Chapter_17; the size-level represented theorem stack is complete. Non-blocking scope note: mutable-array copying allocator constants and sharper RAM models are optional refinements. 17,Augmenting Data Structures,main-proof-complete,17.1;17.2;17.3,79,79,0,"All 79 tracked theorem entries are proved: the size/generic-augmentation/static-interval results plus OS-RANK with the O(log n) query bound, the constant-time-combine augmentation update bound, the dynamic/static interval-tree bridge, and the Interval-keyed O(log n) search bound",Size augmentation invariant; size recomputation; key preservation; size/rank-preserving local rotations; augmented rank-select correctness; generic rotation-invariant augmentation theorem (CLRS 14.1); interval overlap semantics and search specification; OSRBTree wellSized_insert and wellSized_delete with toRB refinement; generic AugmentedRBTree executable insertion and deletion with wellAugmented_insert and wellAugmented_delete for any augmentation; repaintRoot/rootBlack/baldL/baldR/splitMin/join/del/delete pipeline preserving WellAugmented; deletion refinement erasure toRB_delete with toRB_baldL/toRB_baldR/toRB_splitMin/toRB_join/toRB_del commutations; size and max-high instances recovered; Interval-keyed O(log n) search bound (intervalSearchCost_log_bound) via the low-keyed height erasure (toRB_low/intervalHeight_eq_toRB_height),None,CLRSLean/FourthEdition/Chapter_17.lean; CLRSLean/Chapter_14.lean; CLRSLean/Chapter_14/Section_14_1_Order_Statistic_Trees.lean; CLRSLean/Chapter_14/Section_14_3_Interval_Trees.lean; CLRSLean/Status.lean,"OS-RANK with cached/ideal agreement and O(log n) query bound, the constant-time-combine augmentation update bound, the dynamic/static interval-tree bridge with search-after-update, and the Interval-keyed O(log n) search bound (intervalSearchCost_log_bound) are proved." 18,B-Trees,main-proof-complete-for-correctness,18.1;18.2;18.3,134,134,0,The fourth-edition facade reuses 134 proved tracked theorem entries from legacy Chapter 18 across represented Sections 18.1;18.2;18.3,Search and minimum-key facts; exact totalKeys node accounting; non-root augmented power lower bound; root empty-or augmented lower bound; structural minKeys wrappers; universal wellFormed_height_log_bound; split-child and non-full insertion invariants; abstract update membership specifications; top-level full-root insertion exact add-one List.Perm semantics WellFormed and conditional-height preservation membership and specification-search compatibility executable-search correctness and absent-key WellFormedUnique preservation; NodeWF DeleteReady KeysSubset and RootDeleteResult contracts; merge and rotation repair packets; exact parent reassembly; composedDelete structural preservation; raw and normalized Multiset.erase semantics under structural assumptions; different-key membership without uniqueness; raw uniqueness preservation from NodeWF and UniqueKeys; normalized deleted-key absence full membership characterization WellFormedUnique preservation and specification membership-oracle compatibility,None,CLRSLean/FourthEdition/Chapter_18.lean; CLRSLean/Chapter_18.lean; CLRSLean/Chapter_18/Section_18_1_B_Tree_Model/HeightBound.lean; CLRSLean/Chapter_18/Section_18_2_B_Tree_Insertion.lean; CLRSLean/Chapter_18/Section_18_3_B_Tree_Deletion/KeyMultiset.lean; CLRSLean/Chapter_18/Section_18_3_B_Tree_Deletion/ExactReassembly.lean; CLRSLean/Chapter_18/Section_18_3_B_Tree_Deletion/Exact.lean; CLRSLean/Chapter_18/Section_18_3_B_Tree_Deletion/WellFormed.lean; Tests/Chapter_18_Search_Interface.lean; Tests/Chapter_18_Height_Interface.lean; Tests/Chapter_18_Insertion_Interface.lean; Tests/Chapter_18_KeyMultiset_Interface.lean; Tests/Chapter_18_Deletion_Reassembly_Interface.lean; Tests/Chapter_18_Deletion_Exact_Interface.lean; Tests/Chapter_18_Deletion_Root_Exact_Interface.lean; Tests/Chapter_18_Interface.lean; Tests/Chapter_18_Deletion_Interface.lean; Tests/Chapter_18_Root_Occupancy.lean,Canonical fourth-edition Chapter 18 currently reuses its legacy source through a compatibility facade. Legacy source note: The flat insert remains the specification layer and the transient empty parent used by splitRoot is not claimed WellFormed; no executable and specification tree-shape equality is claimed; the structural count uses List key slots without a uniqueness premise; the legal empty root is explicit; disk-page layout pointer mutation page I/O counts and RAM semantics remain optional low-level refinements. @@ -34,4 +34,3 @@ chapter_no,chapter_title,repo_status,represented_sections,tracked_key_theorems,p 33,Machine-Learning Algorithms,main-proof-complete,33.1; 33.2; 33.3,15,15,0,The fourth-edition native Sections 33.1 33.2 and 33.3 prove 15 tracked theorem entries; no edition-map coverage gaps remain,mean_minimizes_sumSqDist (Lemma 33.1); assignStep_cost_le; updateStep_cost_le; lloyd_iteration_cost_le (Theorem 33.2); one_sub_rpow_le_one_sub_mul; neg_log_one_sub_le_add_sq; potential_update_le_exp; potential_weights_le; weights_eq_rpow_expertLoss; totalExpectedLoss_le (Theorem 33.3); gradient_inner_le_sub; gdStep_potential_le; gdIterates_potential_le; sum_suboptimality_le; avgIterate_suboptimality_le (Theorem 33.8),None,CLRSLean/FourthEdition/Chapter_33.lean; CLRSLean/FourthEdition/Chapter_33/Section_33_1_Clustering.lean; CLRSLean/FourthEdition/Chapter_33/Section_33_2_Multiplicative_Weights.lean; CLRSLean/FourthEdition/Chapter_33/Section_33_3_Gradient_Descent.lean,Canonical fourth-edition Chapter 33 formalizes natively the §33.1 Clustering analysis (the k-means cost, its variance decomposition, and Lloyd's two steps with cost monotonicity, Lemma 33.1 and Theorem 33.2), the §33.2 Multiplicative-weights method (the potential and expected-loss accounting, the exponential potential chain, and the regret bound against the best expert, Theorem 33.3), and the §33.3 Gradient-descent analysis (the gradient-descent lemma, the per-step and telescoping potential inequalities, the total-suboptimality bound, and the average-iterate convergence bound, Theorem 33.8). The legacy third-edition Chapter 33 (computational geometry) is cataloged as online material. 34,NP-Completeness,partial,34.1;34.2;34.3;34.4,12,12,1,"The fourth-edition Chapter 34 is supplied by the legacy Chapter 34 sources (compatibility facade; 3rd- and 4th-edition chapter numbers coincide). Section 34.1 formalizes polynomial time and the class P, with the closure of P under composition, complement, union, and intersection; Section 34.2 formalizes polynomial-time verification and P ⊆ NP (Theorem 34.2); Section 34.3 formalizes NP-completeness and reducibility with transitivity of ≤_P; Section 34.4 formalizes CIRCUIT-SAT ≤_P SAT (Lemma 34.6), the SAT → 3-CNF-SAT semantic core (Lemma 34.7), and 3-CNF-SAT ≤_P CLIQUE (Lemma 34.10).",mem_ClassP; PolyTimeComputable.comp; ClassP_compl; ClassP_union; ClassP_inter; PolyTimeVerifiable.of_decidable; ClassP_subset_ClassNP (Theorem 34.2); PolyTimeReducible.trans; circuitSAT_reducible_to_SAT; cnfSatisfiable_iff_hasClique; cnfSatisfiable_to3CNF_iff; threeCNFSat_reducible_to_CLIQUE,The assembled SAT ≤_P 3-CNF-SAT machine reduction (PolyTimeReducible SAT ThreeCNFSat) is pending; Section 34.5 (NP-complete problems) is not represented; Section 34.1 empty/universal-language machines remain a minor recorded gap.,CLRSLean/FourthEdition/Chapter_34.lean; CLRSLean/Chapter_34.lean; CLRSLean/Chapter_34/Section_34_1_Polynomial_Time.lean; CLRSLean/Chapter_34/Section_34_1_Polynomial_Time/Composition.lean; CLRSLean/Chapter_34/Section_34_1_Polynomial_Time/AndOr.lean; CLRSLean/Chapter_34/Section_34_2_Polynomial_Time_Verification.lean; CLRSLean/Chapter_34/Section_34_2_Polynomial_Time_Verification/PairProjection.lean; CLRSLean/Chapter_34/Section_34_3_NP_Completeness_And_Reducibility.lean; CLRSLean/Chapter_34/Section_34_4_NP_Completeness_Proofs.lean; CLRSLean/Chapter_34/Section_34_4_NP_Completeness_Proofs/CircuitSAT.lean; CLRSLean/Chapter_34/Section_34_4_NP_Completeness_Proofs/CNFToClique.lean; CLRSLean/Status.lean,"The fourth-edition Chapter 34 reuses its legacy Chapter 34 sources through the compatibility facade. The theorem layer is complete: the closure of P under composition, complement, union, and intersection, P ⊆ NP (Theorem 34.2), and transitivity of ≤_P; and the §34.4 specific reductions CIRCUIT-SAT ≤_P SAT and 3-CNF-SAT ≤_P CLIQUE, plus the SAT → 3-CNF-SAT semantic core. The assembled SAT ≤_P 3-CNF-SAT machine reduction (PolyTimeReducible SAT ThreeCNFSat) and Section 34.5 remain recorded gaps; the SAT→3-CNF and CNF→CLIQUE machine files are site-nav registered but not yet wired into an aggregator." 35,Approximation Algorithms,main-proof-complete,35.1;35.2;35.3;35.4;35.5,10,10,0,The fourth-edition native Sections 35.1-35.5 prove 10 tracked theorem entries across all five approximation sections; no edition-map coverage gaps remain,approxVertexCover_two_approx (Theorem 35.1); tsp_two_approx (Theorem 35.2); greedySetCover_ln_approx (Theorem 35.4); max3cnf_approx (Theorem 35.5); approxSubsetSum_fptas (Theorem 35.8),None,CLRSLean/FourthEdition/Chapter_35.lean; CLRSLean/FourthEdition/Chapter_35/Section_35_1_The_Vertex_Cover_Problem.lean; CLRSLean/FourthEdition/Chapter_35/Section_35_2_The_Traveling_Salesperson_Problem.lean; CLRSLean/FourthEdition/Chapter_35/Section_35_3_The_Set_Covering_Problem.lean; CLRSLean/FourthEdition/Chapter_35/Section_35_4_Randomization_And_Linear_Programming.lean; CLRSLean/FourthEdition/Chapter_35/Section_35_5_The_Subset_Sum_Problem.lean,"Canonical fourth-edition Chapter 35 formalizes natively all five approximation sections: APPROX-VERTEX-COVER with its 2-approximation (Lemma 35.1, Theorem 35.1); APPROX-TSP-TOUR with the MST depth-first walk and 2-approximation (Lemmas 35.2-35.3, Theorem 35.2); GREEDY-SET-COVER with the harmonic charging H(d) bound and the O(lg |X|)-approximation (Theorems 35.3-35.4); the randomized 8/7-approximation of MAX-3-CNF and the factor-two LP-rounding of minimum-weight vertex cover (Theorems 35.5-35.6); and SUBSET-SUM with TRIM (Lemma 35.5), the (1+epsilon)-approximation (Theorem 35.7), and the FPTAS running-time analysis (Theorem 35.8)." - diff --git a/docs/index.md b/docs/index.md index 13d5cd5b..bb8f6c82 100644 --- a/docs/index.md +++ b/docs/index.md @@ -132,6 +132,14 @@ CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching.lean CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S1_Cache_Model.lean CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S2_Farthest_In_Future.lean CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality.lean +CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality.lean +CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace.lean +CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A1_LegalTrace.lean +CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A2_OnePageDiff.lean +CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A3_CouplingCore.lean +CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A4_CouplingCorrect.lean +CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A5_Exchange.lean +CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A6_Iteration.lean CLRSLean/Chapter_17/Section_17_1_Amortized_Framework.lean CLRSLean/Chapter_17/Section_17_1_Amortized_Framework/Section_17_2_Stack_And_Counter.lean CLRSLean/Chapter_17/Section_17_4_Dynamic_Tables.lean diff --git a/docs/migrations/clrs4.md b/docs/migrations/clrs4.md index f44cffa7..049ac17a 100644 --- a/docs/migrations/clrs4.md +++ b/docs/migrations/clrs4.md @@ -43,7 +43,7 @@ import CLRSLean.OnlineMaterial | --- | --- | --- | | Chapters 1--13 | `CLRSLean.Chapter_01`--`CLRSLean.Chapter_13` | Same chapter number; section differences are recorded in the edition map. | | Chapter 14, Dynamic Programming | `CLRSLean.Chapter_15` | Shifted facade. | -| Chapter 15, Greedy Algorithms | `CLRSLean.FourthEdition.Chapter_15` (native §15.1--15.3) | Sections 15.1--15.3 migrated to native fourth-edition sources; legacy `CLRSLean.Chapter_16.Section_16_1..3_*` forward to them. Matroid and task-scheduling material is supplementary online material. | +| Chapter 15, Greedy Algorithms | `CLRSLean.FourthEdition.Chapter_15` (native §15.1--15.4) | Sections 15.1--15.4 use native fourth-edition sources. Section 15.4 includes the unconditional finite-trace `fifo_optimal` theorem (CLRS Theorem 15.5); legacy `CLRSLean.Chapter_16.Section_16_1..3_*` forward to the first three sections. Matroid and task-scheduling material is supplementary online material. | | Chapter 16, Amortized Analysis | `CLRSLean.FourthEdition.Chapter_16` (native §16.1--16.4) | Sections 16.1--16.4 migrated to native fourth-edition sources; legacy `CLRSLean.Chapter_17.Section_17_*` forward to them. Declarations retain the `CLRS.Chapter17` namespace pending the chapter-by-chapter namespace migration. | | Chapter 17, Augmenting Data Structures | `CLRSLean.Chapter_14` | Shifted facade. | | Chapter 18, B-Trees | `CLRSLean.Chapter_18` | Same chapter number. | diff --git a/docs/proof-map.md b/docs/proof-map.md index 61dd15df..e8318181 100644 --- a/docs/proof-map.md +++ b/docs/proof-map.md @@ -2145,52 +2145,40 @@ reads are proved equal to the pure recurrence value. - Lean source: `CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching.lean`, split into sub-modules `S1_Cache_Model`, `S2_Farthest_In_Future`, and - `S3_Optimality` under the same directory -- Status: `partial` (first native fourth-edition section for Chapter 15) + `S3_Optimality` under the same directory. The final exchange proof is + organized under `Optimality/Trace/A1_LegalTrace` through `A6_Iteration`. +- Status: `proved` for the mathematical finite-cache policy model. The public + theorem covers every finite request list and every nonempty finite initial + cache; pointer/RAM implementations and hardware caching costs are outside + this advertised boundary. - Main theorems: - `CLRS.Caching.Policy` / `Policy.step` / `misses` / `nextUse` - `CLRS.Caching.Farther` / `farthestInFuture` - `CLRS.Caching.fifoPolicy` / `fifo_step_of_mem` / `fifo_step_fault` - `CLRS.Caching.fifo_step_size` - - `CLRS.Caching.exchangeSchedule` / `exchangeSchedule_invariant` / - `exchangeSchedule_misses_le`: one exchange step at the first disagreement - never increases the miss count (the good event at the first `q` request - compensates the unique bad event at the first `q'` request); the chain is - proved under the weakened reducedness hypothesis `hweak` - (`∀ s, t ≤ s → fault → d s resident`), so the counting lemma applies to - schedules that are reduced only from the exchange position on - - `CLRS.Caching.fifoSchedule` / `first_disagree` / `exchange_step`: at a - first disagreement of a schedule reduced from there on, exchanging the - evictions never increases misses and extends agreement with the FIF - schedule by one position - - `CLRS.Caching.exchangeSchedule_reduced_after`: the exchange schedule is - reduced at every fault after the first `q'` request, so the - "reduced from a bound on" state needed by the iteration is preserved - from one exchange to the next (the bound grows to `max hnb J'`) - - `CLRS.Caching.exchangeSchedule_misses_le_plus_one`: the exchange saves a - spare miss when the bad event did not occur (either `q'` is never - requested again and `q` is, or `d` evicts `q'` before its first request) - - `CLRS.Caching.repairSchedule` / `repair_step` / `repairSchedule_window` / - `repairSchedule_superset`: replacing a no-op eviction at the first - disagreement by the policy's choice (evicted again at its first request, - so the caches coincide afterwards) costs at most one extra miss and - extends agreement by one position -- Proof pattern: total-function policy model; the farthest-in-future choice - as a maximum over next-use positions with `none` (never requested again) - as the top element. -- Current gap: the iterated exchange concluding `fifo_optimal` (CLRS Theorem - 15.5) is **blocked**, not a mechanical wrap-up. The one-step pieces are in - place — `exchange_step` (never increases misses, extends agreement), - `exchangeSchedule_reduced_after` (preserves the reducedness state), - `exchangeSchedule_misses_le_plus_one` (spare miss when the bad event did - not occur), and `repair_step` (replacing a no-op eviction by the policy's - choice costs at most one extra miss, paid by the slack) — but the iteration - state machine cannot be assembled without resolving two documented design - blockers (see `Dev/DESIGN.md`): the slack-accounting invariant - `bad ≤ slack` is empirically false (492 counterexample traces over short - inputs), and the `hQ` state field does not hold over the full-history pair - set (988 B2 steps reach broken states). Completing this needs original - research on a correct accounting/state scheme, not a final proof pass. + - `CLRS.Caching.LegalTrace` / `policyTrace` / + `traceMisses_policyTrace`: policy-independent legal executions and the + bridge back to the original policy semantics + - `CLRS.Caching.OnePageDiff`: exact one-page cache difference used by the + local suffix coupling + - `CLRS.Caching.exchange_trace`: replaces the first trace transition that + disagrees with FIF, extends agreement by one boundary, and never increases + total misses + - `CLRS.Caching.exists_fully_agreeing_trace` / `fifo_optimal_trace`: finite + iteration of the local exchange + - `CLRS.Caching.fifo_optimal` (CLRS Theorem 15.5): + `misses (fifoPolicy σ) C₀ σ ≤ misses π C₀ σ` for every policy `π` when + `C₀.Nonempty` +- Proof pattern: turn policy runs into legal cache traces, couple two suffixes + whose caches differ by exactly one page, use FIF's next-use maximality in an + ordered phase, pay a later transformed-only miss with a local one-miss credit, + then iterate the first-disagreement exchange over the finite request length. +- Historical note: the earlier global schedule state machine is retained only + under `Dev/Legacy/StateMachine`. Its known false invariants and search + evidence are recorded in `Dev/Legacy/FAILED_APPROACHES.md`; no public module + imports that route. It is failure documentation, not a remaining section + blocker. +- Current gap: none for the advertised mathematical cache-policy theorem. ## Chapter 16 - Greedy Algorithms diff --git a/docs/superpowers/plans/2026-08-08-fifo-optimality-design.md b/docs/superpowers/plans/2026-08-08-fifo-optimality-design.md index c6a871bc..944f2e3d 100644 --- a/docs/superpowers/plans/2026-08-08-fifo-optimality-design.md +++ b/docs/superpowers/plans/2026-08-08-fifo-optimality-design.md @@ -1,7 +1,10 @@ # FIF (farthest-in-future) optimality — proof design -Status: **design stage** (2026-08-08). Target: CLRS Theorem 15.5 -(`fifo_optimal`), the last gap of §15.4. +Status: **historical and superseded** (2026-08-12). This swap-conjugate design +records an early proof route; it is not the current §15.4 status. The completed +legal-trace coupling architecture is specified in +`docs/superpowers/specs/2026-08-12-ch15-4-fifo-optimality-design.md`, and the +public theorem is `CLRS.Caching.fifo_optimal`. ## Current state diff --git a/docs/superpowers/specs/2026-08-12-ch15-4-fifo-optimality-design.md b/docs/superpowers/specs/2026-08-12-ch15-4-fifo-optimality-design.md index 69b33902..2924193f 100644 --- a/docs/superpowers/specs/2026-08-12-ch15-4-fifo-optimality-design.md +++ b/docs/superpowers/specs/2026-08-12-ch15-4-fifo-optimality-design.md @@ -2,6 +2,13 @@ Date: 2026-08-12 +Status: implemented. The public source now follows the selected legal-trace +coupling architecture, exposes the unconditional `CLRS.Caching.fifo_optimal` +theorem at the approved type, and locks both `fifo_optimal` and +`exchange_trace` in `Tests/Chapter_15_4_Interface.lean`. The superseded global +state-machine route is archived under `Dev/Legacy/StateMachine`, with its known +failed invariants recorded in `Dev/Legacy/FAILED_APPROACHES.md`. + ## Objective Complete the main theorem of CLRS Fourth Edition Section 15.4: the diff --git a/literate.toml b/literate.toml index 52f45b86..9a77a888 100644 --- a/literate.toml +++ b/literate.toml @@ -298,6 +298,18 @@ description = "A Lean 4 companion for CLRS-style algorithm correctness proofs." "CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S1_Cache_Model", "CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S2_Farthest_In_Future", "CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S3_Optimality", + "CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality", +] +"CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality" = [ + "CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace", +] +"CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace" = [ + "CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A1_LegalTrace", + "CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A2_OnePageDiff", + "CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A3_CouplingCore", + "CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A4_CouplingCorrect", + "CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A5_Exchange", + "CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A6_Iteration", ] "CLRSLean.FourthEdition.Chapter_16" = [ "CLRSLean.FourthEdition.Chapter_16.Section_16_1_Amortized_Framework", @@ -881,6 +893,30 @@ title = "Farthest-In-Future Eviction" [modules."CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S3_Optimality"] title = "Optimality" +[modules."CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality"] +title = "Optimality Proof" + +[modules."CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace"] +title = "Optimality — Trace Coupling" + +[modules."CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A1_LegalTrace"] +title = "Optimality — Legal Cache Traces" + +[modules."CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A2_OnePageDiff"] +title = "Optimality — Exact One-Page Cache Difference" + +[modules."CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A3_CouplingCore"] +title = "Optimality — Recursive Coupling Core" + +[modules."CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A4_CouplingCorrect"] +title = "Optimality — Coupling Correctness" + +[modules."CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A5_Exchange"] +title = "Optimality — One-Step FIF Exchange" + +[modules."CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A6_Iteration"] +title = "Optimality — Finite Exchange Iteration" + [modules."CLRSLean.FourthEdition.Chapter_16"] title = "Chapter 16. Amortized Analysis"