Library loststepLib

Require Import Coqlib.
Require Import memory.
Require Import Integers.
Require Import List.
Require Import ZArith.
Require Import language.
Require Import opsem.
Require Import LibTactics.
Require Import simulation.
Require Import assertion.
Require Import baseTac.
Require Export cstepLib.

Tactic Notation "invertstep" tactic (t) :=
  repeat progress
         match goal with
           | H : (_, _) = (_, _) |- _ => inverts H; tryfalse
           | H : estep _ _ _ _ _ _ |- _ => inverts H
           | H : loststep _ _ _ _ _ |- _ => inverts H
           | H : cstep _ _ _ _ _ |- _ => inverts H
           | H : sstep _ _ _ _ _ _ _ |- _ => inverts H
           | _ => t
         end.

Inductive loststepstar: progunit -> code -> taskst -> code -> taskst -> Prop:=
 | loststepstar_0 : forall p C o , loststepstar p C o C o
 | loststepstar_n : forall p C o C´´ o´´ C´ o´, loststep p C o C´´ o´´ ->
                                                 loststepstar p C´´ o´´ C´ o´ ->
                                                 loststepstar p C o C´ o´.

Inductive loststepn : nat -> progunit -> code -> taskst -> code -> taskst -> Prop :=
 | loststepn_0 : forall p C o , loststepn O p C o C o
 | loststepn_n : forall n p C o C´´ o´´ C´ o´, loststep p C o C´´ o´´ ->
                                               loststepn n p C´´ o´´ C´ o´ ->
                                               loststepn (S n) p C o C´ o´.

Inductive lostidstepstar : progunit -> code -> taskst -> code -> taskst -> Prop :=
      | lostidstepstar0 : forall pu C o, lostidstepstar pu C o C o
      | lostidstepstarn : forall pu C o C´ C´´, loststep pu C o C´ o ->
                                        lostidstepstar pu C´ o C´´ o -> lostidstepstar pu C o C´´ o.

Inductive losidstepn : nat -> progunit -> code -> taskst -> code -> taskst -> Prop :=
  | losidstep_0 : forall p C o, losidstepn O p C o C o
  | losidstep_n : forall n p C o C´ C´´, loststep p C o C´´ o ->
                losidstepn n p C´´ o C´ o -> losidstepn (S n) p C o C´ o.

Definition joinenvmem (o: taskst) (E : env) (M : mem) (o´:taskst) : Prop :=
    exists G E0 E1 M0 M1 ir aux, o = ((G, E0, M0), ir, aux) /\ o´ = ((G,E1,M1), ir, aux)
              /\ EnvMod.join E0 E E1 /\ MemMod.join M0 M M1.

Open Local Scope nat_scope.
Definition isallocate (C : code) :=
        exists vl dl ks , C = (curs (salloc vl dl), (kenil, ks)) /\
                dl <> dnil /\ length vl <= length_dl dl.

Definition allocstep (C : code) (o o´ : taskst) :=
   exists vl dl ks x t , C = (curs (salloc vl (dcons x t dl)), (kenil, ks)) /\
                       length vl <= S (length_dl dl) /\
                       (vl = nil -> exists b v M , mapstoval (b,0%Z) t v M
                          /\joinenvmem o (EnvMod.sig x (b,t)) M o´) /\
                       (vl <> nil -> exists b v vl´ M , vl = v :: vl´/\
                            mapstoval (b,0%Z) t v M
                          /\joinenvmem o (EnvMod.sig x (b,t)) M o´).

Definition losallocstep (p:progunit)(C: code) (o: taskst) (C´ : code)(o´:taskst) :=
    loststep p C o C´ o´ /\ allocstep C o o´.


Inductive losallocstepstar : progunit -> code -> taskst -> code -> taskst -> Prop :=
   | losallocstepstar_0 : forall p C o, losallocstepstar p C o C o
   | losallocstepstar_n : forall p C o C´´ o´´ C´ o´, losallocstep p C o C´´ o´´ ->
                                               losallocstepstar p C´´ o´´ C´ o´ ->
                                              losallocstepstar p C o C´ o´.

