Skip to content

GitLab

Commit 0c91f793 authored by Heiko Becker's avatar Heiko Becker
Browse files

Proof remaining admits. Slight changes to iv bounds soundness where necessary

parent 9790dfdd
Hide whitespace changes
Inline Side-by-side
Showing with 426 additions and 223 deletions
coq/CertificateChecker.v
View file @ 0c91f793
......@@ -84,12 +84,19 @@ Proof.
destruct iv as [ivlo ivhi].
rewrite absenv_eq; simpl.
eapply (validErrorboundCmd_sound); eauto.
- hnf.
intros a; split; intros in_set.
+ rewrite NatSet.union_spec in in_set.
destruct in_set as [in_fV | in_empty]; try auto.
- instantiate (1 := outVars).
eapply ssa_equal_set; try eauto.
hnf.
intros a; split; intros in_union.
+ rewrite NatSet.union_spec in in_union.
destruct in_union as [in_fVars | in_empty]; try auto.
inversion in_empty.
+ rewrite NatSet.union_spec; auto.
- hnf.
intros a in_set.
rewrite NatSet.diff_spec in in_set.
destruct in_set as [ in_set not_in_empty].
eapply ssa_subset_freeVars; eauto.
- intros v v_in_empty.
rewrite NatSet.mem_spec in v_in_empty.
inversion v_in_empty.
......
coq/Commands.v
View file @ 0c91f793
......@@ -38,13 +38,13 @@ Inductive bstep : cmd R -> env -> R -> R -> Prop :=
eval_exp eps E e v ->
bstep (Ret e) E eps v.
Fixpoint freeVars (f:cmd Q) :NatSet.t :=
Fixpoint freeVars V (f:cmd V) :NatSet.t :=
match f with
| Let x e1 g => NatSet.remove x (NatSet.union (Expressions.freeVars e1) (freeVars g))
| Ret e => Expressions.freeVars e
end.
Fixpoint definedVars (f:cmd Q) :NatSet.t :=
Fixpoint definedVars V (f:cmd V) :NatSet.t :=
match f with
| Let x _ g => NatSet.add x (definedVars g)
| Ret _ => NatSet.empty
......
coq/ErrorValidation.v
View file @ 0c91f793
......@@ -143,16 +143,14 @@ Proof.
{ rewrite <- maxAbs_impl_RmaxAbs.
apply contained_leq_maxAbs_val.
unfold contained; simpl.
pose proof (validIntervalbounds_sound (Var Q x) A P dVars (E:=fun y : nat => if y =? x then Some nR else E1 y) (vR:=nR) bounds_valid) as valid_bounds_prf.
pose proof (validIntervalbounds_sound (Var Q x) A P (E:=fun y : nat => if y =? x then Some nR else E1 y) (vR:=nR) bounds_valid (fVars := (NatSet.add x fVars))) as valid_bounds_prf.
rewrite absenv_var in valid_bounds_prf; simpl in valid_bounds_prf.
apply valid_bounds_prf; try auto.
intros v v_mem_diff.
eapply P_valid.
rewrite NatSet.mem_spec, NatSet.add_spec.
rewrite NatSet.mem_spec, NatSet.diff_spec in v_mem_diff.
destruct v_mem_diff as [v_eq_x v_no_dVar].
rewrite NatSet.singleton_spec in v_eq_x.
auto. }
rewrite NatSet.diff_spec, NatSet.singleton_spec in v_mem_diff.
destruct v_mem_diff as [v_eq v_no_dVar].
subst.
rewrite NatSet.add_spec; auto. }
+ apply IHapproxCEnv; try auto.
* constructor; auto.
* constructor; auto.
......@@ -1938,6 +1936,7 @@ Qed.
Theorem validErrorbound_sound (e:exp Q):
forall E1 E2 fVars dVars absenv nR nF err P elo ehi,
approxEnv E1 absenv fVars dVars E2 ->
NatSet.Subset (NatSet.diff (Expressions.freeVars e) dVars) fVars ->
eval_exp 0%R E1 (toRExp e) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e) nF ->
validErrorbound e absenv dVars = true ->
......@@ -1953,12 +1952,12 @@ Theorem validErrorbound_sound (e:exp Q):
Proof.
induction e;
try (intros E1 E2 fVars dVars absenv nR nF err P elo ehi;
intros approxCEnv eval_real eval_float valid_error valid_intv valid_dVars P_valid absenv_eq).
intros approxCEnv fVars_subset eval_real eval_float valid_error valid_intv valid_dVars P_valid absenv_eq).
- eapply validErrorboundCorrectVariable; eauto.
- pose proof (validIntervalbounds_sound (Const v) absenv P dVars (vR:=nR) valid_intv valid_dVars).
- pose proof (validIntervalbounds_sound (Const v) absenv P (vR:=nR) valid_intv valid_dVars (fVars:=fVars))
as bounds_valid.
eapply validErrorboundCorrectConstant; eauto.
rewrite absenv_eq in *; simpl in *.
apply H; try auto. admit.
rewrite absenv_eq in *; simpl in *; auto.
- unfold validErrorbound in valid_error.
rewrite absenv_eq in valid_error.
andb_to_prop valid_error.
......@@ -1981,79 +1980,104 @@ Proof.
rewrite absenv_eq, absenv_e1, absenv_e2 in valid_intv.
andb_to_prop valid_intv.
inversion eval_real; subst.
inversion eval_float; subst.
apply binary_unfolding in eval_float.
destruct eval_float as [vF1 [vF2 [ eval_vF1 [eval_vF2 eval_float]]]].
simpl in *.
pose proof (validIntervalbounds_sound e1 absenv P dVars (vR:=v1) L2 valid_dVars).
rewrite absenv_e1 in H.
pose proof (validIntervalbounds_sound e2 absenv P dVars (vR:=v2) R2 valid_dVars).
rewrite absenv_e2 in H0;
pose proof (validIntervalbounds_sound e1 absenv P (vR:=v1) L2 valid_dVars (fVars:=fVars))
as valid_bounds_e1.
rewrite absenv_e1 in valid_bounds_e1.
pose proof (validIntervalbounds_sound e2 absenv P (vR:=v2) R2 valid_dVars (fVars:=fVars))
as valid_bounds_e2.
rewrite absenv_e2 in valid_bounds_e2;
simpl in *.
assert (eval_exp (Q2R machineEpsilon) (updEnv 2 v3 (updEnv 1 v0 emptyEnv))
(Binop b (Var Rdefinitions.R 1) (Var Rdefinitions.R 2)) (perturb (evalBinop b v0 v3) delta0)) by admit.
destruct b.
+ eapply (validErrorboundCorrectAddition (e1:=e1) absenv); eauto.
unfold validErrorbound.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
apply Is_true_eq_true.
apply andb_prop_intro; split.
* apply Is_true_eq_left in L. auto.
* apply andb_prop_intro.
split; try auto.
apply andb_prop_intro.
split; apply Is_true_eq_left; try auto.
apply L1.
apply R.
apply Is_true_eq_left; apply R0.
* admit.
* admit.
+ eapply (validErrorboundCorrectSubtraction (e1:=e1) absenv); eauto.
unfold validErrorbound.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
apply Is_true_eq_true.
apply andb_prop_intro; split.
* apply Is_true_eq_left in L. auto.
* apply andb_prop_intro.
split; try auto.
apply andb_prop_intro.
split; apply Is_true_eq_left; try auto.
apply L1.
apply R.
apply Is_true_eq_left; apply R0.
* admit.
* admit.
+ eapply (validErrorboundCorrectMult (e1 := e1) absenv); eauto.
unfold validErrorbound.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
apply Is_true_eq_true.
apply andb_prop_intro; split.
* apply Is_true_eq_left in L. auto.
* apply andb_prop_intro.
split; try auto.
apply andb_prop_intro.
split; apply Is_true_eq_left; try auto.
apply L1.
apply R.
apply Is_true_eq_left; apply R0.
* admit.
* admit.
+ eapply (validErrorboundCorrectDiv (e1 := e1) absenv); eauto.
unfold validErrorbound.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
apply Is_true_eq_true.
apply andb_prop_intro; split.
* apply Is_true_eq_left in L. auto.
* apply andb_prop_intro.
split; try auto.
apply andb_prop_intro.
split; apply Is_true_eq_left; try auto.
apply L1.
apply R.
apply Is_true_eq_left; apply R0.
* admit.
* admit.
* andb_to_prop R1.
auto.
Admitted.
assert (Rabs (v1 - vF1) <= Q2R err1 /\ Rabs (v2 - vF2) <= Q2R err2)%R.
+ split.
* eapply IHe1; eauto.
hnf. intros a in_diff.
rewrite NatSet.diff_spec in in_diff.
apply fVars_subset.
destruct in_diff.
rewrite NatSet.diff_spec, NatSet.union_spec.
split; auto.
* eapply IHe2; eauto.
hnf. intros a in_diff.
rewrite NatSet.diff_spec in in_diff.
apply fVars_subset.
destruct in_diff.
rewrite NatSet.diff_spec, NatSet.union_spec.
split; auto.
+ destruct H.
assert ((Q2R ivlo1 <= v1 <= Q2R ivhi1) /\ (Q2R ivlo2 <= v2 <= Q2R ivhi2))%R.
* split.
{ apply valid_bounds_e1; try auto.
hnf. intros a in_diff.
rewrite NatSet.diff_spec in in_diff.
destruct in_diff as [in_freeVars no_dVar].
apply fVars_subset.
rewrite NatSet.diff_spec, NatSet.union_spec.
split; try auto. }
{ apply valid_bounds_e2; try auto.
hnf. intros a in_diff.
rewrite NatSet.diff_spec in in_diff.
destruct in_diff as [in_freeVars no_dVar].
apply fVars_subset.
rewrite NatSet.diff_spec, NatSet.union_spec.
split; try auto. }
* destruct H1. destruct b.
{ eapply (validErrorboundCorrectAddition (e1:=e1) absenv); eauto.
unfold validErrorbound.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
apply Is_true_eq_true.
apply andb_prop_intro; split.
- apply Is_true_eq_left in L. auto.
- apply andb_prop_intro.
split; try auto.
apply andb_prop_intro.
split; apply Is_true_eq_left; try auto.
apply L1.
apply R.
apply Is_true_eq_left; apply R0. }
{ eapply (validErrorboundCorrectSubtraction (e1:=e1) absenv); eauto.
unfold validErrorbound.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
apply Is_true_eq_true.
apply andb_prop_intro; split.
- apply Is_true_eq_left in L. auto.
- apply andb_prop_intro.
split; try auto.
apply andb_prop_intro.
split; apply Is_true_eq_left; try auto.
apply L1.
apply R.
apply Is_true_eq_left; apply R0. }
{ eapply (validErrorboundCorrectMult (e1 := e1) absenv); eauto.
unfold validErrorbound.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
apply Is_true_eq_true.
apply andb_prop_intro; split.
- apply Is_true_eq_left in L. auto.
- apply andb_prop_intro.
split; try auto.
apply andb_prop_intro.
split; apply Is_true_eq_left; try auto.
apply L1.
apply R.
apply Is_true_eq_left; apply R0. }
{ eapply (validErrorboundCorrectDiv (e1 := e1) absenv); eauto.
unfold validErrorbound.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
apply Is_true_eq_true.
apply andb_prop_intro; split.
- apply Is_true_eq_left in L. auto.
- apply andb_prop_intro.
split; try auto.
apply andb_prop_intro.
split; apply Is_true_eq_left; try auto.
apply L1.
apply R.
apply Is_true_eq_left; apply R0.
- andb_to_prop R1; auto. }
Qed.
Lemma validErrorbound_subset e absenv dVars dVars':
validErrorbound e absenv dVars = true ->
......@@ -2076,18 +2100,20 @@ Proof.
* case_eq (NatSet.mem n dVars'); intros case_mem';
apply Is_true_eq_left; auto.
- destruct (absenv (Binop b e1 e2)); simpl in *.
rewrite <- andb_lazy_alt in *.
andb_to_prop validBound_e_dV.
rewrite andb_true_iff; split; try auto.
destruct (absenv e1); destruct (absenv e2).
andb_to_prop R.
rewrite <- andb_lazy_alt.
rewrite andb_true_iff; split; try auto.
repeat (rewrite andb_true_iff; split); auto.
Qed.
Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult):
forall E1 E2 inVars outVars fVars dVars vR vF elo ehi err P,
forall E1 E2 outVars fVars dVars vR vF elo ehi err P,
approxEnv E1 absenv fVars dVars E2 ->
ssaPrg f inVars outVars ->
NatSet.Equal (NatSet.union fVars dVars) inVars ->
ssaPrg f (NatSet.union fVars dVars) outVars ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
bstep (toRCmd f) E1 0%R vR ->
bstep (toRCmd f) E2 (Q2R RationalSimps.machineEpsilon) vF ->
validErrorboundCmd f absenv dVars = true ->
......@@ -2102,8 +2128,8 @@ Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult):
(Rabs (vR - vF) <= (Q2R err))%R.
Proof.
induction f;
intros E1 E2 inVars outVars fVars dVars vR vF elo ehi err P;
intros approxc1c2 ssa_f inVars_union eval_real eval_float valid_bounds valid_intv fVars_sound P_valid absenv_res.
intros E1 E2 outVars fVars dVars vR vF elo ehi err P;
intros approxc1c2 ssa_f freeVars_subset eval_real eval_float valid_bounds valid_intv fVars_sound P_valid absenv_res.
- simpl in eval_real, eval_float.
inversion eval_real; inversion eval_float; subst.
inversion ssa_f; subst.
......@@ -2129,12 +2155,25 @@ Proof.
destruct absenv_e as [iv [err_e absenv_e]].
destruct iv.
eapply validErrorbound_sound; eauto.
simpl in valid_intv.
andb_to_prop valid_intv.
assumption.
instantiate (1 := q0). instantiate (1 := q).
rewrite absenv_e; auto. }
* inversion ssa_f; subst.
- hnf. intros a a_in_diff.
apply freeVars_subset.
rewrite NatSet.diff_spec in *.
simpl.
destruct a_in_diff.
split; try auto.
rewrite NatSet.remove_spec, NatSet.union_spec.
split; try auto.
hnf; intros; subst.
apply validVars_valid_subset in H2.
specialize (H2 n H3).
rewrite <- NatSet.mem_spec in H2.
rewrite H2 in *; congruence.
- simpl in valid_intv.
andb_to_prop valid_intv.
assumption.
- instantiate (1 := q0). instantiate (1 := q).
rewrite absenv_e; auto. }
(* * inversion ssa_f; subst.
case_eq (NatSet.mem n fVars); intros case_mem.
{ rewrite NatSet.mem_spec in case_mem.
assert (NatSet.In n fVars \/ NatSet.In n dVars) as in_disj by (left; auto).
......@@ -2148,7 +2187,7 @@ Proof.
rewrite NatSet.mem_spec in case_union.
rewrite inVars_union in case_union.
rewrite <- NatSet.mem_spec in case_union.
rewrite case_union in H7; inversion H7. }
rewrite case_union in H7; inversion H7. } *)
+ simpl in valid_bounds.
andb_to_prop valid_bounds.
rename L0 into validbound_e;
......@@ -2156,28 +2195,28 @@ Proof.
rename R into valid_rec.
simpl in valid_intv;
andb_to_prop valid_intv.
eapply (IHf (updEnv n v E1) (updEnv n v0 E2) _ _ _ _ vR vF elo ehi err P); eauto.
* hnf; intros a; split; intros in_set.
{ rewrite NatSet.add_spec; rewrite NatSet.union_spec in in_set.
destruct in_set.
- right.
apply (NatSetProps.Dec.F.union_2 dVars) in H0.
rewrite <- inVars_union; auto.
- rewrite NatSet.add_spec in H0.
destruct H0; try auto.
apply (NatSetProps.Dec.F.union_3 fVars) in H0.
right; rewrite <- inVars_union; auto. }
{ rewrite NatSet.add_spec in in_set; rewrite NatSet.union_spec.
rewrite NatSet.add_spec.
destruct in_set; try auto.
rewrite <- inVars_union in H0.
rewrite NatSet.union_spec in H0.
destruct H0; auto. }
eapply (IHf (updEnv n v E1) (updEnv n v0 E2) _ _ _ vR vF elo ehi err P); eauto.
* instantiate (1 := outVars).
eapply ssa_equal_set; eauto.
hnf. intros a; split; intros in_set.
{ rewrite NatSet.add_spec, NatSet.union_spec;
rewrite NatSet.union_spec, NatSet.add_spec in in_set.
destruct in_set as [P1 | [ P2 | P3]]; auto. }
{ rewrite NatSet.add_spec, NatSet.union_spec in in_set;
rewrite NatSet.union_spec, NatSet.add_spec.
destruct in_set as [P1 | [ P2 | P3]]; auto. }
* hnf. intros a in_diff.
rewrite NatSet.diff_spec, NatSet.add_spec in in_diff.
destruct in_diff as [ in_freeVars no_dVar].
apply freeVars_subset.
simpl.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
split; try auto.
* intros v1 v1_mem.
unfold updEnv.
case_eq (v1 =? n); intros v1_eq.
{ rename L into eq_lo;
rename R1 into eq_hi.
{ rename R1 into eq_lo;
rename R0 into eq_hi.
apply Qeq_bool_iff in eq_lo.
apply Qeq_eqR in eq_lo.
apply Qeq_bool_iff in eq_hi.
......@@ -2186,15 +2225,34 @@ Proof.
rewrite <- eq_lo, <- eq_hi.
exists v; split; try auto.
eapply validIntervalbounds_sound; eauto.
admit. }
hnf. intros a a_mem_diff.
rewrite NatSet.diff_spec in a_mem_diff.
destruct a_mem_diff as [a_mem_freeVars a_no_dVar].
apply freeVars_subset.
simpl. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
split; try auto.
split; try auto.
hnf; intros; subst.
apply validVars_valid_subset in H2.
specialize (H2 n a_mem_freeVars).
rewrite <- NatSet.mem_spec in H2.
rewrite H2 in *; congruence. }
{ rewrite NatSet.mem_spec in v1_mem.
rewrite NatSet.add_spec in v1_mem.
rewrite Nat.eqb_neq in v1_eq.
destruct v1_mem.
- exfalso; apply v1_eq; auto.
- apply fVars_sound. rewrite NatSet.mem_spec; auto.
}
* admit.
- apply fVars_sound. rewrite NatSet.mem_spec; auto. }
* intros v1 mem_fVars.
specialize (P_valid v1 mem_fVars).
unfold updEnv.
case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try auto.
rewrite Nat.eqb_eq in case_v1; subst.
assert (NatSet.In n (NatSet.union fVars dVars))
as in_union
by (rewrite NatSet.mem_spec in *; rewrite NatSet.union_spec; auto).
rewrite <- NatSet.mem_spec in in_union.
rewrite in_union in *; congruence.
- inversion eval_real; inversion eval_float; subst.
unfold updEnv; simpl.
unfold validErrorboundCmd in valid_bounds.
......@@ -2203,4 +2261,4 @@ Proof.
destruct absenv_e as [iv [err_e absenv_e]].
destruct iv.
eapply validErrorbound_sound; eauto.
Admitted.
Qed.
\ No newline at end of file
coq/IntervalValidation.v
View file @ 0c91f793
......@@ -13,30 +13,34 @@ Require Export Daisy.IntervalArithQ Daisy.IntervalArith Daisy.ssaPrgs.
Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :=
let (intv, _) := absenv e in
match e with
| Var _ v => if NatSet.mem v validVars then true else isSupersetIntv (P v) intv
| Var _ v =>
if NatSet.mem v validVars
then true
else isSupersetIntv (P v) intv && (Qleb (ivlo (P v)) (ivhi (P v)))
| Const n => isSupersetIntv (n,n) intv
| Unop o f =>
let rec := validIntervalbounds f absenv P validVars in
let (iv, _) := absenv f in
let opres :=
if validIntervalbounds f absenv P validVars
then
let (iv, _) := absenv f in
match o with
| Neg =>
let new_iv := negateIntv iv in
isSupersetIntv new_iv intv
| Inv =>
let nodiv0 := orb
(andb (Qleb (ivhi iv) 0) (negb (Qeq_bool (ivhi iv) 0)))
(andb (Qleb 0 (ivlo iv)) (negb (Qeq_bool (ivlo iv) 0))) in
let new_iv := invertIntv iv in
andb (isSupersetIntv new_iv intv) nodiv0
if (((Qleb (ivhi iv) 0) && (negb (Qeq_bool (ivhi iv) 0))) ||
((Qleb 0 (ivlo iv)) && (negb (Qeq_bool (ivlo iv) 0))))
then
let new_iv := invertIntv iv in
isSupersetIntv new_iv intv
else false
end
in
andb rec opres
else false
| Binop op f1 f2 =>
let rec := andb (validIntervalbounds f1 absenv P validVars) (validIntervalbounds f2 absenv P validVars) in
let (iv1,_) := absenv f1 in
let (iv2,_) := absenv f2 in
let opres :=
if ((validIntervalbounds f1 absenv P validVars) &&
(validIntervalbounds f2 absenv P validVars))
then
let (iv1,_) := absenv f1 in
let (iv2,_) := absenv f2 in
match op with
| Plus =>
let new_iv := addIntv iv1 iv2 in
......@@ -48,23 +52,24 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) (vali
let new_iv := multIntv iv1 iv2 in
isSupersetIntv new_iv intv
| Div =>
let nodiv0 := orb
(andb (Qleb (ivhi iv2) 0) (negb (Qeq_bool (ivhi iv2) 0)))
(andb (Qleb 0 (ivlo iv2)) (negb (Qeq_bool (ivlo iv2) 0))) in
let new_iv := divideIntv iv1 iv2 in
andb (isSupersetIntv new_iv intv) nodiv0
if (((Qleb (ivhi iv2) 0) && (negb (Qeq_bool (ivhi iv2) 0))) ||
((Qleb 0 (ivlo iv2)) && (negb (Qeq_bool (ivlo iv2) 0))))
then
let new_iv := divideIntv iv1 iv2 in
isSupersetIntv new_iv intv
else false
end
in
andb rec opres
else false
end.
Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :bool:=
match f with
| Let x e g =>
validIntervalbounds e absenv P validVars &&
(Qeq_bool (fst (fst (absenv e))) (fst (fst (absenv (Var Q x)))) &&
Qeq_bool (snd (fst (absenv e))) (snd (fst (absenv (Var Q x))))) &&
validIntervalboundsCmd g absenv P (NatSet.add x validVars)
if (validIntervalbounds e absenv P validVars &&
Qeq_bool (fst (fst (absenv e))) (fst (fst (absenv (Var Q x)))) &&
Qeq_bool (snd (fst (absenv e))) (snd (fst (absenv (Var Q x)))))
then validIntervalboundsCmd g absenv P (NatSet.add x validVars)
else false
|Ret e =>
validIntervalbounds e absenv P validVars
end.
......@@ -84,7 +89,9 @@ Proof.
rewrite case_mem in approx_true; simpl in *.
+ rewrite NatSet.mem_spec in case_mem.
contradiction.
+ apply Is_true_eq_left in approx_true; auto.
+ apply Is_true_eq_left in approx_true.
apply andb_prop_elim in approx_true.
destruct approx_true; auto.
- intros approx_true v0 v_in_fV; simpl in *.
inversion v_in_fV.
- intros approx_unary_true v v_in_fV.
......@@ -140,11 +147,13 @@ Proof.
env_assert absenv (Binop Div e1 e2) abs_div; destruct abs_div as [iv_div [err_div abs_div]].
env_assert absenv e1 abs_e1; destruct abs_e1 as [iv_e1 [err_e1 abs_e1]].
rewrite abs_div, abs_e1, absenv_eq in validBounds.
repeat (rewrite <- andb_lazy_alt in validBounds).
apply Is_true_eq_left in validBounds.
apply andb_prop_elim in validBounds.
destruct validBounds as [_ validBounds]; apply andb_prop_elim in validBounds.
destruct validBounds as [_ nodiv0].
destruct validBounds as [nodiv0 _].
apply Is_true_eq_true in nodiv0.
unfold isSupersetIntv in *; simpl in *.
apply le_neq_bool_to_lt_prop; auto.
Qed.
......@@ -154,26 +163,27 @@ Fixpoint getRetExp (V:Type) (f:cmd V) :=
| Ret e => e
end.
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) V E:
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars E:
forall vR,
validIntervalbounds f absenv P V = true ->
(forall v, NatSet.mem v V = true ->
validIntervalbounds f absenv P dVars = true ->
(forall v, NatSet.mem v dVars = true ->
exists vR, E v = Some vR /\
(Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
(forall v, NatSet.mem v (NatSet.diff (Expressions.freeVars f) V)= true ->
NatSet.Subset (NatSet.diff (Expressions.freeVars f) dVars) fVars ->
(forall v, NatSet.mem v fVars = true ->
exists vR, E v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
eval_exp 0%R E (toRExp f) vR ->
(Q2R (fst (fst(absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R.
Proof.
induction f; intros vR valid_bounds valid_definedVars valid_freeVars eval_f.
induction f; intros vR valid_bounds valid_definedVars freeVars_subset valid_freeVars eval_f.
- unfold validIntervalbounds in valid_bounds.
env_assert absenv (Var Q n) absenv_var.
destruct absenv_var as [ iv [err absenv_var]].
specialize (valid_freeVars n).
rewrite absenv_var in *; simpl in *.
inversion eval_f; subst.
case_eq (NatSet.mem n V); intros case_mem; rewrite case_mem in *; simpl in *.
case_eq (NatSet.mem n dVars); intros case_mem; rewrite case_mem in *; simpl in *.
+ specialize (valid_definedVars n case_mem).
destruct valid_definedVars as [vR' [E_n_eq precond_sound]].
rewrite E_n_eq in *.
......@@ -182,19 +192,23 @@ Proof.
+ repeat (rewrite delta_0_deterministic in *; try auto).
unfold isSupersetIntv in valid_bounds.
andb_to_prop valid_bounds.
apply Qle_bool_iff in L;
apply Qle_bool_iff in R.
apply Qle_Rle in L;
apply Qle_Rle in R.
apply Qle_bool_iff in L0;