Commit 353631d9 authored by Heiko Becker's avatar Heiko Becker

Finish proving the validRanges and validRangesCmd predicates and adding them...

Finish proving the validRanges and validRangesCmd predicates and adding them to all other soundness proofs
parent 7256c32f
......@@ -3,7 +3,7 @@ Require Import Recdef.
Require Import Flover.AffineForm Flover.AffineArithQ Flover.AffineArith.
Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
Require Import Flover.Infra.Ltacs Flover.Infra.RealSimps Flover.Typing Flover.ssaPrgs.
Require Import Flover.IntervalValidation.
Require Import Flover.IntervalValidation Flover.RealRangeArith.
Lemma usedVars_eq_compat e1 e2:
Q_orderedExps.eq e1 e2 ->
......@@ -113,7 +113,7 @@ Fixpoint validAffineBounds (e: expr Q) (A: analysisResult) (P: precond) (validVa
olet valid := validAffineBounds e' A P validVars exprsAf currentMaxNoise in
let (exprsAf', n') := valid in
olet af := FloverMap.find e' exprsAf' in
match o with
match o with
| Neg =>
updateExpMap e (AffineArithQ.negate_aff af) n' exprsAf' intv
| Inv =>
......@@ -155,7 +155,7 @@ Fixpoint validAffineBounds (e: expr Q) (A: analysisResult) (P: precond) (validVa
let (exprsAf3, n3) := valid3 in
olet af3 := FloverMap.find e3 exprsAf3 in
updateExpMapSucc e (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 n3)) n3 exprsAf3 intv
| Downcast _ e' =>
| Downcast _ e' =>
olet valid' := validAffineBounds e' A P validVars exprsAf currentMaxNoise in
let (exprsAf', n') := valid' in
olet asubres := FloverMap.find e' A in
......@@ -485,7 +485,7 @@ Qed.
Lemma afQ2R_fresh n a:
fresh n a <-> fresh n (afQ2R a).
Proof.
split; induction a; intros *.
split; induction a; intros *.
all: try (unfold fresh, get_max_index; rewrite get_max_index_aux_equation; now simpl).
all: intros A.
all: remember A as A' eqn:tmp; clear tmp.
......@@ -562,7 +562,7 @@ Definition affine_fVars_P_sound (fVars:NatSet.t) (E:env) (P:precond) :Prop :=
NatSet.In v fVars ->
exists vR, E v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R.
Definition affine_vars_typed (S: NatSet.t) (Gamma: nat -> option mType) :=
forall v, NatSet.In v S ->
exists m: mType, Gamma v = Some m.
......@@ -619,7 +619,7 @@ 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 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) ->
(inoise > 0)%nat ->
......@@ -1851,7 +1851,7 @@ Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (valid
end.
Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond)
fVars dVars outVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
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) ->
(inoise > 0)%nat ->
......@@ -2104,7 +2104,7 @@ Proof.
exists ihmap, ihaf, ihvR, ihaiv, ihaerr.
repeat split; try auto.
+ econstructor; try eauto.
eapply IntervalValidation.swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n REAL Gamma)) ; try eauto.
eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n REAL Gamma)) ; try eauto.
intros n1; erewrite Rmap_updVars_comm; eauto.
+ intros e' Hnone Hsome.
specialize (ihchecked e').
......
......@@ -4,12 +4,12 @@
Running this function on the encoded analysis result gives the desired theorem
as shown in the soundness theorem.
**)
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Flover.Infra.RealSimps Flover.Infra.RationalSimps Flover.Infra.RealRationalProps Flover.Infra.Ltacs.
Require Import Flover.RealRangeValidator Flover.RoundoffErrorValidator Flover.Environments Flover.Typing Flover.FPRangeValidator.
From Flover
Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
Environments Typing FPRangeValidator ExpressionAbbrevs Commands.
Require Export Coq.QArith.QArith.
Require Export Flover.Infra.ExpressionAbbrevs Flover.Commands.
Require Export Infra.ExpressionAbbrevs Flover.Commands.
(** Certificate checking function **)
Definition CertificateChecker (e:expr Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
......@@ -68,10 +68,13 @@ 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.
edestruct (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (Gamma:=defVars) (E:=E1))
as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]]; eauto.
assert (validRanges e absenv E1 defVars) 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;
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 L1 H P_valid H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
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.
exists (elo, ehi), err_e, vR, vF, mF; split; auto.
Qed.
......@@ -81,7 +84,7 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) d
then
if (RangeValidatorCmd f absenv P NatSet.empty) &&
FPRangeValidatorCmd f absenv tMap NatSet.empty
then (validErrorboundCmd f tMap absenv NatSet.empty)
then (RoundoffErrorValidatorCmd f tMap absenv NatSet.empty)
else false
else false.
......@@ -126,12 +129,13 @@ Proof.
destruct H0; set_tac. }
assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
as freeVars_contained by set_tac.
edestruct (validIntervalboundsCmd_sound)
as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]]; eauto.
assert (validRangesCmd f absenv E1 defVars) as valid_f.
{ eapply RangeValidatorCmd_sound; eauto.
unfold affine_dVars_range_valid; intros.
set_tac. }
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 validErrorboundCmd_gives_eval as [vF [mF eval_float]]; eauto.
edestruct (RoundoffErrorValidatorCmd_sound) as [[vF [mF eval_float]] ?]; eauto.
exists (f_lo, f_hi), err, vR, vF, mF; split; try auto.
split; try auto; split; try auto.
intros.
eapply validErrorboundCmd_sound; eauto.
Qed.
......@@ -2181,7 +2181,7 @@ Theorem validErrorboundCmd_gives_eval (f:cmd Q) :
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL ->
validErrorboundCmd f Gamma A dVars = true ->
validRangesCmd f A E1 (toRMap defVars) ->
validRangesCmd f A E1 defVars ->
vars_typed (NatSet.union fVars dVars) defVars ->
FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
(exists vF m,
......@@ -2241,32 +2241,12 @@ Proof.
split; try auto. }
{ eapply swap_Gamma_bstep with (Gamma1 := updDefVars n REAL (toRMap defVars));
eauto using Rmap_updVars_comm. }
{ eapply valid_cont.
{ intros v1 v1_mem.
unfold updEnv.
case_eq (v1 =? n); intros v1_eq.
- apply Nat.eqb_eq in v1_eq; subst.
exists v, (q1, q2), e1; split; try auto; split; try auto; simpl.
destruct (validIntervalbounds_sound e (E:=E1) (Gamma:=defVars) L (fVars:=fVars))
as [iv_e' [ err_e' [vR_e [map_e [eval_real_e bounded_real_e]]]]];
eauto.
rewrite map_e in *; inversion Heqo; subst.
pose proof (meps_0_deterministic _ eval_real_e H7); subst.
simpl in *. inversion Heqo0; subst; lra.
- rewrite Nat.eqb_neq in v1_eq; set_tac.
destruct v1_mem; subst; try congruence.
apply fVars_sound ; try auto.
destruct H0; auto. }
{ intros v1 mem_fVars.
specialize (P_valid v1 mem_fVars).
unfold updEnv.
case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try auto.
rewrite Nat.eqb_eq in case_v1; subst.
assert (NatSet.In n (NatSet.union fVars dVars))
as in_union
by (rewrite NatSet.union_spec; auto).
rewrite <- NatSet.mem_spec in in_union.
rewrite in_union in *; congruence. }
{ apply validRangesCmd_swap with (Gamma1 := updDefVars n REAL defVars).
- intros x.
unfold toRMap, updDefVars.
destruct (x =? n) eqn:?; auto.
- apply valid_cont.
apply swap_Gamma_eval_expr with (Gamma1 := toRMap defVars); try auto. }
{ intros v1 v1_mem; set_tac.
unfold updDefVars.
case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try eauto.
......@@ -2277,16 +2257,17 @@ Proof.
rewrite Nat.eqb_neq in case_v1; congruence. }
{ exists vF_res; exists m_res; try auto.
econstructor; eauto. }
+ destruct valid_intv as [[? ?] ?]; auto.
- inversion eval_real; subst.
unfold updEnv; simpl.
unfold validErrorboundCmd in valid_bounds.
simpl in *.
destruct valid_intv.
edestruct validErrorbound_sound as [[vF [mF eval_e]] bounded_e]; eauto.
exists vF; exists mF; econstructor; eauto.
Qed.
Theorem validErrorboundCmd_sound (f:cmd Q):
forall A E1 E2 outVars fVars dVars vR vF mF elo ehi err P Gamma defVars,
forall A E1 E2 outVars fVars dVars vR vF mF elo ehi err Gamma defVars,
typeCheckCmd f defVars Gamma = true ->
approxEnv E1 defVars A fVars dVars E2 ->
ssa f (NatSet.union fVars dVars) outVars ->
......@@ -2294,16 +2275,14 @@ Theorem validErrorboundCmd_sound (f:cmd Q):
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL ->
bstep (toRCmd f) E2 defVars vF mF ->
validErrorboundCmd f Gamma A dVars = true ->
validIntervalboundsCmd f A P dVars = true ->
dVars_range_valid dVars E1 A ->
fVars_P_sound fVars E1 P ->
validRangesCmd f A E1 defVars ->
vars_typed (NatSet.union fVars dVars) defVars ->
FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
(Rabs (vR - vF) <= (Q2R err))%R.
Proof.
induction f;
intros * type_f approxc1c2 ssa_f freeVars_subset eval_real eval_float
valid_bounds valid_intv fVars_sound P_valid types_defined A_res;
valid_bounds valid_intv types_defined A_res;
cbn in *; Flover_compute; try congruence; type_conv; subst.
- inversion eval_real;
inversion eval_float;
......@@ -2317,25 +2296,20 @@ Proof.
match goal with
| [H : validErrorbound _ _ _ _ = true |- _] =>
eapply validErrorbound_sound
with (err := e2) (elo := fst(i)) (ehi:= snd(i)) in H; edestruct i; eauto;
with (err := e0) (elo := fst(i)) (ehi:= snd(i)) in H; edestruct i; eauto;
destruct H as [[vFe [mFe eval_float_e]] bounded_e]
end.
canonize_hyps.
rename R into valid_rec.
rewrite (typingSoundnessExp _ _ L0 eval_float_e) in *;
rewrite (typingSoundnessExp _ _ L eval_float_e) in *;
simpl in *.
(* destruct (Gamma (Var Q n)); try congruence. *)
(* match goal with *)
(* | [ H: _ && _ = true |- _] => andb_to_prop H *)
(* end. *)
(* type_conv. *)
apply (IHf A (updEnv n v E1) (updEnv n v0 E2) outVars fVars
(NatSet.add n dVars) vR vF mF elo ehi err P Gamma
(NatSet.add n dVars) vR vF mF elo ehi err Gamma
(updDefVars n m1 defVars));
eauto.
+ eapply approxUpdBound; try eauto.
simpl in *.
apply Rle_trans with (r2:= Q2R e2); try lra.
apply Rle_trans with (r2:= Q2R e0); try lra.
eapply bounded_e; eauto.
+ eapply ssa_equal_set; eauto.
hnf. intros a; split; intros in_set.
......@@ -2354,34 +2328,13 @@ Proof.
split; try auto.
+ eapply swap_Gamma_bstep with (Gamma1 := updDefVars n REAL (toRMap defVars));
eauto using Rmap_updVars_comm.
+ intros v1 v1_mem.
unfold updEnv.
case_eq (v1 =? n); intros v1_eq.
* apply Nat.eqb_eq in v1_eq; subst.
exists v, (q1,q2), e1; split; try auto; split; try auto.
simpl. rewrite <- R1, <- R0.
destruct (validIntervalbounds_sound e L (E:=E1) (Gamma:=defVars) (fVars:=fVars))
as [iv_e [ err_e [ vR_e [ map_e [eval_real_e bounded_real_e]]]]];
eauto.
repeat destr_factorize.
pose proof (meps_0_deterministic _ eval_real_e H7); subst.
inversion Heqo0; subst.
simpl in *; auto.
* rewrite Nat.eqb_neq in v1_eq.
set_tac.
destruct v1_mem as [? | [? ?]].
{ exfalso; apply v1_eq; auto. }
{ apply fVars_sound ; auto. }
+ intros v1 mem_fVars.
specialize (P_valid v1 mem_fVars).
unfold updEnv.
case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try auto.
rewrite Nat.eqb_eq in case_v1; subst.
assert (NatSet.In n (NatSet.union fVars dVars))
as in_union
by (rewrite NatSet.union_spec; auto).
rewrite <- NatSet.mem_spec in in_union.
rewrite in_union in *; congruence.
+ apply validRangesCmd_swap with (Gamma1 := updDefVars n REAL defVars).
* intros x.
unfold toRMap, updDefVars.
destruct (x =? n) eqn:?; auto.
* destruct valid_intv as [[? valid_cont] ?].
apply valid_cont.
apply swap_Gamma_eval_expr with (Gamma1 := toRMap defVars); try auto.
+ intros v1 v1_mem; set_tac.
unfold updDefVars.
case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try eauto.
......@@ -2390,10 +2343,11 @@ Proof.
destruct v1_mem as [v_fVar | v_dVar]; try auto.
rewrite NatSet.add_spec in v_dVar. destruct v_dVar; try auto.
subst; rewrite Nat.eqb_refl in case_v1; congruence.
+ destruct valid_intv as [[? ?] ?]; auto.
- inversion eval_real; subst.
inversion eval_float; subst.
unfold updEnv; simpl.
unfold validErrorboundCmd in valid_bounds.
simpl in *.
destruct valid_intv as [? ?].
edestruct validErrorbound_sound as [[* [* eval_e]] bounded_e]; eauto.
Qed.
This diff is collapsed.
This diff is collapsed.
......@@ -138,7 +138,7 @@ Theorem validIntervalbounds_sound (f:expr 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 ->
validRanges f A E.
validRanges f A E Gamma.
(* exists iv err vR, *)
(* FloverMap.find f A = Some (iv, err) /\ *)
(* eval_expr E (toRMap Gamma) (toREval (toRExp f)) vR REAL /\ *)
......
......@@ -91,7 +91,6 @@ Proof.
eapply swap_Gamma_eval_expr; eauto.
Qed.
Lemma validRanges_swap Gamma1 Gamma2:
forall e A E,
(forall n, (toRMap Gamma1) n = toRMap (Gamma2) n) ->
......@@ -107,9 +106,9 @@ Proof.
lra]).
- destruct valid1; auto.
- destruct valid1 as [[? [? ?]] ?]; auto.
- admit.
- destruct valid1 as [[? [? ?]] ?]; auto.
- destruct valid1; auto.
Admitted.
Qed.
Fixpoint validRangesCmd (f:cmd Q) A E Gamma {struct f} : Prop :=
match f with
......@@ -133,3 +132,26 @@ Corollary validRangesCmd_single f A E Gamma:
Proof.
destruct f; simpl in *; intros [ _ valid_f]; auto.
Qed.
Lemma validRangesCmd_swap:
forall f A E Gamma1 Gamma2,
(forall n, (toRMap Gamma1) n = toRMap (Gamma2) n) ->
validRangesCmd f A E Gamma1 ->
validRangesCmd f A E Gamma2.
Proof.
induction f; intros * Gamma_swap valid1; simpl in *; try (split; auto);
try (
destruct valid1 as [_ [? [? [? [? [? ?]]]]]];
repeat eexists; eauto;
[eapply swap_Gamma_bstep with (Gamma1 := (toRMap Gamma1)); eauto |
lra |
lra]).
- destruct valid1 as [[? valid_all_exec] ?]; split.
+ eapply validRanges_swap; eauto.
+ intros. eapply IHf; [ | eapply valid_all_exec].
* intros x. unfold updDefVars.
destruct (x =? n) eqn:?; auto.
* eapply swap_Gamma_eval_expr with (Gamma1 := toRMap Gamma2); eauto.
- destruct valid1.
eapply validRanges_swap; eauto.
Qed.
\ No newline at end of file
......@@ -2,7 +2,8 @@ From Coq
Require Import Reals.Reals QArith.Qreals.
From Flover
Require Export Infra.ExpressionAbbrevs ErrorValidation RealRangeValidator.
Require Export Infra.ExpressionAbbrevs ErrorValidation RealRangeValidator
Typing Environments.
Definition RoundoffErrorValidator (e:expr Q) (tMap:FloverMap.t mType) (A:analysisResult) (dVars:NatSet.t) :=
(* if *)
......@@ -12,17 +13,15 @@ Definition RoundoffErrorValidator (e:expr Q) (tMap:FloverMap.t mType) (A:analysi
Theorem RoundoffErrorValidator_sound:
forall (e : expr Q) (E1 E2 : env) (fVars dVars : NatSet.t) (A : analysisResult)
(nR : R) (err : error) (P : precond) (elo ehi : Q) (Gamma : FloverMap.t mType)
(nR : R) (err : error) (elo ehi : Q) (Gamma : FloverMap.t mType)
(defVars : nat -> option mType),
Typing.typeCheck e defVars Gamma = true ->
Environments.approxEnv E1 defVars A fVars dVars E2 ->
typeCheck e defVars Gamma = true ->
approxEnv E1 defVars A fVars dVars E2 ->
NatSet.Subset (usedVars e -- dVars) fVars ->
eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL ->
RoundoffErrorValidator e Gamma A dVars = true ->
RangeValidator e A P dVars = true ->
IntervalValidation.dVars_range_valid dVars E1 A ->
IntervalValidation.fVars_P_sound fVars E1 P ->
IntervalValidation.vars_typed (fVars dVars) defVars ->
validRanges e A E1 defVars ->
vars_typed (fVars dVars) defVars ->
FloverMap.find (elt:=intv * error) e A = Some (elo, ehi, err) ->
(exists (nF : R) (m : mType), eval_expr E2 defVars (toRExp e) nF m) /\
(forall (nF : R) (m : mType), eval_expr E2 defVars (toRExp e) nF m -> (Rabs (nR - nF) <= Q2R err)%R).
......@@ -30,3 +29,33 @@ Proof.
intros. cbn in *.
eapply validErrorbound_sound; eauto.
Qed.
Definition RoundoffErrorValidatorCmd (f:cmd Q) (tMap:FloverMap.t mType) (A:analysisResult) (dVars:NatSet.t) :=
(* if *)
validErrorboundCmd f tMap A dVars.
(*then true *)
(* else validAffineErrorboundsCmd e A tMap dVars ... *)
Theorem RoundoffErrorValidatorCmd_sound f:
forall A E1 E2 outVars fVars dVars vR elo ehi err Gamma defVars,
typeCheckCmd f defVars Gamma = true ->
approxEnv E1 defVars A fVars dVars E2 ->
ssa f (NatSet.union fVars dVars) outVars ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL ->
validErrorboundCmd f Gamma A dVars = true ->
validRangesCmd f A E1 defVars ->
vars_typed (NatSet.union fVars dVars) defVars ->
FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
(exists vF m,
bstep (toRCmd f) E2 defVars vF m) /\
(forall vF mF,
bstep (toRCmd f) E2 defVars vF mF ->
(Rabs (vR - vF) <= (Q2R err))%R).
Proof.
intros.
cbn in *.
split.
- eapply validErrorboundCmd_gives_eval; eauto.
- intros. eapply validErrorboundCmd_sound; eauto.
Qed.
\ No newline at end of file
Require Import Coq.Strings.Ascii Coq.Strings.String Coq.Lists.List Coq.Reals.Reals.
Require Import Coq.Strings.Ascii Coq.Strings.String Coq.Lists.List
Coq.Reals.Reals Coq.Bool.Bool Coq.QArith.QArith.
Require Import CertificateChecker Infra.MachineType.
......
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