Repository navigation
Guarantee ladder follow-up: climb plan in the canonical roadmap graph, derived rung state, construction-walled doc binds - #7489
Conversation
The analysis note landed as an orphan doc: gunbc.doc_graph_roots states that "an unbound doc is an orphan, loudly", and CI duly refused at be1a001 with doc_graph_has_no_orphan_docs returning false in both the dag/test/claim and src/v2/lens consumers. Registered as two HandAuthoredDocBind rows rather than one, because the analysis binds to two independent carriers and they dissolve on different triggers: - v1.compiler.infer module_skips_direct_call_arg_check — the one named violation of the dimension contract's "no escape hatch" clause (docs/thesis/correctness-dimensions.md), exempting v2.* and v1.compiler.* from direct-call argument checking. - v2.std.constraints solve_constraints — passes graph.root as source_facts, algebra AND the sole candidate, so the grounding proof reduces to well_formed(root) and is relabelled CanonicalGrounding. Green by execution, both directions: RED is the CI failure at be1a001; GREEN is all five witnesses in dag/test/claim/doc_reachability_witness_test.dag plus doc_graph_is_clean in src/v2/lens/doc_reachability_test.dag passing locally against the live docs/ tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rections adopted, receipts verified
Adopted (all verified on main this pass):
- Cardinality reclassified UNEXPRESSIBLE -> RepresentableButForgeable, not
statically propagated: v2.std.refinement exists, NonEmptyList fixture +
green cardinality_fold_propagation_test exist, and
refined_vacuous_stub_pack's Rejected arm returns Refined { base } (the
carrier proves nothing). New Sec 4b: the operator independently
re-directed this exact guarantee on 2026-07-04
(interface-summary-declared-use-arity.md Sec 3.1, "hard error in the
language") — the intent is not lost; the lattice design pass (FLAG E)
never started.
- Failure history rewritten (Sec 2): the exemption dates to 2026-06-08
(a13fb57), pre-bankruptcy; correctness-dimensions.md marked type
safety "Yes (blocking)" while return position was unchecked — so the
ledger overstated, then the auditable contract was deleted. The
pipeline_steps_empty_arm_note receipt is withdrawn: empty there is a
deliberate total semantics, not a priced-out wall.
- Status vocabulary widened to the review's 11-state lattice; v2 terminal
calibrated (validate_then_compile door + loop-bound wall are real;
InferredTree is still not a proof boundary); application-arity row added
(formal-driven walk, positional fallback for misspelled labels,
ArityMismatch is constructor-arity); PatternLookupBlocked's silent []
arm confirmed (PatternDynamic does diagnose — review corrected there).
- Sec 7b: DESIGN.md is projected from gunbc.design_document, and its "5
behaviors" is stale against v2.std.node's six (Match) — the guarantee
authority lands as .dag rows, never hand-edited prose.
- Sequencing reconciled to 7 stages: claims authority + expecting-red
probe corpus together; zero-resolution method wall now, ambiguity wall
census-first; cardinality vertical slice third.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…el (review 45299) The first HandAuthoredDocBind trigger said "re-homed into DESIGN.md as its specification half" — wording that predates the reconciliation pass's Sec 7b finding that DESIGN.md is a projection of gunbc.design_document. As written, a direct DESIGN.md edit could have satisfied the trigger, which is exactly the Sec 3 parallel-representation failure Sec 7b names. Trigger now requires .dag claim rows projected via gunbc.design_document and states explicitly that a hand edit does not satisfy it. All five doc-reachability witnesses re-run green by execution after the edit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…the safety ladder as the organizing frame Review 45305, both findings verified correct and fixed: - doc_graph_roots: the two HandAuthoredDocBind rows shared (home, slug), which the carrier's own note defines as the symbolic identity — one doc had two independently removable authority rows. Merged to ONE row whose trigger anchors both carriers (module_skips_direct_call_arg_check, solve_constraints) and gates dissolution on BOTH conditions, with the merge provenance recorded on the carrier. (Observed, not fixed here: module-identity-storage-binding-design and accelerator-demo-roundtrip also carry same-slug duplicate rows — pre-existing, follow-up material.) - Sec 8b's example-0 block still said "unexpressible", contradicting the Sec 4 reclassification and mis-aiming the archetypal RED at inventing a carrier instead of sealing/propagating the one that exists. Rewritten: the RED exercises unforgeable construction + seam propagation, expected refusal at the 0..n -> 1..n seam. Operator direction, same pass: the safety ladder is now Sec 1b, the organizing frame — R3 structurally-impossible / R2 structural guarantee / R1 testable / R0 mitigatable / below-the-floor silent (forbidden, Sec 5). Three rules: floor absolute; climb to a STATED ceiling (mathematical / capability / price — the capability ceiling is unforgeable construction, blocked on reference-level visibility: the keyword set has no private/sealed/opaque); reported rung == measured rung, lens-checked for inflation and stalls. Includes the specimen table (the session's classes placed, cross-representation == as the exemplar full climb) and the non-goals roster (external reality, arbitrary predicates, budgets, optimality, self-governance, byte-identical self-emit — low ceilings BY DESIGN). Stage 1 claim rows gain current_rung / ceiling / next_rung_trigger. All five doc-reachability witnesses re-run green by execution after both file changes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…guarantee-ladder roadmap section
Corrections, each verified against main before adoption:
1. sole_constructor EXISTS (SoleConstructorViolation, sealed-record
specimen) — the DESIGN 4b capability claim ("no private/sealed/opaque
... every proof-carrier is presently forgeable") was false as stated;
corrected to an audited-status claim: sole_constructor is the
candidate wall, completeness for generic carriers unverified. The
earlier keyword-set inference is withdrawn in the Sec 10 ledger.
2. Subject grain: rung honesty is measured at a declared acceptance
boundary; a class's rung is the MINIMUM across in-scope paths (the
interpreter refuses the mislabeled call that order_typed_call_args
reorders for emission). DESIGN 4b meta-obligation 1 amended; Stage-1
carrier gains subject_grain/acceptance_boundary/compile_mode/
realization_target/covered_population.
3. Seed rungs demoted: return/data/generic, field-through-generics,
exhaustiveness, cardinality, full ==-class, and L4 all to
UnknownUnmeasured (compile admission proven is not runtime
disposition proven); census marked specimen-denominated; unknown-
method R0 scoped to the interpretation path.
4. Dissolution on climb amended in DESIGN 4b: production handling
dissolves; the RED + positive controls REMAIN enrolled as the
evidence the higher rung stays real.
5. HandAuthoredDocBind.work -> works: List<DeclarationRef> (40 rows +
witness-test fixture migrated); the guarantee-recovery row now
carries BOTH anchors typed, not one typed + one in prose. Carrier
note records that List admits [] — the exact cardinality gap the
ladder tracks — with the doc-graph witnesses as the interim wall.
6. cardinality_fold_propagation_test relabeled everywhere as manual
value-level specimens (length homomorphism over literals + runtime
refine_byte); "not new design" softened to the accurate scope
statement; the roadmap cardinality node re-briefed accordingly.
7. Sec 8c recast: TypeBinding carries two bespoke coordinates, not a
generic dimension mechanism; extension-vs-redesign is an open audit
question that roadmap pricing must carry.
8. Sec 1 "was not built" -> "never completed as an exhaustive
acceptance contract"; Sec 11 queue updated (correctness-dimensions
done; sole_constructor completeness audit added).
Additions (operator direction): ROADMAP gains the "Guarantee ladder —
climb plan (DESIGN 4b)" section — 13 sized, unowned, dispatchable nodes
in ticket format with dependency edges (probe corpus gates the four
floor walls; carrier gates cardinality slice, emitters, prevalence;
exemption removal gates on the call-shape + inhabitance walls). The
capability node is the sole_constructor completeness audit. State-vs-
work split recorded on the carrier: rung STATE lives in the Stage-1
claims carrier and is emitted (ladder-census-emitters node); roadmap
nodes track CLIMBS.
Verified by execution: main_wet regen (DESIGN.md + ROADMAP.md
projections, never hand-edited); drift 4/4; doc-graph 5/5; roadmap
authority 35/35, model 9/9, focus 12/12.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…bol fields, two-anchor pin, RED control review 45336 was correct: works had a typed carrier and zero readers — representation without a consumer is specification-without-execution (DESIGN 5 / E-10), the exact defect class the guarantee analysis documents, reproduced in its own fix. Consumers now executing in dag/test/claim/doc_reachability_witness_test: - doc_graph_binds_works_all_nonempty — an emptied works list reds - doc_graph_works_refs_carry_symbols — a ref stripped of module_path or decl_name reds - guarantee_recovery_bind_pins_both_anchors — deleting or renaming either of the two anchors (module_skips_direct_call_arg_check, solve_constraints) reds; row multiplicity pinned to one - doc_graph_works_empty_red_control — synthetic empty-works bind fails the predicate, proving the consumer discriminates Predicates live on the authority (gunbc.doc_graph_roots) so the witness consumes the carrier's own definition. Residue named on the carrier note: staleness against the live tree (a ref naming a decl that no longer exists) is NOT witnessed — v1.compiler.* is outside the witness compile pool, so ref-vs-tree resolution is exactly the feature:cited-symbol-resolution lens DESIGN 3 already names; the refs are symbolic citations and inherit that trigger. All 11 doc-reachability witnesses green by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
review 45336: confirmed and fixed in aa06080. The finding was exact — Executing consumers now enrolled in Residue, named on the carrier rather than absorbed: staleness against the live tree — a ref naming a decl that no longer exists — is not witnessed here, because All 11 doc-reachability witnesses green by execution. |
…name the target rung; current rung defers to the census review 45349, third correct catch in this lane: the census demoted method existence (R0 interpretation-path-only), inhabitance (UnknownUnmeasured), and cardinality (UnknownUnmeasured) — and the roadmap nodes, authored before the demotion pass, kept "R0 -> R2" headlines, re-inflating the same claims the same day at the canonical authority. The section's own note says rung STATE lives in the claims carrier, never these nodes; the headlines now name only the TARGET rung and point at the census for current state, per DESIGN 4b's minimum-across-paths rule. ROADMAP.md regenerated via main_wet; roadmap authority witnesses 35/35; drift witnesses 4/4, by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
review 45349: confirmed and fixed. The census demoted these three classes and the roadmap nodes — authored before the demotion pass — kept "R0 → R2" headlines, so the canonical roadmap re-inflated them the same day they were demoted; the section's own state-vs-work note already said rung state lives in the claims carrier, never these nodes. Headlines now name only the target rung and defer current state to the census explicitly ("current rung: the census — …", with the method node carrying the path-scoped claim: R0 proven on the interpretation path only, emission path unmeasured). ROADMAP.md regenerated via main_wet; roadmap authority 35/35 and drift 4/4 green by execution. Worth noting the pattern across this lane's three codex catches: rung inflation in the specimen table (review 45310), representation-without-consumer in the works carrier (review 45336), and now state restated at a second authority (review 45349) — each is the ladder's own honesty rule firing on the artifacts that define it. That is the intended failure mode of the discipline: the rules are catching their own author before they gate anyone else. |
…ruction; rung state derived, never stored Executes the operator's 10-item merge bar on #7489 plus reviews 45356/45367 and tidy-deer-730's measured receipts: - guarantee_ladder_section() deleted; 16 nodes + 23 edges enter declared_roadmap_nodes()/declared_roadmap_edges() via guarantee_ladder_nodes()/ guarantee_ladder_edges(), owner "compiler-guarantee" (lane identity, unbound until closing contracts). Page visibility is the typed focus policy (lane added to roadmap_focus_selection). rendered⊆declared∪derived witnessed with a synthetic-ghost RED. - Graph corrections: probe corpus → carrier → baseline-prevalence → walls; prevalence split baseline/residual; new floor-generic-field-constraint-wall and floor-method-ambiguity-wall nodes; primitive-identity-join is a PREREQUISITE of the general method wall (measured: kernel algebra profiles vs interpreter dispatch fork, tidy-deer-730 on gunbc#7484); cardinality ← sole_constructor audit edge; capability node repointed off the parked visibility-grants doc. - Tickets de-stated: no current-rung transcription anywhere; carrier ticket rewritten to the four-carrier split (Requirement/Path/Measurement/derived Disposition, minimum across paths, no stored rung field) — reconciled across §12 Stage 1, DESIGN §4b tail, and the roadmap node (review 45367); five recovered vocabularies kept orthogonal. - HandAuthoredDocBind: primary_work + additional_works (zero-anchor bind unwritable); empty-works RED deleted with its validation, residue named; duplicate (home,slug) rows merged; bind-identity uniqueness witnessed with a synthetic-duplicate RED. - Census: method-existence subject-grain receipt (narrow kernel wall, gunbc#7484); parser silent-separator below-floor row; §11 items 6-8; §10 fourth-pass ledger. Witnesses: roadmap 37/37 (2 new), identity 9/9, focus 12/12, model 9/9, drift 8/8, doc-graph 11/11. ROADMAP.md/DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Restructure landed at 2d836ed (plus the auto-swept 93b95d2 and the auto-heal regen dceeb89), executing the operator's 10-item merge bar and the two open REQUEST_CHANGES: The verdict's structural findings. The ladder section is gone as a rendering universe: review 45356 (owner: ""): every climb node now carries review 45367 (stored Graph corrections beyond the verdict's list: sequencing corrected by tidy-deer-730's measured receipts on gunbc#7484 — Construction over validation on the binds: Witness receipts: roadmap 37/37 · identity 9/9 · focus 12/12 · model 9/9 · drift 8/8 · doc-graph 11/11; ROADMAP.md regen byte-stable, DESIGN.md re-projected via — sent from cool-badger-514 |
…icket law witness_ticket_brief_budget_holds_and_reds red on the CI floor: the carrier, method-existence, and cardinality briefs ran 169/128/111 words. The old section-local placement had escaped this law entirely (the exact ghost-universe defect the verdict named — the budget never saw those nodes); in the declared graph it applies. Briefs trimmed to 94/91/90 with every cut fact already carried in the gap analysis (sec 12 Stage 1b / Stage 2 amendment / the census), which each node links as its carrier. The budget itself is untouched — widening the declaration to satisfy the check is the DESIGN 5 tell, backwards. Page set 28/28, authority set green, regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
review 45406 verified and fixed at c0ac6e8: the containment wall now checks WHOLE-VALUE membership — a rendered node must be value-equal to a declared node or a projection-derived closing-contract task, so an altered copy reusing a declared identity counts as a ghost instead of passing as sanctioned. Added the altered-copy RED the review asked for: the probe pulls the real declared ladder-claims-carrier node, rebuilds it with one field changed (derived from the canonical node, so the probe duplicates no literals), renders it in a synthetic section, and the witness asserts exactly one ghost; it returns 0 (failing loudly) if the anchor node ever disappears. Authority set 38/38 including both REDs (fresh-identity ghost + altered copy). The containment note records the identity-only first cut as the refused shape. — sent from cool-badger-514 |
…r (review 45412) document_rendered_nodes was a traversal fork beside roadmap_spawner's doc_all_nodes — same semantics, second walker. The predicates (whole-value ghost count + both RED probes) move INTO roadmap_spawner, the walker's module, because the spawner already imports roadmap_authority and the reverse import would cycle. The authority sheds the walker and its now-unused SectionElement imports; the containment note records both refused first cuts (identity-only membership, review 45406; the duplicate walker, review 45412) since each was this wall violating a law it enforces. Authority 38/38, spawner 16/16, page 28/28. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
review 45412 verified and fixed at cd3d4bb: the hand-rolled document_rendered_nodes walker is deleted and the containment predicates (whole-value ghost count + both RED probes) now consume doc_all_nodes, the canonical traversal. They moved into gunbc.roadmap_spawner — the walker's own module — because the spawner already imports roadmap_authority, so importing the walker back into the authority would cycle; the test consumes the predicates from the spawner. The containment note now records both refused first cuts (identity-only membership from review 45406, and this walker fork) since each was the wall violating a law it enforces. Net diff is -6 lines. Receipts: authority 38/38, spawner 16/16, page 28/28. — sent from cool-badger-514 |
…ne, FrontierAccepted, and the closure door Executes all six items of the operator's post-merge verdict on #7489, each verified against live state first (#7484 and #7485 confirmed OPEN; the anchor confirmed as the #7489 squash; Behavior confirmed six-membered): 1. Every "#7484 landed" claim replaced with open-candidate wording — main's disposition stated separately from candidate branch evidence (the ladder's rung-inflation rule applied to open-PR state; my transcription error). 2. Baseline prevalence anchored: anchor_commit 6c6e2dc (content-addressed, reproducible after in-flight merges; walls no longer race a live tree). 3. GuaranteeDisposition gains FrontierAccepted{diagnostic, accepted_boundary, evidence} — typed/located/counted but still Accepted; specimens MethodExistenceUndecided and GroundingNotDerived. 4. Graph: floor-parse-formation-wall + floor-record-construction-wall + compiler-accepted-obligation-closure added; v2-phase-carriers split into five staged nodes (self-grounding frontier → Translate refusal → inferred- tree completeness → per-kind derivation coverage → target realization gate) with the registry's FIRST TOMBSTONE (superseded_by the frontier node); method←join edge deleted per the zero-via-union nuance (join gates only the >1 wall and realization completeness); residual reroutes through the closure door. 5. DESIGN §4: closed vocabulary corrected to 6 connectives + 6 behaviors, matching v2.std.node.Behavior (the decidability denominator). 6. §1d provisional guarantee grid emitted as hand-authored interim, dissolve-on the carrier-emitted projection. Witnesses: authority 38/38, identity 9/9 (first tombstone passes the count-free tombstone claims), focus 12/12, model 9/9, page 28/28 (all 23 ladder briefs within the 100-word law), spawner 16/16, drift 8/8, doc 11/11. ROADMAP.md and DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…cepted, closure door, v2 split (post-merge verdict) (#7500) * WIP: compiler correctness * Bind the guarantee-recovery analysis into the doc graph The analysis note landed as an orphan doc: gunbc.doc_graph_roots states that "an unbound doc is an orphan, loudly", and CI duly refused at be1a001 with doc_graph_has_no_orphan_docs returning false in both the dag/test/claim and src/v2/lens consumers. Registered as two HandAuthoredDocBind rows rather than one, because the analysis binds to two independent carriers and they dissolve on different triggers: - v1.compiler.infer module_skips_direct_call_arg_check — the one named violation of the dimension contract's "no escape hatch" clause (docs/thesis/correctness-dimensions.md), exempting v2.* and v1.compiler.* from direct-call argument checking. - v2.std.constraints solve_constraints — passes graph.root as source_facts, algebra AND the sole candidate, so the grounding proof reduces to well_formed(root) and is relabelled CanonicalGrounding. Green by execution, both directions: RED is the CI failure at be1a001; GREEN is all five witnesses in dag/test/claim/doc_reachability_witness_test.dag plus doc_graph_is_clean in src/v2/lens/doc_reachability_test.dag passing locally against the live docs/ tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Reconcile the gap analysis against the independent review — three corrections adopted, receipts verified Adopted (all verified on main this pass): - Cardinality reclassified UNEXPRESSIBLE -> RepresentableButForgeable, not statically propagated: v2.std.refinement exists, NonEmptyList fixture + green cardinality_fold_propagation_test exist, and refined_vacuous_stub_pack's Rejected arm returns Refined { base } (the carrier proves nothing). New Sec 4b: the operator independently re-directed this exact guarantee on 2026-07-04 (interface-summary-declared-use-arity.md Sec 3.1, "hard error in the language") — the intent is not lost; the lattice design pass (FLAG E) never started. - Failure history rewritten (Sec 2): the exemption dates to 2026-06-08 (a13fb57), pre-bankruptcy; correctness-dimensions.md marked type safety "Yes (blocking)" while return position was unchecked — so the ledger overstated, then the auditable contract was deleted. The pipeline_steps_empty_arm_note receipt is withdrawn: empty there is a deliberate total semantics, not a priced-out wall. - Status vocabulary widened to the review's 11-state lattice; v2 terminal calibrated (validate_then_compile door + loop-bound wall are real; InferredTree is still not a proof boundary); application-arity row added (formal-driven walk, positional fallback for misspelled labels, ArityMismatch is constructor-arity); PatternLookupBlocked's silent [] arm confirmed (PatternDynamic does diagnose — review corrected there). - Sec 7b: DESIGN.md is projected from gunbc.design_document, and its "5 behaviors" is stale against v2.std.node's six (Match) — the guarantee authority lands as .dag rows, never hand-edited prose. - Sequencing reconciled to 7 stages: claims authority + expecting-red probe corpus together; zero-resolution method wall now, ambiguity wall census-first; cardinality vertical slice third. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Status header: two audit passes complete, open items typed Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Align the bind's dissolution trigger with the doc's own authority model (review 45299) The first HandAuthoredDocBind trigger said "re-homed into DESIGN.md as its specification half" — wording that predates the reconciliation pass's Sec 7b finding that DESIGN.md is a projection of gunbc.design_document. As written, a direct DESIGN.md edit could have satisfied the trigger, which is exactly the Sec 3 parallel-representation failure Sec 7b names. Trigger now requires .dag claim rows projected via gunbc.design_document and states explicitly that a hand edit does not satisfy it. All five doc-reachability witnesses re-run green by execution after the edit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Address review 45305 (merge same-slug binds, fix stale block) + land the safety ladder as the organizing frame Review 45305, both findings verified correct and fixed: - doc_graph_roots: the two HandAuthoredDocBind rows shared (home, slug), which the carrier's own note defines as the symbolic identity — one doc had two independently removable authority rows. Merged to ONE row whose trigger anchors both carriers (module_skips_direct_call_arg_check, solve_constraints) and gates dissolution on BOTH conditions, with the merge provenance recorded on the carrier. (Observed, not fixed here: module-identity-storage-binding-design and accelerator-demo-roundtrip also carry same-slug duplicate rows — pre-existing, follow-up material.) - Sec 8b's example-0 block still said "unexpressible", contradicting the Sec 4 reclassification and mis-aiming the archetypal RED at inventing a carrier instead of sealing/propagating the one that exists. Rewritten: the RED exercises unforgeable construction + seam propagation, expected refusal at the 0..n -> 1..n seam. Operator direction, same pass: the safety ladder is now Sec 1b, the organizing frame — R3 structurally-impossible / R2 structural guarantee / R1 testable / R0 mitigatable / below-the-floor silent (forbidden, Sec 5). Three rules: floor absolute; climb to a STATED ceiling (mathematical / capability / price — the capability ceiling is unforgeable construction, blocked on reference-level visibility: the keyword set has no private/sealed/opaque); reported rung == measured rung, lens-checked for inflation and stalls. Includes the specimen table (the session's classes placed, cross-representation == as the exemplar full climb) and the non-goals roster (external reality, arbitrary predicates, budgets, optimality, self-governance, byte-identical self-emit — low ceilings BY DESIGN). Stage 1 claim rows gain current_rung / ceiling / next_rung_trigger. All five doc-reachability witnesses re-run green by execution after both file changes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * WIP: compiler correctness * Ladder follow-up: adopt the post-merge verdict (8 corrections) + the guarantee-ladder roadmap section Corrections, each verified against main before adoption: 1. sole_constructor EXISTS (SoleConstructorViolation, sealed-record specimen) — the DESIGN 4b capability claim ("no private/sealed/opaque ... every proof-carrier is presently forgeable") was false as stated; corrected to an audited-status claim: sole_constructor is the candidate wall, completeness for generic carriers unverified. The earlier keyword-set inference is withdrawn in the Sec 10 ledger. 2. Subject grain: rung honesty is measured at a declared acceptance boundary; a class's rung is the MINIMUM across in-scope paths (the interpreter refuses the mislabeled call that order_typed_call_args reorders for emission). DESIGN 4b meta-obligation 1 amended; Stage-1 carrier gains subject_grain/acceptance_boundary/compile_mode/ realization_target/covered_population. 3. Seed rungs demoted: return/data/generic, field-through-generics, exhaustiveness, cardinality, full ==-class, and L4 all to UnknownUnmeasured (compile admission proven is not runtime disposition proven); census marked specimen-denominated; unknown- method R0 scoped to the interpretation path. 4. Dissolution on climb amended in DESIGN 4b: production handling dissolves; the RED + positive controls REMAIN enrolled as the evidence the higher rung stays real. 5. HandAuthoredDocBind.work -> works: List<DeclarationRef> (40 rows + witness-test fixture migrated); the guarantee-recovery row now carries BOTH anchors typed, not one typed + one in prose. Carrier note records that List admits [] — the exact cardinality gap the ladder tracks — with the doc-graph witnesses as the interim wall. 6. cardinality_fold_propagation_test relabeled everywhere as manual value-level specimens (length homomorphism over literals + runtime refine_byte); "not new design" softened to the accurate scope statement; the roadmap cardinality node re-briefed accordingly. 7. Sec 8c recast: TypeBinding carries two bespoke coordinates, not a generic dimension mechanism; extension-vs-redesign is an open audit question that roadmap pricing must carry. 8. Sec 1 "was not built" -> "never completed as an exhaustive acceptance contract"; Sec 11 queue updated (correctness-dimensions done; sole_constructor completeness audit added). Additions (operator direction): ROADMAP gains the "Guarantee ladder — climb plan (DESIGN 4b)" section — 13 sized, unowned, dispatchable nodes in ticket format with dependency edges (probe corpus gates the four floor walls; carrier gates cardinality slice, emitters, prevalence; exemption removal gates on the call-shape + inhabitance walls). The capability node is the sole_constructor completeness audit. State-vs- work split recorded on the carrier: rung STATE lives in the Stage-1 claims carrier and is emitted (ladder-census-emitters node); roadmap nodes track CLIMBS. Verified by execution: main_wet regen (DESIGN.md + ROADMAP.md projections, never hand-edited); drift 4/4; doc-graph 5/5; roadmap authority 35/35, model 9/9, focus 12/12. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give works its executing consumers (review 45336): nonempty wall, symbol fields, two-anchor pin, RED control review 45336 was correct: works had a typed carrier and zero readers — representation without a consumer is specification-without-execution (DESIGN 5 / E-10), the exact defect class the guarantee analysis documents, reproduced in its own fix. Consumers now executing in dag/test/claim/doc_reachability_witness_test: - doc_graph_binds_works_all_nonempty — an emptied works list reds - doc_graph_works_refs_carry_symbols — a ref stripped of module_path or decl_name reds - guarantee_recovery_bind_pins_both_anchors — deleting or renaming either of the two anchors (module_skips_direct_call_arg_check, solve_constraints) reds; row multiplicity pinned to one - doc_graph_works_empty_red_control — synthetic empty-works bind fails the predicate, proving the consumer discriminates Predicates live on the authority (gunbc.doc_graph_roots) so the witness consumes the carrier's own definition. Residue named on the carrier note: staleness against the live tree (a ref naming a decl that no longer exists) is NOT witnessed — v1.compiler.* is outside the witness compile pool, so ref-vs-tree resolution is exactly the feature:cited-symbol-resolution lens DESIGN 3 already names; the refs are symbolic citations and inherit that trigger. All 11 doc-reachability witnesses green by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * De-inflate the three climb-node headlines (review 45349): work nodes name the target rung; current rung defers to the census review 45349, third correct catch in this lane: the census demoted method existence (R0 interpretation-path-only), inhabitance (UnknownUnmeasured), and cardinality (UnknownUnmeasured) — and the roadmap nodes, authored before the demotion pass, kept "R0 -> R2" headlines, re-inflating the same claims the same day at the canonical authority. The section's own note says rung STATE lives in the claims carrier, never these nodes; the headlines now name only the TARGET rung and point at the census for current state, per DESIGN 4b's minimum-across-paths rule. ROADMAP.md regenerated via main_wet; roadmap authority witnesses 35/35; drift witnesses 4/4, by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * chore: regenerate drifted generated artifacts (ci auto-heal) * Ladder nodes join the declared roadmap graph; binds nonempty by construction; rung state derived, never stored Executes the operator's 10-item merge bar on #7489 plus reviews 45356/45367 and tidy-deer-730's measured receipts: - guarantee_ladder_section() deleted; 16 nodes + 23 edges enter declared_roadmap_nodes()/declared_roadmap_edges() via guarantee_ladder_nodes()/ guarantee_ladder_edges(), owner "compiler-guarantee" (lane identity, unbound until closing contracts). Page visibility is the typed focus policy (lane added to roadmap_focus_selection). rendered⊆declared∪derived witnessed with a synthetic-ghost RED. - Graph corrections: probe corpus → carrier → baseline-prevalence → walls; prevalence split baseline/residual; new floor-generic-field-constraint-wall and floor-method-ambiguity-wall nodes; primitive-identity-join is a PREREQUISITE of the general method wall (measured: kernel algebra profiles vs interpreter dispatch fork, tidy-deer-730 on gunbc#7484); cardinality ← sole_constructor audit edge; capability node repointed off the parked visibility-grants doc. - Tickets de-stated: no current-rung transcription anywhere; carrier ticket rewritten to the four-carrier split (Requirement/Path/Measurement/derived Disposition, minimum across paths, no stored rung field) — reconciled across §12 Stage 1, DESIGN §4b tail, and the roadmap node (review 45367); five recovered vocabularies kept orthogonal. - HandAuthoredDocBind: primary_work + additional_works (zero-anchor bind unwritable); empty-works RED deleted with its validation, residue named; duplicate (home,slug) rows merged; bind-identity uniqueness witnessed with a synthetic-duplicate RED. - Census: method-existence subject-grain receipt (narrow kernel wall, gunbc#7484); parser silent-separator below-floor row; §11 items 6-8; §10 fourth-pass ledger. Witnesses: roadmap 37/37 (2 new), identity 9/9, focus 12/12, model 9/9, drift 8/8, doc-graph 11/11. ROADMAP.md/DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Trim the three over-budget ladder briefs to the operator's 100-word ticket law witness_ticket_brief_budget_holds_and_reds red on the CI floor: the carrier, method-existence, and cardinality briefs ran 169/128/111 words. The old section-local placement had escaped this law entirely (the exact ghost-universe defect the verdict named — the budget never saw those nodes); in the declared graph it applies. Briefs trimmed to 94/91/90 with every cut fact already carried in the gap analysis (sec 12 Stage 1b / Stage 2 amendment / the census), which each node links as its carrier. The budget itself is untouched — widening the declaration to satisfy the check is the DESIGN 5 tell, backwards. Page set 28/28, authority set green, regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Containment predicates consume doc_all_nodes, the one canonical walker (review 45412) document_rendered_nodes was a traversal fork beside roadmap_spawner's doc_all_nodes — same semantics, second walker. The predicates (whole-value ghost count + both RED probes) move INTO roadmap_spawner, the walker's module, because the spawner already imports roadmap_authority and the reverse import would cycle. The authority sheds the walker and its now-unused SectionElement imports; the containment note records both refused first cuts (identity-only membership, review 45406; the duplicate walker, review 45412) since each was this wall violating a law it enforces. Authority 38/38, spawner 16/16, page 28/28. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Post-merge verdict follow-up: open-candidate honesty, anchored baseline, FrontierAccepted, and the closure door Executes all six items of the operator's post-merge verdict on #7489, each verified against live state first (#7484 and #7485 confirmed OPEN; the anchor confirmed as the #7489 squash; Behavior confirmed six-membered): 1. Every "#7484 landed" claim replaced with open-candidate wording — main's disposition stated separately from candidate branch evidence (the ladder's rung-inflation rule applied to open-PR state; my transcription error). 2. Baseline prevalence anchored: anchor_commit 6c6e2dc (content-addressed, reproducible after in-flight merges; walls no longer race a live tree). 3. GuaranteeDisposition gains FrontierAccepted{diagnostic, accepted_boundary, evidence} — typed/located/counted but still Accepted; specimens MethodExistenceUndecided and GroundingNotDerived. 4. Graph: floor-parse-formation-wall + floor-record-construction-wall + compiler-accepted-obligation-closure added; v2-phase-carriers split into five staged nodes (self-grounding frontier → Translate refusal → inferred- tree completeness → per-kind derivation coverage → target realization gate) with the registry's FIRST TOMBSTONE (superseded_by the frontier node); method←join edge deleted per the zero-via-union nuance (join gates only the >1 wall and realization completeness); residual reroutes through the closure door. 5. DESIGN §4: closed vocabulary corrected to 6 connectives + 6 behaviors, matching v2.std.node.Behavior (the decidability denominator). 6. §1d provisional guarantee grid emitted as hand-authored interim, dissolve-on the carrier-emitted projection. Witnesses: authority 38/38, identity 9/9 (first tombstone passes the count-free tombstone claims), focus 12/12, model 9/9, page 28/28 (all 23 ladder briefs within the 100-word law), spawner 16/16, drift 8/8, doc 11/11. ROADMAP.md and DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * chore: regenerate drifted generated artifacts (ci auto-heal) * Route the ambiguity wall and cardinality seam through the closure door (review 45545) The first edge set let compiler-accepted-obligation-closure land while floor-method-ambiguity-wall and cardinality-vertical-slice stayed open — the door would have certified "every required judgment established" over two required-open judgments (the grid marks the cardinality seam P0.2 minimum-R2 and ambiguity part of resolved identity; the verdict's spine routes ALL P0 obligations through the door). Both are now prerequisites of the closure; residual prevalence depends on the door alone. Authority 38/38, focus 12/12, page 28/28, drift 8/8; regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Reconcile the sec-7b behavior-count passage to past tense (review 45558) Sec 7b still described the 5-behaviors drift as current after this PR corrected the authority — the stale-claim problem the PR closes elsewhere. The passage now records the drift as found-and-corrected, keeps the specimen's evidentiary value (the denominator drifted silently in prose), and leaves the Match-promotion adjudication question with the queue. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
…ls at the direct-call seam (#7519) * WIP: compiler correctness * Bind the guarantee-recovery analysis into the doc graph The analysis note landed as an orphan doc: gunbc.doc_graph_roots states that "an unbound doc is an orphan, loudly", and CI duly refused at be1a001 with doc_graph_has_no_orphan_docs returning false in both the dag/test/claim and src/v2/lens consumers. Registered as two HandAuthoredDocBind rows rather than one, because the analysis binds to two independent carriers and they dissolve on different triggers: - v1.compiler.infer module_skips_direct_call_arg_check — the one named violation of the dimension contract's "no escape hatch" clause (docs/thesis/correctness-dimensions.md), exempting v2.* and v1.compiler.* from direct-call argument checking. - v2.std.constraints solve_constraints — passes graph.root as source_facts, algebra AND the sole candidate, so the grounding proof reduces to well_formed(root) and is relabelled CanonicalGrounding. Green by execution, both directions: RED is the CI failure at be1a001; GREEN is all five witnesses in dag/test/claim/doc_reachability_witness_test.dag plus doc_graph_is_clean in src/v2/lens/doc_reachability_test.dag passing locally against the live docs/ tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Reconcile the gap analysis against the independent review — three corrections adopted, receipts verified Adopted (all verified on main this pass): - Cardinality reclassified UNEXPRESSIBLE -> RepresentableButForgeable, not statically propagated: v2.std.refinement exists, NonEmptyList fixture + green cardinality_fold_propagation_test exist, and refined_vacuous_stub_pack's Rejected arm returns Refined { base } (the carrier proves nothing). New Sec 4b: the operator independently re-directed this exact guarantee on 2026-07-04 (interface-summary-declared-use-arity.md Sec 3.1, "hard error in the language") — the intent is not lost; the lattice design pass (FLAG E) never started. - Failure history rewritten (Sec 2): the exemption dates to 2026-06-08 (a13fb57), pre-bankruptcy; correctness-dimensions.md marked type safety "Yes (blocking)" while return position was unchecked — so the ledger overstated, then the auditable contract was deleted. The pipeline_steps_empty_arm_note receipt is withdrawn: empty there is a deliberate total semantics, not a priced-out wall. - Status vocabulary widened to the review's 11-state lattice; v2 terminal calibrated (validate_then_compile door + loop-bound wall are real; InferredTree is still not a proof boundary); application-arity row added (formal-driven walk, positional fallback for misspelled labels, ArityMismatch is constructor-arity); PatternLookupBlocked's silent [] arm confirmed (PatternDynamic does diagnose — review corrected there). - Sec 7b: DESIGN.md is projected from gunbc.design_document, and its "5 behaviors" is stale against v2.std.node's six (Match) — the guarantee authority lands as .dag rows, never hand-edited prose. - Sequencing reconciled to 7 stages: claims authority + expecting-red probe corpus together; zero-resolution method wall now, ambiguity wall census-first; cardinality vertical slice third. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Status header: two audit passes complete, open items typed Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Align the bind's dissolution trigger with the doc's own authority model (review 45299) The first HandAuthoredDocBind trigger said "re-homed into DESIGN.md as its specification half" — wording that predates the reconciliation pass's Sec 7b finding that DESIGN.md is a projection of gunbc.design_document. As written, a direct DESIGN.md edit could have satisfied the trigger, which is exactly the Sec 3 parallel-representation failure Sec 7b names. Trigger now requires .dag claim rows projected via gunbc.design_document and states explicitly that a hand edit does not satisfy it. All five doc-reachability witnesses re-run green by execution after the edit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Address review 45305 (merge same-slug binds, fix stale block) + land the safety ladder as the organizing frame Review 45305, both findings verified correct and fixed: - doc_graph_roots: the two HandAuthoredDocBind rows shared (home, slug), which the carrier's own note defines as the symbolic identity — one doc had two independently removable authority rows. Merged to ONE row whose trigger anchors both carriers (module_skips_direct_call_arg_check, solve_constraints) and gates dissolution on BOTH conditions, with the merge provenance recorded on the carrier. (Observed, not fixed here: module-identity-storage-binding-design and accelerator-demo-roundtrip also carry same-slug duplicate rows — pre-existing, follow-up material.) - Sec 8b's example-0 block still said "unexpressible", contradicting the Sec 4 reclassification and mis-aiming the archetypal RED at inventing a carrier instead of sealing/propagating the one that exists. Rewritten: the RED exercises unforgeable construction + seam propagation, expected refusal at the 0..n -> 1..n seam. Operator direction, same pass: the safety ladder is now Sec 1b, the organizing frame — R3 structurally-impossible / R2 structural guarantee / R1 testable / R0 mitigatable / below-the-floor silent (forbidden, Sec 5). Three rules: floor absolute; climb to a STATED ceiling (mathematical / capability / price — the capability ceiling is unforgeable construction, blocked on reference-level visibility: the keyword set has no private/sealed/opaque); reported rung == measured rung, lens-checked for inflation and stalls. Includes the specimen table (the session's classes placed, cross-representation == as the exemplar full climb) and the non-goals roster (external reality, arbitrary predicates, budgets, optimality, self-governance, byte-identical self-emit — low ceilings BY DESIGN). Stage 1 claim rows gain current_rung / ceiling / next_rung_trigger. All five doc-reachability witnesses re-run green by execution after both file changes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * WIP: compiler correctness * Ladder follow-up: adopt the post-merge verdict (8 corrections) + the guarantee-ladder roadmap section Corrections, each verified against main before adoption: 1. sole_constructor EXISTS (SoleConstructorViolation, sealed-record specimen) — the DESIGN 4b capability claim ("no private/sealed/opaque ... every proof-carrier is presently forgeable") was false as stated; corrected to an audited-status claim: sole_constructor is the candidate wall, completeness for generic carriers unverified. The earlier keyword-set inference is withdrawn in the Sec 10 ledger. 2. Subject grain: rung honesty is measured at a declared acceptance boundary; a class's rung is the MINIMUM across in-scope paths (the interpreter refuses the mislabeled call that order_typed_call_args reorders for emission). DESIGN 4b meta-obligation 1 amended; Stage-1 carrier gains subject_grain/acceptance_boundary/compile_mode/ realization_target/covered_population. 3. Seed rungs demoted: return/data/generic, field-through-generics, exhaustiveness, cardinality, full ==-class, and L4 all to UnknownUnmeasured (compile admission proven is not runtime disposition proven); census marked specimen-denominated; unknown- method R0 scoped to the interpretation path. 4. Dissolution on climb amended in DESIGN 4b: production handling dissolves; the RED + positive controls REMAIN enrolled as the evidence the higher rung stays real. 5. HandAuthoredDocBind.work -> works: List<DeclarationRef> (40 rows + witness-test fixture migrated); the guarantee-recovery row now carries BOTH anchors typed, not one typed + one in prose. Carrier note records that List admits [] — the exact cardinality gap the ladder tracks — with the doc-graph witnesses as the interim wall. 6. cardinality_fold_propagation_test relabeled everywhere as manual value-level specimens (length homomorphism over literals + runtime refine_byte); "not new design" softened to the accurate scope statement; the roadmap cardinality node re-briefed accordingly. 7. Sec 8c recast: TypeBinding carries two bespoke coordinates, not a generic dimension mechanism; extension-vs-redesign is an open audit question that roadmap pricing must carry. 8. Sec 1 "was not built" -> "never completed as an exhaustive acceptance contract"; Sec 11 queue updated (correctness-dimensions done; sole_constructor completeness audit added). Additions (operator direction): ROADMAP gains the "Guarantee ladder — climb plan (DESIGN 4b)" section — 13 sized, unowned, dispatchable nodes in ticket format with dependency edges (probe corpus gates the four floor walls; carrier gates cardinality slice, emitters, prevalence; exemption removal gates on the call-shape + inhabitance walls). The capability node is the sole_constructor completeness audit. State-vs- work split recorded on the carrier: rung STATE lives in the Stage-1 claims carrier and is emitted (ladder-census-emitters node); roadmap nodes track CLIMBS. Verified by execution: main_wet regen (DESIGN.md + ROADMAP.md projections, never hand-edited); drift 4/4; doc-graph 5/5; roadmap authority 35/35, model 9/9, focus 12/12. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give works its executing consumers (review 45336): nonempty wall, symbol fields, two-anchor pin, RED control review 45336 was correct: works had a typed carrier and zero readers — representation without a consumer is specification-without-execution (DESIGN 5 / E-10), the exact defect class the guarantee analysis documents, reproduced in its own fix. Consumers now executing in dag/test/claim/doc_reachability_witness_test: - doc_graph_binds_works_all_nonempty — an emptied works list reds - doc_graph_works_refs_carry_symbols — a ref stripped of module_path or decl_name reds - guarantee_recovery_bind_pins_both_anchors — deleting or renaming either of the two anchors (module_skips_direct_call_arg_check, solve_constraints) reds; row multiplicity pinned to one - doc_graph_works_empty_red_control — synthetic empty-works bind fails the predicate, proving the consumer discriminates Predicates live on the authority (gunbc.doc_graph_roots) so the witness consumes the carrier's own definition. Residue named on the carrier note: staleness against the live tree (a ref naming a decl that no longer exists) is NOT witnessed — v1.compiler.* is outside the witness compile pool, so ref-vs-tree resolution is exactly the feature:cited-symbol-resolution lens DESIGN 3 already names; the refs are symbolic citations and inherit that trigger. All 11 doc-reachability witnesses green by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * De-inflate the three climb-node headlines (review 45349): work nodes name the target rung; current rung defers to the census review 45349, third correct catch in this lane: the census demoted method existence (R0 interpretation-path-only), inhabitance (UnknownUnmeasured), and cardinality (UnknownUnmeasured) — and the roadmap nodes, authored before the demotion pass, kept "R0 -> R2" headlines, re-inflating the same claims the same day at the canonical authority. The section's own note says rung STATE lives in the claims carrier, never these nodes; the headlines now name only the TARGET rung and point at the census for current state, per DESIGN 4b's minimum-across-paths rule. ROADMAP.md regenerated via main_wet; roadmap authority witnesses 35/35; drift witnesses 4/4, by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * chore: regenerate drifted generated artifacts (ci auto-heal) * Ladder nodes join the declared roadmap graph; binds nonempty by construction; rung state derived, never stored Executes the operator's 10-item merge bar on #7489 plus reviews 45356/45367 and tidy-deer-730's measured receipts: - guarantee_ladder_section() deleted; 16 nodes + 23 edges enter declared_roadmap_nodes()/declared_roadmap_edges() via guarantee_ladder_nodes()/ guarantee_ladder_edges(), owner "compiler-guarantee" (lane identity, unbound until closing contracts). Page visibility is the typed focus policy (lane added to roadmap_focus_selection). rendered⊆declared∪derived witnessed with a synthetic-ghost RED. - Graph corrections: probe corpus → carrier → baseline-prevalence → walls; prevalence split baseline/residual; new floor-generic-field-constraint-wall and floor-method-ambiguity-wall nodes; primitive-identity-join is a PREREQUISITE of the general method wall (measured: kernel algebra profiles vs interpreter dispatch fork, tidy-deer-730 on gunbc#7484); cardinality ← sole_constructor audit edge; capability node repointed off the parked visibility-grants doc. - Tickets de-stated: no current-rung transcription anywhere; carrier ticket rewritten to the four-carrier split (Requirement/Path/Measurement/derived Disposition, minimum across paths, no stored rung field) — reconciled across §12 Stage 1, DESIGN §4b tail, and the roadmap node (review 45367); five recovered vocabularies kept orthogonal. - HandAuthoredDocBind: primary_work + additional_works (zero-anchor bind unwritable); empty-works RED deleted with its validation, residue named; duplicate (home,slug) rows merged; bind-identity uniqueness witnessed with a synthetic-duplicate RED. - Census: method-existence subject-grain receipt (narrow kernel wall, gunbc#7484); parser silent-separator below-floor row; §11 items 6-8; §10 fourth-pass ledger. Witnesses: roadmap 37/37 (2 new), identity 9/9, focus 12/12, model 9/9, drift 8/8, doc-graph 11/11. ROADMAP.md/DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Trim the three over-budget ladder briefs to the operator's 100-word ticket law witness_ticket_brief_budget_holds_and_reds red on the CI floor: the carrier, method-existence, and cardinality briefs ran 169/128/111 words. The old section-local placement had escaped this law entirely (the exact ghost-universe defect the verdict named — the budget never saw those nodes); in the declared graph it applies. Briefs trimmed to 94/91/90 with every cut fact already carried in the gap analysis (sec 12 Stage 1b / Stage 2 amendment / the census), which each node links as its carrier. The budget itself is untouched — widening the declaration to satisfy the check is the DESIGN 5 tell, backwards. Page set 28/28, authority set green, regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Containment predicates consume doc_all_nodes, the one canonical walker (review 45412) document_rendered_nodes was a traversal fork beside roadmap_spawner's doc_all_nodes — same semantics, second walker. The predicates (whole-value ghost count + both RED probes) move INTO roadmap_spawner, the walker's module, because the spawner already imports roadmap_authority and the reverse import would cycle. The authority sheds the walker and its now-unused SectionElement imports; the containment note records both refused first cuts (identity-only membership, review 45406; the duplicate walker, review 45412) since each was this wall violating a law it enforces. Authority 38/38, spawner 16/16, page 28/28. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Post-merge verdict follow-up: open-candidate honesty, anchored baseline, FrontierAccepted, and the closure door Executes all six items of the operator's post-merge verdict on #7489, each verified against live state first (#7484 and #7485 confirmed OPEN; the anchor confirmed as the #7489 squash; Behavior confirmed six-membered): 1. Every "#7484 landed" claim replaced with open-candidate wording — main's disposition stated separately from candidate branch evidence (the ladder's rung-inflation rule applied to open-PR state; my transcription error). 2. Baseline prevalence anchored: anchor_commit 6c6e2dc (content-addressed, reproducible after in-flight merges; walls no longer race a live tree). 3. GuaranteeDisposition gains FrontierAccepted{diagnostic, accepted_boundary, evidence} — typed/located/counted but still Accepted; specimens MethodExistenceUndecided and GroundingNotDerived. 4. Graph: floor-parse-formation-wall + floor-record-construction-wall + compiler-accepted-obligation-closure added; v2-phase-carriers split into five staged nodes (self-grounding frontier → Translate refusal → inferred- tree completeness → per-kind derivation coverage → target realization gate) with the registry's FIRST TOMBSTONE (superseded_by the frontier node); method←join edge deleted per the zero-via-union nuance (join gates only the >1 wall and realization completeness); residual reroutes through the closure door. 5. DESIGN §4: closed vocabulary corrected to 6 connectives + 6 behaviors, matching v2.std.node.Behavior (the decidability denominator). 6. §1d provisional guarantee grid emitted as hand-authored interim, dissolve-on the carrier-emitted projection. Witnesses: authority 38/38, identity 9/9 (first tombstone passes the count-free tombstone claims), focus 12/12, model 9/9, page 28/28 (all 23 ladder briefs within the 100-word law), spawner 16/16, drift 8/8, doc 11/11. ROADMAP.md and DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * chore: regenerate drifted generated artifacts (ci auto-heal) * Route the ambiguity wall and cardinality seam through the closure door (review 45545) The first edge set let compiler-accepted-obligation-closure land while floor-method-ambiguity-wall and cardinality-vertical-slice stayed open — the door would have certified "every required judgment established" over two required-open judgments (the grid marks the cardinality seam P0.2 minimum-R2 and ambiguity part of resolved identity; the verdict's spine routes ALL P0 obligations through the door). Both are now prerequisites of the closure; residual prevalence depends on the door alone. Authority 38/38, focus 12/12, page 28/28, drift 8/8; regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Reconcile the sec-7b behavior-count passage to past tense (review 45558) Sec 7b still described the 5-behaviors drift as current after this PR corrected the authority — the stale-claim problem the PR closes elsewhere. The passage now records the drift as found-and-corrected, keeps the specimen's evidentiary value (the denominator drifted silently in prose), and leaves the Match-promotion adjudication question with the queue. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Remove probe demo scaffolding (net-zero vs main: files added by autocommit sweep mid-run, deleted after measurement) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Call-shape wall: refuse unknown argument labels and surplus positionals at the direct-call seam, mirroring the runtime contract The compile seam was silent on both classes call_function_inner refuses at runtime, and the emitter reordered mislabeled args positionally — two realizations of one program disagreeing silently. direct_call_shape_diags (v1.compiler.infer) closes both, blocking, exemption-free (a label has no representation gap). Census before landing refused 28 live rename fossils in 5 fns (to_string i->value, arm_body, is_import_slot_node, fold_list init->empty, path->path_opt), all relabeled to their declared authority; +3 fixed in the measured sig-unresolved blind spot. Probe pair pre/post, enrolled ct_call_shape_wall_witness_test RED/controls, regen fixed point divergence 0, whole-corpus compile-clean 0 blocking. Duplicate/missing stay unwalled with triggers (interpreter-first parity pair next). Roadmap node + census rows amended; ROADMAP regenerated. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * chore: regenerate drifted generated artifacts (ci auto-heal) * Roster the call-shape witness blob in the scaffold index (review 45655) ct_call_shape_wall_witness_test joined compiler_tests_rust without its LanguageSourceScaffoldRow, so the exact-equality enrollment witness (compiler_tests_rust_blobs_are_all_rostered, 29 declared vs 28 rostered) would red on CI. Row added with the same hand-assertion scaffold trigger as its peers and enrolled in the roster; witness re-run green by execution. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
Reverts accidental regression of HandAuthoredDocBind primary_work + additional_works, merged accelerator-demo-roundtrip row, guarantee-recovery dual anchors, and doc_reachability construction witnesses (#7486/#7489). Updates sha256_digest_content_hash_convergence_note to match the construction-walled bridge (as_content_hash_cryptographic), not wire-form rendering prose. Co-authored-by: Cursor <cursoragent@cursor.com>
…ment-schema stage, acceptance-door split (#7553) * WIP: compiler correctness * Bind the guarantee-recovery analysis into the doc graph The analysis note landed as an orphan doc: gunbc.doc_graph_roots states that "an unbound doc is an orphan, loudly", and CI duly refused at be1a001 with doc_graph_has_no_orphan_docs returning false in both the dag/test/claim and src/v2/lens consumers. Registered as two HandAuthoredDocBind rows rather than one, because the analysis binds to two independent carriers and they dissolve on different triggers: - v1.compiler.infer module_skips_direct_call_arg_check — the one named violation of the dimension contract's "no escape hatch" clause (docs/thesis/correctness-dimensions.md), exempting v2.* and v1.compiler.* from direct-call argument checking. - v2.std.constraints solve_constraints — passes graph.root as source_facts, algebra AND the sole candidate, so the grounding proof reduces to well_formed(root) and is relabelled CanonicalGrounding. Green by execution, both directions: RED is the CI failure at be1a001; GREEN is all five witnesses in dag/test/claim/doc_reachability_witness_test.dag plus doc_graph_is_clean in src/v2/lens/doc_reachability_test.dag passing locally against the live docs/ tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Reconcile the gap analysis against the independent review — three corrections adopted, receipts verified Adopted (all verified on main this pass): - Cardinality reclassified UNEXPRESSIBLE -> RepresentableButForgeable, not statically propagated: v2.std.refinement exists, NonEmptyList fixture + green cardinality_fold_propagation_test exist, and refined_vacuous_stub_pack's Rejected arm returns Refined { base } (the carrier proves nothing). New Sec 4b: the operator independently re-directed this exact guarantee on 2026-07-04 (interface-summary-declared-use-arity.md Sec 3.1, "hard error in the language") — the intent is not lost; the lattice design pass (FLAG E) never started. - Failure history rewritten (Sec 2): the exemption dates to 2026-06-08 (a13fb57), pre-bankruptcy; correctness-dimensions.md marked type safety "Yes (blocking)" while return position was unchecked — so the ledger overstated, then the auditable contract was deleted. The pipeline_steps_empty_arm_note receipt is withdrawn: empty there is a deliberate total semantics, not a priced-out wall. - Status vocabulary widened to the review's 11-state lattice; v2 terminal calibrated (validate_then_compile door + loop-bound wall are real; InferredTree is still not a proof boundary); application-arity row added (formal-driven walk, positional fallback for misspelled labels, ArityMismatch is constructor-arity); PatternLookupBlocked's silent [] arm confirmed (PatternDynamic does diagnose — review corrected there). - Sec 7b: DESIGN.md is projected from gunbc.design_document, and its "5 behaviors" is stale against v2.std.node's six (Match) — the guarantee authority lands as .dag rows, never hand-edited prose. - Sequencing reconciled to 7 stages: claims authority + expecting-red probe corpus together; zero-resolution method wall now, ambiguity wall census-first; cardinality vertical slice third. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Status header: two audit passes complete, open items typed Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Align the bind's dissolution trigger with the doc's own authority model (review 45299) The first HandAuthoredDocBind trigger said "re-homed into DESIGN.md as its specification half" — wording that predates the reconciliation pass's Sec 7b finding that DESIGN.md is a projection of gunbc.design_document. As written, a direct DESIGN.md edit could have satisfied the trigger, which is exactly the Sec 3 parallel-representation failure Sec 7b names. Trigger now requires .dag claim rows projected via gunbc.design_document and states explicitly that a hand edit does not satisfy it. All five doc-reachability witnesses re-run green by execution after the edit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Address review 45305 (merge same-slug binds, fix stale block) + land the safety ladder as the organizing frame Review 45305, both findings verified correct and fixed: - doc_graph_roots: the two HandAuthoredDocBind rows shared (home, slug), which the carrier's own note defines as the symbolic identity — one doc had two independently removable authority rows. Merged to ONE row whose trigger anchors both carriers (module_skips_direct_call_arg_check, solve_constraints) and gates dissolution on BOTH conditions, with the merge provenance recorded on the carrier. (Observed, not fixed here: module-identity-storage-binding-design and accelerator-demo-roundtrip also carry same-slug duplicate rows — pre-existing, follow-up material.) - Sec 8b's example-0 block still said "unexpressible", contradicting the Sec 4 reclassification and mis-aiming the archetypal RED at inventing a carrier instead of sealing/propagating the one that exists. Rewritten: the RED exercises unforgeable construction + seam propagation, expected refusal at the 0..n -> 1..n seam. Operator direction, same pass: the safety ladder is now Sec 1b, the organizing frame — R3 structurally-impossible / R2 structural guarantee / R1 testable / R0 mitigatable / below-the-floor silent (forbidden, Sec 5). Three rules: floor absolute; climb to a STATED ceiling (mathematical / capability / price — the capability ceiling is unforgeable construction, blocked on reference-level visibility: the keyword set has no private/sealed/opaque); reported rung == measured rung, lens-checked for inflation and stalls. Includes the specimen table (the session's classes placed, cross-representation == as the exemplar full climb) and the non-goals roster (external reality, arbitrary predicates, budgets, optimality, self-governance, byte-identical self-emit — low ceilings BY DESIGN). Stage 1 claim rows gain current_rung / ceiling / next_rung_trigger. All five doc-reachability witnesses re-run green by execution after both file changes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * WIP: compiler correctness * Ladder follow-up: adopt the post-merge verdict (8 corrections) + the guarantee-ladder roadmap section Corrections, each verified against main before adoption: 1. sole_constructor EXISTS (SoleConstructorViolation, sealed-record specimen) — the DESIGN 4b capability claim ("no private/sealed/opaque ... every proof-carrier is presently forgeable") was false as stated; corrected to an audited-status claim: sole_constructor is the candidate wall, completeness for generic carriers unverified. The earlier keyword-set inference is withdrawn in the Sec 10 ledger. 2. Subject grain: rung honesty is measured at a declared acceptance boundary; a class's rung is the MINIMUM across in-scope paths (the interpreter refuses the mislabeled call that order_typed_call_args reorders for emission). DESIGN 4b meta-obligation 1 amended; Stage-1 carrier gains subject_grain/acceptance_boundary/compile_mode/ realization_target/covered_population. 3. Seed rungs demoted: return/data/generic, field-through-generics, exhaustiveness, cardinality, full ==-class, and L4 all to UnknownUnmeasured (compile admission proven is not runtime disposition proven); census marked specimen-denominated; unknown- method R0 scoped to the interpretation path. 4. Dissolution on climb amended in DESIGN 4b: production handling dissolves; the RED + positive controls REMAIN enrolled as the evidence the higher rung stays real. 5. HandAuthoredDocBind.work -> works: List<DeclarationRef> (40 rows + witness-test fixture migrated); the guarantee-recovery row now carries BOTH anchors typed, not one typed + one in prose. Carrier note records that List admits [] — the exact cardinality gap the ladder tracks — with the doc-graph witnesses as the interim wall. 6. cardinality_fold_propagation_test relabeled everywhere as manual value-level specimens (length homomorphism over literals + runtime refine_byte); "not new design" softened to the accurate scope statement; the roadmap cardinality node re-briefed accordingly. 7. Sec 8c recast: TypeBinding carries two bespoke coordinates, not a generic dimension mechanism; extension-vs-redesign is an open audit question that roadmap pricing must carry. 8. Sec 1 "was not built" -> "never completed as an exhaustive acceptance contract"; Sec 11 queue updated (correctness-dimensions done; sole_constructor completeness audit added). Additions (operator direction): ROADMAP gains the "Guarantee ladder — climb plan (DESIGN 4b)" section — 13 sized, unowned, dispatchable nodes in ticket format with dependency edges (probe corpus gates the four floor walls; carrier gates cardinality slice, emitters, prevalence; exemption removal gates on the call-shape + inhabitance walls). The capability node is the sole_constructor completeness audit. State-vs- work split recorded on the carrier: rung STATE lives in the Stage-1 claims carrier and is emitted (ladder-census-emitters node); roadmap nodes track CLIMBS. Verified by execution: main_wet regen (DESIGN.md + ROADMAP.md projections, never hand-edited); drift 4/4; doc-graph 5/5; roadmap authority 35/35, model 9/9, focus 12/12. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give works its executing consumers (review 45336): nonempty wall, symbol fields, two-anchor pin, RED control review 45336 was correct: works had a typed carrier and zero readers — representation without a consumer is specification-without-execution (DESIGN 5 / E-10), the exact defect class the guarantee analysis documents, reproduced in its own fix. Consumers now executing in dag/test/claim/doc_reachability_witness_test: - doc_graph_binds_works_all_nonempty — an emptied works list reds - doc_graph_works_refs_carry_symbols — a ref stripped of module_path or decl_name reds - guarantee_recovery_bind_pins_both_anchors — deleting or renaming either of the two anchors (module_skips_direct_call_arg_check, solve_constraints) reds; row multiplicity pinned to one - doc_graph_works_empty_red_control — synthetic empty-works bind fails the predicate, proving the consumer discriminates Predicates live on the authority (gunbc.doc_graph_roots) so the witness consumes the carrier's own definition. Residue named on the carrier note: staleness against the live tree (a ref naming a decl that no longer exists) is NOT witnessed — v1.compiler.* is outside the witness compile pool, so ref-vs-tree resolution is exactly the feature:cited-symbol-resolution lens DESIGN 3 already names; the refs are symbolic citations and inherit that trigger. All 11 doc-reachability witnesses green by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * De-inflate the three climb-node headlines (review 45349): work nodes name the target rung; current rung defers to the census review 45349, third correct catch in this lane: the census demoted method existence (R0 interpretation-path-only), inhabitance (UnknownUnmeasured), and cardinality (UnknownUnmeasured) — and the roadmap nodes, authored before the demotion pass, kept "R0 -> R2" headlines, re-inflating the same claims the same day at the canonical authority. The section's own note says rung STATE lives in the claims carrier, never these nodes; the headlines now name only the TARGET rung and point at the census for current state, per DESIGN 4b's minimum-across-paths rule. ROADMAP.md regenerated via main_wet; roadmap authority witnesses 35/35; drift witnesses 4/4, by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * chore: regenerate drifted generated artifacts (ci auto-heal) * Ladder nodes join the declared roadmap graph; binds nonempty by construction; rung state derived, never stored Executes the operator's 10-item merge bar on #7489 plus reviews 45356/45367 and tidy-deer-730's measured receipts: - guarantee_ladder_section() deleted; 16 nodes + 23 edges enter declared_roadmap_nodes()/declared_roadmap_edges() via guarantee_ladder_nodes()/ guarantee_ladder_edges(), owner "compiler-guarantee" (lane identity, unbound until closing contracts). Page visibility is the typed focus policy (lane added to roadmap_focus_selection). rendered⊆declared∪derived witnessed with a synthetic-ghost RED. - Graph corrections: probe corpus → carrier → baseline-prevalence → walls; prevalence split baseline/residual; new floor-generic-field-constraint-wall and floor-method-ambiguity-wall nodes; primitive-identity-join is a PREREQUISITE of the general method wall (measured: kernel algebra profiles vs interpreter dispatch fork, tidy-deer-730 on gunbc#7484); cardinality ← sole_constructor audit edge; capability node repointed off the parked visibility-grants doc. - Tickets de-stated: no current-rung transcription anywhere; carrier ticket rewritten to the four-carrier split (Requirement/Path/Measurement/derived Disposition, minimum across paths, no stored rung field) — reconciled across §12 Stage 1, DESIGN §4b tail, and the roadmap node (review 45367); five recovered vocabularies kept orthogonal. - HandAuthoredDocBind: primary_work + additional_works (zero-anchor bind unwritable); empty-works RED deleted with its validation, residue named; duplicate (home,slug) rows merged; bind-identity uniqueness witnessed with a synthetic-duplicate RED. - Census: method-existence subject-grain receipt (narrow kernel wall, gunbc#7484); parser silent-separator below-floor row; §11 items 6-8; §10 fourth-pass ledger. Witnesses: roadmap 37/37 (2 new), identity 9/9, focus 12/12, model 9/9, drift 8/8, doc-graph 11/11. ROADMAP.md/DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Trim the three over-budget ladder briefs to the operator's 100-word ticket law witness_ticket_brief_budget_holds_and_reds red on the CI floor: the carrier, method-existence, and cardinality briefs ran 169/128/111 words. The old section-local placement had escaped this law entirely (the exact ghost-universe defect the verdict named — the budget never saw those nodes); in the declared graph it applies. Briefs trimmed to 94/91/90 with every cut fact already carried in the gap analysis (sec 12 Stage 1b / Stage 2 amendment / the census), which each node links as its carrier. The budget itself is untouched — widening the declaration to satisfy the check is the DESIGN 5 tell, backwards. Page set 28/28, authority set green, regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Containment predicates consume doc_all_nodes, the one canonical walker (review 45412) document_rendered_nodes was a traversal fork beside roadmap_spawner's doc_all_nodes — same semantics, second walker. The predicates (whole-value ghost count + both RED probes) move INTO roadmap_spawner, the walker's module, because the spawner already imports roadmap_authority and the reverse import would cycle. The authority sheds the walker and its now-unused SectionElement imports; the containment note records both refused first cuts (identity-only membership, review 45406; the duplicate walker, review 45412) since each was this wall violating a law it enforces. Authority 38/38, spawner 16/16, page 28/28. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Post-merge verdict follow-up: open-candidate honesty, anchored baseline, FrontierAccepted, and the closure door Executes all six items of the operator's post-merge verdict on #7489, each verified against live state first (#7484 and #7485 confirmed OPEN; the anchor confirmed as the #7489 squash; Behavior confirmed six-membered): 1. Every "#7484 landed" claim replaced with open-candidate wording — main's disposition stated separately from candidate branch evidence (the ladder's rung-inflation rule applied to open-PR state; my transcription error). 2. Baseline prevalence anchored: anchor_commit 6c6e2dc (content-addressed, reproducible after in-flight merges; walls no longer race a live tree). 3. GuaranteeDisposition gains FrontierAccepted{diagnostic, accepted_boundary, evidence} — typed/located/counted but still Accepted; specimens MethodExistenceUndecided and GroundingNotDerived. 4. Graph: floor-parse-formation-wall + floor-record-construction-wall + compiler-accepted-obligation-closure added; v2-phase-carriers split into five staged nodes (self-grounding frontier → Translate refusal → inferred- tree completeness → per-kind derivation coverage → target realization gate) with the registry's FIRST TOMBSTONE (superseded_by the frontier node); method←join edge deleted per the zero-via-union nuance (join gates only the >1 wall and realization completeness); residual reroutes through the closure door. 5. DESIGN §4: closed vocabulary corrected to 6 connectives + 6 behaviors, matching v2.std.node.Behavior (the decidability denominator). 6. §1d provisional guarantee grid emitted as hand-authored interim, dissolve-on the carrier-emitted projection. Witnesses: authority 38/38, identity 9/9 (first tombstone passes the count-free tombstone claims), focus 12/12, model 9/9, page 28/28 (all 23 ladder briefs within the 100-word law), spawner 16/16, drift 8/8, doc 11/11. ROADMAP.md and DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * chore: regenerate drifted generated artifacts (ci auto-heal) * Route the ambiguity wall and cardinality seam through the closure door (review 45545) The first edge set let compiler-accepted-obligation-closure land while floor-method-ambiguity-wall and cardinality-vertical-slice stayed open — the door would have certified "every required judgment established" over two required-open judgments (the grid marks the cardinality seam P0.2 minimum-R2 and ambiguity part of resolved identity; the verdict's spine routes ALL P0 obligations through the door). Both are now prerequisites of the closure; residual prevalence depends on the door alone. Authority 38/38, focus 12/12, page 28/28, drift 8/8; regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Reconcile the sec-7b behavior-count passage to past tense (review 45558) Sec 7b still described the 5-behaviors drift as current after this PR corrected the authority — the stale-claim problem the PR closes elsewhere. The passage now records the drift as found-and-corrected, keeps the specimen's evidentiary value (the denominator drifted silently in prose), and leaves the Match-promotion adjudication question with the queue. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Remove probe demo scaffolding (net-zero vs main: files added by autocommit sweep mid-run, deleted after measurement) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Call-shape wall: refuse unknown argument labels and surplus positionals at the direct-call seam, mirroring the runtime contract The compile seam was silent on both classes call_function_inner refuses at runtime, and the emitter reordered mislabeled args positionally — two realizations of one program disagreeing silently. direct_call_shape_diags (v1.compiler.infer) closes both, blocking, exemption-free (a label has no representation gap). Census before landing refused 28 live rename fossils in 5 fns (to_string i->value, arm_body, is_import_slot_node, fold_list init->empty, path->path_opt), all relabeled to their declared authority; +3 fixed in the measured sig-unresolved blind spot. Probe pair pre/post, enrolled ct_call_shape_wall_witness_test RED/controls, regen fixed point divergence 0, whole-corpus compile-clean 0 blocking. Duplicate/missing stay unwalled with triggers (interpreter-first parity pair next). Roadmap node + census rows amended; ROADMAP regenerated. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * chore: regenerate drifted generated artifacts (ci auto-heal) * Roster the call-shape witness blob in the scaffold index (review 45655) ct_call_shape_wall_witness_test joined compiler_tests_rust without its LanguageSourceScaffoldRow, so the exact-equality enrollment witness (compiler_tests_rust_blobs_are_all_rostered, 29 declared vs 28 rostered) would red on CI. Row added with the same hand-assertion scaffold trigger as its peers and enrolled in the roster; witness re-run green by execution. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Repair the silent-red ord-eligibility wall: name-grain arms admit only childless nodes d975e10 (2026-07-21) moved Symbol onto the name-only opaque-alias roster, dropping the shape check its enrolled negative control pins — Symbol<Float> became BTreeSet-eligible by name, and the RED sat invisible for ten days because the Rust unit suite left CI on 2026-07-11. Childless gate restores the shape constraint (zero corpus impact; regen fixed point holds); incident + dark-suite evidence gap filed as gap-analysis sixth-pass ledger + queue item 9 (operator decision, priced by this incident). Found by tidy-deer-730 during the 7484 main integration. Suite: 30 passed / 0 failed (was 1 failed). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Dedupe the call-shape witness aggregator entry after the main merge The merge auto-combined both sides' insertions of ct_call_shape_wall_witness_test into compiler_tests_source(); a duplicate generates the #[test] twice. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Spine reconciliation: recut the merged P0 slices at their actual grain, add the measurement-schema stage, split the acceptance door Adopts the operator spine verdict (2026-08-01, seventh pass) into the roadmap authority and the gap analysis: - ladder-measurement-schema precedes probes AND carrier (the receipt protocol both meet through; breaks the probes/carrier protocol cycle). - The three merged P0 slices recut at their actual grain, identities tombstoned: floor-call-shape-wall -> call-label-and-surplus-wall (accepted, #7519) + missing/duplicate + signature-resolution siblings; floor-method-existence-wall -> method-established-surface-wall (accepted, #7484) + receiver-normalization + zero-resolution siblings; floor-inhabitance-wall -> declared-conformance-ground-fragment (accepted, #7484) + grounding + general-wall siblings. - The Accepted door split mechanism/floor/extended (compiler-accepted-obligation-closure tombstoned): the audit form lands with the carrier; refusal never turns on over a known-open judgment (review 45545's substance preserved in the activation nodes). - Exemption removal re-grounded on argument-type-compatibility grounding + declared-conformance grounding (labels never gated it). - guarantee_ladder_edges rewritten wholesale; emitters parallel with the baseline; baseline defined as a two-revision execution. - Gap analysis sec 12 updated in place (Stage 0/1a/1c/2-amendment/4/6/6b); stale dissolution triggers repointed (doc_graph_roots, doc_reachability_witness_test); tombstone-note staleness fixed. - ROADMAP.md regenerated via main_wet; roadmap witness receipts 100 PASS (brief budgets, edge endpoints, acyclicity, identity registry with five tombstones); regen_stage0 --verify divergence 0. The branch additionally carries the ord-eligibility silent-red repair (childless gate on name-grain arms + incident note) and the clean regen of the generated stage0 files after the origin/main merge. Known pre-existing: the whole-tree cold census refuses 23 ambiguous-reference diagnostics in dag/test/claim/occurrence_binding_resolve_witness_test.dag (landed with #7508, byte-identical to origin/main; handed off to the occurrence lane). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Recut the extended activation as per-class admissions (review 45918) The first cut kept requires-all edges on one extended-activation node while its prose promised class-by-class widening — the graph would have deferred every admission behind the slowest climb, preserving the monolithic deferral the door split dissolves. Now: four per-class admission nodes (extended-admission-cardinality/-ambiguity/-v2-realization/-v2-translate, each <- floor-closure + its own climb, ready the day that climb lands) and accepted-extended-obligation-closure recut as the terminal roster-completeness certification, where requires-all honestly belongs. Same closure identity (no slug change, no tombstone); four fresh identities minted. Stage 6b + seventh-pass ledger + lane note updated; ROADMAP regenerated; graph/budget/identity witnesses 26 PASS. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Trim the ord name-grain note to its structural constraint (review 45929) The in-code note duplicated the incident narrative the gap analysis already records (sixth-pass ledger + queue item 9) — a parallel ledger realized into the emitted seed with no executable consumer. The carrier keeps only the constraint the code cannot show: why name-grain arms admit childless nodes only, the discriminating RED's symbol, and the shape-examining sibling path. regen_stage0 divergence 0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
…-schema) (#7572) * WIP: compiler correctness * Bind the guarantee-recovery analysis into the doc graph The analysis note landed as an orphan doc: gunbc.doc_graph_roots states that "an unbound doc is an orphan, loudly", and CI duly refused at be1a001 with doc_graph_has_no_orphan_docs returning false in both the dag/test/claim and src/v2/lens consumers. Registered as two HandAuthoredDocBind rows rather than one, because the analysis binds to two independent carriers and they dissolve on different triggers: - v1.compiler.infer module_skips_direct_call_arg_check — the one named violation of the dimension contract's "no escape hatch" clause (docs/thesis/correctness-dimensions.md), exempting v2.* and v1.compiler.* from direct-call argument checking. - v2.std.constraints solve_constraints — passes graph.root as source_facts, algebra AND the sole candidate, so the grounding proof reduces to well_formed(root) and is relabelled CanonicalGrounding. Green by execution, both directions: RED is the CI failure at be1a001; GREEN is all five witnesses in dag/test/claim/doc_reachability_witness_test.dag plus doc_graph_is_clean in src/v2/lens/doc_reachability_test.dag passing locally against the live docs/ tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Reconcile the gap analysis against the independent review — three corrections adopted, receipts verified Adopted (all verified on main this pass): - Cardinality reclassified UNEXPRESSIBLE -> RepresentableButForgeable, not statically propagated: v2.std.refinement exists, NonEmptyList fixture + green cardinality_fold_propagation_test exist, and refined_vacuous_stub_pack's Rejected arm returns Refined { base } (the carrier proves nothing). New Sec 4b: the operator independently re-directed this exact guarantee on 2026-07-04 (interface-summary-declared-use-arity.md Sec 3.1, "hard error in the language") — the intent is not lost; the lattice design pass (FLAG E) never started. - Failure history rewritten (Sec 2): the exemption dates to 2026-06-08 (a13fb57), pre-bankruptcy; correctness-dimensions.md marked type safety "Yes (blocking)" while return position was unchecked — so the ledger overstated, then the auditable contract was deleted. The pipeline_steps_empty_arm_note receipt is withdrawn: empty there is a deliberate total semantics, not a priced-out wall. - Status vocabulary widened to the review's 11-state lattice; v2 terminal calibrated (validate_then_compile door + loop-bound wall are real; InferredTree is still not a proof boundary); application-arity row added (formal-driven walk, positional fallback for misspelled labels, ArityMismatch is constructor-arity); PatternLookupBlocked's silent [] arm confirmed (PatternDynamic does diagnose — review corrected there). - Sec 7b: DESIGN.md is projected from gunbc.design_document, and its "5 behaviors" is stale against v2.std.node's six (Match) — the guarantee authority lands as .dag rows, never hand-edited prose. - Sequencing reconciled to 7 stages: claims authority + expecting-red probe corpus together; zero-resolution method wall now, ambiguity wall census-first; cardinality vertical slice third. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Status header: two audit passes complete, open items typed Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Align the bind's dissolution trigger with the doc's own authority model (review 45299) The first HandAuthoredDocBind trigger said "re-homed into DESIGN.md as its specification half" — wording that predates the reconciliation pass's Sec 7b finding that DESIGN.md is a projection of gunbc.design_document. As written, a direct DESIGN.md edit could have satisfied the trigger, which is exactly the Sec 3 parallel-representation failure Sec 7b names. Trigger now requires .dag claim rows projected via gunbc.design_document and states explicitly that a hand edit does not satisfy it. All five doc-reachability witnesses re-run green by execution after the edit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Address review 45305 (merge same-slug binds, fix stale block) + land the safety ladder as the organizing frame Review 45305, both findings verified correct and fixed: - doc_graph_roots: the two HandAuthoredDocBind rows shared (home, slug), which the carrier's own note defines as the symbolic identity — one doc had two independently removable authority rows. Merged to ONE row whose trigger anchors both carriers (module_skips_direct_call_arg_check, solve_constraints) and gates dissolution on BOTH conditions, with the merge provenance recorded on the carrier. (Observed, not fixed here: module-identity-storage-binding-design and accelerator-demo-roundtrip also carry same-slug duplicate rows — pre-existing, follow-up material.) - Sec 8b's example-0 block still said "unexpressible", contradicting the Sec 4 reclassification and mis-aiming the archetypal RED at inventing a carrier instead of sealing/propagating the one that exists. Rewritten: the RED exercises unforgeable construction + seam propagation, expected refusal at the 0..n -> 1..n seam. Operator direction, same pass: the safety ladder is now Sec 1b, the organizing frame — R3 structurally-impossible / R2 structural guarantee / R1 testable / R0 mitigatable / below-the-floor silent (forbidden, Sec 5). Three rules: floor absolute; climb to a STATED ceiling (mathematical / capability / price — the capability ceiling is unforgeable construction, blocked on reference-level visibility: the keyword set has no private/sealed/opaque); reported rung == measured rung, lens-checked for inflation and stalls. Includes the specimen table (the session's classes placed, cross-representation == as the exemplar full climb) and the non-goals roster (external reality, arbitrary predicates, budgets, optimality, self-governance, byte-identical self-emit — low ceilings BY DESIGN). Stage 1 claim rows gain current_rung / ceiling / next_rung_trigger. All five doc-reachability witnesses re-run green by execution after both file changes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * WIP: compiler correctness * Ladder follow-up: adopt the post-merge verdict (8 corrections) + the guarantee-ladder roadmap section Corrections, each verified against main before adoption: 1. sole_constructor EXISTS (SoleConstructorViolation, sealed-record specimen) — the DESIGN 4b capability claim ("no private/sealed/opaque ... every proof-carrier is presently forgeable") was false as stated; corrected to an audited-status claim: sole_constructor is the candidate wall, completeness for generic carriers unverified. The earlier keyword-set inference is withdrawn in the Sec 10 ledger. 2. Subject grain: rung honesty is measured at a declared acceptance boundary; a class's rung is the MINIMUM across in-scope paths (the interpreter refuses the mislabeled call that order_typed_call_args reorders for emission). DESIGN 4b meta-obligation 1 amended; Stage-1 carrier gains subject_grain/acceptance_boundary/compile_mode/ realization_target/covered_population. 3. Seed rungs demoted: return/data/generic, field-through-generics, exhaustiveness, cardinality, full ==-class, and L4 all to UnknownUnmeasured (compile admission proven is not runtime disposition proven); census marked specimen-denominated; unknown- method R0 scoped to the interpretation path. 4. Dissolution on climb amended in DESIGN 4b: production handling dissolves; the RED + positive controls REMAIN enrolled as the evidence the higher rung stays real. 5. HandAuthoredDocBind.work -> works: List<DeclarationRef> (40 rows + witness-test fixture migrated); the guarantee-recovery row now carries BOTH anchors typed, not one typed + one in prose. Carrier note records that List admits [] — the exact cardinality gap the ladder tracks — with the doc-graph witnesses as the interim wall. 6. cardinality_fold_propagation_test relabeled everywhere as manual value-level specimens (length homomorphism over literals + runtime refine_byte); "not new design" softened to the accurate scope statement; the roadmap cardinality node re-briefed accordingly. 7. Sec 8c recast: TypeBinding carries two bespoke coordinates, not a generic dimension mechanism; extension-vs-redesign is an open audit question that roadmap pricing must carry. 8. Sec 1 "was not built" -> "never completed as an exhaustive acceptance contract"; Sec 11 queue updated (correctness-dimensions done; sole_constructor completeness audit added). Additions (operator direction): ROADMAP gains the "Guarantee ladder — climb plan (DESIGN 4b)" section — 13 sized, unowned, dispatchable nodes in ticket format with dependency edges (probe corpus gates the four floor walls; carrier gates cardinality slice, emitters, prevalence; exemption removal gates on the call-shape + inhabitance walls). The capability node is the sole_constructor completeness audit. State-vs- work split recorded on the carrier: rung STATE lives in the Stage-1 claims carrier and is emitted (ladder-census-emitters node); roadmap nodes track CLIMBS. Verified by execution: main_wet regen (DESIGN.md + ROADMAP.md projections, never hand-edited); drift 4/4; doc-graph 5/5; roadmap authority 35/35, model 9/9, focus 12/12. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give works its executing consumers (review 45336): nonempty wall, symbol fields, two-anchor pin, RED control review 45336 was correct: works had a typed carrier and zero readers — representation without a consumer is specification-without-execution (DESIGN 5 / E-10), the exact defect class the guarantee analysis documents, reproduced in its own fix. Consumers now executing in dag/test/claim/doc_reachability_witness_test: - doc_graph_binds_works_all_nonempty — an emptied works list reds - doc_graph_works_refs_carry_symbols — a ref stripped of module_path or decl_name reds - guarantee_recovery_bind_pins_both_anchors — deleting or renaming either of the two anchors (module_skips_direct_call_arg_check, solve_constraints) reds; row multiplicity pinned to one - doc_graph_works_empty_red_control — synthetic empty-works bind fails the predicate, proving the consumer discriminates Predicates live on the authority (gunbc.doc_graph_roots) so the witness consumes the carrier's own definition. Residue named on the carrier note: staleness against the live tree (a ref naming a decl that no longer exists) is NOT witnessed — v1.compiler.* is outside the witness compile pool, so ref-vs-tree resolution is exactly the feature:cited-symbol-resolution lens DESIGN 3 already names; the refs are symbolic citations and inherit that trigger. All 11 doc-reachability witnesses green by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * De-inflate the three climb-node headlines (review 45349): work nodes name the target rung; current rung defers to the census review 45349, third correct catch in this lane: the census demoted method existence (R0 interpretation-path-only), inhabitance (UnknownUnmeasured), and cardinality (UnknownUnmeasured) — and the roadmap nodes, authored before the demotion pass, kept "R0 -> R2" headlines, re-inflating the same claims the same day at the canonical authority. The section's own note says rung STATE lives in the claims carrier, never these nodes; the headlines now name only the TARGET rung and point at the census for current state, per DESIGN 4b's minimum-across-paths rule. ROADMAP.md regenerated via main_wet; roadmap authority witnesses 35/35; drift witnesses 4/4, by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * chore: regenerate drifted generated artifacts (ci auto-heal) * Ladder nodes join the declared roadmap graph; binds nonempty by construction; rung state derived, never stored Executes the operator's 10-item merge bar on #7489 plus reviews 45356/45367 and tidy-deer-730's measured receipts: - guarantee_ladder_section() deleted; 16 nodes + 23 edges enter declared_roadmap_nodes()/declared_roadmap_edges() via guarantee_ladder_nodes()/ guarantee_ladder_edges(), owner "compiler-guarantee" (lane identity, unbound until closing contracts). Page visibility is the typed focus policy (lane added to roadmap_focus_selection). rendered⊆declared∪derived witnessed with a synthetic-ghost RED. - Graph corrections: probe corpus → carrier → baseline-prevalence → walls; prevalence split baseline/residual; new floor-generic-field-constraint-wall and floor-method-ambiguity-wall nodes; primitive-identity-join is a PREREQUISITE of the general method wall (measured: kernel algebra profiles vs interpreter dispatch fork, tidy-deer-730 on gunbc#7484); cardinality ← sole_constructor audit edge; capability node repointed off the parked visibility-grants doc. - Tickets de-stated: no current-rung transcription anywhere; carrier ticket rewritten to the four-carrier split (Requirement/Path/Measurement/derived Disposition, minimum across paths, no stored rung field) — reconciled across §12 Stage 1, DESIGN §4b tail, and the roadmap node (review 45367); five recovered vocabularies kept orthogonal. - HandAuthoredDocBind: primary_work + additional_works (zero-anchor bind unwritable); empty-works RED deleted with its validation, residue named; duplicate (home,slug) rows merged; bind-identity uniqueness witnessed with a synthetic-duplicate RED. - Census: method-existence subject-grain receipt (narrow kernel wall, gunbc#7484); parser silent-separator below-floor row; §11 items 6-8; §10 fourth-pass ledger. Witnesses: roadmap 37/37 (2 new), identity 9/9, focus 12/12, model 9/9, drift 8/8, doc-graph 11/11. ROADMAP.md/DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Trim the three over-budget ladder briefs to the operator's 100-word ticket law witness_ticket_brief_budget_holds_and_reds red on the CI floor: the carrier, method-existence, and cardinality briefs ran 169/128/111 words. The old section-local placement had escaped this law entirely (the exact ghost-universe defect the verdict named — the budget never saw those nodes); in the declared graph it applies. Briefs trimmed to 94/91/90 with every cut fact already carried in the gap analysis (sec 12 Stage 1b / Stage 2 amendment / the census), which each node links as its carrier. The budget itself is untouched — widening the declaration to satisfy the check is the DESIGN 5 tell, backwards. Page set 28/28, authority set green, regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Containment predicates consume doc_all_nodes, the one canonical walker (review 45412) document_rendered_nodes was a traversal fork beside roadmap_spawner's doc_all_nodes — same semantics, second walker. The predicates (whole-value ghost count + both RED probes) move INTO roadmap_spawner, the walker's module, because the spawner already imports roadmap_authority and the reverse import would cycle. The authority sheds the walker and its now-unused SectionElement imports; the containment note records both refused first cuts (identity-only membership, review 45406; the duplicate walker, review 45412) since each was this wall violating a law it enforces. Authority 38/38, spawner 16/16, page 28/28. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Post-merge verdict follow-up: open-candidate honesty, anchored baseline, FrontierAccepted, and the closure door Executes all six items of the operator's post-merge verdict on #7489, each verified against live state first (#7484 and #7485 confirmed OPEN; the anchor confirmed as the #7489 squash; Behavior confirmed six-membered): 1. Every "#7484 landed" claim replaced with open-candidate wording — main's disposition stated separately from candidate branch evidence (the ladder's rung-inflation rule applied to open-PR state; my transcription error). 2. Baseline prevalence anchored: anchor_commit 6c6e2dc (content-addressed, reproducible after in-flight merges; walls no longer race a live tree). 3. GuaranteeDisposition gains FrontierAccepted{diagnostic, accepted_boundary, evidence} — typed/located/counted but still Accepted; specimens MethodExistenceUndecided and GroundingNotDerived. 4. Graph: floor-parse-formation-wall + floor-record-construction-wall + compiler-accepted-obligation-closure added; v2-phase-carriers split into five staged nodes (self-grounding frontier → Translate refusal → inferred- tree completeness → per-kind derivation coverage → target realization gate) with the registry's FIRST TOMBSTONE (superseded_by the frontier node); method←join edge deleted per the zero-via-union nuance (join gates only the >1 wall and realization completeness); residual reroutes through the closure door. 5. DESIGN §4: closed vocabulary corrected to 6 connectives + 6 behaviors, matching v2.std.node.Behavior (the decidability denominator). 6. §1d provisional guarantee grid emitted as hand-authored interim, dissolve-on the carrier-emitted projection. Witnesses: authority 38/38, identity 9/9 (first tombstone passes the count-free tombstone claims), focus 12/12, model 9/9, page 28/28 (all 23 ladder briefs within the 100-word law), spawner 16/16, drift 8/8, doc 11/11. ROADMAP.md and DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * chore: regenerate drifted generated artifacts (ci auto-heal) * Route the ambiguity wall and cardinality seam through the closure door (review 45545) The first edge set let compiler-accepted-obligation-closure land while floor-method-ambiguity-wall and cardinality-vertical-slice stayed open — the door would have certified "every required judgment established" over two required-open judgments (the grid marks the cardinality seam P0.2 minimum-R2 and ambiguity part of resolved identity; the verdict's spine routes ALL P0 obligations through the door). Both are now prerequisites of the closure; residual prevalence depends on the door alone. Authority 38/38, focus 12/12, page 28/28, drift 8/8; regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Reconcile the sec-7b behavior-count passage to past tense (review 45558) Sec 7b still described the 5-behaviors drift as current after this PR corrected the authority — the stale-claim problem the PR closes elsewhere. The passage now records the drift as found-and-corrected, keeps the specimen's evidentiary value (the denominator drifted silently in prose), and leaves the Match-promotion adjudication question with the queue. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Remove probe demo scaffolding (net-zero vs main: files added by autocommit sweep mid-run, deleted after measurement) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Call-shape wall: refuse unknown argument labels and surplus positionals at the direct-call seam, mirroring the runtime contract The compile seam was silent on both classes call_function_inner refuses at runtime, and the emitter reordered mislabeled args positionally — two realizations of one program disagreeing silently. direct_call_shape_diags (v1.compiler.infer) closes both, blocking, exemption-free (a label has no representation gap). Census before landing refused 28 live rename fossils in 5 fns (to_string i->value, arm_body, is_import_slot_node, fold_list init->empty, path->path_opt), all relabeled to their declared authority; +3 fixed in the measured sig-unresolved blind spot. Probe pair pre/post, enrolled ct_call_shape_wall_witness_test RED/controls, regen fixed point divergence 0, whole-corpus compile-clean 0 blocking. Duplicate/missing stay unwalled with triggers (interpreter-first parity pair next). Roadmap node + census rows amended; ROADMAP regenerated. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * chore: regenerate drifted generated artifacts (ci auto-heal) * Roster the call-shape witness blob in the scaffold index (review 45655) ct_call_shape_wall_witness_test joined compiler_tests_rust without its LanguageSourceScaffoldRow, so the exact-equality enrollment witness (compiler_tests_rust_blobs_are_all_rostered, 29 declared vs 28 rostered) would red on CI. Row added with the same hand-assertion scaffold trigger as its peers and enrolled in the roster; witness re-run green by execution. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Repair the silent-red ord-eligibility wall: name-grain arms admit only childless nodes d975e10 (2026-07-21) moved Symbol onto the name-only opaque-alias roster, dropping the shape check its enrolled negative control pins — Symbol<Float> became BTreeSet-eligible by name, and the RED sat invisible for ten days because the Rust unit suite left CI on 2026-07-11. Childless gate restores the shape constraint (zero corpus impact; regen fixed point holds); incident + dark-suite evidence gap filed as gap-analysis sixth-pass ledger + queue item 9 (operator decision, priced by this incident). Found by tidy-deer-730 during the 7484 main integration. Suite: 30 passed / 0 failed (was 1 failed). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Dedupe the call-shape witness aggregator entry after the main merge The merge auto-combined both sides' insertions of ct_call_shape_wall_witness_test into compiler_tests_source(); a duplicate generates the #[test] twice. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Spine reconciliation: recut the merged P0 slices at their actual grain, add the measurement-schema stage, split the acceptance door Adopts the operator spine verdict (2026-08-01, seventh pass) into the roadmap authority and the gap analysis: - ladder-measurement-schema precedes probes AND carrier (the receipt protocol both meet through; breaks the probes/carrier protocol cycle). - The three merged P0 slices recut at their actual grain, identities tombstoned: floor-call-shape-wall -> call-label-and-surplus-wall (accepted, #7519) + missing/duplicate + signature-resolution siblings; floor-method-existence-wall -> method-established-surface-wall (accepted, #7484) + receiver-normalization + zero-resolution siblings; floor-inhabitance-wall -> declared-conformance-ground-fragment (accepted, #7484) + grounding + general-wall siblings. - The Accepted door split mechanism/floor/extended (compiler-accepted-obligation-closure tombstoned): the audit form lands with the carrier; refusal never turns on over a known-open judgment (review 45545's substance preserved in the activation nodes). - Exemption removal re-grounded on argument-type-compatibility grounding + declared-conformance grounding (labels never gated it). - guarantee_ladder_edges rewritten wholesale; emitters parallel with the baseline; baseline defined as a two-revision execution. - Gap analysis sec 12 updated in place (Stage 0/1a/1c/2-amendment/4/6/6b); stale dissolution triggers repointed (doc_graph_roots, doc_reachability_witness_test); tombstone-note staleness fixed. - ROADMAP.md regenerated via main_wet; roadmap witness receipts 100 PASS (brief budgets, edge endpoints, acyclicity, identity registry with five tombstones); regen_stage0 --verify divergence 0. The branch additionally carries the ord-eligibility silent-red repair (childless gate on name-grain arms + incident note) and the clean regen of the generated stage0 files after the origin/main merge. Known pre-existing: the whole-tree cold census refuses 23 ambiguous-reference diagnostics in dag/test/claim/occurrence_binding_resolve_witness_test.dag (landed with #7508, byte-identical to origin/main; handed off to the occurrence lane). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Recut the extended activation as per-class admissions (review 45918) The first cut kept requires-all edges on one extended-activation node while its prose promised class-by-class widening — the graph would have deferred every admission behind the slowest climb, preserving the monolithic deferral the door split dissolves. Now: four per-class admission nodes (extended-admission-cardinality/-ambiguity/-v2-realization/-v2-translate, each <- floor-closure + its own climb, ready the day that climb lands) and accepted-extended-obligation-closure recut as the terminal roster-completeness certification, where requires-all honestly belongs. Same closure identity (no slug change, no tombstone); four fresh identities minted. Stage 6b + seventh-pass ledger + lane note updated; ROADMAP regenerated; graph/budget/identity witnesses 26 PASS. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Trim the ord name-grain note to its structural constraint (review 45929) The in-code note duplicated the incident narrative the gap analysis already records (sixth-pass ledger + queue item 9) — a parallel ledger realized into the emitted seed with no executable consumer. The carrier keeps only the constraint the code cannot show: why name-grain arms admit childless nodes only, the discriminating RED's symbol, and the shape-examining sibling path. regen_stage0 divergence 0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Spine A Stage 0: the guarantee measurement schema — evidence identifies its subject before anyone measures gunbc.guarantee_measurement carries the vocabulary probes and claims meet through, and nothing else (roadmap node ladder-measurement-schema; operator spine verdict 2026-08-01): GuaranteeClassId/PathId/ProbeId brands; GuaranteePath over four closed minimal axes (subject grain, acceptance boundary incl. the InferToEval/InferToTranslate phase boundaries the containment workstream consumes, compile mode, realization target with GuaranteeTargetName deferred-grounding brand); GuaranteeMeasurementReceipt with every field required (subject_revision x harness_revision x probe_set_digest, reusing std.types.CommitSha and std.content_hash); ProbeObservation as the raw outcome sum with ProbeNotRunnable structurally separated from verdicts (top-as-ignorance never readable as pass/fail); exactly-one path resolution and a receipt->path join that refuses unknown and duplicate. Registry mechanism without a registry population - no probe executes, no class rows, no disposition, no rung. An initial ObservedOutcome name collided with gunbc.output_policy's process-outcome type (whole-tree census caught the bare-reference break); renamed to ProbeObservation, census back to 0 blocking. Receipts: 8/8 synthetic-row witnesses green by execution (round-trip join, unknown-path refusal, duplicate-registry refusal never-first-pick, exactly-one resolution across four boundary variants, both uniqueness REDs, digest input-determinism incl. order sensitivity, verdict/ignorance separation); whole-tree compile 0 blocking; regen_divergence_count=0; generated artifacts zero drift. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Record the second-consumer re-grounding trigger for observed_is_verdict (review 46075) The predicate/walker dissolution rule triggers where a canonical fold already exists (nat_cata) or a substrate walk is extended; neither holds for a freshly declared domain sum whose only query this is. The note now records the named trigger: when the claims carrier lands as the sum's second consumer, a probe_observation fold becomes the canonical surface and observed_is_verdict re-expresses through it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Grant publication for the eight ungranted #7544 files (main-side gate breakage) The publication gate reds on current main itself: #7544 (heal-revalidation) merged after the P-B wall landed via #7560 but its CI raced the wall, so its eight new files carry no PublicFilePublishGrant rows and every PR merging current main inherits the failure. Rows added for all eight (mechanical placement declarations for files already public on main); cutover..HEAD Added/Copied/Renamed set now fully rostered, gate witnesses green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Grant publication for the three ungranted #7563 files (second main-side race) Same class as the #7544 fix one commit ago: #7563 merged on a pre-wall CI run, adding three SCM-kernel files with no grant rows. Roster now covers the full cutover..HEAD set including current main. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Thread GuaranteePathId through resolution and its refusal variants (review 46179) The resolver's key and both refusal-variant payloads carry the brand end-to-end; join_receipt_to_path no longer erases receipt.path to String. Measured the enforcement honestly: two executed controls show the checker accepting a bare String at a branded parameter and a branded record field, so the note records this as model-correctness and erasure-removal, with brand acceptance-enforcement handed to the probe corpus as its own class. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Merge origin/main; dedupe the roster union and grant the two #7550 lean files The alphabetized roster body on main already carried the 11 straggler paths, so #7580's tail block duplicated every one of them; the union keeps exactly one row per path, with this branch's two guarantee rows slotted alphabetically. Coverage against the cutover then caught a fourth race instance: #7550 merged two new files with no grant rows (dag/extdeps/languages/lean/overflow.dag and its witness), redding main's gate again - swept into the same roster here. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Observation counts are Nat, with the enforcement gap measured (review 46287) RefusedTyped.count and AcceptedCounted.count carry the cardinal type, and the fold's arm signatures follow. An executed control shows the checker still accepting a negative at the Nat field today, so the note records the swap as model-correctness with refusal owed to the numeric-refinement acceptance class, not claimed as a wall. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Orthogonalize the path axes instead of enumerating families (review 46308) InterpreterRun renames to RuntimeRun: run-level acceptance happens IN the path's realization, so which runtime is the realization axis's fact and an emitted-run path (the divergence probes' subject) is expressible rather than contradictory. The compile_mode axis deletes: every landed control derives its pipeline from its boundary, so the stored mode was a second representation whose only writable novelty was the contradiction; it returns as a stored axis with the first path measured under two pipelines at one boundary. Both review-named contradictions are now unwritable without a family coproduct, whose rows would restate the orthogonal axes per combination (the N-by-M shape DESIGN 2 folds into axes). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
…7480) * Ground ContentHash on hash family (Phase A: carriers + R0 backstop) Rebased onto main. ContentHash becomes a family coproduct (Fnv1a64 | Sha256Hash | Sha1Hash) with where-refined hex carriers, compare_content_hash cross-family refusals, OCI algorithm-qualified digests, and construction walls (reviews 45496/45505). Co-authored-by: Cursor <cursoragent@cursor.com> * Fix review 45522 regressions and CI compile-gate timeout. - Restore guarantee-ladder and shell→intent authority in design_document.dag and guarantee_ladder_nodes/roadmap_focus in roadmap_authority.dag from main; keep intentional chash Fnv1a64Structural migration only. - Remove git_sha1 witness Absent fallback (mint must succeed or test reds). - Raise v1-compiler-tests compile-gate step budget to 10m (run 30646205825). Co-authored-by: Cursor <cursoragent@cursor.com> * chore: regenerate drifted generated artifacts (ci auto-heal) * Update DESIGN open-thread row for ContentHash Phase A landing (#7480). Replace the stale pre-migration §3 residue with Phase A receipts and an explicit Phase B dissolve-on remainder (union-level == typecheck refusal). Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Ground ContentHash on its hash family so a cross-family comparison is un * chore: regenerate drifted generated artifacts (ci auto-heal) * Move OCI digest algorithm predicates to extdeps.container.oci.digest. Review 45539 flagged OCI-specific algorithm grammar in std.content_hash as a §3 authority inversion. The predicates and where-refinement entry point now live at the OCI digest authority; infer imports oci_other_digest_algorithm from there and stage0 emits extdeps_container_oci_digest.rs. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Ground ContentHash on its hash family so a cross-family comparison is un * WIP: Ground ContentHash on its hash family so a cross-family comparison is un * fix(stage0): commit emitted extdeps_container_oci_digest seed module Regen emits the OCI digest module but it was never tracked in git after rebase, which broke cargo fmt and the build gate on PR #7480. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Ground ContentHash on its hash family so a cross-family comparison is un * fix(oci digest): realign seed parse path and emitter Optional Present arm Review 45614: use `encoded: encoded` in the other-algorithm parse arm (oci_encoded_digest returns NonEmptyStr?, not a record). Route split parts through oci_wire_digest_parts_from_split so the seed types as String. Fix v1 emitter construction so Present{value: <branded scalar cast>} lowers to Some(...) instead of Optional::String. Restore extdeps_base module path for extdeps_container_oci_digest. Co-authored-by: Cursor <cursoragent@cursor.com> * chore: regenerate drifted generated artifacts (ci auto-heal) * WIP: Ground ContentHash on its hash family so a cross-family comparison is un * WIP: Ground ContentHash on its hash family so a cross-family comparison is un * WIP: Ground ContentHash on its hash family so a cross-family comparison is un * WIP: Ground ContentHash on its hash family so a cross-family comparison is un * chore: regenerate drifted generated artifacts (ci auto-heal) * fix(emit-on-demand-host): refuse crypto ContentHash at structural projection Review 45661: replace emit_host_identity_structural sentinel collapse with typed outcome coproducts (EmitHostStructuralIdentityRefusedCrypto, ResolvedBuildContextIdentityRefusedCrypto, ToolchainIdentityRefusedCrypto). Distinct Sha256/Sha1 digests no longer share one fnv1a64 cache key. Witness resolved_build_context_identity_refuses_sha256_observed_tool exercises the refusal path; structural fixture tests route through outcome helpers. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Ground ContentHash on its hash family so a cross-family comparison is un * test(emitter): fix optional Present witness include/exclude patterns The exclude Optional::String substring matches lawful return-type emission; use the broken-body pattern String { value: text instead so the witness discriminates Some(...) lowering from the generic Optional::String variant path. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(emit-on-demand-host): serialize ContentHash cache path segments Route native cache workspace path construction through serialize_content_hash instead of bare as String casts so cache keys use the canonical wire form (review 45713). Co-authored-by: Cursor <cursoragent@cursor.com> * fix(emit-on-demand-host): drop parallel family field from crypto refusals ContentHash already carries its family; RefusedCrypto variants now hold only component and identity. Witness derives family via content_hash_family (review 45721). Co-authored-by: Cursor <cursoragent@cursor.com> * fix: restore doc-graph construction walls from main (review 45726) Reverts accidental regression of HandAuthoredDocBind primary_work + additional_works, merged accelerator-demo-roundtrip row, guarantee-recovery dual anchors, and doc_reachability construction witnesses (#7486/#7489). Updates sha256_digest_content_hash_convergence_note to match the construction-walled bridge (as_content_hash_cryptographic), not wire-form rendering prose. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Ground ContentHash on its hash family so a cross-family comparison is un * fix(oci-digest): construction-wall OciOtherDigestEncoded payload OciOtherDigestBody.encoded is now NonEmptyStr where oci_other_digest_encoded (descriptor.md charset), not a forgeable bare NonEmptyStr (review 45731). Infer where-refinement enrollment mirrors oci_other_digest_algorithm. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(oci-digest): emit parse wire path without NonEmptyStr cast panic Use parts.encoded as OciOtherDigestEncoded after oci_encoded_digest validates (same pattern as sha512 hex), avoiding emitter panic on String→NonEmptyStr cast in the OtherDigest parse arm. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(oci-digest): OciOtherDigestEncoded as String where for emit parity NonEmptyStr where oci_other_digest_encoded made the emitter emit panic() on String→NonEmptyStr cast in parse_oci_content_digest_wire. String where oci_other_digest_encoded matches OciSha512DigestHex and keeps the construction wall (review 45731). Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: gunbc oracle * WIP: gunbc oracle * fix(content-hash): project .digest at string boundaries; repair the last floor reds Three sites where a structural hash reached a String position: - roadmap_dispatch_actuator dispatch_attempt_key and roadmap_belt_actuate belt_uuid_hex32 cast the content_hash_atom / content_hash_combine_structural RESULT to String. content_hash_atom returns Fnv1a64Structural (a record) since the family grounding, so the cast no longer yields the digest text. Notably this is not a typecheck error -- roadmap_belt_actuate's own uuid witnesses passed while the value was wrong -- so the only witness that caught it was the one comparing a parsed branch against the minted one (attempts_parse_roundtrips_the_minted_branch). Both now project .digest, the idiom site/moodboard.dag already used. A regex + paren-matching sweep over every .dag confirms no structural result is cast directly to a string type anywhere. - source_integration_landing_spine's witness compared a receipt against the raw literal "multiplicity-receipt" after construction moved to content_hash_of_value(...), i.e. the field now holds a hash of that string. Verified by execution: dispatch_attempts 9/9, roadmap_belt_actuate uuid witnesses 3/3, source_integration_landing_spine 22/22. (roadmap_belt_actuate's seven belt_exec witnesses fail locally with "hermetic mode: no mock_response for operation Check" -- they shell out to a real host process and never reach hash code; that is the hermetic runner refusing to fabricate, not a regression.) * fix(content-hash): re-home ContentHash imports that arrived with the main merge The floor's dag_compile_clean_gate went red on the merge commit with one hard diagnostic: name 'ContentHash' not found in module 'std.types'. Two witness files came in from main still importing ContentHash from std.types and initializing it from a string literal -- the shape this PR's family grounding removed: dag/test/claim/check_coverage_admission_witness_test.dag (4 rows) src/v2/test/claim/walk_plan_schedule_lens_test.dag (1 row) Both now import from std.content_hash and mint through content_hash_of_value, matching their consumers, which take the union ContentHash (merge_admission check_coverage_admits; the walk-plan target field). My pre-merge sweep for this class was clean and stayed correct -- these files did not exist on this branch when it ran. The sweep has to be re-run after each merge, not once. Re-run now: zero std.types ContentHash imports and zero string-literal ContentHash initializers corpus-wide. Verified by execution: whole-tree `gunbc compile --target dag` reports 0 hard diagnostics (the gate's own check); check_coverage_admission 12/12; walk_plan_schedule_lens 2/2. * WIP: gunbc oracle * revert(v2-node): restore node.dag hash surface to its 2804c8b state The WIP auto-commit at 8212c2a captured a mid-edit working tree: a speculative retype of v2.std.node content_hash / symbol_identity_digest / bag_hash_digest / byte_offset_cache_key_fingerprint to return Hash, snapshotted BEFORE I had fixed a stray argument label it introduced -- fn symbol_identity_digest(sym: Symbol) -> Hash { structural: content_hash_atom(value: sym) # not an expression } -- so that broken form went out on the branch. My subsequent `git checkout --` restored to that bad commit rather than to the intended baseline, which is how it survived. This restores the file byte-for-byte to 2804c8b. The retype is reverted on its merits regardless of the label bug: executed against the three failing classes (Variant-cast, digest-on-String, atom_identity_hash arity) it fixed NONE of them, so it was an unverified edit to a load-bearing substrate file with no demonstrated benefit. The real roots are recorded in the PR comment: five `ContentHash where brand(...)` types that can no longer be cast, and the raw atom_identity_hash / std.content_hash dual surface in 02_parse and self_host. * WIP: gunbc oracle * chore: regenerate drifted generated artifacts (ci auto-heal) * Project the corrected ContentHash bridge claim into DESIGN.md sha256_digest_content_hash is the VALIDATING PARTIAL bridge Digest->ContentHash?; as_content_hash_cryptographic is the TOTAL injection. Regenerated via tools.generated_artifact_gate main_wet; byte-stable on a second pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: gunbc oracle * WIP: gunbc oracle * WIP: gunbc oracle * WIP: gunbc oracle * WIP: gunbc oracle * WIP: gunbc oracle * WIP: gunbc oracle * WIP: gunbc oracle * WIP: gunbc oracle * WIP: gunbc oracle * WIP: gunbc oracle * WIP: gunbc oracle * WIP: gunbc oracle * Restore the v1 seed sources an auto-commit reverted to main The session auto-commit fired while src/v1 was checked out to origin/main for a control build, snapshotting main's version as this branch's HEAD; a later 'git checkout HEAD -- src/v1/' then restored that poisoned state. Three files lost their reviewed content and are restored from f9dc5a8: 00_core.dag — 'predicate not enforced at compile time' advisory reason 04_infer.dag — lower_hex_{16,40,64,128} / oci_other_digest_* where-predicates and the structural content-hash rewrite 05_emit_rust.dag — variant_surface_name + fn_returns_optional 05_emit_rust.dag is reconstructed onto main's newer revision rather than overwritten, so main's rust_btree_set_ord name-grain childless gate and its note are preserved; the result is byte-identical to f9dc5a8 apart from that addition. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: gunbc oracle * Remove temporary emitter-probe fixture Diagnostic scaffold for isolating the optional-payload cast emit defect; the repro is recorded in the PR discussion, not enrolled as a witness pending a decision on the emitter fix. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the optional-payload cast emit deficit as executing evidence Three poles, each holding one variable constant, isolate the trigger for the E0433 that blocks finding 3's oci_encoded_digest shape: refined return, no cast -> lowers to Some(..) (refined return is harmless) plain String? return, cast inside payload -> broken (the cast alone suffices) cast hoisted to a let -> STILL broken (refutes the workaround) The third pole is load-bearing: hoisting does not avoid the defect, so no respelling both constructs the carrier and lowers correctly, and the emitter repair is required rather than optional. An earlier draft of this file claimed the hoist WAS a working scaffold spelling and briefly landed that spelling in oci_encoded_digest; executing it refuted the claim, and both are reverted -- oci_encoded_digest keeps the reviewed inline shape. Poles 2 and 3 are known-red receipts: they assert the deficit is present, so they pass now and red when the emitter is repaired. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: gunbc oracle * WIP: gunbc oracle * Repair optional-payload cast lowering; regenerate the seed from the authority Confirmed name-loss point (by instrumentation, not by reading): the concrete-type peel in v1.compiler.emit_rust emit_rust_expr_record_lit. A cast reaching an optional payload gives the literal a concrete resolved type, so the peel replaced the authored "Present" with the payload's concrete name; emit_typed_record_lit then missed the optional arm and fabricated "Optional::String { .. }", which is not a Rust constructor (E0433). A probe printing variant_name/tn/peeled at the call site showed the authored name arriving intact and being overwritten. The standing variant_surface_name hypothesis was wrong as a single cause but is a real SECOND contributor: with the peel fixed, optional_variant still keyed off the resolved struct name until variant_surface_name reached the seed. Both were required; neither alone sufficed. The peel is suppressed only when the authored name is a built-in optional constructor AND the concrete type does not itself declare a variant of that name, so a user-defined "Present" still peels (variant_belongs_to_enum finds it) and ordinary variants are untouched. Variant identity is preserved, never inferred from the payload type. Authority is src/v1/05_emit_rust.dag. The seed could not regenerate the fix, so minimal bootstrap edits were lifted by hand and then PROVEN by regeneration: regen_stage0 --verify reports regen_divergence_count=0, so committed stage0 is exactly the fresh self-compile of the authority. Also restores cli_run.rs, the v1_interpreter R0 cross-family guard, and two more hand-written seed files that the earlier auto-commit poisoning reverted to main (the R0 guard is merged onto main's newer interpreter, not overwritten). Witness flipped from known-red receipt to permanent regression control (DESIGN section 4b): 6/6 including the Wrap::Holds and user-defined-Present negative controls. Nested-refinement receipt retains its polarity, 2/2. Whole-tree compile exit 0. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Declare publication grants for the 17 ungranted added public paths The Stage-0 visibility guard (tools.publication_placement_gate, run as the Wet floor runnable publication_placement_gate_passes) diffs the publication cutover to HEAD and refuses any added public path with no Publish grant. It reported PublishGuardLocalViolation count=17, which is why the ci floor failed while build, regen and heal all passed. Six are this PR's: the OCI digest carrier, its generated stage0 projection, and the four ContentHash/emitter witness files. The other eleven arrived with main (the heal-revalidation and source-integration-proof-kernel lanes, ci_heal_dispatch, extdeps.github.workflows and the preflight emit pair); the guard diffs from the cutover rather than from the merge base, so it fires on the union and this branch cannot go green while they are undeclared. All seventeen are already merged and pushed to the public repository, so granting records the publication that already happened rather than newly exposing anything. Flagged rather than silent because eleven of the paths are not this PR's to classify. Gate re-run locally: ExitSuccess. publication_placement_gate_test 8/8. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: gunbc oracle * Converge the fnv1a64 dual surface at the 22 sites the re-key stranded The floor's discovery corpus surfaced 22 witnesses this PR broke, in two classes, both instances of the dual surface DESIGN section 3 tracks: v2 code calls the RAW v1 intrinsics while std.content_hash is the modeled surface over the same authority. Re-keying v2.std.node.Hash to Fnv1a64Structural made that fork observable, because a raw intrinsic yields a native String where the modeled carrier is a record. Class 1 (18) -- "cannot access field digest on String": raw atom_identity_hash flowed into Hash positions. Eleven call sites in v2.compiler.02_parse, v2.compiler.self_host and the parse_table_content_key witness now route through v2.std.node symbol_identity_digest, the modeled surface those modules already import. The substitution is value-preserving: content_hash_atom(v) is by definition structural_content_hash(digest: atom_identity_hash(v)). Class 2 (2) -- "atom_identity_hash requires exactly one string argument": the inverse, a structural passed INTO the intrinsic. v2.lens.interface_summary signature_fingerprint_of_node hashed a node content hash that is now a record; it projects .digest first. A direct cast was tried and rejected by the interpreter (cannot cast Record to Fnv1a64Structural), so the original hash-of-hash semantics are kept rather than changed. Plus one value mismatch: the live_deploy readiness witness compared site_artifact_digest(..) as String against the digests the served body embeds, which now project .digest. After this the raw intrinsics appear nowhere outside dag/std/content_hash.dag and the v1 builtin registry, which is the single-authority end state. Re-run green: parse_table_content_key 5/5, interface_summary_firewall 4/4, ingest_bridge 9/9, cross_language_add_python_to_typescript 4/4, inhabitant_neutralization 6/6, parse_table_memo_governed 9/9, self_host_realized_comparison_floor 6/6, parse_stamp_span_index 2/2, live_deploy readiness 25/25. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: gunbc oracle * Address review 2026-08-01: restore roadmap containment wall, narrow optional emitter, correct design authority Three blocking items from the review, each with executing evidence. 1. Roadmap containment wall (regression against the branch base). My earlier merge dropped main's rendered-node containment wall entirely: roadmap_rendered_ghost_count, both RED probes, and all three witnesses were absent from this head. Restored roadmap_spawner.dag from main wholesale (main was a strict superset there) and grafted the import block, note and three tests onto roadmap_authority_test.dag while keeping this PR's Fnv1a64Structural changes. 38/38 green, the count the review predicted. 2. Optional emitter classification was broader than its stated boundary. The fn_returns_optional disjunct is a fact about the ENCLOSING FUNCTION, so a user-defined MyOpt::Present built inside a `-> String?` function emitted Some(..), overriding an effective_parent that had already resolved correctly. Added the negative control the review asked for and CONFIRMED IT RED before changing anything. Then executed all seven poles with the function-wide arm removed: it was load-bearing for none of them, so it is deleted rather than gated -- resolved_type.return_cardinality == CardOptional is the expression-local statement of the same fact, and the disjunct was a second representation of it. 7/7 green; regen_divergence_count=0. 3. Design authority still described the deleted models. Corrected design_document.dag (v2.std.node Hash is Fnv1a64Structural, not std.types.ContentHash -- wrong home and wrong type, contradicting the Phase A row below it), regenerated DESIGN.md, and corrected both locked plan docs to say the unit carries one agnostic identity from which each realization derives its spelling. Corpus sweep for the three stale claims is clean. Also repairs a main red this branch inherited: CompileDiagnosticCensus became an unrostered inert carrier when main's codex-review-46144 repair deleted census_rows(c: CompileDiagnosticCensus), its only production consumer. The three files involved are byte-identical to main, so the red is main's, not this branch's. Rostered with that reason and the standard dissolve trigger. * Discharge the CR/NUL control gap: main's Unicode escapes fired its dissolve-on trigger Round 2 asked for hostile-spelling controls over / \ CR LF NUL and ". CR and NUL were declared as a coverage BOUNDARY rather than faked, because .dag string literals had no numeric-escape form: backslash-r lexed as literal backslash-then-r and the backslash-u brace form lexed as its raw characters, both measured at the time. The note carried an explicit dissolve-on trigger. Main landed Unicode string escapes (#7585), so the trigger fired. The escapes were RE-MEASURED on this head rather than assumed from the commit title: \u{000d} and \u{0000} each yield exactly one character, of codepoint 13 and 0. CR and NUL are now DIRECT witnesses (a%00000db, a%000000b) and both join the output-always-safe control, so the whole requested hostile set is witnessed against the real encoder with no argument from escape-branch genericity standing in for any member. The encoder needed no change -- the genericity argument the boundary rested on turned out to be correct, which is exactly what direct evidence was owed to show. 24/24 green. The note is kept as the receipt that the boundary was declared, triggered and discharged rather than quietly dropped. Also merges current main (4 commits). One conflict, in dag/extdeps/realization/artifact_store_fs.dag: this branch moved ContentHash to std.content_hash while main added std.access {Permit, Deny} from the access-kernel change. Resolved as the union -- both wanted, neither superseding the other. * WIP: gunbc oracle * Merge main (15 commits): repoint four more ContentHash consumers, re-sync the inert roster Same merge class as the last push, caught this time BEFORE pushing by running the whole-tree compile rather than only the marker census. ContentHash home. Four more files main added import ContentHash from std.types, which Phase A moved. Repointed onto the family member their values actually inhabit, not a bare import swap: - gunbc.guarantee_measurement probe_set_digest is folded from content_hash_atom / content_hash_tagged / content_hash_combine, so it is Fnv1a64Structural. Its fold also had to move to the _structural variants, because Phase A DELETED the union-level combine and content_hash_tagged takes a structural payload while returning the union -- the union simply does not typecheck at this position. - gunbc.stage0_rust_honest_frontier_projection and both witnesses carry the same manifest_content_identity field as the previous batch; their "witness-abc123" String casts became Fnv1a64Structural records with valid 16-hex digests. Field rename collision. This branch renamed tested_base_tree -> tested_base_tree_hash and merge_target_tree -> merge_target_tree_hash alongside the GitObjectId retype, and main's #7583/#7619 lane added new callers on the old names. Updated those call sites (dag/tools/merge_admission_current_context.dag and main's new tests in merge_admission_attempt_witness_test.dag). FLAGGING FOR THE OPERATOR: the rename is incidental to this PR's purpose -- only the retype was required -- and it is what made these collisions instead of clean merges. It is kept because the record's sibling field was already base_tree_hash, but it is a fair thing to ask me to revert. The merge_admission witness import conflict resolved as the UNION: this branch's three Phase A symbols plus main's two roster helpers and its new commit_workflow import. All six are used in the file body and all six are declared. Inert roster re-synced, both directions of the check firing as designed: - DownstreamSupportRoster (#7571) is newly inert -- declared, named in plan prose, constructed and read by nothing -- so it is rostered. - AccessPolicy is no longer inert: main's std.effect_grant effect_grant_policy is a real production consumer, so its row was STALE and is DELETED. That is exactly the dissolve the row's own trigger specifies, not a hand-edit. The roster now equals the live inert set exactly. Verified on a binary rebuilt AFTER the merge (main touched src/v1, so the pre-merge binary was not a valid oracle): whole-tree compile 0 blocking errors, regen_divergence_count=0, and green suites -- merge_admission 28/28, guarantee_measurement 9/9, honest_frontier 7/7, lifecycle_scaffold 28/28, emitter poles 7/7, roadmap 39/39, c_compilation_unit 24/24, compilation_unit 15/15, inert_carrier 4/4. * Merge main #7608: ground the new GitSha1ObjectId fixtures on Sha1Digest Phase A made GitObjectId's digest a Sha1Digest record rather than a raw hex String, and main's new commit_writer_admission witness constructs GitSha1ObjectId { digest: "1111..." } directly. Both fixtures now use the tree's existing idiom, Sha1Digest { hex: <40 hex> as Sha1DigestHex }, with the carriers imported from std.content_hash. The object_store.dag import conflict resolved as the union: this branch's Phase A content_hash block plus main's two new imports (PositiveInt, repeat_string). BLOCKED, and NOT worked around: dag/gunbc/commit_workflow.dag fails to compile with "no field 'path' on type 'T'" at commit_writer_index_entries_for_path. This is NOT this branch's defect and it is deliberately left alone rather than papered over with a speculative type annotation (DESIGN section 5: noticing you are implementing a workaround IS the line-stop signal). Evidence it is main's: - the file is BYTE-IDENTICAL to origin/main here; - it reds in its OWN narrow closure, not just whole-tree, so it is a real defect rather than a resolution artifact; - this branch's only 04_infer changes are where-predicate registrations (lower_hex_*, oci_other_digest_*), which cannot affect lambda parameter inference; - main's CI for #7608 (f3df2ce) was still QUEUED when this merge happened, and three of the preceding main commits are outright red, so the commit landed unverified. Hypotheses tested and REFUTED by execution, so the next person does not repeat them: trailing comma in the parameter list; filter over an imported record type (both compile clean in an isolated probe); a shadowing filter declaration; a lambda/parameter name colliding with an imported symbol; cross-call-site unification collapsing the element type (only two callers, both passing List<GitIndexEntry>). The sibling flat_map over the same type and the same `entry` binding compiles, so it is specific to this call. * WIP: gunbc oracle * Remove cw_probe.dag: a scratch bisect probe the auto-commit swept into the branch Not source. It was a copy of commit_workflow.dag under a probe module name, used to bisect the 'no field path on type T' failure to its cause, and it should never have been committed. * Unblock the compile-clean gate: declared scaffold for the filter name capture, two more ContentHash homes THE BLOCKER, root-caused by bisection rather than guessed. dag/gunbc/commit_workflow.dag failed with "no field 'path' on type 'T'". src/v2/std/algebra.dag declares fn filter<T>(xs: FreeMonoid<T>, predicate: fn(T) -> Bool). commit_workflow does NOT import v2.std.algebra -- but it imports v2.compiler.source_authority, which drags the whole v2 compiler closure including v2.std.algebra into the module POOL. The bare name filter then binds to that declaration instead of the builtin, List<GitIndexEntry> does not unify with FreeMonoid<T>, the lambda parameter stays unbound, and the module reds. Discriminating measurement: importing v2.std.algebra for `length` ALONE -- never filter -- reproduces it, and deleting only the source_authority import makes the original filter form compile. So this is name capture by POOL MEMBERSHIP, not by the import list: DESIGN #6985 Class B in its inverting direction, and silent -- nothing reports that filter rebound. Refuted by execution before landing anything, recorded in the carrier so nobody repeats them: trailing comma in the parameter list; filter over an imported record type; List not imported; two filter calls over different element types in one module; a lambda or parameter name colliding with an imported symbol; cross-call-site unification. The import cannot be dropped -- ModuleStorageBinding, ParsedFromSource and ProducedByBehavior are all genuinely used -- so the only local repair routes around the capture. Per DESIGN section 5 that is a WORKAROUND and may only land as a DECLARED SCAFFOLD, never a quiet respelling: the body selects with flat_map (the spelling the sibling function already uses over the same type with the same binding), and commit_writer_index_filter_capture_scaffold states the root cause, the discriminating measurement, the refuted hypotheses, why the import cannot be dropped, and the dissolve-on -- the namespace-only resolution lane, after which the filter spelling is restored and the row deleted. Behaviour is unchanged: it selects exactly the entries whose path matches. commit_writer_admission_witness_test 13/13 exercises admit_commit_writer, which calls this function, so that is verified by execution and not merely by compiling. This is NOT this branch's defect. It is fixed here because it reds main itself and every job on this PR, and main landed #7608 while its own CI was still queued. Also: two more files from main's #7623 import ContentHash from std.types. Same manifest_content_identity field as the two prior batches, so same grounding onto Fnv1a64Structural, with the contract fixture becoming a valid 16-hex digest. Whole-tree compile 0 blocking errors; regen_divergence_count=0; heal no drift; commit_writer_admission 13/13; live_rust_observation_contract 12/12. --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.com> Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
…air, probe-adequacy mandate (#7643) * WIP: compiler correctness * Bind the guarantee-recovery analysis into the doc graph The analysis note landed as an orphan doc: gunbc.doc_graph_roots states that "an unbound doc is an orphan, loudly", and CI duly refused at be1a001 with doc_graph_has_no_orphan_docs returning false in both the dag/test/claim and src/v2/lens consumers. Registered as two HandAuthoredDocBind rows rather than one, because the analysis binds to two independent carriers and they dissolve on different triggers: - v1.compiler.infer module_skips_direct_call_arg_check — the one named violation of the dimension contract's "no escape hatch" clause (docs/thesis/correctness-dimensions.md), exempting v2.* and v1.compiler.* from direct-call argument checking. - v2.std.constraints solve_constraints — passes graph.root as source_facts, algebra AND the sole candidate, so the grounding proof reduces to well_formed(root) and is relabelled CanonicalGrounding. Green by execution, both directions: RED is the CI failure at be1a001; GREEN is all five witnesses in dag/test/claim/doc_reachability_witness_test.dag plus doc_graph_is_clean in src/v2/lens/doc_reachability_test.dag passing locally against the live docs/ tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Reconcile the gap analysis against the independent review — three corrections adopted, receipts verified Adopted (all verified on main this pass): - Cardinality reclassified UNEXPRESSIBLE -> RepresentableButForgeable, not statically propagated: v2.std.refinement exists, NonEmptyList fixture + green cardinality_fold_propagation_test exist, and refined_vacuous_stub_pack's Rejected arm returns Refined { base } (the carrier proves nothing). New Sec 4b: the operator independently re-directed this exact guarantee on 2026-07-04 (interface-summary-declared-use-arity.md Sec 3.1, "hard error in the language") — the intent is not lost; the lattice design pass (FLAG E) never started. - Failure history rewritten (Sec 2): the exemption dates to 2026-06-08 (a13fb57), pre-bankruptcy; correctness-dimensions.md marked type safety "Yes (blocking)" while return position was unchecked — so the ledger overstated, then the auditable contract was deleted. The pipeline_steps_empty_arm_note receipt is withdrawn: empty there is a deliberate total semantics, not a priced-out wall. - Status vocabulary widened to the review's 11-state lattice; v2 terminal calibrated (validate_then_compile door + loop-bound wall are real; InferredTree is still not a proof boundary); application-arity row added (formal-driven walk, positional fallback for misspelled labels, ArityMismatch is constructor-arity); PatternLookupBlocked's silent [] arm confirmed (PatternDynamic does diagnose — review corrected there). - Sec 7b: DESIGN.md is projected from gunbc.design_document, and its "5 behaviors" is stale against v2.std.node's six (Match) — the guarantee authority lands as .dag rows, never hand-edited prose. - Sequencing reconciled to 7 stages: claims authority + expecting-red probe corpus together; zero-resolution method wall now, ambiguity wall census-first; cardinality vertical slice third. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Status header: two audit passes complete, open items typed Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Align the bind's dissolution trigger with the doc's own authority model (review 45299) The first HandAuthoredDocBind trigger said "re-homed into DESIGN.md as its specification half" — wording that predates the reconciliation pass's Sec 7b finding that DESIGN.md is a projection of gunbc.design_document. As written, a direct DESIGN.md edit could have satisfied the trigger, which is exactly the Sec 3 parallel-representation failure Sec 7b names. Trigger now requires .dag claim rows projected via gunbc.design_document and states explicitly that a hand edit does not satisfy it. All five doc-reachability witnesses re-run green by execution after the edit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Address review 45305 (merge same-slug binds, fix stale block) + land the safety ladder as the organizing frame Review 45305, both findings verified correct and fixed: - doc_graph_roots: the two HandAuthoredDocBind rows shared (home, slug), which the carrier's own note defines as the symbolic identity — one doc had two independently removable authority rows. Merged to ONE row whose trigger anchors both carriers (module_skips_direct_call_arg_check, solve_constraints) and gates dissolution on BOTH conditions, with the merge provenance recorded on the carrier. (Observed, not fixed here: module-identity-storage-binding-design and accelerator-demo-roundtrip also carry same-slug duplicate rows — pre-existing, follow-up material.) - Sec 8b's example-0 block still said "unexpressible", contradicting the Sec 4 reclassification and mis-aiming the archetypal RED at inventing a carrier instead of sealing/propagating the one that exists. Rewritten: the RED exercises unforgeable construction + seam propagation, expected refusal at the 0..n -> 1..n seam. Operator direction, same pass: the safety ladder is now Sec 1b, the organizing frame — R3 structurally-impossible / R2 structural guarantee / R1 testable / R0 mitigatable / below-the-floor silent (forbidden, Sec 5). Three rules: floor absolute; climb to a STATED ceiling (mathematical / capability / price — the capability ceiling is unforgeable construction, blocked on reference-level visibility: the keyword set has no private/sealed/opaque); reported rung == measured rung, lens-checked for inflation and stalls. Includes the specimen table (the session's classes placed, cross-representation == as the exemplar full climb) and the non-goals roster (external reality, arbitrary predicates, budgets, optimality, self-governance, byte-identical self-emit — low ceilings BY DESIGN). Stage 1 claim rows gain current_rung / ceiling / next_rung_trigger. All five doc-reachability witnesses re-run green by execution after both file changes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * WIP: compiler correctness * Ladder follow-up: adopt the post-merge verdict (8 corrections) + the guarantee-ladder roadmap section Corrections, each verified against main before adoption: 1. sole_constructor EXISTS (SoleConstructorViolation, sealed-record specimen) — the DESIGN 4b capability claim ("no private/sealed/opaque ... every proof-carrier is presently forgeable") was false as stated; corrected to an audited-status claim: sole_constructor is the candidate wall, completeness for generic carriers unverified. The earlier keyword-set inference is withdrawn in the Sec 10 ledger. 2. Subject grain: rung honesty is measured at a declared acceptance boundary; a class's rung is the MINIMUM across in-scope paths (the interpreter refuses the mislabeled call that order_typed_call_args reorders for emission). DESIGN 4b meta-obligation 1 amended; Stage-1 carrier gains subject_grain/acceptance_boundary/compile_mode/ realization_target/covered_population. 3. Seed rungs demoted: return/data/generic, field-through-generics, exhaustiveness, cardinality, full ==-class, and L4 all to UnknownUnmeasured (compile admission proven is not runtime disposition proven); census marked specimen-denominated; unknown- method R0 scoped to the interpretation path. 4. Dissolution on climb amended in DESIGN 4b: production handling dissolves; the RED + positive controls REMAIN enrolled as the evidence the higher rung stays real. 5. HandAuthoredDocBind.work -> works: List<DeclarationRef> (40 rows + witness-test fixture migrated); the guarantee-recovery row now carries BOTH anchors typed, not one typed + one in prose. Carrier note records that List admits [] — the exact cardinality gap the ladder tracks — with the doc-graph witnesses as the interim wall. 6. cardinality_fold_propagation_test relabeled everywhere as manual value-level specimens (length homomorphism over literals + runtime refine_byte); "not new design" softened to the accurate scope statement; the roadmap cardinality node re-briefed accordingly. 7. Sec 8c recast: TypeBinding carries two bespoke coordinates, not a generic dimension mechanism; extension-vs-redesign is an open audit question that roadmap pricing must carry. 8. Sec 1 "was not built" -> "never completed as an exhaustive acceptance contract"; Sec 11 queue updated (correctness-dimensions done; sole_constructor completeness audit added). Additions (operator direction): ROADMAP gains the "Guarantee ladder — climb plan (DESIGN 4b)" section — 13 sized, unowned, dispatchable nodes in ticket format with dependency edges (probe corpus gates the four floor walls; carrier gates cardinality slice, emitters, prevalence; exemption removal gates on the call-shape + inhabitance walls). The capability node is the sole_constructor completeness audit. State-vs- work split recorded on the carrier: rung STATE lives in the Stage-1 claims carrier and is emitted (ladder-census-emitters node); roadmap nodes track CLIMBS. Verified by execution: main_wet regen (DESIGN.md + ROADMAP.md projections, never hand-edited); drift 4/4; doc-graph 5/5; roadmap authority 35/35, model 9/9, focus 12/12. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give works its executing consumers (review 45336): nonempty wall, symbol fields, two-anchor pin, RED control review 45336 was correct: works had a typed carrier and zero readers — representation without a consumer is specification-without-execution (DESIGN 5 / E-10), the exact defect class the guarantee analysis documents, reproduced in its own fix. Consumers now executing in dag/test/claim/doc_reachability_witness_test: - doc_graph_binds_works_all_nonempty — an emptied works list reds - doc_graph_works_refs_carry_symbols — a ref stripped of module_path or decl_name reds - guarantee_recovery_bind_pins_both_anchors — deleting or renaming either of the two anchors (module_skips_direct_call_arg_check, solve_constraints) reds; row multiplicity pinned to one - doc_graph_works_empty_red_control — synthetic empty-works bind fails the predicate, proving the consumer discriminates Predicates live on the authority (gunbc.doc_graph_roots) so the witness consumes the carrier's own definition. Residue named on the carrier note: staleness against the live tree (a ref naming a decl that no longer exists) is NOT witnessed — v1.compiler.* is outside the witness compile pool, so ref-vs-tree resolution is exactly the feature:cited-symbol-resolution lens DESIGN 3 already names; the refs are symbolic citations and inherit that trigger. All 11 doc-reachability witnesses green by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * De-inflate the three climb-node headlines (review 45349): work nodes name the target rung; current rung defers to the census review 45349, third correct catch in this lane: the census demoted method existence (R0 interpretation-path-only), inhabitance (UnknownUnmeasured), and cardinality (UnknownUnmeasured) — and the roadmap nodes, authored before the demotion pass, kept "R0 -> R2" headlines, re-inflating the same claims the same day at the canonical authority. The section's own note says rung STATE lives in the claims carrier, never these nodes; the headlines now name only the TARGET rung and point at the census for current state, per DESIGN 4b's minimum-across-paths rule. ROADMAP.md regenerated via main_wet; roadmap authority witnesses 35/35; drift witnesses 4/4, by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * chore: regenerate drifted generated artifacts (ci auto-heal) * Ladder nodes join the declared roadmap graph; binds nonempty by construction; rung state derived, never stored Executes the operator's 10-item merge bar on #7489 plus reviews 45356/45367 and tidy-deer-730's measured receipts: - guarantee_ladder_section() deleted; 16 nodes + 23 edges enter declared_roadmap_nodes()/declared_roadmap_edges() via guarantee_ladder_nodes()/ guarantee_ladder_edges(), owner "compiler-guarantee" (lane identity, unbound until closing contracts). Page visibility is the typed focus policy (lane added to roadmap_focus_selection). rendered⊆declared∪derived witnessed with a synthetic-ghost RED. - Graph corrections: probe corpus → carrier → baseline-prevalence → walls; prevalence split baseline/residual; new floor-generic-field-constraint-wall and floor-method-ambiguity-wall nodes; primitive-identity-join is a PREREQUISITE of the general method wall (measured: kernel algebra profiles vs interpreter dispatch fork, tidy-deer-730 on gunbc#7484); cardinality ← sole_constructor audit edge; capability node repointed off the parked visibility-grants doc. - Tickets de-stated: no current-rung transcription anywhere; carrier ticket rewritten to the four-carrier split (Requirement/Path/Measurement/derived Disposition, minimum across paths, no stored rung field) — reconciled across §12 Stage 1, DESIGN §4b tail, and the roadmap node (review 45367); five recovered vocabularies kept orthogonal. - HandAuthoredDocBind: primary_work + additional_works (zero-anchor bind unwritable); empty-works RED deleted with its validation, residue named; duplicate (home,slug) rows merged; bind-identity uniqueness witnessed with a synthetic-duplicate RED. - Census: method-existence subject-grain receipt (narrow kernel wall, gunbc#7484); parser silent-separator below-floor row; §11 items 6-8; §10 fourth-pass ledger. Witnesses: roadmap 37/37 (2 new), identity 9/9, focus 12/12, model 9/9, drift 8/8, doc-graph 11/11. ROADMAP.md/DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Trim the three over-budget ladder briefs to the operator's 100-word ticket law witness_ticket_brief_budget_holds_and_reds red on the CI floor: the carrier, method-existence, and cardinality briefs ran 169/128/111 words. The old section-local placement had escaped this law entirely (the exact ghost-universe defect the verdict named — the budget never saw those nodes); in the declared graph it applies. Briefs trimmed to 94/91/90 with every cut fact already carried in the gap analysis (sec 12 Stage 1b / Stage 2 amendment / the census), which each node links as its carrier. The budget itself is untouched — widening the declaration to satisfy the check is the DESIGN 5 tell, backwards. Page set 28/28, authority set green, regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Containment predicates consume doc_all_nodes, the one canonical walker (review 45412) document_rendered_nodes was a traversal fork beside roadmap_spawner's doc_all_nodes — same semantics, second walker. The predicates (whole-value ghost count + both RED probes) move INTO roadmap_spawner, the walker's module, because the spawner already imports roadmap_authority and the reverse import would cycle. The authority sheds the walker and its now-unused SectionElement imports; the containment note records both refused first cuts (identity-only membership, review 45406; the duplicate walker, review 45412) since each was this wall violating a law it enforces. Authority 38/38, spawner 16/16, page 28/28. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Post-merge verdict follow-up: open-candidate honesty, anchored baseline, FrontierAccepted, and the closure door Executes all six items of the operator's post-merge verdict on #7489, each verified against live state first (#7484 and #7485 confirmed OPEN; the anchor confirmed as the #7489 squash; Behavior confirmed six-membered): 1. Every "#7484 landed" claim replaced with open-candidate wording — main's disposition stated separately from candidate branch evidence (the ladder's rung-inflation rule applied to open-PR state; my transcription error). 2. Baseline prevalence anchored: anchor_commit 6c6e2dc (content-addressed, reproducible after in-flight merges; walls no longer race a live tree). 3. GuaranteeDisposition gains FrontierAccepted{diagnostic, accepted_boundary, evidence} — typed/located/counted but still Accepted; specimens MethodExistenceUndecided and GroundingNotDerived. 4. Graph: floor-parse-formation-wall + floor-record-construction-wall + compiler-accepted-obligation-closure added; v2-phase-carriers split into five staged nodes (self-grounding frontier → Translate refusal → inferred- tree completeness → per-kind derivation coverage → target realization gate) with the registry's FIRST TOMBSTONE (superseded_by the frontier node); method←join edge deleted per the zero-via-union nuance (join gates only the >1 wall and realization completeness); residual reroutes through the closure door. 5. DESIGN §4: closed vocabulary corrected to 6 connectives + 6 behaviors, matching v2.std.node.Behavior (the decidability denominator). 6. §1d provisional guarantee grid emitted as hand-authored interim, dissolve-on the carrier-emitted projection. Witnesses: authority 38/38, identity 9/9 (first tombstone passes the count-free tombstone claims), focus 12/12, model 9/9, page 28/28 (all 23 ladder briefs within the 100-word law), spawner 16/16, drift 8/8, doc 11/11. ROADMAP.md and DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * chore: regenerate drifted generated artifacts (ci auto-heal) * Route the ambiguity wall and cardinality seam through the closure door (review 45545) The first edge set let compiler-accepted-obligation-closure land while floor-method-ambiguity-wall and cardinality-vertical-slice stayed open — the door would have certified "every required judgment established" over two required-open judgments (the grid marks the cardinality seam P0.2 minimum-R2 and ambiguity part of resolved identity; the verdict's spine routes ALL P0 obligations through the door). Both are now prerequisites of the closure; residual prevalence depends on the door alone. Authority 38/38, focus 12/12, page 28/28, drift 8/8; regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Reconcile the sec-7b behavior-count passage to past tense (review 45558) Sec 7b still described the 5-behaviors drift as current after this PR corrected the authority — the stale-claim problem the PR closes elsewhere. The passage now records the drift as found-and-corrected, keeps the specimen's evidentiary value (the denominator drifted silently in prose), and leaves the Match-promotion adjudication question with the queue. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Remove probe demo scaffolding (net-zero vs main: files added by autocommit sweep mid-run, deleted after measurement) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Call-shape wall: refuse unknown argument labels and surplus positionals at the direct-call seam, mirroring the runtime contract The compile seam was silent on both classes call_function_inner refuses at runtime, and the emitter reordered mislabeled args positionally — two realizations of one program disagreeing silently. direct_call_shape_diags (v1.compiler.infer) closes both, blocking, exemption-free (a label has no representation gap). Census before landing refused 28 live rename fossils in 5 fns (to_string i->value, arm_body, is_import_slot_node, fold_list init->empty, path->path_opt), all relabeled to their declared authority; +3 fixed in the measured sig-unresolved blind spot. Probe pair pre/post, enrolled ct_call_shape_wall_witness_test RED/controls, regen fixed point divergence 0, whole-corpus compile-clean 0 blocking. Duplicate/missing stay unwalled with triggers (interpreter-first parity pair next). Roadmap node + census rows amended; ROADMAP regenerated. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * chore: regenerate drifted generated artifacts (ci auto-heal) * Roster the call-shape witness blob in the scaffold index (review 45655) ct_call_shape_wall_witness_test joined compiler_tests_rust without its LanguageSourceScaffoldRow, so the exact-equality enrollment witness (compiler_tests_rust_blobs_are_all_rostered, 29 declared vs 28 rostered) would red on CI. Row added with the same hand-assertion scaffold trigger as its peers and enrolled in the roster; witness re-run green by execution. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Repair the silent-red ord-eligibility wall: name-grain arms admit only childless nodes d975e10 (2026-07-21) moved Symbol onto the name-only opaque-alias roster, dropping the shape check its enrolled negative control pins — Symbol<Float> became BTreeSet-eligible by name, and the RED sat invisible for ten days because the Rust unit suite left CI on 2026-07-11. Childless gate restores the shape constraint (zero corpus impact; regen fixed point holds); incident + dark-suite evidence gap filed as gap-analysis sixth-pass ledger + queue item 9 (operator decision, priced by this incident). Found by tidy-deer-730 during the 7484 main integration. Suite: 30 passed / 0 failed (was 1 failed). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Dedupe the call-shape witness aggregator entry after the main merge The merge auto-combined both sides' insertions of ct_call_shape_wall_witness_test into compiler_tests_source(); a duplicate generates the #[test] twice. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Spine reconciliation: recut the merged P0 slices at their actual grain, add the measurement-schema stage, split the acceptance door Adopts the operator spine verdict (2026-08-01, seventh pass) into the roadmap authority and the gap analysis: - ladder-measurement-schema precedes probes AND carrier (the receipt protocol both meet through; breaks the probes/carrier protocol cycle). - The three merged P0 slices recut at their actual grain, identities tombstoned: floor-call-shape-wall -> call-label-and-surplus-wall (accepted, #7519) + missing/duplicate + signature-resolution siblings; floor-method-existence-wall -> method-established-surface-wall (accepted, #7484) + receiver-normalization + zero-resolution siblings; floor-inhabitance-wall -> declared-conformance-ground-fragment (accepted, #7484) + grounding + general-wall siblings. - The Accepted door split mechanism/floor/extended (compiler-accepted-obligation-closure tombstoned): the audit form lands with the carrier; refusal never turns on over a known-open judgment (review 45545's substance preserved in the activation nodes). - Exemption removal re-grounded on argument-type-compatibility grounding + declared-conformance grounding (labels never gated it). - guarantee_ladder_edges rewritten wholesale; emitters parallel with the baseline; baseline defined as a two-revision execution. - Gap analysis sec 12 updated in place (Stage 0/1a/1c/2-amendment/4/6/6b); stale dissolution triggers repointed (doc_graph_roots, doc_reachability_witness_test); tombstone-note staleness fixed. - ROADMAP.md regenerated via main_wet; roadmap witness receipts 100 PASS (brief budgets, edge endpoints, acyclicity, identity registry with five tombstones); regen_stage0 --verify divergence 0. The branch additionally carries the ord-eligibility silent-red repair (childless gate on name-grain arms + incident note) and the clean regen of the generated stage0 files after the origin/main merge. Known pre-existing: the whole-tree cold census refuses 23 ambiguous-reference diagnostics in dag/test/claim/occurrence_binding_resolve_witness_test.dag (landed with #7508, byte-identical to origin/main; handed off to the occurrence lane). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Recut the extended activation as per-class admissions (review 45918) The first cut kept requires-all edges on one extended-activation node while its prose promised class-by-class widening — the graph would have deferred every admission behind the slowest climb, preserving the monolithic deferral the door split dissolves. Now: four per-class admission nodes (extended-admission-cardinality/-ambiguity/-v2-realization/-v2-translate, each <- floor-closure + its own climb, ready the day that climb lands) and accepted-extended-obligation-closure recut as the terminal roster-completeness certification, where requires-all honestly belongs. Same closure identity (no slug change, no tombstone); four fresh identities minted. Stage 6b + seventh-pass ledger + lane note updated; ROADMAP regenerated; graph/budget/identity witnesses 26 PASS. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Trim the ord name-grain note to its structural constraint (review 45929) The in-code note duplicated the incident narrative the gap analysis already records (sixth-pass ledger + queue item 9) — a parallel ledger realized into the emitted seed with no executable consumer. The carrier keeps only the constraint the code cannot show: why name-grain arms admit childless nodes only, the discriminating RED's symbol, and the shape-examining sibling path. regen_stage0 divergence 0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Spine A Stage 0: the guarantee measurement schema — evidence identifies its subject before anyone measures gunbc.guarantee_measurement carries the vocabulary probes and claims meet through, and nothing else (roadmap node ladder-measurement-schema; operator spine verdict 2026-08-01): GuaranteeClassId/PathId/ProbeId brands; GuaranteePath over four closed minimal axes (subject grain, acceptance boundary incl. the InferToEval/InferToTranslate phase boundaries the containment workstream consumes, compile mode, realization target with GuaranteeTargetName deferred-grounding brand); GuaranteeMeasurementReceipt with every field required (subject_revision x harness_revision x probe_set_digest, reusing std.types.CommitSha and std.content_hash); ProbeObservation as the raw outcome sum with ProbeNotRunnable structurally separated from verdicts (top-as-ignorance never readable as pass/fail); exactly-one path resolution and a receipt->path join that refuses unknown and duplicate. Registry mechanism without a registry population - no probe executes, no class rows, no disposition, no rung. An initial ObservedOutcome name collided with gunbc.output_policy's process-outcome type (whole-tree census caught the bare-reference break); renamed to ProbeObservation, census back to 0 blocking. Receipts: 8/8 synthetic-row witnesses green by execution (round-trip join, unknown-path refusal, duplicate-registry refusal never-first-pick, exactly-one resolution across four boundary variants, both uniqueness REDs, digest input-determinism incl. order sensitivity, verdict/ignorance separation); whole-tree compile 0 blocking; regen_divergence_count=0; generated artifacts zero drift. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Record the second-consumer re-grounding trigger for observed_is_verdict (review 46075) The predicate/walker dissolution rule triggers where a canonical fold already exists (nat_cata) or a substrate walk is extended; neither holds for a freshly declared domain sum whose only query this is. The note now records the named trigger: when the claims carrier lands as the sum's second consumer, a probe_observation fold becomes the canonical surface and observed_is_verdict re-expresses through it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Grant publication for the eight ungranted #7544 files (main-side gate breakage) The publication gate reds on current main itself: #7544 (heal-revalidation) merged after the P-B wall landed via #7560 but its CI raced the wall, so its eight new files carry no PublicFilePublishGrant rows and every PR merging current main inherits the failure. Rows added for all eight (mechanical placement declarations for files already public on main); cutover..HEAD Added/Copied/Renamed set now fully rostered, gate witnesses green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Grant publication for the three ungranted #7563 files (second main-side race) Same class as the #7544 fix one commit ago: #7563 merged on a pre-wall CI run, adding three SCM-kernel files with no grant rows. Roster now covers the full cutover..HEAD set including current main. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Thread GuaranteePathId through resolution and its refusal variants (review 46179) The resolver's key and both refusal-variant payloads carry the brand end-to-end; join_receipt_to_path no longer erases receipt.path to String. Measured the enforcement honestly: two executed controls show the checker accepting a bare String at a branded parameter and a branded record field, so the note records this as model-correctness and erasure-removal, with brand acceptance-enforcement handed to the probe corpus as its own class. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Merge origin/main; dedupe the roster union and grant the two #7550 lean files The alphabetized roster body on main already carried the 11 straggler paths, so #7580's tail block duplicated every one of them; the union keeps exactly one row per path, with this branch's two guarantee rows slotted alphabetically. Coverage against the cutover then caught a fourth race instance: #7550 merged two new files with no grant rows (dag/extdeps/languages/lean/overflow.dag and its witness), redding main's gate again - swept into the same roster here. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Observation counts are Nat, with the enforcement gap measured (review 46287) RefusedTyped.count and AcceptedCounted.count carry the cardinal type, and the fold's arm signatures follow. An executed control shows the checker still accepting a negative at the Nat field today, so the note records the swap as model-correctness with refusal owed to the numeric-refinement acceptance class, not claimed as a wall. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Orthogonalize the path axes instead of enumerating families (review 46308) InterpreterRun renames to RuntimeRun: run-level acceptance happens IN the path's realization, so which runtime is the realization axis's fact and an emitted-run path (the divergence probes' subject) is expressible rather than contradictory. The compile_mode axis deletes: every landed control derives its pipeline from its boundary, so the stored mode was a second representation whose only writable novelty was the contradiction; it returns as a stored axis with the first path measured under two pipelines at one boundary. Both review-named contradictions are now unwritable without a family coproduct, whose rows would restate the orthogonal axes per combination (the N-by-M shape DESIGN 2 folds into axes). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Roadmap: schema acceptance receipt, axis-prose repair, probe-adequacy mandate Three post-merge obligations from the ladder-measurement-schema landing (gunbc#7572, merged 2026-08-01): - RoadmapAcceptanceReceipt for ladder-measurement-schema: executed red-control (duplicate_class_id_reds_uniqueness) + delivered handback (the schema module and its witness), criteria digest pinned over the corrected boundary text; the node leaves the active graph and the probe corpus promotes to lane top. - Axis-prose repair (snappy-eagle's prose-grep rule): the schema and carrier boundaries plus gap-analysis sec 12 no longer name the deleted compile_mode axis; each records the RuntimeRun re-read and the deletion's re-entry trigger instead (review 46308 on gunbc#7572). - Probe-adequacy mandate in guarantee-baseline-prevalence red_control: closure AND shape AND corpus-prevalence cross-check REQUIRED for every below-floor or silent-class row; a row without its adequacy receipt is unenrollable. ROADMAP.md regenerated via main_wet on the artifact gate; roadmap authority suite 39/39 by execution. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Reconcile the schema node's acceptance bar to what Stage 0 owns (review 46861) The red_control claimed receipt-field unwritability - a wall that was never this node's to claim: corpus-wide construction enforcement is the floor-record-construction-wall class's bar, exactly as the module's receipt_identity_note states. The bar now says required-by-shape with enforcement explicitly delegated, the criteria digest re-pins over the honest text (74da4d8be7125c81, derived by execution), and the receipt stands on the executed duplicate-id control. Also removes a stray digest-probe test fn a background sweep had committed mid-measurement. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Trim claims-carrier boundary under the 100-word ticket-brief budget; drop probe scaffolding The compile_mode de-reference added in this PR pushed the ladder-claims-carrier boundary to 101 words, redding witness_ticket_brief_budget_holds_and_reds (the enforcing witness for the boundary budget — CI batch 3). 'the landed ... row' reassurance prose becomes 'per gunbc.guarantee_measurement' (98 words); the single-authority pointer survives. ROADMAP.md regenerated. Also removes the transient probe_brief_violations diagnostics fn the autocommit sweeper captured (review 46970). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
Follow-up to #7486 (merged), doing the two things the operator asked: correct (the post-merge review verdict, all 8 items, each verified against
mainbefore adoption) and add (the guarantee-ladder climb plan as roadmap work) — then restructured per the operator's second verdict: the climb plan lives inside the canonical roadmap graph, not beside it.Disclosure: this PR changes the design and roadmap authorities
gunbc.design_document(→ regenerated DESIGN.md) andgunbc.roadmap_authority(→ regenerated ROADMAP.md). Both projections regenerated viamain_wetondag/tools/generated_artifact_gate.dag, never hand-edited.The climb plan, in the canonical graph (operator verdict, all 10 merge-bar items)
guarantee_ladder_section()deleted; 16 nodes + 23 edges enterdeclared_roadmap_nodes()/declared_roadmap_edges()viaguarantee_ladder_nodes()/guarantee_ladder_edges(), so they are counted, receipt-checkable, and covered by the identity/endpoint/acyclicity/active-set witnesses like every other lane. Page visibility is the typed focus policy (roadmap_focus_selectiongains the lane), not an out-of-mechanism placement.compiler-guaranteeon every node (owner = lane identity, not an assignee; nodes are unbound until dispatch binds a session and closing contract) — also resolves review 45356's REQUEST_CHANGES on the owner-less rows.field_of_type_varfabrication) and floor-method-ambiguity-wall (>1 resolution, after the join defines sameness); cardinality ←sole_constructoraudit edge; capability-audit node repointed off the parked visibility-grants doc.primitive-identity-joinis a prerequisite of the general method-existence wall, not a follow-on — the kernel algebra profiles disagree with interpreter dispatch (length/count/sizefork), which is what forces per-receiver walls narrow. Census records the landed narrow kernel wall at its honest subject grain.GuaranteeRequirement/GuaranteePath(per in-scope path, population derived or completeness-witnessed) /GuaranteeMeasurement(executed receipts) /GuaranteeDispositionderived per path (Unmeasured | BelowFloor | OnLadder | OutsideModeledGuarantee, folded to minimum-across-paths). No storedcurrent_rungfield exists, so a transcribed rung is unrepresentable. Reconciled across §12 Stage 1, DESIGN §4b tail, and the roadmap node; the five recovered vocabularies stay orthogonal (joined by class identity, never consolidated onto one axis).HandAuthoredDocBindnonempty by construction:primary_work: DeclarationRef + additional_works: List— the zero-anchor bind is unwritable; the empty-works RED deleted with the validation it backed (residue named on the carrier note: the compile-refusal probe belongs to the probe corpus's record-completeness class); the two remaining duplicate(home, slug)pairs merged; bind-identity uniqueness witnessed with a synthetic-duplicate RED.Corrections carried from the first verdict (all verified against
main)sole_constructorexists → §4b corrected to audited-status; subject grain = minimum across paths; seed rungs demoted toUnknownUnmeasured(census specimen-denominated); dissolution-on-climb keeps RED evidence; fold-test relabeled manual value-level; §8c recast; wording fixes. New this round: parser silent-separator below-floor census row + §11 items 6–8 (both parser defects + the two receiver-type resolution defects, from the gunbc#7484 lane's measured receipts).Verified by execution
main_wetregen (ROADMAP.md byte-stable against the auto-heal regen; DESIGN.md §4b tail re-projected) · roadmap authority 37/37 (2 new containment witnesses) · identity 9/9 · focus 12/12 · model 9/9 · drift 8/8 · doc-graph 11/11 (uniqueness + duplicate RED + two-anchor pin).🤖 Generated with Claude Code