Least-recently-used cache

26 fully proved

LRU cache

StructureLeast-recently-used cache#✓fully proved

For a type \(K\) of keys, a type \(V\) of values and a natural number \(c\), an LRU cache of capacity \(c\) is a list of key-value pairs in \(K \times V\), ordered from most to least recently used, whose keys are pairwise distinct and whose length is at most \(c\).

public structure LruCache (K : Type u) (V : Type v) (cap : Nat) where
  /-- The stored key-value pairs, most recently used first. -/
  entries : List (K × V)
  /-- Keys are pairwise distinct. -/
  nodup_keys : (entries.map Prod.fst).Nodup
  /-- The cache holds at most `cap` entries. -/
  length_le : entries.length ≤ cap

Used by 24

Used byEmpty LRU cache · The evicted key is the least recently used one · Extensionality of LRU caches · LRU cache lookup · A lookup of a stored key returns its value · Lookups keep keys distinct · A lookup of an absent key misses · A lookup permutes the entries · A successful lookup moves the entry to the front · Lookup after insertion into an LRU cache · A put without eviction preserves lookups of other keys · Lookup preserves the size · Lookup respects the capacity · Key list of an LRU cache · Keys of an LRU cache are distinct · Lookup preserves the stored bindings · Entries after insertion · Insertion without eviction · Insertion into an LRU cache · With positive capacity, the inserted binding becomes the most recent entry · Insertion keeps the keys of an LRU cache distinct · Insertion respects the capacity of an LRU cache · Size of an LRU cache · An LRU cache never exceeds its capacity

TheoremExtensionality of LRU caches#✓fully proved

Two LRU caches with the same key type, value type and capacity are equal if their lists of entries are equal.

@[ext]
theorem ext {K : Type u} {V : Type v} {cap : Nat} {a b : LruCache K V cap}
    (h : a.entries = b.entries) : a = b

Uses 1

Statement usesLeast-recently-used cache

DefinitionErasing a key from a list of entries#✓fully proved

Given a key \(k\) and a list of key–value pairs, erasing \(k\) deletes every pair whose key is \(k\) and keeps the other pairs in their original order. When the keys in the list are pairwise distinct, at most one pair is deleted.

def eraseKey {K : Type u} {V : Type v} [DecidableEq K] (k : K)
    (entries : List (K × V)) : List (K × V) :=
  entries.filter fun p => decide (p.1 ≠ k)

Used by 11

Used byThe evicted key is the least recently used one · LRU cache lookup · A lookup of a stored key returns its value · A lookup of an absent key misses · A lookup permutes the entries · A successful lookup moves the entry to the front · Lookup after insertion into an LRU cache · Lookup preserves the stored bindings · Entries after insertion · Insertion without eviction · Insertion into an LRU cache

DefinitionEmpty LRU cache#✓fully proved

For every capacity \(c\), the empty LRU cache of capacity \(c\) is the cache with no entries.

public def empty {K : Type u} {V : Type v} {cap : Nat} : LruCache K V cap where
  entries := []
  nodup_keys := by simp
  length_le := Nat.zero_le cap

Uses 1

Statement usesLeast-recently-used cache

DefinitionKey list of an LRU cache#✓fully proved

The key list of an LRU cache is the list of the keys of its entries in the order of the cache, so the most recently used key comes first.

public def keys {K : Type u} {V : Type v} {cap : Nat} (cache : LruCache K V cap) : List K :=
  cache.entries.map Prod.fst

Uses 1 · Used by 7

Statement usesLeast-recently-used cache

Used byThe evicted key is the least recently used one · Lookups keep keys distinct · A lookup of an absent key misses · A put without eviction preserves lookups of other keys · Keys of an LRU cache are distinct · Insertion without eviction · Insertion keeps the keys of an LRU cache distinct

DefinitionSize of an LRU cache#✓fully proved

The size of an LRU cache is the number of entries it stores.

public def size {K : Type u} {V : Type v} {cap : Nat} (cache : LruCache K V cap) : Nat :=
  cache.entries.length

Uses 1 · Used by 7

Statement usesLeast-recently-used cache

Used byThe evicted key is the least recently used one · A put without eviction preserves lookups of other keys · Lookup preserves the size · Lookup respects the capacity · Insertion without eviction · Insertion respects the capacity of an LRU cache · An LRU cache never exceeds its capacity

DefinitionLRU cache lookup#✓fully proved

Looking up a key \(k\) in an LRU cache returns an optional value together with a cache. If the cache stores a binding \((k, v)\), the result is \(v\) together with the cache in which that binding is moved to the front and the other entries keep their order; otherwise the result is no value together with the unchanged cache.

Cslib.Algorithms.Lean.LruCache.get · 18 lines

