Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
12bff6f
WIP: nimble-pike-489
briansrls Apr 29, 2026
8418b20
WIP: nimble-pike-489
briansrls Apr 29, 2026
746273e
chore: apply cargo fmt
briansrls Apr 29, 2026
b795b28
Merge remote-tracking branch 'origin/main' into session/nimble-pike-489
briansrls Apr 29, 2026
d1272ed
Merge remote-tracking branch 'origin/main' into session/nimble-pike-489
briansrls Apr 29, 2026
6294277
WIP: nimble-pike-489
briansrls Apr 29, 2026
fc14a34
WIP: nimble-pike-489
briansrls Apr 29, 2026
e0fde02
WIP: nimble-pike-489
briansrls Apr 29, 2026
4d2405a
chore: apply cargo fmt
briansrls Apr 29, 2026
9778ec4
fix(grounding-lifetime): address api-review tidy-ups (PR #1206)
briansrls Apr 29, 2026
43dde23
fix(grounding-lifetime): fail-closed growability for borrowed params …
briansrls Apr 29, 2026
ba8b527
fix(grounding-lifetime): require transient proof for opaque param use…
briansrls Apr 29, 2026
487530c
docs(grounding-lifetime): Practice 4 enum checkpoints (PR #1206)
briansrls Apr 29, 2026
78207d8
Merge remote-tracking branch 'origin/main' into session/nimble-pike-489
briansrls Apr 29, 2026
60ff47f
Merge remote-tracking branch 'origin/main' into session/nimble-pike-489
briansrls Apr 29, 2026
c3025cd
Merge remote-tracking branch 'origin/main' into session/nimble-pike-489
briansrls Apr 29, 2026
cead784
WIP: nimble-pike-489
briansrls Apr 29, 2026
613c5fd
docs(briefs): author T-Ground-Diagnostic lane brief
briansrls Apr 29, 2026
44f0dfc
Merge remote-tracking branch 'origin/main' into session/nimble-pike-489
briansrls Apr 29, 2026
5432984
WIP: nimble-pike-489
briansrls Apr 29, 2026
05e4ff3
chore: apply cargo fmt
briansrls Apr 29, 2026
a82f46a
WIP: nimble-pike-489
briansrls Apr 29, 2026
c1f61e5
docs(grounding-lifetime): sync program IR rustdoc with extraction C-8…
briansrls Apr 29, 2026
6f88ab3
WIP: nimble-pike-489
briansrls Apr 29, 2026
3f4aef0
docs(briefs): split UnderRefined acceptance into Example 1 + Example 5
briansrls Apr 29, 2026
8f547b4
Merge remote-tracking branch 'origin/main' into session/nimble-pike-489
briansrls Apr 29, 2026
d61ba01
WIP: nimble-pike-489
briansrls Apr 29, 2026
1dd8aea
fix(grounding-lifetime): tie extraction C-8 to DeclarationId boundary…
briansrls Apr 29, 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
1 change: 1 addition & 0 deletions src/v3/compiler/src/bootstrap_generated.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2490,5 +2490,6 @@ pub(crate) fn bootstrapped_fixture_dag() -> Dag {
callable_strategy_variants: CallableStrategyVariants::default(),
clusters: vec![],
optional_match_disjs: HashMap::new(),
user_declaration_append_begin: 0,
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -2407,5 +2407,6 @@ pub(crate) fn bootstrapped_fixture_without_parse_surface_dag() -> Dag {
callable_strategy_variants: CallableStrategyVariants::default(),
clusters: vec![],
optional_match_disjs: HashMap::new(),
user_declaration_append_begin: 0,
}
}
1 change: 1 addition & 0 deletions src/v3/compiler/src/bootstrap_std_generated.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12413,5 +12413,6 @@ pub(crate) fn bootstrapped_std_fixture_dag() -> Dag {
callable_strategy_variants: CallableStrategyVariants::default(),
clusters: vec![],
optional_match_disjs: HashMap::new(),
user_declaration_append_begin: 0,
}
}
18 changes: 18 additions & 0 deletions src/v3/compiler/src/dag.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2358,6 +2358,10 @@ pub struct Dag {
/// inference needs stable `Some` / `None` variant identities without
/// promoting optionals into named top-level declarations.
optional_match_disjs: HashMap<DeclarationId, DeclarationId>,
/// First [`DeclarationId::raw`] value minted **after** the embedded bootstrap fixture
/// rows loaded at `Dag` construction (`lower` / `lower_into` append here; callers cannot
/// claim fixture provenance for these rows by stamping an authority-looking `span.file`).
user_declaration_append_begin: u32,

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: Adding a Dag field used by generated bootstrap struct literals without updating regen_bootstrap_emit.rs leaves the snapshots non-reproducible from their sole writer, violating Facts Flow Forward / pure-bootstrap single authority.

}

static BOOTSTRAPPED_DAG: LazyLock<Dag> = LazyLock::new(|| {
Expand All @@ -2366,6 +2370,7 @@ static BOOTSTRAPPED_DAG: LazyLock<Dag> = LazyLock::new(|| {
assert_bootstrap_fixture_paths_match_regen_keys(&dag);
dag.populate_primitive_cache();
crate::int_literal_ranges::validate_rust_pilot_integer_primitives(&mut dag);
dag.user_declaration_append_begin = dag.declarations.len() as u32;
dag
});

Expand All @@ -2376,6 +2381,7 @@ static BOOTSTRAPPED_STD_FIXTURE_DAG: LazyLock<Dag> = LazyLock::new(|| {
let mut dag = bootstrap_std_generated::bootstrapped_std_fixture_dag();
dag.mark_bootstrap_secret_nominal_opacity();
dag.populate_primitive_cache();
dag.user_declaration_append_begin = dag.declarations.len() as u32;
dag
});

Expand All @@ -2386,6 +2392,7 @@ static BOOTSTRAPPED_DAG_WITHOUT_PARSE_SURFACE_FIXTURE: LazyLock<Dag> = LazyLock:
assert_bootstrap_fixture_paths_match_regen_keys(&dag);
dag.populate_primitive_cache();
crate::int_literal_ranges::validate_rust_pilot_integer_primitives(&mut dag);
dag.user_declaration_append_begin = dag.declarations.len() as u32;
dag
});

Expand Down Expand Up @@ -2417,6 +2424,7 @@ impl Dag {
callable_strategy_variants: CallableStrategyVariants::default(),
clusters: Vec::new(),
optional_match_disjs: HashMap::new(),
user_declaration_append_begin: 0,
}
}

