Define Nuthatch architecture and mutation protocol

docs/protocol/Nuthatch.tla

@@ -0,0 +1,662 @@
+----------------------------- MODULE Nuthatch -----------------------------
+EXTENDS FiniteSets, Naturals, TLC
+
+\* This model covers authorized one-key mutations within one idempotency epoch;
+\* lost bodies are not resumed and settle from the observed object state.
+
+CONSTANTS
+    Users, OperationIds, EnabledKinds, PersonalKeyNames, SharedKeys, Contents,
+    MaxObjectSize, PersonalLimit, SharedLimit,
+    MaxPostgresLosses, MaxObjectStoreLosses,
+    SharedPool, NoObject, NoRecord, NoOwner, NoObservation
+
+ASSUME
+    /\ Users # {}
+    /\ OperationIds # {}
+    /\ EnabledKinds # {}
+    /\ EnabledKinds \subseteq {"put", "delete"}
+    /\ PersonalKeyNames # {}
+    /\ SharedKeys # {}
+    /\ (Users \X PersonalKeyNames) \cap SharedKeys = {}
+    /\ Contents # {}
+    /\ SharedPool \notin Users
+    /\ NoObject \notin Contents
+    /\ MaxObjectSize \in Nat \ {0}
+    /\ PersonalLimit \in Nat
+    /\ SharedLimit \in Nat
+    /\ MaxPostgresLosses \in Nat
+    /\ MaxObjectStoreLosses \in Nat
+
+PersonalKeys == Users \X PersonalKeyNames
+Keys == PersonalKeys \cup SharedKeys
+Pools == Users \cup {SharedPool}
+Kinds == EnabledKinds
+Identities == Users \X Kinds \X OperationIds
+Sizes == 1..MaxObjectSize
+
+ObjectValues ==
+    {NoObject} \cup
+    [size : Sizes, content : Contents]
+
+Requests ==
+    [user      : Users,
+     operation : OperationIds,
+     kind      : Kinds,
+     key       : Keys,
+     size      : 0..MaxObjectSize,
+     content   : Contents \cup {NoObject}]
+
+ValidRequests ==
+    {request \in Requests :
+        /\ \/ request.key \in SharedKeys
+           \/ /\ request.key \in PersonalKeys
+              /\ request.key[1] = request.user
+        /\ IF request.kind = "put"
+           THEN /\ request.size \in Sizes
+                /\ request.content \in Contents
+           ELSE /\ request.size = 0
+                /\ request.content = NoObject}
+
+RecordStates == {"prepared", "applying", "succeeded", "failed", "rejected"}
+ActiveStates == {"prepared", "applying"}
+TerminalStates == {"succeeded", "failed", "rejected"}
+ExternalStates == {"idle", "pending", "settled"}
+
+RecordValues ==
+    [request : ValidRequests,
+     prior   : ObjectValues,
+     state   : RecordStates]
+
+Results == {"pending", "succeeded", "failed", "rejected", "conflict"}
+Dispositions == {"first", "replay", "conflict"}
+
+Observations ==
+    [request     : ValidRequests,
+     result      : Results,
+     disposition : Dispositions]
+
+VARIABLES
+    objects,
+    usedBytes,
+    reservedBytes,
+    keyOwner,
+    records,
+    externalState,
+    uploadBodyAvailable,
+    postgresUp,
+    objectStoreUp,
+    postgresLosses,
+    objectStoreLosses,
+    observation
+
+\* externalState is environmental truth: "settled" means no issued request can
+\* later mutate its key. Process loss does not erase a pending store request.
+
+vars == <<
+    objects,
+    usedBytes,
+    reservedBytes,
+    keyOwner,
+    records,
+    externalState,
+    uploadBodyAvailable,
+    postgresUp,
+    objectStoreUp,
+    postgresLosses,
+    objectStoreLosses,
+    observation
+>>
+
+Identity(request) == <<request.user, request.kind, request.operation>>
+
+PoolOf(key) ==
+    IF key \in PersonalKeys THEN key[1] ELSE SharedPool
+
+PoolKeys(pool) ==
+    IF pool = SharedPool
+    THEN SharedKeys
+    ELSE {key \in PersonalKeys : key[1] = pool}
+
+Limit(pool) ==
+    IF pool = SharedPool THEN SharedLimit ELSE PersonalLimit
+
+ObjectSize(object) ==
+    IF object = NoObject THEN 0 ELSE object.size
+
+DesiredObject(request) ==
+    IF request.kind = "delete"
+    THEN NoObject
+    ELSE [size |-> request.size, content |-> request.content]
+
+Growth(prior, desired) ==
+    IF ObjectSize(desired) > ObjectSize(prior)
+    THEN ObjectSize(desired) - ObjectSize(prior)
+    ELSE 0
+
+RequestFingerprint(request) ==
+    <<request.kind, PoolOf(request.key), request.key,
+      request.size, request.content>>
+
+RECURSIVE ObjectBytes(_, _)
+
+ObjectBytes(objectMap, keys) ==
+    IF keys = {}
+    THEN 0
+    ELSE LET key == CHOOSE candidate \in keys : TRUE
+         IN ObjectSize(objectMap[key]) +
+            ObjectBytes(objectMap, keys \ {key})
+
+Active(identity) ==
+    /\ records[identity] # NoRecord
+    /\ records[identity].state \in ActiveStates
+
+Terminal(identity) ==
+    /\ records[identity] # NoRecord
+    /\ records[identity].state \in TerminalStates
+
+Reservation(identity) ==
+    IF Active(identity)
+    THEN Growth(records[identity].prior,
+                DesiredObject(records[identity].request))
+    ELSE 0
+
+RECURSIVE ReservationTotal(_, _)
+
+ReservationTotal(identities, pool) ==
+    IF identities = {}
+    THEN 0
+    ELSE LET identity == CHOOSE candidate \in identities : TRUE
+             remainder == identities \ {identity}
+             amount ==
+                IF Active(identity) /\
+                   PoolOf(records[identity].request.key) = pool
+                THEN Reservation(identity)
+                ELSE 0
+         IN amount + ReservationTotal(remainder, pool)
+
+StateResult(state) ==
+    CASE state \in ActiveStates -> "pending"
+      [] state = "succeeded" -> "succeeded"
+      [] state = "failed" -> "failed"
+      [] state = "rejected" -> "rejected"
+
+CanAdmit(request) ==
+    LET pool == PoolOf(request.key)
+        prior == objects[request.key]
+        desired == DesiredObject(request)
+    IN /\ keyOwner[request.key] = NoOwner
+       /\ usedBytes[pool] + reservedBytes[pool] +
+          Growth(prior, desired) <= Limit(pool)
+
+Init ==
+    /\ objects \in [Keys -> ObjectValues]
+    /\ \A pool \in Pools :
+        ObjectBytes(objects, PoolKeys(pool)) <= Limit(pool)
+    /\ usedBytes =
+        [pool \in Pools |-> ObjectBytes(objects, PoolKeys(pool))]
+    /\ reservedBytes = [pool \in Pools |-> 0]
+    /\ keyOwner = [key \in Keys |-> NoOwner]
+    /\ records = [identity \in Identities |-> NoRecord]
+    /\ externalState = [identity \in Identities |-> "idle"]
+    /\ uploadBodyAvailable = [identity \in Identities |-> FALSE]
+    /\ postgresUp = TRUE
+    /\ objectStoreUp = TRUE
+    /\ postgresLosses = 0
+    /\ objectStoreLosses = 0
+    /\ observation = NoObservation
+
+FirstRequest(request) ==
+    LET identity == Identity(request)
+        pool == PoolOf(request.key)
+        prior == objects[request.key]
+        desired == DesiredObject(request)
+        admitted == CanAdmit(request)
+        nextState == IF admitted THEN "prepared" ELSE "rejected"
+        record ==
+            [request |-> request, prior |-> prior, state |-> nextState]
+        growth == Growth(prior, desired)
+    IN /\ postgresUp
+       /\ records[identity] = NoRecord
+       /\ records' = [records EXCEPT ![identity] = record]
+       /\ reservedBytes' =
+            IF admitted
+            THEN [reservedBytes EXCEPT ![pool] = @ + growth]
+            ELSE reservedBytes
+       /\ keyOwner' =
+            IF admitted
+            THEN [keyOwner EXCEPT ![request.key] = identity]
+            ELSE keyOwner
+       /\ uploadBodyAvailable' =
+            [uploadBodyAvailable EXCEPT
+                ![identity] = admitted /\ request.kind = "put"]
+       /\ observation' =
+            [request |-> request,
+             result |-> IF admitted THEN "pending" ELSE "rejected",
+             disposition |-> "first"]
+       /\ UNCHANGED <<
+            objects, usedBytes, externalState,
+            postgresUp, objectStoreUp,
+            postgresLosses, objectStoreLosses
+          >>
+
+ReplayRequest(request) ==
+    LET identity == Identity(request)
+        record == records[identity]
+    IN /\ postgresUp
+       /\ record # NoRecord
+       /\ record.request = request
+       /\ observation' =
+            [request |-> request,
+             result |-> StateResult(record.state),
+             disposition |-> "replay"]
+       /\ UNCHANGED <<
+            objects, usedBytes, reservedBytes, keyOwner, records,
+            externalState, uploadBodyAvailable,
+            postgresUp, objectStoreUp,
+            postgresLosses, objectStoreLosses
+          >>
+
+ConflictRequest(request) ==
+    LET identity == Identity(request)
+        record == records[identity]
+    IN /\ postgresUp
+       /\ record # NoRecord
+       /\ RequestFingerprint(record.request) # RequestFingerprint(request)
+       /\ observation' =
+            [request |-> request,
+             result |-> "conflict",
+             disposition |-> "conflict"]
+       /\ UNCHANGED <<
+            objects, usedBytes, reservedBytes, keyOwner, records,
+            externalState, uploadBodyAvailable,
+            postgresUp, objectStoreUp,
+            postgresLosses, objectStoreLosses
+          >>
+
+PrepareEffect(identity) ==
+    /\ postgresUp
+    /\ records[identity] # NoRecord
+    /\ records[identity].state = "prepared"
+    /\ records' = [records EXCEPT ![identity].state = "applying"]
+    /\ observation' = NoObservation
+    /\ UNCHANGED <<
+        objects, usedBytes, reservedBytes, keyOwner, externalState,
+        uploadBodyAvailable,
+        postgresUp, objectStoreUp, postgresLosses, objectStoreLosses
+       >>
+
+DispatchEffect(identity) ==
+    /\ postgresUp
+    /\ objectStoreUp
+    /\ records[identity] # NoRecord
+    /\ records[identity].state = "applying"
+    /\ externalState[identity] = "idle"
+    /\ (records[identity].request.kind = "delete" \/
+        uploadBodyAvailable[identity])
+    /\ externalState' =
+        [externalState EXCEPT ![identity] = "pending"]
+    /\ uploadBodyAvailable' =
+        [uploadBodyAvailable EXCEPT ![identity] = FALSE]
+    /\ observation' = NoObservation
+    /\ UNCHANGED <<
+        objects, usedBytes, reservedBytes, keyOwner, records,
+        postgresUp, objectStoreUp, postgresLosses, objectStoreLosses
+       >>
+
+LoseUploadBody(identity) ==
+    /\ records[identity] # NoRecord
+    /\ records[identity].request.kind = "put"
+    /\ Active(identity)
+    /\ externalState[identity] = "idle"
+    /\ uploadBodyAvailable[identity]
+    /\ uploadBodyAvailable' =
+        [uploadBodyAvailable EXCEPT ![identity] = FALSE]
+    /\ observation' = NoObservation
+    /\ UNCHANGED <<
+        objects, usedBytes, reservedBytes, keyOwner, records, externalState,
+        postgresUp, objectStoreUp, postgresLosses, objectStoreLosses
+       >>
+
+SettleLostUpload(identity) ==
+    /\ postgresUp
+    /\ objectStoreUp
+    /\ records[identity] # NoRecord
+    /\ records[identity].state = "applying"
+    /\ records[identity].request.kind = "put"
+    /\ externalState[identity] = "idle"
+    /\ ~uploadBodyAvailable[identity]
+    /\ externalState' =
+        [externalState EXCEPT ![identity] = "settled"]
+    /\ observation' = NoObservation
+    /\ UNCHANGED <<
+        objects, usedBytes, reservedBytes, keyOwner, records,
+        uploadBodyAvailable,
+        postgresUp, objectStoreUp, postgresLosses, objectStoreLosses
+       >>
+
+ExternalEffectApplied(identity) ==
+    LET request == records[identity].request
+    IN /\ objectStoreUp
+       /\ records[identity] # NoRecord
+       /\ records[identity].state = "applying"
+       /\ externalState[identity] = "pending"
+       /\ objects' =
+            [objects EXCEPT ![request.key] = DesiredObject(request)]
+       /\ externalState' =
+            [externalState EXCEPT ![identity] = "settled"]
+       /\ observation' = NoObservation
+       /\ UNCHANGED <<
+            usedBytes, reservedBytes, keyOwner, records,
+            uploadBodyAvailable,
+            postgresUp, objectStoreUp,
+            postgresLosses, objectStoreLosses
+          >>
+
+ExternalEffectNotApplied(identity) ==
+    /\ objectStoreUp
+    /\ records[identity] # NoRecord
+    /\ records[identity].state = "applying"
+    /\ externalState[identity] = "pending"
+    /\ externalState' =
+        [externalState EXCEPT ![identity] = "settled"]
+    /\ observation' = NoObservation
+    /\ UNCHANGED <<
+        objects, usedBytes, reservedBytes, keyOwner, records,
+        uploadBodyAvailable,
+        postgresUp, objectStoreUp, postgresLosses, objectStoreLosses
+       >>
+
+FinalizeSuccess(identity) ==
+    LET record == records[identity]
+        request == record.request
+        key == request.key
+        pool == PoolOf(key)
+        priorSize == ObjectSize(record.prior)
+        desired == DesiredObject(request)
+        desiredSize == ObjectSize(desired)
+        growth == Growth(record.prior, desired)
+    IN /\ postgresUp
+       /\ objectStoreUp
+       /\ record # NoRecord
+       /\ record.state = "applying"
+       /\ externalState[identity] = "settled"
+       /\ objects[key] = desired
+       /\ records' = [records EXCEPT ![identity].state = "succeeded"]
+       /\ usedBytes' =
+            [usedBytes EXCEPT ![pool] = (@ - priorSize) + desiredSize]
+       /\ reservedBytes' =
+            [reservedBytes EXCEPT ![pool] = @ - growth]
+       /\ keyOwner' = [keyOwner EXCEPT ![key] = NoOwner]
+       /\ externalState' =
+            [externalState EXCEPT ![identity] = "idle"]
+       /\ uploadBodyAvailable' =
+            [uploadBodyAvailable EXCEPT ![identity] = FALSE]
+       /\ observation' = NoObservation
+       /\ UNCHANGED <<
+            objects, postgresUp, objectStoreUp,
+            postgresLosses, objectStoreLosses
+          >>
+
+FinalizeFailure(identity) ==
+    LET record == records[identity]
+        request == record.request
+        key == request.key
+        pool == PoolOf(key)
+        desired == DesiredObject(request)
+        growth == Growth(record.prior, desired)
+    IN /\ postgresUp
+       /\ objectStoreUp
+       /\ record # NoRecord
+       /\ record.state = "applying"
+       /\ externalState[identity] = "settled"
+       /\ objects[key] = record.prior
+       /\ record.prior # desired
+       /\ records' = [records EXCEPT ![identity].state = "failed"]
+       /\ reservedBytes' =
+            [reservedBytes EXCEPT ![pool] = @ - growth]
+       /\ keyOwner' = [keyOwner EXCEPT ![key] = NoOwner]
+       /\ externalState' =
+            [externalState EXCEPT ![identity] = "idle"]
+       /\ uploadBodyAvailable' =
+            [uploadBodyAvailable EXCEPT ![identity] = FALSE]
+       /\ observation' = NoObservation
+       /\ UNCHANGED <<
+            objects, usedBytes, postgresUp, objectStoreUp,
+            postgresLosses, objectStoreLosses
+          >>
+
+LosePostgres ==
+    /\ postgresUp
+    /\ postgresLosses < MaxPostgresLosses
+    /\ postgresUp' = FALSE
+    /\ postgresLosses' = postgresLosses + 1
+    /\ observation' = NoObservation
+    /\ UNCHANGED <<
+        objects, usedBytes, reservedBytes, keyOwner, records,
+        externalState, uploadBodyAvailable,
+        objectStoreUp, objectStoreLosses
+       >>
+
+RestorePostgres ==
+    /\ ~postgresUp
+    /\ postgresUp' = TRUE
+    /\ observation' = NoObservation
+    /\ UNCHANGED <<
+        objects, usedBytes, reservedBytes, keyOwner, records,
+        externalState, uploadBodyAvailable, objectStoreUp,
+        postgresLosses, objectStoreLosses
+       >>
+
+LoseObjectStore ==
+    /\ objectStoreUp
+    /\ objectStoreLosses < MaxObjectStoreLosses
+    /\ objectStoreUp' = FALSE
+    /\ objectStoreLosses' = objectStoreLosses + 1
+    /\ observation' = NoObservation
+    /\ UNCHANGED <<
+        objects, usedBytes, reservedBytes, keyOwner, records,
+        externalState, uploadBodyAvailable, postgresUp, postgresLosses
+       >>
+
+RestoreObjectStore ==
+    /\ ~objectStoreUp
+    /\ objectStoreUp' = TRUE
+    /\ observation' = NoObservation
+    /\ UNCHANGED <<
+        objects, usedBytes, reservedBytes, keyOwner, records,
+        externalState, uploadBodyAvailable, postgresUp,
+        postgresLosses, objectStoreLosses
+       >>
+
+ControllerAdvance(identity) ==
+    \/ PrepareEffect(identity)
+    \/ DispatchEffect(identity)
+    \/ LoseUploadBody(identity)
+    \/ SettleLostUpload(identity)
+    \/ FinalizeSuccess(identity)
+    \/ FinalizeFailure(identity)
+
+StoreSettlement(identity) ==
+    \/ ExternalEffectApplied(identity)
+    \/ ExternalEffectNotApplied(identity)
+
+Next ==
+    \/ \E request \in ValidRequests : FirstRequest(request)
+    \/ \E request \in ValidRequests : ReplayRequest(request)
+    \/ \E request \in ValidRequests : ConflictRequest(request)
+    \/ \E identity \in Identities : ControllerAdvance(identity)
+    \/ \E identity \in Identities : StoreSettlement(identity)
+    \/ LosePostgres
+    \/ RestorePostgres
+    \/ LoseObjectStore
+    \/ RestoreObjectStore
+
+Fairness ==
+    /\ WF_vars(RestorePostgres)
+    /\ WF_vars(RestoreObjectStore)
+    /\ \A identity \in Identities :
+        /\ WF_vars(ControllerAdvance(identity))
+        /\ WF_vars(StoreSettlement(identity))
+
+Spec == Init /\ [][Next]_vars /\ Fairness
+
+TypeOK ==
+    /\ objects \in [Keys -> ObjectValues]
+    /\ usedBytes \in [Pools -> Nat]
+    /\ reservedBytes \in [Pools -> Nat]
+    /\ keyOwner \in [Keys -> Identities \cup {NoOwner}]
+    /\ records \in [Identities -> RecordValues \cup {NoRecord}]
+    /\ externalState \in [Identities -> ExternalStates]
+    /\ uploadBodyAvailable \in [Identities -> BOOLEAN]
+    /\ postgresUp \in BOOLEAN
+    /\ objectStoreUp \in BOOLEAN
+    /\ postgresLosses \in 0..MaxPostgresLosses
+    /\ objectStoreLosses \in 0..MaxObjectStoreLosses
+    /\ observation \in Observations \cup {NoObservation}
+
+RecordIdentityConsistent ==
+    \A identity \in Identities :
+        records[identity] # NoRecord =>
+            Identity(records[identity].request) = identity
+
+PersonalRequestsUseOwnPool ==
+    \A request \in ValidRequests :
+        request.key \in PersonalKeys =>
+            PoolOf(request.key) = request.user
+
+PersonalPoolsDisjoint ==
+    \A first, second \in Users :
+        first # second =>
+            PoolKeys(first) \cap PoolKeys(second) = {}
+
+FingerprintBindsRequest ==
+    \A first, second \in ValidRequests :
+        Identity(first) = Identity(second) /\
+        RequestFingerprint(first) = RequestFingerprint(second)
+        => first = second
+
+ReservationsConsistent ==
+    \A pool \in Pools :
+        reservedBytes[pool] = ReservationTotal(Identities, pool)
+
+LocksConsistent ==
+    \A key \in Keys :
+        \/ /\ keyOwner[key] = NoOwner
+           /\ ~\E identity \in Identities :
+                Active(identity) /\
+                records[identity].request.key = key
+        \/ /\ keyOwner[key] \in Identities
+           /\ Active(keyOwner[key])
+           /\ records[keyOwner[key]].request.key = key
+           /\ \A identity \in Identities :
+                Active(identity) /\
+                records[identity].request.key = key
+                => identity = keyOwner[key]
+
+ActiveObjectConsistent ==
+    \A identity \in Identities :
+        Active(identity) =>
+            LET record == records[identity]
+                key == record.request.key
+            IN objects[key] \in
+                {record.prior, DesiredObject(record.request)}
+
+ExternalStateConsistent ==
+    \A identity \in Identities :
+        /\ (externalState[identity] # "idle" =>
+                /\ records[identity] # NoRecord
+                /\ records[identity].state = "applying")
+        /\ (records[identity] # NoRecord /\
+            records[identity].state # "applying" =>
+                externalState[identity] = "idle")
+
+UploadBodyConsistent ==
+    \A identity \in Identities :
+        uploadBodyAvailable[identity] =>
+            /\ Active(identity)
+            /\ records[identity].request.kind = "put"
+            /\ externalState[identity] = "idle"
+
+QuotaReservationBound ==
+    \A pool \in Pools :
+        usedBytes[pool] + reservedBytes[pool] <= Limit(pool)
+
+ObjectStateCovered ==
+    \A pool \in Pools :
+        ObjectBytes(objects, PoolKeys(pool)) <=
+            usedBytes[pool] + reservedBytes[pool]
+
+ObjectQuotaBound ==
+    \A pool \in Pools :
+        ObjectBytes(objects, PoolKeys(pool)) <= Limit(pool)
+
+AccountingAtQuiescence ==
+    \A pool \in Pools :
+        (~\E identity \in Identities :
+            Active(identity) /\
+            PoolOf(records[identity].request.key) = pool) =>
+            usedBytes[pool] = ObjectBytes(objects, PoolKeys(pool))
+
+ObservationConsistent ==
+    observation # NoObservation =>
+        LET identity == Identity(observation.request)
+            record == records[identity]
+        IN /\ record # NoRecord
+           /\ CASE observation.disposition = "first" ->
+                    /\ record.request = observation.request
+                    /\ observation.result = StateResult(record.state)
+              [] observation.disposition = "replay" ->
+                    /\ record.request = observation.request
+                    /\ observation.result = StateResult(record.state)
+              [] observation.disposition = "conflict" ->
+                    /\ RequestFingerprint(record.request) #
+                       RequestFingerprint(observation.request)
+                    /\ observation.result = "conflict"
+
+RecordsNeverForgottenAction ==
+    \A identity \in Identities :
+        records[identity] # NoRecord => records'[identity] # NoRecord
+
+RequestBindingsStableAction ==
+    \A identity \in Identities :
+        records[identity] # NoRecord =>
+            records'[identity].request = records[identity].request
+
+TerminalRecordsStableAction ==
+    \A identity \in Identities :
+        Terminal(identity) => records'[identity] = records[identity]
+
+PostgresFailureFenceAction ==
+    (~postgresUp /\ ~postgresUp') =>
+        UNCHANGED <<usedBytes, reservedBytes, keyOwner, records>>
+
+ObjectStoreFailureFenceAction ==
+    (~objectStoreUp /\ ~objectStoreUp') =>
+        UNCHANGED <<objects, externalState>>
+
+SettledEffectsDoNotMutateAction ==
+    \A identity \in Identities :
+        Active(identity) /\ externalState[identity] = "settled" =>
+            LET key == records[identity].request.key
+            IN objects'[key] = objects[key]
+
+RecordsNeverForgotten == [][RecordsNeverForgottenAction]_vars
+RequestBindingsStable == [][RequestBindingsStableAction]_vars
+TerminalRecordsStable == [][TerminalRecordsStableAction]_vars
+PostgresFailureFencesDurableState == [][PostgresFailureFenceAction]_vars
+ObjectStoreFailureFencesObjects == [][ObjectStoreFailureFenceAction]_vars
+SettledEffectsDoNotMutate == [][SettledEffectsDoNotMutateAction]_vars
+
+UnfinishedEventuallyTerminal ==
+    \A identity \in Identities :
+        Active(identity) ~> Terminal(identity)
+
+LostUploadEventuallyTerminal ==
+    \A identity \in Identities :
+        (Active(identity) /\
+         records[identity].request.kind = "put" /\
+         ~uploadBodyAvailable[identity] /\
+         externalState[identity] = "idle")
+        ~> Terminal(identity)
+
+=============================================================================