Attributed Permissions Admin

Table of contents

Attributed Permissions Admin

A regulated composition: every permission grant and every revocation is paired atomically with a verifiable attestation under the issuing actor’s credential. Composes Permissions and Actor Identity into a single coherent administration surface where the records alone answer the regulator’s question — “who granted this access, when, and under what credential?” No grant exists in the store without its attribution; no revocation lands without proof of authorization.

Intent

Permissions alone records that a grant exists. Actor Identity alone records that an actor attested to an action. Neither tells the auditor who issued this specific grant, and neither prevents an unattested grant from being inserted into the permissions store directly — by a database administrator, a misconfigured automation, or an attacker with write access to the grant table. The audit question the regulator actually asks — “who authorized this access, and can you prove they did?” — has no structural answer at the bare-atom layer.

This composition addresses that gap. Every issue_grant call walks two atoms in sequence: Actor Identity records the grantor’s attestation over a proposal (subject, scope, intent-to-grant), and then Permissions records the grant. The two records are paired in the composition’s emergent state — the grant’s grant_id is bound to the attestation’s attestation_id, and the binding is recoverable from either side. Revocations follow the same pattern: the revoker attests, then Permissions revokes, and the pairing is recorded against the grant.

The pattern matters because regulated systems consistently fail this audit question when the atoms are wired by hand at the calling layer. A developer who calls Permissions.grant without also calling Actor Identity.attest produces an unattributed grant — silent at the schema level, fatal at audit time. The composition makes the omission impossible through its exposed surface: there is no path through the composition that records a grant without attesting, or records a revocation without attesting. The bare atoms remain unchanged; the application is the wiring that turns two separate records you can forget to coordinate into one administered action you cannot bypass through the composition’s surface. An adversary with direct write access to the underlying Permissions store can still insert unattributed grants, bypassing the composition entirely — this is the exact tamper surface the breach-forensics adversarial scenario exposes and the Tamper Evidence composing pattern addresses.

This is not a Role-Based Access Control (RBAC) layer, not a delegation system, and not an attribute-based policy evaluator. Each of those is a separate composing pattern. This composition supplies only the bottom rung — every grant has a verifiable grantor; every revocation has a verifiable revoker — on top of which delegation, RBAC, ABAC, and policy reconciliation can compose without re-inventing the attribution surface.

Summary

Attributed Permissions Admin is a two-atom regulated composition (a composition that wires constituent atoms whose acceptance bar is set by an external evaluator — regulator, auditor — and therefore inherits the regulated-overlay sections of Regulated adversarial scenarios and Generation acceptance) that pairs every permission grant and every revocation with a cryptographically (or procedurally) verifiable attestation under the issuing actor’s credential. It wires two freestanding atoms (atoms whose specifications do not name any other pattern): Permissions, which records grants and answers permitted queries against the grant store; and Actor Identity, which records attestations binding a named actor to a specific action and supports verify queries against those attestations.

Neither Permissions nor Actor Identity knows about the other. Permissions records grants but has no concept of who issued the grant — its Composition notes explicitly defer grantor attribution to a composing pattern. Actor Identity records attestations but has no concept of grants — its attestations bind actors to opaque action references whose semantics are owned by the composing system. The composition is the wiring that makes them coherent: every state-changing administrative action (issue_grant, revoke_grant) walks both atoms in a fixed order, records the pairing in emergent state, and surfaces a unified result the caller can rely on.

Beyond what either atom guarantees individually, the composition produces eight emergent invariants (properties that only appear when atoms are combined — no single atom carries them). First, attribution completeness: no grant exists in the Permissions store without a paired, verifiable attestation in the Actor Identity store (conditional on the implementation satisfying the pairing-write durability requirement). Second, revocation attribution: every revocation transition (Active → Revoked) has a paired attestation under the revoker’s credential (conditional on the same pairing-write durability requirement as Invariant 1). Third, attribution recoverability: given any grant id, the composition’s records yield the grantor’s identity, the grant timestamp, the attestation id, and the proof that the named grantor authorized this specific grant. Fourth, attribution-time monotonicity: a grant’s recorded attestation timestamp must precede or equal the grant’s recording timestamp — best-effort under non-monotonic or cross-system clocks. Fifth, constituent invariants preserved: all ten Permissions invariants and all nine Actor Identity invariants hold over the respective stores. Sixth, pairing-map durability: once written, entries in grant_attribution and revocation_attribution are never modified or deleted by the composition. Seventh, attestation exclusivity: every attestation is used exactly once and for exactly one purpose — issuance or revocation, for exactly one grant — enforced structurally by the nonce mechanism and the distinct proposal formats. Eighth, orphan log durability: once written, orphan log entries are never modified or deleted by the composition, mirroring the pairing-map durability discipline for the operational-retry surface so that the log is preserved as evidence of failed administrative attempts.

The most common uses are administrative access-control panels in SOX-scoped financial systems, HIPAA-regulated electronic health record systems where every patient-record access grant must be attributable to the granting administrator, PCI DSS-scoped payment systems where Requirement 7 mandates attributed authorization, FDA-regulated software pipelines under 21 CFR Part 11 where branch-protection grants must carry a verifiable approver, and legal document management systems where matter-level access grants must be attributable to the responsible partner. In every case the mechanic is the same — attest first, grant second, record the pairing — and the audit answer is structural: the records alone establish who authorized which access, when, and under what credential.

This composition does not implement role management, attribute-based policy evaluation, scope hierarchy, explicit deny, delegation, time-bounded grants, mass deprovisioning, or grantor authorization (whether the grantor was permitted to issue this grant per organizational policy). Each is a separate composable pattern; see Composition notes in the constituent atoms.

Composes

Permissions — provides the grant store and the evaluation surface: grant, revoke, permitted. The application maintains exactly one Permissions instance scoped to the administered authorization domain. The application wraps grant and revoke behind its own actions; permitted is passed through unchanged.
Actor Identity — provides the attestation surface: attest, verify. The application maintains exactly one Actor Identity instance whose attestations bind grantors and revokers to composition-defined action references. The application wraps attest behind its own actions and surfaces verify results inside the composition’s read-only query.

Composition logic

Application state

Identity model for emergent state. The composition introduces no new entity identity. Its emergent state is keyed by grant_id — the opaque, system-generated id owned by the Permissions atom. There is no separate composition-level id for a pairing record; grant_id is the unique handle through which both maps are accessed, the same id the Permissions store uses as the grant’s identity.

The application owns two pieces of emergent state that neither constituent atom carries:

grant_attribution — a map from grant_id to attestation_id. Populated when issue_grant records both a grant in Permissions and the corresponding attestation in Actor Identity; the pair is durably written before the action returns. Read by verify_grant_attribution and by audit-time reconstruction. The composition exposes no surface to modify or delete these entries; see Invariant 6 — Pairing-map durability.
revocation_attribution — a map from grant_id to attestation_id. Populated when revoke_grant records both a revocation in Permissions and the corresponding attestation in Actor Identity. Each grant has at most one revocation attestation (revocation is terminal per Permissions’ Invariant 2). Read by verify_grant_attribution for revoked grants and by audit-time reconstruction. The composition exposes no surface to modify or delete these entries; see Invariant 6.

The two maps’ lifetimes match the Permissions store’s lifetime: while a grant exists in the Permissions store (Active or Revoked), its attribution record exists in the corresponding map. Map entry lifecycle after a retention purge is governed by the composing Retention Window pattern’s scope — see Retention of attribution records in Edge cases.

Orphan log — an append-only operational record of attestations that were successfully written to Actor Identity but whose corresponding grant or revocation writes failed. Each entry has the shape: {attestation_id, proposal_ref, requested_at, underlying_reason}. underlying_reason is one of grant-storage-failure, revocation-storage-failure, invalid-request (grant side), not-known (revocation side), not-active (revocation side), or pairing-write-failure. The orphan log is the composing system’s operational surface for retry and manual review; it is not the audit mechanism for orphan detection. The audit’s structural orphan detection — Generation acceptance check 5 — operates by cross-referencing the Actor Identity store against the two attribution maps directly and does not depend on the orphan log being populated or retained. The orphan log is populated in step 4 of issue_grant, step 5 of issue_grant, step 4 of revoke_grant, and step 5 of revoke_grant; it is never modified after a write — see Invariant 8 — Orphan log durability.

Configuration

The application exposes one deployment-settable knob:

grant_proposal_format — type: structured reference; default: {subject_ref, action_scope, nonce, requested_at} serialized in a canonical order (e.g., sorted key-value pairs with length prefixes). The format defines the synthetic action_ref that Actor Identity’s attest call binds the grantor’s proof to. Two rules the deployment must enforce: (1) the format must include a unique-per-grant element (the nonce is the canonical solution) so that two distinct grant attempts for the same (subject_ref, action_scope) pair produce distinct proposal references and therefore distinct attestations; (2) the format must include a deployment-specific namespace prefix (e.g., apa:grant: prepended to the serialized proposal body) that distinguishes composition-issued proposal references from attestations issued by other composing systems sharing the same Actor Identity store. Without the namespace prefix, Generation acceptance check 5 — identify orphan attestations — cannot be completed from the records alone: the auditor has no structural criterion by which to filter composition-issued action_ref values from foreign ones. Deployments under regulation that mandates a specific proposal-encoding format (e.g., a national e-prescribing scheme) must conform to that format; the composition’s only requirements are uniqueness per proposal and namespace enumerability.

revocation_proposal_format for revoke_grant is fixed (not configurable): {grant_id, requested_at} serialized canonically with the same deployment namespace prefix as grant_proposal_format. The namespace prefix requirement for revocation proposals is a hard rule, not a rationale: the revocation proposal body must be prefixed with the same deployment-specific namespace prefix used for grant proposals (e.g., if grant proposals use apa:grant:, revocation proposals must also begin with that prefix, yielding apa:grant:{grant_id, requested_at}). Without this rule, a deployment could apply the namespace prefix to grant proposals but omit it from revocation proposals, making revocation-phase orphan attestations indistinguishable from foreign attestations in a shared Actor Identity store and breaking Generation acceptance check 5 for the revocation-side orphan population. Principle. A revocation is uniquely identified by the grant it terminates; the revoker’s intent-claim is {grant_id, requested_at} — which grant, requested when. Neither a nonce nor a configurable shape serves any audit purpose here. Likely objection. “Shouldn’t the revocation proposal format be as configurable as the grant proposal format, for symmetry?” Mechanism that resolves it. The grant proposal format needs two configurable properties: nonce uniqueness (so that two grant attempts for the same pair produce distinct attestations) and namespace prefix (so that orphan attestations are enumerable audit-side). Neither applies to revocation proposals. grant_id uniqueness is already guaranteed by Permissions’ invariants — no nonce needed. Namespace enumerability for revocation-proposal orphans is satisfied by the same namespace prefix as the grant proposal (the composition issues both; the auditor applies the same filter). Providing a separate revocation_proposal_format knob would allow a misconfigured deployment to produce revocation proposals that do not share the grant namespace, making orphan detection incomplete and violating the requirement the namespace prefix is intended to satisfy. Result. revocation_proposal_format is fixed; correctness requires it, not convenience.

requested_at in both proposal formats is taken from the composition’s wall-time clock at the moment the action is invoked. The same clock-semantics caveat that applies to Permissions’ granted_at and Actor Identity’s attested_at applies here: monotonicity is best-effort under NTP adjustments, not guaranteed. Composing with Trusted Timestamping (RFC 3161) supplies an adversarially-defensible time anchor if the deployment requires it.

Primitive policies

The application accepts these string-typed inputs at its outer boundary. Validation rules are stated explicitly; each input that fails validation produces a rejection at the composition layer before either constituent atom is invoked.

