Skip to content

Grant the two lean overflow paths that merged unstamped - #7590

Closed
gunbai-bot[bot] wants to merge 1 commit into
mainfrom
session/proud-swift-104-leanroster
Closed

gunbai-bot[bot] wants to merge 1 commit into
mainfrom
session/proud-swift-104-leanroster

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 1, 2026

Copy link
Copy Markdown
Contributor

publication_placement_gate_passes is red on main again. The duplicates are gone (#7558 removed the appended repair block), but #7550 merged two paths with no grant row:

dag/extdeps/languages/lean/overflow.dag
src/v2/test/claim/lean_overflow_semantics_witness_test.dag

The gate refuses two AddedPathPublishGrantAbsent violations.

After this change

  • 38 rows, 38 unique paths, uniq -d empty.
  • added-since-cutover minus granted is empty — verified against the live cutover sha, which is the check that matters.

The repetition is the actual finding

This is the fourth cycle today, and none of it is anyone's carelessness:

  1. Revalidate generated-artifact heal heads #7544 and Model SCM P1 bounded candidate generation and bind its closing discriminator #7563 merged unstamped → main red on missing rows.
  2. Repair publication roster: stamp 11 post-cutover paths from pre-wall branches (unblocks all PR CI) #7580 repaired by appending rows that A2 presentation seam: one projection authority renders the work row (operator blockers B1-B7) #7565 had already granted in place → main red on FilePublishGrantMarkerRepeated.
  3. Bring every match-arm primitive dispatch site in the v1 interpreter under one token authority (roster R0) #7558 removed those duplicates → duplicates clear.
  4. P3b PR2 overflow semantics #7550 merged two more unstamped paths → main red on missing rows again.

Every cycle has the same shape. The gate is anchored to a fixed cutover and evaluates whatever HEAD it is handed, so a branch cut before the wall landed carries ungranted paths, passes its own checks, and reds main on merge. The author never sees the refusal — unrelated lanes do, and they pay for it. I have now had two PRs invalidated mid-flight by concurrent merges to this one file (#7582 and #7584, both closed), which is the same hazard seen from the other side.

Stamping rows closes each instance and cannot close the class. Two changes would, and neither is a roster edit:

  • Evaluate the gate against the PR's own added paths, so the refusal lands on the change that introduces them.
  • Make it a required branch-protection check, so a merge ref must stamp its own files before it can land.

post_cutover_race_repair_note already names the second as the dissolution trigger. This PR is evidence for how often the gap fires until it arrives — I am not attempting either change here.

🤖 Generated with Claude Code

publication_placement_gate_passes is red on main again. The duplicate
rows are gone (#7558 removed the appended repair block), but #7550
merged dag/extdeps/languages/lean/overflow.dag and
src/v2/test/claim/lean_overflow_semantics_witness_test.dag with no
PublicFilePublishGrant row, so the gate refuses two
AddedPathPublishGrantAbsent violations.

After this: 38 rows, 38 unique paths, no duplicate, and the
added-since-cutover set minus the granted set is empty.

THIS IS THE FOURTH TIME IN ONE DAY, and the repetition is the finding.
#7544 and #7563 merged unstamped; #7580 repaired by appending rows that
were already granted in place and re-red main on repeated markers;
#7558 removed those duplicates while #7550 added two more unstamped
paths. Every cycle is the same shape and none of it is anyone's
carelessness: the gate is anchored to a FIXED CUTOVER and evaluates
whatever HEAD it is handed, so a branch cut before the wall landed
carries ungranted paths, passes its own checks, and reds main on merge.
The author never sees the refusal; unrelated lanes do.

Stamping rows closes each instance and cannot close the class. Two
changes would, and both are outside a roster edit: evaluate the gate
against the PR's OWN added paths so the refusal lands on the change
that introduces them, and make it a required branch-protection check so
a merge ref must stamp its own files. The existing repair note already
names the second as the dissolution trigger; this commit is evidence
for how often the gap fires until it lands.

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

gunbai-bot Bot commented Aug 1, 2026

Copy link
Copy Markdown
Contributor Author

Closing as obsolete — both paths are now granted on main.

Main reads 41 grant rows for 41 unique paths, zero duplicates, and the added-since-cutover set minus the granted set is empty. dag/extdeps/languages/lean/overflow.dag and src/v2/test/claim/lean_overflow_semantics_witness_test.dag each carry exactly one grant, so merging this would add two duplicates and re-red the gate on FilePublishGrantMarkerRepeated — the same trap #7580 fell into.

That is three roster PRs of mine invalidated mid-flight by concurrent merges to this one file (#7582, #7584, and now this one), which is the same finding from the author's side that the PR body describes from main's side: this file is a serialization point and the gate is anchored to a fixed cutover rather than to the diff under test.

The class fix stands and is unaffected by this closure — evaluate the gate against the PR's own added paths, and make it a required branch-protection check so a merge ref must stamp its own files. Nothing in the roster can close it.

— sent from proud-swift-104

@gunbai-bot gunbai-bot Bot closed this Aug 1, 2026
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.

0 participants