Privileged Access Provisioning

Composition partially resolved 10 invariants TLA+ model regulated composes 4 atoms + 2 substrates

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

Privileged Access Provisioning

Summary

Privileged Access Provisioning governs the full life of a request for elevated access — to financial controls, patient records, production credentials, and the like — where the access must be approved by more than one party and must be time-limited rather than standing.

A request is submitted under a named requestor, must clear a mandatory multi-party approval chain, and only then results in a time-limited, scoped access token being issued; every time that access is actually used, the requestor’s session is re-checked for validity first.

It combines six patterns: the multi-party approval gate, credential authentication, time-limited sessions, caller authorization (Permissions), the access token itself (a Capability — a bearer token good for a bounded time and scope), and the tamper-evident audit record spanning the whole arc.

The central guarantees, which appear only when the patterns are combined, are that no access token can exist without an approved chain behind it (so an auditor can confirm every token traces back to real approvals), that access cannot be used under an expired or revoked session, and that the entire arc — request, approvals, provisioning, each use, expiry, and revocation — sits in one audit record with no gaps and nothing to cross-correlate. Modeling the access as a time-limited token rather than a standing permission is deliberate: privileged access is temporary authorization, not indefinite access.

This is the worked example of approval-gated provisioning behind privileged access management, break-glass access, and time-boxed administrative escalation.

Intent

Privileged access — access to financial controls, patient records, production credentials, source-of-truth databases, cryptographic key material — differs from ordinary access in two ways. First, the grant itself must be authorized by more than one party: a single administrator who can self-approve elevated access to any resource is a control failure under every regulated framework from SOX (the Sarbanes-Oxley Act — US corporate financial-reporting law) to HIPAA (the Health Insurance Portability and Accountability Act — US healthcare-data privacy law) to PCI DSS (the Payment Card Industry Data Security Standard). Second, the access must be time-limited and scoped: indefinite standing access to privileged resources is the most common finding in security audits, because standing access that outlives the business need is indistinguishable from residual access that was never intended.

The six constituents address neither property alone. Multi-Party Approval enforces the approval gate but does not produce the access artifact. Capability produces the time-limited scoped access token but knows nothing about whether an approval chain cleared. Session validates the authenticated channel but does not gate any downstream action. Credential authenticates the principal but does not know what they are requesting access to. Permissions authorizes who may ask but neither approves nor provisions. Audit Trail records everything and decides nothing. The composition is the layer that wires these concepts into a single, enforceable arc: no Capability is issued without an Approved chain; no access exercise succeeds without an active Session; the full arc is recorded in one tamper-evident Audit Trail.

The load-bearing design decision is that privileged access is modeled as a Capability token rather than a Permissions grant. Permissions grants are persistent until revoked and identity-keyed — they say “this actor may perform this action, indefinitely.” Capability tokens are time-bounded, scoped, and bearer-keyed — they say “whoever holds this token may exercise this specific access once (or N times), until this date.” Privileged access is temporary authorization, not standing access. The bearer-key property of Capability is a feature here: the access token can be handed off to an automated system or a break-glass process without requiring the executing agent to carry the principal’s identity. The Capability’s own audit record names the allocator (the composition, acting on behalf of the approved request) and the requestor (via the request record); it intentionally does not name the redeemer — the atom’s declared audit asymmetry. What re-binds identity at exercise time is this composition’s session gate: Session.validate’s declared return hands back the session’s principal_ref, and the exercise record names it. The asymmetry the composition defends is therefore precise: the token never knows its bearer; the exercise record names the authenticated principal of the session it was exercised under — which is the identity regulated audit actually needs, supplied by the constituent’s declared surface rather than by subverting the token.

This composition is the library’s worked example of approval-gated provisioning — the pattern that recurs in privileged access management (PAM — the discipline of controlling and auditing elevated accounts), break-glass access, time-boxed administrative escalation, and regulated change-control access in financial, healthcare, and government systems.

Composes

Multi-Party Approval — the approval-gate substrate. The composition maintains one Multi-Party Approval instance whose chain-store subject_ref is the request_id and whose scope is the access_scope of the request. Every privileged access request maps one-to-one to a Multi-Party Approval chain. The substrate’s chain-facing actions — chain-level (initiate_chain, withdraw_chain) and step-level (Approve Step, Reject Step) — are exposed through this composition’s surface, which adds credential verification and Audit Trail recording around the passthrough; the caller’s credential is passed through to the substrate’s own signatures, which require it (initiate_chain(actor_ref, credential, subject_ref, scope, approver_set, quorum_rule, reason?), approve_step(actor_ref, credential, chain_id, step_id, reason?), withdraw_chain(actor_ref, credential, chain_id, reason)). The chain-state read is the substrate’s declared read_chain(actor_ref, query) — gated on its chains:read scope, called by the composition as the configured application_actor_ref with a {chain_id: …} query. Two Permissions gates therefore stand in the arc by construction, and the deployment wires both: this composition’s requests:* vocabulary on its own instance, and Multi-Party Approval’s chains:* vocabulary on the substrate’s instance — the deployment grants requestors chains:initiate and chains:withdraw — chain withdrawal is the substrate’s initiator-only act, so the only lawful withdrawer is the requestor, and a requestor without the substrate grant cannot withdraw their own request (the requestor-grant obligation Withdraw Request step 4 rests on) — and grants the composition actor chains:read, or configures the substrate’s instance to mirror this composition’s grants. Multi-Party Approval’s own Audit Trail substrate is the same Audit Trail instance this composition uses for provisioning and access-exercise events — one Audit Trail instance for the full arc.
Credential — the authentication surface for the requesting principal and for the approvers. The composition calls the atom’s declared verify(principal_ref, credential_type, presented_material) → verified | failed-verification(material-mismatch | no-active-credential) — the acting actor’s reference as the principal, the configured credential_type (Configuration), and the caller-supplied credential as the presented material — to confirm the requestor’s credential verifies before a request is accepted, and again before each approver step is routed (ensuring the approver has not been revoked between chain initiation and decision). Credential is not independently managed by this composition — it is queried read-only. The composition does not call register, rotate, or revoke on any Credential; those belong to Login’s or the identity-management surface.
Session — the time-limited authenticated channel. The composition calls the atom’s declared validate(session_token) → valid(principal_ref, expires_at) | invalid(expired | revoked | not-known) as the first step of Exercise Access. If the session is not valid — expired, revoked, or not known — the exercise is rejected before the Capability is presented; when it is valid, the atom’s own return hands the composition the session’s principal_ref, which the exercise record names (Behavior — the identity surface at exercise time is the session’s declared return, never a reach inside the atom). Session is not independently managed by this composition; it is queried read-only. Sessions are issued by the Login composition. The cascade from Credential revocation through Session invalidation through blocked Exercise Access calls is the composition’s cascading-revocation emergent invariant.
Permissions — the authorization gate for caller-initiated actions. The composition calls Permissions.permitted in Request Access (scope: requests:initiate) and in Revoke Access (scope: requests:revoke); Withdraw Request carries no composition-layer permission check — it is structurally the requestor’s own act, mirroring the substrate’s initiator-only withdrawal rule (Action wiring; Edge cases — Third-party withdrawal is deliberately absent). Permissions is queried read-only; the composition does not call grant or revoke on any permission. The authorization policy — which principals hold which request scopes — is owned by the deployment’s Permissions store.
Capability — the provisioned access token. The composition maintains exactly one Capability instance, dedicated to this composition — which is what lets a redemption there resolve provenance: any token that instance knows was allocated by this composition’s cascade. It calls the atom’s declared allocate(allocator_ref, scope, max_redemptions, ttl) once per approved request, with allocator_ref = application_actor_ref and the composed scope — this composition’s byte-exact serialization of (request_id, resource_ref, access_scope) (Primitive policies): the atom declares its scope opaque, interpreted by whatever uses it, and this composition is the interpreter, so the request↔resource↔token binding rides the Capability’s own immutable scope field rather than any composition-owned truth. redeem(capability_token) → redeemed(scope, allocator_ref) | invalid(exhausted | expired | revoked | not-known) is called inside Exercise Access after Session validation passes — the returned scope is where the exercise recovers the request_id, from the constituent’s own record. revoke(capability_token, revoked_by_ref, reason) is called by Revoke Access. There is no expire action and no expiry write anywhere: a lapsed capability is shown Expired by the atom’s derived Effective-Status projection (its Invariant 13) and refuses redemption with invalid(expired); nothing here or there writes an expiry. The redeemer’s identity is intentionally not recorded by the Capability atom; the session under which Exercise Access was called — whose principal_ref the validate return names — is where the composition’s own record re-binds identity at exercise time.
Audit Trail — the regulated-audit substrate, consumed at its declared contract — record_action(action_ref, actor_ref, credential, data) → event_id | rejected(invalid-credential | invalid-request | recording-failure(step)), the (step) payload read wherever a record follows a committed act, since step-4 means the event is already appended and a retry would double it (the recovery discipline’s pre-check is what makes that safe). One Audit Trail instance is maintained across all five stages of the arc. Multi-Party Approval’s approval-chain events, the provisioning event (access_provisioned), and each access-exercise event (access_exercised) and revocation event (access_revoked) are all recorded in this instance. The instance is configured with the host’s regulatory retention policy at deployment. Event Log, Actor Identity, Retention Window, and Tamper Evidence are reached transitively through Audit Trail; the composition does not maintain separate instances of those atoms.

Composition logic

Composition state

The composition owns emergent state that wires the constituent atoms into one queryable access-request surface. Every element carries its Contract classification per execution-contract.md §Composition state: all six elements are derived indexes inside the audit horizon, and two classes of state here are truth-bearing and are named as such rather than folded into that sentence — (a) each element’s past-horizon half, where the store record is the only surviving copy of what a purged payload carried, held under the never-delete obligation Configuration’s store_durability declares; and (b) the payload of every open audit_pending entry, which is a record owed for a committed act and exists in no constituent store, extraction-pending against a durable Outbox atom (forthcoming) owning records owed for committed acts, and until it lands a durability obligation on the request record stated below. The truth the six elements accelerate lives in the constituent stores plus the substrate audit log, the composition recording its request-level truth as audit events through the substrate’s record_action (the Contract’s record-by-composing-Event-Log rule, the same discharge Multi-Party Approval makes one layer down) and the token binding in the Capability instance’s own immutable scope field (the composed scope — Composes). The payload requirement that makes the rebuilds total: every audit event this composition emits carries request_id and the seam-injected invocation_id of the invocation that emitted it (Logic confinement) in its data — the second is what lets the recovery discipline’s pre-check tell an event that landed from one that is owed, exactly, rather than by matching payload fields — with one declared null-request exception: a not-known exercise attempt’s access_exercise_failed event carries request_id = null, because no request exists and the attempt is evidence about the presenter (the relations and the request_to_events keying below carve the exception out); access_requested additionally carries the full declared request shape — requestor_ref, resource_ref, access_scope, justification, requested_at, expires_at, chain_id, approver_set, quorum_rule; each state-transition event carries the resulting state and, where set, denial_reason. No event carries bearer material: neither capability_token nor session_token appears in any event payload — the token binding is read from the Capability store, and the exercise identity is the session’s principal_ref (the leak the alternative would be: audit data readable under requests:read that grants the very access it records). One bounded exception is named rather than hidden: a request inside a recovery window — its constituent writes committed but the audit event that would carry the fact not yet landed, or its record pre-written ahead of its constituent writes and event (Request Access step 4’s durable pre-write; each window an open audit_pending entry of the recovery discipline, Action wiring) — is invisible to the rebuilds for exactly that window; the affected record is truth-bearing until its event lands, and the durability obligation for the window covers the pending event’s payload, not just the record’s own fields: each open audit_pending entry (the marker is a multi-entry list — the recovery discipline) carries the exact action_ref and event data its pending record_action must carry — for an exercise, the session_principal_ref and exercised_at of the invocation, which exist in no constituent store — since without them a restart could not construct the recovery record it owes. The window is surfaced, bounded, and closed by the recovery discipline. The elements:

request_store — the set of access request records. Each record carries request_id, requestor_ref, resource_ref, access_scope, justification, requested_at, expires_at (computed from ttl — time-to-live, the requested validity duration — at request time), chain_id (written the instant Request Access step 5 returns it, before the request’s own event is recorded — the binding’s durable home for the window in which no event yet carries it), state (Pending Approved Provisioned Denied Withdrawn Revoked ProvisioningFailed), denial_reason (nullable; set when state transitions to Denied or ProvisioningFailed), and the recovery discipline’s audit_pending marker — a multi-entry list of open recovery windows (default empty). request_id, requestor_ref, resource_ref, access_scope, justification, requested_at, expires_at, and chain_id are immutable once written (chain_id is null for exactly the window between the step-4 pre-write and step 5’s return); state advances forward only (Approved is the declared in-cascade transient; Denied, Withdrawn, Revoked, and ProvisioningFailed are terminal; Provisioned is terminal for the store — later Capability lapse or exhaustion is the constituent’s own record, never a request-state write). Contract classification: derived index (outside the recovery window above). Rebuild procedure: enumerate the audit instance through its declared list-query surface (a sequence-range read with an open upper bound, passed through the substrate to its Event Log) and filter in composition code to this composition’s action_refs; each access_requested event supplies one request’s identity fields per the payload requirement — and so does an access_request_withdrawn event whose reason is initiation-failed(…), which carries the full request shape because it is the only event a request closed before its chain existed will ever have (an earlier rebuild that read identity from access_requested alone dropped those requests and left their withdrawal events keyed to nothing) — and the request’s state is the latest state-transition event’s declared state (none → Pending; access_provisioned → Provisioned; access_denied → Denied; access_request_withdrawn → Withdrawn; access_revoked → Revoked; access_provisioning_failed → ProvisioningFailed). The three Contract obligations attach — outside the atomicity surface, rebuild-on-miss, no cross-constituent consistency claim — and the rebuild is bounded by the audit instance’s horizon, exactly as request_to_chain and request_to_events below state for the same traversal: past it a purged access_requested payload is unreadable, so the classification splits by retention state — derived index while the events survive, truth-bearing beyond, where the request record is the only surviving copy of the request’s identity fields and the store’s never-delete rule (Invariant 8) is the durability obligation that makes it one.

