Require Import List Vbase Vlistbase Vlist extralib.
Require Import Classical ClassicalDescription Relations.
Require Import c11.
Set Implicit Arguments.
Program expressions are defined inductively as follows:
Inductive cexp :=
| Evalue (n: nat)
| Ealloc
| Eload (typ: access_type) (l : nat)
| Estore (typ: access_type) (l v : nat)
| Ecas (typ_succ typ_fail: access_type) (l v v´ : nat)
| Elet (e1: cexp) (e2: nat → cexp)
| Epar (e1: cexp) (e2: cexp)
| Erepeat (e : cexp)
| Efence (typ: access_type).
The semantics of expressions is given as a set of tuples containing
the return value and a partial execution (the events performed by the
expression together with the hb-order among them) with distinguished
initial and final nodes.
Definition combine_val (v1 v2 v : option nat) :=
match v with
| Some n ⇒ v1 = Some n ∧ v2 ≠ None
| None ⇒ v1 = None ∨ v2 = None
end.
Fixpoint exp_sem
(e: cexp) (res: option nat)
(acts : list actid)
(lab : actid → act)
(sb : actid → actid → Prop) (fst : actid) (lst : actid) :=
match e with
| Evalue n ⇒ acts = fst :: nil ∧ lst = fst ∧ lab fst = Askip ∧ res = Some n
| Ealloc ⇒ ∃ l, acts = fst :: nil ∧ lst = fst
∧ lab fst = Aalloc l ∧ res = Some l
| Eload typ l ⇒ ∃ v,
acts = fst :: nil ∧ lst = fst ∧ lab fst = Aload typ l v ∧
res = Some v
| Estore typ l v ⇒
acts = fst :: nil ∧ lst = fst ∧ lab fst = Astore typ l v ∧ res = Some v
| Ecas typ1 typ2 l v v´ ⇒
acts = fst :: nil ∧ lst = fst ∧ lab fst = Armw typ1 l v v´ ∧ res = Some v
∨ ∃ v´, acts = fst :: nil ∧ lst = fst ∧ lab fst = Aload typ2 l v´
∧ res = Some v´ ∧ v´ ≠ v
| Elet e1 e2 ⇒
(res = None ∧ exp_sem e1 None acts lab sb fst lst) ∨
(∃ vmid lst1 fst2 acts1 acts2,
acts = acts1 ++ acts2 ∧
disjoint acts1 acts2 ∧
sb lst1 fst2 ∧
<< U1 : (∀ n (SB: sb lst1 n), n = fst2) >> ∧
<< U2 : (∀ n (SB: sb n fst2), n = lst1) >> ∧
<< ESEM1: exp_sem e1 (Some vmid) acts1 lab sb fst lst1 >> ∧
<< ESEM2: exp_sem (e2 vmid) res acts2 lab sb fst2 lst >>)
| Epar e1 e2 ⇒
∃ res1 fst1 lst1 res2 fst2 lst2 acts1 acts2,
acts = fst :: lst :: acts1 ++ acts2 ∧
<< NODUP: NoDup acts >> ∧
<< ESEM1: exp_sem e1 res1 acts1 lab sb fst1 lst1 >> ∧
<< ESEM2: exp_sem e2 res2 acts2 lab sb fst2 lst2 >> ∧
<< LABF : lab fst = Askip >> ∧
<< LABL : lab lst = Askip >> ∧
<< SBF1 : sb fst fst1 >> ∧
<< SBF2 : sb fst fst2 >> ∧
<< SBL1 : sb lst1 lst >> ∧
<< SBL2 : sb lst2 lst >> ∧
<< UL0 : ∀ n (SB: sb n lst), lst1 = n ∨ lst2 = n >> ∧
<< UL1 : ∀ n (SB: sb lst1 n), n = lst >> ∧
<< UL2 : ∀ n (SB: sb lst2 n), n = lst >> ∧
<< UF0 : (∀ n (SB: sb fst n), n = fst1 ∨ n = fst2) >> ∧
<< UF1 : (∀ n (SB: sb n fst1), n = fst) >> ∧
<< UF2 : (∀ n (SB: sb n fst2), n = fst) >> ∧
<< CVAL: combine_val res1 res2 res >>
| Erepeat e ⇒
∃ sems resI actsI lstI actsF fstF,
acts = flatten (map (fun x ⇒ snd (Datatypes.fst (Datatypes.fst x))) sems) ∧
<< ESEM: ∀ res acts fst lst (IN: In (res, acts, fst, lst) sems),
exp_sem e res acts lab sb fst lst >> ∧
<< REP: ∀ prefix res1 acts1 fst1 lst1 res2 acts2 fst2 lst2 suffix
(EQ: sems = prefix ++ (res1, acts1, fst1, lst1) ::
(res2, acts2, fst2, lst2) :: suffix),
<< RES : res1 = Some 0 >> ∧
<< SB : sb lst1 fst2 >> ∧
<< U1 : (∀ n (SB: sb lst1 n), n = fst2) >> ∧
<< U2 : (∀ n (SB: sb n fst2), n = lst1) >> >> ∧
<< NODUP: NoDup acts >> ∧
<< GET_I: ohead sems = Some (resI,actsI,fst,lstI) >> ∧
<< GET_F: olast sems = Some (res,actsF,fstF,lst) >> ∧
<< CVAL: res ≠ Some 0 >>
| Efence typ ⇒
acts = fst :: nil ∧ fst = lst ∧ lab fst = Afence typ
end.
We prove a number of basic well-formedness properties for the expression
semantics.
1. The fst and lst nodes belong to the set of actions, act.
Lemma exp_sem_fst :
∀ e res acts lab sb fst lst (SEM: exp_sem e res acts lab sb fst lst),
In fst acts.
Proof.
induction e; ins; desf; eauto using In_appI1, In_appI2;
destruct sems; ins; desf; eauto using In_appI1, In_appI2, In_eq.
Qed.
Lemma exp_sem_lst :
∀ e res acts lab sb fst lst (SEM: exp_sem e res acts lab sb fst lst),
In lst acts.
Proof.
induction e; ins; desf; eauto using In_appI1, In_appI2, In_cons, In_eq.
eapply olast_inv in GET_F; desf;
rewrite map_app, map_cons, flatten_app, flatten_cons; ins;
eauto 6 using In_appI1, In_appI2, In_cons, In_eq.
Qed.
2. The list of actions contains no duplicate entries.
Lemma exp_sem_nodup :
∀ e res acts lab sb fst lst (SEM: exp_sem e res acts lab sb fst lst),
NoDup acts.
Proof.
induction e; ins; desf; eauto using In_appI1, In_appI2, In_cons, In_eq, nodup_append.
Qed.
Lemma exp_sem_fst_reach :
∀ e res acts lab sb fst lst (SEM: exp_sem e res acts lab sb fst lst)
x (IN: In x acts), clos_refl_trans _ sb fst x.
Proof.
induction e; ins; desf; ins; try rewrite In_app in *; desf; eauto using rt_refl;
try solve [eapply rt_trans with fst1; eauto using exp_sem_lst, rt_step];
try solve [eapply rt_trans with fst2; eauto using exp_sem_lst, rt_step].
× eapply rt_trans with lst1; eauto using exp_sem_lst.
by eapply rt_trans with fst2; eauto using exp_sem_lst, rt_step.
× eapply rt_trans with fst1; eauto using rt_step.
by eapply rt_trans with lst1; eauto using exp_sem_lst, rt_step.
× rewrite In_flatten in *; desf; rewrite In_map in *; desf.
destruct x0 as [[[res0 acts0] fst0] lst0]; ins.
eapply rt_trans; eauto.
assert (X: ∀ res0 acts0 fst0 lst0
(IN: In (res0, acts0, fst0, lst0) sems),
clos_refl_trans _ sb fst0 lst0).
by clear - ESEM IHe; ins; eauto using exp_sem_lst.
clear -REP X IN1 GET_I; destruct sems; ins; desf; vauto.
generalize (X _ _ _ _ (In_eq _ _)).
specialize (fun r a f l H ⇒ X r a f l (In_cons _ H)).
revert resI actsI fst lstI REP; induction sems as [|[[[??]f1]l1]]; ins; desf.
by edestruct (REP nil); ins; desf; eauto using clos_refl_trans.
eapply rt_trans with f1, IHsems; eauto.
by edestruct (REP nil); ins; desf; eauto 6 using clos_refl_trans.
by ins; eapply (REP (_ :: prefix)); ins; f_equal; apply EQ.
Qed.
Lemma exp_sem_lst_reach :
∀ e res acts lab sb fst lst (SEM: exp_sem e res acts lab sb fst lst)
x (IN: In x acts), clos_refl_trans _ sb x lst.
Proof.
induction e; ins; desf; ins; try rewrite In_app in *; desf; eauto using rt_refl.
× eapply rt_trans with lst1; eauto using exp_sem_lst.
by eapply rt_trans with fst2; eauto using exp_sem_fst, rt_step.
× eapply rt_trans with fst1; eauto using exp_sem_fst, rt_step.
eapply rt_trans with lst1; eauto using exp_sem_fst, rt_step.
× eapply rt_trans with lst1; eauto using exp_sem_fst, rt_step.
× eapply rt_trans with lst2; eauto using exp_sem_fst, rt_step.
× rewrite In_flatten in *; desf; rewrite In_map in *; desf.
destruct x0 as [[[res0 acts0] fst0] lst0]; ins.
eapply rt_trans; eauto.
assert (X: ∀ res0 acts0 fst0 lst0
(IN: In (res0, acts0, fst0, lst0) sems),
clos_refl_trans _ sb fst0 lst0).
by clear - ESEM IHe; ins; eauto using exp_sem_fst.
clear -X REP IN1 GET_F.
apply olast_inv in GET_F; desf.
rewrite In_app in *; ins; desf; vauto.
generalize (X _ _ _ _ (In_appI2 (In_eq _ _) _)).
specialize (fun r a f l H ⇒ X r a f l (In_appI1 H _)).
revert res actsF fstF lst REP.
induction prefix as [|[[[??]f1]l1]] using rev_ind; ins;
rewrite In_app in *; ins; desf.
2: by specialize (X _ _ _ _ (In_appI2 (In_eq _ _) _));
edestruct (REP prefix); [by rewrite appA; ins|]; desf;
eauto using clos_refl_trans.
eapply rt_trans with l1; eauto.
2: by edestruct (REP prefix); [by rewrite appA; ins|]; desf;
eauto using clos_refl_trans.
eapply IHprefix; eauto using In_appI1.
intros; eapply (f_equal (fun x ⇒ x ++ (res, actsF, fstF, lst) :: nil)) in EQ.
rewrite !appA in EQ; ins; eapply REP; rewrite appA; apply EQ.
by eauto using In_appI2, In_eq.
Qed.
Lemma exp_sem_pre_closed :
∀ e res acts lab sb fst lst (SEM: exp_sem e res acts lab sb fst lst)
a b (SB: sb a b) (IN: In b acts), b = fst ∨ In a acts.
Proof.
induction e; ins; desc;
try match goal with H: _ = None ∨ _ |- _ ⇒ clear H end;
desf; ins; try rewrite In_app in *; desf; instantiate; eauto;
try (exploit IHe1; eauto using exp_sem_fst, exp_sem_lst; []; intro; desf);
try (exploit IHe2; eauto using exp_sem_fst, exp_sem_lst; []; intro; desf);
try (exploit IHe; eauto using exp_sem_fst, exp_sem_lst; []; intro; desf);
try (exploit H; eauto using exp_sem_fst, exp_sem_lst; []; intro; desf);
try eapply U2 in SB; try eapply UL0 in SB;
try eapply UF1 in SB; try eapply UF2 in SB; desf;
eauto 6 using exp_sem_fst, exp_sem_lst.
intros; rewrite In_flatten in *; desf; rewrite In_map in *; desf.
destruct x as [[[r acts]f]l]; ins.
apply In_split in IN1; desf.
destruct (lastP l1); ins; desf.
specialize (ESEM _ _ _ _ (In_eq _ _)).
by exploit IHe; eauto; []; intro; desf; eauto.
rewrite snocE, appA in *; ins.
destruct x as [[[r1 a1]f1]l1]; ins.
exploit (IHe _ _ _ _ _ _ (ESEM _ _ _ _ (In_appI2 (In_cons _ (In_eq _ _)) _))); eauto;
[]; intro; desf; eauto.
2: by right; ∃ acts,; try done; eapply In_map; eexists,;
[|apply In_appI2, In_cons, In_eq].
exploit REP; ins; desf.
specialize (ESEM _ _ _ _ (In_appI2 (In_eq _ _) _)).
eapply U2 in SB; desf.
right; ∃ a1,; eauto using exp_sem_lst.
by apply In_map; eexists,; [|apply In_appI2, In_eq].
Qed.
This page has been generated by coqdoc