Skip to Content
The Protocol

AHL Protocol Specification (revision 0.4)

Author: Dmitrii Zatona Document: draft-zatona-ahl-00 Revision: 0.4 Date: August 2026

This page is a condensed rendering of the Internet-Draft, not a copy of it. Its section numbers are the I-D’s, so every statement here can be cross-referenced against the source. Where the two differ, the I-D governs.

Abstract

AHL is an open format for record-level, tamper-evident data provenance. It defines signed, digest-bound statements about individual records — ingestion, derivation, retraction, correction, propagation, plus manifest and key statements for corpus governance; a log-binding contract that anchors those statements in an append-only, verifiable log offering inclusion, consistency, and authenticated range enumeration; procedures for point-in-time reconstruction of an asserted derivation as known at a past checkpoint; and revocation propagation semantics computed and verified over an explicitly declared, enumerable corpus.

Conformance is graded L1 through L3. A portable Evidence Receipt container permits offline verification of a declared claim. AHL provides non-repudiation of assertions and tamper-evidence of their history; it does not assert that any statement is true, and every guarantee it offers names the boundary within which it holds. This document specifies the closed-corpus core: one producer, one log, one keyspace. Federation across corpora is out of scope and summarized as future work.

1. Introduction

A derived record — a resolved identity, a risk score, an enriched attribute, a batch-release certificate — is produced from other records by a transform. A party may later ask three distinct questions: derivation (which inputs, code, model version and parameters produced this record), reconstruction (what was asserted about it as of a past point in time, distinguishing what was true of the world from what was known to the producer), and propagation (when a source record was retracted or corrected, did that retraction reach every downstream record derived from it).

Existing tooling answers the first at dataset granularity and records the answer as mutable metadata in a system controlled by the party being audited. The third is generally not answered at all. AHL records record-level derivation as anchored evidence rather than as mutable metadata, and defines revocation propagation as a computation a verifier can repeat independently. It composes with, rather than replaces, existing lineage and build-provenance systems (Appendix C).

1.1. Design Principles

  • Every guarantee names its boundary. Completeness is completeness relative to a declared corpus. Independent verifiability reduces the trust placed in a log operator to the detectability of inconsistent behaviour; it does not eliminate that trust. A receipt proves the claim it declares and nothing beyond it. A statement of assurance without a stated boundary is a specification defect.
  • Order is position; time is evidence. Every ordering relation — “before”, “after”, “latest”, membership in a checkpoint — is evaluated on the entry index. Timestamps, including the log’s own, are evidence for human assessment and are never an ordering primitive.
  • Verification is a fact, not a service. The artifacts AHL defines are verifiable offline, years later, without access to the producer or to the log, given the receipt, the pinned adaptor-profile document, and the verifier’s locally configured trust policy.

1.2. Scope

This document specifies the closed-corpus core: one producer, one log, one keyspace. Cross-corpus record identity, recipient-bearing disclosure statements, and evidenced observation of triggers issued in a foreign corpus are extensions and are out of scope here; they are outlined as future work in Appendix A.

AHL does not define authorization, tenancy, account management, or key distribution. The manifest’s key-access rule is an opaque declaration of policy, not an authorization mechanism.

1.3. Trust Model

Producers may err, and may later have reason to describe their history differently. AHL binds assertions to content digests and anchors them so that history cannot be silently rewritten. It does not prove statements true, does not prove that unstated derivations are absent, and does not prevent a log operator from behaving incorrectly. It makes each such failure detectable within declared boundaries: inaccurate statements by cross-checking against the referenced material, omissions against the manifest’s coverage declarations (§6.2), and divergent log views through the witness protocol (§3.3).

AHL asserts, for an anchored statement verified against the applicable manifest and key state: that the statement was signed by the holder of the identified key; that it binds to exactly the committed content; and that it is included at a stated entry index. At L3, inclusion proofs, consistency proofs, and witnessed checkpoints make rewriting of history and the presentation of inconsistent views detectable. For a propagation claim at its declared checkpoint, AHL determines whether the producer’s dispositions match the closure recomputed from the declared corpus.

AHL does not assert: that any statement is true; that unstated derivations do not exist; that the declared corpus is the whole of the producer’s activity; or that a log operator cannot refuse service.

1.4. Requirements Language

The key words “MUST”, “MUST NOT”, “REQUIRED”, “SHALL”, “SHALL NOT”, “SHOULD”, “SHOULD NOT”, “RECOMMENDED”, “NOT RECOMMENDED”, “MAY”, and “OPTIONAL” are to be interpreted as described in BCP 14 [RFC2119] [RFC8174] when, and only when, they appear in all capitals.

1.5. Terminology

  • Record — the unit provenance is asserted about. AHL constrains how a record is identified (§2.6), not what form it takes.
  • Record commitment — the stable, dataset- and descriptor-scoped cryptographic identifier of record content (§2.6). Triggers name record commitments, and closure traversal follows them.
  • Representation digest — the hash of the bytes a transform actually consumed, which may be the full record or a projection of it.
  • Transform — the code, model, parameters, and optionally environment that produced an output record from its inputs, each identified by digest (§2.5).
  • Statement — a signed assertion (§2). Statement id — SHA-256 over the JCS [RFC8785] serialization of a statement payload. Entry id — SHA-256 over the JCS serialization of a statement envelope. Entry — the anchored envelope bytes.
  • Corpus — all statements anchored in the declared log under the declared manifest lineage. Corpus manifest — the anchored declaration of scope, keys, datasets, pipelines, windows and retention described in §6.2.
  • Dataset — a manifest-declared class of records sharing a canonicalization descriptor, a commitment mode, and an authority. Dataset authority — the key set entitled to issue triggers for records ingested into a dataset; in the core this is the producer, and the field exists so that federation can generalize it.
  • Producer / Log operator / Witness / Verifier — the operator MAY be the producer; a witness MUST be independent of both producer and log operator.
  • Checkpoint — a signed commitment to log state {log_id, tree_size, root_hash, checkpoint_time}. A checkpoint C commits exactly the entries whose index lies in [0, tree_size(C)). A receipt carries a checkpoint in the superset form of §7.1.
  • Entry index — an entry’s immutable position in the log; the ordering primitive for every ordering and checkpoint-membership rule.
  • Log-attested incorporation time (LIT) — the log’s timestamp for an entry; AHL’s transaction time, for evidence purposes only. LIT is never used for ordering, because logs are not required to assign monotonic or unique timestamps.
  • Trigger — a retraction or a correction statement.

2. Statements

2.1. Envelope, Identifiers, and Signing

{ "payload": { ... }, "signatures": [ { "key_id": "<key id from the manifest key set>", "sig": "base64:<Ed25519 signature over JCS(payload)>" } ] }
  • Every statement MUST be signed, at every conformance level. An unsigned object is not an AHL statement, and neither is an envelope that fails the signature rule below: such an envelope is VOID — never a governance statement, never a competing candidate, never effective, never traversed by closure. Whether a void envelope affects a verification RESULT is a question of reliance, settled in §7.5.1 4d, and not of its presence: a log anchors opaque bytes and validates none of them.
  • Envelope signature rule. An envelope is valid only if EVERY entry in its signatures array resolves to a key active at the envelope’s entry index and verifies over JCS(payload) — the conjunction of all entries. An envelope carrying a non-verifying entry, or an entry naming a key that is not active at that index, is invalid regardless of how many other entries verify. A verifier MUST NOT accept a subset of the signatures.
  • Authorization is a separate and later test, applied only to envelopes already valid under that rule. For triggers it is specified in §2.4.3.
  • Signatures MUST use Ed25519 [RFC8032]; digests MUST use SHA-256 [RFC6234]; JSON payloads MUST be canonicalized with JCS [RFC8785] before hashing or signing.
  • The statement id is SHA-256(JCS(payload)), the reference used in the statement graph. The entry id is SHA-256(JCS(envelope)), the reference used wherever signature identity or anchoring identity matters, as in manifest and key statements.
  • A producer MUST NOT anchor two envelopes bearing the same statement id. If duplicates nevertheless occur, the envelope with the smallest entry index governs and later ones are void.
  • DSSE wrapping MAY be used for interoperability with build-provenance tooling; such use is non-normative and does not alter the identifiers above.

Family strings. Every value carrying a digest or raw octets is a string bearing a family prefix, and the three families are fixed here once for every object the protocol defines. An adaptor profile MUST NOT redefine the encoding of a family string appearing in a core object.

  • "sha256:<hex>" — exactly 64 lowercase hexadecimal digits. No 0x prefix, no separators, no whitespace.
  • "hmac-sha256:<hex>" — the same rule for an HMAC-SHA-256 value.
  • "base64:<b64>" — raw octets in the standard base64 alphabet of [RFC4648] §4, WITH padding. The URL-safe alphabet is neither emitted nor accepted.

Acceptance is strict, and MUST NOT be more permissive than emission. A verifier rejects a family string with the wrong prefix, the wrong length, a character outside its alphabet, missing or misplaced padding, whitespace, or a non-canonical base64 encoding whose final quantum sets bits the decoded length does not use. In a receipt, a family string failing any of these checks is a schema failure and the result is invalid (§7.7).

2.2. Common Payload Fields

{ "ahl_version": "0.4", "type": "ingestion | derivation | retraction | correction | propagation | manifest | key", "producer": "<producer id>", "manifest": "<manifest version id; absent only in manifest statements>", "valid_time": "<RFC 3339>" | { "from": "<RFC 3339>", "to": "<RFC 3339 or null>" }, "issued_at": "<RFC 3339>" }

ahl_version is REQUIRED in every statement payload, including a manifest statement’s, and is 0.4 for statements conforming to this revision.

This document defines revision 0.4, and defines no verification of material issued under any earlier revision. That is the clean-break rule:

  • A carried statement whose ahl_version is anything other than 0.4 is unverifiable (§7.7), and never invalid. An old artifact is not a defective one.
  • A corpus anchored under an earlier revision CANNOT be continued under this one. Continuation requires a NEW GENESIS — a fresh corpus under revision 0.4 — and the relationship between old and new is for the operator to record out of band.
  • An absent or malformed ahl_version is a schema failure and is invalid, being decidable from the bytes alone.

The break was chosen because the string 0.3 does not denote one rule set: material issued under it differs in whether a dataset declares a bare canonicalization identifier or a canonicalization descriptor, and the bytes carry nothing that distinguishes those cases. Refusing is honest; guessing is not.

Three times are associated with an anchored statement and MUST NOT be conflated: valid_time (asserted validity in the application domain), issued_at (asserted creation time), and the log-attested incorporation time. Ordering always uses the entry index.

