Require Import VST.msl.log_normalize.
Require Export VST.veric.base.
Require Import VST.veric.rmaps.
Require Import VST.veric.compcert_rmaps.  
Require Import VST.veric.shares. 
Require Import VST.veric.address_conflict.

Import RML. Import R.
Local Open Scope pred.


Program Definition kind_at (k: kind) (l: address) : pred rmap :=
   fun m => exists rsh, exists sh, exists pp, m @ l = YES rsh sh k pp.
 Next Obligation.
(* Goal: @hereditary rmap (@age rmap ag_rmap) (fun phi : rmap => @eq resource (resource_at phi l) (YES sh rsh k (preds_fmap (approx (@level rmap ag_rmap phi)) (approx (@level rmap ag_rmap phi)) pp))) *)
   try intro; intros.
(* Goal: @ex Share.t (fun rsh : Share.t => @ex (readable_share rsh) (fun sh : readable_share rsh => @ex preds (fun pp : preds => @eq resource (resource_at a' l) (YES rsh sh k pp)))) *)
   destruct H0 as [rsh [sh [pp ?]]].
(* Goal: @ex Share.t (fun rsh : Share.t => @ex (readable_share rsh) (fun sh : readable_share rsh => @ex preds (fun pp : preds => @eq resource (resource_at a' l) (YES rsh sh k pp)))) *)
   generalize (eq_sym (resource_at_approx a l)); intro.
(* Goal: forall i : nat, @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
   generalize (age1_resource_at a a'  H l (a@l) H1); intro.
(* Goal: @ex Share.t (fun rsh : Share.t => @ex (readable_share rsh) (fun sh : readable_share rsh => @ex preds (fun pp : preds => @eq resource (resource_at a' l) (YES rsh sh k pp)))) *)
   rewrite H0 in H2. simpl in H2. eauto.
 Qed.

Definition spec : Type :=  forall (sh: Share.t) (l: AV.address), pred rmap.

Program Definition yesat_raw (pp: preds) (k: kind) 
                           (sh: share) (rsh: readable_share sh) (l: address) : pred rmap :=
   fun phi => phi @ l = YES sh rsh k (preds_fmap (approx (level phi)) (approx (level phi)) pp).
  Next Obligation.
(* Goal: @hereditary rmap (@age rmap ag_rmap) (fun phi : rmap => @eq resource (resource_at phi l) (YES sh rsh k (preds_fmap (approx (@level rmap ag_rmap phi)) (approx (@level rmap ag_rmap phi)) pp))) *)
   try intro; intros.
(* Goal: @eq resource (resource_at a' l) (YES sh rsh k (preds_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) pp)) *)
   apply (age1_resource_at a a' H l (YES sh rsh k pp) H0).
  Qed.

Obligation Tactic := idtac.

Program Definition yesat (pp: preds) (k: kind) : spec :=
 fun (sh: share) (l: AV.address) (m: rmap) =>
  exists rsh, yesat_raw pp k sh rsh l m.
  Next Obligation.
(* Goal: forall (_ : memory_chunk) (_ : address) (_ : val) (_ : list memval) (_ : address), (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) *)
    intros; intro; intros.
(* Goal: @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (resource_at a' l)) (resource_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (YES sh rsh k pp))) *)
    destruct H0 as [p ?]; exists p.
(* Goal: @app_pred rmap ag_rmap (yesat_raw pp k sh p l) a' *)
    apply pred_hereditary with a; auto.
  Qed.

Program Definition pureat (pp: preds) (k: kind) (l: AV.address): pred rmap :=
       fun phi => phi @ l = PURE k (preds_fmap (approx (level phi)) (approx (level phi)) pp).
  Next Obligation.
(* Goal: forall (_ : memory_chunk) (_ : address) (_ : val) (_ : list memval) (_ : address), (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) *)
    intros; intro; intros.
(* Goal: @eq resource (resource_at a' l) (PURE k (preds_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) pp)) *)
   apply (age1_resource_at a a' H l (PURE k pp) H0).
  Qed.

Ltac do_map_arg :=
match goal with |- ?a = ?b =>
  match a with context [map ?x _] =>
    match b with context [map ?y _] => replace y with x; auto end end end.


Lemma yesat_raw_eq_aux:
  forall pp k rsh sh l,
    hereditary age
    (fun phi : rmap =>
     resource_fmap (approx (level phi)) (approx (level phi)) (phi @ l) =
     resource_fmap (approx (level phi)) (approx (level phi)) (YES rsh sh k pp)).
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
 intros.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intro; intros.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (resource_at a' l)) (resource_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (YES rsh sh k pp)) *)
  generalize (resource_at_approx a l); intro.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (resource_at a' l)) (resource_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (YES rsh sh k pp)) *)
  generalize (resource_at_approx a' l); intro.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (resource_at a' l)) (resource_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (YES rsh sh k pp)) *)
  rewrite H2.
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat y (@level A H w'))) *)
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
  rewrite H1 in H0.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  apply (age1_resource_at a a'  H); auto.
Qed.

Lemma yesat_raw_eq: yesat_raw =
  fun pp k rsh sh l =>
  ((exist (hereditary age)
   (fun phi =>
   resource_fmap (approx (level phi)) (approx (level phi)) (phi @ l) =
   resource_fmap (approx (level phi)) (approx (level phi)) (YES rsh sh k pp))
   (yesat_raw_eq_aux pp k rsh sh l)) : pred rmap).
Proof.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (yesat_raw NoneP (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) sh p l') m) (@ex AV.kind (fun k : AV.kind => and (@eq kind k (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v)))) (@eq resource (resource_at m l') (YES sh p k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) NoneP))))) *)
unfold yesat_raw.
extensionality pp k rsh sh l.
(* Goal: @eq (@sig (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p)) (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => @ex (readable_share sh) (fun rsh : readable_share sh => @app_pred rmap ag_rmap (yesat_raw pp k sh rsh l) m)) (yesat_obligation_1 pp k sh l)) (@exist (forall _ : rmap, Prop) (@hereditary rmap (@age rmap ag_rmap)) (fun m : rmap => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) (resource_at m l)) (resource_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) (YES sh rsh k pp)))) (yesat_eq_aux pp k sh l)) *)
apply exist_ext.
extensionality phi.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
apply prop_ext; split; intros.
rewrite H.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
simpl.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
f_equal.
rewrite preds_fmap_fmap.
rewrite approx_oo_approx.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
auto.
(* Goal: @eq memval m m0 *)
(* Goal: @eq (list memval) b1 b2 *)
simpl in H.
revert H; case_eq (phi @ l); simpl; intros; inv H0.
f_equal; try apply proof_irr.
revert H4; destruct p as [?A ?p]; destruct pp as [?A ?p]; simpl; intros; auto; inv H4.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
clear - H.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
repeat f_equal.
revert H; unfold resource_at.  rewrite rmap_level_eq.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
case_eq (unsquash phi); simpl; intros.
rename r0 into f.
(* Goal: @ex rmap (fun w : rmap => and (@app_pred rmap ag_rmap (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) (decode_val ch (encode_val ch v))) (Z.divide (align_chunk ch) (@snd block Z loc))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun loc0 : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc0) (@snd block Z loc))) bl Undef)) sh loc0) noat))) noghost)) w) (@eq rmap (@core rmap Join_rmap Sep_rmap w) (@core rmap Join_rmap Sep_rmap w0))) *)
pose proof I.
set (phi' := ((fun l' => if eq_dec l' l 
       then YES rsh r k (SomeP A0 (fun i => fmap _ (approx n) (approx n) (p i))) else fst f l', snd f)): rmap').
assert (phi = squash (n,phi')).
apply unsquash_inj.
replace (unsquash phi) with (unsquash (squash (unsquash phi))).
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
2: rewrite squash_unsquash; auto.
rewrite H.
do 2 rewrite unsquash_squash.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
f_equal.
unfold phi'.
clear - H0.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
simpl.
unfold rmap_fmap.
unfold compose.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
f_equal.
(* Goal: @eq (forall _ : A, @pred rmap ag_rmap) (@compose A (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) p) (@compose A (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) a) *)
extensionality x.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
simpl.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
if_tac; auto.
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
subst.
(* Goal: @eq (option share) (resource_share (NO rsh n)) (resource_share (resource_at phi' l)) *)
rewrite H0.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
simpl.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
do 2 apply f_equal.
extensionality.
rewrite fmap_app.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
rewrite approx_oo_approx; auto.
subst phi.
unfold phi' in H.
rewrite unsquash_squash in H.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
injection H; clear H; intros.
destruct f; simpl in *; inv H.
generalize (equal_f H3 l); intro.
rewrite H0 in H.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
clear - H.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
unfold compose in H. rewrite if_true in H; auto.
(* Goal: @eq memval m m0 *)
(* Goal: @eq (list memval) b1 b2 *)
simpl in H.
revert H; generalize p at 2 3.
intros q ?H.
apply YES_inj in H.
match goal with
| H: ?A = ?B |- _ =>
  assert (snd A = snd B)
end.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
rewrite H; auto.
simpl in H0.
apply SomeP_inj2 in H0.
subst q.
extensionality i.
rewrite fmap_app.
rewrite approx_oo_approx. auto.
Qed.

Lemma yesat_eq_aux: 
  forall pp k sh l, 
    hereditary age
    (fun m : rmap =>
      exists rsh, 
     resource_fmap (approx (level m)) (approx (level m)) (m @ l) =
     resource_fmap (approx (level m)) (approx (level m)) (YES sh rsh k pp)).
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
 intros.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intro; intros.
(* Goal: @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (resource_at a' l)) (resource_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (YES sh rsh k pp))) *)
  destruct H0 as [p ?]; exists p.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (resource_at a' l)) (resource_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (YES sh p k pp)) *)
  rewrite resource_at_approx.
(* Goal: @eq resource (resource_at a' l) (resource_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (YES sh p k pp)) *)
  rewrite resource_at_approx in H0.
(* Goal: @eq resource (resource_at a' l) (resource_fmap (approx (@level rmap ag_rmap a')) (approx (@level rmap ag_rmap a')) (YES sh p k pp)) *)
  apply (age1_resource_at a a' H); auto.
Qed.

Lemma yesat_eq: yesat = fun pp k sh l =>
 exist (hereditary age)
  (fun m => 
  exists rsh, 
   resource_fmap (approx (level m)) (approx (level m)) (m @ l) = 
   resource_fmap (approx (level m)) (approx (level m)) (YES sh rsh k pp))
   (yesat_eq_aux pp k sh l).
Proof.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m) (@ex (readable_share sh) (fun p : readable_share sh => @ex AV.kind (fun k : AV.kind => and (@ex memval (fun v : memval => @eq kind k (VAL v))) (@eq resource (resource_at m l') (YES sh p k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) NoneP)))))) *)
unfold yesat.
(* Goal: @eq (forall (_ : preds) (_ : kind), spec) (fun (pp : preds) (k : kind) (sh : share) (l : AV.address) => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => @ex (readable_share sh) (fun rsh : readable_share sh => @app_pred rmap ag_rmap (yesat_raw pp k sh rsh l) m)) (yesat_obligation_1 pp k sh l)) (fun (pp : preds) (k : kind) (sh : Share.t) (l : AV.address) => @exist (forall _ : rmap, Prop) (@hereditary rmap (@age rmap ag_rmap)) (fun m : rmap => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) (resource_at m l)) (resource_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) (YES sh rsh k pp)))) (yesat_eq_aux pp k sh l)) *)
extensionality pp k sh l.
(* Goal: @eq (@sig (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p)) (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => @ex (readable_share sh) (fun rsh : readable_share sh => @app_pred rmap ag_rmap (yesat_raw pp k sh rsh l) m)) (yesat_obligation_1 pp k sh l)) (@exist (forall _ : rmap, Prop) (@hereditary rmap (@age rmap ag_rmap)) (fun m : rmap => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) (resource_at m l)) (resource_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) (YES sh rsh k pp)))) (yesat_eq_aux pp k sh l)) *)
apply exist_ext. extensionality w.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => @ex (readable_share sh) (fun rsh : readable_share sh => @app_pred rmap ag_rmap (yesat_raw NoneP (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) sh rsh l') m)) (yesat_obligation_1 NoneP (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) sh l')) m) (@ex (readable_share sh) (fun p : readable_share sh => @ex AV.kind (fun k : AV.kind => and (@eq kind k (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v)))) (@eq resource (resource_at m l') (YES sh p k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) NoneP)))))) *)
apply exists_ext; intro p.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (yesat_raw pp k sh p l) w) (@eq resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (resource_at w l)) (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (YES sh p k pp))) *)
rewrite yesat_raw_eq.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
auto.
Qed.

Lemma map_compose_approx_succ_e:
  forall A n pp pp',
       map (compose (A:=A) (approx (S n))) pp =
    map (compose (A:=A) (approx (S n))) pp' ->
  map (compose (A:=A) (approx n)) pp = map (compose (A:=A) (approx n)) pp'.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
induction pp; intros.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
destruct pp'; inv H; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
destruct pp'; inv H; auto.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
simpl.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
rewrite <- (IHpp pp'); auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
replace (approx n oo a) with (approx n oo p); auto.
(* Goal: @eq (forall _ : A, @pred rmap ag_rmap) (@compose A (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) p) (@compose A (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) a) *)
clear - H1.
(* Goal: @eq (forall _ : A, @pred rmap ag_rmap) (@compose A (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) p) (@compose A (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) a) *)
extensionality x.
(* Goal: @eq (forall _ : rmap, Prop) (@app_pred rmap ag_rmap (@compose A (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) p x)) (@app_pred rmap ag_rmap (@compose A (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) a x)) *)
apply pred_ext'. extensionality w.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@compose A (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) p x) w) (@app_pred rmap ag_rmap (@compose A (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) a x) w) *)
generalize (equal_f H1 x); clear H1; intro.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@compose A (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) p x) w) (@app_pred rmap ag_rmap (@compose A (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) a x) w) *)
unfold compose in *.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (approx n (p x)) w) (@app_pred rmap ag_rmap (approx n (a x)) w) *)
assert (approx (S n) (a x) w <-> approx (S n) (p x) w).
(* Goal: iff (@app_pred rmap ag_rmap (approx (S n) (a x)) w) (@app_pred rmap ag_rmap (approx (S n) (p x)) w) *)
(* Goal: @eq Prop (@app_pred rmap ag_rmap (approx n (p x)) w) (@app_pred rmap ag_rmap (approx n (a x)) w) *)
rewrite H; intuition.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
simpl.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
apply and_ext'; auto; intros.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (p x) w) (@app_pred rmap ag_rmap (a x) w) *)
apply prop_ext.
(* Goal: iff (@app_pred rmap ag_rmap P m') (@app_pred rmap ag_rmap Q m') *)
intuition.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
destruct H3; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
split; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
destruct H2; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
split; auto.
Qed.

(* NOT TRUE, because the shares might not match
Lemma extensionally_yesat: forall pp k sh l, extensionally (yesat pp k sh l) = yesat pp k sh l.
*)

Program Definition noat (l: AV.address) : pred rmap :=
    fun m => identity (m @ l).
 Next Obligation.
(* Goal: forall (_ : memory_chunk) (_ : address) (_ : val) (_ : list memval) (_ : address), (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) *)
    intros; intro; intros.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    apply (age1_resource_at_identity _ _ l H); auto.
 Qed.

Definition resource_share (r: resource) : option share :=
 match r with
 | YES sh _ _ _ => Some sh
 | NO sh _ => Some sh
 | PURE _ _ => None
 end.

Definition nonlock (r: resource) : Prop :=
 match r with
 | YES _ _ k _ => isVAL k \/ isFUN k
 | NO _ _ => True
 | PURE _ _ => False
 end.

Lemma age1_nonlock: forall phi phi' l,
  age1 phi = Some phi' -> (nonlock (phi @ l) <-> nonlock (phi' @ l)).
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: @eq (option share) (resource_share (resource_at phi l)) (resource_share (resource_at phi' l)) *)
  destruct (phi @ l) as [rsh | rsh sh k P |] eqn:?H.
  + pose proof (age1_NO phi phi' l rsh n H).
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat y (@level A H w'))) *)
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
    rewrite H1 in H0.
(* Goal: @eq (option share) (resource_share (NO rsh n)) (resource_share (resource_at phi' l)) *)
    rewrite H0.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@andp rmap ag_rmap (shareat l sh) (nonlockat l)) w) (and (@eq (option share) (resource_share (resource_at w l)) (@Some share sh)) (nonlock (resource_at w l))) *)
    reflexivity.
  + pose proof (age1_YES' phi phi' l rsh sh k H).
(* Goal: @eq (option share) (resource_share (PURE k p)) (resource_share (resource_at phi' l)) *)
    destruct H1 as [? _].
(* Goal: @eq (option share) (resource_share (PURE k p)) (resource_share (resource_at phi' l)) *)
    spec H1; [eauto |].
(* Goal: @eq (option share) (resource_share (PURE k p)) (resource_share (resource_at phi' l)) *)
    destruct H1 as [P' ?].
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at phi l)) (resource_at (@core rmap Join_rmap Sep_rmap w0) l) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap phi)) (ghost_of (@core rmap Join_rmap Sep_rmap w0)) *)
    rewrite H1.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@andp rmap ag_rmap (shareat l sh) (nonlockat l)) w) (and (@eq (option share) (resource_share (resource_at w l)) (@Some share sh)) (nonlock (resource_at w l))) *)
    reflexivity.
  + pose proof (age1_PURE phi phi' l k H).
(* Goal: @eq (option share) (resource_share (PURE k p)) (resource_share (resource_at phi' l)) *)
    destruct H1 as [? _].
(* Goal: @eq (option share) (resource_share (PURE k p)) (resource_share (resource_at phi' l)) *)
    spec H1; [eauto |].
(* Goal: @eq (option share) (resource_share (PURE k p)) (resource_share (resource_at phi' l)) *)
    destruct H1 as [P' ?].
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at phi l)) (resource_at (@core rmap Join_rmap Sep_rmap w0) l) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap phi)) (ghost_of (@core rmap Join_rmap Sep_rmap w0)) *)
    rewrite H1.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@andp rmap ag_rmap (shareat l sh) (nonlockat l)) w) (and (@eq (option share) (resource_share (resource_at w l)) (@Some share sh)) (nonlock (resource_at w l))) *)
    reflexivity.
Qed.

Lemma age1_resource_share: forall phi phi' l,
  age1 phi = Some phi' -> (resource_share (phi @ l) = resource_share (phi' @ l)).
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: @eq (option share) (resource_share (resource_at phi l)) (resource_share (resource_at phi' l)) *)
  destruct (phi @ l) as [rsh | rsh sh k P |] eqn:?H.
  + pose proof (age1_NO phi phi' l rsh n H).
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat y (@level A H w'))) *)
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
    rewrite H1 in H0.
(* Goal: @eq (option share) (resource_share (NO rsh n)) (resource_share (resource_at phi' l)) *)
    rewrite H0.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@andp rmap ag_rmap (shareat l sh) (nonlockat l)) w) (and (@eq (option share) (resource_share (resource_at w l)) (@Some share sh)) (nonlock (resource_at w l))) *)
    reflexivity.
  + pose proof (age1_YES' phi phi' l rsh sh k H).
(* Goal: @eq (option share) (resource_share (PURE k p)) (resource_share (resource_at phi' l)) *)
    destruct H1 as [? _].
(* Goal: @eq (option share) (resource_share (PURE k p)) (resource_share (resource_at phi' l)) *)
    spec H1; [eauto |].
(* Goal: @eq (option share) (resource_share (PURE k p)) (resource_share (resource_at phi' l)) *)
    destruct H1 as [P' ?].
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at phi l)) (resource_at (@core rmap Join_rmap Sep_rmap w0) l) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap phi)) (ghost_of (@core rmap Join_rmap Sep_rmap w0)) *)
    rewrite H1.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@andp rmap ag_rmap (shareat l sh) (nonlockat l)) w) (and (@eq (option share) (resource_share (resource_at w l)) (@Some share sh)) (nonlock (resource_at w l))) *)
    reflexivity.
  + pose proof (age1_PURE phi phi' l k H).
(* Goal: @eq (option share) (resource_share (PURE k p)) (resource_share (resource_at phi' l)) *)
    destruct H1 as [? _].
(* Goal: @eq (option share) (resource_share (PURE k p)) (resource_share (resource_at phi' l)) *)
    spec H1; [eauto |].
(* Goal: @eq (option share) (resource_share (PURE k p)) (resource_share (resource_at phi' l)) *)
    destruct H1 as [P' ?].
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at phi l)) (resource_at (@core rmap Join_rmap Sep_rmap w0) l) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap phi)) (ghost_of (@core rmap Join_rmap Sep_rmap w0)) *)
    rewrite H1.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@andp rmap ag_rmap (shareat l sh) (nonlockat l)) w) (and (@eq (option share) (resource_share (resource_at w l)) (@Some share sh)) (nonlock (resource_at w l))) *)
    reflexivity.
Qed.

Lemma resource_share_join_exists: forall r1 r2 r sh1 sh2,
  resource_share r1 = Some sh1 ->
  resource_share r2 = Some sh2 ->
  join r1 r2 r ->
  exists sh, join sh1 sh2 sh /\ resource_share r = Some sh.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
  destruct r1, r2; try solve [inversion H | inversion H0];
  inv H; inv H0; inv H1;
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
  eexists; split; eauto.
Qed.

Lemma resource_share_join: forall r1 r2 r sh1 sh2 sh,
  resource_share r1 = Some sh1 ->
  resource_share r2 = Some sh2 ->
  join r1 r2 r ->
  join sh1 sh2 sh ->
  resource_share r = Some sh.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: @eq (option share) (resource_share r) (@Some share sh) *)
  destruct (resource_share_join_exists _ _ _ _ _ H H0 H1) as [sh' [? ?]].
(* Goal: @eq (option share) (resource_share r) (@Some share sh) *)
  rewrite H4.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
  f_equal.
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
  eapply join_eq; eauto.
Qed.

Lemma resource_share_joins: forall r1 r2 sh1 sh2,
  resource_share r1 = Some sh1 ->
  resource_share r2 = Some sh2 ->
  joins r1 r2 ->
  joins sh1 sh2.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: @joins share Share.Join_ba sh1 sh2 *)
  destruct H1 as [r ?].
(* Goal: @joins share Share.Join_ba sh1 sh2 *)
  destruct (resource_share_join_exists _ _ _ _ _ H H0 H1) as [sh [? ?]].
(* Goal: @joins share Share.Join_ba sh1 sh2 *)
  exists sh.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  auto.
Qed.

Lemma nonlock_join: forall r1 r2 r,
  nonlock r1 ->
  nonlock r2 ->
  join r1 r2 r ->
  nonlock r.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  destruct r1, r2; inv H1; auto.
Qed.

Program Definition nonlockat (l: AV.address): pred rmap :=
  fun m => nonlock (m @ l).
 Next Obligation.
(* Goal: forall (_ : memory_chunk) (_ : address) (_ : val) (_ : list memval) (_ : address), (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) *)
    intros; intro; intros.
(* Goal: @eq (option share) (resource_share (resource_at a' l)) (@Some share sh) *)
    unfold resource_share in *.
(* Goal: @eq (option share) match resource_at a' l with | NO sh n => @Some Share.t sh | YES sh r k p => @Some Share.t sh | PURE k p => @None share end (@Some share sh) *)
    destruct (a @ l) eqn:?H.
    + rewrite (necR_NO a a' l _ n) in H1 by (constructor; auto).
(* Goal: @eq (option share) match resource_at a' l with | NO sh n => @Some Share.t sh | YES sh r k p => @Some Share.t sh | PURE k p => @None share end (@Some share sh) *)
      rewrite H1; assumption.
    + eapply necR_YES in H1; [ | constructor; eassumption].
(* Goal: @eq (option share) match resource_at a' l with | NO sh n => @Some Share.t sh | YES sh r k p => @Some Share.t sh | PURE k p => @None share end (@Some share sh) *)
      rewrite H1; assumption.
    + eapply necR_PURE in H1; [ | constructor; eassumption].
(* Goal: @eq (option share) match resource_at a' l with | NO sh n => @Some Share.t sh | YES sh r k p => @Some Share.t sh | PURE k p => @None share end (@Some share sh) *)
      rewrite H1; assumption.
 Qed.

Program Definition shareat (l: AV.address) (sh: share): pred rmap :=
  fun m => resource_share (m @ l) = Some sh.
 Next Obligation.
(* Goal: forall (_ : memory_chunk) (_ : address) (_ : val) (_ : list memval) (_ : address), (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) *)
    intros; intro; intros.
(* Goal: @eq (option share) (resource_share (resource_at a' l)) (@Some share sh) *)
    unfold resource_share in *.
(* Goal: @eq (option share) match resource_at a' l with | NO sh n => @Some Share.t sh | YES sh r k p => @Some Share.t sh | PURE k p => @None share end (@Some share sh) *)
    destruct (a @ l) eqn:?H.
    + rewrite (necR_NO a a' l _ n) in H1 by (constructor; auto).
(* Goal: @eq (option share) match resource_at a' l with | NO sh n => @Some Share.t sh | YES sh r k p => @Some Share.t sh | PURE k p => @None share end (@Some share sh) *)
      rewrite H1; assumption.
    + eapply necR_YES in H1; [ | constructor; eassumption].
(* Goal: @eq (option share) match resource_at a' l with | NO sh n => @Some Share.t sh | YES sh r k p => @Some Share.t sh | PURE k p => @None share end (@Some share sh) *)
      rewrite H1; assumption.
    + inv H0.
 Qed.

Program Definition jam {A} {JA: Join A}{PA: Perm_alg A}{agA: ageable A}{AgeA: Age_alg A} {B: Type} {S': B -> Prop} (S: forall l, {S' l}+{~ S' l}) (P Q: B -> pred A) : B -> pred A :=
  fun (l: B) m => if S l then P l m else Q l m.
 Next Obligation.
(* Goal: forall (_ : memory_chunk) (_ : address) (_ : val) (_ : list memval) (_ : address), (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) *)
    intros; intro; intros.
(* Goal: if S l then @app_pred A agA (P l) a' else @app_pred A agA (Q l) a' *)
  if_tac; try (eapply pred_hereditary; eauto).
 Qed.

(*Lemma allp_noat_emp: allp noat = emp.
Proof.
  apply pred_ext; unfold derives; intros; simpl in *.
  + apply all_resource_at_identity.
    exact H.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  + intros. apply resource_at_identity.
    exact H.
Qed.*)

Lemma jam_true: forall A JA PA agA AgeA B (S': B -> Prop) S P Q loc, S' loc -> @jam A JA PA agA AgeA B S' S P Q loc = P loc.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: @eq (@pred A agA) (@jam A JA PA agA AgeA B S' S P Q loc) (Q loc) *)
apply pred_ext'.
(* Goal: @eq (forall _ : A, Prop) (@app_pred A agA (@jam A JA PA agA AgeA B S' S P Q loc)) (@app_pred A agA (Q loc)) *)
extensionality m; unfold jam.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
simpl. rewrite if_true; auto.
Qed.

Lemma jam_false: forall A JA PA agA AgeA B (S': B -> Prop) S P Q loc, ~ S' loc -> @jam A JA PA agA AgeA B S' S P Q loc = Q loc.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: @eq (@pred A agA) (@jam A JA PA agA AgeA B S' S P Q loc) (Q loc) *)
apply pred_ext'.
(* Goal: @eq (forall _ : A, Prop) (@app_pred A agA (@jam A JA PA agA AgeA B S' S P Q loc)) (@app_pred A agA (Q loc)) *)
extensionality m; unfold jam.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
simpl; rewrite if_false; auto.
Qed.

Lemma boxy_jam:  forall (m: modality) A (S': A -> Prop) S P Q,
      (forall (x: A), boxy m (P x)) ->
      (forall x, boxy m (Q x)) ->
      forall x, boxy m (@jam rmap _ _ _ _ A S' S P Q x).
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: @boxy rmap ag_rmap m (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap A S' S P Q x) *)
   unfold boxy in *.
(* Goal: @eq (@pred rmap ag_rmap) (@box rmap ag_rmap m (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap A S' S P Q x)) (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap A S' S P Q x) *)
   apply pred_ext; intros w ?.
(* Goal: @app_pred rmap ag_rmap (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (size_chunk ch)) (adr_range_dec l (size_chunk ch)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat l') w *)
   unfold jam in *.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
   simpl in *; if_tac. rewrite <- H . simpl. apply H1.
(* Goal: forall (a' : rmap) (_ : @app_mode rmap ag_rmap m w a'), @app_pred rmap ag_rmap (P x) a' *)
(* Goal: @app_pred rmap ag_rmap (Q x) w *)
(* Goal: @app_pred rmap ag_rmap (@box rmap ag_rmap m (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap A S' S P Q x)) w *)
   rewrite <- H0; simpl; apply H1.
(* Goal: @app_pred rmap ag_rmap (@box rmap ag_rmap m (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap A S' S P Q x)) w *)
   simpl in *; if_tac.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    rewrite <- H in H1; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
   rewrite <- H0 in H1; auto.
Qed.

Definition extensible_jam: forall A (S': A -> Prop) S (P Q: A -> pred rmap),
      (forall (x: A), boxy extendM (P x)) ->
      (forall x, boxy extendM (Q x)) ->
      forall x, boxy extendM  (@jam _ _ _ _ _ _ S' S P Q x).
Proof.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  apply boxy_jam; auto.
Qed.

Definition jam_vacuous:
  forall A JA PA agA AgeA B S S' P Q, (forall x:B, ~ S x) -> @jam A JA PA agA AgeA B S S' P Q = Q.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: @eq (forall _ : rmap, Prop) (@app_pred rmap ag_rmap (@compose A (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) p x)) (@app_pred rmap ag_rmap (@compose A (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) a x)) *)
extensionality l; apply pred_ext'; extensionality w.
(* Goal: @eq (forall _ : address, @pred rmap ag_rmap) (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (Zpos xH)) (adr_range_dec l (Zpos xH)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat) (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (@eq address l) (@eq_dec address EqDec_address l) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat) *)
unfold jam.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
simpl; rewrite if_false; auto.
Qed.
(*
Implicit Arguments jam_vacuous.
*)
Lemma make_sub_rmap: forall w (P: address -> Prop) (P_DEC: forall l, {P l} + {~ P l}),
  (forall l sh k, P l -> res_option (w @ l) = Some (sh, k) -> isVAL k \/ isFUN k) ->
(* Goal: @eq share sh Share.bot *)
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
  {w' | level w' = level w /\ resource_at w' =
       (fun l => if P_DEC l then w @ l else core (w @ l)) /\ ghost_of w' = ghost_of w}.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: @sig rmap (fun w' : rmap => and (@eq nat (@level rmap ag_rmap w') (@level rmap ag_rmap w)) (and (@eq (forall _ : AV.address, resource) (resource_at w') (fun l : AV.address => if P_DEC l then resource_at w l else @core resource Join_resource Sep_resource (resource_at w l))) (@eq ghost (ghost_of w') (ghost_of w)))) *)
  apply remake_rmap.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: or (@ex rmap (fun m : rmap => and (@eq nat (@level rmap ag_rmap m) (@level rmap ag_rmap w)) (@eq resource (if P_DEC l then resource_at w l else @core resource Join_resource Sep_resource (resource_at w l)) (resource_at m l)))) (no_preds (if P_DEC l then resource_at w l else @core resource Join_resource Sep_resource (resource_at w l))) *)
(* Goal: @eq ghost (ghost_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (ghost_of w)) (ghost_of w) *)
    if_tac; [left; eauto |].
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    destruct (w @ l) eqn:?H; rewrite ?core_NO, ?core_YES, ?core_PURE; simpl; auto.
(* Goal: or (@ex rmap (fun m : rmap => and (@eq nat (@level rmap ag_rmap m) (@level rmap ag_rmap w)) (@eq resource (PURE k p) (resource_at m l)))) (@eq preds p NoneP) *)
(* Goal: @eq ghost (ghost_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (ghost_of w)) (ghost_of w) *)
    left.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    exists w; split; auto.
(* Goal: @eq ghost (ghost_fmap (approx (@level rmap ag_rmap w0)) (approx (@level rmap ag_rmap w0)) (ghost_of w0)) (ghost_of w0) *)
    apply ghost_of_approx.
Qed.

Definition is_resource_pred (p: address -> pred rmap) (q: resource -> address -> nat -> Prop) :=
  forall l w, (p l) w = q (w @ l) l (level w).

Definition resource_stable (p: address -> pred rmap) :=
  forall l w w', w @ l = w' @ l -> level w = level w' -> (p l) w = (p l) w'.

(* Goal: @eq share sh Share.bot *)
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
Lemma is_resource_pred_resource_stable: forall {p},
  (exists q, is_resource_pred p q) -> resource_stable p.
Proof.
(* Goal: forall (p : forall _ : address, @pred rmap ag_rmap) (_ : @ex (forall (_ : resource) (_ : address) (_ : nat), Prop) (fun q : forall (_ : resource) (_ : address) (_ : nat), Prop => is_resource_pred p q)), resource_stable p *)
  unfold is_resource_pred, resource_stable.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (p l) w) (@app_pred rmap ag_rmap (p l) w') *)
  destruct H as [q ?]; rewrite !H.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  rewrite H0; auto.
Qed.

Program Definition noghost : pred rmap := fun m => identity (ghost_of m).
Next Obligation.
Proof.
(* Goal: (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => @identity ghost ghost_join (ghost_of m)) *)
  intros ????.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
  rewrite (age1_ghost_of _ _ H), (identity_core H0), ghost_core; simpl.
(* Goal: @identity ghost ghost_join (@nil (option (prod (@sigT ghost.Ghost (fun g : ghost.Ghost => @sig (@ghost.G g) (fun a : @ghost.G g => @ghost.valid g a))) preds))) *)
  rewrite <- (ghost_core nil); apply core_identity.
Defined.

(* This is about split one segment into two segments. *)
Lemma allp_jam_split2: forall (P Q R: address -> Prop) (p q r: address -> pred rmap)
  (P_DEC: forall l, {P l} + {~ P l})
  (Q_DEC: forall l, {Q l} + {~ Q l})
  (R_DEC: forall l, {R l} + {~ R l}),
  (exists resp, is_resource_pred p resp) ->
  (exists resp, is_resource_pred q resp) ->
  (exists resp, is_resource_pred r resp) ->
  Ensemble_join Q R P ->
  (forall l, Q l -> p l = q l) ->
  (forall l, R l -> p l = r l) ->
  (forall l m sh k, P l -> (p l) m -> res_option (m @ l) = Some (sh, k) -> isVAL k \/ isFUN k) ->
  allp (jam P_DEC p noat) && noghost =
  (allp (jam Q_DEC q noat) && noghost) * (allp (jam R_DEC r noat) && noghost).
Proof.
(* Goal: forall (P Q R : forall _ : address, Prop) (p q r : forall _ : address, @pred rmap ag_rmap) (P_DEC : forall l : address, sumbool (P l) (not (P l))) (Q_DEC : forall l : address, sumbool (Q l) (not (Q l))) (R_DEC : forall l : address, sumbool (R l) (not (R l))) (_ : @ex (forall (_ : resource) (_ : address) (_ : nat), Prop) (fun resp : forall (_ : resource) (_ : address) (_ : nat), Prop => is_resource_pred p resp)) (_ : @ex (forall (_ : resource) (_ : address) (_ : nat), Prop) (fun resp : forall (_ : resource) (_ : address) (_ : nat), Prop => is_resource_pred q resp)) (_ : @ex (forall (_ : resource) (_ : address) (_ : nat), Prop) (fun resp : forall (_ : resource) (_ : address) (_ : nat), Prop => is_resource_pred r resp)) (_ : @Ensemble_join address Q R P) (_ : forall (l : address) (_ : Q l), @eq (@pred rmap ag_rmap) (p l) (q l)) (_ : forall (l : address) (_ : R l), @eq (@pred rmap ag_rmap) (p l) (r l)) (_ : forall (l : address) (m : rmap) (sh : rshare) (k : AV.kind) (_ : P l) (_ : @app_pred rmap ag_rmap (p l) m) (_ : @eq (option (prod rshare AV.kind)) (res_option (resource_at m l)) (@Some (prod rshare AV.kind) (@pair rshare AV.kind sh k))), or (isVAL k) (isFUN k)), @eq (@pred rmap ag_rmap) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address P P_DEC p noat)) noghost) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address Q Q_DEC q noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address R R_DEC r noat)) noghost)) *)
  intros until R_DEC.
(* Goal: forall (_ : @ex (forall (_ : resource) (_ : address) (_ : nat), Prop) (fun resp : forall (_ : resource) (_ : address) (_ : nat), Prop => is_resource_pred p resp)) (_ : @ex (forall (_ : resource) (_ : address) (_ : nat), Prop) (fun resp : forall (_ : resource) (_ : address) (_ : nat), Prop => is_resource_pred q resp)) (_ : @ex (forall (_ : resource) (_ : address) (_ : nat), Prop) (fun resp : forall (_ : resource) (_ : address) (_ : nat), Prop => is_resource_pred r resp)) (_ : @Ensemble_join address Q R P) (_ : forall (l : address) (_ : Q l), @eq (@pred rmap ag_rmap) (p l) (q l)) (_ : forall (l : address) (_ : R l), @eq (@pred rmap ag_rmap) (p l) (r l)) (_ : forall (l : address) (m : rmap) (sh : rshare) (k : AV.kind) (_ : P l) (_ : @app_pred rmap ag_rmap (p l) m) (_ : @eq (option (prod rshare AV.kind)) (res_option (resource_at m l)) (@Some (prod rshare AV.kind) (@pair rshare AV.kind sh k))), or (isVAL k) (isFUN k)), @eq (@pred rmap ag_rmap) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address P P_DEC p noat)) noghost) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address Q Q_DEC q noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address R R_DEC r noat)) noghost)) *)
  intros ST_P ST_Q ST_R.
(* Goal: forall (_ : @Ensemble_join address Q R P) (_ : forall (l : address) (_ : Q l), @eq (@pred rmap ag_rmap) (p l) (q l)) (_ : forall (l : address) (_ : R l), @eq (@pred rmap ag_rmap) (p l) (r l)) (_ : forall (l : address) (m : rmap) (sh : rshare) (k : AV.kind) (_ : P l) (_ : @app_pred rmap ag_rmap (p l) m) (_ : @eq (option (prod rshare AV.kind)) (res_option (resource_at m l)) (@Some (prod rshare AV.kind) (@pair rshare AV.kind sh k))), or (isVAL k) (isFUN k)), @eq (@pred rmap ag_rmap) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address P P_DEC p noat)) noghost) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address Q Q_DEC q noat)) noghost) (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address R R_DEC r noat)) noghost)) *)
  intros [? ?] ? ? ?.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  apply pred_ext; intros w; simpl; intros.
  + destruct (make_sub_rmap w Q Q_DEC) as [w1 [? ?]].
(* Goal: @eq share sh Share.bot *)
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
    {
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
      intros. eapply H3; [| | eauto].
      + firstorder.
      + destruct H4; specialize (H4 l); if_tac in H4; [auto | firstorder].
    }
(* Goal: @ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (and (forall b : address, if Q_DEC b then @app_pred rmap ag_rmap (q b) y else @identity resource Join_resource (resource_at y b)) (@identity ghost ghost_join (ghost_of y))) (and (forall b : address, if R_DEC b then @app_pred rmap ag_rmap (r b) z else @identity resource Join_resource (resource_at z b)) (@identity ghost ghost_join (ghost_of z)))))) *)
    destruct (make_sub_rmap w R R_DEC) as [w2 [? ?]].
(* Goal: @eq share sh Share.bot *)
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
    {
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
      intros. eapply H3; [| | eauto].
      + firstorder.
      + destruct H4; specialize (H4 l); if_tac in H4; [auto | firstorder].
    }
(* Goal: @ex rmap (fun y : rmap => @ex rmap (fun z : rmap => and (@join rmap Join_rmap y z w) (and (and (forall b : address, if Q_DEC b then @app_pred rmap ag_rmap (q b) y else @identity resource Join_resource (resource_at y b)) (@identity ghost ghost_join (ghost_of y))) (and (forall b : address, if R_DEC b then @app_pred rmap ag_rmap (r b) z else @identity resource Join_resource (resource_at z b)) (@identity ghost ghost_join (ghost_of z)))))) *)
    exists w1, w2.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    split3; auto.
    - apply resource_at_join2; try congruence.
(* Goal: forall l : AV.address, @identity resource Join_resource (resource_at a l) *)
      intro l.
(* Goal: @join resource Join_resource (resource_at w1 l) (resource_at w2 l) (resource_at w l) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
      destruct H6, H8.
(* Goal: @join resource Join_resource (resource_at w1 l) (resource_at w2 l) (resource_at w l) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
      rewrite H6, H8.
(* Goal: @join resource Join_resource (if Q_DEC l then resource_at w l else @core resource Join_resource Sep_resource (resource_at w l)) (if R_DEC l then resource_at w l else @core resource Join_resource Sep_resource (resource_at w l)) (resource_at w l) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
      pose proof core_unit (w @ l).
(* Goal: @join resource Join_resource (if Q_DEC l then resource_at w l else @core resource Join_resource Sep_resource (resource_at w l)) (if R_DEC l then resource_at w l else @core resource Join_resource Sep_resource (resource_at w l)) (resource_at w l) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
      destruct (Q_DEC l), (R_DEC l).
(* Goal: @app_pred rmap ag_rmap (p b) w *)
      * firstorder.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      * apply join_comm; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      * auto.
      * destruct H4; specialize (H4 l).
(* Goal: @app_pred rmap ag_rmap (p b) w *)
        rewrite if_false in H4 by firstorder.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
        rewrite identity_core by auto.
(* Goal: @join resource Join_resource (@core resource Join_resource Sep_resource (resource_at w l)) (@core resource Join_resource Sep_resource (resource_at w l)) (@core resource Join_resource Sep_resource (resource_at w l)) *)
        apply core_duplicable.
      * destruct H6 as [_ ->], H8 as [_ ->].
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
        destruct H4; apply identity_unit'; auto.
    - split.
(* Goal: forall b : address, if R_DEC b then @app_pred rmap ag_rmap (r b) w2 else @identity resource Join_resource (resource_at w2 b) *)
(* Goal: @identity ghost ghost_join (ghost_of w2) *)
      intros l.
(* Goal: if R_DEC l then @app_pred rmap ag_rmap (r l) w2 else @identity resource Join_resource (resource_at w2 l) *)
(* Goal: @identity ghost ghost_join (ghost_of w2) *)
      destruct H4; specialize (H4 l).
(* Goal: @eq Prop (if @eq_dec address EqDec_address l l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) (if adr_range_dec l (Zpos xH) l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) *)
      if_tac.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      * rewrite <- H1 by auto.
(* Goal: @app_pred rmap ag_rmap (p b) w *)
        rewrite if_true in H4 by firstorder.
        erewrite <- (is_resource_pred_resource_stable ST_P); [eauto | | auto].
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
        destruct H6; rewrite H6, if_true by auto; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      * destruct H6; rewrite H6, if_false by auto.
(* Goal: @identity resource Join_resource (@core resource Join_resource Sep_resource (resource_at w0 l')) *)
(* Goal: @app_pred rmap ag_rmap noghost phi *)
        apply core_identity.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      * destruct H4, H6 as [_ ->]; auto.
    - split.
(* Goal: forall b : address, if R_DEC b then @app_pred rmap ag_rmap (r b) w2 else @identity resource Join_resource (resource_at w2 b) *)
(* Goal: @identity ghost ghost_join (ghost_of w2) *)
      intros l.
(* Goal: if R_DEC l then @app_pred rmap ag_rmap (r l) w2 else @identity resource Join_resource (resource_at w2 l) *)
(* Goal: @identity ghost ghost_join (ghost_of w2) *)
      destruct H4; specialize (H4 l).
(* Goal: @eq Prop (if @eq_dec address EqDec_address l l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) (if adr_range_dec l (Zpos xH) l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) *)
      if_tac.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      * rewrite <- H2 by auto.
(* Goal: @app_pred rmap ag_rmap (p b) w *)
        rewrite if_true in H4 by firstorder.
        erewrite <- (is_resource_pred_resource_stable ST_P); [eauto | | auto].
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
        destruct H8; rewrite H8, if_true by auto; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      * destruct H8; rewrite H8, if_false by auto.
(* Goal: @identity resource Join_resource (@core resource Join_resource Sep_resource (resource_at w0 l')) *)
(* Goal: @app_pred rmap ag_rmap noghost phi *)
        apply core_identity.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      * destruct H4, H8 as [_ ->]; auto.
  + destruct H4 as [y [z [? [[? Hg1] [? Hg2]]]]].
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
    split; intros.
(* Goal: if P_DEC b then @app_pred rmap ag_rmap (p b) w else @identity resource Join_resource (resource_at w b) *)
(* Goal: @identity ghost ghost_join (ghost_of w) *)
    specialize (H5 b); specialize (H6 b).
(* Goal: @eq Prop (if @eq_dec address EqDec_address l l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) (if adr_range_dec l (Zpos xH) l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) *)
    if_tac.
    - if_tac in H5; if_tac in H6.
(* Goal: @app_pred rmap ag_rmap (p b) w *)
      * firstorder.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      * rewrite H1 by auto.
(* Goal: @app_pred rmap ag_rmap (q b) w *)
        erewrite (is_resource_pred_resource_stable ST_Q); [eauto | | apply join_level in H4; symmetry; tauto].
(* Goal: @identity resource Join_resource (resource_at w b) *)
        apply resource_at_join with (loc := b) in H4.
(* Goal: @eq resource (resource_at w b) (resource_at y b) *)
        apply join_comm, H6 in H4.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
        auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      * rewrite H2 by auto; auto.
(* Goal: @app_pred rmap ag_rmap (r b) w *)
        erewrite (is_resource_pred_resource_stable ST_R); [eauto | | apply join_level in H4; symmetry; tauto].
(* Goal: @identity resource Join_resource (resource_at w b) *)
        apply resource_at_join with (loc := b) in H4.
(* Goal: @eq resource (resource_at w b) (resource_at z b) *)
        apply H5 in H4.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
        auto.
(* Goal: @app_pred rmap ag_rmap (p b) w *)
      * firstorder.
(* Goal: @app_pred rmap ag_rmap (p b) w *)
    - rewrite if_false in H5 by firstorder.
(* Goal: @app_pred rmap ag_rmap (p b) w *)
      rewrite if_false in H6 by firstorder.
(* Goal: @identity resource Join_resource (resource_at w b) *)
      apply resource_at_join with (loc := b) in H4.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      apply H5 in H4; rewrite <- H4; auto.
    - apply ghost_of_join in H4.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      rewrite <- (Hg1 _ _ H4); auto.
Qed.


Lemma allp_jam_overlap: forall (P Q: address -> Prop) (p q: address -> pred rmap)
  (P_DEC: forall l, {P l} + {~ P l})
  (Q_DEC: forall l, {Q l} + {~ Q l}),
  (exists resp, is_resource_pred p resp) ->
  (exists resp, is_resource_pred q resp) ->
  (forall l w1 w2, p l w1 -> q l w2 -> joins w1 w2 -> False) ->
  (exists l, P l /\ Q l) ->
  allp (jam P_DEC p noat) * allp (jam Q_DEC q noat) |-- FF.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intro w; simpl; intros.
(* Goal: False *)
  destruct H3 as [w1 [w2 [? [? ?]]]].
(* Goal: False *)
  destruct H2 as [l ?].
(* Goal: False *)
  specialize (H4 l).
(* Goal: False *)
  specialize (H5 l).
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  rewrite if_true in H4, H5 by tauto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  apply (H1 l w1 w2); auto.
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
  eauto.
Qed.

Lemma yesat_join_diff:
  forall pp pp' k k' sh sh' l w, k <> k' -> 
                  yesat pp k sh l w -> yesat pp' k' sh' l w -> False.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
unfold yesat, yesat_raw; intros.
(* Goal: False *)
destruct H0 as [p ?]. destruct H1 as [p' ?].
simpl in *; inversion2 H0 H1.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
contradiction H; auto.
Qed.

Lemma yesat_raw_join:
  forall pp k (sh1 sh2 sh3: Share.t) rsh1 rsh2 rsh3 l phi1 phi2 phi3,
   join sh1 sh2 sh3 ->
   yesat_raw pp k sh1 rsh1 l phi1 ->
   yesat_raw pp k sh2 rsh2 l phi2 ->
   join phi1 phi2 phi3 ->
   yesat_raw pp k sh3 rsh3 l phi3.
Proof.
unfold yesat_raw;
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros until 1; rename H into HR; intros.
simpl in H,H0|-*.
(* Goal: @eq resource (resource_at phi3 l) (YES sh3 rsh3 k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) pp)) *)
assert (level phi2 = level phi3) by (apply join_level in H1; intuition).
rewrite H2 in *; clear H2.
assert (level phi1 = level phi3) by  (apply join_level in H1; intuition).
rewrite H2 in *; clear H2.
(* Goal: @eq resource (resource_at phi3 l) (YES sh3 rsh3 k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) pp)) *)
generalize (resource_at_join _ _ _ l H1); clear H1.
(* Goal: forall _ : @join resource Join_resource (resource_at phi1 l) (resource_at phi2 l) (resource_at phi3 l), @eq resource (resource_at phi3 l) (YES sh3 rsh3 k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) pp)) *)
revert H H0.
(* Goal: forall (_ : @eq resource (resource_at phi1 l) (YES sh1 rsh1 k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) pp))) (_ : @eq resource (resource_at phi2 l) (YES sh2 rsh2 k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) pp))) (_ : @join resource Join_resource (resource_at phi1 l) (resource_at phi2 l) (resource_at phi3 l)), @eq resource (resource_at phi3 l) (YES sh3 rsh3 k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) pp)) *)
case_eq (phi1 @ l); intros; try discriminate.
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat y (@level A H w'))) *)
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
inv H0.
(* Goal: @eq resource (resource_at phi3 l) (YES sh3 rsh3 k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) pp)) *)
revert H1 H2; case_eq (phi2 @ l); intros; try discriminate.
(* Goal: @eq resource (resource_at phi3 l) (YES sh3 rsh3 k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) pp)) *)
inv H1.
(* Goal: @eq resource (resource_at phi3 l) (YES sh3 rsh3 k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) pp)) *)
inv H2.
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat y (@level A H w'))) *)
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
inv H0.
(* Goal: @eq resource (YES sh5 rsh5 k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) pp)) (YES sh3 rsh3 k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) pp)) *)
pose proof (join_eq HR RJ). subst sh5. clear RJ.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
repeat proof_irr. auto.
Qed.

(* Goal: @eq share sh Share.bot *)
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
Lemma nonunit_join: forall A {JA: Join A}{PA: Perm_alg A}{SA: Sep_alg A}{CA: Disj_alg A} (x y z: A),
  nonunit x -> join x y z -> nonunit z.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: @nonunit A JA z *)
intro; intro.
(* Goal: False *)
apply unit_identity in H1.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
apply split_identity in H0; auto.
(* Goal: False *)
apply nonunit_nonidentity in H.
(* Goal: False *)
contradiction.
Qed.

Lemma yesat_join:
  forall pp k sh1 sh2 sh3 l m1 m2 m3,
   join sh1 sh2 sh3 ->   
   yesat pp k sh1 l m1 ->
   yesat pp k sh2 l m2 ->
   join m1 m2 m3 ->
   yesat pp k sh3 l m3.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: @app_pred rmap ag_rmap (yesat pp k sh3 l) m3 *)
destruct H0 as [p1 ?].
(* Goal: @app_pred rmap ag_rmap (yesat pp k sh3 l) m3 *)
destruct H1 as [p2 ?].
(* Goal: @app_pred rmap ag_rmap (yesat pp k sh3 l) m3 *)
assert (p3: readable_share sh3).
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
eapply join_readable1; eauto.
(* Goal: @app_pred rmap ag_rmap (yesat pp k sh3 l) m3 *)
exists p3.
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
eapply yesat_raw_join with (phi1 := m1); eauto.
Qed.

Definition spec_parametric (Q: address -> spec) : Prop :=
   forall l l', exists pp, exists ok,
             forall sh m,
           Q l sh l' m = 
            (exists p, exists k, ok k /\ m @ l' = 
                 YES sh p k (preds_fmap (approx (level m)) (approx (level m)) pp)).

Lemma YES_ext:
  forall sh sh' rsh rsh' k p, sh=sh' -> YES sh rsh k p = YES sh' rsh' k p.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros. subst. f_equal. apply proof_irr.
Qed.

(****** Specific specs  ****************)

(* Memory predicates need to explicitly not capture any ghost state. *)
Definition VALspec : spec :=
       fun (sh: Share.t) (l: address) =>
          allp (jam (eq_dec l)
                                  (fun l' => EX v: memval, 
                                                yesat NoneP (VAL v) sh l')
                                  noat) && noghost.

Definition VALspec_range (n: Z) : spec :=
     fun (sh: Share.t) (l: address) =>
          andp (allp (jam (adr_range_dec l n)
                                  (fun l' => EX v: memval, 
                                                yesat NoneP (VAL v) sh l')
                                  noat)) noghost.

Definition nonlock_permission_bytes (sh: share) (a: address) (n: Z) : pred rmap :=
  andp (allp (jam (adr_range_dec a n) (fun i => shareat i sh && nonlockat i) noat)) noghost.

Definition nthbyte (n: Z) (l: list memval) : memval :=
     nth (nat_of_Z n) l Undef.

(*  Unfortunately address_mapsto_old, while a more elegant definition than
   address_mapsto, is not quite right.  For example, it doesn't uniquely determine v *)
Definition address_mapsto_old (ch: memory_chunk) (v: val) : spec :=
        fun (sh: Share.t) (l: AV.address)  => 
             allp (jam (adr_range_dec l (size_chunk ch)) 
                              (fun l' => yesat NoneP (VAL (nthbyte (snd l' - snd l) (encode_val ch v))) sh l')
                           noat).

Definition address_mapsto (ch: memory_chunk) (v: val) : spec :=
        fun (sh: Share.t) (l: AV.address) =>
           EX bl: list memval, 
               !! (length bl = size_chunk_nat ch  /\ decode_val ch bl = v /\ (align_chunk ch | snd l))  &&
                (allp (jam (adr_range_dec l (size_chunk ch))
                                    (fun loc => yesat NoneP (VAL (nth (nat_of_Z (snd loc - snd l)) bl Undef)) sh loc)
                                    noat)) && noghost.

Lemma address_mapsto_align: forall ch v sh l,
  address_mapsto ch v sh l = address_mapsto ch v sh l && !! (align_chunk ch | snd l).
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: @eq memval m m0 *)
(* Goal: @eq (list memval) b1 b2 *)
  pose proof (@add_andp (pred rmap) _); simpl in H. apply H; clear H.
(* Goal: @ex rmap (fun w : rmap => and (@app_pred rmap ag_rmap (address_mapsto ch (decode_val ch (encode_val ch v)) sh loc) w) (@eq rmap (@core rmap Join_rmap Sep_rmap w) (@core rmap Join_rmap Sep_rmap w0))) *)
  unfold address_mapsto.
(* Goal: @derives rmap ag_rmap (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) v) (Z.divide (align_chunk ch) (@snd block Z l))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (size_chunk ch)) (adr_range_dec l (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z l))) bl Undef)) sh loc) noat))) noghost)) (@prop rmap ag_rmap (Z.divide (align_chunk ch) (@snd block Z l))) *)
  apply exp_left; intro.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval x) (size_chunk_nat ch)) (and (@eq val (decode_val ch x) v) (Z.divide (align_chunk ch) (@snd block Z l))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (size_chunk ch)) (adr_range_dec l (size_chunk ch)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z l))) x Undef)) sh loc) noat))) noghost) (@prop rmap ag_rmap (Z.divide (align_chunk ch) (@snd block Z l))) *)
  do 2 apply andp_left1.
