Polyvariant R1-S1 Contract

Status: implemented and bounded-differential validated

Stage: Roadmap Stage 3 / first R1 control slice

Decision: ADR-0031

1. Purpose

R1-S1 is the first executable slice of the polyvariant specializer. It tests two mechanisms that R0 deliberately does not provide:

specialize a call whose arguments or result remain dynamic
residualize both sides of dynamic control through memoized function versions

The output is ordinary verified P1V0 Core. This slice establishes neither the full R1 evidence boundary nor CoreVM0 dispatch erasure.

2. Lineage and trust boundary

B0 and R0 v1 remain frozen. R1-S1 accepts an existing ValidatedSpecializationRequest as a temporary in-process integrity envelope for:

• a verified Core artifact and its semantic identity;
• the entry function and exact typed entry slots;
• the independently checked static scalar values;
• the existing residual node and canonical-byte resource envelope.

R1-S1 does not reinterpret the B0 v1 control-dependency judgment as path-sensitive permission and does not emit an R0-B, R0-C, or R0-D artifact. It performs a separate structural admission of the pure scalar R1-S1 subset. The dedicated R1-A raw request, policy certificate, canonical encoding, and public admission API remain later work.

The executable entry point is:

specialize_polyvariant_r1(
  validated: ValidatedSpecializationRequest,
  budget: PolyvariantR1Budget
) -> Result<PolyvariantR1Specialization, PolyvariantR1Error>

The specialization result is opaque. Read-only accessors expose its residual artifact and deterministic report; callers cannot construct or mutate a trusted result.

3. Admitted source subset

Admission walks the call graph reachable from the selected entry and requires:

• Core profile P1V0;
• empty effect rows and no effect operation or handler;
• scalar parameter, local, call-argument, and return types only: Unit, Bool, I64, or F64;
• Use, admitted scalar unary/binary primitives, direct Call, Let, If, Return, and TailCall;
• no Tuple construction/projection, Sum construction/Case, array operation, reference, closure, Unique, ownership-return, or other aggregate form;
• at most one reachable recursive call-graph strongly connected component.

Non-recursive helpers may surround the one recursive component. Recursive edges are admitted only through the same verified direct/tail-call forms as other calls. Unsupported reachable syntax, type, effect, or call topology is a typed admission failure, even if one observed input would not execute it.

Entry slots are exactly:

Known scalar SpecializationValue
Dynamic scalar Type

A value/type mismatch, aggregate slot, static array, wrong arity, or non-scalar entry signature has no residual fallback and is rejected.

4. R1-S1 partial values

The slice uses the scalar restriction of ADR-0031:

ScalarPartial =
    Known(Unit | Bool | I64 | F64)
  | Dynamic(Type)

Dynamic(Type) never implies equality with another dynamic slot, even when the two slots have the same type. R1-S1 may share one version for equal ordered scalar/dynamic patterns because the residual call still supplies each operand independently; no equality-based fold is permitted.

The later structural Hole, Tuple, KnownSum, and UnknownSum domain is not silently approximated here. Encountering those values rejects the S1 request.

Canonical scalar identity follows Semantic Encoding v1:

• Unit, Bool, and I64 encode exactly;
• all NaN payloads form the canonical unobservable NaN class;
• positive and negative zero remain bit-distinct;
• infinities retain their exact sign.

5. Version identity

Each S1 version is keyed by:

ScalarVersionKey {
  source_function_id,
  ordered_parameter_pattern: [Known(canonical scalar) | Dynamic(Type)]
}

Source locals, transient residual locals, host addresses, hash-map iteration order, and discovery allocation order are not key material.

Before a body is specialized, its exact key is inserted as Pending. Encountering the same key emits a call to that version and closes a recursive knot. A call with a different pattern reserves another version. No monovariant join, widening, version eviction, or generic fallback is allowed.

After bounded discovery, canonical key encodings determine the final variant order and residual FunctionIds. All calls are lowered through that final table. Repeating specialization with the same source, entry slots, policy, and budgets must produce the same:

variant descriptors
source-to-residual function mapping
residual program
residual semantic hash
exact usage report

