Commit 22a9baa7 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Get rid of DeltaMap in type validator

parent 68dc402f
...@@ -54,10 +54,7 @@ Proof. ...@@ -54,10 +54,7 @@ Proof.
unfold CertificateChecker in certificate_valid. unfold CertificateChecker in certificate_valid.
destruct (getValidMap defVars e (FloverMap.empty mType)) eqn:?; try congruence. destruct (getValidMap defVars e (FloverMap.empty mType)) eqn:?; try congruence.
rename t into Gamma. rename t into Gamma.
assert (validTypes e Gamma DeltaMap). assert (validTypes e Gamma).
{ eapply getValidMap_top_correct; eauto.
intros. cbn in *; congruence. }
assert (validTypes e Gamma DeltaMapR).
{ eapply getValidMap_top_correct; eauto. { eapply getValidMap_top_correct; eauto.
intros. cbn in *; congruence. } intros. cbn in *; congruence. }
rewrite <- andb_lazy_alt in certificate_valid. rewrite <- andb_lazy_alt in certificate_valid.
...@@ -84,7 +81,7 @@ Proof. ...@@ -84,7 +81,7 @@ Proof.
exists Gamma; intros approxE1E2. exists Gamma; intros approxE1E2.
assert (dVars_contained NatSet.empty (FloverMap.empty (affine_form Q))) as Hdvars assert (dVars_contained NatSet.empty (FloverMap.empty (affine_form Q))) as Hdvars
by (unfold dVars_contained; intros * Hset; clear - Hset; set_tac). by (unfold dVars_contained; intros * Hset; clear - Hset; set_tac).
pose proof (RoundoffErrorValidator_sound e _ deltas_matched H approxE1E2 H2 eval_real R pose proof (RoundoffErrorValidator_sound e _ deltas_matched H approxE1E2 H1 eval_real R
valid_e map_e Hdvars) as Hsound. valid_e map_e Hdvars) as Hsound.
unfold validErrorBounds in Hsound. unfold validErrorBounds in Hsound.
eapply validErrorBounds_single in Hsound; eauto. eapply validErrorBounds_single in Hsound; eauto.
...@@ -134,10 +131,7 @@ Proof. ...@@ -134,10 +131,7 @@ Proof.
destruct (getValidMapCmd defVars f (FloverMap.empty mType)) eqn:?; destruct (getValidMapCmd defVars f (FloverMap.empty mType)) eqn:?;
try congruence. try congruence.
rename t into Gamma. rename t into Gamma.
assert (validTypesCmd f Gamma DeltaMap). assert (validTypesCmd f Gamma).
{ eapply getValidMapCmd_correct; try eauto.
intros; cbn in *; congruence. }
assert (validTypesCmd f Gamma DeltaMapR).
{ eapply getValidMapCmd_correct; try eauto. { eapply getValidMapCmd_correct; try eauto.
intros; cbn in *; congruence. } intros; cbn in *; congruence. }
exists Gamma; intros approxE1E2. exists Gamma; intros approxE1E2.
......
...@@ -788,7 +788,7 @@ Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVar ...@@ -788,7 +788,7 @@ Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVar
validRanges e A E1 (toRTMap (toRExpMap Gamma)) -> validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorboundAA e Gamma A dVars noise1 expr_map1 = Some (expr_map2, noise2) -> validErrorboundAA e Gamma A dVars noise1 expr_map1 = Some (expr_map2, noise2) ->
NatSet.Subset (usedVars e -- dVars) fVars -> NatSet.Subset (usedVars e -- dVars) fVars ->
validTypes e Gamma DeltaMap -> validTypes e Gamma ->
FloverMap.find e A = Some (iv__A, err__A) -> FloverMap.find e A = Some (iv__A, err__A) ->
(0 < noise1)%nat -> (0 < noise1)%nat ->
(forall n0 : nat, (n0 >= noise1)%nat -> noise_map1 n0 = None) -> (forall n0 : nat, (n0 >= noise1)%nat -> noise_map1 n0 = None) ->
...@@ -3293,7 +3293,7 @@ Theorem validErrorboundAACmd_sound c: ...@@ -3293,7 +3293,7 @@ Theorem validErrorboundAACmd_sound c:
validErrorboundAACmd c Gamma A dVars noise1 expr_map1 = Some (expr_map2, noise2) -> validErrorboundAACmd c Gamma A dVars noise1 expr_map1 = Some (expr_map2, noise2) ->
ssa c (NatSet.union fVars dVars) outVars -> ssa c (NatSet.union fVars dVars) outVars ->
NatSet.Subset (Commands.freeVars c -- dVars) fVars -> NatSet.Subset (Commands.freeVars c -- dVars) fVars ->
validTypesCmd c Gamma DeltaMap -> validTypesCmd c Gamma ->
(0 < noise1)%nat -> (0 < noise1)%nat ->
(forall n0 : nat, (n0 >= noise1)%nat -> noise_map1 n0 = None) -> (forall n0 : nat, (n0 >= noise1)%nat -> noise_map1 n0 = None) ->
dVars_contained dVars expr_map1 -> dVars_contained dVars expr_map1 ->
......
...@@ -75,7 +75,7 @@ Theorem FPRangeValidator_sound: ...@@ -75,7 +75,7 @@ Theorem FPRangeValidator_sound:
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) -> exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 -> approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v m -> eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v m ->
validTypes e Gamma DeltaMap -> validTypes e Gamma ->
validRanges e A E1 (toRTMap (toRExpMap Gamma)) -> validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorBounds e E1 E2 A Gamma DeltaMap -> validErrorBounds e E1 E2 A Gamma DeltaMap ->
FPRangeValidator e A Gamma dVars = true -> FPRangeValidator e A Gamma dVars = true ->
...@@ -89,7 +89,7 @@ Proof. ...@@ -89,7 +89,7 @@ Proof.
intros *. intros *.
unfold FPRangeValidator. unfold FPRangeValidator.
intros. intros.
pose proof (validTypes_single _ _ _ H2) as validT. pose proof (validTypes_single _ _ H2) as validT.
destruct validT as [mE [type_e valid_exec]]. destruct validT as [mE [type_e valid_exec]].
assert (m = mE) by (eapply valid_exec; eauto); subst. assert (m = mE) by (eapply valid_exec; eauto); subst.
rename mE into m. rename mE into m.
...@@ -152,7 +152,7 @@ Lemma FPRangeValidatorCmd_sound (f:cmd Q): ...@@ -152,7 +152,7 @@ Lemma FPRangeValidatorCmd_sound (f:cmd Q):
ssa f (NatSet.union fVars dVars) outVars -> ssa f (NatSet.union fVars dVars) outVars ->
bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR m -> bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR m ->
bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap v m -> bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap v m ->
validTypesCmd f Gamma DeltaMap -> validTypesCmd f Gamma ->
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) -> validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorBoundsCmd f E1 E2 A Gamma DeltaMap -> validErrorBoundsCmd f E1 E2 A Gamma DeltaMap ->
FPRangeValidatorCmd f A Gamma dVars = true -> FPRangeValidatorCmd f A Gamma dVars = true ->
......
...@@ -288,9 +288,9 @@ Proof. ...@@ -288,9 +288,9 @@ Proof.
Qed. Qed.
Lemma typing_expr_64_bit e: Lemma typing_expr_64_bit e:
forall Gamma DeltaMap, forall Gamma,
is64BitEnv Gamma -> is64BitEnv Gamma ->
validTypes e Gamma DeltaMap -> validTypes e Gamma ->
FloverMap.find e Gamma = Some M64. FloverMap.find e Gamma = Some M64.
Proof. Proof.
destruct e; intros * Gamma_64Bit [mG [find_mG ?]]; destruct e; intros * Gamma_64Bit [mG [find_mG ?]];
...@@ -298,9 +298,9 @@ Proof. ...@@ -298,9 +298,9 @@ Proof.
Qed. Qed.
Lemma typing_cmd_64_bit f: Lemma typing_cmd_64_bit f:
forall Gamma DeltaMap, forall Gamma,
is64BitEnv Gamma -> is64BitEnv Gamma ->
validTypesCmd f Gamma DeltaMap -> validTypesCmd f Gamma ->
FloverMap.find (getRetExp f) Gamma = Some M64. FloverMap.find (getRetExp f) Gamma = Some M64.
Proof. Proof.
induction f; intros * Gamma_64BitEnv valid_f. induction f; intros * Gamma_64BitEnv valid_f.
...@@ -404,7 +404,7 @@ Lemma eval_expr_gives_IEEE (e:expr fl64) : ...@@ -404,7 +404,7 @@ Lemma eval_expr_gives_IEEE (e:expr fl64) :
(forall (e' : expr R) (m' : mType), (forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) -> exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
(forall x, (toREnv E2) x = E2_real x) -> (forall x, (toREnv E2) x = E2_real x) ->
validTypes (B2Qexpr e) Gamma DeltaMap -> validTypes (B2Qexpr e) Gamma ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real -> approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real ->
validRanges (B2Qexpr e) A E1 (toRTMap (toRExpMap Gamma)) -> validRanges (B2Qexpr e) A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorBounds (B2Qexpr e) E1 E2_real A Gamma DeltaMap -> validErrorBounds (B2Qexpr e) E1 E2_real A Gamma DeltaMap ->
...@@ -468,7 +468,7 @@ Proof. ...@@ -468,7 +468,7 @@ Proof.
FloverMap.find (B2Qexpr e2) Gamma = Some M64 /\ FloverMap.find (B2Qexpr e2) Gamma = Some M64 /\
FloverMap.find (Binop b (B2Qexpr e1) (B2Qexpr e2)) Gamma = Some M64) FloverMap.find (Binop b (B2Qexpr e1) (B2Qexpr e2)) Gamma = Some M64)
as [tMap_e1 [tMap_e2 tMap_b]]. as [tMap_e1 [tMap_e2 tMap_b]].
{ repeat split; apply (typing_expr_64_bit _ (Gamma := Gamma) DeltaMap); { repeat split; apply (typing_expr_64_bit _ (Gamma := Gamma));
simpl; auto. } simpl; auto. }
assert (m = M64) by congruence; subst. assert (m = M64) by congruence; subst.
pose proof (validTypes_exec _ valid_arg tMap_e1 H6); subst. pose proof (validTypes_exec _ valid_arg tMap_e1 H6); subst.
...@@ -801,7 +801,7 @@ Proof. ...@@ -801,7 +801,7 @@ Proof.
FloverMap.find (B2Qexpr e3) Gamma = Some M64 /\ FloverMap.find (B2Qexpr e3) Gamma = Some M64 /\
FloverMap.find (Fma (B2Qexpr e1) (B2Qexpr e2) (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]]]. as [tMap_e1 [tMap_e2 [tMap_e3 tMap_fma]]].
{ repeat split; apply (typing_expr_64_bit _ (Gamma := Gamma) DeltaMap); simpl; auto. } { repeat split; apply (typing_expr_64_bit _ (Gamma := Gamma)); simpl; auto. }
assert (m = M64) by congruence. assert (m = M64) by congruence.
pose proof (validTypes_exec _ valid_arg tMap_e1 H6); subst. 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_arg0 tMap_e2 H9); subst.
...@@ -827,7 +827,7 @@ Lemma bstep_gives_IEEE (f:cmd fl64) : ...@@ -827,7 +827,7 @@ Lemma bstep_gives_IEEE (f:cmd fl64) :
(forall x, (toREnv E2) x = E2_real x) -> (forall x, (toREnv E2) x = E2_real x) ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real -> approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real ->
ssa (B2Qcmd f) (NatSet.union fVars dVars) outVars -> ssa (B2Qcmd f) (NatSet.union fVars dVars) outVars ->
validTypesCmd (B2Qcmd f) Gamma DeltaMap -> validTypesCmd (B2Qcmd f) Gamma ->
validRangesCmd (B2Qcmd f) A E1 (toRTMap (toRExpMap 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 ->
FPRangeValidatorCmd (B2Qcmd f) A Gamma dVars = true -> FPRangeValidatorCmd (B2Qcmd f) A Gamma dVars = true ->
...@@ -1162,10 +1162,7 @@ Proof. ...@@ -1162,10 +1162,7 @@ Proof.
eapply getValidMap_preserving with (akk:=FloverMap.empty mType); try eauto. eapply getValidMap_preserving with (akk:=FloverMap.empty mType); try eauto.
intros; cbn in *; congruence. } intros; cbn in *; congruence. }
rename t into Gamma. rename t into Gamma.
assert (validTypes (B2Qexpr e) Gamma DeltaMap). assert (validTypes (B2Qexpr e) Gamma).
{ eapply getValidMap_top_correct; eauto.
intros. cbn in *; congruence. }
assert (validTypes (B2Qexpr e) Gamma DeltaMapR).
{ eapply getValidMap_top_correct; eauto. { eapply getValidMap_top_correct; eauto.
intros. cbn in *; congruence. } intros. cbn in *; congruence. }
rewrite <- andb_lazy_alt in certificate_valid. rewrite <- andb_lazy_alt in certificate_valid.
...@@ -1241,10 +1238,7 @@ Proof. ...@@ -1241,10 +1238,7 @@ Proof.
{ unfold is64BitEnv. { unfold is64BitEnv.
eapply getValidMapCmd_preserving with (akk:=FloverMap.empty mType); eauto. eapply getValidMapCmd_preserving with (akk:=FloverMap.empty mType); eauto.
intros; cbn in *; congruence. } intros; cbn in *; congruence. }
assert (validTypesCmd (B2Qcmd f) Gamma DeltaMap). assert (validTypesCmd (B2Qcmd f) Gamma).
{ eapply getValidMapCmd_correct; try eauto.
intros; cbn in *; congruence. }
assert (validTypesCmd (B2Qcmd f) Gamma DeltaMapR).
{ eapply getValidMapCmd_correct; try eauto. { eapply getValidMapCmd_correct; try eauto.
intros; cbn in *; congruence. } intros; cbn in *; congruence. }
exists Gamma; intros approxE1E2. exists Gamma; intros approxE1E2.
......
...@@ -21,7 +21,7 @@ Theorem RoundoffErrorValidator_sound: ...@@ -21,7 +21,7 @@ Theorem RoundoffErrorValidator_sound:
(nR : R) (err : error) (iv : intv) (Gamma : FloverMap.t mType) DeltaMap, (nR : R) (err : error) (iv : intv) (Gamma : FloverMap.t mType) DeltaMap,
(forall (e' : expr R) (m' : mType), (forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) -> exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
validTypes e Gamma DeltaMap -> validTypes e Gamma ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 -> approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
NatSet.Subset (usedVars e -- dVars) fVars -> NatSet.Subset (usedVars e -- dVars) fVars ->
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) nR REAL -> eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) nR REAL ->
...@@ -81,7 +81,7 @@ Theorem RoundoffErrorValidatorCmd_sound f: ...@@ -81,7 +81,7 @@ Theorem RoundoffErrorValidatorCmd_sound f:
dVars_contained dVars (FloverMap.empty (affine_form Q)) -> dVars_contained dVars (FloverMap.empty (affine_form Q)) ->
RoundoffErrorValidatorCmd f Gamma A dVars = true -> RoundoffErrorValidatorCmd f Gamma A dVars = true ->
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) -> validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
validTypesCmd f Gamma DeltaMap -> validTypesCmd f Gamma ->
validErrorBoundsCmd f E1 E2 A Gamma DeltaMap. validErrorBoundsCmd f E1 E2 A Gamma DeltaMap.
Proof. Proof.
intros. intros.
......
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