Skip to content

Optional de-fork step 2: re-home v2.std.optional to std.optional under the dag root - #13388

Merged
briansrls merged 21 commits into
mainfrom
session/bright-fox-661-rehome2
Oct 6, 2026
Merged

briansrls merged 21 commits into
mainfrom
session/bright-fox-661-rehome2

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Oct 5, 2026

Copy link
Copy Markdown
Contributor

Draft: the stage0 mirrors are not committed yet. The seed does not build at this head until they are; the next commit adds them.

Step 2 of the Optional de-fork, after #13178. The one Optional declaration moves from src/v2/std/optional.dag (v2.std.optional) to dag/std/optional.dag (std.optional). Modules under the dag root, and the seed's own closure, can then import Present/Absent from the authority instead of resolving them only through the seed kernel.

What changes

  • The declaration moves. std.optional Optional = Absent | Present { value: T }, unchanged apart from its path. v2.std.optional no longer exists, so no second binding is left beside it.
  • Every reference is rewritten by a generated, re-runnable instrument: tools.source_reference_repoint (dag/gunbc/instruments/source_reference_repoint.dag).
    • It reads the seed's token stream, not text. It rewrites import paths, qualified-name prefixes and DeclarationRef module_path strings, and never touches comments or other strings.
    • Its output is the 927-file rewrite in this PR, including the kernel mint's binding row in gunbc.structural_realization_bindings.
    • It is idempotent: a second run changes nothing. repoint_pending reports the remainder, which is only two docs/plans files, prose the instrument leaves alone by design.
    • A merge of main is followed by re-running it: gunbc run --source-root dag --source-root src/v2 --entry dag/gunbc/instruments/source_reference_repoint.dag --function repoint.
    • Claims: test.claim.source_reference_repoint_witness_test (8).
  • Acceptance population: the 19 parked R4 modules now import std.optional { … } for the names they use. They are the new home's consumers in this change: std.types, std.algebra, std.keyed_row, std.keyed_roster, std.checked_arithmetic, std.computation, std.content_hash, std.effects, std.induction, std.integer, std.measure, std.nat, std.occurrence_identity, std.realization_schedule, std.source_annotation, std.termination, extdeps.uri, extdeps.external_authority and gunbc.rust_crate_package_ident.
  • First stage0 mirror. std_optional gets a row in the std-core list of v2.workflow.rust_crate_partition (and its generated mirror), plus its module line in stage0_std_core. Without it, regen refuses Stage0EmittedEdgesNotCovered, with 21 edges from those modules.

Evidence so far (BuildBuddy, on this source tree)

  • Repoint run, then a second run: clean, and the second changes nothing.
  • Regen fixed point: first_generation_equal=true, planned 164, once std_optional.rs was installed.
  • Acceptance, gunbc compile --source-root dag (dag root alone), 0 blocking errors: 16 of 19 measured. The run was killed by BuildBuddy's 1-hour cap before extdeps.uri, extdeps.external_authority and gunbc.rust_crate_package_ident. To do: the remaining 3, the claims, clippy and the self-host build, re-run on the head with mirrors.

Not in this PR

  • The none literal and the universal-null join: PR B, then transition 2.
  • The Cardinality connective unification: transition 2.

v1 purpose test (gunbc.v1_maintenance_standing): admitted. The seed gains no surface; it reads the one declaration from its new home, which the v2 self-host requires.

🤖 Generated with Claude Code

Brian Searls and others added 7 commits October 5, 2026 01:18
…claration file moved (references not yet rewritten)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…t every reference with the generated instrument, import it in the 19 parked modules, add the std_optional stage0 partition row

Stage0 mirrors (std_optional.rs and the mirrors of edited sources) follow in the next commit.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… lines: main's side taken; the instrument is re-run next)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…side taken; instrument re-run next)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…side taken; instrument re-run next)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…rs at the fixed point (first std_optional mirror), retire two Optional debt rows as ImportsFixed

Regen BuildBuddy round 10: first_generation_equal=true, 164 planned. All 19 acceptance modules compile from the dag root alone.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
One conflict, an import line in v2.lens.cost.copied_port_citations: main's side taken and its v2.std.optional path repointed exactly as tools.source_reference_repoint does. No src/v1 input changed on main since the round, so the mirrors stand.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review October 5, 2026 14:52
Brian Searls and others added 2 commits October 5, 2026 15:52
… base carries

