§5 determinism mechanism P1: core axis, roster, compose algebra, witnesses

DESIGN.md

@@ -78,7 +78,7 @@ hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/`
 
 ## Open threads
 
-- `v2.std.determinism` inert carrier — §5 determinism mechanism shape-sign draft (operator pending ratification on 2 FLAGs): [determinism mechanism design](docs/plans/determinism-mechanism-design.md)
+- `v2.std.determinism` — §5 determinism mechanism P1 landed (#5941; operator shape-signed, FLAG A/C locked): [determinism mechanism design](docs/plans/determinism-mechanism-design.md)
 - model §1's axioms (A1–A3) explicitly in `.dag` and have a lens **enforce the syllogism** — every claim a consequence-chain back to an axiom, no orphan and no cycle (the §4 acyclicity test turned on the argument itself; the §7 recursion, with this document as the first target). (operator's next project) → candidate articulation for review: [intent-linearity draft](docs/plans/intent-linearity-design-draft.md)
 - can a lens mechanically diagnose the *leaf-side* of decomposition (§2)? (operator-parked)
 - the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ{..} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ{prev:Int(k)} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20)

ROADMAP.md

@@ -103,6 +103,8 @@ A flaky or green-but-broken floor means no gate protects anything — so CI is u
 
 → [resolved-graph representation minimization](docs/plans/representation-minimization.md) — operator-funded root-first leanness after the #5867 InternTable fix (whole-tree resolve 14.2 to 5.5 GiB): emitter-determinism gate, stream/evict (Lever C — converges with resolve-incrementality above), variant-Node minimal representation, func_env.sigs single-authority. Gated on the root-vs-doomed-seed discriminator (v1 is going away).
 
+→ [§5 determinism mechanism](docs/plans/determinism-mechanism-design.md) — signature-derived DeterminismClass axis orthogonal to EffectShape; P1 primitive roster + compose algebra (#5941); bundles into #3468 InferredFacts at P4.
+
 **What's on `.dag` today (the gap map — detail in the charter §2/§4):**
 
 - [x] **execution = a dependency-graph walk** — `claim_executor` interprets `ci_floor_plan.dag`; one fold, batches from dependency edges (the realest layer)

docs/plans/determinism-mechanism-design.md

@@ -1,7 +1,8 @@
 # Determinism mechanism — design proposal (§5)
 
-> **Status: DESIGN-ONLY — awaiting operator shape-sign.** No `std/` or `lens/` authoring until signed.
-> Lane: `v2.std.determinism` inert-carrier activation (keen-bat-281).
+> **Status: OPERATOR SHAPE-SIGNED — P1 landed in #5941 (sunny-wolf-582).** Supersedes #5937 (keen-bat-281) design-for-sign draft; signed status + FLAG locks authoritative here.
+> **FLAG 1 = A** (bundle determinism into #3468 `InferredFacts` block); **FLAG 2 = C** (refinement + emit + determinism horizontal).
+> Lane: `v2.std.determinism` inert-carrier activation (keen-bat-281 → sunny-wolf-582 P1).
 > DESIGN refs: §2 (horizontal — one perturbation/determinism kernel, many readings; deep — ground `NonDetSource` atoms), §3 (single authority vs `behavioral.determinism`, `perturbation`, `emit_determinism_gate`), §5 (construction over validation; decidability trichotomy), §6 (inert carrier → wired consumer; priced in displaced cost), §7 (signature-derived classification dissolves the lens).
 >
 > Every unresolved item is either a **decided-with-rationale** entry (§8) or one of **two genuine operator FLAGS**.
@@ -352,9 +353,7 @@ Existing witness: unordered classifier → `^naming_the_leak`. Add horizontal li
 ### Genuine operator FLAGS (2 only)
 
 **FLAG 1 — `InferredFacts` seam architecture (#3468 bundle).**
-- **Decision:** bundle determinism with the #3468 signature-derived facts block (effect + ownership + determinism) vs a separate `determinism_facts` side-map.
-- **Options:** (A) one bundled extension on `InferredFacts`; (B) parallel side-map keyed by signature.
-- **Recommendation: A** — one signature-derived authority block; avoids three parallel per-edge ratchets. *This is a shared-seam architecture call the analysis cannot close without operator judgment on #3468 sequencing.*
+- **Decision (OPERATOR-LOCKED): A** — bundle determinism with the #3468 signature-derived facts block (effect + ownership + determinism); not a parallel side-map.
 
 **FLAG 2 — Refinement / emit / determinism horizontal (ordered container construction).**
 - **Decision:** how three subsystems jointly guarantee ordered map iteration on output-affecting paths.
@@ -373,4 +372,4 @@ Delete or fold this doc when:
 4. `emit_determinism_gate` failures surface the first located `NonDetSource` on the emit chain;
 5. `DeterminismAxis` is the single core; `OperationDeterminism` projects from `DeterminismFact` without re-declaring `Deterministic | NonDeterministic`.
 
-Until operator shape-sign on §4–§6, **no `std/` or `lens/` edits** — this document is the sole artifact.
+P1 substrate authoring (`dsl/std/determinism.dag`, `v2.std.determinism` roster/compose/witnesses, `determinism_contract_test.dag`) proceeds under this signed shape; lens wiring remains P2+.

dsl/gunbc/design_document.dag

@@ -138,7 +138,7 @@ fn open_threads_blocks() -> List<MarkdownBlock> {
   [
     h2(text: "Open threads"),
     ul(items: [
-      li(text: "`v2.std.determinism` inert carrier — §5 determinism mechanism shape-sign draft (operator pending ratification on 2 FLAGs): [determinism mechanism design](docs/plans/determinism-mechanism-design.md)"),
+      li(text: "`v2.std.determinism` — §5 determinism mechanism P1 landed (#5941; operator shape-signed, FLAG A/C locked): [determinism mechanism design](docs/plans/determinism-mechanism-design.md)"),
       li(text: "model §1's axioms (A1–A3) explicitly in `.dag` and have a lens **enforce the syllogism** — every claim a consequence-chain back to an axiom, no orphan and no cycle (the §4 acyclicity test turned on the argument itself; the §7 recursion, with this document as the first target). (operator's next project) → candidate articulation for review: [intent-linearity draft](docs/plans/intent-linearity-design-draft.md)"),
       li(text: "can a lens mechanically diagnose the *leaf-side* of decomposition (§2)? (operator-parked)"),
       li(text: "the model↔realization fork is systemic, and where unfinished it fails open: every primitive is modeled as a coproduct and realized as a native `Value`, reconciled by per-site bridges, so coverage is accidental and non-compositional. `match` bridges `Int→Zero/Succ` but `Value::eq` has no `Int↔Variant` arm, so `nat_add(85, 32) == 117` silently compared `false` at its `_ => false` chokepoint — a §5 fail-open, not the §2/§7 redundancy the 🟡 dissolve-on markers track. **Landed:** the *numeric tower* fork now fails closed — `eval_binop`'s `BinOp::Eq`/`Ne` raises `InterpError::CrossRepresentationEquality` when a `false` result is *explained* by a native `Int`/`Float` vs `Nat`-coproduct straddle (recursive: catches `nat_add == nat_add` and `[nat_add(1,1)] == [2]`), with `Value::eq` left infallible so it stays the single `CanonKey` map-key authority. The discriminating witness is `cross_representation_equality_test` (forks → typed error; reconciled/native → `true`; genuine diffs `1 == 2`/`Succ\{..\} == Zero` → `false`, not error). **Remaining:** (a) the same straddle for `Bool True|False` over `Value::Bool` (no `==` site in the corpus today) and `Optional/Witness` over `Value::Null` — the latter resists a blanket guard because `Value::Null` is the overloaded `None`/`Absent`/miss sentinel and `present == None` (131 sites) is a *legitimate* `false`, so it needs grounding, not an error arm; (b) the root fix (§1/§2/§7) — ground each primitive into its realization. **Numeric tower: GROUNDED** (#5428, 2026-06-21) — Nat construction-side grounded (`Zero → Int(0)`, `Succ\{prev:Int(k)\} → Int(k+1)`); native form == modeled form; `eval_binop` `CrossRepresentationEquality` guard is dead-in-corpus for numerics, kept as fail-closed backstop until the `Value::Null` split lands (guard removal bundled with that work, fenced out of this window). **Remaining:** `Value::Null` split — Optional/Witness/miss into own carriers (~131 sites; the deeper root, its own runway). (operator: `==` fail-closed, 2026-06-20)"),

dsl/gunbc/roadmap_authority.dag

@@ -160,6 +160,7 @@ fn section_1() -> RoadmapSection {
       ),
       section_prose(content: "**The <1min lever is resolve-phase incrementality, NOT cross-run resolve-cache** — CI is cold-dominated (the exe-hash re-colds on every code change), so §2 P3 resolve-cache is the *warm* ~18% lever and was measured net-negative as the cold-CI path. Incrementality (don't resolve what didn't change) is upstream of caching (memoize what repeats); the <1min target rides the former. **This re-frames the §2 \"core ask\" — operator review.**"),
       section_prose(content: "→ [resolved-graph representation minimization](docs/plans/representation-minimization.md) — operator-funded root-first leanness after the #5867 InternTable fix (whole-tree resolve 14.2 to 5.5 GiB): emitter-determinism gate, stream/evict (Lever C — converges with resolve-incrementality above), variant-Node minimal representation, func_env.sigs single-authority. Gated on the root-vs-doomed-seed discriminator (v1 is going away)."),
+      section_prose(content: "→ [§5 determinism mechanism](docs/plans/determinism-mechanism-design.md) — signature-derived DeterminismClass axis orthogonal to EffectShape; P1 primitive roster + compose algebra (#5941); bundles into #3468 InferredFacts at P4."),
       section_group(
         label: "What's on `.dag` today (the gap map — detail in the charter §2/§4)",
         nodes: [

dsl/std/determinism.dag

@@ -0,0 +1,5 @@
+module std.determinism
+
+type DeterminismAxis
+  = Deterministic
+  | NonDeterministic

src/v1/stage0/src/non_fold_residue_project.rs

@@ -126,6 +126,8 @@ const NON_FOLD_RESIDUE_ROSTER: &[&str] = &[
     "src/v2/std/compilers/target_model.dag::target_type_expr_emitted_validate_wire_shape",
     "src/v2/std/compilers/target_model.dag::target_use_site_ownership_catalog_lookup_step",
     "src/v2/std/effects.dag::key_source_eq",
+    "src/v2/std/determinism.dag::determinism_class_eq",
+    "src/v2/std/determinism.dag::non_det_source_eq",
     "src/v2/std/float.dag::float_body_is_nan",
     "src/v2/std/probe_selector.dag::diagnostic_interface_kind_eq",
     "src/v2/std/qualified_name.dag::qn_fold_step",

src/v2/std/determinism.dag

@@ -1,5 +1,7 @@
 module v2.std.determinism
 
+import v2.std.collection { Optional, Absent, Present, optional_present }
+import v2.std.logic { Bool }
 import v2.std.node { Symbol }
 
 type NonDetSource
@@ -16,3 +18,148 @@ type DeterminismFact {
   signature: Symbol,
   classification: DeterminismClass
 }
+
+data determinism_primitive_roster_dissolution_marker: String = "Base-primitive ground-fact KERNEL for determinism_primitive_lookup (closed Symbol roster: irreducible NonDetSource atoms plus #5913 construction-instance rows). Dissolves when composite determinism is DERIVED via determinism_compose wired into #3468 InferredFacts at infer (P4/FLAG-A bundle); this hand-roster shrinks to base-primitive ground facts only — not a permanent side-map (FLAG A rejected)."
+
+fn non_det_source_eq(a: NonDetSource, b: NonDetSource) -> Bool {
+  match a {
+    HashIteration => match b {
+      HashIteration => true
+      _ => false
+    }
+    TimeRead => match b {
+      TimeRead => true
+      _ => false
+    }
+    RandomRead => match b {
+      RandomRead => true
+      _ => false
+    }
+    EnvRead => match b {
+      EnvRead => true
+      _ => false
+    }
+  }
+}
+
+fn determinism_class_eq(a: DeterminismClass, b: DeterminismClass) -> Bool {
+  match a {
+    Deterministic => match b {
+      Deterministic => true
+      _ => false
+    }
+    NonDeterministic { source: sa } => match b {
+      NonDeterministic { source: sb } => non_det_source_eq(a: sa, b: sb)
+      _ => false
+    }
+  }
+}
+
+fn determinism_primitive_lookup(sig: Symbol) -> Optional<DeterminismClass> {
+  if sig == ^pure_add {
+    optional_present(value: Deterministic)
+  } else if sig == ^sorted_export_set_map_keys {
+    optional_present(value: Deterministic)
+  } else if sig == ^unique_imported_variant_owner {
+    optional_present(value: Deterministic)
+  } else if sig == ^alpha_sorted_variant_fold {
+    optional_present(value: Deterministic)
+  } else if sig == ^find_struct_name_by_fields_disambiguation {
+    optional_present(value: Deterministic)
+  } else if sig == ^hash_map_keys_iter {
+    optional_present(value: NonDeterministic { source: HashIteration })
+  } else if sig == ^unordered_hash_map_iteration {
+    optional_present(value: NonDeterministic { source: HashIteration })
+  } else if sig == ^host_clock_now {
+    optional_present(value: NonDeterministic { source: TimeRead })
+  } else if sig == ^host_random_read {
+    optional_present(value: NonDeterministic { source: RandomRead })
+  } else if sig == ^host_env_var_read {
+    optional_present(value: NonDeterministic { source: EnvRead })
+  } else {
+    Absent
+  }
+}
+
+fn determinism_primitive_in_roster(sig: Symbol) -> Bool {
+  match determinism_primitive_lookup(sig: sig) {
+    Present { value: _ } => true
+    Absent => false
+  }
+}
+
+fn determinism_compose(outer: DeterminismClass, inner: DeterminismClass) -> DeterminismClass {
+  match outer {
+    NonDeterministic { source: source } => NonDeterministic { source: source }
+    Deterministic => inner
+  }
+}
+
+fn determinism_fact_for_signature(sig: Symbol) -> Optional<DeterminismFact> {
+  match determinism_primitive_lookup(sig: sig) {
+    Present { value: classification } =>
+      optional_present(
+        value: DeterminismFact {
+          signature: sig,
+          classification: classification
+        }
+      )
+    Absent => Absent
+  }
+}
+
+data witness_pure_add_is_deterministic: Bool = match determinism_primitive_lookup(sig: ^pure_add) {
+  Present { value: classification } =>
+    determinism_class_eq(a: classification, b: Deterministic)
+  Absent => false
+}
+
+data witness_hash_map_keys_iter_is_hash_iteration_leak: Bool = match determinism_primitive_lookup(
+  sig: ^hash_map_keys_iter
+) {
+  Present { value: classification } =>
+    determinism_class_eq(
+      a: classification,
+      b: NonDeterministic { source: HashIteration }
+    )
+  Absent => false
+}
+
+data witness_unknown_primitive_absent_from_roster: Bool = match determinism_primitive_lookup(
+  sig: ^unknown_determinism_roster_probe
+) {
+  Absent => true
+  Present { value: _ } => false
+}
+
+data witness_deterministic_compose_is_deterministic: Bool = determinism_class_eq(
+  a: determinism_compose(
+    outer: Deterministic,
+    inner: Deterministic
+  ),
+  b: Deterministic
+)
+
+data witness_nondeterministic_compose_propagates_left: Bool = determinism_class_eq(
+  a: determinism_compose(
+    outer: NonDeterministic { source: HashIteration },
+    inner: Deterministic
+  ),
+  b: NonDeterministic { source: HashIteration }
+)
+
+data witness_nondeterministic_compose_propagates_right: Bool = determinism_class_eq(
+  a: determinism_compose(
+    outer: Deterministic,
+    inner: NonDeterministic { source: TimeRead }
+  ),
+  b: NonDeterministic { source: TimeRead }
+)
+
+data witness_sorted_export_set_map_keys_is_deterministic: Bool = match determinism_primitive_lookup(
+  sig: ^sorted_export_set_map_keys
+) {
+  Present { value: classification } =>
+    determinism_class_eq(a: classification, b: Deterministic)
+  Absent => false
+}

src/v2/test/claim/determinism_contract_test.dag

@@ -0,0 +1,87 @@
+module v2.test.claim.determinism_contract_test
+
+import v2.std.collection { Absent, Present }
+import v2.std.determinism {
+  Deterministic,
+  HashIteration,
+  NonDeterministic,
+  TimeRead,
+  determinism_class_eq,
+  determinism_compose,
+  determinism_fact_for_signature,
+  determinism_primitive_in_roster,
+  determinism_primitive_lookup,
+  witness_deterministic_compose_is_deterministic,
+  witness_hash_map_keys_iter_is_hash_iteration_leak,
+  witness_nondeterministic_compose_propagates_left,
+  witness_nondeterministic_compose_propagates_right,
+  witness_pure_add_is_deterministic,
+  witness_sorted_export_set_map_keys_is_deterministic,
+  witness_unknown_primitive_absent_from_roster
+}
+import v2.std.logic { Bool }
+
+fn rostered_classification_eq(sig: Symbol, expected: DeterminismClass) -> Bool {
+  match determinism_primitive_lookup(sig: sig) {
+    Present { value: classification } =>
+      determinism_class_eq(a: classification, b: expected)
+    Absent => false
+  }
+}
+
+test fn determinism_pure_add_is_deterministic_holds() -> Bool {
+  witness_pure_add_is_deterministic
+    && rostered_classification_eq(sig: ^pure_add, expected: Deterministic)
+}
+
+test fn determinism_hash_map_keys_iter_is_hash_iteration_leak_holds() -> Bool {
+  witness_hash_map_keys_iter_is_hash_iteration_leak
+    && rostered_classification_eq(
+      sig: ^hash_map_keys_iter,
+      expected: NonDeterministic { source: HashIteration }
+    )
+}
+
+test fn determinism_unknown_primitive_absent_from_roster_holds() -> Bool {
+  witness_unknown_primitive_absent_from_roster
+}
+
+test fn determinism_compose_algebra_holds() -> Bool {
+  witness_deterministic_compose_is_deterministic
+    && witness_nondeterministic_compose_propagates_left
+    && witness_nondeterministic_compose_propagates_right
+    && determinism_class_eq(
+      a: determinism_compose(
+        outer: NonDeterministic { source: TimeRead },
+        inner: NonDeterministic { source: HashIteration }
+      ),
+      b: NonDeterministic { source: TimeRead }
+    )
+}
+
+test fn determinism_roster_5913_construction_rows_are_deterministic_holds() -> Bool {
+  witness_sorted_export_set_map_keys_is_deterministic
+    && determinism_primitive_in_roster(sig: ^unique_imported_variant_owner)
+    && determinism_primitive_in_roster(sig: ^alpha_sorted_variant_fold)
+    && determinism_primitive_in_roster(sig: ^find_struct_name_by_fields_disambiguation)
+    && rostered_classification_eq(
+      sig: ^unique_imported_variant_owner,
+      expected: Deterministic
+    )
+}
+
+test fn determinism_fact_for_signature_holds() -> Bool {
+  match determinism_fact_for_signature(sig: ^pure_add) {
+    Present { value: fact } =>
+      fact.signature == ^pure_add
+        && determinism_class_eq(a: fact.classification, b: Deterministic)
+    Absent => false
+  }
+}
+
+test fn determinism_fact_for_unknown_signature_is_absent_holds() -> Bool {
+  match determinism_fact_for_signature(sig: ^unknown_determinism_roster_probe) {
+    Absent => true
+    Present { value: _ } => false
+  }
+}