Require Import VST.msl.log_normalize.
Require Import VST.msl.alg_seplog.
Require Import VST.veric.base.
Require Import VST.veric.compcert_rmaps.
Require Import VST.veric.res_predicates.

Require Import compcert.cfrontend.Ctypes.
Require Import VST.veric.address_conflict.
Require Import VST.veric.val_lemmas.
Require Import VST.veric.Cop2.
Require Import VST.veric.shares.
Require Import VST.veric.slice.

Require Import VST.veric.mpred.

(*Lenb: moved to mpred
Definition assert := environ -> mpred.  (* Unfortunately
   can't export this abbreviation through SeparationLogic.v because
  it confuses the Lift system *)
*)

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),
      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.
(* Goal: forall (ch : memory_chunk) (v : val) (sh : share) (_ : readable_share sh) (loc : address) (w0 : rmap) (_ : forall (l' : address) (_ : adr_range loc (size_chunk ch) l'), @eq resource (resource_at w0 l') (NO Share.bot bot_unreadable)) (_ : @identity ghost ghost_join (ghost_of w0)) (_ : Z.divide (align_chunk ch) (@snd block Z loc)), @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))) *)
Proof.  exact address_mapsto_exists. Qed.

Definition permission_block (sh: Share.t)  (v: val) (t: type) : mpred :=
    match access_mode t with
         | By_value ch =>
            match v with
            | Vptr b ofs =>
                 nonlock_permission_bytes sh (b, Ptrofs.unsigned ofs)
                       (size_chunk ch)
            | _ => FF
            end
         | _ => FF
         end.

Local Open Scope pred.

Definition mapsto (sh: Share.t) (t: type) (v1 v2 : val): mpred :=
  match access_mode t with
  | By_value ch =>
   match type_is_volatile t with
   | false =>
    match v1 with
     | Vptr b ofs =>
       if readable_share_dec sh
       then (!!tc_val t v2 &&
             address_mapsto ch v2 sh (b, Ptrofs.unsigned ofs)) ||
            (!! (v2 = Vundef) &&
             EX v2':val, address_mapsto ch v2' sh (b, Ptrofs.unsigned ofs))
       else !! (tc_val' t v2 /\ (align_chunk ch | Ptrofs.unsigned ofs)) && nonlock_permission_bytes sh (b, Ptrofs.unsigned ofs) (size_chunk ch)
     | _ => FF
    end
    | _ => FF
    end
  | _ => FF
  end.

Definition mapsto_ sh t v1 := mapsto sh t v1 Vundef.

Lemma address_mapsto_readable:
  forall m v sh a, address_mapsto m v sh a |-- 
           !! readable_share sh.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
intros.
(* Goal: @derives rmap ag_rmap (address_mapsto ch x sh l) (@prop rmap ag_rmap (Z.divide (align_chunk ch) (@snd block Z l))) *)
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 m)) (and (@eq val (decode_val m bl) v) (Z.divide (align_chunk m) (@snd block Z a))))) (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range a (size_chunk m)) (adr_range_dec a (size_chunk m)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z a))) bl Undef)) sh loc) noat))) noghost)) (@prop rmap ag_rmap (readable_share sh)) *)
unfold derives.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
simpl.
(* Goal: @derives rmap ag_rmap (@prop rmap ag_rmap (and (Z.le Z0 (Ptrofs.unsigned ofs)) (Z.lt (Z.add n (Ptrofs.unsigned ofs)) Ptrofs.modulus))) (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned ofs) n) Ptrofs.modulus)) *)
intros ? ?.
(* Goal: readable_share sh *)
destruct H as [bl [[[? [? ?]] ?]] ].
(* Goal: readable_share sh *)
specialize (H2 a).
(* Goal: readable_share sh *)
rewrite if_true in H2.
(* Goal: readable_share sh *)
(* Goal: adr_range a (size_chunk m) a *)
destruct H2 as [rsh ?]. auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
destruct a; split; auto.
(* Goal: and (Z.le z z) (Z.lt z (Z.add z (size_chunk m))) *)
clear; pose proof (size_chunk_pos m); omega.
Qed.

Lemma mapsto_tc_val': forall sh t p v, mapsto sh t p v |-- !! tc_val' t v.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: @eq (forall (_ : val) (_ : val), mpred) (mapsto sh (Tpointer t a)) (mapsto sh (Tpointer Tvoid a)) *)
  unfold mapsto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  destruct (access_mode t); auto.
  if_tac; auto;
  destruct p; auto;
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  try simple_if_tac; auto.
  + apply orp_left; apply andp_left1.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
    - intros ?; simpl.
(* Goal: forall _ : tc_val t v, tc_val' t v *)
      apply tc_val_tc_val'.
    - intros ? ?; simpl in *; subst.
(* Goal: tc_val' t Vundef *)
      apply tc_val'_Vundef.
  + apply andp_left1.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    intros ?; simpl; tauto.
Qed.

Lemma mapsto_value_range:
 forall sh v sz sgn i,
   readable_share sh ->
   mapsto sh (Tint sz sgn noattr) v (Vint i) =
    !! int_range sz sgn i && mapsto sh (Tint sz sgn noattr) v (Vint i).
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
intros.
(* Goal: @eq mpred (mapsto sh (Tint sz sgn noattr) v (Vint i)) (@andp rmap ag_rmap (@prop rmap ag_rmap (int_range sz sgn i)) (mapsto sh (Tint sz sgn noattr) v (Vint i))) *)
rename H into Hsh.
(* Goal: @eq mpred (mapsto sh (Tint sz sgn noattr) v (Vint i)) (@andp rmap ag_rmap (@prop rmap ag_rmap (int_range sz sgn i)) (mapsto sh (Tint sz sgn noattr) v (Vint i))) *)
assert (GG: forall a b, (a || !!(Vint i = Vundef) && b) = a). {
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
intros. apply pred_ext; intros ? ?. hnf in H.
(* Goal: @app_pred rmap ag_rmap a a0 *)
(* Goal: @app_pred rmap ag_rmap (@orp rmap ag_rmap a (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val (Vint i) Vundef)) b)) a0 *)
destruct H; auto; hnf in H; destruct H; discriminate.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
left; auto.
}
(* Goal: @eq mpred (mapsto sh (Tint sz sgn noattr) v (Vint i)) (@andp rmap ag_rmap (@prop rmap ag_rmap (int_range sz sgn i)) (mapsto sh (Tint sz sgn noattr) v (Vint i))) *)
apply pred_ext; [ | apply andp_left2; auto].
assert (MAX: Int.max_signed = 2147483648 - 1) by reflexivity.
assert (MIN: Int.min_signed = -2147483648) by reflexivity.
assert (Byte.min_signed = -128) by reflexivity.
assert (Byte.max_signed = 128-1) by reflexivity.
assert (Byte.max_unsigned = 256-1) by reflexivity.
(* Goal: @derives rmap ag_rmap (mapsto sh (Tint sz sgn noattr) v (Vint i)) (@andp rmap ag_rmap (@prop rmap ag_rmap (int_range sz sgn i)) (mapsto sh (Tint sz sgn noattr) v (Vint i))) *)
destruct (Int.unsigned_range i).
assert (Int.modulus = Int.max_unsigned + 1) by reflexivity.
(* Goal: @derives rmap ag_rmap (mapsto sh (Tint sz sgn noattr) v (Vint i)) (@andp rmap ag_rmap (@prop rmap ag_rmap (int_range sz sgn i)) (mapsto sh (Tint sz sgn noattr) v (Vint i))) *)
assert (Int.modulus = 4294967296) by reflexivity.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
apply andp_right; auto.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
unfold mapsto; intros.
replace (type_is_volatile (Tint sz sgn noattr)) with false
  by (destruct sz,sgn; reflexivity).
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
simpl.
(* Goal: @derives rmap ag_rmap match match sz with | I8 => match sgn with | Signed => By_value Mint8signed | Unsigned => By_value Mint8unsigned end | I16 => match sgn with | Signed => By_value Mint16signed | Unsigned => By_value Mint16unsigned end | I32 => By_value Mint32 | IBool => By_value Mint8unsigned end with | By_value ch => match v with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap match sz with | I8 => match sgn with | Signed => and (Z.le Byte.min_signed (Int.signed i)) (Z.le (Int.signed i) Byte.max_signed) | Unsigned => Z.le (Int.unsigned i) Byte.max_unsigned end | I16 => match sgn with | Signed => and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))) (Int.signed i)) (Z.le (Int.signed i) (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))) | Unsigned => Z.le (Int.unsigned i) (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))) end | I32 => True | IBool => or (@eq Int.int i Int.zero) (@eq Int.int i Int.one) end) (address_mapsto ch (Vint i) sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val (Vint i) Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint sz sgn noattr) (Vint i)) (Z.divide (align_chunk ch) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk ch)) end | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end (@prop rmap ag_rmap (int_range sz sgn i)) *)
destruct (readable_share_dec sh); [| tauto].
destruct sz, sgn, v; (try rewrite FF_and; auto);
 repeat rewrite GG;
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
 apply prop_andp_left; intros ? ? _; hnf; try omega.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))))))))))) (Int.signed i)) (Z.lt (Int.signed i) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))))))) *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.lt (Int.unsigned i) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))) *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.lt (Int.unsigned i) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))) *)
 pose proof (Int.signed_range i); omega.
 destruct H6; subst;
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
  try rewrite Int.unsigned_zero; try rewrite Int.unsigned_one; omega.
 destruct H6; subst;
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
  try rewrite Int.unsigned_zero; try rewrite Int.unsigned_one; omega.
Qed.

Definition writable_block (id: ident) (n: Z): assert :=
   fun rho => 
        EX b: block,  EX sh: Share.t,
          !! (writable_share sh /\ ge_of rho id = Some b) && VALspec_range n sh (b, 0).

Fixpoint writable_blocks (bl : list (ident*Z)) : assert :=
 match bl with
  | nil =>  fun rho => emp
  | (b,n)::bl' =>  fun rho => writable_block b n rho * writable_blocks bl' rho
 end.

Fixpoint address_mapsto_zeros (sh: share) (n: nat) (adr: address) : mpred :=
 match n with
 | O => emp
 | S n' => address_mapsto Mint8unsigned (Vint Int.zero) sh adr 
               * address_mapsto_zeros sh n' (fst adr, Z.succ (snd adr))
end.

Definition address_mapsto_zeros' (n: Z) : spec :=
     fun (sh: Share.t) (l: address) =>
          allp (jam (adr_range_dec l (Z.max n 0))
                                  (fun l' => yesat NoneP (VAL (Byte Byte.zero)) sh l')
                                  noat) && noghost.

Lemma address_mapsto_zeros_eq:
  forall sh n,
   address_mapsto_zeros sh n =
   address_mapsto_zeros' (Z_of_nat n) sh.
Proof.
  induction n;
  extensionality adr; destruct adr as [b i].
  * (* base case *)
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
    simpl.
(* Goal: @eq mpred (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) (address_mapsto_zeros' Z0 sh (@pair block Z b i)) *)
    unfold address_mapsto_zeros'.
(* Goal: @eq (@pred rmap ag_rmap) (VALspec_range (size_chunk ch) sh l) (@exp rmap ag_rmap val (fun v : val => address_mapsto ch v sh l)) *)
    apply pred_ext.
(* Goal: @derives rmap ag_rmap (VALspec sh (@pair block Z b i)) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b i))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b i))))) *)
    intros w ?.
(* 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 (@pair block Z b i) (Z.max Z0 Z0)) (adr_range_dec (@pair block Z b i) (Z.max Z0 Z0)) (fun l' : address => yesat NoneP (VAL (Byte Byte.zero)) sh l') noat)) noghost) w *)
(* Goal: @derives 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 (@pair block Z b i) (Z.max Z0 Z0)) (adr_range_dec (@pair block Z b i) (Z.max Z0 Z0)) (fun l' : address => yesat NoneP (VAL (Byte Byte.zero)) sh l') noat)) noghost) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
    split; [intros [b' i']|].
(* Goal: is_pointer_or_null (if Archi.ptr64 then Vlong Int64.zero else Vint Int.zero) *)
    hnf.
(* Goal: @identity resource Join_resource (if @eq_dec AV.address EqDec_address loc (@pair block Z b i) then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) *)
(* Goal: @app_pred rmap ag_rmap noghost w1 *)
    rewrite if_false.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
    simpl. apply resource_at_identity; auto.
(* Goal: not (adr_range (@pair block Z b (Z.succ i)) (Z.max (Z.of_nat n) Z0) (@pair block Z b' i')) *)
    intros [? ?]. unfold Z.max in H1;  simpl in H1. omega.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    apply ghost_of_identity; auto.
(* Goal: @derives 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 (@pair block Z b i) (Z.max Z0 Z0)) (adr_range_dec (@pair block Z b i) (Z.max Z0 Z0)) (fun l' : address => yesat NoneP (VAL (Byte Byte.zero)) sh l') noat)) noghost) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
    intros w [].
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
    simpl.
(* Goal: @identity rmap Join_rmap w *)
    apply all_resource_at_identity.
(* Goal: @app_pred rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range (@pair block Z b i) (Z.max (Z.succ (Z.of_nat n)) Z0)) (adr_range_dec (@pair block Z b i) (Z.max (Z.succ (Z.of_nat n)) Z0)) (fun l' : address => yesat NoneP (VAL (Byte Byte.zero)) sh l') noat)) w *)
(* Goal: @app_pred rmap ag_rmap noghost w *)
    intros [b' i'].
(* Goal: @identity resource Join_resource (resource_at w (@pair block Z b' i')) *)
(* Goal: @identity ghost ghost_join (ghost_of w) *)
    specialize (H (b',i')).
(* Goal: @join resource Join_resource (if @eq_dec AV.address EqDec_address loc (@pair block Z b i) then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) (if adr_range_dec (@pair block Z b (Z.succ i)) (Z.max (Z.of_nat n) Z0) loc then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
    hnf in H.
(* Goal: @identity resource Join_resource (resource_at w (@pair block Z b' i')) *)
(* Goal: @identity ghost ghost_join (ghost_of w) *)
    rewrite if_false in H. apply H.
(* Goal: not (adr_range (@pair block Z b (Z.succ i)) (Z.max (Z.of_nat n) Z0) (@pair block Z b' i')) *)
    clear; intros [? ?]. unfold Z.max in H0; simpl in H0. omega.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    auto.
  * (* inductive case *)
(* Goal: @eq mpred (address_mapsto_zeros sh (S n) (@pair block Z b i)) (address_mapsto_zeros' (Z.of_nat (S n)) sh (@pair block Z b i)) *)
    rewrite inj_S.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
    simpl.
(* Goal: @eq mpred (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b i)) (address_mapsto_zeros sh n (@pair block Z b (Z.succ i)))) (address_mapsto_zeros' (Z.succ (Z.of_nat n)) sh (@pair block Z b i)) *)
    rewrite IHn; clear IHn.
(* Goal: @derives rmap ag_rmap (VALspec sh (@pair block Z b i)) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b i))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b i))))) *)
    apply pred_ext; intros w ?.
    - (* forward case *)
(* Goal: @app_pred rmap ag_rmap (address_mapsto_zeros' (Z.succ (Z.of_nat n)) sh (@pair block Z b i)) w *)
      destruct H as [w1 [w2 [? [? [? Hg2]]]]].
(* Goal: and (@ex memory_chunk (fun ch : memory_chunk => @eq mode (By_value m) (By_value ch))) (isptr (Vptr b i)) *)
      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 (@pair block Z b i) (Z.max (Z.succ (Z.of_nat n)) Z0)) (adr_range_dec (@pair block Z b i) (Z.max (Z.succ (Z.of_nat n)) Z0)) (fun l' : address => yesat NoneP (VAL (Byte Byte.zero)) sh l') noat)) w *)
(* Goal: @app_pred rmap ag_rmap noghost w *)
      intros [b' i'].
(* Goal: is_pointer_or_null (if Archi.ptr64 then Vlong Int64.zero else Vint Int.zero) *)
      hnf.
(* Goal: @eq mpred (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tpointer t noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I32 Unsigned noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) *)
      if_tac.
      + destruct H0 as [bl [[[? [? ?]] ?] _]].
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (Byte Byte.zero)) sh (@pair block Z b' i')) w *)
        specialize (H5 (b',i')).
(* Goal: @app_pred rmap ag_rmap (yesat_raw NoneP (VAL (Byte Byte.zero)) sh p (@pair block Z b' i')) w *)
        hnf in H5.
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (Byte Byte.zero)) sh (@pair block Z b' i')) w *)
        if_tac in H5.
       ** destruct H5 as [p ?]; exists p.
(* Goal: @app_pred rmap ag_rmap (yesat_raw NoneP (VAL (Byte Byte.zero)) sh p (@pair block Z b' i')) w *)
          hnf in H5.
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (Byte Byte.zero)) sh (@pair block Z b' i')) w *)
          specialize (H1 (b',i')). hnf in H1. rewrite if_false in H1.
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (Byte Byte.zero)) sh (@pair block Z b' i')) w *)
          assert (LEV := join_level _ _ _ H).
