Actor Suspension

Composition grounded on Final Critique 4 — 2026-06-10 4 invariants TLA+ model buggy twin ×1 regulated composes 3 atoms + 1 substrate

Derived card — generated from the corpus (status line, invariant headers, sibling formal-model files, Composes edges). The specification below is canonical. composition graph →

Table of contents

Actor Suspension

Summary

Actor Suspension is a regulated composition — a specification that wires several freestanding patterns together — that does one job thoroughly: when you need to cut off an actor (a departing employee, a hacked account, a contractor who’s done), it closes every door at once and leaves proof.

The problem it solves is the classic security gap where someone’s access is pulled in one place but not another — their login is disabled but a permission grant still works, or their role is removed but an open session keeps going. This composition makes that impossible by treating suspension as a single all-or-nothing action: it finds every active permission grant the actor holds and every active login session they have, revokes all of them together, marks the actor as suspended, and writes one tamper-proof audit record that lists every grant and session it revoked.

If any part of that can’t complete, the whole thing rolls back and nothing changes — because a half-suspended actor (some access cut, some not) is worse than one who wasn’t touched, since everyone would wrongly believe they were locked out. Optionally, it also revokes the actor’s login credential so they can’t sign back in.

It is the exact mirror of the Login pattern: Login wires up “check the credential, then start a session” on the way in; this wires up “suspend the actor, then revoke every grant and every session” on the way out. The composition’s defining emergent guarantee — a property that exists only when the patterns are combined — is that single multi-surface revocation: after a successful suspension, the actor provably holds zero active grants and zero active sessions, and the audit record names every one that was revoked. Its common uses are exactly the moments compliance regimes care about most: offboarding a terminated employee (the access must be removed promptly and provably), responding to a compromised account, and ending a third-party’s access. Any system that must deactivate an actor across multiple access surfaces at once — and prove from the records that nothing was missed — is a candidate for this composition.

Intent

Every system that distinguishes actors eventually has to un-distinguish one. An employee leaves; a credential is found in a paste dump; a contractor’s engagement ends; an account shows the signature of a takeover. The obligation that follows is deceptively simple to state and notoriously easy to botch: cut off every way that actor can still act, now, and be able to prove afterward that you did. The botch is always the same shape — access is revoked on one surface but not another. The session cookie is invalidated but the API token’s permission grant is still active; the role is removed but a long-lived session keeps working; the login credential is disabled but a service grant the actor still holds quietly authorizes a scheduled job. Each gap is a half-open door, and a half-suspended actor is more dangerous than an un-suspended one, because the system and its operators believe the actor is locked out.

This is the friction this composition exists to resolve, and naming it precisely keeps the composition honest: this composition is not an “account deactivation feature”; it is a multi-surface atomic de-authorization with a records-alone completeness proof. An actor’s ability to act is spread across two independent authorization surfaces that no single atom relates: Permissions holds the grants that say what the actor may do, and Session holds the live authenticated channels that say the actor is currently acting. Revoking one without the other leaves a door open. Worse, each surface has its own multiplicity — an actor may hold many grants (issued at different times, by different grantors) and many sessions (one per device) — so closure on each surface is itself an enumerate-then-revoke-each operation, exactly the mass-revocation pattern Permissions names as the composing system’s responsibility (“enumerate all active grants where grant.subject_ref = departing_subject, then call revoke(grant_id) for each”) and Session supports through its principal_ref-queryable store (“revoke all sessions for this account”). The structure that snapshots both surfaces, revokes every member of both, sets the actor’s suspension state, and seals the whole act as one attributed, tamper-evident record belongs to no single constituent. It belongs to the composition, and this composition is that structure.

this composition is Login’s mirror image, and the symmetry is load-bearing. Login is the inbound wiring: Credential.verify → Session.issue, with the emergent cascade that revoking a credential terminates the derived sessions. This composition is the outbound wiring: suspend → revoke every grant + revoke every session, with the emergent guarantee that suspension closes all surfaces at once. Login’s cascade walks an active-session set under a snapshot and tolerates partial completion (a per-session storage failure is logged and the cascade continues — partial revocation beats none). This composition makes the opposite default choice, and the difference is deliberate: a suspension that half-completes leaves an ambiguous security state, so this composition’s default is all-or-nothing under one transaction — the actor is either fully de-authorized or the operation visibly fails and is retried, never silently half-done. The same TOCTOU (time-of-check-to-time-of-use) race Login surfaced as finding Final Critique 1 in its Final Critique 4 — a concurrent terminal transition during the cascade — recurs here and is resolved the same way: a grant or session the cascade targets that another process already revoked is found already-terminal and counted, not re-revoked.

This is a composition, not a new primitive. Actor Identity, Permissions, Session, and Audit Trail are unchanged; this composition is the wiring that makes them coherent as one suspension surface. It introduces emergent actions — Suspend Actor, the read-only Suspension Report, and the thin Reinstate Actor — and an emergent state machine the constituents do not carry: the actor’s Active → Suspended lifecycle. Actor Identity is the attestation atom, with a single Attested state and no actor lifecycle (it explicitly defers actor registration, deactivation, and suspension to a forthcoming Actor Registry / Identity Provisioning pattern); the Active/Suspended state is therefore a composition-introduced surface This composition owns, not a state read from any constituent.

What the composition is not: it is not the issuance surface — it revokes grants and sessions but never issues them (Permissions.grant and Session.issue are called elsewhere), so it cannot, by itself, prevent a new grant or session being created for a suspended actor after the cascade snapshot (a named composing-layer obligation, exactly as Login’s cascade is snapshot-scoped); it is not the actor registry that provisions actor identities; it is not an authorization-policy engine deciding whether an actor should be suspended (that is wired ahead of Suspend Actor at the administrative / Multi-Party Approval layer); and it does not restore access on reinstatement — Reinstate Actor lifts the suspension state but never un-revokes a terminal grant or session (re-provisioning is the issuance layer’s job). Each is named explicitly in Edge cases.

Composes

Actor Identity — the identity of the actor being suspended. This composition introduces the actor’s Active → Suspended lifecycle as a composition-introduced state machine, because Actor Identity carries no lifecycle state of its own (a single Attested state, with actor registration / deactivation / suspension explicitly deferred to a forthcoming Actor Registry / Identity Provisioning pattern). The actor_ref is the suspension subject and the join key across the two authorization surfaces. This composition does not mutate any attestation (they are immutable — Actor Identity Invariant 1); the attestation surface enters via the Audit Trail substrate, which attests the actor.suspended event under the suspending operator’s credential.
Permissions — the grant surface, used in both directions. Read: Suspend Actor enumerates the actor’s active grants by querying the grant store for {grant_id} where subject_ref = actor_ref and status = Active (the grant store is queryable; Permissions’ Behavior section exposes per-grant fields to composing systems). Write: the cascade calls Permissions.revoke(grant_id) → ok | rejected(not-known | not-active | storage-failure) for each enumerated grant — Permissions provides no bulk-revoke surface, and naming the per-grant enumerate-then-revoke as the composing system’s responsibility is Permissions’ own Mass revocation on subject deprovisioning edge case. This composition is that composing system. A revoke reaching an already-not-active grant (a concurrent revocation) is the benign TOCTOU case (below), not an error.
Session — the live-channel surface, used in both directions. Read: Suspend Actor enumerates the actor’s active sessions by querying the session store for {session_token} where principal_ref = actor_ref and status = Active (Session’s store is principal_ref-queryable precisely to support “show all active sessions for this account” and “revoke all sessions for this account” administrative operations). Write: the cascade calls Session.revoke(session_token, revoked_by_ref = suspended_by_ref, reason) → revoked | rejected(invalid-request | already-terminal | not-known | storage-failure) for each active session. A session that became terminal between the snapshot and the revoke returns already-terminal — the benign TOCTOU case, counted as skipped exactly as Login’s Final Critique 4 (finding Final Critique 1) handles it.
Audit Trail — the regulated-audit substrate: this composition names it the way an atom is named and reaches Event Log, Actor Identity, Tamper Evidence, and Retention Window transitively through it (per the Compositions of compositions convention — see spec-format.md), maintaining one Audit Trail instance for all suspension events. This composition records the actor.suspended event by calling AuditTrail.record_action(action_ref, actor_ref, credential, data) → event_id | rejected(invalid-credential | invalid-request | recording-failure) directly on the one Audit Trail instance the substrate carries — the established substrate-composition pattern (Multi-Party Approval and Resolve a Person’s Data Rights record their own events on the Audit Trail their substrate carries). The capability is Audit Trail’s own declared record_action and its Invariant 1 (attribution coverage), reached through the named substrate — not an ambient reach-through. The event’s data carries the complete enumeration of every revoked grant_id and session_token (Invariant 2). The substrate seals the event (Tamper Evidence) and governs its retention (Retention Window) so the suspension record outlives the access it closed.
Credential (optional fifth constituent) — when composed, the cascade additionally calls Credential.revoke(credential_id, revoked_by_ref = suspended_by_ref, reason) → revoked | rejected(...) on the actor’s authentication credential so the suspended actor cannot re-authenticate to establish a new session. This closes the re-entry door the grant/session revocation alone leaves open (revoking current sessions does not stop a new login). When Credential is not composed, closing that door is a named composing obligation (the deployment revokes the credential through Login’s surface, or wires this composition with Credential). Including Credential makes this composition the full outbound counterpart to Login’s inbound Credential.verify → Session.issue.

The Permissions grant store, the Session store, and (when composed) the Credential store are owned by their respective constituent instances; the Event Log, Actor Identity attestation store, Tamper Evidence seal store, and Retention Window store are owned by the Audit Trail substrate. This composition owns no constituent state — it owns the emergent actor_suspension_state map and indexes the suspension events through the substrate.

A surface this composition needs that crosses the two authorization surfaces is the unified actor namespace: the actor_ref must be the same identity under which the actor holds Permissions grants (as subject_ref) and Session sessions (as principal_ref). This unification is the precise concept the Authenticated Actor composition establishes as a principal_ref ↔ actor_ref bijection, and the precise gap demos/attributed-permissions-admin/CORNERS.md §Cross-atom identity surface aliasing flags when it diverges. This composition names the unification as a deployment precondition (Configuration) — satisfied by Authenticated Actor as a named composing peer or by deployment convention — rather than composing Authenticated Actor directly; the enumeration’s correctness is conditional on it, an externally-clearable check (Generation acceptance).

Composition logic

Composition state

The composition owns emergent state that wires the constituents into one suspension surface. None of this state belongs to a single constituent.

actor_suspension_state — map from actor_ref to {state, suspended_at?, suspended_by_ref?, reason?, suspension_event_id?} where state ∈ {Active, Suspended}. An actor_ref absent from the map is treated as Active (the default — no suspension has been recorded). Populated/transitioned by Suspend Actor (Active → Suspended) and Reinstate Actor (Suspended → Active). This is the composition-introduced actor lifecycle the constituents do not carry. The suspension_event_id binds the Suspended state to the sealed actor.suspended Audit Trail event that enumerates what was revoked.

suspension_log — append-only record of every Suspend Actor and Reinstate Actor call, whether it transitioned, was a no-op, or failed. Each entry: entry_id (opaque, system-generated), actor_ref, operation (suspend reinstate), Outcome (suspended reinstated already-suspended already-active revocation-failure(surface) recording-failure invalid-request), Revoked Grants (the grant_id set, on success), Revoked Sessions (the session_token set, on success), suspension_event_id?, attempted_at. This is the composition’s composition-layer query surface; the Audit Trail substrate is the tamper-evident external-auditor record of the same suspension events. The two are redundant by design, exactly as Login pairs its login_event_log with the Audit Trail.

The actor’s grants live in the Permissions store, its sessions in the Session store, its (optional) credential in the Credential store, and the suspension events in the Audit Trail substrate. This composition duplicates none of them; it transitions the suspension state and binds each suspension to the sealed event that records the revoked set.

The enumerated active set for an actor_ref — its active grants and active sessions — is not stored as standing state; it is computed at suspension time by querying the Permissions and Session stores. The sealed actor.suspended event’s enumerated {revoked_grants, revoked_sessions} is the durable, records-alone snapshot of that set at suspension time.

Configuration

unified_actor_namespace — a deployment-declared precondition (default enforced) asserting that the actor_ref this composition suspends is the same identity value under which the actor holds Permissions grants (as subject_ref) and Session sessions (as principal_ref). This is the declaring source (capability provenance) for the enumeration’s correctness: this composition enumerates subject_ref = actor_ref grants and principal_ref = actor_ref sessions, which is complete only if the namespaces coincide. A deployment satisfies this via the Authenticated Actor principal_ref ↔ actor_ref binding (a named composing peer) or by convention; whether the namespaces actually coincide is an externally-clearable check (Generation acceptance). A deployment whose namespaces diverge under-enumerates and produces an incomplete suspension — the audit-gap the CORNERS finding flags.
revoke_credential_on_suspend — whether the cascade also revokes the actor’s authentication credential (requires the optional Credential constituent). Default true when Credential is composed; absent otherwise. When false or Credential is uncomposed, closing the re-authentication door is a named composing obligation (Edge cases — Re-authentication after suspension).
audit_trail_retention_policy — inherited, not re-configured. this composition records its actor.suspended / actor.reinstated events on the Audit Trail substrate, which carries the host’s regulatory retention policy; record_action takes the policy via the substrate’s configured value. The suspension events should persist at least as long as the longest retention obligation over the access they closed — often longer, for post-offboarding dispute defensibility (the access is gone; the proof it was lawfully closed must outlive it).
partial_failure_posture — all-or-nothing (default) or best-effort. The default rolls the whole cascade back on any constituent revoke failure (no partial state — Invariant 1). best-effort (the Login-style posture, for deployments that prefer maximal closure over atomicity) continues the cascade on a per-surface failure, records the failure, and surfaces a revocation-failure(surface) finding — explicitly weakening Invariant 1 to snapshot-scoped-best-effort. The default is all-or-nothing precisely because a half-suspended actor is a worse security state than a cleanly-failed one.

Primitive policies

actor_ref — opaque reference to the actor being suspended; the key of actor_suspension_state and the join key (= subject_ref = principal_ref under unified_actor_namespace). Must contain at least one non-whitespace character (invalid-request). Byte-identity equality; never normalized.
suspended_by_ref — non-empty reference to the operator performing the suspension; flows to Session.revoke (as revoked_by_ref), Credential.revoke (as revoked_by_ref), and AuditTrail.record_action (as actor_ref), so the records attribute the suspension to one operator. Whether suspended_by_ref is authorized to suspend actors is a named composing concept (Edge cases — Suspension authorization), exactly as Login leaves logout authorization to a composing layer.
credential — the suspending operator’s opaque credential, consumed by AuditTrail.record_action (and the Actor Identity reached through the substrate) to attest the suspension event; never persisted by this composition.
reason — non-empty string naming why the actor is suspended; carried into each Session.revoke / Credential.revoke reason and the actor.suspended event. Mandatory (a suspension without a stated reason is a compliance finding — Permissions, Session, and Credential each require a non-empty reason on revoke).
grant_id / session_token / credential_id — opaque constituent handles surfaced by the enumeration; passed to the respective revoke. Opaque; never normalized.

No primitive is case-sensitivity-normalized at the composition layer; deployments wanting normalization wire it at the calling layer before invoking composition actions.

Action wiring

The composition exposes three actions: one emergent multi-surface suspension (Suspend Actor), one read-only query (Suspension Report), and one thin lifecycle-reversal (Reinstate Actor).

Uniform constituent-rejection mapping. Each constituent revoke maps its rejection taxonomy as named per step. Under the all-or-nothing posture, any non-benign revoke failure aborts the transaction and rolls back (no partial state); under best-effort, it is recorded and the cascade continues. A Permissions.revoke → not-active or Session.revoke → already-terminal is benign in both postures — the target is already terminal, which is the cascade’s goal (the TOCTOU already-terminal case), counted as skipped, never an abort.

`suspend_actor`

suspend_actor(actor_ref, suspended_by_ref, credential, reason) →
  {suspended, revoked_grants, revoked_sessions, revoked_credential?, event_id}
 | rejected(
   invalid-request
  | already-suspended
  | revocation-failure
  | recording-failure
  )

Suspends an actor by atomically revoking every active Permissions grant and every active Session (and, optionally, the actor’s Credential), transitioning the actor to Suspended, and sealing the complete revoked set into one attributed Audit Trail event. Steps:

Validate: actor_ref, suspended_by_ref, credential, reason each non-empty. Any violation → append suspension_log {operation: suspend, outcome: invalid-request}; return rejected(invalid-request). Stop.
Suspension-state gate (Active → Suspended; the cascade ordering, Invariant 3). Read actor_suspension_state[actor_ref]. If state = Suspended → append suspension_log {outcome: already-suspended}; return Already Suspended and change no state — the cascade does not re-run (no-op on already-Suspended; the second suspension is idempotent). An actor_ref absent from the map is Active and proceeds.
Snapshot the active set (read-only, atomic with the cascade). Enumerate the actor’s active grants G = {grant_id : subject_ref = actor_ref ∧ status = Active} from the Permissions store and active sessions S = {session_token : principal_ref = actor_ref ∧ status = Active} from the Session store. The snapshot read and the cascade writes in steps 4–6 are one serialized transaction keyed on actor_ref (the host transaction boundary, exactly as Login’s cascade and Audit Trail’s cascade-on-purge commit in one transactional boundary), so no concurrently-issued grant or session is half-covered: a grant/session created after the snapshot is not in G/S and is not covered by this suspension (snapshot-scoped — Invariant 1’s stated bound, and the Suspension is snapshot-scoped edge case). An empty G and S is a valid suspension (an actor with no active access is still recorded as Suspended) — distinct from any failure.
Cascade — revoke every member of both surfaces (and optionally the credential). Within the transaction:
- For each grant_id ∈ G: Permissions.revoke(grant_id). ok → add to Revoked Grants. not-active (a concurrent revocation already terminalized it) → benign, add to Revoked Grants (the goal is met). not-known → an enumeration/store inconsistency (a grant the query returned but the store no longer knows — structurally near-impossible, since Permissions never deletes grants, Invariant 10): treated as a non-benign failure, handled exactly as storage-failure — abort and return rejected(revocation-failure) under all-or-nothing, or record revocation-failure(permissions) and continue under best-effort — and additionally surfaced as a high-priority store-inconsistency finding in suspension_log. storage-failure → abort under all-or-nothing (roll back; the grant stays whatever it was), or record revocation-failure(permissions) and continue under best-effort.
- For each session_token ∈ S: Session.revoke(session_token, revoked_by_ref = suspended_by_ref, reason). revoked → add to Revoked Sessions. already-terminal (the TOCTOU already-terminal case — a concurrent logout/expiry/cascade terminalized it) → benign, add to Revoked Sessions. not-known → enumeration/store inconsistency (structurally near-impossible — Session is durable, Invariant 9): a non-benign failure handled exactly as the grant case — abort and return rejected(revocation-failure) under all-or-nothing, or record revocation-failure(session) and continue under best-effort — and surfaced as a high-priority store-inconsistency finding in suspension_log. storage-failure → abort under all-or-nothing, or record revocation-failure(session) and continue under best-effort.
- If revoke_credential_on_suspend and Credential is composed: Credential.revoke(credential_id, revoked_by_ref = suspended_by_ref, reason). revoked → set revoked_credential = credential_id. already-terminal → benign (already revoked/rotated/expired). storage-failure → abort / record per posture.
Transition and bind (still within the transaction). Set actor_suspension_state[actor_ref] = {state: Suspended, suspended_at: now, suspended_by_ref, reason, suspension_event_id: <pending>}.
Seal the act — record_action carrying the complete enumeration (Invariant 2). Call AuditTrail.record_action(action_ref = actor.suspended, actor_ref = suspended_by_ref, credential, data = {suspended_actor: actor_ref, revoked_grants, revoked_sessions, revoked_credential?, reason, suspended_at = now}) → event_id; set suspension_event_id = event_id. The data carries the complete revoked set (or, for a very large set, a cryptographic digest of it — mechanism-neutral exactly as Immutable Transaction Ledger/Resolve a Person’s Data Rights treat their large payloads), so the enumeration is sealed and tamper-evident: a later silent edit to the recorded set breaks the seal. Map the substrate’s rejection: invalid-credential / invalid-request / recording-failure → abort under all-or-nothing (roll back the whole cascade — the suspension never happened, retry against intact state) and return rejected(recording-failure); under best-effort the revokes have already committed and the orphan (revoked access with no sealed suspension event) is handled per the Cross-store consistency under partial failure edge case.
Commit the transaction. Append suspension_log {operation: suspend, outcome: suspended, revoked_grants, revoked_sessions, suspension_event_id: event_id}. Return {suspended, revoked_grants, revoked_sessions, revoked_credential?, event_id}. The actor is now Suspended with zero active grants and zero active sessions (Invariant 1).

`suspension_report` (read-only)

suspension_report(actor_ref) →
  {state, suspended_at?, suspended_by_ref?, reason?, revoked_grants?, revoked_sessions?, suspension_event_id?}
 | rejected(invalid-request)

The read-only surface an auditor, operator, or the actor themselves uses to read an actor’s suspension status and, if Suspended, the complete set that was revoked. Resolves actor_suspension_state[actor_ref]: absent or Active → {state: Active}; Suspended → the full suspension record including suspended_at, suspended_by_ref, reason, the suspension_event_id, and the enumerated Revoked Grants / Revoked Sessions (read from the sealed event the suspension_event_id binds, the authoritative record). No Audit Trail event is produced — a pure read. Logging who read a suspension report belongs to a composing access-log concept, named rather than absorbed.

`reinstate_actor`

reinstate_actor(actor_ref, reinstated_by_ref, credential, reason) →
  {reinstated, event_id}
 | rejected(invalid-request | already-active | recording-failure)

Lifts an actor’s suspension by transitioning Suspended → Active and recording an attributed actor.reinstated event. It does not restore any revoked grant or session — those are terminal in their constituents (Permissions Invariant 3, Session Invariant 4) and cannot be un-revoked; re-authorizing the actor means issuing fresh grants and sessions through the issuance layer, which is not this composition’s surface. Steps: validate inputs (invalid-request); if state ≠ Suspended → Already Active (no-op); else record AuditTrail.record_action(action_ref = actor.reinstated, actor_ref = reinstated_by_ref, credential, data = {reinstated_actor: actor_ref, reason, reinstated_at = now}) → event_id, then set actor_suspension_state[actor_ref] = {state: Active} (atomic with the event); append suspension_log; return {reinstated, event_id}. Reinstatement is the state-machine’s reverse edge only — re-provisioning access is the composing layer’s job (Edge cases — Reinstatement does not restore access).

The load-bearing wiring decision — multi-surface revocation is atomic and complete; suspension gates the cascade

The composition’s structural reason to exist has two halves.

Half 1 — every active grant and every active session is revoked in one all-or-nothing transaction. Suspend Actor snapshots both authorization surfaces, revokes every member of both (and optionally the credential), transitions the actor to Suspended, and seals the complete revoked set — all in one transaction; on any non-benign failure the whole act rolls back.

Principle. An actor’s ability to act is spread across two independent surfaces (grants and sessions), each with its own multiplicity; closing the actor out requires closing both surfaces completely, and a partial close is a worse state than no close because it is invisible. Likely objection: why not revoke grants and sessions independently — let an admin call Permissions.revoke per grant and Session.revoke per session — rather than wrapping them in one composition action? Mechanism that resolves it: because independent revocation has no completeness guarantee and no atomicity — an admin who revokes the grants but forgets a session, or whose session-revocation step fails midway, leaves a half-open actor and no record that the closure was incomplete. This composition snapshots both surfaces, revokes every enumerated member within one transaction keyed on actor_ref, and, on any non-benign constituent failure, rolls the whole cascade back (the all-or-nothing default) — so the post-condition is crisp: the actor is either fully de-authorized (zero active grants, zero active sessions) or unchanged and the operation visibly failed. A benign already-terminal target (a concurrent revocation) is counted toward the goal, not treated as a failure, so a TOCTOU race does not spuriously abort. Result: after Suspend Actor returns success, the actor provably holds zero active grants and zero active sessions, committed atomically — the multi-surface completeness no single constituent provides, and the opposite of Login’s deliberately best-effort cascade because suspension’s failure mode (a half-open door) is more dangerous than its retry cost.

Half 2 — the Active→Suspended transition gates the cascade, and the sealed event records exactly what was closed. The cascade runs only on the Active→Suspended edge (a second suspension is a no-op), and the actor.suspended event enumerates every revoked grant_id and session_token.

Principle. The suspension must be idempotent (running it twice must not double-revoke or produce two conflicting records) and its completeness must be provable from the records alone. Likely objection: doesn’t recording the whole revoked set duplicate what the Permissions and Session stores already show (each revoked grant/session carries its own revoked_at)? Mechanism that resolves it: the per-constituent revocation records show that each grant/session was revoked, but only the composition knows they were revoked as one suspension act and which set constituted “the actor’s access at suspension time.” The Active→Suspended gate (step 2) makes the cascade fire exactly once — a second Suspend Actor sees Suspended and returns already-suspended without re-running — and the sealed actor.suspended event binds the complete {revoked_grants, revoked_sessions} enumeration into one tamper-evident record, so an auditor reads one event and sees the whole closure, not a scatter of independently-revoked records they must reassemble and hope is complete. Result: the suspension is idempotent (gated on the state transition) and its completeness is records-alone provable (the sealed enumeration), resting on the substrate’s Tamper Evidence so a later attempt to shrink the recorded set to hide a missed surface breaks the seal.

Composition-level invariants

These invariants emerge from the composition; none belongs to a single constituent. Each invariant’s Rests on: clause is its capability-provenance record (see pressure-testing.md §Capability provenance): every clause traces to a declared source — a named constituent invariant or action, a deployment-declared configuration capability, or a composition-introduced surface this composition owns.

Invariant 1 — Atomicity of multi-surface revocation (load-bearing). After suspend_actor(actor_ref, …) returns success, the actor holds zero active grants (no Active Permissions grant with subject_ref = actor_ref) and zero active sessions (no Active Session with principal_ref = actor_ref) over the snapshot taken in step 3, and the transition + cascade + sealed event committed as one transaction — there is no reachable success state in which the actor is Suspended while an enumerated grant or session remains Active. Snapshot-scoped, modulo concurrent issuance: a grant or session created after the step-3 snapshot is not covered by this suspension (the composition revokes but never issues, so it cannot block a concurrent Permissions.grant / Session.issue); closing that gap is the composing-layer obligation to gate issuance on actor_suspension_state (Edge cases — Suspension is snapshot-scoped), exactly as Login’s cascade is snapshot-scoped. Under the all-or-nothing posture, a non-benign constituent-revoke or audit-write failure rolls the whole cascade back, so a failed Suspend Actor leaves the actor unchanged (not partially suspended). This is the load-bearing concurrency/atomicity claim and the formal-model subject; the model verifies that the atomic cascade admits no Suspended-with-active-access state, and the buggy twin shows a non-atomic multi-surface revocation reaches exactly that partial state. Rests on: Permissions revoke + Invariant 2 (status monotonicity Active→Revoked) + Invariant 8 (revoked grants confer no permission); Session revoke + Invariant 4 (revocation absorbing); the Permissions subject_ref-queryable grant store and Session principal_ref-queryable session store (the enumeration capabilities both atoms declare); the composition-introduced one-transaction cascade (Action wiring steps 3–7) and the unified_actor_namespace configuration capability (the enumeration’s join correctness).
Invariant 2 — Audit completeness. Every successful Suspend Actor produces exactly one actor.suspended Audit Trail event whose data enumerates every grant_id in Revoked Grants and every session_token in Revoked Sessions (and revoked_credential when applicable) — the complete set the cascade closed, with no revoked surface omitted from the record. The enumeration is part of the sealed event payload, so an auditor can confirm the suspension’s completeness from one tamper-evident record. Defended in-line: step 6 carries the complete {revoked_grants, revoked_sessions} (or its digest) into the record_action data, committed in the same transaction as the revokes (step 7). Rests on: Audit Trail record_action and Invariant 1 (attribution coverage) reached through the named substrate, the substrate’s Tamper Evidence sealing (so the enumeration cannot be silently shrunk), and the composition-introduced cascade that assembles the complete set before sealing.
Invariant 3 — Suspension cascade ordering. The cascade runs only on the Active → Suspended transition: Suspend Actor against an actor already in Suspended returns already-suspended and changes no state (no second cascade, no second event, no double-revoke), and the suspension state is monotonic on the suspend edge (an Active actor with a recorded suspension is Suspended until Reinstate Actor explicitly reverses it). The benign TOCTOU case — a grant/session the cascade targets that a concurrent process already terminalized — is counted toward completion (not-active/already-terminal → skipped, not aborted), mirroring Login’s Final Critique 4 (finding Final Critique 1) already-terminal handling. Defended in-line: step 2’s state gate rejects an already-Suspended actor before any cascade; step 4 treats already-terminal targets as benign. Rests on: the composition-introduced actor_suspension_state gate (Action wiring step 2) and the benign-already-terminal mapping (step 4), with the terminal-target semantics resting on Permissions Invariant 3 (revocation terminal) and Session Invariant 5 (terminal-state absorbing).
Invariant 4 — Constituent invariants preserved. All Permissions invariants (1–10) hold over the grant store, all Session invariants (1–11) hold over the session store, all Actor Identity invariants (1–9) hold over the attestation store, all Audit Trail composition-level invariants (1–8) hold over the substrate (and transitively all Event Log, Retention Window, and Tamper Evidence invariants), and — when composed — all Credential invariants (1–11) hold over the credential store. This composition weakens no constituent invariant; it revokes through each constituent’s own revoke and records through the substrate’s own record_action. Rests on: each constituent’s own Generation acceptance bar over its store instance.

