Require Import Coq.Arith.EqNat.
Require Import Coq.Relations.Relations.
(*
Require Import compcert.exportclight.Clightdefs.
Require Import compcert.cfrontend.Ctypes. (*NEW*)*)
Require Import compcert.lib.Axioms.
Require Import compcert.lib.Coqlib.
Require Import compcert.lib.Integers.
Require Import compcert.lib.Floats.
Require Import compcert.lib.Maps.
Require Import compcert.common.AST.
Require Import compcert.common.Values.
Require Import compcert.common.Memdata.
Require Import compcert.common.Memtype.
Require Import compcert.common.Memory.
Require Export VST.sepcomp.Address.

Lemma range_dec: forall a b c: Z, {a <= b < c}+{~(a <= b < c)}.
(* Goal: forall (m : Mem.mem) (b : block) (ofs : Z) (p : permission) (_ : @eq (option permission) (access_at m (@pair block Z b ofs) Cur) (@Some permission p)), @eq bool (Mem.valid_pointer m b ofs) true *)
Proof. intros. destruct (zle a b). destruct (zlt b c). left; split; auto.
(* Goal: sumbool (and (Z.le a b) (Z.lt b c)) (not (and (Z.le a b) (Z.lt b c))) *)
  right;  omega. right; omega.
Qed.

Require Export VST.msl.eq_dec.

Instance EqDec_ident: EqDec ident := ident_eq.

Instance EqDec_byte: EqDec byte := Byte.eq_dec.

(*Moved to base.v so that this file does not need to Import Clightdefs ad Ctypes
  Instance EqDec_type: EqDec type := type_eq.*)
Instance EqDec_int: EqDec int := Int.eq_dec.
Instance EqDec_int64: EqDec int64 := Int64.eq_dec.
Instance EqDec_float: EqDec float := Float.eq_dec.
Instance EqDec_float32: EqDec float32 := Float32.eq_dec.

Instance EqDex_ptr : EqDec ptrofs := Ptrofs.eq_dec. (*NEW*)

Instance EqDec_memval: EqDec memval.
Proof.
(* Goal: EqDec memval *)
 hnf; repeat decide equality; apply eq_dec.
Defined.

Instance EqDec_val: EqDec val.
Proof.
(* Goal: Mem.perm m b ofs Cur Freeable *)
hnf. decide equality; apply eq_dec.
Defined.

Instance EqDec_quantity: EqDec quantity.
Proof.
(* Goal: Mem.perm m b ofs Cur Freeable *)
hnf. decide equality.
Defined.

Definition access_at (m: mem) (loc: address) (k: perm_kind): option permission :=
   PMap.get (fst loc) (Mem.mem_access m) (snd loc) k.

Lemma perm_access: forall m b ofs k p,
    Mem.perm m b ofs k p <-> (Mem.perm_order'' (access_at m (b,ofs) k) (Some p)).
Proof. reflexivity. Qed.

Lemma access_perm: forall m b ofs k p,
  access_at m (b, ofs) k = Some p ->
  Mem.perm m b ofs k p.
