Skip to content

Give the admission refusal a consumer: extract the reason string and witness its wording - #8839

Merged
briansrls merged 4 commits into
mainfrom
session/nimble-fox-671-refusal-witness
Aug 22, 2026
Merged

briansrls merged 4 commits into
mainfrom
session/nimble-fox-671-refusal-witness

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 22, 2026 •

Copy link
Copy Markdown
Contributor

Follow-up to #8831, from post-merge side-chat review. The reviewer's point was sharper than the wording issue it started from, and it's the one worth reading.

The actual defect: a string with no consumer

The operator-facing refusal outran its mechanism twice, and execution caught neither time:

wording narrowed by
1 "which code adjudicated" the advance #8797
2 "which source this run was running from" #8831

Both invite the reader to infer the provenance of the executing binary. The mechanism establishes only that the admission checkout's HEAD was read after the action was derived and before it was materialized — and no binary embeds its own source revision.

Both narrowings were correct. Both were caught by review, because a reason string built inline at its throw site has no consumer — nothing in the corpus could go red for it. That is specification-without-execution in the place it's easiest to miss: the typed decision stays right while the sentence beside it drifts. It is the same class #8787 landed for, a correct refusal coexisting indefinitely with misleading operator prose.

Two narrowings caught by review and zero by execution is the signal. The wording wasn't the bug; the absence of a consumer was.

What changes

fleet_desired_unobservable_judge_source_refusal_reason becomes a pure formatter that the wet entry point calls, so the wording is a subject a claim can fail on rather than a literal buried in an exit path.

The text is narrowed one final step — it names the missing receipt field and says "could not be observed after adjudication", stating the missing observation without inviting the binary-provenance inference.

Behavior unchanged: same arm, same typed refusal, same exit.

Why a witness and not a grep

The new annotation deliberately quotes both retired phrasings to record why they were wrong. A grep over the file would false-positive on the explanation of the defect. The witnesses read the function's return value, so the prose and the claim cannot collide.

Evidence — green plus the discriminating red the reviewer specified

green  28/28 PASS, 0 FAIL, 0 verdictless, 28 enrolled

red    restored the exact pre-#8831 wording:
         FAIL the_unobservable_judge_source_refusal_names_the_field_it_could_not_record
         FAIL the_unobservable_judge_source_refusal_claims_no_binary_provenance
         PASS the_advance_receipt_names_the_observed_judge_source_revision

The untouched advance row holding green proves the two new rows fail for the wording rather than because the module stopped resolving.

Presence before absence on the second row, for the reason the distinctness row upstream already carries it: three bare negations are satisfied by an empty or deleted string, so the positive conjunct pins the subject the negations must be true of.

Scope

This closes the wording class for this refusal by giving it a consumer. It does not claim the class is closed corpus-wide — other inline reason strings remain unwitnessed, and that is a broader change than this one.

…e wording

WHY THIS EXISTS. The operator-facing refusal string outran its mechanism TWICE and
execution caught neither time. It first said the run could not record "which code
adjudicated" the advance (#8797 narrowed it), then "which source this run was running
from" (#8831 narrowed that), and both invite the reader to infer the provenance of the
EXECUTING BINARY. The mechanism establishes only that the admission checkout's HEAD was
read after the action was derived and before it was materialized; no binary embeds its own
source revision.

Both narrowings were correct and both were caught by REVIEW, because a reason string built
inline at its throw site has no consumer. Nothing in the corpus could go red for it. That
is specification-without-execution in the place it is easiest to miss -- the typed decision
stays right while the sentence beside it drifts -- and it is the same class #8787 landed
for: a correct refusal coexisting indefinitely with misleading operator prose. Raised in
post-merge side-chat review of #8831.

WHAT CHANGES. `fleet_desired_unobservable_judge_source_refusal_reason` is extracted as a
pure formatter and the wet entry point calls it, so the wording becomes a SUBJECT a claim
can fail on rather than a literal buried in an exit path. The text is also narrowed one
final step -- it now names the missing receipt field (`judge-source-observed`) and says
"could not be observed after adjudication", which states the missing observation without
inviting the binary-provenance inference.

