Skip to content
  1. CLRS-Lean
  2. Chapters 1–35 · CLRS Fourth Edition
  3. Chapter 15. Greedy Algorithms
  4. 15.4. Offline caching
Browse chapters
Imports
import Mathlib 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.S3_Optimality import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.EmptyStart

15.4. Offline caching

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 the finite-trace exchange proof that the policy is optimal.

Main results:

  • Policy / Policy.step / misses: the caching model (CLRS §15.4)

  • nextUse: the next request position of a page at or after a position

  • Farther: the "at least as far in the future" order

  • 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: optimality for every nonempty eviction-phase cache

  • fifo_optimal_from_empty: optimality from the literal empty cache in the capacity-one core execution, including the compulsory first miss

  • fifo_optimal_after_compulsory_fill: the capacity-independent bridge from a common compulsory-fill phase to the verified eviction phase

Completion boundary:

  • The mathematical offline-caching optimality theorem is complete for finite request lists. Both a nonempty eviction-phase cache and the literal empty start of the core transition semantics are covered. The latter has capacity one after the first load. For larger capacities, compulsoryFillCost only adds a supplied common cost to a supplied nonempty resident set and remaining suffix; no general capacity-parametric empty-start fill execution is proved here. 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:

  • C : cache (a Finset Page of resident pages)

  • σ : request sequence

  • i : position of the fault

  • π : eviction policy

Implementation details

The section is split into the following sub-modules:

Definitions and proofs

CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S1_Cache_Model

S1. Cache model

The eviction-cache model for the offline caching problem of CLRS §15.4 ("Offline caching"): a request sequence is a list of pages, the cache is a finite set of resident pages, and an eviction policy is a total function that decides, at each fault, which resident page to evict. Misses and hits are counted position by position over the request list, and nextUse locates the next request of a given page at or after a given position.

Main results:

  • Policy: an eviction policy (a total eviction function, validity bundled)

  • Policy.step: the cache transition induced by a policy on a request

  • cacheSeq: the cache after each prefix of the request list

  • faultAt / misses / hits: per-request miss indicator and the total miss and hit counts over the request list

  • misses_add_hits: every request is a hit or a miss

  • step_card / cacheSeq_card: policies preserve the cache size, so a cache of size k stays of size k throughout the run

  • nextUse: the offset of the first request of a page at or after a given position, none when the page is never requested again

Notation conventions used in this section:

  • C : cache (a finite set of resident pages)

  • σ : request sequence

  • p, q : pages

  • i, t : positions in the request sequence

namespace CLRSopen Finsetopen scoped BigOperatorsnamespace Caching

Pages are natural numbers; any countably infinite page universe is equivalent.

abbrev Page := ℕ

A cache of size k holds exactly k pages (CLRS §15.4).

def CacheSize (k : ℕ) (C : Finset Page) : Prop := C.card = k

An eviction policy is a total function that, at each request position i, given the current cache C and the requested page p, returns the page to evict when p is not resident. The bundled evict_mem field records that a fault evicts a resident page; on a hit the eviction value is junk. Policies are offline: they may use the position i (and hence the full request sequence) when making the decision (CLRS §15.4).

structure Policy where evict : ℕ → Finset Page → Page → Page evict_mem : ∀ i C p, p ∉ C → C.Nonempty → evict i C p ∈ C

The cache transition of a policy: a hit keeps the cache unchanged, a fault evicts the policy's chosen page and loads the requested page.

def Policy.step (π : Policy) (i : ℕ) (C : Finset Page) (p : Page) : Finset Page := if p ∈ C then C else insert p (C.erase (π.evict i C p))

The cache after the first t requests (requests beyond the end of the list are junk, so the sequence extends arbitrarily).

def cacheSeq (π : Policy) (C₀ : Finset Page) (σ : List Page) : ℕ → Finset Page | 0 => C₀ | t + 1 => π.step t (cacheSeq π C₀ σ t) (σ.getD t 0)

The transition preserves the number of resident pages.

lemma step_card (π : Policy) (i : ℕ) (C : Finset Page) (p : Page) (hC : C.Nonempty) : (π.step i C p).card = C.card := by unfold Policy.step by_cases hp : p ∈ C · rw [if_pos hp] · rw [if_neg hp] have he := π.evict_mem i C p hp hC rw [Finset.card_insert_of_notMem (by intro hmem exact hp (Finset.mem_erase.mp hmem).2)] rw [Finset.card_erase_of_mem he] have hcard : 0 < C.card := Finset.card_pos.mpr ⟨π.evict i C p, he⟩ omega

Every cache in the run of a policy has the same size as the initial cache, so a cache of size k stays of size k throughout (CLRS §15.4).

lemma cacheSeq_card (π : Policy) (C₀ : Finset Page) (σ : List Page) (t : ℕ) (hC₀ : C₀.Nonempty) : (cacheSeq π C₀ σ t).card = C₀.card := by induction t with | zero => rfl | succ t ih => unfold cacheSeq rw [step_card] · exact ih · have hcard : 0 < (cacheSeq π C₀ σ t).card := by rw [ih] exact Finset.card_pos.mpr hC₀ exact Finset.card_pos.mp hcard

Caches in a run starting from a nonempty cache are nonempty.

lemma cacheSeq_nonempty (π : Policy) (C₀ : Finset Page) (σ : List Page) (t : ℕ) (hC₀ : C₀.Nonempty) : (cacheSeq π C₀ σ t).Nonempty := by have hcard : 0 < (cacheSeq π C₀ σ t).card := by rw [cacheSeq_card π C₀ σ t hC₀] exact Finset.card_pos.mpr hC₀ exact Finset.card_pos.mp hcard

Whether the request at position t is a miss for the run of π from C₀ on σ (0 or 1).

def faultAt (π : Policy) (C₀ : Finset Page) (σ : List Page) (t : ℕ) : ℕ := if σ.getD t 0 ∈ cacheSeq π C₀ σ t then 0 else 1

The number of misses (faults) incurred by policy π on the request list σ starting from the initial cache C₀ (CLRS §15.4).

def misses (π : Policy) (C₀ : Finset Page) (σ : List Page) : ℕ := ∑ t ∈ Finset.range σ.length, faultAt π C₀ σ t

The number of hits (requests served from the cache) incurred by policy π on the request list σ starting from the initial cache C₀.

def hits (π : Policy) (C₀ : Finset Page) (σ : List Page) : ℕ := ∑ t ∈ Finset.range σ.length, if σ.getD t 0 ∈ cacheSeq π C₀ σ t then 1 else 0

A sum over a shifted range splits into its first term and the shifted tail.

lemma sum_range_shift {n : ℕ} (f : ℕ → ℕ) : (∑ t ∈ Finset.range (n + 1), f t) = f 0 + ∑ t ∈ Finset.range n, f (t + 1) := by induction n with | zero => simp | succ n ih => rw [Finset.sum_range_succ, ih] rw [Finset.sum_range_succ] omega

Every request is either a hit or a miss, so the two counts add up to the length of the request list.

lemma misses_add_hits (π : Policy) (C₀ : Finset Page) (σ : List Page) : misses π C₀ σ + hits π C₀ σ = σ.length := by unfold misses hits rw [← Finset.sum_add_distrib] have hterm : ∀ t ∈ Finset.range σ.length, faultAt π C₀ σ t + (if σ.getD t 0 ∈ cacheSeq π C₀ σ t then 1 else 0) = 1 := by intro t _ unfold faultAt split <;> omega rw [Finset.sum_congr rfl hterm] simp

The offset of the first request of p at or after position i in σ: nextUse σ i p = some j means the request at absolute position i + j is the first request of p at or after i; none means p is never requested again (CLRS §15.4).

def nextUse (σ : List Page) (i : ℕ) (p : Page) : Option ℕ := (σ.drop i).findIdx? (fun q => q = p)

nextUse σ i p = some j exactly when the request at relative position j of the suffix σ.drop i is p and no earlier request of the suffix is p.

lemma nextUse_eq_some_iff {σ : List Page} {i p j : ℕ} : nextUse σ i p = some j ↔ ∃ h : j < (σ.drop i).length, (σ.drop i)[j] = p ∧ ∀ k (hk : k < j), (σ.drop i)[k] ≠ p := by unfold nextUse rw [List.findIdx?_eq_some_iff_getElem (p := fun q => q = p) (xs := σ.drop i)] simp

nextUse σ i p = none exactly when no request at or after position i is p.

lemma nextUse_eq_none_iff {σ : List Page} {i p : ℕ} : nextUse σ i p = none ↔ ∀ q, q ∈ σ.drop i → q ≠ p := by unfold nextUse rw [List.findIdx?_eq_none_iff] simp

The element of a drop at a relative position is the element of the original list at the shifted absolute position.

lemma getD_drop (l : List Page) (d : Page) (i j : ℕ) : (l.drop i).getD j d = l.getD (i + j) d := by rw [List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD] simp

If nextUse σ i p = some j, then the request at absolute position i + j is p, and no request strictly between i and i + j is p.

lemma getD_nextUse {σ : List Page} {i p j : ℕ} (h : nextUse σ i p = some j) : σ.getD (i + j) 0 = p ∧ ∀ k, i ≤ k → k < i + j → σ.getD k 0 ≠ p := by rcases (nextUse_eq_some_iff.mp h) with ⟨hlt, hget, hmin⟩ constructor · rw [← getD_drop σ 0 i j] rw [List.getD_eq_getElem _ 0 hlt] exact hget · intro k hik hkj have hki : k - i < j := by omega have hne := hmin (k - i) hki have hget' : (σ.drop i).getD (k - i) 0 = σ.getD k 0 := by have hsub : (σ.drop i).getD (k - i) 0 = σ.getD (i + (k - i)) 0 := by rw [getD_drop σ 0 i (k - i)] rw [hsub] rw [Nat.add_sub_of_le hik] rw [← hget'] rw [List.getD_eq_getElem _ 0 (Nat.lt_trans hki hlt)] exact hne

If nextUse σ i p = some j, then the request at absolute position i + j is p.

lemma getD_eq_nextUse {σ : List Page} {i p j : ℕ} (h : nextUse σ i p = some j) : σ.getD (i + j) 0 = p := (getD_nextUse h).1

If nextUse σ i p = some j, then no request strictly between i and i + j is p.

lemma getD_ne_nextUse {σ : List Page} {i p j : ℕ} (h : nextUse σ i p = some j) {k : ℕ} (hik : i ≤ k) (hkj : k < i + j) : σ.getD k 0 ≠ p := (getD_nextUse h).2 k hik hkj
end Cachingend CLRS

CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S2_Farthest_In_Future

S2. The farthest-in-future eviction

The greedy choice of the offline caching problem (CLRS §15.4): when a fault occurs, evict the resident page whose next use is farthest in the future. Pages never requested again count as farthest (none). Ties are broken arbitrarily (towards the left in the enumeration order of the cache).

Main results:

  • Farther: the "at least as far in the future" order on next-use options (none = never again is the farthest)

  • farthestInFuture cache σ i: the resident page whose next use at or after position i is farthest

  • mem_farthestInFuture: the chosen page is resident

  • farthestInFuture_max: no resident page has a farther next use

  • fifoPolicy σ: the farthest-in-future eviction policy for σ

  • fifo_step_of_mem / fifo_step_fault: the cache transition of the policy

Notation conventions used in this section:

  • C : cache

  • σ : request sequence

  • i : position of the fault

namespace CLRSopen Finsetnamespace Caching

Farther a b says that the next use a is at least as far in the future as b: none (never requested again) is the farthest, and among some i / some j the one with the larger position is farther (CLRS §15.4).

def Farther (a b : Option ℕ) : Prop := match a, b with | none, _ => True | some _, none => False | some i, some j => j ≤ i

Farther-in-the-future is reflexive.

lemma farther_refl (a : Option ℕ) : Farther a a := by cases a <;> simp [Farther]

Farther-in-the-future is transitive.

lemma farther_trans {a b c : Option ℕ} (hab : Farther a b) (hbc : Farther b c) : Farther a c := by cases a with | none => simp [Farther] | some i => cases b with | none => simp [Farther] at hab | some j => cases c with | none => simp [Farther] at hbc | some k => simp [Farther] at hab hbc ⊢ omega

Farther-in-the-future is total.

lemma farther_total {a b : Option ℕ} (h : ¬ Farther a b) : Farther b a := by cases a with | none => simp [Farther] at h | some i => cases b with | none => simp [Farther] | some j => simp [Farther] at h ⊢ omega

If a is at least as far as b, then either a is none, or both are some with b's position no later than a's.

lemma farther_cases {a b : Option ℕ} (h : Farther a b) : a = none ∨ ∃ i j, a = some i ∧ b = some j ∧ j ≤ i := by cases a with | none => exact Or.inl rfl | some i => cases b with | none => simp [Farther] at h | some j => exact Or.inr ⟨i, j, rfl, rfl, by simpa [Farther] using h⟩

none is at least as far as any next use.

lemma farther_none (a : Option ℕ) : Farther none a := by cases a <;> simp [Farther]

The farther-in-the-future relation is decidable.

instance instDecidableFarther (a b : Option ℕ) : Decidable (Farther a b) := by unfold Farther cases a <;> cases b <;> infer_instance

A concrete next use is never as far as none.

lemma not_farther_of_some_none {i : ℕ} : ¬ Farther (some i) none := by simp [Farther]

The page in l whose next use under f is farthest in the future, ties broken towards the left; junk value 0 on the empty list.

def farthestInList (f : Page → Option ℕ) : List Page → Page | [] => 0 | p :: rest => if rest = [] then p else let q := farthestInList f rest if Farther (f p) (f q) then p else q

The page chosen by farthestInList is at least as far in the future as every page of the list.

lemma farthestInList_spec (f : Page → Option ℕ) (l : List Page) : ∀ r ∈ l, Farther (f (farthestInList f l)) (f r) := by induction l with | nil => simp [farthestInList] | cons p rest ih => by_cases hrest : rest = [] · rw [hrest] intro r hr simp [farthestInList] at hr ⊢ rw [← hr] exact farther_refl (f r) · by_cases hpq : Farther (f p) (f (farthestInList f rest)) · intro r hr simp [farthestInList, hrest, hpq] at hr ⊢ rcases hr with hr | hr · subst hr exact farther_refl (f r) · exact farther_trans hpq (ih r hr) · intro r hr simp [farthestInList, hrest, hpq] at hr ⊢ rcases hr with rfl | hr · exact farther_total hpq · exact ih r hr

On a nonempty list, farthestInList returns a page of the list.

lemma mem_farthestInList {f : Page → Option ℕ} {l : List Page} (hl : l ≠ []) : farthestInList f l ∈ l := by induction l with | nil => simp at hl | cons p rest ih => by_cases hrest : rest = [] · subst rest simp [farthestInList] · by_cases hpq : Farther (f p) (f (farthestInList f rest)) · simp [farthestInList, hrest, hpq] · simpa [farthestInList, hrest, hpq, List.mem_cons] using (Or.inr (ih hrest))

The resident page of cache whose next use at or after position i is farthest in the future (pages never requested again count as farthest; ties are broken arbitrarily). Junk value 0 on the empty cache (CLRS §15.4).

noncomputable def farthestInFuture (cache : Finset Page) (σ : List Page) (i : ℕ) : Page := farthestInList (fun p => nextUse σ (i + 1) p) cache.toList

On a nonempty cache, farthestInFuture returns a resident page.

lemma mem_farthestInFuture {cache : Finset Page} {σ : List Page} {i : ℕ} (h : cache.Nonempty) : farthestInFuture cache σ i ∈ cache := by unfold farthestInFuture have hmem : farthestInList (fun p => nextUse σ (i + 1) p) cache.toList ∈ cache.toList := by apply mem_farthestInList rcases h with ⟨p, hp⟩ have hp' : p ∈ cache.toList := by simpa [Finset.mem_toList] using hp exact List.ne_nil_of_mem hp' simpa [Finset.mem_toList] using hmem

No resident page has a next use at or after position i that is farther than that of farthestInFuture cache σ i.

lemma farthestInFuture_max {cache : Finset Page} {σ : List Page} {i : ℕ} {p : Page} (hp : p ∈ cache) : Farther (nextUse σ (i + 1) (farthestInFuture cache σ i)) (nextUse σ (i + 1) p) := by unfold farthestInFuture apply farthestInList_spec simpa [Finset.mem_toList] using hp

The farthest-in-future eviction policy for the request list σ (the Belady algorithm, CLRS §15.4): at a fault, evict the resident page whose next use is farthest in the future.

noncomputable def fifoPolicy (σ : List Page) : Policy where evict := fun i C p => farthestInFuture C σ i evict_mem := by intro i C p hp hC exact mem_farthestInFuture hC

The farthest-in-future policy keeps the cache unchanged on a hit.

lemma fifo_step_of_mem (σ : List Page) (i : ℕ) (C : Finset Page) (p : Page) (hp : p ∈ C) : (fifoPolicy σ).step i C p = C := by simp [Policy.step, hp]

On a fault, the farthest-in-future policy evicts the farthest-in-future page and loads the requested page.

lemma fifo_step_fault (σ : List Page) (i : ℕ) (C : Finset Page) (p : Page) (hp : p ∉ C) : (fifoPolicy σ).step i C p = insert p (C.erase (farthestInFuture C σ i)) := by simp [Policy.step, fifoPolicy, hp]
end Cachingend CLRS

CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S3_Optimality

S3. Optimality of the farthest-in-future policy

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 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 / 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

  • 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 eviction schedule; a policy's schedule incurs exactly the policy's misses

  • exchangeSchedule_invariant: from the first disagreement t onwards, the exchange schedule's cache contains every page of d's cache except possibly q and q', so a fault where d hits can only be a request of q or q'

  • exchangeDecision_of_hit / exchangeDecision_of_fault: the exchange eviction at a hit is q, q', or a page d's cache lacks; at a fault it is additionally d s

  • exchangeSchedule_misses_le: one exchange step never increases the miss count — the good event at the first request of q compensates the unique bad event at the first request of q' (or q' is never requested again). The chain of supporting lemmas is proved under a weakened reducedness hypothesis hweak : ∀ s, t ≤ s → fault of dats→d s resident, so the counting lemma applies to schedules that are reduced only from the exchange position on (the iteration's exchange schedules are reduced at every fault after the first q' request, by exchangeSchedule_reduced_after)

  • exchangeSchedule_q_mem / exchangeSchedule_q'_mem: from the first q (resp. q') request on, a page resident in d's cache is also resident in the exchange cache, so bad events are confined to the first q' request

  • fifoSchedule: the eviction schedule of the farthest-in-future policy

  • first_disagree: at a first disagreement of a reduced schedule, both schedules fault, the evictions differ, and the policy's eviction is resident

  • exchange_step: exchanging the first disagreement of a reduced schedule never increases misses and extends agreement with fifoSchedule by one position

  • exchangeSchedule_reduced_after: the exchange schedule is reduced at every fault after the first q' request, so the reducedness state needed by the iteration is preserved from one exchange to the next

  • exchangeSchedule_misses_le_plus_one: when the bad event did not occur (q' never requested again and q is, or d evicts q' before its first request), the exchange saves a spare miss — the compensating slack for the repair step

  • repairSchedule / repair_step: replacing a no-op eviction at the first disagreement by the policy's choice (q', evicted again at its first request so the caches coincide afterwards) costs at most one extra miss and extends agreement by one position, with the window up to J' relation repairSchedule_window and the post-J' containment repairSchedule_superset

Current gaps:

  • None for optimality in the mathematical cache model. Low-level RAM/cache implementation refinement is outside this section's current model.

namespace CLRSnamespace Cachingopen Finset

The farthest-in-future policy always evicts a resident page.

lemma fifo_evicts_resident (σ : List Page) (i : ℕ) (C : Finset Page) (p : Page) (hp : p ∉ C) (hC : C.Nonempty) : (fifoPolicy σ).evict i C p ∈ C := (fifoPolicy σ).evict_mem i C p hp hC

A step of the farthest-in-future policy preserves the cache size.

lemma fifo_step_size (σ : List Page) (i : ℕ) (C : Finset Page) (p : Page) (hC : C.Nonempty) : ((fifoPolicy σ).step i C p).card = C.card := step_card (fifoPolicy σ) i C p hC

A schedule for the request list σ is a decision function d : ℕ → Page giving, for every position s, the page to evict at that position. The schedule's run schedCache d C₀ σ starts from C₀: a hit keeps the cache, a fault evicts d s (an eviction of an absent page is a no-op, so schedules need not be reduced) and loads the requested page.