(* Goal: @derives rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval x) (size_chunk_nat ch)) (and (@eq val (decode_val ch x) v) (Z.divide (align_chunk ch) (@snd block Z l))))) (@prop rmap ag_rmap (Z.divide (align_chunk ch) (@snd block Z l))) *)
  intros ? [? [? ?]].
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  auto.
Qed.

Lemma address_mapsto_fun:
  forall ch sh sh' l v v',
          (address_mapsto ch v sh l * TT) && (address_mapsto ch v' sh' l * TT) |-- !!(v=v').
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v sh l) (@TT rmap ag_rmap)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v' sh' l) (@TT rmap ag_rmap))) (@prop rmap ag_rmap (@eq val v v')) *)
intros m [? ?]. unfold prop.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val v v') (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val v v'))) m *)
destruct H as [m1 [m2 [J [[bl [[[Hlen [? _]] ?] Hg]] _]]]].
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val v v') (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val v v'))) m *)
destruct H0 as [m1' [m2' [J' [[bl' [[[Hlen' [? _]] ?] Hg']] _]]]].
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
subst.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
assert (forall i, nth_error bl i = nth_error bl' i).
intro i; specialize( H1 (fst l, snd l + Z_of_nat i)); specialize( H2 (fst l, snd l + Z_of_nat i)).
(* Goal: @app_pred rmap ag_rmap (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (size_chunk ch)) (adr_range_dec l (size_chunk ch)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat l') w *)
unfold jam in *.
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
destruct l as [b z].
simpl in *.
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
if_tac in H1.
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
destruct H as [_ ?].
replace (z + Z_of_nat i - z) with (Z_of_nat i) in * by omega.
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
assert ((i < length bl)%nat).
(* Goal: lt i (@Datatypes.length memval bl) *)
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
rewrite Hlen.
(* Goal: lt i (size_chunk_nat ch) *)
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
rewrite size_chunk_conv in H.
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (Z.of_nat n))) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
omega.
rewrite <- Hlen' in Hlen.
rewrite nat_of_Z_eq in *.
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
destruct H1; destruct H2.
unfold yesat_raw in *.
repeat rewrite preds_fmap_NoneP in *.
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
assert (H5: nth i bl Undef = nth i bl' Undef).
apply (resource_at_join _ _ _ (b,z + Z_of_nat i)) in J.
apply (resource_at_join _ _ _ (b,z + Z_of_nat i)) in J'.
(* Goal: @eq memval (@nth memval i bl Undef) (@nth memval i bl' Undef) *)
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
rewrite H1 in J; rewrite H2 in J'; clear H1 H2.
(* Goal: @eq memval (@nth memval i bl Undef) (@nth memval i bl' Undef) *)
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
inv J; inv J'; try congruence.
clear - Hlen H0 H5.
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
revert bl bl' Hlen H0 H5; induction i; destruct bl; destruct bl'; simpl; intros; auto; try omegaContradiction.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
apply IHi; auto.
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (Z.of_nat n))) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
omega.
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
assert (~ (i < length bl)%nat).
(* Goal: not (lt i n) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
contradict H.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
split; auto.
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (size_chunk ch))) *)
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
rewrite Hlen in H.
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (size_chunk ch))) *)
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
rewrite size_chunk_conv.
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (Z.of_nat n))) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
omega.
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (Z.of_nat n))) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
assert (i >= length bl)%nat by omega.
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
destruct (nth_error_length i bl).
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
rewrite H5; auto.
(* Goal: @eq (option memval) (@None memval) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
destruct (nth_error_length i bl').
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
rewrite H7; auto.
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (Z.of_nat n))) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
omega.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
clear - H.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
assert (bl=bl'); [| subst; auto].
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
revert bl' H; induction bl; destruct bl'; intros; auto.
(* Goal: @eq memval m m0 *)
(* Goal: @eq (list memval) b1 b2 *)
specialize (H 0%nat); simpl in H. inv H.
(* Goal: @eq memval m m0 *)
(* Goal: @eq (list memval) b1 b2 *)
specialize (H 0%nat); simpl in H. inv H.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
f_equal.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
specialize (H 0%nat); simpl in H. inv H. auto.
(* Goal: @eq (list memval) bl bl' *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl') (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl') (decode_val ch bl')))) m *)
apply IHbl.
(* Goal: forall i : nat, @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
intro.
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl') (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl') (decode_val ch bl')))) m *)
specialize( H (S i)).
(* Goal: @eq memval m m0 *)
(* Goal: @eq (list memval) b1 b2 *)
simpl in H.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
simpl; auto.
Qed.

Definition LKspec lock_size (R: pred rmap) : spec :=
   fun (sh: Share.t) (l: AV.address)  =>
    allp (jam (adr_range_dec l lock_size)
               (fun l' => yesat (SomeP Mpred (fun _ => R)) (LK lock_size (snd l' - snd l)) sh l')
               noat) && noghost.