subject_ref (input to issue_grant) — opaque reference. Validation: non-empty; whitespace-trimmed at the composition layer (the composition normalizes by trimming leading and trailing whitespace before passing to Permissions); case-sensitive (matching Permissions’ exact-match semantics); length cap 256 characters. Empty or all-whitespace inputs produce rejected(invalid-request).
action_scope (input to issue_grant) — opaque reference. Same validation as subject_ref. The scope vocabulary itself is deployment-defined; this composition treats every scope as opaque.
grantor_ref (input to issue_grant) — opaque reference. Same validation. Passed directly to Actor Identity’s attest.
grantor_credential (input to issue_grant) — credential material. Validation: non-empty; structural well-formedness checked by Actor Identity (which produces invalid-credential if it fails). The composition does not inspect credential contents.
grant_id (input to revoke_grant) — opaque id previously returned by issue_grant. Validation: non-empty; existence checked by Permissions (which produces not-known if the id is unknown). The composition does not query Permissions ahead of revoke to pre-validate.
revoker_ref (input to revoke_grant) — same validation as grantor_ref.
revoker_credential (input to revoke_grant) — same validation as grantor_credential.

Whitespace normalization is performed once at the composition layer for each opaque reference; downstream stores receive the normalized value. This forecloses the “whitespace-only difference between the grant and the revocation query” class of Pass 3 finding.

Action wiring

The application exposes two state-changing actions (issue_grant, revoke_grant), one read-only attribution query (verify_grant_attribution), and one passthrough evaluation query (permitted). Each state-changing action walks both constituent atoms in a fixed order; any failure at either step is surfaced at the composition’s boundary with a fully-named rejection taxonomy.

issue_grant(subject_ref, action_scope, grantor_ref, grantor_credential) → (grant_id, attestation_id) | rejected(invalid-request | invalid-credential | attribution-storage-failure | orphan-attestation)
1. Validate inputs per Primitive policies. If any input fails validation, return rejected(invalid-request) without invoking either constituent.
2. Construct the proposal reference per grant_proposal_format: {subject_ref, action_scope, nonce, requested_at} serialized canonically. The nonce is a freshly-generated opaque token unique per call. requested_at is taken from the composition’s wall-time clock at invocation time (see clock note in Configuration).
3. Call ActorIdentity.attest(proposal_ref, grantor_ref, grantor_credential). Outcomes:
  - attestation_id → proceed to step 4.
  - rejected(invalid-credential) → return rejected(invalid-credential). No grant recorded.
  - rejected(invalid-request) → return rejected(invalid-request). No grant recorded. (This code from ActorIdentity.attest indicates the composition-assembled proposal_ref violated Actor Identity’s request format — a configuration error in grant_proposal_format, not a caller-input error. The composition surfaces it as invalid-request since the effective cause is a malformed proposal reference.)
  - rejected(storage-failure) → return rejected(attribution-storage-failure). No grant recorded.
4. Call Permissions.grant(subject_ref, action_scope). Outcomes:
  - grant_id → proceed to step 5.
  - rejected(invalid-request) → an orphan attestation now exists in Actor Identity with no corresponding grant. Return rejected(orphan-attestation) after logging the orphan for the composing system’s orphan-resolution process (see Edge cases). The composition does not delete the attestation — Actor Identity’s Invariant 9 (Attestation durability) forbids it.
  - rejected(storage-failure) → same orphan handling as invalid-request above. Return rejected(orphan-attestation) after logging. The underlying cause (storage failure vs. invalid request) is recorded in the orphan log; the composition’s external signal is always orphan-attestation when a grant-side failure leaves an unmatched attestation.
5. Write the pairing: grant_attribution[grant_id] = attestation_id. This write must be durable before the action returns; if it fails, the composition returns rejected(orphan-attestation) and logs the orphan. The grant exists in Permissions but cannot be attributed without the pairing record — see Edge cases for the implementation requirement.
6. Return (grant_id, attestation_id) to the caller.
revoke_grant(grant_id, revoker_ref, revoker_credential) → (ok, attestation_id) | rejected(invalid-request | invalid-credential | not-known | not-active | attribution-storage-failure | orphan-attestation)

Orphan side-effect note. All rejection codes from step 4 onward — including not-known and not-active — produce an orphan attestation in the Actor Identity store. orphan-attestation is the explicit signal for composition-failure orphans (storage failures). not-known and not-active are caller-error codes: they surface the Permissions rejection directly and do not return orphan-attestation, because the error is caller-caused rather than composition-caused. However, an orphan attestation is created in both cases and is logged internally. Callers who implement retry logic against not-known or not-active should be aware that each failed attempt leaves an orphan attestation in Actor Identity. The orphan log and Generation acceptance check 5 are the recovery and audit surfaces.
1. Validate inputs per Primitive policies. If any input fails, return rejected(invalid-request).
2. Construct the revocation proposal reference: {grant_id, requested_at} serialized canonically. requested_at is taken from the composition’s wall-time clock at invocation time (see clock note in Configuration).
3. Call ActorIdentity.attest(revocation_proposal_ref, revoker_ref, revoker_credential). Outcomes:
  - attestation_id → proceed to step 4.
  - rejected(invalid-credential) → return rejected(invalid-credential). No revocation recorded.
  - rejected(invalid-request) → return rejected(invalid-request). No revocation recorded. (The revocation_proposal_format is fixed, so an invalid-request response from Actor Identity at this step indicates a malformed revoker_ref that passed composition-layer validation but failed Actor Identity’s deeper check — or a composition implementation error in the fixed serialization.)
  - rejected(storage-failure) → return rejected(attribution-storage-failure). No revocation recorded.
4. Call Permissions.revoke(grant_id). Outcomes:
  - ok → proceed to step 5.
  - rejected(not-known) → orphan attestation exists; return rejected(not-known) after logging the orphan. (The caller passed a grant_id that does not exist; the attestation now exists but binds the revoker to a non-existent grant. This is correctly classified as caller error; the orphan attestation stands as evidence of the attempt.)
  - rejected(not-active) → orphan; return rejected(not-active) after logging. (The grant exists but is already revoked. The new attestation binds the revoker to an already-terminal action; the original revocation attestation is the authoritative one.)
  - rejected(storage-failure) → orphan; return rejected(orphan-attestation) after logging. (Same unification as issue_grant step 4: the composition’s external signal for any revocation-side failure that leaves an unmatched attestation is orphan-attestation; the underlying cause is in the orphan log.)
5. Write the pairing: revocation_attribution[grant_id] = attestation_id. Same durability requirement as issue_grant step 5; failure produces rejected(orphan-attestation) after logging.
6. Return (ok, attestation_id) to the caller.
verify_grant_attribution(grant_id) → (grant_record, issuance_attestation_id, issuance_verify_result, revocation_attestation_id?, revocation_verify_result?) | not-known | attribution-inconsistency

grant_record shape: {grant_id, subject_ref, action_scope, status, granted_at, revoked_at?} — the Permissions store’s full record for the grant. status is one of Active or Revoked. revoked_at is present only when status = Revoked.

attribution-inconsistency is a distinct result tag from not-known. not-known means the grant does not exist in Permissions. attribution-inconsistency means the grant exists in Permissions but the corresponding attribution map entry is unpopulated — either a violation of Invariant 1 (Attribution completeness) at step 2a (grant exists, no grant_attribution entry), or a violation of Invariant 2 (Revocation attribution) at step 4a (grant is Revoked, no revocation_attribution entry). Both cases indicate a pairing-write failure under their respective invariants’ conditional-durability requirement. These are structurally different from a normal lookup miss and require different caller responses: not-known is a normal miss; attribution-inconsistency is a forensic finding under the Caller contract below.
1. Look up the grant in Permissions. If not present, return not-known.
2. Look up grant_attribution[grant_id] → issuance_attestation_id. (Invariant 1 — Attribution completeness — guarantees this lookup succeeds under normal operation for every grant in the store.) 2a. If grant_attribution[grant_id] is unpopulated despite the grant existing in step 1: return attribution-inconsistency. Invariant 1 is conditional on pairing-write durability; if the pairing write failed after the Permissions write succeeded (Cross-store consistency edge case), this state is reachable. The caller must treat attribution-inconsistency as a forensic finding and log the inconsistency — the grant exists without an attribution record. This state must not be silently coerced to not-known.
3. Call ActorIdentity.verify(issuance_attestation_id) → issuance_verify_result (one of verified, failed-verification(reason), not-known). A result of not-known from ActorIdentity.verify here is a tamper signal: Invariant 6 (Pairing-map durability) and Actor Identity’s Invariant 9 (Attestation durability) together guarantee this attestation_id should exist; if Actor Identity does not recognize it, the attestation record has been deleted or the grant_attribution map has been rewritten — both prohibited by the respective invariants. The caller must treat not-known at this step as a forensic finding, not a normal lookup miss.
4. If the grant is Revoked, look up revocation_attribution[grant_id] → revocation_attestation_id. (Invariant 2 — Revocation attribution — guarantees this lookup succeeds under normal operation for every Revoked grant.) 4a. If revocation_attribution[grant_id] is unpopulated despite the grant being Revoked in step 1: return attribution-inconsistency. Invariant 2 is conditional on pairing-write durability; if the pairing write failed after Permissions.revoke succeeded (Cross-store consistency edge case), this state is reachable. The caller must treat attribution-inconsistency as a forensic finding and log the inconsistency — the grant is Revoked without a revocation attestation record. This state must not be silently coerced to not-known or to a “no revocation attestation” case. Same caller contract as step 2a — see Caller contract below.
5. Call ActorIdentity.verify(revocation_attestation_id) → revocation_verify_result. Same tamper interpretation applies if ActorIdentity.verify returns not-known: per Invariant 6 (Pairing-map durability) and Actor Identity’s Invariant 9 (Attestation durability), the attestation should exist; not-known here is a tamper signal, not a normal lookup miss.
6. Return the tuple. The caller (typically an auditor or the administration UI) inspects each verify result to determine whether the attribution stands or has been compromised.
Caller contract — forensic-finding result codes. Three of verify_grant_attribution’s outcomes are forensic findings, not routine lookup results, and require distinct caller handling. The composition surfaces them with explicit names so the caller cannot conflate them with normal lookup outcomes:
- attribution-inconsistency (returned from step 2a or step 4a). The grant exists in Permissions, but the corresponding attribution map entry is unpopulated — a violation of Invariant 1 (step 2a) or Invariant 2 (step 4a) under their respective pairing-write-durability conditionals. The caller MUST log the inconsistency naming which invariant was violated and which grant_id is affected; MUST NOT retry the original administrative action against the same grant_id as a normal retry (the original grant or revocation has already committed in Permissions; a retry would create a duplicate administrative event without resolving the attribution gap); MUST NOT coerce the result to not-known (which is a distinct condition — the grant does not exist); MUST surface the finding to the forensic / orphan-resolution process (e.g., the Failed-Grant Reconciliation pattern named in Edge cases).
- not-known from ActorIdentity.verify at step 3 (issuance attestation) or step 5 (revocation attestation). The attribution map points at an attestation_id that Actor Identity does not recognize — a violation of Invariant 6 (Pairing-map durability) together with Actor Identity’s Invariant 9 (Attestation durability). The caller MUST treat this as a tamper signal, log the finding naming the affected attestation_id and grant_id, and surface to the forensic process. The caller MUST NOT treat this as equivalent to step 1’s not-known — the same result word appears at two structurally different positions and the caller’s handling logic must distinguish them by step.
- failed-verification(reason) from ActorIdentity.verify. Distinct from the above two; the attestation record exists but its proof does not verify. This is a tamper or credential-history finding handled per the Disputed grant regulated adversarial scenario and the Compromise Disclosure composing pattern. Not a routine outcome.
not-known returned from step 1 (grant not found in Permissions) is the only verify_grant_attribution outcome the caller may handle as a normal lookup miss.
permitted(subject_ref, action_scope) → permitted | denied — passes through directly to Permissions.permitted(subject_ref, action_scope) unchanged. The composition does not interpose on evaluation, only on administration. Its contract is about how grants are created and revoked, not about how access is evaluated at request time.

The load-bearing wiring decision — attest-before-record

