Repository navigation
Land the add-slice per-stage verdict instrument named as the floor_expected_red note's producer - #10670
Conversation
…pected_red note's producer The add-slice roster note in v2.workflow.floor_expected_red carried a dated receipt (main 3a8344b: infer accepts dag_add_emitted_root; the infer-then-translate composition refuses headed by infer_grounding_not_derived) and named its own next-rung trigger: a .dag entry returning the per-stage verdicts for one root, so the paragraph can name a producer instead of a commit. v2.compiler.self_host.candidate_generation_stage_verdicts is that entry, parameterized over root and target: the receipt's verdict vocabulary (infer_accepted / infer_rejected; candidate_accepted or the rejection head reason) plus the carried-reasons lists -- the half the verdict symbols cannot say, namely that infer accepts while carrying the frontier diagnostic on its accepted path, so the enrolled witness's d == None conjunct fails even where the composition reaches acceptance. v2.test.execution.self_host_candidate_generation_stage_verdicts binds the instrument to the slice's own fixture, with add_slice_stage_verdicts_entry the runnable gunbc run --function form (ExitSuccess only when infer accepts clean and the composition accepts clean). Two witnesses: infer-accepts as a permanent positive control, and the frontier-state pin that is expected to red the day the add-slice stall's trigger lands, flipping to a permanent regression control in the same change that removes the roster row (DESIGN 4b(4)). Measured by execution on this branch: the entry exits 1 printing infer=infer_accepted, infer_carried=[infer_grounding_not_derived x10], composition=infer_grounding_not_derived, composition_carried=[x11] -- the receipt reproduced, with bind_outcome's pending-plus-gate chain counted. Both witnesses PASS; the enrolled semantic witness still fails as enrolled. Co-authored-by: Brian Searls <briansrls@users.noreply.github.com>
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f67d66c75b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| resolved_module: Node, | ||
| dag_target: TargetModel | ||
| ) -> CandidateGenerationStageVerdicts { | ||
| match infer(tree: resolved_module) { |
There was a problem hiding this comment.
Every call performs infer(tree: resolved_module) here and then calls candidate_generation_composition_verdicts, which invokes generate_translate_self_emit_candidate; that production function begins by inferring the same root again. Consequently the runnable entry and each new witness pay for two full self-host inference traversals, even though the first accepted result already contains the InferredTree needed by translate. Preserve that result and share the infer-to-translate continuation so the stage instrument does not double this expensive work.
Useful? React with 👍 / 👎.
| && (verdicts.composition_verdict == ^candidate_accepted) | ||
| && is_empty(xs: verdicts.composition_carried_reasons) { |
There was a problem hiding this comment.
If the composition accepts cleanly but emits the wrong node, this condition returns ExitSuccess. The enrolled witness in self_host_candidate_generation_test.dag requires both clean acceptance and candidate.emitted == dag_emitted_add_fn_node(), but the new instrument discards the accepted candidate value, so its advertised runnable green state is weaker and can signal that the roster row is ready for removal while that row still fails. Retain and compare the emitted candidate before returning success.
Useful? React with 👍 / 👎.
|
Consolidated into #10692 (lane-owner request: one PR for the grounding-frontier push). This commit lands there unchanged as the first commit; CI green on this tree. Closing in favor of the consolidated PR. |
2 participants
What
The add-slice roster note in
v2.workflow.floor_expected_redcarries a dated receipt — at main3a8344b5c, a throwaway probe answeredinfer_acceptedforinfer(dag_add_emitted_root)andinfer_grounding_not_derivedforgenerate_translate_self_emit_candidateover the same root anddag_add_target_model— and named its own next-rung trigger:This lands that entry, in two modules:
v2.compiler.self_host.candidate_generation_stage_verdicts— the instrument, parameterized over one root and target. It returns the receipt's verdict vocabulary (infer_accepted/infer_rejected;candidate_acceptedor the rejection's head reason) plus the carried-reasons lists: the load-bearing half the verdict symbols cannot say, namely that infer ACCEPTS this root while CARRYING the frontier diagnostic on its accepted path, so the enrolled witness'sd == Noneconjunct fails even where the composition reaches acceptance ("both conjuncts fail for the one cause").v2.test.execution.self_host_candidate_generation_stage_verdicts— the add-slice binding over the slice's own fixture.add_slice_stage_verdictsis the pure entry;add_slice_stage_verdicts_entryis the runnablegunbc run --functionform, exiting nonzero with the verdicts rendered while the composition refuses andExitSuccessonly at the enrolled witness's green state.The roster note is updated to name the producer, discharging its trigger; the dated receipt stays, true of its fixed tree forever.
Witnesses
add_slice_infer_accepts_holds— PERMANENT positive control. Infer accepting this root is the fact the note's structural account could not establish; it stays true after the repair lands.add_slice_composition_refuses_at_the_grounding_frontier_holds— pins TODAY's frontier state (composition refusal headed byinfer_grounding_not_derived, infer carrying that reason and nothing else) so the instrument's composition arm has a discriminating consumer (DESIGN §5). It is expected to RED the daygunbc.guarantee_stall.self_host_candidate_generation_add_slice_stall's trigger lands; the repair rewrites it to assertcandidate_acceptedwith empty carried lists — the DESIGN §4b(4) flip from frontier guard to permanent regression control — in the same change that removes the roster row.Measured by execution on this branch
gunbc run --function add_slice_stage_verdicts_entryexits 1 and prints:The receipt reproduced exactly, with the composition chain counted: infer's 10 pending accepted-path diagnostics plus translate's 1 gate refusal, as
bind_outcome'srejected_with_pendingpredicts. Both new witnesses PASS viaclaim_batch; the enrolled semantic witnesscandidate_generation_translate_self_emit_dag_add_slice_holdsstill fails as enrolled — behavior unchanged.Out of scope
The repair itself — infer deriving grounding for the Arrow, Conj and Atom kinds of the add fn — is v2 self-host lane work named as the stall's
next_rung_trigger, deliberately not attempted here: the sibling witnesses indag_add_emit_round_tripgreen only through hand-authoredDerivedGroundingfacts, and making infer answer that way for connective nodes generally is theroot == rootdefect the frontier carrier replaced.