6. Specialization semantics

R1-S1 runs an explicit version worklist. Source call recursion reserves or reuses a version and therefore never follows the recursive call on the host stack. The Rust seed still traverses each already-verified scalar term tree recursively inside one version; replacing that structural traversal with the full R1 continuation machine is required before the larger CoreVM0 artifact is admitted.

Scalar operations

An admitted pure primitive is evaluated only when every operand is Known. It uses the frozen Core-N0 numeric and comparison semantics. Otherwise the primitive is emitted in the current residual version and its result becomes dynamic.

Known Use operands become canonical scalar literals. Dynamic operands become typed residual operands. Let binding, operand evaluation order, wrapping I64 behavior, strict F64 behavior, NaN class, and signed zero are preserved.

Mixed direct calls

A direct call is entered with the ordered partial arguments even if at least one argument or the result is dynamic. Its version is reserved or reused by exact key.

R1-S1 does not compute or propagate callee result summaries. Every direct call is therefore emitted as a residual direct call and its binder becomes dynamic, even when the specialized callee body later returns a known scalar. This is a deliberate conservative boundary, not a semantic requirement of R1. Bounded helper unfolding and known-result propagation belong to R1-S2. The specializer never invokes the dynamic call through the Core seed interpreter.

Mixed tail calls and recursion

A tail call follows the same key rule. A known-result exit becomes a residual return of that scalar; a dynamic or recursive exit becomes a residual tail call. Re-encountering a pending exact key is success, not a cycle error.

A recursive call that changes a known argument creates a new version. If this produces an unbounded sequence of keys, the version or step budget rejects the whole specialization. R1-S1 does not generalize the changing value to dynamic.

Dynamic If

A known Bool condition selects exactly one branch. A dynamic Bool condition:

1. consumes one branch split from the R1-S1 budget;
2. snapshots the incoming scalar partial environment;
3. specializes both branches independently;
4. emits a residual If with both specialized terms.

Neither runtime branch is chosen or executed. Pure known operations may fold inside each branch. A branch-local fact cannot be hoisted, leaked into the other branch, or used after a join unless both results are the same canonical known scalar. Branch order is source order and is part of deterministic specialization.

Case is outside S1, including a scalar-payload Sum.

7. Budgets and usage

PolyvariantR1Budget has four positive bounded fields:

max_steps
max_variants
max_branch_splits
max_dynamic_parameters

The corresponding usage report has one exact counter for each field.

• steps counts normative body-specialization actions, not Core-N0 runtime steps, bytecode opcodes, admission/SCC analysis, canonical-key construction or sorting, final lowering, encoding, or verification. It is therefore not a total CPU or memory meter for the current Rust seed.
• variants counts each distinct reserved scalar version key, including a pending recursive version exactly once.
• branch_splits counts each dynamic If specialized in a distinct version.
• dynamic_parameters counts the dynamic residual parameters allocated by the canonical version table.

The validated request’s existing max_residual_nodes and max_residual_bytes retain their R0 numeric meanings as output resource limits; using those caps does not turn the result into R0 evidence.

Zero, hard-cap overflow, counter overflow, or usage > limit fails closed. The check occurs before publishing a result. Exhaustion returns no partial program, report, or reusable version table.

The verified source and residual node/byte bounds still cap the admitted and published artifacts. Before R1 admits structural partial values, aggregate helpers, or CoreVM0, R1-S2 must add an explicit structural-event work/partial-value-node budget so key construction and helper analysis cannot grow outside a declared resource contract.

8. Residual artifact

Each residual version:

• removes known source parameters;
• retains dynamic parameters in canonical source-slot order;
• contains only admitted scalar P1V0 constructs;
• references only functions present in the final canonical version table.

The residual entry accepts exactly the dynamic entry slots. Known static values are absent from its runtime signature. Dead source functions and unreachable unused variants are not residual roots.

Before success, R1-S1:

1. resolves every pending version and call target;
2. enforces specialization and output budgets;
3. constructs the canonical Core artifact;
4. runs the ordinary Core verifier;
5. records its semantic hash, variant descriptors, and exact usage.

Failure of any check rejects the entire result. An arbitrary verified Core artifact is not an R1-S1 result; opaque construction is the current in-process boundary.

9. Required executable evidence

The bounded S1 test matrix must include:

• complete folding with all-scalar-known inputs;
• one known and one dynamic argument through a direct call with dynamic result;
• a mixed tail call whose exact key re-enters a pending recursive version;
• recursion that creates a finite sequence of distinct static variants;
• recursion that exceeds the variant cap and fails without widening;
• dynamic If preserving both branch results and source evaluation order;
• nested dynamic branches and exact branch-budget rejection;
• deterministic variant descriptors, FunctionIds, semantic hash, and usage;
• canonical NaN key behavior and signed-zero key distinction;
• rejection of Tuple, Sum, array, effectful, malformed, and non-scalar input;
• rejection of more than one reachable recursive SCC;
• residual node/byte, step, variant, branch, and dynamic-parameter limits;
• ordinary Core verification of every successful residual;
• original-versus-residual differential evaluation over a bounded scalar corpus, including wrapping and F64 edge cases.

Mutation tests must cover version descriptors, residual call targets, source identity, and every budget/usage field once a serialized R1 boundary exists. Until R1-D exists, the opaque report is diagnostic output, not portable evidence.

Malformed entry envelopes cannot enter the public S1 function because it accepts only an opaque ValidatedSpecializationRequest. The S1 pipeline corpus demonstrates the wrong-scalar-type rejection; the existing specialization_r0a corpus covers forged arity and identity. These are R0-A admission failures before R1 is callable, not PolyvariantR1Error paths.

10. Implemented evidence and locked vector

The green 19-test R1-S1 integration corpus exercises the pure-scalar P1V0 worklist over known and dynamic entry patterns, mixed-result direct calls, mixed tail calls, same-key and mutually recursive single-SCC knots, finite and budget-divergent static variants, and both sides of single and nested dynamic If. It also covers all-known folding, canonical-key-byte version numbering, nonzero source-entry remapping, exact and hard-cap budget boundaries, output caps, rejected Tuple/Sum/array/effectful and call-graph shapes, canonical NaN keys, signed-zero distinction, dynamic F64 edge values, and original-versus-residual evaluation.

Every successful result is finalized through the ordinary Residual Core path and accepted by the ordinary Core verifier. The stable same-key tail-loop vector locks:

policy_hash =
21658612344c5d3502c3b74769131bb90c9f1f1e6c1599503afd142e536c19d1

request_hash =
0f245e34a481d407afc124b0c540aba06596697a624dcc2794abaec8b6aa2423

residual_hash =
a82ed85ffd70e3bfc8438156a04535e732d60d8166fd53e2ebe2a96f1650f615

usage = {
  steps: 8,
  variants: 2,
  branch_splits: 1,
  dynamic_parameters: 2
}

residual_nodes = 16
residual_bytes = 188

The policy identity is stable across admissible request-budget changes while the request identity changes. This is an in-process deterministic vector, not an independently replayable R1-D certificate.

11. Exit condition and successor

R1-S1 is complete only when its admitted success corpus, fail-closed corpus, determinism vectors, and bounded differential corpus are green under the ordinary interpreter and verifier.

That bounded R1-S1 condition is satisfied. It closes only the pure-scalar control slice.

The accepted follow-on sequence adds, under separately reviewed contracts:

R1-S2  structural PartialValue, KnownSum/UnknownSum and helper unfolding
R1-S3  effects-preserving array operations and CoreVM0 integration
R1-S4  R1-D evidence, independent replay and structural dispatch erasure

Those labels express dependency order. Current status is governed only by ../ROADMAP.md.

12. Non-claims

R1-S1 does not provide portable R1 evidence, an independent replay verifier, partially-static Tuple/Sum values, arrays, effects, CoreVM0 specialization, opcode or fetch erasure, residual SSA, native lowering, standalone execution, Gate A/B/C completion, Futamura P1/P2, performance leadership, Projection Birth, dependency closure, Rust/Cargo removal, or Nauxogenesis.