ADR-0023: R0 Specialization Value and Request Boundary

Status: accepted
Date: 2026-07-26

Context

Complete B0 evidence classifies entry parameters as Static or Dynamic but intentionally contains no concrete values. R0 needs an exact request boundary before any static evaluation or residual generation can be admitted.

The bridge interpreter’s CoreValue contains host-oriented storage such as Arc and later-profile opaque values. Reusing it would make host representation part of specialization identity and make it too easy to admit references or closures accidentally.

Options considered

Option	Benefit	Cost
Reuse bridge `CoreValue`	Existing constructors and type checks	Host storage leaks into identity; later-profile values are representable
Encode arbitrary Core operands	Small value domain	Cannot represent tuples, sums, or read-only arrays needed by P1
Put example values in dynamic slots	Convenient profiling	Conflates specialization with speculative trace feedback
Dedicated canonical value domain and exact slots	Narrow, deterministic, independently reproducible	Requires a separate recursive type checker and encoding

Decision

Introduce a dedicated immutable SpecializationValue domain:

Unit
Bool
I64
F64
Tuple(values)
Sum(type, constructor, fields)
ArrayF64(values)

It contains no runtime pointer, reference, closure, handler, external handle, allocation identity, or bridge container.

Each entry parameter has exactly one specialization slot:

Static(SpecializationValue)
Dynamic(expected Type)

Slot position, kind, and type must match the verified B0 certificate:

B0 Static requires Static(value) and exact recursive Core type matching;
B0 Dynamic requires Dynamic(type) and the exact verified parameter type;
dynamic slots contain no example value.

Canonical identities use three separate domains:

NAUX:core-n0:specialization-value:r0:v1\0
NAUX:core-n0:specialization-policy:r0:v1\0
NAUX:core-n0:specialization-request:r0:v1\0

Value encoding normalizes NaNs exactly like Core Semantic Encoding v1 and preserves signed zero. Tuple, constructor, and array order is semantic.

The R0-A request redundantly binds:

verified source program hash;
P1V0 interpreter-semantics hash;
B0 policy, request, and certificate hashes;
R0 policy version and hash;
ordered specialization slots;
explicit limits for static-value nodes, static array elements, specialization steps, residual nodes, and residual bytes.

All five limits are non-zero, request-hashed, and bounded by fixed implementation hard caps. Validation counts value structure without executing Core.

Rationale

A separate value type prevents interpreter implementation details from becoming specialization semantics.
Exact dynamic holes prevent runtime profiles from masquerading as static facts.
Recursive type checking stops malformed aggregate values before evaluation.
Value/array limits bound request admission itself; later step/residual limits bind the work R0-B/C may perform.
Redundant B0 hashes make certificate substitution fail locally.

Trade-offs

Value and type structure are represented twice in sums and dynamic slots.
Large static arrays require linear validation and hashing.
Fixed hard caps may reject a future legitimate workload.
R0-A adds no executable specialization by itself.

These costs are accepted because an ambiguous static-input boundary would invalidate every later partial-evaluation claim.

Consequences

Positive: R0-B can receive only typed, canonical, B0-consistent static facts under explicit budgets.

Negative: a valid R0-A request proves neither effect-safe evaluation nor residual correctness.

Mitigation: R0-B was kept closed until value, policy, request, type, provenance, and budget vectors passed mutation tests. R0-B must accept only the validated boundary.

Revisit trigger

Add another static value form only when an accepted P1/Core profile requires it. Changing tags, framing, hard caps, NaN policy, or slot semantics requires a new version/domain or superseding ADR.