Inductive losallocstepn : nat -> progunit -> code -> taskst -> code -> taskst -> Prop :=
   | losallocstep_0 : forall p C o, losallocstepn O p C o C o
   | losallocstep_n : forall n p C o C´´ o´´ C´ o´, losallocstep p C o C´´ o´´ ->
                                               losallocstepn n p C´´ o´´ C´ o´ ->
                                              losallocstepn (S n) p C o C´ o´.

Lemma store_mono_join_eq:
  forall M0 v b t M M1 M´,store t M0 (b, 0%Z) v = Some M0 -> MemMod.join M0 M M1 -> store t M1 (b, 0%Z) v = Some M´ -> M1=M´.

Lemma list_is_noteq : forall i (l:is), ~(l = i :: l).

Lemma list_cs_noteq : forall i (l:cs), ~(l = i :: l).

Lemma losstep_idmove_frame : forall p C C´ C´´ o o´ o´´ M,
              loststep p C o C´ o -> joinmem o M o´ ->
              loststep p C o´ C´´ o´´ -> C´ = C´´ /\ o´ = o´´.

Lemma losstep_idmove_determistic : forall p C C´ C´´ o o´,
              loststep p C o C´ o -> loststep p C o C´´ o´
                         -> C´ = C´´ /\ o = o´.

Lemma estep_imply_loststep : forall c c´ ke ke´ m,
           estep c ke m c´ ke´ m -> forall pu ks isr aux C C´ o,
 C = (c, (ke, ks)) -> C´ = (c´, (ke´, ks)) ->
              o = (m, isr, aux) -> loststep pu C o C´ o.

Lemma estepstar_imply_lostidstepstar : forall c c´ ke ke´ m,
           estepstar c ke m c´ ke´ m
           -> forall pu ks isr aux C C´ o,
              C = (c, ( ke, ks)) ->
              C´ =(c´, (ke´,ks)) ->
              o = (m, isr, aux) -> lostidstepstar pu C o C´ o.

Lemma evalval_imply_lostidstepstar : forall (e:expr) (m : smem) v ke,
               evalval e m = Some v -> forall pu ks isr aux C C´ o,
              C = (cure e, (ke, ks)) ->
              C´ = (curs (sskip (Some v)) , (ke, ks)) ->
              o = (m, isr, aux) -> lostidstepstar pu C o C´ o.

Lemma os_skip_not_step : forall p o v, ~ exists o´ c,
                                loststep p (nilcont (sskip v)) o c o´.

Lemma os_ret_not_step : forall p o , ~ exists o´ c,
   loststep p (nilcont sret) o c o´.

Lemma notabt_frame : forall p C o M o1, joinmem o M o1-> ~ loststepabt p C o -> ~ loststepabt p C o1.

Lemma loststep_join_notabt´: forall p C o o1 M, joinmem o M o1 ->
  (exists o´ C´, loststep p C o C´ o´) -> ~ loststepabt p C o1.

Lemma loststep_join_notabt: forall p C o o1 o2 M1 M2, joinmem o M1 o1 -> joinmem o1 M2 o2 ->
  (exists o´ C´, loststep p C o C´ o´) -> ~ loststepabt p C o2.

Lemma ostidstep_imply_idstepn : forall p C o C´,
              lostidstepstar p C o C´ o -> exists n, losidstepn n p C o C´ o.

Lemma alloc_code_eq : forall p p´ C o C´ o´ C´´ o´´,
               losallocstep p C o C´ o´ -> losallocstep p´ C o C´´ o´´ -> C´ = C´´.

Lemma alloc_code_eq´ : forall p C o1 C´ o1´ o2 C´´ o2´,
               losallocstep p C o1 C´ o1´ -> losallocstep p C o2 C´´ o2´ -> C´ = C´´.

Lemma alloc_stepn_code_eq : forall n p C o C´ o´,
        losallocstepn n p C o C´ o´ ->
            forall C´´ o o´´, losallocstepn n p C o C´´ o´´ -> C´ = C´´.

