Module Sarek_df64

type float32 = float
type df64 = {
  1. hi : float32;
  2. lo : float32;
}

Double-float value: hi + lo with |lo| <= ulp(hi)/2 when normalised.

val sarek_get_df64_hi : df64 -> float32
val sarek_get_df64_lo : df64 -> float32
val df64_type_id : df64 Sarek_ir_types.Type_id.t
val df64_vector_type_id : (df64, unit) Spoc_core.Vector.t Sarek_ir_types.Type_id.t
val df64_make_custom : unit -> df64 Spoc_core.Vector.custom_type
module df64_interp_helpers : sig ... end
val fma : float -> float -> float -> float
val float : int32 -> float
val mul_rn : float32 -> float32 -> float32

a * b, correctly rounded, and - unlike a *. b - not a multiply the backend can fuse into a later add or subtract.

Value-identical to a *. b on every input, with exactly one exception: an EXACTLY zero product (+0.0 *. -1.0 and friends) comes back +0.0 here rather than -0.0, because the fma adds +0.0. A nonzero product that UNDERFLOWS to zero keeps its sign under both forms - the fma rounds the exact product once, so the sign survives. Verified over the signed zeros, infinities, NaN, subnormals and 3e6 random float32 pairs: the exact-zero sign is the only divergence, and it is not observable at any df64 entry point, because the quick_two_sum that closes df64_mul/df64_mul_f32 adds +0.0 to it and yields +0.0 either way.

See the comment block above before changing this.

val two_sum : float32 -> float32 -> df64

Knuth TwoSum: a + b as an exact hi + lo pair. Branch-free, 6 flops.

val quick_two_sum : float32 -> float32 -> df64

Dekker QuickTwoSum: exact hi + lo pair, 3 flops. Requires |a| >= |b| (or a = 0).

val two_prod : float32 -> float32 -> df64

Split-free TwoProd via fma: a * b as an exact hi + lo pair, 3 flops.

val df64_neg : df64 -> df64

Negation, 2 flops.

val df64_add : df64 -> df64 -> df64

Addition (Knuth-robust ieee_add), ~20 flops.

val df64_sub : df64 -> df64 -> df64

Subtraction, ~22 flops.

val df64_add_f32 : df64 -> float32 -> df64

df64 + float32, ~10 flops.

val df64_mul : df64 -> df64 -> df64

Multiplication, ~8 flops (2 of them fma).

val df64_mul_f32 : df64 -> float32 -> df64

df64 * float32, ~7 flops.

val df64_div : df64 -> df64 -> df64

Division (long division, 3 quotient digits), ~70 flops incl. 3 divides.

val df64_sqrt : df64 -> df64

Square root (Karp/Newton correction step), ~10 flops + 1 sqrt. Domain: a >= 0; returns 0 for non-positive a.hi.

val df64_abs : df64 -> df64

Absolute value.

val df64_eq : df64 -> df64 -> bool
val df64_lt : df64 -> df64 -> bool
val df64_le : df64 -> df64 -> bool
val df64_of_float32 : float32 -> df64
val df64_to_float32 : df64 -> float32
val (/) : int32 -> int -> int32
val (*) : int32 -> int -> int32
val (-) : int32 -> int32 -> int32
val df64_of_int32 : int32 -> df64

Exact int32 -> df64 conversion via 16-bit limb split (int32 has up to 31 significant bits, float32 only 24; a df64 holds ~48).

module Host : sig ... end