Require Import VST.veric.juicy_base.
Require Import VST.veric.juicy_mem.
Require Import VST.veric.res_predicates.
Require Import VST.veric.shares.

Definition juicy_mem_core (j: juicy_mem) : rmap := core (m_phi j).

(*Lemma inflate_initial_mem_empty:
  forall lev, emp (inflate_initial_mem Mem.empty lev).
intro lev.
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
unfold inflate_initial_mem.
destruct (make_rmap (inflate_initial_mem' Mem.empty lev) (core (ghost_of lev))
        (inflate_initial_mem'_valid Mem.empty lev) (level lev)
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
        (inflate_initial_mem'_fmap Mem.empty lev)); simpl.
{ rewrite core_ghost_of, <- level_core; apply ghost_of_approx. }
destruct a.
apply resource_at_empty2.
intro l; rewrite H0.
(* Goal: @eq resource (@core resource Join_resource Sep_resource (inflate_initial_mem' m lev loc)) (@core resource Join_resource Sep_resource (resource_at lev loc)) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
unfold inflate_initial_mem'.
destruct l.
unfold access_at; unfold empty at 1.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
simpl.
rewrite PMap.gi.
destruct (max_access_at empty (b,z)); try destruct p; try apply NO_identity.
Qed.
Local Hint Resolve inflate_initial_mem_empty.*)

(* fancy initial mem *)

(* TODO: move this somewhere more appropriate *)
Definition no_VALs (phi: rmap) := forall loc,
  match phi @ loc with
    | YES _ _ (VAL _) _ => False | _ => True
  end.

Lemma components_join_joins {A} {JA: Join A}{PA: Perm_alg A}{TA: Trip_alg A}: forall a b c d,
   join a b c -> joins a d -> joins b d -> joins c d.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: @joins A JA c d *)
destruct H0 as [x ?]. destruct H1 as [y ?].
(* Goal: @joins A JA c d *)
destruct (TA a b d c y x H H1 H0).
(* Goal: @ex preds (fun pp : preds => @eq resource (resource_at w loc) (YES rsh sh (VAL v) pp)) *)
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
eauto.
Qed.

(* coherence lemmas *)

Lemma contents_cohere_join_sub: forall m phi phi',
  contents_cohere m phi -> join_sub phi' phi -> contents_cohere m phi'.
Proof.
(* Goal: forall (m : mem) (phi phi' : rmap) (_ : contents_cohere m phi) (_ : @join_sub rmap Join_rmap phi' phi), contents_cohere m phi' *)
unfold contents_cohere.
(* Goal: forall (m : mem) (phi phi' : rmap) (_ : forall (rsh : Share.t) (sh : readable_share rsh) (v : memval) (loc : AV.address) (pp : preds) (_ : @eq resource (resource_at phi loc) (YES rsh sh (VAL v) pp)), and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP)) (_ : @join_sub rmap Join_rmap phi' phi) (rsh : Share.t) (sh : readable_share rsh) (v : memval) (loc : AV.address) (pp : preds) (_ : @eq resource (resource_at phi' loc) (YES rsh sh (VAL v) pp)), and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
intros until phi'; intros H H0.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
destruct H0 as [phi1 H0].
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
generalize (resource_at_join phi' phi1 phi loc H0); intro H2.
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
rewrite H1 in H2.
inv H2;
symmetry in H8;
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
destruct (H _ _ _ _ _ H8); auto.
Qed.

Lemma perm_of_sh_join_sub: forall (sh1 sh2: Share.t) p,
  perm_of_sh sh1 = Some p ->
  join_sub sh1 sh2 ->
  perm_order' (perm_of_sh sh2) p.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
destruct H0.
(* Goal: perm_order' (perm_of_sh sh2) p *)
unfold perm_of_sh in *.
(* Goal: perm_order' (if writable0_share_dec sh2 then if @eq_dec Share.t Share.EqDec_share sh2 Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec sh2 then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) p *)
repeat if_tac in H; inv H.
+
(* Goal: perm_order' (if writable0_share_dec sh2 then if @eq_dec Share.t Share.EqDec_share sh2 Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec sh2 then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) Freeable *)
inv H0. rewrite Share.glb_commute, Share.glb_top in H; subst x.
(* Goal: perm_order' (if writable0_share_dec (Share.lub Share.top Share.bot) then if @eq_dec Share.t Share.EqDec_share (Share.lub Share.top Share.bot) Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec (Share.lub Share.top Share.bot) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.lub Share.top Share.bot) Share.bot then @None permission else @Some permission Nonempty) Freeable *)
 rewrite (Share.lub_bot).
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) *)
rewrite if_true by auto. rewrite if_true by auto. constructor.
+ apply join_writable01 in H0 ;auto. rewrite if_true by auto.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  if_tac; constructor.
+ apply join_readable1 in H0; auto.
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) *)
  if_tac. if_tac; constructor. rewrite if_true by auto. constructor.
+ assert (sh2 <> Share.bot). contradict H3.
(* Goal: @eq Share.t sh1 Share.bot *)
(* Goal: perm_order' (if writable0_share_dec sh2 then if @eq_dec Share.t Share.EqDec_share sh2 Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec sh2 then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) Nonempty *)
  apply split_identity in H0; auto. apply identity_share_bot; auto.
(* Goal: @eq memval (contents_at m (@pair block Z b ofs')) (@ZMap.get memval ofs (@PMap.get (ZMap.t memval) b (mem_contents m))) *)
(* Goal: forall (n0 : nat) (_ : @eq nat (nat_of_Z (Z.sub ofs' ofs)) (S n0)), @eq memval (contents_at m (@pair block Z b ofs')) (@nth memval n0 (getN n (Z.add ofs (Zpos xH)) (@PMap.get (ZMap.t memval) b (mem_contents m))) Undef) *)
  subst; auto.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  repeat if_tac; try constructor. contradiction.
Qed.

Lemma perm_order'_trans: forall p1 p2 p3,
  perm_order' (Some p1) p2 -> perm_order' (Some p2) p3 -> perm_order' (Some p1) p3.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: perm_order' (@Some permission p1) p3 *)
unfold perm_order' in *.
(* Goal: @ex preds (fun pp : preds => @eq resource (resource_at w loc) (YES rsh sh (VAL v) pp)) *)
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
eapply perm_order_trans; eauto.
Qed.

Lemma rmap_unage_YES: forall phi phi' sh rsh k pp loc, 
  age phi phi' 
  -> phi' @ loc = YES sh rsh k pp 
  -> exists pp', phi @ loc = YES sh rsh k pp'.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: @eq mem (m_dry x) (m_dry y) *)
(* Goal: @eq mem (m_dry x) (m_dry z) *)
unfold age in H.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
case_eq (phi @ loc). intros.
cut (necR phi phi'). intro.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize (necR_NO phi phi' loc sh0 n H2). intro.
rewrite H3 in H1.
(* Goal: perm_order' (if writable0_share_dec sh2 then if @eq_dec Share.t Share.EqDec_share sh2 Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec sh2 then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) Freeable *)
rewrite H1 in H0; inv H0.
constructor; auto.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
exists p.
apply necR_YES with (phi' := phi') in H1.
(* Goal: @eq Z z1 z2 *)
rewrite H1 in H0.
(* Goal: perm_order' (if writable0_share_dec sh2 then if @eq_dec Share.t Share.EqDec_share sh2 Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec sh2 then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) Freeable *)
inv H0. apply YES_ext; auto.
constructor; auto.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
elimtype False.
eapply necR_PURE in H1.
2: constructor 1; eassumption.
congruence.
Qed.

Lemma preds_fmap_NoneP_approx: forall pp lev1 lev2,
  preds_fmap (approx lev1) (approx lev1) pp = NoneP ->
  preds_fmap (approx lev2) (approx lev2) pp = NoneP.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: @eq preds (preds_fmap (approx lev2) (approx lev2) pp) NoneP *)
destruct pp.
(* Goal: @eq preds (preds_fmap (approx lev2) (approx lev2) (SomeP A _f)) NoneP *)
unfold NoneP, approx, compose in *.
(* Goal: Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.sub ofs' ofs) (Zneg p)), Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH))) *)
simpl in *. unfold compose in *.
(* Goal: Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.sub ofs' ofs) (Zneg p)), Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH))) *)
inv H. simpl in *.
(* Goal: @eq preds (SomeP (ConstType unit) (fun i : list Type => _f i)) (SomeP (ConstType unit) (fun i : list Type => _f i)) *)
apply EqdepFacts.eq_sigT_eq_dep in H2.
(* Goal: @eq preds (SomeP (ConstType unit) (fun i : list Type => _f i)) (SomeP (ConstType unit) (fun i : list Type => _f i)) *)
apply Eqdep.EqdepTheory.eq_dep_eq in H2.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
auto.
Qed.

Lemma oracle_unage:
  forall (jm': juicy_mem) (w: rmap), age w (m_phi jm') ->
       exists jm, age jm jm' /\ m_phi jm = w.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm jm') (@eq rmap (m_phi jm) w)) *)
destruct jm' as [m phi' CONTENTS ACCESS MAXA ALLOC].
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
simpl m_phi in H.
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
assert (contents_cohere m w).
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
hnf; intros.
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
destruct (necR_YES'' w phi' loc rsh sh (VAL v)).
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
constructor 1; auto.
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
destruct H1 as [p ?].
(* Goal: @ex preds (fun pp : preds => @eq resource (resource_at w loc) (YES rsh sh (VAL v) pp)) *)
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
eauto.
(* Goal: @ex preds (fun pp : preds => @eq resource (resource_at w loc) (YES rsh sh (VAL v) pp)) *)
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
destruct (CONTENTS _ _ _ _ _ H1); eauto.
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
subst p.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
apply (age1_YES w phi') in H1; auto.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
inversion2 H0 H1. auto.
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
assert (access_cohere m w).
(* Goal: access_cohere m w *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
intro loc; specialize (ACCESS loc).
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
case_eq (w @ loc); intros.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
apply (necR_NO w phi') in H1. rewrite H1 in ACCESS; auto.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
constructor 1;auto.
(* Goal: @eq (option permission) (access_at m loc Cur) (perm_of_res (YES sh r k p)) *)
(* Goal: @eq (option permission) (access_at m loc Cur) (perm_of_res (PURE k p)) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
apply (necR_YES w phi') in H1.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
rewrite H1 in ACCESS; auto.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
constructor 1; auto.
(* Goal: @eq (option permission) (access_at m loc Cur) (perm_of_res (PURE k p)) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
apply (necR_PURE w phi') in H1.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
rewrite H1 in ACCESS; auto.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
constructor 1; auto.
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
assert (max_access_cohere m w).
(* Goal: max_access_cohere m w *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
intro loc; specialize (MAXA loc).
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
case_eq (w @ loc); intros; auto.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
apply (necR_NO w phi') in H2. rewrite H2 in MAXA. auto. constructor 1; auto.
(* Goal: perm_order'' (max_access_at m loc) (perm_of_res' (YES sh r k p)) *)
(* Goal: perm_order'' (max_access_at m loc) (perm_of_res' (PURE k p)) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
apply (necR_YES w phi') in H2.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
rewrite H2 in MAXA; auto.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
constructor 1; auto.
(* Goal: perm_order'' (max_access_at m loc) (perm_of_res' (PURE k p)) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
apply (necR_PURE w phi') in H2.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
rewrite H2 in MAXA; auto.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
constructor 1; auto.
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
assert (alloc_cohere m w).
(* Goal: alloc_cohere m w *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
intros loc ?. specialize (ALLOC _ H3).
(* Goal: @eq resource (resource_at w loc) (NO Share.bot bot_unreadable) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
apply (necR_NO w phi').
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
constructor 1; auto.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
auto.
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
exists (mkJuicyMem m w H0 H1 H2 H3).
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
split; auto.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
apply age1_juicy_mem_unpack''; simpl; auto.
Qed.

(* core load and coherence properties *)

Lemma writable_perm:
  forall b i jm, writable (b,i) (m_phi jm) -> Mem.perm (m_dry jm) b i Cur Writable.
Proof.
(* Goal: forall (b : block) (i : Z) (jm : juicy_mem) (_ : @app_pred rmap ag_rmap (writable (@pair block Z b i)) (m_phi jm)), perm (m_dry jm) b i Cur Writable *)
intros until jm; intros H.
(* Goal: perm (m_dry jm) b i Cur Writable *)
assert (Hacc := juicy_mem_access jm).
(* Goal: perm (m_dry jm) b i Cur Writable *)
unfold access_cohere in Hacc.
(* Goal: perm (m_dry jm) b i Cur Writable *)
unfold Mem.perm, Mem.perm_order'.
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
specialize ( Hacc (b, i)).
(* Goal: @eq nat n (nat_of_Z (Zpos p0)) *)
(* Goal: Z.ge (Zpos p0) Z0 *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub (Zpos p) (Zpos xH)) (Zneg p0)), @eq nat n (nat_of_Z (Zneg p0)) *)
simpl in H.
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
destruct (m_phi jm @ (b, i)).
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
contradiction.
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
destruct H as [H1 H2]. destruct k; inv H2.
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
unfold access_at in Hacc.
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
simpl in Hacc.
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
rewrite Hacc.
(* Goal: match perm_of_sh sh with | Some p' => perm_order p' Writable | None => False end *)
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
clear - H1.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
simpl.
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) *)
unfold perm_of_sh. rewrite if_true by auto. if_tac; constructor.
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
contradiction.
Qed.

Lemma valid_access_None: forall m ch b b' ofs ofs' p,
  Mem.valid_access m ch b ofs p
  -> adr_range (b, ofs) (size_chunk ch) (b', ofs')
  -> access_at m (b', ofs') Cur = None
  -> False.
Proof.
(* Goal: forall (m : mem) (ch : memory_chunk) (b b' : block) (ofs ofs' : Z) (p : permission) (_ : valid_access m ch b ofs p) (_ : adr_range (@pair block Z b ofs) (size_chunk ch) (@pair block Z b' ofs')) (_ : @eq (option permission) (access_at m (@pair block Z b' ofs') Cur) (@None permission)), False *)
unfold access_at, Mem.valid_access, Mem.perm, Mem.range_perm, Mem.perm, Mem.perm_order'.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
simpl.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: False *)
destruct H as [H ?].
(* Goal: False *)
destruct H0 as [H3 H4].
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
subst.
(* Goal: False *)
specialize( H ofs' H4).
(* Goal: @eq (option permission) (perm_of_res (resource_at phi (@pair block Z b ofs))) (@Some permission Freeable) *)
rewrite H1 in H.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
auto.
Qed.

Lemma core_load_getN: forall ch v b ofs bl phi m,
  contents_cohere m phi
  -> (core_load' ch (b, ofs) v bl)%pred phi
  -> bl = Mem.getN (size_chunk_nat ch) ofs (PMap.get b (Mem.mem_contents m)).
Proof.
intros until m; intros H0 H.
destruct H as [[H3 H4] H].
unfold allp, jam in H.
rewrite <- H3.
(* Goal: Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.sub ofs' ofs) (Zneg p)), Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH))) *)
simpl in *.
clear H4.
revert ofs H H3.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
assert (H: size_chunk_nat ch = nat_of_Z (size_chunk ch)) by auto.
rewrite H; clear H.
generalize (size_chunk ch) as z.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
induction bl; intros; simpl; auto.
rewrite IHbl with (ofs := ofs + 1) (z := z - 1); auto.
rewrite Mem.getN_length.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
f_equal; auto.
specialize ( H (b, ofs)).
cut (adr_range (b, ofs) z (b, ofs)); [intro H6|].
destruct (adr_range_dec (b, ofs) z (b, ofs)).
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  2: elimtype False; auto.
(* Goal: @eq nat n (nat_of_Z (Zpos p0)) *)
(* Goal: Z.ge (Zpos p0) Z0 *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub (Zpos p) (Zpos xH)) (Zneg p0)), @eq nat n (nat_of_Z (Zneg p0)) *)
simpl in H.
cut (nat_of_Z (ofs - ofs) = O); [intro H7|].
rewrite H7 in H.
destruct H as [sh [rsh H]].
unfold contents_cohere in H0.
symmetry.
destruct (H0 _ _ _ _ _ H) as [? _].
apply H1.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
replace (ofs - ofs) with 0 by omega; auto.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
unfold adr_range; split; auto.
cut (z > 0). omega.
inversion H3.
cut (z = Z_of_nat (length bl) + 1). omega.
assert (HS_nat_Z: forall n z, S n = nat_of_Z z -> Z_of_nat n + 1 = z).
  intros n z' H4.
  cut (Z_of_nat 1 = 1).
  intro H5.
  rewrite <- H5.
  rewrite <- inj_plus.
  replace (Z_of_nat (n + 1%nat)) with (Z_of_nat (S n)).
(* Goal: Z.le (Zpos xH) (Z.sub ofs' ofs) *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.sub ofs' ofs) (Zneg p)), Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH))) *)
  rewrite H4.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  rewrite Coqlib.nat_of_Z_eq; auto.
  destruct z'; try solve [omega].
  inversion H4.
  rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ in H6.
(* Goal: Z.ge (Zpos p0) Z0 *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub (Zpos p) (Zpos xH)) (Zneg p0)), @eq nat n (nat_of_Z (Zneg p0)) *)
  rewrite Zpos_eq_Z_of_nat_o_nat_of_P.
  rewrite <- H6.
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
  omega.
  simpl in H4.
  inv H4.
  idtac.
  replace (plus n (S 0)) with (S n).
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  auto.
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
  omega.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  auto.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
symmetry; apply HS_nat_Z; auto.
intros loc'.
specialize (H loc').
cut ( adr_range (b, ofs + 1) (z - 1) loc' -> adr_range (b, ofs) z loc').
intro H1.
destruct (adr_range_dec (b, ofs + 1) (z - 1) loc').
destruct (adr_range_dec (b, ofs) z loc').
(* Goal: @eq nat n (nat_of_Z (Zpos p0)) *)
(* Goal: Z.ge (Zpos p0) Z0 *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub (Zpos p) (Zpos xH)) (Zneg p0)), @eq nat n (nat_of_Z (Zneg p0)) *)
simpl in H.
case_eq (nat_of_Z (snd loc' - ofs)).
intro H2.
destruct loc' as (b', ofs').
(* Goal: Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.sub ofs' ofs) (Zneg p)), Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH))) *)
simpl in *.
cut (ofs' > ofs). intro H4.
cut (exists p, ofs' - ofs = Zpos p). intros [p H5].
unfold nat_of_Z in H2.
rewrite H5 in H2.
unfold nat_of_P in H2.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize (le_Pmult_nat p 1) as H6; intro.
rewrite Pmult_nat_mult in H6.
rewrite mult_1_r in H6.
change (Pos.to_nat p) with (Z.to_nat (Z.pos p)) in H6.
rewrite H2 in H6.
(* Goal: @eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (@right (Z.lt ofs hi) (not (Z.lt ofs hi)) n)) true *)
omegaContradiction.
assert (ofs' - ofs > 0).
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
omega.
assert (forall z, z > 0 -> exists p, z = Zpos p).
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
  intros.
  assert (exists n, nat_of_Z z0 = S n).
    exists (nat_of_Z (z0 - 1)).
    destruct z0; try solve [inv H6].
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
    destruct p; auto.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
    simpl.
    change (nat_of_P p~0 = S (nat_of_P (p~0 - 1))).
    rewrite <- nat_of_P_succ_morphism.
    rewrite <- Ppred_minus.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
    simpl.
    rewrite Psucc_o_double_minus_one_eq_xO.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
    auto.
  destruct H7 as [n ?].
  exists (P_of_succ_nat n).
  rewrite Zpos_P_of_succ_nat.
  rewrite <- inj_S.
  rewrite <- H7.
  rewrite Coqlib.nat_of_Z_eq.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  auto.
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
omega.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
apply H6; auto.
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
omega.
intros n H2.
(* Goal: @eq nat n (nat_of_Z (Zpos p0)) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub (Zpos p) (Zpos xH)) (Zneg p0)), @eq nat n (nat_of_Z (Zneg p0)) *)
rewrite H2 in H.
assert (nat_of_Z (snd loc' - (ofs + 1)) = n).
  destruct loc'.
(* Goal: Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.sub ofs' ofs) (Zneg p)), Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH))) *)
  simpl in *.
  assert (Z_of_nat (nat_of_Z (z0 - ofs)) = Z_of_nat (S n)).
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  auto.
  assert (z0 - ofs > 0).
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
    omega.
  rewrite Coqlib.nat_of_Z_eq in H4; try solve [omega].
  replace (z0 - (ofs + 1)) with (z0 - ofs - 1) by omega.
(* Goal: Z.le (Zpos xH) (Z.sub ofs' ofs) *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.sub ofs' ofs) (Zneg p)), Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH))) *)
  rewrite H4.
  destruct n; try solve [simpl; omega].
  replace (Z_of_nat (S (S n)) - 1) with (Z_of_nat (S n)).
  rewrite nat_of_Z_eq.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  auto.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  replace (Z_of_nat (S n)) with (Zpos (P_of_succ_nat n)) by auto.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  replace (Z_of_nat (S (S n))) with (Zpos (P_of_succ_nat (S n))) by auto.
  do 2 rewrite Zpos_P_of_succ_nat.
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
  replace (Z.succ (Z_of_nat (S n)) - 1) with (Z_of_nat (S n)) by omega.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
  simpl.
  rewrite Zpos_P_of_succ_nat.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  auto.
(* Goal: Z.le (Zpos xH) (Z.sub ofs' ofs) *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.sub ofs' ofs) (Zneg p)), Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH))) *)
rewrite H4.
apply H.
elimtype False. auto.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
auto.
unfold adr_range.
destruct loc' as (b', ofs').
intros [H1 H2].
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
split; auto || omega.
inversion H3.
assert (z > 0).
  assert (forall n z, S n = nat_of_Z z -> z > 0).
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
    intros.
    destruct z0; try solve [inv H1].
    apply Zgt_pos_0.
(* Goal: @ex preds (fun pp : preds => @eq resource (resource_at w loc) (YES rsh sh (VAL v) pp)) *)
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
  eapply H1; eauto.
assert (z - 1 >= 0).
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
omega.
assert (Z_of_nat (S (length bl)) = Z_of_nat (nat_of_Z z)).
rewrite Coqlib.nat_of_Z_eq; try solve [omega].
(* Goal: @eq resource (@core resource Join_resource Sep_resource match access_at m loc Cur with | Some (Freeable as p0) => YES Share.top readable_share_top (VAL (contents_at m loc)) NoneP | Some (Writable as p0) => YES Ews (@writable_readable Ews writable_Ews) (VAL (contents_at m loc)) NoneP | Some (Readable as p0) => YES Ers readable_Ers (VAL (contents_at m loc)) NoneP | Some (Nonempty as p0) => PURE k p | None => NO Share.bot bot_unreadable end) (@core resource Join_resource Sep_resource (PURE k p)) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
rewrite H2.
rewrite Coqlib.nat_of_Z_eq; try solve [omega].
rewrite Coqlib.nat_of_Z_eq in H5; try solve [omega].
rewrite <- H5.
rewrite inj_S.
assert (forall z, Z.succ z - 1 = z) by (intros; omega).
(* Goal: Z.le (Zpos xH) (Zpos p) *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.sub ofs' ofs) (Zneg p)), Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH))) *)
rewrite H6.
rewrite nat_of_Z_eq.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
auto.
Qed.

Lemma core_load_valid: forall ch v b ofs m phi,
  (core_load ch (b, ofs) v)%pred phi
  -> access_cohere m phi
  -> Mem.valid_access m ch b ofs Readable.
Proof.
intros until phi; intros H H0.
hnf in H.
destruct H as [bl [[H1 [H2 Halign]] H]].
hnf in H.
(* Goal: and (@eq bool (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) true) (@eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) true) *)
split.
intros ofs' H4.
specialize (H (b, ofs')).
hnf in H.
destruct (adr_range_dec (b, ofs) (size_chunk ch) (b, ofs')) as [H5|H5].
  2: unfold adr_range in H5.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  2: elimtype False; apply H5; split; auto.
destruct H as [sh [rsh H]].
(* Goal: @eq nat n (nat_of_Z (Zpos p0)) *)
(* Goal: Z.ge (Zpos p0) Z0 *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub (Zpos p) (Zpos xH)) (Zneg p0)), @eq nat n (nat_of_Z (Zneg p0)) *)
simpl in H.
unfold access_cohere in H0.
specialize (H0 (b, ofs')).
(* Goal: perm (m_dry jm) b i Cur Writable *)
unfold Mem.perm, Mem.perm_order'.
(* Goal: @eq resource (resource_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) match k with | VAL m => if readable_perm (access_at m' loc Cur) then YES sh r (VAL (contents_at m' loc)) NoneP else NO Share.bot bot_unreadable | LK n i => YES sh r k p | FUN f c => YES sh r k p end) match k with | VAL m => if readable_perm (access_at m' loc Cur) then YES sh r (VAL (contents_at m' loc)) NoneP else NO Share.bot bot_unreadable | LK n i => YES sh r k p | FUN f c => YES sh r k p end *)
(* Goal: @eq resource (resource_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) (PURE k p)) (PURE k p) *)
(* Goal: @eq ghost (ghost_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) (ghost_of (m_phi jm))) (ghost_of (m_phi jm)) *)
rewrite H in H0.
unfold access_at in H0.  simpl in H0.
destruct ((mem_access m) !! b ofs' Cur).
clear - H0 rsh.
unfold perm_of_sh in H0.
if_tac in H0.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
if_tac in H0; inv H0; constructor.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
rewrite if_true in H0. inv H0; constructor.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
auto.
clear - rsh H0.
unfold perm_of_sh in H0.
(* Goal: perm_order' (if writable0_share_dec sh2 then if @eq_dec Share.t Share.EqDec_share sh2 Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec sh2 then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) Freeable *)
repeat if_tac in H0; inv H0.
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
contradiction.
assumption.
Qed.

Lemma core_load_load': forall ch b ofs v m,
  core_load ch (b, ofs) v (m_phi m) -> Mem.load ch (m_dry m) b ofs = Some v.
Proof.
intros until m; intros H.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize H as Hcore_load; intro.
Transparent Mem.load.
unfold core_load in H; unfold Mem.load.
unfold allp, jam in H.
destruct H as [bl [[H0 [H1 Halign]] H]].
assert (H3 := juicy_mem_contents m).
pose proof I.
pose proof I.
(* Goal: perm_order'' (@Some permission Writable) (if writable0_share_dec (Share.glb Share.Rsh sh) then if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
if_tac.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) (@fst block Z loc) (mem_access m) (@snd block Z loc) k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) (@fst block Z loc) (mem_access m') (@snd block Z loc) k) *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
f_equal.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize (core_load_getN ch v b ofs bl (m_phi m) (m_dry m) H3) as H7; intro.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
rewrite <- H7; auto.
unfold core_load'.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
repeat split; auto.
elimtype False.
apply H5.
(* Goal: @ex preds (fun pp : preds => @eq resource (resource_at w loc) (YES rsh sh (VAL v) pp)) *)
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
eapply core_load_valid; eauto.
apply juicy_mem_access.
Qed.

Lemma Zminus_lem: forall z1 z2, z1 <= z2 -> nat_of_Z (z2 - z1) = O -> z1=z2.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
case_eq (z2 - z1). intro.
(* Goal: @eq Z z1 z2 *)
rewrite H1 in H0.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
symmetry; apply Zminus_eq; auto.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize (lt_O_nat_of_P p). intro.
(* Goal: @eq Z z1 z2 *)
rewrite H1 in H0.
(* Goal: Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.sub ofs' ofs) (Zneg p)), Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH))) *)
simpl in *.
(* Goal: @eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (@right (Z.lt ofs hi) (not (Z.lt ofs hi)) n)) true *)
omegaContradiction.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize (Zlt_neg_0 p). intro.
(* Goal: @eq Z z1 z2 *)
rewrite H1 in H0.
(* Goal: @eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (@right (Z.lt ofs hi) (not (Z.lt ofs hi)) n)) true *)
omegaContradiction.
Qed.

Lemma nat_of_Z_lem1: forall n z, S n = nat_of_Z z -> n = nat_of_Z (z - 1).
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: @eq nat n (nat_of_Z (Z.sub z (Zpos xH))) *)
destruct z; try solve [inv H].
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize (lt_O_nat_of_P p). intro.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
case_eq (Zpos p - 1). intro.
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
assert (Zpos p = 1) by omega.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
rewrite H2 in H. auto.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
assert (Zpos p = Zpos p0 + 1) by omega.
(* Goal: @eq nat n (nat_of_Z (Zpos p0)) *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub (Zpos p) (Zpos xH)) (Zneg p0)), @eq nat n (nat_of_Z (Zneg p0)) *)
rewrite H2 in H.
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
rewrite nat_of_Z_plus in H; try omega.
(* Goal: @eq nat n (nat_of_Z (Zpos p0)) *)
(* Goal: Z.ge (Zpos p0) Z0 *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub (Zpos p) (Zpos xH)) (Zneg p0)), @eq nat n (nat_of_Z (Zneg p0)) *)
simpl in H.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
simpl.
assert (forall m n, S m = n + 1 -> m = n)%nat.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
  intros. omega.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
apply H3; auto.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize (lt_O_nat_of_P p0). intro.
(* Goal: Z.ge (Zpos p0) Z0 *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub (Zpos p) (Zpos xH)) (Zneg p0)), @eq nat n (nat_of_Z (Zneg p0)) *)
rewrite Zpos_eq_Z_of_nat_o_nat_of_P.
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
omega.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
assert (Zpos p = Zneg p0 + 1) by omega.
(* Goal: @eq nat n (nat_of_Z (Zneg p0)) *)
assert (Zpos p > 0) by (rewrite Zpos_eq_Z_of_nat_o_nat_of_P; omega).
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize (Zlt_neg_0 p0). intro.
(* Goal: @eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (@right (Z.lt ofs hi) (not (Z.lt ofs hi)) n)) true *)
omegaContradiction.
Qed.

Lemma nat_of_Z_lem2: forall n z1 z2, S n = nat_of_Z (z1 - z2) -> n = nat_of_Z (z1 - z2 - 1).
Proof. intros; apply nat_of_Z_lem1; auto. Qed.

Lemma nth_getN: forall m b ofs ofs' z,
  ofs <= ofs' < ofs + z
  -> z >= 0
  -> contents_at m (b, ofs')
  = nth (nat_of_Z (ofs' - ofs)) (Mem.getN (nat_of_Z z) ofs (PMap.get b (Mem.mem_contents m))) Undef.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: @eq memval (contents_at m (@pair block Z b ofs')) (@nth memval (nat_of_Z (Z.sub ofs' ofs)) (getN (nat_of_Z z) ofs (@PMap.get (ZMap.t memval) b (mem_contents m))) Undef) *)
revert ofs ofs' H H0.
(* Goal: forall (ofs ofs' : Z) (_ : and (Z.le ofs ofs') (Z.lt ofs' (Z.add ofs z))) (_ : Z.ge z Z0), @eq memval (contents_at m (@pair block Z b ofs')) (@nth memval (nat_of_Z (Z.sub ofs' ofs)) (getN (nat_of_Z z) ofs (@PMap.get (ZMap.t memval) b (mem_contents m))) Undef) *)
remember (nat_of_Z z) as n.
(* Goal: forall (ofs ofs' : Z) (_ : and (Z.le ofs ofs') (Z.lt ofs' (Z.add ofs z))) (_ : Z.ge z Z0), @eq memval (contents_at m (@pair block Z b ofs')) (@nth memval (nat_of_Z (Z.sub ofs' ofs)) (getN n ofs (@PMap.get (ZMap.t memval) b (mem_contents m))) Undef) *)
revert n z Heqn.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
induction n; intros.
(* Goal: @eq memval (contents_at m (@pair block Z b ofs')) (@nth memval (nat_of_Z (Z.sub ofs' ofs)) (getN O ofs (@PMap.get (ZMap.t memval) b (mem_contents m))) Undef) *)
(* Goal: @eq memval (contents_at m (@pair block Z b ofs')) (@nth memval (nat_of_Z (Z.sub ofs' ofs)) (getN (S n) ofs (@PMap.get (ZMap.t memval) b (mem_contents m))) Undef) *)
destruct z.
(* Goal: @eq (option permission) (perm_of_res (resource_at phi (@pair block Z b ofs))) (@Some permission Freeable) *)
inv H.
(* Goal: @eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (@right (Z.lt ofs hi) (not (Z.lt ofs hi)) n)) true *)
omegaContradiction.
(* Goal: Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.sub ofs' ofs) (Zneg p)), Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH))) *)
simpl in *.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize (lt_O_nat_of_P p). intro.
(* Goal: @eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (@right (Z.lt ofs hi) (not (Z.lt ofs hi)) n)) true *)
omegaContradiction.
(* Goal: Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH))) *)
generalize (Zlt_neg_0 p).
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
intro.
(* Goal: @eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (@right (Z.lt ofs hi) (not (Z.lt ofs hi)) n)) true *)
omegaContradiction.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
simpl.
(* Goal: @eq memval (contents_at m (@pair block Z b ofs')) match nat_of_Z (Z.sub ofs' ofs) with | O => @ZMap.get memval ofs (@PMap.get (ZMap.t memval) b (mem_contents m)) | S m0 => @nth memval m0 (getN n (Z.add ofs (Zpos xH)) (@PMap.get (ZMap.t memval) b (mem_contents m))) Undef end *)
case_eq (nat_of_Z (ofs' - ofs)).
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: @eq memval (contents_at m (@pair block Z b ofs')) (@ZMap.get memval ofs (@PMap.get (ZMap.t memval) b (mem_contents m))) *)
(* Goal: forall (n0 : nat) (_ : @eq nat (nat_of_Z (Z.sub ofs' ofs)) (S n0)), @eq memval (contents_at m (@pair block Z b ofs')) (@nth memval n0 (getN n (Z.add ofs (Zpos xH)) (@PMap.get (ZMap.t memval) b (mem_contents m))) Undef) *)
assert (ofs = ofs').
(* Goal: @eq Share.t sh Share.top *)
  destruct H.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  apply Zminus_lem; auto.
(* Goal: @eq memval (contents_at m (@pair block Z b ofs')) (@ZMap.get memval ofs (@PMap.get (ZMap.t memval) b (mem_contents m))) *)
(* Goal: forall (n0 : nat) (_ : @eq nat (nat_of_Z (Z.sub ofs' ofs)) (S n0)), @eq memval (contents_at m (@pair block Z b ofs')) (@nth memval n0 (getN n (Z.add ofs (Zpos xH)) (@PMap.get (ZMap.t memval) b (mem_contents m))) Undef) *)
subst; auto.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: @eq memval (contents_at m (@pair block Z b ofs')) (@nth memval n0 (getN n (Z.add ofs (Zpos xH)) (@PMap.get (ZMap.t memval) b (mem_contents m))) Undef) *)
symmetry in H1.
(* Goal: @eq memval (contents_at m (@pair block Z b ofs')) (@nth memval n0 (getN n (Z.add ofs (Zpos xH)) (@PMap.get (ZMap.t memval) b (mem_contents m))) Undef) *)
assert (n = nat_of_Z (z - 1)) by (apply nat_of_Z_lem1 in Heqn; auto).
rewrite (IHn (z - 1) H2 (ofs + 1)); try solve [auto|omega].
assert (nat_of_Z (ofs' - (ofs + 1)) = n0).
replace (ofs' - (ofs + 1)) with (ofs' - ofs - 1) by omega.
(* Goal: @eq nat (nat_of_Z (Z.sub (Z.sub ofs' ofs) (Zpos xH))) n0 *)
(* Goal: @eq memval (@nth memval (nat_of_Z (Z.sub ofs' (Z.add ofs (Zpos xH)))) (getN n (Z.add ofs (Zpos xH)) (@PMap.get (ZMap.t memval) b (mem_contents m))) Undef) (@nth memval n0 (getN n (Z.add ofs (Zpos xH)) (@PMap.get (ZMap.t memval) b (mem_contents m))) Undef) *)
(* Goal: and (Z.le (Z.add ofs (Zpos xH)) ofs') (Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH)))) *)
  apply nat_of_Z_lem1 in H1.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  auto.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
rewrite H3; auto.
(* Goal: @eq Share.t sh Share.top *)
destruct H.
(* Goal: and (@eq bool (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) true) (@eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) true) *)
split.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
case_eq (ofs' - ofs). intro. rewrite H4 in H1.
(* Goal: Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.sub ofs' ofs) (Zneg p)), Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH))) *)
simpl in *. inv H1.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros. rewrite H4 in H1. simpl in *.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize (lt_O_nat_of_P p). intro.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
cut (1 <= ofs' - ofs). intro. omega.
(* Goal: Z.le (Zpos xH) (Z.sub ofs' ofs) *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.sub ofs' ofs) (Zneg p)), Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH))) *)
rewrite H4.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize (Zpos_eq_Z_of_nat_o_nat_of_P p). intro. rewrite H6.
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
omega.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize (Zlt_neg_0 p). intro.
(* Goal: @eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (@right (Z.lt ofs hi) (not (Z.lt ofs hi)) n)) true *)
omegaContradiction.
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
omega.
Qed.

Lemma load_core_load: forall ch b ofs v m,
  Mem.load ch (m_dry m) b ofs = Some v ->
  (forall z, ofs <= z < ofs + size_chunk ch ->
                      perm_order'' (perm_of_res (m_phi m @ (b,z))) (Some Readable)) ->
 core_load ch (b, ofs) v (m_phi m).
Proof.
intros until m; intros H PERM.
hnf.
unfold Mem.load in H.

if_tac in H; try solve [inv H].
inversion H.
clear H.
exists (Mem.getN (size_chunk_nat ch) ofs (PMap.get b (Mem.mem_contents (m_dry m)))).
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize H0 as H0'; intro.
Local Hint Resolve Mem.getN_length.
unfold Mem.valid_access in H0'.
destruct H0' as [H0'1 H0'2].
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
repeat split; auto.
clear H0'1 H0'2.
intros (b', ofs').
hnf.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
if_tac; hnf; auto.
assert (Heqbb': b = b').
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  unfold adr_range in H. decompose [and] H. auto.
pose proof (juicy_mem_contents m).
pose proof I. (* pose proof (juicy_mem_access m).*)
pose proof I.
pose proof I.
clear H4. subst b'; clear H5.
destruct H as [_ ?].
specialize (PERM ofs' H).
(*
unfold access_cohere in H3.
specialize (H3 (b, ofs').
*)
unfold perm_of_res in *.
destruct H0 as [H0 _].
specialize (H0 ofs').
specialize (H0 H).
hnf in H0.
(*unfold access_at in H3.
simpl in H3.
*)
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
destruct ((mem_access (m_dry m)) !! b ofs' Cur); try contradiction.
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
destruct (m_phi m @ (b, ofs')) eqn:H8; try contradiction.
if_tac in PERM; inv PERM.
destruct k; try now inv PERM.
pose proof (size_chunk_pos ch).
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
rewrite <- nth_getN with (ofs := ofs) (z := size_chunk ch); auto; try omega.
exists sh, r.
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
destruct (H1 _ _ _ _ _ H8); subst.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) (@fst block Z loc) (mem_access m) (@snd block Z loc) k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) (@fst block Z loc) (mem_access m') (@snd block Z loc) k) *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
f_equal.
inv PERM.
Qed.

Lemma core_load_load: forall ch b ofs v m,
  (forall z, ofs <= z < ofs + size_chunk ch ->
                      perm_order'' (perm_of_res (m_phi m @ (b,z))) (Some Readable)) ->
  (core_load ch (b, ofs) v (m_phi m) <-> Mem.load ch (m_dry m) b ofs = Some v).
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: iff (@app_pred rmap ag_rmap (core_load ch (@pair block Z b ofs) v) (m_phi m)) (@eq (option val) (load ch (m_dry m) b ofs) (@Some val v)) *)
split; [apply core_load_load'| ].
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
intros; apply load_core_load; auto.
Qed.

(*Lemma address_mapsto_exists':
  forall ch v sh (rsh: readable_share sh) loc m lev,
      (align_chunk ch | snd loc)
      -> Mem.load ch m (fst loc) (snd loc) = Some v 
      -> exists w, address_mapsto ch v sh loc w /\ level w = lev.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros. rename H into Halign.
unfold address_mapsto.
pose (f l' := if adr_range_dec loc (size_chunk ch) l'
                     then YES sh rsh (VAL (nthbyte (snd l' - snd loc) (Mem.getN (size_chunk_nat ch) (snd loc) (PMap.get (fst loc) (Mem.mem_contents m))))) NoneP
                     else NO Share.bot bot_unreadable).
assert (CompCert_AV.valid (res_option oo f)).
apply VAL_valid.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
unfold compose, f; intros.
if_tac in H.
(* Goal: @eq nat n (nat_of_Z (Zpos p0)) *)
(* Goal: Z.ge (Zpos p0) Z0 *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub (Zpos p) (Zpos xH)) (Zneg p0)), @eq nat n (nat_of_Z (Zneg p0)) *)
simpl in H.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
injection H;intros; subst k; auto.
(* Goal: @eq (option permission) (perm_of_res (resource_at phi (@pair block Z b ofs))) (@Some permission Freeable) *)
inv H.
destruct (make_rmap f H lev) as [phi [? ?]].
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
extensionality l; unfold f, compose; simpl.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
if_tac; hnf; auto.
exists phi.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
split; auto.
exists (Mem.getN (size_chunk_nat ch) (snd loc) (PMap.get (fst loc) (Mem.mem_contents m))).
(* Goal: and (@eq bool (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) true) (@eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) true) *)
split.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
repeat split; auto.
Transparent Mem.load.
(* Goal: perm_order' (if writable0_share_dec sh2 then if @eq_dec Share.t Share.EqDec_share sh2 Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec sh2 then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) Freeable *)
unfold load in *. if_tac in H0. injection H0. auto. inv H0.
intro l'.
unfold jam.
hnf.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
simpl.
rewrite H2; clear H H1 H2.
unfold f; clear f.
(* Goal: perm_order'' (@Some permission Writable) (if writable0_share_dec (Share.glb Share.Rsh sh) then if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
if_tac.
exists rsh.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) (@fst block Z loc) (mem_access m) (@snd block Z loc) k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) (@fst block Z loc) (mem_access m') (@snd block Z loc) k) *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
f_equal. 
apply NO_identity.
Qed.*)
    
Lemma mapsto_valid_access: forall ch v sh b ofs jm,
  (address_mapsto ch v sh (b, ofs) * TT)%pred (m_phi jm)
  -> Mem.valid_access (m_dry jm) ch b ofs Readable.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
unfold address_mapsto in H.
unfold Mem.valid_access, Mem.range_perm.
(* Goal: and (@eq bool (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) true) (@eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) true) *)
split.
destruct H as [x [y [Hjoin ?]]].
destruct H as [[bl [[[H2 [H3 H3']] H] Hg]] ?].
hnf in H.
intros ofs' H4.
specialize (H (b, ofs')).
hnf in H.
destruct (adr_range_dec (b, ofs) (size_chunk ch) (b, ofs')) as [H5|H5].
  2: unfold adr_range in H5.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  2: elimtype False; apply H5; split; auto.
hnf in H.
destruct H as [pf H].
hnf in H.
rewrite preds_fmap_NoneP in H.
(* Goal: @eq nat n (nat_of_Z (Zpos p0)) *)
(* Goal: Z.ge (Zpos p0) Z0 *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub (Zpos p) (Zpos xH)) (Zneg p0)), @eq nat n (nat_of_Z (Zneg p0)) *)
simpl in H.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize (resource_at_join _ _ _ (b,ofs') Hjoin); rewrite H; intro.
forget ((nth (nat_of_Z (ofs' - ofs)) bl Undef)) as v'.
assert (exists rsh', exists sh', m_phi jm @ (b,ofs') = YES rsh' sh' (VAL v') NoneP).
(* Goal: @ex preds (fun pp : preds => @eq resource (resource_at w loc) (YES rsh sh (VAL v) pp)) *)
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
inv H1; eauto.
destruct H6 as [rsh' [sh' ?]].
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize (juicy_mem_access jm (b,ofs')); rewrite H6; unfold perm_of_res; simpl; intro.
clear - H7 sh'.
unfold perm, access_at in *.
simpl in H7.
forget ((mem_access (m_dry jm)) !! b ofs' Cur) as p1.
unfold perm_of_sh in H7.
if_tac in H7.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
if_tac in H7; inv H7; constructor.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
rewrite if_true in H7 by auto.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
subst; constructor.
repeat match goal with [ H: context[ _ /\ _ ] |- _] => destruct H end.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
auto.
Qed.

Lemma mapsto_valid_access_wr: forall ch v sh (wsh: writable0_share sh) b ofs jm,
  (address_mapsto ch v sh (b, ofs) * TT)%pred (m_phi jm)
  -> Mem.valid_access (m_dry jm) ch b ofs Writable.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
unfold address_mapsto in H.
unfold Mem.valid_access, Mem.range_perm.
(* Goal: and (@eq bool (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) true) (@eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) true) *)
split.
destruct H as [x [y [Hjoin ?]]].
destruct H as [[bl [[[H2 [H3 H3']] H] Hg]] ?].
hnf in H.
intros ofs' H4.
specialize (H (b, ofs')).
hnf in H.
destruct (adr_range_dec (b, ofs) (size_chunk ch) (b, ofs')) as [H5|H5].
  2: unfold adr_range in H5.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  2: elimtype False; apply H5; split; auto.
hnf in H.
destruct H as [pf H].
hnf in H.
rewrite preds_fmap_NoneP in H.
(* Goal: @eq nat n (nat_of_Z (Zpos p0)) *)
(* Goal: Z.ge (Zpos p0) Z0 *)
(* Goal: forall (p0 : positive) (_ : @eq Z (Z.sub (Zpos p) (Zpos xH)) (Zneg p0)), @eq nat n (nat_of_Z (Zneg p0)) *)
simpl in H.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize (resource_at_join _ _ _ (b,ofs') Hjoin); rewrite H; intro.
forget ((nth (nat_of_Z (ofs' - ofs)) bl Undef)) as v'.
assert (exists sh' (wsh': writable0_share sh'), m_phi jm @ (b,ofs') = YES sh' (writable0_readable wsh') (VAL v') NoneP).
inv H1; [ | contradiction (join_writable0_readable RJ wsh rsh2)].
exists sh3, (join_writable01 RJ wsh).
apply YES_ext; auto.
destruct H6 as [sh' [wsh' ?]].
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize (juicy_mem_access jm (b,ofs')); rewrite H6; unfold perm_of_res; simpl; intro.
clear - H7 wsh'.
unfold perm, access_at in *.
simpl in H7.
forget ((mem_access (m_dry jm)) !! b ofs' Cur) as p1.
unfold perm_of_sh in H7.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
rewrite if_true in H7 by auto.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
subst. if_tac; constructor.
repeat match goal with [ H: context[ _ /\ _ ] |- _] => destruct H end.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
auto.
Qed.

Program Definition mapsto_can_store_definition ch v sh (wsh: writable0_share sh) b ofs jm (v':val)
  (MAPSTO: (address_mapsto ch v sh (b, ofs) * TT)%pred (m_phi jm)):
  Memory.mem. 
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
Proof. intros.
(* Goal: mem *)
pose proof (mapsto_valid_access_wr _ _ _ wsh _ _ _ MAPSTO).
apply (mkmem
  (PMap.set b (setN (encode_val ch v') ofs (PMap.get b (mem_contents (m_dry jm))))
    (mem_contents (m_dry jm))) (mem_access (m_dry jm))
  (nextblock (m_dry jm)) (access_max (m_dry jm)) (nextblock_noaccess (m_dry jm))).
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros. destruct jm; simpl.
(* Goal: @eq memval (@fst memval (PTree.t memval) (@PMap.get (ZMap.t memval) b0 (@PMap.set (ZMap.t memval) b (setN (encode_val ch v') ofs (@PMap.get (ZMap.t memval) b (mem_contents m))) (mem_contents m)))) Undef *)
  rewrite PMap.gsspec. destruct (peq b0 b).
(* Goal: @eq memval (@fst memval (PTree.t memval) (setN (encode_val ch v') ofs (@PMap.get (ZMap.t memval) b (mem_contents m)))) Undef *)
(* Goal: @eq memval (@fst memval (PTree.t memval) (@PMap.get (ZMap.t memval) b0 (mem_contents m))) Undef *)
  rewrite setN_default. apply contents_default.
(* Goal: @eq memval (@fst memval (PTree.t memval) (@PMap.get (ZMap.t memval) b0 (mem_contents m))) Undef *)
  apply contents_default.
Defined.

Lemma mapsto_can_store_property: forall (ch:memory_chunk) v sh (wsh: writable0_share sh) b ofs jm v'
  (MAPSTO: (address_mapsto ch v sh (b, ofs) * TT)%pred (m_phi jm)),
  Mem.store ch (m_dry jm) b ofs v' = 
  Some(mapsto_can_store_definition _ _ _ wsh _ _ jm v' MAPSTO).
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: mem *)
pose proof (mapsto_valid_access_wr _ _ _ wsh _ _ _ MAPSTO).
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
unfold mapsto_can_store_definition. simpl.
Transparent Mem.store. unfold store.
destruct (valid_access_dec (m_dry jm) ch b ofs Writable).
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) (@fst block Z loc) (mem_access m) (@snd block Z loc) k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) (@fst block Z loc) (mem_access m') (@snd block Z loc) k) *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
f_equal. f_equal; auto with extensionality.
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
contradiction.
Opaque Mem.store.
Qed.

Lemma mapsto_can_store: forall ch v sh (wsh: writable0_share sh) b ofs jm v',
  (address_mapsto ch v sh (b, ofs) * TT)%pred (m_phi jm)
  -> exists m', Mem.store ch (m_dry jm) b ofs v' = Some m'.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: @ex mem (fun m' : mem => @eq (option mem) (store ch (m_dry jm) b ofs v') (@Some mem m')) *)
exists (mapsto_can_store_definition _ _ _ wsh _ _ jm v' H).
(* Goal: @eq (option mem) (store ch (m_dry jm) b ofs v') (@Some mem (mapsto_can_store_definition ch v sh wsh b ofs jm v' H)) *)
apply mapsto_can_store_property.
Qed.

Lemma store_outside':
   forall ch m b z v m',
          Mem.store ch m b z v = Some m' ->
  (forall b' ofs,
    (b=b' /\ z <= ofs < z + size_chunk ch) \/
     contents_at m (b', ofs) = contents_at m' (b', ofs))
  /\ access_at m = access_at m'
  /\ Mem.nextblock m = Mem.nextblock m'.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: and (@eq bool (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) true) (@eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) true) *)
repeat split.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
generalize (Mem.store_mem_contents _ _ _ _ _ _ H); intro.
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
destruct (eq_block b b').
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
subst b'.
assert (z <= ofs < z + size_chunk ch \/ (ofs < z \/ ofs >= z + size_chunk ch)) by omega.
(* Goal: @eq resource (@core resource Join_resource Sep_resource match access_at m loc Cur with | Some (Freeable as p0) => YES Share.top readable_share_top (VAL (contents_at m loc)) NoneP | Some (Writable as p0) => YES Ews (@writable_readable Ews writable_Ews) (VAL (contents_at m loc)) NoneP | Some (Readable as p0) => YES Ers readable_Ers (VAL (contents_at m loc)) NoneP | Some (Nonempty as p0) => PURE k p | None => NO Share.bot bot_unreadable end) (@core resource Join_resource Sep_resource (PURE k p)) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
destruct H1.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
left; auto.
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
right.
(* Goal: @eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs)) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
unfold contents_at; rewrite H0; clear H0.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
simpl.
(* Goal: @eq memval (@ZMap.get memval ofs (@PMap.get (ZMap.t memval) b (mem_contents m))) (@ZMap.get memval ofs (@PMap.get (ZMap.t memval) b (@PMap.set (ZMap.t memval) b (setN (encode_val ch v) z (@PMap.get (ZMap.t memval) b (mem_contents m))) (mem_contents m)))) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
rewrite PMap.gss.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
rewrite Mem.setN_other; auto.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
rewrite encode_val_length in H0.
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
rewrite <- size_chunk_conv in H0.
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
destruct H0.
(* Goal: @eq resource (@core resource Join_resource Sep_resource match access_at m loc Cur with | Some (Freeable as p0) => YES Share.top readable_share_top (VAL (contents_at m loc)) NoneP | Some (Writable as p0) => YES Ews (@writable_readable Ews writable_Ews) (VAL (contents_at m loc)) NoneP | Some (Readable as p0) => YES Ers readable_Ers (VAL (contents_at m loc)) NoneP | Some (Nonempty as p0) => PURE k p | None => NO Share.bot bot_unreadable end) (@core resource Join_resource Sep_resource (PURE k p)) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
destruct H1.
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
omega.
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
omega.
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
right.
(* Goal: @eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs)) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
unfold contents_at; rewrite H0; clear H0.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
simpl.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
rewrite PMap.gso by auto. auto.
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
unfold access_at.  extensionality loc k.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) (@fst block Z loc) (mem_access m) (@snd block Z loc) k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) (@fst block Z loc) (mem_access m') (@snd block Z loc) k) *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
f_equal.
(* Goal: @ex preds (fun pp : preds => @eq resource (resource_at w loc) (YES rsh sh (VAL v) pp)) *)
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
symmetry; eapply Mem.store_access; eauto.
(* Goal: @ex preds (fun pp : preds => @eq resource (resource_at w loc) (YES rsh sh (VAL v) pp)) *)
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
symmetry; eapply Mem.nextblock_store; eauto.
Qed.

Lemma adr_range_zle_zlt : forall  b lo hi ofs,
  adr_range (b,lo) (hi-lo) (b,ofs)
  -> zle lo ofs && zlt ofs hi = true.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: @eq bool (andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi))) true *)
destruct H as [H [H1 H2]].
(* Goal: @eq bool (andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi))) true *)
rewrite andb_true_iff.
(* Goal: and (@eq bool (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) true) (@eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) true) *)
split.
(* Goal: @eq bool (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) true *)
(* Goal: @eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) true *)
unfold zle.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
case_eq (Z_le_gt_dec lo ofs); intros; auto.
(* Goal: @eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) true *)
unfold zlt.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
case_eq (Z_lt_dec ofs hi); intros; auto.
(* Goal: @eq bool (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (@right (Z.lt ofs hi) (not (Z.lt ofs hi)) n)) true *)
omegaContradiction.
Qed.

Lemma join_top: forall sh2 sh, join Share.top sh2 sh -> sh = Share.top.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros. destruct H. rewrite Share.lub_commute, Share.lub_top in H0. auto.
Qed.

Lemma juicy_free_aux_lemma:
 forall phi b lo hi F,
 app_pred (VALspec_range (hi-lo) Share.top (b,lo) * F) phi ->
  (forall ofs : Z,
   lo <= ofs < hi -> perm_of_res (phi @ (b, ofs)) = Some Freeable).
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: @eq (option permission) (perm_of_res (resource_at phi (@pair block Z b ofs))) (@Some permission Freeable) *)
destruct H as [phi1 [phi2 [? [? ?]]]].
(* Goal: @eq (option permission) (perm_of_res (resource_at phi (@pair block Z b ofs))) (@Some permission Freeable) *)
destruct H1 as [H1 _]; specialize (H1 (b,ofs)).
(* Goal: @eq (option permission) (perm_of_res (resource_at phi (@pair block Z b ofs))) (@Some permission Freeable) *)
apply (resource_at_join _ _ _ (b,ofs)) in H.
(* Goal: @eq (option permission) (perm_of_res (resource_at phi (@pair block Z b ofs))) (@Some permission Freeable) *)
hnf in H1. rewrite if_true in H1 by (split; auto; omega).
(* Goal: @eq (option permission) (perm_of_res (resource_at phi (@pair block Z b ofs))) (@Some permission Freeable) *)
destruct H1 as [? [? ?]].
(* Goal: @eq (option permission) (perm_of_res (resource_at phi (@pair block Z b ofs))) (@Some permission Freeable) *)
hnf in H1. rewrite H1 in H.
(* Goal: @eq (option permission) (perm_of_res (resource_at phi (@pair block Z b ofs))) (@Some permission Freeable) *)
inv H. simpl.
(* Goal: @eq (option permission) (perm_of_sh sh3) (@Some permission Freeable) *)
(* Goal: @eq (option permission) (perm_of_res (YES sh3 rsh3 (VAL x) (SomeP (ConstType unit) (fun _ : list Type => tt)))) (@Some permission Freeable) *)
clear - RJ.
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
apply join_top in RJ. subst. apply perm_of_freeable.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
simpl.
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
apply join_top in RJ. subst. apply perm_of_freeable.
Qed.

Lemma juicy_free_lemma:
  forall {j b lo hi m' m1 F}
    (H: Mem.free (m_dry j) b lo hi = Some m')
    (VR: app_pred (VALspec_range (hi-lo) Share.top (b,lo) * F) (m_phi j)),
    VALspec_range (hi-lo) Share.top (b,lo) m1 ->
    core m1 = core (m_phi j) ->
    (forall l sh rsh k pp, m1 @ l = YES sh rsh k pp 
      -> exists sh', exists (rsh': readable_share sh'), 
            exists pp', join_sub sh sh' 
              /\ m_phi j @ l = YES sh' rsh' k pp') -> 
    join m1 (m_phi (free_juicy_mem _ _ _ _ _ H)) (m_phi j).
Proof.
intros j b lo hi m' m1.
pose (H0 :=True).
intros R H VR H1 H2 Hyes.
assert (forall l, ~adr_range (b,lo) (hi-lo) l -> identity (m1 @ l)).
  unfold VALspec_range, allp, jam in H1.
  intros l. destruct H1 as [H1 _]; specialize (H1 l). intros H3.
  hnf in H1; if_tac in H1; try solve [contradiction].
  apply H1.
assert (forall l, adr_range (b,lo) (hi-lo) l 
  -> exists mv, yesat NoneP (VAL mv) Share.top  l m1).
  unfold VALspec_range, allp, jam in H1.
  intros l. destruct H1 as [H1 _]; specialize (H1 l). intros H4.
  hnf in H1; if_tac in H1; try solve [contradiction].
  apply H1.
remember (free_juicy_mem _ _ _ _ _ H) as j'.
assert (m' = m_dry j') by (subst; reflexivity).
assert (Ha := juicy_mem_access j').
unfold access_cohere in Ha.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
apply resource_at_join2; auto.
rewrite <- (level_core m1). rewrite <- (level_core (m_phi j)). congruence.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
subst j'. simpl. unfold inflate_free. simpl. rewrite level_make_rmap. auto.
intros (b0, ofs0).
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
subst j'. simpl.
unfold inflate_free; rewrite resource_at_make_rmap.
destruct (adr_range_dec (b,lo) (hi-lo) (b0,ofs0)).
* (* adr_range *)
clear H3.
specialize (H4 (b0,ofs0) a).
destruct H4 as [mv H4].
unfold yesat, yesat_raw in H4. destruct H4 as [pp H4].
simpl in H4.
(* Goal: Z.le (Zpos xH) (Z.sub ofs' ofs) *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.sub ofs' ofs) (Zneg p)), Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH))) *)
rewrite H4.
clear H0.
assert (H0 : access_at m' (b0, ofs0) Cur = None).
  clear - H a.
  Transparent free.
  unfold free in H.
  if_tac in H; try solve [congruence].
(* Goal: @eq (option permission) (perm_of_res (resource_at phi (@pair block Z b ofs))) (@Some permission Freeable) *)
  unfold unchecked_free in H. inv H. simpl.
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  assert (b = b0) by (destruct a; auto). subst.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
  unfold access_at; simpl. rewrite PMap.gss.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  rewrite adr_range_zle_zlt with (b:=b0); auto.
specialize (Ha (b0,ofs0)). rewrite <- H5 in Ha.
rewrite H0 in Ha.
assert (H3 : m_phi j @ (b0, ofs0) = YES Share.top readable_share_top (VAL mv) NoneP). {
  clear - H H4 a Hyes.
  assert (Ha := juicy_mem_access j (b0,ofs0)).
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
  generalize (Hyes _ _ _ _ _ H4); intros.
  repeat rewrite preds_fmap_NoneP in *. 
  destruct H0 as [sh' [rsh' [? [RJ ?]]]]. 
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) (@fst block Z loc) (mem_access m) (@snd block Z loc) k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) (@fst block Z loc) (mem_access m') (@snd block Z loc) k) *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
  rewrite H0. repeat f_equal.
(* Goal: @eq (option permission) (perm_of_sh sh3) (@Some permission Freeable) *)
  destruct RJ as [? RJ]; apply join_top in RJ. subst sh'.
  pose proof (juicy_mem_contents j). 
  destruct (H1 _ _ _ _ _ H0); auto. subst. apply YES_ext; auto.
 }
rewrite H3. repeat rewrite preds_fmap_NoneP. unfold pfullshare.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
apply join_unit2. constructor. apply join_unit1; auto.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) (@fst block Z loc) (mem_access m) (@snd block Z loc) k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) (@fst block Z loc) (mem_access m') (@snd block Z loc) k) *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
f_equal. apply proof_irr.
* (* ~adr_range *)
  clear H0.
  generalize (H3 _ n); intro H3'.
  assert (core (m1 @ (b0,ofs0)) = core (m_phi j @ (b0,ofs0))).
  do 2 rewrite core_resource_at. unfold Join_rmap in *.  unfold Sep_rmap in  *; congruence.
  apply identity_resource in H3'.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  revert H3'; case_eq (m1 @ (b0,ofs0));intros; try contradiction; try constructor.
  + apply identity_share_bot in H3'; subst sh.
    rename H6 into Hm1.
    clear H0.
    destruct (free_nadr_range_eq _ _ _ _ _ _ _ n H) as [H0 H10].
    (* rewrite <- H0 in *; clear H0.*)
    assert (Ha0 := juicy_mem_access j (b0,ofs0)).
    revert Ha0;
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
      case_eq (m_phi j @ (b0,ofs0)); intros.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
    constructor. apply join_unit1; auto.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
    constructor. apply join_unit1; auto.

    elimtype False.
    clear - H2 Hm1 H0 H6.
    assert (core (m1 @ (b0,ofs0)) = core (m_phi j @ (b0,ofs0))).
    do 2 rewrite core_resource_at.  unfold Join_rmap in *;  unfold Sep_rmap in  *; congruence.
    rewrite Hm1 in H. rewrite H6 in H.
(* Goal: @eq (option permission) (perm_of_res (resource_at phi (@pair block Z b ofs))) (@Some permission Freeable) *)
    rewrite core_PURE in H. rewrite core_NO in H; inv H.
  + rewrite H6 in H0. rewrite core_PURE in H0.
    destruct (m_phi j @ (b0,ofs0)).
(* Goal: perm_order' (if writable0_share_dec sh2 then if @eq_dec Share.t Share.EqDec_share sh2 Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec sh2 then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) Freeable *)
    rewrite core_NO in H0; inv H0. rewrite core_YES in H0; inv H0.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
    rewrite core_PURE in H0. inversion H0. subst k0 p0; constructor.
* destruct H1 as [_ Hg].
  rewrite (identity_core Hg), core_ghost_of, H2.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
  subst j'; simpl.
  unfold inflate_free.
(* Goal: @eq ghost (ghost_of (@proj1_sig rmap (fun phi : rmap => and (@eq nat (@level rmap ag_rmap phi) (@level rmap ag_rmap (m_phi jm))) (and (@eq (forall _ : AV.address, resource) (resource_at phi) (fun loc : AV.address => if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) loc then NO Share.bot bot_unreadable else resource_at (m_phi jm) loc)) (@eq ghost (ghost_of phi) (ghost_of (m_phi jm))))) (make_rmap (fun loc : AV.address => if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) loc then NO Share.bot bot_unreadable else resource_at (m_phi jm) loc) (ghost_of (m_phi jm)) (@level rmap ag_rmap (m_phi jm)) (@functional_extensionality AV.address resource (fun x : AV.address => resource_fmap (approx (@level rmap ag_rmap (m_phi jm))) (approx (@level rmap ag_rmap (m_phi jm))) (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) x then NO Share.bot bot_unreadable else resource_at (m_phi jm) x)) (fun loc : AV.address => if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) loc then NO Share.bot bot_unreadable else resource_at (m_phi jm) loc) (fun l : AV.address => let (b', ofs') as p return (@eq resource (resource_fmap (approx (@level rmap ag_rmap (m_phi jm))) (approx (@level rmap ag_rmap (m_phi jm))) (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) p then NO Share.bot bot_unreadable else resource_at (m_phi jm) p)) (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) p then NO Share.bot bot_unreadable else resource_at (m_phi jm) p)) := l in if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) (@pair block Z b' ofs') as s return (@eq resource (resource_fmap (approx (@level rmap ag_rmap (m_phi jm))) (approx (@level rmap ag_rmap (m_phi jm))) (if s then NO Share.bot bot_unreadable else resource_at (m_phi jm) (@pair block Z b' ofs'))) (if s then NO Share.bot bot_unreadable else resource_at (m_phi jm) (@pair block Z b' ofs'))) then @eq_refl resource (NO Share.bot bot_unreadable) else resource_at_approx (m_phi jm) (@pair block Z b' ofs'))) (ghost_of_approx (m_phi jm))))) (ghost_of phi2) *)
  rewrite ghost_of_make_rmap.
  rewrite <- core_ghost_of; apply core_unit.
Qed.

Section free.

Variables (jm :juicy_mem) (m': mem)
          (b: block) (lo hi: Z)
          (FREE: free (m_dry jm) b lo hi = Some m')
          (PERM: forall ofs, lo <= ofs < hi ->
                      perm_of_res (m_phi jm @ (b,ofs)) = Some Freeable)
          (phi1 phi2 : rmap) (Hphi1: VALspec_range (hi-lo) Share.top (b,lo) phi1)
          (Hjoin : join phi1 phi2 (m_phi jm)).

Lemma phi2_eq : m_phi (free_juicy_mem _ _ _ _ _ FREE) = phi2.
Proof.
(* Goal: @eq rmap (m_phi (free_juicy_mem jm m' b lo hi FREE)) phi2 *)
  apply rmap_ext; simpl; unfold inflate_free; rewrite ?level_make_rmap, ?resource_at_make_rmap.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  - apply join_level in Hjoin; destruct Hjoin; auto.
(* Goal: forall l : AV.address, @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
  - intro.
(* Goal: @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
    destruct Hphi1 as [Hphi1' _]. specialize (Hphi1' l); simpl in Hphi1'.
(* Goal: @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) l then NO Share.bot bot_unreadable else resource_at (m_phi jm) l) (resource_at phi2 l) *)
    apply (resource_at_join _ _ _ l) in Hjoin.
(* Goal: perm_order'' (@Some permission Writable) (if writable0_share_dec (Share.glb Share.Rsh sh) then if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
    if_tac.
    + destruct Hphi1' as (? & ? & H1); rewrite H1 in Hjoin; inv Hjoin.
      * pose proof (join_top _ _ RJ); subst; apply sepalg.join_comm, unit_identity, identity_share_bot in RJ.
(* Goal: @eq resource (NO Share.bot bot_unreadable) (NO sh2 nsh2) *)
        subst; apply f_equal, proof_irr.
      * pose proof (join_top _ _ RJ); subst; apply sepalg.join_comm, unit_identity, identity_share_bot in RJ.
(* Goal: @eq resource (NO Share.bot bot_unreadable) (YES sh2 rsh2 (VAL x) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
        subst; contradiction bot_unreadable.
    + apply Hphi1' in Hjoin; auto.
(* Goal: @eq ghost (ghost_of (@proj1_sig rmap (fun phi : rmap => and (@eq nat (@level rmap ag_rmap phi) (@level rmap ag_rmap (m_phi jm))) (and (@eq (forall _ : AV.address, resource) (resource_at phi) (fun loc : AV.address => if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) loc then NO Share.bot bot_unreadable else resource_at (m_phi jm) loc)) (@eq ghost (ghost_of phi) (ghost_of (m_phi jm))))) (make_rmap (fun loc : AV.address => if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) loc then NO Share.bot bot_unreadable else resource_at (m_phi jm) loc) (ghost_of (m_phi jm)) (@level rmap ag_rmap (m_phi jm)) (@functional_extensionality AV.address resource (fun x : AV.address => resource_fmap (approx (@level rmap ag_rmap (m_phi jm))) (approx (@level rmap ag_rmap (m_phi jm))) (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) x then NO Share.bot bot_unreadable else resource_at (m_phi jm) x)) (fun loc : AV.address => if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) loc then NO Share.bot bot_unreadable else resource_at (m_phi jm) loc) (fun l : AV.address => let (b', ofs') as p return (@eq resource (resource_fmap (approx (@level rmap ag_rmap (m_phi jm))) (approx (@level rmap ag_rmap (m_phi jm))) (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) p then NO Share.bot bot_unreadable else resource_at (m_phi jm) p)) (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) p then NO Share.bot bot_unreadable else resource_at (m_phi jm) p)) := l in if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) (@pair block Z b' ofs') as s return (@eq resource (resource_fmap (approx (@level rmap ag_rmap (m_phi jm))) (approx (@level rmap ag_rmap (m_phi jm))) (if s then NO Share.bot bot_unreadable else resource_at (m_phi jm) (@pair block Z b' ofs'))) (if s then NO Share.bot bot_unreadable else resource_at (m_phi jm) (@pair block Z b' ofs'))) then @eq_refl resource (NO Share.bot bot_unreadable) else resource_at_approx (m_phi jm) (@pair block Z b' ofs'))) (ghost_of_approx (m_phi jm))))) (ghost_of phi2) *)
  - rewrite ghost_of_make_rmap.
(* Goal: @eq ghost (ghost_of (m_phi jm)) (ghost_of phi2) *)
    destruct Hphi1 as [_ Hg].
(* Goal: @eq ghost (ghost_of (m_phi jm)) (ghost_of phi2) *)
    apply ghost_of_join in Hjoin.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
    symmetry; apply Hg; auto.
Qed.

End free.

Lemma juicy_free_lemma':
  forall {j b lo hi m' m1 m2 F}
    (H: Mem.free (m_dry j) b lo hi = Some m')
    (VR: app_pred (VALspec_range (hi-lo) Share.top (b,lo) * F) (m_phi j)),
    VALspec_range (hi-lo) Share.top (b,lo) m1 ->
    join m1 m2 (m_phi j) ->
    m_phi (free_juicy_mem _ _ _ _ _ H) = m2.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
  intros.
(* Goal: @ex preds (fun pp : preds => @eq resource (resource_at w loc) (YES rsh sh (VAL v) pp)) *)
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
  eapply phi2_eq; eauto.
Qed.

Lemma initial_mem_core: forall lev m j IOK,
  j = initial_mem m lev IOK -> juicy_mem_core j = core lev.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
destruct j; simpl.
(* Goal: @eq rmap (juicy_mem_core (mkJuicyMem m0 phi JMcontents JMaccess JMmax_access JMalloc)) (@core rmap Join_rmap Sep_rmap lev) *)
unfold initial_mem in H.
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
inversion H; subst.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
unfold juicy_mem_core. simpl.
clear - IOK.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev)) (@core rmap Join_rmap Sep_rmap lev) *)
apply rmap_ext.
(* Goal: @eq nat (@level rmap ag_rmap (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (@level rmap ag_rmap (@core rmap Join_rmap Sep_rmap lev)) *)
(* Goal: forall l : AV.address, @eq resource (resource_at (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev)) l) (resource_at (@core rmap Join_rmap Sep_rmap lev) l) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
repeat rewrite level_core.
(* Goal: @ex preds (fun pp : preds => @eq resource (resource_at w loc) (YES rsh sh (VAL v) pp)) *)
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
erewrite inflate_initial_mem_level; eauto.
(* Goal: forall l : AV.address, @eq resource (resource_at (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev)) l) (resource_at (@core rmap Join_rmap Sep_rmap lev) l) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
intro loc.
repeat rewrite <- core_resource_at.
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
unfold inflate_initial_mem.
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at (@proj1_sig rmap (fun phi : rmap => and (@eq nat (@level rmap ag_rmap phi) (@level rmap ag_rmap lev)) (and (@eq (forall _ : AV.address, resource) (resource_at phi) (inflate_initial_mem' m lev)) (@eq ghost (ghost_of phi) (ghost_of lev)))) (make_rmap (inflate_initial_mem' m lev) (ghost_of lev) (@level rmap ag_rmap lev) (inflate_initial_mem'_fmap m lev) (ghost_of_approx lev))) loc)) (@core resource Join_resource Sep_resource (resource_at lev loc)) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
rewrite resource_at_make_rmap.
(* Goal: @eq resource (@core resource Join_resource Sep_resource (inflate_initial_mem' m lev loc)) (@core resource Join_resource Sep_resource (resource_at lev loc)) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
unfold inflate_initial_mem'.
repeat rewrite <- core_resource_at.
(* Goal: @eq resource (@core resource Join_resource Sep_resource match access_at m loc Cur with | Some (Freeable as p) => YES Share.top readable_share_top (VAL (contents_at m loc)) NoneP | Some (Writable as p) => YES Ews (@writable_readable Ews writable_Ews) (VAL (contents_at m loc)) NoneP | Some (Readable as p) => YES Ers readable_Ers (VAL (contents_at m loc)) NoneP | Some (Nonempty as p) => match resource_at lev loc with | NO sh n => NO extern_retainer nonreadable_extern_retainer | YES sh r k p0 => NO extern_retainer nonreadable_extern_retainer | PURE k p0 => resource_at lev loc end | None => NO Share.bot bot_unreadable end) (@core resource Join_resource Sep_resource (resource_at lev loc)) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
destruct (IOK loc). clear IOK.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
revert H0; case_eq (lev @ loc); intros.
(* Goal: @eq resource (@core resource Join_resource Sep_resource match access_at m loc Cur with | Some (Freeable as p) => YES Share.top readable_share_top (VAL (contents_at m loc)) NoneP | Some (Writable as p) => YES Ews (@writable_readable Ews writable_Ews) (VAL (contents_at m loc)) NoneP | Some (Readable as p) => YES Ers readable_Ers (VAL (contents_at m loc)) NoneP | Some (Nonempty as p) => NO extern_retainer nonreadable_extern_retainer | None => NO Share.bot bot_unreadable end) (@core resource Join_resource Sep_resource (NO sh n)) *)
(* Goal: @eq resource (@core resource Join_resource Sep_resource match access_at m loc Cur with | Some (Freeable as p) => YES Share.top readable_share_top (VAL (contents_at m loc)) NoneP | Some (Writable as p) => YES Ews (@writable_readable Ews writable_Ews) (VAL (contents_at m loc)) NoneP | Some (Readable as p) => YES Ers readable_Ers (VAL (contents_at m loc)) NoneP | Some (Nonempty as p) => NO extern_retainer nonreadable_extern_retainer | None => NO Share.bot bot_unreadable end) (@core resource Join_resource Sep_resource (YES sh r k p)) *)
(* Goal: @eq resource (@core resource Join_resource Sep_resource match access_at m loc Cur with | Some (Freeable as p0) => YES Share.top readable_share_top (VAL (contents_at m loc)) NoneP | Some (Writable as p0) => YES Ews (@writable_readable Ews writable_Ews) (VAL (contents_at m loc)) NoneP | Some (Readable as p0) => YES Ers readable_Ers (VAL (contents_at m loc)) NoneP | Some (Nonempty as p0) => PURE k p | None => NO Share.bot bot_unreadable end) (@core resource Join_resource Sep_resource (PURE k p)) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
rewrite core_NO.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
destruct (access_at m loc); try destruct p; try rewrite core_NO; try rewrite core_YES; auto.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
destruct (access_at m loc); try destruct p0; try rewrite core_NO;  repeat rewrite core_YES; auto.
(* Goal: @eq resource (@core resource Join_resource Sep_resource match access_at m loc Cur with | Some (Freeable as p0) => YES Share.top readable_share_top (VAL (contents_at m loc)) NoneP | Some (Writable as p0) => YES Ews (@writable_readable Ews writable_Ews) (VAL (contents_at m loc)) NoneP | Some (Readable as p0) => YES Ers readable_Ers (VAL (contents_at m loc)) NoneP | Some (Nonempty as p0) => PURE k p | None => NO Share.bot bot_unreadable end) (@core resource Join_resource Sep_resource (PURE k p)) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
destruct H1.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
destruct H2. rewrite H2. auto.
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
unfold inflate_initial_mem.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
rewrite <- core_ghost_of, ghost_of_make_rmap, core_ghost_of; auto.
Qed.

Lemma writable_writable_after_alloc' : forall m1 m2 lo hi b lev loc IOK1 IOK2,
  alloc m1 lo hi = (m2, b) ->
  writable loc (m_phi (initial_mem m1 lev IOK1)) ->
  writable loc (m_phi (initial_mem m2 lev IOK2)).
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
hnf in *.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
case_eq (m_phi (initial_mem m1 lev IOK1) @ loc); intros.
(* Goal: @eq Z z1 z2 *)
rewrite H1 in H0.
(* Goal: perm_order' (if writable0_share_dec sh2 then if @eq_dec Share.t Share.EqDec_share sh2 Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec sh2 then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) Freeable *)
inv H0.
(* Goal: @eq Z z1 z2 *)
rewrite H1 in H0.
assert (~adr_range (b,lo) (hi-lo) loc). {
 assert (Ha := juicy_mem_access (initial_mem m1 lev IOK1) loc).
(* Goal: Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.sub ofs' ofs) (Zneg p)), Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH))) *)
  destruct loc. simpl in *.
  rewrite H1 in Ha.
(* Goal: perm_order' (if writable0_share_dec sh2 then if @eq_dec Share.t Share.EqDec_share sh2 Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec sh2 then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) Freeable *)
  destruct H0 as [_ H0]. destruct k; inv H0.
  intro Contra.
  destruct Contra.
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  subst.
  assert (access_at m1 (nextblock m1, z) Cur = None).
(* Goal: not (@eq Z r ofs) *)
(* Goal: or (and (@eq block b b') (and (Z.le z ofs) (Z.lt ofs (Z.add z (size_chunk ch))))) (@eq memval (contents_at m (@pair block Z b' ofs)) (contents_at m' (@pair block Z b' ofs))) *)
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m) (access_at m') *)
(* Goal: @eq block (nextblock m) (nextblock m') *)
    unfold access_at; apply nextblock_noaccess; simpl; xomega.
  assert (b0 = nextblock m1) by (eapply alloc_result; eauto).
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  subst.
(* Goal: @eq resource (resource_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) match k with | VAL m => if readable_perm (access_at m' loc Cur) then YES sh r (VAL (contents_at m' loc)) NoneP else NO Share.bot bot_unreadable | LK n i => YES sh r k p | FUN f c => YES sh r k p end) match k with | VAL m => if readable_perm (access_at m' loc Cur) then YES sh r (VAL (contents_at m' loc)) NoneP else NO Share.bot bot_unreadable | LK n i => YES sh r k p | FUN f c => YES sh r k p end *)
(* Goal: @eq resource (resource_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) (PURE k p)) (PURE k p) *)
(* Goal: @eq ghost (ghost_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) (ghost_of (m_phi jm))) (ghost_of (m_phi jm)) *)
  rewrite Ha in H0. simpl in H0. clear - r H0.
(* Goal: perm_order' (if writable0_share_dec sh2 then if @eq_dec Share.t Share.EqDec_share sh2 Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec sh2 then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) Freeable *)
  unfold perm_of_sh in H0. repeat if_tac in H0; try contradiction; inv H0.
}
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
apply alloc_dry_unchanged_on with (m1:=m1)(m2:=m2) in H2; auto.
(* Goal: @eq resource (@core resource Join_resource Sep_resource match access_at m loc Cur with | Some (Freeable as p0) => YES Share.top readable_share_top (VAL (contents_at m loc)) NoneP | Some (Writable as p0) => YES Ews (@writable_readable Ews writable_Ews) (VAL (contents_at m loc)) NoneP | Some (Readable as p0) => YES Ers readable_Ers (VAL (contents_at m loc)) NoneP | Some (Nonempty as p0) => PURE k p | None => NO Share.bot bot_unreadable end) (@core resource Join_resource Sep_resource (PURE k p)) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
destruct H2.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
unfold initial_mem; simpl.
unfold inflate_initial_mem, inflate_initial_mem'.
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at (@proj1_sig rmap (fun phi : rmap => and (@eq nat (@level rmap ag_rmap phi) (@level rmap ag_rmap lev)) (and (@eq (forall _ : AV.address, resource) (resource_at phi) (inflate_initial_mem' m lev)) (@eq ghost (ghost_of phi) (ghost_of lev)))) (make_rmap (inflate_initial_mem' m lev) (ghost_of lev) (@level rmap ag_rmap lev) (inflate_initial_mem'_fmap m lev) (ghost_of_approx lev))) loc)) (@core resource Join_resource Sep_resource (resource_at lev loc)) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
rewrite resource_at_make_rmap.
destruct loc as (b',ofs').
assert (Ha := juicy_mem_access (initial_mem m1 lev IOK1) (b',ofs')). {
  rewrite H1 in Ha.
  destruct H0 as [Hfree H0]. destruct k; try solve [inversion H0].
  unfold perm_of_res in Ha. simpl in Ha.
  rewrite <- H3.
  rewrite <- H2. rewrite Ha.
  clear - Hfree r.
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) *)
  unfold perm_of_sh. rewrite if_true by auto. if_tac; auto.
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) *)
  rewrite Ha. unfold perm_of_sh. rewrite if_true by auto. 
  clear; if_tac; congruence.
 }
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
 rewrite H1 in H0. simpl in H0. contradiction.
Qed.

Lemma readable_eq_after_alloc' : forall m1 m2 lo hi b lev loc IOK1 IOK2,
  alloc m1 lo hi = (m2, b) ->
  readable loc (m_phi (initial_mem m1 lev IOK1)) ->
  m_phi (initial_mem m1 lev IOK1) @ loc=m_phi (initial_mem m2 lev IOK2) @ loc.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
hnf in H0.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
case_eq (m_phi (initial_mem m1 lev IOK1) @ loc); intros.
(* Goal: @eq Z z1 z2 *)
rewrite H1 in H0.
(* Goal: perm_order' (if writable0_share_dec sh2 then if @eq_dec Share.t Share.EqDec_share sh2 Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec sh2 then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) Freeable *)
inv H0.
(* Goal: @eq Z z1 z2 *)
rewrite H1 in H0.
assert (~adr_range (b,lo) (hi-lo) loc). {
 assert (Ha := juicy_mem_access (initial_mem m1 lev IOK1) loc).
(* Goal: Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: forall (p : positive) (_ : @eq Z (Z.sub ofs' ofs) (Zneg p)), Z.le (Z.add ofs (Zpos xH)) ofs' *)
(* Goal: Z.lt ofs' (Z.add (Z.add ofs (Zpos xH)) (Z.sub z (Zpos xH))) *)
  destruct loc. simpl in *.
  rewrite H1 in Ha.
  destruct k; try solve [inv H0].
  intro Contra.
  destruct Contra.
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  subst.
  assert (b0 = nextblock m1) by (eapply alloc_result; eauto).
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  subst.
  simpl in Ha.
(*
  destruct (perm_of_sh_pshare t p) as [p' H4].
  unfold perm_of_res in Ha; simpl in Ha; rewrite H4 in Ha.
*)
  assert (access_at m1 (nextblock m1, z) Cur = None).
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
    unfold access_at. simpl. apply nextblock_noaccess. xomega.
  rewrite H2 in Ha.
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
  clear - Ha r. unfold perm_of_sh in Ha. repeat if_tac in Ha; inv Ha; try contradiction.
}
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
apply alloc_dry_unchanged_on with (m1:=m1)(m2:=m2) in H2; auto.
(* Goal: @eq resource (@core resource Join_resource Sep_resource match access_at m loc Cur with | Some (Freeable as p0) => YES Share.top readable_share_top (VAL (contents_at m loc)) NoneP | Some (Writable as p0) => YES Ews (@writable_readable Ews writable_Ews) (VAL (contents_at m loc)) NoneP | Some (Readable as p0) => YES Ers readable_Ers (VAL (contents_at m loc)) NoneP | Some (Nonempty as p0) => PURE k p | None => NO Share.bot bot_unreadable end) (@core resource Join_resource Sep_resource (PURE k p)) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
destruct H2.
rewrite <- H1.
(* Goal: @eq rmap (@core rmap Join_rmap Sep_rmap (m_phi (mkJuicyMem m (inflate_initial_mem m lev) JMcontents JMaccess JMmax_access JMalloc))) (@core rmap Join_rmap Sep_rmap lev) *)
unfold initial_mem; simpl.
unfold inflate_initial_mem, inflate_initial_mem'.
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at (@proj1_sig rmap (fun phi : rmap => and (@eq nat (@level rmap ag_rmap phi) (@level rmap ag_rmap lev)) (and (@eq (forall _ : AV.address, resource) (resource_at phi) (inflate_initial_mem' m lev)) (@eq ghost (ghost_of phi) (ghost_of lev)))) (make_rmap (inflate_initial_mem' m lev) (ghost_of lev) (@level rmap ag_rmap lev) (inflate_initial_mem'_fmap m lev) (ghost_of_approx lev))) loc)) (@core resource Join_resource Sep_resource (resource_at lev loc)) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap (inflate_initial_mem m lev))) (ghost_of (@core rmap Join_rmap Sep_rmap lev)) *)
do 2 rewrite resource_at_make_rmap.
destruct loc as (b',ofs').
 assert (Ha := juicy_mem_access (initial_mem m1 lev IOK1) (b',ofs')). {
   rewrite H1 in Ha.   unfold perm_of_res in Ha; simpl in Ha.
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
   simpl in H0. destruct k; try contradiction.
  rewrite <- H2. rewrite Ha in *.
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
  spec H3. clear - r. unfold perm_of_sh. repeat if_tac; try congruence; contradiction.
  rewrite <- H3.
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) *)
  unfold perm_of_sh. if_tac. if_tac; auto. rewrite if_true by auto. auto.

 }
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (mem_access (m_dry jm)) i Cur with | Some p' => perm_order p' Writable | None => False end *)
 rewrite H1 in H0. contradiction.
Qed.


Lemma necR_m_dry:
  forall jm jm', necR jm jm' -> m_dry jm = m_dry jm'.
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
intros.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
induction H; auto.
(* Goal: @eq mem (m_dry x) (m_dry y) *)
(* Goal: @eq mem (m_dry x) (m_dry z) *)
unfold age in H.
(* Goal: @eq mem (m_dry x) (m_dry y) *)
(* Goal: @eq mem (m_dry x) (m_dry z) *)
apply age1_juicy_mem_unpack in H.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
decompose [and] H; auto.
(* Goal: @eq mem (m_dry x) (m_dry z) *)
inv IHclos_refl_trans1.
(* Goal: @eq mem (m_dry x) (m_dry z) *)
inv IHclos_refl_trans2.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
auto.
Qed.

Lemma perm_order''_trans p1 p2 p3 :
  perm_order'' p1 p2 ->
  perm_order'' p2 p3 ->
  perm_order'' p1 p3.
Proof.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  destruct p1, p2, p3; simpl; try tauto.
(* Goal: forall (_ : perm_order p p0) (_ : perm_order p0 p1), perm_order p p1 *)
  apply perm_order_trans.
Qed.

Lemma po_join_sub_sh sh1 sh2 :
  join_sub sh2 sh1 ->
  Mem.perm_order'' (perm_of_sh sh1) (perm_of_sh sh2).
Proof.
(* Goal: forall _ : @join_sub Share.t Share.Join_ba sh2 sh1, perm_order'' (perm_of_sh sh1) (perm_of_sh sh2) *)
  intros [sh J].
(* Goal: perm_order'' (@Some permission Writable) (perm_of_sh (Share.glb Share.Rsh sh)) *)
  unfold perm_of_sh.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  if_tac. if_tac. repeat if_tac; constructor.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  if_tac. rewrite if_false. constructor.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  contradict H0. subst. apply join_top in J; auto.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  repeat if_tac; constructor.
(* Goal: perm_order'' (if readable_share_dec sh1 then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) (if writable0_share_dec sh2 then if @eq_dec Share.t Share.EqDec_share sh2 Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec sh2 then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) *)
  assert (~writable0_share sh2) by (contradict H; eapply join_writable01; eauto).
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  if_tac. rewrite if_false by auto. repeat if_tac; constructor.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  rewrite (if_false (writable0_share sh2)) by auto.
(* Goal: perm_order'' (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) (if readable_share_dec sh2 then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) *)
  assert (~readable_share sh2) by (contradict H1; eapply join_readable1; eauto).
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  rewrite (if_false (readable_share sh2)) by auto.
(* Goal: perm_order'' (@Some permission Writable) (if writable0_share_dec (Share.glb Share.Rsh sh) then if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  if_tac.
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  subst. apply split_identity in J. apply identity_share_bot in J.
(* Goal: perm_order'' (@None permission) (if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh2 Share.bot then @None permission else @Some permission Nonempty) *)
  rewrite if_true by auto. constructor.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  auto. if_tac; constructor.
Qed.

Lemma po_join_sub r1 r2 :
  join_sub r2 r1 ->
  Mem.perm_order'' (perm_of_res r1) (perm_of_res r2).
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
  intros. destruct H as [r J]. inv J; simpl.
(* Goal: perm_order'' (@Some permission Writable) (if writable0_share_dec (Share.glb Share.Rsh sh) then if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.top then @Some permission Freeable else @Some permission Writable else if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  if_tac. subst. apply split_identity in RJ.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  apply identity_share_bot in RJ. rewrite if_true by auto; constructor.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  auto. if_tac; constructor.
(* Goal: @ex preds (fun pp : preds => @eq resource (resource_at w loc) (YES rsh sh (VAL v) pp)) *)
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
  destruct k; try constructor; apply po_join_sub_sh; eexists; eauto.
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
  apply perm_order''_trans with (Some Nonempty).
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  destruct k; try constructor.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  unfold perm_of_sh. if_tac. if_tac; constructor. rewrite if_true by auto; constructor.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  if_tac; constructor.
(* Goal: @ex preds (fun pp : preds => @eq resource (resource_at w loc) (YES rsh sh (VAL v) pp)) *)
(* Goal: and (@eq memval (contents_at m loc) v) (@eq preds pp NoneP) *)
(* Goal: @ex juicy_mem (fun jm : juicy_mem => and (@age juicy_mem juicy_mem_ageable jm (mkJuicyMem m phi' CONTENTS ACCESS MAXA ALLOC)) (@eq rmap (m_phi jm) w)) *)
  destruct k; try constructor. apply po_join_sub_sh; eexists; eauto.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  constructor.
Qed.

(*
Lemma po_join_sub' r1 r2 :
  join_sub r2 r1 ->
  Mem.perm_order'' (perm_of_res' r1) (perm_of_res' r2).
Proof.
  
*)
Lemma perm_of_res_lock_not_Freeable:
  forall r,
    perm_order'' (Some Writable) (perm_of_res_lock r).
Proof.
(* Goal: forall r : resource, perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
  intros.
(* Goal: perm_order'' (@Some permission Writable) (perm_of_res_lock r) *)
  unfold perm_of_res_lock.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  destruct r; try constructor.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  destruct k; try constructor.
(* Goal: perm_order'' (@Some permission Writable) (perm_of_sh (Share.glb Share.Rsh sh)) *)
  unfold perm_of_sh.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  if_tac. rewrite if_false. constructor.
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  apply glb_Rsh_not_top.
(* Goal: perm_order'' (@Some permission Writable) (@Some permission Writable) *)
(* Goal: not (@eq Share.t (Share.glb Share.Rsh sh) Share.top) *)
(* Goal: perm_order'' (@Some permission Writable) (if readable_share_dec (Share.glb Share.Rsh sh) then @Some permission Readable else if @eq_dec Share.t Share.EqDec_share (Share.glb Share.Rsh sh) Share.bot then @None permission else @Some permission Nonempty) *)
  repeat if_tac; constructor.
Qed.

Definition readable_perm (p: option permission) :
  {perm_order'' p (Some Readable)}+{~perm_order'' p (Some Readable)}.
destruct p.
destruct p; try solve [left; constructor].
(* Goal: @eq (option permission) (perm_of_res (resource_at phi (@pair block Z b ofs))) (@Some permission Freeable) *)
all: right; intro; inv H.
Defined.

Definition rebuild_juicy_mem_fmap (jm: juicy_mem) (m': mem) : (AV.address -> resource) :=
 fun loc =>
   match m_phi jm @ loc with
    PURE k pp => PURE k pp
   | NO sh rsh => if readable_perm (access_at m' loc Cur)
                            then YES Tsh (writable_readable writable_share_top)
                                        (VAL (contents_at m' loc)) NoneP
                            else NO sh rsh 
   | YES sh rsh (VAL _) _ => 
                 if readable_perm (access_at m' loc Cur)
                 then YES sh rsh (VAL (contents_at m' loc)) NoneP
                 else NO _ bot_unreadable
   | YES sh rsh _ _ => m_phi jm @ loc
end.

Definition rebuild_juicy_mem_rmap (jm: juicy_mem) (m': mem) :
  {phi : rmap |
  level phi = level jm /\
  resource_at phi = rebuild_juicy_mem_fmap jm m' /\
  ghost_of phi = ghost_of (m_phi jm)}.
(* Goal: @sig rmap (fun phi : rmap => and (@eq nat (@level rmap ag_rmap phi) (@level juicy_mem juicy_mem_ageable jm)) (and (@eq (forall _ : AV.address, resource) (resource_at phi) (rebuild_juicy_mem_fmap jm m')) (@eq ghost (ghost_of phi) (ghost_of (m_phi jm))))) *)
  refine (make_rmap (rebuild_juicy_mem_fmap jm m') (ghost_of (m_phi jm)) (level jm) _ _).
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm))) (rebuild_juicy_mem_fmap jm m')) (rebuild_juicy_mem_fmap jm m') *)
(* Goal: @eq ghost (ghost_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) (ghost_of (m_phi jm))) (ghost_of (m_phi jm)) *)
extensionality loc.
(* Goal: @eq resource (@compose AV.address resource resource (resource_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm))) (rebuild_juicy_mem_fmap jm m') loc) (rebuild_juicy_mem_fmap jm m' loc) *)
(* Goal: @eq ghost (ghost_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) (ghost_of (m_phi jm))) (ghost_of (m_phi jm)) *)
unfold compose.
(* Goal: @eq resource (resource_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) (rebuild_juicy_mem_fmap jm m' loc)) (rebuild_juicy_mem_fmap jm m' loc) *)
(* Goal: @eq ghost (ghost_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) (ghost_of (m_phi jm))) (ghost_of (m_phi jm)) *)
unfold rebuild_juicy_mem_fmap.
(* Goal: @eq resource (resource_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) match resource_at (m_phi jm) loc with | NO sh rsh => if readable_perm (access_at m' loc Cur) then YES Tsh (@writable_readable Tsh writable_share_top) (VAL (contents_at m' loc)) NoneP else NO sh rsh | YES sh rsh (VAL m as k) p => if readable_perm (access_at m' loc Cur) then YES sh rsh (VAL (contents_at m' loc)) NoneP else NO Share.bot bot_unreadable | YES sh rsh (LK n i as k) p => resource_at (m_phi jm) loc | YES sh rsh (FUN f c as k) p => resource_at (m_phi jm) loc | PURE k pp => PURE k pp end) match resource_at (m_phi jm) loc with | NO sh rsh => if readable_perm (access_at m' loc Cur) then YES Tsh (@writable_readable Tsh writable_share_top) (VAL (contents_at m' loc)) NoneP else NO sh rsh | YES sh rsh (VAL m as k) p => if readable_perm (access_at m' loc Cur) then YES sh rsh (VAL (contents_at m' loc)) NoneP else NO Share.bot bot_unreadable | YES sh rsh (LK n i as k) p => resource_at (m_phi jm) loc | YES sh rsh (FUN f c as k) p => resource_at (m_phi jm) loc | PURE k pp => PURE k pp end *)
(* Goal: @eq ghost (ghost_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) (ghost_of (m_phi jm))) (ghost_of (m_phi jm)) *)
destruct (m_phi jm @ loc) eqn:?H.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
if_tac; auto.
(* Goal: @eq resource (resource_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) (PURE k p)) (PURE k p) *)
(* Goal: @eq ghost (ghost_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) (ghost_of (m_phi jm))) (ghost_of (m_phi jm)) *)
pose proof (resource_at_approx (m_phi jm) loc).
(* Goal: @eq resource (resource_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) match k with | VAL m => if readable_perm (access_at m' loc Cur) then YES sh r (VAL (contents_at m' loc)) NoneP else NO Share.bot bot_unreadable | LK n i => YES sh r k p | FUN f c => YES sh r k p end) match k with | VAL m => if readable_perm (access_at m' loc Cur) then YES sh r (VAL (contents_at m' loc)) NoneP else NO Share.bot bot_unreadable | LK n i => YES sh r k p | FUN f c => YES sh r k p end *)
(* Goal: @eq resource (resource_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) (PURE k p)) (PURE k p) *)
(* Goal: @eq ghost (ghost_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) (ghost_of (m_phi jm))) (ghost_of (m_phi jm)) *)
rewrite H in H0. simpl in H0.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
destruct k; simpl; auto.
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
if_tac; auto.
(* Goal: @eq resource (resource_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) (PURE k p)) (PURE k p) *)
(* Goal: @eq ghost (ghost_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) (ghost_of (m_phi jm))) (ghost_of (m_phi jm)) *)
pose proof (resource_at_approx (m_phi jm) loc).
(* Goal: @identity Share.t Share.Join_ba Share.bot *)
(* Goal: perm_order'' (@Some permission Nonempty) (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end (if @eq_dec Share.t Share.EqDec_share sh1 Share.bot then @None permission else @Some permission Nonempty) *)
(* Goal: perm_order'' match k with | VAL m => perm_of_sh sh3 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end match k with | VAL m => perm_of_sh sh1 | LK n i => @Some permission Nonempty | FUN f c => @Some permission Nonempty end *)
(* Goal: perm_order Nonempty Nonempty *)
rewrite H in *; auto.
(* Goal: @eq ghost (ghost_fmap (approx (@level juicy_mem juicy_mem_ageable jm)) (approx (@level juicy_mem juicy_mem_ageable jm)) (ghost_of (m_phi jm))) (ghost_of (m_phi jm)) *)
apply ghost_of_approx.
Defined.


