Require Import Zwf.
Require Import Axioms.
Require Import Coqlib.
Require Import Fappli_IEEE_bits.
Require Import Psatz.

Require Intv.
Require Import Maps.
Require Archi.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Values_symbolictype.
Require Import Values_symbolic.
Require Export Memtype.
Require Import IntFacts.
Require Import Normalise.
Require Import NormaliseSpec.
Require Export Memdata.
Require Import Alloc Align.
Require Import Permutation.
Require Import ExprEval.
Require Export Memperm TwoPowerFacts.

Parameter MA : nat.
Hypothesis MA_bound: (3 <= MA <= 12)%nat.

Local Unset Elimination Schemes.
Local Unset Case Analysis Schemes.

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

Lemma align_le_two_p:
  forall al al' (AlGt: (al <= al')%nat) x,
    align (align x (two_power_nat al)) (two_power_nat al') = align x (two_power_nat al').


Module Mem <: 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.

Inductive msz := M31 | M32.

Definition comp_size q :=
  match q with
    M31 => Int.max_unsigned - two_power_nat MA
  | M32 => Int.max_unsigned
  end.


Definition __szmem := comp_size M31.

Lemma tpMA_pos:
  two_power_nat MA > 0.


Definition box_span (z:Z) :=
  Z.to_nat ((z - 1) / two_power_nat MA + 1).
Lemma s32_ma:
  Int.max_unsigned = two_power_nat MA * (two_power_nat (32 - MA)) - 1.


Lemma box_span_mul z:
  box_span (two_power_nat MA * z - 1) = Z.to_nat z.

Lemma tpMA_sup8:
  8 <= two_power_nat MA.


Lemma tpMA'_sup8:
  8 <= two_power_nat (32-MA).


Definition nb_boxes_max : Z :=
  two_power_nat (32 - MA) - 2.

Lemma nb_boxes_max_pos:
  0 <= nb_boxes_max.


Record is_block_list (m: PMap.t (option (Z*Z))) (nb: nat) l :=
  {
    ibl_lnr: list_norepet (map fst l);
    ibl_size: forall b sz, In (b, sz) l -> get_size m b = sz;
    ibl_length: length l = nb;
    ibl_valid: forall b, (Pos.to_nat b <= nb)%nat -> In (b, get_size m b) l
  }.

Definition nb_boxes_used (lb: list (block * Z)) :=
  fold_left
    plus
    (map (fun bsz : block * Z =>
         let (b,sz) := bsz in
         box_span sz
      ) lb) O.

Record mem' : Type := mkmem {
  mem_contents: PMap.t (ZMap.t memval); (* block -> offset -> memval *)
  mem_access: PMap.t (Z -> perm_kind -> option permission);
  mem_blocksize: PMap.t (option (Z*Z)); (* block -> option(Z*Z) *)
  mem_mask: PMap.t (option nat); (* block -> option mask; the number of 0-trailing-bits *)
  mem_blocktype: PMap.t (option block_type);
  nextblock: block;
  nb_extra: nat;
  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;
  access_bounds_ok: (* permissions and bounds agree *)
    forall b ofs k,
      (mem_access#b ofs k) <> None
      -> in_bound ofs (get_bounds mem_blocksize b);
  msk_valid: (* only valid blocks have non-empty masks *)
    forall b, ~ (Plt b nextblock) -> mem_mask#b = None;
  blocktype_valid: (* only valid blocks have non-empty masks *)
    forall b, ~ (Plt b nextblock) -> mem_blocktype#b = None;
  wfm_alloc_ok: (* the allocation algorithm succeeds on this memory *)
    Z.of_nat (nb_boxes_used (mk_block_list_aux (get_size mem_blocksize) (pred (Pos.to_nat nextblock))) + nb_extra)%nat < nb_boxes_max;
  alignment_ok:
    forall b al,
      mem_mask#b = Some al -> (al <= MA)%nat /\
                              (al >= alignment_of_size (get_size (mem_blocksize) b))%nat;
  bounds_mask_consistency: (* bounds and masks information are present together, or not at all *)
    forall b,
      mem_mask#b = None -> mem_blocksize#b = None;
  bounds_lo_inf0: (* the lower bound of a block is 0 *)
    forall b lo hi,
      mem_blocksize#b = Some (lo,hi) ->
      lo = 0 /\ hi >= 0
}.

Definition mem := mem'.



Lemma bs_valid: (* only valid blocks have non-empty bounds *)
  forall m b,
    ~ (Plt b m.(nextblock)) ->
    m.(mem_blocksize) # b = None.


Definition size_block (m: mem) (b:block) : Z :=
  get_size (m.(mem_blocksize)) b.

Definition size_of_block (m:mem) (b:block) :=
  match PMap.get b m.(mem_blocksize) with
      | Some (lo,hi) => (Int.repr (hi-lo))
      | None => (Int.repr 0)
  end.

Definition bounds_of_block (m:mem) (b:block) : Z*Z :=
  match PMap.get b m.(mem_blocksize) with
      | Some (lo,hi) => (lo,hi)
      | None => (0,0)
  end.

Definition mask (m:mem) (b:block) :=
  match PMap.get b m.(mem_mask) with
      | Some mask => mask
      | None => O
  end.

Definition nat_mask (m:mem) (b:block) :=
  Int.not (Int.repr (two_power_nat (mask m b) - 1)).

Definition mk_block_list (m:mem) : (list (block * Z)) :=
  mk_block_list_aux (size_block m) (pred (Pos.to_nat (Mem.nextblock m))).

Definition nb_boxes_used_m (m: mem) :=
  (nb_boxes_used (mk_block_list m) + nb_extra m)%nat.





Definition mem_norm (m:mem) (e: expr_sym) : val :=
  Normalise.normalise (bounds_of_block m) (nat_mask m) e.

Definition max_def v e :=
  match v with
    Vundef => e
  | _ => Eval v
  end.

Definition try_norm m e := max_def (mem_norm m e) e.

Lemma same_eval_same_eval_on:
  forall e e' (SE: same_eval e e') P,
    same_eval_on P e e'.

Lemma same_eval_eqm:
  forall m v1 v2,
    same_eval v1 v2 ->
    Mem.mem_norm m v1 = Mem.mem_norm m v2.

Lemma lessdef_eqm:
  forall m v1 v2,
    Val.lessdef v1 v2 ->
    Values.Val.lessdef (mem_norm m v1) (mem_norm m v2).




Definition compat_m (m: mem) (q: msz) :=
  compat (comp_size q) (Mem.bounds_of_block m) (Mem.nat_mask m).

Lemma lessdef_on_P_impl:
  forall (P Q : (block -> int) -> Prop) e e' (LD: lessdef_on P e e') (PQ: forall cm, Q cm -> P cm),
    lessdef_on Q e e'.

Ltac unfsize :=
  IntFacts.unfsize.

Lemma size31_inf:
  comp_size M31 <= Int.max_unsigned.

Lemma fold_left_plus_rew:
  forall l n,
    (fold_left plus l n = fold_left plus l O + n)%nat.


Definition make_box_allocation (lb : list (block * Z)) :=
  fold_right (fun (bsz: block * Z)
                (acc: nat * (block -> nat)) =>
               let '(b, sz) := bsz in
               let '(curbox, curalloc) := acc in
               (curbox + box_span sz,
                fun bb => if peq bb b then curbox else curalloc bb)%nat
             )
             (O, fun _ : block => O)
             lb.

Definition box_alloc_to_cm (ba: block -> nat) (b: block) : int :=
  Int.repr (two_power_nat MA * ((Z.of_nat (ba b)) + 1)).


Lemma make_box_allocation_cons:
  forall b sz r,
  make_box_allocation ((b,sz) :: r) =
  let (cb, ca) := make_box_allocation r in
  (cb + box_span sz,
   fun bb => if peq bb b then cb else ca bb)%nat.


Lemma is_block_list_permut:
  forall sz l l' (PERM: Permutation l l') n
    (IBL: is_block_list sz n l),
    is_block_list sz n l'.

Lemma is_block_list_S:
  forall sz n l
    (IBL': is_block_list sz (S n) l),
  exists l',
    is_block_list sz n l' /\
    Permutation ((Pos.of_nat (S n), get_size sz (Pos.of_nat (S n))) :: l') l.


Lemma is_block_list_is_permut:
  forall sz n l l'
    (IBL: is_block_list sz n l)
    (IBL': is_block_list sz n l')
  ,
    Permutation l l'.

Lemma is_block_list_permut_mk_block_list:
  forall sz n l,
  is_block_list sz n l ->
  Permutation l (mk_block_list_aux (get_size sz) n).

Lemma is_block_list_S':
  forall sz n l l'
    (IBL: is_block_list sz n l)
    (IBL': is_block_list sz (S n) l'),
    Permutation ((Pos.of_nat (S n), get_size sz (Pos.of_nat (S n))) :: l) l'.

Lemma fold_left_plus_permut:
  forall l l' (PERM: Permutation l l') n,
    fold_left plus l n = fold_left plus l' n.

Lemma nb_boxes_used_S:
  forall l l' sz n,
    is_block_list sz n l ->
    is_block_list sz (S n) l' ->
    (nb_boxes_used l' = nb_boxes_used l + box_span (get_size sz (Pos.of_nat (S n))))%nat.

Lemma nb_boxes_used_thr:
  forall l curbox curalloc,
    make_box_allocation l = (curbox, curalloc) ->
    (nb_boxes_used l = curbox)%nat.

Lemma make_box_allocation_le:
  forall l curbox curalloc,
    make_box_allocation l = (curbox, curalloc) ->
    forall b, (curalloc b <= curbox)%nat.

Require Import Tactics.

Lemma make_box_allocation_le_in:
  forall l curbox curalloc,
    list_norepet (map fst l) ->
    make_box_allocation l = (curbox, curalloc) ->
    forall b sz, In (b,sz) l -> (curalloc b + box_span sz <= curbox)%nat.

Lemma make_box_allocation_disjoint:
  forall l cb ca,
    list_norepet (map fst l) ->
    make_box_allocation l = (cb, ca) ->
    forall b1 sz1 b2 sz2 (i1: In (b1, sz1) l) (i2: In (b2, sz2) l)
      (d: b1 <> b2) (pos1: sz1 > 0) (pos2: sz2 > 0),
      (ca b1 + box_span sz1 <= ca b2 \/ ca b2 + box_span sz2 <= ca b1)%nat.

Lemma minus_1_div_eq:
  forall z, z > 0 -> -1 / z = -1.

Lemma box_span_align:
  forall z,
    z >= 0 ->
    two_power_nat MA * Z.of_nat (box_span z) = align z (two_power_nat MA).


Lemma s31_ma:
  comp_size M31 = two_power_nat MA * (two_power_nat (32 - MA) - 1) - 1.

Lemma lt_le_minus1:
  forall a b : Z,
    a < b ->
    a <= b - 1.

Lemma in_bound_in_mk:
  forall o m b l,
    in_bound (Int.unsigned o) (bounds_of_block m b) ->
    is_block_list (mem_blocksize m) (pred (Pos.to_nat (nextblock m))) l ->
    In (b, size_block m b) l /\
    Int.unsigned o < two_power_nat MA * Z.of_nat (box_span (size_block m b)) /\
    size_block m b > 0.

Lemma box_alloc_unsigned_range:
  forall thr m ba
    (THR : (thr < Z.to_nat nb_boxes_max)%nat)
    l
    (IBL: is_block_list (mem_blocksize m) (pred (Pos.to_nat (nextblock m))) l)
    (MBA : make_box_allocation l = (thr, ba)) b o
    (IB : in_bound (Int.unsigned o) (bounds_of_block m b)),
    0 <= two_power_nat MA * (Z.of_nat (ba b) + 1) <= Int.max_unsigned.

Lemma box_alloc_in_range:
  forall thr m ba
    (THR : (thr < Z.to_nat nb_boxes_max)%nat)
    l
    (IBL: is_block_list (mem_blocksize m) (pred (Pos.to_nat (nextblock m))) l)
    (MBA : make_box_allocation l = (thr, ba))
    b o
    (IB : in_bound (Int.unsigned o) (bounds_of_block m b)),
    0 < Int.unsigned (Int.repr (two_power_nat MA * (Z.of_nat (ba b) + 1))) + Int.unsigned o < comp_size M31.

Lemma box_alloc_in_range':
  forall thr m ba
    (THR : (thr < Z.to_nat nb_boxes_max)%nat)
    l
    (IBL: is_block_list (mem_blocksize m) (pred (Pos.to_nat (nextblock m))) l)
    (MBA : make_box_allocation l = (thr, ba))
    b o
    (IB : in_bound (Int.unsigned o) (bounds_of_block m b)),
    0 <= Int.unsigned (Int.repr (two_power_nat MA * (Z.of_nat (ba b) + 1))) + Int.unsigned o <= Int.max_unsigned.

Lemma zlt_neq: forall a b : Z, a < b -> a <> b.

Lemma zgt_neq: forall a b : Z, b < a -> a <> b.

Lemma box_alloc_to_cm_compat:
  forall m thr ba
    (THR: (thr < Z.to_nat nb_boxes_max)%nat)
    l
    (IBL: is_block_list (mem_blocksize m) (pred (Pos.to_nat (nextblock m))) l)
    (MBA: make_box_allocation l = (thr, ba)),
    compat_m m M31 (box_alloc_to_cm ba).

Definition mk_cm l nbe :=
  let (thr,al) := make_box_allocation l in
  if zlt (Z.of_nat (thr + nbe)) nb_boxes_max
  then Some al
  else None.

Lemma nb_used_permut:
  forall l l' (P: Permutation l l'),
    nb_boxes_used l = nb_boxes_used l'.

