Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
1be8157
WIP: nimble-pike-489
briansrls Apr 30, 2026
0a1f838
feat(grounding-coercion-fold): Examples 1–2 scratch path (design-emis…
briansrls Apr 30, 2026
db82a05
test(grounding-tests): assert exact Stratum A extra-field diagnostic
briansrls Apr 30, 2026
e7bb35d
Merge remote-tracking branch 'origin/main' into refactor/grounding-li…
briansrls Apr 30, 2026
0f5c9a0
WIP: nimble-pike-489
briansrls Apr 30, 2026
daea209
chore: apply cargo fmt
briansrls Apr 30, 2026
2e3cfc3
WIP: nimble-pike-489
briansrls Apr 30, 2026
160436f
Merge remote-tracking branch 'origin/main' into refactor/grounding-li…
briansrls Apr 30, 2026
cedf2c9
test(grounding-tests): split Stratum A extra-field checks into two tests
briansrls Apr 30, 2026
c4a0def
Merge remote-tracking branch 'origin/main' into refactor/grounding-li…
briansrls Apr 30, 2026
a098071
WIP: nimble-pike-489
briansrls Apr 30, 2026
86f35d6
Merge remote-tracking branch 'origin/main' into refactor/grounding-li…
briansrls Apr 30, 2026
778fc12
test(grounding-tests): structural witness for Int vs MethodDeclaratio…
briansrls Apr 30, 2026
fcd4295
docs(grounding-coercion-fold): Practice 4 checkpoint on EmissionDiagn…
briansrls Apr 30, 2026
e909a89
docs(grounding-coercion-fold): sharpen scratch-path dissolution guard…
briansrls Apr 30, 2026
52eab5c
WIP: nimble-pike-489
briansrls Apr 30, 2026
2a874d7
Merge remote-tracking branch 'origin/main' into refactor/grounding-li…
briansrls Apr 30, 2026
af4fc8d
WIP: nimble-pike-489
briansrls May 1, 2026
80b36da
Merge remote-tracking branch 'origin/main' into refactor/grounding-li…
briansrls May 1, 2026
80a7d2d
Merge remote-tracking branch 'origin/main' into refactor/grounding-li…
briansrls May 1, 2026
02aa822
refactor(grounding-coercion-fold): rename lifetime_facts for scratch …
briansrls May 1, 2026
a3164a6
Merge remote-tracking branch 'origin/main' into refactor/grounding-li…
briansrls May 1, 2026
3c98d52
docs(grounding-coercion-fold): document UnderRefined axis string staging
briansrls May 1, 2026
9b861f5
Merge remote-tracking branch 'origin/main' into refactor/grounding-li…
briansrls May 1, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 17 additions & 3 deletions src/v3/grounding_coercion_fold/src/diagnostic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,26 @@
//!
//! **Lockstep discipline:** any new variant added to substrate
//! `EmissionDiagnostic` MUST land here as a parallel Rust mirror update.
//!
//! **Example 1 (scratch path):** design-emission-model §Example 1 names richer
//! diagnostic fields (candidates, hints). Until the substrate carrier carries
//! those structurally, the fold surfaces the **substrate-shaped** `UnderRefined`
//! with `unspecified_axis: "bound"` only (axis matches the worked example).

/// Rust mirror of substrate `EmissionDiagnostic` (subset; this crate
/// only emits `FoldNotImplemented`). Variant-name lockstep enforced
/// socially until reflection codegen retires the mirror.
/// Rust mirror of substrate `EmissionDiagnostic` (subset; grows with substrate).
///
/// Practice 4 (`docs/modeling-discipline.md`): **🟡 YELLOW** — hand-maintained mirror until this
/// lane consumes reflected substrate types (`.dag` → Rust enum codegen); dissolution aligns with
/// #1216 / #1133 (no second authority for the same diagnostic facts — lockstep only).
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub enum EmissionDiagnostic {
/// Program intent or structural axis under-specified (substrate `UnderRefined`).
UnderRefined {
/// Mirrors substrate’s string axis payload for now. Scratch Example 1 only supplies
/// `"bound"`; when substrate grows structured axes (or this mirror gains a sum type),
/// replace free-form spelling here rather than widening implicit string conventions.
unspecified_axis: String,
},
/// Full structural fold is not implemented; returning `Ok` would fabricate
/// target choices (C-8 / `INVARIANTS.md`).
FoldNotImplemented,
Expand Down
73 changes: 52 additions & 21 deletions src/v3/grounding_coercion_fold/src/fold.rs
Original file line number Diff line number Diff line change
@@ -1,39 +1,70 @@
//! Structural fold entry — **algorithm stub only**.
//! Structural fold entry — coercion = emission (incremental body).
//!
//! ## Design authority (`docs/design-emission-model.md`)
//!
//! The eventual fold reads **program intent** + **substrate facts** (LanguageSpec rows,
//! algebra inhabitance, lifetime facts, …) and returns either a **unique** target
//! inhabitance per binding or a typed [`EmissionDiagnostic`](crate::diagnostic::EmissionDiagnostic).
//! Worked **Examples 1–7** in that doc (e.g. unrefined `Int` → `UnderRefined`, bounded
//! refinement → `u32`, `String` ownership cases, algebra ambiguity, no-inhabitant,
//! cross-target portability sketches) are the **behavioral targets** for the future
//! implementation — **not** implemented in this crate yet.
//! Worked **Examples 1–7** in that doc are behavioral targets. **Examples 1–2** are
//! implemented for the [`LanguageSpecProjection::ScratchIntExamples`](crate::types::LanguageSpecProjection::ScratchIntExamples)
//! checkpoint path only; other examples and `Undeclared` remain
//! [`EmissionDiagnostic::FoldNotImplemented`](crate::diagnostic::EmissionDiagnostic::FoldNotImplemented).
//!
//! ## Gates (dispatch)
//!
//! Full body is gated on T-Ground-LanguageSpec row work post-#1227 and lifetime /
//! substrate boundary metadata (#1130). This module only enforces the **public
//! signature** and **fail-closed** stub (`FoldNotImplemented`).
//! **Call-site (ScratchIntExamples):** While the scratch body ignores `dag` / lifetime inputs and
//! fixes [`BindingId`](v3_grounding_lifetime::BindingId)`(0)`, production wiring must not treat
//! returned map keys as evidence of real program bindings (#1133 / #1286).

use std::collections::BTreeMap;

use v3_compiler::dag::Dag;
use v3_grounding_lifetime::{BindingId, LifetimeAnalysisReport};

use crate::diagnostic::EmissionDiagnostic;
use crate::types::{LanguageSpecProjectionUndeclared, TargetInhabitance};
use crate::types::{IntScratchExample, LanguageSpecProjection, TargetInhabitance};

fn fold_design_doc_example_1_unrefined_int() -> Result<TargetInhabitance, EmissionDiagnostic> {
Err(EmissionDiagnostic::UnderRefined {
unspecified_axis: "bound".to_string(),
})
}

fn fold_design_doc_example_2_semiring_u32() -> Result<TargetInhabitance, EmissionDiagnostic> {
Ok(TargetInhabitance::RustU32)
}

/// Structural fold: program + lifetime analysis + (future) LanguageSpec projection →
/// Structural fold: program + lifetime analysis + LanguageSpec projection →
/// per-binding target inhabitances, **or** a single typed diagnostic.
///
/// Today: **always** [`EmissionDiagnostic::FoldNotImplemented`](EmissionDiagnostic::FoldNotImplemented)
/// (C-8). Parameters are accepted so call sites compile against the eventual shape;
/// they are intentionally unused until the fold body lands.
/// - [`LanguageSpecProjection::Undeclared`](crate::types::LanguageSpecProjection::Undeclared): fail-closed
/// [`EmissionDiagnostic::FoldNotImplemented`](crate::diagnostic::EmissionDiagnostic::FoldNotImplemented).
/// - [`LanguageSpecProjection::ScratchIntExamples`](crate::types::LanguageSpecProjection::ScratchIntExamples): runs
/// design-doc Examples 1–2 for a single synthetic binding [`BindingId`](v3_grounding_lifetime::BindingId)`(0)`.
/// **Checkpoint:** ignores `_dag` by design; on the scratch path, `lifetime_facts` must be
/// empty in debug builds until this body reads real facts. Do not widen this arm to multiple
/// bindings or real program facts without landing the declared projection / dissolution path
/// first (#1133 / #1286).
pub fn fold_program_to_target(
_dag: &Dag,
_lifetime_facts: &LifetimeAnalysisReport,
_language_spec: &LanguageSpecProjectionUndeclared,
lifetime_facts: &LifetimeAnalysisReport,
language_spec: &LanguageSpecProjection,
) -> Result<BTreeMap<BindingId, TargetInhabitance>, EmissionDiagnostic> {
Err(EmissionDiagnostic::FoldNotImplemented)
match language_spec {
LanguageSpecProjection::Undeclared => {
let _ = lifetime_facts;
Err(EmissionDiagnostic::FoldNotImplemented)
}
LanguageSpecProjection::ScratchIntExamples(example) => {
debug_assert!(
lifetime_facts.is_empty(),
"ScratchIntExamples checkpoint: pass an empty LifetimeAnalysisReport until this body reads facts (#1133 / #1286)"
);
let binding = BindingId(0);
let inhabitance = match example {
IntScratchExample::DesignDocExample1UnrefinedInt => {
fold_design_doc_example_1_unrefined_int()?
}
IntScratchExample::DesignDocExample2BoundedU32 => {
fold_design_doc_example_2_semiring_u32()?
}
};
Ok(BTreeMap::from([(binding, inhabitance)]))
}
}
}
80 changes: 51 additions & 29 deletions src/v3/grounding_coercion_fold/src/lib.rs
Original file line number Diff line number Diff line change
@@ -1,43 +1,34 @@
//! T-Ground-Coercion-Fold — **consumer-side scaffold** for the structural emission fold.
//! T-Ground-Coercion-Fold — structural emission fold (**coercion = emission**).
//!
//! Per [`docs/design-emission-model.md`](../../../../docs/design-emission-model.md) lane table
//! (~381–384), this lane is the mechanical **coercion = emission** fold: read program
//! intent + substrate facts, return a unique target inhabitance per binding or
//! [`EmissionDiagnostic`](diagnostic::EmissionDiagnostic). It **replaces** the retracted
//! T-Ground-Engine framing (no separate coercion engine).
//! Per [`docs/design-emission-model.md`](../../../../docs/design-emission-model.md), this lane
//! reads program intent + substrate facts and returns a unique target inhabitance per binding
//! or [`EmissionDiagnostic`](diagnostic::EmissionDiagnostic).
//!
//! ## Algorithm-shape (stub)
//! ## Implemented today
//!
//! - [`fold_program_to_target`](fold::fold_program_to_target) is the public entry matching
//! the manager dispatch shape: [`v3_compiler::dag::Dag`], [`v3_grounding_lifetime::LifetimeAnalysisReport`],
//! and [`types::LanguageSpecProjectionUndeclared`] (open carrier — **do not** guess final
//! LanguageSpec projection).
//! - Until LanguageSpec + Dag boundary work land, the fold **fail-closed** returns
//! [`EmissionDiagnostic::FoldNotImplemented`](diagnostic::EmissionDiagnostic::FoldNotImplemented)
//! for all inputs (C-8).
//!
//! ## Worked examples (targets for future implementation; not implemented here)
//!
//! Authoritative walkthroughs live in [`docs/design-emission-model.md`](../../../../docs/design-emission-model.md)
//! **§Worked examples** — including at minimum **Example 1** (unrefined `Int` → fail-closed
//! diagnostic), **Example 2** (`Int(0..2^32)` → Rust `u32`), **Examples 3–4** (`String`
//! ownership / lifetime), **Example 5** (algebra ambiguity), **Example 6** (`NoInhabitant`),
//! and **Example 7** / cross-target sketches tied to Modeling problem 7. This crate’s
//! rustdoc on [`fold`](crate::fold) cites the same authority without duplicating payloads.
//! - [`fold_program_to_target`](fold::fold_program_to_target) with
//! [`LanguageSpecProjection::Undeclared`](types::LanguageSpecProjection::Undeclared) stays
//! fail-closed [`EmissionDiagnostic::FoldNotImplemented`](diagnostic::EmissionDiagnostic::FoldNotImplemented).
//! - [`LanguageSpecProjection::ScratchIntExamples`](types::LanguageSpecProjection::ScratchIntExamples)
//! drives **design-emission-model §Example 1** (unrefined `Int` → substrate-shaped
//! [`EmissionDiagnostic::UnderRefined`](diagnostic::EmissionDiagnostic::UnderRefined) with axis `"bound"`)
//! and **§Example 2** (`Int(0..2^32)` / `Semiring` exact-bound → [`TargetInhabitance::RustU32`](types::TargetInhabitance::RustU32))
//! for a single synthetic binding — checkpoint until a real LanguageSpec projection replaces
//! the scratch carrier (manager #1133 / #1286).
//!
//! ## SG-0 / discipline
//!
//! - **No** edits under [`src/v3/compiler/`](../../compiler) — consume `v3-compiler` APIs only.
//! - Lane-local [`EmissionDiagnostic`](diagnostic::EmissionDiagnostic) mirrors the Lifetime-Analyzer
//! pattern; converges on substrate carrier per `docs/briefs/t-ground-diagnostic.md` / #1216.
//! - Lane-local [`EmissionDiagnostic`](diagnostic::EmissionDiagnostic) converges per
//! `docs/briefs/t-ground-diagnostic.md` / #1216.

mod diagnostic;
mod fold;
mod types;

pub use diagnostic::EmissionDiagnostic;
pub use fold::fold_program_to_target;
pub use types::{LanguageSpecProjectionUndeclared, TargetInhabitance};
pub use types::{IntScratchExample, LanguageSpecProjection, TargetInhabitance};

#[cfg(test)]
mod tests {
Expand All @@ -47,11 +38,42 @@ mod tests {
use super::*;

#[test]
fn fold_stub_fail_closed_fold_not_implemented() {
fn fold_undeclared_projection_stays_fold_not_implemented() {
let dag = Dag::new();
let lifetime: LifetimeAnalysisReport = Default::default();
let spec = LanguageSpecProjectionUndeclared;
let err = fold_program_to_target(&dag, &lifetime, &spec).expect_err("stub");
let spec = LanguageSpecProjection::Undeclared;
let err = fold_program_to_target(&dag, &lifetime, &spec).expect_err("undeclared");
assert_eq!(err, EmissionDiagnostic::FoldNotImplemented);
}

#[test]
fn design_doc_example_1_unrefined_int_under_refined() {
let dag = Dag::new();
let lifetime: LifetimeAnalysisReport = Default::default();
let spec = LanguageSpecProjection::ScratchIntExamples(
IntScratchExample::DesignDocExample1UnrefinedInt,
);
let err = fold_program_to_target(&dag, &lifetime, &spec).expect_err("under-refined");
assert_eq!(
err,
EmissionDiagnostic::UnderRefined {
unspecified_axis: "bound".to_string(),
}
);
}

#[test]
fn design_doc_example_2_bounded_int_emits_rust_u32() {
let dag = Dag::new();
let lifetime: LifetimeAnalysisReport = Default::default();
let spec = LanguageSpecProjection::ScratchIntExamples(
IntScratchExample::DesignDocExample2BoundedU32,
);
let got = fold_program_to_target(&dag, &lifetime, &spec).expect("ok");
assert_eq!(got.len(), 1);
assert_eq!(
got.get(&v3_grounding_lifetime::BindingId(0)),
Some(&TargetInhabitance::RustU32)
);
}
}
52 changes: 39 additions & 13 deletions src/v3/grounding_coercion_fold/src/types.rs
Original file line number Diff line number Diff line change
@@ -1,17 +1,43 @@
//! Open / stub carriers for the public fold signature until LanguageSpec + lowering land.
//! LanguageSpec projection + target inhabitance carriers for the structural fold.

/// Placeholder for the structural **LanguageSpec** projection the fold will consume.
/// How the fold obtains LanguageSpec / target-primitive substrate facts.
///
/// **Shape TBD** — manager dispatch (#1203 / #1133): substrate may declare a projection
/// carrier, or the fold may walk [`v3_compiler::dag::Dag`] directly. **Do not** treat this
/// type as the final API. No row consumption until LanguageSpec Phase 1.5 (#1227) and
/// related substrate gates land.
#[derive(Debug, Clone, Copy, Default, PartialEq, Eq, Hash)]
pub struct LanguageSpecProjectionUndeclared;
/// Practice 4 (`docs/modeling-discipline.md`): **🟡 YELLOW** — `Undeclared` awaits a declared
/// LanguageSpec projection; `ScratchIntExamples` is an interim checkpoint. Named dissolution:
/// #1133 / #1286 (declared projection replaces this carrier).
///
/// **`Undeclared`** — production entry stays fail-closed until a real projection lands
/// (substrate / #1286 / manager #1133).
///
/// **`ScratchIntExamples`** — **checkpoint only**: drives [`docs/design-emission-model.md`](../../../../docs/design-emission-model.md)
/// **Example 1** and **Example 2** without walking Phase 1 Dag rows. Remove or supersede when
/// a declared projection replaces this scratch path.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default)]
pub enum LanguageSpecProjection {
#[default]
Undeclared,
ScratchIntExamples(IntScratchExample),
}

/// Scratch selector aligned to design-emission-model §Worked examples (Int only).
///
/// Practice 4 (`docs/modeling-discipline.md`): **🟡 YELLOW** — bounded to Examples 1–2 only;
/// superseded when a declared projection generalizes Int examples (#1133 / #1286).
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum IntScratchExample {
/// Example 1 — `data x: Int = 0` → `EmissionDiagnostic::UnderRefined`.
DesignDocExample1UnrefinedInt,
/// Example 2 — `data count: Int(0..2^32) = 100` → unique Rust `u32`.
DesignDocExample2BoundedU32,
}

/// Stub for **unique per-binding target inhabitance** (primitive + refinement witness).
/// Unique target inhabitance for a binding (Examples 1–2 surface only).
///
/// Populated by the real Coercion-Fold body when T-Ground-LanguageSpec + extraction
/// gates unblock; the scaffold never returns `Ok` with populated values.
#[derive(Debug, Clone, Copy, Default, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct TargetInhabitance;
/// Practice 4 (`docs/modeling-discipline.md`): single-variant placeholder — N \< 2, so no 🟢/🟡/🔴
/// coproduct checkpoint until a second inhabitant is introduced. When a second variant lands,
/// classify this enum explicitly (substrate vs Rust mirror / dissolution) — do not grow ad hoc
/// without the same checkpoint discipline as the projection carriers.
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub enum TargetInhabitance {
RustU32,
}
Loading
Loading