# Module Memaux

Require Import Coqlib.
Require Import Integers.
Require Import Values.
Require Import Pointers.
Require Import Mem.
Require Import Ast.
Require Import Maps.
Require Import Libtactics.

Set Implicit Arguments.

# Basic lemmata

Lemma store_allocated:
forall {p c v m m'} (A: store_ptr c m p v = Some m') r k,
range_allocated r k m' <-> range_allocated r k m.
Proof.
by intros; eapply iff_sym, (store_preserves_allocated_ranges A).
Qed.

Lemma alloc_allocated:
forall {r' k' m m'} (A: alloc_ptr r' k' m = Some m') r k,
range_allocated r k m' <-> range_allocated r k m \/ (r = r' /\ k = k').
Proof.
split; intro; des; clarify.
- eapply (alloc_preserves_allocated_back A) in H; tauto.
- by apply (alloc_preserves_allocated A).
- by destruct (alloc_someD A).
Qed.

Lemma free_allocated:
forall {p k' m m' n}
(F: free_ptr p k' m = Some m')
(RA: range_allocated (p,n) k' m) r k,
range_allocated r k m' <-> range_allocated r k m /\ fst r <> p.
Proof.
split; intro; des.
split; [eby eapply (free_preserves_allocated_back F)|].
eby intro; clarify; destruct r; eapply free_not_allocated.
eapply (free_preserves_allocated F) in H; des; clarify.
Qed.

forall {r k m m' c' p'},
alloc_ptr r k m = Some m' ->
range_inside (range_of_chunk p' c') r ->
(if pointer_chunk_aligned_dec p' c' then Some Vundef else None).
Proof.
intros; destruct (pointer_chunk_aligned_dec p' c').
destruct (load_ptr c' m' p') as [] _eqn: X; try done.
Qed.

forall {r k m m' c' p'},
alloc_ptr r k m = Some m' ->
load_ptr c' m p' = None ->
~ range_inside (range_of_chunk p' c') r ->
load_ptr c' m' p' = None.
Proof.
intros; destruct (ranges_disjoint_dec (range_of_chunk p' c') r).
Qed.

forall {p k m m' c' p'},
free_ptr p k m = Some m' ->
load_ptr c' m p' = None ->
load_ptr c' m' p' = None.
Proof.
intros; destruct (free_someD H) as [n RA].
destruct (ranges_disjoint_dec (range_of_chunk p' c') (p, n)).
Qed.

forall {p c v m m' c' p'},
store_ptr c m p v = Some m' ->
load_ptr c' m p' = None ->
load_ptr c' m' p' = None.
Proof.
intros; destruct (load_ptr c' m' p') as [] _eqn: X; clarify.
destruct (load_chunk_allocated_someD X) as [(? & ? & ? & RA) ?].
eapply (store_allocated H) in RA.
eby destruct (load_chunk_allocated_noneD H0); repeat eexists.
Qed.

# 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.
intros; constructor 1 with (k:=k); [|by apply Zone_divide].
exists l; exists h; split; [by left|].
exploit (@alloclist_hbound_impl_l_lt_h); [eassumption|by left|intro].
rewrite Zmod_small; simpl; omega.
Qed.

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.
intros lbnd hbnd l h k a H.
by destruct (alloclist_hbound_impl_l_lt_h H (in_eq _ _)) as (? & ? & ? & ?).
Qed.

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.
intros until 0; intros H [k [l [h [RA ?]]] AL].
eapply @alloclist_hbound_impl_l_lt_h in H; try edone.
destruct c; simpl in *; omega.
Qed.

Lemma Zabs_nat_of_nat: forall n, Zabs_nat (Z_of_nat n) = n.
Proof.
by destruct n; simpl; auto using nat_of_P_o_P_of_succ_nat_eq_succ.
Qed.

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.
intros [mc mr mv] [mc' mr' mv'] b [bc ba] [bc' ba'] RA EQ EQ'; simpl in *.
pose proof (proj2 (proj2 (proj1 (proj2 (proj2 mv _ _ EQ))))) as [hbnd [B M]].
pose proof (proj2 (proj2 (proj1 (proj2 (proj2 mv' _ _ EQ'))))) as [hbnd' [B' M']].
unfold range_allocated in *; simpl in *.

assert (Y: forall ofs s k,
range_allocated_al (Int.unsigned ofs)
(Int.unsigned ofs + Int.unsigned s) k ba <->
range_allocated_al (Int.unsigned ofs)
(Int.unsigned ofs + Int.unsigned s) k ba').
by intros; generalize (RA (Ptr b ofs, s) k); simpl; rewrite EQ, EQ'.
clear RA; revert Y.
simpl in *.
clear EQ' EQ.
revert B B' M'; cut (1 > 0); [|omega]; generalize 1 as lbnd; revert ba' hbnd'.

induction ba as [|[l h k] ba IH]; destruct ba' as [|[l' h' k'] ba']; try done;
intros hbnd' lbnd POS B B' M' Y.
exploit (proj2 (Y (Int.repr l') (Int.repr (h' - l')) k')); try done.
apply alloclist1 in B'.
left; simpl; f_equal; rewrite ?Zmod_small; omega.
exploit (proj1 (Y (Int.repr l) (Int.repr (h - l)) k)); try done.
apply alloclist1 in B.
left; simpl; f_equal; rewrite ?Zmod_small; omega.
assert (l = l' /\ h = h' /\ k = k') as [-> [-> ->]].
pose proof (alloclist1 _ _ _ _ _ B).
pose proof (alloclist1 _ _ _ _ _ B').
exploit (proj1 (Y (Int.repr l) (Int.repr (h - l)) k)); simpl;
rewrite ?Zmod_small, Zplus_minus; try omega; [by left|].
exploit (proj2 (Y (Int.repr l') (Int.repr (h' - l')) k')); simpl;
rewrite ?Zmod_small, Zplus_minus; try omega; [by left|].
intros X' X.
apply range_allocated_al_cons in X; destruct X as [X|X]; try done.
apply range_allocated_al_cons in X'; destruct X' as [[-> [-> ->]]|X']; try done.
simpl in B; destruct aligned_rng_dec; try done; destruct Z_le_dec; try done.
simpl in B'; destruct aligned_rng_dec; try done; destruct Z_le_dec; try done.
pose proof (alloclist_hbound_impl_l_lt_h B' X).
pose proof (alloclist_hbound_impl_l_lt_h B X').
f_equal.
simpl in B, B'; destruct aligned_rng_dec; clarify; destruct Z_le_dec; clarify.
apply IH with (hbnd' := hbnd') (lbnd := h'); try done.
omega.
intros ofs s k.
split; intro IN.
destruct (proj1 (Y ofs s k) (or_intror _ IN)) as [|]; clarify.
pose proof (alloclist_hbound_impl_l_lt_h B IN).
destruct (proj2 (Y ofs s k) (or_intror _ IN)) as [|]; clarify.
pose proof (alloclist_hbound_impl_l_lt_h B' IN).
Qed.

Theorem mem_eq_ext:
forall m1 m2, mem_eq m1 m2 -> m1 = m2.
Proof.
intros [mc mr mv] [mc' mr' mv'] [LD [RA MR]]; simpl in *; subst mr'.
cut (mc = mc'); [by intro; subst mc'; rewrite (proof_irrelevance _ mv mv')|].
apply ZTree.ext; intros b.
destruct (ZTree.get b mc) as [[bc ba]|] _eqn: EQ;
destruct (ZTree.get b mc') as [[bc' ba']|] _eqn: EQ'; try done.

Case "SomeSome".
generalize (range_allocated_implies_allocs_eq _ _ _ RA EQ EQ'); simpl; intros <-.
f_equal; f_equal.
pose proof (proj1 (proj2 (proj2 mv _ _ EQ))) as V.
pose proof (proj1 (proj2 (proj2 mv' _ _ EQ'))) as V'.
apply (contents_eq_ext V V'); intros c ofs VA.
generalize (LD c (Ptr b (Int.repr ofs))).
simpl; unfold load; simpl; rewrite EQ, EQ'; simpl.
rewrite Zmod_small, !in_block_true; try done.
by intro; clarify.
by destruct V as (? & ? & ? & B & ?);
pose proof (valid_access_bounded _ B VA); omega.

Case "SomeNone".
case mv; intros _ V.
pose proof (proj2 (V _ _ EQ)) as [[V1 [_ [hbnd [? ?]]]] M].
destruct ba as [|[l h k] ?].
assert (bc = ZTree.empty _); [|by elim M; subst].
apply ZTree.ext; intro x; rewrite ZTree.gempty; apply V1; simpl.
by intros k [? [? [RA' _]]]; inversion RA'.
simpl; rewrite EQ, EQ'; simpl.
eby rewrite in_block_empty, in_block_true; [|eapply in_block1].

Case "NoneSome".
case mv'; intros _ V.
pose proof (proj2 (V _ _ EQ')) as [[V1 [_ [hbnd [? ?]]]] M].
destruct ba' as [|[l h k] ?].
assert (bc' = ZTree.empty _); [|by elim M; subst].
apply ZTree.ext; intro x; rewrite ZTree.gempty; apply V1; simpl.
by intros k [? [? [RA' _]]]; inversion RA'.
simpl; rewrite EQ, EQ'; simpl.
eby rewrite in_block_empty, in_block_true; [|eapply in_block1].
Qed.

forall {c m mx p c' p' v' m' mx'}
(ST: store_ptr c' m p' v' = Some m')
(STx: store_ptr c' mx p' v' = Some mx'),
Proof.
intros.
pose proof (load_chunk_allocated_spec c m p) as LDAL.
pose proof (load_chunk_allocated_spec c mx p) as LDALX.
pose proof (load_chunk_allocated_spec c m' p) as LDAL'.
pose proof (load_chunk_allocated_spec c mx' p) as LDALX'.
destruct (load_ptr c m p) as [v|] _eqn : SMLD.
destruct (range_eq_dec (range_of_chunk p' c') (range_of_chunk p c))
as [RCeq | RCneq].
injection RCeq.
intro SCeqm.
assert (SCeq: size_chunk c' = size_chunk c).
destruct c; destruct c'; simpl in *; compute in SCeqm; done.
intro Peq; subst.
destruct (ranges_disjoint_dec (range_of_chunk p' c')
(range_of_chunk p c))
as [RDISJ | ROVER].
rewrite <- (load_store_other ST RDISJ), SMLD.
by rewrite <- (load_store_other STx RDISJ).
apply (store_preserves_chunk_allocation ST _ _) in LDAL.
rewrite (load_store_overlap ST ROVER RCneq LDAL).
destruct (load_ptr c mx p) as [v''|] _eqn : SMLD'.
apply (store_preserves_chunk_allocation STx p c) in LDALX.
rewrite (load_store_overlap STx ROVER RCneq LDALX).
done.
by destruct (load_ptr c mx' p);
[apply (store_preserves_chunk_allocation STx _ _) in LDALX'|].
apply sym_eq in Leq. rewrite Leq in LDALX.
destruct (load_ptr c m' p) as [cmv|] _eqn : E2;
destruct (load_ptr c mx' p) as [cmv'|] _eqn : E3;
try apply (store_preserves_chunk_allocation STx _ _) in LDALX';
try apply (store_preserves_chunk_allocation ST _ _) in LDAL';
try done.
Qed.

forall {c m mx p r' k' m' mx'}
(AP: alloc_ptr r' k' m = Some m')
(APx: alloc_ptr r' k' mx = Some mx'),
Proof.
intros; destruct r' as [p' n'].
pose proof (load_chunk_allocated_spec c m p) as LDAL.
pose proof (load_chunk_allocated_spec c mx p) as LDALX.
pose proof (load_chunk_allocated_spec c m' p) as LDAL'.
pose proof (load_chunk_allocated_spec c mx' p) as LDALX'.
destruct (pointer_chunk_aligned_dec p c) as [CA | CNA].
try done; destruct LDAL'; destruct LDALX'; done.
destruct (range_inside_dec (range_of_chunk p c) (p', n')) as [RI | RNI].
destruct (ranges_disjoint_dec (range_of_chunk p c)
(p', n')) as [DISJ | OVER].
destruct (alloc_someD AP) as [APA _].
destruct (alloc_someD APx) as [APA' _].
destruct LDAL' as [[r [k [RI RA]]] _].
destruct (ranges_are_disjoint RA APA) as [[-> ->] | DISJ]; try done.
eby elim OVER; eapply disjoint_inside_disjoint.
destruct (load_ptr c mx' p); try done.
destruct LDALX' as [[r [k [RI RA]]] _].
destruct (ranges_are_disjoint RA APA') as [[-> ->] | DISJ]; try done.
eby elim OVER; eapply disjoint_inside_disjoint.
Qed.

forall {c m mx p p' n' k' m' mx'}
(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'),
Proof.
intros.
destruct (ranges_disjoint_dec (range_of_chunk p c)
(p', n')) as [DISJ | OVER].
by rewrite (load_free_other FP RA DISJ),
by rewrite (load_free_overlap FP RA OVER),
Qed.

forall {c m mx p p' k' m' mx'}
(DB: Ptr.block p <> Ptr.block p')
(FP: free_ptr p' k' m = Some m')
(FPx: free_ptr p' k' mx = Some mx'),
Proof.
intros.
destruct (free_someD FP) as [n RA].
destruct (free_someD FPx) as [nx RAx].
[|by destruct p; destruct p'; simpl in *; left].
[|by destruct p; destruct p'; simpl in *; left].
Qed.

# Commutativity properties of memory operations

Allocation commutes over successful stores

Lemma alloc_comm_store:
forall p c v r k m m1 m2 m'
(A : alloc_ptr r k m = Some m1)
(B1: store_ptr c m1 p v = Some m')
(B2: store_ptr c m p v = Some m2),
alloc_ptr r k m2 = Some m'.
Proof.
intros.
pose proof (alloc_someD A) as (? & ? & ? & HA).
destruct (ranges_disjoint_dec (range_of_chunk p c) r) as [DISJ|OVER].
2: by destruct (store_chunk_allocated_someD B2) as [(? & ? & ? & RA) _];
edestruct HA; try eapply RA; eapply ranges_overlap_comm;
eby intro; destruct OVER; eapply disjoint_inside_disjoint.

destruct (alloc_ptr r k m2) as [] _eqn: D; clarify.
2: by destruct (alloc_noneD D) as [|[|(? & ? & RO & RA)]]; clarify;
[by destruct r as [[]]; simpl in *; rewrite (restr_of_store B2) in *
|eby eapply (store_allocated B2) in RA; edestruct HA].

f_equal; eapply mem_eq_ext; red.
rewrite (restr_of_store B1), (restr_of_alloc D),
(restr_of_store B2), (restr_of_alloc A).
split; [|split]; try done.
intros c' p'.
destruct (range_inside_dec (range_of_chunk p' c') r) as [RI | RNI].
rewrite (load_alloc_inside2 D RI); try done.
rewrite <- (load_store_other B1); try done.
2: eby eapply disjoint_inside_disjoint_r.
destruct (ranges_disjoint_dec (range_of_chunk p' c') r) as [DISJ'| OVER].
rewrite (load_alloc_overlap D RNI OVER); symmetry.
Case "ralloc".
intros.
eapply iff_trans, iff_sym, (store_allocated B1).
eapply iff_trans, iff_sym, (alloc_allocated A).
eapply iff_trans; [eapply (alloc_allocated D)|].
by eapply or_iff_compat_r, (store_allocated B2).
Qed.

Allocation commutes over successful allocations

Lemma alloc_comm_alloc:
forall r k r' k' m m1 m2 m'
(A : alloc_ptr r k m = Some m1)
(B1: alloc_ptr r' k' m1 = Some m')
(B2: alloc_ptr r' k' m = Some m2),
alloc_ptr r k m2 = Some m'.
Proof.
intros.
pose proof (alloc_someD A) as (? & ? & ? & HA).
pose proof (alloc_someD B1) as (? & ? & ? & HB1); des.
pose proof (alloc_someD B2) as (? & ? & ? & HB2); des.
destruct (alloc_ptr r k m2) as [] _eqn: D; clarify.
Case "some".
pose proof (alloc_someD D) as (? & _ & _ & HD); des.
f_equal; eapply mem_eq_ext; red.
rewrite (restr_of_alloc B1), (restr_of_alloc D),
(restr_of_alloc B2), (restr_of_alloc A).
repeat split;
try (by intro X; do 2 (
eapply alloc_preserves_allocated_back in X; try edone;
destruct X as [[? ?]|X]; clarify;
eauto using @alloc_preserves_allocated)); [].
destruct (ranges_disjoint_dec r r') as [DISJ|]; [|eby edestruct HD].
intros c' p'.
destruct (range_inside_dec (range_of_chunk p' c') r) as [RI | RNI].
rewrite (load_alloc_inside2 D RI); try done.
2: eby eapply disjoint_inside_disjoint.
destruct (ranges_disjoint_dec (range_of_chunk p' c') r) as [DISJ'| OVER].
rewrite (load_alloc_overlap D RNI OVER); symmetry.

destruct (load_ptr c' m' p') as [] _eqn: X; clarify.
destruct (load_chunk_allocated_someD X) as [(? & ? & ? & ?) ?].
eapply alloc_preserves_allocated_back in H10; try edone.
des; split; vauto.
eby destruct OVER; eapply ranges_disjoint_comm, disjoint_inside_disjoint_r.

Case "none".
pose proof (alloc_noneD D) as [|[|(r'' & k'' & RO & RA)]]; clarify.
- by destruct r as [[]]; destruct r' as [[]]; simpl in *;
rewrite (restr_of_alloc B2) in *.
destruct (alloc_preserves_allocated_back B2 _ _ RA); des; clarify.
- eby edestruct HB1; try eapply ranges_overlap_comm.
eby edestruct HA.
Qed.

Allocation commutes over successful frees

Lemma alloc_comm_free:
forall r k p k' m m1 m2 m'
(A : alloc_ptr r k m = Some m1)
(B1: free_ptr p k' m1 = Some m')
(B2: free_ptr p k' m = Some m2),
alloc_ptr r k m2 = Some m'.
Proof.
intros.
pose proof (alloc_someD A) as (? & ? & ? & HA).
pose proof (free_someD B1) as (n1 & HB1); des.
pose proof (free_someD B2) as (n2 & HB2); des.
destruct (alloc_preserves_allocated_back A _ _ HB1) as [[]|]; clarify.
- edestruct HA; try edone.
by eapply non_empty_same_ptr_overlap;
eauto using @valid_alloc_range_non_empty, @allocated_range_valid.
destruct (alloc_ranges_same HB2 H2) as [? _]; clarify.
destruct (ranges_disjoint_dec r (p, n1)) as [DISJ|]; [|eby edestruct HA].
clear H2.
destruct (alloc_ptr r k m2) as [] _eqn: D; clarify.

Case "some".
pose proof (alloc_someD D) as (? & _ & _ & HD); des.
f_equal; eapply mem_eq_ext; red.
rewrite (restr_of_free B1), (restr_of_alloc D),
(restr_of_free B2), (restr_of_alloc A).
split; [|split]; try done.
intros c' p'.
destruct (range_inside_dec (range_of_chunk p' c') r) as [RI | RNI].
rewrite (load_alloc_inside2 D RI); try done.
2: eby eapply disjoint_inside_disjoint.
destruct (ranges_disjoint_dec (range_of_chunk p' c') r) as [DISJ'| OVER].
eapply load_eq_preserved_by_free_same_size; try eapply B1; try eapply B2; try eassumption.
rewrite (load_alloc_overlap D RNI OVER); symmetry.
destruct (load_ptr c' m' p') as [] _eqn: X; clarify.
destruct (load_chunk_allocated_someD X) as [(? & ? & ? & RA) ?].
eapply free_preserves_allocated_back in RA; try edone.
by split; vauto.
SCase "ralloc".
intros.
eapply iff_trans, iff_sym, (free_allocated B1); try edone.
eapply iff_trans, iff_sym, and_iff_compat_r, (alloc_allocated A).
eapply iff_trans; [eapply (alloc_allocated D)|].
eapply iff_trans; [eby eapply or_iff_compat_r; eapply (free_allocated B2)|].
destruct r0; split; intro; des; clarify; vauto.
split; vauto; simpl; intro; clarify.
edestruct HA; try edone.
by eapply non_empty_same_ptr_overlap;
eauto using @valid_alloc_range_non_empty, @allocated_range_valid.

Case "none".
pose proof (alloc_noneD D) as [|[[]|(r'' & k'' & RO & RA)]]; clarify.
- by destruct r as [[]]; destruct p; simpl; rewrite (restr_of_free B2).
pose proof (free_preserves_allocated_back B2 _ _ RA); des; clarify.
eby edestruct HA.
Qed.

Free commutes over successful stores

Lemma free_comm_store:
forall p c v r k m m1 m2 m'
(A : free_ptr r k m = Some m1)
(B1: store_ptr c m1 p v = Some m')
(B2: store_ptr c m p v = Some m2),
free_ptr r k m2 = Some m'.
Proof.
intros.
pose proof (free_someD A) as (n & RA).
destruct (store_chunk_allocated_someD B1) as [(rr & k' & RI & RA1) _].
destruct (free_ptr r k m2) as [m''|] _eqn: D; clarify.
2: eby eapply (store_allocated B2) in RA; edestruct (free_noneD D).
f_equal; eapply mem_eq_ext; red.
rewrite (restr_of_store B1), (restr_of_free D),
(restr_of_store B2), (restr_of_free A).
split; [|split]; try done.
destruct (ranges_are_disjoint RA (free_preserves_allocated_back A _ _ RA1)) as [[]|DISJ].
+ eby clarify; edestruct (free_not_allocated A).
intros c' p'.
destruct (ranges_disjoint_dec (range_of_chunk p' c')
(r, n)) as [DISJ' | OVER].
erewrite (load_free_other D); try edone; try eby eapply store_allocated.
erewrite (load_free_overlap D); try edone; try eby eapply store_allocated.
Case "ralloc".
intros.
eapply iff_trans, iff_sym, (store_allocated B1).
eapply iff_trans, iff_sym, (free_allocated A RA).
eapply iff_trans, and_iff_compat_r, (store_allocated B2).
eby eapply (free_allocated D), (store_allocated B2).
Qed.

Free commutes over successful allocations

Lemma free_comm_alloc:
forall p k r k' m m1 m2 m'
(A : free_ptr p k m = Some m1)
(B1: alloc_ptr r k' m1 = Some m')
(B2: alloc_ptr r k' m = Some m2),
free_ptr p k m2 = Some m'.
Proof.
intros.
pose proof (free_someD A) as (n & pRA).
pose proof (alloc_someD B1) as (RA' & _ & _ & HB1).
pose proof (alloc_someD B2) as (RA2 & _ & _ & HB).
destruct (free_ptr p k m2) as [m''|] _eqn: D; clarify.
2: eby edestruct (free_noneD D); eapply alloc_preserves_allocated.
f_equal; eapply mem_eq_ext; red.
rewrite (restr_of_alloc B1), (restr_of_free D),
(restr_of_alloc B2), (restr_of_free A).
split; [|split]; try done.
intros c' p'.
destruct (ranges_disjoint_dec (range_of_chunk p' c') (p, n)) as [DISJ' | OVER].
erewrite (load_free_other D); try edone; try eby eapply alloc_preserves_allocated.
erewrite (load_free_overlap D); try edone; try eby eapply alloc_preserves_allocated.
intro.
destruct OVER.
eapply disjoint_inside_disjoint; try edone.
edestruct (ranges_are_disjoint RA2 (alloc_preserves_allocated B2 _ _ pRA)) as [[]|];
clarify.
edestruct HB; try edone.
by eapply non_empty_same_ptr_overlap;
eauto using @valid_alloc_range_non_empty, @allocated_range_valid.
Case "ralloc".
intros.
eapply iff_trans, iff_sym, (alloc_allocated B1); try done.
eapply iff_trans, iff_sym, or_iff_compat_r, (free_allocated A pRA); try done.
eapply iff_trans.
eapply (free_allocated D); try edone; try eby eapply alloc_preserves_allocated.
eapply iff_trans; [eby eapply and_iff_compat_r; eapply (alloc_allocated B2)|].
split; intro; des; clarify; vauto.
split; vauto; intro; clarify.
destruct r; edestruct HB; try edone.
by eapply non_empty_same_ptr_overlap;
eauto using @valid_alloc_range_non_empty, @allocated_range_valid.
Qed.

Free commutes over successful frees

Lemma free_comm_free:
forall p k p' k' m m1 m2 m'
(A : free_ptr p k m = Some m1)
(B1: free_ptr p' k' m1 = Some m')
(B2: free_ptr p' k' m = Some m2),
free_ptr p k m2 = Some m'.
Proof.
intros.
pose proof (free_someD A) as (n & pRA).
pose proof (free_someD B1) as (n' & RA').
assert (NEQ: p <> p') by (intro; clarify; apply (free_not_allocated A _ _ RA')).
destruct (free_preserves_allocated B2 _ _ pRA); des; clarify.
destruct (free_ptr p k m2) as [m''|] _eqn: D.
2: eby edestruct (free_noneD D).
f_equal; eapply mem_eq_ext; red.
rewrite (restr_of_free B1), (restr_of_free D),
(restr_of_free B2), (restr_of_free A).
split; [|split]; try done.
intros c' p''.
destruct (ranges_disjoint_dec (range_of_chunk p'' c') (p, n)) as [DISJ' | OVER].
erewrite (load_free_other D); try edone; try eby eapply alloc_preserves_allocated.
eapply (load_eq_preserved_by_free_same_size); try eapply B1; try eapply B2; try eassumption.
eby eapply free_preserves_allocated_back in RA'.
Case "ralloc".
intros.
eapply iff_trans, iff_sym, (free_allocated B1); try edone.
eapply iff_trans, iff_sym, and_iff_compat_r, (free_allocated A pRA); try done.
eapply iff_trans; [eby eapply (free_allocated D)|].
eapply iff_trans; [eby eapply and_iff_compat_r; eapply (free_allocated B2);
eapply (free_preserves_allocated_back A _ _ RA')|].
tauto.
Qed.

## Simple corollaries

Lemma alloc_comm_alloc_none:
forall r k r' k' m m1 m2
(A : alloc_ptr r k m = Some m1)
(B : alloc_ptr r' k' m1 = None)
(C : alloc_ptr r' k' m = Some m2),
alloc_ptr r k m2 = None.
Proof.
intros; destruct (alloc_ptr r k m2) as [] _eqn: D; clarify.
eby erewrite alloc_comm_alloc in B.
Qed.

Lemma store_comm_alloc:
forall r k c p v m m1 m2
(A : store_ptr c m p v = Some m1)
(B : alloc_ptr r k m1 = Some m2),
exists m', alloc_ptr r k m = Some m' /\ store_ptr c m' p v = Some m2.
Proof.
intros; destruct (alloc_ptr r k m) as [m'|] _eqn: C; clarify.
- repeat eexists; try edone.
destruct (store_ptr c m' p v) as [] _eqn: D.
+ eby erewrite alloc_comm_store in B.
destruct (store_chunk_allocated_someD A) as [(?&?&?&?)?].
destruct (store_chunk_allocated_noneD D); repeat eexists; try edone.
eby eapply alloc_preserves_allocated.
destruct (alloc_someD B) as (? & ? & ? & BB).
destruct (alloc_noneD C); des; clarify.
- by destruct r as [[]]; simpl in *; rewrite (restr_of_store A) in *.
eby edestruct BB; try edone; eapply (store_allocated A).
Qed.

Lemma free_comm_store2:
forall r k c p v m m1 m2
(A : free_ptr r k m = Some m1)
(B : store_ptr c m1 p v = Some m2),
exists m', store_ptr c m p v = Some m' /\ free_ptr r k m' = Some m2.
Proof.
intros; destruct (store_ptr c m p v) as [m'|] _eqn: C; clarify.
- eby repeat eexists; try edone; eapply free_comm_store.
destruct (store_chunk_allocated_someD B) as [(?&?&?&?)?].
destruct (store_chunk_allocated_noneD C); repeat eexists; try edone.
eby eapply (free_preserves_allocated_back A).
Qed.