(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*          Sandrine Blazy, ENSIIE and INRIA Paris-Rocquencourt        *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation, either version 2 of the License, or  *)
(*  (at your option) any later version.  This file is also distributed *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(* * This file develops the memory model that is used in the dynamic
  semantics of all the languages used in the compiler.
  It defines a type [mem] of memory states, the following 4 basic
  operations over memory states, and their properties:
- [load]: read a memory chunk at a given address;
- [store]: store a memory chunk at a given address;
- [alloc]: allocate a fresh memory block;
- [free]: invalidate a memory block.
*)

include "arithmetics/nat.ma".
include "binary/Z.ma".
include "datatypes/sums.ma".
include "datatypes/list.ma".
include "Plogic/equality.ma".

include "Coqlib.ma".
include "Values.ma".
include "AST.ma".
include "extralib.ma".

ndefinition update : ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z → A. Z → A ≝ 
  λA,x,v,f.
    λy.match eqZb y x with [ true ⇒ v | false ⇒ f y ].
    
(* Implicit Arguments update [A].*)

nlemma update_s:
  ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z -> A.
  update … x v f x = v.
#A;#x;#v;#f;nwhd in ⊢ (??%?);
nrewrite > (eqZb_z_z …);//;
nqed.

nlemma update_o:
  ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z -> A. ∀y: Z.
  x ≠ y → update … x v f y = f y.
#A;#x;#v;#f;#y;#H;nwhd in ⊢ (??%?);
napply eqZb_elim;//;
#H2;ncases H;#H3;nelim (H3 ?);//;
nqed.

(* FIXME: workaround for lack of nunfold *)
nlemma unfold_update : ∀A,x,v,f,y. update A x v f y = match eqZb y x with [ true ⇒ v | false ⇒ f y ].
//; nqed.


(* * Structure of memory states *)

(* A memory state is organized in several disjoint blocks.  Each block
  has a low and a high bound that defines its size.  Each block map
  byte offsets to the contents of this byte. *)

(* The possible contents of a byte-sized memory cell.  To give intuitions,
  a 4-byte value [v] stored at offset [d] will be represented by
  the content [Datum(4, v)] at offset [d] and [Cont] at offsets [d+1],
  [d+2] and [d+3].  The [Cont] contents enable detecting future writes
  that would partially overlap the 4-byte value. *)

ninductive content : Type[0] ≝
  | Undef: content                 (*r undefined contents *)
  | Datum: nat → val → content   (*r first byte of a value *)
  | Cont: content.          (*r continuation bytes for a multi-byte value *)

ndefinition contentmap : Type[0] ≝ Z → content.

(* A memory block comprises the dimensions of the block (low and high bounds)
  plus a mapping from byte offsets to contents.  *)

(* XXX: mkblock *)
nrecord block_contents : Type[0] ≝ {
  low: Z;
  high: Z;
  contents: contentmap;
  space: memory_space
}.

(* A memory state is a mapping from block addresses (represented by [Z]
  integers) to blocks.  We also maintain the address of the next 
  unallocated block, and a proof that this address is positive. *)
(* XXX: mkmem *)

nrecord mem : Type ≝ {
  blocks: Z -> block_contents;
  nextblock: block;
  nextblock_pos: OZ < nextblock
}.

(* * Operations on memory stores *)

(* Memory reads and writes are performed by quantities called memory chunks,
  encoding the type, size and signedness of the chunk being addressed.
  The following functions extract the size information from a chunk. *)

(* FIXME: coercions *)
ndefinition size_chunk : memory_chunk → Z ≝
  λchunk.match chunk return λ_.Z with
  [ Mint8signed => 1
  | Mint8unsigned => 1
  | Mint16signed => 2
  | Mint16unsigned => 2
  | Mint24 ⇒ 3
  | Mint32 => 4
  | Mfloat32 => 4
  | Mfloat64 => 8 ].
 
ndefinition pred_size_chunk : memory_chunk → nat ≝ 
  λchunk.match chunk with
  [ Mint8signed => 0
  | Mint8unsigned => 0
  | Mint16signed => 1
  | Mint16unsigned => 1
  | Mint24 ⇒ 2
  | Mint32 => 3
  | Mfloat32 => 3
  | Mfloat64 => 7].

alias symbol "plus" (instance 2) = "integer plus".
nlemma size_chunk_pred:
  ∀chunk. size_chunk chunk = 1 + pred_size_chunk chunk.
#chunk;ncases chunk;//;
nqed.

nlemma size_chunk_pos:
  ∀chunk. 0 < size_chunk chunk.
#chunk;nrewrite > (size_chunk_pred ?);ncases (pred_size_chunk chunk);
nnormalize;//;
nqed.

(* Memory reads and writes must respect alignment constraints:
  the byte offset of the location being addressed should be an exact
  multiple of the natural alignment for the chunk being addressed.
  This natural alignment is defined by the following 
  [align_chunk] function.  Some target architectures
  (e.g. the PowerPC) have no alignment constraints, which we could
  reflect by taking [align_chunk chunk = 1].  However, other architectures
  have stronger alignment requirements.  The following definition is
  appropriate for PowerPC and ARM. *)

ndefinition align_chunk : memory_chunk → Z ≝ 
  λchunk.match chunk return λ_.Z with
  [ Mint8signed ⇒ 1
  | Mint8unsigned ⇒ 1
  | Mint16signed ⇒ 1
  | Mint16unsigned ⇒ 1
  | _ ⇒ 1 ].

nlemma align_chunk_pos:
  ∀chunk. OZ < align_chunk chunk.
#chunk;ncases chunk;nnormalize;//;
nqed.

(* TODO: nicer proof (though this does mirror the coq one!) *)
nlemma align_size_chunk_divides:
  ∀chunk. (align_chunk chunk ∣ size_chunk chunk).
#chunk;ncases chunk;nnormalize;/3/;
nqed.

nlemma align_chunk_compat:
  ∀chunk1,chunk2.
    size_chunk chunk1 = size_chunk chunk2 → 
      align_chunk chunk1 = align_chunk chunk2.
#chunk1;#chunk2;ncases chunk1;ncases chunk2;nnormalize;//;#H;ndestruct;
nqed.

(* The initial store. *)

ndefinition oneZ ≝ pos one.

nremark one_pos: OZ < oneZ.
//;
nqed.

ndefinition empty_block : Z → Z → memory_space → block_contents ≝ 
  λlo,hi,bty.mk_block_contents lo hi (λy. Undef) bty.

ndefinition empty: mem ≝ 
  mk_mem (λx.empty_block OZ OZ Any) (pos one) one_pos.

ndefinition nullptr: block ≝ OZ.

(* Allocation of a fresh block with the given bounds.  Return an updated
  memory state and the address of the fresh block, which initially contains
  undefined cells.  Note that allocation never fails: we model an
  infinite memory. *)

nremark succ_nextblock_pos:
  ∀m. OZ < Zsucc (nextblock m). (* XXX *)
#m;nlapply (nextblock_pos m);nnormalize;
ncases (nextblock m);//;
#n;ncases n;//;
nqed.

ndefinition alloc : mem → Z → Z → memory_space → mem × block ≝
  λm,lo,hi,bty.〈mk_mem 
              (update … (nextblock m)
                 (empty_block lo hi bty)
                 (blocks m))
              (Zsucc (nextblock m))
              (succ_nextblock_pos m),
            nextblock m〉.

(* Freeing a block.  Return the updated memory state where the given
  block address has been invalidated: future reads and writes to this
  address will fail.  Note that we make no attempt to return the block
  to an allocation pool: the given block address will never be allocated
  later. *)

ndefinition free ≝
  λm,b.mk_mem (update … b 
                (empty_block OZ OZ Any)
                (blocks m))
        (nextblock m)
        (nextblock_pos m).

(* Freeing of a list of blocks. *)

ndefinition free_list ≝ 
  λm,l.foldr ?? (λb,m.free m b) m l.
(* XXX hack for lack of reduction with restricted unfolding *)
nlemma unfold_free_list : ∀m,h,t. free_list m (h::t) = free (free_list m t) h.
nnormalize; //; nqed.

(* Return the low and high bounds for the given block address.
   Those bounds are 0 for freed or not yet allocated address. *)

ndefinition low_bound : mem → block → Z ≝
  λm,b.low (blocks m b).
ndefinition high_bound : mem → block → Z ≝ 
  λm,b.high (blocks m b).
ndefinition block_space: mem → block → memory_space ≝
  λm,b.space (blocks m b).

(* A block address is valid if it was previously allocated. It remains valid
  even after being freed. *)

ndefinition valid_block : mem → block → Prop ≝ 
  λm,b.b < nextblock m.

(* FIXME: hacks to get around lack of nunfold *)
nlemma unfold_low_bound : ∀m,b. low_bound m b = low (blocks m b).
//; nqed.
nlemma unfold_high_bound : ∀m,b. high_bound m b = high (blocks m b).
//; nqed.
nlemma unfold_valid_block : ∀m,b. (valid_block m b) = (b < nextblock m).
//; nqed.

(* Reading and writing [N] adjacent locations in a [contentmap].

  We define two functions and prove some of their properties:
  - [getN n ofs m] returns the datum at offset [ofs] in block contents [m]
    after checking that the contents of offsets [ofs+1] to [ofs+n+1]
    are [Cont].
  - [setN n ofs v m] updates the block contents [m], storing the content [v]
    at offset [ofs] and the content [Cont] at offsets [ofs+1] to [ofs+n+1].
 *)

nlet rec check_cont (n: nat) (p: Z) (m: contentmap) on n : bool ≝
  match n return λ_.bool with
  [ O ⇒ true
  | S n1 ⇒
      match m p with
      [ Cont ⇒ check_cont n1 (Zplus p 1) m (* FIXME: cannot disambiguate + properly  *)
      | _ ⇒ false ] ].

(* XXX : was +, not ∨ logical or
   is used when eqb is expected, coq idiom, is it necessary?? *)
ndefinition eq_nat: ∀p,q: nat. p=q ∨ p≠q.
napply decidable_eq_nat; (* // not working, why *)
nqed.

ndefinition getN : nat → Z → contentmap → val ≝
  λn,p,m.match m p with
  [ Datum n' v ⇒ 
      match andb (eqb n n') (check_cont n (p + oneZ) m) with
      [ true ⇒ v
      | false ⇒ Vundef ]
  | _ ⇒ 
      Vundef ].

nlet rec set_cont (n: nat) (p: Z) (m: contentmap) on n : contentmap ≝
  match n with
  [ O ⇒ m
  | S n1 ⇒ update ? p Cont (set_cont n1 (p + oneZ) m) ].

ndefinition setN : nat → Z → val → contentmap → contentmap ≝ 
  λn,p,v,m.update ? p (Datum n v) (set_cont n (p + oneZ) m).

(* XXX: the daemons *)
naxiom daemon : ∀A:Prop.A.

nlemma check_cont_spec:
  ∀n,m,p.
  match (check_cont n p m) with
  [ true ⇒ ∀q.p ≤ q → q < p + n → m q = Cont
  | false ⇒ ∃q. p ≤ q ∧ q < (p + n) ∧ m q ≠ Cont ].
#n;nelim n;
##[#m;#p;#q;#Hl;#Hr;
   (* derive contradiction from Hl, Hr; needs:
      - p + O = p
      - p ≤ q → q < p → False *)
   napply daemon
##|#n1;#IH;#m;#p;
   (* nwhd : doesn't work either *)
   ncut (check_cont (S n1) p m = match m p with [ Undef ⇒ false | Datum _ _ ⇒ false | Cont ⇒ check_cont n1 (Zplus p oneZ) m ])
   ##[@
   ##|#Heq;nrewrite > Heq;nlapply (refl ? (m p));
      ncases (m p) in ⊢ (???% → %);
      ##[#Heq1;@;
           ##[napply p
           ##|@; ##[napply daemon
                 ##|napply nmk;#Hfalse;nrewrite > Hfalse in Heq1;#Heq1;
                    ndestruct ]
           ##]
      ##|#n2;#v;#Heq1; @;
           ##[napply p
           ##| @; ##[ (* refl≤ and  p < p + S n1 *)napply daemon
                  ##|napply nmk;#Hfalse;nrewrite > Hfalse in Heq1;#Heq1;
                     ndestruct ]
           ##]
      ##|#Heq1;nlapply (IH m (p + 1));
         nlapply (refl ? (check_cont n1 (p + 1) m));
         (* napply daemon *)
         ncases (check_cont n1 (p + 1) m) in ⊢ (???% → %);
         nwhd in ⊢ (? → % → %);
         ##[#H;#H1;#q;#Hl;#Hr;
            ncut (p = q ∨ p + 1 ≤ q)
            ##[(* Hl *) napply daemon
            ##|*;
               ##[//
               ##|#Hl2;napply H1;//;(*Hr*)napply daemon ##] ##]
         ##|#H;#H1;ncases H1;#x;*;*;#Hl;#Hr;#Hx;
            @ x;@
            ##[@
               ##[(*Hl*) napply daemon
               ##|(*Hr*) napply daemon ##]
            ##|//##]##]##]##]
nqed.

nlemma check_cont_true:
  ∀n:nat.∀m,p.
  (∀q. p ≤ q → q < p + n → m q = Cont) →
  check_cont n p m = true.
#n;#m;#p;#H;nlapply (check_cont_spec n m p);
ncases (check_cont n p m);//;
nwhd in ⊢ (%→?);*;
#q;*;*;#Hl;#Hr;#Hfalse;ncases Hfalse;#H1;nelim (H1 ?);napply H;//;
nqed.

nlemma check_cont_false:
  ∀n:nat.∀m,p,q.
  p ≤ q → q < p + n → m q ≠ Cont →
  check_cont n p m = false.
#n;#m;#p;#q;nlapply (check_cont_spec n m p);
ncases (check_cont n p m);//;
nwhd in ⊢ (%→?);#H;
#Hl;#Hr;#Hfalse;ncases Hfalse;#H1;nelim (H1 ?);napply H;//;
nqed.

nlemma set_cont_inside:
  ∀n:nat.∀p:Z.∀m.∀q:Z.
  p ≤ q → q < p + n →
  (set_cont n p m) q = Cont.
#n;nelim n;
##[#p;#m;#q;#Hl;#Hr;(* by Hl, Hr → False *)napply daemon
##|#n1;#IH;#p;#m;#q;#Hl;#Hr;
   ncut (p = q ∨ p+1 ≤ q)
   ##[napply daemon
   ##|*;
      ##[#Heq;nrewrite > Heq;napply update_s;
      ##|#Hl2;nwhd in ⊢ (??%?);nrewrite > (? : eqZb q p = false)
         ##[nwhd in ⊢ (??%?);napply IH
            ##[napply Hl2
            ##|(* Hr *) napply daemon ##]
         ##|(*Hl2*)napply daemon ##]
      ##]
   ##]
##]
nqed.

nlemma set_cont_outside:
  ∀n:nat.∀p:Z.∀m.∀q:Z.
  q < p ∨ p + n ≤ q → 
  (set_cont n p m) q = m q.
#n;nelim n
##[#p;#m;#q;#_;@
##|#n1;#IH;#p;#m;#q;
   #H;nwhd in ⊢ (??%?);nrewrite > (? : eqZb q p = false);
   ##[nwhd in ⊢ (??%?);napply IH;ncases H;
      ##[#Hl;@;napply daemon
      ##|#Hr;@2;napply daemon##]
   ##|(*H*)napply daemon ##]
##]
nqed.

nlemma getN_setN_same:
  ∀n,p,v,m.
  getN n p (setN n p v m) = v.
#n;#p;#v;#m;nchange in ⊢ (??(???%)?) with (update ????);
nwhd in ⊢ (??%?);
nrewrite > (update_s content p ??);nwhd in ⊢ (??%?);
nrewrite > (eqb_n_n n);
nrewrite > (check_cont_true ????)
##[@
##|#q;#Hl;#Hr;nrewrite > (update_o content …);
   ##[/2/;
   ##|(*Hl*)napply daemon ##]
##]
nqed.

nlemma getN_setN_other:
  ∀n1,n2:nat.∀p1,p2:Z.∀v,m.
  p1 + n1 < p2 ∨ p2 + n2 < p1 → 
  getN n2 p2 (setN n1 p1 v m) = getN n2 p2 m.
#n1;#n2;#p1;#p2;#v;#m;#H; 
ngeneralize in match (check_cont_spec n2 m (p2 + oneZ));
nlapply (refl ? (check_cont n2 (p2+oneZ) m));
ncases (check_cont n2 (p2+oneZ) m) in ⊢ (???% → %);
#H1;nwhd in ⊢ (% →?); nwhd in ⊢ (?→(???%)); nrewrite > H1;
##[#H2;
   nchange in ⊢ (??(???%)?) with (update ????);
   nwhd in ⊢(??%%);nrewrite > (check_cont_true …);
   ##[ nrewrite > (check_cont_true … H2);
       nrewrite > (update_o content ?????);
       ##[ nrewrite > (set_cont_outside ?????); //; (* arith *) napply daemon
       ##| (* arith *) napply daemon
       ##]
   ##| #q;#Hl;#Hh; nrewrite > (update_o content ?????);
       ##[ nrewrite > (set_cont_outside ?????); /2/; (* arith *) napply daemon
       ##| (* arith *) napply daemon
       ##]
   ##]
##| *; #q;*;#A;#B;
   nchange in ⊢ (??(???%)?) with (update ????);
   nwhd in ⊢(??%%);
   nrewrite > (check_cont_false n2 (update ? p1 (Datum n1 v) (set_cont n1 (p1 + 1) m)) (p2 + 1) q …);
   ##[ nrewrite > (update_o content ?????);
       ##[ nrewrite > (set_cont_outside ?????); //; (* arith *) napply daemon
       ##| napply daemon
       ##]
   ##| nrewrite > (update_o content ?????);
       ##[ nrewrite > (set_cont_outside ?????); //; (* arith *) napply daemon
       ##| napply daemon
       ##]
   ##| napply daemon
   ##| napply daemon
   ##]
##] nqed.

nlemma getN_setN_overlap:
  ∀n1,n2,p1,p2,v,m.
  p1 ≠ p2 → 
  p2 ≤ p1 + Z_of_nat n1 →  p1 ≤ p2 + Z_of_nat n2 → 
  getN n2 p2 (setN n1 p1 v m) = Vundef.
#n1;#n2;#p1;#p2;#v;#m;
#H;#H1;#H2;
nchange in ⊢ (??(???%)?) with (update ????);
nwhd in ⊢(??%?);nrewrite > (update_o content ?????);
##[nlapply (Z_compare_to_Prop p2 p1);
   nlapply (refl ? (Z_compare p2 p1));
   ncases (Z_compare p2 p1) in ⊢ (???% → %);#H3;
   ##[nchange in ⊢ (% → ?) with (p2 < p1);#H4;
  (* [p1] belongs to [[p2, p2 + n2 - 1]], 
     therefore [check_cont n2 (p2 + 1) ...] is false. *)
     nrewrite > (check_cont_false …);
     ##[ncases (set_cont n1 (p1+oneZ) m p2)
        ##[##1,3:@
        ##|#n3;#v1;nwhd in ⊢ (??%?);
           ncases (eqb n2 n3);@ ##]
     ##|nrewrite > (update_s content …);napply nmk;
        #Hfalse;ndestruct
     ##|(*H2*) napply daemon
     ##|(*H4*) napply daemon
     ##|##skip ##]
  ##|nwhd in ⊢ (% → ?);#H4;nelim H;#H5;nelim (H5 ?);//;
  ##|nchange in ⊢ (% → ?) with (p1 < p2);#H4;
  (* [p2] belongs to [[p1 + 1, p1 + n1 - 1]],
     therefore [
     set_cont n1 (p1 + 1) m p2] is [Cont]. *)
     nrewrite > (set_cont_inside …);
     ##[@
     ##|(*H1*)napply daemon
     ##|(*H4*)napply daemon##]
  ##]
##|//##]
nqed.

nlemma getN_setN_mismatch:
  ∀n1,n2,p,v,m.
  n1 ≠ n2 → 
  getN n2 p (setN n1 p v m) = Vundef.
#n1;#n2;#p;#v;#m;#H;
nchange in ⊢ (??(???%)?) with (update ????);
nwhd in ⊢(??%?);nrewrite > (update_s content …);
nwhd in ⊢(??%?);nrewrite > (not_eq_to_eqb_false … (sym_neq … H));//;
nqed.

nlemma getN_setN_characterization:
  ∀m,v,n1,p1,n2,p2.
  getN n2 p2 (setN n1 p1 v m) = v
  ∨ getN n2 p2 (setN n1 p1 v m) = getN n2 p2 m
  ∨ getN n2 p2 (setN n1 p1 v m) = Vundef.
#m;#v;#n1;#p1;#n2;#p2;
nlapply (eqZb_to_Prop p1 p2); ncases (eqZb p1 p2); #Hp;
##[nrewrite > Hp;
   napply (eqb_elim n1 n2); #Hn;
   ##[nrewrite > Hn;@; @; //;
   ##|@2;/2/]
##|nlapply (Z_compare_to_Prop (p1 + n1) p2);
   ncases  (Z_compare (p1 + n1) p2);#Hcmp;
   ##[@;@2;napply getN_setN_other; /2/
   ##|nlapply (Z_compare_to_Prop (p2 + n2) p1);
      ncases  (Z_compare (p2 + n2) p1);#Hcmp2;
      ##[@;@2;napply getN_setN_other;/2/
      ##|@2;napply getN_setN_overlap;
         ##[//
         ##|##*:(* arith *) napply daemon]
      ##|@2;napply getN_setN_overlap;
         ##[//
         ##|##*:(* arith *) napply daemon]
      ##]
   ##|nlapply (Z_compare_to_Prop (p2 + n2) p1);
      ncases  (Z_compare (p2 + n2) p1);#Hcmp2;
      ##[@;@2;napply getN_setN_other;/2/
      ##|@2;napply getN_setN_overlap;
         ##[//
         ##|##*:(* arith *) napply daemon]
      ##|@2;napply getN_setN_overlap;
         ##[//
         ##|##*:(* arith *) napply daemon]
      ##]
   ##]
##]
nqed.

nlemma getN_init:
  ∀n,p.
  getN n p (λ_.Undef) = Vundef.
#n;#p;//;
nqed.

(* pointer_compat block_space pointer_space *)

ninductive pointer_compat : memory_space → memory_space → Prop ≝
|  same_compat : ∀s. pointer_compat s s
| pxdata_compat : pointer_compat PData XData
| unspecified_compat : ∀p. pointer_compat Any p
| universal_compat : ∀b. pointer_compat b Any.

nlemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
#b p; ncases b;
##[ ##1: @1; //;
##| ##*: ncases p; /2/; @2; @; #H; ninversion H; #e1 e2; ndestruct; #e3; ndestruct;
##] nqed.

ndefinition is_pointer_compat : memory_space → memory_space → bool ≝
λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].

(* [valid_access m chunk psp b ofs] holds if a memory access (load or store)
    of the given chunk is possible in [m] at address [b, ofs].
    This means:
- The block [b] is valid.
- The range of bytes accessed is within the bounds of [b].
- The offset [ofs] is aligned.
- The pointer classs [psp] is compatible with the class of [b].
*)

ninductive valid_access (m: mem) (chunk: memory_chunk) (psp: memory_space) (b: block) (ofs: Z) 
            : Prop ≝ 
  | valid_access_intro:
      valid_block m b → 
      low_bound m b ≤ ofs → 
      ofs + size_chunk chunk ≤ high_bound m b → 
      (align_chunk chunk ∣ ofs) → 
      pointer_compat (block_space m b) psp →
      valid_access m chunk psp b ofs.

(* The following function checks whether accessing the given memory chunk
  at the given offset in the given block respects the bounds of the block. *)

(* XXX: Using + and ¬ instead of Sum and Not causes trouble *)
nlet rec in_bounds 
  (m:mem) (chunk:memory_chunk) (psp:memory_space) (b:block) (ofs:Z) on b :  
    Sum (valid_access m chunk psp b ofs) (Not (valid_access m chunk psp b ofs)) ≝ ?.
napply (Zltb_elim_Type0 b (nextblock m)); #Hnext;
##[ napply (Zleb_elim_Type0 (low_bound m b) ofs); #Hlo;
    ##[ napply (Zleb_elim_Type0 (ofs + size_chunk chunk) (high_bound m b)); #Hhi;
        ##[ nelim (dec_dividesZ (align_chunk chunk) ofs); #Hal;
          ##[ ncases (pointer_compat_dec (block_space m b) psp); #Hcl;
            ##[ @1; @; // ##]
          ##]
        ##]
    ##]
##]
@2; napply nmk; *; #Hval; #Hlo'; #Hhi'; #Hal'; #Hcl'; napply (absurd ???); //;
nqed.

nlemma in_bounds_true:
  ∀m,chunk,psp,b,ofs. ∀A: Type[0]. ∀a1,a2: A.
  valid_access m chunk psp b ofs ->
  (match in_bounds m chunk psp b ofs with
   [ inl _ ⇒ a1 | inr _ ⇒ a2 ]) = a1.
#m chunk psp b ofs A a1 a2 H;
ncases (in_bounds m chunk psp b ofs);nnormalize;#H1;
##[//
##|nelim (?:False);napply (absurd ? H H1)]
nqed.

(* [valid_pointer] holds if the given block address is valid and the
  given offset falls within the bounds of the corresponding block. *)

ndefinition valid_pointer : mem → memory_space → block → Z → bool ≝
λm,psp,b,ofs. Zltb b (nextblock m) ∧
  Zleb (low_bound m b) ofs ∧
  Zltb ofs (high_bound m b) ∧
  is_pointer_compat (block_space m b) psp.

(* [load chunk m b ofs] perform a read in memory state [m], at address
  [b] and offset [ofs].  [None] is returned if the address is invalid
  or the memory access is out of bounds. *)

ndefinition load : memory_chunk → mem → memory_space → block → Z → option val ≝
λchunk,m,psp,b,ofs.
  match in_bounds m chunk psp b ofs with
  [ inl _ ⇒ Some ? (load_result chunk
           (getN (pred_size_chunk chunk) ofs (contents (blocks m b))))
  | inr _ ⇒ None ? ].

nlemma load_inv:
  ∀chunk,m,psp,b,ofs,v.
  load chunk m psp b ofs = Some ? v →
  valid_access m chunk psp b ofs ∧
  v = load_result chunk
           (getN (pred_size_chunk chunk) ofs (contents (blocks m b))).
#chunk m psp b ofs v; nwhd in ⊢ (??%? → ?);
ncases (in_bounds m chunk psp b ofs); #Haccess; nwhd in ⊢ ((??%?) → ?); #H;
##[ @;//; ndestruct; //;
##| ndestruct
##]
nqed.

(* [loadv chunk m addr] is similar, but the address and offset are given
  as a single value [addr], which must be a pointer value. *)

nlet rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝ 
  match addr with
  [ Vptr psp b ofs ⇒ load chunk m psp b (signed ofs)
  | _ ⇒ None ? ].

(* The memory state [m] after a store of value [v] at offset [ofs]
   in block [b]. *)

ndefinition unchecked_store : memory_chunk → mem → block → Z → val → mem ≝
λchunk,m,b,ofs,v.
  let c ≝ (blocks m b) in
  mk_mem
    (update ? b
        (mk_block_contents (low c) (high c)
                 (setN (pred_size_chunk chunk) ofs v (contents c)) (space c))
        (blocks m))
    (nextblock m)
    (nextblock_pos m).

(* [store chunk m b ofs v] perform a write in memory state [m].
  Value [v] is stored at address [b] and offset [ofs].
  Return the updated memory store, or [None] if the address is invalid
  or the memory access is out of bounds. *)

ndefinition store : memory_chunk → mem → memory_space → block → Z → val → option mem ≝ 
λchunk,m,psp,b,ofs,v.
  match in_bounds m chunk psp b ofs with
  [ inl _ ⇒ Some ? (unchecked_store chunk m b ofs v)
  | inr _ ⇒ None ? ].

nlemma store_inv:
  ∀chunk,m,psp,b,ofs,v,m'.
  store chunk m psp b ofs v = Some ? m' → 
  valid_access m chunk psp b ofs ∧
  m' = unchecked_store chunk m b ofs v.
#chunk m psp b ofs v m'; nwhd in ⊢ (??%? → ?);
(*9*)
ncases (in_bounds m chunk psp b ofs);#Hv;nwhd in ⊢(??%? → ?);#Heq;
##[@; ##[//|ndestruct;//]
##|ndestruct]
nqed.

(* [storev chunk m addr v] is similar, but the address and offset are given
  as a single value [addr], which must be a pointer value. *)

ndefinition storev : memory_chunk → mem → val → val → option mem ≝
λchunk,m,addr,v.
  match addr with
  [ Vptr psp b ofs ⇒ store chunk m psp b (signed ofs) v
  | _ ⇒ None ? ].


(* Build a block filled with the given initialization data. *)
ndefinition contents_init_data_step : 
  Z → init_data → (Z → contentmap) → contentmap ≝
  λpos,data,reccall.
  match data with
  [ Init_int8 n ⇒ 
      setN 0 pos (Vint n) (reccall (pos + oneZ))
  | Init_int16 n ⇒ 
      setN 1 pos (Vint n) (reccall (pos + oneZ))
  | Init_int32 n ⇒ 
      setN 3 pos (Vint n) (reccall (pos + oneZ))
  | Init_float32 f ⇒ 
      setN 3 pos (Vfloat f) (reccall (pos + oneZ))
  | Init_float64 f ⇒ 
      setN 7 pos (Vfloat f) (reccall (pos + oneZ))
  | Init_space n ⇒ reccall (pos + Zmax n 0) (*??*)
  | Init_addrof s n ⇒
      (* Not handled properly yet *)
      reccall (pos + 4)
  | Init_pointer x ⇒ 
      (* Not handled properly yet *)
      reccall (pos + 4)].

nlet rec contents_init_data (pos: Z) (i_data: list init_data) on i_data
  : contentmap ≝
  match i_data with
  [ nil ⇒ (λ_.Undef)
  | cons data i_data' ⇒ 
      contents_init_data_step pos data (λn.contents_init_data n i_data') ].

ndefinition size_init_data : init_data → Z ≝ 
 λi_data.match i_data with
  [ Init_int8 _ ⇒ 1
  | Init_int16 _ ⇒ 2
  | Init_int32 _ ⇒ 4
  | Init_float32 _ ⇒ 4
  | Init_float64 _ ⇒ 8
  | Init_space n ⇒ Zmax n 0
  | Init_addrof _ _ ⇒ 4
  | Init_pointer _ ⇒ Z_of_nat (*** can't use implicit coercion??? *)4].

ndefinition size_init_data_list : list init_data → Z ≝ 
  λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) OZ i_data.

nremark size_init_data_list_pos:
  ∀i_data. OZ ≤ size_init_data_list i_data.
#i_data;nelim i_data;//;
#a;#tl;ncut (OZ ≤ size_init_data a)
##[ncases a;nnormalize;//;
   #x;ncases x;nnormalize;//;
##|#Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl));
   ncut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m)
   ##[ncases (size_init_data a) in Hsize IH;
      ##[##1,2:/3/
      ##|nnormalize;#n;#Hfalse;nelim Hfalse]
   ##|#Hdisc;ncases Hdisc
      ##[#Heq;nrewrite > Heq;//;
      ##|#Heq;ncases Heq;#x;#Heq2;nrewrite > Heq2;
         (* TODO: arithmetics *) napply daemon]
   ##]
##]
nqed.

ndefinition block_init_data : list init_data → memory_space → block_contents ≝
  λi_data,bcl.mk_block_contents 
    OZ (size_init_data_list i_data) (contents_init_data OZ i_data) bcl.

ndefinition alloc_init_data : mem → list init_data → memory_space → mem × block ≝ 
  λm,i_data,bcl.
  〈mk_mem (update ? (nextblock m)
                 (block_init_data i_data bcl)
                 (blocks m))
         (Zsucc (nextblock m))
         (succ_nextblock_pos m),
   (nextblock m)〉.

nremark block_init_data_empty:
  ∀bcl. block_init_data [ ] bcl = empty_block OZ OZ bcl.
//;
nqed.

(* * Properties of the memory operations *)

(* ** Properties related to block validity *)

nlemma valid_not_valid_diff:
  ∀m,b,b'. valid_block m b →  ¬(valid_block m b') → b ≠ b'.
#m;#b;#b';#H;#H';napply nmk;#e;nrewrite > e in H;#H;
napply (absurd ? H H');
nqed.

nlemma valid_access_valid_block:
  ∀m,chunk,psp,b,ofs. valid_access m chunk psp b ofs → valid_block m b.
#m;#chunk;#psp;#b;#ofs;#H;
nelim H;//;
nqed.

nlemma valid_access_aligned:
  ∀m,chunk,psp,b,ofs.
  valid_access m chunk psp b ofs → (align_chunk chunk ∣ ofs).
#m;#chunk;#psp;#b;#ofs;#H;
nelim H;//;
nqed.

nlemma valid_access_compat:
  ∀m,chunk1,chunk2,psp,b,ofs.
  size_chunk chunk1 = size_chunk chunk2 →
  valid_access m chunk1 psp b ofs →
  valid_access m chunk2 psp b ofs.
#m;#chunk;#chunk2;#psp;#b;#ofs;#H1;#H2;
nelim H2;#H3;#H4;#H5;#H6;#H7;
nrewrite > H1 in H5;#H5;
@;//;
nrewrite < (align_chunk_compat … H1);//;
nqed.

(* Hint Resolve valid_not_valid_diff valid_access_valid_block valid_access_aligned: mem.*)

(* ** Properties related to [load] *)

ntheorem valid_access_load:
  ∀m,chunk,psp,b,ofs.
  valid_access m chunk psp b ofs → 
  ∃v. load chunk m psp b ofs = Some ? v.
#m;#chunk;#psp;#b;#ofs;#H;@;
##[##2:nwhd in ⊢ (??%?);napply in_bounds_true;//;
##|##skip]
nqed.

ntheorem load_valid_access:
  ∀m,chunk,psp,b,ofs,v.
  load chunk m psp b ofs = Some ? v →
  valid_access m chunk psp b ofs.
#m;#chunk;#psp;#b;#ofs;#v;#H;
ncases (load_inv … H);//;
nqed.

(* Hint Resolve load_valid_access valid_access_load.*)

(* ** Properties related to [store] *)

nlemma valid_access_store:
  ∀m1,chunk,psp,b,ofs,v.
  valid_access m1 chunk psp b ofs →
  ∃m2. store chunk m1 psp b ofs v = Some ? m2.
#m1;#chunk;#psp;#b;#ofs;#v;#H;
@;
##[##2:napply in_bounds_true;//
##|##skip]
nqed.

(* section STORE *)

nlemma low_bound_store:
  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
  ∀b'.low_bound m2 b' = low_bound m1 b'.
#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
#b';ncases (store_inv … STORE);
#H1;#H2;nrewrite > H2;
nwhd in ⊢ (??(?%?)?);nwhd in ⊢ (??%?);
nwhd in ⊢ (??(?%)?);nlapply (eqZb_to_Prop b' b);
ncases (eqZb b' b);nnormalize;//;
nqed.

nlemma nextblock_store :
  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
  nextblock m2 = nextblock m1.
#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
ncases (store_inv … STORE);
#Hvalid;#Heq;
nrewrite > Heq;@;
nqed.

nlemma high_bound_store:
  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
  ∀b'. high_bound m2 b' = high_bound m1 b'.
#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
#b';ncases (store_inv … STORE);
#Hvalid;#H;
nrewrite > H;
nwhd in ⊢ (??(?%?)?);nwhd in ⊢ (??%?);
nwhd in ⊢ (??(?%)?);nlapply (eqZb_to_Prop b' b);
ncases (eqZb b' b);nnormalize;//;
nqed.

nlemma memory_space_store:
  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
  ∀b'. block_space m2 b' = block_space m1 b'.
#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
#b';ncases (store_inv … STORE);
#Hvalid;#H;
nrewrite > H;
nwhd in ⊢ (??(?%?)?);nwhd in ⊢ (??%?);
nwhd in ⊢ (??(?%)?);nlapply (eqZb_to_Prop b' b);
ncases (eqZb b' b);nnormalize;//;
nqed.

nlemma store_valid_block_1:
  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
  ∀b'. valid_block m1 b' → valid_block m2 b'.
#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
#b';nwhd in ⊢ (% → %);#Hv;
nrewrite > (nextblock_store … STORE);//;
nqed.

nlemma store_valid_block_2:
  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
  ∀b'. valid_block m2 b' → valid_block m1 b'.
#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
#b';nwhd in ⊢ (%→%);
nrewrite > (nextblock_store … STORE);//;
nqed.

(*Hint Resolve store_valid_block_1 store_valid_block_2: mem.*)

nlemma store_valid_access_1:
  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
  ∀chunk',psp',b',ofs'.
  valid_access m1 chunk' psp' b' ofs' → valid_access m2 chunk' psp' b' ofs'.
#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
#chunk';#psp';#b';#ofs';
* Hv;
#Hvb;#Hl;#Hr;#Halign;#Hptr;
@;//;
##[napply (store_valid_block_1 … STORE);//
##|nrewrite > (low_bound_store … STORE …);//
##|nrewrite > (high_bound_store … STORE …);//
##|nrewrite > (memory_space_store … STORE …);//]
nqed.

nlemma store_valid_access_2:
  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
  ∀chunk',psp',b',ofs'.
  valid_access m2 chunk' psp' b' ofs' → valid_access m1 chunk' psp' b' ofs'.
#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
#chunk';#psp';#b';#ofs';
* Hv;
#Hvb;#Hl;#Hr;#Halign;#Hcompat;
@;//;
##[napply (store_valid_block_2 … STORE);//
##|nrewrite < (low_bound_store … STORE …);//
##|nrewrite < (high_bound_store … STORE …);//
##|nrewrite < (memory_space_store … STORE …);//]
nqed.

nlemma store_valid_access_3:
  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
  valid_access m1 chunk psp b ofs.
#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
ncases (store_inv … STORE);//;
nqed.

(*Hint Resolve store_valid_access_1 store_valid_access_2
             store_valid_access_3: mem.*)

nlemma load_compat_pointer:
  ∀chunk,m,psp,psp',b,ofs,v.
  pointer_compat (block_space m b) psp' →
  load chunk m psp b ofs = Some ? v →
  load chunk m psp' b ofs = Some ? v.
#chunk m psp psp' b ofs v Hcompat LOAD.
nlapply (load_valid_access … LOAD); #Hvalid;
ncut (valid_access m chunk psp' b ofs);
##[ @;nelim Hvalid; //;
##| #Hvalid';
    nrewrite < LOAD; nwhd in ⊢ (??%%);
    nrewrite > (in_bounds_true … (option val) ?? Hvalid);
    nrewrite > (in_bounds_true … (option val) ?? Hvalid');
    //
##] nqed.

ntheorem load_store_similar:
  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
  ∀chunk'.
  size_chunk chunk' = size_chunk chunk →
  load chunk' m2 psp b ofs = Some ? (load_result chunk' v).
#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
#chunk';#Hsize;ncases (store_inv … STORE);
#Hv;#Heq;
nwhd in ⊢ (??%?);
nrewrite > (in_bounds_true m2 chunk' psp b ofs ? (Some ? (load_result chunk' (getN (pred_size_chunk chunk') ofs (contents (blocks m2 b))))) 
               (None ?) ?);
##[nrewrite > Heq;
   nwhd in ⊢ (??(??(? ? (? ? ? (? (? % ?)))))?);
   nrewrite > (update_s ? b ? (blocks m1)); (* XXX  too many metas for my taste *)
   nrewrite > (? : pred_size_chunk chunk = pred_size_chunk chunk');
   ##[//;
   ##|nrewrite > (size_chunk_pred …) in Hsize;#Hsize;
      nrewrite > (size_chunk_pred …) in Hsize;#Hsize;
      napply injective_Z_of_nat;napply (injective_Zplus_r 1);//;##]
##|napply (store_valid_access_1 … STORE);
   ncases Hv;#H1;#H2;#H3;#H4;#H5;@;//;
   nrewrite > (align_chunk_compat … Hsize);//]
nqed.

ntheorem load_store_same:
  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
  load chunk m2 psp b ofs = Some ? (load_result chunk v).
#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
napply load_store_similar;//;
nqed.
        
ntheorem load_store_other:
  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
  ∀chunk',psp',b',ofs'.
  b' ≠ b
  ∨ ofs' + size_chunk chunk' ≤  ofs
  ∨ ofs + size_chunk chunk ≤ ofs' → 
  load chunk' m2 psp' b' ofs' = load chunk' m1 psp' b' ofs'.
#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
#chunk';#psp';#b';#ofs';#H;
ncases (store_inv … STORE);
#Hvalid;#Heq;nwhd in ⊢ (??%%);
ncases (in_bounds m1 chunk' psp' b' ofs');
##[#Hvalid1;nrewrite > (in_bounds_true m2 chunk' psp' b' ofs' ? (Some ? ?) ??);
   ##[nwhd in ⊢ (???%); napply (eq_f … (Some val));napply (eq_f … (load_result chunk'));
      nrewrite > Heq;nwhd in ⊢ (??(???(? (? % ?)))?);
                     nwhd in ⊢ (??(???(? %))?);
      nlapply (eqZb_to_Prop b' b);ncases (eqZb b' b);
      nwhd in ⊢ (% → ?);
      ##[#Heq1;nrewrite > Heq1;nwhd in ⊢ (??(??? (? %))?);
         nrewrite > (size_chunk_pred …) in H;
         nrewrite > (size_chunk_pred …);#H;
         napply (getN_setN_other …);ncases H
         ##[*
            ##[#Hfalse;nelim Hfalse;#H1;nelim (H1 Heq1)
            ##|#H1;@2;(*H1*)napply daemon ##]
         ##|#H1;@;(*H1*)napply daemon ##]
      ##|#Hneq;@ ##]
   ##|napply (store_valid_access_1 … STORE);//##]
##|nwhd in ⊢ (? → ???%);nlapply (in_bounds m2 chunk' psp' b' ofs');
   #H1;ncases H1;
   ##[#H2;#H3;nlapply (store_valid_access_2 … STORE … H2);#Hfalse;
      ncases H3;#H4;nelim (H4 Hfalse)
   ##|#H2;#H3;@]
##]
nqed.


ntheorem load_store_overlap:
  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
  ∀chunk',ofs',v'. load chunk' m2 psp b ofs' = Some ? v' →
  ofs' ≠ ofs → 
  ofs < ofs' + size_chunk chunk' → 
  ofs' < ofs + size_chunk chunk → 
  v' = Vundef.
#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
#chunk';#ofs';#v';#H;
#H1;#H2;#H3;
ncases (store_inv … STORE);
ncases (load_inv … H);
#Hvalid;#Heq;#Hvalid1;#Heq1;nrewrite > Heq;nrewrite > Heq1;
nchange in ⊢ (??(??(???(?(?%?))))?) with (mk_mem ???);
nrewrite > (update_s block_contents …);
nrewrite > (getN_setN_overlap …);
##[ncases chunk';//
##|nrewrite > (size_chunk_pred …) in H2;(*arith*) napply daemon
##|nrewrite > (size_chunk_pred …) in H3;(*arith*) napply daemon
##|napply sym_neq;//]
nqed.

ntheorem load_store_overlap':
  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
  ∀chunk',ofs'.
  valid_access m1 chunk' psp b ofs' → 
  ofs' ≠ ofs → 
  ofs < ofs' + size_chunk chunk' → 
  ofs' < ofs + size_chunk chunk → 
  load chunk' m2 psp b ofs' = Some ? Vundef.
#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
#chunk';#ofs';#Hvalid;#H;#H1;#H2;
ncut (∃v'.load chunk' m2 psp b ofs' = Some ? v')
##[napply valid_access_load;
   napply (store_valid_access_1 … STORE);//
##|#H3;ncases H3;
   #x;#Hx;nrewrite > Hx;napply (eq_f … (Some val));
   napply (load_store_overlap … STORE … Hx);//;##]
nqed.

ntheorem load_store_mismatch:
  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
  ∀chunk',v'.
  load chunk' m2 psp b ofs = Some ? v' →
  size_chunk chunk' ≠ size_chunk chunk → 
  v' = Vundef.
#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
#chunk';#v';#H;#H1;
ncases (store_inv … STORE);
ncases (load_inv … H);
#Hvalid;#H2;#Hvalid1;#H3;
nrewrite > H2;
nchange in H3:(???%) with (mk_mem ???);
nrewrite > H3;nrewrite > (update_s block_contents …);
nrewrite > (getN_setN_mismatch …);
##[ncases chunk';//;
##|nrewrite > (size_chunk_pred …) in H1;nrewrite > (size_chunk_pred …);
   #H1;napply nmk;#Hfalse;nelim H1;#H4;napply H4;
   napply (eq_f ?? (λx.1 + x) ???);//##]
nqed.

ntheorem load_store_mismatch':
  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
  ∀chunk'.
  valid_access m1 chunk' psp b ofs →
  size_chunk chunk' ≠ size_chunk chunk → 
  load chunk' m2 psp b ofs = Some ? Vundef.
#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
#chunk';#Hvalid;#Hsize;
ncut (∃v'.load chunk' m2 psp b ofs = Some ? v')
##[napply (valid_access_load …);
   napply
    (store_valid_access_1 … STORE);//
##|*;#x;#Hx;nrewrite > Hx;napply (eq_f … (Some val));
   napply (load_store_mismatch … STORE … Hsize);//;##]
nqed.

ninductive load_store_cases 
      (chunk1: memory_chunk) (b1: block) (ofs1: Z)
      (chunk2: memory_chunk) (b2: block) (ofs2: Z) : Type ≝
  | lsc_similar:
      b1 = b2 → ofs1 = ofs2 → size_chunk chunk1 = size_chunk chunk2 →
      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2
  | lsc_other:
      b1 ≠ b2 ∨ ofs2 + size_chunk chunk2 ≤ ofs1 ∨ ofs1 + size_chunk chunk1 ≤ ofs2 →
      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2
  | lsc_overlap:
      b1 = b2 -> ofs1 ≠ ofs2 -> ofs1 < ofs2 + size_chunk chunk2 → ofs2 < ofs1 + size_chunk chunk1 ->
      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2
  | lsc_mismatch:
      b1 = b2 → ofs1 = ofs2 → size_chunk chunk1 ≠ size_chunk chunk2 ->
      load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2.

ndefinition load_store_classification:
  ∀chunk1,b1,ofs1,chunk2,b2,ofs2.
  load_store_cases chunk1 b1 ofs1 chunk2 b2 ofs2.
#chunk1;#b1;#ofs1;#chunk2;#b2;#ofs2;
ncases (decidable_eq_Z_Type b1 b2);#H;
##[ncases (decidable_eq_Z_Type ofs1 ofs2);#H1;
   ##[ncases (decidable_eq_Z_Type (size_chunk chunk1) (size_chunk chunk2));#H2
      ##[napply lsc_similar;//;
      ##|napply lsc_mismatch;//;##]
   ##|nlapply (Z_compare_to_Prop (ofs2 + size_chunk chunk2) ofs1);
      ncases (Z_compare (ofs2+size_chunk chunk2) ofs1);
      ##[nchange with (Zlt ? ? → ?);#H2;
         napply lsc_other;@;@2;(*trivial Zlt_to_Zle BUT the statement is strange*)
         napply daemon
      ##|nchange with (? = ? → ?);#H2;
         napply lsc_other;@;@2;(*trivial eq_to_Zle not defined *) napply daemon
      ##|nchange with (Zlt ? ? → ?);#H2;
         nlapply (Z_compare_to_Prop (ofs1 + size_chunk chunk1) ofs2);
         ncases (Z_compare (ofs1 + size_chunk chunk1) ofs2);
         ##[nchange with (Zlt ? ? → ?);#H3;
            napply lsc_other;@2;(*trivial as previously*) napply daemon
         ##|nchange with (? = ? → ?);#H3;
            napply lsc_other;@2;(*trivial as previously*) napply daemon
         ##|nchange with (Zlt ? ? → ?);#H3;
            napply lsc_overlap;//;##]
      ##]
   ##]
##|napply lsc_other;@;@; (* XXX // doesn't spot this! *) napply H ##]
nqed.

ntheorem load_store_characterization:
  ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 →
  ∀chunk',psp',b',ofs'.
  valid_access m1 chunk' psp' b' ofs' →
  load chunk' m2 psp' b' ofs' =
    match load_store_classification chunk b ofs chunk' b' ofs' with
    [ lsc_similar _ _ _ ⇒ Some ? (load_result chunk' v)
    | lsc_other _ ⇒ load chunk' m1 psp' b' ofs'
    | lsc_overlap _ _ _ _ ⇒ Some ? Vundef
    | lsc_mismatch _ _ _ ⇒ Some ? Vundef ].
#chunk;#m1;#psp b ofs;#v;#m2;#STORE;
#chunk';#psp';#b';#ofs';#Hvalid;
ncut (∃v'. load chunk' m2 psp' b' ofs' = Some ? v')
##[napply valid_access_load;
   napply (store_valid_access_1 … STORE … Hvalid);
##|*;#x;#Hx;
   ncases (load_store_classification chunk b ofs chunk' b' ofs')
   ##[#H1;#H2;#H3;nwhd in ⊢ (???%);nrewrite < H1;nrewrite < H2;
      napply (load_compat_pointer … psp);
      ##[ nrewrite > (memory_space_store … STORE b);
          ncases Hvalid; //;
      ##| napply (load_store_similar … STORE);//;
      ##]
   ##|#H1;napply (load_store_other … STORE);
      ncases H1
      ##[*
         ##[#H2;@;@;napply sym_neq;//
         ##|#H2;@;@2;//]
      ##|#H2;@2;//]
   ##|#H1;#H2;#H3;#H4; nlapply (load_compat_pointer … psp … Hx);
     ##[ nrewrite > (memory_space_store … STORE b');
         nrewrite > H1; nelim (store_valid_access_3 … STORE); //
     ##| nrewrite < H1 in ⊢ (% → ?);#Hx';
         nrewrite < H1 in Hx;#Hx;nrewrite > Hx;
      napply (eq_f … (Some val));napply (load_store_overlap … STORE … Hx');/2/;
     ##]
   ##|#H1;#H2;#H3;
       nlapply (load_compat_pointer … psp … Hx);
       ##[ nrewrite > (memory_space_store … STORE b');
           nrewrite > H1; nelim (store_valid_access_3 … STORE); //
       ##| nrewrite < H1 in Hx ⊢ %; nrewrite < H2; #Hx Hx';
           nrewrite > Hx;napply (eq_f … (Some val));
           napply (load_store_mismatch … STORE … Hx');/2/
       ##]
   ##]
           
##]
nqed.

(*nlemma d : ∀a,b,c,d:nat.∀e:〈a,b〉 = 〈c,d〉. ∀P:(∀a,b,c,d,e.Prop).
           P a b c d e → P a b a b (refl ??).
#a;#b;#c;#d;#e;#P;#H1;ndestruct;*)

(*
Section ALLOC.

Variable m1: mem.
Variables lo hi: Z.
Variable m2: mem.
Variable b: block.
Hypothesis ALLOC: alloc m1 lo hi = (m2, b).
*)

ndefinition pairdisc ≝ 
λA,B.λx,y:pair A B.
match x with 
[(mk_pair t0 t1) ⇒ 
match y with 
[(mk_pair u0 u1) ⇒ 
  ∀P: Type[1].
  (∀e0: (eq A (R0 ? t0) u0).
   ∀e1: (eq (? u0 e0) (R1 ? t0 ? t1 u0 e0) u1).P) → P ] ].

nlemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y.
#A;#B;#x;#y;#e;nrewrite > e;ncases y;
#a;#b;nnormalize;#P;#PH;napply PH;@;
nqed.

nlemma nextblock_alloc:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  nextblock m2 = Zsucc (nextblock m1).
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
nwhd in ALLOC:(??%%); ndestruct; //;
nqed.

nlemma alloc_result:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  b = nextblock m1.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
nwhd in ALLOC:(??%%); ndestruct; //;
nqed.


nlemma valid_block_alloc:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀b'. valid_block m1 b' → valid_block m2 b'.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
#b'; nrewrite > (unfold_valid_block m1 b');
nrewrite > (unfold_valid_block m2 b');
nrewrite > (nextblock_alloc … ALLOC);
(* arith *) napply daemon;
nqed.

nlemma fresh_block_alloc:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ¬(valid_block m1 b).
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
nrewrite > (unfold_valid_block m1 b);
nrewrite > (alloc_result … ALLOC);
(* arith *) napply daemon;
nqed.

nlemma valid_new_block:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  valid_block m2 b.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
nrewrite > (unfold_valid_block m2 b);
nrewrite > (alloc_result … ALLOC);
nrewrite > (nextblock_alloc … ALLOC);
(* arith *) napply daemon;
nqed.

(*
Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.
*)

nlemma valid_block_alloc_inv:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀b'. valid_block m2 b' → b' = b ∨ valid_block m1 b'.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
#b';
nrewrite > (unfold_valid_block m2 b');
nrewrite > (unfold_valid_block m1 b');
nrewrite > (nextblock_alloc … ALLOC); #H;
nrewrite > (alloc_result … ALLOC);
(* arith *) napply daemon;
nqed.

nlemma low_bound_alloc:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀b'. low_bound m2 b' = if eqZb b' b then lo else low_bound m1 b'.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
nwhd in ALLOC:(??%%); ndestruct; #b';
nrewrite > (unfold_update block_contents ????);
ncases (eqZb b' (nextblock m1)); //;
nqed.

nlemma low_bound_alloc_same:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  low_bound m2 b = lo.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
nrewrite > (low_bound_alloc … ALLOC b);
nrewrite > (eqZb_z_z …);
//;
nqed.

nlemma low_bound_alloc_other:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀b'. valid_block m1 b' → low_bound m2 b' = low_bound m1 b'.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
#b'; nrewrite > (low_bound_alloc … ALLOC b');
napply eqZb_elim; #Hb;
##[ nrewrite > Hb; #bad; napply False_ind; napply (absurd ? bad);
    napply (fresh_block_alloc … ALLOC)
##| //
##] nqed.

nlemma high_bound_alloc:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀b'. high_bound m2 b' = if eqZb b' b then hi else high_bound m1 b'.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
nwhd in ALLOC:(??%%); ndestruct; #b'; 
nrewrite > (unfold_update block_contents ????);
ncases (eqZb b' (nextblock m1)); //;
nqed.

nlemma high_bound_alloc_same:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  high_bound m2 b = hi.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
nrewrite > (high_bound_alloc … ALLOC b);
nrewrite > (eqZb_z_z …);
//;
nqed.

nlemma high_bound_alloc_other:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀b'. valid_block m1 b' → high_bound m2 b' = high_bound m1 b'.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
#b'; nrewrite > (high_bound_alloc … ALLOC b');
napply eqZb_elim; #Hb;
##[ nrewrite > Hb; #bad; napply False_ind; napply (absurd ? bad);
    napply (fresh_block_alloc … ALLOC)
##| //
##] nqed.

nlemma class_alloc:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀b'.block_space m2 b' = if eqZb b' b then bcl else block_space m1 b'.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
nwhd in ALLOC:(??%%); ndestruct; #b';
ncases (eqZb b' (nextblock m1)); //;
nqed.

nlemma class_alloc_same:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  block_space m2 b = bcl.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
nwhd in ALLOC:(??%%); ndestruct;
nrewrite > (eqZb_z_z ?); //;
nqed.

nlemma class_alloc_other:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀b'. valid_block m1 b' → block_space m2 b' = block_space m1 b'.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
#b'; nrewrite > (class_alloc … ALLOC b');
napply eqZb_elim; #Hb;
##[ nrewrite > Hb; #bad; napply False_ind; napply (absurd ? bad);
    napply (fresh_block_alloc … ALLOC)
##| //
##] nqed.

nlemma valid_access_alloc_other:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀chunk,psp,b',ofs.
  valid_access m1 chunk psp b' ofs →
  valid_access m2 chunk psp b' ofs.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
#chunk;#psp;#b';#ofs;#H;
ncases H; #Hvalid; #Hlow; #Hhigh;#Halign;#Hcompat;
@;
##[ napply (valid_block_alloc … ALLOC); //
##| nrewrite > (low_bound_alloc_other … ALLOC b' Hvalid); //
##| nrewrite > (high_bound_alloc_other … ALLOC b' Hvalid); //
##| //
##| nrewrite > (class_alloc_other … ALLOC b' Hvalid); //;
##] nqed.

nlemma valid_access_alloc_same:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀chunk,psp,ofs.
  lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) →
  pointer_compat bcl psp →
  valid_access m2 chunk psp b ofs.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
#chunk;#psp;#ofs; #Hlo; #Hhi; #Halign; #Hcompat;
@;
##[ napply (valid_new_block … ALLOC)
##| nrewrite > (low_bound_alloc_same … ALLOC); //
##| nrewrite > (high_bound_alloc_same … ALLOC); //
##| //
##| nrewrite > (class_alloc_same … ALLOC); //
##] nqed.

(*
Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem.
*)

nlemma valid_access_alloc_inv:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀chunk,psp,b',ofs.
  valid_access m2 chunk psp b' ofs →
  valid_access m1 chunk psp b' ofs ∨
  (b' = b ∧ lo ≤ ofs ∧ (ofs + size_chunk chunk ≤ hi ∧ (align_chunk chunk ∣ ofs) ∧ pointer_compat bcl psp)).
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
#chunk;#psp;#b';#ofs;*;#Hblk;#Hlo;#Hhi;#Hal;#Hct;
nelim (valid_block_alloc_inv … ALLOC ? Hblk);#H;
##[ nrewrite < H in ALLOC ⊢ %; #ALLOC';
    nrewrite > (low_bound_alloc_same … ALLOC') in Hlo; #Hlo';
    nrewrite > (high_bound_alloc_same … ALLOC') in Hhi; #Hhi';
    nrewrite > (class_alloc_same … ALLOC') in Hct; #Hct;
    @2; /4/;
##| @1;@;//;
  ##[ nrewrite > (low_bound_alloc_other … ALLOC ??) in Hlo; //
  ##| nrewrite > (high_bound_alloc_other … ALLOC ??) in Hhi; //
  ##| nrewrite > (class_alloc_other … ALLOC ??) in Hct; //
  ##]
##] nqed.

ntheorem load_alloc_unchanged:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo bcl hi = 〈m2,b〉 →
  ∀chunk,psp,b',ofs.
  valid_block m1 b' →
  load chunk m2 psp b' ofs = load chunk m1 psp b' ofs.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
#chunk;#psp;#b';#ofs;#H;nwhd in ⊢ (??%%);
ncases (in_bounds m2 chunk psp b' ofs); #H';
##[ nelim (valid_access_alloc_inv … ALLOC ???? H');
  ##[ #H''; (* XXX: if there's no hint that the result type is an option then the rewrite fails with an odd type error
  nrewrite > (in_bounds_true ???? ??? H''); *) nrewrite > (in_bounds_true … ? (option val) ?? H'');
      nwhd in ⊢ (??%?); (* XXX: if you do this at the point below the proof term is ill-typed. *)
      ncut (b' ≠ b);
      ##[ napply (valid_not_valid_diff … H); napply (fresh_block_alloc … ALLOC);
      ##| nwhd in ALLOC:(??%%); ndestruct; 
          nrewrite > (update_o block_contents ?????); /2/;
      ##]
  ##| *;*;#A;#B;#C; nrewrite < A in ALLOC ⊢ %; #ALLOC;
      napply False_ind; napply (absurd ? H); napply (fresh_block_alloc … ALLOC)
  ##]
##| ncases (in_bounds m1 chunk psp b' ofs); #H''; nwhd in ⊢ (??%%); //;
    napply False_ind; napply (absurd ? ? H'); napply (valid_access_alloc_other … ALLOC); //
##] nqed.
  
ntheorem load_alloc_other:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀chunk,psp,b',ofs,v.
  load chunk m1 psp b' ofs = Some ? v →
  load chunk m2 psp b' ofs = Some ? v.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
#chunk;#psp;#b';#ofs;#v;#H;
nrewrite < H; napply (load_alloc_unchanged … ALLOC ???); ncases (load_valid_access … H); //;
nqed.

ntheorem load_alloc_same:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀chunk,psp,ofs,v.
  load chunk m2 psp b ofs = Some ? v →
  v = Vundef.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
#chunk;#psp;#ofs;#v;#H;
nelim (load_inv … H); #H0; #H1; nrewrite > H1;
 nwhd in ALLOC:(??%%); (* XXX ndestruct; ??? *) napply (pairdisc_elim … ALLOC);
 nwhd in ⊢ (??%% → ?);#e0;nrewrite < e0 in ⊢ (%→?);
 nwhd in ⊢ (??%% → ?);#e1;
nrewrite < e1; nrewrite < e0; nrewrite > (update_s ? ? (empty_block lo hi bcl) ?);
nnormalize; ncases chunk; //;
nqed.

ntheorem load_alloc_same':
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀chunk,psp,ofs.
  lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) →
  pointer_compat bcl psp →
  load chunk m2 psp b ofs = Some ? Vundef.
#m1;#lo;#hi;#bcl;#m2;#b;#ALLOC;
#chunk;#psp;#ofs;#Hlo;#Hhi;#Hal;#Hct;
ncut (∃v. load chunk m2 psp b ofs = Some ? v);
##[ napply valid_access_load; @; //;
  ##[ napply (valid_new_block … ALLOC);
  ##| nrewrite > (low_bound_alloc_same … ALLOC); //
  ##| nrewrite > (high_bound_alloc_same … ALLOC); //
  ##| nrewrite > (class_alloc_same … ALLOC); //
  ##]
##| *; #v;#LOAD; nrewrite > LOAD; napply (eq_f … (Some val));
    napply (load_alloc_same … ALLOC … LOAD);
##] nqed.

(*
End ALLOC.

Hint Resolve valid_block_alloc fresh_block_alloc valid_new_block: mem.
Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem.
Hint Resolve load_alloc_unchanged: mem.

*)

(* ** Properties related to [free]. *)
(*
Section FREE.

Variable m: mem.
Variable bf: block.
*)

nlemma valid_block_free_1:
  ∀m,bf,b. valid_block m b → valid_block (free m bf) b.
nnormalize;//;
nqed.

nlemma valid_block_free_2:
  ∀m,bf,b. valid_block (free m bf) b → valid_block m b.
nnormalize;//;
nqed.

(*
Hint Resolve valid_block_free_1 valid_block_free_2: mem.
*)

nlemma low_bound_free:
  ∀m,bf,b. b ≠ bf -> low_bound (free m bf) b = low_bound m b.
#m;#bf;#b;#H;nwhd in ⊢ (??%%); nwhd in ⊢ (??(?(?%?))?);
nrewrite > (update_o block_contents …); //; napply sym_neq; //;
nqed.

nlemma high_bound_free:
  ∀m,bf,b. b ≠ bf → high_bound (free m bf) b = high_bound m b.
#m;#bf;#b;#H;nwhd in ⊢ (??%%); nwhd in ⊢ (??(?(?%?))?);
nrewrite > (update_o block_contents …); //; napply sym_neq; //;
nqed.

nlemma low_bound_free_same:
  ∀m,b. low_bound (free m b) b = 0.
#m;#b;nwhd in ⊢ (??%%); nwhd in ⊢ (??(?(?%?))?);
nrewrite > (update_s block_contents …); //;
nqed.

nlemma high_bound_free_same:
  ∀m,b. high_bound (free m b) b = 0.
#m;#b;nwhd in ⊢ (??%%); nwhd in ⊢ (??(?(?%?))?);
nrewrite > (update_s block_contents …); //;
nqed.

nlemma class_free:
  ∀m,bf,b. b ≠ bf → block_space (free m bf) b = block_space m b.
#m;#bf;#b;#H;nwhd in ⊢ (??%%); nwhd in ⊢ (??(?(?%?))?);
nrewrite > (update_o block_contents …); //; napply sym_neq; //;
nqed.

nlemma valid_access_free_1:
  ∀m,bf,chunk,psp,b,ofs.
  valid_access m chunk psp b ofs → b ≠ bf →
  valid_access (free m bf) chunk psp b ofs.
#m;#bf;#chunk;#psp b ofs;*;#Hval;#Hlo;#Hhi;#Hal;#Hcompat;#Hneq;
@; //;
##[ napply valid_block_free_1; //
##| nrewrite > (low_bound_free … Hneq); //
##| nrewrite > (high_bound_free … Hneq); //
##| nrewrite > (class_free … Hneq); //
##] nqed.

nlemma valid_access_free_2:
  ∀m,psp,bf,chunk,ofs. ¬(valid_access (free m bf) chunk psp bf ofs).
#m;#psp;#bf;#chunk;#ofs; napply nmk; *; #Hval;#Hlo;#Hhi;#Hal;#Hct;
nwhd in Hlo:(?%?);nwhd in Hlo:(?(?(?%?))?); nrewrite > (update_s block_contents …) in Hlo;
nwhd in Hhi:(??%);nwhd in Hhi:(??(?(?%?))); nrewrite > (update_s block_contents …) in Hhi;
nwhd in ⊢ ((??%)→(?%?)→?); (* arith *) napply daemon;
nqed.

(*
Hint Resolve valid_access_free_1 valid_access_free_2: mem.
*)

nlemma valid_access_free_inv:
  ∀m,bf,chunk,psp,b,ofs.
  valid_access (free m bf) chunk psp b ofs →
  valid_access m chunk psp b ofs ∧ b ≠ bf.
#m;#bf;#chunk;#psp b ofs; nelim (decidable_eq_Z_Type b bf);
##[ #e; nrewrite > e;
    #H; napply False_ind; napply (absurd ? H (valid_access_free_2 …));
##| #ne; *; nrewrite > (low_bound_free … ne);
    nrewrite > (high_bound_free … ne);
    nrewrite > (class_free … ne);
    #Hval; #Hlo; #Hhi; #Hal; #Hct;
    @; ##[ @; /2/; ##| /2/ ##]
##] nqed.

ntheorem load_free:
  ∀m,bf,chunk,psp,b,ofs.
  b ≠ bf →
  load chunk (free m bf) psp b ofs = load chunk m psp b ofs.
#m;#bf;#chunk;#psp b ofs;#ne; nwhd in ⊢ (??%%);
nelim (in_bounds m chunk psp b ofs);
##[ #Hval; nwhd in ⊢ (???%); nrewrite > (in_bounds_true ????? (option val) ???);
  ##[ nwhd in ⊢ (??(??(??(???(?(?%?)))))?); nrewrite > (update_o block_contents …); //;
      napply sym_neq; //
  ##| napply valid_access_free_1; //; napply ne;
  ##]
##| nelim (in_bounds (free m bf) chunk psp b ofs); (* XXX just // used to work *) ##[ ##2: nnormalize; //; ##]
    #H;#H'; napply False_ind; napply (absurd ? ? H');
    nelim (valid_access_free_inv …H); //;
##] nqed.

(*
End FREE.
*)

(* ** Properties related to [free_list] *)

nlemma valid_block_free_list_1:
  ∀bl,m,b. valid_block m b → valid_block (free_list m bl) b.
#bl;nelim bl;
##[ #m;#b;#H; nwhd in ⊢ (?%?); //
##| #h;#t;#IH;#m;#b;#H; nrewrite > (unfold_free_list m h t);
    napply valid_block_free_1; napply IH; //
##] nqed.

nlemma valid_block_free_list_2:
  ∀bl,m,b. valid_block (free_list m bl) b → valid_block m b.
#bl; nelim bl;
##[ #m;#b;#H; nwhd in H:(?%?); //
##| #h;#t;#IH;#m;#b; nrewrite > (unfold_free_list m h t);#H;
    napply IH; napply valid_block_free_2; //
##] nqed.

nlemma valid_access_free_list:
  ∀chunk,psp,b,ofs,m,bl.
  valid_access m chunk psp b ofs → ¬in_list ? b bl →
  valid_access (free_list m bl) chunk psp b ofs.
#chunk; #psp b ofs; #m; #bl; nelim bl;
##[ nwhd in ⊢ (?→?→(?%????)); //
##| #h;#t;#IH;#H;#notin; nrewrite > (unfold_free_list m h t); napply valid_access_free_1;
    ##[ napply IH; //; napply (not_to_not ??? notin); #Ht; napply (in_list_cons … Ht)
    ##| napply nmk; #e; napply (absurd ?? notin); nrewrite > e; // ##]
##] nqed.

nlemma valid_access_free_list_inv:
  ∀chunk,psp,b,ofs,m,bl.
  valid_access (free_list m bl) chunk psp b ofs →
  ¬in_list ? b bl ∧ valid_access m chunk psp b ofs.
#chunk; #psp b ofs; #m; #bl; nelim bl;
##[ nwhd in ⊢ ((?%????)→?); #H; @; //
##| #h;#t;#IH; nrewrite > (unfold_free_list m h t); #H;
    nelim (valid_access_free_inv … H); #H';#ne;
    nelim (IH H'); #notin;#H''; @; //;
    napply (not_to_not ??? notin); #Ht;
    (* WTF? this is specialised to nat! napply (in_list_tail t b h); *) napply daemon
##] nqed.

(* ** Properties related to pointer validity *)

nlemma valid_pointer_valid_access:
  ∀m,psp,b,ofs.
  valid_pointer m psp b ofs = true ↔ valid_access m Mint8unsigned psp b ofs.
#m;#psp b ofs;nwhd in ⊢ (?(??%?)?); @;
##[ #H;
    nlapply (andb_true_l … H); #H';
    nlapply (andb_true_l … H'); #H'';
    nlapply (andb_true_l … H''); #H1;
    nlapply (andb_true_r … H''); #H2;
    nlapply (andb_true_r … H'); #H3;
    nlapply (andb_true_r … H); #H4;
    @;
    ##[ nrewrite > (unfold_valid_block m b); napply (Zltb_true_to_Zlt … H1)
    ##| napply (Zleb_true_to_Zle … H2)
    ##| nwhd in ⊢ (?(??%)?); (* arith, Zleb_true_to_Zle *) napply daemon
    ##| ncases ofs; /2/;
    ##| nwhd in H4:(??%?); nelim (pointer_compat_dec (block_space m b) psp) in H4;
        ##[ //; ##| #Hn e; nwhd in e:(??%%); ndestruct ##]
    ##]
##| *; #Hval;#Hlo;#Hhi;#Hal;#Hct;
    nrewrite > (Zlt_to_Zltb_true … Hval);
    nrewrite > (Zle_to_Zleb_true … Hlo);
    nwhd in Hhi:(?(??%)?); nrewrite > (Zlt_to_Zltb_true … ?);
    ##[ nwhd in ⊢ (??%?); nelim (pointer_compat_dec (block_space m b) psp);
      ##[ //;
      ##| #Hct'; napply False_ind; napply (absurd … Hct Hct');
      ##] 
    ##| (* arith *) napply daemon
    ##]
##]
 nqed. 

ntheorem valid_pointer_alloc:
  ∀m1,m2: mem. ∀lo,hi: Z. ∀bcl,psp. ∀b,b': block. ∀ofs: Z.
  alloc m1 lo hi bcl = 〈m2, b'〉 →
  valid_pointer m1 psp b ofs = true →
  valid_pointer m2 psp b ofs = true.
#m1;#m2;#lo;#hi;#bcl psp;#b;#b';#ofs;#ALLOC;#VALID;
nlapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval;
napply (proj2 ?? (valid_pointer_valid_access ????));
napply (valid_access_alloc_other … ALLOC … Hval);
nqed.

ntheorem valid_pointer_store:
  ∀chunk: memory_chunk. ∀m1,m2: mem.
  ∀psp,psp': memory_space. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val.
  store chunk m1 psp' b' ofs' v = Some ? m2 →
  valid_pointer m1 psp b ofs = true → valid_pointer m2 psp b ofs = true.
#chunk;#m1;#m2;#psp psp';#b;#b';#ofs;#ofs';#v;#STORE;#VALID;
nlapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval;
napply (proj2 ?? (valid_pointer_valid_access ????));
napply (store_valid_access_1 … STORE … Hval);
nqed.

(* * * Generic injections between memory states. *)
(*
(* Section GENERIC_INJECT. *)

ndefinition meminj : Type ≝ block → option (block × Z).
(*
Variable val_inj: meminj -> val -> val -> Prop.

Hypothesis val_inj_undef:
  ∀mi. val_inj mi Vundef Vundef.
*)

ndefinition mem_inj ≝ λval_inj.λmi: meminj. λm1,m2: mem.
  ∀chunk, b1, ofs, v1, b2, delta.
  mi b1 = Some ? 〈b2, delta〉 →
  load chunk m1 b1 ofs = Some ? v1 →
  ∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2 ∧ val_inj mi v1 v2.

(* FIXME: another nunfold hack*)
nlemma unfold_mem_inj : ∀val_inj.∀mi: meminj. ∀m1,m2: mem.
  (mem_inj val_inj mi m1 m2) =
  (∀chunk, b1, ofs, v1, b2, delta.
  mi b1 = Some ? 〈b2, delta〉 →
  load chunk m1 b1 ofs = Some ? v1 →
  ∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2 ∧ val_inj mi v1 v2).
//; nqed.

nlemma valid_access_inj: ∀val_inj.
  ∀mi,m1,m2,chunk,b1,ofs,b2,delta.
  mi b1 = Some ? 〈b2, delta〉 →
  mem_inj val_inj mi m1 m2 →
  valid_access m1 chunk b1 ofs →
  valid_access m2 chunk b2 (ofs + delta).
#val_inj;
#mi;#m1;#m2;#chunk;#b1;#ofs;#b2;#delta;#H;#Hinj;#Hval;
ncut (∃v1. load chunk m1 b1 ofs = Some ? v1);
##[ /2/;
##| *;#v1;#LOAD1;
    nelim (Hinj … H LOAD1);#v2;*;#LOAD2;#VCP;
    /2/
##] nqed.

(*Hint Resolve valid_access_inj: mem.*)
*)
(* FIXME: can't use ndestruct below *)
nlemma grumpydestruct : ∀A,v. None A = Some A v → False.
#A;#v;#H;ndestruct;
nqed.
(*
nlemma store_unmapped_inj: ∀val_inj.
  ∀mi,m1,m2,psp,b,ofs,v,chunk,m1'.
  mem_inj val_inj mi m1 m2 →
  mi b = None ? →
  store chunk m1 psp b ofs v = Some ? m1' →
  mem_inj val_inj mi m1' m2.
#val_inj;
#mi;#m1;#m2;#psp b ofs;#v;#chunk;#m1';#Hinj;#Hmi;#Hstore;
nwhd; #chunk0;#b1;#ofs0;#v1;#b2;#delta; #Hmi0; #Hload;
ncut (load chunk0 m1 b1 ofs0 = Some ? v1);
##[ nrewrite < Hload; napply sym_eq; napply (load_store_other … Hstore);
    @1;@1; napply nmk; #eq; nrewrite > eq in Hmi0; nrewrite > Hmi; #H; ndestruct;
##| #Hload'; napply (Hinj … Hmi0 Hload');
##] nqed.

nlemma store_outside_inj: ∀val_inj.
  ∀mi,m1,m2,chunk,psp,b,ofs,v,m2'.
  mem_inj val_inj mi m1 m2 →
  (∀b',delta.
    mi b' = Some ? 〈b, delta〉 →
    high_bound m1 b' + delta ≤ ofs
    ∨ ofs + size_chunk chunk ≤ low_bound m1 b' + delta) →
  store chunk m2 psp b ofs v = Some ? m2' →
  mem_inj val_inj mi m1 m2'.
#val_inj;
#mi;#m1;#m2;#chunk;#psp b ofs;#v;#m2';#Hinj;#Hbounds;#Hstore;
nwhd; #chunk0;#b1;#ofs0;#v1;#b2;#delta; #Hmi0; #Hload;
nlapply (Hinj … Hmi0 Hload);*;#v2;*;#LOAD2;#VINJ;
@ v2;@;//;
nrewrite < LOAD2; napply (load_store_other … Hstore);
nelim (decidable_eq_Z b2 b);
##[ #Heq; nrewrite > Heq in Hmi0 LOAD2; #Hmi0;#LOAD2;
    nlapply (Hbounds … Hmi0); #Hb;
    ncut (valid_access m1 chunk0 b1 ofs0); /2/;
    #Hv; nelim Hv; #Hv1; #Hlo1; #Hhi1; #Hal1;
    nelim Hb; #Hb; ##[ @1;@2;(* arith *) napply daemon ##| @2;(* arith *) napply daemon ##]
##| #ineq; @1; @1; napply ineq;
##] nqed.

(* XXX: use Or rather than ∨ to bring resource usage under control. *)
ndefinition meminj_no_overlap ≝ λmi: meminj. λm: mem.
  ∀b1,b1',delta1,b2,b2',delta2.
  b1 ≠ b2 →
  mi b1 = Some ? 〈b1', delta1〉 →
  mi b2 = Some ? 〈b2', delta2〉 →
  Or (Or (Or (b1' ≠ b2')
             (low_bound m b1 ≥ high_bound m b1))
         (low_bound m b2 ≥ high_bound m b2))
  (Or (high_bound m b1 + delta1 ≤ low_bound m b2 + delta2)
      (high_bound m b2 + delta2 ≤ low_bound m b1 + delta1)).
*)
(* FIXME *)
nlemma grumpydestruct1 : ∀A,x1,x2. Some A x1 = Some A x2 → x1 = x2.
#A;#x1;#x2;#H;ndestruct;//;
nqed.
nlemma grumpydestruct2 : ∀A,B,x1,y1,x2,y2. Some (A×B) 〈x1,y1〉 = Some (A×B) 〈x2,y2〉 → x1 = x2 ∧ y1 = y2.
#A;#B;#x1;#y1;#x2;#y2;#H;ndestruct;/2/;
nqed. 
(*
nlemma store_mapped_inj: ∀val_inj.∀val_inj_undef:∀mi. val_inj mi Vundef Vundef.
  ∀mi,m1,m2,b1,ofs,b2,delta,v1,v2,chunk,m1'.
  mem_inj val_inj mi m1 m2 →
  meminj_no_overlap mi m1 →
  mi b1 = Some ? 〈b2, delta〉 →
  store chunk m1 b1 ofs v1 = Some ? m1' →
  (∀chunk'. size_chunk chunk' = size_chunk chunk →
    val_inj mi (load_result chunk' v1) (load_result chunk' v2)) →
  ∃m2'.
  store chunk m2 b2 (ofs + delta) v2 = Some ? m2' ∧ mem_inj val_inj mi m1' m2'.
#val_inj;#val_inj_undef;
#mi;#m1;#m2;#b1;#ofs;#b2;#delta;#v1;#v2;#chunk;#m1';
#Hinj;#Hnoover;#Hb1;#STORE;#Hvalinj;
ncut (∃m2'.store chunk m2 b2 (ofs + delta) v2 = Some ? m2');
##[ napply valid_access_store; napply (valid_access_inj ? mi ??????? Hb1 Hinj ?); (* XXX why do I have to give mi here? *) /2/
##| *;#m2';#STORE2;
    @ m2'; @; //;
    nwhd; #chunk';#b1';#ofs';#v;#b2';#delta';#CP;#LOAD1;
    ncut (valid_access m1 chunk' b1' ofs');
    ##[ napply (store_valid_access_2 … STORE); napply (load_valid_access … LOAD1);
    ##| #Hval;
        nlapply (load_store_characterization … STORE … Hval);
        nelim (load_store_classification chunk b1 ofs chunk' b1' ofs');
        ##[ #e;#e0;#e1;#H; (* similar *)
            nrewrite > e in Hb1; #Hb1;
            nrewrite > CP in Hb1; #Hb1; (* XXX ndestruct expands proof state too much;*)
            nelim (grumpydestruct2 ?????? Hb1);
            #e2;#e3; nrewrite < e0; nrewrite > e2; nrewrite > e3;
            @ (load_result chunk' v2);@;
            ##[ napply (load_store_similar … STORE2); //
            ##| nrewrite > LOAD1 in H; #H; nwhd in H:(??%%); ndestruct;
                napply Hvalinj; //;
            ##]
         ##| #Hdis; #H; (* disjoint *)
             nrewrite > LOAD1 in H; #H;
             nlapply (Hinj … CP ?); ##[ napply sym_eq; napply H; ##| ##*: ##]
             *;#v2';*;#LOAD2;#VCP;
             @ v2'; @; //;
             nrewrite < LOAD2; napply (load_store_other … STORE2);
             nelim (decidable_eq_Z b1 b1'); #eb1;
             ##[ nrewrite < eb1 in CP; #CP; nrewrite > CP in Hb1; #eb2d;
                 nelim (grumpydestruct2 ?????? eb2d); #eb2; #ed;
                 nelim Hdis; ##[ #Hdis; nelim Hdis;
                               ##[ #eb1'; napply False_ind; napply (absurd ? eb1 eb1');
                               ##| #Hdis;@1;@2;(* arith *) napply daemon
                               ##] ##| #Hdis;@2;(* arith *) napply daemon ##]
             ##| ncut (valid_access m1 chunk b1 ofs); /2/; #Hval';
                 nlapply (Hnoover … eb1 Hb1 CP);
                 #Ha; nelim Ha; #Ha;
                 ##[ nelim Ha; #Ha;
                 ##[ nelim Ha; #Ha;
                 ##[ @1;@1;/2/
                 ##| nelim Hval'; nlapply (size_chunk_pos chunk); (* arith *) napply daemon ##]
                 ##| nelim Hval; nlapply (size_chunk_pos chunk'); (* arith *) napply daemon ##]
                 ##| nelim Hval'; nelim Hval;  (* arith *) napply daemon ##]
             ##]
         ##| #eb1;#Hofs1;#Hofs2;#Hofs3;#H; (* overlapping *)
             nrewrite < eb1 in CP; #CP; nrewrite > CP in Hb1; #eb2d;
             nelim (grumpydestruct2 ?????? eb2d); #eb2; #ed;
             ncut (∃v2'. load chunk' m2' b2 (ofs' + delta) = Some ? v2');
             ##[ napply valid_access_load; napply (store_valid_access_1 … STORE2); napply (valid_access_inj … Hinj Hval); nrewrite > eb1; //
             ##| *;#v2';#LOAD2';
                 ncut (v2' = Vundef); ##[ napply (load_store_overlap … STORE2 … LOAD2'); (* arith *) napply daemon ##| ##]
                 #ev2'; @ v2'; @;//;
                 nrewrite > LOAD1 in H;#H; nwhd in H:(??%%); nrewrite > (grumpydestruct1 … H);
                 nrewrite > ev2';
                 napply val_inj_undef; ##]
         ##| #eb1;#Hofs;nrewrite < Hofs in Hval LOAD1 ⊢ %;#Hval;#LOAD1;#Hsize;#H; (* overlapping *)
             
             nrewrite < eb1 in CP; #CP; nrewrite > CP in Hb1; #eb2d;
             nelim (grumpydestruct2 ?????? eb2d); #eb2; #ed;
             ncut (∃v2'. load chunk' m2' b2 (ofs + delta) = Some ? v2');
             ##[ napply valid_access_load; napply (store_valid_access_1 … STORE2); napply (valid_access_inj … Hinj Hval); nrewrite > eb1; //
             ##| *;#v2';#LOAD2';
                 ncut (v2' = Vundef); ##[ napply (load_store_mismatch … STORE2 … LOAD2' ?); napply sym_neq;// ##| ##]
                 #ev2'; @ v2'; @;//;
                 nrewrite > LOAD1 in H;#H; nwhd in H:(??%%); nrewrite > (grumpydestruct1 … H);
                 nrewrite > ev2';
                 napply val_inj_undef; ##]
         ##]
     ##]
##] nqed.

ndefinition inj_offset_aligned ≝ λdelta: Z. λsize: Z.
  ∀chunk. size_chunk chunk ≤ size → (align_chunk chunk ∣ delta).

nlemma alloc_parallel_inj: ∀val_inj.∀val_inj_undef:∀mi. val_inj mi Vundef Vundef.
  ∀mi,m1,m2,lo1,hi1,m1',b1,lo2,hi2,m2',b2,delta.
  mem_inj val_inj mi m1 m2 →
  alloc m1 lo1 hi1 = 〈m1', b1〉 →
  alloc m2 lo2 hi2 = 〈m2', b2〉 →
  mi b1 = Some ? 〈b2, delta〉 →
  lo2 ≤ lo1 + delta → hi1 + delta ≤ hi2 →
  inj_offset_aligned delta (hi1 - lo1) →
  mem_inj val_inj mi m1' m2'.
#val_inj;#val_inj_undef;
#mi;#m1;#m2;#lo1;#hi1;#m1';#b1;#lo2;#hi2;#m2';#b2;#delta;
#Hinj;#ALLOC1;#ALLOC2;#Hbinj;#Hlo;#Hhi;#Hal;
nwhd; #chunk;#b1';#ofs;#v;#b2';#delta';#Hbinj';#LOAD;
nlapply (valid_access_alloc_inv … m1 … ALLOC1 chunk b1' ofs ?); /2/;
*;
##[ #A;
    ncut (load chunk m1 b1' ofs = Some ? v);
    ##[ nrewrite < LOAD; napply sym_eq; napply (load_alloc_unchanged … ALLOC1); /2/; ##]
    #LOAD0; nlapply (Hinj … Hbinj' LOAD0); *;#v2;*;#LOAD2;#VINJ;
    @ v2; @;
    ##[ nrewrite < LOAD2; napply (load_alloc_unchanged … ALLOC2);
        napply valid_access_valid_block; ##[ ##3: napply load_valid_access; ##]
        //
    ##| //
    ##]
##| *;*;#A;#B;#C;
    nrewrite > A in Hbinj' LOAD; #Hbinj';#LOAD;
    nrewrite > Hbinj in Hbinj'; #Hbinj'; nelim (grumpydestruct2 ?????? Hbinj');
    #eb2;#edelta; nrewrite < eb2; nrewrite < edelta;
    ncut (v = Vundef); ##[ napply (load_alloc_same … ALLOC1 … LOAD); ##]
    #ev; nrewrite > ev;
    ncut (∃v2. load chunk m2' b2 (ofs + delta) = Some ? v2);
    ##[ napply valid_access_load;
        napply (valid_access_alloc_same … ALLOC2);
        ##[ ##1,2: (*arith*) napply daemon;
        ##| (* arith using Hal *) napply daemon
        ##] ##]
    *;#v2;#LOAD2;
    ncut (v2 = Vundef); ##[ napply (load_alloc_same … ALLOC2 … LOAD2) ##]
    #ev2; nrewrite > ev2;
    @ Vundef; @; //;
##] nqed.

nlemma alloc_right_inj: ∀val_inj.
  ∀mi,m1,m2,lo,hi,b2,m2'.
  mem_inj val_inj mi m1 m2 →
  alloc m2 lo hi = 〈m2', b2〉 →
  mem_inj val_inj mi m1 m2'.
#val_inj;
#mi;#m1;#m2;#lo;#hi;#b2;#m2';
#Hinj;#ALLOC;
nwhd; #chunk; #b1; #ofs; #v1; #b2'; #delta; #Hbinj; #LOAD;
nlapply (Hinj … Hbinj LOAD); *; #v2;*;#LOAD2;#VINJ;
@ v2; @; //;
ncut (valid_block m2 b2');
  ##[ napply (valid_access_valid_block ? chunk ? (ofs + delta)); /2/ ##]
#Hval;
nrewrite < LOAD2; napply (load_alloc_unchanged … ALLOC … Hval);
nqed.

(*
Hypothesis val_inj_undef_any:
  ∀mi,v. val_inj mi Vundef v.
*)

nlemma alloc_left_unmapped_inj: ∀val_inj.
  ∀mi,m1,m2,lo,hi,b1,m1'.
  mem_inj val_inj mi m1 m2 →
  alloc m1 lo hi = 〈m1', b1〉 →
  mi b1 = None ? →
  mem_inj val_inj mi m1' m2.
#val_inj;
#mi;#m1;#m2;#lo;#hi;#b1;#m1';
#Hinj;#ALLOC;#Hbinj;
nwhd;  #chunk; #b1'; #ofs; #v1; #b2'; #delta; #Hbinj'; #LOAD;
nlapply (valid_access_alloc_inv … m1 … ALLOC chunk b1' ofs ?); /2/;
*;
##[ #A;
  napply (Hinj … Hbinj' );
  nrewrite < LOAD; napply sym_eq; napply (load_alloc_unchanged … ALLOC); /2/;
##| *;*;#A;#B;#C;
  nrewrite > A in Hbinj' LOAD; #Hbinj'; #LOAD;
  nrewrite > Hbinj in Hbinj'; #bad; ndestruct;
##] nqed.

nlemma alloc_left_mapped_inj: ∀val_inj.∀val_inj_undef_any:∀mi,v. val_inj mi Vundef v.
  ∀mi,m1,m2,lo,hi,b1,m1',b2,delta.
  mem_inj val_inj mi m1 m2 →
  alloc m1 lo hi = 〈m1', b1〉 →
  mi b1 = Some ? 〈b2, delta〉 →
  valid_block m2 b2 →
  low_bound m2 b2 ≤ lo + delta → hi + delta ≤ high_bound m2 b2 →
  inj_offset_aligned delta (hi - lo) →
  mem_inj val_inj mi m1' m2.
#val_inj;#val_inj_undef_any;
#mi;#m1;#m2;#lo;#hi;#b1;#m1';#b2;#delta;
#Hinj;#ALLOC;#Hbinj;#Hval;#Hlo;#Hhi;#Hal;
nwhd; #chunk; #b1'; #ofs; #v1; #b2'; #delta'; #Hbinj'; #LOAD;
nlapply (valid_access_alloc_inv … m1 … ALLOC chunk b1' ofs ?); /2/;
*;
##[ #A;
    napply (Hinj … Hbinj');
    nrewrite < LOAD; napply sym_eq; napply (load_alloc_unchanged … ALLOC); /2/;
##| *;*;#A;#B;*;#C;#D;
    nrewrite > A in Hbinj' LOAD; #Hbinj'; #LOAD; nrewrite > Hbinj in Hbinj';
    #Hbinj'; (* XXX ndestruct normalizes too much here *) nelim (grumpydestruct2 ?????? Hbinj'); #eb2; #edelta;
    nrewrite < eb2; nrewrite < edelta;
    ncut (v1 = Vundef); ##[ napply (load_alloc_same … ALLOC … LOAD) ##]
    #ev1; nrewrite > ev1;
    ncut (∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2);
    ##[ napply valid_access_load; @; //;
      ##[ (* arith *) napply daemon
      ##| (* arith *) napply daemon
      ##| (* arith *) napply daemon
      ##]
    ##]
    *;#v2;#LOAD2; @ v2; @; //;
##] nqed.

nlemma free_parallel_inj: ∀val_inj.
  ∀mi,m1,m2,b1,b2,delta.
  mem_inj val_inj mi m1 m2 →
  mi b1 = Some ? 〈b2, delta〉 →
  (∀b,delta'. mi b = Some ? 〈b2, delta'〉 → b = b1) →
  mem_inj val_inj mi (free m1 b1) (free m2 b2).
#val_inj;
#mi;#m1;#m2;#b1;#b2;#delta; #Hinj;#Hb1inj;#Hbinj;
nwhd; #chunk; #b1'; #ofs; #v1; #b2'; #delta'; #Hbinj'; #LOAD;
nlapply (valid_access_free_inv … (load_valid_access … LOAD)); *; #A;#B;
ncut (load chunk m1 b1' ofs = Some ? v1);
##[ nrewrite < LOAD; napply sym_eq; napply load_free; napply B ##] #LOAD';
nelim (Hinj … Hbinj' LOAD'); #v2;*;#LOAD2;#INJ;
@ v2;@;
##[ nrewrite < LOAD2; napply load_free;
    napply nmk; #e; napply (absurd ?? B); 
    nrewrite > e in Hbinj'; #Hbinj'; napply (Hbinj ?? Hbinj');
##| //
##] nqed.

nlemma free_left_inj: ∀val_inj.
  ∀mi,m1,m2,b1.
  mem_inj val_inj mi m1 m2 →
  mem_inj val_inj mi (free m1 b1) m2.
#val_inj;#mi;#m1;#m2;#b1;#Hinj;
nwhd; #chunk; #b1'; #ofs; #v1; #b2'; #delta'; #Hbinj'; #LOAD;
nlapply (valid_access_free_inv … (load_valid_access … LOAD)); *; #A;#B;
napply (Hinj … Hbinj');
nrewrite < LOAD; napply sym_eq; napply load_free; napply B;
nqed. 

nlemma free_list_left_inj: ∀val_inj.
  ∀mi,bl,m1,m2.
  mem_inj val_inj mi m1 m2 →
  mem_inj val_inj mi (free_list m1 bl) m2.
#val_inj;#mi;#bl;nelim bl;
##[ nwhd in ⊢ (?→?→?→???%?); //
##| #h;#t;#IH; #m1;#m2;#H; nrewrite > (unfold_free_list m1 h t);
    napply free_left_inj; napply IH; //
##] nqed.

nlemma free_right_inj: ∀val_inj.
  ∀mi,m1,m2,b2.
  mem_inj val_inj mi m1 m2 →
  (∀b1,delta,chunk,ofs. 
   mi b1 = Some ? 〈b2, delta〉 → ¬(valid_access m1 chunk b1 ofs)) →
  mem_inj val_inj mi m1 (free m2 b2).
#val_inj;#mi;#m1;#m2;#b2; #Hinj; #Hinval;
nwhd; #chunk; #b1'; #ofs; #v1; #b2'; #delta'; #Hbinj'; #LOAD;
ncut (b2' ≠ b2);
##[ napply nmk; #e; nrewrite > e in Hbinj'; #Hbinj';
    napply (absurd ?? (Hinval … Hbinj')); napply (load_valid_access … LOAD); ##]
#ne; nlapply (Hinj … Hbinj' LOAD); *;#v2;*;#LOAD2;#INJ;
@ v2; @; //;
nrewrite < LOAD2; napply load_free; napply ne;
nqed.

nlemma valid_pointer_inj: ∀val_inj.
  ∀mi,m1,m2,b1,ofs,b2,delta.
  mi b1 = Some ? 〈b2, delta〉 →
  mem_inj val_inj mi m1 m2 →
  valid_pointer m1 b1 ofs = true →
  valid_pointer m2 b2 (ofs + delta) = true.
#val_inj;#mi;#m1;#m2;#b1;#ofs;#b2;#delta;#Hbinj;#Hinj;#VALID;
nlapply ((proj1 ?? (valid_pointer_valid_access ???)) VALID); #Hval;
napply (proj2 ?? (valid_pointer_valid_access ???));
napply (valid_access_inj … Hval); //;
nqed.

(*
End GENERIC_INJECT.
*)
(* ** Store extensions *)

(* A store [m2] extends a store [m1] if [m2] can be obtained from [m1]
  by increasing the sizes of the memory blocks of [m1] (decreasing
  the low bounds, increasing the high bounds), while still keeping the
  same contents for block offsets that are valid in [m1]. *)

ndefinition inject_id : meminj ≝ λb. Some ? 〈b, OZ〉.

ndefinition val_inj_id ≝ λmi: meminj. λv1,v2: val. v1 = v2.

ndefinition extends ≝ λm1,m2: mem.
  nextblock m1 = nextblock m2 ∧ mem_inj val_inj_id inject_id m1 m2.

ntheorem extends_refl:
  ∀m: mem. extends m m.
#m;@;//;
nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta;nnormalize in ⊢ (%→?);#H; 
(* XXX: ndestruct makes the goal unreadable *) nelim (grumpydestruct2 ?????? H); #eb1;#edelta;#LOAD;
@ v1; @;
##[ nrewrite < edelta; nrewrite > (Zplus_z_OZ ofs); //;
##| //
##] nqed. 

ntheorem alloc_extends:
  ∀m1,m2,m1',m2': mem. ∀lo1,hi1,lo2,hi2: Z. ∀b1,b2: block.
  extends m1 m2 →
  lo2 ≤ lo1 → hi1 ≤ hi2 →
  alloc m1 lo1 hi1 = 〈m1', b1〉 →
  alloc m2 lo2 hi2 = 〈m2', b2〉 →
  b1 = b2 ∧ extends m1' m2'.
#m1;#m2;#m1';#m2';#lo1;#hi1;#lo2;#hi2;#b1;#b2;
*;#Hnext;#Hinj;#Hlo;#Hhi;#ALLOC1;#ALLOC2;
ncut (b1 = b2);
##[ napply (transitive_eq … (nextblock m1)); ##[ napply (alloc_result … ALLOC1);
    ##| napply sym_eq; nrewrite > Hnext; napply (alloc_result … ALLOC2) ##] ##]
#eb; nrewrite < eb in ALLOC2 ⊢ %; #ALLOC2; @; //; @;
##[ nrewrite > (nextblock_alloc … ALLOC1);
    nrewrite > (nextblock_alloc … ALLOC2);
    //;
##| napply (alloc_parallel_inj ??????????????? ALLOC1 ALLOC2 ????);
  ##[ ##1,4: nnormalize; //;
  ##| ##3,5,6: //
  ##| ##7: nwhd; #chunk;#Hsize; (* divides 0 *) napply daemon
  ##]
##] nqed.

ntheorem free_extends:
  ∀m1,m2: mem. ∀b: block.
  extends m1 m2 →
  extends (free m1 b) (free m2 b).
#m1;#m2;#b;*;#Hnext;#Hinj; @;
##[ nnormalize; //;
##| napply (free_parallel_inj … Hinj);
  ##[ ##2: //;
  ##| ##3: nnormalize; #b';#delta;#ee; ndestruct; //
  ##]
##] nqed. 

ntheorem load_extends:
  ∀chunk: memory_chunk. ∀m1,m2: mem. ∀b: block. ∀ofs: Z. ∀v: val.
  extends m1 m2 →
  load chunk m1 psp b ofs = Some ? v →
  load chunk m2 psp b ofs = Some ? v.
#chunk;#m1;#m2;#psp b ofs;#v;
*;#Hnext;#Hinj;#LOAD;
nlapply (Hinj … LOAD); ##[ nnormalize; // ##| ##2,3: ##]
*;#v2;*; nrewrite > (Zplus_z_OZ ofs); #LOAD2;#EQ;nwhd in EQ;
//;
nqed.

ntheorem store_within_extends:
  ∀chunk: memory_chunk. ∀m1,m2,m1': mem. ∀b: block. ∀ofs: Z. ∀v: val.
  extends m1 m2 →
  store chunk m1 psp b ofs v = Some ? m1' →
  ∃m2'. store chunk m2 psp b ofs v = Some ? m2' ∧ extends m1' m2'.
#chunk;#m1;#m2;#m1';#b;#ofs;#v;*;#Hnext;#Hinj;#STORE1;
nlapply (store_mapped_inj … Hinj ?? STORE1 ?);
##[ ##1,2,7: nnormalize; //
##| (* TODO: unfolding, etc ought to tidy this up *)
    nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2;#neb;#Hinj1;#Hinj2;
    nnormalize in Hinj1 Hinj2; @1; @1; @1; ndestruct; //
##| ##4,5,6: ##skip
##]
*;#m2';*;#STORE;#MINJ;
@ m2'; @; nrewrite > (Zplus_z_OZ ofs) in STORE; #STORE; //;
@;
##[ nrewrite > (nextblock_store … STORE1);
    nrewrite > (nextblock_store … STORE);
    //
##| //
##] nqed.

ntheorem store_outside_extends:
  ∀chunk: memory_chunk. ∀m1,m2,m2': mem. ∀b: block. ∀ofs: Z. ∀v: val.
  extends m1 m2 →
  ofs + size_chunk chunk ≤ low_bound m1 b ∨ high_bound m1 b ≤ ofs →
  store chunk m2 psp b ofs v = Some ? m2' →
  extends m1 m2'.
#chunk;#m1;#m2;#m2';#b;#ofs;#v;*;#Hnext;#Hinj;#Houtside;#STORE; @;
##[ nrewrite > (nextblock_store … STORE); //
##| napply (store_outside_inj … STORE); //;
    #b';#delta;#einj;nnormalize in einj; ndestruct;
    nelim Houtside; 
    ##[ #lo;@ 2; nrewrite > (Zplus_z_OZ ?); /2/
    ##| #hi;@ 1;  nrewrite > (Zplus_z_OZ ?); /2/
    ##]
##] nqed.

ntheorem valid_pointer_extends:
  ∀m1,m2,b,ofs.
  extends m1 m2 → valid_pointer m1 psp b ofs = true →
  valid_pointer m2 psp b ofs = true.
#m1;#m2;#b;#ofs;*;#Hnext;#Hinj;#VALID;
nrewrite < (Zplus_z_OZ ofs);
napply (valid_pointer_inj … Hinj VALID); //;
nqed.


(* * The ``less defined than'' relation over memory states *)

(* A memory state [m1] is less defined than [m2] if, for all addresses,
  the value [v1] read in [m1] at this address is less defined than
  the value [v2] read in [m2], that is, either [v1 = v2] or [v1 = Vundef]. *)

ndefinition val_inj_lessdef ≝ λmi: meminj. λv1,v2: val.
  Val_lessdef v1 v2.

ndefinition lessdef ≝ λm1,m2: mem.
  nextblock m1 = nextblock m2 ∧
  mem_inj val_inj_lessdef inject_id m1 m2.

nlemma lessdef_refl:
  ∀m. lessdef m m.
#m; @; //;
nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta;#H;#LOAD;
nwhd in H:(??%?); nelim (grumpydestruct2 ?????? H); #eb1; #edelta;
@ v1; @; //;
nqed.

nlemma load_lessdef:
  ∀m1,m2,chunk,b,ofs,v1.
  lessdef m1 m2 → load chunk m1 psp b ofs = Some ? v1 →
  ∃v2. load chunk m2 psp b ofs = Some ? v2 ∧ Val_lessdef v1 v2.
#m1;#m2;#chunk;#b;#ofs;#v1;*;#Hnext;#Hinj;#LOAD0;
nlapply (Hinj … LOAD0); ##[ nwhd in ⊢ (??%?); // ##| ##2,3:##skip ##]
*;#v2;*;#LOAD;#INJ; @ v2; @;//;
nqed.

nlemma loadv_lessdef:
  ∀m1,m2,chunk,addr1,addr2,v1.
  lessdef m1 m2 → Val_lessdef addr1 addr2 →
  loadv chunk m1 addr1 = Some ? v1 →
  ∃v2. loadv chunk m2 addr2 = Some ? v2 ∧ Val_lessdef v1 v2.
#m1;#m2;#chunk;#addr1;#addr2;#v1;#H;#H0;#LOAD;
ninversion H0;
##[ #v; #e1;#e2; nrewrite > e1 in LOAD; ncases v;
    ##[ nwhd in ⊢ ((??%?)→?); #H'; ndestruct;
    ##| ##2,3: #v'; nwhd in ⊢ ((??%?)→?); #H'; ndestruct;
    ##| #b';#off; napply load_lessdef; //
    ##]
##| #v;#e;nrewrite > e in LOAD; #LOAD; nwhd in LOAD:(??%?); ndestruct;
##] nqed.

nlemma store_lessdef:
  ∀m1,m2,chunk,b,ofs,v1,v2,m1'.
  lessdef m1 m2 → Val_lessdef v1 v2 →
  store chunk m1 psp b ofs v1 = Some ? m1' →
  ∃m2'. store chunk m2 psp b ofs v2 = Some ? m2' ∧ lessdef m1' m2'.
#m1;#m2;#chunk;#b;#ofs;#v1;#v2;#m1';
*;#Hnext;#Hinj;#Hvless;#STORE0;
nlapply (store_mapped_inj … Hinj … STORE0 ?);
##[ #chunk';#Hsize;nwhd;napply load_result_lessdef;napply Hvless
##| nwhd in ⊢ (??%?); //
##| nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2;#neq;
    nwhd in ⊢ ((??%?)→(??%?)→?); #e1; #e2; ndestruct;
    @;@;@;//
##| ##7: #mi; nwhd; //;
##| ##8: *;#m2';*;#STORE;#MINJ;
         @ m2';@; /2/;
         @;
         nrewrite > (nextblock_store … STORE0);
         nrewrite > (nextblock_store … STORE);
         //;
##] nqed.

nlemma storev_lessdef:
  ∀m1,m2,chunk,addr1,v1,addr2,v2,m1'.
  lessdef m1 m2 → Val_lessdef addr1 addr2 → Val_lessdef v1 v2 →
  storev chunk m1 addr1 v1 = Some ? m1' →
  ∃m2'. storev chunk m2 addr2 v2 = Some ? m2' ∧ lessdef m1' m2'.
#m1;#m2;#chunk;#addr1;#v1;#addr2;#v2;#m1';
#Hmless;#Haless;#Hvless;#STORE;
ninversion Haless;
##[ #v; #e1;#e2; nrewrite > e1 in STORE; ncases v;
    ##[ nwhd in ⊢ ((??%?)→?); #H'; napply False_ind; ndestruct;
    ##| ##2,3: #v'; nwhd in ⊢ ((??%?)→?); #H'; ndestruct;
    ##| #b';#off; napply store_lessdef; //
    ##]
##| #v;#e;nrewrite > e in STORE; #STORE; nwhd in STORE:(??%?); ndestruct
##] nqed.

nlemma alloc_lessdef:
  ∀m1,m2,lo,hi,b1,m1',b2,m2'.
  lessdef m1 m2 → alloc m1 lo hi = 〈m1', b1〉 → alloc m2 lo hi = 〈m2', b2〉 →
  b1 = b2 ∧ lessdef m1' m2'.
#m1;#m2;#lo;#hi;#b1;#m1';#b2;#m2';
*;#Hnext;#Hinj;#ALLOC1;#ALLOC2;
ncut (b1 = b2);
##[ nrewrite > (alloc_result … ALLOC1); nrewrite > (alloc_result … ALLOC2); //
##]
#e; nrewrite < e in ALLOC2 ⊢ %; #ALLOC2; @; //;
@;
##[ nrewrite > (nextblock_alloc … ALLOC1);
    nrewrite > (nextblock_alloc … ALLOC2);
    //
##| napply (alloc_parallel_inj … Hinj ALLOC1 ALLOC2);
##[ //
##| ##3: nwhd in ⊢ (??%?); //
##| ##4,5: //;
##| ##6: nwhd; #chunk;#_; ncases chunk;//;
##] nqed.

nlemma free_lessdef:
  ∀m1,m2,b. lessdef m1 m2 → lessdef (free m1 b) (free m2 b).
#m1;#m2;#b;*;#Hnext;#Hinj; @;
##[ nwhd in ⊢ (??%%); //
##| napply (free_parallel_inj … Hinj); //;
    #b';#delta;#H; nwhd in H:(??%?); nelim (grumpydestruct2 ?????? H); //
##] nqed.

nlemma free_left_lessdef:
  ∀m1,m2,b.
  lessdef m1 m2 → lessdef (free m1 b) m2.
#m1;#m2;#b;*;#Hnext;#Hinj;@;
nrewrite < Hnext; //;
napply free_left_inj; //;
nqed.

nlemma free_right_lessdef:
  ∀m1,m2,b.
  lessdef m1 m2 → low_bound m1 b ≥ high_bound m1 b →
  lessdef m1 (free m2 b).
#m1;#m2;#b;*;#Hnext;#Hinj;#Hbounds;
@; nrewrite > Hnext; //;
napply free_right_inj; //;
#b1;#delta;#chunk;#ofs;#H; nwhd in H:(??%?); ndestruct;
napply nmk; *; #H1;#H2;#H3;#H4;
(* arith H2 and H3 contradict Hbounds. *) napply daemon;
nqed.

nlemma valid_block_lessdef:
  ∀m1,m2,b. lessdef m1 m2 → valid_block m1 b → valid_block m2 b.
#m1;#m2;#b;*;#Hnext;#Hinj;
 nrewrite > (unfold_valid_block …); nrewrite > (unfold_valid_block m2 b);
 //; nqed.

nlemma valid_pointer_lessdef:
  ∀m1,m2,b,ofs.
  lessdef m1 m2 → valid_pointer m1 psp b ofs = true → valid_pointer m2 psp b ofs = true.
#m1;#m2;#b;#ofs;*;#Hnext;#Hinj;#VALID;
nrewrite < (Zplus_z_OZ ofs); napply (valid_pointer_inj … Hinj VALID); //;
nqed.


(* ** Memory injections *)

(* A memory injection [f] is a function from addresses to either [None]
  or [Some] of an address and an offset.  It defines a correspondence
  between the blocks of two memory states [m1] and [m2]:
- if [f b = None], the block [b] of [m1] has no equivalent in [m2];
- if [f b = Some〈b', ofs〉], the block [b] of [m2] corresponds to
  a sub-block at offset [ofs] of the block [b'] in [m2].
*)

(* A memory injection defines a relation between values that is the
  identity relation, except for pointer values which are shifted
  as prescribed by the memory injection. *)

ninductive val_inject (mi: meminj): val → val → Prop :=
  | val_inject_int:
      ∀i. val_inject mi (Vint i) (Vint i)
  | val_inject_float:
      ∀f. val_inject mi (Vfloat f) (Vfloat f)
  | val_inject_ptr:
      ∀b1,ofs1,b2,ofs2,x.
      mi b1 = Some ? 〈b2, x〉 →
      ofs2 = add ofs1 (repr x) →
      val_inject mi (Vptr b1 ofs1) (Vptr b2 ofs2)
  | val_inject_undef: ∀v.
      val_inject mi Vundef v.
(*
Hint Resolve val_inject_int val_inject_float val_inject_ptr 
             val_inject_undef.
*)
ninductive val_list_inject (mi: meminj): list val → list val→ Prop:= 
  | val_nil_inject :
      val_list_inject mi (nil ?) (nil ?)
  | val_cons_inject : ∀v,v',vl,vl'.
      val_inject mi v v' → val_list_inject mi vl vl'→
      val_list_inject mi (v :: vl) (v' :: vl').  
(*
Hint Resolve val_nil_inject val_cons_inject.
*)
(* A memory state [m1] injects into another memory state [m2] via the
  memory injection [f] if the following conditions hold:
- loads in [m1] must have matching loads in [m2] in the sense
  of the [mem_inj] predicate;
- unallocated blocks in [m1] must be mapped to [None] by [f];
- if [f b = Some〈b', delta〉], [b'] must be valid in [m2];
- distinct blocks in [m1] are mapped to non-overlapping sub-blocks in [m2];
- the sizes of [m2]'s blocks are representable with signed machine integers;
- the offsets [delta] are representable with signed machine integers.
*)

nrecord mem_inject (f: meminj) (m1,m2: mem) : Prop ≝
  {
    mi_inj:
      mem_inj val_inject f m1 m2;
    mi_freeblocks:
      ∀b. ¬(valid_block m1 b) → f b = None ?;
    mi_mappedblocks:
      ∀b,b',delta. f b = Some ? 〈b', delta〉 → valid_block m2 b';
    mi_no_overlap:
      meminj_no_overlap f m1;
    mi_range_1:
      ∀b,b',delta.
      f b = Some ? 〈b', delta〉 →
      min_signed ≤ delta ∧ delta ≤ max_signed;
    mi_range_2:
      ∀b,b',delta.
      f b = Some ? 〈b', delta〉 →
      delta = 0 ∨ (min_signed ≤ low_bound m2 b' ∧ high_bound m2 b' ≤ max_signed)
  }.


(* The following lemmas establish the absence of machine integer overflow
  during address computations. *)

nlemma address_inject:
  ∀f,m1,m2,chunk,b1,ofs1,b2,delta.
  mem_inject f m1 m2 →
  valid_access m1 chunk b1 (signed ofs1) →
  f b1 = Some ? 〈b2, delta〉 →
  signed (add ofs1 (repr delta)) = signed ofs1 + delta.
#f;#m1;#m2;#chunk;#b1;#ofs1;#b2;#delta;
*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
#Hvalid;#Hb1inj;
nelim (mi_range_2 ??? Hb1inj);
##[ (* delta = 0 *)
    #edelta; nrewrite > edelta;
    nrewrite > (?:repr O = zero); ##[ ##2: // ##]
    nrewrite > (add_zero ?);
    nrewrite > (Zplus_z_OZ …);
    //;
##| (* delta ≠ 0 *)
    #Hrange; nrewrite > (add_signed ??);
    nrewrite > (signed_repr delta ?);
    ##[ nrewrite > (signed_repr ??);
      ##[ //
      ##| ncut (valid_access m2 chunk b2 (signed ofs1 + delta));
        ##[ napply (valid_access_inj … Hvalid); //;
        ##| *; #_; #Hlo; #Hhi; #_; (* arith *) napply daemon
        ##]
      ##]
    ##| /2/
    ##]
##] nqed.

nlemma valid_pointer_inject_no_overflow:
  ∀f,m1,m2,b,ofs,b',x.
  mem_inject f m1 m2 →
  valid_pointer m1 b (signed ofs) = true →
  f b = Some ? 〈b', x〉 →
  min_signed ≤ signed ofs + signed (repr x) ∧ signed ofs + signed (repr x) ≤ max_signed.
#f;#m1;#m2;#b;#ofs;#b';#x;
*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
#Hvalid;#Hb1inj;
nlapply ((proj1 ?? (valid_pointer_valid_access ???)) Hvalid); #Hvalid';
ncut (valid_access m2 Mint8unsigned b' (signed ofs + x));
##[ napply (valid_access_inj … Hvalid'); // ##]
*; nrewrite > (?:size_chunk Mint8unsigned = 1); ##[ ##2: // ##] #_; #Hlo; #Hhi; #_;
nrewrite > (signed_repr ??); ##[ ##2: /2/; ##]
nlapply (mi_range_2 … Hb1inj); *;
##[ #ex; nrewrite > ex; nrewrite > (Zplus_z_OZ ?); napply signed_range;
##| (* arith *) napply daemon
##] nqed.

(* XXX: should use ndestruct, but reduces large definitions *)
nremark vptr_eq: ∀b,b',i,i'. Vptr b i = Vptr b' i' → b = b' ∧ i = i'.
#b b' i i' e; ndestruct; /2/; nqed. 

nlemma valid_pointer_inject:
  ∀f,m1,m2,b,ofs,b',ofs'.
  mem_inject f m1 m2 →
  valid_pointer m1 b (signed ofs) = true →
  val_inject f (Vptr psp b ofs) (Vptr b' ofs') →
  valid_pointer m2 b' (signed ofs') = true.
#f;#m1;#m2;#b;#ofs;#b';#ofs';
#Hinj; #Hvalid; #Hvinj; ninversion Hvinj;
##[ ##1,2,4: #x;#H;ndestruct; ##]
#b0;#i;#b0';#i';#delta;#Hb;#Hi';#eptr;#eptr';
nrewrite < (proj1 … (vptr_eq ???? eptr)) in Hb; nrewrite < (proj1 … (vptr_eq ???? eptr'));
nrewrite < (proj2 … (vptr_eq ???? eptr)) in Hi'; nrewrite < (proj2 … (vptr_eq ???? eptr'));
  #Hofs; #Hbinj;
nrewrite > Hofs;
nlapply (valid_pointer_inject_no_overflow … Hinj Hvalid Hbinj); #NOOV;
nelim Hinj;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
nrewrite > (add_signed ??); nrewrite > (signed_repr ??); //;
nrewrite > (signed_repr ??); /2/;
napply (valid_pointer_inj … mi_inj Hvalid); //;
nqed.

nlemma different_pointers_inject:
  ∀f,m,m',b1,ofs1,b2,ofs2,b1',delta1,b2',delta2.
  mem_inject f m m' →
  b1 ≠ b2 →
  valid_pointer m b1 (signed ofs1) = true →
  valid_pointer m b2 (signed ofs2) = true →
  f b1 = Some ? 〈b1', delta1〉 →
  f b2 = Some ? 〈b2', delta2〉 →
  b1' ≠ b2' ∨
  signed (add ofs1 (repr delta1)) ≠
  signed (add ofs2 (repr delta2)).
#f;#m;#m';#b1;#ofs1;#b2;#ofs2;#b1';#delta1;#b2';#delta2;
#Hinj;#neb;#Hval1;#Hval2;#Hf1;#Hf2;
nlapply ((proj1 ?? (valid_pointer_valid_access …)) Hval1); #Hval1';
nlapply ((proj1 ?? (valid_pointer_valid_access …)) Hval2); #Hval2';
nrewrite > (address_inject … Hinj Hval1' Hf1);
nrewrite > (address_inject … Hinj Hval2' Hf2);
nelim Hval1'; #Hbval; #Hlo; #Hhi;#Hal; nwhd in Hhi:(?(??%)?);
nelim Hval2'; #Hbval2; #Hlo2; #Hhi2;#Hal2; nwhd in Hhi2:(?(??%)?);
nlapply (mi_no_overlap ??? Hinj … Hf1 Hf2 …); //;
*; ##[
*; ##[
*; ##[ /2/;
   ##| (* arith contradiction *) napply daemon ##]
   ##| (* arith contradiction *) napply daemon ##]
   ##| *; ##[ #H;@2; (* arith *) napply daemon 
          ##| #H;@2; (* arith *) napply daemon  ##] ##]
nqed.

(* Relation between injections and loads. *)

nlemma load_inject:
  ∀f,m1,m2,chunk,b1,ofs,b2,delta,v1.
  mem_inject f m1 m2 →
  load chunk m1 b1 ofs = Some ? v1 →
  f b1 = Some ? 〈b2, delta〉 →
  ∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2 ∧ val_inject f v1 v2.
#f;#m1;#m2;#chunk;#b1;#ofs;#b2;#delta;#v1;
*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
#LOAD;#Hbinj;
napply mi_inj; //;
nqed.

nlemma loadv_inject:
  ∀f,m1,m2,chunk,a1,a2,v1.
  mem_inject f m1 m2 →
  loadv chunk m1 a1 = Some ? v1 →
  val_inject f a1 a2 →
  ∃v2. loadv chunk m2 a2 = Some ? v2 ∧ val_inject f v1 v2.
#f;#m1;#m2;#chunk;#a1;#a2;#v1;
#Hinj;#LOADV;#Hvinj; ninversion Hvinj;
##[ ##1,2,4: #x;#ex;#ex'; napply False_ind; ndestruct; ##]
#b;#ofs;#b';#ofs';#delta;#Hbinj;#Hofs;#ea1;#ea2;
nrewrite > ea1 in LOADV; #LOADV; 
nlapply (load_inject … Hinj LOADV … Hbinj); *; #v2; *; #LOAD; #INJ;
@ v2; @; //; nrewrite > Hofs;
nrewrite < (?:signed (add ofs (repr delta)) = signed ofs + delta) in LOAD;
##[ #H; napply H; (* XXX: used to work with /2/ *)
##| napply (address_inject … chunk … Hinj ? Hbinj); napply (load_valid_access …);
    ##[ ##2: napply LOADV; ##]
##] nqed.

(* Relation between injections and stores. *)

ninductive val_content_inject (f: meminj): memory_chunk → val → val → Prop ≝
  | val_content_inject_base:
      ∀chunk,v1,v2.
      val_inject f v1 v2 →
      val_content_inject f chunk v1 v2
  | val_content_inject_8:
      ∀chunk,n1,n2.
      chunk = Mint8unsigned ∨ chunk = Mint8signed →
      zero_ext 8 n1 = zero_ext 8 n2 →
      val_content_inject f chunk (Vint n1) (Vint n2)
  | val_content_inject_16:
      ∀chunk,n1,n2.
      chunk = Mint16unsigned ∨ chunk = Mint16signed →
      zero_ext 16 n1 = zero_ext 16 n2 →
      val_content_inject f chunk (Vint n1) (Vint n2)
  | val_content_inject_32:
      ∀f1,f2.
      singleoffloat f1 = singleoffloat f2 →
      val_content_inject f Mfloat32 (Vfloat f1) (Vfloat f2).

(*Hint Resolve val_content_inject_base.*)

nlemma load_result_inject:
  ∀f,chunk,v1,v2,chunk'.
  val_content_inject f chunk v1 v2 →
  size_chunk chunk = size_chunk chunk' →
  val_inject f (load_result chunk' v1) (load_result chunk' v2).
#f;#chunk;#v1;#v2;#chunk';
#Hvci; ninversion Hvci;
##[ #chunk'';#v1';#v2';#Hvinj;#_;#_;#_;#Hsize; ninversion Hvinj;
  ##[ ncases chunk'; #i;#_;#_; ##[ ##1,2,3,4,5: @ ##| ##6,7: @4 ##]
  ##| ncases chunk'; #f;#_;#_; ##[ ##1,2,3,4,5: @4 ##| ##6,7: @2 ##]
  ##| ncases chunk'; #b1;#ofs1;#b2;#ofs2;#delta;#Hmap;#Hofs;#_;#_; ##[ ##5: @3; // ##| ##*: @4 ##]
  ##| ncases chunk'; #v;#_;#_; @4;
  ##]
(* FIXME: the next two cases are very similar *)
##| #chunk'';#i;#i';*;#echunk;nrewrite > echunk;#Hz;#_;#_;#_;
    nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct;
    ##[ ##2,4: nwhd in ⊢ (??%%); nrewrite > Hz; @
    ##| ##1,3: nwhd in ⊢ (??%%); nrewrite > (sign_ext_equal_if_zero_equal … Hz);
        @; ##[ ##1,3: napply I; ##| ##2,4: napply leb_true_to_le; @; ##]
    ##]
##| #chunk'';#i;#i';*;#echunk;nrewrite > echunk;#Hz;#_;#_;#_;
    nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct;
    ##[ ##2,4: nwhd in ⊢ (??%%); nrewrite > Hz; @
    ##| ##1,3: nwhd in ⊢ (??%%); nrewrite > (sign_ext_equal_if_zero_equal … Hz);
        @; ##[ ##1,3: napply I; ##| ##2,4: napply leb_true_to_le; @; ##]
    ##]

##| #f;#f';#float;#echunk;nrewrite > echunk;#_;#_;
    nelim chunk'; nwhd in ⊢ ((??%%)→?); #Hsize; ndestruct;
    ##[ @4; ##| nrewrite > float; @2 ##]
##] nqed.

nlemma store_mapped_inject_1 :
  ∀f,chunk,m1,b1,ofs,v1,n1,m2,b2,delta,v2.
  mem_inject f m1 m2 →
  store chunk m1 b1 ofs v1 = Some ? n1 →
  f b1 = Some ? 〈b2, delta〉 →
  val_content_inject f chunk v1 v2 →
  ∃n2.
    store chunk m2 b2 (ofs + delta) v2 = Some ? n2
    ∧ mem_inject f n1 n2.
#f;#chunk;#m1;#b1;#ofs;#v1;#n1;#m2;#b2;#delta;#v2;
*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
#STORE1; #INJb1; #Hvcinj;
nlapply (store_mapped_inj … mi_inj mi_no_overlap INJb1 STORE1 ?); //;
##[ #chunk';#Hchunksize;napply (load_result_inject … chunk …);//;
##| ##skip ##]
*;#n2;*;#STORE;#MINJ;
@ n2; @; //; @;
##[ (* inj *) //
##| (* freeblocks *) #b;#notvalid; napply mi_freeblocks;
    napply (not_to_not ??? notvalid); napply (store_valid_block_1 … STORE1);
##| (* mappedblocks *) #b;#b';#delta';#INJb';napply (store_valid_block_1 … STORE);
    /2/;
##| (* no_overlap *) nwhd; #b1';#b1'';#delta1';#b2';#b2'';#delta2';#neqb';
    #fb1';#fb2';
    nrewrite > (low_bound_store … STORE1 ?);  nrewrite > (low_bound_store … STORE1 ?);
    nrewrite > (high_bound_store … STORE1 ?);  nrewrite > (high_bound_store … STORE1 ?);
    napply mi_no_overlap; //;
##| (* range *) /2/;
##| (* range 2 *) #b;#b';#delta';#INJb;
    nrewrite > (low_bound_store … STORE ?);
    nrewrite > (high_bound_store … STORE ?);
    napply mi_range_2; //;
##] nqed.

nlemma store_mapped_inject:
  ∀f,chunk,m1,b1,ofs,v1,n1,m2,b2,delta,v2.
  mem_inject f m1 m2 →
  store chunk m1 b1 ofs v1 = Some ? n1 →
  f b1 = Some ? 〈b2, delta〉 →
  val_inject f v1 v2 →
  ∃n2.
    store chunk m2 b2 (ofs + delta) v2 = Some ? n2
    ∧ mem_inject f n1 n2.
#f;#chunk;#m1;#b1;#ofs;#v1;#n1;#m2;#b2;#delta;#v2;
#MINJ;#STORE;#INJb1;#Hvalinj;napply (store_mapped_inject_1 … STORE);//;
napply val_content_inject_base;//;
nqed.

nlemma store_unmapped_inject:
  ∀f,chunk,m1,b1,ofs,v1,n1,m2.
  mem_inject f m1 m2 →
  store chunk m1 b1 ofs v1 = Some ? n1 →
  f b1 = None ? →
  mem_inject f n1 m2.
#f;#chunk;#m1;#b1;#ofs;#v1;#n1;#m2;
*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
#STORE;#INJb1;@;
##[ (* inj *) napply (store_unmapped_inj … STORE); //
##| (* freeblocks *) #b;#notvalid; napply mi_freeblocks;
    napply (not_to_not ??? notvalid); napply (store_valid_block_1 … STORE);
##| (* mappedblocks *) #b;#b';#delta;#INJb; napply mi_mappedblock; //;
##| (* no_overlap *) nwhd; #b1';#b1'';#delta1';#b2';#b2'';#delta2';#neqb';
    #fb1';#fb2';
    nrewrite > (low_bound_store … STORE ?);  nrewrite > (low_bound_store … STORE ?);
    nrewrite > (high_bound_store … STORE ?);  nrewrite > (high_bound_store … STORE ?);
    napply mi_no_overlap; //;
##| (* range *) /2/
##| /2/
##] nqed.

nlemma storev_mapped_inject_1:
  ∀f,chunk,m1,a1,v1,n1,m2,a2,v2.
  mem_inject f m1 m2 →
  storev chunk m1 a1 v1 = Some ? n1 →
  val_inject f a1 a2 →
  val_content_inject f chunk v1 v2 →
  ∃n2.
    storev chunk m2 a2 v2 = Some ? n2 ∧ mem_inject f n1 n2.
#f;#chunk;#m1;#a1;#v1;#n1;#m2;#a2;#v2;
#MINJ;#STORE;#Hvinj;#Hvcinj;
ninversion Hvinj;
##[ ##1,2,4:#x;#ex1;#ex2;nrewrite > ex1 in STORE; nwhd in ⊢ ((??%?)→?); #H;
    napply False_ind; ndestruct; ##]
#b;#ofs;#b';#ofs';#delta;#INJb;#Hofs;#ea1;#ea2;
nrewrite > Hofs; nrewrite > ea1 in STORE; #STORE;
nlapply (store_mapped_inject_1 … MINJ STORE … INJb Hvcinj); 
nrewrite < (?:signed (add ofs (repr delta)) = signed ofs + delta); //;
napply (address_inject … chunk … MINJ ? INJb);
napply (store_valid_access_3 … STORE);
nqed.

nlemma storev_mapped_inject:
  ∀f,chunk,m1,a1,v1,n1,m2,a2,v2.
  mem_inject f m1 m2 →
  storev chunk m1 a1 v1 = Some ? n1 →
  val_inject f a1 a2 →
  val_inject f v1 v2 →
  ∃n2.
    storev chunk m2 a2 v2 = Some ? n2 ∧ mem_inject f n1 n2.
#f;#chunk;#m1;#a1;#v1;#n1;#m2;#a2;#v2; #MINJ;#STOREV;#Hvinj;#Hvinj';
napply (storev_mapped_inject_1 … STOREV); /2/;
nqed.

(* Relation between injections and [free] *)

nlemma meminj_no_overlap_free:
  ∀mi,m,b.
  meminj_no_overlap mi m →
  meminj_no_overlap mi (free m b).
#mi;#m;#b;#H;nwhd;#b1;#b1';#delta1;#b2;#b2';#delta2;#Hne;#mi1;#mi2;
ncut (low_bound (free m b) b ≥ high_bound (free m b) b);
##[ nrewrite > (low_bound_free_same …); nrewrite > (high_bound_free_same …);// ##]
#Hbounds;
ncases (decidable_eq_Z b1 b);#e1; ##[ nrewrite > e1 in Hne mi1 ⊢ %;#Hne;#mi1;##]
ncases (decidable_eq_Z b2 b);#e2; ##[ ##1,3: nrewrite > e2 in Hne mi2 ⊢ %;#Hne;#mi2;##]
##[ napply False_ind; nelim Hne; /2/
##| @;@2;//;
##| @;@;@2;//
##| nrewrite > (low_bound_free …);//; nrewrite > (low_bound_free …);//;
    nrewrite > (high_bound_free …);//; nrewrite > (high_bound_free …);//;
    /2/;
##] nqed.

nlemma meminj_no_overlap_free_list:
  ∀mi,m,bl.
  meminj_no_overlap mi m →
  meminj_no_overlap mi (free_list m bl).
#mi;#m;#bl; nelim bl;
##[ #H; nwhd in ⊢ (??%); //
##| #h;#t; #IH; #H; napply meminj_no_overlap_free; napply IH; //
##] nqed.

nlemma free_inject:
  ∀f,m1,m2,l,b.
  (∀b1,delta. f b1 = Some ? 〈b, delta〉 → in_list ? b1 l) →
  mem_inject f m1 m2 →
  mem_inject f (free_list m1 l) (free m2 b).
#f;#m1;#m2;#l;#b;#mappedin;
*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
@;
##[ (* inj *)
    napply free_right_inj; ##[ napply free_list_left_inj; //; ##]
    #b1;#delta;#chunk;#ofs;#INJb1; napply nmk; #Hvalid;
    nelim (valid_access_free_list_inv … Hvalid); #b1ni; #Haccess;
    napply (absurd ? (mappedin ?? INJb1) b1ni);
##| (* freeblocks *)
    #b';#notvalid; napply mi_freeblocks; napply (not_to_not ??? notvalid);
    #H; napply valid_block_free_list_1; //
##| (* mappedblocks *)
    #b1;#b1';#delta;#INJb1; napply valid_block_free_1; /2/
##| (* overlap *)
    napply meminj_no_overlap_free_list; //
##| (* range *)
    /2/
##| #b1;#b2;#delta;#INJb1; ncases (decidable_eq_Z b2 b); #eb;
    ##[ nrewrite > eb;
        nrewrite > (low_bound_free_same ??); nrewrite > (high_bound_free_same ??);
        @2; (* arith *) napply daemon
    ##| nrewrite > (low_bound_free …); //; nrewrite > (high_bound_free …); /2/;
    ##]
##] nqed.

(* Monotonicity properties of memory injections. *)

ndefinition inject_incr : meminj → meminj → Prop ≝ λf1,f2.
  ∀b. f1 b = f2 b ∨ f1 b = None ?.

nlemma inject_incr_refl :
   ∀f. inject_incr f f .
#f;nwhd;#b;@;//; nqed.

nlemma inject_incr_trans :
  ∀f1,f2,f3. 
  inject_incr f1 f2 → inject_incr f2 f3 → inject_incr f1 f3 .
#f1;#f2;#f3;nwhd in ⊢ (%→%→%);#H1;#H2;#b;
nelim (H1 b); nelim (H2 b); /2/; nqed.

nlemma val_inject_incr:
  ∀f1,f2,v,v'.
  inject_incr f1 f2 →
  val_inject f1 v v' →
  val_inject f2 v v'.
#f1;#f2;#v;#v';#Hincr;#Hvinj;
ninversion Hvinj;
##[ ##1,2,4: #x;#_;#_; //;
##|#b;#ofs;#b';#ofs';#delta; #INJb; #Hofs; #_;#_; 
nelim (Hincr b); #H;
##[ napply (val_inject_ptr ??????? Hofs); /2/;
##| napply False_ind; nrewrite > INJb in H; #H; ndestruct;
##] nqed.

nlemma val_list_inject_incr:
  ∀f1,f2,vl,vl'.
  inject_incr f1 f2 → val_list_inject f1 vl vl' →
  val_list_inject f2 vl vl'.
#f1;#f2;#vl;nelim vl;
##[ #vl'; #Hincr; #H; ninversion H; //; #v;#v';#l;#l0;#_;#_;#_; #H; ndestruct;
##| #h;#t;#IH;#vl';#Hincr;#H1; ninversion H1;
  ##[ #H; ndestruct
  ##| #h';#h'';#t';#t''; #Hinj1; #Hintt; #_; #e1; #e2; ndestruct;
      @2;/2/; napply IH; //; napply Hincr;
  ##]
##] nqed.

(*
Hint Resolve inject_incr_refl val_inject_incr val_list_inject_incr.
*)

(* Properties of injections and allocations. *)

ndefinition extend_inject ≝
       λb: block. λx: option (block × Z). λf: meminj.
  λb': block. if eqZb b' b then x else f b'.

nlemma extend_inject_incr:
  ∀f,b,x.
  f b = None ? →
  inject_incr f (extend_inject b x f).
#f;#b;#x;#INJb;nwhd;#b'; nwhd in ⊢ (?(???%)?);
napply (eqZb_elim b' b); #eb; /2/;
nqed.

nlemma alloc_right_inject:
  ∀f,m1,m2,lo,hi,m2',b.
  mem_inject f m1 m2 →
  alloc m2 lo hi = 〈m2', b〉 →
  mem_inject f m1 m2'.
#f;#m1;#m2;#lo;#hi;#m2';#b;
*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
#ALLOC; @;
##[ napply (alloc_right_inj … ALLOC); //;
##| /2/;
##| #b1;#b2;#delta;#INJb1; napply (valid_block_alloc … ALLOC); /2/;
##| //;
##| /2/;
##|#b1;#b2;#delta;#INJb1; nrewrite > (?:low_bound m2' b2 = low_bound m2 b2);
   ##[ nrewrite > (?:high_bound m2' b2 = high_bound m2 b2); /2/;
       napply high_bound_alloc_other; /2/;
   ##| napply low_bound_alloc_other; /2/
   ##]
##] nqed.

nlemma alloc_unmapped_inject:
  ∀f,m1,m2,lo,hi,m1',b.
  mem_inject f m1 m2 →
  alloc m1 lo hi = 〈m1', b〉 →
  mem_inject (extend_inject b (None ?) f) m1' m2 ∧
  inject_incr f (extend_inject b (None ?) f).
#f;#m1;#m2;#lo;#hi;#m1';#b;
*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
#ALLOC;
ncut (inject_incr f (extend_inject b (None ?) f));
##[ napply extend_inject_incr; napply mi_freeblocks; /2/; ##]
#Hinject_incr; @; //; @;
##[ (* inj *)
    napply (alloc_left_unmapped_inj … ALLOC); 
    ##[ ##2: nwhd in ⊢ (??%?); nrewrite > (eqZb_z_z …); /2/; ##]
    nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta;
    nwhd in ⊢ ((??%?)→?→?); napply eqZb_elim; #e; nwhd in ⊢ ((??%?)→?→?);
    #Hextend;#LOAD;
    ##[ ndestruct;
    ##| nlapply (mi_inj … Hextend LOAD); *; #v2; *; #LOAD2; #VINJ;
    @ v2; @; //;
    napply val_inject_incr; //;
    ##]
##| (* freeblocks *)
    #b';#Hinvalid; nwhd in ⊢ (??%?); napply (eqZb_elim b' b); //;
    #neb; napply mi_freeblocks; napply (not_to_not ??? Hinvalid);
    napply valid_block_alloc; //;
##| (* mappedblocks *)
    #b1;#b2;#delta; nwhd in ⊢ (??%?→?); napply (eqZb_elim b1 b); #eb;
    ##[ #H; ndestruct;
    ##| #H; napply (mi_mappedblock … H);
    ##]
##| (* overlap *)
    nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2; #neb1; nwhd in ⊢ (??%?→??%?→?);
    nrewrite > (low_bound_alloc … ALLOC ?); nrewrite > (low_bound_alloc … ALLOC ?);
    nrewrite > (high_bound_alloc … ALLOC ?); nrewrite > (high_bound_alloc … ALLOC ?);
    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
    ##[ ndestruct
    ##| nlapply (eqZb_to_Prop b2 b); nelim (eqZb b2 b); #e2; #INJb2;
      ##[ ndestruct
      ##| napply mi_no_overlap; /2/;
      ##]
    ##]
##| (* range *) 
    #b1;#b2;#delta; nwhd in ⊢ (??%?→?);
    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
    ##[ ndestruct
    ##| napply (mi_range_1 … INJb1);
    ##]
##| #b1;#b2;#delta; nwhd in ⊢ (??%?→?);
    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
    ##[  ndestruct
    ##| napply (mi_range_2 … INJb1);
    ##]
##] nqed.

nlemma alloc_mapped_inject:
  ∀f,m1,m2,lo,hi,m1',b,b',ofs.
  mem_inject f m1 m2 →
  alloc m1 lo hi = 〈m1', b〉 →
  valid_block m2 b' →
  min_signed ≤ ofs ∧ ofs ≤ max_signed →
  min_signed ≤ low_bound m2 b' →
  high_bound m2 b' ≤ max_signed →
  low_bound m2 b' ≤ lo + ofs →
  hi + ofs ≤ high_bound m2 b' →
  inj_offset_aligned ofs (hi-lo) →
  (∀b0,ofs0. 
   f b0 = Some ? 〈b', ofs0〉 → 
   high_bound m1 b0 + ofs0 ≤ lo + ofs ∨
   hi + ofs ≤ low_bound m1 b0 + ofs0) →
  mem_inject (extend_inject b (Some ? 〈b', ofs〉) f) m1' m2 ∧
  inject_incr f (extend_inject b (Some ? 〈b', ofs〉) f).
#f;#m1;#m2;#lo;#hi;#m1';#b;#b';#ofs;
*;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
#ALLOC;#validb';#rangeofs;#rangelo;#rangehi;#boundlo;#boundhi;#injaligned;#boundmapped;
ncut (inject_incr f (extend_inject b (Some ? 〈b', ofs〉) f));
##[ napply extend_inject_incr; napply mi_freeblocks; /2/; ##]
#Hincr; @; //; @;
##[ (* inj *)
    napply (alloc_left_mapped_inj … ALLOC … validb' boundlo boundhi); /2/;
    ##[ ##2:nwhd in ⊢ (??%?); nrewrite > (eqZb_z_z …); /2/; ##]
    nwhd; #chunk;#b1;#ofs';#v1;#b2;#delta;#Hextend;#LOAD;
    nwhd in Hextend:(??%?); nrewrite > (eqZb_false b1 b ?) in Hextend;
    ##[ #Hextend; nlapply (mi_inj … Hextend LOAD);
        *; #v2; *; #LOAD2; #VINJ;
    @ v2; @; //;
    napply val_inject_incr; //;
    ##| napply (valid_not_valid_diff m1); /2/;
        napply (valid_access_valid_block … chunk … ofs'); /2/;
    ##]
##| (* freeblocks *)
    #b';#Hinvalid; nwhd in ⊢ (??%?); nrewrite > (eqZb_false b' b ?);
    ##[ napply mi_freeblocks; napply (not_to_not ??? Hinvalid);
    napply valid_block_alloc; //;
    ##| napply sym_neq; napply (valid_not_valid_diff m1'); //;
        napply (valid_new_block … ALLOC);
    ##]
##| (* mappedblocks *)
    #b1;#b2;#delta; nwhd in ⊢ (??%?→?); napply (eqZb_elim b1 b); #eb;#einj;
    ##[ ndestruct; //;
    ##| napply (mi_mappedblock … einj);
    ##]
##| (* overlap *)
    nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2; #neb1; nwhd in ⊢ (??%?→??%?→?);
    nrewrite > (low_bound_alloc … ALLOC ?); nrewrite > (low_bound_alloc … ALLOC ?);
    nrewrite > (high_bound_alloc … ALLOC ?); nrewrite > (high_bound_alloc … ALLOC ?);
    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
    ##[ nelim (grumpydestruct2 ?????? INJb1); #eb1';#eofs1 ##]
    nlapply (eqZb_to_Prop b2 b); nelim (eqZb b2 b); #e2; #INJb2;
    ##[ nelim (grumpydestruct2 ?????? INJb2); #eb2';#eofs2 ##]
    ##[ napply False_ind; nrewrite > e in neb1; nrewrite > e2; /2/;
    ##| nelim (decidable_eq_Z b1' b2'); #e';
        ##[ nrewrite < e' in INJb2 ⊢ %; nrewrite < eb1'; nrewrite < eofs1; #INJb2; nlapply (boundmapped … INJb2);
            *; #H; @2; ##[ @2 ##| @1 ##] napply H;
        ##| @1;@1;@1; napply e'
        ##]
    ##| nelim (decidable_eq_Z b1' b2'); #e';
        ##[ nrewrite < e' in INJb2 ⊢ %; #INJb2; nelim (grumpydestruct2 ?????? INJb2); #eb'; #eofs; nrewrite < eb' in INJb1; nrewrite < eofs; #INJb1; nlapply (boundmapped … INJb1);
            *; #H; @2; ##[ @1; /2/ ##| @2; napply H; ##]
        ##| @1;@1;@1; napply e'
        ##]
    ##| napply mi_no_overlap; /2/;
    ##]
##| (* range *) 
    #b1;#b2;#delta; nwhd in ⊢ (??%?→?);
    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
    ##[ ndestruct; /2/;
    ##| napply (mi_range_1 … INJb1);
    ##]
##| #b1;#b2;#delta; nwhd in ⊢ (??%?→?);
    nlapply (eqZb_to_Prop b1 b); nelim (eqZb b1 b); #e; #INJb1;
    ##[ ndestruct; @2;@;/2/;
    ##| napply (mi_range_2 … INJb1);
    ##]
##] nqed.

nlemma alloc_parallel_inject:
  ∀f,m1,m2,lo,hi,m1',m2',b1,b2.
  mem_inject f m1 m2 →
  alloc m1 lo hi = 〈m1', b1〉 →
  alloc m2 lo hi = 〈m2', b2〉 →
  min_signed ≤ lo → hi ≤ max_signed →
  mem_inject (extend_inject b1 (Some ? 〈b2, OZ〉) f) m1' m2' ∧
  inject_incr f (extend_inject b1 (Some ? 〈b2, OZ〉) f).
#f;#m1;#m2;#lo;#hi;#m1';#m2';#b1;#b2;
#Hminj;#ALLOC1;#ALLOC2;#Hlo;#Hhi;
napply (alloc_mapped_inject … ALLOC1); /2/;
##[ napply (alloc_right_inject … Hminj ALLOC2);
##| nrewrite > (low_bound_alloc_same … ALLOC2); //
##| nrewrite > (high_bound_alloc_same … ALLOC2); //
##| nrewrite > (low_bound_alloc_same … ALLOC2); //
##| nrewrite > (high_bound_alloc_same … ALLOC2); //
##| nwhd; (* arith *) napply daemon
##| #b;#ofs;#INJb0; napply False_ind;
    nelim Hminj;#mi_inj;#mi_freeblocks;#mi_mappedblock;#mi_no_overlap;#mi_range_1;#mi_range_2;
    nlapply (mi_mappedblock … INJb0);
    #H; napply (absurd ? H ?); /2/;
##] nqed.

ndefinition meminj_init ≝ λm: mem.
  λb: block. if Zltb b (nextblock m) then Some ? 〈b, OZ〉 else None ?.

ndefinition mem_inject_neutral ≝ λm: mem.
  ∀f,chunk,b,ofs,v.
  load chunk m b ofs = Some ? v → val_inject f v v.

nlemma init_inject:
  ∀m.
  mem_inject_neutral m →
  mem_inject (meminj_init m) m m.
#m;#neutral;@;
##[ (* inj *)
    nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta; nwhd in ⊢ (??%?→?→?);
    napply Zltb_elim_Type0; #ltb1; ##[
    #H; nelim (grumpydestruct2 ?????? H); #eb1; #edelta;
    nrewrite < eb1; nrewrite < edelta; #LOAD; @v1; @; //;
    napply neutral; //;
    ##| #H;nwhd in H:(??%?); ndestruct;
    ##] 
##| (* free blocks *)
    #b;nrewrite > (unfold_valid_block …); nwhd in ⊢ (?→??%?); #notvalid;
    napply Zltb_elim_Type0; #ltb1;
    ##[ napply False_ind; napply (absurd ? ltb1 notvalid)
    ##| //
    ##]
##| (* mapped blocks *)
    #b;#b';#delta;nwhd in ⊢ (??%?→?); nrewrite > (unfold_valid_block …);
    napply Zltb_elim_Type0; #ltb;
    #H; nwhd in H:(??%?); ndestruct; //
##| (* overlap *) 
    nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2;#neb1; nwhd in ⊢(??%?→??%?→?);
    napply Zltb_elim_Type0; #ltb1;
    ##[ #H; nwhd in H:(??%?); ndestruct;
        napply Zltb_elim_Type0; #ltb2;
        #H2; nwhd in H2:(??%?); ndestruct; @;@;@;/2/;
    ##| #H; nwhd in H:(??%?); ndestruct;
    ##]
##| (* range *)
    #b;#b';#delta;nwhd in ⊢ (??%?→?);
    napply Zltb_elim_Type0; #ltb;
    ##[ #H; nelim (grumpydestruct2 ?????? H); #eb; #edelta; nrewrite < edelta;
        (* FIXME: should be in integers.ma *) napply daemon
    ##| #H; nwhd in H:(??%?); ndestruct;
    ##]
##| (* range *)
    #b;#b';#delta;nwhd in ⊢ (??%?→?);
    napply Zltb_elim_Type0; #ltb;
    ##[ #H; nelim (grumpydestruct2 ?????? H); #eb; #edelta; nrewrite < edelta;
        (* FIXME: should be in integers.ma *) napply daemon
    ##| #H; nwhd in H:(??%?); ndestruct;
    ##]
##] nqed.

nremark getN_setN_inject:
  ∀f,m,v,n1,p1,n2,p2.
  val_inject f (getN n2 p2 m) (getN n2 p2 m) →
  val_inject f v v →
  val_inject f (getN n2 p2 (setN n1 p1 v m))
               (getN n2 p2 (setN n1 p1 v m)).
#f;#m;#v;#n1;#p1;#n2;#p2;#injget;#injv;
ncases (getN_setN_characterization m v n1 p1 n2 p2);##[ * ##] #A;
nrewrite > A; //;
nqed.
             
nremark getN_contents_init_data_inject:
  ∀f,n,ofs,id,pos.
  val_inject f (getN n ofs (contents_init_data pos id))
               (getN n ofs (contents_init_data pos id)).
#f;#n;#ofs;#id;nelim id;
##[ #pos; nrewrite > (getN_init …); //
##| #h;#t;#IH;#pos; ncases h;
##[ ##1,2,3,4,5: #x; napply getN_setN_inject; //
##| ##6,8: #x; napply IH ##| #x;#y;napply IH ##] (* XXX // doesn't work? *)
nqed.

nlemma alloc_init_data_neutral:
  ∀m,id,m',b.
  mem_inject_neutral m →
  alloc_init_data m id = 〈m', b〉 →
  mem_inject_neutral m'.
#m;#id;#m';#b;#Hneutral;#INIT; nwhd in INIT:(??%?); (* XXX: ndestruct makes a bit of a mess *)
napply (pairdisc_elim … INIT);
nwhd in ⊢ (??%% → ?);#B;nrewrite < B in ⊢ (??%% → ?);
nwhd in ⊢ (??%% → ?);#A;
nwhd; #f;#chunk;#b';#ofs;#v; #LOAD;
nlapply (load_inv … LOAD); *; #C; #D;
nrewrite < B in D; nrewrite > A;
nrewrite > (unfold_update block_contents …); napply eqZb_elim;
##[ #eb'; #D; nwhd in D:(???(??(???%))); nrewrite > D;
    napply (load_result_inject … chunk); //; @;
    napply getN_contents_init_data_inject;
##| #neb'; #D; napply (Hneutral ? chunk b' ofs ??); nwhd in ⊢ (??%?);
    nrewrite > (in_bounds_true m chunk b' ofs (option ?) …);
    ##[ nrewrite < D; //
    ##| nelim C; #Cval;#Clo;#Chi;#Cal; @;
    ##[ nrewrite > (unfold_valid_block …);
        nrewrite > (unfold_valid_block …) in Cval; nrewrite < B;
        (* arith using neb' *) napply daemon
    ##| nrewrite > (?:low_bound m b' = low_bound m' b'); //;
        nwhd in ⊢ (??%%); nrewrite < B; nrewrite > A;
        nrewrite > (update_o block_contents …); //; napply sym_neq; //;
    ##| nrewrite > (?:high_bound m b' = high_bound m' b'); //;
        nwhd in ⊢ (??%%); nrewrite < B; nrewrite > A;
        nrewrite > (update_o block_contents …); //; napply sym_neq; //;
    ##| //;
    ##]
##] nqed.


(* ** Memory shifting *)

(* A special case of memory injection where blocks are not coalesced:
  each source block injects in a distinct target block. *)

ndefinition memshift ≝ block → option Z.

ndefinition meminj_of_shift : memshift → meminj ≝ λmi: memshift.
  λb. match mi b with [ None ⇒ None ? | Some x ⇒ Some ? 〈b, x〉 ].

ndefinition val_shift ≝ λmi: memshift. λv1,v2: val.
  val_inject (meminj_of_shift mi) v1 v2.

nrecord mem_shift (f: memshift) (m1,m2: mem) : Prop :=
  {
    ms_inj:
      mem_inj val_inject (meminj_of_shift f) m1 m2;
    ms_samedomain:
      nextblock m1 = nextblock m2;
    ms_domain:
      ∀b. match f b with [ Some _ ⇒ b < nextblock m1 | None ⇒ b ≥ nextblock m1 ];
    ms_range_1:
      ∀b,delta.
      f b = Some ? delta →
      min_signed ≤ delta ∧ delta ≤ max_signed;
    ms_range_2:
      ∀b,delta.
      f b = Some ? delta →
      min_signed ≤ low_bound m2 b ∧ high_bound m2 b ≤ max_signed
  }.

(* * The following lemmas establish the absence of machine integer overflow
  during address computations. *)

nlemma address_shift:
  ∀f,m1,m2,chunk,b,ofs1,delta.
  mem_shift f m1 m2 →
  valid_access m1 chunk b (signed ofs1) →
  f b = Some ? delta →
  signed (add ofs1 (repr delta)) = signed ofs1 + delta.
#f;#m1;#m2;#chunk;#b;#ofs1;#delta;
*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;#Hvalid_access;#INJb;
nelim (ms_range_2 … INJb); #Hlo;#Hhi;
nrewrite > (add_signed …);
nrewrite > (signed_repr …); nrewrite > (signed_repr …); /2/;
ncut (valid_access m2 chunk b (signed ofs1 + delta));
##[ napply (valid_access_inj ? (meminj_of_shift f) … ms_inj Hvalid_access);
    nwhd in ⊢ (??%?); nrewrite > INJb; // ##]
*; (* arith *) napply daemon;
nqed.

nlemma valid_pointer_shift_no_overflow:
  ∀f,m1,m2,b,ofs,x.
  mem_shift f m1 m2 →
  valid_pointer m1 b (signed ofs) = true →
  f b = Some ? x →
  min_signed ≤ signed ofs + signed (repr x) ∧ signed ofs + signed (repr x) ≤ max_signed.
#f;#m1;#m2;#b;#ofs;#x;
*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
#VALID;#INJb;
nlapply (proj1 ?? (valid_pointer_valid_access …) VALID); #Hvalid_access;
ncut (valid_access m2 Mint8unsigned b (signed ofs + x));
##[ napply (valid_access_inj … ms_inj Hvalid_access);
    nwhd in ⊢ (??%?); nrewrite > INJb; // ##]
*;#Hvalid_block;#Hlo;#Hhi;#Hal; nwhd in Hhi:(?(??%)?);
nrewrite > (signed_repr …); /2/;
nlapply (ms_range_2 … INJb);*;#A;#B;
(* arith *) napply daemon;
nqed.

(* FIXME to get around ndestruct problems *)
nlemma vptr_eq_1 : ∀b,b',ofs,ofs'. Vptr b ofs = Vptr b' ofs' → b = b'.
#b;#b';#ofs;#ofs';#H;ndestruct;//;
nqed.
nlemma vptr_eq_2 : ∀b,b',ofs,ofs'. Vptr b ofs = Vptr b' ofs' → ofs = ofs'.
#b;#b';#ofs;#ofs';#H;ndestruct;//;
nqed.

nlemma valid_pointer_shift:
  ∀f,m1,m2,b,ofs,b',ofs'.
  mem_shift f m1 m2 →
  valid_pointer m1 b (signed ofs) = true →
  val_shift f (Vptr b ofs) (Vptr b' ofs') →
  valid_pointer m2 b' (signed ofs') = true.
#f;#m1;#m2;#b;#ofs;#b';#ofs';#Hmem_shift;#VALID;#Hval_shift;
nwhd in Hval_shift; ninversion Hval_shift;
##[ ##1,2,4: #a; #H; ndestruct; ##]
#b1;#ofs1;#b2;#ofs2;#delta;#INJb1;#Hofs;#eb1;#eb2;
nrewrite < (vptr_eq_1 … eb1) in INJb1; nrewrite < (vptr_eq_1 … eb2); #INJb';
nrewrite < (vptr_eq_2 … eb1) in Hofs; nrewrite < (vptr_eq_2 … eb2); #Hofs; nrewrite > Hofs;
ncut (f b = Some ? delta);
##[ nwhd in INJb':(??%?); ncases (f b) in INJb' ⊢ %;
  ##[ #H; napply (False_ind … (grumpydestruct … H)); ##| #delta'; #H; nelim (grumpydestruct2 ?????? H); // ##]
##] #INJb;
nlapply (valid_pointer_shift_no_overflow … VALID INJb); //; #NOOV;
nelim Hmem_shift;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
nrewrite > (add_signed …); nrewrite > (signed_repr …); //;
nrewrite > (signed_repr …); /2/;
napply (valid_pointer_inj … VALID); /2/;
nqed.

(* Relation between shifts and loads. *)

nlemma load_shift:
  ∀f,m1,m2,chunk,b,ofs,delta,v1.
  mem_shift f m1 m2 →
  load chunk m1 b ofs = Some ? v1 →
  f b = Some ? delta →
  ∃v2. load chunk m2 b (ofs + delta) = Some ? v2 ∧ val_shift f v1 v2.
#f;#m1;#m2;#chunk;#b;#ofs;#delta;#v1;
*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
#LOAD; #INJb;
nwhd in ⊢ (??(λ_.??%)); napply (ms_inj … LOAD);
nwhd in ⊢ (??%?); nrewrite > INJb; //;
nqed.

nlemma loadv_shift:
  ∀f,m1,m2,chunk,a1,a2,v1.
  mem_shift f m1 m2 →
  loadv chunk m1 a1 = Some ? v1 →
  val_shift f a1 a2 →
  ∃v2. loadv chunk m2 a2 = Some ? v2 ∧ val_shift f v1 v2.
#f;#m1;#m2;#chunk;#a1;#a2;#v1;#Hmem_shift;#LOADV;#Hval_shift;
ninversion Hval_shift;
##[ ##1,2,4: #x;#H;nrewrite > H in LOADV;#H';nwhd in H':(??%?);napply False_ind; ndestruct; ##]
#b1;#ofs1;#b2;#ofs2;#delta;#INJb1;#Hofs;#ea1;#ea2; nrewrite > ea1 in LOADV; #LOADV;
nlapply INJb1; nwhd in ⊢ (??%? → ?);
nlapply (refl ? (f b1)); ncases (f b1) in ⊢ (???% → %);
##[ #_; nwhd in ⊢ (??%? → ?); #H; napply False_ind; napply (False_ind … (grumpydestruct … H));
##| #delta'; #DELTA; nwhd in ⊢ (??%? → ?); #H; nelim (grumpydestruct2 ?????? H);
    #eb;#edelta; 
##] nlapply (load_shift … Hmem_shift LOADV DELTA); *; #v2; *;#LOAD;#INJ;
@ v2; @; //; nrewrite > Hofs; nrewrite > eb in LOAD; nrewrite > edelta;
nrewrite < (?:signed (add ofs1 (repr delta)) = signed ofs1 + delta);
##[#H'; napply H'; (* XXX // doesn't work *) 
##| nrewrite < edelta; napply (address_shift … chunk … Hmem_shift … DELTA);
    napply (load_valid_access … LOADV);
##]
nqed.

(* Relation between shifts and stores. *)

nlemma store_within_shift:
  ∀f,chunk,m1,b,ofs,v1,n1,m2,delta,v2.
  mem_shift f m1 m2 →
  store chunk m1 b ofs v1 = Some ? n1 →
  f b = Some ? delta →
  val_shift f v1 v2 →
  ∃n2.
    store chunk m2 b (ofs + delta) v2 = Some ? n2
    ∧ mem_shift f n1 n2.
#f;#chunk;#m1;#b;#ofs;#v1;#n1;#m2;#delta;#v2;
*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
#STORE1;#INJb;#Hval_shift;
nlapply (store_mapped_inj … ms_inj ?? STORE1 ?);
##[ #chunk'; #echunk; napply (load_result_inject … chunk); /2/;
##| nwhd in ⊢ (??%?); nrewrite > INJb; (* XXX: // has stopped working *) napply refl
##| nwhd; #b1;#b1';#delta1;#b2;#b2';#delta2;
    nwhd in ⊢ (? → ??%? → ??%? → ?);
    nelim (f b1); nelim (f b2);
    ##[#_;#e1;nwhd in e1:(??%?);ndestruct;
    ##|#z;#_;#e1;nwhd in e1:(??%?);ndestruct;
    ##|#z;#_;#_;#e2;nwhd in e2:(??%?);ndestruct;
    ##|#delta1';#delta2';#neb;#e1;#e2;
       nwhd in e1:(??%?) e2:(??%?);
       ndestruct;
       @1;@1;@1;//;
    ##]
##| ##7: //;
##| ##4,5,6: ##skip
##]
*;#n2;*;#STORE;#MINJ;
@ n2; @; //; @;
##[ (* inj *) //
##| (* samedomain *)
    nrewrite > (nextblock_store … STORE1);
    nrewrite > (nextblock_store … STORE);
    //;
##| (* domain *)
    nrewrite > (nextblock_store … STORE1);
    //
##| (* range *)
    /2/
##| #b1;#delta1;#INJb1;
    nrewrite > (low_bound_store … STORE b1);
    nrewrite > (high_bound_store … STORE b1);
    napply ms_range_2;//;
##] nqed.

nlemma store_outside_shift:
  ∀f,chunk,m1,b,ofs,m2,v,m2',delta.
  mem_shift f m1 m2 →
  f b = Some ? delta →
  high_bound m1 b + delta ≤ ofs
  ∨ ofs + size_chunk chunk ≤ low_bound m1 b + delta →
  store chunk m2 b ofs v = Some ? m2' →
  mem_shift f m1 m2'.
#f;#chunk;#m1;#b;#ofs;#m2;#v;#m2';#delta;
*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
#INJb;#Hbounds;#STORE;@;
##[ (* inj *)
    napply (store_outside_inj … STORE); //;
    #b';#d'; nwhd in ⊢ (??%? → ?); nlapply (refl ? (f b')); nelim (f b') in ⊢ (???% → %);
    ##[ #_; #e; nwhd in e:(??%?); ndestruct;
    ##| #d''; #ef; #e; nelim (grumpydestruct2 ?????? e); #eb; #ed;
        nrewrite > eb in ef ⊢ %; nrewrite > ed; nrewrite > INJb; #ed';
        nrewrite < (grumpydestruct1 ??? ed'); //
    ##]
##| (* samedomain *) nrewrite > (nextblock_store … STORE); //
##| (* domain *) //
##| (* range *) /2/
##| #b1;#delta1;#INJb1;
    nrewrite > (low_bound_store … STORE b1);
    nrewrite > (high_bound_store … STORE b1);
    napply ms_range_2;//;
##] nqed.

nlemma storev_shift:
  ∀f,chunk,m1,a1,v1,n1,m2,a2,v2.
  mem_shift f m1 m2 →
  storev chunk m1 a1 v1 = Some ? n1 →
  val_shift f a1 a2 →
  val_shift f v1 v2 →
  ∃n2.
    storev chunk m2 a2 v2 = Some ? n2 ∧ mem_shift f n1 n2.
#f;#chunk;#m1;#a1;#v1;#n1;#m2;#a2;#v2;
#Hmem_shift;#STOREV;#Hval_shift_a;#Hval_shift_v;
ninversion Hval_shift_a;
##[ ##1,2,4: #x;#H;nrewrite > H in STOREV;#H';nwhd in H':(??%?); napply False_ind; ndestruct; ##]
#b1;#ofs1;#b2;#ofs2;#delta;
nwhd in ⊢ (??%? → ?); nlapply (refl ? (f b1)); nelim (f b1) in ⊢ (???% → %);
##[#_; #e; nwhd in e:(??%?); ndestruct; ##]
#x; #INJb1; #e; nelim (grumpydestruct2 ?????? e); #eb;#ex;
nrewrite > ex in INJb1; #INJb1;
#OFS; #ea1;#ea2; nrewrite > ea1 in STOREV; #STOREV;
nlapply (store_within_shift … Hmem_shift STOREV INJb1 Hval_shift_v);
*; #n2; *; #A;#B;
@ n2; @; //;
nrewrite > OFS; nrewrite > eb in A;
nrewrite < (?:signed (add ofs1 (repr delta)) = signed ofs1 + delta);
##[ #H; napply H; (* XXX /2/ *)
##| napply (address_shift … chunk … Hmem_shift ? INJb1);
    napply (store_valid_access_3 … STOREV);
##]
nqed.

(* Relation between shifts and [free]. *)

nlemma free_shift:
  ∀f,m1,m2,b.
  mem_shift f m1 m2 →
  mem_shift f (free m1 b) (free m2 b).
#f;#m1;#m2;#b;
*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2; @;
##[ (* inj *)
    napply free_right_inj; ##[ napply free_left_inj; //
    ##| #b1;#delta; #chunk;#ofs; nwhd in ⊢ (??%? → ?);
        nlapply (refl ? (f b1)); nelim (f b1) in ⊢ (???% → %);
        ##[ #_; #e; nwhd in e:(??%?); ndestruct;
        ##| #delta'; #INJb1; #e; nwhd in e:(??%?); ndestruct;
            napply valid_access_free_2
        ##]
    ##]
##| (* samedomain *) nwhd in ⊢ (??%%); //
##| (* domain *) nrewrite > (?:nextblock (free m1 b) = nextblock m1); //
##| (* range *) /2/
##| #b';#delta;#INJb'; ncases (decidable_eq_Z b' b); #eb;
    ##[ nrewrite > eb;
        nrewrite > (low_bound_free_same ??); nrewrite > (high_bound_free_same ??);
        (* arith *) napply daemon
    ##| nrewrite > (low_bound_free …); //; nrewrite > (high_bound_free …); /2/;
    ##]
##] nqed.

(* Relation between shifts and allocation. *)

ndefinition shift_incr : memshift → memshift → Prop ≝ λf1,f2: memshift.
  ∀b. f1 b = f2 b ∨ f1 b = None ?.

nremark shift_incr_inject_incr:
  ∀f1,f2.
  shift_incr f1 f2 → inject_incr (meminj_of_shift f1) (meminj_of_shift f2).
#f1;#f2;#Hshift; nwhd in ⊢ (?%%); nwhd; #b;
nelim (Hshift b); #INJ; nrewrite > INJ; /2/;
nqed.

nlemma val_shift_incr:
  ∀f1,f2,v1,v2.
  shift_incr f1 f2 → val_shift f1 v1 v2 → val_shift f2 v1 v2.
#f1;#f2;#v1;#v2;#Hshift_incr; nwhd in ⊢ (% → %);
napply val_inject_incr;
napply shift_incr_inject_incr; //;
nqed.

(* *
Remark mem_inj_incr:
  ∀f1,f2,m1,m2.
  inject_incr f1 f2 → mem_inj val_inject f1 m1 m2 → mem_inj val_inject f2 m1 m2.
Proof.
  intros; red; intros. 
  destruct (H b1). rewrite <- H3 in H1.
  exploit H0; eauto. intros [v2 [A B]]. 
  exists v2; split. auto. apply val_inject_incr with f1; auto.
  congruence.
***)

nlemma alloc_shift:
  ∀f,m1,m2,lo1,hi1,m1',b,delta,lo2,hi2.
  mem_shift f m1 m2 →
  alloc m1 lo1 hi1 = 〈m1', b〉 →
  lo2 ≤ lo1 + delta → hi1 + delta ≤ hi2 →
  min_signed ≤ delta ∧ delta ≤ max_signed →
  min_signed ≤ lo2 → hi2 ≤ max_signed →
  inj_offset_aligned delta (hi1-lo1) →
  ∃f'. ∃m2'.
     alloc m2 lo2 hi2 = 〈m2', b〉
  ∧ mem_shift f' m1' m2'
  ∧ shift_incr f f'
  ∧ f' b = Some ? delta.
#f;#m1;#m2;#lo1;#hi1;#m1';#b;#delta;#lo2;#hi2;
*;#ms_inj;#ms_samedomain;#ms_domain;#ms_range_1;#ms_range_2;
#ALLOC;#Hlo_delta;#Hhi_delta;#Hdelta_range;#Hlo_range;#Hhi_range;#Hinj_aligned;
nlapply (refl ? (alloc m2 lo2 hi2)); nelim (alloc m2 lo2 hi2) in ⊢ (???% → %);
#m2';#b';#ALLOC2;
ncut (b' = b);
##[ nrewrite > (alloc_result … ALLOC); nrewrite > (alloc_result … ALLOC2); // ##]
#eb; nrewrite > eb;
ncut (f b = None ?);
##[ nlapply (ms_domain b); nrewrite > (alloc_result … ALLOC);
    nelim (f (nextblock m1)); //;
    #z; (* arith *) napply daemon
##]
#FB;
nletin f' ≝ (λb':block. if eqZb b' b then Some ? delta else f b');
ncut (shift_incr f f');
##[ nwhd; #b0; nwhd in ⊢ (?(???%)?);
    napply eqZb_elim; /2/; ##]
#Hshift_incr;
ncut (f' b = Some ? delta);
##[ nwhd in ⊢ (??%?); nrewrite > (eqZb_z_z …); // ##] #efb';
@ f'; @ m2'; @; //; @; //; @; //; @;
##[ (* inj *)
    ncut (mem_inj val_inject (meminj_of_shift f') m1 m2);
    ##[ nwhd; #chunk;#b1;#ofs;#v1;#b2;#delta2; #MINJf'; #LOAD;
        ncut (meminj_of_shift f b1 = Some ? 〈b2, delta2〉);
        ##[ nrewrite < MINJf'; nwhd in ⊢ (???(?%?)); nwhd in ⊢ (??%%);
            napply eqZb_elim; //; #eb;
            nrewrite > eb;
            ncut (valid_block m1 b);
            ##[ napply valid_access_valid_block;
              ##[ ##3: napply load_valid_access; // ##]
            ##]
            ncut (¬valid_block m1 b); ##[ /2/ ##]
            #H;#H'; napply False_ind; napply (absurd ? H' H)
        ##] #MINJf;
        nlapply (ms_inj … MINJf LOAD); *; #v2; *; #A; #B;
        @ v2; @; //;
        napply (val_inject_incr … B);
        napply shift_incr_inject_incr; //
    ##] #Hmem_inj;
    napply (alloc_parallel_inj … delta Hmem_inj ALLOC ALLOC2 ?); /2/;
    nwhd in ⊢ (??%?); nrewrite > efb'; /2/;
##| (* samedomain *)
    nrewrite > (nextblock_alloc … ALLOC);
    nrewrite > (nextblock_alloc … ALLOC2);
    //;
##| (* domain *)
    #b0; (* FIXME: unfold *) nrewrite > (refl ? (f' b0):f' b0 = if eqZb b0 b then Some ? delta else f b0);
    nrewrite > (nextblock_alloc … ALLOC);
    nrewrite > (alloc_result … ALLOC);
    napply eqZb_elim; #eb0;
    ##[ nrewrite > eb0; (* arith *) napply daemon
    ##| nlapply (ms_domain b0); nelim (f b0); 
        (* arith *) napply daemon
    ##]
##| (* range *)
    #b0;#delta0; nwhd in ⊢ (??%? → ?);
    napply eqZb_elim;
    ##[ #_; #e; nrewrite < (grumpydestruct1 ??? e); //
    ##| #neb; #e; napply (ms_range_1 … b0); napply e;
    ##] 
##| #b0;#delta0; nwhd in ⊢ (??%? → ?);
    nrewrite > (low_bound_alloc … ALLOC2 ?);
    nrewrite > (high_bound_alloc … ALLOC2 ?);
    napply eqZb_elim; #eb0; nrewrite > eb;
    ##[ nrewrite > eb0; #ed; nrewrite < (grumpydestruct1 ??? ed);
        nrewrite > (eqZb_z_z ?); /3/;
    ##| #edelta0; nrewrite > (eqZb_false … eb0);
        napply ms_range_2; nwhd in edelta0:(??%?); //; 
    ##]
##]
nqed.
*)
(* ** Relation between signed and unsigned loads and stores *)

(* Target processors do not distinguish between signed and unsigned
  stores of 8- and 16-bit quantities.  We show these are equivalent. *)

(* Signed 8- and 16-bit stores can be performed like unsigned stores. *)

nremark in_bounds_equiv:
  ∀chunk1,chunk2,m,psp,b,ofs.∀A:Type.∀a1,a2: A.
  size_chunk chunk1 = size_chunk chunk2 →
  (match in_bounds m chunk1 psp b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]) =
  (match in_bounds m chunk2 psp b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]).
#chunk1;#chunk2;#m;#psp b ofs;#A;#a1;#a2;#Hsize;
nelim (in_bounds m chunk1 psp b ofs);
##[ #H; nwhd in ⊢ (??%?); nrewrite > (in_bounds_true … A a1 a2 ?); //;
    napply valid_access_compat; //;
##| #H; nwhd in ⊢ (??%?); nelim (in_bounds m chunk2 psp b ofs); //;
    #H'; napply False_ind; napply (absurd ?? H);
    napply valid_access_compat; //;
##] nqed. 

nlemma storev_8_signed_unsigned:
  ∀m,a,v.
  storev Mint8signed m a v = storev Mint8unsigned m a v.
#m;#a;#v; nwhd in ⊢ (??%%); nelim a; //;
#psp b ofs; nwhd in ⊢ (??%%);
nrewrite > (in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???); //;
nqed.

nlemma storev_16_signed_unsigned:
  ∀m,a,v.
  storev Mint16signed m a v = storev Mint16unsigned m a v.
#m;#a;#v; nwhd in ⊢ (??%%); nelim a; //;
#psp b ofs; nwhd in ⊢ (??%%);
nrewrite > (in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???); //;
nqed.

(* Likewise, some target processors (e.g. the PowerPC) do not have
  a ``load 8-bit signed integer'' instruction.  
  We show that it can be synthesized as a ``load 8-bit unsigned integer''
  followed by a sign extension. *)

nlemma loadv_8_signed_unsigned:
  ∀m,a.
  loadv Mint8signed m a = option_map ?? (sign_ext 8) (loadv Mint8unsigned m a).
#m;#a; nwhd in ⊢ (??%(????(%))); nelim a; //;
#psp b ofs; nwhd in ⊢ (??%(????%));
nrewrite > (in_bounds_equiv Mint8signed Mint8unsigned … (option val) ???); //;
nelim (in_bounds m Mint8unsigned psp b (signed ofs)); /2/;
#H; nwhd in ⊢ (??%%);
nelim (getN 0 (signed ofs) (contents (blocks m b))); 
##[ ##1,3: //;
##| #i; nwhd in ⊢ (??(??%)(??%));
    nrewrite > (sign_ext_zero_ext ?? i); ##[ napply refl; (* XXX: // ? *)
    ##| (* arith *) napply daemon;
    ##]
##| #sp; ncases sp; //; 
##]
nqed.