WfEnv



This file proves that primitves preserve well-formed Envs.

malloc preserves well-formed Envs.

Lemma malloc__validAddress: forall M MM AMB G S RI rev M' MM' AMB' G' S' RI' rev' loc ri size l,
  validAddress M l ->
  malloc (MkEnv M MM AMB G S RI rev) size = Some ((MkEnv M' MM' AMB' G' S' RI' rev'), loc, ri) ->
  validAddress M' l.

Lemma accessMemMeta_unchanged_malloc : forall M MM M' MM' l from to a,
  (forall l v, accessMemMeta M MM l = Some v -> accessMemMeta M' MM' l = Some v) ->
  (forall l, l < from \/ l >= to -> accessMemMeta M MM l = None -> accessMemMeta M' MM' l = None) ->
  accessMemMeta M' MM' l = a ->
  l < from \/ l >= to ->
  accessMemMeta M MM l = a.

Lemma malloc__wfE__wfOverlapped_case : forall l1 v1 b1 e1 r1 ri1 l2 v2 b2 e2 r2 ri2 M MM AMB M' MM' G' S' RI rev loc RI' ri size,
  wfEnv (MkEnv M MM AMB G' S' RI rev) ->
  (forall l v b e r ri,
    accessMemMeta M MM l = Some (v, (b, e, r, ri)) ->
    wfOverlapped (MkEnv M MM AMB G' S' RI rev) b e r ri) ->
  accessMemMeta M' MM' l1 = Some (v1, (b1, e1, r1, ri1)) ->
  accessMemMeta M' MM' l2 = Some (v2, (b2, e2, r2, ri2)) ->
 ((b1 <= b2 /\ b2 < e1) \/ (b2 <=b1 /\ b1 < e2)) ->
  minAddress <= b1 < e1 -> minAddress <= b2 < e2 ->
  r1 <> 0 ->
  r2 <> 0 ->
  ( l1 < loc \/ l1 >= loc + size ) ->
  ( l2 < loc \/ l2 >= loc + size ) ->
  RI' ri = rev ->
  (forall l v,
    accessMemMeta M MM l = Some v -> accessMemMeta M' MM' l = Some v
  ) ->
  (forall l,
    l < loc \/ l >= loc + size ->
    accessMemMeta M MM l = None -> accessMemMeta M' MM' l = None
    ) ->
  (forall r0, r0 <> ri -> RI r0 = RI' r0) ->
  ((r1 <> r2 -> RI' ri1 <> r1 \/ RI' ri2 <> r2) /\
      (r1 = r2 -> ri1 = ri2)).

Lemma malloc__wfE__wfOverlappedAMB_case : forall b0 e0 l1 v1 b1 e1 r1 ri1 l2 v2 b2 e2 r2 ri2 M MM AMB M' MM' G' S' RI rev loc RI' ri size,
  wfEnv (MkEnv M MM AMB G' S' RI rev) ->
  (forall l v b e r ri,
    accessMemMeta M MM l = Some (v, (b, e, r, ri)) ->
    wfOverlappedAMB (MkEnv M MM AMB G' S' RI rev) b e r ri) ->
  accessMemMeta M' MM' l1 = Some (v1, (b1, e1, r1, ri1)) ->
  accessMemMeta M' MM' l2 = Some (v2, (b2, e2, r2, ri2)) ->
  addAllocMemBlock AMB loc (loc+size) b0 = Some e0 ->
 ((b1 <= b0 /\ b0 < e1) \/ (b0 <=b1 /\ b1 < e0)) ->
 ((b2 <= b0 /\ b0 < e2) \/ (b0 <=b2 /\ b2 < e0)) ->
  minAddress <= b1 < e1 -> minAddress <= b2 < e2 ->
  r1 <> 0 ->
  r2 <> 0 ->
  ( l1 < loc \/ l1 >= loc + size ) ->
  ( l2 < loc \/ l2 >= loc + size ) ->
  RI' ri = rev ->
  (forall l v,
    accessMemMeta M MM l = Some v -> accessMemMeta M' MM' l = Some v
  ) ->
  (forall l,
    l < loc \/ l >= loc + size ->
    accessMemMeta M MM l = None -> accessMemMeta M' MM' l = None
    ) ->
  size > 0 ->
  (forall l,
    loc <= l < loc + size -> accessMemMeta M MM l = None
    ) ->
  (forall r0, r0 <> ri -> RI r0 = RI' r0) ->
  baseAddress <= loc ->
  loc + size <= S'.(top) ->
  size > 0 ->
  ((r1 <> r2 -> RI' ri1 <> r1 \/ RI' ri2 <> r2) /\
      (r1 = r2 -> ri1 = ri2)).

Lemma malloc__wfE__wfUniqRentryH_case : forall l1 v1 b1 e1 r1 ri1 l2 v2 b2 e2 r2 ri2 M MM AMB M' MM' G' S' RI rev loc size,
  wfEnv (MkEnv M MM AMB G' S' RI rev) ->
  (forall l v b e r ri,
    accessMemMeta M MM l = Some (v, (b, e, r, ri)) ->
    wfUniqRentryH (MkEnv M MM AMB G' S' RI rev) b e r ri) ->
  accessMemMeta M' MM' l1 = Some (v1, (b1, e1, r1, ri1)) ->
  accessMemMeta M' MM' l2 = Some (v2, (b2, e2, r2, ri2)) ->
  minAddress <= b1 < e1 -> minAddress <= b2 < e2 ->
  r1 <> 0 ->
  ( l1 < loc \/ l1 >= loc + size ) ->
  ( l2 < loc \/ l2 >= loc + size ) ->
  (forall l v,
    accessMemMeta M MM l = Some v -> accessMemMeta M' MM' l = Some v
  ) ->
  (forall l,
    l < loc \/ l >= loc + size ->
    accessMemMeta M MM l = None -> accessMemMeta M' MM' l = None
    ) ->
  r1 = r2 -> ri1 = ri2.

Lemma malloc__wfFrame: forall M MM AMB G' F S' RI rev M' MM' RI' loc ri size,
  wfFrame M RI F ->
  In F (frames S') ->
  malloc (MkEnv M MM AMB G' S' RI rev) size =
    Some ((MkEnv M' MM' (addAllocMemBlock AMB loc (loc+size)) G' S' RI' (RI' ri+1)), loc, ri) ->
  wfFrame M' RI' F.

Lemma malloc__wfStack: forall M MM AMB G' S' RI rev M' MM' RI' loc ri size,
  wfStack M RI rev S' ->
  malloc (MkEnv M MM AMB G' S' RI rev) size = Some ((MkEnv M' MM' (addAllocMemBlock AMB loc (loc+size)) G' S' RI' (RI' ri+1)), loc, ri) ->
  wfStack M' RI' (RI' ri+1) S'.

Lemma malloc__wfMem: forall E E' loc ri size,
  wfEnv E ->
  malloc E size = Some (E', loc, ri) ->
  wfMem (mem E') (mmeta E') (revInfo E') (rev E').

Lemma malloc__wfE: forall E E' loc ri size,
  wfEnv E ->
  malloc E size = Some (E', loc, ri) ->
  wfEnv E'.

free preserves well-formed Envs.


Lemma accessMemMeta_unchanged_free : forall M MM M' MM' l b e a loc,
  (forall l a, l < b \/ l >= e -> l <> loc -> accessMemMeta M MM l = a -> accessMemMeta M' MM' l = a) ->
  accessMemMeta M' MM' l = a ->
  l < b \/ l >= e -> l <> loc ->
  accessMemMeta M MM l = a.

Lemma free__wfE__wfOverlapped_case : forall loc l1 v1 b1 e1 r1 ri1 l2 v2 b2 e2 r2 ri2 M MM AMB M' MM' G' S' RI rev' RI' ri b e,
  wfEnv (MkEnv M MM AMB G' S' RI rev') ->
  (forall l v b e r ri,
    accessMemMeta M MM l = Some (v, (b, e, r, ri)) ->
    wfOverlapped (MkEnv M MM AMB G' S' RI rev') b e r ri ) ->
  accessMemMeta M' MM' l1 = Some (v1, (b1, e1, r1, ri1)) ->
  accessMemMeta M' MM' l2 = Some (v2, (b2, e2, r2, ri2)) ->
 ((b1 <= b2 /\ b2 < e1) \/ (b2 <=b1 /\ b1 < e2)) ->
  minAddress <= b1 < e1 -> minAddress <= b2 < e2 ->
  r1 <> 0 ->
  r2 <> 0 ->
  ( l1 < b \/ l1 >= e ) ->
  ( l2 < b \/ l2 >= e ) ->
  RI' ri = 0 ->
  (forall l a,
    l < b \/ l >= e -> l <> loc ->
    accessMemMeta M MM l = a -> accessMemMeta M' MM' l = a
    ) ->
  (forall r0, r0 <> ri -> RI r0 = RI' r0) ->
  l1 <> loc ->
  l2 <> loc ->
  ((r1 <> r2 -> RI' ri1 <> r1 \/ RI' ri2 <> r2) /\
      (r1 = r2 -> ri1 = ri2)).

Lemma free__wfE__wfOverlappedAMB_case : forall b0 e0 loc l1 v1 b1 e1 r1 ri1 l2 v2 b2 e2 r2 ri2 M MM AMB M' MM' G' S' RI rev' RI' ri b e,
  wfEnv (MkEnv M MM AMB G' S' RI rev') ->
  (forall l v b e r ri,
    accessMemMeta M MM l = Some (v, (b, e, r, ri)) ->
    wfOverlappedAMB (MkEnv M MM AMB G' S' RI rev') b e r ri ) ->
  accessMemMeta M' MM' l1 = Some (v1, (b1, e1, r1, ri1)) ->
  accessMemMeta M' MM' l2 = Some (v2, (b2, e2, r2, ri2)) ->
 ((b1 <= b0 /\ b0 < e1) \/ (b0 <=b1 /\ b1 < e0)) ->
 ((b2 <= b0 /\ b0 < e2) \/ (b0 <=b2 /\ b2 < e0)) ->
  minAddress <= b1 < e1 -> minAddress <= b2 < e2 ->
  r1 <> 0 ->
  r2 <> 0 ->
  ( l1 < b \/ l1 >= e ) ->
  ( l2 < b \/ l2 >= e ) ->
  RI' ri = 0 ->
  (forall l a,
    l < b \/ l >= e -> l <> loc ->
    accessMemMeta M MM l = a -> accessMemMeta M' MM' l = a
    ) ->
  (forall r0, r0 <> ri -> RI r0 = RI' r0) ->
  l1 <> loc ->
  l2 <> loc ->
  removeAllocMemBlock AMB b b0 = Some e0 ->
  ((r1 <> r2 -> RI' ri1 <> r1 \/ RI' ri2 <> r2) /\
      (r1 = r2 -> ri1 = ri2)).

Lemma free__wfE__wfUniqRentryH_case : forall loc l1 v1 b1 e1 r1 ri1 l2 v2 b2 e2 r2 ri2 M MM AMB M' MM' G' S' RI rev' RI' ri b e,
  wfEnv (MkEnv M MM AMB G' S' RI rev') ->
  (forall l v b e r ri,
    accessMemMeta M MM l = Some (v, (b, e, r, ri)) ->
    wfUniqRentryH (MkEnv M MM AMB G' S' RI rev') b e r ri ) ->
  accessMemMeta M' MM' l1 = Some (v1, (b1, e1, r1, ri1)) ->
  accessMemMeta M' MM' l2 = Some (v2, (b2, e2, r2, ri2)) ->
  minAddress <= b1 < e1 -> minAddress <= b2 < e2 ->
  r1 <> 0 ->
  ( l1 < b \/ l1 >= e ) ->
  ( l2 < b \/ l2 >= e ) ->
  RI' ri = 0 ->
  (forall l a,
    l < b \/ l >= e -> l <> loc ->
    accessMemMeta M MM l = a -> accessMemMeta M' MM' l = a
    ) ->
  (forall r0, r0 <> ri -> RI r0 = RI' r0) ->
  l1 <> loc ->
  l2 <> loc ->
  r1 = r2 -> ri1 = ri2.

Lemma free__wfFrame: forall M MM AMB G' F S' RI rev' M' MM' AMB' RI' loc,
  wfEnv (MkEnv M MM AMB G' S' RI rev') ->
  wfFrms rev' S' ->
  wfFrame M RI F ->
  In F (frames S') ->
  free (MkEnv M MM AMB G' S' RI rev') loc =
    Some (MkEnv M' MM' AMB' G' S' RI' rev') ->
  wfFrame M' RI' F.

Lemma free__wfStack: forall M MM AMB G' S' RI rev' M' MM' AMB' RI' loc,
  wfEnv (MkEnv M MM AMB G' S' RI rev') ->
  wfStack M RI rev' S' ->
  free (MkEnv M MM AMB G' S' RI rev') loc = Some (MkEnv M' MM' AMB' G' S' RI' rev') ->
  wfStack M' RI' rev' S'.

Lemma free__wfMem: forall E E' loc,
  wfEnv E ->
  free E loc = Some E' ->
  wfMem (mem E') (mmeta E') (revInfo E') (rev E').

Lemma free__wfE: forall E E' loc,
  wfEnv E ->
  free E loc = Some E' ->
  wfEnv E'.

createFrame preserves well-formed Envs.


Lemma createFrame__validAddress: forall M MM AMB G S RI rev M' MM' AMB' G' S' RI' rev' l,
  validAddress M l ->
  createFrame (MkEnv M MM AMB G S RI rev) (Stack2frame S') = Some (MkEnv M' MM' AMB' G' S' RI' rev') ->
  validAddress M' l.

Lemma createFrame__wfFrame: forall M MM AMB G' F RI rev M' MM' AMB' RI' ri S S',
  wfFrame M RI F ->
  In F (frames S') ->
  createFrame (MkEnv M MM AMB G' S RI rev) (Stack2frame S') =
     Some (MkEnv M' MM' AMB' G' S' RI' (RI' ri+1)) ->
  wfFrame M' RI' F.

Lemma createFrame__wfFrms: forall E E' f,
  wfFrms E.(rev) E.(stack) ->
  createFrame E f = Some E' ->
  wfFrms E'.(rev) E'.(stack).

Lemma createFrame__wfStack: forall M MM AMB S G' S' RI rev M' MM' AMB' RI' ri,
  wfStack M RI rev S ->
  rev >= 2 ->
  createFrame (MkEnv M MM AMB G' S RI rev) (Stack2frame S') = Some (MkEnv M' MM' AMB' G' S' RI' (RI' ri+1)) ->
  wfStack M' RI' (RI' ri+1) S'.

Lemma createFrame__wfE__wfOverlapped_case : forall F l1 v1 b1 e1 r1 ri1 l2 v2 b2 e2 r2 ri2 M MM AMB M' MM' G' S' RI rev RI' ri S,
  wfEnv (MkEnv M MM AMB G' S RI rev) ->
  (forall l v b e r ri,
    accessMemMeta M MM l = Some (v, (b, e, r, ri)) ->
    wfOverlapped (MkEnv M MM AMB G' S' RI rev) b e r ri) ->
  accessMemMeta M' MM' l1 = Some (v1, (b1, e1, r1, ri1)) ->
  accessMemMeta M' MM' l2 = Some (v2, (b2, e2, r2, ri2)) ->
 ((b1 <= b2 /\ b2 < e1) \/ (b2 <=b1 /\ b1 < e2)) ->
  minAddress <= b1 < e1 -> minAddress <= b2 < e2 ->
  r1 <> 0 ->
  r2 <> 0 ->
  ( l1 < from F \/ l1 >= to F ) ->
  ( l2 < from F \/ l2 >= to F ) ->
  RI' ri = rev ->
  (forall l v,
    accessMemMeta M MM l = Some v -> accessMemMeta M' MM' l = Some v
  ) ->
  (forall l,
    l < from F \/ l >= to F ->
    accessMemMeta M MM l = None -> accessMemMeta M' MM' l = None
    ) ->
  (forall r0, r0 <> ri -> RI r0 = RI' r0) ->
  head (frames S') = Some F ->
  ((r1 <> r2 -> RI' ri1 <> r1 \/ RI' ri2 <> r2) /\
      (r1 = r2 -> ri1 = ri2)).

Lemma createFrame__wfE__wfOverlappedAMB_case : forall b0 e0 F l1 v1 b1 e1 r1 ri1 l2 v2 b2 e2 r2 ri2 M MM AMB M' MM' G' S' RI rev RI' ri S,
  wfEnv (MkEnv M MM AMB G' S RI rev) ->
  (forall l v b e r ri,
    accessMemMeta M MM l = Some (v, (b, e, r, ri)) ->
    wfOverlappedAMB (MkEnv M MM AMB G' S' RI rev) b e r ri) ->
  accessMemMeta M' MM' l1 = Some (v1, (b1, e1, r1, ri1)) ->
  accessMemMeta M' MM' l2 = Some (v2, (b2, e2, r2, ri2)) ->
 ((b1 <= b0 /\ b0 < e1) \/ (b0 <=b1 /\ b1 < e0)) ->
 ((b2 <= b0 /\ b0 < e2) \/ (b0 <=b2 /\ b2 < e0)) ->
  minAddress <= b1 < e1 -> minAddress <= b2 < e2 ->
  r1 <> 0 ->
  r2 <> 0 ->
  ( l1 < from F \/ l1 >= to F ) ->
  ( l2 < from F \/ l2 >= to F ) ->
  RI' ri = rev ->
  (forall l v,
    accessMemMeta M MM l = Some v -> accessMemMeta M' MM' l = Some v
  ) ->
  (forall l,
    l < from F \/ l >= to F ->
    accessMemMeta M MM l = None -> accessMemMeta M' MM' l = None
    ) ->
  (forall r0, r0 <> ri -> RI r0 = RI' r0) ->
  head (frames S') = Some F ->
  AMB b0 = Some e0 ->
  ((r1 <> r2 -> RI' ri1 <> r1 \/ RI' ri2 <> r2) /\
      (r1 = r2 -> ri1 = ri2)).

Lemma createFrame__wfE__wfUniqRentryH_case : forall F l1 v1 b1 e1 r1 ri1 l2 v2 b2 e2 r2 ri2 M MM AMB M' MM' G' S' RI rev S,
  wfEnv (MkEnv M MM AMB G' S RI rev) ->
  (forall l v b e r ri,
    accessMemMeta M MM l = Some (v, (b, e, r, ri)) ->
    wfUniqRentryH (MkEnv M MM AMB G' S' RI rev) b e r ri) ->
  accessMemMeta M' MM' l1 = Some (v1, (b1, e1, r1, ri1)) ->
  accessMemMeta M' MM' l2 = Some (v2, (b2, e2, r2, ri2)) ->
  minAddress <= b1 < e1 -> minAddress <= b2 < e2 ->
  r1 <> 0 ->
  ( l1 < from F \/ l1 >= to F ) ->
  ( l2 < from F \/ l2 >= to F ) ->
  (forall l v,
    accessMemMeta M MM l = Some v -> accessMemMeta M' MM' l = Some v
  ) ->
  (forall l,
    l < from F \/ l >= to F ->
    accessMemMeta M MM l = None -> accessMemMeta M' MM' l = None
    ) ->
  head (frames S') = Some F ->
  r1 = r2 -> ri1 = ri2.

Lemma createFrame__wfMem : forall E f E',
  wfEnv E ->
  createFrame E f = Some E' ->
  wfMem (mem E') (mmeta E') (revInfo E') (rev E').

Lemma createFrame__wfE : forall E f E',
  wfEnv E ->
  createFrame E f = Some E' ->
  wfEnv E'.

destroyFrame preserves well-formed Envs.


Lemma destroyFrame__wfFrame: forall M MM AMB G' f RI rev M' MM' AMB' RI' S S',
  wfFrms rev S ->
  wfFrame M RI f ->
  In f (frames S') ->
  destroyFrame (MkEnv M MM AMB G' S RI rev) =
    Some (MkEnv M' MM' AMB' G' S' RI' rev) ->
  wfFrame M' RI' f.

Lemma destroyFrame__wfFrms: forall E E',
  wfFrms E.(rev) E.(stack) ->
  destroyFrame E = Some E' ->
  wfFrms E'.(rev) E'.(stack).

Lemma destroyFrame__wfStack: forall M MM AMB S G' S' RI rev' M' MM' AMB' RI',
  wfStack M RI rev' S ->
  destroyFrame (MkEnv M MM AMB G' S RI rev') = Some (MkEnv M' MM' AMB' G' S' RI' rev') ->
  wfStack M' RI' rev' S'.

Lemma accessMemMeta_unchanged_destroyFrame : forall M MM M' MM' l b e a,
  (forall l a, l < b \/ l >= e ->accessMemMeta M MM l = a -> accessMemMeta M' MM' l = a) ->
  accessMemMeta M' MM' l = a ->
  l < b \/ l >= e ->
  accessMemMeta M MM l = a.

Lemma destroyFrame__wfE__wfOverlapped_case : forall l1 v1 b1 e1 r1 ri1 l2 v2 b2 e2 r2 ri2 M MM AMB M' MM' G' S RI rev' RI' ri b e,
  wfEnv (MkEnv M MM AMB G' S RI rev') ->
  (forall l v b e r ri,
    accessMemMeta M MM l = Some (v, (b, e, r, ri)) ->
    wfOverlapped (MkEnv M MM AMB G' S RI rev') b e r ri) ->
  accessMemMeta M' MM' l1 = Some (v1, (b1, e1, r1, ri1)) ->
  accessMemMeta M' MM' l2 = Some (v2, (b2, e2, r2, ri2)) ->
 ((b1 <= b2 /\ b2 < e1) \/ (b2 <=b1 /\ b1 < e2)) ->
  minAddress <= b1 < e1 -> minAddress <= b2 < e2 ->
  r1 <> 0 ->
  r2 <> 0 ->
  ( l1 < b \/ l1 >= e ) ->
  ( l2 < b \/ l2 >= e ) ->
  RI' ri = 0 ->
  (forall l a,
    l < b \/ l >= e ->
    accessMemMeta M MM l = a -> accessMemMeta M' MM' l = a
    ) ->
  (forall r0, r0 <> ri -> RI r0 = RI' r0) ->
  ((r1 <> r2 -> RI' ri1 <> r1 \/ RI' ri2 <> r2) /\
      (r1 = r2 -> ri1 = ri2)).

Lemma destroyFrame__wfE__wfOverlappedAMB_case : forall b0 e0 l1 v1 b1 e1 r1 ri1 l2 v2 b2 e2 r2 ri2 M MM AMB M' MM' G' S RI rev' RI' ri b e,
  wfEnv (MkEnv M MM AMB G' S RI rev') ->
  (forall l v b e r ri,
    accessMemMeta M MM l = Some (v, (b, e, r, ri)) ->
    wfOverlappedAMB (MkEnv M MM AMB G' S RI rev') b e r ri) ->
  accessMemMeta M' MM' l1 = Some (v1, (b1, e1, r1, ri1)) ->
  accessMemMeta M' MM' l2 = Some (v2, (b2, e2, r2, ri2)) ->
 ((b1 <= b0 /\ b0 < e1) \/ (b0 <=b1 /\ b1 < e0)) ->
 ((b2 <= b0 /\ b0 < e2) \/ (b0 <=b2 /\ b2 < e0)) ->
  minAddress <= b1 < e1 -> minAddress <= b2 < e2 ->
  r1 <> 0 ->
  r2 <> 0 ->
  ( l1 < b \/ l1 >= e ) ->
  ( l2 < b \/ l2 >= e ) ->
  RI' ri = 0 ->
  (forall l a,
    l < b \/ l >= e ->
    accessMemMeta M MM l = a -> accessMemMeta M' MM' l = a
    ) ->
  (forall r0, r0 <> ri -> RI r0 = RI' r0) ->
  AMB b0 = Some e0 ->
  ((r1 <> r2 -> RI' ri1 <> r1 \/ RI' ri2 <> r2) /\
      (r1 = r2 -> ri1 = ri2)).

Lemma destroyFrame__wfE__wfUniqRentryH_case : forall l1 v1 b1 e1 r1 ri1 l2 v2 b2 e2 r2 ri2 M MM AMB M' MM' G' S RI rev' RI' ri b e,
  wfEnv (MkEnv M MM AMB G' S RI rev') ->
  (forall l v b e r ri,
    accessMemMeta M MM l = Some (v, (b, e, r, ri)) ->
    wfUniqRentryH (MkEnv M MM AMB G' S RI rev') b e r ri) ->
  accessMemMeta M' MM' l1 = Some (v1, (b1, e1, r1, ri1)) ->
  accessMemMeta M' MM' l2 = Some (v2, (b2, e2, r2, ri2)) ->
  minAddress <= b1 < e1 -> minAddress <= b2 < e2 ->
  r1 <> 0 ->
  ( l1 < b \/ l1 >= e ) ->
  ( l2 < b \/ l2 >= e ) ->
  RI' ri = 0 ->
  (forall l a,
    l < b \/ l >= e ->
    accessMemMeta M MM l = a -> accessMemMeta M' MM' l = a
    ) ->
  (forall r0, r0 <> ri -> RI r0 = RI' r0) ->
  r1 = r2 -> ri1 = ri2.

Lemma destroyFrame__wfMem : forall E E',
  wfEnv E ->
  destroyFrame E = Some E' ->
  wfMem (mem E') (mmeta E') (revInfo E') (rev E').

Lemma destroyFrame__wfE : forall E E',
  wfEnv E ->
  destroyFrame E = Some E' ->
  wfEnv E'.