-- SilverSight.RRC.ReceiptDensity — Q16_16 receipt-density scoring
--
-- Ports the core scoring logic from Research Stack's
-- Semantics.RRC.ReceiptDensity into SilverSight.
--
-- Boundary rules:
--   - All scoring arithmetic is Q16_16 fixed-point (no Float in compute paths).
--   - promotion is always not_promoted at this stage.
--   - This module is an admissibility gate, not a proof.

import SilverSight.FixedPoint
import SilverSight.RRCLogogramProjection
import SilverSight.RRC.Emit

/-! # Receipt Density Scoring (RRC)

Ports the receipt-density scoring logic from Research Stack's
`Semantics.RRC.ReceiptDensity` into SilverSight. Computes a weighted
density and confidence score from status, axis flags, spectral features,
and PIST shape agreement — all in Q16_16 fixed-point arithmetic.

This module is an **admissibility gate**, not a proof. Promotion is
always `not_promoted` at this stage.

## Key Definitions
- `SourceStatus` / `statusScore` — base score from row status (BLOCKED→VERIFIED)
- `AxisFlags` / `axisScore` — target-axis hit ratio (5 boolean flags, capped at 4)
- `SpectralFeatures` / `spectralQuality` — weighted spectral quality composite
- `shapeAgreement` — PIST proxy/exact shape match scoring
- `computeDensity` — final weighted density + confidence + warnings

## Dependencies
- `SilverSight.FixedPoint` (Q16_16 arithmetic)
- `SilverSight.RRCLogogramProjection` (RRCShape type)
- `SilverSight.RRC.Emit` (emission boundary)
-/

namespace SilverSight.RRC.ReceiptDensity

open SilverSight.FixedPoint
open SilverSight.FixedPoint.Q16_16
open SilverSight.RRCLogogramProjection

-- ─────────────────────────────────────────────────────────────────────────────
-- §1  Status base scores  (ports STATUS_BASE dict in Research Stack shim)
--     All values are Q16_16 raw integers (denominator = 65536 = 1.0)
--     BLOCKED  = 0.00  → 0
--     HOLD     = 0.12  → 7864
--     CANDIDATE= 0.45  → 29491
--     REVIEWED = 0.78  → 51118
--     VERIFIED = 0.84  → 55050
-- ─────────────────────────────────────────────────────────────────────────────

inductive SourceStatus where
  | blocked
  | hold
  | candidate
  | reviewed
  | verified
  deriving DecidableEq, Repr

def statusScoreRaw : SourceStatus → Int
  | .blocked   => 0
  | .hold      => 7864    -- 0.12 * 65536 ≈ 7864
  | .candidate => 29491   -- 0.45 * 65536 ≈ 29491
  | .reviewed  => 51118   -- 0.78 * 65536 ≈ 51118
  | .verified  => 55050   -- 0.84 * 65536 ≈ 55050

def statusScore (s : SourceStatus) : Q16_16 :=
  Q16_16.ofRawInt (statusScoreRaw s)

-- ─────────────────────────────────────────────────────────────────────────────
-- §2  Target axes  (ports TARGET_AXES set in Research Stack shim)
--
--   projection_declared, negative_control_strength, witness_declared,
--   scale_band_declared, shape_closure
--
-- We represent axes as a structure of Bool flags in this order.
-- ─────────────────────────────────────────────────────────────────────────────

structure AxisFlags where
  projectionDeclared       : Bool
  negativeControlStrength  : Bool
  witnessDeclared          : Bool
  scaleBandDeclared        : Bool
  shapeClosure             : Bool
  deriving Repr

def axisHitCount (flags : AxisFlags) : Nat :=
  (if flags.projectionDeclared      then 1 else 0) +
  (if flags.negativeControlStrength then 1 else 0) +
  (if flags.witnessDeclared         then 1 else 0) +
  (if flags.scaleBandDeclared       then 1 else 0) +
  (if flags.shapeClosure            then 1 else 0)

-- axis_score(row) = clamp(hits / 4, 0, 1)
-- denominator 4 matches the Research Stack shim (not 5 — intentional).
def axisScore (flags : AxisFlags) : Q16_16 :=
  let hits := axisHitCount flags
  if hits == 0 then Q16_16.zero
  else
    let capped := if hits ≥ 4 then 4 else hits
    Q16_16.ofRatio capped 4

-- ─────────────────────────────────────────────────────────────────────────────
-- §3  Shape agreement  (ports shape_agreement in Research Stack shim)
-- ─────────────────────────────────────────────────────────────────────────────

def shapeAgreement
    (rrcShape : RRCShape)
    (pistProxy : Option RRCShape)
    (pistExact : Option RRCShape)
    : Q16_16 :=
  let matchShape (opt : Option RRCShape) : Bool :=
    match opt, rrcShape with
    | some .signalShapedRouteCompiler,          .signalShapedRouteCompiler          => true
    | some .projectableGeometryTopology,        .projectableGeometryTopology        => true
    | some .cognitiveLoadField,                 .cognitiveLoadField                 => true
    | some .cadForceProbeReceipt,               .cadForceProbeReceipt               => true
    | some .logogramProjection,                 .logogramProjection                 => true
    | some .holdForUnlawfulOrUnderspecifiedShape, .holdForUnlawfulOrUnderspecifiedShape => true
    | _, _ => false
  if matchShape pistExact then
    Q16_16.ofRatio 100 100  -- 1.0
  else if matchShape pistProxy then
    Q16_16.ofRawInt 53739   -- 0.82
  else if pistProxy.isSome || pistExact.isSome then
    Q16_16.ofRawInt 22938   -- 0.35
  else
    Q16_16.zero

-- ─────────────────────────────────────────────────────────────────────────────
-- §4  Spectral quality  (ports spectral_quality in Research Stack shim)
-- ─────────────────────────────────────────────────────────────────────────────

