ADR-0032: Structural Partial Values and Bounded Helper Unfolding

Status: accepted

Date: 2026-07-28

Extends: ADR-0031 without changing the frozen R1-S1 policy

Context

ADR-0031 defines the full R1 direction and proves its first pure-scalar control slice through R1-S1. The next slice must retain known Tuple fields and known Sum constructors beside dynamic payloads. It must also transport those facts through helper calls without erasing effects, divergence, alias distinctions, or budget failure.

Changing the existing PolyvariantR1Pattern, its key encoding, or its budget meaning would invalidate the locked S1 identity. Structural normalization, hole aliasing, signature flattening, helper eligibility, and structural-event work accounting are policy decisions in their own right.

The temporary upstream ValidatedSpecializationRequest can express only a whole static or whole dynamic entry slot. Structural partial values can still arise inside specialization from Tuple construction, Sum construction, projection, Case binding, and calls. A dedicated raw R1-A request remains later work.

Options considered

Decision

Add a separate R1-S2 policy, request identity, public API, budget, usage report, pattern vocabulary, and canonical version-key domain. R1-S1 remains byte-for-byte and behaviorally frozen.

Structural domain and normalization

R1-S2 admits recursively pure:

Unit | Bool | I64 | F64 | Tuple | Sum

Its internal domain is:

PartialValue =
    Known(canonical static value)
  | Hole(Type, Atom, ResidualOperand)
  | Tuple([PartialValue])
  | KnownSum(SumType, constructor, [PartialValue])
  | UnknownSum(SumType, Atom, ResidualOperand)

A Tuple whose fields are all known normalizes to one Known Tuple. A KnownSum whose fields are all known normalizes to one Known Sum. An opaque Sum always normalizes to UnknownSum, never a generic Sum-typed hole. Constructor arity, field types, projection indexes, and every reconstructed type are checked or inherited from already verified Core.

Static F64 identity uses the Core canonical NaN class while preserving signed zero. Arrays, references, regions, closures, handlers, effects, Text, Bytes, and non-P1V0 profiles remain outside S2.

Atoms, aliases, and residual signatures

An atom identity denotes a typed equality class. Each partial-value occurrence also carries the residual operand valid at its current scope. Repeated projections of the same opaque Tuple field and fields derived from one UnknownSum constructor preserve their derived atom identity even when Case scope gives an equal field a different local operand. Different atoms never merge merely because their types match.

When one equality class reaches a flattened call more than once, the first left-to-right operand is passed once. This is sound only for S2’s immutable, pure Tuple/Sum domain and is policy-bound; admitting mutation, effects, or identity-observable aggregates must revisit the rule.

Version keys alpha-number distinct atoms in first-occurrence order while walking ordered parameters and structural children left to right:

(x, x) -> Tuple[Hole(0), Hole(0)]
(x, y) -> Tuple[Hole(0), Hole(1)]

Transient LocalId, atom allocation order, and host addresses are not key material. One residual parameter is emitted per distinct alias, in alias order. Static fields and known constructors are omitted. Residual calls pass one operand per alias in the same order.

Residual parameter and materialization locals are allocated deterministically above every source local in that function version. Local exhaustion rejects the whole specialization.

Structural specialization

Tuple and Sum constructors remain partial values until an ordinary Core operand is required. Projection over a structural Tuple transports the chosen child. Projection over an opaque Tuple emits one residual Project and produces a derived typed atom.

A KnownSum, including a partially known payload, selects exactly its proven Case arm and binds its partial children without executing a dynamic payload. An UnknownSum emits the complete canonical Case and specializes every arm; each arm receives typed derived field atoms. Unknown control never invents a constructor or payload.

Returning a partial aggregate materializes children before parents in left-to-right Core order. Unused partial structures allocate nothing.

Bounded helper result propagation

S2 may erase a direct helper call only when a deterministic symbolic unfolding proves all of the following:

• the helper and every transitively unfolded helper are pure and outside a recursive call-graph component;
• the unfolded path is finite and contains only admitted zero-residual structural/scalar work;
• every dynamic value in the result is an existing typed caller atom;
• no residual primitive, branch, Case, call, tail call, or other work is discarded.

The initial S2 helper grammar is deliberately narrow: Let* -> Return using Use, Tuple construction, projection over structural values, Sum construction, all-known scalar primitives, and calls to another eligible helper. Unfolding runs on an explicit frame machine rather than the Rust call stack, and a helper chain is capped at 256 entries. Any other helper remains an ordinary residual version call and its result becomes an opaque hole or UnknownSum.

This restriction prevents a known-looking summary from erasing divergence. The fixed depth boundary is eligibility: once 256 frames are active, the next helper entry is ineligible and its call is conservatively preserved. Budget exhaustion never changes eligibility or silently falls back: it rejects the entire S2 attempt.

