From 5cb58c642b556e9925b1dab82929574a8f78a3a2 Mon Sep 17 00:00:00 2001 From: O6lvl4 Date: Tue, 13 Oct 2026 19:05:33 +0900 Subject: [PATCH 1/2] Canonicalize NaN in every bytes float writer of the reference evaluator and implement set_float32 Co-Authored-By: Claude Opus 5.5 (1M context) --- ref/src/stdlib_ext.rs | 62 +++++++++++++++++++++++++++++++++++++++--- ref/src/stdlib_ext2.rs | 5 ++-- 2 files changed, 61 insertions(+), 6 deletions(-) diff --git a/ref/src/stdlib_ext.rs b/ref/src/stdlib_ext.rs index 630089f4..2f647b32 100644 --- a/ref/src/stdlib_ext.rs +++ b/ref/src/stdlib_ext.rs @@ -75,6 +75,7 @@ pub const EXT_FNS: &[&str] = &[ "bytes.write_uint32", "bytes.write_int32", "bytes.write_float32", + "bytes.set_float32", "bytes.set_uint16", "bytes.set_uint32", "bytes.read_uint16", @@ -216,6 +217,36 @@ fn want_float(name: &str, v: &Value) -> Result { } } +/// The binary32 value a Float32 writer receives: a Float32, or a Float literal +/// narrowed to one (C-182: a literal takes its Float32 context). +fn want_float32(name: &str, v: &Value) -> Result { + match v { + Value::Float32(g) => Ok(*g), + Value::Float(f) => Ok(f.0 as f32), + other => mismatch(name, "Float32", other), + } +} + +/// C-210: every bytes float writer is a NaN-observation boundary — a NaN of +/// any sign or payload writes the one canonical f64 pattern. The whole writer +/// family (append, set, write) reads its bits from here. +pub(crate) fn obs_bits_f64(x: f64) -> u64 { + if x.is_nan() { + 0x7FF8_0000_0000_0000 + } else { + x.to_bits() + } +} + +/// C-210: the binary32 twin of [`obs_bits_f64`] — canonical f32 0x7FC00000. +pub(crate) fn obs_bits_f32(x: f32) -> u32 { + if x.is_nan() { + 0x7FC0_0000 + } else { + x.to_bits() + } +} + fn want_bool(name: &str, v: &Value) -> Result { match v { Value::Bool(b) => Ok(*b), @@ -628,12 +659,35 @@ fn dispatch(it: &mut Interp, name: &str, args: Vec) -> Result { arity(name, &args, 3)?; let b = want_bytes(name, &args[0])?; - let f = want_float(name, &args[1])? as f32; + let bits = obs_bits_f32(want_float32(name, &args[1])?); let le = want_endian(name, &args[2])?; - let raw = if le { f.to_le_bytes() } else { f.to_be_bytes() }; + let raw = if le { + bits.to_le_bytes() + } else { + bits.to_be_bytes() + }; b.borrow_mut().extend_from_slice(&raw); Ok(Value::Unit) } + "bytes.set_float32" => { + // OOB is a silent NO-OP, like every set_* (bytes_negative_offset_family) + arity(name, &args, 4)?; + let b = want_bytes(name, &args[0])?; + let off = want_int(name, &args[1])?; + let bits = obs_bits_f32(want_float32(name, &args[2])?); + let le = want_endian(name, &args[3])?; + let raw = if le { + bits.to_le_bytes() + } else { + bits.to_be_bytes() + }; + let mut buf = b.borrow_mut(); + if off >= 0 && (off as u64).saturating_add(4) <= buf.len() as u64 { + let off = off as usize; + buf[off..off + 4].copy_from_slice(&raw); + } + Ok(Value::Unit) + } "bytes.set_uint16" | "bytes.set_uint32" => { arity(name, &args, 4)?; let b = want_bytes(name, &args[0])?; @@ -1465,9 +1519,9 @@ fn write_bytes_fn(it: &Interp, name: &str, args: &[Value]) -> Result) -> Result) -> Result Date: Tue, 13 Oct 2026 19:05:34 +0900 Subject: [PATCH 2/2] Extend C-210 to every bytes float writer and pin the set and write writers' NaN bits in a fixture Co-Authored-By: Claude Opus 5.5 (1M context) --- docs/contracts/README.md | 2 +- docs/contracts/conformance.md | 4 +-- docs/contracts/contracts.toml | 3 +- .../nan_canonical_bytes_set_write.almd | 35 +++++++++++++++++++ .../wasm_cross/nan_canonical_bytes_write.almd | 15 ++++++++ 5 files changed, 55 insertions(+), 4 deletions(-) create mode 100644 spec/wasm_cross/nan_canonical_bytes_set_write.almd diff --git a/docs/contracts/README.md b/docs/contracts/README.md index 4c44c8f3..ad71436c 100644 --- a/docs/contracts/README.md +++ b/docs/contracts/README.md @@ -244,7 +244,7 @@ contemporaneous 156, **retroactive 132** (shrink-only ceiling 132), unmeasured 1 | C-207 | CM-1 is a versioned constant with a ratio-only wall-clock claim | 0.47.0 | active | fixture | 1 | | C-208 | fan.timeout is omega-relative: fixed ends everywhere, fixed omega replays byte-identically | 0.47.0 | active | fixture | 1 | | C-209 | Codec encode omits none; decode folds missing/null to none; Value passes through verbatim | 0.52.0 | active | fixture | 1 | -| C-210 | NaN observation is canonical — the deterministic-profile conformance law | 0.53.0 | active | fixture | 2 | +| C-210 | NaN observation is canonical — the deterministic-profile conformance law | 0.53.0 | active | fixture | 3 | | C-211 | ! propagates in pure Result/Option-returning fns, byte-identical across targets | 0.53.5 | active | fixture | 1 | | C-212 | Two self-host modules with same-named private helpers link cleanly or wall — never an invalid module | 0.52.0 | active | fixture | 1 | | C-213 | The bytes byte-level writers encode the same buffer on both targets, out-of-range writes included | 0.53.5 | active | fixture | 4 | diff --git a/docs/contracts/conformance.md b/docs/contracts/conformance.md index 86406b07..0ac47a22 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. -134 normative sections; 827 distinct executable fixtures. +134 normative sections; 828 distinct executable fixtures. | Section | Contracts | Fixtures (how CI runs each) | |---------|-----------|------------------------------| @@ -121,7 +121,7 @@ | ALS-ST5 | C-265 | `spec/wasm_cross/guard_statement.almd` (byte-compare) | | ALS-ST6 | C-266 | `spec/wasm_cross/guard_let_statement.almd` (byte-compare) | | ALS-T1 | C-021, C-294 | `spec/wasm_cross/string_whitespace.almd` (byte-compare)
`spec/wasm_cross/fuel_zero_budget_inline.almd` (byte-compare) | -| ALS-T2 | C-024, C-210, C-300, C-301 | `spec/wasm_cross/float_parse.almd` (byte-compare)
`spec/wasm_cross/nan_canonical_observation.almd` (byte-compare)
`spec/wasm_cross/nan_canonical_bytes_write.almd` (byte-compare)
`spec/wasm_cross/map_literal_ctor_values.almd` (byte-compare)
`tests/heap_cap_test.rs` (cargo gate)
`spec/wasm_cross/list_arg_map_view.almd` (byte-compare)
`spec/wasm_cross/map_upsert_str.almd` (byte-compare) | +| ALS-T2 | C-024, C-210, C-300, C-301 | `spec/wasm_cross/float_parse.almd` (byte-compare)
`spec/wasm_cross/nan_canonical_observation.almd` (byte-compare)
`spec/wasm_cross/nan_canonical_bytes_write.almd` (byte-compare)
`spec/wasm_cross/nan_canonical_bytes_set_write.almd` (byte-compare)
`spec/wasm_cross/map_literal_ctor_values.almd` (byte-compare)
`tests/heap_cap_test.rs` (cargo gate)
`spec/wasm_cross/list_arg_map_view.almd` (byte-compare)
`spec/wasm_cross/map_upsert_str.almd` (byte-compare) | | ALS-T3 | C-087, C-298, C-299 | `spec/wasm_cross/json_number_unicode.almd` (byte-compare)
`spec/wasm_cross/json_string_span.almd` (byte-compare)
`spec/wasm_cross/json_parse_lenient_edges.almd` (byte-compare)
`spec/wasm_cross/json_many_keys.almd` (byte-compare)
`spec/wasm_cross/codec_decode_error_surface.almd` (byte-compare)
`spec/wasm_cross/codec_deep_nesting.almd` (byte-compare)
`spec/wasm_cross/codec_doc_array.almd` (byte-compare)
`spec/wasm_cross/codec_empty_and_bool.almd` (byte-compare)
`spec/wasm_cross/codec_extra_keys.almd` (byte-compare)
`spec/wasm_cross/codec_int_float_boundaries.almd` (byte-compare)
`spec/wasm_cross/codec_list_list_field.almd` (byte-compare)
`spec/wasm_cross/codec_list_default_field.almd` (byte-compare)
`spec/wasm_cross/codec_nested_records.almd` (byte-compare)
`spec/wasm_cross/codec_option_numeric.almd` (byte-compare)
`spec/wasm_cross/codec_string_escapes.almd` (byte-compare)
`spec/wasm_cross/codec_variant_roundtrip.almd` (byte-compare)
`spec/wasm_cross/codec_whitespace_tolerance.almd` (byte-compare)
`spec/wasm_cross/codec_list_default.almd` (byte-compare)
`spec/wasm_cross/codec_triple_list.almd` (byte-compare)
`spec/wasm_cross/hash_digests.almd` (byte-compare)
`spec/stdlib/hash_test.almd` (both-target test) | | ALS-T4 | C-129, C-171 | `spec/wasm_cross/list_chunk_windows.almd` (byte-compare)
`spec/wasm_cross/list_chunk_zero.almd` (byte-compare)
`spec/wasm_cross/list_windows_zero.almd` (byte-compare)
`spec/wasm_cross/list_window_zero.almd` (byte-compare)
`spec/wasm_cross/bytes_f16_offset_overflow.almd` (byte-compare) | | ALS-T5 | C-020, C-162 | `spec/wasm_cross/string_case_unicode.almd` (byte-compare)
`spec/wasm_cross/io_write_ordering.almd` (byte-compare) | diff --git a/docs/contracts/contracts.toml b/docs/contracts/contracts.toml index 6be0876d..db0f3df9 100644 --- a/docs/contracts/contracts.toml +++ b/docs/contracts/contracts.toml @@ -2588,12 +2588,13 @@ evidence = [ id = "C-210" spec = "ALS-T2" title = "NaN observation is canonical — the deterministic-profile conformance law" -statement = "A NaN's raw sign/payload bits are the one place the byte-identical law would leak host state: x86 arithmetic produces sign-set NaNs where aarch64 does not, engines may or may not propagate payloads, and `int.bits_to_float` can smuggle arbitrary payloads in. Every OBSERVATION boundary therefore collapses NaN to a single canonical pattern — `float.to_bits` answers 0x7FF8000000000000 for every NaN however produced (arithmetic, negation, from_bits round-trip), and the bytes float writes (`bytes.append_f64_le/be`, `append_f32_le/be`) write the same canonical f64 pattern / the canonical f32 pattern 0x7FC00000. Non-NaN bits stay raw (to_bits(1.5) == 0x3FF8000000000000 — normalization never over-reaches), and a non-canonical NaN still EXISTS as a value (from_bits -> arithmetic keeps IEEE semantics); only observers are blind to its representation. This is the Wasm 3.0 deterministic-profile stance applied at the language layer, so it holds on BOTH targets and on every host architecture — stronger than the profile itself, which constrains only the wasm leg. The emitted module also stays inside the profile's instruction subset: no relaxed SIMD, no threads/atomics/shared memory (machine-checked by crates/almide-mir/tests/deterministic_profile_test.rs)." +statement = "A NaN's raw sign/payload bits are the one place the byte-identical law would leak host state: x86 arithmetic produces sign-set NaNs where aarch64 does not, engines may or may not propagate payloads, and `int.bits_to_float` can smuggle arbitrary payloads in. Every OBSERVATION boundary therefore collapses NaN to a single canonical pattern — `float.to_bits` answers 0x7FF8000000000000 for every NaN however produced (arithmetic, negation, from_bits round-trip), and EVERY bytes float writer writes the same canonical f64 pattern / the canonical f32 pattern 0x7FC00000 on every leg — the appends (`bytes.append_f64_le/be`, `append_f32_le/be`), the in-place sets (`bytes.set_f64_le/be`, `set_f32_le/be`, `set_float32`) and the cursor writes (`bytes.write_f64_be`, `write_float32`) are one family under this one rule. Non-NaN bits stay raw (to_bits(1.5) == 0x3FF8000000000000 — normalization never over-reaches), and a non-canonical NaN still EXISTS as a value (from_bits -> arithmetic keeps IEEE semantics); only observers are blind to its representation. This is the Wasm 3.0 deterministic-profile stance applied at the language layer, so it holds on BOTH targets and on every host architecture — stronger than the profile itself, which constrains only the wasm leg. The emitted module also stays inside the profile's instruction subset: no relaxed SIMD, no threads/atomics/shared memory (machine-checked by crates/almide-mir/tests/deterministic_profile_test.rs)." since = "0.53.0" status = "active" evidence = [ { path = "spec/wasm_cross/nan_canonical_observation.almd", class = "fixture" }, { path = "spec/wasm_cross/nan_canonical_bytes_write.almd", class = "fixture" }, + { path = "spec/wasm_cross/nan_canonical_bytes_set_write.almd", class = "fixture" }, ] # ── PURE-FN ! PROPAGATION — the #1067 E022 lift ─ diff --git a/spec/wasm_cross/nan_canonical_bytes_set_write.almd b/spec/wasm_cross/nan_canonical_bytes_set_write.almd new file mode 100644 index 00000000..978063a6 --- /dev/null +++ b/spec/wasm_cross/nan_canonical_bytes_set_write.almd @@ -0,0 +1,35 @@ +// @contract: C-210 +// The SET and WRITE half of C-210's bytes float-writer family (#3658): every +// writer, not only the appends, is a NaN-observation boundary. `set_f64_le/be`, +// `set_f32_le/be`, `write_f64_be`, `write_float32` and `set_float32` all write +// the canonical pattern (f64 0x7FF8000000000000, f32 0x7FC00000) for every NaN, +// however produced: 0.0/0.0, a from_bits payload NaN (sign set, low payload), a +// negated NaN, an arithmetic NaN. The last row is a non-NaN: its bits stay raw, +// so the rule never over-reaches. +effect fn main() -> Unit = { + let z = 0.0 + let nan_div = z / z + let payload = int.bits_to_float(0 - 256) + let arith = 0.0 - nan_div + let rows = [("div", nan_div), ("payload", payload), ("negated", -nan_div), ("arith", arith), ("half", 1.5)] + for (name, x) in rows { + var s = bytes.new(24) + bytes.set_f64_le(s, 0, x) + bytes.set_f64_be(s, 8, x) + bytes.set_f32_le(s, 16, x) + bytes.set_f32_be(s, 20, x) + println("${name} set=${bytes.to_list(s)}") + var w = bytes.new(0) + bytes.write_f64_be(w, x) + println("${name} write_f64_be=${bytes.to_list(w)}") + let x32 = float.to_float32(x) + var t = bytes.new(0) + bytes.write_float32(t, x32, LittleEndian) + bytes.write_float32(t, x32, BigEndian) + println("${name} write_float32=${bytes.to_list(t)}") + var u = bytes.new(8) + bytes.set_float32(u, 0, x32, LittleEndian) + bytes.set_float32(u, 4, x32, BigEndian) + println("${name} set_float32=${bytes.to_list(u)}") + } +} diff --git a/spec/wasm_cross/nan_canonical_bytes_write.almd b/spec/wasm_cross/nan_canonical_bytes_write.almd index e237f9c7..781904da 100644 --- a/spec/wasm_cross/nan_canonical_bytes_write.almd +++ b/spec/wasm_cross/nan_canonical_bytes_write.almd @@ -14,4 +14,19 @@ effect fn main() -> Unit = { bytes.append_f32_le(b, nan_div) println(if bytes.read_i64_le(b, 0) == canon then "f64write:canonical" else "f64write:RAW-LEAK") println(if bytes.read_u32_le(b, 8) == 0x7FC00000 then "f32write:canonical" else "f32write:RAW-LEAK") + // #3647: 0.0/0.0 is already the canonical pattern on aarch64, so it alone + // could not see a raw write there. A from_bits payload NaN, a negated + // (sign-set) NaN, and an arithmetic NaN (sign-set by x86's default, not by + // aarch64's) must collapse too, through all four append fns: f64 le/be, + // then f32 le/be. + let payload = int.bits_to_float(0 - 256) + let arith = 0.0 - nan_div + for (name, x) in [("payload", payload), ("negated", -nan_div), ("arith", arith)] { + var c = bytes.new(0) + bytes.append_f64_le(c, x) + bytes.append_f64_be(c, x) + bytes.append_f32_le(c, x) + bytes.append_f32_be(c, x) + println("${name}=${bytes.to_list(c)}") + } }