Lemma alloc_compat:
  forall m l
    (IBL: is_block_list (mem_blocksize m) (pred (Pos.to_nat (nextblock m))) l),
    exists al,
      mk_cm l (nb_extra m) = Some al /\
      compat_m m M31 (box_alloc_to_cm al).

Lemma length_mbla:
  forall sz n, length (mk_block_list_aux sz n) = n.

Lemma is_block_list_mk_block_list:
  forall sz n,
    is_block_list sz n (mk_block_list_aux (get_size sz) n).

Lemma concrete_mem':
  forall m, exists al, compat_m m M31 al.

Lemma compat31_32:
  forall m cm, compat_m m M31 cm -> compat_m m M32 cm.

Lemma concrete_mem:
  forall m, exists al, compat_m m M32 al.


Definition good_result_m m e v :=
  good_result Int.max_unsigned (bounds_of_block m) (nat_mask m) e v.

Record is_norm_m m e v :=
  mkIsNormM {
    eval_ok_m: lessdef_on (compat_m m M32) (Eval v) e
  }.

Lemma norm_complete:
  forall m e v
    (INM: is_norm_m m e v),
    Values.Val.lessdef v (mem_norm m e).

Lemma norm_correct:
  forall m e,
    is_norm_m m e (mem_norm m e).

Lemma norm_ld:
  forall m e v,
    mem_norm m e = v ->
    forall cm em,
      compat_m m M32 cm ->
      Values.Val.lessdef (eSval cm v) (eSexpr cm em e).

Lemma norm_gr:
  forall m e,
    good_result_m m e (mem_norm m e).

Lemma eq_norm:
  forall m e v,
    is_norm_m m e v ->
    v <> Vundef ->
    Mem.mem_norm m e = v.

Lemma same_compat_bounds_mask:
  forall m1 m2
    (Bnds: forall b, bounds_of_block m1 b = bounds_of_block m2 b)
    (Msk: forall b, nat_mask m1 b = nat_mask m2 b)
    cm,
    compat_m m1 M32 cm <-> compat_m m2 M32 cm.