(* Goal: and (Z.le Z0 ofs') (Z.le (Z.add ofs' (Z.of_nat n')) Ptrofs.modulus) *)
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh n' (@pair block Z b ofs')) (memory_block' sh n' b ofs') *)
          {
(* Goal: @app_pred rmap ag_rmap (noat (@pair block Z b' i')) w *)
            apply (resource_at_join _ _ _ (b',i')) in H.
(* Goal: @app_pred rmap ag_rmap (yesat_raw NoneP (VAL (Byte Byte.zero)) sh p (@pair block Z b' i')) w *)
            apply join_comm in H; apply H1 in H.
(* Goal: @app_pred rmap ag_rmap (yesat_raw NoneP (VAL (Byte Byte.zero)) sh p (@pair block Z b' i')) w *)
            rewrite H in H5.
(* Goal: is_pointer_or_null (if Archi.ptr64 then Vlong Int64.zero else Vint Int.zero) *)
            hnf. rewrite H5. f_equal.
(* Goal: @eq Prop (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) *)
            f_equal.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
            simpl. destruct H6. simpl in H7. replace (i'-i) with 0 by omega.
(* Goal: @eq memval (@nth memval (nat_of_Z Z0) bl Undef) (Byte Byte.zero) *)
            unfold size_chunk_nat in H0. simpl in H0.
(* Goal: @eq memval (@nth memval (nat_of_Z Z0) bl Undef) (Byte Byte.zero) *)
            unfold nat_of_P in H0. simpl in H0.
(* Goal: @eq memval (@nth memval (nat_of_Z Z0) bl Undef) (Byte Byte.zero) *)
            destruct bl; try solve [inv H0].
(* Goal: @eq memval (@nth memval (nat_of_Z Z0) (@cons memval m bl) Undef) (Byte Byte.zero) *)
            destruct bl; inv H0.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
            simpl.
            clear - H3.
            (* TODO: Clean up the following proof. *)
(* Goal: @eq memval m (Byte Byte.zero) *)
            destruct m; try solve [inv H3].
(* Goal: @eq memval (Byte i) (Byte Byte.zero) *)
            rewrite decode_byte_val in H3.
(* Goal: @eq Prop (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) *)
            f_equal.
            assert (Int.zero_ext 8 (Int.repr (Byte.unsigned i)) = Int.repr 0) by
              (forget (Int.zero_ext 8 (Int.repr (Byte.unsigned i))) as j; inv H3; auto).
(* Goal: @eq Byte.int i Byte.zero *)
            clear H3.
            assert (Int.unsigned (Int.zero_ext 8 (Int.repr (Byte.unsigned i))) =
                Int.unsigned Int.zero) by (f_equal; auto).
(* Goal: @eq Byte.int i Byte.zero *)
            rewrite Int.unsigned_zero in H0.
(* Goal: @eq Byte.int i Byte.zero *)
            clear H.
(* Goal: @eq Byte.int i Byte.zero *)
            rewrite Int.zero_ext_mod in H0 by (compute; split; congruence).
(* Goal: @eq Byte.int i Byte.zero *)
            rewrite Int.unsigned_repr in H0.
(* Goal: @eq Byte.int i Byte.zero *)
(* Goal: and (Z.le Z0 (Byte.unsigned i)) (Z.le (Byte.unsigned i) Int.max_unsigned) *)
            rewrite Zdiv.Zmod_small in H0.
(* Goal: @eq Byte.int i Byte.zero *)
(* Goal: and (Z.le Z0 (Byte.unsigned i)) (Z.lt (Byte.unsigned i) (two_p (Zpos (xO (xO (xO xH)))))) *)
(* Goal: and (Z.le Z0 (Byte.unsigned i)) (Z.le (Byte.unsigned i) Int.max_unsigned) *)
            assert (Byte.repr (Byte.unsigned i) = Byte.zero).
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
            apply f_equal; auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
            rewrite Byte.repr_unsigned in H. auto.
(* Goal: and (Z.le Z0 (Byte.unsigned i)) (Z.lt (Byte.unsigned i) (two_p (Zpos (xO (xO (xO xH)))))) *)
(* Goal: and (Z.le Z0 (Byte.unsigned i)) (Z.le (Byte.unsigned i) Int.max_unsigned) *)
            apply Byte.unsigned_range.
(* Goal: @eq (@pred rmap ag_rmap) (VALspec sh (@pair block Z b i)) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b i))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b i))))) *)
            clear.
(* Goal: and (Z.le Z0 (Byte.unsigned i)) (Z.le (Byte.unsigned i) Int.max_unsigned) *)
            pose proof (Byte.unsigned_range i).
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
            destruct H; split; auto.
(* Goal: Z.le (Byte.unsigned i) Int.max_unsigned *)
            apply Z.le_trans with Byte.modulus.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
            omega.
(* Goal: @eq (@pred rmap ag_rmap) (VALspec sh (@pair block Z b i)) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b i))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b i))))) *)
            clear.
(* Goal: Z.le Byte.modulus Int.max_unsigned *)
            compute; congruence.
          }
(* Goal: adr_range (@pair block Z b i) (size_chunk Mint8unsigned) (@pair block Z b' i') *)
          destruct H2.
(* Goal: not (adr_range (@pair block Z b (Z.succ i)) (Z.max (Z.of_nat n) Z0) (@pair block Z b' i')) *)
          intros [? ?].
(* Goal: False *)
          destruct H6.
          clear - H7 H9 H10. simpl in H10. omega.
       ** assert (LEV := join_level _ _ _ H).
(* Goal: @app_pred rmap ag_rmap (noat (@pair block Z b' i')) w *)
          apply (resource_at_join _ _ _ (b',i')) in H.
(* Goal: @app_pred rmap ag_rmap (noat (@pair block Z b' i')) w *)
          apply H5 in H.
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (Byte Byte.zero)) sh (@pair block Z b' i')) w *)
          specialize (H1 (b',i')).
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (Byte Byte.zero)) sh (@pair block Z b' i')) w *)
          hnf in H1.
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (Byte Byte.zero)) sh (@pair block Z b' i')) w *)
          if_tac in H1.
         -- destruct H1 as [p ?]; exists p.
            hnf in H1|-*.
(* Goal: @eq resource (resource_at w (@pair block Z b' i')) (YES sh p (VAL (Byte Byte.zero)) (preds_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) NoneP)) *)
            rewrite H in H1; rewrite H1.
(* Goal: @eq Prop (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) *)
            f_equal.
         -- contradiction H6.
(* Goal: adr_range (@pair block Z b i) (size_chunk Mint8unsigned) (@pair block Z b' i') *)
            destruct H2.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
            split; auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
            simpl.
(* Goal: and (Z.le i i') (Z.lt i' (Z.add i (Zpos xH))) *)
            subst b'.
            clear - H7 H8.
            assert (~ (Z.succ i <= i' < (Z.succ i + Z.max (Z_of_nat n) 0))).
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
            contradict H7; split; auto.
(* Goal: and (Z.le i i') (Z.lt i' (Z.add i (Zpos xH))) *)
            clear H7.
(* Goal: and (Z.le i i') (Z.lt i' (Z.add i (Zpos xH))) *)
            replace (Z.max (Z.succ (Z_of_nat n)) 0) with (Z.succ (Z_of_nat n)) in H8.
(* Goal: and (Z.le i i') (Z.lt i' (Z.add i (Zpos xH))) *)
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.max (Z.succ (Z.of_nat n)) Z0) *)
            replace (Z.max (Z_of_nat n) 0) with (Z_of_nat n) in H.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
            omega.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.max (Z.succ (Z.of_nat n)) Z0) *)
            symmetry; apply Zmax_left.
(* Goal: Z.ge (Z.of_nat n) Z0 *)
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.max (Z.succ (Z.of_nat n)) Z0) *)
            apply Z_of_nat_ge_O.
(* Goal: @eq Z (Z.succ (Z.of_nat n)) (Z.max (Z.succ (Z.of_nat n)) Z0) *)
            symmetry; apply Zmax_left.
(* Goal: @eq (@pred rmap ag_rmap) (VALspec sh (@pair block Z b i)) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b i))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b i))))) *)
            clear.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
            pose proof (Z_of_nat_ge_O n). omega. 
      + apply (resource_at_join _ _ _ (b',i')) in H.
(* Goal: @app_pred rmap ag_rmap (noat (@pair block Z b' i')) w *)
        destruct H0 as [bl [[[? [? ?]] ?] _]].
(* Goal: @app_pred rmap ag_rmap (yesat NoneP (VAL (Byte Byte.zero)) sh (@pair block Z b' i')) w *)
        specialize (H5 (b',i')); specialize (H1 (b',i')).
(* Goal: @app_pred rmap ag_rmap (noat (@pair block Z b' i')) w *)
        hnf in H1,H5.
(* Goal: @app_pred rmap ag_rmap (noat (@pair block Z b' i')) w *)
        rewrite if_false in H5.
(* Goal: @app_pred rmap ag_rmap (noat (@pair block Z b' i')) w *)
(* Goal: not (adr_range (@pair block Z b i) (size_chunk Mint8unsigned) (@pair block Z b' i')) *)
        rewrite if_false in H1.
       ** apply H5 in H.
          simpl in H1|-*.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
          rewrite <- H; auto.
       ** clear - H2; contradict H2.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
          destruct H2; split; auto.
(* Goal: Z.lt (Z.add (Ptrofs.unsigned ofs) n) Ptrofs.modulus *)
          destruct H0.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
          split; try omega.
(* Goal: Z.lt i' (Z.add i (Z.max (Z.succ (Z.of_nat n)) Z0)) *)
          pose proof (Z_of_nat_ge_O n).
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
          rewrite Zmax_left in H1 by omega.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
          rewrite Zmax_left by omega.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
          omega.
       ** clear - H2; contradict H2; simpl in H2.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
          destruct H2; split; auto.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
          rewrite Zmax_left by omega.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
          omega.
      + destruct H0 as (? & ? & Hg1).
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
        simpl; rewrite <- (Hg1 _ _ (ghost_of_join _ _ _ H)); auto.
    - (* backward direction *)
(* Goal: @ex val (fun b0 : val => @app_pred rmap ag_rmap (address_mapsto Mint8unsigned b0 sh (@pair block Z b i)) w) *)
      destruct H as [H Hg].
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b i)) (address_mapsto_zeros' (Z.of_nat n) sh (@pair block Z b (Z.succ i)))) w *)
      assert (H0 := H (b,i)).
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b i)) (address_mapsto_zeros' (Z.of_nat n) sh (@pair block Z b (Z.succ i)))) w *)
      hnf in H0.
      rewrite if_true in H0
        by (split; auto; pose proof (Z_of_nat_ge_O n); rewrite Zmax_left; omega).
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b i)) (address_mapsto_zeros' (Z.of_nat n) sh (@pair block Z b (Z.succ i)))) w *)
      destruct H0 as [H0 H1].
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (Z.le Z0 (Ptrofs.unsigned ofs)) (Z.lt (Z.add n (Ptrofs.unsigned ofs)) Ptrofs.modulus))) (address_mapsto_zeros sh (nat_of_Z n) (@pair block Z b (Ptrofs.unsigned ofs)))) (memory_block sh n (Vptr b ofs)) *)
      pose proof I.
      destruct (make_rmap  (fun loc => if eq_dec loc (b,i) then 
       YES sh H0 (VAL (Byte Byte.zero)) NoneP
          else core (w @ loc)) (ghost_of w) (level w)) as [w1 [? ?]].
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w))) (fun loc : AV.address => if adr_range_dec (@pair block Z b (Z.succ i)) (Z.max (Z.of_nat n) Z0) loc then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc))) (fun loc : AV.address => if adr_range_dec (@pair block Z b (Z.succ i)) (Z.max (Z.of_nat n) Z0) loc then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) *)
(* Goal: @eq ghost (ghost_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (ghost_of w)) (ghost_of w) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b i)) (address_mapsto_zeros' (Z.of_nat n) sh (@pair block Z b (Z.succ i)))) w *)
      extensionality loc. unfold compose.
      if_tac; [unfold resource_fmap; f_equal; apply preds_fmap_NoneP
           | apply resource_fmap_core].
(* Goal: and (Z.le Z0 ofs') (Z.le (Z.add ofs' (Z.of_nat n')) Ptrofs.modulus) *)
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh n' (@pair block Z b ofs')) (memory_block' sh n' b ofs') *)
      { apply ghost_of_approx. }
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (Z.le Z0 (Ptrofs.unsigned ofs)) (Z.lt (Z.add n (Ptrofs.unsigned ofs)) Ptrofs.modulus))) (address_mapsto_zeros sh (nat_of_Z n) (@pair block Z b (Ptrofs.unsigned ofs)))) (memory_block sh n (Vptr b ofs)) *)
      pose proof I.
      destruct (make_rmap (fun loc => if adr_range_dec (b, Z.succ i) (Z.max (Z.of_nat n) 0) loc
                       then YES sh H0 (VAL (Byte Byte.zero)) NoneP
          else core (w @ loc)) (ghost_of w) (level w)) as [w2 [? ?]].
