Skip to content

Tier-2 step 3: make the intent-lens ImportGraph row live (import_closure_is_clean_live over module_graph.import_closure_live) [stacked on #5669] - #5703

Merged
briansrls merged 16 commits into
mainfrom
step3-dev-on-5669
Jun 24, 2026
Merged

briansrls merged 16 commits into
mainfrom
step3-dev-on-5669

Conversation

@briansrls

@briansrls briansrls commented Jun 24, 2026 •

Copy link
Copy Markdown
Contributor

Tier-2 step 3: make the intent-lens ImportGraph row LIVE (shape B)

Final step of the Tier-2 grounding. Steps 1+2 (the module_declaration_facts builtin + the .dag fixpoint-fold import_closure / import_closure_live in v2.lens.module_graph) merged as #5675. This step wires the lens row itself to derive its closure live and dissolves the host-projected ClosureFact.derived scaffold #5669 introduced.

What changes (delta over #5669)

src/v2/lens/intent_linearity.dag:

  • ParallelRepresentationRule gains a derive: fn(String, List<String>) -> FreeMonoid<String> field (the "live walk fn field" the Tier-2 dissolution trigger named). import_graph_rule().derive = v2.lens.module_graph.import_closure_live; WallNow.construction promoted from the String resolve_imports_transitively (Rust-oracle pointer) to name that live fn.
  • DISSOLVED the ClosureFact type (incl. its stored derived field) and the old import_closure_is_clean(fact) predicate — a stored derived is the redundant second authority the promotion removes, and a writable host-fact carrier is the §5 fail-open.
  • closure_is_clean / closure_drift / closure_is_clean_for_representation are now a pure dispatch kernel over (rule, declared, derived) path-lists.
  • import_closure_is_clean_live(declared, entry_path, pool_roots) is the sole tree-level authority: it produces derived via import_graph_rule.derive and feeds the kernel. No stored/host-projected derived exists for a future caller to misuse.

Witnesses (src/v2/test/claim/intent_linearity/lens_unit/):

  • import_graph_live_test.dag (new): the lens predicate over the real corpus — declared from tools.rust_stage0_gates.coproduct_reflection_conformance_consumed_closure, derived live over witness_layer_roots. Both-direction discriminating teeth (drop entry → red, add bogus → red). 3/3 PASS by execution.
  • import_graph_test.dag: refactored off ClosureFact to feed literal declared/derived lists to the pure kernel (the class-dispatch unit seam: WallNow vs WallAfterGrounding without a live tree). 9/9 PASS.

⚠️ Stacked on #5669 (keep DRAFT until #5669 merges)

Built on session/swift-bat-896 (#5669, which introduces the ImportGraph row) merged with main. The diff against main therefore includes #5669's content. Once #5669 merges, I merge main in — its content drops out, leaving the step-3 delta — re-confirm green, then flip ready. Not independently mergeable before #5669.

🤖 Generated with Claude Code

Brian Searls and others added 11 commits June 23, 2026 19:56
… drift wall

D1 (wall now): Rust drift oracle (consumed_input_closure_drift_test.rs) asserts
each declared ConsumedInputClosure equals its transitive import-graph closure
over the live corpus, closing the admitted slice1_status fail-open. Discriminating
in both directions (drop-path under-declared / bogus-add over-declared -> red).

D2 (modeled lens): Representation gains ImportGraph; ParallelRepresentationRule
family carries a populated ConstructionClass verdict (reused, not minted) so a
WallNow drift is a hard violation while a WallAfterGrounding/RatchetForever drift
is tracked, not failed. Registry-wired via closure_is_clean_for_representation;
lens_unit witnesses both drift directions, set-not-order, and the trichotomy
dispatch. Tier-2 (live .dag walk) named as the dissolution trigger.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…chor binding name

extdeps.ctrl.jobserver (added by #5650) declared its ExternalAuthority as
data ctrl_jobserver_authority, but the extdeps_external_authority gate scans for
a data item named exactly extdeps_external_authority_anchor (every other extdeps
module conforms). The author-provided Https authority URI is correct; only the
binding name was off, so the gate read the anchor as missing -> RED. Main CI was
severely backlogged (runs queued >1h) so main's tip shipped this red unvalidated.
Rename to the recognized convention (value unchanged); no other reference to the
old name. Heals the gate on this PR's merge.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@gunbai-bot gunbai-bot Bot changed the title Tier-2: ground the import closure in .dag — module_declaration_facts builtin + .dag fixpoint-fold closure, make the intent-lens ImportGraph row live Tier-2 step 3: make the intent-lens ImportGraph row live (import_closure_is_clean_live over module_graph.import_closure_live) [stacked on #5669] Jun 24, 2026
Brian Searls and others added 4 commits June 24, 2026 03:09
…e witness

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…-crane §3)

Remove the stored ClosureFact.derived field and import_closure_is_clean(fact):
a stored derived field is the redundant second authority the promotion
dissolves, and a writable host-fact carrier is the fail-open. closure_is_clean
becomes a pure dispatch kernel over (rule, declared, derived) lists;
import_closure_is_clean_live is the SOLE tree-level authority (derives via
import_graph_rule.derive). Synthetic lens_unit feeds literal lists to the kernel
(class-dispatch seam). Green by execution: live 3/3, synthetic 9/9.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
# Conflicts:
#	src/v2/lens/intent_linearity.dag
#	src/v2/test/claim/intent_linearity/lens_unit/import_graph_test.dag
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review June 24, 2026 13:24
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