Repository navigation
Conversation
Lorenzobattistela
left a comment
There was a problem hiding this comment.
Checked on main 2e9722d: the four new cases print True on the native binary, the .js build and inside a bang, and the full test suite passes. A few things to fix in the reference body:
-
The new body only works because the intrinsic shadows it. F32.read is host-only: on device, f32_read posts ERR_FIDS (comp.ts:360). If the f32_from_nat lookup ever misses (a rename of F32.from_nat, a flag on the def), F32.from_nat inside a bang would fail at runtime on Metal/CUDA instead of returning a value. The old body was plain arithmetic and ran anywhere. Please keep the reference body free of host-only primitives: either split into word halves like F32.to_nat.wide does, or declare it as a law the way U32.to_f32 is.
-
The F32.div(0.0, 0.0) fallback can't be reached: F32.read always accepts what Nat.show produces. It reads as if some Nat could become NaN, and if F32.read ever regressed it would hide the failure as a NaN. Please drop it along with the change above.
-
The test can't see the body, since every lane runs the cast. Please add a call inside a bang (e.g. f!(…) over the same four inputs) so the device cast from a 64-bit Nat to f32 on Metal/CUDA is pinned too, plus one small value (e.g. 16777217 -> 16777216) for the old range.
|
Went with a law, like Merged |
|
@Lorenzobattistela this is back under the cap: 65,989/66,000 after merging |
YidaWeng
left a comment
There was a problem hiding this comment.
Independent verification on main 295e9965 plus this diff:
- Issue reproducer:
0before,2^32after.F32.bits(F32.from_nat(2^32))is1333788672(0x4F800000) on native C, Bun and Node. - Boundary sweep (31 values around 2^24, 2^32 and 2^48-1): C, Bun and Node agree bit-for-bit.
tests/base41/41 runnable tests pass on both the C and JS lanes;num_kitand the U32/Nat/F32 controls pass.comp.tsis65,989 / 66,000tokens;bun gates/repo.tsisPASS: 54 / 54with the new test tracked.--checkupprints the ten expectedTrues;-o .bendttsucceeds and the law goes out opaque with a valid model.- Note for the reproducer:
F32.showprints4294967300for 2^32 (its 9-significant-digit round-trip form), so the issue's display is expected; the test'sF32.is_eqis the right check.
Not run here: Metal/CUDA, the cluster gates/test.ts/gates/safe.ts, and the Lean kernel. The ! case is there for the M4 gate. LGTM pending that.
Fixes #1609.
F32.from_natkeeps the full Nat instead of narrowing through U32. It is a law with a direct intrinsic, likeU32.to_f32; no host-onlyF32.reador NaN fallback.Merged main
aee1b1f. The cap blocker is gone:comp.tsis 65,989 / 66,000 tokens and repo-gate passes 54/54. The four cast rules share the existingtpl_ops; no caps changed or code moved out.All five cases, both ordinary and inside
!, pass on native CPU, Bun and Node. Four existing U32/Nat/float control programs also match their expected output on the interpreter, native CPU and compiled JS on both hosts. Native runs use the new+RTSoption brackets.I have not run Metal, CUDA or the private mini-cluster suite.