Capability-Backed Sharing

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

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

Table of contents

Capability-Backed Sharing

Summary

Capability-Backed Sharing is a regulated composition — a specification that wires several freestanding patterns together — that solves a problem that looks impossible at first: how to share data using a “bearer token” (a link or token where simply holding it grants access, no login required) while still keeping the strict disclosure records that privacy laws demand. The apparent contradiction is that bearer tokens deliberately don’t check who’s using them, but regulators want to know who’s accountable for every disclosure.

This composition’s insight is that the accountable party isn’t the person who used the token — it’s the person who issued it. So it records, permanently and with a cryptographic signature, who authorized the share (the allocator), to whom they authorized it, what data, under what legal authority, and for how long — captured at the moment of issuance when that person is present to sign for it. When the token is later redeemed, the disclosure is logged against that authorizer, and the person who actually presented the token is — by design — never named, because the bearer model never asked.

The composition’s defining emergent guarantee is exactly this audit-subject asymmetry: the record always answers “who authorized this disclosure?” and never answers “who redeemed it?”. Its second guarantee, borrowed from the immutable-ledger pattern it mirrors, is that the disclosure record and its sealed audit event are written together or not at all, so there is never a disclosure without its tamper-evident proof.

Its common uses are exactly the places bearer sharing and regulated audit collide: a hospital sharing a scoped slice of a patient record with a referred specialist via a time-limited link (the minimum-necessary fields, logged against the authorizing clinician), a bank issuing a pre-signed link to disclose a customer’s transaction subset to an auditor, or a controller sharing specific personal-data fields with a processor under a consent record. Any system that must share data by token and prove from the records who authorized each disclosure — without being able to (or wanting to) name who consumed it — is a candidate for this composition.

Intent

Two correct designs appear to contradict each other, and reconciling them is the friction this composition exists to resolve. The object-capability (OCAP — a security model in which an unforgeable reference to a resource carries its own authority) model says: a bearer token is the authorization; whoever holds it may act, and asking who is holding it defeats the purpose — a password-reset link, a pre-signed download URL, a scoped API (Application Programming Interface) token all work precisely because no per-redemption identity check happens. The regulated-disclosure model says the opposite: every disclosure of a data subject’s information must be accountable — a regulator asking “who authorized this disclosure, and under what authority?” must get a structural answer from the records alone. A naive reading concludes you cannot have both: either you check identity at the point of access (and lose bearer semantics) or you don’t (and lose accountability). This composition shows the reading is wrong, and naming why is the composition’s contribution.

The resolution is an asymmetry of audit subjects. Accountability does not require naming the redeemer; it requires naming the authorizing party — and those are two different actors at two different moments. The authorizing party is the allocator: the data controller (or their delegate) who decided that a specific subset of a subject’s data may be shared, with a named intended recipient, under a named legal authority, for a bounded number of redemptions, for a bounded time. That decision happens at allocation, when the allocator is present and can be cryptographically attested under their own credential. The redeemer is whoever later presents the token — and by the bearer-token design, their identity is neither checked nor recorded. This composition’s audit record therefore reads “disclosed under authority of allocator X, who authorized this share at time T,” never “redeemed by Z.” The allocator is fully accountable (Capability records the allocator immutably and only the allocator — Capability Invariants 1 and 5; this composition additionally attests the allocator at allocation); the redeemer is structurally unnamed (Capability performs no identity check at redemption — Capability Invariant 3). Regulated audit is satisfied by the allocator’s accountability; bearer semantics are preserved by the redeemer’s anonymity. Neither model is broken.

This reframe carries a precise consequence for what the disclosure record names as recipient. The bearer who actually presents the token is unknowable by design; what the record names is the intended recipient the allocator declared at allocation time. The disclosure was authorized to go to recipient R; whether the actual bearer was R, R’s delegate, or a party who obtained the token improperly is exactly the question bearer semantics make unanswerable — and the records are honest about that boundary (it is the forensic limit Capability’s own disputed-disclosure scenario names). The composition records who authorized the disclosure and to whom it was authorized, not who consumed it.

No single constituent resolves this. Capability is the bearer-token primitive — it records the allocator, authorizes by possession, and refuses to record a redeemer — but it does not record that a disclosure occurred, does not carry the legal authority for the disclosure, and is not tamper-evident. Selective Disclosure is the disclosure-accounting record — to whom, what scope, under what authority, when — but it does not gate access, does not carry a redemption envelope (how many times, until when), and its append-only immutability is by specification, not cryptographically sealed. Audit Trail is the tamper-evident, attributed, retained substrate — but it knows nothing about bearer tokens or disclosure scope. The structure that allocates a bearer token whose scope is an authorized disclosure, performs the disclosure on redemption, records it accountably to the allocator while naming no redeemer, and seals the whole thing belongs to no single constituent. It belongs to the composition, and this composition is that structure.

This is a composition, not a new primitive. Capability, Selective Disclosure, and Audit Trail are unchanged; this composition is the wiring that makes them coherent as one accountable-bearer-sharing surface. It introduces emergent actions — Authorize Sharing (allocate the capability and attest the allocator’s authorization), Redeem And Disclose (the load-bearing surface: redeem by possession, then record the disclosure and seal it), Revoke Sharing, and read-only queries — that belong to no single constituent. What it is not: it is not an identity-keyed access control surface (that is Permissions — this composition is bearer-keyed by design); it is not the disclosure-delivery mechanism (it records that and to whom authorized a disclosure occurred; retrieving, redacting, and transmitting the bytes is the host’s job, exactly as Selective Disclosure records without performing); it is not the adjudicator of whether the declared authority is legally valid (that legitimacy is an externally-clearable check, as in Selective Disclosure and Resolve a Person’s Data Rights); and it does not — cannot — identify the redeemer (the bearer-key design forecloses it). Each is named in Edge cases.

Composes

Capability — the bearer-token primitive and the source of the audit asymmetry. Authorize Sharing calls Capability.allocate(allocator_ref, scope, max_redemptions, ttl) → capability_token | rejected(invalid-request | storage-failure), encoding the sharing descriptor (subject, intended recipient, disclosed scope, authority) as the opaque scope value — Capability treats scope as a black box and this composition is the pattern that defines and interprets it (Capability’s Composition notes name this composition as that pattern). Redeem And Disclose calls Capability.redeem(capability_token) → redeemed(scope, allocator_ref) | invalid(exhausted | expired | revoked | not-known) — note redeem takes no identity argument and returns the allocator_ref, which is exactly the asymmetry this composition turns into accountability: the redemption surfaces who authorized the capability (the allocator, immutable per Capability Invariant 1) and structurally cannot surface who redeemed it (Capability Invariant 3 — bearer redemption; Invariant 5 — audit asymmetry). Revoke Sharing calls Capability.revoke(capability_token, revoked_by_ref, reason). The capability’s redemption envelope (max_redemptions, expires_at) bounds how many disclosures and for how long — a surface Selective Disclosure does not carry.
Selective Disclosure — the disclosure-accounting record. Redeem And Disclose calls SelectiveDisclosure.record(subject_ref, recipient, scope, authority, disclosed_at?) → recorded(disclosure_id) | rejected(invalid-request | unknown-authority-type | storage-failure) with recipient = the allocator-declared intended recipient (not the unknowable bearer — see Intent and the Recipient is the allocator-declared intended recipient edge case), scope = the disclosed field subset, and authority = the {type, reference} the allocator embedded in the capability scope (type ∈ {consent, legal-hold, regulatory}). This composition structurally closes Selective Disclosure’s Invariant 5 (no-disclosure-unrecorded) for capability-backed disclosures by making Redeem And Disclose the only disclosure surface and having it always record — exactly as Immutable Transaction Ledger closes Invariant 5 by making disclose_subset the sole disclosure surface. The composition also calls SelectiveDisclosure.read for the read-only sharing-history queries.
Audit Trail — the regulated-audit substrate: this composition names it the way an atom is named and reaches Event Log, Actor Identity, Tamper Evidence, and Retention Window transitively through it (per the Compositions of compositions convention — see spec-format.md), maintaining one Audit Trail instance for all sharing events. This composition records its events by calling AuditTrail.record_action(action_ref, actor_ref, credential, data) → event_id | rejected(invalid-credential | invalid-request | recording-failure) directly on the one Audit Trail instance the substrate carries — the established substrate-composition pattern (Multi-Party Approval, Immutable Transaction Ledger, and Resolve a Person’s Data Rights record their own events on the Audit Trail their substrate carries). The capability is Audit Trail’s own declared record_action and its Invariant 1 (attribution coverage), reached through the named substrate — not an ambient reach-through. Two event kinds carry the asymmetry: Sharing Authorized, recorded at Authorize Sharing and attested under the allocator’s own credential (the allocator is present and accountable), names the allocator non-repudiably; Sharing Disclosed, recorded at each Redeem And Disclose, is attested under the composition’s service identity (the allocator is not present at redemption; the bearer has no credential) and carries the allocator_ref and capability_token in its data while carrying no redeemer identity. The substrate seals both (Tamper Evidence) and governs their retention (Retention Window) so the accountability outlives the disclosure.

The Capability store, the Selective Disclosure store, and the substrate’s stores (Event Log, Actor Identity, Tamper Evidence, Retention Window) are owned by their respective constituent instances. This composition owns no constituent state — it indexes across them with its own emergent maps (capability_to_sharing, disclosure_to_redemption, below) and binds each disclosure to its sealed event.

A surface this composition needs that no constituent provides is the interpretation of a capability’s opaque scope as a structured sharing descriptor (subject, intended recipient, disclosed scope, authority). Capability stores scope opaquely; Selective Disclosure stores its own scope/recipient/authority opaquely; neither parses a capability scope into a disclosure. This is a composition-introduced surface at this composition’s layer (one of the four legitimate capability-provenance sources — see pressure-testing.md §Capability provenance), governed by the deployment-declared sharing_scope_grammar (Configuration).

