Repository navigation
Post-#6210: whole-floor import_closure semantic oracle (live == legacy BFS) - #6231
Merged
Merged
Conversation
gunbai-bot
Bot
changed the title
Integrate latest main (ratchet/host-effect lanes) and apply rustfmt to cli_run import_closure_equivalence_tests so rust gate fmt passes. Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
added a commit
that referenced
this pull request
Jul 5, 2026
Node-grain equivalence (whole-tree InferredTree resolve) stays BLOCKED per docs/plans/affected-set-precompute-pruning.md — unaffordable, per gentle-owl-459's measurement (whole_tree_resolved_ctx ran 54min without completing). Re-scoped to MODULE grain, using the already-landed import_closure_live authority (#6210/#6231). Adds a thin .dag projection (entry_affected_by_touched_paths / _excluding, v2.lens.module_graph) expressing "entry E is affected by touched-path set T iff T intersects import_closure_live(E)" — the same decision the Rust host already makes via touched_file_in_import_closure over import_closure_files_from_graph (both fed by the same host-realized import_resolution_facts/module_declaration_facts, so this is one fact projected two ways, not a second closure algorithm). Proves by execution (cli_run.rs module_grain_affected_equivalence_tests): - Two real merged-commit diffs (one dag/-only, one src/v2/-only): the .dag decision and the Rust decision agree on every sampled entry. - One discriminating control: excluding an intermediate importer's outgoing edges actually flips the decision (proves the receipts above are a real discriminator, not a tautology). - Cost numbers: resolve/build call counts, wall-clock, peak RSS. No cutover — the live floor skip decision in cli_run.rs is untouched. Also fixes a map_get/Outcome pattern mismatch in module_graph.dag (map_get returns Accepted/Rejected, not Present/Absent directly) surfaced while exercising these paths through the interpreter.
briansrls
added a commit
that referenced
this pull request
Jul 5, 2026
* WIP: Affected-set Step 3: module-grain frontier equivalence receipts * WIP: Affected-set Step 3: module-grain frontier equivalence receipts * WIP: Affected-set Step 3: module-grain frontier equivalence receipts * Affected-set Step 3: module-grain frontier equivalence receipts Node-grain equivalence (whole-tree InferredTree resolve) stays BLOCKED per docs/plans/affected-set-precompute-pruning.md — unaffordable, per gentle-owl-459's measurement (whole_tree_resolved_ctx ran 54min without completing). Re-scoped to MODULE grain, using the already-landed import_closure_live authority (#6210/#6231). Adds a thin .dag projection (entry_affected_by_touched_paths / _excluding, v2.lens.module_graph) expressing "entry E is affected by touched-path set T iff T intersects import_closure_live(E)" — the same decision the Rust host already makes via touched_file_in_import_closure over import_closure_files_from_graph (both fed by the same host-realized import_resolution_facts/module_declaration_facts, so this is one fact projected two ways, not a second closure algorithm). Proves by execution (cli_run.rs module_grain_affected_equivalence_tests): - Two real merged-commit diffs (one dag/-only, one src/v2/-only): the .dag decision and the Rust decision agree on every sampled entry. - One discriminating control: excluding an intermediate importer's outgoing edges actually flips the decision (proves the receipts above are a real discriminator, not a tautology). - Cost numbers: resolve/build call counts, wall-clock, peak RSS. No cutover — the live floor skip decision in cli_run.rs is untouched. Also fixes a map_get/Outcome pattern mismatch in module_graph.dag (map_get returns Accepted/Rejected, not Present/Absent directly) surfaced while exercising these paths through the interpreter. * WIP: Affected-set Step 3: module-grain frontier equivalence receipts * Fix Step 3 receipt: derive touched paths via floor_diff_edits_from_diff_text, not raw git-show paths Review finding (cursor/composer-2.5 on PR #6274): the equivalence receipt fed both sides raw `git show --name-only` file paths, but the live production decision it claims to prove equivalence with — entry_file_touched (cli_run.rs:5217-5221) — is decided over diff_edits.touched_entry_files, a FILTERED set (floor_diff_edits_from_line_ranges excludes pure data-item and test-fn edits). A commit's raw touched-path superset can diverge from that filtered set, so the receipt was proving a looser predicate, not the real one. Fix: derive touched paths via the real floor_diff_edits_from_diff_text call (full `git show <sha>` unified diff -> .touched_entry_files), matching the sibling green_import_closure_helper_fn_edit_runs_importer_entry pattern the reviewer pointed to. Also: - Replaced DAG_ONLY_SHA (81febee..., all new files) with 6edafbb (4 modify-only dag/ files) — floor_diff_edits_from_line_ranges fail-closes on any diff touching line 1, which every new file's diff does, so the old commit could never exercise the real production path at all. - Fixed a duplicate-module-declaration bug surfaced while wiring this up: mixing absolute roots/entries with the diff's inherently repo-relative paths re-resolved the same file under two identities; switched to the relative-path convention the live floor itself uses throughout. All 3 tests still pass: discriminating control + both real-diff equivalence receipts, zero divergence. * cargo fmt Fix formatting from the touched-paths derivation fix (78e1851). * WIP: Affected-set Step 3: module-grain frontier equivalence receipts * Fix review findings: fail-closed map_lookup proof + suffix-tolerant path matching Finding 1 (map_lookup Rejected->Absent coercion): decidably unreachable for this file's call sites -- both call sites only ever pass Maps built via empty_map/map_insert, whose lookup chain can only ever surface Holds or a Violates tagged ^map_key_absent, which map_get already special-cases to Accepted(Absent). Documented the proof as a modeled data-decl (the .dag parser rejects // comments) rather than leaving the coercion silent. Finding 2 (exact vs suffix-tolerant path matching): touched_path_in_closure compared paths with bare string_eq, but the Rust production predicate it mirrors (span_file_matches/touched_file_in_import_closure, cli_run.rs) normalizes and tolerates suffix matches. Added path_matches_touched using the existing starts_with/ends_with/substring builtins to mirror that semantics exactly, so a path pair where suffix matching succeeds but exact equality fails decides the same on both sides. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> * WIP: Affected-set Step 3: module-grain frontier equivalence receipts * WIP: Affected-set Step 3: module-grain frontier equivalence receipts * WIP: Affected-set Step 3: module-grain frontier equivalence receipts --------- Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Claude Sonnet 5 <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.
Summary
Extends the post-#6210 closure-equivalence guard from four spot-check entries to the full floor witness roster (~514
*_test.dagentries underwitness_layer_roots, minus model exclusions).For every enrolled entry, proves set-identity among:
resolve_transitively_bfs_legacy)resolve_transitively(Phase 1 consumer)import_closure_live_paths_with_facts(.dagauthority host realization)Refactors the equivalence helper to thread pre-built
ModuleGraphFactsLiveonce per oracle run (no per-entry corpus re-scan).Test plan
CTRL_BUILD_BYPASS_SHIMS=1 cargo test -p v1-compiler import_closure_equivalence— 10/10 pass (~69s; whole-floor roster ~514 entries)claim_batch --claim-runonimport_closure_live_test.dag(3 DAG witnesses: green equals declared conformance closure + RED under/over controls)