public def get {K : Type u} {V : Type v} {cap : Nat} [DecidableEq K]
    (cache : LruCache K V cap) (k : K) : Option V × LruCache K V cap :=
  match hf : cache.entries.find? (fun q => decide (q.1 = k)) with
  | some p =>
      (some p.2,
        ⟨p :: eraseKey k cache.entries,
         nodup_keys_cons_eraseKey cache.nodup_keys (fst_of_find?_eq_some hf),
         by
           have hmem : (k, p.2) ∈ cache.entries := by
             have hp : (k, p.2) = p :=
               Prod.ext (fst_of_find?_eq_some hf).symm rfl
             rw [hp]
             exact List.mem_of_find?_eq_some hf
           have hlen := length_eraseKey_add_one hmem cache.nodup_keys
           have hle := cache.length_le
           simp only [List.length_cons]
           omega⟩)
  | none => (none, cache)

Uses 2 · Used by 10

Statement usesLeast-recently-used cache · Erasing a key from a list of entries

Used byA lookup of a stored key returns its value · Lookups keep keys distinct · A lookup of an absent key misses · A lookup permutes the entries · A successful lookup moves the entry to the front · Lookup after insertion into an LRU cache · A put without eviction preserves lookups of other keys · Lookup preserves the size · Lookup respects the capacity · Lookup preserves the stored bindings

DefinitionInsertion into an LRU cache#✓fully proved

Putting the binding \((k, v)\) into an LRU cache of capacity \(c\) removes any entry with key \(k\), places \((k, v)\) at the front as the most recently used entry, and then keeps only the first \(c\) entries, so the least recently used entries beyond the capacity are evicted.

public def put {K : Type u} {V : Type v} {cap : Nat} [DecidableEq K]
    (cache : LruCache K V cap) (k : K) (v : V) : LruCache K V cap where
  entries := ((k, v) :: eraseKey k cache.entries).take cap
  nodup_keys := by
    rw [List.map_take]
    exact (nodup_keys_cons_eraseKey cache.nodup_keys rfl).sublist
      (List.take_sublist cap _)
  length_le := by
    rw [List.length_take]
    exact Nat.min_le_left cap _

Uses 2 · Used by 8

Statement usesLeast-recently-used cache · Erasing a key from a list of entries

Used byThe evicted key is the least recently used one · Lookup after insertion into an LRU cache · A put without eviction preserves lookups of other keys · Entries after insertion · Insertion without eviction · With positive capacity, the inserted binding becomes the most recent entry · Insertion keeps the keys of an LRU cache distinct · Insertion respects the capacity of an LRU cache

TheoremKeys of an LRU cache are distinct#✓fully proved

The keys stored in any LRU cache are pairwise distinct.

public theorem keys_nodup {K : Type u} {V : Type v} {cap : Nat} (cache : LruCache K V cap) :
    cache.keys.Nodup

Uses 2 · Used by 2

Statement usesLeast-recently-used cache · Key list of an LRU cache

Used byLookups keep keys distinct · Insertion keeps the keys of an LRU cache distinct

TheoremAn LRU cache never exceeds its capacity#✓fully proved

Every LRU cache of capacity \(c\) has size at most \(c\).

public theorem size_le_cap {K : Type u} {V : Type v} {cap : Nat} (cache : LruCache K V cap) :
    cache.size ≤ cap

Uses 2 · Used by 2

Statement usesLeast-recently-used cache · Size of an LRU cache

Used byLookup respects the capacity · Insertion respects the capacity of an LRU cache

TheoremA lookup of an absent key misses#✓fully proved

If the key \(k\) is not stored in an LRU cache, then looking up \(k\) returns no value and leaves the cache unchanged.

public theorem get_miss {K : Type u} {V : Type v} {cap : Nat} [DecidableEq K]
    {cache : LruCache K V cap} {k : K} (hk : k ∉ cache.keys) :
    (cache.get k).1 = none ∧ (cache.get k).2 = cache

Uses 4 · Used by 1

Statement usesLeast-recently-used cache · LRU cache lookup · Key list of an LRU cache

Proof usesErasing a key from a list of entries

Used byA put without eviction preserves lookups of other keys

TheoremA lookup of a stored key returns its value#✓fully proved

If an LRU cache stores the pair \((k, v)\), then looking up \(k\) returns \(v\).

public theorem get_hit {K : Type u} {V : Type v} {cap : Nat} [DecidableEq K]
    {cache : LruCache K V cap} {k : K} {v : V} (hmem : (k, v) ∈ cache.entries) :
    (cache.get k).1 = some v

Uses 3 · Used by 2

Statement usesLeast-recently-used cache · LRU cache lookup

Proof usesErasing a key from a list of entries

Used byLookup after insertion into an LRU cache · A put without eviction preserves lookups of other keys

TheoremA successful lookup moves the entry to the front#✓fully proved

