Binding-Time B0 Evidence Encoding v1

Status: implemented and vector-locked
Authority: ADR-0022
Scope: typed Rust-seed B0 certificate payload, hash, and independent verifier

1. Domain and sealing

Canonical certificate payloads begin with the exact bytes:

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

The certificate’s declared hash is excluded from the payload:

certificate_hash = SHA256(canonical_certificate_payload)

Changing only certificate_hash therefore does not change the payload, but the verifier rejects the certificate when the declared and recomputed hashes differ.

2. Scalar framing

Certificate encoding uses the Core-N0 canonical scalar rules:

• integers are unsigned big-endian;
• IDs are U32;
• enum and Boolean tags are one byte;
• sequences and embedded byte strings are U32 length followed by contents;
• a length greater than U32::MAX fails encoding.

Binding-time tags:

Node-kind tags:

Static-evaluation eligibility tags:

Reachability uses false = 0 and true = 1.

3. Payload

Fields occur in this exact order:

domain bytes
certificate schema major: U16
certificate schema minor: U16
certificate schema patch: U16
source_program_hash: 32 bytes
interpreter_semantics_hash: 32 bytes
policy_hash: 32 bytes
request_hash: 32 bytes
entry_function: FunctionId
entry_parameters: binding-time sequence
judgments: judgment sequence
function_summaries: summary sequence
declared max_nodes: U64
declared max_call_edges: U64
declared max_fixpoint_iterations: U32
used nodes: U64
used call_edges: U64
used fixpoint_iterations: U32

Certificate schema v1 is 1.0.0.

The source, interpreter-semantics, policy, request, entry, manifest, and declared budgets redundantly bind the certificate to its validated B0-A request. The independent verifier recomputes rather than trusts each field.

4. Judgment encoding

Each judgment is:

node byte length: U32
Node Identity Encoding v1 bytes
node-kind tag
binding-time tag
static-evaluation eligibility tag

The embedded node bytes include their own NAUX:core-n0:binding-time-node:b0:v1\0 domain. Judgments must be strictly ordered by node identity. Missing, duplicate, or reordered judgments fail closed.

5. Function-summary encoding

Each summary is:

function: FunctionId
reachable: U8 Boolean
parameters: binding-time sequence
incoming control: binding-time tag
result: binding-time tag
static-evaluation eligibility tag

There is exactly one summary for every canonical Core function, including unreachable functions. Summaries are strictly ordered by FunctionId.

6. Independent verification

The verifier:

1. validates the original Core artifact and B0 request;
2. verifies all provenance fields and the certificate hash;
3. verifies canonical summary and judgment sets/order;
4. independently replays synchronous fixed-point rounds;
5. requires exact equality of the final summaries, stable-round judgments, and cumulative budget usage.

The replay implementation is isolated from the analyzer and never calls analyze_binding_time_b0c.

The current admitted input is the typed certificate structure. A byte decoder is not admitted yet; a future decoder must reject unknown tags, truncation, trailing bytes, and non-canonical values.

7. Locked vector

The vector program contains:

• function 0(I64) -> I64, which direct-calls function 1 and returns its result;
• function 1(I64) -> I64, which returns its parameter;
• entry manifest [Dynamic];
• budgets max_nodes = 1000, max_call_edges = 100, max_fixpoint_iterations = 20.

Locked identities:

source_program_hash =
6b87a181255c263e0c644c301b13138c938e91554d93dac77a44ac4974d239ee

interpreter_semantics_hash =
d9911cf60e5afa54e271cdff274cde41b522a4a0c9855ccd6efbcd4e981909cc

policy_hash =
ee19444d56fe1de89eab9a0054c556b47e7ad115ec12255511d31a4526261a51

request_hash =
f0dcae4b50ff15e92a11bed8b074c41cf83c7dba961c14f5779ccbc58eeae451

certificate payload bytes = 660

budget usage = nodes 26, call_edges 4, fixpoint_iterations 4

certificate_hash =
9e778974108bec97945e6b64294fc6b4a0cba174ef7970b51cceb92f3cf1c857

Any payload-order, framing, tag, summary, judgment, or budget-accounting change must either preserve this vector or introduce a new version/domain.

8. Non-claims

A valid B0 certificate authorizes no static execution. It is not Residual Core, a partial evaluator, CoreVM0, Futamura P1/P2, native code, dependency closure, Projection Birth, or Nauxogenesis.