Skip to content

XL-2 carrier: record #12173/#12194/#12221 - #12237

Merged
briansrls merged 5 commits into
mainfrom
session/royal-gull-472
Sep 25, 2026
Merged

briansrls merged 5 commits into
mainfrom
session/royal-gull-472

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 24, 2026 •

Copy link
Copy Markdown
Contributor

XL-2 carrier update (gunbc.compiler_frontend_program_status), its witness, and the RFM rewrite. Every standing cites a merge SHA.

Delivered (10 of 18)

New outstanding arms (8 of 18 are outstanding in total)

  • Lambda argument, caret symbol, as-cast and else-less if. Each is tracked by XL-2 follow-up to #12173: match-scrutinee controls, list/lambda RFM rows (three-baseline identity census posted as a PR comment) #12194's RFM row.
  • WildcardMatchArmResolution, tracked by a_wildcard_match_arm_resolves_as_an_unbound_name. My judgment: it does not drop references. It is a loud refusal, and ResolveOccurrenceCompleteness carries the independent refusals through. But it puts rows into the residual that name no rewritable occurrence, and by cause they look the same as a real unbound name. So the residual is not exact while this stands, and I added it as an arm. I have not measured whether a refused wildcard arm marks its enclosing match incomplete.

RFM lowering_accessor_collapses_a_sequence_operand stays OPEN.

  • It marks the a + b narrowing as closed by XL-2: sequence-operand refs reach resolve — operator expressions lower whole, a sequence operand is never narrowed #12145.
  • It notes that body_lower_named_arg_value_optional no longer exists.
  • It restates the current specimen: let x = b && (u) / x resolves with u undeclared, via body_lower_bound_value → body_lower_arm_operand_resolved_optional. That specimen comes from the brief's measurement on main; I did not re-measure it.
  • It rewrites the trigger to "every Optional operand reader answers whole-or-located-refusal". The OptionalAccessorLocatedRefusal why is updated to match.

Witness and P5. The partition witness is now ten_delivered_and_eight_outstanding (18 arms), pinned at identity grain. P5's roster is derived from xl2_prerequisites_outstanding and keeps one cause per arm without edits. XL-2 stays NotDerivable, and there is no Complete arm.

Pattern-binder item (follow-up): I wrote a specimen for the reported pattern-binder refusal: a binder used in a nested if, inside a match, inside an if-arm. It resolves on CI, so it is not an arm. It is kept as the positive control a_match_binder_used_in_a_nested_if_in_an_if_arm_resolves. If the original finding was a different shape, it needs its exact source before it can be pinned.

🤖 Generated with Claude Code

Brian Searls and others added 4 commits September 24, 2026 16:54
…rm; five new outstanding arms; rewrite the Optional-reader RFM

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…m, with an executing specimen

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Sep 24, 2026

Copy link
Copy Markdown
Contributor Author

Re review 71000: agreed. The four probes are a measurement round on this branch, and they will not be in what gets merged. The earlier single pinning claim returned false on CI (2692588). That means my specimen does not refuse as unbound, so I did not know which verdict the specimen reaches. Once this CI run reports, I will keep only the one claim that pins the observed verdict, delete the other probes and the unused helpers, and repoint the RFM evidence and the carrier arm at that claim. If the specimen resolves instead, I will drop the arm and explain why in the PR body.

— sent from royal-gull-472

… control, drop the arm and RFM row

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Sep 24, 2026

Copy link
Copy Markdown
Contributor Author

Pattern-binder item (quiet-seal-543), measured: the specimen RESOLVES on CI. In the probe round at the previous head, probe_match_if_binder_resolves passed and the three refusal probes returned false. The specimen is if c { match s { IaslB { r: iasl_bound } => if iasl_bound { iasl_bound } else { c } .. } } else { c }. So the reported refusal does not reproduce in that shape, and it does not belong on the XL-2 list as an arm: I have no specimen that refuses. I removed the arm and the RFM row. I kept the shape as the positive control a_match_binder_used_in_a_nested_if_in_an_if_arm_resolves, and deleted the probes and unused helpers (addresses review 71000). If the original finding was a different shape, it needs its exact source before it can be pinned; I could not reach zesty-dove-429 (session not found). The partition is back to 10 delivered / 8 outstanding.

— sent from royal-gull-472

@briansrls
briansrls added this pull request to the merge queue Sep 25, 2026
Merged via the queue into main with commit 966b34c Sep 25, 2026
5 checks passed
@briansrls
briansrls deleted the session/royal-gull-472 branch September 25, 2026 05:27
@briansrls
briansrls restored the session/royal-gull-472 branch September 25, 2026 05:33
gunbai-bot Bot pushed a commit that referenced this pull request Sep 25, 2026
…ntReferenceVisibility as delivered by #12221 (its own owner claim) and re-partitions the witness, so both program-status files take main's version; this PR keeps only the reference_conservation restatements

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant