---------------------- MODULE RemoraClaimActivation ----------------------
EXTENDS Naturals

\* Split-store refinement of the atomic JobProtocol ActivateAttempt action.
\* Durable execution is the linearization point; lease creation alone is not authority.

CONSTANTS
    Claims, Fences, Workers, Operations,
    NoWorker, NoOwner, NoRequest, NoResponse, Accepted, Rejected

RequestKeys == Claims \X Fences \X Workers

ASSUME /\ Claims # {}
       /\ Fences # {}
       /\ Workers # {}
       /\ Operations # {}
       /\ NoWorker \notin Workers
       /\ NoRequest \notin RequestKeys

Authorized == "Authorized"
Executing  == "Executing"
Reaped     == "Reaped"
DurableStates == {Authorized, Executing, Reaped}

Idle         == "Idle"
Validated    == "Validated"
LeaseCreated == "LeaseCreated"
Committed    == "Committed"
Finished     == "Finished"
ActivationStages == {Idle, Validated, LeaseCreated, Committed, Finished}

Activator == "Activator"
Recovery  == "Recovery"
LockOwners == {NoOwner, Activator, Recovery}
Responses == {NoResponse, Accepted, Rejected}

VARIABLES
    durableState, attemptFence, attemptWorker, reservation, lease,
    activationStage, durableLock, operationRequest, operationResponse,
    conflictRequest, activationEffectCount

vars == <<durableState, attemptFence, attemptWorker, reservation, lease,
          activationStage, durableLock, operationRequest, operationResponse,
          conflictRequest, activationEffectCount>>

Request(c, f, w) == <<c, f, w>>
ExactRequest(c) == Request(c, attemptFence[c], attemptWorker[c])

Init ==
    /\ durableState = [c \in Claims |-> Authorized]
    /\ attemptFence \in [Claims -> Fences]
    /\ attemptWorker \in [Claims -> Workers]
    /\ reservation = attemptWorker
    /\ lease = [c \in Claims |-> NoWorker]
    /\ activationStage = [c \in Claims |-> Idle]
    /\ durableLock = [c \in Claims |-> NoOwner]
    /\ operationRequest = [op \in Operations |-> NoRequest]
    /\ operationResponse = [op \in Operations |-> NoResponse]
    /\ conflictRequest = [op \in Operations |-> NoRequest]
    /\ activationEffectCount = [c \in Claims |-> 0]

BindOperation(op, c, f, w) ==
    /\ operationRequest[op] = NoRequest
    /\ operationRequest' =
        [operationRequest EXCEPT ![op] = Request(c, f, w)]
    /\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
                    lease, activationStage, durableLock, operationResponse,
                    conflictRequest, activationEffectCount>>

RejectOperationReuse(op, c, f, w) ==
    /\ operationRequest[op] # NoRequest
    /\ operationRequest[op] # Request(c, f, w)
    /\ conflictRequest' =
        [conflictRequest EXCEPT ![op] = Request(c, f, w)]
    /\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
                    lease, activationStage, durableLock, operationRequest,
                    operationResponse, activationEffectCount>>

StartActivation(op, c, f, w) ==
    /\ operationRequest[op] = Request(c, f, w)
    /\ operationResponse[op] = NoResponse
    /\ Request(c, f, w) = ExactRequest(c)
    /\ activationStage[c] = Idle
    /\ durableState[c] = Authorized
    /\ reservation[c] = w
    /\ activationStage' = [activationStage EXCEPT ![c] = Validated]
    /\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
                    lease, durableLock, operationRequest, operationResponse,
                    conflictRequest, activationEffectCount>>

CreateLease(c) ==
    LET w == attemptWorker[c]
    IN /\ activationStage[c] = Validated
       /\ durableState[c] = Authorized
       /\ reservation[c] = w
       /\ lease[c] = NoWorker
       /\ lease' = [lease EXCEPT ![c] = w]
       /\ activationStage' = [activationStage EXCEPT ![c] = LeaseCreated]
       /\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
                       durableLock, operationRequest, operationResponse,
                       conflictRequest, activationEffectCount>>

AcquireActivationLock(c) ==
    /\ activationStage[c] = LeaseCreated
    /\ durableState[c] = Authorized
    /\ durableLock[c] = NoOwner
    /\ durableLock' = [durableLock EXCEPT ![c] = Activator]
    /\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
                    lease, activationStage, operationRequest,
                    operationResponse, conflictRequest,
                    activationEffectCount>>

