Module Memory


This file develops the memory model that is used in the dynamic semantics of all the languages used in the compiler. It defines a type mem of memory states, the following 4 basic operations over memory states, and their properties:

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

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.

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').
Proof.
  intros.
  unfold align.
  elim_div.
  generalize (two_power_nat_pos al) (two_power_nat_pos al'). intuition.
  assert (EQ: two_power_nat al' = two_power_nat al * two_power_nat (al' - al)).
  rewrite ! two_power_nat_two_p. rewrite <- two_p_is_exp; try lia.
  f_equal. lia.
  generalize (two_power_nat_pos (al' - al)).
  rewrite EQ in *. clear EQ.
  generalize dependent (two_power_nat (al' - al)). intros.
  assert (x = two_power_nat al * z1 + z2 - two_power_nat al + 1) by lia. subst.
  clear H2.
  assert (z0 = z1 * two_power_nat al + two_power_nat al * z5 - 1 - two_power_nat al * z5 * z) by lia.
  subst. clear H3.
  assert (two_power_nat al * z1 + z2 - two_power_nat al + 1 +
          two_power_nat al * z5 - 1 - two_power_nat al * z5 * z3 = z4) by lia. clear H1. subst.
  generalize dependent (two_power_nat al). intros.
  f_equal.
  remember (z1 - z5 * z3 - 1) as V1.
  assert (V1 = 0 \/ V1 < 0 \/ V1 > 0) by lia.
  intuition ; try nia.
Qed.


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.
Proof.
  apply two_power_nat_pos.
Qed.


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.
Proof.
  unfold Int.max_unsigned. f_equal.
  rewrite ! two_power_nat_two_p.
  rewrite <- two_p_is_exp by lia.
  rewrite <- Nat2Z.inj_add.
  rewrite <- two_power_nat_two_p.
  unfold Int.modulus. f_equal.
  change Int.wordsize with 32%nat.
  rewrite NPeano.Nat.add_sub_assoc.
  rewrite NPeano.Nat.add_sub_swap by lia. lia. generalize MA_bound; lia.
Qed.


Lemma box_span_mul z:
  box_span (two_power_nat MA * z - 1) = Z.to_nat z.
Proof.
  unfold box_span.
  generalize (BigNumPrelude.Z_div_plus_l z (two_power_nat MA) (-2) (Z.gt_lt _ _ tpMA_pos)).
  intros.
  replace (two_power_nat MA * z - 1 - 1) with (z* two_power_nat MA + -2) by lia. rewrite H.
  f_equal. cut (-2 / two_power_nat MA = -1). intro A; rewrite A. lia.
  unfold Z.div. simpl.
  generalize tpMA_pos.
  intros. Opaque two_power_nat. repeat destr.
  apply Z.leb_le in Heqb.
  apply Z.ltb_ge in Heqb0. assert (two_power_nat MA = 2) by lia. rewrite H1 in *. simpl in *. inv Heqp; auto.
  apply Z.leb_gt in Heqb. apply Z.ltb_lt in Heqb0. assert (two_power_nat MA = 1) by lia.
  rewrite H1 in *.
  assert (MA < S O)%nat. des (lt_dec MA 1).
  generalize (two_p_monotone (Z.of_nat 1) (Z.of_nat MA)).
  intro A; trim A. split. lia. apply inj_le. rewrite NPeano.Nat.le_ngt. auto.
  rewrite <- ! two_power_nat_two_p in A. change (two_power_nat 1) with 2 in A. lia.
  generalize MA_bound; lia.
  apply Z.ltb_ge in Heqb0. clear - Heqb0.
  generalize tpMA_pos. lia.
Qed.

Lemma tpMA_sup8:
  8 <= two_power_nat MA.
Proof.
  change 8 with (two_power_nat 3).
  rewrite ! two_power_nat_two_p.
  apply two_p_monotone. generalize MA_bound. lia.
Qed.


Lemma tpMA'_sup8:
  8 <= two_power_nat (32-MA).
Proof.
  change 8 with (two_power_nat 3).
  rewrite ! two_power_nat_two_p.
  apply two_p_monotone. generalize MA_bound. lia.
Qed.


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


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.
Proof.
  intros. apply bounds_mask_consistency; auto.
  apply msk_valid; auto.
Qed.


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.

The mask of a block is
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.

alloc_mem computes a concrete memory for memory m. size_mem is the first available address after the allocation of m.



Normalisation in a given memory. This is what is called normalise in the paper.

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'.
Proof.
  red; intros; eauto.
Qed.

Lemma same_eval_eqm:
  forall m v1 v2,
    same_eval v1 v2 ->
    Mem.mem_norm m v1 = Mem.mem_norm m v2.
Proof.
  intros m v1 v2 A.
  apply Normalise.norm_eq''; eauto.
  eapply same_eval_same_eval_on; eauto.
Qed.

Lemma lessdef_eqm:
  forall m v1 v2,
    Val.lessdef v1 v2 ->
    Values.Val.lessdef (mem_norm m v1) (mem_norm m v2).
Proof.
  intros m v1 v2 LD.
  apply NormaliseSpec.normalise_ld.
  apply norm_correct.
  apply norm_complete.
  red; intros; eauto.
Qed.


Encoding functions (from Memdata) are also morphisms for same_eval.


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'.
Proof.
  red; intros; eauto.
Qed.

Ltac unfsize :=
  IntFacts.unfsize.

Lemma size31_inf:
  comp_size M31 <= Int.max_unsigned.
Proof.
  Opaque two_power_nat.
  simpl. unfsize.
  generalize (two_power_nat_pos MA); lia.
Qed.

Lemma fold_left_plus_rew:
  forall l n,
    (fold_left plus l n = fold_left plus l O + n)%nat.
Proof.
  induction l; simpl; intros; auto.
  rewrite (IHl (n + a))%nat.
  rewrite (IHl a). lia.
Qed.


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.
Proof.
  simpl. auto.
Qed.


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'.
Proof.
  intros.
  inv IBL; constructor; auto.
  + eapply permutation_norepet. apply Permutation_map. apply PERM. auto.
  + intros. apply ibl_size0. rewrite perm_in. eauto. auto.
  + apply Permutation_length. apply Permutation_sym; auto.
  + intros. rewrite perm_in. eauto. apply Permutation_sym; auto.
Qed.

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.
Proof.
  intros sz n l IBL'.
  exploit (ibl_valid _ _ _ IBL' (Pos.of_nat (S n))). rewrite Nat2Pos.id; auto.
  intro H. apply in_split in H.
  destruct H as (l1 & l2 & SUBST); subst.
  exists (l1 ++ l2).
  split.
  - eapply is_block_list_permut in IBL'.
    2: apply Permutation_sym, Permutation_middle.
    inv IBL'. Opaque Pos.of_nat.
    simpl in *. inv ibl_lnr0. inv ibl_length0.
    constructor; auto.
    intros.
    exploit (ibl_valid0 b). lia. intros [A|A].
    inv A. rewrite Nat2Pos.id in H. lia. lia. auto.
  - apply Permutation_middle.
Qed.


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'.
Proof.
  induction n; simpl; intros.
  - inv IBL; inv IBL'. des l; des l'. constructor.
  - apply is_block_list_S in IBL.
    apply is_block_list_S in IBL'.
    dex. destr. rewrite <- H0, <- H2. apply perm_skip.
    eauto.
Qed.

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).
Proof.
  induction n; simpl; intros.
  - inv H; des l. unfold mk_block_list_aux. constructor.
  - rewrite mbla_rew. apply is_block_list_S in H.
    destruct H as (l' & IBL & PERM).
    apply IHn in IBL. rewrite <- PERM. apply perm_skip. auto.
Qed.

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'.
Proof.
  intros.
  apply is_block_list_S in IBL'. dex; destr. rewrite <- H0. apply perm_skip.
  eapply is_block_list_is_permut; eauto.
Qed.

Lemma fold_left_plus_permut:
  forall l l' (PERM: Permutation l l') n,
    fold_left plus l n = fold_left plus l' n.
Proof.
  induction 1; simpl; intros; auto.
  - f_equal. lia.
  - congruence.
Qed.

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.
Proof.
  Opaque Pos.of_nat.
  unfold nb_boxes_used.
  simpl.
  intros.
  eapply is_block_list_S' in H0; eauto.
  erewrite <- fold_left_plus_permut. 2: apply Permutation_map. 2: eassumption.
  simpl.
  rewrite fold_left_plus_rew. reflexivity.
Qed.

Lemma nb_boxes_used_thr:
  forall l curbox curalloc,
    make_box_allocation l = (curbox, curalloc) ->
    (nb_boxes_used l = curbox)%nat.
Proof.
  induction l.
  simpl; intros. inv H. reflexivity.
  intros. destruct a.
  rewrite make_box_allocation_cons in H.
  Opaque Pos.of_nat.
  des (make_box_allocation l). inv H.
  unfold nb_boxes_used in *. simpl.
  rewrite fold_left_plus_rew. erewrite IHl. 2: eauto. auto.
Qed.

Lemma make_box_allocation_le:
  forall l curbox curalloc,
    make_box_allocation l = (curbox, curalloc) ->
    forall b, (curalloc b <= curbox)%nat.
Proof.
  induction l; simpl; intros.
  - inv H; auto.
  - des (make_box_allocation l). des a. inv H.
    specialize (IHl _ _ eq_refl).
    destr. lia. specialize (IHl b). lia.
Qed.

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.
Proof.
  induction l; simpl; intros.
  - easy.
  - des (make_box_allocation l). des a. inv H. inv H0.
    specialize (IHl _ _ H5 eq_refl).
    des H1. inv e. rewrite peq_true. lia.
    destr. subst.
    exfalso; apply H4. rewrite in_map_iff. eexists; split; eauto. reflexivity.
    specialize (IHl _ _ i). lia.
Qed.

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.
Proof.
  induction l; simpl; intros.
  - easy.
  - des a. des (make_box_allocation l). inv H0.
    inv H.
    specialize (IHl _ _ H3 eq_refl).
    repeat destr.
    + subst. assert (z = sz1). des i1. exfalso; apply H2. rewrite in_map_iff. eexists; split; eauto. reflexivity. subst.
      clear i1. des i2.
      right; eapply make_box_allocation_le_in; eauto.
    + subst. assert (z = sz2). des i2. exfalso; apply H2. rewrite in_map_iff. eexists; split; eauto. reflexivity. subst.
      clear i2. des i1.
      left; eapply make_box_allocation_le_in; eauto.
    + des i1. des i2. eauto.
Qed.

Lemma minus_1_div_eq:
  forall z, z > 0 -> -1 / z = -1.
Proof.
  unfold Z.div. simpl. intros.
  des z. lia.
  destr. lia.
Qed.

Lemma box_span_align:
  forall z,
    z >= 0 ->
    two_power_nat MA * Z.of_nat (box_span z) = align z (two_power_nat MA).
Proof.
  unfold box_span, align.
  intros.
  generalize (BigNumPrelude.Z_div_plus_l 1 (two_power_nat MA) (z-1) (Z.gt_lt _ _ tpMA_pos)).
  rewrite Z2Nat.id.
  intros. rewrite Z.add_comm. rewrite <- H0.
  rewrite Z.mul_comm. f_equal. f_equal. lia.
  destruct (zlt 0 z).
  generalize (Z.div_pos (z-1) (two_power_nat MA)). intro A. trim A. lia. trim A.
  generalize tpMA_pos. lia. lia.
  assert (z = 0) by lia. subst. simpl.
  rewrite minus_1_div_eq. lia. apply tpMA_pos.
Qed.


Lemma s31_ma:
  comp_size M31 = two_power_nat MA * (two_power_nat (32 - MA) - 1) - 1.
Proof.
  unfold comp_size. rewrite s32_ma. lia.
Qed.

Lemma lt_le_minus1:
  forall a b : Z,
    a < b ->
    a <= b - 1.
Proof.
  intros. lia.
Qed.

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.
Proof.
  intros.
  assert (Pos.to_nat b <= pred (Pos.to_nat (nextblock m)))%nat.
  {
    destruct (plt b (nextblock m)).
    apply Pos2Nat.inj_lt in p. lia.
    unfold bounds_of_block in H.
    rewrite bounds_mask_consistency in H.
    unfold in_bound in H; simpl in H; lia.
    apply msk_valid; auto.
  }
  split. rewrite perm_in. apply mbla_below_in'. apply H1.
  apply is_block_list_permut_mk_block_list. eauto.
  split.
  red in H.
  eapply Z.lt_le_trans. apply H.
  unfold size_block, get_size, bounds_of_block.
  destr. des p. eapply bounds_lo_inf0 in Heqo0. destruct Heqo0; subst. rewrite Z.sub_0_r.
  rewrite box_span_align. apply align_le. apply tpMA_pos. auto.
  unfold box_span. simpl. rewrite minus_1_div_eq. simpl. lia. apply tpMA_pos.
  red in H.
  revert H.
  unfold size_block, get_size, bounds_of_block.
  destr. des p. eapply bounds_lo_inf0 in Heqo0. destruct Heqo0; subst. rewrite Z.sub_0_r. lia. lia.
Qed.

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.
Proof.
  intros. split.
  * apply Z.lt_le_incl. apply Z.mul_pos. left. split. generalize tpMA_pos. lia. lia.
  * exploit in_bound_in_mk. eauto. eauto. intros [IN RNG].
    generalize (make_box_allocation_le_in _ _ _ (ibl_lnr _ _ _ IBL) MBA _ _ IN).
    intros LE.
    rewrite s32_ma.
    apply lt_le_minus1.
    rewrite <- Z.mul_lt_mono_pos_l. 2: generalize tpMA_pos; lia.
    cut (Z.of_nat (ba b) < two_power_nat (32 - MA) - 1). lia.
    eapply Z.le_lt_trans with (Z.of_nat thr). apply inj_le. lia.
    apply Nat2Z.inj_lt in THR. eapply Z.lt_le_trans. eauto.
    unfold nb_boxes_max.
    rewrite Z2Nat.id. lia.
    generalize tpMA'_sup8; lia.
Qed.

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.
Proof.
  intros.
  rewrite Int.unsigned_repr.
  + split.
    * change 0 with (0+0). apply Z.add_lt_le_mono.
      apply Z.mul_pos_pos. generalize tpMA_pos. lia.
      lia.
      generalize (Int.unsigned_range o). lia.
    * exploit in_bound_in_mk. eauto. eauto. intros [IN [RNG POS]].
      generalize (make_box_allocation_le_in _ _ _ (ibl_lnr _ _ _ IBL) MBA _ _ IN).
      intro LE.
      eapply Z.lt_le_trans.
      apply Z.add_lt_mono_l. eauto.
      transitivity (two_power_nat MA * (1 + Z.of_nat (ba b + box_span (size_block m b))%nat)).
      rewrite Nat2Z.inj_add. lia.
      eapply Z.le_trans.
      apply Z.mul_le_mono_nonneg_l. generalize tpMA_pos; lia.
      apply Z.add_le_mono_l. apply Nat2Z.inj_le. eauto.
      rewrite s31_ma.
      apply lt_le_minus1.
      rewrite <- Z.mul_lt_mono_pos_l. 2: generalize tpMA_pos; lia.
      cut (Z.of_nat thr < two_power_nat (32 - MA) - 2). lia.
      eapply Z.lt_le_trans. apply inj_lt. eauto.
      unfold nb_boxes_max.
      rewrite Z2Nat.id. lia.
      generalize tpMA'_sup8; lia.
  + eapply box_alloc_unsigned_range; eauto.
Qed.

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.
Proof.
  intros.
  exploit box_alloc_in_range; eauto. intros. split. lia.
  generalize size31_inf; lia.
Qed.

Lemma zlt_neq: forall a b : Z, a < b -> a <> b.
Proof.
  intros. intro; subst. lia.
Qed.

Lemma zgt_neq: forall a b : Z, b < a -> a <> b.
Proof.
  intros. intro; subst. lia.
Qed.

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).
Proof.
  intros; split.
  - unfold box_alloc_to_cm. intros. rewrite Int.add_unsigned.
    cut ( 0 < Int.unsigned (Int.repr (two_power_nat MA * (Z.of_nat (ba b) + 1))) + Int.unsigned o < comp_size M31).
    {
      intro.
      rewrite Int.unsigned_repr; auto. split. lia. transitivity (comp_size M31). lia. apply size31_inf.
    }
    eapply box_alloc_in_range;eauto.
  - intros.
    exploit in_bound_in_mk. apply H0. eauto. intros (IN & RNG & POS).
    exploit in_bound_in_mk. apply H1. eauto. intros (IN' & RNG' & POS').
    generalize (make_box_allocation_disjoint
                  _ _ _
                  (ibl_lnr _ _ _ IBL) MBA _ _ _ _ IN IN' H POS POS').
    unfold box_alloc_to_cm. intros. rewrite ! Int.add_unsigned.
    rewrite Int.unsigned_repr. 2: eapply box_alloc_in_range'; eauto.
    rewrite (Int.unsigned_repr (Int.unsigned _ + _)). 2: eapply box_alloc_in_range'; eauto.
    rewrite Int.unsigned_repr. 2: eapply box_alloc_unsigned_range; eauto.
    rewrite Int.unsigned_repr. 2: eapply box_alloc_unsigned_range; eauto.
    cut (two_power_nat MA * (Z.of_nat (ba b)) + Int.unsigned o <> two_power_nat MA * (Z.of_nat (ba b')) + Int.unsigned o').
    lia.
    destruct H2.
    + apply zlt_neq.
      eapply Z.lt_le_trans. apply Z.add_lt_mono_l. apply RNG.
      transitivity (two_power_nat MA * Z.of_nat (ba b')).
      apply inj_le in H2. apply Z.mul_le_mono_nonneg_l with (p := two_power_nat MA) in H2. lia. generalize tpMA_pos; lia.
      generalize (Int.unsigned_range o'); lia.
    + apply zgt_neq.
      eapply Z.lt_le_trans. apply Z.add_lt_mono_l. apply RNG'.
      transitivity (two_power_nat MA * Z.of_nat (ba b)).
      apply inj_le in H2. apply Z.mul_le_mono_nonneg_l with (p := two_power_nat MA) in H2. lia. generalize tpMA_pos; lia.
      generalize (Int.unsigned_range o); lia.
  - intros. unfold box_alloc_to_cm.
    generalize (Z.of_nat (ba b) + 1). intro.
    unfold nat_mask, mask.
    Opaque minus.
    destr.
    + exploit alignment_ok. eauto. intros [NMA AOS].
      solve_int.
      rewrite Int.bits_not; auto.
      rewrite ! Int.testbit_repr; auto.
      rewrite ! two_power_nat_two_p.
      rewrite Int.Ztestbit_two_p_m1; auto; try omega.
      destr; try ring.
      generalize (Int.Ztestbit_mod_two_p (Z.of_nat MA) (two_p (Z.of_nat MA) * z) i).
      destr; try omega.
      intro H. rewrite <- H; auto with zarith.
      rewrite Z.mul_comm. rewrite Z.mod_mul; auto.
      rewrite Int.Ztestbit_0. reflexivity. generalize tpMA_pos. rewrite two_power_nat_two_p.
      lia.
    + change (two_power_nat 0 - 1) with 0.
      change (Int.repr 0) with Int.zero.
      rewrite Int.not_zero. rewrite Int.and_mone. auto.
Qed.

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'.
Proof.
  intros.
  apply fold_left_plus_permut. apply Permutation_map. auto.
Qed.

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).
Proof.
  intros.
  generalize (wfm_alloc_ok m).
  intros. unfold mk_cm.
  des (make_box_allocation l).
  destr.
  - eexists; split; eauto.
    eapply box_alloc_to_cm_compat. 3: eauto. apply Nat2Z.inj_lt. rewrite Nat2Z.inj_add in l0.
    rewrite Z2Nat.id. lia. lia. auto.
  - eapply nb_boxes_used_thr in Heqp.
    subst.
    erewrite nb_used_permut in H. apply g in H. easy.
    apply Permutation_sym, is_block_list_permut_mk_block_list; auto.
Qed.

Lemma length_mbla:
  forall sz n, length (mk_block_list_aux sz n) = n.
Proof.
  induction n; simpl; intros. auto. rewrite <- IHn at 2.
  f_equal.
Qed.

Lemma is_block_list_mk_block_list:
  forall sz n,
    is_block_list sz n (mk_block_list_aux (get_size sz) n).
Proof.
  intros.
  constructor.
  apply mbla_norepet.
  intros; symmetry; eapply mbla_in; eauto.
  apply length_mbla.
  eapply mbla_below_in'.
Qed.

Lemma concrete_mem':
  forall m, exists al, compat_m m M31 al.
Proof.
  intros.
  edestruct (alloc_compat m) as [al [A B]].
  apply is_block_list_mk_block_list.
  eexists; eauto.
Qed.

Lemma compat31_32:
  forall m cm, compat_m m M31 cm -> compat_m m M32 cm.
Proof.
  intros.
  eapply compat_larger. 2: eauto.
  simpl. generalize (two_power_nat_pos MA); lia.
Qed.

Lemma concrete_mem:
  forall m, exists al, compat_m m M32 al.
Proof.
  intros.
  destruct (concrete_mem' m) as [al A].
  exists al. eapply compat31_32; eauto.
Qed.


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).
Proof.
  intros.
  apply Normalise.norm_complete.
  inv INM; constructor; auto.
Qed.

Lemma norm_correct:
  forall m e,
    is_norm_m m e (mem_norm m e).
Proof.
  intros.
  destruct (Normalise.norm_correct (bounds_of_block m) (nat_mask m) e).
  constructor; auto.
Qed.

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).
Proof.
  intros.
  destruct (norm_correct m e).
  subst.
  apply eval_ok_m0; auto.
Qed.

Lemma norm_gr:
  forall m e,
    good_result_m m e (mem_norm m e).
Proof.
  intros. apply norm_gr.
Qed.

Lemma eq_norm:
  forall m e v,
    is_norm_m m e v ->
    v <> Vundef ->
    Mem.mem_norm m e = v.
Proof.
  intros m e v IS.
  generalize (norm_complete m e v IS). intro A; inv A; destr.
Qed.

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.
Proof.
  split; eapply compat_same_bounds; eauto.
Qed.

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.
Proof.
  split; red; intros; des v;
  red; intros.
  eapply MR in COMP; eauto.
  eapply MR in COMP'; eauto.
  apply H; auto.
  setoid_rewrite <- MR; eauto.
  setoid_rewrite <- MR; eauto.
Qed.

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.
Proof.
  intros.
  generalize (good_result_m_same_compat _ _ e v C).
  intros GR.
  split; intros INM; inv INM; constructor.
  - eapply lessdef_on_P_impl; eauto.
    intros; rewrite C; eauto.
  - eapply lessdef_on_P_impl; eauto.
    intros; rewrite <- C; eauto.
Qed.

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.
Proof.
  intros.
  generalize (norm_correct m1 e) (norm_correct m2 e).
  intros A B.
  generalize (same_compat_bounds_mask _ _ Bnds Msk); intro SC; clear Bnds Msk.
  apply lessdef_antisym; apply norm_complete.
  rewrite <- is_norm_m_same_compat; eauto.
  rewrite is_norm_m_same_compat; eauto.
Qed.


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.
Proof.
  intros; apply in_bound_dec.
Defined.


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}.
Proof.
  decide equality.
Qed.

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.
Proof.
  induction l1; simpl. auto.
  destr.
Qed.

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.
Proof.
  induction l; simpl; intros; auto.
  destr.
Qed.

Lemma put_front_permut:
  forall b sz bl (IN: In (b,sz) bl)
    (LNR: list_norepet bl),
    Permutation bl (put_front bl b sz).
Proof.
  intros.
  cut (exists a c, bl = a ++ (b,sz) :: c).
  clear IN.
  intros [a [c EQ]].
  subst.
  apply list_norepet_app in LNR.
  destruct LNR as [LNRA [LNRB LDSIJ]].
  inversion LNRB as [|? ? NIN LNRB']; subst.
  unfold put_front.
  rewrite ! remove_app.
  rewrite Permutation_middle.
  rewrite remove_not_in.
  simpl. destr.
  rewrite remove_not_in. reflexivity. auto. intro IN.
  red in LDSIJ. specialize (LDSIJ _ _ IN (or_introl eq_refl)). congruence.
  apply in_split. auto.
Qed.

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.
Proof.
  intros.
  symmetry. apply Zmod_small.
  split.
  generalize (two_power_nat_pos x); lia.
  rewrite ! two_power_nat_two_p.
  apply two_p_monotone_strict.
  ppsimpl; lia.
Qed.


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.
Proof.
  intros.
  rewrite Int.add_assoc. rewrite (Int.add_commut _ o).
  rewrite <- Int.add_assoc.
  generalize dependent (Int.add i o).
  intro.
  rewrite <- ! int_add_rew in *.
  rewrite ! Int.unsigned_repr_eq in *.
  replace ((two_power_nat MA) mod Int.modulus) with (two_power_nat MA).
  elim_div. unfold comp_size. unfsize.
  generalize (two_power_nat_pos MA).
  intros.
  lia.
  apply two_power_nat_inf_mod. generalize (MA_bound); unfsize. change (Int.wordsize) with 32%nat. lia.
Qed.

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.
Proof.
  intro.
  rewrite <- ! int_add_rew in *.
  rewrite ! Int.unsigned_repr_eq in *.
  elim_div. unfold comp_size. unfsize.
  Opaque two_power_nat.
  generalize (two_power_nat_pos MA).
  generalize (two_power_nat MA). intro.
  intros.
  assert (z1 = 0 \/ z1 = 1) by lia.
  assert (z = 0 \/ z = 1) by lia. lia.
Qed.

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'.
Proof.
  intros.
  exists (other_cm cm b); repSplit; auto.
  - unfold other_cm; rewrite peq_true; auto.
    rewrite <- Int.add_zero at 1.
    intro ADD.
    apply int_add_eq_l in ADD. apply f_equal with (f:=Int.unsigned) in ADD.
    rewrite Int.unsigned_zero in ADD. rewrite Int.unsigned_repr in ADD.
    generalize (two_power_nat_pos MA); lia.
    generalize (two_power_nat_pos MA); split. lia.
    unfold Int.max_unsigned.
    unfold Int.modulus.
    rewrite ! two_power_nat_two_p.
    generalize (two_p_monotone_strict (Z.of_nat MA) (Z.of_nat Int.wordsize)).
    intro A. trim A. clear A. split. lia.
    generalize (MA_bound). change (Int.wordsize) with (32%nat). lia.
    lia.
  - unfold other_cm; intros; rewrite peq_false; auto.
  -
    destruct COMP; constructor; simpl; intros.
    + apply addr_space in H. unfsize.
      unfold other_cm. destr_cond_match; subst.
      apply add_bounded_plus8. auto.
      generalize (size31_inf); unfsize. lia.
    + specialize (overlap _ _ _ _ H H0 H1).
      generalize (addr_space _ _ H0).
      generalize (addr_space _ _ H1). intros A2 A1.
      unfold other_cm.
      repeat destr_cond_match; subst; try congruence.
      * specialize (LAST _ _ _ n H0 H1).
        intro EQ.
        rewrite <- EQ in LAST.
        revert LAST.
        rewrite Int.add_assoc. rewrite (Int.add_commut _ o).
        rewrite <- Int.add_assoc.
        apply i_bounded_plus8. auto.
      * specialize (LAST _ _ _ n H1 H0).
        intro EQ.
        rewrite EQ in LAST.
        revert LAST.
        rewrite Int.add_assoc. rewrite (Int.add_commut _ o').
        rewrite <- Int.add_assoc. clear EQ overlap.
        apply i_bounded_plus8. auto.
    + generalize (alignment b0).
      unfold other_cm; destr. subst.
      unfold nat_mask. intros.
      eapply alignment_inj with (i1:=mask m b0).
      apply H.
      apply two_p_abs. lia.
      Opaque two_power_nat.
      revert H; unfold nat_mask, mask.
      destr. intros.
      * apply alignment_ok in Heqo.
        destruct Heqo as [C D].
        apply Int.same_bits_eq.
        intros.
        rewrite Int.bits_and; auto.
        rewrite Int.bits_not; auto.
        replace (Int.testbit (Int.repr (two_power_nat MA)) i)
        with (if zeq i (Z.of_nat MA) then true else false).
        rewrite Int.testbit_repr; auto.
        rewrite two_power_nat_two_p.
        rewrite Int.Ztestbit_two_p_m1; auto; try lia.
        destr. destr. subst. generalize (MA_bound); lia.
        rewrite Int.testbit_repr; auto.
        rewrite two_power_nat_two_p. rewrite two_p_equiv.
        rewrite Z.pow2_bits_eqb; auto. 2: lia.
        destr_cond_match. subst; auto. rewrite Z.eqb_refl. auto.
        clear Heqs. rewrite <- Z.eqb_neq in n0. rewrite Z.eqb_sym. auto.
      * rewrite two_power_nat_O. change (Int.repr (1-1)) with Int.zero.
        rewrite Int.not_zero. rewrite ! Int.and_mone. auto.
Qed.

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).
Proof.
  induction l; simpl; intros; eauto.
  destr.
Qed.

Lemma in_bound_plt:
  forall b m o,
    in_bound o (bounds_of_block m b) ->
    Plt b (nextblock m).
Proof.
  intros.
  destruct (plt b (nextblock m)); auto.
  apply msk_valid in n.
  apply bounds_mask_consistency in n.
  unfold bounds_of_block in H; rewrite n in H. red in H; destr; lia.
Qed.

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.
Proof.
  induction l; simpl; intros; auto.
  revert H; destr.
Qed.

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.
Proof.
  intros.
  apply remove_in_before in IN.
  auto.
Qed.


Lemma bounds_lo_0:
  forall m b,
    fst (bounds_of_block m b) = 0.
Proof.
  intros; unfold bounds_of_block; destr. des p.
  eapply bounds_lo_inf0 in Heqo. destr.
Qed.

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).
Proof.
  intros.
  eapply in_bound_zero; eauto.
  apply bounds_lo_0.
Qed.

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.
Proof.
  intros.
  eapply compat_add_unsigned; eauto.
  apply bounds_lo_0.
Qed.

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.
Proof.
  induction l; simpl; intros.
  inv AMA. lia.
  destruct a. simpl in *.
  inv lnr.
  destruct (peq b b'). subst. lia.
  des (make_box_allocation l).
  specialize (IHl _ _ eq_refl H2). inv AMA.
  destr.
  - subst. destr.
    inv AB. des l1.
  - destr. subst.
    eapply make_box_allocation_le; eauto.
    apply IHl.
    inv AB. des l1. inv H. econstructor. eauto. destr.
Qed.


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.
Proof.
  induction l; simpl; intros.
  - apply app_cons_not_nil in H. easy.
  - des fa. inv H. exists nil, a, l. simpl. auto.
    inv H. apply IHl in H2. dex; destr_and. subst.
    exists (a::a0), b, c. auto.
Qed.

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)).
Proof.
  simpl.
  intros.
  exploit in_split; eauto. intro; dex; destr_and.
  apply map_app_cons in H1. dex. destr_and. subst.
  eapply (ab_intro _ _ _ nil); simpl; auto. f_equal.
  rewrite remove_app. simpl. destr. subst; destr.
  rewrite map_app. simpl. eauto.
Qed.

Opaque put_front.

Lemma box_span_pos:
  forall z, z > 0 -> (0 < box_span z)%nat.
Proof.
  intros. rewrite Nat2Z.inj_lt.
  rewrite (Z.mul_lt_mono_pos_l _ _ _ (Z.gt_lt _ _ tpMA_pos)).
  simpl. rewrite box_span_align by lia.
  eapply Z.lt_le_trans. rewrite Z.mul_0_r. apply Z.gt_lt. eauto.
  apply align_le. generalize tpMA_pos; lia.
Qed.


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'.
Proof.
  intros.
  destruct (plt b (nextblock m)).
  - destruct (alloc_compat m (put_front (mk_block_list m) b (size_block m b))) as [al [CONSTR A]].
    eapply is_block_list_permut. apply put_front_permut. eapply mbla_below_in'. apply Pos2Nat.inj_lt in p. lia.
    apply mbla_norepet'. apply is_block_list_mk_block_list.

    exists (box_alloc_to_cm al).
    destruct (compat_shift m (box_alloc_to_cm al) b) as (cm' & DIFF & SAME & COMPAT); auto.
    + intros.

      assert (IBL: is_block_list (mem_blocksize m) (pred (Pos.to_nat (nextblock m))) (put_front (mk_block_list m) b (size_block m b))).
      {
        eapply is_block_list_permut. apply put_front_permut. eapply mbla_below_in'.
        apply Pos2Nat.inj_lt in p. apply NPeano.Nat.lt_le_pred. eauto.
        apply mbla_norepet'. apply is_block_list_mk_block_list.
      }


      exploit in_bound_in_mk. apply H0. eauto. intros (IN & RNG & SZ).
      exploit in_bound_in_mk. apply H1. eauto. intros (IN' & RNG' & SZ').

      unfold mk_cm in CONSTR.
      repeat destr_in CONSTR.
      generalize Heqp0; intro MBA.
      eapply make_box_allocation_order in Heqp0.
      2: eapply permutation_norepet. 2: apply Permutation_map, put_front_permut.
      2: eapply mbla_below_in'. 2: apply Pos2Nat.inj_lt in p. 2: lia.
      2: apply mbla_norepet'. 2: apply mbla_norepet.

      2: apply put_front_appears_before. 3: apply H.
      2: apply mbla_below_in.
      2: apply NPeano.Nat.lt_le_pred. 2: apply Pos2Nat.inj_lt. 2: eapply in_bound_plt. 2: apply H1.

      inv CONSTR.

      exploit make_box_allocation_disjoint. 2: eexact MBA.
      eapply permutation_norepet. apply Permutation_map, put_front_permut.
      eapply mbla_below_in'. apply Pos2Nat.inj_lt in p. lia.
      apply mbla_norepet'. apply mbla_norepet.
      apply IN. apply IN'. auto. auto. auto. intro DISJ. des DISJ.
      eapply box_span_pos in SZ; lia.
      unfold box_alloc_to_cm. rewrite ! Int.add_unsigned.
      rewrite Int.unsigned_repr. 2: eapply box_alloc_in_range'. 4: eauto.
      Focus 2.
      rewrite Nat2Z.inj_add in l. apply Nat2Z.inj_lt. rewrite Z2Nat.id. lia. lia.
      2: eauto. 2: eauto.
      rewrite (Int.unsigned_repr (Int.unsigned _ + _)). 2: eapply box_alloc_in_range'. 4: eauto.
      Focus 2.
      rewrite Nat2Z.inj_add in l. apply Nat2Z.inj_lt. rewrite Z2Nat.id. lia. lia.
      2: eauto. 2: eauto.
      rewrite Int.unsigned_repr. 2: eapply box_alloc_unsigned_range. 4: eauto.
      Focus 2.
      rewrite Nat2Z.inj_add in l. apply Nat2Z.inj_lt. rewrite Z2Nat.id. lia. lia.
      2: eauto. 2: eauto.
      rewrite Int.unsigned_repr. 2: eapply box_alloc_unsigned_range. 4: eauto.
      Focus 2.
      rewrite Nat2Z.inj_add in l. apply Nat2Z.inj_lt. rewrite Z2Nat.id. lia. lia.
      2: eauto. 2: eauto.
      cut (two_power_nat MA * (Z.of_nat (al b')) + Int.unsigned o' < two_power_nat MA * (Z.of_nat (al b)) + Int.unsigned o).
      lia.
      eapply Z.lt_le_trans. apply Z.add_lt_mono_l. apply RNG'.
      transitivity (two_power_nat MA * Z.of_nat (al b)).
      apply inj_le in l0. apply Z.mul_le_mono_nonneg_l with (p := two_power_nat MA) in l0. lia. generalize tpMA_pos; lia.
      generalize (Int.unsigned_range o); lia.

    + eexists; repSplit; eauto.
      apply compat31_32; auto.
  -
    destruct (alloc_compat m (mk_block_list m)) as [al [CONSTR A]].
    apply is_block_list_mk_block_list.
    exists (box_alloc_to_cm al).
    generalize (compat_shift m (box_alloc_to_cm al) b); intro B.
    trim B. intros.
    apply in_bound_plt in H0; congruence.
    trim B; auto.
    dex; destr_and. eexists; repSplit; eauto.
    apply compat31_32; auto.
Qed.

Lemma norm_val:
  forall m v,
    mem_norm m (Eval v) = v.
Proof.
  intros. eapply normalise_val; eauto.
  intros. generalize (exists_two_cms m b1). eauto.
Qed.

Lemma norm_vundef:
  forall m,
    mem_norm m (Eval Vundef) = Vundef.
Proof.
  intros; apply norm_val.
Qed.

Lemma same_Eval_norm:
  forall m vn v,
    same_eval vn (Eval v) ->
    Mem.mem_norm m vn = v.
Proof.
  intros m vn v SE.
  erewrite Mem.same_eval_eqm; eauto.
  apply norm_val.
Qed.

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'.
Proof.
  intros m b o b' o' MN.
  rewrite (norm_val) in MN; auto.
Qed.

Lemma norm_type:
  forall m e v t,
    Mem.mem_norm m e = v ->
    v <> Vundef ->
    wt_val v t ->
    wt_expr e t.
Proof.
  intros m e v t MN NU WT. subst.
  assert (N:= norm_ld m e _ eq_refl).
  destruct (Mem.concrete_mem m).
  specialize (N _ Normalise.dummy_em H).
  inv N; auto.
  generalize (expr_nu_type x dummy_em e t _ (eq_sym H2)).
  des (mem_norm m e).
  des (mem_norm m e).
Qed.

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).
Proof.
  clear.
  intros m vn b SE.
  erewrite same_Eval_norm; eauto.
  rewrite SE. des b; red; simpl; auto.
Qed.

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)).
Proof.
  intros m v i N.
  apply eq_norm.
  constructor.
  - red; intros. eapply norm_ld in Pcm;[|eauto].
    unfold Val.boolval. simpl.
    inv Pcm.
    rewrite <- H1. simpl.
    destruct negb; destr; auto.
  - destruct negb; destr; intro A; inv A.
Qed.

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).
Proof.
  intros m b i N.
  apply eq_norm.
  constructor.
  - red; intros. eapply norm_ld in Pcm;[|eauto].
    simpl.
    inv Pcm.
    rewrite <- H1. simpl. unfold Int.notbool.
    destr; auto.
  - congruence.
Qed.

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.
Proof.
  intros. subst.
  rewrite (proof_irr a1 a2).
  rewrite (proof_irr b1 b2).
  rewrite (proof_irr Pabo1 Pabo2).
  rewrite (proof_irr vm1 vm2).
  rewrite (proof_irr vbt1 vbt2).
  rewrite (proof_irr comp1 comp2).
  rewrite (proof_irr bb1 bb2).
  rewrite (proof_irr bli1 bli2).
  rewrite (proof_irr const1 const2).
  reflexivity.
Qed.

Validity of blocks and accesses


A block address is valid if it was previously allocated. It remains valid even after being freed.

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}.
Proof.
  unfold valid_block; apply plt.
Defined.

Theorem valid_not_valid_diff:
  forall m b b', valid_block m b -> ~(valid_block m b') -> b <> b'.
Proof.
  intros; red; intros. subst b'. contradiction.
Qed.

Hint Local Resolve valid_not_valid_diff: mem.

Permissions

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.
Proof.
  unfold perm, perm_order'; intros.
  destruct (m.(mem_access)#b ofs k); auto.
  eapply perm_order_trans; eauto.
Qed.

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.
Proof.
  assert (forall po1 po2 p,
          perm_order' po2 p -> perm_order'' po1 po2 -> perm_order' po1 p).
  unfold perm_order', perm_order''. intros.
  destruct po2; try contradiction.
  destruct po1; try contradiction.
  eapply perm_order_trans; eauto.
  unfold perm; intros.
  generalize (access_max m b ofs). eauto.
Qed.

Theorem perm_cur:
  forall m b ofs k p, perm m b ofs Cur p -> perm m b ofs k p.
Proof.
  intros. destruct k; auto. apply perm_cur_max. auto.
Qed.

Theorem perm_max:
  forall m b ofs k p, perm m b ofs k p -> perm m b ofs Max p.
Proof.
  intros. destruct k; auto. apply perm_cur_max. auto.
Qed.

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.
Proof.
  unfold perm; intros.
  destruct (plt b m.(nextblock)).
  auto.
  assert (m.(mem_access)#b ofs k = None).
  eapply nextblock_noaccess; eauto.
  rewrite H0 in H.
  contradiction.
Qed.

Hint Local Resolve perm_valid_block: mem.

Remark perm_order_dec:
  forall p1 p2, {perm_order p1 p2} + {~perm_order p1 p2}.
Proof.
  intros. destruct p1; destruct p2; (left; constructor) || (right; intro PO; inversion PO).
Defined.

Remark perm_order'_dec:
  forall op p, {perm_order' op p} + {~perm_order' op p}.
Proof.
  intros. destruct op; unfold perm_order'.
  apply perm_order_dec.
  right; tauto.
Defined.

Theorem perm_dec:
  forall m b ofs k p, {perm m b ofs k p} + {~ perm m b ofs k p}.
Proof.
  unfold perm; intros.
  apply perm_order'_dec.
Defined.



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.
Proof.
  unfold range_perm; intros; eauto with mem.
Qed.

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.
Proof.
  unfold range_perm; intros; eauto with mem.
Qed.

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.
Proof.
  unfold range_perm; intros; eauto with mem.
Qed.






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}.
Proof.
  intros.
  induction lo using (well_founded_induction_type (Zwf_up_well_founded hi)).
  destruct (zlt lo hi).
  destruct (perm_dec m b lo k p).
  destruct (H (lo + 1)). red. omega.
  left; red; intros. destruct (zeq lo ofs). congruence. apply r. omega.
  right; red; intros. elim n. red; intros; apply H0; omega.
  right; red; intros. elim n. apply H0. omega.
  left; red; intros. omegaContradiction.
Defined.

valid_access m chunk b ofs p holds if a memory access of the given chunk is possible in m at address b, ofs with current permissions p. This means:

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.
Proof.
  intros. inv H. constructor; eauto with mem.
Qed.

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.
Proof.
  intros.
  eapply valid_access_implies; eauto. constructor.
Qed.

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.
Proof.
  intros. destruct H.
  assert (perm m b ofs Cur Nonempty).
    apply H. generalize (size_chunk_pos chunk). omega.
  eauto with mem.
Qed.

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.
Proof.
  intros. destruct H. apply perm_cur. apply H. generalize (size_chunk_pos chunk). omega.
Qed.

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.
Proof.
  intros. inv H1. rewrite H in H2. constructor; auto.
  eapply Zdivide_trans; eauto. eapply align_le_divides; eauto.
Qed.

Lemma valid_access_dec:
  forall m chunk b ofs p,
  {valid_access m chunk b ofs p} + {~ valid_access m chunk b ofs p}.
Proof.
  intros.
  destruct (range_perm_dec m b ofs (ofs + size_chunk chunk) Cur p).
  destruct (Zdivide_dec (align_chunk chunk) ofs (align_chunk_pos chunk)).
  left; constructor; auto.
  right; red; intro V; inv V; contradiction.
  right; red; intro V; inv V; contradiction.
Defined.

valid_pointer m b ofs returns true if the address b, ofs is nonempty in m and false if it is empty.
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.
Proof.
  intros. unfold valid_pointer.
  destruct (perm_dec m b ofs Cur Nonempty); simpl;
  intuition congruence.
Qed.

Theorem valid_pointer_valid_access:
  forall m b ofs,
  valid_pointer m b ofs = true <-> valid_access m Mint8unsigned b ofs Nonempty.
Proof.
  intros. rewrite valid_pointer_nonempty_perm.
  split; intros.
  split. simpl; red; intros. replace ofs0 with ofs by omega. auto.
  simpl. apply Zone_divide.
  destruct H. apply H. simpl. omega.
Qed.

C allows pointers one past the last element of an array. These are not valid according to the previously defined valid_pointer. The property weak_valid_pointer m b ofs holds if address b, ofs is a valid pointer in m, or a pointer one past a valid block in m.

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.
Proof.
  intros. unfold weak_valid_pointer. now rewrite orb_true_iff.
Qed.
Lemma valid_pointer_implies:
  forall m b ofs,
  valid_pointer m b ofs = true -> weak_valid_pointer m b ofs = true.
Proof.
  intros. apply weak_valid_pointer_spec. auto.
Qed.

Operations over memory stores


The initial store

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 _ _ _ _ _ _ _ _ _.
Next Obligation.
  repeat rewrite PMap.gi. red; auto.
Qed.
Next Obligation.
  rewrite PMap.gi. auto.
Qed.
Next Obligation.
  repeat rewrite PMap.gi in H.
  congruence.
Qed.
Next Obligation.
  rewrite PMap.gi. auto.
Qed.
Next Obligation.
  rewrite PMap.gi. auto.
Qed.
Next Obligation.
  unfold nb_boxes_max. simpl.
  eapply (Z.lt_le_trans _ (two_power_nat 20 - 2) _). reflexivity.
  cut (two_power_nat 20 <= two_power_nat (32 - MA)). lia.
  rewrite ! two_power_nat_two_p.
  apply two_p_monotone. generalize MA_bound. lia.
Qed.
Next Obligation.
  rewrite PMap.gi in H. congruence.
Qed.
Next Obligation.
  rewrite PMap.gi.
  reflexivity.
Qed.
Next Obligation.
  rewrite PMap.gi in H. congruence.
Qed.

Reading N adjacent bytes in a block content.

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).
Proof.
  induction n; simpl; intros; constructor; auto.
Qed.

Lemma getN_Nlist : forall n p c, length (getN n p c) = n.
Proof.
    induction n.
    intros; reflexivity.
    intros.
    simpl.
    rewrite IHn.
    reflexivity.
  Qed.

  


Writing N adjacent bytes in a block content.

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.
Proof.
  induction vl; intros; simpl.
  auto.
  simpl length in H. rewrite inj_S in H.
  transitivity (ZMap.get q (ZMap.set p a c)).
  apply IHvl. intros. apply H. omega.
  apply ZMap.gso. apply not_eq_sym. apply H. omega.
Qed.

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.
Proof.
  intros. apply setN_other.
  intros. omega.
Qed.

Remark getN_setN_same:
  forall vl p c,
  getN (length vl) p (setN vl p c) = vl.
Proof.
  induction vl; intros; simpl.
  auto.
  decEq.
  rewrite setN_outside. apply ZMap.gss. omega.
  apply IHvl.
Qed.

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.
Proof.
  induction n; intros. auto. rewrite inj_S in H. simpl. decEq.
  apply H. omega. apply IHn. intros. apply H. omega.
Qed.

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.
Proof.
  intros. apply getN_exten. intros. apply setN_other.
  intros; red; intros; subst r. eelim H; eauto.
Qed.

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.
Proof.
  intros. apply getN_setN_disjoint. apply Intv.disjoint_range. auto.
Qed.

Remark setN_default:
  forall vl q c, fst (setN vl q c) = fst c.
Proof.
  induction vl; simpl; intros. auto. rewrite IHvl. auto.
Qed.



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)).
Proof.
  induction vl; simpl; intros.
  - omega.
  - des (zlt lo ofs).
    rewrite IHvl by (zify; omega).
    replace (Z.to_nat (ofs - lo)) with (S (Z.to_nat (ofs - (lo + 1)))).
    simpl. auto.
    zify. repeat rewrite Z2Nat.id by omega. omega.
    replace lo with ofs by omega.
    rewrite setN_outside by omega.
    rewrite ZMap.gss.
    replace (ofs - ofs) with 0 by omega. simpl.
    reflexivity.
Qed.


Lemma same_type_memval_refl:
  forall m,
    same_type_memval m m.
Proof.
  des m.
Qed.

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)).
Proof.
  intros mr WF v v' o ofs t b0 SE.
  assert (range: forall a b c, a <= b < c \/ (a > b \/ c <= b)) by (intros; omega).
  destruct (range o ofs (o + Z.of_nat (length v))).
  + generalize (Mem.get_setN_inside _ _ _ t # b0 H).
    assert (o <= ofs < o + Z.of_nat (length v')).
    { rewrite <- (list_forall2_length SE); eauto. }
    generalize (Mem.get_setN_inside _ _ _ t # b0 H0).
    intros.
    eapply nth_error_property; eauto.
  + rewrite ! Mem.setN_outside. unfold memval_rel; inv WF; eauto.
    split; eauto.
    left; apply same_type_memval_refl.
    rewrite <- (list_forall2_length SE); eauto. omega.
    omega.
Qed.


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).
Proof.
  intros mr v v' ofs o t t' b b0 ME SE.
  rewrite ! PMap.gsspec.
  destruct (peq b0 b); subst; try tauto; auto.
  assert (range: forall a b c, a <= b < c \/ (a > b \/ c <= b)) by (intros; omega).
  destruct (range o ofs (o + Z.of_nat (length v))).
  + generalize (Mem.get_setN_inside _ _ _ t !! b H).
    assert (o <= ofs < o + Z.of_nat (length v')).
    { rewrite <- (list_forall2_length SE); eauto. }
    generalize (Mem.get_setN_inside _ _ _ t' !! b H0).
    intros.
    eapply nth_error_property; eauto.
  + rewrite ! Mem.setN_outside. apply ME. auto.
    rewrite <- (list_forall2_length SE); eauto. omega.
    omega.
Qed.

We initialise the memory of allocated blocks with the appropriate Eundef values.

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.
Proof.
  induction p; unfold ZIndexed.index; simpl.
  exists (Z.neg p); auto.
  exists (Z.pos p); auto.
  exists 0; auto.
Qed.

Lemma zle_zlt:
  forall a b c,
    zle a b && zlt b c = true <->
    a <= b < c.
Proof.
  unfold zle, zlt.
  intros.
  destruct (Z_le_gt_dec a b).
  destruct (Z_lt_dec b c).
  intuition omega.
  split; try discriminate; try omega.
  split; try discriminate; try omega.
Qed.








Lemma maxspec:
  forall (n m: nat),
    max n m = if lt_dec n m then m else n.
Proof.
  intros.
  generalize (Max.max_spec n m).
  repeat destr. lia.
Qed.

Lemma minspec:
  forall (n m: nat),
    min n m = if lt_dec n m then n else m.
Proof.
  intros.
  generalize (Min.min_spec n m).
  repeat destr. lia.
Qed.

Lemma alignment_of_size_bnd sz:
  (alignment_of_size sz <= 3)%nat.
Proof.
  unfold alignment_of_size; repeat destr; lia.
Qed.

Opaque min max.
The allocation is now guarded by the success of conc_mem_alloc.
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.
Next Obligation.
  repeat rewrite PMap.gsspec. destruct (peq b (nextblock m)).
  subst b. destruct (zle 0 ofs && zlt ofs hi); red; auto with mem.
  apply access_max.
Qed.
Next Obligation.
  rewrite PMap.gsspec. destruct (peq b (nextblock m)).
  subst b. elim H0. apply Plt_succ.
  apply nextblock_noaccess. red; intros; elim H0.
  apply Plt_trans_succ; auto.
Qed.
Next Obligation.
  unfold get_bounds.
  repeat rewrite PMap.gsspec in *.
  destruct (peq b (nextblock m)); subst.
  unfold in_bound; simpl.
  destruct (zle 0 ofs && zlt ofs hi) eqn:?; try congruence.
  apply zle_zlt in Heqb. rewrite Zmax_spec. destr. lia.
  eapply access_bounds_ok; eauto.
Qed.
Next Obligation.
  rewrite PMap.gsspec.
  destr. subst. xomega.
  apply msk_valid; auto. xomega.
Qed.
Next Obligation.
  rewrite PMap.gsspec.
  destr. subst. xomega.
  apply blocktype_valid; auto. xomega.
Qed.
Next Obligation.
  erewrite mk_block_list_aux_eq. 2: apply MA_bound.
  unfold nb_boxes_used_m, nb_boxes_used in *; simpl in *.
  rewrite fold_left_plus_rew.
  eapply Z.le_lt_trans. 2: eauto.
  rewrite Z.sub_0_r. unfold mk_block_list.
  rewrite <- ! plus_assoc. rewrite (plus_comm (nb_extra _)).
  apply Z.le_refl.
Qed.
Next Obligation.
  unfold get_size.
  rewrite PMap.gsspec in *.
  des (peq b (nextblock m)); split.
  - inv H0. apply Min.le_min_l.
  - inv H0. clear H.
    rewrite Zmax_spec.
    rewrite ! Z.sub_0_r.
    destr. unfold alignment_of_size.
    des (zlt 0 2); lia.
    generalize MA_bound (alignment_of_size_bnd hi).
    rewrite minspec, maxspec.
    repeat destr; try destr_in l; try lia.
  - revert H0; apply alignment_ok.
  - revert H0; apply alignment_ok.
Qed.
Next Obligation.
  rewrite ! PMap.gsspec in *.
  des (peq b (nextblock m)).
  eapply bounds_mask_consistency; eauto.
Qed.
Next Obligation.
  rewrite ! PMap.gsspec in *.
  destruct (peq b (nextblock m)). inv H0; split; auto.
  apply Z.le_ge. apply Z.le_max_l.
  apply bounds_lo_inf0 in H0; auto.
Qed.

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)).
Proof.
  intros m lo hi m' b bt ALLOC.
  Transparent Mem.alloc Mem.low_alloc.
  unfold Mem.alloc, Mem.low_alloc in ALLOC.
  destr_in ALLOC.
  inv ALLOC.
  unfold Mem.nat_mask, Mem.mask. simpl.
  rewrite PMap.gss. rewrite Z.sub_0_r in *; auto.
  rewrite Max.max_idempotent. rewrite Min.min_r. auto.
  generalize MA_bound (alignment_of_size_bnd hi); lia.
Qed.

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'.
Proof.
  intros m lo hi m' b bt ALLOC b' DIFF.
  unfold Mem.alloc, Mem.low_alloc in ALLOC.
  destr_in ALLOC.
  inv ALLOC. simpl.
  rewrite PMap.gso; auto.
Qed.

Require Import Tactics.

Lemma box_span_le:
  forall x y, 0 <= x <= y ->
         (box_span x <= box_span y)%nat.
Proof.
  intros.
  apply Nat2Z.inj_le.
  apply (Z.mul_le_mono_pos_l _ _ _ (Zgt_lt _ _ (two_power_nat_pos MA))).
  rewrite ! box_span_align by lia.
  apply align_add; try lia. apply tpMA_pos.
Qed.

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.
Proof.
  unfold nb_boxes_used. induction 1; simpl; intros; eauto.
  repeat destr.
  rewrite ! (fold_left_plus_rew _ (box_span _)).
  apply box_span_le in H. lia.
Qed.

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).
Proof.
  induction n; simpl; intros.
  constructor.
  rewrite ! mbla_rew. constructor; auto.
  simpl. auto.
Qed.


Freeing a block between the given bounds.
We only free the block when lo and hi corresponds to the exact bounds of b.
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) _ _ _ _ _ _ _ _ _ .
Next Obligation.
  repeat rewrite PMap.gsspec. destruct (peq b0 b).
  destruct (zle lo ofs && zlt ofs hi). red; auto. apply access_max.
  apply access_max.
Qed.
Next Obligation.
  repeat rewrite PMap.gsspec. destruct (peq b0 b). subst.
  destruct (zle lo ofs && zlt ofs hi). auto. apply nextblock_noaccess; auto.
  apply nextblock_noaccess; auto.
Qed.
Next Obligation.
  unfold get_bounds in *.
  repeat rewrite PMap.gsspec in *. repeat destr_in H.
  - generalize H; intro H1.
    apply access_bounds_ok in H; auto.
    destr; repeat destr_in Heqo; inv Heqo. unfold get_bounds in H; rewrite Heqo0 in H. auto.
    unfold get_bounds in H; rewrite Heqo0 in H.
    unfold in_bound in *. simpl in *.
    des (zeq z lo); des (zeq z0 hi).
    des (zle lo ofs); des (zlt ofs hi).
    unfold get_bounds in H; rewrite Heqo0 in H. auto.
  - eapply access_bounds_ok; eauto.
Qed.
Next Obligation.
  rewrite msk_valid; auto.
Qed.
Next Obligation.
  rewrite blocktype_valid; auto.
Qed.
Next Obligation.
  eapply Z.le_lt_trans. 2: apply wfm_alloc_ok.
  rewrite ! Nat2Z.inj_add.
  apply Z.add_le_mono_r.
  apply inj_le.
  apply nb_boxes_used_le.
  apply mbla_le. unfold get_size. simpl; intros.
  rewrite PMap.gsspec.
  destr.
  - subst. repeat destr.
    destr_in Heqo. inv Heqo. eapply bounds_lo_inf0 in Heqo0. lia.
    eapply bounds_lo_inf0 in Heqo0. lia. lia.
  - destr. destr. eapply bounds_lo_inf0 in Heqo. lia. lia.
Qed.
Next Obligation.
  unfold get_size. rewrite PMap.gsspec.
  destruct (peq b0 b); subst; auto;
  try eapply alignment_ok; eauto.
  apply alignment_ok in H; eauto.
  destruct H; split; auto.
  unfold get_size in H0.
  destruct (mem_blocksize m) #b eqn:?; try omega.
  destruct p.
  destruct (zeq z lo && zeq z0 hi). change (alignment_of_size 0) with O. omega.
  auto.
Qed.
Next Obligation.
  revert H.
  rewrite PMap.gsspec.
  des (peq b0 b); intros.
  - eapply bounds_mask_consistency in H; eauto.
    rewrite H. auto.
  - eapply bounds_mask_consistency; eauto.
Qed.
Next Obligation.
  revert H.
  rewrite PMap.gsspec.
  destruct (peq b0 b).
  - destruct (mem_blocksize m) # b eqn:?; try easy.
    destruct p. destr_cond_match; intro A; inv A.
    apply bounds_lo_inf0 in Heqo; eauto.
  - apply bounds_lo_inf0; auto.
Qed.

Lemma unchecked_free_mask:
  forall m b lo hi b',
    mask (unchecked_free m b lo hi) b' =
    mask m b'.
Proof.
  intros.
  Opaque zeq.
  unfold unchecked_free, mask, eq_block; simpl.
  reflexivity.
Qed.

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

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'.
Proof.
  intros b lo hi m m1 m' m1' SB FL FL'.
  unfold Mem.free, Mem.unchecked_free in *.
  repeat destr_in FL. repeat destr_in FL'. inv FL; inv FL'; simpl.
  rewrite SB. reflexivity.
Qed.

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).
Proof.
  intros b lo hi m m1 SB.
  unfold Mem.unchecked_free in *.
  intros. simpl.
  rewrite SB. reflexivity.
Qed.


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.
Proof.
  Transparent Mem.free.
  unfold Mem.free.
  simpl.
  intros.
  repeat destr_in H; inv H; simpl; auto.
Qed.


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.
Proof.
  intros.
  destruct (valid_block_dec m b); auto.
  unfold bounds_of_block in H.
  rewrite bs_valid in H; auto. inv H; congruence.
Qed.


Lemma size_mem_aux_sup1:
  forall m,
    Alloc.size_mem_aux MA m >= two_power_nat MA.
Proof.
  unfold Alloc.size_mem_aux.
  intros.
  apply Zle_ge.
  apply Alloc.size_mem_al_pos. apply two_power_nat_pos. generalize (two_power_nat_pos MA); omega.
Qed.


Memory reads.

load chunk m b ofs perform a read in memory state m, at address b and offset ofs. It returns the value of the memory chunk at that address. None is returned if the accessed bytes are not readable.

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.

loadv chunk m addr is similar, but the address and offset are given as a single value addr, which must be a pointer value. We normalise the address beforehand.

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.

loadbytes m b ofs n reads n consecutive bytes starting at location (b, ofs). Returns None if the accessed locations are not readable.

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.



Memory stores.

store chunk m b ofs v perform a write in memory state m. Value v is stored at address b and offset ofs. Return the updated memory store, or None if the accessed bytes are not writable.

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.
Next Obligation.
apply access_max. Qed.
Next Obligation.
apply nextblock_noaccess; auto. Qed.
Next Obligation.
  apply access_bounds_ok in H0; auto.
Qed.
Next Obligation.
  destruct m. simpl. auto.
Qed.
Next Obligation.
  destruct m. simpl. auto.
Qed.
Next Obligation.
  destruct m. simpl. auto.
Qed.
Next Obligation.
  destruct m. simpl. auto.
Qed.
Next Obligation.
  destruct m. simpl. eauto.
Qed.
Next Obligation.
  destruct m. simpl. eauto.
Qed.

storev chunk m addr v is similar, but the address and offset are given as a single value addr, which must be a pointer value. We normalise the address beforehand.

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.

storebytes m b ofs bytes stores the given list of bytes bytes starting at location (b, ofs). Returns updated memory state or None if the accessed locations are not writable.

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.
Next Obligation.
apply access_max. Qed.
Next Obligation.
apply nextblock_noaccess; auto. Qed.
Next Obligation.
  apply access_bounds_ok in H0; auto.
Qed.
Next Obligation.
  destruct m. simpl. auto.
Qed.
Next Obligation.
  destruct m. simpl. auto.
Qed.
Next Obligation.
  destruct m. simpl. auto.
Qed.
Next Obligation.
  destruct m. simpl. auto.
Qed.
Next Obligation.
  destruct m. simpl. eauto.
Qed.
Next Obligation.
  destruct m. simpl in *. eauto.
Qed.

drop_perm m b lo hi p sets the max permissions of the byte range (b, lo) ... (b, hi - 1) to p. These bytes must have current permissions Freeable in the initial memory state m. Returns updated memory state, or None if insufficient permissions.

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.
Next Obligation.
  repeat rewrite PMap.gsspec. destruct (peq b0 b). subst b0.
  destruct (zle lo ofs && zlt ofs hi). red; auto with mem. apply access_max.
  apply access_max.
Qed.
Next Obligation.
  specialize (nextblock_noaccess m b0 ofs k H0). intros.
  rewrite PMap.gsspec. destruct (peq b0 b). subst b0.
  destruct (zle lo ofs). destruct (zlt ofs hi).
  assert (perm m b ofs k Freeable). apply perm_cur. apply H; auto.
  unfold perm in H2. rewrite H1 in H2. contradiction.
  auto. auto. auto.
Qed.
Next Obligation.
  repeat rewrite PMap.gsspec in *.
  repeat destr_in H0.
  unfold range_perm in H.
  unfold perm, perm_order' in H.
  apply zle_zlt in Heqb0. apply H in Heqb0. destr_in Heqb0.
  eapply access_bounds_ok. instantiate (1:=Cur); rewrite Heqo; eauto. destr.
  eapply access_bounds_ok in H0; eauto.
  eapply access_bounds_ok in H0; eauto.
Qed.
Next Obligation.
  destruct m. simpl. auto.
Qed.
Next Obligation.
  destruct m. simpl. auto.
Qed.
Next Obligation.
  destruct m. simpl. auto.
Qed.
Next Obligation.
  destruct m. simpl. eauto.
Qed.
Next Obligation.
  destruct m. simpl. eauto.
Qed.
Next Obligation.
  destruct m. simpl in *. eauto.
Qed.

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

Properties of the empty store.

Theorem nextblock_empty: nextblock empty = 1%positive.
Proof.
reflexivity. Qed.

Theorem perm_empty: forall b ofs k p, ~perm empty b ofs k p.
Proof.
  intros. unfold perm, empty; simpl. rewrite PMap.gi. simpl. tauto.
Qed.

Theorem valid_access_empty: forall chunk b ofs p, ~valid_access empty chunk b ofs p.
Proof.
  intros. red; intros. elim (perm_empty b ofs Cur p). apply H.
  generalize (size_chunk_pos chunk); omega.
Qed.

Properties related to load


Lemma Forall_rib:
  forall {A} (P : A -> Prop) l,
    Forall P l ->
    Forall P (rev_if_be l).
Proof.
  unfold rev_if_be; destr_cond_match; intuition try congruence.
  apply Forall_rev.
  rewrite rev_involutive; auto.
Qed.

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.
Proof.
  intros. unfold load.
  rewrite pred_dec_true; eauto.
Qed.

Theorem load_valid_access:
  forall m chunk b ofs v,
  load chunk m b ofs = Some v ->
  valid_access m chunk b ofs Readable.
Proof.
  intros until v. unfold load.
  destruct (valid_access_dec m chunk b ofs Readable); intros.
  auto.
  congruence.
Qed.

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)).
Proof.
  intros until v. unfold load.
  destruct (valid_access_dec m chunk b ofs Readable); intros.
  congruence.
  congruence.
