WEXP Coverage: Claims, Evidence, and Evaluation

1.1. Scope and Non-Goals

The proposed contract specifies claim meanings, scoped premises, sufficient inference rules, counterexamples, result dependencies, and reliance requirements. It does not supply a universal source of ground truth, guarantee truthful administrators, prescribe instrumentation, or prove that a system is safe or correct. Coverage does not establish authorization, goal satisfaction, business acceptance, durable external effect, or future retention.¶

The baseline uses finite populations and exact predicates, not loss percentages. Multiple distinct receipts for one action can satisfy creation-complete and creation-sound while refuting creation-exact. A positive one-to-one claim does not tolerate missing, extra, ambiguous, or duplicate occurrences. Sampling, allowed loss rates, replacement receipts, and probabilistic coverage require separately identified contracts. No universal wire format, signature suite, trust policy, or registry is defined in this revision.¶

1.2. Architecture and Data Flow

The architecture distinguishes four logical responsibilities. These responsibilities can be combined in one implementation; they do not require separate services, processes, operators, or administrative domains.¶

Carrier verification

Parse the selected record encoding, enforce its extension rules, and authenticate the protected bytes under supplied verification inputs. A reusable carrier verifier can leave the authenticated payload opaque. Successful verification does not by itself establish the authority of the signer, population membership, complete capture, or the truth of a signed assertion.¶

Deployment evidence interpretation

Apply the declared deployment binding to interpret payloads, establish scoped identities and membership, check action and source relations, and supply normalized findings with evidence references. Collection, capture, closure, policy applicability, and any remaining assumptions are addressed here rather than inferred from a signature or a sender-provided boolean.¶

Coverage evaluation

Check premise dependencies, apply the rules in Section 7, retain inherited assumptions and counterexamples, aggregate conflicting derivations, and emit a CoverageResult.¶

Consumer reliance

Match the result to the consumer's required claims, exact context, accepted authorities and assumptions before relying on it. The consumer's authority decision is separate from the producer's proposed keys or policy.¶

The generic contract does not select a carrier, signature suite, or deployment technology. A deployment profile specifies its supported mechanisms and the information needed for authority decisions; it does not select trusted parties or approve assumptions on behalf of a consumer. No signature or profile identifier substitutes for that approval. The PostgreSQL profile in Appendix A is one concrete specialization, not a prerequisite for other bindings.¶

The same evidence can separately be mapped into a WEXP Core appraisal for an exact action. Neither result is substituted for the other. In particular, an ordinary execution appraisal does not silently acquire population completeness, and a positive coverage result does not automatically establish the execution claim of every individual receipt.¶

6.1. Premise Records

A premise record MUST contain an identifier, a precise predicate and version, its bound context, state, basis references, dependencies, and limitations. The states are:¶

• checked: the named check succeeded in its declared scope; its remaining assumptions and evidence references remain visible.¶

• assumed: an exact predicate is explicitly accepted by the identified policy, with the authority, reason, and scope of acceptance recorded. This is not a successful empirical check.¶

• unknown: neither an accepted basis nor a counterexample is available.¶

• refuted: a counterexample to that premise is established under its stated basis. Refuting a premise is not automatically refuting the target claim.¶

A usable derivation has only checked or policy-authorized assumed dependencies, and those dependencies are jointly consistent. The dependency graph MUST be acyclic and terminate in explicit evidence checks or assumptions. An assumption MUST NOT merely restate the claim being derived or an equivalent population guarantee. Source capture assumptions can be used only as separately specified deployment properties, not inferred from agreement with receipts. All transitive assumptions MUST be disclosed in the result.¶

Same administrative control does not make a record false, nor does a different key establish independence. A policy can accept a stated controller property as an assumption or require protected evidence of it. Failure to meet the declared requirement leaves the dependent claim unestablished. An evaluator MUST NOT silently weaken the policy to obtain a positive result.¶

6.2. View Closure Is Not Action Capture

The following predicates MUST be distinguished even if a deployment combines them in one mechanism:¶

1. Integrity and authenticity of the supplied view and its individual objects.¶

2. Bounded enumeration: all elements of that view were retrieved; pagination, filters, failures, and retained invalid elements are accounted for.¶

3. Temporal closure: writers and in-flight events are accounted for at the chosen cutoff.¶

4. Branch coverage: the accepted history is not merely one of several relevant forks or suppressed branches.¶

5. Population-view exactness: Cv exactly enumerates C, or Rv exactly enumerates R, under those obligations.¶

6. Action capture, source truthfulness, and source occurrence uniqueness relative to A.¶

A binding that supports a population-view exactness premise MUST state how it addresses each applicable closure and collection obligation and which part is assumed. A seal authenticating a count and digest checks only that commitment unless the binding establishes more. Two matching seals, two organizations, or an append-only prefix do not by themselves establish complete action capture or fork exclusion.¶

Observed empty and unavailable are different states. An unavailable view MUST NOT be substituted with an empty array. A failed or incomplete query MUST NOT be used as exhaustive evidence of absence.¶

7.1. Support Rules

P1: Supplied correspondence

Usable Rv and S, resolved membership and identities, and a checked exact bijection under the comparison predicate support supplied-correspondence. No assumption of completeness relative to A, C, or R is implied.¶

P2a: Delivery completeness

Usable Cv=C, established membership of every used Rv element in R at the named recipient and cutoff, and a checked containment of every Cv member in Rv support delivery-complete. Rv need not enumerate all of R. A proof that Rv receipts are authentic without evidence of recipient availability is insufficient.¶

P2b: Delivery exactness

Usable Cv=C and Rv=R, plus a checked exact receipt identity and content equality Cv=Rv, support delivery-exact. Both views can be empty. Neither P2 rule alone supports a creation-family claim.¶

P3: Source predicates

A binding can support source-complete, source-sound, or source-exact through a scoped capture mechanism and evidence checks. It MUST identify routes, writers, lifecycle stages, bypass paths, failure modes, and controller assumptions. Source-exact requires completeness, soundness, single-valued binding, and uniqueness of representation. Agreement between S and receipts is not a sufficient basis for these properties. A source-exact support derivation also supplies support derivations for source-complete and source-sound, inheriting its entire basis. These implications transport derivations, not final outcomes; their conflicts are resolved before downstream reliance.¶

P4a: Creation completeness

Usable Cv=C and source-exact, together with a checked relation G from Cv to S covering every member of S and checked relation composition, support creation-complete.¶

P4b: Creation soundness

Under the same population and composition premises, G relating every member of Cv to at least one S member supports creation-sound.¶

P4c: Creation exactness

Under the same population and composition premises, a checked exact G bijection supports creation-exact. For all three P4 rules, relation composition means that G followed by F yields exactly B on the declared populations, including payload validity and every relevant binding. An identifier-string lookup alone is insufficient. These sufficient rules are deliberately conservative; they do not assert that a complete source or created view is logically necessary for every possible positive derivation.¶

P5: Creation through exact delivery

Rv can replace Cv in the P4 rules only when the aggregated delivery-exact result is supported and Rv=R is usable. Delivery-complete is insufficient because R can contain additional receipts. The receipt-to-source relation and its composition must still be checked. Every dependency of the exact-delivery derivation is inherited.¶

P6: Empty actions

An actually available, fully read S with no members, together with usable source-complete for that exact S and scope, supports empty-actions. Source soundness is unnecessary for an empty S. Empty receipts or a commitment to an empty source view alone are insufficient.¶

P7: Family support implications

A usable creation-exact support derivation supplies creation-complete and creation-sound support derivations. A usable delivery-exact support derivation supplies a delivery-complete support derivation. These inherit the entire basis. The converse implications do not hold. Like the P3 source implications, these transport derivations before family outcomes are aggregated, not previously aggregated outcome values.¶

P8: Vacuous predicates

An available, completely read empty Cv with usable Cv=C supports delivery-complete and creation-sound without enumerating R or A. A supported aggregated empty-actions result supports creation-complete without enumerating C. Both bases together support creation-exact. These rules inherit all context and premise dependencies. Empty supplied arrays without their required population premises do not activate them.¶

7.2. Refutation Rules and Minimal Counterexamples

N1: Local correspondence counterexample

A demonstrated extra, missing, duplicate, or payload-mismatched element under the exact supplied-view predicate refutes supplied-correspondence. Any absence-based comparison requires complete reading of the relevant supplied view, not a claim that it exhausts A or C.¶

N2a: Missing delivery

A positively established member c of C and usable Rv=R, with an exhaustive check showing no equivalent member in Rv, refute delivery-complete and delivery-exact. A different-content member under the same identifier is not a substitute; an unresolved element that could be equivalent blocks the negative inference. Full enumeration of C is unnecessary.¶

N2b: Extra recipient member

A positively established member of R absent from a usable Cv=C refutes delivery-exact only. The exhaustive comparison must resolve identity and content equivalence. It does not refute delivery-complete.¶

N3: Missing creation

Positive evidence establishing a member a of A, usable Cv=C, and an exhaustive, unambiguous binding check showing no B-related receipt in Cv refute creation-complete and creation-exact. The evaluator need not enumerate all of A. If an uninterpretable element could bind to a, absence is not established.¶

N4a: Duplicate or ambiguous creation binding

Two distinct positively established members of C bound to the same positively established action refute creation-exact without complete enumeration of C. One positively established member of C with two established bindings to distinct members of A also refutes creation-exact. Neither counterexample by itself refutes creation-complete or creation-sound.¶

N4b: Orphan receipt

A positively established member c of C with a justified exhaustive negative basis showing no B-related action in A refutes creation-sound and creation-exact. One sufficient basis is usable source-exact and an exhaustive receipt-to-source relation whose composition represents all B bindings of c. Failure to find an action in an incomplete S is insufficient.¶

N5: Source counterexamples

A positively established action with no F-related entry in the completely read supplied S refutes source-complete. If an uninterpretable or ambiguously bound source element could represent the action, nonrepresentation is not established. Two distinct entries positively bound to the same action, or one entry positively bound to two distinct members of A, refute source-exact, but do not refute source-complete or source-sound. An entry known to have no real in-scope action binding refutes source-sound; mere failure to establish its action is not such knowledge. Every usable refutation derivation for source-complete or source-sound also refutes source-exact with the entire inherited basis.¶

N6: Nonempty action scope

