Binding-Time B0 Contract

Status: complete; B0-A/B/C/D implemented and validated
Stage: Roadmap Stage 2
Authority: ADR-0002 and ADR-0018, with the B0-A boundary fixed by ADR-0019 and B0-B fixed by ADR-0020, with B0-C fixed by ADR-0021

1. Objective

B0 establishes a deterministic and independently checkable binding-time judgment over verified P1V0 Core artifacts:

Γs ; Γd ⊢ node : T @ b ! effects
b ::= Static | Dynamic
Static ≤ Dynamic

B0 classifies dependency. It does not evaluate static code, generate Residual Core, invoke the trace JIT, or claim Futamura P1.

Implementation slices:

2. Admitted input

A B0 request contains:

source CoreArtifact
source_program_hash
interpreter_semantics_hash
entry parameter binding-time manifest
analysis-policy version and hash
max_nodes
max_call_edges
max_fixpoint_iterations

Requirements:

• the artifact verifies under Core P1V0 before analysis;
• source_program_hash equals the verified artifact semantic hash;
• interpreter_semantics_hash equals the locked P1V0 identity;
• the manifest has exactly one entry for each entry-function parameter, in canonical parameter order;
• every budget is non-zero and within an implementation hard cap;
• unknown schema, profile, identity, policy, or field fails closed.

B0-A hard caps:

max_nodes               = 1_000_000
max_call_edges          = 1_000_000
max_fixpoint_iterations = 65_536

Static values are not embedded or evaluated by B0. A later specializer request will bind values to the classifications certified here.

3. Lattice

join(Static, Static)   = Static
join(Static, Dynamic)  = Dynamic
join(Dynamic, Static)  = Dynamic
join(Dynamic, Dynamic) = Dynamic

join is commutative, associative, idempotent, and monotone. Dynamic never becomes Static during inference.

B0-A implements and exhaustively tests this lattice. B0-B assigns it to the entry function’s terms, rvalues, and operands. B0-C applies the same monotone domain to whole-program function summaries.

4. Canonical B0-A identity

Policy domain:

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

Policy bytes contain, in order:

domain
Core schema name and version
policy version 1.0.0
P1V0 profile tag
locked P1V0 interpreter-semantics hash
three hard caps
ordered capability IDs

Capability IDs:

two-point-static-dynamic-lattice-v1
conservative-dynamic-control-v1
fixed-p1v0-input-v1
effect-eligibility-separated-v1
deterministic-least-fixpoint-v1
stable-structural-node-path-v1
fail-closed-budget-v1

Request domain:

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

Request bytes contain, in order:

request schema version
source program hash
P1V0 interpreter-semantics hash
policy version and hash
entry-manifest length and ordered U8 binding-time tags
max_nodes
max_call_edges
max_fixpoint_iterations

All integers are unsigned big-endian. Static = 0 and Dynamic = 1. Strings use U32-length-prefixed UTF-8.

Locked B0-A vectors:

policy_hash =
ee19444d56fe1de89eab9a0054c556b47e7ad115ec12255511d31a4526261a51

The sample request uses a pure P1V0 entry function with two I64 parameters and returns parameter 0; its manifest is [Static, Dynamic] and its budgets are 1024, 512, and 32:

source_program_hash =
681ba7a62f778e3a20aa059b4fc2b2dfc4f17877f6b61a686ecd50618b3b87c2

request_hash =
e338943aedab84880f56cbd627af68cf18a43cf101e17bf08006b2c0add1bfd3

5. Conservative judgment

Literals are Static. A local has the binding time assigned by its parameter, pattern binding, or let definition.

For Use, tuples, projection, construction, and primitives, the result is the join of all data dependencies and current control dependence. For if and case, the condition or scrutinee joins the control dependence of every branch. A value selected under dynamic control is therefore dynamic in B0.

Direct calls and tail calls use monotone, context-insensitive whole-program function summaries:

reachable
ordered parameter binding times
incoming control binding time
result binding time
static-evaluation eligibility

Entry manifest classifications seed the analysis. Call-site argument classifications flow into callee parameters; caller control flows into callee control; callee result classifications flow back into callers. The explicit control field prevents a zero-argument constant callee from being classified static when invoked under dynamic control.

Recursion is solved by synchronous least-fixed-point rounds. Each round reads one immutable summary snapshot, visits snapshot-reachable functions in increasing FunctionId, and joins all contributions into the next snapshot. Newly reachable functions run in the following round. Only judgments from the stable round are returned.

B0 may conservatively classify a value as Dynamic. It may never classify a dynamic-dependent value as Static.

