source: src/common/Mem.ma @ 1878

include "joint/BEMem.ma".
include "common/FrontEndVal.ma".

definition mem ≝ bemem.

let rec loadn (m:bemem) (ptr:pointer) (n:nat) on n : option (list beval) ≝
match n with
[ O ⇒ Some ? ([ ])
| S n' ⇒
  match beloadv m ptr with
  [ None ⇒ None ?
  | Some v ⇒ match loadn m (shift_pointer 2 ptr (bitvector_of_nat … 1)) n' with
             [ None ⇒ None ? 
             | Some vs ⇒ Some ? (v::vs) ]
  ]
].

definition load : typ → mem → pointer → option val ≝
λt,m,ptr.
  match loadn m ptr (typesize t) with
  [ None ⇒ None ?
  | Some vs ⇒ Some ? (be_to_fe_value t vs)
  ].

let rec loadv (t:typ) (m:bemem) (addr:val) on addr : option val ≝
match addr with
[ Vptr ptr ⇒ load t m ptr
| _ ⇒ None ?
].

let rec storen (m:bemem) (ptr:pointer) (vs:list beval) on vs : option bemem ≝
match vs with
[ nil ⇒ Some ? m
| cons v tl ⇒
  match bestorev m ptr v with
  [ None ⇒ None ?
  | Some m' ⇒ storen m' (shift_pointer 2 ptr (bitvector_of_nat … 1)) tl
  ]
].

definition store : typ → bemem → pointer → val → option bemem ≝
λt,m,ptr,v. storen m ptr (fe_to_be_values t v).

definition storev : typ → bemem → val → val → option bemem ≝
λt,m,addr,v.
  match addr with
  [ Vptr ptr ⇒ store t m ptr v
  | _ ⇒ None ? ].

(* Only used by Clight semantics for pointer comparisons.  So in contrast to
   CompCert, we allow a pointer-to-one-off-the-end. *)

definition valid_pointer : mem → pointer → bool ≝
λm,ptr. Zltb (block_id (pblock ptr)) (nextblock ? m) ∧
  Zleb (low_bound ? m (pblock ptr)) (offv (poff ptr)) ∧
  Zleb (offv (poff ptr)) (high_bound ? m (pblock ptr)).


(*
(* *********************************************************************)
(*                                                                     *)
(*              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/lists/list.ma".*)
(*include "Plogic/equality.ma".*)

(*include "Coqlib.ma".*)
include "common/Values.ma".
(*include "AST.ma".*)
include "utilities/binary/division.ma".

definition 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 ].
    
lemma update_s:
  ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z -> A.
  update … x v f x = v.
#A #x #v #f whd in ⊢ (??%?);
>(eqZb_z_z …) //;
qed.

lemma 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 whd in ⊢ (??%?);
@eqZb_elim //;
#H2 cases H;#H3 elim (H3 ?);//;
qed.

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

definition update_block : ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block → A. block → A ≝ 
  λA,x,v,f.
    λy.match eq_block y x with [ true ⇒ v | false ⇒ f y ].
    
lemma update_block_s:
  ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A.
  update_block … x v f x = v.
#A * * #ix #v #f whd in ⊢ (??%?);
>eq_block_b_b //
qed.

lemma update_block_o:
  ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A. ∀y: block.
  x ≠ y → update_block … x v f y = f y.
#A #x #v #f #y #H whd in ⊢ (??%?);
@eq_block_elim //;
#H2 cases H;#H3 elim (H3 ?);//;
qed.

(* FIXME: workaround for lack of nunfold *)
lemma unfold_update_block : ∀A,x,v,f,y.
  update_block A x v f y = match eq_block y x with [ true ⇒ v | false ⇒ f y ].
//; qed.


(* * 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. *)

inductive 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 *)

definition 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.  *)

record block_contents : Type[0] ≝ {
  low: Z;
  high: Z;
  contents: contentmap
}.

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

record mem : Type[0] ≝ {
  blocks: block -> block_contents;
  nextblock: Z;
  nextblock_pos: OZ < nextblock
}.

(* * Operations on memory stores *)

definition pred_size_chunk : typ → nat ≝ 
  λchunk. match chunk with
  [ ASTint sz _ ⇒ pred (size_intsize sz)
  | ASTptr r ⇒ pred (size_pointer r)
  | ASTfloat sz ⇒ pred (size_floatsize sz)
  ].
  
lemma size_chunk_pred:
  ∀chunk. typesize chunk = 1 + pred_size_chunk chunk.
* //
qed.


(* 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. *)

definition align_chunk : typ → Z ≝ 
  λchunk.match chunk return λ_.Z with
  [ ASTint _ _ ⇒ 1
  | ASTptr _ ⇒ 1
  | ASTfloat _ ⇒ 1
  ].

lemma align_chunk_pos:
  ∀chunk. OZ < align_chunk chunk.
#chunk cases chunk;normalize;//;
qed.

lemma align_size_chunk_divides:
  ∀chunk. (align_chunk chunk ∣ typesize chunk).
#chunk cases chunk * [ 1,2,3: * ] normalize /3 by witness/
qed.

lemma align_chunk_compat:
  ∀chunk1,chunk2.
    typesize chunk1 = typesize chunk2 → 
      align_chunk chunk1 = align_chunk chunk2.
* * [ 1,2,3: * ]
* * [ 1,2,3,12,13,14,23,24,25: * ]
normalize //
qed.

(* The initial store. *)

definition oneZ ≝ pos one.

lemma one_pos: OZ < oneZ.
//;
qed.

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

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

definition nullptr: block ≝ mk_block Any 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. *)

lemma succ_nextblock_pos:
  ∀m. OZ < Zsucc (nextblock m). (* XXX *)
#m lapply (nextblock_pos m);normalize;
cases (nextblock m);//;
#n cases n;//;
qed.

definition alloc : mem → Z → Z → region → mem × block ≝
  λm,lo,hi,r.
  let b ≝ mk_block r (nextblock m) in
  〈mk_mem 
    (update_block … b
      (empty_block lo hi)
      (blocks m))
    (Zsucc (nextblock m))
    (succ_nextblock_pos m),
    b〉.

(* 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. *)

definition free ≝
  λm,b.mk_mem (update_block … b 
                (empty_block OZ OZ)
                (blocks m))
        (nextblock m)
        (nextblock_pos m).

(* Freeing of a list of blocks. *)

definition free_list ≝ 
  λm,l.foldr ?? (λb,m.free m b) m l.
(* XXX hack for lack of reduction with restricted unfolding *)
lemma unfold_free_list : ∀m,h,t. free_list m (h::t) = free (free_list m t) h.
normalize; //; qed.

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

definition low_bound : mem → block → Z ≝
  λm,b.low (blocks m b).
definition high_bound : mem → block → Z ≝ 
  λm,b.high (blocks m b).
definition block_region: mem → block → region ≝
  λm,b.block_region b. (* TODO: should I keep the mem argument for uniformity, or get rid of it? *)

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

(* TODO: should this check for region? *)
definition valid_block : mem → block → Prop ≝ 
  λm,b.block_id b < nextblock m.

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

(* 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].
 *)

let 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?? *)
definition eq_nat: ∀p,q: nat. p=q ∨ p≠q.
@decidable_eq_nat (* // not working, why *)
qed.

definition 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 ].

let 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) ].

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

