Commit ebffbd64 authored by Heiko Becker's avatar Heiko Becker
Browse files

Finish porting to finite maps

parent 5f21b490
......@@ -941,8 +941,17 @@ Proof.
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]. *)
edestruct (validIntervalboundsCmd_sound) as [iv_ret [err_ret [v_ret
[map_ret
[eval_ret bound_ret]]]]];
eauto.
{ cbn. Daisy_compute.
rewrite L0, R4, R3, R2. auto. }
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 with (E1 := updEnv n v0 E1); eauto.
{ eapply validErrorboundCmd_gives_eval with (E1 := updEnv n v0 E1)
(elo:=fst(iv_ret))
(ehi:=snd(iv_ret))
(err:= err_ret); eauto.
- eapply approxUpdBound; eauto.
rewrite Qeq_bool_iff in R1.
eapply Rle_trans; eauto.
......@@ -982,38 +991,38 @@ Proof.
rewrite <- Nat.eqb_neq in H1.
rewrite H1.
apply dVars_sound; auto.
- intros; unfold updEnv.
- unfold fVars_P_sound; intros; unfold updEnv.
destruct (v1 =? n) eqn:?.
+ rewrite Nat.eqb_eq in Heqb; subst; exfalso.
set_tac. apply H26; rewrite NatSet.union_spec; auto.
+ apply fVars_defined; rewrite NatSet.mem_spec in *; auto.
- intros. unfold updDefVars. destruct (v1 =? n) eqn:?.
+ apply fVars_defined; auto.
- unfold IntervalValidation.vars_typed. intros.
unfold updDefVars. destruct (v1 =? n) eqn:?.
+ exists M64; auto.
+ apply vars_typed.
rewrite Nat.eqb_neq in Heqb.
set_tac.
rewrite NatSet.union_spec, NatSet.add_spec in H1.
destruct H1 as [HA |[HB | HC]]; try auto; congruence. }
rewrite NatSet.union_spec.
destruct H1 as [HA |[HB | HC]]; try auto; congruence.
- destruct iv_ret; auto.
}
unfold optionLift. rewrite eval_float_e.
assert (tMap (getRetExp (B2Qcmd f)) = Some M64).
{ eapply typingSoundnessCmd; eauto.
destruct (tMap (B2Qexp e)); destruct (tMap (Var Q n)); try congruence;
andb_to_prop R5; type_conv; auto. }
assert (DaisyMap.find (getRetExp (B2Qcmd f)) tMap= Some M64).
{ eapply typingSoundnessCmd; eauto. }
destruct H1 as [vF_new [m_f bstep_float_new]].
assert (m_f = M64).
{ eapply typing_agrees_cmd; eauto.
destruct (tMap (B2Qexp e));
destruct (tMap (Var Q n)); try congruence; andb_to_prop R5;
type_conv; subst; auto. }
{ eapply typing_agrees_cmd; eauto. }
subst.
destruct (IHf (updEnv n v0 E1) (updFlEnv n v_e E2)
(updEnv n (Q2R (B2Q v_e)) E2_real) (updDefVars n M64 Gamma) tMap
vR vF_new A P fVars (NatSet.add n dVars) outVars); try eauto.
+ intros. unfold toREnv, updFlEnv, updEnv.
destruct (x =? n); auto. rewrite <- envs_eq. unfold toREnv; auto.
+ apply approxUpdBound; auto.
+ eapply approxUpdBound; eauto.
eapply Rle_trans; eauto.
rewrite Qeq_bool_iff in R1; apply Qle_Rle; rewrite R1; lra.
canonize_hyps.
inversion Heqo0; subst.
lra.
+ eapply ssa_equal_set; eauto.
hnf; split; intros.
* rewrite NatSet.add_spec, NatSet.union_spec in *.
......@@ -1022,8 +1031,6 @@ Proof.
* rewrite NatSet.add_spec in H1;
rewrite NatSet.union_spec, NatSet.add_spec in *;
destruct H1; auto. destruct H1; auto.
+ destruct (tMap (B2Qexp e)); destruct (tMap (Var Q n)); try congruence;
andb_to_prop R5; type_conv; auto.
+ eapply (swap_Gamma_bstep (Gamma1:= updDefVars n M0 (toRMap Gamma)));
eauto.
intros; unfold updDefVars, toRMap.
......@@ -1043,79 +1050,59 @@ Proof.
+ destruct bstep_sound as [eval_sound bstep_sound].
rewrite eval_float_e in bstep_sound; unfold optionLift in bstep_sound.
auto.
+ intros; unfold updEnv.
+ unfold dVars_range_valid in *; intros; unfold updEnv.
destruct (v1 =? n) eqn:?.
* set_tac. rewrite Nat.eqb_eq in Heqb; subst.
destruct H1 as [? | [? ?]]; try congruence.
exists v0. edestruct validIntervalbounds_sound as [iv_e [err_e [? [? [? ?]]]]]; eauto.
{ set_tac; split; auto. split; auto.
hnf; intros; subst; set_tac. }
canonize_hyps.
destr_factorize; simpl in *.
exists (q1,q2), e1.
split; try auto.
split; try auto.
simpl in *. rewrite R4, R3 in *.
rewrite <- (meps_0_deterministic _ H4 H17). auto.
* eapply dVars_sound; set_tac.
destruct H1; rewrite Nat.eqb_neq in Heqb; try congruence.
destruct H1; auto.
+ unfold fVars_P_sound. intros; unfold updEnv.
destruct (v1 =? n) eqn:?.
* rewrite Nat.eqb_eq in Heqb; subst; exfalso.
set_tac. apply H26; rewrite NatSet.union_spec; auto.
* apply fVars_defined. auto.
+ intros. unfold updDefVars. destruct (v1 =? n) eqn:?.
+ unfold IntervalValidation.vars_typed.
intros. unfold updDefVars. destruct (v1 =? n) eqn:?.
* exists M64; auto.
* apply vars_typed.
rewrite Nat.eqb_neq in Heqb.
set_tac.
destruct H1 as [HA |HB]; try auto.
rewrite NatSet.add_spec in HB. destruct HB; try auto; congruence.
+ 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).
rewrite Nat.eqb_eq in Heqb; subst.
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.
congruence.
* rewrite Nat.eqb_neq in Heqb.
apply dVars_sound; auto.
rewrite NatSet.union_spec, NatSet.add_spec in H1.
rewrite NatSet.union_spec.
destruct H1 as [HA |[HB | HC]]; try auto; congruence.
+ intros. rewrite NatSet.add_spec in H1; unfold updEnv.
destruct (v1 =? n) eqn:?; destruct H1; subst; try congruence.
* destruct (tMap (Var Q n)) eqn:?; exists (Q2R (B2Q v_e)).
exists m; repeat split; try auto.
* exists (Q2R (B2Q v_e)).
exists M64; repeat split; try auto.
eapply FPRangeValidator_sound; eauto.
{ eapply eval_eq_env; eauto.
rewrite H in *; andb_to_prop R5;
type_conv; subst; auto. }
{ eapply eval_eq_env; eauto. }
{ set_tac. split; try auto.
rewrite NatSet.remove_spec, NatSet.union_spec.
split; try auto.
hnf; intros; subst. apply H26. apply H25; auto. }
{ rewrite H in *; congruence. }
hnf; intros; subst. set_tac. }
* rewrite Nat.eqb_eq in Heqb; subst.
exists (Q2R (B2Q v_e)); rewrite H in *.
destruct (tMap (Var Q n)) eqn:?; try congruence;
andb_to_prop R5; type_conv; subst.
exists M64; repeat split; try auto.
eapply FPRangeValidator_sound; eauto.
{ eapply eval_eq_env; eauto. }
{ set_tac. split; try auto.
rewrite NatSet.remove_spec, NatSet.union_spec.
split; try auto.
hnf; intros; subst. apply H26. apply H25; auto. }
hnf; intros; subst. set_tac. }
* rewrite Nat.eqb_neq in Heqb; congruence.
* apply dVars_valid; auto.
+ intros. unfold updDefVars.
destruct (v1 =? n) eqn:?; try auto.
apply freeVars_typed; set_tac.
rewrite NatSet.remove_spec, NatSet.union_spec; split; try auto.
split; try auto.
hnf; intros; subst; rewrite Nat.eqb_neq in Heqb; congruence.
+ exists x; destruct H1;
split; try auto.
......@@ -1145,38 +1132,40 @@ Theorem IEEE_connection_exp e A P E1 E2 defVars:
NatSet.In v (usedVars (B2Qexp e)) ->
exists m, defVars v = Some m) ->
CertificateChecker (B2Qexp e) A P defVars = true ->
exists vR vF, (* m, currently = M64 *)
exists iv err vR vF, (* m, currently = M64 *)
DaisyMap.find (B2Qexp e) A = Some (iv, err) /\
eval_exp E1 (toRMap defVars) (toREval (toRExp (B2Qexp e))) vR M0 /\
eval_exp_float e E2 = Some vF /\
eval_exp (toREnv E2) defVars (toRExp (B2Qexp e)) (Q2R (B2Q vF)) M64 /\
(Rabs (vR - Q2R (B2Q vF )) <= Q2R (snd (A (B2Qexp e))))%R.
(Rabs (vR - Q2R (B2Q vF )) <= Q2R err)%R.
Proof.
intros.
edestruct Certificate_checking_is_sound; eauto.
- intros. set_tac.
- intros. set_tac.
- destruct H7 as [vF [mF [eval_real [eval_float roundoff_sound]]]].
unfold CertificateChecker in H6.
andb_to_prop H6.
assert (typeMap defVars (B2Qexp e) (B2Qexp e) = Some M64).
destruct H7 as [err [vR [vF [mF [map_e [eval_real [eval_float roundoff_sound]]]]]]].
unfold CertificateChecker in H6.
andb_to_prop H6.
assert (DaisyMap.find (B2Qexp e) (typeMap defVars (B2Qexp e) (DaisyMap.empty mType)) = Some M64).
{ eapply typing_exp_64_bit; eauto. }
assert (mF = M64).
{ eapply typing_agrees_exp; eauto. }
subst.
edestruct eval_exp_gives_IEEE; eauto.
+ set_tac.
+ intros. apply H5. destruct H7; try auto.
+ unfold dVars_range_valid. intros. inversion H7.
+ unfold vars_typed. intros.
apply H5.
set_tac. destruct H7; try auto.
inversion H7.
+ intros. inversion H7.
+ intros. inversion H7.
+ destruct H7 as [eval_float_f eval_rel].
exists x; exists x0. repeat split; try auto.
exists x, err, vR, x0.
repeat split; try auto.
eapply roundoff_sound; eauto.
Qed.
Theorem IEEE_connection_cmd (f:cmd fl64) (absenv:analysisResult) P
Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P
defVars E1 E2:
approxEnv E1 defVars absenv (freeVars (B2Qcmd f)) NatSet.empty (toREnv E2) ->
approxEnv E1 defVars A (freeVars (B2Qcmd f)) NatSet.empty (toREnv E2) ->
is64BitBstep (B2Qcmd f) ->
noDowncastFun (B2Qcmd f) ->
bstep_valid f E2 ->
......@@ -1188,14 +1177,15 @@ Theorem IEEE_connection_cmd (f:cmd fl64) (absenv:analysisResult) P
(forall v, (v) mem (freeVars (B2Qcmd f)) = true ->
exists m : mType,
defVars v = Some m) ->
CertificateCheckerCmd (B2Qcmd f) absenv P defVars = true ->
exists vR vF m,
CertificateCheckerCmd (B2Qcmd f) A P defVars = true ->
exists iv err vR vF m,
DaisyMap.find (getRetExp (B2Qcmd f)) A = Some (iv,err) /\
bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRMap defVars) vR M0 /\
bstep_float f E2 = Some vF /\
bstep (toRCmd (B2Qcmd f)) (toREnv E2) defVars (Q2R (B2Q vF)) m /\
(forall vF m,
bstep (toRCmd (B2Qcmd f)) (toREnv E2) defVars vF m ->
(Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp (B2Qcmd f)))))%R).
(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.
......@@ -1207,12 +1197,13 @@ Proof.
pose proof (validSSA_sound _ _ R0).
destruct H6 as [outVars ssa_f].
edestruct Certificate_checking_cmds_is_sound; eauto.
- intros.
apply H4. set_tac.
- unfold CertificateCheckerCmd.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
- destruct H6 as [vF [m [bstep_real [bstep_float roundoff_sound]]]].
assert (typeMapCmd defVars (B2Qcmd f) (getRetExp (B2Qcmd f)) = Some M64).
- destruct H6 as [err [vR [vF [m [map_ret [bstep_real [bstep_float roundoff_sound]]]]]]].
assert (DaisyMap.find (getRetExp (B2Qcmd f)) (typeMapCmd defVars (B2Qcmd f) (DaisyMap.empty mType)) = Some M64).
{ eapply typing_cmd_64_bit; eauto. }
assert (m = M64).
{ eapply typing_agrees_cmd; eauto. }
......@@ -1220,15 +1211,17 @@ Proof.
edestruct bstep_gives_IEEE; eauto.
+ eapply ssa_equal_set; eauto.
hnf; intros; split; intros; set_tac.
rewrite NatSet.union_spec in H7; destruct H7; try auto.
destruct H7; try auto.
inversion H7.
+ set_tac.
+ intros. apply H4; rewrite NatSet.mem_spec; auto.
+ intros. apply H5. set_tac. destruct H7; try auto.
+ unfold dVars_range_valid. intros.
inversion H7.
+ unfold fVars_P_sound; intros.
apply H4; rewrite NatSet.mem_spec; auto.
+ unfold vars_typed. intros. apply H5. set_tac. destruct H7; try auto.
inversion H7.
+ intros. inversion H7.
+ intros * HA; inversion HA.
+ exists x; exists x0; exists M64.
destruct H7 as [bstep_float2 bstep_rel].
+ destruct H7.
exists x, err, vR, x0, M64.
repeat split; auto.
Qed.
\ No newline at end of file
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