Tighten activation recovery and API contracts

docs/api/README.md

@@ -39,12 +39,21 @@ after durable authority changes. It never creates or restores a claim. Progress
 and outcome operations require current fenced authority and return
 `precondition_failed` for stale or non-authoritative tuples.
 
+Activation returns the live lease expiry and a recommended renewal time. Renewal
+returns the corresponding updated projection. These timestamps schedule worker
+behavior; the coordination store remains authoritative for whether the lease is
+live.
+
 A successful claim returns the attempt authority and the attempt's
 `ExecutionEnvelope`. The worker verifies that their job, attempt, fence, and
-worker incarnation agree before source or target I/O. Opaque resolved-source
+worker incarnation agree before source or target I/O. Resolved-source and
-and checkpoint references identify durable streamable state; they are not
+checkpoint descriptors identify durable streamable state; they are not
 reconstructed from coordination data.
 
+Resolved-source and checkpoint references carry their descriptor kind, schema
+version, byte length, and SHA-256. The service accepts them only when their kind,
+ownership, integrity, and fenced attempt authority match the 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. Its `Rejected`
@@ -62,6 +71,11 @@ bound to the authenticated subject and filter.
 credential values, bearer material, URL userinfo, raw upstream response bodies,
 internal stack traces, or unredacted configured endpoints.
 
+Credential creation uses a closed material shape selected by `kind`; rotation
+must use the existing kind's shape. Custom HTTP headers use lowercase canonical
+names and reject connection-nominated, routing, framing, cookie, proxy, and
+authentication headers.
+
 ## Jobs, pages, and results
 
 `Job.phase` uses the exact `JobProtocol` phase vocabulary; this contract does
@@ -81,6 +95,10 @@ unauthorized, absent, and never-committed results are not exposed. The hard
 delete endpoint returns the durable deletion resource established by the
 architecture.
 
+Before hard deletion, job reads return the complete `job` projection. Once only
+the permanent minimal record remains, authorized reads and deleted-job pages use
+the distinct `tombstone` projection rather than inventing discarded job fields.
+
 A deletion whose exact remaining work cannot progress because target access or
 configuration is unavailable enters `blocked` with a redacted problem. It
 retains the deletion obligation and can return to active processing when the

docs/api/openapi.yaml

@@ -61,11 +61,11 @@ paths:
       operationId: getJob
       responses:
         '200':
-          description: Current authorized job projection.
+          description: Current authorized full job or minimal hard-deletion tombstone projection.
           content:
             application/json:
               schema:
-                $ref: '#/components/schemas/Job'
+                $ref: '#/components/schemas/JobResource'
         '404':
           $ref: '#/components/responses/NotFound'
         default:
@@ -438,8 +438,12 @@ paths:
             schema:
               $ref: '#/components/schemas/AttemptRenewRequest'
       responses:
-        '204':
+        '200':
-          description: Existing live coordination lease renewed or duplicate operation accepted; durable authority is unchanged.
+          description: Existing exact live coordination lease renewed or prior response replayed; durable authority is unchanged.
+          content:
+            application/json:
+              schema:
+                $ref: '#/components/schemas/LeaseProjection'
         '409':
           $ref: '#/components/responses/PreconditionFailed'
         default:
@@ -886,17 +890,92 @@ components:
     SourceCredentialKind:
       type: string
       enum: [basic_auth, bearer_token, http_headers, object_store, hugging_face]
-    CredentialMaterial:
+    BasicAuthMaterial:
       type: object
-      minProperties: 1
+      additionalProperties: false
-      maxProperties: 64
+      required: [username, password]
-      additionalProperties:
+      properties:
+        username:
+          type: string
+          minLength: 1
+          maxLength: 1024
+        password:
           type: string
           minLength: 1
           maxLength: 16384
       writeOnly: true
