Module Alloc

Require Import Zwf.
Require Import Axioms.
Require Import Coqlib.
Require Intv.
Require Import Maps.
Require Archi.
Require Import Integers.
Require Import IntFacts.
Require Import Values.
Require Import List Sorted Orders.
Require Import Mergesort.
Require Import Permutation.
Require Import NormaliseSpec.
Local Notation "a # b" := (PMap.get b a) (at level 1).


This module defines a greedy allocation algorithm that ensures that a concrete memory exists for a given abstract memory.

Ltac elim_div :=
  unfold Zdiv, Zmod in *;
  repeat
    match goal with
      | H : context[ Zdiv_eucl ?X ?Y ] |- _ =>
         generalize (Z_div_mod_full X Y) ; destruct (Zdiv_eucl X Y)
      | |- context[ Zdiv_eucl ?X ?Y ] =>
         generalize (Z_div_mod_full X Y) ; destruct (Zdiv_eucl X Y)
    end; unfold Remainder.

Ltac unf_modulus :=
  change (Int.modulus) with 4294967296 in *.



Properties of the align function.

Lemma align_plus:
  forall al z,
    al = 1 \/ al = 2 \/ al = 4 \/ al = 8 ->
    align (align z al) 8 = align z 8.
Proof.
  intros al z.
  unfold align. intros.
  elim_div. assert (al <> 0) by omega.
  intuition subst; omega.
Qed.

Lemma align_align:
  forall z a (apos: a > 0),
    align (align z a) a = align z a.
Proof.
  intros.
  generalize (align_divides z a apos).
  intro A; destruct A as (x & A).
  rewrite A.
  unfold align.
  rewrite <- Z.div_unique with (q:=x) (r:= a-1).
  auto.
  left; omega.
  rewrite Z.mul_comm. omega.
Qed.

Lemma align_ge1:
  forall sz al,
    al > 0 ->
    exists b, 0 <= b < al /\
              align sz al = sz + b /\
              b = (al - 1 - (sz - 1 - al * ((sz - 1) / al))).
Proof.
  intros.
  generalize (align_le sz al H).
  destruct (align_divides sz al H).
  rewrite H0.
  intros.
  unfold align in H0.
  rewrite <- H0.
  replace ((sz+al-1)/al) with (1+ ((sz-1)/al)).
  {
    replace ((1+ ((sz-1)/al))*al) with (al + (sz -1)/al *al).
    {
      rewrite Z.mul_comm.
      replace (al * ((sz - 1) / al)) with
      (al * ((sz - 1) / al) + (sz-1) mod al - (sz-1) mod al) by omega.
      rewrite <- Z.div_mod by omega.
      rewrite Z.mod_eq by omega.
      exists (al - 1 - (sz - 1 - al * ((sz - 1) / al))).
      split; try omega.
      {
        elim_div. assert (al <> 0) by omega. intuition.
      }
    }
    rewrite Z.mul_add_distr_r. omega.
  }
  {
    replace (sz + al - 1) with ((sz -1) + 1*al) by omega.
    rewrite Z_div_plus_full by omega.
    omega.
  }
Qed.

Lemma align_add:
  forall al sz sz',
    al > 0 ->
    0 <= sz <= sz' ->
    align sz al <= align sz' al.
