Equivalence relations on memories.
Require Import Coqlib.
Require Import Specif.
Require Import Maps.
Require Import Ast.
Require Import Pointers.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Mem.
Require Import Libtactics.
Require Import Permutation.
Quotienting on range lists
Lemma range_lists_disjoint_ext:
forall {
l1 l1'
l2 l2'}
(
EQ1:
list_equiv l1 l1')
(
EQ2:
list_equiv l2 l2')
(
DISJ:
range_lists_disjoint l1 l2),
range_lists_disjoint l1'
l2'.
Proof.
unfold range_lists_disjoint,
range_not_in;
intros.
by apply DISJ; [
apply (
proj2 (
EQ1 _)) |
apply (
proj2 (
EQ2 _))].
Qed.
Load equality on memories
Lemma load_eq_preserved_by_store:
forall {
c m mx p c'
p'
v'
m'
mx'}
(
Leq:
load_ptr c m p =
load_ptr c mx p)
(
ST:
store_ptr c'
m p'
v' =
Some m')
(
STx:
store_ptr c'
mx p'
v' =
Some mx'),
load_ptr c m'
p =
load_ptr c mx'
p.
Proof.
Lemma load_eq_preserved_by_alloc:
forall {
c m mx p r'
k'
m'
mx'}
(
Leq:
load_ptr c m p =
load_ptr c mx p)
(
AP:
alloc_ptr r'
k'
m =
Some m')
(
APx:
alloc_ptr r'
k'
mx =
Some mx'),
load_ptr c m'
p =
load_ptr c mx'
p.
Proof.
Lemma load_eq_preserved_by_free_same_size:
forall {
c m mx p p'
n'
k'
m'
mx'}
(
Leq:
load_ptr c m p =
load_ptr c mx p)
(
RA:
range_allocated (
p',
n')
k'
m)
(
FP:
free_ptr p'
k'
m =
Some m')
(
RAx:
range_allocated (
p',
n')
k'
mx)
(
FPx:
free_ptr p'
k'
mx =
Some mx'),
load_ptr c m'
p =
load_ptr c mx'
p.
Proof.
Lemma load_eq_preserved_by_free_diff_block:
forall {
c m mx p p'
k'
m'
mx'}
(
Leq:
load_ptr c m p =
load_ptr c mx p)
(
DB:
Ptr.block p <>
Ptr.block p')
(
FP:
free_ptr p'
k'
m =
Some m')
(
FPx:
free_ptr p'
k'
mx =
Some mx'),
load_ptr c m'
p =
load_ptr c mx'
p.
Proof.
intros.
destruct (
free_someD FP)
as [
n RA].
destruct (
free_someD FPx)
as [
nx RAx].
rewrite (
load_free_other FP RA);
[|
by destruct p;
destruct p';
simpl in *;
left].
by rewrite (
load_free_other FPx RAx);
[|
by destruct p;
destruct p';
simpl in *;
left].
Qed.
Equality on allocated ranges
The allocation ranges are equal
Definition arange_eq (
Cond:
_ ->
bool)
m1 m2 :=
(
forall r k (
COND:
Cond k),
range_allocated r k m1 <->
range_allocated r k m2)
/\ (
mrestr m1 =
mrestr m2).
Lemma arange_eq_sub:
forall {
m1 m2}
C D,
arange_eq C m1 m2 ->
(
forall k,
D k =
true ->
C k) ->
arange_eq D m1 m2.
Proof.
by destruct 1; split; auto. Qed.
Lemma arange_eq_refl:
forall C m,
arange_eq C m m.
Proof.
done. Qed.
Lemma arange_eq_sym:
forall {
C m1 m2},
arange_eq C m1 m2 ->
arange_eq C m2 m1.
Proof.
by destruct 1 as [A R]; repeat split; try done; by eapply A. Qed.
Lemma arange_eq_trans:
forall C x y z,
arange_eq C x y ->
arange_eq C y z ->
arange_eq C x z.
Proof.
intros C x y z (X & ?) (Y & ?); split; [intros r k|congruence].
specialize (X r k); specialize (Y r k); tauto.
Qed.
Lemma arange_eq_store:
forall {
m m'
chunk p v}
C,
store_ptr chunk m p v =
Some m' ->
arange_eq C m'
m.
Proof.
Lemma range_in_allocated_arange:
forall {
m1 m2 r}
(
EQ:
arange_eq (
fun _ =>
true)
m1 m2)
(
RA:
range_in_allocated r m1),
range_in_allocated r m2.
Proof.
intros;
destruct RA as (? & ? & ? & ?).
eby do 2
eexists;
split; [|
eapply (
proj1 EQ)].
Qed.
Lemma chunk_allocated_and_aligned_arange:
forall {
m1 m2 chunk p}
(
EQ:
arange_eq (
fun _ =>
true)
m1 m2)
(
CA:
chunk_allocated_and_aligned p chunk m1),
chunk_allocated_and_aligned p chunk m2.
Proof.
Lemma range_list_of_mem_arange:
forall {
m1 m2}
(
EQ:
arange_eq (
fun _ =>
true)
m1 m2),
list_equiv (
range_list_of_mem m1) (
range_list_of_mem m2).
Proof.
Lemma load_ptr_none_arange:
forall {
m1 m2 chunk p}
(
LD:
load_ptr chunk m1 p =
None)
(
EQ:
arange_eq (
fun _ =>
true)
m1 m2),
load_ptr chunk m2 p =
None.
Proof.
Lemma load_ptr_some_arange:
forall m1 m2 chunk p v1
(
H1:
load_ptr chunk m1 p =
Some v1)
(
EQ:
arange_eq (
fun _ =>
true)
m1 m2),
exists v2,
load_ptr chunk m2 p =
Some v2.
Proof.
Lemma store_ptr_none_arange:
forall {
m1 m2 chunk p v}
v'
(
STO:
store_ptr chunk m1 p v =
None)
(
EQ:
arange_eq (
fun _ =>
true)
m1 m2),
store_ptr chunk m2 p v' =
None.
Proof.
Lemma store_ptr_some_arange1:
forall C m1 m2 chunk p v v'
m1'
m2'
(
STO1:
store_ptr chunk m1 p v =
Some m1')
(
STO2:
store_ptr chunk m2 p v' =
Some m2')
(
REQ:
arange_eq C m1 m2),
arange_eq C m1'
m2'.
Proof.
Lemma store_ptr_some_arange:
forall m1 m2 chunk p v v'
m1'
(
H1:
store_ptr chunk m1 p v =
Some m1')
(
EQ:
arange_eq (
fun _ =>
true)
m1 m2),
exists m2',
store_ptr chunk m2 p v' =
Some m2' /\
arange_eq (
fun _ =>
true)
m1'
m2'.
Proof.
Lemma alloc_ptr_none_arange:
forall m1 m2 r k,
alloc_ptr r k m1 =
None ->
arange_eq (
fun _ =>
true)
m1 m2 ->
alloc_ptr r k m2 =
None.
Proof.
intros m1 m2 r k H EQ.
pose proof (
alloc_cond_spec r k m1)
as A1;
destruct (
alloc_ptr r k m1);
try done.
pose proof (
alloc_cond_spec r k m2)
as A2;
destruct (
alloc_ptr r k m2);
try done.
destruct A2 as [
RA [? [?
AL]]].
destruct A1 as [|[|[[? ?] [? [?
RA']]]]];
try done.
destruct (
fst r)
as [
b ofs];
simpl in *.
by rewrite (
proj2 EQ)
in *.
exploit AL;
try edone.
eby eapply (
proj1 ((
proj1 EQ)
_ _ (
refl_equal _))).
Qed.
Lemma alloc_ptr_some_arange1:
forall C m1 m2 r k m1'
m2',
alloc_ptr r k m1 =
Some m1' ->
alloc_ptr r k m2 =
Some m2' ->
arange_eq C m1 m2 ->
arange_eq C m1'
m2'.
Proof.
Lemma alloc_ptr_some_arange:
forall m1 m2 r k m1',
alloc_ptr r k m1 =
Some m1' ->
arange_eq (
fun _ =>
true)
m1 m2 ->
(
exists m2',
alloc_ptr r k m2 =
Some m2' /\
arange_eq (
fun _ =>
true)
m1'
m2').
Proof.
Lemma free_ptr_none_arange:
forall C m1 m2 p k,
free_ptr p k m1 =
None ->
arange_eq C m1 m2 ->
C k ->
free_ptr p k m2 =
None.
Proof.
intros C m1 m2 p k H [
EQ ?]
CC.
pose proof (
free_noneD H)
as A1.
pose proof (
free_cond_spec p k m2)
as A2;
destruct (
free_ptr p k m2);
try done.
destruct A2 as [
n ?].
by elim (
A1 n);
apply (
proj2 (
EQ _ _ CC)).
Qed.
Lemma free_ptr_some_arange1:
forall C m1 m2 p k m1'
m2',
free_ptr p k m1 =
Some m1' ->
free_ptr p k m2 =
Some m2' ->
arange_eq C m1 m2 ->
arange_eq C m1'
m2'.
Proof.
Lemma free_ptr_some_arange:
forall C m1 m2 p k m1',
free_ptr p k m1 =
Some m1' ->
arange_eq C m1 m2 ->
C k ->
(
exists m2',
free_ptr p k m2 =
Some m2' /\
arange_eq C m1'
m2').
Proof.
Lemma load_eq_preserved_by_free_arange:
forall {
c m mx p p'
k'
m'
mx'}
(
Leq:
load_ptr c m p =
load_ptr c mx p)
(
FP:
free_ptr p'
k'
m =
Some m')
(
FPx:
free_ptr p'
k'
mx =
Some mx')
(
Req:
arange_eq (
fun _ =>
true)
m mx),
load_ptr c m'
p =
load_ptr c mx'
p.
Proof.
Less definedness on memories
Definition opt_lessdef vo vo' :=
match vo,
vo'
with
|
Some v,
Some v' =>
Val.lessdef v v'
|
None,
_ =>
True
|
_,
_ =>
False
end.
Definition mem_lessdef (
m m':
mem) :=
forall p c,
opt_lessdef (
load_ptr c m p) (
load_ptr c m'
p).
Definition mem_lessdef_in_range (
m m':
mem) (
r:
arange) :=
forall p c,
range_inside (
range_of_chunk p c)
r ->
opt_lessdef (
load_ptr c m p) (
load_ptr c m'
p).
Lemma opt_lessdef_refl:
forall v,
opt_lessdef v v.
Proof.
by intros [[]|]; vauto. Qed.
Hint Resolve opt_lessdef_refl.
Lemma mem_lessdef_refl:
forall m,
mem_lessdef m m.
Proof.
by intros m p c;
destruct load_ptr. Qed.
Hint Resolve mem_lessdef_refl.
Lemma opt_lessdef_sim_write:
forall tm sm tm'
sm'
p c v v'
p'
c'
(
LDrel:
opt_lessdef (
load_ptr c'
sm p') (
load_ptr c'
tm p'))
(
tSTO:
store_ptr c tm p v =
Some tm')
(
sSTO:
store_ptr c sm p v' =
Some sm')
(
vLDEF:
Val.lessdef v'
v),
opt_lessdef (
load_ptr c'
sm'
p') (
load_ptr c'
tm'
p').
Proof.
Lemma opt_lessdef_sim_alloc:
forall tm sm tm'
sm'
p n k p'
c'
(
LREL:
opt_lessdef (
load_ptr c'
sm p') (
load_ptr c'
tm p'))
(
ACT:
alloc_ptr (
p,
n)
k tm =
Some tm')
(
ACS:
alloc_ptr (
p,
n)
k sm =
Some sm'),
opt_lessdef (
load_ptr c'
sm'
p') (
load_ptr c'
tm'
p').
Proof.
Lemma opt_lessdef_sim_free_same_size:
forall tm sm tm'
sm'
p k n p'
c'
(
LREL:
opt_lessdef (
load_ptr c'
sm p') (
load_ptr c'
tm p'))
(
Ft:
free_ptr p k tm =
Some tm')
(
Fs:
free_ptr p k sm =
Some sm')
(
RAt:
range_allocated (
p,
n)
k tm)
(
RAs:
range_allocated (
p,
n)
k sm),
opt_lessdef (
load_ptr c'
sm'
p') (
load_ptr c'
tm'
p').
Proof.
Lemma mem_lessdef_sim_write:
forall tm sm tm'
sm'
c p v v'
(
LREL:
mem_lessdef sm tm)
(
tSTO:
store_ptr c tm p v =
Some tm')
(
sSTO:
store_ptr c sm p v' =
Some sm')
(
vLDEF:
Val.lessdef v'
v),
mem_lessdef sm'
tm'.
Proof.
Lemma mem_lessdef_sim_alloc:
forall tm sm tm'
sm'
p n k
(
LREL:
mem_lessdef sm tm)
(
ACT:
alloc_ptr (
p,
n)
k tm =
Some tm')
(
ACS:
alloc_ptr (
p,
n)
k sm =
Some sm'),
mem_lessdef sm'
tm'.
Proof.
Lemma mem_lessdef_sim_free_same_size:
forall tm sm tm'
sm'
p n k
(
LREL:
mem_lessdef sm tm)
(
Ft:
free_ptr p k tm =
Some tm')
(
Fs:
free_ptr p k sm =
Some sm')
(
RAt:
range_allocated (
p,
n)
k tm)
(
RAs:
range_allocated (
p,
n)
k sm),
mem_lessdef sm'
tm'.
Proof.
Lemma mem_lessdef_alloc_src:
forall tm sm sm'
p n k
(
LREL:
mem_lessdef sm tm)
(
RA:
range_in_allocated (
p,
n)
tm)
(
ACS:
alloc_ptr (
p,
n)
k sm =
Some sm'),
mem_lessdef sm'
tm.
Proof.
Lemma mem_lessdef_free_src:
forall tm sm sm'
p k
(
LREL:
mem_lessdef sm tm)
(
F:
free_ptr p k sm =
Some sm'),
mem_lessdef sm'
tm.
Proof.
Lemma mem_lessdef_clear_src:
forall tm sm r
(
LREL:
mem_lessdef sm tm),
mem_lessdef (
clear_range r sm)
tm.
Proof.
intros;
intros p'
c';
specialize (
LREL p'
c').
destruct (
load_ptr c' (
clear_range r sm)
p')
as []
_eqn:
LD.
destruct (
load_clear_back LD)
as (? &
LD' &
LDEF);
rewrite LD'
in *.
destruct (
load_ptr c'
tm p');
simpl in *;
clarify.
by inv LREL;
clarify;
inv LDEF;
clarify.
by eapply load_clear_none in LD;
rewrite LD in *.
Qed.
Partial load equality
Definition mem_agrees_on (
m m' :
mem) (
rs :
list arange) :
Prop :=
forall r p c,
In r rs ->
range_inside (
range_of_chunk p c)
r ->
load_ptr c m p =
load_ptr c m'
p.
Lemma mem_agrees_on_sym:
forall {
m m'
rs} (
H:
mem_agrees_on m m'
rs),
mem_agrees_on m'
m rs.
Proof.
eby unfold mem_agrees_on; intros; symmetry; eapply H.
Qed.
Lemma mem_agrees_on_trans:
forall {
x y z rs}
(
X:
mem_agrees_on x y rs)
(
Y:
mem_agrees_on y z rs),
mem_agrees_on x z rs.
Proof.
intros; intros r p c IN RI;
specialize (X _ _ _ IN RI);
specialize (Y _ _ _ IN RI); congruence.
Qed.
Lemma mem_agrees_on_app:
forall {
m m'
s1 s2},
mem_agrees_on m m' (
s1 ++
s2) <->
mem_agrees_on m m'
s1 /\
mem_agrees_on m m'
s2.
Proof.
split; [
by intros MA;
split;
intros r p c IN;
apply MA;
auto using in_or_app|].
intros [
MA1 MA2];
intros r p c IN.
apply ->
in_app in IN;
destruct IN;
[
by apply MA1 |
by apply MA2].
Qed.
Lemma mem_agrees_on_perm:
forall {
m m'
l l'}
(
P:
Permutation l l')
(
MA:
mem_agrees_on m m'
l),
mem_agrees_on m m'
l'.
Proof.
Lemma mem_agrees_on_list_equiv:
forall {
m m'
l l'}
(
EQ:
list_equiv l l')
(
MA:
mem_agrees_on m m'
l),
mem_agrees_on m m'
l'.
Proof.
by intros; intros r p c IN; eapply MA, EQ.
Qed.
Lemma mem_agrees_on_preserved_by_store:
forall {
m mx l c p v m'
mx'}
(
EQ:
mem_agrees_on m mx l)
(
ST:
store_ptr c m p v =
Some m')
(
STx:
store_ptr c mx p v =
Some mx'),
mem_agrees_on m'
mx'
l.
Proof.
Lemma mem_agrees_on_preserved_by_alloc:
forall {
m mx l r k m'
mx'}
(
EQ:
mem_agrees_on m mx l)
(
A:
alloc_ptr r k m =
Some m')
(
Ax:
alloc_ptr r k mx =
Some mx'),
mem_agrees_on m'
mx'
l.
Proof.
Lemma mem_agrees_on_preserved_by_free_same_size:
forall {
m mx l p n k m'
mx'}
(
EQ:
mem_agrees_on m mx l)
(
RA:
range_allocated (
p,
n)
k m)
(
F:
free_ptr p k m =
Some m')
(
RAx:
range_allocated (
p,
n)
k mx)
(
Fx:
free_ptr p k mx =
Some mx'),
mem_agrees_on m'
mx'
l.
Proof.
Lemma mem_agrees_on_preserved_by_free_arange:
forall {
m mx l p k m'
mx'}
(
EQ:
mem_agrees_on m mx l)
(
REQ:
arange_eq (
fun _ =>
true)
m mx)
(
F:
free_ptr p k m =
Some m')
(
Fx:
free_ptr p k mx =
Some mx'),
mem_agrees_on m'
mx'
l.
Proof.
Extensional equality on memories
Definition mem_eq m1 m2:=
(
forall chunk p,
load_ptr chunk m1 p =
load_ptr chunk m2 p)
/\ (
forall r k,
range_allocated r k m1 <->
range_allocated r k m2)
/\ (
mrestr m1 =
mrestr m2).
Lemma in_block1:
forall lbnd hbnd l h k ba,
alloclist_hbound lbnd (
mkmobj l h k ::
ba) =
Some hbnd -> 0 <
lbnd ->
hbnd <=
Int.modulus ->
valid_access Mint8unsigned (
l mod Int.modulus) (
mkmobj l h k ::
ba).
Proof.
Lemma alloclist1:
forall lbnd hbnd l h k a,
alloclist_hbound lbnd (
mkmobj l h k ::
a) =
Some hbnd ->
lbnd <=
l /\
l <
h /\
h <=
hbnd /\ (
align_size (
h -
l) |
l).
Proof.
Lemma range_allocated_al_cons:
forall l h k l'
h'
k'
ba',
range_allocated_al l h k (
mkmobj l'
h'
k' ::
ba') ->
l =
l' /\
h =
h' /\
k =
k' \/
range_allocated_al l h k ba'.
Proof.
unfold range_allocated_al.
by inversion 1; clarify; [left|right].
Qed.
Lemma valid_access_bounded:
forall c ofs al lbnd hbnd,
alloclist_hbound lbnd al =
Some hbnd ->
valid_access c ofs al ->
lbnd <=
ofs <
hbnd.
Proof.
Lemma Zabs_nat_of_nat:
forall n,
Zabs_nat (
Z_of_nat n) =
n.
Proof.
Lemma contents_eq_ext:
forall bc bc'
ba,
block_valid (
mkblock bc ba) ->
block_valid (
mkblock bc'
ba) ->
(
forall c ofs,
valid_access c ofs ba ->
Val.load_result c (
getN (
pred_size_chunk c) (
ofs mod Int.modulus)
bc)
=
Val.load_result c (
getN (
pred_size_chunk c) (
ofs mod Int.modulus)
bc')) ->
bc =
bc'.
Proof.
intros bc bc'
ba (
UU &
OK &
hbnd &
B &
M) (
UU' &
OK' &
hbnd' &
B' &
M')
LD.
apply ZTree.ext;
intros ofs.
destruct (
ZTree.get ofs bc)
as [[]|]
_eqn:
G.
Case "
Datum".
pose proof (
proj1 (
proj2 OK _ _ _ G))
as [
c [
SZ [
VOK ACCOK]]].
generalize (
LD c ofs ACCOK).
assert (
ofsRNG: 0 <=
ofs <
Int.modulus)
by (
pose proof (
valid_access_bounded _ _ _ _ _ B ACCOK);
omega).
rewrite Zmod_small;
try done.
destruct ACCOK as [
k ? ?];
simpl in *.
unfold getN.
rewrite G,
SZ,
dec_eq_true,
value_chunk_ok1;
try done.
destruct (
ZTree.get ofs bc')
as [[]|]
_eqn:
G';
try done;
try destruct eq_nat_dec;
try rewrite load_result_undef;
intro X;
clarify;
try by revert VOK;
clear;
destruct c.
pose proof (
proj1 (
proj2 OK'
_ _ _ G'))
as [
c' [
SZ' [
VOK'
ACCOK']]].
rewrite value_chunk_ok1;
try done.
by revert VOK VOK'
SZ';
clear;
destruct c';
destruct c;
destruct v0.
Case "
Cont".
pose proof (
proj1 OK _ _ G)
as (
l &
v &
Gm).
pose proof (
proj1 (
proj2 OK _ _ _ Gm))
as [
c [
SZ [
VOK ACCOK]]].
generalize (
LD _ _ ACCOK).
assert (
ofsRNG: 0 <=
ofs -
Z_of_nat n <
Int.modulus)
by (
pose proof (
valid_access_bounded _ _ _ _ _ B ACCOK);
omega).
rewrite Zmod_small;
try done.
destruct ACCOK as [
k ? ?];
simpl in *.
unfold getN.
rewrite Gm,
SZ,
dec_eq_true,
value_chunk_ok1;
try done.
destruct (
ZTree.get (
ofs -
Z_of_nat n)
bc')
as [[]|]
_eqn:
G';
try done;
try destruct eq_nat_dec;
try rewrite load_result_undef;
intro X;
clarify;
try by revert VOK;
clear;
destruct c.
destruct n.
by simpl in *;
rewrite Zminus_0_r in *;
rewrite G in Gm.
pose proof (
proj1 (
proj2 OK'
_ _ _ G'))
as [
c' [
SZ' [
VOK'
ACCOK']]].
exploit (
check_cont_inside _ _ _ _ ofs (
proj2 (
proj2 OK'
_ _ _ G')));
unfold contents;
rewrite inj_S.
omega.
intros ->;
f_equal;
f_equal.
replace (
ofs - (
ofs -
Zsucc (
Z_of_nat n) + 1))
with (
Z_of_nat n); [
rewrite Zabs_nat_of_nat|];
omega.
Case "
None".
destruct (
ZTree.get ofs bc')
as [[]|]
_eqn:
G';
try done.
SCase "
Datum".
pose proof (
proj1 (
proj2 OK'
_ _ _ G'))
as [
c [
SZ [
VOK ACCOK]]].
generalize (
LD c ofs ACCOK).
assert (
ofsRNG: 0 <=
ofs <
Int.modulus)
by (
pose proof (
valid_access_bounded _ _ _ _ _ B ACCOK);
omega).
rewrite Zmod_small;
try done.
destruct ACCOK as [
k ? ?];
simpl in *.
unfold getN.
rewrite G,
G',
SZ,
dec_eq_true,
load_result_undef,
value_chunk_ok1;
try done.
by revert VOK;
clear;
destruct c;
destruct v.
SCase "
Cont".
pose proof (
proj1 OK'
_ _ G')
as (
l &
v &
Gm').
pose proof (
proj1 (
proj2 OK'
_ _ _ Gm'))
as [
c [
SZ [
VOK ACCOK]]].
generalize (
LD _ _ ACCOK).
assert (
ofsRNG: 0 <=
ofs -
Z_of_nat n <
Int.modulus)
by (
pose proof (
valid_access_bounded _ _ _ _ _ B ACCOK);
omega).
rewrite Zmod_small;
try done.
destruct ACCOK as [
k ? ?];
simpl in *.
unfold getN.
rewrite Gm',
SZ,
dec_eq_true.
destruct (
ZTree.get (
ofs -
Z_of_nat n)
bc)
as [[]|]
_eqn:
Gm;
try done;
try destruct eq_nat_dec;
try rewrite load_result_undef;
try (
by revert VOK;
destruct c;
destruct v).
intro X;
clarify.
destruct n.
by simpl in *;
rewrite Zminus_0_r in *;
rewrite G in Gm.
pose proof (
proj1 (
proj2 OK _ _ _ Gm))
as [
c' [
SZ' [
VOK'
ACCOK']]].
exploit (
check_cont_inside _ _ _ _ ofs (
proj2 (
proj2 OK _ _ _ Gm)));
unfold contents;
rewrite inj_S.
omega.
by rewrite G.
Qed.
Lemma range_allocated_implies_allocs_eq:
forall m m'
b bc bc',
(
forall (
r :
arange) (
k :
mobject_kind),
range_allocated r k m <->
range_allocated r k m') ->
ZTree.get b (
mcont m) =
Some bc ->
ZTree.get b (
mcont m') =
Some bc' ->
allocs bc =
allocs bc'.
Proof.
Lemma mem_eq_ext:
forall m1 m2,
mem_eq m1 m2 ->
m1 =
m2.
Proof.