def schedCache (d : ℕ → Page) (C₀ : Finset Page) (σ : List Page) : ℕ → Finset Page | 0 => C₀ | s + 1 => if σ.getD s 0 ∈ schedCache d C₀ σ s then schedCache d C₀ σ s else insert (σ.getD s 0) ((schedCache d C₀ σ s).erase (d s))

Whether position s is a miss for the schedule d from C₀ on σ (0 or 1).

def schedFaultAt (d : ℕ → Page) (C₀ : Finset Page) (σ : List Page) (s : ℕ) : ℕ := if σ.getD s 0 ∈ schedCache d C₀ σ s then 0 else 1

The number of misses of the schedule d from C₀ on σ.

def schedMisses (d : ℕ → Page) (C₀ : Finset Page) (σ : List Page) : ℕ := ∑ s ∈ Finset.range σ.length, schedFaultAt d C₀ σ s

The schedule induced by a policy: at position s it evicts exactly the page the policy evicts in its own run.

def policySchedule (π : Policy) (C₀ : Finset Page) (σ : List Page) : ℕ → Page := fun s => π.evict s (cacheSeq π C₀ σ s) (σ.getD s 0)

The run of a policy's schedule is the policy's own run.

lemma schedCache_policySchedule (π : Policy) (C₀ : Finset Page) (σ : List Page) (s : ℕ) : schedCache (policySchedule π C₀ σ) C₀ σ s = cacheSeq π C₀ σ s := by induction s with | zero => rfl | succ s ih => unfold schedCache rw [ih] cases s with | zero => rfl | succ s' => unfold cacheSeq rfl

A policy and its schedule incur the same number of misses.

lemma schedMisses_policySchedule (π : Policy) (C₀ : Finset Page) (σ : List Page) : schedMisses (policySchedule π C₀ σ) C₀ σ = misses π C₀ σ := by unfold schedMisses misses faultAt apply Finset.sum_congr rfl intro s hs unfold schedFaultAt rw [schedCache_policySchedule]

