removed freeVars from eval_precond

coq/CertificateChecker.v

@@ -30,7 +30,7 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
 **)
 Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P Qmap defVars:
   forall (E1 E2:env),
-    eval_precond (usedVars e) E1 P ->
+    eval_precond E1 P ->
     unsat_queries E1 Qmap ->
     CertificateChecker e absenv P Qmap defVars = true ->
     exists Gamma,
@@ -82,11 +82,72 @@ Proof.
   exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto.
 Qed.
 
+Lemma validSSA_eq_set s s' f :
+  NatSet.Equal s' s -> validSSA f s = true -> validSSA f s' = true.
+Proof.
+  induction f in s, s' |- *; intros sub ?.
+  - andb_to_prop H.
+    apply andb_true_iff; split.
+    apply andb_true_iff; split.
+    + apply negb_true_iff.
+      apply negb_true_iff in L0.
+      apply NatSetProps.FM.not_mem_iff.
+      apply NatSetProps.FM.not_mem_iff in L0.
+      apply NatSetProps.subset_equal in sub.
+      intros ?. auto.
+    + apply NatSetProps.FM.subset_1.
+      apply NatSetProps.FM.subset_2 in R0.
+      apply NatSetProps.equal_sym in sub.
+      apply NatSetProps.subset_equal in sub.
+      set_tac.
+    + fold validSSA in *.
+      eapply IHf; eauto.
+      assert (NatSet.Subset s' s) by now apply NatSetProps.subset_equal in sub.
+      apply NatSetProps.equal_sym in sub.
+      apply NatSetProps.subset_equal in sub.
+      split; set_tac; intuition.
+  - apply NatSetProps.FM.subset_1.
+    apply NatSetProps.FM.subset_2 in H.
+    apply NatSetProps.equal_sym in sub.
+    apply NatSetProps.subset_equal in sub.
+    set_tac.
+Qed.
+
+Lemma validSSA_downward_closed s f vars :
+  NatSet.Subset (freeVars f) vars ->
+  validSSA f (vars ∪ s) = true ->
+  validSSA f vars = true.
+Proof.
+  induction f in vars |- *.
+  - intros sub H. andb_to_prop H.
+    apply andb_true_intro; split.
+    apply andb_true_intro; split.
+    + apply negb_true_iff.
+      apply NatSetProps.FM.not_mem_iff.
+      apply negb_true_iff in L0.
+      apply NatSetProps.FM.not_mem_iff in L0.
+      intros ?. apply L0. set_tac.
+    + apply NatSetProps.FM.subset_1.
+      apply NatSetProps.FM.subset_2 in R0.
+      set_tac. set_tac.
+      split; auto.
+      apply negb_true_iff in L0.
+      apply NatSetProps.FM.not_mem_iff in L0.
+      intros ?. subst. apply L0. set_tac.
+    + fold validSSA in *. apply IHf.
+      * set_tac.
+        destruct (dec_eq_nat a n); [now left | right; set_tac].
+      * eapply validSSA_eq_set; eauto.
+        split; set_tac; intuition.
+  - intros ? _.
+    now apply NatSetProps.FM.subset_1.
+Qed.
+
 Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P: FloverMap.t intv)
            (Qmap: FloverMap.t (SMTLogic * SMTLogic)) defVars :=
   match getValidMapCmd defVars f (FloverMap.empty mType) with
   | Succes Gamma =>
-    if (validSSA f (freeVars f))
+    if (validSSA f (freeVars f ∪ preVars P))
     then
       if (RangeValidatorCmd f absenv P Qmap NatSet.empty) &&
           FPRangeValidatorCmd f absenv Gamma NatSet.empty
@@ -99,7 +160,7 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P: FloverMap
 Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P Qmap
         defVars:
   forall (E1 E2:env),
-    eval_precond (freeVars f) E1 P ->
+    eval_precond E1 P ->
     unsat_queries E1 Qmap ->
     CertificateCheckerCmd f absenv P Qmap defVars = true ->
     exists Gamma,
@@ -127,9 +188,12 @@ Proof.
   exists Gamma; intros approxE1E2.
   repeat rewrite <- andb_lazy_alt in certificate_valid.
   andb_to_prop certificate_valid.
+  assert (validSSA f (freeVars f) = true) as ssa_valid
+    by (eapply validSSA_downward_closed; eauto; set_tac).
+  apply validSSA_sound in ssa_valid as [outVars_small ssa_f_small].
   apply validSSA_sound in L.
   destruct L as [outVars ssa_f].
-  assert (ssa f (freeVars f ∪ NatSet.empty) outVars) as ssa_valid.
+  assert (ssa f ((freeVars f ∪ preVars P) ∪ NatSet.empty) outVars) as ssa_valid.
   { eapply ssa_equal_set; try eauto.
     apply NatSetProps.empty_union_2.
     apply NatSet.empty_spec. }
@@ -140,13 +204,16 @@ Proof.
   assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
     as freeVars_contained by set_tac.
   assert (validRangesCmd f absenv E1 (toRTMap (toRExpMap Gamma))) as valid_f.
-  { eapply RangeValidatorCmd_sound; eauto.
-    unfold RangeValidatorCmd.
+  { eapply (RangeValidatorCmd_sound _ (fVars:=freeVars f ∪ preVars P)); eauto; set_tac.
+    (* unfold RangeValidatorCmd. *)
     unfold affine_dVars_range_valid; intros.
     set_tac. }
   pose proof (validRangesCmd_single _ _ _ _ valid_f) as valid_single.
   destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
   destruct iv as [f_lo f_hi].
   edestruct (RoundoffErrorValidatorCmd_sound) as [[vF [mF eval_float]] ?]; eauto.
-  exists (f_lo, f_hi), err, vR, vF, mF; repeat split; try auto.
+  - eapply ssa_equal_set. 2: exact ssa_f_small.
+    apply NatSetProps.empty_union_2.
+    apply NatSet.empty_spec.
+  - exists (f_lo, f_hi), err, vR, vF, mF; repeat split; try auto.
 Qed.

coq/IntervalValidation.v

@@ -149,7 +149,7 @@ Theorem validIntervalbounds_sound (f:expr Q) (A:analysisResult) (P: FloverMap.t
   validIntervalbounds f A P dVars = true ->
   dVars_range_valid dVars E A ->
   NatSet.Subset ((Expressions.usedVars f) -- dVars) fVars ->
-  eval_precond fVars E P ->
+  eval_precond E P ->
   validTypes f Gamma ->
   validRanges f A E (toRTMap (toRExpMap Gamma)).
 Proof.
@@ -394,14 +394,15 @@ Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):
   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 ->
+    eval_precond E P ->
+    NatSet.Subset (preVars P) fVars ->
     NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
     validIntervalboundsCmd f A P dVars = true ->
     validTypesCmd f Gamma ->
     validRangesCmd f A E (toRTMap (toRExpMap Gamma)).
 Proof.
   induction f;
-    intros *  ssa_f dVars_sound fVars_valid usedVars_subset
+    intros *  ssa_f dVars_sound fVars_valid preVars_free usedVars_subset
                     valid_bounds_f valid_types_f;
     cbn in *.
   - Flover_compute.
@@ -445,9 +446,10 @@ Proof.
         case_eq (x =? n); intros case_x; auto.
         rewrite Nat.eqb_eq in case_x. subst.
         set_tac.
-        assert (NatSet.In n (NatSet.union fVars dVars)) as in_union
-          by (destruct (fVars_valid n iv); auto; set_tac).
-        exfalso. now apply H6.
+        assert (NatSet.In n fVars) as in_free
+            by (apply preVars_free; eapply preVars_sound; eauto).
+          (* by (destruct (fVars_valid n iv); auto; set_tac). *)
+        exfalso. apply H6. set_tac.
       - intros x x_contained.
         set_tac.
         repeat split; try auto.

coq/RealRangeValidator.v

@@ -29,17 +29,16 @@ Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : FloverMap.t
   dVars_range_valid dVars E A ->
   affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
   validTypes e Gamma ->
-  eval_precond (usedVars e) E P ->
+  eval_precond E P ->
   unsat_queries E Qmap ->
   validRanges e A E (toRTMap (toRExpMap Gamma)).
 Proof.
   intros.
   unfold RangeValidator in *.
   destruct (validIntervalbounds e A P dVars) eqn: Hivcheck.
-  - eapply validIntervalbounds_sound; eauto.
-    set_tac.
+  - eapply validIntervalbounds_sound; set_tac; eauto.
     (* unfold dVars_range_valid; intros; set_tac. *)
-  - eapply validSMTIntervalbounds_sound; eauto; set_tac.
+  - eapply validSMTIntervalbounds_sound; set_tac; eauto.
   (*
   - pose (iexpmap := (FloverMap.empty (affine_form Q))).
     pose (inoise := 1%nat).
@@ -89,7 +88,8 @@ Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : FloverMap.
   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 ->
+  eval_precond E P ->
+  NatSet.Subset (preVars P) fVars ->
   NatSet.Subset (freeVars f -- dVars) fVars ->
   validTypesCmd f Gamma ->
   unsat_queries E Qmap ->

coq/SMTArith.v

@@ -274,10 +274,54 @@ Proof.
   apply eqb_var in Heq. cbn in *. now subst.
 Qed.
 
-Definition eval_precond fVars E (P: FloverMap.t intv) :=
+Definition eval_precond E (P: FloverMap.t intv) :=
+  forall x iv, List.In (Var Q x, iv) (FloverMap.elements P) ->
+          exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
+
+Definition addVar2Set (elt: (expr Q * intv)) s :=
+  match elt with
+  | (Var _ x, _) => NatSet.add x s
+  | _ => s
+  end.
+
+Definition preVars (P: FloverMap.t intv) :=
+  List.fold_right addVar2Set NatSet.empty (FloverMap.elements P).
+
+Lemma preVars_sound P x iv :
+  List.In (Var Q x, iv) (FloverMap.elements P) -> x ∈ (preVars P).
+Proof.
+  unfold preVars.
+  induction (FloverMap.elements P).
+  - cbn. tauto.
+  - cbn. intros [-> | ?]; cbn; set_tac.
+    destruct a as [e ?]; destruct e; auto. cbn. set_tac.
+Qed.
+
+(*
+Lemma eval_precond_sound fVars E P :
+  eval_precond fVars E P ->
   forall x iv, List.In (Var Q x, iv) (FloverMap.elements P) ->
-          (x ∈ fVars) /\
           exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
+Proof.
+  intros H x iv Hin. now apply H.
+Qed.
+
+Lemma eval_precond_complete fVars E P :
+  NatSet.Subset (varsPre P) fVars ->
+  (forall x iv, List.In (Var Q x, iv) (FloverMap.elements P) ->
+           exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv)) ->
+  eval_precond fVars E P.
+Proof.
+  intros sub H x iv Hin. split; [set_tac|now apply H].
+  unfold varsPre.
+  clear -Hin.
+  induction (FloverMap.elements P).
+  - cbn in *. tauto.
+  - destruct Hin.
+    + subst. cbn. set_tac.
+    + cbn. destruct a as [e ?]. destruct e; set_tac. set_tac.
+Qed.
+*)
 
 Definition addVarConstraint (el: expr Q * intv) q :=
   match el with
@@ -405,6 +449,7 @@ Proof.
 Qed.
 *)
 
