v2 no longer treats source identity as semantic grounding (P0: protect the replacement compiler)

src/v2/compiler/05_eval.dag

@@ -1,11 +1,15 @@
 module v2.compiler.eval
 
 import v2.compiler.infer {
+  DerivedGrounding,
+  GroundingNotDerived,
   InferredFacts,
   InferredTree,
-  canonical_grounding_admits_infer_facts,
   infer_facts_lookup_miss_diagnostic,
+  inferred_facts_canonical_admitted,
+  inferred_facts_cover_node,
   inferred_facts_descent,
+  inferred_facts_grounding_derived,
   inferred_facts_resolved_type
 }
 import std.algebra { Cons, Empty }
@@ -780,18 +784,36 @@ fn descent_witness_digest(d: Witness<v2.std.cardinality.TerminationProof>) -> Ha
   }
 }
 
+fn eval_grounding_not_derived_digest_node() -> Node {
+  Node {
+    kind: TypeNode { connective: Atom { identity: ^eval_grounding_not_derived_digest_tag } },
+    children: [],
+    occurrence_id: SyntheticOccurrence
+  }
+}
+
 fn inferred_facts_digest(facts: InferredFacts) -> Hash {
-  let g = facts.grounding
-  combine_hash(
-    a: content_hash(n: g.node),
-    b: combine_hash(
-      a: combine_hash(
-        a: structural_property_witness_digest(w: g.witness.structural),
-        b: structural_property_witness_digest(w: g.witness.closedness)
-      ),
-      b: descent_witness_digest(d: inferred_facts_descent(facts: facts))
-    )
-  )
+  match facts.grounding {
+    DerivedGrounding { grounding: g } =>
+      combine_hash(
+        a: content_hash(n: g.node),
+        b: combine_hash(
+          a: combine_hash(
+            a: structural_property_witness_digest(w: g.witness.structural),
+            b: structural_property_witness_digest(w: g.witness.closedness)
+          ),
+          b: descent_witness_digest(d: inferred_facts_descent(facts: facts))
+        )
+      )
+    GroundingNotDerived { node: n } =>
+      combine_hash(
+        a: combine_hash(
+          a: content_hash(n: eval_grounding_not_derived_digest_node()),
+          b: content_hash(n: n)
+        ),
+        b: descent_witness_digest(d: inferred_facts_descent(facts: facts))
+      )
+  }
 }
 
 fn inferred_node_facts_cache_digest(tree: InferredTree, node: Node) -> Hash {
@@ -979,13 +1001,19 @@ fn inferred_facts_witness_for_eval(tree: InferredTree, node: Node) -> Witness<In
 fn inferred_facts_for_eval(tree: InferredTree, node: Node) -> Outcome<InferredFacts> {
   match inferred_facts_witness_for_eval(tree: tree, node: node) {
     Holds { value: facts } =>
-      if facts.grounding.node != node {
+      if !inferred_facts_grounding_derived(facts: facts) {
+        Rejected {
+          diagnostics: diagnostics_singleton(
+            d: eval_diagnostic(reason: ^eval_rejected_grounding_not_derived, node: node)
+          )
+        }
+      } else if !inferred_facts_cover_node(facts: facts, node: node) {
         Rejected {
           diagnostics: diagnostics_singleton(
             d: eval_diagnostic(reason: ^eval_rejected_grounding_node_mismatch, node: node)
           )
         }
-      } else if !canonical_grounding_admits_infer_facts(grounding: facts.grounding) {
+      } else if !inferred_facts_canonical_admitted(facts: facts) {
         Rejected {
           diagnostics: diagnostics_singleton(
             d: eval_diagnostic(reason: ^eval_rejected_canonical_mismatch, node: node)
@@ -1052,21 +1080,28 @@ fn eval_runtime_value_acceptance_witness(
   value: RuntimeValue
 ) -> RuntimeValueAcceptanceWitness {
   RuntimeValueAcceptanceWitness {
-    resolved_type: if inferred_facts_resolved_type(facts: facts) == runtime_value_resolved_type(value: value) {
-      Holds { value: runtime_value_resolved_type(value: value) }
-    } else {
-      Violates {
-        diagnostic: eval_diagnostic(reason: ^eval_rejected_resolved_type_mismatch, node: node)
-      }
+    resolved_type: match inferred_facts_resolved_type(facts: facts) {
+      Violates { diagnostic: _ } =>
+        Violates {
+          diagnostic: eval_diagnostic(reason: ^eval_rejected_grounding_not_derived, node: node)
+        }
+      Holds { value: declared } =>
+        if declared == runtime_value_resolved_type(value: value) {
+          Holds { value: runtime_value_resolved_type(value: value) }
+        } else {
+          Violates {
+            diagnostic: eval_diagnostic(reason: ^eval_rejected_resolved_type_mismatch, node: node)
+          }
+        }
     },
-    inhabitance: if canonical_grounding_admits_infer_facts(grounding: facts.grounding) {
+    inhabitance: if inferred_facts_canonical_admitted(facts: facts) {
       Holds { value: facts }
     } else {
       Violates {
         diagnostic: eval_diagnostic(reason: ^eval_rejected_inhabitance_mismatch, node: node)
       }
     },
-    canonical: if canonical_grounding_admits_infer_facts(grounding: facts.grounding) {
+    canonical: if inferred_facts_canonical_admitted(facts: facts) {
       Holds { value: facts }
     } else {
       Violates {

src/v2/compiler/06_translate.dag

@@ -38,6 +38,7 @@ import v2.std.coercion {
   CoercionCandidateSet,
   CoercionResult,
   coercion_candidate_set_from_declared_inhabitants,
+  coercion_identity_from_target_model,
   coercion_fold_with_declared_priority
 }
 import v2.std.diagnostic {
@@ -1245,28 +1246,31 @@ fn coerce_grounded_node(
   tree: InferredTree,
   target: TargetModel
 ) -> Outcome<CoercionResult> {
-  bind_outcome(
-    o: canonical_grounding_for_node(tree: tree, node: source),
-    f: fn(grounding) {
+  match coercion_identity_from_target_model(source: source, target: target) {
+    Accepted { value: identity, diagnostics: d } =>
+      Accepted { value: identity, diagnostics: d }
+    Rejected { diagnostics: _ } =>
       bind_outcome(
         o: target_selection_priority_from_model(target: target),
         f: fn(priority) {
           bind_outcome(
-            o: coercion_candidates_from_target_model(
-              target: target
-            ),
+            o: coercion_candidates_from_target_model(target: target),
             f: fn(candidates) {
-              coercion_fold_with_declared_priority(
-                source: grounding,
-                candidates: candidates,
-                priority: priority
+              bind_outcome(
+                o: canonical_grounding_for_node(tree: tree, node: source),
+                f: fn(grounding) {
+                  coercion_fold_with_declared_priority(
+                    source: grounding,
+                    candidates: candidates,
+                    priority: priority
+                  )
+                }
               )
             }
           )
         }
       )
-    }
-  )
+  }
 }
 fn translate_type_expression_shape_missing_diagnostic(node: Node) -> Diagnostic {
   Diagnostic {

src/v2/compiler/program_partition.dag

@@ -6,7 +6,8 @@ import v2.compiler.infer {
   InferredFactsEntry,
   InferredTree,
   admitted_inferred_facts_entry,
-  facts_map_from_entries
+  facts_map_from_entries,
+  inferred_facts_subject_node
 }
 import extdeps.communication.medium { Medium }
 import v2.compiler.translate {
@@ -389,7 +390,7 @@ fn partition_grounding_subject_in_segment(
 ) -> Bool {
   node_in_subtree_by_identity(
     root: segment_root,
-    needle: facts.grounding.node
+    needle: inferred_facts_subject_node(facts: facts)
   )
 }
 

src/v2/extdeps/languages/dag.dag

@@ -144,7 +144,7 @@ import v2.std.compilers.target_model {
   derive_bodied_arrow_scaffold}
 import v2.std.logic { Bool }
 import std.algebra { Cons, Empty }
-import v2.std.algebra { fold_list, for_all, is_empty, list_append, list_snoc_item }
+import v2.std.algebra { fold_list, for_all, is_empty, length, list_append, list_snoc_item }
 import v2.std.diagnostic {
   Accepted,
   Diagnostic,
@@ -4190,6 +4190,40 @@ fn dag_int_literal_magnitude_int_from_node(node: Node) -> Outcome<Int> {
   }
 }
 
+type DagCanonicalLiteral
+  = DagCanonicalBoolLiteral { value: Bool }
+  | DagCanonicalIntLiteral { magnitude: Int }
+
+fn dag_canonical_literal_shape_diagnostic(node: Node) -> Diagnostic {
+  Diagnostic {
+    reason: ^dag_literal_shape_invalid,
+    at: node_locus(node: node),
+    correction: None
+  }
+}
+
+data dag_canonical_literal_query_note: String = "dag_canonical_literal_from_node is the single typed query for inference-facing DAG literal shape. It preserves the Bool-vs-Int distinction and the decoded integer magnitude in a coproduct instead of publishing sibling is_* predicates over Node storage. Bool literals admit exactly the childless true/false atoms. Int literals admit exactly one named, decodable magnitude child. Every other shape is a typed refusal."
+
+fn dag_canonical_literal_from_node(node: Node) -> Outcome<DagCanonicalLiteral> {
+  if dag_node_is_kw_true_atom(node: node) && (length(xs: node.children) == 0) {
+    outcome_accepted(value: DagCanonicalBoolLiteral { value: true })
+  } else if dag_node_is_kw_false_atom(node: node) && (length(xs: node.children) == 0) {
+    outcome_accepted(value: DagCanonicalBoolLiteral { value: false })
+  } else if dag_node_is_int_literal_atom(node: node) && (length(xs: node.children) == 1) {
+    match dag_int_literal_magnitude_int_from_node(node: node) {
+      Accepted { value: magnitude, diagnostics: d } =>
+        Accepted {
+          value: DagCanonicalIntLiteral { magnitude: magnitude },
+          diagnostics: d
+        }
+      Rejected { diagnostics: _ } =>
+        outcome_rejected(dag_canonical_literal_shape_diagnostic(node: node))
+    }
+  } else {
+    outcome_rejected(dag_canonical_literal_shape_diagnostic(node: node))
+  }
+}
+
 fn dag_type_atom_node(identity: Symbol) -> Node {
   Node {
     kind: TypeNode { connective: Atom { identity: identity } },

src/v2/lens/common/infer_fixture.dag

@@ -1,6 +1,6 @@
 module v2.test.lens_common.infer_fixture
 
-import v2.compiler.infer { InferredFacts, InferredTree, infer_facts_lookup_miss_diagnostic }
+import v2.compiler.infer { DerivedGrounding, InferredFacts, InferredTree, infer_facts_lookup_miss_diagnostic }
 import v2.std.cardinality { RankingDimension, TerminationProof }
 import v2.std.collection { Map }
 import v2.std.constraints {
@@ -45,7 +45,7 @@ fn claim_inferred_facts_witness(
   descent: Witness<v2.std.cardinality.TerminationProof>
 ) -> InferredFacts {
   InferredFacts {
-    grounding: grounding,
+    grounding: DerivedGrounding { grounding: grounding },
     descent: descent
   }
 }

src/v2/lens/parallelism.dag

@@ -13,7 +13,7 @@ import v2.lens.common.algebraic_composition {
 }
 import std.disposition { SingleAuthority }
 
-import v2.compiler.infer { InferredFacts, InferredTree, inferred_facts_descent, infer_facts_lookup_miss_diagnostic }
+import v2.compiler.infer { InferredFacts, InferredTree, inferred_facts_descent, inferred_facts_subject_node, infer_facts_lookup_miss_diagnostic }
 import v2.std.algebra { bag_eq, list_snoc_item }
 import v2.std.collection {
   List,
@@ -76,7 +76,7 @@ fn parallelism_facts_for_source(tree: InferredTree, view: DependencyView) -> Wit
 fn parallelism_coupling_absent_diagnostic(facts: InferredFacts) -> Diagnostic {
   Diagnostic {
     reason: ^parallelism_reason_coupling_carrier_absent,
-    at: node_locus(node: facts.grounding.node),
+    at: node_locus(node: inferred_facts_subject_node(facts: facts)),
     correction: Unavailable { reason: AmbiguousIntent }
   }
 }

src/v2/std/coercion.dag

@@ -6,6 +6,7 @@ import v2.std.collection { List }
 import v2.std.constraints { CanonicalGrounding, CanonicalGroundingWitness }
 import v2.std.diagnostic {
   Accepted,
+  bind_outcome,
   Diagnostic,
   ExternalContractUnknown,
   None,
@@ -18,6 +19,11 @@ import v2.std.diagnostic {
   Unavailable,
   outcome_rejected
 }
+import v2.std.compilers.target_model {
+  TargetModel,
+  target_model_declared_inhabitants,
+  target_model_selection_priority
+}
 import v2.std.find_witness {
   CandidateSet,
   FindWitnessResult,
@@ -125,6 +131,79 @@ fn coercion_candidate_set_from_declared_inhabitants(
     )
   }
 }
+data identity_coercion_grounding_ruling: String = "Identity admission and semantic coercion are distinct judgments. coercion_identity_from_target_model accepts the TargetModel itself — never a caller-supplied CoercionCandidateSet — and reads its unique target_model_edge_declared_inhabitants and target_model_edge_selection_policy children inside this authority. Exact selection from that authored roster grounds CoercionQuality.Identity without claiming a resolved type for source. A candidate roster derived from source cannot enter this API; generic candidate sets remain available only to the semantic coercion path whose source is a compiler-derived CanonicalGrounding. This is the API-level wall between target-model membership and self-certification."
+
+fn coercion_homomorphism_evidence_for_node(
+  source: Node,
+  fw: FindWitnessResult,
+) -> Node {
+  Node {
+    kind: TypeNode { connective: Conj },
+    children: [
+      Edge { label: Named { name: ^coercion_homomorphism_evidence_source }, target: source },
+      Edge { label: Named { name: ^coercion_homomorphism_evidence_candidate }, target: fw.candidate },
+      Edge {
+        label: Named { name: ^coercion_homomorphism_evidence_find_witness },
+        target: fw.witness.evidence
+      }
+    ],
+    occurrence_id: SyntheticOccurrence
+  }
+}
+
+fn coercion_identity_from_target_model(
+  source: Node,
+  target: TargetModel,
+) -> Outcome<CoercionResult> {
+  bind_outcome(
+    o: target_model_declared_inhabitants(target: target),
+    f: fn(inhabitants_root) {
+      bind_outcome(
+        o: target_model_selection_priority(target: target),
+        f: fn(priority) {
+          bind_outcome(
+            o: coercion_candidate_set_from_declared_inhabitants(
+              inhabitants_root: inhabitants_root,
+              closedness_property: ^target_model_edge_declared_inhabitants
+            ),
+            f: fn(candidates) {
+              match find_witness(
+                source_facts: source,
+                candidates: candidates.set,
+                predicate: PreservationPredicate {
+                  algebra: source,
+                  preservation_rule: ^preservation_rule_exact_structural_equality_zip_fold
+                },
+                multiplicity_policy: TargetSelection {
+                  policy: TargetDeclaredPriority { priority: priority }
+                }
+              ) {
+                Accepted { value: fw, diagnostics: fw_d } =>
+                  Accepted {
+                    value: CoercionResult {
+                      target: fw.candidate,
+                      quality: Identity,
+                      witness: CoercionWitness {
+                        homomorphism: HomomorphismWitness {
+                          rule: ^homomorphism_rule_exact_structural_equality,
+                          evidence: coercion_homomorphism_evidence_for_node(
+                            source: source,
+                            fw: fw
+                          )
+                        }
+                      }
+                    },
+                    diagnostics: fw_d
+                  }
+                Rejected { diagnostics: r } => Rejected { diagnostics: r }
+              }
+            }
+          )
+        }
+      )
+    }
+  )
+}
 fn coercion_quality_for_witness(
   source: CanonicalGrounding,
   fw: FindWitnessResult,
@@ -224,15 +303,7 @@ fn coercion_homomorphism_evidence(
   source: CanonicalGrounding,
   fw: FindWitnessResult,
 ) -> Node {
-  Node {
-    kind: TypeNode { connective: Conj },
-    children: [
-      Edge { label: Named { name: ^coercion_homomorphism_evidence_source }, target: source.node },
-      Edge { label: Named { name: ^coercion_homomorphism_evidence_candidate }, target: fw.candidate },
-      Edge { label: Named { name: ^coercion_homomorphism_evidence_find_witness }, target: fw.witness.evidence }
-    ],
-    occurrence_id: SyntheticOccurrence
-}
+  coercion_homomorphism_evidence_for_node(source: source.node, fw: fw)
 }
 fn coercion_fold_exact_structural(
   source: CanonicalGrounding,