If an LRU cache stores the pair \((k, v)\), then after looking up \(k\) the most recently used (first) entry of the cache is \((k, v)\).

public theorem get_promotes {K : Type u} {V : Type v} {cap : Nat} [DecidableEq K]
    {cache : LruCache K V cap} {k : K} {v : V} (hmem : (k, v) ∈ cache.entries) :
    (cache.get k).2.entries.head? = some (k, v)

Uses 3

Statement usesLeast-recently-used cache · LRU cache lookup

Proof usesErasing a key from a list of entries

TheoremLookup after insertion into an LRU cache#✓fully proved

For every LRU cache of positive capacity, every key \(k\) and every value \(v\), looking up \(k\) in the cache obtained by putting the binding \((k, v)\) returns \(v\).

public theorem get_put {K : Type u} {V : Type v} {cap : Nat} [DecidableEq K]
    (cache : LruCache K V cap) (k : K) (v : V) (hcap : 0 < cap) :
    ((cache.put k v).get k).1 = some v

Uses 5

Statement usesLeast-recently-used cache · LRU cache lookup · Insertion into an LRU cache

Proof usesErasing a key from a list of entries · A lookup of a stored key returns its value

TheoremInsertion respects the capacity of an LRU cache#✓fully proved

For every LRU cache \(C\) of capacity \(c\), key \(k\) and value \(v\), the cache obtained by putting the binding \((k, v)\) into \(C\) has size at most \(c\).

public theorem put_size_le {K : Type u} {V : Type v} {cap : Nat} [DecidableEq K]
    (cache : LruCache K V cap) (k : K) (v : V) : (cache.put k v).size ≤ cap

Uses 4

Statement usesLeast-recently-used cache · Insertion into an LRU cache · Size of an LRU cache

Proof usesAn LRU cache never exceeds its capacity

TheoremInsertion keeps the keys of an LRU cache distinct#✓fully proved

For every LRU cache \(C\), key \(k\) and value \(v\), the keys of the cache obtained by putting the binding \((k, v)\) into \(C\) are pairwise distinct.

public theorem put_keys_nodup {K : Type u} {V : Type v} {cap : Nat} [DecidableEq K]
    (cache : LruCache K V cap) (k : K) (v : V) : (cache.put k v).keys.Nodup

Uses 4

Statement usesLeast-recently-used cache · Key list of an LRU cache · Insertion into an LRU cache

Proof usesKeys of an LRU cache are distinct

TheoremLookup respects the capacity#✓fully proved

For every LRU cache of capacity \(c\) and every key \(k\), the cache after looking up \(k\) holds at most \(c\) entries.

public theorem get_size_le {K : Type u} {V : Type v} {cap : Nat} [DecidableEq K]
    (cache : LruCache K V cap) (k : K) : (cache.get k).2.size ≤ cap

Uses 4

Statement usesLeast-recently-used cache · LRU cache lookup · Size of an LRU cache

Proof usesAn LRU cache never exceeds its capacity

TheoremLookups keep keys distinct#✓fully proved

For every LRU cache and every key \(k\), the keys of the cache obtained by looking up \(k\) are pairwise distinct.

public theorem get_keys_nodup {K : Type u} {V : Type v} {cap : Nat} [DecidableEq K]
    (cache : LruCache K V cap) (k : K) : (cache.get k).2.keys.Nodup

Uses 4

Statement usesLeast-recently-used cache · LRU cache lookup · Key list of an LRU cache

Proof usesKeys of an LRU cache are distinct

TheoremEntries after insertion#✓fully proved

For every LRU cache, key \(k\) and value \(v\), every key-value pair \(p\) stored in the cache after putting the binding \((k, v)\) either equals \((k, v)\), or was stored before and has a key different from \(k\).

public theorem mem_put_entries {K : Type u} {V : Type v} {cap : Nat} [DecidableEq K]
    {cache : LruCache K V cap} {k : K} {v : V} {p : K × V}
    (hp : p ∈ (cache.put k v).entries) :
    p = (k, v) ∨ (p ∈ cache.entries ∧ p.1 ≠ k)

Uses 3

Statement usesLeast-recently-used cache · Insertion into an LRU cache

Proof usesErasing a key from a list of entries

TheoremLookup preserves the stored bindings#✓fully proved

For every LRU cache and every key \(k\), a key-value pair is stored in the cache after looking up \(k\) if and only if it was stored in the cache before the lookup.

public theorem mem_get_entries_iff {K : Type u} {V : Type v} {cap : Nat} [DecidableEq K]
    (cache : LruCache K V cap) (k : K) (p : K × V) :
    p ∈ (cache.get k).2.entries ↔ p ∈ cache.entries

Uses 3

Statement usesLeast-recently-used cache · LRU cache lookup