(* Goal: @eq (forall _ : AV.address, resource) (@compose AV.address resource resource (resource_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w))) (fun loc : AV.address => if adr_range_dec (@pair block Z b (Z.succ i)) (Z.max (Z.of_nat n) Z0) loc then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc))) (fun loc : AV.address => if adr_range_dec (@pair block Z b (Z.succ i)) (Z.max (Z.of_nat n) Z0) loc then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) *)
(* Goal: @eq ghost (ghost_fmap (approx (@level rmap ag_rmap w)) (approx (@level rmap ag_rmap w)) (ghost_of w)) (ghost_of w) *)
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b i)) (address_mapsto_zeros' (Z.of_nat n) sh (@pair block Z b (Z.succ i)))) w *)
      extensionality loc. unfold compose.
      if_tac; [unfold resource_fmap; f_equal; apply preds_fmap_NoneP
           | apply resource_fmap_core].
(* Goal: and (Z.le Z0 ofs') (Z.le (Z.add ofs' (Z.of_nat n')) Ptrofs.modulus) *)
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh n' (@pair block Z b ofs')) (memory_block' sh n' b ofs') *)
      { apply ghost_of_approx. }
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      exists w1; exists w2; split3; auto.
+apply resource_at_join2; try congruence.
(* Goal: forall loc : AV.address, @join resource Join_resource (resource_at w1 loc) (resource_at w2 loc) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
  intro loc; destruct H4; rewrite H4; destruct H7; rewrite H7.
 clear - H.
(* Goal: @join resource Join_resource (if @eq_dec AV.address EqDec_address loc (@pair block Z b i) then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) (if adr_range_dec (@pair block Z b (Z.succ i)) (Z.max (Z.of_nat n) Z0) loc then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
 specialize (H loc).  unfold jam in H. hnf in H.
(* Goal: @join resource Join_resource (if @eq_dec AV.address EqDec_address loc (@pair block Z b i) then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) (if adr_range_dec (@pair block Z b (Z.succ i)) (Z.max (Z.of_nat n) Z0) loc then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
 rewrite Zmax_left by (pose proof (Z_of_nat_ge_O n); omega).
(* Goal: @join resource Join_resource (if @eq_dec AV.address EqDec_address loc (@pair block Z b i) then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) (if adr_range_dec (@pair block Z b (Z.succ i)) (Z.of_nat n) loc then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
 rewrite Zmax_left in H by (pose proof (Z_of_nat_ge_O n); omega).
(* Goal: @identity resource Join_resource (if @eq_dec AV.address EqDec_address loc (@pair block Z b i) then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) *)
(* Goal: @app_pred rmap ag_rmap noghost w1 *)
 if_tac. rewrite if_false.
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) n1 (@pair block Z b0 (Ptrofs.unsigned i0)) n2 *)
 subst. rewrite if_true in H.
(* Goal: @join resource Join_resource (YES sh H0 (VAL (Byte Byte.zero)) NoneP) (@core resource Join_resource Sep_resource (resource_at w (@pair block Z b i))) (resource_at w (@pair block Z b i)) *)
(* Goal: adr_range (@pair block Z b i) (Z.succ (Z.of_nat n)) (@pair block Z b i) *)
(* Goal: not (adr_range (@pair block Z b (Z.succ i)) (Z.of_nat n) loc) *)
(* Goal: @join resource Join_resource (@core resource Join_resource Sep_resource (resource_at w loc)) (if adr_range_dec (@pair block Z b (Z.succ i)) (Z.of_nat n) loc then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
  destruct H as [H' H]; rewrite H. rewrite core_YES.
(* Goal: @eq resource (YES sh H0 (VAL (Byte Byte.zero)) NoneP) (YES sh H0 (VAL (Byte Byte.zero)) (preds_fmap (approx (@level rmap ag_rmap w2)) (approx (@level rmap ag_rmap w2)) NoneP)) *)
(* Goal: @app_pred rmap ag_rmap (noat loc) w2 *)
(* Goal: @app_pred rmap ag_rmap noghost w2 *)
 rewrite preds_fmap_NoneP.
(* Goal: @join resource Join_resource (resource_at w loc) (@core resource Join_resource Sep_resource (resource_at w loc)) (resource_at w loc) *)
(* Goal: not (adr_range (@pair block Z b (Z.succ i)) (Z.of_nat n) loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
 apply join_unit2.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
 constructor. auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
 apply YES_ext; auto.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
 split; auto; omega.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
 subst. intros [? ?]; omega.
(* Goal: @join resource Join_resource (@core resource Join_resource Sep_resource (resource_at w loc)) (if adr_range_dec (@pair block Z b (Z.succ i)) (Z.of_nat n) loc then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
 if_tac in H.
(* Goal: @join resource Join_resource (@core resource Join_resource Sep_resource (resource_at w loc)) (if adr_range_dec (@pair block Z b (Z.succ i)) (Z.of_nat n) loc then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) (resource_at w loc) *)
(* Goal: @join resource Join_resource (@core resource Join_resource Sep_resource (resource_at w loc)) (if adr_range_dec (@pair block Z b (Z.succ i)) (Z.of_nat n) loc then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
 rewrite if_true.
(* Goal: @eq Byte.int i Byte.zero *)
 destruct H as [H' H]; rewrite H; clear H. rewrite core_YES.
(* Goal: @eq resource (YES sh H0 (VAL (Byte Byte.zero)) NoneP) (YES sh H0 (VAL (Byte Byte.zero)) (preds_fmap (approx (@level rmap ag_rmap w2)) (approx (@level rmap ag_rmap w2)) NoneP)) *)
(* Goal: @app_pred rmap ag_rmap (noat loc) w2 *)
(* Goal: @app_pred rmap ag_rmap noghost w2 *)
 rewrite preds_fmap_NoneP.
(* Goal: @join resource Join_resource (NO Share.bot bot_unreadable) (YES sh H0 (VAL (Byte Byte.zero)) NoneP) (YES sh H' (VAL (Byte Byte.zero)) NoneP) *)
(* Goal: adr_range (@pair block Z b (Z.succ i)) (Z.of_nat n) loc *)
(* Goal: @join resource Join_resource (@core resource Join_resource Sep_resource (resource_at w loc)) (if adr_range_dec (@pair block Z b (Z.succ i)) (Z.of_nat n) loc then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
 apply join_unit1.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
 constructor; auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
 apply YES_ext; auto.
 destruct loc;
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
 destruct H2; split; auto.
(* Goal: and (Z.le (Z.succ i) z) (Z.lt z (Z.add (Z.succ i) (Z.of_nat n))) *)
(* Goal: @join resource Join_resource (@core resource Join_resource Sep_resource (resource_at w loc)) (if adr_range_dec (@pair block Z b (Z.succ i)) (Z.of_nat n) loc then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) (resource_at w loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
 assert (z<>i) by congruence.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
 omega.
(* Goal: @identity resource Join_resource (if @eq_dec AV.address EqDec_address loc (@pair block Z b i) then YES sh H0 (VAL (Byte Byte.zero)) NoneP else @core resource Join_resource Sep_resource (resource_at w loc)) *)
(* Goal: @app_pred rmap ag_rmap noghost w1 *)
 rewrite if_false.
(* Goal: @join resource Join_resource (@core resource Join_resource Sep_resource (resource_at w loc)) (@core resource Join_resource Sep_resource (resource_at w loc)) (resource_at w loc) *)
(* Goal: not (adr_range (@pair block Z b (Z.succ i)) (Z.of_nat n) loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
 unfold noat in H. simpl in H.
(* Goal: @join resource Join_resource (@core resource Join_resource Sep_resource (resource_at w loc)) (@core resource Join_resource Sep_resource (resource_at w loc)) (resource_at w loc) *)
(* Goal: not (adr_range (@pair block Z b (Z.succ i)) (Z.of_nat n) loc) *)
(* Goal: @join ghost ghost_join (ghost_of w1) (ghost_of w2) (ghost_of w) *)
 apply join_unit1; [apply core_unit | ].
 clear - H.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
 apply H. apply join_unit2. apply core_unit. auto.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
 destruct loc. intros [? ?]; subst. apply H2; split; auto; omega.
 destruct H4 as [_ ->], H7 as [_ ->].
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
 apply identity_unit'; auto.
+ exists (Byte Byte.zero :: nil); split.
(* Goal: and (@ex memory_chunk (fun ch : memory_chunk => @eq mode (By_value m) (By_value ch))) (isptr (Vptr b i)) *)
 split. split. reflexivity. split.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
 unfold decode_val. simpl. f_equal.
(* Goal: Z.divide (align_chunk Mint8unsigned) (@snd block Z (@pair block Z b i)) *)
(* Goal: @app_pred rmap ag_rmap (@allp rmap ag_rmap address (@jam rmap Join_rmap Perm_rmap ag_rmap Age_rmap address (adr_range (@pair block Z b i) (size_chunk Mint8unsigned)) (adr_range_dec (@pair block Z b i) (size_chunk Mint8unsigned)) (fun loc : address => yesat NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z loc) (@snd block Z (@pair block Z b i)))) (@cons memval (Byte Byte.zero) (@nil memval)) Undef)) sh loc) noat)) w1 *)
(* Goal: @app_pred rmap ag_rmap noghost w1 *)
 apply Z.divide_1_l.
(* Goal: is_pointer_or_null (if Archi.ptr64 then Vlong Int64.zero else Vint Int.zero) *)
 intro loc. hnf. if_tac. exists H0.
(* Goal: and (Z.le i i') (Z.lt i' (Z.add i (Zpos xH))) *)
 destruct loc as [b' i']. destruct H8; subst b'.
(* Goal: @app_pred rmap ag_rmap (yesat_raw NoneP (VAL (@nth memval (nat_of_Z (Z.sub (@snd block Z (@pair block Z b i')) (@snd block Z (@pair block Z b i)))) (@cons memval (Byte Byte.zero) (@nil memval)) Undef)) sh H0 (@pair block Z b i')) w1 *)
(* Goal: @app_pred rmap ag_rmap (noat loc) w1 *)
(* Goal: @app_pred rmap ag_rmap noghost w1 *)
 simpl in H9. assert (i=i') by omega; subst i'.
(* Goal: is_pointer_or_null (if Archi.ptr64 then Vlong Int64.zero else Vint Int.zero) *)
 rewrite Zminus_diag. hnf. rewrite preds_fmap_NoneP.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  destruct H4; rewrite H4. rewrite if_true by auto. f_equal.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
 unfold noat. simpl. destruct H4; rewrite H4. rewrite if_false. apply core_identity.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  contradict H8. subst. split; auto. simpl; omega.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  simpl; destruct H4 as [_ ->]; auto.
+ split. intro loc. hnf.
(* Goal: is_pointer_or_null (if Archi.ptr64 then Vlong Int64.zero else Vint Int.zero) *)
 if_tac. exists H0. hnf. destruct H7; rewrite H7.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
 rewrite if_true by auto. rewrite preds_fmap_NoneP. auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
 unfold noat. simpl. destruct H7; rewrite H7.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
 rewrite if_false by auto. apply core_identity.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
 simpl; destruct H7 as [_ ->]; auto.
Qed.

Definition mapsto_zeros (n: Z) (sh: share) (a: val) : mpred :=
 match a with
  | Vptr b z => 
    !! (0 <= Ptrofs.unsigned z  /\ n + Ptrofs.unsigned z < Ptrofs.modulus)%Z &&
    address_mapsto_zeros sh (nat_of_Z n) (b, Ptrofs.unsigned z)
  | _ => FF
  end.

Fixpoint memory_block' (sh: share) (n: nat) (b: block) (i: Z) : mpred :=
  match n with
  | O => emp
  | S n' => mapsto_ sh (Tint I8 Unsigned noattr) (Vptr b (Ptrofs.repr i))
         * memory_block' sh n' b (i+1)
 end.

Definition memory_block'_alt (sh: share) (n: nat) (b: block) (ofs: Z) : mpred :=
 if readable_share_dec sh 
 then VALspec_range (Z_of_nat n) sh (b, ofs)
 else nonlock_permission_bytes sh (b,ofs) (Z.of_nat n).

Lemma memory_block'_eq:
 forall sh n b i,
  0 <= i ->
  Z_of_nat n + i < Ptrofs.modulus ->
  memory_block' sh n b i = memory_block'_alt sh n b i.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: @eq mpred (memory_block'_alt sh (nat_of_Z j) b ofs) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (memory_block'_alt sh (nat_of_Z i) b ofs) (memory_block'_alt sh (nat_of_Z (Z.sub j i)) b (Z.add ofs i))) *)
  unfold memory_block'_alt.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  revert i H H0; induction n; intros.
  + unfold memory_block'.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
    simpl.
(* Goal: @eq mpred (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) (if readable_share_dec sh then VALspec_range Z0 sh (@pair block Z b i) else nonlock_permission_bytes sh (@pair block Z b i) Z0) *)
    rewrite VALspec_range_0, nonlock_permission_bytes_0.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    if_tac; auto.
  + unfold memory_block'; fold memory_block'.
    rewrite (IHn (i+1)) by (rewrite inj_S in H0; omega).
(* Goal: @eq mpred (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (mapsto_ sh (Tint I8 Unsigned noattr) (Vptr b (Ptrofs.repr i))) (if readable_share_dec sh then VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH))) else nonlock_permission_bytes sh (@pair block Z b (Z.add i (Zpos xH))) (Z.of_nat n))) (if readable_share_dec sh then VALspec_range (Z.of_nat (S n)) sh (@pair block Z b i) else nonlock_permission_bytes sh (@pair block Z b i) (Z.of_nat (S n))) *)
    symmetry.
(* Goal: @eq mpred (if readable_share_dec sh then VALspec_range (Z.of_nat (S n)) sh (@pair block Z b i) else nonlock_permission_bytes sh (@pair block Z b i) (Z.of_nat (S n))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (mapsto_ sh (Tint I8 Unsigned noattr) (Vptr b (Ptrofs.repr i))) (if readable_share_dec sh then VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH))) else nonlock_permission_bytes sh (@pair block Z b (Z.add i (Zpos xH))) (Z.of_nat n))) *)
    rewrite (VALspec_range_split2 1 (Z_of_nat n)) by (try rewrite inj_S; omega).
(* Goal: @eq mpred (if readable_share_dec sh then @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec_range (Zpos xH) sh (@pair block Z b i)) (VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH)))) else nonlock_permission_bytes sh (@pair block Z b i) (Z.of_nat (S n))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (mapsto_ sh (Tint I8 Unsigned noattr) (Vptr b (Ptrofs.repr i))) (if readable_share_dec sh then VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH))) else nonlock_permission_bytes sh (@pair block Z b (Z.add i (Zpos xH))) (Z.of_nat n))) *)
    rewrite VALspec1.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (mapsto_ sh (Tint I8 Unsigned noattr) (Vptr b (Ptrofs.repr ofs'))) *)
    unfold mapsto_, mapsto.
(* Goal: @eq mpred (if readable_share_dec sh then @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec sh (@pair block Z b i)) (VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH)))) else nonlock_permission_bytes sh (@pair block Z b i) (Z.of_nat (S n))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i)))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr i))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end (if readable_share_dec sh then VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH))) else nonlock_permission_bytes sh (@pair block Z b (Z.add i (Zpos xH))) (Z.of_nat n))) *)
    simpl access_mode. cbv beta iota.
(* Goal: @eq mpred (if readable_share_dec sh then @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec sh (@pair block Z b i)) (VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH)))) else nonlock_permission_bytes sh (@pair block Z b i) (Z.of_nat (S n))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (if false then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i)))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk Mint8unsigned) (Ptrofs.unsigned (Ptrofs.repr i))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))) (size_chunk Mint8unsigned))) (if readable_share_dec sh then VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH))) else nonlock_permission_bytes sh (@pair block Z b (Z.add i (Zpos xH))) (Z.of_nat n))) *)
    change (type_is_volatile (Tint I8 Unsigned noattr)) with false. cbv beta iota.
(* Goal: @eq mpred (if readable_share_dec sh then @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec sh (@pair block Z b i)) (VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH)))) else nonlock_permission_bytes sh (@pair block Z b i) (Z.of_nat (S n))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i)))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk Mint8unsigned) (Ptrofs.unsigned (Ptrofs.repr i))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))) (size_chunk Mint8unsigned))) (if readable_share_dec sh then VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH))) else nonlock_permission_bytes sh (@pair block Z b (Z.add i (Zpos xH))) (Z.of_nat n))) *)
    destruct (readable_share_dec sh).
    - f_equal.
(* Goal: @eq (@pred rmap ag_rmap) (VALspec sh (@pair block Z b i)) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))))))) *)
      assert (i < Ptrofs.modulus) by (rewrite Nat2Z.inj_succ in H0; omega).
(* Goal: @eq (@pred rmap ag_rmap) (VALspec sh (@pair block Z b i)) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))))))) *)
      rewrite Ptrofs.unsigned_repr by (unfold Ptrofs.max_unsigned; omega); clear H1.
(* Goal: @eq (@pred rmap ag_rmap) (VALspec sh (@pair block Z b i)) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b i))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b i))))) *)
      forget (Share.unrel Share.Lsh sh) as rsh.
(* Goal: @eq (@pred rmap ag_rmap) (VALspec sh (@pair block Z b i)) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b i))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b i))))) *)
      forget (Share.unrel Share.Rsh sh) as sh'.
(* Goal: @eq (@pred rmap ag_rmap) (VALspec sh (@pair block Z b i)) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b i))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b i))))) *)
      clear.

(* Goal: @eq (@pred rmap ag_rmap) (VALspec sh (@pair block Z b i)) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b i))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b i))))) *)
      assert (EQ: forall loc, jam (adr_range_dec loc (size_chunk Mint8unsigned)) = jam (eq_dec loc)).
      intros [b' z']; unfold jam; extensionality P Q loc;
       destruct loc as [b'' z'']; apply exist_ext; extensionality w;
       if_tac; [rewrite if_true | rewrite if_false]; auto;
        [destruct H; subst; f_equal;  simpl in H0; omega
        | contradict H; inv H; split; simpl; auto; omega].
(* Goal: @eq (@pred rmap ag_rmap) (VALspec_range (size_chunk ch) sh l) (@exp rmap ag_rmap val (fun v : val => address_mapsto ch v sh l)) *)
      apply pred_ext.
      * intros w ?.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
        right; split; hnf; auto.
(* Goal: @ex val (fun b0 : val => @app_pred rmap ag_rmap (address_mapsto Mint8unsigned b0 sh (@pair block Z b i)) w) *)
        destruct H as [H Hg].
(* Goal: @ex val (fun b0 : val => @app_pred rmap ag_rmap (address_mapsto Mint8unsigned b0 sh (@pair block Z b i)) w) *)
        assert (H':= H (b,i)).
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
        hnf in H'. rewrite if_true in H' by auto.
(* Goal: @ex val (fun b0 : val => @app_pred rmap ag_rmap (address_mapsto Mint8unsigned b0 sh (@pair block Z b i)) w) *)
        destruct H' as [v H'].
(* Goal: @ex val (fun b0 : val => @app_pred rmap ag_rmap (address_mapsto Mint8unsigned b0 sh (@pair block Z b i)) w) *)
        pose (l := v::nil).
        destruct v; [exists Vundef | exists (Vint (Int.zero_ext 8 (Int.repr (Byte.unsigned i0)))) | exists Vundef];
        exists l; split; auto; (split; [ split3; [reflexivity |unfold l; (reflexivity || apply decode_byte_val) |  apply Z.divide_1_l ] | ]);
          rewrite EQ; intro loc; specialize (H loc);
         hnf in H|-*; if_tac; auto; subst loc; rewrite Zminus_diag;
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
         unfold l; simpl nth; auto.
      * apply orp_left.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
        apply andp_left2.
(* Goal: and (Z.le Z0 ofs') (Z.le (Z.add ofs' (Z.of_nat n')) Ptrofs.modulus) *)
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh n' (@pair block Z b ofs')) (memory_block' sh n' b ofs') *)
        { intros w [l [[[? [? ?]] ?] Hg]].
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
          split; auto.
          intros [b' i']; specialize (H2 (b',i')); rewrite EQ in H2;
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
            hnf in H2|-*;  if_tac; auto. symmetry in H3; inv H3.
(* Goal: @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh (@pair block Z b i))) w *)
          destruct l; inv H. exists m.
          destruct H2 as [H2' H2]; exists H2'; hnf in H2|-*; rewrite H2.
(* Goal: @eq Prop (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) *)
          f_equal. f_equal. rewrite Zminus_diag. reflexivity.
        }
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
        { rewrite prop_true_andp by auto.
(* Goal: @derives rmap ag_rmap (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b i))) (VALspec sh (@pair block Z b i)) *)
          intros w [v2' [l [[[? [? ?]] ?] Hg]]].
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
          split; auto.
          intros [b' i']; specialize (H2 (b',i')); rewrite EQ in H2;
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
            hnf in H2|-*;  if_tac; auto. symmetry in H3; inv H3.
(* Goal: @app_pred rmap ag_rmap (@exp rmap ag_rmap memval (fun v : memval => yesat NoneP (VAL v) sh (@pair block Z b i))) w *)
          destruct l; inv H. exists m.
          destruct H2 as [H2' H2]; exists H2'; hnf in H2|-*; rewrite H2.
(* Goal: @eq Prop (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) *)
          f_equal. f_equal. rewrite Zminus_diag. reflexivity.
        }
    - rewrite Ptrofs.unsigned_repr by (rewrite Nat2Z.inj_succ in H0; unfold Ptrofs.max_unsigned; omega).
(* Goal: @eq mpred (nonlock_permission_bytes sh (@pair block Z b i) (Z.of_nat (S n))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk Mint8unsigned) i))) (nonlock_permission_bytes sh (@pair block Z b i) (size_chunk Mint8unsigned))) (nonlock_permission_bytes sh (@pair block Z b (Z.add i (Zpos xH))) (Z.of_nat n))) *)
      change (size_chunk Mint8unsigned) with 1.
