Finished adapting VSTlib to gentype branch of vcfloat

lib/proof/spec_math.v

@@ -449,13 +449,25 @@ destruct (float_of_ftype x), (float_of_ftype y); auto; try tauto;
 try discriminate.
 Qed.
 
-Definition fma_ff (t: type) `{STD: is_standard t}  : floatfunc  [ t;t;t ] t (fma_bnds t) (fun x y z => x*y+z)%R.
-apply (Build_floatfunc [t;t;t] t _ _ 
-         (fun x y z => ftype_of_float (Binary.Bfma (fprec t) (femax t) (fprec_gt_0 t) (fprec_lt_femax t) 
-               (fma_nan t) BinarySingleNaN.mode_NE
-              (float_of_ftype x) (float_of_ftype y) (float_of_ftype z)))
-           1%N 1%N).
--
+Ltac binary_float_equiv_cases H := 
+ match type of H with binary_float_equiv ?ah ?bh =>
+   destruct ah as [ [|] | [|] | | [|] ? ?] ; 
+   destruct bh as [ [|] | [|] | | [|] ? ?] ; 
+   simpl in H;
+   try match type of H with _ /\ _ /\ _ => destruct H as [? [? ?]]; subst end;
+   simpl in *; auto; try contradiction; try discriminate
+ end.
+
+Lemma fma_ff_aux1:
+ forall (t : type) (STD : is_standard t),
+ acc_prop [t; t; t] t 1 1 (fma_bnds t) (fun x y z : RR t => (x * y + z)%R)
+   (fun x y z : ftype' t =>
+    ftype_of_float
+     (Binary.Bfma (fprec t) (femax t) (fprec_gt_0 t) (fprec_lt_femax t) 
+        (fma_nan t) BinarySingleNaN.mode_NE (float_of_ftype x) 
+        (float_of_ftype y) (float_of_ftype z))).
+Proof.
+intros.
 intros x ? y ? z ?.
 rewrite <- !B2R_float_of_ftype.
 split3; [ tauto | intro Hx; inv Hx | ].
@@ -493,14 +505,25 @@ set (u := Rabs _) in *.
 set (v := Raux.bpow _ _) in *.
 clear - FIN H3.
 Lra.lra.
--
-hnf; intros.
+Qed.
+
+
+Lemma fma_ff_aux2:
+ forall (t : type) `(STD : is_standard t),
+ @floatfunc_congr [t; t; t] t
+  (fun x y z : ftype' t =>
+    ftype_of_float
+     (Binary.Bfma (fprec t) (femax t) (fprec_gt_0 t) (fprec_lt_femax t)
+        (@fma_nan nans t STD) BinarySingleNaN.mode_NE (@float_of_ftype t STD x)
+        (@float_of_ftype t STD y) (@float_of_ftype t STD z))).
+Proof.
+intros; hnf; intros.
 inv H. apply inj_pair2 in H2,H3.  subst. 
 inv H5. apply inj_pair2 in H1,H2.  subst.
 inv H6. apply inj_pair2 in H1,H2.  subst.
 inv H7. apply inj_pair2 in H,H0.  subst.
 
-rewrite float_equiv_binary_float_equiv in H4, H3, H5.
+rewrite (float_equiv_binary_float_equiv _ STD) in H4, H3, H5.
 destruct t; destruct nonstd; try contradiction; simpl in *.
 unfold eq_rect_r, eq_rect, eq_sym; simpl.
 unfold eq_rect_r, eq_rect, eq_sym; simpl.
@@ -512,27 +535,23 @@ set (J1 := fprec_lt_femax _) in *.
 set (prec := FPCore.fprec _) in *.
 unfold FPCore.femax in *.
 clearbody J0. clearbody J1.
-
-XXXXX.  
-
-simpl ftype in *.
-fold prec in J1, J0.
-unfold FPCore.fprec in *.
-Print BFMA.
-s
-
-Locate BFMA.
-red.
-clear STD.
-
-destruct ah; try destruct s; destruct bh; try destruct s; simpl in *; auto; try contradiction;
- destruct H4 as [? [? ?]]; try discriminate; subst; repeat proof_irr;
+binary_float_equiv_cases H4;
+binary_float_equiv_cases H3;
+binary_float_equiv_cases H5;
 apply binary_float_equiv_refl.