Invariant 1 (atomic multi-surface revocation) is the emergent guarantee the composition exists to provide; Invariant 2 (audit completeness) is what makes that guarantee provable from one sealed record; Invariant 3 (cascade ordering) makes the suspension idempotent and orders the cascade behind the state transition. Invariant 4 preserves every constituent guarantee underneath.

Examples

Walkthrough — offboarding a departing employee, end to end

A bank deploys this composition over its access surfaces with unified_actor_namespace = enforced (the actor_ref is the employee’s directory identity, used as subject_ref for grants and principal_ref for sessions, bound via Authenticated Actor), partial_failure_posture = all-or-nothing, Credential composed with revoke_credential_on_suspend = true, and the substrate’s audit_trail_retention_policy = sox_7_year.

Suspension trigger. An employee resigns; HR’s offboarding workflow calls suspend_actor(actor_ref = "emp_4821", suspended_by_ref = "hr_offboard_svc", credential = <svc-cred>, reason = "employment-ended-2026-06-10").
State gate. actor_suspension_state["emp_4821"] is absent → Active → proceed (Invariant 3).
Snapshot. The Permissions store yields three active grants for subject_ref = "emp_4821": g_finread, g_wireinit, g_reports. The Session store yields two active sessions for principal_ref = "emp_4821": tok_laptop, tok_phone. The snapshot and the cascade below run in one transaction keyed on emp_4821.
Cascade. Permissions.revoke(g_finread) → ok; revoke(g_wireinit) → ok; revoke(g_reports) → ok (revoked_grants = {g_finread, g_wireinit, g_reports}). Session.revoke(tok_laptop, "hr_offboard_svc", "employment-ended-2026-06-10") → revoked; revoke(tok_phone, …) → revoked (revoked_sessions = {tok_laptop, tok_phone}). Credential.revoke(cred_emp4821, "hr_offboard_svc", …) → revoked (revoked_credential = cred_emp4821).
Transition + seal. actor_suspension_state["emp_4821"] = {Suspended, suspended_at, suspended_by_ref: "hr_offboard_svc", reason}; AuditTrail.record_action(actor.suspended, "hr_offboard_svc", <svc-cred>, data = {suspended_actor: "emp_4821", revoked_grants: {g_finread, g_wireinit, g_reports}, revoked_sessions: {tok_laptop, tok_phone}, revoked_credential: cred_emp4821, reason}) → ev_susp_001. Transaction commits.
Result. Returns {suspended, revoked_grants (3), revoked_sessions (2), revoked_credential, event_id: ev_susp_001}. emp_4821 now holds zero active grants and zero active sessions (Invariant 1); Permissions.permitted("emp_4821", "wire:initiate") → denied; Session.validate(tok_laptop) → invalid(revoked); and the revoked credential blocks re-authentication.

Domain example — compromised account, all-or-nothing abort and retry

A security team suspends a compromised account: suspend_actor("svc_8830", "soc_analyst_k", <cred>, "credential-in-paste-dump"). The snapshot finds five grants and one long-lived session. Mid-cascade, Session.revoke(tok_svc) returns storage-failure (the session store is briefly unreachable). Under all-or-nothing, the whole transaction rolls back: the five grant revocations are undone, the suspension state is not set, and suspension_log records {outcome: revocation-failure(session)}. Suspend Actor returns Revocation Failure. The account is left exactly as it was — not half-suspended — and the SOC (Security Operations Center) retries once the session store recovers, at which point the suspension completes atomically. The crisp post-condition (fully suspended or unchanged) is the all-or-nothing posture’s entire point.

Rejection path — already-suspended no-op, and the benign TOCTOU race

Already suspended (idempotent no-op). A retry of the offboarding call: suspend_actor("emp_4821", …) → step 2 finds state = Suspended → rejected(already-suspended); no second cascade, no double-revoke, no second event (Invariant 3). The single suspension from the first call stands.
Benign TOCTOU — concurrent logout during the cascade. While suspend_actor("emp_4821", …) is mid-cascade, the employee’s laptop client fires its own Session.revoke(tok_laptop) (a logout). The cascade’s Session.revoke(tok_laptop, …) then returns already-terminal — the session is already terminal, which is the cascade’s goal. This composition counts tok_laptop in Revoked Sessions (the surface is closed) and does not abort. This mirrors Login’s Final Critique 4 (finding Final Critique 1) already-terminal handling: a concurrent terminal transition during the cascade is benign, not a failure.

Regulated adversarial scenarios

Three scenarios the composition must survive in regulated contexts.

Regulator audit — “prove this terminated employee’s access was fully and promptly removed.” A SOX (Sarbanes-Oxley Act) auditor examines emp_4821’s offboarding. suspension_report("emp_4821") returns Suspended with suspended_at, suspended_by_ref, and the enumerated Revoked Grants (3) and Revoked Sessions (2). The auditor reads the sealed actor.suspended event ev_susp_001 and confirms, via AuditTrail.verify_record, that the enumeration was not altered after the fact (Invariant 2, resting on the substrate’s Tamper Evidence). For each enumerated grant_id, the Permissions store shows status = Revoked with revoked_at at suspension time; for each session_token, the Session store shows Revoked. Invariant 1 is the structural answer: a Suspended actor has zero active grants and zero active sessions. The examiner consults no source code — every claim is verified from the records.

Disputed action — “this employee couldn’t have done that; we suspended them.” An action attributed to emp_4821 is dated after suspended_at. The investigator reads ev_susp_001: the suspension revoked every active grant and session at suspended_at, atomically (Invariant 1). If the disputed action used a session, Session.validate on that token returns invalid(revoked) with revoked_at at suspension time — the session could not have authorized an action afterward. If it used a grant, Permissions.permitted returns denied. The only way the action could post-date the suspension is a new grant/session issued after the snapshot — which Suspension Report plus the issuance records would show, and which is the named snapshot-scoped gap (the composing layer’s obligation to gate issuance on the suspension state). The records bound the question precisely.

Breach investigation — “during the incident, was any suspended actor’s access incompletely closed?” An investigator suspects a suspension half-completed under load. They walk the actor.suspended events in the incident window and, for each, cross-check that every enumerated grant_id/session_token is terminal in its store and that no active grant/session for that actor_ref exists outside the enumerated set as of suspended_at. Invariant 1 forecloses a Suspended-with-active-access state under the all-or-nothing posture: a half-suspended actor is not a reachable success state (the formal model verifies this; the buggy twin shows the non-atomic alternative reaches it). A deployment running best-effort would instead surface revocation-failure(surface) findings in the suspension_log — the honest record of any surface that did not close, which the investigator reads directly. Because the enumeration is in the sealed event payload, an attempt to shrink it to hide a missed surface breaks the seal.

Generation acceptance

A derived implementation of this composition is acceptable — in the regulator-acceptance sense — when an external auditor, given the composition’s emergent state (actor_suspension_state, suspension_log) plus the Permissions, Session, (optional) Credential, and Audit Trail substrate stores, can do all of the following without recourse to source code, runbooks, or developer narration.

Audit-Trail-traversal-clearable checks

These checks an auditor answers by reading the composition’s records (including the Audit Trail substrate reached through it).

Suspension completeness (the multi-surface guarantee). For every actor in actor_suspension_state with state = Suspended, confirm that no Permissions grant with subject_ref = actor_ref is Active and no Session with principal_ref = actor_ref is Active — except grants/sessions whose granted_at/issued_at post-dates suspended_at (the snapshot-scoped concurrent-issuance gap, a composing-layer obligation, not a defect of this composition). A Suspended actor with an active grant or session issued before suspended_at is a conformance failure (Invariant 1).
Audit enumeration completeness. For every Suspended actor, confirm exactly one actor.suspended event carries its suspension_event_id, that AuditTrail.verify_record returns verified for it, and that the event’s enumerated Revoked Grants / Revoked Sessions exactly equals the set of grants/sessions for that actor_ref showing revoked_at = suspended_at. A revoked-at-suspension grant or session absent from the sealed enumeration is a conformance failure (Invariant 2). The inverse: every grant_id/session_token in the enumeration resolves to a Revoked record.
Idempotence and ordering. Confirm the suspension_log shows at most one outcome: suspended per actor_ref between reinstatements, and that any Suspend Actor against an already-Suspended actor recorded already-suspended with no corresponding second actor.suspended event (Invariant 3). Confirm actor_suspension_state transitions only Active→Suspended (via Suspend Actor) and Suspended→Active (via Reinstate Actor), each bound to a sealed event.
Attribution and reason completeness. For every actor.suspended event, confirm it is attributed (via the substrate’s Actor Identity) to the suspended_by_ref and carries a non-empty reason, and that each revoked Session and (optional) Credential record carries the same suspended_by_ref and reason. A suspension with no attributed operator or no reason is a conformance failure.
Constituent Generation acceptance bars. Verify Permissions’ five checks over the grant store, Session’s five checks over the session store, Audit Trail’s six checks over the substrate (transitively clearing Event Log, Actor Identity, Tamper Evidence, Retention Window), and — when composed — Credential’s six checks. This composition’s invariants depend on the correctness of the constituents’ invariants (Invariant 4).

Externally-clearable checks

These questions arise around this composition but cannot be answered from its records alone — they are the composition’s named audit-gaps, each routed to the evidence that owns it.