(* Goal: @eq mpred (nonlock_permission_bytes sh (@pair block Z b i) (Z.of_nat (S n))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk Mint8unsigned) i))) (nonlock_permission_bytes sh (@pair block Z b i) (Zpos xH))) (nonlock_permission_bytes sh (@pair block Z b (Z.add i (Zpos xH))) (Z.of_nat n))) *)
      rewrite prop_true_andp by (split; [apply tc_val'_Vundef | apply Z.divide_1_l]).
(* Goal: @eq mpred (nonlock_permission_bytes sh (@pair block Z b i) (Z.of_nat (S n))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (nonlock_permission_bytes sh (@pair block Z b i) (Zpos xH)) (nonlock_permission_bytes sh (@pair block Z b (Z.add i (Zpos xH))) (Z.of_nat n))) *)
      apply nonlock_permission_bytes_split2.
      * rewrite Nat2Z.inj_succ; omega.
      * omega.
      * omega.
Qed.

Definition memory_block (sh: share) (n: Z) (v: val) : mpred :=
 match v with
 | Vptr b ofs => (!!(Ptrofs.unsigned ofs + n < Ptrofs.modulus)) && memory_block' sh (nat_of_Z n) b (Ptrofs.unsigned ofs)
 | _ => FF
 end.

Lemma mapsto__exp_address_mapsto: forall sh t b i_ofs ch,
  access_mode t = By_value ch ->
  type_is_volatile t = false ->
  readable_share sh ->
  mapsto_ sh t (Vptr b i_ofs) = EX  v2' : val,
            address_mapsto ch v2' sh (b, (Ptrofs.unsigned i_ofs)).
Proof.
(* Goal: forall (sh : share) (t : type) (b : block) (i_ofs : Ptrofs.int) (ch : memory_chunk) (_ : @eq mode (access_mode t) (By_value ch)) (_ : @eq bool (type_is_volatile t) false) (_ : readable_share sh), @eq mpred (mapsto_ sh t (Vptr b i_ofs)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned i_ofs)))) *)
  pose proof (@FF_orp (pred rmap) (algNatDed _)) as HH0.
(* Goal: forall (sh : share) (t : type) (b : block) (i_ofs : Ptrofs.int) (ch : memory_chunk) (_ : @eq mode (access_mode t) (By_value ch)) (_ : @eq bool (type_is_volatile t) false) (_ : readable_share sh), @eq mpred (mapsto_ sh t (Vptr b i_ofs)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned i_ofs)))) *)
  change seplog.orp with orp in HH0.
(* Goal: forall (sh : share) (t : type) (b : block) (i_ofs : Ptrofs.int) (ch : memory_chunk) (_ : @eq mode (access_mode t) (By_value ch)) (_ : @eq bool (type_is_volatile t) false) (_ : readable_share sh), @eq mpred (mapsto_ sh t (Vptr b i_ofs)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned i_ofs)))) *)
  change seplog.FF with FF in HH0.
(* Goal: forall (sh : share) (t : type) (b : block) (i_ofs : Ptrofs.int) (ch : memory_chunk) (_ : @eq mode (access_mode t) (By_value ch)) (_ : @eq bool (type_is_volatile t) false) (_ : readable_share sh), @eq mpred (mapsto_ sh t (Vptr b i_ofs)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned i_ofs)))) *)
  pose proof (@ND_prop_ext (pred rmap) (algNatDed _)) as HH1.
(* Goal: forall (sh : share) (t : type) (b : block) (i_ofs : Ptrofs.int) (ch : memory_chunk) (_ : @eq mode (access_mode t) (By_value ch)) (_ : @eq bool (type_is_volatile t) false) (_ : readable_share sh), @eq mpred (mapsto_ sh t (Vptr b i_ofs)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned i_ofs)))) *)
  change seplog.prop with prop in HH1.

(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros. rename H1 into RS.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (mapsto_ sh (Tint I8 Unsigned noattr) (Vptr b (Ptrofs.repr ofs'))) *)
  unfold mapsto_, mapsto.
(* Goal: @eq mpred match access_mode (Tpointer t a) with | By_value ch => if type_is_volatile (Tpointer t a) then @FF rmap ag_rmap else match v1 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap ((if eqb_type (Tpointer t a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) v2)) (address_mapsto ch v2 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v2 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (forall _ : not (@eq val v2 Vundef), (if eqb_type (Tpointer t a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) v2) (Z.divide (align_chunk ch) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk ch)) end | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end match access_mode (Tpointer Tvoid a) with | By_value ch => if type_is_volatile (Tpointer Tvoid a) then @FF rmap ag_rmap else match v1 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap ((if eqb_type (Tpointer Tvoid a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) v2)) (address_mapsto ch v2 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v2 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (forall _ : not (@eq val v2 Vundef), (if eqb_type (Tpointer Tvoid a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) v2) (Z.divide (align_chunk ch) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk ch)) end | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
  rewrite H, H0.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  rewrite if_true by auto.
(* Goal: and (Z.le Z0 ofs') (Z.le (Z.add ofs' (Z.of_nat n')) Ptrofs.modulus) *)
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh n' (@pair block Z b ofs')) (memory_block' sh n' b ofs') *)
  assert (!!(tc_val t Vundef) = FF). {
(* Goal: @eq (@pred rmap ag_rmap) (@prop rmap ag_rmap (tc_val t Vundef)) (@FF rmap ag_rmap) *)
    clear; unfold FF; f_equal; apply prop_ext; intuition.
(* Goal: False *)
    apply (tc_val_Vundef _ H).
  }
(* Goal: @eq mpred (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned i_ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned i_ofs)))))) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned i_ofs)))) *)
  rewrite H1.

(* Goal: @eq mpred (@orp rmap ag_rmap (@andp rmap ag_rmap (@FF rmap ag_rmap) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned i_ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned i_ofs)))))) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned i_ofs)))) *)
  rewrite FF_and, HH0.
(* Goal: @eq mpred (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned i_ofs))))) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned i_ofs)))) *)
  assert (!!(Vundef = Vundef) = TT) by (apply HH1; tauto).
(* Goal: @eq mpred (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned i_ofs))))) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned i_ofs)))) *)
  rewrite H2.
(* Goal: @eq mpred (@andp rmap ag_rmap (@TT rmap ag_rmap) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned i_ofs))))) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned i_ofs)))) *)
  rewrite TT_and.
(* Goal: @eq mpred (mapsto sh (Tint I32 Unsigned noattr) v1 v2) (mapsto sh (Tint I32 Signed noattr) v1 v2) *)
  reflexivity.
Qed.

Lemma exp_address_mapsto_VALspec_range_eq:
  forall ch sh l,
    EX v: val, address_mapsto ch v sh l = !! (align_chunk ch | snd l) && VALspec_range (size_chunk ch) sh l.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (VALspec_range (size_chunk ch) sh l) (@exp rmap ag_rmap val (fun v : val => address_mapsto ch v sh l)) *)
  apply pred_ext.
  + apply exp_left; intro.
(* Goal: @derives rmap ag_rmap (address_mapsto ch x sh l) (@andp rmap ag_rmap (@prop rmap ag_rmap (Z.divide (align_chunk ch) (@snd block Z l))) (VALspec_range (size_chunk ch) sh l)) *)
    apply andp_right; [| apply address_mapsto_VALspec_range].
(* Goal: @derives rmap ag_rmap (address_mapsto ch x sh l) (@prop rmap ag_rmap (Z.divide (align_chunk ch) (@snd block Z l))) *)
    unfold address_mapsto.
(* Goal: @derives rmap ag_rmap (@exp rmap ag_rmap val (fun x : val => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto m v0 sh1 (@pair block Z b (Ptrofs.unsigned i))) (address_mapsto m x sh2 (@pair block Z b (Ptrofs.unsigned i))))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto m v0 sh1 (@pair block Z b (Ptrofs.unsigned i))) (address_mapsto m v0 sh2 (@pair block Z b (Ptrofs.unsigned i)))) *)
    apply exp_left; intro.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) (@prop rmap ag_rmap (tc_val' t v)) *)
    do 2 apply andp_left1.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    apply (@prop_derives (pred rmap) (algNatDed _)); tauto.
  + apply prop_andp_left; intro.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    apply VALspec_range_exp_address_mapsto; auto.
Qed.

Lemma VALspec_range_exp_address_mapsto_eq:
  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 (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: @eq (@pred rmap ag_rmap) (VALspec_range (size_chunk ch) sh l) (@exp rmap ag_rmap val (fun v : val => address_mapsto ch v sh l)) *)
  apply pred_ext.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  + apply VALspec_range_exp_address_mapsto; auto.
  + apply exp_left; intro; apply address_mapsto_VALspec_range.
Qed.

Lemma mapsto__memory_block: forall sh b ofs t ch,
  access_mode t = By_value ch ->
  type_is_volatile t = false ->
  (align_chunk ch | Ptrofs.unsigned ofs) ->
  Ptrofs.unsigned ofs + size_chunk ch < Ptrofs.modulus ->
  mapsto_ sh t (Vptr b ofs) = memory_block sh (size_chunk ch) (Vptr b ofs).
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (Z.le Z0 (Ptrofs.unsigned ofs)) (Z.lt (Z.add n (Ptrofs.unsigned ofs)) Ptrofs.modulus))) (address_mapsto_zeros sh (nat_of_Z n) (@pair block Z b (Ptrofs.unsigned ofs)))) (memory_block sh n (Vptr b ofs)) *)
  unfold memory_block.
  rewrite memory_block'_eq.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
  2: pose proof Ptrofs.unsigned_range ofs; omega.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
  2: rewrite Coqlib.nat_of_Z_eq by (pose proof size_chunk_pos ch; omega); omega.
(* Goal: @eq mpred (if readable_share_dec sh then @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec sh (@pair block Z b i)) (VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH)))) else nonlock_permission_bytes sh (@pair block Z b i) (Z.of_nat (S n))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i)))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk Mint8unsigned) (Ptrofs.unsigned (Ptrofs.repr i))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))) (size_chunk Mint8unsigned))) (if readable_share_dec sh then VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH))) else nonlock_permission_bytes sh (@pair block Z b (Z.add i (Zpos xH))) (Z.of_nat n))) *)
  destruct (readable_share_dec sh).
 *
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  rewrite mapsto__exp_address_mapsto with (ch := ch); auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  unfold memory_block'_alt. rewrite if_true by auto.
  rewrite Coqlib.nat_of_Z_eq by (pose proof size_chunk_pos ch; omega).
  rewrite VALspec_range_exp_address_mapsto_eq by (exact H1).
  rewrite <- (TT_and (EX  v2' : val,
   address_mapsto ch v2' sh (b, Ptrofs.unsigned ofs))) at 1.
(* Goal: @eq Prop (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) *)
  f_equal.
  pose proof (@ND_prop_ext (pred rmap) _).
  simpl in H3.
  change TT with (!! True).
  apply H3.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  tauto.
 * unfold mapsto_, mapsto, memory_block'_alt.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
   rewrite prop_true_andp by auto.
(* Goal: @eq mpred match access_mode (Tpointer t a) with | By_value ch => if type_is_volatile (Tpointer t a) then @FF rmap ag_rmap else match v1 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap ((if eqb_type (Tpointer t a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) v2)) (address_mapsto ch v2 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v2 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (forall _ : not (@eq val v2 Vundef), (if eqb_type (Tpointer t a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) v2) (Z.divide (align_chunk ch) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk ch)) end | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end match access_mode (Tpointer Tvoid a) with | By_value ch => if type_is_volatile (Tpointer Tvoid a) then @FF rmap ag_rmap else match v1 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap ((if eqb_type (Tpointer Tvoid a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) v2)) (address_mapsto ch v2 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v2 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (forall _ : not (@eq val v2 Vundef), (if eqb_type (Tpointer Tvoid a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) v2) (Z.divide (align_chunk ch) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk ch)) end | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
   rewrite H, H0.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  rewrite !if_false by auto.
   rewrite prop_true_andp by (split; [apply tc_val'_Vundef | auto]).
   rewrite Z2Nat.id by (pose proof (size_chunk_pos ch); omega).
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
   auto.
Qed.

Lemma nonreadable_memory_block_mapsto: forall sh b ofs t ch v,
  ~ readable_share sh ->
  access_mode t = By_value ch ->
  type_is_volatile t = false ->
  (align_chunk ch | Ptrofs.unsigned ofs) ->
  Ptrofs.unsigned ofs + size_chunk ch < Ptrofs.modulus ->
  tc_val' t v ->
  memory_block sh (size_chunk ch) (Vptr b ofs) = mapsto sh t (Vptr b ofs) v.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (Z.le Z0 (Ptrofs.unsigned ofs)) (Z.lt (Z.add n (Ptrofs.unsigned ofs)) Ptrofs.modulus))) (address_mapsto_zeros sh (nat_of_Z n) (@pair block Z b (Ptrofs.unsigned ofs)))) (memory_block sh n (Vptr b ofs)) *)
  unfold memory_block.
  rewrite memory_block'_eq.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
  2: pose proof Ptrofs.unsigned_range ofs; omega.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
  2: rewrite Coqlib.nat_of_Z_eq by (pose proof size_chunk_pos ch; omega); omega.
(* Goal: @eq mpred (if readable_share_dec sh then @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec sh (@pair block Z b i)) (VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH)))) else nonlock_permission_bytes sh (@pair block Z b i) (Z.of_nat (S n))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i)))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk Mint8unsigned) (Ptrofs.unsigned (Ptrofs.repr i))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))) (size_chunk Mint8unsigned))) (if readable_share_dec sh then VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH))) else nonlock_permission_bytes sh (@pair block Z b (Z.add i (Zpos xH))) (Z.of_nat n))) *)
  destruct (readable_share_dec sh).
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
 * tauto.
 * unfold mapsto_, mapsto, memory_block'_alt.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
   rewrite prop_true_andp by auto.
   rewrite H0, H1.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
   rewrite !if_false by auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
   rewrite prop_true_andp by auto.
   rewrite Z2Nat.id by (pose proof (size_chunk_pos ch); omega).
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
   auto.
Qed.

Lemma mapsto_share_join:
 forall sh1 sh2 sh t p v,
   join sh1 sh2 sh ->
   mapsto sh1 t p v * mapsto sh2 t p v = mapsto sh t p v.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: @eq (forall (_ : val) (_ : val), mpred) (mapsto sh (Tpointer t a)) (mapsto sh (Tpointer Tvoid a)) *)
  unfold mapsto.
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap match access_mode t with | By_value ch => if type_is_volatile t then @FF rmap ag_rmap else match p with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh1 then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto ch v sh1 (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh1 (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk ch) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh1 (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk ch)) end | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end match access_mode t with | By_value ch => if type_is_volatile t then @FF rmap ag_rmap else match p with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh2 then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto ch v sh2 (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh2 (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk ch) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh2 (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk ch)) end | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end) match access_mode t with | By_value ch => if type_is_volatile t then @FF rmap ag_rmap else match p with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto ch v sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk ch) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk ch)) end | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
  destruct (access_mode t) eqn:?; try solve [rewrite FF_sepcon; auto].
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (if type_is_volatile t then @FF rmap ag_rmap else match p with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh1 then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh1 (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh1 (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh1 (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk m)) end) (if type_is_volatile t then @FF rmap ag_rmap else match p with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh2 then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh2 (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh2 (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh2 (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk m)) end)) (if type_is_volatile t then @FF rmap ag_rmap else match p with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk m)) end) *)
  destruct (type_is_volatile t) eqn:?; try solve [rewrite FF_sepcon; auto].
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap match p with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => @andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned ofs) n) Ptrofs.modulus)) (memory_block' sh (nat_of_Z n) b (Ptrofs.unsigned ofs)) end match p with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => @andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned ofs) m) Ptrofs.modulus)) (memory_block' sh (nat_of_Z m) b (Ptrofs.unsigned ofs)) end) (@FF rmap ag_rmap) *)
  destruct p; try solve [rewrite FF_sepcon; auto].
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (if readable_share_dec sh1 then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh1 (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh1 (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh1 (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) (if readable_share_dec sh2 then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh2 (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh2 (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh2 (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m)))) (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) *)
  destruct (readable_share_dec sh1), (readable_share_dec sh2).
  + rewrite if_true by (eapply join_sub_readable; [unfold join_sub; eauto | auto]).
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh1 (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh1 (@pair block Z b (Ptrofs.unsigned i)))))) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh2 (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh2 (@pair block Z b (Ptrofs.unsigned i))))))) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned i)))))) *)
    pose proof (@guarded_sepcon_orp_distr (pred rmap) (algNatDed _) (algSepLog _)).
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh1 (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh1 (@pair block Z b (Ptrofs.unsigned i)))))) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh2 (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh2 (@pair block Z b (Ptrofs.unsigned i))))))) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned i)))))) *)
    simpl in H0; rewrite H0 by (intros; subst; pose proof tc_val_Vundef t; tauto); clear H0.
(* Goal: @eq Prop (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) *)
    f_equal; f_equal.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    - apply address_mapsto_share_join; auto.
    - rewrite exp_sepcon1.
(* Goal: @eq (@pred rmap ag_rmap) (@exp rmap ag_rmap val (fun x : val => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto m x sh1 (@pair block Z b (Ptrofs.unsigned i))) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh2 (@pair block Z b (Ptrofs.unsigned i)))))) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned i)))) *)
      pose proof (@exp_congr (pred rmap) (algNatDed _) val); simpl in H0; apply H0; clear H0; intro.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto m v1 sh (@pair block Z b (Ptrofs.unsigned i))) (@exp rmap ag_rmap val (fun v : val => address_mapsto m0 v sh (@pair block Z b0 (Ptrofs.unsigned i0))))) (@FF rmap ag_rmap) *)
      rewrite exp_sepcon2.
      transitivity
       (address_mapsto m v0 sh1 (b, Ptrofs.unsigned i) *
        address_mapsto m v0 sh2 (b, Ptrofs.unsigned i)).
      * apply pred_ext; [| apply (exp_right v0); auto].
(* Goal: @derives rmap ag_rmap (@exp rmap ag_rmap val (fun x : val => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto m v0 sh1 (@pair block Z b (Ptrofs.unsigned i))) (address_mapsto m x sh2 (@pair block Z b (Ptrofs.unsigned i))))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto m v0 sh1 (@pair block Z b (Ptrofs.unsigned i))) (address_mapsto m v0 sh2 (@pair block Z b (Ptrofs.unsigned i)))) *)
        apply exp_left; intro.
        pose proof (fun sh0 sh3 a => 
            (@add_andp (pred rmap) (algNatDed _) _ _ (address_mapsto_value_cohere m v0 x sh0 sh3 a))).
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto m v0 sh1 (@pair block Z b (Ptrofs.unsigned i))) (address_mapsto m x sh2 (@pair block Z b (Ptrofs.unsigned i)))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto m v0 sh1 (@pair block Z b (Ptrofs.unsigned i))) (address_mapsto m v0 sh2 (@pair block Z b (Ptrofs.unsigned i)))) *)
        simpl in H0; rewrite H0; clear H0.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
        apply normalize.derives_extract_prop'; intro; subst; auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      * apply address_mapsto_share_join; auto.
  + rewrite if_true by (eapply join_sub_readable; [unfold join_sub; eauto | auto]).
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh1 (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh1 (@pair block Z b (Ptrofs.unsigned i)))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh2 (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m)))) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned i)))))) *)
    rewrite distrib_orp_sepcon.
    f_equal; rewrite sepcon_comm, sepcon_andp_prop;
    pose proof (@andp_prop_ext (pred rmap) _);
    (simpl in H0; apply H0; clear H0; [reflexivity | intro]).
    - rewrite (address_mapsto_align _ _ sh).
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh1 (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) (address_mapsto m v0 sh2 (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (address_mapsto m v0 sh (@pair block Z b (Ptrofs.unsigned i))) (@prop rmap ag_rmap (Z.divide (align_chunk m) (@snd block Z (@pair block Z b (Ptrofs.unsigned i)))))) *)
      rewrite (andp_comm (address_mapsto _ _ _ _)), sepcon_andp_prop1.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
      pose proof (@andp_prop_ext (pred rmap) _); simpl in H1; apply H1; clear H1; intros.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      * apply tc_val_tc_val' in H0; tauto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      * apply nonlock_permission_bytes_address_mapsto_join; auto.
    - rewrite exp_sepcon2.
(* Goal: @eq (@pred rmap ag_rmap) (@exp rmap ag_rmap val (fun x : val => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh1 (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) (address_mapsto m x sh2 (@pair block Z b (Ptrofs.unsigned i))))) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned i)))) *)
      pose proof (@exp_congr (pred rmap) (algNatDed _) val); simpl in H1; apply H1; clear H1; intro.
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh1 (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) (address_mapsto m v0 sh2 (@pair block Z b (Ptrofs.unsigned i)))) (address_mapsto m v0 sh (@pair block Z b (Ptrofs.unsigned i))) *)
      rewrite (address_mapsto_align _ _ sh).
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh1 (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) (address_mapsto m v0 sh2 (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (address_mapsto m v0 sh (@pair block Z b (Ptrofs.unsigned i))) (@prop rmap ag_rmap (Z.divide (align_chunk m) (@snd block Z (@pair block Z b (Ptrofs.unsigned i)))))) *)
      rewrite (andp_comm (address_mapsto _ _ _ _)), sepcon_andp_prop1.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
      pose proof (@andp_prop_ext (pred rmap) _); simpl in H1; apply H1; clear H1; intros.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      * subst; pose proof tc_val'_Vundef t. tauto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      * apply nonlock_permission_bytes_address_mapsto_join; auto.
  + rewrite if_true by (eapply join_sub_readable; [unfold join_sub; eexists; apply join_comm in H; eauto | auto]).
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh1 (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh2 (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh2 (@pair block Z b (Ptrofs.unsigned i))))))) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned i)))))) *)
    rewrite sepcon_comm, distrib_orp_sepcon.
    f_equal; rewrite sepcon_comm, sepcon_andp_prop;
    pose proof (@andp_prop_ext (pred rmap) _);
    (simpl in H0; apply H0; clear H0; [reflexivity | intro]).
    - rewrite (address_mapsto_align _ _ sh).
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh1 (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) (address_mapsto m v0 sh2 (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (address_mapsto m v0 sh (@pair block Z b (Ptrofs.unsigned i))) (@prop rmap ag_rmap (Z.divide (align_chunk m) (@snd block Z (@pair block Z b (Ptrofs.unsigned i)))))) *)
      rewrite (andp_comm (address_mapsto _ _ _ _)), sepcon_andp_prop1.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
      pose proof (@andp_prop_ext (pred rmap) _); simpl in H1; apply H1; clear H1; intros.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      * apply tc_val_tc_val' in H0; tauto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      * apply nonlock_permission_bytes_address_mapsto_join; auto.
    - rewrite exp_sepcon2.
(* Goal: @eq (@pred rmap ag_rmap) (@exp rmap ag_rmap val (fun x : val => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh1 (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) (address_mapsto m x sh2 (@pair block Z b (Ptrofs.unsigned i))))) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned i)))) *)
      pose proof (@exp_congr (pred rmap) (algNatDed _) val); simpl in H1; apply H1; clear H1; intro.
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh1 (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) (address_mapsto m v0 sh2 (@pair block Z b (Ptrofs.unsigned i)))) (address_mapsto m v0 sh (@pair block Z b (Ptrofs.unsigned i))) *)
      rewrite (address_mapsto_align _ _ sh).
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh1 (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) (address_mapsto m v0 sh2 (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (address_mapsto m v0 sh (@pair block Z b (Ptrofs.unsigned i))) (@prop rmap ag_rmap (Z.divide (align_chunk m) (@snd block Z (@pair block Z b (Ptrofs.unsigned i)))))) *)
      rewrite (andp_comm (address_mapsto _ _ _ _)), sepcon_andp_prop1.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
      pose proof (@andp_prop_ext (pred rmap) _); simpl in H1; apply H1; clear H1; intros.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      * subst; pose proof tc_val'_Vundef t. tauto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      * apply nonlock_permission_bytes_address_mapsto_join; auto.
  + rewrite if_false by (eapply join_unreadable_shares; eauto).
    rewrite sepcon_andp_prop1, sepcon_andp_prop2, <- andp_assoc, andp_dup.
(* Goal: @eq Prop (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) *)
    f_equal.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    apply nonlock_permission_bytes_share_join; auto.
Qed.

Lemma mapsto_mapsto_: forall sh t v v', mapsto sh t v v' |-- mapsto_ sh t v.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
Proof. unfold mapsto_; intros.
(* Goal: @eq (forall (_ : val) (_ : val), mpred) (mapsto sh (Tpointer t a)) (mapsto sh (Tpointer Tvoid a)) *)
  unfold mapsto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  destruct (access_mode t); auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  destruct (type_is_volatile t); auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  destruct v; auto.
(* Goal: @eq mpred (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tpointer t noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I32 Unsigned noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) *)
  if_tac.
  + apply orp_left.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap False) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))))) *)
    apply orp_right2.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
    apply andp_left2.
(* Goal: @derives rmap ag_rmap (address_mapsto m v' sh (@pair block Z b (Ptrofs.unsigned i))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned i))))) *)
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v' Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned i))))) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t Vundef)) (address_mapsto m Vundef sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned i)))))) *)
    apply andp_right.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    - intros ? _; simpl; auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    - apply exp_right with v'; auto.
    - apply andp_left2. apply exp_left; intro v2'.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap False) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))))) *)
      apply orp_right2. apply andp_right; [intros ? _; simpl; auto |]. apply exp_right with v2'.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      auto.
  + apply andp_derives; [| auto].
(* Goal: @derives rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v') (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (@prop rmap ag_rmap (and (tc_val' t Vundef) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) *)
    intros ? [? ?].
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    split; auto.
(* Goal: tc_val' t Vundef *)
    apply tc_val'_Vundef.
Qed.

Lemma mapsto_not_nonunit: forall sh t p v, ~ nonunit sh -> mapsto sh t p v |-- emp.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: @eq (forall (_ : val) (_ : val), mpred) (mapsto sh (Tpointer t a)) (mapsto sh (Tpointer Tvoid a)) *)
  unfold mapsto.
(* Goal: @derives rmap ag_rmap match access_mode t with | By_value ch => if type_is_volatile t then @FF rmap ag_rmap else match p with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto ch v sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk ch) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk ch)) end | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end (@prop rmap ag_rmap (and (@ex memory_chunk (fun ch : memory_chunk => @eq mode (access_mode t) (By_value ch))) (isptr p))) *)
  destruct (access_mode t); try solve [apply FF_derives].
(* Goal: @derives rmap ag_rmap (if type_is_volatile t then @FF rmap ag_rmap else match p with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk m)) end) (@prop rmap ag_rmap (and (@ex memory_chunk (fun ch : memory_chunk => @eq mode (By_value m) (By_value ch))) (isptr p))) *)
  destruct (type_is_volatile t); try solve [apply FF_derives].
(* Goal: @derives rmap ag_rmap match p with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk m)) end (@prop rmap ag_rmap (and (@ex memory_chunk (fun ch : memory_chunk => @eq mode (By_value m) (By_value ch))) (isptr p))) *)
  destruct p; try solve [apply FF_derives].
(* Goal: @eq mpred (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tpointer t noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I32 Unsigned noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) *)
  if_tac.
  + apply readable_nonidentity in H0.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    apply nonidentity_nonunit in H0; tauto.
  + apply andp_left2.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    apply nonlock_permission_bytes_not_nonunit; auto.
Qed.

Lemma mapsto_pure_facts: forall sh t p v,
  mapsto sh t p v |-- !! ((exists ch, access_mode t = By_value ch) /\ isptr p).
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: @eq (forall (_ : val) (_ : val), mpred) (mapsto sh (Tpointer t a)) (mapsto sh (Tpointer Tvoid a)) *)
  unfold mapsto.
(* Goal: @derives rmap ag_rmap match access_mode t with | By_value ch => if type_is_volatile t then @FF rmap ag_rmap else match p with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto ch v sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk ch) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk ch)) end | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end (@prop rmap ag_rmap (and (@ex memory_chunk (fun ch : memory_chunk => @eq mode (access_mode t) (By_value ch))) (isptr p))) *)
  destruct (access_mode t); try solve [apply FF_derives].
(* Goal: @derives rmap ag_rmap (if type_is_volatile t then @FF rmap ag_rmap else match p with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk m)) end) (@prop rmap ag_rmap (and (@ex memory_chunk (fun ch : memory_chunk => @eq mode (By_value m) (By_value ch))) (isptr p))) *)
  destruct (type_is_volatile t); try solve [apply FF_derives].
(* Goal: @derives rmap ag_rmap match p with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk m)) end (@prop rmap ag_rmap (and (@ex memory_chunk (fun ch : memory_chunk => @eq mode (By_value m) (By_value ch))) (isptr p))) *)
  destruct p; try solve [apply FF_derives].

(* Goal: @derives rmap ag_rmap (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) (@prop rmap ag_rmap (and (@ex memory_chunk (fun ch : memory_chunk => @eq mode (By_value m) (By_value ch))) (isptr (Vptr b i)))) *)
  pose proof (@seplog.prop_right (pred rmap) (algNatDed _)).
(* Goal: @eq Byte.int i Byte.zero *)
  simpl in H; apply H; clear H.
(* Goal: and (@ex memory_chunk (fun ch : memory_chunk => @eq mode (By_value m) (By_value ch))) (isptr (Vptr b i)) *)
  split.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  + eauto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  + simpl; auto.
Qed.

(* Goal: and (Z.le Z0 ofs') (Z.le (Z.add ofs' (Z.of_nat n')) Ptrofs.modulus) *)
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh n' (@pair block Z b ofs')) (memory_block' sh n' b ofs') *)
Lemma mapsto_overlap: forall sh {cs: compspecs} t1 t2 p1 p2 v1 v2,
  nonunit sh ->
  pointer_range_overlap p1 (sizeof t1) p2 (sizeof t2) ->
  mapsto sh t1 p1 v1 * mapsto sh t2 p2 v2 |-- FF.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: @eq (forall (_ : val) (_ : val), mpred) (mapsto sh (Tpointer t a)) (mapsto sh (Tpointer Tvoid a)) *)
  unfold mapsto.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap match access_mode t1 with | By_value ch => if type_is_volatile t1 then @FF rmap ag_rmap else match p1 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t1 v1)) (address_mapsto ch v1 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v1 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t1 v1) (Z.divide (align_chunk ch) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk ch)) end | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end match access_mode t2 with | By_value ch => if type_is_volatile t2 then @FF rmap ag_rmap else match p2 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t2 v2)) (address_mapsto ch v2 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v2 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t2 v2) (Z.divide (align_chunk ch) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk ch)) end | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end) (@FF rmap ag_rmap) *)
  destruct (access_mode t1) eqn:AM1; try (rewrite FF_sepcon; auto).
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (if type_is_volatile t1 then @FF rmap ag_rmap else match p1 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t1 v1)) (address_mapsto m v1 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v1 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t1 v1) (Z.divide (align_chunk m) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk m)) end) match access_mode t2 with | By_value ch => if type_is_volatile t2 then @FF rmap ag_rmap else match p2 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t2 v2)) (address_mapsto ch v2 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v2 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t2 v2) (Z.divide (align_chunk ch) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk ch)) end | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end) (@FF rmap ag_rmap) *)
  destruct (access_mode t2) eqn:AM2; try (rewrite normalize.sepcon_FF; auto).
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (if type_is_volatile t1 then @FF rmap ag_rmap else match p1 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t1 v1)) (address_mapsto m v1 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v1 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t1 v1) (Z.divide (align_chunk m) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk m)) end) (if type_is_volatile t2 then @FF rmap ag_rmap else match p2 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t2 v2)) (address_mapsto m0 v2 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v2 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m0 v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t2 v2) (Z.divide (align_chunk m0) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk m0)) end)) (@FF rmap ag_rmap) *)
  destruct (type_is_volatile t1); try (rewrite FF_sepcon; auto).
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap match p1 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t1 v1)) (address_mapsto m v1 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v1 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t1 v1) (Z.divide (align_chunk m) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk m)) end (if type_is_volatile t2 then @FF rmap ag_rmap else match p2 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t2 v2)) (address_mapsto m0 v2 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v2 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m0 v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t2 v2) (Z.divide (align_chunk m0) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk m0)) end)) (@FF rmap ag_rmap) *)
  destruct (type_is_volatile t2); try (rewrite normalize.sepcon_FF; auto).
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap match p1 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t1 v1)) (address_mapsto m v1 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v1 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t1 v1) (Z.divide (align_chunk m) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk m)) end match p2 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t2 v2)) (address_mapsto m0 v2 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v2 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m0 v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t2 v2) (Z.divide (align_chunk m0) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk m0)) end) (@FF rmap ag_rmap) *)
  destruct p1; try (rewrite FF_sepcon; auto).
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t1 v1)) (address_mapsto m v1 sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v1 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t1 v1) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) match p2 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t2 v2)) (address_mapsto m0 v2 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v2 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m0 v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t2 v2) (Z.divide (align_chunk m0) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk m0)) end) (@FF rmap ag_rmap) *)
  destruct p2; try (rewrite normalize.sepcon_FF; auto).
