Sarek_df64.Hostval encode : float -> df64Dekker split of a binary64 value into a df64 pair at f32 precision: hi carries the leading 24 bits, lo the next 24.
val decode : df64 -> floatBack to binary64: exact since both halves are f32 values.
val two_sum : float -> float -> df64val quick_two_sum : float -> float -> df64val two_prod : float -> float -> df64