diff options
Diffstat (limited to 'kvx/abstractbb/SeqSimuTheory.v')
-rw-r--r-- | kvx/abstractbb/SeqSimuTheory.v | 77 |
1 files changed, 39 insertions, 38 deletions
diff --git a/kvx/abstractbb/SeqSimuTheory.v b/kvx/abstractbb/SeqSimuTheory.v index 61f8f2ec..df6b9963 100644 --- a/kvx/abstractbb/SeqSimuTheory.v +++ b/kvx/abstractbb/SeqSimuTheory.v @@ -55,13 +55,14 @@ with list_term_eval ge (l: list_term) (m: mem) {struct l}: option (list value) : end end. -(* the symbolic memory: - - pre: pre-condition expressing that the computation has not yet abort on a None. - - post: the post-condition for each pseudo-register -*) -Record smem:= {pre: genv -> mem -> Prop; post:> R.t -> term}. - -(** initial symbolic memory *) +(** The (abstract) symbolic memory state *) +Record smem := +{ + pre: genv -> mem -> Prop; (**r pre-condition expressing that the computation has not yet abort on a None. *) + post:> R.t -> term (**r the output term computed on each pseudo-register *) +}. + +(** Initial symbolic memory state *) Definition smem_empty := {| pre:=fun _ _ => True; post:=(fun x => Input x) |}. Fixpoint exp_term (e: exp) (d old: smem) : term := @@ -78,11 +79,12 @@ with list_exp_term (le: list_exp) (d old: smem) : list_term := end. -(** assignment of the symbolic memory *) +(** assignment of the symbolic memory state *) Definition smem_set (d:smem) x (t:term) := {| pre:=(fun ge m => (term_eval ge (d x) m) <> None /\ (d.(pre) ge m)); post:=fun y => if R.eq_dec x y then t else d y |}. +(** Simulation theory: the theorem [bblock_smem_simu] ensures that the simulation between two abstract basic blocks is implied by the simulation between their symbolic execution. *) Section SIMU_THEORY. Variable ge: genv. @@ -90,13 +92,13 @@ Variable ge: genv. Lemma set_spec_eq d x t m: term_eval ge (smem_set d x t x) m = term_eval ge t m. Proof. - unfold smem_set; simpl; case (R.eq_dec x x); try congruence. + unfold smem_set; cbn; case (R.eq_dec x x); try congruence. Qed. Lemma set_spec_diff d x y t m: x <> y -> term_eval ge (smem_set d x t y) m = term_eval ge (d y) m. Proof. - unfold smem_set; simpl; case (R.eq_dec x y); try congruence. + unfold smem_set; cbn; case (R.eq_dec x y); try congruence. Qed. Fixpoint inst_smem (i: inst) (d old: smem): smem := @@ -121,15 +123,15 @@ Definition bblock_smem: bblock -> smem Lemma inst_smem_pre_monotonic i old: forall d m, (pre (inst_smem i d old) ge m) -> (pre d ge m). Proof. - induction i as [|[y e] i IHi]; simpl; auto. + induction i as [|[y e] i IHi]; cbn; auto. intros d a H; generalize (IHi _ _ H); clear H IHi. - unfold smem_set; simpl; intuition. + unfold smem_set; cbn; intuition. Qed. Lemma bblock_smem_pre_monotonic p: forall d m, (pre (bblock_smem_rec p d) ge m) -> (pre d ge m). Proof. - induction p as [|i p' IHp']; simpl; eauto. + induction p as [|i p' IHp']; cbn; eauto. intros d a H; eapply inst_smem_pre_monotonic; eauto. Qed. @@ -144,7 +146,7 @@ Proof. intro H. induction e using exp_mut with (P0:=fun l => forall (d:smem) m1, (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> list_term_eval ge (list_exp_term l d od) m0 = list_exp_eval ge l m1 old); - simpl; auto. + cbn; auto. - intros; erewrite IHe; eauto. - intros. erewrite IHe, IHe0; eauto. Qed. @@ -154,12 +156,12 @@ Lemma inst_smem_abort i m0 x old: forall (d:smem), term_eval ge (d x) m0 = None -> term_eval ge (inst_smem i d old x) m0 = None. Proof. - induction i as [|[y e] i IHi]; simpl; auto. + induction i as [|[y e] i IHi]; cbn; auto. intros d VALID H; erewrite IHi; eauto. clear IHi. - unfold smem_set; simpl; destruct (R.eq_dec y x); auto. + unfold smem_set; cbn; destruct (R.eq_dec y x); auto. subst; generalize (inst_smem_pre_monotonic _ _ _ _ VALID); clear VALID. - unfold smem_set; simpl. intuition congruence. + unfold smem_set; cbn. intuition congruence. Qed. Lemma block_smem_rec_abort p m0 x: forall d, @@ -167,7 +169,7 @@ Lemma block_smem_rec_abort p m0 x: forall d, term_eval ge (d x) m0 = None -> term_eval ge (bblock_smem_rec p d x) m0 = None. Proof. - induction p; simpl; auto. + induction p; cbn; auto. intros d VALID H; erewrite IHp; eauto. clear IHp. eapply inst_smem_abort; eauto. Qed. @@ -179,13 +181,13 @@ Lemma inst_smem_Some_correct1 i m0 old (od:smem): (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> forall x, term_eval ge (inst_smem i d od x) m0 = Some (m2 x). Proof. - intro X; induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H. + intro X; induction i as [|[x e] i IHi]; cbn; intros m1 m2 d H. - inversion_clear H; eauto. - intros H0 x0. destruct (exp_eval ge e m1 old) eqn:Heqov; try congruence. refine (IHi _ _ _ _ _ _); eauto. clear x0; intros x0. - unfold assign, smem_set; simpl. destruct (R.eq_dec x x0); auto. + unfold assign, smem_set; cbn. destruct (R.eq_dec x x0); auto. subst; erewrite term_eval_exp; eauto. Qed. @@ -195,7 +197,7 @@ Lemma bblocks_smem_rec_Some_correct1 p m0: forall (m1 m2: mem) (d: smem), forall x, term_eval ge (bblock_smem_rec p d x) m0 = Some (m2 x). Proof. Local Hint Resolve inst_smem_Some_correct1: core. - induction p as [ | i p]; simpl; intros m1 m2 d H. + induction p as [ | i p]; cbn; intros m1 m2 d H. - inversion_clear H; eauto. - intros H0 x0. destruct (inst_run ge i m1 m1) eqn: Heqov. @@ -216,15 +218,15 @@ Lemma inst_smem_None_correct i m0 old (od: smem): (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> inst_run ge i m1 old = None -> exists x, term_eval ge (inst_smem i d od x) m0 = None. Proof. - intro X; induction i as [|[x e] i IHi]; simpl; intros m1 d. + intro X; induction i as [|[x e] i IHi]; cbn; intros m1 d. - discriminate. - intros VALID H0. destruct (exp_eval ge e m1 old) eqn: Heqov. + refine (IHi _ _ _ _); eauto. - intros x0; unfold assign, smem_set; simpl. destruct (R.eq_dec x x0); auto. + intros x0; unfold assign, smem_set; cbn. destruct (R.eq_dec x x0); auto. subst; erewrite term_eval_exp; eauto. + intuition. - constructor 1 with (x:=x); simpl. + constructor 1 with (x:=x); cbn. apply inst_smem_abort; auto. rewrite set_spec_eq. erewrite term_eval_exp; eauto. @@ -239,14 +241,14 @@ Lemma inst_smem_Some_correct2 i m0 old (od: smem): res_eq (Some m2) (inst_run ge i m1 old). Proof. intro X. - induction i as [|[x e] i IHi]; simpl; intros m1 m2 d VALID H0. + induction i as [|[x e] i IHi]; cbn; intros m1 m2 d VALID H0. - intros H; eapply ex_intro; intuition eauto. generalize (H0 x); rewrite H. congruence. - intros H. destruct (exp_eval ge e m1 old) eqn: Heqov. + refine (IHi _ _ _ _ _ _); eauto. - intros x0; unfold assign, smem_set; simpl; destruct (R.eq_dec x x0); auto. + intros x0; unfold assign, smem_set; cbn; destruct (R.eq_dec x x0); auto. subst; erewrite term_eval_exp; eauto. + generalize (H x). rewrite inst_smem_abort; discriminate || auto. @@ -260,7 +262,7 @@ Lemma bblocks_smem_rec_Some_correct2 p m0: forall (m1 m2: mem) d, (forall x, term_eval ge (bblock_smem_rec p d x) m0 = Some (m2 x)) -> res_eq (Some m2) (run ge p m1). Proof. - induction p as [|i p]; simpl; intros m1 m2 d VALID H0. + induction p as [|i p]; cbn; intros m1 m2 d VALID H0. - intros H; eapply ex_intro; intuition eauto. generalize (H0 x); rewrite H. congruence. @@ -291,13 +293,13 @@ Lemma inst_valid i m0 old (od:smem): (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> pre (inst_smem i d od) ge m0. Proof. - induction i as [|[x e] i IHi]; simpl; auto. + induction i as [|[x e] i IHi]; cbn; auto. intros Hold m1 m2 d VALID0 H Hm1. - destruct (exp_eval ge e m1 old) eqn: Heq; simpl; try congruence. + destruct (exp_eval ge e m1 old) eqn: Heq; cbn; try congruence. eapply IHi; eauto. - + unfold smem_set in * |- *; simpl. + + unfold smem_set in * |- *; cbn. rewrite Hm1; intuition congruence. - + intros x0. unfold assign, smem_set; simpl; destruct (R.eq_dec x x0); auto. + + intros x0. unfold assign, smem_set; cbn; destruct (R.eq_dec x x0); auto. subst; erewrite term_eval_exp; eauto. Qed. @@ -309,7 +311,7 @@ Lemma block_smem_rec_valid p m0: forall (m1 m2: mem) (d:smem), pre (bblock_smem_rec p d) ge m0. Proof. Local Hint Resolve inst_valid: core. - induction p as [ | i p]; simpl; intros m1 d H; auto. + induction p as [ | i p]; cbn; intros m1 d H; auto. intros H0 H1. destruct (inst_run ge i m1 m1) eqn: Heqov; eauto. congruence. @@ -320,7 +322,7 @@ Lemma bblock_smem_valid p m0 m1: pre (bblock_smem p) ge m0. Proof. intros; eapply block_smem_rec_valid; eauto. - unfold smem_empty; simpl. auto. + unfold smem_empty; cbn. auto. Qed. Definition smem_valid ge d m := pre d ge m /\ forall x, term_eval ge (d x) m <> None. @@ -337,7 +339,7 @@ Theorem bblock_smem_simu p1 p2: Proof. Local Hint Resolve bblock_smem_valid bblock_smem_Some_correct1: core. intros (INCL & EQUIV) m DONTFAIL; unfold smem_valid in * |-. - destruct (run ge p1 m) as [m1|] eqn: RUN1; simpl; try congruence. + destruct (run ge p1 m) as [m1|] eqn: RUN1; cbn; try congruence. assert (X: forall x, term_eval ge (bblock_smem p1 x) m = Some (m1 x)); eauto. eapply bblock_smem_Some_correct2; eauto. + destruct (INCL m); intuition eauto. @@ -369,21 +371,20 @@ Lemma smem_valid_set_proof d x t m: Proof. unfold smem_valid; intros (PRE & VALID) PREt. split. + split; auto. - + intros x0; unfold smem_set; simpl; case (R.eq_dec x x0); intros; subst; auto. + + intros x0; unfold smem_set; cbn; case (R.eq_dec x x0); intros; subst; auto. Qed. End SIMU_THEORY. -(** REMARKS: more abstract formulation of the proof... - but relying on functional_extensionality. +(** REMARK: this theorem reformulates the lemma above in a more abstract way (but relies on functional_extensionality axiom). *) Definition smem_correct ge (d: smem) (m: mem) (om: option mem): Prop:= forall m', om=Some m' <-> (d.(pre) ge m /\ forall x, term_eval ge (d x) m = Some (m' x)). Lemma bblock_smem_correct ge p m: smem_correct ge (bblock_smem p) m (run ge p m). Proof. - unfold smem_correct; simpl; intros m'; split. + unfold smem_correct; cbn; intros m'; split. + intros; split. * eapply bblock_smem_valid; eauto. * eapply bblock_smem_Some_correct1; eauto. |