Proof usesErasing a key from a list of entries

TheoremA lookup permutes the entries#✓fully proved

For every LRU cache and every key \(k\), the list of entries of the cache after looking up \(k\) is a permutation of the list of entries before.

public theorem get_perm {K : Type u} {V : Type v} {cap : Nat} [DecidableEq K]
    (cache : LruCache K V cap) (k : K) :
    (cache.get k).2.entries.Perm cache.entries

Uses 3 · Used by 1

Statement usesLeast-recently-used cache · LRU cache lookup

Proof usesErasing a key from a list of entries

Used byLookup preserves the size

TheoremLookup preserves the size#✓fully proved

For every LRU cache and every key \(k\), the cache after looking up \(k\) holds exactly as many entries as before.

public theorem get_size {K : Type u} {V : Type v} {cap : Nat} [DecidableEq K]
    (cache : LruCache K V cap) (k : K) :
    (cache.get k).2.size = cache.size

Uses 4

Statement usesLeast-recently-used cache · LRU cache lookup · Size of an LRU cache

Proof usesA lookup permutes the entries

TheoremInsertion without eviction#✓fully proved

Let an LRU cache of capacity \(c\) hold fewer than \(c\) entries or already store a binding for the key \(k\), and let \(v\) be a value. Then a key-value pair \(p\) is stored in the cache after putting the binding \((k, v)\) if and only if \(p = (k, v)\), or \(p\) was stored before and the key of \(p\) differs from \(k\).

public theorem mem_put_entries_iff_of_not_full {K : Type u} {V : Type v} {cap : Nat}
    [DecidableEq K] {cache : LruCache K V cap} {k : K} {v : V} {p : K × V}
    (hroom : cache.size < cap ∨ k ∈ cache.keys) :
    p ∈ (cache.put k v).entries ↔ p = (k, v) ∨ (p ∈ cache.entries ∧ p.1 ≠ k)

Uses 5 · Used by 1

Statement usesLeast-recently-used cache · Key list of an LRU cache · Insertion into an LRU cache · Size of an LRU cache

Proof usesErasing a key from a list of entries

Used byA put without eviction preserves lookups of other keys

TheoremWith positive capacity, the inserted binding becomes the most recent entry#✓fully proved

Let \(C\) be an LRU cache of positive capacity, \(k\) a key and \(v\) a value. After the binding \((k, v)\) is put into \(C\), the first entry of the resulting cache, its most recently used entry, is \((k, v)\).

public theorem put_head? {K : Type u} {V : Type v} {cap : Nat} [DecidableEq K]
    (cache : LruCache K V cap) (k : K) (v : V) (hcap : 0 < cap) :
    (cache.put k v).entries.head? = some (k, v)

Uses 2

Statement usesLeast-recently-used cache · Insertion into an LRU cache

TheoremA put without eviction preserves lookups of other keys#✓fully proved

Let \(C\) be an LRU cache of capacity \(c\) that holds fewer than \(c\) entries or already stores the key \(k\). Then for every key \(k' \ne k\) and every value \(v\), looking up \(k'\) in the cache obtained by putting the binding \((k, v)\) into \(C\) returns the same optional value as looking up \(k'\) in \(C\).

public theorem get_put_of_ne {K : Type u} {V : Type v} {cap : Nat} [DecidableEq K]
    {cache : LruCache K V cap} {k k' : K} {v : V} (hne : k' ≠ k)
    (hroom : cache.size < cap ∨ k ∈ cache.keys) :
    ((cache.put k v).get k').1 = (cache.get k').1

Uses 8

Statement usesLeast-recently-used cache · LRU cache lookup · Key list of an LRU cache · Insertion into an LRU cache · Size of an LRU cache

Proof usesA lookup of a stored key returns its value · A lookup of an absent key misses · Insertion without eviction

TheoremThe evicted key is the least recently used one#✓fully proved

Let \(C\) be an LRU cache of capacity \(c\), let \(k'\) be a key not stored in \(C\), and let \(k\) be a key stored in \(C\). If \(k\) is no longer stored after putting \(k'\) with any value \(v\) into \(C\), then \(C\) held exactly \(c\) entries and \(k\) is the last key of \(C\), that is, the least recently used one.

public theorem evicted_is_least_recent {K : Type u} {V : Type v} {cap : Nat} [DecidableEq K]
    {cache : LruCache K V cap} {k k' : K} {v : V}
    (hnew : k' ∉ cache.keys) (hk : k ∈ cache.keys)
    (hevicted : k ∉ (cache.put k' v).keys) :
    cache.keys.getLast? = some k ∧ cache.size = cap

Uses 5

Statement usesLeast-recently-used cache · Key list of an LRU cache · Insertion into an LRU cache · Size of an LRU cache

Proof usesErasing a key from a list of entries

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.