Composition logic

Composition state

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

capability_to_sharing — map from capability_token to {allocator_ref, subject_ref, recipient, disclosed_scope, authority, authorization_event_id, allocated_at}. Populated by Authorize Sharing after Capability.allocate and the Sharing Authorized attestation both succeed; immutable thereafter. This is the authorization-provenance index: it records who authorized the share, to whom and what it authorizes, under what authority, and binds it to the Sharing Authorized Audit Trail event attested under the allocator’s credential. It is the records-alone source for “who authorized this disclosure?” (Invariant 1) and the authorization half of the asymmetry.
disclosure_to_redemption — map from disclosure_id (a Selective Disclosure record) to {capability_token, allocator_ref, sharing_disclosed_event_id, disclosed_at}. Populated by a successful Redeem And Disclose only after all constituent writes succeed (the binding — Invariant 2). It binds each disclosure to the capability that authorized it and to the sealed Sharing Disclosed event; it carries the allocator_ref (the authorizing party) and, by construction, no redeemer field — there is nowhere in this map, or in any this composition state, to put a redeemer identity (Invariant 1). disclosure_to_redemption is the queryable mirror of the authoritative sealed Sharing Disclosed event, not an independent store an edit could silently diverge from.

The Capability store (capability records, including the immutable allocator_ref and the remaining_redemptions counter), the Selective Disclosure store (disclosure records), and the substrate’s stores are owned by their constituent instances. This composition duplicates none of them.

Configuration

sharing_scope_grammar — the deployment-declared grammar by which a capability’s opaque scope value encodes the structured sharing descriptor: the subject_ref, the intended recipient, the disclosed scope (the field subset to be shared — the minimum-necessary set under HIPAA §164.514(d)), and the authority {type ∈ {consent, legal-hold, regulatory}, reference}. This is the declaring source (capability provenance) for the composition-introduced scope-interpretation surface: every field this composition passes to SelectiveDisclosure.record traces to this declared grammar applied to the capability scope, not to an ambient “the system knows what the scope means.” A capability whose scope does not parse under the grammar is rejected at Authorize Sharing (invalid-sharing-descriptor).
application_actor_ref and application_credential — the composition’s service identity, used to attest the Sharing Disclosed Audit Trail event at redemption time, when the allocator is absent and the bearer has no credential. This is the same service-identity discipline Login and Multi-Party Approval use for system-originated events: the deployment provisions and rotates this credential; its compromise surface and forgery defense follow the same reasoning. The service identity records that this composition’s service performed the disclosure; the responsible authorizing actor is the allocator_ref carried in the event data and provable via the Sharing Authorized attestation — the redeemer is never named (Invariant 1).
audit_trail_retention_policy — inherited, not re-configured. this composition records its sharing.* events on the Audit Trail substrate, which carries the host’s regulatory retention policy; record_action takes the policy via the substrate’s configured value. The sharing audit events should persist at least as long as the longest retention obligation over the disclosed data — GDPR Article 30 / HIPAA §164.528(d)’s six-year accounting-of-disclosures horizon is the typical floor.
default_capability_ttl and default_max_redemptions — passed through to Capability.allocate when Authorize Sharing does not supply them (Capability requires a configured default TTL — time-to-live — and defaults max_redemptions to 1 / single-use).

Primitive policies

capability_token — opaque, cryptographically random bearer credential and the key of capability_to_sharing; produced by Capability.allocate, presented to Redeem And Disclose and Revoke Sharing. Byte-identity equality; never normalized. It is the bearer credential — the only thing required to redeem, and the composition records no identity alongside its presentation (Invariant 1).
allocator_ref — opaque reference to the authorizing actor; non-empty (invalid-request). Flows to Capability.allocate (recorded immutably), to the Sharing Authorized record_action as actor_ref (attested under the allocator’s credential), and into every disclosure’s data and the capability_to_sharing index. The one identity the composition records for a share.
credential — the allocator’s opaque credential at Authorize Sharing (consumed by the Sharing Authorized attestation, never persisted), and the revoker’s credential at Revoke Sharing. The composition never accepts, requests, or records a redeemer credential — Redeem And Disclose takes only the capability_token (Invariant 1).
subject_ref / recipient / disclosed_scope / authority — the sharing descriptor fields parsed from the capability scope per sharing_scope_grammar; passed to SelectiveDisclosure.record, which applies its own non-empty / authority-type validation. Recipient is the allocator-declared intended recipient, not the bearer (see Intent).
disclosed_at — optional; defaults to the substrate clock at record time (logic-confinement, inherited from the substrate). Best-effort wall-time; the Event Log sequence_number is the authoritative order source.

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

Action wiring

The composition exposes four actions: one allocation-with-attestation (Authorize Sharing), one emergent redeem-and-disclose (Redeem And Disclose, the load-bearing surface), one revocation (Revoke Sharing), and read-only queries.

Uniform record_action rejection-mapping. For every AuditTrail.record_action call below, the substrate’s taxonomy (invalid-credential | invalid-request | recording-failure) maps as named per step. Where the audit write is part of an atomic binding (the disclosure path), a substrate failure aborts the whole binding (no partial state) under the host transaction boundary; the cross-store-consistency edge case governs deployments whose stores cannot co-transact.

`authorize_sharing`

authorize_sharing(allocator_ref, credential, sharing_descriptor, max_redemptions?, ttl?) →
  {capability_token, authorization_event_id}
 | rejected(
   invalid-request
  | invalid-sharing-descriptor
  | unknown-authority-type
  | recording-failure
  | storage-failure
  )

Allocates a bearer capability whose scope is an authorized disclosure, and records the allocator’s non-repudiable authorization. Steps:

Validate: allocator_ref, credential non-empty; max_redemptions (if supplied) a positive integer; ttl (if supplied) positive. Any violation → rejected(invalid-request). Stop.
Parse sharing_descriptor against sharing_scope_grammar into {subject_ref, recipient, disclosed_scope, authority}. A descriptor that does not parse, or with empty subject_ref/recipient/disclosed_scope/authority.reference → Invalid Sharing Descriptor. If authority.type ∉ {consent, legal-hold, regulatory} → rejected(unknown-authority-type) (the same authority bound Selective Disclosure enforces, checked at the composition boundary so a malformed share is refused before a capability is allocated). Stop.
Capability.allocate(allocator_ref, scope = <descriptor encoded per grammar>, max_redemptions ?? default_max_redemptions, ttl ?? default_capability_ttl) → capability_token. Map invalid-request → rejected(invalid-request), storage-failure → rejected(storage-failure). On rejection, nothing further is recorded.
AuditTrail.record_action(action_ref = sharing.authorized, actor_ref = allocator_ref, credential, data = {capability_token, subject_ref, recipient, disclosed_scope, authority, max_redemptions, expires_at, authorized_at = now}, retention_policy = audit_trail_retention_policy) → authorization_event_id — attested under the allocator’s own credential, the allocator’s non-repudiable commitment that they authorized this share (Invariant 3). Map invalid-credential / invalid-request → rejected(invalid-request) (a clean pre-disclosure rejection — the capability is allocated but unattached; surfaced as a finding per the Cross-store consistency edge case, mirroring an orphaned allocation), recording-failure → rejected(recording-failure).
Populate capability_to_sharing[capability_token] = {allocator_ref, subject_ref, recipient, disclosed_scope, authority, authorization_event_id, allocated_at = now}. Steps 3–5 commit together or not at all under the host transaction boundary (Invariant 3); where the Capability and Audit Trail stores cannot co-transact, the unattached-capability orphan is surfaced and recovered per the Cross-store consistency under partial failure edge case. Return {capability_token, authorization_event_id}. The allocator delivers the capability_token to the intended recipient out-of-band (email, link, API response) — the delivery channel is outside this composition’s scope, exactly as Capability’s token delivery is.

`redeem_and_disclose`

redeem_and_disclose(capability_token) →
  {disclosure_id, event_id, disclosed_scope, allocator_ref}
 | invalid(exhausted | expired | revoked | not-known)
 | rejected(not-authorized-sharing | recording-failure)

Redeems the capability by possession alone — no identity argument — then records the disclosure accountably to the allocator while naming no redeemer, sealing the disclosure and its audit event together. This is the composition’s load-bearing surface. Steps:

