Commit fcc58289 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Prove soundness of interval validation for FMAs

parent be477b4d
......@@ -65,6 +65,28 @@ Fixpoint validErrorbound (e:exp Q) (* analyzed expression *)
else false
end
else false
| Fma e1 e2 e3 =>
if ((validErrorbound e1 typeMap A dVars)
&& (validErrorbound e2 typeMap A dVars)
&& (validErrorbound e3 typeMap A dVars))
then
let (ive1, err1) := A e1 in
let (ive2, err2) := A e2 in
let (ive3, err3) := A e3 in
let errIve1 := widenIntv ive1 err1 in
let errIve2 := widenIntv ive2 err2 in
let errIve3 := widenIntv ive3 err3 in
let upperBoundE1 := maxAbs ive1 in
let upperBoundE2 := maxAbs ive2 in
let upperBoundE3 := maxAbs ive3 in
Qleb (err1 + (err2 * err3)) err
(* match b with *)
(* | Plus => *)
(* Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * (mTypeToQ m)) err *)
(* | Mult => *)
(* Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multIntv errIve1 errIve2)) * (mTypeToQ m)) err *)
(* end *)
else false
|Downcast m1 e1 =>
if validErrorbound e1 typeMap A dVars
then
......@@ -2148,6 +2170,7 @@ Proof.
{ simpl; rewrite absenv_eq, type_b, L, L2, R1; simpl.
rewrite absenv_e1, absenv_e2; auto. }
{ andb_to_prop R; auto. }
- admit.
- destruct (absenv e) as [[ivlo_e ivhi_e] err_e] eqn: absenv_e.
subst; simpl in *.
rewrite absenv_eq, absenv_e in *.
......@@ -2194,7 +2217,7 @@ Proof.
rewrite L0; auto.
Unshelve.
intros. auto.
Qed.
Admitted.
Theorem validErrorboundCmd_gives_eval (f:cmd Q) :
forall (absenv:analysisResult) E1 E2 outVars fVars dVars vR elo ehi err P Gamma defVars,
......@@ -2451,4 +2474,4 @@ Proof.
unfold validErrorboundCmd in valid_bounds.
simpl in *.
edestruct validErrorbound_sound as [[* [* eval_e]] bounded_e]; eauto.
Qed.
\ No newline at end of file
Qed.
......@@ -354,4 +354,4 @@ Proof.
assert (Rabs b = - b)%R as Rabs_neg_b by (apply Rabs_left; lra).
rewrite Rabs_neg_a, Rabs_neg_b.
rewrite Rmin_right; lra.
Qed.
\ No newline at end of file
Qed.
......@@ -60,6 +60,17 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) (vali
else false
end
else false
| Fma f1 f2 f3 =>
if ((validIntervalbounds f1 absenv P validVars) &&
(validIntervalbounds f2 absenv P validVars) &&
(validIntervalbounds f3 absenv P validVars))
then
let (iv1,_) := absenv f1 in
let (iv2,_) := absenv f2 in
let (iv3,_) := absenv f3 in
let new_iv := addIntv iv1 (multIntv iv2 iv3) in
isSupersetIntv new_iv intv
else false
| Downcast _ f1 =>
if (validIntervalbounds f1 absenv P validVars)
then
......@@ -129,6 +140,31 @@ Proof.
+ apply IHf2; try auto.
* apply Is_true_eq_true; auto.
* rewrite NatSet.diff_spec; split; auto.
- intros approx_fma_true v v_in_fV.
simpl in v_in_fV.
rewrite NatSet.diff_spec in v_in_fV.
destruct v_in_fV as [ v_in_fV v_not_in_V].
repeat rewrite NatSet.union_spec in v_in_fV.
apply Is_true_eq_left in approx_fma_true.
destruct (absenv (Fma f1 f2 f3)); destruct (absenv f1);
destruct (absenv f2); destruct (absenv f3); simpl in *.
apply andb_prop_elim in approx_fma_true.
destruct approx_fma_true.
apply andb_prop_elim in H.
destruct H.
apply andb_prop_elim in H.
destruct H.
destruct v_in_fV.
+ apply IHf1; try auto.
* apply Is_true_eq_true; auto.
* rewrite NatSet.diff_spec; split; auto.
+ destruct H3.
* apply IHf2; try auto.
** apply Is_true_eq_true; auto.
** rewrite NatSet.diff_spec; split; auto.
* apply IHf3; try auto.
** apply Is_true_eq_true; auto.
** rewrite NatSet.diff_spec; split; auto.
- intros approx_rnd_true v v_in_fV.
simpl in *; destruct (absenv (Downcast m f)); destruct (absenv f).
apply Is_true_eq_left in approx_rnd_true.
......@@ -150,10 +186,24 @@ Proof.
unfold IntervalArith.min4, min4; repeat rewrite Q2R_min; auto.
Qed.
(**
Technical definition to help prove soundess for FMA
**)
Definition multIntv (iv1:intv) (iv2:intv) :=
(
min4 (Q2R ((fst iv1) * (fst iv2)))
(Q2R ((fst iv1) * (snd iv2)))
(Q2R ((snd iv1) * (fst iv2)))
(Q2R ((snd iv1) * (snd iv2))),
max4 (Q2R ((fst iv1) * (fst iv2)))
(Q2R ((fst iv1) * (snd iv2)))
(Q2R ((snd iv1) * (fst iv2)))
(Q2R ((snd iv1) * (snd iv2)))
).
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 V ivlo_e2 ivhi_e2 err:
absenv e2 = ((ivlo_e2,ivhi_e2), err) ->
validIntervalbounds (Binop Div e1 e2) absenv P V = true ->
......@@ -356,6 +406,42 @@ Proof.
unfold perturb.
lra.
}
- env_assert absenv (Fma f1 f2 f3) absenv_fma;
destruct absenv_fma as [iv_fma [err_fma absenv_fma]].
env_assert absenv f1 absenv_f1;
destruct absenv_f1 as [iv_f1 [err_f1 absenv_f1]].
env_assert absenv f2 absenv_f2;
destruct absenv_f2 as [iv_f2 [err_f2 absenv_f2]].
env_assert absenv f3 absenv_f3;
destruct absenv_f3 as [iv_f3 [err_f3 absenv_f3]].
rewrite absenv_fma in *; simpl in *.
andb_to_prop valid_bounds.
destruct IHf1 as [vF1 [eval_f1 valid_f1]]; try auto; set_tac.
destruct IHf2 as [vF2 [eval_f2 valid_f2]]; try auto; set_tac.
destruct IHf3 as [vF3 [eval_f3 valid_f3]]; try auto; set_tac.
rewrite absenv_f1, absenv_f2, absenv_f3 in *; simpl in *.
assert (M0 = join3 M0 M0 M0) as M0_join by (cbv; auto);
rewrite M0_join.
exists (perturb (evalFma vF1 vF2 vF3) 0); split.
* econstructor; try congruence. apply Rabs_0_equiv.
* pose proof (interval_multiplication_valid (Q2R (fst iv_f2),Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as valid_mul.
specialize (valid_mul vF2 vF3 valid_f2 valid_f3).
remember (multIntv iv_f2 iv_f3) as iv_f23prod.
pose proof (interval_addition_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (fst iv_f23prod, snd iv_f23prod)) as valid_add.
rewrite Heqiv_f23prod in valid_add.
unfold multIntv in valid_add.
unfold isSupersetIntv in R.
andb_to_prop R.
canonize_hyps.
simpl in *.
repeat rewrite <- Q2R_mult in *;
repeat rewrite <- Q2R_min4, <- Q2R_max4 in *;
repeat rewrite <- Q2R_plus in *;
repeat rewrite <- Q2R_min4, <- Q2R_max4 in *.
specialize (valid_add vF1 (vF2 * vF3)%R valid_f1 valid_mul).
unfold evalFma.
unfold perturb.
lra.
- env_assert absenv (Downcast m f) absenv_d;
destruct absenv_d as [iv_d [err_d absenv_d]];
env_assert absenv f absenv_f;
......@@ -540,4 +626,4 @@ Proof.
destruct valid_iv_e as [vR [eval_e valid_e]]; try auto.
simpl in *; rewrite absenv_f in *; simpl in *.
exists vR; split; [econstructor; eauto | auto].
Qed.
\ No newline at end of file
Qed.
......@@ -12,7 +12,15 @@ Fixpoint typeExpression (V:Type) (Gamma:nat -> option mType) (e:exp V) : option
let tm2 := typeExpression Gamma e2 in
match tm1, tm2 with
| Some m1, Some m2 => Some (join m1 m2)
| _, _=> None
| _, _ => None
end
| Fma e1 e2 e3 =>
let tm1 := typeExpression Gamma e1 in
let tm2 := typeExpression Gamma e2 in
let tm3 := typeExpression Gamma e3 in
match tm1, tm2, tm3 with
| Some m1, Some m2, Some m3 => Some (join3 m1 m2 m3)
| _, _,_ => None
end
| Downcast m e1 =>
let tm1 := typeExpression Gamma e1 in
......@@ -35,6 +43,16 @@ Fixpoint typeMap (Gamma:nat -> option mType) (e:exp Q) (e': exp Q) : option mTyp
| None, Some m2 => Some m2
| None, None => None
end
| Fma e1 e2 e3 => if expEq e e' then typeExpression Gamma e
else
match (typeMap Gamma e1 e'), (typeMap Gamma e2 e'), (typeMap Gamma e2 e') with
| Some m1, Some m2, Some m3 =>
if (mTypeEq m1 m2) && (mTypeEq m2 m3) then Some m1 else None
| Some m1, None, None => Some m1
| None, Some m2, None => Some m2
| None, None, Some m3 => Some m3
| _, _, _ => None
end
| Downcast m e1 => if expEq e e' then typeExpression Gamma (Downcast m e1) else typeMap Gamma e1 e'
end.
......@@ -87,10 +105,18 @@ Fixpoint typeCheck (e:exp Q) (Gamma:nat -> option mType) (tMap: exp Q -> option
| Binop b e1 e2 => match tMap e, tMap e1, tMap e2 with
| Some m, Some m1, Some m2 =>
mTypeEq m (join m1 m2)
&& typeCheck e1 Gamma tMap
&& typeCheck e2 Gamma tMap
&& typeCheck e1 Gamma tMap
&& typeCheck e2 Gamma tMap
| _, _, _ => false
end
| Fma e1 e2 e3 => match tMap e, tMap e1, tMap e2, tMap e3 with
| Some m, Some m1, Some m2, Some m3 =>
mTypeEq m (join3 m1 m2 m3)
&& typeCheck e1 Gamma tMap
&& typeCheck e2 Gamma tMap
&& typeCheck e3 Gamma tMap
| _, _, _, _ => false
end
| Downcast m e1 => match tMap e, tMap e1 with
| Some m', Some m1 => mTypeEq m m' && isMorePrecise m1 m && typeCheck e1 Gamma tMap
| _, _ => false
......@@ -237,6 +263,19 @@ Proof.
assert (expTypes e2 = Some m2) by (eapply IHe2; eauto).
rewrite H0 in H4. rewrite H1 in H5.
inversion H4; inversion H5; subst; auto.
- inversion evals; subst.
simpl in typechecks.
case_eq (expTypes (Fma e1 e2 e3)); intros; rewrite H in typechecks; [ | inversion typechecks ].
case_eq (expTypes e1); intros; rewrite H0 in typechecks; [ | inversion typechecks ].
case_eq (expTypes e2); intros; rewrite H1 in typechecks; [ | inversion typechecks ].
case_eq (expTypes e3); intros; rewrite H4 in typechecks; [ | inversion typechecks ].
andb_to_prop typechecks.
apply mTypeEq_compat_eq in L; subst.
assert (expTypes e1 = Some m1) by (eapply IHe1; eauto).
assert (expTypes e2 = Some m2) by (eapply IHe2; eauto).
assert (expTypes e3 = Some m3) by (eapply IHe3; eauto).
rewrite H0 in H5; rewrite H1 in H8; rewrite H4 in H9.
now inversion H5; inversion H8; inversion H9.
- simpl in typechecks.
case_eq (expTypes (Downcast m e)); intros; rewrite H in typechecks; [ | inversion typechecks ].
case_eq (expTypes e); intros; rewrite H0 in typechecks; [ | inversion typechecks ].
......@@ -267,4 +306,4 @@ Proof.
- simpl in *.
inversion bc; subst.
eapply typingSoundnessExp; eauto.
Qed.
\ No newline at end of file
Qed.
......@@ -35,6 +35,10 @@ Proof.
hnf; intros.
apply in_vars.
rewrite NatSet.union_spec; auto.
- intros vars_fma.
simpl in *.
intros a used_vars.
firstorder.
Qed.
(*
......@@ -588,4 +592,4 @@ Fixpoint exp_subst (e:exp Q) x e_new :=
(* induction ssa_f; *)
(* intros VarEnv ParamEnv P eps fVars_live. *)
(* - *)
(* *) *)
\ 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