Fp8_e2m5 dtype support

[SmoothThunk]

Adds fp8_e2m5 (P3109_8p6) dtype:

• 1 sign + 2 exponent + 5 mantissa, bias=1
• Max=3.875, min normal=0.5, min subnormal=0.015625
• 2 infs (+inf=byte 127, -inf=byte 255), 1 NaN (byte 128), no negative zero
• Bit-exact encoder/decoder verified against gfloat (P3109_8p6)
• Exhaustive 253/256 round-trip (NaN and infs excluded due to Lean fp32 limitations)
• Added cases in join, lossless, castOverflow, and arithmetic
• Guard tests added for +0, -0(NaN), min subnormal (0.015625), min normal (0.5), 1.0, 0.984375, max normal (3.875), +inf
• IO tests for arithmetic, casting, overflow, and inf

[SmoothThunk]

Code review findings (recall-biased, ranked most-severe first).

1. Encoder subnormal flush cutoff is off-by-one — TensorLib/Float.lean:753

The guard if totalShift >= 24 then 0 flushes fp32 values in [2^-7, 2^-6) with any nonzero mantissa bits straight to +0 when they should round up to byte 1 (0.015625, the min subnormal).

Trace: fp32 0.01 has exp=120, so realExp = -7, giving totalShift = 24 — the encoder returns 0 instead of 1. Compare with the analogous e5m2 encoder (line ~504) which uses >= 25. Any fp32 value with exp=120 and nonzero mantissa loses its magnitude entirely.

2. Ndarray.save! missing guard for float8_e2m5 — TensorLib/Npy.lean:435

The existing guard blocks saving .float8_e3m4 because it shares the V1 descriptor with e4m3 (readback ambiguity), but this diff added .float8_e2m5 to the same V1 bucket (line 117) without extending the guard.

Impact: saving an e2m5 Ndarray writes <V1 and reads back as e4m3 (per fromNpyString at line 137), silently reinterpreting every byte with a different float format on load.

3. Finite values just below 3.9375 encode as +inf instead of the max finite byte 126 — TensorLib/Float.lean:744

Values like 3.92 round the 5-bit mantissa up to 31 with e2m5Exp = 3, producing magnitude = 127, and the guard if magnitude >= 127 then …0x7F sends them to +inf.

Trace: fp32 3.92 (bits 0x407AE148, realExp=1, mant=0x7AE147) → truncated=30, roundBit=1, sticky != 0 → rounded=31 → magnitude=127 → encoder returns 0x7F. But 3.92 is closer to 3.875 (byte 126) than to any other representable value, so under round-to-nearest it should encode to byte 126. The whole interval (3.875 + eps, 3.9375) is lost to +inf, breaking arithmetic near max.

4. e2m5 arithmetic case bodies under-indented — TensorLib/Dtype.lean:762 (also 801, 841, 881)

The let/return under | .float8_e2m5 => do sit at column 3, while every neighboring fp8 case body uses column 5. Not a syntax error, but inconsistent with the file's convention, and commit dd434ad specifically fixed indentation in this same file.

5. Test comment misdescribes byte 128 decode — TensorLib/Float.lean:924

Comment claims "decodes to fp32 -0 (0x80000000)" but the #guard correctly asserts NaN (0x7FC00000). Byte 128 is documented elsewhere in the same file (line 663) as the single NaN encoding, not -0. Doc rot.

6. Roundtrip-test skip comment names the wrong bytes as NaN — TensorLib/Float.lean:947

Comment says "Bytes 127 and 255 are NaN encodings" but per the format 127 = +inf, 255 = -inf, 128 = NaN. The filter itself also unnecessarily excludes 127/255 — their roundtrip should hold under normal Float32 BEq, so filtering hides any future regression in inf encoding from the exhaustive coverage.

7. Promotion-table comment contradicts the code — TensorLib/Dtype.lean:202

Comment claims e2m5 "promotes with bool/int8/uint8 to fp32," but the code returns float8_e2m5 for those pairings (matching the e4m3/e3m4 pattern). The code is fine; the annotation is factually wrong.

