/-
  WorkloadTestbench.lean — Virtual GPU Workload Simulation

  Workload characterization: models memory access patterns and feeds them
  into HCMR's cache contention model.

  Clean rewrite for SilverSight — not a port from Research Stack.

  Workload types:
  - Stream:    sequential memory access (low contention, good cache use)
  - Strided:   fixed-stride access (moderate contention, depends on stride)
  - Random:    random access (high contention, cache thrashing)
  - Gather:    indirect access (high contention, pointer chasing)
  - Scatter:   indirect write (highest contention, write-back thrashing)

  Each workload type produces a memory access pattern that feeds into
  HCMR's cache model, predicting the self-loop probability.

  Connection to CRT multiplexer:
  - Stream workloads = ring dispatch regime (q >> 1, low self-loop)
  - Random workloads = AVX-512 regime (q ≈ 1, high self-loop)
  - The workload type determines the q-regime, which determines throughput

  Connection to CacheSieve:
  - Workload access pattern determines sieve state transitions
  - Stream → Stable (low frequency, keep)
  - Random → Unstable → Reset (thrashing, evict)
-/

import Mathlib.Data.Real.Basic
import Mathlib.Tactic
import SilverSight.HCMR
import SilverSight.CacheSieve

namespace SilverSight.WorkloadTestbench

/-- Workload type: characterizes the memory access pattern. -/
inductive WorkloadType where
  | stream  : WorkloadType    -- sequential access (low contention)
  | strided : WorkloadType    -- fixed stride (moderate contention)
  | random  : WorkloadType    -- random access (high contention)
  | gather  : WorkloadType    -- indirect read (pointer chasing)
  | scatter : WorkloadType    -- indirect write (write-back thrashing)
  deriving Repr, DecidableEq

/-- Memory access pattern: list of addresses accessed. -/
structure AccessPattern where
  addresses : List ℕ        -- sequence of memory addresses
  workloadType : WorkloadType
  deriving Repr

/-- Workload configuration. -/
structure Workload where
  pattern      : AccessPattern
  dataSize     : ℕ           -- bytes of data accessed
  iterations   : ℕ           -- number of iterations
  deriving Repr

/-- Predicted HCMR operation type for each workload.

    Stream → ring dispatch (low contention, sequential = no collisions)
    Strided → SUBLEQ (moderate contention, stride causes partial overlap)
    Random → AVX-512 (high contention, random = many collisions)
    Gather → AVX-512 (high contention, pointer chasing)
    Scatter → AVX-512 (highest contention, write-back thrashing) -/
def workloadToOp : WorkloadType → HCMR.OISCOp
  | .stream  => .ringDispatch
  | .strided => .subleqWord
  | .random  => .clAvx512
  | .gather  => .clAvx512
  | .scatter => .clAvx512

/-- Predicted self-loop probability for a workload (Q16_16 raw). -/
def workloadSelfLoop (wt : WorkloadType) : ℕ :=
  HCMR.selfLoopProb (workloadToOp wt)

/-- Predicted throughput for a workload (Q16_16 raw). -/
def workloadThroughput (baseRate : ℕ) (wt : WorkloadType) : ℕ :=
  HCMR.throughput baseRate (workloadToOp wt)

/-- Predicted CacheSieve state for a workload.

    Stream → Stable (low frequency, good locality)
    Strided → Rising (moderate, accumulating heat)
    Random → Unstable (high contention, thrashing)
    Gather → Unstable
    Scatter → Reset (write-back thrashing, evict) -/
def workloadToSieveState : WorkloadType → CacheSieve.SieveState
  | .stream  => .stable
  | .strided => .rising
  | .random  => .unstable
  | .gather  => .unstable
  | .scatter => .reset

/-- Total memory accesses in a workload. -/
def totalAccesses (w : Workload) : ℕ :=
  w.pattern.addresses.length * w.iterations

/-- Working set size: number of distinct addresses. -/
def workingSet (w : Workload) : ℕ :=
  w.pattern.addresses.eraseDups.length

/-- Cache pressure ratio: working set / data size.

    > 1.0: working set exceeds data size (shouldn't happen)
    = 1.0: all data accessed
    < 1.0: only part of data accessed (good locality) -/
def cachePressure (w : Workload) : ℕ :=
  workingSet w * 65536 / (max w.dataSize 1)

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

/-- Stream workloads have zero self-loop (ring dispatch regime). -/
theorem stream_zero_self_loop :
    workloadSelfLoop .stream = 0 := by
  simp [workloadSelfLoop, workloadToOp, HCMR.selfLoopProb]

/-- Random workloads have the highest self-loop (AVX-512 regime). -/
theorem random_highest_self_loop :
    workloadSelfLoop .random ≥ workloadSelfLoop .stream ∧
    workloadSelfLoop .random ≥ workloadSelfLoop .strided := by
  simp [workloadSelfLoop, workloadToOp, HCMR.selfLoopProb]

/-- Stream workloads have the highest throughput. -/
theorem stream_highest_throughput (baseRate : ℕ) :
    workloadThroughput baseRate .stream ≥ workloadThroughput baseRate .strided ∧
    workloadThroughput baseRate .stream ≥ workloadThroughput baseRate .random := by
  simp [workloadThroughput, workloadToOp, HCMR.throughput, HCMR.selfLoopProb]
  omega

/-- Stream workloads map to Stable cache state (good locality). -/
theorem stream_stable : workloadToSieveState .stream = .stable := rfl

/-- Scatter workloads map to Reset cache state (write-back thrashing). -/
theorem scatter_reset : workloadToSieveState .scatter = .reset := rfl

/-- HCMR connection: workload self-loop = HCMR self-loop for mapped op. -/
theorem workload_self_loop_is_hcmr (wt : WorkloadType) :
    workloadSelfLoop wt = HCMR.selfLoopProb (workloadToOp wt) := rfl

/-- COUCH connection: stream workloads are always COUCH-stable. -/
theorem stream_couch_stable (threshold : ℕ) (ht : threshold > 0) :
    HCMR.couchStable (workloadToOp .stream) threshold = true := by
  simp [workloadToOp]
  exact HCMR.ring_always_stable threshold ht

/-- CacheSieve connection: random workloads cause Unstable→Reset transitions. -/
theorem random_causes_reset :
    CacheSieve.sieveTransition .unstable 10 (workloadSelfLoop .random) = (.reset, .demote) := by
  simp [workloadSelfLoop, workloadToOp, HCMR.selfLoopProb, CacheSieve.sieveTransition,
        CacheSieve.ContentionThreshold]

end SilverSight.WorkloadTestbench
