Add C-371 (Float32 arithmetic rounds to binary32) and C-372 (Float32 shortest display)

docs/contracts/README.md

@@ -28,10 +28,10 @@ Evidence classes (weakest → strongest): `doc-only` < `by-construction` <
 
 Measured per contract in [`proofs/contract-provenance.toml`](../../proofs/contract-provenance.toml)
 (`scripts/check-contract-provenance.py`: the instant the id entered this ledger against the instant
-the `since` release was tagged). Of 370 contracts: **requirements-first 65** (two-repo regime, since 2026-08-20),
+the `since` release was tagged). Of 372 contracts: **requirements-first 67** (two-repo regime, since 2026-08-20),
 contemporaneous 156, **retroactive 132** (shrink-only ceiling 132), unmeasured 17.
 
-370 contracts
+372 contracts
 
 | ID | Contract | Since | Status | Strongest Evidence | # Fixtures |
 |----|----------|-------|--------|--------------------|-----------:|
@@ -405,4 +405,6 @@ contemporaneous 156, **retroactive 132** (shrink-only ceiling 132), unmeasured 1
 | C-368 | http router: a handler is a function, the most specific route answers, a broken table is refused, 404/405/400 come from the router, identically on both targets | 0.64.0 | active | fixture | 0 |
 | C-369 | a lambda's failure channel carries the error type its ! operands agree on; a String channel carries a typed error as its interpolation text, identically on both targets | 0.65.0 | active | fixture | 1 |
 | C-370 | An http header that would split the request, or that the client manages, is refused with the same err on every lane | 0.66.0 | active | fixture | 0 |
+| C-371 | Float32 arithmetic rounds every result to binary32 on every leg | 0.66.0 | active | fixture | 1 |
+| C-372 | A Float32 displays as the shortest decimal that round-trips to the same binary32 | 0.66.0 | active | fixture | 1 |
 

docs/contracts/conformance.md

@@ -11,7 +11,7 @@
 > (spec-coverage + evidence-class >= fixture for every active contract), so this
 > page cannot legitimately contain an empty Fixtures cell.
 
-132 normative sections; 813 distinct executable fixtures.
+134 normative sections; 815 distinct executable fixtures.
 
 | Section | Contracts | Fixtures (how CI runs each) |
 |---------|-----------|------------------------------|
@@ -147,3 +147,5 @@
 | ALS-T25 | C-223 | `spec/wasm_cross/matrix_pow_libm.almd` (byte-compare)<br>`spec/wasm_cross/matrix_softmax_fastexp.almd` (byte-compare)<br>`spec/wasm_cross/matrix_domain_edges.almd` (byte-compare) |
 | ALS-T26 | C-359, C-360 | `spec/wasm_cross/datetime_pre_epoch.almd` (byte-compare)<br>`spec/stdlib/datetime_test.almd` (both-target test)<br>`spec/wasm_cross/datetime_parse_iso_strict.almd` (byte-compare) |
 | ALS-T27 | C-361 | `spec/wasm_cross/url_authority_edges.almd` (byte-compare)<br>`spec/stdlib/url_test.almd` (both-target test) |
+| ALS-T28 | C-371 | `spec/wasm_cross/float32_arithmetic_rounds.almd` (byte-compare) |
+| ALS-T29 | C-372 | `spec/wasm_cross/float32_display_shortest.almd` (byte-compare) |

docs/contracts/contracts.toml

@@ -4527,3 +4527,23 @@ status    = "active"
 evidence  = [
   { path = "spec/embedded_cross/http_header_refusal.almd", class = "fixture" },
 ]
+[[contract]]
+id        = "C-371"
+spec      = "ALS-T28"
+title     = "Float32 arithmetic rounds every result to binary32 on every leg"
+statement = "Each Float32 `+`, `-`, `*`, `/`, `%`, `**` and unary `-` result is rounded to IEEE-754 binary32 (round-to-nearest-even) after that one operation, so every leg holds the value native's `f32` arithmetic computes: `1/3` widens to 0.3333333432674408, `2^24 + 1` is `2^24`, and ten additions of `0.1` give 1.0000001192092896. A leg that carries Float32 in an f64 slot rounds after every operation; before this, the wasm leg and the interpreter kept the unrounded f64 quotient (0.3333333333333333), which widening, a comparison or any later operation then observed. A conversion into Float32 (`float.to_float32`, `int.to_float32` and the sized `to_float32` twins) rounds once, a comparison reads the rounded values, and a bare float literal in a Float32 position narrows at birth (C-182). `a ** b` on Float32 is the f64 `**` of the widened operands (the vendored libm pow, C-026's one implementation) rounded once to binary32; before this, native did not build it at all (the f32 operands met the f64 pow, almide#3082). No `math.*` function takes a Float32; one reaches them only through an explicit `float32.to_float64`. spec/wasm_cross/float32_arithmetic_rounds.almd observes each operation through `float32.to_float64` and `float.to_string`, which show every bit of the binary32 value, and through comparisons whose answer flips when a leg does not round."
+since     = "0.66.0"
+status    = "active"
+evidence  = [
+  { path = "spec/wasm_cross/float32_arithmetic_rounds.almd", class = "fixture" },
+]
+[[contract]]
+id        = "C-372"
+spec      = "ALS-T29"
+title     = "A Float32 displays as the shortest decimal that round-trips to the same binary32"
+statement = "A Float32 prints as Rust `f32` Display does: the shortest positional decimal that parses back to the SAME binary32, so `0.1` prints `0.1`, not the widened f64's `0.10000000149011612`, and the f32 maximum prints 340282350000000000000000000000000000000. An exact tie between the two shortest candidates rounds the magnitude up (`2^-12` prints 0.00024414063, `2^20 + 0.25` prints 1048576.3). In interpolation and inside a list, record, option, tuple or variant payload an integral value drops its `.0` (C-011's rule: `${2.0f32}` is `2`), and `float32.to_string` keeps it (`2.0`); `-0` keeps its sign, and the non-finite values are `inf`, `-inf` and `NaN`. Before this, `float32.to_string` printed the widened f64's digits on every leg, and the wasm leg and the interpreter did the same for interpolation where native printed the f32 digits. spec/wasm_cross/float32_display_shortest.almd pins the value matrix (0.1, 1/3, a whole value, ±0, ±inf, NaN, the f32 maximum, the least normal, the least subnormal, a subnormal, both tie shapes) top-level in both forms and nested in each container."
+since     = "0.66.0"
+status    = "active"
+evidence  = [
+  { path = "spec/wasm_cross/float32_display_shortest.almd", class = "fixture" },
+]

docs/specs/als/README.md

