Extend C-210 to every bytes float writer

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 |

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)<br>`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)<br>`spec/wasm_cross/nan_canonical_observation.almd` (byte-compare)<br>`spec/wasm_cross/nan_canonical_bytes_write.almd` (byte-compare)<br>`spec/wasm_cross/map_literal_ctor_values.almd` (byte-compare)<br>`tests/heap_cap_test.rs` (cargo gate)<br>`spec/wasm_cross/list_arg_map_view.almd` (byte-compare)<br>`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)<br>`spec/wasm_cross/nan_canonical_observation.almd` (byte-compare)<br>`spec/wasm_cross/nan_canonical_bytes_write.almd` (byte-compare)<br>`spec/wasm_cross/nan_canonical_bytes_set_write.almd` (byte-compare)<br>`spec/wasm_cross/map_literal_ctor_values.almd` (byte-compare)<br>`tests/heap_cap_test.rs` (cargo gate)<br>`spec/wasm_cross/list_arg_map_view.almd` (byte-compare)<br>`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)<br>`spec/wasm_cross/json_string_span.almd` (byte-compare)<br>`spec/wasm_cross/json_parse_lenient_edges.almd` (byte-compare)<br>`spec/wasm_cross/json_many_keys.almd` (byte-compare)<br>`spec/wasm_cross/codec_decode_error_surface.almd` (byte-compare)<br>`spec/wasm_cross/codec_deep_nesting.almd` (byte-compare)<br>`spec/wasm_cross/codec_doc_array.almd` (byte-compare)<br>`spec/wasm_cross/codec_empty_and_bool.almd` (byte-compare)<br>`spec/wasm_cross/codec_extra_keys.almd` (byte-compare)<br>`spec/wasm_cross/codec_int_float_boundaries.almd` (byte-compare)<br>`spec/wasm_cross/codec_list_list_field.almd` (byte-compare)<br>`spec/wasm_cross/codec_list_default_field.almd` (byte-compare)<br>`spec/wasm_cross/codec_nested_records.almd` (byte-compare)<br>`spec/wasm_cross/codec_option_numeric.almd` (byte-compare)<br>`spec/wasm_cross/codec_string_escapes.almd` (byte-compare)<br>`spec/wasm_cross/codec_variant_roundtrip.almd` (byte-compare)<br>`spec/wasm_cross/codec_whitespace_tolerance.almd` (byte-compare)<br>`spec/wasm_cross/codec_list_default.almd` (byte-compare)<br>`spec/wasm_cross/codec_triple_list.almd` (byte-compare)<br>`spec/wasm_cross/hash_digests.almd` (byte-compare)<br>`spec/stdlib/hash_test.almd` (both-target test) |
 | ALS-T4 | C-129, C-171 | `spec/wasm_cross/list_chunk_windows.almd` (byte-compare)<br>`spec/wasm_cross/list_chunk_zero.almd` (byte-compare)<br>`spec/wasm_cross/list_windows_zero.almd` (byte-compare)<br>`spec/wasm_cross/list_window_zero.almd` (byte-compare)<br>`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)<br>`spec/wasm_cross/io_write_ordering.almd` (byte-compare) |

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 ─

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<f64, Flow> {
     }
 }
 
+/// 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<f32, Flow> {
+    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<bool, Flow> {
     match v {
         Value::Bool(b) => Ok(*b),
@@ -628,12 +659,35 @@ fn dispatch(it: &mut Interp, name: &str, args: Vec<Value>) -> Result<Result<Valu
         "bytes.write_float32" => {
             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<Valu
     };
     let val_at = if is_set { 2 } else { 1 };
     let raw: u64 = if base.starts_with("f32") {
-        (want_float(name, &args[val_at])? as f32).to_bits() as u64
+        obs_bits_f32(want_float(name, &args[val_at])? as f32) as u64
     } else if base.starts_with("f64") {
-        want_float(name, &args[val_at])?.to_bits()
+        obs_bits_f64(want_float(name, &args[val_at])?)
     } else {
         want_int(name, &args[val_at])? as u64
     };

ref/src/stdlib_ext2.rs

@@ -8,6 +8,7 @@ use std::rc::Rc;
 
 use crate::eval::{fnan, Flow, Interp};
 use crate::libm;
+use crate::stdlib_ext::{obs_bits_f32, obs_bits_f64};
 use crate::value::{Value, F64};
 
 pub const EXT2_FNS: &[&str] = &[
@@ -850,7 +851,7 @@ fn dispatch(it: &mut Interp, name: &str, args: Vec<Value>) -> Result<Result<Valu
             let b = want_bytes(name, &args[0])?;
             push_int(
                 &mut b.borrow_mut(),
-                (want_float(name, &args[1])? as f32).to_bits() as u64,
+                obs_bits_f32(want_float(name, &args[1])? as f32) as u64,
                 4,
                 false,
             );
@@ -861,7 +862,7 @@ fn dispatch(it: &mut Interp, name: &str, args: Vec<Value>) -> Result<Result<Valu
             let b = want_bytes(name, &args[0])?;
             push_int(
                 &mut b.borrow_mut(),
-                want_float(name, &args[1])?.to_bits(),
+                obs_bits_f64(want_float(name, &args[1])?),
                 8,
                 true,
             );

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)}")
+  }
+}

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)}")
+  }
 }