Expand Down Expand Up @@ -2470,6 +2478,16 @@ impl Dag {
self.primitives.string
}

/// Raw [`DeclarationId`] boundary between embedded bootstrap fixture rows and any
/// declarations minted afterward (`lower_into`, tests, etc.).
///
/// Lifetime extraction and similar consumers must **not** classify post-boundary rows as
/// “fixture authority” based on [`Declaration::span`] alone — callers can supply an
/// authority-*looking* `span.file` string without being part of the checked-in corpus.
pub fn declaration_append_boundary(&self) -> u32 {
self.user_declaration_append_begin
}

/// The std **scalar** `TypeShape` roots used to prune algebra / ring
/// `TypeConnective::Arrow` from the first-class-`fn` *data* walk in
/// `emit::rust_target` (`decl_includes_first_class_arrow_data` and related).
Expand Down
1 change: 1 addition & 0 deletions src/v3/compiler/src/regen_bootstrap_emit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -96,6 +96,7 @@ fn emit_bootstrap_module(dag: &Dag, function_name: &str) -> String {
&render_optional_match_disjs(dag),
2,
);
out.push_str(" user_declaration_append_begin: 0,\n");
out.push_str(" }\n");
out.push_str("}\n");
out
Expand Down
28 changes: 19 additions & 9 deletions src/v3/grounding_lifetime/src/extract.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,11 @@
//! so extraction returns an **empty** program (the structural fold is validated via
//! [`LifetimeProgram`] fixtures).
//!
//! Any **`data` or `fn` declaration** rooted in a **non-authority** source file (user
//! or test modules) is treated as load-bearing program surface we cannot project yet:
//! fail-closed per C-8 instead of returning `Ok(empty)` and dropping facts.
//! Any **`data` or `fn` declaration** minted **after** the embedded fixture snapshot
//! ([`Dag::declaration_append_boundary`]) is treated as load-bearing program surface we
//! cannot project yet — **even if** `span.file` looks like an authority path (callers
//! control the compile-time file string). Fail-closed per C-8 instead of returning
//! `Ok(empty)` and dropping facts.