Capability.redeem(capability_token). On invalid(exhausted | expired | revoked | not-known) → return the same invalid(...) (first-class outcomes, not rejections — the bearer presented a token that is spent, lapsed, cancelled, or unknown; nothing is disclosed or recorded). On redeemed(scope, allocator_ref) → proceed. No identity is accepted, requested, or recorded at this step — Redeem And Disclose takes exactly one argument, the capability_token (Invariant 1, inheriting Capability Invariant 3).
Resolve capability_to_sharing[capability_token] for the parsed {subject_ref, recipient, disclosed_scope, authority}. Absent → Not Authorized Sharing (the token is a valid Capability but was not allocated through this composition’s Authorize Sharing, so it carries no this composition sharing descriptor — a token from another Capability composition redeemed here; nothing is disclosed). The allocator_ref from step 1’s redeemed(...) must equal the indexed allocator_ref (a consistency check; a mismatch is a finding).
Commit atomically — the binding (Invariant 2), under the host transaction boundary: SelectiveDisclosure.record(subject_ref, recipient, scope = disclosed_scope, authority, disclosed_at = now) → disclosure_id; then AuditTrail.record_action(action_ref = sharing.disclosed, actor_ref = application_actor_ref, credential = application_credential, data = {disclosure_id, capability_token, allocator_ref, subject_ref, recipient, disclosed_scope, authority, authorization_event_id, disclosed_at = now}, retention_policy = audit_trail_retention_policy) → event_id — attested under the composition’s service identity; the data names the allocator_ref (the authorizing party) and carries no redeemer identity (Invariant 1); then populate disclosure_to_redemption[disclosure_id] = {capability_token, allocator_ref, sharing_disclosed_event_id = event_id, disclosed_at}. The redemption-decrement (step 1’s Capability.redeem), the Selective Disclosure record, and the Sharing Disclosed event commit together or not at all under the host transaction boundary — a substrate recording-failure or a Selective Disclosure storage-failure aborts the binding and the redemption-decrement rolls back with it (unlike Resolve a Person’s Data Rights’ irreversible purge, a redemption-decrement is a recoverable store write under the transaction, so the binding is atomic in the conforming case — closer to Immutable Transaction Ledger than Resolve a Person’s Data Rights). Map a failed disclosure or audit write → rejected(recording-failure); the orphan, where the stores cannot co-transact, is handled per the Cross-store consistency under partial failure edge case.
Return {disclosure_id, event_id, disclosed_scope, allocator_ref}. The host now assembles and transmits the actual data for the Disclosed Scope to the intended recipient — the disclosure delivery is the host’s obligation, signalled by the disclosure record; this composition recorded what was disclosed, to whom it was authorized, under what authority, and by whose authorization — never who consumed it.

`revoke_sharing`

revoke_sharing(capability_token, revoked_by_ref, credential, reason) →
  {revoked, event_id}
 | rejected(invalid-request | already-terminal | not-known | storage-failure | recording-failure)

Cancels a sharing capability before its redemptions or time are exhausted (the sharing window closes early; the data should no longer be shareable via this token). Steps: validate inputs (invalid-request); Capability.revoke(capability_token, revoked_by_ref, reason) mapping already-terminal / not-known / storage-failure through (the constituent’s full rejection taxonomy — storage-failure surfaced as storage-failure, mirroring Authorize Sharing’s allocate-failure mapping, so no constituent rejection drifts unmapped); then AuditTrail.record_action(action_ref = sharing.revoked, actor_ref = revoked_by_ref, credential, data = {capability_token, reason, revoked_at = now}, retention_policy = audit_trail_retention_policy) → event_id (attested under the revoker’s credential — a named, accountable act, like the allocator’s authorization). Return {revoked, event_id}. Future Redeem And Disclose calls for the token return invalid(revoked) and disclose nothing.

Read-only queries

sharing_disclosures(subject_ref) → list of disclosure records, each with its authorizing allocator
authorization_provenance(capability_token) → {allocator_ref, subject_ref, recipient, disclosed_scope, authority, authorization_event_id} | not-known

Sharing Disclosures passes through to SelectiveDisclosure.read({subject_ref}) and joins each disclosure to its disclosure_to_redemption entry, returning, per disclosure, the recorded recipient/scope/authority and the authorizing allocator_ref — never a redeemer (there is none to return). Authorization Provenance reads capability_to_sharing for who authorized a given share. Both are pure reads producing no Audit Trail event (logging who read the sharing history is handled as a composing access-log concept, named rather than absorbed, mirroring Immutable Transaction Ledger/Resolve a Person’s Data Rights).

The load-bearing wiring decision — accountability attaches to the allocator, not the redeemer; disclosure and its seal bind atomically

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

Half 1 — the audit subject is the allocator, never the redeemer. Every capability-backed disclosure is recorded accountably to the allocator who authorized it (attested under the allocator’s credential at allocation, carried immutably in the capability), and records no redeemer identity, because the bearer presents only the token.

Principle. Regulated disclosure requires a named, non-repudiable authorizing party, not a named consumer; bearer-token sharing requires the consumer be anonymous. Both are satisfied at once by attaching accountability to the allocator. Likely objection: doesn’t “accountable disclosure” mean you must record who received / accessed the data — and doesn’t recording only the allocator leave a hole? Mechanism that resolves it: no — the regulator’s question is “who authorized this disclosure, and under what authority?”, and that is the allocator and the authority, both recorded: the allocator at allocation under their own credential (Sharing Authorized, Invariant 3), the authority in the capability scope and the disclosure record (Selective Disclosure’s authority field), and the disclosure itself attributed to the allocator in the Sharing Disclosed event data. The redeemer’s identity is structurally unavailable — Capability’s redeem accepts no identity and records none (Capability Invariant 3), and Capability’s allocation/redemption asymmetry (Invariant 5) is the atom’s primary audit contribution — so this composition records what it can prove (who authorized, to whom authorized, what, under what authority) and is honest about what bearer semantics make unprovable (who actually presented the token). The recorded recipient is the intended recipient the allocator declared, not the bearer. Result: the disclosure is fully accountable to the allocator (regulated audit satisfied) and the redeemer is never named (bearer semantics preserved) — the asymmetry no constituent provides alone, resting on Capability Invariants 1/3/5 surfaced through redeem’s allocator_ref return and this composition’s allocation-time attestation.

Half 2 — the disclosure record and its sealed audit event bind atomically. Each redemption-that-discloses commits the Selective Disclosure record and the Sharing Disclosed Audit Trail event together or not at all.

Principle. An accountable disclosure must be inseparable from its tamper-evident proof: there must be no disclosure record without its sealed audit event, and no Sharing Disclosed event without its disclosure record. Likely objection: why not record the disclosure in Selective Disclosure and separately log it in the Audit Trail, letting each store its own copy? Mechanism that resolves it: because two independent writes admit a dangling partial — a disclosure record with no sealed event (unprovable against tampering) or a sealed event with no disclosure record (an accountability claim with no accounting record). This composition commits the redemption-decrement, the Selective Disclosure record, and the Sharing Disclosed event in one transaction (the binding bijection, mirroring Immutable Transaction Ledger’s disclose_subset), populating disclosure_to_redemption only after all land; a substrate or disclosure-store failure aborts the whole binding and the redemption-decrement rolls back with it. Result: every capability-backed disclosure is one immutable, attributed, tamper-evident, accountable act — the binding bijection no constituent provides alone, resting on Selective Disclosure’s record + Invariants 1/6 and Audit Trail’s record_action + Invariant 1 reached through the named substrate.

Composition-level invariants

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

Invariant 1 — Audit-subject asymmetry (load-bearing). For every capability-backed disclosure, the records name the allocator as the authorizing party — the Sharing Authorized event (attested under the allocator’s credential), the allocator_ref carried immutably in the capability and in the Sharing Disclosed event data and the capability_to_sharing / disclosure_to_redemption indices — and record no redeemer identity anywhere: not in the capability record (Capability Invariant 3/5), not in the disclosure record, not in the audit event, not in any this composition emergent state. The recorded recipient is the allocator-declared intended recipient, not the bearer who presented the token (which is structurally unknowable). This is the load-bearing emergent property; it is a structural / by-construction guarantee — there is nowhere in the spec graph to record a redeemer — verified by-construction at this composition’s layer and on Capability’s own surface by capability.als, whose modeled capability record carries no redeemer field and whose redeem transition takes no identity argument — the structural form of Capability Invariants 3 and 5 (enforced by construction, not by a named assertion). Rests on: Capability Invariant 1 (allocation-provenance immutability), Invariant 3 (bearer redemption — no identity at redeem), and Invariant 5 (audit asymmetry — allocator recorded, redeemer never), surfaced through Capability.redeem’s allocator_ref return; the composition-introduced allocation-time Sharing Authorized attestation under the allocator’s credential; and the composition-introduced state (capability_to_sharing, disclosure_to_redemption) which by construction carries an allocator_ref field and no redeemer field.
Invariant 2 — Disclosure-accountability binding bijection. Every capability-backed disclosure commits, together or not at all, exactly one Selective Disclosure record, one Sharing Disclosed Audit Trail event carrying its disclosure_id, and the disclosure_to_redemption binding; and every Sharing Disclosed event corresponds to exactly one Selective Disclosure record whose disclosure_id it carries — the binding is bijective. The redemption-decrement that precedes the binding (Capability’s counter) is part of the same host transaction and rolls back with the binding on failure, so — unlike Resolve a Person’s Data Rights’ irreversible purge — there is no dangling partial in the conforming case (the binding is atomic, mirroring Immutable Transaction Ledger’s disclosure-accountability bijection rather than Resolve a Person’s Data Rights’ modulo-clause). This is the formal-model subject; the TLA+ — Temporal Logic of Actions — model verifies the bijection and the buggy twin shows a non-atomic split reaches a dangling partial. Defended in-line: Redeem And Disclose step 3 commits the three writes in one transaction and populates disclosure_to_redemption only after all land. Rests on: Selective Disclosure’s record and Invariants 1 and 6 (record immutability; append-only durability), Audit Trail’s record_action and Invariant 1 (attribution coverage) reached through the named substrate, Capability’s redeem (the recoverable-under-transaction redemption-decrement), and the composition’s disclosure_to_redemption-population-after-all-writes discipline plus the host transaction boundary.
Invariant 3 — Allocation-authorization binding. Every capability allocated through this composition has exactly one Sharing Authorized Audit Trail event, attested under the allocator’s own credential, bound to the capability_token in capability_to_sharing; and every capability-backed disclosure (Sharing Disclosed) names a capability_token whose Sharing Authorized attestation is the records-alone proof that the named allocator authorized this share. In the conforming case — under the host transaction boundary — Authorize Sharing commits the Capability.allocate, the Sharing Authorized attestation, and the capability_to_sharing binding together or not at all (mirroring Invariant 2’s atomicity); the sole exception is the unattached-capability orphan (a) of Cross-store consistency under partial failure, possible only where the Capability and Audit Trail stores cannot co-transact, which Authorize Sharing surfaces as a rejected(...) finding for recovery (revoke the unattached capability, or retry the attestation) rather than leaving a silent partial. Defended in-line: Authorize Sharing commits steps 3–5 atomically under the host transaction boundary, recording the attestation under the allocator’s credential (step 4) before populating capability_to_sharing (step 5). Rests on: Audit Trail’s record_action + Invariant 1 (the attestation under the allocator’s credential, via the substrate’s Actor Identity), Capability’s Invariant 1 (the immutable allocator_ref), and the composition-introduced capability_to_sharing binding.
Invariant 4 — Scope-bounded disclosure. The scope of every Selective Disclosure record produced by Redeem And Disclose equals the disclosed_scope parsed from the capability’s authorized scope (per sharing_scope_grammar) — no disclosure exceeds, narrows arbitrarily, or diverges from what the allocator authorized; the capability’s immutable scope (Capability Invariant 8 — scope immutability) is the upper bound, and the redemption envelope (max_redemptions, expires_at) bounds how many disclosures and for how long. Defended in-line: Redeem And Disclose step 2 derives the disclosure descriptor solely from the capability’s scope via the grammar; it accepts no caller-supplied scope override. Rests on: Capability Invariant 8 (scope immutability) and the redemption envelope (max_redemptions/expires_at, Capability Invariants 2/10), and the deployment-declared sharing_scope_grammar configuration capability (the parse from capability scope to disclosure descriptor).
Invariant 5 — Constituent invariants preserved. All Capability invariants (1–12) hold over the capability store, all Selective Disclosure invariants (1–6) hold over the disclosure store, and all Audit Trail composition-level invariants (1–8) hold over the substrate (transitively all Event Log, Actor Identity, Tamper Evidence, and Retention Window invariants). This composition weakens no constituent invariant. Rests on: each constituent’s own Generation acceptance bar over its store instance.

