ADR-0027: R0-C2 Folding and Opaque Evaluation Records

Status: accepted
Date: 2026-07-27
Supersedes: the R0-C1 assumption that request-hash equality alone authenticates an evaluation record

Context

R0-C1 emits verified residual artifacts by substituting scalar facts from an R0-B2 record. Its MixedStaticEvaluation fields are currently public. A caller can therefore clone a legitimate record, replace facts while retaining the same request hash, and ask the residual generator to certify a forged program. Cross-request mismatch checks do not prevent same-request mutation.

R0-C2 must also go beyond scalar substitution:

materialize static Tuple/Sum values
fold static If/Case control
eliminate statically executed calls
prune unreachable functions
admit static Array<F64> only when all runtime uses disappear

Core P1V0 has no array literal, so a static array that remains live cannot be represented honestly in Residual Core.

Options considered

Decision

MixedStaticEvaluation becomes opaque outside its module. Its fields are private and exposed only through read-only accessors. The only constructor remains evaluate_static_r0b2. R0-C1 and R0-C2 accept this opaque record. Independent byte-level record verification remains R0-D scope.

R0-C2 adds a new generator and leaves R0-C1 behavior frozen for regression comparison.

Aggregate materialization

Scalar values use literal Use as before. Tuple and Sum values are rebuilt by a deterministic sequence of fresh Let bindings:

children first, original field order
fresh LocalIds increase from max(entry locals) + 1
parent tuple/constructor last

Scalar children remain literal operands. Aggregate children receive fresh locals. Materialization fails closed on LocalId exhaustion or an ArrayF64 that remains live.

A static array slot is admitted when folding eliminates every read of its parameter. A completely static computation that consumes an array and returns a materializable value can therefore collapse normally. A residual ArrayGetF64, return, call argument, or other live use fails closed because P1V0 has no array literal.

Folding

R0-B2 facts rewrite their unique entry Let binders. Scalar, Tuple, and Sum facts are materialized; Array facts are used only when their binding becomes dead.

An If folds when its condition resolves to a static Bool. A Case folds when its scrutinee resolves to a static Sum; selected pattern fields are materialized into the arm binding locals before its body. Unknown control is preserved and both branches are recursively transformed.

Calls and pruning

A call whose binder has a static fact is replaced by that fact, which eliminates the call without syntactic inlining or code growth. After entry folding, a deterministic call-graph walk from the entry retains only reachable functions in original FunctionId order.

Dynamic calls remain unchanged. R0-C2 does not alpha-rename or inline them.

Admission and output

Every output still passes, in order:

request-record association through the opaque type
residual node budget
canonical byte budget
ordinary Core verifier

The existing ResidualCore provenance fields and size metrics remain unchanged.

Rationale

• Opaque construction closes the immediate same-request forgery path without pretending to be the independent R0-D verifier.
• Aggregate builder lets use existing Core semantics and require no schema or encoding extension.
• Eliminate-or-refuse arrays is honest about the missing P1V0 literal form.
• Call elimination from static facts yields the desired specialized code without inlining growth or new renaming proof obligations.
• Reachability pruning removes obsolete interpreter helpers only after calls are demonstrably absent.

Trade-offs

• External serializers cannot construct R0-B2 records yet.
• Static arrays that remain live still cannot residualize.
• Dynamic-call inlining and cross-function constant propagation are deferred.
• Fresh temporary locals change residual semantic hashes even when behavior is equal.

These costs keep R0-C2 inside the already verified Core schema.

Consequences

Positive: residual artifacts can erase static control/calls and represent nested Tuple/Sum values while rejecting forged records and unrepresentable arrays.

Negative: R0-C2 is still generator-owned evidence. It is not an independently verified residual certificate.

Mitigation: R0-D must canonically encode and independently replay source, request, B0 certificate, evaluation record, transformation correspondence, and residual artifact.

Revisit trigger

Adding an array/static-data literal, general call inlining, changing fresh-ID allocation, accepting serialized evaluation records, or changing pruning roots requires a new ADR and semantic/policy review.