Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
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
34 changes: 26 additions & 8 deletions dsl/extdeps/languages/rust/primitives.dag
Original file line number Diff line number Diff line change
Expand Up @@ -177,6 +177,16 @@ type RustPrimitive
carrier: TargetCarrier
is_copy: Bool
overflow: IntegerOverflow
// Inclusive magnitude range as decimal-encoded String. String-decimal
// (not Int / Int64) is a deliberate width-independence bridge: u64's max
// (2^64-1) does not fit i64, so binding the range carrier to the literal
// payload (currently i64 per substrate `LitInt(Int)`) would force
// truncation or omission. Reconciliation parses both bounds and the
// literal magnitude into a host comparison space (i128). Bridge dissolves
// when a typed unbounded magnitude carrier (std.natural / Int128 sub-lane)
// lands and both bounds + literal payload migrate to it.
range_min_inclusive: String
range_max_inclusive: String
}
| NonIntegerPrimitive {
target_name: String // Rust syntactic token: "bool", "()"
Expand All @@ -199,33 +209,41 @@ data rust_pilot_primitives: List<RustPrimitive> = [
// OrderedRing). Wrap is the release-mode semantics.

IntegerPrimitive { target_name: "i8", algebra: OrderedRingAlgebra, carrier: ByteCarrier,
is_copy: true, overflow: TwoComplementWrap },
is_copy: true, overflow: TwoComplementWrap,
range_min_inclusive: "-128", range_max_inclusive: "127" },

IntegerPrimitive { target_name: "i16", algebra: OrderedRingAlgebra, carrier: Word16Carrier,
is_copy: true, overflow: TwoComplementWrap },
is_copy: true, overflow: TwoComplementWrap,
range_min_inclusive: "-32768", range_max_inclusive: "32767" },

IntegerPrimitive { target_name: "i32", algebra: OrderedRingAlgebra, carrier: Word32Carrier,
is_copy: true, overflow: TwoComplementWrap },
is_copy: true, overflow: TwoComplementWrap,
range_min_inclusive: "-2147483648", range_max_inclusive: "2147483647" },

IntegerPrimitive { target_name: "i64", algebra: OrderedRingAlgebra, carrier: Word64Carrier,
is_copy: true, overflow: TwoComplementWrap },
is_copy: true, overflow: TwoComplementWrap,
range_min_inclusive: "-9223372036854775808", range_max_inclusive: "9223372036854775807" },


// -- Unsigned integers : Semiring over machine-word carriers -----------
// Rust Reference §3.4. unsigned = no additive inverse (no negate in
// Semiring). Distinguished from signed by algebra tag, not by carrier.

IntegerPrimitive { target_name: "u8", algebra: SemiringAlgebra, carrier: ByteCarrier,
is_copy: true, overflow: TwoComplementWrap },
is_copy: true, overflow: TwoComplementWrap,
range_min_inclusive: "0", range_max_inclusive: "255" },

IntegerPrimitive { target_name: "u16", algebra: SemiringAlgebra, carrier: Word16Carrier,
is_copy: true, overflow: TwoComplementWrap },
is_copy: true, overflow: TwoComplementWrap,
range_min_inclusive: "0", range_max_inclusive: "65535" },

IntegerPrimitive { target_name: "u32", algebra: SemiringAlgebra, carrier: Word32Carrier,
is_copy: true, overflow: TwoComplementWrap },
is_copy: true, overflow: TwoComplementWrap,
range_min_inclusive: "0", range_max_inclusive: "4294967295" },

IntegerPrimitive { target_name: "u64", algebra: SemiringAlgebra, carrier: Word64Carrier,
is_copy: true, overflow: TwoComplementWrap },
is_copy: true, overflow: TwoComplementWrap,
range_min_inclusive: "0", range_max_inclusive: "18446744073709551615" },


// -- Bool : BooleanAlgebra over Bit -----------------------------------
Expand Down
988 changes: 495 additions & 493 deletions src/v3/compiler/src/bootstrap_generated.rs

Large diffs are not rendered by default.

798 changes: 400 additions & 398 deletions src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs

Large diffs are not rendered by default.

40 changes: 38 additions & 2 deletions src/v3/compiler/src/diagnostics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -185,6 +185,31 @@ pub enum Diagnostic {
span: SourceSpan,
fixes: Vec<Correction>,
},
/// An integer literal's magnitude does not fit the call-site's
/// expected target algebra range. Emitted at lowering time when a
/// `data x: T = N` (or equivalent binding-context literal) is
/// recognized as an integer-target primitive whose declared
/// inclusive range excludes the literal.
///
/// `target_name` is the std-side declaration name (e.g. `UInt8`);
/// `target_min` / `target_max` are the substrate-declared inclusive
/// bounds (decimal-encoded in primitives.dag, parsed and re-rendered
/// for the user). `magnitude` is the literal value as authored.
///
/// Bridge note: bounds are mirrored into the compiler from
/// `dsl/extdeps/languages/rust/primitives.dag` (read by the pilot,
/// not yet by the production walker — `value_body` for the data
/// declaration is `Unparsed` until the top-level `ValueBody::List`
/// substrate sub-lane lands). Once the walker reads the .dag value
/// directly, the in-compiler mirror in `lower.rs` dissolves.
MagnitudeOutOfRange {
target_name: String,
magnitude: i128,
target_min: i128,
target_max: i128,
span: SourceSpan,
fixes: Vec<Correction>,
},
}

impl Diagnostic {
Expand All @@ -196,7 +221,8 @@ impl Diagnostic {
| Diagnostic::ArityMismatch { span, .. }
| Diagnostic::ResolveError { span, .. }
| Diagnostic::UnitMismatch { span, .. }
| Diagnostic::BranchConditionNotBool { span, .. } => span,
| Diagnostic::BranchConditionNotBool { span, .. }
| Diagnostic::MagnitudeOutOfRange { span, .. } => span,
}
}

Expand All @@ -208,7 +234,8 @@ impl Diagnostic {
| Diagnostic::ArityMismatch { fixes, .. }
| Diagnostic::ResolveError { fixes, .. }
| Diagnostic::UnitMismatch { fixes, .. }
| Diagnostic::BranchConditionNotBool { fixes, .. } => fixes,
| Diagnostic::BranchConditionNotBool { fixes, .. }
| Diagnostic::MagnitudeOutOfRange { fixes, .. } => fixes,
}
}

Expand Down Expand Up @@ -240,6 +267,15 @@ impl Diagnostic {
Some(ty) => format!("branch condition port is not Bool (got {ty:?})"),
None => "branch condition port is not Bool (type not resolved)".to_string(),
},
Diagnostic::MagnitudeOutOfRange {
target_name,
magnitude,
target_min,
target_max,
..
} => format!(
"literal magnitude {magnitude} is out of range for `{target_name}` (inclusive range [{target_min}, {target_max}]); use a wider integer type"
),
}
}
}
Expand Down
149 changes: 141 additions & 8 deletions src/v3/compiler/src/lower.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2426,21 +2426,69 @@ fn lower_data_item(
lower_record_to_structural(name, fields, ty_decl_id, body_span, symbols, dag)
}
Some(lit_expr @ SurfaceExpr::Literal { .. }) => {
lower_scalar_literal_for_type(lit_expr, ty_decl_id, dag)
.map(crate::dag::ValueBody::Scalar)
.or_else(|| {
// Magnitude-aware narrowing for integer literals at the
// data-binding boundary. If the declared type walks to a
// narrower integer std type than `Int` (Int8/Int16/Int32/
// UInt8/UInt16/UInt32/UInt64), check the literal magnitude
// against the substrate-declared inclusive range and emit a
// structured `MagnitudeOutOfRange` diagnostic if the literal
// does not fit. Default-when-unconstrained: a literal with
// declared type `Int` (= Int64 = OrderedRing<Word64>)
// continues to accept any i64 — that default is itself a
// host-narrowing heuristic this lane otherwise dissolves;
// its own dissolution belongs to the typed unbounded
// magnitude carrier sub-lane (deferred).
let int_lit_magnitude: Option<i64> = match lit_expr {
SurfaceExpr::Literal {
value: SurfaceLiteral::Int(m),
..
} => Some(*m),
_ => None,
};
let narrowing = int_lit_magnitude
.and_then(|m| integer_target_range(dag, ty_decl_id).map(|r| (m, r)));
if let Some((magnitude, (target_name, target_min, target_max))) = narrowing {
let m: i128 = i128::from(magnitude);
if m < target_min || m > target_max {
report_declaration_error(
dag,
Diagnostic::ResolveError {
name: format!(
"data `{name}`'s scalar body does not match declared type",
),
Diagnostic::MagnitudeOutOfRange {
target_name,
magnitude: m,
target_min,
target_max,
span: body_span.clone(),
fixes: Vec::new(),
},
);
None
})
} else {
// Narrow types (Int8..UInt64) do NOT walk to `Int`, so
// `lower_scalar_literal_for_type`'s walks_to(Int) check
// would reject them and silently drop the body to
// Unparsed. Construct the carrier directly: magnitude
// already fits per the bound check above, and the
// narrow target type is exactly what `integer_target_range`
// identified by name.
Some(crate::dag::ValueBody::Scalar(LiteralBits::Int(magnitude)))
}
} else {
lower_scalar_literal_for_type(lit_expr, ty_decl_id, dag)
.map(crate::dag::ValueBody::Scalar)
.or_else(|| {
report_declaration_error(
dag,
Diagnostic::ResolveError {
name: format!(
"data `{name}`'s scalar body does not match declared type",
),
span: body_span.clone(),
fixes: Vec::new(),
},
);
None
})
}
}
_ => None,
};
Expand Down Expand Up @@ -3149,6 +3197,91 @@ fn lower_structural_field_value(
None
}

