Commit cd137018 authored by Heiko Becker's avatar Heiko Becker
Browse files

Certificate checker can soundly validate constants now

parent 8f121ce2
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.ZArith.ZArith Coq.Reals.Reals.
Require Import Daisy.Expressions.
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.ZArith.ZArith Coq.Reals.Reals Coq.QArith.Qreals Coq.QArith.Qcanon.
Require Import Coq.micromega.Psatz.
Require Import Daisy.Expressions Daisy.Infra.RationalConstruction Daisy.Infra.RealSimps.
Section ComputableErrors.
Definition test (frac:Q) :=
match frac with
|a#b => (a+1)#(b-1)
end.
Definition interval :Type := Q * Q.
Definition error :Type := Q.
Definition analysisResult :Type := exp Q -> interval * error.
Definition Qc2Q (q:Qc) :Q := match q with
Qcmake a P => a end.
Lemma double_inject_eq:
forall q, Qc2Q (Q2Qc q) = Qred q.
Proof.
intros q. unfold Q2Qc.
unfold Qc2Q; auto.
Qed.
Definition Qleb :=Qle_bool.
(*
Definition Qcmax (a:Qc) (b:Qc) := Q2Qc (Qmax a b).
Definition Qcabs (a:Qc) := Q2Qc (Qabs a). *)
Definition maxAbs (iv:interval) :=
Qmax (Qabs (fst iv)) (Qabs (snd iv)).
Lemma maxAbs_pointInterval a:
maxAbs (a,a) == Qabs a.
Proof.
unfold maxAbs; simpl.
(* unfold Qcmax.
unfold Qcabs.
apply Qc_is_canon.
apply Qabs_case; intros.
- pose proof (Q.max_id (Qred a)).
unfold Q2Qc; simpl.
rewrite H0.
rewrite Qred_involutive; apply Qeq_refl.
- pose proof (Q.max_id (Qred (-a))).
unfold Q2Qc; simpl.
rewrite H0.
rewrite Qred_involutive.
apply Qeq_refl.
Qed. *)
apply Qabs_case; intros; eapply Q.max_id.
Qed.
(*
Lemma abs_QR (n:Qc):
Rabs (Q2R n) = Q2R (Qcabs n).
Proof.
unfold Rabs.
unfold Qcabs.
apply Qabs_case; intros.
- destruct Rcase_abs.
+ apply Qle_Rle in H.
unfold Q2R at 1 in H.
unfold Qabs.
simpl.
*)
Definition machineEpsilon := (1#(2^53)).
Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
......@@ -36,6 +81,100 @@ Section ComputableErrors.
end
end.
Definition u:nat := 1.
(** 1655/5 = 331; 0,4 = 2/5 **)
Definition cst1:Q := 1657 # 5.
(** Define abbreviations **)
Definition varU:exp Q := Param Q u.
Definition valCst:exp Q := Const cst1.
Definition valCstAddVarU:exp Q := Binop Plus valCst varU.
(** Error values **)
Definition errCst1 :Q := rationalFromNum (7358558207215537#1) 15 14.
Definition errVaru := rationalFromNum (2220446049250313#1) 15 14.
Definition lowerBoundAddUCst:R := 1157 / 5.
Definition upperBoundAddUCst:R := 2157 / 5.
Definition errAddUCst := rationalFromNum (19158008512931703#1) 16 13.
(** The added assertion becomes the precondition for us **)
Definition precondition := fun env:nat -> R => (- 100 <= env u)%R /\ (env u <= 100)%R.
(** As stated, we need to define the absolute environment now as an inductive predicate
Inductive absEnv : abs_env :=
theCst: absEnv valCst (mkInterval cst1 cst1) errCst1
|theVar: absEnv varU (mkInterval (- 100) (100)) errVaru
|theAddition: absEnv valCstAddVarU (mkInterval lowerBoundAddUCst upperBoundAddUCst) errAddUCst. **)
Definition validConstant := Eval compute in validErrorbound (valCst) (fun x => ((cst1,cst1),errCst1)).
Lemma Q2R0_is_0:
Q2R 0 = 0%R.
Proof.
unfold Q2R; simpl; lra.
Qed.
Lemma Rabs_eq_Qabs:
forall x, Rabs (Q2R x) = Q2R (Qabs x).
Proof.
intro.
apply Qabs_case; unfold Rabs; destruct Rcase_abs; intros; try auto.
- apply Qle_Rle in H. exfalso.
apply Rle_not_lt in H; apply H.
assert (Q2R 0 = 0%R) by (unfold Q2R; simpl; lra).
rewrite H0.
apply r.
- unfold Q2R. simpl. rewrite (Ropp_mult_distr_l).
f_equal. rewrite opp_IZR; auto.
- apply Qle_Rle in H. hnf in r; hnf in H. destruct r, H.
+ exfalso. apply Rlt_not_ge in H. apply H; hnf.
left; rewrite Q2R0_is_0; auto.
+ rewrite H in H0.
apply Rgt_not_le in H0.
exfalso; apply H0.
rewrite Q2R0_is_0.
hnf; right; auto.
+ rewrite H0 in H. rewrite Q2R0_is_0 in H.
apply Rlt_not_ge in H; exfalso; apply H.
hnf; right; auto.
unfold Q2R in *; simpl in *.
rewrite opp_IZR.
rewrite Ropp_mult_distr_l_reverse.
repeat rewrite H0.
rewrite Ropp_0; auto.
Qed.
Lemma validErrorboundCorrectConstant:
forall cenv absenv (n:Q) nR nF e,
eval_exp 0%R cenv (Const (Q2R n)) nR ->
eval_exp (Q2R machineEpsilon) cenv (Const (Q2R n)) nF ->
validErrorbound (Const n) absenv = true ->
absenv (Const n) = ((n,n),e) ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros cenv absenv n nR nF e eval_real eval_float error_valid absenv_const.
unfold validErrorbound in error_valid.
rewrite absenv_const in error_valid.
inversion eval_real; subst.
rewrite perturb_0_val in eval_real; auto.
rewrite perturb_0_val; auto.
clear delta H0.
inversion eval_float; subst.
rewrite maxAbs_pointInterval in error_valid.
unfold perturb in *; simpl in *.
rewrite Rabs_err_simpl.
unfold Qleb in error_valid.
apply Qle_bool_iff in error_valid.
apply Qle_Rle in error_valid.
eapply Rle_trans.
rewrite Rabs_mult.
eapply Rmult_le_compat_l; [ apply Rabs_pos | ].
apply H0.
rewrite Rabs_eq_Qabs.
rewrite Q2R_mult in error_valid.
apply error_valid.
Qed.
Lemma validErrorboundCorrect:
forall cenv (n:Q),
eval_exp 0%R cenv (Const n%R) nR ->
......
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