Refactor to accommodate FPStdLib; adjust jetEngine benchmark

VeriNum · Dec 1, 2023 · da6cfeb · da6cfeb
1 parent 1a499d3
commit da6cfeb
Show file tree

Hide file tree

Showing 8 changed files with 639 additions and 592 deletions.
diff --git a/FPBench/jetengine.v b/FPBench/jetengine.v
@@ -6,7 +6,11 @@ Section WITHNANS.
 Context {NANS:Nans}.
 Open Scope R_scope.
 
-Definition jetengine_bmap_list := [Build_varinfo Tdouble 1%positive (-5) (5);Build_varinfo Tdouble 2%positive (-20) (5)].
+Definition _x1: ident := 1%positive.
+Definition _x2: ident := 2%positive.
+
+Definition jetengine_bmap_list := [Build_varinfo Tdouble _x1 (-5) (5);
+    Build_varinfo Tdouble _x2 (-20) (5)].
 
 Definition jetengine_bmap :=
  ltac:(let z := compute_PTree (boundsmap_of_list jetengine_bmap_list) in exact z).
@@ -20,7 +24,7 @@ Definition jetengine (x1 : ftype Tdouble) (x2 : ftype Tdouble) :=
   (x1 + ((((((((((2)%F64 * x1)%F64 * s)%F64 * (s - (3)%F64)%F64)%F64 + ((x1 * x1)%F64 * (((4)%F64 * s)%F64 - (6)%F64)%F64)%F64)%F64 * d)%F64 + ((((3)%F64 * x1)%F64 * x1)%F64 * s)%F64)%F64 + ((x1 * x1)%F64 * x1)%F64)%F64 + x1)%F64 + ((3)%F64 * s_42_)%F64)%F64)%F64).
 
 Definition jetengine_expr := 
- ltac:(let e' :=  HO_reify_float_expr constr:([1%positive;2%positive]) jetengine in exact e').
+ ltac:(let e' :=  HO_reify_float_expr constr:([_x1;_x2]) jetengine in exact e').
 
 Derive jetengine_b 
 SuchThat (forall vmap, prove_roundoff_bound jetengine_bmap vmap jetengine_expr jetengine_b)
@@ -32,15 +36,17 @@ try (subst jetengine_b; intro; prove_roundoff_bound);
 try (prove_rndval; interval);
 try (prove_roundoff_bound2);
 try match goal with |- Rabs ?a <= _ =>
-interval_intro (Rabs a) with (i_bisect vxH, i_bisect v, i_depth 17) as H
+interval_intro (Rabs a) with (i_bisect v_x1, i_bisect v_x2, i_depth 12) as H
 end;
+(*match type of H with _ <= _ <= ?A => pose (b := ltac:(ShowBound A)) end.
+ unify (Binary.Bcompare _ _ b 2.13e3%F64) (Some Lt).*)
 try (
 eapply Rle_trans;
 try apply H;
 try apply Rle_refl)).
 Time Qed.
 
-Lemma check_jetengine_bound: ltac:(CheckBound jetengine_b 1.4e02%F64).
+Lemma check_jetengine_bound: ltac:(CheckBound jetengine_b 2.13e3%F64).
 Proof. reflexivity. Qed.
 
 End WITHNANS.

diff --git a/vcfloat/.depend b/vcfloat/.depend
@@ -1,5 +1,7 @@
 Automate.vo Automate.glob Automate.v.beautified Automate.required_vo: Automate.v FPLang.vo FPLangOpt.vo RAux.vo Rounding.vo Reify.vo Float_notations.vo compute_tactics_ltac2.vo
 Automate.vio: Automate.v FPLang.vio FPLangOpt.vio RAux.vio Rounding.vio Reify.vio Float_notations.vio compute_tactics_ltac2.vio
+Base.vo Base.glob Base.v.beautified Base.required_vo: Base.v IEEE754_extra.vo klist.vo Float_notations.vo
+Base.vio: Base.v IEEE754_extra.vio klist.vio Float_notations.vio
 BigQAux.vo BigQAux.glob BigQAux.v.beautified BigQAux.required_vo: BigQAux.v 
 BigQAux.vio: BigQAux.v 
 BigRAux.vo BigRAux.glob BigRAux.v.beautified BigRAux.required_vo: BigRAux.v BigQAux.vo Q2RAux.vo
@@ -8,16 +10,16 @@ FMap_lemmas.vo FMap_lemmas.glob FMap_lemmas.v.beautified FMap_lemmas.required_vo
 FMap_lemmas.vio: FMap_lemmas.v 
 FPCompCert.vo FPCompCert.glob FPCompCert.v.beautified FPCompCert.required_vo: FPCompCert.v FPCore.vo
 FPCompCert.vio: FPCompCert.v FPCore.vio
-FPCore.vo FPCore.glob FPCore.v.beautified FPCore.required_vo: FPCore.v IEEE754_extra.vo klist.vo Float_notations.vo
-FPCore.vio: FPCore.v IEEE754_extra.vio klist.vio Float_notations.vio
+FPCore.vo FPCore.glob FPCore.v.beautified FPCore.required_vo: FPCore.v IEEE754_extra.vo klist.vo Float_notations.vo Base.vo
+FPCore.vio: FPCore.v IEEE754_extra.vio klist.vio Float_notations.vio Base.vio
 FPLang.vo FPLang.glob FPLang.v.beautified FPLang.required_vo: FPLang.v RAux.vo IEEE754_extra.vo Fprop_absolute.vo Float_lemmas.vo FPCore.vo klist.vo
 FPLang.vio: FPLang.v RAux.vio IEEE754_extra.vio Fprop_absolute.vio Float_lemmas.vio FPCore.vio klist.vio
 FPLangOpt.vo FPLangOpt.glob FPLangOpt.v.beautified FPLangOpt.required_vo: FPLangOpt.v Float_lemmas.vo FPLang.vo klist.vo LibTac.vo BigRAux.vo
 FPLangOpt.vio: FPLangOpt.v Float_lemmas.vio FPLang.vio klist.vio LibTac.vio BigRAux.vio
 FPLib.vo FPLib.glob FPLib.v.beautified FPLib.required_vo: FPLib.v FPCore.vo RAux.vo Float_notations.vo
 FPLib.vio: FPLib.v FPCore.vio RAux.vio Float_notations.vio
-FPStdLib.vo FPStdLib.glob FPStdLib.v.beautified FPStdLib.required_vo: FPStdLib.v IEEE754_extra.vo klist.vo Float_notations.vo FPCore.vo RAux.vo FPLib.vo Rounding.vo
-FPStdLib.vio: FPStdLib.v IEEE754_extra.vio klist.vio Float_notations.vio FPCore.vio RAux.vio FPLib.vio Rounding.vio
+FPStdLib.vo FPStdLib.glob FPStdLib.v.beautified FPStdLib.required_vo: FPStdLib.v IEEE754_extra.vo klist.vo Float_notations.vo Base.vo FPCore.vo RAux.vo Rounding.vo
+FPStdLib.vio: FPStdLib.v IEEE754_extra.vio klist.vio Float_notations.vio Base.vio FPCore.vio RAux.vio Rounding.vio
 Float_lemmas.vo Float_lemmas.glob Float_lemmas.v.beautified Float_lemmas.required_vo: Float_lemmas.v RAux.vo IEEE754_extra.vo Fprop_absolute.vo FPCore.vo
 Float_lemmas.vio: Float_lemmas.v RAux.vio IEEE754_extra.vio Fprop_absolute.vio FPCore.vio
 Float_notations.vo Float_notations.glob Float_notations.v.beautified Float_notations.required_vo: Float_notations.v IEEE754_extra.vo