From 74fadc79694b1149ab86ce48dd57e0f606c4060f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 12:31:46 +0000 Subject: [PATCH 1/4] =?UTF-8?q?WIP:=20GroupCompletion=20grounding=20lane?= =?UTF-8?q?=20=E2=80=94=20numeric=20tower=20next=20layer,=20design-note-f?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- dag/std/algebra.dag | 5 +- src/v1/stage0/src/std_algebra.rs | 8 +- .../field_of_fractions_construction_test.rs | 89 +++++++++++++++++++ 3 files changed, 99 insertions(+), 3 deletions(-) create mode 100644 src/v1/tests/src/field_of_fractions_construction_test.rs diff --git a/dag/std/algebra.dag b/dag/std/algebra.dag index 00fa3903c5b..541656ded72 100644 --- a/dag/std/algebra.dag +++ b/dag/std/algebra.dag @@ -37,7 +37,10 @@ type AbelianGroup { type GroupCompletion -type FieldOfFractions +type FieldOfFractions { + num: R + denom: R +} type Semiring { add: fn(T, T) -> T diff --git a/src/v1/stage0/src/std_algebra.rs b/src/v1/stage0/src/std_algebra.rs index 49e49ecd7ee..72eb30023ae 100644 --- a/src/v1/stage0/src/std_algebra.rs +++ b/src/v1/stage0/src/std_algebra.rs @@ -64,8 +64,12 @@ pub struct AbelianGroup { #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct GroupCompletion(pub std::marker::PhantomData); -#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] -pub struct FieldOfFractions(pub std::marker::PhantomData); +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct FieldOfFractions { + pub num: R, + pub denom: R, + pub _phantom: std::marker::PhantomData, +} #[derive(Clone)] pub struct Semiring { diff --git a/src/v1/tests/src/field_of_fractions_construction_test.rs b/src/v1/tests/src/field_of_fractions_construction_test.rs new file mode 100644 index 00000000000..0eeec0c5018 --- /dev/null +++ b/src/v1/tests/src/field_of_fractions_construction_test.rs @@ -0,0 +1,89 @@ +use std::rc::Rc; + +use v1_compiler::cli_run; +use v1_compiler::v1_compiler_compile::{compile_to_resolved, ResolvedPipelineResult}; +use v1_compiler::v1_interpreter::{self, ExecutionMode, Value}; + +use crate::helpers::{resolve_imports_transitively_with_source_roots, workspace_root}; + +// Discriminating witness for the §7.2 FieldOfFractions model grounding (sharp-bee-290 +// sign-off): `FieldOfFractions = { num: R, denom: R }` is now a real 2-field record at +// its single authority (dag/std/algebra.dag). Unlike GroupCompletion (#7197), this is +// deliberately negative-space: FieldOfFractions has no native Rust scalar checkpoint to +// collapse into (Rational has no lossless native representation — an f64 collapse would be +// dishonest, per the design doc), so `eval_record_lit` must NOT special-case it. A plain +// `FieldOfFractions { num, denom }` construction with native `Value::Int` fields must stay +// a boxed `Value::Record` carrying both fields untouched. A regression that special-cases +// FieldOfFractions into any native collapse (silently lossy or otherwise) fails this +// witness; a regression that leaves the type hollow (no `num`/`denom` fields at all) fails +// to resolve at all, which this witness's `assert_resolved` also guards. +const RECEIPTS_SOURCE: &str = r#" +module test.field_of_fractions_construction + +import std.algebra { FieldOfFractions } + +fn one_half() -> FieldOfFractions { FieldOfFractions { num: 1, denom: 2 } } +fn three_quarters() -> FieldOfFractions { FieldOfFractions { num: 3, denom: 4 } } +"#; + +fn assert_resolved(resolved: &ResolvedPipelineResult) { + let msgs: Vec = resolved + .diagnostics + .iter() + .map(|d| v1_compiler::v1_std_core::diagnostic_to_message(d.diagnostic.clone())) + .filter(|m| !m.starts_with("complexity: ") && !m.starts_with("unlisted import use ")) + .collect(); + assert!( + msgs.is_empty() && resolved.graph.is_some(), + "receipts source should resolve cleanly, got {:?} (graph present: {})", + msgs, + resolved.graph.is_some(), + ); +} + +fn with_receipts_ctx(body: impl FnOnce(&v1_interpreter::InterpContext) -> R) -> R { + let ws = workspace_root(); + let roots = [ws.join("src/v2"), ws.join("dag")]; + let sources = + resolve_imports_transitively_with_source_roots("test.dag", RECEIPTS_SOURCE, &roots); + let resolved = compile_to_resolved(Rc::new(sources.into())); + assert_resolved(&resolved); + let graph = resolved.graph.as_ref().expect("graph"); + let ctx = + cli_run::make_eval_context(graph, resolved.source_indices.clone(), ExecutionMode::Wet); + body(&ctx) +} + +#[test] +fn field_of_fractions_pair_stays_boxed_record_not_native_collapse() { + with_receipts_ctx(|ctx| { + for (f, expected_num, expected_denom) in [ + ("one_half", 1i64, 2i64), + ("three_quarters", 3i64, 4i64), + ] { + match v1_interpreter::run_in_context(ctx, f, false) { + Ok(Value::Record { type_name, fields }) => { + assert!( + ctx.sym_eq(type_name, "FieldOfFractions"), + "{f}: expected type_name FieldOfFractions, got {}", + ctx.resolve(type_name) + ); + match ctx.field(&fields, "num") { + Some(Value::Int(n)) if *n == expected_num => {} + other => panic!("{f}: num field mismatch, got {other:?}"), + } + match ctx.field(&fields, "denom") { + Some(Value::Int(n)) if *n == expected_denom => {} + other => panic!("{f}: denom field mismatch, got {other:?}"), + } + } + other => panic!( + "{f}: expected a boxed Value::Record{{num, denom}} — FieldOfFractions has \ + no native Rust scalar to collapse into, so a regression that special-cases \ + it into any native Value variant (Int, Float, or otherwise) surfaces here; \ + got {other:?}" + ), + } + } + }); +} From aad4ae01c39095ad0d9ae350e1c2785ca41dd512 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 12:42:14 +0000 Subject: [PATCH 2/4] =?UTF-8?q?WIP:=20GroupCompletion=20grounding=20lane?= =?UTF-8?q?=20=E2=80=94=20numeric=20tower=20next=20layer,=20design-note-f?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...eld_of_fractions_construction_retained.dag | 9 +++ ...ld_of_fractions_single_declaration_test.rs | 79 +++++++++++++++++++ src/v1/tests/src/lib.rs | 4 + 3 files changed, 92 insertions(+) create mode 100644 dag/test/retirement/field_of_fractions_construction_retained.dag create mode 100644 src/v1/tests/src/field_of_fractions_single_declaration_test.rs diff --git a/dag/test/retirement/field_of_fractions_construction_retained.dag b/dag/test/retirement/field_of_fractions_construction_retained.dag new file mode 100644 index 00000000000..cefa7fed43e --- /dev/null +++ b/dag/test/retirement/field_of_fractions_construction_retained.dag @@ -0,0 +1,9 @@ +module test.retirement.field_of_fractions_construction_retained + + +data field_of_fractions_construction_retention: TestModuleRetirement = TestModuleRetirement { + module: "field_of_fractions_construction_test.rs", + disposition: RetainedNonMigratable { + reason: "This witness guards the eval_record_lit construction-side NON-collapse for FieldOfFractions \{ num, denom \} (§7.2 model grounding): a plain-record construction with native Value::Int fields must stay a boxed Value::Record carrying both fields untouched — the deliberate negative-space counterpart to GroupCompletion's collapse (#7197), since FieldOfFractions has no native Rust scalar checkpoint to collapse into (an f64 collapse would be lossy/dishonest; Real/ApproximateField already exists for that). The assertions pattern-match on the host interpreter's internal Value enum (Value::Record vs any native scalar) to catch a regression that special-cases FieldOfFractions into a native collapse — that representation-strategy distinction has no observable surface from within a .dag program (the language has no reflection over Value's native-vs-boxed shape), so it cannot migrate to an exact-stem test dag floor witness. Retained until src/v1 deletes at v2 self-host; not migration debt and not a delete candidate." + } +} diff --git a/src/v1/tests/src/field_of_fractions_single_declaration_test.rs b/src/v1/tests/src/field_of_fractions_single_declaration_test.rs new file mode 100644 index 00000000000..a4e6a3cbdce --- /dev/null +++ b/src/v1/tests/src/field_of_fractions_single_declaration_test.rs @@ -0,0 +1,79 @@ +//! De-fork non-regression witness for the §7.2 FieldOfFractions model grounding. +//! +//! Unlike GroupCompletion (#7197), FieldOfFractions had no existing §3 fork at the time the +//! model landed — this witness guards against a FUTURE fork appearing (a second independent +//! `type FieldOfFractions` declaration anywhere in the corpus, which would duplicate the +//! single authority at dag/std/algebra.dag and desynchronize from it). Reads corpus SHAPE +//! (a per-file top-level `type FieldOfFractions` declaration head), not contents. + +fn workspace_root() -> std::path::PathBuf { + std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("../../..") + .canonicalize() + .expect("workspace root") +} + +fn collect_dag_files(dir: &std::path::Path, out: &mut Vec) { + let mut entries: Vec<_> = match std::fs::read_dir(dir) { + Ok(e) => e.filter_map(|x| x.ok()).collect(), + Err(_) => return, + }; + entries.sort_by_key(|e| e.file_name()); + for e in entries { + let p = e.path(); + if p.is_dir() { + collect_dag_files(&p, out); + } else if p.extension().map(|x| x == "dag").unwrap_or(false) { + out.push(p); + } + } +} + +fn declares_field_of_fractions(content: &str) -> bool { + content.lines().any(|line| { + let t = line.trim_start(); + t.starts_with("type FieldOfFractions") || t.starts_with("type FieldOfFractions<") + }) +} + +#[test] +fn field_of_fractions_has_exactly_one_declaration_corpuswide() { + let ws = workspace_root(); + let mut files = Vec::new(); + for dir in ["dag", "src/v2"] { + collect_dag_files(&ws.join(dir), &mut files); + } + assert!(!files.is_empty(), "no .dag sources found under dag/ or src/v2/"); + + let declaring: Vec = files + .into_iter() + .filter_map(|p| { + let content = std::fs::read_to_string(&p).ok()?; + if declares_field_of_fractions(&content) { + Some(p.strip_prefix(&ws).unwrap_or(&p).to_string_lossy().into_owned()) + } else { + None + } + }) + .collect(); + + assert_eq!( + declaring, + vec!["dag/std/algebra.dag".to_string()], + "FieldOfFractions must have exactly one declaration at its single authority \ + (dag/std/algebra.dag) — a second declaration anywhere else in the corpus is a §3 \ + fork; found: {declaring:?}" + ); +} + +// Red control: the scanner itself must actually detect a declaration when one exists, +// not just report zero unconditionally. +#[test] +fn declares_field_of_fractions_detects_a_real_declaration() { + assert!(declares_field_of_fractions( + "module std.algebra\n\ntype FieldOfFractions {\n num: R\n denom: R\n}\n" + )); + assert!(!declares_field_of_fractions( + "module std.algebra\n\ntype GroupCompletion {\n pos: M\n neg: M\n}\n" + )); +} diff --git a/src/v1/tests/src/lib.rs b/src/v1/tests/src/lib.rs index 3b18398da03..d315d0633bb 100644 --- a/src/v1/tests/src/lib.rs +++ b/src/v1/tests/src/lib.rs @@ -51,6 +51,10 @@ mod faithful_string_element_char_witness_test; #[cfg(test)] mod field_import_surface_generic_arg_test; #[cfg(test)] +mod field_of_fractions_construction_test; +#[cfg(test)] +mod field_of_fractions_single_declaration_test; +#[cfg(test)] mod floor_drain_retention_test; #[cfg(test)] mod fn_as_value_test; From 1b3357f5c2e45e8d8209e26a74ad0a8e557c24a0 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 12:42:32 +0000 Subject: [PATCH 3/4] =?UTF-8?q?FieldOfFractions=20=C2=A77.2:=20de-fork=20n?= =?UTF-8?q?on-regression=20+=20negative-space=20no-collapse=20witnesses?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Registers the two remaining model-scoped witnesses for the FieldOfFractions grounding (dag/std/algebra.dag, num/denom body landed in the prior commit): - field_of_fractions_single_declaration_test: corpus-wide grep-shape witness asserting exactly one `type FieldOfFractions` declaration exists (guards against a future §3 fork; FieldOfFractions had no existing fork to delete, unlike GroupCompletion in #7197). - field_of_fractions_construction_test (retirement-tagged, Rust-retained): asserts eval_record_lit does NOT special-case FieldOfFractions into a native scalar collapse — the deliberate negative-space counterpart to GroupCompletion's collapse, since Rational has no lossless native checkpoint to collapse into. Scope: model only, per sharp-bee-290 sign-off. §7.3 realization (emitter Rust-struct emission + generic arithmetic trait derivation) is explicitly held pending separate sign-off and gated on Root-4. Co-Authored-By: Claude Sonnet 5 --- .../src/field_of_fractions_construction_test.rs | 7 +++---- .../field_of_fractions_single_declaration_test.rs | 12 ++++++++++-- 2 files changed, 13 insertions(+), 6 deletions(-) diff --git a/src/v1/tests/src/field_of_fractions_construction_test.rs b/src/v1/tests/src/field_of_fractions_construction_test.rs index 0eeec0c5018..e3c6118ecee 100644 --- a/src/v1/tests/src/field_of_fractions_construction_test.rs +++ b/src/v1/tests/src/field_of_fractions_construction_test.rs @@ -57,10 +57,9 @@ fn with_receipts_ctx(body: impl FnOnce(&v1_interpreter::InterpContext) -> R) #[test] fn field_of_fractions_pair_stays_boxed_record_not_native_collapse() { with_receipts_ctx(|ctx| { - for (f, expected_num, expected_denom) in [ - ("one_half", 1i64, 2i64), - ("three_quarters", 3i64, 4i64), - ] { + for (f, expected_num, expected_denom) in + [("one_half", 1i64, 2i64), ("three_quarters", 3i64, 4i64)] + { match v1_interpreter::run_in_context(ctx, f, false) { Ok(Value::Record { type_name, fields }) => { assert!( diff --git a/src/v1/tests/src/field_of_fractions_single_declaration_test.rs b/src/v1/tests/src/field_of_fractions_single_declaration_test.rs index a4e6a3cbdce..914856746dd 100644 --- a/src/v1/tests/src/field_of_fractions_single_declaration_test.rs +++ b/src/v1/tests/src/field_of_fractions_single_declaration_test.rs @@ -43,14 +43,22 @@ fn field_of_fractions_has_exactly_one_declaration_corpuswide() { for dir in ["dag", "src/v2"] { collect_dag_files(&ws.join(dir), &mut files); } - assert!(!files.is_empty(), "no .dag sources found under dag/ or src/v2/"); + assert!( + !files.is_empty(), + "no .dag sources found under dag/ or src/v2/" + ); let declaring: Vec = files .into_iter() .filter_map(|p| { let content = std::fs::read_to_string(&p).ok()?; if declares_field_of_fractions(&content) { - Some(p.strip_prefix(&ws).unwrap_or(&p).to_string_lossy().into_owned()) + Some( + p.strip_prefix(&ws) + .unwrap_or(&p) + .to_string_lossy() + .into_owned(), + ) } else { None } From 10fbfb19b922ac422c5fe4eed2fb47d35f508eff Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 25 Jul 2026 20:39:23 +0000 Subject: [PATCH 4/4] WIP: Numeric grounding: GroupCompletion real bodies + orphaned PRs --- .../field_of_fractions_single_declaration_retained.dag | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 dag/test/retirement/field_of_fractions_single_declaration_retained.dag diff --git a/dag/test/retirement/field_of_fractions_single_declaration_retained.dag b/dag/test/retirement/field_of_fractions_single_declaration_retained.dag new file mode 100644 index 00000000000..a4870ca99a5 --- /dev/null +++ b/dag/test/retirement/field_of_fractions_single_declaration_retained.dag @@ -0,0 +1,9 @@ +module test.retirement.field_of_fractions_single_declaration_retained + + +data field_of_fractions_single_declaration_retention: TestModuleRetirement = TestModuleRetirement { + module: "field_of_fractions_single_declaration_test.rs", + disposition: RetainedNonMigratable { + reason: "This witness guards the §7.2 FieldOfFractions de-fork non-regression: a corpus-wide filesystem walk over dag/ and src/v2/ must find exactly one top-level `type FieldOfFractions` declaration, at dag/std/algebra.dag — a second declaration anywhere else is a §3 fork that desynchronizes from the single authority. The scan reads host filesystem shape (per-file declaration heads), not an interpreter-observable .dag surface, so it cannot migrate to an exact-stem test dag floor witness. Retained until src/v1 deletes at v2 self-host; not migration debt and not a delete candidate." + } +}