@@ -153,7 +153,7 @@
 | [ALS-S5](./strings.md#als-s5-split-の区切り規範) | split の区切り規範 | C-050 |
 | [ALS-S6](./strings.md#als-s6-規模不変性) | 規模不変性 | C-074 |
 
-## text-and-numbers.md — 27 section(s)
+## text-and-numbers.md — 29 section(s)
 
 | ID | Section | Contracts |
 |----|---------|-----------|
@@ -184,5 +184,7 @@
 | [ALS-T25](./text-and-numbers.md#als-t25-正準-fast-exp) | 正準 fast-exp | C-223 |
 | [ALS-T26](./text-and-numbers.md#als-t26-datetime-の暦フィールドと-parse_iso-の文法) | datetime の暦フィールドと parse_iso の文法 | C-359, C-360 |
 | [ALS-T27](./text-and-numbers.md#als-t27-urlparse-の-authority-規範) | url.parse の authority 規範 | C-361 |
+| [ALS-T28](./text-and-numbers.md#als-t28-float32-演算の-binary32-丸め) | Float32 演算の binary32 丸め | C-371 |
+| [ALS-T29](./text-and-numbers.md#als-t29-float32-の表示) | Float32 の表示 | C-372 |
 
-132 sections across 11 chapters.
+134 sections across 11 chapters.

docs/specs/als/text-and-numbers.md

@@ -1,6 +1,6 @@
 # ALS §T — Text and Number Semantics (normative)
 
-> Last updated: 2026-08-27
+> Last updated: 2026-09-30
 
 > **Status**: normative. これらの節は実装から独立した**規範**であり、v0（native）と
 > v1（MIR/wasm）の両実装がこの節に適合する義務を負う。適合の証拠は
@@ -531,3 +531,34 @@ host として読まずに名指しで拒否する: userinfo は
 
 テスト: `spec/wasm_cross/url_authority_edges.almd`、
 `spec/stdlib/url_test.almd`。Contracts: C-361。
+
+## ALS-T28 Float32 演算の binary32 丸め
+
+`Float32` の各演算（`+` `-` `*` `/` `%` `**`、単項 `-`）の結果は IEEE-754 **binary32**
+の最近接偶数丸めで **1 演算ごとに** f32 に丸まり、native の `f32` 演算と同じ値に
+なる。より広いスロット（f64）で `Float32` を運ぶ実装も、各演算の直後に binary32 へ
+丸めなければならない — 丸めない値は `float32.to_float64` による拡幅、比較、後続の
+演算のすべてで native と異なる。`Float32` への変換（`float.to_float32`、
+`int.to_float32` と sized 整数の `to_float32`）は 1 回丸める。比較（`==` `!=` `<`
+`<=` `>` `>=`）は丸めた binary32 の値を比べる。`Float32` 文脈の裸の float
+リテラルは生まれたときに binary32 へ狭まる（ALS-E3）。`math.*` は `Float` のみを
+受け取り、`Float32` は明示の拡幅（`float32.to_float64`）を経て渡る。`Float32` の
+`a ** b` は、拡幅した両辺の `Float` の `**`（ALS-T10 の単一の pow 実装）を 1 回
+binary32 へ丸めた値である。
+
+例: `1/3` は `0.3333333432674408` に拡幅され、`2^24 + 1` は `2^24` に丸まり、
+`0.1` を 10 回足した和は `1.0000001192092896`。
+
+テスト: `spec/wasm_cross/float32_arithmetic_rounds.almd`。Contracts: C-371。
+
+## ALS-T29 Float32 の表示
+
+`Float32` は、**同じ binary32 に往復する最短の十進表現**（Rust `f32` の Display、
+位置記法・指数なし）で表示される。`0.1` は `0.1` であり、拡幅した f64 の
+`0.10000000149011612` ではない。二つの最短候補がちょうど等距離なら大きさを
+切り上げる（`2^-12` は `0.00024414063`）。文字列補間とコンテナ内（リスト・
+レコード・Option・タプル・variant のペイロード）は整数値の `.0` を落とし
+（ALS-R2 / C-011 の規則）、`float32.to_string` は保つ。`-0` の符号を保ち、
+非有限値は `inf` / `-inf` / `NaN`。
+
+テスト: `spec/wasm_cross/float32_display_shortest.almd`。Contracts: C-372。

proofs/als-validation.toml

@@ -1081,4 +1081,18 @@ hash = "sha256:be7520120410"
 reviewed = "2026-09-22"
 by = "O6lvl4 (via the Claude session; re-reviewed 2026-09-22 after the batch renumbering: the text now states the variable-width %Y that datetime.format shares with to_iso, and the T26/T27 calendar, parse_iso and url.parse rules, each checked against the fixture output recorded on native, structural wasm and incumbent wasm)"
 independent = "no"
+verdict = "accurate"
+[[section]]
+id = "ALS-T28"
+hash = "sha256:89032e4530e1"
+reviewed = "2026-09-30"
+by = "O6lvl4 (via the Claude session; checked against the ref evaluator, native almide and the host f32 formatter over every f32 exponent and 3000 random patterns)"
+independent = "no"
+verdict = "accurate"
+[[section]]
+id = "ALS-T29"
+hash = "sha256:a1fec2de4a9a"
+reviewed = "2026-09-30"
+by = "O6lvl4 (via the Claude session; checked against the ref evaluator, native almide and the host f32 formatter over every f32 exponent and 3000 random patterns)"
+independent = "no"
 verdict = "accurate"

proofs/contract-provenance.toml

@@ -2786,3 +2786,17 @@ since = "0.66.0"
 entry = "2026-09-28T14:56:42+09:00"
 entry_commit = "e854238"
 class = "requirements-first"
+
+[[contract]]
+id = "C-371"
+since = "0.66.0"
+entry = "2026-09-30T16:15:25+09:00"
+entry_commit = "6b3956e"
+class = "requirements-first"
+
+[[contract]]
+id = "C-372"
+since = "0.66.0"
+entry = "2026-09-30T16:15:25+09:00"
+entry_commit = "6b3956e"
+class = "requirements-first"

ref/src/eval.rs

@@ -196,6 +196,16 @@ fn snapshot_bytes(v: Value) -> Value {
 
 /// canonicalize NaN results: every float operation that produces a NaN
 /// observes as the single canonical quiet NaN (nan_canonical_observation)
+/// The binary32 value of a Float32, or of a Float literal narrowed to one
+/// (C-182: a literal takes its Float32 context).
+fn f32_of(v: &Value) -> f32 {
+    match v {
+        Value::Float32(g) => *g,
+        Value::Float(F64(f)) => *f as f32,
+        _ => f32::NAN,
+    }
+}
+
 pub fn fnan(x: f64) -> f64 {
     if x.is_nan() {
         f64::from_bits(0x7FF8000000000000)
@@ -2446,6 +2456,7 @@ impl Interp {
                 match (op, v) {
                     (UnOp::Neg, Value::Int(n)) => Ok(Value::Int(n.wrapping_neg())),
                     (UnOp::Neg, Value::Float(f)) => Ok(Value::Float(F64(fnan(-f.0)))),
+                    (UnOp::Neg, Value::Float32(g)) => Ok(Value::Float32(-g)),
                     (UnOp::Not, Value::Bool(b)) => Ok(Value::Bool(!b)),
                     (op, v) => Err(Flow::Fatal(format!("unary {op:?} on a {}", v.type_name()))),
                 }
@@ -2753,6 +2764,26 @@ impl Interp {
                     a.0, b.0,
                 )))))
             }
+            // C-371: Float32 arithmetic is IEEE-754 binary32 — every + - * / % **
+            // result is rounded to f32 (round-to-nearest-even), never carried
+            // at f64 width. A bare float literal in a Float32 operation takes
+            // the Float32 type (it narrows at birth, C-182).
+            (Add | Sub | Mul | Div | Rem | Pow, Value::Float32(_), Value::Float(F64(f))) => {
+                self.binop(op, l.clone(), Value::Float32(*f as f32))
+            }
+            (Add | Sub | Mul | Div | Rem | Pow, Value::Float(F64(f)), Value::Float32(_)) => {
+                self.binop(op, Value::Float32(*f as f32), r.clone())
+            }
+            (Add, Value::Float32(a), Value::Float32(b)) => Ok(Value::Float32(a + b)),
+            (Sub, Value::Float32(a), Value::Float32(b)) => Ok(Value::Float32(a - b)),
+            (Mul, Value::Float32(a), Value::Float32(b)) => Ok(Value::Float32(a * b)),
+            (Div, Value::Float32(a), Value::Float32(b)) => Ok(Value::Float32(a / b)),
+            (Rem, Value::Float32(a), Value::Float32(b)) => Ok(Value::Float32(a % b)),
+            // `**` on Float32: the vendored libm pow (ALS-T10) of the widened
+            // operands, rounded once to binary32
+            (Pow, Value::Float32(a), Value::Float32(b)) => Ok(Value::Float32(
+                crate::libm::almide_rt_libm_pow(*a as f64, *b as f64) as f32,
+            )),
             // C-180: sized-integer arithmetic wraps at the declared width;
             // / and % are total per width (zero divisor and signed MIN/-1
             // abort in the T6 form); unsigned widths divide/compare unsigned
@@ -2949,6 +2980,16 @@ impl Interp {
                         Some(o) => o,
                         None => return Ok(Value::Bool(false)),
                     },
+                    // C-371: a Float32 compares its binary32 value; a literal
+                    // operand narrows to Float32 first
+                    (Value::Float32(_), Value::Float32(_))
+                    | (Value::Float32(_), Value::Float(_))
+                    | (Value::Float(_), Value::Float32(_)) => {
+                        match f32_of(&l).partial_cmp(&f32_of(&r)) {
+                            Some(o) => o,
+                            None => return Ok(Value::Bool(false)),
+                        }
+                    }
                     (Value::Str(a), Value::Str(b)) => char_cmp(a, b),
                     // C-099: false < true
                     (Value::Bool(a), Value::Bool(b)) => a.cmp(b),

ref/src/fmtfloat.rs

@@ -151,6 +151,23 @@ pub fn shortest_digits(x: f64) -> (Vec<u8>, i32) {
     shortest_core(m, e as i64, min_normal, x)
 }
 
+/// Shortest digits that round-trip to the same BINARY32 (C-372): the same
+/// free-format core over the f32 significand and exponent — the rounding
+/// interval is the f32's, so `0.1f32` gives "1" at k = 0, not the widened
+/// f64's seventeen digits.
+pub fn shortest_digits_f32(g: f32) -> (Vec<u8>, i32) {
+    let bits = g.abs().to_bits();
+    let raw_exp = (bits >> 23) as i32;
+    let frac = (bits & ((1u32 << 23) - 1)) as u64;
+    let (m, e) = if raw_exp == 0 {
+        (frac, -149)
+    } else {
+        (frac | (1u64 << 23), raw_exp - 150)
+    };
+    let min_normal = m == (1u64 << 23) && e > -149;
+    shortest_core(m, e as i64, min_normal, g as f64)
+}
+
 fn shortest_core(m: u64, e: i64, min_normal: bool, approx: f64) -> (Vec<u8>, i32) {
     // scaled value R/S, boundaries M+ / M-
     let (mut r, mut s, mut m_plus, mut m_minus);
@@ -258,13 +275,13 @@ fn shortest_core(m: u64, e: i64, min_normal: bool, approx: f64) -> (Vec<u8>, i32
                 break;
             }
             (true, true) => {
-                // closest boundary decides; tie → even-ish: round up when 2r >= s
+                // closest candidate decides; an EXACT tie rounds the magnitude
+                // UP (2r >= s) — Rust Display's shortest mode, for binary64
+                // (1669760939663944.25 prints ...944.3) and binary32 alike
+                // (2^-12 prints 0.00024414063). An even-digit rule here read
+                // ...944.2 / 0.00024414062, which no implementation prints.
                 let two_r = r.shl(1);
-                let up = match two_r.cmp(&s) {
-                    std::cmp::Ordering::Greater => true,
-                    std::cmp::Ordering::Less => false,
-                    std::cmp::Ordering::Equal => d % 2 == 1,
-                };
+                let up = two_r.cmp(&s) != std::cmp::Ordering::Less;
                 digits.push(if up { d + 1 } else { d });
                 break;
             }
@@ -377,6 +394,43 @@ pub fn display_form(f: F64) -> String {
     }
 }
 
+/// A Float32's text (C-372): Rust `f32` Display's shortest round-trip digits
+/// of the binary32 value, positional; `dot0` keeps the `.0` of an integral
+/// value (`float32.to_string`), off for interpolation / containers (C-011).
+fn f32_form(g: f32, dot0: bool) -> String {
+    if g.is_nan() {
+        return "NaN".into();
+    }
+    if g.is_infinite() {
+        return if g > 0.0 { "inf".into() } else { "-inf".into() };
+    }
+    if g == 0.0 {
+        let z = if dot0 { "0.0" } else { "0" };
+        return if g.is_sign_negative() {
+            format!("-{z}")
+        } else {
+            z.into()
+        };
+    }
+    let (digits, k) = shortest_digits_f32(g);
+    let body = positional(&digits, k, dot0);
+    if g < 0.0 {
+        format!("-{body}")
+    } else {
+        body
+    }
+}
+
+/// `float32.to_string` (C-372).
+pub fn to_string_form_f32(g: f32) -> String {
+    f32_form(g, true)
+}
+
+/// A Float32 in interpolation or inside a container (C-372).
+pub fn display_form_f32(g: f32) -> String {
+    f32_form(g, false)
+}
+
 /// `float.to_fixed(x, n)` (ALS-T9): round-half-to-even on the EXACT binary
 /// value — the decimal expansion of m·2^e is finite; we compare the true
 /// remainder against one half of the last kept unit, exactly.

ref/src/stdlib_sized.rs

@@ -59,6 +59,8 @@ pub const SIZED_FNS: &[&str] = &[
     "float.to_float32_checked",
     "float32.to_string",
     "float.from_float32",
+    "float.to_float32",
+    "float32.to_float64",
     "int.to_float32",
     "int.to_float32_checked",
     "int.max_value",
@@ -328,6 +330,22 @@ fn dispatch(it: &mut Interp, name: &str, args: Vec<Value>) -> Result<Value, Flow
                 Value::None
             })
         }
+        "float.to_float32" => {
+            // C-371: one rounding to binary32 (round-to-nearest-even)
+            arity(name, &args, 1)?;
+            let f = want_float(name, &args[0])?;
+            Ok(Value::Float32(f as f32))
+        }
+        "float32.to_float64" => {
+            arity(name, &args, 1)?;
+            match &args[0] {
+                Value::Float32(g) => Ok(Value::Float(F64(*g as f64))),
+                other => Err(Flow::Fatal(format!(
+                    "{name}: expected Float32, got {}",
+                    other.type_name()
+                ))),
+            }
+        }
         "float.from_float32" => {
             arity(name, &args, 1)?;
             match &args[0] {
@@ -374,9 +392,9 @@ fn dispatch(it: &mut Interp, name: &str, args: Vec<Value>) -> Result<Value, Flow
         "float32.to_string" => {
             arity(name, &args, 1)?;
             match &args[0] {
-                // measured on 0.59.1: the spelling is the f64 shortest form
-                // of the WIDENED value (0.1f32 prints 0.10000000149011612)
-                Value::Float32(g) => Ok(Value::str(&fmtfloat::to_string_form(F64(*g as f64)))),
+                // C-372: the binary32's own shortest digits (0.1f32 -> "0.1"),
+                // `.0` kept on an integral value like float.to_string
+                Value::Float32(g) => Ok(Value::str(&fmtfloat::to_string_form_f32(*g))),
                 other => Err(Flow::Fatal(format!(
                     "{name}: expected Float32, got {}",
                     other.type_name()