Repository navigation
Repair publication roster: stamp 11 post-cutover paths from pre-wall branches (unblocks all PR CI) - #7580
Merged
Conversation
…om pre-wall branches Branches cut before the placement gate landed (#7560) merged to main carrying post-cutover Added paths with no publication decision, so the gate refused every subsequent PR merge ref. Stamps the 8 CI-heal/workflow paths and the 3 source-integration proof-kernel paths (PR #7563) Publish World — all public machinery. Wet publication_placement_gate_passes green over the repaired HEAD; all 8 hermetic gate probes green. The race class dissolves when the gate becomes a required branch-protection check. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 1, 2026
Brings 11 post-cutover PublicFilePublishGrant stamps from fix/publication-roster-post-cutover-repair; retains primitive-identity stamps for this PR's two new files.
2 of 3 tasks
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 1, 2026
…nly. The eleven post-cutover repair stamps belong on #7580, not hand-copied here. Batch-1 publication placement gate red until that PR lands. Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 1, 2026
Resolve publication_grant roster conflict by deduplicating the eleven post-cutover repair stamps from main with this lane's sole-publisher paths; keep main's post_cutover_race_repair_note. Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 1, 2026
Resolve publication_grant conflict by taking main's repaired roster and retaining dispatch-selection stamps for this lane's two post-cutover modules. Co-authored-by: Cursor <cursoragent@cursor.com>
This was referenced Aug 1, 2026
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 1, 2026
…n on main itself) origin/main 06d7aea lists the eleven pre-wall repair paths TWICE: once from #7565's branch-side enrollment block and once from #7580's repair block — the same enrollment race #7580's own note describes, re-entered by the next concurrent pair. The placement gate refuses repeated grants, so main is currently gate-red and every PR merge ref inherits it. This branch resolves the merge by keeping #7580's repair block (with its note) as the single occurrence and re-adding only this PR's own seven paths; publication_placement_gate_passes PASS by execution on the merged tree (42 unique rows, zero duplicates). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 1, 2026
Co-authored-by: Cursor <cursoragent@cursor.com>
6 tasks done
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 1, 2026
…an 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>
This was referenced Aug 1, 2026
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 1, 2026
…ation profile. Re-home publication placement onto std.authorization_profile.PublicationAdmissionRequest, model git Push/Commit transport shapes, and add read-only shadow replay — no live push path changes. Stamp sole-publisher roster paths deduped against main (#7580 repair rows and post-#7574 additions). Register design doc in doc graph roots with 2026-08-01 incident specimens. Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
added a commit
that referenced
this pull request
Aug 1, 2026
) Land std.primitive_identity carriers, derived four-surface census, refusal coproducts, canonical alias lookup, and 15 executing witnesses. Rebases onto main through c9dc667 (#7580 publication gate). Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.com>
3 of 4 tasks
briansrls
pushed a commit
that referenced
this pull request
Aug 1, 2026
…-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>
briansrls
added a commit
that referenced
this pull request
Aug 1, 2026
…ng preflight + ExternalModelScope carrier (operator verdict on #7556) (#7571) * WIP: DESIGN §3 external-upstream-decomposition subsection + extdeps modeling * chore: regenerate drifted generated artifacts (ci auto-heal) * DESIGN §3 external-upstream-decomposition + extdeps modeling preflight + ExternalModelScope carrier/gate (operator verdict on #7556) - design_document.dag §3: verbatim 'External upstream decomposition' subsection; DESIGN.md regenerated - gunbc.plans.extdeps_modeling_preflight: 8 typed preflight rows (single authority), registered Plan renders the table from them - extdeps.external_authority: ExternalSubjectRef/ExternalRevision/ExternalModelScope (citations nonempty by construction), FactAuthorityOverride.fact -> DeclarationRef; admit_external_model_scope gate with ForeignSubjectRow/ConsumerCoverageInUpstream refusals - gunbc.extdeps_scope_frontier: staged fail-closed enrollment — 2 carriers + 17 machinery-exempt + 397 counted frontier rows over all 416 dag/extdeps files; live-tree cover witness refuses unrostered or stale rows - extdeps.vendor.{microsoft,atlassian} adopt extdeps_model_scope (admitted by execution) - extdeps.browser: loud non-precedent disposition note naming the eventual split - dag/test/claim/external_model_scope_witness_test.dag: 12 claims incl. operator RED (generic browser + Chromium scope + Chrome|Firefox|Safari rows -> refused) and GREEN (shared shape + separate modules + downstream roster -> admitted); stage0 seed + ci.yml + plan doc regenerated Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Consume the module's own anchor in extdeps_model_scope (review 46077), qualified against silent same-name capture cursor review 46077: first_citation re-minted the anchor URI — parallel representation. Fixing it by BARE sibling reference was proven WRONG by execution: atlassian's bare extdeps_external_authority_anchor reference silently captured microsoft's same-named decl (first-occurrence-wins pooling; the duplicate-toplevel-decl fail-open, now witnessed on data decls). The landed spelling is the module-QUALIFIED reference (extdeps.vendor.<m>.extdeps_external_authority_anchor), single authority with no capture; the adopter witness now discriminates per-module citation locators so a future capture regression reds. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Regenerate ci.yml on merged tree (extdeps-modeling-preflight rows on top of main) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Roster the two extdeps modules main added mid-flight (review 46111): git/inspect + github/workflows, frontier count 397 -> 399 The live cover witness red exactly as designed on the merged tree; frontier claims re-run green (418 files = 2 carriers + 17 machinery-exempt + 399 frontier). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Rework carrier/enforcement per operator handback on #7571 (also codex review 46118) (1) ExternalSubjectRef carries a DeclarationRef (symbolic subject identity; vendor scopes point at their existing microsoft/atlassian declarations, no restated legal names). (2) module-grain revision removed — revisions belong on build/release/fact rows. (3) the synthetic function is no longer presented as an admission gate: renamed to the external_model_scope_decision KERNEL over DeclaredScopeFacts with a loud honesty boundary; the mechanical wall today is scope PRESENCE; subject-content-derived enforcement is the named frontier feature:extdeps-subject-content-derived (dissolves when a Node-tree projection derives DeclaredScopeFacts from the real module and feeds the same kernel). (4) the 399-row legacy population moved out of the semantic module into the frozen manifest dag/gunbc/legacy_extdeps_scope_frontier.tsv (one path per line, remove-only, count DERIVED by parse_frontier_manifest, exact bidirectional live diff enforced by the cover witness). (5) consumer coverage identity is DeclarationRef, not free text. 12/12 witness claims green by execution incl. the live 418-file cover against the manifest; stage0 seed regenerated; drift gates PASS. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: DESIGN §3 external-upstream-decomposition subsection + extdeps modeling * Consume std.roster_frontier's declaration_ref_eq instead of re-minting it (review 46136); register std_roster_frontier.rs in the seed roster Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: DESIGN §3 external-upstream-decomposition subsection + extdeps modeling * Merge main; enroll publication grants for this PR's 6 added paths + 11 ungranted main-side additions (publication_placement_gate green) The new Stage-0 publication wall (P-B) requires a PublicFilePublishGrant row for every path added after the cutover commit. This PR's six additions are enrolled, plus the eleven paths merged to main since cutover without rows (heal_revalidation, source_integration_proof_kernel, workflow-dispatch, github/workflows lanes) — main's own floor is red on the gate without them, and the roster is one shared carrier. publication_placement_gate_passes PASS locally by wet execution. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Make the presence wall mechanical (codex review 46215): carrier rows content-verified, manifest frozen against a git anchor Half 1: scope_carrier_paths membership was path-asserted; the cover witness now filesystem_reads every carrier file and refuses one whose bytes lack the extdeps_model_scope declaration (declared text-scan scaffold, corpus_scan precedent, dissolves with the storage-grain frontier). Half 2: the manifest's remove-only lifecycle was review discipline; every manifest row must now name a file that existed at the pinned legacy_manifest_freeze_sha — the witness diffs freeze..HEAD via git.Core.DiffNameStatus (the publication-gate pattern) and refuses any manifest row in the added/copied/renamed set, with diff failure and parse truncation typed as refusals (PostFreezeObservation coproduct), never skips. 17/17 claims green by execution. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: DESIGN §3 external-upstream-decomposition subsection + extdeps modeling * Split the wet live observations out of hermetic discovery (d4bef96 floor red) Hermetic discovery executed the three wet-only fns (Filesystem.List walk, git.Core.DiffNameStatus freeze diff) against the mock corpus, where those operations are unpublished — ReadsLiveTree does not exclude fns from discovery. Structural fix, not a widened mock: - pure decision fns (scope_cover_holds, carrier_content_declares_scope, PostFreezeObservation, manifest_freeze_holds) move to their single authority gunbc.extdeps_scope_frontier; the hermetic witness imports them (also discharges cursor review 46245 both findings) - new dag/test/claim/external_model_scope_live_cover_witness_test.dag (ReadsLiveTree) holds the live walk + freeze diff; discovery-excluded via witness_exclusion_frontier (OfflineLocalRecipe, substantiated reason + dissolve-on + local recipe, artifact_store precedent) and granted in publication_grant - hermetic file keeps all RED controls, kernel controls, manifest accounting, and the filesystem_read carrier-content check per-PR Verified by execution: 14/14 hermetic PASS, 3/3 wet PASS, publication_placement_gate_passes PASS, generated-artifact gate PASS, fmt clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Fix the mainline scm_compatibility homonym capture blocking CI (5 floor reds on origin/main d552ff4) Top-level fn names are not module-scoped in the assembled closure, so native_scm_interaction_scenario_fixture's parametered fixture_projection collided with the zero-arg fixture_projection homonyms in pijul/mercurial_upstream_model_witness_test once #7563 linked their closures — native_scm_receipt_for's internal call then dispatched to a zero-arg winner: 'call contract mismatch: no parameter named scenario'. Fix: rename the parametered helper to the unique prefixed native_scm_scenario_fixture_projection (both references are file-internal; no external caller exists, verified by corpus grep). Verified by execution: all 5 previously failing witnesses PASS, plus 63 witnesses across every other importer of the fixture module (native_scm_interaction_contract 14/14, mercurial compat 6/6, git compat 7/7, roadmap_validation_oracle 36/36). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * State the enforcement grain honestly and gate the roster-to-disk direction per-PR (codex review 46258) Finding 1: the preflight doc and frontier law claimed the population cover as 'the mechanical wall today' while the cover runs only on the discovery-excluded wet lane — grain inflation. Fixed both ways: - new per-PR hermetic test roster_paths_resolve_on_disk: every rostered path across all three rosters (2 carriers + 17 machinery + 399 manifest rows) must resolve in the checkout via the filesystem_read carve-out (22ms for 418 reads); a stale or fabricated roster row reds per-PR via the interpreter's typed hermetic Read refusal (verified by execution on a nonexistent probe path) - law note + preflight bullets now state the grain explicitly: per-PR merge-gated = roster-to-disk resolution, roster disjointness, carrier byte-content, RED controls; wet-lane = live enumeration (disk-to- roster new-file detection) and the freeze diff, with per-PR gating of that direction arriving at the mandatory_tag region promotion the frontier dissolves into 15/15 hermetic witnesses PASS; plan doc regenerated same commit. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Dedupe the publication roster after merging main (gate-red duplication on main itself) origin/main 06d7aea lists the eleven pre-wall repair paths TWICE: once from #7565's branch-side enrollment block and once from #7580's repair block — the same enrollment race #7580's own note describes, re-entered by the next concurrent pair. The placement gate refuses repeated grants, so main is currently gate-red and every PR merge ref inherits it. This branch resolves the merge by keeping #7580's repair block (with its note) as the single occurrence and re-adding only this PR's own seven paths; publication_placement_gate_passes PASS by execution on the merged tree (42 unique rows, zero duplicates). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Land the per-PR merge-gated ExtdepsScopePlacementGate (codex review 46281) Diff-grain sibling of tools.publication_placement_gate: refuses any freeze..HEAD-added dag/extdeps .dag file outside carriers-union- machinery (scope_placement_refused_paths, pure kernel on gunbc.extdeps_scope_frontier with hermetic RED/GREEN controls) and any frozen-manifest row naming a post-freeze-added file; diff failure and parse truncation refuse, never skip. Enrolled as a cheap-floor wet gate (roster 49->50, gates 10->11, cheap membership 4->5). One recorded freeze re-anchor to the gate-landing base (0ec3c10), admitting lean/overflow.dag which merged inside the wall-less interim (#7550); documented in legacy_manifest_freeze_sha_note. Live-cover witness dedupes its diff observation onto the gate module. Law note and preflight bullet updated to state both directions per-PR. RED proven by execution: a committed unrostered dag/extdeps probe file turns extdeps_scope_placement_gate_passes red; removing it greens. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Expose std_roster_frontier in the derived stage0 crate partition (codex review 46329) extdeps_external_authority.rs imports crate::std_roster_frontier, but the partition source authority (v2.workflow.rust_crate_partition) never rostered the new module, so the partitioned crates could not resolve it. Fix at the authority: std_roster_frontier joins the std-core primitive roster with its module-dag edges (extdeps_external_authority -> std_roster_frontier -> std_decl_ref); partition artifacts and the stage0 seed regenerated to fixed point (two regen generations — the renderer bakes the partition rows at its own build time), and stage0_core/src/lib.rs (tracked but outside every regen path — the lifecycle scaffold's open partition contradiction) gains the matching declaration directly. Disclosed, not fixed here: v1-stage0-std-core has four OTHER unresolved modules (std_occurrence_identity, extdeps_units_{dimensionless, iec_80000_13,iso8601}) byte-identical on origin/main — pre-existing partition rot from other lanes (the #7109 class; no CI job compiles these crates). Rostering them correctly requires re-cutting the std/extdeps crate boundary (extdeps_uri + extdeps_external_authority would move below std_measure, emptying v1-stage0-extdeps-base) — the deferred emitted-crate-partition lane's re-cut, not a one-line roster fix; attempted and reverted here after it surfaced that knot. Verified: cargo check -p v1-stage0-std-core no longer reports std_roster_frontier (remaining errors = the four pre-existing, same as main); generated-artifact gate PASS; fmt clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Reconcile freeze anchor with merged main 5669d42 (cpm_pert joined the interim manifest) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Make the manifest's remove-only lifecycle mechanical at line grain (codex review 46378) manifest_freeze_holds judges file CREATION dates, so a pre-freeze file migrated out of the manifest could later be re-added (scope decl deleted, carrier row dropped, manifest row restored) and the freeze check would pass — the escape hatch re-opened after migration. Closed: tools.extdeps_scope_placement_gate now also observes git.Core.DiffUnified0(origin/main...HEAD) and refuses any line the change itself ADDS to the manifest (manifest_line_observation / manifest_remove_only_holds on gunbc.extdeps_scope_frontier). The one admitted arm is ManifestIntroduced — the file absent at the merge base (the unified diff's /dev/null old side), exactly the PR that first lands the manifest, unforgeable once it exists on main (a delete-and- rewrite inside a branch still diffs as modification). Unreadable diff text and failed diffs refuse, never skip; removals stay free, so the manifest is monotonically shrinking by construction at the merge gate. Hermetic controls: red_manifest_remove_only_refuses_added_row, green_manifest_remove_only_admits_removal_and_unrelated_edits, green_manifest_introduction_admitted_once, red_manifest_unreadable_refuses. Verified by execution: 21/21 hermetic witnesses PASS, both placement gates PASS wet on this tree (the introduction arm exercising the live path), fmt clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Reach the unreadable arm from the parser and collapse the verdict to one surface (codex review 46387) Finding 1: manifest_line_observation never constructed ManifestDiffUnreadable — malformed or truncated diff text fell through to ManifestUntouched, which the gate accepts (fail-open), and the RED control bypassed the parser by constructing the variant directly. Closed: the fold tracks whether any line MENTIONS the manifest path and whether its recognized new-side header was ever ENTERED; mention without entry yields ManifestDiffUnreadable — covering truncation mid- header AND making a manifest deletion refuse conservatively (old-side header mentions the path, no new-side header follows; the promotion PR that legitimately deletes the manifest deletes this gate in the same change). New REDs go THROUGH the parser: a truncated header diff and a whole-file deletion diff both yield ManifestDiffUnreadable. Finding 2: manifest_remove_only_holds hand-matched the same coproduct the gate matched into ProcessExit — two verdict authorities. The Bool predicate is deleted; the ONE surface is the pure manifest_remove_only_exit(observation) -> ProcessExit on the gate module, consumed by both the wet gate wrapper and every hermetic control (which assert on its ExitSuccess/failure arms). Verified by execution: 22/22 hermetic witnesses PASS (incl. the two new parser-reaching REDs), extdeps_scope_placement_gate_passes PASS wet, fmt clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Disambiguate decl_ref in the #7549 witness (floor red on 2a04481: ambiguous across std.primitive_identity and std.roster_frontier) Both modules declare an identical top-level decl_ref helper on main; the ambiguity is latent there and fired in this PR's closure, which is the first to link them (extdeps.external_authority imports std.roster_frontier). Minimal fix at the red site only: the six call sites in dag/test/claim/primitive_identity_join_witness_test.dag are module-qualified to std.primitive_identity.decl_ref and the named import row is dropped. 15/15 witnesses in the file PASS by execution. The root defect is a DESIGN section-3 fork: std.primitive_identity re-mints the decl_ref constructor std.roster_frontier already owns (the same re-mint cursor review 46136 removed from this PR's own carrier). Deduplicating it belongs to the primitive-identity lane on main; this commit only unblocks the floor at the site that reds. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Post-merge reconcile: fix stale sibling citations after #7591 deleted the publication gate Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 2, 2026
…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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fleet-wide CI break: branches cut before the placement gate landed (#7560) merged to main carrying 11 post-cutover Added paths with no publication roster row, so
publication_placement_gate_passesrefuses every subsequent PR merge ref (first diagnosed on #7567, run 30691179521).The 11 paths, each stamped Publish World (all public machinery, nothing sensitive):
dag/extdeps/github/workflows.dag,dag/gunbc/heal_revalidation.dag,dag/test/claim/heal_revalidation_integration_witness_test.dag,dag/test/claim/heal_revalidation_witness_test.dag,dag/test/claim/workflow_dispatch_input_witness_test.dag,dag/tools/ci_heal_dispatch.dag,src/v2/workflow/ci_heal_revalidation_preflight_emit.dag,src/v2/workflow/ci_heal_revalidation_preflight_emit_test.dagdag/gunbc/source_integration_proof_kernel.dag,dag/test/claim/source_integration_proof_kernel_acceptance_test.dag,dag/test/claim/source_integration_proof_kernel_model_witness_test.dagVerified by execution in a worktree at origin/main + this commit:
tools.floor_effect_gate_witness.publication_placement_gate_passes→true(wasfalseon main; the residual ungranted set was computed against the pinned cutover7ead65c6and is empty after these rows)publication_placement_gate_testprobes PASS (incl. added-ungranted RED, advanced-cutover RED, rename/copy destination REDs)Race-class note (recorded in
post_cutover_race_repair_notebeside the rows): this state becomes unwritable once the placement gate is a required branch-protection check — a merge ref must then stamp its own added files before merging, so main can never re-enter it. Until that flip, every pre-wall branch that merges can recreate this break.🤖 Generated with Claude Code