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

Implement let-Bindings in Coq and show soundness of let checker

parent 5b919837
...@@ -5,15 +5,15 @@ ...@@ -5,15 +5,15 @@
as shown in the soundness theorem. as shown in the soundness theorem.
**) **)
Require Import Coq.Reals.Reals Coq.QArith.Qreals. Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps. Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs.
Require Import Daisy.IntervalValidation Daisy.ErrorValidation. Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments.
Require Export Coq.QArith.QArith. Require Export Coq.QArith.QArith.
Require Export Daisy.Infra.ExpressionAbbrevs. Require Export Daisy.Infra.ExpressionAbbrevs.
(** Certificate checking function **) (** Certificate checking function **)
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) := Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
andb (validIntervalbounds e absenv P) (validErrorbound e absenv). andb (validIntervalbounds e absenv P NatSet.empty) (validErrorbound e absenv).
(** (**
Soundness proof for the certificate checker. Soundness proof for the certificate checker.
...@@ -22,9 +22,10 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) := ...@@ -22,9 +22,10 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
This property is expressed by the predicate precondValidForExec. This property is expressed by the predicate precondValidForExec.
**) **)
Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P: Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
forall (cenv:env) (vR:R) (vF:R), forall (VarEnv1 VarEnv2 ParamEnv:env) (vR:R) (vF:R),
eval_exp 0%R cenv P (toRExp e) vR -> approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp (Q2R machineEpsilon) cenv P (toRExp e) vF -> eval_exp 0%R VarEnv1 ParamEnv P (toRExp e) vR ->
eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e) vF ->
CertificateChecker e absenv P = true -> CertificateChecker e absenv P = true ->
(Rabs (vR - vF) <= Q2R (snd (absenv e)))%R. (Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
(** (**
...@@ -32,17 +33,50 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P: ...@@ -32,17 +33,50 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
validator and the error bound validator. validator and the error bound validator.
**) **)
Proof. Proof.
intros cenv vR vF eval_real eval_float certificate_valid. intros VarEnv1 VarEnv2 ParamEnv vR vF approxC1C2 eval_real eval_float certificate_valid.
unfold CertificateChecker in certificate_valid. unfold CertificateChecker in certificate_valid.
apply Is_true_eq_left in certificate_valid. andb_to_prop certificate_valid.
apply andb_prop_elim in certificate_valid.
destruct certificate_valid as [iv_valid errorbound_valid].
apply Is_true_eq_true in iv_valid;
apply Is_true_eq_true in errorbound_valid.
assert (exists iv err, absenv e = (iv,err)) by (destruct (absenv e); repeat eexists). assert (exists iv err, absenv e = (iv,err)) by (destruct (absenv e); repeat eexists).
destruct H as [iv [err absenv_eq]]. destruct H as [iv [err absenv_eq]].
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) by (destruct iv; repeat eexists). assert (exists ivlo ivhi, iv = (ivlo, ivhi)) by (destruct iv; repeat eexists).
destruct H as [ivlo [ ivhi iv_eq]]. destruct H as [ivlo [ ivhi iv_eq]].
subst; rewrite absenv_eq in *; simpl in *. subst; rewrite absenv_eq in *; simpl in *.
eapply (validErrorbound_sound e cenv absenv vR vF err P); eauto. 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.
Qed.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :=
andb (validIntervalboundsCmd f absenv P NatSet.empty)
(validErrorboundCmd f absenv).
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
forall (VarEnv1 VarEnv2 ParamEnv:env) outVars envR envF,
approxEnv VarEnv1 absenv VarEnv2 ->
ssaPrg Q f NatSet.empty outVars ->
bstep (toRCmd f) VarEnv1 ParamEnv P 0 (Nop R) envR ->
bstep (toRCmd f) VarEnv2 ParamEnv P (Q2R machineEpsilon) (Nop R) envF ->
CertificateCheckerCmd f absenv P = true ->
(Rabs (envR 0%nat - envF 0%nat) <= Q2R (snd (absenv (Var Q 0))))%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.
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).
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.
Qed. Qed.
\ No newline at end of file
...@@ -3,7 +3,7 @@ ...@@ -3,7 +3,7 @@
FIXME: Currently the semantics are stateful. But daisy actually assumes that a variable may not be verwritten? FIXME: Currently the semantics are stateful. But daisy actually assumes that a variable may not be verwritten?
**) **)
Require Import Coq.Reals.Reals. Require Import Coq.Reals.Reals.
Require Import Daisy.Expressions. Require Export Daisy.Infra.ExpressionAbbrevs.
(** (**
Next define what a program is. Next define what a program is.
Currently no loops, only conditionals and assignments Currently no loops, only conditionals and assignments
......
...@@ -97,18 +97,20 @@ Qed. ...@@ -97,18 +97,20 @@ Qed.
(** (**
Copy-Paste proof with minor differences, was easier then manipulating the evaluations and then applying the lemma Copy-Paste proof with minor differences, was easier then manipulating the evaluations and then applying the lemma
**) **)
Lemma subtract_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (VarEnv ParamEnv:nat->R) P (err1:R) (err2:R): Lemma subtract_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R)
eval_exp 0%R VarEnv ParamEnv P e1 e1R -> (e2F:R) (vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:nat->R) P absenv:
eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P e1 e1F -> approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv ParamEnv P e2 e2R -> eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P e2 e2F -> eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
eval_exp 0%R VarEnv ParamEnv P (Binop Sub e1 e2) vR -> eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv)) ParamEnv P (Binop Sub (Var R 1) (Var R 2)) vF -> eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) e2F ->
(Rabs (e1R - e1F) <= err1)%R -> eval_exp 0%R VarEnv1 ParamEnv P (Binop Sub (toRExp e1) (toRExp e2)) vR ->
(Rabs (e2R - e2F) <= err2)%R -> eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Sub (Var R 1) (Var R 2)) vF ->
(Rabs (vR - vF) <= err1 + err2 + ((Rabs (e1F - e2F)) * (Q2R machineEpsilon)))%R. (Rabs (e1R - e1F) <= Q2R (snd (absenv e1)))%R ->
(Rabs (e2R - e2F) <= Q2R (snd (absenv e2)))%R ->
(Rabs (vR - vF) <= Q2R (snd (absenv e1)) + Q2R (snd (absenv e2)) + ((Rabs (e1F - e2F)) * (Q2R machineEpsilon)))%R.
Proof. Proof.
intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2. intros approxCEnv e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *) (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
inversion sub_real; subst. inversion sub_real; subst.
rewrite delta_0_deterministic in sub_real; auto. rewrite delta_0_deterministic in sub_real; auto.
...@@ -149,16 +151,18 @@ Proof. ...@@ -149,16 +151,18 @@ Proof.
eapply Rmult_le_compat_l; [apply Rabs_pos | auto]. eapply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed. Qed.
Lemma mult_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (VarEnv ParamEnv:env) (P:precond) (err1:R) (err2:R): Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
eval_exp 0%R VarEnv ParamEnv P e1 e1R -> (vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond) absenv:
eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P e1 e1F -> approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv ParamEnv P e2 e2R -> eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P e2 e2F -> eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
eval_exp 0%R VarEnv ParamEnv P (Binop Mult e1 e2) vR -> eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv)) ParamEnv P (Binop Mult (Var R 1) (Var R 2)) vF -> eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) e2F ->
eval_exp 0%R VarEnv1 ParamEnv P (Binop Mult (toRExp e1) (toRExp e2)) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Mult (Var R 1) (Var R 2)) vF ->
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R machineEpsilon))%R. (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R machineEpsilon))%R.
Proof. Proof.
intros e1_real e1_float e2_real e2_float mult_real mult_float. intros approxCEnv e1_real e1_float e2_real e2_float mult_real mult_float.
(* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *) (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
inversion mult_real; subst. inversion mult_real; subst.
rewrite delta_0_deterministic in mult_real; auto. rewrite delta_0_deterministic in mult_real; auto.
...@@ -193,16 +197,18 @@ Proof. ...@@ -193,16 +197,18 @@ Proof.
apply Rabs_pos. apply Rabs_pos.
Qed. Qed.
Lemma div_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (VarEnv ParamEnv:env) (P:precond) (err1:R) (err2:R): Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
eval_exp 0%R VarEnv ParamEnv P e1 e1R -> (vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond) absenv:
eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P e1 e1F -> approxEnv VarEnv1 absenv VarEnv2 ->
eval_exp 0%R VarEnv ParamEnv P e2 e2R -> eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
eval_exp (Q2R machineEpsilon) VarEnv ParamEnv P e2 e2F -> eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
eval_exp 0%R VarEnv ParamEnv P (Binop Div e1 e2) vR -> eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv)) ParamEnv P (Binop Div (Var R 1) (Var R 2)) vF -> eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) e2F ->
eval_exp 0%R VarEnv1 ParamEnv P (Binop Div (toRExp e1) (toRExp e2)) vR ->
eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Div (Var R 1) (Var R 2)) vF ->
(Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R machineEpsilon))%R. (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R machineEpsilon))%R.
Proof. Proof.
intros e1_real e1_float e2_real e2_float div_real div_float. intros approxCenv e1_real e1_float e2_real e2_float div_real div_float.
(* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *) (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
inversion div_real; subst. inversion div_real; subst.
rewrite delta_0_deterministic in div_real; auto. rewrite delta_0_deterministic in div_real; auto.
......
This diff is collapsed.
...@@ -7,7 +7,8 @@ ...@@ -7,7 +7,8 @@
**) **)
Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List Coq.micromega.Psatz. Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List Coq.micromega.Psatz.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps. Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.RealSimps. Require Import Daisy.Infra.Ltacs Daisy.Infra.RealSimps.
Require Export Daisy.IntervalArithQ Daisy.IntervalArith Daisy.ssaPrgs.
Import Lists.List.ListNotations. Import Lists.List.ListNotations.
...@@ -20,14 +21,14 @@ Fixpoint freeVars (V:Type) (f:exp V) : list nat:= ...@@ -20,14 +21,14 @@ Fixpoint freeVars (V:Type) (f:exp V) : list nat:=
|Binop o f1 f2 => (freeVars V f1) ++ (freeVars V f2) |Binop o f1 f2 => (freeVars V f1) ++ (freeVars V f2)
end. end.
Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):= Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) validVars :=
let (intv, _) := absenv e in let (intv, _) := absenv e in
match e with match e with
| Var _ v => false | Var _ v => NatSet.mem v validVars
| Param _ v => isSupersetIntv (P v) intv | Param _ v => isSupersetIntv (P v) intv
| Const n => isSupersetIntv (n,n) intv | Const n => isSupersetIntv (n,n) intv
| Unop o f => | Unop o f =>
let rec := validIntervalbounds f absenv P in let rec := validIntervalbounds f absenv P validVars in
let (iv, _) := absenv f in let (iv, _) := absenv f in
let opres := let opres :=
match o with match o with
...@@ -44,7 +45,7 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):= ...@@ -44,7 +45,7 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
in in
andb rec opres andb rec opres
| Binop op f1 f2 => | Binop op f1 f2 =>
let rec := andb (validIntervalbounds f1 absenv P) (validIntervalbounds f2 absenv P) in let rec := andb (validIntervalbounds f1 absenv P validVars) (validIntervalbounds f2 absenv P validVars) in
let (iv1,_) := absenv f1 in let (iv1,_) := absenv f1 in
let (iv2,_) := absenv f2 in let (iv2,_) := absenv f2 in
let opres := let opres :=
...@@ -69,8 +70,22 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):= ...@@ -69,8 +70,22 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
andb rec opres andb rec opres
end. end.
Theorem ivbounds_approximatesPrecond_sound f absenv P: Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) validVars {struct f} :bool:=
validIntervalbounds f absenv P = true -> 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)
|Ret _ e =>
validIntervalbounds e absenv P validVars &&
(Qeq_bool (fst (fst (absenv e))) (fst (fst (absenv (Var Q 0)))) &&
Qeq_bool (snd (fst (absenv e))) (snd (fst (absenv (Var Q 0)))))
|Nop _ => false
end.
Theorem ivbounds_approximatesPrecond_sound f absenv P V:
validIntervalbounds f absenv P V = true ->
forall v, In v (freeVars Q f) -> forall v, In v (freeVars Q f) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v)))). Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v)))).
Proof. Proof.
...@@ -121,9 +136,9 @@ Qed. ...@@ -121,9 +136,9 @@ Qed.
Ltac env_assert absenv e name := Ltac env_assert absenv e name :=
assert (exists iv err, absenv e = (iv,err)) as name by (destruct (absenv e); repeat eexists; auto). 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 ivlo_e2 ivhi_e2 err: Lemma validBoundsDiv_uneq_zero e1 e2 absenv P V ivlo_e2 ivhi_e2 err:
absenv e2 = ((ivlo_e2,ivhi_e2), err) -> absenv e2 = ((ivlo_e2,ivhi_e2), err) ->
validIntervalbounds (Binop Div e1 e2) absenv P = true -> validIntervalbounds (Binop Div e1 e2) absenv P V = true ->
(ivhi_e2 < 0) \/ (0 < ivlo_e2). (ivhi_e2 < 0) \/ (0 < ivlo_e2).
Proof. Proof.
intros absenv_eq validBounds. intros absenv_eq validBounds.
...@@ -139,19 +154,24 @@ Proof. ...@@ -139,19 +154,24 @@ Proof.
apply le_neq_bool_to_lt_prop; auto. apply le_neq_bool_to_lt_prop; auto.
Qed. Qed.
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) VarEnv ParamEnv: Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) V VarEnv ParamEnv:
forall vR, forall vR,
(* precondValidForExec P cenv ->*) (* precondValidForExec P cenv ->*)
validIntervalbounds f absenv P = true -> validIntervalbounds f absenv P V = true ->
(forall v, NatSet.mem v V = true ->
(Q2R (fst (fst (absenv (Var Q v)))) <= VarEnv v <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
eval_exp 0%R VarEnv ParamEnv P (toRExp f) vR -> eval_exp 0%R VarEnv ParamEnv P (toRExp f) vR ->
(Q2R (fst (fst(absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R. (Q2R (fst (fst(absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R.
Proof. Proof.
induction f. induction f; intros vR valid_bounds valid_freeVars eval_f.
- intros vR valid_bounds eval_f. - unfold validIntervalbounds in valid_bounds.
unfold validIntervalbounds in valid_bounds. env_assert absenv (Var Q n) absenv_var.
destruct (absenv (Var Q n)); inversion valid_bounds. destruct absenv_var as [ iv [err absenv_var]].
- intros vR valid_bounds eval_f. specialize (valid_freeVars n).
pose proof (ivbounds_approximatesPrecond_sound (Param Q n) absenv P valid_bounds) as env_approx_p. rewrite absenv_var in *; simpl in *.
inversion eval_f; subst.
apply valid_freeVars; auto.
- pose proof (ivbounds_approximatesPrecond_sound (Param Q n) absenv P V valid_bounds) as env_approx_p.
unfold validIntervalbounds in valid_bounds. unfold validIntervalbounds in valid_bounds.
case_eq (absenv (Param Q n)). case_eq (absenv (Param Q n)).
intros intv err absenv_n. intros intv err absenv_n.
...@@ -177,8 +197,7 @@ Proof. ...@@ -177,8 +197,7 @@ Proof.
rewrite delta_0_deterministic in *; auto. rewrite delta_0_deterministic in *; auto.
rewrite delta_0_deterministic in *; auto. rewrite delta_0_deterministic in *; auto.
split; lra. split; lra.
- intros vR valid_bounds eval_f. - unfold validIntervalbounds in valid_bounds.
unfold validIntervalbounds in valid_bounds.
destruct (absenv (Const v)) as [intv err]; simpl. destruct (absenv (Const v)) as [intv err]; simpl.
apply Is_true_eq_left in valid_bounds. apply Is_true_eq_left in valid_bounds.
apply andb_prop_elim in valid_bounds. apply andb_prop_elim in valid_bounds.
...@@ -195,8 +214,7 @@ Proof. ...@@ -195,8 +214,7 @@ Proof.
unfold Qleb in *. unfold Qleb in *.
apply Qle_bool_iff in valid_hi. apply Qle_bool_iff in valid_hi.
apply Qle_Rle in valid_hi; auto. apply Qle_Rle in valid_hi; auto.
- intros vR valid_bounds eval_f. - case_eq (absenv (Unop u f)); intros intv err absenv_unop.
case_eq (absenv (Unop u f)); intros intv err absenv_unop.
destruct intv as [unop_lo unop_hi]; simpl. destruct intv as [unop_lo unop_hi]; simpl.
unfold validIntervalbounds in valid_bounds. unfold validIntervalbounds in valid_bounds.
rewrite absenv_unop in valid_bounds. rewrite absenv_unop in valid_bounds.
...@@ -207,7 +225,7 @@ Proof. ...@@ -207,7 +225,7 @@ Proof.
destruct valid_bounds as [valid_rec valid_unop]. destruct valid_bounds as [valid_rec valid_unop].
apply Is_true_eq_true in valid_rec. apply Is_true_eq_true in valid_rec.
inversion eval_f; subst. inversion eval_f; subst.
+ specialize (IHf v1 valid_rec H2). + specialize (IHf v1 valid_rec valid_freeVars H2).
rewrite absenv_f in IHf; simpl in IHf. rewrite absenv_f in IHf; simpl in IHf.
(* TODO: Make lemma *) (* TODO: Make lemma *)
unfold isSupersetIntv in valid_unop. unfold isSupersetIntv in valid_unop.
...@@ -225,7 +243,7 @@ Proof. ...@@ -225,7 +243,7 @@ Proof.
* eapply Rle_trans. * eapply Rle_trans.
Focus 2. apply valid_hi. Focus 2. apply valid_hi.
rewrite Q2R_opp; lra. rewrite Q2R_opp; lra.
+ specialize (IHf v1 valid_rec H3). + specialize (IHf v1 valid_rec valid_freeVars H3).
rewrite absenv_f in IHf; simpl in IHf. rewrite absenv_f in IHf; simpl in IHf.
apply andb_prop_elim in valid_unop. apply andb_prop_elim in valid_unop.
destruct valid_unop as [valid_unop nodiv0]. destruct valid_unop as [valid_unop nodiv0].
...@@ -293,7 +311,7 @@ Proof. ...@@ -293,7 +311,7 @@ Proof.
rewrite <- Q2R0_is_0 in nodiv0_pos. rewrite <- Q2R0_is_0 in nodiv0_pos.
apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra. apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra.
} }
- intros vR valid_bounds eval_f; inversion eval_f; subst. - inversion eval_f; subst.
rewrite delta_0_deterministic in eval_f; auto. rewrite delta_0_deterministic in eval_f; auto.
rewrite delta_0_deterministic; auto. rewrite delta_0_deterministic; auto.
simpl in valid_bounds. simpl in valid_bounds.
...@@ -307,8 +325,8 @@ Proof. ...@@ -307,8 +325,8 @@ Proof.
apply andb_prop_elim in valid_rec. apply andb_prop_elim in valid_rec.
destruct valid_rec as [valid_e1 valid_e2]. destruct valid_rec as [valid_e1 valid_e2].
apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in valid_e2. apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in valid_e2.
specialize (IHf1 v1 valid_e1 H4); specialize (IHf1 v1 valid_e1 valid_freeVars H4);
specialize (IHf2 v2 valid_e2 H5). specialize (IHf2 v2 valid_e2 valid_freeVars H5).
rewrite absenv_f1 in IHf1. rewrite absenv_f1 in IHf1.
rewrite absenv_f2 in IHf2. rewrite absenv_f2 in IHf2.
destruct b; simpl in *. destruct b; simpl in *.
...@@ -439,3 +457,131 @@ Proof. ...@@ -439,3 +457,131 @@ Proof.
repeat rewrite <- Q2R_mult in valid_div_hi. repeat rewrite <- Q2R_mult in valid_div_hi.
rewrite <- Q2R_max4 in valid_div_hi; auto. } rewrite <- Q2R_max4 in valid_div_hi; auto. }
Qed. Qed.
Theorem ssaVars_are_sound (f:cmd Q) freeVars outVars (absenv:analysisResult)
(v_lo v_hi err:R) VarEnv ParamEnv P TEnv:
ssaPrg Q f (freeVars) (outVars) ->
bstep (toRCmd f) VarEnv ParamEnv P 0%R (Nop R) TEnv ->
(forall v, NatSet.mem v freeVars = true ->
(Q2R (fst (fst (absenv (Var Q v)))) <= VarEnv v <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
validIntervalboundsCmd f absenv P (freeVars) = true ->
forall v:nat, NatSet.mem v outVars = true ->
(Q2R (fst (fst (absenv (Var Q v)))) <= TEnv v <= Q2R (snd (fst (absenv (Var Q v)))))%R.
Proof.
intros ssa_f.
revert VarEnv.
induction ssa_f; intros VarEnv bstep_f freeVars_sound validBounds v in_outVars;
unfold validIntervalbounds in validBounds;
andb_to_prop validBounds.
- (* First rename auto-generated hyp names*)
rename L into eq_lo;
rename R1 into eq_hi;
rename L0 into validBounds_e.
inversion bstep_f; subst.
eapply IHssa_f; eauto.
+ intros v1 mem_Vx.
rewrite NatSet.mem_spec, NatSet.add_spec in mem_Vx.
unfold updEnv.
case_eq (v1 =? x); intros v1_eq_dec.
* assert (Q2R (fst (fst (absenv e))) <= v0 <= Q2R (snd (fst (absenv e))))%R
as validIV_e by (eapply validIntervalbounds_sound; eauto).
rewrite Nat.eqb_eq in v1_eq_dec.
rewrite v1_eq_dec.
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 <- eq_lo, <- eq_hi.
auto.
* destruct mem_Vx.
{ subst.
rewrite Nat.eqb_neq in v1_eq_dec.
hnf in v1_eq_dec.
exfalso. apply v1_eq_dec. reflexivity. }
{ apply freeVars_sound.
rewrite NatSet.mem_spec; auto. }
- rename H into eq_V_Vterm.
rewrite NatSet.equal_spec in eq_V_Vterm.
rewrite NatSet.mem_spec in in_outVars.
hnf in eq_V_Vterm.
rewrite <- eq_V_Vterm in in_outVars.
rewrite <- NatSet.mem_spec in in_outVars.
inversion bstep_f; subst.
unfold updEnv.
case_eq (v =? 0); intros v_eq.
+ assert (Q2R (fst (fst (absenv e))) <= v0 <= Q2R (snd (fst (absenv e))))%R
by (eapply validIntervalbounds_sound; eauto).
rename L0 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 v_eq.
subst.
rewrite <- eq_lo, <- eq_hi.
assumption.
+ apply freeVars_sound; auto.
Qed.
Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult):
forall VarEnv ParamEnv envR inVars outVars elo ehi err P,
ssaPrg Q f inVars outVars ->
bstep (toRCmd f) VarEnv ParamEnv P 0%R (Nop R) envR ->
(forall v, NatSet.mem v inVars = true ->
(Q2R (fst (fst (absenv (Var Q v)))) <= VarEnv v <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
validIntervalboundsCmd f absenv P inVars = true ->
absenv (Var Q 0%nat) = ((elo,ehi),err) ->
(Q2R elo <= envR (0%nat) <= Q2R ehi)%R.
Proof.
induction f;
intros VarEnv ParamEnv envR inVars outVars elo ehi err P
ssa_f eval_f freeVars_def 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.
eapply IHf; eauto.
intros v0 mem_v0.
unfold updEnv.
case_eq (v0 =? n); intros v0_eq.
+ assert (Q2R (fst (fst (absenv e))) <= v <= Q2R (snd (fst (absenv e))))%R
by (eapply validIntervalbounds_sound; eauto).
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.
assumption.
+ apply freeVars_def. rewrite NatSet.mem_spec.
rewrite NatSet.mem_spec in mem_v0.
rewrite NatSet.add_spec in mem_v0.
destruct mem_v0.
* rewrite Nat.eqb_neq in v0_eq.
exfalso; apply v0_eq; auto.
* assumption.
- unfold validIntervalboundsCmd in valid_bounds_f.
andb_to_prop valid_bounds_f.
inversion eval_f; subst.
unfold updEnv.
assert (0 =? 0 = true) as refl0 by (apply Nat.eqb_refl).
rewrite refl0.
assert (Q2R (fst (fst (absenv e))) <= v <= Q2R (snd (fst (absenv e))))%R
by (eapply validIntervalbounds_sound; eauto).
rename L0 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.
subst.