environment_agreement handed the HEAD's environment closure to the base's git archive, so a module newly imported into the environment (here dag/std/optional.dag, which std.types now imports) refused the whole reconstruction with a missing pathspec (REQUIRED-FLOOR REFUSAL ChangedWitnessObservationFailed on #13388 at 4e33548). A file absent at the base cannot belong to the base's environment, so it is left out of the base load and still counted as a difference.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… only the members that revision carries

The previous commit filtered absent paths in environment_agreement only; the kernel-names read (kernel_names_at, the closure of dag/std/types.dag) archived the same head closure at the base and refused the same way (CI run 37336368663 at b813c8d). One helper, closure_members_carried_at, now sits under both base loaders (load_parse_environment_with_closure and kernel_names_at), and the environment_agreement-only filter is removed.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Brian Searls and others added 7 commits October 5, 2026 18:12
…uches them

- v2.test.claim.namespace_xl0 call_argument_value_resolve_refusal, if_arm_and_statement_lowering_refusal, let_match_early_return, return_tail_position: read the fatal reason through native_test_file_refusal_fatal_reason; #13364 removed the stored NativeTestFileRefusal.fatal_reason field and these four still read it (main's floor never judged them).
- test.claim.scm_write_spine_witness: import empty_store from gunbc.scm.object_store (it was used bare and refused as unresolved).

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…es and two stage0 mirrors; main's side taken, instrument and regen re-run next)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…rs at the fixed point, evaluation_budget imports Optional (roster row retired ImportsFixed)

Regen BuildBuddy invocation c3f7ae6a-334c-4a3d-8be8-410d23b8223c at c5c974e: first_generation_equal=true (164 planned), repoint and kernel-mint binding claims 16/16 PASS, acceptance modules compile.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… (NonFoldResidueRosterDiverged)

An unreadable file now refuses with its own cause; in the pending check it is listed as pending, so the verdict refuses and names it rather than counting it as repointed.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ain (parse refused it inside the body)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…admitted_identity_cast_emits_through_the_closure_route_holds as BecameSharedByDemand

The floor refused it as SingleClaimFillDebtStale on 6c3712c (run 37388067545): its fixture producer identity_cast_route_emit is now demanded by five claims, so no single-claim identity remains to bill. The test file is unchanged by this PR; it is planned here because the re-home removes v2.std.optional.Optional, which every consumer of it reaches.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Oct 6, 2026

Copy link
Copy Markdown
Contributor Author

#13388 MERGE PACKET. HEAD: 298d12d. Witnesses: GREEN on run 37410109102 (floor, emit-build, generated, rust-unit-tests, witnesses); GitHub reports CLEAN. Regen on this exact head: BuildBuddy invocation 3c498958-8c26-42c5-9329-5015ad04f947, first_generation_equal=true, 164 planned.

  1. THE ONE NON-GENERATED SEMANTIC CHANGE (read this part closely)
    Where: v1_compiler namespace_baseline, new helper closure_members_carried_at (seed host Rust; the floor's base reconstruction).
  • Before: both base loaders read the base through a closure resolved over the LIVE tree, which is the head. These are load_parse_environment_with_closure (the grammar) and kernel_names_at (the kernel-name set of std.types).
  • Defect: a file that is new at head was handed to git archive at the base and failed as a missing pathspec, refusing the whole reconstruction: REQUIRED-FLOOR REFUSAL ChangedWitnessObservationFailed. Any PR that adds a module to either closure hits it; here it was dag/std/optional.dag, imported by std.types.
  • After: the helper keeps only the closure members the base revision carries, and both loaders call it.
  • Why this is correct: a file the base does not carry cannot belong to the base's closure.
  • Why a new file is never a silent agreement: the comparisons that decide agreement are unchanged and still run over the full head closure. environment_agreement compares the blob of every closure path, and a missing base blob never equals a head blob. kernel_set_serves_both compares the std.types blob. Either way the result is a difference, and the base is then read under its own rules.
  • A base member the head closure no longer names is not recovered; resolution refuses, located, as before.
  • SUPERSEDED BY floor: read a revision's environment closure from that revision (base closure was taken from the head tree) #13408 (calm-boar-904 ruling, 2026-10-05). This narrower fix lands now to end the hold. floor: read a revision's environment closure from that revision (base closure was taken from the head tree) #13408 then rebases onto it and REPLACES closure_members_carried_at in the same function: delete-first, with its fuller read of the base's own closure in both directions, plus tests. So the overlap ends in one motion.
  1. THE CONTROL
  • Red: CI run 37328242169, floor at 4e33548 (no fix), refused at the grammar read. CI run 37336368663, floor at b813c8d (a first fix covering the grammar read only), refused at the kernel-names read. So each of the two call sites has its own observed red.
  • Green: the floor at 298d12d (with the fix), run 37410109102, on the same change.
  • No separate claim that a head-only path is a difference:
    • A "silent agreement on a new file" is unreachable. A file enters the environment closure only through an import added to an existing closure file, and that file's blob then differs too, so the verdict is Differs whatever the new path contributes.
    • This function has no fixture harness. Its inputs are two git revisions of the live dag tree, and the seed's cargo tests run on no CI path (rung drop rust_unit_tests_off_the_merge_path), so a unit test would be local diligence only.
    • The next-rung trigger is a revision-pair fixture harness for the floor's base reconstruction.
  1. EVERYTHING ELSE IS GENERATED OR MECHANICAL
  • tools.source_reference_repoint, with its 8 claims, and its output: the repoint of v2.std.optional -> std.optional over about 970 files, re-run after each merge of main. The PR's own source diff is otherwise unchanged across the merges; conflicts were import lines only, and main's side was taken and then repointed.
  • The declaration moved to dag/std/optional.dag, unchanged apart from its path.
  • The 19 acceptance imports. All 19 modules compile from the dag root alone, 0 blocking errors (BuildBuddy rounds 6 and 10).
  • The std_optional stage0 crate partition row in v2.workflow.rust_crate_partition and its generated mirror, plus its module line in the stage0_std_core lib.rs.
  • Stage0 mirrors at a fixed point (first_generation_equal=true, 164 planned), including the first std_optional.rs. BuildBuddy invocation c3f7ae6a-334c-4a3d-8be8-410d23b8223c at c5c974e, the merge of main under the src/v1 hold. The first regen drifted only std_algebra.rs and std_effects.rs; once those were installed, the second and third regens hold. Commits after it touch no seed input: the evaluation_budget import (no mirror) and the instrument's match arms.
  1. HAND EDITS BESIDE THE ONE ABOVE
    (a) Two roster rows retired as Retired { cause: ImportsFixed } in v2.workflow.floor_unimported_bare_provider_debt_roster: dag/extdeps/uri.dag#Optional and dag/gunbc/rust_crate_package_ident.dag#Optional. Those files now import std.optional; the roster gate refused them as RosterStale.
    (b) One import line in v2.lens.cost.copied_port_citations: main's side taken and v2.std.optional repointed, exactly as the instrument does.
    (d) dag/std/evaluation_budget.dag imports Absent, Optional and Present from std.optional, and its roster row is retired as ImportsFixed. The floor had refused it as RosterStale: std.types now imports std.optional, so Optional resolved through the closure.
    (e) tools.source_reference_repoint names every read outcome instead of using a wildcard arm (the floor refused it as NonFoldResidueRosterDiverged). An unreadable file refuses with its own cause, or is listed as pending.
    (f) Pending Fix main: four namespace_xl0 test modules read the removed NativeTestFileRefusal.fatal_reason (use the chain-derived accessor) #13400: if it lands first, it carries the same fix for the four namespace_xl0 readers below; main's version is taken in the next merge.
    (h) floor_single_claim_fill_debt: identity_cast_emission_route an_admitted_identity_cast_emits_through_the_closure_route_holds is retired as BecameSharedByDemand. Its fixture producer is now demanded by 5 claims, and the floor refused the row as SingleClaimFillDebtStale.
    (c) Repairs of defects that are already on main in files this PR touches; the floor judges touched files, and main's floor never judged these:
  1. VERIFY
  • Round 11 at c5c974e: all 16 claims PASS (repoint 8/8, kernel-mint binding 8/8), and the acceptance modules compile.
  • Verify round on 4e33548: the self-host compiler builds, and clippy is clean on all targets.
  • rust-unit-tests timed out at 40 minutes with no test failed. It is not a required lane: the main ruleset requires only witnesses.

…in's side taken and repointed; instrument re-run next)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Brian Searls and others added 3 commits October 6, 2026 12:39
…t main added importing v2.std.optional)

BuildBuddy, pinned to 3c1c48c: repoint then regen, first_generation_equal=true (164 planned).

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…s, main's side taken; one file deleted on main; instrument re-run next)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
BuildBuddy pinned to 3c415f3: repoint then regen, first_generation_equal=true (164 planned).

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@briansrls
briansrls merged commit a453be9 into main Oct 6, 2026
4 checks passed
gunbai-bot Bot pushed a commit that referenced this pull request Oct 6, 2026
#13388 removed that module; required-ci still resolved those five
production imports and refused the floor.

Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot Bot pushed a commit that referenced this pull request Oct 6, 2026
…-debt standing was retired by #13388)

v2.test.claim.coercion.identity_cast_emission_route
an_admitted_identity_cast_emits_through_the_closure_route_holds is a
required_gate_authored_modules member, so it runs on every PR. It was carried
as single-claim fill debt until #13388 retired that row as BecameSharedByDemand;
nothing replaced the standing, and with main resolving again it now blocks
every floor: verdict holds, 657,428 eval steps against the new-witness budget
of 72,300 (runs 37486290875 and 37493248052).

Own list floor_eval_step_cost_drop_identity_cast_route_rows plus the declared
4b(3) drop gunbc.rung_drop identity_cast_route_new_witness_eval_step_cost
(MechanicallyPreventable -> Mitigatable; the claim still executes and a
semantic red or wall crossing still blocks; trigger: the route claims
restructured to supplied inputs, DESIGN section 3 witness rule, keeping one
real-route inhabitance claim).

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Oct 6, 2026
… be regenerated

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Oct 6, 2026
… cost roster.

The safety set is the admitted-route and refused-route inhabitance obligations.
Leftover v2.std.optional imports after the #13388 re-home blocked this PR's
floor before any native claim-cost row could be written.

Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls pushed a commit that referenced this pull request Oct 6, 2026
…ome (main is broken) (#13487)

* Repoint the v2.std.optional imports #13367 landed after #13388's re-home

#13367 (96479e6) merged first and added five imports of v2.std.optional;
#13388 (a453be9) then re-homed that module to std.optional, so main refuses
in every generated job (CarrierRefused: unresolved import v2.std.optional, from
dag/extdeps/llm/claude_code_stream_json.dag). This is #13388's own instrument,
tools.source_reference_repoint repoint, run over the whole tree at a453be9
(TREE_EXACT): it rewrote exactly these five import paths. Present and Absent
are declared in std.optional. String fixtures are untouched by design.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

* Declare the identity-cast route claim's eval-step cost drop (its fill-debt standing was retired by #13388)

v2.test.claim.coercion.identity_cast_emission_route
an_admitted_identity_cast_emits_through_the_closure_route_holds is a
required_gate_authored_modules member, so it runs on every PR. It was carried
as single-claim fill debt until #13388 retired that row as BecameSharedByDemand;
nothing replaced the standing, and with main resolving again it now blocks
every floor: verdict holds, 657,428 eval steps against the new-witness budget
of 72,300 (runs 37486290875 and 37493248052).

Own list floor_eval_step_cost_drop_identity_cast_route_rows plus the declared
4b(3) drop gunbc.rung_drop identity_cast_route_new_witness_eval_step_cost
(MechanicallyPreventable -> Mitigatable; the claim still executes and a
semantic red or wall crossing still blocks; trigger: the route claims
restructured to supplied inputs, DESIGN section 3 witness rule, keeping one
real-route inhabitance claim).

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Oct 6, 2026
gunbai-bot Bot pushed a commit that referenced this pull request Oct 6, 2026
… cost roster.

The safety set is the admitted-route and refused-route inhabitance obligations.
Leftover v2.std.optional imports after the #13388 re-home blocked this PR's
floor before any native claim-cost row could be written.

Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot Bot pushed a commit that referenced this pull request Oct 6, 2026
…e-home (N7 combined tree)

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Oct 6, 2026
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Oct 7, 2026
…l after #13388

The probes at :60, :699, :754 still imported v2.std.optional (defunct since the Optional
de-fork); their compile.frontend refused, so three witnesses red. Same class as the :281
probe re-point review 77124 asked for. Verified attribution for the one remaining red in
this entry (w_depth_one_shared_field_refutation_stays_shape_guarded): it fails on
origin/main's own tree identically (exit=1 FAIL=1 at main), so it is main-carried latent
debt, untouched here.
gunbai-bot Bot pushed a commit that referenced this pull request Oct 7, 2026
body_lowering_unrecognised_lowered_shape_test: imports Optional from std.optional
(main's #13388 retired v2.std.optional); main's field_projection_node import
dropped, since nothing in this branch's rewrite of the file references it.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Oct 7, 2026
#13388 re-homed the mint after this branch's CI; the wall still
admits only the mint DeclarationRef, now std.optional Optional.

Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot Bot pushed a commit that referenced this pull request Oct 7, 2026
…13388 re-homed it; the same edit #13487 made on main)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Oct 7, 2026
…nt; #13388 removed the module)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Oct 7, 2026
…e-homed the mint.

Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot Bot pushed a commit that referenced this pull request Oct 7, 2026
…13388)

Fresh emission at this head no longer contains a v2.std.optional module (re-homed to
std.optional by #13388), so the registration is stale and required-regen refuses. Main's own
lib.rs carries the same stale registration; main's pushes never re-run required-regen, so it
surfaces only at a PR head. Byte-exact inverse of the drift line CI reported at 51aefcc.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant