GitHub

Polyvariant R1-S4 Contract

Status: implemented, structurally erased, and independently replayed

Stage: Roadmap Stage 3 / frozen CoreVM0 branch-mix Residual-Core slice

Decision: ADR-0034

1. Purpose

R1-S4 specializes the frozen CoreVM0 branch-mix lighthouse far enough that the verified Residual Core contains program behavior but no bytecode fetch, opcode dispatch, generic CoreVM helper, trap fallback, VM type, or dynamic program counter.

It is append-only. S1, S2, and S3 APIs, identities, and evidence remain unchanged.

2. APIs and identities

specialize_polyvariant_r1_s4(validated, budget)
specialize_polyvariant_r1_s4_with_control(validated, budget, control)
specialize_corevm0_r1_s4(bound, validated, budget)
emit_corevm0_r1_s4_evidence(specialization)
verify_corevm0_r1_s4_evidence(
  raw_program,
  binding_time_request,
  binding_time_certificate,
  specialization_request,
  budget,
  claimed_residual,
  evidence
)

The CoreVM wrapper invokes the structural erasure checker internally. There is no standalone public erasure-attestation function detached from the bound CoreVM construction.

Generic policy version is 1.3.0. Generic policy, request, control, version key, shared-static table, pure-summary table, variant table, CoreVM binding, erasure report, and sealed evidence have separate domains.

3. Admission inherited from S3

  • P1V0 only;
  • recursively Unit/Bool/I64/F64/Tuple/Sum and dynamic read-only Array<F64, RegionId(0)>;
  • region parameters exactly [] or [RegionId(0)];
  • effect row exactly empty or canonical [Error(Bounds)];
  • static arrays rejected recursively;
  • ArrayLen/Get always residual;
  • at most two recursive SCCs;
  • only empty-effect, acyclic helpers may unfold;
  • all successful outputs pass the ordinary Core verifier.

4. Shared-static semantics

Every aggregate static value is canonicalized and interned. Identity is SHA-256 over canonical specialization bytes. A same-hash/different-bytes collision rejects the attempt.

Patterns contain SharedStatic(hash) rather than a copied aggregate. A projection or known Sum Case follows immutable shared children. Static table identity binds exact sorted hashes and canonical bytes.

5. Pure cross-version summaries

A complete helper summary is keyed by callee and canonical input patterns. The result is an alias-parameterized pattern template. Replaying it instantiates holes with the current caller’s atoms and operands.

A result with a fresh output alias is not published. Effectful, recursive, dynamic-control, tail-calling, region/handler, or otherwise non-finite helpers remain ordinary residual calls. Complete entries are bounded by max_helper_unfolds; all lookup/replay work is charged to work/partial usage.

6. Recursive state quotient

PolyvariantR1S4Control canonically binds pinned recursive parameters. Pins must name an existing parameter of a reachable recursive function.

At a recursive call:

  • pinned arguments retain their exact partial value;
  • every other Tuple is traversed pointwise;
  • known Sum tags remain known;
  • every scalar/read-array payload or prior hole is rebound to a fresh hole carrying the exact current literal/operand;
  • distinct payload locations never acquire a new shared alias.

The CoreVM wrapper pins instruction slots, instruction count, pc, and sp from the exact definitional construction layout. This produces finite version families while retaining the control facts that erase fetch and dispatch.

7. Budgets

R1-S4 retains the exact eight S3 dimensions and hard caps. No cap is raised. Exact usage passes; one-below, zero, and hard-cap overflow fail closed.

Additional sealed usage counters are:

static_interns
summary_entries
summary_hits
widened_values

They are governed by the existing partial/helper/work caps.

8. CoreVM0 structural erasure

An accepted wrapper result must satisfy all of:

  • exactly one source-entry variant and one or more source-loop variants;
  • only source functions 0 and 1 occur in the variant table;
  • residual entry parameters equal the original dynamic CoreVM arguments;
  • instruction image/count and pc/sp patterns are static in every loop variant;
  • no ProgramImage, TypeSlot, InstructionSlot, Instruction, RuntimeValue, ValueLookup, BankUpdate, or VM-bank type;
  • no Case;
  • no direct/tail target outside residual entry/loop variants;
  • ordinary Core verification.

The checker report binds exact residual function, loop-variant, structural node, direct-call, tail-call, and If counts. Its hash also binds the definitional construction, interpreter/artifact/program/image identities, residual source/request, and every S4 policy/request/control/table identity.

9. Independent evidence replay

Evidence binds:

construction, interpreter, artifact, program, image
B0 request and certificate
R0 request
S4 policy, request, control
static, summary, and variant tables
exact budget and usage
residual hash/nodes/bytes
CoreVM binding
erasure version/hash/metrics
evidence version and replay version

