Commit 51a00b83 authored by Nikita Zyuzin's avatar Nikita Zyuzin

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

parent 94297887
...@@ -29,7 +29,9 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult) ...@@ -29,7 +29,9 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
the real valued execution respects the precondition. the real valued execution respects the precondition.
**) **)
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVars: Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVars:
forall (E1 E2:env), forall (E1 E2:env) DeltaMap,
(forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
(forall v, NatSet.In v (Expressions.usedVars e) -> (forall v, NatSet.In v (Expressions.usedVars e) ->
exists vR, E1 v = Some vR /\ exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
...@@ -38,21 +40,24 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVa ...@@ -38,21 +40,24 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVa
approxEnv E1 (toRExpMap Gamma) absenv (usedVars e) NatSet.empty E2 -> approxEnv E1 (toRExpMap Gamma) absenv (usedVars e) NatSet.empty E2 ->
exists iv err vR vF m, exists iv err vR vF m,
FloverMap.find e absenv = Some (iv, err) /\ FloverMap.find e absenv = Some (iv, err) /\
eval_expr E1 (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) vR REAL /\ eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) vR REAL /\
eval_expr E2 (toRExpMap Gamma) (toRExp e) vF m /\ eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m /\
(forall vF m, (forall vF m,
eval_expr E2 (toRExpMap Gamma) (toRExp e) vF m -> eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R. (Rabs (vR - vF) <= Q2R err))%R.
(** (**
The proofs is a simple composition of the soundness proofs for the range The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator. validator and the error bound validator.
**) **)
Proof. Proof.
intros * P_valid certificate_valid. intros * deltas_matched P_valid certificate_valid.
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). assert (validTypes e Gamma DeltaMap).
{ 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.
...@@ -77,12 +82,9 @@ Proof. ...@@ -77,12 +82,9 @@ Proof.
destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]]. destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].
destruct iv_e as [elo ehi]. destruct iv_e as [elo ehi].
exists Gamma; intros approxE1E2. exists Gamma; intros approxE1E2.
rewrite <- eval_expr_REAL_det_nondet in eval_real.
assert (forall (e' : expr Rdefinitions.R) (m' : mType),
exists d, (fun e m => Some 0%R) e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) as Htmp by admit.
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 _ Htmp H approxE1E2 H1 eval_real R pose proof (RoundoffErrorValidator_sound e _ deltas_matched H approxE1E2 H2 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.
(* destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto. *) (* destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto. *)
...@@ -114,7 +116,7 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P ...@@ -114,7 +116,7 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P
approxEnv E1 (toRExpMap Gamma) absenv (freeVars f) NatSet.empty E2 -> approxEnv E1 (toRExpMap Gamma) absenv (freeVars f) NatSet.empty E2 ->
exists iv err vR vF m, exists iv err vR vF m,
FloverMap.find (getRetExp f) absenv = Some (iv,err) /\ FloverMap.find (getRetExp f) absenv = Some (iv,err) /\
bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\ bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR REAL /\
bstep (toRCmd f) E2 (toRExpMap Gamma) vF m /\ bstep (toRCmd f) E2 (toRExpMap Gamma) vF m /\
(forall vF m, (forall vF m,
bstep (toRCmd f) E2 (toRExpMap Gamma) vF m -> bstep (toRCmd f) E2 (toRExpMap Gamma) vF m ->
......
...@@ -145,36 +145,38 @@ Proof. ...@@ -145,36 +145,38 @@ Proof.
Qed. Qed.
Lemma FPRangeValidatorCmd_sound (f:cmd Q): Lemma FPRangeValidatorCmd_sound (f:cmd Q):
forall E1 E2 Gamma v vR m A fVars dVars outVars, forall E1 E2 Gamma DeltaMap v vR m A fVars dVars outVars,
(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 -> approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
ssa f (NatSet.union fVars dVars) outVars -> ssa f (NatSet.union fVars dVars) outVars ->
bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) vR m -> bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR m ->
bstep (toRCmd f) E2 (toRExpMap Gamma) v m -> bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap v m ->
validTypesCmd f Gamma -> validTypesCmd f Gamma DeltaMap ->
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) -> validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorboundCmd f Gamma A dVars = true -> validErrorboundCmd f Gamma A dVars = true ->
FPRangeValidatorCmd f A Gamma dVars = true -> FPRangeValidatorCmd f A Gamma dVars = true ->
NatSet.Subset (NatSet.diff (freeVars f) dVars) fVars -> NatSet.Subset (NatSet.diff (freeVars f) dVars) fVars ->
(forall v, NatSet.In v dVars -> (forall v, NatSet.In v dVars ->
exists vF m, E2 v = Some vF /\ exists vF m, E2 v = Some vF /\
FloverMap.find (Var Q v) Gamma = Some m /\ FloverMap.find (Var Q v) Gamma = Some m /\
validFloatValue vF m) -> validFloatValue vF m) ->
validFloatValue v m. validFloatValue v m.
Proof. Proof.
induction f; intros; induction f; intros;
simpl in *; simpl in *;
(match_pat (bstep _ _ (toRTMap _) _ _) (fun H => inversion H; subst; simpl in * )); (match_pat (bstep _ _ (toRTMap _) _ _ _) (fun H => inversion H; subst; simpl in * ));
(match_pat (bstep _ _ (toRExpMap Gamma) _ _) (fun H => inversion H; subst; simpl in * )); (match_pat (bstep _ _ (toRExpMap Gamma) _ _ _) (fun H => inversion H; subst; simpl in * ));
repeat match goal with repeat match goal with
| H : _ = true |- _ => andb_to_prop H | H : _ = true |- _ => andb_to_prop H
end. end.
- destruct H3 - destruct H4
as [[me [find_me [find_var [? [validt_e validt_f]]]]] valid_exec]. as [[me [find_me [find_var [? [validt_e validt_f]]]]] valid_exec].
assert (m = me) by (eapply validTypes_exec in find_me; eauto); subst. assert (m = me) by (eapply validTypes_exec in find_me; eauto); subst.
rename me into m. rename me into m.
match_pat (ssa _ _ _) (fun H => inversion H; subst; simpl in * ). match_pat (ssa _ _ _) (fun H => inversion H; subst; simpl in * ).
Flover_compute. Flover_compute.
destruct H4 as [[valid_e valid_rec] valid_single]. destruct H5 as [[valid_e valid_rec] valid_single].
pose proof (validRanges_single _ _ _ _ valid_e) as valid_e_single. pose proof (validRanges_single _ _ _ _ valid_e) as valid_e_single.
destruct valid_e_single destruct valid_e_single
as [iv_e [err_e [vR_e [map_e [eval_e_real bounded_vR_e]]]]]. as [iv_e [err_e [vR_e [map_e [eval_e_real bounded_vR_e]]]]].
...@@ -187,9 +189,9 @@ Proof. ...@@ -187,9 +189,9 @@ Proof.
split; try auto. split; try auto.
hnf; intros; subst; set_tac. hnf; intros; subst; set_tac.
+ destruct iv_e; auto. + destruct iv_e; auto.
+ rewrite <- (meps_0_deterministic (toRExp e) eval_e_real H17) in *; try 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) apply (IHf (updEnv n vR_e E1) (updEnv n v1 E2)
Gamma v vR m0 A fVars Gamma DeltaMap v vR m0 A fVars
(NatSet.add n dVars) (outVars)); eauto. (NatSet.add n dVars) (outVars)); eauto.
* eapply approxUpdBound; eauto; simpl in *. * eapply approxUpdBound; eauto; simpl in *.
{ eapply toRExpMap_some; eauto. simpl; auto. } { eapply toRExpMap_some; eauto. simpl; auto. }
...@@ -218,9 +220,9 @@ Proof. ...@@ -218,9 +220,9 @@ Proof.
* set_tac; split. * set_tac; split.
{ split; try auto. { split; try auto.
hnf; intros; subst. hnf; intros; subst.
apply H5; rewrite NatSet.add_spec; auto. } apply H6; rewrite NatSet.add_spec; auto. }
{ hnf; intros. { hnf; intros.
apply H5; rewrite NatSet.add_spec; auto. } apply H6; rewrite NatSet.add_spec; auto. }
(* (*
* unfold vars_typed. intros. * unfold vars_typed. intros.
unfold updDefVars. unfold updDefVars.
...@@ -239,8 +241,8 @@ Proof. ...@@ -239,8 +241,8 @@ Proof.
set_tac. split; try auto. set_tac. split; try auto.
split; try auto. split; try auto.
hnf; intros; subst; set_tac. } hnf; intros; subst; set_tac. }
{ apply H8. { apply H9.
rewrite NatSet.add_spec in H4; destruct H4; rewrite NatSet.add_spec in H5; destruct H5;
auto; subst; congruence. } auto; subst; congruence. }
- destruct H4. destruct H3. eapply FPRangeValidator_sound; eauto. - destruct H5. destruct H4. eapply FPRangeValidator_sound; eauto.
Qed. Qed.
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