Library funsim

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 includeLib.
Require Import baseTac.
Require Import auxdef.

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 fun_seq_comp:
  forall q ri q´
         FSpec sd f s E G I r M Of ks´,
    GoodI I sd ->
    (forall v, GoodFunAsrt (q v)) ->
    ((forall v o o´ Ok O´ ab,
        G = get_genv (get_smem o´) ->
        E = get_lenv (get_smem o´) ->
        (o, Ok, ab) |= q v->
        joinmem o M o´ ->
        OSAbstMod.join Ok Of O´ ->
        {[FSpec, sd,I, r, ri, q´ ]} ||-
                                 ((curs (sskip v), (kenil, ks´)), o´) <_msim (ab, O´))) ->
    forall c ke ks gamma o1 o1´ O1 O1´,
      G = get_genv (get_smem o1) ->
      joinmem o1 M o1´ ->
      OSAbstMod.join O1 Of O1´ ->
      ({[FSpec,sd, I, arfalse, Afalse, q ]} ||- (
                                           (c,(ke,ks ## kcall f s E kstop)), o1) <_msim (
                                                                                      gamma, O1))->
      ( {[FSpec,sd, I, r, ri, q´ ]} ||-
                                 ((c, (ke, ks ## kcall f s E ks´)), o1´) <_msim (gamma, O1´)).

Lemma free_step_sim_hold :
  forall FSpec sd I ri r post b tp ls ks G E M M´ isr aux O aop v,
    free tp b M = Some M´ ->
    ({[FSpec, sd, I, ri, r, fun v => (post v)]} ||-
                                             ((curs (sfree ls v), (kenil, ks)), (G,E,M´,isr,aux)) <_msim (aop, O ))->
    {[FSpec, sd, I, ri, r, fun v => (post v)]} ||-
                                           ((curs (sfree (cons (b, tp) ls) v), (kenil, ks)), (G,E,M,isr,aux)) <_msim (aop, O ).

Lemma free_stepn_sim_hold :
  forall p sd I ri r post ls ks G E M M´ isr aux O aop v,
    freels ls M M´ ->
    ({[p, sd, I, ri, r, fun v=> (post v)]} ||-
                                        ((curs (sfree nil v), (kenil, ks)), (G,E,M´,isr,aux)) <_msim (aop, O ))->
    {[p, sd, I, ri, r, fun v => (post v)]} ||-
                                        ((curs (sfree ls v), (kenil, ks)), (G,E,M,isr,aux)) <_msim (aop, O ).

Lemma fun_free_ignore : forall P f FSpec sd I pr post vl s E´ ks logicl,
           Some pr = BuildRetI P f vl logicl post ->
           callcont ks = None ->
           intcont ks = None ->
          (forall (o : taskst) (O : osabst) (aop : absop) (v:option val) al,
            (o, O, aop) |= (pr v) ->
            getaddr (get_lenv (get_smem o)) = al ->
           {[FSpec, sd, I, arfalse, Afalse, fun v => getasrt (post (rev vl) v logicl) ]} ||- (
          (curs (sfree al v), (kenil, ks ## kcall f s E´ kstop)), o) <_msim (aop, O )).

Lemma fun_free_comp : forall P f FSpec sd I pr post vl s E´ logicl,
           Some pr = BuildRetI P f vl logicl post ->
          (forall (o : taskst) (O : osabst) (aop : absop) (v:option val) al ks1,
            callcont ks1 = None ->
            intcont ks1 = None ->
            (o, O, aop) |= (pr v) ->
            getaddr (get_lenv (get_smem o)) = al ->
           {[FSpec, sd, I, arfalse, Afalse,fun v => getasrt (post (rev vl) v logicl) ]} ||- (
          (curs (sfree al v), (kenil, ks1 ## kcall f s E´ kstop)), o) <_msim (aop, O ))->
        forall c ke ks G E M isr aux O gamma,
        {[FSpec, sd, I, pr, Afalse, lift Afalse]} ||- (
        (c,(ke,ks)), (G, E, M, isr, aux)) <_msim (
        gamma, O ) ->
                 {[FSpec, sd, I, arfalse, Afalse,
   fun v : option val => POST [post, (rev vl), v, logicl] ]} ||-
   ((c, (ke, ks ## kcall f s E´ kstop)),
   (G, E, M, isr, aux)) <_msim (gamma, O ).