ms2k
dfd60cf104
Move API artifacts out of docs/spec, define concrete execution and deletion refinements, and document TLA+ abstraction boundaries so architecture prose cannot become a competing protocol specification.
166 lines
6 KiB
Text
166 lines
6 KiB
Text
-------------------------- 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.
|
|
\* Identities range over one retention epoch; record expiry is outside the 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
|
|
|
|
=============================================================================
|