Commit 528b05b8 authored by Raphaël Monat's avatar Raphaël Monat

Certificate Checker port is straightforward

parent 43ce2820
......@@ -6,7 +6,7 @@
**)
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs.
Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments.
Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments Daisy.Typing.
Require Export Coq.QArith.QArith.
Require Export Daisy.Infra.ExpressionAbbrevs.
......@@ -14,7 +14,7 @@ Require Export Daisy.Infra.ExpressionAbbrevs.
(** Certificate checking function **)
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
if (validIntervalbounds e absenv P NatSet.empty)
then (validErrorbound e absenv NatSet.empty)
then (validErrorbound e (typeExpression e) absenv NatSet.empty)
else false.
(**
......@@ -23,14 +23,14 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
the real valued execution respects the precondition.
**)
Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
forall (E1 E2:env) (vR:R) (vF:R) fVars,
forall (E1 E2:env) (vR:R) (vF:R) fVars m,
approxEnv E1 absenv fVars NatSet.empty E2 ->
(forall v, NatSet.mem v fVars = true ->
exists vR, E1 v = Some vR /\
exists vR, E1 v = Some (vR, M0) /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
NatSet.Subset (Expressions.freeVars e) fVars ->
eval_exp 0%R E1 (toRExp e) vR ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e) vF ->
NatSet.Subset (Expressions.usedVars e) fVars ->
eval_exp E1 (toREval (toRExp e)) vR M0 ->
eval_exp E2 (toRExp e) vF m ->
CertificateChecker e absenv P = true ->
(Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
(**
......@@ -38,8 +38,7 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
validator and the error bound validator.
**)
Proof.
intros E1 E2 vR vF fVars approxE1E2 P_valid fVars_subset eval_real eval_float
certificate_valid.
intros * approxE1E2 P_valid fVars_subset eval_real eval_float certificate_valid.
unfold CertificateChecker in certificate_valid.
rewrite <- andb_lazy_alt in certificate_valid.
andb_to_prop certificate_valid.
......@@ -48,11 +47,13 @@ Proof.
destruct iv as [ivlo ivhi].
rewrite absenv_eq; simpl.
eapply validErrorbound_sound; eauto.
- eapply typeExpressionIsSound; eauto.
- hnf. intros a in_diff.
rewrite NatSet.diff_spec in in_diff.
apply fVars_subset.
destruct in_diff; auto.
- intros v v_in_empty.
- apply stupid; rewrite expEqBool_refl; auto.
- intros e0 v m0 v_in_empty.
rewrite NatSet.mem_spec in v_in_empty.
inversion v_in_empty.
Qed.
......@@ -63,15 +64,15 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :
else false.
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
forall (E1 E2:env) outVars vR vF fVars,
forall (E1 E2:env) outVars vR vF fVars m,
approxEnv E1 absenv fVars NatSet.empty E2 ->
(forall v, NatSet.mem v fVars= true ->
exists vR, E1 v = Some vR /\
exists vR, E1 v = Some (vR, M0) /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
NatSet.Subset (Commands.freeVars f) fVars ->
ssaPrg f fVars outVars ->
bstep (toRCmd f) E1 0 vR ->
bstep (toRCmd f) E2 (Q2R machineEpsilon) vF ->
bstep (toREvalCmd (toRCmd f)) E1 vR M0 ->
bstep (toRCmd f) E2 vF m ->
CertificateCheckerCmd f absenv P = true ->
(Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R.
(**
......@@ -79,7 +80,7 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
validator and the error bound validator.
**)
Proof.
intros E1 E2 outVars vR vF fVars approxE1E2 P_valid fVars_subset ssa_f eval_real eval_float
intros * approxE1E2 P_valid fVars_subset ssa_f eval_real eval_float
certificate_valid.
unfold CertificateCheckerCmd in certificate_valid.
rewrite <- andb_lazy_alt in certificate_valid.
......@@ -101,7 +102,7 @@ Proof.
rewrite NatSet.diff_spec in in_diff.
destruct in_diff.
apply fVars_subset; auto.
- intros v v_in_empty.
- intros v m1 v_in_empty.
rewrite NatSet.mem_spec in v_in_empty.
inversion v_in_empty.
Qed.
\ No newline at end of file
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