structure SpectralFeatures where
  rankScore     : Q16_16   -- rank_estimate / 8.0, clamped [0,1]
  gapScore      : Q16_16   -- spectral_gap, clamped [0,1]
  entropyScore  : Q16_16   -- strand_entropy / 3.0, clamped [0,1]
  densityScore  : Q16_16   -- crossing_density / 0.5, clamped [0,1]
  lapFull       : Bool     -- laplacian_zero_count ≥ 1
  hasHashes     : Bool     -- canonical_hash AND matrix_hash present
  deriving Repr

private def wRank    : Int := 24
private def wGap     : Int := 18
private def wEntropy : Int := 18
private def wDensity : Int := 12
private def wLap     : Int := 12
private def wHash    : Int := 16

private def lapScore (lapFull : Bool) : Q16_16 :=
  if lapFull then Q16_16.one else Q16_16.ofRawInt 29491  -- 0.45 * 65536

private def hashScore (hasHashes : Bool) : Q16_16 :=
  if hasHashes then Q16_16.one else Q16_16.zero

def spectralQuality (f : SpectralFeatures) : Q16_16 :=
  let raw :=
    wRank    * f.rankScore.toInt / 100 +
    wGap     * f.gapScore.toInt  / 100 +
    wEntropy * f.entropyScore.toInt / 100 +
    wDensity * f.densityScore.toInt / 100 +
    wLap     * (lapScore f.lapFull).toInt / 100 +
    wHash    * (hashScore f.hasHashes).toInt / 100
  Q16_16.ofRawInt raw

-- ─────────────────────────────────────────────────────────────────────────────
-- §5  Receipt density and confidence  (ports compute_density in Research Stack shim)
-- ─────────────────────────────────────────────────────────────────────────────

structure DensityComponents where
  statusScore   : Q16_16
  axisScore     : Q16_16
  spectralScore : Q16_16
  shapeScore    : Q16_16
  deriving Repr

structure DensityResult where
  density     : Q16_16
  confidence  : Q16_16
  components  : DensityComponents
  warnings    : List String
  deriving Repr

private def weightedSum (weights : List Int) (scores : List Q16_16) : Q16_16 :=
  let raw := (weights.zip scores).foldl
    (fun acc (ws : Int × Q16_16) => acc + ws.1 * ws.2.toInt / 100)
    0
  Q16_16.ofRawInt raw

def computeDensity
    (status  : SourceStatus)
    (axes    : AxisFlags)
    (spectral: SpectralFeatures)
    (shape   : RRCShape)
    (pistProxy : Option RRCShape)
    (pistExact : Option RRCShape)
    : DensityResult :=
  let sStatus   := statusScore status
  let sAxes     := axisScore axes
  let sSpectral := spectralQuality spectral
  let sShape    := shapeAgreement shape pistProxy pistExact

  let hasPrediction := pistProxy.isSome || pistExact.isSome

  let warnings : List String :=
    (if !hasPrediction then ["missing_pist_prediction"] else []) ++
    (if hasPrediction && sShape.toInt < 32768 then ["pist_shape_disagreement"] else [])

  let densityWeights    : List Int := [26, 24, 26, 24]
  let confidenceWeights : List Int := [20, 20, 28, 32]
  let scoreList         : List Q16_16 := [sStatus, sAxes, sSpectral, sShape]

  let density    := weightedSum densityWeights    scoreList
  let confidence := weightedSum confidenceWeights scoreList

  { density    := density
    confidence := confidence
    components := { statusScore := sStatus, axisScore := sAxes
                    spectralScore := sSpectral, shapeScore := sShape }
    warnings   := warnings.eraseDups }

-- ─────────────────────────────────────────────────────────────────────────────
-- §6  Claim boundary
-- ─────────────────────────────────────────────────────────────────────────────

def claimBoundary : String :=
  "receipt-density-scoring-only; not-a-proof; promotion=not_promoted"

-- ─────────────────────────────────────────────────────────────────────────────
-- §7  Eval witnesses
-- ─────────────────────────────────────────────────────────────────────────────

-- Witness: CANDIDATE row with 3/5 target axes, no PIST prediction.
#eval
  let axes : AxisFlags :=
    { projectionDeclared := true, negativeControlStrength := false
      witnessDeclared := true, scaleBandDeclared := true, shapeClosure := false }
  let spectral : SpectralFeatures :=
    { rankScore := Q16_16.zero, gapScore := Q16_16.zero, entropyScore := Q16_16.zero
      densityScore := Q16_16.zero, lapFull := false, hasHashes := false }
  let r := computeDensity .candidate axes spectral
            RRCShape.cognitiveLoadField none none
  (r.density.toInt, r.warnings)

-- Witness: VERIFIED row, exact PIST match, 5/5 axes, full spectral.
#eval
  let axes : AxisFlags :=
    { projectionDeclared := true, negativeControlStrength := true
      witnessDeclared := true, scaleBandDeclared := true, shapeClosure := true }
  let spectral : SpectralFeatures :=
    { rankScore := Q16_16.ofRatio 1 2  -- rank=4/8=0.5
      gapScore  := Q16_16.ofRatio 3 4  -- gap=0.75
      entropyScore := Q16_16.ofRatio 2 3  -- entropy/3=0.67
      densityScore := Q16_16.ofRatio 1 2  -- crossing/0.5=0.5
      lapFull   := true, hasHashes := true }
  let r := computeDensity .verified axes spectral
            RRCShape.logogramProjection
            (some RRCShape.logogramProjection) (some RRCShape.logogramProjection)
  (r.density.toInt, r.confidence.toInt, r.warnings)

end SilverSight.RRC.ReceiptDensity
