Separating symbolic and concrete floats

kmir/src/kmir/kdist/mir-semantics/rt/data.md

@@ -1414,6 +1414,11 @@ Boolean values can also be cast to Integers (encoding `true` as `1`).
 
 Casts involving `Float` values: `IntToFloat`, `FloatToInt`, and `FloatToFloat`.
 
+These rules use FLOAT hooks (`Int2Float`, `Float2Int`, `roundFloat`) which are not implemented
+in the haskell backend directly. However, the booster delegates FLOAT hook evaluation to the LLVM
+shared library, so these rules must be present in both definitions. The FLOAT hooks inside are
+evaluated by the LLVM library when the booster encounters them.
+
 ```k
   // IntToFloat: convert integer to float with the target float type's precision
   rule <k> #cast(Integer(VAL, _WIDTH, _SIGNEDNESS), castKindIntToFloat, _, TY)
@@ -1604,6 +1609,45 @@ representations of the source and target types are somewhat relatable (or else,
 Support for `castKindTransmute` in this semantics is very limited because of the high-level data model applied.
 What can be supported without additional layout consideration is trivial casts between the same underlying type (mutable or not).
 
+#### Float transmute guard
+
+The semantics does not support byte-level reinterpretation of float values (e.g. `transmute::<f16, u16>()`).
+Without these guard rules, a `castKindTransmute` involving a float type would cause non-deterministic
+branching on the symbolic value's constructor. These rules intercept at the `rvalueCast` level,
+before `#cast` is created, and produce an error that stops the branch cleanly. This applies to both concrete
+and symbolic operands on all backends currently.
+
+```k
+  syntax MIRError ::= "#UnsupportedFloatTransmute"
+
+  // Target type is float
+  rule <k> rvalueCast(castKindTransmute, _OP:Operand, TY) ~> _REST
+          => #UnsupportedFloatTransmute
+       </k>
+    requires #isFloatType(lookupTy(TY))
+    [priority(40)]
+
+  // Source type is float (operandCopy)
+  rule <k> rvalueCast(castKindTransmute, operandCopy(place(local(I), PROJS)), _TY) ~> _REST
+          => #UnsupportedFloatTransmute
+       </k>
+     <locals> LOCALS </locals>
+    requires 0 <=Int I andBool I <Int size(LOCALS)
+     andBool isTypedLocal(LOCALS[I])
+     andBool #isFloatType(lookupTy({getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)}:>Ty))
+    [priority(40), preserves-definedness]
+
+  // Source type is float (operandMove)
+  rule <k> rvalueCast(castKindTransmute, operandMove(place(local(I), PROJS)), _TY) ~> _REST
+          => #UnsupportedFloatTransmute
+       </k>
+     <locals> LOCALS </locals>
+    requires 0 <=Int I andBool I <Int size(LOCALS)
+     andBool isTypedLocal(LOCALS[I])
+     andBool #isFloatType(lookupTy({getTyOf(tyOfLocal({LOCALS[I]}:>TypedLocal), PROJS)}:>Ty))
+    [priority(40), preserves-definedness]
+```
+
 ```k
   rule <k> #cast(Reference(_, _, _, _) #as REF, castKindTransmute, TY_SOURCE, TY_TARGET) => REF ... </k>
       requires lookupTy(TY_SOURCE) ==K lookupTy(TY_TARGET)

kmir/src/kmir/kdist/mir-semantics/rt/decoding.md

@@ -51,12 +51,17 @@ and arrays (where layout is trivial).
   rule #decodeValue(BYTES, TYPEINFO) => #decodeInteger(BYTES, #intTypeOf(TYPEINFO))
     requires #isIntType(TYPEINFO) andBool lengthBytes(BYTES) ==Int #elemSize(TYPEINFO)
      [preserves-definedness]
+```
+
+Float decoding dispatches to `#decodeFloat` in `numbers.md` which uses FLOAT hooks (concrete only).
 
-  // Float: handled in separate module for numeric operations
+```{.k .concrete}
   rule #decodeValue(BYTES, TYPEINFO) => #decodeFloat(BYTES, #floatTypeOf(TYPEINFO))
     requires #isFloatType(TYPEINFO) andBool lengthBytes(BYTES) ==Int #elemSize(TYPEINFO)
     [preserves-definedness]
+```
 
+```k
   // TODO Char type
   // rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), typeInfoPrimitiveType(primTypeChar)) => typedValue(Str(...), TY, mutabilityNot)
 ```

kmir/src/kmir/kdist/mir-semantics/rt/numbers.md

@@ -220,7 +220,12 @@ The bytes are first converted to a raw integer, then the sign, biased exponent,
 are extracted. The value is reconstructed using K's `Int2Float` and float arithmetic, with a
 high-precision intermediate to avoid overflow when reconstructing subnormals and small normal values.
 
-```k
+Float decoding uses FLOAT hooks (`Int2Float`, `Rat2Float`, `--Float`) which are not implemented
+in the haskell backend. These rules are placed in a `concrete` block so they are only included
+in the LLVM definition. For the haskell definition, `#decodeFloat` will not reduce and
+the `#decodeValue` fallback rule will produce `UnableToDecode`.
+
+```{.k .concrete}
   syntax Value ::= #decodeFloat ( Bytes, FloatTy ) [function]
   // --------------------------------------------------------
   rule #decodeFloat(BYTES, FLOATTY) => #decodeFloatRaw(Bytes2Int(BYTES, LE, Unsigned), FLOATTY)
@@ -290,7 +295,7 @@ For positive exponents, shift the significand left and convert directly.
 For negative exponents, use `Rat2Float` to convert the exact rational
 `SIG / 2^|AEXP|` to the target float precision.
 
-```k
+```{.k .concrete}
   syntax Float ::= #reconstructFloat ( sig: Int, adjExp: Int, FloatTy ) [function]
   // -------------------------------------------------------------------------------
   rule #reconstructFloat(SIG, AEXP, FLOATTY)

kmir/src/tests/integration/data/exec-smir/floats/float_arith.rs

@@ -0,0 +1,47 @@
+#![feature(f16)]
+#![feature(f128)]
+
+fn main() {
+    // f16
+    assert!(1.5_f16 + 2.5_f16 == 4.0_f16);
+    assert!(5.0_f16 - 1.5_f16 == 3.5_f16);
+    assert!(2.0_f16 * 3.0_f16 == 6.0_f16);
+    assert!(7.0_f16 / 2.0_f16 == 3.5_f16);
+
+    // f32
+    assert!(1.5_f32 + 2.5_f32 == 4.0_f32);
+    assert!(5.0_f32 - 1.5_f32 == 3.5_f32);
+    assert!(2.0_f32 * 3.0_f32 == 6.0_f32);
+    assert!(7.0_f32 / 2.0_f32 == 3.5_f32);
+
+    // f64
+    assert!(3.5_f64 + 1.5_f64 == 5.0_f64);
+    assert!(3.5_f64 - 1.5_f64 == 2.0_f64);
+    assert!(3.5_f64 * 1.5_f64 == 5.25_f64);
+    assert!(10.0_f64 / 2.0_f64 == 5.0_f64);
+
+    // f128
+    assert!(1.5_f128 + 2.5_f128 == 4.0_f128);
+    assert!(5.0_f128 - 1.5_f128 == 3.5_f128);
+    assert!(2.0_f128 * 3.0_f128 == 6.0_f128);
+    assert!(7.0_f128 / 2.0_f128 == 3.5_f128);
+
+    // Modulo (truncating)
+    assert!(7.0_f16 % 4.0_f16 == 3.0_f16);
+    assert!(7.0_f32 % 4.0_f32 == 3.0_f32);
+    assert!(7.0_f64 % 4.0_f64 == 3.0_f64);
+    assert!(7.0_f128 % 4.0_f128 == 3.0_f128);
+
+    // Subnormal constant literals
+    let sub_16: f16 = 5.96e-8_f16;       // below f16 min normal (6.1e-5)
+    assert!(sub_16 + sub_16 == sub_16 * 2.0_f16);
+
+    let sub_32: f32 = 1.0e-45_f32;       // below f32 min normal (1.2e-38)
+    assert!(sub_32 + sub_32 == sub_32 * 2.0_f32);
+
+    let sub_64: f64 = 5e-324_f64;        // below f64 min normal (2.2e-308)
+    assert!(sub_64 + sub_64 == 1e-323_f64);
+
+    let sub_128: f128 = 1.0e-4933_f128;  // below f128 min normal (~3.4e-4932)
+    assert!(sub_128 + sub_128 == sub_128 * 2.0_f128);
+}