Consolidation #4553 Phase 1: model-first verification.dag BoolWitness/UnifiedTestClaim, gated PR with before-after cut-list and execution-equivalence tranche

docs/planning/test-claim-consolidation-phase1-cut-list-2026-06-09.md

@@ -0,0 +1,37 @@
+# Test-Claim Consolidation #4553 — Phase 1 cut list
+
+**PR:** #4576  
+**Design authority:** `docs/planning/test-claim-consolidation-design-2026-06-08.md` §Phase 1  
+**Gate:** Mgr-C substrate-only; no runner / CI transport / roster deletion
+
+## Before → after
+
+| artifact | before | after |
+| -------- | ------ | ----- |
+| `src/v4/std/verification.dag` | `TestClaim` coproduct only | + `BoolWitness` (`function: Symbol`), `TestClaimTransportMode`, `UnifiedTestClaimModality`, `UnifiedTestClaim` (both arms, dissolution receipts), `unified_test_claim_bool_witness` fail-closed `Outcome` projection |
+| `src/v4/test/claim/workflow/v4_roster_pilot.dag` | `V4RosterPilotClaimRunRow` list only | + `function_symbol: Symbol` pins per row, `bool_witness_from_roster_row` mechanical projection (`function` String retained for shell transport) |
+| `src/v4/test/claim/workflow/unified_test_claim_substrate_equivalence.dag` | absent | Phase 1 compile-time equivalence tranche (`substrate_equivalence_holds`) |
+
+## Explicit non-changes (this PR)
+
+| artifact | reason |
+| -------- | ------ |
+| `src/v4/compiler/05_eval.dag` | `TestClaimEvalSubject` binds at eval boundary — Phase 2 runner |
+| `testclaim_corpus_runner.dag` | runner dispatch deferred Phase 2 |
+| `v4_roster_pilot` row list / count | authoritative until C9–C11 (design §4.4) |
+| `workflow/*_eval.dag` (10 files) | retire Phase 3 |
+| lens-CI / smoke shell scripts | CI transport unification Phase 4 |
+
+## Falsification receipts landed
+
+| ID | receipt |
+| -- | ------- |
+| C3 | `rg 'UnifiedTestClaim\|BoolWitness' src/v4/std/verification.dag` |
+| Phase 1 tranche | `witness_substrate_equivalence` in `unified_test_claim_substrate_equivalence.dag` |
+
+## Deferred to Phase 2+
+
+- `UnifiedClaimRun` / tagged `CorpusEvalReport` run receipts  
+- `run_unified_corpus_eval` dispatch  
+- E1 (`--claim-run` stdout equivalence)  
+- `NodeCorpus.subject: TestClaimEvalSubject<Node>` field (std/eval layering)

src/v4/std/verification.dag

@@ -1,13 +1,15 @@
 // src/v4/std/verification.dag
-// Scope: Closed TestClaim schema — assertion-shape coproduct, TestgenTier/Layer, TestClassification, ImpossibleBugClass, ManualAnchorKey, GeneratedAnchorKey, ClaimAnchorKey.
+// Scope: Closed TestClaim schema — assertion-shape coproduct, TestgenTier/Layer, TestClassification, ImpossibleBugClass, ManualAnchorKey, GeneratedAnchorKey, ClaimAnchorKey; consolidation #4553 Phase 1 — BoolWitness + UnifiedTestClaim registration coproduct.
 // Status: T-3 modeled; substrate extension or file split = operator STOP.
 
 module v4.std.verification
 
 
 import v4.std.algebra { Empty, any, fold_list, list_append, list_snoc_item }
 import v4.std.collection { List }
+import v4.std.logic { Bool }
 import v4.std.node { Node, NodeFold, Symbol, fold_node }
