Lemma validAccessMemMeta__validStoreMemMeta : forall m mm l vm,
  (exists vm, accessMemMeta m mm l = Some vm) <-> (exists m', storeMemMeta m mm l vm = Some m').

Lemma validAccessMemMeta__validAccessMem : forall m mm l,
  (exists vm, accessMemMeta m mm l = Some vm) <-> (exists v, accessMem m l= Some v).

Lemma validStoreMemMeta__validStoreMem : forall m mm l vm1 v2,
  (exists m', storeMemMeta m mm l vm1 = Some m') <-> (exists m', storeMem m l v2= Some m').

Lemma validAccessMemMeta__validStoreMem : forall m mm l v,
  (exists vm, accessMemMeta m mm l = Some vm) <-> (exists m', storeMem m l v= Some m').

Lemma validStoreMemMeta__validAccessMem : forall m mm l vm,
  (exists m', storeMemMeta m mm l vm = Some m') <-> (exists v, accessMem m l = Some v).

Lemma invalidAccessMemMeta__invalidStoreMemMeta : forall m mm l v,
  (accessMemMeta m mm l = None) <-> (storeMemMeta m mm l v = None).

Lemma invalidAccessMem__invalidStoreMem : forall m l v,
  (accessMem m l = None) <-> (storeMem m l v = None).

Lemma validAccessMem__validAddress : forall m l,
  (exists v, accessMem m l = Some v) ->
  validAddress m l.

Lemma validAccessMemMeta__validAddress : forall m mm l,
  (exists v, accessMemMeta m mm l = Some v) ->
  validAddress m l.

Lemma validStoreMemMeta__validAddress : forall m mm l v,
  (exists m', storeMemMeta m mm l v = Some m') ->
  validAddress m l.

Lemma validStoreMem__validAddress : forall m l v,
  (exists m', storeMem m l v = Some m') ->
  validAddress m l.

Lemma accessMemMeta_uniqBehavior : forall v m mm l v',
  (accessMemMeta m mm l = Some v -> accessMemMeta m mm l = Some v' -> v = v') /\
  (accessMemMeta m mm l = None -> accessMemMeta m mm l = None).

Lemma accessMemMeta_accessMem_Some : forall v m mm l be,
  accessMemMeta m mm l = Some (v, be) ->
  accessMem m l = Some v.

Lemma accessMem_accessMemMeta_Some : forall v m mm l,
  accessMem m l = Some v ->
  exists be, accessMemMeta m mm l = Some (v, be).

Lemma accessMemMeta_accessMem_None : forall m mm l,
  accessMemMeta m mm l = None ->
  accessMem m l = None.

Lemma accessMem_accessMemMeta_None : forall m mm l,
  accessMem m l = None ->
  accessMemMeta m mm l = None.

Lemma storeMemMeta_uniqBehavior : forall v m mm l v',
  ((exists m', storeMemMeta m mm l v = Some m') -> (exists m', storeMemMeta m mm l v' = Some m')) /\
  (storeMemMeta m mm l v = None -> storeMemMeta m mm l v' = None).

Lemma storeMemMeta_storeMem_Some : forall M MM l v m M' MM',
  storeMemMeta M MM l (v, m) = Some (M', MM') ->
  storeMem M l v = Some M'.

Lemma storeMem_storeMemMeta_Some : forall M MM l v m M',
  storeMem M l v = Some M' ->
  exists MM', storeMemMeta M MM l (v, m) = Some (M', MM').

Lemma storeMemMeta_storeMem_None : forall M MM l v m,
  storeMemMeta M MM l (v, m) = None ->
  storeMem M l v = None.

Lemma storeMem_storeMemMeta_None : forall M MM l v m,
  storeMem M l v = None ->
  storeMemMeta M MM l (v, m) = None.

Lemma storeMem__inversion : forall M loc d v be M' MM,
  storeMem M loc d = Some M' ->
  accessMemMeta M MM loc = Some (v, be) ->
  accessMemMeta M' MM loc = Some (d, be) /\
  (forall l v,
    l <> loc ->
    accessMemMeta M MM l = Some v ->
    accessMemMeta M' MM l = Some v
  ) /\
  (forall l,
    accessMemMeta M MM l = None ->
    accessMemMeta M' MM l = None
  )
  .