-Defined.
+Qed.
 
+Definition fma_ff (t: type) `{STD: is_standard t}  : floatfunc  [ t;t;t ] t (fma_bnds t) (fun x y z => x*y+z)%R.
+apply (Build_floatfunc [t;t;t] t _ _ 
+         (fun x y z => ftype_of_float (Binary.Bfma (fprec t) (femax t) (fprec_gt_0 t) (fprec_lt_femax t) 
+               (fma_nan t) BinarySingleNaN.mode_NE
+              (float_of_ftype x) (float_of_ftype y) (float_of_ftype z)))
+           1%N 1%N).
+apply fma_ff_aux1.
+apply fma_ff_aux2.
 Defined.
 
-Definition ldexp_spec' (t: type) :=
+Definition ldexp_spec' (t: type) `{STD: is_standard t}:=
    WITH x : ftype t, i: Z
    PRE [ reflect_to_ctype t , tint ]
        PROP (Int.min_signed <= i <= Int.max_signed)
@@ -541,11 +560,12 @@ Definition ldexp_spec' (t: type) :=
     POST [ reflect_to_ctype t ]
        PROP ()
        RETURN (reflect_to_val t 
-                       ((Binary.Bldexp (fprec t) (femax t) 
-                           (fprec_gt_0 t) (fprec_lt_femax t) BinarySingleNaN.mode_NE x i)))
+                (ftype_of_float (Binary.Bldexp (fprec t) (femax t) 
+                  (fprec_gt_0 t) (fprec_lt_femax t) BinarySingleNaN.mode_NE
+                   (float_of_ftype x) i)))
        SEP ().
 
-Definition frexp_spec' (t: type) :=
+Definition frexp_spec' (t: type) `{STD: is_standard t} :=
    WITH x : ftype t, p: val, sh: share
    PRE [ reflect_to_ctype t , tptr tint ]
        PROP (writable_share sh)
@@ -554,24 +574,28 @@ Definition frexp_spec' (t: type) :=
     POST [ reflect_to_ctype t ]
        PROP ()
        RETURN (reflect_to_val t 
-                        (fst (Binary.Bfrexp (fprec t) (femax t)  (fprec_gt_0 t) x)))
+                     (ftype_of_float (fst (Binary.Bfrexp (fprec t) (femax t)  (fprec_gt_0 t) 
+                              (float_of_ftype x)))))
        SEP (@data_at emptyCS sh tint (Vint (Int.repr 
-                         (snd (Binary.Bfrexp (fprec t) (femax t)  (fprec_gt_0 t) x))))
+                         (snd (Binary.Bfrexp (fprec t) (femax t)  (fprec_gt_0 t) 
+                              (float_of_ftype x)))))
                          p).
 
-Definition bogus_nan t := 
+Definition bogus_nan t `(STD: is_standard t) := 
    (* This is probably not the right NaN to use, wherever you see it used *)
    FMA_NAN.quiet_nan t (FMA_NAN.default_nan t). 
 
-Definition nextafter (t: type) (x y: ftype t) : ftype t := 
- match Binary.Bcompare (fprec t) (femax t) x y with
-  | Some Lt => Binary.Bsucc (fprec t) (femax t)  (fprec_gt_0 t) (fprec_lt_femax t) x
+Definition nextafter (t: type) `{STD: is_standard t} (x y: ftype t) : ftype t := 
+ match Binary.Bcompare (fprec t) (femax t) (float_of_ftype x) (float_of_ftype y) with
+  | Some Lt => ftype_of_float (Binary.Bsucc (fprec t) (femax t)  (fprec_gt_0 t) (fprec_lt_femax t)
+                     (float_of_ftype x))
   | Some Eq => y
-  | Some Gt => Binary.Bpred (fprec t) (femax t)  (fprec_gt_0 t) (fprec_lt_femax t) x
-  | None => proj1_sig (bogus_nan t)
+  | Some Gt => ftype_of_float (Binary.Bpred (fprec t) (femax t)  (fprec_gt_0 t) (fprec_lt_femax t) 
+                     (float_of_ftype x))
+  | None => ftype_of_float (proj1_sig (bogus_nan t _))
   end.
 
-Definition nextafter_spec' (t: type) :=
+Definition nextafter_spec' (t: type) `{STD: is_standard t}  :=
    WITH x : ftype t, y: ftype t
    PRE [ reflect_to_ctype t , reflect_to_ctype t ]
        PROP ()
@@ -582,15 +606,16 @@ Definition nextafter_spec' (t: type) :=
        RETURN (reflect_to_val t (nextafter t x y))
        SEP ().
 
-Definition copysign (t: type) (x y: ftype t) :=
- match x with
- | Binary.B754_zero _ _ _ => Binary.B754_zero _ _ (Binary.Bsign _ _ y)
- | Binary.B754_infinity _ _ _ => Binary.B754_infinity _ _ (Binary.Bsign _ _ y)
- | Binary.B754_finite _ _ _ m e H => Binary.B754_finite _ _ (Binary.Bsign _ _ y) m e H
- | Binary.B754_nan _ _ _ pl H => Binary.B754_nan _ _ (Binary.Bsign _ _ y) pl H
+Definition copysign (t: type) `{STD: is_standard t} (x y: ftype t) : ftype t :=
+ ftype_of_float
+ match float_of_ftype x with
+ | Binary.B754_zero _ _ _ => Binary.B754_zero _ _ (Binary.Bsign _ _ (float_of_ftype y))
+ | Binary.B754_infinity _ _ _ => Binary.B754_infinity _ _ (Binary.Bsign _ _ (float_of_ftype y))
+ | Binary.B754_finite _ _ _ m e H => Binary.B754_finite _ _ (Binary.Bsign _ _ (float_of_ftype y)) m e H
+ | Binary.B754_nan _ _ _ pl H => Binary.B754_nan _ _ (Binary.Bsign _ _ (float_of_ftype y)) pl H
 end.
 
-Definition copysign_spec' (t: type) :=
+Definition copysign_spec' (t: type) `{STD: is_standard t} :=
    WITH x : ftype t, y : ftype t
    PRE [ reflect_to_ctype t , reflect_to_ctype t ]
        PROP ()
@@ -601,7 +626,7 @@ Definition copysign_spec' (t: type) :=
        RETURN (reflect_to_val t (copysign t x y))
        SEP ().
 
-Definition nan_spec' (t: type) :=
+Definition nan_spec' (t: type) `{STD: is_standard t} :=
    WITH p: val
    PRE [ tptr tschar ]
        PROP ()
@@ -610,7 +635,7 @@ Definition nan_spec' (t: type) :=
     POST [ reflect_to_ctype t ]
        PROP ()
         (* here it _is_ actually permissible to use bogus_nan *)
-       RETURN (reflect_to_val t (proj1_sig (bogus_nan t)))
+       RETURN (reflect_to_val t (ftype_of_float (proj1_sig (bogus_nan t _))))
        SEP ().
 
 Definition arccosh (x: R) := Rabs (Rpower.arcsinh (sqrt (Rsqr x - 1)))%R.
@@ -622,25 +647,42 @@ Fixpoint always_true (args: list type) : function_type (map RR args) Prop :=
  | _ :: args' => fun _ => always_true args'
  end.
 
+Ltac vacuous_bnds_list tys :=
+ match tys with
+ | nil => constr:(@Knil _ bounds )
+ | ?t :: ?ts =>
+   let b := constr:(vacuous_bnds t) in
+   let bs := vacuous_bnds_list ts in
+   constr:(Kcons b bs)
+ end.
+
+(*
 Fixpoint vacuous_bnds_klist (tys: list type) : klist bounds tys :=
  match tys as l return (klist bounds l) with
   | [] => Knil
   | a :: l =>
       (fun (t : type) (tys0 : list type) =>
        Kcons (vacuous_bnds t) (vacuous_bnds_klist tys0)) a l
   end.
+*)
 
-Parameter c_function: forall (i: ident) (args: list type) (res: type) (f: function_type (map RR args) R),
+Parameter c_function: forall (i: ident) (args: list type) (res: type)
+      bnds
+     (f: function_type (map RR args) R),
    {ff: function_type (map ftype' args) (ftype res) 
-   | acc_prop args res (1 + (2 * GNU_error i))%N 1%N
-             (vacuous_bnds_klist args)           f ff}.
+   | acc_prop args res (1 + (2 * GNU_error i))%N 1%N bnds f ff}.
+
+Parameter axiom_floatfunc_congr: forall args result ff_func, 
+   @floatfunc_congr args result ff_func.
 
 Ltac floatfunc' i args res f :=
  let rel := constr:((1 + 2 * GNU_error i)%N) in
  let rel := eval compute in rel in 
  let abs := constr:(1%N) in
