Commit 71f97008 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Solve admits of approxEnv proofs

parent 453a28ee
......@@ -42,13 +42,16 @@ Proof.
destruct validError_e as (? & ? & ?); eauto.
Qed.
Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop :=
Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap fVars dVars: 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)
approxEnv (updEnv x v__R E1) (toRExpMap Gamma) A fVars
(NatSet.add x dVars) (updEnv x v__FP E2) /\
validErrorBoundsCmd k (updEnv x v__R E1) (updEnv x v__FP E2) A Gamma DeltaMap
fVars (NatSet.add x dVars))
| Ret e => validErrorBounds e E1 E2 A Gamma DeltaMap
end /\
forall v__R (iv: intv) (err: error),
......@@ -60,8 +63,8 @@ Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop :=
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 ->
Lemma validErrorBoundsCmd_single c E1 E2 A Gamma DeltaMap fVars dVars:
validErrorBoundsCmd c E1 E2 A Gamma DeltaMap fVars dVars ->
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) ->
......
......@@ -2426,7 +2426,7 @@ Theorem validErrorboundCmd_sound (f:cmd Q):
validErrorboundCmd f Gamma A dVars = true ->
validTypesCmd f Gamma ->
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorBoundsCmd f E1 E2 A Gamma DeltaMap.
validErrorBoundsCmd f E1 E2 A Gamma DeltaMap fVars dVars.
Proof.
induction f;
intros * deltas_matched approxc1c2 ssa_f freeVars_subset valid_bounds valid_types valid_intv;
......@@ -2454,12 +2454,17 @@ Proof.
rename R into valid_rec.
eapply validTypes_exec in find_me; eauto; subst.
type_conv; subst.
eapply IHf with (fVars := fVars) (outVars := outVars); eauto.
+ eapply approxUpdBound; try eauto; simpl in *.
* eapply toRExpMap_some; eauto.
assert (approxEnv (updEnv n vR E1) (toRExpMap Gamma) A
fVars (NatSet.add n dVars) (updEnv n vF E2)).
{
eapply approxUpdBound; try eauto; simpl in *.
- eapply toRExpMap_some; eauto.
simpl; auto.
* apply Rle_trans with (r2:= Q2R e0); try lra.
- apply Rle_trans with (r2:= Q2R e0); try lra.
eapply bounded_e; eauto.
}
split; auto.
eapply IHf with (fVars := fVars) (outVars := outVars); eauto.
+ eapply ssa_equal_set; eauto.
hnf. intros a; split; intros in_set.
* rewrite NatSet.add_spec, NatSet.union_spec;
......@@ -2491,7 +2496,8 @@ Proof.
subst.
eapply validErrorBounds_single in Hsound; eauto.
destruct Hsound as [[vFe [mFe eval_float_e]] bounded_e].
assert (validErrorBoundsCmd f (updEnv n v E1) (updEnv n v0 E2) A Gamma DeltaMap) as IHf'.
assert (validErrorBoundsCmd f (updEnv n v E1) (updEnv n v0 E2)
A Gamma DeltaMap fVars (NatSet.add n dVars)) as IHf'.
{
apply (IHf A (updEnv n v E1) (updEnv n v0 E2) outVars fVars
(NatSet.add n dVars) Gamma DeltaMap);
......
......@@ -3331,7 +3331,7 @@ Theorem validErrorboundAACmd_sound c:
toInterval (afQ2R af) = ((- err__af)%R, err__af) /\
(err__af <= Q2R err__A)%R /\
af_evals (afQ2R af) (v__R - v__FP) noise_map2 /\
validErrorBoundsCmd c E1 E2 A Gamma DeltaMap /\
validErrorBoundsCmd c E1 E2 A Gamma DeltaMap fVars dVars /\
(forall e' : FloverMap.key,
~ FloverMap.In (elt:=affine_form Q) e' expr_map1 ->
FloverMap.In (elt:=affine_form Q) e' expr_map2 ->
......@@ -3633,7 +3633,11 @@ Proof.
}
edestruct validErrorboundAA_contained_subexpr as (? & ? & ?);
try exact Hvalidbounds'; eauto.
* intros v__R0 v__FP0 Heval__R0 Heval__FP0.
* rename H36 into Heval__R0; rename H37 into Heval__FP0.
apply eval_expr_functional with (v1 := v) in Heval__R0; eauto.
apply eval_expr_functional with (v1 := v__FP) in Heval__FP0; eauto.
subst; auto.
* rename H36 into Heval__R0; rename H37 into Heval__FP0.
apply eval_expr_functional with (v1 := v) in Heval__R0; eauto.
apply eval_expr_functional with (v1 := v__FP) in Heval__FP0; eauto.
subst; auto.
......
......@@ -154,7 +154,7 @@ Lemma FPRangeValidatorCmd_sound (f:cmd Q):
bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap v m ->
validTypesCmd f Gamma ->
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorBoundsCmd f E1 E2 A Gamma DeltaMap ->
validErrorBoundsCmd f E1 E2 A Gamma DeltaMap fVars dVars ->
FPRangeValidatorCmd f A Gamma dVars = true ->
NatSet.Subset (NatSet.diff (freeVars f) dVars) fVars ->
(forall v, NatSet.In v dVars ->
......@@ -184,23 +184,11 @@ Proof.
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))
as [[vF_e [m_e eval_float_e]] err_bounded_e]; eauto.
+ set_tac. split; try auto.
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.
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. }
{ admit. }
* edestruct validerr_rec; eauto.
* eapply ssa_equal_set; eauto.
hnf. intros a; split; intros in_set.
{ rewrite NatSet.add_spec, NatSet.union_spec;
......@@ -209,28 +197,13 @@ Proof.
{ rewrite NatSet.add_spec, NatSet.union_spec in in_set;
rewrite NatSet.union_spec, NatSet.add_spec.
destruct in_set as [P1 | [ P2 | P3]]; auto. }
(*
* eapply (swap_Gamma_bstep (Gamma1 := updDefVars n REAL (toRMap Gamma))); eauto.
eauto using Rmap_updVars_comm.
* apply validRangesCmd_swap with (Gamma1:=updDefVars n REAL Gamma).
{ intros x; unfold toRMap, updDefVars.
destruct (x =? n) eqn:?; auto. }
{ eapply valid_rec. auto. } *)
* edestruct validerr_rec; eauto.
* set_tac; split.
{ split; try auto.
hnf; intros; subst.
apply H6; rewrite NatSet.add_spec; auto. }
{ hnf; intros.
apply H6; rewrite NatSet.add_spec; auto. }
(*
* unfold vars_typed. intros.
unfold updDefVars.
destruct (v2 =? n) eqn:?; eauto.
apply H8. rewrite NatSet.union_spec in *.
destruct H4; try auto.
rewrite NatSet.add_spec in H4.
rewrite Nat.eqb_neq in *.
destruct H4; subst; try congruence; auto. *)
* intros. unfold updEnv.
type_conv; subst.
destruct (v2 =? n) eqn:?; try rewrite Nat.eqb_eq in *;
......@@ -244,4 +217,4 @@ Proof.
rewrite NatSet.add_spec in H5; destruct H5;
auto; subst; congruence. }
- destruct H5. destruct H4. destruct H6. eapply FPRangeValidator_sound; eauto.
Admitted.
Qed.
......@@ -829,7 +829,7 @@ Lemma bstep_gives_IEEE (f:cmd fl64) :
ssa (B2Qcmd f) (NatSet.union fVars dVars) outVars ->
validTypesCmd (B2Qcmd f) Gamma ->
validRangesCmd (B2Qcmd f) A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorBoundsCmd (B2Qcmd f) E1 E2_real A Gamma DeltaMap ->
validErrorBoundsCmd (B2Qcmd f) E1 E2_real A Gamma DeltaMap fVars dVars ->
FPRangeValidatorCmd (B2Qcmd f) A Gamma dVars = true ->
bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR REAL ->
bstep (toRCmd (B2Qcmd f)) (toREnv E2) (toRExpMap Gamma) DeltaMap vF M64 ->
......@@ -913,9 +913,8 @@ Proof.
vR vF_new A fVars (NatSet.add n dVars) outVars); try eauto.
+ intros. unfold toREnv, updFlEnv, updEnv.
destruct (x1 =? n); auto. rewrite <- envs_eq. unfold toREnv; auto.
+ eapply approxUpdBound; eauto.
* eapply toRExpMap_some with (e:=Var Q n); eauto.
* admit.
+ edestruct valid_error_cmd; eauto.
eapply eval_eq_env; eauto.
+ eapply ssa_equal_set; eauto.
hnf; split; intros.
* rewrite NatSet.add_spec, NatSet.union_spec in *.
......
......@@ -82,7 +82,7 @@ Theorem RoundoffErrorValidatorCmd_sound f:
RoundoffErrorValidatorCmd f Gamma A dVars = true ->
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
validTypesCmd f Gamma ->
validErrorBoundsCmd f E1 E2 A Gamma DeltaMap.
validErrorBoundsCmd f E1 E2 A Gamma DeltaMap fVars dVars.
Proof.
intros.
unfold RoundoffErrorValidatorCmd in *.
......
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