Phase C.1: v2.lens.determinism — grounded map_keys root, emergent boundary-relative determinism lens + live contract

src/v2/lens/determinism.dag

@@ -0,0 +1,111 @@
+module v2.lens.determinism
+
+import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
+import std.disposition { SingleAuthority }
+import std.decl_ref { DeclarationRef, WholeDeclaration }
+import std.determinism { DeterminismAxis, Deterministic, NonDeterministic, determinism_compose }
+import v2.std.determinism { DeterminismFact }
+import v2.std.collection { Absent, List, Optional, Present, list_at_optional, optional_absent, optional_present }
+import v2.std.diagnostic { Diagnostic, ExternalContractUnknown, Unavailable, node_locus }
+import v2.std.logic { Bool }
+import v2.std.node { Atom, Edge, Node, NodeFold, Symbol, TypeNode, fold_node }
+import v2.std.node_query { node_is_call, node_positional_child_targets }
+import v2.std.witness { Holds, Violates, Witness }
+
+type DeterminismRoot {
+  signature: Symbol,
+  source: DeclarationRef,
+  citation: String
+}
+
+fn map_keys_leak_source() -> DeclarationRef {
+  DeclarationRef {
+    module_path: "v1.runtime_rust",
+    decl_name: "map_keys",
+    field: WholeDeclaration
+  }
+}
+
+data determinism_root_map_keys: DeterminismRoot = DeterminismRoot {
+  signature: ^map_keys,
+  source: map_keys_leak_source(),
+  citation: "map_keys iterates hash-ordered keys (src/v1/runtime_rust.dag:176), a host-nondeterministic root; sorted_map_keys is its deterministic sibling. Grounds the single NonDeterministic leaf; unregistered callees contribute Deterministic at the within-function boundary (map_keys is always a readable atom, never missed). Extend with clock/entropy roots when Phase B grounds kind:Observation."
+}
+
+data determinism_root_registry: List<DeterminismRoot> = [
+  determinism_root_map_keys
+]
+
+fn determinism_root_for_symbol(registry: List<DeterminismRoot>, s: Symbol) -> Optional<DeterminismRoot> {
+  fold(registry, init: optional_absent(), f: fn(acc, row) {
+    match acc {
+      Present { value: _ } => acc
+      Absent => if row.signature == s { optional_present(value: row) } else { optional_absent() }
+    }
+  })
+}
+
+fn node_callee_symbol(n: Node) -> Optional<Symbol> {
+  if node_is_call(node: n) {
+    match list_at_optional(xs: node_positional_child_targets(node: n), index: 0) {
+      Present { value: callee } => match callee.kind {
+        TypeNode { connective: Atom { identity: sym } } => optional_present(value: sym)
+        _ => optional_absent()
+      }
+      Absent => optional_absent()
+    }
+  } else {
+    optional_absent()
+  }
+}
+
+fn local_determinism_axis(n: Node) -> DeterminismAxis {
+  match node_callee_symbol(n: n) {
+    Present { value: sym } => match determinism_root_for_symbol(registry: determinism_root_registry, s: sym) {
+      Present { value: root } => NonDeterministic { source: root.source }
+      Absent => Deterministic
+    }
+    Absent => Deterministic
+  }
+}
+
+fn determinism_axis_fold_step(acc: DeterminismAxis, _: Edge, child: DeterminismAxis) -> DeterminismAxis {
+  determinism_compose(outer: acc, inner: child)
+}
+
+fn determinism_axis_for_node(n: Node) -> DeterminismAxis {
+  fold_node(
+    n: n,
+    algebra: NodeFold {
+      init: fn(n0) { local_determinism_axis(n: n0) },
+      step: fn(acc, e, child) { determinism_axis_fold_step(acc: acc, e: e, child: child) }
+    }
+  )
+}
+
+fn determinism_fact_for_node(signature: Symbol, n: Node) -> DeterminismFact {
+  DeterminismFact {
+    signature: signature,
+    classification: determinism_axis_for_node(n: n)
+  }
+}
+
+fn determinism_leak_diagnostic(n: Node) -> Diagnostic {
+  Diagnostic {
+    reason: ^determinism_nondeterministic_root_reach,
+    at: node_locus(node: n),
+    correction: Unavailable { reason: ExternalContractUnknown }
+  }
+}
+
+fn determinism_contract_witness(signature: Symbol, n: Node) -> Witness<DeterminismFact> {
+  let fact = determinism_fact_for_node(signature: signature, n: n)
+  match fact.classification {
+    NonDeterministic { source: _ } => Violates { diagnostic: determinism_leak_diagnostic(n: n) }
+    Deterministic => Holds { value: fact }
+  }
+}
+
+data construction_justification: ConstructionJustification = ConstructionJustification {
+  class: WallAfterGrounding { dissolves_to: SingleAuthority }
+}

src/v2/lens/determinism/reach_witness_test.dag

