-------------------------- MODULE RemoraApiMutation --------------------------
EXTENDS Naturals, FiniteSets

\* This model covers the durable API operation ledger around an abstract
\* JobProtocol effect; JobProtocol remains the sole phase-transition model.

CONSTANTS
    OperationScopes, EligibilityClaims, OperationIds, MutationKinds,
    Fingerprints, NoEligibility, NoRecord, NoObservation,
    Accepted, Rejected,
    FirstObservation, ReplayObservation, ConflictObservation

ASSUME
    /\ OperationScopes # {}
    /\ EligibilityClaims # {}
    /\ OperationIds # {}
    /\ MutationKinds # {}
    /\ Fingerprints # {}

Identities == OperationScopes \X OperationIds

Requests ==
    [scope       : OperationScopes,
     operation   : OperationIds,
     eligibility : EligibilityClaims,
     kind        : MutationKinds,
     fingerprint : Fingerprints]

\* Rejected abstracts endpoint-specific idempotency_conflict and
\* precondition_failed responses exercised by the executable contract.
Responses ==
    [status : {Accepted, Rejected},
     revision : 0..Cardinality(Identities)]

Records == [request : Requests, response : Responses]

Observations ==
    [request     : Requests,
     response    : Responses,
     disposition : {FirstObservation, ReplayObservation,
                    ConflictObservation}]

VARIABLES currentEligibility, records, effectCount, revision, observation

vars == <<currentEligibility, records, effectCount, revision, observation>>

Identity(request) == <<request.scope, request.operation>>

Eligible(request) ==
    /\ currentEligibility # NoEligibility
    /\ currentEligibility = request.eligibility

Init ==
    /\ currentEligibility \in EligibilityClaims
    /\ records = [identity \in Identities |-> NoRecord]
    /\ effectCount = [identity \in Identities |-> 0]
    /\ revision = 0
    /\ observation = NoObservation

FirstRequest(request) ==
    LET identity == Identity(request)
        accepted == Eligible(request)
        nextRevision == IF accepted THEN revision + 1 ELSE revision
        response ==
            [status |-> IF accepted THEN Accepted ELSE Rejected,
             revision |-> nextRevision]
        record == [request |-> request, response |-> response]
    IN /\ records[identity] = NoRecord
       /\ records' = [records EXCEPT ![identity] = record]
       /\ effectCount' =
            [effectCount EXCEPT ![identity] = IF accepted THEN 1 ELSE 0]
       /\ revision' = nextRevision
       /\ observation' =
            [request |-> request,
             response |-> response,
             disposition |-> FirstObservation]
       /\ UNCHANGED currentEligibility

ReplayRequest(request) ==
    LET identity == Identity(request)
        record == records[identity]
    IN /\ record # NoRecord
       /\ record.request = request
       /\ observation' =
            [request |-> request,
             response |-> record.response,
             disposition |-> ReplayObservation]
       /\ UNCHANGED <<currentEligibility, records, effectCount, revision>>

ConflictRequest(request) ==
    LET identity == Identity(request)
        record == records[identity]
        response ==
            [status |-> Rejected, revision |-> revision]
    IN /\ record # NoRecord
       /\ record.request # request
       /\ observation' =
            [request |-> request,
             response |-> response,
             disposition |-> ConflictObservation]
       /\ UNCHANGED <<currentEligibility, records, effectCount, revision>>

ChangeEligibility(nextEligibility) ==
    /\ nextEligibility \in EligibilityClaims \cup {NoEligibility}
    /\ nextEligibility # currentEligibility
    /\ currentEligibility' = nextEligibility
    /\ observation' = NoObservation
    /\ UNCHANGED <<records, effectCount, revision>>

Next ==
    \/ \E request \in Requests : FirstRequest(request)
    \/ \E request \in Requests : ReplayRequest(request)
    \/ \E request \in Requests : ConflictRequest(request)
    \/ \E nextEligibility \in EligibilityClaims \cup {NoEligibility} :
           ChangeEligibility(nextEligibility)

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

TypeOK ==
    /\ currentEligibility \in EligibilityClaims \cup {NoEligibility}
    /\ records \in [Identities -> Records \cup {NoRecord}]
    /\ effectCount \in [Identities -> 0..1]
    /\ revision \in 0..Cardinality(Identities)
    /\ observation \in Observations \cup {NoObservation}

RecordEffectConsistency ==
    \A identity \in Identities :
        effectCount[identity] = 1
            <=> /\ records[identity] # NoRecord
                /\ records[identity].response.status = Accepted

RevisionCountsEffects ==
    revision = Cardinality(
        {identity \in Identities : effectCount[identity] = 1})

ObservationConsistent ==
    observation # NoObservation =>
        LET identity == Identity(observation.request)
            record == records[identity]
        IN /\ record # NoRecord
           /\ CASE observation.disposition = FirstObservation ->
                      /\ record.request = observation.request
                      /\ record.response = observation.response
                  [] observation.disposition = ReplayObservation ->
                      /\ record.request = observation.request
                      /\ record.response = observation.response
                  [] observation.disposition = ConflictObservation ->
                      /\ record.request # observation.request
                      /\ observation.response.status = Rejected

RecordsAppendOnlyAction ==
    \A identity \in Identities :
        records[identity] # NoRecord => records'[identity] = records[identity]

EffectsApplyAtMostOnceAction ==
    \A identity \in Identities :
        effectCount[identity] = 1 => effectCount'[identity] = 1

RevisionMonotonicAction == revision' >= revision

RecordsAppendOnly == [][RecordsAppendOnlyAction]_vars
EffectsApplyAtMostOnce == [][EffectsApplyAtMostOnceAction]_vars
RevisionMonotonic == [][RevisionMonotonicAction]_vars

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