Require Import VST.veric.juicy_base.
Import cjoins.
Require Import VST.veric.juicy_mem.
Require Import VST.veric.juicy_mem_lemmas.
Require Import VST.veric.shares.

Module Type JUICY_MEM_OPS.
Parameter juicy_mem_store
  : juicy_mem -> memory_chunk -> block -> Z -> val -> option juicy_mem.

Parameter juicy_mem_storebytes
  : juicy_mem -> block -> Z -> list memval -> option juicy_mem.

Parameter juicy_mem_alloc
  : juicy_mem -> Z -> Z -> juicy_mem * block.

(* See comment below, "this is fixable"

Parameter juicy_mem_free
  : juicy_mem -> block -> Z -> Z -> option juicy_mem.
Axiom juicy_mem_free_succeeds: forall j j' b lo hi,
  juicy_mem_free j b lo hi = Some j'
  -> exists m', free (m_dry j) b lo hi = Some m' /\ m' = m_dry j'.

*)

Axiom juicy_mem_store_succeeds: forall j j' ch b ofs v,
  juicy_mem_store j ch b ofs v = Some j'
  -> exists m', store ch (m_dry j) b ofs v = Some m' /\ m' = m_dry j'.
Axiom juicy_mem_alloc_succeeds: forall j j' b lo hi,
  juicy_mem_alloc j lo hi = (j', b) -> (m_dry j', b) = alloc (m_dry j) lo hi.

End JUICY_MEM_OPS.

Obligation Tactic := Tactics.program_simpl.

Module JuicyMemOps <: JUICY_MEM_OPS.
Program Definition juicy_mem_store j ch b ofs v: option juicy_mem :=
  if valid_access_dec (m_dry j) ch b ofs Writable
    then Some (store_juicy_mem j _ ch b ofs v _)
    else None.
Next Obligation.
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (j j' : juicy_mem) (m : mem) (_ : VU v u) (_ : @eq mem (m_dry j) m) (_ : v j j'), @ex mem (fun m' : mem => u m m') *)
intros.
(* Goal: mem *)
apply (proj1_sig (valid_access_store (m_dry j) ch b ofs v H)).
Defined.
Next Obligation.
(* Goal: @eq (option mem) (store ch (m_dry j) b ofs v) (@Some mem (juicy_mem_store_obligation_1 j ch b ofs v H)) *)
apply (proj2_sig (valid_access_store (m_dry j) ch b ofs v H)).
Defined.

Lemma juicy_mem_store_succeeds: forall j j' ch b ofs v,
  juicy_mem_store j ch b ofs v = Some j'
  -> exists m', store ch (m_dry j) b ofs v = Some m' /\ m' = m_dry j'.
