ITEM 2: construction → DeclarationRef carrier + graph-property witness

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)

dsl/gunbc/plans/construction_justification_rule.dag

@@ -38,7 +38,7 @@ fn construction_justification_rule_body() -> List<MarkdownBlock> {
       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."),
     ]),
   ]

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 `<field>` (the next `"..."`), whitespace/newline tolerant.
+fn quoted_field_value(s: &str, field: &str) -> Option<String> {
+    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<String, String>,
+    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<Vec<(String, String, String)>, String> {
+    let mut module_to_content: std::collections::HashMap<String, String> =
+        std::collections::HashMap::new();
+    let mut authorities: Vec<(String, String, String)> = Vec::new();
+    for root in source_roots {
+        let mut dag_files: Vec<PathBuf> = 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<String, String>,
     justified: &std::collections::BTreeSet<String>,
@@ -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<String, String> = 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)]

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;

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 }
   }
 }

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 }
 

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 }
   }
 }

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<String>
 ) -> 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
   }