ADR-0022: B0 Sealed Evidence and Independent Replay

Status: accepted
Date: 2026-07-25

Context

B0-C computes deterministic interprocedural binding-time summaries and stable node judgments. That analyzer output is not evidence until a consumer can bind it to the exact Core artifact, semantic identity, policy, manifest, and budgets and reject forged analysis-owned decisions.

B0-D must remain narrower than residualization. It may classify and verify, but it must not evaluate Core, generate residual code, invoke the trace JIT, or authorize Futamura P1 claims.

Options considered

Decision

Introduce Binding-Time Certificate Encoding v1 with domain:

NAUX:core-n0:binding-time-certificate:b0:v1\0

The canonical payload contains, in exact order:

certificate schema version
source program hash
P1V0 interpreter-semantics hash
B0 policy hash
request hash
entry FunctionId
entry binding-time manifest
ordered stable-round node judgments
ordered whole-program function summaries
declared budgets
cumulative budget usage

The declared certificate_hash is not part of the payload:

certificate_hash = SHA256(canonical_certificate_payload)

Node identities are embedded as length-prefixed Node Identity Encoding v1 bytes. All other scalar, sequence, tag, and integer framing follows the existing canonical Core encoding rules.

The certificate emitter accepts only a ValidatedBindingTimeRequest, runs B0-C, constructs the canonical envelope, and seals it. It does not accept an arbitrary caller-supplied analysis.

The independent verifier accepts the original Core artifact, B0 request, and certificate. It:

1. validates the artifact and request through the B0-A trust boundary;
2. recomputes every redundant provenance field and the certificate hash;
3. rejects missing, duplicate, or non-canonical summary/judgment order;
4. independently replays the synchronous B0-C fixed point in a separate module that does not call the analyzer;
5. requires exact equality of summaries, stable-round judgments, result consequences, and cumulative budget usage.

Typed in-memory certificates are the admitted Rust-seed boundary. A future transport decoder must reject unknown tags, trailing bytes, truncation, and non-canonical encodings before it can become an admitted input path.

Rationale

• Redundant provenance makes substitution failures local and inspectable.
• Excluding the declared hash from its payload gives an unambiguous sealing rule already used by Core artifacts.
• Separate replay prevents cached analyzer judgments from becoming trusted premises.
• Exact ordered equality rejects omitted evidence as well as forged values.
• Keeping the certificate analysis-only prevents B0 completion from silently opening residual execution.

Trade-offs

• Independent replay duplicates transfer and fixed-point logic.
• Every policy change requires coordinated analyzer, verifier, encoding, specification, and vector changes.
• Verification repeats the full bounded analysis cost.
• The first boundary verifies a typed certificate rather than parsing an untrusted byte stream.

Consequences

Positive: B0 results become deterministic, tamper-evident, and independently checkable against their semantic inputs.

Negative: agreement between two Rust implementations is strong executable evidence, not a machine-checked proof of binding-time soundness.

Mitigation: mutation tests attack every envelope and semantic evidence class; future implementations can reproduce the published canonical bytes and rules without depending on Rust layout.

Revisit trigger

Add a canonical decoder and streaming verification only when certificates cross a process, storage, or toolchain trust boundary. Any change to payload order, tags, or semantics requires a new schema/domain or a superseding ADR.