At L2 and above, a statement’s manifest field MUST reference the manifest version active at the statement’s entry index — the manifest statement with the greatest entry index smaller than the statement’s own (§2.4.5). A mismatch is a conformance violation and is mechanically visible from log order. At L1, where statements are not anchored, the binding is by signed reference to a published manifest version.

2.3. Statement Type Overview

AHL defines seven statement types. Five describe records: ingestion, derivation, retraction, correction, propagation. Two govern the corpus itself: manifest, key.

2.4. Statement Types

2.4.1. ingestion

{ "type": "ingestion", "dataset": "<dataset id>", "record": "<record commitment>", "origin": "<optional non-personal descriptor: source system, batch reference>" }

Every record referenced as an input MUST be introduced by exactly one anchored ingestion, or produced by an anchored derivation, at an entry index smaller than its first use. Consuming a record that has not been introduced is a coverage violation. The dataset authority declared in the manifest is the authority over ingested records for trigger purposes (§2.4.3).

2.4.2. derivation

{ "type": "derivation", "pipeline": "<pipeline id from the manifest>", "outputs": [ { "dataset": "<dataset id>", "record": "<record commitment>", "locator": "<optional URI; no personal data>" } ], "inputs": [ { "dataset": "<dataset id>", "record": "<source record commitment; REQUIRED — what a trigger would name>", "representation": "<digest of the bytes actually consumed, if not the full record>", "projection": { "descriptor": "<spec>", "digest": "sha256:<hex of JCS(descriptor)>" }, "role": "feature | reference | config", "statement": "<optional statement id of the input's ingestion or derivation>" } ], "transform": { "code": { "digest": "sha256:<hex>", "type": "git_commit | artifact | container" }, "model": { "digest": "sha256:<hex>", "version": "<label>" }, "params": { "digest": "sha256:<hex of JCS(params)>" }, "environment": "<optional digest, e.g. build provenance>" } }

Closure traversal (§5.1) uses the (dataset, record) pair only; representation and projection narrow what was consumed and never create or alter identity. A derivation MUST list every input record read to produce the stated outputs, or use the batch form of §2.7.

A derivation MUST NOT consume a record for which an effective trigger (§2.4.3) is anchored at a smaller entry index. In the closed-corpus core the semantic revocation horizon is zero entries: this is a statement about log order, not about wall-clock latency. A parameterized horizon for triggers observed across a corpus boundary — analogous in role to the maximum merge delay of [RFC9162] — belongs to the federation extension (Appendix A).

2.4.3. retraction and correction

{ "type": "retraction", "dataset": "<dataset id>", "record": "<record commitment>", "scope": { "effective_from": "<RFC 3339>", "retroactive": true | false }, "reason_code": "error | fraud | legal_obligation | consent_withdrawn | superseded | other" } { "type": "correction", "dataset": "<dataset id>", "record": "<old commitment>", "replacement": "<new commitment>", "scope": { ... }, "reason_code": "..." }
  • scope is REQUIRED; a trigger without a scope is malformed. With retroactive: true, every derivation consuming the record is affected regardless of valid time. With retroactive: false, a derivation is affected if and only if its valid_time intersects [effective_from, infinity).
  • A trigger anchored at an entry index smaller than the record’s introduction is never effective: authority cannot predate the introduction that creates it.
  • Authority. Authority is tested only after the envelope is valid under the envelope signature rule of §2.1; a trigger whose envelope is invalid is never effective, whoever signed it. A valid trigger is authorized, and therefore effective, if and only if AT LEAST ONE of its verified signers holds a key in the record’s authority key set, active at the trigger’s entry index — the dataset authority for ingested records and, for derived records, the introducing producer’s key set, in both cases evaluated at the trigger’s entry index rather than at the introduction index. Co-signature by other active producer keys is permitted and does not weaken the trigger. A valid trigger with no verified signer in the authority key set anchors as a challenge: it is surfaced by verification and is never traversed by closure.
  • A correction’s replacement MUST be introduced, by ingestion or derivation, at an entry index no greater than that of the correction.
  • Among the effective triggers for one record, the one with the greatest entry index governs. Verifiers surface the whole chain rather than only the governing member.

2.4.4. propagation

{ "type": "propagation", "trigger": "<statement id>", "corpus_checkpoint": { "log_id": "...", "tree_size": 1450, "root_hash": "sha256:<hex>" }, "affected_root": "sha256:<root over disposition leaves, per §2.7 tree rules>", "affected_count": 12, "complete_relative_to_manifest": true }

The declared corpus_checkpoint MUST commit the trigger’s entry. Each disposition leaf is the JCS serialization of:

{ "dataset": "<dataset id>", "record": "<record commitment>", "disposition": "invalidated | recomputed | assessed_unaffected", "successor_statement": "<REQUIRED for recomputed; its inputs MUST include the correction's replacement>", "assessment": "<REQUIRED for assessed_unaffected; sha256 of the retained assessment artifact>" }

The disposition invalidated is operational: the producer MUST NOT rely on or serve the record for the purposes the manifest covers.

Completeness is defined at the declared corpus checkpoint D and nowhere else. §2.4.2 prohibits consuming the triggered record itself after the trigger, but a later derivation MAY consume an already-affected descendant, which enlarges the transitive closure beyond D. Closure is therefore not stable across later checkpoints, and a completeness claim never extends past D. Whether consuming a record dispositioned invalidated should itself be a violation is an open issue in the core specification and is not settled by this revision.

2.4.5. manifest

The payload of a manifest statement is the manifest object: the fields of §6.2 appear at the top level alongside the common fields of §2.2, with no wrapper member, and the manifest common field is absent.

Identifier reconciliation is deliberate and asymmetric. The manifest version id, which every other statement’s manifest field references, is the manifest statement’s statement id. A non-genesis manifest references its predecessor by entry id in a predecessor member, REQUIRED for non-genesis manifests and forbidden for the genesis manifest.

The genesis manifest is the corpus trust anchor. Its ENTRY ID is distributed out of band and is the pin. Because an entry id is SHA-256(JCS(envelope)), requiring the carried genesis envelope to recompute to that entry id binds the WHOLE genesis envelope — its producer key set, its log checkpoint-signing key objects, and its witness key objects alike. The genesis LOG and WITNESS key sets are therefore pinned out of band, which is what the governance-key induction of §7.5.1 rests on.

Initial key fingerprints MAY also be distributed with the entry id, and local policy MAY hold them. Distributing them is OPTIONAL: they add no cryptographic strength, since the entry id already binds every one of them. What they are for is operational — human-reviewable material that lets a verifier report a MISCONFIGURED anchor with a specific diagnostic instead of an unexplained entry-id mismatch. Where local policy does hold them, §7.5.1 requires the comparison to be made.

Each subsequent manifest statement MUST be signed by a key valid under the previous manifest version and MUST reference that version by entry id. Manifest lineage is thus an anchored chain, and “the manifest version active at entry index i” is mechanically resolvable from the log.

2.4.6. key

{ "type": "key", "action": "add | retire", "key": { "key_id": "sha256:<hex>", "pubkey": "base64:<...>", "valid_from": "<RFC 3339>" } }

A key statement MUST be signed by a currently valid key and MUST be anchored. Statements verify against the key set as evaluated at their own entry index; key transitions are ordered by their own entry indexes, and valid_from is informative. For producer keys, key_id is sha256: followed by the lowercase hex SHA-256 of the raw 32-byte Ed25519 public key. Key-id derivation for log and witness keys is defined by the adaptor profile (§3.2).

Recovery from producer-key compromise is not specified in this revision. Until it is, a compromise invalidates conformance claims from the time of compromise forward.

2.5. Transform Identity

A transform is identified by digests, not by names: code by commit, artifact or container digest; model by digest with an informative version label; parameters by the digest of their JCS serialization; and optionally the build or execution environment by digest. Names and version labels are evidence for human assessment; the digests are what verification compares. AHL always proves which artifacts a derivation claims to have used, and detects substitution of a different artifact under the same label. It cannot demonstrate that the named artifact behaves as described.

2.6. Record Identity, Canonicalization, and Commitment Modes

For each dataset the manifest declares a canonicalization descriptor and a commitment mode. The descriptor is bound into every commitment in the dataset, so a verifier handed a descriptor can CHECK it against the commitment by recomputation instead of assuming that the descriptor it was given is the one the commitment was computed under.

Let D be the dataset’s canonicalization descriptor and ddig = SHA-256(JCS(D)) its descriptor digest, taken as the raw 32 digest octets and not as a family string. The two commitment modes are:

plain commitment = SHA-256( dsid || 0x1F || ddig || 0x1F || canonical bytes ) keyed commitment = HMAC-SHA-256( k_dataset, dsid || 0x1F || ddig || 0x1F || canonical bytes )

keyed is REQUIRED for personal or otherwise sensitive data; k_dataset is held by the producer and disclosed under the manifest’s key-access rule to authorized verifiers.

The two separations in the preimage are not equally strong, and the difference is stated rather than smoothed over. Domain separation by dataset id gives identical bytes in different datasets distinct preimages UNCONDITIONALLY, because dsid enters the preimage verbatim. The descriptor enters only through ddig, a fixed-length hash, so identical bytes canonicalized under DIFFERENT DESCRIPTORS receive distinct preimages only under the collision resistance of SHA-256.

Dataset id syntax and encoding. dsid is the dataset id as its US-ASCII octets: at least 1 and at most 128 characters, each printable US-ASCII in 0x21–0x7E — every printable ASCII character except the space. A dataset id MUST NOT contain a control octet: any octet in 0x00–0x1F, or 0x7F. The repertoire already excludes them, and the prohibition is stated separately because it is load-bearing and is exactly the check an implementation omits. A dataset id containing 0x1F makes the preimage AMBIGUOUS, and two distinct records can then collide. An implementation that validates length and printability but omits this check interoperates correctly on every well-formed input and fails only on a crafted one.

Given the prohibition, the preimage encoding is injective OVER THE TRIPLE (dsid, ddig, canonical bytes) — and it is worth being exact about which triple, because it is not the triple of dataset id, DESCRIPTOR and bytes. The first 0x1F always ends dsid; ddig is then exactly 32 octets; the octet after it is the second 0x1F; everything following is the canonical bytes. Distinct values of (dsid, ddig, canonical bytes) therefore produce distinct PREIMAGES unconditionally, by parsing alone. The two remaining steps are not unconditional: distinct DESCRIPTORS yield distinct ddig only on the collision-resistance assumption for SHA-256, and distinct PREIMAGES yield distinct COMMITMENTS only computationally. What the encoding contributes is that the construction adds NO SECOND FAILURE MODE beyond the assumption everything here already rests on (§8.1).