Whether the actor_ref namespace truly coincides with the grant subject_ref and session principal_ref namespaces. This composition’s enumeration (and hence Invariant 1’s completeness) is complete only under unified_actor_namespace; whether the deployment actually unified them — via Authenticated Actor’s binding or convention — requires the deployment’s identity-namespace evidence, not this composition’s records. This is the load-bearing enumeration-completeness audit-gap (Edge cases — Unified actor namespace is a precondition); a divergent namespace under-enumerates silently.
Whether a new grant or session was issued after the suspension snapshot. Invariant 1 is snapshot-scoped; whether the composing layer correctly gated Permissions.grant / Session.issue on the suspension state (so a suspended actor acquired no new access) requires the issuance layer’s records, not this composition’s (Edge cases — Suspension is snapshot-scoped).
Whether the suspended_by_ref was authorized to suspend the actor. This composition attributes who suspended but does not gate whether they were permitted to; that requires a Permissions instance scoped to suspension authority (Edge cases — Suspension authorization).
Whether re-authentication was actually blocked. When Credential is uncomposed or revoke_credential_on_suspend = false, whether the deployment closed the re-authentication door requires the credential/Login records, not this composition’s (Edge cases — Re-authentication after suspension).

Edge cases and explicit non-goals

Suspension is snapshot-scoped; concurrent issuance is a composing-layer gap. Invariant 1’s completeness holds over the active set enumerated at the step-3 snapshot. This composition revokes but never issues; it cannot prevent a concurrent Permissions.grant or Session.issue from creating new access for the actor after the snapshot. This is the exact analog of Login’s snapshot-scoped cascade (Login Invariant 2): the composing layer that issues grants and sessions must gate issuance on actor_suspension_state (refuse to issue for a Suspended actor), which this composition exposes as a queryable surface (Suspension Report). This composition closes the actor’s existing access atomically; keeping it closed against new issuance is the issuance layer’s obligation, and whether it did so is an externally-clearable check. A deployment that wants the suspension to be self-enforcing wires the issuance gate; this composition provides the state the gate reads.
Unified actor namespace is a precondition, not a guarantee. This composition enumerates subject_ref = actor_ref grants and principal_ref = actor_ref sessions; this is complete only if the three namespaces coincide. The composition names this as a deployment precondition (unified_actor_namespace, satisfied by Authenticated Actor’s principal_ref ↔ actor_ref binding or by convention) rather than verifying it — verifying that two opaque namespaces coincide is not a records-alone check at this composition’s layer. A deployment whose namespaces diverge under-enumerates and produces a suspension that misses the actor’s access under the other namespace — the precise gap demos/attributed-permissions-admin/CORNERS.md §Cross-atom identity surface aliasing flags, here named as an externally-clearable check rather than papered over.
All-or-nothing vs. best-effort — a deliberate inversion of Login’s choice. Login’s cascade is best-effort (a per-session storage failure is logged and the cascade continues; partial revocation beats none). This composition’s default is all-or-nothing (a non-benign failure rolls the whole cascade back). The inversion is deliberate and defended: Login is adding a constraint (revoking sessions on a credential already revoked), so more closure is strictly better; this composition is establishing a security post-condition (the actor is locked out), and a half-established post-condition is a false belief that is worse than a clean failure. A deployment that prefers Login’s maximal-closure posture sets partial_failure_posture = best-effort, which explicitly weakens Invariant 1 to snapshot-scoped-best-effort and surfaces revocation-failure(surface) findings — the honest record of any surface that did not close.
Cross-store consistency under partial failure (best-effort posture). Under all-or-nothing, the cascade is one transaction and there is no partial state — a failure rolls back. Under best-effort (or where the constituent stores genuinely cannot share a transaction, e.g. distributed deployments), the revokes may commit before the actor.suspended write fails, leaving revoked access with no sealed suspension event — an orphan. The implementation (a) retries the record_action until it lands, (b) surfaces the actor and the already-revoked set as a high-priority finding in suspension_log, and (c) marks the recovered event cascade_recovery = true so an auditor distinguishes a clean suspension from a recovered one. This mirrors Resolve a Person’s Data Rights’ two-layer orphan discipline; the difference is that this composition’s grant/session revocations are not irreversible in the spoliation sense (a revoked grant is a terminal record, not a destroyed one), so the orphan is an audit-completeness gap, not a data-loss gap.
Reinstatement does not restore access. Reinstate Actor lifts the Suspended state but never un-revokes a grant or session — those are terminal in Permissions (Invariant 3) and Session (Invariant 4) and cannot return to Active. Re-authorizing a reinstated actor means issuing fresh grants (Permissions.grant) and letting them establish new sessions (Login), which is the issuance layer’s surface, not this composition’s. Reinstatement is the state-machine’s reverse edge only — it re-opens the actor to future provisioning; it does not reach back into the constituents’ terminal records. A deployment that needs the old access back re-grants it explicitly, which is the correct, auditable behavior (the new grants carry new granted_at timestamps and their own attributions).
Suspension authorization is a composing concept. Whether the suspended_by_ref is authorized to suspend a given actor is an inward-authorization question this composition does not gate — it composes no Permissions instance scoped to suspension authority (the cut is Actor Identity + Permissions-as-revocation-target + Session + Audit Trail). The operator is attributed cryptographically via the substrate’s Actor Identity, so an auditor can always answer who suspended the actor; whether they were permitted to requires a Permissions check (or a Multi-Party Approval gate for high-stakes suspensions) wired ahead of Suspend Actor, exactly as Resolve a Person’s Data Rights leaves operator authorization to a composing pattern.
Re-authentication after suspension. Revoking the actor’s active grants and sessions closes their current access but does not, by itself, stop a new login that would establish a fresh session. Closing that door is the optional Credential constituent’s job (revoke_credential_on_suspend = true revokes the authentication credential so re-authentication fails — Credential Invariant 4). When Credential is uncomposed, the deployment must revoke the credential through Login’s surface (Credential.revoke then optionally revoke_sessions_for_credential) in parallel — a named composing obligation, with whether it did so an externally-clearable check.
No bulk constituent surfaces — the cascade enumerates and revokes each. Permissions provides no bulk-revoke (its Mass revocation edge case names per-grant enumerate-then-revoke as the composing system’s job) and Session’s bulk revocation is likewise an enumerate-and-revoke over its principal_ref-queryable store. This composition is the composing pattern that performs both enumerations and the per-member revocations within one transaction — which is exactly why the atomicity and completeness guarantees (Invariants 1 and 2) live at the composition layer and not in either atom.
The actor lifecycle is composition-introduced. Actor Identity has a single Attested state and no actor lifecycle; the Active/Suspended state machine is this composition’s own (a composition-introduced surface). This composition therefore does not — and cannot — read a “suspended” flag from Actor Identity; it owns actor_suspension_state. A deployment that also wants the actor’s attestation registry entry deactivated (so the actor cannot produce new attestations) composes that through the forthcoming Actor Registry / Identity Provisioning pattern, or — for the attest surface specifically — through Authenticated Actor, whose revocation cascade closes the attest surface when the credential is revoked. This composition + Authenticated Actor + Credential-revocation together close the full outbound surface (grants, sessions, attestation, re-authentication); this composition alone closes grants and sessions.
Suspending an actor with no active access. An actor_ref with no active grants and no active sessions (a typo, or an actor already de-provisioned) is a valid no-op suspension: the cascade revokes nothing, the actor transitions to Suspended, and the actor.suspended event records empty Revoked Grants/Revoked Sessions. This is meaningful (“we suspended an actor who held no active access”) and harmless; it is distinct from a failure. This composition does not reject it, mirroring Login’s revoke_sessions_for_credential returning {revoked: 0} for a credential with no sessions.
Concurrency. Two concurrent Suspend Actor calls for the same actor_ref are serialized by the transaction keyed on actor_ref and the Active→Suspended gate: the first transitions and cascades; the second observes Suspended and returns already-suspended (Invariant 3). The benign TOCTOU race — a concurrent Session.revoke/logout or Permissions.revoke terminalizing a target the cascade also targets — is counted as skipped (already-terminal/not-active), not aborted, mirroring Login’s Final Critique 4 (finding Final Critique 1). A concurrent Permissions.grant/Session.issue after the snapshot is the snapshot-scoped gap above.
Clock semantics. suspended_at, reinstated_at, and attempted_at are best-effort wall-time annotations read from the substrate’s clock authority at record time (injected by the Audit Trail substrate, not sampled inside this composition’s transition — logic-confinement, inherited from the substrate). The Event Log sequence_number (via the substrate) is the authoritative order source for the suspension events. The cascade’s correctness depends on the snapshot/transaction serialization, not on clock comparison.

Terms

The canonical concepts this spec refers to. Each [Term] marker in the prose above links to its card here. A card states what the concept is, in plain English, plus its Kind — one of four: Type (a thing or category), Operation (a behavior), Member (a value of an enumerated Type), or, for a named datum, Field (a datum a Type carries — what does it carry?) or Parameter (a value an Operation needs — what does it need?). A card also names the Type it is a Member of / Field of, the Operation it is a Parameter of, and its Role where the domain assigns one. A card carries one Projects line — the concept’s single canonical lowering token, the one place the concrete name stays visible on the page — for every Field, Parameter, and pinned/wire Member. Everything else about casing (each target’s snake / camel / pascal / const / wire form) is derived from that one token by tools/harness/term-adapter.mjs, never hand-written. This is a composition, so its own concepts are the three emergent actions it exposes (Suspend Actor, Suspension Report, Reinstate Actor) — none belonging to a single constituent — the audit-completeness enumeration the suspend event carries (Revoked Grants, Revoked Sessions), the suspension_log classification it records (Outcome), and its own rejections (Already Suspended, Revocation Failure, Already Active). The composition also introduces an Active → Suspended actor lifecycle the constituents do not carry (a two-state machine held in actor_suspension_state); its states are left uncarded because Active is pervasively overloaded with the constituents’ own grant/session statuses. Its emergent state — actor_suspension_state and the suspension_log — is a composition-introduced surface no constituent provides, left as backticked store tokens. References to the constituent atoms and their operations — Permissions’ revoke / grant, Session’s revoke / issue / validate, Audit Trail’s record_action / verify_record, Credential’s revoke — the relayed tokens (actor_ref, subject_ref, principal_ref, grant_id, session_token, credential_id, suspended_by_ref), the constituent states (Active / Revoked), the substrate’s inherited rejections (recording-failure, invalid-credential, invalid-request), and the deployment configuration knobs (unified_actor_namespace, revoke_credential_on_suspend, partial_failure_posture) remain qualified/backticked, not carded here. (annotation.md Terms registry; representational only — it changes no guarantee, invariant, or behavior of the composition above.)