Behavior is unchanged: same arm, same typed refusal, same exit.

WHY A WITNESS AND NOT A GREP. The new annotation QUOTES both retired phrasings to record
why they were wrong, so a grep over the file would false-positive on the explanation of
the defect. The witnesses read the function's RETURN VALUE, so the prose and the claim
cannot collide.

EVIDENCE (green plus the discriminating red the reviewer specified, both executed):
  green  28/28 PASS, 0 FAIL, 0 verdictless, 28 enrolled
  red    restored the exact pre-#8831 wording:
           FAIL the_unobservable_judge_source_refusal_names_the_field_it_could_not_record
           FAIL the_unobservable_judge_source_refusal_claims_no_binary_provenance
           PASS the_advance_receipt_names_the_observed_judge_source_revision
         The untouched advance row holding green proves the two new rows fail for the
         wording rather than because the module stopped resolving.

Presence before absence on the second row, for the reason the distinctness row upstream
already carries it: three bare negations are satisfied by an empty or deleted string, so
the positive conjunct pins the subject the negations must be true OF.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot gunbai-bot Bot changed the title srv1 daily workspace still doesn't work at all Give the admission refusal a consumer: extract the reason string and witness its wording Aug 22, 2026
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review August 22, 2026 00:55
gunbc-ci-auto-heal and others added 2 commits August 22, 2026 01:16
The formatter was inserted by anchoring on the `fn fleet_desired_authorized_action_script`
line, which placed it AFTER that renderer's existing annotation. Under Sec 4c module-item
grain a contiguous `//` run attaches to the NEXT declaration, so the two blocks merged into
one and bound to the formatter: it acquired the CAS wire-word, no-op-arm and NonEmptyStr
rationale that describes the renderer, and the renderer -- the subject all of that prose is
actually about -- was left with none.

The grain was VALID the whole time, which is why the frontend check I ran reported zero
`source annotation` diagnostics and why I read that as clean. Syntactic attachment and
correct attachment are different properties, and only the first is decidable at parse. An
annotation on the wrong subject is worse than a missing one: it reads as authoritative
rationale for a declaration it was never written about. Caught by review, not execution.

Repair is placement only -- the formatter and its annotation move above the renderer's
block, restoring the adjacency that existed before the insertion. No text edited, no
behavior touched.

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

gunbai-bot Bot commented Aug 22, 2026

Copy link
Copy Markdown
Contributor Author

Both blockers fixed in ebaa4d006d5 + dcc2c796c9a. Recording the finding here on the reviewer's behalf — the review reported that its GitHub write endpoints returned 403 Resource not accessible by integration, so the finding existed only in the dashboard artifact.

1. Annotation attached to the wrong declaration — fixed

Correct diagnosis. I anchored the insertion on the fn fleet_desired_authorized_action_script line, which placed the formatter after that renderer's existing annotation. Under §4c grain a contiguous // run attaches to the next declaration, so the two blocks merged and bound to the formatter: it inherited the CAS wire-word, no-op-arm and NonEmptyStr rationale, and the renderer that prose is actually about was left with none.

The detail worth keeping: my local §4c check passed, and it was a true zero. The grain was valid throughout. Syntactic attachment and correct attachment are different properties and only the first is decidable at parse — there is no frontend diagnostic for "this block is about a different declaration." So the instrument was working and still could not see it, which is exactly the reviewer's point that compile.frontend cannot diagnose this from valid grain alone.

A misattached annotation is worse than a missing one: it reads as authoritative rationale for a declaration it was never written about. Mine claimed the formatter returns NonEmptyStr for test -s reasons; it returns String.

Repair is placement only — formatter and its annotation moved above the renderer's block, restoring the pre-insertion adjacency. No text edited, no behavior touched. Both sides verified: the formatter carries its own prose, the renderer has its block back.

2. Stale base — refreshed

Merged current main (90986d19) cleanly, no conflicts. Re-verified on the refreshed composition rather than reusing the earlier green: 28/28 PASS, 0 FAIL, 0 verdictless, 28 enrolled, both refusal rows green.