(* Goal: @eq mpred (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tpointer t noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I32 Unsigned noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) *)
  if_tac.
  + apply derives_trans with ((EX  v : val,
          address_mapsto m v sh (b, Ptrofs.unsigned i)) *
      (EX  v : val,
          address_mapsto m0 v sh (b0, Ptrofs.unsigned i0))).
    - apply sepcon_derives; apply orp_left.
      * apply andp_left2, (exp_right v1).
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
        auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      * apply andp_left2; auto.
      * apply andp_left2, (exp_right v2).
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
        auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      * apply andp_left2; auto.
    - clear v1 v2.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@exp rmap ag_rmap val (fun v : val => address_mapsto m v sh (@pair block Z b (Ptrofs.unsigned i)))) (@exp rmap ag_rmap val (fun v : val => address_mapsto m0 v sh (@pair block Z b0 (Ptrofs.unsigned i0))))) (@FF rmap ag_rmap) *)
      rewrite exp_sepcon1.
(* Goal: @derives rmap ag_rmap (@exp rmap ag_rmap val (fun x : val => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto m x sh (@pair block Z b (Ptrofs.unsigned i))) (@exp rmap ag_rmap val (fun v : val => address_mapsto m0 v sh (@pair block Z b0 (Ptrofs.unsigned i0)))))) (@FF rmap ag_rmap) *)
      apply exp_left; intro v1.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto m v1 sh (@pair block Z b (Ptrofs.unsigned i))) (@exp rmap ag_rmap val (fun v : val => address_mapsto m0 v sh (@pair block Z b0 (Ptrofs.unsigned i0))))) (@FF rmap ag_rmap) *)
      rewrite exp_sepcon2.
(* Goal: @derives rmap ag_rmap (@exp rmap ag_rmap val (fun x : val => @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (address_mapsto m v1 sh (@pair block Z b (Ptrofs.unsigned i))) (address_mapsto m0 x sh (@pair block Z b0 (Ptrofs.unsigned i0))))) (@FF rmap ag_rmap) *)
      apply exp_left; intro v2.
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m) (@pair block Z b0 (Ptrofs.unsigned i0)) (size_chunk m0) *)
      clear H H1; rename H0 into H.
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m) (@pair block Z b0 (Ptrofs.unsigned i0)) (size_chunk m0) *)
      destruct H as [? [? [? [? ?]]]].
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) n1 (@pair block Z b0 (Ptrofs.unsigned i0)) n2 *)
      inversion H; subst.
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) n1 (@pair block Z b0 (Ptrofs.unsigned i0)) n2 *)
      inversion H0; subst.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      erewrite !size_chunk_sizeof in H1 by eauto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      apply address_mapsto_overlap; auto.
  + rewrite sepcon_andp_prop1, sepcon_andp_prop2.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t1 v1) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t2 v2) (Z.divide (align_chunk m0) (Ptrofs.unsigned i0)))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m)) (nonlock_permission_bytes sh (@pair block Z b0 (Ptrofs.unsigned i0)) (size_chunk m0))))) (@FF rmap ag_rmap) *)
    apply andp_left2, andp_left2.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    apply nonlock_permission_bytes_overlap; auto.
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m) (@pair block Z b0 (Ptrofs.unsigned i0)) (size_chunk m0) *)
    clear H H1; rename H0 into H.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    erewrite !size_chunk_sizeof in H by eauto.
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m) (@pair block Z b0 (Ptrofs.unsigned i0)) (size_chunk m0) *)
    destruct H as [? [? [? [? ?]]]].
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) n1 (@pair block Z b0 (Ptrofs.unsigned i0)) n2 *)
    inversion H; subst.
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) n1 (@pair block Z b0 (Ptrofs.unsigned i0)) n2 *)
    inversion H0; subst.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    auto.
Qed.

Lemma Nat2Z_add_lt: forall n i, Ptrofs.unsigned i + n < Ptrofs.modulus ->
  Z.of_nat (nat_of_Z n) + Ptrofs.unsigned i < Ptrofs.modulus.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: Z.le (Z.add (Z.of_nat (nat_of_Z n)) (Ptrofs.unsigned i)) Ptrofs.modulus *)
  destruct (zle 0 n).
  + rewrite Coqlib.nat_of_Z_eq by omega. omega.
  + rewrite nat_of_Z_neg by omega.
(* Goal: Z.le (Z.add (Z.of_nat O) (Ptrofs.unsigned i)) Ptrofs.modulus *)
    pose proof Ptrofs.unsigned_range i.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
    simpl.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
    omega.
Qed.

Lemma Nat2Z_add_le: forall n i, Ptrofs.unsigned i + n <= Ptrofs.modulus ->
  Z.of_nat (nat_of_Z n) + Ptrofs.unsigned i <= Ptrofs.modulus.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: Z.le (Z.add (Z.of_nat (nat_of_Z n)) (Ptrofs.unsigned i)) Ptrofs.modulus *)
  destruct (zle 0 n).
  + rewrite Coqlib.nat_of_Z_eq by omega. omega.
  + rewrite nat_of_Z_neg by omega.
(* Goal: Z.le (Z.add (Z.of_nat O) (Ptrofs.unsigned i)) Ptrofs.modulus *)
    pose proof Ptrofs.unsigned_range i.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
    simpl.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
    omega.
Qed.

Lemma memory_block_overlap: forall sh p1 n1 p2 n2, nonunit sh -> pointer_range_overlap p1 n1 p2 n2 -> memory_block sh n1 p1 * memory_block sh n2 p2 |-- FF.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (Z.le Z0 (Ptrofs.unsigned ofs)) (Z.lt (Z.add n (Ptrofs.unsigned ofs)) Ptrofs.modulus))) (address_mapsto_zeros sh (nat_of_Z n) (@pair block Z b (Ptrofs.unsigned ofs)))) (memory_block sh n (Vptr b ofs)) *)
  unfold memory_block.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap match p1 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => @andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned ofs) n1) Ptrofs.modulus)) (memory_block' sh (nat_of_Z n1) b (Ptrofs.unsigned ofs)) end match p2 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => @andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned ofs) n2) Ptrofs.modulus)) (memory_block' sh (nat_of_Z n2) b (Ptrofs.unsigned ofs)) end) (@FF rmap ag_rmap) *)
  destruct p1; try solve [rewrite FF_sepcon; auto].
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned i) n1) Ptrofs.modulus)) (memory_block' sh (nat_of_Z n1) b (Ptrofs.unsigned i))) match p2 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => @andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned ofs) n2) Ptrofs.modulus)) (memory_block' sh (nat_of_Z n2) b (Ptrofs.unsigned ofs)) end) (@FF rmap ag_rmap) *)
  destruct p2; try solve [rewrite normalize.sepcon_FF; auto].
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned i) m) Ptrofs.modulus)) (memory_block' sh (nat_of_Z m) b (Ptrofs.unsigned i))) (memory_block' sh (nat_of_Z n) b (Ptrofs.unsigned i))) (@FF rmap ag_rmap) *)
  rewrite sepcon_andp_prop1.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned i) n1) Ptrofs.modulus)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (memory_block' sh (nat_of_Z n1) b (Ptrofs.unsigned i)) (@andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned i0) n2) Ptrofs.modulus)) (memory_block' sh (nat_of_Z n2) b0 (Ptrofs.unsigned i0))))) (@FF rmap ag_rmap) *)
  rewrite sepcon_andp_prop2.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  apply normalize.derives_extract_prop; intros.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  apply normalize.derives_extract_prop; intros. 
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (memory_block' sh (nat_of_Z n1) b (Ptrofs.unsigned i)) (memory_block' sh (nat_of_Z n2) b0 (Ptrofs.unsigned i0))) (@FF rmap ag_rmap) *)
  rewrite memory_block'_eq; [| pose proof Ptrofs.unsigned_range i; omega | apply Nat2Z_add_lt; omega].
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (memory_block'_alt sh (nat_of_Z n1) b (Ptrofs.unsigned i)) (memory_block' sh (nat_of_Z n2) b0 (Ptrofs.unsigned i0))) (@FF rmap ag_rmap) *)
  rewrite memory_block'_eq; [| pose proof Ptrofs.unsigned_range i0; omega | apply Nat2Z_add_lt; omega].
(* Goal: @eq mpred (memory_block'_alt sh (nat_of_Z j) b ofs) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (memory_block'_alt sh (nat_of_Z i) b ofs) (memory_block'_alt sh (nat_of_Z (Z.sub j i)) b (Z.add ofs i))) *)
  unfold memory_block'_alt.
(* Goal: @eq mpred (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tpointer t noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I32 Unsigned noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) *)
  if_tac.
  + clear H2.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec_range (Z.of_nat (nat_of_Z m)) sh (@pair block Z b (Ptrofs.unsigned i))) (VALspec_range (Z.of_nat (nat_of_Z n)) sh (@pair block Z b (Ptrofs.unsigned i)))) (@FF rmap ag_rmap) *)
    apply VALspec_range_overlap.
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) (Z.of_nat (nat_of_Z n1)) (@pair block Z b0 (Ptrofs.unsigned i0)) (Z.of_nat (nat_of_Z n2)) *)
    pose proof pointer_range_overlap_non_zero _ _ _ _ H0.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
    rewrite !Coqlib.nat_of_Z_eq by omega.
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) n1 (@pair block Z b0 (Ptrofs.unsigned i0)) n2 *)
    destruct H0 as [[? ?] [[? ?] [? [? ?]]]].
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) n1 (@pair block Z b0 (Ptrofs.unsigned i0)) n2 *)
    inversion H0; inversion H4.
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) n1 (@pair block Z b0 (Ptrofs.unsigned i0)) n2 *)
    subst.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  + apply nonlock_permission_bytes_overlap; auto.
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) (Z.of_nat (nat_of_Z n1)) (@pair block Z b0 (Ptrofs.unsigned i0)) (Z.of_nat (nat_of_Z n2)) *)
    pose proof pointer_range_overlap_non_zero _ _ _ _ H0.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
    rewrite !Coqlib.nat_of_Z_eq by omega.
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) n1 (@pair block Z b0 (Ptrofs.unsigned i0)) n2 *)
    destruct H0 as [[? ?] [[? ?] [? [? ?]]]].
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) n1 (@pair block Z b0 (Ptrofs.unsigned i0)) n2 *)
    inversion H0; inversion H5.
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) n1 (@pair block Z b0 (Ptrofs.unsigned i0)) n2 *)
    subst.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    auto.
Qed.

Lemma mapsto_conflict:
  forall sh t v v2 v3,
  nonunit sh ->
  mapsto sh t v v2 * mapsto sh t v v3 |-- FF.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (mapsto sh t v v2) (mapsto sh t v v3)) (@FF rmap ag_rmap) *)
  rewrite (@add_andp (pred rmap) (algNatDed _) _ _ (mapsto_pure_facts sh t v v3)).
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
  simpl.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (mapsto sh t v v2) (@andp rmap ag_rmap (mapsto sh t v v3) (@prop rmap ag_rmap (and (@ex memory_chunk (fun ch : memory_chunk => @eq mode (access_mode t) (By_value ch))) (isptr v))))) (@FF rmap ag_rmap) *)
  rewrite andp_comm.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (mapsto sh t v v2) (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@ex memory_chunk (fun ch : memory_chunk => @eq mode (access_mode t) (By_value ch))) (isptr v))) (mapsto sh t v v3))) (@FF rmap ag_rmap) *)
  rewrite sepcon_andp_prop.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (@ex memory_chunk (fun ch : memory_chunk => @eq mode (access_mode t) (By_value ch))) (isptr v))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (mapsto sh t v v2) (mapsto sh t v v3))) (@FF rmap ag_rmap) *)
  apply prop_andp_left; intros [[? ?] ?].
(* Goal: @eq (forall (_ : val) (_ : val), mpred) (mapsto sh (Tpointer t a)) (mapsto sh (Tpointer Tvoid a)) *)
  unfold mapsto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))) *)
  rewrite H0.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (if type_is_volatile t then @FF rmap ag_rmap else match v with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v2)) (address_mapsto x v2 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v2 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto x v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v2) (Z.divide (align_chunk x) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk x)) end) (if type_is_volatile t then @FF rmap ag_rmap else match v with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v3)) (address_mapsto x v3 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v3 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto x v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v3) (Z.divide (align_chunk x) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk x)) end)) (@FF rmap ag_rmap) *)
  destruct (type_is_volatile t); try (rewrite FF_sepcon; auto).
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap match v with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v2)) (address_mapsto x v2 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v2 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto x v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v2) (Z.divide (align_chunk x) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk x)) end match v with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v3)) (address_mapsto x v3 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v3 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto x v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v3) (Z.divide (align_chunk x) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk x)) end) (@FF rmap ag_rmap) *)
  destruct v; try (rewrite FF_sepcon; auto).
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v2)) (address_mapsto x v2 sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v2 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto x v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v2) (Z.divide (align_chunk x) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk x))) (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v3)) (address_mapsto x v3 sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v3 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto x v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v3) (Z.divide (align_chunk x) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk x)))) (@FF rmap ag_rmap) *)
  pose proof (size_chunk_pos x).
(* Goal: @eq mpred (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tpointer t noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I32 Unsigned noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) *)
  if_tac.
*
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v2)) (address_mapsto x v2 sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v2 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto x v2' sh (@pair block Z b (Ptrofs.unsigned i)))))) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v3)) (address_mapsto x v3 sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v3 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto x v2' sh (@pair block Z b (Ptrofs.unsigned i))))))) (@FF rmap ag_rmap) *)
  normalize.
  rewrite distrib_orp_sepcon, !distrib_orp_sepcon2;
  repeat apply orp_left;
  rewrite ?sepcon_andp_prop1;  repeat (apply prop_andp_left; intro);
  rewrite ?sepcon_andp_prop2;  repeat (apply prop_andp_left; intro);
  rewrite ?exp_sepcon1;  repeat (apply exp_left; intro);
  rewrite ?exp_sepcon2;  repeat (apply exp_left; intro);
  apply address_mapsto_overlap;
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
  exists (b, Ptrofs.unsigned i); repeat split; omega.
*
  rewrite ?sepcon_andp_prop1;  repeat (apply prop_andp_left; intro);
  rewrite ?sepcon_andp_prop2;  repeat (apply prop_andp_left; intro).
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  apply nonlock_permission_bytes_overlap; auto.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
  exists (b, Ptrofs.unsigned i); repeat split; omega.
Qed.

Lemma memory_block_conflict: forall sh n m p,
  nonunit sh ->
  0 < n <= Ptrofs.max_unsigned -> 0 < m <= Ptrofs.max_unsigned ->
  memory_block sh n p * memory_block sh m p |-- FF.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (Z.le Z0 (Ptrofs.unsigned ofs)) (Z.lt (Z.add n (Ptrofs.unsigned ofs)) Ptrofs.modulus))) (address_mapsto_zeros sh (nat_of_Z n) (@pair block Z b (Ptrofs.unsigned ofs)))) (memory_block sh n (Vptr b ofs)) *)
  unfold memory_block.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap match p with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => @andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned ofs) n) Ptrofs.modulus)) (memory_block' sh (nat_of_Z n) b (Ptrofs.unsigned ofs)) end match p with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => @andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned ofs) m) Ptrofs.modulus)) (memory_block' sh (nat_of_Z m) b (Ptrofs.unsigned ofs)) end) (@FF rmap ag_rmap) *)
  destruct p; try solve [rewrite FF_sepcon; auto].
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned i) m) Ptrofs.modulus)) (memory_block' sh (nat_of_Z m) b (Ptrofs.unsigned i))) (memory_block' sh (nat_of_Z n) b (Ptrofs.unsigned i))) (@FF rmap ag_rmap) *)
  rewrite sepcon_andp_prop1.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned i) m) Ptrofs.modulus)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (memory_block' sh (nat_of_Z m) b (Ptrofs.unsigned i)) (memory_block' sh (nat_of_Z n) b (Ptrofs.unsigned i)))) (@FF rmap ag_rmap) *)
  apply prop_andp_left; intro.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (memory_block' sh (nat_of_Z n) b (Ptrofs.unsigned i)) (@andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned i) m) Ptrofs.modulus)) (memory_block' sh (nat_of_Z m) b (Ptrofs.unsigned i)))) (@FF rmap ag_rmap) *)
  rewrite sepcon_comm.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned i) m) Ptrofs.modulus)) (memory_block' sh (nat_of_Z m) b (Ptrofs.unsigned i))) (memory_block' sh (nat_of_Z n) b (Ptrofs.unsigned i))) (@FF rmap ag_rmap) *)
  rewrite sepcon_andp_prop1.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned i) m) Ptrofs.modulus)) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (memory_block' sh (nat_of_Z m) b (Ptrofs.unsigned i)) (memory_block' sh (nat_of_Z n) b (Ptrofs.unsigned i)))) (@FF rmap ag_rmap) *)
  apply prop_andp_left; intro.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (memory_block'_alt sh (nat_of_Z m) b (Ptrofs.unsigned i)) (memory_block' sh (nat_of_Z n) b (Ptrofs.unsigned i))) (@FF rmap ag_rmap) *)
  rewrite memory_block'_eq; [| pose proof Ptrofs.unsigned_range i; omega | rewrite Z2Nat.id; omega].
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (memory_block'_alt sh (nat_of_Z m) b (Ptrofs.unsigned i)) (memory_block' sh (nat_of_Z n) b (Ptrofs.unsigned i))) (@FF rmap ag_rmap) *)
  rewrite memory_block'_eq; [| pose proof Ptrofs.unsigned_range i; omega | rewrite Z2Nat.id; omega].
