GitHub

Polyvariant R1-S2 Contract

Status: implemented and bounded-differential validated

Stage: Roadmap Stage 3 / structural polyvariant slice

Decision: ADR-0032

1. Purpose

R1-S2 extends the proven S1 control machine with structural Tuple/Sum partial values, alias-normalized flattened signatures, exhaustive dynamic Case, and bounded zero-residual helper result propagation.

It is an append-only boundary. Calling S2 cannot create, validate, or mutate an S1 result.

2. API and temporary trust boundary

specialize_polyvariant_r1_s2(
  validated: ValidatedSpecializationRequest,
  budget: PolyvariantR1S2Budget
) -> Result<PolyvariantR1S2Specialization, PolyvariantR1S2Error>

The opaque R0-A validated request temporarily supplies verified source identity, whole static/dynamic entry slots, and an upper resource envelope. S2 creates its own policy hash and request hash and does not emit R0 evidence.

3. Admitted subset

  • P1V0 and empty effect rows;
  • no region parameters;
  • recursively pure Unit/Bool/I64/F64/Tuple/Sum parameters, locals, fields, call arguments, and results;
  • Use, Tuple, Project, Construct, admitted scalar primitives, direct Call, Let, If, exhaustive canonical Case, Return, and TailCall;
  • at most one reachable recursive call-graph SCC;
  • no arrays, references, closures, handlers, effects, Text, or Bytes.

Unsupported reachable syntax is rejected even if one entry input would avoid it.

4. Partial-value and version-key rules

The normalized domain, derived-atom rules, first-occurrence alias numbering, and flattened residual signature are normative as specified by ADR-0032. An atom is a proven equality class; individual occurrences may carry scope-local but structurally proven-equal operands. Flattening passes the first left-to-right operand once.

Whole static entry Tuple/Sum values enter as Known. Whole dynamic Tuple enters as a typed Hole; whole dynamic Sum enters as UnknownSum. Partial entry slots await the dedicated R1-A request, but partial structures may arise inside the admitted program.

Canonical S2 patterns expose:

KnownUnit | KnownBool | KnownI64 | KnownF64
KnownTuple([Pattern])
Hole(Type, alias)
Tuple([Pattern])
KnownSum(SumType, constructor, [Pattern])
UnknownSum(SumType, alias)

All NaNs use one key bit pattern. Positive and negative zero remain distinct.

5. Specialization semantics

  • all-known admitted primitives fold with Core-N0 numeric semantics;
  • dynamic primitives remain residual and produce a typed atom;
  • structural Tuple construction and KnownSum construction remain virtual;
  • structural projection and known Case selection erase;
  • opaque Tuple projection remains residual;
  • UnknownSum Case keeps all canonical arms and consumes arms - 1 control splits;
  • dynamic If keeps both arms and consumes one control split;
  • direct and tail calls use pending exact structural version keys;
  • only ADR-0032 eligible zero-residual helpers may be erased;
  • an explicit frame machine, not host recursion, unfolds helper-summary chains; it accepts exactly 256 entries and preserves the call at the next entry, while declared budget exhaustion rejects the whole attempt;
  • partial aggregate returns materialize children before parents.

Any conservative helper refusal preserves an ordinary residual call. Budget failure rejects the attempt rather than choosing a different residual.

6. Exact budgets

The eight S2 budget fields and their hard caps are policy-bound. Exact usage must pass; one-below usage must fail with the corresponding typed error. Every field rejects zero and values above its hard cap.

work_units has the exact structural-event meaning fixed by ADR-0032. It is not a claim that every host instruction, comparison, byte copy, residual encoder step, or ordinary verifier step is counted; those phases remain size-bounded by the other admitted envelopes.

The S2 request hash binds the source, upstream envelope, policy, entry, and all eight limits. Changing a sufficient limit changes request identity but not policy identity, residual semantics, or measured usage.

7. Required evidence

The first S2 corpus must cover:

  • Tuple projection erasure and partial Tuple return materialization;
  • KnownSum Case erasure and UnknownSum exhaustive Case residualization;
  • nested structural transport;
  • known and partial helper result propagation;
  • refusal of dynamic-control and recursive helper summaries;
  • alias-sensitive (x,x) versus (x,y) version keys and signatures;
  • aggregate recursion through pending exact keys;
  • canonical nested F64 NaN and signed-zero identity;
  • exact/one-below, zero, and hard-cap budget behavior;
  • residual node/byte limits;
  • deterministic policy, request, version, residual, and usage identity;
  • ordinary Core verification and bounded original/residual differential evaluation;
  • unchanged S1 locked vectors and 19-test regression corpus.

8. Exit condition

R1-S2 becomes implemented only when the admitted and rejected corpus, every exact budget boundary, deterministic identity vector, full workspace tests, strict Clippy, formatting, and documentation audits are green.

The accepted sequence continues with R1-S3 effects-preserving arrays and bounded CoreVM0 integration, then R1-S4 independent replay plus structural dispatch erasure. Current status is governed only by ../ROADMAP.md.

9. Locked implementation evidence

Policy version: 1.1.0

policy   034ef346e4b036b8860e196fdb065c3b99ae024809d497a97ebccc66eb5c55f1
request  9a1707f75a3bb4d1f2d0bfea38b62999248b2e549c24f9f90886bda773c0f1f9
residual d617aa9405c91b494a71b9fe533b05ec0c364774e1b766b14b9295e57c27353e

usage:
  work_units=254
  partial_value_nodes=15
  variants=2
  control_splits=2
  dynamic_parameters=6
  helper_unfolds=2
residual_nodes=23
residual_bytes=549

The focused R1-S2 corpus is green at 16/16. The frozen R1-S1 regression corpus remains green at 19/19. Full workspace tests, strict all-target/all-feature Clippy, formatting, and documentation whitespace checks are green at acceptance.

10. Non-claims

R1-S2 is not R1-D evidence, CoreVM0 specialization, dispatch erasure, native code, standalone execution, Futamura P1/P2, performance leadership, Projection Birth, dependency closure, Rust/Cargo removal, or Nauxogenesis.