Commit 91b26b8d authored by Heiko Becker's avatar Heiko Becker

Alpha renaming and bug fixes

parent da33d515
......@@ -28,7 +28,7 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
(forall v, NatSet.mem v fVars = true ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
NatSet.Subset (Expressions.freeVars e) fVars ->
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 ->
......@@ -69,7 +69,7 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
NatSet.Subset (Commands.freeVars f) fVars ->
ssaPrg f fVars outVars ->
ssa f fVars outVars ->
bstep (toRCmd f) E1 0 vR ->
bstep (toRCmd f) E2 (Q2R machineEpsilon) vF ->
CertificateCheckerCmd f absenv P = true ->
......
......@@ -1936,7 +1936,7 @@ Qed.
Theorem validErrorbound_sound (e:exp Q):
forall E1 E2 fVars dVars absenv nR nF err P elo ehi,
approxEnv E1 absenv fVars dVars E2 ->
NatSet.Subset (NatSet.diff (Expressions.freeVars e) dVars) fVars ->
NatSet.Subset (NatSet.diff (usedVars e) dVars) fVars ->
eval_exp 0%R E1 (toRExp e) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e) nF ->
validErrorbound e absenv dVars = true ->
......@@ -2112,7 +2112,7 @@ Qed.
Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult):
forall E1 E2 outVars fVars dVars vR vF elo ehi err P,
approxEnv E1 absenv fVars dVars E2 ->
ssaPrg f (NatSet.union fVars dVars) outVars ->
ssa f (NatSet.union fVars dVars) outVars ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
bstep (toRCmd f) E1 0%R vR ->
bstep (toRCmd f) E2 (Q2R RationalSimps.machineEpsilon) vF ->
......@@ -2164,7 +2164,6 @@ Proof.
rewrite NatSet.remove_spec, NatSet.union_spec.
split; try auto.
hnf; intros; subst.
apply validVars_valid_subset in H2.
specialize (H2 n H3).
rewrite <- NatSet.mem_spec in H2.
rewrite H2 in *; congruence.
......@@ -2233,7 +2232,6 @@ Proof.
split; try auto.
split; try auto.
hnf; intros; subst.
apply validVars_valid_subset in H2.
specialize (H2 n a_mem_freeVars).
rewrite <- NatSet.mem_spec in H2.
rewrite H2 in *; congruence. }
......
......@@ -76,7 +76,7 @@ Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (v
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.
......@@ -169,7 +169,7 @@ Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond)
(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) ->
NatSet.Subset (NatSet.diff (Expressions.freeVars f) dVars) fVars ->
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) ->
......@@ -492,7 +492,7 @@ Qed.
Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult):
forall E vR fVars dVars outVars elo ehi err P,
ssaPrg f (NatSet.union fVars dVars) outVars ->
ssa f (NatSet.union fVars dVars) outVars ->
bstep (toRCmd f) E 0%R vR ->
(forall v, NatSet.mem v dVars = true ->
exists vR,
......@@ -548,7 +548,6 @@ Proof.
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. }
......
......@@ -82,19 +82,19 @@ Proof.
rewrite Rabs_R0; lra.
Qed.
Inductive ssaPrg (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop :=
Inductive ssa (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop :=
ssaLet x e s inVars Vterm:
NatSet.Subset (usedVars e) inVars->
NatSet.mem x inVars = false ->
ssaPrg s (NatSet.add x inVars) Vterm ->
ssaPrg (Let x e s) inVars Vterm
ssa s (NatSet.add x inVars) Vterm ->
ssa (Let x e s) inVars Vterm
|ssaRet e inVars Vterm:
NatSet.Subset (usedVars e) inVars ->
NatSet.Equal inVars Vterm ->
ssaPrg (Ret e) inVars Vterm.
ssa (Ret e) inVars Vterm.
Lemma ssa_subset_freeVars V (f:cmd V) inVars outVars:
ssaPrg f inVars outVars ->
ssa f inVars outVars ->
NatSet.Subset (Commands.freeVars f) inVars.
Proof.
intros ssa_f; induction ssa_f.
......@@ -113,8 +113,8 @@ Qed.
Lemma ssa_equal_set V (f:cmd V) inVars inVars' outVars:
NatSet.Equal inVars' inVars ->
ssaPrg f inVars outVars ->
ssaPrg f inVars' outVars.
ssa f inVars outVars ->
ssa f inVars' outVars.
Proof.
intros set_eq ssa_f.
revert set_eq; revert inVars'.
......@@ -142,7 +142,7 @@ Fixpoint validSSA (f:cmd Q) (inVars:NatSet.t) :=
Lemma validSSA_sound f inVars:
validSSA f inVars = true ->
exists outVars, ssaPrg f inVars outVars.
exists outVars, ssa f inVars outVars.
Proof.
revert inVars; induction f.
- intros inVars validSSA_let.
......@@ -163,7 +163,7 @@ Proof.
Qed.
Lemma ssa_shadowing_free x y v v' e f inVars outVars E:
ssaPrg (Let x e f) inVars outVars ->
ssa (Let x e f) inVars outVars ->
NatSet.In y inVars ->
eval_exp 0 E (toRExp e) v ->
forall E n, updEnv x v (updEnv y v' E) n = updEnv y v' (updEnv x v E) n.
......@@ -339,7 +339,7 @@ Fixpoint map_subst (f:cmd Q) x e :=
end.
Lemma stepwise_substitution x e v f E vR inVars outVars:
ssaPrg f inVars outVars ->
ssa f inVars outVars ->
NatSet.In x inVars ->
NatSet.Subset (usedVars e) inVars ->
eval_exp 0%R E (toRExp e) v ->
......@@ -400,7 +400,7 @@ Fixpoint let_subst (f:cmd Q) :=
end.
Theorem let_free_form f E vR inVars outVars e:
ssaPrg f inVars outVars ->
ssa f inVars outVars ->
bstep (toRCmd f) E 0 vR ->
let_subst f = Some e ->
bstep (toRCmd (Ret e)) E 0 vR.
......@@ -432,7 +432,7 @@ Qed.
(*
Lemma ssa_non_stuck (f:cmd Q) (inVars outVars:NatSet.t) (VarEnv:var_env)
(ParamEnv:param_env) (P:precond) (eps:R):
ssaPrg Q f inVars outVars ->
ssa Q f inVars outVars ->
(forall v, NatSet.In v (freeVars e) ->
(Q2R (ivlo (P v)) <= ParamEnv v <= Q2R (ivhi (P v))))%R ->
(forall v, NatSet.In v inVars ->
......
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