@@ -0,0 +1,98 @@
+module v2.test.lens_determinism.reach_witness
+
+import v2.lens.determinism { determinism_axis_for_node, determinism_contract_witness }
+import std.determinism { DeterminismAxis, Deterministic, NonDeterministic }
+import v2.std.determinism { DeterminismFact }
+import v2.std.node {
+  Atom,
+  ComputationNode,
+  Edge,
+  Node,
+  Positional,
+  Symbol,
+  SyntheticOccurrence,
+  Transform,
+  TypeNode
+}
+import v2.std.witness { Holds, Violates, Witness }
+import v2.std.logic { Bool }
+import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
+
+data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
+
+fn det_atom(id: Symbol) -> Node {
+  Node {
+    kind: TypeNode { connective: Atom { identity: id } },
+    children: [],
+    occurrence_id: SyntheticOccurrence
+  }
+}
+
+fn det_positional(target: Node) -> Edge {
+  Edge { label: Positional, target: target }
+}
+
+fn det_call(callee: Symbol, arg: Node) -> Node {
+  Node {
+    kind: ComputationNode { behavior: Transform },
+    children: [det_positional(target: det_atom(id: callee)), det_positional(target: arg)],
+    occurrence_id: SyntheticOccurrence
+  }
+}
+
+fn map_keys_call_fixture() -> Node {
+  det_call(callee: ^map_keys, arg: det_atom(id: ^emit_export_map))
+}
+
+fn sorted_map_keys_call_fixture() -> Node {
+  det_call(callee: ^sorted_map_keys, arg: det_atom(id: ^emit_export_map))
+}
+
+fn clean_call_fixture() -> Node {
+  det_call(callee: ^emit_concat, arg: det_atom(id: ^emit_export_map))
+}
+
+fn nested_map_keys_fixture() -> Node {
+  det_call(callee: ^emit_concat, arg: map_keys_call_fixture())
+}
+
+fn witness_violates(w: Witness<DeterminismFact>) -> Bool {
+  match w {
+    Violates { diagnostic: _ } => true
+    Holds { value: _ } => false
+  }
+}
+
+fn witness_holds(w: Witness<DeterminismFact>) -> Bool {
+  match w {
+    Holds { value: _ } => true
+    Violates { diagnostic: _ } => false
+  }
+}
+
+fn axis_is_nondeterministic(a: DeterminismAxis) -> Bool {
+  match a {
+    NonDeterministic { source: _ } => true
+    Deterministic => false
+  }
+}
+
+test fn determinism_flags_map_keys_reach() -> Bool {
+  witness_violates(w: determinism_contract_witness(signature: ^emit_fixture, n: map_keys_call_fixture()))
+}
+
+test fn determinism_holds_sorted_map_keys_sibling() -> Bool {
+  witness_holds(w: determinism_contract_witness(signature: ^emit_fixture, n: sorted_map_keys_call_fixture()))
+}
+
+test fn determinism_holds_clean_call() -> Bool {
+  witness_holds(w: determinism_contract_witness(signature: ^emit_fixture, n: clean_call_fixture()))
+}
+
+test fn determinism_flags_nested_map_keys_in_subtree() -> Bool {
+  witness_violates(w: determinism_contract_witness(signature: ^emit_fixture, n: nested_map_keys_fixture()))
+}
+
+test fn determinism_axis_map_keys_is_nondeterministic() -> Bool {
+  axis_is_nondeterministic(a: determinism_axis_for_node(n: map_keys_call_fixture()))
+}

src/v2/lens/registry.dag

@@ -7,7 +7,7 @@ import v2.std.collection { List }
 import v2.std.node { Symbol }
 import v2.std.text { String }
 
-type LensIdV0 = Complexity | Cost | Parallelism | EffectEnumeration | Idempotency | Provenance | UnusedParameters | StructuralResolution | TableDecisionTree
+type LensIdV0 = Complexity | Cost | Parallelism | EffectEnumeration | Idempotency | Provenance | UnusedParameters | StructuralResolution | TableDecisionTree | Determinism
 
 type LensModulePathV0 = Bound { path: String } | Unbound
 
@@ -74,6 +74,11 @@ data lens_registry_v0_table_decision_tree: LensRegistryEntryV0 = {
   module_path: Bound { path: "v2.lens.table_decision_tree" }
 }
 
+data lens_registry_v0_determinism: LensRegistryEntryV0 = {
+  lens_id: Determinism
+  module_path: Bound { path: "v2.lens.determinism" }
+}
+
 data lens_registry_v0: List<LensRegistryEntryV0> = [
   lens_registry_v0_complexity,
   lens_registry_v0_cost,
@@ -83,7 +88,8 @@ data lens_registry_v0: List<LensRegistryEntryV0> = [
   lens_registry_v0_provenance,
   lens_registry_v0_unused_parameters,
   lens_registry_v0_structural_resolution,
-  lens_registry_v0_table_decision_tree
+  lens_registry_v0_table_decision_tree,
+  lens_registry_v0_determinism
 ]
 
 fn lens_id_v0_eq(left: LensIdV0, right: LensIdV0) -> Bool {
@@ -124,6 +130,10 @@ fn lens_id_v0_eq(left: LensIdV0, right: LensIdV0) -> Bool {
       TableDecisionTree => true
       _ => false
     }
+    Determinism => match right {
+      Determinism => true
+      _ => false
+    }
   }
 }
 

src/v2/lens/registry/sg_claims_test.dag

@@ -3,6 +3,7 @@ module v2.test.lens_registry.sg_claims
 import v2.lens.registry {
   Complexity,
   Cost,
+  Determinism,
   EffectEnumeration,
   Idempotency,
   LensIdV0,
@@ -36,7 +37,8 @@ data lens_registry_v0_required_ids: List<LensIdV0> = [
   Provenance,
   UnusedParameters,
   StructuralResolution,
-  TableDecisionTree
+  TableDecisionTree,
+  Determinism
 ]
 
 test fn lens_registry_required_ids_resolve_holds() -> Bool {