adding checker for the merged result

coq/CertificateChecker.v

@@ -12,14 +12,14 @@ Require Export List ExpressionSemantics Coq.QArith.QArith Flover.SMTArith.
 Export ListNotations.
 
 (** Certificate checking function **)
-Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
-           (P: precond) Qmap subdivs (defVars:FloverMap.t  mType):=
+Definition CertificateChecker (e: expr Q) (absenv: analysisResult)
+           (P: precond) Qmap subdivs (defVars: FloverMap.t  mType):=
   let tMap := (getValidMap defVars e (FloverMap.empty mType)) in
   match tMap with
   |Succes Gamma =>
    match subdivs with
    | [] => ResultChecker e absenv P Qmap defVars Gamma
-   | _ => SubdivsChecker e absenv P subdivs defVars Gamma
+   | hd :: tl => SubdivsChecker e absenv P hd tl defVars Gamma
    end
   | _ => false
   end.
@@ -29,11 +29,11 @@ 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 subdivs
+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) ->
+  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 subdivs defVars = true ->

coq/ResultChecker.v

@@ -4,8 +4,8 @@ From Flover
      Environments TypeValidator FPRangeValidator ExpressionAbbrevs.
 
 (** Result checking function **)
-Definition ResultChecker (e:expr Q) (absenv:analysisResult)
-           (P: precond) Qmap (defVars:FloverMap.t  mType) Gamma :=
+Definition ResultChecker (e: expr Q) (absenv: analysisResult)
+           (P: precond) Qmap (defVars: FloverMap.t  mType) Gamma :=
   validSSA e (preVars P) &&
            RangeValidator e absenv P Qmap NatSet.empty &&
            FPRangeValidator e absenv Gamma NatSet.empty &&
@@ -14,10 +14,10 @@ Definition ResultChecker (e:expr Q) (absenv:analysisResult)
 (**
    Soundness proof for the result checker.
 **)
-Theorem result_checking_is_sound (e:expr Q) (absenv:analysisResult) P Qmap 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) ->
+Theorem result_checking_is_sound (e: expr Q) (absenv: analysisResult) P Qmap 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 ->
     unsat_queries Qmap ->
     getValidMap defVars e (FloverMap.empty mType) = Succes Gamma ->

coq/SubdivsChecker.v

@@ -4,12 +4,12 @@ From Flover
      Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
      Environments TypeValidator FPRangeValidator ExpressionAbbrevs.
 *)
-Require Import List.
-
 From Flover
-     Require Import Infra.RealRationalProps Environments ExpressionSemantics SMTArith
+     Require Import Infra.RealRationalProps Environments ExpressionSemantics IntervalArithQ SMTArith
      TypeValidator FPRangeValidator ResultChecker.
 
+Require Import List.
+
 Definition check_subdivs_step e defVars Gamma (b: bool) (PA: precond * analysisResult) :=
   let (P, A) := PA in
   b && (ResultChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma).
@@ -17,22 +17,66 @@ Definition check_subdivs_step e defVars Gamma (b: bool) (PA: precond * analysisR
 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 *)
+Lemma check_subdivs_false_fp e subdivs defVars Gamma :
+  fold_left (check_subdivs_step e defVars Gamma) subdivs false = false.
+Proof.
+  induction subdivs as [|[P A] subdivs]; auto.
+Qed.
+
+Lemma check_subdivs_sound e subdivs defVars Gamma P A :
+  check_subdivs e subdivs defVars Gamma = true ->
+  List.In (P, A) subdivs ->
+  ResultChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma = true.
+Proof.
+  intros H Hin.
+  induction subdivs; cbn in Hin; auto.
+  destruct Hin; subst; auto.
+  - cbn in *. destruct (ResultChecker e A P (FloverMap.empty (SMTLogic * SMTLogic)) defVars Gamma) eqn:?; auto.
+    rewrite check_subdivs_false_fp in H; auto.
+  - apply IHsubdivs; auto. cbn in H.
+    unfold check_subdivs.
+    destruct (check_subdivs_step e defVars Gamma true a) eqn:?; auto.
+    rewrite check_subdivs_false_fp in H. discriminate H.
+Qed.
+
+(* TODO: how to merge 2 analysisResults? *)
+Definition merge_subdivs_step (e: expr Q) (acc A: analysisResult) :=
+  acc.
+
+(* TODO: it might be better to merge all results for one specific expression,
+   instead of merging 2 results for all expressions *)
+Definition merge_subdivs e hd tl : analysisResult :=
+  fold_left (merge_subdivs_step e) tl hd.
+
+Fixpoint check_merge_subdivs e (M A: analysisResult) :=
+  match e with
+  | Unop _ e1 | Downcast _ e1 => check_merge_subdivs e1 M A
+  | Binop _ e1 e2 | Let _ _ e1 e2 => check_merge_subdivs e1 M A && check_merge_subdivs e2 M A 
+  | Fma e1 e2 e3 => check_merge_subdivs e1 M A && check_merge_subdivs e2 M A && check_merge_subdivs e3 M A
+  | _ => true
+  end &&
+      match FloverMap.find e M, FloverMap.find e A with
+      | Some (ivM, errM), Some (ivA, errA) => isSupersetIntv ivM ivA && (Qleb errM errA)
+      | _, _ => false
+      end.
+
+(* TODO: check 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.
+Definition SubdivsChecker (e: expr Q) (absenv: analysisResult)
+           (P: precond) hd tl (defVars: FloverMap.t  mType) Gamma :=
+  check_subdivs e (hd :: tl) defVars Gamma &&
+                check_merge_subdivs e (merge_subdivs e (snd hd) (map snd tl)) absenv.
 
 (**
    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) ->
+Theorem subdivs_checking_is_sound (e: expr Q) (absenv: analysisResult) P hd_subdivs tl_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 ->
+    SubdivsChecker e absenv P hd_subdivs tl_subdivs defVars Gamma = true ->
     exists Gamma,
       approxEnv E1 (toRExpMap Gamma) absenv (freeVars e) NatSet.empty E2 ->
       exists iv err vR vF m,