(*Lenb: moved to veric/seplog.v
(* Goal: @eq share sh Share.bot *)
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
Definition packPQ {A: rmaps.TypeTree}
  (P Q: forall ts, dependent_type_functor_rec ts (AssertTT A) (pred rmap)):
  forall ts, dependent_type_functor_rec ts (SpecTT A) (pred rmap) :=
  fun ts a b => if b then P ts a else Q ts a.
*)
Definition TTat (l: address) : pred rmap := TT.

(*
Definition FUNspec (fml: funsig) cc (A: TypeTree)
  (P Q: forall ts, dependent_type_functor_rec ts (AssertTT A) (pred rmap))
  (l: address): pred rmap :=
  allp (jam (eq_dec l)
         (pureat (SomeP (SpecTT A) (packPQ P Q)) (FUN fml cc)) TTat).

Definition fun_assert (fml: funsig) cc (A: TypeTree)
  (P Q: forall ts, dependent_type_functor_rec ts (AssertTT A) (pred rmap))
  (v: val)  : pred rmap :=
(* Goal: (let (a, _) := readable (adr_add loc i) in a) m *)
(* Goal: adr_range loc n (adr_add loc i) *)
 (EX b : block, !! (v = Vptr b Int.zero) && FUNspec fml cc A P Q (b, 0))%pred.
*)

