ADR-0031: Evidence-Gated Polyvariant R1 Boundary

Status: accepted

Date: 2026-07-28

Supersedes: none; introduces an R1 successor boundary while B0/R0 v1 remain frozen

Context

ADR-0030 provides one generic, verified P1V0 definition of CoreVM0. Its full ProgramImage is static, but its argument array and repetition count are dynamic. The current B0/R0 v1 pipeline cannot specialize that combination:

• binding time is one value for an entire Tuple or Sum, so a dynamic payload destroys a known constructor or tuple shape;
• dynamic control is joined into every value below it, including an otherwise static program image or program counter;
• call summaries are monovariant and R0-B2 enters only wholly static calls;
• a call with a dynamic result is preserved rather than specialized;
• R0-C2 cannot create recursive function versions or specialize both sides of dynamic control.

Changing one of those rules alone is insufficient. For example, splitting a dynamic branch without partial values still loses known instruction tags, and partial values without memoized recursive versions still merge all program counters back into one generic loop.

B0-D and R0-D already have locked policy, encoding, trace, and evidence identities. Reinterpreting those records would make old evidence mean something it did not certify. Stage 3 therefore needs a new versioned boundary.

Relationship to ADR-0029 and ADR-0030

ADR-0029 remains normative for CoreVM0 Bytecode v1 opcode semantics, verification rules, numeric behavior, hard limits, and the locked legacy live-instruction image identity.

ADR-0030 supersedes only ADR-0029’s instruction-only Stage 3 admission interpretation. It adds the fixed full ProgramImage and the generic definitional artifact; it does not invalidate the legacy hash vector or alter the bytecode semantics.

This ADR supersedes neither decision. R1 will eventually consume the ADR-0030 artifact and image through a new specialization/evidence policy. The first R1 slice deliberately does not admit CoreVM0.

Options considered

Decision

Preserve B0 and R0 v1 exactly. Append an R1 pipeline with four explicit boundaries:

R1-A  partial-value admission, path-sensitive permission, request and budgets
R1-B  mixed-call specialization, dynamic control and memoized variants
R1-C  deterministic verified Residual Core and structural correspondence
R1-D  sealed evidence, independent raw-input replay and erasure validation

No R1 artifact may be represented as an R0 v1 artifact or validated under an R0 policy hash. R1 versions its requests, canonical encodings, policies, and evidence independently.

Partial-value domain

R1 uses a typed structural domain:

PartialValue =
    Known(canonical SpecializationValue)
  | Hole(Type, ResidualAtom)
  | Tuple(TupleType, [PartialValue])
  | KnownSum(SumType, constructor, [PartialValue])
  | UnknownSum(SumType, ResidualAtom)

Tuple preserves each field independently. KnownSum proves the constructor while its payload may contain holes. UnknownSum preserves the exact Sum type without inventing a constructor. A fully known structure is normalized to Known; ill-typed fields, constructor arity mismatches, and unbound atoms are rejected.

Residual atoms are typed and alpha-normalized. Repeated use of one atom keeps alias identity; different atoms remain distinct. Transient LocalId or host allocation order is not semantic identity. Static values use their canonical specialization-value encoding, including canonical NaN treatment while preserving signed zero.

Path-sensitive execution permission

Knowledge and permission are separate. A value being known does not by itself authorize executing the node that produced it.

R1-A must prove, for the current function version and residual path, whether a node may be evaluated during specialization, must be residualized, or is outside the admitted profile. Specialization-time evaluation is allowed only for verified pure, effect-free, identity-unobservable work with every required value known. Effectful, dynamically dependent, denied, or unproven work is never executed.

Structural reduction is a separate permission: projecting a known Tuple field or selecting a KnownSum arm may transport partial children without evaluating their holes. An UnknownSum arm derives deterministic typed field atoms from the scrutinee atom and arm position. Neither operation may inspect or execute a dynamic payload.

For dynamic If, R1-B evaluates neither runtime path as a chosen path. It clones the partial environment and specializes both branches. Pure known work may fold inside either residual branch, but it cannot be hoisted out or leak to another path without an explicit equal-value join. Future dynamic Case uses the same rule; KnownSum selects one proven arm and UnknownSum residualizes every admissible arm.

This is a new R1 permission policy. B0 v1’s conservative control join remains correct and unchanged for B0/R0 v1, but it is not R1 execution authority.

Mixed calls and memoized variants

A direct or tail call may be specialized when its arguments are a mixture of known values and typed holes, even when the result remains dynamic. The specializer enters the callee symbolically; it does not execute dynamic operands or observable effects.

Each version has a canonical key:

VersionKey {
  source_function,
  normalized_argument_patterns
}

The key preserves static values, partial structure, types, and hole aliasing. Before specializing a body, R1-B reserves its key as Pending. Encountering the same key through recursion emits a residual call to that pending version and closes the knot. A different key creates another bounded version. R1 never widens, merges, or silently falls back to a generic interpreter when a limit is reached.

Variant discovery uses a normative deterministic worklist. After the complete bounded version graph is known, canonical key encodings are sorted and residual FunctionIds are assigned deterministically. Residual references are then lowered through that table. Host-stack recursion is not part of the algorithm.