Fixpoint good_env_decllist le dl :=
  match dl with
  | dnil => True
  | dcons x _ dl´ => (~EnvMod.indom le x) /\ (good_env_decllist le dl´)
  end.

Lemma set_env_good_env_decllist:
  forall le dl i b t,
    good_env_decllist le dl ->
      ~ EnvMod.indom le i ->
        good_decllist dl = true ->
    in_decllist i dl = false ->
      good_env_decllist (EnvMod.set le i (b, t)) dl.

Lemma alloc_star_exist´ : forall p vl dl ks ge le M ir aux,
   length vl <= length_dl dl ->
     good_decllist dl = true ->
       good_env_decllist le dl ->
   exists le´ M´,
     losallocstepstar p (curs (salloc vl dl), (kenil, ks))
       (ge, le , M, ir, aux) (curs (salloc nil dnil), (kenil, ks))
         (ge, le´, M´, ir, aux).

Lemma alloc_star_exist : forall p vl dl ks ge M ir aux,
   length vl <= length_dl dl -> good_decllist dl = true ->
   exists le´ M´,
   losallocstepstar p (curs (salloc vl dl), (kenil, ks))
     (ge, empenv , M, ir, aux) (curs (salloc nil dnil), (kenil, ks))
     (ge, le´, M´, ir, aux).

Definition env_domain_eq x y := forall a, EnvMod.indom x a <-> EnvMod.indom y a.

Lemma env_domain_set_eq :
  forall le le´ x v v´ ,
    env_domain_eq le le´ ->
      env_domain_eq (EnvMod.set le x v) (EnvMod.set le´ x v´).

Lemma env_domain_eq_imply_alloc_exist :
  forall le le1 le´ x t M M´ M1,
    env_domain_eq le le1 ->
      alloc x t le M le´ M´ ->
        exists le1´ M1´, alloc x t le1 M1 le1´ M1´.

Lemma allocstep_exist : forall p C C´ o o´ o1 ,
  losallocstep p C o C´ o´->
    env_domain_eq (get_lenv (fst (fst o))) (get_lenv (fst (fst o1))) ->
     exists o1´, losallocstep p C o1 C´ o1´.

Lemma allocstepn_exist : forall n p C C´ o o´ o1 ,
  losallocstepn n p C o C´ o´->
    env_domain_eq (get_lenv (fst (fst o))) (get_lenv (fst (fst o1))) ->
     exists o1´, losallocstepn n p C o1 C´ o1´.

Lemma alloc_exist : forall n p C C´ C´´ o o´ o´´ ,
                  losallocstepn (S (S n)) p C o C´´ o´´->
                  losallocstep p C o C´ o´ ->
                 exists o´´´, losallocstepn (S n) p C´ o´ C´´ o´´´.

Lemma lostidstepstar_transitivity : forall p C o C´ C´´ ,
        lostidstepstar p C o C´ o -> lostidstepstar p C´ o C´´ o->
        lostidstepstar p C o C´´ o.

Open Scope list_scope.
Lemma evalexprlist_idstep_star : forall v p f vl´ vl el tl tl´ ks m ir aux ,
       evalexprlist´ el tl vl m ->
       lostidstepstar p ((curs (sskip (Some v))), (kenil, kfuneval f vl´ tl´ el ks)) (m, ir , aux)
            (curs (sfexec f ((List.rev vl) ++ (cons v nil) ++ vl´) ((List.rev tl) ++ tl´)), (kenil, ks)) (m, ir, aux).


Lemma os_ret_not_step_ks : forall p o ks ,callcont ks = None -> intcont ks = None -> ~ exists o´ c,
   loststep p (curs sret,(kenil, ks)) o c o´.

Lemma os_exint_not_step_ks : forall p o ks ,callcont ks = None -> intcont ks = None -> ~ exists o´ c,
   loststep p (curs (sprim exint),(kenil, ks)) o c o´.

Lemma losidstepstar_imply_losidstepn : forall p C o C´ o´,
      lostidstepstar p C o C´ o´ -> exists n, losidstepn n p C o C´ o´.

Lemma losidstepstar_imply_losallocstepn : forall p C o C´ o´,
      losallocstepstar p C o C´ o´ -> exists n, losallocstepn n p C o C´ o´.

