Require Import Memory.
Import Mem.
Require Import Coqlib AST Values Arith ZArith BinPos Psatz MemRel Permutation Tactics.
Program Definition reserve_boxes (
m:
mem) (
n:
nat) :
option mem :=
if zlt (
Z.of_nat (
nb_boxes_used_m m +
n))
nb_boxes_max
then Some (
mkmem (
mem_contents m)
(
mem_access m)
(
mem_blocksize m)
(
mem_mask m)
(
mem_blocktype m)
(
nextblock m)
(
nb_extra m +
n)
_ _ _ _ _ _ _ _ _)
else None.
Solve Obligations using (
destruct m;
simpl;
auto).
Next Obligation.
Program Definition release_boxes (
m:
mem) (
n:
nat) :
option mem :=
if le_dec n (
nb_extra m)
then Some (
mkmem (
mem_contents m)
(
mem_access m)
(
mem_blocksize m)
(
mem_mask m)
(
mem_blocktype m)
(
nextblock m)
(
nb_extra m -
n)
_ _ _ _ _ _ _ _ _)
else None.
Solve Obligations using (
destruct m;
simpl;
auto).
Next Obligation.
destruct m. simpl in *. lia.
Qed.
Lemma release_boxes_rel:
forall mr m1 m2 (
MR:
mem_rel mr m1 m2)
n m1'
(
REL:
release_boxes m1 n =
Some m1'),
exists m2',
release_boxes m2 n =
Some m2' /\
mem_rel mr m1'
m2'.
Proof.
intros.
unfold release_boxes in *.
destr_in REL.
inv REL.
inv MR.
destr.
eexists;
split;
eauto.
constructor;
simpl;
auto.
Qed.
Lemma reserve_boxes_rel:
forall mr m1 m2 (
MR:
mem_rel mr m1 m2)
n m1'
(
REL:
reserve_boxes m1 n =
Some m1'),
exists m2',
reserve_boxes m2 n =
Some m2' /\
mem_rel mr m1'
m2'.
Proof.
Lemma release_load:
forall m b chunk o n m'
(
MR:
release_boxes m n =
Some m'),
Mem.load chunk m b o =
Mem.load chunk m'
b o.
Proof.
Lemma release_bounds_of_block:
forall m b n m'
(
MR:
release_boxes m n =
Some m'),
Mem.bounds_of_block m b =
Mem.bounds_of_block m'
b.
Proof.
Lemma release_mask:
forall m b n m'
(
MR:
release_boxes m n =
Some m'),
Mem.mask m b =
Mem.mask m'
b.
Proof.
Lemma release_is_dynamic_block:
forall m b n m'
(
MR:
release_boxes m n =
Some m'),
Mem.is_dynamic_block m b =
Mem.is_dynamic_block m'
b.
Proof.
Lemma release_nextblock:
forall m n m'
(
MR:
release_boxes m n =
Some m'),
Mem.nextblock m =
Mem.nextblock m'.
Proof.
Lemma reserve_load:
forall m b chunk o n m'
(
MR:
reserve_boxes m n =
Some m'),
Mem.load chunk m b o =
Mem.load chunk m'
b o.
Proof.
Lemma reserve_bounds_of_block:
forall m b n m'
(
MR:
reserve_boxes m n =
Some m'),
Mem.bounds_of_block m b =
Mem.bounds_of_block m'
b.
Proof.
Lemma reserve_mask:
forall m b n m'
(
MR:
reserve_boxes m n =
Some m'),
Mem.mask m b =
Mem.mask m'
b.
Proof.
Lemma reserve_is_dynamic_block:
forall m b n m'
(
MR:
reserve_boxes m n =
Some m'),
Mem.is_dynamic_block m b =
Mem.is_dynamic_block m'
b.
Proof.
Lemma reserve_nextblock:
forall m n m'
(
MR:
reserve_boxes m n =
Some m'),
Mem.nextblock m =
Mem.nextblock m'.
Proof.
Lemma reserve_perm:
forall m n m'
b o k p
(
MR:
reserve_boxes m n =
Some m'),
Mem.perm m b o k p <->
Mem.perm m'
b o k p.
Proof.
Lemma release_perm:
forall m n m'
b o k p
(
MR:
release_boxes m n =
Some m'),
Mem.perm m b o k p <->
Mem.perm m'
b o k p.
Proof.
Lemma reserve_mem_contents:
forall m n m'
(
MR:
reserve_boxes m n =
Some m'),
Mem.mem_contents m =
Mem.mem_contents m'.
Proof.
Lemma reserve_nb_boxes_used_m:
forall m n m'
(
MR:
reserve_boxes m n =
Some m'),
(
Mem.nb_boxes_used_m m +
n =
Mem.nb_boxes_used_m m')%
nat.
Proof.
Open Scope Z_scope.
Lemma nb_boxes_set0:
forall l1 b sz l2,
(
Mem.nb_boxes_used (
l1 ++ (
b,
sz) ::
l2) =
Mem.nb_boxes_used (
l1 ++ (
b,
Z0) ::
l2) +
Mem.box_span sz)%
nat.
Proof.
Lemma nb_bozes_free_eq:
forall sz'
sz n b
(
sz_ext:
forall b',
b <>
b' ->
sz'
b' =
sz b')
(
EQ:
sz'
b = 0),
Mem.nb_boxes_used (
mk_block_list_aux sz n) =
(
Mem.nb_boxes_used (
mk_block_list_aux sz'
n)
+
if le_dec (
Pos.to_nat b)
n
then Mem.box_span (
sz b)
else 0)%
nat.
Proof.
Lemma unchecked_free_nb_boxes:
forall m b lo hi,
Mem.bounds_of_block m b = (
lo,
hi) ->
(
Mem.nb_boxes_used_m (
Mem.unchecked_free m b lo hi) +
Mem.box_span (
Z.max 0
hi)
=
Mem.nb_boxes_used_m m)%
nat.
Proof.
Lemma free_nb_boxes_used':
forall m b lo hi m',
Mem.free m b lo hi =
Some m' ->
(
Mem.nb_boxes_used_m m' +
Mem.box_span (
hi -
lo))%
nat =
Mem.nb_boxes_used_m m.
Proof.
Definition size_list_blocks (
bl :
list Z) :
nat :=
fold_left Peano.plus (
map Mem.box_span bl)
O.
Definition size_of_block (
blh:
block *
Z *
Z) :=
let '(
b,
lo,
hi) :=
blh in
(
hi -
lo)%
Z.
Definition size_list l :=
size_list_blocks (
map size_of_block l).
Lemma free_list_nb_boxes_used:
forall bl m m',
Mem.free_list m bl =
Some m' ->
(
Mem.nb_boxes_used_m m' +
size_list bl =
Mem.nb_boxes_used_m m)%
nat.
Proof.
Lemma nb_boxes_release:
forall m n m' (
REL:
release_boxes m n =
Some m'),
Mem.nb_boxes_used_m m = (
Mem.nb_boxes_used_m m' +
n)%
nat.
Proof.
Lemma release_nb_boxes_used:
forall m n m' (
MR:
release_boxes m n =
Some m'),
(
Mem.nb_boxes_used_m m =
Mem.nb_boxes_used_m m' +
n)%
nat.
Proof.
Lemma release_boxes_mk_block_list:
forall m n m' (
REL:
release_boxes m n =
Some m'),
Mem.mk_block_list m =
Mem.mk_block_list m'.
Proof.
Require Import Maps.
Definition is_static_block_b m b :=
match (
Mem.mem_blocktype m) !!
b with
Some Dynamic =>
false
|
_ =>
true
end.
Definition is_dynamic_block_b m b :=
match (
Mem.mem_blocktype m) !!
b with
Some Dynamic =>
true
|
_ =>
false
end.
Definition nb_boxes_static (
m:
mem) :=
Mem.nb_boxes_used (
filter (
fun bsz =>
is_static_block_b m (
fst bsz)) (
Mem.mk_block_list m)).
Definition nb_boxes_dynamic (
m:
mem) :=
Mem.nb_boxes_used (
filter (
fun bsz =>
is_dynamic_block_b m (
fst bsz)) (
Mem.mk_block_list m)).
Lemma nb_boxes_app:
forall l1 l2,
(
Mem.nb_boxes_used (
l1 ++
l2) =
Mem.nb_boxes_used l1 +
Mem.nb_boxes_used l2)%
nat.
Proof.
Lemma partition_app_perm:
forall {
A:
Type}
f (
l:
list A)
a b,
partition f l = (
a,
b) ->
Permutation l (
a ++
b).
Proof.
induction l;
simpl;
intros;
eauto.
-
inv H.
simpl;
constructor.
-
repeat destr_in H.
+
inv H.
specialize (
IHl _ _ eq_refl).
simpl.
constructor.
auto.
+
inv H.
specialize (
IHl _ _ eq_refl).
eapply perm_trans.
apply perm_skip.
eauto.
apply Permutation_middle.
Qed.
Lemma lnr_nin:
forall {
A:
Type} (
f:
A ->
bool)
l a b,
partition f l = (
a,
b) ->
forall x, ~
In x l ->
~
In x a /\ ~
In x b.
Proof.
induction l;
simpl;
intros;
eauto.
-
inv H;
destr.
-
repeat destr_in H;
inv H;
specialize (
IHl _ _ eq_refl);
destr.
trim (
IHl x).
destr.
split;
destr.
trim (
IHl x).
destr.
split;
destr.
Qed.
Lemma lnr_partition:
forall {
A:
Type} (
f:
A ->
bool)
l a b,
partition f l = (
a,
b) ->
list_norepet l ->
list_norepet a /\
list_norepet b.
Proof.
induction l;
simpl;
intros;
eauto.
-
inv H.
split;
constructor.
-
repeat destr_in H;
inv H;
specialize (
IHl _ _ eq_refl);
inv H0;
split;
trim IHl;
auto.
constructor;
auto.
eapply lnr_nin in H2;
eauto.
destr.
destr.
destr.
destr.
constructor;
auto.
eapply lnr_nin in H2;
eauto.
destr.
destr.
Qed.
Lemma in_partition_l:
forall {
A:
Type} (
f:
A ->
bool)
l a b,
partition f l = (
a,
b) ->
forall x,
In x a <->
In x l /\
f x =
true.
Proof.
induction l;
simpl;
intros;
eauto.
-
inv H.
simpl;
tauto.
-
repeat destr_in H;
inv H;
specialize (
IHl _ _ eq_refl).
simpl.
+
split;
intros.
destruct H;
auto.
destr.
apply IHl in H.
destr.
destruct H.
destruct H;
auto.
right;
rewrite IHl.
destr.
+
split;
intros.
apply IHl in H.
destr.
destruct H.
rewrite IHl.
destruct H;
auto.
congruence.
Qed.
Lemma lnr_nin':
forall {
A B:
Type} (
f:
A *
B ->
bool) (
l:
list (
A*
B))
a b,
partition f l = (
a,
b) ->
forall x, ~
In x (
map fst l) ->
~
In x (
map fst a) /\ ~
In x (
map fst b).
Proof.
induction l;
simpl;
intros;
eauto.
-
inv H;
destr.
-
repeat destr_in H;
inv H;
specialize (
IHl _ _ eq_refl);
destr.
trim (
IHl x).
destr.
split;
destr.
trim (
IHl x).
destr.
split;
destr.
Qed.
Lemma lnr_partition':
forall {
A B:
Type} (
f:
A *
B ->
bool) (
l:
list (
A *
B))
a b,
partition f l = (
a,
b) ->
list_norepet (
map fst l) ->
list_norepet (
map fst a) /\
list_norepet (
map fst b).
Proof.
induction l;
simpl;
intros;
eauto.
-
inv H.
split;
constructor.
-
repeat destr_in H;
inv H;
specialize (
IHl _ _ eq_refl);
inv H0;
split;
trim IHl;
auto;
simpl.
constructor;
auto.
eapply lnr_nin'
in H2;
eauto.
destr.
destr.
destr.
destr.
constructor;
auto.
eapply lnr_nin'
in H2;
eauto.
destr.
destr.
Qed.
Lemma permut_filter_map:
forall {
A B} (
f:
A ->
option B) (
l l':
list A),
Permutation l l' ->
Permutation (
filter_map f l) (
filter_map f l').
Proof.
induction 1;
simpl;
intros;
eauto.
-
destr;
auto.
-
repeat destr;
auto.
apply perm_swap.
-
rewrite IHPermutation1;
auto.
Qed.
Lemma in_partition_r:
forall {
A:
Type} (
f:
A ->
bool)
l a b,
partition f l = (
a,
b) ->
forall x,
In x b <->
In x l /\
f x =
false.
Proof.
induction l;
simpl;
intros;
eauto.
-
inv H.
simpl;
tauto.
-
repeat destr_in H;
inv H;
specialize (
IHl _ _ eq_refl).
simpl.
+
split;
intros.
apply IHl in H.
destr.
destruct H.
rewrite IHl.
destr.
+
split;
intros.
destruct H;
auto.
destr.
apply IHl in H.
destr.
destruct H.
destr.
destruct H;
auto.
right;
rewrite IHl.
destr.
Qed.
Lemma not_inj_filter_map:
forall {
A B} (
f:
A ->
option B) (
l0:
list A)
(
Spec:
forall b,
In b l0 ->
f b =
None),
filter_map f l0 =
nil.
Proof.
induction l0; simpl; intros; eauto.
des (f a). rewrite Spec in Heqo; destr.
eapply IHl0; eauto.
Qed.
Lemma partition_filter:
forall {
A} (
f:
A ->
bool)
l l1 l2,
partition f l = (
l1,
l2) ->
l1 =
filter f l.
Proof.
induction l;
simpl;
intros.
inv H;
auto.
destr_in H.
specialize (
IHl _ _ eq_refl).
subst.
destr_in H;
inv H;
auto.
Qed.
Lemma partition_filter_r:
forall {
A} (
f:
A ->
bool)
l l1 l2,
partition f l = (
l1,
l2) ->
l2 =
filter (
fun b =>
negb (
f b))
l.
Proof.
induction l;
simpl;
intros.
inv H;
auto.
destr_in H.
specialize (
IHl _ _ eq_refl).
subst.
destr_in H;
inv H;
auto.
Qed.
Lemma filter_app:
forall {
A}
f (
l1 l2:
list A),
filter f (
l1 ++
l2) =
filter f l1 ++
filter f l2.
Proof.
induction l1; simpl; intros; eauto.
rewrite IHl1. destr.
Qed.
Lemma filter_dynamic_static_permut:
forall m l,
Permutation
(
filter (
fun bsz :
positive *
Z =>
is_static_block_b m (
fst bsz))
l ++
filter (
fun bsz :
positive *
Z =>
is_dynamic_block_b m (
fst bsz))
l)
l.
Proof.
Lemma nb_boxes_sep:
forall m,
(
Mem.nb_boxes_used_m m =
nb_boxes_static m +
nb_boxes_dynamic m +
Mem.nb_extra m)%
nat.
Proof.
Lemma release_boxes_nb_static:
forall m n m' (
REL:
release_boxes m n =
Some m'),
nb_boxes_static m =
nb_boxes_static m'.
Proof.
Lemma nb_boxes_free_filter:
forall sz'
sz n b
(
sz_ext:
forall b',
b <>
b' ->
sz'
b' =
sz b')
(
EQ:
sz'
b = 0)
f (
F:
forall z,
f (
b,
z) =
true),
Mem.nb_boxes_used (
filter f (
mk_block_list_aux sz n)) =
(
Mem.nb_boxes_used (
filter f (
mk_block_list_aux sz'
n))
+
if le_dec (
Pos.to_nat b)
n
then Mem.box_span (
sz b)
else 0)%
nat.
Proof.
Lemma bounds_eq:
forall m b,
Mem.bounds_of_block m b = (0,
Mem.size_block m b).
Proof.
Lemma box_span_0:
0%
nat =
Mem.box_span 0.
Proof.
Lemma free_static_nb_static:
forall m b lo hi m'
(
DYN: ~
Mem.is_dynamic_block m b)
(
FREE:
Mem.free m b lo hi =
Some m'),
nb_boxes_static m = (
nb_boxes_static m' +
Mem.box_span (
hi -
lo))%
nat.
Proof.
Lemma free_list_nb_static:
forall bl m m',
Mem.free_list m bl =
Some m' ->
Forall (
fun x =>
let '(
b,
_,
_) :=
x in is_static_block_b m b =
true)
bl ->
(
nb_boxes_static m' +
size_list bl =
nb_boxes_static m)%
nat.
Proof.
Lemma nb_extra_release:
forall m n m' (
REL:
release_boxes m n =
Some m'),
Mem.nb_extra m = (
Mem.nb_extra m' +
n)%
nat.
Proof.
unfold release_boxes.
intros m n m'.
destr.
intro;
inv REL.
simpl.
lia.
Qed.
Lemma free_list_nb_static':
forall bl m m',
Mem.free_list m bl =
Some m' ->
Forall (
fun x => ~
Mem.is_dynamic_block m x) (
map fst (
map fst bl)) ->
(
nb_boxes_static m' +
size_list bl =
nb_boxes_static m)%
nat.
Proof.
Lemma size_list_cons:
forall b lo hi l,
size_list (((
b,
lo),
hi)::
l) = (
size_list l +
Mem.box_span (
hi -
lo))%
nat.
Proof.
Lemma alloc_static_nb_static:
forall m lo hi m'
b (
ALLOC:
Mem.alloc m lo hi Normal =
Some (
m',
b)),
(
nb_boxes_static m +
Mem.box_span (
Z.max 0
hi) =
nb_boxes_static m')%
nat.
Proof.
Lemma size_list_permut:
forall l l' (
P:
Permutation l l'),
size_list l =
size_list l'.
Proof.
Lemma reserve_boxes_mk_block_list:
forall m n m' (
REL:
reserve_boxes m n =
Some m'),
Mem.mk_block_list m =
Mem.mk_block_list m'.
Proof.
Lemma reserve_boxes_nb_static:
forall m n m' (
REL:
reserve_boxes m n =
Some m'),
nb_boxes_static m =
nb_boxes_static m'.
Proof.
Lemma release_nb_dynamic:
forall m n m' (
REL:
release_boxes m n =
Some m'),
nb_boxes_dynamic m =
nb_boxes_dynamic m'.
Proof.
unfold release_boxes.
intros.
destr_in REL;
inv REL.
reflexivity.
Qed.
Lemma Permutation_intro:
forall {
A} (
D:
forall (
a b:
A), {
a=
b}+{
a<>
b}) (
l1 l2:
list A),
list_norepet l1 ->
list_norepet l2 ->
(
forall x,
In x l1 <->
In x l2) ->
Permutation l1 l2.
Proof.
Remark filter_norepet:
forall (
A:
Type) (
f:
A ->
bool)
l,
list_norepet l ->
list_norepet (
List.filter f l).
Proof.
induction 1;
simpl.
constructor.
destruct (
f hd);
auto.
constructor;
auto.
rewrite filter_In.
tauto.
Qed.
Lemma in_mbla:
forall b z sz n,
In b (
map fst (
mk_block_list_aux sz n)) ->
z =
sz b ->
In (
b,
z) (
mk_block_list_aux sz n).
Proof.
intros.
rewrite in_map_iff in H.
dex.
des H.
des x.
exploit mbla_in;
eauto.
intro;
subst;
auto.
Qed.
Lemma in_sz_ext:
forall sz sz'
n b,
In b (
map fst (
mk_block_list_aux sz n)) ->
In b (
map fst (
mk_block_list_aux sz'
n)).
Proof.
Lemma free_static_nb_dynamic:
forall m b lo hi m' (
FREE:
Mem.free m b lo hi =
Some m')
(
DYN: ~
Mem.is_dynamic_block m b),
nb_boxes_dynamic m =
nb_boxes_dynamic m'.
Proof.
Lemma free_dynamic_nb_static:
forall m b lo hi m'
(
DYN:
Mem.is_dynamic_block m b)
(
FREE:
Mem.free m b lo hi =
Some m'),
nb_boxes_static m =
nb_boxes_static m'.
Proof.
Lemma free_dynamic_nb_dynamic:
forall m b lo hi m'
(
DYN:
Mem.is_dynamic_block m b)
(
FREE:
Mem.free m b lo hi =
Some m'),
nb_boxes_dynamic m = (
nb_boxes_dynamic m' +
Mem.box_span (
hi -
lo))%
nat.
Proof.
Lemma free_list_static_nb_dynamic:
forall bl m m' (
FREE:
Mem.free_list m bl =
Some m')
(
DYN:
Forall (
fun b => ~
Mem.is_dynamic_block m b) (
map fst (
map fst bl))),
nb_boxes_dynamic m =
nb_boxes_dynamic m'.
Proof.
Lemma reserve_boxes_nb_extra:
forall m n m' (
REL:
reserve_boxes m n =
Some m'),
(
Mem.nb_extra m +
n =
Mem.nb_extra m')%
nat.
Proof.
Lemma reserve_boxes_nb_dynamic:
forall m n m' (
RB:
reserve_boxes m n =
Some m'),
nb_boxes_dynamic m =
nb_boxes_dynamic m'.
Proof.
Lemma store_nb_dynamic:
forall m chunk b ofs v m' (
STORE:
Mem.store chunk m b ofs v =
Some m'),
nb_boxes_dynamic m =
nb_boxes_dynamic m'.
Proof.
Lemma alloc_dynamic_nb_static:
forall m lo hi m'
b (
ALLOC:
Mem.alloc m lo hi Dynamic =
Some (
m',
b)),
nb_boxes_static m =
nb_boxes_static m'.
Proof.
Lemma store_nb_static:
forall m chunk b ofs v m' (
STORE:
Mem.store chunk m b ofs v =
Some m'),
nb_boxes_static m =
nb_boxes_static m'.
Proof.
Lemma storebytes_nb_dynamic:
forall m b ofs v m' (
STOREBYTES:
Mem.storebytes m b ofs v =
Some m'),
nb_boxes_dynamic m =
nb_boxes_dynamic m'.
Proof.
Lemma storebytes_nb_static:
forall m b ofs v m' (
STOREBYTES:
Mem.storebytes m b ofs v =
Some m'),
nb_boxes_static m =
nb_boxes_static m'.
Proof.
Lemma filter_ext':
forall {
A} (
l:
list A)
p p' (
P:
forall b,
In b l ->
p b =
p'
b),
filter p l =
filter p'
l.
Proof.
induction l; simpl; intros; auto.
rewrite P; auto. destr; rewrite (IHl p p'); eauto.
Qed.
Lemma alloc_dynamic_nb_dynamic:
forall m lo hi m'
b (
ALLOC:
Mem.alloc m lo hi Dynamic =
Some (
m',
b)),
(
nb_boxes_dynamic m +
Mem.box_span (
Z.max 0
hi) =
nb_boxes_dynamic m')%
nat.
Proof.
Lemma fold_left_plus_in_le:
forall l x,
In x l ->
(
x <=
fold_left plus l O)%
nat.
Proof.
induction l;
simpl;
intros;
eauto.
easy.
rewrite fold_left_plus_rew.
des H.
lia.
trim (
IHl x);
auto.
lia.
Qed.
Lemma size_block_mu:
forall m b,
Mem.size_block m b <=
Integers.Int.max_unsigned.
Proof.
Lemma match_cont_sm:
forall bl m m'
m''
N,
Mem.free_list m bl =
Some m' ->
release_boxes m'
N =
Some m'' ->
(
Mem.nb_boxes_used_m m'' =
Mem.nb_boxes_used_m m -
size_list bl -
N)%
nat.
Proof.
Lemma free_nb_boxes_used:
forall m b lo hi m',
Mem.free m b lo hi =
Some m' ->
(
Mem.nb_boxes_used_m m' +
Mem.box_span hi)%
nat =
Mem.nb_boxes_used_m m.
Proof.
Lemma store_nb_boxes_used_m:
forall chunk m b ofs v m' (
STORE:
Mem.store chunk m b ofs v =
Some m'),
Mem.nb_boxes_used_m m' =
Mem.nb_boxes_used_m m.
Proof.
intros.
Transparent Mem.store.
unfold Mem.store in STORE.
destr_in STORE.
inv STORE.
reflexivity.
Qed.
Lemma storev_nb_boxes_used_m:
forall chunk m vaddr v m' (
STOREV:
Mem.storev chunk m vaddr v =
Some m'),
Mem.nb_boxes_used_m m' =
Mem.nb_boxes_used_m m.
Proof.
Lemma storev_nb_extra:
forall chunk m vaddr v m' (
STOREV:
Mem.storev chunk m vaddr v =
Some m'),
Mem.nb_extra m =
Mem.nb_extra m'.
Proof.
Lemma nb_boxes_reserve:
forall m n m' (
RES:
reserve_boxes m n =
Some m'),
(
Mem.nb_boxes_used_m m' =
Mem.nb_boxes_used_m m +
n)%
nat.
Proof.
Remark map_filter:
forall (
A B:
Type) (
f:
A ->
B) (
pa:
A ->
bool) (
pb:
B ->
bool),
(
forall a,
pb (
f a) =
pa a) ->
forall l,
List.map f (
List.filter pa l) =
List.filter pb (
List.map f l).
Proof.
induction l; simpl.
auto.
rewrite H. destruct (pa a); simpl; congruence.
Qed.
Lemma perm_free_eq:
forall (
m :
mem) (
b :
block) (
lo hi :
Z) (
m' :
mem),
Mem.free m b lo hi =
Some m' ->
forall (
b' :
block) (
o :
Z) (
k :
perm_kind) (
p :
permission),
Mem.perm m'
b'
o k p ->
Mem.perm m b'
o k p /\
b <>
b'.
Proof.
Lemma release_abi :
forall j m (
ABI:
Mem.all_blocks_injected j m)
n m',
release_boxes m n =
Some m' ->
Mem.all_blocks_injected j m'.
Proof.
Lemma release_bounds:
forall o b m n m',
release_boxes m n =
Some m' ->
Mem.in_bound_m o m'
b ->
Mem.in_bound_m o m b.
Proof.
Lemma free_in_bound:
forall m b lo hi m'
(
FREE:
Mem.free m b lo hi =
Some m')
o b'
(
IB:
Mem.in_bound_m o m'
b'),
Mem.in_bound_m o m b'.
Proof.
unfold Mem.in_bound_m.
intros m b lo hi m'
FREE o b'
IB.
destruct (
Mem.free_bounds'
_ _ _ _ _ b'
FREE).
congruence.
rewrite H in IB;
red in IB;
simpl in IB;
omega.
Qed.
Lemma reserve_boxes_nb_boxes_used:
forall m n m' (
REL:
reserve_boxes m n =
Some m'),
(
Mem.nb_boxes_used_m m +
n =
Mem.nb_boxes_used_m m')%
nat.
Proof.
Lemma alloc_static_nb_dynamic:
forall m lo hi m'
b (
ALLOC:
Mem.alloc m lo hi Normal =
Some (
m',
b)),
(
nb_boxes_dynamic m =
nb_boxes_dynamic m')%
nat.
Proof.
Lemma storev_in_bound_m:
forall chunk m addr v m' (
STOREV:
Mem.storev chunk m addr v =
Some m')
b o,
Mem.in_bound_m o m b <->
Mem.in_bound_m o m'
b.
Proof.
Lemma storev_size_mem:
forall chunk m addr v m' (
STOREV:
Mem.storev chunk m addr v =
Some m'),
Mem.nb_boxes_used_m m' =
Mem.nb_boxes_used_m m.
Proof.
Lemma release_nb_static:
forall m n m' (
MR:
release_boxes m n =
Some m'),
(
nb_boxes_static m =
nb_boxes_static m')%
nat.
Proof.
Lemma box_span_add:
forall a b,
b >= 0 ->
a >= 0 ->
(
Mem.box_span (
a +
b) <=
Mem.box_span a +
Mem.box_span b)%
nat.
Proof.