On the cancelled sibling

Confirmed and slightly sharper than the review had it: both check runs on the old head bf9427b8ecf ended cancelled, zero success. That head never had a green at all — my pushed commits superseded the sha and cancelled its in-flight runs. So there was no green receipt to be stale about on that head; the fresh run on dcc2c796c9a is the only real verdict.

Ceiling, unchanged and acknowledged

The wet arm must keep calling the formatter for this to hold. Full construction would need a typed refusal carrier or an injected execution seam, which is beyond this PR. Recorded as the ceiling rather than claimed as closed.

— sent from nimble-fox-671

@gunbai-bot

gunbai-bot Bot commented Aug 22, 2026

Copy link
Copy Markdown
Contributor Author

The red on dcc2c796c9a is inherited from main, not caused by this PR. Recording the evidence so nobody re-derives it.

Main is red. 90986d19469 — the commit this branch merged in — failed on main itself, as did 67437fcbe90. Last green main was 77ced016ef0. Introduced by #8821.

I compared the two failure sets rather than reasoning from plausibility:

main 90986d19469   16 FAIL
this PR dcc2c796c9a 16 FAIL
in mine but not main: 0

All 16 are non-exhaustive pattern match on: OccurrenceId in v2.test.claim.fold_lowering.* and v2.test.claim.body_lowering.statement_let_bind.*. This PR touches dag/gunbc/fleet_desired_admission.dag and its witness file; it has no path to src/v2 lowering. Locally the affected module is 28/28 PASS on this exact tree.

Two fixes are already open — #8853 and #8854 — so I am not opening a third. I have cross-referenced them to each other, since both modify the same two files and only one should land.

This PR is blocked on main going green, then a refresh and rerun. Nothing here needs changing in the meantime.

One instrument note, since it cost a step: gh api repos/.../actions/jobs/<id>/logs returned 0 bytes for this completed job — a false absence, not an empty log. gh run view <run> --log-failed returned the full 232KB. Worth preferring the latter when a job log comes back empty.

— sent from nimble-fox-671

@gunbai-bot

gunbai-bot Bot commented Aug 22, 2026

Copy link
Copy Markdown
Contributor Author

Correction to my comment above: I named the wrong commit. The conclusion is unchanged; the cause attribution was wrong, and since it points whoever picks this up at the wrong file, it needs fixing rather than leaving.

I wrote that the red was introduced by #8821 / 90986d19469. It was not. That is simply the commit my branch had merged in, and I reached for it instead of reading the run list I had already printed. The first failing main run is one commit earlier:

00:49  77ced016ef0  success   #8820 Repository envelope
00:51  67437fcbe90  FAILURE   #8833 v2_compiler_parse.rs was never flat   <-- first red
00:58  90986d19469  FAILURE   #8821 .dag acceptance harness               <-- what I wrongly blamed

#8833 is the first red, its own run failed 2 seconds after merge, and it touches exactly one code file: src/v2/compiler/02_parse.dag — the same file both fix PRs modify. A parser change altering occurrence allocation is consistent with all sixteen messages naming an OccurrenceId. #8821 merged into an already-red main and is a bystander.

Credit where due: swift-badger-524 traced this to #8833 independently and flagged my error.

Everything else stands — the 16 failures are identical in identity and in OccurrenceId value (27, 30, 79) between main and my unrelated PR head, zero unique to either, so the red is inherited by both of us and neither is the cause.

One diagnostic note that may save time, from swift-badger: non-exhaustive pattern match on: X names the SCRUTINEE, not the arm that failed to bind. An unimported constructor in a match arm is silently unbound and every scrutinee falls through, so the message can point at a value plainly listed in the arms and read as impossible. That is not the mechanism here — this is parser-side occurrence allocation — but the message shape is identical, and "my match is non-exhaustive" is the wrong first read in both cases.

— sent from nimble-fox-671

@briansrls
briansrls merged commit 9479b04 into main Aug 22, 2026
1 check passed
@briansrls
briansrls deleted the session/nimble-fox-671-refusal-witness branch August 22, 2026 17:33
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