Commit f5393bb8 authored by Heiko Becker's avatar Heiko Becker

Merge branch 'master' into 'certificates'

Finish proofs for new semantics in Coq

See merge request !80
parents bc72a362 d9796e96
......@@ -13,7 +13,9 @@ 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 NatSet.empty).
if (validIntervalbounds e absenv P NatSet.empty)
then (validErrorbound e absenv NatSet.empty)
else false.
(**
Soundness proof for the certificate checker.
......@@ -22,10 +24,11 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
**)
Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
forall (E1 E2:env) (vR:R) (vF:R) fVars,
(forall v, NatSet.mem v (Expressions.freeVars e)= true ->
approxEnv E1 absenv fVars NatSet.empty E2 ->
(forall v, NatSet.mem v fVars = true ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
approxEnv E1 absenv fVars NatSet.empty E2 ->
NatSet.Subset (Expressions.freeVars e) fVars ->
eval_exp 0%R E1 (toRExp e) vR ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e) vF ->
CertificateChecker e absenv P = true ->
......@@ -35,32 +38,37 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
validator and the error bound validator.
**)
Proof.
intros VarEnv1 VarEnv2 ParamEnv vR vF P_valid approxC1C2 eval_real eval_float certificate_valid.
intros E1 E2 vR vF fVars 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.
assert (exists iv err, absenv e = (iv,err)) by (destruct (absenv e); 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 (validErrorbound_sound); eauto.
intros v v_in_empty.
rewrite NatSet.mem_spec in v_in_empty.
hnf in v_in_empty.
inversion v_in_empty.
admit.
Admitted.
env_assert absenv e env_e.
destruct env_e as [iv [err absenv_eq]].
destruct iv as [ivlo ivhi].
rewrite absenv_eq; simpl.
eapply validErrorbound_sound; 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.
rewrite NatSet.mem_spec in v_in_empty.
inversion v_in_empty.
Qed.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :=
andb (validIntervalboundsCmd f absenv P NatSet.empty)
(validErrorboundCmd f absenv NatSet.empty).
if (validIntervalboundsCmd f absenv P NatSet.empty)
then (validErrorboundCmd f absenv NatSet.empty)
else false.
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
forall (E1 E2:env) outVars vR vF fVars,
approxEnv E1 absenv fVars NatSet.empty E2 ->
(forall v, NatSet.mem v fVars= true ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
approxEnv E1 absenv fVars NatSet.empty E2 ->
NatSet.Subset (Commands.freeVars f) fVars ->
ssaPrg f fVars outVars ->
bstep (toRCmd f) E1 0 vR ->
bstep (toRCmd f) E2 (Q2R machineEpsilon) vF ->
......@@ -71,22 +79,28 @@ 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 P_valid approxC1C2 ssa_f eval_real eval_float
intros E1 E2 outVars vR vF fVars 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.
andb_to_prop certificate_valid.
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 *.
env_assert absenv (getRetExp f) env_f.
destruct env_f as [iv [err absenv_eq]].
destruct iv as [ivlo ivhi].
rewrite absenv_eq; simpl.
eapply (validErrorboundCmd_sound); eauto.
- hnf.
intros a; split; intros in_set.
+ rewrite NatSet.union_spec in in_set.
destruct in_set; try auto.
inversion H.
- instantiate (1 := outVars).
eapply ssa_equal_set; try eauto.
hnf.
intros a; split; intros in_union.
+ rewrite NatSet.union_spec in in_union.
destruct in_union as [in_fVars | in_empty]; try auto.
inversion in_empty.
+ rewrite NatSet.union_spec; auto.
- hnf; intros a in_diff.
rewrite NatSet.diff_spec in in_diff.
destruct in_diff.
apply fVars_subset; auto.
- intros v v_in_empty.
rewrite NatSet.mem_spec in v_in_empty.
inversion v_in_empty.
......
......@@ -38,13 +38,13 @@ Inductive bstep : cmd R -> env -> R -> R -> Prop :=
eval_exp eps E e v ->
bstep (Ret e) E eps v.
Fixpoint freeVars (f:cmd Q) :NatSet.t :=
Fixpoint freeVars V (f:cmd V) :NatSet.t :=
match f with
| Let x e1 g => NatSet.remove x (NatSet.union (Expressions.freeVars e1) (freeVars g))
| Ret e => Expressions.freeVars e
end.
Fixpoint definedVars (f:cmd Q) :NatSet.t :=
Fixpoint definedVars V (f:cmd V) :NatSet.t :=
match f with
| Let x _ g => NatSet.add x (definedVars g)
| Ret _ => NatSet.empty
......
This diff is collapsed.
......@@ -13,30 +13,34 @@ Require Export Daisy.IntervalArithQ Daisy.IntervalArith Daisy.ssaPrgs.
Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :=
let (intv, _) := absenv e in
match e with
| Var _ v => if NatSet.mem v validVars then true else isSupersetIntv (P v) intv
| Var _ v =>
if NatSet.mem v validVars
then true
else isSupersetIntv (P v) intv && (Qleb (ivlo (P v)) (ivhi (P v)))
| Const n => isSupersetIntv (n,n) intv
| Unop o f =>
let rec := validIntervalbounds f absenv P validVars in
let (iv, _) := absenv f in
let opres :=
if validIntervalbounds f absenv P validVars
then
let (iv, _) := absenv f in
match o with
| Neg =>
let new_iv := negateIntv iv in
isSupersetIntv new_iv intv
| Inv =>
let nodiv0 := orb
(andb (Qleb (ivhi iv) 0) (negb (Qeq_bool (ivhi iv) 0)))
(andb (Qleb 0 (ivlo iv)) (negb (Qeq_bool (ivlo iv) 0))) in
let new_iv := invertIntv iv in
andb (isSupersetIntv new_iv intv) nodiv0
if (((Qleb (ivhi iv) 0) && (negb (Qeq_bool (ivhi iv) 0))) ||
((Qleb 0 (ivlo iv)) && (negb (Qeq_bool (ivlo iv) 0))))
then
let new_iv := invertIntv iv in
isSupersetIntv new_iv intv
else false
end
in
andb rec opres
else false
| Binop op f1 f2 =>
let rec := andb (validIntervalbounds f1 absenv P validVars) (validIntervalbounds f2 absenv P validVars) in
let (iv1,_) := absenv f1 in
let (iv2,_) := absenv f2 in
let opres :=
if ((validIntervalbounds f1 absenv P validVars) &&
(validIntervalbounds f2 absenv P validVars))
then
let (iv1,_) := absenv f1 in
let (iv2,_) := absenv f2 in
match op with
| Plus =>
let new_iv := addIntv iv1 iv2 in
......@@ -48,23 +52,24 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) (vali
let new_iv := multIntv iv1 iv2 in
isSupersetIntv new_iv intv
| Div =>
let nodiv0 := orb
(andb (Qleb (ivhi iv2) 0) (negb (Qeq_bool (ivhi iv2) 0)))
(andb (Qleb 0 (ivlo iv2)) (negb (Qeq_bool (ivlo iv2) 0))) in
let new_iv := divideIntv iv1 iv2 in
andb (isSupersetIntv new_iv intv) nodiv0
if (((Qleb (ivhi iv2) 0) && (negb (Qeq_bool (ivhi iv2) 0))) ||
((Qleb 0 (ivlo iv2)) && (negb (Qeq_bool (ivlo iv2) 0))))
then
let new_iv := divideIntv iv1 iv2 in
isSupersetIntv new_iv intv
else false
end
in
andb rec opres
else false
end.
Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :bool:=
match f with
| Let x e g =>
validIntervalbounds e absenv P validVars &&
(Qeq_bool (fst (fst (absenv e))) (fst (fst (absenv (Var Q x)))) &&
Qeq_bool (snd (fst (absenv e))) (snd (fst (absenv (Var Q x))))) &&
validIntervalboundsCmd g absenv P (NatSet.add x validVars)
if (validIntervalbounds e absenv P validVars &&
Qeq_bool (fst (fst (absenv e))) (fst (fst (absenv (Var Q x)))) &&
Qeq_bool (snd (fst (absenv e))) (snd (fst (absenv (Var Q x)))))
then validIntervalboundsCmd g absenv P (NatSet.add x validVars)
else false
|Ret e =>
validIntervalbounds e absenv P validVars
end.
......@@ -84,7 +89,9 @@ Proof.
rewrite case_mem in approx_true; simpl in *.
+ rewrite NatSet.mem_spec in case_mem.
contradiction.
+ apply Is_true_eq_left in approx_true; auto.
+ apply Is_true_eq_left in approx_true.
apply andb_prop_elim in approx_true.
destruct approx_true; auto.
- intros approx_true v0 v_in_fV; simpl in *.
inversion v_in_fV.
- intros approx_unary_true v v_in_fV.
......@@ -140,11 +147,13 @@ Proof.
env_assert absenv (Binop Div e1 e2) abs_div; destruct abs_div as [iv_div [err_div abs_div]].
env_assert absenv e1 abs_e1; destruct abs_e1 as [iv_e1 [err_e1 abs_e1]].
rewrite abs_div, abs_e1, absenv_eq in validBounds.
repeat (rewrite <- andb_lazy_alt in validBounds).
apply Is_true_eq_left in validBounds.
apply andb_prop_elim in validBounds.
destruct validBounds as [_ validBounds]; apply andb_prop_elim in validBounds.
destruct validBounds as [_ nodiv0].
destruct validBounds as [nodiv0 _].
apply Is_true_eq_true in nodiv0.
unfold isSupersetIntv in *; simpl in *.
apply le_neq_bool_to_lt_prop; auto.
Qed.
......@@ -154,26 +163,27 @@ Fixpoint getRetExp (V:Type) (f:cmd V) :=
| Ret e => e
end.
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) V E:
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars E:
forall vR,
validIntervalbounds f absenv P V = true ->
(forall v, NatSet.mem v V = true ->
validIntervalbounds f absenv P dVars = true ->
(forall v, NatSet.mem v dVars = true ->
exists vR, E v = Some vR /\
(Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
(forall v, NatSet.mem v (NatSet.diff (Expressions.freeVars f) V)= true ->
NatSet.Subset (NatSet.diff (Expressions.freeVars f) dVars) fVars ->
(forall v, NatSet.mem v fVars = true ->
exists vR, E v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
eval_exp 0%R E (toRExp f) vR ->
(Q2R (fst (fst(absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R.
Proof.
induction f; intros vR valid_bounds valid_definedVars valid_freeVars eval_f.
induction f; intros vR valid_bounds valid_definedVars freeVars_subset valid_freeVars eval_f.
- unfold validIntervalbounds in valid_bounds.
env_assert absenv (Var Q n) absenv_var.
destruct absenv_var as [ iv [err absenv_var]].
specialize (valid_freeVars n).
rewrite absenv_var in *; simpl in *.
inversion eval_f; subst.
case_eq (NatSet.mem n V); intros case_mem; rewrite case_mem in *; simpl in *.
case_eq (NatSet.mem n dVars); intros case_mem; rewrite case_mem in *; simpl in *.
+ specialize (valid_definedVars n case_mem).
destruct valid_definedVars as [vR' [E_n_eq precond_sound]].
rewrite E_n_eq in *.
......@@ -182,19 +192,23 @@ Proof.
+ repeat (rewrite delta_0_deterministic in *; try auto).
unfold isSupersetIntv in valid_bounds.
andb_to_prop valid_bounds.
apply Qle_bool_iff in L;
apply Qle_bool_iff in R.
apply Qle_Rle in L;
apply Qle_Rle in R.
apply Qle_bool_iff in L0;
apply Qle_bool_iff in R0.
apply Qle_Rle in L0;
apply Qle_Rle in R0.
simpl in *.
assert (NatSet.mem n (NatSet.diff (NatSet.singleton n) V) = true).
* rewrite NatSet.mem_spec, NatSet.diff_spec, NatSet.singleton_spec.
assert (NatSet.mem n fVars = true) as in_fVars.
* assert (NatSet.In n (NatSet.singleton n))
as in_singleton by (rewrite NatSet.singleton_spec; auto).
rewrite NatSet.mem_spec.
hnf in freeVars_subset.
apply freeVars_subset.
rewrite NatSet.diff_spec, NatSet.singleton_spec.
split; try auto.
hnf; intros mem_V.
rewrite <- NatSet.mem_spec in mem_V;
rewrite mem_V in case_mem.
inversion case_mem.
* specialize (valid_freeVars H);
hnf; intros in_dVars.
rewrite <- NatSet.mem_spec in in_dVars.
rewrite in_dVars in case_mem; congruence.
* specialize (valid_freeVars in_fVars);
destruct valid_freeVars as [vR' [vR_def P_valid]].
rewrite vR_def in H0; inversion H0; subst.
lra.
......@@ -226,7 +240,7 @@ Proof.
destruct valid_bounds as [valid_rec valid_unop].
apply Is_true_eq_true in valid_rec.
inversion eval_f; subst.
+ specialize (IHf v1 valid_rec valid_definedVars valid_freeVars H2).
+ specialize (IHf v1 valid_rec valid_definedVars freeVars_subset valid_freeVars H2).
rewrite absenv_f in IHf; simpl in IHf.
(* TODO: Make lemma *)
unfold isSupersetIntv in valid_unop.
......@@ -244,10 +258,10 @@ Proof.
* eapply Rle_trans.
Focus 2. apply valid_hi.
rewrite Q2R_opp; lra.
+ specialize (IHf v1 valid_rec valid_definedVars valid_freeVars H3).
+ specialize (IHf v1 valid_rec valid_definedVars freeVars_subset valid_freeVars H3).
rewrite absenv_f in IHf; simpl in IHf.
apply andb_prop_elim in valid_unop.
destruct valid_unop as [valid_unop nodiv0].
destruct valid_unop as [nodiv0 valid_unop].
(* TODO: Make lemma *)
unfold isSupersetIntv in valid_unop.
apply andb_prop_elim in valid_unop.
......@@ -333,19 +347,18 @@ Proof.
assert ((Q2R (fst (fst (iv1, err1))) <= v1 <= Q2R (snd (fst (iv1, err1))))%R) as valid_bounds_e1.
+ apply IHf1; try auto.
intros v in_diff_e1.
apply valid_freeVars.
rewrite NatSet.mem_spec, NatSet.diff_spec in *.
simpl.
destruct in_diff_e1; split; try auto.
rewrite NatSet.union_spec; auto.
apply freeVars_subset.
simpl. rewrite NatSet.diff_spec,NatSet.union_spec.
rewrite NatSet.diff_spec in in_diff_e1.
destruct in_diff_e1 as [ in_freeVars not_dVar].
split; try auto.
+ assert (Q2R (fst (fst (iv2, err2))) <= v2 <= Q2R (snd (fst (iv2, err2))))%R as valid_bounds_e2.
* apply IHf2; try auto.
intros v in_diff_e2.
apply valid_freeVars.
rewrite NatSet.mem_spec, NatSet.diff_spec in *.
simpl.
destruct in_diff_e2; split; try auto.
rewrite NatSet.union_spec; auto.
apply freeVars_subset.
simpl. rewrite NatSet.diff_spec, NatSet.union_spec.
rewrite NatSet.diff_spec in in_diff_e2.
destruct in_diff_e2; split; auto.
* destruct b; simpl in *.
{ pose proof (interval_addition_valid (iv1 :=(Q2R (fst iv1),Q2R (snd iv1))) (iv2 :=(Q2R (fst iv2), Q2R (snd iv2)))) as valid_add.
unfold validIntervalAdd in valid_add.
......@@ -423,9 +436,11 @@ Proof.
rewrite <- Q2R_max4 in valid_mul_hi.
unfold absIvUpd; auto. }
{ pose proof (interval_division_valid (a:=v1) (b:=v2) (iv1:=(Q2R (fst iv1), Q2R (snd iv1))) (iv2:=(Q2R (fst iv2),Q2R (snd iv2)))) as valid_div.
rewrite <- andb_lazy_alt in valid_bin.
unfold contained in valid_div.
unfold isSupersetIntv in valid_bin.
apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_bin nodiv0].
apply andb_prop_elim in valid_bin; destruct valid_bin as [nodiv0 valid_bin].
(** CONTINUE **)
apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
......@@ -487,46 +502,87 @@ Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult):
exists vR,
E v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
validIntervalboundsCmd f absenv P dVars = true ->
absenv (getRetExp f) = ((elo, ehi), err) ->
(Q2R elo <= vR <= Q2R ehi)%R.
Proof.
induction f;
intros E envR fVars dVars outVars elo ehi err P ssa_f eval_f dVars_sound fVars_valid valid_bounds_f absenv_f.
intros E vR fVars dVars outVars elo ehi err P ssa_f eval_f dVars_sound
fVars_valid freeVars_subset valid_bounds_f absenv_f.
- inversion ssa_f; subst.
inversion eval_f; subst.
unfold validIntervalboundsCmd in valid_bounds_f.
andb_to_prop valid_bounds_f.
inversion ssa_f; subst.
specialize (IHf (updEnv n v E) vR fVars (NatSet.add n dVars)).
eapply IHf; eauto.
admit.
intros v0 mem_v0.
unfold updEnv.
case_eq (v0 =? n); intros v0_eq.
+ rename L into eq_lo;
rename R1 into eq_hi.
apply Qeq_bool_iff in eq_lo;
apply Qeq_eqR in eq_lo.
apply Qeq_bool_iff in eq_hi;
apply Qeq_eqR in eq_hi.
rewrite Nat.eqb_eq in v0_eq.
subst.
rewrite <- eq_lo, <- eq_hi.
exists v.
split; auto.
eapply validIntervalbounds_sound; eauto.
admit.
+ apply dVars_sound. rewrite NatSet.mem_spec.
rewrite NatSet.mem_spec in mem_v0.
rewrite NatSet.add_spec in mem_v0.
destruct mem_v0; try auto.
rewrite Nat.eqb_neq in v0_eq.
exfalso; apply v0_eq; auto.
+ admit.
+ assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars)) (NatSet.union fVars (NatSet.add n dVars))).
* hnf. intros a; split; intros in_set.
{ rewrite NatSet.add_spec, NatSet.union_spec in in_set.
rewrite NatSet.union_spec, NatSet.add_spec.
destruct in_set as [P1 | [ P2 | P3]]; auto. }
{ rewrite NatSet.add_spec, NatSet.union_spec.
rewrite NatSet.union_spec, NatSet.add_spec in in_set.
destruct in_set as [P1 | [ P2 | P3]]; auto. }
* eapply ssa_equal_set; eauto.
symmetry; eauto.
+ intros v0 mem_v0.
unfold updEnv.
case_eq (v0 =? n); intros v0_eq.
* rename R1 into eq_lo;
rename R0 into eq_hi.
apply Qeq_bool_iff in eq_lo;
apply Qeq_eqR in eq_lo.
apply Qeq_bool_iff in eq_hi;
apply Qeq_eqR in eq_hi.
rewrite Nat.eqb_eq in v0_eq; subst.
rewrite <- eq_lo, <- eq_hi.
exists v; split; auto.
eapply validIntervalbounds_sound; eauto.
simpl in freeVars_subset.
hnf. intros a in_freeVars.
apply freeVars_subset.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
rewrite NatSet.diff_spec in in_freeVars.
destruct in_freeVars as [ in_freeVars not_dVar].
repeat split; try auto.
{ hnf; intros; subst.
apply validVars_subset_freeVars in H2.
specialize (H2 n in_freeVars).
rewrite <- NatSet.mem_spec in H2.
rewrite H2 in H5; congruence. }
* apply dVars_sound. rewrite NatSet.mem_spec.
rewrite NatSet.mem_spec in mem_v0.
rewrite NatSet.add_spec in mem_v0.
destruct mem_v0; try auto.
rewrite Nat.eqb_neq in v0_eq.
exfalso; apply v0_eq; auto.
+ intros v0 mem_fVars.
unfold updEnv.
case_eq (v0 =? n); intros case_v0; auto.
rewrite Nat.eqb_eq in case_v0; subst.
assert (NatSet.mem n (NatSet.union fVars dVars) = true) as in_union.
* rewrite NatSet.mem_spec, NatSet.union_spec; rewrite <- NatSet.mem_spec; auto.
* rewrite in_union in *; congruence.
+ clear L R1 R0 R IHf.
hnf. intros a a_freeVar.
rewrite NatSet.diff_spec in a_freeVar.
destruct a_freeVar as [a_freeVar a_no_dVar].
apply freeVars_subset.
simpl.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
repeat split; try auto.
* hnf; intros; subst.
apply a_no_dVar.
rewrite NatSet.add_spec; auto.
* hnf; intros a_dVar.
apply a_no_dVar.
rewrite NatSet.add_spec; auto.
- unfold validIntervalboundsCmd in valid_bounds_f.
inversion eval_f; subst.
unfold updEnv.
assert (Q2R (fst (fst (absenv e))) <= envR <= Q2R (snd (fst (absenv e))))%R.
assert (Q2R (fst (fst (absenv e))) <= vR <= Q2R (snd (fst (absenv e))))%R.
+ eapply validIntervalbounds_sound; eauto.
admit.
+ simpl in *. rewrite absenv_f in *; auto.
Admitted.
Qed.
......@@ -176,7 +176,7 @@ Proof.
pose proof (const_abs_err_bounded _ _ _ _ eval_cst1 H4).
pose proof (param_abs_err_bounded _ _ _ _ eval_param_u H5).
assert (eval_exp machineEpsilon (updEnv 2 (perturb (cenv u) delta1) (updEnv 1 (perturb cst1 delta0) cenv))
(Binop Plus (Var R 1) (Var R 2)) (perturb (eval_binop Plus (perturb cst1 delta0) (perturb (cenv u) delta1)) delta)) by admit.
(Binop Plus (Var R 1) (Var R 2)) (perturb (eval_binop Plus (perturb cst1 delta0) (perturb (cenv u) delta1)) delta)) by .
pose proof (add_abs_err_bounded _ _ _ _ _ _ _ _ _ _ _ eval_cst1 H4 eval_param_u H5 eval_real H6 H H3).
eapply Rle_trans.
apply H7.
......@@ -384,4 +384,4 @@ Qed.
unfold cst1, errAddUCst, machineEpsilon; prove_constant.
}
Qed. *)
*)
\ No newline at end of file
*)
......@@ -123,7 +123,7 @@ Proof.
rewrite Rmax_left; [ |apply Req_le; auto].
assert (Rabs 100 = 100)%R by (unfold Rabs; destruct Rcase_abs; lra).
rewrite H.
(* TODO: What about vlaues that are actually floats ? *) admit.
(* TODO: What about vlaues that are actually floats ? *) .
+ apply (AbsErrParam u (mkInterval (- 100) (100)) errVaru); [constructor | ].
unfold isSoundErr; simpl.
unfold Expressions.machineEpsilon, errVaru.
......@@ -311,4 +311,4 @@ Proof.
Qed. *)
Admitted.
*)
\ No newline at end of file
*)
......@@ -271,11 +271,11 @@ Proof.
rewrite (Rmult_comm a b).
apply (Rge_trans _ (ivlo1 * ivlo2) _); auto.
apply Rle_ge, Rmax_l.
- admit.
- admit.
- admit.
- admit.
- admit.
- admit.
- admit.
**)
\ No newline at end of file
- .
- .
- .
- .
- .
- .
- .
**)
......@@ -56,12 +56,12 @@ Proof.
rewrite Rabs_Ropp.
erewrite Rmax_eq.
unfold machineEpsilon.
admit.
.
- apply AbsErrVar.
unfold isValidErr.
simpl.
(* There is a flaw on how we handle variable errors currently as far as it seems *)
admit.
.
- split.
+ unfold isValidIntv.
split.
......@@ -122,4 +122,4 @@ Proof.
inversion H5 as [ | | op c d e].
(* float valued eval *)
Qed.
\ No newline at end of file
Qed.
......@@ -11,6 +11,22 @@ Fixpoint validVars (V:Type) (f:exp V) Vs :bool :=
| Binop o f1 f2 => validVars f1 Vs && validVars f2 Vs
end.
Lemma validVars_subset_freeVars T (e:exp T) V:
validVars e V = true->
NatSet.Subset (Expressions.freeVars e) V.
Proof.
revert V; induction e; simpl; intros V valid_V; try auto.
- rewrite NatSet.mem_spec in valid_V.
hnf. intros; rewrite NatSet.singleton_spec in *; subst; auto.
- hnf; intros a in_empty; inversion in_empty.
- andb_to_prop valid_V.
hnf; intros a in_union.
rewrite NatSet.union_spec in in_union.
destruct in_union as [in_e1 | in_e2].
+ specialize (IHe1 V L a in_e1); auto.
+ specialize (IHe2 V R a in_e2); auto.
Qed.