Require Import Zwf.
Require Import Axioms.
Require Import Coqlib.
Require Intv.
Require Import Maps.
Require Archi.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Export Memdata.
Require Export Memtype.
Require Export MemPerm.
Require Export StackADT.

Local Unset Elimination Schemes.
Local Unset Case Analysis Schemes.

Close Scope nat_scope.

Lemma zle_zlt:
  forall lo hi o,
    zle lo o && zlt o hi = true <-> lo <= o < hi.

Section FORALL.

  Variables P: Z -> Prop.
  Variable f: forall (x: Z), {P x} + {~ P x}.
  Variable lo: Z.

  Program Fixpoint forall_rec (hi: Z) {wf (Zwf lo) hi}:
    {forall x, lo <= x < hi -> P x}
    + {~ forall x, lo <= x < hi -> P x} :=
    if zlt lo hi then
      match f (hi - 1) with
      | left _ =>
        match forall_rec (hi - 1) with
        | left _ => left _ _
        | right _ => right _ _
        end
      | right _ => right _ _
      end
    else
      left _ _
  .

End FORALL.


Local Notation "a # b" := (PMap.get b a) (at level 1).

Module Mem.
Export Memtype.Mem.

Definition perm_order' (po: option permission) (p: permission) :=
  match po with
  | Some p' => perm_order p' p
  | None => False
 end.

Definition perm_order'' (po1 po2: option permission) :=
  match po1, po2 with
  | Some p1, Some p2 => perm_order p1 p2
  | _, None => True
  | None, Some _ => False
 end.

Definition in_bounds (o: Z) (bnds: Z*Z) :=
  fst bnds <= o < snd bnds.

Record stack_inv (s: StackADT.stack) (thr: block) (P: perm_type) : Prop :=
  {
    stack_inv_valid': forall b, in_stack_all s b -> Plt b thr;
    stack_inv_norepet: nodup s;
    stack_inv_perms: stack_agree_perms P s;
    stack_inv_below_limit: size_stack s < stack_limit;
    stack_inv_wf: wf_stack P s;
  }.

Lemma stack_inv_valid s thr P (SI: stack_inv s thr P): forall b, in_stack s b -> Plt b thr.

Record mem' : Type := mkmem {
  mem_contents: PMap.t (ZMap.t memval); (* block -> offset -> memval *)
  mem_access: PMap.t (Z -> perm_kind -> option permission);
  nextblock: block;
  access_max:
    forall b ofs, perm_order'' (mem_access#b ofs Max) (mem_access#b ofs Cur);
  nextblock_noaccess:
    forall b ofs k, ~(Plt b nextblock) -> mem_access#b ofs k = None;
  contents_default:
    forall b, fst mem_contents#b = Undef;
  contents_default':
    fst mem_contents = ZMap.init Undef;
  stack:
    StackADT.stack;
  mem_stack_inv:
    stack_inv stack nextblock (fun b o k p => perm_order' ((mem_access#b) o k) p);
  mem_bounds: PMap.t (Z*Z);
  mem_bounds_perm: forall b o k p,
      perm_order' ((mem_access#b) o k) p ->
      in_bounds o (mem_bounds#b);
  }.

Definition mem := mem'.

Lemma mkmem_ext:
  forall cont1 cont2 acc1 acc2 next1 next2
    a1 a2 b1 b2 c1 c2 c1' c2' adt1 adt2 sinv1 sinv2 bnd1 bnd2 bndpf1 bndpf2,
  cont1=cont2 -> acc1=acc2 -> next1=next2 -> adt1 = adt2 -> bnd1 = bnd2 ->
  mkmem cont1 acc1 next1 a1 b1 c1 c1' adt1 sinv1 bnd1 bndpf1 =
  mkmem cont2 acc2 next2 a2 b2 c2 c2' adt2 sinv2 bnd2 bndpf2.

Validity of blocks and accesses

Definition valid_block (m: mem) (b: block) := Plt b (nextblock m).

Theorem valid_not_valid_diff:
  forall m b b', valid_block m b -> ~(valid_block m b') -> b <> b'.

Local Hint Resolve valid_not_valid_diff: mem.


Definition perm (m: mem) (b: block) (ofs: Z) (k: perm_kind) (p: permission) : Prop :=
   perm_order' (m.(mem_access)#b ofs k) p.

Theorem perm_implies:
  forall m b ofs k p1 p2, perm m b ofs k p1 -> perm_order p1 p2 -> perm m b ofs k p2.

Local Hint Resolve perm_implies: mem.

Theorem perm_cur_max:
  forall m b ofs p, perm m b ofs Cur p -> perm m b ofs Max p.

Theorem perm_cur:
  forall m b ofs k p, perm m b ofs Cur p -> perm m b ofs k p.

Theorem perm_max:
  forall m b ofs k p, perm m b ofs k p -> perm m b ofs Max p.

Local Hint Resolve perm_cur perm_max: mem.

Theorem perm_valid_block:
  forall m b ofs k p, perm m b ofs k p -> valid_block m b.

Local Hint Resolve perm_valid_block: mem.

Remark perm_order_dec:
  forall p1 p2, {perm_order p1 p2} + {~perm_order p1 p2}.

Remark perm_order'_dec:
  forall op p, {perm_order' op p} + {~perm_order' op p}.

Theorem perm_dec:
  forall m b ofs k p, {perm m b ofs k p} + {~ perm m b ofs k p}.

Definition range_perm (m: mem) (b: block) (lo hi: Z) (k: perm_kind) (p: permission) : Prop :=
  forall ofs, lo <= ofs < hi -> perm m b ofs k p.

Theorem range_perm_implies:
  forall m b lo hi k p1 p2,
  range_perm m b lo hi k p1 -> perm_order p1 p2 -> range_perm m b lo hi k p2.

Theorem range_perm_cur:
  forall m b lo hi k p,
  range_perm m b lo hi Cur p -> range_perm m b lo hi k p.

Theorem range_perm_max:
  forall m b lo hi k p,
  range_perm m b lo hi k p -> range_perm m b lo hi Max p.

Local Hint Resolve range_perm_implies range_perm_cur range_perm_max: mem.

Lemma range_perm_dec:
  forall m b lo hi k p, {range_perm m b lo hi k p} + {~ range_perm m b lo hi k p}.


Definition valid_access (m: mem) (chunk: memory_chunk) (b: block) (ofs: Z) (p: permission): Prop :=
  range_perm m b ofs (ofs + size_chunk chunk) Cur p
  /\ (align_chunk chunk | ofs)
  /\ (perm_order p Writable -> stack_access (stack m) b ofs (ofs + size_chunk chunk)).

Theorem valid_access_implies:
  forall m chunk b ofs p1 p2,
  valid_access m chunk b ofs p1 -> perm_order p1 p2 ->
  valid_access m chunk b ofs p2.

Theorem valid_access_freeable_any:
  forall m chunk b ofs p,
  valid_access m chunk b ofs Freeable ->
  valid_access m chunk b ofs p.

Local Hint Resolve valid_access_implies: mem.

Theorem valid_access_valid_block:
  forall m chunk b ofs,
  valid_access m chunk b ofs Nonempty ->
  valid_block m b.

Local Hint Resolve valid_access_valid_block: mem.

Lemma valid_access_perm:
  forall m chunk b ofs k p,
  valid_access m chunk b ofs p ->
  perm m b ofs k p.

Lemma valid_access_compat:
  forall m chunk1 chunk2 b ofs p,
  size_chunk chunk1 = size_chunk chunk2 ->
  align_chunk chunk2 <= align_chunk chunk1 ->
  valid_access m chunk1 b ofs p->
  valid_access m chunk2 b ofs p.

Lemma non_writable_private_stack_access_dec : forall p m b ofs chunk,
  {(perm_order p Writable -> stack_access m b ofs (ofs + size_chunk chunk))}
  + {~ (perm_order p Writable -> stack_access m b ofs (ofs + size_chunk chunk))}.

Lemma valid_access_dec:
  forall m chunk b ofs p,
  {valid_access m chunk b ofs p} + {~ valid_access m chunk b ofs p}.

Definition valid_pointer (m: mem) (b: block) (ofs: Z): bool :=
  perm_dec m b ofs Cur Nonempty.

Theorem valid_pointer_nonempty_perm:
  forall m b ofs,
  valid_pointer m b ofs = true <-> perm m b ofs Cur Nonempty.

Theorem valid_pointer_valid_access:
  forall m b ofs,
  valid_pointer m b ofs = true <-> valid_access m Mint8unsigned b ofs Nonempty.


Definition weak_valid_pointer (m: mem) (b: block) (ofs: Z) :=
  valid_pointer m b ofs || valid_pointer m b (ofs - 1).

Lemma weak_valid_pointer_spec:
  forall m b ofs,
  weak_valid_pointer m b ofs = true <->
    valid_pointer m b ofs = true \/ valid_pointer m b (ofs - 1) = true.
Lemma valid_pointer_implies:
  forall m b ofs,
  valid_pointer m b ofs = true -> weak_valid_pointer m b ofs = true.

Operations over memory stores

Lemma stack_perm m:
  stack_agree_perms (perm m) (stack m).

Hint Resolve stack_norepet stack_perm.

Program Definition empty: mem :=
  mkmem (PMap.init (ZMap.init Undef))
        (PMap.init (fun ofs k => None))
        1%positive _ _ _ _ nil _ (PMap.init (0,0)) _.



Lemma stack_valid:
  forall m b, in_stack (stack m) b -> Plt b (nextblock m).

Lemma in_tframes_in_stack_all:
  forall s f a b,
    In f (snd a) ->
    In a s ->
    in_frame f b ->
    in_stack_all s b.

Lemma stack_inv_alloc:
  forall m lo hi,
    stack_inv (stack m) (Pos.succ (nextblock m))
              (fun (b : block) (o : Z) (k : perm_kind) (p : permission) =>
                 perm_order'
                   ((PMap.set (nextblock m) (fun (ofs : Z) (_ : perm_kind) => if zle lo ofs && zlt ofs hi then Some Freeable else None) (mem_access m))
                      # b o k) p).

Program Definition alloc (m: mem) (lo hi: Z) : (mem * block) :=
  (mkmem (PMap.set m.(nextblock)
                   (ZMap.init Undef)
                   m.(mem_contents))
         (PMap.set m.(nextblock)
                   (fun ofs k => if zle lo ofs && zlt ofs hi then Some Freeable else None)
                   m.(mem_access))
         (Psucc m.(nextblock))
         _ _ _ _
         (stack m) _ (PMap.set m.(nextblock) (lo,hi) m.(mem_bounds)) _,
   m.(nextblock)).


Lemma stack_inv_free:
  forall m (P: perm_type),
    (forall b o k p, P b o k p -> perm m b o k p) ->
    stack_inv (stack m) (nextblock m) P.

Program Definition unchecked_free (m: mem) (b: block) (lo hi: Z): mem :=
  mkmem m.(mem_contents)
        (PMap.set b
                (fun ofs k => if zle lo ofs && zlt ofs hi then None else m.(mem_access)#b ofs k)
                m.(mem_access))
        m.(nextblock) _ _ _ _ (stack m) _ m.(mem_bounds) _.

Definition free (m: mem) (b: block) (lo hi: Z): option mem :=
  if range_perm_dec m b lo hi Cur Freeable
  then Some(unchecked_free m b lo hi)
  else None.

Fixpoint free_list (m: mem) (l: list (block * Z * Z)) {struct l}: option mem :=
  match l with
  | nil => Some m
  | (b, lo, hi) :: l' =>
      match free m b lo hi with
      | None => None
      | Some m' => free_list m' l'
      end
  end.



Fixpoint getN (n: nat) (p: Z) (c: ZMap.t memval) {struct n}: list memval :=
  match n with
  | O => nil
  | S n' => ZMap.get p c :: getN n' (p + 1) c
  end.


Definition load (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z): option val :=
  if valid_access_dec m chunk b ofs Readable
  then Some(decode_val chunk (getN (size_chunk_nat chunk) ofs (m.(mem_contents)#b)))
  else None.


Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val :=
  match addr with
  | Vptr b ofs => load chunk m b (Ptrofs.unsigned ofs)
  | _ => None
  end.


Definition loadbytes (m: mem) (b: block) (ofs n: Z): option (list memval) :=
  if range_perm_dec m b ofs (ofs + n) Cur Readable
  then Some (getN (nat_of_Z n) ofs (m.(mem_contents)#b))
  else None.



Definition memval_eq (m1 m2: memval): { m1 = m2 } + { m1 <> m2 }.

Fixpoint setN (vl: list memval) (p: Z) (c: ZMap.t memval) {struct vl}: ZMap.t memval :=
  match vl with
  | nil => c
  | v :: vl' => setN vl' (p + 1) (if memval_eq (ZMap.get p c) v then c else ZMap.set p v c)
  end.

Remark setN_other:
  forall vl c p q,
  (forall r, p <= r < p + Z_of_nat (length vl) -> r <> q) ->
  ZMap.get q (setN vl p c) = ZMap.get q c.

Remark setN_outside:
  forall vl c p q,
  q < p \/ q >= p + Z_of_nat (length vl) ->
  ZMap.get q (setN vl p c) = ZMap.get q c.

Remark getN_setN_same:
  forall vl p c,
  getN (length vl) p (setN vl p c) = vl.

Remark getN_exten:
  forall c1 c2 n p,
  (forall i, p <= i < p + Z_of_nat n -> ZMap.get i c1 = ZMap.get i c2) ->
  getN n p c1 = getN n p c2.

Remark getN_setN_disjoint:
  forall vl q c n p,
  Intv.disjoint (p, p + Z_of_nat n) (q, q + Z_of_nat (length vl)) ->
  getN n p (setN vl q c) = getN n p c.

Remark getN_setN_outside:
  forall vl q c n p,
  p + Z_of_nat n <= q \/ q + Z_of_nat (length vl) <= p ->
  getN n p (setN vl q c) = getN n p c.

Remark setN_default:
  forall vl q c, fst (setN vl q c) = fst c.


Program Definition store (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: val): option mem :=
  if valid_access_dec m chunk b ofs Writable then
    Some (mkmem (PMap.set b
                          (setN (encode_val chunk v) ofs (m.(mem_contents)#b))
                          m.(mem_contents))
                m.(mem_access)
                m.(nextblock)
                _ _ _ _ (stack m) _ m.(mem_bounds) _)
  else
    None.


Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem :=
  match addr with
  | Vptr b ofs => store chunk m b (Ptrofs.unsigned ofs) v
  | _ => None
  end.


Program Definition storebytes (m: mem) (b: block) (ofs: Z) (bytes: list memval) : option mem :=
  if range_perm_dec m b ofs (ofs + Z_of_nat (length bytes)) Cur Writable then
    if stack_access_dec (stack m) b ofs (ofs + Z_of_nat (length bytes)) then
    Some (mkmem
             (PMap.set b (setN bytes ofs (m.(mem_contents)#b)) m.(mem_contents))
             m.(mem_access)
             m.(nextblock)
                 _ _ _ _ (stack m) _ m.(mem_bounds) _)
    else None
  else
    None.


Program Definition drop_perm (m: mem) (b: block) (lo hi: Z) (p: permission): option mem :=
  if range_perm_dec m b lo hi Cur Freeable then
    Some (mkmem m.(mem_contents)
                (PMap.set b
                        (fun ofs k => if zle lo ofs && zlt ofs hi then Some p else m.(mem_access)#b ofs k)
                        m.(mem_access))
                m.(nextblock) _ _ _ _ (stack m) _ m.(mem_bounds) _)
  else None.

Record mem_inj {injperm: InjectPerm} (f: meminj) (g: frameinj) (m1 m2: mem) : Prop :=
  mk_mem_inj {
    mi_perm:
      forall b1 b2 delta ofs k p,
      f b1 = Some(b2, delta) ->
      perm m1 b1 ofs k p ->
      inject_perm_condition p ->
      perm m2 b2 (ofs + delta) k p;
    mi_align:
      forall b1 b2 delta chunk ofs p,
      f b1 = Some(b2, delta) ->
      range_perm m1 b1 ofs (ofs + size_chunk chunk) Max p ->
      (align_chunk chunk | delta);
    mi_memval:
      forall b1 ofs b2 delta,
      f b1 = Some(b2, delta) ->
      perm m1 b1 ofs Cur Readable ->
      memval_inject f (ZMap.get ofs m1.(mem_contents)#b1) (ZMap.get (ofs+delta) m2.(mem_contents)#b2);
    mi_stack_blocks:
      stack_inject f g (perm m1) (stack m1) (stack m2);
  }.

Memory extensions

Record extends' {injperm: InjectPerm} (m1 m2: mem) : Prop :=
  mk_extends {
    mext_next: nextblock m1 = nextblock m2;
    mext_inj: mem_inj inject_id (flat_frameinj (length (stack m1))) m1 m2;
    mext_perm_inv: forall b ofs k p,
      perm m2 b ofs k p ->
      perm m1 b ofs k p \/ ~perm m1 b ofs Max Nonempty;
    mext_length_stack:
      length (stack m2) = length (stack m1);
  }.

Definition extends {injperm: InjectPerm} := extends'.

Memory injections

Definition meminj_no_overlap (f: meminj) (m: mem) : Prop :=
  forall b1 b1' delta1 b2 b2' delta2 ofs1 ofs2,
  b1 <> b2 ->
  f b1 = Some (b1', delta1) ->
  f b2 = Some (b2', delta2) ->
  perm m b1 ofs1 Max Nonempty ->
  perm m b2 ofs2 Max Nonempty ->
  b1' <> b2' \/ ofs1 + delta1 <> ofs2 + delta2.

Record inject' {injperm: InjectPerm} (f: meminj) (g: frameinj) (m1 m2: mem) : Prop :=
  mk_inject {
    mi_inj:
      mem_inj f g m1 m2;
    mi_freeblocks:
      forall b, ~(valid_block m1 b) -> f b = None;
    mi_mappedblocks:
      forall b b' delta, f b = Some(b', delta) -> valid_block m2 b';
    mi_no_overlap:
      meminj_no_overlap f m1;
    mi_representable:
      forall b b' delta,
      f b = Some(b', delta) ->
      delta >= 0
      /\
      forall ofs,
        perm m1 b (Ptrofs.unsigned ofs) Max Nonempty
        \/ perm m1 b (Ptrofs.unsigned ofs - 1) Max Nonempty ->
        0 <= Ptrofs.unsigned ofs + delta <= Ptrofs.max_unsigned;
    mi_perm_inv:
      forall b1 ofs b2 delta k p,
      f b1 = Some(b2, delta) ->
      perm m2 b2 (ofs + delta) k p ->
      perm m1 b1 ofs k p \/ ~perm m1 b1 ofs Max Nonempty
  }.
Definition inject {injperm: InjectPerm} := inject'.

Local Hint Resolve mi_mappedblocks: mem.

Weak Memory injections

    
Record weak_inject {injperm: InjectPerm} (f: meminj) (g: frameinj) (m1 m2: mem) : Prop :=
  mk_weak_inject {
    mwi_inj:
      mem_inj f g m1 m2;
    mwi_mappedblocks:
      forall b b' delta, f b = Some(b', delta) -> valid_block m2 b';
    mwi_no_overlap:
      meminj_no_overlap f m1;
    mwi_representable:
      forall b b' delta,
      f b = Some(b', delta) ->
      delta >= 0
      /\
      forall ofs,
        perm m1 b (Ptrofs.unsigned ofs) Max Nonempty
        \/ perm m1 b (Ptrofs.unsigned ofs - 1) Max Nonempty ->
        0 <= Ptrofs.unsigned ofs + delta <= Ptrofs.max_unsigned;
    mwi_perm_inv:
      forall b1 ofs b2 delta k p,
      f b1 = Some(b2, delta) ->
      perm m2 b2 (ofs + delta) k p ->
      perm m1 b1 ofs k p \/ ~perm m1 b1 ofs Max Nonempty
  }.



Definition locset := block -> Z -> Prop.

Record magree' {injperm: InjectPerm} (m1 m2: mem) (P: locset) : Prop := mk_magree {
  ma_perm:
    forall b ofs k p,
      perm m1 b ofs k p -> inject_perm_condition p -> perm m2 b ofs k p;
  ma_perm_inv:
    forall b ofs k p,
      perm m2 b ofs k p -> perm m1 b ofs k p \/ ~ perm m1 b ofs Max Nonempty;
  ma_memval:
    forall b ofs,
    perm m1 b ofs Cur Readable ->
    P b ofs ->
    memval_lessdef (ZMap.get ofs (PMap.get b (mem_contents m1)))
                   (ZMap.get ofs (PMap.get b (mem_contents m2)));
  ma_nextblock:
    nextblock m2 = nextblock m1;
  ma_stack:
    stack_inject inject_id (flat_frameinj (length (stack m1))) (perm m1) (stack m1) (stack m2);
  ma_length_stack:
    length (stack m2) = length (stack m1);
}.

Definition magree {injperm: InjectPerm} := magree'.


Definition flat_inj (thr: block) : meminj :=
  fun (b: block) => if plt b thr then Some(b, 0) else None.

Definition inject_neutral {injperm: InjectPerm} (thr: block) (m: mem) :=
  mem_inj (flat_inj thr) (flat_frameinj (length (stack m))) m m.

Record unchanged_on' (P: block -> Z -> Prop) (m_before m_after: mem) : Prop := mk_unchanged_on {
  unchanged_on_nextblock:
    Ple (nextblock m_before) (nextblock m_after);
  unchanged_on_perm:
    forall b ofs k p,
    P b ofs -> valid_block m_before b ->
    (perm m_before b ofs k p <-> perm m_after b ofs k p);
  unchanged_on_contents:
    forall b ofs,
    P b ofs -> perm m_before b ofs Cur Readable ->
    ZMap.get ofs (PMap.get b m_after.(mem_contents)) =
    ZMap.get ofs (PMap.get b m_before.(mem_contents));
}.

Definition unchanged_on := unchanged_on'.

Definition valid_frame f m :=
  forall b, in_frame f b -> valid_block m b.

Definition valid_block_dec m b: { valid_block m b } + { ~ valid_block m b }.

Definition valid_block_dec_eq m b: { forall b0, b0 = b -> valid_block m b0 } + { ~ (forall b0, b0 = b -> valid_block m b0) }.

Definition valid_block_list_dec m l: { forall b, In b l -> valid_block m b } + { ~ (forall b, In b l -> valid_block m b) }.

Definition valid_frame_dec f m: { valid_frame f m } + { ~ valid_frame f m }.

Definition sumbool_not {A} (x: {A} + {~A}): {~A} + {~ (~A)}.

Definition in_bounds_inside (orng: option (Z*Z)) (z1 z2: Z) : Prop :=
  match orng with
    Some (lo, hi) => lo <= z1 /\ z2 <= hi
  | None => True
  end.

Lemma in_bounds_inside_dec:
  forall (o: option Z) (p: Z * Z),
    { in_bounds_inside (option_map (fun x => (0,x)) o) (fst p) (snd p) } + { ~ in_bounds_inside (option_map (fun x => (0,x)) o) (fst p) (snd p) }.

Definition eq_bounds (orng: option (Z*Z)) (z1 z2: Z) : Prop :=
  match orng with
    Some (lo, hi) => lo = z1 /\ z2 = hi
  | None => True
  end.

Lemma eq_bounds_dec:
  forall (o: option Z) (p: Z * Z),
    { eq_bounds (option_map (fun x => (0,x)) o) (fst p) (snd p) } + { ~ eq_bounds (option_map (fun x => (0,x)) o) (fst p) (snd p) }.

Definition prepend_to_current_stage a (l: StackADT.stack) : option StackADT.stack :=
  match l with
  | (None,b)::r => Some ((Some a,b)::r)
  | _ => None
  end.

Lemma valid_frames_add:
  forall s f thr,
    (forall b, in_stack s b -> Plt b thr) ->
    (forall b, in_frames f b -> Plt b thr) ->
    forall b : block, in_stack (f :: s) b -> Plt b thr.

Lemma valid_frame_add:
  forall s f thr s',
    (forall b, in_stack s b -> Plt b thr) ->
    (forall b, in_frame f b -> Plt b thr) ->
    prepend_to_current_stage f s = Some s' ->
    forall b : block, in_stack s' b -> Plt b thr.

Lemma frame_agree_perms_add:
  forall (f: frame_adt) (s: StackADT.stack) s' m,
    stack_agree_perms
      (fun (b : block) (o : Z) (k : perm_kind) (p : permission) => perm_order' ((mem_access m) # b o k) p)
      s ->
    (Forall (fun b =>
                forall o k p,
                  Mem.perm m (fst b) o k p ->
                  0 <= o < frame_size (snd b))%Z (frame_adt_blocks f)) ->
    prepend_to_current_stage f s = Some s' ->
    stack_agree_perms
      (fun (b : block) (o : Z) (k : perm_kind) (p : permission) => perm_order' ((mem_access m) # b o k) p)
      s'.

Lemma size_stack_add:
  forall f s
    (SZ: (size_stack s + size_frames f < stack_limit)%Z),
    size_stack (f :: s) < stack_limit.

Lemma nodup_add:
  forall f s s',
    nodup s ->
    Forall (fun x => ~ in_stack s x) (map fst (frame_adt_blocks f)) ->
    prepend_to_current_stage f s = Some s' ->
    nodup s'.

Definition mem_stack_wf_plus f m s':
  prepend_to_current_stage f (stack m) = Some s' ->
  wf_stack (perm m) s' .

Lemma mem_stack_inv_plus f m s':
  valid_frame f m ->
  (forall b, in_frame f b -> ~ in_stack (stack m) b) ->
  frame_agree_perms (perm m) f ->
  size_stack (tl (stack m)) + align (frame_adt_size f) 8 < stack_limit ->
  prepend_to_current_stage f (stack m) = Some s' ->
  stack_inv s' (nextblock m) (perm m).

Definition frame_agree_perms_forall (P: block -> Z -> perm_kind -> permission -> Prop) f :=
  Forall (fun bfi =>
            let '(b,fi) := bfi in
            forall o k p,
              P b o k p -> 0 <= o < frame_size fi
         )(frame_adt_blocks f).

Lemma frame_agree_perms_rew:
  forall P f,
    frame_agree_perms P f <-> frame_agree_perms_forall P f.


Definition dec (P: Prop) := {P} + {~ P}.

Lemma dec_eq:
  forall (P Q: Prop) (EQ: P <-> Q), dec P -> dec Q.

Lemma dec_impl:
  forall (A: Type) (P Q R: A -> Prop)
    (IMPL: forall x, P x -> Q x)
    (DECR: dec (forall x, Q x -> P x -> R x)),
    dec (forall x, P x -> R x).

Definition zle_zlt_dec:
  forall (a b c: Z), {a <= b < c} + { ~ a <= b < c }.

Lemma perm_impl_prop_dec m b (P: Z -> Prop) (Pdec: forall o, dec (P o)):
  dec (forall o k p, perm m b o k p -> P o).

Definition frame_agree_perms_forall_dec m f:
  {frame_agree_perms_forall (perm m) f} + { ~ frame_agree_perms_forall (perm m) f}.

Definition frame_agree_perms_dec m f:
  {frame_agree_perms (perm m) f} + { ~ frame_agree_perms (perm m) f}.

Definition top_tframe_prop_dec (P: tframe_adt -> Prop) (Pdec: forall t, {P t} + { ~ P t}):
  forall s, { top_tframe_prop P s } + { ~ top_tframe_prop P s }.

Definition dec_true_impl:
  forall (P Q: Prop),
    P ->
    dec Q ->
    dec (P -> Q).

Program Definition record_stack_blocks (m: mem) (f: frame_adt) : option mem :=
  if valid_frame_dec f m
  then if (Forall_dec _ (fun x => sumbool_not (in_stack_dec (stack m) (fst x))) (frame_adt_blocks f))
       then if (zlt (size_stack (tl (stack m)) + align (Z.max 0 (frame_adt_size f)) 8) stack_limit)
            then if frame_agree_perms_forall_dec m f
                 then
                   match prepend_to_current_stage f (stack m) with
                   | Some s =>
                     Some
                       (mkmem (mem_contents m)
                              (mem_access m)
                              (nextblock m)
                              (access_max m)
                              (nextblock_noaccess m)
                              (contents_default m)
                              (contents_default' m)
                              s
                              _
                              (mem_bounds m)
                              (mem_bounds_perm m))
                   | _ => None
                   end
                 else None
            else None
       else None
  else None.

Program Definition push_new_stage (m: mem) : mem :=
  (mkmem (mem_contents m)
         (mem_access m)
         (nextblock m)
         (access_max m)
         (nextblock_noaccess m)
         (contents_default m)
         (contents_default' m)
         ((None,nil)::stack m)
         _
         (mem_bounds m)
         (mem_bounds_perm m)).


Lemma destr_dep_let:
  forall {A1 A2 B: Type} (a: A1*A2) (bres: B) (T: forall m b (p: (m,b) = a), option B),
    (let (m,b) as ano return (ano = a -> option B) := a in
     fun Heq : (m,b) = a => T _ _ Heq) eq_refl = Some bres ->
    forall (P: B -> Prop),
      (forall m b (pf: (m, b) = a) x, T _ _ pf = Some x -> P x) ->
      P bres.

Lemma destr_dep_match:
  forall {A B: Type} (a: option A) (x: B)
    (T: forall x (pf: Some x = a), B)
    (MATCH: match a as ano return (ano = a -> option B) with
            | Some m1 => fun Heq: Some m1 = a => Some (T _ Heq)
            | None => fun Heq => None
            end eq_refl = Some x) ,
  forall P: B -> Prop,
    (forall m (pf: Some m = a) x, T m pf = x -> P x) ->
    P x.

Lemma constr_let:
  forall {A1 A2 B: Type} (a: A1 * A2)
    m b (EQ: a = (m,b))
    (T: forall m b (pf: (m,b) = a), option B)
    X
    (EQ: T _ _ (eq_sym EQ) = Some X),
    (let (m0,b0) as ano return (ano = a -> option B) := a in
     fun Heq : (m0,b0) = a => T m0 b0 Heq) eq_refl = Some X.

Lemma constr_match:
  forall {A B: Type} (a: option A)
    x (EQ: a = Some x)
    (T: forall x (pf: Some x = a), option B)
    X
    (EQ: T _ (eq_sym EQ) = Some X),
    (match a as ano return (ano = a -> option B) with
       Some m1 =>
       fun Heq : Some m1 = a => T m1 Heq
     | None => fun _ => None
     end) eq_refl = Some X.


Definition stage_tailcallable (tf: tframe_adt) (m: mem) : Prop :=
  match fst tf with
    None => True
  | Some f => forall b o k p, in_frame f b -> ~ Mem.perm m b o k p
  end.

Definition stage_tailcallable_dec m tf : { stage_tailcallable tf m } + { ~ stage_tailcallable tf m }.

Definition top_frame_no_perm m :=
  top_tframe_prop
    (fun tf =>
       forall b,
         in_frames tf b ->
         forall o k p,
           ~ perm m b o k p) (stack m).

Definition top_frame_no_perm_dec m2: { top_frame_no_perm m2 } + { ~ top_frame_no_perm m2}.

Definition tailcall_stage_stack (m: mem) : option StackADT.stack :=
  if top_frame_no_perm_dec m
  then Some ((None, opt_cons (fst (hd (None,nil) (stack m))) (snd (hd (None,nil) (stack m))))::tl (stack m))
  else None.

Lemma in_stack_all_tailcall_stage_stack:
  forall m s' b,
    tailcall_stage_stack m = Some s' ->
    in_stack_all s' b ->
    in_stack_all (stack m) b.

Program Definition tailcall_stage (m: mem) : option mem :=
  match tailcall_stage_stack m with
  | None => None
  | Some s' => Some (mkmem (mem_contents m)
                          (mem_access m)
                          (nextblock m)
                          (access_max m)
                          (nextblock_noaccess m)
                          (contents_default m)
                          (contents_default' m)
                          s'
                          _
                          (mem_bounds m)
                          (mem_bounds_perm m))
  end.

Lemma alloc_stack:
  forall m1 m2 lo hi b,
    alloc m1 lo hi = (m2,b) ->
    stack m2 = stack m1.

Lemma mem_stack_inv_tl:
  forall m, stack_inv (tl (stack m)) (nextblock m) (perm m).

Definition unrecord_stack_block (m: mem) : option mem :=
  match stack m with
    nil => None
  | a::r => Some ((mkmem (mem_contents m)
                        (mem_access m)
                        (nextblock m)
                        (access_max m)
                        (nextblock_noaccess m)
                        (contents_default m)
                        (contents_default' m)
                        (tl (stack m))
                        (mem_stack_inv_tl _)
                        (mem_bounds m)
                        (mem_bounds_perm m)
                ))
  end.

Ltac unfold_unrecord' H m :=
  unfold unrecord_stack_block in H;
  let A := fresh in
  case_eq (stack m); [
    intro A
  | intros ? ? A
  ]; setoid_rewrite A in H; inv H.
Ltac unfold_unrecord :=
  match goal with
    H: unrecord_stack_block ?m = _ |- _ => unfold_unrecord' H m
  end.

Local Instance memory_model_ops :
  MemoryModelOps mem.

Section WITHINJPERM.
Context {injperm: InjectPerm}.

Properties of the memory operations

Theorem nextblock_empty: nextblock empty = 1%positive.

Theorem perm_empty: forall b ofs k p, ~perm empty b ofs k p.

Theorem valid_access_empty: forall chunk b ofs p, ~valid_access empty chunk b ofs p.

Theorem empty_weak_inject : forall f m,
  stack m = nil ->
  (forall b b' delta, f b = Some(b', delta) -> delta >= 0) ->
  (forall b b' delta, f b = Some(b', delta) -> valid_block m b') ->
  weak_inject f nil Mem.empty m.

Theorem weak_inject_to_inject : forall f g m1 m2,
  weak_inject f g m1 m2 ->
  (forall b p, f b = Some p -> valid_block m1 b) ->
  inject f g m1 m2.

Properties related to load

Theorem valid_access_load:
  forall m chunk b ofs,
  valid_access m chunk b ofs Readable ->
  exists v, load chunk m b ofs = Some v.

Theorem load_valid_access:
  forall m chunk b ofs v,
  load chunk m b ofs = Some v ->
  valid_access m chunk b ofs Readable.

Lemma load_result:
  forall chunk m b ofs v,
  load chunk m b ofs = Some v ->
  v = decode_val chunk (getN (size_chunk_nat chunk) ofs (m.(mem_contents)#b)).

Local Hint Resolve load_valid_access valid_access_load: mem.

Theorem load_type:
  forall m chunk b ofs v,
  load chunk m b ofs = Some v ->
  Val.has_type v (type_of_chunk chunk).

Theorem load_cast:
  forall m chunk b ofs v,
  load chunk m b ofs = Some v ->
  match chunk with
  | Mint8signed => v = Val.sign_ext 8 v
  | Mint8unsigned => v = Val.zero_ext 8 v
  | Mint16signed => v = Val.sign_ext 16 v
  | Mint16unsigned => v = Val.zero_ext 16 v
  | _ => True
  end.

Theorem load_int8_signed_unsigned:
  forall m b ofs,
  load Mint8signed m b ofs = option_map (Val.sign_ext 8) (load Mint8unsigned m b ofs).

Theorem load_int16_signed_unsigned:
  forall m b ofs,
  load Mint16signed m b ofs = option_map (Val.sign_ext 16) (load Mint16unsigned m b ofs).

Properties related to loadbytes

Theorem range_perm_loadbytes:
  forall m b ofs len,
  range_perm m b ofs (ofs + len) Cur Readable ->
  exists bytes, loadbytes m b ofs len = Some bytes.

Theorem loadbytes_range_perm:
  forall m b ofs len bytes,
  loadbytes m b ofs len = Some bytes ->
  range_perm m b ofs (ofs + len) Cur Readable.

Theorem loadbytes_load:
  forall chunk m b ofs bytes,
  loadbytes m b ofs (size_chunk chunk) = Some bytes ->
  (align_chunk chunk | ofs) ->
  load chunk m b ofs = Some(decode_val chunk bytes).

Theorem load_loadbytes:
  forall chunk m b ofs v,
  load chunk m b ofs = Some v ->
  exists bytes, loadbytes m b ofs (size_chunk chunk) = Some bytes
             /\ v = decode_val chunk bytes.

Lemma getN_length:
  forall c n p, length (getN n p c) = n.

Theorem loadbytes_length:
  forall m b ofs n bytes,
  loadbytes m b ofs n = Some bytes ->
  length bytes = nat_of_Z n.

Theorem loadbytes_empty:
  forall m b ofs n,
  n <= 0 -> loadbytes m b ofs n = Some nil.

Lemma getN_concat:
  forall c n1 n2 p,
  getN (n1 + n2)%nat p c = getN n1 p c ++ getN n2 (p + Z_of_nat n1) c.

Theorem loadbytes_concat:
  forall m b ofs n1 n2 bytes1 bytes2,
  loadbytes m b ofs n1 = Some bytes1 ->
  loadbytes m b (ofs + n1) n2 = Some bytes2 ->
  n1 >= 0 -> n2 >= 0 ->
  loadbytes m b ofs (n1 + n2) = Some(bytes1 ++ bytes2).

Theorem loadbytes_split:
  forall m b ofs n1 n2 bytes,
  loadbytes m b ofs (n1 + n2) = Some bytes ->
  n1 >= 0 -> n2 >= 0 ->
  exists bytes1, exists bytes2,
     loadbytes m b ofs n1 = Some bytes1
  /\ loadbytes m b (ofs + n1) n2 = Some bytes2
  /\ bytes = bytes1 ++ bytes2.

Theorem load_rep:
 forall ch m1 m2 b ofs v1 v2,
  (forall z, 0 <= z < size_chunk ch -> ZMap.get (ofs + z) m1.(mem_contents)#b = ZMap.get (ofs + z) m2.(mem_contents)#b) ->
  load ch m1 b ofs = Some v1 ->
  load ch m2 b ofs = Some v2 ->
  v1 = v2.

Theorem load_int64_split:
  forall m b ofs v,
  load Mint64 m b ofs = Some v -> Archi.ptr64 = false ->
  exists v1 v2,
     load Mint32 m b ofs = Some (if Archi.big_endian then v1 else v2)
  /\ load Mint32 m b (ofs + 4) = Some (if Archi.big_endian then v2 else v1)
  /\ Val.lessdef v (Val.longofwords v1 v2).

Lemma addressing_int64_split:
  forall i,
  Archi.ptr64 = false ->
  (8 | Ptrofs.unsigned i) ->
  Ptrofs.unsigned (Ptrofs.add i (Ptrofs.of_int (Int.repr 4))) = Ptrofs.unsigned i + 4.

Theorem loadv_int64_split:
  forall m a v,
  loadv Mint64 m a = Some v -> Archi.ptr64 = false ->
  exists v1 v2,
     loadv Mint32 m a = Some (if Archi.big_endian then v1 else v2)
  /\ loadv Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if Archi.big_endian then v2 else v1)
  /\ Val.lessdef v (Val.longofwords v1 v2).

Properties related to store

Theorem valid_access_store' :
  forall m1 chunk b ofs v,
  valid_access m1 chunk b ofs Writable ->
  exists m2: mem, store chunk m1 b ofs v = Some m2 .

Local Hint Resolve valid_access_store': mem.

Theorem valid_access_store:
  forall m1 chunk b ofs v,
  valid_access m1 chunk b ofs Writable ->
  { m2: mem | store chunk m1 b ofs v = Some m2 }.

Local Hint Resolve valid_access_store: mem.

Lemma get_setN_inside:
  forall bytes t o o',
    (o' <= o < o' + Z.of_nat (length bytes))%Z ->
    ZMap.get o (setN bytes o' t) = nth (Z.to_nat (o - o')) bytes Undef.

Lemma zle_zlt_false:
  forall lo hi o,
    zle lo o && zlt o hi = false <-> ~ (lo <= o < hi)%Z.

Lemma get_setN:
  forall bytes t o o',
    ZMap.get o (setN bytes o' t) =
    if zle o' o && zlt o (o' + Z.of_nat (length bytes))
    then nth (Z.to_nat (o - o')) bytes Undef
    else ZMap.get o t.

Lemma nth_getN:
  forall n m o t,
    (n < m)%nat ->
    nth n (getN m o t) Undef = ZMap.get (Z.of_nat n + o) t.

Section STORE.
Variable chunk: memory_chunk.
Variable m1: mem.
Variable b: block.
Variable ofs: Z.
Variable v: val.
Variable m2: mem.
Hypothesis STORE: store chunk m1 b ofs v = Some m2.

Lemma store_access: mem_access m2 = mem_access m1.

Lemma store_mem_contents:
  mem_contents m2 = PMap.set b (setN (encode_val chunk v) ofs m1.(mem_contents)#b) m1.(mem_contents).

Theorem perm_store_1:
  forall b' ofs' k p, perm m1 b' ofs' k p -> perm m2 b' ofs' k p.
 
Theorem perm_store_2:
  forall b' ofs' k p, perm m2 b' ofs' k p -> perm m1 b' ofs' k p.

Local Hint Resolve perm_store_1 perm_store_2: mem.

Theorem nextblock_store:
  nextblock m2 = nextblock m1.

Theorem store_valid_block_1:
  forall b', valid_block m1 b' -> valid_block m2 b'.

Theorem store_valid_block_2:
  forall b', valid_block m2 b' -> valid_block m1 b'.

Local Hint Resolve store_valid_block_1 store_valid_block_2: mem.

Theorem store_stack_access_1: forall b lo hi,
  stack_access (stack m1) b lo hi -> stack_access (stack m2) b lo hi.

Theorem store_stack_access_2: forall b lo hi,
  stack_access (stack m2) b lo hi -> stack_access (stack m1) b lo hi.

Local Hint Resolve store_stack_access_1 store_stack_access_2 : mem.

Theorem store_valid_access_1:
  forall chunk' b' ofs' p,
  valid_access m1 chunk' b' ofs' p -> valid_access m2 chunk' b' ofs' p.

Theorem store_valid_access_2:
  forall chunk' b' ofs' p,
  valid_access m2 chunk' b' ofs' p -> valid_access m1 chunk' b' ofs' p.

Theorem store_valid_access_3:
  valid_access m1 chunk b ofs Writable.

Local Hint Resolve store_valid_access_1 store_valid_access_2 store_valid_access_3: mem.

Theorem load_store_similar:
  forall chunk',
  size_chunk chunk' = size_chunk chunk ->
  align_chunk chunk' <= align_chunk chunk ->
  exists v', load chunk' m2 b ofs = Some v' /\ decode_encode_val v chunk chunk' v'.

Theorem load_store_similar_2:
  forall chunk',
  size_chunk chunk' = size_chunk chunk ->
  align_chunk chunk' <= align_chunk chunk ->
  type_of_chunk chunk' = type_of_chunk chunk ->
  load chunk' m2 b ofs = Some (Val.load_result chunk' v).

Theorem load_store_same:
  load chunk m2 b ofs = Some (Val.load_result chunk v).

Theorem load_store_other:
  forall chunk' b' ofs',
  b' <> b
  \/ ofs' + size_chunk chunk' <= ofs
  \/ ofs + size_chunk chunk <= ofs' ->
  load chunk' m2 b' ofs' = load chunk' m1 b' ofs'.

Theorem loadbytes_store_same:
  loadbytes m2 b ofs (size_chunk chunk) = Some(encode_val chunk v).

Theorem loadbytes_store_other:
  forall b' ofs' n,
  b' <> b
  \/ n <= 0
  \/ ofs' + n <= ofs
  \/ ofs + size_chunk chunk <= ofs' ->
  loadbytes m2 b' ofs' n = loadbytes m1 b' ofs' n.

Lemma setN_in:
  forall vl p q c,
  p <= q < p + Z_of_nat (length vl) ->
  In (ZMap.get q (setN vl p c)) vl.

Lemma getN_in:
  forall c q n p,
  p <= q < p + Z_of_nat n ->
  In (ZMap.get q c) (getN n p c).

End STORE.

Local Hint Resolve perm_store_1 perm_store_2: mem.
Local Hint Resolve store_valid_block_1 store_valid_block_2: mem.
Local Hint Resolve store_valid_access_1 store_valid_access_2
             store_valid_access_3: mem.

Lemma load_store_overlap:
  forall chunk m1 b ofs v m2 chunk' ofs' v',
  store chunk m1 b ofs v = Some m2 ->
  load chunk' m2 b ofs' = Some v' ->
  ofs' + size_chunk chunk' > ofs ->
  ofs + size_chunk chunk > ofs' ->
  exists mv1 mvl mv1' mvl',
      shape_encoding chunk v (mv1 :: mvl)
  /\ shape_decoding chunk' (mv1' :: mvl') v'
  /\ ( (ofs' = ofs /\ mv1' = mv1)
       \/ (ofs' > ofs /\ In mv1' mvl)
       \/ (ofs' < ofs /\ In mv1 mvl')).

Definition compat_pointer_chunks (chunk1 chunk2: memory_chunk) : Prop :=
  match chunk1, chunk2 with
  | (Mint32 | Many32), (Mint32 | Many32) => True
  | (Mint64 | Many64), (Mint64 | Many64) => True
  | _, _ => False
  end.

Lemma compat_pointer_chunks_true:
  forall chunk1 chunk2,
  (chunk1 = Mint32 \/ chunk1 = Many32 \/ chunk1 = Mint64 \/ chunk1 = Many64) ->
  (chunk2 = Mint32 \/ chunk2 = Many32 \/ chunk2 = Mint64 \/ chunk2 = Many64) ->
  quantity_chunk chunk1 = quantity_chunk chunk2 ->
  compat_pointer_chunks chunk1 chunk2.

Theorem load_pointer_store:
  forall chunk m1 b ofs v m2 chunk' b' ofs' v_b v_o,
  store chunk m1 b ofs v = Some m2 ->
  load chunk' m2 b' ofs' = Some(Vptr v_b v_o) ->
  (v = Vptr v_b v_o /\ compat_pointer_chunks chunk chunk' /\ b' = b /\ ofs' = ofs)
  \/ (b' <> b \/ ofs' + size_chunk chunk' <= ofs \/ ofs + size_chunk chunk <= ofs').

Theorem load_store_pointer_overlap:
  forall chunk m1 b ofs v_b v_o m2 chunk' ofs' v,
  store chunk m1 b ofs (Vptr v_b v_o) = Some m2 ->
  load chunk' m2 b ofs' = Some v ->
  ofs' <> ofs ->
  ofs' + size_chunk chunk' > ofs ->
  ofs + size_chunk chunk > ofs' ->
  v = Vundef.

Theorem load_store_pointer_mismatch:
  forall chunk m1 b ofs v_b v_o m2 chunk' v,
  store chunk m1 b ofs (Vptr v_b v_o) = Some m2 ->
  load chunk' m2 b ofs = Some v ->
  ~compat_pointer_chunks chunk chunk' ->
  v = Vundef.

Lemma store_similar_chunks:
  forall chunk1 chunk2 v1 v2 m b ofs,
  encode_val chunk1 v1 = encode_val chunk2 v2 ->
  align_chunk chunk1 = align_chunk chunk2 ->
  store chunk1 m b ofs v1 = store chunk2 m b ofs v2.

Theorem store_signed_unsigned_8:
  forall m b ofs v,
  store Mint8signed m b ofs v = store Mint8unsigned m b ofs v.

Theorem store_signed_unsigned_16:
  forall m b ofs v,
  store Mint16signed m b ofs v = store Mint16unsigned m b ofs v.

Theorem store_int8_zero_ext:
  forall m b ofs n,
  store Mint8unsigned m b ofs (Vint (Int.zero_ext 8 n)) =
  store Mint8unsigned m b ofs (Vint n).

Theorem store_int8_sign_ext:
  forall m b ofs n,
  store Mint8signed m b ofs (Vint (Int.sign_ext 8 n)) =
  store Mint8signed m b ofs (Vint n).

Theorem store_int16_zero_ext:
  forall m b ofs n,
  store Mint16unsigned m b ofs (Vint (Int.zero_ext 16 n)) =
  store Mint16unsigned m b ofs (Vint n).

Theorem store_int16_sign_ext:
  forall m b ofs n,
  store Mint16signed m b ofs (Vint (Int.sign_ext 16 n)) =
  store Mint16signed m b ofs (Vint n).

Properties related to storebytes.

Theorem range_perm_storebytes':
  forall m1 b ofs bytes,
    range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable ->
    stack_access (stack m1) b ofs (ofs + Z_of_nat (length bytes)) ->
  exists m2, storebytes m1 b ofs bytes = Some m2.

Theorem range_perm_storebytes:
  forall m1 b ofs bytes,
  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable ->
  stack_access (stack m1) b ofs (ofs + Z_of_nat (length bytes)) ->
  { m2 : mem | storebytes m1 b ofs bytes = Some m2 }.

Theorem storebytes_store:
  forall m1 b ofs chunk v m2,
  storebytes m1 b ofs (encode_val chunk v) = Some m2 ->
  (align_chunk chunk | ofs) ->
  store chunk m1 b ofs v = Some m2.

Theorem store_storebytes:
  forall m1 b ofs chunk v m2,
  store chunk m1 b ofs v = Some m2 ->
  storebytes m1 b ofs (encode_val chunk v) = Some m2.

Lemma push_storebytes_unrecord:
  forall m b o bytes m1 m2,
    storebytes m b o bytes = Some m1 ->
    storebytes (push_new_stage m) b o bytes = Some m2 ->
    unrecord_stack_block m2 = Some m1.

Section STOREBYTES.
Variable m1: mem.
Variable b: block.
Variable ofs: Z.
Variable bytes: list memval.
Variable m2: mem.
Hypothesis STORE: storebytes m1 b ofs bytes = Some m2.

Lemma storebytes_access: mem_access m2 = mem_access m1.

Lemma storebytes_mem_contents:
  mem_contents m2 = PMap.set b (setN bytes ofs m1.(mem_contents)#b) (m1.(mem_contents)).

Theorem perm_storebytes_1:
  forall b' ofs' k p, perm m1 b' ofs' k p -> perm m2 b' ofs' k p.

Theorem perm_storebytes_2:
  forall b' ofs' k p, perm m2 b' ofs' k p -> perm m1 b' ofs' k p.

Local Hint Resolve perm_storebytes_1 perm_storebytes_2: mem.

Theorem storebytes_stack_access_1: forall b lo hi,
  stack_access (stack m1) b lo hi -> stack_access (stack m2) b lo hi.

Theorem storebytes_stack_access_2: forall b lo hi,
  stack_access (stack m2) b lo hi -> stack_access (stack m1) b lo hi.

Theorem storebytes_stack_access_3:
  stack_access (stack m1) b ofs (ofs + Z.of_nat (length bytes)).

Local Hint Resolve storebytes_stack_access_1
      storebytes_stack_access_2
      storebytes_stack_access_3: mem.

Theorem storebytes_valid_access_1:
  forall chunk' b' ofs' p,
  valid_access m1 chunk' b' ofs' p -> valid_access m2 chunk' b' ofs' p.

Theorem storebytes_valid_access_2:
  forall chunk' b' ofs' p,
  valid_access m2 chunk' b' ofs' p -> valid_access m1 chunk' b' ofs' p.

Local Hint Resolve storebytes_valid_access_1 storebytes_valid_access_2: mem.

Theorem nextblock_storebytes:
  nextblock m2 = nextblock m1.

Theorem storebytes_valid_block_1:
  forall b', valid_block m1 b' -> valid_block m2 b'.

Theorem storebytes_valid_block_2:
  forall b', valid_block m2 b' -> valid_block m1 b'.

Local Hint Resolve storebytes_valid_block_1 storebytes_valid_block_2: mem.

Theorem storebytes_range_perm:
  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable.

Theorem loadbytes_storebytes_same:
  loadbytes m2 b ofs (Z_of_nat (length bytes)) = Some bytes.

Theorem loadbytes_storebytes_disjoint:
  forall b' ofs' len,
  len >= 0 ->
  b' <> b \/ Intv.disjoint (ofs', ofs' + len) (ofs, ofs + Z_of_nat (length bytes)) ->
  loadbytes m2 b' ofs' len = loadbytes m1 b' ofs' len.

Theorem loadbytes_storebytes_other:
  forall b' ofs' len,
  len >= 0 ->
  b' <> b
  \/ ofs' + len <= ofs
  \/ ofs + Z_of_nat (length bytes) <= ofs' ->
  loadbytes m2 b' ofs' len = loadbytes m1 b' ofs' len.

Theorem load_storebytes_other:
  forall chunk b' ofs',
  b' <> b
  \/ ofs' + size_chunk chunk <= ofs
  \/ ofs + Z_of_nat (length bytes) <= ofs' ->
  load chunk m2 b' ofs' = load chunk m1 b' ofs'.

End STOREBYTES.

Lemma push_store_unrecord:
  forall m b o chunk v m1 m2,
    store chunk m b o v = Some m1 ->
    store chunk (push_new_stage m) b o v = Some m2 ->
    unrecord_stack_block m2 = Some m1.

Lemma setN_concat:
  forall bytes1 bytes2 ofs c,
  setN (bytes1 ++ bytes2) ofs c = setN bytes2 (ofs + Z_of_nat (length bytes1)) (setN bytes1 ofs c).

Lemma public_stack_range_concat : forall lo mid hi f,
  public_stack_range lo mid f ->
  public_stack_range mid hi f ->
  public_stack_range lo hi f.

Lemma stack_access_concat : forall m b lo hi mid,
  stack_access m b lo mid ->
  stack_access m b mid hi ->
  stack_access m b lo hi.

Theorem storebytes_concat:
  forall m b ofs bytes1 m1 bytes2 m2,
  storebytes m b ofs bytes1 = Some m1 ->
  storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2 ->
  storebytes m b ofs (bytes1 ++ bytes2) = Some m2.

Lemma storebytes_get_frame_info:
  forall m1 b o v m2,
    storebytes m1 b o v = Some m2 ->
    forall b', get_frame_info (stack m2) b' = get_frame_info (stack m1) b'.

Lemma storebytes_is_stack_top:
  forall m1 b o v m2,
    storebytes m1 b o v = Some m2 ->
    forall b', is_stack_top (stack m2) b' <-> is_stack_top (stack m1) b'.

Lemma storebytes_stack:
  forall m1 b o v m2,
    storebytes m1 b o v = Some m2 ->
    stack m2 = stack m1.

Theorem storebytes_split:
  forall m b ofs bytes1 bytes2 m2,
  storebytes m b ofs (bytes1 ++ bytes2) = Some m2 ->
  exists m1,
     storebytes m b ofs bytes1 = Some m1
  /\ storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2.

Theorem store_int64_split:
  forall m b ofs v m',
  store Mint64 m b ofs v = Some m' -> Archi.ptr64 = false ->
  exists m1,
     store Mint32 m b ofs (if Archi.big_endian then Val.hiword v else Val.loword v) = Some m1
  /\ store Mint32 m1 b (ofs + 4) (if Archi.big_endian then Val.loword v else Val.hiword v) = Some m'.

Theorem storev_int64_split:
  forall m a v m',
  storev Mint64 m a v = Some m' -> Archi.ptr64 = false ->
  exists m1,
     storev Mint32 m a (if Archi.big_endian then Val.hiword v else Val.loword v) = Some m1
  /\ storev Mint32 m1 (Val.add a (Vint (Int.repr 4))) (if Archi.big_endian then Val.loword v else Val.hiword v) = Some m'.

Properties related to alloc.

Section ALLOC.

Variable m1: mem.
Variables lo hi: Z.
Variable m2: mem.
Variable b: block.
Hypothesis ALLOC: alloc m1 lo hi = (m2, b).

Theorem nextblock_alloc:
  nextblock m2 = Psucc (nextblock m1).

Theorem alloc_result:
  b = nextblock m1.

Theorem valid_block_alloc:
  forall b', valid_block m1 b' -> valid_block m2 b'.

Theorem fresh_block_alloc:
  ~(valid_block m1 b).

Theorem valid_new_block:
  valid_block m2 b.

Local Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.

Theorem valid_block_alloc_inv:
  forall b', valid_block m2 b' -> b' = b \/ valid_block m1 b'.

Theorem perm_alloc_1:
  forall b' ofs k p, perm m1 b' ofs k p -> perm m2 b' ofs k p.

Theorem perm_alloc_2:
  forall ofs k, lo <= ofs < hi -> perm m2 b ofs k Freeable.

Theorem perm_alloc_inv:
  forall b' ofs k p,
  perm m2 b' ofs k p ->
  if eq_block b' b then lo <= ofs < hi else perm m1 b' ofs k p.

Theorem perm_alloc_3:
  forall ofs k p, perm m2 b ofs k p -> lo <= ofs < hi.

Theorem perm_alloc_4:
  forall b' ofs k p, perm m2 b' ofs k p -> b' <> b -> perm m1 b' ofs k p.

Local Hint Resolve perm_alloc_1 perm_alloc_2 perm_alloc_3 perm_alloc_4: mem.

Lemma alloc_get_frame_info:
  forall b,
    get_frame_info (stack m2) b = get_frame_info (stack m1) b.

Lemma alloc_is_stack_top:
  forall b,
    is_stack_top (stack m2) b <-> is_stack_top (stack m1) b.



Theorem valid_access_alloc_other:
  forall chunk b' ofs p,
  valid_access m1 chunk b' ofs p ->
  valid_access m2 chunk b' ofs p.

Lemma alloc_get_frame_info_new:
  get_frame_info (stack m2) b = None.

Lemma stack_top_in_frames:
  forall m b,
    is_stack_top (stack m) b -> in_stack (stack m) b.

Lemma stack_top_valid:
  forall m b, is_stack_top (stack m) b -> valid_block m b.

Theorem valid_access_alloc_same:
  forall chunk ofs,
  lo <= ofs -> ofs + size_chunk chunk <= hi -> (align_chunk chunk | ofs) ->
  valid_access m2 chunk b ofs Freeable.

Local Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem.

Theorem valid_access_alloc_inv:
  forall chunk b' ofs p,
  valid_access m2 chunk b' ofs p ->
  if eq_block b' b
  then lo <= ofs /\ ofs + size_chunk chunk <= hi /\ (align_chunk chunk | ofs)
  else valid_access m1 chunk b' ofs p.

Theorem load_alloc_unchanged:
  forall chunk b' ofs,
  valid_block m1 b' ->
  load chunk m2 b' ofs = load chunk m1 b' ofs.

Theorem load_alloc_other:
  forall chunk b' ofs v,
  load chunk m1 b' ofs = Some v ->
  load chunk m2 b' ofs = Some v.

Theorem load_alloc_same:
  forall chunk ofs v,
  load chunk m2 b ofs = Some v ->
  v = Vundef.

Theorem load_alloc_same':
  forall chunk ofs,
  lo <= ofs -> ofs + size_chunk chunk <= hi -> (align_chunk chunk | ofs) ->
  load chunk m2 b ofs = Some Vundef.

Theorem loadbytes_alloc_unchanged:
  forall b' ofs n,
  valid_block m1 b' ->
  loadbytes m2 b' ofs n = loadbytes m1 b' ofs n.

Theorem loadbytes_alloc_same:
  forall n ofs bytes byte,
  loadbytes m2 b ofs n = Some bytes ->
  In byte bytes -> byte = Undef.

End ALLOC.

Local Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.
Local Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem.

Properties related to free.

Theorem range_perm_free':
  forall m1 b lo hi,
  range_perm m1 b lo hi Cur Freeable ->
  exists m2: mem, free m1 b lo hi = Some m2.

Theorem range_perm_free:
  forall m1 b lo hi,
  range_perm m1 b lo hi Cur Freeable ->
  { m2: mem | free m1 b lo hi = Some m2 }.

Section FREE.

Variable m1: mem.
Variable bf: block.
Variables lo hi: Z.
Variable m2: mem.
Hypothesis FREE: free m1 bf lo hi = Some m2.

Theorem free_range_perm:
  range_perm m1 bf lo hi Cur Freeable.

Lemma free_result:
  m2 = unchecked_free m1 bf lo hi.

Theorem nextblock_free:
  nextblock m2 = nextblock m1.

Theorem valid_block_free_1:
  forall b, valid_block m1 b -> valid_block m2 b.

Theorem valid_block_free_2:
  forall b, valid_block m2 b -> valid_block m1 b.

Local Hint Resolve valid_block_free_1 valid_block_free_2: mem.

Theorem perm_free_1:
  forall b ofs k p,
  b <> bf \/ ofs < lo \/ hi <= ofs ->
  perm m1 b ofs k p ->
  perm m2 b ofs k p.

Theorem perm_free_2:
  forall ofs k p, lo <= ofs < hi -> ~ perm m2 bf ofs k p.

Theorem perm_free_3:
  forall b ofs k p,
  perm m2 b ofs k p -> perm m1 b ofs k p.

Theorem perm_free_inv:
  forall b ofs k p,
  perm m1 b ofs k p ->
  (b = bf /\ lo <= ofs < hi) \/ perm m2 b ofs k p.


Lemma free_stack: stack m2 = stack m1.
  
Lemma get_frame_info_free: forall b,
  get_frame_info (stack m1) b = get_frame_info (stack m2) b.

Lemma get_stack_top_blocks_free:
  (get_stack_top_blocks (stack m1)) = (get_stack_top_blocks (stack m2)).
  
Lemma free_is_stack_top: forall b,
  is_stack_top (stack m1) b <-> is_stack_top (stack m2) b.

Lemma free_public_stack_access: forall b lo hi,
  public_stack_access (stack m1) b lo hi <->
  public_stack_access (stack m2) b lo hi.

Lemma free_stack_access: forall b lo hi,
  stack_access (stack m1) b lo hi <->
  stack_access (stack m2) b lo hi.

Theorem valid_access_free_1:
  forall chunk b ofs p,
  valid_access m1 chunk b ofs p ->
  b <> bf \/ lo >= hi \/ ofs + size_chunk chunk <= lo \/ hi <= ofs ->
  valid_access m2 chunk b ofs p.

Theorem valid_access_free_2:
  forall chunk ofs p,
  lo < hi -> ofs + size_chunk chunk > lo -> ofs < hi ->
  ~(valid_access m2 chunk bf ofs p).

Theorem valid_access_free_inv_1:
  forall chunk b ofs p,
  valid_access m2 chunk b ofs p ->
  valid_access m1 chunk b ofs p.

Theorem valid_access_free_inv_2:
  forall chunk ofs p,
  valid_access m2 chunk bf ofs p ->
  lo >= hi \/ ofs + size_chunk chunk <= lo \/ hi <= ofs.

Theorem load_free:
  forall chunk b ofs,
  b <> bf \/ lo >= hi \/ ofs + size_chunk chunk <= lo \/ hi <= ofs ->
  load chunk m2 b ofs = load chunk m1 b ofs.

Theorem load_free_2:
  forall chunk b ofs v,
  load chunk m2 b ofs = Some v -> load chunk m1 b ofs = Some v.

Theorem loadbytes_free:
  forall b ofs n,
  b <> bf \/ lo >= hi \/ ofs + n <= lo \/ hi <= ofs ->
  loadbytes m2 b ofs n = loadbytes m1 b ofs n.

Theorem loadbytes_free_2:
  forall b ofs n bytes,
  loadbytes m2 b ofs n = Some bytes -> loadbytes m1 b ofs n = Some bytes.

End FREE.

Local Hint Resolve valid_block_free_1 valid_block_free_2
             perm_free_1 perm_free_2 perm_free_3
             valid_access_free_1 valid_access_free_inv_1: mem.

Properties related to drop_perm

Theorem range_perm_drop_1:
  forall m b lo hi p m', drop_perm m b lo hi p = Some m' -> range_perm m b lo hi Cur Freeable.

Theorem range_perm_drop_2':
  forall m b lo hi p,
  range_perm m b lo hi Cur Freeable -> exists m', drop_perm m b lo hi p = Some m' .

Theorem range_perm_drop_2:
  forall m b lo hi p,
  range_perm m b lo hi Cur Freeable -> { m' | drop_perm m b lo hi p = Some m' }.


Section DROP.

Variable m: mem.
Variable b: block.
Variable lo hi: Z.
Variable p: permission.
Variable m': mem.
Hypothesis DROP: drop_perm m b lo hi p = Some m'.

Theorem nextblock_drop:
  nextblock m' = nextblock m.

Theorem drop_perm_valid_block_1:
  forall b', valid_block m b' -> valid_block m' b'.

Theorem drop_perm_valid_block_2:
  forall b', valid_block m' b' -> valid_block m b'.

Theorem perm_drop_1:
  forall ofs k, lo <= ofs < hi -> perm m' b ofs k p.

Theorem perm_drop_2:
  forall ofs k p', lo <= ofs < hi -> perm m' b ofs k p' -> perm_order p p'.

Theorem perm_drop_3:
  forall b' ofs k p', b' <> b \/ ofs < lo \/ hi <= ofs -> perm m b' ofs k p' -> perm m' b' ofs k p'.

Theorem perm_drop_4:
  forall b' ofs k p', perm m' b' ofs k p' -> perm m b' ofs k p'.

Lemma drop_stack: stack m' = stack m.
  
Lemma get_frame_info_drop: forall b,
  get_frame_info (stack m) b = get_frame_info (stack m') b.

Lemma get_stack_top_blocks_drop:
  (get_stack_top_blocks (stack m)) = (get_stack_top_blocks (stack m')).
  
Lemma drop_perm_is_stack_top: forall b,
  is_stack_top (stack m) b <-> is_stack_top (stack m') b.

Lemma drop_perm_public_stack_access: forall b lo hi,
  public_stack_access (stack m) b lo hi <->
  public_stack_access (stack m') b lo hi.

Lemma drop_perm_stack_access: forall b lo hi,
  stack_access (stack m) b lo hi <->
  stack_access (stack m') b lo hi.

Lemma valid_access_drop_1:
  forall chunk b' ofs p',
  b' <> b \/ ofs + size_chunk chunk <= lo \/ hi <= ofs \/ perm_order p p' ->
  valid_access m chunk b' ofs p' -> valid_access m' chunk b' ofs p'.

Lemma valid_access_drop_2:
  forall chunk b' ofs p',
  valid_access m' chunk b' ofs p' -> valid_access m chunk b' ofs p'.

Theorem load_drop:
  forall chunk b' ofs,
  b' <> b \/ ofs + size_chunk chunk <= lo \/ hi <= ofs \/ perm_order p Readable ->
  load chunk m' b' ofs = load chunk m b' ofs.

Theorem loadbytes_drop:
  forall b' ofs n,
  b' <> b \/ ofs + n <= lo \/ hi <= ofs \/ perm_order p Readable ->
  loadbytes m' b' ofs n = loadbytes m b' ofs n.

End DROP.

Local Hint Resolve range_perm_drop_1 range_perm_drop_2: mem.
Local Hint Resolve perm_drop_1 perm_drop_2 perm_drop_3 perm_drop_4: mem.
Local Hint Resolve drop_perm_valid_block_1 drop_perm_valid_block_2: mem.
Local Hint Resolve valid_access_drop_1 valid_access_drop_2 : mem.

Generic injections

Lemma perm_inj:
  forall f g m1 m2 b1 ofs k p b2 delta,
  mem_inj f g m1 m2 ->
  perm m1 b1 ofs k p ->
  f b1 = Some(b2, delta) ->
  inject_perm_condition p ->
  perm m2 b2 (ofs + delta) k p.

Lemma range_perm_inj:
  forall f g m1 m2 b1 lo hi k p b2 delta,
  mem_inj f g m1 m2 ->
  range_perm m1 b1 lo hi k p ->
  f b1 = Some(b2, delta) ->
  inject_perm_condition p ->
  range_perm m2 b2 (lo + delta) (hi + delta) k p.


Lemma is_stack_top_inj:
  forall f g m1 m2 b1 b2 delta
    (MINJ: mem_inj f g m1 m2)
    (FB: f b1 = Some (b2, delta))
    (PERM: exists o k p, perm m1 b1 o k p /\ inject_perm_condition p)
    (IST: is_stack_top (stack m1) b1),
    is_stack_top (stack m2) b2.

Lemma is_stack_top_extends:
  forall m1 m2 b
    (MINJ: extends m1 m2)
    (PERM: exists o k p, perm m1 b o k p /\ inject_perm_condition p)
    (IST: is_stack_top (stack m1) b),
    is_stack_top (stack m2) b.

Lemma is_stack_top_inject:
  forall f g m1 m2 b1 b2 delta
    (MINJ: inject f g m1 m2)
    (FB: f b1 = Some (b2, delta))
    (PERM: exists o k p, perm m1 b1 o k p /\ inject_perm_condition p)
    (IST: is_stack_top (stack m1) b1),
    is_stack_top (stack m2) b2.

Lemma get_frame_info_inj:
  forall f g m1 m2 b1 b2 delta
    (MINJ: mem_inj f g m1 m2)
    (FB : f b1 = Some (b2, delta))
    (PERM: exists o k p, perm m1 b1 o k p /\ inject_perm_condition p),
    option_le_stack (fun fi =>
                 forall ofs k p,
                   perm m1 b1 ofs k p ->
                   inject_perm_condition p ->
                   frame_public fi (ofs + delta))
              (inject_frame_info delta)
              delta
              (get_frame_info (stack m1) b1)
              (get_frame_info (stack m2) b2).

Lemma stack_access_inj:
  forall f g m1 m2 b1 b2 delta lo hi p
    (MINJ : mem_inj f g m1 m2)
    (FB : f b1 = Some (b2, delta))
    (RP: range_perm m1 b1 lo hi Cur p)
    (IPC: inject_perm_condition p)
    (NPSA: stack_access (stack m1) b1 lo hi),
    stack_access (stack m2) b2 (lo + delta) (hi + delta).

Lemma valid_access_inj_gen:
  forall f g m1 m2 b1 b2 delta chunk ofs p
         (MINJ : stack_inject f g (perm m1) (stack m1) (stack m2))
         (PERMS: forall b1 b2 delta,
             f b1 = Some (b2, delta) ->
             forall o k p,
               perm m1 b1 o k p ->
               inject_perm_condition p ->
               perm m2 b2 (o+delta) k p)
         (ALIGN: forall b1 b2 delta chunk ofs p,
             f b1 = Some (b2, delta) ->
             range_perm m1 b1 ofs (ofs+size_chunk chunk) Max p ->
             (align_chunk chunk | delta)),
    f b1 = Some(b2, delta) ->
    valid_access m1 chunk b1 ofs p ->
    inject_perm_condition p ->
    valid_access m2 chunk b2 (ofs + delta) p.

Lemma valid_access_inj:
  forall f g m1 m2 b1 b2 delta chunk ofs p,
  mem_inj f g m1 m2 ->
  f b1 = Some(b2, delta) ->
  valid_access m1 chunk b1 ofs p ->
  inject_perm_condition p ->
  valid_access m2 chunk b2 (ofs + delta) p.


Lemma getN_inj:
  forall f g m1 m2 b1 b2 delta,
  mem_inj f g m1 m2 ->
  f b1 = Some(b2, delta) ->
  forall n ofs,
  range_perm m1 b1 ofs (ofs + Z_of_nat n) Cur Readable ->
  list_forall2 (memval_inject f)
               (getN n ofs (m1.(mem_contents)#b1))
               (getN n (ofs + delta) (m2.(mem_contents)#b2)).

Lemma load_inj:
  forall f g m1 m2 chunk b1 ofs b2 delta v1,
  mem_inj f g m1 m2 ->
  load chunk m1 b1 ofs = Some v1 ->
  f b1 = Some (b2, delta) ->
  exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ Val.inject f v1 v2.

Lemma loadbytes_inj:
  forall f g m1 m2 len b1 ofs b2 delta bytes1,
  mem_inj f g m1 m2 ->
  loadbytes m1 b1 ofs len = Some bytes1 ->
  f b1 = Some (b2, delta) ->
  exists bytes2, loadbytes m2 b2 (ofs + delta) len = Some bytes2
              /\ list_forall2 (memval_inject f) bytes1 bytes2.

Lemma proj_value_is_inj_value:
  forall q t v,
    proj_value q t = v ->
    v <> Vundef ->
    t = inj_value q v.


Lemma setN_getN_old:
  forall l o t,
    t = setN (getN l o t) o t.

Lemma maybe_store:
  forall m1 b1 o1 b o m2,
    load Mptr m1 b1 o1 = Some (Vptr b o) ->
    store Mptr m1 b1 o1 (Vptr b o) = Some m2 -> m1 = m2.


Lemma getN_undef_not_inj_bytes:
  forall n o l,
    (n > 0)%nat ->
    getN n o (ZMap.init Undef) <> inj_bytes l.

Lemma getN_undef_not_inj_value:
  forall n o q v,
    (n > 0)%nat ->
    getN n o (ZMap.init Undef) <> inj_value q v.

Lemma maybe_store_val:
  forall m1 b o v m2,
    v <> Vundef ->
    Val.has_type v Tptr ->
    loadbytes m1 b o (size_chunk Mptr) = Some (encode_val Mptr v) ->
    store Mptr m1 b o v = Some m2 -> m1 = m2.



Lemma val_inject_eq:
  forall f v1 v2 v2',
    Val.inject f v1 v2 ->
    Val.inject f v1 v2' ->
    v1 = Vundef \/ v2 = v2'.

Lemma memval_inject_eq:
  forall f m1 m2 m2',
    memval_inject f m1 m2 ->
    memval_inject f m1 m2' ->
    m1 = Undef \/ (exists q n, m1 = Fragment Vundef q n) \/ m2 = m2'.

Lemma setN_inj:
  forall (access: Z -> Prop) delta f vl1 vl2,
  list_forall2 (memval_inject f) vl1 vl2 ->
  forall p c1 c2,
  (forall q, access q -> memval_inject f (ZMap.get q c1) (ZMap.get (q + delta) c2)) ->
  (forall q, access q -> memval_inject f (ZMap.get q (setN vl1 p c1))
                                         (ZMap.get (q + delta) (setN vl2 (p + delta) c2))).

Lemma store_stack:
  forall chunk m1 b1 ofs v1 n1,
    store chunk m1 b1 ofs v1 = Some n1 ->
    stack n1 = stack m1.

Lemma store_mapped_inj:
  forall f g chunk m1 b1 ofs v1 n1 m2 b2 delta v2,
    mem_inj f g m1 m2 ->
    store chunk m1 b1 ofs v1 = Some n1 ->
    meminj_no_overlap f m1 ->
    f b1 = Some (b2, delta) ->
    Val.inject f v1 v2 ->
    exists n2,
      store chunk m2 b2 (ofs + delta) v2 = Some n2
      /\ mem_inj f g n1 n2.

Lemma store_unmapped_inj:
  forall f g chunk m1 b1 ofs v1 n1 m2,
    mem_inj f g m1 m2 ->
    store chunk m1 b1 ofs v1 = Some n1 ->
    f b1 = None ->
    mem_inj f g n1 m2.

Lemma store_outside_inj:
  forall f g m1 m2 chunk b ofs v m2',
    mem_inj f g m1 m2 ->
    (forall b' delta ofs',
        f b' = Some(b, delta) ->
        perm m1 b' ofs' Cur Readable ->
        ofs <= ofs' + delta < ofs + size_chunk chunk -> False) ->
    store chunk m2 b ofs v = Some m2' ->
    mem_inj f g m1 m2'.

Lemma nth_getN_refl : forall n ofs ofs' mcontents,
        ofs' >= ofs -> ofs' < ofs + Z.of_nat n ->
        nth (nat_of_Z (ofs' - ofs)) (getN n ofs mcontents) Undef = ZMap.get ofs' mcontents.

Lemma nth_setN_refl : forall lv ofs' ofs mcontents,
  ofs' >= ofs -> ofs' < ofs + Zlength lv ->
  nth (nat_of_Z (ofs' - ofs)) lv Undef = ZMap.get ofs' (setN lv ofs mcontents).

Lemma store_right_inj:
  forall f g m1 m2 chunk b ofs v m2',
    mem_inj f g m1 m2 ->
    (forall b' delta ofs',
        f b' = Some(b, delta) ->
        ofs' + delta = ofs ->
        exists vl, loadbytes m1 b' ofs' (size_chunk chunk) = Some vl /\
        list_forall2 (memval_inject f) vl (encode_val chunk v)) ->
    store chunk m2 b ofs v = Some m2' ->
    mem_inj f g m1 m2'.


Lemma storebytes_mapped_inj:
  forall f g m1 b1 ofs bytes1 n1 m2 b2 delta bytes2,
    mem_inj f g m1 m2 ->
    storebytes m1 b1 ofs bytes1 = Some n1 ->
    meminj_no_overlap f m1 ->
    f b1 = Some (b2, delta) ->
    list_forall2 (memval_inject f) bytes1 bytes2 ->
    exists n2,
      storebytes m2 b2 (ofs + delta) bytes2 = Some n2
      /\ mem_inj f g n1 n2.

Lemma storebytes_unmapped_inj:
  forall f g m1 b1 ofs bytes1 n1 m2,
    mem_inj f g m1 m2 ->
    storebytes m1 b1 ofs bytes1 = Some n1 ->
    f b1 = None ->
    mem_inj f g n1 m2.

Lemma storebytes_outside_inj:
  forall f g m1 m2 b ofs bytes2 m2',
    mem_inj f g m1 m2 ->
    (forall b' delta ofs',
        f b' = Some(b, delta) ->
        perm m1 b' ofs' Cur Readable ->
        ofs <= ofs' + delta < ofs + Z_of_nat (length bytes2) -> False) ->
    storebytes m2 b ofs bytes2 = Some m2' ->
    mem_inj f g m1 m2'.

Lemma storebytes_empty_inj:
  forall f g m1 b1 ofs1 m1' m2 b2 ofs2 m2',
    mem_inj f g m1 m2 ->
    storebytes m1 b1 ofs1 nil = Some m1' ->
    storebytes m2 b2 ofs2 nil = Some m2' ->
    mem_inj f g m1' m2'.


Lemma alloc_right_inj:
  forall f g m1 m2 lo hi b2 m2',
    mem_inj f g m1 m2 ->
    alloc m2 lo hi = (m2', b2) ->
    mem_inj f g m1 m2'.

Lemma alloc_left_unmapped_inj:
  forall f g m1 m2 lo hi m1' b1,
    mem_inj f g m1 m2 ->
    alloc m1 lo hi = (m1', b1) ->
    f b1 = None ->
    mem_inj f g m1' m2.

Definition inj_offset_aligned (delta: Z) (size: Z) : Prop :=
  forall chunk, size_chunk chunk <= size -> (align_chunk chunk | delta).

Lemma alloc_left_mapped_inj:
  forall f g m1 m2 lo hi m1' b1 b2 delta,
    mem_inj f g m1 m2 ->
    alloc m1 lo hi = (m1', b1) ->
    valid_block m2 b2 ->
    inj_offset_aligned delta (hi-lo) ->
    (forall ofs k p, lo <= ofs < hi -> inject_perm_condition p -> perm m2 b2 (ofs + delta) k p) ->
    f b1 = Some(b2, delta) ->
    (~ Plt b1 (nextblock m1) ->
     forall fi,
       in_stack' (stack m2) (b2,fi) ->
       forall o k pp,
         perm m1' b1 o k pp ->
         inject_perm_condition pp ->
         frame_public fi (o + delta)
    ) ->
    mem_inj f g m1' m2.

Lemma free_left_inj:
  forall f g m1 m2 b lo hi m1',
  mem_inj f g m1 m2 ->
  free m1 b lo hi = Some m1' ->
  mem_inj f g m1' m2.

Lemma free_right_inj:
  forall f g m1 m2 b lo hi m2',
  mem_inj f g m1 m2 ->
  free m2 b lo hi = Some m2' ->
  (forall b' delta ofs k p,
    f b' = Some(b, delta) ->
    perm m1 b' ofs k p -> lo <= ofs + delta < hi -> False) ->
  mem_inj f g m1 m2'.


Lemma drop_perm_stack:
  forall m1 b lo hi p m1',
    drop_perm m1 b lo hi p = Some m1' ->
    stack m1' = stack m1.

Lemma drop_unmapped_inj:
  forall f g m1 m2 b lo hi p m1',
  mem_inj f g m1 m2 ->
  drop_perm m1 b lo hi p = Some m1' ->
  f b = None ->
  mem_inj f g m1' m2.

Lemma drop_mapped_inj:
  forall f g m1 m2 b1 b2 delta lo hi p m1',
  mem_inj f g m1 m2 ->
  drop_perm m1 b1 lo hi p = Some m1' ->
  range_perm m2 b2 (lo + delta) (hi + delta) Cur Freeable ->
  meminj_no_overlap f m1 ->
  f b1 = Some(b2, delta) ->
  exists m2',
      drop_perm m2 b2 (lo + delta) (hi + delta) p = Some m2'
   /\ mem_inj f g m1' m2'.

Lemma drop_partial_mapped_inj:
  forall f g m1 m2 b1 b2 delta lo1 hi1 lo2 hi2 p m1',
  mem_inj f g m1 m2 ->
  drop_perm m1 b1 lo1 hi1 p = Some m1' ->
  f b1 = Some(b2, delta) ->
  lo2 <= lo1 -> hi1 <= hi2 ->
  range_perm m2 b2 (lo2 + delta) (hi2 + delta) Cur Freeable ->
  meminj_no_overlap f m1 ->
  (forall b' delta' ofs' k p,
    f b' = Some(b2, delta') ->
    perm m1 b' ofs' k p ->
    ((lo2 + delta <= ofs' + delta' < lo1 + delta )
     \/ (hi1 + delta <= ofs' + delta' < hi2 + delta)) -> False) ->
  exists m2',
      drop_perm m2 b2 (lo2 + delta) (hi2 + delta) p = Some m2'
   /\ mem_inj f g m1' m2'.


Lemma drop_outside_inj: forall f g m1 m2 b lo hi p m2',
  mem_inj f g m1 m2 ->
  drop_perm m2 b lo hi p = Some m2' ->
  (forall b' delta ofs' k p,
    f b' = Some(b, delta) ->
    perm m1 b' ofs' k p ->
    lo <= ofs' + delta < hi -> False) ->
  mem_inj f g m1 m2'.

Lemma drop_right_inj: forall f g m1 m2 b lo hi p m2',
  mem_inj f g m1 m2 ->
  drop_perm m2 b lo hi p = Some m2' ->
  (forall b' delta ofs' k p',
    f b' = Some(b, delta) ->
    perm m1 b' ofs' k p' ->
    lo <= ofs' + delta < hi -> p' = p) ->
  mem_inj f g m1 m2'.

Theorem extends_refl:
  forall m, extends m m.

Theorem load_extends:
  forall chunk m1 m2 b ofs v1,
  extends m1 m2 ->
  load chunk m1 b ofs = Some v1 ->
  exists v2, load chunk m2 b ofs = Some v2 /\ Val.lessdef v1 v2.

Theorem loadv_extends:
  forall chunk m1 m2 addr1 addr2 v1,
  extends m1 m2 ->
  loadv chunk m1 addr1 = Some v1 ->
  Val.lessdef addr1 addr2 ->
  exists v2, loadv chunk m2 addr2 = Some v2 /\ Val.lessdef v1 v2.

Theorem loadbytes_extends:
  forall m1 m2 b ofs len bytes1,
  extends m1 m2 ->
  loadbytes m1 b ofs len = Some bytes1 ->
  exists bytes2, loadbytes m2 b ofs len = Some bytes2
              /\ list_forall2 memval_lessdef bytes1 bytes2.

Lemma storev_stack:
 forall chunk m1 addr v m2,
   storev chunk m1 addr v = Some m2 ->
   stack m2 = stack m1.

Ltac rewrite_stack_backwards :=
  repeat match goal with
         | H: store _ ?m1 _ _ _ = Some ?m2 |- context [stack ?m2] =>
           rewrite (store_stack _ _ _ _ _ _ H)
         | H: storev _ ?m1 _ _ = Some ?m2 |- context [stack ?m2] =>
           rewrite (storev_stack _ _ _ _ _ H)
         | H: storebytes ?m1 _ _ _ = Some ?m2 |- context [stack ?m2] =>
           rewrite (storebytes_stack _ _ _ _ _ H)
         | H: alloc ?m1 _ _ = (?m2,_) |- context [stack ?m2] =>
           rewrite (alloc_stack _ _ _ _ _ H)
         | H: free ?m1 _ _ _ = Some ?m2 |- context [stack ?m2] =>
           rewrite (free_stack _ _ _ _ _ H)
         | H: drop_perm ?m1 _ _ _ _ = Some ?m2 |- context [stack ?m2] =>
           rewrite (drop_perm_stack _ _ _ _ _ _ H)
         end.

Theorem store_within_extends:
  forall chunk m1 m2 b ofs v1 m1' v2,
  extends m1 m2 ->
  store chunk m1 b ofs v1 = Some m1' ->
  Val.lessdef v1 v2 ->
  exists m2',
     store chunk m2 b ofs v2 = Some m2'
  /\ extends m1' m2'.

Theorem store_outside_extends:
  forall chunk m1 m2 b ofs v m2',
  extends m1 m2 ->
  store chunk m2 b ofs v = Some m2' ->
  (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + size_chunk chunk -> False) ->
  extends m1 m2'.

Theorem storev_extends:
  forall chunk m1 m2 addr1 v1 m1' addr2 v2,
  extends m1 m2 ->
  storev chunk m1 addr1 v1 = Some m1' ->
  Val.lessdef addr1 addr2 ->
  Val.lessdef v1 v2 ->
  exists m2',
     storev chunk m2 addr2 v2 = Some m2'
  /\ extends m1' m2'.

Theorem storebytes_within_extends:
  forall m1 m2 b ofs bytes1 m1' bytes2,
  extends m1 m2 ->
  storebytes m1 b ofs bytes1 = Some m1' ->
  list_forall2 memval_lessdef bytes1 bytes2 ->
  exists m2',
     storebytes m2 b ofs bytes2 = Some m2'
  /\ extends m1' m2'.

Theorem storebytes_outside_extends:
  forall m1 m2 b ofs bytes2 m2',
  extends m1 m2 ->
  storebytes m2 b ofs bytes2 = Some m2' ->
  (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + Z_of_nat (length bytes2) -> False) ->
  extends m1 m2'.

Theorem alloc_extends:
  forall m1 m2 lo1 hi1 b m1' lo2 hi2,
  extends m1 m2 ->
  alloc m1 lo1 hi1 = (m1', b) ->
  lo2 <= lo1 -> hi1 <= hi2 ->
  exists m2',
     alloc m2 lo2 hi2 = (m2', b)
  /\ extends m1' m2'.

Theorem free_left_extends:
  forall m1 m2 b lo hi m1',
  extends m1 m2 ->
  free m1 b lo hi = Some m1' ->
  extends m1' m2.

Theorem free_right_extends:
  forall m1 m2 b lo hi m2',
  extends m1 m2 ->
  free m2 b lo hi = Some m2' ->
  (forall ofs k p, perm m1 b ofs k p -> lo <= ofs < hi -> False) ->
  extends m1 m2'.

Theorem free_parallel_extends:
  forall m1 m2 b lo hi m1',
  extends m1 m2 ->
  inject_perm_condition Freeable ->
  free m1 b lo hi = Some m1' ->
  exists m2',
     free m2 b lo hi = Some m2'
  /\ extends m1' m2'.

Theorem valid_block_extends:
  forall m1 m2 b,
  extends m1 m2 ->
  (valid_block m1 b <-> valid_block m2 b).

Theorem perm_extends:
  forall m1 m2 b ofs k p,
  extends m1 m2 -> perm m1 b ofs k p -> inject_perm_condition p -> perm m2 b ofs k p.

Theorem perm_extends_inv:
  forall m1 m2 b ofs k p,
  extends m1 m2 -> perm m2 b ofs k p -> perm m1 b ofs k p \/ ~perm m1 b ofs Max Nonempty.

Theorem valid_access_extends:
  forall m1 m2 chunk b ofs p,
    extends m1 m2 -> valid_access m1 chunk b ofs p -> inject_perm_condition p ->
    valid_access m2 chunk b ofs p.

Theorem valid_pointer_extends:
  forall m1 m2 b ofs,
  extends m1 m2 -> valid_pointer m1 b ofs = true -> valid_pointer m2 b ofs = true.

Theorem weak_valid_pointer_extends:
  forall m1 m2 b ofs,
  extends m1 m2 ->
  weak_valid_pointer m1 b ofs = true -> weak_valid_pointer m2 b ofs = true.

Lemma magree_monotone:
  forall m1 m2 (P Q: locset),
  magree m1 m2 P ->
  (forall b ofs, Q b ofs -> P b ofs) ->
  magree m1 m2 Q.

Lemma mextends_agree:
  forall m1 m2 P, extends m1 m2 -> magree m1 m2 P.

Lemma magree_extends:
  forall m1 m2 (P: locset),
  (forall b ofs, P b ofs) ->
  magree m1 m2 P -> extends m1 m2.

Lemma magree_loadbytes:
  forall m1 m2 P b ofs n bytes,
  magree m1 m2 P ->
  loadbytes m1 b ofs n = Some bytes ->
  (forall i, ofs <= i < ofs + n -> P b i) ->
  exists bytes', loadbytes m2 b ofs n = Some bytes' /\ list_forall2 memval_lessdef bytes bytes'.

Lemma magree_load:
  forall m1 m2 P chunk b ofs v,
  magree m1 m2 P ->
  load chunk m1 b ofs = Some v ->
  (forall i, ofs <= i < ofs + size_chunk chunk -> P b i) ->
  exists v', load chunk m2 b ofs = Some v' /\ Val.lessdef v v'.

Lemma is_stack_top_magree:
  forall P m1 m2 b
    (MINJ: magree m1 m2 P)
    (PERM: exists o k p, perm m1 b o k p /\ inject_perm_condition p)
    (IST: is_stack_top (stack m1) b),
    is_stack_top (stack m2) b.

Lemma get_frame_info_magree:
  forall P m1 m2 b
    (MINJ: magree m1 m2 P)
    (PERM: exists o k p, perm m1 b o k p /\ inject_perm_condition p),
    option_le_stack (fun fi =>
                 forall ofs k p,
                   perm m1 b ofs k p ->
                   inject_perm_condition p ->
                   frame_public fi ofs)
              (inject_frame_info 0) 0
              (get_frame_info (stack m1) b)
              (get_frame_info (stack m2) b).

Lemma stack_access_magree:
  forall P m1 m2 b lo hi p
    (MINJ : magree m1 m2 P)
    (RP: range_perm m1 b lo hi Cur p)
    (IPC: inject_perm_condition p)
    (NPSA: stack_access (stack m1) b lo hi),
    stack_access (stack m2) b lo hi.

Lemma magree_storebytes_parallel:
  forall m1 m2 (P Q: locset) b ofs bytes1 m1' bytes2,
  magree m1 m2 P ->
  storebytes m1 b ofs bytes1 = Some m1' ->
  (forall b' i, Q b' i ->
                b' <> b \/ i < ofs \/ ofs + Z_of_nat (length bytes1) <= i ->
                P b' i) ->
  list_forall2 memval_lessdef bytes1 bytes2 ->
  exists m2', storebytes m2 b ofs bytes2 = Some m2' /\ magree m1' m2' Q.

Lemma magree_storebytes_left:
  forall m1 m2 P b ofs bytes1 m1',
  magree m1 m2 P ->
  storebytes m1 b ofs bytes1 = Some m1' ->
  (forall i, ofs <= i < ofs + Z_of_nat (length bytes1) -> ~(P b i)) ->
  magree m1' m2 P.

Lemma magree_store_left:
  forall m1 m2 P chunk b ofs v1 m1',
  magree m1 m2 P ->
  store chunk m1 b ofs v1 = Some m1' ->
  (forall i, ofs <= i < ofs + size_chunk chunk -> ~(P b i)) ->
  magree m1' m2 P.

Lemma magree_free:
  forall m1 m2 (P Q: locset) b lo hi m1',
  magree m1 m2 P ->
  inject_perm_condition Freeable ->
  free m1 b lo hi = Some m1' ->
  (forall b' i, Q b' i ->
                b' <> b \/ ~(lo <= i < hi) ->
                P b' i) ->
  exists m2', free m2 b lo hi = Some m2' /\ magree m1' m2' Q.

Lemma magree_valid_access:
  forall m1 m2 (P: locset) chunk b ofs p,
  magree m1 m2 P ->
  valid_access m1 chunk b ofs p ->
  inject_perm_condition p ->
  valid_access m2 chunk b ofs p.


Theorem valid_block_inject_1:
  forall f g m1 m2 b1 b2 delta,
  f b1 = Some(b2, delta) ->
  inject f g m1 m2 ->
  valid_block m1 b1.

Theorem valid_block_inject_2:
  forall f g m1 m2 b1 b2 delta,
  f b1 = Some(b2, delta) ->
  inject f g m1 m2 ->
  valid_block m2 b2.

Local Hint Resolve valid_block_inject_1 valid_block_inject_2: mem.

Theorem perm_inject:
  forall f g m1 m2 b1 b2 delta ofs k p,
  f b1 = Some(b2, delta) ->
  inject f g m1 m2 ->
  perm m1 b1 ofs k p ->
  inject_perm_condition p ->
  perm m2 b2 (ofs + delta) k p.

Theorem perm_inject_inv:
  forall f g m1 m2 b1 ofs b2 delta k p,
  inject f g m1 m2 ->
  f b1 = Some(b2, delta) ->
  perm m2 b2 (ofs + delta) k p ->
  perm m1 b1 ofs k p \/ ~perm m1 b1 ofs Max Nonempty.

Theorem range_perm_inject:
  forall f g m1 m2 b1 b2 delta lo hi k p,
  f b1 = Some(b2, delta) ->
  inject f g m1 m2 ->
  range_perm m1 b1 lo hi k p ->
  inject_perm_condition p ->
  range_perm m2 b2 (lo + delta) (hi + delta) k p.

Theorem valid_access_inject:
  forall f g m1 m2 chunk b1 ofs b2 delta p,
  f b1 = Some(b2, delta) ->
  inject f g m1 m2 ->
  valid_access m1 chunk b1 ofs p ->
  inject_perm_condition p ->
  valid_access m2 chunk b2 (ofs + delta) p.

Theorem weak_valid_pointer_nonempty_perm:
  forall m b ofs,
  weak_valid_pointer m b ofs = true <->
  (perm m b ofs Cur Nonempty) \/ (perm m b (ofs-1) Cur Nonempty).

Lemma weak_valid_pointer_size_bounds : forall f g b1 b2 m1 m2 ofs delta,
  f b1 = Some (b2, delta) ->
  inject f g m1 m2 ->
  weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
  0 <= delta <= Ptrofs.max_unsigned /\
  0 <= Ptrofs.unsigned ofs + delta <= Ptrofs.max_unsigned.

Theorem valid_pointer_inject:
  forall f g m1 m2 b1 ofs b2 delta,
  f b1 = Some(b2, delta) ->
  inject f g m1 m2 ->
  valid_pointer m1 b1 ofs = true ->
  valid_pointer m2 b2 (ofs + delta) = true.

Theorem valid_pointer_inject' :
  forall f g m1 m2 b1 ofs b2 delta,
    f b1 = Some(b2, delta) ->
    inject f g m1 m2 ->
    valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
    valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.

Theorem weak_valid_pointer_inject:
  forall f g m1 m2 b1 ofs b2 delta,
  f b1 = Some(b2, delta) ->
  inject f g m1 m2 ->
  weak_valid_pointer m1 b1 ofs = true ->
  weak_valid_pointer m2 b2 (ofs + delta) = true.

Theorem weak_valid_pointer_inject':
  forall f g m1 m2 b1 ofs b2 delta,
  f b1 = Some(b2, delta) ->
  inject f g m1 m2 ->
  weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
  weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.



Lemma delta_pos:
  forall f g m1 m2 b1 b2 delta,
  inject f g m1 m2 ->
  f b1 = Some (b2, delta) ->
  delta >= 0.

Lemma address_inject:
  forall f g m1 m2 b1 ofs1 b2 delta p,
  inject f g m1 m2 ->
  perm m1 b1 (Ptrofs.unsigned ofs1) Cur p ->
  f b1 = Some (b2, delta) ->
  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta.

Lemma address_inject':
  forall f g m1 m2 chunk b1 ofs1 b2 delta,
  inject f g m1 m2 ->
  valid_access m1 chunk b1 (Ptrofs.unsigned ofs1) Nonempty ->
  f b1 = Some (b2, delta) ->
  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta.

Theorem weak_valid_pointer_inject_no_overflow:
  forall f g m1 m2 b ofs b' delta,
  inject f g m1 m2 ->
  weak_valid_pointer m1 b (Ptrofs.unsigned ofs) = true ->
  f b = Some(b', delta) ->
  0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.

Theorem valid_pointer_inject_no_overflow:
  forall f g m1 m2 b ofs b' delta,
  inject f g m1 m2 ->
  valid_pointer m1 b (Ptrofs.unsigned ofs) = true ->
  f b = Some(b', delta) ->
  0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.

Theorem valid_pointer_inject_val:
  forall f g m1 m2 b ofs b' ofs',
  inject f g m1 m2 ->
  valid_pointer m1 b (Ptrofs.unsigned ofs) = true ->
  Val.inject f (Vptr b ofs) (Vptr b' ofs') ->
  valid_pointer m2 b' (Ptrofs.unsigned ofs') = true.

Theorem weak_valid_pointer_inject_val:
  forall f g m1 m2 b ofs b' ofs',
  inject f g m1 m2 ->
  weak_valid_pointer m1 b (Ptrofs.unsigned ofs) = true ->
  Val.inject f (Vptr b ofs) (Vptr b' ofs') ->
  weak_valid_pointer m2 b' (Ptrofs.unsigned ofs') = true.

Theorem inject_no_overlap:
  forall f g m1 m2 b1 b2 b1' b2' delta1 delta2 ofs1 ofs2,
  inject f g m1 m2 ->
  b1 <> b2 ->
  f b1 = Some (b1', delta1) ->
  f b2 = Some (b2', delta2) ->
  perm m1 b1 ofs1 Max Nonempty ->
  perm m1 b2 ofs2 Max Nonempty ->
  b1' <> b2' \/ ofs1 + delta1 <> ofs2 + delta2.

Theorem different_pointers_inject:
  forall f g m m' b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
  inject f g m m' ->
  b1 <> b2 ->
  valid_pointer m b1 (Ptrofs.unsigned ofs1) = true ->
  valid_pointer m b2 (Ptrofs.unsigned ofs2) = true ->
  f b1 = Some (b1', delta1) ->
  f b2 = Some (b2', delta2) ->
  b1' <> b2' \/
  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <>
  Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)).

Theorem disjoint_or_equal_inject:
  forall f g m m' b1 b1' delta1 b2 b2' delta2 ofs1 ofs2 sz,
  inject f g m m' ->
  f b1 = Some(b1', delta1) ->
  f b2 = Some(b2', delta2) ->
  range_perm m b1 ofs1 (ofs1 + sz) Max Nonempty ->
  range_perm m b2 ofs2 (ofs2 + sz) Max Nonempty ->
  sz > 0 ->
  b1 <> b2 \/ ofs1 = ofs2 \/ ofs1 + sz <= ofs2 \/ ofs2 + sz <= ofs1 ->
  b1' <> b2' \/ ofs1 + delta1 = ofs2 + delta2
             \/ ofs1 + delta1 + sz <= ofs2 + delta2
             \/ ofs2 + delta2 + sz <= ofs1 + delta1.

Theorem aligned_area_inject:
  forall f g m m' b ofs al sz b' delta,
  inject f g m m' ->
  al = 1 \/ al = 2 \/ al = 4 \/ al = 8 -> sz > 0 ->
  (al | sz) ->
  range_perm m b ofs (ofs + sz) Cur Nonempty ->
  (al | ofs) ->
  f b = Some(b', delta) ->
  (al | ofs + delta).


Theorem load_inject:
  forall f g m1 m2 chunk b1 ofs b2 delta v1,
  inject f g m1 m2 ->
  load chunk m1 b1 ofs = Some v1 ->
  f b1 = Some (b2, delta) ->
  exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ Val.inject f v1 v2.

Theorem loadv_inject:
  forall f g m1 m2 chunk a1 a2 v1,
  inject f g m1 m2 ->
  loadv chunk m1 a1 = Some v1 ->
  Val.inject f a1 a2 ->
  exists v2, loadv chunk m2 a2 = Some v2 /\ Val.inject f v1 v2.

Theorem loadbytes_inject:
  forall f g m1 m2 b1 ofs len b2 delta bytes1,
  inject f g m1 m2 ->
  loadbytes m1 b1 ofs len = Some bytes1 ->
  f b1 = Some (b2, delta) ->
  exists bytes2, loadbytes m2 b2 (ofs + delta) len = Some bytes2
              /\ list_forall2 (memval_inject f) bytes1 bytes2.


Theorem store_mapped_inject:
  forall f g chunk m1 b1 ofs v1 n1 m2 b2 delta v2,
  inject f g m1 m2 ->
  store chunk m1 b1 ofs v1 = Some n1 ->
  f b1 = Some (b2, delta) ->
  Val.inject f v1 v2 ->
  exists n2,
    store chunk m2 b2 (ofs + delta) v2 = Some n2
    /\ inject f g n1 n2.

Theorem store_mapped_weak_inject:
  forall f g chunk m1 b1 ofs v1 n1 m2 b2 delta v2,
  weak_inject f g m1 m2 ->
  store chunk m1 b1 ofs v1 = Some n1 ->
  f b1 = Some (b2, delta) ->
  Val.inject f v1 v2 ->
  exists n2,
    store chunk m2 b2 (ofs + delta) v2 = Some n2
    /\ weak_inject f g n1 n2.

Theorem store_unmapped_inject:
  forall f g chunk m1 b1 ofs v1 n1 m2,
  inject f g m1 m2 ->
  store chunk m1 b1 ofs v1 = Some n1 ->
  f b1 = None ->
  inject f g n1 m2.

Theorem store_outside_inject:
  forall f g m1 m2 chunk b ofs v m2',
  inject f g m1 m2 ->
  (forall b' delta ofs',
    f b' = Some(b, delta) ->
    perm m1 b' ofs' Cur Readable ->
    ofs <= ofs' + delta < ofs + size_chunk chunk -> False) ->
  store chunk m2 b ofs v = Some m2' ->
  inject f g m1 m2'.

Theorem store_right_inject:
  forall f g m1 m2 chunk b ofs v m2',
    inject f g m1 m2 ->
    (forall b' delta ofs',
        f b' = Some(b, delta) ->
        ofs' + delta = ofs ->
        exists vl, loadbytes m1 b' ofs' (size_chunk chunk) = Some vl /\
        list_forall2 (memval_inject f) vl (encode_val chunk v)) ->
    store chunk m2 b ofs v = Some m2' ->
    inject f g m1 m2'.

Theorem storev_mapped_inject:
  forall f g chunk m1 a1 v1 n1 m2 a2 v2,
  inject f g m1 m2 ->
  storev chunk m1 a1 v1 = Some n1 ->
  Val.inject f a1 a2 ->
  Val.inject f v1 v2 ->
  exists n2,
    storev chunk m2 a2 v2 = Some n2 /\ inject f g n1 n2.

Theorem storebytes_mapped_inject:
  forall f g m1 b1 ofs bytes1 n1 m2 b2 delta bytes2,
  inject f g m1 m2 ->
  storebytes m1 b1 ofs bytes1 = Some n1 ->
  f b1 = Some (b2, delta) ->
  list_forall2 (memval_inject f) bytes1 bytes2 ->
  exists n2,
    storebytes m2 b2 (ofs + delta) bytes2 = Some n2
    /\ inject f g n1 n2.

Theorem storebytes_unmapped_inject:
  forall f g m1 b1 ofs bytes1 n1 m2,
  inject f g m1 m2 ->
  storebytes m1 b1 ofs bytes1 = Some n1 ->
  f b1 = None ->
  inject f g n1 m2.

Theorem storebytes_outside_inject:
  forall f g m1 m2 b ofs bytes2 m2',
  inject f g m1 m2 ->
  (forall b' delta ofs',
    f b' = Some(b, delta) ->
    perm m1 b' ofs' Cur Readable ->
    ofs <= ofs' + delta < ofs + Z_of_nat (length bytes2) -> False) ->
  storebytes m2 b ofs bytes2 = Some m2' ->
  inject f g m1 m2'.

Theorem storebytes_empty_inject:
  forall f g m1 b1 ofs1 m1' m2 b2 ofs2 m2',
  inject f g m1 m2 ->
  storebytes m1 b1 ofs1 nil = Some m1' ->
  storebytes m2 b2 ofs2 nil = Some m2' ->
  inject f g m1' m2'.


Theorem alloc_right_inject:
  forall f g m1 m2 lo hi b2 m2',
  inject f g m1 m2 ->
  alloc m2 lo hi = (m2', b2) ->
  inject f g m1 m2'.


Theorem alloc_left_unmapped_inject:
  forall f g m1 m2 lo hi m1' b1,
  inject f g m1 m2 ->
  alloc m1 lo hi = (m1', b1) ->
  exists f',
     inject f' g m1' m2
  /\ inject_incr f f'
  /\ f' b1 = None
  /\ (forall b, b <> b1 -> f' b = f b).

Theorem alloc_left_unmapped_weak_inject:
  forall f g m1 m2 lo hi m1' b1,
  f b1 = None ->
  weak_inject f g m1 m2 ->
  alloc m1 lo hi = (m1', b1) ->
  weak_inject f g m1' m2.

Theorem alloc_left_mapped_inject:
  forall f g m1 m2 lo hi m1' b1 b2 delta,
  inject f g m1 m2 ->
  alloc m1 lo hi = (m1', b1) ->
  valid_block m2 b2 ->
  0 <= delta <= Ptrofs.max_unsigned ->
  (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Ptrofs.max_unsigned) ->
  (forall ofs k p, lo <= ofs < hi -> inject_perm_condition p -> perm m2 b2 (ofs + delta) k p) ->
  inj_offset_aligned delta (hi-lo) ->
  (forall b delta' ofs k p,
   f b = Some (b2, delta') ->
   perm m1 b ofs k p ->
   lo + delta <= ofs + delta' < hi + delta -> False) ->
  (forall fi,
      in_stack' (stack m2) (b2,fi) ->
      forall o k pp,
        perm m1' b1 o k pp ->
        inject_perm_condition pp ->
        frame_public fi (o + delta)) ->
  exists f',
     inject f' g m1' m2
  /\ inject_incr f f'
  /\ f' b1 = Some(b2, delta)
  /\ (forall b, b <> b1 -> f' b = f b).

Theorem alloc_parallel_inject:
  forall f g m1 m2 lo1 hi1 m1' b1 lo2 hi2,
  inject f g m1 m2 ->
  alloc m1 lo1 hi1 = (m1', b1) ->
  lo2 <= lo1 -> hi1 <= hi2 ->
  exists f', exists m2', exists b2,
  alloc m2 lo2 hi2 = (m2', b2)
  /\ inject f' g m1' m2'
  /\ inject_incr f f'
  /\ f' b1 = Some(b2, 0)
  /\ (forall b, b <> b1 -> f' b = f b).

Theorem alloc_left_mapped_weak_inject:
  forall f g m1 m2 lo hi m1' b1 b2 delta,
  f b1 = Some(b2, delta) ->
  weak_inject f g m1 m2 ->
  alloc m1 lo hi = (m1', b1) ->
  valid_block m2 b2 ->
  0 <= delta <= Ptrofs.max_unsigned ->
  (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Ptrofs.max_unsigned) ->
  (forall ofs k p, lo <= ofs < hi -> inject_perm_condition p -> perm m2 b2 (ofs + delta) k p) ->
  inj_offset_aligned delta (hi-lo) ->
  (forall b delta' ofs k p,
   f b = Some (b2, delta') ->
   perm m1 b ofs k p ->
   lo + delta <= ofs + delta' < hi + delta -> False) ->
  (forall fi,
      in_stack' (stack m2) (b2,fi) ->
      forall o k pp,
        perm m1' b1 o k pp ->
        inject_perm_condition pp ->
        frame_public fi (o + delta)) ->
  weak_inject f g m1' m2.


Lemma free_left_inject:
  forall f g m1 m2 b lo hi m1',
  inject f g m1 m2 ->
  free m1 b lo hi = Some m1' ->
  inject f g m1' m2.

Lemma free_list_left_inject:
  forall f g m2 l m1 m1',
  inject f g m1 m2 ->
  free_list m1 l = Some m1' ->
  inject f g m1' m2.

Lemma free_right_inject:
  forall f g m1 m2 b lo hi m2',
  inject f g m1 m2 ->
  free m2 b lo hi = Some m2' ->
  (forall b1 delta ofs k p,
    f b1 = Some(b, delta) -> perm m1 b1 ofs k p ->
    lo <= ofs + delta < hi -> False) ->
  inject f g m1 m2'.

Lemma perm_free_list:
  forall l m m' b ofs k p,
  free_list m l = Some m' ->
  perm m' b ofs k p ->
  perm m b ofs k p /\
  (forall lo hi, In (b, lo, hi) l -> lo <= ofs < hi -> False).

Theorem free_inject:
  forall f g m1 l m1' m2 b lo hi m2',
  inject f g m1 m2 ->
  free_list m1 l = Some m1' ->
  free m2 b lo hi = Some m2' ->
  (forall b1 delta ofs k p,
    f b1 = Some(b, delta) ->
    perm m1 b1 ofs k p -> lo <= ofs + delta < hi ->
    exists lo1, exists hi1, In (b1, lo1, hi1) l /\ lo1 <= ofs < hi1) ->
  inject f g m1' m2'.

Theorem free_parallel_inject:
  forall f g m1 m2 b lo hi m1' b' delta,
  inject f g m1 m2 ->
  free m1 b lo hi = Some m1' ->
  f b = Some(b', delta) ->
  inject_perm_condition Freeable ->
  exists m2',
     free m2 b' (lo + delta) (hi + delta) = Some m2'
  /\ inject f g m1' m2'.

Lemma drop_parallel_inject:
  forall f g m1 m2 b1 b2 delta lo hi p m1',
  inject f g m1 m2 ->
  inject_perm_condition Freeable ->
  drop_perm m1 b1 lo hi p = Some m1' ->
  f b1 = Some(b2, delta) ->
  exists m2',
      drop_perm m2 b2 (lo + delta) (hi + delta) p = Some m2'
   /\ inject f g m1' m2'.

Lemma drop_parallel_weak_inject:
  forall f g m1 m2 b1 b2 delta lo hi p m1',
  weak_inject f g m1 m2 ->
  inject_perm_condition Freeable ->
  drop_perm m1 b1 lo hi p = Some m1' ->
  f b1 = Some(b2, delta) ->
  exists m2',
      drop_perm m2 b2 (lo + delta) (hi + delta) p = Some m2'
   /\ weak_inject f g m1' m2'.

Lemma drop_extended_parallel_inject:
  forall f g m1 m2 b1 b2 delta lo1 hi1 lo2 hi2 p m1',
  inject f g m1 m2 ->
  inject_perm_condition Freeable ->
  drop_perm m1 b1 lo1 hi1 p = Some m1' ->
  f b1 = Some(b2, delta) ->
  lo2 <= lo1 -> hi1 <= hi2 ->
  range_perm m2 b2 (lo2 + delta) (hi2 + delta) Cur Freeable ->
  (forall b' delta' ofs' k p,
    f b' = Some(b2, delta') ->
    perm m1 b' ofs' k p ->
    ((lo2 + delta <= ofs' + delta' < lo1 + delta )
     \/ (hi1 + delta <= ofs' + delta' < hi2 + delta)) -> False) ->
  exists m2',
      drop_perm m2 b2 (lo2 + delta) (hi2 + delta) p = Some m2'
   /\ inject f g m1' m2'.

Lemma drop_extended_parallel_weak_inject:
  forall f g m1 m2 b1 b2 delta lo1 hi1 lo2 hi2 p m1',
  weak_inject f g m1 m2 ->
  inject_perm_condition Freeable ->
  drop_perm m1 b1 lo1 hi1 p = Some m1' ->
  f b1 = Some(b2, delta) ->
  lo2 <= lo1 -> hi1 <= hi2 ->
  range_perm m2 b2 (lo2 + delta) (hi2 + delta) Cur Freeable ->
  (forall b' delta' ofs' k p,
    f b' = Some(b2, delta') ->
    perm m1 b' ofs' k p ->
    ((lo2 + delta <= ofs' + delta' < lo1 + delta )
     \/ (hi1 + delta <= ofs' + delta' < hi2 + delta)) -> False) ->
  exists m2',
      drop_perm m2 b2 (lo2 + delta) (hi2 + delta) p = Some m2'
   /\ weak_inject f g m1' m2'.


Lemma drop_outside_inject: forall f g m1 m2 b lo hi p m2',
  inject f g m1 m2 ->
  drop_perm m2 b lo hi p = Some m2' ->
  (forall b' delta ofs k p,
    f b' = Some(b, delta) ->
    perm m1 b' ofs k p -> lo <= ofs + delta < hi -> False) ->
  inject f g m1 m2'.

Lemma drop_right_inject: forall f g m1 m2 b lo hi p m2',
  inject f g m1 m2 ->
  drop_perm m2 b lo hi p = Some m2' ->
  (forall b' delta ofs' k p',
    f b' = Some(b, delta) ->
    perm m1 b' ofs' k p' ->
    lo <= ofs' + delta < hi -> p' = p) ->
  inject f g m1 m2'.



Lemma zero_delta_inject f g m1 m2:
  (forall b1 b2 delta, f b1 = Some (b2, delta) -> delta = 0) ->
  (forall b1 b2, f b1 = Some (b2, 0) -> Mem.valid_block m1 b1 /\ Mem.valid_block m2 b2) ->
  (forall b1 p, f b1 = Some p -> forall b2, f b2 = Some p -> b1 = b2) ->
  (forall b1 b2,
     f b1 = Some (b2, 0) ->
     forall o k p,
       Mem.perm m1 b1 o k p ->
       inject_perm_condition p ->
       Mem.perm m2 b2 o k p) ->
  (forall b1 b2,
     f b1 = Some (b2, 0) ->
     forall o k p,
       Mem.perm m2 b2 o k p ->
       Mem.perm m1 b1 o k p \/ ~ Mem.perm m1 b1 o Max Nonempty) ->
  (forall b1 b2,
     f b1 = Some (b2, 0) ->
     forall o v1,
       loadbytes m1 b1 o 1 = Some (v1 :: nil) ->
       exists v2,
         loadbytes m2 b2 o 1 = Some (v2 :: nil) /\
         memval_inject f v1 v2) ->
  stack_inject f g (perm m1) (stack m1) (stack m2) ->
  Mem.inject f g m1 m2.


Lemma wf_stack_mem m:
  wf_stack (perm m) (stack m).

Lemma stack_inject_aux_flat:
  forall s P f (F: forall b, f b = None \/ f b = Some (b, 0)),
    stack_inject_aux f P (flat_frameinj (length s)) s s.

Lemma self_inject f m:
  (forall b, f b = None \/ f b = Some (b, 0)) ->
  (forall b, f b <> None -> Mem.valid_block m b) ->
  (forall b,
     f b <> None ->
     forall o b' o' q n,
       loadbytes m b o 1 = Some (Fragment (Vptr b' o') q n :: nil) ->
       f b' <> None) ->
  Mem.inject f (flat_frameinj (length (stack m))) m m.


Lemma mem_inj_compose:
  forall f f' g g' m1 m2 m3,
    mem_inj f g m1 m2 -> mem_inj f' g' m2 m3 ->
    forall g2 , compose_frameinj g g' = Some g2 ->
    mem_inj (compose_meminj f f') g2 m1 m3.

Theorem inject_compose:
  forall f f' g g' m1 m2 m3,
    inject f g m1 m2 -> inject f' g' m2 m3 ->
    forall g2 , compose_frameinj g g' = Some g2 ->
    inject (compose_meminj f f') g2 m1 m3.

Lemma val_lessdef_inject_compose:
  forall f v1 v2 v3,
  Val.lessdef v1 v2 -> Val.inject f v2 v3 -> Val.inject f v1 v3.

Lemma val_inject_lessdef_compose:
  forall f v1 v2 v3,
  Val.inject f v1 v2 -> Val.lessdef v2 v3 -> Val.inject f v1 v3.

Lemma lt_lt_eq:
  (forall a b, a = b <-> (forall i, i < a <-> i < b))%nat.

Lemma take_flat_frameinj:
  forall a b,
    take a (flat_frameinj (a + b)) = Some (flat_frameinj a).

Lemma drop_flat_frameinj:
  forall a b,
    drop a (flat_frameinj (a + b)) = flat_frameinj b.

Lemma sum_list_flat:
  forall a,
    sum_list (flat_frameinj a) = a.

Lemma compose_frameinj_flat:
  forall g,
    compose_frameinj (flat_frameinj (sum_list g)) g = Some g.

Lemma compose_frameinj_flat':
  forall g,
    compose_frameinj g (flat_frameinj (length g)) = Some g.

Lemma compose_frameinj_same:
  forall g,
    compose_frameinj (flat_frameinj g) (flat_frameinj g) = Some (flat_frameinj g).

Lemma extends_inject_compose:
  forall f g m1 m2 m3,
  extends m1 m2 -> inject f g m2 m3 -> inject f g m1 m3.

Lemma inject_extends_compose:
  forall f g m1 m2 m3,
    inject f g m1 m2 -> extends m2 m3 -> inject f g m1 m3.

Lemma extends_extends_compose:
  forall m1 m2 m3,
  extends m1 m2 -> extends m2 m3 -> extends m1 m3.

Remark flat_inj_no_overlap:
  forall thr m, meminj_no_overlap (flat_inj thr) m.

Theorem neutral_inject:
  forall m, inject_neutral (nextblock m) m -> inject (flat_inj (nextblock m)) (flat_frameinj (length (stack m))) m m.

Theorem empty_inject_neutral:
  forall thr, inject_neutral thr empty.

Theorem alloc_inject_neutral:
  forall thr m lo hi b m',
  alloc m lo hi = (m', b) ->
  inject_neutral thr m ->
  Plt (nextblock m) thr ->
  inject_neutral thr m'.

Theorem store_inject_neutral:
  forall chunk m b ofs v m' thr,
  store chunk m b ofs v = Some m' ->
  inject_neutral thr m ->
  Plt b thr ->
  Val.inject (flat_inj thr) v v ->
  inject_neutral thr m'.

Theorem drop_inject_neutral:
  forall m b lo hi p m' thr,
  drop_perm m b lo hi p = Some m' ->
  inject_neutral thr m ->
  Plt b thr ->
  inject_neutral thr m'.

Invariance properties between two memory states

Section UNCHANGED_ON.

Variable P: block -> Z -> Prop.

Lemma unchanged_on_refl:
  forall m, unchanged_on P m m.

Lemma valid_block_unchanged_on:
  forall m m' b,
  unchanged_on P m m' -> valid_block m b -> valid_block m' b.

Lemma perm_unchanged_on:
  forall m m' b ofs k p,
  unchanged_on P m m' -> P b ofs ->
  perm m b ofs k p -> perm m' b ofs k p.

Lemma perm_unchanged_on_2:
  forall m m' b ofs k p,
  unchanged_on P m m' -> P b ofs -> valid_block m b ->
  perm m' b ofs k p -> perm m b ofs k p.

Lemma unchanged_on_trans:
  forall m1 m2 m3, unchanged_on P m1 m2 -> unchanged_on P m2 m3 -> unchanged_on P m1 m3.

Lemma loadbytes_unchanged_on_1:
  forall m m' b ofs n,
  unchanged_on P m m' ->
  valid_block m b ->
  (forall i, ofs <= i < ofs + n -> P b i) ->
  loadbytes m' b ofs n = loadbytes m b ofs n.

Lemma loadbytes_unchanged_on:
  forall m m' b ofs n bytes,
  unchanged_on P m m' ->
  (forall i, ofs <= i < ofs + n -> P b i) ->
  loadbytes m b ofs n = Some bytes ->
  loadbytes m' b ofs n = Some bytes.

Lemma load_unchanged_on_1:
  forall m m' chunk b ofs,
  unchanged_on P m m' ->
  valid_block m b ->
  (forall i, ofs <= i < ofs + size_chunk chunk -> P b i) ->
  load chunk m' b ofs = load chunk m b ofs.

Lemma load_unchanged_on:
  forall m m' chunk b ofs v,
  unchanged_on P m m' ->
  (forall i, ofs <= i < ofs + size_chunk chunk -> P b i) ->
  load chunk m b ofs = Some v ->
  load chunk m' b ofs = Some v.

Lemma store_unchanged_on:
  forall chunk m b ofs v m',
  store chunk m b ofs v = Some m' ->
  (forall i, ofs <= i < ofs + size_chunk chunk -> ~ P b i) ->
  unchanged_on P m m'.

Lemma storebytes_unchanged_on:
  forall m b ofs bytes m',
  storebytes m b ofs bytes = Some m' ->
  (forall i, ofs <= i < ofs + Z_of_nat (length bytes) -> ~ P b i) ->
  unchanged_on P m m'.

Lemma alloc_unchanged_on:
  forall m lo hi m' b,
  alloc m lo hi = (m', b) ->
  unchanged_on P m m'.

Lemma free_unchanged_on:
  forall m b lo hi m',
  free m b lo hi = Some m' ->
  (forall i, lo <= i < hi -> ~ P b i) ->
  unchanged_on P m m'.

Lemma drop_perm_unchanged_on:
  forall m b lo hi p m',
  drop_perm m b lo hi p = Some m' ->
  (forall i, lo <= i < hi -> ~ P b i) ->
  unchanged_on P m m'.


End UNCHANGED_ON.

Lemma unchanged_on_implies:
  forall (P Q: block -> Z -> Prop) m m',
  unchanged_on P m m' ->
  (forall b ofs, Q b ofs -> valid_block m b -> P b ofs) ->
  unchanged_on Q m m'.


Lemma inject_unchanged_on j g m0 m m' :
   inject j g m0 m ->
   unchanged_on
     (fun (b : block) (ofs : Z) =>
        exists (b0 : block) (delta : Z),
          j b0 = Some (b, delta) /\
          perm m0 b0 (ofs - delta) Max Nonempty) m m' ->
   stack m' = stack m ->
   inject j g m0 m' .


Lemma unrecord_stack_block_mem_unchanged:
  mem_unchanged (fun m1 m2 => unrecord_stack_block m1 = Some m2).

Lemma unrecord_stack:
   forall m m',
     unrecord_stack_block m = Some m' ->
     exists b,
       stack m = b :: stack m'.

Lemma stack_eq_get_frame_info:
  forall m m' b,
    stack m = stack m' ->
    get_frame_info (stack m) b = get_frame_info (stack m') b.

Lemma stack_eq_is_stack_top:
  forall m m' b,
    stack m = stack m' ->
    is_stack_top (stack m) b <-> is_stack_top (stack m') b.

Lemma record_stack_blocks_mem_unchanged:
  forall f, mem_unchanged (fun m1 m2 => record_stack_blocks m1 f = Some m2).

Lemma unrecord_stack_block_succeeds:
   forall m b r,
     stack m = b :: r ->
     exists m',
       unrecord_stack_block m = Some m'
       /\ stack m' = r.

Lemma inject_stack:
   forall f g m1 m2,
     inject f g m1 m2 ->
     stack_inject f g (perm m1) (stack m1) (stack m2).

Lemma extends_stack:
   forall m1 m2,
     extends m1 m2 ->
     stack_inject inject_id (flat_frameinj (length (stack m1))) (perm m1) (stack m1) (stack m2).

Lemma public_stack_access_inj:
  forall f g m1 m2 b1 b2 delta lo hi p
    (MINJ : mem_inj f g m1 m2)
    (FB : f b1 = Some (b2, delta))
    (RP: range_perm m1 b1 lo hi Cur p)
    (IPC: inject_perm_condition p)
    (NPSA: public_stack_access (stack m1) b1 lo hi),
    public_stack_access (stack m2) b2 (lo + delta) (hi + delta).

Lemma public_stack_access_extends:
   forall m1 m2 b lo hi p,
     extends m1 m2 ->
     range_perm m1 b lo hi Cur p ->
     inject_perm_condition p ->
     public_stack_access (stack m1) b lo hi ->
     public_stack_access (stack m2) b lo hi.

Lemma public_stack_access_inject:
   forall f g m1 m2 b b' delta lo hi p,
     f b = Some (b', delta) ->
     inject f g m1 m2 ->
     public_stack_access (stack m1) b lo hi ->
     range_perm m1 b lo hi Cur p ->
     inject_perm_condition p ->
     public_stack_access (stack m2) b' (lo + delta) (hi + delta).

Open Scope nat_scope.

Definition packed_frameinj (g: nat -> option nat) (s1 s2: nat) :=
  forall j,
    j < s2 ->
    exists lo hi,
      lo < hi <= s1 /\ (forall o, lo <= o < hi <-> g o = Some j).


Lemma stack_inject_unrecord_left:
  forall j n g m1 s1 s2
    (SI: stack_inject j (S n :: g) m1 s1 s2)
    (LE: (1 <= n)%nat)
    (TOPNOPERM: top_tframe_prop (fun tf => forall b, in_frames tf b -> forall o k p, ~ m1 b o k p) s1)
    f l
    (STK1 : s1 = f :: l),
    stack_inject j (n :: g) m1 l s2.

Lemma unrecord_stack_block_mem_inj_left:
  forall (m1 m1' m2 : mem) (j : meminj) n g,
    mem_inj j (S n :: g) m1 m2 ->
    unrecord_stack_block m1 = Some m1' ->
    (1 <= n)%nat ->
    top_frame_no_perm m1 ->
    mem_inj j (n :: g) m1' m2.

Lemma unrecord_stack_block_mem_inj_parallel:
  forall (m1 m1' m2 : mem) (j : meminj) g
    (MINJ: mem_inj j (1%nat :: g) m1 m2)
    (USB: unrecord_stack_block m1 = Some m1'),
  exists m2',
    unrecord_stack_block m2 = Some m2' /\
    mem_inj j g m1' m2'.

Lemma unrecord_stack_block_magree:
    forall m1 m2 P m1',
      magree m1 m2 P ->
      unrecord_stack_block m1 = Some m1' ->
      exists m2',
        unrecord_stack_block m2 = Some m2' /\
        magree m1' m2' P.



Lemma loadbytes_push:
  forall m b o n,
    Mem.loadbytes (Mem.push_new_stage m) b o n = Mem.loadbytes m b o n.

Lemma unrecord_stack_block_inject_left:
  forall (m1 m1' m2 : mem) (j : meminj) n g,
    inject j (S n :: g) m1 m2 ->
    unrecord_stack_block m1 = Some m1' ->
    1 <= n ->
    top_frame_no_perm m1 ->
    inject j (n :: g) m1' m2.

Lemma unrecord_stack_block_inject_parallel:
  forall (m1 m1' m2 : mem) (j : meminj) g,
    inject j (1 :: g) m1 m2 ->
    unrecord_stack_block m1 = Some m1' ->
    exists m2',
      unrecord_stack_block m2 = Some m2' /\
      inject j g m1' m2'.

Lemma unrecord_stack_block_inject_parallel_flat:
  forall (m1 m1' m2 : mem) (j : meminj),
    inject j (flat_frameinj (length (Mem.stack m1))) m1 m2 ->
    unrecord_stack_block m1 = Some m1' ->
    exists m2',
      unrecord_stack_block m2 = Some m2' /\
      inject j (flat_frameinj (length (Mem.stack m1'))) m1' m2'.

Lemma unrecord_stack_block_extends:
    forall m1 m2 m1',
      extends m1 m2 ->
      unrecord_stack_block m1 = Some m1' ->
      exists m2',
        unrecord_stack_block m2 = Some m2' /\
        extends m1' m2'.

Lemma valid_frame_extends:
  forall m1 m2 fi,
    extends m1 m2 ->
    valid_frame fi m1 ->
    valid_frame fi m2.

Lemma record_stack_inject:
  forall j g m1 s1 s2
    (SI : stack_inject j g m1 s1 s2)
    f1 f2
    (FI : frame_inject j f1 f2)
    (INF : forall (b1 b2 : block) (delta : Z), j b1 = Some (b2, delta) -> in_frame f1 b1 <-> in_frame f2 b2)
    (EQsz : frame_adt_size f1 = frame_adt_size f2)
    s1' s2'
    (PREP1: prepend_to_current_stage f1 s1 = Some s1')
    (PREP2: prepend_to_current_stage f2 s2 = Some s2'),
    stack_inject j
                 g
                 m1
                 s1' s2'.

Lemma stack_inject_push_new_stage:
  forall j g P s1 s2,
    stack_inject j g P s1 s2 ->
    stack_inject j (1 :: g) P ((None,nil)::s1) ((None,nil)::s2).

Lemma stack_inject_push_new_stage_left:
  forall j n g P s1 s2,
    stack_inject j (n::g) P s1 s2 ->
    stack_inject j (S n::g) P ((None,nil)::s1) s2.

Lemma mem_inj_push_new_stage:
  forall j g m1 m2,
    mem_inj j g m1 m2 ->
    mem_inj j (1 :: g) (push_new_stage m1) (push_new_stage m2).

Lemma mem_inj_push_new_stage_left:
  forall j n g m1 m2,
    mem_inj j (n :: g) m1 m2 ->
    mem_inj j (S n :: g) (push_new_stage m1) m2.

Lemma mem_inj_push_new_stage_right:
  forall j n g m1 m2,
    mem_inj j (S n :: g) m1 m2 ->
    top_tframe_tc (stack m1) ->
    1 <= n ->
    mem_inj j (1 :: n :: g) m1 (push_new_stage m2).

Lemma inject_push_new_stage_right:
  forall j n g m1 m2,
    inject j (S n :: g) m1 m2 ->
    top_tframe_tc (stack m1) ->
    1 <= n ->
    inject j (1 :: n :: g) m1 (push_new_stage m2).

Lemma inject_push_new_stage:
  forall j g m1 m2,
    inject j g m1 m2 ->
    inject j (1 :: g) (push_new_stage m1) (push_new_stage m2).

Lemma extends_push_new_stage:
  forall m1 m2,
    extends m1 m2 ->
    extends (push_new_stage m1) (push_new_stage m2).

Lemma magree_push_new_stage:
  forall m1 m2 P,
    magree m1 m2 P ->
    magree (push_new_stage m1) (push_new_stage m2) P.

Lemma push_new_stage_mem_unchanged:
  mem_unchanged (fun m1 m2 => push_new_stage m1 = m2).

Lemma tailcall_stage_mem_unchanged:
  mem_unchanged (fun m1 m2 => tailcall_stage m1 = Some m2).

Lemma inject_push_new_stage_left:
  forall j n g m1 m2,
    inject j (n :: g) m1 m2 ->
    inject j (S n :: g) (push_new_stage m1) m2.

Lemma tailcall_stage_perm:
  forall m1 m2,
    tailcall_stage m1 = Some m2 ->
    forall b o k p,
      Mem.perm m2 b o k p <-> Mem.perm m1 b o k p.

Lemma tailcall_stage_nextblock:
  forall m1 m2,
    tailcall_stage m1 = Some m2 ->
    Mem.nextblock m2 = Mem.nextblock m1.

Lemma inject_incr_spec:
  forall j1 j2 b1 b2 delta,
    inject_incr j1 j2 ->
    j2 b1 = Some (b2, delta) ->
    j1 b1 = None \/ j1 b1 = Some (b2, delta).

Lemma stack_inject_mem_inj:
  forall j1 g1 m1 m2 g2 m3 m4
    (MINJ: mem_inj j1 g1 m1 m2)
    (SINJ: stack_inject j1 g1 (perm m1) (stack m1) (stack m2) ->
           stack_inject j1 g2 (perm m3) (stack m3) (stack m4))
    (PERMINJ2: forall b o k p, perm m2 b o k p -> perm m4 b o k p)
    (PERMINJ1: forall b o k p, perm m3 b o k p -> perm m1 b o k p)
    (CONTENTS1: mem_contents m1 = mem_contents m3)
    (CONTENTS2: mem_contents m2 = mem_contents m4),
    mem_inj j1 g2 m3 m4.

Lemma stack_inject_inject:
  forall j1 g1 m1 m2 g2 m3 m4
    (MINJ: inject j1 g1 m1 m2)
    (SINJ: stack_inject j1 g1 (perm m1) (stack m1) (stack m2) ->
           stack_inject j1 g2 (perm m3) (stack m3) (stack m4))
    (PERMINJ2: forall b o k p, perm m2 b o k p <-> perm m4 b o k p)
    (PERMINJ1: forall b o k p, perm m3 b o k p <-> perm m1 b o k p)
    (CONTENTS1: mem_contents m1 = mem_contents m3)
    (CONTENTS2: mem_contents m2 = mem_contents m4)
    (NB1: nextblock m1 = nextblock m3)
    (NB2: nextblock m2 = nextblock m4),
    inject j1 g2 m3 m4.


Lemma tailcall_stage_tc:
  forall m1 m2,
    tailcall_stage m1 = Some m2 ->
    top_tframe_tc (stack m2).

Lemma tailcall_stage_tl_stack:
  forall m1 m2,
    tailcall_stage m1 = Some m2 ->
    tl (Mem.stack m2) = tl (Mem.stack m1).


Lemma stack_inject_aux_tailcall_stage_gen:
  forall j g (m: perm_type) o1 l1 s1 o2 l2 s2 (m': perm_type),
    (forall b1 b2 delta o k p, j b1 = Some (b2, delta) -> m b1 o k p ->
                          inject_perm_condition p ->
                          m' b2 (o + delta)%Z k p) ->
    top_tframe_prop (fun tf => forall b, in_frames tf b -> forall o k p, ~ m' b o k p) ((o2, l2)::s2) ->
    stack_inject_aux j m g ((o1,l1)::s1) ((o2, l2)::s2) ->
    stack_inject_aux j m g ((None, opt_cons o1 l1)::s1) ((None, opt_cons o2 l2)::s2).

Lemma stack_inject_tailcall_stage_gen:
  forall j g (m: perm_type) f1 l1 s1 f2 l2 s2 (m': perm_type),
    (forall b1 b2 delta o k p, j b1 = Some (b2, delta) -> m b1 o k p ->
                          inject_perm_condition p ->
                          m' b2 (o + delta)%Z k p) ->
    top_tframe_prop (fun tf => forall b, in_frames tf b -> forall o k p, ~ m' b o k p) ((f2, l2)::s2) ->
    stack_inject j g m ((f1,l1)::s1) ((f2, l2)::s2) ->
    stack_inject j g m ((None, opt_cons f1 l1)::s1) ((None, opt_cons f2 l2)::s2).

Lemma stack_inject_tailcall_stage_gen':
  forall j g m m' ,
    (forall (b1 b2 : block) (delta o : Z) (k : perm_kind) (p : permission),
        j b1 = Some (b2, delta) -> perm m b1 o k p ->
        inject_perm_condition p ->
        perm m' b2 (o + delta)%Z k p) ->
    top_frame_no_perm m' ->
    forall s1' s2',
      tailcall_stage_stack m = Some s1' ->
      tailcall_stage_stack m' = Some s2' ->
      stack_inject j g (perm m) (stack m) (stack m') ->
      stack_inject j g (perm m) s1' s2'.

Lemma tailcall_stage_extends:
  forall m1 m2 m1',
    Mem.extends m1 m2 ->
    Mem.tailcall_stage m1 = Some m1' ->
    top_frame_no_perm m2 ->
    exists m2',
      Mem.tailcall_stage m2 = Some m2' /\ Mem.extends m1' m2'.


Lemma tailcall_stage_magree:
    forall m1 m2 P m1',
      magree m1 m2 P ->
      tailcall_stage m1 = Some m1' ->
      top_frame_no_perm m2 ->
      exists m2',
        tailcall_stage m2 = Some m2' /\
        magree m1' m2' P.

Lemma tailcall_stage_inject:
  forall j g m1 m2 m1',
    Mem.inject j g m1 m2 ->
    Mem.tailcall_stage m1 = Some m1' ->
    top_frame_no_perm m2 ->
    exists m2',
      Mem.tailcall_stage m2 = Some m2' /\ Mem.inject j g m1' m2'.

Lemma tailcall_stage_stack_equiv:
  forall m1 m2 m1' m2',
    tailcall_stage m1 = Some m1' ->
    tailcall_stage m2 = Some m2' ->
    stack_equiv (stack m1) (stack m2) ->
    stack_equiv (stack m1') (stack m2').

Lemma tailcall_stage_same_length_pos:
  forall m1 m2,
    tailcall_stage m1 = Some m2 ->
    length (stack m2) = length (stack m1) /\ lt O (length (stack m1)).

Lemma tailcall_stage_stack_eq:
  forall m1 m2,
    tailcall_stage m1 = Some m2 ->
    exists f r,
      stack m1 = f :: r /\ stack m2 = (None, opt_cons (fst f) (snd f))::r.



Lemma stack_inject_aux_new_stage_left_tailcall_right:
  forall j n g m t1 s1 t2 s2,
    (forall a l,
        take (n) (t1::s1) = Some l ->
        In a l ->
        tframe_inject j m a t2 -> forall b, in_frames a b ->
                                                   forall o k p , ~ m b o k p) ->
    stack_inject_aux j m (n::g) (t1::s1) (t2::s2) ->
    stack_inject_aux j m (S n :: g) ((None,nil)::t1::s1) ((None,opt_cons (fst t2) (snd t2))::s2).

Lemma stack_inject_new_stage_left_tailcall_right:
  forall j n g m t1 s1 t2 s2,
    (forall a l,
        take (n) (t1::s1) = Some l ->
        In a l -> tframe_inject j m a t2 -> forall b, in_frames a b ->
                                        forall o k p , ~ m b o k p) ->
    stack_inject j (n::g) m (t1::s1) (t2::s2) ->
    stack_inject j (S n :: g) m ((None,nil)::t1::s1) ((None,opt_cons (fst t2) (snd t2))::s2).

Lemma inject_new_stage_left_tailcall_right:
  forall j n g m1 m2,
    inject j (n :: g) m1 m2 ->
    (forall l, take ( n) (stack m1) = Some l ->
          Forall (fun tf => forall b, in_frames tf b -> forall o k p, ~ perm m1 b o k p) l) ->
    top_frame_no_perm m2 ->
    exists m2',
      tailcall_stage m2 = Some m2' /\
      inject j (S n :: g) (push_new_stage m1) m2'.

Lemma inject_tailcall_leftnew_stage_right:
  forall (j : meminj) (n : nat) (g : list nat) (m1 m2 m1' : mem),
    Mem.inject j (S n :: g) m1 m2 ->
    lt O n ->
    tailcall_stage m1 = Some m1' ->
    Mem.inject j (1%nat:: n :: g) m1' (Mem.push_new_stage m2).

Lemma tailcall_stage_inject_left:
  forall j n g m1 m2 m1',
    Mem.inject j (n :: g) m1 m2 ->
    Mem.tailcall_stage m1 = Some m1' ->
    Mem.inject j (n::g) m1' m2.

Lemma tailcall_stage_right_extends:
  forall m1 m2 (EXT: Mem.extends m1 m2)
    (TFNP1: Mem.top_frame_no_perm m1)
    (TFNP2: Mem.top_frame_no_perm m2),
  exists m2', Mem.tailcall_stage m2 = Some m2' /\ Mem.extends m1 m2'.
      

Lemma record_stack_blocks_mem_inj:
    forall j g m1 m2 f1 f2 m1',
      mem_inj j g m1 m2 ->
      record_stack_blocks m1 f1 = Some m1' ->
      frame_inject j f1 f2 ->
      valid_frame f2 m2 ->
      (forall b, in_stack (stack m2) b -> ~ in_frame f2 b) ->
      frame_agree_perms (perm m2) f2 ->
      top_tframe_tc (stack m2) ->
      (forall b1 b2 delta, j b1 = Some (b2, delta) -> in_frame f1 b1 <-> in_frame f2 b2) ->
      frame_adt_size f1 = frame_adt_size f2 ->
      (size_stack (tl (stack m2)) <= size_stack (tl (stack m1)))%Z ->
      exists m2',
        record_stack_blocks m2 f2 = Some m2'
        /\ mem_inj j g m1' m2'.

Lemma record_stack_inject_left':
  forall j g m1 s1 s2
    (SI : stack_inject j g m1 s1 s2)
    f1 f2
    (FAP: frame_at_pos s2 O f2)
    (FI : tframe_inject j m1 (Some f1,nil) f2)
    s1'
    (PREP: prepend_to_current_stage f1 s1 = Some s1'),
    stack_inject j g m1 s1' s2.

Lemma record_stack_blocks_mem_inj_left':
    forall j g m1 m2 f1 f2 m1',
      mem_inj j g m1 m2 ->
      record_stack_blocks m1 f1 = Some m1' ->
      frame_at_pos (stack m2) O f2 ->
      tframe_inject j (perm m1) (Some f1,nil) f2 ->
      mem_inj j g m1' m2.

Lemma record_stack_blocks_valid:
  forall m1 fi m2,
    record_stack_blocks m1 fi = Some m2 ->
    valid_frame fi m1.

Lemma record_stack_blocks_bounds:
  forall m1 fi m2,
    record_stack_blocks m1 fi = Some m2 ->
    frame_agree_perms (perm m1) fi.

Lemma record_stack_blocks_stack:
  forall m f m' of1 s1,
    record_stack_blocks m f = Some m' ->
    stack m = of1::s1 ->
    stack m' = (Some f, snd of1)::s1.

Lemma record_stack_blocks_stack_original:
  forall m f m',
    record_stack_blocks m f = Some m' ->
    exists f r, stack m = (None,f)::r.

Lemma record_stack_blocks_stack':
  forall m f m',
    record_stack_blocks m f = Some m' ->
    exists f1 r, stack m = (None, f1)::r /\ stack m' = (Some f,f1)::r.

Lemma record_stack_blocks_extends:
    forall m1 m2 fi m1',
      extends m1 m2 ->
      record_stack_blocks m1 fi = Some m1' ->
      (forall bb, in_frame fi bb -> ~ in_stack (stack m2) bb) ->
      frame_agree_perms (perm m2) fi ->
      top_tframe_tc (stack m2) ->
      (size_stack (tl (stack m2)) <= size_stack (tl (stack m1)))%Z ->
      exists m2',
        record_stack_blocks m2 fi = Some m2'
        /\ extends m1' m2'.

Lemma free_list_stack_blocks:
    forall bl m m',
      free_list m bl = Some m' ->
      stack m' = stack m.

Lemma in_frames_valid:
  forall m b,
    in_stack (stack m) b -> valid_block m b.

Lemma record_stack_block_inject:
   forall m1 m1' m2 j g f1 f2
     (INJ: inject j g m1 m2)
     (FI: frame_inject j f1 f2)
     (NOIN: forall b, in_stack (stack m2) b -> ~ in_frame f2 b)
     (VF: valid_frame f2 m2)
     (BOUNDS: frame_agree_perms (perm m2) f2)
     (EQINF: forall (b1 b2 : block) (delta : Z), j b1 = Some (b2, delta) -> in_frame f1 b1 <-> in_frame f2 b2)
     (EQsz: frame_adt_size f1 = frame_adt_size f2)
     (TTNP: top_tframe_tc (stack m2))
     (RSB: record_stack_blocks m1 f1 = Some m1')
     (SZ: (size_stack (tl (stack m2)) <= size_stack (tl (stack m1)))%Z),
     exists m2',
       record_stack_blocks m2 f2 = Some m2' /\
       inject j g m1' m2'.

Lemma record_stack_block_inject_flat:
   forall m1 m1' m2 j f1 f2
     (INJ: inject j (flat_frameinj (length (Mem.stack m1))) m1 m2)
     (FI: frame_inject j f1 f2)
     (NOIN: forall b, in_stack (stack m2) b -> ~ in_frame f2 b)
     (VF: valid_frame f2 m2)
     (BOUNDS: frame_agree_perms (perm m2) f2)
     (EQINF: forall (b1 b2 : block) (delta : Z), j b1 = Some (b2, delta) -> in_frame f1 b1 <-> in_frame f2 b2)
     (EQsz: frame_adt_size f1 = frame_adt_size f2)
     (TTNP: top_tframe_tc (stack m2))
     (RSB: record_stack_blocks m1 f1 = Some m1')
     (SZ: (size_stack (tl (stack m2)) <= size_stack (tl (stack m1)))%Z),
     exists m2',
       record_stack_blocks m2 f2 = Some m2' /\
       inject j (flat_frameinj (length (Mem.stack m1'))) m1' m2'.

Lemma record_stack_block_inject_left':
   forall m1 m1' m2 j g f1 f2
     (INJ: inject j g m1 m2)
     (FAP: frame_at_pos (stack m2) 0 f2)
     (FI: tframe_inject j (perm m1) (Some f1,nil) f2)
     (RSB: record_stack_blocks m1 f1 = Some m1'),
     inject j g m1' m2.

Lemma public_stack_access_magree: forall P (m1 m2 : mem) (b : block) (lo hi : Z) p,
    magree m1 m2 P ->
    range_perm m1 b lo hi Cur p ->
    inject_perm_condition p ->
    public_stack_access (stack m1) b lo hi ->
    public_stack_access (stack m2) b lo hi.

Lemma inject_frame_flat a thr:
  frame_inject (flat_inj thr) a a.

Lemma record_stack_blocks_sep:
  forall m1 fi m2 ,
    record_stack_blocks m1 fi = Some m2 ->
    forall b : block, in_stack (stack m1) b -> ~ in_frame fi b.

Lemma unrecord_stack_block_inject_neutral:
  forall thr m m',
    inject_neutral thr m ->
    unrecord_stack_block m = Some m' ->
    inject_neutral thr m'.

Lemma store_no_abstract:
  forall (chunk : memory_chunk) (b : block) (o : Z) (v : val),
    stack_unchanged (fun m1 m2 : mem => store chunk m1 b o v = Some m2).

Lemma storebytes_no_abstract:
  forall (b : block) (o : Z) (bytes : list memval),
    stack_unchanged (fun m1 m2 : mem => storebytes m1 b o bytes = Some m2).

Lemma alloc_no_abstract: forall (lo hi : Z) (b : block),
 stack_unchanged (fun m1 m2 : mem => alloc m1 lo hi = (m2, b)).

Lemma free_no_abstract:
 forall (lo hi : Z) (b : block),
 stack_unchanged (fun m1 m2 : mem => free m1 b lo hi = Some m2).

Lemma freelist_no_abstract:
 forall bl : list (block * Z * Z),
 stack_unchanged (fun m1 m2 : mem => free_list m1 bl = Some m2).

Lemma drop_perm_no_abstract:
 forall (b : block) (lo hi : Z) (p : permission),
 stack_unchanged (fun m1 m2 : mem => drop_perm m1 b lo hi p = Some m2).

Lemma record_stack_inject_left_zero:
  forall j n g m1 s1 s2 f1 f2
    (FAP: frame_at_pos s2 0 f2)
    (FI: tframe_inject j m1 f1 f2)
    (SI: stack_inject j (n :: g) m1 s1 s2)
  ,
    stack_inject j (S n :: g) m1 (f1 :: s1) s2.

Lemma record_stack_inject_left_zero':
  forall j g m1 s1 s2 f1 f2 l
    (FAP: frame_at_pos s2 0 f2)
    (FI: tframe_inject j m1 f1 f2)
    (SI: stack_inject j g m1 ((None,l) :: s1) s2),
    stack_inject j g m1 (f1 :: s1) s2.

Lemma record_stack_blocks_mem_inj_left_zero':
  forall j g m1 m2 f1 f2 m1',
    mem_inj j g m1 m2 ->
    record_stack_blocks m1 f1 = Some m1' ->
    frame_at_pos (stack m2) O f2 ->
    tframe_inject j (perm m1) (Some f1,nil) f2 ->
    mem_inj j g m1' m2.

Lemma record_stack_block_inject_left_zero':
  forall m1 m1' m2 j g f1 f2
    (INJ: inject j g m1 m2)
    (FAP: frame_at_pos (stack m2) 0 f2)
    (FI: tframe_inject j (perm m1) (Some f1, nil) f2)
    (RSB: record_stack_blocks m1 f1 = Some m1'),
    inject j g m1' m2.

Lemma unrecord_stack_inject_left_zero:
  forall j n g m1 f s1 s2
    (SI: stack_inject j (S n :: g) m1 (f :: s1) s2)
    (LE: 1 <= n)
    (TOPNOPERM: top_tframe_prop (fun tf => forall b, in_frames tf b -> forall o k p, ~ m1 b o k p) (f::s1)),
    stack_inject j (n :: g) m1 s1 s2.

Lemma unrecord_stack_block_mem_inj_left_zero:
  forall (m1 m1' m2 : mem) (j : meminj) n g,
    mem_inj j (S n :: g) m1 m2 ->
    unrecord_stack_block m1 = Some m1' ->
    top_frame_no_perm m1 ->
    1 <= n ->
    mem_inj j (n :: g) m1' m2.
  
Lemma unrecord_stack_block_inject_left_zero:
  forall (m1 m1' m2 : mem) (j : meminj) n g,
    inject j (S n :: g) m1 m2 ->
    unrecord_stack_block m1 = Some m1' ->
    top_frame_no_perm m1 ->
    1 <= n ->
    inject j (n :: g) m1' m2.

  Lemma mem_inj_ext':
    forall j1 j2 g m1 m2,
      mem_inj j1 g m1 m2 ->
      (forall x, j1 x = j2 x) ->
      mem_inj j2 g m1 m2.

  Lemma mem_inject_ext':
    forall j1 j2 g m1 m2,
      inject j1 g m1 m2 ->
      (forall x, j1 x = j2 x) ->
      inject j2 g m1 m2.

  Lemma mem_inj_unrecord_parallel_frameinj_flat:
    forall j m1 m2
      (MI: mem_inj j (flat_frameinj (length (stack m2))) m1 m2)
      m1'
      (USB: unrecord_stack_block m1 = Some m1')
    ,
    exists m2',
      unrecord_stack_block m2 = Some m2' /\
      mem_inj j (flat_frameinj (pred (length (stack m2)))) m1' m2'.

  Lemma inject_unrecord_parallel_frameinj_flat:
    forall j m1 m2
      (MI: inject j (flat_frameinj (length (stack m2))) m1 m2)
      m1'
      (USB: unrecord_stack_block m1 = Some m1'),
    exists m2',
      unrecord_stack_block m2 = Some m2' /\
      inject j (flat_frameinj (pred (length (stack m2)))) m1' m2'.

  Lemma record_stack_blocks_top_noperm:
    forall m1 f m1',
      record_stack_blocks m1 f = Some m1' ->
      top_tframe_tc (stack m1).

  Lemma in_range:
    forall (a b c : Z),
      (a <= b < c \/ ~ (a <= b < c))%Z.

  Lemma free_perm:
    forall m1 b lo hi m2,
      free m1 b lo hi = Some m2 ->
      forall b' o k p,
        perm m1 b' o k p ->
        if peq b b' then ((lo <= o < hi)%Z) <-> forall k p, ~ perm m2 b' o k p else perm m2 b' o k p.

Lemma record_stack_blocks_inject_neutral:
  forall thr m fi m',
    inject_neutral thr m ->
    record_stack_blocks m fi = Some m' ->
    inject_neutral thr m'.

Lemma unrecord_push:
  forall m, unrecord_stack_block (push_new_stage m) = Some m.















End WITHINJPERM.

Local Instance memory_model_prf:
  MemoryModel mem.

End Mem.

Global Opaque Mem.alloc Mem.free Mem.store Mem.load Mem.storebytes Mem.loadbytes.