ADR-0034: Canonical Summaries and CoreVM0 Structural Erasure

Status: accepted

Date: 2026-07-28

Extends: ADR-0033 without changing the frozen R1-S1, R1-S2, or R1-S3 policies

Context

R1-S3 admits an exactly bound CoreVM0 package, but the frozen branch-mix lighthouse does not terminate within its partial-value envelope. The one million-node failure is a symptom, not the cause:

the static 64-slot instruction image is traversed and reconstructed in exact version keys;
after a dynamic loop guard, known index and repetition values continue as 0, 1, 2, ...;
exact recursive keys therefore never close, even though program counter and stack pointer range over a finite verified program.

Raising the cap only delays this chain. Caching a concrete helper result is also invalid because its atoms and operands belong to one residual caller. Decoding the bytecode in Rust and directly emitting its CFG would produce a hand-specialized compiler, not specialization of the definitional Core interpreter.

Options considered

Option	Benefit	Cost
Raise S3 hard caps	Minimal code	Delays an unbounded exact-key chain and hides the cause
Cache concrete helper `Partial` values	Reuses some work	Leaks caller-local atoms and operands across residual functions
Decode `CoreVmProgram` and emit Core directly	Easy dispatch removal	Bypasses the definitional interpreter and invalidates the intended evidence
Implement a general learned widening fixed point	Maximum generality	Larger proof and implementation surface than the current lighthouse requires
Add canonical static interning, alias templates, and a bound recursive-state quotient	Finite keys while preserving Core specialization	Deliberately loses static payload precision at recursive boundaries

Decision

Add an append-only R1-S4 policy/API at version 1.3.0.

Canonical shared-static table

Static Tuple/Sum values are canonicalized and interned by their canonical specialization bytes and SHA-256 identity. A hash hit must have identical bytes or the attempt fails closed. Structural children are shared through immutable references.

Version and summary patterns use the static identity, never a host pointer, encounter number, or a recursively copied ProgramImage. Static, summary, and variant tables each receive a separate domain and deterministic table hash.

Pure result summary templates

A pure, acyclic, zero-residual helper result is cached by:

(callee FunctionId, canonical input patterns)

The cached result is a pattern template. Every output hole must refer to an input alias. Replaying the template rebinds those aliases to the current caller’s atoms and operands. Caller-local AtomId, LocalId, Operand, or host references are never stored as reusable output evidence.

Effectful, recursive, dynamically controlled, non-finite, or fresh-dynamic helper attempts are not published as complete summaries. Budget failure aborts the whole attempt; it is never converted into a conservative cache entry.

Request-bound recursive control plan

R1-S4 introduces a canonical control manifest. It names recursive parameters whose static precision must be retained, and its hash is part of the S4 request identity. A pin for a missing parameter or a non-recursive function is rejected.

For the exact CoreVM0 construction version, the wrapper pins loop parameters:

instruction slots = 0
instruction count = 1
program counter   = 2 + argument_count
stack pointer     = 3 + argument_count

The manifest comes from the frozen definitional layout and argument count, not from branch-mix opcode contents.

At every recursive boundary, every unpinned argument is summarized structurally:

Tuple shape is retained;
a known Sum constructor is retained;
scalar/read-array payloads become fresh typed holes;
an existing hole is freshened while passing its current operand;
no two payload aliases are merged merely because their current values agree.

For example:

RuntimeValue::I64(Known 17)
→ RuntimeValue::I64(Hole(current literal 17))

This is a deterministic loss of binding-time precision, not a loss of runtime data. Flattened residual calls pass the exact current literal or operand. P1V0 contains only by-value scalars, immutable structural values, and read-only arrays in this slice, so discarding payload alias equality is not observable.

Keeping image/count/pc/sp static lets the existing Core helper machine select the fetch tree, instruction-slot Case, 16-opcode Case, stack/local helpers, and verified control targets. Generalizing state payloads closes the dynamic loop instead of unrolling it forever.

Bounds

The eight S3 budget dimensions and hard caps remain unchanged:

work units
partial-value nodes
variants
control splits
dynamic parameters
helper unfolds / complete summary entries
residual nodes
residual bytes

No cap is raised. Usage additionally reports shared-static entries, complete summary entries, summary hits, and widened values. These are bound by the existing partial/helper/work caps and sealed as exact evidence.

Structural erasure gate

The CoreVM0 wrapper accepts no S4 residual unless its internal versioned checker proves:

one specialized source entry and at least one specialized source loop;
no variant from fetch, get/set, argument lookup, or trap helpers;
exact residual entry ABI containing only the original dynamic arguments;
instruction image, instruction count, pc, and sp remain static in every loop descriptor;
no ProgramImage, TypeSlot, InstructionSlot, Instruction, RuntimeValue, ValueLookup, BankUpdate, or VM-bank type remains;
no Case dispatch remains;
every direct or tail call targets an admitted entry/loop residual version;
the ordinary Core verifier accepts the artifact.

The checker is not exposed as a source-detached public attestation API. Its separately domain-bound report/hash commits to the trusted definitional construction, interpreter/artifact/program/image identities, residual source/request, every S4 policy/request/control/table identity, and the exact structural metrics.

Independent regenerative replay

Sealed R1-S4 evidence binds construction/interpreter/program/image/source, B0 request/certificate, R0 request, S4 policy/request/control, all three table hashes, exact budget/usage, residual identity/metrics, binding identity, and erasure report/metrics.

The public verifier starts from raw CoreVmProgram, B0 request/certificate, R0 request, S4 budget, claimed residual, and claimed evidence. It rebuilds the definitional artifact, independently regenerates the B0 certificate, validates R0, reruns S4 and the erasure checker, then compares the exact residual and evidence. It does not accept an emitter-owned validated request, summary table, variant table, or residual wrapper.

The claimed residual must first pass the ordinary Core verifier. Exact regeneration compares canonical semantic bytes and the semantic hash rather than derived Rust/IEEE equality, so +0.0 and -0.0 cannot alias and canonical NaN does not reject itself.

Rationale

Append-only S4 preserves every prior locked policy and vector.
Static interning removes representation amplification without changing semantics.
Template summaries reuse pure results without caller-local identity leaks.
The recursive-state quotient fixes the actual infinite known-value chain while retaining exactly the control facts needed for dispatch erasure.
A structural checker prevents a residual hash alone from masquerading as an erasure claim.
Raw-input replay turns one successful run into reproducible, mutation- resistant evidence.

Trade-offs and consequences

Positive:

the frozen 62-instruction, all-16-opcode branch-mix package specializes under the unchanged hard caps;
fetch, opcode dispatch, generic helpers, trap, VM types, and dynamic pc/sp disappear from verified Residual Core;
dynamic loops remain loops over residual payload parameters rather than being statically unrolled;
table, binding, erasure, and evidence identities are reproducible.

Negative:

the control manifest currently knows the exact CoreVM0 definitional layout;
recursive payload constants are residualized earlier than a general least-fixed-point join might require;
regenerative replay uses the same Rust seed implementation and is not an implementation-diverse proof;
121 residual entry/loop versions remain before later SSA joining.

The simpler quotient is accepted because it is deterministic, sound for the admitted immutable P1V0 slice, sufficient for the lighthouse, and materially smaller than a general widening framework. A future general fixed point must be a new append-only decision.

Acceptance evidence

The focused five-test corpus covers the frozen branch-mix specialization and source/residual differential cases, the four-opcode Bounds package, exact and one-below budgets, zero/hard-cap rejection, invalid control manifests, independent replay, every sealed-evidence field class, resealed identity mutation, stale-hash signed-zero residual substitution, and same-shape program substitution.

Generic vector:

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 vector:

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

Non-claims

R1-S4 is not residual SSA, standalone/native output, Gate B/C, a performance result, Futamura P1/P2, full node-origin R1-D, an implementation-diverse proof, Projection Birth, dependency closure, Rust/Cargo removal, or Nauxogenesis.