The composition’s central architectural decision: every state-changing administrative action attests before recording the corresponding state change in Permissions. The order is fixed; the reverse order would let an attacker (or a buggy implementation) record a grant in Permissions without an attestation and have the composition fail to detect it after the fact.

Principle. No grant exists in the Permissions store without its attestation in Actor Identity. The attestation is a prerequisite, not a complement.

Likely objection. “Why not record both as one transaction? Attesting first creates an orphan-attestation risk if the Permissions write fails.”

Mechanism that resolves it. A single transactional boundary across two atoms requires either (a) the atoms to share a database backend (which neither atom requires or specifies — both are vocabulary-neutral about storage) or (b) a distributed-transaction protocol at the composition layer (which is out of scope for the simplest two-atom composition). The attest-first ordering is the correct sequential approach because Actor Identity’s records are by construction immutable and verifiable independently — an orphan attestation is a recoverable anomaly (the composing system flags it, attempts the corresponding grant on retry, or accepts it as evidence of an attempted-but-failed administrative action). A grant in Permissions with no attestation, by contrast, is unrecoverable — the composition has no way to know what credential to attest with after the fact. The asymmetry of the failure modes makes attest-first the correct order.

Result. Application-level Invariant 1 (Attribution completeness) holds structurally: any grant the composition records was preceded by a successful attestation. Orphan attestations on the Actor Identity side are an acknowledged operational concern handled in Edge cases, but they do not violate Invariant 1.

The same logic applies to revoke_grant: attest the revocation first, then mutate Permissions. An orphan revocation attestation is recoverable evidence of an attempted revocation; a revoked grant with no revocation attestation would be an unattributed state change.

Composition-level invariants

These invariants emerge from the composition. None of them belong to a single constituent atom; each requires both atoms working together to hold.

Invariant 1 — Attribution completeness. For every grant_id in the Permissions store, grant_attribution[grant_id] is populated with a corresponding attestation_id in the Actor Identity store. Equivalently: the composition exposes no surface that records a grant without first recording its attestation. This invariant holds conditionally on the implementation satisfying the pairing-write durability requirement stated in issue_grant step 5 — the pairing write must be in the same transactional boundary as the Permissions write, or the implementation must use a write-ahead-log discipline that ensures either both succeed or neither is visible as committed. An implementation that permits the Permissions write to commit independently of the pairing write can violate this invariant during a failure window; the failure mode and the implementation requirement are named in Edge cases under Cross-store consistency under failure. (Established by issue_grant steps 3–5 and the attest-before-record wiring decision.)
Invariant 2 — Revocation attribution. For every grant in Revoked state in the Permissions store, revocation_attribution[grant_id] is populated with a corresponding attestation_id in the Actor Identity store. Equivalently: the composition exposes no surface that revokes a grant without first recording the revoker’s attestation. This invariant holds conditionally on the implementation satisfying the pairing-write durability requirement stated in revoke_grant step 5 — the pairing write must be in the same transactional boundary as the Permissions.revoke write, or the implementation must use a write-ahead-log discipline that ensures either both succeed or neither is visible as committed. An implementation that permits the Permissions.revoke write to commit independently of the pairing write can violate this invariant during a failure window; the failure mode mirrors Invariant 1’s, named in Edge cases under Cross-store consistency under failure. verify_grant_attribution step 4a returns attribution-inconsistency when this conditional fails. (Established by revoke_grant steps 3–5 and the attest-before-record wiring decision.)
Invariant 3 — Attribution recoverability. Given any grant_id known to Permissions, the composition’s records yield, without recourse to logs or developer narration: the grant’s full state (per Permissions’ invariants), the issuance attestation (per Invariant 1), the issuance attestation’s verify result, and — if the grant is Revoked — the revocation attestation and its verify result. verify_grant_attribution is the canonical query.
Invariant 4 — Attribution-time monotonicity. For every grant, attestation.attested_at ≤ grant.granted_at. The attestation precedes (or equals) the grant in wall-time because the attestation is recorded before the grant is recorded. Equivalent for revocations: revocation_attestation.attested_at ≤ grant.revoked_at. This invariant is best-effort under two conditions: (1) non-monotonic clocks per node — it holds under a monotonic clock and may be violated by NTP adjustments (the same clock-semantics caveat that applies to Permissions’ Invariant 9 and Actor Identity’s attested_at); (2) cross-system clock skew — attested_at is written by the Actor Identity store’s clock and granted_at / revoked_at is written by the Permissions store’s clock; if the two stores run on nodes with unsynchronized clocks, the inequality can be violated even when each node’s clock is monotonic. Deployments where Actor Identity and Permissions share a single clock source are protected against (2); deployments with separate clock sources should treat this invariant as a clock-alignment signal rather than a strong audit guarantee. Composing with Trusted Timestamping (RFC 3161) supplies an adversarially-defensible time anchor that addresses both conditions.
Invariant 5 — Constituent invariants preserved. All invariants of the Permissions atom hold over the Permissions instance. All invariants of the Actor Identity atom hold over the Actor Identity instance. The composition never bypasses preconditions; constituent rejections flow through unchanged (or are wrapped with composition-layer names like attribution-storage-failure to distinguish their origin).
Invariant 6 — Pairing-map durability. Once an entry is written to grant_attribution or revocation_attribution by the composition, it is never modified or deleted by the composition. The composition exposes no surface to update or remove either map; the only writes are the initial pairing writes in issue_grant step 5 and revoke_grant step 5. This is the composition-level analog of Actor Identity’s Invariant 9 (Attestation durability) and Permissions’ Invariant 10 applied to the composition’s own emergent state. An adversary with direct write access to the composition’s storage can rewrite the maps — the tamper surface named in Edge cases under Tamper-evidence over the composition’s emergent state; composing with Tamper Evidence over the composition’s emergent state addresses that surface.
Invariant 7 — Attestation exclusivity. Every attestation record referenced by the composition’s attribution maps is used exactly once and for exactly one purpose. Formally: grant_attribution is injective — no two grants share an issuance attestation; revocation_attribution is injective — no two grants share a revocation attestation; and the ranges of the two maps are disjoint — no attestation record serves as both issuance proof and revocation proof for any combination of grants. This invariant is enforced structurally by the proposal-format mechanism: every grant proposal includes a unique nonce (Invariant 7 holds because two distinct issue_grant calls produce distinct proposal_ref values and therefore distinct attestations), and the revocation proposal format {grant_id, requested_at} is structurally distinct from the grant proposal format by construction. (Surfaced by the Round 1 Alloy model — see Lineage notes. The prose review did not state this as a named invariant because the nonce mechanism was argued in Configuration as sufficient; the Alloy model revealed that the mechanism argument does not substitute for an invariant.)
Invariant 8 — Orphan log durability. Once an entry is written to the orphan log by the composition, it is never modified or deleted by the composition. The composition exposes no surface to update or remove orphan log entries; the only writes are in issue_grant step 4, issue_grant step 5, revoke_grant step 4, and revoke_grant step 5. This is the composition-level analog of Invariant 6 (Pairing-map durability) applied to the orphan log surface — same append-only discipline, same evidence-preservation purpose, same prohibition on the composition’s own surface mutating recorded entries. An adversary with direct write access to the composition’s storage can rewrite the orphan log — the same tamper surface named in Edge cases under Tamper-evidence over the composition’s emergent state; composing with Tamper Evidence over the orphan log addresses that surface. As with the attribution maps under Invariant 6, an externally-coordinated Retention Window purge may remove entries when its scope explicitly includes the orphan log; the Retention of attribution records edge case names that requirement. (Surfaced by Round 3; the append-only behavior was stated in Application state prose but never promoted to a named, checkable invariant. Generation acceptance check 5’s structural orphan detection is independent of the orphan log being populated or retained, but the log’s append-only durability is the operational-retry surface’s contract and warrants the same named-invariant status the attribution maps carry.)

Attribution completeness and attribution recoverability together give the attributable-by-construction property — the regulator’s question “who authorized this grant?” has a structural answer for every grant in the store, not a procedural one. Attribution-time monotonicity gives the audit-timeline-coherent property: the records cannot describe a grant that was issued before its grantor attested to it.

Examples

Walkthrough

A healthcare organization administers HIPAA-regulated access to ward-level patient records. A grant administrator issues a new grant for Dr. Chen.

The administrator (admin_a7) submits an issuance request. Subject: dr_chen. Scope: records:ward-7-patients. Grantor: admin_a7. Credential: admin_a7’s smart-card-bound credential, presented at the admin UI. Application call: issue_grant(dr_chen, records:ward-7-patients, admin_a7, admin_a7_credential).
The composition validates inputs. All fields non-empty and within length caps. Whitespace-normalized. Proceeds to step 3.
The composition constructs the proposal reference. proposal_ref = {dr_chen, records:ward-7-patients, nonce_n91a, 2026-05-18T14:32:11Z}, serialized canonically.
The composition calls ActorIdentity.attest(proposal_ref, admin_a7, admin_a7_credential). The smart-card-bound credential validates; the attestation is recorded with attestation_id = att_q88r. Returned to the composition.
The composition calls Permissions.grant(dr_chen, records:ward-7-patients). The grant is recorded with grant_id = grt_p44c. Returned to the composition.
The composition writes grant_attribution[grt_p44c] = att_q88r. The pairing is durable.
Return (grt_p44c, att_q88r) to the caller. The administrator’s UI displays “Grant issued — id grt_p44c, attestation att_q88r.”

Six months later, an internal compliance officer audits the ward-7 grants.

Audit query: verify_grant_attribution(grt_p44c). The composition retrieves the grant from Permissions: subject dr_chen, scope records:ward-7-patients, status Active, granted_at 2026-05-18T14:32:12Z. It retrieves grant_attribution[grt_p44c] = att_q88r. It calls ActorIdentity.verify(att_q88r) → verified. Returns the full tuple: the grant record, att_q88r, verified, no revocation.
The compliance officer concludes structurally: admin_a7 issued the grant on 2026-05-18, the attestation verifies under admin_a7’s currently-published key, and Dr. Chen has held the grant continuously since. The audit answer is the records’ answer; no developer testimony is consulted.

Later, Dr. Chen rotates to a different ward. Another administrator (admin_a8) revokes the grant.

Revocation request: revoke_grant(grt_p44c, admin_a8, admin_a8_credential). Validation passes. Revocation proposal {grt_p44c, 2026-08-01T09:15:00Z} is constructed.
ActorIdentity.attest(...) → att_r53s. admin_a8’s credential validates.
Permissions.revoke(grt_p44c) → ok. The grant moves Active → Revoked with revoked_at.
revocation_attribution[grt_p44c] = att_r53s is written durably.
Return (ok, att_r53s). The administrator’s UI displays “Grant revoked — attestation att_r53s.”

At year-end audit, verify_grant_attribution(grt_p44c) returns the full tuple including both attestations: admin_a7 issued; admin_a8 revoked. Both verify. The four-question audit answer (who, what, when, by whose authority) is complete from the records.

Rejection-path examples

invalid-credential on issue_grant. An administrator’s smart card has expired. Call: issue_grant(contractor_c12, source:production:read, admin_a7, a7_expired_credential). Step 1 validates inputs — all well-formed. Step 2 constructs proposal_ref = {contractor_c12, source:production:read, nonce_x04b, 2026-05-18T16:00:00Z}. Step 3 calls ActorIdentity.attest(proposal_ref, admin_a7, a7_expired_credential) → rejected(invalid-credential) (the smart-card validation service rejects the expired token). The composition immediately returns rejected(invalid-credential) to the caller. No grant recorded. No orphan attestation — the attest call was rejected before any record was written in Actor Identity.

