Interpreter: a match over an optional sees the present value where the checker says so, for constructed optionals too

[gunbai-bot]

Fixes an interpreter/inference divergence found by wise-hawk-615 on #12261. It also consolidates into one authority the decision of which arms of a match over an optional see the present value (requested in GitHub review 5314402835).

Defect. Inference types a bare binding after an unguarded null/Absent arm as the payload, and a literal arm matches only a present value. The interpreter holds an optional in two representations:

• a bare value, when a host builtin such as first produced it;
• an Optional.Present variant, when source wrote Present { value }.

v1.compiler.interpreter eval_match passed the scrutinee to match_pattern unchanged. So over a constructed optional, match o { null => "n" "x" => "ex" v => v } missed the literal arm and bound v to the whole variant. Over Int?, v + 1 refused with cannot apply Add to Variant and Int.

One authority (§3). Which arms see the present value was decided in more than one place:

• the checker owned only the binding case, optional_scrutinee_binding_is_present;
• the literal case was decided locally in v1.compiler.emit_rust's String-literal re-emission (sf_scrut_optional && is_string_lit_pattern(..));
• the first cut of this PR decided it a third time in the interpreter, with a matches!(.. LitPattern ..).

This PR replaces all of them with ONE predicate, v1.compiler.infer optional_match_arm_sees_present_value(scrutinee_type, arm_pattern, arm_index, absent_arm_index). It is true for (1) a bare binding after an unguarded Absent arm, and (2) a non-null literal arm, over a CardOptional scrutinee. It is read by:

• the checker's own ExprMatch typing;
• emit_rust's ordinary match (emit_typed_match_arm_strs);
• the TCO match (emit_rust_tco_match);
• the String-literal re-emission (emit_typed_match, needs_string_from);
• the interpreter's eval_match.

optional_scrutinee_binding_is_present, the emitter's sf_scrut_optional term and the interpreter's local literal check are all deleted. The interpreter decides nothing itself. It only reaches the payload of either representation (optional_present_payload) in the arms the predicate names.

Consequence for emission: a non-String literal arm over an optional is now emitted Some(7) =>. Before, it was a bare 7 => against an Option<i64>, which the literal rule never reached because only the String re-emission applied it. The grouped (no-irrefutable-arm) rendering still passes false. A literal arm is never exhaustive by itself, so an accepted match with a literal arm always has an irrefutable arm and takes the ordinary path.

Evidence (local, gen-2 binary; sha256 values are in the comments below):

• test.claim.interpreter_constructed_present_match_witness_test:
  • 4 interpreted claims. Each pairs a constructed optional with the same match over a builtin-produced one as the positive control. On main, 3 are red.
  • 2 emitted claims (Some(7) / Some(ref __s) / Some(v)).
  • All 6 PASS.
• Rust emitter: String ordering via the host text carrier, present-binding arms, bytes_octets/utf8_encode_bytes as realized seams (native App Attest) #12261's test.claim.emitter_string_order_present_binding_witness_test: 5/5 PASS.
• Coupled-movement control: results for mutating the one predicate are in the comments below.
• --required-regen: gen 1 drifted exactly v1_compiler_emit_rust.rs and v1_compiler_infer.rs, which are installed. The gen-2 fixed-point result is in the comments below.

Population. A static scan finds 67 bind-after-absent arms and 11 literal-after-absent arms across 24 files. A local diff of an old and a new binary over 18 optional/serialize/match claim modules changed only this PR's claims.

Receipt: gunbc.recurring_failure_mode realization_arms_diverge_on_whether_the_program_refuses. Not climbed: an optional still has two runtime representations, which is the deeper link.

v1 seed purpose (v1_seed_standing): interpreter correctness for v2, since the interpreter is the oracle for the emitted-parity fixtures. The hand-written seed Rust is eval_match plus optional_present_payload, about 50 lines, which read the checker's predicate.

🤖 Generated with Claude Code

[gunbai-bot]

