(* *********************************************************************)
(*                                                                     *)
(*              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. Actually, it is so tiny that
     the functions defined here could be put elsewhere.
*)

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

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

record contentT: Type[1] ≝
 { contentcarr:> Type[0]
 ; undef: contentcarr
 }.

definition contentmap: contentT → Type[0] ≝ λcontent. 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 (content:contentT) : Type[0] ≝ {
  low: Z;
  high: Z;
  contents: contentmap content
}.

(* 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 (content:contentT): Type[0] ≝ {
  blocks: block -> block_contents content;
  nextblock: Z;
  nextblock_pos: OZ < nextblock
}.

(* The initial store. *)

definition oneZ ≝ pos one.

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

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

definition empty: ∀content. mem content ≝
 λcontent.mk_mem content (λx.empty_block content 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:
  ∀content.∀m. OZ < Zsucc (nextblock content m).
#content #m lapply (nextblock_pos … m);normalize;
cases (nextblock … m);//;
#n cases n;//;
qed.

definition alloc : ∀content. mem content → Z → Z → ∀r:region. mem content × Σb:block. block_region b = r ≝
  λcontent,m,lo,hi,r.
  let b ≝ mk_block r (nextblock … m) in
  〈mk_mem content
    (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 ≝
  λcontent,m,b.mk_mem content (update_block … b
                (empty_block … OZ OZ)
                (blocks … m))
        (nextblock … m)
        (nextblock_pos … m).

(* Freeing of a list of blocks. *)

definition free_list ≝
  λcontent,m,l.foldr ?? (λb,m.free content m b) m l.

(* XXX hack for lack of reduction with restricted unfolding *)
lemma unfold_free_list :
 ∀content,m,h,t. free_list content 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 : ∀content. mem content → block → Z ≝
  λcontent,m,b.low … (blocks … m b).
definition high_bound : ∀content. mem content → block → Z ≝ 
  λcontent,m,b.high … (blocks … m b).
definition block_region: ∀content. mem content → block → region ≝
  λcontent,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 : ∀content. mem content → block → Prop ≝
  λcontent,m,b.block_id b < nextblock … m.

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