(***********)

(*Lenb: dead?
Lemma ewand_lem1x:
  forall S P: mpred,
          S |-- P * TT ->
          S |-- P * (ewand P S).
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: @derives rmap ag_rmap (address_mapsto ch v sh l) (VALspec_range (size_chunk ch) sh l) *)
intros w ?. specialize (H w H0).
destruct H as [w1 [w2 [? [? _]]]].
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
exists w1; exists w2; split3; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
exists w1; exists w; split3; auto.
Qed.*)

Lemma address_mapsto_old_parametric: forall ch v, 
   spec_parametric (fun l sh l' => yesat NoneP (VAL (nthbyte (snd l' - snd l) (encode_val ch v))) sh l').
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
exists NoneP. exists (fun k => k= VAL (nthbyte (snd l' - snd l) (encode_val ch v))).
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m) (@ex (readable_share sh) (fun p : readable_share sh => @ex AV.kind (fun k : AV.kind => and (@ex memval (fun v : memval => @eq kind k (VAL v))) (@eq resource (resource_at m l') (YES sh p k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) NoneP)))))) *)
unfold yesat.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => @ex (readable_share sh) (fun rsh : readable_share sh => @app_pred rmap ag_rmap (yesat_raw NoneP (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) sh rsh l') m)) (yesat_obligation_1 NoneP (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) sh l')) m) (@ex (readable_share sh) (fun p : readable_share sh => @ex AV.kind (fun k : AV.kind => and (@eq kind k (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v)))) (@eq resource (resource_at m l') (YES sh p k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) NoneP)))))) *)
apply exists_ext; intro p.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (yesat_raw NoneP (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) sh p l') m) (@ex AV.kind (fun k : AV.kind => and (@eq kind k (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v)))) (@eq resource (resource_at m l') (YES sh p k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) NoneP))))) *)
unfold yesat_raw.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
simpl.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
apply prop_ext; split; intros.
(* Goal: @ex AV.kind (fun k : AV.kind => and (@eq kind k (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v)))) (@eq resource (resource_at m l') (YES sh p k (SomeP (ConstType unit) (fun _ : list Type => tt))))) *)
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
econstructor; split; [reflexivity | ].
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
rewrite H; f_equal.

(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
simpl.
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
eauto.
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
destruct H as [k [? ?]].
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
subst; auto.
Qed.

Lemma VALspec_parametric: 
  spec_parametric (fun l sh l' => EX v: memval,  yesat NoneP (VAL v) sh l').
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: spec_parametric (fun (_ : address) (sh : Share.t) (l' : AV.address) => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) *)
exists NoneP.
(* Goal: @ex (forall _ : AV.kind, Prop) (fun ok : forall _ : AV.kind, Prop => forall (sh : Share.t) (m : rmap), @eq Prop (@app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m) (@ex (readable_share sh) (fun p : readable_share sh => @ex AV.kind (fun k : AV.kind => and (ok k) (@eq resource (resource_at m l') (YES sh p k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) NoneP))))))) *)
exists (fun k => exists v, k=VAL v).
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m) (@ex (readable_share sh) (fun p : readable_share sh => @ex AV.kind (fun k : AV.kind => and (@ex memval (fun v : memval => @eq kind k (VAL v))) (@eq resource (resource_at m l') (YES sh p k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) NoneP)))))) *)
unfold yesat.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
apply prop_ext; split; intros.
(* Goal: @app_pred rmap ag_rmap (readable (adr_add loc i)) m *)
(* Goal: adr_range loc n (adr_add loc i) *)
destruct H as [v [p ?]].
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z l))) bl Undef)) sh l') w *)
exists p.
(* Goal: @ex AV.kind (fun k : AV.kind => and (@ex memval (fun v : memval => @eq kind k (VAL v))) (@eq resource (resource_at m l') (YES sh p k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) NoneP)))) *)
(* Goal: @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => @ex (readable_share sh) (fun rsh : readable_share sh => @app_pred rmap ag_rmap (yesat_raw NoneP (VAL v) sh rsh l') m)) (yesat_obligation_1 NoneP (VAL v) sh l'))) m *)
exists (VAL v).
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
split; eauto.
(* Goal: @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => @ex (readable_share sh) (fun rsh : readable_share sh => @app_pred rmap ag_rmap (yesat_raw NoneP (VAL v) sh rsh l') m)) (yesat_obligation_1 NoneP (VAL v) sh l'))) m *)
destruct H as [p [k [[v ?] ?]]].
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
subst.
(* Goal: @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => @ex (readable_share sh) (fun rsh : readable_share sh => @app_pred rmap ag_rmap (yesat_raw NoneP (VAL v) sh rsh l') m)) (yesat_obligation_1 NoneP (VAL v) sh l'))) m *)
exists v.
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z l))) bl Undef)) sh l') w *)
exists p.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
auto.
Qed.

Lemma LKspec_parametric lock_size: forall R: pred rmap,
  spec_parametric (fun l sh l' => yesat (SomeP Mpred (fun _ => R)) (LK lock_size (snd l' - snd l)) sh l').
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: @eq (forall _ : address, @pred rmap ag_rmap) (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (Zpos xH)) (adr_range_dec l (Zpos xH)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat) (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (@eq address l) (@eq_dec address EqDec_address l) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat) *)
unfold jam.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intro; intros.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
simpl.
exists (SomeP Mpred (fun _ => R)).
exists (fun k => k = LK lock_size (snd l' - snd l)).
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => @ex (readable_share sh) (fun rsh : readable_share sh => @app_pred rmap ag_rmap (yesat_raw NoneP (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) sh rsh l') m)) (yesat_obligation_1 NoneP (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) sh l')) m) (@ex (readable_share sh) (fun p : readable_share sh => @ex AV.kind (fun k : AV.kind => and (@eq kind k (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v)))) (@eq resource (resource_at m l') (YES sh p k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) NoneP)))))) *)
apply exists_ext; intro p.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
apply prop_ext; split; intros.
rewrite H.
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
econstructor.  split; eauto.

(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
destruct H as [k [? ?]].
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
subst; auto.
Qed.

(*
Lemma FUNspec_parametric: forall fml cc A P Q,
   spec_parametric (fun l sh => yesat (SomeP (SpecTT A) (packPQ P Q)) (FUN fml cc) sh).
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
exists (SomeP (SpecTT A) (packPQ P Q)).
exists (fun k => k=FUN fml cc).
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
simpl.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => @ex (readable_share sh) (fun rsh : readable_share sh => @app_pred rmap ag_rmap (yesat_raw NoneP (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) sh rsh l') m)) (yesat_obligation_1 NoneP (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) sh l')) m) (@ex (readable_share sh) (fun p : readable_share sh => @ex AV.kind (fun k : AV.kind => and (@eq kind k (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v)))) (@eq resource (resource_at m l') (YES sh p k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) NoneP)))))) *)
apply exists_ext; intro p.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (yesat_raw NoneP (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) sh p l') m) (@ex AV.kind (fun k : AV.kind => and (@eq kind k (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v)))) (@eq resource (resource_at m l') (YES sh p k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) NoneP))))) *)
unfold yesat_raw.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
apply prop_ext; split; intros.
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
econstructor; eauto.
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
destruct H as [k [? ?]].
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
subst; auto.
Qed.
*)
Definition val2address (v: val) : option AV.address := 
  match v with Vptr b ofs => Some (b, Ptrofs.signed ofs) | _ => None end.

Lemma VALspec_readable:
  forall l sh w,  (VALspec sh l * TT) %pred w -> readable l w.
(* The converse is not quite true, because "readable" does constraint to NoneP *)
Proof.
unfold VALspec, readable;
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => match resource_at phi l as anonymous' return (forall _ : @eq resource anonymous' (resource_at phi l), Prop) with | NO sh n => fun _ : @eq resource (NO sh n) (resource_at phi l) => False | YES wildcard' wildcard'0 k wildcard'1 => fun _ : @eq resource (YES wildcard' wildcard'0 k wildcard'1) (resource_at phi l) => isVAL k | PURE k p => fun _ : @eq resource (PURE k p) (resource_at phi l) => False end (@eq_refl resource (resource_at phi l))) (compcert_rmaps.readable_obligation_3 l)) w *)
destruct H as [w1 [w2 [? [[? ?] _]]]].
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => match resource_at phi l as anonymous' return (forall _ : @eq resource anonymous' (resource_at phi l), Prop) with | NO sh n => fun _ : @eq resource (NO sh n) (resource_at phi l) => False | YES wildcard' wildcard'0 k wildcard'1 => fun _ : @eq resource (YES wildcard' wildcard'0 k wildcard'1) (resource_at phi l) => isVAL k | PURE k p => fun _ : @eq resource (PURE k p) (resource_at phi l) => False end (@eq_refl resource (resource_at phi l))) (compcert_rmaps.readable_obligation_3 l)) w *)
specialize ( H0 l).
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => match resource_at phi l as anonymous' return (forall _ : @eq resource anonymous' (resource_at phi l), Prop) with | NO sh n => fun _ : @eq resource (NO sh n) (resource_at phi l) => False | YES wildcard' wildcard'0 k wildcard'1 => fun _ : @eq resource (YES wildcard' wildcard'0 k wildcard'1) (resource_at phi l) => isVAL k | PURE k p => fun _ : @eq resource (PURE k p) (resource_at phi l) => False end (@eq_refl resource (resource_at phi l))) (compcert_rmaps.readable_obligation_3 l)) w *)
unfold jam in H0.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
hnf in H0|-*; rewrite if_true in H0 by auto.
(* Goal: @app_pred rmap ag_rmap (writable (adr_add loc i)) m *)
(* Goal: adr_range loc n (adr_add loc i) *)
destruct H0 as [v [p ?]].
(* Goal: match resource_at w l as anonymous' return (forall _ : @eq resource anonymous' (resource_at w l), Prop) with | NO sh n => fun _ : @eq resource (NO sh n) (resource_at w l) => False | YES wildcard' wildcard'0 k wildcard'1 => fun _ : @eq resource (YES wildcard' wildcard'0 k wildcard'1) (resource_at w l) => isVAL k | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w l) => False end (@eq_refl resource (resource_at w l)) *)
unfold yesat_raw in H0.
(* Goal: match resource_at w l as anonymous' return (forall _ : @eq resource anonymous' (resource_at w l), Prop) with | NO sh n => fun _ : @eq resource (NO sh n) (resource_at w l) => False | YES wildcard' wildcard'0 k wildcard'1 => fun _ : @eq resource (YES wildcard' wildcard'0 k wildcard'1) (resource_at w l) => isVAL k | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w l) => False end (@eq_refl resource (resource_at w l)) *)
generalize (resource_at_join _ _ _ l H); rewrite H0; intro Hx.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
inv Hx; auto.
Qed.


