Skip to content

DESIGN.md listed a retired rung drop as standing: derive the list from the rows' own standing - #9865

Merged
gunbai-bot[bot] merged 2 commits into
mainfrom
session/gentle-bear-446
Sep 1, 2026
Merged

gunbai-bot[bot] merged 2 commits into
mainfrom
session/gentle-bear-446

Conversation

@gunbai-bot

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

Copy link
Copy Markdown
Contributor

What was wrong

DESIGN.md's "The ones standing today" list was projected as an unfiltered map over gunbc.rung_drop rung_drop_roster. Retirement was written only as prose inside each row's authored paragraph, which a projection cannot read.

So the list asserted "Cited-symbol resolution as a required check" as currently standing for six days after its restoration trigger fired on 2026-08-25 — in a document that is loaded in full on every turn of every session. Two sessions independently built work on that false premise, which is the measured harm rather than a hypothetical one.

Why not a hand-edit

DESIGN.md declares itself a projection of gunbc.design_document that is never hand-edited. Correcting the rendered list would have left the second authority in place to drift again on the next retirement — the §3 fork this list already demonstrated once.

The repair is derivation:

  • gunbc.rung_drop gains RungDropStanding = Standing | Retired { trigger_fired } and a standing field, so retirement is a fact the row owns rather than prose beside it. A predicate over the pre-existing data could not have fixed this: there was no data.
  • rung_drop_is_standing / standing_rung_drops derive the list; gunbc.design_document projects standing_rung_drops().
  • gunbc.design_ledgers still folds the full roster — a ledger records retired drops too. Two consumers, each asking its own question of one authority.

Vocabulary follows the gunbc.deleted_cadence_reference_census precedent (a typed standing carried beside a row) rather than inventing a parallel shape.

Census of the other rows

A list that drifted once may have drifted more. It had not — exactly one row is retired. emit_stage_blocking says "NARROWED RATHER THAN RETIRED" and fabric_evidence_gating says "THIS IS NOT RETIRED BY THE MEMO PR MERGING"; the rest carry no retirement language. DESIGN.md goes 8 rows to 7, a one-line deletion.

Evidence, executed

test.claim.rung_drop_standing_partition_witness_test returns true on this tree and false when the retired row is re-marked Standing — run through gunbc run against the real modules, both arms observed.

Its second conjunct is the point: it asserts the roster still holds a retired row. Without it, a filter over an all-Standing roster excludes nothing and the check is permanently green by construction — the §4b decoration this project refuses to count as coverage.

Residue, named

standing is authored, and nothing derives it from the paragraph beside it. authored is carried byte-for-byte on purpose (gunbc.rung_drop records why splitting it has no oracle). This change removes the second authority for the standing list; it does not close the gap between a row's prose and its field. Stated here rather than left to be discovered.

Provenance — this is not what the lane was assigned

The lane (XL-0-CITE) was briefed to measure a dangling-citation population created when the #9752/#9753/#9751 prose-bankruptcy sweeps converted citable declarations into uncitable §4c annotations, on the premise that this happened while the cited-symbol check was down.

That population is zero, and the premise was false — the brief's error, not a finding against its author:

  • The check enrolls only typed DeclarationRef citations, via exactly two producers in v1_compiler.declaration_index (citation_from_record_literal, citation_from_constructor_call). More decisively, v1_compiler.cli_run annotation_erased_scan_text feeds the semantic passes per §4c, so annotation prose is not present in the tree the harvester walks. A prose name is not an unresolved citation; it is not a citation.
  • Joining 1205 typed citation identities against 4209 declarations the three sweeps removed gives 0 — today, and also 0 computed as of the sweep commit itself, ruling out a later repair. A two-arm planted control confirms the join discriminates in both directions.
  • The drop was retired 2026-08-25, five days before the sweep landed 2026-08-30, restored strictly wider inside --required-ci. The sweep landed under a live, wider check.

Chasing that false premise is what surfaced the defect this PR fixes — DESIGN.md is where the premise came from.

Coordination

No overlap with #9831: it touches docs/design-ledgers.md and the phase-series board; this touches DESIGN.md and the drops list. Disjoint files, disjoint subjects.

🤖 Generated with Claude Code

https://claude.ai/code/session_016Fk4zsZLzxJ3zJ3o969vBQ

…m the rows' own standing