Rules that follow:

  1. One canonicalization descriptor and one commitment mode per dataset, used by all statement types referencing that dataset, so that trigger matching always works within the corpus. The unit is the DESCRIPTOR, not the canonicalization identifier alone.
  2. The canonicalization descriptor is {canonicalization, media_type?}. canonicalization is an identifier from the “AHL Canonicalization Identifiers” registry (§10.3) or a private-use identifier beginning x-. media_type is present if and only if the descriptor requires it, which is a property of the identifier: exact-bytes requires it, jcs does not. Presence is a producer duty and is never a syntactic matter — deciding it needs either the registration or a corpus-scoped local configuration, and a receipt carries neither, so presence NEVER rejects a manifest. A verifier that IMPLEMENTS the procedure and finds media_type absent where the procedure requires it, or present where it does not, reports that dataset’s content-binding finding as invalid (§7.7); one that does not implement the procedure reports unverifiable. Identifier syntax: lowercase ASCII restricted to a-z, 0-9 and -, 1 to 64 characters, beginning with a-z. JSON records canonicalize per [RFC8785] under jcs; other records canonicalize under exact-bytes, qualified by the descriptor’s media type, or under a registered identifier. This document defines only jcs and exact-bytes; every other procedure reaches a dataset by registration (§10.3).
  3. Private use is corpus-scoped: an x- identifier is resolved only from configuration keyed on (genesis entry id, identifier).

2.7. Batching and Tree Rules

For a batch derivation, the top-level members outputs_root, outputs_count and leaf_format: "ahl-leaf-v2" replace the outputs array. A version-2 leaf is the JCS serialization of { "dataset", "record", "inputs" }, where inputs is either the full array of input objects from §2.4.2 or the input-set form { "input_set_root", "input_set_count" }.

Tree rules, identical for every AHL tree — outputs, input sets and dispositions:

LeafHash = SHA-256( 0x00 || leaf ) NodeHash = SHA-256( 0x01 || left || right )
  • SHA-256 throughout.
  • Leaves are sorted by record, comparing the UTF-8 bytes of the canonical commitment string in ascending lexicographic order. Commitment strings are family strings under §2.1, and one failing those rules is rejected.
  • Duplicate leaves are prohibited.
  • Membership proofs are O(log n).

Retrievability. The full leaf set of every committed tree is corpus material, subject to the retention and enumeration duties of §3.4 and §6.2.

3. Log Binding

AHL does not define a log. It defines a log-binding contract, which a given log satisfies through a published adaptor profile pinned in the manifest.

3.1. The Contract

A conforming log MUST provide:

  1. Append-only semantics, entries treated as opaque bytes, and a log-attested incorporation time per entry.
  2. Signed checkpoints at the declared cadence, with log keys discoverable through the manifest.
  3. Inclusion proofs from an entry to a checkpoint, and consistency proofs from one checkpoint to another.
  4. Retrieval by entry id.
  5. Authenticated enumeration: the ability to serve the entries in a range [i, j) under a checkpoint together with a proof of completeness and order, so that a verifier can walk the whole log, or any interval of it, and know that nothing was skipped.
  6. Proof and checkpoint serialization as specified by the adaptor profile.

3.2. Adaptor Profiles

Adaptor profiles MUST be versioned, immutable, content-addressed — identified by name and hash — openly published, and independently implementable. The profile id and hash are pinned in the manifest and carried in every Evidence Receipt (§7). No conformant verification may require implementation-specific knowledge outside the profile document.

Logs of the class described by [RFC9162] and [RFC6962] are expected to satisfy the contract through thin adaptors. That expectation is a feasibility claim to be assessed per adaptor; it is not a grant of conformance to any particular log. One profile is released: ahl-adaptor-atl-v1.

3.3. Witness Protocol (L3)

Inclusion and consistency proofs establish consistency only within the view presented to the verifier; an operator that presents inconsistent views to different parties is not detected by those proofs alone. L3 therefore requires at least one independent witness per log, operating this state machine:

  1. The witness retains, per log, the latest checkpoint it has cosigned. Before it has cosigned any it retains none; that is the BOOTSTRAP state.
  2. On receiving a new checkpoint at the declared cadence, the witness verifies the log’s signature and verifies a consistency proof from the retained checkpoint. On success it cosigns, retains, and publishes the result through a stable query interface.
    • 2a. Bootstrap. A witness holding no retained checkpoint has no prior view for the new one to be consistent with. It verifies the log’s signature alone and, on success, cosigns, retains and publishes. A blanket refusal at bootstrap would be wrong: a witness MUST be able to cosign a FIRST checkpoint, or no log could ever acquire one.
  3. On failure — an inconsistency, or a missing proof — the witness MUST refuse to cosign and MUST publish signed refusal evidence containing both conflicting checkpoints. This form of evidence is SELF-AUTHENTICATING: it exhibits two signed checkpoints that cannot both be true, so anyone can evaluate the contradiction without trusting the witness that published it.
    • 3a. Refusal at bootstrap names ONE checkpoint and a reason, and is NOT self-authenticating. Malformedness is decidable from the carried checkpoint alone, so the evidence is CHECKABLE by any party. A failing log signature is not: checking it requires the applicable log key state, which the evidence is not required to carry. A verifier that independently holds that key state MAY re-run the check; one that does not can establish only THAT THIS WITNESS REPORTED THIS. In no case does bootstrap refusal evidence establish equivocation.
  4. A witness whose latest cosigned checkpoint is older than the declared cadence by more than the declared grace period is stale. Verifiers treat staleness as a finding.

The bootstrap boundary. A witness attests only from its own first retained checkpoint forward. A verifier MUST NOT read a witness cosignature as evidence about any tree size smaller than the first that witness retained. Equivocation detection begins there and not earlier.

At L3 a verifier accepts a checkpoint C only with a valid witness cosignature, and verifies consistency from C to the latest witnessed checkpoint.

Claim discipline. L3 reduces the trust placed in the log operator to the detectability of inconsistent behaviour; refusal of service remains possible and remains visible. Documents describing AHL MUST NOT claim that no trust is required.

3.4. Availability at L3

At L3, digest-only anchoring is prohibited. Entries MUST be retrievable, by id and by enumeration, from the log or from an independent mirror outside the producer’s control. The complete leaf material of every committed tree (§2.7) MUST be published to the log or to such a mirror — retrievable and enumerable in full, with authenticated binding to the anchored root, for the retention period.

Recomputation of closure MUST NOT depend on the producer’s cooperation. A verifier can therefore reconstruct the complete corpus up to any witnessed checkpoint without producer cooperation for entries, and with mechanically checkable completeness for tree material.

4. Point-in-Time Reconstruction

Reconstruction is parameterized by two independent coordinates: an as-of checkpoint C, which fixes the knowledge boundary to statements with entry index less than tree_size(C), and a valid time T, the domain time asked about. The answer produced is “as known at C, about T”.

  1. Fix C, which SHOULD be witnessed. Enumerate the statements concerning the record (ds, r) with entry index less than tree_size(C): its ingestion or derivations, and the effective triggers naming it or, transitively, its inputs.
  2. Determine the effective status for T at C by applying those triggers whose scope covers T. Among conflicting effective triggers committed by C, the one with the greatest entry index governs. Corrections anchored beyond C are invisible at C by construction; re-running the procedure at a later checkpoint shows how knowledge evolved.
  3. Resolve the asserted derivation context: input commitments, representation digests and transform digests, each under the manifest version its statement references.
  4. Verify all of it: signatures against the key set as of each statement’s entry index; inclusion against C; consistency from C to the latest witnessed checkpoint; and manifest lineage back to genesis.

Boundary. Reconstruction yields the evidenced assertion set, not the data itself. Reproducible reconstruction — the ability to re-execute the asserted derivation — is an optional, manifest-declared property that requires retention and retrieval of the referenced artifacts and of the canonical input and output bytes for the declared period. Erasure of any required content terminates the property for the affected records, and a reconstruction result MUST report the property as terminated rather than silently degrading.

5. Revocation and Propagation

5.1. The Affected Set

For an effective trigger on (ds, X) with scope S, evaluated at a checkpoint C that commits the trigger, the affected set is the transitive closure over derivations with entry index less than tree_size(C) whose inputs match (ds, X), then over the consumers of those derivations’ outputs, and so on, filtered by S. The trigger’s scope applies to every seed.

The seeds themselves are never members of the affected set: a seed is the record the trigger acts on, and the trigger is its disposition; the affected set is what derives from the seeds, transitively.

Seeding rules:

  • For a retraction on (ds, X), the seed set is exactly {(ds, X)}. A retraction never seeds superseded replacements.
  • For a correction X to Xnew, the replacement Xnew is never itself a closure seed.
  • If a later correction of the same original X supersedes an earlier correction X to Xold, the later correction’s closure seeds include X and every previously superseded replacement Xold.
  • A correction targeting Xold independently starts closure at Xold.

5.2. Obligations by Level

L3. Within the propagation window declared in the manifest, measured from the trigger’s log-attested incorporation time, the producer computes the affected set at a checkpoint committing the trigger, dispositions every member with evidence (§2.4.4), and anchors the propagation statement. Completeness is relative to the declared checkpoint D. Later consumption of affected descendants may enlarge the closure past D and creates fresh propagation duties for the enlarged set.

L2. A producer MUST anchor its own triggers. L2 carries no closure duty, and claims about an L2 deployment MUST state “revocation recorded, not propagated” verbatim.

5.3. Completeness, and Its Boundary

Completeness is verifiable at L3 only. At L3 a verifier reconstructs the corpus up to the declared checkpoint — the availability requirements of §3.4 make this possible without the producer’s cooperation — recomputes the affected set, and compares the result against the anchored disposition tree. Both computations run over the same anchored statements, so disagreement is decidable.

At L1 and L2 no availability duty applies: entries need not be retrievable independently of the producer, and committed tree material need not be published at all. Nothing in this document supports a completeness claim below L3.

What this does not establish is that derivations outside the corpus do not exist. That is the manifest’s coverage assertion, auditable by comparing the declared inclusion and exclusion lists against the organization’s actual systems. AHL converts “is propagation complete?” into two questions: is it complete relative to the declared corpus?, which is cryptographically checkable, and is the declared corpus the real corpus?, which is an auditable scope assertion.

5.4. Cycles

Derived attributes that feed later training data create cycles, and the statement graph makes them visible. Closure computation MUST detect cycles, MUST NOT loop, and dispositions each record once. Producers SHOULD surface cycles: a cycle means that apparently independent corroboration may be self-derived, which is precisely what an auditor needs to see.

6. Conformance

6.1. Levels

