From 2a42e5e6faf61de9ecde1ae3cf5bb17cebcdb0fc Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 29 Jun 2026 15:25:31 +0000 Subject: [PATCH] =?UTF-8?q?=C2=A75=20determinism=20mechanism=20P1:=20core?= =?UTF-8?q?=20axis,=20roster,=20compose=20algebra,=20witnesses.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Re-harvest closed #5941 onto fresh main (post-#5937 design merge): - v2.std.determinism primitive roster + determinism_compose algebra + witness data - dsl/std/determinism.dag DeterminismAxis authority - determinism_contract_test.dag (7 fail-closed witnesses) - design doc reconciled as MODIFY on #5937; DESIGN.md + ROADMAP.md regen'd - non_fold_residue roster: determinism_class_eq + non_det_source_eq Co-authored-by: Cursor --- DESIGN.md | 2 +- ROADMAP.md | 2 + docs/plans/determinism-mechanism-design.md | 11 +- dsl/gunbc/design_document.dag | 2 +- dsl/gunbc/roadmap_authority.dag | 1 + dsl/std/determinism.dag | 5 + src/v1/stage0/src/non_fold_residue_project.rs | 2 + src/v2/std/determinism.dag | 147 ++++++++++++++++++ .../test/claim/determinism_contract_test.dag | 87 +++++++++++ 9 files changed, 251 insertions(+), 8 deletions(-) create mode 100644 dsl/std/determinism.dag create mode 100644 src/v2/test/claim/determinism_contract_test.dag diff --git a/DESIGN.md b/DESIGN.md index d30057d18d7..e119e8efe6a 100644 --- a/DESIGN.md +++ b/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) diff --git a/ROADMAP.md b/ROADMAP.md index 4e6cf7d04bb..fe6bfe902a6 100644 --- a/ROADMAP.md +++ b/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) diff --git a/docs/plans/determinism-mechanism-design.md b/docs/plans/determinism-mechanism-design.md index 5f2feb54974..67b64de3ae9 100644 --- a/docs/plans/determinism-mechanism-design.md +++ b/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+. diff --git a/dsl/gunbc/design_document.dag b/dsl/gunbc/design_document.dag index d214c623bf8..e89b3d80c90 100644 --- a/dsl/gunbc/design_document.dag +++ b/dsl/gunbc/design_document.dag @@ -138,7 +138,7 @@ fn open_threads_blocks() -> List { [ 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)"), diff --git a/dsl/gunbc/roadmap_authority.dag b/dsl/gunbc/roadmap_authority.dag index 7861a44b259..a6acf867151 100644 --- a/dsl/gunbc/roadmap_authority.dag +++ b/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: [ diff --git a/dsl/std/determinism.dag b/dsl/std/determinism.dag new file mode 100644 index 00000000000..dda0a3764bf --- /dev/null +++ b/dsl/std/determinism.dag @@ -0,0 +1,5 @@ +module std.determinism + +type DeterminismAxis + = Deterministic + | NonDeterministic diff --git a/src/v1/stage0/src/non_fold_residue_project.rs b/src/v1/stage0/src/non_fold_residue_project.rs index 4cbbfc3e10f..04cc6f63f90 100644 --- a/src/v1/stage0/src/non_fold_residue_project.rs +++ b/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", diff --git a/src/v2/std/determinism.dag b/src/v2/std/determinism.dag index 87a023976f9..c6947df1b28 100644 --- a/src/v2/std/determinism.dag +++ b/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 { + 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 { + 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 +} diff --git a/src/v2/test/claim/determinism_contract_test.dag b/src/v2/test/claim/determinism_contract_test.dag new file mode 100644 index 00000000000..41d50951b65 --- /dev/null +++ b/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 + } +}