Repository navigation
PARKED (awaiting operator blessing): scope DESIGN §3 'the deletion is the census' to the population something compiles - #11266
Conversation
…ion something compiles Awaiting the operator's explicit blessing of the wording; not for review or landing until then. Edits the authority gunbc.design_document only. DESIGN.md is left to the generated-artifact regeneration, never hand-edited. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ABhPYzsR1vusUjoA6S94t1
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: badd5cc682
ℹ️ 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".
| h3(text: "§3 standing rule — replacement migrations cut over at the root"), | ||
| p(text: "When two structures answer the same semantic question and one is intended to disappear, the change is a **replacement migration**, not a refinement. §2 prices an intermediate representation destined to be discarded as redundant work, and §3 forbids X and Y both answering for one fact. Editing X from its leaves upward preserves its root while every intermediate state becomes observable and load-bearing, so the migration creates more authority before it removes any. The deeper cost is that a surviving X is an **attractor**: while it stands, every nearby question is answered in its vocabulary, so decisions keep being premised on an assumption already scheduled for death — and A3 grounds agreement only on what stays stable across time, which a dead assumption by definition does not."), | ||
| p(text: "So the default is **delete-first**: uproot the root as early as you can, then fix forward minimally with the new solution, solving each surfaced problem from first principles rather than restoring it to its old binding. In a fail-closed substrate **the deletion is the census** — every real dependent refuses loudly, so what breaks is exactly what was load-bearing. What cannot break loudly is covered by a declared, bounded §4b rung-drop, never by silence. Two carve-outs: a gap-intolerant boundary keeps the staged form — Y built in shadow, then one transition that switches the root and deletes X together — and where no Y can hold the boundary at all, X stays but stays **frozen**: no new investment, no new rows on its growth surfaces."), | ||
| p(text: "So the default is **delete-first**: uproot the root as early as you can, then fix forward minimally with the new solution, solving each surfaced problem from first principles rather than restoring it to its old binding. In a fail-closed substrate **the deletion is the census over the population something compiles** — every real dependent refuses loudly, so what breaks is exactly what was load-bearing. The required gate is a static roster the operator signed, the compiler floor and nothing else (`v2.workflow.required_floor` `required_gate_prefixes`), so outside it the substrate still refuses and nothing asks it to: a product-layer dependent can stop resolving, stay broken, and let every required lane report SUCCESS. **For a root outside the gate the census is yours to take — enumerate the consumers by name before you delete.** What cannot break loudly is covered by a declared, bounded §4b rung-drop, never by silence. Two carve-outs: a gap-intolerant boundary keeps the staged form — Y built in shadow, then one transition that switches the root and deletes X together — and where no Y can hold the boundary at all, X stays but stays **frozen**: no new investment, no new rows on its growth surfaces."), |
There was a problem hiding this comment.
The manual-census obligation is incorrectly conditioned on the replacement root being “outside the gate.” required_gate_prefixes selects witness modules, while required_floor_runner compiles a forward import closure; compiling or admitting the root does not pull in reverse dependents, so an admitted root can still have an unchanged product-layer consumer outside the prepared closure that remains broken while every required lane succeeds. Conversely, an outside-prefix module may be compiled when another closure seed reaches it. Scope this obligation to whether every consumer is proven present in the prepared closure, rather than to the root's gate membership, or this retains the same unsafe migration path the paragraph is intended to close.
Useful? React with 👍 / 👎.
|
Thanks — the finding is correct about the state of this branch, and it is not being fixed by a hand commit right now, for two reasons. This PR is parked, not merge-bound. It carries the proposed §3 wording for the operator's explicit blessing and was returned to draft for that reason. Nothing here lands until the operator says yes, so the stale The projection's regeneration route is heal, and it has not run. The branch's only CI run was deliberately cancelled before any job started, to avoid spending a runner on an unblessed proposal. Your content read — that the edit narrows an over-claim, preserves the rung-drop clause, and matches what — sent from bright-eagle-728 |
…09-design-s3-scope
…e gate as a resolvable reference
Operator blessed the substance and took the reviewed wording (bright-eagle-728).
Three changes against the parked proposal:
- "the population something compiles" -> "the population a run compiles". "Something"
was the only vague term in an otherwise precise sentence and read ambiguously as
either the compiling agent or the thing compiled.
- The restated ruling ("a static roster the operator signed, the compiler floor and
nothing else") is dropped. The proposal's own stated choice was to cite the ruling
by symbol rather than fork its text into §3; restating it did the thing it forbade.
- One bolded span instead of two, and the paragraph grows by roughly a third rather
than tripling -- DESIGN.md is loaded in full on every turn of every session.
The gate is now cited as a typed DeclarationRef row in gunbc.documentary_refs rather
than backticked prose, so v2.lens.cited_symbol_resolution resolves it on the required
path and a rename or deletion of required_gate_prefixes reds without anyone editing
the document. That module's own header names the alternative -- a system named only
inside a string literal is unreachable by that lens -- and an unresolvable citation in
the paragraph about §3 citation discipline was the weaker choice.
DESIGN.md is not hand-edited; the projection regenerates from the authority.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Addresses review 67464 (REQUEST_CHANGES), which is correct. DESIGN.md is a committed projection carrying AuthorRegeneratesBeforeMerge -- gunbc.generated_artifact concurrent_divergence_repair hands HealRegeneratesAfterProvisionalMerge to DesignRungDropsArtifact and to nothing else, so DesignArtifact is the author's obligation. The earlier claim on this PR that the projection regenerates from the authority was wrong: it carried over the merge-driver instructions from the docs/design-rung-drops.md conflict on gunbc#10994, a different artifact on a different repair route. This PR has also never dispatched a CI run, so heal-generated-artifacts never fired either. Left stale, the authority and the projection answered "what does §3 say about the census" with materially different obligations, and the stale one is the copy loaded in full by every session -- the §3 fork, in the paragraph about §3. Regenerated through gunbc.instruments.generated_artifact_gate main_wet_one for the single path, not main_wet: that module's own annotation records that main_wet rewrites all 35 artifacts whatever you came for and can silently resurrect a file in the working tree. Exactly one line of DESIGN.md changed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Fixed in 3935017 — review 67464 was right, and the diagnosis in it is exact.
Why I got it wrong, since it is the more useful part: my earlier statement on this PR that "the projection regenerates from the authority" carried over the merge-driver instructions from the Regenerated through Separately, and not a request for anything: this branch still has no CI run on any head — — sent from bright-eagle-728 |
Addresses review 67476 (REQUEST_CHANGES), which is correct: adding required_gate_prefixes_ref to generated_document_declaration_refs() broke that function's own discriminating controls instead of extending them, which is DESIGN §5 backwards. - fixture_modules() gains v2.workflow.required_floor. - intact_facts() gains the required_gate_prefixes declaration, so the intact control is intact again for both rows. - documentary_refs_population_is_the_union: length(generated) == 1 -> == 2. Two beyond the review, because the change made existing prose false: - documentary_refs_generated_document_renders_the_rows asserted only the v1 row while its annotation says it asserts the rendered symbol text of EACH row. With two rows the new one's rendering was unchecked -- and that claim is the one stopping a row and its printed name from diverging, which is the whole reason the row exists. It now asserts both. - The intact_facts() comment read "The four declarations" against a one-element list. It now states the invariant (one fact per row) rather than a count that rots. THE FIRST ATTEMPT AT THIS FIX WAS STILL RED AND THE REASON IS WORTH CARRYING. A DeclFact holds the LOGICAL qualified name: v2.std.decl_index logical_qualified_name_from_module strips a leading `v2.`, while module_path_declared compares the module row against the FULL path. So the module row is `v2.workflow.required_floor` and the fact is `workflow.required_floor.required_gate_prefixes`, and both are correct. The asymmetry was invisible in this fixture until now because its only other fact names a `gunbc.` module with nothing to strip. An annotation records it, since the absent prefix reads as a typo and would otherwise be "corrected" back into the bug. Verified by execution: all five witnesses return true, and breaking the new fact's qualified name drives documentary_refs_intact_population_resolves_clean to false -- so the control discriminates for the new row rather than passing vacuously. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Fixed in 73d22f0 — review 67476 was right, and both findings reproduced exactly as described.
Two beyond the findings, because the change made existing prose false. The first attempt at this fix was still red, and the reason is the useful part. A Verified by execution rather than by reasoning, which is what the finding was about: all five witnesses return — sent from bright-eagle-728 |
The required floor's parse phase refused six lines of dag/test/claim/documentary_refs_witness_test.dag: "source annotation sits inside a declaration body. Only module-item grain is modeled." DESIGN §4c admits only standalone leading // blocks attached to module-scope declarations, and the note explaining why the required_gate_prefixes DeclFact omits the v2. prefix had been placed inside the intact_facts() list literal. Its three downstream blockers (namespace-wave-admission, floor ArmSetConsumerPlanningUnavailable) were cascades of the parse refusal producing no index. The note now leads intact_facts(), joined to that function's existing annotation, and says the same thing. No other file on this branch adds an indented //. A local `gunbc run` of these witnesses accepted the body-grain annotation, which is why it passed locally and refused in CI; the interpreter entry does not run the strict parse phase, so it is not evidence for this class. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The required floor refused documentary_refs_population_is_the_union at 126,434 eval steps against the 72,300 new-witness budget. The claim compared length(all_documentary_declaration_refs()) against a second, direct evaluation of hand_authored_doc_declaration_refs(), so it paid the hand-authored population twice -- all_documentary_declaration_refs() already evaluates it. The cost was latent on main: touching this file is what planned the claim as a changed witness. The union is now evaluated once. The claim asserts every generated ref is a member of it (std.decl_ref declaration_ref_in_list) and that it is strictly larger than the generated side, so dropping either side reds. A partial loss inside the hand-authored population is that population's own subject, carried by test.claim.doc_graph_reference_partition_witness_test, and the annotation says so. No debt row: DESIGN §3's witness rule removes the repeated derivation rather than buying it a budget. Verified by execution: all five witnesses return true, and substituting the generated list for the union (the hand side dropped) drives the claim to false. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The required floor refused documentary_refs_population_is_the_union twice: 126,434 eval steps on the original form, then 139,882 after the previous commit rewrote it to evaluate the union once. That rewrite rested on a wrong diagnosis -- the cost was never the double evaluation of the hand-authored population, it was evaluating the union at all. The union has no consumer. all_documentary_declaration_refs is called by exactly one site, this witness. Its annotation says it widens the cited-symbol lens's denominator, and that lens was deleted (test.claim.long.carrier_reference_integrity_witness_test records the deletion). The live enforcement of a cited DeclarationRef is v1_compiler.declaration_index, which resolves every std.decl_ref constructor literal at ingestion -- so required_gate_prefixes_ref is enforced on the live path with or without the union. A claim proving an unconsumed declaration is well formed is DESIGN §3c's dangling case; making it cheaper would keep dead code alive, so both go, together with the annotation that described the deleted lens and an import nothing now reads. What remains exercises the resolver itself against planted populations: the intact control, the rename and ambiguity reds, and the rendering claim. All four return true under a local run. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
1 participant
Scopes the delete-first doctrine's safety claim in DESIGN §3 (the replacement-migration standing rule) to the census the gate actually performs. The failure class this repairs is filed as
gunbc.recurring_failure_mode.doctrine_safety_claim_stated_wider_than_the_census_that_delivers_itin #11173.One sentence in the authority
gunbc.design_document(dag/gunbc/design_document.dag) is changed.DESIGN.mdis not hand-edited. It is a projection of that authority and is left to the generated-artifact regeneration.Today
Proposed (the shorter variant)
Why the sentence is wrong today
The required gate is a static roster by operator ruling (2026-08-29): the compiler floor and nothing else. Receipts are in #11173. On gunbc#10994's head
46b4ba130cd, five references to a renamedRemainingShapefield in three product-layer modules could not resolve. The floor still reported SUCCESS. Its disposition artifact (run 34689263434) records every identity of those modules atdeclined_outside_gate_closure/not_executed, meaning the modules were never compiled. The substrate does refuse such references, but only in modules a run compiles.Three deliberate choices (blessed by bright-eagle-728; the operator's to overrule)
required_gate_prefixes), not restated with its price. Restating it would fork the ruling's own text into §3, which is the §3 single-authority rule applied to §3 itself.The longer variant carried two mechanism facts: changing an authority does not enrol its unchanged witness consumers, and discovery ranges more widely than preparation. They were deliberately dropped from §3 because the failure-mode row filed in #11173 carries them. §3 carries the rule, and the row carries the mechanism.
Verification
origin/mainatdf34fbc3228, and the diff changes exactly that one line.gunbc.design_documentresolves and evaluates locally undergunbc run.🤖 Generated with Claude Code
https://claude.ai/code/session_01ABhPYzsR1vusUjoA6S94t1
What changed after the blessing (bright-eagle-728)
The operator approved the substance and asked for the reviewed wording. Three edits against the proposal above:
somethingwas the only vague term in an otherwise precise sentence, and it read ambiguously as either the agent doing the compiling or the thing compiled. A run is the thing with a closure, which is also how the floor's own dispositions talk (declined_outside_gate_closure).The citation is now resolvable, not prose
The proposal cited
required_gate_prefixesin backticks.gunbc.documentary_refsexists precisely to carry a named system as a typedDeclarationRefso thatv2.lens.cited_symbol_resolutionresolves it on the required path; its header states the measured consequence of the alternative, where a prerequisite sentence stayed true-looking across four copies after the prerequisite was discharged. So this addsto that module's population, and the paragraph renders the row. A rename, deletion, or fork of
required_gate_prefixesnow reds without anyone editing the document — which seemed like the right standard for the paragraph that is about §3 citation discipline.Verified by execution
gunbc run --source-root dag --source-root src/v2 --entry dag/gunbc/design_document.dag --function design_documentevaluates, and the rendered paragraph carries the new sentence with the reference resolved to`v2.workflow.required_floor required_gate_prefixes`.DESIGN.mdis not hand-edited; the projection regenerates from the authority.