Skip to content

GitLab

Commit 85fe6a93 authored by Raphaël Monat's avatar Raphaël Monat
Browse files
Options

Mixed precision port, up to interval validation

parent 7ca212cb
Hide whitespace changes
Inline Side-by-side
Showing with 119 additions and 59 deletions
coq/Infra/RationalSimps.v
View file @ 85fe6a93
......@@ -8,7 +8,7 @@ Require Import Daisy.Infra.Abbrevs Daisy.Infra.Ltacs.
Definition Qleb :=Qle_bool.
Definition Qeqb := Qeq_bool.
Definition machineEpsilon := (1#(2^53)).
(* Definition machineEpsilon := (1#(2^53)). *)
Definition maxAbs (iv:intv) :=
Qmax (Qabs (fst iv)) (Qabs (snd iv)).
......
coq/Infra/RealRationalProps.v
View file @ 85fe6a93
......@@ -139,15 +139,15 @@ Proof.
unfold Q2RP; destruct iv; apply minAbs_impl_RminAbs.
Qed.
Lemma mEps_geq_zero:
(0 <= Q2R RationalSimps.machineEpsilon)%R.
Proof.
rewrite <- Q2R0_is_0.
apply Qle_Rle.
unfold machineEpsilon.
apply Qle_bool_iff.
unfold Qle_bool; auto.
Qed.
(* Lemma mEps_geq_zero: *)
(* (0 <= Q2R RationalSimps.machineEpsilon)%R. *)
(* Proof. *)
(* rewrite <- Q2R0_is_0. *)
(* apply Qle_Rle. *)
(* unfold machineEpsilon. *)
(* apply Qle_bool_iff. *)
(* unfold Qle_bool; auto. *)
(* Qed. *)
Lemma Q_case_div_to_R_case_div a b:
(b < 0 \/ 0 < a)%Q ->
......
coq/IntervalArithQ.v
View file @ 85fe6a93
......@@ -46,6 +46,29 @@ Proof.
rewrite H0. unfold Is_true; auto.
Qed.
Definition isEqIntv (iv1:intv) (iv2:intv) :=
(ivlo iv1 == ivlo iv2) /\ (ivhi iv1 == ivhi iv2).
Lemma supIntvAntisym (iv1:intv) (iv2:intv) :
isSupersetIntv iv1 iv2 = true ->
isSupersetIntv iv2 iv1 = true ->
isEqIntv iv1 iv2.
Proof.
intros incl12 incl21.
unfold isSupersetIntv in *.
apply andb_true_iff in incl12.
apply andb_true_iff in incl21.
destruct incl12 as [incl12_low incl12_hi].
destruct incl21 as [incl21_low incl21_hi].
apply Qle_bool_iff in incl12_low.
apply Qle_bool_iff in incl12_hi.
apply Qle_bool_iff in incl21_low.
apply Qle_bool_iff in incl21_hi.
split.
- apply (Qle_antisym (ivlo iv1) (ivlo iv2)); auto.
- apply (Qle_antisym (ivhi iv1) (ivhi iv2)); auto.
Qed.
(**
Definition of validity conditions for intv operations, Addition, Subtraction, Multiplication and Division
**)
......
coq/IntervalValidation.v
View file @ 85fe6a93
......@@ -87,6 +87,12 @@ Fixpoint erasure (e:exp Q) :exp Q :=
|_ => e
end.
Fixpoint erasureCmd (c:cmd Q) :cmd Q :=
match c with
| Let m x e g => Let M0 x (erasure e) (erasureCmd g)
| Ret e => Ret (erasure e)
end.
Theorem ivbounds_approximatesPrecond_sound f absenv P V:
validIntervalbounds (erasure f) absenv P V = true ->
forall v, NatSet.In v (NatSet.diff (Expressions.usedVars f) V) ->
......@@ -136,8 +142,14 @@ Proof.
+ apply IHf2; auto.
apply Is_true_eq_true; auto.
rewrite NatSet.diff_spec; split; auto.
- admit.
Admitted.
- intros approx_rnd_true v v_in_fV.
simpl in *; destruct (absenv (Downcast M0 (erasure f))); destruct (absenv (erasure f)).
apply Is_true_eq_left in approx_rnd_true.
apply andb_prop_elim in approx_rnd_true.
destruct approx_rnd_true.
apply IHf; auto.
apply Is_true_eq_true in H; auto.
Qed.
Corollary Q2R_max4 a b c d:
Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
......@@ -176,37 +188,38 @@ Qed.
Fixpoint getRetExp (V:Type) (f:cmd V) :=
match f with
|Let x e g => getRetExp g
|Let m x e g => getRetExp g
| Ret e => e
end.
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars E:
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars (E:env):
forall vR,
validIntervalbounds f absenv P dVars = true ->
validIntervalbounds (erasure 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) ->
exists vR, E v = Some (vR, M0) /\
(Q2R (fst (fst (absenv (Var Q M0 v)))) <= vR <= Q2R (snd (fst (absenv (Var Q M0 v)))))%R) ->
NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
(forall v, NatSet.mem v fVars = true ->
exists vR, E v = Some vR /\
exists vR, E v = Some (vR, M0) /\
(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.
eval_exp E (toREval (toRExp f)) vR M0 ->
(Q2R (fst (fst (absenv (erasure f)))) <= vR <= Q2R (snd (fst (absenv (erasure f)))))%R.
Proof.
induction f; intros vR valid_bounds valid_definedVars usedVars_subset valid_usedVars eval_f.
- unfold validIntervalbounds in valid_bounds.
env_assert absenv (Var Q n) absenv_var.
env_assert absenv (Var Q M0 n) absenv_var.
destruct absenv_var as [ iv [err absenv_var]].
specialize (valid_usedVars n).
rewrite absenv_var in *; simpl in *.
simpl; rewrite absenv_var in *; simpl in *.
inversion eval_f; subst.
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 *.
inversion H0; subst.
inversion H4; subst.
rewrite absenv_var in *; auto.
+ repeat (rewrite delta_0_deterministic in *; try auto).
rewrite absenv_var in valid_bounds.
unfold isSupersetIntv in valid_bounds.
andb_to_prop valid_bounds.
apply Qle_bool_iff in L0;
......@@ -227,10 +240,11 @@ Proof.
rewrite in_dVars in case_mem; congruence.
* specialize (valid_usedVars in_fVars);
destruct valid_usedVars as [vR' [vR_def P_valid]].
rewrite vR_def in H0; inversion H0; subst.
rewrite vR_def in H4; inversion H4; subst.
lra.
- unfold validIntervalbounds in valid_bounds.
destruct (absenv (Const v)) as [intv err]; simpl.
simpl erasure in valid_bounds.
simpl in *; destruct (absenv (Const v)) as [intv err]; simpl in *.
apply Is_true_eq_left in valid_bounds.
apply andb_prop_elim in valid_bounds.
destruct valid_bounds as [valid_lo valid_hi].
......@@ -246,18 +260,19 @@ Proof.
unfold Qleb in *.
apply Qle_bool_iff in valid_hi.
apply Qle_Rle in valid_hi; auto.
- case_eq (absenv (Unop u f)); intros intv err absenv_unop.
+ simpl in H0; rewrite Q2R0_is_0 in H0; auto.
- case_eq (absenv (Unop u (erasure f))); intros intv err absenv_unop.
destruct intv as [unop_lo unop_hi]; simpl.
unfold validIntervalbounds in valid_bounds.
rewrite absenv_unop in valid_bounds.
case_eq (absenv f); intros intv_f err_f absenv_f.
simpl in valid_bounds; rewrite absenv_unop in valid_bounds.
case_eq (absenv (erasure f)); intros intv_f err_f absenv_f.
rewrite absenv_f in valid_bounds.
apply Is_true_eq_left in valid_bounds.
apply andb_prop_elim in valid_bounds.
destruct valid_bounds as [valid_rec valid_unop].
apply Is_true_eq_true in valid_rec.
inversion eval_f; subst.
+ specialize (IHf v1 valid_rec valid_definedVars usedVars_subset valid_usedVars H2).
+ specialize (IHf v1 valid_rec valid_definedVars usedVars_subset valid_usedVars H3).
rewrite absenv_f in IHf; simpl in IHf.
(* TODO: Make lemma *)
unfold isSupersetIntv in valid_unop.
......@@ -270,12 +285,12 @@ Proof.
apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
destruct IHf.
split.
* eapply Rle_trans. apply valid_lo.
* eapply Rle_trans. rewrite absenv_unop; simpl; apply valid_lo.
rewrite Q2R_opp; lra.
* eapply Rle_trans.
Focus 2. apply valid_hi.
Focus 2. rewrite absenv_unop; simpl; apply valid_hi.
rewrite Q2R_opp; lra.
+ specialize (IHf v1 valid_rec valid_definedVars usedVars_subset valid_usedVars H3).
+ specialize (IHf v1 valid_rec valid_definedVars usedVars_subset valid_usedVars H4).
rewrite absenv_f in IHf; simpl in IHf.
apply andb_prop_elim in valid_unop.
destruct valid_unop as [nodiv0 valid_unop].
......@@ -297,7 +312,7 @@ Proof.
destruct IHf.
rewrite delta_0_deterministic; auto.
unfold perturb; split.
{ eapply Rle_trans. apply valid_lo.
{ eapply Rle_trans. rewrite absenv_unop; simpl; apply valid_lo.
destruct nodiv0_prop as [nodiv0_neg | nodiv0_pos].
(* TODO: Extract lemma maybe *)
- assert (0 < - (Q2R (snd intv_f)))%R as negation_pos by lra.
......@@ -319,7 +334,7 @@ Proof.
apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra.
}
{ eapply Rle_trans.
Focus 2. apply valid_hi.
Focus 2. rewrite absenv_unop; simpl; apply valid_hi.
destruct nodiv0_prop as [nodiv0_neg | nodiv0_pos].
- assert (Q2R (fst intv_f) < 0)%R as fst_lt_0 by lra.
assert (0 < - (Q2R (fst intv_f)))%R as negation_pos by lra.
......@@ -343,13 +358,15 @@ Proof.
rewrite <- Q2R0_is_0 in nodiv0_pos.
apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra.
}
{ rewrite Q2R0_is_0 in H1; auto. }
- inversion eval_f; subst.
rewrite delta_0_deterministic in eval_f; auto.
rewrite delta_0_deterministic; auto.
simpl in valid_bounds.
case_eq (absenv (Binop b f1 f2)); intros iv err absenv_bin.
case_eq (absenv f1); intros iv1 err1 absenv_f1.
case_eq (absenv f2); intros iv2 err2 absenv_f2.
case_eq (absenv (Binop b (erasure f1) (erasure f2))); intros iv err absenv_bin.
case_eq (absenv (erasure f1)); intros iv1 err1 absenv_f1.
case_eq (absenv (erasure f2)); intros iv2 err2 absenv_f2.
simpl.
rewrite absenv_bin, absenv_f1, absenv_f2 in valid_bounds.
apply Is_true_eq_left in valid_bounds.
apply andb_prop_elim in valid_bounds.
......@@ -369,6 +386,7 @@ Proof.
rewrite NatSet.diff_spec in in_diff_e1.
destruct in_diff_e1 as [ in_usedVars not_dVar].
split; try auto.
assert (m1 = M0) by (apply (ifM0isJoin_l M0 m1 m2); auto); subst; auto.
+ assert (Q2R (fst (fst (iv2, err2))) <= v2 <= Q2R (snd (fst (iv2, err2))))%R as valid_bounds_e2.
* apply IHf2; try auto.
intros v in_diff_e2.
......@@ -376,6 +394,7 @@ Proof.
simpl. rewrite NatSet.diff_spec, NatSet.union_spec.
rewrite NatSet.diff_spec in in_diff_e2.
destruct in_diff_e2; split; auto.
assert (m2 = M0) by (apply (ifM0isJoin_r M0 m1 m2); auto); subst; auto.
* destruct b; simpl in *.
{ pose proof (interval_addition_valid (iv1 :=(Q2R (fst iv1),Q2R (snd iv1))) (iv2 :=(Q2R (fst iv2), Q2R (snd iv2)))) as valid_add.
unfold validIntervalAdd in valid_add.
......@@ -388,7 +407,7 @@ Proof.
apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
destruct valid_add as [valid_add_lo valid_add_hi].
split.
- eapply Rle_trans. apply valid_lo.
- eapply Rle_trans. rewrite absenv_bin; apply valid_lo.
unfold ivlo. unfold addIntv.
simpl in valid_add_lo.
repeat rewrite <- Q2R_plus in valid_add_lo.
......@@ -396,7 +415,7 @@ Proof.
unfold absIvUpd; auto.
- eapply Rle_trans.
Focus 2.
apply valid_hi.
rewrite absenv_bin; apply valid_hi.
unfold ivlo, addIntv.
simpl in valid_add_hi.
repeat rewrite <- Q2R_plus in valid_add_hi.
......@@ -412,7 +431,7 @@ Proof.
apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
destruct valid_sub as [valid_sub_lo valid_sub_hi].
split.
- eapply Rle_trans. apply valid_lo.
- eapply Rle_trans. rewrite absenv_bin; apply valid_lo.
unfold ivlo. unfold subtractIntv.
simpl in valid_sub_lo.
repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_lo.
......@@ -421,7 +440,7 @@ Proof.
unfold absIvUpd; auto.
- eapply Rle_trans.
Focus 2.
apply valid_hi.
rewrite absenv_bin; apply valid_hi.
unfold ivlo, addIntv.
simpl in valid_sub_hi.
repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_hi.
......@@ -438,7 +457,7 @@ Proof.
apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
destruct valid_mul as [valid_mul_lo valid_mul_hi].
split.
- eapply Rle_trans. apply valid_lo.
- eapply Rle_trans. rewrite absenv_bin; apply valid_lo.
unfold ivlo. unfold multIntv.
simpl in valid_mul_lo.
repeat rewrite <- Q2R_mult in valid_mul_lo.
......@@ -446,7 +465,7 @@ Proof.
unfold absIvUpd; auto.
- eapply Rle_trans.
Focus 2.
apply valid_hi.
rewrite absenv_bin; apply valid_hi.
unfold ivlo, addIntv.
simpl in valid_mul_hi.
repeat rewrite <- Q2R_mult in valid_mul_hi.
......@@ -490,7 +509,7 @@ Proof.
rewrite ivlo2_0 in H0.
lra. }
{ split.
- eapply Rle_trans. apply valid_lo.
- eapply Rle_trans. rewrite absenv_bin; apply valid_lo.
unfold ivlo. unfold multIntv.
simpl in valid_div_lo.
rewrite <- Q2R_inv in valid_div_lo; [ | auto].
......@@ -499,29 +518,48 @@ Proof.
rewrite <- Q2R_min4 in valid_div_lo; auto.
- eapply Rle_trans.
Focus 2.
apply valid_hi.
rewrite absenv_bin; 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. } }
+ simpl in H3; rewrite Q2R0_is_0 in H3; auto.
+ simpl in H3; rewrite Q2R0_is_0 in H3; auto.
- unfold validIntervalbounds in valid_bounds.
simpl erasure in valid_bounds.
simpl in *; destruct (absenv (Downcast M0 (erasure f))); destruct (absenv (erasure f)); simpl in *.
apply Is_true_eq_left in valid_bounds.
apply andb_prop_elim in valid_bounds.
destruct valid_bounds as [vI1 vI2].
apply andb_prop_elim in vI2.
destruct vI2 as [vI2 vI2'].
apply Is_true_eq_true in vI2.
apply Is_true_eq_true in vI2'.
assert (isEqIntv i i0) as Eq by (apply supIntvAntisym; auto).
destruct Eq as [Eqlo Eqhi].
simpl in *.
apply Qeq_eqR in Eqlo; rewrite Eqlo.
apply Qeq_eqR in Eqhi; rewrite Eqhi.
apply IHf; auto.
apply Is_true_eq_true in vI1; apply vI1.
Qed.
Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult):
forall E vR fVars dVars outVars elo ehi err P,
ssaPrg f (NatSet.union fVars dVars) outVars ->
bstep (toRCmd f) E 0%R vR ->
bstep (toREvalCmd (toRCmd f)) E vR M0 ->
(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) ->
E v = Some (vR, M0) /\
(Q2R (fst (fst (absenv (Var Q M0 v)))) <= vR <= Q2R (snd (fst (absenv (Var Q M0 v)))))%R) ->
(forall v, NatSet.mem v fVars = true ->
exists vR,
E v = Some vR /\
E v = Some (vR, M0) /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
NatSet.Subset (NatSet.diff (Commands.usedVars f) dVars) fVars ->
validIntervalboundsCmd f absenv P dVars = true ->
absenv (getRetExp f) = ((elo, ehi), err) ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
validIntervalboundsCmd (erasureCmd f) absenv P dVars = true ->
absenv (getRetExp (erasureCmd f)) = ((elo, ehi), err) ->
(Q2R elo <= vR <= Q2R ehi)%R.
Proof.
induction f;
......@@ -532,7 +570,7 @@ Proof.
unfold validIntervalboundsCmd in valid_bounds_f.
andb_to_prop valid_bounds_f.
inversion ssa_f; subst.
specialize (IHf (updEnv n v E) vR fVars (NatSet.add n dVars)).
specialize (IHf (updEnv n M0 v E) vR fVars (NatSet.add n dVars)).
eapply IHf; eauto.
+ assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars)) (NatSet.union fVars (NatSet.add n dVars))).
* hnf. intros a; split; intros in_set.
......@@ -565,10 +603,9 @@ Proof.
destruct in_usedVars as [ in_usedVars not_dVar].
repeat split; try auto.
{ hnf; intros; subst.
apply validVars_subset_usedVars in H2.
specialize (H2 n in_usedVars).
rewrite <- NatSet.mem_spec in H2.
rewrite H2 in H5; congruence. }
specialize (H5 n in_usedVars).
rewrite <- NatSet.mem_spec in H5.
rewrite H5 in H6; congruence. }
* apply dVars_sound. rewrite NatSet.mem_spec.
rewrite NatSet.mem_spec in mem_v0.
rewrite NatSet.add_spec in mem_v0.
......@@ -599,7 +636,7 @@ Proof.
- unfold validIntervalboundsCmd in valid_bounds_f.
inversion eval_f; subst.
unfold updEnv.
assert (Q2R (fst (fst (absenv e))) <= vR <= Q2R (snd (fst (absenv e))))%R.
+ eapply validIntervalbounds_sound; eauto.
assert (Q2R (fst (fst (absenv (erasure e)))) <= vR <= Q2R (snd (fst (absenv (erasure e)))))%R.
+ simpl in valid_bounds_f; eapply validIntervalbounds_sound; eauto.
+ simpl in *. rewrite absenv_f in *; auto.
Qed.
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