(** {1 A lightweight memory model dedicated to extraction to C code} *)

module C

  use mach.int.Unsigned
  use mach.int.Int32
  use mach.int.UInt32GMP as UInt32
  use array.Array
  use map.Map
  use int.Int
  predicate in_us_bounds (n:int) = 0 <= n <= UInt32.max_uint32
  predicate in_bounds (n:int) = min_int32 <= n <= max_int32
  use ref.Ref

  type zone

  constant null_zone : zone

  (** The pointer type *)
  type ptr 'a = abstract {
    mutable data : array 'a ;
    offset : int ;
    mutable min : int ;
    mutable max : int ;
    writable : bool;
    zone : zone ;
  }

  let ghost function plength (p:ptr 'a) : int
  = p.data.length

  let ghost function pelts (p:ptr 'a) : int -> 'a
  = p.data.elts

  (** the NULL pointer *)
  val null () : ptr 'a
    ensures { result.zone = null_zone }

  val predicate is_not_null (p:ptr 'a) : bool
    ensures { result <-> p.zone <> null_zone }

  (** pointer incrementation *)
  val incr (p:ptr 'a) (ofs:int32) : ptr 'a
    requires { p.min <= p.offset + ofs <= p.max }
    ensures { result.offset = p.offset + ofs }
    ensures { plength result = plength p }
    ensures { pelts result = pelts p }
    ensures { result.data = p.data }
    ensures { result.min = p.min }
    ensures { result.max = p.max }
    ensures { result.zone = p.zone }
    ensures { result.writable = p.writable }
    alias { p.data with result.data }

  (** pointer dereference *)
  val get (p:ptr 'a) : 'a
    requires { p.min <= p.offset < p.max }
    ensures { result = (pelts p)[p.offset] }

  (** pointer dereference with offset *)
  let get_ofs (p:ptr 'a) (ofs:int32) : 'a
    requires { p.min <= p.offset + ofs < p.max }
    ensures { result = (pelts p)[p.offset + ofs] }
  = get (incr p ofs)

  (** pointer assignment *)
  val set (p:ptr 'a) (v:'a) : unit
    requires { p.min <= p.offset < p.max }
    requires { writable p }
    ensures { pelts p = Map.set (pelts (old p)) p.offset v }
    writes { p.data.elts }

  (** pointer assignment with offset *)
  let set_ofs (p:ptr 'a) (ofs:int32) (v:'a) : unit
    requires { p.min <= p.offset + ofs < p.max }
    requires { writable p }
    ensures { pelts p = Map.set (pelts (old p))
              (p.offset + ofs) v }
    ensures { (pelts p)[p.offset + ofs] = v }
    writes { p.data.elts }
 =
    set (incr p ofs) v

  predicate valid_ptr_shift (p:ptr 'a) (i:int) =
    p.min <= p.offset + i < p.max

  predicate valid (p:ptr 'a) (sz:int) =
    in_bounds sz /\ 0 <= sz /\ 0 <= p.min <= p.offset
    /\ p.offset + sz <= p.max <= plength p

  let lemma valid_itv_to_shift (p:ptr 'a) (sz:int)
    requires { valid p sz }
    ensures { forall i. 0 <= i < sz -> valid_ptr_shift p i }
  = ()


  (** {2 basic C functions for memory handling} *)

  val malloc (sz:UInt32.uint32) : ptr 'a
    requires { 0 <= sz }
    ensures { result.zone <> null_zone -> plength result = sz }
    ensures { result.offset = 0 }
    ensures { result.min = 0 }
    ensures { result.max = plength result }
    ensures { writable result }

  val partial c_assert (e:bool) : unit
    ensures { e }

  let partial salloc sz
    requires { 0 <= sz }
    ensures { plength result = sz }
    ensures { result.offset = 0 }
    ensures { result.min = 0 }
    ensures { result.max = sz }
    ensures { writable result }
  = let p = malloc sz in
    c_assert (is_not_null p);
    p

  val free (p:ptr 'a) : unit
    requires { p.offset = 0 }
    requires { p.min = 0 }
    requires { p.max = plength p }
    requires { writable p }
    writes { p }
    writes { p.data }

  let sfree p
    requires { p.offset = 0 }
    requires { p.min = 0 }
    requires { p.max = plength p }
    requires { writable p }
    writes { p }
    writes { p.data }
  = free p

  val realloc (p:ptr 'a) (sz:int32) : ptr 'a
    requires { 0 <= sz }
    requires { p.offset = 0 }
    requires { p.min = 0 }
    requires { p.max = plength p }
    requires { plength p > 0 }
    requires { writable p }
    writes { p }
    writes { p.data }
    ensures { writable result }
    ensures { result.zone <> null_zone -> result.min = 0 }
    ensures { result.zone <> null_zone -> result.max = plength result }
    ensures { result.offset = 0 }
    ensures { result.zone <> null_zone -> plength result = sz }
    ensures { result.zone <> null_zone ->
                forall i:int. 0 <= i < plength (old p) /\ i < sz ->
                  (pelts result)[i] = (pelts (old p))[i] }
    ensures { result.zone = null_zone -> p = old p }

  val incr_split (p:ptr 'a) (i:int32) : ptr 'a
    requires { 0 <= i }
    requires { p.min <= p.offset + i <= p.max }
    requires { writable p }
    writes   { p.max }
    writes   { p.data }
    ensures  { writable result }
    ensures  { result.offset = p.offset + i }
    ensures  { p.max = p.offset + i }
    ensures  { result.min = p.offset + i }
    ensures  { result.max = old p.max }
    ensures  { result.zone = p.zone }
    ensures  { pelts p = old pelts p }
    ensures  { plength p = old plength p }
    ensures  { pelts result = old pelts p }
    ensures  { plength result = old plength p }
    (* NOT alias result.data old p.data *)

  val join (p1 p2: ptr 'a) : unit
    requires { p1.zone = p2.zone }
    requires { p1.max = p2.min }
    requires { writable p1 /\ writable p2 }
    writes   { p1.max }
    writes   { p1.data.elts }
    writes   { p2 }
    writes   { p2.data }
    ensures  { p1.max = old p2.max }
    ensures  { plength p1 = old plength p1 }
    ensures  { forall i. old p1.min <= i < old p1.max ->
                         (pelts p1)[i] = old (pelts p1)[i] }
    ensures  { forall i. old p2.min <= i < old p2.max ->
                         (pelts p1)[i] = old (pelts p2)[i] }

  val decr_split (p:ptr 'a) (i:int32) : ptr 'a
    requires { 0 <= i }
    requires { p.min <= p.offset - i <= p.max }
    requires { writable p }
    writes   { p.min }
    writes   { p.data }
    ensures  { writable result }
    ensures  { result.offset = p.offset - i }
    ensures  { p.min = p.offset - i }
    ensures  { result.min = old p.min }
    ensures  { result.max = p.offset - i }
    ensures  { result.zone = p.zone }
    ensures  { pelts p = old pelts p }
    ensures  { plength p = old plength p }
    ensures  { pelts result = old pelts p }
    ensures  { plength result = old plength p }
    (* NOT alias result.data old p.data *)

  val join_r (p1 p2: ptr 'a) : unit
    requires { p1.zone = p2.zone }
    requires { p1.max = p2.min }
    requires { writable p1 /\ writable p2 }
    writes   { p1 }
    writes   { p1.data }
    writes   { p2.min }
    writes   { p2.data.elts }
    ensures  { p2.min = old p1.min }
    ensures  { plength p2 = old plength p2 }
    ensures  { forall i. old p1.min <= i < old p1.max ->
                         (pelts p2)[i] = old (pelts p1)[i] }
    ensures  { forall i. old p2.min <= i < old p2.max ->
                         (pelts p2)[i] = old (pelts p2)[i] }

  (** {2 Printing} *)

  val print_space () : unit
  val print_newline () : unit

  val print_uint32 (n:UInt32.uint32):unit

end

module String [@W:non_conservative_extension:N]

  use int.Int
  use mach.int.Int32
  use string.String
  use string.Char

  meta coercion function code

  val code (c:char) : int32
    ensures { result = code c }

  val (=) (c1 c2:char) : bool
    ensures { result <-> c1 = c2 }

  val get (s:string) (i:int32) : char
    requires { 0 <= i <= length s }
    ensures  { 0 <= i < length s -> result = (get s i) }
    ensures  { i = length s -> result = chr 0 }

  val constant zero_char : char
    ensures { code result = 0 }

  val constant zero_num : char
    ensures { result = get "0" 0 }

  val constant nine_num : char
    ensures { result = get "9" 0 }

  val constant minus_char : char
    ensures { result = Char.get "-" 0 }

  val constant small_a : char
    ensures { result = Char.get "a" 0 }

  val constant small_z : char
    ensures { result = Char.get "z" 0 }

  val constant big_a : char
    ensures { result = Char.get "A" 0 }

  val constant big_z : char
    ensures { result = Char.get "Z" 0 }

  constant digitstring : string = "0123456789"
  constant lowstring : string = "abcdefghijklmnopqrstuvwxyz"
  constant upstring : string = "ABCDEFGHIJKLMNOPQRSTUVWXYZ"

  axiom numcodes:
        forall i. 0 <= i < 10 ->
               code (get digitstring i) = code (get "0" 0) + i

  axiom lowcodes:
        forall i. 0 <= i < 26 ->
               code (get lowstring i)
               = code (get "a" 0) + i

  axiom upcodes:
        forall i. 0 <= i < 26 ->
               code (get upstring i)
               = code (get "A" 0) + i

  axiom code_0: code (get "0" 0) = 48
  axiom code_a: code (get "a" 0) = 97
  axiom code_A: code (get "A" 0) = 65
  axiom code_minus : code minus_char = 45

  use C
  use map.Map

  function strlen (s:map int char) (ofs:int) : int

  axiom strlen_def:
    forall s ofs i. 0 <= i
    -> (forall j. 0 <= j < i -> code s[ofs + j] <> 0)
    -> code s[ofs + i] = 0
    -> strlen s ofs = i

  axiom strlen_invalid:
    forall s ofs. (forall i. 0 <= i -> code s[ofs + i] <> 0) -> strlen s ofs < 0

  predicate valid_string (p: ptr char)
    = strlen (pelts p) (offset p) >= 0
      /\ valid p (1 + strlen (pelts p) (offset p))

  use mach.int.UInt32

  val length (s: string) : uint32
    ensures { result = String.length s }

  val strlen (p: ptr char) : uint32
    requires { valid_string p }
    ensures  { result = strlen (pelts p) (offset p) }

end

module StrlenLemmas

  use int.Int
  use string.Char
  use map.Map
  use String

  let rec lemma strlen_before_null (s: map int char) (ofs i:int)
    requires { 0 <= i < strlen s ofs }
    ensures { s[ofs + i] <> 0 }
    variant { i }
  =
    for j = 0 to i-1 do
      invariant { forall k. 0 <= k < j -> s[ofs + k] <> 0 }
      strlen_before_null s ofs j
    done;
    assert { forall j. 0 <= j < i -> s[ofs + j] <> 0 }

  let lemma strlen_at_null (s: map int char) (ofs:int)
    requires { 0 <= strlen s ofs }
    ensures  { s[ofs + strlen s ofs] = 0 }
  =
    let rec lemma aux (i:int)
      requires { strlen s ofs <= i }
      requires { s[ofs + i] = 0 }
      ensures  { s[ofs + strlen s ofs] = 0 }
      variant  { i }
    =
      if pure { strlen s ofs } = i then ()
      else begin
        let j = any int ensures { 0 <= result < i /\ s[ofs + result] = 0 } in
        aux j
      end in
    (* Why3 checks that this exists *)
    let i = any int ensures { 0 <= result /\ s[ofs + result] = 0 } in
    if i < pure { strlen s ofs } then begin
      strlen_before_null s ofs i;
      absurd
    end else aux i

  lemma strlen_not_0: forall s ofs i. 0 <= i < strlen s ofs
                                      -> s[ofs + i] <> 0
                                      -> i < strlen s ofs

  lemma strlen_0: forall s ofs i.
                      0 <= i < strlen s ofs
                      -> s[ofs + i] = 0
                      -> i = strlen s ofs

  let lemma strlen_sup (s: map int char) (ofs i:int)
    requires { 0 <= i }
    requires { s[ofs + i] = 0 }
    ensures  { 0 <= strlen s ofs <= i }
  =
    if pure { strlen s ofs } > i
    then begin
      strlen_before_null s ofs i;
      absurd
    end;
    for j = 0 to (i-1) do
      invariant { forall k. 0 <= k < j -> s[ofs + k] <> 0 }
      if s[ofs + j] = zero_char
      then begin
        assert { 0 <= strlen s ofs = j <= i };
        return
      end
    done;
    assert { strlen s ofs = i }

end

module SChar

  type schar = < range -128 127 >
  let constant min_char : int = -128
  let constant max_char : int = 127
  function to_int (x:schar) : int = schar'int x

  clone export mach.int.Bounded_int with
    type t = schar,
    constant min = schar'minInt,
    constant max = schar'maxInt,
    function to_int = schar'int,
    lemma to_int_in_bounds,
    lemma extensionality

end

module UChar

  type uchar = < range 0 255 >

  let constant max_uchar : int = 255
  function to_int (x:uchar) : int = uchar'int x
  let constant length : int = 8
  let constant radix : int = 256

  clone export mach.int.Unsigned with
    type t = uchar,
    constant max = uchar'maxInt,
    constant radix = radix,
    goal radix_def,
    function to_int = uchar'int,
    lemma zero_unsigned_is_zero,
    lemma to_int_in_bounds,
    lemma extensionality

  use int.Int
  use mach.int.UInt64

  val of_uint64 (x:uint64) : uchar
    requires { 0 <= x <= 255 }
    ensures  { result = to_int x }

  val to_uint64 (x:uchar) : uint64
    ensures  { to_int result = x }

  use mach.int.Int32

  val of_int32 (x:int32) : uchar
    requires { 0 <= x <= 255 }
    ensures  { result = to_int x }

  val to_int32 (x:uchar) : int32
    ensures  { to_int result = x }

  use string.Char
  use map.Map

  (* char can be signed or unsigned *)
  val function of_char (x:char) : uchar
    ensures { 0 <= code x <= 127 -> result = code x }

  val function to_char (x:uchar) : char
    ensures { 0 <= x <= 127 -> code result = x }


  (* cast to and from char* *)

  use C

  type cast_mem = abstract { mi: int; ma: int; z: zone; l: int;
                             mutable ok: bool }

  val open_from_charptr (x: ptr char) : (nx: ptr uchar, ghost mem: cast_mem)
    requires { writable x }
    writes   { x }
    ensures  { min nx = old min x = mem.mi }
    ensures  { max nx = old max x = mem.ma }
    ensures  { old zone x = mem.z }
    ensures  { plength nx = old plength x = mem.l }
    ensures  { mem.ok }
    ensures  { nx.offset = old x.offset }
    ensures  { forall i. 0 <= i < old plength x
               -> (pelts nx)[i] = of_char (old pelts x)[i] }
    ensures  { writable nx }

  val close_from_charptr (x:ptr char) (nx:ptr uchar) (ghost mem:cast_mem) : unit
    requires { mem.ok }
    requires { mem.z = x.zone }
    requires { mem.mi = nx.min }
    requires { mem.ma = nx.max }
    requires { x.offset = nx.offset }
    requires { plength nx = mem.l }
    writes   { x, nx, mem.ok }
    ensures  { x.min = mem.mi /\ x.max = mem.ma }
    ensures  { forall i. 0 <= i < plength x
               -> (pelts x)[i] = to_char (old pelts nx)[i] }
    ensures  { plength x = old plength nx }

end