Library lmachLib

Require Import include.
Require Import memory.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import baseTac.
Require Import val.

Lemma evalval_imply_evaltype : forall (e : expr) (m : smem) v ,
 evalval e m = Some v -> exists t,
 evaltype e m = Some t.

Lemma field_offset_plus : forall i d n z1 z2, field_offsetfld i d z1 = Some n ->
                field_offsetfld i d (Int.add z1 z2) = Some (Int.add n z2).

Lemma structtype_imply_fieldoffset : forall i d t, memory.ftype i d = Some t ->
                      exists n, field_offset i d = Some n.

Lemma eval_addr_prop : forall e m v, evaladdr e m = Some v ->
(exists e´, e = ederef e´)\/
( exists x, e = evar x) \/
(exists e´ id, e = efield e´ id) \/(exists e1 e2, e = earrayelem e1 e2).

Lemma evaltype_irrev_mem : forall e G E M M´, evaltype e (G,E,M) = evaltype e (G,E,M´).

Lemma evaltype_mono: forall e ge le m M m´ ,
  MemMod.join m M m´ -> evaltype e (ge, le, m´) = evaltype e (ge, le, m).

Lemma loadbytes_mono: forall m M m´ l n v ,
  MemMod.join m M m´ ->
  loadbytes m l n = Some v -> loadbytes m´ l n = loadbytes m l n.

Lemma loadm_mono: forall m M m´ t l v, MemMod.join m M m´ ->
  loadm t m l = Some v -> loadm t m´ l = loadm t m l .

Lemma load_mono: forall m M m´ t l v, MemMod.join m M m´ ->
  load t m l = Some v -> load t m´ l = load t m l .

Lemma getoff_mono: forall ge le m M m´ b o i e, MemMod.join m M m´ ->
   getoff b o i e (le, ge, m´) = getoff b o i e (le, ge, m).

Lemma evalvaladdr_mono:
  forall ge le e m M m´ v , ( MemMod.join m M m´ -> evalval e (ge, le, m) = Some v -> evalval e (ge, le, m´) = evalval e (ge, le, m)) /\
      (MemMod.join m M m´ -> evaladdr e (ge, le, m) = Some v -> evaladdr e (ge, le, m´) = evaladdr e (ge, le, m)).
  Lemma match_loadbytes :
    forall t m M m´ b v, MemMod.join m M m´ ->
     match loadbytes m (b, 0%Z) (typelen t) with
     | Some bls => Some (decode_val t bls)
     | None => None
     end = Some v ->
     match loadbytes m´ (b, 0%Z) (typelen t) with
     | Some bls => Some (decode_val t bls)
     | None => None
     end =
     match loadbytes m (b, 0%Z) (typelen t) with
     | Some bls => Some (decode_val t bls)
     | None => None
     end.






















Qed.

Lemma evalval_mono:
  forall ge le e m M m´ v , ( MemMod.join m M m´ -> evalval e (ge, le, m) = Some v -> evalval e (ge, le, m´) = evalval e (ge, le, m)).

Lemma evaladdr_mono:forall e M1 M2 M v ge le, MemMod.join M1 M2 M -> evaladdr e (ge, le, M1) = Some v -> evaladdr e (ge,le,M)= Some v.

Lemma typematch_mono:
  forall ge le m M m´ el dl, MemMod.join m M m´ -> (typematch el dl (ge, le, m) <-> typematch el dl (ge, le, m´)).

Lemma storebytes_mono: forall m M m´ m0 l vl, MemMod.join m M m´ ->
  storebytes m l vl = Some m0 -> (exists m0´,storebytes m´ l vl = Some m0´).

Lemma store_mono: forall m M m´ m0 a t v, MemMod.join m M m´ ->
  store t m a v = Some m0 -> (exists m0´,store t m´ a v = Some m0´).

Lemma freeb_mono: forall m M m´ m0 b i n, MemMod.join m M m´ ->
  freeb m b i n = Some m0 -> (exists m0´,freeb m´ b i n = Some m0´).

Lemma free_mono: forall m M m´ m0 b t, MemMod.join m M m´ ->
  free t b m = Some m0 -> (exists m0´,free t b m´ = Some m0´).

Lemma alloc_empmem_mapstoval:
  forall b t,
    mapstoval (b, 0)%Z t Vundef (allocb empmem b 0 (typelen t)).
  Lemma alloc_exist_ptomvallist : forall b i l,
    ptomvallist (b, i) (list_repeat l Undef)
      (allocb empmem b i l).
Lemma allocb_emp_get_none : forall b i l x, (x > 0)%Z ->
  MemMod.get (allocb empmem b (i + x) l) (b, i) = None.
  Qed.
Qed.

Lemma alloc_exist_mem_env:
       forall x t le M le´ M´, alloc x t le M le´ M´
    -> exists M´´ le´´ b v, mapstoval (b,0)%Z t v M´´ /\
          le´´ = EnvMod.sig x (b,t)/\ MemMod.join M M´´ M´/\
          EnvMod.join le le´´ le´.

Lemma set_empmem_sig_eq : forall a val, MemMod.set empmem a val = MemMod.sig a val.

Lemma beq_Z_Zeqb_ident : forall a b : Z, beq_Z a b = Z.eqb a b.
Goal forall a b : positive, beq_pos a b = Pos.eqb a b.

Qed.

Fixpoint init_mem (b:block) (i:offset) (vl:mvallist) {struct vl} : mem :=
match vl with
| nil => empmem
| u :: vl´ => MemMod.set (init_mem b (i+1)%Z vl´) (b, i)%Z u
end.

Definition fresh_index (M : mem) (b : block) (i : offset): Prop :=
forall offset, (offset >= 0)%Z -> MemMod.get M (b, i + offset)%Z = None.

Lemma init_mem_not_in_dom : forall b i vl n,
  (n > 0)%Z -> MemMod.get (init_mem b (i + n)%Z vl) (b, i) = None.

Lemma ptomvallist_init_mem : forall b i vl, ptomvallist (b, i) vl (init_mem b i vl).

Lemma init_mem_get_some : forall b i vl b1 ba ia,
  MemMod.get (init_mem b i vl) (ba, ia) = Some b1 ->
  b = ba /\ exists off, (off >= 0)%Z /\ ia = (i + off)%Z.

Lemma mem_set_a_set_a : forall M a val1 val2, MemMod.set (MemMod.set M a val1) a val2 = MemMod.set M a val2.

Lemma mem_set_a_set_a´ : forall M a v a´ v´, a <> a´ ->
  MemMod.set (MemMod.set M a v) a´ v´ = MemMod.set (MemMod.set M a´ v´) a v.

Lemma memset_allocb_comm : forall M b i n len, (n > 0)%Z -> ((MemMod.set (allocb M b (i + n) len) (b, i) Undef)
=
((allocb (MemMod.set M (b, i) Undef) b (i + n) len))).

Lemma allocb_storebytes_memjoin : forall M b i len val M´,
   fresh_index M b i -> storebytes (allocb M b i len) (b, i) (list_repeat len val) = Some M´ ->
   MemMod.join M (init_mem b i (list_repeat len val)) M´.

Lemma fresh_implies_fresh_index : forall M b i, fresh M b -> fresh_index M b i.

Lemma mem_join_sig_r : forall M a v, ~MemMod.indom M a -> MemMod.join M (MemMod.sig a v) (MemMod.set M a v).

Lemma env_join_sig_r : forall M a v, ~EnvMod.indom M a -> EnvMod.join M (EnvMod.sig a v) (EnvMod.set M a v).