One positively established in-scope action refutes empty-actions. No complete receipt or source population is required.¶

N7: Family refutation implications

Each usable refutation derivation for creation-complete or creation-sound also refutes creation-exact. Each usable refutation derivation for delivery-complete also refutes delivery-exact. All dependencies are retained. A refutation of an exact predicate does not, in general, refute its weaker predicates.¶

Each counterexample MUST preserve the scope, positive membership evidence, relevant exhaustive search predicate, and its assumptions. Malformed input, an unavailable source, or a failed authentication check alone does not establish that a real action occurred without a receipt.¶

7.3. Deterministic Reporting Procedure

1. Validate contract identity, requested claim identities, context bindings, references, and dependency structure. A malformed top-level request produces an input error, not a fabricated coverage result. An unsupported contract or deployment-profile revision is reported as unsupported input; it is not silently interpreted as a supported revision.¶

2. Record availability and validity per view. Preserve interpretable local findings when another view is unusable. An unavailable view is a valid reported condition, not necessarily a malformed request.¶

3. Resolve premise states and transitive assumptions under the fixed policy. Detect cycles, contradictory premises, unresolved identity, and unresolved scope. Do not derive a conclusion from an internally inconsistent premise set.¶

4. Evaluate primitive derivations and apply the P3, P7, N5, and N7 family implications before relying on any affected family outcome. These implications propagate exact support towards weaker predicates and weaker refutation towards exact predicates; they do not construct cyclic outcome dependencies. Apply each applicable support and refutation rule to each evaluated requested claim and required internal claim, retaining rule identifiers, exact witnesses, and dependency identifiers. Internal claims not requested for display are marked as dependencies, not as additional user requests.¶

5. If at least one usable support and no usable refutation exists, report supported. If at least one usable refutation and no usable support exists, report refuted. If both exist, report not-established with a conflict diagnostic and retain both derivations. If neither exists, report not-established with the missing or unusable dependencies.¶

6. Emit the bound result and its provenance. Sort unordered diagnostic collections by stable identifiers under the binding; never rely on wall-clock time, a hidden oracle, or nondeterministic iteration to select a verdict.¶

A failure to parse or authenticate an evidence package, an unsupported required feature, or exhaustion of processing resources MUST NOT by itself be reported as a refuted population claim. When producing a CoverageResult from a valid bound request, the evaluator MUST preserve interpretable local findings and distinguish evaluated not-established claims from requested claims not evaluated. An interface can apply its declared package-level rejection rules without producing a CoverageResult; it MUST identify that processing failure separately from claim outcomes. Package rejection is not permission to suppress an established counterexample in an emitted result. A failed or incomplete collection MUST NOT become an empty view.¶

Package failure is distinct from invalid content in an established population member. An authenticated collection can establish that particular retained bytes belong to C or R even when those bytes do not constitute a valid action binding. Such a candidate remains visible and can contribute to a refutation only with the membership and negative-binding basis required by Section 7.2. Conversely, inability to perform a cryptographic or interpretation check leaves that binding unresolved; it does not establish that no binding exists. Independently usable byte-delivery or local-comparison evidence is not discarded merely because an action-binding check remains unresolved.¶

A derived claim MAY satisfy a downstream dependency only after aggregation of its applicable support and refutation derivations yields supported. A refuted or not-established claim, including one with a conflict diagnostic, MUST NOT be relabeled as a checked premise by selecting one positive derivation. An independently sufficient alternative basis MAY be used with its own dependencies. Required dependent claims are evaluated in dependency order after their family implications have been resolved. This applies to source-exact in P4, delivery-exact in P5, source-complete in P6, and empty-actions in P8.¶

Outcome names in this procedure mean support or refutation conditional on the reported basis. Even a checked premise has an evidence scope and can have explicit assumptions. An interface MUST NOT render supported as an unconditional guarantee. A false assumed premise can yield a valid conditional derivation whose consequent is false in the actual world.¶

11.1. Core Target Correspondence Example (Informative)

This example illustrates the information a future PG/Core joint-use profile would need. It is not a complete Core mapping profile, a new conformance profile, or a claim of implemented interoperability. The pg-ledger/0.2.0 profile remains usable without Core.¶

The Coverage action is the durable commit of the admitted ledger row, identified by (database incarnation, epoch UUID, action UUID), with the exact payload bytes as its content, as defined in Appendix A.1. A compatible Core mapping profile could designate that same commit occurrence as its exact target. Its immutable equality rules would bind the three identity components and distinguish that occurrence from receipt creation, delivery, or an external business effect. Equal action UUIDs in different incarnations or epochs would not match.¶

For a task requiring one Core appraisal for each action in the closed epoch, the joint profile would have to establish the enumerated action population and exactly one applicable target mapping per required action. Missing or multiple candidate mappings would remain explicit failures of that correspondence, not evidence that the action did not occur. A valid target correspondence would not by itself provide Core boundary, content base, PROV, or IV findings. Those findings would still require the applicable Core mapping profile and its evidence.¶

The associated Coverage context would retain the exact incarnation, epoch, recipient, pinned policies and three committed logical seal coordinates. A Core evaluation time would not substitute for those seals. The task would specify which exact Core claim and Coverage claims it needs, whether it accepts the five PG deployment assumptions, and any additional shared-source limitations. For example, separately supported appraisals for 99 actions can coexist with refuted creation completeness for an established closed population of 100 actions when the required membership and exhaustive negative-binding evidence establishes a missing receipt. Merely counting 99 appraisals would not establish that omission. A positive joint decision requiring complete receipt creation would then be unavailable; the 99 appraisals would not be rewritten.¶

11.2. Examples of Other Deployment Bindings (Informative)

The following examples identify possible future profile work. They do not define additional evidence paths, extend pg-ledger/0.2.0, or supply a basis for any supported claim. The limited extension scope follows the design considerations in [RFC6709]; this revision defines no exhaustive catalogue or automatic profile-negotiation mechanism:¶

Streaming windows

A streaming profile would need finite declared windows, separate action/creation/delivery boundaries, and rules for late arrivals, closure and replay. A watermark alone would not establish complete capture.¶

Partitioned populations

A partitioned profile would need an established partition set, occurrence identity across partitions, and evidence for each required closure and cross-partition relation. Matching per-partition counts would not establish global exactness.¶

External effects

A profile for payments, external business mutations or physical effects would need an explicit occurrence relation and evidence for coupling the effect to its source and receipt, including ambiguous failures. A ledger append alone would not establish the external effect.¶

13.1. Joint-Use Contract

A system claiming conformance to a joint-use profile MUST identify the immutable profile revision and the exact Core semantics, Core mapping and result contracts, Coverage deployment profile, rule set, and result encoding that it supports. Conformance to Core and Coverage separately does not establish conformance to their joint use. This section defines requirements on such a profile; it does not register or fully specify a concrete joint-use profile.¶

The joint-use profile MUST define:¶

1. the meaning of the action on each side, the correspondence between exact Core targets and Coverage population elements, the evidence for that correspondence, its permitted cardinalities, and the treatment of missing, ambiguous, conflicting, or unsupported mappings;¶

2. the supported tasks, their required exact Core claims and Coverage claims, whether the task ranges over selected actions or the full population, and the basis for any required exhaustive enumeration;¶

3. the required compatibility of scopes, epochs, recipients, logical cutoffs, evaluation contexts, trust configurations, and policies, including any additional transformation or correspondence premises; equal identifiers alone do not establish compatible meanings;¶

4. the acceptance and validation of each supplied result, the binding to its exact request and evidence, and preservation of assumptions, counter-evidence, conflicts, evaluation gaps, limitations, and failures; and¶

5. the separate application-policy decision procedure, unsupported version and missing-input behavior, and positive and negative cases that distinguish the declared joint-use obligations.¶

A deployment profile determines its action domain but need not support Core. A selected joint-use profile MUST be consistent with that deployment profile; a reference to a Core appraisal is not itself a correspondence proof. An action UUID shared by a committed ledger append and an external payment does not identify the same action unless the required semantic binding is separately established.¶

13.2. Separate Results and Application Decision

A joint report MUST keep three parts distinguishable: the original Core appraisals, the original CoverageResult or its production failure, and the application-policy decision with the dependencies used to make it. The report MUST bind the parts to the selected task and joint-use profile. It MUST NOT replace either contract's result with a single unqualified success label. The application decision is not an additional Core verdict or Coverage outcome.¶

Core rejection is not refutation of a Coverage claim. Likewise, Coverage not-established, input rejection, and not-evaluated are not interchangeable. A joint consumer MUST NOT convert an unavailable result, an unsupported version, or a failed computation into evidence that a world claim is false. If a component required by the selected task is absent, unsupported, unvalidated, or unusable, the consumer MUST NOT issue a positive decision for that task. A component not required by a Core-only or Coverage-only task need not be produced.¶

Request provenance and processing failures MUST remain outside any result whose contract does not permit those fields. In particular, a rejected appraisal that withholds its input-derived target or context does not establish them. A joint wrapper may retain the submitted request and association attempt as separately labelled diagnostics; it MUST NOT reconstruct a partial accepted appraisal or treat that association attempt as a validated mapping.¶

Every relied-on assumption and limitation MUST remain traceable through the application decision. Where Core evidence and Coverage collection share an issuer, administrator, observation source, or other failure dependency, the joint profile MUST expose the relevant dependency. Independence is claim-relative: a shared source neither automatically invalidates every IV claim nor permits independence established for one check to be credited to the other. Combining results does not create a second independent observation of the same source.¶

Names in a joint presentation MUST identify their contract. For example, a Core supported-base set and Coverage's receipt-action relation are not the same object merely because each document uses B. Consumer decisions, Core verdicts, and Coverage outcomes require separate names or explicit qualification.¶

13.3. Limits and Further Profiles

Neither separate nor joint use establishes that every required action was performed. A population of actual actions A is not the set of obligations M. Establishing fulfilment of M requires a separate obligation contract and evidence relating its requirements to actions. Coverage exactness under accepted deployment assumptions does not automatically establish Core execution, PROV, IV, or an external effect.¶

A future Core revision is a legitimate alternative if a demonstrated consumer requirement cannot be represented safely by separate results and explicit joint-use rules. Reconsidering document packaging need not first merge the semantic contracts. A proposal for semantic merger needs an explicit domain, compatibility analysis, and evidence of the insufficiency of composition.¶

A.1. Action Domain, Identity and Authority

An action is the durable commit of an admitted action-ledger row. Its identity is the tuple (database incarnation, epoch UUID, action UUID); its content is the exact payload byte string. Different action UUIDs identify different actions even when their payloads are equal. Failed or rolled-back admission is not an action. Loss of the client's commit response does not undo a committed action. The epoch begins with its committed open record.¶

A is every admitted action in the immutable sealed epoch slice whose transaction commits no later than the action-seal transaction, including admission in that same transaction and actions with lost replies. Admission and sealing are governed by the epoch lock and committed seal state, never numerical transaction-ID ordering. S is that full sealed slice. F(s,a) holds exactly when incarnation, epoch, action UUID and raw payload bytes agree. G(c,s) applies the B predicate in Appendix A.5 to s's action identity and payload; established source exactness supplies its composition with F to B. Action uniqueness does not imply receipt uniqueness.¶

The domain excludes external payments, network delivery, physical effects, mutations to other business tables, rejected requests and effects produced by other systems. Including one of those effects requires another binding establishing its relation to the ledger. Planned or expected work MUST NOT be substituted for the actual action population.¶

The deployment has a non-login owner and five non-login capability roles: action writer, finalizer, recipient receiver, sealer and reader. Authenticated login principals receive minimum memberships. Application principals MUST NOT own profile objects, unintentionally inherit owner or sealer capabilities, have superuser or role-administration powers, install arbitrary extensions, or obtain a direct write path bypassing admission. Sender and finalizer principals MUST NOT hold the receiver capability; that capability belongs to the named recipient service. The collector uses the reader role. Signer and publisher need reader access to sealed actions and committed final bytes; this access grants no writes and does not waive publication ordering.¶

The owner, database and host administrators, credential administration, configuration auditor, and PostgreSQL and storage correctness are trusted. Sender and receiver storage share an administrative domain. Role separation establishes operational separation, not independent administration or resistance to a malicious administrator. Receiver possession is limited to the named durable inbox, not downstream application execution.¶

A key or policy change, restore, failover, primary replacement, timeline fork, schema or privilege change, or action-scope change requires a new incarnation or epoch and explicit new verification. This version specifies no transition inference. An unexplained discontinuity leaves affected premises unestablished; assigning a new identifier does not repair earlier loss.¶

A.2. Pinned Epoch Policy

SHA-256 in this profile is the 256-bit hash function specified by [FIPS180-4]. All artifact and payload digests apply to the exact stated bytes.¶

Before opening an epoch, the verifier MUST pin the exact bytes and SHA-256 digest of an externally approved policy. The policy is the deterministic CBOR map below with exactly eight integer keys. UUID values are 16 bytes obtained by removing the hyphens from the canonical UUID representation and hexadecimal-decoding the resulting 32 hexadecimal digits, preserving their displayed byte order. JSON UUIDs use lowercase hexadecimal and hyphens as specified by the schemas; this version imposes no UUID-version, nonzero-UUID or unequal-incarnation-and-epoch requirement.¶

Recipient and issuer identifiers contain 1 to 256 Unicode scalar values. Text comparisons use exact UTF-8 bytes, without normalization, case folding or URI rewriting. The verifier MUST recompute the policy digest and match every policy-bearing epoch field to the pin: incarnation, epoch, recipient, issuer, key identifier, public key and policy digest. A key supplied in the snapshot does not itself establish authority.¶

A.3. Admission, Three Committed Barriers and Durability

Every admission and every seal MUST acquire the same exclusive epoch-row lock, hold it through transaction end, and examine the appropriate seal state after acquiring it. The applicable PostgreSQL row-lock and transaction behavior is specified in [PG18]. This serializes admission with closure; it is not a wall-clock ordering rule.¶

The three seals MUST commit in different transactions. A stage MUST NOT advance on the basis of its own uncommitted sealing transaction. There is no reopening operation. A rolled-back seal closes nothing. A blocked writer MUST recheck the seal state; a serialization failure requires retrying the entire transaction, never bypassing admission. A timeout is failure to obtain a seal, not evidence of an empty population. A writer wins admission when it obtains the lock before the seal and subsequently commits.¶

An action admission and action seal MAY occur in the same transaction; creation still waits for that transaction's commit. The cutoff is the committed logical seal. Sequence numbers and transaction identifiers are identifiers and diagnostic coordinates, not counts, clocks or completeness arguments. The three seal coordinates MUST be distinct positive unsigned xid8 values; the wire contract does not require numerical ordering.¶

The database MUST use durable logged tables, fsync=on, full_page_writes=on, functioning durable storage and synchronous_commit=on at the commit of every operation and seal. An installation-time setting alone is insufficient: a transaction driver can change a transaction-local setting before commit. An ambiguous commit response requires reconnecting and checking durable state. A returned admission or seal result before COMMIT does not establish durability.¶

A.4. Selected CBOR and COSE Carrier

The selected carrier is N2-COSE-Sign1-Ed25519/0.1.0. It uses the core deterministic encoding requirements of [RFC8949], Section 4.2.1. The restricted CBOR language consists of integers from -2^64 through 2^64-1, byte strings, valid UTF-8 text, arrays and maps; map keys are integers, byte strings or text. Booleans, null, floating point, complex map keys, indefinite lengths and tags are excluded except for the one outer carrier tag below. Map keys are ordered by bytewise lexicographic comparison of their encoded bytes, not length-first order. Duplicate keys, non-shortest encodings, out-of-order keys and trailing bytes MUST be rejected from the received encoding.¶

A record is shortest-form CBOR tag 18 followed by the four-element COSE_Sign1 array [protected, {}, payload, signature], following [RFC9052], Sections 4.2 and 4.4. The protected byte string is the deterministic encoding of exactly {1: -19, 4: kid}. Algorithm -19 is the fully specified Ed25519 identifier in [RFC9864]; polymorphic EdDSA -8 is not accepted. The unprotected map is empty, the payload is an embedded byte string, and the signature is 64 bytes. There are no additional headers, fields or tags, no detached payload and no algorithm negotiation.¶

The signed bytes are the deterministic encoding of ["Signature1", protected, h'', payload], with empty external AAD. The verifier MUST check the exact expected key identifier and use the externally pinned raw 32-byte public key with the Ed25519 verification rules of [RFC8032]. Signature length alone is not verification. It MUST NOT silently repair or reserialize received bytes. Successful carrier verification authenticates the exact embedded bytes under that key; authorization, payload meaning, identity, closure and Coverage claims require the separate checks below.¶

Each encoded or decoded CBOR object and the complete tagged record is at most 65,536 bytes. Each container has at most 10,000 direct entries. Root depth is zero; a child increments depth by one, with maximum depth 16. A decoder MUST enforce lengths, container sizes and depth before unbounded allocation. The record limit includes overhead: a one-byte key identifier allows at most 65,457 payload bytes. No truncation or normalization is permitted. These bounds also apply to the signed collection record.¶

These are the selected carrier's stable failure categories; diagnostic wording and error priority for multiply invalid input are not an interoperability interface. CRYPTO_UNAVAILABLE MUST remain unresolved verification, not an invalid-signature finding. Resource exhaustion invalidates the attempted computation; it does not authorize removing a candidate from a population. This carrier definition makes no assertion of byte compatibility with a WEXP Core carrier.¶

A.5. Final Receipt Payload and B

The final receipt payload is the deterministic CBOR encoding of exactly the following ten-key map. Its carrier uses the policy's issuer key and key identifier.¶

B(c,a) holds exactly when the full received carrier and payload encodings and Ed25519 signature are valid, all policy, scope and identity bindings match, the action UUID equals a's UUID, and the payload hash equals SHA-256 of a's exact payload. No timestamp, count or signer-provided completeness flag establishes B. Unknown keys, invalid signatures, wrong scope, wrong payload hashes and references to absent actions remain retained candidates with no valid B edge. Unavailable cryptography or policy verification leaves the check unresolved; it MUST NOT create a negative B edge.¶

A.6. Finalization, Retries and Recipient Possession

Signing occurs only after the signer can read the committed action seal and sealed action. Finalization is the durable admission of full final bytes to the finalization ledger, not signing, an outbox intention or a precommit return value. The publisher MUST wait for the committed creation seal and publish only committed finalization-ledger bytes. Precommit or unrecorded publication removes the basis for Cv=C. An authorized signer can leak bytes outside the database, so this is also an application and audit obligation.¶

The transport envelope is (epoch UUID, receipt UUID, final bytes). Both ledgers MUST retain every committed attempt, including identical retries, conflicting variants, orphan references and malformed bytes. Admission and collection MUST NOT suppress evidence through receipt-key uniqueness, action-reference uniqueness, receipt-to-action referential constraints or receipt-validity filters. Raw entry IDs identify attempts, not receipts.¶

Trusted admission and authenticated capture MUST establish each occurrence's context, outer receipt key and exact retained bytes. Only with that basis may exact duplicate (epoch UUID, receipt UUID, final bytes) tuples be normalized as retries. All original entry IDs MUST remain available in diagnostics or normalization provenance. Without that basis, affected normalization, identity and delivery checks remain unresolved. Arbitrary supplied byte equality is insufficient.¶

C and R are the resulting finalization and inbox candidate sets. Different receipt UUIDs remain distinct even when they refer to the same action. Different bytes under one UUID are retained as separate candidate variants and exposed as an identity conflict. An evaluator MUST NOT select a preferred variant to obtain exactness. Malformed candidates remain in C or R. Authenticated outer identity and the signed payload's agreement with it are separate checks.¶

Creation completeness requires a B-related candidate for each A element; creation soundness requires a B-related A element for each C candidate; creation exactness requires the bijection and no unresolved identity conflict. Two valid receipt UUIDs for one action can preserve completeness and soundness while refuting exactness.¶

The named recipient MUST commit the full envelope to its inbox before acknowledgment. Ordinary sender privileges MUST NOT permit inbox writes. R describes durable possession in that inbox, not downstream processing. A signature alone does not establish possession. Given authenticated candidate identity and the logical prerequisites, delivery completeness compares C subset R by exact tuple equality, and delivery exactness compares C=R with conflict handling. Delivery of malformed or wrongly signed final bytes can therefore be supported while B is false or unresolved. Excess receiver candidates alone do not refute delivery completeness.¶

