Polyvariant R1-S3 Contract

Status: implemented and bounded-differential validated

Stage: Roadmap Stage 3 / bounds-preserving CoreVM0 admission slice

Decision: ADR-0033

1. Purpose

R1-S3 extends the accepted structural S2 machine just far enough to preserve dynamic read-only Array<F64> operations and admit an exactly bound definitional CoreVM0 package.

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

2. Generic API

specialize_polyvariant_r1_s3(
  validated: ValidatedSpecializationRequest,
  budget: PolyvariantR1S3Budget
) -> Result<PolyvariantR1S3Specialization, PolyvariantR1S3Error>

Policy version is 1.2.0. Policy, request, version-key, and CoreVM0 wrapper identities use separate domains.

3. Admission

• P1V0 only;
• recursively Unit/Bool/I64/F64/Tuple/Sum and read-only Array<F64, RegionId(0)>;
• region parameters exactly [] or [RegionId(0)];
• effect row exactly empty or canonical [Error(Bounds)];
• dynamic arrays only; every static ArrayF64 slot is rejected recursively;
• the S2 term language plus ArrayLenF64 and ArrayGetF64;
• at most two reachable recursive SCCs;
• all other types, effects, regions, nodes, and primitives fail closed.

4. Semantics

• a dynamic array is one opaque typed Hole;
• ArrayLenF64 always residualizes;
• ArrayGetF64 always residualizes and retains its Bounds authority;
• source region/effect signatures are copied exactly to each residual version;
• only empty-effect helpers may unfold;
• a pure helper may select known If/Case control on the explicit frame machine; dynamic helper control preserves the call;
• static entry Tuple/Sum values become shared structural partial children;
• alias, version-key, worklist, materialization, and helper-depth rules remain those of ADR-0032 under the new S3 identity.

5. Budgets

S3 has the same eight independent dimensions as S2. Exact usage passes and one-below fails with the matching typed error. Zero and hard-cap overflow reject every field.

work_units remains deterministic structural-event evidence, not a claim to meter every host instruction, allocation, comparison, byte copy, encoder step, or ordinary verifier step.

6. CoreVM0 wrapper

specialize_corevm0_r1_s3(
  bound: DefinitionalCoreVmArtifact,
  validated: ValidatedSpecializationRequest,
  budget: PolyvariantR1S3Budget
) -> Result<CoreVmR1S3Specialization, CoreVmR1S3Error>

The wrapper requires the validated source to be the bound artifact, slot zero to equal the package’s canonical full ProgramImage, and every remaining slot to be Dynamic with the exact entry type. Its report binds:

CoreVM0 program hash
CoreVM0 full ProgramImage hash
Core interpreter-semantics hash
definitional construction version
generic artifact hash
upstream R0-A request hash
S3 policy/request/residual hashes

Any package, slot, image, source, or identity mismatch returns no residual.

7. Required evidence

• ArrayLen and in-bounds/out-of-bounds ArrayGet source/residual parity;
• exact Bounds outcome and effect-event order;
• region/effect signature preservation;
• static/mutable/wrong-element arrays and foreign effects rejected;
• two recursive SCCs admitted and a third rejected;
• effectful helpers never unfolded;
• concrete CoreVM0 package admission and mutation/binding rejection;
• bounded four-opcode Bounds CoreVM0 source/residual differential cases;
• all eight exact/one-below and zero/hard-cap boundaries;
• deterministic policy/request/residual/usage vector;
• ordinary Core verification;
• frozen R1-S1 19-test and R1-S2 16-test corpora unchanged;
• full workspace, strict Clippy, format, whitespace, and link gates green.

8. Exit and successor

R1-S3 becomes implemented only when all required evidence is green. Its separately decided successor is R1-S4 independent replay evidence plus structural fetch/opcode-dispatch erasure. Current status is governed only by ../ROADMAP.md.

9. Locked implementation evidence

policy   3ec434c5443ce2daa846470b5c505566ab17c98b61f78e2552efb39239413d53
request  4462a744327e1048c1d9a3b358d7700282a9cafa6cb536a8d1a3d82ad410434d
residual 72918bb40a2868a86a6df5a98d1518cf7141d9afb91d7b5e90fb84697bee3575
usage    work=109 partial=8 variants=1 control=1 dynamic=3 helper=1
output   nodes=14 bytes=157

CoreVM program  f44da961b0335c097119a7ed12f941a1c0cbc4fea42813f989e6996fdeae2c5f
CoreVM image    a6f9bb6cecb949b2485e9c025b1fdb21d2cdffe421d58f295555e2be2afb0be4
binding         2c17c52206f0a07b69f0be885ab0070a791c36b4674517cf2908e5a5422870e7
residual        50504e086dcb043f7dcbc82ea38bb225f01ce23e24b20bbbb369721b48afe55c

The focused S3 corpus is green at 9/9, S2 at 16/16, and frozen S1 at 19/19. Full workspace tests and strict all-target/all-feature Clippy are green at acceptance. The frozen branch-mix lighthouse remains outside S3 and requires R1-S4 cross-version summaries plus structural dispatch erasure.

10. Non-claims

R1-S3 does not specialize the frozen branch-mix lighthouse, erase dispatch, establish R1-D or Gate A, emit native code, implement Futamura P1/P2, prove performance leadership, remove Rust/Cargo, or complete Projection Birth or Nauxogenesis.