On review 71167's one substantive remark (the literal-arm rule is a local matches!, not a checker read): agreed, and there is no checker predicate to read for it on main. #12261's emitter decides the same rule locally too (sf_scrut_optional && is_string_lit_pattern). The right repair is one v1.compiler.infer predicate for "this arm sees the present value", covering both the binding and the literal case, which the interpreter and all three Rust renderings would then read. That touches #12261's emitter code, so I'm leaving it as a follow-up once #12261 lands rather than forking it here.

— sent from bold-boar-418

[gunbai-bot]

Evidence at head fc6be23:

• CI floor: it evaluated the claims (phases_failed=0), and all 4 of test.claim.interpreter_constructed_present_match_witness_test are planned-and-passed. The floor runs only diff-touched claims, so this is not a corpus census.
• Local old/new binary diff over 18 claim modules matching optional, present, serialize or match: the only verdict changes are this PR's claim (3 red → PASS). Everything else is identical: 137 PASS, and 1 FAIL present in both binaries.

— sent from bold-boar-418

[briansrls]

SOURCE HOLD at exact head fc6be23c0a02bd0138a3317d130e7eca8c698991.

The interpreter defect and the four-cell RED are accepted. On the old eval_match, the two constructed-String cells fail because the literal sees Optional.Present and the fallback binds that whole variant; the constructed-Int cell refuses at Variant + Int; the absent control stays green. On this head, optional_present_payload makes all four pass while the builtin-produced controls prove the match itself was already sound.

Two landing walls remain.

1. The present-value decision is still forked for literal arms.

The PR/body/receipt say the interpreter reads the same checker decision without re-deriving it. That is true only for the bind-after-unguarded-absent case. eval_match independently decides the literal case with:

matches!(&*pattern, MatchPattern::LitPattern { value }
    if !matches!(&**value, LiteralValue::LitNull))

#12261 independently makes the corresponding emitter decision with sf_scrut_optional && is_string_lit_pattern. The PR discussion already acknowledges that no shared checker predicate exists and proposes a follow-up. That cannot remain a follow-up on a PR whose purpose and durable RFM receipt are that independently realized match arms consult one authority: the exact class being repaired is left with two locally restated rules.

After #12261 lands, introduce one v1.compiler.infer projection answering whether an optional match arm sees the present payload, covering both (a) the narrowed binding arm and (b) a non-null literal arm. Have eval_match and all three Rust match renderings consume that projection. Remove the local matches! and emitter-side literal test, then correct the receipt’s “same predicate/no re-derivation” statement to be literally true.

2. The requested population and three-route agreement are not established at this exact head.

The body gives a syntactic upper bound—67 bind-after-absent arms plus 11 literal-after-absent arms across 24 files—but posts neither the promised identity/location roster nor the base/head floor-verdict join. More importantly, those 78 sites are not the behavior-change population: behavior changes only when the runtime producer supplies the authored Optional.Present representation. A green changed-file floor does not establish that every affected site executed.

Publish either a producer-joined affected-site census, or explicitly label the 78-site scan as an upper bound and execute the complete 24-file population on base and head with a joined verdict report. The current four-cell repro remains the discriminating local RED.

Likewise, this head contains only the interpreter repair; #12261 is still a separate open PR. Its emitter claim checks emitted shape, while its execution fixture deliberately uses builtin first, not constructed Present. Therefore interpreted == inferred == emitted for the constructed repro is not yet an executing receipt. Once restacked after #12261, run one emitted/interpreted parity fixture over constructed String? and Int? values, covering literal, narrowed binding, and absent arms. Compilation establishes the inferred side; equal execution establishes both realizations.

All five CI jobs are green at this SHA, so this is a source/evidence hold only. No objection remains to optional_present_payload, the existing four claim cells, or the RFM placement once the authority and population gaps above are closed.

[gunbai-bot]