[SmoothThunk]

Fixes:

• Changed the threshold from >= 24 to >= 25 so values above half the min subnormal (like 0.01) round up to byte 1 instead of being flushed to zero. Verified against gfloat with ties to even; 0.008+ rounds to code 1, 0.0078125 (exact midpoint) rounds to 0 (ties to even).
• Fixed; added e2m5 to both the Ndarray.save! and toNpy guards since it shares the same V1 descriptor ambiguity as e3m4. Also added a #guard asserting toNpy errors for e2m5.
• Verified against gfloat (TiesToEven): 3.92 correctly encodes to +inf (byte 127). The midpoint between max finite (3.875) and +inf is 3.90625; values above this round to inf per IEEE. gfloat confirms 3.9 -> code 126 (3.875), 3.90625 -> code 126 (ties to even), > 3.907 -> code 127 (inf). So our encoder matches this.
• Fixed indentation
• Updated comment
• Fixed comment (127/255 are inf, not NaN) and removed them from the exclusion list only byte 128 (NaN) is excluded. Inf round-trips under Lean's BEq so it's covered by the exhaustive test.
• Fixed comment on promotion between fp8_e2m5 and int/uint/x etc.

[SmoothThunk]

Re-reviewed at 68c4649. Fixes for the subnormal flush threshold, save!/toNpy guards, arithmetic indentation, and the wrong-comment items all landed cleanly and check out. Two items remain / just showed up.

1. (Still open) Finite values near the max still encode to +inf — TensorLib/Float.lean:744

Not addressed in this revision. Trace at HEAD 68c4649:

• fp32 3.9375 (halfway between max 3.875 and 4.0, bits 0x407C0000, realExp=1, mant=0x7C0000) → truncated=31, roundBit=0, sticky=0 → rounded=31 → e2m5Exp=3, finalMant=31 → magnitude = (3<<5)|31 = 127 → the if magnitude >= 127 then …0x7F guard emits +inf (byte 127). Under round-to-nearest-even the LSB neighbors are byte 126 (mant=30, even) and inf (mant=31, odd), so this should tie down to 3.875 (byte 126).
• fp32 3.91 (bits ~0x407A3D71, realExp=1, mant=0x7A3D71) → truncated=30, roundBit=1, sticky!=0 → rounded=31 → same path → emits +inf. But |3.91 − 3.875| = 0.035 is smaller than |3.91 − 4.0| = 0.09, so nearest-representable is byte 126.

Concretely, everything in (3.90625, 4.0) that this branch reaches gets clamped to +inf instead of to 3.875. The > 0x1F overshoot handler on line 738 bumps e2m5Exp on the assumption that (exp, mant=31) with exp=3 is a legal encoding, but that slot is +inf. Two fixes to consider:

• After the rounding step, if e2m5Exp == 3 && rounded == 31, saturate the mantissa to 30 instead of promoting the exponent — i.e., produce byte 126 rather than byte 127.
• Alternatively, do the round-up bump conditionally: only bump exponent when e2m5Exp < 3; otherwise saturate to max finite.

Worth adding a targeted #guard for 3.9375, 3.9, and a value just under 4.0 to the encode test block once fixed.

2. (New) Stale comment on byte-96 decode guard — TensorLib/Float.lean:934

-- Takes byte 96 (0b01100000 = sign=0, exp=11, mant=00000), decodes to +inf
#guard (96 : UInt8).toFloat32FromFloat8E2M5 == Float32.ofBits 0x40000000 -- 2.0 (exp=3, mant=0 is normal, not inf)

Header line says "decodes to +inf" but the assertion (and the trailing note on the same line) correctly says 2.0. The header should read "decodes to 2.0 (exp=3, mant=0 is the largest normal-range exponent, not the inf slot)". Byte 127 (exp=3, mant=31) is +inf; byte 96 is not.