(* NOT TRUE, because of CompCert_AV.valid problems.
Lemma jam_con: forall A (S: A -> Prop) P Q,
     allp (jam S P Q) |-- allp (jam S P (fun _ => emp)) * (allp (jam S (fun _ => emp) Q)).
*)

Lemma address_mapsto_VALspec:
  forall ch v sh l i, 0 <= i < size_chunk ch ->
        address_mapsto ch v sh l |-- VALspec sh (adr_add l i) * TT.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros. intros w ?.
pose (f l' := if eq_dec (adr_add l i) l' then w @ l' 
                   else if adr_range_dec l (size_chunk ch) l' then NO Share.bot bot_unreadable else w @ l').
pose (g l' := if eq_dec (adr_add l i) l' then NO Share.bot bot_unreadable else w @ l').
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
exploit (deallocate (w) f g); intros.
*
unfold f,g; clear f g.
destruct H0 as [b [[? ?] Hg]]. specialize (H1 l0).  hnf in H1.
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
if_tac in H1. destruct H1.  hnf in H1. if_tac; rewrite H1; constructor.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
apply join_unit2; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
apply join_unit1; auto.
(* Goal: @eq Prop (if @eq_dec address EqDec_address l l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) (if adr_range_dec l (Zpos xH) l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) *)
if_tac.
contradiction H2. unfold adr_add in H3; destruct l; destruct l0; simpl in H3. inv H3.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
split; auto. omega.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
do 3 red in H1. apply identity_unit' in H1. auto.
*
apply join_comm, core_unit.
*
destruct H1 as [phi1 [phi2 [? ?]]].
destruct (join_ex_identities w) as [e [? ?]].
exists phi1; exists phi2.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
split; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
split; auto.
(* Goal: @app_pred rmap ag_rmap (nonlock_permission_bytes sh a Z0) a0 *)
unfold VALspec; split.
(* Goal: @app_pred rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (size_chunk ch)) (adr_range_dec l (size_chunk ch)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat)) w *)
intro l'.
(* Goal: @app_pred rmap ag_rmap (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (size_chunk ch)) (adr_range_dec l (size_chunk ch)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat l') w *)
unfold jam in *.
destruct H0 as [bl [[H0' ?] Hg]].
specialize ( H0 l').
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => match resource_at phi l as anonymous' return (forall _ : @eq resource anonymous' (resource_at phi l), Prop) with | NO sh n => fun _ : @eq resource (NO sh n) (resource_at phi l) => False | YES wildcard' wildcard'0 k wildcard'1 => fun _ : @eq resource (YES wildcard' wildcard'0 k wildcard'1) (resource_at phi l) => isVAL k | PURE k p => fun _ : @eq resource (PURE k p) (resource_at phi l) => False end (@eq_refl resource (resource_at phi l))) (compcert_rmaps.readable_obligation_3 l)) w *)
unfold jam in H0.
hnf in H0|-*; if_tac.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m) (if adr_range_dec l (Zpos xH) l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) *)
(* Goal: @eq Prop (@app_pred rmap ag_rmap (noat l') m) (if adr_range_dec l (Zpos xH) l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) *)
subst l'.
(* Goal: @app_pred rmap ag_rmap (writable (adr_add loc i)) m *)
rewrite if_true in H0.
(* Goal: @identity resource Join_resource (resource_at a l) *)
destruct H0.
(* Goal: match resource_at w l as anonymous' return (forall _ : @eq resource anonymous' (resource_at w l), Prop) with | NO sh n => fun _ : @eq resource (NO sh n) (resource_at w l) => False | YES wildcard' wildcard'0 k wildcard'1 => fun _ : @eq resource (YES wildcard' wildcard'0 k wildcard'1) (resource_at w l) => isVAL k | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w l) => False end (@eq_refl resource (resource_at w l)) *)
unfold yesat_raw in H0.
destruct H2 as [H2 _].
pose proof (equal_f H2 (adr_add l i)).
unfold f in H5.
rewrite if_true in H5.
rewrite H0 in H5.
exists (nth (nat_of_Z (snd (adr_add l i) - snd l)) bl Undef).
exists x.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (yesat_raw NoneP (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) sh p l') m) (@ex AV.kind (fun k : AV.kind => and (@eq kind k (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v)))) (@eq resource (resource_at m l') (YES sh p k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) NoneP))))) *)
unfold yesat_raw.
hnf in H0|-*.
repeat rewrite preds_fmap_NoneP in *.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
destruct l; unfold adr_range, adr_add. split; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
destruct l; unfold adr_range, adr_add. split; auto.
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (Z.of_nat n))) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
simpl; omega.
(* Goal: @app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) a *)
do 3 red.
destruct H2 as [-> _]. unfold f.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
rewrite if_false; auto.
(* Goal: @eq Prop (if @eq_dec address EqDec_address l l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) (if adr_range_dec l (Zpos xH) l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) *)
if_tac. apply NO_identity. apply H0.
simpl; destruct H2 as [_ ->].
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
destruct H0 as [bl [[H0' ?] Hg]]; auto.
Qed.


Lemma address_mapsto_exists:
  forall ch v sh (rsh: readable_share sh) loc w0
      (RESERVE: forall l', adr_range loc (size_chunk ch) l' -> w0 @ l' = NO Share.bot bot_unreadable)
      (Hg: identity (ghost_of w0)),
      (align_chunk ch | snd loc) ->
      exists w, address_mapsto ch (decode_val ch (encode_val ch v)) sh loc w 
                    /\ core w = core w0.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros. rename H into Halign.
(* Goal: @ex rmap (fun w : rmap => and (@app_pred rmap ag_rmap (address_mapsto ch (decode_val ch (encode_val ch v)) sh loc) w) (@eq rmap (@core rmap Join_rmap Sep_rmap w) (@core rmap Join_rmap Sep_rmap w0))) *)
unfold address_mapsto.
pose (f l' := if adr_range_dec loc (size_chunk ch) l'
                     then YES sh rsh (VAL (nthbyte (snd l' - snd loc) (encode_val ch v))) NoneP
                     else core w0 @ l').
(* Goal: @ex rmap (fun w : rmap => and (@app_pred rmap ag_rmap (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) (decode_val ch (encode_val ch v))) (Z.divide (align_chunk ch) (@snd block Z loc))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun loc0 : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc0) (@snd block Z loc))) bl Undef)) sh loc0) noat))) noghost)) w) (@eq rmap (@core rmap Join_rmap Sep_rmap w) (@core rmap Join_rmap Sep_rmap w0))) *)
pose proof I.
(* Goal: @ex rmap (fun w : rmap => and (@app_pred rmap ag_rmap (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) (decode_val ch (encode_val ch v))) (Z.divide (align_chunk ch) (@snd block Z loc))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun loc0 : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc0) (@snd block Z loc))) bl Undef)) sh loc0) noat))) noghost)) w) (@eq rmap (@core rmap Join_rmap Sep_rmap w) (@core rmap Join_rmap Sep_rmap w0))) *)
destruct (make_rmap f (ghost_of w0) (level w0)) as [phi [? ?]].
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
extensionality l; unfold f, compose; simpl.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
if_tac; simpl; auto.
rewrite <- level_core.
(* Goal: @eq resource (resource_fmap (approx (@level rmap ag_rmap (@core rmap Join_rmap Sep_rmap w0))) (approx (@level rmap ag_rmap (@core rmap Join_rmap Sep_rmap w0))) (resource_at (@core rmap Join_rmap Sep_rmap w0) l)) (resource_at (@core rmap Join_rmap Sep_rmap w0) l) *)
(* Goal: @eq ghost (ghost_fmap (approx (@level rmap ag_rmap w0)) (approx (@level rmap ag_rmap w0)) (ghost_of w0)) (ghost_of w0) *)
(* Goal: @ex rmap (fun w : rmap => and (@app_pred rmap ag_rmap (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) (decode_val ch (encode_val ch v))) (Z.divide (align_chunk ch) (@snd block Z loc))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun loc0 : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc0) (@snd block Z loc))) bl Undef)) sh loc0) noat))) noghost)) w) (@eq rmap (@core rmap Join_rmap Sep_rmap w) (@core rmap Join_rmap Sep_rmap w0))) *)
apply resource_at_approx.
(* Goal: @eq ghost (ghost_fmap (approx (@level rmap ag_rmap w0)) (approx (@level rmap ag_rmap w0)) (ghost_of w0)) (ghost_of w0) *)
{ apply ghost_of_approx. }
(* Goal: @ex rmap (fun w : rmap => and (@app_pred rmap ag_rmap (@exp rmap ag_rmap (list memval) (fun bl : list memval => @andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval bl) (size_chunk_nat ch)) (and (@eq val (decode_val ch bl) (decode_val ch (encode_val ch v))) (Z.divide (align_chunk ch) (@snd block Z loc))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun loc0 : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc0) (@snd block Z loc))) bl Undef)) sh loc0) noat))) noghost)) w) (@eq rmap (@core rmap Join_rmap Sep_rmap w) (@core rmap Join_rmap Sep_rmap w0))) *)
exists phi.
(* Goal: @app_pred rmap ag_rmap (nonlock_permission_bytes sh a Z0) a0 *)
split.
+ exists (encode_val ch v).
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@eq nat (@Datatypes.length memval (encode_val ch v)) (size_chunk_nat ch)) (and (@eq val (decode_val ch (encode_val ch v)) (decode_val ch (encode_val ch v))) (Z.divide (align_chunk ch) (@snd block Z loc))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun loc0 : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc0) (@snd block Z loc))) (encode_val ch v) Undef)) sh loc0) noat))) noghost) phi *)
  split; [split|].
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  split; auto.
(* Goal: @eq nat (@Datatypes.length memval (encode_val ch v)) (size_chunk_nat ch) *)
(* Goal: @app_pred rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range loc (size_chunk ch)) (adr_range_dec loc (size_chunk ch)) (fun loc0 : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc0) (@snd block Z loc))) (encode_val ch v) Undef)) sh loc0) noat)) phi *)
(* Goal: @app_pred rmap ag_rmap noghost phi *)
  apply encode_val_length.
(* Goal: @app_pred rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (size_chunk ch)) (adr_range_dec l (size_chunk ch)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat)) w *)
  intro l'.
(* Goal: @eq (forall _ : address, @pred rmap ag_rmap) (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (Zpos xH)) (adr_range_dec l (Zpos xH)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat) (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (@eq address l) (@eq_dec address EqDec_address l) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat) *)
  unfold jam.
(* Goal: @app_pred rmap ag_rmap (@prop rmap ag_rmap (@eq val v1 v2)) w *)
  hnf.
(* Goal: if adr_range_dec loc (size_chunk ch) l' then @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) (encode_val ch v) Undef)) sh l') phi else @app_pred rmap ag_rmap (noat l') phi *)
(* Goal: @app_pred rmap ag_rmap noghost phi *)
  unfold yesat, yesat_raw, noat.
(* Goal: if adr_range_dec loc (size_chunk ch) l' then @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => @ex (readable_share sh) (fun rsh : readable_share sh => @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun phi : rmap => @eq resource (resource_at phi l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) (encode_val ch v) Undef)) (preds_fmap (approx (@level rmap ag_rmap phi)) (approx (@level rmap ag_rmap phi)) NoneP))) (yesat_raw_obligation_1 NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) (encode_val ch v) Undef)) sh rsh l')) m)) (yesat_obligation_1 NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) (encode_val ch v) Undef)) sh l')) phi else @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => @identity resource Join_resource (resource_at m l')) (noat_obligation_1 l')) phi *)
(* Goal: @app_pred rmap ag_rmap noghost phi *)
  unfold app_pred, proj1_sig. destruct H1; rewrite H1; clear H H1.
(* Goal: if adr_range_dec loc (size_chunk ch) l' then @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (f l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) (encode_val ch v) Undef)) (preds_fmap (approx (@level rmap ag_rmap phi)) (approx (@level rmap ag_rmap phi)) NoneP))) else @identity resource Join_resource (f l') *)
(* Goal: @app_pred rmap ag_rmap noghost phi *)
  unfold f; clear f.
(* Goal: @eq Prop (if @eq_dec address EqDec_address l l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) (if adr_range_dec l (Zpos xH) l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) *)
  if_tac.
(* Goal: @ex (readable_share sh) (fun rsh0 : readable_share sh => @eq resource (YES sh rsh (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z loc)) (encode_val ch v))) NoneP) (YES sh rsh0 (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z loc))) (encode_val ch v) Undef)) (preds_fmap (approx (@level rmap ag_rmap phi)) (approx (@level rmap ag_rmap phi)) NoneP))) *)
(* Goal: @identity resource Join_resource (resource_at (@core rmap Join_rmap Sep_rmap w0) l') *)
(* Goal: @app_pred rmap ag_rmap noghost phi *)
  exists rsh.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
  f_equal.
  rewrite <- core_resource_at.
(* Goal: @identity resource Join_resource (@core resource Join_resource Sep_resource (resource_at w0 l')) *)
(* Goal: @app_pred rmap ag_rmap noghost phi *)
  apply core_identity.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
  simpl.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  destruct H1 as [_ ->]; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
+ apply rmap_ext. do 2 rewrite level_core. auto.
(* Goal: forall l : AV.address, @eq resource (resource_at (@core rmap Join_rmap Sep_rmap phi) l) (resource_at (@core rmap Join_rmap Sep_rmap w0) l) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap phi)) (ghost_of (@core rmap Join_rmap Sep_rmap w0)) *)
  intro l; specialize (RESERVE l).
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at phi l)) (resource_at (@core rmap Join_rmap Sep_rmap w0) l) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap phi)) (ghost_of (@core rmap Join_rmap Sep_rmap w0)) *)
  rewrite <- core_resource_at. destruct H1. rewrite H1. unfold f.
(* Goal: @eq Prop (if @eq_dec address EqDec_address l l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) (if adr_range_dec l (Zpos xH) l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) *)
  if_tac.
(* Goal: @eq resource (@core resource Join_resource Sep_resource (YES sh rsh (VAL (nthbyte (Z.sub (@snd block Z l) (@snd block Z loc)) (encode_val ch v))) NoneP)) (resource_at (@core rmap Join_rmap Sep_rmap w0) l) *)
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at (@core rmap Join_rmap Sep_rmap w0) l)) (resource_at (@core rmap Join_rmap Sep_rmap w0) l) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap phi)) (ghost_of (@core rmap Join_rmap Sep_rmap w0)) *)
  rewrite core_YES.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  rewrite <- core_resource_at. rewrite RESERVE; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  rewrite core_NO; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  rewrite <- core_resource_at; rewrite core_idem; auto.
(* Goal: @eq share sh Share.bot *)
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
  { rewrite <- core_ghost_of.
    destruct H1 as [_ ->].
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    rewrite core_ghost_of; auto. }
Qed.

(*  NOT TRUE, because readable doesn't constraint NoneP ...
Lemma readable_VAL:
 forall w l, readable l (w_m w) <-> exists sh, (VALspec sh l * TT) w.

*)

Lemma VALspec1: VALspec_range 1 = VALspec.
Proof.
(* Goal: @eq spec (VALspec_range (Zpos xH)) VALspec *)
unfold VALspec, VALspec_range.
(* Goal: @eq spec (fun (sh : Share.t) (l : address) => @andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (Zpos xH)) (adr_range_dec l (Zpos xH)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat)) noghost) (fun (sh : Share.t) (l : address) => @andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (@eq address l) (@eq_dec address EqDec_address l) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat)) noghost) *)
extensionality sh l.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
f_equal; f_equal.
(* Goal: @eq (forall _ : address, @pred rmap ag_rmap) (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (Zpos xH)) (adr_range_dec l (Zpos xH)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat) (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (@eq address l) (@eq_dec address EqDec_address l) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat) *)
unfold jam.
(* Goal: @eq (forall _ : address, @pred rmap ag_rmap) (fun l0 : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => if adr_range_dec l (Zpos xH) l0 then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l0)) m else @app_pred rmap ag_rmap (noat l0) m) (jam_obligation_1 rmap ag_rmap address (adr_range l (Zpos xH)) (adr_range_dec l (Zpos xH)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat l0)) (fun l0 : address => @exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => if @eq_dec address EqDec_address l l0 then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l0)) m else @app_pred rmap ag_rmap (noat l0) m) (jam_obligation_1 rmap ag_rmap address (@eq address l) (@eq_dec address EqDec_address l) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat l0)) *)
extensionality l'.
(* Goal: @eq (@sig (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p)) (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => if adr_range_dec l (Zpos xH) l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) (jam_obligation_1 rmap ag_rmap address (adr_range l (Zpos xH)) (adr_range_dec l (Zpos xH)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat l')) (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun m : rmap => if @eq_dec address EqDec_address l l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) (jam_obligation_1 rmap ag_rmap address (@eq address l) (@eq_dec address EqDec_address l) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat l')) *)
apply exist_ext; extensionality m.
(* Goal: @eq Prop (if adr_range_dec l (Zpos xH) l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) (if @eq_dec address EqDec_address l l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) *)
symmetry.
(* Goal: @eq Prop (if @eq_dec address EqDec_address l l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) (if adr_range_dec l (Zpos xH) l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) *)
if_tac.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
 subst l'. rewrite if_true; auto.
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (Z.of_nat n))) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
destruct l; split; auto; omega.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
rewrite if_false; auto.
destruct l; destruct l'; unfold block in *; intros [? ?]; try omega.
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
subst.
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (Z.of_nat n))) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
contradict H. f_equal; omega.
Qed.

