SilverSight/formal/SilverSight/CacheSieve.lean

/-
  CacheSieve.lean — L0 Local Sorter Cache Admission Control

  Static cache filtering: decides which cache lines to admit based on
  a 4-state machine. Pairs with HCMR for the complete cache performance
  model (admission + contention).

  Clean rewrite for SilverSight — not a port from Research Stack.
  Based on the chiral CRT multiplexing framework.

  States:
  - Stable:  line is cached, low access frequency, keep
  - Rising:  line is being promoted (frequency increasing)
  - Unstable: line is hot but contended (may thrash)
  - Reset:   line evicted, must re-fetch

  Admission policy:
  - Stable → Rising on access
  - Rising → Unstable if contention detected (HCMR self-loop high)
  - Unstable → Reset if contention persists (COUCH gate fails)
  - Reset → Rising on re-access (re-admission)

  Connection to CRT multiplexer:
  - CacheSieve decides WHICH channels to admit (admission control)
  - HCMR models CONTENTION on admitted channels (throughput)
  - Together: complete cache performance model
-/

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

namespace SilverSight.CacheSieve

/-- Sieve state: the 4-state machine for cache admission. -/
inductive SieveState where
  | stable   : SieveState   -- cached, low frequency, keep
  | rising   : SieveState   -- being promoted (frequency increasing)
  | unstable : SieveState   -- hot but contended (may thrash)
  | reset    : SieveState   -- evicted, must re-fetch
  deriving Repr, DecidableEq

/-- Cache line with sieve state and access count. -/
structure CacheLine where
  addr       : ℕ            -- cache line address
  state      : SieveState
  accessCount : ℕ           -- number of accesses since admission
  deriving Repr

/-- The sieve: a collection of cache lines with a capacity. -/
structure CacheSieve where
  lines     : List CacheLine
  capacity  : ℕ             -- max lines the cache can hold
  deriving Repr

/-- Access outcome: did the access hit, miss, or promote/demote? -/
inductive AccessResult where
  | hit      : AccessResult   -- line was stable/rising, access succeeded
  | miss     : AccessResult   -- line was reset/absent, must fetch
  | promote  : AccessResult   -- line promoted (stable→rising or reset→rising)
  | demote   : AccessResult   -- line demoted (rising→unstable or unstable→reset)
  deriving Repr

/-- Contention level from HCMR (self-loop probability as Q16_16 raw). -/
-- 0 = no contention, 65536 = fully contended
def ContentionThreshold : ℕ := 49152  -- 0.75 × 65536 — high contention cutoff

/-- Transition: given current state, access count, and contention, what's next?

    - Stable + access → Rising (promote)
    - Rising + low contention → Rising (stay, accumulating heat)
    - Rising + high contention → Unstable (demote)
    - Unstable + high contention → Reset (evict)
    - Unstable + low contention → Rising (recover)
    - Reset + access → Rising (re-admit)
-/
def sieveTransition (s : SieveState) (accessCount : ℕ) (contention : ℕ) : SieveState × AccessResult :=
  match s with
  | .stable =>
    (.rising, .promote)
  | .rising =>
    if contention ≥ ContentionThreshold then
      (.unstable, .demote)
    else
      (.rising, .hit)
  | .unstable =>
    if contention ≥ ContentionThreshold then
      (.reset, .demote)
    else
      (.rising, .promote)
  | .reset =>
    (.rising, .promote)

/-- Check if a cache line should be admitted (admission control).

    A line is admitted if:
    - There's capacity available (new line), OR
    - An existing line is already present (re-admit / keep — always true).

    Note: both existing-line cases (Reset re-admit and Stable/Rising keep)
    return `true`, so the existing-line branch collapses to a constant. -/
def shouldAdmit (sieve : CacheSieve) (addr : ℕ) : Bool :=
  if (sieve.lines.filter (fun l => l.addr == addr)).isEmpty then
    -- New line: admit if active (non-Reset) line count is under capacity.
    (sieve.lines.filter (fun l => l.state ≠ .reset)).length < sieve.capacity
  else
    -- Line already present: keep or re-admit.
    true