not-active on revoke_grant (double-revocation attempt). A previous revocation of grant grt_p44c succeeded (attestation att_r53s was recorded in a prior call). A second revocation attempt arrives — perhaps a UI retry after a network timeout that did not actually fail server-side. Call: revoke_grant(grt_p44c, admin_a8, admin_a8_credential). Step 1 validates inputs. Step 2 constructs revocation_proposal_ref = {grt_p44c, 2026-08-01T09:15:42Z}. Step 3 calls ActorIdentity.attest(...) → att_r99z (the attestation is recorded — Actor Identity does not know the grant is already revoked). Step 4 calls Permissions.revoke(grt_p44c) → rejected(not-active) (Permissions sees the grant is already Revoked). An orphan attestation att_r99z now exists; the composition logs the orphan (with the underlying not-active reason) and returns rejected(not-active) to the caller. The original revocation attestation att_r53s is unaffected; att_r99z is recoverable evidence of the attempted double-revocation.

orphan-attestation on issue_grant (grant-side storage failure). A write-heavy deployment experiences intermittent storage pressure. Call: issue_grant(dr_chen, records:ward-8-patients, admin_a7, admin_a7_credential). Step 3 calls ActorIdentity.attest(...) → att_q77t (attestation recorded successfully). Step 4 calls Permissions.grant(dr_chen, records:ward-8-patients) → rejected(storage-failure) (the Permissions store returns a transient error). An orphan attestation att_q77t now exists in Actor Identity with no corresponding grant in Permissions. The composition logs the orphan (attestation id, proposal ref, timestamp, underlying reason grant-storage-failure) and returns rejected(orphan-attestation) to the caller. The caller’s appropriate response: retry issue_grant (which will produce a new nonce and a new proposal_ref, and therefore a new attestation on retry — the prior orphan attestation att_q77t remains in Actor Identity as evidence of the failed attempt). The Failed-Grant Reconciliation pattern described in Edge cases is responsible for periodically confirming that att_q77t remains an orphan or flagging it for manual review.

Banking — SOX-scoped wire-transfer authorization grants

A bank’s controls require that the ability to approve high-value wires (>$25,000) be granted by a named manager and that the grant itself carry the manager’s verifiable approval. issue_grant(supervisor_s4, approve:transfer, ops_manager_m9, m9_credential) → (grt_b1, att_b1). Six months later a SOX §404 internal-control review queries the grant store: every active approve:transfer grant must be linked to a verified attestation under a current operations manager’s credential. The composition’s audit query produces the structural answer; no audit-tool integration is needed to cross-reference grant records against an external approval log.

Healthcare — HIPAA minimum-necessary access grants with named granter

A hospital’s HIPAA compliance program requires that every patient-record access grant be attributable to the privacy officer or their delegate who issued it. issue_grant(dr_chen, records:ward-7-patients, privacy_officer_p2, p2_credential) → (grt_h1, att_h1). When OCR (HHS Office for Civil Rights) audits the hospital after an unrelated breach, the audit team enumerates active grants on PHI scopes and verifies each grant’s attestation. Any grant whose attestation fails to verify (because the named granter’s credential was rotated and the registry no longer recognizes the original key) is flagged for re-attestation or revocation; the failure is a finding, but a finding the records surface structurally rather than one that hides until the next audit.

Payments — PCI DSS Requirement 7 attributed authorization

PCI DSS Requirement 7 mandates restricted access to cardholder data with formal access authorization documented in records. issue_grant(analyst_a6, cardholder-data:read, security_lead_l3, l3_credential) → (grt_p1, att_p1). A QSA’s annual assessment walks the cardholder-data grants. For each: who is the subject, what scope, who authorized it, can the authorization be cryptographically verified? The composition’s verify_grant_attribution is the structural answer to all four questions per grant.

Legal — matter-staffing grants with partner attribution

A law firm’s matter-management system grants associates access to documents in matters they are staffed on. The firm’s professional-responsibility rules require that staffing decisions be attributable to the responsible partner. issue_grant(associate_j, documents:matter-2024-91, partner_k, partner_k_credential) → (grt_l1, att_l1). When opposing counsel’s discovery request asks the firm to demonstrate matter-team composition over time, the firm produces the grant records with verified partner attestations — a structurally defensible answer to the question of who decided who had access.

Source control — FDA-regulated branch-protection grants

An FDA-cleared medical-device team restricts merge access to the release branch and requires every grant to be issued by the release engineer’s manager. issue_grant(release_engineer_r, branch:release:merge, eng_director_d, d_credential) → (grt_s1, att_s1). During an FDA 21 CFR Part 11 software-validation audit, the auditor queries the grant store and verifies every active release-branch grant’s attestation. Grants whose attestations verify under the current director’s credential satisfy the regulatory bar; grants whose attestations fail to verify (because the original director left the company and their credential is no longer registered) are surfaced for re-attestation under the new director.

The mechanic is identical across all five. What differs: the scope vocabulary, the regulatory regime (SOX, HIPAA, PCI DSS, professional responsibility, 21 CFR Part 11), the credential mechanism (smart card, hardware token, qualified electronic signature), and the composing patterns active around it (Audit Trail composition for the grant-issuance event log, Retention Window for grant-record lifetime, Tamper Evidence over the grant store, RBAC for role-based grant batching).

Regulated adversarial scenarios

Three scenarios the composition must survive in regulated contexts:

Regulator audit — “show me every active grant and prove who authorized each one.” A regulator (HIPAA OCR, SOX auditor, PCI QSA, FDA inspector) queries the composition: for each Active grant in the Permissions store, produce the grantor’s verified attestation. The composition’s verify_grant_attribution returns the tuple for each grant. Invariants 1 and 3 are the structural answer: every grant in the store has a paired attestation (Invariant 1); the pairing is recoverable from the records alone (Invariant 3). Grants whose attestations fail to verify are themselves structurally observable — the audit query distinguishes verified from failed-verification(...) from not-known and the regulator sees the distribution directly. There is no developer testimony in the loop.
Disputed grant — “I never authorized this grant.” A named grantor claims they did not issue a specific grant. The investigator calls verify_grant_attribution(grant_id). If issuance_verify_result = verified, the proof binds the named grantor to the grant proposal at attested_at (Actor Identity’s Invariant 8 — non-repudiation contract). The grantor cannot plausibly deny it without claiming credential compromise — which is then an out-of-band investigation governed by a Compromise Disclosure composing pattern. If failed-verification(...), the dispute is upheld and the grant’s status is reconsidered (revocation is the typical follow-on action, itself recorded as an attributed administrative action).
Breach forensics — “the grant store may have been tampered with.” A security incident suggests an attacker may have inserted unauthorized grants directly into the Permissions store, bypassing the composition. The investigator enumerates all grants in the Permissions store and, for each, calls verify_grant_attribution. Any grant for which grant_attribution[grant_id] is unpopulated, or for which the paired attestation verifies as not-known (the attestation id was never recorded), or for which the attestation verifies as failed-verification(proof-invalid) (the attestation exists but the proof does not bind the named grantor) is flagged as a structurally illegitimate grant. The investigation’s forensic boundary is exactly the population of grants whose attestations fail; everything inside that boundary is structurally defensible. Composing with Tamper Evidence over the Permissions store and the Actor Identity store turns the breach scope into a verifiable cryptographic claim rather than an investigator’s assertion.

Generation acceptance

A derived implementation of Attributed Permissions Admin is acceptable — in the regulator-acceptance sense — when an external auditor, given the composition’s emergent state plus the two constituent stores, can do all of the following without recourse to source code, runbooks, or developer narration.

Audit-Trail-traversal-clearable checks

Checks the composition’s records alone answer:

For every grant in the Permissions store, produce the issuance attestation and its verify result. From grant_id: look up grant_attribution[grant_id] (Invariant 1 guarantees the lookup succeeds); call ActorIdentity.verify(attestation_id); report the result. The composition exposes verify_grant_attribution as the canonical query. Application-level Invariant 1 and Invariant 3 are the structural answer.
For every Revoked grant, produce the revocation attestation and its verify result. Same as above, against revocation_attribution[grant_id]. Application-level Invariant 2.
Verify the attribution-time monotonicity contract for every grant. For each grant, check attestation.attested_at ≤ grant.granted_at. Application-level Invariant 4. Under non-monotonic clocks or cross-system clock skew the contract is best-effort; the auditor sees the inequality directly and can flag exceptions.
Verify each constituent atom’s Generation acceptance bar over its own instance. Permissions’ Generation acceptance (enumerate every grant with full history, reconstruct authorization state at any past point in time, confirm denial by absence, confirm revocation is terminal and immediate, identify active composing patterns). Actor Identity’s Generation acceptance (enumerate every attestation, verify every attestation against the actor registry, distinguish verified from failed-verification from not-known outcomes).
Identify orphan attestations. Using the deployment’s configured namespace prefix (required by grant_proposal_format and the fixed revocation_proposal_format — see Configuration), enumerate all attestations in the Actor Identity store whose action_ref begins with that prefix. This set is the complete population of composition-issued attestations (both grant proposals and revocation proposals share the namespace). Cross-reference each attestation_id against grant_attribution and revocation_attribution: any attestation whose id is absent from both maps is an orphan — a structurally observable failed-issuance-or-revocation. Each orphan is evidence of an attempted action that did not complete; the audit either accepts it as benign (retried and succeeded, or abandoned) or queries the failed-grant-reconciliation pattern that handles them. The audit’s ability to enumerate orphans completely — and to bound the orphan population rather than merely sample it — depends directly on the namespace prefix being present and consistent in both proposal formats. A deployment that omits the namespace prefix from either proposal format cannot satisfy this check from the records alone; action_ref values become indistinguishable from attestations issued by other composing systems and the orphan population cannot be bounded. The audit’s distinction between “orphan attestation we can see” and “missing attestation we can’t see” is the composition’s contribution to forensic completability; the namespace prefix is the structural requirement that makes the distinction possible. Note: the orphan log in Application state is the composition’s operational retry surface; the audit’s orphan detection described here is independent — it operates structurally against Actor Identity and the two maps, and does not require the orphan log to be populated or retained.
Verify attestation exclusivity (Invariant 7). Enumerate grant_attribution and revocation_attribution. Confirm no attestation_id appears more than once in grant_attribution (injectivity of issuance map). Confirm no attestation_id appears more than once in revocation_attribution (injectivity of revocation map). Confirm the two sets of attestation_id values are disjoint — no attestation appears in both maps. Any violation is a structural breach of Invariant 7 — Attestation Exclusivity — surfacing either a nonce-uniqueness failure (two grant proposals produced the same proposal_ref), a fixed-format collision (a revocation proposal somehow matched a grant proposal), or adversarial reuse of an attestation across roles. Application-level Invariant 7.

Externally-clearable checks

Questions that arise around the composition but require external evidence to answer:

Was the grantor authorized to issue this grant per organizational policy? The composition records that the named grantor attested; it does not record whether organizational policy permits that grantor to issue this scope. A Delegation composing pattern (forthcoming) or an external policy registry supplies the answer.
Has the grantor’s credential been compromised since attested_at? Actor Identity’s non-repudiation contract is conditional on credential integrity; reinterpretation under compromise belongs to a Compromise Disclosure composing pattern. The composition’s records do not invalidate themselves under credential compromise — invariants 1 and 5 are immutable — but the meaning of verified results may shift under external disclosure.
Does the composition’s emergent state itself preserve tamper-evidence? grant_attribution and revocation_attribution are deployment-owned maps; without composing with Tamper Evidence over them, the auditor must trust the implementation’s storage discipline. Composing with Tamper Evidence elevates the trust to a verifiable cryptographic claim.
Was the grant’s scope vocabulary recognized by the system at the time of grant? The composition treats action_scope as opaque; whether a given scope was a valid scope per the deployment’s policy belongs to a Scope Registry composing pattern.

This is the generator’s contract: any code generated from this composition must produce records and a runtime surface that pass the Audit-Trail-traversal-clearable checks above. The Externally-clearable checks document the boundary of what the composition itself can prove; they are not the composition’s own contract to satisfy but they are part of an honest answer to the regulator when the composition’s evidence ends.

Edge cases and explicit non-goals

What this composition does not cover:

Grantor authorization (separation-of-duties). Whether grantor_ref is permitted to issue a grant for the given action_scope belongs to a higher-layer policy: a Delegation composing pattern (which checks that the grantor holds a meta-grant covering “grant for scope X”), an RBAC layer (which checks that the grantor holds an “admin” role for the scope’s domain), or organizational policy reviewed externally. This composition records the grantor’s attestation; it does not validate the grantor’s authority to grant. Externally-clearable in the Generation acceptance split below.
Role management. Mapping a role name to a set of (subject, scope) grants — and revoking the set when the role is rescinded — belongs to a RBAC composing pattern that calls this composition once per grant. The bare composition handles individual grants; bulk role operations are the composing layer’s responsibility.
Mass revocation on grantor deprovisioning. When an administrator leaves the organization, every grant they issued remains valid (the attestation stands as a permanent record of the historical authorization). What may need re-attestation is a separate organizational decision: do the grants the departing administrator issued still represent the organization’s intent? This composition records the historical attribution; the decision to re-attest or revoke belongs to organizational policy.
Orphan attestation handling. If Permissions.grant fails after ActorIdentity.attest succeeds, an orphan attestation exists in the Actor Identity store with no corresponding grant. The composition acknowledges the orphan, returns a composition-layer rejection naming it, and logs the orphan for the composing system’s orphan-resolution process. The composition does not delete the orphan — Actor Identity’s Invariant 9 (Attestation durability) forbids it. High-assurance deployments should compose with a Failed-Grant Reconciliation pattern that periodically enumerates Actor Identity attestations under composition-issued proposal references and confirms each has a corresponding grant_attribution entry; orphans are flagged for manual review or retry.
Cross-store consistency under failure. If Permissions.grant succeeds but writing grant_attribution[grant_id] = attestation_id fails (durability failure), the composition has a grant in the store with no recorded pairing — the worst case for Invariant 1. The symmetric case exists for revocation: if Permissions.revoke succeeds but writing revocation_attribution[grant_id] = attestation_id fails, the composition has a Revoked grant with no recorded revocation pairing — the worst case for Invariant 2. The composition’s contract for both cases: the pairing write must be in the same transactional boundary as the corresponding Permissions write, or the implementation must use a write-ahead-log discipline that ensures either both writes succeed or both are absent. The bare composition spec names the requirement; the implementation owns the mechanism. verify_grant_attribution step 2a returns attribution-inconsistency for the Invariant 1 failure window; step 4a returns the same code for the Invariant 2 failure window — both surfaced as forensic findings under the Caller contract paragraph in Action wiring, not as normal lookup misses. A Cross-Store Coordination composing pattern (the same one Audit Trail names) handles the general case.
Concurrent issuance of the same grant. Two simultaneous issue_grant(subject_ref, action_scope, ...) calls for the same (subject_ref, action_scope) pair from different grantors produce two distinct attestations and two distinct grants — Permissions’ Edge case Concurrent grant proliferation allows this. The composition does not prevent it; whether the duplicate is intentional (a second grantor confirming) or accidental (a UI double-click before the first request returned) is a composing-layer concern. Deployments that need single-issuance semantics should compose with Idempotent Reservation or wrap issue_grant with a token-based deduplication layer.
Credential rotation between issuance and revocation. A grantor who issues a grant under credential C1 may later revoke under rotated credential C2. The composition records two separate attestations; both verify under the actor registry’s view of the actor at their respective attested_at times (per Actor Identity’s Invariant 6 and Edge case Verification result caching). The historical attribution remains stable; only the verification result depends on the registry’s handling of credential history. Composing with an Actor Registry that maintains historical credential material is required for full historical verification.
Clock semantics for proposal references. The requested_at field in both grant_proposal_format and revocation_proposal_format is taken from the composition’s wall-time clock at invocation time. This field is informational within the proposal — the nonce ensures proposal uniqueness regardless of whether two proposals share the same requested_at. If the wall-time clock is adjusted backward (NTP correction), requested_at may be earlier than the previous call’s requested_at; this does not affect uniqueness but will appear as a timestamp discontinuity in audit records. If the clock is significantly ahead of the constituent stores’ clocks, Invariant 4 (Attribution-time monotonicity) may appear violated (attested_at < granted_at may not hold) even for legitimate proposals — see Invariant 4’s cross-system clock skew condition and the clock note in Configuration. Implementations should record the wall-time clock source alongside the composition’s emergent state to enable post-hoc disambiguation of clock anomalies.
Tamper-evidence over the composition’s emergent state. grant_attribution and revocation_attribution are emergent maps; if an adversary with write access can rewrite them, they can re-pair grants to different attestations and forge attribution. Cryptographic hash chains, Merkle-tree commitment, or external anchoring over the emergent state belong to a Tamper Evidence composing pattern applied to the composition’s state — the same composition Audit Trail applies to its emergent state. The bare composition assumes the emergent state has not been adversarially rewritten.
Retention of attribution records. The Permissions store and the Actor Identity store each have their own retention obligations (typically the longer of the two applies to the pair). The composition does not specify a retention policy; composing with Retention Window (or with the Audit Trail composition over the pair of stores) supplies the retention discipline. However, a Retention Window composing pattern that purges records from the Permissions or Actor Identity stores must explicitly scope its purge to include the corresponding entries in grant_attribution, revocation_attribution, and the orphan log — otherwise, after a Permissions grant is purged, orphaned map entries persist indefinitely (Invariant 6 forbids the composition from deleting map entries on its own; only an externally-scoped retention purge can do so). A purge that removes a grant from Permissions without removing its grant_attribution and revocation_attribution entries leaves dangling map entries pointing at deleted records; the Application state lifetime claim (“while a grant exists in the Permissions store, its attribution record exists in the map”) cannot be inverted without explicit cross-store coordination in the Retention Window scope. The bare composition names the requirement; the retention composing pattern owns the mechanism.
Multi-actor authorization (m-of-n grant issuance). A grant that requires two or more administrators to attest jointly is a separate composing pattern (Witness / Co-signature, or Multi-Party Approval over a grant-issuance action type). This composition records one attestation per grant; multi-actor schemes wrap it with an additional layer that aggregates multiple attestations before invoking issue_grant.
Grant modification (as distinct from revoke-and-re-issue). Permissions has no edit surface — subject_ref and action_scope are immutable per Invariant 1. To “modify” a grant, the composing system revokes the original and issues a new one. Both administrative actions are attributed under this composition; the audit trail shows the revocation and the new issuance as separate attributed events. The composition does not provide a modify shortcut.
permitted query attribution. The composition does not attribute permitted queries (i.e., it does not record who asked whether a subject was permitted). Whether and how to log access checks belongs to an Event Log composing pattern; the composition’s contract is about administrative state changes (grants and revocations), not about evaluation queries.

Where the composition breaks down: when the host environment lacks an actor registry the verifier can consult (Actor Identity’s verify cannot complete); when the grantor’s credential mechanism cannot produce a verifiable proof (shared-secret credentials); when the Permissions store and the Actor Identity store have inconsistent retention policies such that attestations are purged while grants persist (or vice versa) — composing with Defensible Retention over the pair handles this.

Standards references

This composition draws on:

NIST SP 800-53 Rev. 5, AC-3 (Access Enforcement) + AU-2 (Event Logging) + IA-2 (Identification and Authentication, Organizational Users) — the combined administrative-action-with-attribution surface that AC-3 + AU-2 together require, with IA-2 supplying the grantor identity discipline.
SOX §404 (Internal Control over Financial Reporting) — segregation-of-duties controls over access provisioning; the composition produces the records §404 examines.
HIPAA §164.312(a)(1) + §164.312(b) (Technical Safeguards — Access Control + Audit Controls) — the combined access-control-with-audit-controls bar that the two paragraphs together establish; the composition is the structural form that satisfies both without the system administrator filling the gap by hand.
PCI DSS Requirement 7 (Restrict Access to System Components and Cardholder Data) + Requirement 10 (Track and Monitor Access) — Requirement 7 mandates that access authorization be documented; Requirement 10 mandates that the documentation be tamper-evident and attributable. The composition satisfies the first; composing with Tamper Evidence over its stores satisfies the second.
21 CFR Part 11 §11.10 (Controls for closed systems) + §11.50 (Signature manifestations) — Part 11’s electronic-signature regime applied to the grantor’s attestation on an administrative action.
GDPR Article 25 (Data Protection by Design and by Default) + Article 30 (Records of Processing Activities) — the composition’s records satisfy the Article 30 record-keeping obligation for the access-control processing activity.
ISO/IEC 27001 §A.9.2 (User access management) — formal user-access-management procedure with records of authorization; the composition is the structural answer.

The two atoms it composes carry their own standards inheritance — Permissions (NIST SP 800-53 AC family, NIST SP 800-207 Zero Trust, ISO/IEC 27001 §A.9, HIPAA §164.312(a)(1), SOX §404, PCI DSS Req. 7, GDPR Art. 25, NIST SP 800-63-3) and Actor Identity (eIDAS Regulation qualified electronic signatures, DEA EPCS for controlled-substance prescriptions, ISO 14533 and CAdES for long-term signature preservation, 21 CFR Part 11 §11.50).

It inherits from:

Daniel Jackson, The Essence of Software — the composition discipline: an application is the wiring of freestanding concepts, not a new primitive. Attribution and authorization are separate concepts; the composition wires them rather than absorbing attribution into Permissions.
The principle of attributable administrative action — the structural form of what professional-responsibility codes (legal, medical, financial), regulatory regimes (SOX, HIPAA, PCI DSS), and security frameworks (NIST, ISO 27001) all require: every state-changing administrative action carries a verifiable record of who authorized it. The composition gives the principle a single composable concept.

Status

grounded on Final Critique 6 — 2026-05-23 — Composition logic specified across both constituent atoms; emergent state (grant_attribution, revocation_attribution, orphan log) named with explicit identity model (keyed by grant_id); two state-changing actions (issue_grant, revoke_grant), one attribution query (verify_grant_attribution) carrying a formal Caller contract paragraph for forensic-finding result codes, and one passthrough evaluation (permitted), with rejection taxonomies unified around orphan-attestation for all orphan-producing failure paths; verify_grant_attribution carries an attribution-inconsistency result tag for the Invariant 1 conditional-failure path (step 2a) and the symmetric Invariant 2 conditional-failure path (step 4a); eight application-level invariants stated (Invariant 6 — Pairing-map durability and Invariant 7 — Attestation Exclusivity both added in Round 1; Invariant 7 surfaced by Alloy formal model; Invariant 8 — Orphan log durability added in Round 3, covered by the dynamic Alloy model in Final Critique 4); walkthrough, three rejection-path examples (invalid-credential, not-active, orphan-attestation), plus five domain examples (banking SOX, healthcare HIPAA, payments PCI DSS, legal professional responsibility, source control FDA 21 CFR Part 11) and three regulated adversarial scenarios (regulator audit, disputed grant, breach forensics); thirteen edge cases including orphan attestation handling, cross-store consistency under failure (covering both Invariant 1 and Invariant 2 worst cases), concurrent issuance, credential rotation, clock semantics for proposal references, and tamper-evidence over emergent state; Generation acceptance in canonical position (after Examples, before Edge cases) with Audit-Trail-traversal-clearable (six checks, including orphan-attestation check 5 requiring namespace prefix and Invariant 7 attestation-exclusivity check 6) and Externally-clearable (four checks); dynamic Alloy trace model with six LTL assertions covering Invariants 1, 2, 6 (pairing-map durability over time), 8 (orphan log durability over time), revocation terminality, and the attest-before-record consequence; TLA+ operational peer at compositions/attributedPermissionsAdmin.tla (+ .cfg) checks the same eight named invariants under TLC’s exhaustive-interleaving semantics at bounds {a1,a2} × {g1,g2} × {t1,t2,t3}, MaxClock=4, single (s, x) pair — all eight invariants hold across 397 reachable states. Eighth entry in compositions/. Round 1 (Pass 1 GRID structural, Pass 2 EOS conceptual independence, Pass 3 Linus adversarial) complete; sixteen findings resolved. Round 2 complete; seven findings resolved. Round 3 complete; five findings resolved (Pass 1: one stale-reference cleanup; Pass 3: four — Invariant 2 conditional gap, orphan-log-durability invariant promotion, caller-contract formalization, dynamic-trace Alloy model). Final Critique 4 complete; two findings resolved (Pass 3: two — dynamic-model comment accuracy on the attest-before-record assertion, Invariant 8 added to the dynamic Alloy model) — see Lineage notes. Round 5 (touch-triggered re-pass, 2026-05-20): TLA+ Lineage entry reframed to acknowledge Round 5 as the triggered round; redundant parenthetical removed from Final Critique 4 round summary; article correction (a → an) in revoke_grant step 3 inline note; demos/ stale Alloy copy resolved by repo hygiene pass before this round ran. Round 6 (touch-triggered re-pass, 2026-05-23): TLC CLI re-run after .tla rename (kebab-case → camelCase, SANY filename↔module-name fix); NULL = NullMV model-value override added to .cfg for TLC 2.19 strict-equality compatibility; 397 states confirmed clean, all nine invariants hold. Convention: rounds 1–3 are the 3×3 baseline (each round runs Pass 1 GRID / Pass 2 EOS / Pass 3 Linus); Final Critique N is the Final Critique under the unified methodology — grounding is recorded as grounded on Final Critique N where N is the round at which the Final Critique passes.