Suspend Actor

The composition’s load-bearing emergent action: within one transaction keyed on actor_ref, it snapshots the actor’s active grants and sessions, revokes every one (and, optionally, the actor’s Credential), transitions the actor Active → Suspended, and seals the complete revoked set into one attributed Audit Trail event. Returns {suspended, revoked_grants, revoked_sessions, revoked_credential?, event_id}, or Already Suspended (idempotent no-op), Revocation Failure (a non-benign constituent revoke failed — rolls back under all-or-nothing), or recording-failure. Neither constituent carries this multi-surface cascade.

Kind: Operation

Suspension Report

The composition’s read-only query: resolves actor_suspension_state[actor_ref], returning {state: Active} for an unsuspended actor or the full Suspended record — suspended_at, suspended_by_ref, reason, and the enumerated Revoked Grants / Revoked Sessions read from the sealed event. Changes no state; the queryable surface the issuance layer gates new access on.

Kind: Operation

Reinstate Actor

The composition’s thin lifecycle-reversal: transitions Suspended → Active and records an attributed actor.reinstated event. It does not restore any revoked grant or session (those are terminal in their constituents) — re-provisioning is the issuance layer’s job. Returns {reinstated, event_id}, or Already Active (no-op) / recording-failure.

Kind: Operation

Revoked Grants

The set of grant_ids the suspension cascade revoked, carried in the sealed actor.suspended event’s data (Invariant 2 — audit completeness). Its completeness — every active grant for the actor, no surface omitted — is what makes the suspension provable from one tamper-evident record.

Kind: Field Field of: the suspension event Role: the revoked grant enumeration Projects: revoked_grants

Revoked Sessions

The set of session_tokens the suspension cascade revoked, carried in the sealed actor.suspended event’s data (Invariant 2). Together with Revoked Grants it is the complete, sealed record of everything the suspension closed.

Kind: Field Field of: the suspension event Role: the revoked session enumeration Projects: revoked_sessions

Outcome

The suspension_log entry’s classification of a Suspend Actor / Reinstate Actor call: suspended, reinstated, Already Suspended, Already Active, revocation-failure(surface), recording-failure, or invalid-request. The composition’s own records-alone query surface alongside the tamper-evident Audit Trail.

Kind: Field Field of: the suspension-log entry Role: the call classification Projects: outcome

Already Suspended

The composition’s own idempotence rejection from Suspend Actor — returned when the actor is already Suspended: the cascade does not re-run (no second revoke, no second event; Invariant 3). The state gate that fires the cascade exactly once, on the Active → Suspended edge.

Kind: Member Member of: the suspend rejection Role: Rejection Projects: already-suspended

Revocation Failure

The composition’s own rejection from Suspend Actor — returned when a non-benign constituent revoke (or store inconsistency) fails: under the all-or-nothing default the whole cascade rolls back and the actor is left unchanged (Invariant 1). A benign already-terminal target (a concurrent revocation) is not this — it is counted toward completion.

Kind: Member Member of: the suspend rejection Role: Rejection Projects: revocation-failure

Already Active

The composition’s own no-op rejection from Reinstate Actor — returned when the actor is not Suspended, so there is nothing to reinstate.

Kind: Member Member of: the reinstate rejection Role: Rejection Projects: already-active

Standards references

this composition is the structural form of the prompt-and-provable-removal-of-access requirement that every access-control regime imposes at offboarding, deprovisioning, and incident response. Its primary anchors:

NIST (National Institute of Standards and Technology — US federal standards body) SP 800-53 Rev. 5, AC-2(3) (Account Management — Disable Accounts) and AC-6(5) (Least Privilege — Privileged Accounts) — AC-2(3) requires disabling accounts on termination, when they pose a significant risk, or when no longer required; AC-6(5) requires that privileged access be removed when no longer authorized. Suspend Actor’s atomic multi-surface revocation (Invariant 1) is the operational form of “disable the account across every surface it can act through,” and the sealed enumeration (Invariant 2) is the records-alone proof the control was applied.
SOX (Sarbanes-Oxley Act) §404 (Internal Control over Financial Reporting) — segregation of duties and access removal on role change are §404 controls; the actor.suspended event’s enumerated, attributed, tamper-evident record is the §404 evidence that a departing or reassigned actor’s access to financial systems was removed promptly and completely.
HIPAA (US Health Insurance Portability and Accountability Act) §164.308(a)(3)(ii)(C) (Termination Procedures) — the administrative safeguard requiring procedures for terminating access to electronic protected health information when a workforce member’s employment ends. This composition is the structural realization: the suspension closes every grant and session at once and proves it from the records.
PCI DSS (Payment Card Industry Data Security Standard — the card networks’ mandatory security rules for cardholder data) Requirement 8.1.3 (revoke access for terminated users immediately) — the requirement that access for terminated users be revoked immediately and completely. This composition’s all-or-nothing multi-surface revocation and its sealed enumeration are the structural form of “immediately and completely, provably.”
ISO/IEC 27001 §A.9.2.6 (Removal or Adjustment of Access Rights) — the International Organization for Standardization / International Electrotechnical Commission control requiring that access rights be removed on termination or adjusted on change. The composition’s enumerate-and-revoke-each-surface cascade is the operational control; the suspension report and sealed event are the audit evidence.

this composition inherits the broader standards compliance of its constituents:

Through Permissions: NIST SP 800-53 AC-2/AC-3/AC-6, NIST SP 800-207 (Zero Trust), ISO/IEC 27001 §A.9, HIPAA §164.312(a)(1), SOX §404, PCI DSS Requirement 7 — the grant-revocation surface the cascade drives.
Through Session: NIST SP 800-63B §7 (Session Management), OWASP ASVS V3, HIPAA §164.312(a)(2)(iii) (automatic logoff) — the session-revocation surface.
Through the Audit Trail substrate (and transitively Event Log, Actor Identity, Tamper Evidence, Retention Window): SOX §404/§802, HIPAA §164.312(b)/§164.530(j), PCI DSS Requirement 10, 21 CFR (US Code of Federal Regulations) Part 11, SEC Rule 17a-4, ISO/IEC 27001 §A.12.4, GDPR (EU General Data Protection Regulation) Articles 30 and 32 — the attributed, retained, tamper-evident record the suspension event lands on.
Through the optional Credential: NIST SP 800-63B (authenticator revocation), PCI DSS Requirement 8 — the re-authentication door the optional credential revocation closes.

Status

grounded on Final Critique 4 — 2026-06-10 (2026-06-10) — three-round baseline + author Final Critique + the fresh-reader Phase 4 Opus Happy-Torvalds-X2 clearance gate all complete; foundational findings at zero (the gate folded five refining findings — see Lineage). Formal-layer vote YES and the derived TLA+ — Temporal Logic of Actions — model + buggy twin verified in tools/harness/ (the CORRECT model holds at 2 states; the buggy twin is rejected on Invariant 1), so the formal prerequisite is discharged. Drafted against the approved this composition architectural cut — Actor Identity (the suspended actor’s composition-introduced Active/Suspended lifecycle) + Permissions (grant-revocation target) + Session (session-revocation target) + Audit Trail (substrate → Event Log + Actor Identity + Tamper Evidence + Retention Window) + optional Credential — as Login’s outbound-side counterpart, with multi-surface atomic revocation, audit completeness, and cascade ordering as the load-bearing claims. Regulated-pattern conventions (Regulated adversarial scenarios; Generation acceptance with the Audit-Trail-traversal-clearable / externally-clearable split) baked in from the first draft, inherited from the methodology directly per pressure-testing.md §Regulated-pattern conventions. This is the status Resolve a Person’s Data Rights and Authenticated Actor sat at before their own Phase 4 gates; the fresh-reader gate (Opus, claude-opus-4-8, 2026-06-10) cleared with zero foundational findings, flipping this status to grounded on Final Critique 4, bumping the catalog counts, and promoting the roadmap entry.

Lineage notes

Regulated composition (composes regulated atoms and records regulated events on the Audit Trail substrate). The two regulated-overlay conventions — Regulated adversarial scenarios and Generation acceptance (with the Audit-Trail-traversal-clearable / externally-clearable split) — are inherited from the methodology directly (pressure-testing.md), baked in from the first draft, not re-derived from predecessor patterns. The primary structural reference is Login: this composition is Login’s outbound-side counterpart, and it mirrors Login’s cascade structure (snapshot-scoped revocation), atomic-commit discipline (the cascade + audit write in one transaction), and TOCTOU handling (a concurrent terminal transition during the cascade is benign, the same already-terminal case Login’s Final Critique 4 (finding Final Critique 1) resolved) — inverting only Login’s best-effort posture to all-or-nothing because suspension’s failure mode is more dangerous. The substrate-composition shape (recording on the Audit Trail the substrate carries) follows Audit Trail, Multi-Party Approval, and Resolve a Person’s Data Rights; the TLA+ atomic-cascade + buggy-twin structure mirrors audit-trail.tla and login.tla. The motivating gap is the deprovisioning cascade Permissions’ Mass revocation on subject deprovisioning edge case and Actor Identity’s Actor lifecycle / Actor Registry note both anticipate.

