Commit 94297887 authored by Nikita Zyuzin's avatar Nikita Zyuzin

[WIP] Change the proofs to account for DeltaMap[s]

parent 68d4bc7b
......@@ -71,6 +71,8 @@ Ltac prove_fprangeval m v L1 R:=
Theorem FPRangeValidator_sound:
forall (e:expr Q) E1 E2 Gamma DeltaMap v m A fVars dVars,
(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 ->
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v m ->
validTypes e Gamma DeltaMap ->
......@@ -87,12 +89,12 @@ Proof.
intros *.
unfold FPRangeValidator.
intros.
pose proof (validTypes_single _ _ H1) as validT.
pose proof (validTypes_single _ _ _ H2) as validT.
destruct validT as [mE [type_e valid_exec]].
assert (m = mE) by (eapply valid_exec; eauto); subst.
rename mE into m.
unfold validFloatValue.
pose proof (validRanges_single _ _ _ _ H2) as valid_e.
pose proof (validRanges_single _ _ _ _ H3) as valid_e.
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.
......@@ -110,10 +112,10 @@ Proof.
rewrite type_e in *; cbn in *.
- Flover_compute.
destruct (n mem dVars) eqn:?.
+ set_tac. edestruct H6 as [? [? [? [? ?]]]]; eauto.
rewrite H9 in type_e; inversion type_e; subst.
inversion H0; subst.
rewrite H13 in H3; inversion H3; subst.
+ set_tac. edestruct H7 as [? [? [? [? ?]]]]; eauto.
rewrite H10 in type_e; inversion type_e; subst.
inversion H1; subst.
rewrite H14 in H4; inversion H4; subst.
auto.
+ Flover_compute. prove_fprangeval m v L2 R.
- Flover_compute; try congruence.
......@@ -122,15 +124,15 @@ Proof.
- Flover_compute; destruct u; Flover_compute; try congruence.
type_conv; subst.
prove_fprangeval m v L1 R.
- inversion H0; subst.
destruct H1 as [mE [find_mE [[validt_e1 [validt_e2 [m_e1 [m_e2 [find_m1 [find_m2 join_valid]]]]]] _ ]]].
- inversion H1; subst.
destruct H2 as [mE [find_mE [[validt_e1 [validt_e2 [m_e1 [m_e2 [find_m1 [find_m2 join_valid]]]]]] _ ]]].
assert (m_e1 = m1) by (eapply validTypes_exec in find_m1; eauto).
assert (m_e2 = m2) by (eapply validTypes_exec in find_m2; eauto).
subst.
Flover_compute; try congruence.
prove_fprangeval m (perturb (evalBinop b v1 v2) m delta) L1 R.
- inversion H0; subst.
destruct H1 as [mE [find_mE [[validt_e1 [validt_e2 [validt_e3 [m_e1 [m_e2 [m_e3 [find_m1 [find_m2 [find_m3 join_valid]]]]]]]]] _ ]]].
- inversion H1; subst.
destruct H2 as [mE [find_mE [[validt_e1 [validt_e2 [validt_e3 [m_e1 [m_e2 [m_e3 [find_m1 [find_m2 [find_m3 join_valid]]]]]]]]] _ ]]].
assert (m_e1 = m1) by (eapply validTypes_exec in find_m1; eauto).
assert (m_e2 = m2) by (eapply validTypes_exec in find_m2; eauto).
assert (m_e3 = m3) by (eapply validTypes_exec in find_m3; eauto).
......
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