Immutable Transaction Ledger with Selective Disclosure

Composition partially resolved 6 invariants TLA+ model buggy twin ×1 regulated composes 1 atom + 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

Immutable Transaction Ledger with Selective Disclosure

Summary

Immutable Transaction Ledger with Selective Disclosure is a regulated composition (a spec that wires two or more atoms — freestanding, self-contained pattern specs — together) that solves a problem no single atom solves alone: keeping a tamper-evident, attributed, append-only ledger of transactions and being able to hand a regulator, counterparty, or data subject a verifiable slice of it — proving that slice is genuine and was part of the ledger, recording that the disclosure happened and under what authority, and revealing nothing about the rest. It wires two constituents: the Audit Trail substrate (the immutable, attributed, tamper-evident, retention-governed ledger, assembled from Event Log, Actor Identity, Tamper Evidence, and Retention Window) and Selective Disclosure (the durable, append-only accounting of every disclosure — recipient, scope, authority, time).

The composition’s two defining emergent guarantees are disclosure-accountability binding bijection — every Disclose Subset writes exactly one Selective Disclosure record and exactly one Audit Trail ledger event recording that the disclosure happened — preceded by an intent event that records the attempt and is where the discloser’s credential is checked — three writes in a fixed order, intent then accounting record then outcome, never atomic, with any partial failure surfaced and compensated until the pair is restored — so the act of disclosing is itself an immutable, attributed, sealed ledger entry and no disclosure ever lacks its ledger proof silently or permanently — and verifiable partial disclosure — any disclosed subset can be independently verified by its recipient as authentic and derived from the ledger, while the undisclosed remainder stays undisclosed and its integrity uncompromised. The first is a structural binding between the two stores; the second is a behavioral obligation on the ledger’s tamper-evidence, realized (not defined) by mechanisms such as Merkle inclusion proofs, cryptographic accumulators, or signed disclosure packages.

This composition’s most common uses are broker-dealer transaction records under SEC Rule 17a-4, accounting-of-disclosures under HIPAA §164.528, regulatory submissions under 21 CFR Part 11, and data-subject disclosure accounting under GDPR Article 15. Any system that must keep an immutable, attributed ledger and prove a subset of it to an outside party — without exposing the rest and without being able to deny that the disclosure occurred — is a candidate for this composition.

Intent

Every domain that keeps a record of consequential transactions faces the same paired requirement. First, the record must be a trustworthy ledger: append-only and totally ordered (no entry inserted out of sequence or quietly back-dated), attributed (every entry tied to a verified actor), tamper-evident (any after-the-fact rewrite detectable from the records alone), and retention-governed (kept for its regulatory lifetime, lawfully destroyable with a defensible record). Second, the record must be selectively shareable with accountability: a regulator, counterparty, auditor, or data subject is shown a subset of the ledger — a single trade, one patient’s billing disclosures, the records pertaining to one matter — and that act of sharing must itself be recorded (to whom, what scope, under what authority, when), while the disclosed subset can be independently verified as genuine and the undisclosed remainder is neither revealed nor weakened.

No single atom satisfies both. The Audit Trail substrate supplies the first: it is the immutable, attributed, tamper-evident, retention-governed ledger, assembled from Event Log (append-only total order), Actor Identity (attribution), Tamper Evidence (sealing), and Retention Window (lifetime). Selective Disclosure supplies the accountability half of the second: a durable, append-only record of every disclosure — recipient, scope, authority, timestamp. But neither provides the full surface until they are wired together. Audit Trail does not know what a disclosure is or that disclosing a subset of its own events is itself an auditable event. Selective Disclosure does not perform disclosures, does not seal anything, and — by its own Invariant 5 (no-disclosure-unrecorded) — cannot enforce from inside that every disclosure was in fact recorded; it names that as an integration obligation for a composing pattern to close. The wiring is this composition.

The cross-domain structural identity is the composition’s thesis. Under SEC Rule 17a-4 a broker-dealer must keep transaction records in a non-rewritable, non-erasable form and produce them, or a defined subset, on demand for an examiner. Under HIPAA §164.528 a covered entity must give an individual an accounting of disclosures of their protected health information — what was disclosed, to whom, when, and why — drawn from its records alone. Under 21 CFR Part 11 an electronic record submitted to a regulator must be attributable, contemporaneous, and tamper-evident, with disclosures to the agency themselves recorded. Under GDPR Article 15 a data subject may demand to know what data was disclosed and to which recipients. The structural form is identical across all four: one immutable attributed ledger, and an accountable, independently verifiable mechanism for disclosing a subset of it. One grounded composition satisfies all four.

This is a composition, not a new primitive. The Audit Trail substrate (with its constituent atoms Event Log, Actor Identity, Retention Window, and Tamper Evidence, reached transitively) and Selective Disclosure are unchanged. The composition is the wiring that makes them coherent as a single immutable-ledger-with-accountable-disclosure surface. It introduces emergent actions — Record Entry, Disclose Subset, Verify Disclosure, Verify Ledger, and a read passthrough — that belong to no single constituent and exist only because the two are wired together. Disclose Subset in particular belongs to neither: Selective Disclosure records that a disclosure happened but does not seal a verifiable subset of a ledger; Audit Trail seals events but does not know a disclosure is occurring or that it must be accounted. The composition is the layer that answers: was this subset genuinely part of the ledger, was its disclosure recorded and authorized, and did showing it compromise nothing else?

What the composition is not: it is not a redaction or transmission engine (Selective Disclosure’s boundary holds — the composition records and proves disclosure; it does not fetch, redact, or route the underlying payloads); it is not the authorization layer that decides whether a disclosure is permitted (that is Consent / Permissions, named as a composing peer); it is not the legal-hold suspension layer over the ledger’s retention (Legal Hold / Defensible Retention); it is not an at-most-once append guarantee under retry (Idempotent Reservation / Duplicate Prevention, named as an optional enrichment); and it is not the clock-authority layer (inherited from Audit Trail). Each is named explicitly in Edge cases.

Composes

Audit Trail — the regulated-audit substrate that is the immutable transaction ledger. Every ledger entry the composition appends records here as one AuditTrail.record_action call — consumed at the substrate’s declared contract, record_action(action_ref, actor_ref, credential, data) → event_id | rejected(invalid-credential | invalid-request | recording-failure(step)), the (step) payload carried on every transcription (Primitive policies, the by-position rule) — producing an Event Log entry (append-only, totally ordered — the ledger’s sequence), an Actor Identity attestation (binding the entry’s acting actor to a verified credential — the attribution), a Tamper Evidence seal per the configured cadence (the tamper-evidence), and a Retention Window record (the lifetime). The act of disclosing a subset is likewise recorded here — as two record_action calls: an intent record (ledger.disclose_intended) written before the Selective Disclosure write and an outcome record (ledger.disclosed) written after it, each producing its own Event Log entry, attestation, seal, and retention record. The doubling of substrate writes on the disclosure path is a real addition to ledger volume and retention footprint, stated here where the substrate wiring is introduced rather than left to be discovered. The composition maintains exactly one Audit Trail instance configured with the host’s regulatory retention policy. Event Log, Actor Identity, Tamper Evidence, and Retention Window are reached transitively through Audit Trail — the composition does not maintain separate instances of those four atoms at this layer, per the Compositions of compositions convention (see spec-format.md): naming Audit Trail as the substrate satisfies the Event Log + Actor Identity + Tamper Evidence + Retention Window requirement transitively. Instance capability requirement — the ledger-side enumeration. Every records-alone claim on this page that quantifies over ledger.disclosed or ledger.entry events — the disclosure_to_event rebuild, both orphan enumerations, Verify Ledger’s rebuild read, Generation acceptance checks 1 and 5 — is an action_ref-shaped selection, and the substrate does not serve that shape: Event Log’s Reverse lookup / indexing edge case routes payload-field and action_ref-shaped lookup to a separate Reverse Index pattern, Audit Trail disclaims it, and the passthrough’s own invalid-query definition would reject it. The route this composition declares is therefore the substrate’s pass-through list read by sequence-number range, over the range beginning at 1 with an open upper bound, with every selection made composition-side on the returned events’ action_ref and payload fields; the wired Audit Trail instance must expose that open-upper-bound sequence-range read (the same requirement the substrate places on its own Event Log). Id-addressed reads go through AuditTrail.read_record(event_id), which the substrate does declare. A deployment that composes Reverse Index over the ledger may use it to accelerate the selection; the enumeration is the declared route and the one an auditor reproduces.
Selective Disclosure — the disclosure-accountability surface. Every Disclose Subset action records here as one SelectiveDisclosure.record(subject_ref, recipient, scope, authority, …) call, producing the durable, immutable disclosure record (recipient, scope, authority {type, reference}, timestamp) that regulators require for disclosure accounting. The composition calls record and read. Selective Disclosure deliberately does not perform the disclosure, seal anything, or enforce that every disclosure is recorded — its Edge cases name “Cryptographic protection … → Tamper Evidence”, “Retention governance → Retention Window”, and its Invariant 5 (no-disclosure-unrecorded) is an integration obligation. The composition is where all three re-converge: Tamper Evidence (via the Audit Trail substrate) seals the disclosure outcome event (whose data mirrors the disclosure record’s accounting field set — the seal covers exactly the mirrored fields; see Disclose Subset step 4), Retention Window (via the substrate) governs that event’s lifetime, and the composition structurally closes Invariant 5 for disclosures routed through it by making Disclose Subset its only disclosure surface and having it always record (system-wide exclusivity is a deployment property this composition cannot enforce — Invariant 4 states the honest scope). Retention governance over the Selective Disclosure store itself is not absorbed here — it is handled at the deployment layer; see the Retention of the disclosure-accounting store edge case.

The Audit Trail substrate and the Selective Disclosure store are owned by their respective constituent instances; the composition does not duplicate their state. It indexes between them with one emergent map (disclosure_to_event, below).

Composition logic

Composition state

The composition owns one piece of emergent state that wires the two constituents into a queryable, records-alone-defensible disclosure-accountability surface:

disclosure_to_event — a derived index (per execution-contract.md §Composition state — the derived-index rule) from a Selective Disclosure disclosure_id to the Audit Trail event_id that recorded the disclosure act in the ledger. The binding fact lives in the substrate: every ledger.disclosed event carries data.disclosure_id, so the index carries no truth of its own — it is read-path acceleration over substrate truth. The rule’s three obligations, discharged here: (1) named derivation — the index derives from the Audit Trail substrate’s Event Log; the rebuild procedure is to enumerate the ledger by the declared route — the open-upper-bound sequence-range read, selecting action_ref = ledger.disclosed composition-side (Composes, instance capability requirement) — and record data.disclosure_id → event_id for each (the same enumerating read the inverse orphan check below already uses); the reconciliation scan runs it in full, as a write, every cycle (partial-failure edge case (a)). (2) Outside the binding surface — the index is excluded from Disclose Subset’s binding obligation: Invariant 1’s binding surface is the two truth-bearing sub-writes (the Selective Disclosure record and the Audit Trail ledger.disclosed event), and the index’s population after both succeed is evidence the truth-bearing writes committed, never a peer write the compensation protocol must handle. A missing or lost index entry is a rebuild trigger, not data loss, and not an orphan. (3) No consistency claim — the index inherits best-effort composition-query semantics; the authoritative binding check is always the substrate read. Entries are never modified after insertion. The classification splits at the retention horizon, and the purged half is truth-bearing. When a ledger.disclosed event is lawfully purged at its retention end, the substrate destroys its payload in its entirety — data.disclosure_id with it. What survives on the substrate side is the destruction record’s (event_id, attestation_id) pair, from which the attestation keeps action_ref = ledger.disclosed, actor_ref and attested_at readable; the substrate declares that its destruction record carries no payload field, so the accounting key survives nowhere in any constituent. It survives here: the index entry disclosure_id → event_id — written at Disclose Subset step 5 while the event was live, and re-written by every reconciliation scan cycle’s full rebuild, which is the write the truth-bearing half actually rests on, since step 5 is reached only by an invocation that returned and its failure is by its own terms a rebuild trigger — is the only carrier of the binding key past the horizon, and for a purged event it is therefore truth-bearing under a durability obligation — a lost entry there is a finding, not a rebuild trigger, because no rebuild can recover it. The finding is honest only because the fact was captured before it was presumed: the Configuration inequality keeps every scan cycle shorter than the shortest retention period, so an event lives through at least one rebuild before any purge can reach it, and a never-written entry is foreclosed (§A derived index splits at the horizon). That half is extraction-pending against the forthcoming Erasure Tombstone atom the substrate itself names for the same class of fact (a durable record of what a purge destroyed and how it was keyed); until it lands, the obligation is the deployment’s — the index store must be as durable as the Selective Disclosure store whose records it keys. A rebuild from the live ledger never touches a purged entry: it repopulates the live half and leaves the purged half standing, and the binding is thereafter answerable as binding-purged (Invariant 1’s retention-horizon arm) through that entry’s event_id and the Purged retention record it resolves to — never silently re-asserted as a live binding. A disclosure_id present in the Selective Disclosure store with no ledger.disclosed event naming it, or a ledger.disclosed event whose data.disclosure_id is not present in the Selective Disclosure store, is a structural finding (Invariant 1 — binding bijection). Both orphan checks are run over the declared enumeration route — the sequence-range read passed through Audit Trail, with the action_ref selection made composition-side, never a filtered query the substrate would refuse — the inverse check enumerating every ledger.disclosed event; disclosed_entry_ids validation, by contrast, is id-addressed and goes through read_record. The composition needs no separate index for either direction, which is precisely why the map classifies as derived — for events whose payloads are still readable.

The ledger entries themselves are Audit Trail events; the composition does not maintain a separate entry store. A “transaction entry” is an Audit Trail event id; the “subset” named in a disclosure is a set of those ledger event ids. The Selective Disclosure store and the Audit Trail substrate state are owned by their constituent instances; the composition indexes into them via disclosure_to_event.

Configuration