DESIGN.md's "The ones standing today" list was projected as an UNFILTERED map over
gunbc.rung_drop rung_drop_roster. Retirement was written only as prose inside each row's
`authored` paragraph, which a projection cannot read. So the list asserted
"Cited-symbol resolution as a required check" as currently standing for six days after
its restoration trigger fired on 2026-08-25 -- in a document loaded in full on every turn
of every session. Two sessions independently built work on that false premise.

The repair is derivation, not a hand-edit: DESIGN.md declares itself a projection that is
never hand-edited, so editing the list would have left the second authority in place to
drift again on the next retirement.

- gunbc.rung_drop gains RungDropStanding (Standing | Retired { trigger_fired }) and a
  `standing` field, so retirement is a fact the row owns rather than prose beside it.
- rung_drop_is_standing / standing_rung_drops derive the list; gunbc.design_document
  projects standing_rung_drops() instead of the whole roster.
- gunbc.design_ledgers still folds the FULL roster: a ledger records retired drops too.
  Two consumers, each asking its own question of one authority.

CENSUS OF THE OTHER SEVEN ROWS, since a list that drifted once may have drifted more: it
had not. Exactly one row is retired. emit_stage_blocking says "NARROWED RATHER THAN
RETIRED" and fabric_evidence_gating says "THIS IS NOT RETIRED BY THE MEMO PR MERGING";
the rest carry no retirement language. DESIGN.md goes 8 rows to 7.

EVIDENCE, executed, not described. test.claim.rung_drop_standing_partition_witness_test
returns true on this tree and false when the retired row is re-marked Standing. Its second
conjunct asserts the roster still HOLDS a retired row: without it, a filter over an
all-Standing roster excludes nothing and the check would be permanently green by
construction -- a decoration, not a wall.

RESIDUE, named rather than left to be discovered: `standing` is authored and nothing
derives it from the paragraph beside it. This change removes the second authority for the
standing LIST; it does not close the gap between a row's prose and its field.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016Fk4zsZLzxJ3zJ3o969vBQ
@gunbai-bot

gunbai-bot Bot commented Sep 1, 2026

Copy link
Copy Markdown
Contributor Author

Thanks — I verified this one rather than applying it, and I'm declining it as a finding. The verdict correctly calls the standing-list correction sound; the objection to rung_drop_is_standing does not hold, on three independent checks.

1. The cited rule does not exist. The finding says this is "the exact predicate-dissolution pattern prohibited by DESIGN.md". I grepped DESIGN.md for predicate, dissolution, and boolean predicate. There is no such prohibition. predicate appears exactly once, in §4b — "does not lift arbitrary predicates to proof" — which is about not treating an arbitrary predicate as a proof obligation, not about how a total match over a coproduct may be written. The two rules in DESIGN.md that use the word dissolution are §4b(4) "Dissolution on climb" (a climb deletes the redundant lower-rung production machinery it obsoletes) and §5's dissolution conditions for admitted debt. Neither is about this. Since the rule named is the whole basis of the REQUEST_CHANGES, I can't act on it without inventing a requirement the authority doesn't carry.

2. The corpus disagrees, at scale. A total match over a coproduct returning only true/false from a -> Bool function occurs 1059 times across the tracked .dag corpus — including inside dag/std/types.dag, the substrate's own core module (hold_local_frame_is_ready, dimension_evidence_is_spendable). If this pattern were prohibited, the substrate violates it in its own foundation a thousand times over. That's not a defect population; it's the idiom.

3. It is the shape of the precedent this PR was explicitly pointed at. gunbc.deleted_cadence_reference_census — named to me as the worked precedent for dispositioning a premise-invalidated reference — carries terminal_execution_standing_is_terminal, which is this function byte-for-byte in structure: a -> Bool total match over a standing coproduct, true on one arm, false on the other. I followed that precedent deliberately rather than inventing a parallel shape, which is the §3 single-authority move.

On "must consume a canonical fold/query surface": it does. rung_drop_is_standing is a total, exhaustive match over RungDropStanding — the closed coproduct declared four lines above it. A match over a closed variant is the substrate's elimination form (§4: Match is one of the six behaviors). There is no other query surface for a two-variant coproduct to route through, and adding an indirection layer would be the re-invention §2 prices as a failed decomposition. Nor is a bounded disposition owed: a disposition/receipt is for admitted debt, and no debt is being admitted here.

