Commit 3747df48 authored by Heiko Becker's avatar Heiko Becker

Prove all necessary properties for new semantics

parent 3bf112d9
......@@ -13,19 +13,18 @@ Require Export Daisy.Infra.ExpressionAbbrevs.
(** Certificate checking function **)
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
andb (validIntervalbounds e absenv P NatSet.empty) (validErrorbound e absenv).
andb (validIntervalbounds e absenv P NatSet.empty) (validErrorbound e absenv NatSet.empty).
(**
Soundness proof for the certificate checker.
Apart from assuming two executions, one in R and one on floats, we assume that
the real valued execution respects the precondition.
This property is expressed by the predicate precondValidForExec.
**)
Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
forall (VarEnv1 VarEnv2 ParamEnv:env) (vR:R) (vF:R),
approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv1 ParamEnv P (toRExp e) vR ->
eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e) vF ->
forall (E1 E2:env) (vR:R) (vF:R) fVars,
approxEnv E1 absenv fVars NatSet.empty E2 ->
eval_exp 0%R E1 P (toRExp e) vR ->
eval_exp (Q2R machineEpsilon) E2 P (toRExp e) vF ->
CertificateChecker e absenv P = true ->
(Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
(**
......@@ -50,33 +49,38 @@ Qed.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :=
andb (validIntervalboundsCmd f absenv P NatSet.empty)
(validErrorboundCmd f absenv).
(validErrorboundCmd f absenv NatSet.empty).
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
forall (VarEnv1 VarEnv2 ParamEnv:env) outVars vR vF,
approxEnv VarEnv1 absenv VarEnv2 ->
ssaPrg Q f NatSet.empty outVars ->
bstep (toRCmd f) VarEnv1 ParamEnv P 0 (Nop R) vR ->
bstep (toRCmd f) VarEnv2 ParamEnv P (Q2R machineEpsilon) (Nop R) vF ->
forall (E1 E2:env) outVars vR vF fVars,
approxEnv E1 absenv fVars NatSet.empty E2 ->
ssaPrg f fVars outVars ->
bstep (toRCmd f) E1 P 0 vR ->
bstep (toRCmd f) E2 P (Q2R machineEpsilon) vF ->
CertificateCheckerCmd f absenv P = true ->
(Rabs (vR - vF) <= Q2R (snd (absenv (Var Q 0))))%R.
(Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R.
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
**)
Proof.
intros VarEnv1 VarEnv2 ParamEnv outVars envR envF
approxC1C2 ssa_f eval_real eval_float certificate_valid.
intros E1 E2 outVars vR vF fVars approxC1C2 ssa_f eval_real eval_float
certificate_valid.
unfold CertificateCheckerCmd in certificate_valid.
andb_to_prop certificate_valid.
assert (exists iv err, absenv (Var Q 0) = (iv,err)) by (destruct (absenv (Var Q 0)); repeat eexists).
assert (exists iv err, absenv (getRetExp f) = (iv,err)) by (destruct (absenv (getRetExp f)); repeat eexists).
destruct H as [iv [err absenv_eq]].
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) by (destruct iv; repeat eexists).
destruct H as [ivlo [ ivhi iv_eq]].
subst; rewrite absenv_eq in *; simpl in *.
eapply (validErrorboundCmd_sound); eauto.
intros v v_in_empty.
rewrite NatSet.mem_spec in v_in_empty.
hnf in v_in_empty.
inversion v_in_empty.
- hnf.
intros a; split; intros in_set.
+ rewrite NatSet.union_spec in in_set.
destruct in_set; try auto.
inversion H.
+ rewrite NatSet.union_spec; auto.
- intros v v_in_empty.
rewrite NatSet.mem_spec in v_in_empty.
inversion v_in_empty.
Qed.
\ No newline at end of file
......@@ -18,12 +18,12 @@ Inductive approxEnv : env -> analysisResult -> NatSet.t -> NatSet.t -> env -> Pr
|approxUpdFree E1 E2 A v1 v2 x fVars dVars:
approxEnv E1 A fVars dVars E2 ->
(Rabs (v1 - v2) <= v1 * Q2R machineEpsilon)%R ->
NatSet.mem x dVars = false ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1) A (NatSet.add x fVars) dVars (updEnv x v2 E2)
|approxUpdBound E1 E2 A v1 v2 x fVars dVars:
approxEnv E1 A fVars dVars E2 ->
(Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R ->
NatSet.mem x fVars = false ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1) A fVars (NatSet.add x dVars) (updEnv x v2 E2).
Inductive approxParams :env -> R -> env -> Prop :=
......
......@@ -83,12 +83,18 @@ Lemma validErrorboundCorrectVariable:
approxEnv E1 absenv fVars dVars E2 ->
eval_exp 0%R E1 P (toRExp (Var Q v)) nR ->
eval_exp (Q2R (RationalSimps.machineEpsilon)) E2 P (toRExp (Var Q v)) nF ->
validIntervalbounds (Var Q v) absenv P dVars = true ->
(forall v : NatSet.elt,
NatSet.mem v dVars = true ->
exists vR0 : R,
E1 v = Some vR0 /\
(Q2R (fst (fst (absenv (Var Q v)))) <= vR0 <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
validErrorbound (Var Q v) absenv dVars = true ->
absenv (Var Q v) = ((nlo,nhi),e) ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros E1 E2 absenv v nR nF e nlo nhi P fVars dVars approxCEnv eval_real eval_float
error_valid absenv_var.
intros E1 E2 absenv v nR nF e nlo nhi P fVars dVars approxCEnv eval_real
eval_float bounds_valid dVars_sound error_valid absenv_var.
inversion eval_real; inversion eval_float; subst.
unfold validErrorbound in error_valid.
rewrite absenv_var in *; simpl in *.
......@@ -101,7 +107,13 @@ Proof.
- unfold updEnv in *; simpl in *.
case_eq (v =? x); intros eq_case; rewrite eq_case in *.
+ rewrite Nat.eqb_eq in eq_case; subst.
rewrite H4 in error_valid.
assert (NatSet.mem x dVars = false).
* case_eq (NatSet.mem x dVars); intros case_mem; try auto.
rewrite NatSet.mem_spec in case_mem.
assert (NatSet.In x (NatSet.union fVars dVars)) by (rewrite NatSet.union_spec; auto).
rewrite <- NatSet.mem_spec in H5.
rewrite H5 in H4. inversion H4.
* rewrite H5 in error_valid.
inversion H0; inversion H6; subst.
eapply Rle_trans.
apply H.
......@@ -111,10 +123,30 @@ Proof.
eapply Rle_trans.
Focus 2.
apply error_valid.
admit.
rewrite Q2R_mult.
apply Rmult_le_compat_r.
{ apply mEps_geq_zero. }
{ rewrite <- maxAbs_impl_RmaxAbs.
apply contained_leq_maxAbs_val.
unfold contained.
pose proof (validIntervalbounds_sound (Var Q x) A dVars (P:=P) (E:=fun y : nat => if y =? x then Some nR else E1 y) (vR:=nR) bounds_valid) as valid_bounds_prf.
rewrite absenv_var in valid_bounds_prf; simpl in valid_bounds_prf.
simpl; apply valid_bounds_prf; auto. }
+ apply IHapproxCEnv; try auto.
{ apply (Var_load _ P _ H0 H1 H2 H3). }
{ apply (Var_load _ _ _ H6 H7 H8 H9). }
intros v0 mem_dVars;
specialize (dVars_sound v0 mem_dVars).
destruct dVars_sound as [vR0 [val_def iv_sound_val]].
case_eq (v0 =? x); intros case_mem;
rewrite case_mem in val_def; simpl in val_def.
* rewrite Nat.eqb_eq in case_mem.
subst.
rewrite NatSet.mem_spec in mem_dVars.
assert (NatSet.In x (NatSet.union fVars dVars)) by (rewrite NatSet.union_spec; auto).
rewrite <- NatSet.mem_spec in H5;
rewrite H5 in H4; inversion H4.
* exists vR0; split; auto.
- unfold updEnv in *; simpl in *.
case_eq (v =? x); intros eq_case; rewrite eq_case in *.
+ rewrite Nat.eqb_eq in eq_case; subst.
......@@ -124,12 +156,12 @@ Proof.
rewrite absenv_var in H; auto.
+ unfold updEnv in *; simpl in *.
apply IHapproxCEnv; try auto.
admit.
admit.
case_eq (NatSet.mem v dVars);
intros case_dVars; rewrite case_dVars in *; simpl in *.
* auto.
* assert (NatSet.mem v (NatSet.add x dVars) = false) as not_in_add.
* apply (Var_load _ P _ H0 H1 H2 H3).
* apply (Var_load _ _ _ H6 H7 H8 H9).
* rewrite absenv_var.
case_eq (NatSet.mem v dVars);
intros case_dVars; rewrite case_dVars in *; simpl in *; try auto.
assert (NatSet.mem v (NatSet.add x dVars) = false) as not_in_add.
{ case_eq (NatSet.mem v (NatSet.add x dVars));
intros case_add; rewrite case_add in *; simpl in *.
- rewrite NatSet.mem_spec in case_add.
......@@ -139,9 +171,37 @@ Proof.
+ rewrite <- NatSet.mem_spec in H5. rewrite H5 in case_dVars.
inversion case_dVars.
- auto. }
{ rewrite not_in_add in error_valid.
auto.
Admitted.
{ rewrite absenv_var in bounds_valid. rewrite not_in_add in bounds_valid.
auto. }
* intros v0 mem_dVars.
rewrite absenv_var in *; simpl in *.
rewrite NatSet.mem_spec in mem_dVars.
assert (NatSet.In v0 (NatSet.add x dVars)).
{ rewrite NatSet.add_spec. right; auto. }
{ rewrite <- NatSet.mem_spec in H5.
specialize (dVars_sound v0 H5).
destruct dVars_sound as [vR0 [val_def iv_sound_val]].
case_eq (v0 =? x); intros case_mem;
rewrite case_mem in val_def; simpl in val_def.
rewrite Nat.eqb_eq in case_mem; subst.
- apply (NatSetProps.Dec.F.union_3 fVars) in mem_dVars.
rewrite <- NatSet.mem_spec in mem_dVars.
rewrite mem_dVars in H4; inversion H4.
- exists vR0; split; auto. }
* rewrite absenv_var in bounds_valid.
case_eq (NatSet.mem v dVars); intros case_mem; try auto.
case_eq (NatSet.mem v (NatSet.add x dVars));
intros case_add; rewrite case_add in *; simpl in *;
try auto.
rewrite NatSet.mem_spec in case_add.
rewrite NatSet.add_spec in case_add.
destruct case_add as [eq_x | in_dVars].
{ rewrite Nat.eqb_neq in eq_case.
exfalso; apply eq_case; auto. }
{ rewrite <- NatSet.mem_spec in in_dVars.
rewrite case_mem in in_dVars.
inversion in_dVars. }
Qed.
Lemma validErrorboundCorrectConstant:
forall E1 E2 absenv (n:Q) nR nF e nlo nhi (P:precond) dVars,
......@@ -2025,13 +2085,20 @@ Proof.
instantiate (1 := q0). instantiate (1 := q).
rewrite absenv_e; auto. }
* inversion ssa_f; subst.
case_eq (NatSet.mem n fVars); intros case_mem; try auto.
rewrite NatSet.mem_spec in case_mem.
assert (NatSet.In n fVars \/ NatSet.In n dVars) as in_disj by (left; auto).
rewrite <- NatSet.union_spec, <- NatSet.mem_spec in in_disj.
hnf in inVars_union.
(** TODO **)
rewrite in_disj in H5; inversion H5.
case_eq (NatSet.mem n fVars); intros case_mem.
{ rewrite NatSet.mem_spec in case_mem.
assert (NatSet.In n fVars \/ NatSet.In n dVars) as in_disj by (left; auto).
rewrite <- NatSet.union_spec, <- NatSet.mem_spec in in_disj.
hnf in inVars_union.
rewrite NatSet.mem_spec in in_disj.
rewrite inVars_union in in_disj.
rewrite <- NatSet.mem_spec in in_disj.
rewrite in_disj in H5. inversion H5. }
{ case_eq (NatSet.mem n (NatSet.union fVars dVars)); intros case_union; try auto.
rewrite NatSet.mem_spec in case_union.
rewrite inVars_union in case_union.
rewrite <- NatSet.mem_spec in case_union.
rewrite case_union in H5; inversion H5. }
+ simpl in valid_bounds.
andb_to_prop valid_bounds.
rename L0 into validbound_e;
......@@ -2040,7 +2107,22 @@ Proof.
simpl in valid_intv;
andb_to_prop valid_intv.
eapply (IHf (updEnv n v E1) (updEnv n v0 E2) _ _ _ _ vR vF elo ehi err P); eauto.
* rewrite <- NatSetProps.union_add. admit.
* hnf; intros a; split; intros in_set.
{ rewrite NatSet.add_spec; rewrite NatSet.union_spec in in_set.
destruct in_set.
- right.
apply (NatSetProps.Dec.F.union_2 dVars) in H0.
rewrite <- inVars_union; auto.
- rewrite NatSet.add_spec in H0.
destruct H0; try auto.
apply (NatSetProps.Dec.F.union_3 fVars) in H0.
right; rewrite <- inVars_union; auto. }
{ rewrite NatSet.add_spec in in_set; rewrite NatSet.union_spec.
rewrite NatSet.add_spec.
destruct in_set; try auto.
rewrite <- inVars_union in H0.
rewrite NatSet.union_spec in H0.
destruct H0; auto. }
* intros v1 v1_mem.
unfold updEnv.
case_eq (v1 =? n); intros v1_eq.
......
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