Commit 43cdec44 authored by Joachim Bard's avatar Joachim Bard
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:AVA/FloVer

parents c6ea9dea 6a6ee6a4
# Project FloVer
## FM 2019
All implementations included in the FM2019 submission are on the branch [FM19][2].
The folder `scripts` contains the scripts we used to run the evaluation from the paper.
Changes described in the paper can be found in the folder `coq`. The overall soundness theorem is stated in file `CertificateChecker.v`.
The SMT-based range validator and its soundness proof can be found in file [SMTValidation.v][3], and the Subdivision checker can be found in file [SubdivsChecker.v][4].
## FMCAD 2018
The artifact and scripts used to run the evaluation for FMCAD 2018 can be found on the branch [FMCAD 2018][1].
......@@ -30,7 +37,7 @@ Full support for fixed-point programs is also only available in `affine_arithmet
## Checking Coq certificates
FloVer is known to compile with coq `8.7.2` and `8.8.0`.
FloVer is known to compile with coq `8.8.2`.
To check the Coq certificate, you need to enter the `coq` directory.
Place any certificate you want to have checked into the `output` folder in the
coq directory and then run
......@@ -43,9 +50,8 @@ This will compile all coq files and then in the end the certificate in the outpu
To compile the file `IEEE_connection.v` showing the relation to IEEE754 semantics, it is necessary to install
the Flocq library via opam:
```bash
$ opam install coq-flocq.2.6.1
$ opam install coq-flocq.3.1.0
```
Note that due to some incompatibilities, FloVer currently does not support flocq 3.0.
The coq binary is build in the directory `coq/binary` and you can compile it by
running `make native` in the directory.
......@@ -99,7 +105,7 @@ $ ./cake_checker CERTIFICATE_FILE
## Contributors
In no particular order: Raphael Monat, Nikita Zyuzin, Heiko Becker
In no particular order: Raphael Monat, Nikita Zyuzin, Joachim Bard, Heiko Becker
Acknowledgements
......@@ -107,4 +113,7 @@ Acknowledgements
We would like to thank Jacques-Henri Jourdan for the many insightful discussions
and technical help while working on the initial version of FloVer.
[1]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/FMCAD2018
\ No newline at end of file
[1]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/FMCAD2018
[2]: https://gitlab.mpi-sws.org/AVA/FloVer/tree/FM19
[3]: https://gitlab.mpi-sws.org/AVA/FloVer/blob/FM19/coq/SMTValidation.v
[4]: https://gitlab.mpi-sws.org/AVA/FloVer/blob/FM19/coq/SubdivsChecker.v
\ No newline at end of file
(*
Lemma shadowing_free_rewriting_expr e v E1 E2 defVars:
(forall n, E1 n = E2 n)->
eval_expr E1 defVars (toREval e) v REAL <->
eval_expr E2 defVars (toREval e) v REAL.
Proof.
revert v E1 E2.
induction e; intros v' E1 E2 agree_on_vars.
- split; intros eval_Var.
+ inversion eval_Var; subst.
rewrite agree_on_vars in H1.
constructor; auto.
+ inversion eval_Var; subst.
rewrite <- agree_on_vars in H1.
eapply Var_load; eauto.
- split; intros eval_Const; inversion eval_Const; subst; econstructor; auto.
- split; intros eval_Unop; inversion eval_Unop; subst; econstructor; try auto.
+ erewrite IHe; eauto.
+ erewrite IHe; eauto.
+ erewrite <- IHe; eauto.
+ erewrite <- IHe; eauto.
- split; intros eval_Binop; inversion eval_Binop; subst; econstructor; eauto.
destruct m1; destruct m2; inversion H2.
try (erewrite IHe1; eauto);
try (erewrite IHe2; eauto); auto.
- split; intros eval_Downcast; simpl; simpl in eval_Downcast; erewrite IHe; eauto.
Qed.
Lemma shadowing_free_rewriting_cmd f E1 E2 vR defVars:
(forall n, E1 n = E2 n) ->
bstep (toREvalCmd f) E1 defVars vR REAL <->
bstep (toREvalCmd f) E2 defVars vR REAL.
Proof.
revert E1 E2 defVars vR.
induction f; intros E1 E2 vR agree_on_vars.
- split; intros bstep_Let; inversion bstep_Let; subst.
+ erewrite shadowing_free_rewriting_expr in H8; auto.
econstructor; eauto.
rewrite <- IHf.
apply H10.
intros n'; unfold updEnv.
case_eq (n' =? n); auto.
+ erewrite <- shadowing_free_rewriting_expr in H8; auto.
econstructor; eauto.
rewrite IHf.
apply H10.
intros n'; unfold updEnv.
case_eq (n' =? n); auto.
- split; intros bstep_Ret; inversion bstep_Ret; subst.
+ erewrite shadowing_free_rewriting_expr in H1; auto.
constructor; auto.
+ erewrite <- shadowing_free_rewriting_expr in H1; auto.
constructor; auto.
Qed.
Lemma dummy_bind_ok e v x v' inVars E defVars:
NatSet.Subset (usedVars e) inVars ->
NatSet.mem x inVars = false ->
eval_expr E defVars (toREval (toRExp e)) v REAL ->
eval_expr (updEnv x v' E) defVars (toREval (toRExp e)) v REAL.
Proof.
revert v x v' inVars E.
induction e; intros v1 x v2 inVars E valid_vars x_not_free eval_e.
- inversion eval_e; subst.
assert ((updEnv x v2 E) n = E n).
+ unfold updEnv.
case_eq (n =? x); try auto.
intros n_eq_x.
rewrite Nat.eqb_eq in n_eq_x.
subst; simpl in *.
hnf in valid_vars.
assert (NatSet.mem x (NatSet.singleton x) = true)
as in_singleton by (rewrite NatSet.mem_spec, NatSet.singleton_spec; auto).
rewrite NatSet.mem_spec in *.
specialize (valid_vars x in_singleton).
rewrite <- NatSet.mem_spec in valid_vars.
rewrite valid_vars in *; congruence.
+ econstructor; eauto.
rewrite H; auto.
- inversion eval_e; subst; constructor; auto.
- inversion eval_e; subst; econstructor; eauto.
- simpl in valid_vars.
inversion eval_e; subst; econstructor; eauto;
destruct m1; destruct m2; inversion H2;
subst.
+ eapply IHe1; eauto.
hnf; intros a in_e1.
apply valid_vars;
rewrite NatSet.union_spec; auto.
+ eapply IHe2; eauto.
hnf; intros a in_e2.
apply valid_vars;
rewrite NatSet.union_spec; auto.
- apply (IHe v1 x v2 inVars E); auto.
Qed.
Fixpoint expr_subst (e:expr Q) x e_new :=
match e with
|Var _ v => if v =? x then e_new else Var Q v
|Unop op e1 => Unop op (expr_subst e1 x e_new)
|Binop op e1 e2 => Binop op (expr_subst e1 x e_new) (expr_subst e2 x e_new)
|Downcast m e1 => Downcast m (expr_subst e1 x e_new)
| e => e
end.
*)
(* Lemma expr_subst_correct e e_sub E x v v_res defVars: *)
(* eval_expr E defVars (toREval (toRExp e_sub)) v REAL -> *)
(* eval_expr (updEnv x v E) defVars (toREval (toRExp e)) v_res REAL <-> *)
(* eval_expr E defVars (toREval (toRExp (expr_subst e x e_sub))) v_res REAL. *)
(* Proof. *)
(* intros eval_e. *)
(* revert v_res. *)
(* induction e. *)
(* - intros v_res; split; [intros eval_upd | intros eval_subst]. *)
(* + unfold updEnv in eval_upd. simpl in *. *)
(* inversion eval_upd; subst. *)
(* case_eq (n =? x); intros; try auto. *)
(* * rewrite H in H1. *)
(* inversion H1; subst; auto. *)
(* * rewrite H in H1. *)
(* eapply Var_load; eauto. *)
(* + simpl in eval_subst. *)
(* case_eq (n =? x); intros n_eq_case; *)
(* rewrite n_eq_case in eval_subst. *)
(* * simpl. *)
(* assert (updEnv x v E n = Some v_res). *)
(* { unfold updEnv; rewrite n_eq_case. *)
(* f_equal. assert (v = v_res) by (eapply meps_0_deterministic; eauto). rewrite H. auto. } *)
(* { econstructor; eauto. *)
(* rewrite n_eq_case; auto. } *)
(* * simpl. inversion eval_subst; subst. *)
(* assert (E n = updEnv x v E n). *)
(* { unfold updEnv; rewrite n_eq_case; reflexivity. } *)
(* { rewrite H in H1. eapply Var_load; eauto. rewrite n_eq_case. auto. } *)
(* - intros v_res; split; [intros eval_upd | intros eval_subst]. *)
(* + inversion eval_upd; constructor; auto. *)
(* + inversion eval_subst; constructor; auto. *)
(* - split; [intros eval_upd | intros eval_subst]. *)
(* + inversion eval_upd; econstructor; auto; *)
(* rewrite <- IHe; auto. *)
(* + inversion eval_subst; constructor; try auto; *)
(* rewrite IHe; auto. *)
(* - intros v_res; split; [intros eval_upd | intros eval_subst]. *)
(* + inversion eval_upd; econstructor; auto; *)
(* destruct m1; destruct m2; inversion H2. *)
(* * rewrite <- IHe1; auto. *)
(* * rewrite <- IHe2; auto. *)
(* + inversion eval_subst; econstructor; auto; *)
(* destruct m1; destruct m2; inversion H2. *)
(* * rewrite IHe1; auto. *)
(* * rewrite IHe2; auto. *)
(* - split; [intros eval_upd | intros eval_subst]. *)
(* + rewrite <- IHe; auto. *)
(* + rewrite IHe; auto. *)
(* Qed. *)
(* Fixpoint map_subst (f:cmd Q) x e := *)
(* match f with *)
(* |Let m y e_y g => Let m y (expr_subst e_y x e) (map_subst g x e) *)
(* |Ret e_r => Ret (expr_subst e_r x e) *)
(* end. *)
(* Lemma stepwise_substitution x e v f E vR inVars outVars defVars: *)
(* ssa (toREvalCmd (toRCmd f)) inVars outVars -> *)
(* NatSet.In x inVars -> *)
(* NatSet.Subset (usedVars e) inVars -> *)
(* eval_expr E defVars (toREval (toRExp e)) v REAL -> *)
(* bstep (toREvalCmd (toRCmd f)) (updEnv x v E) (fun n => if (n =? x) then Some REAL else defVars n) vR REAL <-> *)
(* bstep (toREvalCmd (toRCmd (map_subst f x e))) E defVars vR REAL. *)
(* Proof. *)
(* revert E e x vR inVars outVars defVars. *)
(* induction f; intros E e0 x vR inVars outVars defVars ssa_f x_free valid_vars_e eval_e. *)
(* - split; [ intros bstep_let | intros bstep_subst]. *)
(* + inversion bstep_let; subst. *)
(* inversion ssa_f; subst. *)
(* assert (forall E var, updEnv n v0 (updEnv x v E) var = updEnv x v (updEnv n v0 E) var). *)
(* * eapply ssa_shadowing_free. *)
(* apply ssa_f. *)
(* apply x_free. *)
(* eauto. *)
(* * erewrite (shadowing_free_rewriting_cmd _ _ _ _) in H8; try eauto. *)
(* simpl in *. *)
(* econstructor; eauto. *)
(* { rewrite <- expr_subst_correct; eauto. } *)
(* { rewrite <- IHf; eauto. *)
(* admit. *)
(* rewrite NatSet.add_spec; right; auto. *)
(* apply validVars_add; auto. *)
(* eapply dummy_bind_ok; eauto. } *)
(* + inversion bstep_subst; subst. *)
(* simpl in *. *)
(* inversion ssa_f; subst. *)
(* econstructor; try auto. *)
(* rewrite expr_subst_correct; eauto. *)
(* rewrite <- IHf in H8; eauto. *)
(* * rewrite <- shadowing_free_rewriting_cmd in H8; eauto. *)
(* admit. *)
(* (* eapply ssa_shadowing_free; eauto. *) *)
(* (* rewrite <- expr_subst_correct in H7; eauto. *) *)
(* * rewrite NatSet.add_spec; auto. *)
(* * apply validVars_add; auto. *)
(* * eapply dummy_bind_ok; eauto. *)
(* - split; [intros bstep_let | intros bstep_subst]. *)
(* + inversion bstep_let; subst. *)
(* simpl in *. *)
(* rewrite expr_subst_correct in H0; eauto. *)
(* constructor. assumption. *)
(* + inversion bstep_subst; subst. *)
(* simpl in *. *)
(* rewrite <- expr_subst_correct in H0; eauto. *)
(* econstructor; eauto. *)
(* Abort. *)
(* Fixpoint let_subst (f:cmd Q) := *)
(* match f with *)
(* | Let m x e1 g => *)
(* expr_subst (let_subst g) x e1 *)
(* | Ret e1 => e1 *)
(* end. *)
(* Lemma eval_subst_subexpr E e' n e vR defVars: *)
(* NatSet.In n (usedVars e) -> *)
(* eval_expr E defVars (toREval (toRExp (expr_subst e n e'))) vR REAL -> *)
(* exists v, eval_expr E defVars (toREval (toRExp e')) v REAL. *)
(* Proof. *)
(* revert E e' n vR. *)
(* induction e; *)
(* intros E e' n' vR n_fVar eval_subst; simpl in *; try eauto. *)
(* - case_eq (n =? n'); intros case_n; rewrite case_n in *; eauto. *)
(* rewrite NatSet.singleton_spec in n_fVar. *)
(* exfalso. *)
(* rewrite Nat.eqb_neq in case_n. *)
(* apply case_n; auto. *)
(* - inversion n_fVar. *)
(* - inversion eval_subst; subst; *)
(* eapply IHe; eauto. *)
(* - inversion eval_subst; subst. *)
(* rewrite NatSet.union_spec in n_fVar. *)
(* destruct m1; destruct m2; inversion H2. *)
(* destruct n_fVar as [n_fVar_e1 | n_fVare2]; *)
(* [eapply IHe1; eauto | eapply IHe2; eauto]. *)
(* Qed. *)
(* Lemma bstep_subst_subexpr_any E e x f vR defVars: *)
(* NatSet.In x (liveVars f) -> *)
(* bstep (toREvalCmd (toRCmd (map_subst f x e))) E defVars vR REAL -> *)
(* exists E' v, eval_expr E' defVars (toREval (toRExp e)) v REAL. *)
(* Proof. *)
(* revert E e x vR defVars; *)
(* induction f; *)
(* intros E e' x vR defVars x_live eval_f. *)
(* - inversion eval_f; subst. *)
(* simpl in x_live. *)
(* rewrite NatSet.union_spec in x_live. *)
(* destruct x_live as [x_used | x_live]. *)
(* + exists E. eapply eval_subst_subexpr; eauto. *)
(* + eapply IHf; eauto. *)
(* Abort. *)
(* - simpl in *. *)
(* inversion eval_f; subst. *)
(* exists E. eapply eval_subst_subexpr; eauto. *)
(* Qed. *)
(* Lemma bstep_subst_subexpr_ret E e x e' vR defVars: *)
(* NatSet.In x (liveVars (Ret e')) -> *)
(* bstep (toREvalCmd (toRCmd (map_subst (Ret e') x e))) E defVars vR REAL -> *)
(* exists v, eval_expr E defVars (toREval (toRExp e)) v REAL. *)
(* Proof. *)
(* simpl; intros x_live bstep_ret. *)
(* inversion bstep_ret; subst. *)
(* eapply eval_subst_subexpr; eauto. *)
(* Qed. *)
(* Lemma no_forward_refs V (f:cmd V) inVars outVars: *)
(* ssa f inVars outVars -> *)
(* forall v, NatSet.In v (definedVars f) -> *)
(* NatSet.mem v inVars = false. *)
(* Proof. *)
(* intros ssa_f; induction ssa_f; simpl. *)
(* - intros v v_defVar. *)
(* rewrite NatSet.add_spec in v_defVar. *)
(* destruct v_defVar as [v_x | v_defVar]. *)
(* + subst; auto. *)
(* + specialize (IHssa_f v v_defVar). *)
(* case_eq (NatSet.mem v inVars); intros mem_inVars; try auto. *)
(* assert (NatSet.mem v (NatSet.add x inVars) = true) by (rewrite NatSet.mem_spec, NatSet.add_spec, <- NatSet.mem_spec; auto). *)
(* congruence. *)
(* - intros v v_in_empty; inversion v_in_empty. *)
(* Qed. *)
(* Lemma bstep_subst_subexpr_let E e x y e' g vR m defVars: *)
(* NatSet.In x (liveVars (Let m y e' g)) -> *)
(* (forall x, NatSet.In x (usedVars e) -> *)
(* exists v, E x = v) -> *)
(* bstep (toREvalCmd (toRCmd (map_subst (Let m y e' g) x e))) E defVars vR REAL -> *)
(* exists v, eval_expr E defVars (toREval (toRExp e)) v REAL. *)
(* Proof. *)
(* revert E e x y e' vR; *)
(* induction g; *)
(* intros E e0 x y e' vR x_live uedVars_def bstep_f. *)
(* - simpl in *. *)
(* inversion bstep_f; subst. *)
(* specialize (IHg (updEnv y m v E) e0 x n e). *)
(* rewrite NatSet.union_spec in x_live. *)
(* destruct x_live as [x_used | x_live]. *)
(* + eapply eval_subst_subexpr; eauto. *)
(* + edestruct IHg as [v0 eval_v0]; eauto. *)
(* Abort. *)
(* Theorem let_free_agree f E vR inVars outVars e defVars: *)
(* ssa f inVars outVars -> *)
(* (forall v, NatSet.In v (definedVars f) -> *)
(* NatSet.In v (liveVars f)) -> *)
(* let_subst f = e -> *)
(* bstep (toREvalCmd (toRCmd (Ret e))) E defVars vR REAL -> *)
(* bstep (toREvalCmd (toRCmd f)) E defVars vR REAL. *)
(* Proof. *)
(* intros ssa_f. *)
(* revert E vR e; *)
(* induction ssa_f; *)
(* intros E vR e_subst dVars_live subst_step bstep_e; *)
(* simpl in *. *)
(* (* Let Case, prove that the value of the let binding must be used somewhere *) *)
(* - case_eq (let_subst s). *)
(* + intros e0 subst_s; rewrite subst_s in *. *)
(* Abort. *)
(* (*inversion subst_step; subst. *)
(* clear subst_s subst_step. *)
(* inversion bstep_e; subst. *)
(* specialize (dVars_live x). *)
(* rewrite NatSet.add_spec in dVars_live. *)
(* assert (NatSet.In x (NatSet.union (usedVars e) (liveVars s))) *)
(* as x_used_or_live *)
(* by (apply dVars_live; auto). *)
(* rewrite NatSet.union_spec in x_used_or_live. *)
(* destruct x_used_or_live as [x_used | x_live]. *)
(* * specialize (H x x_used). *)
(* rewrite <- NatSet.mem_spec in H; congruence. *)
(* * *)
(* eapply let_b. *)
(* Focus 2. *)
(* eapply IHssa_f; try auto. *) *)
(* Theorem let_free_form f E vR inVars outVars e defVars: *)
(* ssa f inVars outVars -> *)
(* bstep (toREvalCmd (toRCmd f)) E defVars vR REAL -> *)
(* let_subst f = e -> *)
(* bstep (toREvalCmd (toRCmd (Ret e))) E defVars vR REAL. *)
(* Proof. *)
(* revert E vR inVars outVars e; *)
(* induction f; *)
(* intros E vR inVars outVars e_subst ssa_f bstep_f subst_step. *)
(* - simpl. *)
(* inversion bstep_f; subst. *)
(* inversion ssa_f; subst. *)
(* Abort. *)
(* (* case_eq (let_subst f). *)
(* + intros f_subst subst_f_eq. *)
(* specialize (IHf (updEnv n REAL v E) vR (NatSet.add n inVars) outVars f_subst H9 H7 subst_f_eq). *)
(* rewrite subst_f_eq in subst_step. *)
(* inversion IHf; subst. *)
(* constructor. *)
(* inversion subst_step. *)
(* subst. *)
(* rewrite <- expr_subst_correct; eauto. *)
(* + intros subst_eq; rewrite subst_eq in subst_step; inversion subst_step. *)
(* - inversion bstep_f; subst. *)
(* constructor. *)
(* simpl in *. *)
(* inversion subst_step; subst. *)
(* assumption. *)
(* Qed. *)
(* *) *)
(* (* *)
(* Lemma ssa_non_stuck (f:cmd Q) (inVars outVars:NatSet.t) (VarEnv:var_env) *)
(* (ParamEnv:param_env) (P:precond) (eps:R): *)
(* ssa Q f inVars outVars -> *)
(* (forall v, NatSet.In v (freeVars e) -> *)
(* (Q2R (ivlo (P v)) <= ParamEnv v <= Q2R (ivhi (P v))))%R -> *)
(* (forall v, NatSet.In v inVars -> *)
(* exists r, VarEnv v = Some r) -> *)
(* exists vR, *)
(* bstep (toRCmd f) VarEnv ParamEnv P eps (Nop R) vR. *)
(* Proof. *)
(* intros ssa_f; revert VarEnv ParamEnv P eps. *)
(* induction ssa_f; *)
(* intros VarEnv ParamEnv P eps fVars_live. *)
(* - *)
(* *) *)
\ No newline at end of file
......@@ -25,6 +25,10 @@ Definition CertificateChecker (e: expr Q) (absenv: analysisResult)
| _ => false
end.
(**
General soundness theorem, exposing all invariants that are shown by
the separate validator functions
**)
Theorem Certificate_checking_is_sound_general (e:expr Q) (absenv:analysisResult)
P Qmap subdivs defVars:
forall (E1 E2:env) DeltaMap,
......@@ -63,13 +67,11 @@ Proof.
intros. cbn in *; congruence. }
exists Gamma; intros approxEnv_E1E2.
destruct subdivs.
- edestruct result_checking_sound as (validR & validFPR & validErr); eauto.
- edestruct result_checking_sound; eauto.
intuition.
edestruct validRanges_single as (iv_e & err_e & vR & find_e & eval_real_e & ?); eauto.
edestruct validErrorBoundsRec_single as ((vFP & mFP & eval_fp_e) & H4); eauto.
assert (validSSA e (freeVars e) = true) as Hssa_small.
{ apply andb_true_iff in certificate_valid as (Hssa & _).
eapply validSSA_downward_closed; eauto using validSSA_checks_freeVars. set_tac. }
apply validSSA_sound in Hssa_small as (outVars & Hssa_small).
edestruct validErrorBoundsRec_single; eauto.
destruct H5 as (? & ? & ?).
repeat eexists; eauto.
- (* general version of subdivs_checking_sound *) admit.
Admitted.
......@@ -84,7 +86,6 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult)
forall (E1 E2:env) DeltaMap,
(forall (v : R) (m' : mType),
exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
eval_precond E1 P ->
unsat_queries Qmap ->
(forall Qmap, In Qmap (queriesInSubdivs subdivs) -> unsat_queries Qmap) ->
......
......@@ -17,23 +17,26 @@ Definition ResultChecker (e: expr Q) (absenv: analysisResult)
(**
Soundness proof for the result checker.
**)
Theorem result_checking_sound (e: expr Q) (absenv: analysisResult) P Qmap defVars Gamma DeltaMap:
forall (E1 E2: env),
(forall (v : R) (m' : mType), exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
Theorem result_checking_sound (e: expr Q) (absenv: analysisResult) P Qmap defVars Gamma:
forall (E1 E2: env) DeltaMap,
(forall (v : R) (m' : mType),
exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
approxEnv E1 (toRExpMap Gamma) absenv (freeVars e) NatSet.empty E2 ->
eval_precond E1 P ->
unsat_queries Qmap ->
getValidMap defVars e (FloverMap.empty mType) = Succes Gamma ->
ResultChecker e absenv P Qmap defVars Gamma = true ->
validRanges e absenv E1 (toRTMap (toRExpMap Gamma)) /\
validFPRanges e E2 Gamma DeltaMap /\
validErrorBounds e E1 E2 absenv Gamma.
exists outVars,
ssa e (freeVars e) outVars /\
validRanges e absenv E1 (toRTMap (toRExpMap Gamma)) /\
validErrorBounds e E1 E2 absenv Gamma /\
validFPRanges e E2 Gamma DeltaMap.
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
**)
Proof.
intros * deltas_matched approxE1E2 P_valid unsat_qs valid_typeMap results_valid.
intros * deltaMap_valid approxE1E2 P_valid unsat_qs valid_typeMap results_valid.
unfold ResultChecker in results_valid.
assert (validTypes e Gamma).
{ eapply getValidMap_top_correct; eauto.
......@@ -75,11 +78,11 @@ Proof.
*)
assert (ssa e (NatSet.union (freeVars e) (NatSet.empty)) outVars2).
{ eapply ssa_equal_set; eauto. }
repeat split; auto.
eexists; repeat split; try eauto.
- eapply RoundoffErrorValidator_sound; eauto.
- eapply FPRangeValidator_sound; eauto.
+ eapply RoundoffErrorValidator_sound; eauto.
+ intros v Hin. set_tac.
- eapply RoundoffErrorValidator_sound; eauto.
+ intros; set_tac.
Qed.
(**
......@@ -105,96 +108,10 @@ Corollary result_checking_sound_single (e: expr Q) (absenv: analysisResult) P Qm
Proof.
intros * deltas_matched P_valid unsat_qs valid_typeMap results_valid.
exists Gamma; intros approxE1E2.
assert (validRanges e absenv E1 (toRTMap (toRExpMap Gamma))) as validRange
by (eapply result_checking_sound; eauto).
assert (validErrorBounds e E1 E2 absenv Gamma) as Hsound
by (eapply result_checking_sound; eauto).
edestruct result_checking_sound as (? & _ & validRange & Hsound & _); try eauto.
eapply validRanges_single in validRange.
destruct validRange as [iv [err [vR [Hfind [eval_real validRange]]]]].
eapply validErrorBoundsRec_single in Hsound; eauto.
destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto.
exists iv, err, vR, vF, mF; repeat split; auto.
Qed.
(*
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P: precond)
(Qmap: FloverMap.t (SMTLogic * SMTLogic)) defVars :=
match getValidMapCmd defVars f (FloverMap.empty mType) with
| Succes Gamma =>
if (validSSA f (preVars P))
then
if (RangeValidatorCmd f absenv P Qmap NatSet.empty) &&
FPRangeValidatorCmd f absenv Gamma NatSet.empty
then (RoundoffErrorValidatorCmd f Gamma absenv NatSet.empty)
else false
else false
| _ => false
end.
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P Qmap
defVars DeltaMap:
forall (E1 E2:env),
(forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
eval_precond E1 P ->
unsat_queries Qmap ->
CertificateCheckerCmd f absenv P Qmap defVars = true ->
exists Gamma,
approxEnv E1 (toRExpMap Gamma) absenv (freeVars f) NatSet.empty E2 ->
exists iv err vR vF m,
FloverMap.find (getRetExp f) absenv = Some (iv,err) /\
bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR REAL /\
bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap vF m /\
(forall vF m,
bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap vF m ->
(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.
**)
Proof.
intros * deltas_matched P_valid unsat_qs certificate_valid.
unfold CertificateCheckerCmd in certificate_valid.
destruct (getValidMapCmd defVars f (FloverMap.empty mType)) eqn:?;