Qed.




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.
Proof.
  intros.
  rewrite Int.add_unsigned. rewrite Int.unsigned_repr. auto.
  exploit Mem.load_valid_access. eexact H. intros [P Q]. simpl in Q.
  exploit (Zdivide_interval (Int.unsigned i) Int.modulus 8).
  omega. apply Int.unsigned_range. auto. exists (two_p (32-3)); reflexivity.
  change (Int.unsigned (Int.repr 4)) with 4. unfold Int.max_unsigned. omega.
Qed.

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).
Proof.
  intros. exploit load_result; eauto; intros.
  subst.
  eapply decode_val_type; eauto.
Qed.

Lemma loadv_type:
  forall m c a v (L: Mem.loadv c m a = Some v), wt v (type_of_chunk c).
Proof.
  unfold Mem.loadv; intros.
  des (Mem.mem_norm m a).
  eapply Mem.load_type; eauto.
Qed.

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.
Proof.
  intros. exploit load_result; eauto.
  set (l := getN (size_chunk_nat chunk) ofs m.(mem_contents)#b).
  intro; subst.
  generalize (decode_val_cast chunk l).
  des chunk; simpl.
  red; intros; seval. rewrite Int.sign_ext_above; auto. unfsize. lia.
Qed.

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.
Proof.
  intros until v2. unfold load.
  change (size_chunk_nat Mint8signed) with (size_chunk_nat Mint8unsigned).
  set (cl := getN (size_chunk_nat Mint8unsigned) ofs m.(mem_contents)#b).
  destruct (valid_access_dec m Mint8signed b ofs Readable); try discriminate.
  rewrite pred_dec_true; auto. unfold decode_val. simpl.
  intros A B; inv A; inv B.
  red; simpl; intros; auto.
  destr.
  seval.
  rewrite Int.sign_ext_zero_ext; auto; omega.
Qed.

Theorem load_int8_signed_unsigned_none:
  forall m b ofs,
    load Mint8signed m b ofs = None ->
    load Mint8unsigned m b ofs = None.
Proof.
  intros m b ofs.
  unfold load.
  destr.
  rewrite pred_dec_false; auto.
Qed.

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.
Proof.
  intros until v2. unfold load.
  change (size_chunk_nat Mint16signed) with (size_chunk_nat Mint16unsigned).
  set (cl := getN (size_chunk_nat Mint16unsigned) ofs m.(mem_contents)#b).
  destruct (valid_access_dec m Mint16signed b ofs Readable).
  - rewrite pred_dec_true; auto. unfold decode_val.
    red; intros A B; inv A; inv B. simpl; intros.
    seval.
    rewrite Int.sign_ext_zero_ext; auto; omega.
  - rewrite pred_dec_false; auto. destr.
Qed.

Theorem load_int16_signed_unsigned_none:
  forall m b ofs,
    load Mint16signed m b ofs = None ->
    load Mint16unsigned m b ofs = None.
Proof.
  intros m b ofs.
  unfold load.
  destr. rewrite pred_dec_false; auto.
Qed.

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.
Proof.
  intros. econstructor. unfold loadbytes. rewrite pred_dec_true; eauto.
Qed.

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.
Proof.
  intros until bytes. unfold loadbytes.
  destruct (range_perm_dec m b ofs (ofs + len) Cur Readable). auto. congruence.
Qed.

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).
Proof.
  unfold loadbytes, load; intros.
  destruct (range_perm_dec m b ofs (ofs + size_chunk chunk) Cur Readable);
  try congruence.
  inv H. rewrite pred_dec_true. auto.
  split; auto.
Qed.

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.
Proof.
  intros. exploit load_valid_access; eauto. intros [A B].
  exploit load_result; eauto. intros.
  exists (getN (size_chunk_nat chunk) ofs m.(mem_contents)#b); split.
  unfold loadbytes. rewrite pred_dec_true; auto.
  auto.
Qed.

Lemma getN_length:
  forall c n p, length (getN n p c) = n.
Proof.
  induction n; simpl; intros. auto. decEq; auto.
Qed.

Theorem loadbytes_length:
  forall m b ofs n bytes,
  loadbytes m b ofs n = Some bytes ->
  length bytes = nat_of_Z n.
Proof.
  unfold loadbytes; intros.
  destruct (range_perm_dec m b ofs (ofs + n) Cur Readable); try congruence.
  inv H. apply getN_length.
Qed.

Theorem loadbytes_empty:
  forall m b ofs n,
  n <= 0 -> loadbytes m b ofs n = Some nil.
Proof.
  intros. unfold loadbytes. rewrite pred_dec_true. rewrite nat_of_Z_neg; auto.
  red; intros. omegaContradiction.
Qed.



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.
Proof.
  induction n1; intros.
  simpl. decEq. omega.
  rewrite inj_S. simpl. decEq.
  replace (p + Zsucc (Z_of_nat n1)) with ((p + 1) + Z_of_nat n1) by omega.
  auto.
Qed.

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).
Proof.
  unfold loadbytes; intros.
  destruct (range_perm_dec m b ofs (ofs + n1) Cur Readable); try congruence.
  destruct (range_perm_dec m b (ofs + n1) (ofs + n1 + n2) Cur Readable); try congruence.
  rewrite pred_dec_true. rewrite nat_of_Z_plus; auto.
  rewrite getN_concat. rewrite nat_of_Z_eq; auto.
  congruence.
  red; intros.
  assert (ofs0 < ofs + n1 \/ ofs0 >= ofs + n1) by omega.
  destruct H4. apply r; omega. apply r0; omega.
Qed.

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.
Proof.
  unfold loadbytes; intros.
  destruct (range_perm_dec m b ofs (ofs + (n1 + n2)) Cur Readable);
  try congruence.
  rewrite nat_of_Z_plus in H; auto. rewrite getN_concat in H.
  rewrite nat_of_Z_eq in H; auto.
  repeat rewrite pred_dec_true.
  econstructor; econstructor.
  split. reflexivity. split. reflexivity. congruence.
  red; intros; apply r; omega.
  red; intros; apply r; omega.
Qed.

Lemma Forall_dec:
  forall {A} (P: A -> Prop)
         (Pdec: forall a, P a \/ ~ P a)
         l,
    Forall P l \/ ~ Forall P l.
Proof.
  induction l; simpl; intros.
  left; constructor.
  destruct (Pdec a); destruct IHl; intuition try congruence.
  left; constructor; auto.
  right; intro C; inv C; congruence.
  right; intro C; inv C; congruence.
  right; intro C; inv C; congruence.
Qed.

Lemma Forall_app_l:
  forall {A} (P: A -> Prop) l1 l2,
    Forall P (l1 ++ l2) ->
    Forall P l1.
Proof.
  induction l1; try constructor.
  change ((a::l1)++ l2) with (a:: (l1 ++ l2)) in H.
  inv H; auto.
  change ((a::l1)++ l2) with (a:: (l1 ++ l2)) in H.
  inv H; auto.
  apply IHl1 with (l2:=l2); auto.
Qed.

Lemma Forall_rev':
  forall {A} (P: A -> Prop) l,
    Forall P l ->
    Forall P (rev l).
Proof.
  intros; apply Forall_rev.
  rewrite rev_involutive; auto.
Qed.

Lemma Forall_app_r:
  forall {A} (P: A -> Prop) l1 l2,
    Forall P (l1 ++ l2) ->
    Forall P l2.
Proof.
  intros.
  apply Forall_rev' in H.
  rewrite rev_app_distr in H.
  apply Forall_app_l in H.
  apply Forall_rev; auto.
Qed.

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).
Proof.
  Opaque decode_val.
  intros.
  exploit load_valid_access; eauto. intros [A B]. simpl in *.
  exploit load_loadbytes. eexact H. simpl. intros [bytes [LB EQ]].
  change 8 with (4 + 4) in LB.
  exploit loadbytes_split. eexact LB. omega. omega.
  intros (bytes1 & bytes2 & LB1 & LB2 & APP).
  change 4 with (size_chunk Mint32) in LB1.
  exploit loadbytes_load. eexact LB1.
  simpl. apply Zdivides_trans with 8; auto. exists 2; auto.
  intros L1.
  change 4 with (size_chunk Mint32) in LB2.
  exploit loadbytes_load. eexact LB2.
  simpl. apply Zdivide_plus_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto.
  intros L2.
  rewrite L1.
  simpl in L2.
  rewrite L2.
  rewrite APP in EQ.
  exists (if Archi.big_endian then decode_val Mint32 bytes1 else decode_val Mint32 bytes2).
  exists (if Archi.big_endian then decode_val Mint32 bytes2 else decode_val Mint32 bytes1).
  split. destruct Archi.big_endian; auto.
  split. destruct Archi.big_endian; auto. subst.
  rewrite decode_val_int64; auto.
  constructor; simpl; intros; auto.
  rewrite (loadbytes_length m b ofs (size_chunk Mint32)); auto.
  rewrite (loadbytes_length m b (ofs+size_chunk Mint32) (size_chunk Mint32)); auto.
Qed.

Lemma perm_bounds:
  forall m b ofs p k,
    Mem.perm m b ofs k p ->
    in_bound_m ofs m b.
Proof.
  unfold Mem.perm, Mem.perm_order'.
  intros.
  destruct ((Mem.mem_access m) !! b ofs k) eqn:?; intuition try congruence.
  generalize (Mem.access_bounds_ok m b ofs k).
  rewrite Heqo.
  intros. unfold in_bound_m, Mem.bounds_of_block, get_bounds.
  destruct ((Mem.mem_blocksize m) !! b) eqn:?; eauto.
  destruct p1.
  unfold get_bounds in H0.
  rewrite Heqo0 in H0.
  apply H0; congruence.
  unfold get_bounds in H0.
  rewrite Heqo0 in H0.
  exfalso; exploit H0; eauto. congruence. unfold in_bound. simpl. omega.
Qed.



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).
Proof.
  intros.
  apply RP in OFS.
  eapply Mem.perm_bounds; eauto.