Lemma VALspec_range_exp_address_mapsto:
  forall ch sh l,
    (align_chunk ch | snd l) ->
    VALspec_range (size_chunk ch) sh l |-- EX v: val, address_mapsto ch v sh l.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: @derives rmap ag_rmap (address_mapsto ch v sh l) (VALspec_range (size_chunk ch) sh l) *)
  intros w ?.
(* Goal: @app_pred rmap ag_rmap (@exp rmap ag_rmap val (fun v : val => address_mapsto ch v sh l)) w *)
  destruct H0 as [H0 Hg].
  simpl in H0 |- *.
  cut (exists (b0 : list memval),
     length b0 = size_chunk_nat ch /\
     (forall b1 : address,
      if adr_range_dec l (size_chunk ch) b1
      then
       exists rsh: readable_share sh,
         w @ b1 =
         YES sh rsh
           (VAL (nth (nat_of_Z (snd b1 - snd l)) b0 Undef))
           (SomeP (ConstType unit) (fun _ => tt))
      else identity (w @ b1))).
(* Goal: @eq share sh Share.bot *)
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
  {
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
    intros.
(* Goal: @ex val (fun b : val => @ex (list memval) (fun b0 : list memval => and (and (and (@eq nat (@Datatypes.length memval b0) (size_chunk_nat ch)) (and (@eq val (decode_val ch b0) b) (Z.divide (align_chunk ch) (@snd block Z l)))) (forall b1 : address, if adr_range_dec l (size_chunk ch) b1 then @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b1) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b1) (@snd block Z l))) b0 Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))) else @identity resource Join_resource (resource_at w b1))) (@identity ghost ghost_join (ghost_of w)))) *)
    destruct H1 as [b0 [? ?]].
(* Goal: @ex val (fun b : val => @ex (list memval) (fun b0 : list memval => and (and (and (@eq nat (@Datatypes.length memval b0) (size_chunk_nat ch)) (and (@eq val (decode_val ch b0) b) (Z.divide (align_chunk ch) (@snd block Z l)))) (forall b1 : address, if adr_range_dec l (size_chunk ch) b1 then @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b1) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b1) (@snd block Z l))) b0 Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))) else @identity resource Join_resource (resource_at w b1))) (@identity ghost ghost_join (ghost_of w)))) *)
    exists (decode_val ch b0), b0.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    tauto.
  }
  rewrite !size_chunk_conv in *.
  forget (size_chunk_nat ch) as n; clear - H0.

  cut (exists b0 : list memval,
     length b0 = n /\
     (forall b1 : address,
        adr_range l (Z.of_nat n) b1 ->
       exists rsh: readable_share sh,
         w @ b1 =
         YES sh rsh
           (VAL (nth (nat_of_Z (snd b1 - snd l)) b0 Undef))
           (SomeP (ConstType unit) (fun _ => tt)))).
(* Goal: @eq share sh Share.bot *)
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
  {
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
    intros.
(* Goal: @ex (list memval) (fun b0 : list memval => and (@eq nat (@Datatypes.length memval b0) n) (forall b1 : address, if adr_range_dec l (Z.of_nat n) b1 then @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b1) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b1) (@snd block Z l))) b0 Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))) else @identity resource Join_resource (resource_at w b1))) *)
    destruct H as [b0 H].
(* Goal: @ex (list memval) (fun b0 : list memval => and (@eq nat (@Datatypes.length memval b0) n) (forall b1 : address, if adr_range_dec l (Z.of_nat n) b1 then @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b1) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b1) (@snd block Z l))) b0 Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))) else @identity resource Join_resource (resource_at w b1))) *)
    exists b0.
(* Goal: and (@eq nat (@Datatypes.length memval b0) n) (forall b1 : address, if adr_range_dec l (Z.of_nat n) b1 then @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b1) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b1) (@snd block Z l))) b0 Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))) else @identity resource Join_resource (resource_at w b1)) *)
    split; [tauto |].
(* Goal: forall b1 : address, if adr_range_dec l (Z.of_nat n) b1 then @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b1) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b1) (@snd block Z l))) b0 Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))) else @identity resource Join_resource (resource_at w b1) *)
    intros b; specialize (H0 b).
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    if_tac; [apply (proj2 H) |]; auto.
  }

  assert (forall b : address,
    adr_range l (Z.of_nat n) b ->
        exists (b0 : memval) (rsh : readable_share sh),
          w @ b =
          YES sh rsh (VAL b0)
            (SomeP (ConstType unit) (fun _ => tt))).
(* Goal: @eq share sh Share.bot *)
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
  {
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
    intros.
(* Goal: @ex memval (fun b0 : memval => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b) (YES sh rsh (VAL b0) (SomeP (ConstType unit) (fun _ : list Type => tt))))) *)
    specialize (H0 b).
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    if_tac in H0; tauto.
  }
(* Goal: @ex (list memval) (fun b0 : list memval => and (@eq nat (@Datatypes.length memval b0) n) (forall (b1 : address) (_ : adr_range l (Z.of_nat n) b1), @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b1) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b1) (@snd block Z l))) b0 Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))))) *)
  clear H0.

(* Goal: @ex (list memval) (fun b0 : list memval => and (@eq nat (@Datatypes.length memval b0) n) (forall (b1 : address) (_ : adr_range l (Z.of_nat n) b1), @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b1) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b1) (@snd block Z l))) b0 Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))))) *)
  destruct l as [bl ofs].
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  revert ofs H; induction n; intros.
  + exists nil.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    split; auto.
(* Goal: forall (b1 : address) (_ : adr_range (@pair block Z bl ofs) (Z.of_nat O) b1), @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b1) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b1) (@snd block Z (@pair block Z bl ofs)))) (@nil memval) Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))) *)
    intros b.
(* Goal: forall _ : adr_range (@pair block Z bl ofs) (Z.of_nat O) b, @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z (@pair block Z bl ofs)))) (@nil memval) Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))) *)
    specialize (H b).
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    auto.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
    intros.
(* Goal: @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b) (@snd block Z (@pair block Z bl ofs)))) (@nil memval) Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))) *)
    apply adr_range_non_zero in H0.
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (Z.of_nat n))) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
    simpl in H0; omega.
  + specialize (IHn (ofs + 1)).
(* Goal: @ex (list memval) (fun b0 : list memval => and (@eq nat (@Datatypes.length memval b0) (S n)) (forall (b1 : address) (_ : adr_range (@pair block Z bl ofs) (Z.of_nat (S n)) b1), @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b1) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b1) (@snd block Z (@pair block Z bl ofs)))) b0 Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))))) *)
    spec IHn.
    - clear - H; intros b; specialize (H b).
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      intros; spec H; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      apply adr_range_shift_1; auto.
    - assert (adr_range (bl, ofs) (Z.of_nat (S n)) (bl, ofs))
        by (rewrite Nat2Z.inj_succ; repeat split; auto; omega).
(* Goal: @ex (list memval) (fun b0 : list memval => and (@eq nat (@Datatypes.length memval b0) n) (forall (b1 : address) (_ : adr_range l (Z.of_nat n) b1), @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b1) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b1) (@snd block Z l))) b0 Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))))) *)
      destruct (H _ H0) as [b_hd ?H]; clear H0.
(* Goal: @ex (list memval) (fun b0 : list memval => and (@eq nat (@Datatypes.length memval b0) (S n)) (forall (b1 : address) (_ : adr_range (@pair block Z bl ofs) (Z.of_nat (S n)) b1), @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b1) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b1) (@snd block Z (@pair block Z bl ofs)))) b0 Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))))) *)
      destruct IHn as [b_tl ?H].
(* Goal: @ex (list memval) (fun b0 : list memval => and (@eq nat (@Datatypes.length memval b0) (S n)) (forall (b1 : address) (_ : adr_range (@pair block Z bl ofs) (Z.of_nat (S n)) b1), @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b1) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b1) (@snd block Z (@pair block Z bl ofs)))) b0 Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))))) *)
      exists (b_hd :: b_tl).
(* Goal: and (@eq nat (@Datatypes.length memval (@cons memval b_hd b_tl)) (S n)) (forall (b1 : address) (_ : adr_range (@pair block Z bl ofs) (Z.of_nat (S n)) b1), @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b1) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b1) (@snd block Z (@pair block Z bl ofs)))) (@cons memval b_hd b_tl) Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt))))) *)
      split; [simpl; omega |]; destruct H0 as [_ ?].
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
      intros.
(* Goal: @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b1) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b1) (@snd block Z (@pair block Z bl ofs)))) (@cons memval b_hd b_tl) Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))) *)
      apply adr_range_S_split in H2.
(* Goal: @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b1) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b1) (@snd block Z (@pair block Z bl ofs)))) (@cons memval b_hd b_tl) Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))) *)
      destruct H2.
      * destruct (H0 b1 H2) as [p ?H].
(* Goal: @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w b1) (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z b1) (@snd block Z (@pair block Z bl ofs)))) (@cons memval b_hd b_tl) Undef)) (SomeP (ConstType unit) (fun _ : list Type => tt)))) *)
        destruct b1; destruct H2 as [_ ?].
        exists p; clear - H2 H3.
        unfold snd in *.
        replace (nat_of_Z (z - ofs)) with (S (nat_of_Z (z - (ofs + 1)))); [exact H3 |].
(* Goal: @eq nat (S (nat_of_Z (Z.sub z (Z.add ofs (Zpos xH))))) (nat_of_Z (Z.sub z ofs)) *)
        unfold nat_of_Z.
        replace (z - ofs) with (Z.succ (z - (ofs + 1))) by omega.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
        rewrite Z2Nat.inj_succ; auto.
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (Z.of_nat n))) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
        omega.
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
      * subst. rewrite Z.sub_diag. simpl nth.
(* Goal: @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at w (@pair block Z bl ofs)) (YES sh rsh (VAL b_hd) (SomeP (ConstType unit) (fun _ : list Type => tt)))) *)
        exact H1.
Qed.

Lemma address_mapsto_VALspec_range:
  forall ch v sh l,
        address_mapsto ch v sh l |-- VALspec_range (size_chunk ch) sh l.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: @derives rmap ag_rmap (address_mapsto ch v sh l) (VALspec_range (size_chunk ch) sh l) *)
intros w ?. unfold VALspec_range.
(* Goal: @app_pred rmap ag_rmap (@andp rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (size_chunk ch)) (adr_range_dec l (size_chunk ch)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat)) noghost) w *)
destruct H as [bl [[Hbl ?] Hg]].
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
split; auto.
(* Goal: @app_pred rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (size_chunk ch)) (adr_range_dec l (size_chunk ch)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat)) w *)
intro l'.
(* Goal: @app_pred rmap ag_rmap (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (size_chunk ch)) (adr_range_dec l (size_chunk ch)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat l') w *)
specialize ( H l').
(* Goal: @app_pred rmap ag_rmap (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (size_chunk ch)) (adr_range_dec l (size_chunk ch)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat l') w *)
unfold jam in *.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
hnf in H|-*. if_tac; auto.
exists (nth (nat_of_Z (snd l' - snd l)) bl Undef).
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z l))) bl Undef)) sh l') w *)
destruct H as [p ?].
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z l))) bl Undef)) sh l') w *)
exists p.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
auto.
Qed.

Lemma approx_eq_i:
  forall (P Q: pred rmap) (w: rmap),
      (|> ! (P <=> Q)) w -> approx (level w) P = approx (level w) Q.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: @eq (@pred rmap ag_rmap) (approx (@level rmap ag_rmap w) P) (approx (@level rmap ag_rmap w) Q) *)
apply pred_ext'; extensionality m'.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (approx (@level rmap ag_rmap w) P) m') (@app_pred rmap ag_rmap (approx (@level rmap ag_rmap w) Q) m') *)
unfold approx.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
apply and_ext'; auto; intros.
(* Goal: @eq Prop (@app_pred rmap ag_rmap P m') (@app_pred rmap ag_rmap Q m') *)
destruct (level_later_fash _ _ H0) as [m1 [? ?]].
(* Goal: @eq Prop (@app_pred rmap ag_rmap P m') (@app_pred rmap ag_rmap Q m') *)
specialize (H _ H1).
(* Goal: @eq Prop (@app_pred rmap ag_rmap P m') (@app_pred rmap ag_rmap Q m') *)
specialize (H m').
(* Goal: @eq Prop (@app_pred rmap ag_rmap P m') (@app_pred rmap ag_rmap Q m') *)
spec H.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
rewrite H2; auto.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (p x) w) (@app_pred rmap ag_rmap (a x) w) *)
destruct H; apply prop_ext. intuition.
Qed.