Lineage notes

This composition is the first entry in the library whose central concern is attributed administration of an authorization surface — pairing the whether-a-permission-exists atom (Permissions) with the who-authorized-it atom (Actor Identity) into a single coherent administrative surface where the records alone answer the regulator’s four questions (who, what, when, by whose authority).

Structural milestone. This composition retires the forthcoming-link in Permissions’ Composition notes that names grantor attribution via Actor Identity composing with grant as a future composing pattern. The Permissions atom’s text “Calling attest(grant_action_ref, grantor_ref, grantor_credential) alongside grant produces a verifiable non-repudiation record for each grant issuance. The composing system stores attestation_id alongside grant_id” is now a named composition rather than an inline suggestion. Similarly retires the implicit forthcoming-link in Actor Identity’s Composition notes section that names authorization-with-attribution as a downstream composing surface.

Conventions inherited from the methodology. The regulated-pattern conventions — Regulated adversarial scenarios and Generation acceptance split into Audit-Trail-traversal-clearable and Externally-clearable — are inherited from the canonical methodology in PRESSURE_TESTING.md and baked in from the first draft. The split-Generation-acceptance convention is inherited from Multi-Party Approval’s Round 3 (where it was canonicalized) and applied here directly. Lineage cites the methodology, not earlier worked examples.

Pass 1 — Structural completeness (GRID), Round 1. Complete. Five findings; all closed in-pattern.

F1.1 — issue_grant signature inconsistency. The signature listed grant-storage-failure as a distinct rejection code for the step-4 storage-failure path, but the step-5 pairing-write failure already used orphan-attestation for the same structural situation (a grant exists without an attributed pairing). The asymmetry was arbitrary and misleading. Closed: unified grant-storage-failure into orphan-attestation across the issue_grant signature and step 4 prose; the orphan log carries the underlying cause.
F1.2 — revoke_grant signature inconsistency. Same pattern: revocation-storage-failure was listed separately from orphan-attestation for a situation where a revocation-side storage failure also produces an orphan attestation. Closed: unified with the same fix applied to revoke_grant step 4 and signature.
F1.3 — Emergent state identity model implicit; Invariant 6 missing. Application state named the two maps but never stated their key (grant_id) as the composition’s identity handle or that the composition introduces no new entity identity. Invariant 6 (pairing-map durability) was referenced by action wiring and Application state prose but did not exist in the invariants list. Closed: added explicit identity model paragraph to Application state; added Invariant 6 — Pairing-map durability; updated Summary invariant count from five to six.
F1.4 — Generation acceptance in wrong section position. The section was placed after Standards references, contrary to the canonical position in SPEC_FORMAT.md (after Examples, before Edge cases). Closed: moved.
F1.5 — Concurrent-issuance edge case misnaming. The edge case cited “Permissions’ Invariant concurrent grant proliferation” — concurrent grant proliferation is an Edge case in the Permissions atom, not one of its numbered invariants. Closed: corrected to “Permissions’ Edge case Concurrent grant proliferation.”

Pass 2 — Conceptual independence (EOS), Round 1. Complete. No findings. All concerns the drafter identified as over-absorption candidates — grantor authorization / separation-of-duties, role management, mass deprovisioning, tamper-evidence over emergent state, retention of attribution records, multi-actor authorization, permitted query attribution — are correctly externalized in Edge cases with named composing patterns. No concept embedded in this composition requires extraction as a separate atom.

Pass 3 — Adversarial scrutiny (Linus mode), Round 1. Complete. Eleven findings; all closed in-pattern.

F3.1 — Identity model implicit in Application state. Same finding as F1.3; addressed together.
F3.2 — grant_record shape undefined. verify_grant_attribution’s return type included grant_record but never defined its shape. An auditor implementing the query cannot write the return type. Closed: added grant_record shape definition ({grant_id, subject_ref, action_scope, status, granted_at, revoked_at?}) inline in the action step.
F3.3 — requested_at clock source unspecified. requested_at appeared in both proposal formats and in step 2 of each action with no statement of where it comes from. A deployment with a misconfigured or mocked clock could produce proposals inconsistent with the constituent atoms’ timestamps, violating Invariant 4 without the composition naming the mechanism. Closed: added a clock note to the Configuration section (covering both proposal formats and citing the NTP caveat); added inline references at step 2 of each action; added Clock semantics for proposal references edge case.
F3.4 — Invariant 4 missing cross-system clock skew condition. The invariant named only the NTP-adjustment caveat for per-node non-monotonic clocks, but attested_at is written by Actor Identity’s clock and granted_at / revoked_at is written by Permissions’ clock — if those stores run on separate nodes, the inequality can be violated even under a per-node monotonic clock. Closed: added cross-system clock skew as a second condition, named which stores supply which timestamps, and noted that single-clock-source deployments are protected against it.
F3.5 — No rejection-path examples. The walkthrough covered only the happy path through the entire issuance-audit-revocation-reaudit arc. The rejection taxonomy includes invalid-credential, not-active, and orphan-attestation — each a structurally distinct outcome that a fresh reader cannot trace from the action wiring alone. Closed: added three rejection-path examples with concrete ids: invalid-credential on issue_grant (expired smart card), not-active on revoke_grant (double-revocation attempt), and orphan-attestation on issue_grant (grant-side storage failure with retry semantics).
F3.6 — “Cannot bypass” overclaim in Intent. The sentence “one administered action you cannot bypass” implied the composition was tamper-proof at all layers. An adversary with direct write access to the underlying Permissions store can insert unattributed grants without touching the composition. Closed prior to Round 1 pass record: qualified to “cannot bypass through the composition’s surface” and added an explicit sentence naming the direct-write tamper surface and the Tamper Evidence composing pattern as the remedy.
F3.7 — Invariant 1 unconditional. The invariant stated “for every grant_id in the Permissions store, grant_attribution[grant_id] is populated” without acknowledging that issue_grant step 5 (the pairing write) can fail after the Permissions write succeeds, violating the invariant during a failure window. The invariant was stronger than the action wiring could guarantee. Closed: added conditional qualification pointing to step 5’s durability requirement and the Cross-store consistency edge case as the named failure mode.
F3.8 — grant_proposal_format missing namespace prefix requirement; Generation acceptance check 5 incompletable. Without a namespace prefix on composition-issued action_ref values, the orphan attestation enumeration in Generation acceptance check 5 cannot be bounded: the auditor has no structural criterion to filter composition-issued attestations from foreign ones in a shared Actor Identity store. Closed: added namespace prefix as a second required rule in grant_proposal_format; updated check 5 to state the namespace prefix as the structural requirement that makes orphan enumeration possible.
F3.9 — not-known from ActorIdentity.verify unexplained in verify_grant_attribution. Step 3 of verify_grant_attribution passes the result of ActorIdentity.verify through without noting that not-known at this step — where Invariant 6 and Actor Identity’s Invariant 9 both guarantee the attestation id should exist — is a tamper signal, not a routine lookup miss. A fresh reader treats not-known as equivalent to the not-known from step 1 (grant not found) and misses the forensic implication. Closed: added tamper-signal explanation at step 3 (and the same note at step 4 for revocation attestations).
F3.10 — revocation_proposal_format non-configurability undefended. The non-configurability was stated as a parenthetical (“not configurable”) with only “the grant id is already unique; no nonce is needed” as rationale — a preference argument, not a defended architectural decision. The actual reason is stronger: making revocation_proposal_format configurable would allow a misconfigured deployment to produce revocation proposals outside the grant namespace, breaking the namespace-prefix-based orphan enumeration. Closed: applied four-step rubric (principle, likely objection, mechanism, result) with the namespace-correctness argument as the mechanism.
F3.11 — permitted passthrough not stated as a formal action. permitted was mentioned in Composes (“passed through unchanged”) and at the end of Action wiring in prose, but never stated as a formal action entry with a signature. An implementer reading only Action wiring would not know the composition exposes a permitted evaluation path. Closed: added permitted(subject_ref, action_scope) → permitted | denied as a formal action entry in Action wiring, immediately after verify_grant_attribution.

Formal model — Round 1 static structural model. compositions/attributed-permissions-admin.als — an Alloy model covering the six application-level invariants as facts and running five checks and three instance-finding predicates. The model is directly loadable by the Alloy Analyzer. It confirmed Invariants 1–3 and 6 are satisfiable and that Invariant 3 (recoverability) follows structurally from Invariant 1. It also identified one spec gap the prose review did not catch: three of the five checks find counterexamples because the model’s facts do not prevent the same Attestation atom from being used as the issuance proof for multiple grants, as both issuance and revocation proof for the same grant, or as the issuance proof for one grant and the revocation proof for another. All three counterexamples are facets of one missing invariant — Invariant 7 — Attestation Exclusivity: every Attestation record is used at most once, for exactly one purpose (issuance or revocation), for exactly one grant. The spec relies on the proposal-format mechanism (nonce uniqueness, fixed revocation format) to enforce this in practice, but never promotes the consequence to a named, checkable invariant. The model includes Invariant 7 in commented-out form; uncommenting it causes all three checks to pass. Invariant 7 closed before Round 2: added to the spec as a named invariant and activated as a fact in the Alloy model; all three previously-failing checks now pass clean. Dynamic trace model (verifying that issue_grant and revoke_grant reach and maintain the invariants over operation sequences) is deferred to Round 3.

Pass 1 — Structural completeness (GRID), Round 2. Complete. One finding; closed in-pattern.

F2.1 — Status invariant count stale. Status section said “six application-level invariants stated” after Invariant 7 was added when the Alloy finding was closed before Round 2. Summary (correctly) said “seven.” Closed: updated Status to “seven application-level invariants stated; Invariant 6 and Invariant 7 both added in Round 1.”

Pass 2 — Conceptual independence (EOS), Round 2. Complete. No findings. Orphan log, attribution maps, and all emergent concerns are correctly scoped to this composition. No concept embedded here requires extraction as a separate atom.

Pass 3 — Adversarial scrutiny (Linus mode), Round 2. Complete. Six findings; all closed in-pattern.

