Skip to content

GitLab

Commit 92da81e9 authored by Heiko Becker's avatar Heiko Becker
Browse files
Options

Port Error validator to finite maps, some proof simplification in interval validator

parent 41b255c9
Hide whitespace changes
Inline Side-by-side
Showing with 138 additions and 117 deletions
coq/ErrorValidation.v
View file @ 92da81e9
......@@ -6,23 +6,21 @@
encoded in the analysis result. The validator is used in the file
CertificateChecker.v to build the complete checker.
**)
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs
Coq.QArith.Qreals Coq.micromega.Psatz Coq.Reals.Reals.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps
Daisy.Infra.RealRationalProps Daisy.Infra.RealSimps
Daisy.Infra.Ltacs Daisy.Environments
Daisy.IntervalValidation Daisy.Typing Daisy.ErrorBounds.
From Coq
Require Import QArith.QArith QArith.Qminmax QArith.Qabs QArith.Qreals
micromega.Psatz Reals.Reals.
From Daisy
Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
Infra.RealSimps Infra.Ltacs Environments IntervalValidation Typing
ErrorBounds.
(** Error bound validator **)
Fixpoint validErrorbound (e:exp Q) (* analyzed expression *)
(typeMap:exp Q -> option mType) (* derived types for e *)
(typeMap:DaisyMap.t mType) (* derived types for e *)
(A:analysisResult) (* encoded result of Daisy *)
(dVars:NatSet.t) (* let-bound variables encountered previously *):=
let (intv, err) := (A e) in
let mopt := typeMap e in
match mopt with
| None => false
| Some m =>
match DaisyMap.find e A, DaisyMap.find e typeMap with
| Some (intv, err), Some m =>
if (Qleb 0 err) (* encoding soundness: errors are positive *)
then
match e with (* case analysis for the expression *)
......@@ -34,60 +32,74 @@ Fixpoint validErrorbound (e:exp Q) (* analyzed expression *)
Qleb (maxAbs intv * (mTypeToQ m)) err
|Unop Neg e1 =>
if (validErrorbound e1 typeMap A dVars)
then Qeq_bool err (snd (A e1))
then
match DaisyMap.find e1 A with
| Some (iv_e1, err1) => Qeq_bool err err1
| None => false
end
else false
|Unop Inv e1 => false
|Binop b e1 e2 =>
if ((validErrorbound e1 typeMap A dVars)
&& (validErrorbound e2 typeMap A dVars))
then
let (ive1, err1) := A e1 in
let (ive2, err2) := A e2 in
let errIve1 := widenIntv ive1 err1 in
let errIve2 := widenIntv ive2 err2 in
let upperBoundE1 := maxAbs ive1 in
let upperBoundE2 := maxAbs ive2 in
match b with
| Plus =>
Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * (mTypeToQ m)) err
| Sub =>
Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * (mTypeToQ m)) err
| Mult =>
Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multIntv errIve1 errIve2)) * (mTypeToQ m)) err
| Div =>
if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) ||
((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0))))
then
let upperBoundInvE2 := maxAbs (invertIntv ive2) in
let minAbsIve2 := minAbs (errIve2) in
let errInv := (1 / (minAbsIve2 * minAbsIve2)) * err2 in
Qleb ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideIntv errIve1 errIve2)) * (mTypeToQ m)) err
else false
match DaisyMap.find e1 A, DaisyMap.find e2 A with
| Some (ive1, err1), Some (ive2, err2) =>
let errIve1 := widenIntv ive1 err1 in
let errIve2 := widenIntv ive2 err2 in
let upperBoundE1 := maxAbs ive1 in
let upperBoundE2 := maxAbs ive2 in
match b with
| Plus =>
Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * (mTypeToQ m)) err
| Sub =>
Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * (mTypeToQ m)) err
| Mult =>
Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multIntv errIve1 errIve2)) * (mTypeToQ m)) err
| Div =>
if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) ||
((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0))))
then
let upperBoundInvE2 := maxAbs (invertIntv ive2) in
let minAbsIve2 := minAbs (errIve2) in
let errInv := (1 / (minAbsIve2 * minAbsIve2)) * err2 in
Qleb ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideIntv errIve1 errIve2)) * (mTypeToQ m)) err
else false
end
| _, _ => false
end
else false
|Downcast m1 e1 =>
if validErrorbound e1 typeMap A dVars
then
let (ive1, err1) := A e1 in
let errIve1 := widenIntv ive1 err1 in
(Qleb (err1 + maxAbs errIve1 * (mTypeToQ m1)) err)
match DaisyMap.find e1 A with
| Some (ive1, err1) =>
let errIve1 := widenIntv ive1 err1 in
(Qleb (err1 + maxAbs errIve1 * (mTypeToQ m1)) err)
| None => false
end
else
false
end
else false
| _, _ => false
end.
(** Error bound command validator **)
Fixpoint validErrorboundCmd (f:cmd Q) (* analyzed cmd with let's *)
(typeMap:exp Q -> option mType) (* inferred types *)
typeMap (* inferred types *)
(A:analysisResult) (* Daisy's encoded result *)
(dVars:NatSet.t) (* defined variables *)
: bool :=
match f with
|Let m x e g =>
if ((validErrorbound e typeMap A dVars) && (Qeq_bool (snd (A e)) (snd (A (Var Q x)))))
then validErrorboundCmd g typeMap A (NatSet.add x dVars)
else false
match DaisyMap.find e A, DaisyMap.find (Var Q x) A with
| Some (iv_e, err_e), Some (iv_x, err_x) =>
if ((validErrorbound e typeMap A dVars) && (Qeq_bool err_e err_x))
then validErrorboundCmd g typeMap A (NatSet.add x dVars)
else false
| _,_ => false
end
|Ret e => validErrorbound e typeMap A dVars
end.
......
coq/Infra/Ltacs.v
View file @ 92da81e9
......@@ -91,6 +91,15 @@ Ltac match_simpl :=
repeat match_factorize;
try pair_factorize.
Ltac bool_factorize :=
match goal with
| [H: _ = true |- _] => andb_to_prop H
end.
Ltac Daisy_compute :=
repeat
(match_simpl || bool_factorize).
(* Ltac destruct_if := *)
(* match goal with *)
(* | [H: if ?c then ?a else ?b = _ |- _ ] => *)
......
coq/IntervalValidation.v
View file @ 92da81e9
......@@ -105,22 +105,20 @@ Theorem ivbounds_approximatesPrecond_sound f A P dVars iv err:
Proof.
induction f; cbn; intros approx_true var var_in_fV find_A; set_tac.
- subst.
match_simpl.
Daisy_compute.
destruct (var mem dVars) eqn:?; set_tac; try congruence.
andb_to_prop approx_true; unfold isSupersetIntv.
Daisy_compute.
unfold isSupersetIntv.
apply andb_prop_intro; split;
apply Is_true_eq_left; auto.
- match_simpl.
andb_to_prop approx_true.
- Daisy_compute; try congruence.
apply IHf; try auto.
set_tac.
- match_simpl.
andb_to_prop approx_true.
- Daisy_compute; try congruence.
destruct H.
+ apply IHf1; try auto; set_tac.
+ apply IHf2; try auto; set_tac.
- match_simpl.
andb_to_prop approx_true.
- Daisy_compute; try congruence.
apply IHf; try auto; set_tac.
Qed.
......@@ -142,20 +140,16 @@ Lemma validBoundsDiv_uneq_zero e1 e2 A P V ivlo_e2 ivhi_e2 err:
(ivhi_e2 < 0) \/ (0 < ivlo_e2).
Proof.
intros A_eq validBounds; cbn in *.
match_simpl.
andb_to_prop validBounds.
repeat match_simpl.
andb_to_prop R.
unfold isSupersetIntv in *; simpl in *.
Daisy_compute; try congruence.
apply le_neq_bool_to_lt_prop; auto.
Qed.
Definition dVars_range_valid (dVars:NatSet.t) (E:env) (A:analysisResult) :Prop :=
forall v, NatSet.In v dVars ->
exists vR ivlo ivhi err,
exists vR iv err,
E v = Some vR /\
DaisyMap.find (Var Q v) A = Some ((ivlo, ivhi), err) /\
(Q2R ivlo <= vR <= Q2R ivhi)%R.
DaisyMap.find (Var Q v) A = Some (iv, err) /\
(Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
Definition fVars_P_sound (fVars:NatSet.t) (E:env) (P:precond) :Prop :=
forall v,
......@@ -167,6 +161,11 @@ Definition vars_typed (S:NatSet.t) (Gamma: nat -> option mType) :=
forall v, NatSet.In v S ->
exists m :mType, Gamma v = Some m.
Ltac kill_trivial_exists :=
match goal with
| [ |- exists iv err v, Some (?i,?e) = Some (iv, err) /\ _ /\ _] => exists i, e
end.
Theorem validIntervalbounds_sound (f:exp Q) (A:analysisResult) (P:precond)
fVars dVars (E:env) Gamma:
validIntervalbounds f A P dVars = true ->
......@@ -174,22 +173,23 @@ Theorem validIntervalbounds_sound (f:exp Q) (A:analysisResult) (P:precond)
NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
fVars_P_sound fVars E P ->
vars_typed (NatSet.union fVars dVars) Gamma ->
exists ivlo ivhi err vR,
DaisyMap.find f A = Some ((ivlo, ivhi), err) /\
exists iv err vR,
DaisyMap.find f A = Some (iv, err) /\
eval_exp E (toRMap Gamma) (toREval (toRExp f)) vR M0 /\
(Q2R ivlo <= vR <= Q2R ivhi)%R.
(Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
Proof.
induction f;
intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined;
cbn in *.
- match_simpl.
- Daisy_compute.
destruct (NatSet.mem n dVars) eqn:?; simpl in *.
+ destruct (valid_definedVars n)
as [vR [ivlo_n [ivhi_n [err_n [env_valid [map_n bounds_valid]]]]]];
as [vR [iv_n [err_n [env_valid [map_n bounds_valid]]]]];
try set_tac.
rewrite map_n in *.
inversion Heqo; subst.
exists ivlo_n, ivhi_n, e; eexists; split; [auto| split; try eauto ].
kill_trivial_exists.
eexists; split; [auto| split; try eauto ].
eapply Var_load; simpl; try auto.
destruct (types_defined n) as [m type_m];
set_tac.
......@@ -199,43 +199,42 @@ Proof.
assert (NatSet.In n fVars) by set_tac.
andb_to_prop valid_bounds.
canonize_hyps; simpl in *.
exists (fst i), (snd i), e; eexists; split;
[destruct i; auto | split].
kill_trivial_exists.
eexists; split; [auto | split].
* econstructor; try eauto.
destruct (types_defined n) as [m type_m]; set_tac.
destruct (types_defined n) as [m type_m];
set_tac.
match_simpl; auto.
* lra.
- match_simpl.
andb_to_prop valid_bounds.
canonize_hyps; simpl in *.
exists (fst i), (snd i), e, (perturb (Q2R v) 0).
split; [destruct i; auto| split].
- Daisy_compute; canonize_hyps; simpl in *.
kill_trivial_exists.
exists (perturb (Q2R v) 0).
split; [auto| split].
+ econstructor; try eauto. apply Rabs_0_equiv.
+ unfold perturb; simpl; lra.
- match_simpl.
andb_to_prop valid_bounds.
match_simpl.
destruct IHf as [ivlo_f [ivhi_f [err_f [vF [iveq_f [eval_f valid_bounds_f]]]]]];
- Daisy_compute; simpl in *; try congruence.
destruct IHf as [iv_f [err_f [vF [iveq_f [eval_f valid_bounds_f]]]]];
try auto.
destruct u; try andb_to_prop R.
+ exists (fst i), (snd i), e, (evalUnop Neg vF); split;
[destruct i; auto | split ;
inversion iveq_f; subst.
destruct u; try andb_to_prop R; simpl in *.
+ kill_trivial_exists.
exists (evalUnop Neg vF); split;
[auto | split ;
[econstructor; eauto | ]].
canonize_hyps; simpl in *.
canonize_hyps.
rewrite Q2R_opp in *.
destruct valid_bounds_f.
inversion iveq_f; subst; simpl in *; lra.
+ inversion iveq_f; subst; simpl in *.
rename L0 into nodiv0.
simpl; lra.
+ rename L0 into nodiv0.
apply le_neq_bool_to_lt_prop in nodiv0.
exists (fst i), (snd i), e, (perturb (evalUnop Inv vF) 0); split;
kill_trivial_exists.
exists (perturb (evalUnop Inv vF) 0); split;
[destruct i; auto | split].
* econstructor; eauto; try apply Rabs_0_equiv.
(* Absence of division by zero *)
hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0;
rewrite Q2R0_is_0 in nodiv0; lra.
* canonize_hyps.
pose proof (interval_inversion_valid ((Q2R ivlo_f),(Q2R ivhi_f)) (a :=vF)) as inv_valid.
pose proof (interval_inversion_valid ((Q2R (fst iv_f)),(Q2R (snd iv_f))) (a :=vF)) as inv_valid.
unfold invertInterval in inv_valid; simpl in *.
rewrite delta_0_deterministic; [| rewrite Rbasic_fun.Rabs_R0; lra].
destruct inv_valid; try auto.
......@@ -245,7 +244,7 @@ Proof.
- rewrite Q2R_inv; try auto.
destruct nodiv0; try lra.
hnf; intros.
assert (0 < Q2R (ivhi_f))%R.
assert (0 < Q2R (snd iv_f))%R.
{ eapply Rlt_le_trans.
apply Qlt_Rlt in H1.
rewrite <- Q2R0_is_0.
......@@ -258,7 +257,7 @@ Proof.
- rewrite <- Q2R_inv; try auto.
hnf; intros.
destruct nodiv0; try lra.
assert (Q2R ivlo_f < 0)%R.
assert (Q2R (fst iv_f) < 0)%R.
{ eapply Rle_lt_trans.
Focus 2.
rewrite <- Q2R0_is_0;
......@@ -267,23 +266,23 @@ Proof.
}
rewrite <- Q2R0_is_0 in H3.
apply Rlt_Qlt in H3. lra. }
- match_simpl.
andb_to_prop valid_bounds.
repeat match_simpl.
destruct IHf1 as [ivlo_f1 [ivhi_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]]];
- Daisy_compute; try congruence.
destruct IHf1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]];
try auto; set_tac.
destruct IHf2 as [ivlo_f2 [ivhi_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]]];
destruct IHf2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]];
try auto; set_tac.
assert (M0 = join M0 M0) as M0_join by (cbv; auto);
rewrite M0_join.
exists (fst i), (snd i), e, (perturb (evalBinop b vF1 vF2) 0);
kill_trivial_exists.
exists (perturb (evalBinop b vF1 vF2) 0);
split; [destruct i; auto | ].
inversion env1; inversion env2; subst.
destruct b; simpl in *.
* split;
[econstructor; try congruence; apply Rabs_0_equiv | ].
pose proof (interval_addition_valid ((Q2R ivlo_f1), Q2R ivhi_f1)
(Q2R ivlo_f2, Q2R ivhi_f2)) as valid_add.
pose proof (interval_addition_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
(Q2R (fst iv_f2), Q2R (snd iv_f2)))
as valid_add.
specialize (valid_add vF1 vF2 valid_f1 valid_f2).
unfold isSupersetIntv in R.
andb_to_prop R.
......@@ -293,8 +292,8 @@ Proof.
unfold perturb. lra.
* split;
[econstructor; try congruence; apply Rabs_0_equiv |].
pose proof (interval_subtraction_valid (Q2R ivlo_f1, Q2R ivhi_f1)
(Q2R ivlo_f2, Q2R ivhi_f2))
pose proof (interval_subtraction_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
(Q2R (fst iv_f2), Q2R (snd iv_f2)))
as valid_sub.
specialize (valid_sub vF1 vF2 valid_f1 valid_f2).
unfold isSupersetIntv in R.
......@@ -306,8 +305,8 @@ Proof.
unfold perturb; lra.
* split;
[ econstructor; try congruence; apply Rabs_0_equiv |].
pose proof (interval_multiplication_valid (Q2R ivlo_f1, Q2R ivhi_f1)
(Q2R ivlo_f2, Q2R ivhi_f2))
pose proof (interval_multiplication_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
(Q2R (fst iv_f2), Q2R (snd iv_f2)))
as valid_mul.
specialize (valid_mul vF1 vF2 valid_f1 valid_f2).
unfold isSupersetIntv in R.
......@@ -325,19 +324,19 @@ Proof.
{ hnf; intros.
destruct L as [L | L]; apply Qlt_Rlt in L; rewrite Q2R0_is_0 in L; lra. }
{ pose proof (interval_division_valid (a:=vF1) (b:=vF2)
(Q2R ivlo_f1, Q2R ivhi_f1)
(Q2R ivlo_f2, Q2R ivhi_f2))
((Q2R (fst iv_f1)), Q2R (snd iv_f1))
(Q2R (fst iv_f2), Q2R (snd iv_f2)))
as valid_div.
simpl in *.
destruct valid_div; try auto.
- destruct L; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto.
- assert (~ ivhi_f2 == 0).
- assert (~ (snd iv_f2) == 0).
{ hnf; intros. destruct L; try lra.
assert (0 < ivhi_f2) by (apply Rlt_Qlt; apply Qlt_Rlt in H2; lra).
assert (0 < (snd iv_f2)) by (apply Rlt_Qlt; apply Qlt_Rlt in H2; lra).
lra. }
assert (~ ivlo_f2 == 0).
assert (~ (fst iv_f2) == 0).
{ hnf; intros; destruct L; try lra.
assert (ivlo_f2 < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H3; lra).
assert ((fst iv_f2) < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H3; lra).
lra. }
repeat (rewrite <- Q2R_inv in *; try auto).
repeat rewrite <- Q2R_mult in *.
......@@ -348,10 +347,11 @@ Proof.
- match_simpl.
andb_to_prop valid_bounds.
match_simpl.
destruct IHf as [ivlo_f [ivhi_f [err_f [vF [env_f [eval_f valid_f]]]]]];
destruct IHf as [iv_f [err_f [vF [env_f [eval_f valid_f]]]]];
try auto.
inversion env_f; subst.
exists (fst i), (snd i), e, (perturb vF 0).
kill_trivial_exists.
exists (perturb vF 0).
split; [destruct i; try auto |].
split; [try econstructor; try eauto; try apply Rabs_0_equiv; unfold isMorePrecise; auto |].
unfold isSupersetIntv in *; andb_to_prop R.
......@@ -407,20 +407,20 @@ Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult) Gamma:
vars_typed (NatSet.union fVars dVars) Gamma ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
validIntervalboundsCmd f A P dVars = true ->
exists elo ehi err vR,
DaisyMap.find (getRetExp f) A = Some ((elo, ehi), err) /\
exists iv_e err_e vR,
DaisyMap.find (getRetExp f) A = Some (iv_e, err_e) /\
bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR M0 /\
(Q2R elo <= vR <= Q2R ehi)%R.
(Q2R (fst iv_e) <= vR <= Q2R (snd iv_e))%R.
Proof.
revert Gamma.
induction f;
intros * ssa_f dVars_sound fVars_valid types_valid usedVars_subset valid_bounds_f;
cbn in *.
- repeat match_simpl. andb_to_prop valid_bounds_f.
- Daisy_compute.
inversion ssa_f; subst.
canonize_hyps.
pose proof (validIntervalbounds_sound e (Gamma:=Gamma) (E:=E) (fVars:=fVars) L) as validIV_e.
destruct validIV_e as [v_lo [v_hi [err_v [v [find_v [eval_e valid_bounds_e]]]]]];
destruct validIV_e as [iv_e [err_v [v [find_v [eval_e valid_bounds_e]]]]];
try auto.
{ set_tac. repeat split; auto.
hnf; intros; subst.
......@@ -433,7 +433,7 @@ Proof.
destruct H0; auto.
* destruct in_set as [? | ?]; try auto; set_tac.
destruct H as [? | [? ?]]; auto.
+ edestruct IHf as [ivlo_f [ivhi_f [err_f [vR [env_f [eval_f valid_bounds_f]]]]]];
+ edestruct IHf as [iv_f [err_f [vR [env_f [eval_f valid_bounds_f]]]]];
try eauto.
eapply ssa_equal_set. symmetry in H. apply H. apply H7.
* intros v0 mem_v0.
......@@ -442,7 +442,7 @@ Proof.
{ rename R1 into eq_lo;
rename R0 into eq_hi.
rewrite Nat.eqb_eq in v0_eq; subst.
exists v; eexists; eexists; eexists; repeat split; try eauto; lra. }
exists v; eexists; eexists; repeat split; try eauto; simpl in *; lra. }
{ apply dVars_sound.
set_tac.
destruct mem_v0 as [? | [? ?]]; try auto.
......@@ -486,12 +486,12 @@ Proof.
{ hnf; intros a_dVar.
apply a_no_dVar.
rewrite NatSet.add_spec; auto. }
* simpl. exists ivlo_f, ivhi_f, err_f, vR; repeat split; try auto; try lra.
* simpl. exists iv_f, err_f, vR; repeat split; try auto; try lra.
econstructor; try eauto.
eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n M0 Gamma)) ; try eauto.
intros n1; erewrite Rmap_updVars_comm; eauto.
- unfold validIntervalboundsCmd in valid_bounds_f.
pose proof (validIntervalbounds_sound e (E:=E) (Gamma:=Gamma) valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e.
destruct valid_iv_e as [?[?[?[? [? [? ?]]]]]]; try auto.
destruct valid_iv_e as [?[?[? [? [? ?]]]]]; try auto.
simpl in *. repeat eexists; repeat split; try eauto; [econstructor; eauto| | ]; lra.
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