From 8414e5ff65f562a56b8c76052f7f6e8a07a15488 Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Fri, 4 May 2018 15:13:28 +0200
Subject: [PATCH] Extract general RoundoffErrorValidator
---
coq/CertificateChecker.v | 6 +++---
coq/RoundoffErrorValidator.v | 33 +++++++++++++++++++++++++++++++++
2 files changed, 36 insertions(+), 3 deletions(-)
create mode 100644 coq/RoundoffErrorValidator.v
diff --git a/coq/CertificateChecker.v b/coq/CertificateChecker.v
index 1874fac4..378bd7e5 100644
--- a/coq/CertificateChecker.v
+++ b/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.
diff --git a/coq/RoundoffErrorValidator.v b/coq/RoundoffErrorValidator.v
new file mode 100644
index 00000000..2fd69bf1
--- /dev/null
+++ b/coq/RoundoffErrorValidator.v
@@ -0,0 +1,33 @@
+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.
--
GitLab