Lemma alloc_store_exist_mem_env:
       forall x v b t le M le´ M´ M´´, alloc x t le M le´ M´ ->
          EnvMod.get le´ x = Some (b, t) ->
     store t M´ (b, BinNums.Z0) v = Some M´´
    -> exists M1 le´´, mapstoval (b,BinNums.Z0) t v M1 /\
          le´´ = EnvMod.sig x (b,t)/\ MemMod.join M M1 M´´/\
          EnvMod.join le le´´ le´.

Fixpoint length_dl (dl : decllist) : nat :=
 match dl with
 | dnil => O
 | dcons _ _ dl´ => S (length_dl dl´)
end.

Lemma eval_type_match: forall el tl vl dl m,
                 evalexprlist el tl vl m -> tlmatch tl dl ->
                  typematch el dl m.

Lemma revlcons_nil : forall d d´, revlcons d d´ = dnil -> d = dnil /\ d´ = dnil.

Lemma evalexprlist_len_eq : forall el tl vl m,
evalexprlist el tl vl m -> length el = length tl /\ length tl = length vl.

Lemma tlmatch_len_eq : forall tl dl, tlmatch tl dl -> length tl = length_dl dl.

Lemma revlcons_len_plus : forall d d´, length_dl (revlcons d d´) = (length_dl d + length_dl d´)%nat.

Lemma evallist_length_leb : forall (vl:vallist) d d´ tl el m,
        evalexprlist el tl vl m ->
        tlmatch tl d ->
  length vl <= length_dl (revlcons d d´).

Lemma rev_len_eq : forall vl : vallist, length (rev vl) = length vl.

Lemma evallist_length_leb_rev : forall (vl:vallist) d d´ tl el m,
        evalexprlist el tl vl m ->
        tlmatch tl d ->
  length (List.rev vl) <= length_dl (revlcons d d´).

Inductive evalexprlist´ : exprlist -> typelist -> vallist -> smem -> Prop :=
     | evalexprlist_b : forall m, evalexprlist´ nil nil nil m
     | evalexprlist_i : forall e el t tl v vl m, evalval e m = Some v ->
                             evaltype e m = Some t -> v<>Vundef -> evalexprlist´ el tl vl m ->
                             evalexprlist´ (cons e el) (cons t tl) (cons v vl) m .

Lemma evalexprlist_imply_evalexprlist´ : forall el tl vl m , evalexprlist el tl vl m ->
     evalexprlist´ el tl vl m.

Lemma evalexprlist´_imply_evalexprlist : forall el tl vl m , evalexprlist´ el tl vl m ->
     evalexprlist el tl vl m.

Lemma mapstoval_exist :
  forall l t v, exists m, mapstoval l t v m.
Goal forall b o i vl M,
  (i >= 1)%Z ->
  ptomvallist (b, (o + i)%Z) vl M ->
  MemMod.get M (b, o) = None.

Qed.

Lemma join_mapstoval_allocb´ :
  forall m b t M i,
    fresh m b ->
      mapstoval (b, i) t Vundef M ->
    MemMod.join m M (allocb m b i (typelen t)).
Lemma allocb_nindom : forall m b i1 i2 n, fresh m b -> (i1 < i2)%Z -> ~ MemMod.indom (allocb m b i2 n) (b, i1).


Qed.

Lemma join_mapstoval_allocb :
  forall m b t M,
    fresh m b ->
      mapstoval (b,0%Z) t Vundef M ->
    MemMod.join m M (allocb m b 0 (typelen t)).

Lemma length_list_repeat : forall (A : Type) len (v : A), length (list_repeat len v) = len.

Lemma join_mapstoval_store_allocb :
  forall m b t v M m´,
    fresh m b ->
      mapstoval (b,0%Z) t v M ->
        store t (allocb m b 0 (typelen t)) (b, 0%Z) v = Some m´->
    MemMod.join m M m´.
Lemma storebytes_memjoin : forall vl m M m´ b len i, fresh_index m b i -> storebytes (allocb m b i len) (b, i%Z) vl = Some m´ ->
  length vl = len -> ptomvallist (b, i%Z) vl M -> MemMod.join m M m´.


Qed.

