I'm trying to figure out how to use the flocq package. Below I have a simple script where I created a simple function. However I can't figure out how to create two binary32's that I can use to evaluate this function. I get stuck on how to create the proof of "bounded". I'd also like to be able to prove that, for example, for a particular x and y I won't get a NaN. Is this the sort of thing that flocq is good for? Or might there be another package I should look into? Any help is appreciated!
Require Import Psatz.
From Flocq Require Import Fcore_FTZ Fcore Fcalc_ops Fappli_IEEE Fappli_IEEE_bits.
Definition b32_my_fun (x y : binary32) : binary32 :=
b32_div mode_NE (b32_plus mode_NE x y) y.
I cobbled this answer together by exploring the copy of flocq that is included in CompCert. You may be interested in looking at CompCert's lib/Floats.v and especially lib/Fappli_IEEE_extra.v which layer some convenience functions on top of flocq. (This also means that my answer might not be applicable to vanilla flocq, but I think it should.)
To create a binary32, use flocq's binary_normalize function from Fappli_IEEE. Here is its type:
binary_normalize
: forall prec emax : Z,
Prec_gt_0 prec -> prec < emax -> mode -> Z -> Z -> bool -> binary_float prec emax
For a 32-bit IEEE float, prec is 24 (bits of precision in the mantissa) and emax is 128 (the maximal value of the exponent). The mode argument is the rounding mode, mode_NE should be a reasonable choice. The two Z arguments are the values of the mantissa and the exponent, respectively; the final bool appears to be the sign to use if the mantissa is 0.
So for a 32-bit float with mantissa 42 and exponent 32, we can try the following:
Check (binary_normalize 24 128 _ _ mode_NE 42 23 false).
binary_normalize 24 128 ?prec_gt_0_ ?Hmax mode_NE 42 23 false
: binary_float 24 128
where
?prec_gt_0_ : [ |- Prec_gt_0 24]
?Hmax : [ |- 24 < 128]
It remains to provide proofs of two simple goals: Prec_gt_0 24 and 24 < 128. In interactive mode, both of these can be proved simply by reflexivity:
Goal Prec_gt_0 24.
Proof.
reflexivity.
Qed.
The proof term for such proofs is simply eq_refl (as you can check with Show Proof. before the Qed., for example). So we arrive at:
Check (binary_normalize 24 128 eq_refl eq_refl mode_NE 42 23 false).
binary_normalize 24 128 eq_refl eq_refl mode_NE 42 23 false
: binary_float 24 128
And we can look at the real internal representation of this:
Eval simpl in (binary_normalize 24 128 eq_refl eq_refl mode_NE 42 23 false).
= B754_finite 24 128 false 11010048 (FLT_exp (-149) 24 29)
(proj1 (binary_round_correct 24 128 eq_refl eq_refl mode_NE false 42 23))
: binary_float 24 128
Eval compute in (binary_normalize 24 128 eq_refl eq_refl mode_NE 42 23 false).
= B754_finite 24 128 false 11010048 5
(proj1 (binary_round_correct 24 128 eq_refl eq_refl mode_NE false 42 23))
: binary_float 24 128
And finally we can package this in a nice little function:
Definition my_binary32 (mantissa exponent: Z): binary32 :=
binary_normalize 24 128 eq_refl eq_refl mode_NE mantissa exponent false.
And test it:
Eval simpl in (my_binary32 42 23).
= B754_finite 24 128 false 11010048 (FLT_exp (-149) 24 29)
(proj1 (binary_round_correct 24 128 eq_refl eq_refl mode_NE false 42 23))
: binary32
Eval simpl in (my_binary32 42 230).
= B754_infinity 24 128 false
: binary32