LevelCumulative requirementsProperty
L1Signed statements for every covered output; ingestions for consumed sources; own triggers issued; retention per the manifest; manifest binding by signed reference (§2.2)Non-repudiable provenance exists
L2Anchored in a log satisfying the contract, within the declared anchoring window; manifest lineage anchored; rotation-anchoring proof for every governance-key rotation, log or witness (§7.5.1); claims state “revocation recorded, not propagated”Tamper-evident history
L3Witnessed checkpoints (§3.3); L3 availability (§3.4); every rotation-anchoring proof additionally cosigned under the OUTGOING witness set, whichever set rotated (§7.5.1); propagation obligations (§5.2) met within the declared window; completeness verifiable (§5.3)Independently verifiable; revocation-complete relative to the declared corpus

6.2. The Corpus Manifest

The manifest is anchored as a manifest statement (§2.4.5). Its machine-readable payload contains at minimum:

  • Producer id and producer key set. A manifest’s producer key array is the complete producer-key snapshot effective from that manifest’s entry index: it discards the prior snapshot, and later key statements then modify it in entry order until the next manifest version. Each entry is a producer key object {key_id, pubkey} — both family strings; pubkey decodes to exactly 32 octets; key_id equals sha256: plus the lowercase hex SHA-256 of those octets, so it is recomputable rather than merely declared. A producer key object carrying any member beyond those two is a schema failure. The shape deliberately differs from the log and witness key objects below: a log or witness key object needs a per-key index because a manifest MAY list such a key as valid from a later index, while a producer key needs none — the array IS the producer key state at the manifest’s entry index.
  • Log: id, operator, adaptor: {id, hash}, checkpoint cadence, witness_grace_period, and the log’s checkpoint-signing key objects {key_id, pubkey, valid_from_index}.
  • Witnesses: at L3, witness key objects {witness_id, key_id, pubkey, valid_from_index}. Log and witness key rotation is performed by anchoring a new manifest version — the manifest chain is the rotation mechanism for them, as key statements are for producer keys. Each version’s log and witness key objects replace the prior set in full. A manifest version that replaces either set is a GOVERNANCE-KEY ROTATION, and a receipt carrying it must additionally carry a rotation-anchoring proof under the outgoing states (§7.1, §7.5.1); a manifest signature alone does not establish either set.
  • Datasets: for each dataset id, a canonicalization descriptor (§2.6), a commitment mode, a key-access rule, and a dataset authority { "producer": "<id>", "key_ids": [...] }. In the core the authority’s producer MUST equal the manifest producer. Authority MAY be omitted only for datasets with no ingestion statements in corpus scope; an ingestion into an authority-less dataset is invalid.
  • Pipelines: the covered transforms, expressed as inclusion and exclusion lists. This is the scope boundary.
  • Windows: anchoring and propagation. Retention: for statements, and for artifacts if reproducible reconstruction is claimed. Level and any optional properties claimed.

Statements bind to their manifest version (§2.2), so changes to declared scope are visible on the face of the manifest chain.

6.3. Canonicalization Identifier Conformance

Two questions are settled here and MUST NOT be conflated: what a PRODUCER may put in a manifest, judged at publication time when a current registry is at hand, and what a VERIFIER does with what it finds, judged offline, years later, from carried material alone.

Producer conformance. A dataset’s canonicalization identifier MUST be syntactically valid (§2.6) and MUST be either registered in the “AHL Canonicalization Identifiers” registry (§10.3) at the time the manifest is anchored or a private-use identifier beginning x-. Occupying a plain, unregistered name is a conformance violation by the producer. It is NOT a verifier obligation, and a verifier MUST NOT attempt to discharge it.

Verifier resolution, offline.

Identifier stateRequired outcome
Syntactically invalid dataset declaration — an identifier violating the identifier syntax, a media_type violating the descriptor media-type production, or a dataset id violating its syntax or containing a control octetThe manifest is REJECTED and the receipt’s result is invalid — not merely the affected dataset’s claims
Syntactically valid descriptor, and this verifier implements the procedure the identifier names for this corpusNormal verification of that dataset’s content binding. For an x- identifier, “for this corpus” means configuration keyed on (genesis_entry_id, identifier), and the receipt carries canonicalization_namespace: "private-use"
Syntactically valid descriptor, and this verifier does not implement the procedureThe content-binding FINDING for that dataset is unverifiable. The verifier MUST NOT accept the asserted content_binding, and MUST NOT rehabilitate the receipt by treating it as content_binding: "none". Nothing else in the receipt is affected

The first row is decidable by every verifier alike from the carried bytes; the second and third are capability-gated. None of the three depends on a registry snapshot. A verifier’s result MUST NOT depend on whether an identifier appears in the registry at all, nor on an entry’s Status: a receipt carries no registry state, so a rule consulting one would make a historic receipt’s verdict a function of the verifier’s snapshot date. An identifier registered as obsolete verifies exactly as if active.

Rejecting a whole MANIFEST is reserved for the syntactic row for a second reason: manifest lineage is a chain validated from genesis, so a rejection propagates FORWARD through every later version. A snapshot-dependent rejection would let a single manifest version declaring a single never-used dataset id retire a producer’s entire anchored evidence base at the moment a registry changed.

Where content-evidence fields appear, the material carries the COMPLETE descriptor. For each receipt object, including each embedded one, both members MUST equal the declaration in the manifest version named by THAT object’s subject statement’s manifest member — a member authenticated by §7.6 and not merely copied — and not the version governing the receipt’s checkpoint. A mismatch in either member makes the receipt invalid; it is never downgraded.

7. Evidence Receipts

The AHL Evidence Receipt is the portable verification artifact: a versioned, JCS-canonical container that proves a declared claim offline, years later, without access to the producer or the log. Receipts use the file extension .ahl and the media type application/ahl-receipt+json (§10.1). Section 7 of the I-D is self-contained and normative; the companion container document carries non-normative detail.

7.1. Container

{ "ahl_receipt_version": "2", "spec_version": "0.4.0", "claim": { "type": "<registry id>", "record_subject": { "dataset": "...", "record": "..." }, "assurance": { ... }, "note": "<optional, informative only>" }, "subject": { "statement_id": "sha256:<hex>", "entry_id": "sha256:<hex>", "entry_index": 142, "manifest": "sha256:<manifest version id>" }, "envelope": { "payload": { ... }, "signatures": [ ... ] }, "keys": { "log": [ ... ], "witness": [ ... ], "producer": [ ... ] }, "anchoring": { "adaptor": { "id": "<profile name>", "hash": "sha256:<hex>" }, "checkpoint": { "log_id": "...", "tree_size": 1450, "root_hash": "sha256:<hex>", "checkpoint_time": "<RFC 3339>", "key_id": "sha256:<hex>", "signature": "base64:<...>", "raw": "base64:<optional adaptor form>" }, "inclusion_path": [ "sha256:<hex>", ... ], "witnesses": [ { "witness_id": "...", "key_id": "sha256:<hex>", "cosignature": "base64:<...>", "cosigned_at": "<RFC 3339>" } ], "later_checkpoint": { ... }, "consistency_path": [ "sha256:<hex>", ... ], "later_witnesses": [ { ... } ] }, "governance": { "genesis_entry_id": "sha256:<hex>", "chain": [ { "envelope": { ... }, "entry_index": 0, "inclusion_path": [ "sha256:<hex>", ... ] } ], "rotation_proofs": [ { "manifest_entry_index": 812, "checkpoint": { ... }, "inclusion_path": [ ... ], "witnesses": [ ... ] } ], "currency": { "mode": "declared | enumerated", "material": { ... } } }, "claim_material": { ... }, "anchors": [ { "type": "rfc3161 | bitcoin_ots", "target": "checkpoint_root", "target_hash": "sha256:<hex>", ... } ] }

Byte-carrying members. pubkey, signature, cosignature, raw, record_bytes, output_bytes, and enumeration material’s adaptor_form are base64: family strings; every other non-digest, non-integer, non-timestamp, non-token member is a sha256: family string. The strict acceptance rule of §2.1 applies; a failure is a schema failure and the result is invalid.

keys. A log or producer key object is {key_id, pubkey, source, binding}; a witness key object additionally carries witness_id. source is exactly one of "manifest-chain" or "local-policy". binding is { "entry_index": <integer> }, REQUIRED where source is "manifest-chain". Every key used in verification MUST appear in keys with its source and its binding. A manifest-chain key MUST match a key object in the manifest version its binding names — equality of every member the two objects share, and for a producer key the verifier MUST also recompute key_id from pubkey rather than trust the pair as presented. For log and witness keys the binding MUST identify the manifest version active for the checkpoint being verified: the manifest statement with the greatest entry index STRICTLY SMALLER than that checkpoint’s tree_size. The bound is strict because a checkpoint of tree size n commits exactly [0, n), so a manifest anchored AT index n cannot govern it. source: "local-policy" is acceptable only for witness keys the verifier already trusts, for the genesis anchor, and for authorized dataset keys.

anchoring.checkpoint is a SUPERSET of the checkpoint of §1.5: it adds key_id, naming the entry in keys.log[] whose pubkey verifies it, and signature. It MAY carry raw, the adaptor’s own binary or textual form; where present the verifier MUST check that it parses to the same values as the JSON members, which govern, and a mismatch is invalid.

anchoring.later_witnesses[] is present if and only if later_checkpoint is carried, and each element cosigns later_checkpoint rather than anchoring.checkpoint, validated under the manifest version active for later_checkpoint. At L3 a receipt asserting continued_history MUST carry at least one element that verifies; every carried element is validated and any that does not verify is invalid. The consistency path establishes that later_checkpoint extends anchoring.checkpoint; only its cosignatures establish that a witness saw it.

A producer MUST NOT assert continued_history where any manifest statement lies at an entry index in [anchoring.checkpoint.tree_size, later_checkpoint.tree_size). Governance material in a receipt reaches the anchoring root only, so a manifest anchored in that window has no place in the receipt and a verifier cannot decide from a receipt alone whether one exists. The obligation is the producer’s, and it is auditable: an auditor holding the log’s entries in that window, authenticated against later_checkpoint.root_hash, finds any such manifest by inspection. A receipt asserting continued_history across one is a defective receipt in the same sense as any other false assertion of the producer — the receipt’s own result is unaffected, and the defect is the auditor’s finding against the producer.

governance.chain[]. Each element is {envelope, entry_index, inclusion_path} — an anchored manifest statement’s complete envelope, the index at which it is anchored, and its inclusion path to the receipt’s checkpoint. Elements appear in ascending entry_index order and begin with the genesis manifest, whose entry id MUST equal governance.genesis_entry_id.

