Skip to content

GitLab

Commit 2cb96884 authored by Heiko Becker's avatar Heiko Becker
Browse files
Options

WIP port to finite maps

parent fcf368ba
Hide whitespace changes
Inline Side-by-side
Showing with 184 additions and 169 deletions
coq/Environments.v
View file @ 2cb96884
......@@ -20,9 +20,10 @@ Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t
(Rabs (v1 - v2) <= (Rabs v1) * Q2R (mTypeToQ m))%R ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A (NatSet.add x fVars) dVars (updEnv x v2 E2)
|approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars m:
|approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars m iv err:
approxEnv E1 defVars A fVars dVars E2 ->
(Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R ->
DaisyMap.find (Var Q x) A = Some (iv, err) ->
(Rabs (v1 - v2) <= Q2R err)%R ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A fVars (NatSet.add x dVars) (updEnv x v2 E2).
......@@ -66,8 +67,8 @@ Proof.
set_tac.
rewrite NatSet.union_spec in x_valid.
destruct x_valid; set_tac.
rewrite NatSet.add_spec in H1.
destruct H1; subst; try auto.
rewrite NatSet.add_spec in H2.
destruct H2; subst; try auto.
rewrite Nat.eqb_refl in eq_case; congruence.
Qed.
......@@ -100,7 +101,7 @@ Proof.
- assert (x =? x0 = false) as x_x0_neq.
{ rewrite Nat.eqb_neq; hnf; intros; subst.
set_tac.
apply H0.
apply H1.
set_tac. }
unfold updEnv in *; rewrite x_x0_neq in *.
apply IHa; auto.
......@@ -108,12 +109,12 @@ Proof.
rewrite x_x0_neq in x_typed; auto.
Qed.
Lemma approxEnv_dVar_bounded v2 m e:
Lemma approxEnv_dVar_bounded v2 m iv e:
E1 x = Some v ->
E2 x = Some v2 ->
NatSet.In x dVars ->
Gamma x = Some m ->
snd (A (Var Q x)) = e ->
DaisyMap.find (Var Q x) A = Some (iv, e) ->
(Rabs (v - v2) <= Q2R e)%R.
Proof.
induction approxEnvs;
......@@ -132,7 +133,8 @@ Proof.
destruct x_def as [x_x0 | [x_neq x_def]]; subst.
+ unfold updEnv in *;
rewrite Nat.eqb_refl in *; simpl in *.
inversion E1_def; inversion E2_def; subst; auto.
inversion E1_def; inversion E2_def; subst.
rewrite A_e in *; inversion H; auto.
+ unfold updEnv in *; simpl in *.
rewrite <- Nat.eqb_neq in x_neq.
rewrite x_neq in *; simpl in *.
......
coq/Expressions.v
View file @ 2cb96884
(**
Formalization of the base expression language for the daisy framework
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith
Coq.QArith.Qreals Coq.Structures.Orders Coq.Structures.OrderedType
Coq.Structures.OrdersFacts.
From Coq
Require Import Reals.Reals micromega.Psatz QArith.QArith QArith.Qreals
Structures.Orders.
Require Import Daisy.Infra.RealRationalProps Daisy.Infra.RationalSimps
Daisy.Infra.Ltacs.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet
......@@ -194,8 +194,10 @@ Proof.
eapply IHe; eauto.
Qed.
Module ExpOrderedType (V_ordered:OrderedType) <: OrderedType.
Module V_orderedFacts := OrderedTypeFacts (V_ordered).
Module Type OrderType := Coq.Structures.Orders.OrderedType.
Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
Module V_orderedFacts := OrdersFacts.OrderedTypeFacts (V_ordered).
Definition V := V_ordered.t.
Definition t := exp V.
......
coq/Infra/Abbrevs.v
View file @ 2cb96884
......@@ -62,3 +62,15 @@ Definition updEnv (x:nat) (v: R) (E:env) (y:nat) :=
Definition updDefVars (x:nat) (m:mType) (defVars:nat -> option mType) (y:nat) :=
if (y =? x) then Some m else defVars y.
Definition optionLift (V T:Type) (v:option V) default (f: V -> T) :=
match v with
| None => default
| Some val => f val
end.
Ltac optionD :=
match goal with
|H: context[optionLift ?v ?default ?f] |- _ =>
destruct ?v eqn:?
end.
\ No newline at end of file
coq/Infra/ExpressionAbbrevs.v
View file @ 2cb96884
......@@ -2,11 +2,20 @@
Some abbreviations that require having defined expressions beforehand
If we would put them in the Abbrevs file, this would create a circular dependency which Coq cannot resolve.
**)
Require Import Coq.QArith.QArith Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Coq.QArith.QArith Coq.Reals.Reals Coq.QArith.Qreals Coq.QArith.QOrderedType Coq.FSets.FMapAVL Coq.FSets.FMapFacts.
Require Export Daisy.Infra.Abbrevs Daisy.Expressions.
Module Q_orderedExps := ExpOrderedType (Q_as_OT).
Module legacy_OrderedQExps := Structures.OrdersAlt.Backport_OT (Q_orderedExps).
Module DaisyMap := FMapAVL.Make(legacy_OrderedQExps).
Module DaisyMapFacts := OrdProperties (DaisyMap).
Definition analysisResult :Type := DaisyMap.t (intv * error).
(**
We treat a function mapping an expression arguing on fractions as value type
to pairs of intervals on rationals and rational errors as the analysis result
**)
Definition analysisResult :Type := exp Q -> intv * error.
\ No newline at end of file
(* Definition analysisResult :Type := exp Q -> intv * error. *)
\ No newline at end of file
coq/Infra/NatSet.v
View file @ 2cb96884
......@@ -55,26 +55,6 @@ Proof.
congruence.
Qed.
(** TODO: Merge with NatSet_prop tactic in Ltacs file **)
Ltac set_hnf_tac :=
match goal with
| [ H: NatSet.mem ?x _ = true |- _ ] => rewrite NatSet.mem_spec in H; set_hnf_tac
| [ H: NatSet.mem ?x _ = false |- _] => apply not_in_not_mem in H; set_hnf_tac
| [ |- context [NatSet.mem ?x _]] => rewrite NatSet.mem_spec; set_hnf_tac
| [ |- context [NatSet.In ?x (NatSet.union ?SA ?SB)]] => rewrite NatSet.union_spec; set_hnf_tac
| [ |- context [NatSet.In ?x (NatSet.diff ?A ?B)]] => rewrite NatSet.diff_spec; set_hnf_tac
| [ H: context [NatSet.In ?x (NatSet.diff ?A ?B)] |- _] => rewrite NatSet.diff_spec in H; destruct H; set_hnf_tac
| [ |- context [NatSet.In ?x (NatSet.singleton ?y)]] => rewrite NatSet.singleton_spec
| [ |- context [NatSet.Subset ?SA ?SB]] => hnf; intros; set_hnf_tac
| [ H: NatSet.Subset ?SA ?SB |- NatSet.In ?v ?SB] => apply H; set_hnf_tac
| _ => idtac
end.
Ltac set_tac :=
set_hnf_tac;
simpl in *; try auto.
Lemma add_spec_strong:
forall x y S,
(x ∈ (NatSet.add y S)) <-> x = y \/ ((~ (x = y)) /\ (x ∈ S)).
......@@ -91,3 +71,24 @@ Proof.
- rewrite NatSet.add_spec.
destruct x_in_add as [ x_eq | [x_neq x_in_S]]; auto.
Qed.
(** TODO: Merge with NatSet_prop tactic in Ltacs file **)
Ltac set_hnf_tac :=
match goal with
| [ H: NatSet.mem ?x _ = true |- _ ] => rewrite NatSet.mem_spec in H
| [ H: NatSet.mem ?x _ = false |- _] => apply not_in_not_mem in H
| [ H: context [NatSet.In ?x (NatSet.diff ?A ?B)] |- _] => rewrite NatSet.diff_spec in H; destruct H
| [ H: NatSet.Subset ?SA ?SB |- NatSet.In ?v ?SB] => apply H
| [ H: NatSet.In ?x (NatSet.singleton ?y) |- _] => apply NatSetProps.Dec.F.singleton_1 in H
| [ H: NatSet.In ?x NatSet.empty |- _ ] => inversion H
| [ H: NatSet.In ?x (NatSet.union ?S1 ?S2) |- _ ] => rewrite NatSet.union_spec in H
| [ |- context [NatSet.mem ?x _]] => rewrite NatSet.mem_spec
| [ |- context [NatSet.In ?x (NatSet.union ?SA ?SB)]] => rewrite NatSet.union_spec
| [ |- context [NatSet.In ?x (NatSet.diff ?A ?B)]] => rewrite NatSet.diff_spec
| [ |- context [NatSet.In ?x (NatSet.singleton ?y)]] => rewrite NatSet.singleton_spec
| [ |- context [NatSet.Subset ?SA ?SB]] => hnf; intros
end.
Ltac set_tac :=
repeat set_hnf_tac;
simpl in *; try auto.
coq/IntervalValidation.v
View file @ 2cb96884
......@@ -10,37 +10,42 @@ Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRat
Require Import Daisy.Infra.Ltacs Daisy.Infra.RealSimps Daisy.Typing.
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 && (Qleb (ivlo (P v)) (ivhi (P v)))
| Const _ n => isSupersetIntv (n,n) intv
| Unop o f =>
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 =>
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
Fixpoint validIntervalbounds (e:exp Q) (A:analysisResult) (P:precond) (validVars:NatSet.t) :bool:=
match DaisyMap.find e A with
| None => false
| Some (intv, _) =>
match e with
| 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 =>
if validIntervalbounds f A P validVars
then
match DaisyMap.find f A with
| None => false
| Some (iv, _) =>
match o with
| Neg =>
let new_iv := negateIntv iv in
isSupersetIntv new_iv intv
else false
| Inv =>
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
end
else false
| Binop op f1 f2 =>
if ((validIntervalbounds f1 absenv P validVars) &&
(validIntervalbounds f2 absenv P validVars))
if ((validIntervalbounds f1 A P validVars) &&
(validIntervalbounds f2 A P validVars))
then
let (iv1,_) := absenv f1 in
let (iv2,_) := absenv f2 in
match DaisyMap.find f1 A, DaisyMap.find f2 A with
| Some (iv1, _), Some (iv2, _) =>
match op with
| Plus =>
let new_iv := addIntv iv1 iv2 in
......@@ -59,83 +64,67 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) (vali
isSupersetIntv new_iv intv
else false
end
| _, _ => false
end
else false
| Downcast _ f1 =>
if (validIntervalbounds f1 absenv P validVars)
if (validIntervalbounds f1 A P validVars)
then
let (iv1, _) := absenv f1 in
match DaisyMap.find f1 A with
| None => false
| Some (iv1, _) =>
(* TODO: intv = iv1 might be a hard constraint... *)
(isSupersetIntv intv iv1) && (isSupersetIntv iv1 intv)
end
else
false
end.
end
end.
Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :bool:=
Fixpoint validIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P:precond) (validVars:NatSet.t) :bool:=
match f with
| Let m x e g =>
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
match DaisyMap.find e A, DaisyMap.find (Var Q x) A with
| Some ((e_lo,e_hi), _), Some ((x_lo, x_hi), _) =>
if (validIntervalbounds e A P validVars &&
Qeq_bool (e_lo) (x_lo) &&
Qeq_bool (e_hi) (x_hi))
then validIntervalboundsCmd g A P (NatSet.add x validVars)
else false
| _, _ => false
end
|Ret e =>
validIntervalbounds e absenv P validVars
validIntervalbounds e A 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.usedVars f) V) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Var Q v)))).
Theorem ivbounds_approximatesPrecond_sound f A P dVars iv err:
validIntervalbounds f A P dVars = true ->
forall v, NatSet.In v (NatSet.diff (Expressions.usedVars f) dVars) ->
DaisyMap.find (Var Q v) A = Some (iv, err) ->
Is_true(isSupersetIntv (P v) iv).
Proof.
induction f; unfold validIntervalbounds.
- simpl. intros approx_true v v_in_fV; simpl in *.
rewrite NatSet.diff_spec in v_in_fV.
rewrite NatSet.singleton_spec in v_in_fV;
destruct v_in_fV; subst.
destruct (absenv (Var Q n)); simpl in *.
case_eq (NatSet.mem n V); intros case_mem;
rewrite case_mem in approx_true; simpl in *.
+ rewrite NatSet.mem_spec in case_mem.
contradiction.
+ 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; simpl in *.
apply Is_true_eq_left in approx_unary_true.
simpl in *.
destruct (absenv (Unop u f)); destruct (absenv f); simpl in *.
apply andb_prop_elim in approx_unary_true.
destruct approx_unary_true.
induction f; cbn; intros approx_true var var_in_fV find_A; set_tac.
- subst.
rewrite find_A in *.
destruct (var mem dVars) eqn:?; set_tac; try congruence.
andb_to_prop approx_true; unfold isSupersetIntv.
apply andb_prop_intro; split;
apply Is_true_eq_left; auto.
- destruct (DaisyMap.find (Unop u f) A) as [[iv_u err_u] | ] eqn:?;
try congruence.
andb_to_prop approx_true.
apply IHf; try auto.
apply Is_true_eq_true; auto.
- intros approx_bin_true v v_in_fV.
simpl in v_in_fV.
rewrite NatSet.diff_spec in v_in_fV.
destruct v_in_fV as [ v_in_fV v_not_in_V].
rewrite NatSet.union_spec in v_in_fV.
apply Is_true_eq_left in approx_bin_true.
destruct (absenv (Binop b f1 f2)); destruct (absenv f1);
destruct (absenv f2); simpl in *.
apply andb_prop_elim in approx_bin_true.
destruct approx_bin_true.
apply andb_prop_elim in H.
set_tac.
- destruct (DaisyMap.find (Binop b f1 f2) A) as [[iv_b err_b] | ] eqn:?;
try congruence.
andb_to_prop approx_true.
destruct H.
destruct v_in_fV.
+ apply IHf1; try auto.
* apply Is_true_eq_true; auto.
* rewrite NatSet.diff_spec; split; auto.
+ apply IHf2; try auto.
* apply Is_true_eq_true; auto.
* rewrite NatSet.diff_spec; split; auto.
- intros approx_rnd_true v v_in_fV.
simpl in *; destruct (absenv (Downcast m f)); destruct (absenv f).
apply Is_true_eq_left in approx_rnd_true.
apply andb_prop_elim in approx_rnd_true.
destruct approx_rnd_true.
apply IHf; auto.
apply Is_true_eq_true in H; try auto.
+ apply IHf1; try auto; set_tac.
+ apply IHf2; try auto; set_tac.
- destruct (DaisyMap.find (Downcast m f) A) as [[iv_m err_m] | ] eqn:?;
try congruence.
andb_to_prop approx_true.
apply IHf; try auto; set_tac.
Qed.
Corollary Q2R_max4 a b c d:
......@@ -150,20 +139,20 @@ Proof.
unfold IntervalArith.min4, min4; repeat rewrite Q2R_min; auto.
Qed.
Ltac env_assert absenv e name :=
assert (exists iv err, absenv e = (iv,err)) as name by (destruct (absenv e); repeat eexists; auto).
Ltac env_assert A e name :=
assert (exists iv err, A e = (iv,err)) as name by (destruct (A 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 ->
Lemma validBoundsDiv_uneq_zero e1 e2 A P V ivlo_e2 ivhi_e2 err:
A e2 = ((ivlo_e2,ivhi_e2), err) ->
validIntervalbounds (Binop Div e1 e2) A P V = true ->
(ivhi_e2 < 0) \/ (0 < ivlo_e2).
Proof.
intros absenv_eq validBounds.
intros A_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.
env_assert A (Binop Div e1 e2) abs_div; destruct abs_div as [iv_div [err_div abs_div]].
env_assert A e1 abs_e1; destruct abs_e1 as [iv_e1 [err_e1 abs_e1]].
rewrite abs_div, abs_e1, A_eq in validBounds.
repeat (rewrite <- andb_lazy_alt in validBounds).
apply Is_true_eq_left in validBounds.
apply andb_prop_elim in validBounds.
......@@ -174,12 +163,12 @@ Proof.
apply le_neq_bool_to_lt_prop; auto.
Qed.
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond)
Theorem validIntervalbounds_sound (f:exp Q) (A:analysisResult) (P:precond)
fVars dVars (E:env) Gamma:
validIntervalbounds f absenv P dVars = true ->
validIntervalbounds f A 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) ->
(Q2R (fst (fst (A (Var Q v)))) <= vR <= Q2R (snd (fst (A (Var Q v)))))%R) ->
NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
(forall v, NatSet.mem v fVars = true ->
exists vR, E v = Some vR /\
......@@ -187,15 +176,15 @@ Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond)
(forall v, NatSet.mem v (NatSet.union fVars dVars) = true ->
exists m :mType, Gamma v = Some m) ->
exists vR, eval_exp E (toRMap Gamma) (toREval (toRExp f)) vR M0 /\
(Q2R (fst (fst (absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R.
(Q2R (fst (fst (A f))) <= vR <= Q2R (snd (fst (A f))))%R.
Proof.
induction f;
intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined;
simpl in *.
- env_assert absenv (Var Q n) absenv_var.
destruct absenv_var as [iv_n [err_n absenv_var]].
- env_assert A (Var Q n) A_var.
destruct A_var as [iv_n [err_n A_var]].
case_eq (NatSet.mem n dVars); intros dVars_case;
rewrite dVars_case, absenv_var in valid_bounds; simpl in *.
rewrite dVars_case, A_var in valid_bounds; simpl in *.
+ destruct (valid_definedVars n) as [vR [env_valid bounds_valid]]; try auto.
eexists; split; simpl; try eauto.
eapply Var_load; simpl; try auto.
......@@ -210,24 +199,24 @@ Proof.
* andb_to_prop valid_bounds.
unfold Qleb in *.
canonize_hyps.
rewrite absenv_var.
rewrite A_var.
simpl in *.
lra.
- exists (perturb (Q2R v) 0).
split; [econstructor; eauto; apply Rabs_0_equiv | ].
env_assert absenv (Const m v) absenv_const;
destruct absenv_const as [iv_v [err_v absenv_const]].
rewrite absenv_const in *; simpl in *.
env_assert A (Const m v) A_const;
destruct A_const as [iv_v [err_v A_const]].
rewrite A_const in *; simpl in *.
andb_to_prop valid_bounds.
canonize_hyps.
simpl in *; unfold perturb; lra.
- env_assert absenv (Unop u f) absenv_unop;
destruct absenv_unop as [iv_u [err_u absenv_unop]].
rewrite absenv_unop in *; simpl in *.
case_eq (validIntervalbounds f absenv P dVars);
- env_assert A (Unop u f) A_unop;
destruct A_unop as [iv_u [err_u A_unop]].
rewrite A_unop in *; simpl in *.
case_eq (validIntervalbounds f A P dVars);
intros case_bounds; rewrite case_bounds in *; try congruence.
env_assert absenv f absenv_f;
destruct absenv_f as [iv_f [ err_f absenv_f]]; rewrite absenv_f in *; simpl in *.
env_assert A f A_f;
destruct A_f as [iv_f [ err_f A_f]]; rewrite A_f in *; simpl in *.
destruct IHf as [vF [eval_f valid_bounds_f]]; try auto.
destruct u.
+ exists (evalUnop Neg vF); split; [econstructor; auto | ].
......@@ -278,17 +267,17 @@ Proof.
}
rewrite <- Q2R0_is_0 in H3.
apply Rlt_Qlt in H3. lra. }
- env_assert absenv (Binop b f1 f2) absenv_b;
destruct absenv_b as [iv_b [err_b absenv_b]].
env_assert absenv f1 absenv_f1;
destruct absenv_f1 as [iv_f1 [err_f1 absenv_f1]].
env_assert absenv f2 absenv_f2;
destruct absenv_f2 as [iv_f2 [err_f2 absenv_f2]].
rewrite absenv_b in *; simpl in *.
- env_assert A (Binop b f1 f2) A_b;
destruct A_b as [iv_b [err_b A_b]].
env_assert A f1 A_f1;
destruct A_f1 as [iv_f1 [err_f1 A_f1]].
env_assert A f2 A_f2;
destruct A_f2 as [iv_f2 [err_f2 A_f2]].
rewrite A_b in *; simpl in *.
andb_to_prop valid_bounds.
destruct IHf1 as [vF1 [eval_f1 valid_f1]]; try auto; set_tac.
destruct IHf2 as [vF2 [eval_f2 valid_f2]]; try auto; set_tac.
rewrite absenv_f1, absenv_f2 in *; simpl in *.
rewrite A_f1, A_f2 in *; simpl in *.
assert (M0 = join M0 M0) as M0_join by (cbv; auto);
rewrite M0_join.
exists (perturb (evalBinop b vF1 vF2) 0);
......@@ -356,11 +345,11 @@ Proof.
unfold perturb.
lra.
}
- env_assert absenv (Downcast m f) absenv_d;
destruct absenv_d as [iv_d [err_d absenv_d]];
env_assert absenv f absenv_f;
destruct absenv_f as [iv_f [err_f absenv_f]];
rewrite absenv_d, absenv_f in *; simpl in *.
- env_assert A (Downcast m f) A_d;
destruct A_d as [iv_d [err_d A_d]];
env_assert A f A_f;
destruct A_f as [iv_f [err_f A_f]];
rewrite A_d, A_f in *; simpl in *.
andb_to_prop valid_bounds.
destruct IHf as [vF [eval_f valid_f]]; try auto.
exists (perturb vF 0).
......@@ -428,32 +417,32 @@ Proof.
eapply swap_Gamma_eval_exp; eauto.
Qed.
Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult) Gamma:
Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult) Gamma:
forall E fVars dVars outVars elo ehi err P,
ssa f (NatSet.union fVars dVars) outVars ->
(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) ->
(Q2R (fst (fst (A (Var Q v)))) <= vR <= Q2R (snd (fst (A (Var Q v)))))%R) ->
(forall v, NatSet.mem v fVars = true ->
exists vR, E v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
(forall v, NatSet.mem v (NatSet.union fVars dVars) = true ->
exists m :mType, Gamma v = Some m) ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
validIntervalboundsCmd f absenv P dVars = true ->
absenv (getRetExp f) = ((elo, ehi), err) ->
validIntervalboundsCmd f A P dVars = true ->
A (getRetExp f) = ((elo, ehi), err) ->
exists vR,
bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR M0 /\
(Q2R elo <= vR <= Q2R ehi)%R.
Proof.
revert Gamma.
induction f;
intros * ssa_f dVars_sound fVars_valid types_valid usedVars_subset valid_bounds_f absenv_f.
intros * ssa_f dVars_sound fVars_valid types_valid usedVars_subset valid_bounds_f A_f.
- inversion ssa_f; subst.
unfold validIntervalboundsCmd in valid_bounds_f.
andb_to_prop valid_bounds_f.
inversion ssa_f; subst.
pose proof (validIntervalbounds_sound e absenv P E Gamma (fVars:=fVars) L) as validIV_e.
pose proof (validIntervalbounds_sound e A P E Gamma (fVars:=fVars) L) as validIV_e.
destruct validIV_e as [v [eval_e valid_bounds_e]]; try auto.
{ simpl in usedVars_subset.
hnf. intros a in_usedVars.
......@@ -536,8 +525,8 @@ Proof.
eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n M0 Gamma)) ; try eauto.
intros n1; erewrite Rmap_updVars_comm; eauto.
- unfold validIntervalboundsCmd in valid_bounds_f.
pose proof (validIntervalbounds_sound e absenv P E Gamma valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e.
pose proof (validIntervalbounds_sound e A P E Gamma valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e.
destruct valid_iv_e as [vR [eval_e valid_e]]; try auto.
simpl in *; rewrite absenv_f in *; simpl in *.
simpl in *; rewrite A_f in *; simpl in *.
exists vR; split; [econstructor; eauto | auto].
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