(* Nonessential properties that may require arithmetic
(* XXX: the daemons *)
axiom daemon : ∀A:Prop.A.

lemma 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 elim 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
   (* whd : doesn't work either *)
   cut (check_cont (S n1) p m = match m p with [ Undef ⇒ false | Datum _ _ ⇒ false | Cont ⇒ check_cont n1 (Zplus p oneZ) m ])
   [@
   |#Heq >Heq lapply (refl ? (m p));
      cases (m p) in ⊢ (???% → %);
      [#Heq1 %
           [napply p
           |% [napply daemon
                 |@nmk #Hfalse >Hfalse in Heq1 #Heq1
                    destruct ]
           ]
      |#n2 #v #Heq1 %
           [napply p
           | % [ (* refl≤ and  p < p + S n1 *)napply daemon
                  |@nmk #Hfalse >Hfalse in Heq1 #Heq1
                     destruct ]
           ]
      |#Heq1 lapply (IH m (p + 1));
         lapply (refl ? (check_cont n1 (p + 1) m));
         (* napply daemon *)
         cases (check_cont n1 (p + 1) m) in ⊢ (???% → %);
         whd in ⊢ (? → % → %);
         [#H #H1 #q #Hl #Hr
            cut (p = q ∨ p + 1 ≤ q)
            [(* Hl *) napply daemon
            |*;
               [//
               |#Hl2 @H1 //;(*Hr*)napply daemon ] ]
         |#H #H1 cases H1;#x *;*;#Hl #Hr #Hx
            %{ x} @
            [@
               [(*Hl*) napply daemon
               |(*Hr*) napply daemon ]
            |//]]]]
qed.

lemma 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 lapply (check_cont_spec n m p);
cases (check_cont n p m);//;
whd in ⊢ (%→?);*;
#q *;*;#Hl #Hr #Hfalse cases Hfalse;#H1 elim (H1 ?);@H //;
qed.

lemma 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 lapply (check_cont_spec n m p);
cases (check_cont n p m);//;
whd in ⊢ (%→?);#H
#Hl #Hr #Hfalse cases Hfalse;#H1 elim (H1 ?);@H //;
qed.

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

lemma set_cont_outside:
  ∀n:nat.∀p:Z.∀m.∀q:Z.
  q < p ∨ p + n ≤ q → 
  (set_cont n p m) q = m q.
#n elim n
[#p #m #q #_ @
|#n1 #IH #p #m #q
   #H whd in ⊢ (??%?);>(? : eqZb q p = false)
   [whd in ⊢ (??%?);@IH cases H;
      [#Hl % napply daemon
      |#Hr %{2} napply daemon]
   |(*H*)napply daemon ]
]
qed.

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

lemma 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));
lapply (refl ? (check_cont n2 (p2+oneZ) m));
cases (check_cont n2 (p2+oneZ) m) in ⊢ (???% → %);
#H1 whd in ⊢ (% →?); whd in ⊢ (?→(???%)); >H1
[#H2
   nchange in ⊢ (??(???%)?) with (update ????);
   whd in ⊢(??%%);>(check_cont_true …)
   [ >(check_cont_true … H2)
       >(update_o content ?????)
       [ >(set_cont_outside ?????) //; (* arith *) napply daemon
       | (* arith *) napply daemon
       ]
   | #q #Hl #Hh >(update_o content ?????)
       [ >(set_cont_outside ?????) /2/; (* arith *) napply daemon
       | (* arith *) napply daemon
       ]
   ]
| *; #q *;#A #B
   nchange in ⊢ (??(???%)?) with (update ????);
   whd in ⊢(??%%);
   >(check_cont_false n2 (update ? p1 (Datum n1 v) (set_cont n1 (p1 + 1) m)) (p2 + 1) q …)
   [ >(update_o content ?????)
       [ >(set_cont_outside ?????) //; (* arith *) napply daemon
       | napply daemon
       ]
   | >(update_o content ?????)
       [ >(set_cont_outside ?????) //; (* arith *) napply daemon
       | napply daemon
       ]
   | napply daemon
   | napply daemon
   ]
] qed.

lemma 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 ????);
whd in ⊢(??%?);>(update_o content ?????)
[lapply (Z_compare_to_Prop p2 p1);
   lapply (refl ? (Z_compare p2 p1));
   cases (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. *)
     >(check_cont_false …)
     [cases (set_cont n1 (p1+oneZ) m p2)
        [1,3:@
        |#n3 #v1 whd in ⊢ (??%?);
           cases (eqb n2 n3);@ ]
     |>(update_s content …) @nmk
        #Hfalse destruct
     |(*H2*) napply daemon
     |(*H4*) napply daemon
     |##skip ]
  |whd in ⊢ (% → ?);#H4 elim H;#H5 elim (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]. *)
     >(set_cont_inside …)
     [@
     |(*H1*)napply daemon
     |(*H4*)napply daemon]
  ]
|//]
qed.

lemma 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 ????);
whd in ⊢(??%?);>(update_s content …)
whd in ⊢(??%?);>(not_eq_to_eqb_false … (sym_neq … H)) //;
qed.

lemma 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
lapply (eqZb_to_Prop p1 p2); cases (eqZb p1 p2); #Hp
[>Hp
   @(eqb_elim n1 n2) #Hn
   [>Hn % % //;
   |%{2} /2/]
|lapply (Z_compare_to_Prop (p1 + n1) p2);
   cases  (Z_compare (p1 + n1) p2);#Hcmp
   [% %{2} @getN_setN_other /2/
   |lapply (Z_compare_to_Prop (p2 + n2) p1);
      cases  (Z_compare (p2 + n2) p1);#Hcmp2
      [% %{2} @getN_setN_other /2/
      |%{2} @getN_setN_overlap
         [//
         |*:(* arith *) napply daemon]
      |%{2} @getN_setN_overlap
         [//
         |*:(* arith *) napply daemon]
      ]
   |lapply (Z_compare_to_Prop (p2 + n2) p1);
      cases  (Z_compare (p2 + n2) p1);#Hcmp2
      [% %{2} @getN_setN_other /2/
      |%{2} @getN_setN_overlap
         [//
         |*:(* arith *) napply daemon]
      |%{2} @getN_setN_overlap
         [//
         |*:(* arith *) napply daemon]
      ]
   ]
]
qed.

lemma getN_init:
  ∀n,p.
  getN n p (λ_.Undef) = Vundef.
#n #p //;
qed.
*)

(* [valid_access m chunk r 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 representation (i.e., region) [r] is compatible with the class of [b].
*)

inductive valid_access (m: mem) (chunk: typ) (r: region) (b: block) (ofs: Z) 
            : Prop ≝ 
  | valid_access_intro:
      valid_block m b → 
      low_bound m b ≤ ofs → 
      ofs + typesize chunk ≤ high_bound m b → 
      (align_chunk chunk ∣ ofs) → 
      pointer_compat b r →
      valid_access m chunk r 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 *)
let rec in_bounds 
  (m:mem) (chunk:typ) (r:region) (b:block) (ofs:Z) on b :  
    Sum (valid_access m chunk r b ofs) (Not (valid_access m chunk r b ofs)) ≝ ?.
cases b #br #bi
@(Zltb_elim_Type0 bi (nextblock m)) #Hnext
[ @(Zleb_elim_Type0 (low_bound m (mk_block br bi)) ofs) #Hlo
    [ @(Zleb_elim_Type0 (ofs + typesize chunk) (high_bound m (mk_block br bi))) #Hhi
        [ elim (dec_dividesZ (align_chunk chunk) ofs); #Hal
          [ cases (pointer_compat_dec (mk_block br bi) r); #Hcl
            [ %1 % // @Hnext ]
          ]
        ]
    ]
]
%2 @nmk *; #Hval #Hlo' #Hhi' #Hal' #Hcl'
[ @(absurd ? Hcl' Hcl) | @(absurd ? Hal' Hal) | @(absurd ? Hhi' Hhi)
| @(absurd ? Hlo' Hlo) | @(absurd ? Hval Hnext) ]
qed.

lemma in_bounds_true:
  ∀m,chunk,r,b,ofs. ∀A: Type[0]. ∀a1,a2: A.
  valid_access m chunk r b ofs ->
  (match in_bounds m chunk r b ofs with
   [ inl _ ⇒ a1 | inr _ ⇒ a2 ]) = a1.
#m #chunk #r #b #ofs #A #a1 #a2 #H
cases (in_bounds m chunk r b ofs);normalize;#H1
[//
|elim (?:False); @(absurd ? H H1)]
qed.

(* [valid_pointer] holds if the given block address is valid (and can be
  represented in a pointer with the region [r]) and the
  given offset falls within the bounds of the corresponding block. *)

definition valid_pointer : mem → pointer → bool ≝
λm,ptr. Zltb (block_id (pblock ptr)) (nextblock m) ∧
  Zleb (low_bound m (pblock ptr)) (offv (poff ptr)) ∧
  Zltb (offv (poff ptr)) (high_bound m (pblock ptr)).

(* [load chunk m r 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 or the address cannot be represented
  by a pointer with region [r]. *)

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

lemma load_inv:
  ∀chunk,m,r,b,ofs,v.
  load chunk m r b ofs = Some ? v →
  valid_access m chunk r b ofs ∧
  v = load_result chunk
           (getN (pred_size_chunk chunk) ofs (contents (blocks m b))).
#chunk #m #r #b #ofs #v whd in ⊢ (??%? → ?);
cases (in_bounds m chunk r b ofs); #Haccess whd in ⊢ ((??%?) → ?); #H
[ % //; destruct; //;
| destruct
]
qed.

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

let rec loadv (chunk:typ) (m:mem) (addr:val) on addr : option val ≝ 
  match addr with
  [ Vptr ptr ⇒ load chunk m (ptype ptr) (pblock ptr) (offv (poff ptr))
  | _ ⇒ None ? ].

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

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

(* [store chunk m r 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 or the address cannot be represented
  by a pointer with region [r]. *)

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

lemma store_inv:
  ∀chunk,m,r,b,ofs,v,m'.
  store chunk m r b ofs v = Some ? m' → 
  valid_access m chunk r b ofs ∧
  m' = unchecked_store chunk m b ofs v.
#chunk #m #r #b #ofs #v #m' whd in ⊢ (??%? → ?);
(*9*)
cases (in_bounds m chunk r b ofs);#Hv whd in ⊢(??%? → ?);#Heq
[% [//|destruct;//]
|destruct]
qed.

(* [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. *)

definition storev : typ → mem → val → val → option mem ≝
λchunk,m,addr,v.
  match addr with
  [ Vptr ptr ⇒ store chunk m (ptype ptr) (pblock ptr) (offv (poff ptr)) v
  | _ ⇒ None ? ].

(* * Properties of the memory operations *)

(* ** Properties related to block validity *)

lemma valid_not_valid_diff:
  ∀m,b,b'. valid_block m b →  ¬(valid_block m b') → b ≠ b'.
#m #b #b' #H #H' @nmk #e >e in H; #H
@(absurd ? H H')
qed.

lemma valid_access_valid_block:
  ∀m,chunk,r,b,ofs. valid_access m chunk r b ofs → valid_block m b.
#m #chunk #r #b #ofs #H
elim H;//;
qed.

lemma valid_access_aligned:
  ∀m,chunk,r,b,ofs.
  valid_access m chunk r b ofs → (align_chunk chunk ∣ ofs).
#m #chunk #r #b #ofs #H
elim H;//;
qed.

lemma valid_access_compat:
  ∀m,chunk1,chunk2,r,b,ofs.
  typesize chunk1 = typesize chunk2 →
  valid_access m chunk1 r b ofs →
  valid_access m chunk2 r b ofs.
#m #chunk #chunk2 #r #b #ofs #H1 #H2
elim H2;#H3 #H4 #H5 #H6 #H7
>H1 in H5; #H5
% //;
<(align_chunk_compat … H1) //;
qed.

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

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

theorem valid_access_load:
  ∀m,chunk,r,b,ofs.
  valid_access m chunk r b ofs → 
  ∃v. load chunk m r b ofs = Some ? v.
#m #chunk #r #b #ofs #H %
[2:whd in ⊢ (??%?);@in_bounds_true //;
|skip]
qed.

theorem load_valid_access:
  ∀m,chunk,r,b,ofs,v.
  load chunk m r b ofs = Some ? v →
  valid_access m chunk r b ofs.
#m #chunk #r #b #ofs #v #H
cases (load_inv … H);//;
qed.

(* Hint Resolve load_valid_access valid_access_load.*)

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

lemma valid_access_store:
  ∀m1,chunk,r,b,ofs,v.
  valid_access m1 chunk r b ofs →
  ∃m2. store chunk m1 r b ofs v = Some ? m2.
#m1 #chunk #r #b #ofs #v #H
%
[2:@in_bounds_true //
|skip]
qed.

(* section STORE *)

lemma low_bound_store:
  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
  ∀b'.low_bound m2 b' = low_bound m1 b'.
#chunk #m1 #r #b #ofs #v #m2 #STORE
#b' cases (store_inv … STORE)
#H1 #H2 >H2
whd in ⊢ (??(?%?)?); whd in ⊢ (??%?);
whd in ⊢ (??(?%)?); @eq_block_elim #E
normalize //
qed.

lemma nextblock_store :
  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
  nextblock m2 = nextblock m1.
#chunk #m1 #r #b #ofs #v #m2 #STORE
cases (store_inv … STORE);
#Hvalid #Heq
>Heq %
qed.

lemma high_bound_store:
  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
  ∀b'. high_bound m2 b' = high_bound m1 b'.
#chunk #m1 #r #b #ofs #v #m2 #STORE
#b' cases (store_inv … STORE);
#Hvalid #H
>H
whd in ⊢ (??(?%?)?);whd in ⊢ (??%?);
whd in ⊢ (??(?%)?); @eq_block_elim #E
normalize;//;
qed.

lemma region_store:
  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
  ∀b'. block_region m2 b' = block_region m1 b'.
#chunk #m1 #r #b #ofs #v #m2 #STORE
* #r #b' //
qed.

lemma store_valid_block_1:
  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
  ∀b'. valid_block m1 b' → valid_block m2 b'.
#chunk #m1 #r #b #ofs #v #m2 #STORE
#b' whd in ⊢ (% → %);#Hv
>(nextblock_store … STORE) //;
qed.

lemma store_valid_block_2:
  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
  ∀b'. valid_block m2 b' → valid_block m1 b'.
#chunk #m1 #r #b #ofs #v #m2 #STORE
#b' whd in ⊢ (%→%);
>(nextblock_store … STORE) //;
qed.

(*Hint Resolve store_valid_block_1 store_valid_block_2: mem.*)

lemma store_valid_access_1:
  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
  ∀chunk',r',b',ofs'.
  valid_access m1 chunk' r' b' ofs' → valid_access m2 chunk' r' b' ofs'.
#chunk #m1 #r #b #ofs #v #m2 #STORE
#chunk' #r' #b' #ofs'
* as Hv
#Hvb #Hl #Hr #Halign #Hptr
% //;
[@(store_valid_block_1 … STORE) //
|>(low_bound_store … STORE …) //
|>(high_bound_store … STORE …) //
] qed.

lemma store_valid_access_2:
  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
  ∀chunk',r',b',ofs'.
  valid_access m2 chunk' r' b' ofs' → valid_access m1 chunk' r' b' ofs'.
#chunk #m1 #r #b #ofs #v #m2 #STORE
#chunk' #r' #b' #ofs'
* as Hv
#Hvb #Hl #Hr #Halign #Hcompat
% //;
[@(store_valid_block_2 … STORE) //
|<(low_bound_store … STORE …) //
|<(high_bound_store … STORE …) //
] qed.

lemma store_valid_access_3:
  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
  valid_access m1 chunk r b ofs.
#chunk #m1 #r #b #ofs #v #m2 #STORE
cases (store_inv … STORE);//;
qed.

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

lemma load_compat_pointer:
  ∀chunk,m,r,r',b,ofs,v.
  pointer_compat b r' →
  load chunk m r b ofs = Some ? v →
  load chunk m r' b ofs = Some ? v.
#chunk #m #r #r' #b #ofs #v #Hcompat #LOAD
lapply (load_valid_access … LOAD); #Hvalid
cut (valid_access m chunk r' b ofs);
[ % elim Hvalid; //;
| #Hvalid'
    <LOAD whd in ⊢ (??%%);
    >(in_bounds_true … (option val) ?? Hvalid)
    >(in_bounds_true … (option val) ?? Hvalid')
    //
] qed.

(* Nonessential properties that may require arithmetic
theorem load_store_similar:
  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
  ∀chunk'.
  size_chunk chunk' = size_chunk chunk →
  load chunk' m2 r b ofs = Some ? (load_result chunk' v).
#chunk #m1 #r #b #ofs #v #m2 #STORE
#chunk' #Hsize cases (store_inv … STORE);
#Hv #Heq
whd in ⊢ (??%?);
nrewrite > (in_bounds_true m2 chunk' r b ofs ? (Some ? (load_result chunk' (getN (pred_size_chunk chunk') ofs (contents (blocks m2 b))))) 
               (None ?) ?);
[>Heq
   whd in ⊢ (??(??(? ? (? ? ? (? (? % ?)))))?);
   >(update_s ? b ? (blocks m1)) (* XXX  too many metas for my taste *)
   >(? : pred_size_chunk chunk = pred_size_chunk chunk')
   [//;
   |>(size_chunk_pred …) in Hsize #Hsize
      >(size_chunk_pred …) in Hsize #Hsize
      @injective_Z_of_nat @(injective_Zplus_r 1) //;]
|@(store_valid_access_1 … STORE)
   cases Hv;#H1 #H2 #H3 #H4 #H5 % //;
   >(align_chunk_compat … Hsize) //]
qed.

theorem load_store_same:
  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
  load chunk m2 r b ofs = Some ? (load_result chunk v).
#chunk #m1 #r #b #ofs #v #m2 #STORE
@load_store_similar //;
qed.
        
theorem load_store_other:
  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
  ∀chunk',r',b',ofs'.
  b' ≠ b
  ∨ ofs' + size_chunk chunk' ≤  ofs
  ∨ ofs + size_chunk chunk ≤ ofs' → 
  load chunk' m2 r' b' ofs' = load chunk' m1 r' b' ofs'.
#chunk #m1 #r #b #ofs #v #m2 #STORE
#chunk' #r' #b' #ofs' #H
cases (store_inv … STORE);
#Hvalid #Heq whd in ⊢ (??%%);
cases (in_bounds m1 chunk' r' b' ofs');
[#Hvalid1 >(in_bounds_true m2 chunk' r' b' ofs' ? (Some ? ?) ??)
   [whd in ⊢ (???%); @(eq_f … (Some val)) @(eq_f … (load_result chunk'))
      >Heq whd in ⊢ (??(???(? (? % ?)))?);
                     whd in ⊢ (??(???(? %))?);
      lapply (eqZb_to_Prop b' b);cases (eqZb b' b);
      whd in ⊢ (% → ?);
      [#Heq1 >Heq1 whd in ⊢ (??(??? (? %))?);
         >(size_chunk_pred …) in H
         >(size_chunk_pred …) #H
         @(getN_setN_other …) cases H
         [*
            [#Hfalse elim Hfalse;#H1 elim (H1 Heq1)
            |#H1 %{2} (*H1*)napply daemon ]
         |#H1 % (*H1*)napply daemon ]
      |#Hneq @ ]
   |@(store_valid_access_1 … STORE) //]
|whd in ⊢ (? → ???%);lapply (in_bounds m2 chunk' r' b' ofs');
   #H1 cases H1;
   [#H2 #H3 lapply (store_valid_access_2 … STORE … H2);#Hfalse
      cases H3;#H4 elim (H4 Hfalse)
   |#H2 #H3 @]
]
qed.


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

theorem load_store_overlap':
  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
  ∀chunk',ofs'.
  valid_access m1 chunk' r b ofs' → 
  ofs' ≠ ofs → 
  ofs < ofs' + size_chunk chunk' → 
  ofs' < ofs + size_chunk chunk → 
  load chunk' m2 r b ofs' = Some ? Vundef.
#chunk #m1 #r #b #ofs #v #m2 #STORE
#chunk' #ofs' #Hvalid #H #H1 #H2
cut (∃v'.load chunk' m2 r b ofs' = Some ? v')
[@valid_access_load
   @(store_valid_access_1 … STORE) //
|#H3 cases H3;
   #x #Hx >Hx @(eq_f … (Some val))
   @(load_store_overlap … STORE … Hx) //;]
qed.

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

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

inductive load_store_cases 
      (chunk1: memory_chunk) (b1: block) (ofs1: Z)
      (chunk2: memory_chunk) (b2: block) (ofs2: Z) : Type[0] ≝
  | 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.

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

theorem load_store_characterization:
  ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 →
  ∀chunk',r',b',ofs'.
  valid_access m1 chunk' r' b' ofs' →
  load chunk' m2 r' 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 r' b' ofs'
    | lsc_overlap _ _ _ _ ⇒ Some ? Vundef
    | lsc_mismatch _ _ _ ⇒ Some ? Vundef ].
#chunk #m1 #r #b #ofs #v #m2 #STORE
#chunk' #r' #b' #ofs' #Hvalid
cut (∃v'. load chunk' m2 r' b' ofs' = Some ? v')
[@valid_access_load
   @(store_valid_access_1 … STORE … Hvalid)
|*;#x #Hx
   cases (load_store_classification chunk b ofs chunk' b' ofs')
   [#H1 #H2 #H3 whd in ⊢ (???%);<H1 <H2
      @(load_compat_pointer … r)
      [ >(region_store … STORE b)
          cases Hvalid; //;
      | @(load_store_similar … STORE) //;
      ]
   |#H1 @(load_store_other … STORE)
      cases H1
      [*
         [#H2 % % @sym_neq //
         |#H2 % %{2} //]
      |#H2 %{2} //]
   |#H1 #H2 #H3 #H4 lapply (load_compat_pointer … r … Hx);
     [ >(region_store … STORE b')
         >H1 elim (store_valid_access_3 … STORE); //
     | <H1 in ⊢ (% → ?) #Hx'
         <H1 in Hx #Hx >Hx
      @(eq_f … (Some val)) @(load_store_overlap … STORE … Hx') /2/;
     ]
   |#H1 #H2 #H3
       lapply (load_compat_pointer … r … Hx);
       [ >(region_store … STORE b')
           >H1 elim (store_valid_access_3 … STORE); //
       | <H1 in Hx ⊢ % <H2 #Hx #Hx'
           >Hx @(eq_f … (Some val))
           @(load_store_mismatch … STORE … Hx') /2/
       ]
   ]
           
]
qed.

(*lemma 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 destruct;*)

(*
Section ALLOC.

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

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

lemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y.
#A #B #x #y #e >e cases y;
#a #b normalize;#P #PH @PH %
qed.

lemma 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
whd in ALLOC:(??%%); destruct; //;
qed.

lemma 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
whd in ALLOC:(??%%); destruct; //;
qed.


lemma 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' >(unfold_valid_block m1 b')
>(unfold_valid_block m2 b')
>(nextblock_alloc … ALLOC)
(* arith *) @daemon
qed.

lemma 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
>(unfold_valid_block m1 b)
>(alloc_result … ALLOC)
(* arith *) @daemon
qed.

lemma 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
>(unfold_valid_block m2 b)
>(alloc_result … ALLOC)
>(nextblock_alloc … ALLOC)
(* arith *) @daemon
qed.

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

lemma 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'
>(unfold_valid_block m2 b')
>(unfold_valid_block m1 b')
>(nextblock_alloc … ALLOC) #H
>(alloc_result … ALLOC)
(* arith *) @daemon
qed.

lemma 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
whd in ALLOC:(??%%); destruct; #b'
>(unfold_update block_contents ????)
cases (eqZb b' (nextblock m1)); //;
qed.

lemma 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
>(low_bound_alloc … ALLOC b)
>(eqZb_z_z …)
//;
qed.

lemma 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' >(low_bound_alloc … ALLOC b')
@eqZb_elim #Hb
[ >Hb #bad @False_ind @(absurd ? bad)
    napply (fresh_block_alloc … ALLOC)
| //
] qed.

lemma 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
whd in ALLOC:(??%%); destruct; #b'
>(unfold_update block_contents ????)
cases (eqZb b' (nextblock m1)); //;
qed.

lemma 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
>(high_bound_alloc … ALLOC b)
>(eqZb_z_z …)
//;
qed.

lemma 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' >(high_bound_alloc … ALLOC b')
@eqZb_elim #Hb
[ >Hb #bad @False_ind @(absurd ? bad)
    napply (fresh_block_alloc … ALLOC)
| //
] qed.

lemma class_alloc:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀b'.block_region m2 b' = if eqZb b' b then bcl else block_region m1 b'.
#m1 #lo #hi #bcl #m2 #b #ALLOC
whd in ALLOC:(??%%); destruct; #b'
cases (eqZb b' (nextblock m1)); //;
qed.

lemma class_alloc_same:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  block_region m2 b = bcl.
#m1 #lo #hi #bcl #m2 #b #ALLOC
whd in ALLOC:(??%%); destruct;
>(eqZb_z_z ?) //;
qed.

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

lemma valid_access_alloc_other:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀chunk,r,b',ofs.
  valid_access m1 chunk r b' ofs →
  valid_access m2 chunk r b' ofs.
#m1 #lo #hi #bcl #m2 #b #ALLOC
#chunk #r #b' #ofs #H
cases H; #Hvalid #Hlow #Hhigh #Halign #Hcompat
%
[ @(valid_block_alloc … ALLOC) //
| >(low_bound_alloc_other … ALLOC b' Hvalid) //
| >(high_bound_alloc_other … ALLOC b' Hvalid) //
| //
| >(class_alloc_other … ALLOC b' Hvalid) //;
] qed.

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

(*
Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem.
*)

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

theorem load_alloc_unchanged:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo bcl hi = 〈m2,b〉 →
  ∀chunk,r,b',ofs.
  valid_block m1 b' →
  load chunk m2 r b' ofs = load chunk m1 r b' ofs.
#m1 #lo #hi #bcl #m2 #b #ALLOC
#chunk #r #b' #ofs #H whd in ⊢ (??%%);
cases (in_bounds m2 chunk r b' ofs); #H'
[ elim (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
  >(in_bounds_true ???? ??? H'') *) >(in_bounds_true … ? (option val) ?? H'')
      whd in ⊢ (??%?); (* XXX: if you do this at the point below the proof term is ill-typed. *)
      cut (b' ≠ b);
      [ @(valid_not_valid_diff … H) @(fresh_block_alloc … ALLOC)
      | whd in ALLOC:(??%%); destruct; 
          >(update_o block_contents ?????) /2/;
      ]
  | *;*;#A #B #C <A in ALLOC ⊢ % #ALLOC
      @False_ind @(absurd ? H) napply (fresh_block_alloc … ALLOC)
  ]
| cases (in_bounds m1 chunk r b' ofs); #H'' whd in ⊢ (??%%); //;
    @False_ind @(absurd ? ? H') @(valid_access_alloc_other … ALLOC) //
] qed.
  
theorem load_alloc_other:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀chunk,r,b',ofs,v.
  load chunk m1 r b' ofs = Some ? v →
  load chunk m2 r b' ofs = Some ? v.
#m1 #lo #hi #bcl #m2 #b #ALLOC
#chunk #r #b' #ofs #v #H
<H @(load_alloc_unchanged … ALLOC ???) cases (load_valid_access … H); //;
qed.

theorem load_alloc_same:
  ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 →
  ∀chunk,r,ofs,v.
  load chunk m2 r b ofs = Some ? v →
  v = Vundef.
#m1 #lo #hi #bcl #m2 #b #ALLOC
#chunk #r #ofs #v #H
elim (load_inv … H); #H0 #H1 >H1
 whd in ALLOC:(??%%); (* XXX destruct; ??? *) @(pairdisc_elim … ALLOC)
 whd in ⊢ (??%% → ?);#e0 <e0 in ⊢ (%→?)
 whd in ⊢ (??%% → ?);#e1
<e1 <e0 >(update_s ? ? (empty_block lo hi bcl) ?)
normalize; cases chunk; //;
qed.

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

(*
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.
*)

lemma valid_block_free_1:
  ∀m,bf,b. valid_block m b → valid_block (free m bf) b.
normalize;//;
qed.

lemma valid_block_free_2:
  ∀m,bf,b. valid_block (free m bf) b → valid_block m b.
normalize;//;
qed.

(*
Hint Resolve valid_block_free_1 valid_block_free_2: mem.
*)

lemma low_bound_free:
  ∀m,bf,b. b ≠ bf -> low_bound (free m bf) b = low_bound m b.
#m #bf #b #H whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?);
>(update_o block_contents …) //; @sym_neq //;
qed.

lemma high_bound_free:
  ∀m,bf,b. b ≠ bf → high_bound (free m bf) b = high_bound m b.
#m #bf #b #H whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?);
>(update_o block_contents …) //; @sym_neq //;
qed.

lemma low_bound_free_same:
  ∀m,b. low_bound (free m b) b = 0.
#m #b whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?);
>(update_s block_contents …) //;
qed.

lemma high_bound_free_same:
  ∀m,b. high_bound (free m b) b = 0.
#m #b whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?);
>(update_s block_contents …) //;
qed.

lemma class_free:
  ∀m,bf,b. b ≠ bf → block_region (free m bf) b = block_region m b.
#m #bf #b #H whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?);
>(update_o block_contents …) //; @sym_neq //;
qed.

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

lemma valid_access_free_2:
  ∀m,r,bf,chunk,ofs. ¬(valid_access (free m bf) chunk r bf ofs).
#m #r #bf #chunk #ofs @nmk *; #Hval #Hlo #Hhi #Hal #Hct
whd in Hlo:(?%?);whd in Hlo:(?(?(?%?))?); >(update_s block_contents …) in Hlo
whd in Hhi:(??%);whd in Hhi:(??(?(?%?))); >(update_s block_contents …) in Hhi
whd in ⊢ ((??%)→(?%?)→?); (* arith *) @daemon
qed.

(*
Hint Resolve valid_access_free_1 valid_access_free_2: mem.
*)

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

theorem load_free:
  ∀m,bf,chunk,r,b,ofs.
  b ≠ bf →
  load chunk (free m bf) r b ofs = load chunk m r b ofs.
#m #bf #chunk #r #b #ofs #ne whd in ⊢ (??%%);
elim (in_bounds m chunk r b ofs);
[ #Hval whd in ⊢ (???%); >(in_bounds_true ????? (option val) ???)
  [ whd in ⊢ (??(??(??(???(?(?%?)))))?); >(update_o block_contents …) //;
      @sym_neq //
  | @valid_access_free_1 //; @ne
  ]
| elim (in_bounds (free m bf) chunk r b ofs); (* XXX just // used to work *) [ 2: normalize; //; ]
    #H #H' @False_ind @(absurd ? ? H')
    elim (valid_access_free_inv …H); //;
] qed.

(*
End FREE.
*)

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

lemma valid_block_free_list_1:
  ∀bl,m,b. valid_block m b → valid_block (free_list m bl) b.
#bl elim bl;
[ #m #b #H whd in ⊢ (?%?); //
| #h #t #IH #m #b #H >(unfold_free_list m h t)
    @valid_block_free_1 @IH //
] qed.

lemma valid_block_free_list_2:
  ∀bl,m,b. valid_block (free_list m bl) b → valid_block m b.
#bl elim bl;
[ #m #b #H whd in H:(?%?); //
| #h #t #IH #m #b >(unfold_free_list m h t) #H
    @IH @valid_block_free_2 //
] qed.

lemma valid_access_free_list:
  ∀chunk,r,b,ofs,m,bl.
  valid_access m chunk r b ofs → ¬in_list ? b bl →
  valid_access (free_list m bl) chunk r b ofs.
#chunk #r #b #ofs #m #bl elim bl;
[ whd in ⊢ (?→?→(?%????)); //
| #h #t #IH #H #notin >(unfold_free_list m h t) @valid_access_free_1
    [ @IH //; @(not_to_not ??? notin) #Ht napply (in_list_cons … Ht)
    | @nmk #e @(absurd ?? notin) >e // ]
] qed.

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

(* ** Properties related to pointer validity *)

lemma valid_pointer_valid_access:
  ∀m,r,b,ofs.
  valid_pointer m r b ofs = true ↔ valid_access m Mint8unsigned r b ofs.
#m #r #b #ofs whd in ⊢ (?(??%?)?); %
[ #H
    lapply (andb_true_l … H); #H'
    lapply (andb_true_l … H'); #H''
    lapply (andb_true_l … H''); #H1
    lapply (andb_true_r … H''); #H2
    lapply (andb_true_r … H'); #H3
    lapply (andb_true_r … H); #H4
    %
    [ >(unfold_valid_block m b) napply (Zltb_true_to_Zlt … H1)
    | napply (Zleb_true_to_Zle … H2)
    | whd in ⊢ (?(??%)?); (* arith, Zleb_true_to_Zle *) napply daemon
    | cases ofs; /2/;
    | whd in H4:(??%?); elim (pointer_compat_dec (block_region m b) r) in H4;
        [ //; | #Hn #e whd in e:(??%%); destruct ]
    ]
| *; #Hval #Hlo #Hhi #Hal #Hct
    >(Zlt_to_Zltb_true … Hval)
    >(Zle_to_Zleb_true … Hlo)
    whd in Hhi:(?(??%)?); >(Zlt_to_Zltb_true … ?)
    [ whd in ⊢ (??%?); elim (pointer_compat_dec (block_region m b) r);
      [ //;
      | #Hct' @False_ind @(absurd … Hct Hct')
      ] 
    | (* arith *) napply daemon
    ]
]
 qed. 

theorem valid_pointer_alloc:
  ∀m1,m2: mem. ∀lo,hi: Z. ∀bcl,r. ∀b,b': block. ∀ofs: Z.
  alloc m1 lo hi bcl = 〈m2, b'〉 →
  valid_pointer m1 r b ofs = true →
  valid_pointer m2 r b ofs = true.
#m1 #m2 #lo #hi #bcl #r #b #b' #ofs #ALLOC #VALID
lapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval
@(proj2 ?? (valid_pointer_valid_access ????))
@(valid_access_alloc_other … ALLOC … Hval)
qed.

theorem valid_pointer_store:
  ∀chunk: memory_chunk. ∀m1,m2: mem.
  ∀r,r': region. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val.
  store chunk m1 r' b' ofs' v = Some ? m2 →
  valid_pointer m1 r b ofs = true → valid_pointer m2 r b ofs = true.
#chunk #m1 #m2 #r #r' #b #b' #ofs #ofs' #v #STORE #VALID
lapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval
@(proj2 ?? (valid_pointer_valid_access ????))
@(store_valid_access_1 … STORE … Hval)
qed.

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

definition meminj : Type[0] ≝ block → option (block × Z).
(*
Variable val_inj: meminj -> val -> val -> Prop.

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

definition 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*)
lemma 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).
//; qed.

lemma 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
cut (∃v1. load chunk m1 b1 ofs = Some ? v1);
[ /2/;
| *;#v1 #LOAD1
    elim (Hinj … H LOAD1);#v2 *;#LOAD2 #VCP
    /2/
] qed.

(*Hint Resolve valid_access_inj: mem.*)
*)
(* FIXME: can't use destruct below *)
lemma grumpydestruct : ∀A,v. None A = Some A v → False.
#A #v #H destruct;
qed.
(*
lemma store_unmapped_inj: ∀val_inj.
  ∀mi,m1,m2,r,b,ofs,v,chunk,m1'.
  mem_inj val_inj mi m1 m2 →
  mi b = None ? →
  store chunk m1 r b ofs v = Some ? m1' →
  mem_inj val_inj mi m1' m2.
#val_inj
#mi #m1 #m2 #r #b #ofs #v #chunk #m1' #Hinj #Hmi #Hstore
whd; #chunk0 #b1 #ofs0 #v1 #b2 #delta #Hmi0 #Hload
cut (load chunk0 m1 b1 ofs0 = Some ? v1);
[ <Hload @sym_eq @(load_store_other … Hstore)
    %{1} %{1} @nmk #eq >eq in Hmi0 >Hmi #H destruct;
| #Hload' @(Hinj … Hmi0 Hload')
] qed.

lemma store_outside_inj: ∀val_inj.
  ∀mi,m1,m2,chunk,r,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 r b ofs v = Some ? m2' →
  mem_inj val_inj mi m1 m2'.
#val_inj
#mi #m1 #m2 #chunk #r #b #ofs #v #m2' #Hinj #Hbounds #Hstore
whd; #chunk0 #b1 #ofs0 #v1 #b2 #delta #Hmi0 #Hload
lapply (Hinj … Hmi0 Hload);*;#v2 *;#LOAD2 #VINJ
%{ v2} % //;
<LOAD2 @(load_store_other … Hstore)
elim (decidable_eq_Z b2 b);
[ #Heq >Heq in Hmi0 LOAD2 #Hmi0 #LOAD2
    lapply (Hbounds … Hmi0); #Hb
    cut (valid_access m1 chunk0 b1 ofs0); /2/;
    #Hv elim Hv; #Hv1 #Hlo1 #Hhi1 #Hal1
    elim Hb; #Hb [ %{1} %{2} (* arith *) napply daemon | %{2} (* arith *) napply daemon ]
| #ineq %{1} %{1} @ineq
] qed.

(* XXX: use Or rather than ∨ to bring resource usage under control. *)
definition 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 *)
lemma grumpydestruct1 : ∀A,x1,x2. Some A x1 = Some A x2 → x1 = x2.
#A #x1 #x2 #H destruct;//;
qed.
lemma 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 destruct;/2/;
qed. 
(*
lemma 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
cut (∃m2'.store chunk m2 b2 (ofs + delta) v2 = Some ? m2');
[ @valid_access_store @(valid_access_inj ? mi ??????? Hb1 Hinj ?) (* XXX why do I have to give mi here? *) /2/
| *;#m2' #STORE2
    %{ m2'} % //;
    whd; #chunk' #b1' #ofs' #v #b2' #delta' #CP #LOAD1
    cut (valid_access m1 chunk' b1' ofs');
    [ @(store_valid_access_2 … STORE) @(load_valid_access … LOAD1)
    | #Hval
        lapply (load_store_characterization … STORE … Hval);
        elim (load_store_classification chunk b1 ofs chunk' b1' ofs');
        [ #e #e0 #e1 #H (* similar *)
            >e in Hb1 #Hb1
            >CP in Hb1 #Hb1 (* XXX destruct expands proof state too much;*)
            elim (grumpydestruct2 ?????? Hb1);
            #e2 #e3 <e0 >e2 >e3
            %{ (load_result chunk' v2)} %
            [ @(load_store_similar … STORE2) //
            | >LOAD1 in H #H whd in H:(??%%); destruct;
                @Hvalinj //;
            ]
         | #Hdis #H (* disjoint *)
             >LOAD1 in H #H
             lapply (Hinj … CP ?); [ @sym_eq @H | *: ]
             *;#v2' *;#LOAD2 #VCP
             %{ v2'} % //;
             <LOAD2 @(load_store_other … STORE2)
             elim (decidable_eq_Z b1 b1'); #eb1
             [ <eb1 in CP #CP >CP in Hb1 #eb2d
                 elim (grumpydestruct2 ?????? eb2d); #eb2 #ed
                 elim Hdis; [ #Hdis elim Hdis;
                               [ #eb1' @False_ind @(absurd ? eb1 eb1')
                               | #Hdis %{1} %{2} (* arith *) napply daemon
                               ] | #Hdis %{2} (* arith *) napply daemon ]
             | cut (valid_access m1 chunk b1 ofs); /2/; #Hval'
                 lapply (Hnoover … eb1 Hb1 CP);
                 #Ha elim Ha; #Ha
                 [ elim Ha; #Ha
                 [ elim Ha; #Ha
                 [ %{1} %{1} /2/
                 | elim Hval'; lapply (size_chunk_pos chunk); (* arith *) napply daemon ]
                 | elim Hval; lapply (size_chunk_pos chunk'); (* arith *) napply daemon ]
                 | elim Hval'; elim Hval;  (* arith *) napply daemon ]
             ]
         | #eb1 #Hofs1 #Hofs2 #Hofs3 #H (* overlapping *)
             <eb1 in CP #CP >CP in Hb1 #eb2d
             elim (grumpydestruct2 ?????? eb2d); #eb2 #ed
             cut (∃v2'. load chunk' m2' b2 (ofs' + delta) = Some ? v2');
             [ @valid_access_load @(store_valid_access_1 … STORE2) @(valid_access_inj … Hinj Hval) >eb1 //
             | *;#v2' #LOAD2'
                 cut (v2' = Vundef); [ @(load_store_overlap … STORE2 … LOAD2') (* arith *) napply daemon | ]
                 #ev2' %{ v2'} % //;
                 >LOAD1 in H #H whd in H:(??%%); >(grumpydestruct1 … H)
                 >ev2'
                 @val_inj_undef ]
         | #eb1 #Hofs <Hofs in Hval LOAD1 ⊢ % #Hval #LOAD1 #Hsize #H (* overlapping *)
             
             <eb1 in CP #CP >CP in Hb1 #eb2d
             elim (grumpydestruct2 ?????? eb2d); #eb2 #ed
             cut (∃v2'. load chunk' m2' b2 (ofs + delta) = Some ? v2');
             [ @valid_access_load @(store_valid_access_1 … STORE2) @(valid_access_inj … Hinj Hval) >eb1 //
             | *;#v2' #LOAD2'
                 cut (v2' = Vundef); [ @(load_store_mismatch … STORE2 … LOAD2' ?) @sym_neq // | ]
                 #ev2' %{ v2'} % //;
                 >LOAD1 in H #H whd in H:(??%%); >(grumpydestruct1 … H)
                 >ev2'
                 @val_inj_undef ]
         ]
     ]
] qed.

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

lemma 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
whd; #chunk #b1' #ofs #v #b2' #delta' #Hbinj' #LOAD
lapply (valid_access_alloc_inv … m1 … ALLOC1 chunk b1' ofs ?); /2/;
*;
[ #A
    cut (load chunk m1 b1' ofs = Some ? v);
    [ <LOAD @sym_eq @(load_alloc_unchanged … ALLOC1) /2/; ]
    #LOAD0 lapply (Hinj … Hbinj' LOAD0); *;#v2 *;#LOAD2 #VINJ
    %{ v2} %
    [ <LOAD2 @(load_alloc_unchanged … ALLOC2)
        @valid_access_valid_block [ 3: @load_valid_access ]
        //
    | //
    ]
| *;*;#A #B #C
    >A in Hbinj' LOAD #Hbinj' #LOAD
    >Hbinj in Hbinj' #Hbinj' elim (grumpydestruct2 ?????? Hbinj');
    #eb2 #edelta <eb2 <edelta
    cut (v = Vundef); [ @(load_alloc_same … ALLOC1 … LOAD) ]
    #ev >ev
    cut (∃v2. load chunk m2' b2 (ofs + delta) = Some ? v2);
    [ @valid_access_load
        @(valid_access_alloc_same … ALLOC2)
        [ 1,2: (*arith*) @daemon
        | (* arith using Hal *) napply daemon
        ] ]
    *;#v2 #LOAD2
    cut (v2 = Vundef); [ napply (load_alloc_same … ALLOC2 … LOAD2) ]
    #ev2 >ev2
    %{ Vundef} % //;
] qed.

lemma 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
whd; #chunk #b1 #ofs #v1 #b2' #delta #Hbinj #LOAD
lapply (Hinj … Hbinj LOAD); *; #v2 *;#LOAD2 #VINJ
%{ v2} % //;
cut (valid_block m2 b2');
  [ @(valid_access_valid_block ? chunk ? (ofs + delta)) /2/ ]
#Hval
<LOAD2 @(load_alloc_unchanged … ALLOC … Hval)
qed.

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

lemma 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
whd;  #chunk #b1' #ofs #v1 #b2' #delta #Hbinj' #LOAD
lapply (valid_access_alloc_inv … m1 … ALLOC chunk b1' ofs ?); /2/;
*;
[ #A
  @(Hinj … Hbinj' )
  <LOAD @sym_eq @(load_alloc_unchanged … ALLOC) /2/;
| *;*;#A #B #C
  >A in Hbinj' LOAD #Hbinj' #LOAD
  >Hbinj in Hbinj' #bad destruct;
] qed.

lemma 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
whd; #chunk #b1' #ofs #v1 #b2' #delta' #Hbinj' #LOAD
lapply (valid_access_alloc_inv … m1 … ALLOC chunk b1' ofs ?); /2/;
*;
[ #A
    @(Hinj … Hbinj')
    <LOAD @sym_eq @(load_alloc_unchanged … ALLOC) /2/;
| *;*;#A #B *;#C #D
    >A in Hbinj' LOAD #Hbinj' #LOAD >Hbinj in Hbinj'
    #Hbinj' (* XXX destruct normalizes too much here *) elim (grumpydestruct2 ?????? Hbinj'); #eb2 #edelta
    <eb2 <edelta
    cut (v1 = Vundef); [ napply (load_alloc_same … ALLOC … LOAD) ]
    #ev1 >ev1
    cut (∃v2. load chunk m2 b2 (ofs + delta) = Some ? v2);
    [ @valid_access_load % //;
      [ (* arith *) napply daemon
      | (* arith *) napply daemon
      | (* arith *) napply daemon
      ]
    ]
    *;#v2 #LOAD2 %{ v2} % //;
] qed.

lemma 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
whd; #chunk #b1' #ofs #v1 #b2' #delta' #Hbinj' #LOAD
lapply (valid_access_free_inv … (load_valid_access … LOAD)); *; #A #B
cut (load chunk m1 b1' ofs = Some ? v1);
[ <LOAD @sym_eq @load_free @B ] #LOAD'
elim (Hinj … Hbinj' LOAD'); #v2 *;#LOAD2 #INJ
%{ v2} %
[ <LOAD2 @load_free
    @nmk #e @(absurd ?? B)
    >e in Hbinj' #Hbinj' @(Hbinj ?? Hbinj')
| //
] qed.

lemma 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
whd; #chunk #b1' #ofs #v1 #b2' #delta' #Hbinj' #LOAD
lapply (valid_access_free_inv … (load_valid_access … LOAD)); *; #A #B
@(Hinj … Hbinj')
<LOAD @sym_eq @load_free @B
qed. 

lemma 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 elim bl;
[ whd in ⊢ (?→?→?→???%?); //
| #h #t #IH #m1 #m2 #H >(unfold_free_list m1 h t)
    @free_left_inj @IH //
] qed.

lemma 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
whd; #chunk #b1' #ofs #v1 #b2' #delta' #Hbinj' #LOAD
cut (b2' ≠ b2);
[ @nmk #e >e in Hbinj' #Hbinj'
    @(absurd ?? (Hinval … Hbinj')) @(load_valid_access … LOAD) ]
#ne lapply (Hinj … Hbinj' LOAD); *;#v2 *;#LOAD2 #INJ
%{ v2} % //;
<LOAD2 @load_free @ne
qed.

lemma 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
lapply ((proj1 ?? (valid_pointer_valid_access ???)) VALID); #Hval
@(proj2 ?? (valid_pointer_valid_access ???))
@(valid_access_inj … Hval) //;
qed.

(*
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]. *)

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

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

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

theorem extends_refl:
  ∀m: mem. extends m m.
#m % //;
whd; #chunk #b1 #ofs #v1 #b2 #delta normalize in ⊢ (%→?);#H
(* XXX: destruct makes the goal unreadable *) elim (grumpydestruct2 ?????? H); #eb1 #edelta #LOAD
%{ v1} %
[ <edelta >(Zplus_z_OZ ofs) //;
| //
] qed. 

theorem 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
cut (b1 = b2);
[ @(transitive_eq … (nextblock m1)) [ @(alloc_result … ALLOC1)
    | @sym_eq >Hnext napply (alloc_result … ALLOC2) ] ]
#eb <eb in ALLOC2 ⊢ % #ALLOC2 % //; %
[ >(nextblock_alloc … ALLOC1)
    >(nextblock_alloc … ALLOC2)
    //;
| @(alloc_parallel_inj ??????????????? ALLOC1 ALLOC2 ????)
  [ 1,4: normalize; //;
  | 3,5,6: //
  | 7: whd; #chunk #Hsize (* divides 0 *) napply daemon
  ]
] qed.

theorem free_extends:
  ∀m1,m2: mem. ∀b: block.
  extends m1 m2 →
  extends (free m1 b) (free m2 b).
#m1 #m2 #b *;#Hnext #Hinj %
[ normalize; //;
| @(free_parallel_inj … Hinj)
  [ 2: //;
  | 3: normalize; #b' #delta #ee destruct; //
  ]
] qed. 

theorem load_extends:
  ∀chunk: memory_chunk. ∀m1,m2: mem. ∀b: block. ∀ofs: Z. ∀v: val.
  extends m1 m2 →
  load chunk m1 r b ofs = Some ? v →
  load chunk m2 r b ofs = Some ? v.
#chunk #m1 #m2 #r #b #ofs #v
*;#Hnext #Hinj #LOAD
lapply (Hinj … LOAD); [ normalize; // | 2,3: ]
*;#v2 *; >(Zplus_z_OZ ofs) #LOAD2 #EQ whd in EQ;
//;
qed.

theorem store_within_extends:
  ∀chunk: memory_chunk. ∀m1,m2,m1': mem. ∀b: block. ∀ofs: Z. ∀v: val.
  extends m1 m2 →
  store chunk m1 r b ofs v = Some ? m1' →
  ∃m2'. store chunk m2 r b ofs v = Some ? m2' ∧ extends m1' m2'.
#chunk #m1 #m2 #m1' #b #ofs #v *;#Hnext #Hinj #STORE1
lapply (store_mapped_inj … Hinj ?? STORE1 ?);
[ 1,2,7: normalize; //
| (* TODO: unfolding, etc ought to tidy this up *)
    whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neb #Hinj1 #Hinj2
    normalize in Hinj1 Hinj2; %{1} %{1} %{1} destruct; //
| 4,5,6: ##skip
]
*;#m2' *;#STORE #MINJ
%{ m2'} % >(Zplus_z_OZ ofs) in STORE #STORE //;
%
[ >(nextblock_store … STORE1)
    >(nextblock_store … STORE)
    //
| //
] qed.

theorem 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 r b ofs v = Some ? m2' →
  extends m1 m2'.
#chunk #m1 #m2 #m2' #b #ofs #v *;#Hnext #Hinj #Houtside #STORE %
[ >(nextblock_store … STORE) //
| @(store_outside_inj … STORE) //;
    #b' #delta #einj normalize in einj; destruct;
    elim Houtside; 
    [ #lo %{ 2} >(Zplus_z_OZ ?) /2/
    | #hi %{ 1}  >(Zplus_z_OZ ?) /2/
    ]
] qed.

theorem valid_pointer_extends:
  ∀m1,m2,b,ofs.
  extends m1 m2 → valid_pointer m1 r b ofs = true →
  valid_pointer m2 r b ofs = true.
#m1 #m2 #b #ofs *;#Hnext #Hinj #VALID
<(Zplus_z_OZ ofs)
@(valid_pointer_inj … Hinj VALID) //;
qed.


(* * 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]. *)

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

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

lemma lessdef_refl:
  ∀m. lessdef m m.
#m % //;
whd; #chunk #b1 #ofs #v1 #b2 #delta #H #LOAD
whd in H:(??%?); elim (grumpydestruct2 ?????? H); #eb1 #edelta
%{ v1} % //;
qed.

lemma load_lessdef:
  ∀m1,m2,chunk,b,ofs,v1.
  lessdef m1 m2 → load chunk m1 r b ofs = Some ? v1 →
  ∃v2. load chunk m2 r b ofs = Some ? v2 ∧ Val_lessdef v1 v2.
#m1 #m2 #chunk #b #ofs #v1 *;#Hnext #Hinj #LOAD0
lapply (Hinj … LOAD0); [ whd in ⊢ (??%?); // | 2,3:##skip ]
*;#v2 *;#LOAD #INJ %{ v2} % //;
qed.

lemma 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
inversion H0;
[ #v #e1 #e2 >e1 in LOAD cases v;
    [ whd in ⊢ ((??%?)→?); #H' destruct;
    | 2,3: #v' whd in ⊢ ((??%?)→?); #H' destruct;
    | #b' #off @load_lessdef //
    ]
| #v #e >e in LOAD #LOAD whd in LOAD:(??%?); destruct;
] qed.

lemma store_lessdef:
  ∀m1,m2,chunk,b,ofs,v1,v2,m1'.
  lessdef m1 m2 → Val_lessdef v1 v2 →
  store chunk m1 r b ofs v1 = Some ? m1' →
  ∃m2'. store chunk m2 r b ofs v2 = Some ? m2' ∧ lessdef m1' m2'.
#m1 #m2 #chunk #b #ofs #v1 #v2 #m1'
*;#Hnext #Hinj #Hvless #STORE0
lapply (store_mapped_inj … Hinj … STORE0 ?);
[ #chunk' #Hsize whd;@load_result_lessdef napply Hvless
| whd in ⊢ (??%?); //
| whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neq
    whd in ⊢ ((??%?)→(??%?)→?); #e1 #e2 destruct;
    % % % //
| 7: #mi whd; //;
| 8: *;#m2' *;#STORE #MINJ
         %{ m2'} % /2/;
         %
         >(nextblock_store … STORE0)
         >(nextblock_store … STORE)
         //;
] qed.

lemma 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
inversion Haless;
[ #v #e1 #e2 >e1 in STORE cases v;
    [ whd in ⊢ ((??%?)→?); #H' @False_ind destruct;
    | 2,3: #v' whd in ⊢ ((??%?)→?); #H' destruct;
    | #b' #off @store_lessdef //
    ]
| #v #e >e in STORE #STORE whd in STORE:(??%?); destruct
] qed.

lemma 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
cut (b1 = b2);
[ >(alloc_result … ALLOC1) >(alloc_result … ALLOC2) //
]
#e <e in ALLOC2 ⊢ % #ALLOC2 % //;
%
[ >(nextblock_alloc … ALLOC1)
    >(nextblock_alloc … ALLOC2)
    //
| @(alloc_parallel_inj … Hinj ALLOC1 ALLOC2)
[ //
| 3: whd in ⊢ (??%?); //
| 4,5: //;
| 6: whd; #chunk #_ cases chunk;//;
] qed.

lemma free_lessdef:
  ∀m1,m2,b. lessdef m1 m2 → lessdef (free m1 b) (free m2 b).
#m1 #m2 #b *;#Hnext #Hinj %
[ whd in ⊢ (??%%); //
| @(free_parallel_inj … Hinj) //;
    #b' #delta #H whd in H:(??%?); elim (grumpydestruct2 ?????? H); //
] qed.

lemma free_left_lessdef:
  ∀m1,m2,b.
  lessdef m1 m2 → lessdef (free m1 b) m2.
#m1 #m2 #b *;#Hnext #Hinj %
<Hnext //;
@free_left_inj //;
qed.

lemma 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
% >Hnext //;
@free_right_inj //;
#b1 #delta #chunk #ofs #H whd in H:(??%?); destruct;
@nmk *; #H1 #H2 #H3 #H4
(* arith H2 and H3 contradict Hbounds. *) @daemon
qed.

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

lemma valid_pointer_lessdef:
  ∀m1,m2,b,ofs.
  lessdef m1 m2 → valid_pointer m1 r b ofs = true → valid_pointer m2 r b ofs = true.
#m1 #m2 #b #ofs *;#Hnext #Hinj #VALID
<(Zplus_z_OZ ofs) @(valid_pointer_inj … Hinj VALID) //;
qed.


(* ** 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. *)

inductive 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.
*)
inductive 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.
*)

record 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. *)

lemma 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
elim (mi_range_2 ??? Hb1inj);
[ (* delta = 0 *)
    #edelta >edelta
    >(?:repr O = zero) [ 2: // ]
    >(add_zero ?)
    >(Zplus_z_OZ …)
    //;
| (* delta ≠ 0 *)
    #Hrange >(add_signed ??)
    >(signed_repr delta ?)
    [ >(signed_repr ??)
      [ //
      | cut (valid_access m2 chunk b2 (signed ofs1 + delta));
        [ @(valid_access_inj … Hvalid) //;
        | *; #_ #Hlo #Hhi #_ (* arith *) napply daemon
        ]
      ]
    | /2/
    ]
] qed.

lemma 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
lapply ((proj1 ?? (valid_pointer_valid_access ???)) Hvalid); #Hvalid'
cut (valid_access m2 Mint8unsigned b' (signed ofs + x));
[ @(valid_access_inj … Hvalid') // ]
*; >(?:size_chunk Mint8unsigned = 1) [ 2: // ] #_ #Hlo #Hhi #_
>(signed_repr ??) [ 2: /2/; ]
lapply (mi_range_2 … Hb1inj); *;
[ #ex >ex >(Zplus_z_OZ ?) @signed_range
| (* arith *) napply daemon
] qed.

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

lemma 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 r b ofs) (Vptr b' ofs') →
  valid_pointer m2 b' (signed ofs') = true.
#f #m1 #m2 #b #ofs #b' #ofs'
#Hinj #Hvalid #Hvinj inversion Hvinj;
[ 1,2,4: #x #H destruct; ]
#b0 #i #b0' #i' #delta #Hb #Hi' #eptr #eptr'
<(proj1 … (vptr_eq ???? eptr)) in Hb <(proj1 … (vptr_eq ???? eptr'))
<(proj2 … (vptr_eq ???? eptr)) in Hi' <(proj2 … (vptr_eq ???? eptr'))
  #Hofs #Hbinj
>Hofs
lapply (valid_pointer_inject_no_overflow … Hinj Hvalid Hbinj); #NOOV
elim Hinj;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2
>(add_signed ??) >(signed_repr ??) //;
>(signed_repr ??) /2/;
@(valid_pointer_inj … mi_inj Hvalid) //;
qed.

lemma 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
lapply ((proj1 ?? (valid_pointer_valid_access …)) Hval1); #Hval1'
lapply ((proj1 ?? (valid_pointer_valid_access …)) Hval2); #Hval2'
>(address_inject … Hinj Hval1' Hf1)
>(address_inject … Hinj Hval2' Hf2)
elim Hval1'; #Hbval #Hlo #Hhi #Hal whd in Hhi:(?(??%)?);
elim Hval2'; #Hbval2 #Hlo2 #Hhi2 #Hal2 whd in Hhi2:(?(??%)?);
lapply (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  ] ]
qed.

(* Relation between injections and loads. *)

lemma 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
@mi_inj //;
qed.

lemma 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 inversion Hvinj;
[ 1,2,4: #x #ex #ex' @False_ind destruct; ]
#b #ofs #b' #ofs' #delta #Hbinj #Hofs #ea1 #ea2
>ea1 in LOADV #LOADV
lapply (load_inject … Hinj LOADV … Hbinj); *; #v2 *; #LOAD #INJ
%{ v2} % //; >Hofs
<(?:signed (add ofs (repr delta)) = signed ofs + delta) in LOAD
[ #H @H (* XXX: used to work with /2/ *)
| @(address_inject … chunk … Hinj ? Hbinj) @(load_valid_access …)
    [ 2: @LOADV ]
] qed.

(* Relation between injections and stores. *)

inductive 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.*)

lemma 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 inversion Hvci;
[ #chunk'' #v1' #v2' #Hvinj #_ #_ #_ #Hsize inversion Hvinj;
  [ cases chunk'; #i #_ #_ [ 1,2,3,4,5: @ | 6,7: @4 ]
  | cases chunk'; #f #_ #_ [ 1,2,3,4,5: @4 | 6,7: @2 ]
  | cases chunk'; #b1 #ofs1 #b2 #ofs2 #delta #Hmap #Hofs #_ #_ [ 5: %{3} // | *: @4 ]
  | cases chunk'; #v #_ #_ %{4}
  ]
(* FIXME: the next two cases are very similar *)
| #chunk'' #i #i' *;#echunk >echunk #Hz #_ #_ #_
    elim chunk'; whd in ⊢ ((??%%)→?); #Hsize destruct;
    [ 2,4: whd in ⊢ (??%%); >Hz @
    | 1,3: whd in ⊢ (??%%); >(sign_ext_equal_if_zero_equal … Hz)
        % [ 1,3: @I | 2,4: @leb_true_to_le % ]
    ]
| #chunk'' #i #i' *;#echunk >echunk #Hz #_ #_ #_
    elim chunk'; whd in ⊢ ((??%%)→?); #Hsize destruct;
    [ 2,4: whd in ⊢ (??%%); >Hz @
    | 1,3: whd in ⊢ (??%%); >(sign_ext_equal_if_zero_equal … Hz)
        % [ 1,3: @I | 2,4: @leb_true_to_le % ]
    ]

| #f #f' #float #echunk >echunk #_ #_
    elim chunk'; whd in ⊢ ((??%%)→?); #Hsize destruct;
    [ %{4} | >float @2 ]
] qed.

lemma 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
lapply (store_mapped_inj … mi_inj mi_no_overlap INJb1 STORE1 ?); //;
[ #chunk' #Hchunksize @(load_result_inject … chunk …) //;
| ##skip ]
*;#n2 *;#STORE #MINJ
%{ n2} % //; %
[ (* inj *) //
| (* freeblocks *) #b #notvalid @mi_freeblocks
    @(not_to_not ??? notvalid) @(store_valid_block_1 … STORE1)
| (* mappedblocks *) #b #b' #delta' #INJb' @(store_valid_block_1 … STORE)
    /2/;
| (* no_overlap *) whd; #b1' #b1'' #delta1' #b2' #b2'' #delta2' #neqb'
    #fb1' #fb2'
    >(low_bound_store … STORE1 ?)  >(low_bound_store … STORE1 ?)
    >(high_bound_store … STORE1 ?)  >(high_bound_store … STORE1 ?)
    @mi_no_overlap //;
| (* range *) /2/;
| (* range 2 *) #b #b' #delta' #INJb
    >(low_bound_store … STORE ?)
    >(high_bound_store … STORE ?)
    @mi_range_2 //;
] qed.

lemma 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 @(store_mapped_inject_1 … STORE) //;
@val_content_inject_base //;
qed.

lemma 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 *) @(store_unmapped_inj … STORE) //
| (* freeblocks *) #b #notvalid @mi_freeblocks
    @(not_to_not ??? notvalid) @(store_valid_block_1 … STORE)
| (* mappedblocks *) #b #b' #delta #INJb @mi_mappedblock //;
| (* no_overlap *) whd; #b1' #b1'' #delta1' #b2' #b2'' #delta2' #neqb'
    #fb1' #fb2'
    >(low_bound_store … STORE ?)  >(low_bound_store … STORE ?)
    >(high_bound_store … STORE ?)  >(high_bound_store … STORE ?)
    @mi_no_overlap //;
| (* range *) /2/
| /2/
] qed.

lemma 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
inversion Hvinj;
[ 1,2,4:#x #ex1 #ex2 >ex1 in STORE whd in ⊢ ((??%?)→?); #H
    @False_ind destruct; ]
#b #ofs #b' #ofs' #delta #INJb #Hofs #ea1 #ea2
>Hofs >ea1 in STORE #STORE
lapply (store_mapped_inject_1 … MINJ STORE … INJb Hvcinj); 
<(?:signed (add ofs (repr delta)) = signed ofs + delta) //;
@(address_inject … chunk … MINJ ? INJb)
@(store_valid_access_3 … STORE)
qed.

lemma 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'
@(storev_mapped_inject_1 … STOREV) /2/;
qed.

(* Relation between injections and [free] *)

lemma meminj_no_overlap_free:
  ∀mi,m,b.
  meminj_no_overlap mi m →
  meminj_no_overlap mi (free m b).
#mi #m #b #H whd;#b1 #b1' #delta1 #b2 #b2' #delta2 #Hne #mi1 #mi2
cut (low_bound (free m b) b ≥ high_bound (free m b) b);
[ >(low_bound_free_same …) >(high_bound_free_same …) // ]
#Hbounds
cases (decidable_eq_Z b1 b);#e1 [ >e1 in Hne mi1 ⊢ % #Hne #mi1 ]
cases (decidable_eq_Z b2 b);#e2 [ 1,3: >e2 in Hne mi2 ⊢ % #Hne #mi2 ]
[ @False_ind elim Hne; /2/
| % %{2} //;
| % % %{2} //
| >(low_bound_free …) //; >(low_bound_free …) //;
    >(high_bound_free …) //; >(high_bound_free …) //;
    /2/;
] qed.

lemma meminj_no_overlap_free_list:
  ∀mi,m,bl.
  meminj_no_overlap mi m →
  meminj_no_overlap mi (free_list m bl).
#mi #m #bl elim bl;
[ #H whd in ⊢ (??%); //
| #h #t #IH #H @meminj_no_overlap_free @IH //
] qed.

lemma 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 *)
    @free_right_inj [ @free_list_left_inj //; ]
    #b1 #delta #chunk #ofs #INJb1 @nmk #Hvalid
    elim (valid_access_free_list_inv … Hvalid); #b1ni #Haccess
    @(absurd ? (mappedin ?? INJb1) b1ni)
| (* freeblocks *)
    #b' #notvalid @mi_freeblocks @(not_to_not ??? notvalid)
    #H @valid_block_free_list_1 //
| (* mappedblocks *)
    #b1 #b1' #delta #INJb1 @valid_block_free_1 /2/
| (* overlap *)
    @meminj_no_overlap_free_list //
| (* range *)
    /2/
| #b1 #b2 #delta #INJb1 cases (decidable_eq_Z b2 b); #eb
    [ >eb
        >(low_bound_free_same ??) >(high_bound_free_same ??)
        %{2} (* arith *) napply daemon
    | >(low_bound_free …) //; >(high_bound_free …) /2/;
    ]
] qed.

(* Monotonicity properties of memory injections. *)

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

lemma inject_incr_refl :
   ∀f. inject_incr f f .
#f whd;#b % //; qed.

lemma inject_incr_trans :
  ∀f1,f2,f3. 
  inject_incr f1 f2 → inject_incr f2 f3 → inject_incr f1 f3 .
#f1 #f2 #f3 whd in ⊢ (%→%→%);#H1 #H2 #b
elim (H1 b); elim (H2 b); /2/; qed.

lemma 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
inversion Hvinj;
[ 1,2,4: #x #_ #_ //;
|#b #ofs #b' #ofs' #delta #INJb #Hofs #_ #_
elim (Hincr b); #H
[ @(val_inject_ptr ??????? Hofs) /2/;
| @False_ind >INJb in H #H destruct;
] qed.

lemma 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 elim vl;
[ #vl' #Hincr #H inversion H; //; #v #v' #l #l0 #_ #_ #_ #H destruct;
| #h #t #IH #vl' #Hincr #H1 inversion H1;
  [ #H destruct
  | #h' #h'' #t' #t'' #Hinj1 #Hintt #_ #e1 #e2 destruct;
      %{2} /2/; @IH //; @Hincr
  ]
] qed.

(*
Hint Resolve inject_incr_refl val_inject_incr val_list_inject_incr.
*)

(* Properties of injections and allocations. *)

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

lemma extend_inject_incr:
  ∀f,b,x.
  f b = None ? →
  inject_incr f (extend_inject b x f).
#f #b #x #INJb whd;#b' whd in ⊢ (?(???%)?);
@(eqZb_elim b' b) #eb /2/;
qed.

lemma 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 %
[ @(alloc_right_inj … ALLOC) //;
| /2/;
| #b1 #b2 #delta #INJb1 @(valid_block_alloc … ALLOC) /2/;
| //;
| /2/;
|#b1 #b2 #delta #INJb1 >(?:low_bound m2' b2 = low_bound m2 b2)
   [ >(?:high_bound m2' b2 = high_bound m2 b2) /2/;
       @high_bound_alloc_other /2/;
   | @low_bound_alloc_other /2/
   ]
] qed.

lemma 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
cut (inject_incr f (extend_inject b (None ?) f));
[ @extend_inject_incr @mi_freeblocks /2/; ]
#Hinject_incr % //; %
[ (* inj *)
    @(alloc_left_unmapped_inj … ALLOC)
    [ 2: whd in ⊢ (??%?); >(eqZb_z_z …) /2/; ]
    whd; #chunk #b1 #ofs #v1 #b2 #delta
    whd in ⊢ ((??%?)→?→?); @eqZb_elim #e whd in ⊢ ((??%?)→?→?);
    #Hextend #LOAD
    [ destruct;
    | lapply (mi_inj … Hextend LOAD); *; #v2 *; #LOAD2 #VINJ
    %{ v2} % //;
    @val_inject_incr //;
    ]
| (* freeblocks *)
    #b' #Hinvalid whd in ⊢ (??%?); @(eqZb_elim b' b) //;
    #neb @mi_freeblocks @(not_to_not ??? Hinvalid)
    @valid_block_alloc //;
| (* mappedblocks *)
    #b1 #b2 #delta whd in ⊢ (??%?→?); @(eqZb_elim b1 b) #eb
    [ #H destruct;
    | #H @(mi_mappedblock … H)
    ]
| (* overlap *)
    whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neb1 whd in ⊢ (??%?→??%?→?);
    >(low_bound_alloc … ALLOC ?) >(low_bound_alloc … ALLOC ?)
    >(high_bound_alloc … ALLOC ?) >(high_bound_alloc … ALLOC ?)
    lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1
    [ destruct
    | lapply (eqZb_to_Prop b2 b); elim (eqZb b2 b); #e2 #INJb2
      [ destruct
      | @mi_no_overlap /2/;
      ]
    ]
| (* range *) 
    #b1 #b2 #delta whd in ⊢ (??%?→?);
    lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1
    [ destruct
    | @(mi_range_1 … INJb1)
    ]
| #b1 #b2 #delta whd in ⊢ (??%?→?);
    lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1
    [  destruct
    | @(mi_range_2 … INJb1)
    ]
] qed.

lemma 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
cut (inject_incr f (extend_inject b (Some ? 〈b', ofs〉) f));
[ @extend_inject_incr @mi_freeblocks /2/; ]
#Hincr % //; %
[ (* inj *)
    @(alloc_left_mapped_inj … ALLOC … validb' boundlo boundhi) /2/;
    [ 2:whd in ⊢ (??%?); >(eqZb_z_z …) /2/; ]
    whd; #chunk #b1 #ofs' #v1 #b2 #delta #Hextend #LOAD
    whd in Hextend:(??%?); >(eqZb_false b1 b ?) in Hextend
    [ #Hextend lapply (mi_inj … Hextend LOAD);
        *; #v2 *; #LOAD2 #VINJ
    %{ v2} % //;
    @val_inject_incr //;
    | @(valid_not_valid_diff m1) /2/;
        @(valid_access_valid_block … chunk … ofs') /2/;
    ]
| (* freeblocks *)
    #b' #Hinvalid whd in ⊢ (??%?); >(eqZb_false b' b ?)
    [ @mi_freeblocks @(not_to_not ??? Hinvalid)
    @valid_block_alloc //;
    | @sym_neq @(valid_not_valid_diff m1') //;
        @(valid_new_block … ALLOC)
    ]
| (* mappedblocks *)
    #b1 #b2 #delta whd in ⊢ (??%?→?); @(eqZb_elim b1 b) #eb #einj
    [ destruct; //;
    | @(mi_mappedblock … einj)
    ]
| (* overlap *)
    whd; #b1 #b1' #delta1 #b2 #b2' #delta2 #neb1 whd in ⊢ (??%?→??%?→?);
    >(low_bound_alloc … ALLOC ?) >(low_bound_alloc … ALLOC ?)
    >(high_bound_alloc … ALLOC ?) >(high_bound_alloc … ALLOC ?)
    lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1
    [ elim (grumpydestruct2 ?????? INJb1); #eb1' #eofs1 ]
    lapply (eqZb_to_Prop b2 b); elim (eqZb b2 b); #e2 #INJb2
    [ elim (grumpydestruct2 ?????? INJb2); #eb2' #eofs2 ]
    [ @False_ind >e in neb1 >e2 /2/;
    | elim (decidable_eq_Z b1' b2'); #e'
        [ <e' in INJb2 ⊢ % <eb1' <eofs1 #INJb2 lapply (boundmapped … INJb2);
            *; #H %{2} [ %{2 | @1 ] napply H}
        | %{1} %{1} %{1} napply e'
        ]
    | elim (decidable_eq_Z b1' b2'); #e'
        [ <e' in INJb2 ⊢ % #INJb2 elim (grumpydestruct2 ?????? INJb2); #eb' #eofs <eb' in INJb1 <eofs #INJb1 lapply (boundmapped … INJb1);
            *; #H %{2} [ %{1} /2/ | %{2} @H ]
        | %{1} %{1} %{1} napply e'
        ]
    | @mi_no_overlap /2/;
    ]
| (* range *) 
    #b1 #b2 #delta whd in ⊢ (??%?→?);
    lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1
    [ destruct; /2/;
    | @(mi_range_1 … INJb1)
    ]
| #b1 #b2 #delta whd in ⊢ (??%?→?);
    lapply (eqZb_to_Prop b1 b); elim (eqZb b1 b); #e #INJb1
    [ destruct; %{2} % /2/;
    | @(mi_range_2 … INJb1)
    ]
] qed.

lemma 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
@(alloc_mapped_inject … ALLOC1) /2/;
[ @(alloc_right_inject … Hminj ALLOC2)
| >(low_bound_alloc_same … ALLOC2) //
| >(high_bound_alloc_same … ALLOC2) //
| >(low_bound_alloc_same … ALLOC2) //
| >(high_bound_alloc_same … ALLOC2) //
| whd; (* arith *) napply daemon
| #b #ofs #INJb0 @False_ind
    elim Hminj;#mi_inj #mi_freeblocks #mi_mappedblock #mi_no_overlap #mi_range_1 #mi_range_2
    lapply (mi_mappedblock … INJb0);
    #H @(absurd ? H ?) /2/;
] qed.

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

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

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

lemma 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
cases (getN_setN_characterization m v n1 p1 n2 p2);[ * ] #A
>A //;
qed.
             
lemma 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 elim id;
[ #pos >(getN_init …) //
| #h #t #IH #pos cases h;
[ 1,2,3,4,5: #x @getN_setN_inject //
| 6,8: #x @IH | #x #y napply IH ] (* XXX // doesn't work? *)
qed.

lemma 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 whd in INIT:(??%?); (* XXX: destruct makes a bit of a mess *)
@(pairdisc_elim … INIT)
whd in ⊢ (??%% → ?);#B <B in ⊢ (??%% → ?)
whd in ⊢ (??%% → ?);#A
whd; #f #chunk #b' #ofs #v #LOAD
lapply (load_inv … LOAD); *; #C #D
<B in D >A
>(unfold_update block_contents …) @eqZb_elim
[ #eb' #D whd in D:(???(??(???%))); >D
    @(load_result_inject … chunk) //; %
    @getN_contents_init_data_inject
| #neb' #D @(Hneutral ? chunk b' ofs ??) whd in ⊢ (??%?);
    >(in_bounds_true m chunk b' ofs (option ?) …)
    [ <D //
    | elim C; #Cval #Clo #Chi #Cal %
    [ >(unfold_valid_block …)
        >(unfold_valid_block …) in Cval <B
        (* arith using neb' *) napply daemon
    | >(?:low_bound m b' = low_bound m' b') //;
        whd in ⊢ (??%%); <B >A
        >(update_o block_contents …) //; @sym_neq //;
    | >(?:high_bound m b' = high_bound m' b') //;
        whd in ⊢ (??%%); <B >A
        >(update_o block_contents …) //; @sym_neq //;
    | //;
    ]
] qed.


(* ** Memory shifting *)

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

definition memshift ≝ block → option Z.

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

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

record 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. *)

lemma 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
elim (ms_range_2 … INJb); #Hlo #Hhi
>(add_signed …)
>(signed_repr …) >(signed_repr …) /2/;
cut (valid_access m2 chunk b (signed ofs1 + delta));
[ @(valid_access_inj ? (meminj_of_shift f) … ms_inj Hvalid_access)
    whd in ⊢ (??%?); >INJb // ]
*; (* arith *) @daemon
qed.

lemma 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
lapply (proj1 ?? (valid_pointer_valid_access …) VALID); #Hvalid_access
cut (valid_access m2 Mint8unsigned b (signed ofs + x));
[ @(valid_access_inj … ms_inj Hvalid_access)
    whd in ⊢ (??%?); >INJb // ]
*;#Hvalid_block #Hlo #Hhi #Hal whd in Hhi:(?(??%)?);
>(signed_repr …) /2/;
lapply (ms_range_2 … INJb);*;#A #B
(* arith *) @daemon
qed.

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

lemma 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
whd in Hval_shift; inversion Hval_shift;
[ 1,2,4: #a #H destruct; ]
#b1 #ofs1 #b2 #ofs2 #delta #INJb1 #Hofs #eb1 #eb2
<(vptr_eq_1 … eb1) in INJb1 <(vptr_eq_1 … eb2) #INJb'
<(vptr_eq_2 … eb1) in Hofs <(vptr_eq_2 … eb2) #Hofs >Hofs
cut (f b = Some ? delta);
[ whd in INJb':(??%?); cases (f b) in INJb' ⊢ %;
  [ #H @(False_ind … (grumpydestruct … H)) | #delta' #H elim (grumpydestruct2 ?????? H); // ]
] #INJb
lapply (valid_pointer_shift_no_overflow … VALID INJb); //; #NOOV
elim Hmem_shift;#ms_inj #ms_samedomain #ms_domain #ms_range_1 #ms_range_2
>(add_signed …) >(signed_repr …) //;
>(signed_repr …) /2/;
@(valid_pointer_inj … VALID) /2/;
qed.

(* Relation between shifts and loads. *)

lemma 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
whd in ⊢ (??(λ_.??%)); @(ms_inj … LOAD)
whd in ⊢ (??%?); >INJb //;
qed.

lemma 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
inversion Hval_shift;
[ 1,2,4: #x #H >H in LOADV #H' whd in H':(??%?);@False_ind destruct; ]
#b1 #ofs1 #b2 #ofs2 #delta #INJb1 #Hofs #ea1 #ea2 >ea1 in LOADV #LOADV
lapply INJb1; whd in ⊢ (??%? → ?);
lapply (refl ? (f b1)); cases (f b1) in ⊢ (???% → %);
[ #_ whd in ⊢ (??%? → ?); #H @False_ind @(False_ind … (grumpydestruct … H))
| #delta' #DELTA whd in ⊢ (??%? → ?); #H elim (grumpydestruct2 ?????? H);
    #eb #edelta
] lapply (load_shift … Hmem_shift LOADV DELTA); *; #v2 *;#LOAD #INJ
%{ v2} % //; >Hofs >eb in LOAD >edelta
<(?:signed (add ofs1 (repr delta)) = signed ofs1 + delta)
[#H' @H' (* XXX // doesn't work *) 
| <edelta @(address_shift … chunk … Hmem_shift … DELTA)
    @(load_valid_access … LOADV)
]
qed.

(* Relation between shifts and stores. *)

lemma 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
lapply (store_mapped_inj … ms_inj ?? STORE1 ?);
[ #chunk' #echunk @(load_result_inject … chunk) /2/;
| whd in ⊢ (??%?); >INJb (* XXX: // has stopped working *) napply refl
| whd; #b1 #b1' #delta1 #b2 #b2' #delta2
    whd in ⊢ (? → ??%? → ??%? → ?);
    elim (f b1); elim (f b2);
    [#_ #e1 whd in e1:(??%?);destruct;
    |#z #_ #e1 whd in e1:(??%?);destruct;
    |#z #_ #_ #e2 whd in e2:(??%?);destruct;
    |#delta1' #delta2' #neb #e1 #e2
       whd in e1:(??%?) e2:(??%?);
       destruct;
       %{1} %{1} %{1} //;
    ]
| 7: //;
| 4,5,6: ##skip
]
*;#n2 *;#STORE #MINJ
%{ n2} % //; %
[ (* inj *) //
| (* samedomain *)
    >(nextblock_store … STORE1)
    >(nextblock_store … STORE)
    //;
| (* domain *)
    >(nextblock_store … STORE1)
    //
| (* range *)
    /2/
| #b1 #delta1 #INJb1
    >(low_bound_store … STORE b1)
    >(high_bound_store … STORE b1)
    @ms_range_2 //;
] qed.

lemma 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 *)
    @(store_outside_inj … STORE) //;
    #b' #d' whd in ⊢ (??%? → ?); lapply (refl ? (f b')); elim (f b') in ⊢ (???% → %);
    [ #_ #e whd in e:(??%?); destruct;
    | #d'' #ef #e elim (grumpydestruct2 ?????? e); #eb #ed
        >eb in ef ⊢ % >ed >INJb #ed'
        <(grumpydestruct1 ??? ed') //
    ]
| (* samedomain *) >(nextblock_store … STORE) //
| (* domain *) //
| (* range *) /2/
| #b1 #delta1 #INJb1
    >(low_bound_store … STORE b1)
    >(high_bound_store … STORE b1)
    @ms_range_2 //;
] qed.

lemma 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
inversion Hval_shift_a;
[ 1,2,4: #x #H >H in STOREV #H' whd in H':(??%?); @False_ind destruct; ]
#b1 #ofs1 #b2 #ofs2 #delta
whd in ⊢ (??%? → ?); lapply (refl ? (f b1)); elim (f b1) in ⊢ (???% → %);
[#_ #e whd in e:(??%?); destruct; ]
#x #INJb1 #e elim (grumpydestruct2 ?????? e); #eb #ex
>ex in INJb1 #INJb1
#OFS #ea1 #ea2 >ea1 in STOREV #STOREV
lapply (store_within_shift … Hmem_shift STOREV INJb1 Hval_shift_v);
*; #n2 *; #A #B
%{ n2} % //;
>OFS >eb in A
<(?:signed (add ofs1 (repr delta)) = signed ofs1 + delta)
[ #H @H (* XXX /2/ *)
| @(address_shift … chunk … Hmem_shift ? INJb1)
    @(store_valid_access_3 … STOREV)
]
qed.

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

lemma 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 *)
    @free_right_inj [ @free_left_inj //
    | #b1 #delta #chunk #ofs whd in ⊢ (??%? → ?);
        lapply (refl ? (f b1)); elim (f b1) in ⊢ (???% → %);
        [ #_ #e whd in e:(??%?); destruct;
        | #delta' #INJb1 #e whd in e:(??%?); destruct;
            napply valid_access_free_2
        ]
    ]
| (* samedomain *) whd in ⊢ (??%%); //
| (* domain *) >(?:nextblock (free m1 b) = nextblock m1) //
| (* range *) /2/
| #b' #delta #INJb' cases (decidable_eq_Z b' b); #eb
    [ >eb
        >(low_bound_free_same ??) >(high_bound_free_same ??)
        (* arith *) napply daemon
    | >(low_bound_free …) //; >(high_bound_free …) /2/;
    ]
] qed.

(* Relation between shifts and allocation. *)

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

lemma shift_incr_inject_incr:
  ∀f1,f2.
  shift_incr f1 f2 → inject_incr (meminj_of_shift f1) (meminj_of_shift f2).
#f1 #f2 #Hshift whd in ⊢ (?%%); whd; #b
elim (Hshift b); #INJ >INJ /2/;
qed.

lemma 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 whd in ⊢ (% → %);
@val_inject_incr
@shift_incr_inject_incr //;
qed.

(* *
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.
***)

lemma 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
lapply (refl ? (alloc m2 lo2 hi2)); elim (alloc m2 lo2 hi2) in ⊢ (???% → %);
#m2' #b' #ALLOC2
cut (b' = b);
[ >(alloc_result … ALLOC) >(alloc_result … ALLOC2) // ]
#eb >eb
cut (f b = None ?);
[ lapply (ms_domain b); >(alloc_result … ALLOC)
    elim (f (nextblock m1)); //;
    #z (* arith *) napply daemon
]
#FB
letin f' ≝ (λb':block. if eqZb b' b then Some ? delta else f b');
cut (shift_incr f f');
[ whd; #b0 whd in ⊢ (?(???%)?);
    @eqZb_elim /2/; ]
#Hshift_incr
cut (f' b = Some ? delta);
[ whd in ⊢ (??%?); >(eqZb_z_z …) // ] #efb'
%{ f'} %{ m2'} % //; % //; % //; %
[ (* inj *)
    cut (mem_inj val_inject (meminj_of_shift f') m1 m2);
    [ whd; #chunk #b1 #ofs #v1 #b2 #delta2 #MINJf' #LOAD
        cut (meminj_of_shift f b1 = Some ? 〈b2, delta2〉);
        [ <MINJf' whd in ⊢ (???(?%?)); whd in ⊢ (??%%);
            @eqZb_elim //; #eb
            >eb
            cut (valid_block m1 b);
            [ @valid_access_valid_block
              [ 3: @load_valid_access // ]
            ]
            cut (¬valid_block m1 b); [ /2/ ]
            #H #H' @False_ind napply (absurd ? H' H)
        ] #MINJf
        lapply (ms_inj … MINJf LOAD); *; #v2 *; #A #B
        %{ v2} % //;
        @(val_inject_incr … B)
        @shift_incr_inject_incr //
    ] #Hmem_inj
    @(alloc_parallel_inj … delta Hmem_inj ALLOC ALLOC2 ?) /2/;
    whd in ⊢ (??%?); >efb' /2/;
| (* samedomain *)
    >(nextblock_alloc … ALLOC)
    >(nextblock_alloc … ALLOC2)
    //;
| (* domain *)
    #b0 (* FIXME: unfold *) >(refl ? (f' b0):f' b0 = if eqZb b0 b then Some ? delta else f b0)
    >(nextblock_alloc … ALLOC)
    >(alloc_result … ALLOC)
    @eqZb_elim #eb0
    [ >eb0 (* arith *) napply daemon
    | lapply (ms_domain b0); elim (f b0); 
        (* arith *) napply daemon
    ]
| (* range *)
    #b0 #delta0 whd in ⊢ (??%? → ?);
    @eqZb_elim
    [ #_ #e <(grumpydestruct1 ??? e) //
    | #neb #e @(ms_range_1 … b0) @e
    ] 
| #b0 #delta0 whd in ⊢ (??%? → ?);
    >(low_bound_alloc … ALLOC2 ?)
    >(high_bound_alloc … ALLOC2 ?)
    @eqZb_elim #eb0 >eb
    [ >eb0 #ed <(grumpydestruct1 ??? ed)
        >(eqZb_z_z ?) /3/;
    | #edelta0 >(eqZb_false … eb0)
        @ms_range_2 whd in edelta0:(??%?); //; 
    ]
]
qed.
*)*)
(* ** 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. *)

lemma in_bounds_equiv:
  ∀chunk1,chunk2,m,r,b,ofs.∀A:Type[0].∀a1,a2: A.
  typesize chunk1 = typesize chunk2 →
  (match in_bounds m chunk1 r b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]) =
  (match in_bounds m chunk2 r b ofs with [ inl _ ⇒ a1 | inr _ ⇒ a2]).
#chunk1 #chunk2 #m #r #b #ofs #A #a1 #a2 #Hsize
elim (in_bounds m chunk1 r b ofs);
[ #H whd in ⊢ (??%?); >(in_bounds_true … A a1 a2 ?) //;
    @valid_access_compat //;
| #H whd in ⊢ (??%?); elim (in_bounds m chunk2 r b ofs); //;
    #H' @False_ind @(absurd ?? H)
    @valid_access_compat //;
] qed. 

lemma storev_8_signed_unsigned:
  ∀m,a,v.
  storev (ASTint I8 Signed) m a v = storev (ASTint I8 Unsigned) m a v.
#m #a #v whd in ⊢ (??%%); elim a //
#ptr whd in ⊢ (??%%);
>(in_bounds_equiv (ASTint I8 Signed) (ASTint I8 Unsigned) … (option mem) ???) //
qed.

lemma storev_16_signed_unsigned:
  ∀m,a,v.
  storev (ASTint I16 Signed) m a v = storev (ASTint I16 Unsigned) m a v.
#m #a #v whd in ⊢ (??%%); elim a //
#ptr whd in ⊢ (??%%);
>(in_bounds_equiv (ASTint I16 Signed) (ASTint I16 Unsigned) … (option mem) ???) //
qed.

(* 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. *)

(* Nonessential properties that may require arithmetic
lemma loadv_8_signed_unsigned:
  ∀m,a.
  loadv Mint8signed m a = option_map ?? (sign_ext 8) (loadv Mint8unsigned m a).
#m #a whd in ⊢ (??%(????(%))); elim a; //;
#r #b #ofs whd in ⊢ (??%(????%));
>(in_bounds_equiv Mint8signed Mint8unsigned … (option val) ???) //;
elim (in_bounds m Mint8unsigned r b (signed ofs)); /2/;
#H whd in ⊢ (??%%);
elim (getN 0 (signed ofs) (contents (blocks m b))); 
[ 1,3: //;
| #i whd in ⊢ (??(??%)(??%));
    >(sign_ext_zero_ext ?? i) [ @refl (* XXX: // ? *)
    | (* arith *) @daemon
    ]
| #sp cases sp; //; 
]
qed.
*)
*)