Commit c7fc112c authored by Nikita Zyuzin's avatar Nikita Zyuzin

Make the proofs compile at the costs of admits

parent 51a00b83
......@@ -106,8 +106,10 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond)
end.
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P
defVars:
defVars DeltaMap:
forall (E1 E2:env),
(forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
(forall v, NatSet.In v (freeVars f) ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
......@@ -117,21 +119,24 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P
exists iv err vR vF m,
FloverMap.find (getRetExp f) absenv = Some (iv,err) /\
bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR REAL /\
bstep (toRCmd f) E2 (toRExpMap Gamma) vF m /\
bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap vF m /\
(forall vF m,
bstep (toRCmd f) E2 (toRExpMap Gamma) vF m ->
bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap vF m ->
(Rabs (vR - vF) <= Q2R (err))%R).
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
**)
Proof.
intros * P_valid certificate_valid.
intros * deltas_matched P_valid certificate_valid.
unfold CertificateCheckerCmd in certificate_valid.
destruct (getValidMapCmd defVars f (FloverMap.empty mType)) eqn:?;
try congruence.
rename t into Gamma.
assert (validTypesCmd f Gamma).
assert (validTypesCmd f Gamma DeltaMap).
{ eapply getValidMapCmd_correct; try eauto.
intros; cbn in *; congruence. }
assert (validTypesCmd f Gamma DeltaMapR).
{ eapply getValidMapCmd_correct; try eauto.
intros; cbn in *; congruence. }
exists Gamma; intros approxE1E2.
......
......@@ -288,9 +288,9 @@ Proof.
Qed.
Lemma typing_expr_64_bit e:
forall Gamma,
forall Gamma DeltaMap,
is64BitEnv Gamma ->
validTypes e Gamma ->
validTypes e Gamma DeltaMap ->
FloverMap.find e Gamma = Some M64.
Proof.
destruct e; intros * Gamma_64Bit [mG [find_mG ?]];
......@@ -298,15 +298,15 @@ Proof.
Qed.
Lemma typing_cmd_64_bit f:
forall Gamma,
forall Gamma DeltaMap,
is64BitEnv Gamma ->
validTypesCmd f Gamma ->
validTypesCmd f Gamma DeltaMap ->
FloverMap.find (getRetExp f) Gamma = Some M64.
Proof.
induction f; intros * Gamma_64BitEnv valid_f.
- destruct valid_f as [(? & ? & ? & ? & ? & ?) ?].
eapply IHf; eauto.
- destruct valid_f; simpl in *; eapply typing_expr_64_bit; auto.
- destruct valid_f; simpl in *; eapply typing_expr_64_bit; eauto.
Qed.
Lemma round_0_zero:
......@@ -400,35 +400,37 @@ Qed.
(* (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53) *)
(* (-1022)%Z 53%Z) *)
Lemma eval_expr_gives_IEEE (e:expr fl64) :
forall E1 E2 E2_real Gamma vR A fVars dVars,
forall E1 E2 E2_real Gamma DeltaMap vR A fVars dVars,
(forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
(forall x, (toREnv E2) x = E2_real x) ->
validTypes (B2Qexpr e) Gamma ->
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 ->
FPRangeValidator (B2Qexpr e) A Gamma dVars = true ->
eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp (B2Qexpr e)) vR M64 ->
eval_expr (toREnv E2) (toRExpMap Gamma) DeltaMap (toRExp (B2Qexpr e)) vR M64 ->
NatSet.Subset ((usedVars (B2Qexpr e)) -- dVars) fVars ->
is64BitEval (B2Qexpr e) ->
is64BitEnv Gamma ->
noDowncast (B2Qexpr e) ->
eval_expr_valid e E2 ->
(forall v,
(forall v,
NatSet.In v dVars ->
exists vF m,
(E2_real v = Some vF /\ FloverMap.find (Var Q v) Gamma = Some m /\
validFloatValue vF m)) ->
exists v,
eval_expr_float e E2 = Some v /\
eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp (B2Qexpr e)) (Q2R (B2Q v)) M64.
(E2_real v = Some vF /\ FloverMap.find (Var Q v) Gamma = Some m /\
validFloatValue vF m)) ->
exists v,
eval_expr_float e E2 = Some v /\
eval_expr (toREnv E2) (toRExpMap Gamma) DeltaMap (toRExp (B2Qexpr e)) (Q2R (B2Q v)) M64.
Proof.
Opaque validTypes.
induction e; simpl in *;
intros * envs_eq typecheck_e approxEnv_E1_E2_real valid_rangebounds
valid_roundoffs valid_float_ranges eval_e_float
usedVars_sound is64BitTEnv is64BitEval_e noDowncast_e
eval_IEEE_valid_e dVars_sound;
(match_pat (eval_expr _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
intros * deltas_matched envs_eq typecheck_e approxEnv_E1_E2_real valid_rangebounds
valid_roundoffs valid_float_ranges eval_e_float
usedVars_sound is64BitTEnv is64BitEval_e noDowncast_e
eval_IEEE_valid_e dVars_sound;
(match_pat (eval_expr _ _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
revert eval_IEEE_valid_e;
Flover_compute_asm; try congruence; type_conv; subst;
unfold optionBind;
......@@ -440,9 +442,8 @@ Proof.
exists f; split; try eauto.
eapply Var_load; try auto. rewrite HE2; auto.
- eexists; split; try eauto.
eapply (Const_dist') with (delta:=0%R); eauto.
+ rewrite Rabs_R0; apply mTypeToR_pos_R.
+ unfold perturb. lra.
eapply (Const_dist') with (delta := delta); eauto.
admit.
- destruct valid_rangebounds as [valid_e valid_intv].
destruct m eqn:?; cbn in *; try congruence.
subst.
......@@ -465,28 +466,29 @@ Proof.
FloverMap.find (B2Qexpr e2) Gamma = Some M64 /\
FloverMap.find (Binop b (B2Qexpr e1) (B2Qexpr e2)) Gamma = Some M64)
as [tMap_e1 [tMap_e2 tMap_b]].
{ repeat split; apply (typing_expr_64_bit _ (Gamma := Gamma)); simpl; auto. }
{ repeat split; apply (typing_expr_64_bit _ (Gamma := Gamma) DeltaMap);
simpl; auto. }
(*
- cbn in typecheck_e; Flover_compute; auto;
intros; apply usedVars_64bit; set_tac.
- intros; apply usedVars_64bit; set_tac. } *)
assert (m = M64) by congruence; subst.
pose proof (validTypes_exec _ valid_arg tMap_e1 H5); subst.
pose proof (validTypes_exec _ valid_arg0 tMap_e2 H8); subst.
destruct (IHe1 E1 E2 E2_real Gamma v1 A fVars dVars)
pose proof (validTypes_exec _ valid_arg tMap_e1 H6); subst.
pose proof (validTypes_exec _ valid_arg0 tMap_e2 H9); subst.
destruct (IHe1 E1 E2 E2_real Gamma DeltaMap v1 A fVars dVars)
as [v_e1 [eval_float_e1 eval_rel_e1]];
try auto; try set_tac.
destruct (IHe2 E1 E2 E2_real Gamma v2 A fVars dVars)
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 _ _ _ _ H15) as valid_e.
pose proof (validRanges_single _ _ _ _ H16) 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.
destr_factorize.
destruct iv_2 as [ivlo_2 ivhi_2].
assert (forall vF2 m2,
eval_expr E2_real (toRExpMap Gamma) (toRExp (B2Qexpr e2)) 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. }
assert (contained (Q2R (B2Q v_e2))
......@@ -494,7 +496,7 @@ Proof.
(Q2R ivlo_2, Q2R ivhi_2) (Q2R err_2))).
{ eapply distance_gives_iv.
- simpl. eapply e2_bounded_real.
- eapply H16. instantiate(1:=M64).
- eapply H17. instantiate(1:=M64).
eapply eval_eq_env; eauto. }
assert (b = Div -> (Q2R (B2Q v_e2)) <> 0%R).
{ intros; subst; simpl in *.
......@@ -503,24 +505,23 @@ Proof.
rewrite Heqo2 in *.
destruct i1; symmetry in map_e2; inversion map_e2; subst.
destruct L3; hnf; intros.
- rewrite H19 in *.
apply Qlt_Rlt in H18.
rewrite Q2R0_is_0, Q2R_plus in H18. simpl in *; lra.
- rewrite H19 in *.
apply Qlt_Rlt in H18.
rewrite Q2R0_is_0, Q2R_minus in H18; simpl in *; lra. }
- 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. }
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:=0%R); eauto.
+ rewrite Rabs_R0. apply mTypeToR_pos_R.
+ unfold perturb; lra.
eapply Binop_dist' with (delta:=delta); eauto.
admit.
- repeat split; try auto.
+ intros ? iv2 err2 find. subst.
destruct iv2; rewrite find in *;
eapply H12; eauto.
eapply H13; eauto.
+ rewrite Heqo0. auto.
- Flover_compute.
apply Is_true_eq_true.
......@@ -553,11 +554,12 @@ Proof.
+ simpl in H2. Transparent mTypeToQ. unfold mTypeToQ.
eapply Rle_trans; eauto.
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 H12; eauto.
eapply H13; eauto.
+ rewrite Heqo0. auto.
- cbn. Flover_compute.
apply Is_true_eq_true.
......@@ -571,10 +573,10 @@ Proof.
andb_to_prop R3.
apply le_neq_bool_to_lt_prop in L3.
destruct L3 as [case_low | case_high]; hnf; intros.
- rewrite H23 in *.
- rewrite H24 in *.
apply Qlt_Rlt in case_low.
rewrite Q2R0_is_0, Q2R_plus in case_low. lra.
- rewrite H23 in *.
- 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
......@@ -597,7 +599,7 @@ Proof.
{ revert H1; intros case_val.
destruct case_val as [eval_is_zero | eval_normal]; try auto.
left; unfold Normal, Denormal in H15; unfold Normal;
destruct H19 as [normal_b | [denormal_b |zero_b]].
destruct H20 as [normal_b | [denormal_b |zero_b]].
- repeat rewrite <- B2Q_B2R_eq; try auto.
- destruct denormal_b.
assert ((Rabs (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2)))) < (Rabs (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2)))))%R.
......@@ -617,7 +619,7 @@ Proof.
unfold IZR in eval_normal.
simpl in eval_normal. rewrite <- INR_IPR in eval_normal.
simpl in eval_normal. lra. }
pose proof (validValue_bounded b v_e1 v_e2 H2 H22) as cond_valid.
pose proof (validValue_bounded b v_e1 v_e2 H2 H23) as cond_valid.
destruct b; revert H1; intros case_eval.
(* Addition *)
+ unfold evalBinop in *. unfold b64_plus.
......@@ -634,10 +636,12 @@ Proof.
split; try auto.
rewrite B2Q_B2R_eq; try auto.
unfold dmode; rewrite add_round.
eapply Binop_dist' with (delta:=0%R); eauto.
{ rewrite Rabs_R0; apply mTypeToR_pos_R. }
eapply Binop_dist' with (delta:=delta); eauto.
{ unfold perturb, evalBinop. cbn.
repeat rewrite B2Q_B2R_eq; try auto; lra. }
repeat rewrite B2Q_B2R_eq; try auto.
symmetry.
apply Rmult_eq_0_compat_r.
lra. }
{ eapply toRExpMap_some; eauto. simpl; auto. }
* simpl in *.
destruct (rel_error_exists
......@@ -654,6 +658,7 @@ Proof.
unfold dmode.
eapply Binop_dist' with (delta:=eps); eauto.
- cbn; lra.
- admit.
- unfold perturb, evalBinop.
repeat rewrite B2Q_B2R_eq; try auto.
rewrite <- round_eq. rewrite <- add_round; auto.
......@@ -673,10 +678,12 @@ Proof.
split; try auto.
rewrite B2Q_B2R_eq; try auto.
unfold dmode; rewrite add_round.
eapply Binop_dist' with (delta:=0%R); eauto.
{ rewrite Rabs_R0; apply mTypeToR_pos_R. }
eapply Binop_dist' with (delta:=delta); eauto.
{ unfold perturb, evalBinop; cbn.
repeat rewrite B2Q_B2R_eq; try auto; lra. }
repeat rewrite B2Q_B2R_eq; try auto.
symmetry.
apply Rmult_eq_0_compat_r.
lra. }
{ eapply toRExpMap_some; try eauto. simpl; auto. }
* simpl in *.
destruct (rel_error_exists
......@@ -693,6 +700,7 @@ Proof.
unfold dmode.
eapply Binop_dist' with (delta:=eps); eauto.
- cbn; lra.
- admit.
- unfold perturb, evalBinop; cbn.
repeat rewrite B2Q_B2R_eq; try auto.
rewrite <- round_eq. rewrite <- add_round; auto.
......@@ -712,10 +720,12 @@ Proof.
split; try auto.
rewrite B2Q_B2R_eq; try auto.
unfold dmode; rewrite mult_round.
eapply Binop_dist' with (delta:=0%R); eauto.
{ rewrite Rabs_R0; apply mTypeToR_pos_R. }
eapply Binop_dist' with (delta:=delta); eauto.
{ unfold perturb, evalBinop; cbn.
repeat rewrite B2Q_B2R_eq; try auto; lra. }
repeat rewrite B2Q_B2R_eq; try auto.
symmetry.
apply Rmult_eq_0_compat_r.
lra. }
{ eapply toRExpMap_some; try eauto. simpl; auto. }
{ rewrite finite_e1, finite_e2 in finite_res.
auto. }
......@@ -734,6 +744,7 @@ Proof.
unfold dmode.
eapply Binop_dist' with (delta:=eps); eauto.
- cbn; lra.
- admit.
- unfold perturb, evalBinop.
repeat rewrite B2Q_B2R_eq; try auto.
rewrite <- round_eq. rewrite <- mult_round; auto.
......@@ -755,10 +766,12 @@ Proof.
split; try auto.
rewrite B2Q_B2R_eq; try auto.
unfold dmode; rewrite div_round.
eapply Binop_dist' with (delta:=0%R); eauto.
{ rewrite Rabs_R0; apply mTypeToR_pos_R. }
eapply Binop_dist' with (delta:=delta); eauto.
{ unfold perturb, evalBinop; cbn.
repeat rewrite B2Q_B2R_eq; try auto; lra. }
repeat rewrite B2Q_B2R_eq; try auto.
symmetry.
apply Rmult_eq_0_compat_r.
lra. }
{ eapply toRExpMap_some; try eauto. simpl; auto. }
{ rewrite finite_e1 in finite_res; auto. }
* simpl in *.
......@@ -776,6 +789,7 @@ Proof.
unfold dmode.
eapply Binop_dist' with (delta:=eps); eauto.
- cbn; lra.
- admit.
- unfold perturb, evalBinop.
repeat rewrite B2Q_B2R_eq; try auto.
rewrite <- round_eq. rewrite <- div_round; auto.
......@@ -789,36 +803,38 @@ Proof.
FloverMap.find (B2Qexpr e3) Gamma = Some M64 /\
FloverMap.find (Fma (B2Qexpr e1) (B2Qexpr e2) (B2Qexpr e3)) Gamma = Some M64)
as [tMap_e1 [tMap_e2 [tMap_e3 tMap_fma]]].
{ repeat split; apply (typing_expr_64_bit _ (Gamma := Gamma)); simpl; auto. }
{ repeat split; apply (typing_expr_64_bit _ (Gamma := Gamma) DeltaMap); simpl; auto. }
assert (m = M64) by congruence.
pose proof (validTypes_exec _ valid_arg tMap_e1 H5); subst.
pose proof (validTypes_exec _ valid_arg0 tMap_e2 H8); subst.
pose proof (validTypes_exec _ valid_arg1 tMap_e3 H9); subst.
destruct (IHe1 E1 E2 E2_real Gamma v1 A fVars dVars)
pose proof (validTypes_exec _ valid_arg tMap_e1 H6); subst.
pose proof (validTypes_exec _ valid_arg0 tMap_e2 H9); subst.
pose proof (validTypes_exec _ valid_arg1 tMap_e3 H10); subst.
destruct (IHe1 E1 E2 E2_real Gamma DeltaMap v1 A fVars dVars)
as [v_e1 [eval_float_e1 eval_rel_e1]];
try auto; try set_tac.
destruct (IHe2 E1 E2 E2_real Gamma v2 A fVars dVars)
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.
destruct (IHe3 E1 E2 E2_real Gamma v3 A fVars dVars)
destruct (IHe3 E1 E2 E2_real Gamma DeltaMap v3 A fVars dVars)
as [v_e3 [eval_float_e3 eval_rel_e3]];
try auto; try set_tac.
rewrite eval_float_e1, eval_float_e2, eval_float_e3 in H6.
contradiction H6.
rewrite eval_float_e1, eval_float_e2, eval_float_e3 in H7.
contradiction H7.
- inversion noDowncast_e.
Qed.
Admitted.
Lemma bstep_gives_IEEE (f:cmd fl64) :
forall E1 E2 E2_real Gamma vR vF A fVars dVars outVars,
forall E1 E2 E2_real Gamma DeltaMap vR vF A fVars dVars outVars,
(forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
(forall x, (toREnv E2) x = E2_real x) ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real ->
ssa (B2Qcmd f) (NatSet.union fVars dVars) outVars ->
validTypesCmd (B2Qcmd f) Gamma ->
validTypesCmd (B2Qcmd f) Gamma DeltaMap ->
validRangesCmd (B2Qcmd f) A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorboundCmd (B2Qcmd f) Gamma A dVars = true ->
FPRangeValidatorCmd (B2Qcmd f) A Gamma dVars = true ->
bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRTMap (toRExpMap Gamma)) vR REAL ->
bstep (toRCmd (B2Qcmd f)) (toREnv E2) (toRExpMap Gamma) vF M64 ->
bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR REAL ->
bstep (toRCmd (B2Qcmd f)) (toREnv E2) (toRExpMap Gamma) DeltaMap vF M64 ->
NatSet.Subset (NatSet.diff (freeVars (B2Qcmd f)) dVars) fVars ->
is64BitBstep (B2Qcmd f) ->
is64BitEnv Gamma ->
......@@ -831,10 +847,10 @@ Lemma bstep_gives_IEEE (f:cmd fl64) :
validFloatValue vF m)) ->
exists v,
bstep_float f E2 = Some v /\
bstep (toRCmd (B2Qcmd f)) (toREnv E2) (toRExpMap Gamma) (Q2R (B2Q v)) M64.
bstep (toRCmd (B2Qcmd f)) (toREnv E2) (toRExpMap Gamma) DeltaMap (Q2R (B2Q v)) M64.
Proof.
induction f;
intros * envs_eq approxEnv_E1_E2_real ssa_f typeCheck_f valid_ranges_f
intros * deltas_matched envs_eq approxEnv_E1_E2_real ssa_f typeCheck_f valid_ranges_f
valid_roundoffs_f valid_float_ranges bstep_real bstep_float
freeVars_sound is64_eval is64_env nodowncast_f bstep_sound
dVars_valid ;
......@@ -852,27 +868,28 @@ Proof.
type_conv; subst.
assert (FloverMap.find (B2Qexpr e) Gamma = Some M64).
{ eapply typing_expr_64_bit; eauto. }
pose proof (validTypes_exec _ validt_e H H7); subst.
pose proof (validTypes_exec _ validt_e H H8); subst.
assert (exists v_e, eval_expr_float e E2 = Some v_e /\
eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp (B2Qexpr e)) (Q2R (B2Q v_e)) M64)
eval_expr (toREnv E2) (toRExpMap Gamma) DeltaMap
(toRExp (B2Qexpr e)) (Q2R (B2Q v_e)) M64)
as eval_float_e.
{ eapply eval_expr_gives_IEEE; try eauto.
- destruct valid_ranges_f as [[? ?] ?]; auto.
- hnf; intros. rewrite NatSet.diff_spec in H0.
destruct H0.
specialize (H25 a H0). rewrite NatSet.union_spec in H25.
destruct H25; try congruence; auto.
specialize (H27 a H0). rewrite NatSet.union_spec in H27.
destruct H27; try congruence; auto.
- destruct is64_eval; auto.
- destruct nodowncast_f; auto.
- destruct bstep_sound; auto. }
destruct eval_float_e as [v_e [eval_float_e eval_rel_e]].
assert (forall v m, eval_expr E2_real (toRExpMap Gamma) (toRExp (B2Qexpr e)) v m ->
assert (forall v m, eval_expr E2_real (toRExpMap Gamma) DeltaMap (toRExp (B2Qexpr e)) v m ->
Rabs (v0 - v) <= Q2R e0)%R
as err_e_valid.
{ eapply validErrorbound_sound; try eauto.
- hnf; intros. rewrite NatSet.diff_spec in H0.
destruct H0. specialize (H25 a H0). rewrite NatSet.union_spec in H25.
destruct H25; try auto; congruence.
destruct H0. specialize (H27 a H0). rewrite NatSet.union_spec in H27.
destruct H27; try auto; congruence.
- unfold eval_Real. destruct valid_ranges_f as [[? ?] ?]; auto.
- instantiate (1:= snd i). instantiate (1:=fst i).
destruct i; simpl in *; auto. }
......@@ -885,7 +902,7 @@ Proof.
assert (exists vF m,
bstep (toRCmd (B2Qcmd f))
(updEnv n (Q2R (B2Q v_e)) E2_real)
(toRExpMap Gamma) vF m).
(toRExpMap Gamma) DeltaMap vF m).
{ eapply validErrorboundCmd_gives_eval with (E1 := updEnv n v0 E1)
(elo:=fst(iv_ret))
(ehi:=snd(iv_ret))
......@@ -933,7 +950,7 @@ Proof.
destruct H1 as [vF_new [m_f bstep_float_new]].
assert (m_f = M64) by (eapply bstep_Gamma_det; eauto); subst.
destruct (IHf (updEnv n v0 E1) (updFlEnv n v_e E2)
(updEnv n (Q2R (B2Q v_e)) E2_real) Gamma
(updEnv n (Q2R (B2Q v_e)) E2_real) Gamma DeltaMap
vR vF_new A fVars (NatSet.add n dVars) outVars); try eauto.
+ intros. unfold toREnv, updFlEnv, updEnv.
destruct (x =? n); auto. rewrite <- envs_eq. unfold toREnv; auto.
......@@ -1156,7 +1173,7 @@ Proof.
- eapply getValidMap_preserving with (akk:=akk); eauto.
Qed.
Theorem IEEE_connection_expr e A P E1 E2 defVars:
Theorem IEEE_connection_expr e A P E1 E2 defVars DeltaMap:
is64BitEval (B2Qexpr e) ->
is64BitEnv defVars ->
noDowncast (B2Qexpr e) ->
......@@ -1171,9 +1188,9 @@ Theorem IEEE_connection_expr e A P E1 E2 defVars:
approxEnv E1 Gamma A (usedVars (B2Qexpr e)) (NatSet.empty) (toREnv E2) ->
exists iv err vR vF,
FloverMap.find (B2Qexpr e) A = Some (iv, err) /\
eval_expr E1 (toRTMap Gamma) (toREval (toRExp (B2Qexpr e))) vR REAL /\
eval_expr E1 (toRTMap Gamma) DeltaMapR (toREval (toRExp (B2Qexpr e))) vR REAL /\
eval_expr_float e E2 = Some vF /\
eval_expr (toREnv E2) Gamma (toRExp (B2Qexpr e)) (Q2R (B2Q vF)) M64 /\
eval_expr (toREnv E2) Gamma DeltaMap (toRExp (B2Qexpr e)) (Q2R (B2Q vF)) M64 /\
(Rabs (vR - Q2R (B2Q vF )) <= Q2R err)%R.
Proof.
intros * is64eval is64bitenv no_cast eval_valid P_valid certificate_valid.
......@@ -1184,7 +1201,7 @@ Proof.
eapply getValidMap_preserving with (akk:=FloverMap.empty mType); try eauto.
intros; cbn in *; congruence. }
rename t into Gamma.
assert (validTypes (B2Qexpr e) Gamma).
assert (validTypes (B2Qexpr e) Gamma DeltaMapR).
{ eapply getValidMap_top_correct; eauto.
intros. cbn in *; congruence. }
rewrite <- andb_lazy_alt in certificate_valid.
......@@ -1225,7 +1242,9 @@ Proof.
Admitted.
Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P
defVars E1 E2:
defVars E1 E2 DeltaMap:
(forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
is64BitBstep (B2Qcmd f) ->
is64BitEnv defVars ->
noDowncastFun (B2Qcmd f) ->
......@@ -1238,14 +1257,15 @@ Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P
approxEnv E1 (toRExpMap Gamma) A (freeVars (B2Qcmd f)) NatSet.empty (toREnv E2) ->
exists iv err vR vF m,
FloverMap.find (getRetExp (B2Qcmd f)) A = Some (iv,err) /\
bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR REAL /\
bstep_float f E2 = Some vF /\
bstep (toRCmd (B2Qcmd f)) (toREnv E2) (toRExpMap Gamma) (Q2R (B2Q vF)) m /\
bstep (toRCmd (B2Qcmd f)) (toREnv E2) (toRExpMap Gamma) DeltaMap (Q2R (B2Q vF)) m /\
(forall vF m,
bstep (toRCmd (B2Qcmd f)) (toREnv E2) (toRExpMap Gamma) vF m ->
bstep (toRCmd (B2Qcmd f)) (toREnv E2) (toRExpMap Gamma) DeltaMap vF m ->
(Rabs (vR - vF) <= Q2R err)%R).
Proof.
intros * is64bitBstep is64BitEnv_def noDowncast bstep_valid P_valid certificate_valid.
intros * deltas_matched is64bitBstep is64BitEnv_def noDowncast bstep_valid
P_valid certificate_valid.
unfold CertificateCheckerCmd in certificate_valid.
destruct (getValidMapCmd defVars (B2Qcmd f) (FloverMap.empty mType)) eqn:?;
try congruence.
......@@ -1254,7 +1274,10 @@ Proof.
{ unfold is64BitEnv.
eapply getValidMapCmd_preserving with (akk:=FloverMap.empty mType); eauto.
intros; cbn in *; congruence. }
assert (validTypesCmd (B2Qcmd f) Gamma).
assert (validTypesCmd (B2Qcmd f) Gamma DeltaMap).
{ eapply getValidMapCmd_correct; try eauto.
intros; cbn in *; congruence. }
assert (validTypesCmd (B2Qcmd f) Gamma DeltaMapR).
{ eapply getValidMapCmd_correct; try eauto.
intros; cbn in *; congruence. }
exists Gamma; intros approxE1E2.
......@@ -1292,6 +1315,6 @@ Proof.
edestruct bstep_gives_IEEE; eauto.
- admit.
- intros; set_tac.
- destruct H2.
- destruct H3.
repeat eexists; eauto.
Admitted.
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