Fp16 Dtype

[SmoothThunk]

Added support for fp16 in TensorLib.

[seanmcl]

Please make sure you squash all these commits when you merge.

[govereau]

Looks good to me.
May be worth checking if the conversion to and from f16 matches what S0 semantics will want.

[seanmcl]

Review of the fp16 support. The dtype plumbing (itemsize, Npy f2, byte encoders) is mostly fine, but the IEEE-754 fp16<->fp32 conversion core in Float.lean has several correctness bugs, and the new constructor was not fully threaded through the shared infrastructure (isFloat, join, lossless, gen, floatVariant). The added test is vacuous and catches none of it. Inline comments below, ranked roughly by severity.

Additional notes that didn't map cleanly to a changed line:

• floatVariant (Dtype.lean:637) never produces float16. The line-638 branch + TODO admit it should return Dtype.float16 but returns float32, so Tensor.asFloat widens float16 tensors to float32 for all transcendental ops. Not a value-correctness bug (fp32 holds all fp16 values), but the dtype was added without finishing the one place meant to produce it.
• Checked and NOT a bug: liftFloatUnop's _ => throw "operation requires a float type" looks like it rejects float16 for sin/cos/etc., but Ufunc.asFloat promotes float16 -> float32 first (via floatVariant), so the Dtype-level catch-all is never reached on the public path.
• Minor: the doc comment on byteArrayToFloat16AsFloat32 (Dtype.lean:382) describes the whole arithmetic round-trip, not what the function does; | .float16, .float16 => impossible (line 555) could fold into the existing combined impossible arm; and the new code mixes Unicode <--arrow style (the castOverflow / helper lines use the Unicode arrow while the surrounding file uses ASCII <-).

Suggested direction: rewrite the two conversion functions with explicit zero / subnormal / normal / Inf / NaN cases in both directions, round-to-nearest-even on narrowing, a corrected 0x1F exponent test and <<< 31 sign placement; then thread float16 through isFloat / join / lossless / gen / floatVariant, and replace the arange test with one that decodes non-trivial values.

[seanmcl]

I ran the generic /code-review on the PR. If something was already broken, feel free to just push back. A "TODO" comment would be great in those cases.

[seanmcl]

Review of the revision. The conversion rewrites fix the headline bugs from the first round (correct 0x1F Inf/NaN test, <<< 31 sign placement, subnormal decode, NaN payload preservation, isFloat/gen/floatVariant/lossless/join threading). Three real correctness issues remain, plus a few minor items.

Summary of remaining issues:

1. UInt32 shift wraparound in the subnormal fp32→fp16 encoder (confirmed concrete counterexample)
2. Two property-based tests are wrong — the lossless round-trip PBT is logically falsified by float16, and the add-zero identity PBT fails for fp16 -0.0
3. NaN decoder drops sign bit (behavioral divergence from NumPy)
4. Several dead arms in join and an unused !-variant helper

[seanmcl]

Review of revision 3. The fixes from the prior round all landed correctly:

• UInt32 shift-wraparound guarded at totalShift >= 25 ✓
• NaN decoder preserves sign bit ✓
• Add-zero PBT extended with -0 escape (f == 0) ✓
• Lossless PBT range-guarded with maxSafeNat ✓
• Dead join arms (float16/float16, float16/bool, etc.) removed ✓
• byteArrayToFloat16AsFloat32, byteArrayToFloat16!, byteArrayOfFloat16! all removed ✓
• Tests extended with below-subnormal values ✓

Two remaining issues:

1. (Bug) Self-cast PBT still unguarded — the pre-existing property example (dtype : Dtype) (n : Nat) : canCastLosslessIntRoundTrip dtype n dtype (Dtype.lean line 965, inside the Test section, not in this diff) is now falsified by float16 being added to gen. For dtype = float16, n = 2049: byteArrayOfInt .float16 2049 fails the range check (2049 > maxSafeNatForFloat16 = 2048), so canCastLosslessIntRoundTrip returns false — a genuine counterexample. The lossless PBT at line 974 got the maxSafeNat guard; this one didn't. Plausible's Nat generator uses small sizes by default and won't find 2049, but the property is logically wrong. Fix: add the same guard — if n > dtype.maxSafeNat.getD n then true else canCastLosslessIntRoundTrip dtype n dtype.

2. (Minor) Dead catch-all arm in join — see inline comment.

The implementation itself looks correct. The totalShift >= 25 guard is right (verified: the rounding at totalShift=24 produces correct IEEE RNE behavior), and the NaN sign fix is consistent with NumPy.

[seanmcl]

Would good to tal at the last couple comments, but looks solid now.