This is a finite batch contract. Post-creation-seal finalizations and post-receiver-seal arrivals are rejected. Continuously open late arrivals, cross-epoch supersession, revocation and policy rotation are unspecified. Reissuing under a new UUID before closure adds a candidate rather than replacing the original. Pending signing work is not a receipt. With exact populations, a missing finalization at the cutoff is a creation counterexample even if recovery could succeed in a later epoch.¶

A.7. Complete Collection and Snapshot Encoding

The collector MUST begin a fresh read-only REPEATABLE READ transaction after closure, observe the committed receiver seal in its stable snapshot, and enumerate every row of the three epoch slices. The snapshot is one UTF-8 JSON object conforming to Appendix A.14.1. It includes all policy columns, the three seal coordinates, every action, and every raw finalization and receiver attempt. There is no validity, success, key, time, content or pagination filter. Row security MUST NOT silently hide rows; the specified collection uses row_security=off, for which an applicable row-security policy is an error.¶

Collection requires successful process completion and COMMIT. A partial file, timeout, resource failure, missing epoch or missing seal is an unavailable collection, never an empty or usable partial population. An empty array alone does not establish empty actions. Replacing the bounded one-object snapshot with pagination requires a separately specified and reviewed stable-snapshot collection protocol.¶

The snapshot's server_version identifies PostgreSQL 18. snapshot_coordinate is the colon-delimited PostgreSQL snapshot coordinate string defined by the schema; it is not a population count. Action payloads and retained final bytes use lowercase, even-length hexadecimal. Action UUIDs MUST be unique within the snapshot. Raw entry IDs MUST be canonical positive decimal strings less than 2^63 and unique within their respective attempt ledger. Seal coordinates MUST be canonical positive decimal strings less than 2^64. Receipt keys intentionally need not be unique.¶

The package includes exact output bytes and their digest, the approved policy, endpoint identity, schema and grants audit, server configuration, seal-operation outcomes, and driver, publication and inbox evidence. Their provenance MUST be authenticated through the trusted collection procedure or a separately specified mechanism. An export is not self-authenticating and is not a cryptographic proof of complete database history.¶

No input flag such as source_exact=true can establish a premise. The adapter MUST report reasoned evidence references and unresolved checks. Conflicting admissible evidence branches MUST remain visible.¶

A.8. Explicit Deployment Assumptions

The separately approved assumption policy conforms to Appendix A.14.3 and binds the same incarnation and epoch as the signing policy. Accepted predicates have version pg-ledger/0.2.0, unique entry IDs and unique predicate names. Each acceptance MUST identify authority, reason, limitations and its relevant transaction interval within that scope. Only these five predicates are permitted; a target claim or complete-population assertion is not an acceptable substitute.¶

Every accepted predicate covers the same database incarnation and epoch from the commit opening that epoch through the successful COMMIT of the collection transaction producing the snapshot bound by this evaluation. The policy and manifest digests bind this acceptance to the evaluated package. The reason and limitations fields explain the acceptance but MUST NOT narrow that interval or replace the predicate. If the authority accepts only a shorter interval, that predicate is omitted and dependent premises remain unestablished. The policy-level version identifies the approving policy revision; it is distinct from predicate_version.¶

The schema permits omission of assumptions. Its array bound is 128, while the permitted predicate set and semantic uniqueness allow at most five accepted entries. An omitted predicate MUST NOT be silently added. The bounded full-collection path requires all five; that conservative choice is not a new assumption requirement for every other possible proof path.¶

A.9. PG-SealedSnapshot/0.2.0 Authentication Interchange

This named collection contract uses the carrier in Appendix A.4 with a separate approved collector key. The embedded payload is exact UTF-8 JSON, not CBOR and not canonicalized JSON. The signature authenticates the received payload bytes. The payload and all objects defined below have exactly their listed fields. Unknown fields, duplicate JSON member names, invalid Unicode and structural bounds violations are errors.¶

This profile selects the full-collection evidence path. After structural manifest validation, the evidence array MUST contain exactly one entry, of kind collection-provenance. Its artifact reference locates the exact N2-signed collection record defined here. A missing or multiple entry selection yields EVIDENCE_MISSING; a sole structurally recognized but different evidence kind yields NOT_IMPLEMENTED. In either case the adapter rejects the package and emits no CoverageResult. Unknown evidence kinds fail structural validation. No additional evidence family is silently ignored. Other collection paths require a separately identified profile.¶

The external trust configuration has exactly six fields. It is supplied through an approved channel separately from the untrusted package; a package-construction helper's proposed pins are not approval. All hex strings below are lowercase.¶

Approval of the six external pins and the collector authority MUST be valid for this evaluation under the consumer's declared trust policy. Freshness, expiry, revocation and historical-validity decisions are supplied by that policy; this profile specifies no online key discovery or revocation protocol. Missing, expired or revoked approval leaves authentication unestablished and yields AUTHENTICITY_UNRESOLVED, a rejected adapter report and no CoverageResult. A policy that expressly accepts historical validity records that scope; reassessment produces a new result rather than rewriting an earlier one.¶

Collector approval MUST cover the particular incarnation, epoch, endpoint, procedure and assertion scope. Possessing a mathematically valid key does not grant that authority. The policy and assumption-policy pins bind scope; deployment governance establishes the collector's authority over it. Procedure digests identify the exact approved procedure artifacts; this contract does not require a private source file, programming language or API. The collector MUST retain its actual query and driver transcript alongside the package. A digest does not prove faithful execution, and signing supplied assertions does not itself observe a database.¶

The next table lists every field of the observation objects and the exact values needed to establish the corresponding checks. Structure validation and observation evaluation are distinct. An authenticated object with all required fields but nonmatching observation values does not establish the check; it is not automatically malformed. In particular this version does not impose an additional structural type restriction on each observation value beyond the matching predicates shown here.¶

schema_grants has exactly five array-valued fields: tables, roles, direct_write_grants, public_function_execute, and public_schema_create. The first array has at most four rows, each with exactly name, owner, persistence, row_security. The second has at most six rows, each with exactly name, superuser, createdb, createrole, replication, bypassrls, login. These exact field sets and array bounds are structural requirements. This version assigns no entry schema to the three prohibited-grant arrays: support requires all three to be empty.¶

The supported table observation contains exactly one row for each name epoch, action_ledger, finalization_ledger, and receiver_inbox. Every owner is wexp_pg_owner, persistence is p (logged), and row security is boolean false. The supported role observation contains exactly wexp_pg_owner, wexp_pg_action, wexp_pg_finalizer, wexp_pg_receiver, wexp_pg_sealer, and wexp_pg_reader; all six capability flags for every role are boolean false. Row order is irrelevant. These names are exact audit identifiers in this interchange, not requirements to use a particular supplied installation program.¶

The full-collection path establishes its capture, exact-source, exact-creation-view and exact-receiver-view premises only when every required operational observation matches and all five deployment predicates are approved. Its composition premise additionally requires no unresolved finalization binding; its receiver-binding premise requires no unresolved inbox binding. Derived premises retain the capture basis and transitive accepted assumptions. These observations do not prove administrator honesty, credential exclusivity, absence of hidden publication or storage correctness. A missing assumption or unestablished observation leaves this path's population claims not-established.¶

The support declaration and additional limits of the reference implementation are described separately in Appendix B.1.¶

The aggregate receipt_binding check reports not-evaluated if not attempted, unresolved if any retained candidate has unresolved B interpretation, refuted if all candidate interpretations are resolved and at least one is invalid, and supported if every candidate has a valid B binding, including the vacuous empty case. An invalid candidate remains visible even when another candidate makes the aggregate unresolved. Identity conflicts are separately retained; this aggregate does not decide creation or delivery outcomes. This profile uses only the four active check states specified in Appendix A.11 and does not emit the reserved conflicted state. Logical derivation conflicts are handled separately by Coverage aggregation.¶

A.10. Timestamp Encoding

Both collected_at and actual-result evaluation_time MUST use the following restricted UTC form of [RFC3339], expressed in ABNF [RFC5234]. The grammar matches the entire decoded string without leading or trailing whitespace. DIGIT is imported from [RFC5234], Appendix B.1.¶

timestamp = 4DIGIT "-" 2DIGIT "-" 2DIGIT
            %x54 2DIGIT ":" 2DIGIT ":" 2DIGIT
            [ "." 1*6DIGIT ] %x5A

The four-digit year is 0001 through 9999. The month and day MUST form a valid Gregorian calendar date, including the leap-year rule. Hours are 00 through 23; minutes and seconds are 00 through 59. The optional fraction has one through six digits. Only uppercase T and Z are allowed. Leap-second notation, offsets other than Z, reduced-precision or week dates, comma fractions and extra suffixes are rejected as INPUT_INVALID. This deliberately narrower language is part of profile 0.2.0; it is not silently imposed on an artifact from another profile revision.¶

Examples are 2026-10-21T09:00:00Z and 2026-10-21T09:00:00.123456Z. Timestamp syntax establishes neither clock accuracy nor an authenticated observation time. Timestamps do not replace logical seal coordinates or prove commit order.¶

A.11. Input, Reports and Semantic Validation

The five schemas listed here are normative structural contracts using JSON Schema 2020-12 [JSONSCHEMA] [JSONSCHEMA-VALIDATION]. They do not replace the semantic requirements of this appendix. JSON follows [RFC8259], with valid UTF-8, unique member names, no unpaired surrogates and no nonfinite numbers. Insignificant whitespace and object member order do not change logical meaning; every artifact digest nevertheless binds exact supplied bytes. There is no canonical-JSON transformation before hashing.¶

The manifest supplies profile and version, a request naming coverage/0.2.0 and unique requested claim IDs, detached snapshot and policy references, a detached assumption-policy reference, and evidence references. Every artifact reference has exactly name, sha256 and octets. A name is a flat relative artifact name, never a path or network URL; all named artifacts have unique names distinct from the manifest name. Every length and SHA-256 digest MUST be verified. The adapter MUST NOT fetch URLs or execute artifact contents. Evidence IDs are unique and MUST NOT use the reserved IDs input-snapshot or pinned-policy. An evidence kind names material to inspect, not a trusted boolean.¶

