Commit d8aebad0 authored by Joachim Bard's avatar Joachim Bard

fixing SMT validation

parent e5f2fd9e
......@@ -43,43 +43,64 @@ Fixpoint inlineLets (L: let_env) (e: expr Q) :=
| Cond e1 e2 e3 => Cond (inlineLets L e1) (inlineLets L e2) (inlineLets L e3)
end.
Lemma inlineLets_sound L E Gamma e v :
Lemma inlineLets_sound L E Gamma inVars outVars e v :
lets_sound L E Gamma ->
(forall x e, L x = Some e -> NatSet.Subset (NatSet.add x (freeVars e)) inVars) ->
ssa e inVars outVars ->
eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v REAL ->
eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp (inlineLets L e))) v
REAL.
Proof.
induction e in L, E, v |- *; cbn; intros Lsound H.
induction e in L, E, inVars, v |- *; cbn; intros Lsound LfVars_valid ssa_e H.
- Flover_compute; eauto.
- auto.
- inversion H; subst; econstructor; eauto.
+ destruct m; try discriminate.
inversion ssa_e; subst.
eauto.
+ destruct m; try discriminate.
inversion ssa_e; subst.
eauto.
- inversion H; subst; econstructor; eauto.
+ assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
inversion ssa_e; subst.
subst. eauto.
+ assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
inversion ssa_e; subst.
subst. eauto.
- inversion H; subst; econstructor; eauto.
+ assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
inversion ssa_e; subst.
subst. eauto.
+ assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
inversion ssa_e; subst.
subst. eauto.
+ assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
inversion ssa_e; subst.
subst. eauto.
- inversion H; subst; econstructor; eauto.
inversion ssa_e; subst.
assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst. eauto.
- inversion H; subst. econstructor; eauto.
apply IHe2; eauto.
- inversion H; subst.
inversion ssa_e; subst.
econstructor; eauto.
eapply (IHe2 _ _ (NatSet.add n inVars)); eauto.
2: intros; set_tac; right; eapply LfVars_valid; eauto;
set_tac; tauto.
intros x e v'.
unfold updEnv.
destruct (x =? n) eqn: Heq.
+ intros Hx He. inversion He; subst.
destruct (x =? n) eqn: Heq.
+ intros Hx He.
apply beq_nat_true in Heq; subst.
set_tac. exfalso. apply H11. eapply LfVars_valid; eauto.
set_tac.
(*
inversion He; subst.
rewrite Heq in *.
assert (v' = v1) by congruence. subst.
apply eval_expr_ignore_bind; auto.
* eapply Lsound.
admit.
(*
apply eval_expr_ignore_bind; auto.
......@@ -87,6 +108,7 @@ Proof.
rewrite freeVars_toREval_toRExp_compat.
set_tac.
intros <- H0. inversion H0; subst.
*)
*)
+ intros H0 H1.
inversion H1; subst. rewrite Heq in *.
......@@ -94,21 +116,20 @@ Proof.
* eapply Lsound; eauto. now constructor.
* rewrite freeVars_toREval_toRExp_compat.
set_tac. intros ?.
(*
assert (n fVars dVars) by (eapply Lvars_valid; eauto).
eauto.
*)
admit.
apply H11. eapply LfVars_valid; eauto.
set_tac.
- inversion H; subst.
+ assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
inversion ssa_e; subst.
subst.
assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst. eapply Cond_then; eauto.
+ assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
inversion ssa_e; subst.
subst.
assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst. eapply Cond_else; eauto.
Admitted.
Qed.
(* (forall x e, L x = Some e -> NatSet.Subset (freeVars e) (fVars dVars)) -> *)
......@@ -325,7 +346,7 @@ Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: precond
(Q: usedQueries) L fVars dVars outVars (E: env) Gamma :
unsat_queries Q ->
lets_sound L E Gamma ->
(forall x e, L x = Some e -> NatSet.Subset (freeVars e) (fVars dVars)) ->
(forall x e, L x = Some e -> NatSet.Subset (NatSet.add x (freeVars e)) (fVars dVars)) ->
ssa f (fVars dVars) outVars ->
validSMTIntervalbounds f A P Q L dVars = true ->
dVars_range_valid dVars E A ->
......@@ -393,7 +414,8 @@ Proof.
split; auto.
canonize_hyps.
eapply Rle_trans2; eauto.
eapply tightenBounds_sound; eauto using inlineLets_sound.
eapply tightenBounds_sound; eauto.
eapply inlineLets_sound; eauto.
cbn. rewrite !Q2R_opp. lra.
+ rename L1 into nodiv0.
apply le_neq_bool_to_lt_prop in nodiv0.
......@@ -551,7 +573,9 @@ Proof.
(vF1 * vF2) REAL).
{ eapply Binop_dist' with (delta := 0%R); try congruence;
try rewrite Rabs_R0; cbn; try lra; try reflexivity; eauto. }
eapply tightenBounds_sound; eauto using inlineLets_sound.
eapply tightenBounds_sound; eauto.
eapply inlineLets_sound; eauto.
econstructor; eauto.
cbn. now rewrite ?Q2R_min4, ?Q2R_max4, ?Q2R_mult.
- destruct types_defined
as [mG [find_mG [[validt_f _] _]]].
......@@ -604,11 +628,13 @@ Proof.
* eapply Lsound; eauto. now constructor.
* rewrite freeVars_toREval_toRExp_compat.
set_tac. intros ?.
assert (n fVars dVars) by (eapply Lvars_valid; eauto).
assert (n fVars dVars) by (eapply Lvars_valid; eauto; set_tac).
eauto.
- intros x e'. unfold updLets. destruct (x =? n) eqn: Heq.
+ intros H0. injection H0. intros <-.
eapply NatSetProps.subset_trans; eauto. set_tac. tauto.
apply beq_nat_true in Heq; subst.
set_tac. destruct H1 as [? | [_ ?]]; auto.
apply H in H1. set_tac. tauto.
+ intros H0.
eapply NatSetProps.subset_trans. eauto. set_tac. tauto.
- eapply ssa_equal_set; eauto.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment