implemented checker for return cmd

coq/CertificateChecker.v

@@ -9,7 +9,7 @@ From Flover
      Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
      Environments TypeValidator FPRangeValidator ExpressionAbbrevs Commands.
 
-Require Export ExpressionSemantics Flover.Commands Coq.QArith.QArith.
+Require Export ExpressionSemantics Flover.Commands Coq.QArith.QArith Flover.SMTArith.
 
 (** Certificate checking function **)
 Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
@@ -83,12 +83,12 @@ Proof.
 Qed.
 
 Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P: FloverMap.t intv)
-           defVars :=
+           (Qmap: FloverMap.t (SMTLogic * SMTLogic)) defVars :=
   match getValidMapCmd defVars f (FloverMap.empty mType) with
   | Succes Gamma =>
     if (validSSA f (freeVars f))
     then
-      if (RangeValidatorCmd f absenv P NatSet.empty) &&
+      if (RangeValidatorCmd f absenv P Qmap NatSet.empty) &&
           FPRangeValidatorCmd f absenv Gamma NatSet.empty
       then (RoundoffErrorValidatorCmd f Gamma absenv NatSet.empty)
       else false
@@ -101,7 +101,7 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P Q
   forall (E1 E2:env),
     eval_precond (freeVars f) E1 P ->
     unsat_queries E1 Qmap ->
-    CertificateCheckerCmd f absenv P defVars = true ->
+    CertificateCheckerCmd f absenv P Qmap defVars = true ->
     exists Gamma,
       approxEnv E1 (toRExpMap Gamma) absenv (freeVars f) NatSet.empty E2 ->
       exists iv err vR vF m,

coq/RealRangeValidator.v

@@ -23,8 +23,8 @@ Definition RangeValidator e A P Qmap dVars :=
        end.
 *)
 
-Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : FloverMap.t intv) Qmap dVars
-        (E : env) (Gamma : FloverMap.t mType):
+Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : FloverMap.t intv)
+        Qmap dVars (E : env) (Gamma : FloverMap.t mType):
   RangeValidator e A P Qmap dVars = true ->
   dVars_range_valid dVars E A ->
   affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
@@ -67,8 +67,11 @@ Proof.
 *)
 Qed.
 
-Definition RangeValidatorCmd e A P (* Qmap *) dVars:=
-  validIntervalboundsCmd e A P dVars.
+Definition RangeValidatorCmd e A P Qmap dVars:=
+  if
+    validIntervalboundsCmd e A P dVars
+  then true
+  else validSMTIntervalboundsCmd e A P Qmap dVars.
   (*
   if
     validIntervalboundsCmd e A P dVars
@@ -79,22 +82,24 @@ Definition RangeValidatorCmd e A P (* Qmap *) dVars:=
        end.
 *)
 
-Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : FloverMap.t intv) dVars
+Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : FloverMap.t intv)
+        (Qmap: FloverMap.t (SMTLogic * SMTLogic)) dVars
         (E : env) Gamma fVars outVars:
-  RangeValidatorCmd f A P dVars = true ->
+  RangeValidatorCmd f A P Qmap dVars = true ->
   ssa f (NatSet.union fVars dVars) outVars ->
   dVars_range_valid dVars E A ->
   affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
   eval_precond fVars E P ->
   NatSet.Subset (freeVars f -- dVars) fVars ->
   validTypesCmd f Gamma ->
+  unsat_queries E Qmap ->
   validRangesCmd f A E (toRTMap (toRExpMap Gamma)).
 Proof.
   intros ranges_valid; intros.
   unfold RangeValidatorCmd in ranges_valid.
   destruct (validIntervalboundsCmd f A P dVars) eqn:iv_valid.
   - eapply validIntervalboundsCmd_sound; eauto.
-  - discriminate.
+  - eapply validSMTIntervalboundsCmd_sound; eauto.
 (*
   - pose (iexpmap := (FloverMap.empty (affine_form Q))).
     pose (inoise := 1%nat).

coq/SMTValidation.v

@@ -108,7 +108,7 @@ Lemma Rle_trans2 a b x y z :
 Proof. lra. Qed.
 
 Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: FloverMap.t intv)