Qed.

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.
Proof.
  intros.
  generalize (range_perm_bounds _ _ _ _ _ _ RP o1).
  generalize (range_perm_bounds _ _ _ _ _ _ RP (o2-1)).
  intros A B; trim A. lia. trim B. lia.
  destr; unfold in_bound in *; simpl in *; lia.
Qed.


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.
Proof.
  intros.
  revert H; unfold Mem.loadv. des (Mem.mem_norm m a).
  cut (Mem.mem_norm m (Val.add a (Eval (Vint (Int.repr 4)))) =
       Vptr b (Int.add i (Int.repr 4))).
  intro A; rewrite A. intros.
  replace (Int.unsigned (Int.add i (Int.repr 4))) with (Int.unsigned i + 4). intros.
  exploit Mem.load_int64_split; eauto. intros (v1 & v2 & B & C & D).
  exists v1, v2. split; auto. split; auto.
  split; red; intros; simpl; rewrite D; simpl; seval; auto.
  rewrite Int64.hi_ofwords; auto. rewrite Int64.lo_ofwords; auto.
  erewrite load_int64_eq_add; eauto.
  apply eq_norm; try congruence.
  constructor.
  - red; intros.
    exploit norm_ld; eauto. simpl.
    intro A; inv A. rewrite <- H1. simpl.
    sint. auto.
Qed.

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 }.
Proof.
  intros.
  unfold store.
  destruct (valid_access_dec m1 chunk b ofs Writable); [|contradiction].
  eauto.
Defined.

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.
Proof.
  unfold store in STORE.
  destruct ( valid_access_dec m1 chunk b ofs Writable); inv STORE.
  auto.
Qed.

Lemma store_mem_contents:
  mem_contents m2 = PMap.set b (setN (encode_val chunk v) ofs m1.(mem_contents)#b) m1.(mem_contents).
Proof.
  unfold store in STORE. destruct (valid_access_dec m1 chunk b ofs Writable); inv STORE.
  auto.
Qed.

Theorem perm_store_1:
  forall b' ofs' k p, perm m1 b' ofs' k p -> perm m2 b' ofs' k p.
Proof.
  intros.
 unfold perm in *. rewrite store_access; auto.
Qed.

Theorem perm_store_2:
  forall b' ofs' k p, perm m2 b' ofs' k p -> perm m1 b' ofs' k p.
Proof.
  intros. unfold perm in *. rewrite store_access in H; auto.
Qed.

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'.
Proof.
  intros.
  revert STORE.
  unfold store.
  destr_cond_match; try congruence.
  intro A; inv A.
  unfold size_of_block; simpl.
  reflexivity.
Qed.

Theorem mask_store:
  forall b',
    mask m1 b' = mask m2 b'.
Proof.
  intros.
  revert STORE.
  unfold store.
  destr_cond_match; try congruence.
  intro A; inv A; unfold mask; reflexivity.
Qed.

Theorem bounds_of_block_store:
  forall b',
    bounds_of_block m1 b' = bounds_of_block m2 b'.
Proof.
  intros; revert STORE; unfold store; repeat (destr_cond_match; try congruence).
  intro A; inv A; reflexivity.
Qed.

Theorem nat_mask_store:
  forall b',
    nat_mask m1 b' = nat_mask m2 b'.
Proof.
  intros; revert STORE; unfold store; repeat destr_cond_match; try congruence.
  intro A; inv A; reflexivity.
Qed.


Lemma store_compat:
  forall cm q,
    Mem.compat_m m2 q cm ->
    Mem.compat_m m1 q cm.
Proof.
  intros cm q COMP.
  unfold Mem.compat_m in *.
  des q;
    (eapply Normalise.compat_same_bounds;
      [intros; rewrite <- bounds_of_block_store; eauto|
       intros; rewrite <- nat_mask_store; eauto|auto]).
Qed.

Theorem nextblock_store:
  nextblock m2 = nextblock m1.
Proof.
  intros.
  unfold store in STORE. destruct ( valid_access_dec m1 chunk b ofs Writable); inv STORE.
  auto.
Qed.

Theorem store_valid_block_1:
  forall b', valid_block m1 b' -> valid_block m2 b'.
Proof.
  unfold valid_block; intros. rewrite nextblock_store; auto.
Qed.

Theorem store_valid_block_2:
  forall b', valid_block m2 b' -> valid_block m1 b'.
Proof.
  unfold valid_block; intros. rewrite nextblock_store in H; auto.
Qed.

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.
Proof.
  intros. inv H. constructor; try red; auto with mem.
Qed.

Theorem store_valid_access_2:
  forall chunk' b' ofs' p,
  valid_access m2 chunk' b' ofs' p -> valid_access m1 chunk' b' ofs' p.
Proof.
  intros. inv H. constructor; try red; auto with mem.
Qed.

Theorem store_valid_access_3:
  valid_access m1 chunk b ofs Writable.
Proof.
  unfold store in STORE. destruct (valid_access_dec m1 chunk b ofs Writable).
  auto.
  congruence.
Qed.



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'.
Proof.
  intros.
  destruct (valid_access_load m2 chunk' b ofs).
  eapply valid_access_compat. symmetry; eauto. auto. eauto with mem.
  exists x; split; auto.
  exploit load_result; eauto. intros B.
  rewrite store_mem_contents in B; simpl in B.
  rewrite PMap.gss in B.
  replace (size_chunk_nat chunk') with (length (encode_val chunk v)) in B.
  rewrite getN_setN_same in B.
  subst.
  apply decode_encode_val_general; auto.
  rewrite encode_val_length.
  repeat rewrite size_chunk_conv in H.
  apply inj_eq_rev; auto.
Qed.

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).
Proof.
  intros. destruct (load_store_similar chunk') as [v' [A B]]; auto.
  rewrite A in H2; inv H2.
  des chunk; des chunk'; try (rewrite se_eval; simpl; auto).
  unfold get_type in B.
  repeat destr. destr_in B. destr_in Heqs. destr_in Heqs.
  - rewrite B. red; intros; symmetry; destr.
    erewrite (wt_expr_2_is_undef _ Tsingle Tfloat); destr.
  - repeat destr_in B; repeat destr_in Heqs.
    rewrite B. red; intros; symmetry; destr.
    rewrite nwt_expr_undef; auto.
    intro; dex. des t.
Qed.

Theorem load_store_same:
  exists v1, load chunk m2 b ofs = Some v1 /\
             same_eval v1 (Val.load_result chunk v).
Proof.
  intros.
  exploit load_store_similar; eauto. omega.
  intros [v' [A B]]. rewrite A. exists v'; split; auto.
  des chunk.
  destruct (get_type_correct v).
  - des (get_type v); repeat destr.
    + rewrite B.
      red; intros; simpl; erewrite (wt_expr_2_is_undef _ _ _ H w); auto. congruence.
    + rewrite B.
      red; intros; simpl; erewrite (wt_expr_2_is_undef _ _ _ H w); auto. congruence.
    + rewrite B.
      red; intros; simpl; erewrite (wt_expr_2_is_undef _ _ _ H w); auto. congruence.
    + rewrite B.
      red; intros; simpl; erewrite (wt_expr_2_is_undef _ _ _ H w); auto. congruence.
  - des (get_type v); repeat destr; rewrite B; red; intros;
    simpl; rewrite ! nwt_expr_undef; auto.
Qed.

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'.
Proof.
  intros. unfold load.
  destruct (valid_access_dec m1 chunk' b' ofs' Readable).
  rewrite pred_dec_true.
  decEq. rewrite store_mem_contents; simpl; auto.
  rewrite PMap.gsspec. destruct (peq b' b); auto. subst b'. f_equal.
  apply getN_setN_outside. rewrite encode_val_length. repeat rewrite <- size_chunk_conv.
  intuition.
  auto.
  eauto with mem.
  rewrite pred_dec_false. auto.
  eauto with mem.
Qed.

Theorem loadbytes_store_same:
  loadbytes m2 b ofs (size_chunk chunk) = Some (encode_val chunk v).
Proof.
 intros.
  assert (valid_access m2 chunk b ofs Readable) by eauto with mem.
  unfold loadbytes. rewrite pred_dec_true. rewrite store_mem_contents; simpl.
  rewrite PMap.gss.
  replace (nat_of_Z (size_chunk chunk)) with (length (encode_val chunk v)).
  rewrite getN_setN_same. auto.
  rewrite encode_val_length. auto.
  apply H.
Qed.

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.
Proof.
   intros. unfold loadbytes.
  destruct (range_perm_dec m1 b' ofs' (ofs' + n) Cur Readable).
  rewrite pred_dec_true.
  decEq. rewrite store_mem_contents; simpl.
  rewrite PMap.gsspec. destruct (peq b' b). subst b'.
  destruct H. congruence.
  destruct (zle n 0) as [z | n0].
  rewrite (nat_of_Z_neg _ z). auto.
  destruct H. omegaContradiction.
  apply getN_setN_outside. rewrite encode_val_length. rewrite <- size_chunk_conv.
  rewrite nat_of_Z_eq. auto. omega.
  auto.
  red; intros. eauto with mem.
  rewrite pred_dec_false. auto.
  red; intro; elim n0; red; intros; eauto with mem.
Qed.

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)).
Proof.
  induction vl; intros.
  simpl in H0. omegaContradiction.
  simpl length in H0. rewrite inj_S in H0. simpl.
  destruct (zeq p q). subst q. rewrite setN_outside. rewrite ZMap.gss.
  auto with coqlib. omega.
  apply IHvl. auto with coqlib. omega.
Qed.

Lemma getN_in:
  forall c q n p,
  p <= q < p + Z_of_nat n ->
  In (ZMap.get q c) (getN n p c).
Proof.
  induction n; intros.
  simpl in H; omegaContradiction.
  rewrite inj_S in H. simpl. destruct (zeq p q).
  subst q. auto.
  right. apply IHn. omega.
Qed.

Lemma psa_ptr:
  forall l b o, proj_symbolic_aux_le l = Eval (Vptr b o) -> False.
Proof.
  unfold proj_symbolic_le.
  induction l; destr.
Qed.

Lemma ps_ptr:
  forall l b o, proj_symbolic_le l = Eval (Vptr b o) -> False.
Proof.
  intros.
  eapply psa_ptr; eauto.
Qed.

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').
Proof.
  intros.
  assert (True) by (destruct m1; auto).
  contradict H.
  unfold load.
  destr_cond_match; try congruence.
  Transparent decode_val.
  unfold decode_val. intro H. inv H.
  des chunk'.
  - inv H2.
  - repeat destr_in H2.
  - repeat destr_in H2. repeat destr_in Heqo. inv H2.
Qed.



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.
Proof.
  unfold store; intros.
  destr_in H; inv H.
  unfold size_block. simpl. auto.
Qed.


Lemma store_mask:
  forall chunk m b o v m',
    store chunk m b o v = Some m' ->
    mask m' = mask m.
Proof.
  unfold store; intros.
  destr_in H.
  inv H; simpl.
  unfold mask. simpl. auto.
Qed.


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.
Proof.
  intros.
  exploit store_size_block; eauto.
  exploit store_mask; eauto.
  unfold store in H.
  destr_in H.
  inv H; simpl. intros.
  unfold mk_block_list. simpl.
  rewrite H0. auto.
Qed.





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'.
Proof.
  intros.
  unfold size_block, get_size.
  unfold store in H.
  repeat destr_in H; inv H; simpl. auto.
Qed.

Lemma store_in_bound_m_1:
  forall b' ofs',
    in_bound_m ofs' m1 b' ->
    in_bound_m ofs' m2 b'.
Proof.
  unfold in_bound_m.
  intros.
  erewrite <- bounds_of_block_store; eauto.
Qed.

Lemma store_in_bound_m_2:
  forall b' ofs',
    in_bound_m ofs' m2 b' ->
    in_bound_m ofs' m1 b'.
Proof.
  unfold in_bound_m.
  intros.
  erewrite bounds_of_block_store; eauto.
Qed.


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.
Proof.
  intros.
  generalize (bounds_of_block_store _ _ _ _ _ _ H).
  generalize (Mem.nat_mask_store _ _ _ _ _ _ H).
  intros M B.
  apply norm_same_compat; auto.
Qed.

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.
Proof.
  intros.
  unfold Mem.storev in H; revert H; destr.
  eapply store_norm; eauto.
Qed.

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.
Proof.
  intros. unfold store.
  assert (size_chunk chunk1 = size_chunk chunk2).
  {
    repeat rewrite size_chunk_conv.
    erewrite <- (encode_val_length chunk1 v1); eauto.
    erewrite <- (encode_val_length chunk2 v2); eauto.
    rewrite H. auto.
  }
  destruct (valid_access_dec m chunk1 b ofs Writable);
  destruct (valid_access_dec m chunk2 b ofs Writable); auto.
  erewrite (mkmem_ext); eauto.
  rewrite H; auto.
  elim n. apply valid_access_compat with chunk1; auto. omega.
  elim n. apply valid_access_compat with chunk2; auto. omega.
Qed.

Theorem store_signed_unsigned_8:
  forall m b ofs v,
  store Mint8signed m b ofs v = store Mint8unsigned m b ofs v.
Proof.
  intros.
  apply store_similar_chunks.
  apply encode_val_int8_signed_unsigned.
  simpl. omega.
Qed.

Theorem store_signed_unsigned_16:
  forall m b ofs v,
  store Mint16signed m b ofs v = store Mint16unsigned m b ofs v.
Proof.
  intros.
  apply store_similar_chunks.
  apply encode_val_int16_signed_unsigned.
  simpl. omega.
Qed.

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).
Proof.
  induction al; simpl; intros.
  rewrite ZMap.gso; auto.
  destruct (Z_eq_dec o ofs); subst.
  rewrite ZMap.set2. auto.
  destruct (Z_eq_dec o ofs0); subst.
  repeat rewrite setN_outside by omega.
  repeat rewrite ZMap.gss. auto.
  repeat rewrite IHal; auto.
Qed.


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 }.
Proof.
  intros. unfold storebytes.
  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable).
  econstructor; reflexivity.
  contradiction.
Defined.

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.
Proof.
  unfold storebytes, store. intros.
  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Cur Writable); inv H;
  destruct (valid_access_dec m1 chunk b ofs Writable).
  - erewrite mkmem_ext; eauto.
  - elim n. constructor; auto.
    erewrite encode_val_length in r; eauto. rewrite size_chunk_conv. auto.
Qed.

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.
Proof.
  unfold storebytes, store. intros.
  destruct (valid_access_dec m1 chunk b ofs Writable); inv H.
  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Cur Writable).
  erewrite mkmem_ext; eauto.
  destruct v0. elim n.
  erewrite encode_val_length;eauto. rewrite <- size_chunk_conv. auto.
Qed.
  
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.
Proof.
  unfold storebytes in STORE.
  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
  inv STORE.
  auto.
Qed.

Lemma storebytes_mem_contents:
   mem_contents m2 = PMap.set b (setN bytes ofs m1.(mem_contents)#b) m1.(mem_contents).
Proof.
  unfold storebytes in STORE.
  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
  inv STORE.
  auto.
Qed.

Theorem perm_storebytes_1:
  forall b' ofs' k p, perm m1 b' ofs' k p -> perm m2 b' ofs' k p.
Proof.
  intros. unfold perm in *. rewrite storebytes_access; auto.
Qed.

Theorem perm_storebytes_2:
  forall b' ofs' k p, perm m2 b' ofs' k p -> perm m1 b' ofs' k p.
Proof.
  intros. unfold perm in *. rewrite storebytes_access in H; auto.
Qed.

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.
Proof.
  intros. inv H. constructor; try red; auto with mem.
Qed.

Theorem storebytes_valid_access_2:
  forall chunk' b' ofs' p,
  valid_access m2 chunk' b' ofs' p -> valid_access m1 chunk' b' ofs' p.
Proof.
  intros. inv H. constructor; try red; auto with mem.
Qed.

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'.
Proof.
  intros; revert STORE.
  unfold storebytes; repeat destr_cond_match; try congruence.
  intro A; inv A; unfold size_of_block; reflexivity.
Qed.

Theorem mask_storebytes:
  forall b',
    mask m1 b' = mask m2 b'.
Proof.
  intros; revert STORE.
  unfold storebytes; repeat destr_cond_match; try congruence.
  intro A; inv A; unfold mask; reflexivity.
Qed.

Theorem bounds_of_block_storebytes:
  forall b',
    bounds_of_block m1 b' = bounds_of_block m2 b'.
Proof.
  intros; revert STORE; unfold storebytes; repeat destr_cond_match; try congruence.
  intro A; inv A; reflexivity.
Qed.

Theorem nat_mask_storebytes:
  forall b',
    nat_mask m1 b' = nat_mask m2 b'.
Proof.
  intros; revert STORE; unfold storebytes; repeat destr_cond_match; try congruence.
  intro A; inv A; reflexivity.
Qed.

Theorem nextblock_storebytes:
  nextblock m2 = nextblock m1.
Proof.
  intros.
  unfold storebytes in STORE.
  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
  inv STORE.
  auto.
Qed.

Theorem storebytes_valid_block_1:
  forall b', valid_block m1 b' -> valid_block m2 b'.
Proof.
  unfold valid_block; intros. rewrite nextblock_storebytes; auto.
Qed.

Theorem storebytes_valid_block_2:
  forall b', valid_block m2 b' -> valid_block m1 b'.
Proof.
  unfold valid_block; intros. rewrite nextblock_storebytes in H; auto.
Qed.

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.
Proof.
  intros.
  unfold storebytes in STORE.
  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
  inv STORE.
  auto.
Qed.

Theorem loadbytes_storebytes_same:
  loadbytes m2 b ofs (Z_of_nat (length bytes)) = Some bytes.
Proof.
  intros. unfold storebytes in STORE. unfold loadbytes.
  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
  try discriminate.
  rewrite pred_dec_true.
  decEq. inv STORE; simpl. rewrite PMap.gss. rewrite nat_of_Z_of_nat.
  apply getN_setN_same.
  red; eauto with mem.
Qed.

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.
Proof.
  intros. unfold loadbytes.
  destruct (range_perm_dec m1 b' ofs' (ofs' + len) Cur Readable).
  rewrite pred_dec_true.
  rewrite storebytes_mem_contents. decEq.
  rewrite PMap.gsspec. destruct (peq b' b). subst b'.
  apply getN_setN_disjoint. rewrite nat_of_Z_eq; auto. intuition congruence.
  auto.
  red; auto with mem.
  apply pred_dec_false.
  red; intros; elim n. red; auto with mem.
Qed.

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.
Proof.
  intros. apply loadbytes_storebytes_disjoint; auto.
  destruct H0; auto. right. apply Intv.disjoint_range; auto.
Qed.

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'.
Proof.
  intros. unfold load.
  destruct (valid_access_dec m1 chunk b' ofs' Readable).
  rewrite pred_dec_true.
  rewrite storebytes_mem_contents. decEq.
  rewrite PMap.gsspec. destruct (peq b' b). subst b'.
  rewrite getN_setN_outside. auto. rewrite <- size_chunk_conv. intuition congruence.
  auto.
  destruct v; split; auto. red; auto with mem.
  apply pred_dec_false.
  red; intros; elim n. destruct H0. split; auto. red; auto with mem.
Qed.


Lemma storebytes_size_block:
  size_block m2 = size_block m1.
Proof.
  unfold storebytes in STORE. destr_in STORE.
  inv STORE; auto.
Qed.

Lemma storebytes_blocksize:
  mem_blocksize m2 = mem_blocksize m1.
Proof.
  unfold storebytes in STORE. destr_in STORE.
  inv STORE; auto.
Qed.


Lemma storebytes_mask:
    mem_mask m2 = mem_mask m1.
Proof.
  unfold storebytes in STORE. destr_in STORE.
  inv STORE; auto.
Qed.

  
Lemma storebytes_mk_block_list:
  mk_block_list m2 = mk_block_list m1.
Proof.
  intros.
  unfold mk_block_list.
  erewrite storebytes_size_block; eauto.
  rewrite nextblock_storebytes; auto.
Qed.


Lemma size_block_storebytes:
  forall b',
    size_block m2 b' = size_block m1 b'.
Proof.
  intros.
  unfold size_block, get_size.
  rewrite storebytes_blocksize; auto.
Qed.

Lemma storebytes_in_bound_m_1:
    forall b' ofs',
      in_bound_m ofs' m1 b' ->
      in_bound_m ofs' m2 b'.
Proof.
  unfold in_bound_m.
  intros.
  erewrite <- bounds_of_block_storebytes; eauto.
Qed.

Lemma storebytes_in_bound_m_2:
    forall b' ofs',
      in_bound_m ofs' m2 b' ->
      in_bound_m ofs' m1 b'.
Proof.
  unfold in_bound_m.
  intros.
  erewrite bounds_of_block_storebytes; eauto.
Qed.


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'.
Proof.
  intros chunk m b ofs v m' STORE j ABI.
  red; intros.
  eapply ABI.
  erewrite Mem.bounds_of_block_store; eauto.
  auto.
Qed.


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'.
Proof.
  intros chunk m bofs v m'.
  unfold Mem.storev.
  destr.
  eapply store_abi; eauto.
Qed.


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'.
Proof.
  red; intros.
  eapply ABI.
  erewrite Mem.bounds_of_block_storebytes; eauto.
  auto.
Qed.


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).
Proof.
  induction bytes1; intros.
  simpl. decEq. omega.
  simpl length. rewrite inj_S. simpl. rewrite IHbytes1. decEq. omega.
Qed.

Lemma Forall_app_not:
  forall {A} P (a b:list A),
  (~ Forall P a) \/ (~ Forall P b) ->
  ~ Forall P (a++b).
Proof.
  intros.
  destruct H.
  intro.
  apply Forall_app_l in H0; congruence.
  intro.
  apply Forall_app_r in H0; congruence.
Qed.

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.
Proof.
  intros. generalize H; intro ST1. generalize H0; intro ST2.
  unfold storebytes; unfold storebytes in ST1; unfold storebytes in ST2.
  destruct (range_perm_dec m b ofs (ofs + Z_of_nat(length bytes1)) Cur Writable); try congruence.
  destruct (range_perm_dec m1 b (ofs + Z_of_nat(length bytes1)) (ofs + Z_of_nat(length bytes1) + Z_of_nat(length bytes2)) Cur Writable); try congruence.
  destruct (range_perm_dec m b ofs (ofs + Z_of_nat (length (bytes1 ++ bytes2))) Cur Writable).
  inv ST1; inv ST2; simpl.
  erewrite mkmem_ext; eauto.
  simpl.
  rewrite PMap.gss. rewrite setN_concat. symmetry. apply PMap.set2.
  elim n.
  rewrite app_length. rewrite inj_plus. red; intros.
  destruct (zlt ofs0 (ofs + Z_of_nat(length bytes1))).
  apply r. omega.
  eapply perm_storebytes_2; eauto. apply r0. omega.
Qed.

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.
Proof.
  intros.
  destruct (range_perm_storebytes m b ofs bytes1) as [m1 ST1].
  red; intros. exploit storebytes_range_perm; eauto. rewrite app_length.
  rewrite inj_plus. omega.
  destruct (range_perm_storebytes m1 b (ofs + Z_of_nat (length bytes1)) bytes2) as [m2' ST2].
  red; intros. eapply perm_storebytes_1; eauto. exploit storebytes_range_perm.
  eexact H. instantiate (1 := ofs0). rewrite app_length. rewrite inj_plus. omega.
  auto.
  assert (Some m2 = Some m2').
  rewrite <- H. eapply storebytes_concat; eauto.
  inv H0.
  exists m1; split; auto.
Qed.

Lemma load_align_chunk:
  forall m b ofs chunk v,
    load chunk m b ofs = Some v ->
    (align_chunk chunk | ofs).
Proof.
  intros until v.
  unfold load.
  destr_cond_match; try congruence.
  destruct v0.
  intros; auto.
Qed.

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.
Proof.
  intros.
  generalize (loadbytes_range_perm _ _ _ _ _ H); intro r.
  assert (r1 : range_perm m b o (o + 1) Cur Readable).
  {
    unfold range_perm in *.
    intros.
    apply r; omega.
  }
  assert (r2 : range_perm m b (o + 1) (o + n) Cur Readable).
  {
    unfold range_perm in *.
    intros.
    apply r; omega.
  }
  generalize (range_perm_loadbytes m b o 1 r1).
  generalize (range_perm_loadbytes m b (o+1) (n-1)).
  replace (o+1 +(n-1)) with (o+n) by omega.
  intros A B; specialize (A r2).
  destruct A; destruct B.
  rewrite H2; rewrite H1.
  repeat eexists; repeat split; eauto.
  replace n with (1 + (n - 1)) in H by omega.
  erewrite loadbytes_concat in H; eauto.
  inv H; auto.
  omega.
  omega.
Qed.

Lemma int_range_int64:
  forall i,
  0 <= Int.unsigned i <= Int64.max_unsigned.
Proof.
  intros.
  generalize (Int.unsigned_range i). split. omega.
  transitivity Int.modulus. omega.
  vm_compute. congruence.
Qed.

Lemma int_inf_two_p_32:
  forall i,
    0 <= Int.unsigned i < two_power_nat 32.
Proof.
  intros.
  change (two_power_nat 32) with Int.modulus.
  generalize (Int.unsigned_range i). omega.
Qed.

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.
Proof.
  intros.
  rewrite Int.add_unsigned. rewrite Int.unsigned_repr. auto.
  exploit store_valid_access_3. eexact H. intros [P Q]. simpl in Q.
  exploit (Zdivide_interval (Int.unsigned i) Int.modulus 8).
  omega. apply Int.unsigned_range. auto. exists (two_p (32-3)); reflexivity.
  change (Int.unsigned (Int.repr 4)) with 4. unfold Int.max_unsigned. omega.
Qed.



Properties related to alloc.


Lemma pos2nat_id:
  forall p,
    Pos.of_nat (S (pred (Pos.to_nat p))) = p.
Proof.
  intro.
  rewrite <- (S_pred (Pos.to_nat p) (pred (Pos.to_nat p))).
  rewrite Pos2Nat.id; auto.
  zify. omega.
Qed.


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'.
Proof.
  unfold alloc, low_alloc in ALLOC.
destr_in ALLOC. injection ALLOC; intros; subst; unfold mask; simpl in *.
  rewrite PMap.gso by congruence.
  reflexivity.
Qed.

Theorem size_of_block_alloc_other:
  forall b',
    b <> b' ->
    size_of_block m1 b' = size_of_block m2 b'.
Proof.
  unfold alloc, low_alloc in ALLOC.
destr_in ALLOC. injection ALLOC; intros; subst; unfold size_of_block; simpl.
  rewrite PMap.gso by congruence.
  reflexivity.
Qed.

Theorem bounds_of_block_alloc_other:
  forall b',
    b <> b' ->
    bounds_of_block m1 b' = bounds_of_block m2 b'.
Proof.
  unfold alloc, low_alloc in ALLOC.
destr_in ALLOC. injection ALLOC; intros; subst; unfold bounds_of_block; simpl.
  rewrite PMap.gso by congruence.
  reflexivity.
Qed.

Theorem nat_mask_alloc_other:
  forall b',
    b <> b' ->
    nat_mask m1 b' = nat_mask m2 b'.
Proof.
  intros; unfold nat_mask.
  f_equal; f_equal. f_equal. f_equal.
  apply mask_alloc_other; auto.
Qed.

Theorem nextblock_alloc:
  nextblock m2 = Psucc (nextblock m1).
Proof.
  unfold alloc, low_alloc in ALLOC.
destr_in ALLOC. injection ALLOC; intros. rewrite <- H0; auto.
Qed.

Theorem alloc_result:
  b = nextblock m1.
Proof.
  unfold alloc, low_alloc in ALLOC.
  destr_in ALLOC.
Qed.

Theorem valid_block_alloc:
  forall b', valid_block m1 b' -> valid_block m2 b'.
Proof.
  unfold valid_block; intros. rewrite nextblock_alloc.
  apply Plt_trans_succ; auto.
Qed.

Theorem fresh_block_alloc:
  ~(valid_block m1 b).
Proof.
  unfold valid_block. rewrite alloc_result. apply Plt_strict.
Qed.

Theorem valid_new_block:
  valid_block m2 b.
Proof.
  unfold valid_block. rewrite alloc_result. rewrite nextblock_alloc. apply Plt_succ.
Qed.

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'.
Proof.
  unfold valid_block; intros.
  rewrite nextblock_alloc in H. rewrite alloc_result.
  exploit Plt_succ_inv; eauto. tauto.
Qed.

Theorem perm_alloc_1:
  forall b' ofs k p, perm m1 b' ofs k p -> perm m2 b' ofs k p.
Proof.
  unfold perm; intros.
  unfold alloc, low_alloc in ALLOC.
destr_in ALLOC. injection ALLOC; intros. rewrite <- H1; simpl.
  subst b. rewrite PMap.gsspec. destruct (peq b' (nextblock m1)); auto.
  rewrite nextblock_noaccess in H. contradiction. subst b'. apply Plt_strict.
Qed.

Theorem perm_alloc_2:
  forall ofs k, 0 <= ofs < hi -> perm m2 b ofs k Freeable.
Proof.
  unfold perm; intros.
  unfold alloc, low_alloc in ALLOC.
destr_in ALLOC. injection ALLOC; intros. rewrite <- H1; simpl.
  subst b. rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true.
  rewrite zlt_true. simpl. auto with mem. omega. omega.
Qed.

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.
Proof.
  intros until p; unfold perm.
  unfold alloc, low_alloc in ALLOC.
destr_in ALLOC. inv ALLOC. simpl.
  rewrite PMap.gsspec. unfold eq_block. destruct (peq b' (nextblock m1)); intros.
  destruct (zle 0 ofs); try contradiction. destruct (zlt ofs hi); try contradiction.
  split; auto.
  auto.
Qed.

Theorem perm_alloc_3:
  forall ofs k p, perm m2 b ofs k p -> 0 <= ofs < hi.
Proof.
  intros. exploit perm_alloc_inv; eauto. rewrite dec_eq_true; auto.
Qed.

Theorem perm_alloc_4:
  forall b' ofs k p, perm m2 b' ofs k p -> b' <> b -> perm m1 b' ofs k p.
Proof.
  intros. exploit perm_alloc_inv; eauto. rewrite dec_eq_false; auto.
Qed.

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.
Proof.
  intros. inv H. constructor; auto with mem.
  red; auto with mem.
Qed.

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.
Proof.
  intros. constructor; auto with mem.
  red; intros. apply perm_alloc_2. omega.
Qed.

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.
Proof.
  intros. inv H.
  generalize (size_chunk_pos chunk); intro.
  destruct (eq_block b' b). subst b'.
  assert (perm m2 b ofs Cur p). apply H0. omega.
  assert (perm m2 b (ofs + size_chunk chunk - 1) Cur p). apply H0. omega.
  exploit perm_alloc_inv. eexact H2. rewrite dec_eq_true. intro.
  exploit perm_alloc_inv. eexact H3. rewrite dec_eq_true. intro.
  intuition omega.
  split; auto. red; intros.
  exploit perm_alloc_inv. apply H0. eauto. rewrite dec_eq_false; auto.
Qed.

Theorem load_alloc_unchanged:
  forall chunk b' ofs,
  valid_block m1 b' ->
  load chunk m2 b' ofs = load chunk m1 b' ofs.
Proof.
  intros. unfold load.
  destruct (valid_access_dec m2 chunk b' ofs Readable).
  exploit valid_access_alloc_inv; eauto. destruct (eq_block b' b); intros.
  subst b'. elimtype False. eauto with mem.
  rewrite pred_dec_true; auto.
  unfold alloc, low_alloc in ALLOC.
destr_in ALLOC. injection ALLOC; intros. rewrite <- H2; simpl.
  rewrite PMap.gso. auto. rewrite H1. apply sym_not_equal; eauto with mem.
  rewrite pred_dec_false. auto.
  eauto with mem.
Qed.

Theorem load_alloc_other:
  forall chunk b' ofs v,
  load chunk m1 b' ofs = Some v ->
  load chunk m2 b' ofs = Some v.
Proof.
  intros. rewrite <- H. apply load_alloc_unchanged. eauto with mem.
Qed.

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).
Proof.
  induction n; simpl; intros. lia.
  destruct H.
  destruct o.
  simpl.
  rewrite Int.add_zero; auto.
  simpl.
  rewrite IHn; auto.
  rewrite Int.add_assoc.
  f_equal. f_equal. f_equal.
  f_equal.
  rewrite Val.int_add_repr. f_equal. lia.
  lia.
Qed.

Lemma in_nth_error:
  forall (A: Type) (vl: list A) (x:A),
    In x vl ->
    exists n, nth_error vl n = Some x.
Proof.
  induction vl; simpl; intros.
  exfalso; auto.
  destruct H; subst; auto.
  exists O; auto.
  destruct (IHvl _ H).
  exists (S x0); auto.
Qed.

Lemma nth_error_length:
  forall (A:Type) (l:list A) x v,
    nth_error l x = Some v ->
    (length l > x)%nat.
Proof.
  induction l; simpl; intros.
  rewrite nth_error_nil in H; congruence.
  destruct x. omega.
  simpl in H.
  apply IHl in H. omega.
Qed.

Lemma init_block'_length:
  forall n b c,
    length (init_block' n b c) = n.
Proof.
  induction n; simpl; intros; eauto.
Qed.

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)).
Proof.
  induction n; simpl; intros.
  constructor.
  constructor; auto.
  - unfold init_block.
    rewrite ZMap.gi. auto.
Qed.

Theorem loadbytes_alloc_unchanged:
  forall b' ofs n,
  valid_block m1 b' ->
  loadbytes m2 b' ofs n = loadbytes m1 b' ofs n.
Proof.
  intros. unfold loadbytes.
  destruct (range_perm_dec m1 b' ofs (ofs + n) Cur Readable).
  rewrite pred_dec_true.
  unfold alloc, low_alloc in ALLOC.
destr_in ALLOC. injection ALLOC; intros A B. rewrite <- B; simpl.
  rewrite PMap.gso. auto. rewrite A. eauto with mem.
  red; intros. eapply perm_alloc_1; eauto.
  rewrite pred_dec_false; auto.
  red; intros; elim n0. red; intros. eapply perm_alloc_4; eauto. eauto with mem.
Qed.

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.
Proof.
  unfold loadbytes; intros. destruct (range_perm_dec m2 b ofs (ofs + n) Cur Readable); inv H.
  revert H0.
  unfold alloc, low_alloc in ALLOC.
destr_in ALLOC. injection ALLOC; intros A B. rewrite <- A; rewrite <- B; simpl. rewrite PMap.gss.
  revert byte.
  rewrite <- Forall_forall.
  destruct (zle n 0).
  rewrite nat_of_Z_neg. simpl; constructor. auto.
  apply init_block_eundef.
Qed.


Opaque Pos.of_nat.


Lemma bounds_of_block_alloc:
    bounds_of_block m2 b = (0,Z.max 0 hi).
Proof.
  intros.
  unfold alloc, low_alloc in ALLOC.
destr_in ALLOC. unfold bounds_of_block; inv ALLOC; simpl.
  rewrite PMap.gss. auto.
Qed.


Lemma bounds_of_block_alloc_old:
  bounds_of_block m1 b = (0,0).
Proof.
  intros.
  unfold alloc, low_alloc in ALLOC.
destr_in ALLOC. unfold bounds_of_block; inv ALLOC; simpl.
  rewrite bs_valid; auto. xomega.
Qed.

Lemma alloc_mask:
  mask m2 b = alignment_of_size hi.
Proof.
  unfold alloc, low_alloc in ALLOC.
  destr_in ALLOC.
  inv ALLOC.
  unfold mask; simpl.
  rewrite PMap.gss. auto.
  rewrite Z.sub_0_r; auto.
  rewrite Max.max_idempotent.
  rewrite Min.min_r. auto.
  generalize MA_bound (alignment_of_size_bnd hi); lia.
Qed.


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).
Proof.
  intros.
  destr.
  subst.
  erewrite bounds_of_block_alloc; eauto.
  destr.
  erewrite <- bounds_of_block_alloc_other; eauto.
  unfold bounds_of_block; rewrite bs_valid; auto.
Qed.



Lemma alloc_in_bound:
  forall b0 o,
    in_bound_m (Int.unsigned o) m1 b0 ->
    in_bound_m (Int.unsigned o) m2 b0.
Proof.
  intros b0 o IB.
  unfold in_bound_m in *.
  erewrite bounds_of_block_alloc_eq; eauto.
  destr_cond_match; subst; auto.
  + erewrite bounds_of_block_alloc_old in IB; eauto.
    unfold NormaliseSpec.in_bound in IB; simpl in IB; omega.
  + destr_cond_match; simpl; auto.
    destruct (bounds_of_block m1 b0) eqn:?; simpl in *.
    destruct IB; simpl in *.
    destruct (zeq z z0); subst. omega.
    apply Mem.bounds_of_block_valid in Heqp; auto.
    unfold Mem.valid_block in Heqp. clear Heqs0.
    rewrite nextblock_alloc in n0.
    xomega.
Qed.



Lemma mask_alloc_old:
  mask m1 b = O.
Proof.
  intros.
  unfold alloc, low_alloc in ALLOC.
destr_in ALLOC. unfold nat_mask, mask; inv ALLOC; simpl.
  rewrite msk_valid; auto. xomega.
Qed.

Lemma nat_mask_alloc_old:
  nat_mask m1 b = Int.mone.
Proof.
  unfold nat_mask.
  erewrite mask_alloc_old; eauto.
  rewrite two_power_nat_O. change (Int.repr (1-1)) with Int.zero.
  apply Int.not_zero.
Qed.

Lemma compat_alloc:
  forall cm q,
    compat_m m2 q cm ->
    compat_m m1 q cm.
Proof.
  intros cm q COMPAT.
  inv COMPAT. constructor; simpl; intros; eauto.
  - eapply addr_space.
    eapply alloc_in_bound; eauto.
  - eapply overlap; eauto.
    eapply alloc_in_bound; eauto.
    eapply alloc_in_bound; eauto.
  - generalize nat_mask_alloc_old; intro A.
     destruct (peq b b0); subst.
    + rewrite A. apply Int.and_mone.
    + rewrite nat_mask_alloc_other; eauto.
Qed.

Lemma norm_alloc:
  forall e v,
    Mem.mem_norm m1 e = v ->
    v <> Vundef ->
    Mem.mem_norm m2 e = v.
Proof.
  intros e v MN NU.
  generalize (norm_correct m1 e).
  rewrite MN.
  intro A; inv A.
  assert (is_norm_m m2 e (Mem.mem_norm m1 e)).
  {
    constructor.
    - red; intros.
      eapply lessdef_on_P_impl; eauto.
      eapply compat_alloc with (q:=M32); eauto.
  }
  generalize (norm_complete m2 e _ H).
  intro A; inv A; congruence.
Qed.

Lemma normalise_alloc:
  forall e,
    Values.Val.lessdef (Mem.mem_norm m1 e) (Mem.mem_norm m2 e).
Proof.
  intros.
  generalize (norm_alloc e _ eq_refl). intros B.
  des (mem_norm m1 e); auto; try rewrite <- B; auto; destr.
Qed.

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).
Proof.
  induction n; simpl; intros.
  - omega.
  - des (eq_nat_dec ofs O).
    + rewrite Int.add_zero. reflexivity.
    + des ofs.
      rewrite IHn by omega.
      f_equal. f_equal. f_equal.
      rewrite Int.add_assoc.
      f_equal.
      zify. rewrite <- Z.add_1_l.
      rewrite Val.int_add_repr.
      auto.
Qed.

Lemma init_block_length:
  forall n b i,
    length (init_block' n b i) = n.
Proof.
  induction n; simpl; intros; try omega.
  rewrite IHn; omega.
Qed.

Lemma get_init_block:
  forall ofs lo hi b,
    ZMap.get ofs (init_block lo hi b) = Symbolic (Eval Vundef) None O.
Proof.
  clear.
  unfold init_block. intros; rewrite ZMap.gi. auto.
Qed.

Lemma mem_alloc_block_undefs:
  block_undefs 0 hi 0 m2 b.
Proof.
  unfold Mem.alloc, Mem.low_alloc in ALLOC.
  destr_in ALLOC.
  inv ALLOC.
  red; simpl. intros.
  rewrite PMap.gss.
  intros; rewrite Z.add_0_r.
  apply get_init_block; auto.
Qed.

Lemma alloc_contents_old:
  forall b' (DIFF: b' <> b),
    (mem_contents m2) # b' = (mem_contents m1) # b'.
Proof.
  unfold alloc, low_alloc in ALLOC. destr_in ALLOC. inv ALLOC; simpl.
  intros;
  rewrite PMap.gso; auto.
Qed.

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.
Proof.
  unfold Mem.bounds_of_block, Mem.size_block, get_size.
  intros. repeat destr_in H; inv H; auto.
Qed.

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)).
Proof.
  Local Opaque Pos.of_nat.
  induction n; simpl; intros.
  unfold Alloc.mk_block_list_aux. simpl. auto.
  rewrite Alloc.mbla_rew.
  destr.
  rewrite H; [|xomega].
  rewrite Alloc.size_mem_aux_first.
  rewrite Z.max_r by lia. rewrite align_0. lia.
  apply two_power_nat_pos.
Qed.

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).
Proof.
  induction l; simpl; intros; eauto.
  unfold f at 2. des a.
  rewrite ! IHl.
  generalize tpMA_pos. intro. rewrite <- ! align_distr by lia.
  rewrite align_align by lia. rewrite align_0 by lia. simpl. lia.
Qed.
Lemma size_block_pos:
  forall m b,
    0 <= Mem.size_block m b.
Proof.
  unfold Mem.size_block, Alloc.get_size.
  intros.
  repeat destr. 2: lia.
  exploit Mem.bounds_lo_inf0; eauto. lia.
Qed.

Lemma mbl_pos:
  forall m,
    Forall (fun x : block * Z => 0 <= snd x) (mk_block_list m).
Proof.
  unfold mk_block_list.
  intros; generalize (pred (Pos.to_nat (nextblock m))).
  induction n; simpl; intros. constructor.
  rewrite mbla_rew; constructor; auto. simpl. apply size_block_pos.
Qed.

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 }.
Proof.
  intros; unfold free. rewrite pred_dec_true; auto.
  rewrite H0.
  econstructor; eauto.
Defined.

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.
Proof.
  unfold free in FREE. destruct (range_perm_dec m1 bf lo hi Cur Freeable); auto.
  congruence.
Qed.

Lemma free_result:
  m2 = unchecked_free m1 bf lo hi.
Proof.
  unfold free in FREE.
  repeat destr_in FREE.
Qed.

Lemma mask_free:
  forall b', Mem.mask m1 b' = Mem.mask m2 b'.
Proof.
  intros.
  unfold Mem.free in FREE. repeat destr_in FREE; inv FREE.
  reflexivity.
Qed.

Theorem size_of_block_free:
  forall b',
    bf <> b' ->
    size_of_block m1 b' = size_of_block m2 b'.
Proof.
  intros.
  rewrite free_result.
  unfold size_of_block, unchecked_free; try reflexivity.
  simpl.
  rewrite PMap.gso by congruence; reflexivity.
Qed.

Theorem nextblock_free:
  nextblock m2 = nextblock m1.
Proof.
  rewrite free_result; reflexivity.
Qed.

Theorem valid_block_free_1:
  forall b, valid_block m1 b -> valid_block m2 b.
Proof.
  intros. rewrite free_result. assumption.
Qed.

Theorem valid_block_free_2:
  forall b, valid_block m2 b -> valid_block m1 b.
Proof.
  intros. rewrite free_result in H. assumption.
Qed.

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.
Proof.
  intros. rewrite free_result. unfold perm, unchecked_free; simpl.
  rewrite PMap.gsspec. destruct (peq b bf). subst b.
  destruct (zle lo ofs); simpl.
  destruct (zlt ofs hi); simpl.
  elimtype False; intuition.
  auto. auto.
  auto.
Qed.

Theorem perm_free_2:
  forall ofs k p, lo <= ofs < hi -> ~ perm m2 bf ofs k p.
Proof.
  intros. rewrite free_result. unfold perm, unchecked_free; simpl.
  rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true.
  simpl. tauto. omega. omega.
Qed.

Theorem perm_free_3:
  forall b ofs k p,
  perm m2 b ofs k p -> perm m1 b ofs k p.
Proof.
  intros until p. rewrite free_result. unfold perm, unchecked_free; simpl.
  rewrite PMap.gsspec. destruct (peq b bf). subst b.
  destruct (zle lo ofs); simpl.
  destruct (zlt ofs hi); simpl. tauto.
  auto. auto. auto.
Qed.

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.
Proof.
  intros. rewrite free_result. unfold perm, unchecked_free; simpl.
  rewrite PMap.gsspec. destruct (peq b bf); auto. subst b.
  destruct (zle lo ofs); simpl; auto.
  destruct (zlt ofs hi); simpl; auto.
Qed.

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.
Proof.
  intros. inv H. constructor; auto with mem.
  red; intros. eapply perm_free_1; eauto.
  destruct (zlt lo hi). intuition. right. omega.
Qed.

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).
Proof.
  intros; red; intros. inv H2.
  generalize (size_chunk_pos chunk); intros.
  destruct (zlt ofs lo).
  elim (perm_free_2 lo Cur p).
  omega. apply H3. omega.
  elim (perm_free_2 ofs Cur p).
  omega. apply H3. omega.
Qed.

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.
Proof.
  intros. destruct H. split; auto.
  red; intros. generalize (H ofs0 H1).
  rewrite free_result. unfold perm, unchecked_free; simpl.
  rewrite PMap.gsspec. destruct (peq b bf). subst b.
  destruct (zle lo ofs0); simpl.
  destruct (zlt ofs0 hi); simpl.
  tauto. auto. auto. auto.
Qed.

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.
Proof.
  intros.
  destruct (zlt lo hi); auto.
  destruct (zle (ofs + size_chunk chunk) lo); auto.
  destruct (zle hi ofs); auto.
  elim (valid_access_free_2 chunk ofs p); auto. omega.
Qed.

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.
Proof.
  intros. unfold load.
  destruct (valid_access_dec m2 chunk b ofs Readable).
  rewrite pred_dec_true.
  rewrite free_result; auto.
  eapply valid_access_free_inv_1; eauto.
  rewrite pred_dec_false; auto.
  red; intro; elim n. eapply valid_access_free_1; eauto.
Qed.

Theorem load_free_2:
  forall chunk b ofs v,
  load chunk m2 b ofs = Some v -> load chunk m1 b ofs = Some v.
Proof.
  intros. unfold load. rewrite pred_dec_true.
  rewrite (load_result _ _ _ _ _ H). rewrite free_result; auto.
  apply valid_access_free_inv_1. eauto with mem.
Qed.

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.
Proof.
  intros. unfold loadbytes.
  destruct (range_perm_dec m2 b ofs (ofs + n) Cur Readable).
  rewrite pred_dec_true.
  rewrite free_result; auto.
  red; intros. eapply perm_free_3; eauto.
  rewrite pred_dec_false; auto.
  red; intros. elim n0; red; intros.
  eapply perm_free_1; eauto. destruct H; auto. right; omega.
Qed.

Theorem loadbytes_free_2:
  forall b ofs n bytes,
  loadbytes m2 b ofs n = Some bytes -> loadbytes m1 b ofs n = Some bytes.
Proof.
  intros. unfold loadbytes in *.
  destruct (range_perm_dec m2 b ofs (ofs + n) Cur Readable); inv H.
  rewrite pred_dec_true. rewrite free_result; auto.
  red; intros. apply perm_free_3; auto.
Qed.

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'.
Proof.
  intros.
  Opaque zeq.
  unfold unchecked_free, bounds_of_block, eq_block; simpl.
  rewrite PMap.gsspec.
  unfold get_size.
  des (mem_blocksize m) # b;
    destruct (peq b' b); subst; destr; try des p;
    unfold bounds_of_block; try rewrite Heqo; destr;
    try rewrite Heqo0; auto.
  inv Heqo0. auto.
Qed.

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).
Proof.
  intros m b lo hi m' b' FREE.
  unfold Mem.free in FREE. repeat destr_in FREE; inv FREE.
  rewrite unchecked_free_bounds'.
  repeat destr.
Qed.

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'.
Proof.
  red; intros.
  destruct (Mem.free_bounds' _ _ _ _ _ b0 FREE).
  eapply ABI; eauto. congruence.
  rewrite H in H1; inv H1. omega.
Qed.

Lemma free_mask:
  forall m b lo hi m' b',
    free m b lo hi = Some m' ->
    mask m' b' = mask m b'.
Proof.
  intros m b lo hi m' b' FREE.
  unfold Mem.free in FREE. repeat destr_in FREE; inv FREE.
  reflexivity.
Qed.


Lemma freelist_mask:
  forall l m m' b',
    free_list m l = Some m' ->
    mask m' b' = mask m b'.
Proof.
  induction l; simpl; intros; eauto.
  inv H; auto.
  des a; des p.
  destr_in H.
  specialize (IHl _ _ b' H).
  rewrite IHl.
  eapply free_mask; eauto.
Qed.

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'.
Proof.
  induction l; simpl; intros; eauto.
  inv FREE; auto.
  destruct a as [[b lo] hi].
  des (Mem.free m b lo hi).
  eapply IHl; eauto.
  eapply free_abi; eauto.
Qed.


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.
Proof.
  intros.
  inv COMP.
  constructor; simpl; intros.
  - destruct (free_bounds' _ _ _ _ _ b0 FREE).
    + rewrite H0 in H; eauto.
    + rewrite H0 in H.
      unfold in_bound in H; simpl in H; omega.
  - destruct (Mem.free_bounds' _ _ _ _ _ b0 FREE);
    rewrite H2 in H0; eauto;
    destruct (Mem.free_bounds' _ _ _ _ _ b' FREE);
      rewrite H3 in H1; eauto;
      unfold in_bound in *; simpl in *; try omega.
  - unfold Mem.nat_mask.
    erewrite Mem.free_mask; eauto.
Qed.


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.
Proof.
  intros.
  inv COMP.
  constructor; simpl; intros.
  - rewrite unchecked_free_bounds' in H.
    destruct (eq_block b0 b); eauto.
    subst.
    destruct (bounds_of_block m b) eqn:?.
    destruct (zeq z lo && zeq z0 hi); eauto.
    red in H; simpl in H; omega.
    apply addr_space; auto. congruence.
  - rewrite unchecked_free_bounds' in *.
    destruct (eq_block b0 b), (eq_block b' b); subst; eauto;
    destruct (bounds_of_block m b) eqn:?;
             destruct (zeq z lo && zeq z0 hi); eauto.
    red in H0; simpl in H0; omega.
    apply overlap; auto. congruence.
    red in H1; simpl in H1; omega.
    apply overlap; auto. congruence.
  - unfold Mem.nat_mask.
    erewrite unchecked_free_mask; eauto.
Qed.


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.
Proof.
  intros m1 bf lo hi m2 FREE e v MN NU.
  generalize (norm_correct m2 e).
  rewrite MN.
  intro A; inv A.
  assert (is_norm_m m1 e (Mem.mem_norm m2 e)).
  {
    constructor.
    - eapply lessdef_on_P_impl; eauto. intro.
      eapply compat_free with (q:=M32); eauto.
  }
  generalize (norm_complete m1 e _ H).
  intro A; inv A; congruence.
Qed.

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.
Proof.
  intros m1 bf lo hi e v MN NU.
  generalize (norm_correct (unchecked_free m1 bf lo hi) e).
  rewrite MN.
  intro A; inv A.
  assert (is_norm_m m1 e (Mem.mem_norm (unchecked_free m1 bf lo hi) e)).
  {
    constructor.
    - eapply lessdef_on_P_impl; eauto.
      intro;
        eapply compat_unchecked_free with (q:=M32); eauto.
  }
  generalize (norm_complete m1 e _ H).
  intro A; inv A; congruence.
Qed.

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).
Proof.
  intros.
  generalize (norm_free _ _ _ _ _ FREE e _ eq_refl).
  intro H0.
  des (mem_norm m2 e); auto; rewrite <- H0; auto; destr.
Qed.

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.
Proof.
  intros; unfold unchecked_free, bounds_of_block; simpl.
  rewrite PMap.gss.
  des ((mem_blocksize m) # b). des p.
  destr.
  repeat destr.
Qed.

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'.
Proof.
  intros; unfold unchecked_free, bounds_of_block; simpl.
  rewrite PMap.gso; auto.
Qed.


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'.
Proof.
  intros.
  unfold Mem.free in H.
  repeat destr_in H. inv H.
  unfold Mem.unchecked_free. unfold Mem.bounds_of_block; simpl.
  rewrite PMap.gso by congruence. auto.
Qed.

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.
Proof.
  induction fbl; simpl; intros.
  inv H. auto.
  destruct a as [[b' lo] hi]. destruct (Mem.free m b' lo hi) eqn:?; try congruence.
  intros. intuition try congruence. simpl in *.
  generalize (IHfbl _ _ _ H H2).
  intro A; rewrite A.
  erewrite bounds_free; eauto.
Qed.

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.
Proof.
  induction fbl; simpl; intros.
  inv H. auto.
  destruct a as [[b' lo'] hi']. destruct (Mem.free m b' lo' hi') eqn:?; try congruence.
  intros. intuition try congruence. simpl in *.
  generalize (IHfbl _ _ _ H H3 _ _ _ _ H1).
  unfold Mem.range_perm. intros.
  specialize (H0 ofs H4).
  eapply Mem.perm_free_3; eauto.
Qed.

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'.
Proof.
  intros.
  unfold free in H.
  repeat destr_in H.
  inv H.
  unfold Mem.unchecked_free; simpl. auto.
Qed.



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'.
Proof.
  induction fbl; simpl; intros; eauto.
  inv H; auto.
  repeat destr_in H.
  rewrite <- (IHfbl _ _ _ H).
  rewrite (Mem.free_contents _ _ _ _ _ Heqo). auto.
Qed.

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.
Proof.
  induction fbl; simpl; intros.
  inv H; auto.
  destruct a as [[b0 lo] hi].
  destruct (Mem.free m b0 lo hi) eqn:?; try congruence.
  generalize (IHfbl _ _ _ H H0).
  intros.
  intro.
  generalize (Mem.valid_block_free_1 _ _ _ _ _ Heqo _ H2); auto.
Qed.


Lemma permut_filter:
  forall A f (l l' : list A)
    (P: Permutation l l'),
    Permutation (filter f l) (filter f l').
Proof.
  induction 1; simpl; intros; eauto.
  destr. constructor; auto.
  destr; destr; try reflexivity.
  apply perm_swap.
  eapply Permutation_trans; eauto.
Qed.

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).
Proof.
  induction l; simpl; intros. auto.
  rewrite IHl.
  rewrite align_align. auto. apply two_power_nat_pos.
Qed.

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.
Proof.
  intros.
  apply size_mem_al_permut; try omega.
  apply two_power_nat_pos.
  apply Permutation.Permutation_rev.
Qed.

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).
Proof.
  intros.
  unfold size_mem_al.
  rewrite fold_left_app. auto.
Qed.

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).
Proof.
  induction l; simpl; intros; auto.
  apply IHl.
  destruct a.
  rewrite <- ! align_distr.
  rewrite align_align; try lia.
  apply two_power_nat_pos.
  apply two_power_nat_pos.
  apply two_power_nat_pos.
Qed.

Lemma size_mem_aux_aligned:
  forall l,
    size_mem_aux MA l = align (size_mem_aux MA l) (two_power_nat MA).
Proof.
  intros; unfold size_mem_aux.
  apply size_mem_al_aligned; auto.
  rewrite align_refl; auto.
  apply two_power_nat_pos.
Qed.






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.
Proof.
  unfold drop_perm; intros.
  destruct (range_perm_dec m b lo hi Cur Freeable). auto. discriminate.
Qed.

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' }.
Proof.
  unfold drop_perm; intros.
  destruct (range_perm_dec m b lo hi Cur Freeable). econstructor. eauto. contradiction.
Defined.



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'.
Proof.
  revert DROP; unfold drop_perm; destr_cond_match; try congruence.
  intro A; inv A.
  intros.
  unfold mask; reflexivity.
Qed.

Theorem size_of_block_drop_perm:
  forall b',
    size_of_block m b' = size_of_block m' b'.
Proof.
  revert DROP; unfold drop_perm; destr_cond_match; try congruence.
  intro A; inv A.
  intros.
  unfold size_of_block; reflexivity.
Qed.

Theorem nextblock_drop:
  nextblock m' = nextblock m.
Proof.
  unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP; auto.
Qed.

Theorem drop_perm_valid_block_1:
  forall b', valid_block m b' -> valid_block m' b'.
Proof.
  unfold valid_block; rewrite nextblock_drop; auto.
Qed.