Skip to content

GitLab

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

Show substitution properties for ssa programs

parent 3747df48
Hide whitespace changes
Inline Side-by-side
Showing with 323 additions and 0 deletions
coq/ssaPrgs.v
View file @ abe26619
......@@ -91,6 +91,329 @@ Proof.
rewrite Rabs_R0; lra.
Qed.
Fixpoint validSSA (f:cmd Q) (inVars:NatSet.t) :=
match f with
|Let x e g =>
andb (andb (negb (NatSet.mem x inVars)) (validVars e inVars)) (validSSA g (NatSet.add x inVars))
|Ret e => validVars e inVars && (negb (NatSet.mem 0%nat inVars))
end.
Lemma validSSA_sound f inVars:
validSSA f inVars = true ->
exists outVars, ssaPrg f inVars outVars.
Proof.
revert inVars; induction f.
- intros inVars validSSA_let.
simpl in *.
andb_to_prop validSSA_let.
specialize (IHf (NatSet.add n inVars) R).
destruct IHf as [outVars IHf].
exists outVars.
constructor; eauto.
rewrite negb_true_iff in L0. auto.
- intros inVars validSSA_ret.
simpl in *.
exists (NatSet.add 0%nat inVars).
andb_to_prop validSSA_ret.
constructor; auto.
rewrite negb_true_iff in R.
hnf in R.
rewrite NatSet.equal_spec.
hnf.
intros a.
rewrite NatSet.remove_spec, NatSet.add_spec.
split.
+ intros in_inVars.
case_eq (a =? 0%nat).
* intros a_zero.
rewrite Nat.eqb_eq in a_zero.
rewrite a_zero in in_inVars.
rewrite <- NatSet.mem_spec in in_inVars.
rewrite in_inVars in R.
inversion R.
* intros a_neq_zero. apply beq_nat_false in a_neq_zero.
split; auto.
+ intros in_add_rem.
destruct in_add_rem as [ [a_zero | a_inVars] a_neq_zero]; try auto.
exfalso; eauto.
Qed.
Lemma ssa_shadowing_free x y v v' e f inVars outVars E P:
ssaPrg (Let x e f) inVars outVars ->
NatSet.In y inVars ->
eval_exp 0 E P (toRExp e) v ->
forall E n, updEnv x v (updEnv y v' E) n = updEnv y v' (updEnv x v E) n.
Proof.
intros ssa_let y_free eval_e.
inversion ssa_let; subst.
intros E' n; unfold updEnv.
case_eq (n =? x).
- intros n_eq_x.
rewrite Nat.eqb_eq in n_eq_x.
case_eq (n =? y); try auto.
intros n_eq_y.
rewrite Nat.eqb_eq in n_eq_y.
rewrite n_eq_x in n_eq_y.
rewrite <- n_eq_y in y_free.
rewrite <- NatSet.mem_spec in y_free.
rewrite y_free in H5. inversion H5.
- intros n_neq_x.
case_eq (n =? y); auto.
Qed.
Lemma shadowing_free_rewriting_exp e v E1 E2 P:
(forall n, E1 n = E2 n) ->
eval_exp 0 E1 P e v <->
eval_exp 0 E2 P e v.
Proof.
revert v E1 E2 P.
induction e; intros v' E1 E2 P agree_on_vars.
- split; intros eval_Var.
+ inversion eval_Var; subst.
rewrite agree_on_vars in H0.
apply (Var_load _ _ _ H0 H1 H2 H3).
+ inversion eval_Var; subst.
rewrite <- agree_on_vars in H0.
apply (Var_load _ _ _ H0 H1 H2 H3).
- split; intros eval_Const; inversion eval_Const; subst; econstructor; auto.
- split; intros eval_Unop; inversion eval_Unop; subst; econstructor; try auto.
+ erewrite IHe; eauto.
+ erewrite IHe; eauto.
+ erewrite <- IHe; eauto.
+ erewrite <- IHe; eauto.
- split; intros eval_Binop; inversion eval_Binop; subst; econstructor; try auto;
try (erewrite IHe1; eauto);
try (erewrite IHe2; eauto).
Qed.
Lemma shadowing_free_rewriting_cmd f E1 E2 P vR:
(forall n, E1 n = E2 n) ->
bstep f E1 P 0 vR <->
bstep f E2 P 0 vR.
Proof.
revert E1 E2 P vR.
induction f; intros E1 E2 P vR agree_on_vars.
- split; intros bstep_Let; inversion bstep_Let; subst.
+ erewrite shadowing_free_rewriting_exp in H6; auto.
econstructor; eauto.
rewrite <- IHf.
apply H7.
intros n'; unfold updEnv.
case_eq (n' =? n); auto.
+ erewrite <- shadowing_free_rewriting_exp in H6; auto.
econstructor; eauto.
rewrite IHf.
apply H7.
intros n'; unfold updEnv.
case_eq (n' =? n); auto.
- split; intros bstep_Ret; inversion bstep_Ret; subst.
+ erewrite shadowing_free_rewriting_exp in H0; auto.
constructor; auto.
+ erewrite <- shadowing_free_rewriting_exp in H0; auto.
constructor; auto.
Qed.
Lemma dummy_bind_ok e v x v' inVars E P:
validVars e inVars = true ->
NatSet.mem x inVars = false ->
eval_exp 0 E P (toRExp e) v ->
eval_exp 0 (updEnv x v' E) P (toRExp e) v.
Proof.
revert v x v' inVars E P.
induction e; intros v1 x v2 inVars E P valid_vars x_not_free eval_e.
- inversion eval_e; subst.
assert ((updEnv x v2 E) n = E n).
+ unfold updEnv.
case_eq (n =? x); try auto.
intros n_eq_x.
rewrite Nat.eqb_eq in n_eq_x.
subst; simpl in *.
rewrite x_not_free in valid_vars; inversion valid_vars.
+ econstructor.
rewrite H; auto.
apply H1.
apply H2.
auto.
- inversion eval_e; subst; constructor; auto.
- inversion eval_e; subst; constructor; auto.
+ eapply IHe; eauto.
+ eapply IHe; eauto.
- simpl in valid_vars.
apply Is_true_eq_left in valid_vars.
apply andb_prop_elim in valid_vars.
destruct valid_vars.
inversion eval_e; subst; constructor; auto.
+ eapply IHe1; eauto.
apply Is_true_eq_true; auto.
+ eapply IHe2; eauto.
apply Is_true_eq_true; auto.
Qed.
Fixpoint exp_subst (e:exp Q) x e_new :=
match e with
|Var _ v => if v =? x then e_new else Var Q v
|Unop op e1 => Unop op (exp_subst e1 x e_new)
|Binop op e1 e2 => Binop op (exp_subst e1 x e_new) (exp_subst e2 x e_new)
| e => e
end.
Lemma exp_subst_correct e e_sub E P x v v_res:
eval_exp (0%R) E P (toRExp e_sub) v ->
(Q2R (ivlo (P x)) <= v <= (Q2R (ivhi (P x))))%R ->
eval_exp (0%R) (updEnv x v E) P (toRExp e) v_res <->
eval_exp (0%R) E P (toRExp (exp_subst e x e_sub)) v_res.
Proof.
intros eval_e.
revert v_res.
induction e.
- intros v_res P_valid; split; [intros eval_upd | intros eval_subst].
+ unfold updEnv in eval_upd. simpl in *.
inversion eval_upd; subst.
case_eq (n =? x); intros; try auto.
* rewrite H in H0.
inversion H0; subst; auto.
* rewrite H in H0.
apply (Var_load _ _ _ H0 H1 H2 H3).
+ simpl in eval_subst.
case_eq (n =? x); intros n_eq_case;
rewrite n_eq_case in eval_subst.
* simpl.
assert (updEnv x v E n = Some v_res).
{ unfold updEnv; rewrite n_eq_case.
f_equal. eapply meps_0_deterministic; eauto. }
{ econstructor; eauto.
instantiate (1 := 0%R).
rewrite Rabs_R0; lra.
instantiate (1 := 0%R).
rewrite Rabs_R0; lra.
repeat (rewrite delta_0_deterministic); try auto.
rewrite Nat.eqb_eq in n_eq_case; subst; auto.
assert (v_res = v) by (eapply meps_0_deterministic; eauto).
subst; auto.
rewrite Rabs_R0; lra.
rewrite Rabs_R0; lra. }
* simpl. inversion eval_subst; subst.
assert (E n = updEnv x v E n).
{ unfold updEnv; rewrite n_eq_case; reflexivity. }
{ rewrite H in H0. apply (Var_load _ _ _ H0 H1 H2 H3). }
- intros v_res; split; [intros eval_upd | intros eval_subst].
+ inversion eval_upd; constructor; auto.
+ inversion eval_subst; constructor; auto.
- split; [intros eval_upd | intros eval_subst].
+ inversion eval_upd; constructor; try auto.
* rewrite <- IHe; auto.
* rewrite <- IHe; auto.
+ inversion eval_subst; constructor; try auto.
* rewrite IHe; auto.
* rewrite IHe; auto.
- intros v_res; split; [intros eval_upd | intros eval_subst].
+ inversion eval_upd; constructor; try auto.
* rewrite <- IHe1; auto.
* rewrite <- IHe2; auto.
+ inversion eval_subst; constructor; try auto.
* rewrite IHe1; auto.
* rewrite IHe2; auto.
Qed.
Fixpoint map_subst (f:cmd Q) x e :=
match f with
|Let y e_y g => Let y (exp_subst e_y x e) (map_subst g x e)
|Ret e_r => Ret (exp_subst e_r x e)
end.
Lemma stepwise_substitution x e v f E P vR inVars outVars:
ssaPrg f inVars outVars ->
NatSet.In x inVars ->
validVars e inVars = true ->
eval_exp 0%R E P (toRExp e) v ->
(Q2R (ivlo (P x)) <= v <= Q2R (ivhi (P x)))%R ->
bstep (toRCmd f) (updEnv x v E) P 0%R vR <->
bstep (toRCmd (map_subst f x e)) E P 0%R vR.
Proof.
revert E e x P vR inVars outVars.
induction f; intros E e0 x P vR inVars outVars ssa_f x_free valid_vars_e eval_e P_valid.
- split; [ intros bstep_let | intros bstep_subst].
+ inversion bstep_let; subst.
simpl in *.
inversion ssa_f; subst.
assert (forall E var, updEnv n v0 (updEnv x v E) var = updEnv x v (updEnv n v0 E) var).
* eapply ssa_shadowing_free.
apply ssa_f.
apply x_free.
apply H6.
* rewrite (shadowing_free_rewriting_cmd _ _ _ _ _ (H E)) in H7.
econstructor; auto.
rewrite <- exp_subst_correct; eauto.
rewrite <- IHf; eauto.
rewrite NatSet.add_spec.
right; auto.
apply validVars_add; auto.
eapply dummy_bind_ok; eauto.
+ inversion bstep_subst; subst.
simpl in *.
inversion ssa_f; subst.
econstructor.
rewrite exp_subst_correct; eauto.
rewrite <- IHf in H7; eauto.
rewrite <- shadowing_free_rewriting_cmd in H7; eauto.
eapply ssa_shadowing_free; eauto.
rewrite <- exp_subst_correct in H6; eauto.
rewrite NatSet.add_spec.
right; auto.
apply validVars_add; auto.
eapply dummy_bind_ok; eauto.
- split; [intros bstep_let | intros bstep_subst].
+ inversion bstep_let; subst.
simpl in *.
rewrite exp_subst_correct in H0; eauto.
constructor. assumption.
+ inversion bstep_subst; subst.
simpl in *.
rewrite <- exp_subst_correct in H0; eauto.
constructor; assumption.
Qed.
Fixpoint let_subst (f:cmd Q) :=
match f with
| Let x e1 g =>
match (let_subst g) with
|Some e' => Some (exp_subst e' x e1)
|None => None
end
| Ret e1 => Some e1
end.
Theorem let_free_form f E P vR inVars outVars e:
ssaPrg f inVars outVars ->
bstep (toRCmd f) E P 0 vR ->
let_subst f = Some e ->
bstep (toRCmd (Ret e)) E P 0 vR.
Proof.
revert E P vR inVars outVars e;
induction f;
intros E P vR inVars outVars e_subst ssa_f bstep_f subst_step.
- simpl.
inversion bstep_f; subst.
inversion ssa_f; subst.
simpl in subst_step.
case_eq (let_subst f).
+ intros f_subst subst_f_eq.
specialize (IHf (updEnv n v E) P vR (NatSet.add n inVars) outVars f_subst H8 H7 subst_f_eq).
rewrite subst_f_eq in subst_step.
inversion IHf; subst.
constructor.
inversion subst_step.
subst.
rewrite <- exp_subst_correct; eauto.
admit.
+ intros subst_eq; rewrite subst_eq in subst_step; inversion subst_step.
- inversion bstep_f; subst.
constructor.
simpl in *.
inversion subst_step; subst.
assumption.
Admitted.
(*
Lemma ssa_non_stuck (f:cmd Q) (inVars outVars:NatSet.t) (VarEnv:var_env)
(ParamEnv:param_env) (P:precond) (eps:R):
......
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