Repository navigation
algebra unfork: remove FreeMonoid variant-drop shadow (single authority; §9 narrows scope) - #6341
Conversation
…ode-gated Three execution-found walls (§9): reserved builtin-method-name collision (blocks op-move to std.*), Root-A emitter hardcoded op paths in 05_emit_rust.dag (blocks 3 host-bridge ops), and QualifiedName node-gating (v2.std.node/diagnostic/lexing deps). Delivered scope = the clean core: delete v2.std.algebra's duplicate FreeMonoid/Empty/Cons, import the single dag/std.algebra authority (158 importers repointed). No dag/std edit, no seed regen, no Root-A touch, no node dependency. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2f052c3 to
d7a9275
Compare
Resolve grammar_validation.dag import conflict (main's diagnostic symbols + this branch's std.algebra repoint of Cons/Empty); repoint straggler infer_emit_compile_anchor.dag (Empty) missed by the initial migration. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
|
On the failing The This PR is a pure v2-tree repoint (delete the duplicate — sent from calm-lark-461 |
|
Fixed in — sent from calm-lark-461 |
|
The floor step This PR is a line-reducing v2-tree repoint; it cannot cause a main-wide chronic timeout. Meanwhile the real code gate — sent from calm-lark-461 |
…6341 defork-audit drift into its authority Operator directive (2026-07-07): the roadmap must carry the execution-model direction — emit-on-demand (emit → build → run, content-addressed reuse) as the canonical execution path, built and proven alongside v2 self-hosting. - roadmap_authority §0-④: execution-as-realization — interpreted-vs-compiled is a per-node realization policy (spine doc); no bytecode VM, no JIT; interpreter roles are bounded scaffolds dissolving with self-hosting. - roadmap_authority §1: new milestone 5-emit-on-demand with acceptance receipts (agreement witness, content-hash reuse, bounded interpreter roles) grounded in the 2026-07-07 forensics (compiled parser linear 1.1→13.9ms; interpreted class-broken via length-builtin O(n^2)). - ROADMAP.md regenerated via main_wet (gunbc run, --source-root dag+src/v2). - Drift repair: #6341's execution-update section was hand-added to GENERATED docs/plans/dag-v2-defork-audit.md only; re-homed verbatim into dag/gunbc/plans/dag_v2_defork_audit.dag — regen now reproduces the committed bytes exactly (git hash-object 5f3292c both sides). The drift gate never fired because the CI floor dies at the compile wall before batch-2 artifact gates run — one more displaced-cost receipt for levers A/B. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…-audit drift re-home (#6363) * WIP: 6343 * WIP: 6343 * WIP: 6343 * execution-spine design draft: refresh #6348 gate cell (merged) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: 6343 * roadmap: execution-as-realization + emit-on-demand milestone; re-home #6341 defork-audit drift into its authority Operator directive (2026-07-07): the roadmap must carry the execution-model direction — emit-on-demand (emit → build → run, content-addressed reuse) as the canonical execution path, built and proven alongside v2 self-hosting. - roadmap_authority §0-④: execution-as-realization — interpreted-vs-compiled is a per-node realization policy (spine doc); no bytecode VM, no JIT; interpreter roles are bounded scaffolds dissolving with self-hosting. - roadmap_authority §1: new milestone 5-emit-on-demand with acceptance receipts (agreement witness, content-hash reuse, bounded interpreter roles) grounded in the 2026-07-07 forensics (compiled parser linear 1.1→13.9ms; interpreted class-broken via length-builtin O(n^2)). - ROADMAP.md regenerated via main_wet (gunbc run, --source-root dag+src/v2). - Drift repair: #6341's execution-update section was hand-added to GENERATED docs/plans/dag-v2-defork-audit.md only; re-homed verbatim into dag/gunbc/plans/dag_v2_defork_audit.dag — regen now reproduces the committed bytes exactly (git hash-object 5f3292c both sides). The drift gate never fired because the CI floor dies at the compile wall before batch-2 artifact gates run — one more displaced-cost receipt for levers A/B. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Operator ruled nat prerequisites discharged (#6341 merged, coproduct keystone green). Replace stale BLOCKED+LAST with DESIGN READY and SEQUENCED WITH integer+float repoint; clarify 138 as closure risk measure. Regenerate dag-v2-defork-audit.md from .dag authority via main_wet; sync algebra cross-ref and std_integer fork note. Co-authored-by: Cursor <cursoragent@cursor.com>
* WIP: Nat census handback * chore: regenerate drifted generated artifacts (ci auto-heal) * Nat census follow-up: discharge BLOCKED+LAST, regen defork audit Operator ruled nat prerequisites discharged (#6341 merged, coproduct keystone green). Replace stale BLOCKED+LAST with DESIGN READY and SEQUENCED WITH integer+float repoint; clarify 138 as closure risk measure. Regenerate dag-v2-defork-audit.md from .dag authority via main_wet; sync algebra cross-ref and std_integer fork note. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Nat census handback * Fix §3b nat row: retire stale smart-ant-466 escalation label Bring grounding-cluster decision-input table in line with §2A and §3 sequencing (DESIGN READY, census complete, prerequisites discharged). Regenerate dag-v2-defork-audit.md from .dag authority. Co-authored-by: Cursor <cursoragent@cursor.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: Cursor <cursoragent@cursor.com>
…view 57807) The row classified the two-Nat fork as AwaitsOneGrounding, whose grounding sentence claimed the modeling direction was still undecided. Checked against the authority the review cited and the review is correct: gunbc.plans.dag_v2_defork_audit records the nat census complete with the per-concept design DESIGN READY and its prerequisites discharged (algebra FreeMonoid shadow #6341 merged, generic-alias coproduct keystone green), and it specifies the cutover file by file -- dag/std/nat.dag takes the coproduct and the Peano ops with the semiring alias deleted, v2.std.nat becomes a thin reimport plus the node-bound law roster, integer and float repoint GroupCompletion<Nat> to std.nat.Nat, every importer in the same push. So the direction is decided and the work is scheduled: the blocker is ClimbableButUnbuilt and the trigger now names that atomic wave rather than a ruling nobody owes. Calling it a grounding question converted actionable work into an indefinite decision stall -- the untracked stall DESIGN section 4b forbids -- and diluted the canonical plan by implying the question was open. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013koFunEtpLQCnvUiz85k7Y
…a stall row, prose leaves the data plane (#9794) * XL-0N residue: refusals carry the BinOp coproduct, the Nat fork gets a stall row, prose leaves the data plane The review findings on #9719 (reviews 57754, 57758) that did not travel with #9710. Rebuilt against main rather than landed from the stale branch, and re-verified against main rather than assumed: - dag/std/operator_realization.dag binop_is_ordering had no consumer corpus-wide (its sibling binop_is_equality is already absent from main). Deleted. - OperatorRealizationRefusal typed its operator as String -- a closed vocabulary flattened to text. Both variants now carry BinOp itself, all nine producers pass the variant, and the spelling happens once at the message boundary. binop_label stays as that rendering fact, annotated with the corpus check that no other BinOp-to-glyph producer exists (v1's compile.dag renders the variant NAME; glyph recognition is in the tokenizer against token kinds). Rendered message text is unchanged. - src/v2/std/nat.dag carried commentary as a String data row; converted to a module-scope // annotation on nat_max, the section 4c quarantine boundary. - The two-Nat fork it narrated is now gunbc.guarantee_rung_drop two_nat_authorities_stall: ceiling StructurallyImpossible, trigger naming the capability (one Nat declaration with the other derived), bounded population. Verified still true on main: dag/std/nat.dag declares Nat as CommutativeSemiring<Magnitude> and src/v2/std/nat.dag declares the Peano coproduct, with nat_max in both. NOT carried: the structural_connective_stall row from the old branch. Main already declares StructuralConnectiveBinding and routes And/Or through structural_connective_realization -- that IS the capability the row named as its next-rung trigger, so main retiring it is correct and re-adding it would declare a stall its own trigger has dissolved. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013koFunEtpLQCnvUiz85k7Y * XL-0N residue: regenerated std_operator_realization mirror The projection of the .dag change in the parent commit. Produced by a regen round bootstrapped from this branch's own committed seed (main's stage0, which compiles), installed by the generated-header discriminator rather than by a byte comparison against a third tree, and gated: both rounds rebuilt the seed from the installed tree and re-verified at first_generation_equal=true 148/148, followed by a whole-package build of exactly these bytes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013koFunEtpLQCnvUiz85k7Y * XL-0N: retire the stale namespace admission row -- its trigger fired The row admitted one TargetChanged binding for relocating type_reference_declaration_ref to v1.compiler.infer_env, with DISSOLVE-ON: this pull request merging. #9710 carried that relocation to main (#9719 itself closed as superseded), so base and head both have it and no run can produce the delta. gunbc#9794's witnesses lane reported it exactly as the row predicted: namespace-wave-admission STALE ADMISSION type_reference_declaration_ref relocated to v1.compiler.infer_env (XL-0N, gunbc#9719) ... matches no delta in this run FAILED PHASE namespace-wave-admission (0 unadjudicated delta(s), 1 stale admission(s)) Removed by its own stated trigger, which is also why it could not be left: a stale row here refuses every unrelated PR against main, so this was blocking more than this branch. The floor itself was clean in that run (verdict=FloorClean unexpected_failures=0); this phase was the only failure. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013koFunEtpLQCnvUiz85k7Y * XL-0N: the Nat fork is ClimbableButUnbuilt, not awaiting a ruling (review 57807) The row classified the two-Nat fork as AwaitsOneGrounding, whose grounding sentence claimed the modeling direction was still undecided. Checked against the authority the review cited and the review is correct: gunbc.plans.dag_v2_defork_audit records the nat census complete with the per-concept design DESIGN READY and its prerequisites discharged (algebra FreeMonoid shadow #6341 merged, generic-alias coproduct keystone green), and it specifies the cutover file by file -- dag/std/nat.dag takes the coproduct and the Peano ops with the semiring alias deleted, v2.std.nat becomes a thin reimport plus the node-bound law roster, integer and float repoint GroupCompletion<Nat> to std.nat.Nat, every importer in the same push. So the direction is decided and the work is scheduled: the blocker is ClimbableButUnbuilt and the trigger now names that atomic wave rather than a ruling nobody owes. Calling it a grounding question converted actionable work into an indefinite decision stall -- the untracked stall DESIGN section 4b forbids -- and diluted the canonical plan by implying the question was open. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013koFunEtpLQCnvUiz85k7Y * XL-0N: the Nat stall's population is UncountedNotEnumerable, not falsely bounded (review 57881) The row declared BoundedPopulation while its second member was the open-ended category "every reference site" rather than an enumerated identity -- bounded in appearance only, which is what the carrier's second variant exists to prevent. Checked whether the half could instead be enumerated, and the attempt is what settles it: the property is about a module's CLOSURE, not its import list, and closure membership is transitive -- a module importing one neighbour that reaches std.nat and another that reaches v2.std.nat has both while importing neither. A direct-import scan finds four dual-importing files and is therefore not that set. Rendering those four as a bounded list would have read as bounded while measuring the wrong property: an enumeration that is false the moment it is written. So the carrier is UncountedNotEnumerable, and the reason keeps the enumerable declaration half (the two declarations and the four forked operations) inside it, states why the exposure half is not enumerable, and records that the population is bounded in principle by the corpus and goes to zero with the trigger. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013koFunEtpLQCnvUiz85k7Y --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
algebra unfork — remove the FreeMonoid variant-drop shadow (single authority)
Kills the §5 fail-open the de-fork audit tracks as the LIVE
{algebra}pair:FreeMonoid/Empty/Conswas defined in both std trees (dag/std/algebra.dag:111andsrc/v2/std/algebra.dag), so a closure pulling both silently dropped the coproduct's variant bindings (undefined variable: Empty, reproduced 2026-07-05).Change (pure v2-tree repoint): delete
v2.std.algebra's duplicateFreeMonoid/Empty/Cons, import the singledag/std/algebraauthority, repoint the 158FreeMonoid/Empty/Consimporters. Nodag/stdedit → no stage0 seed regen; no op moved; no05_emit_rust.dag(Root-A) touch; nonodedependency.Scope is narrower than the signed design — see
docs/plans/algebra-grounding-unification-design.md§9 (execution revision). Three walls, each found by-execution, keep the rest deferred to explicit follow-on lanes:std.*free fn namedfilter/length/any/contains/skip/is_emptycollides withdag/std/algebra's template-declared builtin methods and breaks barefold(...)resolution corpus-wide. So the operational ops cannot move to astd.*module as-is; they dissolve into the builtin methods in a separate v2 lane.src/v1/05_emit_rust.daghardcodescrate::v2_std_algebra::{freemonoid_empty,fold_list,list_snoc_item}for theString=FreeMonoid<Char>host bridge (the design-fenced, unowned Root-A seam). Moving those 3 ops breaks the emitter.v2.std.node/v2.std.diagnostic/lexing, so promoting it tostd.qualified_nameneeds the separatenodedefork, not algebra alone.Verified by-execution: single
FreeMonoiddefinition remains (structural); v1 whole-tree resolve clean (902 sources); the bmc whole-tree v2+dag precompute passes; thegeneric_alias_coproductkeystone (a both-trees closure over recursiveCons.tail) passes.