Require Import VST.floyd.base2.
Require Import VST.floyd.client_lemmas.
Require Import VST.floyd.nested_pred_lemmas.

Local Open Scope logic.

(******************************************

Basic lemmas about local_facts, isptr, offset_zero

******************************************)

Lemma local_facts_isptr: forall P Q (p: val), P p |-- !! Q -> (Q -> isptr p) -> P p = !! (isptr p) && P p.
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq mpred (P p) (@andp mpred Nveric (@prop mpred Nveric (isptr p)) (P p)) *)
  rewrite andp_comm; apply add_andp.
(* Goal: @derives mpred Nveric (P p) (@prop mpred Nveric (isptr p)) *)
  eapply derives_trans; [eassumption |].
(* Goal: @derives mpred Nveric (@prop mpred Nveric Q) (@prop mpred Nveric (isptr p)) *)
  apply prop_derives; auto.
Qed.

Lemma local_facts_offset_zero: forall P, (forall p, P p |-- !! isptr p) -> (forall p, P p = P (offset_val 0 p)).
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
  pose proof (H p).
  pose proof (H Vundef).
  destruct p; simpl in *; apply pred_ext; normalize.
all: try solve [eapply derives_trans; [eassumption | normalize]].
Qed.

(******************************************

Lemmas about mapsto and mapsto_.

******************************************)

Lemma mapsto_local_facts:
  forall sh t v1 v2,  mapsto sh t v1 v2 |-- !! (isptr v1 /\ tc_val' t v2).
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @derives mpred Nveric (mapsto sh t v1 v2) (@prop mpred Nveric (and (isptr v1) (tc_val' t v2))) *)
  rewrite prop_and.
(* Goal: @derives mpred Nveric (mapsto sh t v1 v2) (@andp mpred Nveric (@prop mpred Nveric (isptr v1)) (@prop mpred Nveric (tc_val' t v2))) *)
  apply andp_right.
  + unfold mapsto.
(* Goal: @derives mpred Nveric match access_mode t with | By_value ch => if type_is_volatile t then @FF mpred Nveric else match v1 with | Vundef => @FF mpred Nveric | Vint i => @FF mpred Nveric | Vlong i => @FF mpred Nveric | Vfloat f => @FF mpred Nveric | Vsingle f => @FF mpred Nveric | Vptr b ofs => if readable_share_dec sh then @orp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (tc_val t v2)) (res_predicates.address_mapsto ch v2 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v2 Vundef)) (@exp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric val (fun v2' : val => res_predicates.address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (and (tc_val' t v2) (Z.divide (align_chunk ch) (Ptrofs.unsigned ofs)))) (res_predicates.nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk ch)) end | By_reference => @FF mpred Nveric | By_copy => @FF mpred Nveric | By_nothing => @FF mpred Nveric end (@prop mpred Nveric (isptr v1)) *)
    destruct (access_mode t); try apply FF_left.
(* Goal: @derives mpred Nveric (if type_is_volatile t then @FF mpred Nveric else match v1 with | Vundef => @FF mpred Nveric | Vint i => @FF mpred Nveric | Vlong i => @FF mpred Nveric | Vfloat f => @FF mpred Nveric | Vsingle f => @FF mpred Nveric | Vptr b ofs => if readable_share_dec sh then @orp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (tc_val t v2)) (res_predicates.address_mapsto m v2 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v2 Vundef)) (@exp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric val (fun v2' : val => res_predicates.address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (and (tc_val' t v2) (Z.divide (align_chunk m) (Ptrofs.unsigned ofs)))) (res_predicates.nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk m)) end) (@prop mpred Nveric (isptr v1)) *)
    destruct (type_is_volatile t); try apply FF_left.
(* Goal: @derives mpred Nveric match v1 with | Vundef => @FF mpred Nveric | Vint i => @FF mpred Nveric | Vlong i => @FF mpred Nveric | Vfloat f => @FF mpred Nveric | Vsingle f => @FF mpred Nveric | Vptr b ofs => if readable_share_dec sh then @orp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (tc_val t v2)) (res_predicates.address_mapsto m v2 sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v2 Vundef)) (@exp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric val (fun v2' : val => res_predicates.address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (and (tc_val' t v2) (Z.divide (align_chunk m) (Ptrofs.unsigned ofs)))) (res_predicates.nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk m)) end (@prop mpred Nveric (isptr v1)) *)
    destruct v1; try apply FF_left.
(* Goal: @derives mpred Nveric (if readable_share_dec sh then @orp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (tc_val t v2)) (res_predicates.address_mapsto m v2 sh (@pair block Z b (Ptrofs.unsigned i)))) (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v2 Vundef)) (@exp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric val (fun v2' : val => res_predicates.address_mapsto m v2' sh (@pair block Z b (Ptrofs.unsigned i))))) else @andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (and (tc_val' t v2) (Z.divide (align_chunk m) (Ptrofs.unsigned i)))) (res_predicates.nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned i)) (size_chunk m))) (@prop mpred Nveric (isptr (Vptr b i))) *)
    apply prop_right; split; auto; apply Coq.Init.Logic.I.
  + apply mapsto_tc_val'.
Qed.

Lemma mapsto__local_facts:
  forall sh t v1, mapsto_ sh t v1 |-- !! isptr v1.
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @derives mpred Nveric (mapsto sh t p v2) (@prop mpred Nveric (isptr p)) *)
  eapply derives_trans; [apply mapsto_local_facts |].
(* Goal: @derives mpred Nveric (@prop mpred Nveric (and (isptr v1) (tc_val' t Vundef))) (@prop mpred Nveric (isptr v1)) *)
  apply prop_derives; tauto.
Qed.
Hint Resolve mapsto_local_facts mapsto__local_facts : saturate_local.

Lemma mapsto_offset_zero:
  forall sh t v1 v2, mapsto sh t v1 v2 = mapsto sh t (offset_val 0 v1) v2.
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq mpred (mapsto sh t v1 v2) (mapsto sh t (offset_val Z0 v1) v2) *)
  change (mapsto sh t (offset_val 0 v1) v2) with ((fun v0 => mapsto sh t v0 v2) (offset_val 0 v1)).
(* Goal: @eq mpred (memory_block sh n v) (memory_block sh n (offset_val Z0 v)) *)
  rewrite <- local_facts_offset_zero.
(* Goal: @eq val (Vptr b (Ptrofs.add i (Ptrofs.repr (Z.add pos be)))) (Vptr b (Ptrofs.add i (Ptrofs.repr (Z.add pos be)))) *)
  reflexivity.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
  eapply derives_trans; [  apply mapsto_local_facts | ].
(* Goal: @eq mpred (P p) (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (P p)) *)
  normalize.
Qed.

Lemma mapsto__offset_zero:
  forall sh t v1, mapsto_ sh t v1 = mapsto_ sh t (offset_val 0 v1).
Proof.
(* Goal: forall (sh : Share.t) (t : type) (v1 : val), @eq mpred (mapsto_ sh t v1) (mapsto_ sh t (offset_val Z0 v1)) *)
  unfold mapsto_.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq mpred (mapsto sh t v1 Vundef) (mapsto sh t (offset_val Z0 v1) Vundef) *)
  apply mapsto_offset_zero.
Qed.

Lemma mapsto_isptr: forall sh t v1 v2, mapsto sh t v1 v2 = !! (isptr v1) && mapsto sh t v1 v2.
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
  change (mapsto sh t v1 v2) with ((fun v1 => mapsto sh t v1 v2) v1).
  eapply local_facts_isptr.
  + apply mapsto_local_facts.
  + tauto.
Qed.

Lemma mapsto__isptr: forall sh t v1, mapsto_ sh t v1 = !! (isptr v1) && mapsto_ sh t v1.
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
  eapply local_facts_isptr.
  + apply mapsto_local_facts.
  + tauto.
Qed.

(******************************************

Lemmas about memory_block

******************************************)

Hint Rewrite memory_block_zero_Vptr: norm.

Definition size_compatible' (n: Z) (p: val) :=
match p with
| Vundef => True
| Vint _ => True
| Vlong _ => True
| Vfloat _ => True
| Vsingle _ => True
| Vptr _ i_ofs => Ptrofs.unsigned i_ofs + n < Ptrofs.modulus
end.

Lemma memory_block_local_facts: forall sh n p, 
  memory_block sh n p |-- !! (isptr p /\ size_compatible' n p).
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @derives mpred Nveric (memory_block sh n p) (@prop mpred Nveric (and (isptr p) (size_compatible' n p))) *)
   unfold memory_block.
(* Goal: @eq mpred (P p) (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (P p)) *)
  destruct p; simpl; normalize. apply prop_right;split; auto.
Qed.

Hint Resolve memory_block_local_facts : saturate_local.

Lemma memory_block_offset_zero:
  forall sh n v, memory_block sh n v = memory_block sh n (offset_val 0 v).
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq mpred (memory_block sh n v) (memory_block sh n (offset_val Z0 v)) *)
  rewrite <- local_facts_offset_zero.
(* Goal: @eq val (Vptr b (Ptrofs.add i (Ptrofs.repr (Z.add pos be)))) (Vptr b (Ptrofs.add i (Ptrofs.repr (Z.add pos be)))) *)
  reflexivity.
(* Goal: @eq mpred (P p) (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (P p)) *)
  intro. eapply derives_trans;[ apply memory_block_local_facts | ]. normalize.
Qed.

Lemma memory_block_isptr: forall sh n p, memory_block sh n p = !!(isptr p) && memory_block sh n p.
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
  eapply local_facts_isptr.
  + apply memory_block_local_facts.
  + intuition.
Qed.

Lemma memory_block_zero: forall sh p, memory_block sh 0 p = !! isptr p && emp.
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq mpred (memory_block sh Z0 p) (@andp mpred Nveric (@prop mpred Nveric (isptr p)) (@emp mpred Nveric Sveric)) *)
  rewrite memory_block_isptr.
  destruct p;
  try rewrite memory_block_zero_Vptr;
  simpl;
  change (!!False) with FF;
  repeat rewrite FF_andp;
(* Goal: Z.divide (align_chunk ch) (Ptrofs.unsigned i) *)
  auto.
Qed.

Lemma access_mode_by_value: forall t, type_is_by_value t = true -> exists ch, access_mode t = By_value ch.
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @ex memory_chunk (fun ch : memory_chunk => @eq mode (access_mode t) (By_value ch)) *)
  assert (forall ch', exists ch, By_value ch' = By_value ch).
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
    intros. exists ch'. reflexivity.
(* Goal: @ex memory_chunk (fun ch : memory_chunk => @eq mode (access_mode t) (By_value ch)) *)
  destruct t; inversion H; simpl.
  - destruct i, s; apply H0.
  - apply H0.
  - destruct f; apply H0.
  - apply H0.
Qed.

Lemma mapsto_by_value: forall sh t p v, mapsto sh t p v = !! (type_is_by_value t = true) && mapsto sh t p v.
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq mpred (P p) (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (P p)) *)
  apply pred_ext; normalize.
(* Goal: @derives mpred Nveric (mapsto sh t p v) (@andp mpred Nveric (@prop mpred Nveric (@eq bool (type_is_by_value t) true)) (mapsto sh t p v)) *)
  apply andp_right; [|cancel].
(* Goal: @derives mpred Nveric (mapsto sh t p v) (@prop mpred Nveric (@eq bool (type_is_by_value t) true)) *)
  unfold mapsto.
(* Goal: @derives mpred Nveric match access_mode t with | By_value ch => if type_is_volatile t then @FF mpred Nveric else match p with | Vundef => @FF mpred Nveric | Vint i => @FF mpred Nveric | Vlong i => @FF mpred Nveric | Vfloat f => @FF mpred Nveric | Vsingle f => @FF mpred Nveric | Vptr b ofs => if readable_share_dec sh then @orp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (tc_val t v)) (res_predicates.address_mapsto ch v sh (@pair block Z b (Ptrofs.unsigned ofs)))) (@andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@eq val v Vundef)) (@exp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric val (fun v2' : val => res_predicates.address_mapsto ch v2' sh (@pair block Z b (Ptrofs.unsigned ofs))))) else @andp (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (@prop (@predicates_hered.pred compcert_rmaps.RML.R.rmap compcert_rmaps.RML.R.ag_rmap) Nveric (and (tc_val' t v) (Z.divide (align_chunk ch) (Ptrofs.unsigned ofs)))) (res_predicates.nonlock_permission_bytes sh (@pair block Z b (Ptrofs.unsigned ofs)) (size_chunk ch)) end | By_reference => @FF mpred Nveric | By_copy => @FF mpred Nveric | By_nothing => @FF mpred Nveric end (@prop mpred Nveric (@eq bool (type_is_by_value t) true)) *)
  destruct t; simpl; normalize; try (apply prop_right; auto).
Qed.

(******************************************

Lemmas from veric

******************************************)

Section COMPSPECS.

Context {cs: compspecs}.

Lemma memory_block_mapsto_:
  forall sh t p,
   type_is_by_value t = true ->
   type_is_volatile t = false ->
   size_compatible t p ->
   align_compatible t p ->
   memory_block sh (sizeof t) p = mapsto_ sh t p.
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq mpred (memory_block sh (@sizeof (@cenv_cs cs) t) p) (mapsto sh t p v) *)
  assert (isptr p \/ ~isptr p) by (destruct p; simpl; auto).
(* Goal: @eq mpred (memory_block sh (@sizeof (@cenv_cs cs) t) p) (mapsto_ sh t p) *)
  destruct H3. destruct p; try contradiction.
  + simpl in H1, H2.
(* Goal: @eq mpred (memory_block sh (@sizeof (@cenv_cs cs) t) (Vptr b i)) (mapsto_ sh t (Vptr b i)) *)
    destruct (access_mode_by_value _ H) as [ch ?].
    unfold sizeof in *; erewrite size_chunk_sizeof in H1 |- * by eauto.
(* Goal: @eq mpred (memory_block sh (size_chunk ch) (Vptr b i)) (mapsto_ sh t (Vptr b i)) *)
    rewrite mapsto_memory_block.mapsto__memory_block with (ch := ch); auto.
(* Goal: Z.divide (align_chunk ch) (Ptrofs.unsigned i) *)
    eapply align_compatible_rec_by_value_inv in H2; [| eassumption].
(* Goal: Z.divide (align_chunk ch) (Ptrofs.unsigned i) *)
    auto.
  + apply pred_ext; saturate_local; try contradiction.
Qed.

Lemma nonreadable_memory_block_mapsto: forall sh p t v,
  ~ readable_share sh ->
  type_is_by_value t = true ->
  type_is_volatile t = false ->
  size_compatible t p ->
  align_compatible t p ->
  tc_val' t v ->
  memory_block sh (sizeof t) p = mapsto sh t p v.
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq mpred (memory_block sh (@sizeof (@cenv_cs cs) t) p) (mapsto sh t p v) *)
  apply access_mode_by_value in H0; destruct H0 as [ch ?].
(* Goal: @eq mpred (memory_block sh (@sizeof (@cenv_cs cs) t) p) (mapsto sh t p v) *)
  assert (isptr p \/ ~isptr p) by (destruct p; simpl; auto).
(* Goal: @eq mpred (memory_block sh (@sizeof (@cenv_cs cs) t) p) (mapsto sh t p v) *)
(* Goal: @eq mpred (memory_block sh (@sizeof (@cenv_cs cs) t) p) (mapsto sh t p v) *)
  destruct H5. destruct p; try contradiction.
  + simpl in H2, H3.
    erewrite size_chunk_sizeof in H2 |- * by eauto.
(* Goal: Z.divide (align_chunk ch) (Ptrofs.unsigned i) *)
    apply mapsto_memory_block.nonreadable_memory_block_mapsto; auto.
(* Goal: Z.divide (align_chunk ch) (Ptrofs.unsigned i) *)
    eapply align_compatible_rec_by_value_inv in H3; [| eassumption].
(* Goal: Z.divide (align_chunk ch) (Ptrofs.unsigned i) *)
    auto.
  + apply pred_ext; saturate_local; try contradiction.
Qed.

Lemma memory_block_size_compatible:
  forall sh t p,
  memory_block sh (sizeof t) p = 
  !! (size_compatible t p) && memory_block sh (sizeof t) p.
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq mpred (memory_block sh (@sizeof (@cenv_cs cs) t) p) (@andp mpred Nveric (@prop mpred Nveric (@size_compatible cs t p)) (memory_block sh (@sizeof (@cenv_cs cs) t) p)) *)
  unfold memory_block, size_compatible.
(* Goal: @eq mpred (P p) (@sepcon mpred Nveric Sveric (@emp mpred Nveric Sveric) (P p)) *)
  apply pred_ext; destruct p; normalize.
Qed.

Global Opaque memory_block.

End COMPSPECS.

(******************************************

Lemmas about specific types

******************************************)

(* We do these as Hint Extern, instead of Hint Resolve,
  to limit their application and make them fail faster *)

Hint Extern 1 (mapsto _ _ _ _ |-- mapsto _ _ _ _) =>
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (spacer sh be ed p) (x p)) (@sepcon mpred Nveric Sveric (spacer sh be ed p) (x p)) *)
   (simple apply mapsto_mapsto_int32; apply Coq.Init.Logic.I)  : cancel.

Hint Extern 1 (mapsto _ _ _ _ |-- mapsto_ _ _ _) =>
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (spacer sh be ed p) (x p)) (@sepcon mpred Nveric Sveric (spacer sh be ed p) (x p)) *)
   (simple apply mapsto_mapsto__int32; apply Coq.Init.Logic.I)  : cancel.

Hint Extern 1 (mapsto _ _ _ _ |-- mapsto_ _ _ _) =>
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (spacer sh be ed p) (x p)) (@sepcon mpred Nveric Sveric (spacer sh be ed p) (x p)) *)
    (apply mapsto_mapsto_) : cancel.

Hint Extern 1 (mapsto _ _ _ _ |-- mapsto_ _ _ _) =>
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (spacer sh be ed p) (x p)) (@sepcon mpred Nveric Sveric (spacer sh be ed p) (x p)) *)
   (apply mapsto_mapsto__int32)  : cancel.

Hint Extern 1 (mapsto _ _ _ _ |-- mapsto _ _ _ _) =>
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (spacer sh be ed p) (x p)) (@sepcon mpred Nveric Sveric (spacer sh be ed p) (x p)) *)
   (apply mapsto_mapsto_int32)  : cancel.

Hint Extern 0 (legal_alignas_type _ = true) => reflexivity : cancel.

Lemma mapsto_force_ptr: forall sh t v v',
  mapsto sh t (force_ptr v) v' = mapsto sh t v v'.
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
intros.
(* Goal: Z.divide (align_chunk ch) (Ptrofs.unsigned i) *)
destruct v; simpl; auto.
Qed.

Hint Rewrite mapsto_force_ptr: norm.

(******************************************

Definition of at_offset.

at_offset is the elementary definition. All useful lemmas about at_offset will be proved here.

******************************************)

Definition at_offset (P: val -> mpred) (z: Z): val -> mpred :=
 fun v => P (offset_val z v).

Arguments at_offset P z v : simpl never.

Lemma at_offset_eq: forall P z v,
  at_offset P z v = P (offset_val z v).
Proof.
(* Goal: Z.divide (align_chunk ch) (Ptrofs.unsigned i) *)
intros; auto.
Qed.

Lemma lifted_at_offset_eq: forall (P: val -> mpred) z v,
  `(at_offset P z) v = `P (`(offset_val z) v).
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq (lifted (LiftEnviron mpred)) (@liftx (Tarrow val (LiftEnviron mpred)) (at_offset P z : forall _ : val, mpred) v) (@liftx (Tarrow val (LiftEnviron mpred)) P (@liftx (Tarrow val (LiftEnviron val)) (offset_val z : forall _ : val, val) v)) *)
  unfold liftx, lift in *. simpl in *.
(* Goal: @eq (forall _ : environ, mpred) (fun x : environ => at_offset P z (v x)) (fun x : environ => P (offset_val z (v x))) *)
  extensionality p.
(* Goal: @eq mpred (at_offset P z (v p)) (P (offset_val z (v p))) *)
  apply at_offset_eq.
Qed.

Lemma at_offset_eq2: forall pos pos' P,
  forall p, at_offset P (pos + pos') p = at_offset P pos' (offset_val pos p).
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq mpred (at_offset (memory_block sh (Z.sub ed be)) be (Vptr b i)) (memory_block sh (Z.sub ed be) (offset_val be (Vptr b i))) *)
  rewrite at_offset_eq.
(* Goal: @eq mpred (at_offset (memory_block sh (Z.sub ed be)) be (Vptr b i)) (memory_block sh (Z.sub ed be) (offset_val be (Vptr b i))) *)
  rewrite at_offset_eq.
(* Goal: @eq mpred (P (offset_val z (Vptr b (Ptrofs.repr ofs)))) (P (Vptr b (Ptrofs.repr (Z.add ofs z)))) *)
  unfold offset_val.
(* Goal: Z.divide (align_chunk ch) (Ptrofs.unsigned i) *)
  destruct p; auto.
(* Goal: @eq val (Vptr b (Ptrofs.add (Ptrofs.add i (Ptrofs.repr pos)) (Ptrofs.repr be))) (Vptr b (Ptrofs.add i (Ptrofs.repr (Z.add pos be)))) *)
  rewrite ptrofs_add_assoc1.
(* Goal: @eq val (Vptr b (Ptrofs.add i (Ptrofs.repr (Z.add pos be)))) (Vptr b (Ptrofs.add i (Ptrofs.repr (Z.add pos be)))) *)
  reflexivity.
Qed.

Lemma at_offset_eq3: forall P z b ofs,
  at_offset P z (Vptr b (Ptrofs.repr ofs)) = P (Vptr b (Ptrofs.repr (ofs + z))).
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq mpred (at_offset (memory_block sh (Z.sub ed be)) be (Vptr b i)) (memory_block sh (Z.sub ed be) (offset_val be (Vptr b i))) *)
  rewrite at_offset_eq.
(* Goal: @eq mpred (P (offset_val z (Vptr b (Ptrofs.repr ofs)))) (P (Vptr b (Ptrofs.repr (Z.add ofs z)))) *)
  unfold offset_val.
(* Goal: @eq mpred (P (Vptr b (Ptrofs.add (Ptrofs.repr ofs) (Ptrofs.repr z)))) (P (Vptr b (Ptrofs.repr (Z.add ofs z)))) *)
  solve_mod_modulus.
(* Goal: @eq val (Vptr b (Ptrofs.add i (Ptrofs.repr (Z.add pos be)))) (Vptr b (Ptrofs.add i (Ptrofs.repr (Z.add pos be)))) *)
  reflexivity.
Qed.

Lemma at_offset_derives: forall P Q p , (forall p, P p |-- Q p) -> forall pos, at_offset P pos p |-- at_offset Q pos p.
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric (at_offset (memory_block sh (Z.sub ed be)) (Z.add pos be) p) (P (offset_val pos p))) (@sepcon mpred Nveric Sveric (at_offset (memory_block sh (Z.sub ed be)) be (offset_val pos p)) (P (offset_val pos p))) *)
  rewrite !at_offset_eq.
(* Goal: @derives mpred Nveric (P p) (@prop mpred Nveric (isptr p)) *)
  apply H.
Qed.

(******************************************

Definitions of spacer and withspacer

Comment: spacer only has offset_zero property but does not have local_facts
and isptr property.

******************************************)

Definition spacer (sh: share) (be: Z) (ed: Z) : val -> mpred :=
  if Z.eq_dec (ed - be) 0
  then fun _ => emp
  else
    at_offset (memory_block sh (ed - be)) be.
(* Arguments spacer sh be ed / _ . *)

Definition withspacer sh (be: Z) (ed: Z) P (p: val): mpred :=
   if Z.eq_dec (ed - be) 0
   then P p
   else P p * spacer sh be ed p.

Lemma withspacer_spacer: forall sh be ed P p,
   withspacer sh be ed P p = spacer sh be ed p * P p.
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq mpred (withspacer sh be ed P p) (@sepcon mpred Nveric Sveric (spacer sh be ed p) (P p)) *)
  unfold withspacer, spacer.
(* Goal: @eq mpred (if Z.eq_dec (Z.sub ed be) Z0 then P p else @sepcon mpred Nveric Sveric (P p) ((if Z.eq_dec (Z.sub ed be) Z0 then fun _ : val => @emp mpred Nveric Sveric else at_offset (memory_block sh (Z.sub ed be)) be) p)) (@sepcon mpred Nveric Sveric ((if Z.eq_dec (Z.sub ed be) Z0 then fun _ : val => @emp mpred Nveric Sveric else at_offset (memory_block sh (Z.sub ed be)) be) p) (P p)) *)
  if_tac.
  + normalize.
  + simpl; apply sepcon_comm.
Qed.

Lemma withspacer_ramif_Q: forall sh be ed P p,
  withspacer sh be ed P p |-- P p *
    allp ((fun Q => Q p) -* (fun Q => withspacer sh be ed Q p)).
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @derives mpred Nveric (withspacer sh be ed P p) (@sepcon mpred Nveric Sveric (P p) (@allp mpred Nveric (forall _ : val, mpred) (@wand (forall _ : forall _ : val, mpred, mpred) (@LiftNatDed (forall _ : val, mpred) mpred Nveric) (@LiftSepLog (forall _ : val, mpred) mpred Nveric Sveric) (fun Q : forall _ : val, mpred => Q p) (fun Q : forall _ : val, mpred => withspacer sh be ed Q p)))) *)
  apply RAMIF_Q.solve with (spacer sh be ed p).
  + rewrite withspacer_spacer.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (spacer sh be ed p) (x p)) (@sepcon mpred Nveric Sveric (spacer sh be ed p) (x p)) *)
    cancel.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  + intros.
(* Goal: @derives mpred Nveric (withspacer sh be ed P p) (@prop mpred Nveric (isptr p)) *)
    rewrite withspacer_spacer.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (spacer sh be ed p) (x p)) (@sepcon mpred Nveric Sveric (spacer sh be ed p) (x p)) *)
    cancel.
Qed.

Lemma spacer_offset_zero:
  forall sh be ed v, spacer sh be ed v = spacer sh be ed (offset_val 0 v).
Proof.
  intros;
(* Goal: @eq mpred (spacer sh be ed (Vptr b i)) (memory_block sh (Z.sub ed be) (offset_val be (Vptr b i))) *)
  unfold spacer.
  destruct (Z.eq_dec (ed - be) 0);  auto.
  repeat rewrite at_offset_eq;
(* Goal: Z.divide (align_chunk ch) (Ptrofs.unsigned i) *)
  try rewrite offset_offset_val; try  rewrite Int.add_zero_l; auto.
Qed.

Lemma withspacer_add:
  forall sh pos be ed P p,
  withspacer sh (pos + be) (pos + ed) (fun p0 => P (offset_val pos p)) p =
  withspacer sh be ed P (offset_val pos p).
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq mpred (withspacer sh (Z.add pos be) (Z.add pos ed) (fun _ : val => P (offset_val pos p)) p) (withspacer sh be ed P (offset_val pos p)) *)
  rewrite !withspacer_spacer.
(* Goal: @eq mpred (spacer sh be ed (Vptr b i)) (memory_block sh (Z.sub ed be) (offset_val be (Vptr b i))) *)
  unfold spacer.
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric ((if Z.eq_dec (Z.sub (Z.add pos ed) (Z.add pos be)) Z0 then fun _ : val => @emp mpred Nveric Sveric else at_offset (memory_block sh (Z.sub (Z.add pos ed) (Z.add pos be))) (Z.add pos be)) p) (P (offset_val pos p))) (@sepcon mpred Nveric Sveric ((if Z.eq_dec (Z.sub ed be) Z0 then fun _ : val => @emp mpred Nveric Sveric else at_offset (memory_block sh (Z.sub ed be)) be) (offset_val pos p)) (P (offset_val pos p))) *)
  simpl.
  replace (pos + ed - (pos + be)) with (ed - be) by omega.
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric ((if Z.eq_dec (Z.sub ed be) Z0 then fun _ : val => @emp mpred Nveric Sveric else at_offset (memory_block sh (Z.sub ed be)) (Z.add pos be)) p) (P (offset_val pos p))) (@sepcon mpred Nveric Sveric ((if Z.eq_dec (Z.sub ed be) Z0 then fun _ : val => @emp mpred Nveric Sveric else at_offset (memory_block sh (Z.sub ed be)) be) (offset_val pos p)) (P (offset_val pos p))) *)
  if_tac; [reflexivity|].
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric (at_offset (memory_block sh (Z.sub ed be)) (Z.add pos be) p) (P (offset_val pos p))) (@sepcon mpred Nveric Sveric (at_offset (memory_block sh (Z.sub ed be)) be (offset_val pos p)) (P (offset_val pos p))) *)
  rewrite !at_offset_eq.
  replace (offset_val (pos + be) p) with
          (offset_val be (offset_val pos p)).
(* Goal: @eq val (Vptr b (Ptrofs.add i (Ptrofs.repr (Z.add pos be)))) (Vptr b (Ptrofs.add i (Ptrofs.repr (Z.add pos be)))) *)
  reflexivity.
(* Goal: @eq val (Vptr b (Ptrofs.add i (Ptrofs.repr (Z.add pos be)))) (Vptr b (Ptrofs.add i (Ptrofs.repr (Z.add pos be)))) *)
  destruct p; simpl; try reflexivity.
(* Goal: @eq val (Vptr b (Ptrofs.add (Ptrofs.add i (Ptrofs.repr pos)) (Ptrofs.repr be))) (Vptr b (Ptrofs.add i (Ptrofs.repr (Z.add pos be)))) *)
  rewrite ptrofs_add_assoc1.
(* Goal: @eq val (Vptr b (Ptrofs.add i (Ptrofs.repr (Z.add pos be)))) (Vptr b (Ptrofs.add i (Ptrofs.repr (Z.add pos be)))) *)
  reflexivity.
Qed.

Lemma offset_val_preserve_isptr: forall p pos, !! (isptr (offset_val pos p)) |-- !! (isptr p).
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @derives mpred Nveric (@prop mpred Nveric (isptr (offset_val pos p))) (@prop mpred Nveric (isptr p)) *)
  destruct p; simpl; apply derives_refl.
Qed.

Lemma at_offset_preserve_local_facts: forall P pos, (forall p, P p |-- !!(isptr p)) -> (forall p, at_offset P pos p |-- !!(isptr p)).
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq mpred (at_offset (memory_block sh (Z.sub ed be)) be (Vptr b i)) (memory_block sh (Z.sub ed be) (offset_val be (Vptr b i))) *)
  rewrite at_offset_eq.
(* Goal: @derives mpred Nveric (P (offset_val pos p)) (@prop mpred Nveric (isptr p)) *)
  specialize (H (offset_val pos p)).
(* Goal: @derives mpred Nveric (P (offset_val pos p)) (@prop mpred Nveric (isptr p)) *)
  eapply derives_trans; [exact H |].
(* Goal: @derives mpred Nveric (@prop mpred Nveric (isptr (offset_val pos p))) (@prop mpred Nveric (isptr p)) *)
  apply offset_val_preserve_isptr.
Qed.

Lemma withspacer_preserve_local_facts: forall sh be ed P, (forall p, P p |-- !! (isptr p)) -> (forall p, withspacer sh be ed P p |-- !! (isptr p)).
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @derives mpred Nveric (withspacer sh be ed P p) (@prop mpred Nveric (isptr p)) *)
  rewrite withspacer_spacer.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (spacer sh be ed p) (P p)) (@prop mpred Nveric (isptr p)) *)
  simpl; rewrite sepcon_comm.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (P p) (spacer sh be ed p)) (@prop mpred Nveric (isptr p)) *)
  apply (derives_left_sepcon_right_corable (!!isptr p) (P p) _); [apply corable_prop|].
(* Goal: @derives mpred Nveric (P p) (@prop mpred Nveric (isptr p)) *)
  apply H.
Qed.

Transparent memory_block.

Lemma spacer_memory_block:
  forall sh be ed v, isptr v ->
 spacer sh be ed v = memory_block sh (ed - be) (offset_val be v).
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq mpred (spacer sh be ed v) (memory_block sh (Z.sub ed be) (offset_val be v)) *)
  destruct v; inv H.
(* Goal: @eq mpred (spacer sh be ed (Vptr b i)) (memory_block sh (Z.sub ed be) (offset_val be (Vptr b i))) *)
  unfold spacer.
  destruct (Z.eq_dec (ed - be) 0);
  try solve [rewrite e; simpl offset_val; rewrite memory_block_zero_Vptr; auto].
(* Goal: @eq mpred (at_offset (memory_block sh (Z.sub ed be)) be (Vptr b i)) (memory_block sh (Z.sub ed be) (offset_val be (Vptr b i))) *)
  rewrite at_offset_eq.
(* Goal: Z.divide (align_chunk ch) (Ptrofs.unsigned i) *)
  destruct be; auto.
Qed.

Lemma spacer_sepcon_memory_block: forall sh ofs lo hi b i,
  0 <= lo ->
  0 <= ofs ->
  lo <= hi < Ptrofs.modulus ->
  Ptrofs.unsigned i + ofs + hi < Ptrofs.modulus ->
  spacer sh (ofs + lo) (ofs + hi) (Vptr b i) * memory_block sh lo (offset_val ofs (Vptr b i)) = memory_block sh hi (offset_val ofs (Vptr b i)).
Proof.
(* Goal: forall (sh : share) (ofs lo hi : Z) (b : block) (i : Ptrofs.int) (_ : Z.le Z0 lo) (_ : Z.le Z0 ofs) (_ : and (Z.le lo hi) (Z.lt hi Ptrofs.modulus)) (_ : Z.lt (Z.add (Z.add (Ptrofs.unsigned i) ofs) hi) Ptrofs.modulus), @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  intros.
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric (spacer sh (Z.add ofs lo) (Z.add ofs hi) (Vptr b i)) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  rewrite spacer_memory_block by (simpl; auto).
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric (memory_block sh (Z.sub (Z.add ofs hi) (Z.add ofs lo)) (offset_val (Z.add ofs lo) (Vptr b i))) (memory_block sh lo (offset_val ofs (Vptr b i)))) (memory_block sh hi (offset_val ofs (Vptr b i))) *)
  simpl offset_val.
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric (memory_block sh (Z.sub (Z.add ofs hi) (Z.add ofs lo)) (Vptr b (Ptrofs.add i (Ptrofs.repr (Z.add ofs lo))))) (memory_block sh lo (Vptr b (Ptrofs.add i (Ptrofs.repr ofs))))) (memory_block sh hi (Vptr b (Ptrofs.add i (Ptrofs.repr ofs)))) *)
  inv_int i.
(* Goal: @eq mpred (@sepcon mpred Nveric Sveric (memory_block sh (Z.sub (Z.add ofs hi) (Z.add ofs lo)) (Vptr b (Ptrofs.add (Ptrofs.repr ofs0) (Ptrofs.repr (Z.add ofs lo))))) (memory_block sh lo (Vptr b (Ptrofs.add (Ptrofs.repr ofs0) (Ptrofs.repr ofs))))) (memory_block sh hi (Vptr b (Ptrofs.add (Ptrofs.repr ofs0) (Ptrofs.repr ofs)))) *)
  rewrite !ptrofs_add_repr.
  rewrite sepcon_comm, Z.add_assoc, <- memory_block_split by omega.
(* Goal: @eq mpred (memory_block sh (Z.add lo (Z.sub (Z.add ofs hi) (Z.add ofs lo))) (Vptr b (Ptrofs.repr (Z.add ofs0 ofs)))) (memory_block sh hi (Vptr b (Ptrofs.repr (Z.add ofs0 ofs)))) *)
  f_equal.
(* Goal: @eq Z (Z.add lo (Z.sub (Z.add ofs hi) (Z.add ofs lo))) hi *)
  omega.
Qed.

Hint Rewrite at_offset_eq3 : at_offset_db.
Hint Rewrite withspacer_spacer : at_offset_db.
Hint Rewrite spacer_memory_block using (simpl; auto): at_offset_db.

Opaque memory_block.