(* Goal: @eq share sh Share.bot *)
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
Lemma level_later {A} `{H : ageable A}: forall {w: A} {n': nat},
         laterR (level w) n' ->
       exists w', laterR w w' /\ n' = level w'.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat n' (@level A H w'))) *)
remember (level w) as n.
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
revert w Heqn; induction H0; intros; subst.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
case_eq (age1 w); intros.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
exists a; split. constructor; auto.
symmetry; unfold age in H0; simpl in H0.
  unfold natAge1 in H0; simpl in H0. revert H0; case_eq (level w); intros; inv H2.
(* Goal: @eq nat (@level A H a) y *)
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat y (@level A H w'))) *)
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
  apply age_level in H1. congruence. rewrite age1_level0 in H1.
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat y (@level A H w'))) *)
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
   rewrite H1 in H0. inv H0.
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
 specialize (IHclos_trans1 _ (refl_equal _)).
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
  destruct IHclos_trans1 as [w2 [? ?]].
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
  subst.
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
  specialize (IHclos_trans2 _ (refl_equal _)).
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
  destruct IHclos_trans2 as [w3 [? ?]].
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
  subst.
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
  exists w3; split; auto. econstructor 2; eauto.
Qed.

(* TODO: resume this lemma. *)
(*
Lemma fun_assert_contractive:
   forall fml cc (A: TypeTree)
     (P Q: pred rmap -> forall ts, dependent_type_functor_rec ts (AssertTT A) (pred rmap)) v,
      (forall ts x rho, nonexpansive (fun R => P R ts x rho)) ->
      (forall ts x rho, nonexpansive (fun R => Q R ts x rho)) ->
      contractive (fun R : pred rmap => fun_assert fml cc A (P R) (Q R) v).
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
  (*
  assert (H': forall xvl: A * environ, nonexpansive (fun R => P R (fst xvl) (snd xvl)))
    by auto; clear H; rename H' into H.
  assert (H': forall xvl: A * environ, nonexpansive (fun R => Q R (fst xvl) (snd xvl)))
    by auto; clear H0; rename H' into H0.
  *)
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intro; intros.
  rename H0 into H'.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intro; intros.
  intro; intros; split; intros ? ? H7; simpl in H1.
  + assert (a >= level a')%nat.
(* Goal: @eq share sh Share.bot *)
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
    {
      apply necR_level in H2. clear - H1 H2.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      apply le_trans with (level y); auto.
    }
    clear y H1 H2. rename H3 into H2.
(* Goal: @app_pred rmap ag_rmap (@prop rmap ag_rmap (@eq val v1 v2)) w *)
    hnf.
    destruct H7 as [loc H7].
    hnf in H7. destruct H7 as [H1 H3].  hnf in H1.
    exists loc.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    apply prop_andp_i; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    split; auto.
    hnf in H3|-*.
    intro; specialize ( H3 b).
    hnf in H3|-*.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    if_tac; auto.
    subst b.
    hnf in H3|-*.
    rewrite H3; clear H3.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
    f_equal.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
    simpl.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
    f_equal.
    extensionality ts.
(* Goal: @eq (forall _ : A, @pred rmap ag_rmap) (@compose A (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) p) (@compose A (@pred rmap ag_rmap) (@pred rmap ag_rmap) (approx n) a) *)
    extensionality x.
    extensionality b.
    extensionality rho.
    unfold packPQ.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
    simpl.
(* Goal: @eq Prop (if @eq_dec address EqDec_address l l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) (if adr_range_dec l (Zpos xH) l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) *)
    if_tac.
    - (* P proof *)
      specialize ( H ts x rho P0 Q0).
Check approx_eq_i.
      apply approx_eq_i.
pose proof (later_derives (unfash_derives H)).
      apply (later_derives (unfash_derives H)); clear H.
      rewrite later_unfash.
      unfold unfash.
(* Goal: (let (a, _) := readable (adr_add loc i) in a) m *)
(* Goal: adr_range loc n (adr_add loc i) *)
      red. red.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      apply pred_nec_hereditary with a; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      apply nec_nat; auto.
(* Q proof *)
clear H; rename H' into H.
specialize ( H (x,vl) P0 Q0).
apply approx_eq_i.
apply (later_derives (unfash_derives H)); clear H.
rewrite later_unfash.
(* Goal: (let (a, _) := readable (adr_add loc i) in a) m *)
(* Goal: adr_range loc n (adr_add loc i) *)
red. red. red.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
apply pred_nec_hereditary with a; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
apply nec_nat; auto.
(* Part 2 *)
assert (a >= level a')%nat.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
 apply necR_level in H2. clear - H1 H2. apply le_trans with (level y); auto.
 clear y H1 H2. rename H3 into H2.
unfold fun_assert.
destruct H7 as [loc H7].
hnf in H7. destruct H7 as [H1 H3].  hnf in H1.
exists loc.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
apply prop_andp_i; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
split; auto.
(* Goal: @app_pred rmap ag_rmap (@prop rmap ag_rmap (@eq val v1 v2)) w *)
hnf.
(* Goal: forall i : nat, @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
intro.
specialize ( H3 b).
hnf in H3|-*.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
if_tac; auto.
subst b.
hnf in H3|-*.
unfold yesat_raw in *.
rewrite H3; clear H3.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
f_equal.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
simpl.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
f_equal.
unfold compose.
extensionality xy; destruct xy as [x [y [vl [ ] ]]].
unfold packPQ.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
simpl.
(* Goal: @eq Prop (if @eq_dec address EqDec_address l l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) (if adr_range_dec l (Zpos xH) l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) *)
if_tac.
(* P proof *)
specialize ( H (x,vl) P0 Q0).
(* Goal: @eq Prop (if adr_range_dec l (Zpos xH) l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) (if @eq_dec address EqDec_address l l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) *)
symmetry.
apply approx_eq_i.
apply (later_derives (unfash_derives H)); clear H.
rewrite later_unfash.
(* Goal: (let (a, _) := readable (adr_add loc i) in a) m *)
(* Goal: adr_range loc n (adr_add loc i) *)
red. red. red.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
apply pred_nec_hereditary with a; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
apply nec_nat; auto.
(* Q proof *)
clear H; rename H' into H.
specialize ( H (x,vl) P0 Q0).
(* Goal: @eq Prop (if adr_range_dec l (Zpos xH) l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) (if @eq_dec address EqDec_address l l' then @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) m else @app_pred rmap ag_rmap (noat l') m) *)
symmetry.
apply approx_eq_i.
apply (later_derives (unfash_derives H)); clear H.
rewrite later_unfash.
(* Goal: (let (a, _) := readable (adr_add loc i) in a) m *)
(* Goal: adr_range loc n (adr_add loc i) *)
red. red. red.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
apply pred_nec_hereditary with a; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
apply nec_nat; auto.
Qed.
*)
Lemma VALspec_range_bytes_readable:
  forall n sh loc m, VALspec_range n sh loc m -> bytes_readable loc n m.
Proof.
(* Goal: forall (_ : memory_chunk) (_ : address) (_ : val) (_ : list memval) (_ : address), (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) *)
intros; intro; intros.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch1 v1 sh l1) (address_mapsto ch2 v2 sh l2)) (@FF rmap ag_rmap) *)
destruct H.
(* Goal: @app_pred rmap ag_rmap (readable (adr_add loc i)) m *)
specialize ( H (adr_add loc i)).
(* Goal: @app_pred rmap ag_rmap (readable (adr_add loc i)) m *)
(* Goal: adr_range loc n (adr_add loc i) *)
hnf in H.
(* Goal: @app_pred rmap ag_rmap (readable (adr_add loc i)) m *)
rewrite if_true in H.
(* Goal: @app_pred rmap ag_rmap (readable (adr_add loc i)) m *)
(* Goal: adr_range loc n (adr_add loc i) *)
destruct H as [v [p ?]].
(* Goal: @app_pred rmap ag_rmap (readable (adr_add loc i)) m *)
(* Goal: adr_range loc n (adr_add loc i) *)
hnf in H.
(* Goal: (let (a, _) := readable (adr_add loc i) in a) m *)
(* Goal: adr_range loc n (adr_add loc i) *)
red. red. red.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
rewrite H; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
destruct loc; split; unfold adr_add; auto.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
simpl. omega.
Qed.

Lemma VALspec_range_bytes_writable:
  forall n sh loc m, writable_share sh -> VALspec_range n sh loc m -> bytes_writable loc n m.
Proof.
(* Goal: forall (_ : memory_chunk) (_ : address) (_ : val) (_ : list memval) (_ : address), (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) *)
intros; intro; intros.
(* Goal: @identity resource Join_resource (resource_at a l) *)
destruct H0.
(* Goal: @app_pred rmap ag_rmap (writable (adr_add loc i)) m *)
specialize ( H0 (adr_add loc i)).
(* Goal: @app_pred rmap ag_rmap (writable (adr_add loc i)) m *)
(* Goal: adr_range loc n (adr_add loc i) *)
hnf in H0.
(* Goal: @app_pred rmap ag_rmap (writable (adr_add loc i)) m *)
rewrite if_true in H0.
(* Goal: @app_pred rmap ag_rmap (writable (adr_add loc i)) m *)
(* Goal: adr_range loc n (adr_add loc i) *)
destruct H0 as [v [p ?]].
(* Goal: @app_pred rmap ag_rmap (writable (adr_add loc i)) m *)
(* Goal: adr_range loc n (adr_add loc i) *)
hnf in H0.
(* Goal: @app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) a *)
do 3 red.
rewrite H0; auto with extensionality.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
destruct loc; split; unfold adr_add; auto.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
simpl. omega.
Qed.

Lemma yesat_join_sub:
  forall pp k l sh m m',
          join_sub m m' ->
          yesat pp k sh l m ->
         exists sh', yesat pp k sh' l m'.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: @identity resource Join_resource (resource_at a l) *)
destruct H0.
(* Goal: match resource_at w l as anonymous' return (forall _ : @eq resource anonymous' (resource_at w l), Prop) with | NO sh n => fun _ : @eq resource (NO sh n) (resource_at w l) => False | YES wildcard' wildcard'0 k wildcard'1 => fun _ : @eq resource (YES wildcard' wildcard'0 k wildcard'1) (resource_at w l) => isVAL k | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w l) => False end (@eq_refl resource (resource_at w l)) *)
unfold yesat_raw in H0.
(* Goal: forall i : nat, @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
generalize (resource_at_join_sub _ _ l H); rewrite H0; intro.
assert (level m = level m').
(* Goal: iff (@app_pred rmap ag_rmap P m') (@app_pred rmap ag_rmap Q m') *)
destruct H; apply join_level in H; intuition.
(* Goal: @eq resource (@core resource Join_resource Sep_resource (resource_at phi l)) (resource_at (@core rmap Join_rmap Sep_rmap w0) l) *)
(* Goal: @eq ghost (ghost_of (@core rmap Join_rmap Sep_rmap phi)) (ghost_of (@core rmap Join_rmap Sep_rmap w0)) *)
destruct H1.
(* Goal: @eq resource (resource_at phi3 l) (YES sh3 rsh3 k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) pp)) *)
destruct x0; case_eq (m' @ l); intros; rewrite H3 in H1; inv H1.
(* Goal: @eq Prop (@app_pred rmap ag_rmap (yesat_raw NoneP (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) sh p l') m) (@ex AV.kind (fun k : AV.kind => and (@eq kind k (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v)))) (@eq resource (resource_at m l') (YES sh p k (preds_fmap (approx (@level rmap ag_rmap m)) (approx (@level rmap ag_rmap m)) NoneP))))) *)
do 2 econstructor. unfold yesat_raw. simpl. rewrite <- H2.  eapply H3.
exists sh1.
(* Goal: and (Z.le z (Z.add (@snd block Z (@pair block Z b z)) i)) (Z.lt (Z.add (@snd block Z (@pair block Z b z)) i) (Z.add z n)) *)
unfold yesat. simpl.
exists r0.
rewrite <- H2. rewrite H3.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
subst; f_equal; auto.
Qed.

Lemma VALspec_range_precise: forall n sh l,  precise (VALspec_range n sh l).
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intro; intros.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
apply rmap_ext; auto.
(* Goal: iff (@app_pred rmap ag_rmap P m') (@app_pred rmap ag_rmap Q m') *)
1: destruct H1,H2; apply join_level in H1; apply join_level in H2; intuition.
(* Goal: forall i : nat, @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
intro.
destruct H as [H Hg], H0 as [H0 Hg0].
specialize (H l0); specialize (H0 l0).
(* Goal: @app_pred rmap ag_rmap (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (size_chunk ch)) (adr_range_dec l (size_chunk ch)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat l') w *)
unfold jam in *.
hnf in H, H0. if_tac in H.
+ destruct H as [v [p ?]].
  destruct H0 as [v' [p' ?]].
  unfold yesat_raw in *.
(* Goal: forall i : nat, @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
  generalize (resource_at_join_sub _ _ l0 H1); rewrite H; clear H1; intro.
(* Goal: forall i : nat, @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
  generalize (resource_at_join_sub _ _ l0 H2); rewrite H0; clear H2; intro.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
  f_equal. auto with extensionality.
  clear - H1 H2.
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @eq (option memval) (@nth_error memval bl i) (@nth_error memval bl' i) *)
(* Goal: @app_pred rmap ag_rmap (@exist (forall _ : rmap, Prop) (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => @eq val (decode_val ch bl) (decode_val ch bl')) (predicates_hered.prop_obligation_1 rmap ag_rmap (@eq val (decode_val ch bl) (decode_val ch bl')))) m *)
  destruct H1; destruct H2.
  simpl in *.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
  f_equal.
(* Goal: @eq nat (@level A H a) y *)
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat y (@level A H w'))) *)
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
  inv H0; inv H; congruence.
+ do 3 red in H,H0.
  apply (resource_at_join_sub _ _ l0) in H1.
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
  eapply join_sub_same_identity; eauto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  * apply identity_unit'; auto.
  * apply (resource_at_join_sub _ _ l0) in H2.
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
    eapply join_sub_unit_for; eauto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    apply identity_unit'; auto.
+ destruct H as [H Hg], H0 as [H0 Hg0].
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  eapply same_identity; auto.
  * destruct H1 as [? H1%ghost_of_join].
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
    rewrite (Hg _ _ H1) in H1; eauto.
  * destruct H2 as [? H2%ghost_of_join].
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
    rewrite (Hg0 _ _ H2) in H2; eauto.
Qed.

Lemma nonlock_permission_bytes_precise: forall sh p n,
  precise (nonlock_permission_bytes sh p n).
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intro; intros.
  destruct H as [H Hg], H0 as [H0 Hg0].
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  apply rmap_ext; auto.
(* Goal: iff (@app_pred rmap ag_rmap P m') (@app_pred rmap ag_rmap Q m') *)
  1: destruct H1,H2; apply join_level in H1; apply join_level in H2; intuition.
(* Goal: forall i : nat, @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
  intro.
  specialize (H l); specialize (H0 l).
(* Goal: @app_pred rmap ag_rmap (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range l (size_chunk ch)) (adr_range_dec l (size_chunk ch)) (fun l' : address => @exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh l')) noat l') w *)
  unfold jam in *.
  hnf in H, H0. if_tac in H.
  + unfold shareat, nonlockat in H, H0; simpl in H, H0.
    apply (resource_at_join_sub _ _ l) in H1.
    apply (resource_at_join_sub _ _ l) in H2.
    destruct H as [? _], H0 as [? _].
    clear - H H0 H1 H2.
    destruct H1 as [b1 H1], H2 as [b2 H2].
    destruct (w1 @ l), (w2 @ l); inv H1; inv H2; simpl in *;
    repeat match goal with H: Some _ = Some _ |- _ => inv H end;
    repeat f_equal; try apply proof_irr; try congruence;
(* Goal: False *)
    try contradiction.
  + do 3 red in H,H0.
    apply (resource_at_join_sub _ _ l) in H1.
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
    eapply join_sub_same_identity; eauto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    * apply identity_unit'; auto.
    * apply (resource_at_join_sub _ _ l) in H2.
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
      eapply join_sub_unit_for; eauto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      apply identity_unit'; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  + eapply same_identity; auto.
    * destruct H1 as [? H1%ghost_of_join].
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
      rewrite (Hg _ _ H1) in H1; eauto.
    * destruct H2 as [? H2%ghost_of_join].
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
      rewrite (Hg0 _ _ H2) in H2; eauto.
Qed.

Lemma address_mapsto_precise: forall ch v sh l, precise (address_mapsto ch v sh l).
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: @precise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (address_mapsto ch v sh l) *)
apply (derives_precise _ _ (address_mapsto_VALspec_range ch v sh l)).
(* Goal: @precise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap (VALspec_range (size_chunk ch) sh l) *)
apply VALspec_range_precise.
Qed.

Lemma LKspec_precise lock_size: forall R sh l, precise (LKspec lock_size R sh l).
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intros.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
intro; intros.
assert (level w1 = level w2) as Hlevel.
(* Goal: iff (@app_pred rmap ag_rmap P m') (@app_pred rmap ag_rmap Q m') *)
{ destruct H1,H2; apply join_level in H1; apply join_level in H2; intuition. }
destruct H as [H Hg], H0 as [H0 Hg0].
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
apply rmap_ext; auto; intros.
-
specialize (H l0); specialize (H0 l0).
simpl in *.
if_tac in H0.
(* Goal: @identity resource Join_resource (resource_at a l) *)
destruct H. destruct H0. rewrite H,H0.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
f_equal. proof_irr. auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
rewrite Hlevel; auto.
apply (resource_at_join_sub _ _ l0) in H1.
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
  eapply join_sub_same_identity; eauto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  * apply identity_unit'; auto.
  * apply (resource_at_join_sub _ _ l0) in H2.
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
    eapply join_sub_unit_for; eauto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    apply identity_unit'; auto.
-
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
 eapply same_identity; auto.
    * destruct H1 as [? H1%ghost_of_join].
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
      rewrite (Hg _ _ H1) in H1; eauto.
    * destruct H2 as [? H2%ghost_of_join].
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
      rewrite (Hg0 _ _ H2) in H2; eauto.
Qed.

Program Definition core_load (ch: memory_chunk) (l: address) (v: val): pred rmap :=
  EX bl: list memval,
  !!(length bl = size_chunk_nat ch /\ decode_val ch bl = v /\ (align_chunk ch | snd l)) &&
    allp (jam (adr_range_dec l (size_chunk ch))
      (fun l' phi => exists sh, exists rsh, phi @ l' 
        = YES sh rsh (VAL (nth (nat_of_Z (snd l' - snd l)) bl Undef)) NoneP)
      (fun _ _ => True)).
 Next Obligation.
(* Goal: forall (_ : memory_chunk) (_ : address) (_ : val) (_ : list memval) (_ : address), (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) *)
    intros; intro; intros.
(* Goal: @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at a' l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z l))) bl Undef)) NoneP))) *)
  destruct H0 as [sh [rsh ?]]; exists sh, rsh.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    apply (age1_YES a a'); auto.
  Qed.
  Next Obligation.     intros; intro; intros. auto.
  Qed.

Program Definition core_load' (ch: memory_chunk) (l: address) (v: val) (bl: list memval)
  : pred rmap :=
  !!(length bl = size_chunk_nat ch /\ decode_val ch bl = v /\ (align_chunk ch | snd l)) &&
    allp (jam (adr_range_dec l (size_chunk ch))
      (fun l' phi => exists sh, exists rsh, phi @ l' 
        = YES sh rsh (VAL (nth (nat_of_Z (snd l' - snd l)) bl Undef)) NoneP)
      (fun _ _ => True)).
 Next Obligation.
(* Goal: forall (_ : memory_chunk) (_ : address) (_ : val) (_ : list memval) (_ : address), (fun p : forall _ : rmap, Prop => @hereditary rmap (@age rmap ag_rmap) p) (fun _ : rmap => True) *)
    intros; intro; intros.
(* Goal: @ex Share.t (fun sh : Share.t => @ex (readable_share sh) (fun rsh : readable_share sh => @eq resource (resource_at a' l') (YES sh rsh (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z l') (@snd block Z l))) bl Undef)) NoneP))) *)
  destruct H0 as [sh [rsh ?]]; exists sh, rsh.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    apply (age1_YES a a'); auto.
  Qed.
  Next Obligation.     intros; intro; intros. auto.
  Qed.

Lemma VALspec_range_0: forall sh loc, VALspec_range 0 sh loc = emp.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
 intros.
(* Goal: @eq (@pred rmap ag_rmap) (nonlock_permission_bytes sh a Z0) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
 apply pred_ext.
(* Goal: @eq memval m m0 *)
(* Goal: @eq (list memval) b1 b2 *)
 - intros ? [? ?]. simpl in H.
(* Goal: @app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) a *)
   do 3 red.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
   apply all_resource_at_identity; auto.
(* Goal: forall l : AV.address, @identity resource Join_resource (resource_at a l) *)
   intro l. specialize (H l).
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
   rewrite if_false in H; auto.
   destruct loc, l; intros [? ?]; simpl in *; omega.
 - intros ? ?. split. intro b. rewrite jam_false.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
   do 3 red. apply resource_at_identity; auto.
   destruct loc, b; intros [? ?]; simpl in *; omega.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
   apply ghost_of_identity; auto.
Qed.
Hint Resolve VALspec_range_0: normalize.

Lemma nonlock_permission_bytes_0: forall sh a, nonlock_permission_bytes sh a 0 = emp.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (nonlock_permission_bytes sh a Z0) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
  apply pred_ext.
(* Goal: @eq memval m m0 *)
(* Goal: @eq (list memval) b1 b2 *)
  + intros ? [? ?]. simpl in H.
(* Goal: @app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) a *)
    do 3 red.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    apply all_resource_at_identity; auto.
(* Goal: forall l : AV.address, @identity resource Join_resource (resource_at a l) *)
    intro l. specialize (H l).
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    rewrite if_false in H; auto.
    destruct a, l; intros [? ?]; simpl in *; omega.
  + intros ? ?. split. intro b. rewrite jam_false.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    do 3 red. apply resource_at_identity; auto.
    destruct a, b; intros [? ?]; simpl in *; omega.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    apply ghost_of_identity; auto.
Qed.

Lemma nonlock_permission_bytes_not_nonunit: forall sh p n,
  ~ nonunit sh ->
  nonlock_permission_bytes sh p n |-- emp.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
  assert (sh = Share.bot).
(* Goal: @eq share sh Share.bot *)
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
  {
(* Goal: @eq share sh Share.bot *)
    destruct (dec_share_identity sh).
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    + apply identity_share_bot; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    + apply nonidentity_nonunit in n0; tauto.
  }
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
  subst.
(* Goal: @eq memval m m0 *)
(* Goal: @eq (list memval) b1 b2 *)
  intros ? ?. simpl in H.
(* Goal: @app_pred rmap ag_rmap (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) a *)
  do 3 red.
(* Goal: @identity resource Join_resource (resource_at a l) *)
  destruct H0.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  apply all_resource_at_identity; auto.
(* Goal: forall l : AV.address, @identity resource Join_resource (resource_at a l) *)
  intro l.
  specialize (H0 l); simpl in H0.
(* Goal: @identity resource Join_resource (resource_at a l) *)
  if_tac in H0; [| auto].
(* Goal: @identity resource Join_resource (resource_at a l) *)
  destruct H0.
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat y (@level A H w'))) *)
(* Goal: @ex A (fun w' : A => and (@laterR A H w w') (@eq nat z (@level A H w'))) *)
  destruct (a @ l); inv H0.
  + apply NO_identity. 
  + contradiction (bot_unreadable r).
Qed.

Lemma is_resource_pred_YES_VAL sh:
  is_resource_pred
    (fun l' => EX  v: memval, yesat NoneP (VAL v) sh l')
    (fun r _ n => (exists b0 rsh, r = YES sh rsh (VAL b0)
        (SomeP (ConstType unit) (fun _ => tt)))).
Proof. hnf; intros. reflexivity. Qed.

Lemma is_resource_pred_YES_VAL' sh v:
  is_resource_pred
    (fun l' => yesat NoneP (VAL (v l')) sh l')
    (fun r l n => (exists rsh, r = YES sh rsh (VAL (v l))
        (SomeP (ConstType unit) (fun _ => tt)))).
Proof. hnf; intros. reflexivity. Qed.

Lemma is_resource_pred_nonlock_shareat sh:
  is_resource_pred
    (fun i : address => shareat i sh && nonlockat i)
    (fun r _ _ => resource_share r = Some sh /\ nonlock r).
Proof. hnf; intros. reflexivity. Qed.

Lemma VALspec_range_split2:
  forall (n m r: Z) (sh: Share.t) (b: block) (ofs: Z),
    r = n + m -> n >= 0 -> m >= 0 ->
    VALspec_range r sh (b, ofs) = 
    VALspec_range n sh (b, ofs) * VALspec_range m sh (b, ofs + n).
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
  assert (exists resp, is_resource_pred (fun l' => EX  v: memval, yesat NoneP (VAL v) sh l') resp) by (eexists; apply is_resource_pred_YES_VAL).
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  apply allp_jam_split2; auto.
  + split; intros [? ?]; unfold adr_range.
    - assert (ofs <= z < ofs + r <-> ofs <= z < ofs + n \/ ofs + n <= z < ofs + n + m) by omega.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      tauto.
    - omega.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  + intros.
(* Goal: or (isVAL k) (isFUN k) *)
    simpl in H4.
(* Goal: or (isVAL k) (isFUN k) *)
    destruct (m0 @ l); try solve [inversion H5; simpl; auto].
(* Goal: or (isVAL k) (isFUN k) *)
    destruct H4 as [? [? ?]].
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
    inversion H4; subst.
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh p n) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
    inversion H5; subst.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    auto.
Qed.

Lemma nonlock_permission_bytes_split2:
  forall (n m r: Z) (sh: Share.t) (b: block) (ofs: Z),
    r = n + m -> n >= 0 -> m >= 0 ->
    nonlock_permission_bytes sh (b, ofs) r =
    nonlock_permission_bytes sh (b, ofs) n *
    nonlock_permission_bytes sh (b, ofs + n) m.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (nonlock_permission_bytes sh (@pair block Z b ofs) r) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (nonlock_permission_bytes sh (@pair block Z b ofs) n) (nonlock_permission_bytes sh (@pair block Z b (Z.add ofs n)) m)) *)
  assert (exists resp, is_resource_pred (fun i : address => shareat i sh && nonlockat i) resp) by (eexists; apply is_resource_pred_nonlock_shareat).
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  apply allp_jam_split2; auto.
  + split; intros [? ?]; unfold adr_range.
    - assert (ofs <= z < ofs + r <-> ofs <= z < ofs + n \/ ofs + n <= z < ofs + n + m) by omega.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
      tauto.
    - omega.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  + intros.
(* Goal: or (isVAL k) (isFUN k) *)
    destruct H4 as [_ ?].
(* Goal: or (isVAL k) (isFUN k) *)
    simpl in H4.
(* Goal: or (isVAL k) (isFUN k) *)
    destruct (m0 @ l); inv H5.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    simpl in H4; auto.
Qed.

Lemma VALspec_range_VALspec:
  forall (n : Z) (v : val) (sh : Share.t) (l : address) (i : Z),
       0 <= i < n ->
       VALspec_range n sh l
       |-- VALspec sh (adr_add l i) * TT.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
 intros.
(* Goal: @derives rmap ag_rmap (VALspec_range n sh l) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec sh (adr_add l i)) (@TT rmap ag_rmap)) *)
  destruct l as [b ofs].
  rewrite (VALspec_range_split2 i (n-i) n sh b ofs); try omega.
  rewrite (VALspec_range_split2 1 (n-i-1) (n-i) sh b (ofs+i)); try omega.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec_range i sh (@pair block Z b ofs)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec_range (Zpos xH) sh (@pair block Z b (Z.add ofs i))) (VALspec_range (Z.sub (Z.sub n i) (Zpos xH)) sh (@pair block Z b (Z.add (Z.add ofs i) (Zpos xH)))))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec sh (adr_add (@pair block Z b ofs) i)) (@TT rmap ag_rmap)) *)
  change (VALspec_range 1) with (VALspec_range 1).
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec_range i sh (@pair block Z b ofs)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec_range (Zpos xH) sh (@pair block Z b (Z.add ofs i))) (VALspec_range (Z.sub (Z.sub n i) (Zpos xH)) sh (@pair block Z b (Z.add (Z.add ofs i) (Zpos xH)))))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec sh (adr_add (@pair block Z b ofs) i)) (@TT rmap ag_rmap)) *)
  rewrite VALspec1.
  rewrite <- sepcon_assoc.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec_range i sh (@pair block Z b ofs)) (VALspec sh (@pair block Z b (Z.add ofs i)))) (VALspec_range (Z.sub (Z.sub n i) (Zpos xH)) sh (@pair block Z b (Z.add (Z.add ofs i) (Zpos xH))))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec sh (adr_add (@pair block Z b ofs) i)) (@TT rmap ag_rmap)) *)
  rewrite (sepcon_comm (VALspec_range i sh (b, ofs))).
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec sh (@pair block Z b (Z.add ofs i))) (VALspec_range i sh (@pair block Z b ofs))) (VALspec_range (Z.sub (Z.sub n i) (Zpos xH)) sh (@pair block Z b (Z.add (Z.add ofs i) (Zpos xH))))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec sh (adr_add (@pair block Z b ofs) i)) (@TT rmap ag_rmap)) *)
  rewrite sepcon_assoc.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  apply sepcon_derives; auto.
Qed.

Lemma VALspec_range_overlap': forall sh p1 p2 n1 n2,
  adr_range p1 n1 p2 ->
  n2 > 0 ->
  VALspec_range n1 sh p1 * VALspec_range n2 sh p2 |-- FF.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
  intros w [w1 [w2 [? [[? Hg1] [? Hg2]]]]].
  specialize ( H2 p2).
  specialize ( H3 p2).
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  rewrite jam_true in H2 by auto.
  rewrite jam_true in H3 by (destruct p2; simpl; split; auto; omega).
  destruct H2; destruct H3. hnf in H2,H3.
  apply (resource_at_join _ _ _ p2) in H1.
  destruct H2, H3.
  rewrite H2, H3 in H1.
  clear - x1 H1; simpl in H1.
(* Goal: @eq resource (resource_at phi3 l) (YES sh3 rsh3 k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) pp)) *)
  inv H1.
  clear - x1 RJ.
(* Goal: forall i : nat, @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
  generalize (join_self' RJ); intro. subst sh3.
  apply readable_nonidentity in x1.
  apply x1. apply identity_unit_equiv. apply RJ.
Qed.

Lemma address_mapsto_overlap':
  forall sh ch1 v1 ch2 v2 a1 a2,
     adr_range a1 (size_chunk ch1) a2 ->
     address_mapsto ch1 v1 sh a1 * address_mapsto ch2 v2 sh a2 |-- FF.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
  eapply derives_trans; [eapply sepcon_derives | apply VALspec_range_overlap'].
  + apply address_mapsto_VALspec_range.
  + apply address_mapsto_VALspec_range.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  + auto.
  + apply size_chunk_pos.
Qed.

Lemma VALspec_range_overlap: forall sh l1 n1 l2 n2,
  range_overlap l1 n1 l2 n2 ->
  VALspec_range n1 sh l1 * VALspec_range n2 sh l2 |-- FF.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec_range n1 sh l1) (VALspec_range n2 sh l2)) (@FF rmap ag_rmap) *)
  pose proof range_overlap_non_zero _ _ _ _ H.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  apply range_overlap_spec in H; try tauto.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch1 v1 sh l1) (address_mapsto ch2 v2 sh l2)) (@FF rmap ag_rmap) *)
  destruct H.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  + apply VALspec_range_overlap'; tauto.
  + rewrite sepcon_comm.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    apply VALspec_range_overlap'; tauto.
Qed.

Lemma address_mapsto_overlap: forall sh l1 ch1 v1 l2 ch2 v2,
  range_overlap l1 (size_chunk ch1) l2 (size_chunk ch2) ->
  address_mapsto ch1 v1 sh l1 * address_mapsto ch2 v2 sh l2 |-- FF.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
  apply range_overlap_spec in H; try apply size_chunk_pos.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch1 v1 sh l1) (address_mapsto ch2 v2 sh l2)) (@FF rmap ag_rmap) *)
  destruct H.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  + apply address_mapsto_overlap'; auto.
  + rewrite sepcon_comm.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    apply address_mapsto_overlap'; auto.
Qed.

Lemma share_joins_self: forall sh: share, joins sh sh -> nonunit sh -> False.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
(* Goal: False *)
  destruct H as [sh' ?].
(* Goal: False *)
  apply nonunit_nonidentity in H0; contradiction H0.
(* Goal: @eq resource (resource_at m l') (YES sh p (VAL (nthbyte (Z.sub (@snd block Z l') (@snd block Z l)) (encode_val ch v))) (SomeP (ConstType unit) (fun _ : list Type => tt))) *)
  eapply join_self; eauto.
Qed.

Lemma nonlock_permission_bytes_overlap:
  forall sh n1 n2 p1 p2,
  nonunit sh ->
  range_overlap p1 n1 p2 n2 ->
  nonlock_permission_bytes sh p1 n1 * nonlock_permission_bytes sh p2 n2 |-- FF.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  intros.
  eapply derives_trans; [apply sepcon_derives; apply andp_left1, derives_refl|].
  apply allp_jam_overlap.
  + eexists. apply is_resource_pred_nonlock_shareat.
  + eexists. apply is_resource_pred_nonlock_shareat.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
  + unfold shareat; simpl; intros.
    destruct H3 as [w ?].
    apply (resource_at_join _ _ _ l) in H3.
    pose proof resource_share_joins (w1 @ l) (w2 @ l) sh sh.
    do 2 (spec H4; [tauto |]).
    spec H4; [firstorder |].
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
    apply (share_joins_self sh); auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
  + auto.
Qed.

Lemma address_mapsto_value_cohere':
  forall ch v1 v2 sh1 sh2 a r
 (Hmaps1 : address_mapsto ch v1 sh1 a r)
 (Hmaps2 : address_mapsto ch v2 sh2 a r), v1=v2.
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
 intros.
(* Goal: @eq val v1 v2 *)
 destruct Hmaps1 as [b1 [[[Hlen1 [? ?]] Hall1] Hg1]].
(* Goal: @eq val v1 v2 *)
 destruct Hmaps2 as [b2 [[[Hlen2 [? ?]] Hall2] Hg2]].
(* Goal: @eq val v1 v2 *)
 assert (b1 = b2); [ | subst; auto].
 clear - Hlen1 Hlen2 Hall1 Hall2.
 rewrite size_chunk_conv in *.
(* Goal: @eq (list memval) b1 b2 *)
 forget (size_chunk_nat ch) as n. clear ch.
(* Goal: @eq (list memval) b1 b2 *)
 assert (forall i, nth_error b1 i = nth_error b2 i).
(* Goal: forall i : nat, @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 intro.
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 destruct a as [b z].
 specialize (Hall1 (b, (z+Z.of_nat i))).
 specialize (Hall2 (b, (z+Z.of_nat i))).
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 hnf in Hall1,Hall2. if_tac in Hall1. destruct H as [_ [_ ?]].
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 destruct Hall1 as (? & Hall1), Hall2 as (? & Hall2). simpl in Hall1, Hall2.
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 rewrite Hall1 in Hall2; inversion Hall2.
 replace (z + Z.of_nat i - z) with (Z.of_nat i) in H2 by omega.
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 rewrite Nat2Z.id in H2.
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (Z.of_nat n))) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 rewrite nth_error_nth with (z:=Undef) by omega.
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (Z.of_nat n))) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 rewrite nth_error_nth with (z:=Undef) by omega.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
 f_equal; auto.
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 assert (~(i<n)%nat).
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
 contradict H. split; auto. omega.
 transitivity (@None memval); [ | symmetry];
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (Z.of_nat n))) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 apply nth_error_length; omega.
 clear - H Hlen1 Hlen2.
(* Goal: @eq (list memval) b1 b2 *)
 revert b1 b2 Hlen1 Hlen2 H.
(* Goal: forall (b1 b2 : list memval) (_ : @eq nat (@Datatypes.length memval b1) n) (_ : @eq nat (@Datatypes.length memval b2) n) (_ : forall i : nat, @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i)), @eq (list memval) b1 b2 *)
 induction n; destruct b1,b2; intros; auto; inv Hlen1; inv Hlen2.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
 f_equal.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
 specialize (H O). simpl in H. inv H; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
 apply IHn; auto.
(* Goal: forall i : nat, @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
 intro i; specialize (H (S i)); apply H.
Qed.

Lemma address_mapsto_value_cohere:
  forall ch v1 v2 sh1 sh2 a,
 address_mapsto ch v1 sh1 a * address_mapsto ch v2 sh2 a |-- !! (v1=v2).
Proof.
(* Goal: forall (ch : memory_chunk) (v1 v2 : val) (sh1 sh2 : Share.t) (a : AV.address), @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto ch v1 sh1 a) (address_mapsto ch v2 sh2 a)) (@prop rmap ag_rmap (@eq val v1 v2)) *)
 intros.
(* Goal: @app_pred rmap ag_rmap (@prop rmap ag_rmap (@eq val v1 v2)) w *)
 intros w [w1 [w2 [? [? ?]]]]. hnf.
(* Goal: @eq val v1 v2 *)
 destruct H0 as [b1 [[[? [? ?]] ?] Hg1]].
(* Goal: @eq val v1 v2 *)
 destruct H1 as [b2 [[[? [? ?]] ?] Hg2]].
(* Goal: @eq val v1 v2 *)
 assert (b1 = b2); [ | subst; auto].
 clear - H H0 H4 H1 H7.
 rewrite size_chunk_conv in *.
(* Goal: @eq (list memval) b1 b2 *)
 forget (size_chunk_nat ch) as n. clear ch.
(* Goal: @eq (list memval) b1 b2 *)
 assert (forall i, nth_error b1 i = nth_error b2 i).
(* Goal: forall i : nat, @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 intro.
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 destruct a as [b z].
 specialize (H4 (b, (z+Z.of_nat i))).
 specialize (H7 (b, (z+Z.of_nat i))).
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 hnf in H4,H7. if_tac in H4. destruct H2 as [_ [_ ?]].
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 destruct H4, H7. hnf in H3,H4.
 apply (resource_at_join _ _ _ (b, z + Z.of_nat i)) in H.
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 rewrite H3,H4 in H. inv  H.
 clear - H2 H10 H1.
 replace (z + Z.of_nat i - z) with (Z.of_nat i) in H10 by omega.
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 rewrite Nat2Z.id in H10.
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (Z.of_nat n))) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 rewrite nth_error_nth with (z:=Undef) by omega.
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (Z.of_nat n))) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 rewrite nth_error_nth with (z:=Undef) by omega.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
 f_equal; auto.
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 assert (~(i<n)%nat).
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
 contradict H2. split; auto. omega.
 transitivity (@None memval); [ | symmetry];
(* Goal: and (Z.le z (Z.add z (Z.of_nat i))) (Z.lt (Z.add z (Z.of_nat i)) (Z.add z (Z.of_nat n))) *)
(* Goal: @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
(* Goal: @eq (list memval) b1 b2 *)
 apply nth_error_length; omega.
 clear - H2 H0 H1.
(* Goal: @eq (list memval) b1 b2 *)
 revert b1 b2 H0 H1 H2.
(* Goal: @eq resource (resource_at phi3 l) (YES sh3 rsh3 k (preds_fmap (approx (@level rmap ag_rmap phi3)) (approx (@level rmap ag_rmap phi3)) pp)) *)
 induction n; destruct b1,b2; intros; auto; inv H0; inv H1.
(* Goal: @eq (list memval) (@cons memval m b1) (@cons memval m0 b2) *)
 f_equal.
(* Goal: @eq memval m m0 *)
(* Goal: @eq (list memval) b1 b2 *)
 specialize (H2 O). simpl in H2. inv H2; auto.
(* Goal: or (isVAL (VAL x)) (isFUN (VAL x)) *)
 apply IHn; auto.
(* Goal: forall i : nat, @eq (option memval) (@nth_error memval b1 i) (@nth_error memval b2 i) *)
 intro i; specialize (H2 (S i)); apply H2.
Qed.

Definition almost_empty rm: Prop:=
  forall loc sh psh k P, rm @ loc = YES sh psh k P -> forall val, ~ k = VAL val.

(*Lenb: moved here from veric.initial_world.v*)
Definition no_locks phi :=
  forall addr sh sh' z z' P,
phi @ addr <> YES sh sh' (LK z z') P.

(*Lenb: moved here from veric.initial_world.v
Definition no_locks phi :=
  forall addr sh sh' z P,
    phi @ addr <> YES sh sh' (LK z) P /\
    phi @ addr <> YES sh sh' (CT z) P.

Definition func_at (f: funspec): address -> pred rmap :=
  match f with
   | mk_funspec fsig cc A P Q _ _ => pureat (SomeP (SpecTT A) (packPQ P Q)) (FUN fsig cc)
  end.

Definition func_at' (f: funspec) (loc: address) : pred rmap :=
  match f with
   | mk_funspec fsig cc _ _ _ _ _ => EX pp:_, pureat pp (FUN fsig cc) loc
  end.
*)