- let cf := constr:(c_function i args res f) in 
- exact (Build_floatfunc args res (vacuous_bnds_klist args) f (proj1_sig cf) rel abs (proj2_sig cf)).
+ let bnds := vacuous_bnds_list args in
+ let cf := constr:(c_function i args res bnds f) in
+ exact (Build_floatfunc args res bnds f (proj1_sig cf) rel abs (proj2_sig cf)
+        (axiom_floatfunc_congr _ _ _)).
 
 
 Module Type MathFunctions.
@@ -767,7 +809,7 @@ compute.
 reflexivity. (* If this line fails, then it lists the duplicate names in your DECLARE statements above *)
 Abort.
 
-Local Remark sqrt_accurate: forall x, 
+Local Remark sqrt_accurate: forall x: ftype Tdouble, 
   (0 <= FT2R x ->
    Binary.is_finite (fprec Tdouble) (femax Tdouble) x = true ->
    exists delta, exists epsilon,
@@ -781,7 +823,7 @@ rename H0 into H8.
 assert (H0: Binary.is_finite _ _ (ff_func (sqrt_ff Tdouble) x) = true). {
   destruct x; try destruct s; try discriminate; simpl; auto.
  -
-  simpl in H. unfold Defs.F2R in H. simpl in H.
+  simpl in H. unfold FT2R in H.  simpl in H. unfold Defs.F2R in H. simpl in H.
   pose proof Raux.bpow_gt_0 Zaux.radix2 e.
   rewrite IZR_NEG in H. unfold IZR in H.
   set (j :=  Raux.bpow Zaux.radix2 e) in *. clearbody j.

lib/test/verif_testmath.v

@@ -48,46 +48,55 @@ Definition ROUND {NAN: Nans} (t: type) (r: R) : R :=
                 (BinarySingleNaN.round_mode BinarySingleNaN.mode_NE)
                 r).
 
-Lemma BMULT_correct {NAN: Nans} {t} (x y: ftype t) :
+Lemma BMULT_correct {NAN: Nans} {t} `{STD: is_standard t} (x y: ftype t) :
   let prec := fprec t in let emax := femax t in 
   if Raux.Rlt_bool 
          (Rabs (ROUND t (FT2R x * FT2R y)))
          (Raux.bpow Zaux.radix2 emax)
        then
         FT2R (BMULT x y) = ROUND t (FT2R x * FT2R y) /\
-        is_finite _ _ (BMULT x y) = andb (is_finite _ _ x) (is_finite _ _ y) /\
-        (is_nan _ _ (BMULT x y) = false ->
-         Bsign _ _ (BMULT x y) = xorb (Bsign _ _ x) (Bsign _ _ y))
+        FPCore.is_finite (BMULT x y) = andb (FPCore.is_finite x) (FPCore.is_finite y) /\
+        (is_nan _ _ (float_of_ftype (BMULT x y)) = false ->
+         Bsign _ _ (float_of_ftype (BMULT x y)) = xorb (Bsign _ _ (float_of_ftype x)) (Bsign _ _ (float_of_ftype y)))
        else
-        B2FF _ _ (BMULT x y) = 
+        B2FF _ _ (float_of_ftype (BMULT x y)) = 
         binary_overflow prec emax BinarySingleNaN.mode_NE
-                    (xorb (Bsign _ _ x) (Bsign _ _ y)).
+                    (xorb (Bsign _ _ (float_of_ftype x)) (Bsign _ _ (float_of_ftype y))).
 Proof.
 intros.
+unfold BMULT, BINOP, ROUND.
+rewrite !FT2R_ftype_of_float.
+rewrite <- !B2R_float_of_ftype.
+rewrite !is_finite_Binary, !float_of_ftype_of_float.
 apply Bmult_correct.
 Qed.
 
-Lemma BPLUS_correct {NAN: Nans} {t} (x y: ftype t) :
+Lemma BPLUS_correct {NAN: Nans} {t} `{STD: is_standard t}  (x y: ftype t) :
   let prec := fprec t in let emax := femax t in 
-  is_finite _ _ x = true ->
-  is_finite _ _ y = true ->
+  FPCore.is_finite x = true ->
+  FPCore.is_finite y = true ->
   if   Raux.Rlt_bool (Rabs (ROUND t (FT2R x + FT2R y)))
           (Raux.bpow Zaux.radix2 emax)
   then FT2R (BPLUS x y) = ROUND t (FT2R x + FT2R y)%R /\
-        is_finite _ _ (BPLUS x y) = true /\
-        Bsign _ _ (BPLUS x y) = match
+        FPCore.is_finite (BPLUS x y) = true /\
+        Bsign _ _ (float_of_ftype (BPLUS x y)) = match
                     Raux.Rcompare (FT2R x + FT2R y)%R 0
                   with
-                  | Eq => (Bsign prec emax x &&
-                                 Bsign prec emax y)%bool
+                  | Eq => (Bsign prec emax (float_of_ftype x) &&
+                                 Bsign prec emax (float_of_ftype y))%bool
                   | Lt => true
                   | Gt => false
                   end
-       else B2FF _ _  (BPLUS x y) = 
-                 binary_overflow prec emax BinarySingleNaN.mode_NE  (Bsign _ _ x) /\  
-              Bsign _ _ x = Bsign _ _ y.
+       else B2FF _ _  (float_of_ftype (BPLUS x y)) = 
+                 binary_overflow prec emax BinarySingleNaN.mode_NE  
+                    (Bsign _ _ (float_of_ftype x)) /\  
+              Bsign _ _ (float_of_ftype x) = Bsign _ _ (float_of_ftype y).
 Proof.
 intros.
+unfold BPLUS, BINOP, ROUND.
+rewrite !FT2R_ftype_of_float.
+rewrite <- !B2R_float_of_ftype.
+rewrite !is_finite_Binary, !float_of_ftype_of_float in *.
 apply Bplus_correct; auto.
 Qed.
 
@@ -133,6 +142,18 @@ prove_roundoff_bound2.
  interval.
 Qed.
 
+Definition some_valmap [v: Maps.PTree.t {x: type & ftype x}] (H: valmap_valid v) :=
+  exist (@valmap_valid empty_collection) _ H.
+
+Ltac pose_valmap_of_list name vml :=
+    let z := compute_PTree (valmap_of_list' vml) in
+    let z := constr:(@abbreviate _ z) in
+    let H := fresh "VV" in
+    assert (H: valmap_valid z);
+      [apply (@compute_valmap_valid _); repeat apply conj; try apply I;
+         cbv[test_ptree test_ptree']; prove_incollection
+      | pose (name := some_valmap H : valmap)].
+
 
 
 Lemma f_model_accurate': forall t, 
@@ -142,9 +163,7 @@ Lemma f_model_accurate': forall t,
 Proof.
 intros.
 rename t into x.
-pose (vmap_list := [(_x, existT ftype _ x)]).
-pose (vmap :=
- ltac:(let z := compute_PTree (valmap_of_list (vmap_list)) in exact z)).
+pose_valmap_of_list vmap [(_x, existT ftype Tdouble (ftype_of_float x))].
 pose proof prove_roundoff_bound_x vmap.
 red in H0.
 spec H0. {
@@ -159,11 +178,10 @@ unfold f_model.
 change (FT2R _) with (FT2R (fval (env_ vmap) F')).
 forget (FT2R (fval (env_ vmap) F')) as g.
 simpl in H1.
-change (env_ vmap Tdouble _x) with x in H1.
-forget (B2R (fprec Tdouble) 1024 x) as t; intros.
+change (env_ vmap Tdouble _ _x) with x in H1.
 clear - H1.
 rewrite  Rplus_comm in H1.
-change (sin t * sin t + cos t * cos t) with ((sin t)² + (cos t)²) in H1.
+change (sin ?t * sin ?t + cos ?t * cos ?t) with ((sin t)² + (cos t)²) in H1.
 rewrite sin2_cos2 in H1.
 apply Rabs_le_inv in H1.
 lra.