(* Goal: @eq mpred (memory_block'_alt sh (nat_of_Z j) b ofs) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (memory_block'_alt sh (nat_of_Z i) b ofs) (memory_block'_alt sh (nat_of_Z (Z.sub j i)) b (Z.add ofs i))) *)
  unfold memory_block'_alt.
(* Goal: @eq mpred (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tpointer t noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I32 Unsigned noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) *)
  if_tac.
  + apply VALspec_range_overlap.
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) (Z.of_nat (nat_of_Z m)) (@pair block Z b (Ptrofs.unsigned i)) (Z.of_nat (nat_of_Z n)) *)
    exists (b, Ptrofs.unsigned i).
    simpl; repeat split; auto; try omega;
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
    rewrite Z2Nat.id; omega.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  + apply nonlock_permission_bytes_overlap; auto.
(* Goal: range_overlap (@pair block Z b (Ptrofs.unsigned i)) (Z.of_nat (nat_of_Z m)) (@pair block Z b (Ptrofs.unsigned i)) (Z.of_nat (nat_of_Z n)) *)
    exists (b, Ptrofs.unsigned i).
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
    repeat split; auto; try rewrite Z2Nat.id; omega.
Qed.

Lemma memory_block_non_pos_Vptr: forall sh n b z, n <= 0 -> memory_block sh n (Vptr b z) = emp.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros. unfold memory_block.
(* Goal: @eq mpred (@andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned z) n) Ptrofs.modulus)) (memory_block' sh (nat_of_Z n) b (Ptrofs.unsigned z))) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
  replace (nat_of_Z n) with (0%nat) by (symmetry; apply nat_of_Z_neg; auto).
(* Goal: @eq mpred (@andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned z) n) Ptrofs.modulus)) (memory_block' sh O b (Ptrofs.unsigned z))) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
  unfold memory_block'.
(* Goal: @eq mpred (@andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned z) n) Ptrofs.modulus)) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap)) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
  pose proof Ptrofs.unsigned_range z.
  assert (Ptrofs.unsigned z + n < Ptrofs.modulus) by omega.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v2)) (address_mapsto x v2 sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v2 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto x v2' sh (@pair block Z b (Ptrofs.unsigned i)))))) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v3)) (address_mapsto x v3 sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v3 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto x v2' sh (@pair block Z b (Ptrofs.unsigned i))))))) (@FF rmap ag_rmap) *)
  apply pred_ext; normalize.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  apply andp_right; auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  intros ? _; simpl; auto.
Qed.

Lemma memory_block_zero_Vptr: forall sh b z, memory_block sh 0 (Vptr b z) = emp.
Proof.
(* Goal: forall (sh : share) (b : block) (z : Ptrofs.int), @eq mpred (memory_block sh Z0 (Vptr b z)) (@emp rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap) *)
  intros; apply memory_block_non_pos_Vptr.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
  omega.
Qed.

Lemma mapsto_zeros_memory_block: forall sh n p,
  readable_share sh ->
  mapsto_zeros n sh p |--
  memory_block sh n p.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: @derives rmap ag_rmap (mapsto_zeros n sh p) (memory_block sh n p) *)
  unfold mapsto_zeros.
(* Goal: @derives rmap ag_rmap match p with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b z => @andp rmap ag_rmap (@prop rmap ag_rmap (and (Z.le Z0 (Ptrofs.unsigned z)) (Z.lt (Z.add n (Ptrofs.unsigned z)) Ptrofs.modulus))) (address_mapsto_zeros sh (nat_of_Z n) (@pair block Z b (Ptrofs.unsigned z))) end (memory_block sh n p) *)
  destruct p; try solve [intros ? ?; contradiction].
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (Z.le Z0 (Ptrofs.unsigned i)) (Z.lt (Z.add n (Ptrofs.unsigned i)) Ptrofs.modulus))) (address_mapsto_zeros sh (nat_of_Z n) (@pair block Z b (Ptrofs.unsigned i)))) (memory_block sh n (Vptr b i)) *)
  rename i into ofs.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros. rename H into RS. pose proof I.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (Z.le Z0 (Ptrofs.unsigned ofs)) (Z.lt (Z.add n (Ptrofs.unsigned ofs)) Ptrofs.modulus))) (address_mapsto_zeros sh (nat_of_Z n) (@pair block Z b (Ptrofs.unsigned ofs)))) (memory_block sh n (Vptr b ofs)) *)
  unfold memory_block.
(* Goal: and (Z.le Z0 ofs') (Z.le (Z.add ofs' (Z.of_nat n')) Ptrofs.modulus) *)
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh n' (@pair block Z b ofs')) (memory_block' sh n' b ofs') *)
  destruct (zlt n 0).   {
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
     rewrite nat_of_Z_neg by omega. simpl.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
     apply andp_derives; auto.
(* Goal: @derives rmap ag_rmap (@prop rmap ag_rmap (and (Z.le Z0 (Ptrofs.unsigned ofs)) (Z.lt (Z.add n (Ptrofs.unsigned ofs)) Ptrofs.modulus))) (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned ofs) n) Ptrofs.modulus)) *)
     intros ? ?. simpl in *. destruct H0.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
     omega. 
  }
