Repository navigation
v2: a fn's uses clause parses; lowering refuses the fn at the clause until an effect-requirement carrier exists - #12816
Conversation
…s the fn at the clause on both arms v2 has no carrier for a fn's resource requirement, so the fn refuses with body_lowering_reason_uses_clause_unmodeled located at the clause (never lowered without it); new recurring_failure_mode uses_clause_has_no_carrier names the carrier as the trigger. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…chor is the uses_clause shell Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
|
Executed evidence for the return-clause depth (it replaces the PR body's 'can't serve as the depth wall right now'): the wall was silent on main because its entry refused on an unimported — sent from keen-fox-715 |
…eads the Outcome-valued signature inside the uses refusal; warm-roster union) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
HOLD / REQUEST_CHANGES at exact head 08a8136.
[P1] This PR creates a new live fatal front-end cause, body_lowering_reason_uses_clause_unmodeled, and measures 11 real corpus modules reaching it, but does not add it to v2.workflow.compile_door_cause_ownership known_frontier_causes. That module is the single cause-ownership authority used by the door/native-route frontier at diagnostic grain. The result is a typed, located refusal with an RFM, but an unowned fatal cause once those recovered modules enter the native-route census.
Add one FatalGrain CauseOwnership row for body_lowering_reason_uses_clause_unmodeled, with the lane and flip trigger matching uses_clause_has_no_carrier: the cause retires when the lowered fn signature carries every uses entry's resource requirement. Keep the one-authority key unique. A focused ownership/table control is appropriate if the existing table witness does not execute this new symbol.
The grammar placement, two-arm fail-closed lowering, located controls, occurrence-role row, and return-clause depth evidence otherwise look coherent. Return the corrected exact head for merge-queue-only review.
… compile_door_cause_ownership (FatalGrain, flip on the effect-requirement carrier) Addresses GitHub review 5371574103. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
|
Addressed GitHub review 5371574103 at c767ff7. The new live fatal cause Executed at this head (claim_batch, 30 GB BuildBuddy runner):
— sent from keen-fox-715 |
briansrls
left a comment
There was a problem hiding this comment.
APPROVE at exact head c767ff7, superseding CHANGES_REQUESTED review 5371574103.
The held ownership defect is corrected. known_frontier_causes now contains one FatalGrain / SharedSelfHostCriticalPath row for body_lowering_reason_uses_clause_unmodeled, with the flip trigger tied to the effect-requirement carrier described by uses_clause_has_no_carrier. The correction is the only delta from the previously reviewed head, and the ownership and exact-head checks pass.
This exact head is currently reported non-mergeable by GitHub, so it is not presently queueable. Any conflict-resolution or main-merge commit creates a new head and requires renewed exact-head approval. Landing remains merge-queue only; no direct merge or check bypass.
…union) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
APPROVE-MERGE / REBIND at exact head f37d223. Supersedes my approval at c767ff7. The new commit is a main merge whose parents are that approved head and main a00d1fe. The current branch diff retains the approved seven-file set and 201/24 change counts; the warm-roster resolution adds only uses_parsed and uses_refusal beside main's rows. Exact-head floor, generated, emit-build, and witnesses pass. Merge-queue landing only: the actual merge_group candidate must pass against then-current main; no direct merge or check bypass.
XL-2, per quiet-seal-543's ruling A on class D: the v2 parse refusals for a fn's
usesclause.Is the form legitimate? Yes, and it is a semantic fact
v102_parseparse_uses_clause/parse_uses_entryreaduses name: Type[(cfg)], ...after a fn's return clause. The corpus writes it in 16 files (58 clauses, e.g.uses net: Network,uses net: Network, fs: Filesystem). v2's grammar had nousesclause at all, so every one of those modules refused whole at parse.The clause is the fn's resource (effect) requirement: DESIGN's CLI section notes a resource method is admitted only where the fn declares that resource in its
usesclause. v2 has no carrier for that requirement, so parsing the clause and then lowering the fn without it would erase an effect requirement silently.The change (never parse-then-drop)
v2.extdeps.languages.dag): two new productions,uses_clause(dag_grammar_uses_clause_expr) anduses_entry(dag_grammar_uses_entry_expr), mirroring v1. The clause sits indag_grammar_fn_decl_exprafter the return clause and beforeadmit_callers, where v1 puts it, so the positional return-clause read (body_lower_fn_decl_return_clause_optional, right four times then left) is unaffected. The spine note is updated from three optionals to four.v2.compiler.body_lowering_fold):body_lower_fn_uses_refusal_optionalrefuses any fn carrying a clause with the new reasonbody_lowering_reason_uses_clause_unmodeled, anchored at theuses_clausenode. It is asked first on both arms (body_lower_fn_decl_to_arrowandbody_lower_fn_decl_to_census_arrow), because the requirement is part of the signature both read. Both new shells are on the structure-preserved list, so they don't retain generically before the fn refuses.v2.compiler.occurrence_role): table admission requires a row foruses_entry, whose name terminal is a resource binder. It getsNameRoleRead { DeclarationRole, LexicalValueOccurrence }via thename: valuedecoder.gunbc.recurring_failure_modeuses_clause_has_no_carrier. Rung: mitigated. Ceiling: structurally impossible. Trigger, naming the capability: a v2 effect-requirement carrier on the lowered fn signature that body lowering reads eachusesentry onto.Carrier note, for the XL-2 status: these modules stay out of the XL-2 reference census until that carrier exists. They now parse, but refuse at normalize, located at the clause.
Controls (
v2.test.claim.parse.uses_clause, nullary values enrolled warm)a_fn_with_a_uses_clause_parses_holds: a two-entry clause parses. Red on main.a_fn_with_a_uses_clause_refuses_at_the_clause_holds: normalize refuses withbody_lowering_reason_uses_clause_unmodeled. Red on main.the_uses_refusal_is_located_at_the_clause_holds: the refusal'sNodeLocusanchor is theuses_clauseproduction shell. Red on main.All three were executed red on main (test added alone) and pass on the branch (claim_batch, 30 GB BuildBuddy runner).
Parse count, the 16 files (v2 parse, main against branch)
gunbc.auth.approval_device_routes: theadmit_callerstrailing comma, v2 grammar: an admit_callers list may end in a comma (27 of 31 measured modules stop refusing whole) #12796.gunbc.auth.credentials@840,gunbc.assimilate.bmc_bootstrap_provision@1542 andgunbc.tailscale_acl_phase2_credential@5525: not yet attributed.gunbc.auth.approval_ntfy_access_readbackmoves past its clause to a later defect.Suites
occurrence_role(including table admission with the new row) andclosure_parse_batch_two(admit_callers).reference_conservation's two refused-normalization controls are red on main too, fixed by reference_conservation: refused-normalization controls use a service module (red on main since #12713) #12812.dag/test/claim/parse_test_fn_decl_return_clause_test.dagexits 1 with no verdict output identically on main and this branch, so it is broken independently of this change and currently can't serve as the depth wall. Its subject, the return clause, is before the inserted slot by construction, and the normalize suites above, which lower fns with return types, pass. I'm flagging it rather than claiming the wall held.Land only via the merge queue.
🤖 Generated with Claude Code