From de1df113f509fe45176077675d6ec3e58007b21b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 29 Jun 2026 17:14:22 +0000 Subject: [PATCH] =?UTF-8?q?ITEM=202:=20construction=20=E2=86=92=20Declarat?= =?UTF-8?q?ionRef=20carrier=20+=20graph-property=20witness?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The keystone of the reference-grounding migration (#5952). WallNow's free-text `construction: String` becomes `WallNow { mechanism: ConstructionMechanism, authority: DeclarationRef }`, so "this lens chains to a real construction" stops being prose and becomes a WALKABLE graph property. Carrier (no mint, no widen): - ConstructionMechanism reused (std.disposition) — the 3 live sites map 1:1 onto its 3 variants, real §2 evidence the HOW-axis is right, not a guess: - intent_linearity → SingleAuthority + v2.lens.module_graph.import_closure_live - application_serializer → RealizationDispatch + v2.compiler.translate.target_serialize_source_from_model - cost → SubstrateMandatoryTag + v2.std.node.NodeKind (the closed Connective×Behavior kernel that MANDATES total cost — NOT SymbolicCost, which is the codomain and carries an UnknownCost escape; the totality prose dissolves into the tag + a ref) - authority is std.decl_ref.DeclarationRef VERBATIM — the one authority the disposition/determinism scaffold markers (#5954) bind through, byte-identical idiom. Witness (jolly-cat gates by execution): - wall_now_authority_graph_is_total: every WallNow authority resolves to a real top-level decl in the corpus → green over the 3 sites; perturb-to-RED by planting a dangling decl_name. - Resolution keys on identity (module_path + decl_name) kind-agnostically via the reused extract_top_level_decls (made pub — no second decl scanner forked). NOT a fn-index ∪ type-index union. - SCAFFOLD (DESIGN §6): host-side resolution stands in for a not-yet-exposed unified kind-agnostic .dag decl-resolution primitive (item (ii), coordinator-tracked resolver lane); marked to dissolve onto it. Discriminating control + parse-unit tests included. Plan doc: construction-justification-rule vacuity-residual now CLOSED (no free string survives in ConstructionClass); regenerated md. Drift gate green. Co-Authored-By: Claude Opus 4.8 --- docs/plans/construction-justification-rule.md | 2 +- .../plans/construction_justification_rule.dag | 2 +- src/v1/stage0/src/cli_run.rs | 176 ++++++++++++++++++ src/v1/stage0/src/fact_cardinality_census.rs | 2 +- src/v2/lens/application_serializer.dag | 5 +- .../common/construction_justification.dag | 6 +- src/v2/lens/cost.dag | 5 +- src/v2/lens/intent_linearity.dag | 5 +- 8 files changed, 193 insertions(+), 10 deletions(-) diff --git a/docs/plans/construction-justification-rule.md b/docs/plans/construction-justification-rule.md index d2e4d0ac1bd..3ee189651f8 100644 --- a/docs/plans/construction-justification-rule.md +++ b/docs/plans/construction-justification-rule.md @@ -37,7 +37,7 @@ So the bad state ("a lens with no recorded reason to be a lens") is unwritable b - `v2.lens.common.construction_justification` — the typed model (`ConstructionClass` + `ConstructionJustification`). - All 35 top-level `v2.lens.*` modules carry a recorded justification (retroactive classification from each lens's existing header — the audit that surfaces any lens that is secretly a `WallNow`). - Presence check + discriminating tests wired into `discover_floor_corpus_rows`. -- **Vacuity residual (honest bound):** the free-text prose payloads (the per-justification `rationale` and `RatchetForever`'s `undecidable_because`) were the stub-satisfiable surface — unverifiable strings that no consumer reads, a §6 parallel-ledger — and have been removed; the judgment now lives entirely in the *typed* `ConstructionClass` (the structured `dissolves_to: ConstructionMechanism` on `WallAfterGrounding` is grounded, not free text). The one remaining free string is `WallNow { construction }`; its empty-string vacuity stays a **WallAfterGrounding** until v2 gains a non-empty-string refinement (`NonEmptyStr` lives in `dsl/std/types.dag`; the v2 std omits it). Until then the empty-`construction` case is honest review residue, not a silent gap. +- **Vacuity residual — CLOSED.** Every `ConstructionClass` payload is now typed/grounded, no free string survives: the per-justification `rationale` and `RatchetForever`'s `undecidable_because` were removed (unverifiable §6 parallel-ledger prose no consumer reads); `WallAfterGrounding` carries the structured `dissolves_to: ConstructionMechanism`; and `WallNow`'s former free-text `construction` is now `{ mechanism: ConstructionMechanism, authority: DeclarationRef }` — the authority being the *one* `std.decl_ref.DeclarationRef` the disposition/determinism scaffold markers also bind through (no parallel ref type). So 'this lens chains to a real construction' is no longer prose but a **walkable graph property**: a host-side graph-property witness (`wall_now_authority_graph_is_total`) proves every `WallNow` authority resolves to a real top-level decl and goes RED on a planted dangling binding. That witness is a §6 scaffold (host-side resolution) dissolving onto a unified kind-agnostic decl-resolution primitive once exposed to `.dag`. - **Residue / follow-on (honest):** the *correctness* of each recorded class is review, not gated. Modules recorded as `WallNow` (cost, application_serializer) and the support module `affected_set_examples` flag a §3 home question — they are computations/support filed under `v2.lens.*`, not validation lenses; relocating them is out of scope here (it touches module resolution) and is left as a marked follow-up. ## Dissolution trigger (DESIGN §6) diff --git a/dsl/gunbc/plans/construction_justification_rule.dag b/dsl/gunbc/plans/construction_justification_rule.dag index e2cb627c86c..2bb10ad2b86 100644 --- a/dsl/gunbc/plans/construction_justification_rule.dag +++ b/dsl/gunbc/plans/construction_justification_rule.dag @@ -38,7 +38,7 @@ fn construction_justification_rule_body() -> List { li(text: "`v2.lens.common.construction_justification` — the typed model (`ConstructionClass` + `ConstructionJustification`)."), li(text: "All 35 top-level `v2.lens.*` modules carry a recorded justification (retroactive classification from each lens's existing header — the audit that surfaces any lens that is secretly a `WallNow`)."), li(text: "Presence check + discriminating tests wired into `discover_floor_corpus_rows`."), - li(text: "**Vacuity residual (honest bound):** the free-text prose payloads (the per-justification `rationale` and `RatchetForever`'s `undecidable_because`) were the stub-satisfiable surface — unverifiable strings that no consumer reads, a §6 parallel-ledger — and have been removed; the judgment now lives entirely in the *typed* `ConstructionClass` (the structured `dissolves_to: ConstructionMechanism` on `WallAfterGrounding` is grounded, not free text). The one remaining free string is `WallNow { construction }`; its empty-string vacuity stays a **WallAfterGrounding** until v2 gains a non-empty-string refinement (`NonEmptyStr` lives in `dsl/std/types.dag`; the v2 std omits it). Until then the empty-`construction` case is honest review residue, not a silent gap."), + li(text: "**Vacuity residual — CLOSED.** Every `ConstructionClass` payload is now typed/grounded, no free string survives: the per-justification `rationale` and `RatchetForever`'s `undecidable_because` were removed (unverifiable §6 parallel-ledger prose no consumer reads); `WallAfterGrounding` carries the structured `dissolves_to: ConstructionMechanism`; and `WallNow`'s former free-text `construction` is now `{ mechanism: ConstructionMechanism, authority: DeclarationRef }` — the authority being the *one* `std.decl_ref.DeclarationRef` the disposition/determinism scaffold markers also bind through (no parallel ref type). So 'this lens chains to a real construction' is no longer prose but a **walkable graph property**: a host-side graph-property witness (`wall_now_authority_graph_is_total`) proves every `WallNow` authority resolves to a real top-level decl and goes RED on a planted dangling binding. That witness is a §6 scaffold (host-side resolution) dissolving onto a unified kind-agnostic decl-resolution primitive once exposed to `.dag`."), li(text: "**Residue / follow-on (honest):** the *correctness* of each recorded class is review, not gated. Modules recorded as `WallNow` (cost, application_serializer) and the support module `affected_set_examples` flag a §3 home question — they are computations/support filed under `v2.lens.*`, not validation lenses; relocating them is out of scope here (it touches module resolution) and is left as a marked follow-up."), ]), ] diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index dca66a6d5e1..ba9afa80d74 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -2777,6 +2777,102 @@ fn declares_construction_justification(content: &str) -> bool { }) } +// ITEM 2 (reference grounding): the construction->authority graph witness. +// +// `WallNow.construction` was free-text prose; it is now +// `WallNow { mechanism: ConstructionMechanism, authority: DeclarationRef }`, so "this +// lens chains to a real construction" becomes a WALKABLE graph property: every WallNow +// authority must resolve to a real top-level decl in the corpus. The witness below proves +// that graph is TOTAL and goes RED if any binding dangles. +// +// SCAFFOLD (DESIGN §6): resolution is done HOST-SIDE here (extract authority refs from +// source + the kind-agnostic `extract_top_level_decls` over the resolved module), standing +// in for a not-yet-exposed unified .dag decl-resolution primitive. It keys on identity +// (module_path + decl_name), kind-agnostically — NOT a per-kind union (no fn-index ∪ +// type-index fork). Dissolve-on: item (ii) "unified kind-agnostic decl-resolution authority +// exposed to .dag" (coordinator-tracked, resolver/spine lane) — when it lands, this witness +// re-expresses over the .dag primitive and the host-side resolution is deleted. + +/// Extract every `authority: DeclarationRef { module_path: "..", decl_name: ".." }` in a +/// source file as `(module_path, decl_name)`. The field name `authority` typed +/// `DeclarationRef` is unique to `WallNow`, so this captures exactly the WallNow authorities. +pub fn wall_now_authority_refs(content: &str) -> Vec<(String, String)> { + const NEEDLE: &str = "authority: DeclarationRef {"; + let mut out = Vec::new(); + let mut rest = content; + while let Some(pos) = rest.find(NEEDLE) { + let after = &rest[pos + NEEDLE.len()..]; + if let (Some(mp), Some(dn)) = ( + quoted_field_value(after, "module_path:"), + quoted_field_value(after, "decl_name:"), + ) { + out.push((mp, dn)); + } + rest = after; + } + out +} + +/// The string literal following `` (the next `"..."`), whitespace/newline tolerant. +fn quoted_field_value(s: &str, field: &str) -> Option { + let start = s.find(field)? + field.len(); + let rest = &s[start..]; + let open = rest.find('"')? + 1; + let tail = &rest[open..]; + let close = tail.find('"')?; + Some(tail[..close].to_string()) +} + +/// Resolve WallNow authorities against the kind-agnostic top-level decl table of their +/// declaring module. Returns the unresolved refs as `(declaring_file, module_path, decl_name)`; +/// empty = the construction->authority graph is TOTAL. +pub fn construction_authority_unresolved( + module_to_content: &std::collections::HashMap, + authorities: &[(String, String, String)], +) -> Vec<(String, String, String)> { + authorities + .iter() + .filter(|(_, module_path, decl_name)| { + !module_to_content.get(module_path).is_some_and(|content| { + crate::fact_cardinality_census::extract_top_level_decls(content) + .iter() + .any(|(name, _)| name == decl_name) + }) + }) + .cloned() + .collect() +} + +/// Walk the corpus, collect WallNow authorities + the module->source map, and return the +/// unresolved refs (empty = total). The live driver behind the witness test. +pub fn construction_authority_graph_unresolved( + source_roots: &[String], +) -> Result, String> { + let mut module_to_content: std::collections::HashMap = + std::collections::HashMap::new(); + let mut authorities: Vec<(String, String, String)> = Vec::new(); + for root in source_roots { + let mut dag_files: Vec = Vec::new(); + collect_dag_files_tolerant(Path::new(root), &mut dag_files); + dag_files.sort(); + for path in dag_files { + let content = std::fs::read_to_string(&path) + .map_err(|e| format!("read {}: {e}", path.display()))?; + let file = path.to_string_lossy().into_owned(); + for (module_path, decl_name) in wall_now_authority_refs(&content) { + authorities.push((file.clone(), module_path, decl_name)); + } + if let Some(m) = extract_module_path(&content) { + module_to_content.insert(m, content); + } + } + } + Ok(construction_authority_unresolved( + &module_to_content, + &authorities, + )) +} + fn unjustified_lens_modules( module_to_path: &std::collections::HashMap, justified: &std::collections::BTreeSet, @@ -4220,7 +4316,9 @@ mod inert_lens_hygiene_tests { #[cfg(test)] mod construction_justification_hygiene_tests { use super::{ + construction_authority_graph_unresolved, construction_authority_unresolved, declares_construction_justification, discover_floor_corpus_rows, unjustified_lens_modules, + wall_now_authority_refs, }; use std::collections::{BTreeSet, HashMap}; use std::path::PathBuf; @@ -4297,6 +4395,84 @@ mod construction_justification_hygiene_tests { result.err().unwrap_or_default() ); } + + // ITEM 2 graph-property witness: the construction->authority graph is TOTAL over the + // live corpus (every WallNow authority DeclarationRef resolves to a real top-level decl). + // Perturb-to-RED: plant a dangling decl_name in any WallNow site -> this flips to a + // non-empty unresolved list and the test fails. (SCAFFOLD, dissolves on item (ii) — + // unified kind-agnostic decl-resolution exposed to .dag; see construction_authority_* docs.) + #[test] + fn wall_now_authority_graph_is_total() { + let ws = workspace_root(); + std::env::set_current_dir(&ws).expect("chdir to workspace root"); + let roots = vec![ + ws.join("dsl").to_string_lossy().into_owned(), + ws.join("src/v2").to_string_lossy().into_owned(), + ]; + let unresolved = + construction_authority_graph_unresolved(&roots).expect("corpus walk must succeed"); + assert!( + unresolved.is_empty(), + "every WallNow construction-authority must resolve to a real decl; dangling: {unresolved:?}" + ); + } + + // Discriminating control: the resolver detects a dangling authority and clears on a real one. + #[test] + fn dangling_authority_is_detected() { + let mut module_to_content: HashMap = HashMap::new(); + module_to_content.insert( + "v2.std.node".to_string(), + "module v2.std.node\ntype NodeKind\n = TypeNode { connective: Connective }\n" + .to_string(), + ); + + let real = vec![( + "src/v2/lens/cost.dag".to_string(), + "v2.std.node".to_string(), + "NodeKind".to_string(), + )]; + assert!( + construction_authority_unresolved(&module_to_content, &real).is_empty(), + "a real authority (v2.std.node.NodeKind) must resolve" + ); + + let dangling = vec![( + "src/v2/lens/cost.dag".to_string(), + "v2.std.node".to_string(), + "NoSuchDecl".to_string(), + )]; + assert_eq!( + construction_authority_unresolved(&module_to_content, &dangling).len(), + 1, + "a dangling decl_name must be flagged unresolved" + ); + + let missing_module = vec![( + "src/v2/lens/cost.dag".to_string(), + "v2.absent.module".to_string(), + "NodeKind".to_string(), + )]; + assert_eq!( + construction_authority_unresolved(&module_to_content, &missing_module).len(), + 1, + "an authority whose module is absent must be flagged unresolved" + ); + } + + // Parse unit: extraction pulls (module_path, decl_name) from a WallNow authority, + // whitespace/newline tolerant, and ignores non-WallNow DeclarationRef binds. + #[test] + fn wall_now_authority_refs_extraction() { + let src = " class: WallNow {\n mechanism: SubstrateMandatoryTag,\n authority: DeclarationRef { module_path: \"v2.std.node\", decl_name: \"NodeKind\", field: WholeDeclaration }\n }\n"; + assert_eq!( + wall_now_authority_refs(src), + vec![("v2.std.node".to_string(), "NodeKind".to_string())] + ); + // a Scaffold `bind: DeclarationRef { .. }` has no `authority:` field -> not captured. + let other = " bind: DeclarationRef { module_path: \"x.y\", decl_name: \"Z\", field: WholeDeclaration }\n"; + assert!(wall_now_authority_refs(other).is_empty()); + } } #[cfg(test)] diff --git a/src/v1/stage0/src/fact_cardinality_census.rs b/src/v1/stage0/src/fact_cardinality_census.rs index fafca3a5a05..10368c45ba8 100644 --- a/src/v1/stage0/src/fact_cardinality_census.rs +++ b/src/v1/stage0/src/fact_cardinality_census.rs @@ -41,7 +41,7 @@ fn decl_body_hash(body: &str) -> String { crate::v1_rt::atom_identity_hash(normalize_decl_body(body)) } -fn extract_top_level_decls(content: &str) -> Vec<(String, String)> { +pub fn extract_top_level_decls(content: &str) -> Vec<(String, String)> { let lines: Vec<&str> = content.lines().collect(); let mut out = Vec::new(); let mut i = 0; diff --git a/src/v2/lens/application_serializer.dag b/src/v2/lens/application_serializer.dag index a2ff5af88f0..65fc8e67b7c 100644 --- a/src/v2/lens/application_serializer.dag +++ b/src/v2/lens/application_serializer.dag @@ -1,5 +1,7 @@ module v2.lens.application_serializer import v2.lens.common.construction_justification { ConstructionJustification, WallNow } +import std.disposition { RealizationDispatch } +import std.decl_ref { DeclarationRef, WholeDeclaration } import extdeps.communication.medium { Medium } import v2.compiler.translate { target_serialize_source_from_model } @@ -45,6 +47,7 @@ fn serialize_diff_as_source_patch( data construction_justification: ConstructionJustification = ConstructionJustification { class: WallNow { - construction: "the row-driven grammar inverse (DESIGN sec 4: emit = apply_diff . serialize, one grammar read backward) realized in v2.compiler translate" + mechanism: RealizationDispatch, + authority: DeclarationRef { module_path: "v2.compiler.translate", decl_name: "target_serialize_source_from_model", field: WholeDeclaration } } } diff --git a/src/v2/lens/common/construction_justification.dag b/src/v2/lens/common/construction_justification.dag index bb3eeb1ec90..26f0b1d0637 100644 --- a/src/v2/lens/common/construction_justification.dag +++ b/src/v2/lens/common/construction_justification.dag @@ -1,12 +1,12 @@ module v2.lens.common.construction_justification -import v2.std.text { String } - import std.disposition { ConstructionMechanism } +import std.decl_ref { DeclarationRef } + type ConstructionClass - = WallNow { construction: String } + = WallNow { mechanism: ConstructionMechanism, authority: DeclarationRef } | WallAfterGrounding { dissolves_to: ConstructionMechanism } diff --git a/src/v2/lens/cost.dag b/src/v2/lens/cost.dag index b592d783e2a..64f61113abb 100644 --- a/src/v2/lens/cost.dag +++ b/src/v2/lens/cost.dag @@ -1,5 +1,7 @@ module v2.lens.cost import v2.lens.common.construction_justification { ConstructionJustification, WallNow } +import std.disposition { SubstrateMandatoryTag } +import std.decl_ref { DeclarationRef, WholeDeclaration } import v2.extdeps.languages.llvm_ir { LlvmInstruction } import v2.std.algebra { @@ -669,6 +671,7 @@ fn llvm_instruction_cost(i: LlvmInstruction) -> Int { data construction_justification: ConstructionJustification = ConstructionJustification { class: WallNow { - construction: "cost is TOTAL over the closed 6-connective x 5-behavior kernel -- anything expressible is kernel-composed, so it has a SymbolicCost by construction (a new connective/behavior is a C1 STOP)" + mechanism: SubstrateMandatoryTag, + authority: DeclarationRef { module_path: "v2.std.node", decl_name: "NodeKind", field: WholeDeclaration } } } diff --git a/src/v2/lens/intent_linearity.dag b/src/v2/lens/intent_linearity.dag index 81cbc699a96..7739ddcbe43 100644 --- a/src/v2/lens/intent_linearity.dag +++ b/src/v2/lens/intent_linearity.dag @@ -1,6 +1,7 @@ module v2.lens.intent_linearity import v2.lens.common.construction_justification { ConstructionJustification, ConstructionClass, WallNow, WallAfterGrounding, RatchetForever } import std.disposition { SingleAuthority } +import std.decl_ref { DeclarationRef, WholeDeclaration } import v2.lens.simulated_relationship { chain_is_simulated } import v2.lens.structural_similarity { type_decls_anti_unify } import v2.lens.complexity_lowering { cost_is_lowerable } @@ -71,7 +72,7 @@ fn import_graph_rule() -> ParallelRepresentationRule { name: ^consumed_input_closure, axis: ChangeTime, representation: ImportGraph, - class: WallNow { construction: "v2.lens.module_graph.import_closure_live" }, + class: WallNow { mechanism: SingleAuthority, authority: DeclarationRef { module_path: "v2.lens.module_graph", decl_name: "import_closure_live", field: WholeDeclaration } }, derive: fn(entry, roots) { import_closure_live(entry_path: entry, pool_roots: roots) } } } @@ -102,7 +103,7 @@ fn closure_is_clean( derived: FreeMonoid ) -> Bool { match rule.class { - WallNow { construction: _ } => !closure_drift(declared: declared, derived: derived) + WallNow { mechanism: _, authority: _ } => !closure_drift(declared: declared, derived: derived) WallAfterGrounding { dissolves_to: _ } => true RatchetForever => true }