Require Import VST.veric.base.
Require Import VST.msl.normalize.
Require Import VST.veric.compcert_rmaps.
Require Import VST.msl.msl_standard.
Require Import VST.veric.res_predicates.
Require Import VST.veric.Clight_seplog. (*need Clight_seplog rather than general seplog to ensure availability of 
                                          mapsto and memory_block -maybe move the lemmas using them elsewhere?*)
Require Import VST.veric.tycontext.
Require Import VST.veric.expr2.
Require Import VST.veric.expr_lemmas.

Definition size_compatible {C: compspecs} t p :=
  match p with
  | Vptr b i_ofs => Ptrofs.unsigned i_ofs + sizeof t < Ptrofs.modulus
  | _ => True
  end.

Lemma nonlock_permission_bytes_valid_pointer: forall sh b ofs n i,
  0 <= ofs /\ ofs + n <= Ptrofs.modulus ->
  0 <= i < n ->
  nonidentity sh ->
  nonlock_permission_bytes sh (b, ofs) n |-- valid_pointer (Vptr b (Ptrofs.repr (ofs + i))).
Proof.
(* Goal: forall (sh : share) (b : block) (ofs n i : Z) (_ : and (Z.le Z0 ofs) (Z.lt (Z.add ofs n) Ptrofs.modulus)) (_ : and (Z.le Z0 i) (Z.le i n)) (_ : Z.lt Z0 n) (_ : @nonidentity share Share.Join_ba pa_share sh), @derives rmap ag_rmap (nonlock_permission_bytes sh (@pair block Z b ofs) n) (weak_valid_pointer (Vptr b (Ptrofs.repr (Z.add ofs i)))) *)
  intros.
(* Goal: @derives rmap ag_rmap (nonlock_permission_bytes sh (@pair block Z b ofs) n) (valid_pointer (Vptr b (Ptrofs.repr (Z.add ofs i)))) *)
  unfold nonlock_permission_bytes, valid_pointer.
(* 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 ofs) n) (adr_range_dec (@pair block Z b ofs) n) (fun i : address => @andp rmap ag_rmap (shareat i sh) (nonlockat i)) noat)) noghost) (@orp rmap ag_rmap (valid_pointer' (Vptr b (Ptrofs.repr (Z.add ofs i))) Z0) (valid_pointer' (Vptr b (Ptrofs.repr (Z.add ofs i))) (Zneg xH))) *)
  intros w ?.
(* Goal: @app_pred rmap ag_rmap (@orp rmap ag_rmap (valid_pointer' (Vptr b (Ptrofs.repr (Z.add ofs i))) Z0) (valid_pointer' (Vptr b (Ptrofs.repr (Z.add ofs i))) (Zneg xH))) w *)
  simpl in H2 |- *.
(* Goal: or (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))))) (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))))) *)
  rewrite Ptrofs.unsigned_repr by (unfold Ptrofs.max_unsigned; omega).
(* Goal: or (match resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))))) (match resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))))) *)
  rewrite Z.add_0_r.
(* Goal: or (match resource_at w (@pair block Z b (Z.add ofs i)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add ofs i))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add ofs i))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add ofs i))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add ofs i))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add ofs i))))) (match resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))))) *)
  destruct H2 as [H2 _].
(* Goal: or (match resource_at w (@pair block Z b (Z.add ofs i)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add ofs i))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add ofs i))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add ofs i))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add ofs i))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add ofs i))))) (match resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))))) *)
  specialize (H2 (b, ofs + i)).
(* Goal: match resource_at w (@pair block Z b (Z.add (Z.add ofs n) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Z.add ofs n) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Z.add ofs n) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Z.add ofs n) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Z.add ofs n) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Z.add ofs n) (Zneg xH))))) *)
  if_tac in H2.
  + destruct H2.
    destruct (w @ (b, ofs + i)); inv H2; inv H4; auto.
  + exfalso.
(* Goal: False *)
    simpl in H3.
(* Goal: False *)
    apply H3.
(* Goal: and (@eq block b b) (and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n))) *)
    split; auto.
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
    omega.
Qed.

Lemma VALspec_range_valid_pointer: forall sh b ofs n i,
  0 <= ofs /\ ofs + n <= Ptrofs.modulus ->
  0 <= i < n ->
  VALspec_range n sh (b, ofs) |-- valid_pointer (Vptr b (Ptrofs.repr (ofs + i))).
Proof.
(* Goal: forall (sh : share) (b : block) (ofs n i : Z) (_ : and (Z.le Z0 ofs) (Z.lt (Z.add ofs n) Ptrofs.modulus)) (_ : and (Z.le Z0 i) (Z.le i n)) (_ : Z.lt Z0 n) (_ : @nonidentity share Share.Join_ba pa_share sh), @derives rmap ag_rmap (nonlock_permission_bytes sh (@pair block Z b ofs) n) (weak_valid_pointer (Vptr b (Ptrofs.repr (Z.add ofs i)))) *)
  intros.
(* Goal: @derives rmap ag_rmap (VALspec_range n sh (@pair block Z b ofs)) (valid_pointer (Vptr b (Ptrofs.repr (Z.add ofs i)))) *)
  unfold VALspec_range, valid_pointer.
(* 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 ofs) n) (adr_range_dec (@pair block Z b ofs) n) (fun i : address => @andp rmap ag_rmap (shareat i sh) (nonlockat i)) noat)) noghost) (@orp rmap ag_rmap (valid_pointer' (Vptr b (Ptrofs.repr (Z.add ofs i))) Z0) (valid_pointer' (Vptr b (Ptrofs.repr (Z.add ofs i))) (Zneg xH))) *)
  intros w ?.
(* Goal: @app_pred rmap ag_rmap (valid_pointer' (Vptr b (Ptrofs.repr (Z.add ofs i))) Z0) w *)
  simpl in H1 |- *.
(* Goal: or (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))))) (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))))) *)
  rewrite Ptrofs.unsigned_repr by (unfold Ptrofs.max_unsigned; omega).
(* Goal: or (match resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))))) (match resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))))) *)
  rewrite Z.add_0_r.
(* Goal: match resource_at w (@pair block Z b (Z.add ofs i)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add ofs i))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add ofs i))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add ofs i))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add ofs i))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add ofs i)))) *)
  destruct H1 as [H1 _].
  specialize (H1 (b, ofs + i)).
(* Goal: match resource_at w (@pair block Z b (Z.add ofs i)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add ofs i))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add ofs i))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add ofs i))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add ofs i))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add ofs i)))) *)
  if_tac in H1.
  + destruct H1 as [? [? ?]].
(* Goal: match resource_at w (@pair block Z b (Z.add ofs i)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add ofs i))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add ofs i))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add ofs i))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add ofs i))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add ofs i)))) *)
    rewrite H1; auto.
  + exfalso.
(* Goal: False *)
    simpl in H2.
(* Goal: False *)
    apply H2.
(* Goal: and (@eq block b b) (and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n))) *)
    split; auto.
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
    omega.
Qed.

Lemma address_mapsto_valid_pointer: forall ch v sh b ofs i,
  0 <= ofs /\ ofs + size_chunk ch <= Ptrofs.modulus ->
  0 <= i < size_chunk ch ->
  address_mapsto ch v sh (b, ofs) |-- valid_pointer (Vptr b (Ptrofs.repr (ofs + i))).
Proof.
(* Goal: forall (sh : share) (b : block) (ofs n i : Z) (_ : and (Z.le Z0 ofs) (Z.lt (Z.add ofs n) Ptrofs.modulus)) (_ : and (Z.le Z0 i) (Z.le i n)) (_ : Z.lt Z0 n) (_ : @nonidentity share Share.Join_ba pa_share sh), @derives rmap ag_rmap (nonlock_permission_bytes sh (@pair block Z b ofs) n) (weak_valid_pointer (Vptr b (Ptrofs.repr (Z.add ofs i)))) *)
  intros.
(* Goal: @derives rmap ag_rmap (address_mapsto ch v sh (@pair block Z b ofs)) (valid_pointer (Vptr b (Ptrofs.repr (Z.add ofs i)))) *)
  eapply derives_trans; [apply address_mapsto_VALspec_range |].
(* Goal: @derives rmap ag_rmap (VALspec_range (size_chunk ch) sh (@pair block Z b ofs)) (valid_pointer (Vptr b (Ptrofs.repr (Z.add ofs i)))) *)
  apply VALspec_range_valid_pointer; auto.
Qed.

Lemma mapsto_valid_pointer: forall {cs: compspecs} sh t p v i,
  size_compatible t p ->
  0 <= i < sizeof t ->
  nonidentity sh ->
  mapsto sh t p v |-- valid_pointer (offset_val i p).
Proof.
(* Goal: forall (sh : share) (b : block) (ofs n i : Z) (_ : and (Z.le Z0 ofs) (Z.lt (Z.add ofs n) Ptrofs.modulus)) (_ : and (Z.le Z0 i) (Z.le i n)) (_ : Z.lt Z0 n) (_ : @nonidentity share Share.Join_ba pa_share sh), @derives rmap ag_rmap (nonlock_permission_bytes sh (@pair block Z b ofs) n) (weak_valid_pointer (Vptr b (Ptrofs.repr (Z.add ofs i)))) *)
  intros.
  unfold mapsto.
  destruct (access_mode t) eqn:?H; auto.
  destruct (type_is_volatile t); auto.
  destruct p; auto.
  destruct (readable_share_dec sh).
  + apply orp_left; apply andp_left2.
    - simpl in H.
      erewrite size_chunk_sizeof in H by eauto.
      erewrite size_chunk_sizeof in H0 by eauto.
      pose proof Ptrofs.unsigned_range i0.
      apply address_mapsto_valid_pointer.
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
      * omega.
(* Goal: or (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))))) (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))))) *)
      * rewrite Ptrofs.unsigned_repr by (unfold Ptrofs.max_unsigned; omega).
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
        omega.
    - apply exp_left; intro.
      simpl in H.
      erewrite size_chunk_sizeof in H by eauto.
      erewrite size_chunk_sizeof in H0 by eauto.
      pose proof Ptrofs.unsigned_range i0.
      apply address_mapsto_valid_pointer.
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
      * omega.
(* Goal: or (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))))) (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))))) *)
      * rewrite Ptrofs.unsigned_repr by (unfold Ptrofs.max_unsigned; omega).
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
        omega.
  + simpl in H.
    erewrite size_chunk_sizeof in H by eauto.
    erewrite size_chunk_sizeof in H0 by eauto.
    pose proof Ptrofs.unsigned_range i0.
    apply andp_left2.
    apply nonlock_permission_bytes_valid_pointer.
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
    - omega.
(* Goal: or (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))))) (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))))) *)
    - rewrite Ptrofs.unsigned_repr by (unfold Ptrofs.max_unsigned; omega).
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
      omega.
    - auto.
Qed.

Lemma memory_block_valid_pointer: forall {cs: compspecs} sh n p i,
  0 <= i < n ->
  nonidentity sh ->
  memory_block sh n p |-- valid_pointer (offset_val i p).
Proof.
(* Goal: forall (sh : share) (b : block) (ofs n i : Z) (_ : and (Z.le Z0 ofs) (Z.lt (Z.add ofs n) Ptrofs.modulus)) (_ : and (Z.le Z0 i) (Z.le i n)) (_ : Z.lt Z0 n) (_ : @nonidentity share Share.Join_ba pa_share sh), @derives rmap ag_rmap (nonlock_permission_bytes sh (@pair block Z b ofs) n) (weak_valid_pointer (Vptr b (Ptrofs.repr (Z.add ofs i)))) *)
  intros.
  unfold memory_block.
  destruct p; auto.
  normalize.
  pose proof Ptrofs.unsigned_range i0.
  rewrite memory_block'_eq.
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
  2: omega.
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
  2: rewrite Z2Nat.id; omega.
  unfold memory_block'_alt.
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
  rewrite Z2Nat.id by omega.
  destruct (readable_share_dec sh).
  + apply VALspec_range_valid_pointer.
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
    - split; try omega.
(* Goal: or (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))))) (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))))) *)
    - rewrite Ptrofs.unsigned_repr by (unfold Ptrofs.max_unsigned; omega).
      auto.
  + apply nonlock_permission_bytes_valid_pointer.
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
    - omega.
(* Goal: or (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))))) (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))))) *)
    - rewrite Ptrofs.unsigned_repr by (unfold Ptrofs.max_unsigned; omega).
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
      omega.
    - auto.
Qed.

Lemma VALspec_range_weak_valid_pointer: forall sh b ofs n i,
  0 <= ofs /\ ofs + n < Ptrofs.modulus -> 0 <= i <= n -> 0 < n ->
  VALspec_range n sh (b, ofs) |-- weak_valid_pointer (Vptr b (Ptrofs.repr (ofs + i))).
Proof.
(* Goal: forall (sh : share) (b : block) (ofs n i : Z) (_ : and (Z.le Z0 ofs) (Z.lt (Z.add ofs n) Ptrofs.modulus)) (_ : and (Z.le Z0 i) (Z.le i n)) (_ : Z.lt Z0 n) (_ : @nonidentity share Share.Join_ba pa_share sh), @derives rmap ag_rmap (nonlock_permission_bytes sh (@pair block Z b ofs) n) (weak_valid_pointer (Vptr b (Ptrofs.repr (Z.add ofs i)))) *)
  intros. unfold VALspec_range, weak_valid_pointer. intros w ?. simpl in H2 |- *.
(* Goal: or (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))))) (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))))) *)
  rewrite Ptrofs.unsigned_repr by (unfold Ptrofs.max_unsigned; omega).
(* Goal: or (match resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))))) (match resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))))) *)
  rewrite Z.add_0_r. destruct H2 as [H2 _].
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
  assert (0 <= i < n \/ i = n) by omega. destruct H3.
(* Goal: or (match resource_at w (@pair block Z b (Z.add ofs i)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add ofs i))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add ofs i))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add ofs i))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add ofs i))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add ofs i))))) (match resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))))) *)
  - specialize (H2 (b, ofs + i)). if_tac in H2.
    + left. destruct H2 as [? [? ?]]. rewrite H2; auto.
    + exfalso. simpl in H4. apply H4. split; auto. omega.
(* Goal: match resource_at w (@pair block Z b (Z.add (Z.add ofs n) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Z.add ofs n) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Z.add ofs n) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Z.add ofs n) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Z.add ofs n) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Z.add ofs n) (Zneg xH))))) *)
  - subst i. specialize (H2 (b, ofs + n - 1)). right. if_tac in H2.
    + destruct H2 as [? [? ?]]. replace (ofs + n + -1) with (ofs + n - 1) by omega.
      rewrite H2; auto.
    + exfalso. simpl in H3. apply H3. split; auto. omega.
Qed.

Lemma nonlock_permission_bytes_weak_valid_pointer: forall sh b ofs n i,
  0 <= ofs /\ ofs + n < Ptrofs.modulus -> 0 <= i <= n -> 0 < n -> nonidentity sh ->
  nonlock_permission_bytes sh (b, ofs) n |--
                           weak_valid_pointer (Vptr b (Ptrofs.repr (ofs + i))).
Proof.
(* Goal: forall (sh : share) (b : block) (ofs n i : Z) (_ : and (Z.le Z0 ofs) (Z.lt (Z.add ofs n) Ptrofs.modulus)) (_ : and (Z.le Z0 i) (Z.le i n)) (_ : Z.lt Z0 n) (_ : @nonidentity share Share.Join_ba pa_share sh), @derives rmap ag_rmap (nonlock_permission_bytes sh (@pair block Z b ofs) n) (weak_valid_pointer (Vptr b (Ptrofs.repr (Z.add ofs i)))) *)
  intros. unfold nonlock_permission_bytes, weak_valid_pointer.
(* 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 ofs) n) (adr_range_dec (@pair block Z b ofs) n) (fun i : address => @andp rmap ag_rmap (shareat i sh) (nonlockat i)) noat)) noghost) (@orp rmap ag_rmap (valid_pointer' (Vptr b (Ptrofs.repr (Z.add ofs i))) Z0) (valid_pointer' (Vptr b (Ptrofs.repr (Z.add ofs i))) (Zneg xH))) *)
  intros w ?. simpl in H3 |- *.
(* Goal: or (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))))) (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))))) *)
  rewrite Ptrofs.unsigned_repr by (unfold Ptrofs.max_unsigned; omega).
(* Goal: or (match resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Z.add ofs i) Z0))))) (match resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Z.add ofs i) (Zneg xH)))))) *)
  rewrite Z.add_0_r. destruct H3 as [H3 _].
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
  assert (0 <= i < n \/ i = n) by omega. destruct H4.
  - left. specialize (H3 (b, ofs + i)). if_tac in H3.
    + destruct H3. destruct (w @ (b, ofs + i)); inv H3; auto.
    + exfalso. simpl in H5. apply H5. split; auto. omega.
  - subst i. right. specialize (H3 (b, ofs + n - 1)). if_tac in H3.
    + destruct H3. replace (ofs + n + -1) with (ofs + n - 1) by omega.
      destruct (w @ (b, ofs + n - 1)); inv H3; auto.
    + exfalso. simpl in H4. apply H4. split; auto. omega.
Qed.

Lemma memory_block_weak_valid_pointer: forall {cs: compspecs} sh n p i,
  0 <= i <= n -> 0 < n -> nonidentity sh ->
  memory_block sh n p |-- weak_valid_pointer (offset_val i p).
Proof.
(* Goal: forall (sh : share) (b : block) (ofs n i : Z) (_ : and (Z.le Z0 ofs) (Z.lt (Z.add ofs n) Ptrofs.modulus)) (_ : and (Z.le Z0 i) (Z.le i n)) (_ : Z.lt Z0 n) (_ : @nonidentity share Share.Join_ba pa_share sh), @derives rmap ag_rmap (nonlock_permission_bytes sh (@pair block Z b ofs) n) (weak_valid_pointer (Vptr b (Ptrofs.repr (Z.add ofs i)))) *)
  intros. unfold memory_block. destruct p; auto. normalize.
  pose proof Ptrofs.unsigned_range i0. rewrite memory_block'_eq.
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
  2: omega. 2: rewrite Z2Nat.id; omega. unfold memory_block'_alt.
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
  rewrite Z2Nat.id by omega. destruct (readable_share_dec sh).
  + apply VALspec_range_weak_valid_pointer; auto.
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
    - split; try omega.
(* Goal: or (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))))) (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))))) *)
    - rewrite Ptrofs.unsigned_repr by (unfold Ptrofs.max_unsigned; omega). auto.
  + apply nonlock_permission_bytes_weak_valid_pointer; auto.
(* Goal: and (Z.le ofs (Z.sub (Z.add ofs n) (Zpos xH))) (Z.lt (Z.sub (Z.add ofs n) (Zpos xH)) (Z.add ofs n)) *)
    - omega.
(* Goal: or (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0)) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) Z0))))) (match resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH))) as anonymous' return (forall _ : @eq resource anonymous' (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))), Prop) with | NO sh wildcard' => fun _ : @eq resource (NO sh wildcard') (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => @nonidentity Share.t Share.Join_ba pa_share sh | YES wildcard' wildcard'0 wildcard'1 pp => fun _ : @eq resource (YES wildcard' wildcard'0 wildcard'1 pp) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => True | PURE k p => fun _ : @eq resource (PURE k p) (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))) => False end (@eq_refl resource (resource_at w (@pair block Z b (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add ofs i))) (Zneg xH)))))) *)
    - rewrite Ptrofs.unsigned_repr by (unfold Ptrofs.max_unsigned; omega). omega.
Qed.
