-- File: lean/LruSpec.lean
-- LRU Cache Specification
-- Agents migrate a C++ LRU (std::list + unordered_map) to Rust Vec<(u64,u64)>.
-- Representation: List (Nat × Nat), head = MRU (most recently used).

namespace LruSpec

abbrev CacheState := List (Nat × Nat)   -- (key, value), head = MRU

-- Trim to capacity (keep MRU end)
def lruEvict (cache : CacheState) (cap : Nat) : CacheState :=
  cache.take cap

-- Insert/update key-val at MRU position; evict LRU tail if over capacity
def lruPut (cache : CacheState) (cap : Nat) (key val : Nat) : CacheState :=
  ((key, val) :: cache.filter (fun p => p.1 ≠ key)).take cap

-- Look up key; move to front (MRU) on hit
def lruGet (cache : CacheState) (key : Nat) : Option Nat × CacheState :=
  match cache.find? (fun p => p.1 == key) with
  | none => (none, cache)
  | some (_, v) =>
    let newCache := (key, v) :: cache.filter (fun p => p.1 ≠ key)
    (some v, newCache)

-- lruPut never exceeds capacity
theorem lruPut_bounded (cache : CacheState) (cap key val : Nat) :
    (lruPut cache cap key val).length ≤ cap := by
  simp only [lruPut]
  exact List.length_take_le cap _

-- DRT checks
example : lruPut [(1, 10), (2, 20)] 2 1 99 = [(1, 99), (2, 20)] := by native_decide
example : lruPut [(1, 10), (2, 20)] 2 3 30 = [(3, 30), (1, 10)] := by native_decide
example : lruEvict [(1, 10), (2, 20), (3, 30)] 2 = [(1, 10), (2, 20)] := by native_decide
example : lruGet [(1, 10), (2, 20), (3, 30)] 2 =
    (some 20, [(2, 20), (1, 10), (3, 30)]) := by native_decide
example : lruGet [(1, 10)] 2 = (none, [(1, 10)]) := by native_decide

end LruSpec