Library ruleLib

Require Import include.
Require Import memory.
Require Import memdata.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import simulation.
Require Import lemmasforseplog.
Require Import inferules.
Require Import tacticsforseplog.
Require Import lmachLib.
Require Import contLib.
Require Import loststepLib.
Require Import baseTac.
Require Import joinmemLib.
Require Import asrtLib.
Require Import auxdef.
Require Import tst_prop.

Definition isfree (C:code) := exists ls v ks, C = (curs (sfree ls v), (kenil,ks)).

Definition isalloc (C:code) :=exists vl dl ks,
C = (curs (salloc vl dl), (kenil, ks)) .

Definition nci (C:code) := exists s ke ks, C = (s, (ke,ks))/\callcont ks = None /\ intcont ks = None.

Lemma adisj_astar_elim_l : forall s P Q R, s |= (P \\// Q) ** R -> s |= P ** R \/ s |= Q ** R.

Lemma adisj_astar_elim_r : forall s P Q R, s |= P ** (Q \\// R) -> s |= P ** Q \/ s |= P ** R.

Lemma goodfrm_prop : forall p m isr aux O aop ,
 GoodFrm p ->
 sat ((m,isr,aux),O,aop) p ->
 forall isr´ aux´ aop´, sat ((m,isr´,aux´),O,aop´) p.

Lemma OSAbst_join_disj :
  forall O Of O´ Os, OSAbstMod.join O Of O´ ->
                     OSAbstMod.disj O´ Os ->
                     OSAbstMod.disj O Os /\
                     OSAbstMod.disj Of Os.

Lemma hmstep_eqdomO :
  forall r r´ O O´ ,
    hmstep r O r´ O´ -> eqdomO O O´.

Lemma eqdomO_trans:
  forall O O´ O´´,
    eqdomO O O´ ->
    eqdomO O´ O´´ ->
    eqdomO O O´´.

Lemma hmstepstar_eqdomO :
  forall r r´ O O´ ,
    hmstepstar r O r´ O´ -> eqdomO O O´.

Lemma eqdomO_disj_disj :
  forall O O1 O1´,
    eqdomO O1 O1´ -> OSAbstMod.disj O O1 -> OSAbstMod.disj O O1´.

Lemma eqdomO_merge :
  forall O O1 O2,
    eqdomO O1 O2 -> eqdomO (OSAbstMod.merge O O1) (OSAbstMod.merge O O2).

Lemma osabst_disj_merge_get_r :
  forall O1 O2 a x,
    OSAbstMod.disj O1 O2 ->
    OSAbstMod.get O2 a = Some x -> OSAbstMod.get (OSAbstMod.merge O1 O2) a = Some x.

Lemma specstep_locality :
  forall r O r´ O´ O´´,
    spec_step r O r´ O´ ->
    OSAbstMod.disj O´´ O ->
    spec_step r (OSAbstMod.merge O´´ O) r´ (OSAbstMod.merge O´´ O´) /\
    OSAbstMod.disj O´´ O´.

Lemma hmstep_locality :
  forall r O r´ O´ O´´,
    hmstep r O r´ O´ ->
    OSAbstMod.disj O´´ O ->
    hmstep r (OSAbstMod.merge O´´ O) r´ (OSAbstMod.merge O´´ O´) /\ OSAbstMod.disj O´´ O´.


Lemma Goodg_hmstepstar :
  forall gamma O´´ O gamma´ O´,
    hmstepstar gamma O gamma´ O´ ->
    OSAbstMod.disj O´´ O ->
    hmstepstar gamma (OSAbstMod.merge O´´ O) gamma´
                (OSAbstMod.merge O´´ O´) /\ OSAbstMod.disj O´´ O´.

Lemma OSAbstMod_join_disj :
  forall O1 O2 O3, OSAbstMod.join O1 O2 O3 -> OSAbstMod.disj O1 O2.

Lemma OSAbst_join_merge :
  forall O Of O´ Os , OSAbstMod.join O Of O´ ->
                      OSAbstMod.disj Of Os ->
                      OSAbstMod.disj O Os ->
                      OSAbstMod.disj Of (OSAbstMod.merge O Os) /\
                      OSAbstMod.disj Of O .

Lemma OSAbst_disj_merge :
  forall O´´ Os´ Of ,
    OSAbstMod.disj O´´ Os´ ->
    OSAbstMod.disj Of (OSAbstMod.merge O´´ Os´) ->
    OSAbstMod.disj (OSAbstMod.merge Of O´´) Os´.

Lemma OSAbst_merge_eq :
  forall O´´ Os´ Of, OSAbstMod.disj O´´ Os´ ->
                     OSAbstMod.disj Of (OSAbstMod.merge O´´ Os´) ->
                     OSAbstMod.merge Of (OSAbstMod.merge O´´ Os´) =
                     OSAbstMod.merge (OSAbstMod.merge Of O´´) Os´.

Lemma OSAbst_merge_eq´ :
  forall O Of O´ Os,
    OSAbstMod.join O Of O´ ->
    OSAbstMod.disj O Os ->
    OSAbstMod.disj Of (OSAbstMod.merge O Os) ->
    OSAbstMod.merge O´ Os = OSAbstMod.merge Of (OSAbstMod.merge O Os).

Lemma OSAbst_disj_join :
  forall O´´ Os´ Of,
    OSAbstMod.disj O´´ Os´ -> OSAbstMod.disj Of (OSAbstMod.merge O´´ Os´) ->
    OSAbstMod.join O´´ Of (OSAbstMod.merge Of O´´).

Lemma n_dym_com_int_scont_callcont :
  forall ks ks´ f s le´,
    callcont ks = Some (kcall f s le´ ks´) -> n_dym_com_int_scont ks ->
    n_dym_com_int_scont ks´.

Lemma n_dym_com_int_scont_intcont_n_dym_com_int_cd :
  forall ks (ks´:stmtcont) ke ks´ le´ c,
    n_dym_com_int_scont ks -> intcont ks = Some (kint c ke le´ ks´) -> n_dym_com_int_cd (c, (ke, ks´)).

Lemma loststep_good_code_prop :
  forall p C o C´ o´, loststep p C o C´ o´ ->
                      ~ IsFcall C -> n_dym_com_int_cd C -> n_dym_com_int_cd C´.

Lemma loststep_code_prop: forall p C o C´ o´ ,
 loststep p C o C´ o´ -> ~ IsFcall C /\
      ~ isalloc C /\ ~ isfree C /\ nci C /\ n_dym_com_int_cd C ->
          ~ isalloc C´ /\ ~ isfree C´ /\ nci C´ /\ n_dym_com_int_cd C´.

Lemma loststep_eqenv :
forall p C o C´ o´ ,
 loststep p C o C´ o´ -> ~ IsFcall C ->
      ~ isalloc C /\ ~ isfree C /\ nci C /\ n_dym_com_int_cd C -> eqenv o o´.

Lemma join3mem_eqenv : forall oo M of1 Mss of Mf o2´,
  joinmem oo M of1 -> joinmem of1 Mss of -> joinmem of Mf o2´ -> eqenv oo o2´.

 Lemma eqenv_goodg_sat :
   forall o O gamma M Of frm oo O´´ gam ,
     eqenv oo o ->
     GoodFrm frm ->
     substmo (o, O, gamma) M Of |= frm -> substmo (oo, O´´, gam) M Of |= frm.

 Lemma OSAbstMod_disj_join_disj3 :
   forall Of Os´ Ot Off OO´,
     OSAbstMod.disj Of (OSAbstMod.merge OO´ Os´) -> OSAbstMod.join Ot Off OO´
     -> OSAbstMod.disj Of Off/\ OSAbstMod.disj Of Ot /\ OSAbstMod.disj Of Os´.

 Lemma OSAbst_disj_merge_disj:
   forall OO´ Os´ Of, OSAbstMod.disj OO´ Os´ ->
                       OSAbstMod.disj Of (OSAbstMod.merge OO´ Os´) ->
                       OSAbstMod.disj (OSAbstMod.merge Of OO´) Os´.

 Lemma OSAbst_join_of :
   forall Of OO´ Os´ Ot Off,
     OSAbstMod.disj Of (OSAbstMod.merge OO´ Os´) ->
     OSAbstMod.join Ot Off OO´ ->
     OSAbstMod.join Ot (OSAbstMod.merge Of Off)
                    (OSAbstMod.merge Of OO´).

 Lemma OSAbstMod_disj_join2 :
   forall Of Off O1 O´´,
     OSAbstMod.disj Of Off -> OSAbstMod.join O1 (OSAbstMod.merge Of Off) O´´ ->
     OSAbstMod.join (OSAbstMod.merge O1 Off) Of O´´.

 Lemma eqenv_join2_eqenv :
   forall o´ o´0 M o o2, eqenv o´ o´0 -> joinmem o M o´ -> joinmem o2 M o´0 -> eqenv o2 o.

 Lemma OSAbstMod_join_disj2´ :
   forall O1 Of Off O´´,
     OSAbstMod.join O1 (OSAbstMod.merge Of Off) O´´ -> OSAbstMod.disj O1 Off/\OSAbstMod.disj O1 Of.

 Lemma OSAbst_join_get2:
   forall O Of O´ a,
     OSAbstMod.join O Of O´ ->
     ( exists tls,
         OSAbstMod.get O abstcblsid = Some (abstcblist tls) /\
         TcbMod.get tls a = None) ->
     exists tls,
       OSAbstMod.get O´ abstcblsid = Some (abstcblist tls) /\
       TcbMod.get tls a = None.


Lemma OSAbstMod_disj_disj:
  forall OO´ Os´ Of , OSAbstMod.disj OO´ Os´ ->
                       OSAbstMod.disj Of (OSAbstMod.merge OO´ Os´) ->
                       OSAbstMod.disj (OSAbstMod.merge Of OO´) Os´/\ (OSAbstMod.merge Of (OSAbstMod.merge OO´ Os´)) =(OSAbstMod.merge (OSAbstMod.merge Of OO´) Os´) .

Lemma OSAbstMod_disj_join_meg:
  forall Of OO´ Os´,
    OSAbstMod.disj Of (OSAbstMod.merge OO´ Os´) ->
    OSAbstMod.join OO´ Of (OSAbstMod.merge Of OO´).

Lemma OSAbstMod_join_disj_eq :
  forall O Of O´ Os ,
    OSAbstMod.join O Of O´ -> OSAbstMod.disj O Os ->
    (OSAbstMod.merge Of (OSAbstMod.merge O Os)) =
    (OSAbstMod.merge O´ Os).

Lemma OSAbstMod_join_disj3:
  forall O Of O´ Os,
    OSAbstMod.join O Of O´ -> OSAbstMod.disj O Os -> OSAbstMod.disj Of Os ->
    OSAbstMod.disj (OSAbstMod.merge O Os) Of.

Lemma astar_l_aconj_elim_zh :
  forall P P´ Q,
    (P //\\ P´) ** Q ==> P ** Q //\\ P´ ** Q.

Lemma swinv_inv_O´´´: forall ge le M M´ O O´ Os´ ir ie is cs xxx I sd,
                        GoodI I sd ->
                        MemMod.disj M´ M ->
                        OSAbstMod.disj O´ Os´ ->
                        OSAbstMod.disj O (OSAbstMod.merge O´ Os´) ->
                        ( (ge, le, M, ir, (ie, is, cs)), Os´, xxx)
                          |= INV I ->
                        (ge, le, M´, ir, (ie, is, cs), O´, xxx) |= SWINV I ->
                        O = empabst.

Lemma goodI_sw_empO: forall I sd oo Mc Ms o1 O´ Os´ Of ab0,
                        GoodI I sd ->
                        joinmem oo Mc o1 -> MemMod.disj Mc Ms ->OSAbstMod.disj O´ Os´ ->
                        OSAbstMod.disj Of (OSAbstMod.merge O´ Os´) ->
                        (substaskst o1 Ms, Os´, ab0) |= INV I ->
                        (substaskst oo Mc, O´, ab0) |= SWINV I ->
                        Of = empabst.

Lemma OSAbstMod_join_emp_eq : forall O Of O´, OSAbstMod.join O Of O´ -> Of = empabst -> O = O´.

Lemma OSAbstMod_join_emp : forall O Of, Of = empabst -> OSAbstMod.join O Of O.

Lemma GoodFrm_sat_absop : forall frm gam gam´ X,
                            GoodFrm frm -> (X, gam) |= frm -> (X, gam´) |= frm.

Lemma frm_asrt_prop:
  forall frm o M o´ Of O O´´ q gam gam´,
    GoodFrm frm ->
    OSAbstMod.disj Of O´´ -> joinmem o M o´ ->
    (o, O´´, gam) |= q -> substmo (o, O, gam´) M Of |= frm->
    (o´, OSAbstMod.merge Of O´´, gam) |= q ** frm .

Lemma OSabstMod_disj_merger_disj2:
  forall Of O Os, OSAbstMod.disj Of (OSAbstMod.merge O Os) ->
                   OSAbstMod.disj Of O/\ OSAbstMod.disj Of Os.

Lemma GoodStmt_ndym: forall s , GoodStmt´ s -> n_dym_com_s s.


Lemma OSAbstMod_join_disj2_merge :
  forall O1 Of O1´ O´´ Os´ Os,
    OSAbstMod.join O1 Of O1´ ->
    OSAbstMod.disj O´´ Os´ ->
    OSAbstMod.disj O1 Os ->
    OSAbstMod.disj Of Os ->
    OSAbstMod.merge O1 Os = OSAbstMod.merge O´´ Os´ ->
    OSAbstMod.disj (OSAbstMod.merge Of O´´) Os´ /\ OSAbstMod.merge O1´ Os = OSAbstMod.merge (OSAbstMod.merge Of O´´) Os´/\ OSAbstMod.disj Of O´´ .

Lemma OSAbstMod_disj_merge :
  forall Of O´´, OSAbstMod.disj Of O´´ -> OSAbstMod.join O´´ Of (OSAbstMod.merge Of O´´).

Lemma OSAbstMod_join_disj2:
  forall Ot Of Off O´,
    OSAbstMod.disj Of O´ ->
    OSAbstMod.join Ot Off O´->
    OSAbstMod.join Ot (OSAbstMod.merge Of Off) (OSAbstMod.merge Of O´).

Lemma OSAbstMod_joinmerge_join:
  forall O0 Of Off O´´, OSAbstMod.join O0 (OSAbstMod.merge Of Off) O´´ ->
                        OSAbstMod.join O0 Off (OSAbstMod.merge O0 Off).

Lemma OSAbstMod_join_gettls :
  forall O1 Of O1´ v3, OSAbstMod.join O1 Of O1´ ->
                        ( exists tls,
                            OSAbstMod.get O1 abstcblsid = Some (abstcblist tls) /\
                            TcbMod.get tls v3 = None) -> exists tls,
                                                             OSAbstMod.get O1´ abstcblsid = Some (abstcblist tls) /\
                                                             TcbMod.get tls v3 = None.

Lemma OSAbstMod_disj_join3: forall Of O´ Ot Off O0 O´´,
 OSAbstMod.disj Of O´ ->
    OSAbstMod.join Ot Off O´->
         OSAbstMod.join O0 (OSAbstMod.merge Of Off) O´´ ->
              OSAbstMod.join (OSAbstMod.merge O0 Off) Of O´´.

Lemma OSAbstMod_join_disj3´ : forall O1 Of O1´ Os ,
                                OSAbstMod.join O1 Of O1´ -> OSAbstMod.disj O1 Os -> OSAbstMod.disj Of Os ->
                                OSAbstMod.disj Of (OSAbstMod.merge O1 Os).

Lemma notvundef_true_false: forall v, v <> Vundef -> istrue v = Some true \/ istrue v = Some false.


Lemma alloc_step_msim_hold : forall p FSpec sd C o gamma O I r ri q,
                 isallocate C -> ~ loststepabt p C o ->
                 (forall p o´ C´, losallocstep p C o C´ o´ ->
                       MethSimMod FSpec sd C´ o´ gamma O I r ri q) ->
           MethSimMod FSpec sd C o gamma O I r ri q .

Lemma alloc_stepn_msim_hold : forall n p FSpec sd C o gamma O I r ri q,
                 (exists C´´ o´´, losallocstepn n p C o C´´ o´´) ->
                                (forall C´ o´, losallocstepn n p C o C´ o´ ->
                       MethSimMod FSpec sd C´ o´ gamma O I r ri q ) ->
           MethSimMod FSpec sd C o gamma O I r ri q .

Lemma swinv_prop1:forall I e e0 m i i0 i1 c O aop is cs,
          (e, e0, m, i, (i0, i1, c), O, aop) |= SWINV
                                             I ** Ais is ** Acs cs ->
          (e, e0, m, i, (i0, i1, c), O, aop) |= SWINV I /\ i1=is /\ c =cs.

Lemma swinv_prop2:forall I e e0 m i i0 O aop is cs,
                (e, e0, m, i, (i0, is, cs), O, aop) |= SWINV I ->
                (e, e0, m, i, (i0, is, cs), O, aop) |= SWINV
                                    I ** Ais is ** Acs cs .

Lemma swpre_join_prop´ : forall oo M oz Mc OO´ ab x sd,
                           joinmem oo M oz -> (substaskst oo Mc, OO´, ab) |= SWPRE sd x -> (substaskst oz Mc, OO´, ab) |= SWPRE sd x.

Ltac fdestruct :=
  repeat progress
         match goal with
           | H : exists _, _ |- _ => destruct H
           | H : _ /\ _ |- _ => destruct H
         end.


Lemma hmstepstart_dom_exprop:
  forall O´´ Os´ O1 O1´ Of Os gamma gam ,
    hmstepstar gamma (OSAbstMod.merge O1 Os) gam
               (OSAbstMod.merge O´´ Os´) ->
    OSAbstMod.disj O1 Os ->
    OSAbstMod.disj Of Os ->
    OSAbstMod.join O1 Of O1´ ->
    OSAbstMod.disj O1´ Os ->
    OSAbstMod.disj O´´ Os´ ->
    OSAbstMod.disj (OSAbstMod.merge Of O´´) Os´ /\
    OSAbstMod.join O´´ Of (OSAbstMod.merge Of O´´)/\
    hmstepstar gamma (OSAbstMod.merge O1´ Os) gam
               (OSAbstMod.merge (OSAbstMod.merge Of O´´) Os´).

Lemma htstepstar_compose_tail:
    forall p c O cst c´ O´ cst´ c´´ cst´´ O´´ t,
      htstepstar p t c cst O c´ cst´ O´ ->
      htstep p t c´ cst´ O´ c´´ cst´´ O´´ ->
      htstepstar p t c cst O c´´ cst´´ O´´.

Lemma abst_get_merge:
  forall O O´ x y ,
    OSAbstMod.get O x = Some y ->
    OSAbstMod.get (OSAbstMod.merge O O´) x = Some y.


Definition empprogunit : progunit := fun _ => None.

Lemma identity_step_msim_hold :
  forall C C´ o,
    notabortm C ->
    (forall p, loststep p C o C´ o) ->
    forall FSpec sd gamma O I r ri q,
      MethSimMod FSpec sd C´ o gamma O I r ri q ->
      MethSimMod FSpec sd C o gamma O I r ri q .

Lemma estep_msim_hold :
  forall c ke m c´ ke´ m´ ,
    estep c ke m c´ ke´ m´ ->
    forall ks Fspec sd gamma O I r ri q isr aux,
      MethSimMod Fspec sd (c´,(ke´,ks)) (m´,isr,aux) gamma O I r ri q ->
      MethSimMod Fspec sd (c,(ke,ks)) (m,isr,aux) gamma O I r ri q .

Lemma estepstar_msim_hold :
  forall c ke m c´ ke´ m´ ,
    estepstar c ke m c´ ke´ m´ ->
    forall ks Fspec sd gamma O I r ri q isr aux,
      MethSimMod Fspec sd (c´,(ke´,ks)) (m´,isr,aux) gamma O I r ri q ->
      MethSimMod Fspec sd (c,(ke,ks)) (m,isr,aux) gamma O I r ri q .

Lemma skip_expr_eval_msim_hold :
  forall (e:expr) (m : smem) v ke,
    evalval e m = Some v ->
    forall ks isr aux C C´ o,
      C = (cure e, (ke,ks)) ->
      C´ = ((curs (sskip (Some v))), (ke, ks)) ->
      o = (m , isr, aux) ->
      forall FSpec sd gamma O I r ri q,
        MethSimMod FSpec sd C´ o gamma O I r ri q ->
        MethSimMod FSpec sd C o gamma O I r ri q.