Invariant 1 (audit-subject asymmetry) is the emergent property the composition exists to provide — the reconciliation of bearer semantics with regulated audit. Invariant 2 (binding bijection) makes each disclosure an inseparable, tamper-evident, accountable act; Invariant 3 (allocation-authorization binding) is what makes the allocator’s accountability non-repudiable; Invariant 4 (scope-bounded disclosure) holds the disclosure to what was authorized. Invariant 5 preserves every constituent guarantee underneath.

Examples

Walkthrough — a clinician shares a scoped patient record with a referred specialist, end to end

A hospital deploys this composition with sharing_scope_grammar encoding subject::recipient::fields::authority, the substrate’s audit_trail_retention_policy = hipaa_6_year, and a provisioned service identity.

Authorization. A treating clinician refers a patient to a specialist and authorizes a one-time, 24-hour share of the minimum-necessary fields: authorize_sharing(allocator_ref = "dr_chen", credential = <chen-cred>, sharing_descriptor = {subject: "patient-7842", recipient: "dr-okafor-cardiology", fields: "cardiology-summary", authority: {type: consent, reference: "consent-8821"}}, max_redemptions: 1, ttl: 86400). This composition parses the descriptor, Capability.allocate(...) returns capability_token = tok_share_x1, and AuditTrail.record_action(sharing.authorized, actor_ref = "dr_chen", <chen-cred>, data = {tok_share_x1, subject: patient-7842, recipient: dr-okafor-cardiology, fields: cardiology-summary, authority: consent/consent-8821, …}) → ev_auth_01 — attested under Dr. Chen’s credential (Invariant 3). capability_to_sharing[tok_share_x1] is populated. Returns {tok_share_x1, ev_auth_01}. The hospital emails the specialist a link embedding tok_share_x1.
Redemption and disclosure. The specialist’s system opens the link within the day: redeem_and_disclose(tok_share_x1) — no identity is presented. Capability.redeem(tok_share_x1) → redeemed(scope, allocator_ref = "dr_chen"); the capability exhausts (single-use → Redeemed). This composition commits atomically: SelectiveDisclosure.record(subject: "patient-7842", recipient: "dr-okafor-cardiology", scope: "cardiology-summary", authority: {consent, consent-8821}) → disc_01; AuditTrail.record_action(sharing.disclosed, actor_ref = <service identity>, data = {disc_01, tok_share_x1, allocator_ref: "dr_chen", subject: patient-7842, recipient: dr-okafor-cardiology, fields: cardiology-summary, authority: consent/consent-8821}) → ev_disc_01 — attributed to the service identity, naming Dr. Chen as the authorizing allocator, naming no redeemer; disclosure_to_redemption[disc_01] is populated. Returns {disc_01, ev_disc_01, "cardiology-summary", "dr_chen"}. The hospital then transmits the cardiology-summary fields to the specialist.
The audit answer. sharing_disclosures("patient-7842") returns disc_01: disclosed cardiology-summary to dr-okafor-cardiology, under consent consent-8821, authorized by dr_chen (Invariant 1). authorization_provenance(tok_share_x1) confirms Dr. Chen authorized it. There is no field anywhere recording who at the specialist’s office actually opened the link — by design.

Domain example — a multi-use pre-signed disclosure to an auditor

A bank authorizes a 10-redemption, 7-day capability for an external auditor to pull a customer’s transaction subset: authorize_sharing("compliance_officer_m", <cred>, {subject: "acct-0187", recipient: "audit-firm-AF3", fields: "transactions:2024", authority: {type: regulatory, reference: "SOX §404"}}, max_redemptions: 10, ttl: 604800). Over the week the auditor’s tooling redeems the token nine times from various systems; each Redeem And Disclose records a distinct Selective Disclosure record bound to its own sealed Sharing Disclosed event, every one attributed to compliance_officer_m as the allocator and none recording which of the auditor’s systems redeemed it. The remaining_redemptions counter (Capability) decrements 10→1; the regulated-audit record shows nine accountable disclosures under one authorization. The audit-subject asymmetry holds across every redemption.

Rejection path — spent, lapsed, cancelled, foreign, and unrecorded tokens

Exhausted / expired / revoked. A bearer redeems a single-use token a second time: redeem_and_disclose(tok_share_x1) → invalid(exhausted); nothing is disclosed or recorded (Capability returned invalid(exhausted) at step 1). A token presented after its TTL → invalid(expired); after Revoke Sharing → invalid(revoked). These are first-class outcomes, not rejections — the bearer presented a token that no longer authorizes a disclosure, and no disclosure record is created (the no-disclosure-unrecorded direction holds: no disclosure occurred, so none is recorded).
Foreign capability. A valid Capability token allocated by some other Capability composition (not this composition’s Authorize Sharing) is redeemed here: step 1 redeem may succeed, but step 2 finds no capability_to_sharing entry → rejected(not-authorized-sharing); nothing is disclosed. This composition discloses only what it authorized.
Early revocation closes the window. revoke_sharing(tok_share_x1, "compliance_officer_m", <cred>, "sharing-window-closed") records a sharing.revoked event under the revoker’s credential and transitions the capability to Revoked; subsequent redemptions return invalid(revoked).

Regulated adversarial scenarios

Three scenarios the composition must survive in regulated contexts.

Regulator audit — “who authorized this disclosure of subject DS-99’s data, and under what authority?” A GDPR (EU General Data Protection Regulation) Data Protection Authority examines a disclosure. sharing_disclosures("DS-99") returns the disclosure record with its authority ({type, reference}) and the authorizing allocator_ref; AuditTrail.verify_record on the bound Sharing Disclosed event confirms it was not altered (Invariant 2, resting on the substrate’s Tamper Evidence), and the Sharing Authorized event — attested under the allocator’s own credential (Invariant 3) — is the non-repudiable proof that the named allocator authorized the share. The auditor’s question is answered by the allocator and the authority, both recorded; the auditor does not ask “who redeemed it,” and Invariant 1 makes clear the records structurally cannot and do not answer that — which is the correct, honest boundary for bearer-token sharing, not a gap.

Disputed disclosure — “I never received that data.” A named intended recipient claims they never received the data. The records show capability tok_share_x1 was authorized for disclosure to dr-okafor-cardiology (the Sharing Authorized event, attested by Dr. Chen) and that a redemption-disclosure occurred (Sharing Disclosed, bound to disc_01). What the records cannot establish is whether dr-okafor-cardiology — versus a party who obtained the forwarded or intercepted token — actually presented it: bearer semantics make the redeemer unknowable (Capability Invariant 3/5, surfaced as Invariant 1). The records bound the forensic window precisely — this share was authorized to this recipient, by this allocator, and a bearer redeemed it at this time — without resolving redeemer identity, which is exactly Capability’s own disputed-disclosure boundary. Whether the recipient’s denial is accurate (the token was taken before redemption) or not is a question the bearer design deliberately leaves open; the composition is honest that it does.

Breach investigation — “during the incident window, was any disclosure made under a capability that should have been revoked, or any sealed event altered?” An investigator walks the Sharing Disclosed events in the window (reached through the substrate Audit Trail in Event Log insertion order), and for each, cross-reads the bound Selective Disclosure record and the capability’s state. A disclosure under a capability whose sharing.revoked event predates it would be the smoking gun — but Invariant 2’s binding plus Capability’s terminal-absorbing revocation (a Revoked capability returns invalid(revoked) and discloses nothing) forecloses it: no Sharing Disclosed event exists for a redemption that occurred after revocation. Because each disclosure’s descriptor is part of the sealed event payload, an attempt to silently widen a disclosed scope (to exfiltrate beyond what was authorized) breaks the seal (Invariant 4 + Tamper Evidence). The forensic window is bounded by the substrate’s seal cadence; the newest disclosures in the unsealed tail carry per-event immutability and become seal-verifiable at the next cadence.

