Commit 954cb8ec authored by Joachim Bard's avatar Joachim Bard

moving stuff around and trying something for lets

parent 0dc98cd9
......@@ -13,9 +13,8 @@ From Flover
Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
Infra.Ltacs Infra.RealSimps TypeValidator.
(* TODO: SMTArith is only needed for eval_precond, change that *)
From Flover
Require Export IntervalArithQ IntervalArith SMTArith ssaPrgs RealRangeArith.
Require Export IntervalArithQ IntervalArith ssaPrgs RealRangeArith.
Fixpoint validIntervalbounds (e:expr Q) (A:analysisResult) (P: FloverMap.t intv)
(validVars:NatSet.t) :bool:=
......
......@@ -6,6 +6,51 @@ From Flover
Infra.Ltacs Infra.RealSimps TypeValidator ssaPrgs IntervalArithQ
IntervalArith Commands.
Lemma eqb_var x e : FloverMapFacts.P.F.eqb (Var Q x) e = true -> e = Var Q x.
Proof.
rewrite eqb_cmp_eq. destruct e; cbn; try discriminate.
case_eq (x ?= n)%nat; intros H; try discriminate.
apply Nat.compare_eq in H. now subst.
Qed.
Lemma find_in_precond P x (iv: intv) :
FloverMap.find (Var Q x) P = Some iv -> List.In (Var Q x, iv) (FloverMap.elements P).
Proof.
rewrite FloverMapFacts.P.F.elements_o.
intros H. apply findA_find in H as [e [H _]].
apply List.find_some in H as [Hin Heq].
apply eqb_var in Heq. cbn in *. now subst.
Qed.
(*
Definition eval_precond E (P: precond) :=
forall x iv, FloverMap.find (Var Q x) P = Some iv
-> exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
*)
Definition eval_precond E (P: precond) :=
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))%R.
Definition addVar2Set (elt: (expr Q * intv)) s :=
match elt with
| (Var _ x, _) => NatSet.add x s
| _ => s
end.
Definition preVars (P: precond) :=
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.
Definition dVars_range_valid (dVars:NatSet.t) (E:env) (A:analysisResult) :Prop :=
forall v, NatSet.In v dVars ->
exists vR iv err,
......
......@@ -6,7 +6,9 @@ Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Flover.Expressions.
Require Import Flover.Infra.ExpressionAbbrevs.
Require Import Flover.ExpressionSemantics.
Require Import Flover.Commands.
Require Import Flover.Infra.Ltacs.
Require Import Flover.RealRangeArith.
Open Scope R.
......@@ -181,7 +183,7 @@ Proof with try (right; apply Rabs_R0).
induction 1.
- now constructor.
- rewrite <- (delta_0_deterministic (Q2R r) REAL 0)... constructor... auto.
- rewrite <- (delta_0_deterministic _ REAL 0)... apply (Unop_neg (m:= REAL)); auto.
- apply (Unop_neg (m:= REAL)); auto.
- rewrite <- (delta_0_deterministic _ REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
- rewrite <- (delta_0_deterministic _ REAL 0)...
......@@ -192,6 +194,26 @@ Proof with try (right; apply Rabs_R0).
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto...
Qed.
Lemma eval_smt_cmd E e1 e2 x v1 v2:
eval_smt E e2 v2 ->
(* TODO: Condition here -> *)
eval_expr E (fun _ => Some REAL) DeltaMapR (toRExp (SMTArith2Expr e1)) v1 REAL ->
eval_expr (updEnv x v1 E) (fun _ => Some REAL) DeltaMapR (toRExp (SMTArith2Expr e2)) v2 REAL.
Proof with try (right; apply Rabs_R0).
induction 1; intros He1.
- constructor; auto. unfold updEnv. admit.
- rewrite <- (delta_0_deterministic (Q2R r) REAL 0)... constructor... auto.
- apply (Unop_neg (m:= REAL)); auto.
- rewrite <- (delta_0_deterministic (_ + _) REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
- rewrite <- (delta_0_deterministic (_ - _) REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
- rewrite <- (delta_0_deterministic (_ * _) REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
- rewrite <- (delta_0_deterministic (_ / _) REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto...
Abort.
Lemma eval_expr_smt E Gamma e v :
eval_expr E (toRTMap Gamma) DeltaMapR (toREval (toRExp (SMTArith2Expr e))) v REAL
-> eval_smt E e v.
......@@ -271,52 +293,6 @@ Inductive eval_smt_logic (E: env) : SMTLogic -> Prop :=
Definition unsat_queries E qMap :=
forall e ql qh, FloverMap.find e qMap = Some (ql, qh) -> ~ eval_smt_logic E ql /\ ~ eval_smt_logic E qh.
(*
Definition eval_precond E (P: precond) :=
forall x iv, FloverMap.find (Var Q x) P = Some iv
-> exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
*)
(* TODO: move eqb_var, find_in_precond and eval_precond somewhere else *)
Lemma eqb_var x e : FloverMapFacts.P.F.eqb (Var Q x) e = true -> e = Var Q x.
Proof.
rewrite eqb_cmp_eq. destruct e; cbn; try discriminate.
case_eq (x ?= n)%nat; intros H; try discriminate.
apply Nat.compare_eq in H. now subst.
Qed.
Lemma find_in_precond P x (iv: intv) :
FloverMap.find (Var Q x) P = Some iv -> List.In (Var Q x, iv) (FloverMap.elements P).
Proof.
rewrite FloverMapFacts.P.F.elements_o.
intros H. apply findA_find in H as [e [H _]].
apply List.find_some in H as [Hin Heq].
apply eqb_var in Heq. cbn in *. now subst.
Qed.
Definition eval_precond E (P: precond) :=
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: precond) :=
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 ->
......@@ -617,3 +593,120 @@ Proof.
split; cbn; auto.
do 2 eexists. repeat split; first [eassumption | constructor].
Qed.
Fixpoint inline_expr x (e e': expr Q) :=
match e' with
| Var _ n => if (n =? x) then e else e'
| Expressions.Const _ _ => e'
| Unop op e1 => Unop op (inline_expr x e e1)
| Binop op e1 e2 => Binop op (inline_expr x e e1) (inline_expr x e e2)
| Fma e1 e2 e3 => Fma (inline_expr x e e1) (inline_expr x e e2) (inline_expr x e e3)
| Downcast m e1 => Downcast m (inline_expr x e e1)
end.
Fixpoint inline_cmd x e f :=
match f with
| Let m n e' f' => Let m n (inline_expr x e e') (inline_cmd x e f')
| Ret e' => Ret (inline_expr x e e')
end.
Fixpoint inline_all f :=
match f with
| Ret e => e
| Let _ n e f' => inline_expr n e (inline_all f')
end.
Lemma test_let_to_expr E Gamma x e1 e2 v :
bstep (toREvalCmd (toRCmd (Let REAL x e1 (Ret e2)))) E (toRTMap Gamma) DeltaMapR v REAL ->
eval_expr E (toRTMap Gamma) DeltaMapR (toREval (toRExp (inline_expr x e1 e2))) v REAL.
Proof.
intros H.
induction e2 in v, H |- *.
- cbn. case_eq (n =? x).
+ intros eq.
inversion H; subst.
inversion H10; subst.
inversion H1; subst. unfold updEnv in *.
rewrite eq in *.
injection H3; intros ?; subst.
assumption.
+ intros neq.
inversion H; subst.
inversion H10; subst.
inversion H1; subst. unfold updEnv in H3.
rewrite neq in H3.
constructor; auto.
- cbn in *.
inversion H; subst.
inversion H10; subst.
inversion H1; subst.
now constructor.
- cbn.
inversion H; subst.
inversion H10; subst.
destruct u.
+ inversion H1; subst.
destruct m; try discriminate.
econstructor; eauto.
apply IHe2.
econstructor; eauto.
now constructor.
+ inversion H1; subst.
destruct m; try discriminate.
econstructor; eauto.
apply IHe2.
econstructor; eauto.
now constructor.
- inversion H; subst.
inversion H10; subst.
inversion H1; subst.
econstructor; eauto.
+ fold toREval toRExp inline_expr.
assert (m1 = REAL) by apply (toRTMap_eval_REAL _ H8).
assert (m2 = REAL) by apply (toRTMap_eval_REAL _ H13).
subst.
apply IHe2_1.
econstructor; eauto.
now constructor.
+ fold toREval toRExp inline_expr.
assert (m1 = REAL) by apply (toRTMap_eval_REAL _ H8).
assert (m2 = REAL) by apply (toRTMap_eval_REAL _ H13).
subst.
apply IHe2_2.
econstructor; eauto.
now constructor.
- admit. (* FMA *)
- cbn in *.
apply (@Downcast_dist' _ _ REAL _ v 0); auto; try (right; apply Rabs_R0).
apply IHe2.
inversion H; subst.
econstructor; eauto.
inversion H10; subst.
inversion H1; subst.
destruct m1; try discriminate.
now constructor.
Admitted.
Lemma test_RangeBound_let_low_sound E P preQ m x e e1 e2 r Gamma v :
eval_precond E P
-> checkPre P preQ = true
-> ~ eval_smt_logic E (AndQ preQ (AndQ (LessQ e (ConstQ r)) TrueQ))
-> SMTArith2Expr e = inline_expr x e1 e2
-> bstep (toREvalCmd (toRCmd (Let m x e1 (Ret e2)))) E (toRTMap Gamma) DeltaMapR v REAL
-> Q2R r <= v.
Proof.
intros validP chk unsatQ Heq H.
eapply RangeBound_low_sound; eauto.
rewrite Heq.
eapply test_let_to_expr; eauto.
Qed.
Lemma test_RangeBound_cmd_low_sound E P preQ e f r Gamma v :
eval_precond E P
-> checkPre P preQ = true
-> ~ eval_smt_logic E (AndQ preQ (AndQ (LessQ e (ConstQ r)) TrueQ))
-> SMTArith2Expr e = inline_all f (* TODO use smt_expr_eq *)
-> bstep (toREvalCmd (toRCmd f)) E (toRTMap Gamma) DeltaMapR v REAL
-> Q2R r <= v.
Proof.
Admitted.
......@@ -14,7 +14,8 @@ From Flover
Infra.Ltacs Infra.RealSimps TypeValidator.
From Flover
Require Export IntervalArithQ IntervalArith IntervalValidation SMTArith ssaPrgs RealRangeArith.
Require Export IntervalArithQ IntervalArith IntervalValidation SMTArith ssaPrgs
RealRangeArith.
Definition tightenLowerBound (e: expr Q) (lo: Q) (q: SMTLogic) P :=
match q with
......@@ -195,25 +196,6 @@ Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: precond)
end
end.
Fixpoint validSMTIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P: precond)
(Q: usedQueries) (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: precond)
(Q: usedQueries) fVars dVars (E: env) Gamma :
unsat_queries E Q ->
......@@ -436,23 +418,134 @@ Proof.
cbn in *; lra.
Qed.
Fixpoint validSMTIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P: precond)
(Qmap: usedQueries) (validVars:NatSet.t) : bool :=
match f with
| Let m x e g =>
match FloverMap.find e A, FloverMap.find (Var Q x) A with
| Some ((e_lo,e_hi), _), Some ((x_lo, x_hi), _) =>
if (validSMTIntervalbounds e A P Qmap validVars &&
Qeq_bool (e_lo) (x_lo) &&
Qeq_bool (e_hi) (x_hi))
then validSMTIntervalboundsCmd g A P Qmap (NatSet.add x validVars)
else false
| _, _ => false
end
| Ret e =>
validSMTIntervalbounds e A P Qmap validVars
end.
Theorem validSMTIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult)
(Q: usedQueries):
forall Gamma E fVars dVars outVars P,
ssa f (NatSet.union fVars dVars) outVars ->
dVars_range_valid dVars E A ->
eval_precond E P ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
NatSet.Subset (preVars P) fVars ->
NatSet.Subset (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
intros * ssa_f dVars_sound fVars_valid preVars_free usedVars_subset
unsat_qs valid_bounds_f valid_types_f;
cbn in *.
- discriminate.
- Flover_compute.
inversion ssa_f; subst.
canonize_hyps.
pose proof (validSMTIntervalbounds_sound e Gamma (E:=E) (fVars:=fVars) unsat_qs L)
as validIV_e.
destruct valid_types_f
as [[mG [find_mG [_ [_ [validt_e validt_f]]]]] _].
assert (validRanges e A E (toRTMap (toRExpMap Gamma))) as valid_e.
{ apply validIV_e; try auto.
set_tac. repeat split; auto.
hnf; intros; subst.
set_tac. }
assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars)) (NatSet.union fVars (NatSet.add n dVars))).
{ hnf. intros a; split; intros in_set; set_tac.
- destruct in_set as [ ? | [? ?]]; try auto; set_tac.
destruct H0; auto.
- destruct in_set as [? | ?]; try auto; set_tac.
destruct H as [? | [? ?]]; auto. }
pose proof (validRanges_single _ _ _ _ valid_e) as valid_single_e.
destruct valid_single_e as [iv_e [err_v [v [find_v [eval_e valid_bounds_e]]]]].
rewrite find_v in *; inversion Heqo; subst.
specialize (IHf Gamma (updEnv n v E) fVars (NatSet.add n dVars)) as IHf_spec.
assert (validRangesCmd f A (updEnv n v E) (toRTMap (toRExpMap Gamma))).
{ eapply IHf_spec; eauto.
- symmetry in H. eapply ssa_equal_set; eauto.
- intros v0 mem_v0.
unfold updEnv.
case_eq (v0 =? n); intros v0_eq.
+ rename R1 into eq_lo;
rename R0 into eq_hi.
rewrite Nat.eqb_eq in v0_eq; subst.
exists v; eexists; eexists; repeat split; try eauto; simpl in *; lra.
+ apply dVars_sound.
set_tac.
destruct mem_v0 as [? | [? ?]]; try auto.
rewrite Nat.eqb_neq in v0_eq.
congruence.
- hnf. intros x ? ?.
unfold updEnv.
case_eq (x =? n); intros case_x; auto.
rewrite Nat.eqb_eq in case_x. subst.
set_tac.
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.
+ hnf; intros; subst. apply H1; set_tac.
+ hnf; intros. apply H1; set_tac.
- admit. (* TODO: fix def of unsat_queries *)
}
(*
destruct x_contained as [x_free | x_def].
+ destruct (types_valid x) as [m_x Gamma_x]; try set_tac.
exists m_x.
unfold updDefVars. case_eq (x =? n); intros eq_case; try auto.
rewrite Nat.eqb_eq in eq_case.
subst.
exfalso; apply H6; set_tac.
+ set_tac.
destruct x_def as [x_n | x_def]; subst.
* exists REAL; unfold updDefVars; rewrite Nat.eqb_refl; auto.
* destruct x_def. destruct (types_valid x) as [m_x Gamma_x].
{ rewrite NatSet.union_spec; auto. }
{ exists m_x.
unfold updDefVars; case_eq (x =? n); intros eq_case; try auto.
rewrite Nat.eqb_eq in eq_case; subst.
congruence. }
{ clear L R1 R0 R IHf.
hnf. intros a a_freeVar.
rewrite NatSet.diff_spec in a_freeVar.
destruct a_freeVar as [a_freeVar a_no_dVar].
apply usedVars_subset.
simpl.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
repeat split; try auto.
+ hnf; intros; subst.
apply a_no_dVar.
rewrite NatSet.add_spec; auto.
+ hnf; intros a_dVar.
apply a_no_dVar.
rewrite NatSet.add_spec; auto. } *)
repeat split; try auto.
+ intros vR ?.
assert (vR = v) by (eapply meps_0_deterministic; eauto); subst.
auto.
+ apply validRangesCmd_single in H0.
destruct H0 as [? [? [? [? [? ?]]]]].
repeat eexists; eauto.
* econstructor; try eauto.
* lra.
* lra.
- 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 [? ?].
......@@ -461,4 +554,4 @@ Proof.
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
Admitted.
\ No newline at end of file
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