What I did carry, so this isn't read as declining scrutiny generally: the PR already names the one real second authority in this change — standing is authored, and nothing derives it from the authored paragraph beside it. That residue is stated in the module note, the commit message and the PR body rather than left for a reader to find. It's the honest open item; the predicate is not.

One small note in the same spirit as this PR's subject: the finding cites dag/gunbc/rung_drop.dag:140 positionally. §3's standing rule asks for the module and symbol (gunbc.rung_drop rung_drop_is_standing) precisely because any edit above line 140 silently invalidates the pointer — which is the decay class this PR is about.

Happy to reconsider immediately if someone can point me at the actual clause; I searched for it and it isn't there.

— sent from gentle-bear-446

@gunbai-bot

gunbai-bot Bot commented Sep 1, 2026

Copy link
Copy Markdown
Contributor Author

CI fixed at 3fd86d0f4c. The failure was real and worth naming precisely, because neither parent commit contained the defect.

required-witnesses-floor refused with:

dag/gunbc/rung_drop.dag:120:46: error: missing required field 'standing' in literal of type 'RungDrop'

Cause: a semantic merge conflict that git resolved cleanly. This PR adds a required standing field to RungDrop. While it was in review, #9720 landed on main adding a ninth drop row, text_boundary_identity_wall, written against the eight-field-less type. Each side is internally consistent; the synthetic merge combines my new required field with main's new literal that lacks it. Git auto-merged rung_drop.dag with no conflict — the two edits touch different regions of the file — so nothing surfaced until the type-checker ran over the merged tree. My branch alone type-checks; main alone type-checks; only the merge is broken.

Fix: merged main and gave the new row standing: Standing. I determined that by reading its own paragraph rather than defaulting — it declares a fresh drop on 2026-08-30 and carries no retirement language, so Standing is its honest state, not merely the value that compiles.

DESIGN.md came through as unmerged with no conflict markers — the generated-artifact merge driver refusing rather than picking a side, exactly as intended. I resolved it by re-running the real actuator (gunbc run … generated_artifact_gate main_wet) on the merged tree, never by hand-editing a file that declares itself never hand-edited.

Verified on the merged tree:

  • Every RungDrop literal now carries standing (9 rows, 0 missing).
  • test.claim.rung_drop_standing_partition_witness_test returns true.
  • The standing list renders 8 rows: the 7 that were standing, plus main's new text_boundary_identity_wall — and still without the retired cited-symbol row. That the new drop appears automatically is the point of the change: main's author added a row and it landed in DESIGN.md without touching the projection.

Worth noting for the record, since it argues for this PR rather than against it: the new required field is what caused the merge to fail loudly instead of silently. Before this change, a row could be added with its retirement state unrepresentable and nothing would object — which is precisely how DESIGN.md came to publish a retired drop as standing for six days.

The rust-unit-tests and fabric-evidence checks passed on the previous head; re-running now on the merge.

— sent from gentle-bear-446

@gunbai-bot
gunbai-bot Bot merged commit 12da79d into main Sep 1, 2026
6 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/gentle-bear-446 branch September 1, 2026 02:57
@briansrls
briansrls restored the session/gentle-bear-446 branch September 1, 2026 03:04
briansrls pushed a commit that referenced this pull request Sep 1, 2026
Resolves six unmerged paths from the squash-merge of #9850.

Two were genuine .dag authority conflicts, resolved toward this branch's
newer content. One mattered beyond recency: main's side of 05_emit_rust.dag
still carried string_contains(sp.file, "<kernel:"), the substring test that
this branch replaces with exact equality against the resolved kernel identity.
Taking either side wholesale would have silently reinstated the weaker
second authority.

Four were generated paths where the merge driver refused: no conflict
markers, ours-side bytes in the worktree, main's newer generated content
dropped. A marker grep reads that tree as clean; git ls-files -u does not.
The build then failed on LiteralUnfolding::UnicodeScalarSequenceUnfold not
covered -- main's own #9720 content missing from exactly those four files --
so the mirror was internally inconsistent in a way only a compile revealed.
Bootstrapped to main's consistent mirror to obtain a buildable seed; the
bytes here are regenerated from the merged authority, which is the
resolution that is neither side.

#9865 added a required `standing` field to RungDrop after this branch
authored its row. The text merge combined both sides with no conflict and
the typecheck refused with an exact location, which is the fail-closed
property working as intended.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BDnHQs9oE5AKJXe1vReU8v
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