LoseActivatorLock(c) ==
    /\ durableLock[c] = Activator
    /\ durableLock' = [durableLock EXCEPT ![c] = NoOwner]
    /\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
                    lease, activationStage, operationRequest,
                    operationResponse, conflictRequest,
                    activationEffectCount>>

CommitActivation(c) ==
    LET w == attemptWorker[c]
    IN /\ activationStage[c] = LeaseCreated
       /\ durableLock[c] = Activator
       /\ durableState[c] = Authorized
       /\ reservation[c] = w
       /\ lease[c] = w
       /\ durableState' = [durableState EXCEPT ![c] = Executing]
       /\ reservation' = [reservation EXCEPT ![c] = NoWorker]
       /\ activationStage' = [activationStage EXCEPT ![c] = Committed]
       /\ durableLock' = [durableLock EXCEPT ![c] = NoOwner]
       /\ activationEffectCount' =
            [activationEffectCount EXCEPT ![c] = @ + 1]
       /\ UNCHANGED <<attemptFence, attemptWorker, lease,
                       operationRequest, operationResponse, conflictRequest>>

ReplayActivation(op, c, f, w) ==
    /\ operationRequest[op] = Request(c, f, w)
    /\ Request(c, f, w) = ExactRequest(c)
    /\ durableState[c] = Executing
    /\ lease[c] = w
    /\ activationEffectCount[c] = 1
    /\ operationResponse' =
        [operationResponse EXCEPT ![op] = Accepted]
    /\ activationStage' = [activationStage EXCEPT ![c] = Finished]
    /\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
                    lease, durableLock, operationRequest, conflictRequest,
                    activationEffectCount>>

RejectPrecondition(op, c, f, w) ==
    /\ operationRequest[op] = Request(c, f, w)
    /\ operationResponse[op] = NoResponse
    /\ \/ Request(c, f, w) # ExactRequest(c)
       \/ durableState[c] = Reaped
       \/ /\ durableState[c] = Executing
          /\ lease[c] # w
    /\ operationResponse' =
        [operationResponse EXCEPT ![op] = Rejected]
    /\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
                    lease, activationStage, durableLock, operationRequest,
                    conflictRequest, activationEffectCount>>

ExpireReservation(c) ==
    /\ durableState[c] = Authorized
    /\ reservation[c] # NoWorker
    /\ reservation' = [reservation EXCEPT ![c] = NoWorker]
    /\ UNCHANGED <<durableState, attemptFence, attemptWorker, lease,
                    activationStage, durableLock, operationRequest,
                    operationResponse, conflictRequest,
                    activationEffectCount>>

ExpireLease(c) ==
    /\ durableState[c] = Executing
    /\ lease[c] = attemptWorker[c]
    /\ lease' = [lease EXCEPT ![c] = NoWorker]
    /\ operationResponse' =
        [op \in Operations |->
            IF operationResponse[op] = Accepted
               /\ operationRequest[op][1] = c
            THEN NoResponse ELSE operationResponse[op]]
    /\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
                    activationStage, durableLock, operationRequest,
                    conflictRequest, activationEffectCount>>

AcquireRecoveryLock(c) ==
    /\ durableState[c] = Authorized
    /\ reservation[c] = NoWorker
    /\ durableLock[c] = NoOwner
    /\ durableLock' = [durableLock EXCEPT ![c] = Recovery]
    /\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
                    lease, activationStage, operationRequest,
                    operationResponse, conflictRequest,
                    activationEffectCount>>

FinishRecovery(c) ==
    /\ durableLock[c] = Recovery
    /\ durableState[c] = Authorized
    /\ durableState' = [durableState EXCEPT ![c] = Reaped]
    /\ reservation' = [reservation EXCEPT ![c] = NoWorker]
    /\ lease' = [lease EXCEPT ![c] = NoWorker]
    /\ durableLock' = [durableLock EXCEPT ![c] = NoOwner]
    /\ UNCHANGED <<attemptFence, attemptWorker, activationStage,
                    operationRequest, operationResponse, conflictRequest,
                    activationEffectCount>>

CompensateRejectedActivation(c) ==
    LET w == attemptWorker[c]
    IN /\ durableState[c] = Reaped
       /\ activationStage[c] \in {Validated, LeaseCreated}
       /\ lease[c] \in {NoWorker, w}
       /\ lease' = [lease EXCEPT ![c] = NoWorker]
       /\ activationStage' = [activationStage EXCEPT ![c] = Finished]
       /\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
                       durableLock, operationRequest, operationResponse,
                       conflictRequest, activationEffectCount>>

Done ==
    /\ \A c \in Claims : durableState[c] \in {Executing, Reaped}
    /\ UNCHANGED vars

Next ==
    \/ \E op \in Operations, c \in Claims, f \in Fences, w \in Workers :
           BindOperation(op, c, f, w)
    \/ \E op \in Operations, c \in Claims, f \in Fences, w \in Workers :
           RejectOperationReuse(op, c, f, w)
    \/ \E op \in Operations, c \in Claims, f \in Fences, w \in Workers :
           StartActivation(op, c, f, w)
    \/ \E c \in Claims : CreateLease(c)
    \/ \E c \in Claims : AcquireActivationLock(c)
    \/ \E c \in Claims : LoseActivatorLock(c)
    \/ \E c \in Claims : CommitActivation(c)
    \/ \E op \in Operations, c \in Claims, f \in Fences, w \in Workers :
           ReplayActivation(op, c, f, w)
    \/ \E op \in Operations, c \in Claims, f \in Fences, w \in Workers :
           RejectPrecondition(op, c, f, w)
    \/ \E c \in Claims : ExpireReservation(c)
    \/ \E c \in Claims : ExpireLease(c)
    \/ \E c \in Claims : AcquireRecoveryLock(c)
    \/ \E c \in Claims : FinishRecovery(c)
    \/ \E c \in Claims : CompensateRejectedActivation(c)
    \/ Done

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

TypeOK ==
    /\ durableState \in [Claims -> DurableStates]
    /\ attemptFence \in [Claims -> Fences]
    /\ attemptWorker \in [Claims -> Workers]
    /\ reservation \in [Claims -> Workers \cup {NoWorker}]
    /\ lease \in [Claims -> Workers \cup {NoWorker}]
    /\ activationStage \in [Claims -> ActivationStages]
    /\ durableLock \in [Claims -> LockOwners]
    /\ operationRequest \in [Operations -> RequestKeys \cup {NoRequest}]
    /\ operationResponse \in [Operations -> Responses]
    /\ conflictRequest \in [Operations -> RequestKeys \cup {NoRequest}]
    /\ activationEffectCount \in [Claims -> 0..1]

LiveLeaseMatchesAuthority ==
    \A c \in Claims :
        lease[c] # NoWorker => lease[c] = attemptWorker[c]

ExecutingIsCommitted ==
    \A c \in Claims :
        durableState[c] = Executing =>
            /\ reservation[c] = NoWorker
            /\ activationStage[c] \in {Committed, Finished}
            /\ activationEffectCount[c] = 1

AcceptedResponseIsExactReplay ==
    \A op \in Operations :
        operationResponse[op] = Accepted =>
            \E c \in Claims :
                /\ operationRequest[op] = ExactRequest(c)
                /\ durableState[c] = Executing
                /\ lease[c] = attemptWorker[c]
                /\ activationEffectCount[c] = 1

ConflictIsChangedRequest ==
    \A op \in Operations :
        conflictRequest[op] # NoRequest =>
            /\ operationRequest[op] # NoRequest
            /\ conflictRequest[op] # operationRequest[op]

ReapedClaimHasNoActivationEffect ==
    \A c \in Claims :
        durableState[c] = Reaped => activationEffectCount[c] = 0

ReapedCoordinationIsClean ==
    \A c \in Claims :
        durableState[c] = Reaped =>
            /\ reservation[c] = NoWorker
            /\ lease[c] = NoWorker

RecoveryOwnsInactiveClaim ==
    \A c \in Claims :
        durableLock[c] = Recovery => reservation[c] = NoWorker

ActivationAppliesAtMostOnceAction ==
    \A c \in Claims :
        activationEffectCount[c] = 1 => activationEffectCount'[c] = 1

ActivationAppliesAtMostOnce == [][ActivationAppliesAtMostOnceAction]_vars

OperationRequestIsImmutableAction ==
    \A op \in Operations :
        operationRequest[op] # NoRequest =>
            operationRequest'[op] = operationRequest[op]

OperationRequestIsImmutable == [][OperationRequestIsImmutableAction]_vars

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