The exchange schedule for the first fault where d and the farthest-in-future policy disagree (position t, request p, d evicting q, the policy evicting q'): it agrees with d before t, evicts q' at t, and afterwards follows d except that it never evicts a page that d keeps while the exchange schedule lacks it (when d evicts q' the exchange schedule evicts q' too — a no-op when it already lacks q' — and a multi-set element — a page d does not have — when d hits a request of q or q' that the exchange schedule misses), so that no bad event (a fault where d hits) is created.

The eviction decision at position s, based on the exchange schedule's cache C' (the cache just before the request at s) and d's cache.

noncomputable def exchangeDecision (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ C' : Finset Page) (s : ℕ) : Page := if s < t then d s else if s = t then q' else if d s = q' then q' else if (σ.getD s 0 = q' ∨ σ.getD s 0 = q) ∧ σ.getD s 0 ∈ schedCache d C₀ σ s then let M : Finset Page := C' \ schedCache d C₀ σ s if h : (M.filter (fun x => x ≠ q')).Nonempty then Classical.choose h else if h : M.Nonempty then Classical.choose h else 0 else if d s ∈ C' then d s else let M : Finset Page := C' \ schedCache d C₀ σ s if h : M.Nonempty then Classical.choose h else 0
noncomputable def exchangeScheduleCore (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) : ℕ → Finset Page × Page | 0 => (C₀, exchangeDecision d t q q' σ C₀ C₀ 0) | s + 1 => let prev := exchangeScheduleCore d t q q' σ C₀ s let r : Page := σ.getD s 0 let Csucc : Finset Page := if r ∈ prev.1 then prev.1 else insert r (prev.1.erase prev.2) (Csucc, exchangeDecision d t q q' σ C₀ Csucc (s + 1))

The decision function of the exchange schedule.

noncomputable def exchangeSchedule (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) : ℕ → Page := fun s => (exchangeScheduleCore d t q q' σ C₀ s).2

The exchange schedule's run is the cache component of the core.

lemma schedCache_exchangeScheduleCore (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) (s : ℕ) : schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s = (exchangeScheduleCore d t q q' σ C₀ s).1 := by induction s with | zero => rfl | succ s ih => unfold schedCache rw [ih] cases s with | zero => rfl | succ s' => unfold exchangeScheduleCore rfl

Strictly before t, the exchange schedule's cache and decision agree with d's.

lemma exchangeScheduleCore_eq_d (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) {s : ℕ} (hs : s < t) : exchangeScheduleCore d t q q' σ C₀ s = (schedCache d C₀ σ s, d s) := by induction s with | zero => unfold exchangeScheduleCore simp [exchangeDecision, hs] rfl | succ s ih => rw [exchangeScheduleCore] rw [ih (lt_trans (Nat.lt_succ_self s) hs)] simp [exchangeDecision, hs] cases s with | zero => rfl | succ s' => unfold schedCache rfl

The exchange schedule agrees with d strictly before t.

lemma exchangeSchedule_eq_d_of_lt (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) {s : ℕ} (hs : s < t) : exchangeSchedule d t q q' σ C₀ s = d s := by unfold exchangeSchedule rw [exchangeScheduleCore_eq_d d t q q' σ C₀ hs]

Up to and including position t, the exchange schedule's cache agrees with d's.

lemma schedCache_exchangeSchedule_eq_d (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) {s : ℕ} (hs : s ≤ t) : schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s = schedCache d C₀ σ s := by induction s with | zero => rfl | succ s ih => unfold schedCache rw [exchangeSchedule_eq_d_of_lt d t q q' σ C₀ (Nat.lt_of_succ_le hs)] rw [ih (by omega)]

The exchange schedule evicts q' at position t.

lemma exchangeSchedule_at_t (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) : exchangeSchedule d t q q' σ C₀ t = q' := by unfold exchangeSchedule exchangeScheduleCore induction t with | zero => simp [exchangeDecision] | succ t ih => unfold exchangeScheduleCore simp [exchangeDecision]

A reduced schedule's cache size is constant (evictions hit resident pages and faults load a page that was absent).

lemma schedCache_card_const (d : ℕ → Page) (C₀ : Finset Page) (σ : List Page) (t : ℕ) (hweak : ∀ s, t ≤ s → σ.getD s 0 ∉ schedCache d C₀ σ s → d s ∈ schedCache d C₀ σ s) {s : ℕ} (hts : t ≤ s) : (schedCache d C₀ σ (s + 1)).card = (schedCache d C₀ σ s).card := by rw [schedCache] by_cases hr : σ.getD s 0 ∈ schedCache d C₀ σ s · rw [if_pos hr] · rw [if_neg hr] rw [Finset.card_insert_of_notMem] · rw [Finset.card_erase_of_mem (hweak s hts hr)] have hc : 0 < (schedCache d C₀ σ s).card := Finset.card_pos.mpr ⟨d s, hweak s hts hr⟩ omega · intro hm exact hr (Finset.mem_erase.mp hm).2

One step never shrinks the exchange schedule's cache.

lemma exchangeScheduleCore_card_step (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) (s : ℕ) : (exchangeScheduleCore d t q q' σ C₀ (s + 1)).1.card ≥ (exchangeScheduleCore d t q q' σ C₀ s).1.card := by rw [exchangeScheduleCore] by_cases hr : σ.getD s 0 ∈ (exchangeScheduleCore d t q q' σ C₀ s).1 · rw [if_pos hr] · rw [if_neg hr] rw [Finset.card_insert_of_notMem] · have hle : ((exchangeScheduleCore d t q q' σ C₀ s).1.erase (exchangeScheduleCore d t q q' σ C₀ s).2).card + 1 ≥ (exchangeScheduleCore d t q q' σ C₀ s).1.card := by by_cases hx : (exchangeScheduleCore d t q q' σ C₀ s).2 ∈ (exchangeScheduleCore d t q q' σ C₀ s).1 · rw [Finset.card_erase_of_mem hx] omega · simp [hx] omega · intro hm exact hr (Finset.mem_erase.mp hm).2

The exchange schedule's cache never shrinks below d's: from t onwards it has at least as many pages as d's cache.

lemma exchangeScheduleCore_card (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) (hweak : ∀ s, t ≤ s → σ.getD s 0 ∉ schedCache d C₀ σ s → d s ∈ schedCache d C₀ σ s) {s : ℕ} (hs : t ≤ s) : (exchangeScheduleCore d t q q' σ C₀ s).1.card ≥ (schedCache d C₀ σ s).card := by have hmono : (exchangeScheduleCore d t q q' σ C₀ s).1.card ≥ (exchangeScheduleCore d t q q' σ C₀ t).1.card := by induction s with | zero => have ht : t = 0 := by omega subst t rfl | succ s ih => by_cases hst : t ≤ s · exact le_trans (ih hst) (exchangeScheduleCore_card_step d t q q' σ C₀ s) · have hs' : s + 1 = t := by omega rw [← schedCache_exchangeScheduleCore] rw [← schedCache_exchangeScheduleCore] rw [schedCache_exchangeSchedule_eq_d d t q q' σ C₀ (le_of_eq hs')] rw [schedCache_exchangeSchedule_eq_d d t q q' σ C₀ le_rfl] rw [hs'] have hbase : (exchangeScheduleCore d t q q' σ C₀ t).1.card = (schedCache d C₀ σ t).card := by rw [← schedCache_exchangeScheduleCore] rw [schedCache_exchangeSchedule_eq_d d t q q' σ C₀ le_rfl] have hconst : (schedCache d C₀ σ s).card = (schedCache d C₀ σ t).card := by have h : ∀ n, (schedCache d C₀ σ (t + n)).card = (schedCache d C₀ σ t).card := by intro n induction n with | zero => rfl | succ n ih => rw [Nat.add_succ] rw [schedCache_card_const d C₀ σ t hweak (s := t + n) (by omega)] exact ih have hs' : s = t + (s - t) := by omega rw [hs'] exact h (s - t) rw [hconst] rw [← hbase] exact hmono

The decision component of the core is the exchange decision at the same position.

lemma exchangeScheduleCore_second (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) (s : ℕ) : (exchangeScheduleCore d t q q' σ C₀ s).2 = exchangeDecision d t q q' σ C₀ (exchangeScheduleCore d t q q' σ C₀ s).1 s := by induction s with | zero => rfl | succ s ih => rw [exchangeScheduleCore]

When d hits at s and the exchange schedule faults, the exchange eviction at s is q, q', or a page d's cache lacks.

lemma exchangeDecision_of_hit (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ C' : Finset Page) {s : ℕ} (hst : t < s) (hr : σ.getD s 0 ∈ schedCache d C₀ σ s) (hr' : σ.getD s 0 ∉ C') (hrqq : σ.getD s 0 = q' ∨ σ.getD s 0 = q) (hcard : (schedCache d C₀ σ s).card ≤ C'.card) : exchangeDecision d t q q' σ C₀ C' s = q ∨ exchangeDecision d t q q' σ C₀ C' s = q' ∨ exchangeDecision d t q q' σ C₀ C' s ∉ schedCache d C₀ σ s := by unfold exchangeDecision have hlt : ¬ s < t := by omega have hne : ¬ s = t := by omega rw [if_neg hlt, if_neg hne] by_cases h1 : d s = q' · rw [if_pos h1] exact Or.inr (Or.inl rfl) · rw [if_neg h1] by_cases h2 : (σ.getD s 0 = q' ∨ σ.getD s 0 = q) ∧ σ.getD s 0 ∈ schedCache d C₀ σ s · rw [if_pos h2] by_cases hf : ((C' \ schedCache d C₀ σ s).filter (fun x => x ≠ q')).Nonempty · rw [dif_pos hf] right; right have hspec := Classical.choose_spec hf intro hdec exact (Finset.mem_sdiff.mp (Finset.mem_filter.mp hspec).1).2 hdec · rw [dif_neg hf] by_cases hm : (C' \ schedCache d C₀ σ s).Nonempty · rw [dif_pos hm] right; right have hspec := Classical.choose_spec hm intro hdec exact (Finset.mem_sdiff.mp hspec).2 hdec · rw [dif_neg hm] exfalso have hsub : C' ⊆ schedCache d C₀ σ s := by intro y hy by_contra hyn exact hm ⟨y, Finset.mem_sdiff.mpr ⟨hy, hyn⟩⟩ have hEq : C' = schedCache d C₀ σ s := Finset.eq_of_subset_of_card_le hsub hcard have hrC' : σ.getD s 0 ∈ C' := by rw [hEq] exact hr exact hr' hrC' · rw [if_neg h2] exfalso exact h2 ⟨hrqq, hr⟩

When d faults at s, the exchange eviction at s is q, q', d s, or a page d's cache lacks.

lemma exchangeDecision_of_fault (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ C' : Finset Page) (hweak : ∀ s, t ≤ s → σ.getD s 0 ∉ schedCache d C₀ σ s → d s ∈ schedCache d C₀ σ s) {s : ℕ} (hst : t < s) (hr : σ.getD s 0 ∉ schedCache d C₀ σ s) (hcard : (schedCache d C₀ σ s).card ≤ C'.card) : exchangeDecision d t q q' σ C₀ C' s = q ∨ exchangeDecision d t q q' σ C₀ C' s = q' ∨ exchangeDecision d t q q' σ C₀ C' s = d s ∨ exchangeDecision d t q q' σ C₀ C' s ∉ schedCache d C₀ σ s := by unfold exchangeDecision have hlt : ¬ s < t := by omega have hne : ¬ s = t := by omega rw [if_neg hlt, if_neg hne] by_cases h1 : d s = q' · rw [if_pos h1] exact Or.inr (Or.inl rfl) · rw [if_neg h1] by_cases h2 : (σ.getD s 0 = q' ∨ σ.getD s 0 = q) ∧ σ.getD s 0 ∈ schedCache d C₀ σ s · exfalso exact hr h2.2 · rw [if_neg h2] by_cases h3 : d s ∈ C' · rw [if_pos h3] exact Or.inr (Or.inr (Or.inl rfl)) · rw [if_neg h3] by_cases hm : (C' \ schedCache d C₀ σ s).Nonempty · rw [dif_pos hm] right; right; right have hspec := Classical.choose_spec hm intro hdec exact (Finset.mem_sdiff.mp hspec).2 hdec · rw [dif_neg hm] exfalso have hsub : C' ⊆ schedCache d C₀ σ s := by intro y hy by_contra hyn exact hm ⟨y, Finset.mem_sdiff.mpr ⟨hy, hyn⟩⟩ have hEq : C' = schedCache d C₀ σ s := Finset.eq_of_subset_of_card_le hsub hcard have hds : d s ∈ C' := by rw [hEq] exact hweak s (by omega) hr exact h3 hds

The invariant of the exchange schedule: for every position s ≥ t+1, the exchange schedule's cache contains every page of d's cache except possibly q and q'. Consequently a fault of d on a request outside {q, q'} is never a hit of the exchange schedule — bad events (faults where d hits) can only happen on requests of q or q'.

lemma exchangeSchedule_invariant (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) (hq : d t = q) (hweak : ∀ s, t ≤ s → σ.getD s 0 ∉ schedCache d C₀ σ s → d s ∈ schedCache d C₀ σ s) : ∀ s ≥ t + 1, ∀ x, x ∉ ({q, q'} : Finset Page) → x ∈ schedCache d C₀ σ s → x ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s := by intro s hs induction s with | zero => omega | succ s ih => intro x hx hmem by_cases hst : s = t · -- base: after the request at t, the caches differ only in q vs q' subst s rw [schedCache_exchangeScheduleCore] rw [exchangeScheduleCore] dsimp rw [show (exchangeScheduleCore d t q q' σ C₀ t).1 = schedCache d C₀ σ t by rw [← schedCache_exchangeScheduleCore] exact schedCache_exchangeSchedule_eq_d d t q q' σ C₀ le_rfl] rw [show (exchangeScheduleCore d t q q' σ C₀ t).2 = q' by exact exchangeSchedule_at_t d t q q' σ C₀] unfold schedCache at hmem rw [hq] at hmem by_cases hp : σ.getD t 0 ∈ schedCache d C₀ σ t · rw [if_pos hp] at hmem ⊢ exact hmem · rw [if_neg hp] at hmem ⊢ rcases Finset.mem_insert.mp hmem with hxeq | hxin · rw [hxeq] exact Finset.mem_insert_self (σ.getD t 0) ((schedCache d C₀ σ t).erase q') · have hxq' : x ≠ q' := by intro h exact hx (by simp [h]) exact Finset.mem_insert_of_mem (Finset.mem_erase.mpr ⟨hxq', (Finset.mem_erase.mp hxin).2⟩) · -- step: s > t have hs' : t + 1 ≤ s := by omega have hst : t < s := by omega have ih' := ih hs' rw [schedCache_exchangeScheduleCore] rw [exchangeScheduleCore] dsimp rw [show (exchangeScheduleCore d t q q' σ C₀ s).1 = schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s by rw [← schedCache_exchangeScheduleCore]] rw [show (exchangeScheduleCore d t q q' σ C₀ s).2 = exchangeDecision d t q q' σ C₀ (schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s) s by rw [exchangeScheduleCore_second] congr 1 rw [← schedCache_exchangeScheduleCore]] by_cases hr : σ.getD s 0 ∈ schedCache d C₀ σ s · -- d hits at s unfold schedCache at hmem rw [if_pos hr] at hmem by_cases hr' : σ.getD s 0 ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s · -- the exchange schedule hits too: no eviction rw [if_pos hr'] exact ih' x hx hmem · -- d hits, the exchange schedule faults: the decision evicts q, q', -- or a page d's cache lacks, so x survives rw [if_neg hr'] have hrqq : σ.getD s 0 = q' ∨ σ.getD s 0 = q := by by_contra hnot exact hr' (ih' (σ.getD s 0) (by intro hmem apply hnot rcases Finset.mem_insert.mp hmem with hqeq | hq' · exact Or.inr hqeq · exact Or.inl (Finset.mem_singleton.mp hq')) hr) have hcard : (schedCache d C₀ σ s).card ≤ (schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s).card := by rw [schedCache_exchangeScheduleCore] exact exchangeScheduleCore_card d t q q' σ C₀ hweak (by omega) have hdec := exchangeDecision_of_hit d t q q' σ C₀ (schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s) hst hr hr' hrqq hcard have hxq : x ≠ q := by intro h exact hx (by simp [h]) have hxq' : x ≠ q' := by intro h exact hx (by simp [h]) have hxne : x ≠ exchangeDecision d t q q' σ C₀ (schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s) s := by intro hxdec rcases hdec with hdecq | hdecq' | hdecnot · exact hxq (hxdec.trans hdecq) · exact hxq' (hxdec.trans hdecq') · exact hdecnot (hxdec ▸ hmem) have hxC' : x ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s := ih' x hx hmem exact Finset.mem_insert_of_mem (Finset.mem_erase.mpr ⟨hxne, hxC'⟩) · -- d faults at s unfold schedCache at hmem rw [if_neg hr] at hmem by_cases hr' : σ.getD s 0 ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s · -- the exchange schedule hits: its cache is unchanged rw [if_pos hr'] rcases Finset.mem_insert.mp hmem with hxr | hxin · rw [hxr] exact hr' · exact ih' x hx (Finset.mem_erase.mp hxin).2 · -- both fault: r is inserted, and the decision evicts q, q', d s, or -- a page d's cache lacks, so x survives rw [if_neg hr'] rcases Finset.mem_insert.mp hmem with hxr | hxin · rw [hxr] exact Finset.mem_insert_self (σ.getD s 0) _ · have hxC_d : x ∈ schedCache d C₀ σ s := (Finset.mem_erase.mp hxin).2 have hxne_ds : x ≠ d s := (Finset.mem_erase.mp hxin).1 have hcard : (schedCache d C₀ σ s).card ≤ (schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s).card := by rw [schedCache_exchangeScheduleCore] exact exchangeScheduleCore_card d t q q' σ C₀ hweak (by omega) have hdec := exchangeDecision_of_fault d t q q' σ C₀ (schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s) hweak hst hr hcard have hxq : x ≠ q := by intro h exact hx (by simp [h]) have hxq' : x ≠ q' := by intro h exact hx (by simp [h]) have hxne : x ≠ exchangeDecision d t q q' σ C₀ (schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s) s := by intro hxdec rcases hdec with hdecq | hdecq' | hdecds | hdecnot · exact hxq (hxdec.trans hdecq) · exact hxq' (hxdec.trans hdecq') · exact hxne_ds (hxdec.trans hdecds) · exact hdecnot (hxdec ▸ hxC_d) have hxC' : x ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s := ih' x hx hxC_d exact Finset.mem_insert_of_mem (Finset.mem_erase.mpr ⟨hxne, hxC'⟩)

If q' is the farthest-in-future page of a cache at position i and q is a different resident page, then either q' is never requested again, or q's next request comes strictly before q''s next request.

lemma fifo_nextUse_order (σ : List Page) (cache : Finset Page) (i : ℕ) (q' q : Page) (hq' : q' = farthestInFuture cache σ i) (hq : q ∈ cache) (hqq' : q ≠ q') : nextUse σ (i + 1) q' = none ∨ ∃ j j', nextUse σ (i + 1) q = some j ∧ nextUse σ (i + 1) q' = some j' ∧ j < j' := by have hmax := farthestInFuture_max (σ := σ) (i := i) (p := q) hq rw [← hq'] at hmax have hc := farther_cases hmax rcases hc with hnone' | ⟨jq', jq, hq'eq, hqeq, hle⟩ · exact Or.inl hnone' · right refine ⟨jq, jq', hqeq, hq'eq, ?_⟩ have hne : jq ≠ jq' := by intro hjj have hget := getD_eq_nextUse hqeq have hget' := getD_eq_nextUse hq'eq rw [hjj] at hget exact hqq' (hget.symm.trans hget') omega

Before the first request of q (inclusive), d's cache does not contain q (d evicts q at t, and q is not requested within (t, J)).

lemma d_cache_ne_q (d : ℕ → Page) (t : ℕ) (q Variable name `q'` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`q' : Page) (σ : List Page) (C₀ : Finset Page) (hq : d t = q) (hweak : ∀ s, t ≤ s → σ.getD s 0 ∉ schedCache d C₀ σ s → d s ∈ schedCache d C₀ σ s) (hft : σ.getD t 0 ∉ schedCache d C₀ σ t) {j : ℕ} (hj : nextUse σ (t + 1) q = some j) {s : ℕ} (hs1 : t < s) (hs2 : s ≤ t + 1 + j) : q ∉ schedCache d C₀ σ s := by induction s with | zero => omega | succ s ih => by_cases hs_eq : s = t · subst s rw [schedCache, hq, if_neg hft] rw [Finset.mem_insert] intro h rcases h with hqr | hqin · have hqinD : q ∈ schedCache d C₀ σ t := by have hd : d t ∈ schedCache d C₀ σ t := hweak t le_rfl hft rw [hq] at hd exact hd exact hft (hqr ▸ hqinD) · exact (by simpa [hq] using (Finset.mem_erase.mp hqin).1) · have hts : t < s := by omega have hsJ : s < t + 1 + j := by omega rw [schedCache] by_cases hr : σ.getD s 0 ∈ schedCache d C₀ σ s · rw [if_pos hr] exact ih hts (by omega) · rw [if_neg hr] intro hmem rcases Finset.mem_insert.mp hmem with hqr | hqin · have hneq := getD_ne_nextUse hj (by omega) hsJ exact hneq hqr.symm · exact ih hts (by omega) (Finset.mem_erase.mp hqin).2

Before the first request of q, the exchange cache differs from d's cache only by the swap of q' and q.

lemma exchangeSchedule_window (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) (hq : d t = q) (hqq' : q ≠ q') (hweak : ∀ s, t ≤ s → σ.getD s 0 ∉ schedCache d C₀ σ s → d s ∈ schedCache d C₀ σ s) (hft : σ.getD t 0 ∉ schedCache d C₀ σ t) (hq'res : q' ∈ schedCache d C₀ σ t) {j : ℕ} (hj : nextUse σ (t + 1) q = some j) (hq'ne : ∀ k, t + 1 ≤ k → k < t + 1 + j → σ.getD k 0 ≠ q') {s : ℕ} (hs1 : t < s) (hs2 : s ≤ t + 1 + j) : schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s = insert q ((schedCache d C₀ σ s).erase q') := by induction s with | zero => omega | succ s ih => by_cases hs_eq : s = t · subst s rw [schedCache_exchangeScheduleCore, exchangeScheduleCore] dsimp rw [show (exchangeScheduleCore d t q q' σ C₀ t).1 = schedCache d C₀ σ t by rw [← schedCache_exchangeScheduleCore] exact schedCache_exchangeSchedule_eq_d d t q q' σ C₀ le_rfl] rw [show (exchangeScheduleCore d t q q' σ C₀ t).2 = q' by exact exchangeSchedule_at_t d t q q' σ C₀] rw [if_neg hft] rw [schedCache] rw [hq] rw [if_neg hft] -- goal: insert r (D(t) − q') = insert q ((insert r (D(t) − q)) − q') have hqin : q ∈ schedCache d C₀ σ t := by have hd : d t ∈ schedCache d C₀ σ t := hweak t le_rfl hft rw [hq] at hd exact hd have hr_ne_q : σ.getD t 0 ≠ q := by intro h exact hft (h ▸ hqin) have hr_ne_q' : σ.getD t 0 ≠ q' := by intro h exact hft (h ▸ hq'res) apply Finset.ext intro x constructor · intro hx rw [Finset.mem_insert] rcases Finset.mem_insert.mp hx with hxr | hxin · subst x right rw [Finset.mem_erase] constructor · exact hr_ne_q' · rw [Finset.mem_insert] left rfl · by_cases hxq : x = q · left exact hxq · right rw [Finset.mem_erase] constructor · exact (Finset.mem_erase.mp hxin).1 · rw [Finset.mem_insert] right exact Finset.mem_erase.mpr ⟨hxq, (Finset.mem_erase.mp hxin).2⟩ · intro hx rw [Finset.mem_insert] at hx rcases hx with hxq | hxin · subst x rw [Finset.mem_insert] right rw [Finset.mem_erase] constructor · exact hqq' · exact hqin · have hxne_q' : x ≠ q' := (Finset.mem_erase.mp hxin).1 rw [Finset.mem_insert] rcases Finset.mem_insert.mp (Finset.mem_erase.mp hxin).2 with hxr | hxin2 · left exact hxr · right rw [Finset.mem_erase] constructor · exact hxne_q' · exact (Finset.mem_erase.mp hxin2).2 · -- step: t < s, process position s have hts : t < s := by omega have hsJ : s < t + 1 + j := by omega have hqne : q ∉ schedCache d C₀ σ s := d_cache_ne_q d t q q' σ C₀ hq hweak hft hj hts (by omega) have hsig_ne_q : σ.getD s 0 ≠ q := getD_ne_nextUse hj (by omega) hsJ have hsig_ne_q' : σ.getD s 0 ≠ q' := hq'ne s (by omega) hsJ rw [schedCache_exchangeScheduleCore, exchangeScheduleCore] dsimp rw [show (exchangeScheduleCore d t q q' σ C₀ s).1 = schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s by rw [← schedCache_exchangeScheduleCore]] rw [show (exchangeScheduleCore d t q q' σ C₀ s).2 = exchangeDecision d t q q' σ C₀ (schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s) s by rw [exchangeScheduleCore_second] congr 1 rw [← schedCache_exchangeScheduleCore]] rw [schedCache] by_cases hr : σ.getD s 0 ∈ schedCache d C₀ σ s · -- both hit rw [if_pos hr] have hrE : σ.getD s 0 ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s := by rw [ih hts (by omega)] rw [Finset.mem_insert] right rw [Finset.mem_erase] constructor · exact hsig_ne_q' · exact hr rw [if_pos hrE] rw [ih hts (by omega)] · -- both fault rw [if_neg hr] have hrE : σ.getD s 0 ∉ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s := by rw [ih hts (by omega)] intro hm rcases Finset.mem_insert.mp hm with hqeq | hmem · exact hsig_ne_q hqeq · exact hr (Finset.mem_erase.mp hmem).2 rw [if_neg hrE] have hw := ih hts (by omega) rw [hw] unfold exchangeDecision have hlt : ¬ s < t := by omega have hne : ¬ s = t := by omega rw [if_neg hlt, if_neg hne] by_cases hdsq' : d s = q' · rw [if_pos hdsq'] rw [hdsq'] -- the erase q' on both sides has no effect have hq'notE : q' ∉ insert q ((schedCache d C₀ σ s).erase q') := by rw [Finset.mem_insert] intro hmem rcases hmem with hq'q | hq'mem · exact hqq' hq'q.symm · exact (Finset.mem_erase.mp hq'mem).1 rfl have hq'notE2 : q' ∉ insert (σ.getD s 0) ((schedCache d C₀ σ s).erase q') := by rw [Finset.mem_insert] intro hmem rcases hmem with hq'q | hq'mem · exact hsig_ne_q' hq'q.symm · exact (Finset.mem_erase.mp hq'mem).1 rfl rw [Finset.erase_eq_of_notMem hq'notE] rw [Finset.erase_eq_of_notMem hq'notE2] -- both sides equal insert q (insert r (D(s) − q')) rw [Finset.insert_comm] · rw [if_neg hdsq'] -- d s ≠ q': branch 4 does not trigger (σ[s] ∉ {q, q'}) by_cases hb4 : (σ.getD s 0 = q' ∨ σ.getD s 0 = q) ∧ σ.getD s 0 ∈ schedCache d C₀ σ s · exfalso exact hb4.1.elim (fun h => hsig_ne_q' h) (fun h => hsig_ne_q h) · rw [if_neg hb4] -- d s ∈ E(s): by the invariant (d s ∈ D(s) and d s ∉ {q, q'}) have hdne : d s ≠ q := by intro hdsq exact hqne (hdsq ▸ hweak s (by omega) hr) have hdE : d s ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s := by have hinv := exchangeSchedule_invariant d t q q' σ C₀ hq hweak s (by omega) exact hinv (d s) (by rw [Finset.mem_insert] intro hmem rcases hmem with hdsq | hdsqmem · exact hdne hdsq · exact hdsq' (Finset.mem_singleton.mp hdsqmem)) (hweak s (by omega) hr) have hdE' : d s ∈ insert q ((schedCache d C₀ σ s).erase q') := by rw [← hw] exact hdE rw [if_pos hdE'] -- dec = d s: both sides are insert q (insert r (D(s) − {q', d s})) rw [Finset.erase_insert_of_ne hdne.symm] rw [Finset.erase_insert_of_ne hsig_ne_q'] have herase_comm : ((schedCache d C₀ σ s).erase q').erase (d s) = ((schedCache d C₀ σ s).erase (d s)).erase q' := by ext x simp [Finset.mem_erase, and_left_comm, This simp argument is unused: and_assoc Hint: Omit it from the simp argument list. simp [Finset.mem_erase, and_left_comm,̵ ̵a̵n̵d̵_̵a̵s̵s̵o̵c̵] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`and_assoc] rw [herase_comm] rw [Finset.insert_comm]

When p is in both d's cache and the exchange cache, the exchange's eviction at s is not p (unless p is q' and d happens to evict q', which is excluded by hpq'; the 0-fallback branch is excluded by h0hit/h0fault together with a cardinality argument).

lemma exchangeDecision_ne (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) (hweak : ∀ s, t ≤ s → σ.getD s 0 ∉ schedCache d C₀ σ s → d s ∈ schedCache d C₀ σ s) {s : ℕ} (hst : t < s) (C' : Finset Page) (p : Page) (Variable name `hpE` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hpE : p ∈ C') (hpD : p ∈ schedCache d C₀ σ s) (hdsq' : d s = q' → p ≠ q') (hdsC' : d s ∈ C' → p ≠ d s) (hcard : (schedCache d C₀ σ s).card ≤ C'.card) (h0hit : σ.getD s 0 ∈ schedCache d C₀ σ s → σ.getD s 0 ∉ C') : exchangeDecision d t q q' σ C₀ C' s ≠ p := by unfold exchangeDecision have hlt : ¬ s < t := by omega have hne : ¬ s = t := by omega rw [if_neg hlt, if_neg hne] by_cases h1 : d s = q' · rw [if_pos h1] intro hpeq exact hdsq' h1 hpeq.symm · rw [if_neg h1] by_cases h2 : (σ.getD s 0 = q' ∨ σ.getD s 0 = q) ∧ σ.getD s 0 ∈ schedCache d C₀ σ s · rw [if_pos h2] by_cases hf : ((C' \ schedCache d C₀ σ s).filter (fun x => x ≠ q')).Nonempty · rw [dif_pos hf] intro hpeq have hspec := Classical.choose_spec hf have hpnotM : p ∉ C' \ schedCache d C₀ σ s := by intro hmem exact (Finset.mem_sdiff.mp hmem).2 hpD exact hpnotM (hpeq ▸ (Finset.mem_filter.mp hspec).1) · rw [dif_neg hf] by_cases hm : (C' \ schedCache d C₀ σ s).Nonempty · rw [dif_pos hm] intro hpeq have hspec := Classical.choose_spec hm have hpnotM : p ∉ C' \ schedCache d C₀ σ s := by rw [Finset.mem_sdiff] intro hmem exact hmem.2 hpD exact hpnotM (hpeq ▸ hspec) · rw [dif_neg hm] have hsub : C' ⊆ schedCache d C₀ σ s := by intro y hy by_contra hyn exact hm ⟨y, Finset.mem_sdiff.mpr ⟨hy, hyn⟩⟩ have hEq : C' = schedCache d C₀ σ s := Finset.eq_of_subset_of_card_le hsub hcard intro hpeq exact (h0hit h2.2) (hEq ▸ h2.2) · rw [if_neg h2] by_cases h3 : d s ∈ C' · rw [if_pos h3] intro hpeq exact hdsC' h3 hpeq.symm · rw [if_neg h3] by_cases hm : (C' \ schedCache d C₀ σ s).Nonempty · rw [dif_pos hm] intro hpeq have hspec := Classical.choose_spec hm have hpnotM : p ∉ C' \ schedCache d C₀ σ s := by rw [Finset.mem_sdiff] intro hmem exact hmem.2 hpD exact hpnotM (hpeq ▸ hspec) · rw [dif_neg hm] have hsub : C' ⊆ schedCache d C₀ σ s := by intro y hy by_contra hyn exact hm ⟨y, Finset.mem_sdiff.mpr ⟨hy, hyn⟩⟩ have hEq : C' = schedCache d C₀ σ s := Finset.eq_of_subset_of_card_le hsub hcard intro hpeq by_cases hr0 : σ.getD s 0 ∈ schedCache d C₀ σ s · exact (h0hit hr0) (hEq ▸ hr0) · have hdsin : d s ∈ C' := by rw [hEq] exact hweak s (by omega) hr0 exact h3 hdsin

When σ[s] ∈ {q,q'} and d hits, while p is in both caches (branch 4 triggers), the exchange's eviction at s is not p.

lemma exchangeDecision_ne_of_branch4 (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) (Variable name `hqq'` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hqq' : q ≠ q') (Variable name `hweak` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hweak : ∀ s, t ≤ s → σ.getD s 0 ∉ schedCache d C₀ σ s → d s ∈ schedCache d C₀ σ s) {s : ℕ} (hst : t < s) (C' : Finset Page) (p : Page) (Variable name `hpE` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hpE : p ∈ C') (hpD : p ∈ schedCache d C₀ σ s) (hpq' : p ≠ q') (hb4 : (σ.getD s 0 = q' ∨ σ.getD s 0 = q) ∧ σ.getD s 0 ∈ schedCache d C₀ σ s) (hcard : (schedCache d C₀ σ s).card ≤ C'.card) (h0hit : σ.getD s 0 ∈ schedCache d C₀ σ s → σ.getD s 0 ∉ C') : exchangeDecision d t q q' σ C₀ C' s ≠ p := by unfold exchangeDecision have hlt : ¬ s < t := by omega have hne : ¬ s = t := by omega rw [if_neg hlt, if_neg hne] by_cases h1 : d s = q' · rw [if_pos h1] intro hpeq exact hpq' hpeq.symm · rw [if_neg h1] rw [if_pos hb4] by_cases hf : ((C' \ schedCache d C₀ σ s).filter (fun x => x ≠ q')).Nonempty · rw [dif_pos hf] intro hpeq have hspec := Classical.choose_spec hf have hpnotM : p ∉ C' \ schedCache d C₀ σ s := by intro hmem exact (Finset.mem_sdiff.mp hmem).2 hpD exact hpnotM (hpeq ▸ (Finset.mem_filter.mp hspec).1) · rw [dif_neg hf] by_cases hm : (C' \ schedCache d C₀ σ s).Nonempty · rw [dif_pos hm] intro hpeq have hspec := Classical.choose_spec hm have hpnotM : p ∉ C' \ schedCache d C₀ σ s := by intro hmem exact (Finset.mem_sdiff.mp hmem).2 hpD exact hpnotM (hpeq ▸ hspec) · rw [dif_neg hm] have hsub : C' ⊆ schedCache d C₀ σ s := by intro y hy by_contra hyn exact hm ⟨y, Finset.mem_sdiff.mpr ⟨hy, hyn⟩⟩ have hEq : C' = schedCache d C₀ σ s := Finset.eq_of_subset_of_card_le hsub hcard intro hpeq exact (h0hit hb4.2) (hEq ▸ hb4.2)

If q is in d's cache then q is also in the exchange cache (at any position after t): q leaves the exchange cache only when d evicts it, and at that point d evicts it too.

lemma exchangeSchedule_q_mem (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) (hq : d t = q) (hqq' : q ≠ q') (hweak : ∀ s, t ≤ s → σ.getD s 0 ∉ schedCache d C₀ σ s → d s ∈ schedCache d C₀ σ s) (hft : σ.getD t 0 ∉ schedCache d C₀ σ t) (Variable name `hq'res` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hq'res : q' ∈ schedCache d C₀ σ t) {j : ℕ} (hj : nextUse σ (t + 1) q = some j) (Variable name `hq'ne` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hq'ne : ∀ k, t + 1 ≤ k → k < t + 1 + j → σ.getD k 0 ≠ q') : ∀ s, t < s → q ∈ schedCache d C₀ σ s → q ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s := by intro s induction s with | zero => omega | succ s ih => intro hs hqin by_cases hs_eq : s = t · -- q ∉ D(t+1): d evicts q at t, and there is no q request before t subst s exfalso have hqne : q ∉ schedCache d C₀ σ (t + 1) := d_cache_ne_q d t q q' σ C₀ hq hweak hft hj (by omega) (by omega) exact hqne hqin · have hts : t < s := by omega -- unfold E(s+1) rw [schedCache_exchangeScheduleCore, exchangeScheduleCore] dsimp rw [show (exchangeScheduleCore d t q q' σ C₀ s).1 = schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s by rw [← schedCache_exchangeScheduleCore]] rw [show (exchangeScheduleCore d t q q' σ C₀ s).2 = exchangeDecision d t q q' σ C₀ (schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s) s by rw [exchangeScheduleCore_second] congr 1 rw [← schedCache_exchangeScheduleCore]] -- unfold D(s+1) in hqin rw [schedCache] at hqin by_cases hr : σ.getD s 0 ∈ schedCache d C₀ σ s · -- d hits: D(s+1) = D(s) rw [if_pos hr] at hqin have hqE : q ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s := ih hts hqin by_cases hrE : σ.getD s 0 ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s · rw [if_pos hrE] exact hqE · -- bad event: σ[s] ∈ D(s) − E(s) ⊆ {q, q'} rw [if_neg hrE] have hqqq' : σ.getD s 0 = q' ∨ σ.getD s 0 = q := by by_contra hnot have hinv := exchangeSchedule_invariant d t q q' σ C₀ hq hweak s (by omega) exact hrE (hinv (σ.getD s 0) (by intro hmem apply hnot rcases Finset.mem_insert.mp hmem with hqeq | hq'eq · exact Or.inr hqeq · exact Or.inl (Finset.mem_singleton.mp hq'eq)) hr) rcases hqqq' with hq'eq | hqeq · -- σ[s] = q': branch 4 triggers, dec ≠ q have hb4 : (σ.getD s 0 = q' ∨ σ.getD s 0 = q) ∧ σ.getD s 0 ∈ schedCache d C₀ σ s := ⟨Or.inl hq'eq, hr⟩ have hcard : (schedCache d C₀ σ s).card ≤ (schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s).card := by rw [schedCache_exchangeScheduleCore] exact exchangeScheduleCore_card d t q q' σ C₀ hweak (by omega) have hdec : exchangeDecision d t q q' σ C₀ (schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s) s ≠ q := by apply exchangeDecision_ne_of_branch4 d t q q' σ C₀ hqq' hweak hts · exact hqE · exact hqin · exact hqq' · exact hb4 · exact hcard · exact fun _ => hrE exact Finset.mem_insert_of_mem (b := σ.getD s 0) (Finset.mem_erase.mpr ⟨hdec.symm, hqE⟩) · -- σ[s] = q: contradicts q ∈ E(s) exfalso exact hrE (hqeq ▸ hqE) · -- d faults rw [if_neg hr] at hqin rcases Finset.mem_insert.mp hqin with hqeq | hqin' · -- q = σ[s]: the exchange loads q by_cases hrE : σ.getD s 0 ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s · rw [if_pos hrE] exact hqeq.symm ▸ hrE · rw [if_neg hrE] exact hqeq.symm ▸ Finset.mem_insert_self (σ.getD s 0) _ · -- q ∈ D(s) and q ≠ d s have hqD : q ∈ schedCache d C₀ σ s := (Finset.mem_erase.mp hqin').2 have hqds : q ≠ d s := (Finset.mem_erase.mp hqin').1 have hqE : q ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s := ih hts hqD have hcard : (schedCache d C₀ σ s).card ≤ (schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s).card := by rw [schedCache_exchangeScheduleCore] exact exchangeScheduleCore_card d t q q' σ C₀ hweak (by omega) have hdec : exchangeDecision d t q q' σ C₀ (schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s) s ≠ q := by apply exchangeDecision_ne d t q q' σ C₀ hweak hts · exact hqE · exact hqD · intro hds exact hqq' · intro hdsin exact hqds · exact hcard · intro hmem exact False.elim (hr hmem) by_cases hrE : σ.getD s 0 ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s · rw [if_pos hrE] exact hqE · rw [if_neg hrE] exact Finset.mem_insert_of_mem (b := σ.getD s 0) (Finset.mem_erase.mpr ⟨hdec.symm, hqE⟩)

Up to and including the first q' request, the exchange cache does not contain q' (q' is evicted at t, and there is no q' request within (t, J')).

lemma exchangeSchedule_q'_absent (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) (Variable name `hweak` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hweak : ∀ s, t ≤ s → σ.getD s 0 ∉ schedCache d C₀ σ s → d s ∈ schedCache d C₀ σ s) (hft : σ.getD t 0 ∉ schedCache d C₀ σ t) (hq'res : q' ∈ schedCache d C₀ σ t) {j' : ℕ} (hj' : nextUse σ (t + 1) q' = some j') {s : ℕ} (hs1 : t < s) (hs2 : s ≤ t + 1 + j') : q' ∉ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s := by induction s with | zero => omega | succ s ih => by_cases hs_eq : s = t · subst s rw [schedCache_exchangeScheduleCore, exchangeScheduleCore] dsimp rw [show (exchangeScheduleCore d t q q' σ C₀ t).1 = schedCache d C₀ σ t by rw [← schedCache_exchangeScheduleCore] exact schedCache_exchangeSchedule_eq_d d t q q' σ C₀ le_rfl] rw [show (exchangeScheduleCore d t q q' σ C₀ t).2 = q' by exact exchangeSchedule_at_t d t q q' σ C₀] rw [if_neg hft] rw [Finset.mem_insert] intro hmem rcases hmem with hq'eq | hq'mem · exact hft (hq'eq ▸ hq'res) · exact (Finset.mem_erase.mp hq'mem).1 rfl · have hts : t < s := by omega have hsJ' : s < t + 1 + j' := by omega have hsig_ne_q' : σ.getD s 0 ≠ q' := getD_ne_nextUse hj' (by omega) hsJ' rw [schedCache_exchangeScheduleCore, exchangeScheduleCore] dsimp rw [show (exchangeScheduleCore d t q q' σ C₀ s).1 = schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s by rw [← schedCache_exchangeScheduleCore]] rw [show (exchangeScheduleCore d t q q' σ C₀ s).2 = exchangeDecision d t q q' σ C₀ (schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s) s by rw [exchangeScheduleCore_second] congr 1 rw [← schedCache_exchangeScheduleCore]] by_cases hrE : σ.getD s 0 ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s · rw [if_pos hrE] exact ih hts (by omega) · rw [if_neg hrE] intro hmem rcases Finset.mem_insert.mp hmem with hq'eq | hq'in · exact hsig_ne_q' hq'eq.symm · exact ih hts (by omega) (Finset.mem_erase.mp hq'in).2

After the first q' request, if q' is in d's cache then q' is also in the exchange cache (q' is reloaded by both schedules at J', and afterwards only evicted together with d).

lemma exchangeSchedule_q'_mem (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) (hq : d t = q) (hqq' : q ≠ q') (hweak : ∀ s, t ≤ s → σ.getD s 0 ∉ schedCache d C₀ σ s → d s ∈ schedCache d C₀ σ s) (hft : σ.getD t 0 ∉ schedCache d C₀ σ t) (hq'res : q' ∈ schedCache d C₀ σ t) {j : ℕ} (hj : nextUse σ (t + 1) q = some j) (hq'ne : ∀ k, t + 1 ≤ k → k < t + 1 + j → σ.getD k 0 ≠ q') {j' : ℕ} (hj' : nextUse σ (t + 1) q' = some j') : ∀ s, t + 1 + j' < s → q' ∈ schedCache d C₀ σ s → q' ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s := by intro s induction s with | zero => omega | succ s ih => intro hs hqin by_cases hs_eq : s = t + 1 + j' · -- base: at position J' the exchange loads q' subst s rw [schedCache_exchangeScheduleCore, exchangeScheduleCore] dsimp rw [show (exchangeScheduleCore d t q q' σ C₀ (t + 1 + j')).1 = schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ (t + 1 + j') by rw [← schedCache_exchangeScheduleCore]] have hsig : σ.getD (t + 1 + j') 0 = q' := getD_eq_nextUse hj' have hJ'ne : σ.getD (t + 1 + j') 0 ∉ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ (t + 1 + j') := by rw [hsig] apply exchangeSchedule_q'_absent d t q q' σ C₀ hweak hft hq'res hj' · omega · rfl rw [hsig] rw [hsig] at hJ'ne rw [if_neg hJ'ne] exact Finset.mem_insert_self q' _ · have hsJ' : t + 1 + j' < s := by omega rw [schedCache_exchangeScheduleCore, exchangeScheduleCore] dsimp rw [show (exchangeScheduleCore d t q q' σ C₀ s).1 = schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s by rw [← schedCache_exchangeScheduleCore]] rw [show (exchangeScheduleCore d t q q' σ C₀ s).2 = exchangeDecision d t q q' σ C₀ (schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s) s by rw [exchangeScheduleCore_second] congr 1 rw [← schedCache_exchangeScheduleCore]] rw [schedCache] at hqin by_cases hr : σ.getD s 0 ∈ schedCache d C₀ σ s · -- d hits rw [if_pos hr] at hqin have hq'E : q' ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s := ih hsJ' hqin by_cases hrE : σ.getD s 0 ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s · rw [if_pos hrE] exact hq'E · -- bad event: σ[s] ∈ D(s) − E(s) ⊆ {q, q'}, both subcases excluded by the membership lemmas rw [if_neg hrE] have hqqq' : σ.getD s 0 = q' ∨ σ.getD s 0 = q := by by_contra hnot have hinv := exchangeSchedule_invariant d t q q' σ C₀ hq hweak s (by omega) exact hrE (hinv (σ.getD s 0) (by intro hmem apply hnot rcases Finset.mem_insert.mp hmem with hqeq | hq'eq · exact Or.inr hqeq · exact Or.inl (Finset.mem_singleton.mp hq'eq)) hr) rcases hqqq' with hq'eq | hqeq · exfalso exact hrE (hq'eq ▸ hq'E) · exfalso have hqE : q ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s := exchangeSchedule_q_mem d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'ne s (by omega) (hqeq ▸ hr) exact hrE (hqeq ▸ hqE) · -- d faults rw [if_neg hr] at hqin rcases Finset.mem_insert.mp hqin with hq'eq | hq'in · -- q' = σ[s]: the exchange loads q' by_cases hrE : σ.getD s 0 ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s · rw [if_pos hrE] exact hq'eq.symm ▸ hrE · rw [if_neg hrE] exact hq'eq.symm ▸ Finset.mem_insert_self (σ.getD s 0) _ · -- q' ∈ D(s) and q' ≠ d s have hts : t < s := by omega have hq'D : q' ∈ schedCache d C₀ σ s := (Finset.mem_erase.mp hq'in).2 have hq'ds : q' ≠ d s := (Finset.mem_erase.mp hq'in).1 have hq'E : q' ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s := ih hsJ' hq'D have hcard : (schedCache d C₀ σ s).card ≤ (schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s).card := by rw [schedCache_exchangeScheduleCore] exact exchangeScheduleCore_card d t q q' σ C₀ hweak (by omega) have hdec : exchangeDecision d t q q' σ C₀ (schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s) s ≠ q' := by apply exchangeDecision_ne d t q q' σ C₀ hweak hts · exact hq'E · exact hq'D · intro hds exact False.elim (hq'ds hds.symm) · intro hdsin exact hq'ds · exact hcard · intro hmem exact False.elim (hr hmem) by_cases hrE : σ.getD s 0 ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s · rw [if_pos hrE] exact hq'E · rw [if_neg hrE] exact Finset.mem_insert_of_mem (b := σ.getD s 0) (Finset.mem_erase.mpr ⟨hdec.symm, hq'E⟩)

Good event: at the first request of q, the exchange hits while d faults.

lemma exchangeSchedule_good (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) (hq : d t = q) (hqq' : q ≠ q') (hweak : ∀ s, t ≤ s → σ.getD s 0 ∉ schedCache d C₀ σ s → d s ∈ schedCache d C₀ σ s) (hft : σ.getD t 0 ∉ schedCache d C₀ σ t) (hq'res : q' ∈ schedCache d C₀ σ t) {j : ℕ} (hj : nextUse σ (t + 1) q = some j) (hq'ne : ∀ k, t + 1 ≤ k → k < t + 1 + j → σ.getD k 0 ≠ q') : σ.getD (t + 1 + j) 0 ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ (t + 1 + j) ∧ σ.getD (t + 1 + j) 0 ∉ schedCache d C₀ σ (t + 1 + j) := by have hsig : σ.getD (t + 1 + j) 0 = q := getD_eq_nextUse hj constructor · rw [hsig] rw [exchangeSchedule_window d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'ne (s := t + 1 + j) (by omega) (by rfl)] rw [Finset.mem_insert] left rfl · rw [hsig] exact d_cache_ne_q d t q q' σ C₀ hq hweak hft hj (by omega) (by omega)

The bad event (the exchange faults while d hits) can only occur at the first q' request.

lemma exchangeSchedule_bad (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) (hq : d t = q) (hqq' : q ≠ q') (hweak : ∀ s, t ≤ s → σ.getD s 0 ∉ schedCache d C₀ σ s → d s ∈ schedCache d C₀ σ s) (hft : σ.getD t 0 ∉ schedCache d C₀ σ t) (hq'res : q' ∈ schedCache d C₀ σ t) {j : ℕ} (hj : nextUse σ (t + 1) q = some j) (hq'ne : ∀ k, t + 1 ≤ k → k < t + 1 + j → σ.getD k 0 ≠ q') {j' : ℕ} (hj' : nextUse σ (t + 1) q' = some j') {s : ℕ} (hst : t < s) : σ.getD s 0 ∈ schedCache d C₀ σ s → σ.getD s 0 ∉ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s → s = t + 1 + j' := by intro hmem hnot have hqqq' : σ.getD s 0 = q' ∨ σ.getD s 0 = q := by by_contra hnot' have hinv := exchangeSchedule_invariant d t q q' σ C₀ hq hweak s (by omega) exact hnot (hinv (σ.getD s 0) (by intro hmem2 apply hnot' rcases Finset.mem_insert.mp hmem2 with hqeq | hq'eq · exact Or.inr hqeq · exact Or.inl (Finset.mem_singleton.mp hq'eq)) hmem) rcases hqqq' with hq'eq | hqeq · -- σ[s] = q': exclude s < J' and s > J' by_cases hlt : s < t + 1 + j' · exfalso exact (getD_ne_nextUse hj' (by omega) hlt) hq'eq · by_cases hgt : t + 1 + j' < s · exfalso have hq'E : q' ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s := by have hq'in' : q' ∈ schedCache d C₀ σ s := hq'eq ▸ hmem exact exchangeSchedule_q'_mem d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'ne hj' s hgt hq'in' exact hnot (hq'eq ▸ hq'E) · omega · -- σ[s] = q: contradicts L-q exfalso have hqE : q ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s := by have hqin' : q ∈ schedCache d C₀ σ s := hqeq ▸ hmem exact exchangeSchedule_q_mem d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'ne s hst hqin' exact hnot (hqeq ▸ hqE)

The exchange schedule has no more misses than d: the good event (first q request) compensates for the unique bad event (first q' request).

lemma exchangeSchedule_misses_le (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) (hq : d t = q) (hqq' : q ≠ q') (hweak : ∀ s, t ≤ s → σ.getD s 0 ∉ schedCache d C₀ σ s → d s ∈ schedCache d C₀ σ s) (hft : σ.getD t 0 ∉ schedCache d C₀ σ t) (hq'res : q' ∈ schedCache d C₀ σ t) (hfifo : nextUse σ (t + 1) q' = none ∨ ∃ j j', nextUse σ (t + 1) q = some j ∧ nextUse σ (t + 1) q' = some j' ∧ j < j') : schedMisses (exchangeSchedule d t q q' σ C₀) C₀ σ ≤ schedMisses d C₀ σ := by let e : ℕ → Page := exchangeSchedule d t q q' σ C₀ let eF : ℕ → ℕ := schedFaultAt e C₀ σ let dF : ℕ → ℕ := schedFaultAt d C₀ σ rcases hfifo with hnone | ⟨j, j', hj, hj', hjlt⟩ · -- CASE A: `q'` is never requested again have hq'ne_s : ∀ s, t + 1 ≤ s → s < σ.length → σ.getD s 0 ≠ q' := by intro s hs hlen have hnone' := nextUse_eq_none_iff.mp hnone apply hnone' (σ.getD s 0) have hget : (σ.drop (t + 1)).getD (s - (t + 1)) 0 = σ.getD s 0 := by rw [getD_drop] rw [Nat.add_sub_of_le hs] rw [← hget] have hlt' : s - (t + 1) < (σ.drop (t + 1)).length := by rw [List.length_drop] omega rw [List.getD_eq_getElem _ 0 hlt'] exact List.getElem_mem hlt' by_cases hqreq : ∃ j, nextUse σ (t + 1) q = some j · -- q will be requested: the good event at J compensates for everything rcases hqreq with ⟨j, hj⟩ have hJlen : t + 1 + j < σ.length := by have hjlt' : j < (σ.drop (t + 1)).length := (nextUse_eq_some_iff.mp hj).1 rw [List.length_drop] at hjlt' omega have hJle : t + 1 + j + 1 ≤ σ.length := by omega have hq'neA : ∀ k, t + 1 ≤ k → k < t + 1 + j → σ.getD k 0 ≠ q' := by intro k hk1 hk2 exact hq'ne_s k hk1 (by omega) -- pointwise: fault equal for s ≤ t have hP0 : ∀ s, s ≤ t → eF s = dF s := by intro s hs unfold eF dF e schedFaultAt rw [schedCache_exchangeSchedule_eq_d d t q q' σ C₀ hs] -- pointwise: fault equal for t < s < J (window) have hP1 : ∀ s, t < s → s < t + 1 + j → eF s = dF s := by intro s hst hsJ unfold eF dF e schedFaultAt rw [exchangeSchedule_window d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'neA (s := s) hst (by omega)] have hne1 : σ.getD s 0 ≠ q := getD_ne_nextUse hj (by omega) hsJ have hne2 : σ.getD s 0 ≠ q' := hq'neA s (by omega) hsJ by_cases hr : σ.getD s 0 ∈ schedCache d C₀ σ s · rw [if_pos hr] have hrE' : σ.getD s 0 ∈ insert q ((schedCache d C₀ σ s).erase q') := by rw [Finset.mem_insert] right rw [Finset.mem_erase] constructor · exact hne2 · exact hr rw [if_pos hrE'] · rw [if_neg hr] have hrE' : σ.getD s 0 ∉ insert q ((schedCache d C₀ σ s).erase q') := by intro hm rcases Finset.mem_insert.mp hm with hqeq | hmem · exact hne1 hqeq · exact hr (Finset.mem_erase.mp hmem).2 rw [if_neg hrE'] -- pointwise: eF ≤ dF for J < s (no bad event) have hP3A : ∀ s, t < s → s < σ.length → eF s ≤ dF s := by intro s hst hlen unfold eF dF e schedFaultAt by_cases hr : σ.getD s 0 ∈ schedCache d C₀ σ s · by_cases hrE : σ.getD s 0 ∈ schedCache e C₀ σ s · rw [if_pos hrE, if_pos hr] · rw [if_neg hrE, if_pos hr] exfalso have hqqq' : σ.getD s 0 = q' ∨ σ.getD s 0 = q := by by_contra hnot have hinv := exchangeSchedule_invariant d t q q' σ C₀ hq hweak s (by omega) exact hrE (hinv (σ.getD s 0) (by intro hmem2 apply hnot rcases Finset.mem_insert.mp hmem2 with hqeq | hq'eq · exact Or.inr hqeq · exact Or.inl (Finset.mem_singleton.mp hq'eq)) hr) rcases hqqq' with hq'eq | hqeq · exact hq'ne_s s (by omega) hlen hq'eq · have hqE : q ∈ schedCache e C₀ σ s := by exact exchangeSchedule_q_mem d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'neA s hst (hqeq ▸ hr) exact hrE (hqeq ▸ hqE) · rw [if_neg hr] by_cases hrE : σ.getD s 0 ∈ schedCache e C₀ σ s · rw [if_pos hrE] omega · rw [if_neg hrE] -- good event at J have hgood := exchangeSchedule_good d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'neA -- split the sum have hdisj : Disjoint (Finset.range (t + 1 + j + 1)) (Finset.Ico (t + 1 + j + 1) σ.length) := by rw [Finset.disjoint_left] intro s hs1 hs2 have h1 : s < t + 1 + j + 1 := Finset.mem_range.mp hs1 have h2 : t + 1 + j + 1 ≤ s := (Finset.mem_Ico.mp hs2).1 omega have hunion : Finset.range (t + 1 + j + 1) ∪ Finset.Ico (t + 1 + j + 1) σ.length = Finset.range σ.length := by ext s simp [Finset.mem_Ico] constructor · intro h rcases h with hs | ⟨h1, h2⟩ · omega · exact h2 · intro hs by_cases hs' : s < t + 1 + j + 1 · exact Or.inl (Nat.lt_succ_iff.mp hs') · right constructor · omega · exact hs have hsum_e : (∑ s ∈ Finset.range σ.length, eF s) = (∑ s ∈ Finset.range (t + 1 + j + 1), eF s) + ∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, eF s := by rw [← hunion, Finset.sum_union hdisj] have hsum_d : (∑ s ∈ Finset.range σ.length, dF s) = (∑ s ∈ Finset.range (t + 1 + j + 1), dF s) + ∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, dF s := by rw [← hunion, Finset.sum_union hdisj] -- first part: Σ_{<J+1} eF + 1 ≤ Σ_{<J+1} dF have hpart1 : (∑ s ∈ Finset.range (t + 1 + j + 1), eF s) + 1 ≤ ∑ s ∈ Finset.range (t + 1 + j + 1), dF s := by rw [Finset.sum_range_succ] rw [Finset.sum_range_succ] have heJ : eF (t + 1 + j) = 0 := by unfold eF schedFaultAt rw [if_pos hgood.1] have hdJ : dF (t + 1 + j) = 1 := by unfold dF schedFaultAt rw [if_neg hgood.2] rw [heJ, hdJ] have hle : (∑ s ∈ Finset.range (t + 1 + j), eF s) ≤ ∑ s ∈ Finset.range (t + 1 + j), dF s := by exact Finset.sum_le_sum (fun s hs => by by_cases hst' : s ≤ t · exact le_of_eq (hP0 s hst') · have hts' : t < s := by omega exact le_of_eq (hP1 s hts' (Finset.mem_range.mp hs))) have hle' : (∑ s ∈ Finset.range (t + 1 + j), eF s) + 1 ≤ (∑ s ∈ Finset.range (t + 1 + j), dF s) + 1 := Nat.add_le_add_right hle 1 simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using hle' -- second part: Σ_{[J+1,len)} eF ≤ Σ dF have hpart2 : (∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, eF s) ≤ ∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, dF s := by apply Finset.sum_le_sum intro s hs have hst' : t < s := by have h1 : t + 1 + j + 1 ≤ s := (Finset.mem_Ico.mp hs).1 omega exact hP3A s hst' (Finset.mem_Ico.mp hs).2 -- assemble unfold schedMisses change (∑ s ∈ Finset.range σ.length, eF s) ≤ ∑ s ∈ Finset.range σ.length, dF s rw [hsum_e, hsum_d] omega · -- q is never requested either: no q request, no q' request, pointwise comparison suffices have hqne_s : ∀ s, t + 1 ≤ s → s < σ.length → σ.getD s 0 ≠ q := by intro s hs hlen have hnoneq : nextUse σ (t + 1) q = none := by cases hopt : nextUse σ (t + 1) q with | none => rfl | some j => exact False.elim (hqreq ⟨j, hopt⟩) have hnoneq' := nextUse_eq_none_iff.mp hnoneq apply hnoneq' (σ.getD s 0) have hget : (σ.drop (t + 1)).getD (s - (t + 1)) 0 = σ.getD s 0 := by rw [getD_drop] rw [Nat.add_sub_of_le hs] rw [← hget] have hlt' : s - (t + 1) < (σ.drop (t + 1)).length := by rw [List.length_drop] omega rw [List.getD_eq_getElem _ 0 hlt'] exact List.getElem_mem hlt' -- pointwise eF ≤ dF have hP : ∀ s, s < σ.length → eF s ≤ dF s := by intro s hlen by_cases hst : s ≤ t · -- caches equal unfold eF dF e schedFaultAt rw [schedCache_exchangeSchedule_eq_d d t q q' σ C₀ hst] · have hts' : t < s := by omega unfold eF dF e schedFaultAt by_cases hr : σ.getD s 0 ∈ schedCache d C₀ σ s · by_cases hrE : σ.getD s 0 ∈ schedCache e C₀ σ s · rw [if_pos hrE, if_pos hr] · rw [if_neg hrE, if_pos hr] exfalso have hqqq' : σ.getD s 0 = q' ∨ σ.getD s 0 = q := by by_contra hnot have hinv := exchangeSchedule_invariant d t q q' σ C₀ hq hweak s (by omega) exact hrE (hinv (σ.getD s 0) (by intro hmem2 apply hnot rcases Finset.mem_insert.mp hmem2 with hqeq | hq'eq · exact Or.inr hqeq · exact Or.inl (Finset.mem_singleton.mp hq'eq)) hr) rcases hqqq' with hq'eq | hqeq · exact hq'ne_s s (by omega) hlen hq'eq · exact hqne_s s (by omega) hlen hqeq · rw [if_neg hr] by_cases hrE : σ.getD s 0 ∈ schedCache e C₀ σ s · rw [if_pos hrE] omega · rw [if_neg hrE] unfold schedMisses change (∑ s ∈ Finset.range σ.length, eF s) ≤ ∑ s ∈ Finset.range σ.length, dF s exact Finset.sum_le_sum (fun s hs => hP s (Finset.mem_range.mp hs)) · -- CASE B: the first request of `q` comes before the first request of `q'` have hJlen : t + 1 + j < σ.length := by have hjlt' : j < (σ.drop (t + 1)).length := (nextUse_eq_some_iff.mp hj).1 rw [List.length_drop] at hjlt' omega have hJ'len : t + 1 + j' < σ.length := by have hj'lt' : j' < (σ.drop (t + 1)).length := (nextUse_eq_some_iff.mp hj').1 rw [List.length_drop] at hj'lt' omega have hJle : t + 1 + j + 1 ≤ σ.length := by omega have hJ'le : t + 1 + j' + 1 ≤ σ.length := by omega have hJJ' : t + 1 + j + 1 ≤ t + 1 + j' := by omega have hq'neB : ∀ k, t + 1 ≤ k → k < t + 1 + j → σ.getD k 0 ≠ q' := by intro k hk1 hk2 exact getD_ne_nextUse hj' hk1 (by omega) -- pointwise: fault equal for s ≤ t have hP0 : ∀ s, s ≤ t → eF s = dF s := by intro s hs unfold eF dF e schedFaultAt rw [schedCache_exchangeSchedule_eq_d d t q q' σ C₀ hs] -- pointwise: fault equal for t < s < J (window) have hP1 : ∀ s, t < s → s < t + 1 + j → eF s = dF s := by intro s hst hsJ unfold eF dF e schedFaultAt rw [exchangeSchedule_window d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'neB (s := s) hst (by omega)] have hne1 : σ.getD s 0 ≠ q := getD_ne_nextUse hj (by omega) hsJ have hne2 : σ.getD s 0 ≠ q' := hq'neB s (by omega) hsJ by_cases hr : σ.getD s 0 ∈ schedCache d C₀ σ s · rw [if_pos hr] have hrE' : σ.getD s 0 ∈ insert q ((schedCache d C₀ σ s).erase q') := by rw [Finset.mem_insert] right rw [Finset.mem_erase] constructor · exact hne2 · exact hr rw [if_pos hrE'] · rw [if_neg hr] have hrE' : σ.getD s 0 ∉ insert q ((schedCache d C₀ σ s).erase q') := by intro hm rcases Finset.mem_insert.mp hm with hqeq | hmem · exact hne1 hqeq · exact hr (Finset.mem_erase.mp hmem).2 rw [if_neg hrE'] -- pointwise: eF ≤ dF for s ≠ J' (the bad event only at J') have hP3 : ∀ s, t < s → s < σ.length → s ≠ t + 1 + j' → eF s ≤ dF s := by intro s hst hlen hsne unfold eF dF e schedFaultAt by_cases hr : σ.getD s 0 ∈ schedCache d C₀ σ s · by_cases hrE : σ.getD s 0 ∈ schedCache e C₀ σ s · rw [if_pos hrE, if_pos hr] · rw [if_neg hrE, if_pos hr] exfalso exact hsne (exchangeSchedule_bad d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'neB hj' hst hr hrE) · rw [if_neg hr] by_cases hrE : σ.getD s 0 ∈ schedCache e C₀ σ s · rw [if_pos hrE] omega · rw [if_neg hrE] -- good event at J have hgood := exchangeSchedule_good d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'neB -- split the sum have hdisj : Disjoint (Finset.range (t + 1 + j + 1)) (Finset.Ico (t + 1 + j + 1) σ.length) := by rw [Finset.disjoint_left] intro s hs1 hs2 have h1 : s < t + 1 + j + 1 := Finset.mem_range.mp hs1 have h2 : t + 1 + j + 1 ≤ s := (Finset.mem_Ico.mp hs2).1 omega have hunion : Finset.range (t + 1 + j + 1) ∪ Finset.Ico (t + 1 + j + 1) σ.length = Finset.range σ.length := by ext s simp [Finset.mem_Ico] constructor · intro h rcases h with hs | ⟨h1, h2⟩ · omega · exact h2 · intro hs by_cases hs' : s < t + 1 + j + 1 · exact Or.inl (Nat.lt_succ_iff.mp hs') · right constructor · omega · exact hs have hsum_e : (∑ s ∈ Finset.range σ.length, eF s) = (∑ s ∈ Finset.range (t + 1 + j + 1), eF s) + ∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, eF s := by rw [← hunion, Finset.sum_union hdisj] have hsum_d : (∑ s ∈ Finset.range σ.length, dF s) = (∑ s ∈ Finset.range (t + 1 + j + 1), dF s) + ∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, dF s := by rw [← hunion, Finset.sum_union hdisj] -- first part: Σ_{<J+1} eF + 1 ≤ Σ_{<J+1} dF have hpart1 : (∑ s ∈ Finset.range (t + 1 + j + 1), eF s) + 1 ≤ ∑ s ∈ Finset.range (t + 1 + j + 1), dF s := by rw [Finset.sum_range_succ] rw [Finset.sum_range_succ] have heJ : eF (t + 1 + j) = 0 := by unfold eF schedFaultAt rw [if_pos hgood.1] have hdJ : dF (t + 1 + j) = 1 := by unfold dF schedFaultAt rw [if_neg hgood.2] rw [heJ, hdJ] have hle : (∑ s ∈ Finset.range (t + 1 + j), eF s) ≤ ∑ s ∈ Finset.range (t + 1 + j), dF s := by exact Finset.sum_le_sum (fun s hs => by by_cases hst' : s ≤ t · exact le_of_eq (hP0 s hst') · have hts' : t < s := by omega exact le_of_eq (hP1 s hts' (Finset.mem_range.mp hs))) have hle' : (∑ s ∈ Finset.range (t + 1 + j), eF s) + 1 ≤ (∑ s ∈ Finset.range (t + 1 + j), dF s) + 1 := Nat.add_le_add_right hle 1 simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using hle' -- second part: Σ_{[J+1,len)} eF ≤ Σ dF + 1 have hpart2 : (∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, eF s) ≤ (∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, dF s) + 1 := by have hper : ∀ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, eF s ≤ dF s + (if s = t + 1 + j' then 1 else 0) := by intro s hs have hst' : t < s := by have h1 : t + 1 + j + 1 ≤ s := (Finset.mem_Ico.mp hs).1 exact lt_of_lt_of_le (by omega : t < t + 1 + j + 1) h1 by_cases hsne : s = t + 1 + j' · subst s unfold eF dF schedFaultAt dsimp [e] by_cases hr : σ.getD (t + 1 + j') 0 ∈ schedCache d C₀ σ (t + 1 + j') · by_cases hrE : σ.getD (t + 1 + j') 0 ∈ schedCache e C₀ σ (t + 1 + j') · rw [if_pos hrE, if_pos hr] norm_num · rw [if_neg hrE, if_pos hr] norm_num · by_cases hrE : σ.getD (t + 1 + j') 0 ∈ schedCache e C₀ σ (t + 1 + j') · rw [if_pos hrE, if_neg hr] norm_num · rw [if_neg hrE, if_neg hr] norm_num · have hle := hP3 s hst' (Finset.mem_Ico.mp hs).2 hsne have hif : (if s = t + 1 + j' then 1 else 0) = 0 := if_neg hsne rw [hif] exact hle have hsum1 : (∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, eF s) ≤ ∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, (dF s + (if s = t + 1 + j' then 1 else 0)) := by exact Finset.sum_le_sum hper have hsum2 : (∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, (dF s + (if s = t + 1 + j' then 1 else 0))) = (∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, dF s) + ∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, (if s = t + 1 + j' then 1 else 0) := by rw [Finset.sum_add_distrib] have hsum3 : (∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, (if s = t + 1 + j' then 1 else 0)) ≤ 1 := by rw [Finset.sum_ite_eq'] by_cases hJ'in : t + 1 + j' ∈ Finset.Ico (t + 1 + j + 1) σ.length · simp [hJ'in] · simp [hJ'in] rw [hsum2] at hsum1 exact le_trans hsum1 (Nat.add_le_add_left hsum3 _) -- assemble unfold schedMisses change (∑ s ∈ Finset.range σ.length, eF s) ≤ ∑ s ∈ Finset.range σ.length, dF s rw [hsum_e, hsum_d] have hboth : (∑ s ∈ Finset.range σ.length, eF s) + 1 ≤ (∑ s ∈ Finset.range σ.length, dF s) + 1 := by rw [hsum_e, hsum_d] have h := add_le_add hpart1 hpart2 simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using h omega

The farthest-in-future (Belady) eviction schedule for σ from C₀.

noncomputable def fifoSchedule (σ : List Page) (C₀ : Finset Page) : ℕ → Page := policySchedule (fifoPolicy σ) C₀ σ

d agrees with the farthest-in-future schedule on caches through n.

def agreeWithFIF (d : ℕ → Page) (C₀ : Finset Page) (σ : List Page) (n : ℕ) : Prop := ∀ s ≤ n, schedCache d C₀ σ s = schedCache (fifoSchedule σ C₀) C₀ σ s

The run of the FIF schedule is the run of the FIF policy.

lemma schedCache_fifoSchedule (σ : List Page) (C₀ : Finset Page) (s : ℕ) : schedCache (fifoSchedule σ C₀) C₀ σ s = cacheSeq (fifoPolicy σ) C₀ σ s := by unfold fifoSchedule exact schedCache_policySchedule (fifoPolicy σ) C₀ σ s

When d agrees with the FIF schedule through t, the FIF eviction at t is the farthest-in-future page of d's cache.

lemma fifo_evict_eq_farthest (d : ℕ → Page) (σ : List Page) (C₀ : Finset Page) {t : ℕ} (hagree : agreeWithFIF d C₀ σ t) : (fifoSchedule σ C₀) t = farthestInFuture (schedCache d C₀ σ t) σ t := by change farthestInFuture (cacheSeq (fifoPolicy σ) C₀ σ t) σ t = farthestInFuture (schedCache d C₀ σ t) σ t rw [← schedCache_fifoSchedule σ C₀ t] rw [← hagree t le_rfl]

The caches in a run of a reduced schedule from a nonempty cache are nonempty.

lemma schedCache_nonempty_of_reduced (d : ℕ → Page) (σ : List Page) (C₀ : Finset Page) (hC₀ : C₀.Nonempty) (s : ℕ) : (schedCache d C₀ σ s).Nonempty := by cases s with | zero => exact hC₀ | succ s => rw [schedCache] by_cases hr : σ.getD s 0 ∈ schedCache d C₀ σ s · rw [if_pos hr] exact ⟨σ.getD s 0, hr⟩ · rw [if_neg hr] exact ⟨σ.getD s 0, Finset.mem_insert_self _ _⟩

At a first disagreement t of a reduced schedule d with the FIF schedule, both fault at t, the evictions differ, and the FIF eviction is resident in d's cache.

lemma first_disagree (d : ℕ → Page) (σ : List Page) (C₀ : Finset Page) (hC₀ : C₀.Nonempty) {t : ℕ} (Variable name `ht` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`ht : t < σ.length) (hagree : agreeWithFIF d C₀ σ t) (hdis : schedCache d C₀ σ (t + 1) ≠ schedCache (fifoSchedule σ C₀) C₀ σ (t + 1)) : σ.getD t 0 ∉ schedCache d C₀ σ t ∧ d t ≠ (fifoSchedule σ C₀) t ∧ (fifoSchedule σ C₀) t ∈ schedCache d C₀ σ t := by have hft : σ.getD t 0 ∉ schedCache d C₀ σ t := by intro hft have hFt : σ.getD t 0 ∈ schedCache (fifoSchedule σ C₀) C₀ σ t := by rw [← hagree t le_rfl] exact hft have hD : schedCache d C₀ σ (t + 1) = schedCache d C₀ σ t := by rw [schedCache] rw [if_pos hft] have hF : schedCache (fifoSchedule σ C₀) C₀ σ (t + 1) = schedCache (fifoSchedule σ C₀) C₀ σ t := by rw [schedCache] rw [if_pos hFt] exact hdis ((hD.trans (hagree t le_rfl)).trans hF.symm) constructor · exact hft · constructor · intro hq have hFt : σ.getD t 0 ∉ schedCache (fifoSchedule σ C₀) C₀ σ t := by rw [← hagree t le_rfl] exact hft have hD : schedCache d C₀ σ (t + 1) = insert (σ.getD t 0) ((schedCache d C₀ σ t).erase (d t)) := by rw [schedCache] rw [if_neg hft] have hF : schedCache (fifoSchedule σ C₀) C₀ σ (t + 1) = insert (σ.getD t 0) ((schedCache (fifoSchedule σ C₀) C₀ σ t).erase ((fifoSchedule σ C₀) t)) := by rw [schedCache] rw [if_neg hFt] have hEq : schedCache d C₀ σ t = schedCache (fifoSchedule σ C₀) C₀ σ t := hagree t le_rfl rw [hD, hF] at hdis rw [hEq] at hdis rw [hq] at hdis exact hdis rfl · rw [fifo_evict_eq_farthest d σ C₀ hagree] apply mem_farthestInFuture exact schedCache_nonempty_of_reduced d σ C₀ hC₀ t

Exchanging the first disagreement of a reduced schedule never increases misses and extends agreement with the FIF schedule by one position.

lemma exchange_step (d : ℕ → Page) (σ : List Page) (C₀ : Finset Page) (hdreduced : ∀ s, σ.getD s 0 ∉ schedCache d C₀ σ s → d s ∈ schedCache d C₀ σ s) (hC₀ : C₀.Nonempty) {t : ℕ} (ht : t < σ.length) (hagree : agreeWithFIF d C₀ σ t) (hdis : schedCache d C₀ σ (t + 1) ≠ schedCache (fifoSchedule σ C₀) C₀ σ (t + 1)) : schedMisses (exchangeSchedule d t (d t) (fifoSchedule σ C₀ t) σ C₀) C₀ σ ≤ schedMisses d C₀ σ ∧ agreeWithFIF (exchangeSchedule d t (d t) (fifoSchedule σ C₀ t) σ C₀) C₀ σ (t + 1) := by let q : Page := d t let q' : Page := fifoSchedule σ C₀ t have hfd := first_disagree d σ C₀ hC₀ ht hagree hdis have hqq' : q ≠ q' := hfd.2.1 have hft : σ.getD t 0 ∉ schedCache d C₀ σ t := hfd.1 have hq'res : q' ∈ schedCache d C₀ σ t := hfd.2.2 have hfifo : nextUse σ (t + 1) q' = none ∨ ∃ j j', nextUse σ (t + 1) q = some j ∧ nextUse σ (t + 1) q' = some j' ∧ j < j' := by apply fifo_nextUse_order σ (schedCache d C₀ σ t) t q' q · exact fifo_evict_eq_farthest d σ C₀ hagree · exact hdreduced t hft · exact hqq' constructor · exact exchangeSchedule_misses_le d t q q' σ C₀ rfl hqq' (fun s hs hr => hdreduced s hr) hft hq'res hfifo · intro s hs by_cases hs' : s ≤ t · rw [schedCache_exchangeSchedule_eq_d d t q q' σ C₀ hs'] exact hagree s hs' · have hst : s = t + 1 := by omega subst s have hFt : σ.getD t 0 ∉ schedCache (fifoSchedule σ C₀) C₀ σ t := by rw [← hagree t le_rfl] exact hft have hE : schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ (t + 1) = insert (σ.getD t 0) ((schedCache d C₀ σ t).erase q') := by rw [schedCache_exchangeScheduleCore, exchangeScheduleCore] dsimp rw [show (exchangeScheduleCore d t q q' σ C₀ t).1 = schedCache d C₀ σ t by rw [← schedCache_exchangeScheduleCore] exact schedCache_exchangeSchedule_eq_d d t q q' σ C₀ le_rfl] rw [show (exchangeScheduleCore d t q q' σ C₀ t).2 = q' by exact exchangeSchedule_at_t d t q q' σ C₀] rw [if_neg hft] have hF : schedCache (fifoSchedule σ C₀) C₀ σ (t + 1) = insert (σ.getD t 0) ((schedCache d C₀ σ t).erase q') := by rw [schedCache_fifoSchedule σ C₀ (t + 1)] unfold cacheSeq Policy.step rw [← schedCache_fifoSchedule σ C₀ t] rw [if_neg hFt] congr 2 · rw [← hagree t le_rfl] · change farthestInFuture (schedCache (fifoSchedule σ C₀) C₀ σ t) σ t = q' rw [← hagree t le_rfl] rw [← fifo_evict_eq_farthest d σ C₀ hagree] rw [hE, hF]

The exchange schedule is reduced at every fault after the first q' request: from J' on, q' is resident whenever d evicts it, and the multi-set branches always evict resident pages.

lemma exchangeSchedule_reduced_after (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) (hq : d t = q) (hqq' : q ≠ q') (hweak : ∀ s, t ≤ s → σ.getD s 0 ∉ schedCache d C₀ σ s → d s ∈ schedCache d C₀ σ s) (hft : σ.getD t 0 ∉ schedCache d C₀ σ t) (hq'res : q' ∈ schedCache d C₀ σ t) {j : ℕ} (hj : nextUse σ (t + 1) q = some j) (hq'ne : ∀ k, t + 1 ≤ k → k < t + 1 + j → σ.getD k 0 ≠ q') {j' : ℕ} (hj' : nextUse σ (t + 1) q' = some j') {s : ℕ} (hsJ' : t + 1 + j' < s) (hFault : σ.getD s 0 ∉ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s) : exchangeSchedule d t q q' σ C₀ s ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s := by let e : ℕ → Page := exchangeSchedule d t q q' σ C₀ let C' : Finset Page := schedCache e C₀ σ s have hC' : C' = (exchangeScheduleCore d t q q' σ C₀ s).1 := by unfold C' rw [schedCache_exchangeScheduleCore] have hFault' : σ.getD s 0 ∉ C' := by simpa [C'] using hFault have hcard : (schedCache d C₀ σ s).card ≤ C'.card := by rw [hC'] exact exchangeScheduleCore_card d t q q' σ C₀ hweak (by omega) -- a request that `d` serves from the cache is `q` or `q'` have hsig_in : σ.getD s 0 ∈ schedCache d C₀ σ s → σ.getD s 0 = q' ∨ σ.getD s 0 = q := by intro hsigD by_contra hnot have hinv := exchangeSchedule_invariant d t q q' σ C₀ hq hweak s (by omega) have hmem : σ.getD s 0 ∈ C' := by simpa [e, C'] using hinv (σ.getD s 0) (by intro hmem apply hnot rcases Finset.mem_insert.mp hmem with hqeq | hq'eq · exact Or.inr hqeq · exact Or.inl (Finset.mem_singleton.mp hq'eq)) hsigD exact hFault' hmem -- resident pages of `d` are resident in the exchange cache have hq_memD : q ∈ schedCache d C₀ σ s → q ∈ C' := by intro hqD have hmem := exchangeSchedule_q_mem d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'ne s (by omega) hqD simpa [e, C'] using hmem have hq'_memD : q' ∈ schedCache d C₀ σ s → q' ∈ C' := by intro hq'D have hmem := exchangeSchedule_q'_mem d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'ne hj' s hsJ' hq'D simpa [e, C'] using hmem -- `d` cannot hit at `s` (the exchange schedule faults there) have hdFault : σ.getD s 0 ∉ schedCache d C₀ σ s := by intro hdHit rcases hsig_in hdHit with hq'eq | hqeq · exact hFault' (hq'eq ▸ hq'_memD (hq'eq ▸ hdHit)) · exact hFault' (hqeq ▸ hq_memD (hqeq ▸ hdHit)) -- branch analysis of the exchange decision change (exchangeScheduleCore d t q q' σ C₀ s).2 ∈ schedCache (exchangeSchedule d t q q' σ C₀) C₀ σ s rw [exchangeScheduleCore_second] rw [← hC'] change exchangeDecision d t q q' σ C₀ C' s ∈ C' unfold exchangeDecision have hlt : ¬ s < t := by omega have hne : ¬ s = t := by omega rw [if_neg hlt, if_neg hne] by_cases h1 : d s = q' · rw [if_pos h1] -- d faults at s, so q' ∈ D(s), hence q' ∈ E(s) have hq'inD : q' ∈ schedCache d C₀ σ s := by have hd : d s ∈ schedCache d C₀ σ s := hweak s (by omega) hdFault rwa [h1] at hd exact hq'_memD hq'inD · rw [if_neg h1] by_cases hb4 : (σ.getD s 0 = q' ∨ σ.getD s 0 = q) ∧ σ.getD s 0 ∈ schedCache d C₀ σ s · rw [if_pos hb4] by_cases hf : ((C' \ schedCache d C₀ σ s).filter (fun x => x ≠ q')).Nonempty · rw [dif_pos hf] have hspec := Classical.choose_spec hf exact (Finset.mem_sdiff.mp (Finset.mem_filter.mp hspec).1).1 · rw [dif_neg hf] by_cases hm : (C' \ schedCache d C₀ σ s).Nonempty · rw [dif_pos hm] exact (Finset.mem_sdiff.mp (Classical.choose_spec hm)).1 · rw [dif_neg hm] exfalso have hsub : C' ⊆ schedCache d C₀ σ s := by intro y hy by_contra hyn exact hm ⟨y, Finset.mem_sdiff.mpr ⟨hy, hyn⟩⟩ have hEq : C' = schedCache d C₀ σ s := Finset.eq_of_subset_of_card_le hsub hcard exact hFault' (hEq ▸ hb4.2) · rw [if_neg hb4] by_cases h5 : d s ∈ C' · rw [if_pos h5] exact h5 · rw [if_neg h5] by_cases hm : (C' \ schedCache d C₀ σ s).Nonempty · rw [dif_pos hm] exact (Finset.mem_sdiff.mp (Classical.choose_spec hm)).1 · rw [dif_neg hm] exfalso have hsub : C' ⊆ schedCache d C₀ σ s := by intro y hy by_contra hyn exact hm ⟨y, Finset.mem_sdiff.mpr ⟨hy, hyn⟩⟩ have hEq : C' = schedCache d C₀ σ s := Finset.eq_of_subset_of_card_le hsub hcard exact h5 (hEq ▸ hweak s (by omega) hdFault)

The exchange has 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 (so d misses there too).

lemma exchangeSchedule_misses_le_plus_one (d : ℕ → Page) (t : ℕ) (q q' : Page) (σ : List Page) (C₀ : Finset Page) (hq : d t = q) (hqq' : q ≠ q') (hweak : ∀ s, t ≤ s → σ.getD s 0 ∉ schedCache d C₀ σ s → d s ∈ schedCache d C₀ σ s) (hft : σ.getD t 0 ∉ schedCache d C₀ σ t) (hq'res : q' ∈ schedCache d C₀ σ t) (hslack : (nextUse σ (t + 1) q' = none ∧ ∃ j, nextUse σ (t + 1) q = some j) ∨ ∃ j j', nextUse σ (t + 1) q = some j ∧ nextUse σ (t + 1) q' = some j' ∧ j < j' ∧ σ.getD (t + 1 + j') 0 ∉ schedCache d C₀ σ (t + 1 + j')) : schedMisses (exchangeSchedule d t q q' σ C₀) C₀ σ + 1 ≤ schedMisses d C₀ σ := by let e : ℕ → Page := exchangeSchedule d t q q' σ C₀ let eF : ℕ → ℕ := schedFaultAt e C₀ σ let dF : ℕ → ℕ := schedFaultAt d C₀ σ rcases hslack with ⟨hnone, hqreq⟩ | ⟨j, j', hj, hj', hjlt, hnoBad⟩ · -- CASE A: `q'` is never requested again have hq'ne_s : ∀ s, t + 1 ≤ s → s < σ.length → σ.getD s 0 ≠ q' := by intro s hs hlen have hnone' := nextUse_eq_none_iff.mp hnone apply hnone' (σ.getD s 0) have hget : (σ.drop (t + 1)).getD (s - (t + 1)) 0 = σ.getD s 0 := by rw [getD_drop] rw [Nat.add_sub_of_le hs] rw [← hget] have hlt' : s - (t + 1) < (σ.drop (t + 1)).length := by rw [List.length_drop] omega rw [List.getD_eq_getElem _ 0 hlt'] exact List.getElem_mem hlt' rcases hqreq with ⟨j, hj⟩ have hJlen : t + 1 + j < σ.length := by have hjlt' : j < (σ.drop (t + 1)).length := (nextUse_eq_some_iff.mp hj).1 rw [List.length_drop] at hjlt' omega have hJle : t + 1 + j + 1 ≤ σ.length := by omega have hq'neA : ∀ k, t + 1 ≤ k → k < t + 1 + j → σ.getD k 0 ≠ q' := by intro k hk1 hk2 exact hq'ne_s k hk1 (by omega) -- pointwise: fault equal for s ≤ t have hP0 : ∀ s, s ≤ t → eF s = dF s := by intro s hs unfold eF dF e schedFaultAt rw [schedCache_exchangeSchedule_eq_d d t q q' σ C₀ hs] -- pointwise: fault equal for t < s < J (window) have hP1 : ∀ s, t < s → s < t + 1 + j → eF s = dF s := by intro s hst hsJ unfold eF dF e schedFaultAt rw [exchangeSchedule_window d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'neA (s := s) hst (by omega)] have hne1 : σ.getD s 0 ≠ q := getD_ne_nextUse hj (by omega) hsJ have hne2 : σ.getD s 0 ≠ q' := hq'neA s (by omega) hsJ by_cases hr : σ.getD s 0 ∈ schedCache d C₀ σ s · rw [if_pos hr] have hrE' : σ.getD s 0 ∈ insert q ((schedCache d C₀ σ s).erase q') := by rw [Finset.mem_insert] right rw [Finset.mem_erase] constructor · exact hne2 · exact hr rw [if_pos hrE'] · rw [if_neg hr] have hrE' : σ.getD s 0 ∉ insert q ((schedCache d C₀ σ s).erase q') := by intro hm rcases Finset.mem_insert.mp hm with hqeq | hmem · exact hne1 hqeq · exact hr (Finset.mem_erase.mp hmem).2 rw [if_neg hrE'] -- pointwise: eF ≤ dF for J < s (no bad event) have hP3A : ∀ s, t < s → s < σ.length → eF s ≤ dF s := by intro s hst hlen unfold eF dF e schedFaultAt by_cases hr : σ.getD s 0 ∈ schedCache d C₀ σ s · by_cases hrE : σ.getD s 0 ∈ schedCache e C₀ σ s · rw [if_pos hrE, if_pos hr] · rw [if_neg hrE, if_pos hr] exfalso have hqqq' : σ.getD s 0 = q' ∨ σ.getD s 0 = q := by by_contra hnot have hinv := exchangeSchedule_invariant d t q q' σ C₀ hq hweak s (by omega) exact hrE (hinv (σ.getD s 0) (by intro hmem2 apply hnot rcases Finset.mem_insert.mp hmem2 with hqeq | hq'eq · exact Or.inr hqeq · exact Or.inl (Finset.mem_singleton.mp hq'eq)) hr) rcases hqqq' with hq'eq | hqeq · exact hq'ne_s s (by omega) hlen hq'eq · have hqE : q ∈ schedCache e C₀ σ s := by exact exchangeSchedule_q_mem d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'neA s hst (hqeq ▸ hr) exact hrE (hqeq ▸ hqE) · rw [if_neg hr] by_cases hrE : σ.getD s 0 ∈ schedCache e C₀ σ s · rw [if_pos hrE] omega · rw [if_neg hrE] -- good event at J have hgood := exchangeSchedule_good d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'neA -- split the sum have hdisj : Disjoint (Finset.range (t + 1 + j + 1)) (Finset.Ico (t + 1 + j + 1) σ.length) := by rw [Finset.disjoint_left] intro s hs1 hs2 have h1 : s < t + 1 + j + 1 := Finset.mem_range.mp hs1 have h2 : t + 1 + j + 1 ≤ s := (Finset.mem_Ico.mp hs2).1 omega have hunion : Finset.range (t + 1 + j + 1) ∪ Finset.Ico (t + 1 + j + 1) σ.length = Finset.range σ.length := by ext s simp [Finset.mem_Ico] constructor · intro h rcases h with hs | ⟨h1, h2⟩ · omega · exact h2 · intro hs by_cases hs' : s < t + 1 + j + 1 · exact Or.inl (Nat.lt_succ_iff.mp hs') · right constructor · omega · exact hs have hsum_e : (∑ s ∈ Finset.range σ.length, eF s) = (∑ s ∈ Finset.range (t + 1 + j + 1), eF s) + ∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, eF s := by rw [← hunion, Finset.sum_union hdisj] have hsum_d : (∑ s ∈ Finset.range σ.length, dF s) = (∑ s ∈ Finset.range (t + 1 + j + 1), dF s) + ∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, dF s := by rw [← hunion, Finset.sum_union hdisj] -- first part: Σ_{<J+1} eF + 1 ≤ Σ_{<J+1} dF have hpart1 : (∑ s ∈ Finset.range (t + 1 + j + 1), eF s) + 1 ≤ ∑ s ∈ Finset.range (t + 1 + j + 1), dF s := by rw [Finset.sum_range_succ] rw [Finset.sum_range_succ] have heJ : eF (t + 1 + j) = 0 := by unfold eF schedFaultAt rw [if_pos hgood.1] have hdJ : dF (t + 1 + j) = 1 := by unfold dF schedFaultAt rw [if_neg hgood.2] rw [heJ, hdJ] have hle : (∑ s ∈ Finset.range (t + 1 + j), eF s) ≤ ∑ s ∈ Finset.range (t + 1 + j), dF s := by exact Finset.sum_le_sum (fun s hs => by by_cases hst' : s ≤ t · exact le_of_eq (hP0 s hst') · have hts' : t < s := by omega exact le_of_eq (hP1 s hts' (Finset.mem_range.mp hs))) have hle' : (∑ s ∈ Finset.range (t + 1 + j), eF s) + 1 ≤ (∑ s ∈ Finset.range (t + 1 + j), dF s) + 1 := Nat.add_le_add_right hle 1 simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using hle' -- second part: Σ_{[J+1,len)} eF ≤ Σ dF have hpart2 : (∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, eF s) ≤ ∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, dF s := by apply Finset.sum_le_sum intro s hs have hst' : t < s := by have h1 : t + 1 + j + 1 ≤ s := (Finset.mem_Ico.mp hs).1 omega exact hP3A s hst' (Finset.mem_Ico.mp hs).2 -- assemble unfold schedMisses change (∑ s ∈ Finset.range σ.length, eF s) + 1 ≤ ∑ s ∈ Finset.range σ.length, dF s rw [hsum_e, hsum_d] have h := add_le_add hpart1 hpart2 simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using h · -- CASE B: the first request of `q` comes before the first request of `q'` have hJlen : t + 1 + j < σ.length := by have hjlt' : j < (σ.drop (t + 1)).length := (nextUse_eq_some_iff.mp hj).1 rw [List.length_drop] at hjlt' omega have hJ'len : t + 1 + j' < σ.length := by have hj'lt' : j' < (σ.drop (t + 1)).length := (nextUse_eq_some_iff.mp hj').1 rw [List.length_drop] at hj'lt' omega have hJle : t + 1 + j + 1 ≤ σ.length := by omega have hJ'le : t + 1 + j' + 1 ≤ σ.length := by omega have hJJ' : t + 1 + j + 1 ≤ t + 1 + j' := by omega have hq'neB : ∀ k, t + 1 ≤ k → k < t + 1 + j → σ.getD k 0 ≠ q' := by intro k hk1 hk2 exact getD_ne_nextUse hj' hk1 (by omega) -- pointwise: fault equal for s ≤ t have hP0 : ∀ s, s ≤ t → eF s = dF s := by intro s hs unfold eF dF e schedFaultAt rw [schedCache_exchangeSchedule_eq_d d t q q' σ C₀ hs] -- pointwise: fault equal for t < s < J (window) have hP1 : ∀ s, t < s → s < t + 1 + j → eF s = dF s := by intro s hst hsJ unfold eF dF e schedFaultAt rw [exchangeSchedule_window d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'neB (s := s) hst (by omega)] have hne1 : σ.getD s 0 ≠ q := getD_ne_nextUse hj (by omega) hsJ have hne2 : σ.getD s 0 ≠ q' := hq'neB s (by omega) hsJ by_cases hr : σ.getD s 0 ∈ schedCache d C₀ σ s · rw [if_pos hr] have hrE' : σ.getD s 0 ∈ insert q ((schedCache d C₀ σ s).erase q') := by rw [Finset.mem_insert] right rw [Finset.mem_erase] constructor · exact hne2 · exact hr rw [if_pos hrE'] · rw [if_neg hr] have hrE' : σ.getD s 0 ∉ insert q ((schedCache d C₀ σ s).erase q') := by intro hm rcases Finset.mem_insert.mp hm with hqeq | hmem · exact hne1 hqeq · exact hr (Finset.mem_erase.mp hmem).2 rw [if_neg hrE'] -- pointwise: eF ≤ dF for s ≠ J' (the bad event only at J') have hP3 : ∀ s, t < s → s < σ.length → s ≠ t + 1 + j' → eF s ≤ dF s := by intro s hst hlen hsne unfold eF dF e schedFaultAt by_cases hr : σ.getD s 0 ∈ schedCache d C₀ σ s · by_cases hrE : σ.getD s 0 ∈ schedCache e C₀ σ s · rw [if_pos hrE, if_pos hr] · rw [if_neg hrE, if_pos hr] exfalso exact hsne (exchangeSchedule_bad d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'neB hj' hst hr hrE) · rw [if_neg hr] by_cases hrE : σ.getD s 0 ∈ schedCache e C₀ σ s · rw [if_pos hrE] omega · rw [if_neg hrE] -- good event at J have hgood := exchangeSchedule_good d t q q' σ C₀ hq hqq' hweak hft hq'res hj hq'neB -- split the sum have hdisj : Disjoint (Finset.range (t + 1 + j + 1)) (Finset.Ico (t + 1 + j + 1) σ.length) := by rw [Finset.disjoint_left] intro s hs1 hs2 have h1 : s < t + 1 + j + 1 := Finset.mem_range.mp hs1 have h2 : t + 1 + j + 1 ≤ s := (Finset.mem_Ico.mp hs2).1 omega have hunion : Finset.range (t + 1 + j + 1) ∪ Finset.Ico (t + 1 + j + 1) σ.length = Finset.range σ.length := by ext s simp [Finset.mem_Ico] constructor · intro h rcases h with hs | ⟨h1, h2⟩ · omega · exact h2 · intro hs by_cases hs' : s < t + 1 + j + 1 · exact Or.inl (Nat.lt_succ_iff.mp hs') · right constructor · omega · exact hs have hsum_e : (∑ s ∈ Finset.range σ.length, eF s) = (∑ s ∈ Finset.range (t + 1 + j + 1), eF s) + ∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, eF s := by rw [← hunion, Finset.sum_union hdisj] have hsum_d : (∑ s ∈ Finset.range σ.length, dF s) = (∑ s ∈ Finset.range (t + 1 + j + 1), dF s) + ∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, dF s := by rw [← hunion, Finset.sum_union hdisj] -- first part: Σ_{<J+1} eF + 1 ≤ Σ_{<J+1} dF have hpart1 : (∑ s ∈ Finset.range (t + 1 + j + 1), eF s) + 1 ≤ ∑ s ∈ Finset.range (t + 1 + j + 1), dF s := by rw [Finset.sum_range_succ] rw [Finset.sum_range_succ] have heJ : eF (t + 1 + j) = 0 := by unfold eF schedFaultAt rw [if_pos hgood.1] have hdJ : dF (t + 1 + j) = 1 := by unfold dF schedFaultAt rw [if_neg hgood.2] rw [heJ, hdJ] have hle : (∑ s ∈ Finset.range (t + 1 + j), eF s) ≤ ∑ s ∈ Finset.range (t + 1 + j), dF s := by exact Finset.sum_le_sum (fun s hs => by by_cases hst' : s ≤ t · exact le_of_eq (hP0 s hst') · have hts' : t < s := by omega exact le_of_eq (hP1 s hts' (Finset.mem_range.mp hs))) have hle' : (∑ s ∈ Finset.range (t + 1 + j), eF s) + 1 ≤ (∑ s ∈ Finset.range (t + 1 + j), dF s) + 1 := Nat.add_le_add_right hle 1 simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using hle' -- second part: Σ_{[J+1,len)} eF ≤ Σ dF + 1 have hpart2 : (∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, eF s) ≤ ∑ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, dF s := by have hper : ∀ s ∈ Finset.Ico (t + 1 + j + 1) σ.length, eF s ≤ dF s := by intro s hs have hst' : t < s := by have h1 : t + 1 + j + 1 ≤ s := (Finset.mem_Ico.mp hs).1 exact lt_of_lt_of_le (by omega : t < t + 1 + j + 1) h1 by_cases hsne : s = t + 1 + j' · subst s unfold eF dF schedFaultAt dsimp [e] have hsig : σ.getD (t + 1 + j') 0 = q' := getD_eq_nextUse hj' have hnotE : σ.getD (t + 1 + j') 0 ∉ schedCache e C₀ σ (t + 1 + j') := by rw [hsig] apply exchangeSchedule_q'_absent d t q q' σ C₀ hweak hft hq'res hj' · omega · rfl rw [if_neg hnotE] rw [if_neg hnoBad] · exact hP3 s hst' (Finset.mem_Ico.mp hs).2 hsne exact Finset.sum_le_sum hper -- assemble unfold schedMisses change (∑ s ∈ Finset.range σ.length, eF s) + 1 ≤ ∑ s ∈ Finset.range σ.length, dF s rw [hsum_e, hsum_d] have h := add_le_add hpart1 hpart2 simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using h

The repair schedule: agrees with e everywhere except it evicts q' at t and at nop (the first q' request; the second eviction is a no-op that makes the cache coincide with e's afterwards).

noncomputable def repairSchedule (e : ℕ → Page) (t : ℕ) (q' : Page) (nop : ℕ) : ℕ → Page := fun s => if s = t ∨ s = nop then q' else e s

The repair schedule evicts q' at t.

lemma repairSchedule_at_t (e : ℕ → Page) (t : ℕ) (q' : Page) (nop : ℕ) : repairSchedule e t q' nop t = q' := by unfold repairSchedule simp

The repair schedule's cache agrees with e's up to t.

lemma schedCache_repairSchedule_eq_e (e : ℕ → Page) (t : ℕ) (q' : Page) (nop : ℕ) (htn : t < nop) (σ : List Page) (C₀ : Finset Page) {s : ℕ} (hs : s ≤ t) : schedCache (repairSchedule e t q' nop) C₀ σ s = schedCache e C₀ σ s := by induction s with | zero => rfl | succ s ih => rw [schedCache, schedCache] rw [ih (by omega)] unfold repairSchedule simp [show s ≠ t by omega, show s ≠ nop by omega]

The repair's cache just after t is e's cache with q' removed.

lemma repairSchedule_base (e : ℕ → Page) (σ : List Page) (C₀ : Finset Page) (hC₀ : C₀.Nonempty) {t : ℕ} (ht : t < σ.length) (hagree : agreeWithFIF e C₀ σ t) (hdis : schedCache e C₀ σ (t + 1) ≠ schedCache (fifoSchedule σ C₀) C₀ σ (t + 1)) (hnoop : e t ∉ schedCache e C₀ σ t) (hq' : q' = fifoSchedule σ C₀ t) {j' : ℕ} (Variable name `hj'` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hj' : nextUse σ (t + 1) q' = some j') : schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ (t + 1) = (schedCache e C₀ σ (t + 1)).erase q' := by have hft : σ.getD t 0 ∉ schedCache e C₀ σ t := by intro hft have hFt : σ.getD t 0 ∈ schedCache (fifoSchedule σ C₀) C₀ σ t := by rw [← hagree t le_rfl] exact hft have hD : schedCache e C₀ σ (t + 1) = schedCache e C₀ σ t := by rw [schedCache] rw [if_pos hft] have hF : schedCache (fifoSchedule σ C₀) C₀ σ (t + 1) = schedCache (fifoSchedule σ C₀) C₀ σ t := by rw [schedCache] rw [if_pos hFt] exact hdis ((hD.trans (hagree t le_rfl)).trans hF.symm) have hq'res : q' ∈ schedCache e C₀ σ t := by have hfd := first_disagree e σ C₀ hC₀ ht hagree hdis rw [hq'] exact hfd.2.2 have hsig_ne : σ.getD t 0 ≠ q' := by intro hsig exact hft (hsig ▸ hq'res) rw [schedCache] rw [schedCache_repairSchedule_eq_e e t q' (t + 1 + j') (by omega) σ C₀ le_rfl] rw [repairSchedule_at_t] rw [if_neg hft] rw [schedCache] rw [if_neg hft] rw [Finset.erase_eq_of_notMem hnoop] rw [Finset.erase_insert_of_ne hsig_ne]

The repair's cache step inside the window.

lemma repairSchedule_step (e : ℕ → Page) (σ : List Page) (C₀ : Finset Page) (Variable name `hC₀` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hC₀ : C₀.Nonempty) {t : ℕ} (Variable name `ht` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`ht : t < σ.length) (Variable name `hagree` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hagree : agreeWithFIF e C₀ σ t) (Variable name `hdis` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hdis : schedCache e C₀ σ (t + 1) ≠ schedCache (fifoSchedule σ C₀) C₀ σ (t + 1)) (Variable name `hnoop` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hnoop : e t ∉ schedCache e C₀ σ t) (Variable name `hq'` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hq' : q' = fifoSchedule σ C₀ t) {j' : ℕ} (hj' : nextUse σ (t + 1) q' = some j') (s : ℕ) (ih : t < s → s ≤ t + 1 + j' → schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s = (schedCache e C₀ σ s).erase q') (hts : t < s) (hsJ' : s < t + 1 + j') : schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ (s + 1) = (schedCache e C₀ σ (s + 1)).erase q' := by have hsig_ne_q' : σ.getD s 0 ≠ q' := getD_ne_nextUse (k := s) hj' (by omega) hsJ' have hds : repairSchedule e t q' (t + 1 + j') s = e s := by unfold repairSchedule simp [show s ≠ t by omega, show s ≠ t + 1 + j' by omega] change (if σ.getD s 0 ∈ schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s then schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s else insert (σ.getD s 0) ((schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s).erase (repairSchedule e t q' (t + 1 + j') s))) = (if σ.getD s 0 ∈ schedCache e C₀ σ s then schedCache e C₀ σ s else insert (σ.getD s 0) ((schedCache e C₀ σ s).erase (e s))).erase q' rw [hds] rw [ih hts (by omega)] by_cases hr : σ.getD s 0 ∈ schedCache e C₀ σ s · have hr' : σ.getD s 0 ∈ (schedCache e C₀ σ s).erase q' := by rw [Finset.mem_erase] constructor · exact hsig_ne_q' · exact hr rw [if_pos hr, if_pos hr'] · rw [if_neg hr] have hr' : σ.getD s 0 ∉ (schedCache e C₀ σ s).erase q' := by intro hm exact hr (Finset.mem_erase.mp hm).2 rw [if_neg hr'] rw [Finset.erase_insert_of_ne hsig_ne_q'] have herase_comm : ((schedCache e C₀ σ s).erase q').erase (e s) = ((schedCache e C₀ σ s).erase (e s)).erase q' := by ext x simp [Finset.mem_erase, and_left_comm, This simp argument is unused: and_assoc Hint: Omit it from the simp argument list. simp [Finset.mem_erase, and_left_comm,̵ ̵a̵n̵d̵_̵a̵s̵s̵o̵c̵] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`and_assoc] rw [herase_comm]

In the window (t, J'], the repair schedule's cache is e's cache with q' removed.

lemma repairSchedule_window (e : ℕ → Page) (σ : List Page) (C₀ : Finset Page) (hC₀ : C₀.Nonempty) {t : ℕ} (ht : t < σ.length) (hagree : agreeWithFIF e C₀ σ t) (hdis : schedCache e C₀ σ (t + 1) ≠ schedCache (fifoSchedule σ C₀) C₀ σ (t + 1)) (hnoop : e t ∉ schedCache e C₀ σ t) (hq' : q' = fifoSchedule σ C₀ t) {j' : ℕ} (hj' : nextUse σ (t + 1) q' = some j') {s : ℕ} (hs1 : t < s) (hs2 : s ≤ t + 1 + j') : schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s = (schedCache e C₀ σ s).erase q' := by induction s with | zero => omega | succ s ih => by_cases hs_eq : s = t · subst s exact repairSchedule_base e σ C₀ hC₀ ht hagree hdis hnoop hq' hj' · exact repairSchedule_step e σ C₀ hC₀ ht hagree hdis hnoop hq' hj' s ih (by omega) (by omega)

After the first q' request, the repair's cache contains e's.

lemma repairSchedule_superset (e : ℕ → Page) (σ : List Page) (C₀ : Finset Page) (hC₀ : C₀.Nonempty) {t : ℕ} (ht : t < σ.length) (hagree : agreeWithFIF e C₀ σ t) (hdis : schedCache e C₀ σ (t + 1) ≠ schedCache (fifoSchedule σ C₀) C₀ σ (t + 1)) (hnoop : e t ∉ schedCache e C₀ σ t) (hq' : q' = fifoSchedule σ C₀ t) {j' : ℕ} (hj' : nextUse σ (t + 1) q' = some j') {s : ℕ} (hs : t + 1 + j' < s) : schedCache e C₀ σ s ⊆ schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s := by induction s with | zero => omega | succ s ih => by_cases hs_eq : s = t + 1 + j' · subst s -- base: the repair evicts q' at J' (a no-op) and reloads it have hwin : schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ (t + 1 + j') = (schedCache e C₀ σ (t + 1 + j')).erase q' := by exact repairSchedule_window e σ C₀ hC₀ ht hagree hdis hnoop hq' hj' (by omega) (by rfl) have hsig : (σ[t + 1 + j']?).getD 0 = q' := by simpa using getD_eq_nextUse hj' have hq'notE : q' ∉ (schedCache e C₀ σ (t + 1 + j')).erase q' := by intro hm exact (Finset.mem_erase.mp hm).1 rfl change (if σ.getD (t + 1 + j') 0 ∈ schedCache e C₀ σ (t + 1 + j') then schedCache e C₀ σ (t + 1 + j') else insert (σ.getD (t + 1 + j') 0) ((schedCache e C₀ σ (t + 1 + j')).erase (e (t + 1 + j')))) ⊆ (if σ.getD (t + 1 + j') 0 ∈ schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ (t + 1 + j') then schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ (t + 1 + j') else insert (σ.getD (t + 1 + j') 0) ((schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ (t + 1 + j')).erase (repairSchedule e t q' (t + 1 + j') (t + 1 + j')))) rw [hwin] unfold repairSchedule simp [show t + 1 + j' ≠ t by omega] simp [hsig] intro x hx by_cases hr : q' ∈ schedCache e C₀ σ (t + 1 + j') · rw [if_pos hr] at hx rw [Finset.mem_insert] by_cases hxq' : x = q' · left exact hxq' · right rw [Finset.mem_erase] constructor · exact hxq' · exact hx · rw [if_neg hr] at hx rcases Finset.mem_insert.mp hx with hxq' | hxin · rw [hxq'] rw [Finset.mem_insert] left rfl · have hxin' : x ∈ (schedCache e C₀ σ (t + 1 + j')).erase (e (t + 1 + j')) := hxin have hxE : x ∈ schedCache e C₀ σ (t + 1 + j') := (Finset.mem_erase.mp hxin').2 have hxne_q' : x ≠ q' := by intro hxq' exact hr (hxq' ▸ hxE) rw [Finset.mem_insert] right rw [Finset.mem_erase] constructor · exact hxne_q' · exact hxE · -- step: s > J' have hsJ' : t + 1 + j' < s := by omega have ih' := ih hsJ' have hds : repairSchedule e t q' (t + 1 + j') s = e s := by unfold repairSchedule simp [show s ≠ t by omega, show s ≠ t + 1 + j' by omega] change (if σ.getD s 0 ∈ schedCache e C₀ σ s then schedCache e C₀ σ s else insert (σ.getD s 0) ((schedCache e C₀ σ s).erase (e s))) ⊆ (if σ.getD s 0 ∈ schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s then schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s else insert (σ.getD s 0) ((schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s).erase (repairSchedule e t q' (t + 1 + j') s))) rw [hds] intro x hx by_cases hr : σ.getD s 0 ∈ schedCache e C₀ σ s · rw [if_pos hr] at hx rw [if_pos (ih' hr)] exact ih' hx · rw [if_neg hr] at hx rcases Finset.mem_insert.mp hx with hxr | hxin · subst x by_cases hrE : σ.getD s 0 ∈ schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s · rw [if_pos hrE] exact hrE · rw [if_neg hrE] rw [Finset.mem_insert] left rfl · have hxE : x ∈ schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s := ih' (Finset.mem_erase.mp hxin).2 have hxne : x ≠ e s := (Finset.mem_erase.mp hxin).1 by_cases hrE : σ.getD s 0 ∈ schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s · rw [if_pos hrE] exact hxE · rw [if_neg hrE] rw [Finset.mem_insert] right rw [Finset.mem_erase] constructor · exact hxne · exact hxE
lemma repair_step (e : ℕ → Page) (σ : List Page) (C₀ : Finset Page) (hC₀ : C₀.Nonempty) {t : ℕ} (ht : t < σ.length) (hagree : agreeWithFIF e C₀ σ t) (hdis : schedCache e C₀ σ (t + 1) ≠ schedCache (fifoSchedule σ C₀) C₀ σ (t + 1)) (hnoop : e t ∉ schedCache e C₀ σ t) {j' : ℕ} (hj' : nextUse σ (t + 1) (fifoSchedule σ C₀ t) = some j') : schedMisses (repairSchedule e t (fifoSchedule σ C₀ t) (t + 1 + j')) C₀ σ ≤ schedMisses e C₀ σ + 1 ∧ agreeWithFIF (repairSchedule e t (fifoSchedule σ C₀ t) (t + 1 + j')) C₀ σ (t + 1) := by let q' : Page := fifoSchedule σ C₀ t let r : ℕ → Page := repairSchedule e t q' (t + 1 + j') let eF : ℕ → ℕ := schedFaultAt e C₀ σ let rF : ℕ → ℕ := schedFaultAt r C₀ σ have hft : σ.getD t 0 ∉ schedCache e C₀ σ t := by intro hft have hFt : σ.getD t 0 ∈ schedCache (fifoSchedule σ C₀) C₀ σ t := by rw [← hagree t le_rfl] exact hft have hD : schedCache e C₀ σ (t + 1) = schedCache e C₀ σ t := by rw [schedCache] rw [if_pos hft] have hF : schedCache (fifoSchedule σ C₀) C₀ σ (t + 1) = schedCache (fifoSchedule σ C₀) C₀ σ t := by rw [schedCache] rw [if_pos hFt] exact hdis ((hD.trans (hagree t le_rfl)).trans hF.symm) have hq'res : q' ∈ schedCache e C₀ σ t := by have hfd := first_disagree e σ C₀ hC₀ ht hagree hdis exact hfd.2.2 have hsig_ne : σ.getD t 0 ≠ q' := by intro hsig exact hft (hsig ▸ hq'res) have hJ'len : t + 1 + j' < σ.length := by have hj'lt' : j' < (σ.drop (t + 1)).length := (nextUse_eq_some_iff.mp hj').1 rw [List.length_drop] at hj'lt' omega constructor · -- misses: rF ≤ eF + 1 pointwise have hper : ∀ s, s < σ.length → rF s ≤ eF s + (if s = t + 1 + j' then 1 else 0) := by intro s hlen by_cases hst : s ≤ t · unfold rF eF r schedFaultAt rw [schedCache_repairSchedule_eq_e e t q' (t + 1 + j') (by omega) σ C₀ hst] rw [show (if s = t + 1 + j' then 1 else 0) = 0 by simp [show s ≠ t + 1 + j' by omega]] omega · have hts' : t < s := by omega by_cases hsJ' : s < t + 1 + j' · -- in the window: faults coincide have hwin : schedCache r C₀ σ s = (schedCache e C₀ σ s).erase q' := by exact repairSchedule_window e σ C₀ hC₀ ht hagree hdis hnoop rfl hj' hts' (by omega) unfold rF eF r schedFaultAt rw [hwin] have hneq : σ.getD s 0 ≠ q' := getD_ne_nextUse (k := s) hj' (by omega) hsJ' by_cases hr : σ.getD s 0 ∈ schedCache e C₀ σ s · rw [if_pos hr] have hr' : σ.getD s 0 ∈ (schedCache e C₀ σ s).erase q' := by rw [Finset.mem_erase] constructor · exact hneq · exact hr rw [if_pos hr'] rw [show (if s = t + 1 + j' then 1 else 0) = 0 by simp [show s ≠ t + 1 + j' by omega]] · rw [if_neg hr] have hr' : σ.getD s 0 ∉ (schedCache e C₀ σ s).erase q' := by intro hm exact hr (Finset.mem_erase.mp hm).2 rw [if_neg hr'] rw [show (if s = t + 1 + j' then 1 else 0) = 0 by simp [show s ≠ t + 1 + j' by omega]] · -- s ≥ J' by_cases hseq : s = t + 1 + j' · subst s -- at J': r faults unfold rF eF r schedFaultAt have hwin : schedCache r C₀ σ (t + 1 + j') = (schedCache e C₀ σ (t + 1 + j')).erase q' := by exact repairSchedule_window e σ C₀ hC₀ ht hagree hdis hnoop rfl hj' (by omega) (by rfl) rw [hwin] have hsig : σ.getD (t + 1 + j') 0 = q' := getD_eq_nextUse hj' have hq'notE : q' ∉ (schedCache e C₀ σ (t + 1 + j')).erase q' := by intro hm exact (Finset.mem_erase.mp hm).1 rfl rw [hsig] rw [if_neg hq'notE] have hind : (if t + 1 + j' = t + 1 + j' then 1 else 0) = 1 := by simp rw [hind] by_cases hr : q' ∈ schedCache e C₀ σ (t + 1 + j') · rw [if_pos hr] · rw [if_neg hr] omega · -- s > J': E ⊆ Ê have hsJ''' : t + 1 + j' < s := by omega have hsup : schedCache e C₀ σ s ⊆ schedCache r C₀ σ s := by exact repairSchedule_superset e σ C₀ hC₀ ht hagree hdis hnoop rfl hj' hsJ''' unfold rF eF r schedFaultAt by_cases hr : σ.getD s 0 ∈ schedCache e C₀ σ s · rw [if_pos hr] rw [if_pos (hsup hr)] rw [show (if s = t + 1 + j' then 1 else 0) = 0 by simp [show s ≠ t + 1 + j' by omega]] · rw [if_neg hr] by_cases hr' : σ.getD s 0 ∈ schedCache r C₀ σ s · rw [if_pos hr'] rw [show (if s = t + 1 + j' then 1 else 0) = 0 by simp [show s ≠ t + 1 + j' by omega]] omega · rw [if_neg hr'] rw [show (if s = t + 1 + j' then 1 else 0) = 0 by simp [show s ≠ t + 1 + j' by omega]] unfold schedMisses change (∑ s ∈ Finset.range σ.length, rF s) ≤ (∑ s ∈ Finset.range σ.length, eF s) + 1 have hsum1 : (∑ s ∈ Finset.range σ.length, rF s) ≤ ∑ s ∈ Finset.range σ.length, (eF s + (if s = t + 1 + j' then 1 else 0)) := by exact Finset.sum_le_sum (fun s hs => hper s (Finset.mem_range.mp hs)) have hsum2 : (∑ s ∈ Finset.range σ.length, (eF s + (if s = t + 1 + j' then 1 else 0))) = (∑ s ∈ Finset.range σ.length, eF s) + ∑ s ∈ Finset.range σ.length, (if s = t + 1 + j' then 1 else 0) := by rw [Finset.sum_add_distrib] have hsum3 : (∑ s ∈ Finset.range σ.length, (if s = t + 1 + j' then 1 else 0)) ≤ 1 := by rw [Finset.sum_ite_eq'] by_cases hJ'in : t + 1 + j' ∈ Finset.range σ.length · simp [hJ'in] · simp [hJ'in] rw [hsum2] at hsum1 exact le_trans hsum1 (Nat.add_le_add_left hsum3 _) · -- agree through t + 1 intro s hs by_cases hs' : s ≤ t · rw [schedCache_repairSchedule_eq_e e t q' (t + 1 + j') (by omega) σ C₀ hs'] exact hagree s hs' · have hst : s = t + 1 := by omega subst s have hbase : schedCache r C₀ σ (t + 1) = (schedCache e C₀ σ (t + 1)).erase q' := by exact repairSchedule_base e σ C₀ hC₀ ht hagree hdis hnoop rfl hj' have hF : schedCache (fifoSchedule σ C₀) C₀ σ (t + 1) = insert (σ.getD t 0) ((schedCache e C₀ σ t).erase q') := by rw [schedCache_fifoSchedule σ C₀ (t + 1)] unfold cacheSeq Policy.step rw [← schedCache_fifoSchedule σ C₀ t] rw [if_neg (by rw [← hagree t le_rfl]; exact hft)] congr 2 · rw [hagree t le_rfl] · change farthestInFuture (schedCache (fifoSchedule σ C₀) C₀ σ t) σ t = q' rw [← hagree t le_rfl] rw [← fifo_evict_eq_farthest e σ C₀ hagree] have hE : schedCache r C₀ σ (t + 1) = insert (σ.getD t 0) ((schedCache e C₀ σ t).erase q') := by rw [hbase] rw [schedCache] rw [if_neg hft] rw [Finset.erase_eq_of_notMem hnoop] rw [Finset.erase_insert_of_ne hsig_ne] rw [hE, hF]

The B2 window base: when q = e t is resident, repair's cache at t+1 is insert q ((E(t+1)).erase q').

lemma repairSchedule_base_swap (e : ℕ → Page) (σ : List Page) (C₀ : Finset Page) (hC₀ : C₀.Nonempty) {t : ℕ} (ht : t < σ.length) (hagree : agreeWithFIF e C₀ σ t) (hdis : schedCache e C₀ σ (t + 1) ≠ schedCache (fifoSchedule σ C₀) C₀ σ (t + 1)) (hqin : e t ∈ schedCache e C₀ σ t) (hq' : q' = fifoSchedule σ C₀ t) (hq : q = e t) {j' : ℕ} (Variable name `hj'` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hj' : nextUse σ (t + 1) q' = some j') : schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ (t + 1) = insert q ((schedCache e C₀ σ (t + 1)).erase q') := by have hft : σ.getD t 0 ∉ schedCache e C₀ σ t := by intro hft have hFt : σ.getD t 0 ∈ schedCache (fifoSchedule σ C₀) C₀ σ t := by rw [← hagree t le_rfl] exact hft have hD : schedCache e C₀ σ (t + 1) = schedCache e C₀ σ t := by rw [schedCache] rw [if_pos hft] have hF : schedCache (fifoSchedule σ C₀) C₀ σ (t + 1) = schedCache (fifoSchedule σ C₀) C₀ σ t := by rw [schedCache] rw [if_pos hFt] exact hdis ((hD.trans (hagree t le_rfl)).trans hF.symm) have hq'res : q' ∈ schedCache e C₀ σ t := by have hfd := first_disagree e σ C₀ hC₀ ht hagree hdis rw [hq'] exact hfd.2.2 have hqne : q ≠ q' := by have hfd := first_disagree e σ C₀ hC₀ ht hagree hdis intro hqq' exact hfd.2.1 (by rw [← hq, ← hq']; exact hqq') have hsig_ne_q' : σ.getD t 0 ≠ q' := by intro hsig exact hft (hsig ▸ hq'res) have hsig_ne_q : σ.getD t 0 ≠ q := by intro hsig exact hft (hsig ▸ hq ▸ hqin) rw [schedCache] rw [schedCache_repairSchedule_eq_e e t q' (t + 1 + j') (by omega) σ C₀ le_rfl] rw [repairSchedule_at_t] rw [if_neg hft] rw [schedCache] rw [if_neg hft] rw [← hq] rw [Finset.erase_insert_of_ne hsig_ne_q'] have hqin' : q ∈ schedCache e C₀ σ t := by rw [hq] exact hqin have hE : (schedCache e C₀ σ t).erase q' = insert q (((schedCache e C₀ σ t).erase q).erase q') := by ext x constructor · intro hx have hxq' : x ≠ q' := (Finset.mem_erase.mp hx).1 have hxin : x ∈ schedCache e C₀ σ t := (Finset.mem_erase.mp hx).2 rw [Finset.mem_insert] by_cases hxq : x = q · exact Or.inl hxq · exact Or.inr (Finset.mem_erase.mpr ⟨hxq', Finset.mem_erase.mpr ⟨hxq, hxin⟩⟩) · intro hx rw [Finset.mem_insert] at hx rcases hx with hxq | hxin · rw [hxq] exact Finset.mem_erase.mpr ⟨hqne, hqin'⟩ · have hx' := Finset.mem_erase.mp (Finset.mem_erase.mp hxin).2 exact Finset.mem_erase.mpr ⟨(Finset.mem_erase.mp hxin).1, hx'.2⟩ rw [hE] rw [Finset.insert_comm]

Within the (t, J] window, q is not in e's cache (e evicts q at t, and q is not requested before J).

lemma swap_q_not_mem (e : ℕ → Page) (σ : List Page) (C₀ : Finset Page) {t : ℕ} {q : Page} (hq : e t = q) (hqin : q ∈ schedCache e C₀ σ t) (hft : σ.getD t 0 ∉ schedCache e C₀ σ t) {j : ℕ} (hj : nextUse σ (t + 1) q = some j) {s : ℕ} (hs1 : t < s) (hs2 : s ≤ t + 1 + j) : q ∉ schedCache e C₀ σ s := by induction s with | zero => omega | succ s ih => by_cases hs_eq : s = t · subst s rw [schedCache] rw [if_neg hft] intro hm rw [Finset.mem_insert] at hm rcases hm with hqr | hqin2 · have h : σ.getD t 0 ∈ schedCache e C₀ σ t := by rwa [← hqr] exact hft h · exact (Finset.mem_erase.mp hqin2).1 hq.symm · have hts : t < s := by omega have hsJ' : s < t + 1 + j := by omega have hsig_ne : σ.getD s 0 ≠ q := getD_ne_nextUse (k := s) hj (by omega) hsJ' rw [schedCache] by_cases hr : σ.getD s 0 ∈ schedCache e C₀ σ s · rw [if_pos hr] exact ih hts (by omega) · rw [if_neg hr] intro hm rcases Finset.mem_insert.mp hm with hqr | hqin2 · exact hsig_ne hqr.symm · exact ih hts (by omega) (Finset.mem_erase.mp hqin2).2

The B2 window step (disjunctive version): the swap relation Ê = insert q (E − q') or the B1-style relation Ê = E − q' is preserved within (t, J) (the former switches to the latter when e evicts q).

lemma repairSchedule_step_swap' (e : ℕ → Page) (σ : List Page) (C₀ : Finset Page) (Variable name `hC₀` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hC₀ : C₀.Nonempty) {t : ℕ} (Variable name `ht` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`ht : t < σ.length) (hagree : agreeWithFIF e C₀ σ t) (hdis : schedCache e C₀ σ (t + 1) ≠ schedCache (fifoSchedule σ C₀) C₀ σ (t + 1)) (hqin : e t ∈ schedCache e C₀ σ t) (Variable name `hq'` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hq' : q' = fifoSchedule σ C₀ t) (hq : q = e t) {j : ℕ} (hj : nextUse σ (t + 1) q = some j) {j' : ℕ} (hj' : nextUse σ (t + 1) q' = some j') (hjj' : j < j') (s : ℕ) (ih : t < s → s ≤ t + 1 + j → schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s = insert q ((schedCache e C₀ σ s).erase q') ∨ schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s = (schedCache e C₀ σ s).erase q') (hts : t < s) (hsJ : s + 1 ≤ t + 1 + j) : schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ (s + 1) = insert q ((schedCache e C₀ σ (s + 1)).erase q') ∨ schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ (s + 1) = (schedCache e C₀ σ (s + 1)).erase q' := by have hsJ' : s < t + 1 + j := by omega have hsig_ne_q : σ.getD s 0 ≠ q := getD_ne_nextUse (k := s) hj (by omega) hsJ' have hsig_ne_q' : σ.getD s 0 ≠ q' := getD_ne_nextUse (k := s) hj' (by omega) (by omega) have hds : repairSchedule e t q' (t + 1 + j') s = e s := by unfold repairSchedule simp [show s ≠ t by omega, show s ≠ t + 1 + j' by omega] change (if σ.getD s 0 ∈ schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s then schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s else insert (σ.getD s 0) ((schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s).erase (repairSchedule e t q' (t + 1 + j') s))) = insert q ((if σ.getD s 0 ∈ schedCache e C₀ σ s then schedCache e C₀ σ s else insert (σ.getD s 0) ((schedCache e C₀ σ s).erase (e s))).erase q') ∨ schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ (s + 1) = (schedCache e C₀ σ (s + 1)).erase q' rw [hds] rcases ih hts (by omega) with hrel1 | hrel2 · -- relation 1: Ê(s) = insert q (E(s) − q') by_cases hes : e s = q · -- e s = q: on a hit relation 1 is preserved, on a fault it switches to relation 2 by_cases hr : σ.getD s 0 ∈ schedCache e C₀ σ s · -- σ[s] ∈ E: both hit, relation 1 preserved have hrE : σ.getD s 0 ∈ insert q ((schedCache e C₀ σ s).erase q') := by rw [Finset.mem_insert] right rw [Finset.mem_erase] constructor · exact hsig_ne_q' · exact hr left rw [hrel1] rw [hes] rw [if_pos hrE] rw [if_pos hr] · -- fault: relation 2 have hrE : σ.getD s 0 ∉ insert q ((schedCache e C₀ σ s).erase q') := by intro hm rcases Finset.mem_insert.mp hm with hqeq | hmem · exact hsig_ne_q hqeq · exact hr (Finset.mem_erase.mp hmem).2 have hqnotE : q ∉ schedCache e C₀ σ s := swap_q_not_mem e σ C₀ hq.symm (by rw [hq]; exact hqin) (by intro hft have hFt : σ.getD t 0 ∈ schedCache (fifoSchedule σ C₀) C₀ σ t := by rw [← hagree t le_rfl] exact hft have hD : schedCache e C₀ σ (t + 1) = schedCache e C₀ σ t := by rw [schedCache] rw [if_pos hft] have hF : schedCache (fifoSchedule σ C₀) C₀ σ (t + 1) = schedCache (fifoSchedule σ C₀) C₀ σ t := by rw [schedCache] rw [if_pos hFt] exact hdis ((hD.trans (hagree t le_rfl)).trans hF.symm)) hj (by omega) (by omega) have hqnotE' : q ∉ (schedCache e C₀ σ s).erase q' := by intro hm exact hqnotE (Finset.mem_erase.mp hm).2 right rw [schedCache] rw [hrel1] rw [hds] rw [hes] rw [if_neg hrE] rw [Finset.erase_insert hqnotE'] rw [show schedCache e C₀ σ (s + 1) = if σ.getD s 0 ∈ schedCache e C₀ σ s then schedCache e C₀ σ s else insert (σ.getD s 0) ((schedCache e C₀ σ s).erase (e s)) by rw [schedCache]] rw [hes] rw [if_neg hr] rw [Finset.erase_eq_of_notMem hqnotE] rw [Finset.erase_insert_of_ne hsig_ne_q'] · -- e s ≠ q: relation 1 preserved left rw [hrel1] by_cases hr : σ.getD s 0 ∈ schedCache e C₀ σ s · -- both hit have hr' : σ.getD s 0 ∈ insert q ((schedCache e C₀ σ s).erase q') := by rw [Finset.mem_insert] right rw [Finset.mem_erase] constructor · exact hsig_ne_q' · exact hr rw [if_pos hr, if_pos hr'] · -- both fault rw [if_neg hr] have hr' : σ.getD s 0 ∉ insert q ((schedCache e C₀ σ s).erase q') := by intro hm rcases Finset.mem_insert.mp hm with hqeq | hmem · exact hsig_ne_q hqeq · exact hr (Finset.mem_erase.mp hmem).2 rw [if_neg hr'] rw [Finset.erase_insert_of_ne hsig_ne_q'] have hqne_es : q ≠ e s := Ne.symm hes rw [show (insert q ((schedCache e C₀ σ s).erase q')).erase (e s) = insert q (((schedCache e C₀ σ s).erase q').erase (e s)) from Finset.erase_insert_of_ne hqne_es] rw [Finset.insert_comm] have herase_comm : ((schedCache e C₀ σ s).erase q').erase (e s) = ((schedCache e C₀ σ s).erase (e s)).erase q' := by ext x simp [Finset.mem_erase, and_left_comm, This simp argument is unused: and_assoc Hint: Omit it from the simp argument list. simp [Finset.mem_erase, and_left_comm,̵ ̵a̵n̵d̵_̵a̵s̵s̵o̵c̵] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`and_assoc] rw [herase_comm] · -- relation 2: Ê(s) = E(s) − q' (B1-style), preserved right rw [schedCache] rw [hrel2] rw [hds] rw [show schedCache e C₀ σ (s + 1) = if σ.getD s 0 ∈ schedCache e C₀ σ s then schedCache e C₀ σ s else insert (σ.getD s 0) ((schedCache e C₀ σ s).erase (e s)) by rw [schedCache]] by_cases hr : σ.getD s 0 ∈ schedCache e C₀ σ s · -- both hit have hr' : σ.getD s 0 ∈ (schedCache e C₀ σ s).erase q' := by rw [Finset.mem_erase] constructor · exact hsig_ne_q' · exact hr rw [if_pos hr, if_pos hr'] · -- both fault rw [if_neg hr] have hr' : σ.getD s 0 ∉ (schedCache e C₀ σ s).erase q' := by intro hm exact hr (Finset.mem_erase.mp hm).2 rw [if_neg hr'] rw [Finset.erase_insert_of_ne hsig_ne_q'] have herase_comm : ((schedCache e C₀ σ s).erase q').erase (e s) = ((schedCache e C₀ σ s).erase (e s)).erase q' := by ext x simp [Finset.mem_erase, and_left_comm, This simp argument is unused: and_assoc Hint: Omit it from the simp argument list. simp [Finset.mem_erase, and_left_comm,̵ ̵a̵n̵d̵_̵a̵s̵s̵o̵c̵] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`and_assoc] rw [herase_comm]

The B2 window (disjunctive): when q = e t is resident, repair's cache within (t, J] is either insert q (E − q') (swap relation) or E − q' (B1-style relation, after e evicts q).

lemma repairSchedule_window_swap' (e : ℕ → Page) (σ : List Page) (C₀ : Finset Page) (hC₀ : C₀.Nonempty) {t : ℕ} (ht : t < σ.length) (hagree : agreeWithFIF e C₀ σ t) (hdis : schedCache e C₀ σ (t + 1) ≠ schedCache (fifoSchedule σ C₀) C₀ σ (t + 1)) (hqin : e t ∈ schedCache e C₀ σ t) (hq' : q' = fifoSchedule σ C₀ t) (hq : q = e t) {j : ℕ} (hj : nextUse σ (t + 1) q = some j) {j' : ℕ} (hj' : nextUse σ (t + 1) q' = some j') (hjj' : j < j') {s : ℕ} (hs1 : t < s) (hs2 : s ≤ t + 1 + j) : schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s = insert q ((schedCache e C₀ σ s).erase q') ∨ schedCache (repairSchedule e t q' (t + 1 + j')) C₀ σ s = (schedCache e C₀ σ s).erase q' := by induction s with | zero => omega | succ s ih => by_cases hs_eq : s = t · subst s left exact repairSchedule_base_swap e σ C₀ hC₀ ht hagree hdis hqin hq' hq hj' · 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 Cachingend CLRS

CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.EmptyStart

Empty-start boundary for offline caching

The core eviction trace starts from a nonempty cache because every fault must name a resident page to evict. This module isolates the compulsory first miss: under the core transition semantics an empty cache becomes the singleton containing the first request, independently of the policy. Thereafter the existing exchange theorem applies unchanged. This literal-empty execution is capacity one after its first request: it cannot represent filling a capacity-k cache for k > 1.

For a capacity greater than one, the deterministic compulsory-fill phase is represented separately by compulsoryFillCost; once a nonempty resident set is handed to the eviction phase, adding the same fill cost preserves optimality. The fill cost, resident set, and remaining suffix are supplied parameters. This module does not compute them from a capacity and empty initial state, or prove that such a capacity-parametric fill execution realizes this decomposition.

namespace CLRS.Cachingopen Finset

Shift from an empty cache and from the first-page singleton agrees after request 0.

theorem cacheSeq_empty_eq_singleton_after_first (π : Policy) (p : Page) (rest : List Page) (t : Nat) : cacheSeq π ∅ (p :: rest) (t + 1) = cacheSeq π {p} (p :: rest) (t + 1) := by induction t with | zero => simp [cacheSeq, Policy.step] | succ t ih => change π.step (t + 1) (cacheSeq π ∅ (p :: rest) (t + 1)) ((p :: rest).getD (t + 1) 0) = π.step (t + 1) (cacheSeq π {p} (p :: rest) (t + 1)) ((p :: rest).getD (t + 1) 0) rw [ih]

The core literal-empty run has capacity one after the first request.

theorem cacheSeq_empty_card_one_after_first (π : Policy) (p : Page) (rest : List Page) (t : Nat) : (cacheSeq π ∅ (p :: rest) (t + 1)).card = 1 := by rw [cacheSeq_empty_eq_singleton_after_first] rw [cacheSeq_card π {p} (p :: rest) (t + 1) (by simp)] simp
theorem faultAt_empty_zero (π : Policy) (p : Page) (rest : List Page) : faultAt π ∅ (p :: rest) 0 = 1 := by simp [faultAt, cacheSeq]theorem faultAt_singleton_zero (π : Policy) (p : Page) (rest : List Page) : faultAt π {p} (p :: rest) 0 = 0 := by simp [faultAt, cacheSeq] theorem faultAt_empty_eq_singleton_succ (π : Policy) (p : Page) (rest : List Page) (t : Nat) : faultAt π ∅ (p :: rest) (t + 1) = faultAt π {p} (p :: rest) (t + 1) := by unfold faultAt rw [cacheSeq_empty_eq_singleton_after_first]

Every policy pays exactly one additional compulsory miss when starting empty.

theorem misses_empty_eq_singleton_add_one (π : Policy) (p : Page) (rest : List Page) : misses π ∅ (p :: rest) = misses π {p} (p :: rest) + 1 := by have hempty : misses π ∅ (p :: rest) = 1 + ∑ t ∈ Finset.range rest.length, faultAt π ∅ (p :: rest) (t + 1) := by unfold misses rw [show (p :: rest).length = rest.length + 1 by simp, sum_range_shift] rw [faultAt_empty_zero] have hsingleton : misses π {p} (p :: rest) = ∑ t ∈ Finset.range rest.length, faultAt π {p} (p :: rest) (t + 1) := by unfold misses rw [show (p :: rest).length = rest.length + 1 by simp, sum_range_shift] rw [faultAt_singleton_zero, zero_add] rw [hempty, hsingleton] have hsum : (∑ t ∈ Finset.range rest.length, faultAt π ∅ (p :: rest) (t + 1)) = ∑ t ∈ Finset.range rest.length, faultAt π {p} (p :: rest) (t + 1) := by apply Finset.sum_congr rfl intro t _ exact faultAt_empty_eq_singleton_succ π p rest t rw [hsum, Nat.add_comm]

Farthest-in-future is optimal from the literal empty cache in the core transition semantics of capacity one after the first load; the empty request list and the compulsory first miss are both covered. This is not an arbitrary capacity empty-start execution theorem.

theorem fifo_optimal_from_empty (π : Policy) (σ : List Page) : misses (fifoPolicy σ) ∅ σ ≤ misses π ∅ σ := by cases σ with | nil => simp [misses] | cons p rest => rw [misses_empty_eq_singleton_add_one (fifoPolicy (p :: rest)) p rest, misses_empty_eq_singleton_add_one π p rest] exact Nat.add_le_add_right (fifo_optimal π {p} (p :: rest) (by simp)) 1

Cost decomposition after a policy-independent compulsory-fill phase.

def compulsoryFillCost (fillMisses : Nat) (π : Policy) (resident : Finset Page) (remaining : List Page) : Nat := fillMisses + misses π resident remaining

Adding a common compulsory-fill cost does not change the optimal eviction policy for the remaining requests. This is the capacity-independent bridge for supplied fill data. It does not establish that a capacity-parametric empty-start algorithm produces those data.

theorem fifo_optimal_after_compulsory_fill (fillMisses : Nat) (π : Policy) (resident : Finset Page) (remaining : List Page) (hresident : resident.Nonempty) : compulsoryFillCost fillMisses (fifoPolicy remaining) resident remaining ≤ compulsoryFillCost fillMisses π resident remaining := by unfold compulsoryFillCost exact Nat.add_le_add_left (fifo_optimal π resident remaining hresident) fillMisses
end CLRS.Caching

CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A1_LegalTrace

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 farthest-in-future optimality.

namespace CLRSopen Finsetopen scoped BigOperatorsnamespace 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 Cachingend CLRS

CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A2_OnePageDiff

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.

namespace CLRSopen Finsetnamespace 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 OnePageDifflemma left_mem (h : OnePageDiff A B a b) : a ∈ A := h.1lemma left_not_mem_right (h : OnePageDiff A B a b) : a ∉ B := h.2.1lemma right_not_mem_left (h : OnePageDiff A B a b) : b ∉ A := h.2.2.1lemma right_mem (h : OnePageDiff A B a b) : b ∈ B := h.2.2.2.1lemma 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

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, 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]

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) : 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

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 OnePageDiffend Cachingend CLRS

CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A3_CouplingCore

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.

namespace CLRSopen Finsetnamespace 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 Cachingend CLRS

CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A4_CouplingCorrect

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.

namespace CLRSopen Finsetopen scoped BigOperatorsnamespace 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 rfllemma 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_leftlemma 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 Cachingend CLRS

CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A5_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 misses.

namespace CLRSopen Finsetnamespace 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 Cachingend CLRS

CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Optimality.Trace.A6_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.

namespace CLRSopen Finsetopen scoped BigOperatorsnamespace 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 Cachingend CLRS