From bfd97ca0f061f181a5da96340d76d246e47e4926 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 14 Jul 2026 00:30:21 +0000 Subject: [PATCH 1/9] WIP: emit determinism --- dag/std/determinism.dag | 36 ++++++++- src/v2/std/determinism.dag | 158 ++----------------------------------- 2 files changed, 40 insertions(+), 154 deletions(-) diff --git a/dag/std/determinism.dag b/dag/std/determinism.dag index dda0a3764bf..548497799c8 100644 --- a/dag/std/determinism.dag +++ b/dag/std/determinism.dag @@ -1,5 +1,37 @@ module std.determinism -type DeterminismAxis +import std.types { Bool } +import std.perturbation { PerturbationVerdict, ResponseConsistent, ResponseViolation } +import std.decl_ref { DeclarationRef } + +type Determinism = Deterministic - | NonDeterministic + | NonDeterministic { source: DeclarationRef } + +fn determinism_from_perturbation(verdict: PerturbationVerdict, reached: DeclarationRef) -> Determinism { + match verdict { + ResponseConsistent => Deterministic + ResponseViolation => NonDeterministic { source: reached } + } +} + +fn determinism_compose(outer: Determinism, inner: Determinism) -> Determinism { + match outer { + NonDeterministic { source: s } => NonDeterministic { source: s } + Deterministic => inner + } +} + +fn determinism_is_deterministic(c: Determinism) -> Bool { + match c { + Deterministic => true + NonDeterministic { source: _ } => false + } +} + +fn determinism_reached(c: Determinism) -> DeclarationRef? { + match c { + Deterministic => Absent + NonDeterministic { source: s } => Present { value: s } + } +} diff --git a/src/v2/std/determinism.dag b/src/v2/std/determinism.dag index 36171b5016d..eb207bbe060 100644 --- a/src/v2/std/determinism.dag +++ b/src/v2/std/determinism.dag @@ -1,163 +1,17 @@ module v2.std.determinism -import v2.std.collection { Optional, Absent, Present, optional_present } -import v2.std.logic { Bool } +import std.determinism { Determinism, Deterministic, NonDeterministic } import v2.std.node { Symbol } -type NonDetSource - = HashIteration - | TimeRead - | RandomRead - | EnvRead - -type DeterminismClass - = Deterministic - | NonDeterministic { source: NonDetSource } - type DeterminismFact { signature: Symbol, - classification: DeterminismClass -} - -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 - } - } + classification: Determinism } -fn determinism_primitive_lookup(sig: Symbol) -> Optional { - 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_fact_classification(fact: DeterminismFact) -> Determinism { + fact.classification } -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 { - 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 +fn determinism_fact_signature(fact: DeterminismFact) -> Symbol { + fact.signature } From 39edba2053be9e2c1917b67dadc5cc093945cfb4 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 14 Jul 2026 00:40:44 +0000 Subject: [PATCH 2/9] WIP: emit determinism --- dag/std/determinism.dag | 15 --- src/v2/std/determinism.dag | 8 ++ .../test/claim/determinism_contract_test.dag | 110 ++++++++---------- 3 files changed, 54 insertions(+), 79 deletions(-) diff --git a/dag/std/determinism.dag b/dag/std/determinism.dag index 548497799c8..1a51881ff14 100644 --- a/dag/std/determinism.dag +++ b/dag/std/determinism.dag @@ -1,6 +1,5 @@ module std.determinism -import std.types { Bool } import std.perturbation { PerturbationVerdict, ResponseConsistent, ResponseViolation } import std.decl_ref { DeclarationRef } @@ -21,17 +20,3 @@ fn determinism_compose(outer: Determinism, inner: Determinism) -> Determinism { Deterministic => inner } } - -fn determinism_is_deterministic(c: Determinism) -> Bool { - match c { - Deterministic => true - NonDeterministic { source: _ } => false - } -} - -fn determinism_reached(c: Determinism) -> DeclarationRef? { - match c { - Deterministic => Absent - NonDeterministic { source: s } => Present { value: s } - } -} diff --git a/src/v2/std/determinism.dag b/src/v2/std/determinism.dag index eb207bbe060..ed0f33da49e 100644 --- a/src/v2/std/determinism.dag +++ b/src/v2/std/determinism.dag @@ -1,6 +1,7 @@ module v2.std.determinism import std.determinism { Determinism, Deterministic, NonDeterministic } +import v2.std.logic { Bool } import v2.std.node { Symbol } type DeterminismFact { @@ -15,3 +16,10 @@ fn determinism_fact_classification(fact: DeterminismFact) -> Determinism { fn determinism_fact_signature(fact: DeterminismFact) -> Symbol { fact.signature } + +fn determinism_is_deterministic(c: Determinism) -> Bool { + match c { + Deterministic => true + NonDeterministic { source: _ } => false + } +} diff --git a/src/v2/test/claim/determinism_contract_test.dag b/src/v2/test/claim/determinism_contract_test.dag index f740f440cdc..d19c0078110 100644 --- a/src/v2/test/claim/determinism_contract_test.dag +++ b/src/v2/test/claim/determinism_contract_test.dag @@ -1,92 +1,74 @@ module v2.test.claim.determinism_contract_test -import v2.std.collection { Absent, Present } -import v2.std.determinism { - DeterminismClass, +import std.decl_ref { DeclarationRef, WholeDeclaration } +import 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 + determinism_from_perturbation +} +import std.perturbation { ResponseConsistent, ResponseViolation } +import v2.std.determinism { + DeterminismFact, + determinism_fact_classification, + determinism_fact_signature, + determinism_is_deterministic } -import v2.std.logic { Bool } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.logic { Bool } import v2.std.node { Symbol } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly -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 +fn example_root() -> DeclarationRef { + DeclarationRef { + module_path: "std.resources", + decl_name: "Clock", + field: WholeDeclaration } } -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_perturbation_consistent_is_deterministic() -> Bool { + determinism_is_deterministic( + c: determinism_from_perturbation(verdict: ResponseConsistent, reached: example_root()) + ) } -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_perturbation_violation_is_nondeterministic() -> Bool { + !determinism_is_deterministic( + c: determinism_from_perturbation(verdict: ResponseViolation, reached: example_root()) + ) } -test fn determinism_unknown_primitive_absent_from_roster_holds() -> Bool { - witness_unknown_primitive_absent_from_roster +test fn determinism_compose_det_det_is_deterministic() -> Bool { + determinism_is_deterministic( + c: determinism_compose(outer: Deterministic, inner: Deterministic) + ) } -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_compose_nondet_left_propagates() -> Bool { + !determinism_is_deterministic( + c: determinism_compose( + outer: NonDeterministic { source: example_root() }, + inner: Deterministic ) + ) } -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_compose_nondet_right_propagates() -> Bool { + !determinism_is_deterministic( + c: determinism_compose( + outer: Deterministic, + inner: NonDeterministic { source: example_root() } ) + ) } -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 +test fn determinism_fact_binds_signature_and_classification() -> Bool { + let fact = DeterminismFact { + signature: ^emit_export_set, + classification: Deterministic } + determinism_is_deterministic(c: determinism_fact_classification(fact: fact)) + && (determinism_fact_signature(fact: fact) == ^emit_export_set) } From f7b710197860b9baf5067fc8239a1b9aabc03b1c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 14 Jul 2026 00:51:17 +0000 Subject: [PATCH 3/9] WIP: emit determinism --- dag/std/determinism.dag | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dag/std/determinism.dag b/dag/std/determinism.dag index 1a51881ff14..a03103a550c 100644 --- a/dag/std/determinism.dag +++ b/dag/std/determinism.dag @@ -16,7 +16,7 @@ fn determinism_from_perturbation(verdict: PerturbationVerdict, reached: Declarat fn determinism_compose(outer: Determinism, inner: Determinism) -> Determinism { match outer { - NonDeterministic { source: s } => NonDeterministic { source: s } + NonDeterministic { source: s } => inner Deterministic => inner } } From 7db1da3aaa8a3d8857ed87daad4864c186e9b474 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 14 Jul 2026 00:52:23 +0000 Subject: [PATCH 4/9] Phase A: determinism grounded on perturbation, emergent source, single authority Replace the forked, inert determinism model with one grounded authority. - dag/std/determinism.dag: Determinism = Deterministic | NonDeterministic{source: DeclarationRef}, built on std.perturbation (determinism_from_perturbation bridges ResponseConsistent/Violation) + determinism_compose. The leak source is a reference to the reached root (emergent), not a NonDetSource label enum. Deletes the orphaned DeterminismAxis. - src/v2/std/determinism.dag: imports the authority; keeps only the signature binding (DeterminismFact) and the Bool projection (v2 side of the Bool fork). Deletes NonDetSource, the forked DeterminismClass, and the phantom-symbol roster. - determinism_contract_test.dag: rewritten to the grounded shape. 6 claims green by execution; discriminating RED verified (break compose -> propagation claims FAIL, revert -> PASS). Also fixes the CI red at bfd97ca, where a mid-edit snapshot paired the new v2 module with the stale test still importing the deleted symbols. Co-Authored-By: Claude Opus 4.8 (1M context) --- dag/std/determinism.dag | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dag/std/determinism.dag b/dag/std/determinism.dag index a03103a550c..1a51881ff14 100644 --- a/dag/std/determinism.dag +++ b/dag/std/determinism.dag @@ -16,7 +16,7 @@ fn determinism_from_perturbation(verdict: PerturbationVerdict, reached: Declarat fn determinism_compose(outer: Determinism, inner: Determinism) -> Determinism { match outer { - NonDeterministic { source: s } => inner + NonDeterministic { source: s } => NonDeterministic { source: s } Deterministic => inner } } From 96cc568b452d6be4cf81fff48a602d0a09dcc91f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 14 Jul 2026 01:30:16 +0000 Subject: [PATCH 5/9] WIP: emit determinism --- src/v1/stage0/src/cli_run.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index e48db5bc619..bc79b03be5b 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -12081,8 +12081,6 @@ 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/decl_index.dag::decl_facts_is_fn_like", "src/v2/std/float.dag::float_body_is_nan", "src/v2/std/node_minimal.dag::node_superset_field_eq", From 3b8a71cd6edac8b5982ed23b3681227742f3cdb5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 14 Jul 2026 01:48:15 +0000 Subject: [PATCH 6/9] WIP: emit determinism --- dag/std/determinism.dag | 6 +++--- src/v2/std/determinism.dag | 14 +++----------- 2 files changed, 6 insertions(+), 14 deletions(-) diff --git a/dag/std/determinism.dag b/dag/std/determinism.dag index 1a51881ff14..20bc289e23c 100644 --- a/dag/std/determinism.dag +++ b/dag/std/determinism.dag @@ -3,18 +3,18 @@ module std.determinism import std.perturbation { PerturbationVerdict, ResponseConsistent, ResponseViolation } import std.decl_ref { DeclarationRef } -type Determinism +type DeterminismAxis = Deterministic | NonDeterministic { source: DeclarationRef } -fn determinism_from_perturbation(verdict: PerturbationVerdict, reached: DeclarationRef) -> Determinism { +fn determinism_from_perturbation(verdict: PerturbationVerdict, reached: DeclarationRef) -> DeterminismAxis { match verdict { ResponseConsistent => Deterministic ResponseViolation => NonDeterministic { source: reached } } } -fn determinism_compose(outer: Determinism, inner: Determinism) -> Determinism { +fn determinism_compose(outer: DeterminismAxis, inner: DeterminismAxis) -> DeterminismAxis { match outer { NonDeterministic { source: s } => NonDeterministic { source: s } Deterministic => inner diff --git a/src/v2/std/determinism.dag b/src/v2/std/determinism.dag index ed0f33da49e..5a751bc963c 100644 --- a/src/v2/std/determinism.dag +++ b/src/v2/std/determinism.dag @@ -1,25 +1,17 @@ module v2.std.determinism -import std.determinism { Determinism, Deterministic, NonDeterministic } -import v2.std.logic { Bool } +import std.determinism { DeterminismAxis } import v2.std.node { Symbol } type DeterminismFact { signature: Symbol, - classification: Determinism + classification: DeterminismAxis } -fn determinism_fact_classification(fact: DeterminismFact) -> Determinism { +fn determinism_fact_classification(fact: DeterminismFact) -> DeterminismAxis { fact.classification } fn determinism_fact_signature(fact: DeterminismFact) -> Symbol { fact.signature } - -fn determinism_is_deterministic(c: Determinism) -> Bool { - match c { - Deterministic => true - NonDeterministic { source: _ } => false - } -} From 48a48fc7bdae051d9d626d5841f39d8c59729e0c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 14 Jul 2026 01:50:29 +0000 Subject: [PATCH 7/9] =?UTF-8?q?Address=20review:=20rename=20core=20to=20De?= =?UTF-8?q?terminismAxis=20(kill=20behavioral.Determinism=20=C2=A73=20coll?= =?UTF-8?q?ision),=20dissolve=20determinism=5Fis=5Fdeterministic=20Bool=20?= =?UTF-8?q?projection=20into=20a=20test-local=20helper,=20reconcile=20sign?= =?UTF-8?q?ed=20design=20doc=20with=20the=20emergent/perturbation=20pivot?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two REQUEST_CHANGES reviews on #6551: - claude-opus-4-7: stale NON_FOLD_RESIDUE_ROSTER entries (fixed in 96cc568b4). - cursor/composer-2.5: (1) type Determinism collided with std.behavioral.Determinism -> renamed back to DeterminismAxis (the signed-doc core name); the single-Determinism rename + behavioral dissolution stays in Phase E where EventuallyConsistent is handled. (2) determinism_is_deterministic was a v2.std coproduct->Bool predicate dissolution -> dissolved out of substrate; the contract test asserts via a test-local helper, mirroring the descent_evidence_lattice precedent. (3) signed design doc unreconciled -> supersession note records the operator's 2026-07-13 emergent/perturbation direction (no forged re-sign; new shape's details remain open to operator shape-review). Green-by-execution: 6 contract claims PASS, non_fold_residue_clean_holds PASS (unrostered+stale=0), discriminating RED confirmed (break compose left-propagation -> FAIL). Co-Authored-By: Claude Opus 4.8 (1M context) --- docs/plans/determinism-mechanism-design.md | 10 ++++++++ .../test/claim/determinism_contract_test.dag | 23 ++++++++++++------- 2 files changed, 25 insertions(+), 8 deletions(-) diff --git a/docs/plans/determinism-mechanism-design.md b/docs/plans/determinism-mechanism-design.md index f9e6ffecc48..6cff1cb1f48 100644 --- a/docs/plans/determinism-mechanism-design.md +++ b/docs/plans/determinism-mechanism-design.md @@ -9,6 +9,16 @@ --- +> **⚠️ SUPERSEDED IN PART — 2026-07-14 (operator direction, 2026-07-13, session `emit-determinism`).** The **source representation** below is superseded; the mechanism's principles are unchanged and strengthened. Specifically: +> - **Source is emergent, not labeled.** The `NonDetSource` label-enum (`HashIteration | TimeRead | RandomRead | EnvRead`, §0/§2-deep) is dissolved. Nondeterminism **emerges** by folding a node's dependencies to grounded external-world roots; the leak carries a **`DeclarationRef` reference to the root reached**, not a coined tag (operator: *"ideally that stuff is emergent from the modeling — I prefer not to model/label things as opposed to properly modeling dependencies"*). Grounded roots follow termination's shrunk registry (`measure_descent_fact_registry`): only the irreducible external-world leaf is grounded. +> - **Built on `std.perturbation`.** `ForwardSameInSameOut` *is* the objective definition (perturb outside declared inputs → output must not respond); determinism refines it by naming *which root* was reached. One objective, boundary-relative determinism usable by any node — not a compiler-only axis. +> - **Core carries the source directly.** P1's two-layer `DeterminismAxis` (core, two arms) + `DeterminismClass` (refinement, `source`) split is **collapsed**: `std.determinism.DeterminismAxis = Deterministic | NonDeterministic { source: DeclarationRef }` is the single authority. The core **name `DeterminismAxis` is retained** (avoids the `std.behavioral.Determinism` §3 collision the P1 name was chosen to prevent); the rename to a single `Determinism` lands together with the `behavioral`/`coordination` dissolution, not before. +> - **Preserved:** §3 single authority (vs `behavioral.determinism` / `perturbation` / `emit_determinism_gate`), §5 construction-over-validation and the located/typed-leak requirement, §7 signature-derived classification. FLAG 1 = A and FLAG 2 = C still hold. +> +> **Execution (phased, green-by-execution):** (A) grounded authority on perturbation, emergent source — **landed** (`dag/std/determinism.dag`, PR #6551); (B) ground roots via `kind: Observation` — *needs seed work + a `service→resource` binding not present in source, deferred/escalation-worthy*; (C) the emit lens over the `map_keys`/`sorted_map_keys` callee-symbol root (the class the x2 gate actually guards) — the gate replacement; (D) delete `emit_determinism_gate`; (E) unify `behavioral`/`coordination`, lift a convergence `Bound`, rename to single `Determinism`. This note records the operator's redirection; the new shape's detailed decisions remain open to operator shape-review. + +--- + ## 0. The one-sentence claim > **Determinism is a signature-derived classification axis orthogonal to `EffectShape`**, carried by `DeterminismFact { signature, classification }`, where `NonDeterministic { source: NonDetSource }` names one of four **grounded leak atoms** (`HashIteration | TimeRead | RandomRead | EnvRead`). A pure function's output must be a function of its declared inputs only; any dependence outside that key is a **located, typed `NonDetSource` leak**, not a silent bit-identical drift discovered later by `emit_determinism_gate`. diff --git a/src/v2/test/claim/determinism_contract_test.dag b/src/v2/test/claim/determinism_contract_test.dag index d19c0078110..4d202208624 100644 --- a/src/v2/test/claim/determinism_contract_test.dag +++ b/src/v2/test/claim/determinism_contract_test.dag @@ -2,6 +2,7 @@ module v2.test.claim.determinism_contract_test import std.decl_ref { DeclarationRef, WholeDeclaration } import std.determinism { + DeterminismAxis, Deterministic, NonDeterministic, determinism_compose, @@ -11,8 +12,7 @@ import std.perturbation { ResponseConsistent, ResponseViolation } import v2.std.determinism { DeterminismFact, determinism_fact_classification, - determinism_fact_signature, - determinism_is_deterministic + determinism_fact_signature } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import v2.std.logic { Bool } @@ -28,26 +28,33 @@ fn example_root() -> DeclarationRef { } } +fn det_is_deterministic(c: DeterminismAxis) -> Bool { + match c { + Deterministic => true + NonDeterministic { source: _ } => false + } +} + test fn determinism_perturbation_consistent_is_deterministic() -> Bool { - determinism_is_deterministic( + det_is_deterministic( c: determinism_from_perturbation(verdict: ResponseConsistent, reached: example_root()) ) } test fn determinism_perturbation_violation_is_nondeterministic() -> Bool { - !determinism_is_deterministic( + !det_is_deterministic( c: determinism_from_perturbation(verdict: ResponseViolation, reached: example_root()) ) } test fn determinism_compose_det_det_is_deterministic() -> Bool { - determinism_is_deterministic( + det_is_deterministic( c: determinism_compose(outer: Deterministic, inner: Deterministic) ) } test fn determinism_compose_nondet_left_propagates() -> Bool { - !determinism_is_deterministic( + !det_is_deterministic( c: determinism_compose( outer: NonDeterministic { source: example_root() }, inner: Deterministic @@ -56,7 +63,7 @@ test fn determinism_compose_nondet_left_propagates() -> Bool { } test fn determinism_compose_nondet_right_propagates() -> Bool { - !determinism_is_deterministic( + !det_is_deterministic( c: determinism_compose( outer: Deterministic, inner: NonDeterministic { source: example_root() } @@ -69,6 +76,6 @@ test fn determinism_fact_binds_signature_and_classification() -> Bool { signature: ^emit_export_set, classification: Deterministic } - determinism_is_deterministic(c: determinism_fact_classification(fact: fact)) + det_is_deterministic(c: determinism_fact_classification(fact: fact)) && (determinism_fact_signature(fact: fact) == ^emit_export_set) } From 7ceb8f4ce96b7f8745d9df2fd625b033d97bc410 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 14 Jul 2026 03:01:46 +0000 Subject: [PATCH 8/9] WIP: emit determinism --- src/v2/lens/determinism.dag | 111 ++++++++++++++++++++++++++++++++++++ 1 file changed, 111 insertions(+) create mode 100644 src/v2/lens/determinism.dag diff --git a/src/v2/lens/determinism.dag b/src/v2/lens/determinism.dag new file mode 100644 index 00000000000..7b9f1f5dd88 --- /dev/null +++ b/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 } +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 = [ + determinism_root_map_keys +] + +fn determinism_root_for_symbol(registry: List, s: Symbol) -> Optional { + fold(registry, init: Absent, f: fn(acc, row) { + match acc { + Present { value: _ } => acc + Absent => if row.signature == s { Present { value: row } } else { Absent } + } + }) +} + +fn node_callee_symbol(n: Node) -> Optional { + 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 } } => Present { value: sym } + _ => Absent + } + Absent => Absent + } + } else { + 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 { + 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 } +} From cd089bed8917578e7c2eceaf8b30ef28b00ed731 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 14 Jul 2026 03:10:10 +0000 Subject: [PATCH 9/9] =?UTF-8?q?Phase=20C.1:=20v2.lens.determinism=20?= =?UTF-8?q?=E2=80=94=20grounded=20map=5Fkeys=20root,=20emergent=20boundary?= =?UTF-8?q?-relative=20fold,=20live=20contract=20+=20discriminating=20witn?= =?UTF-8?q?ess?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The determinism authority (Phase A, #6551) gains its first live consumer. A new lens v2.lens.determinism grounds ^map_keys as the single nondeterministic root (its sibling sorted_map_keys canonicalizes it) and DERIVES a node's determinism by folding its structural closure to that root via std.determinism.determinism_compose — emergent, not labeled; boundary-relative (within-function structural closure). Unregistered callees contribute Deterministic at that boundary (map_keys is always a readable atom, never missed); cross-function reach is Phase F (resolved call edges), other roots (clock/entropy) Phase B (kind:Observation seed work). Mirrors cardinality.dag exactly: grounded List registry + first-match fold lookup + fold_node catamorphism (determinism_axis_for_node) + Witness contract (determinism_contract_witness) that Violates (located) on a nondeterministic reach. Enrolled in the lens registry (LensIdV0 Determinism arm + bound row). Scope is explicit, NOT silently narrowed: this is the mechanism + the contract over the clean v2 emit layer (src/v2 has zero map_keys — a forward-looking wall that reds the instant one enters). v1 05_emit_rust.dag stays under the x2 gate: its map_keys sites are order-safe (|>count, |>sort_by, let-bound) and need binding-aware dataflow (Phase C.2) before the gate can be deleted (Phase D / O1(b)). Green-by-execution: 5 witness claims PASS (map_keys+nested->Violates, sorted_map_keys+clean ->Holds, axis->NonDeterministic); registry coverage 2 PASS; discriminating RED confirmed (disable the map_keys root -> determinism_flags_map_keys_reach FAIL). Hygiene floors green: non_fold_residue, inert_carrier, wiring_liveness, and 10 enforcement gate_test consumers. Co-Authored-By: Claude Opus 4.8 (1M context) --- src/v2/lens/determinism.dag | 14 +-- .../lens/determinism/reach_witness_test.dag | 98 +++++++++++++++++++ src/v2/lens/registry.dag | 14 ++- src/v2/lens/registry/sg_claims_test.dag | 4 +- 4 files changed, 120 insertions(+), 10 deletions(-) create mode 100644 src/v2/lens/determinism/reach_witness_test.dag diff --git a/src/v2/lens/determinism.dag b/src/v2/lens/determinism.dag index 7b9f1f5dd88..fb9f908114c 100644 --- a/src/v2/lens/determinism.dag +++ b/src/v2/lens/determinism.dag @@ -5,7 +5,7 @@ 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 } +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 } @@ -37,10 +37,10 @@ data determinism_root_registry: List = [ ] fn determinism_root_for_symbol(registry: List, s: Symbol) -> Optional { - fold(registry, init: Absent, f: fn(acc, row) { + fold(registry, init: optional_absent(), f: fn(acc, row) { match acc { Present { value: _ } => acc - Absent => if row.signature == s { Present { value: row } } else { Absent } + Absent => if row.signature == s { optional_present(value: row) } else { optional_absent() } } }) } @@ -49,13 +49,13 @@ fn node_callee_symbol(n: Node) -> Optional { 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 } } => Present { value: sym } - _ => Absent + TypeNode { connective: Atom { identity: sym } } => optional_present(value: sym) + _ => optional_absent() } - Absent => Absent + Absent => optional_absent() } } else { - Absent + optional_absent() } } diff --git a/src/v2/lens/determinism/reach_witness_test.dag b/src/v2/lens/determinism/reach_witness_test.dag new file mode 100644 index 00000000000..d421399855a --- /dev/null +++ b/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) -> Bool { + match w { + Violates { diagnostic: _ } => true + Holds { value: _ } => false + } +} + +fn witness_holds(w: Witness) -> 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())) +} diff --git a/src/v2/lens/registry.dag b/src/v2/lens/registry.dag index 7261aa1d6b1..f722fec4743 100644 --- a/src/v2/lens/registry.dag +++ b/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 = [ lens_registry_v0_complexity, lens_registry_v0_cost, @@ -83,7 +88,8 @@ data lens_registry_v0: List = [ 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 + } } } diff --git a/src/v2/lens/registry/sg_claims_test.dag b/src/v2/lens/registry/sg_claims_test.dag index 791f9c713b8..d1957348287 100644 --- a/src/v2/lens/registry/sg_claims_test.dag +++ b/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 = [ Provenance, UnusedParameters, StructuralResolution, - TableDecisionTree + TableDecisionTree, + Determinism ] test fn lens_registry_required_ids_resolve_holds() -> Bool {