Commit ca317706 authored by Heiko Becker's avatar Heiko Becker

Prove soundness for interval validation

parent 9d6ce326
......@@ -39,9 +39,11 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
let new_iv := multIntv iv1 iv2 in
isSupersetIntv new_iv intv
| Div =>
let nodiv0 := orb (Qleb (ivhi iv2) 0) (Qleb 0 (ivlo iv2)) in
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
isSupersetIntv new_iv intv
andb (isSupersetIntv new_iv intv) nodiv0
end
in
andb rec opres
......@@ -93,6 +95,30 @@ Qed.
Ltac env_assert absenv e name :=
assert (exists iv err, absenv e = (iv,err)) as name by (destruct (absenv e); repeat eexists; auto).
Lemma validBoundsDiv_uneq_zero e1 e2 absenv P ivlo_e2 ivhi_e2 err:
absenv e2 = ((ivlo_e2,ivhi_e2), err) ->
validIntervalbounds (Binop Div e1 e2) absenv P = true ->
(ivhi_e2 < 0) \/ (0 < ivlo_e2).
Proof.
intros absenv_eq validBounds.
unfold validIntervalbounds in validBounds.
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.
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].
apply orb_prop_elim in nodiv0.
destruct nodiv0 as [lt_0 | lt_0];
apply andb_prop_elim in lt_0; destruct lt_0 as [le_0 neq_0];
apply Is_true_eq_true in le_0; apply Is_true_eq_true in neq_0;
apply negb_true_iff in neq_0; apply Qeq_bool_neq in neq_0;
rewrite Qle_bool_iff in le_0;
rewrite Qle_lteq in le_0; destruct le_0 as [lt_0 | eq_0];
[ | exfalso; apply neq_0; auto | | exfalso; apply neq_0; symmetry; auto]; auto.
Qed.
Theorem validIntervalbounds_sound (e:exp Q):
forall (absenv:analysisResult) (P:precond) cenv vR,
precondValidForExec P cenv ->
......@@ -262,28 +288,52 @@ Proof.
+ pose proof (divisionIsValid v1 v2 (Q2R (fst iv1), Q2R (snd iv1)) (Q2R (fst iv2),Q2R (snd iv2))) as valid_div.
unfold contained in valid_div.
unfold isSupersetIntv in valid_bin.
apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_bin nodiv0].
apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
destruct valid_div as [valid_div_lo valid_div_hi]; try auto.
* admit.
* unfold divideInterval, IVlo, IVhi in valid_div_lo, valid_div_hi.
simpl in *.
split.
{ eapply Rle_trans. apply valid_lo.
unfold ivlo. unfold multIntv.
simpl in valid_div_lo.
rewrite <- Q2R_inv in valid_div_lo; [ | admit].
rewrite <- Q2R_inv in valid_div_lo; [ | admit].
repeat rewrite <- Q2R_mult in valid_div_lo.
rewrite <- Q2R_min4 in valid_div_lo; auto. }
{ eapply Rle_trans.
Focus 2.
apply valid_hi.
simpl in valid_div_hi.
rewrite <- Q2R_inv in valid_div_hi; [ | admit].
rewrite <- Q2R_inv in valid_div_hi; [ | admit].
repeat rewrite <- Q2R_mult in valid_div_hi.
rewrite <- Q2R_max4 in valid_div_hi; auto. }
Admitted.
\ No newline at end of file
apply orb_prop_elim in nodiv0.
assert (snd iv2 < 0 \/ 0 < fst iv2).
* destruct nodiv0 as [lt_0 | lt_0];
apply andb_prop_elim in lt_0; destruct lt_0 as [le_0 neq_0];
apply Is_true_eq_true in le_0; apply Is_true_eq_true in neq_0;
apply negb_true_iff in neq_0; apply Qeq_bool_neq in neq_0;
rewrite Qle_bool_iff in le_0;
rewrite Qle_lteq in le_0; destruct le_0 as [lt_0 | eq_0];
[ | exfalso; apply neq_0; auto | | exfalso; apply neq_0; symmetry; auto]; auto.
* destruct valid_div as [valid_div_lo valid_div_hi]; simpl; try auto.
{ rewrite <- Q2R0_is_0.
destruct H; [left | right]; apply Qlt_Rlt; auto. }
{ unfold divideInterval, IVlo, IVhi in valid_div_lo, valid_div_hi.
simpl in *.
assert (Q2R (fst iv2) <= (Q2R (snd iv2)))%R by lra.
assert (~ snd iv2 == 0).
- destruct H; try lra.
hnf; intros ivhi2_0.
apply Rle_Qle in H0.
rewrite ivhi2_0 in H0.
lra.
- assert (~ fst iv2 == 0).
+ destruct H; try lra.
hnf; intros ivlo2_0.
apply Rle_Qle in H0.
rewrite ivlo2_0 in H0.
lra.
+ split.
* eapply Rle_trans. apply valid_lo.
unfold ivlo. unfold multIntv.
simpl in valid_div_lo.
rewrite <- Q2R_inv in valid_div_lo; [ | auto].
rewrite <- Q2R_inv in valid_div_lo; [ | auto].
repeat rewrite <- Q2R_mult in valid_div_lo.
rewrite <- Q2R_min4 in valid_div_lo; auto.
* eapply Rle_trans.
Focus 2.
apply valid_hi.
simpl in valid_div_hi.
rewrite <- Q2R_inv in valid_div_hi; [ | auto].
rewrite <- Q2R_inv in valid_div_hi; [ | auto].
repeat rewrite <- Q2R_mult in valid_div_hi.
rewrite <- Q2R_max4 in valid_div_hi; auto. }
Qed.
\ 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