-      description: Write-only adapter credential fields. Values are never returned or logged.
+    TokenMaterial:
+      type: object
+      additionalProperties: false
+      required: [token]
+      properties:
+        token:
+          type: string
+          minLength: 1
+          maxLength: 16384
+      writeOnly: true
+    HttpHeadersMaterial:
+      type: object
+      additionalProperties: false
+      required: [headers]
+      properties:
+        headers:
+          type: object
+          minProperties: 1
+          maxProperties: 64
+          propertyNames:
+            allOf:
+              - pattern: '^[a-z0-9!#$%&''*+.^_`|~-]+$'
+              - not:
+                  enum: [authorization, connection, content-length, cookie, host, keep-alive, proxy-authenticate, proxy-authorization, te, trailer, transfer-encoding, upgrade]
+          additionalProperties:
+            type: string
+            minLength: 1
+            maxLength: 16384
+          description: Canonical lowercase end-to-end headers. Connection-nominated and routing, framing, cookie, proxy, and authentication headers are rejected.
+      writeOnly: true
+    ObjectStoreCredentialMaterial:
+      type: object
+      additionalProperties: false
+      required: [access_key_id, secret_access_key]
+      properties:
+        access_key_id:
+          type: string
+          minLength: 1
+          maxLength: 1024
+        secret_access_key:
+          type: string
+          minLength: 1
+          maxLength: 16384
+        session_token:
+          type: string
+          minLength: 1
+          maxLength: 16384
+      writeOnly: true
+    CredentialMaterial:
+      oneOf:
+        - $ref: '#/components/schemas/BasicAuthMaterial'
+        - $ref: '#/components/schemas/TokenMaterial'
+        - $ref: '#/components/schemas/HttpHeadersMaterial'
+        - $ref: '#/components/schemas/ObjectStoreCredentialMaterial'
+      writeOnly: true
+      description: Write-only material whose closed shape must match the credential kind. Values are never returned or logged.
     SourceCredentialCreate:
+      oneOf:
+        - $ref: '#/components/schemas/BasicAuthCredentialCreate'
+        - $ref: '#/components/schemas/BearerTokenCredentialCreate'
+        - $ref: '#/components/schemas/HttpHeadersCredentialCreate'
+        - $ref: '#/components/schemas/ObjectStoreCredentialCreate'
+        - $ref: '#/components/schemas/HuggingFaceCredentialCreate'
+      discriminator:
+        propertyName: kind
+        mapping:
+          basic_auth: '#/components/schemas/BasicAuthCredentialCreate'
+          bearer_token: '#/components/schemas/BearerTokenCredentialCreate'
+          http_headers: '#/components/schemas/HttpHeadersCredentialCreate'
+          object_store: '#/components/schemas/ObjectStoreCredentialCreate'
+          hugging_face: '#/components/schemas/HuggingFaceCredentialCreate'
+    BasicAuthCredentialCreate:
       type: object
       additionalProperties: false
       required: [label, kind, material]
@@ -906,13 +985,66 @@ components:
           minLength: 1
           maxLength: 200
         kind:
-          $ref: '#/components/schemas/SourceCredentialKind'
+          const: basic_auth
         material:
-          $ref: '#/components/schemas/CredentialMaterial'
+          $ref: '#/components/schemas/BasicAuthMaterial'
+    BearerTokenCredentialCreate:
+      type: object
+      additionalProperties: false
+      required: [label, kind, material]
+      properties:
+        label:
+          type: string
+          minLength: 1
+          maxLength: 200
+        kind:
+          const: bearer_token
+        material:
+          $ref: '#/components/schemas/TokenMaterial'
+    HttpHeadersCredentialCreate:
+      type: object
+      additionalProperties: false
+      required: [label, kind, material]
+      properties:
+        label:
+          type: string
+          minLength: 1
+          maxLength: 200
+        kind:
+          const: http_headers
+        material:
+          $ref: '#/components/schemas/HttpHeadersMaterial'
+    ObjectStoreCredentialCreate:
+      type: object
+      additionalProperties: false
+      required: [label, kind, material]
+      properties:
+        label:
+          type: string
+          minLength: 1
+          maxLength: 200
+        kind:
+          const: object_store
+        material:
+          $ref: '#/components/schemas/ObjectStoreCredentialMaterial'
+    HuggingFaceCredentialCreate:
+      type: object
+      additionalProperties: false
+      required: [label, kind, material]
+      properties:
+        label:
+          type: string
+          minLength: 1
+          maxLength: 200
+        kind:
+          const: hugging_face
+        material:
+          $ref: '#/components/schemas/TokenMaterial'
     SourceCredentialRotate:
       type: object
       additionalProperties: false
       required: [material]
+      description: The material shape must match the stored credential kind; rotation never changes kind.
       properties:
         material:
           $ref: '#/components/schemas/CredentialMaterial'
@@ -977,6 +1109,9 @@ components:
     JobPhase:
       type: string
       enum: [Queued, Running, RetryWait, Cancelling, Succeeded, Failed, Cancelled]
+    TerminalJobPhase:
+      type: string
+      enum: [Succeeded, Failed, Cancelled]
     JobLifecycle:
       type: string
       enum: [visible, soft_deleted, hard_deleting, hard_deleted]
@@ -992,6 +1127,19 @@ components:
           minimum: 1
         worker_incarnation:
           $ref: '#/components/schemas/OpaqueId'
+    LeaseProjection:
+      type: object
+      additionalProperties: false
+      required: [expires_at, renew_after]
+      properties:
+        expires_at:
+          type: string
+          format: date-time
+          description: Expiry of the exact coordination lease established for this authority.
+        renew_after:
+          type: string
+          format: date-time
+          description: Earliest recommended renewal time, strictly before expires_at.
     Progress:
       type: object
       additionalProperties: false
@@ -1129,6 +1277,27 @@ components:
     Sha256Digest:
       type: string
       pattern: '^sha256:[a-f0-9]{64}$'
+    DurableDescriptorRef:
+      type: object
+      additionalProperties: false
+      required: [id, kind, schema_version, byte_length, checksum]
+      properties:
+        id:
+          $ref: '#/components/schemas/OpaqueId'
+        kind:
+          type: string
+          enum: [resolved_source, checkpoint]
+        schema_version:
+          type: integer
+          minimum: 1
+        byte_length:
+          type: integer
+          minimum: 0
+        item_count:
+          type: integer
+          minimum: 0
+        checksum:
+          $ref: '#/components/schemas/Sha256Digest'
     ResultMember:
       type: object
       additionalProperties: false
@@ -1160,8 +1329,10 @@ components:
     Job:
       type: object
       additionalProperties: false
-      required: [id, owner, label, revision, phase, lifecycle, source, target, authoritative_attempt, progress, checkpoint, result, failure, created_at, updated_at, event_cursor]
+      required: [resource_kind, id, owner, label, revision, phase, lifecycle, source, target, authoritative_attempt, progress, checkpoint, result, failure, created_at, updated_at, event_cursor]
       properties:
+        resource_kind:
+          const: job
         id:
           $ref: '#/components/schemas/OpaqueId'
         owner:
@@ -1210,6 +1381,44 @@ components:
         event_cursor:
           type: string
           minLength: 16
+    JobTombstone:
+      type: object
+      additionalProperties: false
+      required: [resource_kind, id, owner, target, terminal_phase, deletion_operation_id, created_at, hard_delete_started_at, updated_at, event_cursor]
+      properties:
+        resource_kind:
+          const: tombstone
+        id:
+          $ref: '#/components/schemas/OpaqueId'
+        owner:
+          $ref: '#/components/schemas/PrincipalId'
+        target:
+          $ref: '#/components/schemas/Target'
+        terminal_phase:
+          $ref: '#/components/schemas/TerminalJobPhase'
+        deletion_operation_id:
+          $ref: '#/components/schemas/OpaqueId'
+        created_at:
+          type: string
+          format: date-time
+        hard_delete_started_at:
+          type: string
+          format: date-time
+        updated_at:
+          type: string
+          format: date-time
+        event_cursor:
+          type: string
+          minLength: 16
+    JobResource:
+      oneOf:
+        - $ref: '#/components/schemas/Job'
+        - $ref: '#/components/schemas/JobTombstone'
+      discriminator:
+        propertyName: resource_kind
+        mapping:
+          job: '#/components/schemas/Job'
+          tombstone: '#/components/schemas/JobTombstone'
     JobPage:
       type: object
       additionalProperties: false
