/*
 * Copyright (C) 2026 HCALC / Foundry J contributors
 * SPDX-License-Identifier: AGPL-3.0-only
 *
 * Module: Contract — production C = scale-or-id (Spec); ContractAlg = Gershgorin→C.
 * SoftProject/A3 remains Foundry *schedule* soft_project cite-only (prop 43).
 * DO NOT assert C = soft_project prop43.
 * Cite: PRODUCTION.md §3 Gap-C-wrapper, §7 Gap-ContractAlg CLOSED.
 * Provenance: SpecDefined (C, ContractAlg); source-claim (A2/A3/A5)
 */

module modules/Contract

open modules/State

/* Provenance: source-claim — PROPERTIES 25 tier labels. */
abstract sig EpsilonTier {}
one sig T1, T2, T3, T4 extends EpsilonTier {}

sig Jacobian {}

sig SpectralBound {
  of: one Jacobian,
  belowMargin: lone EpsilonTier,
  powerIterOK: lone EpsilonTier
}

/* A2 — contractive(J,ε) iff gershgorin(J) < 1-ε (optional power-iter).
 * Provenance: source-claim — FOUNDRY_J_CROSSLINKS §3 A2 / props 33–37. */
pred contractive[j: Jacobian, e: EpsilonTier] {
  some sb: SpectralBound | sb.of = j and (sb.belowMargin = e or sb.powerIterOK = e)
}

pred gershgorin_below[j: Jacobian, e: EpsilonTier] {
  some sb: SpectralBound | sb.of = j and sb.belowMargin = e
}

fact fact_A2_contractive_iff {
  all j: Jacobian, e: EpsilonTier |
    contractive[j, e] iff
      (gershgorin_below[j, e] or
       (some sb: SpectralBound | sb.of = j and sb.powerIterOK = e))
}

assert A2_contractive_iff_gershgorin_bound {
  /* Sealed assert id A2 — PROPERTY_MAP */
  all j: Jacobian, e: EpsilonTier |
    contractive[j, e] iff
      (gershgorin_below[j, e] or
       (some sb: SpectralBound | sb.of = j and sb.powerIterOK = e))
}

/* ---- SoftProject: Foundry *schedule* soft_project cite-only (prop 43 / A3) ----
 * NOT identified with Spec C (scale-or-id on state). */
sig QBudget {
  q: Int,
  epsTier: one EpsilonTier,
  overMargin: Int
}

sig SoftProject {
  budget: one QBudget,
  applied: Int
}

fact fact_A3_soft_project {
  all sp: SoftProject |
    (sp.budget.overMargin = 1) implies sp.applied = 1
}

assert A3_soft_project_when_q_over_margin {
  /* Sealed assert id A3 — PROPERTY_MAP; Foundry schedule soft_project cite-only */
  all sp: SoftProject |
    (sp.budget.overMargin = 1) implies sp.applied = 1
}

/* ---- Production Spec C: scale-or-id on state ----
 * C(x) = ((1-ε)/q)·x if q>1-ε else x. Provenance: SpecDefined — PRODUCTION §3.
 * Distinct from SoftProject (Foundry schedule API). */
abstract sig CMode {}
one sig ScaleOrId extends CMode {}

sig COp {
  mode: one CMode,
  apply: State -> lone State
}

fact fact_P3_c_scale_or_id {
  all c: COp | c.mode = ScaleOrId
}

pred c_scale_or_id_ok {
  all c: COp | c.mode = ScaleOrId
}

assert P3_c_scale_or_id {
  /* Production assert P3 — C = Spec scale-or-id (NOT soft_project identity) */
  c_scale_or_id_ok
}

/* SoftProject and COp remain distinct families (no forced equality). */
fact fact_C_not_soft_project_identity {
  /* Structural: SoftProject and COp are different sigs; no bridge equating them. */
  all sp: SoftProject | some sp.budget
  all c: COp | c.mode = ScaleOrId
}

/* ---- Production ContractAlg: Gershgorin then scale-or-id (Spec C) ----
 * Provenance: SpecDefined — PRODUCTION.md §7. */
abstract sig ContractAlgKind {}
one sig GershgorinThenScaleOrId extends ContractAlgKind {}

one sig ProductionContractAlg {
  kind: one ContractAlgKind
}

fact fact_P8_contractalg_gershgorin_then_c {
  ProductionContractAlg.kind = GershgorinThenScaleOrId
}

pred contractalg_gershgorin_then_c_ok {
  ProductionContractAlg.kind = GershgorinThenScaleOrId
}

assert P8_contractalg_gershgorin_then_c {
  /* Production assert P8 — ContractAlg = Gershgorin → scale-or-id C */
  contractalg_gershgorin_then_c_ok
}

/* Measure non-increase — relational order (no Int). */
one sig MeasureOrder {
  nonIncrease: Measure -> Measure
}

fact fact_measure_order_reflexive {
  all m: Measure | m in m.(MeasureOrder.nonIncrease)
}

pred measure_non_increase[s: State, sNext: State] {
  all sm: StateMeasure, smNext: StateMeasure |
    (sm.of = s and smNext.of = sNext) implies
      smNext.m in sm.m.(MeasureOrder.nonIncrease)
}

sig ContractLink {
  pre: one State,
  post: one State
}

fact fact_measure_on_contract_links {
  all cl: ContractLink | measure_non_increase[cl.pre, cl.post]
}

assert INV_contract_measure_non_increase {
  all cl: ContractLink | measure_non_increase[cl.pre, cl.post]
}

/* A5 — PMAT conservation if used (optional/gated). */
sig PMATUsage {
  conserved: Int
}

fact fact_A5_pmat_if_used {
  all p: PMATUsage | p.conserved = 1
}

assert A5_PMAT_conservation_gated {
  /* Sealed assert id A5 — PROPERTY_MAP */
  all p: PMATUsage | p.conserved = 1
}