governance.rotation_proofs[] is REQUIRED IF AND ONLY IF the carried chain contains a GOVERNANCE-KEY ROTATION — a manifest version whose LOG checkpoint-signing key objects OR whose WITNESS key objects differ from its predecessor’s — and carries one element per rotation in ascending manifest_entry_index order. Either set alone is enough, because either substitution defeats a guarantee this document makes (§8.3). “Contains” means the chain AS CARRIED: under declared governance a manifest may be omitted, so this rule proves the rotations a receipt presents and is silent about any it does not. Each element carries:

  • manifest_entry_index, which MUST equal the entry_index of that manifest’s own chain element;
  • checkpoint, in the receipt-borne form, whose tree_size MUST be GREATER than manifest_entry_index and which MUST verify under a key of the OUTGOING log key set;
  • inclusion_path, proving the rotating manifest’s entry id at that index to this element’s checkpoint.root_hash — note that it runs to the ROTATION checkpoint’s root, not to anchoring.checkpoint.root_hash;
  • witnesses, REQUIRED AT L3, where at least one cosignature MUST verify under a key of the OUTGOING witness key set. At L3 a change to EITHER set is attested under BOTH outgoing states, because what is sought is the attestation of the authorities being retired that the handover happened.

Key binding for rotation material: a transition exception. A rotation_proofs[] checkpoint cannot satisfy the general binding rule — its tree_size exceeds the rotating manifest’s entry index, so the version active for it is the rotating manifest or later, while the key required is the predecessor’s. For a rotation_proofs[] element ONLY, its log and witness keys bind to the manifest version active IMMEDIATELY BEFORE manifest_entry_index. The exception is safe: it applies to rotation material and nothing else, and it is STRICTLY HARDER to satisfy than the general rule, which would accept a signature by the INCOMING key — exactly the key an attacker installs.

A receipt that omits rotation_proofs[] where the carried chain rotates either governance key set, or that carries an element failing any requirement above, is invalid: this is material the receipt MUST carry, and its absence is not a capability the verifier lacks.

Revision and rule selection. Receipts conforming to this revision carry ahl_receipt_version: "2" and spec_version: "0.4.0", and every statement they carry declares ahl_version: "0.4". The version members are not a selector among rule sets; their whole job is to make refusal immediate and unambiguous. A verifier MUST read ahl_receipt_version and act on it BEFORE any other check, including schema validation — any other value yields unverifiable and no further processing. Each carried statement’s ahl_version is likewise checked before validating that statement, except an entry an enumeration alone carries, which is exempt until its own-index signature check has passed. Neither outcome is invalid.

7.2. Claim Types

A receipt declares its claim type, and proves exactly that claim.

Claim typeProvesRequired claim_material and mode
statement-anchoredThe subject envelope is anchored at an index under a checkpoint and signed under the declared manifest chain. Applies to any statement type, manifest, key and propagation statements included{}; declared permitted
record-ingestedThe record was introduced by the subject ingestion statement{ "record_bytes", "canonicalization" } present iff content_binding is not none, with media_type iff the descriptor requires it. record_bytes carries the record AS RECEIVED, base64-encoded, NOT its canonical form; verification APPLIES the descriptor’s procedure and recomputes the commitment with the descriptor digest in the preimage. declared permitted
record-derivedOne output record’s derivation is committed by the subject derivation, batched or notUnbatched: { "output": { "dataset", "record" } }, matching an entry in envelope.payload.outputs. Batch: additionally { "batch_leaf", "leaf_index", "leaf_path" } to outputs_root, and input_members only where batch_leaf.inputs is the input-set form. Either form carries { "output_bytes", "canonicalization" } on the same terms as record-ingested. declared permitted
trigger-declaredA trigger naming the record is anchored and its envelope is valid under §2.1, signed by the declared issuer{ "introduction": <embedded introduction receipt>, "replacement_introduction": <corrections only> }; declared permitted
trigger-effectiveAdditionally: at least one verified signer held authority under enumerated governance at the trigger’s entry index, and this trigger governs at checkpoint Ctrigger-declared material plus { "checkpoint_C", "competing": { "corpus_range" } }. The range MUST be [0, tree_size(C)), or [introduction_index, tree_size(C)) where the embedded introduction receipt fixes that index. Every carried purported competing-trigger envelope MUST be verified under §2.1 before authority is compared; one that does not verify is void — never a challenge, never effective, and not a defect of this receipt. checkpoint_C MUST match the verified anchoring.checkpoint on {log_id, tree_size, root_hash}. REQUIRES governance: "enumerated" and competing_triggers: "enumerated"
disposition-declaredA propagation statement anchored under the declared chain dispositions the record{ "trigger": <embedded trigger-declared receipt>, "disposition_leaf", "leaf_index", "leaf_path" } to affected_root. leaf_index is REQUIRED: a Merkle path is verifiable only against the leaf’s position. declared permitted
disposition-effectiveAs above, with an embedded trigger-effective receiptSame material; REQUIRES governance: "enumerated"
propagation-completeThe propagation statement’s affected set equals the closure recomputable at the propagation’s declared corpus checkpoint D, and never at a later checkpoint{ "corpus_checkpoint": <D, authenticated by a consistency proof from D to the receipt's checkpoint or by recomputation of D's prefix root>, "corpus_prefix": <the §7.4 enumeration form for [0, tree_size(D))>, "trees": { ... } } for every batch, input-set and disposition root referenced in the prefix. REQUIRES an embedded trigger-effective receipt and governance: "enumerated"
governance-stateThe manifest and key state at a target index is exactly the presented chain{ "target_index" }, with anchoring.checkpoint as the enumeration checkpoint. The subject MUST be the manifest statement claimed active at target_index, with subject.entry_index no greater than it, and the enumerated material MUST prove that no manifest or key statement exists in (subject.entry_index, target_index]. REQUIRES governance: "enumerated"

record_subject is REQUIRED for the record-*, trigger-* and disposition-* types and MUST be absent for statement-anchored and governance-state, which targets an index instead.

Naming is disciplined by rule: types suffixed -declared carry declared governance and never use the words “effective”, “governs” or “complete” in a rendered verdict; types suffixed -effective or -complete REQUIRE enumerated governance.

Why checkpoint_C compares three fields and not four. {log_id, tree_size, root_hash} determine the COMMITTED TREE STATE. checkpoint_time is not identity — it distinguishes REPUBLICATIONS of one state, and a log publishing at a declared cadence republishes a quiet log’s unchanged tree_size with a fresh time. The comparison is also deliberately CLOSED at these three, so that a future extension member is not accidentally made semantic.

A propagation-complete receipt carries the authenticated corpus prefix through D together with the full leaf material of every referenced tree. There is no compact completeness receipt, by construction.

7.3. Assurance Fields

Assurance is expressed in structured fields rather than in prose. Those fields state what the PRODUCER asserts the receipt supports: they are written when the receipt is issued, they are static, and they are not a verdict.

  • governance: declared or enumerated (§7.4).
  • competing_triggers: not-checked, or enumerated, meaning that all triggers for the subject record through checkpoint C are carried and the governing one is established by entry index.
  • witnessed: at least one valid witness cosignature on the inclusion checkpoint.
  • continued_history: a later checkpoint, its cosignatures in anchoring.later_witnesses[], and a valid consistency proof are present; at L3 at least one of those cosignatures verifies.
  • content_binding: none; plain-verified; or keyed-authorized, recomputed with a verifier-held dataset key. Dataset keys are never packaged in a receipt. In both non-none cases the VERIFIER runs the canonicalization itself, because the carried bytes are the record as received: what is established is “the record I hold canonicalizes to a preimage committing to C”, not merely “these bytes hash to C”.
  • canonicalization_namespace: REQUIRED where content_binding is not none, and absent otherwise. private-use where the carried identifier begins x-, public otherwise. It names only the namespace: public asserts nothing about registration, and nothing in a receipt does.

A verifier MUST render its verdict from the claim type and the assurance fields TOGETHER WITH its result (§7.7), and MUST NOT report anything stronger. An assurance the verifier could not evaluate MUST NOT be rendered as though it had been established. A receipt whose assurance fields disagree with its own material is invalid and is never downgraded.

7.4. Governance Currency Modes and Enumeration Material

  • declared: chain validity from genesis only. Compact. The active governance state at the subject’s entry index is not independently proven. Permitted for statement-anchored, record-ingested, record-derived, trigger-declared and disposition-declared.
  • enumerated: additionally, an authenticated range enumeration over exactly [0, tree_size(C)), proving that the presented governance statements are the only VERIFYING manifest and key entries in that range — a void entry is not a governance statement and its absence from the chain is not an omission. REQUIRED for trigger-effective, disposition-effective, propagation-complete and governance-state.

Declared mode and producer-key transitions. governance.chain[] carries manifest statements; producer-key transitions are key statements, and those reach a verifier only through enumeration material. Where a declared-mode receipt’s envelope names a producer key that a key statement ADDED after the manifest version the subject binds to, or that such a statement RETIRED while the manifest still lists it, the induction never sees the transition. Such a receipt is unverifiable, not invalid: the omitted transition is not material this mode required the receipt to carry, and a verifier holding the enumerated material would verify the same bytes. Correspondingly, a producer intending its receipts to be verifiable in declared mode MUST anchor a manifest version snapshotting the current producer key set before issuing them. In a corpus that rotates producer keys between manifest versions and does not snapshot them, declared mode is materially weaker than it looks.

In a propagation-complete receipt two ranges deliberately coexist: governance and competing-trigger evidence cover [0, tree_size(A)), because authority is judged against current knowledge, while the completeness prefix covers [0, tree_size(D)), because completeness is defined at the declared checkpoint.

Enumerated receipts are large. That is the honest cost of the claim until an adaptor capability for typed governance sub-trees is specified. Enumeration material takes this canonical inline form:

{ "range": { "from_index": 0, "to_index": 1450 }, "entries": [ { "entry_index": 57, "envelope": { ... } } ], "range_proof": { "adaptor_form": "base64:<authenticated proof that `entries` is the complete, in-order entry set of `range` under the checkpoint>" } }

7.5. Verification Algorithm