(* Goal: not (adr_range (@pair block Z b (Z.succ i)) (Z.max (Z.of_nat n) Z0) (@pair block Z b' i')) *)
 apply prop_andp_left; intros [? ?].
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
 rewrite prop_true_andp by omega.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
 assert (n <= Ptrofs.modulus) by omega. clear H H0. rename H1 into H'.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
 assert (0 <= n <= Ptrofs.modulus) by omega. clear H2 g.
    rewrite <- (Z2Nat.id n) in H', H by omega.
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh (nat_of_Z n) (@pair block Z b (Ptrofs.unsigned ofs))) (memory_block' sh (nat_of_Z n) b (Ptrofs.unsigned ofs)) *)
    change nat_of_Z with Z.to_nat.
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh (Z.to_nat n) (@pair block Z b (Ptrofs.unsigned ofs))) (memory_block' sh (Z.to_nat n) b (Ptrofs.unsigned ofs)) *)
    forget (Z.to_nat n) as n'.
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh n' (@pair block Z b (Ptrofs.unsigned ofs))) (memory_block' sh n' b (Ptrofs.unsigned ofs)) *)
    clear n.
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh n' (@pair block Z b (Ptrofs.unsigned ofs))) (memory_block' sh n' b (Ptrofs.unsigned ofs)) *)
    remember (Ptrofs.unsigned ofs) as ofs'.
    assert (Ptrofs.unsigned (Ptrofs.repr ofs') = ofs')
      by (subst; rewrite Ptrofs.repr_unsigned; reflexivity).
    assert (0 <= ofs' /\ ofs' + Z.of_nat n' <= Ptrofs.modulus).
(* Goal: and (Z.le Z0 ofs') (Z.le (Z.add ofs' (Z.of_nat n')) Ptrofs.modulus) *)
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh n' (@pair block Z b ofs')) (memory_block' sh n' b ofs') *)
    {
(* Goal: and (Z.le Z0 ofs') (Z.le (Z.add ofs' (Z.of_nat n')) Ptrofs.modulus) *)
      pose proof Ptrofs.unsigned_range ofs.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
      omega.
    }
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh n' (@pair block Z b ofs')) (memory_block' sh n' b ofs') *)
    clear Heqofs' H'.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    assert (Ptrofs.unsigned (Ptrofs.repr ofs') = ofs' \/ n' = 0%nat) by tauto.
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh n' (@pair block Z b ofs')) (memory_block' sh n' b ofs') *)
    clear H0; rename H2 into H0.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
    revert ofs' H H1 H0; induction n'; intros.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    - simpl; auto.
    - destruct H1.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
      rewrite inj_S in H2. unfold Z.succ in H2. simpl.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      apply sepcon_derives; auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) match access_mode (Tint I8 Unsigned noattr) with | By_value ch => if type_is_volatile (Tint I8 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto ch Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk ch) (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
      * unfold mapsto_, mapsto. simpl.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
        rewrite if_true by auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (@orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap False) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))))) *)
        apply orp_right2.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
        rewrite prop_true_andp by auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs'))))) *)
        apply exp_right with (Vint Int.zero).
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))) *)
        destruct H0; [| omega].
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr ofs')))) *)
        rewrite H0.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
        auto.
      * fold address_mapsto_zeros. fold memory_block'.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
        apply IHn'. omega. omega.
        destruct (zlt (ofs' + 1) Ptrofs.modulus).
(* Goal: or (@eq Z (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs' (Zpos xH)))) (Z.add ofs' (Zpos xH))) (@eq nat n' O) *)
(* Goal: or (@eq Z (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs' (Zpos xH)))) (Z.add ofs' (Zpos xH))) (@eq nat n' O) *)
        rewrite Ptrofs.unsigned_repr; [left; reflexivity | ].
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
        unfold Ptrofs.max_unsigned; omega.
(* Goal: or (@eq Z (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs' (Zpos xH)))) (Z.add ofs' (Zpos xH))) (@eq nat n' O) *)
        right.
(* Goal: @eq nat n' O *)
           destruct H0; [| inversion H0].
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
           omega.
Qed.

Lemma memory_block'_split:
  forall sh b ofs i j,
   0 <= i <= j ->
    j <= j+ofs < Ptrofs.modulus ->
   memory_block' sh (nat_of_Z j) b ofs =
      memory_block' sh (nat_of_Z i) b ofs * memory_block' sh (nat_of_Z (j-i)) b (ofs+i).
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
  rewrite memory_block'_eq; try rewrite Coqlib.nat_of_Z_eq; try omega.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
  rewrite memory_block'_eq; try rewrite Coqlib.nat_of_Z_eq; try omega.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
  rewrite memory_block'_eq; try rewrite Coqlib.nat_of_Z_eq; try omega.
(* Goal: @eq mpred (memory_block'_alt sh (nat_of_Z j) b ofs) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (memory_block'_alt sh (nat_of_Z i) b ofs) (memory_block'_alt sh (nat_of_Z (Z.sub j i)) b (Z.add ofs i))) *)
  unfold memory_block'_alt.
(* Goal: @eq mpred (if readable_share_dec sh then VALspec_range (Z.of_nat (nat_of_Z j)) sh (@pair block Z b ofs) else nonlock_permission_bytes sh (@pair block Z b ofs) (Z.of_nat (nat_of_Z j))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (if readable_share_dec sh then VALspec_range (Z.of_nat (nat_of_Z i)) sh (@pair block Z b ofs) else nonlock_permission_bytes sh (@pair block Z b ofs) (Z.of_nat (nat_of_Z i))) (if readable_share_dec sh then VALspec_range (Z.of_nat (nat_of_Z (Z.sub j i))) sh (@pair block Z b (Z.add ofs i)) else nonlock_permission_bytes sh (@pair block Z b (Z.add ofs i)) (Z.of_nat (nat_of_Z (Z.sub j i))))) *)
  repeat (rewrite Coqlib.nat_of_Z_eq; try omega).
(* Goal: @eq mpred (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tpointer t noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I32 Unsigned noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) *)
  if_tac.
  + etransitivity ; [ | eapply VALspec_range_split2; [reflexivity | omega | omega]].
(* Goal: @eq Prop (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) *)
    f_equal.
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
    omega.
  + apply nonlock_permission_bytes_split2; omega.
Qed.

Lemma memory_block_split:
  forall (sh : share) (b : block) (ofs n m : Z),
  0 <= n ->
  0 <= m ->
  n + m <= n + m + ofs < Ptrofs.modulus ->
  memory_block sh (n + m) (Vptr b (Ptrofs.repr ofs)) =
  memory_block sh n (Vptr b (Ptrofs.repr ofs)) *
  memory_block sh m (Vptr b (Ptrofs.repr (ofs + n))).
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (Z.le Z0 (Ptrofs.unsigned ofs)) (Z.lt (Z.add n (Ptrofs.unsigned ofs)) Ptrofs.modulus))) (address_mapsto_zeros sh (nat_of_Z n) (@pair block Z b (Ptrofs.unsigned ofs)))) (memory_block sh n (Vptr b ofs)) *)
  unfold memory_block.
  rewrite memory_block'_split with (i := n); [| omega |].
(* Goal: and (Z.le Z0 ofs') (Z.le (Z.add ofs' (Z.of_nat n')) Ptrofs.modulus) *)
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh n' (@pair block Z b ofs')) (memory_block' sh n' b ofs') *)
  2:{
    pose proof Ptrofs.unsigned_range (Ptrofs.repr ofs).
    pose proof Ptrofs.unsigned_repr_eq ofs.
    assert (ofs mod Ptrofs.modulus <= ofs) by (apply Z.mod_le; omega).
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
    omega.
  } 
  replace (n + m - n) with m by omega.
  replace (memory_block' sh (nat_of_Z m) b (Ptrofs.unsigned (Ptrofs.repr ofs) + n)) with
    (memory_block' sh (nat_of_Z m) b (Ptrofs.unsigned (Ptrofs.repr (ofs + n)))).
(* Goal: and (Z.le Z0 ofs') (Z.le (Z.add ofs' (Z.of_nat n')) Ptrofs.modulus) *)
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh n' (@pair block Z b ofs')) (memory_block' sh n' b ofs') *)
  2: {
    destruct (zeq m 0).
    + subst. reflexivity.
    + assert (ofs + n < Ptrofs.modulus) by omega.
      rewrite !Ptrofs.unsigned_repr by (unfold Ptrofs.max_unsigned; omega).
(* Goal: @eq mpred (mapsto sh (Tint I32 Unsigned noattr) v1 v2) (mapsto sh (Tint I32 Signed noattr) v1 v2) *)
      reflexivity.
  }
(* Goal: @eq (@pred rmap ag_rmap) (VALspec_range (size_chunk ch) sh l) (@exp rmap ag_rmap val (fun v : val => address_mapsto ch v sh l)) *)
  apply pred_ext.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  + apply prop_andp_left; intros.
    apply sepcon_derives; (apply andp_right; [intros ? _; simpl | apply derives_refl]).
    - omega.
    - rewrite Ptrofs.unsigned_repr_eq.
      assert ((ofs + n) mod Ptrofs.modulus <= ofs + n) by (apply Z.mod_le; omega).
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
      omega.
  + apply andp_right; [intros ? _; simpl |].
    - rewrite Ptrofs.unsigned_repr_eq.
      assert (ofs mod Ptrofs.modulus <= ofs) by (apply Z.mod_le; omega).
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
      omega.
    - apply sepcon_derives; apply andp_left2; apply derives_refl.
Qed.

Lemma memory_block_share_join:
  forall sh1 sh2 sh n p,
   sepalg.join sh1 sh2 sh ->
   memory_block sh1 n p * memory_block sh2 n p = memory_block sh n p.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
  destruct p; try solve [unfold memory_block; rewrite FF_sepcon; auto].
(* Goal: Z.le (Z.add (Z.of_nat (nat_of_Z n)) (Ptrofs.unsigned i)) Ptrofs.modulus *)
  destruct (zle 0 n).
(* Goal: and (Z.le Z0 ofs') (Z.le (Z.add ofs' (Z.of_nat n')) Ptrofs.modulus) *)
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh n' (@pair block Z b ofs')) (memory_block' sh n' b ofs') *)
  2:{
(* Goal: @eq Z j (Z.add i (Z.sub j i)) *)
    rewrite !memory_block_non_pos_Vptr by omega.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    rewrite emp_sepcon; auto.
  }
(* Goal: @derives rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (and (Z.le Z0 (Ptrofs.unsigned ofs)) (Z.lt (Z.add n (Ptrofs.unsigned ofs)) Ptrofs.modulus))) (address_mapsto_zeros sh (nat_of_Z n) (@pair block Z b (Ptrofs.unsigned ofs)))) (memory_block sh n (Vptr b ofs)) *)
  unfold memory_block.
  destruct (zlt (Ptrofs.unsigned i + n) Ptrofs.modulus).
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  + rewrite !prop_true_andp by auto.
    repeat (rewrite memory_block'_eq; [| pose proof Ptrofs.unsigned_range i; omega | rewrite Coqlib.nat_of_Z_eq; omega]).
(* Goal: @eq mpred (memory_block'_alt sh (nat_of_Z j) b ofs) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (memory_block'_alt sh (nat_of_Z i) b ofs) (memory_block'_alt sh (nat_of_Z (Z.sub j i)) b (Z.add ofs i))) *)
    unfold memory_block'_alt.
(* Goal: @eq (@pred rmap ag_rmap) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (if readable_share_dec sh1 then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh1 (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh1 (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh1 (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) (if readable_share_dec sh2 then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh2 (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh2 (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh2 (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m)))) (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val t v)) (address_mapsto m v sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' t v) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) *)
    destruct (readable_share_dec sh1), (readable_share_dec sh2).
    - rewrite if_true by (eapply readable_share_join; eauto).
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      apply VALspec_range_share_join; auto.
    - rewrite if_true by (eapply readable_share_join; eauto).
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (memory_block' sh (nat_of_Z n) b (Ptrofs.unsigned i)) (@andp rmap ag_rmap (@prop rmap ag_rmap (Z.lt (Z.add (Ptrofs.unsigned i) m) Ptrofs.modulus)) (memory_block' sh (nat_of_Z m) b (Ptrofs.unsigned i)))) (@FF rmap ag_rmap) *)
      rewrite sepcon_comm.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      apply nonlock_permission_bytes_VALspec_range_join; auto.
    - rewrite if_true by (eapply readable_share_join; eauto).
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      apply nonlock_permission_bytes_VALspec_range_join; auto.
    - rewrite if_false.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      * apply nonlock_permission_bytes_share_join; auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
      * eapply join_unreadable_shares; eauto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
  + rewrite !prop_false_andp by auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
    rewrite FF_sepcon; auto.
Qed.

Lemma mapsto_pointer_void:
  forall sh t a, 
   eqb_type (Tpointer t a) int_or_ptr_type = false ->
   eqb_type (Tpointer Tvoid a) int_or_ptr_type = false ->
   mapsto sh (Tpointer t a) = mapsto sh (Tpointer Tvoid a).
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
intros.
(* Goal: @eq (forall (_ : val) (_ : val), mpred) (mapsto sh (Tpointer t a)) (mapsto sh (Tpointer Tvoid a)) *)
unfold mapsto.
(* Goal: @eq (forall (_ : val) (_ : val), mpred) (mapsto sh (Tint I32 Unsigned noattr)) (mapsto sh (Tint I32 Signed noattr)) *)
extensionality v1 v2.
(* Goal: @eq mpred match access_mode (Tpointer t a) with | By_value ch => if type_is_volatile (Tpointer t a) then @FF rmap ag_rmap else match v1 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap ((if eqb_type (Tpointer t a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) v2)) (address_mapsto ch v2 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v2 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (forall _ : not (@eq val v2 Vundef), (if eqb_type (Tpointer t a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) v2) (Z.divide (align_chunk ch) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk ch)) end | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end match access_mode (Tpointer Tvoid a) with | By_value ch => if type_is_volatile (Tpointer Tvoid a) then @FF rmap ag_rmap else match v1 with | Vundef => @FF rmap ag_rmap | Vint i => @FF rmap ag_rmap | Vlong i => @FF rmap ag_rmap | Vfloat f => @FF rmap ag_rmap | Vsingle f => @FF rmap ag_rmap | Vptr b ofs => if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap ((if eqb_type (Tpointer Tvoid a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) v2)) (address_mapsto ch v2 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val v2 Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (forall _ : not (@eq val v2 Vundef), (if eqb_type (Tpointer Tvoid a) int_or_ptr_type then is_pointer_or_integer else is_pointer_or_null) v2) (Z.divide (align_chunk ch) (Ptrofs.unsigned ofs)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk ch)) end | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
unfold tc_val', tc_val. rewrite H, H0.
(* Goal: @eq mpred (mapsto sh (Tint I32 Unsigned noattr) v1 v2) (mapsto sh (Tint I32 Signed noattr) v1 v2) *)
reflexivity.
Qed.

Lemma is_pointer_or_null_nullval: is_pointer_or_null nullval.
Proof.
(* Goal: is_pointer_or_null nullval *)
unfold is_pointer_or_null, nullval.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
simple_if_tac; auto.
Qed.
Hint Resolve is_pointer_or_null_nullval.

Lemma tc_val_pointer_nullval':
 forall t a, tc_val (Tpointer t a) nullval.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
 intros. hnf. unfold nullval.
 simple_if_tac; hnf;
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
 simple_if_tac; auto.
Qed.
Hint Resolve tc_val_pointer_nullval'.

Arguments type_is_volatile ty / .

Definition is_int32_noattr_type t :=
 match t with
(* Goal: and (Z.le Z0 ofs') (Z.le (Z.add ofs' (Z.of_nat n')) Ptrofs.modulus) *)
(* Goal: @derives rmap ag_rmap (address_mapsto_zeros sh n' (@pair block Z b ofs')) (memory_block' sh n' b ofs') *)
 | Tint I32 _ {| attr_volatile := false; attr_alignas := None |} => True
 | _ => False
 end.

Lemma mapsto_mapsto_int32:
  forall sh t1 t2 p v,
   is_int32_noattr_type t1 ->
   is_int32_noattr_type t2 ->
   mapsto sh t1 p v |-- mapsto sh t2 p v.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
intros.
(* Goal: @derives rmap ag_rmap (mapsto sh t1 p v) (mapsto_ sh t2 p) *)
destruct t1; try destruct i; try contradiction.
(* Goal: @derives rmap ag_rmap (mapsto sh (Tint I32 s (mk_attr false (@None N))) p v) (mapsto_ sh (Tint I32 s0 a) p) *)
destruct a as [ [ | ] [ | ] ]; try contradiction.
(* Goal: @derives rmap ag_rmap (mapsto sh (Tint I32 s (mk_attr false (@None N))) p v) (mapsto_ sh t2 p) *)
destruct t2; try destruct i; try contradiction.
(* Goal: @derives rmap ag_rmap (mapsto sh (Tint I32 s (mk_attr false (@None N))) p v) (mapsto_ sh (Tint I32 s0 a) p) *)
destruct a as [ [ | ] [ | ] ]; try contradiction.
(* Goal: @derives rmap ag_rmap (mapsto sh (Tint I32 s (mk_attr false (@None N))) p v) (mapsto sh (Tint I32 s0 (mk_attr false (@None N))) p v) *)
apply derives_refl.
Qed.

Lemma mapsto_mapsto__int32:
  forall sh t1 t2 p v,
   is_int32_noattr_type t1 ->
   is_int32_noattr_type t2 ->
   mapsto sh t1 p v |-- mapsto_ sh t2 p.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
intros.
(* Goal: @derives rmap ag_rmap (mapsto sh t1 p v) (mapsto_ sh t2 p) *)
destruct t1; try destruct i; try contradiction.
(* Goal: @derives rmap ag_rmap (mapsto sh (Tint I32 s (mk_attr false (@None N))) p v) (mapsto_ sh (Tint I32 s0 a) p) *)
destruct a as [ [ | ] [ | ] ]; try contradiction.
(* Goal: @derives rmap ag_rmap (mapsto sh (Tint I32 s (mk_attr false (@None N))) p v) (mapsto_ sh t2 p) *)
destruct t2; try destruct i; try contradiction.
(* Goal: @derives rmap ag_rmap (mapsto sh (Tint I32 s (mk_attr false (@None N))) p v) (mapsto_ sh (Tint I32 s0 a) p) *)
destruct a as [ [ | ] [ | ] ]; try contradiction.
(* Goal: @derives rmap ag_rmap (mapsto sh (Tint I32 s (mk_attr false (@None N))) p v) (mapsto_ sh (Tint I32 s0 (mk_attr false (@None N))) p) *)
unfold mapsto_. apply mapsto_mapsto_.
Qed.

Lemma mapsto_tuint_tint:
  forall sh, mapsto sh (Tint I32 Unsigned noattr) = mapsto sh (Tint I32 Signed noattr).
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
intros.
(* Goal: @eq (forall (_ : val) (_ : val), mpred) (mapsto sh (Tint I32 Unsigned noattr)) (mapsto sh (Tint I32 Signed noattr)) *)
extensionality v1 v2.
(* Goal: @eq mpred (mapsto sh (Tint I32 Unsigned noattr) v1 v2) (mapsto sh (Tint I32 Signed noattr) v1 v2) *)
reflexivity.
Qed.

Lemma tc_val_pointer_nullval:
 forall t, tc_val (Tpointer t noattr) nullval.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
 intros. unfold nullval; simpl.
(* Goal: (if andb (eqb_type t Tvoid) false then is_pointer_or_integer else is_pointer_or_null) (if Archi.ptr64 then Vlong Int64.zero else Vint Int.zero) *)
 rewrite andb_false_r.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
 hnf. simple_if_tac; auto.
Qed.
Hint Resolve tc_val_pointer_nullval.

Lemma mapsto_tuint_tptr_nullval:
  forall sh p t, mapsto sh (Tpointer t noattr) p nullval = mapsto sh size_t p nullval.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
intros.
(* Goal: @eq mpred (mapsto sh (Tpointer t noattr) p nullval) (mapsto sh size_t p nullval) *)
unfold mapsto, size_t.
(* Goal: @eq mpred (mapsto sh (Tint I32 Unsigned noattr) v1 v2) (mapsto sh (Tint I32 Signed noattr) v1 v2) *)
destruct p; try reflexivity.
(* Goal: @eq mpred match access_mode (Tpointer t noattr) with | By_value ch => if type_is_volatile (Tpointer t noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tpointer t noattr) nullval)) (address_mapsto ch nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk ch) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end match access_mode (if Archi.ptr64 then Tlong Unsigned noattr else Tint I32 Unsigned noattr) with | By_value ch => if type_is_volatile (if Archi.ptr64 then Tlong Unsigned noattr else Tint I32 Unsigned noattr) then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (if Archi.ptr64 then Tlong Unsigned noattr else Tint I32 Unsigned noattr) nullval)) (address_mapsto ch nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (if Archi.ptr64 then Tlong Unsigned noattr else Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk ch) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk ch)) | By_reference => @FF rmap ag_rmap | By_copy => @FF rmap ag_rmap | By_nothing => @FF rmap ag_rmap end *)
destruct Archi.ptr64 eqn:Hp.
*
(* Goal: @eq mpred (if readable_share_dec sh then @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec sh (@pair block Z b i)) (VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH)))) else nonlock_permission_bytes sh (@pair block Z b i) (Z.of_nat (S n))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (if false then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i)))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk Mint8unsigned) (Ptrofs.unsigned (Ptrofs.repr i))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))) (size_chunk Mint8unsigned))) (if readable_share_dec sh then VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH))) else nonlock_permission_bytes sh (@pair block Z b (Z.add i (Zpos xH))) (Z.of_nat n))) *)
simpl access_mode; cbv beta iota.
(* Goal: @eq mpred (if readable_share_dec sh then @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec sh (@pair block Z b i)) (VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH)))) else nonlock_permission_bytes sh (@pair block Z b i) (Z.of_nat (S n))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (if false then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i)))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk Mint8unsigned) (Ptrofs.unsigned (Ptrofs.repr i))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))) (size_chunk Mint8unsigned))) (if readable_share_dec sh then VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH))) else nonlock_permission_bytes sh (@pair block Z b (Z.add i (Zpos xH))) (Z.of_nat n))) *)
simpl type_is_volatile;  cbv beta iota.
(* Goal: @eq mpred (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tpointer t noattr) nullval)) (address_mapsto Mptr nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mptr v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mptr) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mptr))) (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I32 Unsigned noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) *)
unfold Mptr; rewrite Hp. 
(* Goal: @eq mpred (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tpointer t noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I32 Unsigned noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) *)
if_tac.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
rewrite !prop_true_andp by auto.
(* Goal: @eq Prop (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) *)
f_equal.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
rewrite prop_true_andp; auto.
(* Goal: tc_val (Tint I32 Unsigned noattr) nullval *)
(* Goal: @eq mpred (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) *)
unfold nullval;rewrite Hp; apply I.
(* Goal: @eq Prop (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) *)
f_equal.
(* Goal: @eq Prop (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) *)
f_equal.
(* Goal: @eq Prop (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) *)
f_equal.
apply prop_ext; split; intros _ _;
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
unfold nullval; rewrite Hp; hnf; auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
simple_if_tac; simpl; rewrite Hp; auto.
*
(* Goal: @eq mpred (if readable_share_dec sh then @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec sh (@pair block Z b i)) (VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH)))) else nonlock_permission_bytes sh (@pair block Z b i) (Z.of_nat (S n))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (if false then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i)))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk Mint8unsigned) (Ptrofs.unsigned (Ptrofs.repr i))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))) (size_chunk Mint8unsigned))) (if readable_share_dec sh then VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH))) else nonlock_permission_bytes sh (@pair block Z b (Z.add i (Zpos xH))) (Z.of_nat n))) *)
simpl access_mode; cbv beta iota.
(* Goal: @eq mpred (if readable_share_dec sh then @sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (VALspec sh (@pair block Z b i)) (VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH)))) else nonlock_permission_bytes sh (@pair block Z b i) (Z.of_nat (S n))) (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap (if false then @FF rmap ag_rmap else if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I8 Unsigned noattr) Vundef)) (address_mapsto Mint8unsigned Vundef sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val Vundef Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint8unsigned v2' sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i)))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I8 Unsigned noattr) Vundef) (Z.divide (align_chunk Mint8unsigned) (Ptrofs.unsigned (Ptrofs.repr i))))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned (Ptrofs.repr i))) (size_chunk Mint8unsigned))) (if readable_share_dec sh then VALspec_range (Z.of_nat n) sh (@pair block Z b (Z.add i (Zpos xH))) else nonlock_permission_bytes sh (@pair block Z b (Z.add i (Zpos xH))) (Z.of_nat n))) *)
simpl type_is_volatile;  cbv beta iota.
(* Goal: @eq mpred (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tpointer t noattr) nullval)) (address_mapsto Mptr nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mptr v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mptr) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mptr))) (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I32 Unsigned noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) *)
unfold Mptr; rewrite Hp. 
(* Goal: @eq mpred (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tpointer t noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) (if readable_share_dec sh then @orp rmap ag_rmap (@andp rmap ag_rmap (@prop rmap ag_rmap (tc_val (Tint I32 Unsigned noattr) nullval)) (address_mapsto Mint32 nullval sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp rmap ag_rmap (@prop rmap ag_rmap (@eq val nullval Vundef)) (@exp rmap ag_rmap val (fun v2' : val => address_mapsto Mint32 v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) *)
if_tac.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
rewrite !prop_true_andp by auto.
(* Goal: @eq Prop (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) *)
f_equal.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
rewrite prop_true_andp; auto.
(* Goal: tc_val (Tint I32 Unsigned noattr) nullval *)
(* Goal: @eq mpred (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) (@andp rmap ag_rmap (@prop rmap ag_rmap (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i)))) (nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk Mint32))) *)
unfold nullval;rewrite Hp; apply I.
(* Goal: @eq Prop (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) *)
f_equal.
(* Goal: @eq Prop (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) *)
f_equal.
(* Goal: @eq Prop (and (tc_val' (Tpointer t noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) (and (tc_val' (Tint I32 Unsigned noattr) nullval) (Z.divide (align_chunk Mint32) (Ptrofs.unsigned i))) *)
f_equal.
apply prop_ext; split; intros _ _;
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
unfold nullval; rewrite Hp; hnf; auto.
(* Goal: @derives rmap ag_rmap (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) (address_mapsto Mint8unsigned (Vint Int.zero) sh (@pair block Z b ofs')) *)
simple_if_tac; simpl; rewrite Hp; auto.
Qed.

Lemma mapsto_null_mapsto_pointer:
  forall t sh v,
   Archi.ptr64 = false -> 
             mapsto sh (Tint I32 Signed noattr) v nullval =
             mapsto sh (Tpointer t noattr) v nullval.
Proof.
(* Goal: forall (t : type) (sh : Share.t) (v : val) (_ : @eq bool Archi.ptr64 false), @eq mpred (mapsto sh (Tint I32 Signed noattr) v nullval) (mapsto sh (Tpointer t noattr) v nullval) *)
  intros.
  try solve [inversion H];
 (
  unfold mapsto, nullval; rewrite H;
  simpl;
  destruct v; auto; f_equal; auto;
  if_tac;
   [f_equal; f_equal; rewrite andb_false_r;
   unfold is_pointer_or_null; rewrite H;
   apply pred_ext; unfold derives; simpl; tauto
   | f_equal; f_equal;
      unfold tc_val';
      f_equal; simpl; 
      simple_if_tac; simpl; rewrite H; auto;
      apply prop_ext; intuition]).
Qed.
