Repository navigation
§5 de-fork Step 1 PR-B: grounded cross-tree admission (delete QN-prefix guess) - #5486
Merged
Merged
Conversation
gunbai-bot
Bot
changed the title
No tree change vs c86459a. The reused self-hosted runner resolved the inconsistent intermediate commit 2c5750a (resolution.dag had the symbol deleted while 03_name_resolve.dag still called it); HEAD c86459a is clean. A fresh sha forces actions/checkout to reset the poisoned workspace. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Jun 22, 2026
…n from host tags (#5506) The remaining activation gate: prove by execution that the source_root carrier (#5473/#5486) is CONSUMED on the real grounded compile path, not merely carried. Feeds a host-tagged SourceRootIngest through the real machinery — program_assembly_fold_ingest builds the QualifiedName->SourceRootRef index, source_root_set_from_ingest builds the active-root set — then runs cross_tree_edge_decision (the exact fn admit_import_entry calls). Nothing about fundamentality is supplied; MoreFundamental/LessFundamental is derived by tree_fundamentality_order. By execution (gunbc run --claim-run): - v2-subject (V2Tree) -> dsl-target (DslTree) => EdgeCrossAdmitted (true) - tags reversed: dsl-subject -> v2-target => EdgeCrossDenied (true) Asserts the exact decision variant (not a Bool proxy) so the RED leg cannot pass for a wrong reason. Flip either source_root tag and the witness goes the wrong way (discriminating oracle). Verdict: cross-tree import is ACTIVE on current main, grounded on filesystem-truth source-root tags — the de-fork collapse fan-out is unblocked. Floor-auto-enrolled via _test.dag naming. Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Jun 22, 2026
…-forks + 7 grounding cluster) (#5511) * §5 de-fork audit: re-verdict census by execution — 2 mirrors + 2 not-a-forks + 7 grounding cluster The dsl↔v2 std fork is not "mostly temp v2 mirrors": by-execution decl-set comm + shared-type-body diff shows 2 true mirrors (reducible/measure), 2 pure name-collisions (coercion/node), and 7 divergent groundings (algebra/logic/nat/ integer/float/effects/verification) — the same concept grounded on a different axis/realization per tree (e.g. EffectShape: operation-axis in dsl vs idempotency-class in v2; TestClaim simple-proposition vs grounded coproduct). The grounding cluster is a single-authority unification DESIGN downstream of the numeric tower (#5428) + model↔realization grounding, not a mechanical repoint. Also: §1 updated — cross-tree import is ACTIVATED (#5473/#5486 grounded, #5506 arbiter witness proves it live, #5504 fixed the abs-vs-rel admission bug); the former "wired but off" blocker is dissolved. Structured §2 as operator decision-input per concept (shared / shared-body-divergence / each-side-unique / grounding-entanglement). DESIGN §6: a stale doc contradicting ground-truth is parallel-representation debt. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * §5 audit: correct node/coercion to v1-artifact category (DEFER to v1-shrink) verify-before-act caught a scoping error: importer greps omitted src/v1, and src/v1 is a live consumer of dsl/std. node + coercion renames are NOT clean-lane — both cascade into the v1 seed (04_infer inference stage import + emitted Rust std_{node,coercion}.rs + a guard test). Per bright-stag's ruling, DEFER both to v1-shrink: on v1-delete node self-dissolves (dead file → delete, no rename) and coercion shrinks to a v1-free disambiguation (4 extdeps + v2). Census now has THREE categories: (a) 2 true mirrors, (b) 7 grounding divergences, (c) 2 v1-artifact collisions. Recorded the dissolution trigger. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jul 6, 2026
…d by broken regen); keep source_root_ingest V2Tree fix The #6289 witness ownership_movable_test.dag emits test_claim_ownership_movable.rs, which references v1.compiler.ownership symbols (merge_branch_licenses, MoveLicenseAccum, LiveState, move_site_key, ...) that are NOT in the committed v1_compiler_ownership.rs seed. Registering it as a GENERATED file therefore breaks the seed crate's compile (E0432/E0425/E0061) -- 'just register it' cannot land in isolation. Measured blast radius: the fresh self-compile drifts from the committed seed across 33 files (the known-broken regen, emitter bugs #6298), so pulling in the fresh v1_compiler_ownership.rs cascades into the whole regen. Not a scoped fix; parked for the regen project (or exclude the off-auto-path witness from the emit closure). KEPT: the source_root_ingest_gate_passes main-red fix -- emit_source_root_ingest_manifest now imports v2.std.cross_tree.import_model { DagTree, V2Tree }. The manifest emitter hardcodes its import block and missed this when source_root became a grounded SourceRootRef (#5473/#5486), so every witness importing the manifest failed with 'undefined variable V2Tree'. Verified locally: all 3 real_ingest witnesses + the 2 runnable closure witnesses now return true (were compile errors). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jul 6, 2026
…nert-gate hole #1) (#6311) * WIP: Fork of realization * WIP: Fork of realization * WIP: Fork of realization * WIP: Fork of realization * Floor affected-set: non-.dag-only diff is structural-∅, not ignorance (unblock pure-.rs PRs) floor_diff_edits_from_line_ranges refused (Err) when a diff changed only non-.dag files (saw_non_dag && !saw_dag) — reddening the discovery-corpus batch for every pure-.rs PR (seed hand-syncs, Rust-only changes). That conflated a structural-∅ .dag frontier with an ignorance state. Per the operator's arity ruling: a successful git-diff observation whose .dag subset is empty is NOMINAL (present, empty) — the SAME outcome as an empty diff (every row takes the not-affected skip). The only ignorance state is a FAILED observation (UnifiedDiffFail, floor_diff_observe.dag), refused upstream in floor_git_diff_range. This mirrors the function's own departed-.dag-path arm, which already distinguishes structural-∅ (continue) from ignorance (refuse). Fix: drop the saw_non_dag/saw_dag refusal; a non-.dag-only diff falls through to the empty frontier. Observation layer (Ok/Fail + exit code) and the shell docs-only shortcut are unchanged (already correct / downstream- safe). Red control: non_dag_only_diff_is_structural_empty_frontier_not_refusal (was Err, now Ok empty). Also fixes the compile error at 32fac2e (auto-commit captured this edit mid-flight: declarations removed, refusal block not yet dropped). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: Fork of realization * Revert roster registration of test_claim_ownership_movable.rs (blocked by broken regen); keep source_root_ingest V2Tree fix The #6289 witness ownership_movable_test.dag emits test_claim_ownership_movable.rs, which references v1.compiler.ownership symbols (merge_branch_licenses, MoveLicenseAccum, LiveState, move_site_key, ...) that are NOT in the committed v1_compiler_ownership.rs seed. Registering it as a GENERATED file therefore breaks the seed crate's compile (E0432/E0425/E0061) -- 'just register it' cannot land in isolation. Measured blast radius: the fresh self-compile drifts from the committed seed across 33 files (the known-broken regen, emitter bugs #6298), so pulling in the fresh v1_compiler_ownership.rs cascades into the whole regen. Not a scoped fix; parked for the regen project (or exclude the off-auto-path witness from the emit closure). KEPT: the source_root_ingest_gate_passes main-red fix -- emit_source_root_ingest_manifest now imports v2.std.cross_tree.import_model { DagTree, V2Tree }. The manifest emitter hardcodes its import block and missed this when source_root became a grounded SourceRootRef (#5473/#5486), so every witness importing the manifest failed with 'undefined variable V2Tree'. Verified locally: all 3 real_ingest witnesses + the 2 runnable closure witnesses now return true (were compile errors). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Red-control test for source_root_ingest manifest cross_tree import manifest_imports_grounded_source_root_constructors: asserts the emitted manifest imports v2.std.cross_tree.import_model whenever it emits a grounded source_root value -- deleting the import line reddens this test (paired with the CI witness program_assembly_real_ingest_module_roots_parse_holds as the execution oracle). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Resolve merge with main #6269 in floor_diff_edits + manifest emitter The auto-committer flushed the in-progress merge with conflict markers (0b74fe4); this resolves both: - floor_diff_edits_from_line_ranges: keep #6269's v1_attribution_index + added_paths handling; keep the structural-∅ fix (no saw_non_dag/saw_dag refusal -- a non-.dag-only diff is a nominal empty frontier). The two are orthogonal and compose. - emit_source_root_ingest_manifest: take #6269's emit_source_root_ref_import (derives the referenced SourceRootRef constructors from records) over the earlier hardcoded both-constructors line -- same source_root_ingest V2Tree fix, more precise form. Kept both red-control tests; retargeted the structural-∅ test off a src/v1/ path (which #6269 now eagerly resolves via the real workspace tree, unavailable from the unit-test cwd) onto a path-agnostic non-.dag path. Both green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: regen * WIP: regen * Revert inert selective-import filter (ancestry bypasses type_env_for_import) The type_env_for_import specific_names filter was auto-committed to this PR but is a no-op: lookup_binding_by_name reads ancestry_str_bindings, which build_type_env fills from union_parent_type_env_caches (04_infer.dag:5507) and the single-import path (:133) -- both merge each import's full parent.type_env_cache, bypassing type_env_for_import (which only feeds the unused 'parents' field). Measured: dag_collect still resolves un-imported ErrorNode with the filter built in. Reverting so #6311 does not carry a fail-closed illusion; the real fix belongs in the ancestry-cache seam. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.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
1 participant
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.
§5 de-fork Step 1 PR-B: grounded cross-tree admission
Activates cross-tree imports on filesystem-truth provenance, replacing the unsound
QualifiedName-prefix source-tree guess. Builds directly on PR-A's host-tagged
DagSourceReadWitness.source_root(#5473). Second and final half of de-fork Step 1.What lands
std/cross_tree/resolution.dag— DELETE the QN-prefix fallback(
source_root_ref_from_qualified_name,source_root_set_from_module_roots,cross_tree_import_is_same_tree,cross_tree_import_admitted_qualified). ADD the groundedQualifiedName -> SourceRootRefindex (SourceRootIndex, lookup with fail-closedAmbiguouson a module bound to conflicting trees),tree_fundamentality_order, and theper-edge
cross_tree_edge_decision.compiler/program_assembly.dag— the assembly fold now pairs each parsed module root'sQualifiedNamewith its hostsource_roottag into the index;assemble_program_from_ingestresolves with that grounded index +source_root_set_from_ingestasactive_roots.compiler/03_name_resolve.dag— admission threads the index (replacing the globalorderscalar).resolve_with_admissionstays index-less single-tree;resolve_with_admission_groundedis the cross-tree authority. Deletes deadmodule_root_nodes_to_qns.Design note — fundamentality is a grounded relation, not a global scalar
The plan called for
order = MoreFundamental. Implemented as a tree-pair relation(
tree_fundamentality_order: v2→dsl =MoreFundamentaladmit, dsl→v2 =LessFundamentaldeny) rather than a caller-supplied global. A global
MoreFundamentalfails open on adsl→v2.stdpeer edge (layer direction holds at equal ordinals); deriving the order per paircloses that inversion (§5). This faithfully encodes the operator's decision (dsl is the
authority v2 builds on) as a single grounded authority.
Why grounding, not the QN-prefix guess (measured)
9
src/v2files declare non-v2.-prefixed modules (extdeps.shell,bisect.add,extdeps.fixture.*,test.claim.fold_list_generic_instantiation), so the prefix guessmis-tagged every one as
DslTree— unsound, not merely impure (the documented KNOWNLIMITATION the old scaffold carried).
Proven by execution (
claim_batch)name_resolve_cross_tree_resolution_witnessesgreen: same-tree dsl/v2 resolve; v2→dslcross-tree resolves (denied before grounding); dsl→v2 cross-tree denied fail-closed.
isolates to fundamentality — perturbing
tree_fundamentality_order(Dsl,V2)toMoreFundamentalflips it to FAIL.memo, admission fail-closed, malformed root, and PR-A's
source_root_taggingwitness.(
resolve_dual_imports_do_not_collide_on_header_metadatais pre-existing red on main —the dead TestClaim corpus, not a live
test fn; behavior unchanged by this PR.)🤖 Generated with Claude Code