Skip to content

XL-2 named Nat/Int decimal conversions (#13436 fixed, folded onto v1-closeout) #13668

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
gunbai-bot merged 5 commits into from
Oct 10, 2026
Merged

XL-2 named Nat/Int decimal conversions (#13436 fixed, folded onto v1-closeout) #13668

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
0f14618
Merge origin/main into session/deep-newt-14-conv
Oct 9, 2026
82da0e4
Close the post-main census: drop the Map interpolation hole, concat t…
Oct 9, 2026
1eb675f
Merge remote-tracking branch 'origin/session/deep-newt-14-conv' into …
Oct 10, 2026
7749d8b
decimal_digit_of_units: construct the units digit via the successor t…
Oct 10, 2026
df9e66d
Regenerate std_integer stage0 mirror (remote required-regen candidate)
Oct 10, 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
2 changes: 1 addition & 1 deletion dag/gunbc/product/spatial_dimension.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -154,6 +154,6 @@ fn render_wire(dimension: RoomDimensionKnowledge) -> String {
RenderHypothesis { value: v, purpose: _ } =>
"<line class={style} data-mm={nat_to_decimal_string(value: millimeter_count(m: v))}/>"
RenderUnknown { obligation: o } =>
"<obligation class={style} data-survey={o as String}/>"
concat("<obligation class=", concat(style, concat(" data-survey=", concat(o as String, "/>"))))
}
}
44 changes: 16 additions & 28 deletions dag/std/integer.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ module std.integer
import std.optional { Absent, Present }

import std.algebra { AbelianGroup, GroupCompletion }
import std.nat { Nat, DecimalDigit, D0, D1, D2, D3, D4, D5, D6, D7, D8, D9, decimal_digit_value, decimal_digit_glyph }
import std.nat { Nat, DecimalDigit, D0, D1, D2, D3, D4, D5, D6, D7, D8, D9, decimal_digit_value, decimal_digit_glyph, decimal_digit_successor, DecimalDigitNext, DecimalDigitCarry }
import std.machine_constraints { Compose, MachineWidth, PointerWidth }
import std.measure { bit_width, bit_width_count, bits_per_byte }
import std.induction { int_pow_bounded }
Expand Down Expand Up @@ -240,43 +240,31 @@ fn uint8_channel_inclusive_max_value_derived() -> Int? {

// THE UNITS DIGIT OF A MACHINE INTEGER'S MAGNITUDE, for EVERY Int. A value of ten or more steps
// down by ten and a value below minus nine steps up by ten (neither step changes the units digit of
// the magnitude), a value in minus nine to minus one is negated (no overflow: its magnitude is at
// most nine), so the selection below receives exactly 0..9 and its final arm is the digit 9, never
// a default for an out-of-range value. Selection is by the one value table, std.nat
// decimal_digit_value, so no second table of digit values exists.
// the magnitude), so the walk below receives only -9..9.
// The digit is CONSTRUCTED, never looked up: zero is D0 and each unit above it advances the digit
// through the one successor table in std.nat (a carry out of D9 wraps to D0, which IS the units
// digit of ten), and a value in -9..-1 is its own negation's digit (no overflow: its magnitude is
// at most nine). No Int-to-digit selection exists to be out of range and no default arm exists to
// answer one (DESIGN section 5: a failure arm must refuse, never widen; section 4b: construction
// over validation) -- -1 is D1, 9 is D9, 10 is D0, 99 is D9, each by derivation.
fn decimal_digit_of_units(value: Int) -> DecimalDigit {
if value >= 10 {
decimal_digit_of_units(value: value - 10)
} else if value < -9 {
decimal_digit_of_units(value: value + 10)
} else if value < 0 {
decimal_digit_of_reduced_units(value: 0 - value)
decimal_digit_of_units(value: 0 - value)
} else if value == 0 {
D0
} else {
decimal_digit_of_reduced_units(value: value)
decimal_digit_advance(d: decimal_digit_of_units(value: value - 1))
}
}

fn decimal_digit_of_reduced_units(value: Int) -> DecimalDigit {
if decimal_digit_value(d: D0) == value {
D0
} else if decimal_digit_value(d: D1) == value {
D1
} else if decimal_digit_value(d: D2) == value {
D2
} else if decimal_digit_value(d: D3) == value {
D3
} else if decimal_digit_value(d: D4) == value {
D4
} else if decimal_digit_value(d: D5) == value {
D5
} else if decimal_digit_value(d: D6) == value {
D6
} else if decimal_digit_value(d: D7) == value {
D7
} else if decimal_digit_value(d: D8) == value {
D8
} else {
D9
fn decimal_digit_advance(d: DecimalDigit) -> DecimalDigit {
match decimal_digit_successor(d: d) {
DecimalDigitNext { digit: next } => next
DecimalDigitCarry => D0
}
}

Expand Down
8 changes: 3 additions & 5 deletions dag/test/claim/canonical_order_enrolled_witness_test.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,15 +35,13 @@ fn scrambled_str_map() -> Map<String, Int> {
data canonical_int_map_rendering: String = "\{0: 0, 1: 10, 2: 20, 3: 30, 4: 40, 5: 50, 6: 60, 7: 70, 8: 80, 9: 90, 10: 100, 11: 110, 12: 120, 13: 130, 14: 140, 15: 150, 16: 160, 17: 170, 18: 180, 19: 190}"

// Rendering a map is the canonical content order (Display of Value::Map through canonical_entries).
// Interpolation of a Map is not a named conversion (DESIGN section 4: no implicit stringify); XL-2
// admits only std.nat nat_to_decimal_string, std.integer int_to_decimal_string, and
// v2.std.node symbol_lexeme at interpolating holes, so the order property is held here, not by a Map hole.
test fn to_string_renders_a_map_in_canonical_key_order() -> Bool {
to_string(scrambled_int_map()) == canonical_int_map_rendering
}

// Interpolation lowers to the same Display, so it must agree byte for byte.
test fn interpolation_renders_a_map_in_the_same_order_as_to_string() -> Bool {
"{scrambled_int_map()}" == canonical_int_map_rendering
}

// sorted_map_keys over Int keys is numeric order -- native Ord on i64, which is what the emitted
// v1_rt::sorted_map_keys uses (CanonicalOrdKey), so the two realizations agree.
test fn sorted_map_keys_orders_int_keys_as_native_ord() -> Bool {
Expand Down
84 changes: 21 additions & 63 deletions src/v1/stage0/src/std_integer.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,9 @@ pub use crate::std_machine_constraints::PointerWidth;
pub use crate::std_machine_constraints::{Compose, MachineWidth};
pub use crate::std_measure::{bit_width, bit_width_count, bits_per_byte};
use crate::std_nat::DecimalDigit::{D0, D1, D2, D3, D4, D5, D6, D7, D8, D9};
pub use crate::std_nat::{decimal_digit_glyph, decimal_digit_value};
pub use crate::std_nat::{DecimalDigit, Nat};
use crate::std_nat::DecimalDigitSuccessor::{DecimalDigitCarry, DecimalDigitNext};
pub use crate::std_nat::{decimal_digit_glyph, decimal_digit_successor, decimal_digit_value};
pub use crate::std_nat::{DecimalDigit, DecimalDigitSuccessor, Nat};
pub use crate::std_optional::Optional;
pub use crate::std_types::gt_zero;
pub use crate::std_types::List;
Expand Down Expand Up @@ -197,78 +198,35 @@ pub fn uint8_channel_inclusive_max_value_derived() -> Option<Int> {
}
}

pub fn decimal_digit_of_units(mut __tco_loop_value: Int) -> DecimalDigit {
loop {
#[allow(unused_mut)]
let mut value = __tco_loop_value;
pub fn decimal_digit_of_units(value: Int) -> DecimalDigit {
stacker::maybe_grow(512 * 1024, 2 * 1024 * 1024, || {
if (value.clone() >= 10) {
{
let __tco_0 = v1_rt::int_sub(value, 10);
__tco_loop_value = __tco_0;
continue;
}
decimal_digit_of_units(v1_rt::int_sub(value.clone(), 10))
} else {
if (value.clone() < v1_rt::int_neg(9)) {
{
let __tco_0 = v1_rt::int_add(value, 10);
__tco_loop_value = __tco_0;
continue;
}
decimal_digit_of_units(v1_rt::int_add(value.clone(), 10))
} else {
if (value.clone() < 0) {
break decimal_digit_of_reduced_units(v1_rt::int_sub(0, value.clone()));
decimal_digit_of_units(v1_rt::int_sub(0, value.clone()))
} else {
break decimal_digit_of_reduced_units(value.clone());
}
}
}
}
}

pub fn decimal_digit_of_reduced_units(value: Int) -> DecimalDigit {
if (crate::std_nat::decimal_digit_value(DecimalDigit::D0) == value.clone()) {
DecimalDigit::D0
} else {
if (crate::std_nat::decimal_digit_value(DecimalDigit::D1) == value.clone()) {
DecimalDigit::D1
} else {
if (crate::std_nat::decimal_digit_value(DecimalDigit::D2) == value.clone()) {
DecimalDigit::D2
} else {
if (crate::std_nat::decimal_digit_value(DecimalDigit::D3) == value.clone()) {
DecimalDigit::D3
} else {
if (crate::std_nat::decimal_digit_value(DecimalDigit::D4) == value.clone()) {
DecimalDigit::D4
if (value.clone() == 0) {
DecimalDigit::D0
} else {
if (crate::std_nat::decimal_digit_value(DecimalDigit::D5) == value.clone())
{
DecimalDigit::D5
} else {
if (crate::std_nat::decimal_digit_value(DecimalDigit::D6)
== value.clone())
{
DecimalDigit::D6
} else {
if (crate::std_nat::decimal_digit_value(DecimalDigit::D7)
== value.clone())
{
DecimalDigit::D7
} else {
if (crate::std_nat::decimal_digit_value(DecimalDigit::D8)
== value.clone())
{
DecimalDigit::D8
} else {
DecimalDigit::D9
}
}
}
}
decimal_digit_advance(decimal_digit_of_units(v1_rt::int_sub(
value.clone(),
1,
)))
}
}
}
}
})
}

pub fn decimal_digit_advance(d: DecimalDigit) -> DecimalDigit {
match (*crate::std_nat::decimal_digit_successor(d.clone())).clone() {
DecimalDigitSuccessor::DecimalDigitNext { digit: next, .. } => next.clone(),
DecimalDigitSuccessor::DecimalDigitCarry => DecimalDigit::D0,
}
}

Expand Down
15 changes: 13 additions & 2 deletions src/v2/test/claim/self_host/peano_nat_structural_realization_test.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,14 +21,14 @@ import std.operator_realization {
}
import std.syntax { BinOp, Lt, Le, Gt, Ge, Eq, Div, Mod, Sub, And, Add }
import gunbc.structural_realization_bindings { literal_homomorphism_rows, structural_ordering_rows }
import std.nat { Nat, Zero, Succ, nat_compare, nat_to_decimal_string, decimal_digit_nat, D0, D7 }
import std.nat { Nat, Zero, Succ, nat_compare, nat_to_decimal_string, decimal_digit_nat, D0, D1, D7, D9 }
import test.fixture.structural_peano_nat {
StructuralNat, StructuralZero, StructuralSucc,
StructuralNatDifference, StructuralNatSubtrahendExceedsMinuend,
StructuralNatQuotientRemainder, StructuralNatDivisionByZero,
structural_nat_compare, structural_nat_sub, structural_nat_div_rem, structural_nat_div_rem_by_succ
}
import std.integer { int_to_decimal_string }
import std.integer { int_to_decimal_string, decimal_digit_of_units }

// FALSIFIERS FOR THE STRUCTURAL PEANO NAT REALIZATION (XL-0N, adhoc-aec65f93-b00), the
// interpreter-executed half. The emitted-bytes half -- that a kernel literal at a test.fixture.structural_peano_nat.StructuralNat
Expand Down Expand Up @@ -142,6 +142,17 @@ test fn int_to_decimal_is_the_machine_integer_formatter() -> Bool {
&& int_to_decimal_string(value: 99) == "99"
}

// The units digit is constructed, not looked up, so no Int is out of range: 9 is D9 by derivation
// (not by a default arm), and -1, 10 and 99 each answer their own units digit rather than D9.
test fn decimal_digit_of_units_is_constructed_not_defaulted() -> Bool {
decimal_digit_of_units(value: 9) == D9
&& decimal_digit_of_units(value: 0) == D0
&& decimal_digit_of_units(value: 0 - 1) == D1
&& decimal_digit_of_units(value: 10) == D0
&& decimal_digit_of_units(value: 99) == D9
&& decimal_digit_of_units(value: 0 - 10) == D0
}

// The minimum host integer has no representable negation, so a renderer that negates before it
// divides overflows here; this one divides the signed value and never negates it.
test fn int_to_decimal_renders_the_minimum_machine_integer() -> Bool {
Expand Down