Generation acceptance

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

Audit-Trail-traversal-clearable checks

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

Audit-subject asymmetry (the load-bearing guarantee). For every capability-backed disclosure, confirm the Sharing Disclosed event and the bound Selective Disclosure record name an allocator_ref (the authorizing party) and an authority, and confirm that no field anywhere — capability record, disclosure record, audit event data, or this composition emergent state — records a redeemer identity. A redeemer identity present in any record is a conformance failure against Invariant 1 (and against Capability Invariant 3/5). Confirm the recorded recipient is the allocator-declared intended recipient from the Sharing Authorized event, not a per-redemption value.
Disclosure-accountability binding. For every Selective Disclosure record produced by this composition, confirm exactly one Sharing Disclosed event carries its disclosure_id, that AuditTrail.verify_record returns verified for it, and that disclosure_to_redemption binds it to a capability_token. A disclosure with no sealed event, more than one, or a dangling binding is a conformance failure (Invariant 2); the inverse — every Sharing Disclosed event names a disclosure_id present in the disclosure store and disclosure_to_redemption.
Allocation-authorization provenance. For every capability_token in capability_to_sharing, confirm exactly one Sharing Authorized event carries it, that AuditTrail.verify_record returns verified, and that the event is attributed (via the substrate’s Actor Identity) to the recorded allocator_ref — i.e., the allocator’s authorization is non-repudiable (Invariant 3). For every Sharing Disclosed event, confirm its capability_token resolves to such a Sharing Authorized event.
Scope-bounded disclosure. For every disclosure, confirm its scope equals the disclosed_scope recorded in the corresponding Sharing Authorized event (and the capability’s immutable scope) — no disclosure exceeds or diverges from what was authorized (Invariant 4). Confirm the number of Sharing Disclosed events for a capability does not exceed its max_redemptions.
Constituent Generation acceptance bars. Verify Capability’s six checks over the capability store (including no redeemer identity is present in any record — Capability’s own check 3, which is the atom-level half of Invariant 1), Selective Disclosure’s six checks over the disclosure store, and Audit Trail’s six checks over the substrate (transitively clearing Event Log, Actor Identity, Tamper Evidence, Retention Window). This composition’s invariants depend on the correctness of the constituents’ invariants (Invariant 5).

Externally-clearable checks

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

Who actually redeemed a capability. By construction (Invariant 1, Capability Invariant 3/5) the records do not name the redeemer; whether the actual bearer was the allocator-declared intended recipient or another party is structurally unanswerable from any records — it is the inherent forensic limit of bearer-token sharing, not a gap a different store could close. An auditor needing redemption-identity assurance must require an identity-keyed access model (Permissions / Session) instead, which is a different composition with different semantics (named in Edge cases).
Whether the declared authority was legally valid. This composition records the asserted authority {type, reference}; whether the referenced consent was granted and in scope, the legal hold genuinely active, or the regulatory citation genuinely applicable at disclosure time requires the Consent / Legal Hold store or legal analysis — exactly Selective Disclosure’s authority legitimacy is unclearable gap, here inherited at the composition layer.
Whether the disclosed bytes matched the declared scope. This composition records that disclosed_scope was authorized and disclosed; whether the host actually transmitted only those fields (and not more) is the host’s delivery obligation, not provable from this composition’s records (mirroring Selective Disclosure’s the atom does not perform disclosures boundary).
Whether the allocator was authorized to authorize the share. This composition attests who allocated (the Sharing Authorized event under the allocator’s credential) but does not gate whether they were permitted to share that subject’s data; that requires a Permissions instance scoped to sharing authority, wired ahead of Authorize Sharing.

Edge cases and explicit non-goals

The audit-subject asymmetry is the design, not a gap. This composition records the allocator and never the redeemer. This is not an accountability hole to be patched — it is the precise reconciliation the composition exists to provide. A deployment that needs to know who accessed the data (not merely who authorized the access) does not want bearer-token sharing at all; it wants an identity-keyed access model (Permissions gating on the accessing actor, Session establishing who is present). The two are structurally distinct authorization models (Capability’s own Identity-bound authorization edge case names the boundary), and this composition deliberately implements the bearer one. Forcing a redeemer identity into this composition would break Capability Invariant 3 and defeat the purpose; the honest move is to choose the right primitive.
Recipient is the allocator-declared intended recipient, not the bearer. The recipient recorded in every disclosure is the party the allocator named at allocation time (the share was authorized to go to recipient R), not the party who actually presented the token (unknowable by bearer design). A deployment must choose recipient values meaningful to its regulatory audience (the GDPR Article 15(1)(c) named-recipient obligation, inherited from Selective Disclosure’s subject-recognizable recipient vocabulary edge case). Whether the actual bearer was R is the externally-unanswerable question the disputed-disclosure scenario names.
Redemption-decrement is recoverable under the host transaction; the binding is atomic (unlike Resolve a Person’s Data Rights). Redeem And Disclose performs the Capability.redeem decrement, the Selective Disclosure record, and the Sharing Disclosed event in one host transaction; on failure the whole binding aborts and the decrement rolls back with it. This is closer to Immutable Transaction Ledger (a pure atomic binding) than to Resolve a Person’s Data Rights (whose purge was irreversible and forced a modulo-clause): a counter decrement is a recoverable store write under a transaction, not a destruction. Where a deployment’s Capability, Selective Disclosure, and Audit Trail stores genuinely cannot share a transaction (distinct databases), the Cross-store consistency under partial failure case governs the orphan.
Cross-store consistency under partial failure. Under the host transaction boundary the binding is atomic and there is no partial state. Where the stores cannot co-transact, two orphans are possible and named: (a) Authorize Sharing allocated a capability but the Sharing Authorized write failed — an unattached capability with no authorization provenance; this composition returns rejected(...) and surfaces the orphan (revoke the unattached capability, or retry the attestation). (b) Redeem And Disclose decremented the redemption and recorded the disclosure but the Sharing Disclosed write failed — a disclosure record with no sealed event; the implementation retries the audit write until it lands, surfaces the orphan as a finding, and marks the recovered event cascade_recovery = true so an auditor distinguishes a clean disclosure from a recovered one (mirroring Resolve a Person’s Data Rights’ orphan discipline, but without Resolve a Person’s Data Rights’ irreversible-destruction severity — nothing is destroyed).
Scope is interpreted by this composition, opaque to Capability. Capability stores scope as a black box; this composition parses it per sharing_scope_grammar into the disclosure descriptor. A capability whose scope does not parse is refused at Authorize Sharing (invalid-sharing-descriptor), and a foreign capability (one not allocated through this composition) redeemed here is refused at Redeem And Disclose (not-authorized-sharing) — this composition discloses only shares it authorized, so a generic Capability token cannot drive an unscoped disclosure.
this composition does not deliver the data. Like Selective Disclosure, this composition records that a disclosure was authorized and occurred and to whom it was authorized; it does not retrieve, redact, format, or transmit the bytes. The host performs the delivery for the disclosed_scope, signalled by the disclosure record. Whether the host transmitted only the authorized fields is the host’s obligation and an externally-clearable check.
Authority legitimacy is not adjudicated. This composition enforces that authority.type ∈ {consent, legal-hold, regulatory} and that the reference is non-empty (the structural bound Selective Disclosure enforces, lifted to the composition boundary), but does not validate that the referenced consent/hold/regulation genuinely authorizes the disclosure — that legitimacy is an externally-clearable check (Consent store, Legal Hold store, or legal analysis), exactly as in Selective Disclosure and Resolve a Person’s Data Rights.
Allocator authorization is a composing concept. Whether the allocator_ref is permitted to share the named subject’s data is an inward-authorization question this composition does not gate — it composes no Permissions instance (the cut is Capability + Selective Disclosure + Audit Trail). The allocator is attested (so an auditor can always answer who authorized the share); whether they were permitted to requires a Permissions check wired ahead of Authorize Sharing, exactly as Resolve a Person’s Data Rights leaves operator authorization to a composing pattern.
Multi-use capabilities produce multiple disclosures. A capability with max_redemptions > 1 produces one Selective Disclosure record and one Sharing Disclosed event per redemption, each bound independently (Invariant 2 holds per redemption), all attributed to the same allocator (Invariant 1), all under the same authorized scope (Invariant 4). The redemption envelope bounds the count; the asymmetry holds across every redemption.
Token delivery and confidentiality in transit are out of scope. How the capability_token reaches the intended recipient (email, link, API response, QR code) and whether it is transmitted over an encrypted channel are handled at the deployment layer, inherited directly from Capability’s token delivery channel and token confidentiality in transit edge cases. This composition produces and records the token; the host delivers it.
Concurrency. Two concurrent Redeem And Disclose calls on a capability with remaining_redemptions = 1 are serialized by Capability’s exhaustion atomicity (Capability Invariant 4): exactly one redeems-and-discloses; the other receives invalid(exhausted) and discloses nothing — no double-disclosure beyond the authorized redemption count (Invariant 4). Concurrent disclosures on a multi-use capability each bind independently. A concurrent Revoke Sharing and Redeem And Disclose are serialized by Capability’s terminal-absorbing revocation: the redeem either precedes the revoke (discloses) or observes Revoked (discloses nothing).
Clock semantics. authorized_at, disclosed_at, and revoked_at are best-effort wall-time read from the substrate’s clock authority at record time (logic-confinement, inherited from the substrate per Immutable Transaction Ledger’s clock-source treatment); the Event Log sequence_number is the authoritative order source. For deployments where disclosure timestamps carry legal force, a Trusted Timestamping composition (RFC 3161 — the Internet standard for trusted time-stamping) provides the verifiable anchor; this composition inherits the substrate’s treatment.

