---------------------------- MODULE TokenLabels ----------------------------
(***************************************************************************)
(* A data-publishing pipeline for energy "nutrition labels".               *)
(*                                                                         *)
(* Source measurements come from a benchmark repo.  Each measurement has:  *)
(*   - an arm (runtime identifier)                                         *)
(*   - a methodology group (e.g. battery-delta vs. wall-power windows;     *)
(*     abstracted here as model values)                                    *)
(*   - a quantization/build string (possibly missing, modeled as NoQuant)  *)
(*   - an energy value jPerTok (abstracted as a small natural)             *)
(*                                                                         *)
(* A build step derives labels from measurements.  The label's kcal value  *)
(* is derived ONLY from jPerTok via an abstract derivation function.       *)
(* Labels are published grouped by methodology group, and ranking badges   *)
(* ("class best") are computed only among labels of the same group.        *)
(*                                                                         *)
(* Checked invariants:                                                     *)
(*   PublishedHasQuant    - every published label carries a non-empty      *)
(*                          quantization/build                             *)
(*   PublishedHasSource   - every published label references an existing   *)
(*                          source measurement                             *)
(*   NoCrossGroupRanking  - badges compare only same-group labels          *)
(*   DerivationConsistent - a published label's kcal corresponds to its    *)
(*                          measurement's jPerTok (and group/quant match)  *)
(***************************************************************************)
EXTENDS Naturals, FiniteSets, TLC

CONSTANTS
    Arms,      \* runtime identifiers
    Groups,    \* methodology groups
    Quants,    \* valid (non-empty) quantization/build strings
    NoQuant,   \* marker for a measurement lacking a quantization string
    Ids,       \* measurement / source-file identifiers
    JVals      \* possible jPerTok energy values (small naturals)

ASSUME NoQuant \notin Quants
ASSUME JVals \subseteq Nat

(***************************************************************************)
(* Abstract derivation: stands in for kcal = jPerTok * 1e6 / 4184.         *)
(* All that matters for the design is that kcal is a function of jPerTok   *)
(* alone, applied identically at build time and demanded by the invariant. *)
(***************************************************************************)
Derive(j) == j * 239

MeasRec  == [arm: Arms, group: Groups, quant: Quants \cup {NoQuant}, j: JVals]
LabelRec == [src: Ids, group: Groups, quant: Quants,
             kcal: {Derive(j) : j \in JVals}]
BadgeRec == [src: Ids, group: Groups, comparedWith: SUBSET Ids]

VARIABLES
    meas,       \* partial function Ids -> MeasRec: ingested measurements
    labels,     \* set of LabelRec: labels derived by the build step
    published,  \* subset of labels published onto the site
    badges      \* set of BadgeRec: "class best" style ranking badges

vars == <<meas, labels, published, badges>>

TypeOK ==
    /\ DOMAIN meas \subseteq Ids
    /\ \A id \in DOMAIN meas : meas[id] \in MeasRec
    /\ labels \subseteq LabelRec
    /\ published \subseteq labels
    /\ badges \subseteq BadgeRec

-----------------------------------------------------------------------------

Init ==
    /\ meas = [id \in {} |-> {}]
    /\ labels = {}
    /\ published = {}
    /\ badges = {}

(* A new measurement arrives from the benchmark repo, possibly one that    *)
(* lacks a quantization/build string (quant = NoQuant).                    *)
Ingest ==
    \E id \in Ids \ DOMAIN meas :
        \E r \in MeasRec :
            /\ meas' = meas @@ (id :> r)
            /\ UNCHANGED <<labels, published, badges>>

(* The build step derives a label from a measurement.  Design decisions    *)
(* under check: it refuses measurements without a quantization string,     *)
(* and kcal comes only from the measurement's jPerTok via Derive.          *)
Build ==
    \E id \in DOMAIN meas :
        /\ meas[id].quant # NoQuant
        /\ ~\E l \in labels : l.src = id
        /\ labels' = labels \cup
             {[src   |-> id,
               group |-> meas[id].group,
               quant |-> meas[id].quant,
               kcal  |-> Derive(meas[id].j)]}
        /\ UNCHANGED <<meas, published, badges>>

(* A built label goes onto the site. *)
Publish ==
    \E l \in labels \ published :
        /\ published' = published \cup {l}
        /\ UNCHANGED <<meas, labels, badges>>

(* A ranking badge is granted to a published label.  The comparison set is *)
(* exactly the published labels of the SAME methodology group (the design  *)
(* rule NoCrossGroupRanking checks).  At most one badge per source.        *)
GrantBadge ==
    \E l \in published :
        /\ ~\E b \in badges : b.src = l.src
        /\ badges' = badges \cup
             {[src          |-> l.src,
               group        |-> l.group,
               comparedWith |-> {p.src : p \in {q \in published :
                                                   q.group = l.group}}]}
        /\ UNCHANGED <<meas, labels, published>>

Next == Ingest \/ Build \/ Publish \/ GrantBadge

Spec == Init /\ [][Next]_vars

-----------------------------------------------------------------------------
(* Invariants *)

(* 1. Every published label carries a non-empty quantization/build. *)
PublishedHasQuant ==
    \A l \in published : l.quant \in Quants

(* 2. Every published label's source reference exists among the ingested   *)
(*    measurements.                                                        *)
PublishedHasSource ==
    \A l \in published : l.src \in DOMAIN meas

(* 3. Ranking badges are computed only among labels of the same            *)
(*    methodology group.                                                   *)
NoCrossGroupRanking ==
    \A b \in badges :
        \A s \in b.comparedWith :
            /\ s \in DOMAIN meas
            /\ meas[s].group = b.group

(* 4. A published label's kcal value is exactly the abstract derivation    *)
(*    applied to its source measurement's jPerTok; group and quant carry   *)
(*    through unchanged.                                                   *)
DerivationConsistent ==
    \A l \in published :
        /\ l.src \in DOMAIN meas
        /\ l.kcal  = Derive(meas[l.src].j)
        /\ l.group = meas[l.src].group
        /\ l.quant = meas[l.src].quant

=============================================================================