+import v4.std.target_model { TargetModel }
 import v4.std.diagnostic {
   Accepted,
   Correction,
@@ -30,6 +32,7 @@ import v4.std.diagnostic {
 
 data v4_std_verification_file: Symbol = v4_std_verification_file
 data test_claim_expected_outcome_undeclared: Symbol = test_claim_expected_outcome_undeclared
+data unified_test_claim_bool_witness_absent: Symbol = unified_test_claim_bool_witness_absent
 
 
 fn test_claim_expected_outcome_undeclared_diagnostic() -> Diagnostic {
@@ -41,6 +44,15 @@ fn test_claim_expected_outcome_undeclared_diagnostic() -> Diagnostic {
 }
 
 
+fn unified_test_claim_bool_witness_absent_diagnostic() -> Diagnostic {
+  Diagnostic {
+    reason: unified_test_claim_bool_witness_absent,
+    at: Textual { file: v4_std_verification_file, extent: WholeFile },
+    correction: Unavailable { reason: UserInputBoundary }
+  }
+}
+
+
 // RULING-1: pretty-much-done — closed TestClaim tier set.
 // 🟢 coproduct dissolution — LB-P4-3212.
 type TestgenTier
@@ -464,3 +476,80 @@ fn test_claim_expected_outcome(c: TestClaim) -> Outcome<Outcome<Node>> {
       }
   }
 }
+
+
+// Consolidation #4553 Phase 1 — Bool-witness registration descriptor (ctrl#1490 / test-claim-consolidation-design §3).
+// P2: descriptor fields only — execution output lives on run-receipt types in Phase 2 eval module.
+// RULING-1: pretty-much-done — nullary fn () -> Bool witness identity at registration boundary.
+// 🟢 coproduct dissolution — consolidation #4553 Phase 1 terminal registration descriptor.
+type BoolWitness {
+  entry: String
+  function: Symbol
+}
+
+
+// Node-corpus transport mode on `UnifiedTestClaim.NodeCorpus` — not a separate runner.
+// RULING-1: pretty-much-done — closed NodeCorpus transport modes (design §3.4).
+// 🟢 coproduct dissolution — consolidation #4553 Phase 1.
+type TestClaimTransportMode
+// 🟢 coproduct dissolution — consolidation #4553 Phase 1
+  = EvalOnly
+  | EmitVsEval { target: TargetModel }
+
+
+// Structural modality tag for unified dispatch — keys off the coproduct arm, not string heuristics.
+// RULING-1: pretty-much-done — closed modality tag for unified dispatch (design §3.1).
+// 🟢 coproduct dissolution — consolidation #4553 Phase 1.
+type UnifiedTestClaimModality
+// 🟢 coproduct dissolution — consolidation #4553 Phase 1
+  = UnifiedNodeCorpusModality
+  | UnifiedBoolWitnessModality
+
+
+// Unified registration coproduct (both modalities, one authority).
+// `NodeCorpus` carries `claim` + `transport` at std layer; `TestClaimEvalSubject` binds at the
+// eval boundary in Phase 2 runner migration (std cannot import `v4.compiler.eval`).
+// RULING-1: needs-more-work — NodeCorpus lacks TestClaimEvalSubject until Phase 2 runner migration.
+// 🟡 coproduct dissolution — consolidation #4553 Phase 2 binds subject at eval boundary; dissolve-on: NodeCorpus.subject lands when unified runner migrates.
+type UnifiedTestClaim
+// 🟡 coproduct dissolution — consolidation #4553 Phase 2 runner migration
+  = NodeCorpus {
+      claim: TestClaim
+      transport: TestClaimTransportMode
+    }
+  | BoolWitnessClaim { witness: BoolWitness }
+
+
+fn unified_test_claim_modality(c: UnifiedTestClaim) -> UnifiedTestClaimModality {
+  match c {
+    NodeCorpus { claim: _, transport: _ } => UnifiedNodeCorpusModality
+    BoolWitnessClaim { witness: _ } => UnifiedBoolWitnessModality
+  }
+}
+
+
+fn bool_witness_descriptor(w: BoolWitness) -> UnifiedTestClaim {
+  BoolWitnessClaim { witness: w }
+}
+
+
+// Arm-specific projection — Rejected on NodeCorpus (no fabricated empty String/Symbol).
+fn unified_test_claim_bool_witness(c: UnifiedTestClaim) -> Outcome<BoolWitness> {
+  match c {
+    BoolWitnessClaim { witness: w } =>
+      Accepted { value: w, diagnostics: None }
+    NodeCorpus { claim: _, transport: _ } =>
+      Rejected {
+        diagnostics: diagnostics_singleton(d: unified_test_claim_bool_witness_absent_diagnostic())
+      }
+  }
+}
+
+
+fn bool_witness_matches_entry_function(
+  w: BoolWitness,
+  entry: String,
+  function: Symbol
+) -> Bool {
+  w.entry == entry && w.function == function
+}

src/v4/test/claim/workflow/unified_test_claim_substrate_equivalence.dag

@@ -0,0 +1,94 @@
+// src/v4/test/claim/workflow/unified_test_claim_substrate_equivalence.dag
+// Scope: Consolidation #4553 Phase 1 substrate equivalence tranche (design §6.3).
+// Status: compile-time law — C3 modality discrimination + roster mechanical projection (E5 prep).
+// No runner / `--claim-run` execution in this tranche (E1 lands Phase 2).
+
+module v4.test.claim.workflow.unified_test_claim_substrate_equivalence
+
+
+import v4.std.diagnostic { Accepted, Rejected }
+import v4.std.logic { Bool }
+import v4.std.verification {
+  EvalOnly,
+  NodeCorpus,
+  UnifiedBoolWitnessModality,
+  UnifiedNodeCorpusModality,
+  UnifiedTestClaim,
+  bool_witness_descriptor,
+  bool_witness_matches_entry_function,
+  unified_test_claim_bool_witness,
+  unified_test_claim_modality
+}
+import v4.test.claim.manual.eval_runtime_mvp { claim_eval_mvp2_test_claim_route }
+import v4.test.claim.workflow.v4_roster_pilot {
+  bool_witness_from_roster_row,
+  v4_roster_pilot_claim_run_row_transport_symbol_consistency_holds,
+  v4_roster_pilot_row_edit_locus_narrow
+}
+
+
+fn substrate_equivalence_sample_bool_unified_claim() -> UnifiedTestClaim {
+  bool_witness_descriptor(
+    w: bool_witness_from_roster_row(row: v4_roster_pilot_row_edit_locus_narrow)
+  )
+}
+
+
+fn substrate_equivalence_sample_node_corpus_claim() -> UnifiedTestClaim {
+  NodeCorpus {
+    claim: claim_eval_mvp2_test_claim_route,
+    transport: EvalOnly
+  }
+}
+
+
+fn substrate_equivalence_roster_projection_preserves_entry_function() -> Bool {
+  let w = bool_witness_from_roster_row(row: v4_roster_pilot_row_edit_locus_narrow)
+  bool_witness_matches_entry_function(
+    w: w,
+    entry: v4_roster_pilot_row_edit_locus_narrow.entry,
+    function: v4_roster_pilot_row_edit_locus_narrow.function_symbol
+  )
+}
+
+
+fn substrate_equivalence_bool_modality_discriminates() -> Bool {
+  match unified_test_claim_modality(c: substrate_equivalence_sample_bool_unified_claim()) {
+    UnifiedBoolWitnessModality => true
+    UnifiedNodeCorpusModality => false
+  }
+}
+
+
+fn substrate_equivalence_node_corpus_modality_discriminates() -> Bool {
+  match unified_test_claim_modality(c: substrate_equivalence_sample_node_corpus_claim()) {
+    UnifiedNodeCorpusModality => true
+    UnifiedBoolWitnessModality => false
+  }
+}
+
+
+fn substrate_equivalence_unified_claim_preserves_bool_fields() -> Bool {
+  let w = bool_witness_from_roster_row(row: v4_roster_pilot_row_edit_locus_narrow)
+  match unified_test_claim_bool_witness(c: bool_witness_descriptor(w: w)) {
+    Accepted { value: extracted, diagnostics: None } =>
+      bool_witness_matches_entry_function(
+        w: extracted,
+        entry: w.entry,
+        function: w.function
+      )
+    Rejected { diagnostics: _ } => false
+  }
+}
+
+
+fn substrate_equivalence_holds() -> Bool {
+  v4_roster_pilot_claim_run_row_transport_symbol_consistency_holds()
+    && substrate_equivalence_roster_projection_preserves_entry_function()
+    && substrate_equivalence_bool_modality_discriminates()
+    && substrate_equivalence_node_corpus_modality_discriminates()
+    && substrate_equivalence_unified_claim_preserves_bool_fields()
+}
+
+
+data witness_substrate_equivalence: Bool = substrate_equivalence_holds()