F2.2 — Orphan log schema defined only in an example parenthetical. The spec invoked “logs the orphan” six times but defined the log entry shape only in a parenthetical inside a rejection-path example. An implementer reading the action wiring had nothing to derive the schema from. Additionally, the relationship between the orphan log (operational) and audit-time orphan detection (structural, via Actor Identity + maps) was invisible. Closed: added a formal orphan log entry in Application state with the explicit schema {attestation_id, proposal_ref, requested_at, underlying_reason} and an enumerated underlying_reason vocabulary; added a sentence distinguishing the log (operational, for retry) from check 5’s structural detection (independent of the log). [Note: this entry originally read “check 6”; Round 3 F3.5 corrected it to the current numbering after Round 2 F2.6 added Invariant 7’s check at position 6.]
F2.3 — Revocation proposal namespace prefix stated as rationale, not as a rule. The revocation_proposal_format section said namespace enumerability “is satisfied by” the shared prefix — rationale language. A deployment could apply the prefix to grant proposals but not revocation proposals and satisfy the letter of the rules. Closed: added an explicit requirement: “the revocation proposal body must be prefixed with the same deployment-specific namespace prefix used for grant proposals” stated as a hard rule at the top of the revocation_proposal_format section.
F2.4 — verify_grant_attribution has no code path when Invariant 1’s conditional fails. Invariant 1 is conditional on pairing-write durability. If the pairing write fails after the Permissions write succeeds, a grant exists in the store with no grant_attribution entry. Step 2 asserted the lookup is guaranteed by Invariant 1 but had no path for this reachable failure state; the action was undefined when Invariant 1’s conditional broke. Returning the same not-known code as step 1’s “grant not found” case would conflate structurally different conditions. Closed: added attribution-inconsistency as a new result tag to the action signature; added step 2a with an explicit return path and explanation that this is a forensic finding, not a normal lookup miss; added prose distinguishing not-known (“grant does not exist”) from attribution-inconsistency (“grant exists, attribution missing — Invariant 1 violated”).
F2.5 — not-known and not-active from revoke_grant silently produce orphan attestations. The action signature showed not-known and not-active as simple caller-error codes with no indication of orphan side effects. A caller implementing retry logic against these codes would not know to check for orphan attestations. The inline step commentary covered the design but was invisible at the signature level. Closed: added an orphan side-effect preamble note to the revoke_grant action explaining the distinction between explicit orphan codes (orphan-attestation for composition-failure paths) and silent orphan side effects (not-known, not-active for caller-error paths), and alerting callers that each failed attempt on these paths leaves an orphan attestation in Actor Identity.
F2.6 — Generation acceptance missing Invariant 7 check. The five Audit-Trail-traversal-clearable checks covered Invariants 1–5 by reference but had no check for Invariant 7 (Attestation Exclusivity), which was added when the Alloy finding was closed. The check is structurally derivable from records alone (map enumeration and set intersection). The Alloy model was the finding mechanism; the Generation acceptance is the audit mechanism — both are required. Closed: added check 6 (Verify attestation exclusivity) enumerating both maps, confirming injectivity of each, confirming disjointness of their ranges, and naming the classes of violation each failure indicates.
F2.7 — Application state map lifetime claim inconsistent with Invariant 6 under retention purge. Application state said “as long as a grant exists in the Permissions store, its attribution record exists in the corresponding map” — implying the map entry’s lifetime is bounded by the grant’s lifetime. But Invariant 6 forbids the composition from deleting map entries. If a Retention Window composing pattern purges a grant from Permissions, the map entry persists (per Invariant 6) even though the grant is gone, violating the lifetime claim. One of them must give. Closed: qualified the Application state lifetime claim (“while a grant is retained”) with a forward reference to the Retention edge case; updated the Retention edge case to state explicitly that a Retention Window composing pattern must scope its purge to include grant_attribution, revocation_attribution, and the orphan log entries for purged grants — and that Invariant 6 forbids the composition from doing this on its own; only the retention pattern’s coordinated purge can.

Pass 1 — Structural completeness (GRID), Round 3. Complete. One finding; closed in-pattern.

F3.5 — Stale “Generation acceptance check 6” references after Round 2 F2.6 renumbering. Round 2’s F2.6 added check 6 (Verify attestation exclusivity) at the end of the Audit-Trail-traversal-clearable list. The orphan-attestations check had been check 5 since Round 1’s F3.8 first added it, but three body references and one Lineage reference still pointed at the orphan check as “check 6”: Application state’s orphan log paragraph, the revocation_proposal_format namespace-prefix justification, the revoke_grant orphan side-effect note, and Lineage F2.2’s Closed clause. After F2.6 was applied, all four references silently re-targeted attestation-exclusivity — the wrong check. Closed: updated all four “check 6” references to “check 5”; annotated Lineage F2.2’s entry with a parenthetical noting the corrected number and the F2.6 cause of the drift, so the historical record remains traceable. (Class of finding: post-renumbering reference-integrity. Inherited convention from the pressure-testing methodology: when a numbered checklist gains an entry, sweep the body for stale references in the same pass.)

Pass 2 — Conceptual independence (EOS), Round 3. Complete. No findings. The newly-promoted Invariant 8 (orphan log durability), the formal Caller contract paragraph, the dynamic-trace formal model, and the symmetric Invariant 2 conditional-failure surface are all properly scoped to this composition. Orphan log durability is a property of the composition’s emergent state — not a standalone concept that recurs across domains. The Caller contract is a contract-surface, not a concept. The dynamic-trace model is a formal-methods artifact tracking this composition’s own temporal claims, not a freestanding concept. No concept embedded here requires extraction as a separate atom.

Pass 3 — Adversarial scrutiny (Linus mode), Round 3. Complete. Four findings; all closed in-pattern.

F3.1 — verify_grant_attribution step 4 missing Invariant 2 conditional-failure path; Invariant 2 unconditional; Cross-store edge case names only Invariant 1. Round 2’s F2.4 closed the issuance side of this finding: added attribution-inconsistency as a result tag, step 2a as the failure-branch return, and prose distinguishing it from not-known. The revocation side was missed. revoke_grant step 5’s pairing write can fail after Permissions.revoke commits, producing a Revoked grant with no revocation_attribution entry — symmetric to the Invariant 1 case and reachable for identical reasons. Step 4 asserted Invariant 2 guarantees the lookup but had no path for the reachable failure state, the action was undefined when Invariant 2’s conditional broke, and Invariant 2’s statement carried no conditional qualifier matching Invariant 1’s. The Cross-store consistency edge case named only the Invariant 1 worst case. Closed: split step 4 (lookup only) from step 5 (renamed; verify call) and renumbered the original step 5 to step 6; inserted step 4a with the explicit return path, the forensic-finding obligation, and a forward reference to the new Caller contract paragraph; added the conditional qualifier to Invariant 2 mirroring Invariant 1’s language and pointing to the same Cross-store consistency edge case; updated Cross-store consistency under failure to name both worst cases (Invariant 1 for grant pairing, Invariant 2 for revocation pairing) and to cite step 2a and step 4a as the structural surfaces that report each; updated the Summary line for Invariant 2 to carry the conditional qualifier.
F3.2 — Orphan log durability declared in Application state prose but not promoted to a named invariant. Application state said the orphan log “is never modified after a write” — the same load-bearing append-only property Invariant 6 promotes for grant_attribution and revocation_attribution. Invariant 6 covers the two attribution maps but not the orphan log; the orphan log’s append-only nature was prose-only, with no named invariant to violate. An implementation that mutates orphan log entries — to scrub failure reasons, compress duplicates, or rewrite evidence — silently violates the spec’s evidence-preservation contract. Generation acceptance check 5’s structural orphan detection is independent of the orphan log, but the log itself is the operational-retry surface and its append-only durability is load-bearing for any retrospective recovery work. Closed: added Invariant 8 — Orphan log durability — naming the four write sites (issue_grant steps 4 and 5, revoke_grant steps 4 and 5), framing it as the composition-level analog of Invariant 6 applied to the orphan log surface, noting the same Retention-Window-purge conditional that scopes Invariants 1, 2, and 6, and naming the same tamper surface and Tamper Evidence composing-pattern remedy as Invariant 6. Updated Application state orphan log paragraph to point at Invariant 8. Updated Summary to “eight emergent invariants” and added the eighth bullet. Dynamic Alloy trace model (F3.4 closure) verifies orphan-log durability as a temporal property.
F3.3 — Caller contract for verify_grant_attribution’s forensic-finding result codes scattered across inline parentheticals, not formalized. The action returns three structurally distinct forensic findings — attribution-inconsistency from steps 2a and 4a, not-known from ActorIdentity.verify at step 3 (issuance) and step 5 (revocation), and failed-verification(reason). F2.4 added the first result tag without the matching caller contract; the caller’s normative obligations (log the finding, do not retry as a normal operation, do not coerce to not-known, surface to the forensic process) were scattered across step prose. A caller implementing against the action wiring had no single place to read the contract and could plausibly conflate forensic findings with normal misses. Closed: added a formal Caller contract — forensic-finding result codes paragraph at the end of verify_grant_attribution’s step list, enumerating the three forensic-finding outcomes with their distinct caller obligations (MUST log naming invariant and grant_id; MUST NOT retry against the same grant_id as a normal retry; MUST NOT coerce to not-known; MUST surface to the forensic process), and contrasting them with step 1’s not-known which is the only outcome that may be handled as a normal lookup miss.
F3.4 — Static Alloy model does not cover the spec’s temporal claims; dynamic-trace-model deferral repeated from Round 1 and Round 2 has no stronger reason to continue. The .als header explicitly named the gap and Round 1 / Round 2 Lineage both deferred a dynamic trace model. The spec makes load-bearing temporal claims the static model cannot verify: attest-before-record ordering, Invariants 1 / 2 / 6 / 8 holding in every reachable state (not just in valid snapshots), revocation terminality. The static checks coincidentally pass on snapshots; they prove nothing about transitions. Closed: implemented a dynamic trace model in the existing attributed-permissions-admin.als file as an appended Round 3 section. Uses Alloy 6’s var keyword on a fresh set of sigs (DynGrant, DynAttestation, DynSystem) to keep the dynamic model isolated from the static model above. Defines dyn_init (initial empty state), dyn_stutter (no-op), dyn_issue_grant (atomic add-attestation-add-grant-write-pairing), and dyn_revoke_grant (atomic add-revocation-attestation-flip-status-write-revocation-pairing). The trace fact pins the initial state and constrains every transition to one of these. Five LTL assertions verify the temporal properties: Dyn_Invariant_1_Always (Invariant 1 holds in every reachable state), Dyn_Invariant_2_Always (Invariant 2 holds over Revoked grants in every reachable state), Dyn_Pairing_Durability (Invariant 6 dynamically — entries persist after their first write), Dyn_Revocation_Terminal (revocation is terminal — no Revoked → Active), and Dyn_Attest_Before_Record (no transition records a grant or revocation without simultaneously writing the pairing). One run predicate exercises a trace producing a Revoked grant. Orphan-log durability and failure-path orphan creation are intentionally not modeled — the happy-path transitions are sufficient to discharge the load-bearing temporal claims, and adding failure transitions is the natural Final Critique 4 extension if evidence accumulates. The .als header was updated to “Status: Round 3 — static + dynamic” and the original “DEFERRED: Dynamic model (Round 2)” trailer was replaced with the closing rationale for the chosen scope.

Formal model — Round 3 dynamic trace model. compositions/attributed-permissions-admin.als (appended section) — Alloy 6 LTL extension covering the spec’s temporal claims. The static section above remains intact for Round 1 / Round 2 compatibility; the dynamic section uses fresh Dyn* sig names so the two coexist in one file without interference. The five LTL assertions named under F3.4 pass clean under typical scopes (for 4 but 1..6 steps); the run predicate (dyn_trace_with_revoked) demonstrates that a satisfying trace producing a Revoked grant is reachable from dyn_init. The deferral chain (Round 1 → Round 2 → Round 3) closes here for the snapshot-level claims and the four genuinely-distinct temporal claims; Final Critique 4 closes the under-defended orphan-log-durability deferral and the comment-accuracy gap on Dyn_Attest_Before_Record — see Final Critique 4 below. Failure-path orphan creation transitions (modeling rejection branches that populate the orphan log nontrivially) remain a natural later extension if a failure-case evidence requirement arises.

