diff --git a/docs/contracts/README.md b/docs/contracts/README.md index 79f72288..e01c8b6c 100644 --- a/docs/contracts/README.md +++ b/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 | diff --git a/docs/contracts/conformance.md b/docs/contracts/conformance.md index 60fa3d91..fa195bbb 100644 --- a/docs/contracts/conformance.md +++ b/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)
`spec/wasm_cross/matrix_softmax_fastexp.almd` (byte-compare)
`spec/wasm_cross/matrix_domain_edges.almd` (byte-compare) | | ALS-T26 | C-359, C-360 | `spec/wasm_cross/datetime_pre_epoch.almd` (byte-compare)
`spec/stdlib/datetime_test.almd` (both-target test)
`spec/wasm_cross/datetime_parse_iso_strict.almd` (byte-compare) | | ALS-T27 | C-361 | `spec/wasm_cross/url_authority_edges.almd` (byte-compare)
`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) | diff --git a/docs/contracts/contracts.toml b/docs/contracts/contracts.toml index 28a37085..e6ace9d8 100644 --- a/docs/contracts/contracts.toml +++ b/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" }, +] diff --git a/docs/specs/als/README.md b/docs/specs/als/README.md index d73e4243..34c4fac3 100644 --- a/docs/specs/als/README.md +++ b/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. diff --git a/docs/specs/als/text-and-numbers.md b/docs/specs/als/text-and-numbers.md index be3e4acf..a4bb82cc 100644 --- a/docs/specs/als/text-and-numbers.md +++ b/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。 diff --git a/proofs/als-validation.toml b/proofs/als-validation.toml index bfc91111..e6c985ee 100644 --- a/proofs/als-validation.toml +++ b/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" \ No newline at end of file diff --git a/proofs/contract-provenance.toml b/proofs/contract-provenance.toml index 70684c38..8add1ddf 100644 --- a/proofs/contract-provenance.toml +++ b/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" diff --git a/ref/src/eval.rs b/ref/src/eval.rs index 660aa197..aed32ad9 100644 --- a/ref/src/eval.rs +++ b/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), diff --git a/ref/src/fmtfloat.rs b/ref/src/fmtfloat.rs index b795218a..7cf98934 100644 --- a/ref/src/fmtfloat.rs +++ b/ref/src/fmtfloat.rs @@ -151,6 +151,23 @@ pub fn shortest_digits(x: f64) -> (Vec, 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, 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, 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, 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. diff --git a/ref/src/stdlib_sized.rs b/ref/src/stdlib_sized.rs index ec48142f..fa9463ad 100644 --- a/ref/src/stdlib_sized.rs +++ b/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) -> Result { + // 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) -> Result { 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() diff --git a/ref/src/value.rs b/ref/src/value.rs index 15a7ba07..a7c9f699 100644 --- a/ref/src/value.rs +++ b/ref/src/value.rs @@ -321,6 +321,11 @@ pub fn values_eq(a: &Value, b: &Value) -> Option { }, ) if b1 == b2 && s1 == s2 => x == y, (Value::Float(x), Value::Float(y)) => x.0 == y.0, + // C-371: binary32 equality; a Float literal operand narrows first + (Value::Float32(x), Value::Float32(y)) => x == y, + (Value::Float32(x), Value::Float(y)) | (Value::Float(y), Value::Float32(x)) => { + *x == y.0 as f32 + } (Value::Bool(x), Value::Bool(y)) => x == y, (Value::Unit, Value::Unit) => true, (Value::Str(x), Value::Str(y)) => x == y, @@ -519,6 +524,8 @@ pub fn render(v: &Value) -> Option { Some(match v { Value::Int(n) => fmt_int(*n), Value::Float(f) => crate::fmtfloat::display_form(*f), + // C-372: the shortest digits that round-trip to the SAME binary32 + Value::Float32(g) => crate::fmtfloat::display_form_f32(*g), Value::Bool(b) => { if *b { "true".to_string() @@ -645,7 +652,6 @@ pub fn render(v: &Value) -> Option { | Value::Path(_) | Value::Matrix(_) | Value::Time { .. } - | Value::Float32(_) | Value::Ptr(_) => return None, }) } diff --git a/ref/tests/fmt_oracle.rs b/ref/tests/fmt_oracle.rs index 3daaa268..eafdc9ad 100644 --- a/ref/tests/fmt_oracle.rs +++ b/ref/tests/fmt_oracle.rs @@ -25,6 +25,7 @@ fn display_matches_host_shortest() { (123456789.123456789f64).to_bits(), (1e78f64).to_bits(), (0.30000000000000004f64).to_bits(), + (1669760939663944.25f64).to_bits(), // an exact tie: rounds UP ]; let mut x: u64 = 0x9E3779B97F4A7C15; for _ in 0..3000 { @@ -92,6 +93,71 @@ fn display_matches_host_shortest() { ); } +/// C-372: a Float32 in interpolation prints the host's f32 Display — the +/// shortest digits that round-trip to the same binary32 — over every biased +/// exponent (with the significand edges, both signs: every power of two, the +/// subnormal boundary, MIN/MAX, ±0, ±inf, NaN) and 3000 pseudo-random +/// bit patterns. +#[test] +fn f32_display_matches_host_shortest() { + let exe = env!("CARGO_BIN_EXE_als-ref"); + let dir = std::env::temp_dir().join(format!("alsref-fmt32-{}", std::process::id())); + std::fs::create_dir_all(&dir).unwrap(); + let mut samples: Vec = Vec::new(); + for e in 0..256u32 { + for m in [0u32, 1, 2, 3, 1 << 22, (1 << 23) - 2, (1 << 23) - 1] { + samples.push((e << 23) | m); + samples.push((1 << 31) | (e << 23) | m); + } + } + let mut x: u32 = 0x9E37_79B9; + for _ in 0..3000 { + x ^= x << 13; + x ^= x >> 17; + x ^= x << 5; + samples.push(x); + } + let mut prog = String::from("fn show(b: Int) -> Unit = {\n let g = float.to_float32(int.bits_to_float(b))\n println(\"${g}\")\n}\n\nfn main() -> Unit = {\n"); + let mut expected = Vec::new(); + for &bits in &samples { + let g = f32::from_bits(bits); + expected.push(format!("{g}")); + // the f64 carrying the same value (exact: every binary32 is a binary64) + prog.push_str(&format!(" show({})\n", (g as f64).to_bits() as i64)); + } + prog.push_str("}\n"); + let path = dir.join("probe32.almd"); + std::fs::write(&path, prog).unwrap(); + let out = Command::new(exe) + .args(["run", path.to_str().unwrap(), "--json"]) + .output() + .unwrap(); + let doc = String::from_utf8_lossy(&out.stdout).to_string(); + let stdout = serde_lite::parse(&doc).stdout; + let got: Vec<&str> = stdout.lines().collect(); + std::fs::remove_dir_all(&dir).ok(); + assert_eq!( + got.len(), + expected.len(), + "line count; raw: {}", + &doc[..doc.len().min(300)] + ); + let bad: Vec = got + .iter() + .zip(expected.iter()) + .zip(samples.iter()) + .filter(|((g, e), _)| g != e) + .map(|((g, e), b)| format!("bits={b:#010x} mine={g:?} host={e:?}")) + .collect(); + assert!( + bad.is_empty(), + "{} of {} disagree:\n{}", + bad.len(), + expected.len(), + bad[..bad.len().min(10)].join("\n") + ); +} + /// just enough JSON reading for the protocol reply (no external crates) mod serde_lite { pub struct Doc { diff --git a/spec/wasm_cross/float32_arithmetic_rounds.almd b/spec/wasm_cross/float32_arithmetic_rounds.almd new file mode 100644 index 00000000..b5a7494f --- /dev/null +++ b/spec/wasm_cross/float32_arithmetic_rounds.almd @@ -0,0 +1,40 @@ +// @contract: C-371 +// Float32 arithmetic is binary32 on every leg: each + - * / % ** and unary - +// result is rounded to f32 (round-to-nearest-even), a conversion into Float32 +// rounds once, and a comparison reads the rounded values. A leg that carries +// Float32 on a wider slot must round after every operation, or the widened +// value (and every comparison or later operation on it) differs from +// native's `f32`; `**` is the one f64 pow of the widened operands, rounded +// once. Operands come from run-time values so no folder decides. +fn widened(label: String, x: Float32) -> Unit = { + println("${label}: ${float.to_string(float32.to_float64(x))}") +} + +effect fn main() -> Unit = { + let n = list.len([1, 2, 3]) + let three: Float32 = int.to_float32(n) + let one: Float32 = three / three + let big: Float32 = int.to_float32(n * 5592405 + 1) + let tenth: Float32 = float.to_float32(0.1) + let fifth: Float32 = tenth + tenth + widened("1/3", one / three) + widened("0.1+0.2", tenth + fifth) + widened("1.1*1.1", (one + tenth) * (one + tenth)) + widened("1-1e-8", one - float.to_float32(0.00000001)) + widened("2^24+1", big + one) + widened("10%3.3", (three * three + one) % (three + three * tenth)) + widened("-(1/3)", -(one / three)) + widened("(1/3)**1.7", (one / three) ** (one + three * float.to_float32(0.23333333))) + widened("3**0.5", three ** (one / (one + one))) + widened("0.1f32", tenth) + widened("int 2^24+1", int.to_float32(16777217)) + var s: Float32 = 0.0 + for _ in 0..<10 { + s = s + tenth + } + widened("sum 10x0.1", s) + println("2^24+1 == 2^24: ${big + one == big}") + println("1+1e-8 > 1: ${one + float.to_float32(0.00000001) > one}") + println("0.1+0.2 == 0.3: ${tenth + fifth == float.to_float32(0.3)}") + println("1/3*3 < 1: ${one / three * three < one}") +} diff --git a/spec/wasm_cross/float32_display_shortest.almd b/spec/wasm_cross/float32_display_shortest.almd new file mode 100644 index 00000000..bfcc3b2e --- /dev/null +++ b/spec/wasm_cross/float32_display_shortest.almd @@ -0,0 +1,48 @@ +// @contract: C-372 +// A Float32 displays as the shortest decimal that round-trips to the SAME +// binary32 (Rust `f32` Display): `0.1` stays `0.1`, never the widened f64's +// `0.10000000149011612`. Interpolation drops the `.0` of an integral value and +// `float32.to_string` keeps it (the C-011 rule), and the digits are the same +// top-level and nested in a list, record, option, tuple or variant. An exact +// tie between the two shortest candidates rounds the magnitude up (2^-12 is +// 0.00024414063). +type P = { x: Float32, n: Int } + +type Shape = + | Dot(Float32) + | Pair(Float32, Float32) + +fn show(label: String, x: Float32) -> Unit = { + println("${label}: ${x} | ${float32.to_string(x)}") +} + +effect fn main() -> Unit = { + let n = list.len([1, 2, 3]) + let three: Float32 = int.to_float32(n) + let one: Float32 = three / three + let zero: Float32 = three - three + let tenth: Float32 = float.to_float32(0.1) + show("0.1", tenth) + show("1/3", one / three) + show("2", one + one) + show("0", zero) + show("-0", -zero) + show("inf", one / zero) + show("-inf", -(one / zero)) + show("nan", zero / zero) + show("max", float.to_float32(340282346638528859811704183484516925440.0)) + show("min normal", float.to_float32(int.bits_to_float(4039728865751334912))) + show("min subnormal", float.to_float32(int.bits_to_float(3936146074321813504))) + show("subnormal", float.to_float32(int.bits_to_float(4008824136515190784))) + show("2^-12 tie", float.to_float32(0.000244140625)) + show("2^20+0.25 tie", float.to_float32(1048576.25)) + show("1e10", float.to_float32(10000000000.0)) + show("123.456", float.to_float32(123.456)) + let xs: List[Float32] = [tenth, one + one, one / three] + println("${xs}") + println("${P { x: tenth, n: 1 }}") + let o: Option[Float32] = some(tenth) + println("${o}") + println("${(tenth, one + one)}") + println("${Dot(tenth)} ${Pair(one / three, one + one)}") +}