/// In-compiler mirror of the `range_min_inclusive` /
/// `range_max_inclusive` substrate facts authored on `IntegerPrimitive`
/// in `dsl/extdeps/languages/rust/primitives.dag`. Keyed by std-side
/// integer-type declaration name (Int8..UInt64) — the names that
/// appear in user type annotations like `data x: UInt8 = 256`.
///
/// **Why a mirror, not a substrate read.** The production compiler does
/// load `primitives.dag` (via `EXTDEPS_BOOTSTRAP_FIXTURES`), but the
/// `rust_pilot_primitives` data declaration's `value_body` is
/// `ValueBody::Unparsed` because v3 lacks a top-level
/// `ValueBody::List`/aggregate variant — the same gap flagged on
/// `dag.rust_pilot_primitives()` (`dag.rs:2825-2848`). Until the
/// R2 T-Substrate top-level `ValueBody::List` sub-lane lands, no
/// production walker can read the declared field values, so the
/// compiler mirrors them in Rust here.
///
/// **Dissolution trigger.** When `ValueBody::List` lands and a walker
/// can read the 10-element pilot enumeration, this map is replaced by
/// a substrate-walking helper that returns ranges directly from the
/// `IntegerPrimitive` `range_min_inclusive` / `range_max_inclusive`
/// fields. Both the grounding-pilot Rust mirror in
/// `src/v3/grounding_pilot/src/lib.rs` and this map dissolve together.
///
/// **Second substrate fact required at dissolution.** `ValueBody::List`
/// alone is necessary but not sufficient. The pilot's range facts are
/// keyed by the *Rust target name* (`"i8"`/`"u8"`/…) on
/// `IntegerPrimitive`, but this narrowing keys by the *std-side*
/// declaration name (`"Int8"`/`"UInt8"`/…) the user wrote. A
/// substrate-walking helper still needs the std↔target correspondence
/// (e.g. `Int8 = OrderedRing<Byte>` ↔ `IntegerPrimitive { algebra:
/// OrderedRingAlgebra, carrier: ByteCarrier, target_name: "i8" }`).
/// That correspondence today lives in the grounding-pilot's
/// `dag_type_facts` mapping; the production-walker version reads it
/// from the algebra/carrier match (the homomorphism the pilot probe
/// validated). Future reader: do not assume `ValueBody::List` alone
/// unblocks dissolution — the routing fact must also be substrate-
/// read.
///
/// **Default-when-unconstrained.** `Int` (alias to `Int64`) and `UInt`
/// (alias to `UInt64`) are deliberately omitted: literals declared at
/// those alias names accept any tokenizer-parseable `i64`, matching
/// pre-narrowing behavior (the lane's tracked-follow-up is to dissolve
/// that default once the typed unbounded magnitude carrier sub-lane
/// lifts the literal payload above i64).
fn integer_target_range(dag: &Dag, expected_type: DeclarationId) -> Option<(String, i128, i128)> {
let mut current = expected_type;
// 32-hop bound: defensive cycle-stop matching the analogous walk in
// `walks_to` (this file, ~3550). Real alias chains in std/ are 1-2
// hops (e.g. `Int = Int64 = OrderedRing<Word64>`); 32 is the
// already-established invariant used by the sibling helper, so
// alias-chain walks across the lowering codebase share one bound.
for _ in 0..32 {
let decl = dag.declaration(current);
if let Some(name) = &decl.name {
let bounds: Option<(i128, i128)> = match name.as_str() {
"Int8" => Some((-128, 127)),
"Int16" => Some((-32_768, 32_767)),
"Int32" => Some((-2_147_483_648, 2_147_483_647)),
"UInt8" => Some((0, 255)),
"UInt16" => Some((0, 65_535)),
"UInt32" => Some((0, 4_294_967_295)),
"UInt64" => Some((0, 18_446_744_073_709_551_615_i128)),
_ => None,
};
if let Some((min, max)) = bounds {
return Some((name.clone(), min, max));
}
}
match &decl.connective {
TypeConnective::Atom(AtomPayload::ResolvedByStructure(next))
| TypeConnective::Atom(AtomPayload::ResolvedByName(next)) => {
current = *next;
}
// Type aliases (`type Tiny = UInt8`) lower through
// Instantiation; follow the template so aliased forms
// narrow consistently with direct ones.
TypeConnective::Instantiation { template, .. } => {
current = *template;
}
_ => return None,
Comment on lines +3269 to +3279

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P2 Badge Traverse instantiation aliases in integer_target_range

integer_target_range only follows ResolvedByStructure/ResolvedByName links and returns None for other connectives, but type aliases lower through TypeConnective::Instantiation. As a result, alias forms like type Tiny = UInt8; data x: Tiny = 256 do not resolve to the underlying integer primitive here and skip MagnitudeOutOfRange, creating inconsistent overflow diagnostics between direct and aliased type annotations.

Useful? React with 👍 / 👎.

}
}
None
}

