Separate protocol authority from mutable API contracts

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.

docs/protocol/Remora.tla

@@ -97,6 +97,7 @@ NoOutcome             == "NoOutcome"
 WantsSuccess          == "WantsSuccess"
 WantsRetryableFailure == "WantsRetryableFailure"
 WantsPermanentFailure == "WantsPermanentFailure"
+\* Adapters map concrete failure classes to these dispositions before JobProtocol.
 FailureOutcomes == {WantsRetryableFailure, WantsPermanentFailure}
 OutcomeRequests == {NoOutcome, WantsSuccess} \cup FailureOutcomes
 
@@ -113,7 +114,9 @@ TokenOf(a) == a.token
 VARIABLES
     \* DurableStore authority.
     phase, cancelRequested, currentToken, authority, dispatchNeeded,
-    committedAttempt, checkpoint, checkpointValid,
+    committedAttempt, checkpoint,
+    \* Abstracts the complete source-identity and destination-state proof.
+    checkpointValid,
 
     \* CoordinationStore (reconstructible).
     queued, reservation, leaseState, leaseAge, cancelNotice,
@@ -275,6 +278,7 @@ AuthorizeAttempt(j, w) ==
        /\ UNCHANGED workerVars
        /\ UNCHANGED pendingOutcome
 
+\* Concrete ExecutionEnvelope validation is abstracted into activation.
 ActivateAttempt(a) ==
     LET j == JobOf(a)
         w == attemptWorker[a]
@@ -447,6 +451,7 @@ ReapLostAttempt(a) ==
        /\ UNCHANGED <<attemptWorker, attemptProgress, initialProgress,
                        resumedFromCheckpoint, stageState, pendingOutcome>>
 
+\* RetryWait abstracts backoff; operation timeouts are outcomes, not a job deadline.
 ScheduleRetry(j) ==
     /\ phase[j] = RetryWait
     /\ phase'          = [phase EXCEPT ![j] = Queued]
@@ -721,6 +726,7 @@ RejectOutcome(a) ==
     /\ UNCHANGED <<attemptState, attemptWorker, attemptProgress,
                     initialProgress, resumedFromCheckpoint, stageState>>
 
+\* Concrete cleanup streams exact durable identities; this action models eligibility.
 CleanupStage(a) ==
     LET j == JobOf(a)
     IN /\ stageState[a] \in {StagePartial, StageComplete}
@@ -953,6 +959,7 @@ StagingOwnership ==
         /\ (committedAttempt[JobOf(a)] = a =>
                 stageState[a] = StageComplete)
 
+\* Deletion is outside JobProtocol and must preserve terminal-state immutability.
 TerminalStep ==
     \A j \in Jobs :
         Terminal(j) =>