prelude.mlw

(* Why3 Logical Types *)
module Mapping
  let function from_fn (f : 'a -> 'b) : ('a -> 'b) = f
end

module Seq
  use export seq.Seq

  function to_owned (a : 'a) : 'a = a
end

module Int
  use export mach.int.Int
end

(* Rust primitive types *)

module Opaque
  type opaque_ptr
  type dyn
  type foreign
end

module Bool
  let eqb (a : bool) (b : bool) : bool =
    ensures { result <-> a = b  }
    match a, b with
    | True, True -> True
    | False, False -> True
    | _ -> False
    end

  let neqb (a : bool) (b : bool) : bool =
    ensures { result <-> a <> b  }
    not (eqb a b)

  let to_int (b : bool) : int =
    if b then 1 else 0

  use int.Int

  let of_int (i : int) : bool =
    i = 1
end
module Borrow
  type borrowed 'a = { current : 'a; final : 'a; id : int }
  let function ( *_ ) x = x.current
  let function ( ^_ ) x = x.final
  let function get_id (x : borrowed 'a) = x.id
  let function borrow_logic (cur fin : 'a) (id : int) = { current = cur; final = fin; id = id; }
  val borrow_mut (a : 'a) : borrowed 'a
    ensures { *result = a }
  val function inherit_id (old_id inherit_path: int) : int
  val borrow_final (a: 'a) (id: int) : borrowed 'a
    ensures { *result = a }
    ensures { result.id = id }
end

module Real


end

(* Signed Integer *)
module IntSize
  use export mach.int.Int64
  type isize = int64
end
module Int8
  use int.Int

  type int8 = < range -0x80 0x7f >

  let constant min_int8 : int = - 0x80
  let constant max_int8 : int =   0x7f
  function to_int (x : int8) : int = int8'int x

  clone export mach.int.Bounded_int with
    type t = int8,
    constant min = int8'minInt,
    constant max = int8'maxInt,
    function to_int = int8'int,
    lemma to_int_in_bounds,
    lemma extensionality
end
module Int16
  use int.Int

  type int16 = < range -0x8000 0x7fff >

  let constant min_int16 : int = - 0x8000
  let constant max_int16 : int =   0x7fff
  function to_int (x : int16) : int = int16'int x

  clone export mach.int.Bounded_int with
    type t = int16,
    constant min = int16'minInt,
    constant max = int16'maxInt,
    function to_int = int16'int,
    lemma to_int_in_bounds,
    lemma extensionality
end
module Int32
  use export mach.int.Int32
end
module Int64
  use export mach.int.Int64
end
module Int128
  use int.Int

  type int128 = < range -0x80000000000000000000000000000000 0x7fffffffffffffffffffffffffffffff >

  let constant min_int128 : int = - 0x80000000000000000000000000000000
  let constant max_int128 : int =   0x7fffffffffffffffffffffffffffffff
  function to_int (x : int128) : int = int128'int x

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

(* Unsigned Integers *)
module UIntSize
  use export mach.int.UInt64
  type usize = uint64
end
module UInt8
  use int.Int

  type uint8 = < range 0x0 0xff >

  let constant min_uint8 : int =  0x00
  let constant max_uint8 : int =  0xff
  function to_int (x : uint8) : int = uint8'int x

  clone export mach.int.Bounded_int with
    type t = uint8,
    constant min = uint8'minInt,
    constant max = uint8'maxInt,
    function to_int = uint8'int,
    lemma to_int_in_bounds,
    lemma extensionality
end
module UInt16
  use int.Int

  type uint16 = < range 0x0 0xffff >

  let constant min_uint16 : int =  0x00
  let constant max_uint16 : int =  0xffff
  function to_int (x : uint16) : int = uint16'int x

  clone export mach.int.Bounded_int with
    type t = uint16,
    constant min = uint16'minInt,
    constant max = uint16'maxInt,
    function to_int = uint16'int,
    lemma to_int_in_bounds,
    lemma extensionality
end
module UInt32
  use export mach.int.UInt32
end
module UInt64
  use export mach.int.UInt64
end
module UInt128
  use int.Int

  type uint128 = < range 0x0 0xffffffffffffffffffffffffffffffff >

  let constant min_uint128 : int =  0x00000000000000000000000000000000
  let constant max_uint128 : int =  0xffffffffffffffffffffffffffffffff
  function to_int (x : uint128) : int = uint128'int x

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

(* Floats *)
module Float32
  use export ieee_float.Float32
end
module Float64
  use export ieee_float.Float64
end

module Char
  (* utf8 characters (not glyphs)
      highly restricted until Why3 supports Unicode strings
  *)
  use int.Int

  type char

  function code char : int

  axiom code: forall c. 0 <= code c < 0x10FFFF

  val function chr (n: int) : char

  axiom code_chr: forall n. 0 <= n < 0x10FFFF -> code (chr n) = n

  axiom chr_code: forall c. chr (code c) = c
end

module Snapshot
  type snap_ty 't
  val function new (Snapshot x : 't) : snap_ty 't
  val function inner (x : snap_ty 't) : 't
  axiom new_spec: forall x: 't [new x]. inner (new x) = x
  axiom inner_spec: forall x: snap_ty 't [inner x]. new (inner x) = x
end

module Slice
  use seq.Seq
  use UIntSize
  use int.Int

  type slice 'a =
    { elts : seq 'a }
    invariant { Seq.length elts <= max_uint64 }
  axiom slice_ext :
    forall x y: slice 'a. x.elts = y.elts -> x = y

  type array 'a = slice 'a

  let create (len : uint64) (f : int -> 'a) : slice 'a =
    { elts = Seq.create (to_int len) f}

  let function length (s : slice 'a) : uint64 = of_int (Seq.length s.elts)

  let function get (s : slice 'a) (ix : uint64) : 'a =
    requires { ix < Seq.length s.elts }
    Seq.get s.elts (to_int ix)

  let set (s : slice 'a) (ix : uint64) (v : 'a) : slice 'a =
    requires { 0 <= ix < Seq.length s.elts }
    ensures { Seq.length result.elts = Seq.length s.elts }
    ensures { result.elts[ix] = v }
    ensures { forall j. 0 <= j < Seq.length s.elts /\ j <> ix -> result.elts[j] = s.elts[j] }
    { elts = Seq.set s.elts (to_int ix) v }

  function id (s : slice 'a) : seq 'a = s.elts
end