Refactor range validator into a separate file for future extensions

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.IntervalValidation Flover.ErrorValidation Flover.Environments Flover.Typing Flover.FPRangeValidator.
+Require Import Flover.RealRangeValidator Flover.ErrorValidation Flover.Environments Flover.Typing Flover.FPRangeValidator.
 
 Require Export Coq.QArith.QArith.
 Require Export Flover.Infra.ExpressionAbbrevs Flover.Commands.
@@ -16,7 +16,7 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (def
   let tMap := (typeMap defVars e (FloverMap.empty mType)) in
   if (typeCheck e defVars tMap)
   then
-    if (validIntervalbounds e absenv P NatSet.empty) && FPRangeValidator e absenv tMap NatSet.empty
+    if RangeValidator e absenv P && FPRangeValidator e absenv tMap NatSet.empty
     then (validErrorbound e tMap absenv NatSet.empty)
     else false
   else false.
@@ -64,7 +64,7 @@ Proof.
   { unfold vars_typed. intros; apply types_defined. set_tac. destruct H1; set_tac.
     split; try auto. hnf; intros; set_tac. }
   rename R into validFPRanges.
-  edestruct (validIntervalbounds_sound e (A:=absenv) (P:=P) (fVars:=usedVars e) (dVars:=NatSet.empty) (Gamma:=defVars) (E:=E1))
+  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.

coq/RealRangeValidator.v

+Require Import Coq.Reals.Reals Coq.QArith.Qreals.
+Require Import Flover.Infra.RealSimps Flover.Infra.RationalSimps Flover.Infra.RealRationalProps Flover.Infra.Ltacs.
+Require Export Flover.IntervalValidation.
+Require Export Coq.QArith.QArith.
+Require Export Flover.Infra.ExpressionAbbrevs Flover.Commands.
+
+Definition RangeValidator e A P :=
+  (* if *)
+  validIntervalbounds e A P NatSet.empty.
+(* then true
+   match validAffineBounds e A P NatSet.empty with
+   | Some (p, b) => b
+   | None => false
+   end.
+else validAffineBounds e A P NatSet.empty *)
+
+Theorem RangeValidator_sound (f : exp Q) (A : analysisResult) (P : precond)
+        (E : env) (Gamma : nat -> option mType) :
+  RangeValidator f A P = true ->
+  fVars_P_sound (usedVars f) E P ->
+  vars_typed (usedVars f) Gamma ->
+  exists (iv : intv) (err : error) (vR : R),
+    FloverMap.find (elt:=intv * error) f A = Some (iv, err) /\
+    eval_exp E (toRMap Gamma) (toREval (toRExp f)) vR M0 /\ (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
+Proof.
+  intros.
+  unfold RangeValidator in *.
+  eapply validIntervalbounds_sound; eauto.
+  - unfold dVars_range_valid; intros; set_tac.
+  - set_tac.
+  - unfold vars_typed. intros v in_set; set_tac. destruct in_set; set_tac.
+Qed.