fn lower_scalar_literal_for_type(
expr: &SurfaceExpr,
expected_type: DeclarationId,
Expand Down
12 changes: 12 additions & 0 deletions src/v3/compiler/src/regen_bootstrap_emit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -652,6 +652,18 @@ fn render_diagnostic(diagnostic: &Diagnostic) -> String {
render_source_span(span),
render_corrections(fixes),
),
Diagnostic::MagnitudeOutOfRange {
target_name,
magnitude,
target_min,
target_max,
span,
fixes,
} => format!(
"Diagnostic::MagnitudeOutOfRange {{ target_name: {target_name:?}.to_string(), magnitude: {magnitude}_i128, target_min: {target_min}_i128, target_max: {target_max}_i128, span: {}, fixes: {} }}",
render_source_span(span),
render_corrections(fixes),
),
}
}

Expand Down
1 change: 1 addition & 0 deletions src/v3/compiler/src/test_runner.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2327,6 +2327,7 @@ fn diagnostic_kind(diagnostic: &Diagnostic) -> &'static str {
Diagnostic::ArityMismatch { .. } => "ArityMismatch",
Diagnostic::ResolveError { .. } => "ResolveError",
Diagnostic::BranchConditionNotBool { .. } => "BranchConditionNotBool",
Diagnostic::MagnitudeOutOfRange { .. } => "MagnitudeOutOfRange",
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -72,8 +72,19 @@ fn dag_new_exposes_rust_pilot_primitives_type_structure() {
};
assert_eq!(
integer_field_labels,
vec!["target_name", "algebra", "carrier", "is_copy", "overflow"],
"IntegerPrimitive field order is load-bearing for T-Ground L4-(C) witness consumption"
vec![
"target_name",
"algebra",
"carrier",
"is_copy",
"overflow",
"range_min_inclusive",
"range_max_inclusive",
],
"IntegerPrimitive field order is load-bearing for T-Ground L4-(C) witness \
consumption; range_{{min,max}}_inclusive added by R2 T-Substrate cardinality- \
for-int-lit sub-lane (String-decimal width-independence bridge — dissolves to a \
typed unbounded magnitude carrier when std.natural / Int128 sub-lane lands)"
);

let non_integer_variant = dag.declaration(variants[1].ty);
Expand Down
2 changes: 2 additions & 0 deletions src/v3/compiler/tests/integration/m1_5_testgen_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -460,6 +460,7 @@ fn diagnostic_kind(diag: &Diagnostic) -> &'static str {
Diagnostic::ArityMismatch { .. } => "ArityMismatch",
Diagnostic::ResolveError { .. } => "ResolveError",
Diagnostic::BranchConditionNotBool { .. } => "BranchConditionNotBool",
Diagnostic::MagnitudeOutOfRange { .. } => "MagnitudeOutOfRange",
}
}

Expand All @@ -480,6 +481,7 @@ fn diagnostic_detail(diag: &Diagnostic) -> String {
Diagnostic::UnitMismatch { .. } => diag.message(),
Diagnostic::ResolveError { name, .. } => name.clone(),
Diagnostic::BranchConditionNotBool { .. } => diag.message(),
Diagnostic::MagnitudeOutOfRange { .. } => diag.message(),
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -86,6 +86,7 @@ fn bootstrap_loads_verification_authority_types() {
(String::from("UnitMismatch"), Vec::new()),
(String::from("ArityMismatch"), Vec::new()),
(String::from("ResolveError"), Vec::new()),
(String::from("MagnitudeOutOfRange"), Vec::new()),
]
);
assert_eq!(
Expand Down
Loading
Loading