B0-B retains its bounded entry-only API and rejects calls with UnsupportedInterprocedural. B0-C implements the interprocedural API, deterministically sorted stable-round judgments, ordered whole-program summaries, and cumulative node/call-edge/fixed-point usage.

6. Effects versus evaluation permission

Binding-time classification does not authorize specialization-time execution. Each evidence node separately records whether default static evaluation is:

EligiblePure
Denied

Only effect-free, deterministic P1V0 work may be EligiblePure. Typed errors, unknown effects, allocation, mutation, handlers, IO, FFI, time, randomness, environment access, external state, and nondeterminism are Denied unless a future accepted capability says otherwise.

B0 performs no effect and consumes no compile-time capability.

7. Stable node identity

Evidence identifies a node by:

FunctionId + canonical structural path

A structural path is a sequence of versioned grammar-field tags and big-endian sequence indices. It is derived from canonical Core order; Rust addresses, enum layout, filenames, traversal hash-map order, and source names are absent. The function body has an empty path; non-sequence fields use index zero.

Node Identity Encoding v1 uses:

domain = "NAUX:core-n0:binding-time-node:b0:v1\0"
FunctionId: U32
path length: U32
path segment = field tag: U8 + index: U32

The tag table is normative in ADR-0020. The locked vector for function 3, path LetValue[0] / PrimitiveArgument[1] is:

node_hash =
dd595008d078ed4efbcf91aabb73ac9bccb16bea1cdeda63a4385996f95501fa

8. Evidence and independent verification

A canonical certificate follows binding_time_b0_evidence_v1.md.

A B0 certificate contains:

certificate schema/version
source_program_hash
interpreter_semantics_hash
analysis_policy_hash
request_hash
entry manifest
ordered node judgments
ordered function summaries
declared budgets
budget usage
certificate hash

The independent verifier accepts the verified Core artifact, request, and certificate. It recomputes node identities, dependency propagation, joins, effect eligibility, fixed-point summaries, hashes, and budget accounting. It does not trust analyzer-owned cached decisions.

Missing, duplicate, reordered, unknown, inconsistent, over-budget, or forged evidence fails closed.

9. Determinism and exhaustion

Canonical ordering is:

1. increasing FunctionId;
2. grammar field order;
3. increasing sequence index;
4. increasing fixed-point iteration.

The same artifact and request must produce byte-identical evidence. Node and call-edge usage is cumulative across every analyzed round; iteration usage counts every started synchronous round. Each budget is checked before consumption. Exhaustion returns a typed B0 failure and no analysis or valid certificate. It must not emit partial evidence, silently raise a budget, evaluate the program, or fall back to trace-JIT specialization.

10. Acceptance evidence

B0 is complete only when all of the following are green:

• exhaustive two-point lattice-law tests;
• literal, parameter, let, primitive, tuple, constructor, branch, case, direct-call, tail-call, and recursive-summary positive tests;
• dynamic dependency and dynamic control contamination tests;
• pure-eligibility and effect-denial tests;
• exact node-identity and certificate stability vectors;
• deterministic results across repeated runs and sufficient budgets;
• exact budget accounting and exhaustion tests;
• forged program, semantics, policy, request, node, summary, ordering, budget, and certificate hash rejection tests;
• analyzer/verifier differential mutation tests;
• strict lint, full workspace, governance, shell, link, and diff gates.

The implemented subsets are locked by naux-lang/tests/binding_time_b0a.rs, naux-lang/tests/binding_time_b0b.rs, and naux-lang/tests/binding_time_b0c.rs. This list remains the acceptance gate for complete B0.

11. Complete B0 validation evidence

The complete B0-A/B/C/D boundary passed:

• 33 focused tests covering lattice, request, node, and certificate vectors, provenance forgery, path ordering, data/control contamination, tuple/sum propagation, effect eligibility, B0-B call rejection, direct/tail calls, dynamic incoming control, recursive convergence, conservative context merging, exact cumulative budgets, analyzer/verifier differential replay, and certificate mutation rejection;
• strict Clippy and formatting;
• all 455 workspace tests;
• 22 governance tests;
• syntax checks for all 9 shell scripts;
• 67 Markdown files and 121 local links with no missing target;
• diff hygiene and Core source-isolation gates.

The only emitted warning is the already-declared bridge dependency warning for nom 1.2.4; it is not part of the std-only Core staging module.

12. Non-claims

B0 is not static evaluation, partial evaluation, residualization, a specializer, CoreVM0, P1, P2, native code generation, dependency closure, Projection Birth, or Nauxogenesis.