request_to_chain — map from request_id to the chain_id in Multi-Party Approval. Set at Request Access step 5, the instant the chain id returns, and immutable; every request maps to exactly one chain. Contract classification: derived index — over the request record’s own chain_id field first, the event second. The record carries the binding from step 5 onward, so the actions resolve a chain from the record (request_store[request_id].chain_id) and this map is read-path acceleration over that field; the map is never the binding’s only home, which is what lets Approve Step and Withdraw Request find a live chain during the window before its access_requested event lands. Rebuild procedure: from the request records’ chain_id fields where the record survives, else the chain_id carried in each access_requested event’s data (the chain is initiated before the event is recorded, precisely so the binding exists to be recorded) — bounded by the audit instance’s horizon, past which the payload is destroyed in its entirety and the traversal cannot identify an access_requested event at all; entries for purged events are not rebuildable.

A second source appears to exist here, and whether it is one depends on a deployment fact worth checking rather than assuming. The Multi-Party Approval instance’s chain-store subject_ref is the request_id (Composes), so enumerating that store and re-keying by subject_ref reconstructs the same binding. But Multi-Party Approval’s chain_store is itself a derived index over audit events, so the fallback recovers the binding only if that store’s own contents survive — and where the two compositions share one Audit Trail instance, they share one horizon, and the fallback is not a fallback at all: both sides are erased by the same purge. It is a genuine second source only where the instances are distinct and the approval instance’s horizon is the longer. A constituent whose state is a derived index over the same substrate is not an independent source, and treating it as one would be the more dangerous mistake, since it reads as coverage.
request_to_capability and capability_to_request — the forward and inverse maps between request_id and the provisioned capability_token. Entries appear at provisioning and are immutable and never deleted. Contract classification: derived indexes over the Capability instance’s declared read surface. Rebuild procedure: enumerate Capability.read on the composition’s dedicated instance and parse each record’s composed scope — this composition’s own serialization of (request_id, resource_ref, access_scope) (Primitive policies) — re-keying by request_id (forward) or by the record’s own capability_token (inverse). The binding fact lives in the constituent’s immutable record, so both maps are pure read-path acceleration; a lost entry is a rebuild trigger. The raw token is a field of the constituent’s own store and of these internal indexes — it appears on no caller-facing surface of this composition: not in audit event data, not in Read Request results (the token reaches exactly one party, the requestor, through the provisioning delivery channel). Same three obligations.

session_access_log — the per-request record of every Exercise Access call that reached the Capability redeem step, successful or not. Each entry carries request_id, session_principal_ref (from the validate return), exercised_at, and result (redeemed capability-invalid(reason)). Contract classification: derived index over the substrate audit log — the truth is the access_exercised and access_exercise_failed events the exercise wiring records (each carrying exactly these fields per the payload requirement), and this element is read-path acceleration over them, not a second event stream: an append-only attributed log is precisely what the substrate exists to provide, and this composition does not rebuild one inside itself. Rebuild procedure: the same enumerate-and-filter as request_store, restricted to the two exercise action_refs — and bounded by the same horizon: the classification splits by retention state, and past the horizon the entries are truth-bearing, retained under the same never-delete obligation as the request record. Within the horizon its durability is the substrate’s own (Invariant 10 restates this rather than claiming a parallel obligation). Same three obligations.

request_to_events — map from request_id to the event_ids of every audit event recorded for that request, in recording order. This is the declared request→audit traversal — the surface an auditor walks from a request to the events that prove its arc, which Read Request surfaces and Generation acceptance’s arc-reconstruction check uses; without it, “find this request’s events” would be a payload-field query the substrate routes to Reverse Index. Populated as each record_action returns. Null-request events (the payload requirement’s declared not-known-exercise exception) key to no request and appear in no request’s traversal — an auditor reaches them by enumerating the exercise action_refs directly, not through this map. Contract classification: derived index. Rebuild procedure: the same enumerate-and-filter, keyed by each event’s data request_id (the payload requirement’s first clause exists for exactly this; null-request events are excluded by the same rule) — bounded by the audit instance’s horizon. The filter keys on data.request_id and on the action_ref the enumerate-and-filter selects by, and a purge destroys both together with the rest of the payload, leaving event_id and sequence_number; entries for purged events are not rebuildable, and the classification splits by retention state. What the horizon costs here is this traversal itself — the declared surface an auditor walks from a request to the events proving its arc, which Read Request surfaces and the arc-reconstruction check uses. There is no second source by construction: without this map the same question is a payload-field query the substrate routes to Reverse Index, which is the reason the map exists and the reason its loss is not recoverable elsewhere.

Configuration

default_ttl — the Capability token’s time-to-live if the requestor does not supply a ttl. Deployment-configurable. Must be positive. Absent default is invalid-request.
max_redemptions_default — the max_redemptions value passed to Capability.allocate. Defaults to 1 (single-exercise). This is deployment configuration, not caller input: Request Access takes no redemption-count parameter, so a requestor cannot ask for a multi-use token — deployments permitting multi-use privileged access (break-glass, time-boxed windows) raise the configured value for the instance, and the audit record reflects the configuration.
credential_type — the credential_type argument this composition passes to every Credential.verify call (the atom’s contract is verify(principal_ref, credential_type, presented_material), and the type names which of the principal’s credentials is being checked). Deployment-declared — one type per composition instance (a smart-card deployment names its card type; a password deployment its password type). A deployment whose requestors and approvers authenticate under different credential types resolves the type at its calling layer before invoking this composition; this composition passes exactly one configured value and never guesses.
credential_check_on_request — whether Credential.verify is called against the requestor’s credential before accepting the request. Defaults to true. Deployments that manage requestor credential verification upstream may disable; disabling does not change the session-validation requirement at Exercise Access.
approver_set_minimum — passed through to Multi-Party Approval’s configuration. The composition enforces that privileged access requires genuine multi-party approval by defaulting this to 2. A deployment that wants single-approver privileged access explicitly sets this to 1; the audit record reflects the single-approver configuration.
audit_trail_retention_policy — the policy reference the Audit Trail instance is configured with at deployment (Audit Trail’s record_action(action_ref, actor_ref, credential, data) takes no per-call retention argument). Typically sox_7_year, hipaa_6_year, or pci_dss_1_year depending on the regulated domain. Deployment-configurable. It carries a declared ordering obligation: the horizon must outlast the longest token lifetime the deployment admits plus the period over which it must be able to prove approval-gated provisioning from the trail, because request and Capability records are never deleted while the events that bind a token to its approval are purged at the horizon. Past it, a token is verifiable only to the depth its surviving attestations carry — the access_provisioned attestation’s action_ref, actor_ref and attested_at survive readable through the destruction record, the payload naming the request does not — and Invariants 1, 5, 7 and 9 and records-clearable checks 1, 4, 5 and 6 are stated over the horizon for that reason.
recording_completion_bound — the deployment-declared maximum duration between a committed act and the audit write that records it inside one invocation — from Capability.redeem’s return to the access_exercised write, from Capability.allocate’s return to the access_provisioned write, from a substrate decision’s commit to its approval_step_decided write — read against the seam-injected now the invocation carried. It is the lower edge of every leg of the recovery sweep that runs outside the per-request_id serialization’s hold: Exercise Access’s record write at step 3 runs after the hold is released, so an entry marked redeemed younger than this bound may belong to an invocation still about to write, and a sweep that landed its recovery record then would put two events under one redemption. The legs that run wholly inside the hold (the cascade, the evaluation) need no bound — a live invocation holds the serialization and a dead one has released it — and the sweep’s pre-check against the trail (the recovery discipline) is the second guard either way. The upper edge of every leg is audit_trail_retention_policy’s horizon, past which a missing event is destruction and the request record’s truth-bearing half is what answers. Default: none; a bound shorter than the slowest conforming invocation makes the exercise leg unsafe in the direction that writes.
store_durability — the durability the deployment owes the request store and the dedicated Capability instance, stated as an ordering: the request store at least as durable as the Capability instance, and neither ever purged — the Capability atom permits a deployment to purge terminal records under a retention policy (its External purge and retention edge case), and this composition’s dedicated instance is declared exempt: a purged token record would leave a Provisioned request whose binding parses to nothing, which check 1 would read as a bypass. Inside the audit horizon the request store is derived and this entry is what the rebuild rebuilds into; past it the request record is the only carrier of the request’s identity fields and of every open audit_pending payload, and this entry is the obligation Invariant 8’s never-delete rule spends.
application_actor_ref and application_credential — the composition’s service identity, used to attribute system-originated events in the Audit Trail — exactly the events with no human-actor origin: access_provisioned, access_provisioning_failed, access_denied, access_exercised, access_exercise_failed, the recovery records access_recovery_intended and access_audit_recovery, and the Approve Step step-5 reconciliation’s access_request_withdrawn (a chain found Withdrawn by a concurrent withdrawal whose own recording had not completed — the reconciliation runs inside the decision invocation with no live withdrawing human, so it is emitted with credential = application_credential and the same data the concurrent path would write; the exercise events are system-attributed because the exercise caller presents bearer material, not an actor identity — the recorded human-side identity there is the session’s principal_ref in the event data). All other events carry the acting human’s reference and credential. The same identity is the substrate reader: read_chain calls are made as this actor, which therefore holds chains:read in the substrate’s Permissions instance (Composes). Same discipline as Multi-Party Approval’s application_actor_ref: the deployment provisions and rotates this credential; its compromise surface and forgery defense follow the same reasoning as documented in Multi-Party Approval’s Configuration section, with this composition’s structural backstop being Invariant 1 — a forged access_provisioned event names a request whose chain the step records show un-Approved, detectable by recomputation.

Logic confinement

The clock is an injected input at the composition’s single I/O seam, never read inside a guard or a transition and never threaded through a caller signature. Per the Logic Confinement Principle (execution-contract.md), the host reads the clock once per invocation and injects now (clock_t) at the seam before the orchestration runs; the actions below are pure functions of the stored records plus that injected now. Because the clock enters at the seam rather than as a parameter, the action signatures carry no now argument.

now is consumed for exactly two clearly separated purposes:

Stamping immutable timestamps on a committed write — requested_at on Request Access and exercised_at on each session_access_log entry.
Computing derived deadlines from an injected duration — expires_at = now + ttl at Request Access, and the remaining-lifetime scalar ttl = request.expires_at − now passed to Capability.allocate in the provisioning cascade. Both are computed from the injected now and the caller-supplied or default ttl; neither samples a clock inside the transition.

No stored expiry flag. The composition stores the expires_at deadline, never a derived “expired” or “eligible” boolean — expiry is a condition computed from the stored deadline against an injected now at the moment it is asked, so nothing can lag the clock. Request-expiry enforcement and session validity are the constituents’ own guards (Capability’s TTL — time-to-live — exhaustion, Session’s Active determination), each evaluated against the now injected at that constituent’s seam; this composition adds no clock-bearing guard of its own.

One injected now per invocation — for this composition’s own stamps and arithmetic. Within a single invocation, one injected reading serves both the stamp and the deadline arithmetic, so requested_at and expires_at derive from one reading rather than two — expires_at − requested_at is exactly the requested ttl, not ttl plus an inter-read drift. It does not extend into the constituents: each constituent call is its own pipeline invocation with its own seam, so Session’s Active determination and Capability’s TTL exhaustion are evaluated against the readings injected at their seams, not this one. The consequence is stated plainly rather than papered over — a request exercised at the margin of a TTL boundary can be judged differently by two seams, which is why the Generation acceptance session-gating check reads the recorded exercised_at against the Session record rather than re-deriving validity, and why no invariant here rests on comparing timestamps across seams. A deployment wanting one reading across all seams in a request must supply it as a host obligation; the spec does not promise it. Ids are allocated at the seam or by constituents: the seam injects one fresh invocation_id (id_t) per state-changing invocation, written into every audit event and every audit_pending entry the invocation produces (the Composition-state payload requirement), and at Request Access that same injected id is the request_id — one identifier, two names, so a request’s initiating invocation and its record share a key; chain_id, capability_token, session_token, and event_id are minted by Multi-Party Approval, Capability, Session, and Audit Trail respectively. This composition mints no id inside a transition and generates no cryptographic material.

Primitive policies

The composition takes string-typed inputs at every action boundary. Each is validated at this layer or by a named constituent; nothing is normalized anywhere — no trimming, no case-folding, no Unicode normalization — and equality is opaque byte-identity throughout.

requestor_ref / actor_ref — opaque actor references. Non-empty and non-whitespace, validated at this layer before any constituent is called; failure → rejected(invalid-request), nothing written. Byte-identity is the equality Permissions, Credential, and the substrate apply.
credential — opaque credential material, consumed only by Credential.verify (as the presented material) and by the substrate’s record_action and chain actions (which attest it inside the substrate). Never inspected, stored, or logged by this composition; never enters any event payload. Required on every state-changing action — the substrate’s signatures require it and nothing else can supply a human caller’s credential.
resource_ref and access_scope — opaque references to the resource and the access being requested. Each non-empty, non-whitespace, and within its declared length cap, validated at this layer — the caps are deployment constants derived from every surface the values must fit: the audit-payload budget (the references travel whole in access_requested), the Capability instance’s own scope-string cap less the request_id-and-separator envelope (the composed scope must be allocatable, so a length refusal at the cascade is foreclosed at intake rather than surfacing as a mischaracterized ProvisioningFailed), and the substrate’s chain-shape reference caps (access_scope doubles as the chain’s scope, and each approver_set element must satisfy the substrate’s approver_ref cap). An oversized value is rejected(invalid-request) with nothing written. The Permissions scopes this composition consults (requests:*) are composition-fixed vocabulary, never caller input.
The composed capability scope — the serialization this composition writes into Capability.allocate’s opaque scope argument: the three fields request_id, resource_ref, access_scope, in that order, in a fixed, byte-exact, self-delimiting encoding the deployment declares once per instance (any unambiguous encoding qualifies; the declaration is what makes parse(serialize(x)) = x mechanical). It is how the request↔resource↔token binding rides the Capability’s own immutable record (Composes) — the composition parses it back from redeem’s returned scope and from Capability.read in the map rebuilds, and never stores the binding as composition truth.
justification — free text, stored verbatim in the request record and the access_requested event; never interpreted. Size-checked at this layer against the audit-payload budget — the wired Audit Trail instance’s configured payload_cap less the event envelope — before any constituent is called, so an oversized justification is rejected(invalid-request) with nothing written rather than a partial-state discovery at the record step. Because the reference primitives and each approver_set element carry their own budget-derived caps (above), the check covers the full constructed event data, not the justification alone — which is what makes the record_action invalid-request arm genuinely unreachable at the wiring steps that claim it. reason (on decisions, withdrawal, revocation) carries the same rule.
ttl — time-to-live: a positive duration bounding the provisioned access. Validated positive at this layer where supplied; defaulted from default_ttl otherwise.
request_id, chain_id, step_id, session_token, capability_token — opaque identifiers and bearer material, allocated by the seam (request_id) or by the constituents. Equality-only; an unknown id yields not-known (or the constituent’s own invalid(not-known)) from the addressed action; never normalized. session_token and capability_token are bearer material: they are consumed by their atoms and appear on no caller-facing record surface of this composition.