Budgets and fail-closed behavior

PolyvariantR1S2Budget independently declares:

max_work_units
max_partial_value_nodes
max_variants
max_control_splits
max_dynamic_parameters
max_helper_unfolds
max_residual_nodes
max_residual_bytes

Usage mirrors every specialization counter. work_units meter normative source/type/operand admission visits, call-graph nodes and edges, per-version local scans, partial normalization nodes, pattern/type visits at reservation/build/lowering, helper-shape and abstract-evaluation visits, materialization nodes, and residual target-rewrite nodes. It is deterministic machine-work evidence, not wall-clock time.

Canonical name-byte copying, ordered-map/tree comparisons, residual encoding, and ordinary verification are not individual work units; their input sizes are bounded by the verified source, partial/key visits, version cap, and residual node/byte caps. partial_value_nodes counts cumulative normalized node construction. control_splits counts one for dynamic If and arms - 1 for UnknownSum Case. dynamic_parameters counts distinct flattened aliases across versions. helper_unfolds counts attempted eligible helper entries, whether they ultimately succeed or conservatively refuse.

S2 owns residual node and byte caps but also respects the tighter temporary upstream envelope. Zero, hard-cap overflow, counter overflow, exhaustion, unsupported structure, unresolved variants, invalid materialization, identity failure, or verifier rejection returns no partial result.

Deterministic residual

Version discovery retains the pending-key worklist from S1. Final FunctionIds are assigned by sorting canonical S2 key bytes, and every temporary call target is remapped through that table. The result is ordinary Core and must pass the ordinary verifier before its opaque report is exposed.

R1-S2 does not produce portable R1-D evidence or an origin/erasure certificate.

Rationale

1. A separate policy preserves all locked S1 vectors.
2. Structural normalization retains exactly the facts required by the definitional interpreter without treating dynamic payloads as static.
3. Alpha-numbered aliases make version identity independent of transient locals while preserving equality relationships.
4. Zero-residual acyclic helper unfolding propagates useful results without erasing effects or divergence.
5. Independent work, partial-value, graph, helper, and output caps make aggregate growth explicit and fail-closed.

Trade-offs

• S2 duplicates part of the S1 version machine instead of mutating it.
• Whole-dynamic entry aggregates remain limited by the temporary R0-A envelope; a native R1-A request is still required.
• The first helper grammar refuses many safe programs rather than speculate.
• Flattened signatures can increase parameter counts for highly structural arguments.
• Cumulative accounting and regenerative work cost more than an unmetered optimizer.

These costs are accepted to preserve identity, termination, and auditability.

Consequences

Positive:

• Tuple fields and Sum tags can survive dynamic payloads and calls;
• alias-sensitive versions become deterministic and testable;
• helper result propagation has an explicit divergence-safe boundary;
• CoreVM0 can be approached without changing S1 or hand-translating bytecode.

Negative:

• CoreVM0, arrays, effect preservation, R1-D replay, and dispatch erasure remain closed;
• S2 has a larger API, policy, and test surface;
• the Rust seed still traverses verified term trees structurally.

Acceptance evidence

The accepted implementation is exposed through core::specialize_polyvariant_r1_s2 under policy version 1.1.0. The focused 16-test corpus covers structural Tuple/Sum behavior, alias flattening, known-result helper propagation and conservative refusal, recursive aggregate versions, the exact 256/+1 helper boundary, LocalId exhaustion, admission rejection, all eight zero/hard-cap and exact/one-below budget boundaries, ordinary Core verification, and bounded differential evaluation.

The locked stability vector is:

policy   034ef346e4b036b8860e196fdb065c3b99ae024809d497a97ebccc66eb5c55f1
request  9a1707f75a3bb4d1f2d0bfea38b62999248b2e549c24f9f90886bda773c0f1f9
residual d617aa9405c91b494a71b9fe533b05ec0c364774e1b766b14b9295e57c27353e

usage work=254 partial=15 variants=2 control=2 dynamic=6 helper=2
residual nodes=23 bytes=549

The frozen R1-S1 corpus remains 19/19 with its existing vector unchanged. cargo test --workspace, strict all-target/all-feature Clippy, formatting, and whitespace audits are acceptance gates for this decision.

Non-claims

This decision does not specialize CoreVM0, admit arrays or effects, erase fetch/opcode dispatch, provide independent R1 evidence, emit native code, establish Futamura P1/P2, remove Rust/Cargo, close dependency debt, prove performance leadership, complete Projection Birth, or complete Nauxogenesis.

Revisit trigger

Changing structural normalization, atom derivation, alias numbering, signature flattening, helper eligibility, any budget meaning, key ordering, or residual-cap authority requires a new policy version and a superseding ADR.