Structural milestone. This composition is the composing pattern that Permissions’ Actor Registry / Identity Provisioning (forthcoming) note (“Deprovisioning an actor should cascade revocation of their grants; that cascade belongs to the composing system”) and Actor Identity’s actor-lifecycle deferral both anticipate. No atom carries an exact Actor Suspension *(forthcoming)* marker to retire (the anticipation is phrased as the Actor Registry concern), so this composition retires no named forthcoming-link; it realizes the named cascade obligation. It also stands as the outbound counterpart to Login and composes naturally with Authenticated Actor (which closes the attest surface) and Credential revocation to close the full outbound surface.

Capability-provenance self-check. Every emergent invariant’s Rests on: clause traces to one of the four declared sources (pressure-testing.md §Capability provenance): named constituent invariants/actions (Permissions revoke + Invariants 2/8 and the subject_ref-queryable store; Session revoke + Invariant 4 and the principal_ref-queryable store; Audit Trail record_action + Invariant 1 reached through the named substrate; Permissions Invariant 3 and Session Invariant 5 for the benign-terminal semantics), the deployment-declared unified_actor_namespace configuration capability (the enumeration’s join correctness), and composition-introduced surfaces (the one-transaction cascade; the actor_suspension_state gate; the suspension_log). No invariant rests on an ambient “the system can…”. In particular, the Active/Suspended lifecycle is not attributed to Actor Identity (which carries no lifecycle state) — it is a composition-introduced state machine, named explicitly to avoid the Final Critique 5-class capability mis-attribution.

Author gating review — 2026-06-10 (3×3 baseline + author Final Critique; author-led, not fresh-reader). The author ran the three passes (Pass 1 GRID — the nine-node structural-completeness framework; Pass 2 EOS — Essence of Software conceptual independence; Pass 3 Linus adversarial) across three rounds and consolidated an author Final-Critique-shaped closing pass. The grounding-granting fresh-reader Phase 4 gate is a separate step (pending, fresh session). Per-finding format F-id — short name — class → fix:

F1 — Active/Suspended lifecycle mis-attributed to Actor Identity — foundational (Pass 2 EOS, capability-provenance / Final Critique 5 class). An early draft read the actor’s suspension state “from Actor Identity,” but Actor Identity has a single Attested state and no lifecycle — it explicitly defers actor suspension to a forthcoming Actor Registry. → The Active/Suspended state machine is reframed as a composition-introduced surface (actor_suspension_state) this composition owns, named explicitly in Composes, Composition state, and the actor lifecycle is composition-introduced edge case. This is the round’s foundational soundness fix.
F2 — multi-surface revocation atomicity unstated; partial-state hazard unaddressed — foundational (Pass 3). The draft revoked grants then sessions as two steps without stating their atomicity, leaving a Suspended-with-active-session partial state reachable on a mid-cascade failure — exactly the half-open-door hazard the composition exists to foreclose. → Action wiring steps 3–7 are now one serialized transaction keyed on actor_ref with an explicit all-or-nothing default (roll back on any non-benign failure); Invariant 1 states the atomicity claim the formal model verifies (with the non-atomic multi-surface revocation as the buggy twin); the partial_failure_posture config and the Login-inversion rationale are added.
F3 — unified actor namespace assumed silently — foundational (Pass 2 EOS, capability-provenance). The enumeration (subject_ref = actor_ref, principal_ref = actor_ref) silently assumed the three namespaces coincide; if they diverge, the suspension under-enumerates — the exact CORNERS aliasing gap. → unified_actor_namespace added as a deployment-declared configuration capability (the declaring source for the enumeration’s join correctness), satisfied by Authenticated Actor’s binding or convention, with the divergence named as an externally-clearable check and a dedicated edge case.
F4 — benign TOCTOU (already-terminal target) conflated with failure — refining (Pass 3). The draft treated a Session.revoke → already-terminal (a concurrent logout during the cascade) as a failure that could abort the all-or-nothing transaction, which would let a benign race spuriously roll back a suspension. → Step 4 now treats not-active/already-terminal as benign (the surface is closed, the goal met), counted toward completion, never an abort — mirroring Login’s Final Critique 4 (finding Final Critique 1) already-terminal handling; Invariant 3 names it.
F5 — reinstatement implied access restoration — refining (Pass 3). An early Reinstate Actor read as if it restored the revoked grants/sessions, but those are terminal in their constituents and cannot be un-revoked. → Reinstate Actor is reframed as a thin state-flip (Suspended→Active) that explicitly does not restore access; re-provisioning is named as the issuance layer’s job (the Reinstatement does not restore access edge case).
F6 — snapshot-scoped bound not stated; concurrent issuance gap hidden — refining (Pass 3). Invariant 1 read as unconditional completeness, but this composition revokes and never issues, so a grant/session issued after the snapshot is uncovered. → Invariant 1 carries an explicit snapshot-scoped modulo-clause (parallel to Login Invariant 2), and the Suspension is snapshot-scoped edge case names the composing-layer obligation to gate issuance on the suspension state.
F7 — TLA+, TOCTOU, SOC acronyms unglossed at first body use — refining (Pass 1 acronym discipline). → Glossed at first occurrence.
Final Critique (author, X2 posture). Re-ran all three passes after the fixes. Foundational findings (F1, F2, F3) confirmed closed; the capability-provenance self-check re-verified every Rests on: clause resolves to a declared source with zero ambient dependencies, and confirmed the Active/Suspended lifecycle is housed at the composition layer rather than mis-attributed to a constituent. Pass 2 confirmed the externalizations a fresh reader is most likely to probe — suspension authorization (no Permissions-for-authorization in the cut), the actor registry (the lifecycle is this composition’s own, the registry remains forthcoming), and re-provisioning (the issuance layer, not this composition) — are EOS-clean. Foundational findings at zero. The pattern is author-clean but not yet grounded: grounding is gated on the fresh-reader Phase 4 Opus clearance gate (pending, separate session), per fresh-reader discipline.

Formal-layer vote: YES. The atomicity of multi-surface revocation (Invariant 1) is a load-bearing concurrency/safety claim: under interleaving of the cascade and concurrent revocations/issuance, no reachable success state may have a Suspended actor with an active grant or session — a multi-store atomic-cascade claim of exactly the shape login.tla (snapshot-scoped cascade) and audit-trail.tla (atomic cascade-on-purge, with the non-atomic twin showing a dangling partial) verify. Audit completeness (Invariant 2) is verified jointly (the sealed enumeration equals the revoked set in the atomic model). Cascade ordering / no-op-on-already-Suspended (Invariant 3) is the Active→Suspended gate’s idempotence, exercised by the model’s guard. Invariant 4 is each constituent’s own bar.

Formal model — 2026-06-10: TLA+ authored and verified; formal layer discharged. Derived model actor-suspension.tla with config actor-suspension.cfg, checked via tools/harness/ (the repo’s tla-checker WASM — WebAssembly — checker; no Java). What it checks: the actor’s two authorization surfaces are modeled as a set of grants Grants and sessions Sessions, each in {active, revoked}, plus a suspended flag and a per-surface audited set (the enumeration carried in the actor.suspended event). The CORRECT model performs the cascade as a single atomic action (SuspendAtomic, guarded on ~suspended — the Active→Suspended gate): it revokes every grant and every session, records the complete enumeration into auditedGrants/auditedSessions, and sets suspended in one step. The model (and its conjunction Safety) asserts the following, all holding across every reachable state: Invariant 1 in two forms — Inv1_Coherent (the state is either fully un-suspended with nothing audited, or fully suspended with everything revoked and everything audited — the atomic-cascade coherence form) and the load-bearing Inv1_FullyDeauthorized (suspended ⇒ every grant revoked ∧ every session revoked; no Suspended-with-active-access state) — and Invariant 2 (Inv2_AuditComplete — every revoked grant/session is enumerated in the audited set). Invariant 3 (cascade ordering / no-op-on-already-Suspended) is covered by-construction, not as a named assertion: the SuspendAtomic guard ~suspended disables a second suspend (exactly-once firing) and the model defines no action that clears suspended (monotonicity), so both hold structurally. Per the coverage cross-check this is recorded as an assumption rather than a verified property — promotable to an explicit check should a future edit add a suspended-clearing (reinstate) action to this model. Bounds/saturation: Grants = {g1, g2}, Sessions = {s1, s2}; the property is per-actor-local, so the atomic commit collapses the partial-state space — raising the surface counts adds no new behavior class (the atomicity, not the cardinality, is what is verified). Buggy twin: actor-suspension-buggy.tla splits the cascade into separate, interleavable sub-steps (RevokeGrants → RevokeSessions → RecordSuspended) with no transaction — the non-atomic multi-surface revocation the All-or-nothing edge case and Invariant 1 warn against. The interleaving RevokeGrants → RecordSuspended reaches suspended = TRUE while a session is still active (a half-open door); TLC rejects the twin on Invariant 1. (The committed .cfg lists Inv1_Coherent first, so the checker reports the violation on it — Invariant 0 in the harness output; Inv1_FullyDeauthorized is independently violated by the same Suspended-with-active state, confirmed by an isolated single-invariant run.) The twin is the vacuity guard — it proves the checker can fail on this property, so the correct model’s green is meaningful. Conflict-protocol outcome: none — the model corroborates the English; the spec already requires the cascade + transition + seal to commit as one transaction (Action wiring steps 3–7, all-or-nothing default), which is exactly the atomic/non-atomic distinction between the correct model and the twin. Canonical English unchanged. The snapshot-scoped concurrent-issuance gap, the best-effort posture, and the optional Credential surface are deliberately out of model scope (composing-layer obligation / configurable posture / optional constituent; see the vote and edge cases). Reproduce: cd tools/harness && node check.mjs ../../compositions/actor-suspension.tla (and … -buggy.tla --buggy).

