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

Merge with new semantics and fix compilation

parents 340b623d 939af786
......@@ -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 (usedVars e) fVars ->
eval_exp 0%R E1 (toRExp e) vR ->
eval_exp (Q2R machineEpsilon) E2 (toRExp e) vF ->
CertificateChecker e absenv P = true ->
......@@ -35,33 +38,38 @@ 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 ->
ssaPrg f fVars outVars ->
NatSet.Subset (Commands.freeVars f) fVars ->
ssa f fVars outVars ->
bstep (toRCmd f) E1 0 vR ->
bstep (toRCmd f) E2 (Q2R machineEpsilon) vF ->
CertificateCheckerCmd f absenv P = true ->
......@@ -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.
......
......@@ -6,28 +6,16 @@ Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Infra.NatSet.
(**
Next define what a program is.
Currently no loops, only conditionals and assignments
Final return statement
Currently no loops, or conditionals.
Only assignments and return statement
**)
Inductive cmd (V:Type) :Type :=
Let: nat -> exp V -> cmd V -> cmd V
| Ret: exp V -> cmd V.
(*| Nop: cmd V. *)
(*
UNUSED!
Small Step semantics for Daisy language
Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
let_s x e s E v eps:
eval_exp eps E e v ->
sstep (Let x e s) E eps s (updEnv x v E)
|ret_s e E v eps:
eval_exp eps E e v ->
sstep (Ret e) E eps (Nop R) (updEnv 0 v E).
*)
(**
Analogously define Big Step semantics for the Daisy language
Define big step semantics for the Daisy language, terminating on a "returned"
result value
**)
Inductive bstep : cmd R -> env -> R -> R -> Prop :=
let_b x e s E v eps res:
......@@ -38,14 +26,31 @@ 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 :=
(**
The free variables of a command are all used variables of expressions
without the let bound variables
**)
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
| Let x e g => NatSet.remove x (NatSet.union (usedVars e) (freeVars g))
| Ret e => usedVars e
end.
Fixpoint definedVars (f:cmd Q) :NatSet.t :=
(**
The defined variables of a command are all let bound variables
**)
Fixpoint definedVars V (f:cmd V) :NatSet.t :=
match f with
| Let x _ g => NatSet.add x (definedVars g)
| Ret _ => NatSet.empty
end.
(**
The live variables of a command are all variables which occur on the right
hand side of an assignment or at a return statement
**)
Fixpoint liveVars V (f:cmd V) :NatSet.t :=
match f with
| Let _ e g => NatSet.union (usedVars e) (liveVars g)
| Ret e => usedVars e
end.
\ No newline at end of file
......@@ -17,7 +17,7 @@ Inductive approxEnv : env -> analysisResult -> NatSet.t -> NatSet.t -> env -> Pr
approxEnv emptyEnv A NatSet.empty NatSet.empty emptyEnv
|approxUpdFree E1 E2 A v1 v2 x fVars dVars:
approxEnv E1 A fVars dVars E2 ->
(Rabs (v1 - v2) <= v1 * Q2R machineEpsilon)%R ->
(Rabs (v1 - v2) <= Rabs v1 * Q2R machineEpsilon)%R ->
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:
......
......@@ -60,21 +60,21 @@ Proof.
rewrite (delta_0_deterministic (evalBinop Plus v1 v2) delta); auto.
unfold evalBinop in *; simpl in *.
clear delta H2.
rewrite (meps_0_deterministic H4 e1_real);
rewrite (meps_0_deterministic H3 e1_real);
rewrite (meps_0_deterministic H5 e2_real).
rewrite (meps_0_deterministic H4 e1_real) in plus_real.
rewrite (meps_0_deterministic H3 e1_real) in plus_real.
rewrite (meps_0_deterministic H5 e2_real) in plus_real.
clear H4 H5 v1 v2.
clear H3 H5 H6 v1 v2.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion plus_float; subst.
unfold perturb; simpl.
inversion H4; subst; inversion H5; subst.
inversion H3; subst; inversion H5; subst.
unfold updEnv; simpl.
unfold updEnv in H0,H1; simpl in *.
symmetry in H0, H1.
inversion H0; inversion H1; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear plus_float H4 H5 plus_real e1_real e1_float e2_real e2_float H0 H1.
clear plus_float H3 H5 plus_real e1_real e1_float e2_real e2_float H0 H1.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
......@@ -123,21 +123,21 @@ Proof.
rewrite delta_0_deterministic; auto.
unfold evalBinop in *; simpl in *.
clear delta H2.
rewrite (meps_0_deterministic H4 e1_real);
rewrite (meps_0_deterministic H3 e1_real);
rewrite (meps_0_deterministic H5 e2_real).
rewrite (meps_0_deterministic H4 e1_real) in sub_real.
rewrite (meps_0_deterministic H3 e1_real) in sub_real.
rewrite (meps_0_deterministic H5 e2_real) in sub_real.
clear H4 H5 v1 v2.
clear H3 H5 H6 v1 v2.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion sub_float; subst.
unfold perturb; simpl.
inversion H4; subst; inversion H5; subst.
inversion H3; subst; inversion H5; subst.
unfold updEnv; simpl.
symmetry in H0, H1.
unfold updEnv in H0, H1; simpl in H0, H1.
inversion H0; inversion H1; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear sub_float H4 H5 sub_real e1_real e1_float e2_real e2_float H0 H1.
clear sub_float H3 H5 sub_real e1_real e1_float e2_real e2_float H0 H1.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
repeat rewrite Rsub_eq_Ropp_Rplus.
......@@ -177,20 +177,20 @@ Proof.
rewrite delta_0_deterministic; auto.
unfold evalBinop in *; simpl in *.
clear delta H2.
rewrite (meps_0_deterministic H4 e1_real);
rewrite (meps_0_deterministic H3 e1_real);
rewrite (meps_0_deterministic H5 e2_real).
rewrite (meps_0_deterministic H4 e1_real) in mult_real.
rewrite (meps_0_deterministic H3 e1_real) in mult_real.
rewrite (meps_0_deterministic H5 e2_real) in mult_real.
clear H4 H5 v1 v2.
clear H3 H5 H6 v1 v2.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion mult_float; subst.
unfold perturb; simpl.
inversion H4; subst; inversion H5; subst.
inversion H3; subst; inversion H5; subst.
symmetry in H0, H1;
unfold updEnv in *; simpl in *.
inversion H0; inversion H1; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear mult_float H4 H5 mult_real e1_real e1_float e2_real e2_float H0 H1.
clear mult_float H3 H5 mult_real e1_real e1_float e2_real e2_float H0 H1.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
......@@ -224,20 +224,20 @@ Proof.
rewrite delta_0_deterministic; auto.
unfold evalBinop in *; simpl in *.
clear delta H2.
rewrite (meps_0_deterministic H4 e1_real);
rewrite (meps_0_deterministic H3 e1_real);
rewrite (meps_0_deterministic H5 e2_real).
rewrite (meps_0_deterministic H4 e1_real) in div_real.
rewrite (meps_0_deterministic H3 e1_real) in div_real.
rewrite (meps_0_deterministic H5 e2_real) in div_real.
clear H4 H5 v1 v2.
clear H3 H5 H6 v1 v2.
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
inversion div_float; subst.
unfold perturb; simpl.
inversion H4; subst; inversion H5; subst.
inversion H3; subst; inversion H5; subst.
symmetry in H0, H1;
unfold updEnv in *; simpl in *.
inversion H0; inversion H1; subst.
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
clear div_float H4 H5 div_real e1_real e1_float e2_real e2_float H0 H1.
clear div_float H3 H5 div_real e1_real e1_float e2_real e2_float H0 H1.
repeat rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rsub_eq_Ropp_Rplus.
......
This diff is collapsed.
(**
Formalization of the base expression language for the daisy framework
Required in all files, since we will always reason about expressions.
Formalization of the base expression language for the daisy framework
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet.
(**
Expressions will use binary operators.
......@@ -99,12 +99,9 @@ Definition perturb (r:R) (e:R) :=
(**
Define expression evaluation relation parametric by an "error" epsilon.
This value will be used later to express float computations using a perturbation
of the real valued computation by (1 + delta), where |delta| <= machine epsilon.
It is important that variables are not perturbed when loading from an environment.
This is the case, since loading a float value should not increase an additional error.
Unary negation is special! We do not have a new error here since IEE 754 gives us a sign bit
The result value expresses float computations according to the IEEE standard,
using a perturbation of the real valued computation by (1 + delta), where
|delta| <= machine epsilon.
**)
Inductive eval_exp (eps:R) (E:env) :(exp R) -> R -> Prop :=
| Var_load x v:
......@@ -124,18 +121,23 @@ Inductive eval_exp (eps:R) (E:env) :(exp R) -> R -> Prop :=
Rle (Rabs delta) eps ->
eval_exp eps E f1 v1 ->
eval_exp eps E f2 v2 ->
((op = Div) -> (~ v2 = 0)%R) ->
eval_exp eps E (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta).
Fixpoint freeVars (V:Type) (e:exp V) :NatSet.t :=
(**
Define the set of "used" variables of an expression to be the set of variables
occuring in it
**)
Fixpoint usedVars (V:Type) (e:exp V) :NatSet.t :=
match e with
| Var _ x => NatSet.singleton x
| Unop u e1 => freeVars e1
| Binop b e1 e2 => NatSet.union (freeVars e1) (freeVars e2)
| Unop u e1 => usedVars e1
| Binop b e1 e2 => NatSet.union (usedVars e1) (usedVars e2)
| _ => NatSet.empty
end.
(**
If |delta| <= 0 then perturb v delta is exactly v.
If |delta| <= 0 then perturb v delta is exactly v.
**)
Lemma delta_0_deterministic (v:R) (delta:R):
(Rabs delta <= 0)%R ->
......@@ -172,8 +174,7 @@ Qed.
Helping lemma. Needed in soundness proof.
For each evaluation of using an arbitrary epsilon, we can replace it by
evaluating the subexpressions and then binding the result values to different
variables in the Eironment.
This relies on the property that variables are not perturbed as opposed to parameters
variables in the Environment.
**)
Lemma binary_unfolding b f1 f2 eps E vF:
eval_exp eps E (Binop b f1 f2) vF ->
......@@ -218,15 +219,15 @@ Proof.
inversion H2; subst; auto.
Qed.
(**
Using the parametric expressions, define boolean expressions for conditionals
**)
Inductive bexp (V:Type) : Type :=
leq: exp V -> exp V -> bexp V
| less: exp V -> exp V -> bexp V.
(**
Define evaluation of booleans for reals
Define evaluation of boolean expressions
**)
Inductive bval (eps:R) (E:env): (bexp R) -> Prop -> Prop :=
leq_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R):
......
......@@ -16,7 +16,6 @@ define them to automatically unfold upon simplification.
**)
Definition interval:Type := R * R.
Definition err:Type := R.
Definition ann:Type := interval * err.
Definition mkInterval (ivlo:R) (ivhi:R) := (ivlo,ivhi).
Definition IVlo (intv:interval) := fst intv.
Definition IVhi (intv:interval) := snd intv.
......@@ -36,9 +35,6 @@ Arguments mkIntv _ _/.
Arguments ivlo _ /.
Arguments ivhi _ /.
Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
(**
Later we will argue about program preconditions.
Define a precondition to be a function mapping numbers (resp. variables) to intervals.
......@@ -50,10 +46,15 @@ Definition precond :Type := nat -> intv.
**)
Definition env := nat -> option R.
(**
The empty environment must return NONE for every variable
**)
Definition emptyEnv:env := fun _ => None.
(**
Define environment update function as abbreviation, for variable environments
**)
Definition updEnv (x:nat) (v: R) (E:env) (y:nat) :=
if y =? x
then Some v
......
......@@ -2,6 +2,10 @@
Require Import Coq.Bool.Bool Coq.Reals.Reals.
Require Import Daisy.Infra.RealSimps Daisy.Infra.NatSet.
Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
(** Automatic translation and destruction of conjuctinos with andb into Props **)
Ltac andb_to_prop H :=
apply Is_true_eq_left in H;
......
......@@ -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,30 +52,31 @@ 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.
Theorem ivbounds_approximatesPrecond_sound f absenv P V:
validIntervalbounds f absenv P V = true ->
forall v, NatSet.In v (NatSet.diff (Expressions.freeVars f) V) ->
forall v, NatSet.In v (NatSet.diff (usedVars f) V) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Var Q v)))).
Proof.
induction f; unfold validIntervalbounds.
......@@ -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.
......@@ -130,50 +137,27 @@ Qed.
Ltac env_assert absenv e name :=
assert (exists iv err, absenv e = (iv,err)) as name by (destruct (absenv e); repeat eexists; auto).
Lemma validBoundsDiv_uneq_zero e1 e2 absenv P V ivlo_e2 ivhi_e2 err:
absenv e2 = ((ivlo_e2,ivhi_e2), err) ->
validIntervalbounds (Binop Div e1 e2) absenv P V = true ->
(ivhi_e2 < 0) \/ (0 < ivlo_e2).
Proof.
intros absenv_eq validBounds.
unfold validIntervalbounds in validBounds.
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.
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].
apply Is_true_eq_true in nodiv0.
apply le_neq_bool_to_lt_prop; auto.
Qed.
Fixpoint getRetExp (V:Type) (f:cmd V) :=
match f with
|Let x e g => getRetExp g
| 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 (usedVars 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.