The load-bearing wiring decision

Privileged access is provisioned as a Capability token, allocated only by the approval-gated cascade — never as a Permissions grant flipped on approval.

Principle. Privileged access is temporary authorization: the thing the regulators’ findings condemn is standing access that outlives its business need. An artifact that expires structurally — a token with an immutable deadline, refused by its own atom after lapse with nothing written — makes the time-bound a property of the record rather than a cleanup job someone must remember.

Likely objection. A Permissions grant flipped on approval is simpler: identity-keyed, revocable, queryable, and already composed here for the request gates — why introduce a bearer token and a second gate at exercise time?

Mechanism that resolves it. A grant is standing until someone revokes it — exactly the failure mode; its revocation is an act someone must perform, where the Capability’s expiry is a derivation nobody can forget. The bearer property is load-bearing, not incidental: break-glass and automated executors exercise access without carrying the requestor’s identity, and the identity that regulated audit actually needs at exercise time is re-bound by this composition’s session gate — Session.validate first, its returned principal_ref in the exercise record — not by the token. And the cascade is the only allocation path: Capability.allocate is called at exactly one step, fired only by a chain the substrate reports Approved, with the binding written into the token’s own immutable scope.

Result. Every provisioned access traces to a documented, quorum-satisfied approval (Invariant 1, recomputable from records); every exercise is session-gated and principal-attributed; expiry needs no janitor; and a leaked audit trail grants nothing, because no record surface carries the bearer material.

Action wiring

Each step below names every rejection its constituent call can return and where it lands at this composition’s boundary; the enumeration is exhaustive rather than illustrative. Two standing rules govern every action. First, truth-order: the constituent acts commit first, the audit event that carries the resulting request state records second, and the composition’s own maps are derived-index writes outside the atomicity surface — a failed map write is a rebuild trigger, never a failure arm. Second, committed acts are never reported as failures: where a recording step fails after the load-bearing constituent act committed, the action returns its success token, the request carries an open audit_pending entry, and the record catches up (the recovery discipline, below) — the alternative teaches callers to retry acts that already happened, which for a redemption would consume a second use.

request_access(requestor_ref, credential, resource_ref, access_scope, justification, approver_set, quorum_rule, ttl?) → request_id | rejected(invalid-request | permission-denied | credential-invalid | recording-failure)

Validate the primitives at this layer (Primitive policies): requestor_ref, resource_ref, access_scope non-empty, non-whitespace, and within their declared caps (each approver_set element likewise); justification present, with the full constructed event data — the capped references, the approver_set, and the justification — within the audit-payload budget; ttl positive where supplied. Any violation → invalid-request, nothing written.
Permissions.permitted(requestor_ref, requests:initiate) → denied returns Permission Denied (the atom’s contract is the two-outcome permitted | denied; there is no rejection arm to map).
If credential_check_on_request: Credential.verify(requestor_ref, credential_type, credential) → either failed-verification reason (material-mismatch, no-active-credential) returns Credential Invalid; nothing written.
Allocate request_id (the seam-injected id_t); stamp requested_at and expires_at = requested_at + ttl from the single seam-injected now (Logic confinement); durably commit the request record now — state Pending, chain_id null, with an open audit_pending initiation entry carrying the access_requested payload-to-be less the chain_id step 5 has not yet minted — before any constituent write. The pre-write is what keeps step 5’s chain from ever being an orphan: a crash after the chain commits would otherwise leave a live Pending chain (with Active approver Assignments) whose subject_ref resolves to nothing — invisible to every rebuild and withdrawable by no one, since the substrate’s withdrawal is initiator-only and the composition actor is not the initiator. The record is truth-bearing for exactly this window (Composition state’s bounded exception; the sweep’s initiation leg closes it). The pre-write’s own failure landing: a store refusal here is recording-failure with nothing written anywhere — no chain, no event, no record — and the caller retries the whole action.
MultiPartyApproval.initiate_chain(actor_ref=requestor_ref, credential, subject_ref=request_id, scope=access_scope, approver_set, quorum_rule) → chain_id. On success, before anything else: durably write chain_id onto the request record (its immutable field) and complete the initiation entry’s payload with it, under the per-request_id serialization — so from this instant the binding has a durable home, the entry carries the exact access_requested data its pending record must carry, and a live approver resolving the chain from the record finds it even if step 6 never lands. Populate request_to_chain (an index write over the field just committed). Rejection mapping — the pre-written request record is closed, not discarded (records are immutable and the store forward-only): the composition records access_request_withdrawn (composition actor, data = {request_id, state=Withdrawn, reason=initiation-failed(<the mapped arm>), requestor_ref, resource_ref, access_scope, justification, requested_at, expires_at, approver_set, quorum_rule} — the full request shape the step-4 pre-write holds, chain_id null, because this event is the only one such a request will ever have and the rebuild must reconstruct the record from it), transitions the request to Withdrawn, and closes the initiation entry before returning the mapped rejection, so the rebuilds see a closed request rather than a ghost: invalid-request → invalid-request (the substrate’s shape validation refused); invalid-credential → Credential Invalid; permission-denied → Permission Denied — the requestor lacks chains:initiate in the substrate’s Permissions instance, the double-gate the deployment wires (Composes); reaching it with requests:initiate held is a deployment wiring fault to alert on, surfaced honestly to the caller either way; recording-failure(step) → recording-failure.
Record the request: AuditTrail.record_action(action_ref=access_requested, actor_ref=requestor_ref, credential, data={request_id, requestor_ref, resource_ref, access_scope, justification, requested_at, expires_at, chain_id, approver_set, quorum_rule}) — the full request shape per the Composition-state payload requirement. On success, close the initiation entry (the record it awaited has landed) and populate request_to_events (an index write; the request record committed at step 4 and its chain_id at step 5). Rejection mapping: the chain now exists but the request’s access_requested record did not land — the initiation entry simply stays open (step 5 completed its payload, chain_id included) and the action returns request_id anyway (the chain is live and approvers hold in-tray items; failing the caller would orphan it), the recovery discipline landing the record; invalid-credential here after step 5 accepted the same credential is a rotation race, handled the same way; invalid-request is unreachable by construction once step 1’s constructed-data size check passed — observing it is the payload-budget/instance-cap disagreement, a deployment fault taking the same recovery path.
Return request_id.

Validate the primitives (actor_ref non-empty; reason within the audit budget where supplied) → invalid-request. Resolve the request (rebuild-on-miss); no request → not-known; take chain_id from the request record’s own field (request_to_chain is the cache over it), which is set from Request Access step 5 onward — a request whose chain_id is still null is inside its initiation window and returns not-pending, since there is no chain to decide yet.
Credential.verify(actor_ref, credential_type, credential) → either failed-verification reason returns Credential Invalid. The approver’s credential must verify at decision time (Invariant 6).
MultiPartyApproval.approve_step(actor_ref, credential, chain_id, step_id, reason?) → propagates invalid-request | not-known | not-pending | unauthorized unchanged; its invalid-credential re-levels to Credential Invalid; its recording-failure → recording-failure (the substrate’s own recovery owns that partial). On any rejection nothing further runs — with one exception: not-pending still runs step 5 before returning it. A chain the substrate reports already terminal may be terminal against a request still Pending (a decision whose invocation died between its substrate commit and its evaluation — Withdraw Request step 4 already treats its own not-pending this way); running the evaluation here is what lets the retry of a dead decision complete the request rather than stop at the door.
AuditTrail.record_action(action_ref=approval_step_decided, actor_ref, credential, data={request_id, chain_id, step_id, decision=approved, reason}), its event_id into request_to_events. On failure: the decision committed at step 3 and is not reported as a failure — audit_pending opens on the request and step 5 still runs (second standing rule).
Chain-state evaluation — under the per-request_id serialization the Concurrency edge case obliges (the read-evaluate-transition-cascade sequence is single-threaded per request, which is what makes the guard below a decision rather than a race): MultiPartyApproval.read_chain(actor_ref=application_actor_ref, {chain_id}) (the substrate’s declared two-argument, chains:read-gated query). Its permission-denied is a deployment wiring fault — the composition actor’s grant is a declared obligation — and it is never this caller’s rejection: the decision committed at step 3, so the action alerts, opens an audit_pending evaluation entry on the request (payload: evaluation-pending, the chain and step ids), and returns approved at step 6 as the second standing rule requires; the sweep’s approval-without-token and terminal-chain legs perform the evaluation once the grant is restored, and the entry closes when either lands its record. (An earlier draft surfaced this arm as recording-failure, contradicting step 6 and inviting a retry of an applied decision into not-pending.) Then by the chain’s state and the request’s:
- Approved → fire the provisioning cascade (below) iff the same conjunction the sweep’s second leg tests, tested here live: the request is non-terminal (Pending, or the Approved transient) ∧ no token in the dedicated Capability instance parses to this request_id (capability_to_request consulted with rebuild-on-miss over the instance’s scope-parse) ∧ no open audit_pending entry for access_provisioning_failed. If the conjunction holds, record the transient (request_store[request_id].state = Approved — the in-cascade marker) and fire; otherwise skip — the cascade ran, is running, or was refused. The request-state read alone is not the guard, and the reason is the rebuild: Approved is a transient no event maps to, so a request_store lost and rebuilt between an allocation and its access_provisioned record shows Pending, and a guard that trusted the state would allocate a second token for one request — the exact defect the token-existence conjunct forecloses. The conjunction plus the per-request_id serialization is what makes Invariant 2 hold under the substrate’s trailing-decision semantics.
- Rejected, request Pending or Approved → first resolve the terminal reason, because the chain record does not carry one. The substrate’s read_chain result returns the chain’s state and its event-id list, not a reason field: the terminal reason lives only in the chain_resolved event’s data. So take the chain’s terminal event id from that list and read it — AuditTrail.read_record(<terminal event_id>) — and use its data.reason. The fetch has its own failure landing, and it must not block the reconciliation: where the read fails or the event’s payload is unavailable (a recording-failure, or a payload past the substrate’s retention horizon), proceed with denial_reason = null and leave audit_pending open on the request, surfacing it the same way the other recovery paths do. The denial is a fact the chain has already established; withholding the state transition because its narration could not be fetched would trade a missing field for a stuck request. Then AuditTrail.record_action(action_ref=access_denied, actor_ref=application_actor_ref, credential=application_credential, data={request_id, state=Denied, denial_reason}), then request_store → Denied (index write). Already terminal → skip.
- Withdrawn, request Pending → the chain was withdrawn out from under the request (a concurrent Withdraw Request that has not completed its own recording): record access_request_withdrawn naming the reconciliation (actor_ref=application_actor_ref, credential=application_credential — no live withdrawing human is present in this invocation — with data={request_id, state=Withdrawn, reason} — the reason resolved by the same fetch the Rejected arm above names, from the chain_withdrawn event’s data.reason via the chain’s terminal event id, with the same null-plus-audit_pending landing where the fetch fails — the same data the concurrent path would write; Configuration’s system-attributed roster names this emission), transition the request to Withdrawn — idempotent with the concurrent path under the serialization. Already terminal → skip.
- Pending → no-op: the quorum is not yet resolved, nothing transitions, no event is emitted.
Return approved — the decision outcome, unconditionally, once step 3 committed. A cascade or recording failure after it surfaces through the request state (ProvisioningFailed, audit_pending) and the deployment’s alerts, never as this caller’s rejection: the approver’s decision is durable in the substrate, and a rejection here would invite a retry of an applied decision.

Mirrors Approve Step steps 1–6 with MultiPartyApproval.reject_step, decision=rejected, and reason required (the substrate requires it; step 1 size-checks it). Step 5’s evaluation runs identically — under all-of-N a rejection typically fires the Rejected arm.

Validate the primitives (reason required, size-checked) → invalid-request. Look up the request (rebuild-on-miss); none → not-known; state not Pending → not-pending.
Credential.verify(actor_ref, credential_type, credential) → either failure reason → Credential Invalid.
Validate actor_ref == request.requestor_ref → unauthorized otherwise. Withdrawal is the requestor’s own act, structurally: the underlying chain admits withdrawal only from its initiator — who is the requestor, by Request Access step 5’s construction — so no non-requestor path exists to promise (Edge cases — Third-party withdrawal is deliberately absent). No composition-layer Permissions check runs; the substrate’s own chains:withdraw gate is the permission surface (step 4).
MultiPartyApproval.withdraw_chain(actor_ref, credential, chain_id=<the request record's chain_id>, reason) — a null chain_id (the initiation window) is not-pending, nothing to withdraw yet — under the same per-request_id serialization as Approve Step step 5, so this call and any concurrent decision’s evaluation cannot interleave. Rejection mapping: not-pending — the chain reached a terminal concurrently — triggers the step-5 evaluation of Approve Step here and now (read the chain, set the request to the terminal the chain actually reached, with its event), then returns not-pending to this caller, whose withdrawal lost the race to a real outcome; permission-denied → the requestor lacks chains:withdraw in the substrate’s Permissions instance — the double-gate requestor-grant obligation the deployment wires (Composes); a deployment wiring fault to alert on, surfaced as Permission Denied so the caller learns the true cause (the same treatment as Request Access step 5’s substrate arm); unauthorized → unreachable by construction once step 3 enforced requestor-only, since the requestor is the chain’s initiator — observing it means the request’s requestor_ref and the chain’s initiator_ref disagree, a conformance fault to alert on, surfaced as recording-failure; invalid-credential → Credential Invalid; not-known → recording-failure (an index resolved a chain the substrate does not know — a rebuild-then-alert conformance fault); invalid-request → invalid-request; recording-failure(step) → recording-failure.
AuditTrail.record_action(action_ref=access_request_withdrawn, actor_ref, credential, data={request_id, state=Withdrawn, reason}); request_store → Withdrawn (index write). On recording failure: the chain withdrawal committed and is irreversible — return withdrawn with audit_pending open (second standing rule).
Return withdrawn.

exercise_access(session_token, capability_token) → exercised | rejected(session-invalid(reason) | capability-invalid(reason))

Session.validate(session_token) → valid(principal_ref, expires_at) or invalid(expired | revoked | not-known). Not valid → rejected(session-invalid(reason)), immediately, before the Capability is touched; nothing is logged or recorded for a failed session gate (the substrate cannot attribute an event to a session that does not validate, and a Failed-Attempt Log (forthcoming) composing pattern owns pre-authentication attempt auditing, as in the substrate’s own edge case). The returned principal_ref is the exercise record’s identity.
Write the intent, then redeem. Resolve the token’s request_id before anything is consumed: capability_to_request (rebuild-on-miss over the Capability store, whose record and composed scope exist independent of redemption). A token resolving to nothing is the not-known arm below — no request, no intent to write. For a resolved request, durably open an audit_pending exercise intent entry on it — carrying the pending payload (session_principal_ref, exercised_at; the action_ref is fixed by the outcome) — before Capability.redeem is called, and hold the per-request_id serialization from the entry’s open through the redeem call’s return (Concurrency): at most one exercise intent entry is open per request at any instant, which is what makes the redemption-reconciliation leg decidable — with one open entry, a counter one ahead of the recorded exercises can belong to nothing else. The marker-before-act ordering means a crash between the redemption and its record leaves its own durable evidence rather than a silent gap. The entry’s own failure landing: a store refusal opening it is rejected(capability-invalid(recording-failure)) with nothing consumed — redeem is not called, the serialization is released, and the caller retries. The entry carries the invocation’s invocation_id, which is the key the recovery discipline’s pre-check pairs it to its landed record by. Then Capability.redeem(capability_token):
- redeemed(scope, allocator_ref) → the composed scope confirms the request_id (the constituent’s own record carried the binding; an allocator_ref other than application_actor_ref is impossible on the dedicated instance and read as a conformance fault if ever observed). The redemption is committed and irreversible — one use is consumed — and before the serialization is released, the intent entry is durably marked redeemed (its action_ref fixed to access_exercised): from this instant the entry says a use was consumed and its record is owed, which is a different fact from an exercise was intended, and the redemption-reconciliation leg reads the two apart. Every path from here returns exercised.
- invalid(exhausted | expired | revoked) → the request is already resolved and its intent entry open (this step’s pre-write) → proceed to step 3’s failure recording → rejected(capability-invalid(reason)). A presented-but-dead token is an auditable event.
- invalid(not-known) → the token resolves to nothing: never allocated by this composition’s instance. rejected(capability-invalid(not-known)), recorded per step 3 with the declared null-request exception (Composition state payload requirement); the presented material itself is never recorded.
Record the outcome — AuditTrail.record_action(actor_ref=application_actor_ref, credential=application_credential, …) with action_ref=access_exercised and data={request_id, session_principal_ref, exercised_at, result=redeemed} on success, or action_ref=access_exercise_failed and data={request_id (null for not-known), session_principal_ref, exercised_at, reason} on an invalid(...) outcome — exercised_at from the seam-injected now; the event_id into request_to_events; session_access_log follows as a derived index over these events. Each landed record closes the step-2 intent entry. On recording failure after a committed redemption: return exercised with the intent entry left open, its payload standing (second standing rule — a rejection would invite a retry that consumes a second redemption); the recovery discipline lands the record. On recording failure over a failed presentation (the three dead-token reasons — exhausted, expired, revoked): the intent entry likewise stays open carrying the failure payload, and the record catches up (access_audit_recovery where the invocation is gone), preserving exactly the who-presented-a-dead-token evidence Invariants 5 and 10 claim; the caller still receives rejected(capability-invalid(reason)), since no act committed. For the not-known case there is no request to carry a marker — the unrecorded attempt is a declared bounded exception: the loss is bounded to never-allocated material presented during an audit outage (the presentation consumed nothing and granted nothing), named here rather than silent; a deployment needing even that attempt durable composes the Failed-Attempt Log (forthcoming) pattern.
Return exercised, or the step-2 rejection.

Exercise Access is deliberately not idempotent, and the at-most-once obligation is the caller’s. Each call presenting a live token consumes one redemption — that is the Capability’s contract and the point of a bounded-use token; the composition adds no idempotency key, because a replay-safe exercise would need a result memo this composition has no truth-store to hold (the same shape the Contract routes to an Idempotency Result Memo atom). What the composition guarantees instead: exercised is returned iff a redemption was consumed — including under recording failure — so a caller that treats any exercised as final and never blind-retries a timeout without checking Read Request cannot double-spend by mistake. A deployment automating exercise wires its own at-most-once delivery to this action.

Validate the primitives (reason required, size-checked) → invalid-request. Look up the request (rebuild-on-miss); none → not-known; state not Provisioned → Not Provisioned.
Credential.verify(actor_ref, credential_type, credential) → either failure reason → Credential Invalid.
Permissions.permitted(actor_ref, requests:revoke) → denied → Permission Denied.
Capability.revoke(capability_token=request_to_capability[request_id] (rebuild-on-miss), revoked_by_ref=actor_ref, reason). Rejection mapping: already-terminal → continue — the Capability is already dead (redeemed out, lapsed, or revoked by another path); the request-level revocation record still serves the audit; not-known after a rebuild → a conformance fault (the Capability store lacks a token its own scope-parse rebuild produced) — alert and recording-failure; invalid-request → unreachable for composition-built arguments; a deployment fault if observed; storage-failure → recording-failure, nothing transitioned, plain retry.
AuditTrail.record_action(action_ref=access_revoked, actor_ref, credential, data={request_id, state=Revoked, reason}); request_store → Revoked (index write). On recording failure: the constituent revocation committed — return revoked with audit_pending open.
Return revoked.

read_request(actor_ref, query) → ordered_sequence_of_requests | rejected(permission-denied | invalid-query) — a pure projection: no state change, no audit event, no credential (nothing here records).

Permissions.permitted(actor_ref, requests:read) → denied → Permission Denied, with no existence-hiding fork (a deployment wanting that posture builds it in its calling layer).
Query the request store on the declared filter axes: request_id, requestor_ref, resource_ref, access_scope, state, and time ranges on requested_at or expires_at in the {after, before} sub-key form. An unrecognized filter key, a blank filter value, or an undeclared state token is invalid-query; a well-formed query matching nothing returns an empty sequence.
Each result carries the request record’s fields (audit_pending included when set), the chain’s current state (via the substrate’s read_chain, as the composition actor), the provisioned Capability’s derived effective status where one exists (via Capability.read — a lapsed token honestly reads Expired), and the request’s audit event_ids from request_to_events — the declared request→audit traversal an auditor takes into the substrate’s own read_record / two-argument verify_record asymmetry. No raw capability_token or session_token appears in any result (Primitive policies — bearer material).
Results are ordered ascending by requested_at, tie-broken by ascending byte order of request_id — total and deterministic.

Provisioning cascade

The provisioning cascade fires inside Approve Step / Reject Step step 5 when the substrate reports the chain Approved and the request is Pending. It is internal — there is no caller-invokable provisioning action — and it runs under the same per-request_id serialization as the evaluation that fires it:

Capability.allocate(allocator_ref=application_actor_ref, scope=<composed scope: request_id, resource_ref, access_scope>, max_redemptions=max_redemptions_default, ttl=request.expires_at − now) — the remaining lifetime from the stored deadline and the seam-injected now; the expiry guard is structural rather than clock-branched: a request approved after its expires_at yields a non-positive ttl, which the atom’s own validation refuses (Edge cases — request expiry). Rejection mapping (the atom’s two arms, and only those): invalid-request → the remaining-ttl case above, or composition-built-argument disagreement (a genuine deployment fault — a scope-length refusal is foreclosed at intake by the composed-scope-aware caps, Primitive policies, so it cannot be a caller’s oversize mischaracterized) — open an audit_pending entry carrying the access_provisioning_failed payload (denial_reason = ttl-elapsed, or the relayed reason), then record access_provisioning_failed (actor_ref=application_actor_ref, credential=application_credential, data={request_id, state=ProvisioningFailed, denial_reason}), then transition request_store → ProvisioningFailed (index write) — the first standing rule’s order, record before index, with the marker giving the window its own evidence. The record’s own arms: recording-failure(step) or the deployment-fault invalid-credential → the entry stays open with its payload and the transition still proceeds, the marker retry or the sweep landing the record (access_audit_recovery at restart); invalid-request → unreachable for composition-built data, a deployment fault taking the same path. storage-failure from allocate → the same ProvisioningFailed path with the reason relayed. In both arms the Approve Step caller still receives approved (their decision committed; the failure is the request’s, surfaced in its state and the deployment’s alerts).
Record AuditTrail.record_action(action_ref=access_provisioned, actor_ref=application_actor_ref, credential=application_credential, data={request_id, requestor_ref, resource_ref, access_scope, state=Provisioned}) — no token in the payload — and transition request_store → Provisioned; populate request_to_capability / capability_to_request (index writes over the constituent truth the composed scope already carries). On recording failure: the allocation committed — audit_pending opens and the recovery discipline lands the record; the token is still delivered (step 3), because the access lawfully exists.
Deliver capability_token to the requestor via the deployment’s delivery channel — the only surface that carries the raw token (Composition state).

The compensation story is completion, not undo, and it is one sweep with detector legs for each window. Three crash windows exist around the evaluation, and each has a reachable detector — none relies on a later decision call, because under all-of-N every step is terminal the moment quorum fires and no later call ever reaches the evaluation; the third window, a decision committed against a chain that resolved Rejected or Withdrawn with no evaluation run, is the terminal-chain leg’s (the recovery discipline, below). Leg one — token without record (a crash between step 1’s committed allocation and step 2’s record): a token exists whose request never reached Provisioned. Nothing needs revoking — the chain was Approved, so the allocation is lawful; the recovery is to finish: the sweep enumerates the dedicated Capability instance, parses each composed scope, and for any token whose request_id is not in a Provisioned/Revoked request re-runs step 2 idempotently (the same check the breach-forensics scenario runs from outside, used from inside as the detector). Leg two — approval without token (a crash before step 1, or before the evaluation transitioned the request at all): the request sits Pending or Approved-transient against a chain the substrate reports Approved, with no token for it in the instance. The sweep’s second leg detects exactly that conjunction — request non-terminal ∧ chain Approved ∧ no token in the dedicated instance ∧ no open audit_pending entry for access_provisioning_failed (a request whose allocation failed and whose record is still pending rebuilds to Pending if its index write was lost, and the marker is what keeps the leg from allocating a token against a request the cascade already refused) — and fires the cascade under the per-request_id serialization, writing the Approved transient first where the crash preceded it; the detector’s own conjunction is the re-fire guard (an Approved request with a token is leg one’s case or already complete, never re-allocated), so the re-fire is single and idempotent. (A trailing decision call is not the recovery path: the step-5 guard rightly skips an already-Approved request, and under all-of-N no such call comes at all.)

The recovery discipline, named as one surface. One multi-entry marker and one four-leg sweep, triggered at restart and retried until closed, all surfaced via Read Request:

audit_pending (a request-record marker list — multi-entry, one entry per pending record) — an entry opens whenever a committed act’s audit record failed to land (the arms each action names), and in two places before the act as declared intent: Request Access step 4’s initiation entry and Exercise Access step 2’s exercise intent entry (each stated at its wiring step — the marker-before-act ordering is what gives a crash window its own evidence). Entries close independently as each record lands, so overlapping windows — a failed provisioning record followed by a failed exercise record in one outage, or two exercises of a multi-use token whose first record failed while the second proceeded — each hold their own entry with its own payload (two unmarked intent entries are never open simultaneously, since the serialization spans intent-to-redeem-to-mark; the first entry is marked redeemed before the second opens, and the reconciliation leg reads marked and unmarked entries apart); a single-slot marker could not carry the second owed record. Each open entry carries its payload: the exact action_ref and event data its pending record_action must carry — for an exercise, the session_principal_ref and exercised_at of the invocation, which exist in no constituent store — a durability obligation on the request record for exactly the open window (Composition state names it as the bounded truth-bearing exception); without it, a restart could not construct the record it owes. Where the original actor’s credential is in hand (same invocation), the record is retried as written; where recovery runs outside the invocation (restart), the substrate cannot re-attest the absent human, so the recovery record is access_audit_recovery, emitted by the composition actor, carrying the entry’s action_ref and full original data — the rebuilds treat a recovery record as standing in for the original it names. Entry writes are serialized: opening or closing an entry takes the per-request_id serialization (Concurrency), the exercise path included.
The completion-and-reconciliation sweep, five legs, all under the per-request_id serialization — the Capability-instance scope-parse detector (token without record → finish step 2 of the cascade), the approval-without-token detector (request non-terminal ∧ chain Approved ∧ no token → re-fire the evaluation-and-cascade; Provisioning cascade — the compensation story), the terminal-chain detector (request non-terminal ∧ chain Rejected or Withdrawn in the substrate → run the corresponding step-5 arm of Approve Step — record access_denied or access_request_withdrawn and transition the request — which is the leg that catches a decision whose invocation died between its substrate commit and its evaluation: no marker opens there, because step 4’s entry opens only on a returned record failure, and without this leg such a request sat Pending forever against a chain that had already refused it, its requestor never told. The same leg lands the dead decision’s own missing record: a step_approved / step_rejected event in the chain’s list that no approval_step_decided names is landed as access_audit_recovery for approval_step_decided, the decision’s data read from the substrate’s event), the redemption-reconciliation leg (over the open exercise entries on a request, of which several may stand — entries already marked redeemed, each a committed use whose record is owed, and at most one unmarked intent entry, because Exercise Access step 2 holds the serialization from the entry’s open through redeem’s return and the mark: compare the token’s consumed redemptions, the Capability record’s own counter, against the count of access_exercised events for the request plus the count of open entries marked redeemed (access_exercise_failed events consumed nothing and are not in the comparand). Every marked entry’s record is owed regardless of the count — the mark is the durable statement that its use was consumed — and the sweep lands access_audit_recovery for access_exercised with each one’s payload. The unmarked intent entry is then attributed by the remaining difference: counter one ahead means its redemption committed and the mark was lost with the crash, so it is marked and landed likewise; equal means the crash preceded the redemption — nothing was consumed, nothing is owed, and the entry is cleared; any other difference is a conformance finding. An earlier draft compared the counter against the events alone and read two open entries as a finding, when the page itself admitted that shape), and the initiation leg (for every open initiation entry — Request Access step 4 — probe the substrate: the chain present — by the request record’s stored chain_id where step 5 wrote it, or, where the crash preceded that write, a read_chain({subject_ref: request_id}) probe under the composition actor’s chains:read grant, after which the leg writes the found chain_id onto the record and into the entry’s payload — means the initiation committed — land the access_requested record via access_audit_recovery and the request proceeds; the chain absent means the initiation died before the substrate write — record access_request_withdrawn (composition actor, reason = initiation-failed(crash), carrying the full request shape from the entry’s payload exactly as Request Access step 5’s rejection arm does), transition the request Withdrawn, and close the entry, nothing having been promised to anyone, since the caller never received the id).

Four rules govern every leg, stated once. (1) Pre-check before emitting. Every leg detects on rebuilt state and the absence of the event, never on an index alone: before it emits any record, the sweep enumerates the trail by the declared route for an event carrying the same action_ref and the same invocation_id as the entry or act it is about to land, and where one exists it closes the entry without emitting — an index that was stale while the event had already landed is a rebuild trigger, and record_action is not idempotent, so a leg that trusted the index re-emitted duplicates. The pairing is by invocation_id, carried on every event and every entry (Composition state’s payload requirement), so it is exact; where an entry predates that field the pre-check falls back to the entry’s own payload fields (request_id, action_ref, exercised_at, session_principal_ref), names the candidate events it finds, and lands nothing while more than one matches. (2) The lower edge. A leg whose window opens outside the serialization’s hold — the redemption-reconciliation leg, over entries whose record write runs after the hold is released — examines no entry younger than recording_completion_bound (Configuration); the legs whose windows sit wholly inside the hold need none, a live invocation holding the serialization the sweep must take first. Every leg’s upper edge is the audit horizon: an event absent past it is destruction, and the request record’s truth-bearing half is the answer, not a recovery. (3) As the composition, behind a recovery record. Every write the sweep makes is attested under application_actor_ref / application_credential — the original actor is not present, and the recovery record carries them in its data — and every leg that commits constituent state or emits a state-transition record outside the invocation that owed it writes access_recovery_intended first: data = {invocation_id, request_id, leg, plan} naming the entry or conjunction it detected and what it is about to do (an allocation, a denial record, a withdrawal, a landed exercise), so the trail shows the act was occasioned by the sweep and not by a direct call; access_audit_recovery then stands in for the original record, carrying the entry’s action_ref, its full original data, and its invocation_id. (4) Re-derive, never remember. What a recovery record carries comes from the entry’s payload, the constituent stores, or the substrate’s own events — the decision’s data read from the chain’s event, the denial reason from the terminal event, the binding from the Capability record’s composed scope — and where the entry’s payload is the only source (an exercise’s session_principal_ref and exercised_at), that payload is the truth-bearing state Composition state names and Outbox will own; a lost entry there is a finding, not something the sweep reconstructs.

The markers live on records and events the composition already writes; there is no second store and no cadence knob — the trigger is restart plus retry-until-closed, and the open state is never silent: Read Request surfaces audit_pending, and the auditor’s closure procedure is named in Generation acceptance.

Scope vocabulary

The composition defines these scopes for its Permissions instance:

Scope	Permits
Requests Initiate	Call Request Access
Requests Revoke	Call Revoke Access on any provisioned request
Requests Read	Query request records and their associated chain, capability, and audit events

There is deliberately no requests:withdraw scope: Withdraw Request is the requestor’s own act, structurally — the underlying chain admits withdrawal only from its initiator, so a third-party grant would promise a path the substrate refuses (Edge cases — Third-party withdrawal is deliberately absent).

Behavior

Approval-gates-provisioning is structurally enforced, not advisory. The action wiring makes it impossible to allocate a Capability for a request via the composition’s surface without the Multi-Party Approval chain for that request reaching Approved. The provisioning cascade is the only path from chain-approval to capability-allocation; there is no provision_access action a caller can invoke directly. An implementation that provides a direct provisioning path outside the cascade violates Invariant 1.
Session validity is the first check at access exercise, not an afterthought. Exercise Access calls Session.validate before touching the Capability. A revoked or expired session blocks the exercise regardless of whether the Capability is still valid. This is the composition’s enforcement of the cascading-revocation invariant: Credential revocation → Session invalidation (via Login) → Exercise Access returns Session Invalid → privileged access blocked without any direct action on the Capability or the request record.
The Capability’s bearer-key property is preserved, not subverted. The composition adds no identity check at redemption time: Exercise Access takes a session_token (the authenticated channel) and a capability_token (presented to the Capability atom), and the atom records no redeemer — its declared asymmetry stands. The identity in the exercise record is the session’s principal_ref, which Session.validate’s own declared return supplies — no reach inside the atom, no field the composition was not given. Neither bearer token appears in the record (Primitive policies): the exercise event names the principal and the request, which is what an auditor needs, and grants nothing, which is what a leaked trail must not do. The asymmetry, stated precisely: the token never knows its bearer; the exercise record names the session’s authenticated principal at the moment of presentation.
One Audit Trail covers the full arc. Every event from access_requested through approval decisions through access_provisioned through each access_exercised through access_revoked is recorded in the same Audit Trail instance. The temporal sequence of these events in the Event Log is the structural form of the full arc. No second store is required to reconstruct the arc; no correlation step is needed.
Approver authorization is enforced by the approver_set, not by a Permissions grant. Approve Step and Reject Step do not call Permissions.permitted on the deciding actor. Approver authorization is encoded in the approver_set declared at chain initiation and enforced at the Multi-Party Approval level — the atom rejects any step decision from an actor not in the approver_set for that step. Adding a Permissions.permitted(actor_ref, requests:approve) check at this composition’s layer would double-enforce an already-enforced rule via a different mechanism, creating two failure modes for the same condition. The composition’s authorization for step decisions is limited to credential validity (Credential.verify) and approver-set membership (Multi-Party Approval’s enforcement). This is the composition’s deliberate design, not an oversight.
Credential revocation blocks both new requests and existing approvals. If an approver’s Credential is revoked between chain initiation and their decision, step 2 of Approve Step (Credential.verify) returns failed-verification(no-active-credential) and the step is rejected with Credential Invalid. The approval chain remains in-flight; the revoked approver’s step remains Pending. The chain can be withdrawn and re-initiated with a replacement approver. This is the correct behavior: a decision from a revoked actor is not valid evidence of approval.

Composition-level invariants

The composition’s three structural relations. Per spec-format.md §Structural-relation invariant templates, a declared relation carries its cardinality and modality:

request → chain — one-to-one, mandatory on both sides at quiescence with no open initiation entry, over requests that reached a chain. A request closed inside its initiation window — Request Access step 5’s rejection arm, or the sweep’s chain-absent closure — is Withdrawn with chain_id null and is carved out of this relation by that state: it never had a chain and never will, and its initiation-failed withdrawal event is its whole record. Every request opened through Request Access has exactly one substrate chain (subject_ref = request_id) — the request record commits first (step 4’s durable pre-write) and the chain follows, so the one directional window is a request briefly chain-less inside its open initiation entry, a declared bounded transient the sweep’s initiation leg closes (the chain found and its access_requested landed, or the entry closed with the request Withdrawn). Every chain in the composition’s substrate instance belongs to exactly one request whose record precedes it — the pre-write ordering is what makes an orphan chain unreachable by construction (the quantifier stands: chains initiated around this composition are not covered — it declares exactly one way in). Invariants 1 and 2 ride this relation.
request → capability — one-to-zero-or-one, at most one ever. A request acquires at most one token across the lifetime of the system, at provisioning; the binding lives in the token’s own composed scope (Capability’s immutable record), and the maps over it are derived indexes. Invariant 2 states the bijection over the provisioned subset.
request → audit events — one-to-many, at least one per request, mandatory on the event side. Every request carries at least its access_requested (or, in the recovery window’s closure, its access_audit_recovery; or, for a request closed inside its initiation window, its full-shape initiation-failed access_request_withdrawn) event, plus one event per state transition and per exercise outcome; every event of this composition names an existing request in its data request_id, with the one declared null-request exception (a not-known exercise attempt). The traversal is request_to_events (Composition state).

The inverse directions are read through the derived indexes; a lost index entry is a rebuild trigger, never a relation violation.

Invariant 1 — Approval-gates-provisioning (within the audit horizon). Every Capability token in the composition’s dedicated instance parses (via its composed scope) to a request_id whose Multi-Party Approval chain is in Approved state — recomputable by any reader from the chain and step records under the substrate’s own quorum determinism while those records’ payloads survive; past the horizon (Configuration’s ordering obligation) the token’s request record, its Provisioned state, and the surviving access_provisioned attestation are the evidence, and a token older than the horizon is not a bypass finding but a horizon finding against the deployment’s ordering. The provisioning cascade is the only allocation path through this composition’s surface, it fires only on the substrate’s reported Approved, and it runs under the per-request_id serialization, so no interleaving produces a token ahead of its approval. A token whose scope names an un-Approved chain — or one whose scope parses to no request — is evidence of a provisioning bypass, a critical control failure. Rests on: the cascade’s sole-path construction, Approve Step step 5’s guard, the composed scope (Primitive policies), and the substrate’s Invariant 2 (quorum determinism).

Invariant 2 — Request-capability bijection (at quiescence, under the declared serialization). Each request_id acquires at most one capability_token across the lifetime of the system; re-access requires a new request and a new chain. The defense is named, not assumed: the read-evaluate-transition-cascade sequence of Approve Step/Reject Step step 5 is serialized per request_id (Concurrency), so two decision calls cannot both observe Pending and both fire the cascade — without that obligation the guard is a read-then-act race and the invariant is unenforceable. The crash window between allocation and its record is closed by the completion sweep (the recovery discipline), which finishes, never re-allocates. Rests on: step 5’s fire conjunction under the serialization — request non-terminal, no token in the dedicated instance parsing to the request, no open provisioning-failed entry — which is the sweep’s own detector run live, and not the request-state read alone (the Approved transient rebuilds to Pending); the completion sweep; Capability’s no-token-reuse.

Invariant 3 — Session-gated exercise. Every access_exercised event was produced by an Exercise Access call whose first step obtained valid(principal_ref, expires_at) from Session.validate in that same call, before the Capability was presented; the event’s session_principal_ref is that return’s principal. No token is redeemed through this composition’s surface without the session gate passing first.

Invariant 4 — Cascading-revocation chain (conditional on the wired session-issuance surface). Where the deployment wires Login (or an equivalent issuance surface honoring the same credential→session revocation cascade), revoking a principal’s Credential closes their exercise surface end-to-end with no action on the request or the token: Credential.revoke makes the credential terminal; Login’s declared peer action revoke_sessions_for_credential(credential_id, revoked_by_ref, reason) — the named provenance of the session half, with its own snapshot-scoped cascade-completeness invariant — moves every session derived from it to a terminal state; and any subsequent Exercise Access under such a session returns Session Invalid at step 1, before the Capability is presented. The condition is honest, not decorative: Login is a peer, not a constituent (Composition notes), and a deployment issuing sessions through a surface with no credential→session cascade does not get this invariant — this composition’s own gate still refuses whatever the Session store calls terminal, but nothing here makes the credential revocation reach the sessions. The chain spans Credential → Login’s cascade → Session → this composition’s gate, and is expressible at no single layer. Where a deployment also wants the token dead immediately, that is Revoke Access’s job, wired by a listener (Edge cases).

Invariant 5 — Audit-arc completeness (at quiescence, within the audit horizon). With no invocation in flight and no audit_pending entry open, and for events not yet past the horizon (Configuration): every request has its access_requested event (or the recovery record standing in for it); every state the request store shows is the state its latest transition event declares; every consumed redemption has its access_exercised event and every reached-the-atom failed presentation its access_exercise_failed event (with one declared exception: a not-known presentation whose recording failed has no request to carry a marker — the bounded evidence loss Exercise Access step 3 names); and session_access_log agrees with those events by construction, because it is a derived index over them — the correspondence needs no second mechanism and has no second direction to establish. Inside a recovery window the gap is open but never silent: the marker is set, Read Request surfaces it, and the recovery discipline closes it. An auditor reconstructs the full arc from the Audit Trail alone, through request_to_events.

Invariant 6 — Approver-credential completeness (through this composition’s surface). Every approval decision routed through Approve Step / Reject Step carried a Credential.verify(actor_ref, credential_type, credential) → verified immediately before the substrate call, so no decision this composition routed is attributed to an actor whose credential did not verify at decision time. The qualifier is the honest scope: a decision written into the substrate around this composition is the substrate’s business, not this invariant’s.

Invariant 7 — Denial completeness (at quiescence, within the audit horizon). Every request in Denied has its access_denied event naming the terminal state and denial_reason — or denial_reason = null with audit_pending open, the declared landing for a terminal-reason fetch that failed (Approve Step step 5). The reason is not a field of the chain record; it is read from the chain’s terminal event, so it is subject to that read’s availability and, past the substrate’s retention horizon, to the payload’s. Stating the null arm here is what keeps this invariant true rather than aspirational: a denial whose narration could not be fetched is still a denial, and the audit_pending marker is what distinguishes it from one that was never recorded, and its chain shows Rejected; every request in ProvisioningFailed has its access_provisioning_failed event with the relayed reason, or an open audit_pending entry carrying it (the cascade’s record-before-index order with its marker, Provisioning cascade). An auditor determines from the records alone which requests were refused, by which quorum failure or provisioning fault, and when.

Invariant 8 — Immutable request identity. Once a request record is created, request_id, requestor_ref, resource_ref, access_scope, justification, requested_at, and expires_at never change. The state field advances forward only — Approved is the declared in-cascade transient, and no terminal state returns to Pending; the recovery marker audit_pending is a multi-entry list, each entry opened once and closed once per its own window, and is not a state.

Invariant 9 — Single audit instance (deployment-declared; verified in two halves). One Audit Trail instance receives the whole arc: the substrate’s chain events and this composition’s request, provisioning, exercise, and revocation events. The records-alone half, within the horizon: every event request_to_events names for any request resolves in the one instance the deployment declares, and the arc reconstruction of Generation acceptance succeeds against that instance alone. The topology half — that no second instance exists receiving a fork of these event classes — is not provable from any one instance’s records and is an externally-clearable check (Generation acceptance names it there). A deployment that fragments the arc has an auditor reading an incomplete record.

Invariant 10 — Exercise-record durability (inherited, not parallel). The exercise history is substrate truth: access_exercised / access_exercise_failed events are ordinary audit events under the substrate’s own append-only, retention-governed, tamper-evident guarantees, and session_access_log is a derived index over them — never modified, because its sources never are, and rebuildable at any time. A log entry with result = capability-invalid(revoked) is durable evidence that someone presented a revoked token under a valid session, auditable from the substrate alone.

Examples

Happy path — privileged database access under two-approver gate

An engineer requests read access to a production database for incident investigation:

request_access(requestor_ref: eng_u42, credential: cred_e42, resource_ref: db::prod::incidents, access_scope: "read", justification: "INC-2891 investigation — prod log correlation", approver_set: [mgr_u10, sec_u03], quorum_rule: all-of-2, ttl: 3600) → request_id: req_p7h3k2

Both approvers receive Assignment in-tray notifications. The security lead approves first:

approve_step(actor_ref: sec_u03, request_id: req_p7h3k2, step_id: step_s1, reason: "INC-2891 confirmed active", credential: cred_s03)

The chain is still Pending (one of two). The manager approves:

approve_step(actor_ref: mgr_u10, request_id: req_p7h3k2, step_id: step_s2, reason: "authorized", credential: cred_m10)

The chain reaches Approved. The provisioning cascade fires: Capability.allocate(allocator_ref: svc_pap, scope: <composed: req_p7h3k2, db::prod::incidents, "read">, max_redemptions: 1, ttl: 3387) → capability_token: cap_9f2d1e — the ttl is the remaining lifetime, expires_at − now: 213 seconds of the requested 3600 elapsed while the two approvals were gathered, and the token’s window honestly ends where the request’s does. The access_provisioned event records the request, never the token. The request transitions to Provisioned; the engineer receives cap_9f2d1e through the delivery channel.

The engineer authenticates (via Login, out of scope here) and acquires session_token: sess_a4b7c1. They exercise the access:

exercise_access(session_token: sess_a4b7c1, capability_token: cap_9f2d1e) → exercised

Session validates as valid(principal_ref: eng_u42, expires_at: …). The Capability redeems — redeemed(scope, allocator_ref: svc_pap), the composed scope parsing back to req_p7h3k2 — and its remaining-redemptions counter decrements 1 → 0, moving the stored status to Redeemed (terminal). The Audit Trail records access_exercised with {request_id: req_p7h3k2, session_principal_ref: eng_u42, exercised_at, result: redeemed}; session_access_log derives the entry from that event.

Rejection path — first approver rejects; quorum unachievable

A request under all-of-2 quorum receives a rejection from the first approver:

reject_step(actor_ref: sec_u03, request_id: req_q5m8n1, step_id: step_s1, reason: "requestor does not have business need for this scope", credential: cred_s03)

Under all-of-2, one rejection makes quorum unachievable. Multi-Party Approval transitions the chain to Rejected. The composition detects this at step 5 of Reject Step and transitions the request to Denied, recording denial_reason. The Audit Trail records access_denied. No Capability is ever allocated. Any subsequent Exercise Access attempt with a made-up token returns rejected(capability-invalid(not-known)) — no token was ever issued for this request, so there is nothing in the dedicated Capability instance to present.

Rejection path — session invalid at exercise time

An engineer was provisioned access (Capability token issued after approval). Before they can exercise it, an administrator revokes their Credential (employment terminated):

Credential.revoke(credential_id: cred_e42, revoked_by_ref: hr_admin, reason: "employment-terminated")

The Login composition detects this and invalidates all Sessions derived from cred_e42, including sess_a4b7c1. The Session record transitions to Revoked.

The engineer (or an attacker with their token) attempts:

exercise_access(session_token: sess_a4b7c1, capability_token: cap_9f2d1e) → rejected(session-invalid(revoked))

Session.validate(sess_a4b7c1) returns invalid(revoked). The Capability is never presented. The Capability token cap_9f2d1e remains in Allocated state — unconsumed and revocable, until Revoke Access or its own deadline lapses it. No audit event is recorded for this attempt (the session gate refused before anything attributable happened — the Failed-Attempt Log (forthcoming) pattern owns pre-authentication attempt auditing).

Rejection path — forged token under a valid session

The gate’s rejecting arm, fired: an insider with a perfectly valid session guesses at a token that was never provisioned:

exercise_access(session_token: sess_k9r2m4, capability_token: cap_FORGED) → rejected(capability-invalid(not-known))

Session validates as valid(principal_ref: user_u77, …) — the session gate passes. Capability.redeem(cap_FORGED) returns invalid(not-known): the dedicated instance never allocated it, so it traces to no approval and grants nothing. The attempt is recorded — access_exercise_failed with {request_id: null, session_principal_ref: user_u77, reason: not-known} (the declared null-request exception; the forged material itself is never written) — so the auditor sees who, under a real session, presented a token the system never issued. The approval gate is visible here in its refusing mode: no chain, no token, no access, and a named principal attached to the attempt.

Regulated adversarial scenarios

Three scenarios the composition must survive in regulated contexts:

Regulator audit — SOX §404 privileged access control. An external auditor asks “can you prove that no one accessed the production financial database with elevated privileges without documented, multi-party authorization?” The walk uses the declared surfaces, not payload-field queries the substrate does not offer: read_request({resource_ref: db::prod::financials}) returns every request ever opened against the resource, each carrying its state and its request_to_events ids. For each Provisioned request the auditor takes the event ids into the substrate — access_provisioned, then every access_exercised — and traces the approval side through request_to_chain to the chain’s own step records, recomputing the quorum outcome under the substrate’s Invariant 2. Invariant 1 closes the other direction: enumerating the dedicated Capability instance and parsing each composed scope proves every token that exists traces to an Approved chain — no orphan tokens, no single-approver grants. SOX §404 is satisfied from the records alone.

Disputed access — former employee denies using privileged token. A security investigation reveals the production credentials database was queried at 2026-11-14T03:22:00Z. A former employee claims they did not access it. The investigator runs read_request({resource_ref: db::prod::credentials}), finds req_r9s4t1 provisioned that night, and reads its events: the access_exercised event at 03:22:11Z carries session_principal_ref: user_u88 — the identity Session.validate returned at the moment of exercise, recorded in the event itself rather than recovered by a later cross-reference. The approval chain for req_r9s4t1 shows the same principal as requestor_ref, with both approvals attested at 02:58Z. Invariant 3 guarantees the session gate passed in the same call; the Session store corroborates a session issued to user_u88 at 03:15Z. The denial cannot be sustained against the structural record; a credential-compromise reinterpretation is the Compromise Disclosure (forthcoming) pattern’s business, never a mutation of this trail.

HIPAA break-glass access trace — clinical PHI access audit. A compliance officer must demonstrate to an OCR (Office for Civil Rights) auditor that a nurse’s emergency break-glass access to a patient record on 2026-09-12 was authorized and documented. read_request({resource_ref: ehr::patient::p4471}) returns req_h8k3n2; its events show the arc in order: access_requested (justification: “INC-4418 cardiac event — emergency PHI (Protected Health Information) access required”), the chain’s two approval decisions (charge nurse + attending physician, all-of-2, credentials verified at decision time — Invariant 6), access_provisioned, and one access_exercised at 02:44Z carrying session_principal_ref: nurse_n21. The full arc is present in the one Audit Trail instance (Invariant 9’s records-alone half); HIPAA §164.312(b)’s access-audit requirement is satisfied from the records alone.

Breach investigation — approval gate bypassed? A security team finds an access_exercised event at 2026-12-01T18:44Z against a high-security vault and asks whether the approval gate was bypassed. The event’s request_id leads to req_v2w5x8: state Provisioned, chain Approved, two decision records, quorum recomputation clean. Then the systemic half — the same check the recovery discipline runs from inside: enumerate the dedicated Capability instance and parse every composed scope. A token whose scope parses to no request, to a request whose chain is not Approved, or that fails to parse at all is evidence of out-of-band allocation. All tokens accounting for themselves is the structural no-bypass answer; Invariant 1 makes the check deterministic.

Non-goals and edge cases

Approval chain composition belongs to Multi-Party Approval. This composition surfaces the chain-initiation and step-decision actions as pass-throughs. The quorum rules (all-of-N, M-of-N, one-of-N), the trailing-decision behavior, the partial-failure recovery paths, and the cascading withdrawal logic are all owned by Multi-Party Approval. See its specification for those details.
Capability expiry is derived, never written — here or in the atom. When a Provisioned request’s token deadline passes without exercise, nothing transitions anywhere: the Capability atom has no expire action and stores no expiry (its Invariant 13 — a lapsed record is shown Expired by the read projection’s Effective Status, computed from the immutable deadline and the injected clock), and the request record’s state remains Provisioned, because Provisioned names what this composition did, not whether the token is still live. A subsequent Exercise Access returns rejected(capability-invalid(expired)) from the atom’s own derivation; Read Request shows the honest pair — request Provisioned, capability effective status Expired. There is no background scheduler to run and no write for one to perform.
Request expiry is guarded structurally, at the one place access could arise. expires_at is read at exactly one guard-bearing point: the provisioning cascade’s ttl = expires_at − now arithmetic, whose non-positive result the Capability’s own positive-ttl validation refuses — an expired request that later clears its chain lands ProvisioningFailed(ttl-elapsed) without a clock branch in this composition (Logic confinement: the constituent’s seam owns the guard). Pre-provisioning actions on an expired request are deliberately not clock-gated: approvals may still be recorded — they are decisions of record either way — and the expiry bites where it matters, at provisioning, the only step that could mint access. A deployment wanting stale requests withdrawn rather than left to fail at provisioning wires a scheduler that calls Withdraw Request past a business deadline — an ordinary, attributed withdrawal, exactly the shape the substrate’s own no-deadline non-goal prescribes.
Re-access after expiry or revocation requires a new request. There is no renew or re-provision action. If access is needed after the Capability expires or is revoked, the requestor calls Request Access again with a fresh justification, which initiates a new approval chain. The old request record and its chain remain in the store as immutable history. Invariant 2 (request-capability bijection) guarantees no second Capability is issued against the old request_id.
ProvisioningFailed is a terminal state requiring a new request. If the provisioning cascade fires but Capability.allocate returns a rejection (resource exhaustion, allocation service failure, TTL already elapsed), the request transitions to ProvisioningFailed. The approval chain record remains in Approved state — the approvers’ decisions are valid and durable. However, the chain cannot be re-used: ProvisioningFailed is terminal for the request record. The requestor must call Request Access again with a fresh justification, which initiates a new chain requiring the same (or a newly configured) approval set. The ProvisioningFailed record and the corresponding access_provisioning_failed Audit Trail event remain as permanent history. Notifying the requestor of ProvisioningFailed is a deployment obligation — the composition fires the cascade internally after an Approve Step call; the requestor is not present at that call and receives no automatic notification. A deployment must wire the access_provisioning_failed Audit Trail event to a notification or inbox mechanism so the requestor knows their request failed to provision and can retry. Operational runbooks for deployments where Capability.allocate has meaningful failure rates should instrument on access_provisioning_failed events and alert; silent ProvisioningFailed accumulation indicates a capacity or configuration problem.
Credential revocation of the requestor does not auto-revoke the Capability. Revoking the requestor’s Credential invalidates their Sessions, which blocks Exercise Access via the session check. But the Capability token itself remains Allocated until its TTL expires or an administrator calls Revoke Access. A deployment that requires immediate Capability revocation on Credential revocation must implement a listener that calls Revoke Access when Credential revocation events appear in the Audit Trail. This composition does not implement that listener; it is a composing-system obligation. The composition provides the Revoke Access action precisely to support this pattern.
Concurrency. Two serialization obligations, implementation-owned. (1) Per-request_id: the chain-state evaluation and provisioning cascade (Approve Step/Reject Step step 5), Withdraw Request’s chain call and reconciliation, and Revoke Access’s transition serialize on the request_id — the guard that forecloses a double allocation (Invariant 2) reads request state and fires the cascade, and unserialized readers could both observe Pending; the substrate’s own per-chain mutex covers its side but cannot cover this layer’s request-state read. (2) The recovery discipline’s closures (the audit_pending retry and the completion sweep) take the same per-request_id serialization, so a recovery and a live invocation cannot both act on one request’s open window. Exercise Access takes the per-request_id serialization from the step-2 intent entry’s open through Capability.redeem’s return, and again to close the entry at step 3. The atom’s counter would serialize the redemption on its own; what the composition serializes is the pairing of one open entry with one redemption, so the redemption-reconciliation leg has at most one entry to attribute a counter step to. The cost is that two exercises of a multi-use token on one request serialize on the redeem (not on the whole action — steps 1 and 3’s record write run outside the hold), which a break-glass deployment accepts for a decidable audit. Read Request is a pure projection, excluded from every obligation.
Delivering the Capability token to the requestor is handled at the deployment layer. The composition allocates the Capability token and records it in request_to_capability. Delivering it to the requestor — via notification, response payload, or a secure channel — is the deployment’s responsibility. The Capability atom’s allocate action returns the token to the composition; the composition records it and surfaces it in the provisioning cascade’s step 3. The delivery mechanism (push notification, pull from a secure store, email link) is out of scope.
This composition does not implement Login. Session issuance (Credential verification → Session.issue) is Login’s. This composition assumes sessions have already been established by Login and validates them at access-exercise time. A deployment that has not wired Login must satisfy the session-validation precondition through an equivalent mechanism.
Third-party withdrawal is deliberately absent. An earlier draft promised a requests:withdraw-holding administrator the power to withdraw any request; the promise was structurally empty — the substrate’s chain withdrawal is initiator-only, so every non-requestor call died in its unauthorized — and this composition now states the substrate’s discipline instead of promising around it: Withdraw Request is the requestor’s own act, enforced at step 3. The administrative needs the dropped path appeared to serve have honest homes: a Pending request an organization must kill is refused through the approval surface itself (an approver rejects a step, and quorum-unreachability lands the request in Denied — an attributed, negative decision of record, which is what an administrative kill is); a provisioned request is closed by Revoke Access; and a requestor who has left mid-flight leaves a chain that simply never resolves, withdrawable by no one but harmless — approvers’ in-tray items are discharged by their own decisions, and provisioning never fires without quorum. A deployment for which none of those suffice is asking for a substrate-level administrative withdrawal, a Multi-Party Approval matter to raise there, not a promise this layer can keep.
Authorization policy — who may request access to what — is a deployment configuration. The composition checks Permissions for requests:initiate before accepting a request, but it does not define the policy for which principals may request access to which resources. That policy is encoded in the Permissions store’s grant records and is owned by the deployment’s authorization surface. This composition enforces that the policy is checked; it does not define the policy.
Multi-use Capability tokens. max_redemptions defaults to 1 (single-exercise), but the composition supports max_redemptions > 1 for break-glass or time-boxed access scenarios. When max_redemptions > 1, the session_access_log records each exercise separately; the Capability’s remaining_redemptions counter decrements on each redeem call; the token is exhausted when the counter reaches 0 (Capability state: Redeemed); the request does not transition on exhaustion — its request_store state remains Provisioned until explicit revocation or natural expiry. An auditor reading both stores recovers the full usage picture.
Clock semantics. now — used to stamp requested_at / exercised_at and to compute the derived deadlines expires_at and the Capability.allocate remaining-lifetime ttl — is the injected clock_t supplied at the composition’s single I/O seam (see Logic confinement); no action reads a wall clock internally and no signature carries a now parameter. Clock quality — honesty, monotonicity, skew relative to the constituents’ own seams — remains a deployment matter. Skew between this composition’s injected reading and the Session or Capability seam can shift an access exercise across a TTL boundary at the margin. The Generation acceptance session-gating check therefore compares recorded evidence — the event’s exercised_at against the Session record’s own issue and expiry stamps — and its verdict at the boundary is honestly bounded: two stamps from two seams cannot prove which side of a shared instant an exercise fell on, so the check condemns only violations wider than the deployment’s operating skew and reads boundary-width discrepancies as inconclusive rather than as findings. Nothing load-bearing rests on cross-seam comparison — the gate itself ran against Session’s own seam, which is the enforcement; the check audits the evidence trail of that enforcement. Where privileged-access timestamps carry legal or forensic force, a Trusted Timestamping (forthcoming) pattern (the one Audit Trail’s externally-clearable clock check names) supplies the verifiable anchor; the residual risk under injection is a deployment that injects a dishonest now, not an internal race.

Composition notes

Login — the upstream composition that issues Sessions. This composition depends on Sessions being issued by Login (Credential.verify → Session.issue → session_token returned to principal). Without Login or an equivalent session-issuance surface, Exercise Access always returns session-invalid(not-known). Login is a peer composition, not a constituent; the two share the same Session and Credential atoms but own distinct composition-level surfaces.
Session-Gated Authorization — a peer composition that gates permission checks on session validity. Privileged Access Provisioning gates Capability redemption on session validity; Session-Gated Authorization gates Permissions.permitted checks. The two are structurally parallel: both call Session.validate before a downstream action, neither managing Session issuance. A deployment that wires both ensures that session validity is checked consistently at every protected surface — Capability redemption and Permissions evaluation alike.
External Onboarding — in regulated deployments where privileged users are external contractors or auditors rather than internal employees, External Onboarding (Invitation → Party Identity → Credential registration) is the upstream surface that establishes the requestor’s Credential. A Request Access call with an unregistered requestor_ref fails the Credential.verify check at step 2. External Onboarding establishes the Credential that this composition verifies.
Capability-Backed Sharing — a peer composition that uses Capability for resource disclosure rather than privileged access. The two compositions share the Capability atom but wire it to different upstream gates: Capability-Backed Sharing gates on Selective Disclosure policy; this composition gates on Multi-Party Approval. The structural similarity — approve first, allocate Capability second, record in Audit Trail third — is the pattern the library names as approval-gated capability provisioning.
Tamper Evidence — already applied where the truth lives, and not applicable where it does not. Everything evidentiary in this composition’s arc is already tamper-evidence-covered or immutably constituent-held: the request, approval, provisioning, exercise, and revocation events are ordinary audit events under the substrate’s Tamper Evidence sealing, and the token binding is a field of the Capability’s own immutable record. The composition’s maps are derived indexes — rebuildable caches carrying no truth of their own — so there is nothing there to seal, and sealing them would certify a cache, not a fact. A deployment is not offered a “seal the request_store” surface, and deliberately: Tamper Evidence commits to a record set presented at seal time, which is meaningless over state that includes a still-transitioning field; the evidentiary surface for legal proceedings is the sealed event trail, reached through request_to_events.

Standards references

SOX §404 (Management Assessment of Internal Controls) — privileged access to financial systems requires documented, multi-party authorization. This composition’s approval-gates-provisioning invariant and its Audit Trail arc are the structural implementation of the §404 access-control evidence requirement. Every access_exercised event traces to a documented, approved request with named approvers.
HIPAA §164.312(a)(1) (Access Control) — covered entities must implement technical policies and procedures for electronic information systems that allow access only to authorized users. The composition’s multi-party approval gate is the authorization policy; the Credential.verify checks at both request and approval time ensure the actors in the arc are authenticated; the Session.validate check ensures the principal is currently authenticated at exercise time.
PCI DSS Requirements 7 and 8 (Restrict Access and Identify Users) — Requirement 7 mandates that access to system components and cardholder data is restricted to only those individuals whose job requires such access. Requirement 8 mandates that all users are assigned a unique ID before access is allowed. This composition enforces both: the approval chain documents the business need; the requestor_ref and the Session record establish the unique user identity.
NIST (National Institute of Standards and Technology — US federal standards body) SP 800-53 AC-2 (Account Management) and AC-6 (Least Privilege) — AC-2 requires that privileged user accounts are authorized by senior officials and reviewed regularly. AC-6 requires that privileged access is limited to the minimum required. This composition models the authorization record (AC-2) and the time-limited, scoped Capability (AC-6’s minimum-necessary principle expressed as a token with explicit TTL — time-to-live, a validity duration — and scope).
NIST SP 800-53 AC-17 (Remote Access) — in deployments where privileged access is exercised remotely, the session-gated exercise check enforces that remote access is only permitted under an authenticated session. The Audit Trail records the session’s authenticated principal_ref and the exercised_at stamp for every remote access exercise — never the session token, which is bearer material and appears on no record surface — satisfying the remote-access audit requirement without the trail granting what it records.
ISO/IEC 27001 §A.9.2.3 (Management of Privileged Access Rights) — the International Organization for Standardization / International Electrotechnical Commission information-security standard requires that the allocation and use of privileged access rights is controlled and restricted. This composition directly implements that control: allocation is gated by approval; use is gated by session validity; both are recorded in a tamper-evident log.

Generation acceptance

A derived implementation of Privileged Access Provisioning is acceptable — in the regulator-acceptance sense — when an external auditor, given the composition’s emergent state plus the constituent stores (the substrate chain and audit records, the dedicated Capability instance, the Session and Credential stores), can clear the checks below without recourse to source code, runbooks, or developer narration. The bar splits in two, because two structurally different things are asked: what the records answer, and what needs evidence the records cannot hold.

Records-clearable checks

Confirm approval-gates-provisioning for every token that exists. Enumerate the dedicated Capability instance; parse each record’s composed scope to its request_id; confirm the request’s chain is in Approved state with the quorum-consistent decision records, recomputing the outcome under the substrate’s own quorum rule. A token whose scope parses to no request, to an un-Approved chain, or not at all is evidence of a provisioning bypass — for tokens whose request events are within the audit horizon; for an older token the check reads the request record’s Provisioned state and the surviving access_provisioned attestation instead, and a token with neither is the finding, while one with both is verified to the depth the horizon allows (Configuration’s ordering obligation is what keeps that depth adequate). Invariant 1 is the contract, and the enumeration direction matters: walking the tokens (not the requests) is what catches out-of-band allocation.
Confirm session-gated exercise for every recorded exercise. For every access_exercised event, confirm the named session_principal_ref’s Session record was live across the recorded exercised_at within the deployment’s operating skew — condemning clear violations, reading boundary-width discrepancies as inconclusive rather than findings (Edge cases — Clock semantics; the gate’s enforcement ran at Session’s own seam, and this check audits its evidence trail). Invariant 3 is the contract.
Confirm approver-credential validity at decision time. For every approval_step_decided event, confirm the approving actor’s Credential record verifies as having been Active at the recorded decision time. A decision through this composition’s surface attributed to a credential that was not Active then is evidence of a verification bypass. Invariant 6 is the contract, with its declared surface qualifier.
Confirm denial and failure completeness (within the horizon). Every Denied request whose events are within the horizon has its access_denied event and a Rejected chain; every ProvisioningFailed request has its access_provisioning_failed event with the relayed reason, or the open marker carrying it. Invariant 7 is the contract.
Rebuild the derived indexes and get the same answers — over the retention state each declares. All six elements are derived within the audit horizon (Composition state): discard their in-horizon entries, run the named rebuild procedures — the audit-log enumerate-and-filter for request_store, request_to_chain, session_access_log, and request_to_events; the Capability-instance scope-parse for request_to_capability / capability_to_request — and reproduce every traversal answer. An in-horizon entry that cannot be rebuilt is carrying truth it should not, and is a conformance failure; an entry for purged events is the declared truth-bearing half, and the check there is that it is present (the never-delete obligation), not that it rebuilds. The auditor also confirms no bearer material appears in any event payload or Read Request result — a raw capability_token or session_token on a record surface is a finding in itself.
Reconstruct the full arc for any request — at quiescence, within the horizon, with the recovery state read honestly. From a request_id, through request_to_events: who requested (with justification), against which resource and scope, when; who the approvers were and what each decided, with timestamps and credential-verification evidence; when provisioning happened; each exercise with its session principal and outcome; and any withdrawal or revocation. Verification of each event runs through the substrate’s own read_record → two-argument verify_record asymmetry. A request carrying an open audit_pending entry is a surfaced recovery window, not a finding — the finding is a committed act with no event and no open marker (a gap the recovery discipline should have caught), or an access_audit_recovery record whose original data disagrees with the constituent stores.

External checks

Whether the arc is un-fragmented. Invariant 9’s topology half: that no second Audit Trail instance receives a fork of these event classes is not provable from any one instance’s records; it is attested by deployment declaration and verified against the deployment’s wiring, like the substrate’s own externally-clearable declarations.
Whether the composed-scope encoding is the declared one. The scope-parse checks above assume the deployment’s declared serialization; that the running code writes exactly that encoding is evidenced by the deployment’s declaration and conformance tests, not by the records (a wrong encoder would surface as parse failures — visible — but a systematically different-but-parseable encoding needs the declaration to condemn).
Whether the delivery channel leaked the token. The raw token lawfully crosses exactly one surface — the provisioning delivery. That the deployment’s channel (push, secure store, response payload) did not expose it more widely is an operational-security question outside these records.
Whether application_credential custody held. The composition actor’s forgery surface is bounded by Invariant 1’s recomputability, but credential custody itself — issuance, rotation, retirement — is the deployment’s discipline, evidenced operationally (the same posture as Multi-Party Approval’s Configuration states).

Terms

The canonical concepts this spec refers to. Each [Term] marker in the prose above links to its term entry here. A term entry states what the concept is, in plain English, plus its Kind — one of five: 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 term entry 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 term entry carries one Projection 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 seven actions it exposes — the request intake (Request Access), the two chain-decision wrappers (Approve Step, Reject Step), the withdrawal (Withdraw Request), the session-gated use (Exercise Access), the revocation (Revoke Access), and the read (Read Request); the three-scope authorization vocabulary it defines for its Permissions instance (Requests Initiate, Requests Revoke, Requests Read — there is deliberately no withdraw scope, Scope vocabulary); and its own rejections — the exercise-gate Session Invalid, the revoke-gate Not Provisioned, and the Permission Denied / Credential Invalid it surfaces from its Permissions and Credential checks. Its load-bearing guarantees — approval-gates-provisioning (no Capability without an Approved chain), session-gated exercise, and single-Audit-Trail arc completeness (Invariant 1 through 10) — are structural properties, not data. Its emergent state (request_store, request_to_chain, request_to_capability, capability_to_request, session_access_log, request_to_events) — all derived indexes per Composition state — wires the constituents, left as backticked tokens; there is no composition-introduced record store to carry a term entry as a Type. The request-lifecycle states (Pending → Approved → Provisioned Denied Withdrawn Revoked ProvisioningFailed) are a composition-owned progression but are left uncarded — Pending / Approved / Denied / Withdrawn / Revoked overload the constituents’ own states (Multi-Party Approval, Capability, Session), so carding them would be ambiguous. The audit event types it emits (access_requested, approval_step_decided, access_provisioned, access_denied, access_request_withdrawn, access_provisioning_failed, access_exercised, access_exercise_failed, access_revoked, and the recovery record access_audit_recovery) — plus the recovery marker audit_pending and the event-data fields (session_principal_ref, exercised_at, denial_reason) — stay backticked as wire values, as do the constituent calls and their outcomes — Multi-Party Approval’s initiate_chain / approve_step / reject_step / withdraw_chain / read_chain, Capability’s allocate / redeem / revoke, Session’s validate, Credential’s verify, Permissions’ permitted, Audit Trail’s record_action — the relayed constituent tokens (request_id, chain_id, capability_token, session_token, actor_ref, requestor_ref, credential, access_scope, resource_ref), the parameterized session-invalid(reason) / capability-invalid(reason) and their reason values, the generic/relayed rejections (invalid-request, not-known, not-pending, unauthorized, storage-failure, recording-failure), the deployment configuration knobs (default_ttl, max_redemptions_default, credential_type, credential_check_on_request, approver_set_minimum, audit_trail_retention_policy, application_actor_ref, application_credential), and concrete example ids. Constituent atom and substrate names remain the existing full links to ../atoms/* and ./multi-party-approval.md / ./audit-trail.md; constituent operations stay backticked qualified calls, not cross-page links (the decided convention). (annotation.md Terms registry; representational only — it changes no guarantee, invariant, or behavior of the composition above.)

Request Access

The composition’s intake action: submit a privileged-access request under a named requestor, gate it on the requests:initiate permission and (optionally) a credential check, open a mandatory Multi-Party Approval chain for it, and audit the request (access_requested). Returns the request_id; the request is now Pending.

Kind: Operation

Approve Step

The composition’s wrapper over Multi-Party Approval’s step-approval: verify the approver’s credential is Active, record the decision (approval_step_decided), and — when the wrapped chain reaches Approved — fire the provisioning cascade that allocates the Capability (the only path to a provisioned token).

Kind: Operation

Reject Step

The composition’s wrapper over Multi-Party Approval’s step-rejection: verify the approver’s credential, record the decision, and transition the request to Denied when the chain reaches Rejected. Mirrors Approve Step but requires a reason.

Kind: Operation

Withdraw Request

The composition action by which the requestor — and structurally only the requestor, since the underlying chain admits withdrawal solely from its initiator — withdraws their own still-Pending request and its approval chain, audited (access_request_withdrawn). The requestor’s chains:withdraw grant in the substrate instance is the deployment-wired permission surface (Composes).

Kind: Operation

Exercise Access

The session-gated use of a provisioned Capability: validate the presented session first (a non-valid session is Session Invalid before the Capability is touched), then redeem the Capability — the composed scope in the redemption’s own return names the request — auditing every attempt that reached the atom (access_exercised or access_exercise_failed, each naming the session’s principal_ref; session_access_log derives from these events). Not idempotent by design: each live presentation consumes a redemption, and a committed redemption is always answered exercised. Enforces the cascading-revocation invariant (Invariants 3, 4).

Kind: Operation

Revoke Access

The composition action that revokes a provisioned Capability and transitions the request to Revoked, gated by the requests:revoke permission and audited (access_revoked). Rejects Not Provisioned when the request is not in Provisioned state.

Kind: Operation

Read Request

The read-only query over request records, gated by Requests Read: each result carries the request’s fields (the audit_pending recovery marker included), the chain’s current state, the provisioned Capability’s derived effective status, and the request’s audit event_ids from request_to_events — never any bearer token — in declared order (ascending requested_at, tie-broken by request_id). Produces no audit event and takes no credential.

Kind: Operation

Requests Initiate

The scope permitting Request Access — submit a privileged-access request.

Kind: Member Member of: the request scope vocabulary Role: Scope Projection: requests:initiate

Requests Revoke

The scope permitting Revoke Access on any provisioned request.

Kind: Member Member of: the request scope vocabulary Role: Scope Projection: requests:revoke

Requests Read

The scope permitting queries over request records and their associated chain, capability, and audit events.

Kind: Member Member of: the request scope vocabulary Role: Scope Projection: requests:read

Not Provisioned

The Revoke Access rejection when the target request is not in Provisioned state — there is no live Capability to revoke.

Kind: Member Member of: the revoke rejection Role: Rejection Projection: not-provisioned

Session Invalid

The Exercise Access gate rejection — parameterized by the Session’s own reason (expired, revoked, not-known) — returned when Session.validate is not valid, before the Capability is presented. The structural form of the cascading-revocation invariant (Invariant 4).

Kind: Member Member of: the exercise rejection Role: Rejection Projection: session-invalid

Permission Denied

The composition’s rejection when the acting actor lacks the required request scope at the Permissions check in Request Access or Revoke Access — and, relayed, when the substrate’s own chains:* gate refuses (Request Access step 5 and Withdraw Request step 4: the double-gate the deployment wires, surfaced under this code so the caller learns the true cause).

Kind: Member Member of: the request rejection Role: Rejection Projection: permission-denied

Credential Invalid

The composition’s rejection when Credential.verify reports the requestor’s or approver’s credential is not Active at the moment it is checked — the enforcement behind approver-credential completeness (Invariant 6).

Kind: Member Member of: the request rejection Role: Rejection Projection: credential-invalid

Status

partially resolved — see the Ledger.

Ledger

status: partially resolved
formal: verified — privileged-access-provisioning.tla, no twin, 2026-06-03
last gate: 2026-08-28 — second gate after closure, fresh reader — 5 foundational (all since closed), 19 refining, 5 rhetorical

open:
- 2026-08-27-e · refining · [Approve Step] step 5 · attributes a `recording-failure` arm to `read_record`, whose contract has no rejection arm; its `not-known` arm is never named → map the real arm
- 2026-08-27-f · refining · [Approve Step] step 5; Invariant 7 · no rule for identifying the chain's terminal event id in `chain_to_events`; the last id can be a `step_approved` → state the selection rule
- 2026-08-27-g · refining · [Read Request] step 3 · names no constituent rejection landings for `read_chain` or `Capability.read` → enumerate them
- 2026-08-27-h · refining · [Request Access] step 1 · validates primitives but not chain shape, so malformed submissions are discovered after the durable pre-write and mint permanent `Withdrawn` records → validate chain shape at intake
- 2026-08-27-i · refining · [Exercise Access] step 2 · a `capability_to_request` miss is conflated with `invalid(not-known)` and recorded as never-issued; whether `redeem` is called on the miss is unstated → separate the cases and state the call
- 2026-08-27-j · refining · Provisioning cascade; Examples, happy path · `ttl = expires_at − now` is evaluated at Capability's seam, so the token does not end where the request does; the example asserts it does → restate, or pass an absolute expiry
- 2026-08-27-k · refining · Summary; Edge cases · the Summary counts expiry among six stages "with no gaps"; expiry writes no event → correct the count
- 2026-08-27-m · refining · Action signatures · optional `reason?` precedes required `credential`; `credential` sits second in one action and last in four, against every constituent → make the position uniform
- 2026-08-27-n · refining · Composes, Permissions bullet · enumerates two `permitted` call sites; [Read Request] step 1's `requests:read` is a third → add it
- 2026-08-27-o · refining · Composes (Session); Behavior · state the cascading-revocation invariant unconditionally where Invariant 4 conditions it on a wired cascading issuance surface → carry the qualifier
- 2026-08-27-p · refining · Recovery discipline, initiation leg · no rule for a chain found present when step 5's own closure already moved the request to `Withdrawn` but crashed before closing the entry → add the case
- 2026-08-27-r · rhetorical · Terms · [Permission Denied] and [Credential Invalid] filed under "the request rejection" though returned by other actions → widen the membership
- 2026-08-27-s · rhetorical · Composition state, opening · one ~500-word sentence-chain carries four separately cited rules → split into citable paragraphs
- 2026-08-27-t · rhetorical · Composes (Audit Trail) · "five stages" against the Summary's six → reconcile
- 2026-08-26-a · refining · [Approve Step] steps 5–6 · a `read_chain` `permission-denied` at step 5 contradicts step 6's unconditional `approved`; `invalid-query` and empty-result arms unmapped → pin the step-6 reading and map the arms
- 2026-08-26-b · refining · Action wiring standing rules; [Approve Step] step 3 · a substrate `invalid-credential` / `recording-failure` over a committed decision rejects the caller and skips the evaluation — a third path to approval-without-token → route it to the sweep's second leg
- 2026-08-26-c · refining · Examples · `quorum_rule: all-of-2` is not in the substrate's declared vocabulary (`all-of-N`) → use the declared form
- 2026-08-26-d · refining · Summary · "the requestor's session is re-checked" overstates the bearer-shaped identity claim → narrow
- 2026-08-26-e · refining · Generation acceptance check 3 · lacks the operating-skew qualifier check 2 carries for the same cross-seam comparison → add it
- 2026-08-26-f · refining · Composition state, `request_store` · "`Provisioned` is terminal for the store" contradicts [Revoke Access]'s Provisioned → Revoked → restate
- 2026-08-26-g · refining · Recovery discipline · no leg for a crash before the `access_denied` / `access_request_withdrawn` record, leaving a Pending request against a terminal chain → add the leg
- 2026-08-26-h · refining · Examples, happy path · credits "Assignment in-tray notifications" no constituent supplies → remove or attribute
- 2026-08-26-i · rhetorical · Examples · `cred_e42` doubles as presented material and credential id → separate them
- 2026-08-26-j · rhetorical · Examples, example 3 · "deadline lapses it" glosses derived expiry as a transition → restate
- 2026-08-26-k · rhetorical · Examples · "Three scenarios" precedes four → fix the count
- 2026-08-26-l · rhetorical · Terms, progression diagram · reads all terminals off `Approved` → redraw
- 2026-08-28-a · refining · Composes (Credential, Audit Trail) · one `credential` feeds `Credential.verify` as presented material and `record_action` for Actor Identity's attest; that one material satisfies both registries is an unstated deployment assumption → declare it or split the argument
- 2026-08-28-b · refining · [Approve Step] step 5 Rejected arm · attributes `recording-failure` to `read_record`, whose contract is `audit_record | not-known` with no rejection arm; `not-known` unlanded → map it and a purged record to the null-reason landing
- 2026-08-28-c · refining · step 5 null-reason landing · the `audit_pending` entry opened there has no closure, `access_denied` having already landed → define what the retry emits and when the entry closes
- 2026-08-28-d · refining · [Request Access] step 1 · omits chain-shape validation (`approver_set` size and uniqueness, `quorum_rule` shape), so a caller shape error is caught at step 5 after the durable pre-write and leaves a permanent `Withdrawn` record → validate the shape at step 1
- 2026-08-28-g · refining · [Exercise Access] step 2 · rebuild-on-miss of `capability_to_request` on every unresolved token is a full enumeration per forged presentation → resolve by `Capability.read` filtered on the token, then parse its scope
- 2026-08-28-h · refining · [Exercise Access] · a token whose request has not reached `Provisioned` (leg-one window) is exercised and `access_exercised` lands before `access_provisioned` → state the ordering as lawful or gate on request state
- 2026-08-28-i · refining · [Withdraw Request] step 4 `not-pending` arm · the triggered evaluation can fire the cascade and deliver a token inside a call that returns `not-pending` → say so; the caller reads the request to learn it was provisioned
- 2026-08-28-j · refining · step 1 of [Withdraw Request], [Approve Step], [Revoke Access] · `not-known` / `not-pending` / [Not Provisioned] answered before any credential or permission check — an existence and state oracle → order the credential check first or declare the leak
- 2026-08-28-k · refining · Configuration `max_redemptions_default` · "the audit record reflects the configuration" but `access_provisioned` carries neither `max_redemptions` nor `expires_at` → add them or point at the Capability record
- 2026-08-28-m · refining · check 2 · the event carries only `session_principal_ref`, so "the principal's Session record was live" is satisfiable by any session of that principal → state the check as existential or record a non-bearer session identifier
- 2026-08-28-n · refining · Pass 2 · `approval_step_decided` duplicates the substrate's `step_approved`/`step_rejected` for the same commit, and `Credential.verify` double-authenticates ahead of the substrate's attest → drop, or state what the second record and check add
- 2026-08-28-p · refining · step 5 Rejected arm · "take the chain's terminal event id from that list" — the list is bare ids → specify the walk (read from the tail until `action_ref ∈ {chain_resolved, chain_withdrawn}`)
- 2026-08-28-q · refining · step 5 Rejected arm · the `access_denied` `record_action`'s own arms and whether the `Denied` index write proceeds on failure are unenumerated → enumerate as the provisioning-failed arm does
- 2026-08-28-r · refining · [Read Request] step 3 · `read_chain` is called for every result, but chain-less requests have no `chain_id` → state the skip
- 2026-08-28-s · rhetorical · Invariant 8 · immutable-field list omits `chain_id`, which Composition state declares immutable → add it
- 2026-08-28-t · rhetorical · Terms [Credential Invalid] · "not Active" omits `material-mismatch`, which also lands there → reword
- 2026-08-28-u · rhetorical · Provisioning cascade compensation story · "under all-of-N every step is terminal the moment quorum fires" holds for `Approved` only; `Rejected` leaves trailing Pending steps → qualify
- 2026-08-28-v · rhetorical · step 5 · "`Rejected`, request `Pending` or `Approved`" — the `Approved` case is unreachable (chain terminal-stable) → drop or mark unreachable
- 2026-08-28-w · rhetorical · [Exercise Access] step 2 · whether `redeem` is called when the map resolves nothing is implicit → pin it
- 2026-08-29-a · refining · formal · the model's sweep carries no pre-check, no identity, no recovery record, and no age bound → extend the model with the four sweep rules

Decisions

Directional changes only — the turns a future reader must know the pattern took, and why. Everything smaller lives in the commit that made it: git log -- compositions/privileged-access-provisioning.md.

2026-08-25 — Every Composition-state element is a derived index over the substrate audit log and the Capability instance’s composed scope. Chose: no bearer material on any record surface, every index rebuildable from the trail and the token’s scope, a named recovery discipline. Over: composition-owned stores carrying request and access truth of their own. Because: the records-alone control claim — every privileged token traces to an approved request — is only as strong as the evidence that outlives the composition’s own state.
2026-08-28 — The live provisioning guard is the sweep’s detector, and every crash window around the evaluation has a leg. Chose: Approve Step step 5 fires the cascade on the same conjunction the sweep’s second leg tests (non-terminal ∧ no token for the request ∧ no open provisioning-failed entry), a not-pending from the substrate still runs the evaluation, a terminal-chain leg closes a request whose decision died before evaluating, exercise entries are marked redeemed inside the hold, and a failed evaluation opens an entry and still returns approved. Over: a guard on the request-state read, and a reconciliation that compared the redemption counter against events alone. Because: the Approved transient rebuilds to Pending, so the state read alone allocated a second token after a crash; the reconciliation read two open entries — a shape the page admitted — as a conformance finding; and a decision that died between commit and evaluation left its request Pending forever.
2026-08-29 — The sweep pre-checks the trail, is bounded where it runs outside the hold, writes as the composition behind a recovery record, and the truth-bearing state is named. Chose: every sweep leg detects on rebuilt state and the absence of the event, paired by a seam-injected invocation_id on every event and entry; the redemption-reconciliation leg examines no entry younger than a declared recording_completion_bound; every sweep write is attested under the service identity behind an access_recovery_intended record; the open audit_pending payloads are declared truth-bearing, extraction-pending against Outbox, and the store’s never-delete rule and the dedicated Capability instance’s purge exemption are declared as store_durability. Over: legs that detected on an index and re-ran a non-idempotent record_action, an exercise leg with no lower edge over a window the serialization does not cover, and “all six elements are derived indexes” over state the page itself called truth-bearing. Because: a stale index with the event already landed re-emitted duplicates; an entry marked redeemed seconds ago belongs to an invocation about to write; a compensation the absent actor did not make cannot be attested as theirs; and a record owed for a committed act that exists in no constituent is not a cache (the frozen rules of 2026-08-29 — A reconciliation is bounded at both ends, Intents pair with outcomes, Recovery commits under a declared service identity, A derived index splits at the horizon).
2026-08-26 — The requests:withdraw scope and third-party withdrawal are dropped. Chose: remove the scope, its term entry and registry entry, and name the administrative alternatives. Over: keeping a promise the wiring could not honor. Because: the substrate’s chain withdrawal is initiator-only and the composition actor is not the initiator, so no honest wiring existed for the path.