Nit: the four targeted decode-then-encode #guards that were dropped in this revision (bytes 1/2/16/31) are already covered by the exhaustive round-trip, so this cleanup is fine — no action needed there.

[SmoothThunk]

Fixes:

• Verified against gfloat (TiesToEven) and our encoder matches. 3.90625 -> code 126 (ties to even, rounds down to max finite), 3.9375 -> code 127 (inf). The midpoint between max finite (3.875) and inf is 3.90625; values above this correctly round to inf per IEEE semantics. Added #guard tests for both boundary values.
• Fixed comment

[SmoothThunk]

Re-reviewed at cdabdf2.

Status of prior findings

• Subnormal flush threshold (Float.lean:753, >= 24 → >= 25): fixed. Traced 0.01 (fp32 exp=120), which now correctly rounds to byte 1 (min subnormal 0.015625). Halfway case 2^-7 still ties to 0 (even). Good.
• toNpy / Ndarray.save! guards for float8_e2m5: fixed, plus a new #guard in Tensor.lean covers the toNpy path.
• Arithmetic case indentation for .float8_e2m5 in add/sub/mul/div: fixed.
• Wrong comments on byte-128 decode, roundtrip-skip filter, byte-96 decode, promotion table for e2m5: all corrected.

On the overflow-to-inf concern I flagged last round

Withdrawing this one. Re-checked against IEEE round-to-nearest-even overflow semantics: the "overflow threshold" is max_finite + 0.5 * ulp(max_finite). For e2m5 that's 3.875 + 0.03125 = 3.90625. Values >= that round to +inf; at exactly 3.90625 ties-to-even picks the even mantissa (30, i.e. byte 126). The encoder does exactly this — my earlier "nearest-neighbor" reasoning was wrong. The two new #guards at lines 946-947 (3.90625 → 126, 3.9375 → 127) pin down this behavior nicely.

Remaining nits (not blockers)

1. Typo promotoes → promotes — TensorLib/Dtype.lean:202. Comment introduced in this PR.
2. Typo rountrip → roundtrip — TensorLib/Float.lean:53. Comment introduced in this PR.
3. Optional test polish — TensorLib/Float.lean:946-947. The two new near-max encode #guards pair nicely; consider also adding a negative-side pair (e.g. Float32.ofBits 0xC07A0000 → 254, Float32.ofBits 0xC07C0000 → 255) to lock in symmetric behavior at the negative overflow boundary. Not required — the exhaustive roundtrip covers it in one direction, but the encode direction from finite-fp32-just-above-max on the negative side isn't asserted anywhere.

Nothing correctness-level open on my side.

[SmoothThunk]

Re-reviewed the working-tree changes on top of cdabdf2 (not yet committed/pushed as of comment time — reviewed against the pending diff).

Status of prior nits

1. Typo promotoes → promotes at TensorLib/Dtype.lean:202 — fixed.

2. Typo rountrip → round trip at TensorLib/Float.lean:53 — fixed.

3. Negative-side boundary encode #guards added at TensorLib/Float.lean:942-943:

   • 0xC07A0000 (-3.90625) → byte 254 (-3.875, ties to even)
   • 0xC07C0000 (-3.9375) → byte 255 (-inf)

   Traced both manually: sign8=0x80, magnitudes 126/127 respectively → OR'd with sign gives 254/255. Matches the positive-side pair and locks in symmetric IEEE RNE overflow behavior at the negative boundary.

Nothing else on my end. Just a note that these changes are still local (working tree) at the time of this review — push cdabdf2's successor commit for them to land on the PR.

[SmoothThunk]

Fixes:

• Fixed typos in Dtype and Float.lean
• Added guards

[SmoothThunk]

Confirmed the pushed commit (f9070e8) matches the working-tree diff I reviewed last round. All three items landed:

• promotoes → promotes at TensorLib/Dtype.lean:202
• rountrip → round-trip at TensorLib/Float.lean:53
• Negative-boundary #guards at TensorLib/Float.lean:942-943 (−3.90625 → 254, −3.9375 → 255)

No open items from my side. LGTM.