Steps 1 through 3 are key-independent and run in order; step 4 is an INDUCTION; steps 5 through 7 follow it.

  1. Version first, then parse. Read ahl_receipt_version and act on it before any other check, including schema validation. Then parse the receipt, enforce the resource limits of §7.8 — distinguishing the fixed limits, which are invalid, from the verifier-local budgets, which are unverifiable and name the budget and the value in force — and recompute statement_id and entry_id from the carried envelope.

  2. Resolve the adaptor profile by id and hash from local possession. The two failure cases are not the same failure. Possessing NO profile under that id is a missing capability and the result is unverifiable. Possessing a profile under that id whose HASH DIFFERS is a disagreement decidable from the bytes in hand, and the result is invalid. Where anchoring.checkpoint.raw is carried, verify that it parses to the same values as the JSON members; a mismatch is invalid.

  3. Key-independent structural and path checks. No signature and no cosignature is verified in this step. The subject’s entry_index is less than the checkpoint’s tree_size, and anchoring.inclusion_path recomputes from subject.entry_id at that asserted index to anchoring.checkpoint.root_hash; EVERY governance.chain[] element’s inclusion_path recomputes from that element’s envelope entry id at its asserted index to the same root; consistency_path recomputes where continued_history is asserted; and the family-string, arity and ordering checks of §7.1 hold. A failure is invalid.

    The governance-chain elements are checked HERE, not inside the induction, because §7.5.1 walks them in ascending entry-index order and every activity test is “at index i”: an unproven entry_index would let a producer present a chain in an order the log never had. The path proof IS the index proof. At this point root_hash is an UNAUTHENTICATED STRUCTURAL COMMITMENT; a verifier MUST NOT report any result from this step alone, and it is 4f that upgrades every path result here from a statement about carried bytes to a statement about the log’s state.

    Why this is not circular: there are TWO inductions, not one. Trust flows from the LOCALLY CONFIGURED genesis anchor (4a) and never from the checkpoint. The first induction is over PRODUCER keys (4b). The second is the GOVERNANCE-key induction, over the log and witness key sets together, and it is what makes 4f’s key resolution safe: the genesis sets are pinned by entry-id equality, and each subsequent set is trusted only where its introducing manifest’s own anchoring has been proven under the OUTGOING states. Without it the gap would be exactly at the join — a manifest is signed by a PRODUCER key yet replaces the LOG and WITNESS key objects in full (§8.3).

  4. Governance bootstrap, as an induction (§7.5.1), which also fixes, by reliance, whose failure is invalid and whose makes the envelope void.

  5. Verify the claim material against §7.2, including embedded receipts recursively and enumeration material. Where content evidence is carried, APPLY the dataset’s declared canonicalization procedure to record_bytes or output_bytes — the record AS RECEIVED — and recompute the commitment with the descriptor digest in the preimage. A recomputed commitment differing from the one the subject statement names is invalid.

  6. Check the cross-field consistency rules of §7.6.

  7. Determine the result — verified, invalid, or unverifiable (§7.7) — and render the verdict from claim type and assurance fields together with that result, never stronger.

7.5.1. Governance Bootstrap

Establishing the key state and verifying the governance envelopes are ONE OPERATION, interleaved, and not two steps in either order: a governance-chain element is itself a carried envelope, so “verify the chain, then verify every carried envelope” either duplicates and contradicts itself or derives the key state from unauthenticated material. Two authenticity properties are separate here: lineage authenticity comes from signatures chained to the locally configured genesis anchor, and anchoring authenticity comes from the checkpoint (4f). The induction needs only the first.

4a. Base case. An offline verifier cannot authenticate a genesis anchor supplied by the receipt itself; it MUST compare governance.genesis_entry_id against independently configured policy. Three outcomes follow: no configured anchor for this log — the verifier lacks a configuration, not evidence, and the result is unverifiable; configured and DIFFERENT — the receipt is evidence about a corpus this verifier is not configured to accept, and may be a perfectly valid receipt of that other corpus, so the result is unverifiable reported as an anchor mismatch naming both values; configured and equal — verification proceeds.

Recompute the entry id of the first chain element and require it to equal the configured anchor. That equality alone authenticates the genesis envelope IN FULL, payload and signatures together, because an entry id is SHA-256(JCS(envelope)) — no key is needed, which is what makes the base case genuinely basal. Where local policy holds initial key fingerprints they MUST match those the genesis manifest declares; a mismatch means the verifier’s own policy is internally inconsistent, so the result is unverifiable, reported as a configuration fault and not as a defect in the receipt.

The genesis manifest is INSIDE the typed checks: it takes the manifest validation of 4b(M) on the same terms as any later version, earning exactly two exemptions — from the predecessor linkage rule, since a predecessor is forbidden for genesis, and from signature derivation under a prior key state, since entry-id equality has already bound its complete bytes. Only after all of those pass does the genesis key state become K.

4b. Inductive step. Walk the carried governance statements after genesis in ascending ENTRY-INDEX order: the manifest statements of governance.chain[], merged in entry-index order with the key statements the enumeration carries. An entry the enumeration alone reveals is selected by its purported type but ENTERS the induction only if its envelope verifies in phase 1 under K as established so far: a purported manifest or key entry that does not verify is void — not inducted, no effect on K, the walk continues past it — and is reported as an informative item naming its index. A governance.chain[] element is different: the receipt presents it as its own lineage, so its phase-1 failure is invalid. A VERIFYING enumerated manifest entry of this revision that is absent from governance.chain[] is an omission and is invalid. A VERIFYING governance entry declaring an ahl_version this revision does not define is neither: it is not inducted, K is unestablished at and after its index, the governance finding is unverifiable, and a later required invalid still dominates.

Each statement is processed in THREE PHASES, in this order, for both types:

  1. Signature. Verify the envelope under §2.1 against K AS ESTABLISHED SO FAR — the governance state in force immediately before this statement’s own entry index.
  2. Type-specific validation, per 4b(M) or 4b(K).
  3. Effect. Only after phases 1 and 2 have BOTH passed.

A phase-2 failure is invalid, and the induction does not continue past it: a verifying statement the protocol cannot interpret is signed corpus material, not noise. The phase order is load-bearing, and the reason is attacker-driven cost: type-specific validation MUST NOT run on material whose signature has not verified, or anyone able to hand a verifier a receipt could drive descriptor resolution, base64 and key decoding, and manifest semantics on bytes no key vouches for.

4b(M) — a manifest statement’s phase-2 validation. Validate against §6.2. Resolve every canonicalization descriptor under §6.3: a syntactically invalid descriptor REJECTS the manifest and is invalid, while an identifier this verifier does not implement affects only that dataset’s content-binding finding, which is unverifiable. Check the predecessor linkage — it MUST equal the entry id of the preceding manifest in the chain, is REQUIRED for non-genesis and forbidden for genesis, and a failure is invalid. This is what makes lineage a chain rather than a set.

The rotation-anchoring rule, also phase 2. Where this manifest’s LOG checkpoint-signing key objects OR its WITNESS key objects DIFFER from its predecessor’s, it is a GOVERNANCE-KEY ROTATION, and a manifest may be trusted to introduce either set only where its own anchoring is proven under the OUTGOING states. The verifier locates its rotation_proofs[] element by manifest_entry_index and requires all of the following; any failure, and the absence of the element itself, is invalid:

  • the element’s checkpoint verifies under a log key of K AS ESTABLISHED SO FAR — the outgoing log set;
  • its tree_size is greater than this manifest’s entry index;
  • its inclusion_path recomputes from this manifest’s envelope entry id, at that entry index, to that checkpoint’s root_hash;
  • AT L3, at least one of the element’s witnesses cosignatures verifies under a witness key of that same outgoing state, whichever set changed. Without it a rotation would turn on the log operator alone, and L3 would buy nothing over L2 at exactly the point where it should buy most.

Phase 2 is where this check belongs, because the outgoing states are in hand there: phase 3 replaces the log and witness key objects in full.

Phase-3 effect for a manifest: it replaces the log and witness key objects in full and installs a complete producer-key snapshot, discarding the prior one.

4b(K) — a key statement takes no manifest checks, and is not thereby unvalidated. No §6.2 validation, no §6.3 descriptor resolution, no predecessor linkage: it declares no datasets and has no lineage of its own. Its phase-1 signature is the rule that it MUST be signed by a key valid in the state established so far. Its phase-2 validation is its own form, against §2.4.6, and MUST run before the effect is applied: type is exactly key; action is exactly one of add or retire, with no third value and no default; the key object carries key_id, pubkey and valid_from; both family strings are well formed and pubkey decodes to exactly 32 octets; key_id EQUALS sha256: plus the lowercase hex SHA-256 of those octets, recomputed rather than trusted; and valid_from is a well-formed RFC 3339 timestamp — INFORMATIVE DOES NOT MEAN OPTIONAL, and a missing or malformed one is invalid. Phase-3 effect: add or retire modifies the PRODUCER key set in entry order. A key statement NEVER changes log or witness keys.

4c. Termination, and what K means in each mode. The induction runs until it has covered every index the receipt needs a key state for. Under declared governance, K is the key state THE PRESENTED CHAIN IMPLIES and no more: it does not establish that nothing was omitted, since the induction cannot see an absence. A declared-mode result MUST NOT speak of the ACTIVE governance state at any index. Under enumerated governance the range proof over exactly [0, tree_size(C)) forecloses omission, so K at each index IS the state that was in force. Only enumerated mode earns the word “active”.

4d. Remaining carried envelopes, and the reliance rule. With K established, verify every carried envelope that is not part of the induction — the subject’s, each embedded receipt’s, every purported competing-trigger envelope’s, and every entry carried solely by an enumeration — under §2.1, each at THAT ENVELOPE’S OWN entry index.

What that failure means for the RESULT is decided by reliance, not by presence. For an envelope the receipt itself rests on — the subject’s, each embedded receipt’s subject, and every governance.chain[] element — failure is invalid. For every other carried envelope a non-verifying envelope is VOID: excluded before any authority comparison, never effective, never traversed, no effect on the result, and reported as an informative item naming its entry index. The reason is the log contract: a log anchors opaque bytes and validates none, so were a void entry a defect of every later receipt, any party able to anchor one envelope could disable every enumerated claim of that log from that index on. The range proof still proves the enumeration complete, so voiding hides nothing.

4e. Authorization, separate and strictly after 4d. Applied only to envelopes already valid under 4d, and only where the claim depends on authority: a trigger is authorized if and only if at least one of its verified signers holds a key in the applicable authority key set, active at the trigger’s own entry index. A trigger whose envelope does not verify is void and never effective, whoever signed it, and it is not a challenge. A valid trigger with no verified signer in the authority key set is a challenge, not a defect.

4f. Authenticated checkpoint validation. Verify anchoring.checkpoint.signature under the keys.log[] entry its key_id names, and every anchoring.witnesses[] cosignature under the keys.witness[] entry its key_id names, each key’s source and binding first validated per §7.1. 4f MUST NOT resolve a checkpoint-verification or cosignature-validating key from a manifest version whose log or witness key set was not established by the governance-key induction — that is, from a rotating manifest whose rotation-anchoring rule at 4b(M) did not pass. Where continued_history is asserted, later_checkpoint and its cosignatures are validated the same way against the manifest version active for ITS tree size. Only on passing this step do the path results of step 3 become claims about the log’s state rather than about carried bytes.

Dependency graph.

4a -> 4b -> 4c -> { 4d -> 4e , 4f }