Evidence at head 102288c (#12261 merged in; consolidation folded into this PR):

Gen-2 binary (gunbc sha256 95cc9621…, claim_executor c04bd0c2…):

• test.claim.interpreter_constructed_present_match_witness_test 6/6 PASS (4 interpreted, 2 emitted).
• Rust emitter: String ordering via the host text carrier, present-binding arms, bytes_octets/utf8_encode_bytes as realized seams (native App Attest) #12261's test.claim.emitter_string_order_present_binding_witness_test 5/5 PASS.

Regen:

• Gen 1 drifted exactly v1_compiler_emit_rust.rs and v1_compiler_infer.rs, which are installed.
• Gen 2 --required-regen: first_generation_equal=true, 161/161 adjudicated, and cmp of every candidate file against the committed mirrors shows no byte difference.

Coupled-movement control, executed. Mutation: the literal case of optional_match_arm_sees_present_value set to false, in the .dag and its mirror. Binary sha256 e09f8760…; the tree was restored after the build.

• Interpreted: literal_arm_matches_a_constructed_present_string FAIL, literal_and_binding_arms_see_a_constructed_present_int FAIL.
• Emitted: emitted_..._optional_int_... FAIL, emitted_..._optional_string_... FAIL, and Rust emitter: String ordering via the host text carrier, present-binding arms, bytes_octets/utf8_encode_bytes as realized seams (native App Attest) #12261's present_binding_in_the_string_literal_reemission FAIL.
• Unmutated half stays green: binding_arm_binds_the_payload..., absent_arm_still_takes..., and the ordinary and tail-call binding claims PASS.

So one edit to the one authority moves the interpreter and all the emitted renderings together, and only on the case it changed.

— sent from bold-boar-418

[gunbai-bot]

Review 71313, fixed in 30d481c:

1. Untyped scrutinee. Agreed, that was a silent fallback. The decision only matters when the runtime value is an Optional variant. With a bare value every arm sees the same value either way, so arm selection can't differ. That case now refuses with a located TypeError naming the match span and the predicate it couldn't read. An untyped scrutinee holding a bare value is unaffected. I did not make every untyped match refuse, because I have no evidence that all interpreted match nodes carry inferred, and refusing there would break paths where the decision is immaterial.
2. Malformed Optional.Present. optional_present_payload now returns InterpResult and refuses a Present without its value field, rather than reading it as absent.
3. Seed purpose receipt. It's in the PR body's v1 seed purpose paragraph (v1_seed_standing): interpreter correctness for v2, because the interpreter is the oracle the emitted-parity fixtures compare against. The growth is eval_match's read of the checker predicate plus payload access for the two representations.

Verification (gunbc sha256 22300243…): I ran 20 claim modules (the 18 optional/serialize/match modules plus both present-binding modules) under this binary and under the previous head's binary. The verdicts are identical: 150 PASS, and 1 pre-existing FAIL (optional_consumer_fail_closed_test required_param_optional_arg_emits_located_fail_closed_unwrap, red on every binary I've run including the pre-PR one). So the new refusal doesn't fire anywhere in that population.

— sent from bold-boar-418

[briansrls]

APPROVE-MERGE — exact current head 30d481c.

Rechecked the seven-file delta. optional_match_arm_sees_present_value is the one decision read by ExprMatch inference, ordinary Rust arms, TCO arms, String-literal re-emission, and eval_match; the prior binding-only helper and both local literal decisions are removed. The source and generated mirrors agree. optional_present_payload only realizes the selected projection for the interpreter's two representations; it does not choose which arms narrow.

The two requested refusal boundaries are present: an Optional variant scrutinee without inferred type produces a located TypeError instead of silently skipping the predicate, and a Present without its value field returns an error rather than absence. The witnesses distinguish constructed optionals from builtin-produced values and include the emitted Some(7), Some(v), and guarded Some(ref __s) forms. The deeper dual-representation debt remains explicitly stated rather than claimed retired.

Exact-head workflow 36169983407 is completed/success. I inspected the witness sources and carried coupled-movement evidence but did not rerun those mutations in this environment. No source blocker remains from the earlier hold. Merge through the queue with required checks; this approval is only for the named SHA.