Skip to content

GitLab

F
FloVer
Commit 97e83312 authored by Nikita Zyuzin's avatar Nikita Zyuzin
Browse files
Options

Continue adopting deterministic rounding semantics

parent dd226fbe
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 542 additions and 224 deletions
coq/CertificateChecker.v
View file @ 97e83312
......@@ -87,9 +87,10 @@ Proof.
pose proof (RoundoffErrorValidator_sound e _ deltas_matched H approxE1E2 H2 eval_real R
valid_e map_e Hdvars) as Hsound.
unfold validErrorBounds in Hsound.
(* destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto. *)
(* exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto. *)
Admitted.
eapply validErrorBounds_single in Hsound; eauto.
destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto.
exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto.
Qed.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond)
defVars :=
......@@ -162,6 +163,9 @@ Proof.
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; [admit|].
pose proof RoundoffErrorValidatorCmd_sound as Hsound.
eapply validErrorBoundsCmd_single in Hsound; eauto.
2: unfold dVars_contained; intros; set_tac.
specialize Hsound as ((vF & mF & eval_float) & ?).
exists (f_lo, f_hi), err, vR, vF, mF; repeat split; try auto.
Admitted.
Qed.
coq/ErrorAnalysis.v
View file @ 97e83312
......@@ -2,7 +2,7 @@ From Coq
Require Import Reals.Reals QArith.Qreals.
From Flover
Require Import ExpressionSemantics Environments RealRangeArith TypeValidator.
Require Import Commands ExpressionSemantics Environments RealRangeArith TypeValidator.
Fixpoint validErrorBounds (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
(match e with
......@@ -29,7 +29,7 @@ Fixpoint validErrorBounds (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
Lemma validErrorBounds_single e E1 E2 A Gamma DeltaMap:
validErrorBounds e E1 E2 A Gamma DeltaMap ->
forall v__R iv err,
eval_expr E1 (toRTMap (toRExpMap Gamma)) (fun x m => Some 0%R) (toREval (toRExp e)) v__R REAL ->
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
FloverMap.find e A = Some (iv, err) ->
(exists v__FP m__FP,
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
......@@ -41,3 +41,37 @@ Proof.
intros; destruct e; cbn in *; split;
destruct validError_e as (? & ? & ?); eauto.
Qed.
Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop :=
match c with
| Let m x e k => validErrorBounds e E1 E2 A Gamma DeltaMap /\
(forall v__R v__FP,
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m ->
validErrorBoundsCmd k (updEnv x v__R E1) (updEnv x v__FP E2) A Gamma DeltaMap)
| Ret e => validErrorBounds e E1 E2 A Gamma DeltaMap
end /\
forall v__R (iv: intv) (err: error),
bstep (toREvalCmd (toRCmd c)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR v__R REAL ->
FloverMap.find (getRetExp c) A = Some (iv, err) ->
(exists v__FP m__FP,
bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP) /\
(forall v__FP m__FP,
bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP ->
(Rabs (v__R - v__FP) <= (Q2R err))%R).
Lemma validErrorBoundsCmd_single c E1 E2 A Gamma DeltaMap:
validErrorBoundsCmd c E1 E2 A Gamma DeltaMap ->
forall v__R (iv: intv) (err: error),
bstep (toREvalCmd (toRCmd c)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR v__R REAL ->
FloverMap.find (getRetExp c) A = Some (iv, err) ->
(exists v__FP m__FP,
bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP) /\
(forall v__FP m__FP,
bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP ->
(Rabs (v__R - v__FP) <= (Q2R err))%R).
Proof.
intros validError_e;
intros; destruct c; cbn in *; split;
destruct validError_e as (? & ? & ?); eauto.
Qed.
coq/ErrorValidation.v
View file @ 97e83312
This diff is collapsed.
coq/ErrorValidationAA.v
View file @ 97e83312
......@@ -5087,3 +5087,128 @@ Proof.
intuition.
eauto.
Qed.
Fixpoint contained_command_subexpr (c: cmd Q) (expr_map: FloverMap.t (affine_form Q)): Prop :=
match c with
| Let m x e c => contained_subexpr e expr_map /\ contained_command_subexpr c expr_map
| Ret e => contained_subexpr e expr_map
end.
Lemma validErrorBoundAACmd_contained_command_subexpr c Gamma A fVars dVars outVars
noise1 expr_map1 noise2 expr_map2:
(forall e', FloverMap.In e' expr_map1 ->
contained_subexpr e' expr_map1) ->
(forall n, NatSet.In n dVars -> FloverMap.In (Var Q n) expr_map1) ->
ssa c (NatSet.union fVars dVars) outVars ->
NatSet.Subset (Commands.freeVars c -- dVars) fVars ->
validErrorboundAACmd c Gamma A dVars noise1 expr_map1 = Some (expr_map2, noise2) ->
contained_flover_map expr_map1 expr_map2 /\
contained_command_subexpr c expr_map2.
Proof.
revert dVars expr_map1 expr_map2 noise1 noise2.
induction c; intros * Hsubexpr Hdvars Hssa Hsubset Hvalid; cbn in *.
- destruct (validErrorboundAA e Gamma A dVars noise1 expr_map1) eqn: Hvalid__e;
cbn in Hvalid; [|congruence].
destruct p as (expr_map', noise').
destruct (FloverMap.find e expr_map') eqn: Hein; cbn in Hvalid; [|congruence].
destruct (FloverMap.find e A) eqn: Hecert; cbn in Hvalid; [|congruence].
destruct p as (?, ?).
destruct (FloverMap.find (Var Q n) A) eqn: Hvarcert; cbn in Hvalid; [|congruence].
destruct p as (?, ?).
destruct (Qeq_bool e0 e1) eqn: Heq; cbn in Hvalid; [|congruence].
destruct (FloverMap.find (Var Q n) expr_map') eqn: Hvarin; cbn in Hvalid; [congruence|].
pose proof (validErrorboundAA_contained_subexpr _ _ _ _ Hsubexpr Hdvars Hvalid__e) as Hcont.
specialize Hcont as (Hcont__e & Hcontf' & Hconte').
inversion Hssa; subst.
assert (contained_flover_map (FloverMap.add (Var Q n) a expr_map') expr_map2 /\
contained_command_subexpr c expr_map2) as (H1 & H2).
{
eapply IHc with (dVars := NatSet.add n dVars); eauto.
- intros.
destruct (q_expr_eq_dec (Var Q n) e').
+ eapply contained_subexpr_eq_compat; eauto.
cbn.
split; auto.
apply flover_map_in_add.
+ rewrite FloverMapFacts.P.F.add_neq_in_iff in H; auto.
destruct (flover_map_in_dec e' expr_map1).
* eapply contained_subexpr_map_extension; eauto.
etransitivity; try apply Hcontf'; eauto.
now apply contained_flover_map_extension.
* apply contained_subexpr_add_compat; auto.
- intros n__e Hn__e.
set_tac.
destruct Hn__e.
+ subst.
apply flover_map_in_add.
+ specialize H as (_ & ?).
eapply flover_map_in_extension; eauto.
etransitivity; try apply Hcontf'; eauto.
now apply contained_flover_map_extension.
- assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars))
(NatSet.union fVars (NatSet.add n dVars))) as Hseteq.
{
hnf. intros ?; split; intros in_set; set_tac.
- destruct in_set as [ ? | [? ?]]; try auto; set_tac.
destruct H0; auto.
- destruct in_set as [? | ?]; try auto; set_tac.
destruct H as [? | [? ?]]; auto.
}
eapply ssa_equal_set; symmetry in Hseteq.
exact Hseteq.
assumption.
- hnf. intros ? a_freeVar.
rewrite NatSet.diff_spec in a_freeVar.
destruct a_freeVar as [a_freeVar a_no_dVar].
apply Hsubset.
simpl.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
repeat split; try auto.
{ hnf; intros; subst.
apply a_no_dVar.
rewrite NatSet.add_spec; auto. }
{ hnf; intros a_dVar.
apply a_no_dVar.
rewrite NatSet.add_spec; auto. }
}
split; [|split]; auto.
+ etransitivity; eauto.
etransitivity; eauto.
apply contained_flover_map_extension; auto.
+ eapply contained_subexpr_map_extension; eauto.
eapply contained_subexpr_map_extension; eauto.
apply contained_flover_map_extension; auto.
- pose proof (validErrorboundAA_contained_subexpr _ _ _ _ Hsubexpr Hdvars Hvalid) as Hcont.
intuition.
Qed.
Lemma validErrorboundAACmd_validErrorBoundsCmd c:
forall E1 E2 A Gamma DeltaMap fVars dVars outVars
(expr_map1 expr_map2 : FloverMap.t (affine_form Q))
(noise_map1 : nat -> option noise_type) (noise1 noise2 : nat),
(forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
validRangesCmd c A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorboundAACmd c Gamma A dVars noise1 expr_map1 = Some (expr_map2, noise2) ->
ssa c (NatSet.union fVars dVars) outVars ->
NatSet.Subset (Commands.freeVars c -- dVars) fVars ->
validTypesCmd c Gamma DeltaMap ->
(0 < noise1)%nat ->
(forall n0 : nat, (n0 >= noise1)%nat -> noise_map1 n0 = None) ->
dVars_contained dVars expr_map1 ->
(forall e' : FloverMap.key,
FloverMap.In (elt:=affine_form Q) e' expr_map1 ->
NatSet.Subset (usedVars e') (NatSet.union fVars dVars) /\
exists (v__FP' : R) (m__FP' : mType),
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP') ->
(forall e' : FloverMap.key,
FloverMap.In (elt:=affine_form Q) e' expr_map1 ->
checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map1 noise1 expr_map1) ->
validErrorBoundsCmd c E1 E2 A Gamma DeltaMap.
Proof.
induction c;
intros * Hdeltamap Henv Hrange Hvalidbounds Hssa Hsubset Htypes Hnoise1
Hnoise_map1 Hdvars Hcheckedex Hcheckedall.
Admitted.
coq/FPRangeValidator.v
View file @ 97e83312
From Flover
Require Import Expressions Commands Environments ssaPrgs TypeValidator
IntervalValidation ErrorValidation Infra.Ltacs Infra.RealRationalProps.
IntervalValidation RoundoffErrorValidator Infra.Ltacs Infra.RealRationalProps.
Fixpoint FPRangeValidator (e:expr Q) (A:analysisResult) typeMap dVars {struct e}
: bool :=
......@@ -77,7 +77,7 @@ Theorem FPRangeValidator_sound:
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v m ->
validTypes e Gamma DeltaMap ->
validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorbound e Gamma A dVars = true ->
validErrorBounds e E1 E2 A Gamma DeltaMap ->
FPRangeValidator e A Gamma dVars = true ->
NatSet.Subset (NatSet.diff (usedVars e) dVars) fVars ->
(forall v, NatSet.In v dVars ->
......@@ -98,7 +98,7 @@ Proof.
destruct valid_e as [iv_e [err_e [vR[ map_e[eval_real vR_bounded]]]]].
destruct iv_e as [e_lo e_hi].
assert (Rabs (vR - v) <= Q2R (err_e))%R.
{ eapply validErrorbound_sound; eauto. }
{ eapply validErrorBounds_single; eauto. }
destruct (distance_gives_iv (a:=vR) v (e:=Q2R err_e) (Q2R e_lo, Q2R e_hi))
as [v_in_errIv];
try auto.
......@@ -113,15 +113,15 @@ Proof.
- Flover_compute.
destruct (n mem dVars) eqn:?.
+ set_tac. edestruct H7 as [? [? [? [? ?]]]]; eauto.
rewrite H10 in type_e; inversion type_e; subst.
rewrite H11 in type_e; inversion type_e; subst.
inversion H1; subst.
rewrite H14 in H4; inversion H4; subst.
rewrite H15 in H10; inversion H10; subst.
auto.
+ Flover_compute. prove_fprangeval m v L2 R.
+ Flover_compute. prove_fprangeval m v L1 R.
- Flover_compute; try congruence.
type_conv; subst.
prove_fprangeval m v L1 R.
- Flover_compute; destruct u; Flover_compute; try congruence.
- Flover_compute; try congruence.
type_conv; subst.
prove_fprangeval m v L1 R.
- inversion H1; subst.
......@@ -154,7 +154,7 @@ Lemma FPRangeValidatorCmd_sound (f:cmd Q):
bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap v m ->
validTypesCmd f Gamma DeltaMap ->
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorboundCmd f Gamma A dVars = true ->
validErrorBoundsCmd f E1 E2 A Gamma DeltaMap ->
FPRangeValidatorCmd f A Gamma dVars = true ->
NatSet.Subset (NatSet.diff (freeVars f) dVars) fVars ->
(forall v, NatSet.In v dVars ->
......@@ -180,7 +180,11 @@ Proof.
pose proof (validRanges_single _ _ _ _ valid_e) as valid_e_single.
destruct valid_e_single
as [iv_e [err_e [vR_e [map_e [eval_e_real bounded_vR_e]]]]].
destr_factorize.
destruct H6 as ((validerr_e & validerr_rec) & validerr_single).
pose proof (validErrorBounds_single _ _ _ _ validerr_e) as validerr_e_single.
specialize (validerr_e_single v0 iv_e err_e H19 map_e) as
((vF_e & m_e & eval_float_e) & err_bounded_e).
(* destr_factorize.
edestruct (validErrorbound_sound (e:=e) (E1:=E1) (E2:=E2) (fVars:=fVars)
(dVars := dVars) (A:=A)
(nR:=v0) (err:=err_e) (elo:=fst iv_e) (ehi:=snd iv_e))
......@@ -189,19 +193,14 @@ Proof.
split; try auto.
hnf; intros; subst; set_tac.
+ destruct iv_e; auto.
+ rewrite <- (meps_0_deterministic (toRExp e) eval_e_real H19) in *; try auto.
+ *)
rewrite <- (meps_0_deterministic (toRExp e) eval_e_real H19) in *; try auto.
apply (IHf (updEnv n vR_e E1) (updEnv n v1 E2)
Gamma DeltaMap v vR m0 A fVars
(NatSet.add n dVars) (outVars)); eauto.
* eapply approxUpdBound; eauto; simpl in *.
{ eapply toRExpMap_some; eauto. simpl; auto. }
{ apply Rle_trans with (r2:= Q2R err_e); try lra.
eapply err_bounded_e. eauto.
apply Qle_Rle.
rewrite Qeq_bool_iff in *.
destruct i0; inversion Heqo0; subst.
rewrite R1.
lra. }
{ admit. }
* eapply ssa_equal_set; eauto.
hnf. intros a; split; intros in_set.
{ rewrite NatSet.add_spec, NatSet.union_spec;
......@@ -244,5 +243,5 @@ Proof.
{ apply H9.
rewrite NatSet.add_spec in H5; destruct H5;
auto; subst; congruence. }
- destruct H5. destruct H4. eapply FPRangeValidator_sound; eauto.
Qed.
- destruct H5. destruct H4. destruct H6. eapply FPRangeValidator_sound; eauto.
Admitted.
coq/IEEE_connection.v
View file @ 97e83312
......@@ -4,7 +4,7 @@ From Coq
From Flover
Require Import Expressions Infra.RationalSimps TypeValidator IntervalValidation
ErrorValidation CertificateChecker FPRangeValidator Environments
ErrorAnalysis CertificateChecker FPRangeValidator Environments
Infra.RealRationalProps Commands Infra.Ltacs.
From Flocq
......@@ -407,7 +407,7 @@ Lemma eval_expr_gives_IEEE (e:expr fl64) :
validTypes (B2Qexpr e) Gamma DeltaMap ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real ->
validRanges (B2Qexpr e) A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorbound (B2Qexpr e) Gamma A dVars = true ->
validErrorBounds (B2Qexpr e) E1 E2_real A Gamma DeltaMap ->
FPRangeValidator (B2Qexpr e) A Gamma dVars = true ->
eval_expr (toREnv E2) (toRExpMap Gamma) DeltaMap (toRExp (B2Qexpr e)) vR M64 ->
NatSet.Subset ((usedVars (B2Qexpr e)) -- dVars) fVars ->
......@@ -443,14 +443,24 @@ Proof.
eapply Var_load; try auto. rewrite HE2; auto.
- eexists; split; try eauto.
eapply (Const_dist') with (delta := delta); eauto.
assert (forall e m delta v,
eval_expr_float e E2 = Some v ->
eval_expr (toREnv E2) (toRExpMap Gamma) DeltaMap (toRExp (B2Qexpr e)) (Q2R (B2Q v)) m ->
DeltaMap (toRExp (B2Qexpr e)) m = Some delta ->
delta = 0%R) by admit.
cbn.
admit.
- destruct valid_rangebounds as [valid_e valid_intv].
destruct m eqn:?; cbn in *; try congruence.
subst.
edestruct IHe as [v_e [eval_float_e eval_rel_e]]; eauto.
{
intuition.
}
assert (is_finite 53 1024 v_e = true).
{ apply validValue_is_finite.
eapply FPRangeValidator_sound with (e:=B2Qexpr e); eauto.
2: intuition.
eapply eval_eq_env; eauto. }
(* - cbn in typecheck_e; Flover_compute; auto. } *)
rewrite eval_float_e.
......@@ -459,6 +469,7 @@ Proof.
rewrite B2Q_B2R_eq; auto. rewrite B2R_Bopp.
eapply Unop_neg'; eauto.
unfold evalUnop. rewrite is_finite_Bopp in H. rewrite B2Q_B2R_eq; auto.
- admit.
- repeat (match goal with
|H: _ /\ _ |- _ => destruct H
end).
......@@ -481,58 +492,64 @@ Proof.
destruct (IHe2 E1 E2 E2_real Gamma DeltaMap v2 A fVars dVars)
as [v_e2 [eval_float_e2 eval_rel_e2]];
try auto; try set_tac.
pose proof (validRanges_single _ _ _ _ H16) as valid_e.
pose proof (validRanges_single _ _ _ _ H19) as valid_e.
destruct valid_e as [iv_2 [err_2 [nR2 [map_e2 [eval_real_e2 e2_bounded_real]]]]].
rewrite eval_float_e1, eval_float_e2.
inversion Heqo1; subst.
(* inversion Heqo1; subst. *)
destr_factorize.
destruct iv_2 as [ivlo_2 ivhi_2].
assert (forall vF2 m2,
eval_expr E2_real (toRExpMap Gamma) DeltaMap (toRExp (B2Qexpr e2)) vF2 m2 ->
(Rabs (nR2 - vF2) <= Q2R err_2))%R.
{ eapply validErrorbound_sound; try eauto; set_tac. }
{ eapply validErrorBounds_single; try eauto; set_tac. }
assert (contained (Q2R (B2Q v_e2))
(widenInterval
(Q2R ivlo_2, Q2R ivhi_2) (Q2R err_2))).
{ eapply distance_gives_iv.
- simpl. eapply e2_bounded_real.
- eapply H17. instantiate(1:=M64).
- eapply H20. instantiate(1:=M64).
eapply eval_eq_env; eauto. }
assert (b = Div -> (Q2R (B2Q v_e2)) <> 0%R).
{ intros; subst; simpl in *.
andb_to_prop R3.
apply le_neq_bool_to_lt_prop in L3.
rewrite Heqo2 in *.
destruct i1; symmetry in map_e2; inversion map_e2; subst.
destruct L3; hnf; intros.
- rewrite H20 in *.
apply Qlt_Rlt in H19.
rewrite Q2R0_is_0, Q2R_plus in H19. simpl in *; lra.
- rewrite H20 in *.
apply Qlt_Rlt in H19.
rewrite Q2R0_is_0, Q2R_minus in H19; simpl in *; lra. }
{
(* intros; subst; simpl in *. *)
(* andb_to_prop R3. *)
(* apply le_neq_bool_to_lt_prop in L3. *)
(* rewrite Heqo2 in *. *)
(* destruct i1; symmetry in map_e2; inversion map_e2; subst. *)
(* destruct L3; hnf; intros. *)
(* - rewrite H20 in *. *)
(* apply Qlt_Rlt in H19. *)
(* rewrite Q2R0_is_0, Q2R_plus in H19. simpl in *; lra. *)
(* - rewrite H20 in *. *)
(* apply Qlt_Rlt in H19. *)
(* rewrite Q2R0_is_0, Q2R_minus in H19; simpl in *; lra. *)
admit.
}
assert (validFloatValue
(evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2))) M64).
{ eapply (FPRangeValidator_sound (Binop b (B2Qexpr e1) (B2Qexpr e2)));
try eauto; set_tac.
- eapply eval_eq_env; eauto.
eapply Binop_dist' with (delta:=delta); eauto.
cbn.
admit.
- repeat split; try auto.
+ intros ? iv2 err2 find. subst.
destruct iv2; rewrite find in *;
eapply H13; eauto.
+ rewrite Heqo0. auto.
- Flover_compute.
apply Is_true_eq_true.
repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
rewrite Heqo2 in map_e2; destruct i0; inversion map_e2; subst.
apply andb_prop_intro; split; apply Is_true_eq_left; try auto.
rewrite L4, R1. auto.
admit.
(* + intros ? iv2 err2 find. subst. *)
(* destruct iv2; rewrite find in *; *)
(* eapply H13; eauto. *)
(* + rewrite Heqo0. auto. *)
- admit.
(* Flover_compute. *)
(* apply Is_true_eq_true. *)
(* repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left. *)
(* rewrite Heqo2 in map_e2; destruct i0; inversion map_e2; subst. *)
(* apply andb_prop_intro; split; apply Is_true_eq_left; try auto. *)
(* rewrite L4, R1. auto. *)
- Flover_compute.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left. }
rewrite Heqo2 in map_e2; destruct i0; inversion map_e2; subst.
(* rewrite Heqo2 in map_e2; destruct i0; inversion map_e2; subst. *)
assert (validFloatValue (Q2R (B2Q v_e1)) M64).
{ eapply (FPRangeValidator_sound (B2Qexpr e1)); try eauto; try set_tac.
eapply eval_eq_env; eauto. }
......@@ -556,32 +573,38 @@ Proof.
simpl. lra.
+ admit.
+ unfold perturb. repeat rewrite B2Q_B2R_eq; try auto.
- cbn; repeat split; try auto.
+ intros ? iv2 err2 find. subst.
destruct iv2; rewrite find in *;
eapply H13; eauto.
+ rewrite Heqo0. auto.
- admit.
(* cbn; repeat split; try auto. *)
(* + intros ? iv2 err2 find. subst. *)
(* destruct iv2; rewrite find in *; *)
(* eapply H13; eauto. *)
(* + rewrite Heqo0. auto. *)
- admit.
- cbn. Flover_compute.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
- cbn. Flover_compute.
inversion Heqo1; inversion Heqo2; subst.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left). }
(* - cbn. Flover_compute. *)
(* inversion Heqo1; inversion Heqo2; subst. *)
(* apply Is_true_eq_true. *)
(* repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left). *)
}
assert (b = Div -> (Q2R (B2Q v_e2)) <> 0%R) as no_div_zero_float.
{ intros; subst; simpl in *.
andb_to_prop R3.
apply le_neq_bool_to_lt_prop in L3.
destruct L3 as [case_low | case_high]; hnf; intros.
- rewrite H24 in *.
apply Qlt_Rlt in case_low.
rewrite Q2R0_is_0, Q2R_plus in case_low. lra.
- rewrite H24 in *.
apply Qlt_Rlt in case_high.
rewrite Q2R0_is_0, Q2R_minus in case_high; lra. }
clear H2 H12 dVars_sound usedVars_sound R2 R1 L1 L
L0 R3 L2 Heqo Heqo0 Heqo1 IHe1
IHe2.
{
(* intros; subst; simpl in *. *)
(* andb_to_prop R3. *)
(* apply le_neq_bool_to_lt_prop in L3. *)
(* destruct L3 as [case_low | case_high]; hnf; intros. *)
(* - rewrite H24 in *. *)
(* apply Qlt_Rlt in case_low. *)
(* rewrite Q2R0_is_0, Q2R_plus in case_low. lra. *)
(* - rewrite H24 in *. *)
(* apply Qlt_Rlt in case_high. *)
(* rewrite Q2R0_is_0, Q2R_minus in case_high; lra. *)
admit.
}
(* clear H2 H12 dVars_sound usedVars_sound R2 R1 L1 L *)
(* L0 R3 L2 Heqo Heqo0 Heqo1 IHe1 *)
(* IHe2. *)
pose proof (fexp_correct 53 1024 eq_refl) as fexpr_corr.
assert (forall k : Z, (-1022 < k)%Z ->
(53 <= k - Fcore_FLT.FLT_exp (3 - 1024 - 53) 53 k)%Z)
......
coq/RoundoffErrorValidator.v
View file @ 97e83312
......@@ -34,7 +34,7 @@ Proof.
unfold RoundoffErrorValidator.
intros; cbn in *.
destruct (validErrorbound e Gamma A dVars) eqn: Hivvalid.
- admit.
- eapply validErrorbound_sound; eauto.
- destruct (validErrorboundAA e Gamma A dVars 1 (FloverMap.empty (affine_form Q))) eqn: Hafvalid;
[|congruence].
destruct p as (expr_map, noise).
......@@ -58,7 +58,7 @@ Proof.
[now rewrite FloverMapFacts.P.F.empty_in_iff|].
split; eauto.
eapply Hall; eauto; now rewrite FloverMapFacts.P.F.empty_in_iff.
Admitted.
Qed.
Definition RoundoffErrorValidatorCmd (f:cmd Q) (tMap:FloverMap.t mType)
(A:analysisResult) (dVars:NatSet.t) :=
......@@ -71,26 +71,31 @@ Definition RoundoffErrorValidatorCmd (f:cmd Q) (tMap:FloverMap.t mType)
end.
Theorem RoundoffErrorValidatorCmd_sound f:
forall A E1 E2 outVars fVars dVars vR elo ehi err Gamma DeltaMap,
forall A E1 E2 outVars fVars dVars Gamma DeltaMap,
(forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
approxEnv E1 (toRExpMap Gamma) 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 (toRTMap (toRExpMap Gamma)) DeltaMapR vR REAL ->
validErrorboundCmd f Gamma A dVars = true ->
dVars_contained dVars (FloverMap.empty (affine_form Q)) ->
RoundoffErrorValidatorCmd f Gamma A dVars = true ->
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
validTypesCmd f Gamma DeltaMap ->
FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
(exists vF m,
bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap vF m) /\
(forall vF mF,
bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap vF mF ->
(Rabs (vR - vF) <= (Q2R err))%R).
validErrorBoundsCmd f E1 E2 A Gamma DeltaMap.
Proof.
intros.
cbn in *.
split.
- eapply validErrorboundCmd_gives_eval; eauto.
- intros. eapply validErrorboundCmd_sound; eauto.
unfold RoundoffErrorValidatorCmd in *.
destruct (validErrorboundCmd f Gamma A dVars) eqn: Hivvalid.
- eapply validErrorboundCmd_sound; eauto.
- destruct (validErrorboundAACmd f Gamma A dVars 1 (FloverMap.empty (affine_form Q)))
eqn: Hvalid; [|congruence].
destruct p as (expr_map2, noise2).
eapply validErrorboundAACmd_validErrorBoundsCmd with
(expr_map1 := FloverMap.empty (affine_form Q)) (noise1 := 1%nat)
(expr_map2 := expr_map2) (noise2 := noise2)
(noise_map1 := fun x => None); eauto.
+ intros ? Hin.
now rewrite FloverMapFacts.P.F.empty_in_iff in Hin.
+ intros ? Hin.
now rewrite FloverMapFacts.P.F.empty_in_iff in Hin.
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