4a, 4b and 4c are strictly sequential, and 4b is internally ordered by entry index. The only pair with no dependency between them is the 4d -> 4e branch and 4f; a verifier MAY run them in either order or concurrently.

7.6. Cross-Field Consistency

Each of the following is a disagreement among fields the receipt itself carries, decidable from the receipt alone and identically by every verifier. A receipt failing any of them is invalid; none is ever a capability gap, and none is downgraded.

  • assurance.governance equals governance.currency.mode.
  • assurance.witnessed is true if and only if at least one witness cosignature verifies.
  • assurance.continued_history is true if and only if later_checkpoint, later_witnesses and consistency_path are present and verify, with at least one element of later_witnesses verifying at L3.
  • assurance.competing_triggers is enumerated only where the range required by §7.2 is present.
  • assurance.content_binding other than none occurs only with the content evidence the claim type requires.
  • assurance.canonicalization_namespace is present if and only if content_binding is not none, and is private-use if and only if the carried identifier begins x-.
  • Every embedded receipt’s record_subject and entry indexes match the referencing material — trigger to introduction record, disposition leaf to trigger record, correction to replacement introduction — with introduction index less than trigger index, and trigger index no greater than propagation index.
  • subject.entry_id and subject.statement_id equal the values recomputed from envelope, and subject.entry_index is the index at which the entry id is proven included, strictly smaller than the checkpoint’s tree_size.
  • subject.manifest equals the subject envelope’s payload.manifest for every subject other than a manifest statement. The payload’s member is covered by the subject’s signature; the receipt’s copy is not, so this equality is the only thing that authenticates the copy.
  • The manifest version named by subject.manifest is PRESENT in governance.chain and that element’s entry_index is strictly smaller than subject.entry_index. A named version absent from the chain, or anchored at or after the subject, cannot have governed it.
  • subject.manifest is absent for every manifest-statement subject, genesis and non-genesis alike.
  • In a propagation-complete receipt verifying two checkpoints, each checkpoint’s log key resolves against the manifest version active for that checkpoint. Byte equality between the two is never a substitute for validating both.

7.7. Verification Results

A verifier’s result over a receipt, for every verification run that RUNS TO COMPLETION, is exactly one of three values:

  • verified — the verifier established the asserted property from the presented material.
  • invalid — the presented material does not verify. This covers a malformed or non-JCS artifact, a claim-type and assurance combination the schema cannot satisfy, and a structurally well-formed receipt whose signatures or proofs fail.
  • unverifiable — the presented material neither establishes the asserted property nor contradicts it. The verifier lacks material, a capability, a local configuration or a local budget: a canonicalization identifier it does not implement, an artifact declaring an earlier revision, an adaptor profile it does not possess, a genesis anchor it has not configured, a dataset key it is not authorized to hold, or a declared-mode receipt resting on a producer-key transition that mode does not carry.

A run that does not complete — an I/O failure, an exhausted heap, a crash — yields no result in this model. It is a local execution failure; it says nothing about the receipt and MUST NOT be rendered as any of the three values.

Mapping rejections to results. Material the receipt MUST carry and does not; a cryptographic check that fails; a schema failure; a disagreement among carried fields — invalid, because all are decidable from the receipt’s own bytes, so every verifier decides them alike in every year. A capability the verifier lacks, a local configuration it has not been given, or a local budget it has set — unverifiable, because all are properties of the verifier and not of the artifact. The division is not stylistic: a verifier-local condition reported as invalid would let two verifiers make contradictory statements about one artifact.

A verifier never establishes the negation of a historic fact. An invalid result says that this artifact does not verify; it does not say that the subject was not anchored or that any other asserted fact is false. Only verified MAY be rendered in words that assert the property. No result may be represented by rewriting the receipt’s assurance fields.

Findings, and the reduction to a result. A verification run produces one finding — with the same three values — for each assertion the receipt REQUIRES: every assertion its claim type’s material requires under §7.2, together with the anchoring, envelope-validity, governance and cross-field checks of §7.5 steps 1 through 4 and §7.6; its content binding, if and only if its own assurance.content_binding is not none; and, for each embedded receipt, every required assertion of THAT receipt, with one exception: an embedded receipt’s CONTENT BINDING is never a required assertion of the receipt that embeds it. The exception holds because no claim type in §7.2 rests on an embedded receipt’s record bytes.

The reduction. A receipt’s result is invalid if any required finding is invalid; otherwise unverifiable if any required finding is unverifiable; otherwise verified. invalid dominates unverifiable because a demonstrated defect in required material is a fact about the artifact, while a capability gap is not.

Reporting. The scalar result is not the whole report. A verifier MUST report the findings alongside it, because the result alone does not say which assertion produced it, and a reader cannot act on unverifiable without knowing what was missing. A verifier MUST NOT present a finding as though it were the result.

Informative items. For each void entry it inspected (4d) the verifier MUST report one informative item carrying the entry index and the failure reason. Informative items are not findings: they belong to no required assertion, carry no result value, and never enter the reduction.

7.8. Resource Limits

Fixed limits are properties of the artifact, decided identically by every verifier in every year, so a receipt exceeding either is invalid: maximum embedded-receipt nesting depth 4, maximum embedded receipts per file 64.

Verifier-local budgets. A verifier MUST enforce a decoded-size budget and a verification-work budget, and MUST fail closed — never degrading to a partial check. These budgets are VERIFIER-LOCAL POLICY: no receipt member, manifest field or other declaration source sets them, this document states no value for them, and each verifier configures its own and MUST be able to state the values in force for a run. No floor is stated, because none follows from anything else here, and an arbitrary MUST is worse than none.

Exhaustion of either budget yields unverifiable, never invalid, and a verifier MUST report WHICH budget was exhausted and the value that was in force — unverifiable without that is not actionable.

Order dependence under exhaustion is accepted and stated rather than left to be inferred. Because exhaustion is unverifiable while a failed check is invalid, the result of a run in which a budget is exhausted can depend on which independent check ran first. This document does NOT impose determinism: imposing it would mean fixing a total order over checks §7.5.1 deliberately leaves independent, which would forbid concurrent verification and buy nothing.

Deduplication of embedded receipts MUST key on the digest of the JCS serialization of the complete embedded receipt object. An entry id alone is insufficient, because claim material is not determined by the envelope.

8. Security Considerations

8.1. Cryptographic Agility

This revision fixes SHA-256 [RFC6234] for digests and Ed25519 [RFC8032] for signatures. The security of statement identity, trees and commitments rests on the collision resistance of SHA-256; for keyed commitments the corresponding property of HMAC-SHA-256 under a known dataset key reduces to it by the nesting construction, and the secrecy of the dataset key is a separate, confidentiality property (§9). Algorithm agility, including posture toward post-quantum signatures, is not specified in this revision.

8.2. Key Management

Producer keys sign statements; log keys sign checkpoints; witness keys sign cosignatures. Producer key transitions are anchored key statements verified against the key set at their own entry index; log and witness key rotation is performed by anchoring a new manifest version. Because verification is always evaluated at an entry index, a key retired later does not retroactively invalidate statements it signed while valid, and a key retired by a later manifest version MUST NOT validate a checkpoint issued under that later state.

Recovery from producer-key compromise is not specified here. A party holding a compromised key can produce statements indistinguishable, by signature alone, from the legitimate producer’s, up to the index at which the key is retired; anchoring makes such statements visible and dated but does not make them false. Deployments SHOULD keep signing keys in hardware and SHOULD monitor their own corpus.

8.3. Log Integrity and Detection of Inconsistent Views

Consistency proofs establish append-only growth within the view presented to the verifier. An operator that presents inconsistent views to different parties is not detected by consistency proofs alone, which is why the witness protocol of §3.3 is required at L3. Refusal evidence published at BOOTSTRAP names one checkpoint and a reason rather than two conflicting ones, and MUST NOT be read as evidence of equivocation. Detection is not prevention. A log operator can refuse service, and refusal is visible but not remediable by this protocol.

Governance-key rotation. A manifest is signed by a PRODUCER key, yet each manifest version replaces the LOG and WITNESS key objects IN FULL. Producer-key trust alone would let a holder of a valid prior producer key install either set at will, and the two substitutions defeat two different guarantees.

Substituting the log key set attacks anchoring: the attacker signs a successor manifest carrying log keys it controls, places that manifest in a tree of its own construction, and signs that tree’s checkpoint with the installed key. Every individual check would pass — and no checkpoint of the real log would ever have anchored that manifest.

Substituting the witness key set attacks L3 independence and needs no forged log at all. The attacker leaves the log key set alone and simply replaces the declared witnesses with witnesses of its own; the cosignatures verify, and witnessed is asserted and confirmed — while the party attesting independence is the producer itself.

What defeats both is that log and witness keys form their own induction, rooted out of band (§7.5.1). The genesis sets are pinned by the entry-id equality that binds the whole genesis envelope, and every later set is trusted only where its introducing manifest’s anchoring is proven under the OUTGOING states. The forged log-key rotation fails there and cannot be repaired: producing that checkpoint needs the OUTGOING LOG key, a different key set from the producer keys the attacker holds.

What the witness arm does and does not establish is narrower than it may read. It makes a witness handover ATTESTED AND DATED by the outgoing, independent witnesses. Under ENUMERATED governance that means a set cannot be replaced silently, retroactively, or invisibly to a later verifier; under DECLARED governance the guarantee is narrower, since the proof is required only for rotations in the chain the receipt CARRIES. It does NOT establish that the incoming witnesses are independent: a producer that openly rotates to witnesses it controls, with the outgoing set’s cosignature on the anchoring, produces conforming material. Witness independence remains a declared property assessed against the verifier’s own trust policy. The rule converts an undetectable substitution into a detectable and attested one; it does not make the producer’s choice trustworthy.

Compromise of a log signing key itself is a different threat and is not addressed here. A witness stale beyond the declared grace period weakens detection to the age of its last cosignature, which is why staleness is a finding rather than a silent condition.

8.4. Authority and Coverage Limits

Validity and authorization are separate tests, applied in that order. A party without a valid key cannot dilute a statement by appending to it, and a verifier that accepted a subset of signatures would accept an envelope its declared signers did not all sign. The following limits are inherent to the design:

  • AHL establishes that a statement was signed by the holder of an identified key, binds to exactly the committed content, and was incorporated at a stated entry index. It does not establish that the statement is true.
  • AHL does not establish that unstated derivations do not exist. Coverage is the manifest’s assertion, made auditable by requiring inclusion and exclusion lists rather than silence.
  • Completeness of propagation is completeness relative to the declared corpus, at the declared checkpoint D, and no further.
  • An introduction proof inside a trigger receipt establishes who may retract a record. It does not establish the truth or completeness of that record’s own upstream provenance.
  • L3 reduces the trust placed in the log operator to detectability of inconsistent behaviour. It does not eliminate that trust.

