JS backend violates a machine-checked theorem: F32 does not preserve signaling-NaN bits (found by opus 4.8)

(Bug found and report composed by Opus 4.8)

What you did

bend nan.bend            # checks, then runs main   (also: bend nan.bend -o nan.js && node nan.js)

What happened

bend nan.bend prints All terms check. — including a proof of

def theorem() -> {roundtrip() == sNaN() : U32}:
  {==}

i.e. the checker certifies roundtrip() == 2139095041. But running the program prints

2143289345

A term the checker proved equal to 2139095041 evaluates to 2143289345 at runtime. The machine-checked theorem is false in the compiled program, so LAWS.bend's core promise — "a proven property can't be violated" — does not hold on the JS backend.

The file

import Base

# F32 is F32{data: Word(32n)}, so reinterpreting a U32's 32 bits as an F32
# and back is the identity on the 32-bit word.
def as_f32(u: U32) -> F32:
  U32{w} = u
  F32{w}
def bits(f: F32) -> U32:
  F32{w} = f
  U32{w}

def sNaN() -> U32:            # 0x7f800001, a signaling NaN
  {2139095041 : U32}
def roundtrip() -> U32:
  bits(as_f32(sNaN()))

# machine-checked: the round-trip leaves the bits unchanged
def theorem() -> {roundtrip() == sNaN() : U32}:
  {==}

# but the compiled program prints 2143289345 (0x7fc00001)
def main() -> IO(Unit):
  IO.print(U32.show(roundtrip()))

bend --version

bend 2.0.5

uname -sm

Linux x86_64

clang --version (the first line)

clang version 22.1.8 — (not relevant: the C backend is unaffected)

Root cause

bend2/comp.ts, OPTIMIZED.F32, represents an F32 on the JS lane as a native JS number:

F32: {
  intr: { F32: "f32_from_bits(word_to_u32($0))" },   // construct: Word -> u32 -> native float
  elim: { F32: ["u32_to_word(f32_bits($0))"] },       // destructure: native float -> u32 -> Word
},

So bits(as_f32(u)) lowers to f32_bits(f32_from_bits(u)). That round-trip is not the identity for a signaling NaN, because a float32 sNaN cannot survive a load into / store from a JS number (Float32Array/Uint32Array): the quiet bit gets set.

0x7f800001  --f32_from_bits/f32_bits-->  0x7fc00001   (quiet bit set)
0x7fa00000  -->  0x7fe00000
0x7fffffff  -->  0x7fc00000
0x80000000 (-0), 0x7f800000 (+inf), finite values:  preserved

The checker (bend2/bend.ts) has no native-float representation — it keeps an F32 as its Word(32n) and never converts to a machine float — so at the type level bits(as_f32(u)) = u exactly, and the proof of theorem goes through. The checker's model of F32 (an exact 32-bit word) and the JS backend's model (a native double) disagree, and the disagreement is observable from proven code.

Scope

• JS lane only: bend f.bend -o f.js, the bun/node .bend loader, and the browser bundler.
• C lane is fine: f32_from_bits/f32_bits are bit-casts there, which preserve the pattern. Verified locally — 0x7f800001 round-trips unchanged through both a memcpy bitcast and an f32 register on x86_64.
• The hosted lab (lab.js) is also fine, because it evaluates the game with the checker's own reducer (term_snf) rather than compiling it — there is no native float there. The gap is specific to programs that actually go through the JS code generator.