The adapter report has exactly the nine checks in the mapping table above. Each check records not-evaluated, supported, refuted or unresolved, with evidence references and a reason. References resolve to manifest evidence IDs or the two reserved artifact IDs. Supported and refuted checks require inspected evidence. Not-evaluated means unattempted; unresolved means attempted without sufficient basis. adapter_status=evaluated means all checks were attempted, not that all passed. The report's input_sha256 hashes the exact manifest bytes and MUST be present for an evaluated report; null means those bytes were unavailable or no input was supplied. An adapter report does not override a logical prerequisite.¶

The structural schema retains conflicted as a reserved adapter check state. A producer of this profile version MUST NOT emit it, and a semantic validator MUST reject an adapter report containing it as an invalid profile report. Structural acceptance of that reserved value does not make the report semantically valid. This restriction does not change the logical Coverage aggregation of conflicting derivations.¶

The logical result has contract CoverageResult/0.2.0, rule set coverage/0.2.0 and the profile identifiers above. It supports all ten claim IDs: supplied-correspondence, source-complete, source-sound, source-exact, creation-complete, creation-sound, creation-exact, delivery-complete, delivery-exact and empty-actions. An evaluated claim has outcome supported, refuted or not-established; an unevaluated claim has a reason, no outcome and no derivations.¶

Actual results use artifact_kind=evaluation-result, identify the evaluator and version, and bind the real input manifest, pinned policies, evaluation timestamp and all three seal coordinates. The timestamp MUST be validated as a date and time, not merely accepted because of a schema format annotation. Null cutoffs are permitted only for constructed-example, which consumers MUST reject as evaluation evidence. A missing actual seal yields a collection error rather than an invented bound result. Declaring a coordinate does not authenticate it. Appendix A.10 specifies the required timestamp language.¶

The serialized context's fixed scope value is durable-commits-to-coverage_pg.action_ledger-in-epoch, its receipt_stream is coverage_pg.finalization_ledger, and its payload_projection is sha256-of-exact-action-payload-bytes. These exact wire identifiers designate the ledger semantics defined here and do not require a private SQL or programming-language interface.¶

The serialized context object and its enclosing profile, profile_version, evaluator and assumption_policy fields jointly encode the logical context required by Section 3. The mapping below makes explicit the fields and fixed profile semantics used by the result schema in Appendix A.14.5. These constants do not admit arbitrary tenant partitions, resource kinds or business-action meanings under the same scope identifier; changing those meanings requires another identified binding or profile revision.¶

A semantic validator MUST additionally check unique IDs; exact agreement of requested claims and records marked requested; matching context IDs, policy digests and cutoffs; permitted rule and polarity pairs; complete, acyclic dependency graphs; authorized assumptions, transitive basis inheritance and transitive assumption inheritance; resolvable evidence and JSON Pointer references; actual positive counterexample witnesses and required exhaustive-search bases; consistent view availability, integrity, closure, branch coverage and exactness; and the model's aggregation and conflict rules. Structural validity alone makes neither an imported result nor its premises trusted.¶

Both usable support and usable refutation produce not-established with a derivation-conflict diagnostic retaining both branches. Downstream claim dependencies require the aggregated claim to be supported; selecting a favorable derivation from a conflicted claim is forbidden. Family implications operate on derivations before aggregation without creating cyclic outcome dependencies.¶

References use evidence:<manifest-id>, input-snapshot#<JSON-Pointer>, premise:<id>, claim:<claim-id>, derivation:<id> or transformation:<id> as applicable. JSON Pointer follows [RFC6901]. Detached-artifact references are bound by their manifest digest. Premise and assumption references use premise IDs, claim dependencies use claim IDs, and diagnostic references use diagnostic IDs. Resolution alone does not confer trust. Assumptions, premises, diagnostics, transformations and derivations are ordered lexicographically by stable IDs. Claims preserve requested order followed by dependency claims in claim-ID order. Retained invalid-member references and normalization transformations MUST preserve access to the raw evidence.¶

A.12. Resource and Failure Contract

The schemas impose the remaining per-field, array and result bounds. Receipt and collection carrier limits also apply. Exceeding a bound MUST yield RESOURCE_LIMIT and no positive result. Truncating, skipping large records, sampling, discarding counterexamples or manufacturing empty views is forbidden. If collection fails before producing a complete object, it is COLLECTION_INCOMPLETE. A larger retained population requires a revised collection or profile contract.¶

Receipt diagnostic locations are JSON Pointers into the complete raw snapshot. If more than 1000 diagnostics would be needed, evaluation MUST fail with RESOURCE_LIMIT rather than emit an apparently complete truncated report. Failure does not remove original evidence. A rejected package MUST NOT yield a positive Coverage result.¶

In the bounded collection path, structural, digest, pin or collection authentication failure yields a rejected adapter report and no CoverageResult. A correctly authenticated observation that does not establish an operational prerequisite instead yields unresolved checks. A bad receipt signature remains an invalid candidate; unavailable receipt cryptography remains unresolved binding. The latter blocks unsupported absence inferences but need not block authenticated byte-for-byte delivery comparison. No evaluator may turn verifier unavailability into a fabricated negative witness.¶

A.13. Conformance Cases and Their Preconditions

The following cases specify observable expectations, not a claim that any deployment has passed them. Except where a row varies a prerequisite, assume authenticated complete sealed populations, the exact approved context and policies, all five accepted deployment predicates, no identity conflicts and available cryptography. Initially two distinct actions each have one correctly bound final receipt, and both receipts are in the recipient inbox. For the illustrative consumer decisions, the consumer requires creation-exact and delivery-exact. Every negative expectation requires its indicated positive membership witness and complete search basis; fixture labels or a hidden test oracle cannot establish those premises.¶

Claim and adapter expectations concern the profile. The accept, reject and hold labels illustrate the consumer in Appendix B.2; they are not additional Coverage outcomes or a requirement to implement that consumer interface.¶

Additional encoding cases exercise the original received bytes: duplicate JSON members; extra closed-object fields; alternate, duplicate or unordered CBOR keys; forbidden algorithm -8; wrong protected key ID; detached payload; extra COSE header or tag; trailing bytes; and all stated size and depth boundaries. A malformed retained finalization exercises an invalid B edge while remaining in its population; the same defect in the collection authentication record prevents that record from establishing capture. Exact action UUIDs, payload hashes, policy digests, recipient, issuer and outer-to-inner receipt identities MUST each be checked rather than inferred from a valid signature.¶

Admission cases include rollback, lost commit response followed by durable recollection, writers blocked behind each seal, whole-transaction retry on serialization failure, rejected post-seal admission and inability of an ordinary sender to admit inbox records. Constructed assertions can test parser and inference behavior but do not observe these database events. Deployment conformance requires the applicable checks against its actual authenticated endpoints, storage, principal bindings and publication and acknowledgment discipline. This appendix does not claim power-loss, storage-fault, failover, restore or independently operated interoperability evidence merely from successful process-crash or same-host tests.¶

A.14. Complete Profile JSON Schemas

The following five schemas are normative structural constraints for this profile. They use JSON Schema Draft 2020-12 [JSONSCHEMA] [JSONSCHEMA-VALIDATION]. Schema validity does not replace the semantic checks specified above. Schema identifiers are identifiers, not instructions to fetch resources. Local references resolve within each complete schema. Listings carrying the RFC 8792 single-backslash header [RFC8792] MUST be unfolded before JSON parsing; folding is document presentation only and never applies to signed or hashed deployment bytes.¶

NOTE: '\' line wrapping per RFC 8792

{
  "$schema": "https://json-schema.org/draft/2020-12/schema",
  "$id": "urn:wexp:coverage:pg-ledger:0.2.0:snapshot",
  "title": "PG Ledger 0.2.0 raw snapshot (structural validity only)"\
    ,
  "type": "object",
  "additionalProperties": false,
  "required": ["profile", "version", "server_version", "snapshot_coo\
    rdinate", "epoch", "actions", "finalization_attempts", "receiver\
    _attempts"],
  "properties": {
    "profile": {"const": "wexp-coverage-pg-ledger"},
    "version": {"const": "0.2.0"},
    "server_version": {"type": "string", "pattern": "^18(?:[. ]|$)"\
    , "maxLength": 256},
    "snapshot_coordinate": {"type": "string", "pattern": "^[0-9]+:[0\
    -9]+:([0-9]+(,[0-9]+)*)?$", "maxLength": 262144},
    "epoch": {
      "type": "object", "additionalProperties": false,
      "required": ["epoch_id", "database_incarnation", "recipient_id\
    ", "issuer_id", "issuer_key_id_hex", "issuer_public_key_hex", "p\
    olicy_digest_hex", "action_seal_xid", "creation_seal_xid", "rece\
    iver_seal_xid"],
      "properties": {
        "epoch_id": {"$ref": "#/$defs/uuid"},
        "database_incarnation": {"$ref": "#/$defs/uuid"},
        "recipient_id": {"type": "string", "minLength": 1, "maxLengt\
    h": 256},
        "issuer_id": {"type": "string", "minLength": 1, "maxLength"\
    : 256},
        "issuer_key_id_hex": {"type": "string", "pattern": "^([0-9a-\
    f]{2}){1,64}$"},
        "issuer_public_key_hex": {"$ref": "#/$defs/hex32"},
        "policy_digest_hex": {"$ref": "#/$defs/hex32"},
        "action_seal_xid": {"$ref": "#/$defs/decimal"},
        "creation_seal_xid": {"$ref": "#/$defs/decimal"},
        "receiver_seal_xid": {"$ref": "#/$defs/decimal"}
      }
    },
    "actions": {
      "type": "array", "maxItems": 10000,
      "items": {
        "type": "object", "additionalProperties": false,
        "required": ["action_id", "payload_hex"],
        "properties": {
          "action_id": {"$ref": "#/$defs/uuid"},
          "payload_hex": {"type": "string", "pattern": "^([0-9a-f]{2\
    })*$", "maxLength": 2097152}
        }
      }
    },
    "finalization_attempts": {"type": "array", "maxItems": 10000, "i\
    tems": {"$ref": "#/$defs/attempt"}},
    "receiver_attempts": {"type": "array", "maxItems": 10000, "items\
    ": {"$ref": "#/$defs/attempt"}}
  },
  "$defs": {
    "uuid": {"type": "string", "pattern": "^[0-9a-f]{8}-[0-9a-f]{4}-\
    [0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{12}$"},
    "decimal": {"type": "string", "pattern": "^[1-9][0-9]{0,19}$"},
    "hex32": {"type": "string", "pattern": "^[0-9a-f]{64}$"},
    "attempt": {
      "type": "object", "additionalProperties": false,
      "required": ["entry_id", "receipt_key", "final_bytes_hex"],
      "properties": {
        "entry_id": {"$ref": "#/$defs/decimal"},
        "receipt_key": {"$ref": "#/$defs/uuid"},
        "final_bytes_hex": {"type": "string", "pattern": "^([0-9a-f]\
    {2})*$", "maxLength": 131072}
      }
    }
  }
}