Terms

The canonical concepts this spec refers to. Each [Term] marker in the prose above links to its card here. A card states what the concept is, in plain English, plus its Kind — one of four: Type (a thing or category), Operation (a behavior), Member (a value of an enumerated Type), or, for a named datum, Field (a datum a Type carries — what does it carry?) or Parameter (a value an Operation needs — what does it need?). A card also names the Type it is a Member of / Field of, the Operation it is a Parameter of, and its Role where the domain assigns one. A card carries one Projects line — the concept’s single canonical lowering token, the one place the concrete name stays visible on the page — for every Field, Parameter, and pinned/wire Member. Everything else about casing (each target’s snake / camel / pascal / const / wire form) is derived from that one token by tools/harness/term-adapter.mjs, never hand-written. This is a composition, so its own concepts are the emergent actions it exposes (Authorize Sharing, Redeem And Disclose, Revoke Sharing) and the two read-only queries (Sharing Disclosures, Authorization Provenance); the two Audit Trail event kinds that realize the audit-subject asymmetry (Sharing Authorized, attested under the allocator’s credential; Sharing Disclosed, attested under the service identity, naming no redeemer); the sharing-descriptor fields it interprets from the capability scope (Recipient — the allocator-declared intended recipient, not the bearer; Disclosed Scope); and its own rejections (Invalid Sharing Descriptor, Not Authorized Sharing). The audit-subject asymmetry itself is a structural guarantee (Invariant 1), not a cardable datum — there is no redeemer field to card. Its emergent state — the capability_to_sharing and disclosure_to_redemption indices — is a composition-introduced surface no constituent provides, left as backticked store tokens. References to the constituent atoms and their operations — Capability’s allocate / redeem / revoke, Selective Disclosure’s record / read, Audit Trail’s record_action / verify_record — the relayed tokens (capability_token, allocator_ref, subject_ref, authority, disclosure_id), the constituent redeem outcomes (redeemed, invalid(exhausted | expired | revoked | not-known)) and rejections (invalid-request, unknown-authority-type, recording-failure, storage-failure), and the deployment configuration knobs (sharing_scope_grammar, default_capability_ttl, default_max_redemptions) remain qualified/backticked, not carded here. (annotation.md Terms registry; representational only — it changes no guarantee, invariant, or behavior of the composition above.)

The composition’s allocation-with-attestation action: it parses the sharing descriptor against sharing_scope_grammar, allocates a bearer capability whose scope is the authorized disclosure (Capability.allocate), and records the allocator’s non-repudiable authorization as a Sharing Authorized event under the allocator’s own credential — committing the allocation, attestation, and binding together (Invariant 3). Returns {capability_token, authorization_event_id}, or Invalid Sharing Descriptor / an inherited rejection.

Kind: Operation

Redeem And Disclose

The composition’s load-bearing emergent action: it redeems the capability by possession alone (no identity argument), then — atomically — records a Selective Disclosure record and a sealed Sharing Disclosed event and binds them (Invariant 2). Returns {disclosure_id, event_id, disclosed_scope, allocator_ref}, a first-class invalid(...) outcome for a spent / lapsed / cancelled / unknown token, or Not Authorized Sharing for a foreign capability. Records the allocator, never the redeemer (Invariant 1).

Kind: Operation

The composition’s revocation action: it closes a sharing capability early (Capability.revoke) and records a sharing.revoked event under the revoker’s credential. Subsequent Redeem And Disclose calls for the token return invalid(revoked) and disclose nothing.

Kind: Operation

The read-only query returning a subject’s disclosure records joined to their authorizing allocator (never a redeemer) — a passthrough to SelectiveDisclosure.read plus the disclosure_to_redemption binding. Produces no Audit Trail event.

Kind: Operation

Authorization Provenance

The read-only query returning who authorized a given share — reads capability_to_sharing[capability_token] for the allocator, subject, recipient, disclosed scope, authority, and authorization event. Produces no Audit Trail event.

Kind: Operation

The Audit Trail event recorded at Authorize Sharing, attested under the allocator’s own credential — the allocator’s non-repudiable commitment that they authorized this share (Invariant 3). The authorization half of the audit-subject asymmetry.

Kind: Member Member of: the sharing event kinds Role: Audit event kind (allocator-attested) Projects: sharing.authorized

The Audit Trail event recorded at each Redeem And Disclose, attested under the composition’s service identity (the allocator is absent, the bearer has no credential); its data names the allocator_ref and carries no redeemer identity (Invariant 1). The disclosure half of the audit-subject asymmetry.

Kind: Member Member of: the sharing event kinds Role: Audit event kind (service-attested) Projects: sharing.disclosed

Recipient

The sharing descriptor’s allocator-declared intended recipient — the party the allocator named at allocation time as authorized to receive the share, recorded in every disclosure. Deliberately not the bearer who presented the token (unknowable by bearer design); whether the actual bearer was this recipient is the externally-unanswerable disputed-disclosure question.

Kind: Field Field of: the sharing descriptor Role: the allocator-declared intended recipient Projects: recipient

Disclosed Scope

The field subset the capability authorizes for disclosure (the minimum-necessary set), parsed from the capability’s immutable scope per sharing_scope_grammar. Every disclosure’s scope equals it exactly — no widening, no divergence (Invariant 4, scope-bounded disclosure).

Kind: Field Field of: the sharing descriptor Role: the authorized field subset Projects: disclosed_scope

The composition’s own rejection from Authorize Sharing — returned when the supplied descriptor does not parse under sharing_scope_grammar or leaves a required field (subject, recipient, disclosed scope, authority reference) empty. The share is refused before a capability is allocated.

Kind: Member Member of: the authorize-sharing rejection Role: Rejection Projects: invalid-sharing-descriptor

The composition’s own rejection from Redeem And Disclose — returned when a valid Capability token has no capability_to_sharing entry: a foreign capability allocated by some other composition, carrying no sharing descriptor. Nothing is disclosed; this composition discloses only shares it authorized.

Kind: Member Member of: the redeem rejection Role: Rejection Projects: not-authorized-sharing

Standards references

this composition is the structural form of accountable bearer-token data sharing: share by possession, prove who authorized each disclosure. Its primary anchors:

GDPR (EU General Data Protection Regulation) Article 32 (Security of Processing) — requires appropriate technical measures ensuring the confidentiality, integrity, and accountability of personal-data processing, including disclosures. This composition’s allocation provenance (the immutable, attested allocator_ref), the sealed disclosure-accountability binding, and the bounded redemption envelope are the technical measures that make a bearer-token disclosure accountable; the Sharing Authorized / Sharing Disclosed records demonstrate the measure from the records alone. (Article 30’s records-of-processing and Article 15(1)(c)’s recipient-disclosure obligations are inherited through Selective Disclosure.)
HIPAA (US Health Insurance Portability and Accountability Act) §164.514(d) (Minimum Necessary Standard) — disclosures of protected health information must be limited to the minimum necessary. The capability’s immutable scope encodes the minimum-necessary field subset, and Invariant 4 (scope-bounded disclosure) is the structural enforcement that the disclosure does not exceed it; the accounting-of-disclosures obligation (§164.528) is inherited through Selective Disclosure and the substrate’s six-year retention.
Object-capability (OCAP) model — the foundational theory that an unforgeable reference carries its own authority and the holder’s identity is irrelevant at use time (Dennis & Van Horn; Mark Miller’s capability-security work; Levy, Capability-Based Computer Systems). This composition is the library’s worked example of OCAP composed with regulated audit: it preserves the OCAP bearer semantics (no identity at redemption) intact while attaching accountability to the allocator — demonstrating that OCAP and regulated disclosure audit are compatible, the composition’s thesis.

this composition inherits the broader standards compliance of its constituents:

Through Capability: the OCAP literature (Jackson’s Software Abstractions Capability [Resource] concept, Miller, Levy, Birgisson et al.’s Macaroons), RFC 6749 §1.4 (OAuth 2.0 access tokens — the bearer-token-adjacent pattern), GDPR Article 32, HIPAA §164.514(d).
Through Selective Disclosure: GDPR Article 15(1)(c) and Article 30 (recipient disclosure and records of processing), HIPAA §164.528 (accounting of disclosures), SEC (US Securities and Exchange Commission) Rule 17a-4 — the disclosure-accounting layer.
Through the Audit Trail substrate (and transitively Event Log, Actor Identity, Tamper Evidence, Retention Window): SOX (Sarbanes-Oxley Act) §404/§802, HIPAA §164.312(b)/§164.530(j), PCI DSS (Payment Card Industry Data Security Standard) Requirement 10, 21 CFR (US Code of Federal Regulations) Part 11, SEC Rule 17a-4, ISO/IEC 27001 §A.12.4, GDPR Articles 30 and 32 — the attributed, retained, tamper-evident record the sharing events land on.

Status

grounded on Final Critique 4 — 2026-06-10 (2026-06-10) — three-round baseline + author Final Critique complete (three foundational + four refining findings closed in-pattern, foundational to zero); formal-layer vote YES and the derived TLA+ — Temporal Logic of Actions — model + buggy twin verified in tools/harness/ (CORRECT holds at 4 states; -buggy rejected on Inv2_BindingBijection); and the Phase 4 Opus Happy-Torvalds-X2 fresh-reader clearance gate cleared 2026-06-10 (claude-opus-4-8): foundational findings at zero, three refining + one rhetorical folded, the TLA+ model + twin re-verified mechanically, and capability provenance re-derived head-on against the constituent specs (Capability, Selective Disclosure, Audit Trail). Drafted against the approved this composition architectural cut — Capability (bearer token whose scope is an authorized disclosure) + Selective Disclosure (the disclosure-accounting record) + Audit Trail (substrate → Event Log + Actor Identity + Tamper Evidence + Retention Window) — mirroring Immutable Transaction Ledger’s substrate-plus-Selective-Disclosure shape, with the audit-subject asymmetry as the load-bearing emergent invariant and the disclosure-accountability binding bijection as the formal-model subject. Regulated-pattern conventions (Regulated adversarial scenarios; Generation acceptance with the Audit-Trail-traversal-clearable / externally-clearable split) baked in from the first draft, inherited from the methodology directly per pressure-testing.md §Regulated-pattern conventions.