Lemma good_result_m_same_compat:
  forall m m' e v
    (MR: forall cm, compat_m m M32 cm <-> compat_m m' M32 cm),
    good_result_m m e v <->
    good_result_m m' e v.

Lemma is_norm_m_same_compat:
  forall m m' e v
    (C: forall cm, compat_m m M32 cm <-> compat_m m' M32 cm),
    is_norm_m m e v <->
    is_norm_m m' e v.

Lemma norm_same_compat:
  forall m1 m2 e
    (Bnds: forall b, bounds_of_block m1 b = bounds_of_block m2 b)
    (Msk: forall b, nat_mask m1 b = nat_mask m2 b),
    mem_norm m1 e = mem_norm m2 e.


Definition in_bound_m (o: Z) (m: mem) (b: block) : Prop :=
  in_bound o (bounds_of_block m b).

Definition in_bound_m_dec:
  forall o m b,
    in_bound_m o m b \/ ~ in_bound_m o m b.


Definition pair_eq {A B} (eqA: forall (a b : A), {a = b} + {a<>b})
           (eqB: forall (a b: B), {a = b} + {a<>b}) :
  forall (a b : (A*B)),
    {a = b} + {a<>b}.

Definition put_front (bl: list (positive * Z)) (b: positive) (sz: Z) :=
  (b,sz) :: remove (pair_eq peq zeq) (b,sz) bl.

Lemma remove_app:
  forall {A} (eqA: forall (a b : A), {a = b} + {a<>b})
    a l1 l2,
    remove eqA a (l1 ++ l2) = remove eqA a l1 ++ remove eqA a l2.

Lemma remove_not_in:
    forall {A} (eqA: forall (a b : A), {a = b} + {a<>b})
      a l (NIN: ~ In a l),
      remove eqA a l = l.

Lemma put_front_permut:
  forall b sz bl (IN: In (b,sz) bl)
    (LNR: list_norepet bl),
    Permutation bl (put_front bl b sz).

Definition other_cm cm b :=
  fun bb =>
    if peq b bb
    then Int.add (cm b) (Int.repr (two_power_nat MA))
    else cm bb.


Lemma two_power_nat_inf_mod:
  forall x y,
    (x < y)%nat ->
    two_power_nat x = two_power_nat x mod two_power_nat y.


Lemma add_bounded_plus8:
  forall i o
    (H : 0 < Int.unsigned (Int.add i o) < comp_size M31),
    0 < Int.unsigned (Int.add (Int.add i (Int.repr (two_power_nat MA))) o) < Int.max_unsigned.

Lemma i_bounded_plus8:
   forall i : int,
   0 < Int.unsigned i < comp_size M31 ->
   Int.unsigned (Int.add i (Int.repr (two_power_nat MA))) < Int.unsigned i -> False.

Lemma compat_shift:
  forall m cm b
    (LAST: forall b' o o', b <> b' ->
                      in_bound (Int.unsigned o) (bounds_of_block m b) ->
                      in_bound (Int.unsigned o') (bounds_of_block m b') ->
                      Int.unsigned (Int.add (cm b') o') < Int.unsigned (Int.add (cm b) o))
    (COMP : compat_m m M31 cm),
  exists cm',
    cm b <> cm' b /\
    (forall b' (diff: b' <> b), cm b' = cm' b') /\
    compat_m m M32 cm'.

Lemma remove_in:
  forall {A} (eqA: forall (a b: A), {a=b}+{a<>b}) a b l,
    a <> b ->
    In a l ->
    In a (remove eqA b l).

Lemma in_bound_plt:
  forall b m o,
    in_bound o (bounds_of_block m b) ->
    Plt b (nextblock m).

Lemma remove_in_before:
  forall {A} (pdec: forall (a b : A), {a=b}+{a<>b})
    a b l,
    In a (remove pdec b l) ->
    In a l.

Lemma remove_P:
  forall {A B} (pdec: forall (a b : A*B), {a=b}+{a<>b}) f
    (p: A*B) (l: list (A*B))
    (Pr: forall a b, In (a,b) l -> b = f a)
    a b
    (IN:In (a,b) (remove pdec p l)),
    b = f a.


Lemma bounds_lo_0:
  forall m b,
    fst (bounds_of_block m b) = 0.

Lemma in_bound_zero:
  forall o m b,
    in_bound o (bounds_of_block m b) ->
    in_bound (Int.unsigned Int.zero) (bounds_of_block m b).

Lemma compat_add_unsigned:
  forall m cm (COMP: compat_m m M32 cm) b
    o (IB: in_bound (Int.unsigned o) (bounds_of_block m b)),
    Int.unsigned (Int.add (cm b) o) = Int.unsigned (cm b) + Int.unsigned o.

Lemma make_box_allocation_order:
  forall l sz al
    (AMA: make_box_allocation l = (sz,al))
    (lnr: list_norepet (map fst l))
    b b'
    (AB: appears_before b b' (map fst l)),
    (al b' <= al b)%nat.


Lemma map_app_cons {A B}:
  forall (f: A -> B) l fa fb fc,
    map f l = fa ++ fb :: fc ->
    exists a b c, l = a ++ b :: c /\ fa = map f a /\ fb = f b /\ fc = map f c.

Lemma put_front_appears_before:
  forall b sz l b',
    In b' (map fst l) -> b <> b' ->
    appears_before b b' (map fst (put_front l b sz)).

Opaque put_front.

Lemma box_span_pos:
  forall z, z > 0 -> (0 < box_span z)%nat.


Theorem exists_two_cms:
  forall m b,
  exists cm cm' : block -> int,
    compat_m m M32 cm /\
    compat_m m M32 cm' /\
    cm b <> cm' b /\
    forall b', b <> b' -> cm b' = cm' b'.

Lemma norm_val:
  forall m v,
    mem_norm m (Eval v) = v.

Lemma norm_vundef:
  forall m,
    mem_norm m (Eval Vundef) = Vundef.

Lemma same_Eval_norm:
  forall m vn v,
    same_eval vn (Eval v) ->
    Mem.mem_norm m vn = v.

Lemma norm_ptr_same:
  forall m b o b' o',
    Mem.mem_norm m (Eval (Vptr b o)) = Vptr b' o' ->
    Vptr b o = Vptr b' o'.

Lemma norm_type:
  forall m e v t,
    Mem.mem_norm m e = v ->
    v <> Vundef ->
    wt_val v t ->
    wt_expr e t.

Lemma same_val_ofbool_norm:
  forall m vn b,
    same_eval vn (Val.of_bool b) ->
    Mem.mem_norm m vn = Vint (if b then Int.one else Int.zero).

Lemma norm_boolval:
  forall m v i,
    Mem.mem_norm m v = Vint i ->
    Mem.mem_norm m (Val.boolval v) = Values.Val.of_bool (negb (Int.eq i Int.zero)).

Lemma normalise_int_notbool:
  forall m b i,
    Mem.mem_norm m b = Vint i ->
    Mem.mem_norm m (Eunop OpNotbool Tint b) = Vint (Int.notbool i).

Lemma mkmem_ext:
 forall cont1 cont2 acc1 acc2 next1 next2 bt1 bt2 nbe1 nbe2
        a1 a2 b1 b2 bs1 bs2
        mask1 mask2 Pabo1 Pabo2 comp2 comp1 vm1 vm2 vbt1 vbt2
        const1 const2 bb1 bb2
        bli1 bli2,
   cont1=cont2 -> acc1=acc2 -> next1=next2 ->
   bs1=bs2 -> mask1=mask2 -> bt1 = bt2 -> nbe1 = nbe2 ->
   mkmem cont1 acc1 bs1 mask1 bt1 next1 nbe1
         a1 b1 Pabo1 vm1 vbt1
         comp1 bb1 const1 bli1 =
   mkmem cont2 acc2 bs2 mask2 bt2 next2 nbe2
         a2 b2 Pabo2 vm2 vbt2
         comp2 bb2 const2 bli2.

Validity of blocks and accesses

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

Definition valid_block_dec (m:mem) (b:block) : {valid_block m b} + {~ valid_block m b}.

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

Hint Local 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.

Hint Local 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.

Hint Local 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.

Hint Local 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.






Hint Local 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).

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.

Hint Local 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.

Hint Local 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 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

Program Definition empty: mem :=
  mkmem (PMap.init (ZMap.init (Symbolic (Eval (Vint Int.zero)) None O)))
        (PMap.init (fun ofs k => None))
        (PMap.init None)
        (PMap.init None)
        (PMap.init None)
        1%positive O _ _ _ _ _ _ _ _ _.


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.


Lemma memval_rel_lf2:
  forall mr n o t t' b,
    (forall (b0 : positive) (ofs : ZIndexed.t),
       memval_rel mr (ZMap.get ofs t !! b0)
                    (ZMap.get ofs t' !! b0)) ->
    list_forall2 (memval_rel mr)
                 (Mem.getN n o t !! b)
                 (Mem.getN n o t' !! b).

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

  



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) (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.



Require Import Setoid.

Lemma get_setN_inside:
  forall vl ofs lo t,
    lo <= ofs < lo + Z.of_nat (length vl) ->
    Some (ZMap.get ofs (setN vl lo t)) = nth_error vl (Z.to_nat (ofs - lo)).


Lemma same_type_memval_refl:
  forall m,
    same_type_memval m m.

Lemma memval_rel_set:
  forall mr (WF: wf_mr mr) v v' o ofs t b0,
    list_forall2 (memval_rel mr) v v' ->
   memval_rel mr
     (ZMap.get ofs (setN v o t # b0))
     (ZMap.get ofs (setN v' o t # b0)).


Lemma memval_rel_set':
  forall mr v v' ofs o t t' b b0,
    (forall b o, memval_rel mr (ZMap.get o t !! b) ( ZMap.get o t' !! b)) ->
    list_forall2 (memval_rel mr) v v' ->
    memval_rel mr
      (ZMap.get
         ofs
         (PMap.set b (Mem.setN v o t !! b) t) !! b0)
      (ZMap.get
         ofs
         (PMap.set b (Mem.setN v' o t' !! b) t') !! b0).


Fixpoint init_block' (n:nat) (b:block) (cur:int) : list memval :=
  match n with
      O => nil
    | S m => Symbolic ( (Eundef b cur)) None O :: (init_block' m b (Int.add cur (Int.repr 1)))
  end.

Definition init_block (lo hi: Z) (b: block) : memval * PTree.t memval :=
  ZMap.init (Symbolic (Eval Vundef) None O).


Lemma pos_ex_index:
  forall p,
    exists z,
      ZIndexed.index z = p.

Lemma zle_zlt:
  forall a b c,
    zle a b && zlt b c = true <->
    a <= b < c.








Lemma maxspec:
  forall (n m: nat),
    max n m = if lt_dec n m then m else n.

Lemma minspec:
  forall (n m: nat),
    min n m = if lt_dec n m then n else m.

Lemma alignment_of_size_bnd sz:
  (alignment_of_size sz <= 3)%nat.

Opaque min max.
Program Definition low_alloc (m: mem) (lo hi: Z) (al: nat) bt : option (mem * block) :=
  let lo := 0 in
  let al := (min MA (max al (alignment_of_size (hi-lo)))) in
  if zlt (Z.of_nat (nb_boxes_used_m m + box_span (Z.max 0 hi))) nb_boxes_max
  then
    Some (mkmem (PMap.set m.(nextblock)
                              (init_block lo hi m.(nextblock))
                              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))
                (PMap.set m.(nextblock)
                              (Some (0,Z.max 0 hi))
                              m.(mem_blocksize))
                (PMap.set m.(nextblock)
                              (Some al)
                              m.(mem_mask))
                (PMap.set m.(nextblock)
                              (Some bt)
                              m.(mem_blocktype))
                (Psucc m.(nextblock)) (nb_extra m)
                _ _ _ _ _ _ _ _ _,
          m.(nextblock))
  else None.

Definition alloc (m: mem) (lo hi: Z) bt :=
  low_alloc m lo hi (alignment_of_size hi) bt.

Lemma alloc_nat_mask:
  forall m lo hi m' b bt,
    Mem.alloc m lo hi bt = Some (m',b) ->
    Mem.nat_mask m' b = Int.not (Int.repr (two_power_nat (alignment_of_size hi) - 1)).

Lemma alloc_contents:
  forall m lo hi m' b bt,
    alloc m lo hi bt = Some (m',b) ->
    forall b', b <> b' ->
          (mem_contents m') !! b' = (mem_contents m) !! b'.

Require Import Tactics.

Lemma box_span_le:
  forall x y, 0 <= x <= y ->
         (box_span x <= box_span y)%nat.

Lemma nb_boxes_used_le:
  forall l l',
    list_forall2 (fun x x' => 0 <= snd x <= snd x') l l' ->
    (nb_boxes_used l <= nb_boxes_used l')%nat.

Lemma mbla_le:
  forall sz sz' (SZspec: forall b, 0 <= sz b <= sz' b) n,
   list_forall2 (fun x x' : block * Z => 0 <= snd x <= snd x')
     (mk_block_list_aux sz n)
     (mk_block_list_aux sz' n).


Opaque zeq.
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))
            (PMap.set b (match m.(mem_blocksize)#b with
                             Some (l,h) => if zeq l lo && zeq h hi then
                                             None
                                           else m.(mem_blocksize)#b
                           | None => None
                      end)
                      m.(mem_blocksize))
            m.(mem_mask)
            m.(mem_blocktype)
            m.(nextblock) (nb_extra m) _ _ _ _ _ _ _ _ _ .

Lemma unchecked_free_mask:
  forall m b lo hi b',
    mask (unchecked_free m b lo hi) b' =
    mask m b'.

Lemma unchecked_free_nat_mask:
  forall m b lo hi b',
    nat_mask (unchecked_free m b lo hi) b' =
    nat_mask m b'.

Definition has_bounds m b lo hi :=
  let (lo',hi') := Mem.bounds_of_block m b in
  if zeq lo lo' && zeq hi hi' then true else false.

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


Lemma free_bounds:
  forall b lo hi m m1 m' m1'
         (SB: Mem.mem_blocksize m = Mem.mem_blocksize m1)
         (FL : Mem.free m1 b lo hi = Some m')
         (FL' : Mem.free m b lo hi = Some m1'),
    Mem.mem_blocksize m' = Mem.mem_blocksize m1'.

Lemma unchecked_free_bounds:
  forall b lo hi m m1
         (SB: Mem.mem_blocksize m = Mem.mem_blocksize m1),
    Mem.mem_blocksize (Mem.unchecked_free m1 b lo hi) = Mem.mem_blocksize (Mem.unchecked_free m b lo hi).


Lemma free_contents:
  forall m b lo hi m',
    Mem.free m b lo hi = Some m' ->
    Mem.mem_contents m' = Mem.mem_contents m.


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.

Lemma bounds_of_block_valid:
  forall m b lo hi,
    bounds_of_block m b = (lo,hi) ->
    lo <> hi ->
    valid_block m b.


Lemma size_mem_aux_sup1:
  forall m,
    Alloc.size_mem_aux MA m >= two_power_nat MA.




Definition load (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z): option expr_sym :=
  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: expr_sym) : option expr_sym :=
  match mem_norm m addr with
    Vptr b ofs => load chunk m b (Int.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.





Program Definition store (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: expr_sym): 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.(mem_blocksize)
                          m.(mem_mask)
                              m.(mem_blocktype)
                              m.(nextblock) (nb_extra m)
                                  _ _ _ _ _ _ _ _ _ )
  else
    None.


Definition storev (chunk: memory_chunk) (m: mem) (addr v: expr_sym) : option mem :=
  match mem_norm m addr with
      Vptr b ofs => store chunk m b (Int.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
      Some (mkmem
              (PMap.set b (setN bytes ofs (m.(mem_contents)#b)) m.(mem_contents))
              m.(mem_access)
                  m.(mem_blocksize)
                      m.(mem_mask)
                          m.(mem_blocktype)
                          m.(nextblock) (nb_extra m)
                              _ _ _ _ _ _ _ _ _)
  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.(mem_blocksize)
                    m.(mem_mask)
                        m.(mem_blocktype)
                            m.(nextblock)
                                (nb_extra m)
                                _ _ _ _ _ _ _ _ _)
  else None.

Definition drop_perm_list m (bl: list (block * Z * Z)) p :=
  fold_right (fun (elt: block*Z*Z) m =>
                let (blo,hi) := elt in
                let (b,lo) := blo in
                match m with
                  None => None
                | Some m => drop_perm m b lo hi p
                end) (Some m) bl.

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.

Properties related to load

Lemma Forall_rib:
  forall {A} (P : A -> Prop) l,
    Forall P l ->
    Forall P (rev_if_be l).

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)).




Lemma load_int64_eq_add:
  forall m b i v ,
    Mem.load Mint64 m b (Int.unsigned i) = Some v ->
    Int.unsigned (Int.add i (Int.repr 4)) = Int.unsigned i + 4.

Hint Local Resolve load_valid_access valid_access_load: mem.

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

Lemma loadv_type:
  forall m c a v (L: Mem.loadv c m a = Some v), wt v (type_of_chunk c).

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

Theorem load_int8_signed_unsigned:
  forall m b ofs v1 v2,
  load Mint8signed m b ofs = Some v1 ->
  option_map (Val.sign_ext 8) (load Mint8unsigned m b ofs) = Some v2 ->
  same_eval v1 v2.

Theorem load_int8_signed_unsigned_none:
  forall m b ofs,
    load Mint8signed m b ofs = None ->
    load Mint8unsigned m b ofs = None.

Theorem load_int16_signed_unsigned:
  forall m b ofs v1 v2,
  load Mint16signed m b ofs = Some v1 ->
  option_map (Val.sign_ext 16) (load Mint16unsigned m b ofs) = Some v2 ->
  same_eval v1 v2.

Theorem load_int16_signed_unsigned_none:
  forall m b ofs,
    load Mint16signed m b ofs = None ->
    load Mint16unsigned m b ofs = None.

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.

Lemma Forall_dec:
  forall {A} (P: A -> Prop)
         (Pdec: forall a, P a \/ ~ P a)
         l,
    Forall P l \/ ~ Forall P l.

Lemma Forall_app_l:
  forall {A} (P: A -> Prop) l1 l2,
    Forall P (l1 ++ l2) ->
    Forall P l1.

Lemma Forall_rev':
  forall {A} (P: A -> Prop) l,
    Forall P l ->
    Forall P (rev l).

Lemma Forall_app_r:
  forall {A} (P: A -> Prop) l1 l2,
    Forall P (l1 ++ l2) ->
    Forall P l2.

Theorem load_int64_split:
  forall m b ofs v,
  load Mint64 m b ofs = Some v ->
  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)
  /\ same_eval v (Val.longofwords v1 v2).

Lemma perm_bounds:
  forall m b ofs p k,
    Mem.perm m b ofs k p ->
    in_bound_m ofs m b.



Lemma range_perm_bounds:
  forall m b o1 o2 k p
    (RP: Mem.range_perm m b o1 o2 k p)
    ofs
    (OFS: o1 <= ofs < o2),
    in_bound ofs (Mem.bounds_of_block m b).

Lemma range_perm_bounds':
  forall m b o1 o2 k p
    (RP: Mem.range_perm m b o1 o2 k p)
    (OFS: o1 < o2),
    let (z0,z1) := Mem.bounds_of_block m b in
    z0 <= o1 /\ o2 <= z1.


Lemma loadv_int64_split:
  forall m a v,
  Mem.loadv Mint64 m a = Some v ->
  exists v1 v2,
     Mem.loadv Mint32 m a = Some (if Archi.big_endian then v1 else v2)
  /\ Mem.loadv Mint32 m (Val.add a (Eval (Vint (Int.repr 4)))) = Some (if Archi.big_endian then v2 else v1)
  /\ Val.lessdef (Val.hiword v) v1
  /\ Val.lessdef (Val.loword v) v2.

Properties related to store

  
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 }.

Hint Local Resolve valid_access_store: mem.
 
Section STORE.
Variable chunk: memory_chunk.
Variable m1: mem.
Variable b: block.
Variable ofs: Z.
Variable v: expr_sym.
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 size_of_block_store:
  forall b',
    size_of_block m1 b' = size_of_block m2 b'.

Theorem mask_store:
  forall b',
    mask m1 b' = mask m2 b'.

Theorem bounds_of_block_store:
  forall b',
    bounds_of_block m1 b' = bounds_of_block m2 b'.

Theorem nat_mask_store:
  forall b',
    nat_mask m1 b' = nat_mask m2 b'.


Lemma store_compat:
  forall cm q,
    Mem.compat_m m2 q cm ->
    Mem.compat_m m1 q cm.

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_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_expr_sym v chunk chunk' v'.

Theorem load_store_similar_2:
  forall chunk' v1,
  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 v1 ->
  same_eval v1 (Val.load_result chunk' v).

Theorem load_store_same:
  exists v1, load chunk m2 b ofs = Some v1 /\
             same_eval v1 (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_property:
  forall (P: memval -> Prop) vl p q c,
  (forall v, In v vl -> P v) ->
  p <= q < p + Z_of_nat (length vl) ->
  P(ZMap.get q (setN vl p c)).

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

Lemma psa_ptr:
  forall l b o, proj_symbolic_aux_le l = Eval (Vptr b o) -> False.

Lemma ps_ptr:
  forall l b o, proj_symbolic_le l = Eval (Vptr b o) -> False.

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



Lemma store_size_block:
  forall chunk m b o v m',
    store chunk m b o v = Some m' ->
    size_block m' = size_block m.


Lemma store_mask:
  forall chunk m b o v m',
    store chunk m b o v = Some m' ->
    mask m' = mask m.


Lemma store_mk_block_list:
  forall chunk m b o v m',
    store chunk m b o v = Some m' ->
    mk_block_list m' = mk_block_list m.





Lemma size_block_store:
  forall chunk m1 b1 ofs v1 n1,
    store chunk m1 b1 ofs v1 = Some n1 ->
    forall b',
      size_block n1 b' = size_block m1 b'.

Lemma store_in_bound_m_1:
  forall b' ofs',
    in_bound_m ofs' m1 b' ->
    in_bound_m ofs' m2 b'.

Lemma store_in_bound_m_2:
  forall b' ofs',
    in_bound_m ofs' m2 b' ->
    in_bound_m ofs' m1 b'.


End STORE.

Lemma store_norm:
  forall chunk m1 b o v m2 e,
    Mem.store chunk m1 b o v = Some m2 ->
    Mem.mem_norm m1 e = Mem.mem_norm m2 e.

Lemma storev_norm:
  forall chunk m1 bo v m2 e,
    Mem.storev chunk m1 bo v = Some m2 ->
    Mem.mem_norm m1 e = Mem.mem_norm m2 e.

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 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.

Lemma get_setN_not_last:
  forall al ofs0 ofs o a t,
    ofs0 <> ofs ->
    (ZMap.get ofs0 (setN al o (ZMap.set ofs a t))) = ZMap.get ofs0 (setN al o t).

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 ->
  { 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.
  
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_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 size_of_block_storebytes:
  forall b',
    size_of_block m1 b' = size_of_block m2 b'.

Theorem mask_storebytes:
  forall b',
    mask m1 b' = mask m2 b'.

Theorem bounds_of_block_storebytes:
  forall b',
    bounds_of_block m1 b' = bounds_of_block m2 b'.

Theorem nat_mask_storebytes:
  forall b',
    nat_mask m1 b' = nat_mask m2 b'.

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'.


Lemma storebytes_size_block:
  size_block m2 = size_block m1.

Lemma storebytes_blocksize:
  mem_blocksize m2 = mem_blocksize m1.


Lemma storebytes_mask:
    mem_mask m2 = mem_mask m1.

  
Lemma storebytes_mk_block_list:
  mk_block_list m2 = mk_block_list m1.


Lemma size_block_storebytes:
  forall b',
    size_block m2 b' = size_block m1 b'.

Lemma storebytes_in_bound_m_1:
    forall b' ofs',
      in_bound_m ofs' m1 b' ->
      in_bound_m ofs' m2 b'.

Lemma storebytes_in_bound_m_2:
    forall b' ofs',
      in_bound_m ofs' m2 b' ->
      in_bound_m ofs' m1 b'.


End STOREBYTES.

Definition all_blocks_injected (f:meminj) (m:mem) : Prop :=
  forall b lo hi,
    bounds_of_block m b = (lo,hi) ->
    hi - lo <> 0 ->
    f b <> None.



Lemma store_abi:
  forall chunk m b ofs v m',
    Mem.store chunk m b ofs v = Some m' ->
    forall j,
      Mem.all_blocks_injected j m ->
      Mem.all_blocks_injected j m'.


Lemma storev_abi:
  forall chunk m bofs v m',
    Mem.storev chunk m bofs v = Some m' ->
    forall j,
      Mem.all_blocks_injected j m ->
      Mem.all_blocks_injected j m'.


Lemma storebytes_abi:
  forall m b ofs v m'
    (SB: Mem.storebytes m b ofs v = Some m')
    j (ABI: Mem.all_blocks_injected j m),
    Mem.all_blocks_injected j m'.


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 Forall_app_not:
  forall {A} P (a b:list A),
  (~ Forall P a) \/ (~ Forall P b) ->
  ~ Forall P (a++b).

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.

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.

Lemma load_align_chunk:
  forall m b ofs chunk v,
    load chunk m b ofs = Some v ->
    (align_chunk chunk | ofs).

Lemma loadbytes_one:
  forall m b o n bytes,
    loadbytes m b o n = Some bytes ->
    n > 0 ->
    exists b1 b2,
      loadbytes m b o 1 = Some b1 /\
      loadbytes m b (o+1) (n-1) = Some b2 /\
      bytes = b1 ++ b2.

Lemma int_range_int64:
  forall i,
  0 <= Int.unsigned i <= Int64.max_unsigned.

Lemma int_inf_two_p_32:
  forall i,
    0 <= Int.unsigned i < two_power_nat 32.

Lemma store_int64_eq_add:
  forall m b i v m',
    store Mint64 m b (Int.unsigned i) v = Some m' ->
    Int.unsigned (Int.add i (Int.repr 4)) = Int.unsigned i + 4.

Properties related to alloc.

Lemma pos2nat_id:
  forall p,
    Pos.of_nat (S (pred (Pos.to_nat p))) = p.


Section ALLOC.

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

Theorem mask_alloc_other:
  forall b',
    b <> b' ->
    mask m1 b' = mask m2 b'.

Theorem size_of_block_alloc_other:
  forall b',
    b <> b' ->
    size_of_block m1 b' = size_of_block m2 b'.

Theorem bounds_of_block_alloc_other:
  forall b',
    b <> b' ->
    bounds_of_block m1 b' = bounds_of_block m2 b'.

Theorem nat_mask_alloc_other:
  forall b',
    b <> b' ->
    nat_mask m1 b' = nat_mask 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, 0 <= 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 0 <= ofs < hi else perm m1 b' ofs k p.

Theorem perm_alloc_3:
  forall ofs k p, perm m2 b ofs k p -> 0 <= 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.

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

Theorem valid_access_alloc_same:
  forall chunk ofs,
  0 <= 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 0 <= 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.

Require Import Classical.

Lemma init_block'_eundef:
  forall n b cur o,
    (0 <= o < n)%nat ->
    nth_error (init_block' n b cur) o =
    Some (Symbolic
            ( (Eundef b (Int.add cur (Int.repr (Z.of_nat o)))))
            None O).

Lemma in_nth_error:
  forall (A: Type) (vl: list A) (x:A),
    In x vl ->
    exists n, nth_error vl n = Some x.

Lemma nth_error_length:
  forall (A:Type) (l:list A) x v,
    nth_error l x = Some v ->
    (length l > x)%nat.

Lemma init_block'_length:
  forall n b c,
    length (init_block' n b c) = n.

Lemma init_block_eundef:
  forall n o lo hi c,
    Forall (fun x => x = Symbolic ((Eval Vundef)) None O) (getN n o (init_block lo hi c)).

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 = Symbolic (Eval Vundef) None O.


Opaque Pos.of_nat.


Lemma bounds_of_block_alloc:
    bounds_of_block m2 b = (0,Z.max 0 hi).


Lemma bounds_of_block_alloc_old:
  bounds_of_block m1 b = (0,0).

Lemma alloc_mask:
  mask m2 b = alignment_of_size hi.


Lemma bounds_of_block_alloc_eq:
  forall b',
    bounds_of_block m2 b' = if eq_block b' b
                              then (0,Z.max 0 hi)
                              else if plt b' (nextblock m2)
                                   then bounds_of_block m1 b'
                                   else (0,0).



Lemma alloc_in_bound:
  forall b0 o,
    in_bound_m (Int.unsigned o) m1 b0 ->
    in_bound_m (Int.unsigned o) m2 b0.



Lemma mask_alloc_old:
  mask m1 b = O.

Lemma nat_mask_alloc_old:
  nat_mask m1 b = Int.mone.

Lemma compat_alloc:
  forall cm q,
    compat_m m2 q cm ->
    compat_m m1 q cm.

Lemma norm_alloc:
  forall e v,
    Mem.mem_norm m1 e = v ->
    v <> Vundef ->
    Mem.mem_norm m2 e = v.

Lemma normalise_alloc:
  forall e,
    Values.Val.lessdef (Mem.mem_norm m1 e) (Mem.mem_norm m2 e).

Definition block_undefs lo hi delta m2 b2 :=
  forall ofs : Z,
    lo <= ofs < hi ->
    ZMap.get (ofs + delta) (mem_contents m2) # b2 =
    Symbolic ( Eval Vundef ) None 0.

Lemma nth_error_init_block':
  forall n b cur ofs,
    (ofs < n)%nat ->
    nth_error (init_block' n b cur) ofs = Some (Symbolic ((Eundef b (Int.add cur (Int.repr (Z.of_nat ofs))))) None O).

Lemma init_block_length:
  forall n b i,
    length (init_block' n b i) = n.

Lemma get_init_block:
  forall ofs lo hi b,
    ZMap.get ofs (init_block lo hi b) = Symbolic (Eval Vundef) None O.

Lemma mem_alloc_block_undefs:
  block_undefs 0 hi 0 m2 b.

Lemma alloc_contents_old:
  forall b' (DIFF: b' <> b),
    (mem_contents m2) # b' = (mem_contents m1) # b'.

End ALLOC.

Lemma bounds_size:
  forall m b lo hi,
    Mem.bounds_of_block m b = (lo,hi) ->
    Mem.size_block m b = hi - lo.

Lemma mbla_pred_nextblock:
  forall sz n,
    (forall b, Ple (Pos.of_nat n) b -> sz b = (0)) ->
    Alloc.size_mem_aux MA (Alloc.mk_block_list_aux sz n) =
    Alloc.size_mem_aux MA (Alloc.mk_block_list_aux sz (pred n)).

Lemma fold_left_align:
  let f := fun acc (bsz: block * Z) => let (_, sz) := bsz in align (align acc (two_power_nat MA) + Z.max 0 sz) (two_power_nat MA) in
  forall l z,
    fold_left f l (align z (two_power_nat MA)) =
    fold_left f l 0 + align z (two_power_nat MA).
Lemma size_block_pos:
  forall m b,
    0 <= Mem.size_block m b.

Lemma mbl_pos:
  forall m,
    Forall (fun x : block * Z => 0 <= snd x) (mk_block_list m).

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 ->
  has_bounds m1 b lo hi = true ->
  { 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.

Lemma mask_free:
  forall b', Mem.mask m1 b' = Mem.mask m2 b'.

Theorem size_of_block_free:
  forall b',
    bf <> b' ->
    size_of_block m1 b' = size_of_block m2 b'.

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.

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.

Lemma unchecked_free_bounds':
  forall m b lo hi b',
    bounds_of_block (unchecked_free m b lo hi) b' =
    if eq_block b' b
    then match bounds_of_block m b with
             (lo',hi') => (if zeq lo' lo && zeq hi' hi
                           then (0,0)
                           else (lo',hi'))
         end
    else bounds_of_block m b'.

Lemma free_bounds':
  forall m b lo hi m' b',
    free m b lo hi = Some m' ->
    bounds_of_block m' b' = bounds_of_block m b' \/ bounds_of_block m' b' = (0,0).

Lemma free_abi:
  forall m b lo hi m'
    (FREE: Mem.free m b lo hi = Some m')
    j (ABI: Mem.all_blocks_injected j m),
    Mem.all_blocks_injected j m'.

Lemma free_mask:
  forall m b lo hi m' b',
    free m b lo hi = Some m' ->
    mask m' b' = mask m b'.


Lemma freelist_mask:
  forall l m m' b',
    free_list m l = Some m' ->
    mask m' b' = mask m b'.

Lemma freelist_abi:
  forall l m m'
    (FREE: Mem.free_list m l = Some m')
    j (ABI: Mem.all_blocks_injected j m),
    Mem.all_blocks_injected j m'.


Lemma compat_free:
  forall m b lo hi m'
         (FREE: Mem.free m b lo hi = Some m')
         cm q (COMP: Mem.compat_m m q cm),
    Mem.compat_m m' q cm.


Lemma compat_unchecked_free:
  forall m b lo hi
    q cm (COMP: Mem.compat_m m q cm),
    Mem.compat_m (unchecked_free m b lo hi) q cm.


Lemma norm_free:
  forall m1 bf lo hi m2 (FREE: free m1 bf lo hi = Some m2),
  forall e v,
    Mem.mem_norm m2 e = v ->
    v <> Vundef ->
    Mem.mem_norm m1 e = v.

Lemma norm_unchecked_free:
  forall m1 bf lo hi,
  forall e v,
    Mem.mem_norm (unchecked_free m1 bf lo hi) e = v ->
    v <> Vundef ->
    Mem.mem_norm m1 e = v.

Lemma normalise_free:
  forall m1 bf lo hi m2 (FREE: free m1 bf lo hi = Some m2),
  forall e,
    Values.Val.lessdef (Mem.mem_norm m2 e) (Mem.mem_norm m1 e).

Lemma unchecked_free_bounds_of_block:
  forall m b lo hi,
    bounds_of_block (unchecked_free m b lo hi) b =
    match (bounds_of_block m b) with
        (lo',hi') => if zeq lo' lo && zeq hi' hi then (0,0) else (lo',hi')
    end.

Lemma unchecked_free_bounds_of_block_other:
  forall m b lo hi b', b <> b' ->
    bounds_of_block (unchecked_free m b lo hi) b' =
    bounds_of_block m b'.


Lemma bounds_free:
  forall m m' b b' lo hi ,
  Mem.free m b lo hi = Some m' ->
  b <> b' ->
  Mem.bounds_of_block m' b' = Mem.bounds_of_block m b'.

Lemma bounds_freelist:
  forall fbl m m' b ,
  Mem.free_list m fbl = Some m' ->
  ~ In b (map (fun a => fst (fst a)) fbl) ->
  Mem.bounds_of_block m' b = Mem.bounds_of_block m b.

Lemma range_perm_freelist:
  forall fbl m m' b,
    Mem.free_list m fbl = Some m' ->
    ~ In b (map (fun a => fst (fst a)) fbl) ->
    forall lo hi k p,
      Mem.range_perm m' b lo hi k p ->
      Mem.range_perm m b lo hi k p.

Lemma contents_free:
  forall m b lo hi m' b',
    Mem.free m b lo hi = Some m' ->
    b <> b' ->
    (Mem.mem_contents m) !! b' = (Mem.mem_contents m') !! b'.



Lemma contents_freelist:
  forall (fbl : list (block * Z * Z)) (m m' : mem) (b' : block),
  Mem.free_list m fbl = Some m' ->
  (Mem.mem_contents m) !! b' = (Mem.mem_contents m') !! b'.

Lemma freelist_valid:
  forall fbl m m' b,
    Mem.free_list m fbl = Some m' ->
    ~ Mem.valid_block m' b ->
    ~ Mem.valid_block m b.


Lemma permut_filter:
  forall A f (l l' : list A)
    (P: Permutation l l'),
    Permutation (filter f l) (filter f l').

Definition size_mem_blocks (bl: list (block * Z * Z)) (z:Z) : Z :=
  fold_left
    (fun acc x =>
       align acc (two_power_nat MA) + Z.max 0 (snd x - snd (fst x))) bl z.

Definition list_of_blocks (bl: list (block*Z*Z)) : list (block*Z) :=
  map (fun a : ident * Z * Z => (fst (fst a), snd a - snd (fst a))) bl.

Lemma size_mem_blocks_al:
  forall l z,
    size_mem_al (two_power_nat MA) (list_of_blocks l) (align z (two_power_nat MA)) =
    align (size_mem_blocks l z) (two_power_nat MA).

Lemma size_mem_al_rev:
  forall l z,
    size_mem_al (two_power_nat MA) l z = size_mem_al (two_power_nat MA) (rev l) z.

Lemma size_mem_app:
  forall a b c,
    size_mem_al (two_power_nat MA) (a++b) c = size_mem_al (two_power_nat MA) b (size_mem_al (two_power_nat MA) a c).

Lemma size_mem_al_aligned:
  forall l z,
    z = align z (two_power_nat MA) ->
    size_mem_al (two_power_nat MA) l z = align (size_mem_al (two_power_nat MA) l z) (two_power_nat MA).

Lemma size_mem_aux_aligned:
  forall l,
    size_mem_aux MA l = align (size_mem_aux MA l) (two_power_nat MA).

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 -> {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 mask_drop_perm:
  forall b',
    mask m b' = mask m' b'.

Theorem size_of_block_drop_perm:
  forall b',
    size_of_block m b' = size_of_block m' b'.

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 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.



Lemma drop_perm_bounds:
  forall b',
    bounds_of_block m b' = bounds_of_block m' b'.

Lemma nat_mask_drop_perm:
  forall b',
    nat_mask m b' = nat_mask m' b'.

Lemma drop_perm_blocksize:
  mem_blocksize m' = mem_blocksize m.

Lemma drop_perm_size_block:
  size_block m' = size_block m.

Lemma drop_perm_mask:
  mask m' = mask m.

Lemma drop_perm_nextblock:
  nextblock m' = nextblock m.

Lemma drop_perm_mk_block_list:
  mk_block_list m = mk_block_list m'.


End DROP.

Section DROPLIST.


  Variable bl: list (block*Z*Z).
  Variable m: mem.
Variable p: permission.
Variable m': mem.
Hypothesis DROP: drop_perm_list m bl p = Some m'.

Theorem mask_drop_perm_list:
  forall b',
    mask m b' = mask m' b'.

Theorem size_of_block_drop_perm_list:
  forall b',
    size_of_block m b' = size_of_block m' b'.

Theorem nextblock_drop_list:
  nextblock m' = nextblock m.

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

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



Theorem perm_drop_perm:
  forall m b lo hi p m',
    Mem.drop_perm m b lo hi p = Some m' ->
  forall bb ofs k p',
    perm m' bb ofs k p' <->
    (if eq_block b bb
     then
       if zle lo ofs && zlt ofs hi
       then perm_order p p'
       else perm m bb ofs k p'
     else perm m bb ofs k p').


Lemma zle_zlt_false:
  forall a b c,
    zle a b && zlt b c = false -> b < a \/ b >= c.

Theorem perm_drop_perm_list:
  list_norepet (map fst (map fst bl)) ->
  forall b ofs k p',
    perm m' b ofs k p' <->
    ((In b (map fst (map fst bl)) ->
     forall lo hi,
       In (b,lo,hi) bl ->
       (lo <= ofs < hi ->
        perm_order p p') /\
       (~ (lo <= ofs < hi) -> perm m b ofs k p')) /\
     (~ In b (map fst (map fst bl)) -> perm m b ofs k p')).

Lemma drop_perm_bounds_list:
  forall b',
    bounds_of_block m b' = bounds_of_block m' b'.

Lemma nat_mask_drop_perm_list:
  forall b',
    nat_mask m b' = nat_mask m' b'.

Lemma drop_perm_blocksize_list:
  mem_blocksize m' = mem_blocksize m.

Lemma drop_perm_size_block_list:
  size_block m' = size_block m.

Lemma drop_perm_mask_list:
  mask m' = mask m.

Lemma drop_perm_nextblock_list:
  nextblock m' = nextblock m.

Lemma drop_perm_mk_block_list_list:
  mk_block_list m = mk_block_list m'.


Lemma drop_perm_contents:
  forall m b lo hi p m',
    drop_perm m b lo hi p = Some m' ->
    mem_contents m = mem_contents m'.

Lemma drop_perm_list_contents:
  mem_contents m = mem_contents m'.

End DROPLIST.

Generic injections

Lemma load_in_bound:
  forall chunk b ofs m v,
    load chunk m b ofs = Some v ->
    in_bound_m ofs m b.

Lemma alignment_of_size_inj:
  forall n n0,
    Z.max 0 n >= Z.max 0 n0 ->
    (alignment_of_size n >= alignment_of_size n0)%nat.

Ltac egt H :=
  match type of H with
  | context [get_type ?v = get_type ?v'] =>
      unfold get_type in H; destruct (wt_expr_dec v Tint);
       destruct (wt_expr_dec v Tfloat); destruct (wt_expr_dec v Tsingle);
       destruct (wt_expr_dec v Tlong); destruct (wt_expr_dec v' Tint);
       destruct (wt_expr_dec v' Tfloat); destruct (wt_expr_dec v' Tsingle);
       destruct (wt_expr_dec v' Tlong); destr
  end.


Lemma mr_vundef_get_type:
  forall mr (wf: wf_mr mr) v v'
    (Rel: mr v v'),
    same_eval v (Eval Vundef) \/
    get_type v = get_type v'.
    
Lemma list_forall2_and:
  forall A B P Q (l: list A) (l': list B),
    list_forall2 (fun a b => P a b) l l' ->
    list_forall2 (fun a b => Q a b) l l' ->
    list_forall2 (fun a b => P a b /\ Q a b) l l'.

Lemma match_eSexpr:
  forall al em a b c d e,
    eSexpr al em match a with
                   Tint => b
                 | Tlong => c
                 | Tfloat => d
                 | Tsingle => e
                 end =
    match a with
      Tint => eSexpr al em b
    | Tlong => eSexpr al em c
    | Tfloat => eSexpr al em d
    | Tsingle => eSexpr al em e
    end.

Lemma encode_val_memval_rel:
  forall mr (wf: wf_mr mr) v v' chunk,
    mr v v' ->
    list_forall2 (memval_rel mr) (encode_val chunk v) (encode_val chunk v').

Lemma free_list_bounds_after:
  forall bl m m',
    Mem.free_list m bl = Some m' ->
    forall b lo0 hi0,
      Mem.bounds_of_block m' b = (lo0, hi0) ->
      hi0 - lo0 <> 0 ->
      Mem.bounds_of_block m b = (lo0, hi0).




Ltac genAlloc :=
  repeat match goal with
         | H: Mem.alloc ?m ?lo ?hi ?bt = Some (?m',?b') |- _ =>
           generalize (Mem.nextblock_alloc _ _ _ _ _ _ H);
             generalize (Mem.alloc_result _ _ _ _ _ _ H);
             let x := fresh in let y := fresh "NA" in
                               intros x y; subst; clear H;
                               try rewrite y in *
         end.

Lemma align_small:
  forall al (AlPos: al > 0) x (Xsmall: 0 < x <= al),
    align x al = al.

Lemma mul_lt_slack:
  forall a b c d,
    0 <= d < a ->
    a * b < a * c ->
    a * b < a * c - d.

Lemma align_mul:
  forall al (AlPos: al > 0) x,
    align (x * al) al = x * al.

Lemma align_big_smaller:
  forall z n, n >= 0 -> z >= 0 ->
         align (z+n) (two_power_nat MA) <= (two_power_nat MA) * n + align z (two_power_nat MA).

Lemma alloc_perm:
  forall m n m' b' bt
    (AB: Mem.alloc m 0 n bt = Some (m',b'))
    b o k p
    (Cond: Mem.perm m b o k p \/
           (b = b' /\ 0 <= o < n)),
    Mem.perm m' b o k p.

Lemma alloc_perm_inv:
  forall m n m' b' bt
    (AB: Mem.alloc m 0 n bt = Some (m',b'))
    b o k p
    (PERM: Mem.perm m' b o k p),
    Mem.perm m b o k p \/
    (b = b' /\ 0 <= o < n).

Lemma alloc_lo_0:
  forall m lo hi bt,
    alloc m lo hi bt = alloc m 0 hi bt.

Lemma in_bound_valid:
  forall m b o,
    Mem.in_bound_m o m b ->
    Mem.valid_block m b.

Lemma a_mask:
  forall m sz m' sp bt,
    Mem.alloc m 0 sz bt = Some (m',sp) ->
    forall b, Mem.mask m' b = if plt b sp then Mem.mask m b
                         else if peq b sp then Alloc.alignment_of_size sz
                              else O.

Lemma a_mem_contents:
  forall m1 sz m2 sp bt (ALLOC: Mem.alloc m1 0 sz bt = Some (m2, sp)),
    Maps.PMap.get sp (Mem.mem_contents m2) = Mem.init_block 0 sz sp.

Lemma a_mem_contents':
  forall m1 sz m2 sp bt (ALLOC: Mem.alloc m1 0 sz bt = Some (m2, sp)),
    (Mem.mem_contents m2) =
    Maps.PMap.set sp (Mem.init_block 0 sz sp) (Mem.mem_contents m1).

Lemma init_block_spec_out:
  forall ofs sz b,
    ofs < 0 \/ ofs >= sz ->
   Maps.ZMap.get ofs (Mem.init_block 0 sz b) = Symbolic (Eval Vundef) None 0.

Lemma init_block_spec:
  forall ofs sz b,
    Maps.ZMap.get ofs (Mem.init_block 0 sz b) =
    Symbolic (if zle 0 ofs && zlt ofs sz
              then Eval Vundef
              else Eval Vundef) None 0.

Require Import IntFacts.

Lemma get_getN:
  forall t1 t2
    (CONT : forall ofs, Maps.ZMap.get ofs t1 = Maps.ZMap.get ofs t2),
  forall n o, Mem.getN n o t1 = Mem.getN n o t2.

Lemma same_access_same_perm:
  forall m1 m2
    (ACC: Mem.mem_access m1 = Mem.mem_access m2)
    b o k p,
    Mem.perm m1 b o k p <-> Mem.perm m2 b o k p.

Lemma same_access:
  forall m1 m2
    (ACC: Mem.mem_access m1 = Mem.mem_access m2)
    chunk b ofs p,
    Mem.valid_access m1 chunk b ofs p <->
    Mem.valid_access m2 chunk b ofs p.

Lemma load_contents_access:
  forall m1 m2
    (CONT: forall b ofs,
        Maps.ZMap.get ofs (Maps.PMap.get b (Mem.mem_contents m1)) =
        Maps.ZMap.get ofs (Maps.PMap.get b (Mem.mem_contents m2)))
    (ACC: Mem.mem_access m1 = Mem.mem_access m2)
    b ofs chunk,
    Mem.load chunk m1 b ofs = Mem.load chunk m2 b ofs.

Lemma perm_freelist:
  forall fbl m m' b ofs k p,
  Mem.free_list m fbl = Some m' ->
  Mem.perm m' b ofs k p ->
  Mem.perm m b ofs k p.

Lemma nextblock_freelist:
  forall fbl m m',
  Mem.free_list m fbl = Some m' ->
  Mem.nextblock m' = Mem.nextblock m.

Hint Resolve two_power_nat_pos.

Lemma size_mem_blocks_rew:
  forall l z,
    align (Mem.size_mem_blocks l z) (two_power_nat MA) =
    align z (two_power_nat MA) + align (Mem.size_mem_blocks l 0) (two_power_nat MA).

Lemma exact_bounds_perm_free_list:
  forall e m m'
         (LNR: list_norepet (map (fun a => fst (fst a)) e))
         (FREELIST: Mem.free_list m e = Some m'),
  forall b,
    In b (map (fun a => fst (fst a)) e) ->
    Mem.bounds_of_block m' b = (0,0).

Lemma exact_bounds_free_list:
  forall e m m'
         (LNR: list_norepet (map (fun a => fst (fst a)) e))
         (FREELIST: Mem.free_list m e = Some m'),
  forall b,
    In b (map (fun a => fst (fst a)) e) ->
    Mem.bounds_of_block m' b = (0,0) /\
    (forall k p ofs,
      ~ Mem.perm m' b ofs k p).

Lemma free_list_freeable:
  forall l m m',
  Mem.free_list m l = Some m' ->
  forall b lo hi,
  In (b, lo, hi) l -> Mem.range_perm m b lo hi Cur Freeable.

Lemma nextblock_storev:
  forall chunk m addr v m',
  Mem.storev chunk m addr v = Some m' -> Mem.nextblock m' = Mem.nextblock m.


Remark free_list_nextblock:
  forall l m m',
  Mem.free_list m l = Some m' -> Mem.nextblock m' = Mem.nextblock m.

Remark free_list_load:
  forall chunk b' l m m',
  Mem.free_list m l = Some m' ->
  (forall b lo hi, In (b, lo, hi) l -> Plt b' b) ->
  Mem.load chunk m' b' 0 = Mem.load chunk m b' 0.




Lemma store_storev:
  forall m c b v m',
    Mem.store c m b (Int.unsigned Int.zero) v = Some m' ->
    Mem.storev c m (Eval (Vptr b Int.zero)) v = Some m'.

Lemma free_list_perm':
  forall b lo hi l m m',
  Mem.free_list m l = Some m' ->
  In (b, lo, hi) l ->
  Mem.range_perm m b lo hi Cur Freeable.

Lemma memval_rel_refl:
  forall mr mv (WF: wf_mr mr),
    memval_rel mr mv mv.

Lemma storev_bounds:
  forall chunk m1 ptr v m2,
    Mem.storev chunk m1 ptr v = Some m2 ->
    forall b,
      Mem.bounds_of_block m1 b = Mem.bounds_of_block m2 b.


Lemma storev_addr_lessdef:
  forall m chunk vaddr vaddr' v m',
    Val.lessdef vaddr vaddr' ->
    storev chunk m vaddr v = Some m' ->
    storev chunk m vaddr' v = Some m'.



Lemma perm_unchecked_free:
  forall
    m bb lo hi
    (Bnds: Mem.bounds_of_block m bb = (lo,hi))
    m'
    (UFL: Mem.unchecked_free m bb lo hi = m')
    b o k p,
    Mem.perm m' b o k p <->
    (b <> bb /\ Mem.perm m b o k p).

Lemma perm_free_eq:
  forall m b lo hi m'
    (FREE: Mem.free m b lo hi = Some m')
    (BND: Mem.bounds_of_block m b = (lo,hi))
    b' o k p
    (PERM: Mem.perm m' b' o k p),
    Mem.perm m b' o k p /\ b <> b'.


Lemma free_bounds_exact:
  forall m b lo hi m'
    (Free: Mem.free m b lo hi = Some m')
    b',
    Mem.bounds_of_block m' b' =
    if eq_block b b'
    then (0,0)
    else Mem.bounds_of_block m b'.



Lemma unchecked_free_contents:
  forall m bb lo hi,
    Mem.mem_contents (Mem.unchecked_free m bb lo hi) = Mem.mem_contents m.


Lemma nextblock_unchecked_free:
  forall b lo hi m,
    Mem.nextblock m = Mem.nextblock (Mem.unchecked_free m b lo hi).


Lemma Zeq_ge:
  forall x y, x = y -> x >= y.

Lemma bounds_dec:
  forall m b lo hi,
    {bounds_of_block m b = (lo,hi)} + {bounds_of_block m b <> (lo,hi)}.



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.

  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) ->
      in_bound_m ofs1 m b1 ->
      in_bound_m ofs2 m b2 ->
      b1' <> b2' \/ ofs1 + delta1 <> ofs2 + delta2.

  Definition inj_offset_aligned (delta: Z) (size: Z) : Prop :=
    (two_power_nat (alignment_of_size size) | delta).
  
Section MEMINJ.

  Variable sm: bool.
  Variable ei: meminj -> expr_sym -> expr_sym -> Prop.
  Hypothesis WF : wf_inj ei.
  
  Record mem_inj (f: meminj) (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 ->
            perm m2 b2 (ofs + delta) k p;
        mi_bounds: (* we mimic mi_perm with bounds instead of permissions. *)
          forall b1 b2 delta ofs,
            f b1 = Some(b2, delta) ->
            in_bound_m ofs m1 b1 ->
            in_bound_m (ofs+delta) m2 b2;
        mi_align':
          forall b b0 z, (* we can now talk of the alignment of blocks *)
            f b = Some (b0, z) ->
            (mask m2 b0 >= mask m1 b)%nat /\
            Z.divide (two_p (Z.of_nat (mask m1 b))) z;
        mi_memval:
          forall b1 ofs b2 delta,
            f b1 = Some(b2, delta) ->
            perm m1 b1 ofs Cur Readable ->
            memval_inject ei f
                       (ZMap.get ofs m1.(mem_contents)#b1)
                       (ZMap.get (ofs+delta) m2.(mem_contents)#b2);
        mi_size_mem: (* m2 must be ``smaller'' than m1. *)
          sm = true ->
          (nb_boxes_used_m m2 <= nb_boxes_used_m m1)%nat
      }.
  
  Lemma mi_align:
    forall f m1 m2,
      mem_inj f m1 m2 ->
      forall (b1 b2: block) delta,
        f b1 = Some (b2, delta) ->
        forall chunk ofs p,
          range_perm m1 b1 ofs (ofs + size_chunk chunk) Max p ->
          (align_chunk chunk | delta).


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

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

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


  Lemma getN_inj:
    forall f m1 m2 b1 b2 delta,
      mem_inj f 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 ei f)
                     (getN n ofs (m1.(mem_contents)#b1))
                     (getN n (ofs + delta) (m2.(mem_contents)#b2)).

  Lemma load_inj:
    forall f m1 m2 chunk b1 ofs b2 delta v1
           (MIG: mem_inj f m1 m2)
           (LOAD: load chunk m1 b1 ofs = Some v1)
           (FB: f b1 = Some (b2, delta)),
    exists v2,
      load chunk m2 b2 (ofs + delta) = Some v2 /\
      ei f v1 v2.

  Lemma loadbytes_inj:
    forall f m1 m2 len b1 ofs b2 delta bytes1,
      mem_inj f 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 ei f) bytes1 bytes2.


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

  Lemma filter_ext:
    forall A p p' (l: list A),
      (forall b, p b = p' b) ->
      filter p l = filter p' l.

  Lemma nb_extra_store:
    forall chunk m1 b ofs v m2 (STORE: store chunk m1 b ofs v = Some m2),
      nb_extra m1 = nb_extra m2.


  Lemma nb_extra_storebytes:
    forall m1 b ofs v m2 (STORE: storebytes m1 b ofs v = Some m2),
      nb_extra m1 = nb_extra m2.


  Lemma nb_extra_low_alloc:
    forall m1 lo hi bt al b m2 (STORE: low_alloc m1 lo hi al bt = Some (m2, b)),
      nb_extra m1 = nb_extra m2.

  Lemma nb_extra_alloc:
    forall m1 lo hi bt b m2 (STORE: alloc m1 lo hi bt = Some (m2, b)),
      nb_extra m1 = nb_extra m2.


  Lemma nb_extra_unchecked_free:
    forall m1 lo hi b,
      nb_extra m1 = nb_extra (unchecked_free m1 b lo hi).

  Lemma nb_extra_free:
    forall m1 lo hi b m2 (STORE: free m1 b lo hi = Some m2),
      nb_extra m1 = nb_extra m2.

  
  Lemma nb_extra_drop_perm:
    forall m1 b lo hi p m2 (STORE: drop_perm m1 b lo hi p = Some m2),
      nb_extra m1 = nb_extra m2.



  Lemma nb_extra_free_list:
    forall bl m1 m2 (STORE: free_list m1 bl = Some m2),
      nb_extra m1 = nb_extra m2.




  Lemma nb_boxes_used_same:
    forall m1 m2,
      mk_block_list m1 = mk_block_list m2 ->
      nb_extra m1 = nb_extra m2 ->
      nb_boxes_used_m m1 = nb_boxes_used_m m2.


  Ltac rew_nb_extra :=
    repeat
      match goal with
      | H: store _ ?m1 _ _ _ = Some ?m2 |- context [nb_extra ?m2] => rewrite <- (nb_extra_store _ _ _ _ _ _ H)
      | H: storebytes ?m1 _ _ _ = Some ?m2 |- context [nb_extra ?m2] => rewrite <- (nb_extra_storebytes _ _ _ _ _ H)
      | H: drop_perm ?m1 _ _ _ _ = Some ?m2 |- context [nb_extra ?m2] => rewrite <- (nb_extra_drop_perm _ _ _ _ _ _ H)
      end.


  Ltac rew_mk_block_list :=
    repeat
      match goal with
      | H: store _ ?m1 _ _ _ = Some ?m2 |- context [mk_block_list ?m2] => rewrite (store_mk_block_list _ _ _ _ _ _ H)
      | H: storebytes ?m1 _ _ _ = Some ?m2 |- context [mk_block_list ?m2] => rewrite (storebytes_mk_block_list _ _ _ _ _ H)
      | H: drop_perm ?m1 _ _ _ _ = Some ?m2 |- context [mk_block_list ?m2] => rewrite <- (drop_perm_mk_block_list _ _ _ _ _ _ H)
      end.



  Lemma nb_boxes_used_cons:
    forall a b l,
      nb_boxes_used ((a,b)::l) = (nb_boxes_used l + box_span b)%nat.

  Lemma nb_boxes_alloc:
    forall m1 lo hi bt b m2,
      alloc m1 lo hi bt = Some (m2, b) ->
      nb_boxes_used_m m2 = (nb_boxes_used_m m1 + box_span (Z.max 0 hi))%nat.


  Ltac solve_size_mem :=
    match goal with
    | H: alloc ?m1 _ _ _ = Some (?m2,_) |- context [nb_boxes_used_m ?m2] => rewrite (nb_boxes_alloc _ _ _ _ _ _ H)
    | H: mem_inj _ _ _ |- _ => unfold nb_boxes_used_m; rew_mk_block_list; rew_nb_extra; inv H; auto
    | |- _ => unfold nb_boxes_used_m; rew_mk_block_list; rew_nb_extra; auto
    end.



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

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

  Lemma store_outside_inj:
    forall f m1 m2 chunk b ofs v m2',
      mem_inj f 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 m1 m2'.

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

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

Lemma storebytes_outside_inj:
  forall f m1 m2 b ofs bytes2 m2',
    mem_inj f 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 m1 m2'.

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




Lemma alloc_left_unmapped_inj:
  forall f m1 m2 lo hi m1' b1 bt,
  mem_inj f m1 m2 ->
  alloc m1 lo hi bt = Some (m1', b1) ->
  f b1 = None ->
  forall (VB: forall b, ~ valid_block m1 b -> f b = None),
  mem_inj f m1' m2.

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

Lemma drop_mapped_inj:
  forall f m1 m2 b1 b2 delta lo hi p m1',
    mem_inj f m1 m2 ->
    drop_perm m1 b1 lo hi p = Some m1' ->
    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 m1' m2'.

Lemma drop_outside_inj:
  forall f m1 m2 b lo hi p m2',
    mem_inj f 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 m1 m2'.

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

End MEMINJ.

Memory injections

Opaque Z.add. Opaque Pos.of_nat.


Lemma size_sup_one_block:
  forall m bs b z0
         (BS: bs # b = Some (0, z0))
         (PLE: ((Pos.to_nat b) <= m)%nat)
,
    z0 <=
    size_mem_aux MA
      (mk_block_list_aux (get_size bs) m).

Lemma nb_boxes_used_le_one:
  forall b z0 l, In (b, z0) l ->
            (box_span z0 <= nb_boxes_used l)%nat.

Lemma in_bound_rep_aux:
  forall m b o,
    in_bound_m o m b ->
    0 <= o < __szmem.

Lemma in_bound_rep:
  forall m b o,
    in_bound_m o m b ->
    0 <= o < Int.max_unsigned.

Lemma mi_representable':
  forall sm m f m1 m2
         (MI: mem_inj sm m f m1 m2),
  forall b b' delta ofs
         (FB: f b = Some(b', delta))
         (PERM: in_bound_m (Int.unsigned ofs) m1 b \/
                in_bound_m (Int.unsigned ofs - 1) m1 b)
         (delta_pos: delta >= 0),
    0 <= Int.unsigned ofs + delta <= Int.max_unsigned.

Lemma mi_representable:
  forall sm m f m1 m2
         (MI: mem_inj sm m f m1 m2),
  forall b b' delta ofs
         (FB: f b = Some(b', delta))
         (PERM: perm m1 b (Int.unsigned ofs) Max Nonempty \/
                perm m1 b (Int.unsigned ofs - 1) Max Nonempty)
         (delta_pos: delta >= 0),
    0 <= Int.unsigned ofs + delta <= Int.max_unsigned.


Lemma meminj_no_overlap_impl:
  forall f m,
    Mem.meminj_no_overlap' f m ->
    Mem.meminj_no_overlap f m.

Definition is_dynamic_block m b :=
  (mem_blocktype m) # b = Some Dynamic.

Lemma is_block_dynamic_alloc:
  forall m lo hi m' b
    (AB: Mem.alloc m lo hi Normal = Some (m',b))
    b',
    Mem.is_dynamic_block m b' <-> Mem.is_dynamic_block m' b'.

Lemma is_block_dynamic_alloc':
  forall m lo hi m' b bt
    (AB: Mem.alloc m lo hi bt = Some (m',b))
    b' (diff: b <> b'),
    Mem.is_dynamic_block m b' <-> Mem.is_dynamic_block m' b'.

Lemma is_block_dynamic_storebytes:
  forall m b o l m'
    (AB: Mem.storebytes m b o l = Some m')
    b',
    Mem.is_dynamic_block m b' <-> Mem.is_dynamic_block m' b'.



Lemma is_block_dynamic_drop_perm:
  forall m b lo hi p m'
    (AB: Mem.drop_perm m b lo hi p = Some m')
    b',
    Mem.is_dynamic_block m b' <-> Mem.is_dynamic_block m' b'.



Lemma is_block_dynamic_unchfree:
  forall m b lo hi b',
    Mem.is_dynamic_block (Mem.unchecked_free m b lo hi) b' <-> Mem.is_dynamic_block m b'.



Lemma is_block_dynamic_free:
  forall m b lo hi b' m' (FREE: Mem.free m b lo hi = Some m'),
    Mem.is_dynamic_block m' b' <-> Mem.is_dynamic_block m b'.


Lemma is_block_dynamic_freelist:
  forall l m b' m' (FL: Mem.free_list m l = Some m'),
    Mem.is_dynamic_block m' b' <-> Mem.is_dynamic_block m b'.

Lemma size_block_snd:
  forall m2 b0,
    snd (Mem.bounds_of_block m2 b0) = Mem.size_block m2 b0.


Lemma size_block_unchecked_free:
  forall m b lo hi b',
    Mem.size_block (Mem.unchecked_free m b lo hi) b' =
    if eq_block b b'
    then let (lo',hi') := Mem.bounds_of_block m b in
         if zeq lo' lo && zeq hi' hi
         then 0
         else hi'
    else Mem.size_block m b'.



Ltac rewbnd :=
  try rewrite <- ! size_block_snd;
  repeat
    match goal with
      H: Mem.storebytes ?m ?b ?o ?l = Some ?m' |-
      context [Mem.bounds_of_block ?m' ?b'] =>
      rewrite <- (Mem.bounds_of_block_storebytes _ _ _ _ _ H b')
    | H: Mem.drop_perm ?m ?b ?lo ?hi ?p = Some ?m' |-
      context [Mem.bounds_of_block ?m' ?b'] =>
      rewrite <- (Mem.drop_perm_bounds _ _ _ _ _ _ H b')
    | H: Mem.alloc ?m ?lo ?hi ?bt = Some (?m',?b) |-
      context [Mem.bounds_of_block ?m' ?b] =>
      rewrite (Mem.bounds_of_block_alloc _ _ _ _ _ _ H)
    | H: Mem.alloc ?m ?lo ?hi ?bt = Some (?m',?b),
         H1: ?b <> ?b' |-
      context [Mem.bounds_of_block ?m' ?b'] =>
      rewrite <- (Mem.bounds_of_block_alloc_other _ _ _ _ _ _ H _ H1)
    | H: Mem.alloc ?m ?lo ?hi ?bt = Some (?m',?b),
         H1: ?b' <> ?b |-
      context [Mem.bounds_of_block ?m' ?b'] =>
      rewrite <- (Mem.bounds_of_block_alloc_other _ _ _ _ _ _ H _ (not_eq_sym H1))
    end;
  try rewrite ! size_block_snd.

Ltac rewmsk :=
  repeat
    match goal with
      H: Mem.storebytes ?m ?b ?o ?l = Some ?m' |-
      context [Mem.mask ?m' ?b'] =>
      rewrite <- (Mem.mask_storebytes _ _ _ _ _ H b')
    | H: Mem.drop_perm ?m ?b ?lo ?hi ?p = Some ?m' |-
      context [Mem.mask ?m' ?b'] =>
      rewrite <- (Mem.mask_drop_perm _ _ _ _ _ _ H b')
    | H: Mem.alloc ?m ?lo ?hi ?bt = Some (?m',?b) |-
      context [Mem.mask ?m' ?b] =>
      rewrite (Mem.alloc_mask _ _ _ _ _ _ H)
    | H: Mem.alloc ?m ?lo ?hi ?bt = Some (?m',?b),
         H1: ?b <> ?b' |-
      context [Mem.mask ?m' ?b'] =>
      rewrite <- (Mem.mask_alloc_other _ _ _ _ _ _ H _ H1)
    | H: Mem.alloc ?m ?lo ?hi ?bt = Some (?m',?b),
         H1: ?b' <> ?b |-
      context [Mem.mask ?m' ?b'] =>
      rewrite <- (Mem.mask_alloc_other _ _ _ _ _ _ H _ (not_eq_sym H1))
    end.

Ltac rewvb :=
  repeat
    match goal with
      H: Mem.storebytes ?m ?b ?o ?l = Some ?m' |-
      Mem.valid_block ?m' ?b' =>
      apply (Mem.storebytes_valid_block_1 _ _ _ _ _ H b')
    | H: Mem.drop_perm ?m ?b ?lo ?hi ?p = Some ?m' |-
      Mem.valid_block ?m' ?b' =>
      apply (Mem.drop_perm_valid_block_1 _ _ _ _ _ _ H)
    | H: Mem.alloc ?m ?lo ?hi _ = Some (?m',?b) |-
      Mem.valid_block ?m' ?b =>
      apply (Mem.valid_new_block _ _ _ _ _ _ H)
    | H: Mem.alloc ?m ?lo ?hi _ = Some (?m',?b),
         H1: ?b <> ?b' |-
      Mem.valid_block ?m' ?b' =>
      apply (Mem.valid_block_alloc _ _ _ _ _ _ H)
    | H: Mem.alloc ?m ?lo ?hi _ = Some (?m',?b),
         H1: ?b' <> ?b |-
      Mem.valid_block ?m' ?b' =>
      apply (Mem.valid_block_alloc _ _ _ _ _ _ H)
    | H: Mem.alloc ?m ?lo ?hi _ = Some (?m',?b)
      |-
      Mem.valid_block ?m' ?b' =>
      let i := fresh in
      set (i := b' <> b); exfalso
    end.




Lemma Forall_impl':
  forall {A : Type} (P Q : A -> Prop),
  forall l : list A,
    (forall a : A, In a l -> P a -> Q a) ->
    Forall P l -> Forall Q l.
Lemma size_block_free_list:
  forall l m b
    (F: Forall (fun x =>
                  let '(b,lo,hi) := x in
                  Mem.bounds_of_block m b = (lo,hi)) l)
    (lnr: list_norepet (map fst (map fst l)))
    m',
    Mem.free_list m l = Some m' ->
    Mem.size_block m' b =
    if in_dec peq b (map fst (map fst l))
    then 0
    else Mem.size_block m b.


Lemma bounds_of_block_free_list:
  forall l m b
    (F: Forall (fun x =>
                  let '(b,lo,hi) := x in
                  Mem.bounds_of_block m b = (lo,hi)) l)
    (lnr: list_norepet (map fst (map fst l)))
    m',
    Mem.free_list m l = Some m' ->
    Mem.bounds_of_block m' b =
    if in_dec peq b (map fst (map fst l))
    then (0,0)
    else Mem.bounds_of_block m b.




Lemma freelist_in_bound_m:
  forall l m m'
    (FL: Mem.free_list m l = Some m')
    o b
    (IB: Mem.in_bound_m o m' b),
    Mem.in_bound_m o m b.

Lemma freelist_perm:
  forall l m m'
    (FL: Mem.free_list m l = Some m')
    b o k p
    (NIN: ~ In b (map fst (map fst l)))
    (P: Mem.perm m b o k p),
    Mem.perm m' b o k p.

Lemma free_list_not_in_bound:
  forall l m m' (FL: Mem.free_list m l = Some m')
    o b (NIB: ~ Mem.in_bound_m o m b),
    ~ Mem.in_bound_m o m' b.

Lemma freelist_in_bound_m':
  forall l m m'
     (FL: Mem.free_list m l = Some m')
     (LNR: list_norepet (map fst (map fst l)))
    o b
    (IB: Mem.in_bound_m o m' b),
    (forall lo hi, In b (map fst (map fst l)) ->
              lo <= o < hi ->
              False).

Lemma uf_load:
  forall chunk m b o b' lo hi ,
    b <> b' ->
    Mem.load chunk (Mem.unchecked_free m b' lo hi) b o =
    Mem.load chunk m b o.

Lemma free_size:
  forall m b lo hi m'
    (FREE: Mem.free m b lo hi = Some m'),
  forall b',
    Mem.size_block m' b' <= Mem.size_block m b'.

Lemma lnr_remove:
  forall {A: Type} (eq: forall (a b: A), {a = b} + {a <> b}) (a: A) (l: list A),
    list_norepet l ->
    list_norepet (remove eq a l).

Lemma has_bounds_bounds:
  forall m b lo hi,
    Mem.has_bounds m b lo hi = true ->
    Mem.bounds_of_block m b = (lo,hi).

Lemma free_bounds_exact':
  forall m b lo hi m',
    Mem.free m b lo hi = Some m' ->
    Mem.bounds_of_block m b = (lo,hi).


Section INJECT.

  Variable sm : bool.
  Variable ei: meminj -> expr_sym -> expr_sym -> Prop.
  Hypothesis wf: wf_inj ei.



  Record inject' (f: meminj) (m1 m2: mem) : Prop :=
    mk_inject {
        mi_inj:
          mem_inj sm ei f 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_delta_pos: (* the mi_representable is derivable from mi_delta_pos and mi_inj *)
          forall b b' delta,
            f b = Some(b', delta) ->
            delta >= 0;
        mi_inj_dynamic:
          forall b b' delta,
            f b = Some (b',delta) ->
            (is_dynamic_block m1 b <-> is_dynamic_block m2 b') /\
            (is_dynamic_block m1 b -> delta = 0 /\ bounds_of_block m1 b = bounds_of_block m2 b') /\
            (is_dynamic_block m2 b' -> forall b'' delta', f b'' = Some (b', delta') -> b'' = b)
      }.

Definition inject := inject'.

Local Hint Resolve mi_mappedblocks: mem.

Lemma inject_meminj_no_overlap:
  forall f m1 m2,
    inject f m1 m2 ->
    meminj_no_overlap f m1.


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

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

Local Hint Resolve valid_block_inject_1 valid_block_inject_2: mem.

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

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

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

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

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


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

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

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

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

Theorem valid_pointer_inject_val:
  forall f m1 m2 b ofs b' ofs',
  inject f m1 m2 ->
  valid_pointer m1 b (Int.unsigned ofs) = true ->
  ei f (Eval (Vptr b ofs)) (Eval (Vptr b' ofs')) ->
  valid_pointer m2 b' (Int.unsigned ofs') = true.

Theorem weak_valid_pointer_inject_val:
  forall f m1 m2 b ofs b' ofs',
  inject f m1 m2 ->
  weak_valid_pointer m1 b (Int.unsigned ofs) = true ->
  ei f (Eval (Vptr b ofs)) (Eval (Vptr b' ofs')) ->
  weak_valid_pointer m2 b' (Int.unsigned ofs') = true.

Theorem inject_no_overlap:
  forall f m1 m2 b1 b2 b1' b2' delta1 delta2 ofs1 ofs2,
  inject f 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 m m' b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
  inject f m m' ->
  b1 <> b2 ->
  valid_pointer m b1 (Int.unsigned ofs1) = true ->
  valid_pointer m b2 (Int.unsigned ofs2) = true ->
  f b1 = Some (b1', delta1) ->
  f b2 = Some (b2', delta2) ->
  b1' <> b2' \/
  Int.unsigned (Int.add ofs1 (Int.repr delta1)) <>
  Int.unsigned (Int.add ofs2 (Int.repr delta2)).

Require Intv.

Theorem disjoint_or_equal_inject:
  forall f m m' b1 b1' delta1 b2 b2' delta2 ofs1 ofs2 sz,
  inject f 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 m m' b ofs al sz b' delta,
  inject f 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 m1 m2 chunk b1 ofs b2 delta v1,
  inject f m1 m2 ->
  load chunk m1 b1 ofs = Some v1 ->
  f b1 = Some (b2, delta) ->
  exists v2, load chunk m2 b2 (ofs + delta) = Some v2 /\ ei f v1 v2.

Lemma alloc_0_inject:
  forall tm1 tm2 sp f1 m2 bt,
    alloc tm1 0 0 bt = Some (tm2, sp) ->
    inject f1 m2 tm1 ->
    inject f1 m2 tm2.

Lemma compat_wider:
  forall m m'
         (bw : forall b o, in_bound_m o m b -> in_bound_m o m' b)
         (ms: forall b, nat_mask m b = nat_mask m' b)
         cm q
         (COMP: compat_m m' q cm),
    compat_m m q cm.



Lemma abi_in_bound:
  forall f m b o
         (ABI : all_blocks_injected f m)
         (IB : in_bound (Int.unsigned o) (bounds_of_block m b))
         (Fnone : f b = None),
    False.


Lemma compat_inject:
  forall f m m'
         (ABI: all_blocks_injected f m)
         (INJ : inject f m m')
         cm q
         (COMP: compat_m m' q cm),
    compat_m m q (Val.inj_alloc cm f).

Lemma is_norm_m_is_norm:
  forall m e v,
    is_norm_m m e v ->
    IsNorm.t (bounds_of_block m) (nat_mask m) e v.

Lemma tpMA_not_null:
  Int.zero = Int.repr (two_power_nat MA) -> False.

Lemma inject_dep:
  forall f m e e' b
    (EI: expr_inj f e e')
    (DEP: depends Int.max_unsigned (bounds_of_block m) (nat_mask m) e b),
    f b <> None.

Lemma not_injected_not_dep:
  forall f m m' e1 e1' b i (ABI : all_blocks_injected f m)
    (INJ : inject f m m') (EI : ei f e1 e1')
    (N : is_norm_m m e1 (Vptr b i)) (Fnone : f b = None), False.

Lemma norm_inject:
  forall f m m' e1 v1 e1'
         (ABI: all_blocks_injected f m)
         (INJ: inject f m m')
         (EI: ei f e1 e1')
         (NU: v1 <> Vundef),
  forall (MN:mem_norm m e1 = v1),
    mem_norm m' e1' <> Vundef /\
    ei f (Eval v1) (Eval (mem_norm m' e1')).

Lemma ei_vi_norm:
  forall f v1 v2 m m',
    all_blocks_injected f m ->
    inject f m m' ->
    ei f (Eval (mem_norm m v1)) (Eval v2) ->
    val_inject f (mem_norm m v1) v2.

Lemma norm_inject_val':
  forall f m m' e1 e1'
         (ABI: all_blocks_injected f m)
         (INJ: inject f m m')
         (EI: ei f e1 e1'),
    val_inject f (mem_norm m e1) (mem_norm m' e1').


Lemma sgn_lt:
  forall a, a > 0 -> Z.sgn a = 1.

Lemma sgn_le:
  forall a, a >= 0 -> Z.sgn a = 1 \/ Z.sgn a = 0.

Lemma propZ:
  forall (a b c d:Z),
    a = b -> c = d ->
    a = c ->
    b = d.

Lemma align_ge2:
  forall al z,
    al > 0 ->
    align z al = z + (al - 1 - (z-1) mod al).

Lemma sgn_gt x:
  Z.sgn x = 1 -> x > 0.

Lemma zpos_of_nat : forall n,
    Z.pos (Pos.of_nat n) = Z.max 1 (Z.of_nat n).
    
Lemma filter_mbla_ext:
  forall sz n p p' (P: forall b, Ple b (Pos.of_nat n) -> p b = p' b),
    filter (fun x => p (fst x)) (mk_block_list_aux sz n) =
    filter (fun x => p' (fst x)) (mk_block_list_aux sz n).

Theorem loadv_inject:
  forall f m1 m2 chunk a1 a2 v1
    (ABI: all_blocks_injected f m1)
    (MINJ: inject f m1 m2),
    loadv chunk m1 a1 = Some v1 ->
    ei f a1 a2 ->
    exists v2, loadv chunk m2 a2 = Some v2 /\ ei f v1 v2.

Theorem loadbytes_inject:
  forall f m1 m2 b1 ofs len b2 delta bytes1,
  inject f 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 ei f) bytes1 bytes2.


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

Theorem storev_inject:
  forall f m1 m2 chunk a1 a2 b1 b2 v1
    (ABI: all_blocks_injected f m1),
    inject f m1 m2 ->
    storev chunk m1 a1 b1 = Some v1 ->
    ei f a1 a2 ->
    ei f b1 b2 ->
    exists v2, storev chunk m2 a2 b2 = Some v2 /\ inject f v1 v2.

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

Theorem store_outside_inject:
  forall f m1 m2 chunk b ofs v m2',
  inject f 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 m1 m2'.

Theorem storev_mapped_inject:
  forall f chunk m1 a1 v1 n1 m2 a2 v2
    (ABI: all_blocks_injected f m1),
  inject f m1 m2 ->
  storev chunk m1 a1 v1 = Some n1 ->
  ei f a1 a2 ->
  ei f v1 v2 ->
  exists n2,
    storev chunk m2 a2 v2 = Some n2 /\ inject f n1 n2.

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

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

Theorem storebytes_outside_inject:
  forall f m1 m2 b ofs bytes2 m2',
  inject f 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 m1 m2'.

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

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

Lemma alloc_in_bound':
  forall m1 lo hi m2 b bt (ALLOC: alloc m1 lo hi bt = Some (m2, b)) b0 o,
    in_bound_m o m1 b0 ->
    in_bound_m o m2 b0.

Lemma alloc_in_bound_old:
  forall m1 lo hi m2 b bt (ALLOC: alloc m1 lo hi bt = Some (m2, b)) b0 o (diff: b <> b0),
    in_bound_m o m2 b0 ->
    in_bound_m o m1 b0.

Lemma ioa_div:
  forall sz delta,
    inj_offset_aligned delta sz ->
    (two_p (Z.of_nat (alignment_of_size sz)) | delta).
 
Definition align_distr := align_distr.

Opaque align.


Lemma alloc_less_ok:
  forall m z z0 bt,
    Mem.alloc m 0 z bt = None ->
    Mem.alloc m 0 z0 bt <> None ->
    0 <= z <= z0 ->
    False.

Lemma alloc_parallel_inj:
  forall f m1 m2 lo hi m1' b1 m b bt
         (INJ: inject f m1 m2)
         (ALLOC: alloc m1 lo hi bt = Some (m1', b1))
         (HIpos : hi >= 0)
         (ALLOC2 : alloc m2 lo hi bt = Some (m, b)),
    mem_inj sm ei (fun b0 : positive => if peq b0 b1 then Some (b, 0) else f b0) m1' m.

Lemma alloc_none_too_many_boxes:
  forall m lo hi bt (ALLOC: alloc m lo hi bt = None),
    Z.of_nat (nb_boxes_used_m m + box_span (Z.max 0 hi))%nat >= nb_boxes_max.

Lemma wfm_alloc: forall m, Z.of_nat (nb_boxes_used_m m) < nb_boxes_max.

Theorem alloc_parallel_inject:
  forall f m1 m2 lo1 hi1 m1' b1 (ORD: lo1 <= hi1) bt
    (INJ: inject f m1 m2)
    (ALLOC: alloc m1 lo1 hi1 bt = Some (m1', b1))
    (HIpos: hi1 >= 0)
    (SM: sm = true),
  exists f', exists m2', exists b2,
        alloc m2 lo1 hi1 bt = Some (m2', b2)
        /\ inject f' m1' m2'
        /\ inject_incr f f'
        /\ f' b1 = Some(b2, 0)
        /\ (forall b, b <> b1 -> f' b = f b).


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).

Lemma drop_outside_inject:
  forall f m1 m2 b lo hi p m2',
    inject f 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 m1 m2'.


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

Definition inject_neutral (thr: block) (m: mem) :=
  mem_inj sm ei (flat_inj thr) m m.

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)) m m.

Theorem empty_inject_neutral:
  forall thr, inject_neutral thr empty.

Theorem alloc_inject_neutral:
  forall thr m lo hi b m' bt
         (ALLOC: alloc m lo hi bt = Some (m', b))
         (LO: lo <= 0)
         (INJ: inject_neutral thr m)
         (LT: 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 ->
  ei (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'.

End INJECT.

Definition one2oneinject (f: meminj) :=
  forall b b' delta, f b = Some (b', delta) -> delta = 0.
  

Invariance properties between two memory states

Section UNCHANGED_ON.

Variable P: block -> Z -> Prop.

Record unchanged_on (m_before m_after: mem) : Prop := mk_unchanged_on {
  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))
}.

Lemma unchanged_on_refl:
  forall m, unchanged_on m m.

Lemma perm_unchanged_on:
  forall m m' b ofs k p,
  unchanged_on m m' -> P b ofs -> valid_block m b ->
  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 m m' -> P b ofs -> valid_block m b ->
  perm m' b ofs k p -> perm m b ofs k p.

Lemma loadbytes_unchanged_on_1:
  forall m m' b ofs n,
  unchanged_on 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 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 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 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 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 m m'.

Lemma alloc_unchanged_on:
  forall m lo hi m' b bt,
  alloc m lo hi bt = Some (m', b) ->
  unchanged_on 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 m m'.

End UNCHANGED_ON.



End Mem.

Notation mem := Mem.mem.



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

Hint Resolve
  Mem.valid_not_valid_diff
  Mem.perm_implies
  Mem.perm_cur
  Mem.perm_max
  Mem.perm_valid_block
  Mem.range_perm_implies
  Mem.range_perm_cur
  Mem.range_perm_max
  Mem.valid_access_implies
  Mem.valid_access_valid_block
  Mem.valid_access_perm
  Mem.valid_access_load
  Mem.load_valid_access
  Mem.loadbytes_range_perm
  Mem.valid_access_store
  Mem.perm_store_1
  Mem.perm_store_2
  Mem.nextblock_store
  Mem.store_valid_block_1
  Mem.store_valid_block_2
  Mem.store_valid_access_1
  Mem.store_valid_access_2
  Mem.store_valid_access_3
  Mem.storebytes_range_perm
  Mem.perm_storebytes_1
  Mem.perm_storebytes_2
  Mem.storebytes_valid_access_1
  Mem.storebytes_valid_access_2
  Mem.nextblock_storebytes
  Mem.storebytes_valid_block_1
  Mem.storebytes_valid_block_2
  Mem.nextblock_alloc
  Mem.alloc_result
  Mem.valid_block_alloc
  Mem.fresh_block_alloc
  Mem.valid_new_block
  Mem.perm_alloc_1
  Mem.perm_alloc_2
  Mem.perm_alloc_3
  Mem.perm_alloc_4
  Mem.perm_alloc_inv
  Mem.valid_access_alloc_other
  Mem.valid_access_alloc_same
  Mem.valid_access_alloc_inv
  Mem.range_perm_free
  Mem.free_range_perm
  Mem.nextblock_free
  Mem.valid_block_free_1
  Mem.valid_block_free_2
  Mem.perm_free_1
  Mem.perm_free_2
  Mem.perm_free_3
  Mem.valid_access_free_1
  Mem.valid_access_free_2
  Mem.valid_access_free_inv_1
  Mem.valid_access_free_inv_2
  Mem.unchanged_on_refl
: mem.