8.5. Verification Resource Consumption

A verifier MUST enforce the fixed nesting and count limits and the verifier-local decoded-size and verification-work budgets of §7.8, and MUST fail closed — rejecting rather than degrading — on exhaustion. Exceeding a fixed limit is invalid; exhausting a local budget is unverifiable, and the verifier MUST name the exhausted budget and its value.

8.6. Descriptor Binding

The canonicalization descriptor is inside the commitment preimage, through ddig. DESCRIPTOR SUBSTITUTION CANNOT PRESERVE A COMMITMENT: a party reinterpreting a dataset’s records under a different canonicalization, or under the same canonicalization with a different media type, produces different commitments, and every trigger, disposition and closure edge naming the old ones ceases to match. The substitution shows up as a break in the record graph instead of passing silently.

That last claim is computational, not structural. The descriptor reaches the preimage only as the fixed-length ddig, so a substituted descriptor yields a different commitment under the collision resistance of SHA-256 and not otherwise. The construction adds no second failure mode beyond that one assumption, which is the strongest thing that can honestly be said for it.

What the verifier gains is detection, not disclosure. A digest does not reveal its input, and no verifier recovers a descriptor from a commitment. The verifier takes the descriptor from the receipt’s claim material and from the manifest version the subject names, recomputes ddig, recomputes the commitment, and compares. Descriptor stability becomes producer hygiene rather than a condition of soundness, because the verifier no longer has to ASSUME a descriptor it cannot check.

8.7. Formally Stated Properties (Informative)

This section is INFORMATIVE. It records which properties of the constructions above have been proved in a machine-checked development, under which assumptions, and which have not. It introduces no requirement.

The development is in Lean 4 (toolchain leanprover/lean4:v4.31.0) with no dependency beyond the Lean prelude. It contains no sorry and declares no axiom of its own; every result has at most propext and Quot.sound in its axiom footprint, with one exception noted below. The proofs artifact is to be published; the results are properties of an abstract model — octet strings, digests, an abstract hash, a finite derivation graph over record references, and the tree geometry of [RFC9162] §2.1 with the domain separation of §2.7 — and not of any source code.

Assumptions. Collision resistance of SHA-256 is a hypothesis nowhere in the development: injectivity of the hash would be false, so the results CONCLUDE an exhibited collision — a pair of distinct octet strings with equal digests. The same treatment applies to HMAC-SHA-256 under a known dataset key. Injectivity of [RFC8785] canonicalization on I-JSON values is the one assumption carried as a hypothesis, and every result consuming it says so. Unforgeability of Ed25519 enters no proof: signatures are not modelled, and envelope validity reaches the closure model only as a flag on an entry. Honest enumeration is not assumed.

8.7.2. Commitment preimage injectivity. preimage_injective is unconditional and constructive: over well-formed dataset ids, equal preimages give equal dataset ids, descriptor digests and canonical octets — §2.6’s “by parsing alone”, carried out. commit_plain_collision and commit_keyed_collision turn two distinct well-formed triples with one commitment into an exhibited collision. descriptor_digest_collision and commit_plain_descriptor_collision add the canonicalization-injectivity hypothesis; the latter is the one result whose axiom footprint also contains Classical.choice.

8.7.3. Affected-set well-definedness and determinism. No cryptographic assumption enters this group. closureReach_isLeastClosed and isLeastClosed_unique make the closure the least fixed point of the §5.1 operator, so “the” affected set is well defined however a verifier arrives at it; exists_stable, mem_closure_reach_iff and mem_affected_set_iff give termination, cycles being no obstacle since the iteration is over a set and not over paths; nodup_closure_reach and nodup_affected_at show the results duplicate-free. affected_of_prefix_eq gives order-freeness: two verifiers holding the same prefix compute the same affected set. dispositionsAgree is an executable Boolean function of two finite lists, so the comparison against the anchored disposition tree is an algorithm and not merely decidable in principle. affected_mono gives the enlargement of §5.2. seeding_rules_differ and affected_retraction_ne_correction exhibit a corpus in which a retraction and a correction at one and the same scope have different affected sets: the seeding rules of §5.1 do not collapse into one.

8.7.4. Log prefix, inclusion, and enumeration soundness. Every clause concludes the intended property OR an exhibited collision. consistency_sound — a verifying consistency proof shows the smaller entry list to be a prefix of the larger, which is append-only WITHIN THE VIEW SHOWN TO THE VERIFIER. inclusion_sound — a verifying inclusion proof shows the leaf to be the list’s i-th entry. range_sound — a verifying range proof shows the carried entries to be, in order, the entries at those indexes; within the model this is what makes a reconstructed corpus a complete prefix. affected_mono_of_consistency and enumerated_closure_eq compose the two groups.

8.7.5. What is not covered. Split-view; publication completeness; checkpoint signatures, governance and key compromise; authority and effectiveness; corpus coverage; canonicalization procedures and every parsing and serialization layer; disclosure and confidentiality; completeness (as opposed to soundness) of the [RFC9162] proof systems; cycle surfacing; and time, the scope predicate being abstract.

8.7.6. Relationship to the reference implementation. There is no extraction, no translation, and no refinement argument connecting any implementation to the definitions the results are stated over; names were aligned so the two can be read side by side, which is a convenience and not a proof. What connects them is empirical evidence: the published conformance vector corpus, which records what the implementation computes on named inputs at a named revision. A finite corpus does not establish that every path through an implementation preserves the model’s hypotheses. The proof results and the corpus results are two separate bodies of evidence about one design.

9. Privacy Considerations

Commitments, not content. Statements carry record commitments and digests, never record content. A verifier without content can still check signatures, anchoring, graph structure and propagation completeness, because all of those operate on commitments.

Keyed mode for personal data. keyed is REQUIRED for personal or otherwise sensitive data (§2.6). Keying with a dataset-scoped HMAC key defeats dictionary reconstruction of content from commitments and confines the ability to map commitments to content to holders of the dataset key. Dataset keys are never packaged in receipts, so a verifier not authorized to hold one cannot establish the binding and its result for that binding is unverifiable. The receipt does not say so and cannot: content_binding is producer-set and static, one receipt serves authorized and unauthorized holders alike, and authorization is a property of the verifier.

Erasure composed with an append-only log. Erasure is performed on record bytes, not on the log: erasing content while retaining statements preserves the evidence graph without the data, and destroying a dataset key prevents future mapping of that dataset’s commitments to content. Two consequences MUST be stated to deployers. First, anchored equality relations among commitments remain visible after key destruction: erasure limits content recovery, it does not unlink history. Second, where reproducible reconstruction was claimed, erasure terminates that property for the affected records, and reconstruction results report it as terminated (§4).

Content-bearing receipts. Statements never carry content, but receipts MAY: a claim with content_binding other than none carries the record’s bytes AS RECEIVED inside the receipt. Neither commitment mode protects those bytes. A content-bearing receipt discloses the record to every party that holds it, and because receipts are portable and verify offline they travel further and outlive the systems that issued them. Erasure at the source does not reach a copy packaged into a distributed receipt, so producers SHOULD track issuance of content-bearing receipts for datasets subject to erasure duties and SHOULD bound their retention. For personal or otherwise sensitive datasets, producers SHOULD issue receipts with content_binding: "none", and where content binding is genuinely required a receipt SHOULD be issued to a named authorized verifier rather than published, with keyed-authorized binding preferred.

Residual linkability and metadata. Within an authorized set, identical records within one dataset produce identical commitments, so repetition and co-occurrence remain observable to key holders; domain separation by dataset id prevents that linkage across datasets by construction. Statement volume, timing, pipeline identifiers and dataset structure remain observable to anyone who can enumerate the corpus. Locators and projection descriptors MUST NOT embed personal data. A formal analysis of commitment linkability, and guidance for erasure workflows, remain open work.

10. IANA Considerations

§10.1 registers the media type application/ahl-receipt+json. §10.2 establishes the AHL Receipt Claim Types registry, whose initial entries are the nine claim types of §7.2. §10.3 establishes the AHL Canonicalization Identifiers registry, whose initial entries are jcs and exact-bytes; every registration states whether its descriptor requires media_type, and a verifier’s result never depends on registry state (§6.3).

Appendix A. Future Work: Federation (Out of Scope)

Federation — provenance whose statements cross corpus boundaries — is deliberately out of scope for this document, which specifies the closed-corpus core. A federation extension is anticipated and is expected to address at least the following, none of which is specified here:

  • Cross-corpus record identity: translation of commitments across keyspaces without disclosing content.
  • Recipient-bearing disclosure statements: the material an obligation to notify prior recipients of a correction requires, and which the core deliberately omits because it carries no recipient identity.
  • A foreign-trigger observation horizon: a normative maximum staleness for a consumer’s view of another party’s log. In the closed-corpus core the semantic revocation horizon is zero entries (§2.4.2); across a boundary it must be a parameter, analogous in role to the maximum merge delay of [RFC9162].
  • Cross-manifest propagation obligations, including how a completeness claim composes across corpora with differently declared scopes.

The constraint inherited from the core applies to all of it: every cross-boundary claim names whose corpus it is relative to.

Appendix C. Relationship to Existing Work (Informative)

  • in-toto and SLSA define digest-bound, signed statements about software builds, with an envelope format AHL is compatible with. AHL applies the same discipline at record granularity and adds bitemporal reconstruction and revocation semantics, which build provenance does not address.
  • Certificate Transparency [RFC6962] [RFC9162] is the target log class and the origin of the witness idea.
  • C2PA binds provenance assertions to media assets; AHL is concerned with records in data pipelines and with what must happen when an input is later withdrawn.
  • SCITT [RFC9943] [RFC9942] defines single-issuer signed-statement transparency with COSE-encoded Signed Statements and Receipts. AHL record-level statements are Statements in the SCITT sense with defined payload semantics — how the manifest and key statements of corpus governance map to a SCITT Artifact and subject is left to a future carriage profile — and a Transparency Service is a candidate AHL log. The correspondence and its limits are set out in the I-D’s Appendix E.
  • W3C PROV provides a vocabulary in which AHL statements are expressible; AHL is an enforceable, digest-bound profile with integrity and propagation semantics that the data model alone does not supply. A construct-by-construct mapping is given in the I-D’s Appendix F.
  • Operational lineage systems record dataset-level lineage as mutable metadata and are complementary.
  • Bitemporal database literature supplies the distinction between valid time and transaction time that §4 depends on; AHL’s contribution is to make the transaction-time coordinate an externally attested entry index rather than a value the recording system can set.
Last updated on