Proof.
(* Goal: forall (m : Mem.mem) (b : block) (ofs : Z) (p : permission) (_ : @eq (option permission) (access_at m (@pair block Z b ofs) Cur) (@Some permission p)), @eq bool (Mem.valid_pointer m b ofs) true *)
intros.
(* Goal: Mem.perm m b ofs k p *)
unfold Mem.perm, Mem.perm_order'.
(* Goal: Mem.perm_order' (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m1) ofs Cur) Freeable *)
unfold access_at in H. simpl in H.
(* Goal: match @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k with | Some p' => perm_order p' p | None => False end *)
rewrite H; auto.
(* Goal: perm_order Freeable Freeable *)
constructor.
Qed.

Lemma access_cur_max: forall m a,
           Mem.perm_order'' (access_at m a Max)  (access_at m a Cur).
Proof.
(* Goal: forall (m : Mem.mem) (a : address), Mem.perm_order'' (access_at m a Max) (access_at m a Cur) *)
 destruct a as [b z].
(* Goal: Mem.perm_order'' (access_at m (@pair block Z b z) Max) (access_at m (@pair block Z b z) Cur) *)
 destruct (access_at m (b,z) Cur) eqn:Hc.
(* Goal: Mem.perm_order'' (access_at m (@pair block Z b z) Max) (@Some permission p) *)
(* Goal: Mem.perm_order'' (access_at m (@pair block Z b z) Max) (@None permission) *)
 rewrite <- perm_access.
(* Goal: Mem.perm m b z Max p *)
(* Goal: Mem.perm_order'' (access_at m (@pair block Z b z) Max) (@None permission) *)
 apply (Mem.perm_cur_max m b z).
(* Goal: perm_order Freeable Freeable *)
 rewrite perm_access. rewrite Hc. constructor.
(* Goal: perm_order Freeable Freeable *)
 destruct (access_at m (b, z) Max); constructor.
Qed.

Lemma invalid_noaccess: forall m b ofs k,
     ~Mem.valid_block m b -> access_at m (b, ofs) k = None.
Proof. intros; apply Mem.nextblock_noaccess. assumption. Qed.

Lemma access_empty: forall a k, access_at Mem.empty a k = None.
Proof.
(* Goal: forall (m : Mem.mem) (b : block) (ofs : Z) (p : permission) (_ : @eq (option permission) (access_at m (@pair block Z b ofs) Cur) (@Some permission p)), @eq bool (Mem.valid_pointer m b ofs) true *)
  intros. unfold access_at, Mem.empty; simpl. rewrite PMap.gi. reflexivity.
Qed.

Transparent Mem.alloc.

Theorem alloc_access_other:
  forall m1 lo hi m2 b, Mem.alloc m1 lo hi = (m2, b) ->
  forall b' ofs k,
  b'<>b \/ (ofs < lo \/ ofs >= hi) ->
  access_at m1 (b', ofs) k = access_at m2 (b', ofs) k.
Proof.
(* Goal: forall (m : Mem.mem) (b : block) (ofs : Z) (p : permission) (_ : @eq (option permission) (access_at m (@pair block Z b ofs) Cur) (@Some permission p)), @eq bool (Mem.valid_pointer m b ofs) true *)
 intros.
(* Goal: @eq (option permission) (access_at m1 (@pair block Z b' ofs) k) (access_at m2 (@pair block Z b' ofs) k) *)
pose proof (Mem.nextblock_noaccess m1 b ofs k).
(* Goal: @eq (option permission) (access_at m1 (@pair block Z b' ofs) k) (access_at m2 (@pair block Z b' ofs) k) *)
pose proof (Mem.alloc_result _ _ _ _ _ H).
(* Goal: @eq (option permission) (access_at m1 (@pair block Z b' ofs) k) (access_at m2 (@pair block Z b' ofs) k) *)
unfold access_at; inversion H; clear H; subst; simpl.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (Mem.mem_access m1) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (Mem.nextblock m1) (fun (ofs : Z) (_ : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission Freeable else @None permission) (Mem.mem_access m1)) ofs k) *)
destruct (eq_block b' (Mem.nextblock m1)).
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (Mem.mem_access m1) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (Mem.nextblock m1) (fun (ofs : Z) (_ : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission Freeable else @None permission) (Mem.mem_access m1)) ofs k) *)
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (Mem.mem_access m1) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (Mem.nextblock m1) (fun (ofs : Z) (_ : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission Freeable else @None permission) (Mem.mem_access m1)) ofs k) *)
destruct H0; try contradiction.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (Mem.mem_access m1) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (Mem.nextblock m1) (fun (ofs : Z) (_ : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission Freeable else @None permission) (Mem.mem_access m1)) ofs k) *)
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (Mem.mem_access m1) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (Mem.nextblock m1) (fun (ofs : Z) (_ : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission Freeable else @None permission) (Mem.mem_access m1)) ofs k) *)
subst b'.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) ofs k) *)
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (Mem.mem_access m) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) ofs k) *)
rewrite PMap.gss.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) (Mem.nextblock m1) (Mem.mem_access m1) ofs k) (if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission Freeable else @None permission) *)
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (Mem.mem_access m1) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) (Mem.nextblock m1) (fun (ofs : Z) (_ : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission Freeable else @None permission) (Mem.mem_access m1)) ofs k) *)
destruct (zle lo ofs), (zlt ofs hi); try omega; simpl; apply H1; apply Plt_strict.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (Mem.mem_access m) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) ofs k) *)
rewrite PMap.gso by auto. auto.
Qed.