Lineage notes

Regulated composition (composes two regulated atoms — Capability and Selective Disclosure — and records regulated events on the Audit Trail substrate). The two regulated-overlay conventions — Regulated adversarial scenarios and Generation acceptance (with the Audit-Trail-traversal-clearable / externally-clearable split) — are inherited from the methodology directly (pressure-testing.md), baked in from the first draft, not re-derived from predecessor patterns. The primary structural reference is Immutable Transaction Ledger with Selective Disclosure: this composition mirrors Immutable Transaction Ledger’s substrate-plus-Selective-Disclosure shape, its disclosure-accountability binding-bijection (the atomic SD-record-plus-*.disclosed-event commit), and its TLA+ binding-bijection model + buggy-twin structure. The substrate-composition recording pattern (recording on the Audit Trail the substrate carries) follows Audit Trail, Multi-Party Approval, and Resolve a Person’s Data Rights; the service-identity discipline for system-originated events follows Login. The novel contribution over Immutable Transaction Ledger is the audit-subject asymmetry: where Immutable Transaction Ledger’s disclosures are attributed to a present, credentialed actor, this composition’s redemptions have no present redeemer, so accountability attaches to the allocator (attested at allocation) while the redeemer is structurally unnamed — Capability’s bearer semantics (Invariants 3 and 5) carried intact into a regulated-audit composition.

Structural milestone. This composition retires the Capability-Backed Sharing *(not started)* forthcoming-reference in atoms/capability.md (Composition notes), making the reference a live link. Selective Disclosure’s Composition notes already list compositions adjacent to this composition (Immutable Transaction Ledger, Resolve a Person’s Data Rights) without a pending this composition marker, so no Selective Disclosure marker is retired. (Per the brief, the link resolution is applied at drafting since Capability points at this file; the marker is retired in the same change.)

Capability-provenance self-check. Every emergent invariant’s Rests on: clause traces to one of the four declared sources (pressure-testing.md §Capability provenance): named constituent invariants/actions (Capability Invariants 1/3/5/8 and redeem/allocate; Selective Disclosure record + Invariants 1/6; Audit Trail record_action + Invariant 1 reached through the named substrate), the deployment-declared sharing_scope_grammar and service-identity configuration capabilities, and composition-introduced surfaces (the scope-interpretation surface; the capability_to_sharing / disclosure_to_redemption maps; the allocation-time Sharing Authorized attestation). No invariant rests on an ambient “the system can…”. In particular, the audit-subject asymmetry (Invariant 1) is grounded on Capability’s declared bearer-redemption and audit-asymmetry invariants (3 and 5) surfaced through redeem’s allocator_ref return — not on an assumption that “the system doesn’t record redeemers”; the absence of a redeemer is a constituent guarantee plus a composition-introduced state shape with no redeemer field.

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

F1 — the disclosure audit event had no attestable subject — foundational (Pass 1 GRID / Pass 3). An early draft attributed the Sharing Disclosed event to the redeemer, but the redeemer has no credential (bearer) and the allocator is absent at redemption — there was no credential to attest the event, breaking record_action’s attestation requirement and the asymmetry itself. → Split the accountability across two events: Sharing Authorized attested under the allocator’s credential at allocation (the allocator’s non-repudiable commitment, Invariant 3), and Sharing Disclosed attested under the composition’s service identity at redemption with the allocator_ref named in the data and no redeemer — the asymmetry’s structural realization. This is the round’s foundational soundness fix.
F2 — the recorded recipient conflated “authorized to” with “consumed by” — foundational (Pass 3). The draft recorded the bearer as recipient, but the bearer is unknowable (Capability Invariant 3); recording it as the recipient would be a false claim. → The recorded recipient is the allocator-declared intended recipient (from the capability scope at allocation), never the bearer; Invariant 1 and a dedicated edge case state the distinction, and the disputed-disclosure scenario makes the forensic boundary explicit (who actually redeemed is externally-unanswerable by design).
F3 — audit-subject asymmetry mis-grounded as “the system records no redeemer” — foundational (Pass 2 EOS, capability-provenance). The draft asserted the asymmetry as an ambient property rather than tracing it to a declared source. → Invariant 1 now rests on Capability’s declared Invariants 3 (bearer redemption) and 5 (audit asymmetry), surfaced through redeem’s allocator_ref return, plus the composition-introduced state shape that has an allocator_ref field and no redeemer field — a declared-source provenance, not an ambient claim.
F4 — binding-bijection orphan over-stated as irreversible the way Resolve a Person’s Data Rights is — refining (Pass 3). An early draft carried the kind of modulo-clause Resolve a Person’s Data Rights uses for an irreversible redemption orphan, but a redemption-decrement is a recoverable store write under the host transaction (unlike the destruction Resolve a Person’s Data Rights performs). → Invariant 2 states the binding is atomic in the conforming case (the decrement rolls back with the binding), closer to Immutable Transaction Ledger than Resolve a Person’s Data Rights; the cross-store-consistency edge case names the orphan only for deployments whose stores cannot co-transact.
F5 — foreign-capability redemption unhandled — refining (Pass 3). A valid Capability token from another composition redeemed at Redeem And Disclose had no defined outcome. → Step 2 now rejects a token with no capability_to_sharing entry as not-authorized-sharing; this composition discloses only shares it authorized.
F6 — authority-type bound not enforced at the composition boundary — refining (Pass 1). The draft relied on Selective Disclosure to reject a bad authority.type at redemption, allowing a capability to be allocated for an invalid share that only fails later. → Authorize Sharing checks authority.type ∈ {consent, legal-hold, regulatory} up front (unknown-authority-type), refusing the share before a capability is allocated.
F7 — OCAP, TLA+, TTL acronyms unglossed at first body use — refining (Pass 1 acronym discipline). → Glossed at first occurrence.
Final Critique (author, X2 posture). Re-ran all three passes after the fixes. Foundational findings (F1, F2, F3) confirmed closed; the capability-provenance self-check re-verified every Rests on: clause resolves to a declared source with zero ambient dependencies, and confirmed the asymmetry is grounded on Capability’s declared Invariants 3/5 rather than an ambient “no redeemer recorded.” Pass 2 confirmed the externalizations a fresh reader is most likely to probe — the redeemer-identity externally-unanswerable boundary (the design, not a gap), authority legitimacy (externally-clearable), the data-delivery boundary (the host’s, like Selective Disclosure), and allocator authorization (no Permissions in the cut) — are EOS-clean. Foundational findings at zero. The pattern is author-clean but not yet grounded: grounding is gated on the fresh-reader Phase 4 Opus clearance gate (pending, separate session), per fresh-reader discipline.

Formal-layer vote: YES. The disclosure-accountability binding bijection (Invariant 2) is a load-bearing concurrency/safety claim — the Selective Disclosure record, the Sharing Disclosed event, and the redemption-decrement commit together or not at all under every interleaving — of exactly the shape Immutable Transaction Ledger’s binding-bijection model verifies. The audit-subject asymmetry (Invariant 1), the load-bearing emergent property, is a structural / by-construction guarantee (there is no redeemer field anywhere in the spec graph) verified by-construction at this composition’s layer and on Capability’s own surface by capability.als (Capability Invariants 3 and 5); it is not a TLA+-class temporal claim, so it is scoped out of the temporal model exactly as a structural property is — the temporal model carries the binding bijection, the structural asymmetry is Capability-model-verified. Allocation-authorization binding (Invariant 3) and scope-bounded disclosure (Invariant 4) are single-write-path / records-shape arguments; Invariant 5 is each constituent’s own bar.

Formal model — 2026-06-10: TLA+ authored and verified; formal layer discharged. Derived model capability-backed-sharing.tla with config capability-backed-sharing.cfg, checked via tools/harness/ (the repo’s tla-checker WASM — WebAssembly — checker; no Java). What it checks: per disclosure d (a redemption-that-discloses), three sub-writes — sdState[d] (the Selective Disclosure record), auditState[d] (the Sharing Disclosed Audit Trail event), and bound[d] (the disclosure_to_redemption binding, which also represents the committed redemption-decrement). The load-bearing Invariant 2 is checked as three safety properties under every interleaving: Inv2_BindingBijection (each disclosure is in one of two coherent configurations — uncommitted or fully-committed, never a dangling partial), Inv2_NoDanglingDisclosure (no Selective Disclosure record without its sealed Sharing Disclosed event and binding), and Inv2_NoOrphanAudit (no Sharing Disclosed event without its Selective Disclosure record). The CORRECT model performs all three sub-writes as a single atomic action (CommitDisclosure, the step-3 atomic-commit form); the properties hold across all reachable states. Bounds/saturation: Disclosures = {d1, d2}; the property is per-disclosure-local and the atomic commit is redemption-count-insensitive (mirroring Immutable Transaction Ledger’s disclosure-count insensitivity), so the bound is saturated and the verification value lives in the twin. Buggy twin: capability-backed-sharing-buggy.tla splits the commit into separate interleavable sub-steps (WriteSD → WriteAudit → Bind) with no compensation — the non-atomic implementation the Cross-store consistency edge case warns against; TLC stops after WriteSD alone (sdState = present, auditState = absent, bound = FALSE — a disclosure record with no sealed event) and rejects the twin on Inv2_BindingBijection. The twin is the vacuity guard — it proves the checker can fail on this property, so the correct model’s green is meaningful. Conflict-protocol outcome: none — the model corroborates the English; the spec already requires the disclosure, the seal, and the redemption to commit atomically (Invariant 2, Action wiring step 3), which is exactly the atomic/non-atomic distinction between the correct model and the twin. Canonical English unchanged. The audit-subject asymmetry (Invariant 1) is deliberately out of the temporal model scope (a structural / by-construction property, Capability-model-verified; see the vote). Reproduce: cd tools/harness && node check.mjs ../../compositions/capability-backed-sharing.tla (and … -buggy.tla --buggy).

