Model API mutation replay semantics

docs/protocol/RemoraApiMutation.cfg

@@ -0,0 +1,29 @@
+SPECIFICATION Spec
+
+CHECK_DEADLOCK TRUE
+
+CONSTANTS
+    OperationScopes = {scope1}
+    EligibilityClaims = {eligibility1, eligibility2}
+    OperationIds = {op1, op2}
+    MutationKinds = {submit, renew, progress, success, failure}
+    Fingerprints = {fp1, fp2}
+    NoEligibility = NoEligibility
+    NoRecord = NoRecord
+    NoObservation = NoObservation
+    Accepted = Accepted
+    PreconditionFailed = PreconditionFailed
+    FirstObservation = FirstObservation
+    ReplayObservation = ReplayObservation
+    ConflictObservation = ConflictObservation
+
+INVARIANTS
+    TypeOK
+    RecordEffectConsistency
+    RevisionCountsEffects
+    ObservationConsistent
+
+PROPERTIES
+    RecordsAppendOnly
+    EffectsApplyAtMostOnce
+    RevisionMonotonic

docs/protocol/RemoraApiMutation.tla

@@ -0,0 +1,163 @@
+-------------------------- 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, PreconditionFailed,
+    FirstObservation, ReplayObservation, ConflictObservation
+
+ASSUME
+    /\ OperationScopes # {}
+    /\ EligibilityClaims # {}
+    /\ OperationIds # {}
+    /\ MutationKinds # {}
+    /\ Fingerprints # {}
+
+Identities == OperationScopes \X OperationIds
+
+Requests ==
+    [scope       : OperationScopes,
+     operation   : OperationIds,
+     eligibility : EligibilityClaims,
+     kind        : MutationKinds,
+     fingerprint : Fingerprints]
+
+Responses ==
+    [status : {Accepted, PreconditionFailed},
+     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 PreconditionFailed,
+             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 |-> PreconditionFailed, 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 = PreconditionFailed
+
+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
+
+=============================================================================

docs/spec/api/README.md

@@ -26,6 +26,10 @@ and `operation_id`. Each operation identity retains a request fingerprint. An
 exact replay has the original effect; a changed worker, fence, payload, stale,
 or non-authoritative tuple returns `precondition_failed` without mutation.
 
+[`RemoraApiMutation`](../../protocol/RemoraApiMutation.tla) models this durable
+operation ledger around an abstract successful `JobProtocol` effect. It does
+not redefine job phases or attempt-authority transitions.
+
 ## Authorization and errors
 
 Public operations apply the authorization rules in the architecture. List is

docs/spec/api/openapi.yaml

@@ -222,7 +222,7 @@ paths:
         content:
           application/json:
             schema:
-              $ref: '#/components/schemas/AttemptMutation'
+              $ref: '#/components/schemas/AttemptRenewRequest'
       responses:
         '204':
           description: Renewed or duplicate operation accepted.
@@ -721,6 +721,10 @@ components:
           minimum: 1
         worker_incarnation:
           $ref: '#/components/schemas/OpaqueId'
+    AttemptRenewRequest:
+      unevaluatedProperties: false
+      allOf:
+        - $ref: '#/components/schemas/AttemptMutation'
     AttemptProgressRequest:
       unevaluatedProperties: false
       allOf: