Catchup work

coq/CertificateChecker.v

@@ -6,7 +6,7 @@
 **)
 Require Import Coq.Reals.Reals Coq.QArith.Qreals.
 Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs.
-Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments Daisy.Typing.
+Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments Daisy.Typing Daisy.FPRangeValidator.
 
 Require Export Coq.QArith.QArith.
 Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
@@ -14,7 +14,7 @@ Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
 (** Certificate checking function **)
 Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
   if (typeCheck e defVars (typeMap defVars e)) then
-    if (validIntervalbounds e absenv P NatSet.empty)
+    if (validIntervalbounds e absenv P NatSet.empty) && FPRangeValidator e absenv (typeMap defVars e) NatSet.empty
     then (validErrorbound e (typeMap defVars e) absenv NatSet.empty)
     else false
   else false.
@@ -63,19 +63,21 @@ Proof.
   assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
   { hnf; intros a in_empty.
     set_tac. }
-  assert (forall v, (v) mem (NatSet.empty) = true -> exists vR : R, E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R).
+  rename R into validFPRanges.
+  assert (forall v, (v) mem (NatSet.empty) = true -> exists vR :R, E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R).
   { intros v v_in_empty.
     rewrite NatSet.mem_spec in v_in_empty.
     inversion v_in_empty. }
   edestruct validIntervalbounds_sound as [vR [eval_real real_bounds_e]]; eauto.
-  destruct (validErrorbound_sound e P (typeMap defVars e) L approxE1E2 H0 eval_real R0 L0 H1 P_valid H absenv_eq) as [[vF [mF eval_float]] err_bounded]; auto.
+  destruct (validErrorbound_sound e P (typeMap defVars e) L approxE1E2 H0 eval_real R0 L1 H1 P_valid H absenv_eq) as [[vF [mF eval_float]] err_bounded]; auto.
   exists vR; exists vF; exists mF; split; auto.
 Qed.
 
 Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:=
   if (typeCheckCmd f defVars (typeMapCmd defVars f) && validSSA f (freeVars f))
   then
-    if (validIntervalboundsCmd f absenv P NatSet.empty)
+    if (validIntervalboundsCmd f absenv P NatSet.empty) &&
+       FPRangeValidatorCmd f absenv (typeMapCmd defVars f) NatSet.empty
     then (validErrorboundCmd f (typeMapCmd defVars f) absenv NatSet.empty)
     else false
   else false.
@@ -114,6 +116,7 @@ Proof.
   { eapply ssa_equal_set; try eauto.
     apply NatSetProps.empty_union_2.
     apply NatSet.empty_spec. }
+  rename R into validFPRanges.
   assert (forall v, (v) mem (NatSet.empty) = true ->
                exists vR : R,
                  E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) as no_dVars_valid.

coq/FPRangeValidator.v

 
 (* TODO: Flocq ops open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory *)
 
-Require Import Daisy.Infra.MachineType Daisy.Typing Daisy.Infra.RealSimps Daisy.CertificateChecker.
+Require Import Coq.QArith.QArith.
 
-Fixpoint FPRangeValidator (e:exp Q) A typeMap dVars {struct e} : bool :=
+Require Import Daisy.Infra.MachineType Daisy.Typing Daisy.Infra.RealSimps Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Commands Daisy.Environments Daisy.ssaPrgs.
+
+Fixpoint FPRangeValidator (e:exp Q) (A:analysisResult) typeMap dVars {struct e} : bool :=
   match typeMap e with
   |Some m =>
         let (iv_e, err_e) := A e in
-        let iv_e_float := widenInterval iv_e err_e in
+        let iv_e_float := widenIntv iv_e err_e in
         let recRes :=
             match e with
             | Binop b e1 e2 =>
-              FPRangeValidator e1 A typeMap dVars /\
+              FPRangeValidator e1 A typeMap dVars &&
               FPRangeValidator e2 A typeMap dVars
             | Unop u e =>
               FPRangeValidator e A typeMap dVars
@@ -24,26 +26,27 @@ Fixpoint FPRangeValidator (e:exp Q) A typeMap dVars {struct e} : bool :=
           if NatSet.mem v dVars
           then true
           else
-            if (validValue (IVhi iv_e_float) m /\
-                validValue (IVlo iv_e_float) m)
-            then ((normal (IVlo iv_e_float) m) \/ ((IVlo iv_e_float) = 0) \/
-                  normal (IVhi iv_e_float) m \/ (IVhi iv_e_float) = 0) /\ recRes
+            if (validValue (ivhi iv_e_float) m &&
+                validValue (ivlo iv_e_float) m)
+            then ((normal (ivlo iv_e_float) m) || (Qeq_bool (ivlo iv_e_float) 0)) &&
+                  (normal (ivhi iv_e_float) m || (Qeq_bool (ivhi iv_e_float) 0)) && recRes
             else
               false
-        | _ => if (validValue (IVhi iv_e_float) m /\
-                  validValue (IVlo iv_e_float) m)
-              then ((normal (IVlo iv_e_float) m) \/ ((IVlo iv_e_float) = 0) \/
-                    normal (IVhi iv_e_float) m \/ (IVhi iv_e_float) = 0) /\ recRes
+        | _ => if (validValue (ivhi iv_e_float) m &&
+                validValue (ivlo iv_e_float) m)
+              then ((normal (ivlo iv_e_float) m) || (Qeq_bool (ivlo iv_e_float) 0)) &&
+                  (normal (ivhi iv_e_float) m || (Qeq_bool (ivhi iv_e_float) 0)) && recRes
               else
                 false
         end
   | None => false
   end.
-      | SOME m =>
-
-      | NONE => F`;
-  .
 
-open AbbrevsTheory MachineTypeTheory TypingTheory RealSimpsTheory IntervalArithTheory
-     ExpressionsTheory DaisyTactics IntervalValidationTheory ErrorValidationTheory
-     CommandsTheory EnvironmentsTheory ssaPrgsTheory
\ No newline at end of file
+Fixpoint FPRangeValidatorCmd (f:cmd Q) (A:analysisResult) typeMap dVars :=
+  match f with
+  | Let m n e g =>
+    if FPRangeValidator e A typeMap dVars
+    then FPRangeValidatorCmd g A typeMap (NatSet.add n dVars)
+     else false
+| Ret e => FPRangeValidator e A typeMap dVars
+  end.
\ No newline at end of file