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).
Require Import Align Psatz PpsimplZ.
This module defines a greedy allocation algorithm that ensures that a
concrete memory exists for a given abstract memory.
Properties of the align function.
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.
Require Import Compat.
Definition alignment_of_size (
sz:
Z) :
nat :=
(
if zlt sz 2
then O
else if zlt sz 3
then 1
else if zle sz 4
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.
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.
Lemma size_mem_al_pos:
forall l b al,
al > 0 -> 0 <=
b ->
b <=
size_mem_al al l b.
Proof.
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.
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.
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 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.
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.
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 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.
Lemma size_mem_al_last:
forall al (
AlPos:
al > 0)
szb l b o,
size_mem_al al (
l ++ (
b,
szb) ::
nil) (
align o al) =
size_mem_al al l (
align o al) +
align (
Z.max 0 (
szb))
al.
Proof.
induction l;
simpl;
intros.
-
repeat rewrite <- !
align_distr.
rewrite align_align.
auto.
auto.
auto.
-
destruct a.
rewrite IHl.
auto.
Qed.
Lemma Zle_add:
forall a b,
0 <=
b ->
a <=
a +
b.
Proof.
intros; omega.
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 al (
AlPos:
al > 0)
sz l
(
lSpec:
forall b z,
In (
b,
z)
l ->
z =
sz b)
m0 size m
size0
(
ALLOC :
alloc_mem_al al l (
size0,
m0) =
(
size,
m))
(
size0pos: 0 <=
size0)
b
(
IN:
In b (
map fst l)),
size0 <=
m b /\
m b +
Z.max 0 (
sz b) <=
size.
Proof.
Lemma compat_alloc_range_al':
forall al (
AlPos:
al > 0)
l (
nr:
list_norepet (
map fst l))
size0 m0 size m
(
size0pos: 0 <=
size0)
(
ALLOC :
alloc_mem_al al l (
size0,
m0) = (
size,
m))
b szb
(
inf:
In (
b,
szb)
l),
size0 <=
m b /\
m b +
Z.max 0
szb <=
size.
Proof.
Lemma compat_alloc_aligned_al:
forall al (
AlPos:
al > 0)
l size0 m0 size m b
(
i:
In b (
map fst l))
(
ALLOC :
alloc_mem_al al l (
size0,
m0) =
(
size,
m)),
Z.divide al (
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.
auto.
Qed.
Lemma mbla_in:
forall sz n (
b0 :
block) (
z :
Z),
In (
b0,
z) (
mk_block_list_aux sz n) ->
z =
sz b0.
Proof.
induction n; simpl; intros.
contradiction.
destruct H. inv H. auto.
apply IHn. auto.
Qed.
Definition f_perm f (
sz':
positive ->
Z)
n:=
forall l
(
all_in:
forall b, (
Pos.to_nat b <=
n)%
nat ->
In (
b,
sz'
b)
l)
(
lnr:
list_norepet l),
Permutation l (
f l).
Lemma mbla_below_in:
forall sz n b,
(
Pos.to_nat b <=
n)%
nat ->
In b (
map fst (
mk_block_list_aux sz n)).
Proof.
induction n;
simpl;
intros.
xomega.
apply le_lt_or_eq in H.
destruct H as [
inf|
eq]; [
right|
left];
auto.
apply IHn.
omega.
rewrite <-
eq.
apply Pos2Nat.id.
Qed.
Lemma mbla_below_in':
forall sz n b,
(
Pos.to_nat b <=
n)%
nat ->
In (
b,
sz b) (
mk_block_list_aux sz n).
Proof.
Opaque mk_block_list_aux.
Lemma mbla_norepet:
forall sz n,
list_norepet (
map fst (
mk_block_list_aux sz n)).
Proof.
Lemma mbla_norepet':
forall sz n,
list_norepet (
mk_block_list_aux sz n).
Proof.
Lemma fperm_mbla:
forall f sz n (
fperm:
f_perm f sz n),
Permutation (
mk_block_list_aux sz n) (
f (
mk_block_list_aux sz n)).
Proof.
intros.
apply fperm.
apply mbla_below_in'.
apply mbla_norepet'.
Qed.
Lemma f_mbla_in:
forall f sz n (
fperm:
f_perm f sz n) (
b0 :
block) (
z :
Z),
In (
b0,
z) (
f (
mk_block_list_aux sz n)) ->
z =
sz b0.
Proof.
Lemma compat_alloc_overlap_al:
forall al (
AlPos:
al > 0)
sz l b b'
s0 m0 s m
(
s0sup: 0 <=
s0)
(
ALLOC:
alloc_mem_al al 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.
Section MaxAlign.
Variable MA:
nat.
Hypothesis MA_bound: (3 <=
MA)%
nat.
Let tpMA :=
two_power_nat MA.
Let tpMA_pos :=
two_power_nat_pos MA.
Definition size_mem_aux (
t :
list (
block *
Z)) :
Z :=
size_mem_al tpMA t tpMA.
Definition alloc_mem_aux (
t :
list (
block *
Z)) :
Z * (
block ->
Z) :=
alloc_mem_al tpMA t (
tpMA, (
fun _ => 0)).
Lemma alloc_size_mem_aux:
forall bl z m,
alloc_mem_aux bl = (
z,
m) ->
size_mem_aux bl =
z.
Proof.
Lemma size_mem_aux_alloc :
forall t p,
size_mem_aux t <=
size_mem_aux (
p::
t).
Proof.
Lemma size_mem_aux_permut:
forall t t',
Permutation t t' ->
size_mem_aux t =
size_mem_aux t'.
Proof.
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))
tpMA.
Proof.
Lemma size_mem_aux_first:
forall szb l b,
size_mem_aux ((
b,
szb) ::
l) =
size_mem_aux l +
align (
Z.max 0 (
szb))
tpMA.
Proof.
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))
tpMA -
align (
Z.max 0 (
sz'
b))
tpMA
else 0.
Proof.
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))
tpMA
else 0.
Proof.
Lemma compat_alloc_range:
forall sz n size m f (
fperm:
f_perm f sz n)
(
ALLOC:
alloc_mem_aux (
f (
mk_block_list_aux sz n)) = (
size,
m)),
forall b,
(
Pos.to_nat b <=
n)%
nat ->
tpMA <=
m b /\
m b +
Z.max 0 (
sz b) <=
size.
Proof.
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_f:
forall sz n size m f (
fperm:
f_perm f sz n)
(
ALLOC:
alloc_mem_aux (
f (
mk_block_list_aux sz n)) = (
size,
m)),
forall b,
(
Pos.to_nat b <=
n)%
nat ->
Z.divide tpMA (
m b).
Proof.
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 tpMA (
m b).
Proof.
Opaque mk_block_list_aux.
Lemma compat_alloc_no_overlap:
forall sz l (
lSpec:
forall b z,
In (
b,
z)
l ->
z =
sz b)
(
lnr:
list_norepet (
map fst l))
size m
(
ALLOC:
alloc_mem_aux l = (
size,
m)),
forall b b',
b <>
b' ->
In b (
map fst l) ->
In b' (
map fst l) ->
sz b' > 0 ->
~ (
m b <=
m b' <
m b +
Z.max 0 (
sz b)).
Proof.
unfold alloc_mem_aux;
simpl.
intros.
rewrite in_map_iff in H0,
H1.
destruct H0 as ((
b0 &
z0) &
A &
B).
destruct H1 as ((
b1 &
z1) &
C &
D).
simpl in *;
subst.
generalize (
lSpec _ _ D);
intro;
subst;
auto.
generalize (
lSpec _ _ B);
intro;
subst;
auto.
eapply compat_alloc_overlap_al. 3:
eauto.
auto.
unfold tpMA;
lia.
auto.
auto.
auto.
auto.
auto.
Qed.
Lemma compat_alloc_no_overlap_mbla:
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.
Lemma perm_in:
forall A l l' (
x:
A),
Permutation l l' ->
(
In x l <->
In x l').
Proof.
Lemma f_mbla_norepet:
forall f sz n (
fperm:
f_perm f sz n),
list_norepet (
map fst (
f (
mk_block_list_aux sz n))).
Proof.
Lemma compat_alloc_no_overlap_f_mbla:
forall sz n size m
f (
fperm:
f_perm f sz n)
(
ALLOC:
alloc_mem_aux (
f (
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.
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.
Inductive appears_before {
A:
Type} :
A ->
A ->
list A ->
Prop :=
|
ab_intro:
forall a b l l1 l2 l3,
l =
l1 ++ (
a ::
l2) ++
b ::
l3 ->
~
In b l1 ->
appears_before a b l.
Lemma ab_rev:
forall A l (
a b:
A) (
Aeq:
forall a b :
A , {
a =
b} + {
a <>
b }),
list_norepet l ->
appears_before a b l ->
appears_before b a (
rev l).
Proof.
induction l;
simpl;
intros.
-
inv H0.
contradict H1;
clear.
apply app_cons_not_nil.
-
inv H.
inv H0.
generalize (
f_equal (@
rev A)
H).
simpl.
intro B;
rewrite B.
rewrite !
rev_app_distr.
simpl.
rewrite !
rev_app_distr.
simpl.
rewrite <- !
app_assoc.
eapply ab_intro.
instantiate (1:=
rev l1).
instantiate (1:=
rev l2).
instantiate (1:=
rev l3).
simpl.
auto.
des (
Aeq a0 a).
des l1.
inv H.
simpl in *.
apply H3.
rewrite in_app.
right.
simpl;
auto.
right.
apply in_rev;
auto.
inv H.
simpl in *.
apply H3.
rewrite in_app.
right.
simpl;
auto.
des l1.
inv H.
clear -
H4 H0.
rewrite !
list_norepet_app in H4.
intuition.
inv H2.
clear -
H0 H5.
apply H5.
apply in_app.
simpl.
apply in_rev in H0;
auto.
Qed.
Lemma ab_in2:
forall A l (
a b:
A)
(
AB :
appears_before a b (
a ::
l)),
In b l.
Proof.
intros.
inv AB.
des l1;
inv H;
repeat (
rewrite in_app;
simpl;
auto).
Qed.
Lemma ab_inl:
forall (
b b':
block)
l
(
APB :
appears_before b b' (
map fst l)),
exists szb':
Z,
In (
b',
szb')
l.
Proof.
intros.
inv APB.
assert (
In b' (
map fst l)).
rewrite H.
repeat (
rewrite in_app;
simpl;
auto).
rewrite in_map_iff in H1.
destruct H1 as ((
bb &
zz) &
A &
B).
simpl in *;
subst.
eexists;
eauto.
Qed.
Lemma ab_first_in:
forall (
b b':
block)
l
(
APB :
appears_before b b' (
map fst l)),
exists szb:
Z,
In (
b,
szb)
l.
Proof.
intros.
inv APB.
assert (
In b (
map fst l)).
rewrite H.
repeat (
rewrite in_app;
simpl;
auto).
rewrite in_map_iff in H1.
destruct H1 as ((
bb &
zz) &
A &
B).
simpl in *;
subst.
eexists;
eauto.
Qed.
Lemma alloc_mem_al_order:
forall aa (
AlPos:
aa > 0)
l al sz z cur
(
AMA:
alloc_mem_al aa l (
z,
cur) = (
sz,
al))
(
Zpos: 0 <=
z)
(
lnr:
list_norepet (
map fst l))
b b'
(
AB:
appears_before b b' (
map fst l))
z z'
(
I1:
In (
b,
z)
l) (
I2:
In (
b',
z')
l)
(
Zpos:
z > 0) (
Zpos':
z' > 0),
al b <
al b' \/
b =
b'.
Proof.
induction l;
simpl;
intros.
contradiction.
destruct a.
simpl in *.
inv lnr.
destruct (
peq b b');
auto.
left.
destruct (
peq b b0).
-
subst.
destruct I1.
inv H.
generalize (
alloc_mem_al_pos _ _ _ _ _ _ AMA _ H1).
rewrite peq_true.
intro A;
rewrite A.
assert (
In b' (
map fst l)).
eapply ab_in2.
eauto.
generalize H;
rewrite in_map_iff.
intros ((
b &
z1) &
B &
C).
simpl in *;
subst.
generalize (
fun pos =>
compat_alloc_range_al'
_ AlPos _ H2 _ _ _ _ pos AMA _ _ C).
intro D;
trim D.
generalize (
align_le z _ AlPos) (
Z.le_max_l 0
z0).
generalize (
align_le (
align z aa +
Z.max 0
z0)
aa).
omega.
destruct D.
rewrite <-
align_distr in H0.
apply Z.lt_le_trans with (
m:=
align z aa +
align (
Z.max 0
z0)
aa).
generalize (
Z.le_max_r 0
z0) (
align_le (
Z.max 0
z0)
aa).
omega.
auto.
auto.
apply (
in_map fst)
in H.
simpl in H;
congruence.
-
destruct I1.
inv H.
congruence.
exploit IHl.
eexact AMA.
generalize (
align_le z aa) (
Z.le_max_l 0
z1).
generalize (
align_le (
align z aa +
Z.max 0
z1)
_ AlPos).
omega.
auto.
inv AB.
des l1.
apply (
ab_intro _ _ _ l0 l2 l3).
inv H0.
rewrite H8;
simpl;
eauto.
auto.
eauto.
inv AB.
des l1.
inv H0.
eauto.
auto.
auto.
intros [
A|
A];
auto.
congruence.
Qed.
Lemma norepet_eq:
forall {
A B}
l,
list_norepet (
map fst l) ->
forall (
b:
A) (
z z':
B),
In (
b,
z)
l ->
In (
b,
z')
l ->
z =
z'.
Proof.
induction l;
simpl;
intros.
contradiction.
inv H.
destruct a;
simpl in *.
trim IHl.
auto.
destruct H0,
H1.
inv H.
inv H0;
auto.
inv H.
apply (
in_map fst)
in H0.
simpl in H0.
congruence.
inv H0.
apply (
in_map fst)
in H.
simpl in H.
congruence.
eauto.
Qed.
Lemma ab_dec:
forall A (
Aeq:
forall (
a b :
A), {
a=
b} + {
a <>
b}) (
l:
list A)
b b'
(
diff:
b <>
b')
(
IN1:
In b l)
(
IN2:
In b'
l),
appears_before b b'
l \/
appears_before b'
b l.
Proof.
induction l;
simpl;
intros;
auto.
contradiction.
destruct IN1 as [
IN1|
IN1],
IN2 as [
IN2|
IN2];
subst;
try congruence.
-
left.
destruct (
in_split _ _ IN2)
as (
l1 &
l2 &
EQ).
apply (
ab_intro _ _ _ nil l1 l2).
subst.
simpl.
auto.
simpl;
auto.
-
right.
destruct (
in_split _ _ IN1)
as (
l1 &
l2 &
EQ).
apply (
ab_intro _ _ _ nil l1 l2).
subst.
simpl.
auto.
simpl;
auto.
-
specialize (
IHl _ _ diff IN1 IN2).
destruct (
Aeq b a);
destruct (
Aeq b'
a);
subst;
try congruence.
+
left.
destruct (
in_split _ _ IN2)
as (
l1 &
l2 &
EQ).
apply (
ab_intro _ _ _ nil l1 l2);
subst;
simpl;
auto.
+
right.
destruct (
in_split _ _ IN1)
as (
l1 &
l2 &
EQ).
apply (
ab_intro _ _ _ nil l1 l2);
subst;
simpl;
auto.
+
destruct IHl as [
I|
I]; [
left|
right];
inversion I as [? ? ?
X Y Z];
subst;
apply (
ab_intro _ _ _ (
a::
X)
Y Z);
subst;
simpl;
auto;
intro G;
destruct G;
try congruence.
Qed.
Lemma list_norepet_rev:
forall A (
l:
list A),
list_norepet l ->
list_norepet (
rev l).
Proof.
Lemma mk_block_list_aux_eq:
forall lo hi b'
bs ,
mk_block_list_aux
(
fun b0 :
block =>
get_size
(
PMap.set b' (
Some (
lo,
hi))
bs)
b0)
(
pred (
Pos.to_nat (
Pos.succ b'))) =
(
b',
hi-
lo)::
mk_block_list_aux
(
fun b0 =>
get_size bs b0)
(
pred (
Pos.to_nat b')).
Proof.
Lemma size_mem_inf_add_larger:
forall m1 m2 (
p1 p2:
block) (
lo hi lo'
hi':
Z),
hi >= 0 ->
hi' >= 0 ->
hi >=
lo ->
hi' -
lo' >=
hi -
lo ->
size_mem_aux
(
mk_block_list_aux (
get_size m2)
(
pred (
Pos.to_nat p2))) <=
size_mem_aux
(
mk_block_list_aux (
get_size m1)
(
pred (
Pos.to_nat p1))) ->
size_mem_aux
(
mk_block_list_aux
(
get_size
(
PMap.set (
p2) (
Some (
lo,
hi)) (
m2)))
(
Pos.to_nat p2)) <=
size_mem_aux
(
mk_block_list_aux
(
get_size
(
PMap.set (
p1) (
Some (
lo',
hi')) (
m1)))
(
Pos.to_nat p1)).
Proof.
Lemma size_mem_inf_add':
forall m1 m2 (
p1 p2:
block) (
lo hi :
Z),
hi >= 0 ->
lo <=
hi ->
size_mem_aux
(
mk_block_list_aux (
get_size m2)
(
pred (
Pos.to_nat p2))) <=
size_mem_aux
(
mk_block_list_aux (
get_size m1)
(
pred (
Pos.to_nat p1))) ->
size_mem_aux
(
mk_block_list_aux
(
get_size
(
PMap.set (
p2) (
Some (
lo,
hi)) (
m2)))
(
Pos.to_nat (
p2))) <=
size_mem_aux
(
mk_block_list_aux
(
get_size
(
PMap.set (
p1) (
Some (
lo,
hi)) (
m1)))
(
Pos.to_nat (
p1))).
Proof.
Section AllocBlocks.
Variable memsize:
Z.
Hypothesis memsize_int:
memsize <=
Int.max_unsigned.
Definition alloc_blocks (
t:
list (
block*
Z)) :
option (
block ->
int) :=
let (
sz,
m) :=
alloc_mem_aux t in
if zlt sz memsize
then Some (
fun b =>
Int.repr (
m b))
else None.
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.
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 compat_alloc:
forall (
sz:
block ->
Z*
Z)
sz'
msk
(
MSKeq:
forall b,
exists n,
(
n <=
MA)%
nat /\
msk b =
Int.not (
Int.repr (
two_power_nat n - 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))
f
(
fperm:
f_perm f sz'
n)
(
ALLOC:
alloc_blocks (
f (
mk_block_list_aux sz'
n)) =
Some al),
compat memsize sz msk al.
Proof.
Lemma compat_alloc'':
forall (
sz:
block ->
Z*
Z)
sz'
msk
(
MSKeq:
forall b,
exists n,
(
n <=
MA)%
nat /\
msk b =
Int.not (
Int.repr (
two_power_nat n - 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))
f
(
fperm:
forall l,
Permutation l (
f l))
(
ALLOC:
alloc_blocks (
f (
mk_block_list_aux sz'
n)) =
Some al),
compat memsize sz msk al.
Proof.
Lemma compat_alloc':
forall (
sz:
block ->
Z*
Z)
sz'
msk
(
MSKeq:
forall b,
exists n,
(
n <=
MA)%
nat /\
msk b =
Int.not (
Int.repr (
two_power_nat n - 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 memsize sz msk al.
Proof.
intros.
eapply compat_alloc''
with (
f:=
id);
simpl;
eauto.
Qed.
Lemma alloc_blocks_order:
forall l al,
list_norepet (
map fst l) ->
alloc_blocks l =
Some al ->
forall b b'
z z',
appears_before b b' (
map fst l) ->
In (
b,
z)
l ->
In (
b',
z')
l ->
z > 0 ->
z' > 0 ->
Int.ltu (
al b) (
al b') =
true \/
b =
b'.
Proof.
End AllocBlocks.
End MaxAlign.