Program expressions and their semantics


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 : nat)
  | Elet (e1: cexp) (e2: natcexp)
  | 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 nv1 = Some n v2 None
    | Nonev1 = None v2 = None
  end.

Fixpoint exp_sem
  (e: cexp) (res: option nat)
  (acts : list actid)
  (lab : actidact)
  (sb : actidactidProp) (fst : actid) (lst : actid) :=
  match e with
    | Evalue nacts = 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
          acts = fst :: nil lst = fst lab fst = Armw typ1 l v res = Some v
       , acts = fst :: nil lst = fst lab fst = Aload typ2 l
                     res = Some 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 xsnd (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.

3. Every node in acts is sb-reachable from the initial node, fst.

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 HX 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.

4. The final node, lst, is sb-reachable from every node in acts.

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 HX 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 xx ++ (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.

5. Nodes other than fst have no incoming sb-edges.

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