Skip to content

GitLab

Commit 313ac660 authored by Heiko Becker's avatar Heiko Becker
Browse files
Options

Fix Fixed-Point implementation by properly implementing type join for fixed-points

parent c6efd235
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1773 additions and 941 deletions
coq/AffineValidation.v
View file @ 313ac660
......@@ -57,8 +57,8 @@ Proof.
destruct e5.
+ apply Ndec.Pcompare_Peqb in e8.
congruence.
+ apply Ndec.Pcompare_Peqb in Heq.
congruence.
+ apply Nat.compare_eq in Heq; subst.
rewrite Nat.eqb_refl in H; congruence.
Qed.
Lemma usedVars_toREval_toRExp_compat e:
......@@ -69,10 +69,10 @@ Proof.
- now rewrite IHe1, IHe2, IHe3.
Qed.
Lemma validRanges_eq_compat (e1: expr Q) e2 A E Gamma:
Lemma validRanges_eq_compat (e1: expr Q) e2 A E Gamma fBits:
Q_orderedExps.eq e1 e2 ->
validRanges e1 A E Gamma ->
validRanges e2 A E Gamma.
validRanges e1 A E Gamma fBits ->
validRanges e2 A E Gamma fBits.
Proof.
intros Heq.
unfold Q_orderedExps.eq in Heq.
......@@ -104,8 +104,8 @@ Proof.
destruct e3.
+ apply Ndec.Pcompare_Peqb in e6.
congruence.
+ apply Ndec.Pcompare_Peqb in Heq.
congruence.
+ apply Nat.compare_eq in Heq; subst.
rewrite Nat.eqb_refl in H; congruence.
- intros valid1; destruct valid1 as [validsub1 validr1].
specialize (IHc Heq validsub1).
split; auto.
......@@ -229,8 +229,8 @@ Proof.
destruct e5.
+ apply Ndec.Pcompare_Peqb in e8.
congruence.
+ apply Ndec.Pcompare_Peqb in Heq.
congruence.
+ apply Nat.compare_eq in Heq; subst.
rewrite Nat.eqb_refl in *; congruence.
Qed.
Definition updateExpMapIncr e new_af noise (emap: expressionsAffine) intv incr :=
......@@ -745,15 +745,15 @@ Proof.
congruence.
Qed.
Lemma validAffineBounds_validRanges e (A: analysisResult) E Gamma:
Lemma validAffineBounds_validRanges e (A: analysisResult) E Gamma fBits:
(exists map af vR aiv aerr,
FloverMap.find e A = Some (aiv, aerr) /\
isSupersetIntv (toIntv af) aiv = true /\
eval_expr E (toRMap Gamma) (toREval (toRExp e)) vR REAL /\
eval_expr E (toRMap Gamma) fBits (toREval (toRExp e)) vR REAL /\
af_evals (afQ2R af) vR map) ->
exists iv err vR,
FloverMap.find e A = Some (iv, err) /\
eval_expr E (toRMap Gamma) (toREval (toRExp e)) vR REAL /\
eval_expr E (toRMap Gamma) fBits (toREval (toRExp e)) vR REAL /\
(Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
Proof.
intros sound_affine.
......@@ -773,7 +773,7 @@ Proof.
split; eauto using Rle_trans.
Qed.
Definition checked_expressions (A: analysisResult) E Gamma fVars dVars e iexpmap inoise map1 :=
Definition checked_expressions (A: analysisResult) E Gamma fBits fVars dVars e iexpmap inoise map1 :=
exists af vR aiv aerr,
NatSet.Subset (usedVars e) (NatSet.union fVars dVars) /\
FloverMap.find e A = Some (aiv, aerr) /\
......@@ -781,17 +781,17 @@ Definition checked_expressions (A: analysisResult) E Gamma fVars dVars e iexpmap
FloverMap.find e iexpmap = Some af /\
fresh inoise af /\
(forall n, (n >= inoise)%nat -> map1 n = None) /\
eval_expr E (toRMap Gamma) (toREval (toRExp e)) vR REAL /\
validRanges e A E Gamma /\
eval_expr E (toRMap Gamma) fBits (toREval (toRExp e)) vR REAL /\
validRanges e A E Gamma fBits /\
af_evals (afQ2R af) vR map1.
Lemma checked_expressions_contained A E Gamma fVars dVars e expmap1 expmap2 map1 map2 noise1 noise2:
Lemma checked_expressions_contained A E Gamma fBits fVars dVars e expmap1 expmap2 map1 map2 noise1 noise2:
contained_map map1 map2 ->
contained_flover_map expmap1 expmap2 ->
(noise2 >= noise1)%nat ->
(forall n : nat, (n >= noise2)%nat -> map2 n = None) ->
checked_expressions A E Gamma fVars dVars e expmap1 noise1 map1 ->
checked_expressions A E Gamma fVars dVars e expmap2 noise2 map2.
checked_expressions A E Gamma fBits fVars dVars e expmap1 noise1 map1 ->
checked_expressions A E Gamma fBits fVars dVars e expmap2 noise2 map2.
Proof.
intros cont contf Hnoise Hvalidmap checked1.
unfold checked_expressions in checked1 |-*.
......@@ -800,10 +800,10 @@ Proof.
intuition; eauto using fresh_monotonic, af_evals_map_extension.
Qed.
Lemma checked_expressions_flover_map_add_compat A E Gamma fVars dVars e e' af expmap noise map:
Lemma checked_expressions_flover_map_add_compat A E Gamma fBits fVars dVars e e' af expmap noise map:
Q_orderedExps.exprCompare e e' <> Eq ->
checked_expressions A E Gamma fVars dVars e' expmap noise map ->
checked_expressions A E Gamma fVars dVars e' (FloverMap.add e af expmap) noise map.
checked_expressions A E Gamma fBits fVars dVars e' expmap noise map ->
checked_expressions A E Gamma fBits fVars dVars e' (FloverMap.add e af expmap) noise map.
Proof.
intros Hneq checked1.
unfold checked_expressions in checked1 |-*.
......@@ -814,9 +814,9 @@ Proof.
Qed.
Lemma validAffineBounds_sound (e: expr Q) (A: analysisResult) (P: precond)
fVars dVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
fVars dVars (E: env) Gamma fBits exprAfs noise iexpmap inoise map1:
(forall e, (exists af, FloverMap.find e iexpmap = Some af) ->
checked_expressions A E Gamma fVars dVars e iexpmap inoise map1) ->
checked_expressions A E Gamma fBits fVars dVars e iexpmap inoise map1) ->
(inoise > 0)%nat ->
(forall n, (n >= inoise)%nat -> map1 n = None) ->
validAffineBounds e A P dVars iexpmap inoise = Some (exprAfs, noise) ->
......@@ -833,12 +833,12 @@ Lemma validAffineBounds_sound (e: expr Q) (A: analysisResult) (P: precond)
fresh noise af /\
(forall n, (n >= noise)%nat -> map2 n = None) /\
(noise >= inoise)%nat /\
eval_expr E (toRMap Gamma) (toREval (toRExp e)) vR REAL /\
validRanges e A E Gamma /\
eval_expr E (toRMap Gamma) fBits (toREval (toRExp e)) vR REAL /\
validRanges e A E Gamma fBits /\
af_evals (afQ2R af) vR map2 /\
(forall e, FloverMap.find e iexpmap = None ->
(exists af, FloverMap.find e exprAfs = Some af) ->
checked_expressions A E Gamma fVars dVars e exprAfs noise map2).
checked_expressions A E Gamma fBits fVars dVars e exprAfs noise map2).
Proof.
revert noise exprAfs inoise iexpmap map1.
induction e;
......@@ -885,7 +885,7 @@ Proof.
specialize (fVarsSound H') as [vR [eMap interval_containment]].
assert (FloverMap.find (Var Q n) (FloverMap.add (Var Q n) (fromIntv (P n) inoise) iexpmap) = Some (fromIntv (P n) inoise)) as Hfind
by (rewrite FloverMapFacts.P.F.add_eq_o; try auto; apply Q_orderedExps.exprCompare_refl).
assert (eval_expr E (toRMap Gamma) (toREval (toRExp (Var Q n))) vR REAL) as Heeval
assert (eval_expr E (toRMap Gamma) fBits (toREval (toRExp (Var Q n))) vR REAL) as Heeval
by (constructor; auto; simpl; rewrite varsTyped; reflexivity).
destruct (Qeq_bool (ivlo (P n)) (ivhi (P n))) eqn: Heq.
* assert (af_evals (afQ2R (fromIntv (P n) inoise)) vR map1) as Hevals.
......@@ -1137,7 +1137,7 @@ Proof.
assert (FloverMap.find (elt:=affine_form Q) (Const m v) (FloverMap.add (Const m v) (fromIntv (v, v) noise) iexpmap) = Some (fromIntv (v, v) noise))
by (rewrite FloverMapFacts.P.F.add_eq_o; try auto;
apply Q_orderedExps.exprCompare_refl).
assert (eval_expr E (toRMap Gamma) (toREval (toRExp (Const m v))) (perturb (Q2R v) REAL 0) REAL)
assert (eval_expr E (toRMap Gamma) fBits (toREval (toRExp (Const m v))) (perturb (Q2R v) REAL 0) REAL)
by (constructor; simpl; rewrite Rabs_R0; lra).
exists map1, (fromIntv (v, v) noise), (perturb (Q2R v) REAL 0), i, e.
repeat split; auto.
......@@ -1373,10 +1373,11 @@ Proof.
apply plus_aff_sound; auto.
eauto using af_evals_map_extension.
}
assert (eval_expr E (toRMap Gamma) (toREval (toRExp (Binop Plus e1 e2)))
(perturb (evalBinop Plus vR1 vR2) REAL 0) REAL)
by (replace REAL with (join REAL REAL) by trivial;
apply Binop_dist; try rewrite Rabs_R0; simpl; auto; try lra; congruence).
assert (eval_expr E (toRMap Gamma) fBits (toREval (toRExp (Binop Plus e1 e2)))
(perturb (evalBinop Plus vR1 vR2) REAL 0) REAL).
{ eapply Binop_dist' with (delta := 0%R); eauto; try congruence.
- rewrite Rabs_R0; cbn; lra.
- intros; cbn in *; contradiction. }
exists ihmap2, (AffineArithQ.plus_aff af1 af2), (perturb (evalBinop Plus vR1 vR2) REAL 0)%R, aiv, aerr.
rewrite plus_0_r.
repeat split; eauto using AffineArithQ.plus_aff_preserves_fresh, fresh_monotonic.
......@@ -1461,9 +1462,10 @@ Proof.
unfold AffineArithQ.negate_aff.
now apply AffineArithQ.fresh_mult_aff_const.
}
assert (eval_expr E (toRMap Gamma) (toREval (toRExp (Binop Sub e1 e2))) (perturb (evalBinop Sub vR1 vR2) REAL 0) REAL)
by (replace REAL with (join REAL REAL) by trivial; apply Binop_dist;
try rewrite Rabs_R0; simpl; auto; try lra; congruence).
assert (eval_expr E (toRMap Gamma) fBits (toREval (toRExp (Binop Sub e1 e2))) (perturb (evalBinop Sub vR1 vR2) REAL 0) REAL).
{ eapply Binop_dist' with (delta := 0%R); eauto; try congruence.
- rewrite Rabs_R0; cbn; lra.
- intros; cbn in *; contradiction. }
exists ihmap2, (AffineArithQ.subtract_aff af1 af2), (perturb (evalBinop Sub vR1 vR2) REAL 0)%R, aiv, aerr.
repeat split; auto.
* etransitivity; try exact ihcont1.
......@@ -1556,9 +1558,10 @@ Proof.
apply AffineArithQ.mult_aff_aux_preserves_fresh;
apply fresh_inc; now rewrite afQ2R_fresh.
}
assert (eval_expr E (toRMap Gamma) (toREval (toRExp (Binop Mult e1 e2))) (perturb (evalBinop Mult vR1 vR2) REAL 0) REAL)
by (replace REAL with (join REAL REAL) by trivial;
apply Binop_dist; try rewrite Rabs_R0; simpl; auto; try lra; congruence).
assert (eval_expr E (toRMap Gamma) fBits (toREval (toRExp (Binop Mult e1 e2))) (perturb (evalBinop Mult vR1 vR2) REAL 0) REAL).
{ eapply Binop_dist' with (delta := 0%R); eauto; try congruence.
- rewrite Rabs_R0; cbn; lra.
- intros; cbn in *; contradiction. }
assert (af_evals (afQ2R (AffineArithQ.mult_aff af1 af2 subnoise2)) (perturb (evalBinop Mult vR1 vR2) REAL 0) (updMap ihmap2 subnoise2 qMult)) by
(unfold perturb; simpl evalBinop; rewrite afQ2R_mult_aff; assumption).
assert (forall n : nat, (n >= subnoise2 + 1)%nat -> updMap ihmap2 subnoise2 qMult n = None).
......@@ -1712,11 +1715,11 @@ Proof.
apply Hsubvalidmap2.
lia.
}
assert (eval_expr E (toRMap Gamma) (toREval (toRExp (Binop Div e1 e2))) (perturb (evalBinop Div vR1 vR2) REAL 0) REAL)
by (replace REAL with (join REAL REAL) by trivial;
apply Binop_dist; try rewrite Rabs_R0; simpl; auto; try lra;
intros _;
eauto using above_below_nonzero).
assert (eval_expr E (toRMap Gamma) fBits (toREval (toRExp (Binop Div e1 e2))) (perturb (evalBinop Div vR1 vR2) REAL 0) REAL).
{ eapply Binop_dist' with (delta := 0%R); eauto; try congruence.
- rewrite Rabs_R0; cbn; lra.
- intros _; eauto using above_below_nonzero.
- intros; cbn in *; contradiction. }
assert (af_evals (afQ2R (AffineArithQ.divide_aff af1 af2 subnoise2)) (perturb (evalBinop Div vR1 vR2) REAL 0) (updMap (updMap ihmap2 subnoise2 qInv) (subnoise2 + 1) qMult))
by (unfold perturb; simpl evalBinop; rewrite afQ2R_divide_aff; auto).
exists (updMap (updMap ihmap2 subnoise2 qInv) (subnoise2 + 1) qMult),
......@@ -1954,9 +1957,10 @@ Proof.
apply Hsubmapvalid3.
lia.
}
assert (eval_expr E (toRMap Gamma) (toREval (toRExp (Fma e1 e2 e3))) (perturb (evalFma vR1 vR2 vR3)REAL 0) REAL)
by (replace REAL with (join3 REAL REAL REAL) by trivial;
apply Fma_dist; try rewrite Rabs_R0; auto; simpl; lra).
assert (eval_expr E (toRMap Gamma) fBits (toREval (toRExp (Fma e1 e2 e3))) (perturb (evalFma vR1 vR2 vR3)REAL 0) REAL).
{ eapply Fma_dist'; eauto; try congruence.
- rewrite Rabs_R0; cbn; lra.
- intros. cbn in *. contradiction. }
assert (af_evals (afQ2R (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 subnoise3))) (perturb (evalFma vR1 vR2 vR3) REAL 0) (updMap ihmap3 subnoise3 qMult)).
{
unfold perturb.
......@@ -2142,6 +2146,7 @@ Proof.
* rewrite FloverMapFacts.P.F.add_neq_o in Hsome; auto.
apply checked_expressions_flover_map_add_compat; auto.
apply visitedSubexpr; eauto.
Unshelve. all:exact 0%nat.
Qed.
Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (validVars: NatSet.t)
......@@ -2164,24 +2169,24 @@ Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (valid
| Ret e => validAffineBounds e A P validVars exprsAf currentMaxNoise
end.
Lemma eval_expr_ssa_extension (e: expr R) (e' : expr Q) E Gamma vR vR' m n c fVars dVars outVars:
Lemma eval_expr_ssa_extension (e: expr R) (e' : expr Q) E Gamma fBits vR vR' m n c fVars dVars outVars:
ssa (Let m n e' c) (fVars ∪ dVars) outVars ->
NatSet.Subset (usedVars e) (fVars ∪ dVars) ->
~ (n ∈ fVars ∪ dVars) ->
eval_expr E Gamma e vR REAL ->
eval_expr (updEnv n vR' E) (updDefVars n REAL Gamma) e vR REAL.
eval_expr E Gamma fBits e vR REAL ->
eval_expr (updEnv n vR' E) (updDefVars n REAL Gamma) fBits e vR REAL.
Proof.
intros Hssa Hsub Hnotin Heval.
eapply eval_expr_ignore_bind; [auto |].
edestruct ssa_inv_let; eauto.
Qed.
Lemma validRanges_ssa_extension (e: expr Q) (e' : expr Q) A E Gamma vR' m n c fVars dVars outVars:
Lemma validRanges_ssa_extension (e: expr Q) (e' : expr Q) A E Gamma fBits vR' m n c fVars dVars outVars:
ssa (Let m n e' c) (fVars ∪ dVars) outVars ->
NatSet.Subset (usedVars e) (fVars ∪ dVars) ->
~ (n ∈ fVars ∪ dVars) ->
validRanges e A E Gamma ->
validRanges e A (updEnv n vR' E) (updDefVars n REAL Gamma).
validRanges e A E Gamma fBits ->
validRanges e A (updEnv n vR' E) (updDefVars n REAL Gamma) fBits.
Proof.
intros Hssa Hsub Hnotin Hranges.
induction e.
......@@ -2251,10 +2256,10 @@ Proof.
rewrite usedVars_toREval_toRExp_compat; auto.
Qed.
Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond)
Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond) fBits
fVars dVars outVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
(forall e, (exists af, FloverMap.find e iexpmap = Some af) ->
checked_expressions A E Gamma fVars dVars e iexpmap inoise map1) ->
checked_expressions A E Gamma fBits fVars dVars e iexpmap inoise map1) ->
(inoise > 0)%nat ->
(forall n, (n >= inoise)%nat -> map1 n = None) ->
validAffineBoundsCmd c A P dVars iexpmap inoise = Some (exprAfs, noise) ->
......@@ -2272,12 +2277,12 @@ Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond)
fresh noise af /\
(forall n, (n >= noise)%nat -> map2 n = None) /\
(noise >= inoise)%nat /\
bstep (toREvalCmd (toRCmd c)) E (toRMap Gamma) vR REAL /\
validRangesCmd c A E Gamma /\
bstep (toREvalCmd (toRCmd c)) E (toRMap Gamma) fBits vR REAL /\
validRangesCmd c A E Gamma fBits /\
af_evals (afQ2R af) vR map2 /\
(forall e, FloverMap.find e iexpmap = None ->
(exists af, FloverMap.find e exprAfs = Some af) ->
exists E' Gamma' dVars, checked_expressions A E' Gamma' fVars dVars e exprAfs noise map2).
exists E' Gamma' dVars, checked_expressions A E' Gamma' fBits fVars dVars e exprAfs noise map2).
Proof.
revert E Gamma dVars iexpmap inoise exprAfs noise map1.
induction c; intros * visitedExpr Hnoise Hmapvalid valid_bounds_cmd
......
coq/CertificateChecker.v
View file @ 313ac660
......@@ -12,9 +12,10 @@ From Flover
Require Export Infra.ExpressionAbbrevs Flover.Commands Coq.QArith.QArith.
(** Certificate checking function **)
Definition CertificateChecker (e:expr Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
let tMap := (typeMap defVars e (FloverMap.empty mType)) in
if (typeCheck e defVars tMap)
Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
(P:precond) (defVars:nat -> option mType) (fBits:FloverMap.t nat):=
let tMap := (typeMap defVars e (FloverMap.empty mType) fBits) in
if (typeCheck e defVars tMap fBits)
then
if RangeValidator e absenv P NatSet.empty && FPRangeValidator e absenv tMap NatSet.empty
then RoundoffErrorValidator e tMap absenv NatSet.empty
......@@ -26,7 +27,8 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult) (P:precond) (de
Apart from assuming two executions, one in R and one on floats, we assume that
the real valued execution respects the precondition.
**)
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVars:
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P
defVars fBits:
forall (E1 E2:env),
approxEnv E1 defVars absenv (usedVars e) NatSet.empty E2 ->
(forall v, NatSet.In v (Expressions.usedVars e) ->
......@@ -35,13 +37,13 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVa
(forall v, NatSet.In v (usedVars e) ->
exists m : mType,
defVars v = Some m) ->
CertificateChecker e absenv P defVars = true ->
CertificateChecker e absenv P defVars fBits = true ->
exists iv err vR vF m,
FloverMap.find e absenv = Some (iv, err) /\
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) vR REAL /\
eval_expr E2 defVars (toRExp e) vF m /\
eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e)) vR REAL /\
eval_expr E2 defVars (toRBMap fBits) (toRExp e) vF m /\
(forall vF m,
eval_expr E2 defVars (toRExp e) vF m ->
eval_expr E2 defVars (toRBMap fBits) (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
(**
The proofs is a simple composition of the soundness proofs for the range
......@@ -68,19 +70,20 @@ Proof.
{ unfold vars_typed. intros; apply types_defined. set_tac. destruct H1; set_tac.
split; try auto. hnf; intros; set_tac. }
rename R into validFPRanges.
assert (validRanges e absenv E1 defVars) as valid_e.
assert (validRanges e absenv E1 defVars (toRBMap fBits)) as valid_e.
{ eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (Gamma:=defVars) (E:=E1));
auto. }
pose proof (validRanges_single _ _ _ _ valid_e) as valid_single;
pose proof (validRanges_single _ _ _ _ _ valid_e) as valid_single;
destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].
destruct iv_e as [elo ehi].
edestruct (RoundoffErrorValidator_sound e (typeMap defVars e (FloverMap.empty mType)) L approxE1E2 H0 eval_real R0 valid_e H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
edestruct (RoundoffErrorValidator_sound e (typeMap defVars e (FloverMap.empty mType) fBits) L approxE1E2 H0 eval_real R0 valid_e H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
exists (elo, ehi), err_e, vR, vF, mF; split; auto.
Qed.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:=
let tMap := typeMapCmd defVars f (FloverMap.empty mType) in
if (typeCheckCmd f defVars tMap && validSSA f (freeVars f))
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond)
defVars fBits:=
let tMap := typeMapCmd defVars f (FloverMap.empty mType) fBits in
if (typeCheckCmd f defVars tMap fBits && validSSA f (freeVars f))
then
if (RangeValidatorCmd f absenv P NatSet.empty) &&
FPRangeValidatorCmd f absenv tMap NatSet.empty
......@@ -88,7 +91,8 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) d
else false
else false.
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P defVars:
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P
defVars fBits:
forall (E1 E2:env),
approxEnv E1 defVars absenv (freeVars f) NatSet.empty E2 ->
(forall v, NatSet.In v (freeVars f) ->
......@@ -97,13 +101,13 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P d
(forall v, NatSet.In v (freeVars f) ->
exists m : mType,
defVars v = Some m) ->
CertificateCheckerCmd f absenv P defVars = true ->
CertificateCheckerCmd f absenv P defVars fBits = true ->
exists iv err vR vF m,
FloverMap.find (getRetExp f) absenv = Some (iv,err) /\
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL /\
bstep (toRCmd f) E2 defVars vF m /\
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) (toRBMap fBits) vR REAL /\
bstep (toRCmd f) E2 defVars (toRBMap fBits) vF m /\
(forall vF m,
bstep (toRCmd f) E2 defVars vF m ->
bstep (toRCmd f) E2 defVars (toRBMap fBits) vF m ->
(Rabs (vR - vF) <= Q2R (err))%R).
(**
The proofs is a simple composition of the soundness proofs for the range
......@@ -129,11 +133,11 @@ Proof.
destruct H0; set_tac. }
assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
as freeVars_contained by set_tac.
assert (validRangesCmd f absenv E1 defVars) as valid_f.
assert (validRangesCmd f absenv E1 defVars (toRBMap fBits)) as valid_f.
{ eapply RangeValidatorCmd_sound; eauto.
unfold affine_dVars_range_valid; intros.
set_tac. }
pose proof (validRangesCmd_single _ _ _ _ valid_f) as valid_single.
pose proof (validRangesCmd_single _ _ _ _ _ valid_f) as valid_single.
destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
destruct iv as [f_lo f_hi].
edestruct (RoundoffErrorValidatorCmd_sound) as [[vF [mF eval_float]] ?]; eauto.
......
coq/Commands.v
View file @ 313ac660
......@@ -49,14 +49,14 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
Define big step semantics for the Flover language, terminating on a "returned"
result value
**)
Inductive bstep : cmd R -> env -> (nat -> option mType) -> R -> mType -> Prop :=
let_b m m' x e s E v res defVars:
eval_expr E defVars e v m ->
bstep s (updEnv x v E) (updDefVars x m defVars) res m' ->
bstep (Let m x e s) E defVars res m'
|ret_b m e E v defVars:
eval_expr E defVars e v m ->
bstep (Ret e) E defVars v m.
Inductive bstep : cmd R -> env -> (nat -> option mType) -> (expr R -> option nat) -> R -> mType -> Prop :=
let_b m m' x e s E v res defVars fBits:
eval_expr E defVars fBits e v m ->
bstep s (updEnv x v E) (updDefVars x m defVars) fBits res m' ->
bstep (Let m x e s) E defVars fBits res m'
|ret_b m e E v defVars fBits:
eval_expr E defVars fBits e v m ->
bstep (Ret e) E defVars fBits v m.
(**
The free variables of a command are all used variables of exprressions
......@@ -88,14 +88,14 @@ Fixpoint liveVars V (f:cmd V) :NatSet.t :=
end.
Lemma bstep_eq_env f:
forall E1 E2 Gamma v m,
forall E1 E2 Gamma fBits v m,
(forall x, E1 x = E2 x) ->
bstep f E1 Gamma v m ->
bstep f E2 Gamma v m.
bstep f E1 Gamma fBits v m ->
bstep f E2 Gamma fBits v m.
Proof.
induction f; intros * eq_envs bstep_E1;
inversion bstep_E1; subst; simpl in *.
- eapply eval_eq_env in H7; eauto. eapply let_b; eauto.
- eapply eval_eq_env in H8; eauto. eapply let_b; eauto.
eapply IHf. instantiate (1:=(updEnv n v0 E1)).
+ intros; unfold updEnv.
destruct (x=? n); auto.
......
coq/ErrorBounds.v
View file @ 313ac660
......@@ -7,9 +7,9 @@ Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.
Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealSimps Flover.Infra.RealRationalProps.
Require Import Flover.Environments Flover.Infra.ExpressionAbbrevs.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars:
eval_expr E1 (toRMap defVars) (Const REAL n) nR REAL ->
eval_expr E2 defVars (Const m n) nF m ->
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars fBits:
eval_expr E1 (toRMap defVars) fBits (Const REAL n) nR REAL ->
eval_expr E2 defVars fBits (Const m n) nF m ->
(Rabs (nR - nF) <= computeErrorR n m)%R.
Proof.
intros eval_real eval_float.
......@@ -30,14 +30,19 @@ Proof.
Qed.
Lemma add_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR REAL ->
(vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars fBits:
eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars fBits (toRExp e1) e1F m1->
eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars fBits (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) fBits (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(fun e =>
match e with
| Binop b (Var _ 1) (Var _ 2) => fBits (toRExp (Binop b e1 e2))
| _ => fBits e
end)
(Binop Plus (Var R 1) (Var R 2)) vF m ->
(Rabs (e1R - e1F) <= Q2R err1)%R ->
(Rabs (e2R - e2F) <= Q2R err2)%R ->
......@@ -50,22 +55,20 @@ Proof.
assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
subst; simpl in H3; auto.
rewrite delta_0_deterministic in plus_real; auto.
rewrite (delta_0_deterministic (evalBinop Plus v1 v2) (join REAL REAL) delta); auto.
rewrite (delta_0_deterministic (evalBinop Plus v1 v2) REAL delta); auto.
unfold evalBinop in *; simpl in *.
clear delta H3.
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in plus_real.
rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in plus_real.
clear H5 H6 H7 v1 v2.
clear delta H2.
rewrite (meps_0_deterministic (toRExp e1) H3 e1_real);
rewrite (meps_0_deterministic (toRExp e2) H4 e2_real).
rewrite (meps_0_deterministic (toRExp e1) H3 e1_real) in plus_real.
rewrite (meps_0_deterministic (toRExp e2) H4 e2_real) in plus_real.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion plus_float; subst.
unfold perturb; simpl.
inversion H4; subst; inversion H7; subst.
unfold updEnv; simpl.
unfold updEnv in H1,H6; simpl in *.
symmetry in H1,H6.
inversion H1; inversion H6; subst.
inversion H6; subst; inversion H7; subst.
unfold updEnv in H1,H12; simpl in *.
symmetry in H1,H12.
inversion H1; inversion H12; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear plus_float H4 H7 plus_real e1_real e1_float e2_real e2_float H8 H6 H1.
repeat rewrite Rmult_plus_distr_l.
......@@ -73,7 +76,7 @@ Proof.
rewrite Rsub_eq_Ropp_Rplus.
unfold computeErrorR.
pose proof (Rabs_triang (e1R + - e1F) ((e2R + - e2F) + - ((e1F + e2F) * delta))).
destruct (join m0 m3);
destruct m;
repeat rewrite Ropp_plus_distr; try rewrite plus_bounds_simplify; try rewrite Rplus_assoc.
{ repeat rewrite <- Rplus_assoc.
assert (e1R + e2R + - e1F + - e2F = e1R + - e1F + e2R + - e2F)%R by lra.
......@@ -83,13 +86,13 @@ Proof.
apply Rabs_triang; apply Rplus_le_compat; try auto.
rewrite Rplus_0_r.
apply Rplus_le_compat; try auto. }
Focus 4.
4: {
eapply Rle_trans.
apply Rabs_triang. setoid_rewrite Rplus_assoc at 2.
apply Rplus_le_compat; try auto.
eapply Rle_trans.
apply Rabs_triang.
rewrite Rabs_Ropp. apply Rplus_le_compat; auto.
rewrite Rabs_Ropp. apply Rplus_le_compat; auto. }
all: eapply Rle_trans; try eapply H.
all: setoid_rewrite Rplus_assoc at 2.
all: eapply Rplus_le_compat; try auto.
......@@ -103,14 +106,19 @@ Qed.
Copy-Paste proof with minor differences, was easier then manipulating the evaluations and then applying the lemma
**)
Lemma subtract_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R)
(e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars:
eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR REAL ->
(e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars fBits:
eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e1)) e1R REAL ->
eval_expr E2 defVars fBits (toRExp e1) e1F m1 ->
eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e2)) e2R REAL ->
eval_expr E2 defVars fBits (toRExp e2) e2F m2 ->
eval_expr E1 (toRMap defVars) fBits (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR REAL ->
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(fun e =>
match e with
| Binop b (Var _ 1) (Var _ 2) => fBits (toRExp (Binop b e1 e2))
| _ => fBits e
end)
(Binop Sub (Var R 1) (Var R 2)) vF m ->