Commit 5f21b490 authored by Heiko Becker's avatar Heiko Becker

Work on finishing finite maps port, finish soundness of IEEE evaluation for expressions

parent ea7e921d
......@@ -598,24 +598,25 @@ Lemma eval_exp_gives_IEEE (e:exp fl64) :
rewrite H21. unfold Z2R, P2R. lra.
unfold perturb.
repeat rewrite B2Q_B2R_eq; auto.
- simpl. rewrite tMap_b, tMap_e1, tMap_e2.
- cbn. Daisy_compute.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
- simpl; rewrite Heqp, Heqp0, Heqp1.
- cbn. Daisy_compute.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
- simpl. rewrite Heqp, Heqp0, Heqp1, tMap_b.
- cbn. Daisy_compute.
inversion Heqo1; inversion Heqo2; subst.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
- simpl. rewrite Heqp, tMap_b.
- cbn. Daisy_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 R2.
apply le_neq_bool_to_lt_prop in L4.
rewrite Heqp1 in *; simpl in *.
destruct L4 as [case_low | case_high]; hnf; intros.
andb_to_prop R3.
apply le_neq_bool_to_lt_prop in L3.
destruct L3 as [case_low | case_high]; hnf; intros.
- rewrite H19 in *.
apply Qlt_Rlt in case_low.
rewrite Q2R0_is_0, Q2R_plus in case_low. lra.
......@@ -623,7 +624,7 @@ Lemma eval_exp_gives_IEEE (e:exp fl64) :
apply Qlt_Rlt in case_high.
rewrite Q2R0_is_0, Q2R_minus in case_high; lra. }
clear H2 H12 dVars_sound dVars_valid usedVars_64bit vars_typed fVars_defined
usedVars_sound R2 R1 L1 L R6 L0 R3 L3 R4 L2 R5 R7 L5 Heqo Heqo0 Heqo1 IHe1
usedVars_sound R2 R1 L1 L R6 L0 R3 R4 L2 R5 R7 L5 Heqo Heqo0 Heqo1 IHe1
IHe2.
pose proof (fexp_correct 53 1024 eq_refl) as fexp_corr.
assert (forall k : Z, (-1022 < k)%Z ->
......@@ -870,19 +871,13 @@ Lemma bstep_gives_IEEE (f:cmd fl64) :
is64BitBstep (B2Qcmd f) ->
noDowncastFun (B2Qcmd f) ->
bstep_valid f E2 ->
(forall v,
NatSet.In v fVars ->
exists vR, E1 v = Some vR /\ Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R ->
(forall v, NatSet.In v fVars \/ NatSet.In v dVars -> exists m, Gamma v = Some m) ->
(forall v,
NatSet.In v dVars ->
exists vR,
E1 v = Some vR /\ Q2R (fst (fst (A (Var Q v)))) <= vR
<= Q2R (snd (fst (A (Var Q v)))))%R ->
dVars_range_valid dVars E1 A ->
fVars_P_sound fVars E1 P ->
vars_typed (NatSet.union fVars dVars) Gamma ->
(forall v,
NatSet.In v dVars ->
exists vF m,
(E2_real v = Some vF /\ tMap (Var Q v) = Some m /\
(E2_real v = Some vF /\ DaisyMap.find (Var Q v) tMap= Some m /\
validFloatValue vF m)) ->
(forall v, NatSet.In v (freeVars (B2Qcmd f)) -> Gamma v = Some M64) ->
exists v,
......@@ -893,24 +888,26 @@ Proof.
intros * 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 nodowncast_f bstep_sound
fVars_defined vars_typed dVars_sound dVars_valid
dVars_sound fVars_defined vars_typed dVars_valid
freeVars_typed;
inversion bstep_float; inversion bstep_real;
cbn in *; Daisy_compute_asm; try congruence; type_conv; subst;
unfold Ltacs.optionLift;
inversion bstep_float; inversion bstep_real;
inversion ssa_f; subst; simpl in *;
repeat (match goal with
| H: _ = true |- _ => andb_to_prop H
end).
- assert (tMap (B2Qexp e) = Some M64).
- assert (DaisyMap.find (B2Qexp e) tMap= Some M64).
{ eapply typing_exp_64_bit; try eauto.
simpl in *; destruct nodowncast_f; auto.
destruct is64_eval; auto.
intros; apply freeVars_typed.
set_tac. rewrite NatSet.remove_spec.
set_tac.
split; [ set_tac | ].
hnf; intros; subst.
apply H26.
apply (H25 n H). }
assert (m = M64).
assert (m1 = M64).
{ eapply typing_agrees_exp; eauto. }
subst.
assert (exists v_e, eval_exp_float e E2 = Some v_e /\
......@@ -928,38 +925,29 @@ Proof.
rewrite NatSet.remove_spec, NatSet.union_spec.
split; try auto.
hnf; intros; subst.
specialize (H25 n H0); set_tac. }
specialize (H25 n H0).
set_tac. apply H26; set_tac. }
destruct eval_float_e as [v_e [eval_float_e eval_rel_e]].
assert (forall v m, eval_exp E2_real Gamma (toRExp (B2Qexp e)) v m ->
Rabs (v0 - v) <= Q2R (snd (A (B2Qexp e))))%R
Rabs (v0 - v) <= Q2R e2)%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.
- intros. apply dVars_sound. rewrite <- NatSet.mem_spec; auto.
- intros. apply fVars_defined. rewrite <- NatSet.mem_spec; auto.
- intros. apply vars_typed.
rewrite <- NatSet.union_spec, <- NatSet.mem_spec; auto.
- instantiate (1:= snd (fst(A (B2Qexp e)))).
instantiate (1:= fst (fst(A (B2Qexp e)))).
destruct (A (B2Qexp e)) eqn:?. simpl.
destruct i; auto. }
assert (Rabs (v0 - (Q2R (B2Q v_e))) <= Q2R( snd (A (B2Qexp e))))%R.
destruct H25; try auto; congruence. }
assert (Rabs (v0 - (Q2R (B2Q v_e))) <= Q2R e2)%R.
{ eapply err_e_valid. eapply eval_eq_env; eauto. }
(* Now construct a new evaluation according to our big-step semantics
using lemma validErrorboundCmd_gives_eval *)
destruct (A (getRetExp (B2Qcmd f))) as [iv_f err_f] eqn:A_f.
destruct iv_f as [ivlo_f ivhi_f].
(* destruct (A (getRetExp (B2Qcmd f))) as [iv_f err_f] eqn:A_f. *)
(* destruct iv_f as [ivlo_f ivhi_f]. *)
assert (exists vF m, bstep (toRCmd (B2Qcmd f)) (updEnv n (Q2R (B2Q v_e)) E2_real) (updDefVars n M64 Gamma) vF m).
{ eapply validErrorboundCmd_gives_eval; eauto.
- destruct (tMap (B2Qexp e)); destruct (tMap (Var Q n)); try congruence;
andb_to_prop R5; inversion H; subst; auto.
{ eapply validErrorboundCmd_gives_eval with (E1 := updEnv n v0 E1); eauto.
- eapply approxUpdBound; eauto.
instantiate (1:= v0).
rewrite Qeq_bool_iff in R1.
eapply Rle_trans; eauto.
apply Qle_Rle. rewrite R1. lra.
canonize_hyps. rewrite <- R1.
inversion Heqo0; subst; lra.
- eapply ssa_equal_set; eauto.
hnf; split; intros.
+ rewrite NatSet.add_spec, NatSet.union_spec in *.
......@@ -978,33 +966,21 @@ Proof.
eauto.
intros; unfold updDefVars, toRMap.
destruct (n0 =? n); auto.
- intros. unfold updEnv. set_tac.
rewrite NatSet.add_spec in H1. destruct (v1 =? n) eqn:?.
destruct H1; subst; try congruence.
+ exists v0; split; try auto.
assert (exists vR, eval_exp E1 (toRMap Gamma) (toREval (toRExp (B2Qexp e))) vR M0 /\
Q2R (fst (fst (A (B2Qexp e)))) <= vR <= Q2R (snd (fst (A (B2Qexp e)))))%R.
{ eapply validIntervalbounds_sound; eauto.
- intros. eapply dVars_sound; rewrite NatSet.mem_spec in *; auto.
- instantiate (1:=fVars).
hnf; intros; rewrite NatSet.diff_spec in *.
destruct H1.
specialize (H25 a H1); rewrite NatSet.union_spec in H25;
destruct H25; try auto; congruence.
- intros; apply fVars_defined. rewrite NatSet.mem_spec in *; auto.
- intros. apply vars_typed.
rewrite NatSet.mem_spec, NatSet.union_spec in *; auto. }
destruct H1 as [vR_e [eval_real_e bounded_e]].
rewrite <- (meps_0_deterministic (toRExp (B2Qexp e)) eval_real_e H17).
split;
destruct bounded_e; eapply Rle_trans; eauto;
apply Qle_Rle.
apply Qeq_bool_iff in R4; rewrite R4; lra.
apply Qeq_bool_iff in R3; rewrite R3; lra.
+ rewrite Nat.eqb_eq in Heqb; subst.
exfalso; apply H26; rewrite NatSet.union_spec; auto.
+ rewrite Nat.eqb_neq in Heqb.
destruct H1; try congruence.
- unfold dVars_range_valid in *. intros. unfold updEnv. set_tac.
destruct H1; subst.
+ exists v0, (q1, q2), e1; split; try eauto.
* rewrite Nat.eqb_refl; auto.
* split; try auto.
edestruct validIntervalbounds_sound
as [iv_e [err_e [v_e' [map_e [? ?]]]]]; eauto.
{ set_tac; split; try auto. split; try auto.
hnf; intros. eapply H26. subst; set_tac. }
simpl. destr_factorize; simpl in *.
canonize_hyps. rewrite <- R4, <- R3.
rewrite <- (meps_0_deterministic _ H17 H1) in H2; auto.
+ destruct H1.
rewrite <- Nat.eqb_neq in H1.
rewrite H1.
apply dVars_sound; auto.
- intros; unfold updEnv.
destruct (v1 =? n) eqn:?.
......
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