(* *********************************************************************)
(*                                                                     *)
(*              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 describes the part of the memory model that is in common
     between the front-end and the back-end.
*)

include "utilities/extralib.ma".
include "common/Pointers.ma".
include "common/ByteValues.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.

(***************************************)

definition contentmap: Type[0] ≝ Z → beval.

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

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

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).
#m lapply (nextblock_pos … m);normalize;
cases (nextblock … m);//;
#n cases n;//;
qed.

definition alloc : mem → Z → Z → ∀r:region. mem × Σb:block. block_region b = r ≝
  λ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〉.
% qed.

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


(* This function should be moved to common/GenMem.ma and replaces in_bounds *)
definition do_if_in_bounds:
 ∀A:Type[0]. mem → pointer → (block → block_contents → Z → A) → option A ≝
 λS,m,ptr,F.
  let b ≝ pblock ptr in
  if Zltb (block_id b) (nextblock … m) then
   let content ≝ blocks … m b in
   let off ≝ offv (poff ptr) in
   if andb (Zleb (low … content) off) (Zleb off (high … content)) then
    Some … (F b content off)
   else
    None ?
  else
   None ?.

definition beloadv: ∀m:mem. ∀ptr:pointer. option beval ≝
 λm,ptr. do_if_in_bounds … m ptr (λb,content,off. contents … content off).

definition bestorev: ∀m:mem. ∀ptr:pointer. beval → option mem ≝
 λm,ptr,v. do_if_in_bounds … m ptr
  (λb,content,off.
    let contents ≝ update … off v (contents … content) in
    let content ≝ mk_block_contents (low … content) (high … content) contents in
    let blocks ≝ update_block … b content (blocks … m) in
     mk_mem … blocks (nextblock … m) (nextblock_pos … m)).