Proof.
  intros.
  generalize (align_ge1 sz al H)
             (align_ge1 sz' al H).
  intros [b [A [B C]]] [c [D [E F]]].
  destruct (zlt (sz'-sz) al); try intuition omega.
  assert (exists d, 0 <= d < al /\ sz' = sz + d).
  {
    clear - H0 H l.
    exists (sz'-sz). intuition try omega.
  }
  destruct H1 as [d [ENC EQ]]. rewrite EQ in *.
  clear EQ.

  rewrite B; rewrite E.
  cut ( al * ((sz - 1) / al) <=
      ( al * ((sz + d - 1) / al))); intros; try omega.
  apply Z.mul_le_mono_nonneg_l; try omega.
  apply Z.div_le_mono; try omega.
Qed.

Lemma align_distr:
  forall z z1,
    align z 8 + align z1 8 = align (align z 8 + z1) 8.
Proof.
  unfold align. intros.
  elim_div. intuition.
Qed.


Helper functions.
Definition get_mask (m: PMap.t (option nat)) (b:block) : nat :=
  (match PMap.get b m with
       Some m => m | None => O
   end).

Definition get_size (bs: PMap.t (option (Z*Z))) (b:block) : Z :=
  match PMap.get b bs with
      Some (lo, hi) => hi-lo
    | None => 0
  end.

Definition get_bounds (bs: PMap.t (option (Z*Z))) (b:block) : Z*Z :=
  match PMap.get b bs with
      Some (lo, hi) => (lo,hi)
    | None => (0,0)
  end.

Definition alignment_of_size (sz:Z) : nat :=
  (if zlt sz 2 then O else if zlt sz 4 then 1 else if zlt sz 8 then 2 else 3)%nat.


Fixpoint list_ints (b:nat) : list nat :=
  match b with
      O => nil
    | S m => b :: list_ints m
  end.

Definition mk_block_list_aux (sz:block -> Z) (b:nat) :=
  map (fun n => let b':= Pos.of_nat n in
                (b',sz b'))
              (list_ints b).

Definition size_mem_al (al:Z) (lb: list (block*Z)) (b:Z) :=
  List.fold_left
    (fun acc (bsz:block*Z) =>
       let (b,sz) := bsz in
       align (align acc al + Z.max 0 sz) al
    ) lb b.

Lemma size_mem_al_permut:
  forall al lb lb',
    al > 0 ->
    Permutation lb lb' ->
    forall b,
      size_mem_al al lb b = size_mem_al al lb' b.
Proof.
  induction 2; simpl; intros; auto.
  - destruct x. destruct y.
    f_equal.
    generalize (align_divides b al H).
    generalize (align b al).
    intros.
    rewrite ! align_align; auto.
    destruct (align_divides (z1 + Z.max 0 z0) al H).
    destruct (align_divides (z1 + Z.max 0 z) al H).
    rewrite H1; rewrite H2.
    destruct H0 as [x1 H0]. subst.
    assert (forall x z a (apos: a > 0),
              align (x*a+z) a = x*a + align z a).
    {
      clear; intros.
      unfold align.
      rewrite <- Z.add_opp_r.
      rewrite <- ! Z.add_assoc.
      rewrite Z_div_plus_full_l; try omega.
      rewrite Z.add_assoc.
      rewrite Z.add_opp_r.
      rewrite Z.mul_add_distr_r.
      auto.
    }
    rewrite H0 in H1; auto.
    rewrite H0 in H2; auto.
    rewrite ! H0; auto.
    rewrite <- H1; auto. rewrite <- H2; auto. omega.
  - rewrite IHPermutation1. auto.
Qed.

Lemma size_mem_al_add:
  forall l b b' al,
    al > 0 ->
    0 <= b <= b' ->
    0 <= size_mem_al al l b <=
    size_mem_al al l b'.
Proof.
  induction l; simpl; intros; auto.
  destruct a.
  apply IHl; auto.
  split.
  generalize (align_le (align b al + Z.max 0 z) al H).
  generalize (align_le b al H).
  generalize (Zmax_spec 0 z).
  destr; omega.
  apply align_add; auto.
  split.
  generalize (align_le b al H).
  generalize (Zmax_spec 0 z).
  destr; omega.
  generalize (align_add al b b' H H0). omega.
Qed.

Definition size_mem_aux (t : list (block *Z)) : Z :=
  size_mem_al 8 t 8.

Definition alloc_mem_al (al:Z) (lb: list (block*Z)) (b : Z * (block -> Z)) :=
  List.fold_left
    (fun (acc:Z*(block-> Z)) (bsz:block*Z) =>
       let (cur,fn) := acc in
       let (b,sz) := bsz in
       let new := align cur al in
       (align (new + Z.max 0 sz) al,
        (fun bb => if peq bb b
                   then new
                   else fn bb))
    ) lb b.

Definition alloc_mem_aux (t : list (block *Z)) : Z * (block -> Z) :=
  alloc_mem_al 8 t (8, (fun _ => 0)).

Definition alloc_blocks (t: list (block*Z)) : option (block -> int) :=
  let (sz,m) := alloc_mem_aux t in
  if zlt sz Int.max_unsigned
  then Some (fun b => Int.repr (m b))
  else None.

Lemma alloc_size_mem_al:
  forall al bl zi mi z m,
    alloc_mem_al al bl (zi, mi) = (z, m) ->
    size_mem_al al bl zi = z.
Proof.
  induction bl; simpl; intros.
  inv H; auto.
  destruct a.
  apply IHbl in H; auto.
Qed.

Lemma alloc_size_mem_aux:
  forall bl z m,
    alloc_mem_aux bl = (z, m) ->
    size_mem_aux bl = z.
Proof.
  unfold alloc_mem_aux, size_mem_aux.
  intros until 0.
  apply alloc_size_mem_al.
Qed.

Remark permutation_norepet:
  forall (A: Type) (l l': list A),
    Permutation l l' ->
    list_norepet l ->
    list_norepet l'.
Proof.
  induction 1; intros.
  - constructor.
  - inv H0. constructor; auto. red; intros; elim H3.
    apply Permutation_in with l'; auto. apply Permutation_sym; auto.
  - inv H. simpl in H2. inv H3.
    constructor. simpl; intuition. constructor. intuition. auto.
  - eauto.
Qed.

Lemma size_mem_aux_alloc :
  forall t p,
    size_mem_aux t <=
    size_mem_aux (p::t).
Proof.
  intros.
  unfold size_mem_aux.
  destruct p as [b z].
  Opaque Z.add.
  simpl.
  apply size_mem_al_add.
  omega. split. omega.
  rewrite <- align_distr.
  change (align 8 8) with 8.
  generalize (align_le (Z.max 0 z) 8).
  rewrite Zmax_spec; destr; omega.
Qed.

Ltac trim H :=
  match type of H with
      ?A -> ?B =>
      let x:= fresh in
      assert (x:A); [|specialize (H x); clear x]
  end.

Lemma mk_block_list_aux_ext:
  forall sz sz' m
         (same_sz: forall i,
                     Ple i (Pos.of_nat m) ->
                     sz i = sz' i
         ),
    mk_block_list_aux sz m =
    mk_block_list_aux sz' m.
Proof.
  Opaque Pos.of_nat.
  induction m; simpl; auto.
  unfold mk_block_list_aux. simpl.
  intros.
  rewrite same_sz by xomega.
  trim IHm.
  - intros. apply same_sz.
    unfold Ple in *.
    rewrite Pos2Nat.inj_le in *.
    rewrite Nat2Pos.id_max in *.
    des m. omega.
  - destr.
    f_equal.
    apply IHm.
Qed.

Lemma if_false:
  forall {A} b (a c: A),
    b = false ->
    (if b then a else c) = c.
Proof.
  destruct b; auto. congruence.
Qed.

Lemma if_true:
  forall {A} b (a c: A),
    b = true ->
    (if b then a else c) = a.
Proof.
  destruct b; auto. congruence.
Qed.

Lemma get_size_same:
  forall b p t,
    get_size (PMap.set b (Some p) t) b = snd p - fst p.
Proof.
  intros; unfold get_size.
  rewrite PMap.gss. des p.
Qed.

Lemma size_mem_al_pos:
  forall l b al,
    al > 0 -> 0 <= b ->
    b <= size_mem_al al l b.
Proof.
  induction l; simpl; intros; auto.
  omega. destruct a.
  apply Zle_trans with (align (align b al + Z.max 0 z) al).
  generalize (align_le b al H).
  generalize (align_le (align b al + Z.max 0 z) al H).
  generalize (Zmax_spec 0 z). destr; omega.
  apply IHl; auto.
  generalize (align_le b al H).
  generalize (align_le (align b al + Z.max 0 z) al H).
  generalize (Zmax_spec 0 z). destr; omega.
Qed.

Lemma mbla_rew:
  forall sz n,
    mk_block_list_aux sz (S n) =
    let s := sz (Pos.of_nat (S n)) in
    (Pos.of_nat (S n), s) :: mk_block_list_aux sz n.
Proof.
  reflexivity.
Qed.

Lemma blocks_not_empty:
  forall b sz,
    forall n,
      (Pos.to_nat b <= n)%nat ->
      (mk_block_list_aux sz n) <> nil.
Proof.
  induction n; intros. xomega.
  rewrite mbla_rew; simpl. discriminate.
Qed.

Lemma size_mem_aux_permut:
  forall t t',
    Permutation t t' ->
    size_mem_aux t = size_mem_aux t'.
Proof.
  intros.
  unfold size_mem_aux.
  apply size_mem_al_permut; auto. omega.
Qed.

Lemma mbla_suppr_above:
  forall sz' sz b
         (sz_ext: forall b',
                    b <> b' ->
                    sz' b' = sz b')
         n
         (sup: (Pos.to_nat b > n)%nat),
    (mk_block_list_aux sz' n) =
    (mk_block_list_aux sz n).
Proof.
  induction n; simpl; auto.
  intro sup.
  assert (b <> Pos.of_nat (S (n))).
  {
    intro; subst. rewrite Nat2Pos.id in sup; omega.
  }
  rewrite ! mbla_rew.
  rewrite IHn by omega.
  rewrite sz_ext by auto.
  reflexivity.
Qed.

Lemma mbla_suppr_below:
  forall sz' sz b
         (sz_ext: forall b',
                    b <> b' ->
                    sz' b' = sz b')
         n
         (inf: (Pos.to_nat b <= n)%nat),
    Permutation ((b,sz b)::(mk_block_list_aux sz' n))
                ((b,sz' b)::(mk_block_list_aux sz n)).
Proof.
  induction n; simpl; auto.
  xomega.
  intros.
  apply le_lt_or_eq in inf.
  destruct inf as [inf|eq].
  - rewrite ! mbla_rew. simpl.
    assert (Pos.of_nat (S n) <> b).
    { intro; subst. rewrite Nat2Pos.id in inf; omega. }
    rewrite sz_ext by auto.
    repeat rewrite (perm_swap (Pos.of_nat _,_)).
    apply perm_skip.
    apply IHn. omega.
  - clear IHn.
    assert (b = Pos.of_nat (S n)).
    { rewrite <- eq. rewrite Pos2Nat.id. auto. }
    rewrite ! mbla_rew.
    rewrite <- H.
    rewrite (mbla_suppr_above sz' sz b); auto.
    apply perm_swap. omega.
Qed.

Lemma size_mem_al_last:
  forall szb l b o,
    size_mem_al 8 (l ++ (b, szb) :: nil) (align o 8) =
    size_mem_al 8 l (align o 8) +
    align (Z.max 0 (szb)) 8.
Proof.
  induction l; unfold size_mem_aux; simpl; intros.
  - repeat rewrite <- ! align_distr. rewrite align_align. auto. omega.
  - destruct a. rewrite IHl. auto.
Qed.

Lemma size_mem_aux_last:
  forall szb l b,
    size_mem_aux (l ++ (b, szb) :: nil) =
    size_mem_aux l +
    align (Z.max 0 (szb)) 8.
Proof.
  unfold size_mem_aux; intros.
  change 8 with (align 8 8) at 2 4.
  rewrite size_mem_al_last. auto.
Qed.

Lemma size_mem_aux_first:
  forall szb l b,
    size_mem_aux ((b, szb) :: l) =
    size_mem_aux l + align (Z.max 0 (szb)) 8.
Proof.
  intros.
  rewrite <- (size_mem_aux_last _ _ b).
  apply size_mem_aux_permut.
  rewrite Permutation_rev.
  simpl.
  apply Permutation_app; auto.
  rewrite Permutation_rev.
  rewrite rev_involutive; auto.
Qed.

Lemma size_mem_free_eq:
  forall sz' sz n b
         (sz_ext: forall b',
                    b <> b' ->
                    sz' b' = sz b'),
    size_mem_aux (mk_block_list_aux sz n) =
    size_mem_aux (mk_block_list_aux sz' n)
    + if le_dec (Pos.to_nat b) n
      then align (Z.max 0 (sz b)) 8 - align (Z.max 0 (sz' b)) 8
      else 0.
Proof.
  intros.
  destruct (le_dec (Pos.to_nat b) n).
  - specialize (mbla_suppr_below sz' sz b sz_ext n l). simpl in *.
    intros H.
    apply Permutation_sym in H; auto.
    apply size_mem_aux_permut in H.
    rewrite ! size_mem_aux_first in H.
    omega.
  - rewrite (mbla_suppr_above sz' sz b); auto; omega.
Qed.

Lemma size_mem_free_eq':
  forall sz' sz n b
         (sz_ext: forall b',
                    b <> b' ->
                    sz' b' = sz b')
         (new_sz: sz' b = 0),
    size_mem_aux (mk_block_list_aux sz n) =
    size_mem_aux (mk_block_list_aux sz' n)
    + if le_dec (Pos.to_nat b) n
      then align (Z.max 0 (sz b)) 8
      else 0.
Proof.
  intros.
  erewrite size_mem_free_eq; eauto.
  rewrite new_sz.
  rewrite Z.max_id.
  change (align 0 8) with 0.
  rewrite Z.sub_0_r; auto.
Qed.

Lemma Zle_add:
  forall a b,
    0 <= b ->
    a <= a + b.
Proof.
  intros; omega.
Qed.

Lemma allocs_blocks_free':
  forall sz' sz n b
         (sz_ext: forall b',
                    b <> b' ->
                    sz' b' = sz b')
         (new_sz: sz' b = 0),
    alloc_blocks (mk_block_list_aux sz n) <> None ->
    alloc_blocks (mk_block_list_aux sz' n) <> None.
Proof.
  intros sz' sz n b sz_ext new_sz.
  unfold alloc_blocks.
  destr.
  revert H; destr.
  repeat (revert H0; destr).
  apply alloc_size_mem_aux in Heqp.
  apply alloc_size_mem_aux in Heqp0.
  cut (z1 <= z). omega.
  subst.
  rewrite (size_mem_free_eq' sz' sz n b); eauto.
  destr; try omega.
  apply Zle_add.
  generalize (align_le (Z.max 0 (sz b)) 8)
             (Zmax_bound_l 0 0 (sz b)); omega.
Qed.

Lemma allocs_blocks_free:
  forall sz' sz n b
         (sz_ext: forall b',
                    b <> b' ->
                    sz' b' = sz b')
         (new_sz_msk: (sz' b = sz b) \/
                      ( sz' b = 0)),
    alloc_blocks (mk_block_list_aux sz n) <> None ->
    alloc_blocks (mk_block_list_aux sz' n) <> None.
Proof.
  intros.
  destruct new_sz_msk as [A|A].
  - rewrite <- mk_block_list_aux_ext with (sz:=sz); auto.
    intros; destruct (peq i b); subst; auto.
    rewrite sz_ext; auto.
  - eapply allocs_blocks_free'; eauto.
Qed.

Lemma alloc_mem_al_pos:
  forall l al s m s' m',
    alloc_mem_al al l (s,m) = (s',m') ->
    forall b,
      ~ In b (map fst l) ->
      m' b = m b.
Proof.
  induction l; simpl; intros.
  inv H; auto.
  des a.
  apply IHl with (b:=b) in H; auto.
  rewrite H. destr.
Qed.

Lemma mbla_not_above:
  forall sz n b,
    (n < Pos.to_nat b)%nat ->
    ~ In b (map fst (mk_block_list_aux sz n)).
Proof.
  induction n. simpl; intros; auto.
  intros.
  rewrite mbla_rew. simpl.
  destr.
  subst. rewrite Nat2Pos.id in H; omega.
  apply IHn in H1; auto. omega.
Qed.

Lemma compat_alloc_range_al:
  forall sz n b
         (inf: (Pos.to_nat b <= n)%nat)
         size0 m0 size m
         (size0pos: 0 <= size0)
         (ALLOC : alloc_mem_al 8 (mk_block_list_aux sz n) (size0,m0) =
                  (size, m)),
    size0 <= m b /\ m b + Z.max 0 (sz b) <= size.
Proof.
  induction n.
  - simpl; intros. xomega.
  - intros. rewrite mbla_rew in ALLOC. simpl in ALLOC.
    apply le_lt_or_eq in inf.
    destruct inf as [inf|eq].
    + specialize (IHn b).
      trim IHn. omega.
      eapply IHn in ALLOC; eauto.
      destruct ALLOC; split; auto.
      * refine (Zle_trans _ _ _ _ H).
        rewrite <- align_distr.
        refine (Zle_trans _ _ _ (align_le _ 8 _) _); try omega.
        apply Zle_add.
        refine (Zle_trans _ _ _ (Zmax_bound_l 0 _ _ _) (align_le _ _ _)); try omega.
      * rewrite <- align_distr.
        transitivity size0; auto.
        refine (Zle_trans _ _ _ (align_le size0 8 _) _); try omega.
        apply Zle_add.
        refine (Zle_trans _ _ _ (Zmax_bound_l 0 _ _ _) (align_le _ _ _)); try omega.
    + rewrite <- eq in ALLOC.
      rewrite Pos2Nat.id in ALLOC.
      generalize (alloc_mem_al_pos _ _ _ _ _ _ ALLOC b).
      intro A; trim A.
      apply mbla_not_above. omega.
      rewrite peq_true in A.
      rewrite A.
      apply alloc_size_mem_al in ALLOC. subst.
      split.
      * apply align_le; omega.
      * rewrite <- align_distr.
        refine (Zle_trans _ _ _ _ (size_mem_al_pos _ _ _ _ _)); try omega.
        apply Z.add_le_mono; try omega.
        apply align_le; omega.
        generalize (align_le size0 8)
                   (align_le (Z.max 0 (sz b)) 8)
                   (Zmax_bound_l 0 0 (sz b)). omega.
Qed.

Lemma compat_alloc_range_al':
  forall l (nr: list_norepet (map fst l))
         size0 m0 size m
         (size0pos: 0 <= size0)
         (ALLOC : alloc_mem_al 8 l (size0,m0) = (size, m))
         b szb
         (inf: In (b,szb) l),
    size0 <= m b /\ m b + Z.max 0 szb <= size.
Proof.
  induction l; simpl; intros. exfalso; auto.
  destruct a.
  destruct inf as [inf|inf].
  - inv inf.
    simpl in ALLOC.
    generalize ALLOC; apply alloc_mem_al_pos with (b:=b) in ALLOC.
    rewrite peq_true in ALLOC.
    rewrite ALLOC. intro.
    split.
    * apply align_le; omega.
    * apply alloc_size_mem_al in ALLOC0.
      subst.
      refine (Zle_trans _ _ _ (align_le _ _ (two_power_nat_pos 3)) _).
      apply size_mem_al_pos.
      omega.
      refine (Zle_trans _ _ _ _ (align_le _ _ (two_power_nat_pos 3))).
      transitivity (align size0 8).
      apply (Zle_trans _ _ _ size0pos). apply align_le; omega.
      rewrite Zmax_spec; destr; omega.
    * inv nr; auto.
  - eapply IHl in ALLOC; eauto.
    + destruct ALLOC; split; auto.
      etransitivity; eauto.
      refine (Zle_trans _ _ _ (align_le _ 8 _) _); try omega.
      refine (Zle_trans _ _ _ (align_le _ 8 _) _); try omega.
      apply align_add. omega.
      split.
      refine (Zle_trans _ _ _ size0pos (align_le _ 8 _)).
      omega. rewrite Zmax_spec; destr; omega.
    + inv nr; auto.
    + transitivity size0; auto.
      refine (Zle_trans _ _ _ (align_le _ 8 _) _). omega.
      refine (Zle_trans _ _ _ (align_le _ 8 _) _). omega.
      apply align_add. omega.
      split.
      refine (Zle_trans _ _ _ size0pos (align_le _ 8 _)). omega.
      rewrite Zmax_spec; destr; omega.
Qed.

Lemma compat_alloc_aligned_al:
  forall l size0 m0 size m b
         (i: In b (map fst l))
         (ALLOC : alloc_mem_al (two_power_nat 3) l (size0,m0) =
                  (size, m)),
    Z.divide 8 (m b).
Proof.
  induction l; simpl; intros.
  exfalso; auto.
  destruct (in_dec peq b (map fst l)).
  destruct a.
  - apply IHl with (b:=b) in ALLOC; auto.
  - des a. subst.
    apply alloc_mem_al_pos with (b:=b) in ALLOC; auto.
    rewrite ALLOC.
    rewrite peq_true.
    apply align_divides. apply two_power_nat_pos.
Qed.

Lemma compat_alloc_range:
  forall sz n size m
         (ALLOC: alloc_mem_aux (mk_block_list_aux sz n) = (size,m)),
  forall b,
    (Pos.to_nat b <= n)%nat ->
    8 <= m b /\ m b + Z.max 0 (sz b) <= size.
Proof.
  unfold alloc_mem_aux; simpl.
  intros.
  eapply compat_alloc_range_al; eauto.
  omega.
Qed.

Lemma blocks_not_empty_in:
  forall b sz,
    forall n,
      (Pos.to_nat b <= n)%nat ->
      In (b,sz b) (mk_block_list_aux sz n).
Proof.
  induction n; intros. xomega.
  apply le_lt_or_eq in H; destruct H.
  - rewrite mbla_rew. simpl.
    right. apply IHn; omega.
  - clear IHn.
    rewrite mbla_rew; simpl.
    rewrite <- H.
    rewrite Pos2Nat.id. auto.
Qed.

Lemma compat_alloc_aligned:
  forall sz n size m
         (ALLOC: alloc_mem_aux (mk_block_list_aux sz n) = (size,m)),
  forall b,
    (Pos.to_nat b <= n)%nat ->
    Z.divide 8 (m b).
Proof.
  intros.
  eapply compat_alloc_aligned_al; eauto.
  generalize (blocks_not_empty_in b sz _ H).
  intro MBL.
  apply in_map with (f:=fst) in MBL; simpl in *; auto.
Qed.

Lemma compat_alloc_overlap_al:
  forall sz l b b'
         s0 m0 s m
         (s0sup: 0 <= s0)
         (ALLOC: alloc_mem_al 8 l (s0, m0) = (s, m))
         (nr: list_norepet (map fst l))
         (SZb': sz b' > 0)
         (diff: b <> b')
         (i1: In (b', sz b') l)
         (i0: In (b, sz b) l),
    ~ m b <= m b' < m b + Z.max 0 (sz b).
Proof.
  induction l; simpl; intros; auto.
  destruct a.
  inv nr.
  des i0.
  - inv e.
    generalize (alloc_mem_al_pos _ _ _ _ _ _ ALLOC _ H1); auto.
    rewrite peq_true. intro A; rewrite A in H0, H3.
    apply (compat_alloc_range_al') with (b:=b') (szb:=sz b') in ALLOC; eauto.
    + destruct ALLOC.
      assert (m b' < m b').
      eapply Z.lt_le_trans; eauto.
      etransitivity; eauto.
      apply align_le; omega. omega.
    + refine (Z.le_trans _ _ _ _ (align_le _ 8 _)); try omega.
      transitivity (align s0 8).
      refine (Z.le_trans _ _ _ s0sup (align_le _ 8 _)); try omega.
      rewrite Zmax_spec; destr; omega.
  - inv H.
    generalize (alloc_mem_al_pos _ _ _ _ _ _ ALLOC _ H1); auto.
    rewrite peq_true. intro A; rewrite A in H0 , H3.
    apply (compat_alloc_range_al') with (b:=b) (szb:=sz b) in ALLOC; eauto.
    * destruct ALLOC.
      assert (m b < m b); try omega.
      eapply Z.lt_le_trans; eauto.
      eapply Z.le_lt_trans; eauto.
      rewrite <- align_distr.
      assert (align 1 8 <= align (Z.max 0 (sz b')) 8).
      apply align_add; auto. omega.
      rewrite Zmax_spec; destr; omega.
      change (align 1 8) with 8 in H5. omega.
    * refine (Z.le_trans _ _ _ _ (align_le _ 8 _)); try omega.
      transitivity (align s0 8).
      refine (Z.le_trans _ _ _ s0sup (align_le _ 8 _)); try omega.
      rewrite Zmax_spec; destr; omega.
  - apply IHl with (b:=b) (b':=b') in ALLOC; eauto.
    refine (Z.le_trans _ _ _ _ (align_le _ 8 _)); try omega.
    transitivity (align s0 8).
    refine (Z.le_trans _ _ _ s0sup (align_le _ 8 _)); try omega.
    rewrite Zmax_spec; destr; omega.
Qed.

Opaque mk_block_list_aux.

Lemma mbla_norepet:
  forall sz n,
    list_norepet (map fst (mk_block_list_aux sz n)).
Proof.
  induction n; simpl; intros.
  constructor.
  rewrite mbla_rew; simpl.
  destr.
  constructor; auto.
  eapply mbla_not_above; eauto.
  rewrite Nat2Pos.id; auto.
Qed.

Lemma compat_alloc_no_overlap:
  forall sz n size m
         (ALLOC: alloc_mem_aux (mk_block_list_aux sz n) = (size,m)),
  forall b b',
    b <> b' ->
    (Pos.to_nat b <= n)%nat ->
    (Pos.to_nat b' <= n)%nat ->
    sz b' > 0 ->
    ~ (m b <= m b' < m b + Z.max 0 (sz b)).
Proof.
  unfold alloc_mem_aux; simpl.
  intros.
  eapply compat_alloc_overlap_al; eauto.
  omega.
  apply mbla_norepet.
  apply blocks_not_empty_in; auto; omega.
  apply blocks_not_empty_in; auto; omega.
Qed.

Lemma compat_alloc:
  forall (sz: block -> Z*Z) sz' msk
         (MSKeq: forall b, msk b = Int.not (Int.repr (two_power_nat (alignment_of_size (sz' b)) - 1)))
         (lo0: forall b, fst (sz b) <= 0)
         (SZeq: forall b, let (lo,hi) := sz b in sz' b = hi - lo)
         n al
         (SZabove:
            forall b, (Pos.to_nat b > n)%nat -> sz b = (0, 0))
         (ALLOC: alloc_blocks (mk_block_list_aux sz' n) = Some al),
    compat al sz msk.
Proof.
  intros.
  constructor.
  - intros.
    clear MSKeq.
    unfold alloc_blocks in ALLOC.
    destruct (alloc_mem_aux (mk_block_list_aux sz' n)) eqn:?.
    destruct (le_dec (Pos.to_nat b) n).
    + generalize (compat_alloc_range _ _ _ _ Heqp
                                     b l).
      unfold in_bound in H.
      specialize (SZeq b).
      destruct (sz b) eqn:?.
      simpl in *.
      rewrite SZeq.
      intro A.
      destruct (zlt z Int.max_unsigned); try congruence.
      inv ALLOC.
      unfold Int.add.
      rewrite (Int.unsigned_repr (z0 b)).
      rewrite Int.unsigned_repr.
      split.
      * apply Z.lt_le_trans with (m:=z0 b); auto.
        intuition omega.
        generalize (Int.unsigned_range o); omega.
      * apply Z.le_lt_trans with (m:=z); auto.
        destruct A; etransitivity; eauto.
        apply Z.add_le_mono; try omega.
        rewrite Zmax_spec. destr_no_dep; try omega.
        specialize (lo0 b). rewrite Heqp0 in lo0; simpl in lo0. omega.
      * split.
        generalize (Int.unsigned_range o); omega.
        transitivity z; auto. destruct A; etransitivity; eauto.
        apply Z.add_le_mono_l.
        rewrite Zmax_spec. destr_no_dep; try omega.
        specialize (lo0 b). rewrite Heqp0 in lo0. simpl in lo0. omega.
        omega.
      * destruct A; split; try omega.
        transitivity z; auto.
        etransitivity ; eauto.
        rewrite Zmax_spec; destr; omega. omega.
    + destruct (eq_nat_dec n O).
      * subst. rewrite SZabove in H.
        unfold in_bound in H; simpl in H; omega. omega.
      * rewrite SZabove in H.
        unfold in_bound in H; simpl in H; omega.
        omega.
  - intros.
    unfold alloc_blocks in ALLOC.
    repeat (revert ALLOC; destr).
    generalize (compat_alloc_no_overlap
                  _ _ _ _ Heqp _ _ H
               ).
    assert (b' <> b) by auto.
    generalize (compat_alloc_no_overlap
                  _ _ _ _ Heqp _ _ H3
               ).
    destruct (le_dec (Pos.to_nat b) n).
    destruct (le_dec (Pos.to_nat b') n).
    + intros B A; specialize (A l0 l1);
      specialize (B l1 l0).
      generalize (SZeq b) (SZeq b').
      generalize (compat_alloc_range _ _ _ _ Heqp
                                     b l0 ).
      generalize (compat_alloc_range _ _ _ _ Heqp
                                     b' l1).
      destruct (sz b) eqn:?; destruct (sz b') eqn:?.
      unfold in_bound in *. simpl in *.
      intros C D E F.
      trim A. clear - F H1. omega.
      trim B. clear - E H0. omega.
      inv ALLOC.
      unfold Int.add in H2.
      generalize (lo0 b) (lo0 b').
      rewrite Heqp0, Heqp1. simpl; intros; subst.
      rewrite (Int.unsigned_repr (z0 b)) in H2.
      rewrite (Int.unsigned_repr (z0 b')) in H2.
      rewrite Int.unsigned_repr in H2.
      rewrite Int.unsigned_repr in H2.
      destruct (zlt (Int.unsigned o) (Int.unsigned o')).
      * apply B.
        assert (z0 b = z0 b' + Int.unsigned o' - Int.unsigned o) by omega.
        rewrite H6.
        split. omega.
        rewrite F. rewrite Zmax_spec. destr; try omega.
        cut (Int.unsigned o' < z4 - z3).
        cut (Int.unsigned o >= 0); try omega.
        generalize (Int.unsigned_range o); omega.
        omega.
      * apply A.
        assert (z0 b' = z0 b + Int.unsigned o - Int.unsigned o') by omega.
        rewrite H6.
        split. omega.
        rewrite E. rewrite Zmax_spec. destr; try omega.
        cut (Int.unsigned o < z2 - z1).
        cut (Int.unsigned o' >= 0); try omega.
        generalize (Int.unsigned_range o'); omega.
        omega.
      * generalize (Int.unsigned_range_2 o').
        destruct C. intro.
        split. omega.
        transitivity z; auto.
        etransitivity; eauto. rewrite F.
        rewrite Zmax_spec; destr; try omega. omega.
      * generalize (Int.unsigned_range_2 o).
        destruct D. intro.
        split. omega.
        transitivity z; auto.
        etransitivity; eauto. rewrite E.
        rewrite Zmax_spec; destr; omega. omega.
      * split. omega.
        transitivity z; auto.
        destruct C; etransitivity; eauto.
        rewrite Zmax_spec; destr; omega. omega.
      * split. omega.
        transitivity z; auto.
        destruct D; etransitivity; eauto.
        rewrite Zmax_spec; destr; omega. omega.
    + rewrite SZabove in H1. unfold in_bound in H1; simpl in H1. omega. omega.
    + rewrite SZabove in H0.
      unfold in_bound in H0; simpl in H0; omega.
      omega.
  - intros.
    destruct (le_dec (Pos.to_nat b) n).
    * unfold alloc_blocks in ALLOC.
        Opaque two_power_nat.
        repeat (revert ALLOC; destr).
        generalize (compat_alloc_aligned _ _ _ _ Heqp _ l ).
        intros [x A].
        inv ALLOC.
        rewrite A.
        rewrite MSKeq. simpl.
        {
          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 3 (x*8) i).
          assert (i < 3).
          + clear - l1.
            revert l1; unfold alignment_of_size; repeat (destruct zlt; simpl; try (intros; omega)).
          + destr; try omega.
            rewrite <- H2; auto.
            rewrite Z.mod_mul; auto.
            rewrite Int.Ztestbit_0. reflexivity. change (two_power_pos 3) with 8; omega.
            omega.
        }
      * { rewrite MSKeq.
          generalize (SZeq b).
          rewrite SZabove.
          intro A; rewrite A.
          unfold alignment_of_size; simpl.
          change (two_power_nat 0 - 1) with 0. simpl.
          replace (Int.not (Int.repr 0)) with Int.mone.
          rewrite Int.and_mone. auto. setoid_rewrite Int.not_zero. auto.
          omega.
        }
Qed.

Lemma mk_block_list_aux_ext':
  forall (m : nat) (sz sz' : positive -> Z),
    (forall i : positive, Plt i (Pos.of_nat m) -> sz i = sz' i) ->
    mk_block_list_aux sz (pred m) =
    mk_block_list_aux sz' (pred m).
Proof.
  intros.
  des m. des n.
  apply mk_block_list_aux_ext.
  intros. apply H; auto.
  rewrite Nat2Pos.inj_succ; try omega.
  xomega.
Qed.

Generated by coq2html