Lemma storeMemMeta__inversion : forall M MM loc d M' MM',
  storeMemMeta M MM loc d = Some (M', MM') ->
  accessMemMeta M' MM' loc = Some d /\
  (forall l v,
    l <> loc ->
    accessMemMeta M MM l = Some v ->
    accessMemMeta M' MM' l = Some v
  ) /\
  (forall l,
    accessMemMeta M MM l = None ->
    accessMemMeta M' MM' l = None
  )
  .

Lemma storeMemMeta__validAddress: forall M MM M' MM' d loc l,
  storeMemMeta M MM loc d = Some (M', MM') ->
  (validAddress M l <->validAddress M' l).

Lemma storeMem__validAddress: forall M M' loc d l,
  storeMem M loc d = Some M' ->
  (validAddress M l <-> validAddress M' l).

Lemma storeMemMeta__invalidAddress: forall M MM M' MM' d loc l,
  storeMemMeta M MM loc d = Some (M', MM') ->
  (~validAddress M l <->~validAddress M' l).

Lemma storeMem__invalidAddress: forall M M' d loc l,
  storeMem M loc d = Some M' ->
  (~validAddress M l <->~validAddress M' l).

Lemma storeMem__invalidAddresses: forall M M' d loc l,
  storeMem M loc d = Some M' ->
  (~validAddress M l <-> ~validAddress M' l).

Lemma storeMemMeta__invalidAddresses: forall M MM M' MM' d loc l,
  storeMemMeta M MM loc d = Some (M', MM') ->
  (~validAddress M l <-> ~validAddress M' l).

Lemma invalidStoreMem__invalidAddress : forall m l v,
  (storeMem m l v = None) ->
  ~validAddress m l.

Lemma invalidStoreMemMeta__invalidAddress : forall m mm l v,
  (storeMemMeta m mm l v = None) ->
  ~validAddress m l.

Lemma malloc__inversion : forall E n M' MM' AMB' G' S' RI' r' loc ri,
  malloc E n = Some ((MkEnv M' MM' AMB' G' S' RI' r'), loc, ri) ->
  exists M, exists MM, exists AMB, exists RI, exists r,
  E = MkEnv M MM AMB G' S' RI r /\
  (baseAddress<=loc /\ loc+ n <= E.(stack).(top) /\ n > 0) /\
  (forall l v,
    accessMemMeta M MM l = Some v -> accessMemMeta M' MM' l = Some v
  ) /\
  (forall l,
    l < loc \/ l >= loc + n ->
    accessMemMeta M MM l = None -> accessMemMeta M' MM' l = None
    ) /\
  (forall l,
    loc <= l < loc + n -> accessMemMeta M MM l = None
  ) /\
  (forall l,
    loc <= l < loc + n ->
    accessMemMeta M' MM' l = Some (0, (0, 0,0,0))
  ) /\
  (forall r0,
    r0 <> ri -> RI r0 = RI' r0
  ) /\
  RI ri = 0 /\
  RI' ri = r /\
  r' = r + 1 /\
  AMB' = addAllocMemBlock AMB loc (loc+n)
  .

Lemma malloc__umalloc_Some : forall E n E' b r,
  malloc E n = Some (E', b, r) ->
  umalloc (Env2uEnv E) n = Some (Env2uEnv E', b).

Lemma _free__inversion : forall E M' MM' AMB' G' S' RI' r' loc,
  free E loc = Some (MkEnv M' MM' AMB' G' S' RI' r') ->
  exists M, exists MM, exists AMB, exists RI,
    E = MkEnv M MM AMB G' S' RI r'.

Lemma free__inversion : forall E M' MM' AMB' G' S' RI' r' loc,
  wfEnv E ->
  free E loc = Some (MkEnv M' MM' AMB' G' S' RI' r') ->
  exists M, exists MM, exists AMB, exists RI,
  exists b, exists e, exists e', exists r, exists ri,
  E = MkEnv M MM AMB G' S' RI r' /\
  accessMem M loc = Some b /\ AMB b = Some e /\
  accessMemMeta M MM loc = Some (b, (b, e', r, ri)) /\
  (loc < b \/ loc >= e ->
    exists v, accessMemMeta M' MM' loc = Some (v, (0, 0,0,0))
  ) /\
  (forall l a,
    l < b \/ l >= e -> l <> loc ->
    accessMemMeta M MM l = a -> accessMemMeta M' MM' l = a
  ) /\
  (forall l,
    b <= l < e -> exists v, accessMemMeta M MM l = Some v
  ) /\
  (forall l,
    b <= l < e -> accessMemMeta M' MM' l = None
  ) /\
  (forall r0,
    r0 <> ri -> RI r0 = RI' r0
  ) /\
  e <= E.(stack).(top) /\
  b >= baseAddress /\
  RI ri = r /\
  RI' ri = 0 /\
  AMB' = removeAllocMemBlock AMB b
  .

Lemma free__ufree_Some : forall E loc E',
  free E loc = Some E' ->
  ufree (Env2uEnv E) loc = Some (Env2uEnv E').

Lemma createFrame__inversion : forall E f E',
  createFrame E f = Some E' ->
  exists ri, exists F,
  f = Stack2frame (E'.(stack)) /\
  E.(global) = E'.(global) /\
  E.(amb) = E'.(amb) /\
  head (E'.(stack).(frames)) = Some F /\
  F.(to) = E.(stack).(top) /\
  F.(from) = E'.(stack).(top) /\
  baseAddress < E'.(stack).(top) < E.(stack).(top) /\
  tail (E'.(stack).(frames)) = E.(stack).(frames) /\
  revInfo E ri = 0 /\
  revInfo E' ri + 1 = E'.(rev) /\
  E'.(rev) = E.(rev) + 1 /\
  (forall r0,
    r0 <> ri -> revInfo E r0 = revInfo E' r0
  ) /\
  (forall v t,
      f v = Some t ->
     exists l,
        lookUpStack E'.(stack) v = Some (l, t, E.(rev) , ri) /\
        F.(from) <= l < F.(to)
  ) /\
  (forall l v,
     accessMemMeta E.(mem) E.(mmeta) l = Some v -> accessMemMeta E'.(mem) E'.(mmeta) l = Some v
  ) /\
  (forall l,
    l < F.(from) \/ l >= F.(to) ->
    accessMemMeta E.(mem) E.(mmeta) l = None -> accessMemMeta E'.(mem) E'.(mmeta) l = None
    ) /\
  (forall l,
      F.(from) <= l < F.(to) ->
      accessMemMeta E.(mem) E.(mmeta) l = None
  ) /\
  (forall l,
      F.(from) <= l < F.(to) ->
      accessMemMeta E'.(mem) E'.(mmeta) l = Some (0, (0, 0, 0, 0))
  ) /\
  wfFrameNoOverlapped F /\
  F.(fr) = E.(rev) /\
  F.(fri) = ri /\
  E'.(stack).(sr) = F.(fr)
  .

Lemma createFrame__ucreateFrame_Some : forall E f E',
  createFrame E f = Some E' ->
  ucreateFrame (Env2uEnv E) f = Some (Env2uEnv E').

Lemma destroyFrame__inversion : forall E E',
  destroyFrame E = Some E' ->
  exists F,
  E.(global) = E'.(global) /\
  E.(amb) = E'.(amb) /\
  E.(rev) = E'.(rev) /\
  head (E.(stack).(frames)) = Some F /\
  E'.(stack).(top) = F.(to) /\
  E'.(stack).(frames) = tail (E.(stack).(frames)) /\
  (forall l a,
    l < F.(from) \/ l >= F.(to) ->
    accessMemMeta (mem E) (mmeta E) l = a -> accessMemMeta (mem E') (mmeta E') l = a
  ) /\
  (forall l,
    F.(from) <= l < F.(to) -> exists v, accessMemMeta (mem E) (mmeta E) l = Some v
  ) /\
  (forall l,
    F.(from) <= l < F.(to) -> accessMemMeta (mem E') (mmeta E') l = None
  ) /\
  (forall r0,
    r0 <> F.(fri) -> revInfo E r0 = revInfo E' r0
  ) /\
  revInfo E (F.(fri)) = F.(fr) /\
  revInfo E' (F.(fri)) = 0 /\
  (head (E'.(stack).(frames)) = None -> E'.(stack).(sr) = 1) /\
  (forall F0, head (E'.(stack).(frames)) = Some F0 -> E'.(stack).(sr) = F0.(fr))
  .

Lemma destroyFrame__udestroyFrame_Some : forall E E',
  destroyFrame E = Some E' ->
  udestroyFrame (Env2uEnv E) = Some (Env2uEnv E').

Lemma accessMemMeta_unchanged_store : forall M MM M' MM' l loc a,
  (forall l v, l <> loc -> accessMemMeta M MM l = Some v -> accessMemMeta M' MM' l = Some v) ->
  (forall l, accessMemMeta M MM l = None -> accessMemMeta M' MM' l = None) ->
  accessMemMeta M' MM' l = a ->
  l <> loc ->
  accessMemMeta M MM l = a.

Lemma wfFrame__storeMemMeta__wfFrame : forall M MM F RI loc v b e r ri M' MM' rev,
  wfFrame M RI F ->
  wfData M RI (b, e, r, ri) rev ->
  storeMemMeta M MM loc (v, (b, e, r, ri)) = Some (M', MM') ->
  wfFrame M' RI F.

Lemma wfStack__storeMemMeta__wfStack : forall M MM S RI loc v b e r ri M' MM' rev,
  wfStack M RI rev S ->
  rev >= 2 ->
  wfData M RI (b, e, r, ri) rev ->
  storeMemMeta M MM loc (v, (b, e, r, ri)) = Some (M', MM') ->
  wfStack M' RI rev S.

Lemma wfE__storeMemMeta__wfE : forall M MM AMB G S RI loc v b e r ri M' MM' rev,
  wfEnv (MkEnv M MM AMB G S RI rev) ->
  wfData M RI (b, e, r, ri) rev ->
  storeMemMeta M MM loc (v, (b, e, r, ri)) = Some (M', MM') ->
  wfOverlapped (MkEnv M MM AMB G S RI rev) b e r ri ->
  wfGlobalPtr b r ri ->
  wfStackPtr S RI b e r ri ->
  wfNonGlobalPtr e r ->
  wfNonStackPtr S RI b r ri ->
  wfOverlappedAMB (MkEnv M MM AMB G S RI rev) b e r ri ->
  wfUniqRentryH (MkEnv M MM AMB G S RI rev) b e r ri ->
  wfUniqRentryGS (MkEnv M MM AMB G S RI rev) r ri ->
  wfEnv (MkEnv M' MM' AMB G S RI rev).

Lemma wfFrame__storeMem__wfFrame : forall M F RI loc v M',
  wfFrame M RI F ->
  storeMem M loc v = Some M' ->
  wfFrame M' RI F.

Lemma wfStack__storeMem__wfStack : forall M S RI loc v M' rev,
  wfStack M RI rev S ->
  storeMem M loc v = Some M' ->
  wfStack M' RI rev S.

Lemma wfE__storeMem__wfE : forall M MM AMB G S RI loc v M' rev,
  wfEnv (MkEnv M MM AMB G S RI rev) ->
  storeMem M loc v = Some M' ->
  wfEnv (MkEnv M' MM AMB G S RI rev).

Lemma malloc_dec : forall E n,
  (exists E', exists b, exists r, malloc E n = Some (E', b, r)) \/ malloc E n = None.

Lemma accessMemMeta_dec : forall M MM loc,
  (exists d, accessMemMeta M MM loc = Some d) \/ accessMemMeta M MM loc = None.

Lemma assertion_spatial_ptr_dec : forall v be t,
  assertion_spatial_ptr v be t \/ ~assertion_spatial_ptr v be t.

Lemma assertion_temporal_ptr_dec : forall be t RI,
  assertion_temporal_ptr be t RI \/ ~assertion_temporal_ptr be t RI.

Lemma assertion_ptr_dec : forall v be t RI,
  assertion_ptr v be t RI \/ ~assertion_ptr v be t RI.

Lemma storeMemMeta_dec : forall M MM loc d,
  (exists m, storeMemMeta M MM loc d = Some m) \/ storeMemMeta M MM loc d = None.

Lemma isPtr_dec : forall t,
  isPtr t \/ ~isPtr t.

Lemma storeMem_dec : forall E loc d,
  (exists m, storeMem E loc d = Some m) \/ storeMem E loc d = None.

Lemma free_dec : forall E l,
  (exists E', free E l = Some E') \/ free E l = None.

Lemma createFrame_dec : forall E f,
  (exists E', createFrame E f = Some E') \/ createFrame E f = None.

Lemma destroyFrame_dec : forall E,
  (exists E', destroyFrame E = Some E') \/ destroyFrame E = None.

Lemma wfFrms_top_interval : forall rev S,
  wfFrms rev S ->
  baseAddress <= top S <= maxAddress.

Lemma wfStack_top_interval : forall M RI rev S,
  wfStack M RI rev S ->
  baseAddress <= top S <= maxAddress.

Lemma wfEnv_top_interval : forall E,
  wfEnv E -> baseAddress <= top (stack E) <= maxAddress.

Lemma wfStack_topS_eq_fromF_head : forall M RI rev S F,
  wfStack M RI rev S ->
  head (frames S) = Some F ->
  from F = top S.

Lemma wfEnv_topS_eq_fromF_head : forall E F,
  wfEnv E ->
  head (frames (stack E)) = Some F ->
  from F = top (stack E).

Lemma wfStack_F_interval_head : forall M RI rev S F,
  wfStack M RI rev S ->
  head (frames S) = Some F ->
  baseAddress <= from F <= to F /\ to F <= maxAddress.

Lemma wfEnv_F_interval_head : forall E F,
  wfEnv E ->
  head (frames (stack E)) = Some F ->
  baseAddress <= from F <= to F /\ to F <= maxAddress.

Lemma wfEnv_frF_interval_head : forall E F,
  wfEnv E ->
  head (frames (stack E)) = Some F ->
  2 <= fr F <= E.(rev).

Lemma wfFrms_fromF_interval_In : forall rev S F,
  wfFrms rev S ->
  In F (frames S) ->
  baseAddress <= top S /\ (top S) <= from F <= maxAddress.

Lemma wfEnv_fromF_interval_In : forall E F,
  wfEnv E ->
  In F (frames (stack E)) ->
  baseAddress <= top (stack E) /\ (top (stack E)) <= from F <= maxAddress.

Lemma wfFrms_headTo_lesseq_tailFrom : forall F1 F2 Fs S rev,
  wfFrms rev S ->
  F1 :: Fs = frames S ->
  In F2 Fs ->
  to F1 <= from F2.

Lemma wfEnv_headTo_lesseq_tailFrom : forall F1 F2 Fs E,
  wfEnv E ->
  F1 :: Fs = frames (stack E) ->
  In F2 Fs ->
  to F1 <= from F2.

Lemma wfEnv_frF_interval_In : forall E F,
  wfEnv E ->
  In F (frames (stack E))->
  2 <= fr F < E.(rev).

Lemma wfFrms_srS_interval : forall rev S,
  wfFrms rev S ->
  1 <= sr S < rev.

Lemma wfFrms_srS_in_nonempty : forall rev S F,
  wfFrms rev S ->
  In F (frames S)->
  fr F <= S.(sr).

Lemma wfFrms_headfr_gt_tailfr : forall F1 F2 Fs S rev,
  wfFrms rev S ->
  F1 :: Fs = frames S ->
  In F2 Fs ->
  fr F1 > fr F2.

Lemma wfFrms_sr_eq_Ffr : forall rev Fs top sr,
  wfFrms rev (MkStack Fs top sr) ->
  Fs <> nil ->
  exists F, head Fs = Some F /\ F.(fr) = sr.

Lemma wfFrms__monorev: forall S rev1 rev2,
  wfFrms rev1 S ->
  rev1 < rev2 ->
  wfFrms rev2 S.

Lemma wf_AType__wf_subAType : forall s id t',
  wf_AType (A_Pointer (P_Struct s)) ->
  getStructType s id = Some t' ->
  wf_AType t'.

Lemma wf_lhs__wf_AType : forall G lhs f t,
  wf_lhs G f lhs t -> wf_AType t.

Lemma wf_rhs__wf_AType : forall G f rhs t,
  wf_rhs G f rhs t -> wf_AType t.

Lemma wf_lhs_uniq : forall S f lhs t t',
  wf_lhs S f lhs t ->
  wf_lhs S f lhs t' ->
  t = t'.

Lemma wf_AType__some_size : forall p,
   wf_AType (A_Pointer p) ->
   exists size, sizeOfPType p = Some size.

Lemma wf_PType__sizeOfType: forall p0,
  wf_PType p0 ->
  exists s, sizeOfPType p0 = Some s.

Lemma dataCast__valid : forall t' d t,
  wf_AType t ->
  exists d', dataCast t' d t = d'.

Lemma sizeOfAType_one : forall t,
  sizeOfAType t = 1.


Lemma sizeOfFields__non_zero : forall s,
  sizeOfStruct s >=0.

Lemma getStructType__getStructOffset : forall s id t,
  getStructType s id = Some t ->
  exists offset, getStructOffset s id = Some offset.

Lemma struct__subfield : forall s id offset t',
  getStructOffset s id = Some offset ->
  getStructType s id = Some t' ->
  offset + sizeOfAType t' <= sizeOfStruct s.

Lemma le_ge__eq : forall (i j:nat),
   i <= j ->
   j <= i ->
   i = j.


Lemma omega_ex1 : forall a b c d,
  d <= a <= b - c ->
  c > 0 ->
  d <> 0 ->
  (b > c /\ a < b).


Lemma r_lesseq_rev : forall E l d,
  wfEnv E ->
  accessMemMeta (mem E) (mmeta E) l = Some d ->
  snd (fst (snd d)) < (rev E).

Lemma overlapped_interval : forall b e b' e' i,
  b <= i < e ->
  b' <= i < e' ->
  ((b <= b' /\ b' < e) \/ (b' <=b /\ b < e')).

Lemma overlapped_interval_sub : forall b e b' e' b0 e0,
  ((b' <= b0 < e') \/ (b0 <= b' < e0)) ->
  b <= b' -> b' < e' -> e' <= e ->
  ((b <= b0 < e) \/ (b0 <= b < e0)).

Lemma neqzero__largerthanzero : forall n,
  n <> 0 -> n > 0.

Lemma nateq_plus_inv : forall n m i,
  n + i = m + i ->
  n = m.