ledger_retention_policy — the policy reference configured on this composition’s single Audit Trail instance, governing the lifetime of the ledger events (both transaction entries and disclosure events). Set once on the Audit Trail instance; record_action takes no per-call retention argument. For broker-dealer deployments under SEC Rule 17a-4 the policy must encode at least the six-year (and first-two-years-accessible) retention floor; for HIPAA §164.528 deployments the disclosure-accounting horizon is at least six years. Multi-jurisdiction reconciliation is a Policy Reconciliation composing concept; this composition takes the reconciled policy_ref as input.
seal_cadence — inherited from the Audit Trail substrate’s configuration (per-event, interval-based, or on-demand). For a ledger whose subsets will be disclosed and independently verified, per-event or tight interval-based cadences are recommended: an unsealed entry cannot yet anchor a partial-disclosure proof, so the unsealed tail is the window during which a freshly-appended entry is not yet independently verifiable on disclosure. This composition does not override the cadence; it names the consequence explicitly in Invariant 2.
disclosure_completion_bound — the deployment-declared maximum duration of a Disclose Subset invocation from its seam reading to its outcome record (step 4): the reading is taken before step 1 and passed through as the record’s disclosed_at at step 3, so the bound is measured from that reading to the scan’s own seam-injected reading — two readings of one clock authority, this composition’s (Clock source edge case) — and spans validation, the intent record, the accounting write and every outcome attempt. It is the lower edge of the reconciliation scan and of Generation acceptance check 1’s orphan enumeration: a Selective Disclosure record whose disclosed_at is younger than it may belong to an invocation still between its two truth-bearing writes, and a compensation fired at it would append a ledger.disclosed beside the one the invocation is about to write — the two-events-for-one-disclosure state Invariant 1’s exactly-one forbids. The upper edge is ledger_retention_policy’s horizon: a record older than it whose event is gone is binding-purged through the index’s truth-bearing half, or an index-loss finding — never a compensable orphan (Cross-store consistency under partial failure). Default: none; the deployment sets it above the slowest conforming invocation’s seam-to-step-4 interval including its outcome_retry_attempts; it is also the length of the disclosure_section lease (below), so an invocation still inside step 4 when the bound elapses has yielded whether or not its attempts are spent. A bound shorter than that is no longer unsafe in the direction that writes — the invocation’s step 4 pre-checks under the same per-disclosure_id section the scan takes and adopts the scan’s event rather than appending beside it (§A compensator is exclusive) — but it costs attribution: the record is bound under the recovery identity with the discloser preserved only in disclosed_by, where a longer bound would have let the discloser’s own credential attest it.
reconciliation_cadence and outcome_write_latency — the interval at which the reconciliation scan runs in addition to its mandatory run at restart, and the deployment’s disclosed bound on one record_action landing. Together with the bound they fix the two promises the scan makes. The surfacing bound: an orphan created at t is invisible to the scan until t + disclosure_completion_bound, the next run is at most a cadence later, so no orphan survives unsurfaced past disclosed_at + disclosure_completion_bound + reconciliation_cadence (Invariant 1’s safety arm), and none survives unbound past that plus outcome_write_latency on the run whose compensating write lands (a run whose write fails transiently retries at the next, one cadence later). The horizon inequality: disclosure_completion_bound + reconciliation_cadence + outcome_write_latency < the shortest retention period ledger_retention_policy can assign, strictly — the first term is also the longest a stalled-but-alive invocation can hold the disclosure_section against the scan, since the lease is exactly that long, so no separate hold term is needed — every ledger.disclosed event then lives at least one full scan cycle before any purge can reach it, which is what makes the scan’s every-cycle rebuild of disclosure_to_event a guarantee that the purged half was captured (Composition state) and makes an orphan bindable before its own intent event purges. Cadence no longer than the horizon is satisfied by a deployment that breaches on every orphan; the three terms are checked at instance start, and a deployment whose knobs fail the inequality refuses to start (§Liveness is arithmetic). Default: none for either.
outcome_retry_attempts — the number of times a Disclose Subset invocation re-attempts its outcome record_action on a transient recording-failure(step-2 | step-3) — each attempt preceded by the pre-check, all while the disclosure_section is held — before it returns rejected(recording-failure(outcome)) and yields the orphan to the scan. The invocation holds one clock reading and cannot time its own terminus, so this terminus is counted rather than timed; the timed terminus is the section’s lease expiry at disclosure_completion_bound, and the invocation yields at whichever comes first. It is the invocation’s half of the one-writer-per-record rule (partial-failure edge case). Default: none.
disclosure_section — an instance capability requirement: a deployment-supplied per-disclosure_id mutual exclusion that Disclose Subset step 4 and every reconciliation-scan write share. It is a critical section spanning calls of two constituents — a read of the ledger and a write to it, beside a scan that reads the Selective Disclosure store — and neither constituent declares one (Audit Trail serializes each record_action, Selective Disclosure each record), so it is the host’s, named here and nowhere attributed to a constituent (§Capability provenance, the critical-section tell). Its semantics are stated, not assumed. The section is taken by the invocation the moment step 3 returns disclosure_id — the key does not exist before that write, and no leg can see the record before it exists — and by the scan before its pre-check on any record it examines. It is released on the holder’s return or death. Where the host implements it as a lease, the lease is exactly disclosure_completion_bound long, measured from the invocation’s seam reading, and its expiry is the invocation’s terminus: an invocation whose lease has expired has yielded, and a stalled-but-alive holder therefore blocks the scan for at most the bound, which is the term the liveness inequality already carries. No write after the accounting write is made except while the section is held: an invocation that finds its section lost re-takes it before its pre-check, and the re-taken section — obtained only past the bound — permits adopting an event the scan landed and permits no append. A deployment that cannot supply the section cannot run Disclose Subset conformingly; there is no degraded mode, because the one-writer rule is what the binding bijection’s exactly one rests on. Default: none — deployment-required.
disclosed_entry_ids_cap and intent_candidates_cap — the most members disclosed_entry_ids may name, and the most intent_event_candidates a compensating ledger.disclosed event may name. Step 1 sizes the largest record the act can write — the outcome payload at the first cap plus the compensation’s fields at the second — against the substrate’s payload_cap before the intent record, and the argument that the outcome-position invalid-request is foreclosed is true only because both sets are bounded (§An outcome is sized before the intent): non-empty is a lower bound, and a caller can reach any upper bound the Configuration does not state. A set over the first cap is rejected(invalid-request) at step 1; an orphan whose candidate set exceeds the second is escalated as an unresolved finding rather than compensated. Default: none for either.
application_actor_ref and application_credential — the composition’s recovery identity: a registered actor in the substrate’s Actor Identity registry under which the reconciliation scan attests every record it writes outside the invocation that owed it — the ledger.recovery_intended record, the compensating ledger.disclosed event, and the ledger.disclosure_unbindable marker. The discloser is carried in the compensating event’s sealed data (actor_ref preserved as disclosed_by), never as its attesting actor_ref: the discloser’s credential is not in hand when the scan runs. Earlier revisions named this identity as “the deployment’s declared recovery identity” without declaring it; it is declared here, since the liveness arm of Invariant 1 spends it.
index_durability — the durability the deployment owes the disclosure_to_event store, stated as an ordering: at least as durable as the Selective Disclosure store whose records it keys. Inside the horizon the index is derived and a lost entry is a rebuild trigger; past it an entry is the only carrier of the binding key (Composition state — the purged half is truth-bearing), and a lost entry there is the binding-gap finding Verify Ledger case (c) reports against this obligation. The obligation is against loss, not against capture: capture is the scan’s every-cycle rebuild under the reconciliation_cadence inequality, so an entry the auditor finds missing for a purged event was written and lost, and the finding is honestly this obligation’s. The obligation is the deployment’s until the Erasure Tombstone atom lands.
tamper_evidence_supports_partial_disclosure — a deployment-declared boolean (default required-for-disclosure) asserting that the Tamper Evidence mechanism configured inside the Audit Trail substrate can produce a verification artifact for an individual entry or a named subset that an independent party can check against the ledger seal without access to the undisclosed entries. This is the mechanism capability on which Invariant 2 (Verifiable Partial Disclosure) rests. This composition introduces the surface that consumes this capability — the verification_bundle and Verify Disclosure — at the composition layer: no Tamper Evidence or Audit Trail action produces or checks a subset proof today (the Tamper Evidence atom verifies whole record-sets), so that surface is emergent here, pending a forthcoming Subset Proof atom (see the Subset proofs edge case). It is stated as a behavioral obligation, never as a mechanism: see The load-bearing wiring decision for why the composition requires the capability but not any particular realization of it. A deployment whose Tamper Evidence mechanism cannot satisfy this capability may still use Record Entry (the ledger remains immutable, attributed, tamper-evident as a whole) but its Disclose Subset proofs degrade to whole-ledger verification — named explicitly as the Whole-ledger-only tamper evidence edge case.

Primitive policies

The composition takes string-typed inputs at its action boundaries; each is validated either at this layer or by a constituent.

entry_id / event_id — opaque, system-generated by the Audit Trail substrate’s Event Log. A ledger transaction entry is addressed by its event_id; the composition returns it as entry_id at Record Entry and accepts a set of them as the disclosed subset at Disclose Subset. Byte-identity equality; never normalized.
disclosure_id — opaque, system-generated by Selective Disclosure. Returned at Disclose Subset; the key in disclosure_to_event. Byte-identity equality; never normalized — the bijection’s matching predicate (data.disclosure_id against the Selective Disclosure store) compares bytes.
invocation_id — one fresh identifier per state-changing invocation, injected at the composition’s I/O seam alongside now (the Logic Confinement Principle — minted nowhere inside a transition) and written into every event payload the invocation emits: ledger.entry, ledger.disclose_intended, ledger.disclosed. It is what makes Record Entry’s read-back after an indeterminate substrate arm exact (the by-position rule) — Disclose Subset’s read-back keys on disclosure_id, which the scan’s compensating event carries too — and it is the join the reconciliation scan uses to tell one invocation’s records from a repeat with identical parameters. It is not the intent-to-outcome key — that stays intent_event_id, substrate-minted and sealed — and Selective Disclosure records do not carry it (the atom’s record has no field for it), which is why the scan pairs an orphan to its intent by the injected reading rather than by this id (Cross-store consistency under partial failure).
transaction_data — opaque payload of a ledger entry, passed through to AuditTrail.record_action’s data. The composition does not interpret it; the host system defines its schema.
actor_ref + credential — the acting party for a ledger write or a disclosure, and their opaque credential, consumed by the Actor Identity inside the Audit Trail substrate. The substrate validates the credential inside every record_action — for Disclose Subset that is the intent record, which stands before the SelectiveDisclosure.record call that commits the disclosure (the intent record is itself a substrate write — an attestation, an Event Log entry and a retention record — so the precise claim is Invariant 6’s: no constituent call that commits is reached before the caller’s credential has validated), so invalid-credential is a pre-state refusal there with nothing recorded in either store; for Record Entry it is the single ledger write, which is itself the load-bearing write. Mapped per the by-position rejection rule below.
disclosed_entry_ids — a non-empty set of ledger event_ids naming the subset being disclosed, of at most disclosed_entry_ids_cap members (Configuration — the upper bound step 1’s sizing rests on; a set over the cap is rejected(invalid-request) before the intent record). Each must resolve to a known ledger.entry (transaction) event in the Audit Trail substrate: the composition validates membership by reading the substrate’s Event Log for each id and confirming its action_ref = ledger.entry. An id that is unknown to the Event Log, or that resolves to a ledger.disclosed event (a disclosure event, not a transaction entry), yields rejected(unknown-entry). An empty set is rejected(invalid-request). The composition keeps no separate entry store — a transaction entry is a ledger.entry Audit Trail event — so the substrate Event Log is the authoritative membership oracle.
subject_ref — opaque reference to the subject the disclosed subset pertains to (an account, a patient, a counterparty, a matter). Passed to SelectiveDisclosure.record; validated by the constituent (non-empty).
recipient — non-empty string naming the party receiving the disclosure. Validated by Selective Disclosure.
scope — non-empty string naming what subset/fields were disclosed (Selective Disclosure’s scope). The composition additionally records the structured disclosed_entry_ids in the ledger disclosure event’s data; scope is the human/regulatory-facing descriptor, disclosed_entry_ids is the machine-checkable set.
authority — the structured {type ∈ {consent, legal-hold, regulatory}, reference} field Selective Disclosure requires; validated by the constituent (unknown-authority-type propagated). This composition does not itself check that the authority is valid (that a referenced Consent was in force) — that is a composing Consent/Permissions concept named in Edge cases; this composition records the asserted authority and makes the assertion auditable.

record_action rejection-mapping rule — by call position, and by step. For every AuditTrail.record_action call below, the substrate’s rejection taxonomy (invalid-credential | invalid-request | recording-failure(step)) maps by the call’s position relative to the truth-bearing constituent write, not uniformly — and the (step) payload is load-bearing at every position, because the substrate attests at its step 2, appends at its step 3, and places retention at its step 4: recording-failure(step-2 | step-3) means the event is not in the log, while recording-failure(step-4) means the event is appended and attested and only its retention placement failed — the substrate’s own Invariant 2 liveness arm owns that gap, and a retry from this layer would append a second event. invalid-request has the same two-sidedness by a different route: the substrate routes its own retention-configuration faults (Retention Window’s invalid-policy / policy-not-found at its step 4) onto this arm, reached with the event already appended, so the token alone does not say whether the event landed — the read-back does. There are three positions for the substrate’s arms, and a fourth position for the one constituent write that is not a record_action.

At an intent record — nothing has committed, so every arm is a clean pre-state rejection. invalid-credential → rejected(invalid-credential): the credential did not validate against the actor registry for the supplied actor_ref, and the composition refuses with nothing written to either store. invalid-request → rejected(invalid-request): a deployment fault, pageable, never retried until the fault is corrected — on its retention source the intent event stands in the log with no outcome, which is the expected residue check 5 already triages. recording-failure(step) → rejected(recording-failure(intent)): the genuinely retryable arm — nothing truth-bearing committed, so the caller may retry the whole action; on step-4 the intent event likewise stands, same residue.

At an outcome record — the Selective Disclosure record is immutable once committed and cannot be rolled back, so no arm can refuse the act, only report it — and one arm reports that it succeeded. recording-failure(step-4) → the outcome event is appended and attested: the invocation reads it back by the declared enumeration route, selecting action_ref = ledger.disclosed and this disclosure_id composition-side — the key the scan’s compensating event carries too, so the read-back finds the leg’s write as readily as the invocation’s own — and proceeds as landed — populates the index, constructs the bundle, returns success — with a hard alert on the unretained event, never a retry. recording-failure(step-2 | step-3) → rejected(recording-failure(outcome)) with the orphan handled per the Cross-store consistency under partial failure edge case. invalid-request → the same read-back decides: found (the retention source) → proceed as landed; absent (the payload source) → rejected(recording-failure(outcome)) and the orphan discipline’s deterministic arm. invalid-credential → rejected(recording-failure(outcome)) and the orphan discipline; note what is reachable there and what is not: it survives only as a mid-flight revocation or expiry between the intent record and the outcome record, since the same credential validated moments earlier.

At the accounting write — Selective Disclosure’s record, between the intent record and the outcome record. Its storage-failure means no record was persisted (that atom’s own contract: no record is durably persisted and recorded(disclosure_id) is not returned), so nothing a retry would duplicate exists and it lands rejected(recording-failure(intent)) — the intent event stands as the attempt’s record, the residue check 5 triages; its invalid-request and unknown-authority-type are relayed by name, and both are likewise pre-commit (Disclose Subset step 3).

At Record Entry — a single substrate write that is itself the credential-verifying call. This is the nothing-commits-first case: no state depends on an unverified claim, so invalid-credential is a clean pre-state rejection without any second mechanism. The same write is also the load-bearing one, so its step-4 arm and its invalid-request retention source both mean the entry is in the ledger, and returning a rejection would send the caller back to append it again — Record Entry is not idempotent (At-most-once append under retry). Both are read back by invocation_id and returned as success with a hard alert; only recording-failure(step-2 | step-3) and the payload-source invalid-request reject.

Two dispositions, two positions, and the position rides the composition’s own code. From the intent record recording-failure(intent) means nothing committed — retry the whole action. From the outcome record recording-failure(outcome) means the disclosure record committed and its ledger event is owed — there the reconciliation scan, not the caller, owns the retry, and re-invoking Disclose Subset would create a second disclosure record. Inside the action the substrate’s (step) decides which; at the caller boundary the composition’s arm carries the position, because the caller is the one who retries and a bare token after an outcome-position failure would tell them, by the signature, that nothing was committed (§A composition’s own rejection arm carries the retry bit). Record Entry exports the bare token lawfully: its one record_action is its only write, so the token has one position.

This composition enforces the seam at its own boundary. An upstream Actor Identity pre-check is defence in depth, not a control this composition depends on: authentication is not inheritable across a composition boundary and this surface is independently callable, so its own verification is the direct-call path’s only defence.

No primitive is case-sensitivity-normalized at the composition layer, and no whitespace trimming is applied anywhere. “Present” and “non-empty” name the same checkable predicate throughout: the value is supplied and has length ≥ 1 (byte length for strings, element count for sets) — a whitespace-only string is accepted, never normalized, per the byte-identity discipline.

Action wiring

The composition exposes four orchestrating actions and one read passthrough. Record Entry and Disclose Subset change ledger state and record in Audit Trail; Verify Disclosure and Verify Ledger are read-only verification queries; read passes through to the substrate. The disclosure_to_event insertion occurs only after both truth-bearing constituent writes succeed — its population is evidence that the binding obligation was met, not part of the obligation itself (the map is a derived index, outside the binding surface; see Composition state).

Authentication precedes commitment — the intent record. Disclose Subset opens, after its read-only validation, with an intent record: an AuditTrail.record_action naming what the invocation is about to do, written before the SelectiveDisclosure.record call that commits. One call doing two jobs. First, it is where the caller’s credential is verified — the substrate validates it against the actor registry’s public material for the supplied actor_ref inside record_action (Actor Identity’s own guard) — so a permanent, non-removable disclosure-accounting record, naming a recipient, a scope and an asserted authority, is never committed on an unverified actor’s say-so; invalid-credential is a clean pre-state refusal with nothing written to either store. Second, it is the marker-before-act recovery record: an intent event with no outcome event names an invocation that committed nothing, committed and failed to record, or died in between, which the reconciliation scan resolves against the Selective Disclosure store. The intent record carries the invocation’s parameters and never a constituent-minted id (none exists yet); the outcome record carries disclosure_id, the result, and intent_event_id back to its intent record. Record Entry has no intent record and needs none — its single AuditTrail.record_action is the load-bearing write, so no state depends on an unverified claim (Invariant 6).

The intent-to-outcome relation, declared. Every ledger.disclosed outcome event names exactly one ledger.disclose_intended event through intent_event_id; every intent event is named by at most one outcome event. The zero case on the second side is not a defect — it is the attempt an invocation left behind. The relation is composition-introduced, lives inside the outcome event’s sealed payload (so it is covered by Tamper Evidence rather than carrying only the weaker spec-level guarantee), and is deliberately not part of Invariant 1’s binding bijection, which is over Selective Disclosure records and ledger.disclosed outcome events alone.

`record_entry`

record_entry(transaction_data, actor_ref, credential) →
    {entry_id}
  | rejected(invalid-credential | invalid-request | recording-failure)

Appends one transaction to the ledger. Steps:

Validate transaction_data present and actor_ref non-empty. Failure → rejected(invalid-request). Stop.
AuditTrail.record_action(action_ref = ledger.entry, actor_ref, credential, data = {invocation_id, transaction_data, recorded_at = now}) → event_id. (Throughout the action wiring, now denotes the clock reading injected at this composition’s I/O seam — one reading per invocation, read by the host before the transition runs and composed into every payload the invocation writes, never a clock the composition samples inside a step and never a value the substrate supplies, since Audit Trail exposes no clock to its callers; see the Clock source edge case — and invocation_id the identifier injected at the same seam, Primitive policies.) Map invalid-credential → rejected(invalid-credential); recording-failure(step-4) → the entry is appended: read its event_id back by the declared enumeration route selecting action_ref = ledger.entry and this invocation_id, and continue to step 3 with a hard alert on the unretained event; invalid-request → the same read-back: found → continue to step 3; absent → rejected(invalid-request); recording-failure(step-2 | step-3) → rejected(recording-failure). Stop on any arm that rejects.
Return {entry_id = event_id}. The entry is now an immutable, attributed, sealed (per cadence), retained ledger event.

`disclose_subset`

disclose_subset(
  disclosed_entry_ids,
  subject_ref,
  recipient,
  scope,
  authority,
  actor_ref,
  credential
) →
    {disclosure_id, event_id, verification_bundle}
  | rejected(
      invalid-credential
    | invalid-request
    | unknown-entry
    | unknown-authority-type
    | recording-failure(intent | outcome)
    )

Records that a named subset of the ledger was disclosed to a recipient under an authority, and produces the artifact by which the recipient can independently verify that subset. The disclosure act is itself appended to the ledger. Steps:

Validate: disclosed_entry_ids non-empty (invalid-request if empty); subject_ref, recipient, scope non-empty (invalid-request); every id in disclosed_entry_ids resolves, via AuditTrail.read_record(event_id) — the substrate’s declared id-addressed read — to a known event whose action_ref = ledger.entry (a transaction) — not a ledger.disclosed event (Unknown Entry naming every failing id — the full set, deterministically; sets have no “first” element); disclosed_entry_ids within disclosed_entry_ids_cap (Configuration; over → invalid-request); and the largest record this act can write fits the substrate’s payload_cap: construct the maximal envelope — the step-4 outcome payload with this disclosed_entry_ids and every other field at its maximal width (disclosure_id, intent_event_id, disclosed_at, recorded_at at the widths the seams mint them), plus the fields a compensating event adds (disclosed_by, cascade_recovery, entry_set_unresolved, and intent_event_candidates at intent_candidates_cap members) — serialized as the substrate sizes it ({action_ref, actor_ref, attestation_id, data}, the envelope Audit Trail’s own step 1 measures), and refuse invalid-request if it exceeds the cap. The intent payload is a strict subset of that envelope, so what passes here passes at step 2, at step 4, and on the scan’s compensating write alike; sizing the intent alone would let a set through that step 4 cannot land, over a Selective Disclosure record that cannot be rolled back (§An outcome is sized before the intent). Stop on any.
Intent record. AuditTrail.record_action(action_ref = ledger.disclose_intended, actor_ref, credential, data = {invocation_id, disclosed_entry_ids, subject_ref, recipient, scope, authority.type, authority.reference, recorded_at = now}) → event_id_intent. Nothing has committed, so every arm is a clean pre-state rejection: invalid-credential → rejected(invalid-credential) — the caller’s credential did not validate against the actor registry for actor_ref, and the composition refuses the disclosure with nothing written to either store; invalid-request → rejected(invalid-request), a deployment fault, pageable and never retried until corrected — its retention source leaves this intent event standing with no outcome, the residue check 5 triages (note that this code now has two producing sites — the caller’s empty set, empty field, over-cap set or over-cap envelope at step 1, and this one). This payload is a strict subset of the envelope step 1 sized — the outcome adds intent_event_id, disclosure_id and disclosed_at, and a compensating event adds more — so a disclosed_entry_ids set that passes here cannot deterministically fail at step 4 over a Selective Disclosure record that has already committed and cannot be rolled back; step 1’s sizing is what forecloses that window, and it is the only thing that does; recording-failure(step) → rejected(recording-failure(intent)) with nothing truth-bearing committed, the genuine-retry arm and structurally distinct from step 4’s same-token arm (on step-4 the intent event stands, same residue). Stop on any. The payload carries the invocation’s parameters and no constituent-minted id — disclosure_id does not exist yet, and it is the key the derived index and both orphan enumerations read, so an intent event carrying one would be a rebuild hazard.
SelectiveDisclosure.record(subject_ref, recipient, scope, authority, disclosed_at = now) → disclosure_id — the injected reading is passed explicitly through the constituent’s optional disclosed_at? parameter, so the accounting record’s timestamp and the outcome event’s disclosed_at (step 4) are one reading rather than two taken at two seams, and that shared reading is also the key the scan pairs an orphaned record to its intent event by (disclosed_at = the intent event's recorded_at; Cross-store consistency under partial failure). Map invalid-request → rejected(invalid-request) — reachable here on two conditions, a field Selective Disclosure’s own rule refuses and its not-in-future guard, which compares the passed disclosed_at against its own seam’s reading, a reading this composition assumes is never behind its own (Clock source edge case); either way nothing is written and the intent event stands, the residue check 5 triages; unknown-authority-type → rejected(unknown-authority-type); storage-failure → rejected(recording-failure(intent)) — no record was persisted, so nothing a retry would duplicate exists. Stop on any. (Selective Disclosure writes first; it is the disclosure-accounting record of record. If the subsequent ledger write fails, the orphan is a Selective Disclosure record with no ledger.disclosed event — index absence merely follows — surfaced per the partial-failure edge case.)
Under the disclosure_section: pre-check, then append. The invocation holds the per-disclosure_id section from the moment step 3 returned (disclosure_section, Configuration — the same section the reconciliation scan takes for every record it examines, partial-failure edge case (a)); if it finds the section lost — a lease that expired at disclosure_completion_bound — it re-takes the section before anything else, and having re-taken it past the bound it has yielded: it may adopt below and may not append. Inside the section, run the scan’s own pre-check first: enumerate by the declared route for a ledger.disclosed event whose data.disclosure_id equals this disclosure_id. If one exists, adopt it as this invocation’s outcome: the scan compensated this record while the invocation was stalled past disclosure_completion_bound, or an earlier attempt’s acknowledgment was lost; take its event_id, continue to step 5 as landed, and append nothing — a second ledger.disclosed for one disclosure_id is the two-events-for-one-disclosure state Invariant 1’s exactly one forbids, and the sealed trail would then protect it (§A compensator is exclusive). An adopted event carries cascade_recovery = true where the scan wrote it; the invocation returns the event_id it holds, whichever writer landed it, and where the adopted event carries entry_set_unresolved = true the invocation carries that fact to step 6, which must not build a bundle over a set the sealed event does not determine. If none exists and the section is the invocation’s own (not re-taken past the bound), AuditTrail.record_action(action_ref = ledger.disclosed, actor_ref, credential, data = {invocation_id, intent_event_id: event_id_intent, disclosure_id, disclosed_entry_ids, subject_ref, recipient, scope, authority.type, authority.reference, disclosed_at, recorded_at = now}) → event_id. The disclosing actor’s credential attests the disclosure. The event’s data mirrors the disclosure record’s full accounting field set — subject_ref, authority.reference, and disclosed_at (the Selective Disclosure record’s timestamp — the reading step 3 passed, the accounted disclosure time) included — because the substrate seal covers exactly what this payload carries: the tamper-evidence guarantee over the disclosure record extends to the mirrored set and no further. (Selective Disclosure’s immutability is the atom’s spec-level guarantee, not records-alone verifiable — by that atom’s own composition notes, Tamper Evidence is what lifts it to a cryptographically checkable property; a field not mirrored into the sealed payload keeps only the weaker spec-level guarantee, so its rewrite by a storage-layer adversary would leave no records-alone trace.) recorded_at is the audit-write time: on the invocation’s own outcome it is the same reading as disclosed_at (one reading per invocation), and on the scan’s compensating event it is the scan’s reading, while disclosed_at preserves when the disclosure was accounted (the field §164.528’s “date” and Part 11’s “contemporaneous” actually need under seal). Arms per the by-position rule’s outcome position: recording-failure(step-4), and invalid-request whose read-back finds the event → the event is appended; take its event_id from the read-back and continue to step 5 with a hard alert; recording-failure(step-2 | step-3) → re-run the pre-check and re-attempt, still inside the section, at most outcome_retry_attempts times (Configuration) — the invocation holds one clock reading and cannot time its own terminus, so it counts it — and when the attempts are spent, rejected(recording-failure(outcome)), the section released, the orphan the scan’s; invalid-credential, and invalid-request whose read-back finds nothing → rejected(recording-failure(outcome)); orphan per the partial-failure edge case. An invocation past the bound whose pre-check finds no event has no append to make and returns rejected(recording-failure(outcome)) — the scan’s next cycle is the writer. Stop on any arm that rejects; the section is released on every exit from this step, and on the invocation’s death.
Populate the derived index: disclosure_to_event[disclosure_id] = event_id. (Inside the horizon, read-path acceleration only — the binding truth is already durable in the ledger.disclosed event’s data.disclosure_id, and a failure to populate here is a rebuild trigger, not a partial write. The entry’s truth-bearing life begins at the purge, and this step is not what guarantees it exists by then: the reconciliation scan re-runs the full rebuild every cycle and writes every live binding into the index, so an entry this step failed to write is written within reconciliation_cadence of the event’s landing, and the Configuration inequality keeps every cycle shorter than the shortest retention period — Composition state, the purged half.)
Construct Verification Bundle — the subset verification artifact for disclosed_entry_ids. This is a composition-introduced surface, not an action of any constituent. The Tamper Evidence atom’s verify checks a whole sealed record-set, and Audit Trail’s verify_record checks a single whole event — neither exposes an action that produces an inclusion proof for a named subset of a sealed range. This composition constructs the bundle at this layer by invoking the configured Tamper Evidence mechanism’s inclusion-proof capability over the seal material the substrate has already committed to — the capability the deployment declares via tamper_evidence_supports_partial_disclosure. This is the mechanism-capability residual invocation class the Execution Contract permits under capability-provenance discipline (execution-contract.md §Substrate composition invocation); the bundle lets a recipient confirm each disclosed entry is a genuine, unaltered ledger entry covered by the ledger seal, without access to the undisclosed entries. (Realization is mechanism-specific — a set of Merkle inclusion proofs, an accumulator witness, or a signed package; this composition requires the bundle to be independently checkable against the ledger seal, not any particular form. A forthcoming Subset Proof atom would let this delegate to a named constituent surface rather than a composition-layer construction — see the *Subset proofs are a composition-introduced surface edge case.)* This step has a defined failure arm: both truth-bearing writes have already committed and the binding holds, so a bundle-construction failure (the mechanism briefly unreachable) returns success with verification_bundle = unavailable(reason) — never a rejection, which would falsely tell the caller the disclosure was not recorded. The same arm is taken, deterministically, for an adopted event carrying entry_set_unresolved = true (step 4): the bundle is a projection over the disclosed_entry_ids the sealed disclosure event records, and an event that omits the set determines none, so the invocation returns verification_bundle = unavailable(entry-set-unresolved) rather than a bundle built from the set it still holds in memory — a set no record under seal asserts is not one this composition may prove; the disclosure is bound, and its bundle is not reissuable (partial-failure edge case (a)). The bundle is a pure projection over committed material (the seal material plus the disclosed_entry_ids recorded in the sealed disclosure event), so it is re-derivable at any time by re-invoking the same construction for a committed disclosure — the reissue path, which the deployment exposes read-only; a failed or lost bundle is recoverable, not a permanent loss of Invariant 2. The same arm covers a crash between step 4 and step 6; the index entry step 5 did not reach is written by the scan’s next rebuild.
Return {disclosure_id, event_id, verification_bundle} (verification_bundle = unavailable(reason) only on step 6’s failure arm, unavailable(entry-set-unresolved) included).

`verify_disclosure`

verify_disclosure(disclosed_entries, verification_bundle, ledger_seal_reference) →
    disclosure-proof

The emergent verification action — a composition-introduced surface (no constituent exposes a subset-proof check; see step 6 of Disclose Subset and the Subset proofs edge case), runnable by the recipient of a disclosure or any auditor holding the disclosed entries and the bundle — without access to the ledger’s undisclosed contents. disclosed_entries is the set of disclosed entry records the recipient received — each its entry_id and the entry payload — against which the bundle is checked; it is not the whole ledger, and the action never reads an undisclosed entry. The action is self-contained given those disclosed entries, the bundle, and a reference to the ledger seal (the published seal/root the Tamper Evidence mechanism anchors to; how that reference is published and kept singular — so that two recipients verifiably hold the same ledger’s seal — is a deployment obligation named in the externally-clearable checks). It is total: it always returns a disclosure-proof, never a rejected(...) — a structurally malformed verification_bundle or ledger_seal_reference yields per-entry authenticity = unverifiable(bundle-malformed) and overall_verdict = disclosure-unverified, not a thrown rejection. This is deliberate: the action is a check a recipient runs on material they already hold, so every outcome is a verdict, not a precondition rejection. Zero presented entries is likewise a verdict, never a vacuous success: overall_verdict = disclosure-unverified(no-entries-presented) — “every entry authentic” is not satisfiable over an empty set. Returns a disclosure-proof:

entries — per disclosed entry: entry_id, and authenticity ∈ {authentic, altered, not-in-ledger, unverifiable(reason)} — the result of checking the entry against the verification_bundle and ledger_seal_reference. Authentic means the entry is a genuine, unaltered ledger entry covered by the seal; Altered means the entry does not match what the seal committed to; Not In Ledger means the bundle does not place the entry under the seal.
Confidentiality Preserved — true iff the bundle and disclosed entries reveal nothing about the count, content, or position of undisclosed entries beyond what the seal reference inherently publishes. This is the structural statement of “the remainder stays undisclosed”; its realization is the mechanism’s zero-knowledge-of-complement property (a Merkle proof reveals sibling hashes but not sibling contents; an accumulator witness reveals nothing of non-members). This value is self-reported: it is computed by the verification routine over the bundle the discloser produced, and is not independently recomputable from this composition’s records. Its trustworthiness rests on the deployment’s security review of the configured mechanism’s zero-knowledge-of-complement construction (the externally-clearable check), not on this composition’s word — so a recipient independently confirms authenticity against the published seal, while confidentiality is an assurance about the audited mechanism rather than a recipient-recomputable verdict.
overall_verdict — disclosure-verified (every entry authentic and confidentiality_preserved = true) or disclosure-unverified(reasons).

Verify Disclosure is the composition’s defining emergent contribution on the disclosure side: neither Selective Disclosure (which records that a disclosure happened but seals nothing) nor Audit Trail alone (which seals the whole ledger but has no notion of a verifiable disclosed subset) can answer it. Note this action does not consult disclosure_to_event — it is deliberately runnable by an external recipient who holds only the bundle; the accountability side (was this disclosure recorded and attributed?) is answered separately by Verify Ledger / read against the disclosure event.

`verify_ledger`

verify_ledger(disclosure_id, original_event_payloads) →
    accountability-proof
  | rejected(not-known)

The accountability-side verification, run by an auditor with access to the composition’s stores. original_event_payloads is a map keyed by the audit log’s sequence_number to the byte-exact payload Event Log holds at that position — keyed by position and not by event_id, because the record set a seal commits to is a sequence range, not one event: AuditTrail.verify_record takes the payloads of every event in the covering seal’s coverage in ascending sequence_number order, and read_record names that range for the event (Audit Trail Invariant 7). Under the interval cadence the substrate recommends that range spans transaction entries, intent records, and whatever else the deployment records on the instance, so a map keyed by event_id could hold at most one payload per event and every verification would return failed-verification(seal-record-set-mismatch) on an intact ledger; under per-event cadence each range is a singleton and the map holds one payload per event — the special case, not the rule. Given a disclosure_id, returns whether the disclosure is bound to exactly one immutable, attributed, sealed, retained ledger event (the binding bijection, Invariant 1):

Look up disclosure_id in the Selective Disclosure store. If absent → rejected(not-known). Stop.
Resolve the binding against the substrate — the authoritative binding check is always the substrate read (Composition state, obligation 3); the disclosure_to_event index only accelerates it. On an index hit, AuditTrail.read_record(event_id) — and branch on the retention state it returns before anything else is checked: Purged, with the surviving attestation’s action_ref = ledger.disclosed → case (b) below, without running the rebuild read, since the payload a match would need was lawfully destroyed and its absence is destruction, not a miss (§Lawful destruction is answered before absence); Retained, or unresolved (compensation window) → confirm the event’s data.disclosure_id matches the queried disclosure_id before reporting Bound (an accountability verdict never rests on a best-effort cache alone). On an index miss, run the rebuild read: enumerate the ledger by the declared route (Composes), selecting ledger.disclosed events composition-side, for one whose data.disclosure_id matches — a derived index may be stale or lost without any truth being lost; a miss the rebuild read resolves is a rebuild trigger, not a finding. Three terminal cases: (a) the event is found → proceed with its event_id. (b) No live event names the disclosure_id, but disclosure_to_event[disclosure_id] holds an event_id — the purged half of the index, truth-bearing (Composition state) — whose retention record is Purged and whose destruction record’s attestation carries action_ref = ledger.disclosed → binding = binding-purged (Invariant 1’s retention-horizon arm — lawful, distinguishable, not a finding). The key is decidable from the records because this composition preserved it, in the one store that keys it after the payload is gone; the substrate’s destruction record carries (event_id, attestation_id) and nothing else, so the case is unreachable from the substrate alone (see the Retention of the disclosure-accounting store edge case). An index entry lost past the horizon leaves the case indistinguishable from (c) and is reported as binding-gap — a finding against the durability obligation, which is what that obligation exists to make visible, and honestly a finding of loss: the scan’s every-cycle rebuild under the Configuration inequality captured the entry before the purge could reach the event (Composition state). (d) No event, but a ledger.disclosure_unbindable event names the disclosure_id → Binding Unbindable, binding = binding-unbindable(reason): the permanently unbindable orphan’s terminal verdict — a deployment-configuration finding, not a transient (the Cross-store consistency under partial failure edge case, the deterministic invalid-request arm); superseded by (a) if a ledger.disclosed event later lands. (c) No event, no honest-destruction record, and no unbindable marker → accountability-proof with binding = binding-gap. Per Invariant 1’s liveness arm, binding-gap is never a steady state under a conforming implementation: it denotes either an orphan observed during compensation (already surfaced per the safety arm; the Cross-store consistency under partial failure edge case) or a conformance failure — in both cases a high-priority finding (a recorded disclosure with no ledger event), not a routine outcome.
Only on binding = bound: read the covering range — AuditTrail.read_record(event_id) names the event’s sequence_number, the [lo .. hi] range its covering seal commits to, and the coverage status. Destruction is answered before absence. If the coverage status is partially purged — another member of the range was lawfully destroyed — call AuditTrail.verify_record(event_id, <whatever members of the range the map holds>) and relay its unverifiable(partially-purged-coverage) unchanged: the substrate answers that before it reads a presentation, and a membership check run ahead of it would report a payload the caller cannot supply as one they failed to supply (§Lawful destruction is answered before absence). Otherwise assemble the presentation original_event_payloads[lo] .. original_event_payloads[hi] in ascending order, and call AuditTrail.verify_record(event_id, <presentation>) (Audit Trail Invariant 7 — the original record set is re-presented by the caller, not fetched); record attribution-verification, seal status, and retention state. If the map lacks any member of the covering range, the proof carries attestation_verification = unverifiable(payload-not-supplied(missing)), naming the absent sequence numbers — a defined verdict, not a rejection, and not a failure: the seal cannot be checked without its whole record set, which is a fact about what was presented, not about the ledger. An event still in the unsealed tail returns the substrate’s own failed-verification(unsealed), relayed unchanged. The other arms skip this step: on Binding Purged the proof carries the event_id the purge record preserves, attestation_verification = unverifiable(purged), and retention_state = Purged; on Binding Gap the proof carries no event_id and omits attestation_verification / retention_state — the gap itself is the finding; on binding-unbindable(reason) the proof carries the marker event’s event_id, the substrate_rejection it recorded, and no retention_state for a ledger event that never landed.
Return accountability-proof { disclosure_id, event_id, binding ∈ {bound, binding-purged, binding-unbindable(reason), binding-gap}, attestation_verification, retention_state }.

`read` (passthrough)

read(query) → results | rejected(invalid-query)

Routes by query class: disclosure-accounting queries (by subject, recipient, authority type, time range) pass to SelectiveDisclosure.read(query); ledger queries by sequence-number range or wall-time range pass through to the Audit Trail substrate’s list read unchanged, and a query by event_id goes to AuditTrail.read_record. An action_ref-shaped ledger query is not a passthrough shape — the substrate routes it to Reverse Index and would reject it as invalid-query — so “every ledger.disclosed event” is answered by the open-upper-bound range read with the selection made in composition code (Composes, instance capability requirement), which is the route Verify Ledger’s rebuild read, the orphan enumerations, and Generation acceptance checks 1 and 5 all take. rejected(invalid-query) has exactly one producing condition: the query conforms to neither constituent’s declared query shape — an action_ref-shaped query included. Without recording. No state change.

The load-bearing wiring decision — disclosure ⇒ {intent, accounting record, ledger event}, ordered and compensated; partial-verifiability as a capability, not a mechanism

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

Half 1 — the binding. Every Disclose Subset writes, in a fixed order and never atomically, an Audit Trail ledger.disclose_intended intent event (where the discloser is authenticated), a Selective Disclosure record (the disclosure-accounting record of record) and an Audit Trail ledger.disclosed outcome event (the immutable, attributed, sealed, retained proof that the disclosure occurred) — no transactional boundary spans the two stores, the accounting record is irreversible once written, and any partial failure between it and the outcome is surfaced and compensated by one writer (Invariant 1’s safety + liveness arms) — and indexes the pair in disclosure_to_event.

Principle. Disclosure accounting that an outside party can trust requires two facts to be inseparable: that the disclosure was recorded with its authority (Selective Disclosure’s contribution), and that this record of disclosure is itself immutable, attributed, and tamper-evident (Audit Trail’s contribution). Likely objection: why not let Selective Disclosure alone carry it? Mechanism that resolves it: Selective Disclosure deliberately extracted tamper-evidence, retention, and attribution during its own EOS (Essence of Software — Daniel Jackson’s framework for specifying software concepts as freestanding, composable units) Pass 2 — its Edge cases name all three as composing concepts, and its Invariant 5 (no-disclosure-unrecorded) is explicitly an integration obligation it cannot self-enforce. The composition is exactly where those re-converge: the Audit Trail substrate supplies attribution + seal + retention in one surface, and by making Disclose Subset the only disclosure surface and having it always write both records, the composition structurally closes Invariant 5 — a disclosure cannot occur through this composition without producing both records. Result: a disclosure-accounting record that is itself non-repudiable and tamper-evident, which neither constituent provides alone.

Half 2 — partial verifiability as a behavioral obligation. A disclosed subset must be independently verifiable as authentic and derived from the ledger, while the undisclosed remainder stays undisclosed and uncompromised. The composition requires this capability of its tamper-evidence substrate; it does not require any particular realization.

Principle. The point of disclosing a subset is to prove that slice genuine without exposing the rest. Likely objection: doesn’t this force a Merkle tree — i.e., bake a mechanism into the spec? Mechanism that resolves it: No — and deliberately not. Tamper Evidence is itself mechanism-neutral by design (its spec names hash chains, Merkle trees, and external anchoring as interchangeable realizations); for this composition to normatively demand Merkle would contradict its own constituent and elevate one realization into the ontology. So the composition states the obligation behaviorally — “the substrate’s tamper-evidence can produce, for a named subset, a verification artifact an independent party checks against the ledger seal without access to the undisclosed entries” — and lists realizations (Merkle inclusion proofs, cryptographic accumulators, signed disclosure packages, or future proof systems) only as rationale. A deployment whose Tamper Evidence cannot meet the capability is not non-conforming to this composition; its Disclose Subset degrades to whole-ledger verification, named in Edge cases. Result: the essential capability — verifiable partial disclosure — is specified; the implementation mechanism is left to the deployment, preserving the abstraction boundary the library holds between what must be true and how it is achieved.

Composition-level invariants

These invariants emerge from the composition. None belongs to a single constituent; each requires both the Audit Trail substrate and Selective Disclosure working together.

Invariant 1 — Disclosure-accountability binding bijection (safety + liveness). A one-to-one binding between Selective Disclosure records produced by this composition and Audit Trail ledger.disclosed events: every such disclosure record has exactly one corresponding ledger event whose data.disclosure_id points back to it, and vice versa. The two truth-bearing writes (the Selective Disclosure record and the ledger.disclosed event; the disclosure_to_event map is a derived index outside this surface — see Composition state) are written in order — intent record, accounting record, outcome — never atomically, and the failure path of the Cross-store consistency under partial failure edge case runs on any partial failure between them. Because Selective Disclosure is irreversible and synchronous rollback is unavailable, the orphan state — a disclosure record with no ledger event — is reachable under the prescribed design, durably, until compensation lands. The honest claim therefore splits:
- Safety — no unsurfaced orphan. At every instant the records answer whether an orphan exists (enumerate the Selective Disclosure store against the ledger.disclosed events through the substrate’s read surface); its surfacing is bounded, not instantaneous. Surfacing has two mandatory legs: a partial failure that returns surfaces the orphan as a high-priority compliance finding in the same outcome that returns rejected(recording-failure(outcome)); a partial failure that cannot return — a process crash between the two truth-bearing writes — is caught by the mandated reconciliation scan (the same orphan enumeration, run at restart and on reconciliation_cadence; see the partial-failure edge case), so no orphan survives unsurfaced past the scan bound, disclosed_at + disclosure_completion_bound + reconciliation_cadence (Configuration). Never a quiet inconsistency. A ledger.disclosed event naming a disclosure_id absent from the Selective Disclosure store (the inverse orphan) is unreachable through this composition’s wiring. Recovered bindings remain distinguishable from clean ones via the cascade_recovery marker on the compensating event.
- Liveness — every orphan is eventually bound. The mandated compensation (retry the failed AuditTrail.record_action — inside the invocation under the discloser’s credential for at most outcome_retry_attempts, by the scan under the recovery identity thereafter, one cycle at a time until it lands, never both: one writer per record, serialized on disclosure_id, partial-failure edge case) restores the bijection: an orphan is a surfaced transient under compensation, never a steady state of a conforming implementation. Formally: Orphan(d) ↝ Bound(d) under weak fairness on the retry — the eventuality lives in the implementation’s retry obligation; the formal model carries its enabledness half (the retry action is enabled in exactly the orphan configuration, so no orphan state is a dead end). The retry discharges transient failures (recording-failure); a deterministic rejection of the outcome write cannot land by repetition, and the two deterministic arms part ways: invalid-credential — first detectable at the intent record, before anything commits, surviving at the outcome record only as a mid-flight revocation or expiry — is cured by re-attestation under the deployment’s declared recovery identity; invalid-request is a function of payload or policy that no re-attestation touches, and its retention-configuration source leaves the event appended (bound, with the retention gap the substrate’s own), while its payload source is foreclosed by step 1’s sizing of the maximal outcome-and-compensation envelope and, where a configured payload_cap that disagrees with the wired Event Log’s defeats that, lands as the terminal binding-unbindable verdict through a ledger.disclosure_unbindable marker (the partial-failure edge case). So the eventuality is Orphan(d) ↝ Bound(d) ∨ Unbindable(d): every orphan reaches a lawful terminal state, and the unbindable one is a deployment-configuration finding with a records-alone verdict rather than a permanent transient. The re-attestation is therefore the backstop for a committed disclosure’s owed audit event — never, as the ordering once made it, the landing for an act committed on an unverified actor claim, since the discloser’s own authentication is already witnessed by the intent record (see the partial-failure edge case) — the eventuality holds across both failure classes, by retry on one and by recovery-attestation on the other.
- Retention horizon — the bijection holds modulo honest destruction. ledger_retention_policy governs disclosure events too, and Selective Disclosure records are never removable (Selective Disclosure Invariant 6), so when a ledger.disclosed event reaches its retention end and is lawfully purged (Audit Trail cascade-on-purge, honest destruction per Audit Trail Invariant 8), its disclosure record survives the event — permanently, and conformingly. This is not an orphan and not a binding-gap: the purge leaves a Purged retention record that distinguishes destroyed from missing, and Verify Ledger reports it as binding = binding-purged (see step 2). The bijection claim is therefore scoped: it holds unconditionally over disclosure events inside their retention lifetime; past the horizon it degrades to every disclosure record is bound to exactly one ledger event or to that event’s honest-destruction record. Deployments whose disclosure-accounting horizon must outlast the ledger policy align the two policies in ledger_retention_policy (see the Retention of the disclosure-accounting store edge case).
This is the load-bearing claim and the formal-model subject — the model covers both arms, the clean ordered sequence and the compensated partial failure; it mirrors the shape of Audit Trail Invariant 4 (cascade coordination on purge — one act driving several stores to a coherent end state, with a reconciliation that closes what a partial failure leaves) at the disclosure boundary. Rests on: Selective Disclosure Invariants 1 and 6 (record immutability, append-only durability), Audit Trail Invariants 1 (attribution coverage), 3 (integrity coverage — the seal over the disclosure event), 5 (append-only durability, transitively over Event Log), and 8 (honest destruction — the retention-horizon arm’s distinguishability), the compensation protocol of the Cross-store consistency under partial failure edge case, and Configuration’s reconciliation_cadence inequality (the liveness arm’s bound).
Invariant 2 — Verifiable partial disclosure (conditional on the declared substrate capability). The antecedent is stated inside the invariant rather than as an after-the-fact weakening, because partial-verifiability is a present-or-absent capability of the configured mechanism, not a property that holds in every deployment. When tamper_evidence_supports_partial_disclosure = true: any subset disclosed via Disclose Subset can be independently verified — by a party holding only the disclosed entries, the verification_bundle, and the published ledger_seal_reference — as authentic and derived from the ledger (Verify Disclosure returns authentic per entry), while the undisclosed remainder stays undisclosed and its integrity uncompromised (confidentiality_preserved = true, a self-reported property of the bundle’s mechanism — see Verify Disclosure). When the capability is false: the weaker whole-ledger property holds instead — a recipient can verify only by verifying the entire ledger seal, which requires access to the whole ledger and breaks the confidentiality half — and Disclose Subset’s bundle declares the degradation (the Whole-ledger-only tamper evidence edge case). In neither case does this composition mandate a mechanism: the obligation is behavioral (Merkle inclusion proofs, accumulators, signed packages, or equivalent are realizations). Rests on: Audit Trail Invariant 3 (integrity coverage modulo unsealed tail) and Invariant 7 (verification asymmetry — the verifier presents the records), the declared tamper_evidence_supports_partial_disclosure capability, and the composition-introduced subset-proof surface (Verify Disclosure; see the Subset proofs edge case).
Invariant 3 — Immutable, attributed, retention-governed ledger. Every ledger entry (transaction, disclosure intent, or disclosure outcome event) is append-only and totally ordered (Event Log), attributed to a verified actor (Actor Identity), tamper-evident under the configured seal cadence (Tamper Evidence), and placed under retention at write time with honest cascade-on-purge (Retention Window). No ledger entry is modified or reordered after commit. Rests on: the Audit Trail substrate’s Invariant 1 through 4, 6, 8, holding transitively over Event Log, Actor Identity, Tamper Evidence, and Retention Window.
Invariant 4 — No-disclosure-unrecorded, structurally closed. Selective Disclosure’s Invariant 5 (no-disclosure-unrecorded), which that atom can only state as an integration obligation, is structurally enforced at this layer: Disclose Subset is the composition’s only disclosure surface and it always writes both the Selective Disclosure record and the ledger disclosure event before returning success. A disclosure performed outside the composition is outside this composition’s scope (and a system-conformance failure against Selective Disclosure Invariant 5); a disclosure performed through this composition cannot escape accounting. Rests on: Invariant 1 and the action wiring.
Invariant 5 — Constituent invariants preserved. Selective Disclosure Invariant 1 through 6 hold over the disclosure store; Audit Trail Invariant 1 through 8 hold over the substrate, and transitively all Event Log, Actor Identity, Tamper Evidence, and Retention Window invariants hold over their instances. The composition weakens no constituent invariant.
Invariant 6 — Authentication precedes commitment. No constituent call that commits is reached on any path before this composition’s caller has presented a credential that validates against the actor registry’s public material for the supplied actor_ref. For Disclose Subset the intent record is the mechanism: it is an AuditTrail.record_action call (ledger.disclose_intended), the substrate validates the credential inside it, and it stands before SelectiveDisclosure.record — the irreversible write, since Selective Disclosure records are never removable (that atom’s Invariant 6). A permanent disclosure-accounting record is therefore never created on an unverified actor’s asserted authority; invalid-credential is a pre-state refusal with nothing recorded in either store, not a fault discovered over a completed and unrecallable disclosure. For Record Entry no second mechanism is needed and none is added: its single AuditTrail.record_action is the load-bearing write. The verification queries take no credential and assert no actor’s authority.

What this does and does not establish: a successful validation establishes that material matching the actor’s registered verifier was presented at that instant. It does not establish that the presenter is that actor (a stolen credential validates), that the presentation is bound to a channel or session, or that it cannot be replayed. And it establishes nothing whatever about the other three references a disclosure carries — not the subject_ref, whose correspondence to a real party is the host’s assertion and is already externally cleared; not the recipient, who is never authenticated here (the verification queries are described as runnable by a recipient, which is a capability statement, not an identity claim); and not the holder of the authority.reference, whose validity is likewise an external check. No guarantee of this composition asserts otherwise, and this invariant must not be read as widening any of them. Rests on: Audit Trail’s record_action and the Actor Identity attestation reached through it. Defended in-line: the ordering is visible in Disclose Subset’s step list, and Generation acceptance check 5 tests it from the records alone.

Examples

Walkthrough — broker-dealer trade-confirmation ledger under SEC Rule 17a-4

A registered broker-dealer deploys this composition as the trade-confirmation ledger for one trading desk. Configuration: ledger_retention_policy = sec_17a4_6yr (encoding the six-year floor with the first two years immediately accessible), seal_cadence = per-event (each entry independently verifiable the moment it lands, so any subset disclosed later carries a valid partial proof), tamper_evidence_supports_partial_disclosure = true (the substrate’s Tamper Evidence mechanism — a per-ledger Merkle tree — can produce an inclusion proof for any named subset).

Three trades are recorded. For each executed trade, the desk calls record_entry(transaction_data = {symbol, qty, price, counterparty, …}, actor_ref = "trader-d12", credential = <trader_cred>). The composition calls AuditTrail.record_action(action_ref = ledger.entry, actor_ref = "trader-d12", <trader_cred>, data = {transaction_data, recorded_at}) three times → {entry_id = "ev_5001"}, {entry_id = "ev_5002"}, {entry_id = "ev_5003"}. Each entry is now an immutable, attributed, per-event-sealed, retained ledger event. No disclosure has occurred, so disclosure_to_event is empty.
An examiner requests one trade. A FINRA (Financial Industry Regulatory Authority) examiner requests the confirmation for the single trade recorded at ev_5002 — and only that trade; the desk’s other positions are outside the examiner’s scope. The compliance officer calls:
```
disclose_subset(
  disclosed_entry_ids = {"ev_5002"},
  subject_ref = "account-7731",
  recipient = "FINRA-exam-2026-Q2",
  scope = "trade-confirmation:single-trade:ev_5002",
  authority = { type: "regulatory", reference: "SEC Rule 17a-4(b)(4) — examiner production" },
  actor_ref = "compliance-c4",
  credential = <compliance_cred>
)
→ { disclosure_id = "disc-2210", event_id = "ev_5004", verification_bundle = <Merkle inclusion proof for ev_5002> }
```
The intent record goes first: AuditTrail.record_action(action_ref = ledger.disclose_intended, actor_ref = "compliance-c4", <compliance_cred>, data = {disclosed_entry_ids: {"ev_5002"}, subject_ref: "account-7731", recipient, scope, authority.type, authority.reference, recorded_at}) → ev_5003. That call is where compliance-c4’s credential is validated, so nothing has been written to either store if it does not — the permanent disclosure-accounting record below is never created on an unverified claim. Then the binding fires: SelectiveDisclosure.record(...) → disc-2210; then AuditTrail.record_action(action_ref = ledger.disclosed, actor_ref = "compliance-c4", <compliance_cred>, data = {intent_event_id: "ev_5003", disclosure_id: "disc-2210", disclosed_entry_ids: {"ev_5002"}, subject_ref: "account-7731", recipient, scope, authority.type, authority.reference, disclosed_at, recorded_at}) → ev_5004; then disclosure_to_event["disc-2210"] = "ev_5004". The outcome event names its intent event, which is what lets an auditor confirm from the records alone that the disclosing actor was authenticated before the disclosure existed. The act of disclosing is now itself an immutable, attributed, sealed ledger entry. The verification_bundle is the Tamper Evidence inclusion proof for ev_5002 against the published ledger seal — and for ev_5002 only.
The examiner independently verifies the disclosed trade. The examiner holds the disclosed entry payload (the ev_5002 confirmation), the verification_bundle, and the broker-dealer’s published ledger_seal_reference (the Merkle root, anchored to an RFC 3161 (the Internet standard for trusted time-stamping) Time-Stamp Authority (TSA) — a trusted third party that signs proofs of when data existed). The examiner — without any access to ev_5001 or ev_5003 — runs verify_disclosure(disclosed_entries = [ev_5002 payload], verification_bundle, ledger_seal_reference):
- entries: [{entry_id: "ev_5002", authenticity: authentic}] — the inclusion proof checks against the root, so the disclosed trade is a genuine, unaltered ledger entry.
- confidentiality_preserved = true — the inclusion proof reveals sibling hashes but not the contents, count, or position of ev_5001 / ev_5003.
- overall_verdict = disclosure-verified.
The examiner trusts the trade without trusting the broker-dealer and without seeing the rest of the book. This is Invariant 2 (verifiable partial disclosure) in operation.
A compliance auditor verifies the accountability side. Separately, an internal auditor with access to the composition’s stores asks: was this disclosure recorded and attributed? The auditor calls verify_ledger(disclosure_id = "disc-2210", original_event_payloads):
- binding = bound — the ledger.disclosed event ev_5004 carries data.disclosure_id = "disc-2210", confirmed by the substrate read (Invariant 1); the disclosure_to_event index supplied the accelerating hit.
- attestation_verification = verified — read_record("ev_5004") names its position and covering range, the auditor’s original_event_payloads supplies every payload in that range keyed by sequence_number, and AuditTrail.verify_record("ev_5004", <the range's payloads>) confirms the disclosing officer’s credential and the seal over the disclosure event.
- retention_state = Retained.
The two verification surfaces answer two different questions: Verify Disclosure (anyone holding the bundle) proves the subset is genuine; Verify Ledger (an auditor with the stores) proves the disclosure was accounted. Neither constituent answers either alone.

Healthcare — accounting of disclosures under HIPAA §164.528

A covered entity keeps each patient’s billing-disclosure ledger in this composition. Every time PHI (Protected Health Information) is disclosed to a payer, a public-health authority, or a business associate, the entity calls Disclose Subset naming the disclosed billing entries, the recipient, and the authority ({ type: regulatory, reference: "HIPAA §164.512(b)" } for public-health reporting; { type: consent, reference: "<consent-id>" } for patient-authorized sharing). When the patient exercises their §164.528 right to an accounting of disclosures, the entity calls read against the Selective Disclosure store filtered by subject_ref = <patient>: the result is every disclosure — date, recipient, scope, authority — drawn from the records alone. Because each disclosure is also a ledger.disclosed event (Invariant 1), the accounting is itself immutable, attributed, and tamper-evident — a property §164.528’s accounting obligation needs but the plain Selective Disclosure atom cannot supply alone.

Clinical-trial submission ledger under 21 CFR Part 11

A sponsor records each electronic submission to a regulator as a Record Entry in a 21 CFR Part 11 submission ledger (attributable, contemporaneous, original, accurate — ALCOA — satisfied by the Audit Trail substrate). When the sponsor discloses a defined subset of the submission record to an inspector or an IRB (Institutional Review Board), Disclose Subset produces both the accountable disclosure record and the partial-disclosure proof for exactly the disclosed documents, leaving the remainder of the submission sealed and unrevealed. The inspector verifies the disclosed subset against the published seal; the sponsor’s disclosure log answers what was shown, to whom, under what authority from the records alone.

Rejection path — empty or unknown subset

A caller attempts to disclose with no entries: disclose_subset(disclosed_entry_ids = {}, …) → rejected(invalid-request) at step 1; nothing is written to either store. A caller names an entry id that is not a ledger transaction entry — a fabricated id, or the event_id of a ledger.disclosed event rather than a ledger.entry event: disclose_subset(disclosed_entry_ids = {"ev_5004"}, …) → rejected(unknown-entry) naming ev_5004 (it is a disclosure event, not a transaction entry); nothing is written. The membership test (every id resolves to a ledger.entry event) runs before the irreversible Selective Disclosure write, so an invalid subset never produces a disclosure-accounting record.

Rejection path — ledger write fails after the disclosure record commits (the orphan)

The compliance officer calls Disclose Subset with a valid subset. Step 3 succeeds: SelectiveDisclosure.record(...) → disc-2211 is durably written (Selective Disclosure records are immutable once committed). Step 4 fails: the pre-check under the per-disclosure_id section finds no ledger.disclosed event naming disc-2211, and AuditTrail.record_action(ledger.disclosed, …) returns recording-failure(step-3) (the log’s store is briefly unreachable) on the first attempt and on each of the outcome_retry_attempts re-attempts. The composition returns rejected(recording-failure(outcome)) — the position telling the officer the disclosure record exists and the action must not be re-run — and yields the orphan to the scan. The result is an orphan: a Selective Disclosure record (disc-2211) with no ledger.disclosed event (and consequently no disclosure_to_event entry — the missing event is the orphan’s defining lack; the index merely reflects it). This is exactly the orphan Invariant 1’s safety arm requires to be surfaced (never silent) and its liveness arm requires to be eventually bound; the Cross-store consistency under partial failure edge case governs its compensation (the scan retries the audit write under the recovery identity once the record is older than disclosure_completion_bound, one cycle at a time until it lands; surfaces the orphan to the compliance dashboard as a high-priority finding; marks the recovered event cascade_recovery = true). The TLA+ (Temporal Logic of Actions — a formal specification language for concurrent and distributed systems) model covers this compensated path mechanically, and its buggy twin demonstrates that the same sequence without surfacing and compensation is reachably unsafe — see the Ledger’s formal: line and the commit that landed the model.

Retention horizon — a disclosure event reaches its lawful end

Years later, the ev_5004 disclosure event from the walkthrough reaches the end of ledger_retention_policy and is lawfully purged (Audit Trail cascade-on-purge): its payload — data.disclosure_id included — is unreadable, and the substrate’s destruction record keeps only (ev_5004, a_5004), off which action_ref = ledger.disclosed and the discloser still read. The Selective Disclosure record disc-2210 survives — its store is not governed by that policy — and so does the composition’s own index entry disclosure_to_event[disc-2210] = ev_5004, the purged half that is truth-bearing under the durability obligation (Composition state). An auditor later calls verify_ledger("disc-2210", …): the rebuild read finds no live ledger.disclosed event, the index entry resolves ev_5004 to a Purged retention record and a destruction record whose attestation names ledger.disclosed, and the action returns binding = binding-purged, attestation_verification = unverifiable(purged), retention_state = Purged — honest destruction, distinguishable from a binding-gap, exactly Invariant 1’s retention-horizon arm. Nothing is surfaced as a finding; nothing is wrong.

Regulated adversarial scenarios

Three scenarios the composition must survive in regulated contexts:

Regulator audit — “produce the accounting of disclosures, and prove each is genuine” (HIPAA §164.528 / SEC Rule 17a-4).

A regulator queries the disclosure-accounting surface for a subject (a patient under §164.528, an account under 17a-4). The system calls read against the Selective Disclosure store filtered by subject_ref, returning every disclosure — date, recipient, scope, authority. For any disclosure the regulator wishes to verify, the system calls verify_ledger(disclosure_id, original_event_payloads):

binding = bound: by Invariant 1 (binding bijection), every disclosure record produced by the composition has exactly one corresponding ledger.disclosed event. A disclosure cannot appear in the accounting without its immutable, attributed, sealed ledger event.
attestation_verification = verified: by Invariant 3 (immutable, attributed, retention-governed ledger), the disclosure event is attributed to the disclosing actor’s verified credential and covered by a seal.
retention_state = Retained (or Purged with an honest retention record for lawfully expired entries).

The accounting and its proof come from the records alone. Invariants 1, 3, and 4 are the structural basis; no developer narration is required.

Disputed transaction / data-subject request — “prove this disclosed trade subset is authentic without revealing my other trades” (GDPR Article 15).

A data subject (or a counterparty) was shown a subset of the ledger and challenges it: either (a) the disclosed entries were not genuine ledger entries, or (b) showing them exposed or compromised the undisclosed remainder. The recipient — holding only the disclosed entries, the verification_bundle, and the published ledger_seal_reference — runs Verify Disclosure:

Claim (a): per-entry authenticity = authentic, resting on Invariant 2 and Audit Trail Invariant 3 (integrity coverage). The inclusion proof checks each disclosed entry against the published seal; an altered or fabricated entry returns altered or not-in-ledger. The recipient verifies authenticity without trusting the discloser — the proof is self-contained against the seal (conditional on the seal-publication obligation: the recipient’s ledger_seal_reference must be independently obtained, or the proof is self-contained against whatever ledger the discloser handed them — see the externally-clearable checks).
Claim (b): confidentiality_preserved = true, resting on Invariant 2’s zero-knowledge-of-complement obligation. The bundle reveals nothing about the count, content, or position of the undisclosed entries beyond what the published seal inherently commits to. The GDPR Article 15 right to one’s own disclosed data is satisfied without a parallel breach of every other data subject whose entries share the ledger.

The disputed claim has no structural basis on the authenticity axis: claim (a) is checkable by the challenger themselves against the published seal (Invariant 2, authenticity half). Claim (b) — confidentiality of the remainder — rests on the audited mechanism’s zero-knowledge-of-complement property: confidentiality_preserved is self-reported, and its independent assurance is the deployment’s security review of the mechanism (the externally-clearable check), not a verdict the challenger recomputes. The spec does not overclaim claim (b) as recipient-recomputable.

Breach or incident investigation — “is every disclosure accounted, and is any disclosure orphaned?”

An incident responder suspects that a disclosure occurred without being recorded, or that a disclosure record was tampered with. The responder runs the binding-bijection audit (Invariant 1) across the two stores:

For every Selective Disclosure record produced by the composition, confirm a ledger.disclosed event exists whose data.disclosure_id points back (the authoritative substrate read; disclosure_to_event accelerates it as a derived index). A disclosure record with no such event is an orphan — the partial-failure signature, which Invariant 1’s safety arm guarantees is already surfaced as a high-priority finding (a recorded disclosure whose immutable ledger proof is missing); an orphan found here that was not surfaced is a conformance failure, not a transient. A recovered binding is distinguishable by its cascade_recovery marker.
For every ledger.disclosed event, confirm its data.disclosure_id resolves to a Selective Disclosure record. A ledger.disclosed event naming a disclosure_id absent from the disclosure store is the inverse orphan.
For the disclosure events themselves, walk the Audit Trail seal store in sealed_at order (inherited from the substrate’s breach-forensics scenario): the most recent seal that verifies end-to-end and the first that returns failed-verification(seal-proof-invalid) bound the forensic window during which a disclosure event may have been tampered with.

The binding bijection is what makes “every disclosure is accounted” a checkable property rather than a hope; the orphan is exactly the reachable bad state the formal model rejects.

Generation acceptance

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

Record checks

These checks are answerable by reading the composition’s records (including the Audit Trail substrate). Every “every ledger.disclosed event” or “every ledger.entry event” below is obtained by the declared route — the open-upper-bound sequence-range read with the action_ref selection made composition-side (Composes) — never by asking the substrate for a query it routes to Reverse Index:

Every disclosure is doubly recorded and bound. For every Selective Disclosure record produced by this composition, confirm a ledger.disclosed event exists in the Audit Trail substrate whose data.disclosure_id matches — the authoritative check is the substrate read; disclosure_to_event is a derived index that accelerates it and must agree with it (a stale or missing index entry against an existing event is a rebuild trigger, not a conformance failure). Conversely, for every ledger.disclosed event, confirm its data.disclosure_id resolves to a Selective Disclosure record. A disclosure record with no matching live ledger.disclosed event resolves to exactly one of four classes: the composition’s own index binds it to a purged event whose Purged retention record attests honest destruction (binding-purged — lawful under Invariant 1’s retention-horizon arm, not a finding); a ledger.disclosure_unbindable marker names it (binding-unbindable — a deployment-configuration finding with a terminal verdict); an orphan under active compensation (Invariant 1’s named transient); or a conformance failure. The enumeration runs between two edges (Configuration, disclosure_completion_bound): a disclosure record whose disclosed_at is younger than the bound may belong to an invocation still between its two truth-bearing writes and is inconclusive, not an orphan; one older than ledger_retention_policy’s horizon with no live event resolves through the index’s purged half or, where that entry is lost, to the index-loss finding — never to an orphan. The orphan/failure detection is traversal-clearable — the record sets answer it. Whether a detected orphan was surfaced and is under active compensation is not clearable from these stores (the finding surface is handled at the observability layer; see the partial-failure edge case) — that half routes to the externally-clearable checks. Confirm also that every recovered binding carries cascade_recovery = true and no clean binding does. Invariant 1 (binding bijection, safety + liveness) is the contract.
Every disclosed subset is independently verifiable as authentic. For a disclosure whose verification_bundle and disclosed entries are presented (with the published ledger_seal_reference), confirm Verify Disclosure returns authentic per entry. A disclosed entry that returns altered or not-in-ledger is a conformance failure. The confidentiality half — that the bundle leaks nothing about the complement — is not clearable from this traversal: confidentiality_preserved is self-reported by the verification routine over the bundle the discloser produced (see Verify Disclosure), so complement-leakage is assessed by the deployment’s security review of the configured mechanism, listed under the externally-clearable checks below. Where the deployment declares tamper_evidence_supports_partial_disclosure = false, the degraded whole-ledger form is the acceptance bar instead (named in the Whole-ledger-only tamper evidence edge case), and the bundle says so. Invariant 2 (verifiable partial disclosure), authenticity half, is the contract.
The ledger is immutable, attributed, sealed, and retention-governed. For every ledger entry — transaction ledger.entry, disclosure intent ledger.disclose_intended, and disclosure outcome ledger.disclosed, the three classes Invariant 3 ranges over — confirm via the Audit Trail substrate that the event is append-only and totally ordered (Event Log), attributed to a verified actor (Actor Identity), covered by a seal per the configured cadence (Tamper Evidence), and under a retention record in Retained or Purged state (Retention Window). AuditTrail.verify_record returns verified (or failed-verification(purged) for lawfully expired entries, distinguishing destroyed from missing). Invariant 3 is the contract; it delegates to Audit Trail’s own six-check Generation acceptance bar over the substrate.
No disclosure escapes accounting. Confirm that Disclose Subset is the composition’s only disclosure surface and that it writes both records before returning success — so a disclosure performed through the composition cannot exist without its Selective Disclosure record and its ledger.disclosed event. (A disclosure performed outside the composition is a system-conformance failure against Selective Disclosure Invariant 5, named in the externally-clearable checks.) Invariant 4 (no-disclosure-unrecorded, structurally closed) is the contract.
Authentication precedence. For every ledger.disclosed outcome event in the trail, take its data.intent_event_id, resolve it to a ledger.disclose_intended event, and confirm that event precedes it in the Event Log’s own order and carries the same invocation parameters. Because the substrate validates the caller’s credential against the actor registry inside every record_action, the named intent event is the records-alone proof that the disclosing actor was authenticated before the permanent disclosure record was created — which is what makes Invariant 6 verifiable rather than asserted. The join must be by intent_event_id and nothing weaker. Disclose Subset is repeatable with identical parameters — the same subject disclosed to the same recipient under the same scope any number of times, which is exactly what a disclosure accounting is built to record — so a join over subject_ref, recipient, scope or actor_ref does not distinguish invocations, and one stale intent event would satisfy the check for an unbounded number of later disclosures. Nor may the join run through disclosure_to_event: that is a derived index carrying no consistency claim and losable by design, so a check resting on it would live in evictable state.

For a compensated outcome event — one carrying cascade_recovery = true, attested under application_actor_ref (Configuration) — compare the intent event’s actor against the original discloser preserved in the sealed data (disclosed_by), never against the attesting identity; expect the original intent_event_id where the scan could pair it, or intent_event_candidates naming every ledger.disclose_intended event that matches where it could not (the same parameters, the same discloser, recorded_at equal to the record’s disclosed_at); and confirm a ledger.recovery_intended record naming the same disclosure_id precedes it. A compensated event carrying candidates is verified against each candidate — every one must precede it and name the same discloser — and its disclosed_entry_ids is present only where every candidate carries the same set (otherwise the event carries entry_set_unresolved = true and no bundle is reissuable for it). Without this carve-out the check condemns every event the composition’s own compensation path produces.

An intent event with no outcome event is not a failure, and resolving which case it is needs the Selective Disclosure store, not the trail alone: it names an invocation that committed nothing, one that committed and has not yet recorded, or one that died between. Enumerate intent events through the same ledger-route read the two existing orphan enumerations use — no new read surface is required.

Horizon, and one window inside it. This check is answerable only within the retention horizon: the disclosure-accounting retention rule preserves data.disclosure_id past a purge but not intent_event_id, and not the intent event itself, so for disclosures behind the horizon the determination is unverifiable(purged-horizon) — never a conformance failure. The same verdict covers a narrower window that sits inside the horizon, and it must, or the check convicts a conforming deployment: both events are placed under retention by their own record_action at write time under one policy, so the intent event’s retention_until precedes the outcome event’s by the inter-write interval, and a purge sweep landing between them destroys the intent while the outcome is still live. An outcome event whose intent_event_id resolves to nothing is therefore unverifiable(purged-horizon) too — the resolution failing is not evidence the intent record never existed. Without this clause the check would convert lawful, honest destruction into a finding, which is the defect Invariant 1’s own retention-horizon arm exists to prevent.

Constituent Generation acceptance bars. Verify each constituent’s own Generation acceptance bar over its respective store: Selective Disclosure’s six checks (record completeness, field completeness, immutability, authority-type enforcement, subject-history queryability, temporal soundness) and Audit Trail’s six checks (all four audit questions answerable, all eight composition-level invariants verifiable, each constituent atom’s bar satisfied, forensic window boundable, honest destruction distinguishable, composing patterns identifiable). The composition’s invariants depend on the correctness of the constituents’. Invariant 5 is the contract.

External checks

These audit questions arise around this composition but cannot be answered from the composition’s records alone:

Whether the orphan-surfacing and compensation discipline is operating. Invariant 1’s safety arm requires every orphan to be surfaced as a high-priority finding in the same outcome that returns rejected(recording-failure(outcome)), and its liveness arm requires the scan to run, cycle after cycle, until the compensating event lands. This composition’s records prove an orphan exists (traversal check 1) and prove a recovery happened (cascade_recovery = true), but whether a currently-open orphan has been surfaced to the compliance dashboard and is under active retry — and whether the reconciliation scan actually runs at restart and on reconciliation_cadence, on an instance that refused to start on a Configuration triple failing the liveness inequality — is a property of the deployment’s finding/alerting surface — handled at the observability layer (see the partial-failure edge case), assessed by the deployment’s operational review, not clearable from this composition’s stores.
Whether the asserted authority was valid. This composition records the disclosing party’s asserted authority ({type, reference}) and makes the assertion immutable and attributed. It does not verify that a referenced Consent was in force, that a referenced Legal Hold was Active, or that a cited regulation genuinely permitted the disclosure at the time. Authority legitimacy is a composing Consent / Permissions concept (and, for legal-hold authority, a Legal Hold concept) — named as a peer in Edge cases. This composition makes the assertion auditable; it does not adjudicate it.
Whether the disclosure was permitted. This composition is not the authorization layer that decides whether a given party may disclose a given subset to a given recipient. That gate is Consent / Permissions, a composing peer. This composition records and proves disclosures that occur; it does not authorize them.
Whether transaction_data is accurate or corresponds to a real-world transaction. This composition records transaction_data as an opaque payload and seals it. It does not validate that the payload matches an external trade-confirmation, billing event, or submission. The host system owns the correspondence between the ledger entry and the real-world transaction it represents.
Whether disclosed_entry_ids genuinely pertain to subject_ref. This composition records the disclosing party’s asserted subject_ref and the entry set, and makes both immutable and attributed; but transaction_data is opaque, so this composition cannot validate from its records that the disclosed entries are in fact the subject’s — the correspondence is the host’s assertion, mirroring the transaction_data bullet above. Whether a disclosure was filed under the right subject (and therefore appears in the right party’s accounting) is cleared by the host’s tagging discipline and the deployment’s review of it, not from this composition’s records. See the Subject correspondence is the host’s assertion edge case.
Whether the tamper_evidence_supports_partial_disclosure capability is genuinely met by the configured mechanism — including complement confidentiality. This composition takes the capability as a deployment-declared boolean. Whether the deployment’s actual Tamper Evidence mechanism can produce sound, complement-hiding partial proofs — i.e., whether confidentiality_preserved, a value the verification routine self-reports over the discloser-produced bundle, deserves trust, and whether any bundle leaks the count, content, or position of undisclosed entries — is a property of that mechanism’s cryptographic construction, assessed by the deployment’s security review — not clearable from this composition’s records. This check carries the confidentiality half of Invariant 2 (the authenticity half is traversal-clearable, check 2 above).
Whether the published ledger_seal_reference is singular and independently obtainable — and the verifier independently buildable. Verify Disclosure’s “without trusting the discloser” property holds only if the recipient’s seal reference is the same one the ledger’s other observers hold, obtained through a channel the discloser does not unilaterally control (a time-stamping authority, a regulator filing, a public anchor). A discloser who maintains a forked side-ledger and hands the recipient the fork’s root passes every records-level check against that fork — split-view protection is a property of the deployment’s seal-publication discipline, not of this composition’s records. The same deployment obligation covers verifier independence: the configured mechanism’s bundle format must be documented or standard enough that an independent party can implement or obtain a verifier without relying on the discloser’s code.

Non-goals and edge cases

This composition does not authorize disclosures — Consent / Permissions is the authorization peer. This composition records and proves that a disclosure occurred and was accounted; it does not decide whether the disclosure was permitted. The authorization gate — may this actor disclose this subset to this recipient under this basis? — is a composing Consent / Permissions concept, run before Disclose Subset. This composition’s authority field records the asserted basis and makes the assertion immutable and attributable; validating that the basis was genuinely in force is the authorization peer’s obligation (see the externally-clearable checks). A deployment composing this composition + Consent/Permissions gets both the gate (may I?) and the accountable, verifiable record (I did, here is the proof).
This composition does not perform, redact, or transmit the disclosure — the Selective Disclosure boundary holds. Selective Disclosure deliberately does not fetch subject data, apply redaction, or route transmissions, and this composition inherits that boundary. This composition records that a subset was disclosed and produces the proof that the disclosed subset is genuine; it does not retrieve the underlying payloads, decide what falls within a scope, or deliver anything to the recipient. The verification_bundle is a tamper-evidence artifact, not a data-delivery channel — the disclosed payloads themselves travel by whatever transmission mechanism the deployment uses, outside this composition.
Whole-ledger-only tamper evidence (Invariant 2 degradation). Where the configured Tamper Evidence mechanism cannot produce a partial proof for a named subset (tamper_evidence_supports_partial_disclosure = false) — for example, a single whole-ledger hash with no inclusion-proof structure — Disclose Subset still records the accountable disclosure and the ledger.disclosed event (the binding bijection, Invariant 1, is unaffected), but its verification_bundle degrades: a recipient can verify the disclosed subset only by verifying the whole ledger seal, which requires access to the entire ledger and therefore breaks the confidentiality half of Invariant 2. The composition does not silently weaken the guarantee; it surfaces the degradation in the bundle, and Invariant 2 names this explicitly. A deployment that requires verifiable partial disclosure must configure a Tamper Evidence mechanism with inclusion-proof capability (Merkle tree, accumulator, or equivalent). The degraded path’s verdicts are pinned, not implementer-chosen: Verify Disclosure over a degraded bundle returns per-entry authenticity = unverifiable(whole-ledger-required) unless the verifier is actually given the whole ledger; confidentiality_preserved = false (whole-ledger verification inherently exposes the remainder); overall_verdict = disclosure-unverified(degraded-bundle). A verifier that waves a degraded bundle through as disclosure-verified is non-conforming.
Subset proofs are a composition-introduced surface today — a forthcoming Subset Proof atom is the eventual home. The verification_bundle and Verify Disclosure are introduced at this composition layer; they are not delegated to a constituent action, because none exists. The Tamper Evidence atom’s verify checks a whole sealed record-set, and the Audit Trail substrate’s verify_record checks a single whole event — neither exposes an action that produces or checks an inclusion proof for a named subset of a sealed range. This composition supplies that surface itself, invoking the configured Tamper Evidence mechanism’s inclusion-proof capability (declared via tamper_evidence_supports_partial_disclosure) over the substrate’s seal material. This invocation class — neither a substrate action call nor a query — is the mechanism-capability residual the Execution Contract names and permits: see execution-contract.md §Substrate composition invocation, Mechanism capability invocation is the named residual, which cites this bundle as the worked case and states the conditions this composition meets (the capability is deployment-declared and verified by an externally-clearable check; the consuming surface is composition-introduced and specified at this layer; the invocation is logic-confinement-clean — configured material invoked at a named step, never crypto improvised inside core logic). The Contract also names the construct’s exit: a recurring mechanism-capability surface is a not-yet-extracted-atom signal, and the forthcoming Subset Proof atom remains this composition’s retirement path. The honest boundary: this composition requires the capability and owns the surface; it does not pretend a constituent action produces the bundle. A forthcoming Subset Proof (selective tamper-evidence) atom — the freestanding concept “prove a named subset of a sealed set is included, without revealing the complement”, the verification dual of Tamper Evidence’s whole-set seal — would let this composition delegate the bundle to a named constituent surface and let Invariant 2 rest on that atom rather than on a deployment-declared mechanism capability. Until it lands, the surface is emergent here and the capability is the deployment’s to supply; mechanism-neutrality is preserved either way (the atom would itself be mechanism-neutral, exactly as Tamper Evidence is). (Forthcoming — no live link; the atom is named on the roadmap, not yet authored.)
Cross-store consistency under partial failure. Every Disclose Subset writes an intent record to Audit Trail first, then Selective Disclosure, then the outcome record to Audit Trail (the two truth-bearing writes), then populates the disclosure_to_event derived index. An intent record with no outcome record is not itself a finding — it may name an invocation that committed nothing, one that committed and failed to record, or one that died between. Which case it is, is decided by the store-against-store enumeration keyed on disclosure_id, not by the intent record, and the limit is worth stating precisely because the opposite is easy to assume: the intent record deliberately carries no constituent-minted id (none exists when it is written), and Selective Disclosure records carry no intent reference, so the only join available between them is the parameter tuple — which check 5 establishes does not distinguish invocations, since Disclose Subset is repeatable with identical parameters. What the intent record does add is a durable, authenticated statement of what was attempted, which the scan reads alongside its enumeration; the compensation obligation itself is still decided by the enumeration, which is complete on its own. A failure after the Selective Disclosure write but before the Audit Trail write produces an orphan: a Selective Disclosure record with no ledger.disclosed event. Selective Disclosure records are immutable once committed, so synchronous rollback is not available — the orphan is reachable and durable until compensated, which is exactly why Invariant 1 is stated as safety + liveness rather than as an unconditional atomicity claim. The implementation must:

(a) Compensate with check-then-retry, between two edges, as the composition, behind a recovery record. The orphan enumeration — Selective Disclosure records with no ledger.disclosed event — runs at process restart and on reconciliation_cadence (Configuration) over records whose disclosed_at is older than disclosure_completion_bound (Configuration) — a younger record may belong to an invocation still between its step 3 and step 4, and compensating it would append a second event beside the invocation’s own — and inside ledger_retention_policy’s horizon: an older record with no live event is binding-purged through the index’s truth-bearing half, or the index-loss finding where that entry is gone, and is never compensated, since appending a fresh ledger.disclosed for a disclosure whose event was lawfully destroyed would manufacture the record the purge removed. Each cycle first runs disclosure_to_event’s full rebuild as a write — every live ledger.disclosed event’s data.disclosure_id → event_id into the index — so the half that will be truth-bearing after a purge is captured within one cycle of every event’s landing, before any purge can reach it (the Configuration inequality; Composition state). Before each compensation attempt, run the rebuild read — does any ledger.disclosed event already name this disclosure_id? — and append only if none does: a retry after a lost acknowledgment (the audit write landed but the success never returned) must not double-append, because the bijection says exactly one — two events naming the same disclosure_id is itself a conformance finding, surfaced by the same enumeration. Compensation attempts for one disclosure_id are serialized on the disclosure_section (Configuration) — a per-disclosure_id critical section the deployment supplies as a declared instance capability, attributed to no constituent, since neither Selective Disclosure nor Audit Trail declares a section spanning a call of the other — and the invocation’s own step 4, its pre-check and its read-back sit inside the same section, so a compensation and an invocation never interleave on one record. The scan takes the section before its pre-check and holds it through its compensating write; an invocation that lost its section re-takes it before its own pre-check, so neither can slip between the other’s look and its append. Never interleaving is not enough; never sequencing is the rule. An invocation that resumes after the scan compensated its record runs the same pre-check under the same section and adopts the scan’s event (Disclose Subset step 4); a scan run that finds a record’s section held — by a live invocation, or by the other scan run, restart beside cadence, one node beside another — skips the record until its next cycle rather than racing it, and waits at most disclosure_completion_bound for any holder, the lease’s length; and the look-then-append pre-check is re-read under the section, never before it. One writer per record: the invocation for at most outcome_retry_attempts, the scan thereafter, never both (§A compensator is exclusive). Every write the scan makes is attested under the composition’s recovery identity (application_actor_ref / application_credential, Configuration) — the discloser’s credential is not in hand — and is preceded by a ledger.recovery_intended record, data = {invocation_id, disclosure_id, intent_event_id | intent_event_candidates, recorded_at = now}, naming the record it is about to bind and the intent it pairs it to, so the trail shows the compensation was occasioned by the scan and not by a direct call. The pairing is by the records. The invocation passed its injected now to SelectiveDisclosure.record as disclosed_at and stamped the same reading as its intent event’s recorded_at (step 3), so the intent to pair with is the ledger.disclose_intended event carrying this record’s subject_ref, recipient, scope and authority, from the actor the record’s own store attributes it to where it does, whose recorded_at equals the record’s disclosed_at, and which no ledger.disclosed event already names. Exactly one → intent_event_id; more than one (the deployment’s clock resolution admitting two identical disclosures in one reading) → intent_event_candidates naming every match, never a choice — at most intent_candidates_cap of them (Configuration), past which the orphan is escalated as an unresolved finding and not compensated, so the compensating payload stays inside the envelope step 1 sized; none → the record was written by a direct constituent call outside this composition — a write-ownership finding, and no compensation is owed or may be written. What the compensating event carries is re-derived, never remembered: subject_ref, recipient, scope, authority and disclosed_at from the Selective Disclosure record; disclosed_by and disclosed_entry_ids from the paired intent event — and where the pairing is a candidate set whose members do not all carry the same disclosed_entry_ids, the compensating event omits the set and carries entry_set_unresolved = true, because a set no record determines is not one this composition may assert under seal; such a disclosure is bound but its bundle cannot be reissued. Transient failures (recording-failure(step-2 | step-3)) are retried by the scan one cycle at a time until the write lands — the liveness arm, bounded by the Configuration inequality; the step-4 arm and the retention-source invalid-request are found by the pre-check as already landed and are never re-appended. A deterministic rejection cannot land by repetition, and the two deterministic arms land differently because they are functions of different things. invalid-credential is a function of the credential, so re-attestation cures it: there the compensating record_action is attested by the recovery identity like every scan write, with the original actor_ref (as disclosed_by) and the original invocation’s intent_event_id carried inside the sealed data. Both matter: the first preserves who disclosed, the second keeps the intent-to-outcome join intact through compensation, so the authentication-precedence check does not condemn every recovered event. One intent record per invocation, carried through compensation unchanged — a compensating event must never mint a fresh one, which would make the recovery identity rather than the discloser the authenticated principal for a disclosure the discloser made. Note also that invalid-credential on this path is now narrowed to a mid-flight revocation or expiry between the intent and outcome writes. Recovered-event attribution is explicit, not ambiguous: the recovery identity attests the recording; the sealed payload preserves who disclosed.

invalid-request at the outcome write is a function of the payload or the policy, never of the credential, so re-attestation cannot cure it — and its two sources resolve differently. The retention-configuration source does not produce an orphan at all: the substrate places retention after it appends, so on that arm the ledger.disclosed event is already in the log, appended and attested, carrying data.disclosure_id; the check-then-retry above finds it, the binding is bound, and the unretained event is the substrate’s own reconciliation’s to repair — never re-appended here. The payload-size source is foreclosed at Disclose Subset step 1, which sizes the maximal outcome and compensation envelope — disclosed_entry_ids at disclosed_entry_ids_cap, intent_event_candidates at intent_candidates_cap — against the substrate’s payload_cap before the intent record, so what the intent passed the outcome and the compensating write pass too (§An outcome is sized before the intent). What remains is a configured payload_cap that disagrees with the wired Event Log instance’s own — the substrate’s declared deployment fault — observed as invalid-request on an outcome write whose intent write succeeded — and that residual gets a terminal verdict rather than an endless retry: the compensation records AuditTrail.record_action(action_ref = ledger.disclosure_unbindable, actor_ref = <recovery identity>, credential = <recovery identity>, data = {disclosure_id, intent_event_id, substrate_rejection, recorded_at = now}) — a small, bounded payload that fits any cap the outcome could have failed — and stops. Verify Ledger then reports binding = binding-unbindable(reason) (case (d)): the disclosure is accounted (the Selective Disclosure record stands), attested (the intent record witnesses the discloser), and its outcome could not be sealed at the configured cap — a conformance finding against the deployment’s Configuration, with a lawful terminal state for the record rather than an orphan that matches no recovery path. The marker is not absorbing: once the cap is corrected the compensation may land the ledger.disclosed event, and Verify Ledger prefers a live binding over the marker.

(b) Surface the orphan as a high-priority finding — in the same outcome that returns rejected(recording-failure(outcome)) when the failure returns, and via the mandated reconciliation scan (the orphan enumeration run at restart and on reconciliation_cadence) for the partial failure that cannot return: a process crash between the two truth-bearing writes produces an orphan with no outcome at all, and the scan is what bounds its silence (the safety arm’s surfacing bound, disclosure_completion_bound + reconciliation_cadence after the record’s disclosed_at).

(c) Once the compensating event lands, populate disclosure_to_event and mark the event with cascade_recovery = true so an auditor can distinguish a clean disclosure from a recovered one (the safety arm’s distinguishability clause). The finding store itself — the open → compensating → closed lifecycle of surfaced orphans, with its own state machine — is not this composition’s state: this composition mandates the surfacing obligation and proves recovery from its own records (cascade_recovery), but the finding/alerting surface is handled at the observability layer, mirroring how Audit Trail names attempted-but-not-committed actions as a Failed-Attempt Log composing concept rather than absorbing them (and verified accordingly: see the externally-clearable checks). This mirrors the shape of Audit Trail Invariant 4 (cascade coordination on purge) at the disclosure boundary: one act, several stores, a reconciliation that closes what a partial failure leaves. The TLA+ model covers both this compensated path (orphan reachable → surfaced → retried → bijection restored, with the recovered binding distinguishable) and the buggy twin’s sequential-without-compensation form, which the checker rejects on the silent orphan. Record Entry is a single substrate write and has no cross-store orphan of its own (an Audit Trail-internal partial-failure is the substrate’s Partial attestation on step failure edge case).
Concurrent disclosures. Distinct Disclose Subset calls — including two that name overlapping disclosed_entry_ids — do not conflict. Each produces its own disclosure_id, its own Selective Disclosure record and ledger.disclosed event, its own disclosure_to_event binding, and its own verification_bundle built against the ledger seal in force at its step 6; the binding bijection is per-disclosure local (the formal model proves it insensitive to disclosure count). There is no serialization constraint across distinct Disclose Subset calls, mirroring Selective Disclosure’s Concurrency edge case. A ledger.entry appended concurrently between two disclosures’ step-6 reads may move the seal, so two bundles over an overlapping subset can anchor to different seal points — each remains independently valid against the seal it names; the recipient verifies against the ledger_seal_reference paired with their bundle. Implementations serialize only each single store write (the per-disclosure_id Selective Disclosure write and the per-event_id audit append) and the per-disclosure_id section that Disclose Subset step 4 and the compensation share (see the partial-failure edge case), never across calls. A lawful purge can likewise race the action window: an entry that passes step 1’s membership read may reach its retention end and be purged before step 6 constructs its proof. The disclosure stands — the truth-bearing writes committed against a then-valid subset — and the bundle marks that entry unverifiable(entry-purged), exactly as a post-disclosure purge surfaces at verification time (the Disclosure of an entry that is later lawfully purged edge case).
At-most-once append under retry — Idempotent Reservation / Duplicate Prevention enrichment. This composition’s Record Entry is not idempotent: two calls with identical transaction_data produce two distinct ledger entries (the same non-idempotency Selective Disclosure and Event Log carry). For deployments where a retried Record Entry under a lost acknowledgment must not double-append a trade, compose Idempotent Reservation (or the Duplicate Prevention atom directly) as an optional enrichment over Record Entry, keyed on a caller-supplied idempotency token. This is named as enrichment, not a constituent: the immutable-attributed-disclosable-ledger guarantee does not depend on at-most-once append, and many deployments (where the host already de-duplicates upstream) do not need it.
Legal-hold suspension and defensible disposal of the ledger. When litigation or investigation requires suspending normal purge over the ledger’s retention, a Legal Hold pattern intercepts purge against the Audit Trail substrate’s retention records; Defensible Retention composes Legal Hold + Retention Window + Audit Trail into the hold-blocks-purge surface. This composition does not absorb this; a deployment composing this composition + Defensible Retention gets both the disclosable ledger and the hold-blocks-purge gate over its entries. The right-to-erasure-versus-retention collision (GDPR Article 17 versus a regulatory retention obligation) is likewise an Erasure Coordination composing concept, inherited from the Audit Trail substrate.
Disclosure of an entry that is later lawfully purged. A verification_bundle is issued at disclosure time against the seal then in force. If a disclosed entry’s underlying ledger event later reaches its retention end and is lawfully purged (Audit Trail cascade-on-purge), a subsequent Verify Disclosure against the original bundle may return unverifiable(entry-purged) for that entry — the seal can no longer be checked against a destroyed payload. This is the honest-destruction property (Audit Trail Invariant 8) surfacing at the disclosure-verification boundary, not a tamper finding: the ledger.disclosed accounting event persists under its own retention and Verify Ledger still proves the disclosure occurred. The disclosure proof is contemporaneous evidence; it is not a perpetual oracle over a record the retention policy has authorized destroying. The same honest-destruction property applies to the ledger.disclosed accounting event itself when it reaches its own retention end: its purge leaves the surviving Selective Disclosure record permanently unbound — lawfully, distinguishably (binding-purged, per Invariant 1’s retention-horizon arm and Verify Ledger step 2), never as a silent gap.
Retention of the disclosure-accounting store. This composition wires Retention Window (via the substrate) over the ledger events; it does not configure retention over the Selective Disclosure store, whose records are never removable by that atom’s own Invariant 6 — left alone, the disclosure-accounting store retains forever while its bound ledger events purge at ledger_retention_policy’s horizon (the mismatch Invariant 1’s retention-horizon arm makes lawful and distinguishable). A deployment whose disclosure-accounting horizon is itself regulated (HIPAA §164.528’s six-year accounting window; GDPR Article 30 records) has two conforming moves: align ledger_retention_policy so disclosure events outlive every accounting obligation, and/or declare a second Retention Window instance over the Selective Disclosure store — a declared multi-instance topology per execution-contract.md §Substrate composition invocation (the Defensible Retention / Customer Onboarding pattern), not a silent duplicate. This composition names the seam; it does not absorb the policy reconciliation (a Policy Reconciliation composing concept, as with ledger_retention_policy itself). One decidability obligation rides this edge case: the purge destroys the payload, and the accounting key survives only where this composition keeps it. The substrate’s destruction record preserves (event_id, attestation_id) and declares that it carries no payload field — data.disclosure_id is destroyed with the rest of the payload, and an earlier draft that had the substrate carry it forward was pinning a capability on a surface that disclaims it. The surviving key is the composition’s own disclosure_to_event entry, truth-bearing for purged events under a durability obligation (Composition state; extraction-pending against the Erasure Tombstone atom). That entry is what keeps binding-purged answerable after the event’s destruction; without it, a lawfully purged binding is indistinguishable from a binding-gap — precisely the destroyed-versus-missing confusion honest destruction (Audit Trail Invariant 8) exists to prevent, extended here from event existence to the binding key.
Clock source. recorded_at timestamps on ledger entries and disclosure events are best-effort wall-time annotations; the Event Log sequence_number (via the Audit Trail substrate) is the authoritative order source. The now written into a Record Entry or Disclose Subset payload is host-injected at this composition’s own I/O seam — read before the transition runs, one reading per invocation, the same seam that injects invocation_id (Primitive policies) — and never a value the substrate supplies: Audit Trail exposes no clock to its callers, and Event Log stamps its own recorded_at at its own seam from its own injected reading, so the payload’s recorded_at and the log’s stamped recorded_at are two readings of two clocks, and this composition compares them nowhere. An earlier revision attributed the reading to the substrate’s clock authority, which pinned a capability on a surface that does not expose it (§Capability provenance, the clock tell). The one reading serves every stamp the invocation writes — the intent event’s payload recorded_at, the disclosed_at passed through to SelectiveDisclosure.record at step 3, and the outcome event’s disclosed_at and recorded_at — so equality among them is by construction, not by comparison, which is what lets the scan pair a record to its intent on recorded_at = disclosed_at exactly (§A stamp from another seam never decides a write alone, the pass-through). The scan’s own reading is injected the same way at its seam, one per run; its lower-edge comparison against a record’s disclosed_at is two readings of this composition’s clock authority, which the deployment keeps monotone and shared across the nodes that run invocations and scans. One assumption is load-bearing and is stated: Selective Disclosure’s not-in-future guard compares the passed disclosed_at against its seam’s reading, so this composition’s seam must never be ahead of Selective Disclosure’s — the deployment injects both from one authority; where it does not, the guard refuses invalid-request at step 3 with nothing written and the intent event standing (the residue check 5 triages), never after the disclosure record. The seal-cadence timer and the retention-purge comparison are the substrate’s own and run on its clock; this composition inherits Audit Trail’s Clock source for cadence and purge edge case for those. For deployments where ledger or disclosure timestamps carry legal force, a Trusted Timestamping composition (per RFC 3161) provides the verifiable time anchor, and the Tamper Evidence seal’s anchored_at already supplies an adversary-resistant upper bound for the breach-forensics scenario.
Auditing the verification queries themselves. Verify Disclosure, Verify Ledger, and read are pure reads; they record no ledger event. For high-assurance deployments that must also account for who requested a disclosure proof or read the disclosure log, and when, an access-logging composing pattern wraps this composition’s read surface — mirroring how Audit Trail names attempted-but-not-committed actions as a Failed-Attempt Log composing concept rather than absorbing them. This composition’s own ledger surface is committed entries and committed disclosures, not queries against them.
Subset membership is over transaction entries. disclosed_entry_ids names ledger.entry (transaction) events; the composition validates membership against the set of ledger.entry events and rejects an id that resolves to a ledger.disclosed event (or to no event) with unknown-entry. Disclosing the fact of a prior disclosure — showing an auditor the disclosure log — is a read against the disclosure-accounting store, not a Disclose Subset of a ledger.disclosed event. This keeps the disclosed-subset semantics crisp: a disclosed subset is always a set of transactions, never a set of disclosure events.
Subject correspondence is the host’s assertion. transaction_data is opaque, so this composition cannot validate that disclosed_entry_ids actually pertain to subject_ref — nothing in this composition’s records connects an entry’s payload to the subject the disclosure is filed under; the correspondence is asserted by the discloser and recorded, mirroring the transaction_data accuracy bullet in the externally-clearable checks. The consequence is sharpest in accounting-of-disclosures deployments: under HIPAA §164.528, entries belonging to patient A but disclosed under the wrong subject_ref escape A’s accounting with no records-alone detection — the completeness of any subject’s accounting silently rests on the host tagging subject_ref correctly at each Disclose Subset. This composition makes the assertion immutable, attributed, and auditable; validating it is the host’s obligation, named in the externally-clearable checks (Whether disclosed_entry_ids genuinely pertain to subject_ref).
Single-artifact financial-instrument custody. Where a ledger entry represents a tracked artifact (a bearer instrument, a physical certificate) whose custody chain must also be proven, Provenance (via Chain of Custody) enriches this composition for those entries: the transaction_data references the artifact, and a parallel custody chain records its hand-to-hand transfers. This is an optional enrichment named for the artifact-backed case, not a constituent of the general ledger.

Terms

The canonical concepts this spec refers to. Each [Term] marker in the prose above links to its term entry here. A term entry states what the concept is, in plain English, plus its Kind — one of five: Type (a thing or category), Operation (a behavior), Member (a value of an enumerated Type), or, for a named datum, Field (a datum a Type carries — what does it carry?) or Parameter (a value an Operation needs — what does it need?). A term entry also names the Type it is a Member of / Field of, the Operation it is a Parameter of, and its Role where the domain assigns one. A term entry carries one Projection line — the concept’s single canonical lowering token, the one place the concrete name stays visible on the page — for every Field, Parameter, and pinned/wire Member. Everything else about casing (each target’s snake / camel / pascal / const / wire form) is derived from that one token by tools/harness/term-adapter.mjs, never hand-written. This is a composition, so its own concepts are: the four actions it exposes — the ledger append (Record Entry), the accountable disclosure (Disclose Subset), and the two verification queries (Verify Disclosure on the recipient side, Verify Ledger on the accountability side); the composition-introduced subset-proof artifact (Verification Bundle) and the Confidentiality Preserved property it carries; the accountability-side binding verdicts (Bound, Binding Purged, Binding Unbindable, Binding Gap); the disclosure-side authenticity verdicts (Authentic, Altered, Not In Ledger); and the composition’s own subset-membership rejection (Unknown Entry). Its load-bearing guarantees — the disclosure-accountability binding bijection (every disclosure is exactly one immutable ledger event, Invariant 1) and verifiable partial disclosure (Invariant 2) — are structural properties, not data. Its emergent state (disclosure_to_event) is a single derived index over the Audit Trail substrate, left as a backticked token; there is no composition-introduced record store to carry a term entry as a Type — a ledger entry is an Audit Trail event. The disclosure-proof and accountability-proof return-structure names, the ledger event types (ledger.entry, ledger.disclose_intended, ledger.disclosed, ledger.recovery_intended, ledger.disclosure_unbindable), the seam-injected invocation_id and the pairing tokens (intent_event_id, intent_event_candidates, disclosed_by, cascade_recovery), and the per-verdict reason parameters stay backticked as wire values, as do the read passthrough (read), the constituent calls and their outcomes — Audit Trail’s record_action / verify_record, Selective Disclosure’s record / read — the relayed constituent tokens (entry_id, event_id, disclosure_id, disclosed_entry_ids, transaction_data, subject_ref, recipient, scope, authority, actor_ref, credential, ledger_seal_reference), the composition output fields left uncarded (entries, overall_verdict, attestation_verification, retention_state, authenticity), the generic/relayed rejections (invalid-request, invalid-credential, unknown-authority-type, recording-failure, not-known, invalid-query), the deployment configuration knobs (ledger_retention_policy, seal_cadence, tamper_evidence_supports_partial_disclosure, disclosure_completion_bound, reconciliation_cadence, outcome_write_latency, outcome_retry_attempts, disclosed_entry_ids_cap, intent_candidates_cap, disclosure_section, application_actor_ref, application_credential, index_durability), and concrete example ids. Constituent atom and substrate names remain the existing full links to ../atoms/* and ./audit-trail.md; constituent operations stay backticked qualified calls, not cross-page links (the decided convention). (annotation.md Terms registry; representational only — it changes no guarantee, invariant, or behavior of the composition above.)

Record Entry

The composition action that appends one transaction to the ledger — a single AuditTrail.record_action (ledger.entry) producing an immutable, attributed, sealed, retained event. Returns the entry_id (the Audit Trail event_id).

Kind: Operation

Disclose Subset

The composition’s defining action: record that a named subset of ledger entries was disclosed to a recipient under an authority, and produce the Verification Bundle by which the recipient can independently verify that subset. Writes both the Selective Disclosure record and an immutable ledger.disclosed event — the intent record that authenticates the discloser, then the two truth-bearing writes the binding bijection lands in order and compensates until restored (Invariant 1).

Kind: Operation

Verify Disclosure

The recipient-side emergent verification: given the disclosed entries, the Verification Bundle, and the published ledger-seal reference, check each entry’s authenticity (Authentic / Altered / Not In Ledger / unverifiable) and whether the undisclosed remainder stayed hidden (Confidentiality Preserved) — without access to the undisclosed contents. Total: always returns a disclosure-proof, never a rejection.

Kind: Operation

Verify Ledger

The accountability-side verification, run by an auditor with access to the composition’s stores: given a disclosure_id, resolve whether the disclosure is bound to exactly one immutable, attributed, sealed, retained ledger event — Bound, Binding Purged (lawfully destroyed at its retention end), or Binding Gap (a finding). Returns an accountability-proof.

Kind: Operation

Verification Bundle

The composition-introduced subset-proof artifact Disclose Subset produces and Verify Disclosure checks — an independently verifiable proof that each disclosed entry is a genuine, unaltered ledger entry covered by the seal, without exposing the undisclosed remainder. No constituent produces it (Tamper Evidence verifies whole record-sets); it is emergent here, pending a forthcoming Subset Proof atom. Realized as Merkle inclusion proofs, an accumulator witness, or a signed package — the composition requires the capability, not any form.

Kind: Type Role: the independently-checkable subset proof

Confidentiality Preserved

The disclosure-proof field asserting that the Verification Bundle and disclosed entries reveal nothing about the count, content, or position of undisclosed entries beyond what the seal reference inherently publishes — the structural “the remainder stays undisclosed.” Self-reported by the verification routine, its trustworthiness resting on a security review of the mechanism’s zero-knowledge-of-complement construction (an externally-clearable check), not on recomputation from the records.

Kind: Field Field of: the disclosure proof Role: the remainder-stays-hidden assertion Projection: confidentiality_preserved

Bound

The Verify Ledger binding verdict when the disclosure resolves to exactly one live, immutable, attributed, sealed ledger event whose data.disclosure_id matches — the bijection holds within the retention lifetime.

Kind: Member Member of: the accountability binding Role: Binding verdict Projection: bound

Binding Purged

The Verify Ledger binding verdict when no live ledger.disclosed event names the disclosure but the composition’s own index still binds it to an event_id whose Purged retention record attests the event’s honest destruction at its retention end (Invariant 1’s retention-horizon arm) — lawful and distinguishable from a gap, not a finding.

Kind: Member Member of: the accountability binding Role: Binding verdict Projection: binding-purged

Binding Gap

The Verify Ledger binding verdict when no ledger event and no honest-destruction record name the disclosure — a recorded disclosure with no ledger event. Never a steady state under a conforming implementation (Invariant 1’s liveness arm); a high-priority finding.

Kind: Member Member of: the accountability binding Role: Binding verdict Projection: binding-gap

Binding Unbindable

The Verify Ledger binding verdict when no ledger event names the disclosure but a ledger.disclosure_unbindable marker does: the outcome write was refused deterministically for a reason no re-attestation cures (a payload the configured cap rejects), so the disclosure is accounted and attested but its ledger event could not land — a deployment-configuration finding with a lawful terminal state, superseded by Bound if the event later lands.

Kind: Member Member of: the accountability binding Role: Binding verdict Projection: binding-unbindable

Authentic

The Verify Disclosure per-entry authenticity verdict: the entry is a genuine, unaltered ledger entry covered by the seal.

Kind: Member Member of: the per-entry authenticity Role: Authenticity verdict Projection: authentic

Altered

The Verify Disclosure per-entry authenticity verdict: the entry does not match what the seal committed to.

Kind: Member Member of: the per-entry authenticity Role: Authenticity verdict Projection: altered

Not In Ledger

The Verify Disclosure per-entry authenticity verdict: the Verification Bundle does not place the entry under the seal.

Kind: Member Member of: the per-entry authenticity Role: Authenticity verdict Projection: not-in-ledger

Unknown Entry

The Disclose Subset rejection when a named subset id is unknown to the ledger’s Event Log, or resolves to a ledger.disclosed event rather than a ledger.entry transaction — naming every failing id, deterministically.

Kind: Member Member of: the disclose-subset rejection Role: Rejection Projection: unknown-entry

Standards references

This composition is the structural form of the immutable-ledger-with-accountable-disclosure requirement across its canonical domains:

SEC (US Securities and Exchange Commission) Rule 17a-4 (Records to be preserved by certain exchange members, brokers, and dealers) — requires broker-dealer transaction records to be preserved in a non-rewriteable, non-erasable form and produced, in whole or as a defined subset, on demand for an examiner. The Audit Trail substrate’s Tamper Evidence (Invariant 3) satisfies the non-rewriteable/non-erasable standard; Disclose Subset + Verify Disclosure (Invariant 2) is the structural form of producing a verifiable subset to an examiner without exposing the rest of the book; the configured ledger_retention_policy satisfies the six-year (first-two-years-accessible) lifetime requirement.
HIPAA (US Health Insurance Portability and Accountability Act) §164.528 (Accounting of disclosures of protected health information) — requires a covered entity to give an individual an accounting of disclosures of their PHI: date, recipient, scope, and purpose, drawn from the records alone. The Selective Disclosure store answers the accounting query (read by subject_ref); the binding bijection (Invariant 1) makes each accounted disclosure itself immutable, attributed, and tamper-evident — the property §164.528 needs but plain disclosure accounting cannot supply alone.
21 CFR (US Code of Federal Regulations) Part 11 (Electronic records and electronic signatures) — requires electronic records submitted to a regulator to be attributable, contemporaneous, original, and accurate (ALCOA), with disclosures to the agency themselves recorded. The four-atom Audit Trail stack supplies ALCOA over every ledger entry; Disclose Subset records each disclosure to the agency as an attributed, sealed ledger.disclosed event.
GDPR (EU General Data Protection Regulation) Article 15 (Right of access by the data subject) — a data subject may demand to know what data was disclosed and to which recipients. The Selective Disclosure store is the source for the recipients-and-scope answer; Verify Disclosure additionally lets the subject independently confirm a disclosed subset is genuine without the controller exposing every other subject’s entries on the shared ledger (Invariant 2’s confidentiality half).
W3C Verifiable Credentials Data Model and the selective-disclosure / BBS+ (a pairing-based signature scheme supporting selective disclosure of signed messages) proof literature — the standards surface for cryptographically proving a subset of a set of claims authentic while withholding the remainder. This composition’s verification_bundle and Verify Disclosure are the composition-layer form of this capability; the W3C VC selective-disclosure mechanisms (and accumulator / Merkle-inclusion-proof constructions) are typical realizations of Invariant 2’s behavioral obligation, named in rationale only — this composition requires the capability, not any particular proof system, exactly as Tamper Evidence is mechanism-neutral.

This composition inherits the broader standards compliance of its constituents:

Through Audit Trail (and its transitive atoms Event Log, Actor Identity, Tamper Evidence, Retention Window): SOX (Sarbanes-Oxley Act) §802 record retention, HIPAA §164.312(b) audit controls, PCI DSS (Payment Card Industry Data Security Standard) Requirement 10, 21 CFR Part 11 electronic records, ISO/IEC 27001 §A.12.4 logging and monitoring, GDPR Articles 30 and 32, and the full Audit Trail standards inheritance. Deployments composing this composition receive these as the substrate’s contribution; they are framed as inherited, not as this composition’s own primary anchors.
Through Selective Disclosure: GDPR Article 15(1)(c) and Article 30, HIPAA §164.528, and SEC Rule 17a-4 at the disclosure-accounting layer. This composition lifts these to the immutable-and-independently-verifiable form those standards actually require but that Selective Disclosure alone — which records that a disclosure occurred but seals nothing — cannot satisfy.

Status

partially resolved — see the Ledger.

Ledger

status: partially resolved
formal: pending — re-derivation against the one-writer protocol of 2026-08-30; was verified — immutable-transaction-ledger.tla + 1 twin, 2026-06-10
last gate: 2026-08-30 — third gate, fresh reader, under the frozen rules — 5 foundational corrected in-round, 12 refining and 7 rhetorical routed (2 refining and 2 rhetorical closed in-round, the second by the closure check; 1 refining a duplicate of 2026-08-26-f; 1 further refining line on the formal model added; the closure check's 2 refining corrected in-round); 2026-08-26 — authentication-precedence gate, fresh reader — 3 foundational (all pre-existing; all since closed), 7 refining, 1 rhetorical

open:
- 2026-08-26-e · refining · Invariant 1 · "produced by this composition" has no declared discriminator, so a direct constituent write enumerates as an orphan indistinguishable from a conformance failure → add a non-goal plus a reserved namespace, as the substrate does
- 2026-08-26-f · refining · Generation acceptance · Audit Trail's delegated bar enumerated as six checks where it declares eight; the two dropped are the ones the derived-index discipline leans on → cite eight
- 2026-08-26-i · refining · Invariant 2; Configuration · Invariant 2 lacks the unsealed-tail qualification Configuration says it carries, and no verdict is pinned for an entry still in the tail → add both
- 2026-08-26-j · refining · Summary · four regulatory acronyms unglossed at first use → gloss
- 2026-08-26-k · rhetorical · Terms, [Disclose Subset] term entry; The load-bearing wiring decision · both still describe a two-write sequence, predating the intent record → restate as three
- 2026-08-29-a · refining · formal · the model's compensation action carries no identity, no recovery record, and no age bound; the twin predates the scan's two edges → extend the model with the recovery-identity compensation behind `ledger.recovery_intended` and the bounded scan
- 2026-08-30-a · refining · [Verify Ledger] step 2 · no verdict for more than one live `ledger.disclosed` naming one `disclosure_id` → `binding-duplicate(event_ids)` (the index-hit-with-unreadable-payload half closed in-round)
- 2026-08-30-b · refining · [Verify Ledger] step 3 · only strict tail mode is named; lenient returns no covering range; the `(compensation-window)` qualifier's relay is unstated → pin (the `partially-purged-coverage` relay closed in-round)
- 2026-08-30-c · refining · step 1 vs *Primitive policies* · "whitespace-only accepted" while Selective Disclosure refuses whitespace-only — an `invalid-request` reachable after the intent → validate with the constituent's rule at step 1 (the clock half closed in-round)
- 2026-08-30-d · refining · step 1 · `read_record` returns `action_ref` from the attestation for a purged event, so a purged `ledger.entry` passes membership → pin (reject, or `unverifiable(entry-purged)` in the bundle)
- 2026-08-30-e · refining · Configuration, `seal_cadence` · "names the consequence in Invariant 2" — it does not; an unsealed entry at disclosure is unpinned → `authenticity = unverifiable(unsealed)`; bundle partial or `unavailable(unsealed)` (with 2026-08-26-i)
- 2026-08-30-f · refining · step 6 · the reissue path is load-bearing for Invariant 2 but only "exposed by the deployment" → declare `reissue_bundle(disclosure_id)` or drop the claim
- 2026-08-30-g · refining · Invariant 1; check 1 · "every Selective Disclosure record produced by this composition" is not enumerable — no producer field → define as paired by the pairing predicate; check 1 enumerates every record, unpaired = write-ownership findings (with 2026-08-26-e)
- 2026-08-30-h · refining · Walkthrough step 2 · the intent event is assigned `ev_5003`, already issued to the third trade, and step 3 treats `ev_5003` as an undisclosed trade → renumber (`ev_5004`, `ev_5005`)
- 2026-08-30-i · refining · `read` passthrough · "`invalid-query` has exactly one producing condition" is false → enumerate the relayed conditions
- 2026-08-30-j · refining · the `ledger.disclosed`-to-`ledger.entry` relation · undeclared (cardinality, modality, acyclicity) → declare it
- 2026-08-30-k · refining · Summary; Standards references · SEC, HIPAA, CFR, GDPR, W3C, ISO/IEC, "Merkle inclusion proofs", "cryptographic accumulators" unglossed at first use → gloss (with 2026-08-26-j)
- 2026-08-30-l · refining · *Primitive policies*, `invocation_id` · "every event payload the invocation emits" vs (a): the compensating `ledger.disclosed` and the `ledger.disclosure_unbindable` marker are unstated → state the field on every composition-written type
- 2026-08-30-m · refining · formal · the model commits the invocation's outcome as one atomic step and has no scan process, so the second writer, the counted terminus, the every-cycle rebuild and the step-1 sizing are not exhibited → extend it (with 2026-08-29-a)
- 2026-08-30-n · rhetorical · [Verify Ledger] step 2 · "Three terminal cases" introduces four, lettered (a)(b)(d)(c) → fix
- 2026-08-30-o · rhetorical · Terms, [Verify Ledger] term entry · omits [Binding Unbindable] → add
- 2026-08-30-p · rhetorical · Composes, Selective Disclosure · quotes edge-case titles the atom does not carry → quote accurately
- 2026-08-30-r · rhetorical · `recorded_at` · names both the payload field and Event Log's stamped field → qualify "payload `recorded_at`"
- 2026-08-30-s · rhetorical · *Primitive policies* `disclosed_entry_ids`; [Unknown Entry] term entry · narrower than step 1's rule → align
- 2026-08-30-t · rhetorical · Walkthrough · `record_action` payloads omit `invocation_id` → include, or mark abbreviated
- 2026-08-30-u · rhetorical · Composes · "pass-through list read" has no projected contract → cite Audit Trail's *List-shaped queries* paragraph

Decisions

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

2026-08-30 — One writer per disclosure, the purged answer first, the outcome sized before the intent, the clock at the composition’s seam, the position on the code. Chose: Disclose Subset step 4 pre-checks under the per-disclosure_id section the scan also takes and adopts an existing ledger.disclosed as its own outcome, with an in-invocation retry counted by outcome_retry_attempts and the scan the only writer thereafter; the scan runs disclosure_to_event’s full rebuild as a write every cycle, under a declared reconciliation_cadence and the inequality disclosure_completion_bound + reconciliation_cadence + outcome_write_latency < the shortest retention period, so the index’s purged half is captured before any purge can reach its event and a lost entry is honestly a loss; step 1 sizes the maximal outcome-and-compensation envelope against payload_cap before the intent, with disclosed_entry_ids_cap and intent_candidates_cap bounding the two set-valued fields; now declared host-injected at this composition’s seam, one reading per invocation, with the pass-through to Selective Disclosure making the pairing equality by construction and the constituent’s not-in-future guard named as the one cross-seam comparison; recording-failure(intent | outcome) on the Disclose Subset signature; Verify Ledger branching on retention state at its index hit and on coverage status at its presentation before any composition-side membership check; and — from the closure check — the per-disclosure_id section declared as the disclosure_section instance capability with lease semantics (taken at step 3’s return, released on return or death, a lease exactly disclosure_completion_bound long whose expiry is the invocation’s terminus, re-taken before any pre-check and never permitting an append past the bound), the bound restated seam-to-step-4, an adopted entry_set_unresolved event yielding verification_bundle = unavailable(entry-set-unresolved), and every remaining “atomically” replaced by the ordered three-write sequence the protocol actually runs. Over: a bare append at step 4 beside a scan that starts at the bound; a truth-bearing half written only by a step an invocation may never reach; “foreclosed by construction” argued about the intent while the outcome and the compensation grow without a cap; a clock attributed to a substrate that exposes none; two dispositions on one token at the caller boundary; a payload-not-supplied verdict for a payload the substrate destroyed; a critical section attributed to the host in no Configuration entry, with no release or expiry bound; and a page that said atomically about a sequence its own edge case calls irreversible-then-compensated. Because: two compensators over one act land two outcomes the seal then protects; a truth-bearing index that presumes the fact was captured is a finding-generator against a durability obligation nobody breached; an unbounded set is an input, not a construction; a reading mislocated to a constituent mislocates every stamp the composition writes; a caller who cannot tell intent from outcome re-runs a committed disclosure; lawful destruction is not omission; a section nobody declared has no lease, and a lease no bound governs blocks the leg forever; and a bundle over a set no sealed record determines proves a set the composition never recorded (the frozen rules of 2026-08-30 — A compensator is exclusive, Lawful destruction is answered before absence, An outcome is sized before the intent, Liveness is arithmetic, A stamp from another seam never decides a write alone, A composition’s own rejection arm carries the retry bit, and Capability provenance frozen — with §A derived index splits at the horizon’s truth-bearing half).
2026-08-29 — The scan is bounded and writes as the composition, the substrate’s step decides the landing, and the seal is verified over its range. Chose: a declared disclosure_completion_bound below which the orphan enumeration examines nothing, with the ledger horizon as its upper edge; every scan write attested under a declared recovery identity behind a ledger.recovery_intended record, the orphan paired to its intent by the reading step 3 now passes explicitly as disclosed_at (candidates named where undecidable, and an undetermined entry set omitted rather than asserted); a seam-injected invocation_id on every event payload so an indeterminate substrate arm is read back exactly; every transcription carrying recording-failure(step), with step-4 and the retention-source invalid-request proceeding as landed at both actions; and Verify Ledger’s presentation keyed by sequence_number over the covering range read_record names. Over: an unbounded scan under an undeclared identity, a bare token that sent Record Entry’s caller back to append a second entry, and a one-payload presentation that returns a mismatch on every intact ledger under interval cadence. Because: an unbounded scan compensates in-flight disclosures beside their own outcome events and re-manufactures lawfully purged ones; a compensation the discloser did not make cannot be attested as theirs; the substrate’s step-4 arm means the event exists; and a seal commits to a range (the frozen rules of 2026-08-29 — A reconciliation is bounded at both ends, Recovery commits under a declared service identity, Intents pair with outcomes, A transcribed rejection arm keeps its payload, A seal presentation is keyed by log position).
2026-08-27 — The purged binding’s key lives in the composition, and the unbindable orphan gets a terminal verdict. Chose: disclosure_to_event’s purged half is truth-bearing under a durability obligation (extraction-pending against the Erasure Tombstone atom), and a deterministic invalid-request on the outcome write lands as a ledger.disclosure_unbindable marker read back as binding-unbindable. Over: configuring the substrate to carry data.disclosure_id on its destruction record, and retrying the unbindable orphan indefinitely under the recovery identity. Because: the substrate declares its destruction record carries no payload field, so the earlier obligation pinned a capability on a surface that disclaims it; and re-attestation changes only the credential, so an orphan the payload or policy refuses had no lawful terminal state until one was declared.
2026-06-10 — Invariant 1 is safety plus liveness, and the model checks the compensated arm. Chose: state the disclosure-accountability binding as “no unsurfaced orphan” (safety) and “every orphan is eventually bound or surfaced” (liveness), and re-derive the model over the two truth-bearing sub-writes so the reachable orphan is in scope. Over: the original model’s idealization, which committed the sub-writes as one atomic action. Because: Selective Disclosure writes first and irreversibly and no synchronous rollback exists, so the orphan is reachable by design and an invariant that assumed it away verified nothing.

Immutable Transaction Ledger with Selective Disclosure

Summary

Intent

Composes

Composition logic

Composition state

Configuration

Primitive policies

Action wiring

record_entry

disclose_subset

verify_disclosure

verify_ledger

read (passthrough)

The load-bearing wiring decision — disclosure ⇒ {intent, accounting record, ledger event}, ordered and compensated; partial-verifiability as a capability, not a mechanism

Composition-level invariants

Examples

Walkthrough — broker-dealer trade-confirmation ledger under SEC Rule 17a-4

Healthcare — accounting of disclosures under HIPAA §164.528

Clinical-trial submission ledger under 21 CFR Part 11

Rejection path — empty or unknown subset

Rejection path — ledger write fails after the disclosure record commits (the orphan)

Retention horizon — a disclosure event reaches its lawful end

Regulated adversarial scenarios

Generation acceptance

Record checks

External checks

Non-goals and edge cases

Terms

Record Entry

Disclose Subset

Verify Disclosure

Verify Ledger

Verification Bundle

Confidentiality Preserved

Bound

Binding Purged

Binding Gap

Binding Unbindable

Authentic

Altered

Not In Ledger

Unknown Entry

Standards references

Status

Ledger

Decisions

`record_entry`

`disclose_subset`

`verify_disclosure`

`verify_ledger`

`read` (passthrough)