/-
SilverSight.Semantics.Layout

A Layout is a physical encoding choice for a Schema. It is independent of
the logical shape: the same schema may be encoded as row-major, columnar,
compact, or an mmap view. The Core only defines the layout enum and a
fixed-point cost model; layout-specific encoders live in WireFormat.
-/

import SilverSight.FixedPoint

namespace SilverSight.Semantics

open SilverSight.FixedPoint.Q0_16

/-- Physical layout choices for a fixed-size schema. -/
inductive Layout where
  | rowMajor   -- natural C-array order, good for sequential scans
  | columnar   -- field-major order, good for random field access
  | compact    -- bit-packed or delta-coded, good for storage/transfer
  | mmapView   -- direct memory-map view, no copy on read
  deriving Repr, DecidableEq, BEq

export Layout (rowMajor columnar compact mmapView)

/-- Access profile used to score a layout. All counts are raw event tallies;
    the cost function compresses them into a Q0_16 dimensionless score. -/
structure AccessProfile where
  randomReads     : Nat
  sequentialReads : Nat
  writes          : Nat
  deriving Repr, DecidableEq, BEq

namespace Layout

/-- Per-layout operation weights (relative, dimensionless). -/
def randomReadWeight : Layout → Nat
  | rowMajor  => 4
  | columnar  => 1
  | compact   => 3
  | mmapView  => 1

def sequentialReadWeight : Layout → Nat
  | rowMajor  => 1
  | columnar  => 3
  | compact   => 4
  | mmapView  => 2

def writeWeight : Layout → Nat
  | rowMajor  => 3
  | columnar  => 3
  | compact   => 1
  | mmapView  => 4

/-- Cost of a layout for a given access profile. Lower is better.

    The raw score is a weighted sum of event counts. It is clamped into the
    Q0_16 range, so extremely hot profiles saturate rather than overflow. -/
def cost (layout : Layout) (profile : AccessProfile) : Q0_16 :=
  let raw :=
    profile.randomReads     * randomReadWeight layout +
    profile.sequentialReads * sequentialReadWeight layout +
    profile.writes          * writeWeight layout
  ofRawInt (Int.ofNat raw)

end Layout

/-- All Core layouts, in the order used by the default cost-based selector. -/
def allLayouts : List Layout :=
  [Layout.rowMajor, Layout.columnar, Layout.compact, Layout.mmapView]

private def pickBest (best l : Layout) (profile : AccessProfile) : Layout :=
  if lt (Layout.cost l profile) (Layout.cost best profile) then l else best

private lemma le_refl (a : Q0_16) : le a a := by simp [le]

private lemma le_trans {a b c : Q0_16} (h1 : le a b) (h2 : le b c) : le a c := by
  simp [le] at h1 h2 ⊢
  omega

private lemma not_lt_iff_le (a b : Q0_16) : lt a b = false ↔ le b a := by
  simp [lt, le]

private lemma pickBest_le_best (best l : Layout) (profile : AccessProfile) :
    le (Layout.cost (pickBest best l profile) profile) (Layout.cost best profile) := by
  unfold pickBest
  split_ifs with h
  · have hlt : (Layout.cost l profile).toInt < (Layout.cost best profile).toInt := by
      simpa [lt] using h
    simp [le]
    omega
  · exact le_refl _

private lemma pickBest_le_l (best l : Layout) (profile : AccessProfile) :
    le (Layout.cost (pickBest best l profile) profile) (Layout.cost l profile) := by
  unfold pickBest
  split_ifs with h
  · exact le_refl _
  · have hle : (Layout.cost best profile).toInt ≤ (Layout.cost l profile).toInt := by
      simpa [lt, le] using h
    simp [le]
    omega

private lemma foldl_le_seen (profile : AccessProfile) (init : Layout) (ls : List Layout) :
    let result := ls.foldl (fun b l => pickBest b l profile) init
    le (Layout.cost result profile) (Layout.cost init profile) ∧
    ∀ l ∈ ls, le (Layout.cost result profile) (Layout.cost l profile) := by
  induction ls generalizing init with
  | nil => simp [le_refl]
  | cons h t ih =>
      simp [List.foldl]
      apply And.intro
      · apply le_trans
        · exact (ih (pickBest init h profile)).1
        · exact pickBest_le_best init h profile
      · apply And.intro
        · apply le_trans
          · exact (ih (pickBest init h profile)).1
          · exact pickBest_le_l init h profile
        · intro a hmem
          exact (ih (pickBest init h profile)).2 a hmem

/-- Choose the layout with minimal cost for a given access profile.
    Ties are broken toward the earlier layout in `allLayouts`. -/
def chooseLayoutByCost (profile : AccessProfile) : Layout :=
  allLayouts.foldl (fun best l => pickBest best l profile) Layout.rowMajor

/-- The cost-based selector is ε-suboptimal: it never picks a layout with
    higher cost than any other Core layout. -/
theorem chooseLayoutByCost_le (profile : AccessProfile) (l : Layout) :
    le (Layout.cost (chooseLayoutByCost profile) profile) (Layout.cost l profile) := by
  have h : ∀ x ∈ allLayouts,
      le (Layout.cost (chooseLayoutByCost profile) profile) (Layout.cost x profile) := by
    simp [chooseLayoutByCost]
    exact (foldl_le_seen profile Layout.rowMajor allLayouts).2
  cases l
  all_goals
    apply h
    simp [allLayouts]

end SilverSight.Semantics