Theorem alloc_access_same:
  forall m1 lo hi m2 b, Mem.alloc m1 lo hi = (m2, b) ->
  forall ofs k,
  lo <= ofs < hi -> access_at m2 (b,ofs) k = Some Freeable.
Proof.
(* Goal: forall (m : Mem.mem) (b : block) (ofs : Z) (p : permission) (_ : @eq (option permission) (access_at m (@pair block Z b ofs) Cur) (@Some permission p)), @eq bool (Mem.valid_pointer m b ofs) true *)
 intros.
(* Goal: @eq (option permission) (access_at m2 (@pair block Z b ofs) k) (@Some permission Freeable) *)
 inversion H; clear H; subst. unfold access_at; simpl.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) ofs k) *)
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (Mem.mem_access m) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) ofs k) *)
 rewrite PMap.gss.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs Cur) (@Some permission p) *)
destruct (zle lo ofs), (zlt ofs hi); try omega; simpl; auto.
Qed.

Opaque Mem.alloc.
Transparent Mem.free.

Lemma access_free:
  forall m1 b lo hi,
  (forall ofs, lo <= ofs < hi -> access_at m1 (b,ofs) Cur = Some Freeable) ->
  { m2: mem | Mem.free m1 b lo hi = Some m2 }.
Proof.
(* Goal: forall (m : Mem.mem) (b : block) (ofs : Z) (p : permission) (_ : @eq (option permission) (access_at m (@pair block Z b ofs) Cur) (@Some permission p)), @eq bool (Mem.valid_pointer m b ofs) true *)
 intros.
(* Goal: @sig Mem.mem (fun m2 : Mem.mem => @eq (option Mem.mem) (Mem.free m1 b lo hi) (@Some Mem.mem m2)) *)
 unfold Mem.free.
(* Goal: @sig Mem.mem (fun m2 : Mem.mem => @eq (option Mem.mem) (if Mem.range_perm_dec m1 b lo hi Cur Freeable then @Some Mem.mem (Mem.unchecked_free m1 b lo hi) else @None Mem.mem) (@Some Mem.mem m2)) *)
 destruct (Mem.range_perm_dec m1 b lo hi Cur Freeable).
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs Cur) (@Some permission p) *)
 eauto.
(* Goal: @sig Mem.mem (fun m2 : Mem.mem => @eq (option Mem.mem) (@None Mem.mem) (@Some Mem.mem m2)) *)
 contradiction n; clear n.
(* Goal: forall (m : Mem.mem) (b : block) (ofs : Z) (p : permission) (_ : @eq (option permission) (access_at m (@pair block Z b ofs) Cur) (@Some permission p)), @eq bool (Mem.valid_pointer m b ofs) true *)
 hnf; intros. unfold Mem.perm. unfold access_at in H.
(* Goal: perm_order Freeable Freeable *)
 simpl in H; rewrite H by auto. constructor.
Qed.

Lemma free_access:
  forall m1 b lo hi m2, Mem.free m1 b lo hi = Some m2 ->
  (forall ofs, lo <= ofs < hi ->
      access_at m1 (b,ofs) Cur = Some Freeable /\ access_at m2 (b,ofs) Max = None).
Proof.
(* Goal: forall (m : Mem.mem) (b : block) (ofs : Z) (p : permission) (_ : @eq (option permission) (access_at m (@pair block Z b ofs) Cur) (@Some permission p)), @eq bool (Mem.valid_pointer m b ofs) true *)
 intros.
(* Goal: @eq (option permission) (access_at m1 (@pair block Z b ofs) k) (access_at m2 (@pair block Z b ofs) k) *)
 unfold Mem.free in H.
(* Goal: @eq (option permission) (access_at m2 (@pair block Z b ofs) k) (@Some permission Freeable) *)
 destruct (Mem.range_perm_dec m1 b lo hi Cur Freeable); inversion H; clear H; subst.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (@Some permission Freeable) *)
 specialize (r _ H0).
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (@Some permission Freeable) *)
 hnf in r.
(* Goal: @eq (option permission) (access_at m1 (@pair block Z b' z') k) (access_at m2 (@pair block Z b' z') k) *)
 unfold access_at. simpl.
(* Goal: and (@eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m1) ofs Cur) (@Some permission Freeable)) (@eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @None permission else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m1) ofs k) (Mem.mem_access m1)) ofs Max) (@None permission)) *)
 destruct ((Mem.mem_access m1) !! b ofs Cur); try contradiction.
(* Goal: and (@eq (option permission) (@Some permission p) (@Some permission Freeable)) (@eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @None permission else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m1) ofs k) (Mem.mem_access m1)) ofs Max) (@None permission)) *)
 assert (p=Freeable) by (destruct p; inversion r; auto). subst p.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs Cur) (@Some permission p) *)
 split; auto.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) ofs k) *)
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (Mem.mem_access m) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) ofs k) *)
 simpl. rewrite PMap.gss.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m1) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m1) ofs k) *)
 destruct (zle lo ofs), (zlt ofs hi); try omega. reflexivity.
Qed.

Lemma free_access_other:
  forall m1 bf lo hi m2, Mem.free m1 bf lo hi = Some m2 ->
  forall b ofs k,
  b <> bf \/ ofs < lo \/ hi <= ofs ->
  access_at m1 (b,ofs) k = access_at m2 (b,ofs) k.
Proof.
(* Goal: forall (m : Mem.mem) (b : block) (ofs : Z) (p : permission) (_ : @eq (option permission) (access_at m (@pair block Z b ofs) Cur) (@Some permission p)), @eq bool (Mem.valid_pointer m b ofs) true *)
 intros.
(* Goal: @eq (option permission) (access_at m1 (@pair block Z b ofs) k) (access_at m2 (@pair block Z b ofs) k) *)
 unfold Mem.free in H.
(* Goal: @eq (option permission) (access_at m2 (@pair block Z b ofs) k) (@Some permission Freeable) *)
 destruct (Mem.range_perm_dec m1 bf lo hi Cur Freeable); inversion H; clear H; subst.
(* Goal: @eq (option permission) (access_at m (@pair block Z b' ofs) k) (access_at (Mem.mkmem (Mem.mem_contents m) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) (Mem.nextblock m) (fun (b0 : positive) (ofs : Z) => Memory.Mem.drop_perm_obligation_1 m b lo hi p b0 ofs) (fun (b0 : positive) (ofs : Z) (k : perm_kind) (H0 : not (Plt b0 (Mem.nextblock m))) => Memory.Mem.drop_perm_obligation_2 m b lo hi p r b0 ofs k H0) (fun b0 : positive => Memory.Mem.drop_perm_obligation_3 m b0)) (@pair block Z b' ofs) k) *)
 unfold access_at; simpl.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m1) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) bf (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @None permission else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) bf (Mem.mem_access m1) ofs k) (Mem.mem_access m1)) ofs k) *)
 destruct (eq_block b bf).
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) ofs k) *)
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (Mem.mem_access m) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) ofs k) *)
 subst bf; rewrite PMap.gss.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs Cur) (@Some permission p) *)
 destruct H0. contradiction H; auto.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs Cur) (@Some permission p) *)
 destruct (zle lo ofs), (zlt ofs hi); try omega; simpl; auto.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m1) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m1) ofs k) *)
 rewrite PMap.gso by auto. reflexivity.
Qed.

Opaque Mem.free.

Lemma access_drop_1:
  forall m b lo hi p m', Mem.drop_perm m b lo hi p = Some m' ->
  (forall ofs, lo <= ofs < hi ->
     forall k,
     access_at m (b, ofs) k = Some Freeable /\ access_at m' (b, ofs) k = Some p).
Proof.
(* Goal: forall (m : Mem.mem) (b : block) (ofs : Z) (p : permission) (_ : @eq (option permission) (access_at m (@pair block Z b ofs) Cur) (@Some permission p)), @eq bool (Mem.valid_pointer m b ofs) true *)
 intros.
(* Goal: @eq (option permission) (access_at m (@pair block Z b' ofs) k) (access_at m' (@pair block Z b' ofs) k) *)
 unfold Mem.drop_perm in H.
(* Goal: @eq (option permission) (access_at m2 (@pair block Z b ofs) k) (@Some permission Freeable) *)
 destruct (Mem.range_perm_dec m b lo hi Cur Freeable); inversion H; clear H; subst.
(* Goal: @eq (option permission) (access_at m (@pair block Z b' ofs) k) (access_at (Mem.mkmem (Mem.mem_contents m) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) (Mem.nextblock m) (fun (b0 : positive) (ofs : Z) => Memory.Mem.drop_perm_obligation_1 m b lo hi p b0 ofs) (fun (b0 : positive) (ofs : Z) (k : perm_kind) (H0 : not (Plt b0 (Mem.nextblock m))) => Memory.Mem.drop_perm_obligation_2 m b lo hi p r b0 ofs k H0) (fun b0 : positive => Memory.Mem.drop_perm_obligation_3 m b0)) (@pair block Z b' ofs) k) *)
 unfold access_at; simpl.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) ofs k) *)
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (Mem.mem_access m) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) ofs k) *)
 rewrite PMap.gss.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs Cur) (@Some permission p) *)
 destruct (zle lo ofs), (zlt ofs hi); try omega; simpl; auto.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs Cur) (@Some permission p) *)
 split; auto.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (@Some permission Freeable) *)
 specialize (r _ H0). hnf in r. destruct ( (Mem.mem_access m) !! b ofs Cur) eqn:?; try contradiction.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (@Some permission Freeable) *)
 assert (p0=Freeable) by (destruct p0; inv r; auto). subst.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (@Some permission Freeable) *)
 pose proof (Mem.access_max m b ofs).
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (@Some permission Freeable) *)
 rewrite Heqo in H.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs Cur) (@Some permission p) *)
 destruct k; auto.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs Cur) (@Some permission p) *)
 destruct ((Mem.mem_access m) !! b ofs Max); inv H; auto.
Qed.

Lemma access_drop_2:
  forall m b lo hi p,
  (forall ofs, lo <= ofs < hi -> access_at m (b,ofs) Cur = Some Freeable) ->
  { m' | Mem.drop_perm m b lo hi p = Some m' }.
Proof.
(* Goal: forall (m : Mem.mem) (b : block) (ofs : Z) (p : permission) (_ : @eq (option permission) (access_at m (@pair block Z b ofs) Cur) (@Some permission p)), @eq bool (Mem.valid_pointer m b ofs) true *)
 intros.
(* Goal: @sig Mem.mem (fun m' : Mem.mem => @eq (option Mem.mem) (Mem.drop_perm m b lo hi p) (@Some Mem.mem m')) *)
 unfold Mem.drop_perm.
(* Goal: @sig Mem.mem (fun m' : Mem.mem => @eq (option Mem.mem) match Mem.range_perm_dec m b lo hi Cur Freeable with | left x => @Some Mem.mem (Mem.mkmem (Mem.mem_contents m) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) (Mem.nextblock m) (fun (b0 : positive) (ofs : Z) => Memory.Mem.drop_perm_obligation_1 m b lo hi p b0 ofs) (fun (b0 : positive) (ofs : Z) (k : perm_kind) (H0 : not (Plt b0 (Mem.nextblock m))) => Memory.Mem.drop_perm_obligation_2 m b lo hi p x b0 ofs k H0) (fun b0 : positive => Memory.Mem.drop_perm_obligation_3 m b0)) | right x => @None Mem.mem end (@Some Mem.mem m')) *)
 destruct (Mem.range_perm_dec m b lo hi Cur Freeable).
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs Cur) (@Some permission p) *)
 eauto.
(* Goal: forall (m : Mem.mem) (b : block) (ofs : Z) (p : permission) (_ : @eq (option permission) (access_at m (@pair block Z b ofs) Cur) (@Some permission p)), @eq bool (Mem.valid_pointer m b ofs) true *)
 contradiction n; hnf; intros.
(* Goal: Mem.perm m b ofs Cur Freeable *)
 specialize (H _ H0).
(* Goal: Mem.perm m b ofs Cur Freeable *)
 unfold access_at in *.  hnf. simpl in *; rewrite H. constructor.
Qed.

Lemma access_drop_3:
  forall m b lo hi p m', Mem.drop_perm m b lo hi p = Some m' ->
  forall b' ofs k, b' <> b \/ ofs < lo \/ hi <= ofs ->
    access_at m (b', ofs) k = access_at m' (b',ofs) k.
Proof.
(* Goal: forall (m : Mem.mem) (b : block) (ofs : Z) (p : permission) (_ : @eq (option permission) (access_at m (@pair block Z b ofs) Cur) (@Some permission p)), @eq bool (Mem.valid_pointer m b ofs) true *)
 intros.
(* Goal: @eq (option permission) (access_at m (@pair block Z b' ofs) k) (access_at m' (@pair block Z b' ofs) k) *)
 unfold Mem.drop_perm in H.
(* Goal: @eq (option permission) (access_at m2 (@pair block Z b ofs) k) (@Some permission Freeable) *)
 destruct (Mem.range_perm_dec m b lo hi Cur Freeable); inversion H; clear H; subst.
(* Goal: @eq (option permission) (access_at m (@pair block Z b' ofs) k) (access_at (Mem.mkmem (Mem.mem_contents m) (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) (Mem.nextblock m) (fun (b0 : positive) (ofs : Z) => Memory.Mem.drop_perm_obligation_1 m b lo hi p b0 ofs) (fun (b0 : positive) (ofs : Z) (k : perm_kind) (H0 : not (Plt b0 (Mem.nextblock m))) => Memory.Mem.drop_perm_obligation_2 m b lo hi p r b0 ofs k H0) (fun b0 : positive => Memory.Mem.drop_perm_obligation_3 m b0)) (@pair block Z b' ofs) k) *)
 unfold access_at; simpl.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (Mem.mem_access m) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) ofs k) *)
 destruct (eq_block b' b).
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) ofs k) *)
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (Mem.mem_access m) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) ofs k) *)
 subst. rewrite PMap.gss.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) *)
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (Mem.mem_access m) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) ofs k) *)
 destruct H0.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs Cur) (@Some permission p) *)
 contradiction H; auto.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs Cur) (@Some permission p) *)
 destruct (zle lo ofs), (zlt ofs hi); try omega; simpl; auto.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (Mem.mem_access m) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b' (@PMap.set (forall (_ : Z) (_ : perm_kind), option permission) b (fun (ofs : Z) (k : perm_kind) => if andb (@proj_sumbool (Z.le lo ofs) (Z.gt lo ofs) (zle lo ofs)) (@proj_sumbool (Z.lt ofs hi) (Z.ge ofs hi) (zlt ofs hi)) then @Some permission p else @PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs k) (Mem.mem_access m)) ofs k) *)
 rewrite PMap.gso by auto.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs Cur) (@Some permission p) *)
 auto.