@@ -1218,7 +1427,7 @@ components:
         items:
           type: array
           items:
-            $ref: '#/components/schemas/Job'
+            $ref: '#/components/schemas/JobResource'
         next_cursor:
           type: [string, 'null']
         event_cursor:
@@ -1378,7 +1587,7 @@ components:
             - type: 'null'
         resolved_source_ref:
           oneOf:
-            - $ref: '#/components/schemas/OpaqueId'
+            - $ref: '#/components/schemas/DurableDescriptorRef'
             - type: 'null'
         target:
           $ref: '#/components/schemas/Target'
@@ -1388,7 +1597,7 @@ components:
           $ref: '#/components/schemas/OpaqueId'
         checkpoint_ref:
           oneOf:
-            - $ref: '#/components/schemas/OpaqueId'
+            - $ref: '#/components/schemas/DurableDescriptorRef'
             - type: 'null'
     ClaimResponse:
       type: object
@@ -1402,12 +1611,14 @@ components:
     ActivationResponse:
       type: object
       additionalProperties: false
-      required: [authority, execution]
+      required: [authority, execution, lease]
       properties:
         authority:
           $ref: '#/components/schemas/AttemptAuthority'
         execution:
           $ref: '#/components/schemas/ExecutionEnvelope'
+        lease:
+          $ref: '#/components/schemas/LeaseProjection'
     AttemptMutation:
       type: object
       required: [operation_id, fence, worker_incarnation]
@@ -1435,7 +1646,12 @@ components:
           required: [resolved_source_ref]
           properties:
             resolved_source_ref:
-              $ref: '#/components/schemas/OpaqueId'
+              allOf:
+                - $ref: '#/components/schemas/DurableDescriptorRef'
+                - type: object
+                  properties:
+                    kind:
+                      const: resolved_source
     AttemptCheckpointRequest:
       unevaluatedProperties: false
       allOf:
@@ -1444,7 +1660,12 @@ components:
           required: [checkpoint_ref]
           properties:
             checkpoint_ref:
-              $ref: '#/components/schemas/OpaqueId'
+              allOf:
+                - $ref: '#/components/schemas/DurableDescriptorRef'
+                - type: object
+                  properties:
+                    kind:
+                      const: checkpoint
     AttemptProgressRequest:
       unevaluatedProperties: false
       allOf:

docs/protocol/RemoraClaimActivation.cfg

@@ -22,6 +22,7 @@ INVARIANTS
     ConflictIsChangedRequest
     ReapedClaimHasNoActivationEffect
     ReapedCoordinationIsClean
+    RecoveryOwnsInactiveClaim
 
 PROPERTIES
     ActivationAppliesAtMostOnce

docs/protocol/RemoraClaimActivation.tla

@@ -163,7 +163,6 @@ RejectPrecondition(op, c, f, w) ==
 ExpireReservation(c) ==
     /\ durableState[c] = Authorized
     /\ reservation[c] # NoWorker
-    /\ lease[c] = NoWorker
     /\ reservation' = [reservation EXCEPT ![c] = NoWorker]
     /\ UNCHANGED <<durableState, attemptFence, attemptWorker, lease,
                     activationStage, durableLock, operationRequest,
@@ -185,6 +184,7 @@ ExpireLease(c) ==
 
 AcquireRecoveryLock(c) ==
     /\ durableState[c] = Authorized
+    /\ reservation[c] = NoWorker
     /\ durableLock[c] = NoOwner
     /\ durableLock' = [durableLock EXCEPT ![c] = Recovery]
     /\ UNCHANGED <<durableState, attemptFence, attemptWorker, reservation,
@@ -291,6 +291,10 @@ ReapedCoordinationIsClean ==
             /\ 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