-         (Q: FloverMap.t (SMTLogic * SMTLogic)) (validVars: NatSet.t) : bool:=
+         (Q: FloverMap.t (SMTLogic * SMTLogic)) (validVars: NatSet.t) : bool :=
   match FloverMap.find e A with
   | None => false
   | Some (intv, _) =>
@@ -195,6 +195,25 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: FloverMap.t
        end
   end.
 
+Fixpoint validSMTIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P: FloverMap.t intv)
+         (Q: FloverMap.t (SMTLogic * SMTLogic)) (validVars:NatSet.t) : bool :=
+  match f with
+  | Let m x e g => false
+    (*
+    match FloverMap.find e A, FloverMap.find (Var Q x) A with
+    | Some ((e_lo,e_hi), _), Some ((x_lo, x_hi), _) =>
+      if (validIntervalbounds e A P validVars &&
+                              Qeq_bool (e_lo) (x_lo) &&
+                              Qeq_bool (e_hi) (x_hi))
+      then validIntervalboundsCmd g A P (NatSet.add x validVars)
+      else false
+    | _, _ => false
+    end
+     *)
+  |Ret e =>
+   validSMTIntervalbounds e A P Q validVars
+  end.
+
 Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: FloverMap.t intv)
         (Q: FloverMap.t (SMTLogic * SMTLogic)) fVars dVars (E: env) Gamma :
   unsat_queries E Q ->
@@ -414,3 +433,30 @@ Proof.
     canonize_hyps.
     cbn in *; lra.
 Qed.
+
+Theorem validSMTIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult)
+        (Q: FloverMap.t (SMTLogic * SMTLogic)):
+  forall Gamma E fVars dVars outVars P,
+    ssa f (NatSet.union fVars dVars) outVars ->
+    dVars_range_valid dVars E A ->
+    eval_precond fVars E P ->
+    NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
+    unsat_queries E Q ->
+    validSMTIntervalboundsCmd f A P Q dVars = true ->
+    validTypesCmd f Gamma ->
+    validRangesCmd f A E (toRTMap (toRExpMap Gamma)).
+Proof.
+  induction f;
+    intros *  ssa_f dVars_sound fVars_valid usedVars_subset
+                    unsat_qs valid_bounds_f valid_types_f;
+    cbn in *.
+  - discriminate.
+  - unfold validIntervalboundsCmd in valid_bounds_f.
+    pose proof (validSMTIntervalbounds_sound e (E:=E) Gamma unsat_qs valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e.
+    destruct valid_types_f as [? ?].
+    assert (validRanges e A E (toRTMap (toRExpMap Gamma))) as valid_e by (apply valid_iv_e; auto).
+    split; try auto.
+    apply validRanges_single in valid_e.
+    destruct valid_e as [?[?[? [? [? ?]]]]]; try auto.
+    simpl in *. repeat eexists; repeat split; try eauto; [econstructor; eauto| | ]; lra.
+Qed.
\ No newline at end of file

coq/testcase_aritmetic.v

@@ -22,13 +22,11 @@ FloverMap.add e5 (( (29)#(10), (75821)#(10240)), (316565750324396041763684170206
 Definition querymap_fnc1 :=
 FloverMap.add e2 (FalseQ, (AndQ (AndQ (LessEqQ (VarQ 0) (ConstQ ((6)#(1)))) (AndQ (LessEqQ (VarQ 1) (ConstQ ((8)#(1)))) (AndQ (LessEqQ (ConstQ ((-3)#(1))) (VarQ 0)) (AndQ (LessEqQ (ConstQ ((2)#(1))) (VarQ 1)) TrueQ)))) (AndQ (LessQ (ConstQ ((8201)#(2048))) (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1))) TrueQ))) (FloverMap.empty (SMTLogic * SMTLogic)).
 
-(*
-Theorem test_validation :
-  validSMTIntervalbounds e5 absenv_fnc1 thePrecondition_fnc1 querymap_fnc1 NatSet.empty = true.
+Theorem ErrorBound_fnc1_Sound :
+  CertificateChecker e5 absenv_fnc1 thePrecondition_fnc1 querymap_fnc1 defVars_fnc1 = true.
 Proof.
-  cbv.
+  vm_compute.
 Abort.
-*)
 
 Require Import Coq.Reals.Reals Coq.QArith.Qreals.
 Require Import RealRangeArith.