adding checker for subintervals

coq/CertificateChecker.v

@@ -5,17 +5,21 @@
    as shown in the soundness theorem.
 **)
 From Flover
-     Require Import Infra.RealRationalProps Environments TypeValidator ResultChecker.
+     Require Import Infra.RealRationalProps Environments TypeValidator
+     ResultChecker SubdivsChecker.
 
 Require Export ExpressionSemantics Coq.QArith.QArith Flover.SMTArith.
 
-(* TODO: add subdivs *)
 (** Certificate checking function **)
 Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
-           (P: precond) Qmap (defVars:FloverMap.t  mType):=
+           (P: precond) Qmap subdivs (defVars:FloverMap.t  mType):=
   let tMap := (getValidMap defVars e (FloverMap.empty mType)) in
   match tMap with
-  |Succes Gamma => ResultChecker e absenv P Qmap defVars Gamma
+  |Succes Gamma =>
+   match subdivs with
+   | List.nil => ResultChecker e absenv P Qmap defVars Gamma
+   | _ => SubdivsChecker e absenv P subdivs defVars Gamma
+   end
   | _ => false
   end.
 
@@ -24,13 +28,14 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
    Apart from assuming two executions, one in R and one on floats, we assume that
    the real valued execution respects the precondition.
 **)
-Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P Qmap defVars:
+Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P Qmap subdivs
+        defVars:
   forall (E1 E2:env) DeltaMap,
     (forall (e' : expr R) (m' : mType),
         exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
     eval_precond E1 P ->
     unsat_queries Qmap ->
-    CertificateChecker e absenv P Qmap defVars = true ->
+    CertificateChecker e absenv P Qmap subdivs defVars = true ->
     exists Gamma,
       approxEnv E1 (toRExpMap Gamma) absenv (freeVars e) NatSet.empty E2 ->
       exists iv err vR vF m,
@@ -44,5 +49,7 @@ Proof.
   intros * deltas_matched P_valid unsat_qs certificate_valid.
   unfold CertificateChecker in certificate_valid.
   destruct (getValidMap defVars e (FloverMap.empty mType)) eqn:?; try congruence.
-  eapply result_checking_is_sound; eauto.
+  destruct subdivs.
+  - eapply result_checking_is_sound; eauto.
+  - eapply subdivs_checking_is_sound; eauto.
 Qed.

coq/SubdivsChecker.v

+(*
+From Flover
+     Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
+     Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
+     Environments TypeValidator FPRangeValidator ExpressionAbbrevs.
+*)
+Require Import List.
+
+From Flover
+     Require Import Infra.RealRationalProps Environments ExpressionSemantics SMTArith
+     TypeValidator FPRangeValidator ResultChecker.
+
+Definition check_subdivs_step e defVars Gamma (b: bool) (p: analysisResult * precond) :=
+  let (A, P) := p in
+  b && (ResultChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma).
+
+Definition check_subdivs e subdivs defVars Gamma :=
+  fold_left (check_subdivs_step e defVars Gamma) subdivs true.
+
+(* TODO: check absenv and precond sound wrt. subdivs *)
+(** Interval subdivisions checking function **)
+Definition SubdivsChecker (e:expr Q) (absenv:analysisResult)
+           (P: precond) subdivs (defVars:FloverMap.t  mType) Gamma :=
+  check_subdivs e subdivs defVars Gamma.
+
+(**
+   Soundness proof for the interval subdivs checker.
+**)
+Theorem subdivs_checking_is_sound (e:expr Q) (absenv:analysisResult) P subdivs defVars Gamma:
+  forall (E1 E2:env) DeltaMap,
+    (forall (e' : expr R) (m' : mType),
+        exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
+    eval_precond E1 P ->
+    getValidMap defVars e (FloverMap.empty mType) = Succes Gamma ->
+    SubdivsChecker e absenv P subdivs defVars Gamma = true ->
+    exists Gamma,
+      approxEnv E1 (toRExpMap Gamma) absenv (freeVars e) NatSet.empty E2 ->
+      exists iv err vR vF m,
+        FloverMap.find e absenv = Some (iv, err) /\
+        eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) vR REAL /\
+        eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m /\
+        (forall vF m,
+            eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
+            (Rabs (vR - vF) <= Q2R err))%R.
+Proof.
+Admitted.
\ No newline at end of file