+(*
 Lemma precond_free_vars fVars E P q :
   eval_precond fVars E P ->
   checkPre P q = true ->
@@ -438,18 +483,18 @@ Proof with try discriminate.
       apply (prec_valid a (lo, hi)). subst. auto.
       * eapply IHl; eauto.
 Qed.
+*)
 
-Lemma checkPre_pre_smt fVars E P q :
+Lemma checkPre_pre_smt E P q :
   checkPre P q = true ->
-  eval_precond fVars E P ->
+  eval_precond E P ->
   eval_smt_logic E q.
 Proof with try discriminate.
   unfold checkPre, eval_precond.
   induction (FloverMap.elements P) as [|[e [lo hi]] l IHl] in q |- *.
   - destruct q; cbn; intros chk... now auto.
   - destruct e as [x| | | | |].
-    2-6: cbn; try (intros H0 H1; apply IHl; auto). (* ; intros x iv Hin;
-      apply (H2 e'); auto). *)
+    2-6: (cbn; intros; apply IHl; auto).
     cbn.
     destruct q as [? ?|? ?|? ?| |?|q1 q2|? ?]...
     destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
@@ -468,9 +513,9 @@ Proof with try discriminate.
     apply Qeq_sym in chk2. apply Qeq_sym in chk1.
     (* assert (x ∈ fVars) as fx by (subst; set_tac; set_tac). *)
     repeat split.
-    + destruct (H x (lo, hi)) as [Hin [v [H0 [H1 H2]]]]; cbn; auto.
+    + destruct (H x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; auto.
       exists (Q2R r), v. repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
-    + destruct (H x (lo, hi)) as [Hin [v [H0 [H1 H2]]]]; cbn; auto.
+    + destruct (H x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; auto.
       exists v, (Q2R r'). repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
     + apply IHl; auto.
 Qed.
@@ -512,9 +557,8 @@ Proof with try discriminate.
 Qed.
 *)
 
-Lemma precond_bound_correct fVars E P preQ bound :
-  eval_precond fVars E P
-  -> NatSet.Subset (varsLogic preQ) fVars
+Lemma precond_bound_correct E P preQ bound :
+  eval_precond E P
   -> checkPre P preQ = true
   -> eval_smt_logic E bound
   -> eval_smt_logic E (AndQ preQ bound).
@@ -524,34 +568,32 @@ Proof.
   eapply checkPre_pre_smt; eauto.
 Qed.
 
-Lemma RangeBound_low_sound fVars E P preQ e r Gamma v :
-  eval_precond fVars E P
-  -> NatSet.Subset (varsLogic preQ) fVars
+Lemma RangeBound_low_sound E P preQ e r Gamma v :
+  eval_precond E P
   -> checkPre P preQ = true
   -> ~ eval_smt_logic E (AndQ preQ (AndQ (LessQ e (ConstQ r)) TrueQ))
   -> eval_expr E (toRTMap Gamma) (toREval (toRExp (SMTArith2Expr e))) v REAL
   -> Q2R r <= v.
 Proof.
-  intros H0 H1 H2 H3 H4.
-  apply eval_expr_smt in H4.
+  intros H0 H1 H2 H3.
+  apply eval_expr_smt in H3.
   apply Rnot_lt_le. intros B.
-  apply H3. eapply precond_bound_correct; eauto.
+  apply H2. eapply precond_bound_correct; eauto.
   split; cbn; auto.
   do 2 eexists. repeat split; first [eassumption | constructor].
 Qed.
 
-Lemma RangeBound_high_sound fVars E P preQ e r Gamma v :
-  eval_precond fVars E P
-  -> NatSet.Subset (varsLogic preQ) fVars
+Lemma RangeBound_high_sound E P preQ e r Gamma v :
+  eval_precond E P
   -> checkPre P preQ = true
   -> ~ eval_smt_logic E (AndQ preQ (AndQ (LessQ (ConstQ r) e) TrueQ))
   -> eval_expr E (toRTMap Gamma) (toREval (toRExp (SMTArith2Expr e))) v REAL
   -> v <= Q2R r.
 Proof.
-  intros H0 H1 H2 H3 H4.
-  apply eval_expr_smt in H4.
+  intros H0 H1 H2 H3.
+  apply eval_expr_smt in H3.
   apply Rnot_lt_le. intros B.
-  apply H3. eapply precond_bound_correct; eauto.
+  apply H2. eapply precond_bound_correct; eauto.
   split; cbn; auto.
   do 2 eexists. repeat split; first [eassumption | constructor].
 Qed.

coq/SMTValidation.v

@@ -34,8 +34,8 @@ Definition tightenBounds (e: expr Q) (iv: intv) (qMap: FloverMap.t (SMTLogic * S
   | Some (loQ, hiQ) => (tightenLowerBound e (fst iv) loQ P, tightenUpperBound e (snd iv) hiQ P)
   end.
 
-Lemma tightenBounds_low_sound fVars E Gamma e v iv qMap P :
-  eval_precond fVars E P
+Lemma tightenBounds_low_sound E Gamma e v iv qMap P :
+  eval_precond E P
   -> (forall ql qh, FloverMap.find e qMap = Some (ql, qh) -> ~ eval_smt_logic E ql)
   -> eval_expr E (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) v REAL
   -> (Q2R (fst iv) <= v)%R
@@ -55,14 +55,14 @@ Proof.
   symmetry in Hchk.
   andb_to_prop Hchk.
   rewrite <- Q2R_max. apply Rmax_lub; auto.
-  eapply RangeBound_low_sound; eauto using precond_free_vars.
+  eapply RangeBound_low_sound; eauto.
   erewrite eval_smt_expr_complete in H; eauto.
   rewrite SMTArith2Expr_exact.
   exact H.
 Qed.
 
-Lemma tightenBounds_high_sound fVars E Gamma e v iv qMap P :
-  eval_precond fVars E P
+Lemma tightenBounds_high_sound E Gamma e v iv qMap P :
+  eval_precond E P
   -> (forall ql qh, FloverMap.find e qMap = Some (ql, qh) -> ~ eval_smt_logic E qh)
   -> eval_expr E (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) v REAL
   -> (v <= Q2R (snd iv))%R
@@ -82,14 +82,14 @@ Proof.
   symmetry in Hchk.
   andb_to_prop Hchk.
   rewrite <- Q2R_min. apply Rmin_glb; auto.
-  eapply RangeBound_high_sound; eauto using precond_free_vars.
+  eapply RangeBound_high_sound; eauto.
   erewrite eval_smt_expr_complete in H; eauto.
   rewrite SMTArith2Expr_exact.
   exact H.
 Qed.
 
-Lemma tightenBounds_sound fVars E Gamma e v iv qMap P :
-  eval_precond fVars E P
+Lemma tightenBounds_sound E Gamma e v iv qMap P :
+  eval_precond E P
   -> (forall ql qh, FloverMap.find e qMap = Some (ql, qh) -> ~ eval_smt_logic E ql /\ ~ eval_smt_logic E qh)
   -> eval_expr E (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) v REAL
   -> (Q2R (fst iv) <= v <= Q2R (snd iv))%R
@@ -220,7 +220,7 @@ Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: FloverM
   validSMTIntervalbounds f A P Q dVars = true ->
   dVars_range_valid dVars E A ->
   NatSet.Subset ((Expressions.usedVars f) -- dVars) fVars ->
-  eval_precond fVars E P ->
+  eval_precond E P ->
   validTypes f Gamma ->
   validRanges f A E (toRTMap (toRExpMap Gamma)).
 Proof.
@@ -439,7 +439,7 @@ Theorem validSMTIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult)
   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 ->
+    eval_precond E P ->
     NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
     unsat_queries E Q ->
     validSMTIntervalboundsCmd f A P Q dVars = true ->