Extract general RoundoffErrorValidator

coq/CertificateChecker.v

@@ -6,7 +6,7 @@
 **)
 Require Import Coq.Reals.Reals Coq.QArith.Qreals.
 Require Import Flover.Infra.RealSimps Flover.Infra.RationalSimps Flover.Infra.RealRationalProps Flover.Infra.Ltacs.
-Require Import Flover.RealRangeValidator Flover.ErrorValidation Flover.Environments Flover.Typing Flover.FPRangeValidator.
+Require Import Flover.RealRangeValidator Flover.RoundoffErrorValidator Flover.Environments Flover.Typing Flover.FPRangeValidator.
 
 Require Export Coq.QArith.QArith.
 Require Export Flover.Infra.ExpressionAbbrevs Flover.Commands.
@@ -17,7 +17,7 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult) (P:precond) (de
   if (typeCheck e defVars tMap)
   then
     if RangeValidator e absenv P && FPRangeValidator e absenv tMap NatSet.empty
-    then (validErrorbound e tMap absenv NatSet.empty)
+    then RoundoffErrorValidator e tMap absenv NatSet.empty
     else false
   else false.
 
@@ -67,7 +67,7 @@ Proof.
   edestruct (RangeValidator_sound e absenv (P:=P) (Gamma:=defVars) (E:=E1))
     as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]]; eauto.
   destruct iv_e as [elo ehi].
-  edestruct (validErrorbound_sound e (typeMap defVars e (FloverMap.empty mType)) L approxE1E2 H0 eval_real R0 L1 H P_valid H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
+  edestruct (RoundoffErrorValidator_sound e (typeMap defVars e (FloverMap.empty mType)) L approxE1E2 H0 eval_real R0 L1 H P_valid H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
   exists (elo, ehi), err_e, vR, vF, mF; split; auto.
 Qed.
 

coq/RoundoffErrorValidator.v

+From Coq
+     Require Import Reals.Reals QArith.Qreals.
+
+From Flover
+     Require Export Infra.ExpressionAbbrevs ErrorValidation.
+
+Definition RoundoffErrorValidator (e:expr Q) (tMap:FloverMap.t mType) (A:analysisResult) (dVars:NatSet.t) :=
+  (* if *)
+  validErrorbound e tMap A dVars.
+  (*then true *)
+  (* else validAffineErrorBounds e A tMap dVars *)
+
+Theorem RoundoffErrorValidator_sound:
+forall (e : expr Q) (E1 E2 : env) (fVars dVars : NatSet.t) (A : analysisResult)
+         (nR : R) (err : error) (P : precond) (elo ehi : Q) (Gamma : FloverMap.t mType)
+         (defVars : nat -> option mType),
+       Typing.typeCheck e defVars Gamma = true ->
+       Environments.approxEnv E1 defVars A fVars dVars E2 ->
+       NatSet.Subset (usedVars e -- dVars) fVars ->
+       eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL ->
+       RoundoffErrorValidator e Gamma A dVars = true ->
+       IntervalValidation.validIntervalbounds e A P dVars = true ->
+       IntervalValidation.dVars_range_valid dVars E1 A ->
+       IntervalValidation.fVars_P_sound fVars E1 P ->
+       IntervalValidation.vars_typed (fVars ∪ dVars) defVars ->
+       FloverMap.find (elt:=intv * error) e A = Some (elo, ehi, err) ->
+       (exists (nF : R) (m : mType), eval_expr E2 defVars (toRExp e) nF m) /\
+       (forall (nF : R) (m : mType), eval_expr E2 defVars (toRExp e) nF m -> (Rabs (nR - nF) <= Q2R err)%R).
+Proof.
+  intros.
+  cbn in *.
+  eapply validErrorbound_sound; eauto.
+Qed.