use v3_compiler::dag::{Dag, TypeConnective};

Expand All @@ -21,6 +23,9 @@ use std::collections::BTreeMap;

/// Span roots that appear on [`Dag::new()`] bootstrap fixtures (regenerated snapshots).
///
/// Used only as **defense in depth** for rows with `DeclarationId::raw` **below**
/// [`Dag::declaration_append_boundary`]: those rows are expected to be corpus-only.
///
/// Keep aligned with `bootstrap_generated.rs` / `bootstrap_generated_without_parse_surface.rs`
/// when new fixture corpora land; otherwise user/test modules may be misclassified.
///
Expand All @@ -42,11 +47,9 @@ fn is_bootstrap_fixture_authority_source_file(file: &str) -> bool {
)
}

fn first_non_authority_lifetime_surface_declaration(dag: &Dag) -> Option<(String, String)> {
fn first_unextracted_lifetime_surface_declaration(dag: &Dag) -> Option<(String, String)> {
let boundary = dag.declaration_append_boundary();
for decl in dag.declarations() {
if is_bootstrap_fixture_authority_source_file(&decl.span.file) {
continue;
}
let surface =
decl.value_body.is_some() || matches!(&decl.connective, TypeConnective::Arrow { .. });
if !surface {
Expand All @@ -56,7 +59,14 @@ fn first_non_authority_lifetime_surface_declaration(dag: &Dag) -> Option<(String
.name
.clone()
.unwrap_or_else(|| format!("declaration#{}", decl.id.raw()));
return Some((name, decl.span.file.clone()));
let post_fixture = decl.id.raw() >= boundary;
if post_fixture {
return Some((name, decl.span.file.clone()));
}
if !is_bootstrap_fixture_authority_source_file(&decl.span.file) {
// Fixture-id range but not stamped like the embedded corpus — do not trust.
return Some((name, decl.span.file.clone()));
}
}
None
}
Expand All @@ -65,7 +75,7 @@ fn first_non_authority_lifetime_surface_declaration(dag: &Dag) -> Option<(String
///
/// Fail-closed on constructs the R2 analyzer does not model (once lowering surfaces them).
pub fn extract_lifetime_program(dag: &Dag) -> Result<LifetimeProgram, EmissionDiagnostic> {
if let Some((name, file)) = first_non_authority_lifetime_surface_declaration(dag) {
if let Some((name, file)) = first_unextracted_lifetime_surface_declaration(dag) {
return Err(EmissionDiagnostic::LifetimeProgramExtractionPending {
detail: format!("{name} ({file})"),
});
Expand Down
15 changes: 15 additions & 0 deletions src/v3/grounding_lifetime/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -165,6 +165,21 @@ mod tests {
}
}

/// `span.file` is caller-controlled; authority-looking paths must not bypass C-8.
#[test]
fn extract_fail_closed_when_user_code_uses_authority_looking_span_path() {
let source = "module spoof\n\nfn f() -> Int = 0\n";
let file = "dsl/std/user_spoof_under_extractor_test.dag";
let dag = v3_compiler::compile_to_dag(source, file).expect("compile");
let err = extract_lifetime_program(&dag).expect_err("must not Ok(empty) on spoof path");
match err {
EmissionDiagnostic::LifetimeProgramExtractionPending { detail } => {
assert!(detail.contains('f'), "unexpected detail: {detail}");
}
other => panic!("unexpected diagnostic: {other:?}"),
}
}

#[test]
fn function_param_indeterminate_growability_fails_closed_even_when_borrowed() {
let mut bindings = BTreeMap::new();
Expand Down
Loading