NOTE: '\' line wrapping per RFC 8792

{
  "$schema": "https://json-schema.org/draft/2020-12/schema",
  "$id": "urn:wexp:coverage:pg-ledger:0.2.0:adapter-input",
  "title": "Detached evidence package for the PG Ledger adapter",
  "type": "object", "additionalProperties": false,
  "required": ["profile", "version", "request", "snapshot", "pinned_\
    policy", "evidence"],
  "properties": {
    "profile": {"const": "wexp-coverage-pg-ledger"},
    "version": {"const": "0.2.0"},
    "request": {
      "type": "object", "additionalProperties": false,
      "required": ["request_id", "rule_set", "requested_claims", "as\
    sumption_policy"],
      "properties": {
        "request_id": {"type": "string", "pattern": "^[A-Za-z0-9._-]\
    {1,64}$"},
        "rule_set": {"const": "coverage/0.2.0"},
        "requested_claims": {"type": "array", "minItems": 1, "maxIte\
    ms": 10, "uniqueItems": true, "items": {"enum": ["supplied-corre\
    spondence", "source-complete", "source-sound", "source-exact", "\
    creation-complete", "creation-sound", "creation-exact", "deliver\
    y-complete", "delivery-exact", "empty-actions"]}},
        "assumption_policy": {"$ref": "#/$defs/artifact"}
      }
    },
    "snapshot": {"$ref": "#/$defs/artifact"},
    "pinned_policy": {"$ref": "#/$defs/artifact"},
    "evidence": {
      "type": "array", "maxItems": 128,
      "items": {
        "type": "object", "additionalProperties": false,
        "required": ["id", "kind", "artifact"],
        "properties": {
          "id": {"type": "string", "pattern": "^[A-Za-z0-9._-]{1,64}\
    $"},
          "kind": {"enum": ["policy-approval", "collection-provenanc\
    e", "schema-grants-audit", "durability-continuity", "seal-transc\
    ript", "publication-discipline", "recipient-possession"]},
          "artifact": {"$ref": "#/$defs/artifact"}
        }
      }
    }
  },
  "$defs": {
    "artifact": {
      "type": "object", "additionalProperties": false,
      "required": ["name", "sha256", "octets"],
      "properties": {
        "name": {"type": "string", "pattern": "^[A-Za-z0-9][A-Za-z0-\
    9._-]{0,127}$"},
        "sha256": {"type": "string", "pattern": "^[0-9a-f]{64}$"},
        "octets": {"type": "integer", "minimum": 0, "maximum": 26843\
    5456}
      }
    }
  }
}

NOTE: '\' line wrapping per RFC 8792

{
  "$schema": "https://json-schema.org/draft/2020-12/schema",
  "$id": "urn:wexp:coverage:pg-ledger:0.2.0:assumption-policy",
  "title": "Explicit assumption acceptance policy (approval authenti\
    cation is external)",
  "type": "object", "additionalProperties": false,
  "required": ["policy_id", "version", "authority", "database_incarn\
    ation", "epoch_id", "accepted_assumptions"],
  "properties": {
    "policy_id": {"type": "string", "minLength": 1, "maxLength": 128\
    },
    "version": {"type": "string", "minLength": 1, "maxLength": 64},
    "authority": {"type": "string", "minLength": 1, "maxLength": 256\
    },
    "database_incarnation": {"type": "string", "pattern": "^[0-9a-f]\
    {8}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{12}$"},
    "epoch_id": {"type": "string", "pattern": "^[0-9a-f]{8}-[0-9a-f]\
    {4}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{12}$"},
    "accepted_assumptions": {
      "type": "array", "maxItems": 128,
      "items": {
        "type": "object", "additionalProperties": false,
        "required": ["id", "predicate", "predicate_version", "reason\
    ", "limitations"],
        "properties": {
          "id": {"type": "string", "pattern": "^[A-Za-z0-9._-]{1,64}\
    $"},
          "predicate": {"enum": ["trusted-database-host-administrati\
    on", "correct-postgresql-storage", "exclusive-principal-capabili\
    ties", "publisher-obeys-finalization-order", "recipient-service-\
    obeys-inbox-contract"]},
          "predicate_version": {"const": "pg-ledger/0.2.0"},
          "reason": {"type": "string", "minLength": 1, "maxLength": \
    2048},
          "limitations": {"type": "array", "maxItems": 128, "items"\
    : {"type": "string", "maxLength": 2048}}
        }
      }
    }
  }
}

NOTE: '\' line wrapping per RFC 8792

{
  "$schema": "https://json-schema.org/draft/2020-12/schema",
  "$id": "urn:wexp:coverage:pg-ledger:0.2.0:adapter-result",
  "title": "Profile evidence-check report, not a CoverageResult",
  "type": "object", "additionalProperties": false,
  "required": ["profile", "version", "adapter_status", "input_sha25\
    6", "checks", "diagnostics"],
  "allOf": [{"if": {"properties": {"adapter_status": {"const": "eva\
    luated"}}}, "then": {"properties": {"input_sha256": {"type": "s\
    tring", "pattern": "^[0-9a-f]{64}$"}}}}],
  "properties": {
    "profile": {"const": "wexp-coverage-pg-ledger"},
    "version": {"const": "0.2.0"},
    "adapter_status": {"enum": ["not-evaluated", "rejected", "evalu\
    ated"]},
    "input_sha256": {"oneOf": [{"type": "null"}, {"type": "string"\
    , "pattern": "^[0-9a-f]{64}$"}]},
    "checks": {
      "type": "object", "additionalProperties": false,
      "required": ["structure", "policy", "capture_authenticity", "\
    schema_grants", "durability_continuity", "barriers", "finalizat\
    ion_publication", "receiver_possession", "receipt_binding"],
      "properties": {
        "structure": {"$ref": "#/$defs/check"},
        "policy": {"$ref": "#/$defs/check"},
        "capture_authenticity": {"$ref": "#/$defs/check"},
        "schema_grants": {"$ref": "#/$defs/check"},
        "durability_continuity": {"$ref": "#/$defs/check"},
        "barriers": {"$ref": "#/$defs/check"},
        "finalization_publication": {"$ref": "#/$defs/check"},
        "receiver_possession": {"$ref": "#/$defs/check"},
        "receipt_binding": {"$ref": "#/$defs/check"}
      }
    },
    "diagnostics": {"type": "array", "maxItems": 1000, "items": {"$\
    ref": "#/$defs/diagnostic"}}
  },
  "$defs": {
    "check": {
      "type": "object", "additionalProperties": false,
      "required": ["status", "evidence_refs", "reason"],
      "properties": {
        "status": {"description": "conflicted is reserved: profile \
    0.2.0 producers MUST NOT emit it; semantic validators MUST reje\
    ct reports containing it.", "enum": ["not-evaluated", "supporte\
    d", "refuted", "unresolved", "conflicted"]},
        "evidence_refs": {"type": "array", "maxItems": 128, "unique\
    Items": true, "items": {"type": "string", "pattern": "^[A-Za-z0\
    -9._-]{1,64}$"}},
        "reason": {"type": "string", "minLength": 1, "maxLength": 2\
    048}
      }
    },
    "diagnostic": {
      "type": "object", "additionalProperties": false,
      "required": ["code", "location", "detail"],
      "properties": {
        "code": {"enum": ["NOT_IMPLEMENTED", "INPUT_INVALID", "UNSU\
    PPORTED_VERSION", "UNKNOWN_FIELD", "RESOURCE_LIMIT", "HASH_MISM\
    ATCH", "EVIDENCE_MISSING", "AUTHENTICITY_UNRESOLVED", "POLICY_M\
    ISMATCH", "BARRIER_UNESTABLISHED", "COLLECTION_INCOMPLETE", "CO\
    NFIG_DISCONTINUITY", "RECEIPT_INVALID", "IDENTITY_CONFLICT", "B\
    INDING_UNRESOLVED"]},
        "location": {"type": "string", "maxLength": 256},
        "detail": {"type": "string", "minLength": 1, "maxLength": 2\
    048}
      }
    }
  }
}

NOTE: '\' line wrapping per RFC 8792