The raw verifier rebuilds the CoreVM package and B0 certificate, validates R0, reruns S4 and erasure, and compares exact residual and evidence. An invalid evidence hash fails before replay. Recomputed hashes do not authorize a forged identity: exact raw-input regeneration must still match.

The claimed residual first passes the ordinary verifier. Equality with the regenerated residual is canonical semantic-byte equality plus exact semantic hash equality, never Rust/IEEE PartialEq; signed zero remains distinct and canonical NaN remains replayable.

This is regenerative validation through the same semantic kernel, not an implementation-diverse proof or full node-origin R1-D certificate.

10. Required evidence

  • frozen 62-instruction branch-mix uses every CoreVM0 opcode and specializes under unchanged caps;
  • source/residual parity for empty, negative/zero repetition, signed zero, NaN, infinity-capable numeric semantics, and multi-iteration cases;
  • four-opcode in-bounds/out-of-bounds Bounds parity and effect order;
  • structural erasure gate;
  • exact/one-below and zero/hard-cap tests for all eight budgets;
  • invalid control pins rejected;
  • raw-input replay;
  • mutation of every evidence field class rejected;
  • stale-hash signed-zero residual substitution rejected before IEEE equality;
  • resealed identity mutation and same-shape program substitution rejected;
  • locked generic and branch-mix vectors;
  • frozen S1/S2/S3 focused suites unchanged;
  • full workspace, strict Clippy, format, whitespace, and Markdown-link gates.

11. Locked vectors

Generic:

policy   d5320ad01a9ed44762575f7c44c0dc5d5b567f0b2b411bdece40ec864673e8ad
request  84562d7a59ce990d954dc0e429957e237f8f380fbf1efd6f919624dbb4bb9ac4
static   d4c22acdc02cdb4d5cd82b62b67fd42deef21c35fd8357a7aec21b7762abc4a6
summary  85be896774885a54795223cb40bed0388f251d20680bc5aa45ef8ec3d95a80df
variants 057cd1b777340c9a4258703c916643c5ab2b61f9db1df6f5ad295269c0280c6c
residual 72918bb40a2868a86a6df5a98d1518cf7141d9afb91d7b5e90fb84697bee3575
usage    work=119 partial=8 variants=1 control=1 dynamic=3 helper=1
output   nodes=14 bytes=157

Frozen branch-mix:

program  9770cd0fb20fefaebba063674e02b1881173a817b73b9f910c9ba8e025a9b2d5
image    732cc709778d757988b34b1efcf5c376b1b1443e6cebec3bb61375d1f8fa1142
policy   d5320ad01a9ed44762575f7c44c0dc5d5b567f0b2b411bdece40ec864673e8ad
request  e73aa7869e45df9a364eb3a9b985f9b2a2f32fc984aa2c8f65f0c0c4549944dd
control  f98faa10987f044206e09b271de2e97654d9a1b58d914c12593b8016f12bc92a
static   47241ddfe7888c870518a0e07b0738218ec8060ce77550f652909249c9410956
summary  6f99ab66dd2c84d30b903747e022b8297e479af58ef033ca8206deb881c379d0
variants 195fcb9713e6f11675bfe681ff791da9e61806ed66e596784010c8320213a476
residual fd90f6b16813a851aea7b1151a2df9ad87f9a9bfb8e994a5797407700f9fb2e9
binding  49e9cdf6620f0997c0ae62bedac481509bfc5229c045753a9384ec62005a2d2c
erasure  a100096fbfc49ccb367d9f5207f8f9fcff64205b7d64d32c98ec3621bccb4176
evidence 8d648c021a3c806d76790e49ae8655ee59f2e97427800827db91577c90d64896
usage    work=234073 partial=8227 variants=121 control=9 dynamic=1085
         helper=134 static=93 summaries=134 hits=199 widened=1151
output   nodes=1391 bytes=16575
scan     functions=121 loop_variants=120 nodes=185 calls=0 tail=127 if=9

12. Exit and successor

R1-S4 is complete when every required gate is green and S1-S3 vectors remain unchanged. Its successor is the separately decided R1-S5 Residual-Core Gate A and residual SSA handoff.

R1-S5 now validates the fixed finite source-to-residual correspondence at the Stage 3 lighthouse boundary and defines the ordinary verified Residual Core to NAUX-owned SSA transition under ADR-0035. Native output and performance remain later gates.

13. Non-claims

R1-S4 does not emit SSA or native code, produce a standalone artifact, pass Gate B/C, establish a performance result or Futamura P1/P2, provide full node-origin R1-D or a theorem, remove Rust/Cargo, or complete Projection Birth or Nauxogenesis.