Opus clearance gate — Happy Torvalds X2 — 2026-06-10 (claude-opus-4-8). Fresh-reader Phase 4 readiness check: Pass 1 GRID and Pass 2 EOS at standard intensity, Pass 3 Linus at X2 depth, fresh-reader discipline throughout — the spec body and the constituent specs read on their own terms, and every “closed”/”verified” claim in this composition’s own Lineage treated as an unproven assertion re-derived from source. Clean of foundational findings; four refining/rhetorical folded; foundational at zero; grounds on Final Critique 4.

Cross-reference re-verification (head-on against the constituent specs). Each invariant count and each cited invariant confirmed against the source. Capability declares twelve invariants — Invariant 1 (allocation-provenance immutability), 3 (bearer redemption), 5 (audit asymmetry), 8 (scope immutability), 2/10 (the redemption envelope — counter-monotonic / finite-lifetime), 4 (exhaustion atomicity) — every this composition citation name- and number-consistent, with allocate/redeem/revoke signatures as cited. Selective Disclosure declares six — 1 (record immutability), 5 (no-disclosure-unrecorded), 6 (append-only durability) — and record(subject_ref, recipient, scope, authority, disclosed_at?) as cited. Audit Trail declares eight application-level invariants — 1 (attribution coverage) — with record_action(action_ref, actor_ref, credential, data) and verify_record as cited, reached transitively as Event Log + Actor Identity + Tamper Evidence + Retention Window. This composition Invariant 5’s “(1–12)/(1–6)/(1–8)” counts are exact. (The retention_policy = audit_trail_retention_policy annotation on each record_action call matches the library-wide grounded substrate-composition convention — Defensible Retention, Multi-Party Approval, Immutable Transaction Ledger, Resolve a Person’s Data Rights, PAP all write it — so it is not a drift specific to this composition.)

Harness re-verification (mechanical, this session). node check.mjs ../../compositions/capability-backed-sharing.tla → all invariants hold, 4 states, PASS — the reachable space saturates at Disclosures = {d1, d2} (each disclosure independently uncommitted or fully-committed, so the fully-committed coherent configuration is genuinely reached: non-vacuous). node check.mjs ../../compositions/capability-backed-sharing-buggy.tla --buggy → VIOLATION on Inv2_BindingBijection, 2 states, correctly rejected — the twin’s non-atomic WriteSD → WriteAudit → Bind split stops after WriteSD alone (a Selective Disclosure record with no sealed Sharing Disclosed event and no binding — the exact cross-store orphan the bijection forecloses), so the checker can fail on this property and the correct model’s green is meaningful. The model faithfully encodes Invariant 2 in both directions (Inv2_NoDanglingDisclosure, Inv2_NoOrphanAudit); Invariant 1 (audit-subject asymmetry) is correctly out of TLA+ scope as a by-construction structural property, Capability-model-verified.

Capability-provenance re-verification. Every emergent invariant’s Rests on: clause resolves to a declared source — a named constituent invariant/action, a deployment-declared configuration capability, or a composition-introduced surface — with zero ambient dependencies. Invariant 1 (audit-subject asymmetry) rests on Capability’s declared Invariants 3 (bearer redemption) and 5 (audit asymmetry), surfaced through Capability.redeem’s allocator_ref return, plus the composition-introduced state (capability_to_sharing / disclosure_to_redemption) that by construction carries an allocator_ref field and no redeemer field — not an ambient “the system records no redeemer.” Confirmed there is nowhere in the spec graph — capability record, Selective Disclosure record, Sharing Disclosed event data, or any this composition emergent map — to record a redeemer; and the recorded recipient is honestly the allocator-declared intended recipient, with the disputed-disclosure scenario explicit that the actual bearer is structurally unprovable.

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

Final Critique 4 — Revoke Sharing left Capability.revoke’s storage-failure unmapped — refining (Pass 1 reference-graph). The taxonomy named already-terminal/not-known “through” plus its own recording-failure, but Capability.revoke’s storage-failure had no surface — silent rejection-code drift (PAP closes the same constituent’s other rejections with a catch-all). → Added storage-failure to the Revoke Sharing signature and mapped the constituent’s storage-failure through as storage-failure, mirroring Authorize Sharing’s allocate-failure mapping.
Final Critique 4 — Invariant 3 stated an unconditional allocation↔authorization binding the authorize-time orphan contradicts — refining (Pass 3). Orphan case (a) admits a capability allocated through this composition with no Sharing Authorized event where the stores cannot co-transact, but Invariant 3 lacked the “in the conforming case” qualifier Invariant 2 carries. → Invariant 3 now scopes its absolute to the conforming case under the host transaction boundary (allocate + attest + bind commit together or not at all) and names orphan (a) as the sole cross-store exception; Authorize Sharing step 5 gains the matching atomicity note.
Final Critique 4 — GDPR and HIPAA unglossed at first use — refining (Pass 1 acronym discipline). Both first appear in the summary blockquote (and Configuration) but were glossed only later, in the adversarial-scenario and Standards sections. → Glossed at first use in the blockquote (“EU General Data Protection Regulation”; “US Health Insurance Portability and Accountability Act”), matching the canonical Audit Trail blockquote convention.
Final Critique 4 — Invariant 1 said capability.als “checks” Capability Invariants 3 and 5 — rhetorical. The Alloy model enforces the asymmetry by construction (its capability record carries no redeemer field; redeem takes no identity argument), not via a named assertion, so “checks” overstated the mechanism. → Rephrased to “enforced by construction” in Invariant 1 and aligned the .tla header comment; the underlying claim — the asymmetry is formally grounded on Capability’s surface — is unchanged and sound.

The four findings sharpen content the spec already carried; none added previously-absent methodology-required content, so the gate is clean for grounding. Foundational findings: zero. This composition grounds on Final Critique 4.

Showcase pass — 2026-06-29. Representational-only annotation/legibility pass; no guarantee, invariant, number, formula, signature, or rejection taxonomy changed (the invariant count held at five). (a) Four-kind [Term] annotation applied across the body and a ## Terms registry added after Edge cases (11 terms): 5 Operations — the emergent actions (Authorize Sharing, Redeem And Disclose, Revoke Sharing) and the two read-only queries (Sharing Disclosures, Authorization Provenance); 4 Members — the two asymmetry-carrying Audit Trail event kinds (Sharing Authorized under the allocator’s credential; Sharing Disclosed under the service identity, naming no redeemer) and the composition’s own rejections (Invalid Sharing Descriptor, Not Authorized Sharing); and 2 Fields — the sharing-descriptor fields the composition interprets from the capability scope (Recipient — the allocator-declared intended recipient, not the bearer; Disclosed Scope). The audit-subject asymmetry itself is left uncarded — it is a structural guarantee (Invariant 1), not a datum: there is deliberately no redeemer field anywhere to card. No Type card (the emergent state maps capability_to_sharing / disclosure_to_redemption are backticked store tokens) and no Parameter (all action inputs are relayed constituent tokens or the descriptor fields above). Survivors left backticked: the fenced projected-contract signatures (the #### \name` action headings and their code blocks); every qualified constituent call (Capability's allocate / redeem / revoke, Selective Disclosure's record / read, Audit Trail's record_action / verify_record); the constituent redeem outcomes (redeemed, invalid(exhausted | expired | revoked | not-known)) and inherited rejections (invalid-request, unknown-authority-type, recording-failure, storage-failure); the relayed tokens (capability_token, allocator_ref, subject_ref, authority, disclosure_id), the sharing.revoked event kind, the deployment configuration knobs; and concrete example ids. Constituent atom names remain the existing full links to ../atoms/*; constituent operations stay backticked qualified calls, not cross-page links (the decided convention). (b) **Summary/blockquote merge** — ## Summary moved to the top (after TOC, before Intent), its first run-on paragraph split one-idea-per-paragraph (cut #1, lossless) with the common-uses paragraph kept intact; the dense descriptive top blockquote folded out after confirming each claim (the bearer-sharing / regulated-audit reconciliation; the three-atom composition; the audit-subject asymmetry; the disclosure-accountability binding bijection; the OCAP anchor) is carried by Summary / Intent / Composes / the load-bearing wiring decision; no *also-known-as* line existed, so none was invented. *Note:* the folded blockquote also carried the first inline glosses of GDPR / HIPAA; these acronyms remain glossed in the adversarial-scenario and Standards sections, so no claim was lost. (c) **Lineage collapsed** into a

 block. (d) **prose cut #5 — skipped (with reason):** the composition owns no state machine — the capability lifecycle (Active / Redeemed / Expired / Revoked) is Capability's, and the composition's own logic is a uniform authorize → redeem-and-disclose → revoke wiring already stated crisply. Re-verified, not re-grounded: Status stays at

grounded on Final Critique 4 — 2026-06-10

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

.tla models untouched — harness re-run green: capability-backed-sharing.tla PASS (4 states) + capability-backed-sharing-buggy.tla –buggy rejected on Inv2_BindingBijection`.