Proof.
(* Goal: forall (j j' : juicy_mem) (ch : memory_chunk) (b : block) (ofs : Z) (v : val) (_ : @eq (option juicy_mem) (juicy_mem_store j ch b ofs v) (@Some juicy_mem j')), @ex mem (fun m' : mem => and (@eq (option mem) (store ch (m_dry j) b ofs v) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
intros until v; intro H.
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (store ch (m_dry j) b ofs v) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
unfold juicy_mem_store in H.
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (store ch (m_dry j) b ofs v) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
destruct (valid_access_dec (m_dry j) ch b ofs Writable) as [H1 | H1].
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
exists (m_dry j').
(* Goal: and (@eq memval (contents_at m' loc) v) (@eq preds pp NoneP) *)
split; auto.
(* Goal: @eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem (m_dry j')) *)
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
inversion H.
(* Goal: @eq (prod mem block) (@pair mem block (m_dry (mkJuicyMem (@fst mem' block (alloc (m_dry j) lo hi)) (after_alloc lo hi (@snd mem' block (alloc (m_dry j) lo hi)) (m_phi j) (juicy_mem_alloc_aux1 j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi)))) (after_alloc_contents_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_max_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_alloc_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))))) (@snd mem' block (alloc (m_dry j) lo hi))) (alloc (m_dry j) lo hi) *)
simpl.
(* Goal: @eq (option mem) (store ch (m_dry j) b ofs v) (@Some mem (juicy_mem_store_obligation_1 j ch b ofs v H1)) *)
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (store ch (m_dry j) b ofs v) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
unfold juicy_mem_store_obligation_1.
(* Goal: @eq (option mem) (store ch (m_dry j) b ofs v) (@Some mem (@proj1_sig mem (fun m2 : mem => @eq (option mem) (store ch (m_dry j) b ofs v) (@Some mem m2)) (valid_access_store (m_dry j) ch b ofs v H1))) *)
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (store ch (m_dry j) b ofs v) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
destruct (valid_access_store (m_dry j) ch b ofs v H1).
(* Goal: @eq (prod mem block) (@pair mem block (m_dry (mkJuicyMem (@fst mem' block (alloc (m_dry j) lo hi)) (after_alloc lo hi (@snd mem' block (alloc (m_dry j) lo hi)) (m_phi j) (juicy_mem_alloc_aux1 j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi)))) (after_alloc_contents_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_max_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_alloc_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))))) (@snd mem' block (alloc (m_dry j) lo hi))) (alloc (m_dry j) lo hi) *)
simpl. auto.
(* Goal: @ex mem (fun m' : mem => u m m') *)
inv H.
Qed.

Program Definition juicy_mem_storebytes j b ofs bytes: option juicy_mem :=
  if range_perm_dec (m_dry j) b ofs (ofs + Z_of_nat (length bytes)) Cur Writable
    then Some (storebytes_juicy_mem j _ b ofs bytes _)
    else None.
Next Obligation.
(* Goal: mem *)
apply (proj1_sig (range_perm_storebytes (m_dry j) b ofs bytes H)).
Defined.
Next Obligation.
(* Goal: @eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem (juicy_mem_storebytes_obligation_1 j b ofs bytes H)) *)
apply (proj2_sig (range_perm_storebytes (m_dry j) b ofs bytes H)).
Qed.

Lemma juicy_mem_storebytes_succeeds: forall j j' b ofs bytes,
  juicy_mem_storebytes j b ofs bytes = Some j' ->
  exists m', storebytes (m_dry j) b ofs bytes = Some m' /\ m' = m_dry j'.
Proof.
(* Goal: forall (j j' : juicy_mem) (b : block) (ofs : Z) (bytes : list memval) (_ : @eq (option juicy_mem) (juicy_mem_storebytes j b ofs bytes) (@Some juicy_mem j')), @ex mem (fun m' : mem => and (@eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
intros until bytes; intro H.
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
unfold juicy_mem_storebytes in H.
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
destruct (range_perm_dec (m_dry j) b ofs (ofs + Z_of_nat (length bytes)) Cur Writable).
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
exists (m_dry j').
(* Goal: and (@eq memval (contents_at m' loc) v) (@eq preds pp NoneP) *)
split; auto.
(* Goal: @eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem (m_dry j')) *)
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
inversion H.
(* Goal: @eq (prod mem block) (@pair mem block (m_dry (mkJuicyMem (@fst mem' block (alloc (m_dry j) lo hi)) (after_alloc lo hi (@snd mem' block (alloc (m_dry j) lo hi)) (m_phi j) (juicy_mem_alloc_aux1 j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi)))) (after_alloc_contents_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_max_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_alloc_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))))) (@snd mem' block (alloc (m_dry j) lo hi))) (alloc (m_dry j) lo hi) *)
simpl.
(* Goal: @eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem (juicy_mem_storebytes_obligation_1 j b ofs bytes r)) *)
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
unfold juicy_mem_storebytes_obligation_1.
(* Goal: @eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem (@proj1_sig mem (fun m2 : mem => @eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem m2)) (range_perm_storebytes (m_dry j) b ofs bytes r))) *)
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
destruct (range_perm_storebytes (m_dry j) b ofs bytes r).
(* Goal: @eq (prod mem block) (@pair mem block (m_dry (mkJuicyMem (@fst mem' block (alloc (m_dry j) lo hi)) (after_alloc lo hi (@snd mem' block (alloc (m_dry j) lo hi)) (m_phi j) (juicy_mem_alloc_aux1 j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi)))) (after_alloc_contents_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_max_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_alloc_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))))) (@snd mem' block (alloc (m_dry j) lo hi))) (alloc (m_dry j) lo hi) *)
simpl. auto.
(* Goal: @ex mem (fun m' : mem => u m m') *)
inv H.
Qed.


Lemma pshare_sh_bot: forall p, pshare_sh p = Share.bot -> False.
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (j j' : juicy_mem) (m : mem) (_ : VU v u) (_ : @eq mem (m_dry j) m) (_ : v j j'), @ex mem (fun m' : mem => u m m') *)
Proof. destruct p; intros. simpl in H. subst x. apply nonunit_nonidentity in n.
(* Goal: False *)
apply n. apply bot_identity.
Qed.

Lemma juicy_mem_alloc_aux1:
  forall jm lo hi m' b, alloc (m_dry jm) lo hi = (m',b) ->
        forall ofs, m_phi jm @ (b,ofs) = NO Share.bot bot_unreadable.
Proof.
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (j j' : juicy_mem) (m : mem) (_ : VU v u) (_ : @eq mem (m_dry j) m) (_ : v j j'), @ex mem (fun m' : mem => u m m') *)
 intros.
(* Goal: @eq resource (resource_at (m_phi jm) (@pair block Z b ofs)) (NO Share.bot bot_unreadable) *)
 pose proof (juicy_mem_max_access jm (b,ofs)).
(* Goal: @eq resource (resource_at (m_phi jm) (@pair block Z b ofs)) (NO Share.bot bot_unreadable) *)
 unfold max_access_at in H0.
(* Goal: @eq resource (resource_at (m_phi jm) (@pair block Z b ofs)) (NO Share.bot bot_unreadable) *)
 simpl in H0.
(* Goal: False *)
 pose proof (alloc_result _ _ _ _ _ H).
(* Goal: @eq resource (resource_at (m_phi jm) (@pair block Z b ofs)) (NO Share.bot bot_unreadable) *)
 subst b.
(* Goal: @eq resource (resource_at (m_phi jm) (@pair block Z (nextblock (m_dry jm)) ofs)) (NO Share.bot bot_unreadable) *)
 destruct jm; simpl in *.
(* Goal: @eq (prod mem block) (@pair mem block (m_dry (mkJuicyMem (@fst mem' block (alloc (m_dry j) lo hi)) (after_alloc lo hi (@snd mem' block (alloc (m_dry j) lo hi)) (m_phi j) (juicy_mem_alloc_aux1 j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi)))) (after_alloc_contents_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_max_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_alloc_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))))) (@snd mem' block (alloc (m_dry j) lo hi))) (alloc (m_dry j) lo hi) *)
 rewrite JMalloc; auto; simpl.
(* Goal: Pos.ge (nextblock m) (nextblock m) *)
 xomega.
Qed.

(* Transparent alloc. *)
Lemma after_alloc_contents_cohere:
 forall jm lo hi m' b (H : alloc (m_dry jm) lo hi = (m', b)),
  contents_cohere m'
    (after_alloc lo hi b (m_phi jm) (juicy_mem_alloc_aux1 jm lo hi m' b H)).
Proof.
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (j j' : juicy_mem) (m : mem) (_ : VU v u) (_ : @eq mem (m_dry j) m) (_ : v j j'), @ex mem (fun m' : mem => u m m') *)
intros.
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (j j' : juicy_mem) (m : mem) (_ : VU v u) (_ : @eq mem (m_dry j) m) (_ : v j j'), @ex mem (fun m' : mem => u m m') *)
unfold after_alloc; hnf; intros.
(* Goal: and (@eq memval (contents_at m' loc) v) (@eq preds pp NoneP) *)
rewrite resource_at_make_rmap in H0. unfold after_alloc' in H0.
(* Goal: and (@eq memval (contents_at m' loc) v) (@eq preds pp NoneP) *)
if_tac in H0.
*
(* Goal: and (@eq memval (contents_at m' loc) v) (@eq preds pp NoneP) *)
inv H0; split; auto.
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
apply (alloc_dry_updated_on _ _ _ _ _ _ H); auto.
*
(* Goal: and (@eq memval (contents_at m' loc) v) (@eq preds pp NoneP) *)
destruct (alloc_dry_unchanged_on _ _ _ _ _ b H H1).
(* Goal: @eq (option permission) (access_at m' loc Cur) (perm_of_res (resource_at (m_phi jm) loc)) *)
pose proof (juicy_mem_access jm loc).
(* Goal: and (@eq memval (contents_at m' loc) v) (@eq preds pp NoneP) *)
rewrite H0 in H4. rewrite H4 in H3.
(* Goal: and (@eq memval (contents_at m' loc) v) (@eq preds pp NoneP) *)
spec H3.
(* Goal: not (@eq (option permission) (perm_of_res (YES rsh sh (VAL v) pp)) (@None permission)) *)
(* Goal: and (@eq memval (contents_at m' loc) v) (@eq preds pp NoneP) *)
clear.
(* Goal: @eq (prod mem block) (@pair mem block (m_dry (mkJuicyMem (@fst mem' block (alloc (m_dry j) lo hi)) (after_alloc lo hi (@snd mem' block (alloc (m_dry j) lo hi)) (m_phi j) (juicy_mem_alloc_aux1 j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi)))) (after_alloc_contents_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_max_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_alloc_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))))) (@snd mem' block (alloc (m_dry j) lo hi))) (alloc (m_dry j) lo hi) *)
unfold perm_of_res, perm_of_sh; simpl.
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
if_tac. if_tac. congruence. congruence. rewrite if_true by auto. congruence.
(* Goal: and (@eq memval (contents_at m' loc) v) (@eq preds pp NoneP) *)
destruct (juicy_mem_contents jm _ _ _ _ _ H0).
(* Goal: and (@eq memval (contents_at m' loc) v) (@eq preds pp NoneP) *)
split; auto.
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
rewrite <- H3; auto.
Qed.

Lemma after_alloc_access_cohere:
 forall jm lo hi m' b (H : alloc (m_dry jm) lo hi = (m', b)),
 access_cohere m'
  (after_alloc lo hi b (m_phi jm) (juicy_mem_alloc_aux1 jm lo hi m' b H)).
Proof.
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (j j' : juicy_mem) (m : mem) (_ : VU v u) (_ : @eq mem (m_dry j) m) (_ : v j j'), @ex mem (fun m' : mem => u m m') *)
intros; hnf; intros.
(* Goal: @eq resource (resource_at (after_alloc lo hi b (m_phi jm) (juicy_mem_alloc_aux1 jm lo hi m' b H)) loc) (NO Share.bot bot_unreadable) *)
unfold after_alloc. rewrite resource_at_make_rmap.
(* Goal: @eq resource (after_alloc' lo hi (@snd mem' block (alloc (m_dry jm) lo hi)) (m_phi jm) (juicy_mem_alloc_aux1 jm lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry jm)) (@ZMap.init memval Undef) (mem_contents (m_dry jm))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry jm)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry jm))) (Pos.succ (nextblock (m_dry jm))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry jm) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry jm))))) => Memory.Mem.alloc_obligation_2 (m_dry jm) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry jm) b)) (nextblock (m_dry jm)) (@eq_refl (prod mem' block) (alloc (m_dry jm) lo hi))) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
unfold after_alloc'.
(* Goal: @eq (option permission) (access_at m' loc Cur) (perm_of_res (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc)) *)
if_tac.
*
(* Goal: @eq (prod mem block) (@pair mem block (m_dry (mkJuicyMem (@fst mem' block (alloc (m_dry j) lo hi)) (after_alloc lo hi (@snd mem' block (alloc (m_dry j) lo hi)) (m_phi j) (juicy_mem_alloc_aux1 j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi)))) (after_alloc_contents_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_max_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_alloc_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))))) (@snd mem' block (alloc (m_dry j) lo hi))) (alloc (m_dry j) lo hi) *)
unfold perm_of_res; simpl.   rewrite perm_of_freeable.
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
apply (alloc_dry_updated_on _ _ _ _ _ _ H); auto.
*
(* Goal: @eq (option permission) (access_at m' loc Cur) (perm_of_res (resource_at (m_phi jm) loc)) *)
destruct (alloc_dry_unchanged_on _ _ _ _ _ b H H0).
(* Goal: @eq (option permission) (access_at m' loc Cur) (perm_of_res (resource_at (m_phi jm) loc)) *)
pose proof (juicy_mem_access jm loc).
(* Goal: @eq (option permission) (access_at m' loc Cur) (perm_of_res (resource_at (m_phi jm) loc)) *)
congruence.
Qed.

Lemma after_alloc_max_access_cohere:
 forall jm lo hi m' b (H : alloc (m_dry jm) lo hi = (m', b)),
 max_access_cohere m'
  (after_alloc lo hi b (m_phi jm) (juicy_mem_alloc_aux1 jm lo hi m' b H)).
Proof.

(* Goal: forall (v : relation juicy_mem) (u : relation mem) (j j' : juicy_mem) (m : mem) (_ : VU v u) (_ : @eq mem (m_dry j) m) (_ : v j j'), @ex mem (fun m' : mem => u m m') *)
intros; pose proof I; hnf; intros.
(* Goal: @eq resource (resource_at (after_alloc lo hi b (m_phi jm) (juicy_mem_alloc_aux1 jm lo hi m' b H)) loc) (NO Share.bot bot_unreadable) *)
unfold after_alloc. rewrite resource_at_make_rmap.
(* Goal: @eq resource (after_alloc' lo hi (@snd mem' block (alloc (m_dry jm) lo hi)) (m_phi jm) (juicy_mem_alloc_aux1 jm lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry jm)) (@ZMap.init memval Undef) (mem_contents (m_dry jm))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry jm)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry jm))) (Pos.succ (nextblock (m_dry jm))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry jm) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry jm))))) => Memory.Mem.alloc_obligation_2 (m_dry jm) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry jm) b)) (nextblock (m_dry jm)) (@eq_refl (prod mem' block) (alloc (m_dry jm) lo hi))) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
unfold after_alloc'.
(* Goal: @eq (option permission) (access_at m' loc Cur) (perm_of_res (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc)) *)
if_tac.
*
(* Goal: @eq (option permission) (access_at m' loc Cur) (perm_of_sh Share.top) *)
 simpl; rewrite perm_of_freeable.
 destruct loc. destruct H1. subst b0.
 unfold max_access_at.
 rewrite (alloc_access_same _ _ _ _ _ H) by omega.
(* Goal: @StratifiedSemantics juicy_mem AbsPrimcom AbsPrimexpr mem ConcPrimcom ConcPrimexpr abstract concrete m_dry VU GF *)
 constructor.
*
  assert (HH:= juicy_mem_max_access jm loc).

(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
    eapply perm_order''_trans; eauto.
    unfold max_access_at in *.
    destruct loc as [b' z].
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
    rewrite (alloc_access_other _ _ _ _ _ H); auto.

    destruct ((access_at m' (b', z) Max)); [apply perm_refl |constructor].
    destruct (eq_block b b').
    right. assert (~(lo <= z < lo + (hi - lo))).
(* Goal: and (@eq memval (contents_at m' loc) v) (@eq preds pp NoneP) *)
    { intros HHH; apply H1. split; auto. }
(* Goal: Pos.ge (nextblock m) (nextblock m) *)
    xomega.
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
    left; auto.
Qed.

Lemma after_alloc_alloc_cohere:
 forall jm lo hi m' b (H : alloc (m_dry jm) lo hi = (m', b)),
 alloc_cohere m'
  (after_alloc lo hi b (m_phi jm) (juicy_mem_alloc_aux1 jm lo hi m' b H)).
Proof.
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (j j' : juicy_mem) (m : mem) (_ : VU v u) (_ : @eq mem (m_dry j) m) (_ : v j j'), @ex mem (fun m' : mem => u m m') *)
intros; hnf; intros.
(* Goal: @eq resource (resource_at (after_alloc lo hi b (m_phi jm) (juicy_mem_alloc_aux1 jm lo hi m' b H)) loc) (NO Share.bot bot_unreadable) *)
unfold after_alloc.
(* Goal: @eq resource (resource_at (@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) (after_alloc' lo hi b (m_phi jm) (juicy_mem_alloc_aux1 jm lo hi m' b H))) (@eq ghost (ghost_of phi) (ghost_of (m_phi jm))))) (make_rmap (after_alloc' lo hi b (m_phi jm) (juicy_mem_alloc_aux1 jm lo hi m' b H)) (ghost_of (m_phi jm)) (@level rmap ag_rmap (m_phi jm)) (after_alloc'_ok lo hi b (m_phi jm) (juicy_mem_alloc_aux1 jm lo hi m' b H)) (ghost_of_approx (m_phi jm)))) loc) (NO Share.bot bot_unreadable) *)
rewrite resource_at_make_rmap.
(* Goal: @eq resource (after_alloc' lo hi (@snd mem' block (alloc (m_dry jm) lo hi)) (m_phi jm) (juicy_mem_alloc_aux1 jm lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry jm)) (@ZMap.init memval Undef) (mem_contents (m_dry jm))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry jm)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry jm))) (Pos.succ (nextblock (m_dry jm))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry jm) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry jm))))) => Memory.Mem.alloc_obligation_2 (m_dry jm) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry jm) b)) (nextblock (m_dry jm)) (@eq_refl (prod mem' block) (alloc (m_dry jm) lo hi))) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
unfold after_alloc'.
(* Goal: @eq resource (if adr_range_dec (@pair block Z b lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (NO Share.bot bot_unreadable) *)
rewrite if_false.
(* Goal: @eq resource (resource_at (m_phi jm) loc) (NO Share.bot bot_unreadable) *)
(* Goal: not (adr_range (@pair block Z b lo) (Z.sub hi lo) loc) *)
apply (juicy_mem_alloc_cohere jm loc).
(* Goal: Pos.ge (@fst positive Z loc) (nextblock (m_dry jm)) *)
(* Goal: not (adr_range (@pair block Z b lo) (Z.sub hi lo) loc) *)
rewrite (nextblock_alloc _ _ _ _ _ H) in H0.
(* Goal: Pos.ge (@fst positive Z loc) (nextblock (m_dry jm)) *)
(* Goal: not (adr_range (@pair block Z b lo) (Z.sub hi lo) loc) *)
zify. omega.
destruct loc as [b' z']; simpl in *; intros [? ?]; subst b'.
(* Goal: False *)
pose proof (alloc_result _ _ _ _ _ H).
(* Goal: False *)
pose proof (nextblock_alloc _ _ _ _ _ H).
(* Goal: False *)
rewrite <- H1 in H3.
(* Goal: False *)
rewrite H3 in H0.
(* Goal: False *)
clear - H0.
(* Goal: Z.ge (Zpos (@fst positive Z loc)) (Zpos (nextblock (m_dry jm))) *)
(* Goal: not (adr_range (@pair block Z b lo) (Z.sub hi lo) loc) *)
zify; omega.
Qed.

Definition juicy_mem_alloc (jm: juicy_mem) (lo hi: Z) : juicy_mem * block :=
         (mkJuicyMem (fst (alloc (m_dry jm) lo hi))
                     (after_alloc lo hi (snd (alloc (m_dry jm) lo hi)) (m_phi jm)
                            (juicy_mem_alloc_aux1 _ _ _ _ _ (eq_refl _)))
                     (after_alloc_contents_cohere _ _ _ _ _ (eq_refl _))
                     (after_alloc_access_cohere _ _ _ _ _ (eq_refl _))
                     (after_alloc_max_access_cohere _ _ _ _ _ (eq_refl _))
                     (after_alloc_alloc_cohere _ _ _ _ _ (eq_refl _)),
           snd (alloc (m_dry jm) lo hi)).

Lemma juicy_mem_alloc_at:
  forall jm lo hi jm' b,
     juicy_mem_alloc jm lo hi = (jm',b) ->
     forall loc, m_phi jm' @ loc =
       if adr_range_dec (b, lo) (hi - lo) loc
       then YES Share.top readable_share_top (VAL Undef) NoneP
       else m_phi jm @ loc.
Proof.
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (j j' : juicy_mem) (m : mem) (_ : VU v u) (_ : @eq mem (m_dry j) m) (_ : v j j'), @ex mem (fun m' : mem => u m m') *)
 intros.
(* Goal: @eq (prod mem block) (@pair mem block (m_dry (mkJuicyMem (@fst mem' block (alloc (m_dry j) lo hi)) (after_alloc lo hi (@snd mem' block (alloc (m_dry j) lo hi)) (m_phi j) (juicy_mem_alloc_aux1 j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi)))) (after_alloc_contents_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_max_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_alloc_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))))) (@snd mem' block (alloc (m_dry j) lo hi))) (alloc (m_dry j) lo hi) *)
 inv H. simpl.
(* Goal: @eq resource (resource_at (@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) (after_alloc' lo hi b (m_phi jm) (juicy_mem_alloc_aux1 jm lo hi m' b H))) (@eq ghost (ghost_of phi) (ghost_of (m_phi jm))))) (make_rmap (after_alloc' lo hi b (m_phi jm) (juicy_mem_alloc_aux1 jm lo hi m' b H)) (ghost_of (m_phi jm)) (@level rmap ag_rmap (m_phi jm)) (after_alloc'_ok lo hi b (m_phi jm) (juicy_mem_alloc_aux1 jm lo hi m' b H)) (ghost_of_approx (m_phi jm)))) loc) (NO Share.bot bot_unreadable) *)
 unfold after_alloc; rewrite resource_at_make_rmap.
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
 unfold after_alloc'. auto.
Qed.

Lemma juicy_mem_alloc_level:
 forall jm lo hi jm' b,
   juicy_mem_alloc jm lo hi = (jm', b) -> level jm = level jm'.
Proof.
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (j j' : juicy_mem) (m : mem) (_ : VU v u) (_ : @eq mem (m_dry j) m) (_ : v j j'), @ex mem (fun m' : mem => u m m') *)
 unfold juicy_mem_alloc; intros.
(* Goal: @ex mem (fun m' : mem => u m m') *)
 inv H.
(* Goal: @eq (prod mem block) (@pair mem block (m_dry (mkJuicyMem (@fst mem' block (alloc (m_dry j) lo hi)) (after_alloc lo hi (@snd mem' block (alloc (m_dry j) lo hi)) (m_phi j) (juicy_mem_alloc_aux1 j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi)))) (after_alloc_contents_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_max_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_alloc_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))))) (@snd mem' block (alloc (m_dry j) lo hi))) (alloc (m_dry j) lo hi) *)
 unfold after_alloc; simpl. rewrite level_make_rmap; auto.
Qed.

Lemma juicy_mem_alloc_succeeds: forall j j' b lo hi,
  juicy_mem_alloc j lo hi = (j', b) -> (m_dry j', b) = alloc (m_dry j) lo hi.
Proof.
(* Goal: forall (j j' : juicy_mem) (b : block) (lo hi : Z) (_ : @eq (prod juicy_mem block) (juicy_mem_alloc j lo hi) (@pair juicy_mem block j' b)), @eq (prod mem block) (@pair mem block (m_dry j') b) (alloc (m_dry j) lo hi) *)
intros until hi; intro H.
(* Goal: @eq (prod mem block) (@pair mem block (m_dry j') b) (alloc (m_dry j) lo hi) *)
unfold juicy_mem_alloc in H.
(* Goal: @ex mem (fun m' : mem => u m m') *)
inv H.
(* Goal: @eq (prod mem block) (@pair mem block (m_dry (mkJuicyMem (@fst mem' block (alloc (m_dry j) lo hi)) (after_alloc lo hi (@snd mem' block (alloc (m_dry j) lo hi)) (m_phi j) (juicy_mem_alloc_aux1 j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi)))) (after_alloc_contents_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_max_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_alloc_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))))) (@snd mem' block (alloc (m_dry j) lo hi))) (alloc (m_dry j) lo hi) *)
simpl.
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
simpl; auto.
Qed.

(* This is fixable, as long as we replace range_perm_dec
  with something based on the PERM argument of free_juicy_mem ...
Program Definition juicy_mem_free j b lo hi: option juicy_mem :=
  if range_perm_dec (m_dry j) b lo hi Cur Freeable
    then Some (free_juicy_mem j _ b lo hi _ _)
    else None.
Next Obligation.
apply (proj1_sig (range_perm_free (m_dry j) b lo hi H)).
Defined.
Next Obligation.
apply (proj2_sig (range_perm_free (m_dry j) b lo hi H)).
Defined.
Next Obligation.
pose proof (juicy_mem_access j (b,ofs)).
specialize (H ofs).
spec H; [ omega | ].
hnf in H. unfold access_at in H2.
simpl in *.
destruct ((mem_access (m_dry j)) !! b ofs Cur); try contradiction.
(* Goal: @ex mem (fun m' : mem => u m m') *)
destruct p; inv H.
(* Goal: @ex mem (fun m' : mem => u m m') *)
inv H.
hnf in H.

Lemma juicy_mem_free_succeeds: forall j j' b lo hi,
  juicy_mem_free j b lo hi = Some j'
  -> exists m', free (m_dry j) b lo hi = Some m' /\ m' = m_dry j'.
Proof.
(* Goal: forall (j j' : juicy_mem) (b : block) (lo hi : Z) (_ : @eq (prod juicy_mem block) (juicy_mem_alloc j lo hi) (@pair juicy_mem block j' b)), @eq (prod mem block) (@pair mem block (m_dry j') b) (alloc (m_dry j) lo hi) *)
intros until hi; intro H.
unfold juicy_mem_free in H.
destruct (range_perm_dec (m_dry j) b lo hi Cur Freeable) as [H1 | H1].
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
exists (m_dry j').
(* Goal: and (@eq memval (contents_at m' loc) v) (@eq preds pp NoneP) *)
split; auto.
(* Goal: @eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem (m_dry j')) *)
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
inversion H.
unfold juicy_mem_free_obligation_1 in *.
clear H H2.
(* Goal: @eq (prod mem block) (@pair mem block (m_dry (mkJuicyMem (@fst mem' block (alloc (m_dry j) lo hi)) (after_alloc lo hi (@snd mem' block (alloc (m_dry j) lo hi)) (m_phi j) (juicy_mem_alloc_aux1 j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi)))) (after_alloc_contents_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_max_access_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))) (after_alloc_alloc_cohere j lo hi (mkmem (@PMap.set (prod memval (PTree.t memval)) (nextblock (m_dry j)) (@ZMap.init memval Undef) (mem_contents (m_dry j))) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (nextblock (m_dry j)) (fun (ofs : Z) (_ : perm_kind) => if 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)) then @Some permission Freeable else @None permission) (mem_access (m_dry j))) (Pos.succ (nextblock (m_dry j))) (fun (b : positive) (ofs : Z) => Memory.Mem.alloc_obligation_1 (m_dry j) lo hi b ofs) (fun (b : positive) (ofs : Z) (k : perm_kind) (H : not (Coqlib.Plt b (Pos.succ (nextblock (m_dry j))))) => Memory.Mem.alloc_obligation_2 (m_dry j) lo hi b ofs k H) (fun b : positive => Memory.Mem.alloc_obligation_3 (m_dry j) b)) (nextblock (m_dry j)) (@eq_refl (prod mem' block) (alloc (m_dry j) lo hi))))) (@snd mem' block (alloc (m_dry j) lo hi))) (alloc (m_dry j) lo hi) *)
simpl.
destruct (range_perm_free (m_dry j) b lo hi H1).
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
simpl in *; subst; auto.
(* Goal: @eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem (m_dry j')) *)
(* Goal: @ex mem (fun m' : mem => and (@eq (option mem) (storebytes (m_dry j) b ofs bytes) (@Some mem m')) (@eq mem m' (m_dry j'))) *)
inversion H.
Qed.
*)

End JuicyMemOps.


(* Here we construct an instance of StratifiedSemanticsWithSeparation using
   the juicy mem operations. *)
Module Abs := JuicyMemOps.
Require Import VST.veric.local.

Inductive AbsPrimcom : relation juicy_mem -> Prop :=
| AbsPrimcom_store : forall ch b ofs v,
  AbsPrimcom (fun j j' => Abs.juicy_mem_store j ch b ofs v = Some j')
| AbsPrimcom_alloc : forall lo hi,
  AbsPrimcom (fun j j' => fst (Abs.juicy_mem_alloc j lo hi) = j')
(*
| AbsPrimcom_free : forall b ofs n,
  AbsPrimcom (fun j j' => Abs.juicy_mem_free j b ofs n = Some j').
*).
Inductive AbsPrimexpr : pfunc juicy_mem val -> Prop :=.

Instance abstract : GenericSemantics juicy_mem AbsPrimcom AbsPrimexpr := {}.

Inductive ConcPrimcom : relation mem -> Prop :=
| ConcPrimcom_store : forall ch b ofs v,
  ConcPrimcom (fun m m' => store ch m b ofs v = Some m')
| ConcPrimcom_alloc : forall lo hi,
  ConcPrimcom (fun m m' => fst (alloc m lo hi) = m')
| ConcPrimcom_free : forall b ofs n,
  ConcPrimcom (fun m m' => free m b ofs n = Some m').

Inductive ConcPrimexpr : pfunc mem val -> Prop :=.

Instance concrete : GenericSemantics mem ConcPrimcom ConcPrimexpr := {}.

Inductive VU : relation juicy_mem -> relation mem -> Prop :=
| VU_store : forall ch b ofs v,
  VU (fun j j' => Abs.juicy_mem_store j ch b ofs v = Some j')
     (fun m m' => store ch m b ofs v = Some m')
| VU_alloc : forall lo hi,
  VU (fun j j' => fst (Abs.juicy_mem_alloc j lo hi) = j')
     (fun m m' => fst (alloc m lo hi) = m')
(*| VU_free : forall b ofs n,
  VU (fun j j' => Abs.juicy_mem_free j b ofs n = Some j')
     (fun m m' => free m b ofs n = Some m')*).

Inductive GF : pfunc juicy_mem val -> pfunc mem val -> Prop :=.

Lemma PrimexprErasure : forall g f, GF g f -> False. Proof. inversion 1. Qed.

Lemma PrimexprSafety : forall g f, GF g f -> False. Proof. inversion 1. Qed.

Lemma PrimcomErasure : forall v u j j' m m',
  VU v u -> m_dry j = m -> v j j' -> u m m' -> m_dry j' = m'.
Proof.
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (j j' : juicy_mem) (m : mem) (_ : VU v u) (_ : @eq mem (m_dry j) m) (_ : v j j'), @ex mem (fun m' : mem => u m m') *)
intros.
(* Goal: @ex mem (fun m' : mem => u m m') *)
inv H.
(* store *)
(* Goal: @ex mem (fun m' : mem => @eq (option mem) (store ch (m_dry j) b ofs v0) (@Some mem m')) *)
(* Goal: @ex mem (fun m' : mem => @eq mem' (@fst mem' block (alloc (m_dry j) lo hi)) m') *)
apply JuicyMemOps.juicy_mem_store_succeeds in H1.
(* Goal: @ex mem (fun m' : mem => @eq (option mem) (store ch (m_dry j) b ofs v0) (@Some mem m')) *)
(* Goal: @ex mem (fun m' : mem => @eq mem' (@fst mem' block (alloc (m_dry j) lo hi)) m') *)
destruct H1 as [? [? ?]]; subst.
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
rewrite H in H2; inv H2; auto.
(* alloc *)
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (j j' : juicy_mem) (m : mem) (_ : VU v u) (_ : @eq mem (m_dry j) m) (_ : v j j'), @ex mem (fun m' : mem => u m m') *)
generalize JuicyMemOps.juicy_mem_alloc_succeeds; intros.
(* Goal: @ex mem (fun m' : mem => @eq mem' (@fst mem' block (alloc (m_dry j) lo hi)) m') *)
specialize (H j j' (snd (JuicyMemOps.juicy_mem_alloc j lo hi)) lo hi).
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (j j' : juicy_mem) (m : mem) (_ : VU v u) (_ : @eq mem (m_dry j) m) (_ : v j j'), @ex mem (fun m' : mem => u m m') *)
case_eq (JuicyMemOps.juicy_mem_alloc j lo hi); intros.
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
rewrite H0 in *. spec H; auto. simpl in *.
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
destruct (alloc (m_dry j) lo hi); simpl in *. inv H; auto.
(* free *)
(*apply JuicyMemOps.juicy_mem_free_succeeds in H1.
destruct H1 as [? [? ?]].
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
subst. rewrite H in H2; inv H2; auto.
*)
Qed.

Lemma PrimcomSafety : forall v u j j' m,
  VU v u -> m_dry j = m -> v j j' -> exists m', u m m'.
Proof.
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (j j' : juicy_mem) (m : mem) (_ : VU v u) (_ : @eq mem (m_dry j) m) (_ : v j j'), @ex mem (fun m' : mem => u m m') *)
intros.
(* Goal: @ex mem (fun m' : mem => u m m') *)
inv H.
(* store *)
(* Goal: @ex mem (fun m' : mem => @eq (option mem) (store ch (m_dry j) b ofs v0) (@Some mem m')) *)
(* Goal: @ex mem (fun m' : mem => @eq mem' (@fst mem' block (alloc (m_dry j) lo hi)) m') *)
apply JuicyMemOps.juicy_mem_store_succeeds in H1.
(* Goal: @ex mem (fun m' : mem => @eq (option mem) (store ch (m_dry j) b ofs v0) (@Some mem m')) *)
(* Goal: @ex mem (fun m' : mem => @eq mem' (@fst mem' block (alloc (m_dry j) lo hi)) m') *)
destruct H1 as [? [? ?]]; subst.
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
eexists; eauto.
(* alloc *)
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (j j' : juicy_mem) (m : mem) (_ : VU v u) (_ : @eq mem (m_dry j) m) (_ : v j j'), @ex mem (fun m' : mem => u m m') *)
generalize JuicyMemOps.juicy_mem_alloc_succeeds; intros.
(* Goal: @ex mem (fun m' : mem => @eq mem' (@fst mem' block (alloc (m_dry j) lo hi)) m') *)
specialize (H j j' (snd (JuicyMemOps.juicy_mem_alloc j lo hi)) lo hi).
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (j j' : juicy_mem) (m : mem) (_ : VU v u) (_ : @eq mem (m_dry j) m) (_ : v j j'), @ex mem (fun m' : mem => u m m') *)
case_eq (JuicyMemOps.juicy_mem_alloc j lo hi); intros.
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
rewrite H0 in *. spec H; auto. simpl in *.
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
destruct (alloc (m_dry j) lo hi); simpl in *. inv H; auto.
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
eexists; eauto.
(* free *)
(*apply JuicyMemOps.juicy_mem_free_succeeds in H1.
destruct H1 as [? [? ?]].
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
subst. eexists; eauto.
*)
Qed.

Existing Instance abstract.
Existing Instance concrete.

Instance stratsem : @StratifiedSemantics
  juicy_mem
  AbsPrimcom
  AbsPrimexpr
  mem
  ConcPrimcom
  ConcPrimexpr
  abstract
  concrete
  m_dry
  VU
  GF.
Proof.
(* Goal: @StratifiedSemantics juicy_mem AbsPrimcom AbsPrimexpr mem ConcPrimcom ConcPrimexpr abstract concrete m_dry VU GF *)
constructor.
(* Goal: @StratifiedSemantics juicy_mem AbsPrimcom AbsPrimexpr mem ConcPrimcom ConcPrimexpr abstract concrete m_dry VU GF *)
intros; inv H; split; constructor.
(* Goal: @StratifiedSemantics juicy_mem AbsPrimcom AbsPrimexpr mem ConcPrimcom ConcPrimexpr abstract concrete m_dry VU GF *)
intros; inv H; split; constructor.
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (w w' : juicy_mem) (s s' : mem) (_ : VU v u) (_ : @eq mem (m_dry w) s) (_ : v w w') (_ : u s s'), @eq mem (m_dry w') s' *)
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (w w' : juicy_mem) (s : mem) (_ : VU v u) (_ : @eq mem (m_dry w) s) (_ : v w w'), @ex mem (fun s' : mem => u s s') *)
(* Goal: forall (g : pfunc juicy_mem val) (f : pfunc mem val) (b1 b2 : val) (w : juicy_mem) (s : mem) (_ : GF g f) (_ : @eq mem (m_dry w) s) (_ : @exprEval juicy_mem AbsPrimexpr (@EPrim juicy_mem g) w b1) (_ : @exprEval mem ConcPrimexpr (@EPrim mem f) s b2), @eq val b1 b2 *)
(* Goal: forall (g : pfunc juicy_mem val) (f : pfunc mem val) (b1 : val) (w : juicy_mem) (s : mem) (_ : GF g f) (_ : @eq mem (m_dry w) s) (_ : @exprEval juicy_mem AbsPrimexpr (@EPrim juicy_mem g) w b1), @ex val (fun b2 : val => @exprEval mem ConcPrimexpr (@EPrim mem f) s b2) *)
apply PrimcomErasure.
(* Goal: forall (v : relation juicy_mem) (u : relation mem) (w w' : juicy_mem) (s : mem) (_ : VU v u) (_ : @eq mem (m_dry w) s) (_ : v w w'), @ex mem (fun s' : mem => u s s') *)
(* Goal: forall (g : pfunc juicy_mem val) (f : pfunc mem val) (b1 b2 : val) (w : juicy_mem) (s : mem) (_ : GF g f) (_ : @eq mem (m_dry w) s) (_ : @exprEval juicy_mem AbsPrimexpr (@EPrim juicy_mem g) w b1) (_ : @exprEval mem ConcPrimexpr (@EPrim mem f) s b2), @eq val b1 b2 *)
(* Goal: forall (g : pfunc juicy_mem val) (f : pfunc mem val) (b1 : val) (w : juicy_mem) (s : mem) (_ : GF g f) (_ : @eq mem (m_dry w) s) (_ : @exprEval juicy_mem AbsPrimexpr (@EPrim juicy_mem g) w b1), @ex val (fun b2 : val => @exprEval mem ConcPrimexpr (@EPrim mem f) s b2) *)
apply PrimcomSafety.
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
intros; elimtype False; eapply PrimexprErasure; eauto.
(* Goal: @eq resource (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) (if adr_range_dec (@pair block Z (@snd mem' block (alloc (m_dry jm) lo hi)) lo) (Z.sub hi lo) loc then YES Share.top readable_share_top (VAL Undef) NoneP else resource_at (m_phi jm) loc) *)
intros; elimtype False; eapply PrimexprSafety; eauto.
Qed.

Existing Instance stratsem.

Require Import VST.veric.compcert_rmaps.

Inductive RmapPrimexpr : pfunc rmap val -> Prop :=.

Inductive HG : pfunc rmap val -> pfunc juicy_mem val -> Prop :=.

Instance stratsemsep : StratifiedSemanticsWithSeparation m_phi RmapPrimexpr HG.
Proof.
(* Goal: @ex mem (fun m' : mem => u m m') *)
constructor; intros; inv H.
Qed.

(*Lenb: moved alloc_juicy_variables, juicy_mem_alloc_core, and alloc_juicy_variables_e to veric/semax_call.v*)