Opus clearance gate — Happy Torvalds X2 — 2026-06-10 (claude-opus-4-8): clean of foundational findings; 5 refining folded; foundational at zero; grounds on Final Critique 4. Fresh-reader Phase 4 gate conducted with no author context — every “closed”/”verified” claim in the prior Lineage was re-derived from the spec body and the constituent specs rather than trusted. Pass 1 (GRID) and Pass 2 (EOS) at standard intensity; Pass 3 (Linus) at X2 depth, stressing multi-surface revocation atomicity, audit completeness, cascade ordering, capability provenance, and regulated-overlay completeness.

Cross-reference re-verification (head-on against the constituent specs). Every cited constituent invariant count and capability was confirmed against the source: Permissions 1–10 (Invariant 2 status-monotonicity, 3 revocation-terminal, 8 revoked-confer-no-permission; the subject_ref-queryable grant store; the Mass revocation on subject deprovisioning edge case verbatim); Session 1–11 (Invariant 4 revocation-absorbing, 5 terminal-absorbing; the principal_ref-queryable store with “revoke all sessions for this account”); Actor Identity 1–9 (Invariant 1 attestation-immutability; single Attested state, actor lifecycle explicitly deferred to a forthcoming Actor Registry — confirming the Active/Suspended lifecycle is composition-introduced, not mis-attributed); Audit Trail application-level 1–8 (Invariant 1 attribution-coverage; record_action / verify_record signatures); Credential 1–11 (Invariant 4 revocation-absorbing; revoke signature). The constituent action signatures this composition cites match their sources exactly, and the Generation-acceptance check counts this composition names (Permissions 5, Session 5, Audit Trail 6, Credential 6) are each correct.

Capability-provenance re-verification. Every emergent invariant’s Rests on: clause resolves to a declared source among the legitimate kinds: named constituent invariants/actions (Permissions revoke + Inv 2/3/8 + the queryable store; Session revoke + Inv 4/5 + the queryable store; Audit Trail record_action + Inv 1 + Tamper Evidence, reached through the named substrate — not an ambient reach-through), the deployment-declared unified_actor_namespace configuration capability (the enumeration’s join correctness — an honest config capability whose actual coincidence is routed to an externally-clearable check, per declared-is-not-verified), and composition-introduced surfaces (the one-transaction cascade; the actor_suspension_state gate). The Active/Suspended lifecycle is housed at the composition layer, and the snapshot-scoped concurrent-issuance gap is a named composing-layer obligation parallel to Login Invariant 2. Zero ambient/undeclared dependencies; zero Final Critique 5-class mis-attributions.

Harness re-verification (mechanical, re-run this session through tools/harness/check.mjs). CORRECT — node check.mjs ../../compositions/actor-suspension.tla → TLA+ actor-suspension.tla (states: 2) -> all invariants hold — PASS. BUGGY — node check.mjs ../../compositions/actor-suspension-buggy.tla --buggy → TLA+ actor-suspension-buggy.tla (states: 2) -> VIOLATION: Invariant 0 violated — PASS (twin correctly rejected; Invariant 0 is Inv1_Coherent, the first-listed Invariant-1 encoding — an isolated cfg checking only Inv1_FullyDeauthorized confirms the twin violates that invariant specifically). Bound-saturation bump: raising the surfaces to Grants = {g1,g2,g3} / Sessions = {s1,s2,s3} keeps the CORRECT model at 2 states, all invariants holding — the atomic commit collapses the partial-state space, so cardinality adds no behavior class (saturated). The model faithfully encodes Invariant 1 (no reachable Suspended-with-active state), is non-vacuous (suspended reaches TRUE, so the implication’s antecedent is exercised, and the twin proves the checker can fail), and the twin re-introduces a real non-atomic-cascade hazard.

Per-finding (F-id — short name — class → fix):

Final Critique 4 — already-terminal handling mis-cited as “Login’s Final Critique 1” — refining → Login has no Final Critique 1; the benign already-terminal / TOCTOU handling is Login finding Final Critique 1, surfaced in its Final Critique 4 (login.md). All seven citations corrected to “Login’s Final Critique 4 (finding Final Critique 1)”.
Final Critique 4 — Lineage named a model invariant (Inv3_SuspendMonotone) absent from the committed .tla — refining → the model checks Inv1_Coherent, Inv1_FullyDeauthorized, Inv2_AuditComplete (+ Safety); Invariant 3 is covered by-construction (the ~suspended guard + no suspended-clearing action). The Formal-model paragraph now names the actual constructs and records Invariant 3 as by-construction.
Final Critique 4 — twin-rejection over-specified to Inv1_FullyDeauthorized — refining → the committed .cfg lists Inv1_Coherent first, so the harness reports the violation on Invariant 0 (Inv1_Coherent); both encode Invariant 1 and both are violated. Paragraph corrected, with the isolated single-invariant confirmation noted.
Final Critique 4 — not-known revoke result under-mapped at the Suspend Actor boundary — refining → step 4 named a revoke → not-known (enumeration/store inconsistency) only as “surfaced as a finding”; now stated as a non-benign failure (abort + rejected(revocation-failure) under all-or-nothing, recorded under best-effort) plus a high-priority suspension_log finding, for both the grant and session surfaces (the case is structurally near-impossible given Permissions Inv 10 / Session Inv 9).
Final Critique 4 — SOC unglossed at first body use — refining (Pass 1 acronym) → glossed “Security Operations Center (SOC)” at first use in the compromised-account domain example (the prior Lineage F7 claimed it closed, but it had not propagated).

Foundational findings: zero. Five refining findings folded in-pattern. Pass 1 (GRID) and Pass 2 (EOS) clean — the regulated overlay is complete (Regulated adversarial scenarios’ three classes: regulator audit / disputed action / breach investigation; Generation acceptance with the Audit-Trail-traversal-clearable / externally-clearable split), identity model and action signatures and rejection taxonomies are explicit, and examples cover the rejection and adversarial paths. At the 92%-good threshold (foundational density zero), this composition grounds on Final Critique 4.

Showcase pass — 2026-06-29. Representational-only annotation/legibility pass; no guarantee, invariant, number, formula, signature, or rejection taxonomy changed (the invariant count held at four). (a) Four-kind [Term] annotation applied across the body and a ## Terms registry added after Edge cases (9 terms): 3 Operations — the emergent actions (Suspend Actor, Suspension Report, Reinstate Actor); 3 Fields — the audit-completeness enumeration the suspend event carries (Revoked Grants, Revoked Sessions) and the suspension_log classification field (Outcome); and 3 Members — the composition’s own rejections (Already Suspended, Revocation Failure on suspend; Already Active on reinstate). The Active → Suspended actor lifecycle (a genuine composition-introduced two-state machine held in actor_suspension_state) is described in prose but its states are left uncarded, because Active is pervasively overloaded with the constituents’ own grant/session Active status — carding it would be ambiguous. No Type card (the emergent state maps actor_suspension_state / suspension_log are backticked store tokens) and no Parameter (all action inputs are relayed constituent tokens). Survivors left backticked: the fenced projected-contract signatures (the #### \name` action headings and their code blocks); every qualified constituent call (Permissions' revoke / grant, Session's revoke / issue / validate, Audit Trail's record_action / verify_record, Credential's revoke) and outcome (ok, revoked, denied, not-active, already-terminal); the relayed tokens and constituent states; the substrate's inherited rejections (recording-failure, invalid-credential); the deployment configuration knobs (unified_actor_namespace, revoke_credential_on_suspend, partial_failure_posture); and concrete example ids. Constituent atom names remain the existing full links to ../atoms/*; constituent operations stay backticked qualified calls, not cross-page links (the decided convention). (b) **Summary/blockquote merge** — ## Summary moved to the top (after TOC, before Intent), its first run-on paragraph split one-idea-per-paragraph (cut #1, lossless) with the Login-mirror / common-uses paragraph kept intact; the dense descriptive top blockquote folded out after confirming each claim (multi-surface atomic de-authorization; the Login-outbound-counterpart framing; the four-atom-plus-optional-Credential composition; the three emergent invariants — atomicity, audit completeness, cascade ordering; the all-or-nothing default) is carried by Summary / Intent / Composes / the load-bearing wiring decision; no *also-known-as* line existed, so none was invented. (c) **Lineage collapsed** into a

 block. (d) **prose cut #5 — skipped (with reason):** the composition does own an emergent state machine (Active ⇄ Suspended), but it is a trivial two-state lifecycle already stated crisply (the step-2 Active→Suspended gate, the [Reinstate Actor] reverse edge) — a transition table would add nothing. Re-verified, not re-grounded: Status stays at

grounded on Final Critique 4 — 2026-06-10

. Gates: lint clean (O-term resolver — every marker resolves and every card is used); term-adapter derives cleanly (9 terms); four composition-level invariants preserved; the

.tla models untouched — harness re-run green: actor-suspension.tla PASS (2 states) + actor-suspension-buggy.tla –buggy` rejected on Invariant 1.

Actor Suspension

Summary

Intent

Composes

Composition logic

Composition state

Configuration

Primitive policies

Action wiring

suspend_actor

suspension_report (read-only)

reinstate_actor

The load-bearing wiring decision — multi-surface revocation is atomic and complete; suspension gates the cascade

Composition-level invariants

Examples

Walkthrough — offboarding a departing employee, end to end

Domain example — compromised account, all-or-nothing abort and retry

Rejection path — already-suspended no-op, and the benign TOCTOU race

Regulated adversarial scenarios

Generation acceptance

Audit-Trail-traversal-clearable checks

Externally-clearable checks

Edge cases and explicit non-goals

Terms

Suspend Actor

Suspension Report

Reinstate Actor

Revoked Grants

Revoked Sessions

Outcome

Already Suspended

Revocation Failure

Already Active

Standards references

Status

Lineage notes

`suspend_actor`

`suspension_report` (read-only)

`reinstate_actor`