Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
29 commits
Select commit Hold shift + click to select a range
b216074
WIP: docs/briefs/t-substrate-nominal-opaque-secret-worker.md
briansrls Apr 25, 2026
9519c3c
WIP: docs/briefs/t-substrate-nominal-opaque-secret-worker.md
briansrls Apr 25, 2026
e726d62
chore: apply cargo fmt
briansrls Apr 25, 2026
c8bc824
fix(v3): refine pilot range text + name range-pair dissolution
briansrls Apr 25, 2026
b5081e8
WIP: docs/briefs/t-substrate-nominal-opaque-secret-worker.md
briansrls Apr 25, 2026
813499c
fix(v3): IntLit payload is IntLiteralMagnitude in token taxonomy
briansrls Apr 25, 2026
26c7a40
docs: note LiteralBits i128 comes from IntLiteralMagnitude, not Int o…
briansrls Apr 25, 2026
9be51b2
fix(v3): SurfaceLiteral int payload is IntLiteralMagnitude in .dag
briansrls Apr 25, 2026
0509720
chore(v3): ingest api-review — range authority docs, decide dead branch
briansrls Apr 25, 2026
85c46d7
WIP: docs/briefs/t-substrate-nominal-opaque-secret-worker.md
briansrls Apr 25, 2026
2469977
chore: apply cargo fmt
briansrls Apr 25, 2026
366dfd6
WIP: docs/briefs/t-substrate-nominal-opaque-secret-worker.md
briansrls Apr 25, 2026
db54d1a
chore: apply cargo fmt
briansrls Apr 25, 2026
89c9a14
WIP: docs/briefs/t-substrate-nominal-opaque-secret-worker.md
briansrls Apr 25, 2026
ab224a2
chore: apply cargo fmt
briansrls Apr 25, 2026
8903f97
chore: regen bootstrap + parse corpus manifest (substrate.dag span dr…
briansrls Apr 25, 2026
d72ae20
docs: note dissolution of extdeps/std integer range drift test
briansrls Apr 25, 2026
00e46e0
test+docs: rebut extdeps range fields (PilotIntegerRangeBound, not St…
briansrls Apr 25, 2026
b1e9d7b
WIP: docs/briefs/t-substrate-nominal-opaque-secret-worker.md
briansrls Apr 25, 2026
ffde495
fix(v3): mirror MagnitudeOutOfRange in std diagnostic DAGs
briansrls Apr 25, 2026
16a1443
docs(v3): name T-Lens-LiteralIntAtI128 for i64-only literal_int_at
briansrls Apr 25, 2026
55dd9f5
WIP: t-substrate-nominal-opaque
briansrls Apr 25, 2026
753124e
WIP: t-substrate-nominal-opaque
briansrls Apr 25, 2026
3d28a8d
chore(ci): retrigger workflow after parse_generated IntLit u128 sync
briansrls Apr 25, 2026
9b74a50
WIP: t-substrate-nominal-opaque
briansrls Apr 25, 2026
33bf450
fix(v3): refresh bootstrap and corpus manifest for UnsignedLiteralDig…
briansrls Apr 25, 2026
3f219d5
fix(v3): anchor integer_range pilot ratchet on RUST_PILOT_PRIMITIVES
briansrls Apr 25, 2026
7c484c7
Merge remote-tracking branch 'origin/main' into session/zesty-ram-745
briansrls Apr 25, 2026
849f4e9
Merge remote-tracking branch 'origin/main' into session/zesty-ram-745
briansrls Apr 25, 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 Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

35 changes: 27 additions & 8 deletions dsl/extdeps/languages/rust/primitives.dag
Original file line number Diff line number Diff line change
Expand Up @@ -66,11 +66,22 @@
// object is the canonical inhabitant. Pilot uses the sentinel pair
// because cardinality-substrate is not yet available (out-of-scope
// per brief: "Container types — block on cardinality-substrate.").
// 4. `range_min_inclusive` / `range_max_inclusive` use
// `std.types.PilotIntegerRangeBound` (refined `String`, base-10 numerals
// only) so arbitrary text is not silently admissible. The refinement
// does not yet express `min <= max` or i128 witnessability of the
// closed interval — those illegal states are excluded by **host
// invariants** (`v3_grounding_pilot` unit test) until the engine walks
// `data` with full predicate discharge. **Named dissolution:**
// **T-Ground-PilotRangePairWitness** — closed interval + ordering as
// substrate-first-class facts (carrier-native or std.natural once
// modeled), per Illegal-States-Unrepresentable at the graph boundary.

module extdeps.languages.rust.primitives

import std.algebra { OrderedRing, Semiring, BooleanAlgebra }
import std.bit { Bit, Byte, Word16, Word32, Word64 }
import std.types { PilotIntegerRangeBound }


// =========================================================================
Expand Down Expand Up @@ -177,6 +188,14 @@ type RustPrimitive
carrier: TargetCarrier
is_copy: Bool
overflow: IntegerOverflow
// Inclusive range endpoints (R2). `std.types.PilotIntegerRangeBound` is a
// `String` refined to base-10 numeral form; that predicate is **not** lowered
// in the bootstrap graph yet, so the graph boundary is not fail-closed here.
// **Host (v3_grounding_pilot):** the mirror and unit tests lock base-10 shape,
// i128 parse, and `min <= max` for `rust_pilot_primitives` data until
// **T-Ground-PilotRangePairWitness** lands in substrate.
range_min_inclusive: PilotIntegerRangeBound
range_max_inclusive: PilotIntegerRangeBound
}

This comment was marked as resolved.

| NonIntegerPrimitive {
target_name: String // Rust syntactic token: "bool", "()"
Expand All @@ -199,33 +218,33 @@ 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
10 changes: 10 additions & 0 deletions dsl/std/types.dag
Original file line number Diff line number Diff line change
Expand Up @@ -244,6 +244,16 @@ type SecretName = String where non_empty
type PositiveInt = Int where range(min: 1)
type NonNegativeInt = Int where range(min: 0)

// T-Ground / R2: base-10 integer *numeral* text for Rust pilot range bounds
// (`dsl/extdeps/languages/rust/primitives.dag`). Rejects non-numeral garbage.
// Does not prove `min <= max` or i128-closed intervals — that pair witness
// stays host-tested until **T-Ground-PilotRangePairWitness** dissolves it into
// carrier-native bounds (see extdeps file Substrate-gap flag #4). The `where
// pattern(...)` text itself: **T-Ground-PilotRangeBoundPredicateLower** in
// generated `bootstrap_*.rs` (placeholder: predicate not lowered until
// that trigger lands; host mirrors close `rust_pilot_primitives` today).
type PilotIntegerRangeBound = String where pattern("^[-+]?[0-9]+$")

// Path modeling (EX-2):
// - FilePath remains a compatibility alias for existing modules.
// - FilePathParts and GlobPattern provide structured forms for new DSL code.
Expand Down
13 changes: 12 additions & 1 deletion scripts/regen_runtime_mirrors.py
Original file line number Diff line number Diff line change
Expand Up @@ -610,10 +610,14 @@ def rust_type(source: str, overrides: dict[str, str] | None = None) -> str:
overrides = overrides or {}
if source in overrides:
return overrides[source]
# Literal carriers: also wired in v3 `regen_tokenize` `rust_type_for_decl_id` — one width
# for both (see T-Substrate-IntLiteralMagnitudeRustI128; same dissolution bucket).
mapping = {
"String": "String",
"Bool": "bool",
"Int": "i64",
"IntLiteralMagnitude": "i128",
"UnsignedLiteralDigitMagnitude": "u128",
"NodeId": "NodeId",
"PortId": "PortId",
"ClusterId": "ClusterId",
Expand Down Expand Up @@ -731,7 +735,10 @@ def render_parse_surface_sum(name: str, variants: list[VariantDef]) -> str:
if variant.kind == "unit":
lines.append(f" {variant.name},")
elif variant.kind == "tuple":
lines.append(f" {variant.name}({rust_type(variant.payload)}),")
# `rust_type` maps substrate names (e.g. `IntLiteralMagnitude` -> i128);
# no per-variant overrides — parse_surface.dag must name the same carriers as substrate.
rust_tuple_ty = rust_type(variant.payload)
lines.append(f" {variant.name}({rust_tuple_ty}),")
elif variant.kind == "record":
lines.append(f" {variant.name} {{")
for label, ty in variant.fields or []:
Expand Down Expand Up @@ -776,6 +783,10 @@ def render_parse_surface_module(records: dict[str, RecordDef], sums: dict[str, l

def render_dag_scalar_module(records: dict[str, RecordDef], sums: dict[str, list[VariantDef]]) -> str:
parts = [
# LiteralBits: `substrate.dag` uses `LitInt(IntLiteralMagnitude)` — not `Int`.
# The i128 width comes from `rust_type()["IntLiteralMagnitude"]` (see mapping
# in `rust_type`). Do **not** reintroduce `overrides={"Int": "i128"}` here; that
# would desync the mirror from the DAG payload name (single authority + FFF).
render_sum(
"LiteralBits",
sums["LiteralBits"],
Expand Down
2 changes: 2 additions & 0 deletions src/v2/stage0/src/std_types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -219,6 +219,8 @@ pub type PositiveInt = i64;

pub type NonNegativeInt = i64;

pub type PilotIntegerRangeBound = String;

pub type PathSegment = String;

pub type GlobSegment = String;
Expand Down
4 changes: 4 additions & 0 deletions src/v3/compiler/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,10 @@ bootstrap-regen-fresh = []
libc = { version = "0.2", default-features = false }

[dev-dependencies]
# `integer_range` tests: decimal range strings must come from
# `v3_grounding_pilot::RUST_PILOT_PRIMITIVES` (drift catch vs hardcoded test rows; see
# T-Ground-IntegerRangeSingleAuthority in `src/integer_range.rs`).
v3-grounding-pilot = { path = "../grounding_pilot" }
# Interpreter-backed receipts for substrate behavior (repeat_string, etc.).
v2-compiler = { path = "../../v2/stage0" }
v2-compiler-tests = { path = "../../v2/tests" }
Expand Down
105 changes: 101 additions & 4 deletions src/v3/compiler/parse_parser_body.txt
Original file line number Diff line number Diff line change
Expand Up @@ -1189,7 +1189,101 @@ impl<'a> Parser<'a> {
}
}

/// The tokenizer records each integer as an **unsigned** decimal magnitude
/// (`u128`); the signed i128 value is only fixed here, after unary `-`.
/// This keeps `|i128::MIN|` in range (2^127 is not representable as a positive
/// `i128` token, but fits in `u128` until negation).
fn i128_from_int_literal_magnitude(
&self,
mag: u128,
is_negative: bool,
err_span: SourceSpan,
) -> Result<i128, Diagnostic> {
const I128_MAX_U: u128 = i128::MAX as u128;
const I128_MIN_ABS: u128 = 1u128 << 127;
if is_negative {
if mag == I128_MIN_ABS {
return Ok(i128::MIN);
}
if mag > I128_MAX_U {
return Err(Diagnostic::ParseError {
message: "this integer literal cannot be negated without overflow".to_string(),
span: err_span,
fixes: Vec::new(),
});
}
return (mag as i128).checked_neg().ok_or_else(|| Diagnostic::ParseError {
message: "this integer literal cannot be negated (overflow)".to_string(),
span: err_span,
fixes: Vec::new(),
});
}
if mag > I128_MAX_U {
return Err(Diagnostic::ParseError {
message: if mag == I128_MIN_ABS {
"this unsigned literal is out of range for i128; write the minimum with \
unary `-` and the same digits"
.to_string()
} else {
"this integer literal is out of range for i128".to_string()
},
span: err_span,
fixes: Vec::new(),
});
}
Ok(mag as i128)
}

fn parse_primary(&mut self) -> Result<SurfaceExpr, Diagnostic> {
// Unary minus for integer magnitudes: lives in *this* file; `regen_parse`
// splices the fragment into `parse_generated.rs` (do not edit only the .rs).
if matches!(self.peek().kind, TokenKind::Minus) {
let minus = self.bump().clone();
if let TokenKind::IntLit(mag) = &self.peek().kind {
let mag = *mag;
let int_tok = self.bump().clone();
let full = SourceSpan::new(
self.file,
minus.span.byte_start,
int_tok.span.byte_end,
);
let v = self.i128_from_int_literal_magnitude(mag, true, full.clone())?;
return Ok(SurfaceExpr::Literal {
value: SurfaceLiteral::Int(v),
span: full,
});
}
let inner = self.parse_primary()?;
return match inner {
SurfaceExpr::Literal {
value: SurfaceLiteral::Int(n),
span: inner_span,
} => {
let v = n.checked_neg().ok_or_else(|| Diagnostic::ParseError {
message: "this integer literal cannot be negated (overflow)".to_string(),
span: SourceSpan::new(
self.file,
minus.span.byte_start,
inner_span.byte_end,
),
fixes: Vec::new(),
})?;
Ok(SurfaceExpr::Literal {
value: SurfaceLiteral::Int(v),
span: SourceSpan::new(
self.file,
minus.span.byte_start,
inner_span.byte_end,
),
})
}
_ => Err(Diagnostic::ParseError {
message: "unary `-` is only valid before an integer literal".to_string(),
span: minus.span,
fixes: Vec::new(),
}),
};
}
let peek = &self.peek().kind;
match primary_prefix_dispatch(peek) {
Some(PrimaryPrefixDispatch::If) => return self.parse_if(),
Expand All @@ -1205,10 +1299,13 @@ impl<'a> Parser<'a> {
fixes: Vec::new(),
})?;
match (cls, token.kind) {
(PrimaryAtomClass::IntLiteral, TokenKind::IntLit(value)) => Ok(SurfaceExpr::Literal {
value: SurfaceLiteral::Int(value),
span: token.span,
}),
(PrimaryAtomClass::IntLiteral, TokenKind::IntLit(mag)) => {
let v = self.i128_from_int_literal_magnitude(mag, false, token.span.clone())?;
Ok(SurfaceExpr::Literal {
value: SurfaceLiteral::Int(v),
span: token.span,
})
}
(PrimaryAtomClass::True, TokenKind::KwTrue) => Ok(SurfaceExpr::Literal {
value: SurfaceLiteral::Bool(true),
span: token.span,
Expand Down
13 changes: 11 additions & 2 deletions src/v3/compiler/src/bin/regen_tokenize.rs
Original file line number Diff line number Diff line change
Expand Up @@ -293,12 +293,17 @@ fn emit_token_kind_enum(dag: &Dag) -> String {
lines.join("\n")
}

// P2: literal-magnitude `substrate` name → Rust width matches `rust_type()` in
// `scripts/regen_runtime_mirrors.py` (T-Substrate-IntLiteralMagnitudeRustI128, etc.); keep
// the two regen entry points in sync.
fn rust_type_for_decl_id(dag: &Dag, id: DeclarationId) -> String {
let decl = dag.declaration(id);
if let Some(name) = &decl.name {
match name.as_str() {
"String" => return "String".to_string(),
"Int" | "Int64" => return "i64".to_string(),
"IntLiteralMagnitude" => return "i128".to_string(),
"UnsignedLiteralDigitMagnitude" => return "u128".to_string(),
_ => {}
}
}
Expand All @@ -314,6 +319,8 @@ fn rust_type_for_decl_id(dag: &Dag, id: DeclarationId) -> String {
match template_decl.name.as_deref() {
Some("String") => "String".to_string(),
Some("Int") | Some("Int64") => "i64".to_string(),
Some("IntLiteralMagnitude") => "i128".to_string(),
Some("UnsignedLiteralDigitMagnitude") => "u128".to_string(),
other => panic!("unsupported instantiated type {other:?}"),
}
}
Expand Down Expand Up @@ -656,7 +663,9 @@ fn extract_int_field(fields: &[(String, FieldValue)], key: &str) -> i64 {
.find_map(|(k, v)| (k == key).then_some(v))
.unwrap_or_else(|| panic!("missing field {key}"));
match fv {
FieldValue::Literal(v3_compiler::dag::LiteralBits::Int(n)) => *n,
FieldValue::Literal(v3_compiler::dag::LiteralBits::Int(n)) => {
i64::try_from(*n).expect("string escape codepoint out of i64 for tokenizer")
}
_ => panic!("field {key}: expected int literal"),
}
}
Expand Down Expand Up @@ -741,7 +750,7 @@ fn emit_tokenize_fn(
s.push_str(" }\n");

This comment was marked as resolved.

s.push_str(" let literal = &source[start..end];\n");
s.push_str(
" let value: i64 = literal.parse().map_err(|_| Diagnostic::TokenizerError {\n",
" let value: u128 = literal.parse().map_err(|_| Diagnostic::TokenizerError {\n",
);
s.push_str(&format!(
" message: format!(\"{{}}{{}}{{}}\", {}, literal, {}),\n",
Expand Down
3,806 changes: 1,907 additions & 1,899 deletions src/v3/compiler/src/bootstrap_generated.rs

Large diffs are not rendered by default.

3,640 changes: 1,824 additions & 1,816 deletions src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs

Large diffs are not rendered by default.

Loading
Loading