{
  "$schema": "https://json-schema.org/draft/2020-12/schema",
  "$id": "urn:wexp:coverage:pg-ledger:0.2.0:coverage-result",
  "title": "PG Ledger profile encoding of the Coverage 0.2.0 logica\
    l result",
  "type": "object", "additionalProperties": false,
  "required": ["artifact_kind", "contract", "rule_set", "profile", "\
    profile_version", "result_id", "evaluator", "evaluation_time", "\
    input_manifest", "context", "assumption_policy", "requested_clai\
    ms", "claims", "premises", "views", "diagnostics", "transformati\
    ons", "unperformed_checks", "limitations", "supersedes"],
  "properties": {
    "artifact_kind": {"enum": ["evaluation-result", "constructed-exa\
    mple"]},
    "contract": {"const": "CoverageResult/0.2.0"},
    "rule_set": {"const": "coverage/0.2.0"},
    "profile": {"const": "wexp-coverage-pg-ledger"},
    "profile_version": {"const": "0.2.0"},
    "result_id": {"$ref": "#/$defs/id"},
    "evaluator": {
      "type": "object", "additionalProperties": false, "required": [\
    "id", "version"],
      "properties": {"id": {"$ref": "#/$defs/id"}, "version": {"type\
    ": "string", "minLength": 1, "maxLength": 64}}
    },
    "evaluation_time": {"oneOf": [{"type": "string", "format": "date\
    -time", "minLength": 20, "maxLength": 27, "pattern": "^[0-9]{4}-\
    [0-9]{2}-[0-9]{2}T[0-9]{2}:[0-9]{2}:[0-9]{2}(\\.[0-9]{1,6})?Z$"}\
    , {"type": "null"}]},
    "input_manifest": {"oneOf": [{"$ref": "#/$defs/artifact"}, {"typ\
    e": "null"}]},
    "context": {
      "type": "object", "additionalProperties": false,
      "required": ["id", "epoch_id", "database_incarnation", "scope"\
    , "receipt_stream", "recipient_id", "payload_projection", "pinne\
    d_policy", "action_cutoff", "creation_cutoff", "receiver_cutoff"\
    ],
      "properties": {
        "id": {"$ref": "#/$defs/id"}, "epoch_id": {"$ref": "#/$defs/\
    uuid"}, "database_incarnation": {"$ref": "#/$defs/uuid"},
        "scope": {"const": "durable-commits-to-coverage_pg.action_le\
    dger-in-epoch"},
        "receipt_stream": {"const": "coverage_pg.finalization_ledger\
    "},
        "recipient_id": {"type": "string", "minLength": 1, "maxLengt\
    h": 256},
        "payload_projection": {"const": "sha256-of-exact-action-payl\
    oad-bytes"},
        "pinned_policy": {"oneOf": [{"$ref": "#/$defs/artifact"}, {"\
    type": "null"}]},
        "action_cutoff": {"$ref": "#/$defs/cutoff"},
        "creation_cutoff": {"$ref": "#/$defs/cutoff"},
        "receiver_cutoff": {"$ref": "#/$defs/cutoff"}
      }
    },
    "assumption_policy": {
      "oneOf": [{"type": "null"}, {
        "type": "object", "additionalProperties": false, "required"\
    : ["id", "version", "artifact"],
        "properties": {"id": {"type": "string", "minLength": 1, "max\
    Length": 128}, "version": {"type": "string", "minLength": 1, "ma\
    xLength": 64}, "artifact": {"$ref": "#/$defs/artifact"}}
      }]
    },
    "requested_claims": {"type": "array", "minItems": 1, "maxItems"\
    : 10, "uniqueItems": true, "items": {"$ref": "#/$defs/claim_id"}\
    },
    "claims": {"type": "array", "minItems": 1, "maxItems": 10, "item\
    s": {"$ref": "#/$defs/claim"}},
    "premises": {"type": "array", "maxItems": 1000, "items": {"$ref"\
    : "#/$defs/premise"}},
    "views": {
      "type": "object", "additionalProperties": false, "required": [\
    "S", "Cv", "Rv"],
      "properties": {"S": {"$ref": "#/$defs/view"}, "Cv": {"$ref": "\
    #/$defs/view"}, "Rv": {"$ref": "#/$defs/view"}}
    },
    "diagnostics": {"type": "array", "maxItems": 1000, "items": {"$r\
    ef": "#/$defs/diagnostic"}},
    "transformations": {"type": "array", "maxItems": 1000, "items": \
    {"type": "object", "additionalProperties": false, "required": ["\
    id", "operation", "input_refs", "output_refs", "basis_refs"], "p\
    roperties": {"id": {"$ref": "#/$defs/id"}, "operation": {"type"\
    : "string", "minLength": 1, "maxLength": 2048}, "input_refs": {"\
    $ref": "#/$defs/refs"}, "output_refs": {"$ref": "#/$defs/refs"}\
    , "basis_refs": {"$ref": "#/$defs/refs"}}}},
    "unperformed_checks": {"$ref": "#/$defs/texts"},
    "limitations": {"$ref": "#/$defs/texts"},
    "supersedes": {"type": "array", "maxItems": 128, "items": {"$ref\
    ": "#/$defs/artifact"}}
  },
  "allOf": [{"if": {"properties": {"artifact_kind": {"const": "evalu\
    ation-result"}}}, "then": {"properties": {"evaluation_time": {"t\
    ype": "string", "format": "date-time", "minLength": 20, "maxLeng\
    th": 27, "pattern": "^[0-9]{4}-[0-9]{2}-[0-9]{2}T[0-9]{2}:[0-9]{\
    2}:[0-9]{2}(\\.[0-9]{1,6})?Z$"}, "input_manifest": {"$ref": "#/$\
    defs/artifact"}, "assumption_policy": {"type": "object"}, "conte\
    xt": {"properties": {"pinned_policy": {"$ref": "#/$defs/artifact\
    "}, "action_cutoff": {"type": "string"}, "creation_cutoff": {"ty\
    pe": "string"}, "receiver_cutoff": {"type": "string"}}}}}}],
  "$defs": {
    "id": {"type": "string", "pattern": "^[A-Za-z0-9._-]{1,128}$"},
    "uuid": {"type": "string", "pattern": "^[0-9a-f]{8}-[0-9a-f]{4}-\
    [0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{12}$"},
    "refs": {"type": "array", "maxItems": 1000, "uniqueItems": true\
    , "items": {"type": "string", "minLength": 1, "maxLength": 512}}\
    ,
    "texts": {"type": "array", "maxItems": 1000, "items": {"type": "\
    string", "minLength": 1, "maxLength": 2048}},
    "artifact": {
      "type": "object", "additionalProperties": false, "required": [\
    "name", "sha256", "octets"],
      "properties": {"name": {"type": "string", "pattern": "^[A-Za-z\
    0-9][A-Za-z0-9._-]{0,127}$"}, "sha256": {"type": "string", "patt\
    ern": "^[0-9a-f]{64}$"}, "octets": {"type": "integer", "minimum"\
    : 0, "maximum": 268435456}}
    },
    "cutoff": {"oneOf": [{"type": "null"}, {"type": "string", "patte\
    rn": "^[1-9][0-9]{0,19}$"}]},
    "claim_id": {"enum": ["supplied-correspondence", "source-complet\
    e", "source-sound", "source-exact", "creation-complete", "creati\
    on-sound", "creation-exact", "delivery-complete", "delivery-exac\
    t", "empty-actions"]},
    "claim": {
      "type": "object", "additionalProperties": false,
      "required": ["id", "role", "evaluation_status", "derivations"\
    , "inherited_assumptions", "diagnostic_refs", "limitations"],
      "properties": {
        "id": {"$ref": "#/$defs/claim_id"}, "role": {"enum": ["reque\
    sted", "dependency"]},
        "evaluation_status": {"enum": ["evaluated", "not-evaluated"]\
    },
        "outcome": {"enum": ["supported", "refuted", "not-establishe\
    d"]},
        "reason": {"type": "string", "minLength": 1, "maxLength": 20\
    48},
        "derivations": {"type": "array", "maxItems": 1000, "items": \
    {"$ref": "#/$defs/derivation"}},
        "inherited_assumptions": {"$ref": "#/$defs/refs"}, "diagnost\
    ic_refs": {"$ref": "#/$defs/refs"}, "limitations": {"$ref": "#/$\
    defs/texts"}
      },
      "allOf": [{"if": {"properties": {"evaluation_status": {"const"\
    : "evaluated"}}}, "then": {"required": ["outcome"]}, "else": {"r\
    equired": ["reason"], "not": {"required": ["outcome"]}, "propert\
    ies": {"derivations": {"maxItems": 0}}}}]
    },
    "premise": {
      "type": "object", "additionalProperties": false,
      "required": ["id", "predicate", "predicate_version", "definiti\
    on", "context_id", "state", "basis_refs", "dependencies", "assum\
    ption_authority", "limitations"],
      "properties": {
        "id": {"$ref": "#/$defs/id"}, "predicate": {"$ref": "#/$defs\
    /id"}, "predicate_version": {"type": "string", "minLength": 1, "\
    maxLength": 64},
        "definition": {"type": "string", "minLength": 1, "maxLength"\
    : 2048}, "context_id": {"$ref": "#/$defs/id"},
        "state": {"enum": ["checked", "assumed", "unknown", "refuted\
    "]}, "basis_refs": {"$ref": "#/$defs/refs"}, "dependencies": {"$\
    ref": "#/$defs/refs"},
        "assumption_authority": {"oneOf": [{"type": "null"}, {"type"\
    : "object", "additionalProperties": false, "required": ["authori\
    ty", "policy_entry_id", "reason"], "properties": {"authority": {\
    "type": "string", "minLength": 1, "maxLength": 256}, "policy_ent\
    ry_id": {"$ref": "#/$defs/id"}, "reason": {"type": "string", "mi\
    nLength": 1, "maxLength": 2048}}}]},
        "limitations": {"$ref": "#/$defs/texts"}
      },
      "allOf": [{"if": {"properties": {"state": {"const": "assumed"}\
    }}, "then": {"properties": {"assumption_authority": {"type": "ob\
    ject"}}}, "else": {"properties": {"assumption_authority": {"type\
    ": "null"}}}}]
    },
    "derivation": {
      "type": "object", "additionalProperties": false,
      "required": ["id", "rule", "polarity", "basis_refs", "premise_\
    refs", "claim_dependencies", "witness_refs", "counterexample", "\
    inherited_assumptions"],
      "properties": {
        "id": {"$ref": "#/$defs/id"}, "rule": {"enum": ["P1", "P2a"\
    , "P2b", "P3", "P4a", "P4b", "P4c", "P5", "P6", "P7", "P8", "N1"\
    , "N2a", "N2b", "N3", "N4a", "N4b", "N5", "N6", "N7"]},
        "polarity": {"enum": ["support", "refutation"]}, "basis_refs\
    ": {"$ref": "#/$defs/refs"}, "premise_refs": {"$ref": "#/$defs/r\
    efs"},
        "claim_dependencies": {"type": "array", "maxItems": 10, "uni\
    queItems": true, "items": {"$ref": "#/$defs/claim_id"}},
        "witness_refs": {"$ref": "#/$defs/refs"}, "inherited_assumpt\
    ions": {"$ref": "#/$defs/refs"},
        "counterexample": {"oneOf": [{"type": "null"}, {"type": "obj\
    ect", "additionalProperties": false, "required": ["context_id", \
    "positive_membership_refs", "exhaustive_search", "assumption_ref\
    s"], "properties": {"context_id": {"$ref": "#/$defs/id"}, "posit\
    ive_membership_refs": {"$ref": "#/$defs/refs"}, "exhaustive_sear\
    ch": {"oneOf": [{"type": "null"}, {"type": "object", "additional\
    Properties": false, "required": ["predicate", "basis_refs"], "pr\
    operties": {"predicate": {"type": "string", "minLength": 1, "max\
    Length": 2048}, "basis_refs": {"$ref": "#/$defs/refs"}}}]}, "ass\
    umption_refs": {"$ref": "#/$defs/refs"}}}]}
      },
      "allOf": [{"if": {"properties": {"polarity": {"const": "refuta\
    tion"}}}, "then": {"properties": {"counterexample": {"type": "ob\
    ject"}}}, "else": {"properties": {"counterexample": {"type": "nu\
    ll"}}}}]
    },
    "view": {
      "type": "object", "additionalProperties": false, "required": [\
    "availability", "enumeration", "integrity", "temporal_closure", \
    "branch_coverage", "population_exactness", "premise_refs", "reta\
    ined_invalid_refs", "limitations"],
      "properties": {
        "availability": {"enum": ["available", "unavailable"]}, "enu\
    meration": {"enum": ["complete-view", "partial-view", "unavailab\
    le"]},
        "integrity": {"enum": ["checked", "unknown", "refuted"]}, "t\
    emporal_closure": {"enum": ["checked", "assumed", "unknown", "re\
    futed"]},
        "branch_coverage": {"enum": ["checked", "assumed", "unknown"\
    , "refuted"]}, "population_exactness": {"enum": ["checked", "ass\
    umed", "unknown", "refuted"]},
        "premise_refs": {"$ref": "#/$defs/refs"}, "retained_invalid_\
    refs": {"$ref": "#/$defs/refs"}, "limitations": {"$ref": "#/$def\
    s/texts"}
      }
    },
    "diagnostic": {
      "type": "object", "additionalProperties": false, "required": [\
    "id", "code", "claim_refs", "evidence_refs", "detail"],
      "properties": {
        "id": {"$ref": "#/$defs/id"}, "code": {"enum": ["missing", "\
    extra", "duplicate", "identity-conflict", "content-mismatch", "u\
    nresolved-identity", "invalid-member", "view-unavailable", "prem\
    ise-gap", "derivation-conflict", "not-implemented", "resource-li\
    mit"]},
        "claim_refs": {"type": "array", "maxItems": 10, "uniqueItems\
    ": true, "items": {"$ref": "#/$defs/claim_id"}}, "evidence_refs"\
    : {"$ref": "#/$defs/refs"}, "detail": {"type": "string", "minLen\
    gth": 1, "maxLength": 2048}
      }
    }
  }
}