Lemma loststep_frame_prop : forall p C C´ o M oM oM´, joinmem o M oM ->
        ~ loststepabt p C o -> loststep p C oM C´ oM´ -> exists o´, joinmem o´ M oM´ /\
                   loststep p C o C´ o´.

Lemma callcont_nonone_addcont:
  forall ks ks1,
    callcont ks <> None -> callcont (ks ## ks1) <> None.

Lemma lostabt_cont_frm : forall p c ke ks ks´ o, ~ loststepabt p (c, (ke, ks)) o -> ~ loststepabt p (c, (ke, ks##ks´)) o.

Lemma loststep_genv_prev : forall p G E M isr aux C G´ E´ M´ isr´ aux´ C´,
 loststep p C (G, E, M ,isr, aux) C´ (G´,E´,M´,isr´,aux´) -> G = G´.


Lemma loststep_cont_locality: forall pu c ke ks o C o´ s, loststep pu (c, (ke, ks)) o C o´ ->
         exists C´ o´´, loststep pu (c, (ke, AddStmtToKs s ks)) o C´ o´´.
Lemma callcont_nonone_addstmts:
  forall ks s,
    callcont ks <> None -> callcont (AddStmtToKs s ks) <> None.

Qed.

Lemma estep_join_lstep: forall p c ke m c´ ke´ m´ isr aux Ms o1 Mf o2,
        estep c ke m c´ ke´ m´ -> joinmem (m, isr, aux) Ms o1 -> joinmem o1 Mf o2 ->
       exists o2´ C, loststep p (c, (ke, kstop)) o2 C o2´ /\ o2 = o2´ /\ C = (c´,(ke´,kstop)).

Lemma alloc_irev_prog : forall p vl dl ks o, ~ loststepabt p (curs (salloc vl dl), (kenil, ks)) o ->
                                  forall p´, ~ loststepabt p´ (curs (salloc vl dl), (kenil, ks)) o .

Lemma losallocstep_irev_prog : forall p C o C´ o´, losallocstep p C o C´ o´ ->
                                  forall p´, losallocstep p´ C o C´ o´ .

Lemma alloc_not_abort : forall p C o C´ o´ o´´ C´´ o1,
      losallocstep p C o C´ o´ ->
      losallocstep p C o C´ o´´ ->
      losallocstep p C´ o´ C´´ o1 ->
      ~ loststepabt p C´ o´´.

Definition frp (C : code) := (exists v ks, C = (curs (sfree nil v),(kenil,ks))/\
                                      callcont ks = None/\intcont ks = None).

Lemma not_free_cont_loc : forall p c ke ks o o´ f s E ks´ C, ~ frp (c, (ke, ks)) ->
                          loststep p (c, (ke, ks ## kcall f s E ks´)) o C o´->
                          ~ loststepabt p (c, (ke, ks ## kcall f s E kstop)) o ->
                          exists c´ ke´ ks´´,
                               loststep p (c, (ke, ks ## kcall f s E kstop)) o
                                          (c´,(ke´,ks´´## kcall f s E kstop)) o´ /\ C =
                                          (c´,(ke´,ks´´## kcall f s E ks´)).
  Lemma callcont_addkcall_nonone_imply_callcont_addkcall:
    forall (ks : stmtcont) (f : fid) (s : stmts)
           (ks´ : stmtcont)
           (E : env) ( ks1 : stmtcont),
      callcont (ks ## kcall f s E ks´) <> None ->
      callcont (ks ## kcall f s E ks1) <> None.

Qed.

Lemma loststepabt_cont_loststepabt : forall p c ke ks ks´ f s E o2,
   ~ loststepabt p (c, (ke, ks ## kcall f s E kstop)) o2 ->
               ~ loststepabt p (c, (ke, ks ## kcall f s E ks´)) o2.

Lemma cont_frame_mono : forall p c ke ks o C´ o´ ks´,
                       ~ loststepabt p (c, (ke, ks)) o ->
                       loststep p (c, (ke, ks ## ks´)) o C´ o´ ->
                       exists c´ ke´ ks´´, loststep p (c, (ke, ks)) o (c´, (ke´,ks´´)) o´
                         /\ C´ = (c´,(ke´,ks´´ ## ks´)).

Lemma loststepabt_cont_loststepabt´ :
      forall (p : progunit) (c : cureval) (ke : exprcont)
         (ks ks´ : stmtcont) (o2 : taskst),
       ~ loststepabt p (c, (ke, ks )) o2 ->
       ~ loststepabt p (c, (ke, ks ## ks´)) o2.

Lemma loststep_keq_while_mono :
forall p c ke ks e s o C o´ ,
     loststep p (c, (ke, ks ## kseq (swhile e s) kstop)) o C o´ ->
     ~ loststepabt p (c, (ke, ks)) o ->
     exists c´ ke´ ks´ , loststep p (c, (ke, ks)) o (c´,(ke´,ks´)) o´ /\
     C = (c´,(ke´,ks´## kseq (swhile e s) kstop)).
  Lemma callcont_kseq_kstop_nonone:
    forall (ks : stmtcont) (e : expr) (s : stmts),
      callcont (ks ## kseq (swhile e s) kstop) <> None ->
      callcont ks <> None.

Qed.

Lemma alloc_locality_pre1 :
  forall x l t v E E´ M1 M2 M3 M4 M5 M6 M´´,
    MemMod.join M1 M2 M3 ->
    MemMod.join M3 M4 M5 ->
    mapstoval l t v M´´ ->
    MemMod.join M5 M´´ M6 ->
    alloc x t E M5 E´ M6 ->
    exists M1´, alloc x t E M1 E´ M1´ /\
                MemMod.join M1 M´´ M1´.

Lemma alloc_locality_pre2 :
  forall x l t v b E E´ M1 M2 M3 M4 M5 M6 M7 M´´,
    MemMod.join M1 M2 M3 ->
    MemMod.join M3 M4 M5 ->
    mapstoval l t v M´´ ->
    MemMod.join M5 M´´ M7 ->
    alloc x t E M5 E´ M6 ->
    EnvMod.get E´ x = Some (b, t) ->
    store t M6 (b, BinNums.Z0) v = Some M7 ->
    exists M1´ M1´´, alloc x t E M1 E´ M1´ /\
                     store t M1´ (b, BinNums.Z0) v = Some M1´´ /\
                     MemMod.join M1 M´´ M1´´.

Lemma alloc_locality :forall p vl dl ks o o1 o2 C´ o2´ M1 M2,
                    length vl <= length_dl dl -> dl <> dnil ->
                    joinmem o M1 o1 -> joinmem o1 M2 o2 ->
                    loststep p (curs (salloc vl dl), (kenil, ks)) o2 C´ o2´->
                    exists o´ o1´,
   losallocstep p (curs (salloc vl dl), (kenil, ks)) o C´ o´ /\ joinmem o´ M1 o1´
                    /\ joinmem o1´ M2 o2´.

 Lemma loststep_keepG : forall p C o C´ o´, loststep p C o C´ o´ -> get_genv (get_smem o) = get_genv (get_smem o´).

Lemma allocsteop_imply_isalloc : forall C o o´,allocstep C o o´ -> isallocate C.

Lemma estep_lstep_deter :
  forall c G E M isr aux M1 M2 c´ ke´ m´ p ke ks o1 o2 C o2´,
    estep c ke (G, E, M) c´ ke´ m´ ->
    joinmem (G,E,M,isr,aux) M1 o1 ->
    joinmem o1 M2 o2 ->
    loststep p (c, (ke, ks)) o2 C o2´ ->
    o2 = o2´ /\ C = (c´,(ke´, ks )).
  Definition cjy_and := and.




Qed.

Lemma estep_frame_loststep : forall p Mf c ke m c´ ke´ m´ ks isr aux Ms o1 o2,
                      estep c ke m c´ ke´ m´ ->
                     joinmem (m, isr, aux) Ms o1 ->
                      joinmem o1 Mf o2 ->
               loststep p (c, (ke, ks)) o2 (c´, (ke´, ks)) o2.