Lemma allocb_storebytes_some : forall vl m b i len, fresh_index m b i ->
  length vl = len -> exists m´, storebytes (allocb m b i len) (b, i) vl = Some m´.

Lemma storebytes_ptomvallist_frame :
  forall b o vl1 vl2 M1 M2 M12 M12´,
    ptomvallist (b,o) vl1 M1 ->
    MemMod.join M1 M2 M12 ->
    storebytes M12 (b,o) vl2 = Some M12´ ->
    length vl1 = length vl2 ->
    exists M1´,storebytes M1 (b,o) vl2 = Some M1´ /\ MemMod.join M1´ M2 M12´.
  Lemma storebytes_indom :
    forall M l vl M´ l´,
      storebytes M l vl = Some M´ ->
        MemMod.indom M l´->
          MemMod.indom M´ l´.
Qed.

Lemma store_mapstoval_frame :
  forall M1 M2 M12 M12´ l t v1 v2,
    mapstoval l t v1 M1 ->
    MemMod.join M1 M2 M12 ->
    store t M12 l v2 = Some M12´ ->
    exists M1´, store t M1 l v2 = Some M1´ /\ MemMod.join M1´ M2 M12´.

Lemma storebytes_ptomvallist_eqlen_infer :
  forall M1 M2 b o l1 l2,
    ptomvallist (b, o) l1 M1 ->
    length l1 = length l2 ->
    storebytes M1 (b, o) l2 = Some M2 ->
    ptomvallist (b, o) l2 M2.
Lemma ptomvallist_get_none : forall l b i1 i2 m, (i2 < i1)%Z -> ptomvallist (b, i1) l m -> MemMod.get m (b, i2) = None.

Qed.

Lemma store_mapstoval_frame1 :
  forall M1 M2 M12 M12´ l t v1 v2,
    mapstoval l t v1 M1 ->
    MemMod.join M1 M2 M12 ->
    store t M12 l v2 = Some M12´ ->
    exists M1´, mapstoval l t v2 M1´ /\ store t M1 l v2 = Some M1´ /\ MemMod.join M1´ M2 M12´.

Lemma eval_length_tlmatch :
  forall tl dl,
    tlmatch tl dl -> length tl = length_dl dl.

Open Local Scope nat_scope.
Lemma length_prop : forall (vl:vallist) tl d1 d2, length vl = length tl -> tlmatch (rev tl) d1 ->
          length vl <= length_dl (revlcons d1 d2).

Lemma eval_length_rev : forall (tl:typelist) (vl:vallist) , length vl = length tl -> length (rev vl) = length (rev tl).

Lemma len_rev: forall (vl:vallist)( tl:typelist) , length vl = length tl -> length vl = length (rev tl).

Lemma evaltype_eq_prop : forall G E M1 M2 e t, evaltype e (G,E, M1) = Some t ->
               evaltype e (G,E,M2) = Some t.

Lemma load_mem_mono :
  forall t M M´ a v,
    load t M a = Some v ->
    MemMod.sub M M´ ->
    load t M´ a = Some v.

Lemma evalval_eq_prop :
  forall e G E M M´ v,
    evalval e (G, E, M) = Some v ->
    MemMod.sub M M´ ->
    evalval e (G, E, M´) = Some v.

Lemma evaltype_deter :
  forall G E M1 M2 e t1 t2,
    evaltype e (G, E, M1) = Some t1 ->
    evaltype e (G, E, M2) = Some t2 ->
    t1 = t2.

Lemma evalval_deter :
  forall G E M1 M2 e v1 v2,
    evalval e (G, E, M1) = Some v1 ->
    evalval e (G, E, M2) = Some v2 ->
    MemMod.sub M1 M2 ->
    v1 = v2.

Lemma load_mem_deter :
  forall t M1 M2 a v1 v2,
    load t M1 a = Some v1 ->
    load t M2 a = Some v2 ->
    MemMod.sub M1 M2 ->
    v1 = v2.