Pass 1 — Structural completeness (GRID), Final Critique 4. Complete. No findings. Step renumbering from Round 3 propagated correctly; cross-references hold (verify_grant_attribution step 5 — the revocation verify call — and step 6 — the return — are consistently referenced from the Caller contract paragraph and from Invariant 2’s body; no other site references the old step 4-as-lookup-and-verify form). Counts in Summary, Status, Composition-level invariants, edge cases, and Generation acceptance reconcile after Round 3’s additions.

Pass 2 — Conceptual independence (EOS), Final Critique 4. Complete. No findings. The Round 3 additions (Invariant 8, the formal Caller contract paragraph, the dynamic Alloy trace model) and the Final Critique 4 additions (orphan-log durability in the dynamic model) remain properly scoped to this composition. No concept embedded here requires extraction as a separate atom.

Pass 3 — Adversarial scrutiny (Linus mode), Final Critique 4. Complete. Two findings; both closed in-pattern.

F4.1 — .als comment for Dyn_Attest_Before_Record inaccurately claims it is “exactly Dyn_Invariant_1_Always above, restated by construction.” The two assertions check distinct properties. Dyn_Invariant_1_Always asserts one DynSystem.dyn_grant_attribution[g] — a pairing exists in the map relation. Dyn_Attest_Before_Record asserts DynSystem.dyn_grant_attribution[g] in DynSystem.dyn_attestations_in_store — the pairing target is currently stored. The latter is strictly stronger: it rules out states where the pairing references an attestation that isn’t in (or has been removed from) the Actor Identity store. Both hold on the current transition set only because no transition removes from dyn_attestations_in_store; absent that monotonicity (which Actor Identity’s Invariant 9 forbids but which an adversarial deletion could violate), the two assertions diverge. The comment misleads a reader who would otherwise question whether the assertion is doing real work, and it sets up confusion when a future round considers whether to keep the assertion. Closed: rewrote the comment block before Dyn_Attest_Before_Record to accurately distinguish the two assertions, explain that the assertion captures the consequence of attest-before-record ordering (the pairing’s target must be currently stored), name the implicit reliance on Actor Identity’s monotonicity-of-attestations-in-store discipline, and replace the “exactly restated by construction” phrasing with the strictly-stronger framing.
F4.2 — Invariant 8 added in Round 3 but not covered by the Round 3 dynamic Alloy model; deferral under-defended. F3.4’s closing note said orphan-log durability is “intentionally not modeled — happy-path transitions are sufficient to discharge the load-bearing temporal claims.” But Invariant 8 is itself a load-bearing temporal claim newly added in Round 3, and it is structurally identical to pairing-map durability (which the dynamic model does verify via Dyn_Pairing_Durability). The deferral conflated two separable concerns: orphan-log durability (verifiable on happy-path traces as a vacuously-true-but-structurally-meaningful assertion, the same way Dyn_Pairing_Durability is structurally meaningful on traces where no entries are added) and failure-path orphan creation (which legitimately requires modeling rejection branches and remains a later extension). The Round 3 model deferred both; only the latter needed to be deferred. Closed: extended DynSystem with var dyn_orphan_log : set DynAttestation; updated dyn_init (empty), dyn_stutter (preserve), dyn_issue_grant (preserve — happy paths produce no orphans), and dyn_revoke_grant (preserve) to keep the field consistent across transitions; added Dyn_Orphan_Log_Durability as a sixth LTL assertion (entries, once written, persist over time); added an explicit comment noting that on the current happy-path-only trace fact the assertion is vacuously satisfied (the log is always empty), and that the assertion structure encodes the durability discipline so adding failure-path transitions later does not require rewriting the durability contract. Updated the dynamic-model section header’s temporal-claims list to include T6 (Invariant 8 over time). Updated the section’s prologue comment to acknowledge the F4.2 closure and to scope the remaining deferral narrowly to failure-path orphan creation.

Formal model — Final Critique 4 dynamic trace model extension. compositions/attributed-permissions-admin.als (ROUND 3 DYNAMIC TRACE MODEL section, extended). Adds var dyn_orphan_log : set DynAttestation to DynSystem; updates dyn_init, dyn_stutter, dyn_issue_grant, and dyn_revoke_grant to keep the field consistent; adds Dyn_Orphan_Log_Durability as the sixth LTL assertion. Rewrites the Dyn_Attest_Before_Record comment block to accurately distinguish that assertion from Dyn_Invariant_1_Always (F4.1 closure). All six LTL assertions pass clean under the same for 4 but 1..6 steps scope. The remaining deferral — failure-path orphan creation transitions — is narrowed and explicitly scoped to a possible later round if a failure-case evidence requirement arises.

Formal model — TLA+ operational peer (precipitating touch for Round 5; artifact added before this Lineage entry was written). compositions/attributedPermissionsAdmin.tla (+ attributedPermissionsAdmin.cfg). Added 2026-05-20 as a peer artifact to the static + dynamic Alloy model; its addition constituted an edit to a grounded pattern and, per PRESSURE_TESTING.md §Touch triggers re-pass, triggered the full three-pass Round 5 recorded below. Models the operational state machine implied by §Action wiring (IssueGrant, RevokeGrant — atomic at the action grain, stamping attestation + grant/status + pairing-map write at the same logical-clock tick) and checks the eight named application-level invariants under TLC’s exhaustive-interleaving semantics. Bounds: Actors = {a1, a2}, GrantIds = {g1, g2}, AttIds = {t1, t2, t3}, MaxClock = 4, single (subject_ref, action_scope) = (s, x) pair. Result: all eight invariants hold across 397 reachable states. Single-active-per-pair is deliberately not checked — the spec’s §Edge cases → “Concurrent issuance of the same grant” explicitly allows two concurrent issuers to produce two grants and two attestations for the same pair, both fully attributed; the model accepts and exercises that scenario. Scope exclusions mirror the Final Critique 4 dynamic-Alloy scope decision: failure-path orphan-creation transitions deferred; permitted and verify_grant_attribution out of scope as pure reads; single logical clock (cross-system clock skew belongs to deployments composing with RFC 3161 Trusted Timestamping). The Alloy and TLA+ artifacts are siblings: Alloy proves snapshot facts and runs LTL assertions over short bounded traces; TLC enumerates every reachable interleaving of the spec’s actions at the bounds. Either can be re-run against changes to the spec; together they discharge the same eight named invariants through two independent mechanical checks.

Pass 1 — Structural completeness (GRID), Round 5 (touch-triggered re-pass, 2026-05-20). Complete. No new structural findings. All nine GRID nodes resolved. Regulated overlay complete (Regulated adversarial scenarios: three classes; Generation acceptance: Audit-Trail-traversal-clearable and Externally-clearable split present). Formal model Lineage entries carry plain-English summaries, artifact locations, bounds, scope exclusions, and results per CONTRIBUTING.md §Formal-model artifacts. Constituent atoms spot-checked: Permissions holds ten invariants (Invariant 5 count correct); Actor Identity holds nine invariants (Invariant 5 count correct). Permissions’ grant validation language (“at least one non-whitespace character”) is consistent with the composition’s Primitive policies (“non-empty; whitespace-trimmed at the composition layer” — all-whitespace inputs are rejected after trimming, which is the same bar). Actor Identity’s rejection-path examples added 2026-05-20 do not change its API; no composition cross-references affected.

Pass 2 — Conceptual independence (EOS), Round 5. Complete. No findings. All concerns confirmed correctly scoped to this composition or explicitly externalized. No concept embedded here requires extraction as a separate atom.

Pass 3 — Adversarial scrutiny (Linus mode), Round 5. Complete. Four findings; all closed in-pattern.

R5-F1 — TLA+ Lineage entry “not a new round” framing — refining → closed. The prior Lineage entry for the TLA+ model said “Additive sibling to the static + dynamic Alloy model, not a new round.” This directly contradicts PRESSURE_TESTING.md §Touch triggers re-pass: any edit to a grounded pattern requires a full three-pass round before grounded may be restored, regardless of how incremental the edit is. A reader scanning the Lineage notes would see the “not a new round” claim and have no way to reconcile it with the partially resolved status or with the methodology they are expected to follow. Closed: reframed the TLA+ entry header and opening sentence to state that the artifact’s addition constituted an edit to a grounded pattern that triggered Round 5, per the methodology.
R5-F2 — Status-line dense opening clause — refining → closed. The Status line before this round opened with a single extended clause referencing Round 5’s scope items inline (the demos/ copy, the “two refining wording tightenings,” the self-referential dense-clause note), making the Status harder to read than necessary. Closed: rewrote the Status to the grounded on Final Critique 5 — 2026-05-20 form, moved the round summary to the end of the content description where it follows the established pattern, and removed references to now-resolved scope items.
R5-F3 — Article error in revoke_grant step 3 — refining → closed. “so a invalid-request response” — the article “a” before a word beginning with a vowel sound should be “an.” Closed: corrected to “so an invalid-request response.”
R5-F4 — Redundant parenthetical in Final Critique 4 round summary — refining → closed. “Final Critique 4 (= Final Critique 4) complete” — the parenthetical restated the round name it was immediately following and added no information. Closed: removed the parenthetical.
demos/ stale Alloy copy — already resolved. The demos/ directory was deleted as part of a 2026-05-20 repo hygiene pass before this round ran; no in-pattern action required.

Formal model re-verification — TLC CLI re-run (precipitating touch for Round 6). compositions/attributedPermissionsAdmin.tla (+ attributedPermissionsAdmin.cfg). Re-run 2026-05-23 after the cross-cutting rename of all four .tla files in compositions/ from kebab-case to lower-camelCase to satisfy SANY’s filename↔module-name rule — recorded in DISCOVERIES.md §2026-05-23. The rename is an effective touch under PRESSURE_TESTING.md §Touch triggers re-pass and triggered Round 6. The .cfg required one addition to become CLI-runnable: NULL = NullMV in the CONSTANTS block, which overrides the NULL == "_none_" operator with an opaque model value. TLC 2.19 enforces strict-equality type checking and refuses to compare a string (the "_none_" sentinel) with a record value; assigning NULL to the model value NullMV makes every x /= NULL comparison type-homogeneous from TLC’s perspective. Bounds and scope unchanged from the Round 5 run: Actors = {a1, a2}, GrantIds = {g1, g2}, AttIds = {t1, t2, t3}, MaxClock = 4, single (s, x) pair. Result: all nine invariants (TypeOK + eight named emergent) hold across 397 reachable distinct states — identical to the Round 5 claim. The NULL = NullMV assignment in the CONSTANTS block is not a spec change; it is a tool-compatibility directive that leaves the NULL == "_none_" definition in the .tla unchanged and affects only how TLC evaluates equality comparisons during model checking.

Pass 1 — Structural completeness (GRID), Round 6 (touch-triggered re-pass, 2026-05-23). Complete. No findings. All nine GRID nodes still resolved. The .cfg addition (NULL = NullMV) is a tool-compatibility directive; no body cross-references affected. State counts in Summary, Status, and Composition-level invariants unchanged.

Pass 2 — Conceptual independence (EOS), Round 6. Complete. No findings. The NULL = NullMV override introduces no new concept. The formal model’s state variables and invariants remain correctly scoped to this composition; no concept embedded here requires extraction as a separate atom.

Pass 3 — Adversarial scrutiny (Linus mode), Round 6. Complete. No findings. TLC’s exhaustive enumeration of 397 reachable distinct states produced no counterexample to any of the nine invariants. The state count matches the Round 5 claim exactly, confirming the rename did not alter the model’s reachable state space. The .cfg NULL = NullMV fix resolves the TLC 2.19 CLI-runability gap; the model is now reproducible from a fresh checkout: java -cp tla2tools.jar tlc2.TLC -config attributedPermissionsAdmin.cfg -workers 4 attributedPermissionsAdmin.tla. No spec finding surfaced.

Round 6 closed clean. Foundational findings: zero. Refining findings: zero. Attributed Permissions Admin moves from grounded on Final Critique 5 to grounded on Final Critique 6.