B.1. Supported Evidence Path and Implementation Limits

The bounded reference path accepts exactly one manifest evidence item of kind collection-provenance; it rejects extra or absent branches with EVIDENCE_MISSING rather than ignoring possible conflicts. The earlier prototype also reports EVIDENCE_MISSING for a sole different recognized evidence kind; the current profile instead specifies NOT_IMPLEMENTED for that case in Appendix A.9. This historical behavior is not the normative selection contract. It does not implement alternate evidence families, the P5 receipt-view substitution path, the N5 source-counterexample path or a WEXP Core mapping. Its support paths are P1, P2a, P2b, P3, P4a, P4b, P4c, P6 and P8; its refutation paths are N1, N2a, N2b, N3, N4a, N4b and N6, with P7 and N7 family transport. It returns all ten claims, marking unrequested claims as dependencies. Validation of its generated dependency graph does not make it an importer of arbitrary CoverageResult objects. It reads only flat local regular nonsymlink files and additionally bounds its manifest to 1 MiB. These are declared limits of that path, not a reduction of the earlier profile's input schema's zero-to-128 evidence entries or seven permitted evidence kinds.¶

B.2. Recomputing Consumer Interface

The reference consumer recomputes evaluation from the evidence package and external pins; it does not accept a supplied result object as authority. Its caller supplies a nonempty list of unique required claim IDs and an expected context object with exactly these six fields: database_incarnation, epoch_id, recipient_id, action_cutoff, creation_cutoff, receiver_cutoff. Their values must equal the evaluated context exactly. This consumer interface is one bounded application of the profile, not a requirement that every Coverage consumer recompute results.¶

Invalid required claims or an expected context with a missing or extra field is an INPUT_INVALID interface error. For a valid request, the consumer returns hold for unavailable evaluation, unestablished authentication or any context-value mismatch before considering claim outcomes. With matching context, any refuted required claim produces reject; all required claims supported produces accept; otherwise it returns hold. Its result fields are decision, reason, required_claims, input_sha256, inherited_assumptions, meaning, and evaluation. They carry the decision and explanation, requested claim list, inspected manifest digest when available, sorted unique inherited assumption IDs, an explanation of the decision's Coverage-only meaning, and an object with adapter and coverage fields. The latter is null when no CoverageResult was obtained. Explanation text is not a stable interoperability identifier. Acceptance is conditional on that context and those assumptions; it is not a Core accept verdict or production certification.¶

B.3. Native Reconciliation Comparison

A plain set-and-binding reconciliation baseline may share input authentication, candidate normalization and receipt verification with the evaluator. Agreement then tests the rule and result layer, not independent capture or cryptographic verification, and does not establish superiority of one representation.¶

C.1. Signed Receipt Bytes

This example uses the Ed25519 seed and public key from [RFC8032], Section 7.1, TEST 1. The seed is disclosed test material and is unsuitable for an operational signing key. The key identifier is the one-byte string h'01'.¶

seed:
9d61b19deffd5a60ba844af492ec2cc44449c5697b326919703bac031cae7f60
public key:
d75a980182b10ab7d54bfed3c964073a0ee172f3daa62325af021a68f707511a

The epoch, database incarnation, receipt and action UUIDs are, respectively, the following canonical values:¶

00000000-0000-0000-0000-000000000001
00000000-0000-0000-0000-000000000010
00000000-0000-0000-0000-000000000020
00000000-0000-0000-0000-000000000030

The recipient is r, the issuer is i, and the action payload is the empty byte string. The exact 113-byte policy encoding from Appendix A.2 is:¶

a80177776578702d636f7665726167652d70672d6c65646765720265302e322e
3003500000000000000000000000000000001004500000000000000000000000
0000000001056172066169074101085820d75a980182b10ab7d54bfed3c96407
3a0ee172f3daa62325af021a68f707511a

Its SHA-256 digest is:¶

808a5ca10093b0a12b6aafb45606e58f53000c012450adc1e437dd80b8bb8a52

The receipt payload has the ten fields of Appendix A.5, with those identities, the SHA-256 of the empty action payload in key 7, and the policy digest above in key 9. The protected header bytes are h'a20132044101'. The payload is 181 bytes and the complete tagged COSE_Sign1 record is 259 bytes:¶

d28446a20132044101a058b5aa0177776578702d636f7665726167652d70672d
6c65646765720265302e322e3003500000000000000000000000000000000104
5000000000000000000000000000000010055000000000000000000000000000
000020065000000000000000000000000000000030075820e3b0c44298fc1c14
9afbf4c8996fb92427ae41e4649b934ca495991b7852b855086172095820808a
5ca10093b0a12b6aafb45606e58f53000c012450adc1e437dd80b8bb8a520a61
695840a9bdacca8a7bfc158af3bfb3e56c498381e03b1a35be6145f84133b828
5e3bd2f3892566aca4b4fc31b8fab3cd36fb2c911aa5445ffcb49a73f691c23b
b3fe00

Line breaks and spaces in these hexadecimal listings are display separators; discard them before hexadecimal decoding. The signature verifies over the exact Sig_structure specified in Appendix A.4. Reproducing these bytes checks encoding and signature handling; it does not establish issuer authority, occurrence of an action, population closure or a Coverage claim.¶

C.2. Complete Single-Claim Result Example

This separate JSON object requests one claim; it does not evaluate the preceding receipt. It is explicitly a constructed format example: no collection or evaluation has taken place, so the claim is not-evaluated and has no outcome. Null bindings and cutoffs are permitted for this artifact kind only; a consumer rejects it as evaluation evidence under Appendix A.11.¶

{
  "artifact_kind": "constructed-example",
  "contract": "CoverageResult/0.2.0",
  "rule_set": "coverage/0.2.0",
  "profile": "wexp-coverage-pg-ledger",
  "profile_version": "0.2.0",
  "result_id": "example-1",
  "evaluator": {
    "id": "example",
    "version": "0"
  },
  "evaluation_time": null,
  "input_manifest": null,
  "context": {
    "id": "example-context",
    "epoch_id": "00000000-0000-0000-0000-000000000001",
    "database_incarnation": "00000000-0000-0000-0000-000000000010",
    "scope":
      "durable-commits-to-coverage_pg.action_ledger-in-epoch",
    "receipt_stream": "coverage_pg.finalization_ledger",
    "recipient_id": "r",
    "payload_projection": "sha256-of-exact-action-payload-bytes",
    "pinned_policy": null,
    "action_cutoff": null,
    "creation_cutoff": null,
    "receiver_cutoff": null
  },
  "assumption_policy": null,
  "requested_claims": [
    "creation-exact"
  ],
  "claims": [
    {
      "id": "creation-exact",
      "role": "requested",
      "evaluation_status": "not-evaluated",
      "reason": "Format example; no collection or evaluation.",
      "derivations": [],
      "inherited_assumptions": [],
      "diagnostic_refs": [],
      "limitations": []
    }
  ],
  "premises": [],
  "views": {
    "S": {
      "availability": "unavailable",
      "enumeration": "unavailable",
      "integrity": "unknown",
      "temporal_closure": "unknown",
      "branch_coverage": "unknown",
      "population_exactness": "unknown",
      "premise_refs": [],
      "retained_invalid_refs": [],
      "limitations": []
    },
    "Cv": {
      "availability": "unavailable",
      "enumeration": "unavailable",
      "integrity": "unknown",
      "temporal_closure": "unknown",
      "branch_coverage": "unknown",
      "population_exactness": "unknown",
      "premise_refs": [],
      "retained_invalid_refs": [],
      "limitations": []
    },
    "Rv": {
      "availability": "unavailable",
      "enumeration": "unavailable",
      "integrity": "unknown",
      "temporal_closure": "unknown",
      "branch_coverage": "unknown",
      "population_exactness": "unknown",
      "premise_refs": [],
      "retained_invalid_refs": [],
      "limitations": []
    }
  },
  "diagnostics": [],
  "transformations": [],
  "unperformed_checks": [
    "Deployment collection and Coverage evaluation."
  ],
  "limitations": [
    "Constructed example; not evaluation evidence."
  ],
  "supersedes": []
}