ADR-0033: Bounds-Preserving Arrays and CoreVM0 Admission

Status: accepted

Date: 2026-07-28

Extends: ADR-0032 without changing the frozen R1-S1 or R1-S2 policies

Context

R1-S2 retains pure Tuple/Sum structure and propagates zero-residual helper results, but rejects every array, region parameter, and effect. The definitional CoreVM0 lighthouse artifact has a static full ProgramImage, dynamic read-only Array<F64> input, one declared array region, and the typed Error<Bounds> effect. It also has two recursive call-graph components: the execution loop and the non-returning trap.

Admitting this artifact by weakening R1-S2 would invalidate its locked policy. Treating ArrayGetF64 as a pure static operation could erase a Bounds outcome. Using only the generic definitional artifact hash would also fail to identify the bytecode: artifacts with the same argument shape intentionally share that hash.

Options considered

Option	Benefit	Cost
Mutate R1-S2 admission	Least new code	Invalidates the accepted S2 identity
Admit every Core array/effect	Broad surface	Opens mutation, allocation, region, and handler semantics at once
Fold known array operations	More static work	Requires residual array literals and typed-error specialization semantics
Use only the generic artifact hash	Simple wrapper	Does not bind the concrete CoreVM0 program
Add an append-only S3 policy and bound CoreVM0 package	Preserves prior evidence and binds the real program	Duplicates bounded machinery and deliberately retains dispatch

Decision

Add a separate R1-S3 policy/API at version 1.2.0.

Admitted language slice

R1-S3 admits P1V0 and recursively:

Unit | Bool | I64 | F64 | Tuple | Sum | Read Array<F64, RegionId(0)>

A reachable function has either no region parameters or exactly [RegionId(0)]. Its effect row is either empty or exactly canonical [Error(Bounds)]. Text, Bytes, mutable arrays, arrays of other elements, references, allocation/state, checked-overflow effects, handlers, operations, IO, FFI, unsafe memory, closures, and general regions remain rejected.

Static ArrayF64 specialization values, including arrays nested in a static Tuple/Sum, remain rejected. A dynamic read-only array is one opaque typed atom and one flattened residual parameter.

Static entry Tuple/Sum values are structuralized once into shared partial children rather than repeatedly cloning one monolithic known aggregate.

Array and effect semantics

ArrayLenF64 and ArrayGetF64 always remain ordinary residual primitives. The specializer never reads a host array and never evaluates an array index. In particular, it never erases, manufactures, or reorders a Bounds outcome. Every residual version copies the source function’s exact region parameters and effect row.

Helper result propagation remains limited to empty-effect helpers. S3 extends the helper frame machine through If and Case only when the condition or constructor is already known; dynamic control conservatively preserves the call. A helper with Error(Bounds) is always an ordinary residual call.

Recursion and bounds

R1-S3 admits at most two reachable recursive call-graph components. Every member is helper-ineligible, and exact version keys close recursion through the existing explicit worklist. A third component rejects the entire attempt.

The eight R1-S2 resource dimensions remain independently request-bound: structural-event work, partial-value nodes, variants, control splits, dynamic parameters, helper unfolds, residual nodes, and residual bytes. Array/effect nodes are already charged by structural work and output bounds, so S3 adds no redundant counter.

Concrete CoreVM0 binding

A dedicated CoreVM0 S3 wrapper accepts an opaque DefinitionalCoreVmArtifact plus the validated R0-A envelope. It verifies:

exact definitional artifact identity;
exact static full ProgramImage entry slot;
exact dynamic entry types for the package’s declared argument shape;
the package’s CoreVM0 program hash and full-image hash;
Core interpreter-semantics identity and construction version;
the ordinary S3 policy/request and upstream request identities.

The wrapper report exposes those identities beside the S3 residual report. This is a bounded admission/parity boundary. It does not claim fetch or opcode dispatch erasure.

Rationale

An append-only policy preserves every S1/S2 stability vector.
Opaque dynamic arrays require no literal representation or host reads.
Residualizing both array primitives makes Bounds preservation direct and auditable.
Two recursive components are the smallest graph widening that admits the current definitional CoreVM0.
Binding the opaque package identities prevents one program from borrowing another program’s generic artifact evidence.

Trade-offs and consequences

Positive:

the real CoreVM0 package can cross the R1 boundary;
array Bounds behavior remains observable in ordinary verified Residual Core;
region/effect signatures are preserved rather than reconstructed;
prior R1 policies remain frozen.

Negative:

fetch and opcode dispatch remain in the residual;
static arrays and even safe static array reads are refused;
only RegionId(0) and Error(Bounds) are admitted;
the Rust seed still builds and verifies the artifact.

These restrictions are accepted so that the first effectful R1 slice is small, deterministic, and fail-closed.

Acceptance evidence

The accepted nine-test corpus covers ArrayLen/Get residualization, in/out of bounds outcomes and effect order, exact region/effect preservation, pure known-control helper unfolding, dynamic/effectful helper refusal, two/three recursive-component boundaries, admission rejection, all eight budget boundaries, and a concrete four-opcode CoreVM0 Bounds package plus same-shape ProgramImage substitution rejection.

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

R1-S1 remains green at 19/19 and R1-S2 at 16/16 with their locked vectors unchanged. Full workspace tests and strict all-target/all-feature Clippy are green.

The frozen branch_mix_kernel is intentionally not an S3 success claim. Without cross-version summaries and complete dispatch erasure it exceeds the S3 partial-value envelope. That optimization/evidence boundary is R1-S4; S3 does not raise a cap to conceal the expansion.

Non-claims

R1-S3 is not frozen-branch-mix specialization, independent R1-D evidence, dispatch erasure, Residual-Core Gate A, standalone/native output, Futamura P1/P2, performance leadership, Projection Birth, dependency closure, Rust/Cargo removal, or Nauxogenesis.