Budgets and fail-closed behavior

The full R1 request has independent caps for at least:

max_specialization_steps
max_partial_value_nodes
max_specialized_versions
max_branch_splits
max_dynamic_parameters_per_version
max_residual_nodes
max_residual_bytes

Each counter has one versioned meaning and exact recorded usage. Arithmetic overflow, unsupported structure, malformed authority, exhausted budget, unresolved pending version, invalid residual, or identity mismatch rejects the whole attempt. No partial residual or fallback artifact is returned. Existing R0 budget fields are not reinterpreted.

Deterministic residual and structural erasure

R1-C emits ordinary canonical Core and requires the existing Core verifier to accept it. It also builds a canonical origin map from every reachable residual function and node back to its source version/path. The map is transformation evidence, not trusted runtime metadata.

For the future CoreVM0 integration, the structural checker must inspect the entire reachable residual graph and prove at least:

• no ProgramImage, InstructionSlot, Instruction, RuntimeValue, or VM-bank value remains;
• no 64-slot fetch or 16-arm opcode dispatch remains;
• no call to the original entry, loop, fetch, get/set, argument, or trap helper remains;
• no dynamic parameter or hole originates from the static program image, opcode, or source program counter;
• the residual entry contains only the declared dynamic lighthouse inputs;
• every loop-derived version has a canonical descriptor for its static program counter;
• no generic-interpreter fallback is reachable.

Passing the ordinary Core verifier is necessary but does not by itself prove those erasure properties.

Independent replay

R1-D accepts raw source/artifact, raw request and authority, the claimed residual, origin map, structural report, and sealed evidence. It does not trust an emitter-owned validated request, version table, usage report, or residual wrapper.

The verifier re-admits the inputs, reconstructs path permissions and partial values, rediscovers and canonically numbers the version graph, regenerates the residual and origin map, reruns the structural checker, and requires exact identity and budget equality. Evidence binds the source/artifact and ProgramImage hashes, R1 request and policy hashes, version-table and origin-map hashes, residual hash and metrics, exact budget usage, structural-checker version, and canonical structural report.

This is independent admission and regenerative replay, not implementation diversity or a proof-producing optimizer.

First implementation slice: R1-S1

The first bounded slice validates the recursive-version and dynamic-control mechanics before partial aggregates are introduced:

pure P1V0 scalar functions only
known or dynamic scalar arguments
mixed direct and tail calls
at most one reachable recursive call-graph SCC
dynamic If with both branches residualized
memoized exact-key variants
explicit step, variant, branch and dynamic-parameter budgets
ordinary verified scalar Residual Core

R1-S1 excludes Tuple, Sum, arrays, effects, CoreVM0, R1-D evidence, the CoreVM0 structural-erasure checker, and every P1 claim. Its exact executable contract is recorded separately. Its step counter meters body-specialization actions rather than total host work, and direct calls do not propagate callee result summaries. The successor slice must add a structural-event work/partial-value-node budget before admitting structural values or CoreVM0, and owns bounded helper unfolding/result-summary propagation.

Rationale

1. A new R1 identity keeps every accepted B0/R0 v1 artifact meaningful.
2. Structural partial values, path-sensitive permission, mixed calls, dynamic branches, and memoized versions form one sound specialization boundary; omitting any one leaves the CoreVM0 loop generic.
3. Exact-key recursion plus explicit caps gives a deterministic finite algorithm without widening or hidden fallback.
4. Ordinary Core verification checks the output language, while origin and erasure validation check the specialization claim.
5. A scalar first slice isolates the two highest-risk control mechanisms before aggregate and CoreVM0 complexity is admitted.

Trade-offs

• R1 duplicates some request, budget, validation, and replay machinery instead of extending R0 records.
• Exact variants can grow rapidly when static state changes; hard caps may reject programs that a widening specializer could accept.
• Specializing both dynamic branches increases work and residual size.
• Canonical graph discovery and a separate lowering pass use more memory than allocation in encounter order.
• Regenerative R1-D validation repeats specialization and structural checking.

These costs are accepted to preserve deterministic identity, fail-closed authority, and a reviewable route to dispatch erasure.

Consequences

Positive:

• R0 remains a stable, regression-testable specialization lineage;
• R1 can represent known constructors and static program counters alongside dynamic payloads;
• recursive residual versions have bounded, replayable identities;
• future P1 evidence can distinguish semantic equivalence from actual interpreter-structure erasure.

Negative:

• R1-S1 is intentionally not usable for the CoreVM0 lighthouse;
• a second evidence schema and policy must be implemented and maintained;
• no performance claim is permitted until later native and benchmark gates.

Non-claims

This decision does not implement partially-static aggregates, specialize the CoreVM0 artifact, erase dispatch, emit native code, execute standalone, prove semantic preservation for an infinite domain, establish Futamura P1/P2, remove Rust/Cargo seed debt, close third-party dependencies, demonstrate performance leadership, establish Projection Birth, or complete Nauxogenesis.

Revisit trigger

Changing the PartialValue normalization, path permission, version key, aliasing rule, discovery/numbering order, budget meaning, fail-closed rule, origin mapping, structural-erasure predicate, or replay payload requires a new policy/schema version and a superseding ADR.