Qed.

Lemma storebytes_access:
 forall m1 b ofs bytes m2 (STORE: Mem.storebytes m1 b ofs bytes = Some m2),
  access_at m1 = access_at m2.
Proof.
(* Goal: forall (m : Mem.mem) (b : block) (ofs : Z) (p : permission) (_ : @eq (option permission) (access_at m (@pair block Z b ofs) Cur) (@Some permission p)), @eq bool (Mem.valid_pointer m b ofs) true *)
intros.
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m1) (access_at m2) *)
apply extensionality ;intros [b' z].
(* Goal: @eq (forall _ : perm_kind, option permission) (access_at m1 (@pair block Z b' z')) (access_at m2 (@pair block Z b' z')) *)
apply extensionality ;intro k.
(* Goal: @eq (option permission) (access_at m1 (@pair block Z b' z) k) (access_at m2 (@pair block Z b' z) k) *)
apply Mem.storebytes_access in STORE.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs Cur) (@Some permission p) *)
unfold access_at; f_equal; auto.
Qed.

Lemma store_access:
 forall chunk m1 b ofs v m2 (STORE: Mem.store chunk m1 b ofs v = Some m2),
  access_at m1 = access_at m2.
Proof.
(* Goal: forall (m : Mem.mem) (b : block) (ofs : Z) (p : permission) (_ : @eq (option permission) (access_at m (@pair block Z b ofs) Cur) (@Some permission p)), @eq bool (Mem.valid_pointer m b ofs) true *)
intros.
(* Goal: @eq (forall (_ : address) (_ : perm_kind), option permission) (access_at m1) (access_at m2) *)
apply extensionality; intros [b' z'].
(* Goal: @eq (forall _ : perm_kind, option permission) (access_at m1 (@pair block Z b' z')) (access_at m2 (@pair block Z b' z')) *)
apply extensionality ;intro k.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs Cur) (@Some permission p) *)
unfold access_at. apply Mem.store_access in STORE. rewrite STORE; auto.
Qed.

Lemma perm_order'_dec_fiddle:
  forall y x, y = Some x ->
     proj_sumbool (Mem.perm_order'_dec y Nonempty) = true.
Proof.
(* Goal: forall (m : Mem.mem) (b : block) (ofs : Z) (p : permission) (_ : @eq (option permission) (access_at m (@pair block Z b ofs) Cur) (@Some permission p)), @eq bool (Mem.valid_pointer m b ofs) true *)
intros. subst. simpl.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m1) ofs k) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m1) ofs k) *)
unfold Mem.perm_order_dec. destruct x; reflexivity.
Qed.

Lemma access_at_valid_pointer:
  forall m b ofs p, access_at m (b,ofs) Cur = Some p ->
   Mem.valid_pointer m b ofs = true.
Proof.
(* Goal: forall (m : Mem.mem) (b : block) (ofs : Z) (p : permission) (_ : @eq (option permission) (access_at m (@pair block Z b ofs) Cur) (@Some permission p)), @eq bool (Mem.valid_pointer m b ofs) true *)
intros.
(* Goal: @eq bool (Mem.valid_pointer m b ofs) true *)
unfold access_at, Mem.valid_pointer in *.
(* Goal: @eq bool (@proj_sumbool (Mem.perm m b ofs Cur Nonempty) (not (Mem.perm m b ofs Cur Nonempty)) (Mem.perm_dec m b ofs Cur Nonempty)) true *)
simpl in *.
(* Goal: @eq bool (@proj_sumbool (Mem.perm m b ofs Cur Nonempty) (not (Mem.perm m b ofs Cur Nonempty)) (Mem.perm_dec m b ofs Cur Nonempty)) true *)
apply perm_order'_dec_fiddle with p.
(* Goal: @eq (option permission) (@PMap.get (forall (_ : Z) (_ : perm_kind), option permission) b (Mem.mem_access m) ofs Cur) (@Some permission p) *)
auto.
Qed.