/-- Evict a line to make room (victim selection: oldest Unstable or Reset). -/
def evictVictim (sieve : CacheSieve) : Option ℕ :=
  -- Prefer evicting Reset lines, then Unstable
  let resetLines := sieve.lines.filterMap (fun l =>
    if l.state == .reset then some l.addr else none)
  match resetLines.head? with
  | some addr => some addr
  | none =>
    let unstableLines := sieve.lines.filterMap (fun l =>
      if l.state == .unstable then some l.addr else none)
    unstableLines.head?

-- ── Theorems ──────────────────────────────────────────────────────────

/-- A stable line with an access transitions to Rising (promotion). -/
theorem stable_access_promotes :
    sieveTransition .stable 0 0 = (.rising, .promote) := rfl

/-- A rising line with low contention stays Rising (hit). -/
theorem rising_low_contention_hits :
    sieveTransition .rising 5 0 = (.rising, .hit) := by
  simp [sieveTransition, ContentionThreshold]

/-- A rising line with high contention transitions to Unstable (demote). -/
theorem rising_high_contention_demotes :
    sieveTransition .rising 5 65536 = (.unstable, .demote) := by
  simp [sieveTransition, ContentionThreshold]

/-- An unstable line with persistent contention transitions to Reset (evict). -/
theorem unstable_high_contention_resets :
    sieveTransition .unstable 10 65536 = (.reset, .demote) := by
  simp [sieveTransition, ContentionThreshold]

/-- A reset line with re-access transitions to Rising (re-admission). -/
theorem reset_access_readmits :
    sieveTransition .reset 0 0 = (.rising, .promote) := rfl

/-- Admission control: a new line is admitted when active capacity is available.

    The line being new (no cache line with this address) is enough to force
    the existing-line filter empty, so `shouldAdmit` reduces to the capacity
    check, which is exactly `hcap`. -/
theorem admit_when_capacity (sieve : CacheSieve)
    (hcap : (sieve.lines.filter (fun l => l.state ≠ .reset)).length < sieve.capacity)
    (addr : ℕ) (hnew : ∀ l ∈ sieve.lines, l.addr ≠ addr) :
    shouldAdmit sieve addr = true := by
  -- No cache line carries this address, so the existing-line filter is empty.
  have h_empty : (sieve.lines.filter (fun l => l.addr == addr)).isEmpty = true := by
    simp [List.isEmpty_eq_true, List.filter_eq_nil, Nat.beq_iff_eq]
    exact hnew
  simp only [shouldAdmit, h_empty, if_true, decide_eq_true_eq]
  exact hcap

/-- Eviction prefers Reset lines: if any Reset line exists, `evictVictim`
    returns an address (i.e. succeeds) rather than failing with `none`.

    This is the "prefers Reset" guarantee — when a Reset victim is
    available, eviction does not fall through to the Unstable scan. -/
theorem evict_prefers_reset (sieve : CacheSieve)
    (hreset : ∃ l ∈ sieve.lines, l.state == .reset) :
    evictVictim sieve ≠ none := by
  obtain ⟨l, hl, hlr⟩ := hreset
  -- `l` contributes `some l.addr` to the Reset filterMap, so it is nonempty.
  have hfm_mem : some l.addr ∈
      sieve.lines.filterMap (fun x => if x.state == .reset then some x.addr else none) := by
    simp [hl, hlr]
  have hfm_ne : (sieve.lines.filterMap
      (fun x => if x.state == .reset then some x.addr else none)) ≠ [] := by
    intro hnil; rw [hnil] at hfm_mem; simp at hfm_mem
  -- Split on the Reset filterMap's head; nonemptiness rules out the `none` arm.
  simp only [evictVictim]
  split
  · simp
  · rename_i h
    rw [List.head?_eq_none_iff] at h
    exact (hfm_ne h).elim

/-- COUCH gate connection: unstable→reset transition is the COUCH filter.

    When contention exceeds threshold (COUCH fails), the sieve evicts
    the line. This is the cache-level implementation of the COUCH gate
    from GCCL.lean. -/
theorem couch_evicts_on_contention :
    ∀ (accessCount : ℕ),
      sieveTransition .unstable accessCount 65536 = (.reset, .demote) := by
  intro accessCount
  simp [sieveTransition, ContentionThreshold]

end SilverSight.CacheSieve