val zeros: t:inttype -> l:secrecy_level -> n:int_t t l{v n = 0}
let zeros t l = mk_int 0
val zeros: t:inttype -> l:secrecy_level -> n:int_t t l{v n = 0}
let zeros t l =
mk_int 0
Lib.IntTypes.fst.checked
prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt128.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Int8.fsti.checked FStar.Int64.fsti.checked FStar.Int32.fsti.checked FStar.Int16.fsti.checked FStar.Int128.fsti.checked FStar.Int.Cast.Full.fst.checked FStar.Int.Cast.fst.checked FStar.Int.fsti.checked FStar.BitVector.fst.checked
Lib.IntTypes.fst
Lib.IntTypes.inttype Lib.IntTypes.secrecy_level Lib.IntTypes.mk_int Lib.IntTypes.int_t Prims.b2t Prims.op_Equality Prims.int Lib.IntTypes.v
module Lib.IntTypes

open FStar.Math.Lemmas

#push-options "--max_fuel 0 --max_ifuel 1 --z3rlimit 200"

let pow2_2 _   = assert_norm (pow2 2 = 4)
let pow2_3 _   = assert_norm (pow2 3 = 8)
let pow2_4 _   = assert_norm (pow2 4 = 16)
let pow2_127 _ = assert_norm (pow2 127 = 0x80000000000000000000000000000000)

let bits_numbytes t = ()

let sec_int_t t = pub_int_t t

let sec_int_v #t u = pub_int_v u

let secret #t x = x

[@(strict_on_arguments [0])]
let mk_int #t #l x =
  match t with
  | U1 -> UInt8.uint_to_t x
  | U8 -> UInt8.uint_to_t x
  | U16 -> UInt16.uint_to_t x
  | U32 -> UInt32.uint_to_t x
  | U64 -> UInt64.uint_to_t x
  | U128 -> UInt128.uint_to_t x
  | S8 -> Int8.int_to_t x
  | S16 -> Int16.int_to_t x
  | S32 -> Int32.int_to_t x
  | S64 -> Int64.int_to_t x
  | S128 -> Int128.int_to_t x

val v_extensionality:
   #t:inttype
 -> #l:secrecy_level
 -> a:int_t t l
 -> b:int_t t l
 -> Lemma
  (requires v a == v b)
  (ensures  a == b)
let v_extensionality #t #l a b =
  match t with
  | U1   -> ()
  | U8   -> UInt8.v_inj a b
  | U16  -> UInt16.v_inj a b
  | U32  -> UInt32.v_inj a b
  | U64  -> UInt64.v_inj a b
  | U128 -> UInt128.v_inj a b
  | S8   -> Int8.v_inj a b
  | S16  -> Int16.v_inj a b
  | S32  -> Int32.v_inj a b
  | S64  -> Int64.v_inj a b
  | S128 -> Int128.v_inj a b

let v_injective #t #l a =
  v_extensionality a (mk_int (v a))

let v_mk_int #t #l n = ()

let u128 n = FStar.UInt128.uint64_to_uint128 (u64 n)

// KaRaMeL will extract this to FStar_Int128_int_to_t, which isn't provided
// We'll need to have FStar.Int128.int64_to_int128 to support int128_t literals
let i128 n =
  assert_norm (pow2 (bits S64 - 1) <= pow2 (bits S128 - 1));
  sint #S128 #SEC n

let size_to_uint32 x = x

let size_to_uint64 x = Int.Cast.uint32_to_uint64 x

let byte_to_uint8 x = x

let byte_to_int8 x = Int.Cast.uint8_to_int8 x

let op_At_Percent = Int.op_At_Percent

// FStar.UInt128 gets special treatment in KaRaMeL. There is no
// equivalent for FStar.Int128 at the moment, so we use the three
// assumed cast operators below.
//
// Using them will fail at runtime with an informative message.
// The commented-out implementations show that they are realizable.
//
// When support for `FStar.Int128` is added KaRaMeL, these casts must
// be added as special cases. When using builtin compiler support for
// `int128_t`, they can be implemented directly as C casts without
// undefined or implementation-defined behaviour.

assume
val uint128_to_int128: a:UInt128.t{v a <= maxint S128} -> b:Int128.t{Int128.v b == UInt128.v a}
//let uint128_to_int128 a = Int128.int_to_t (v a)

assume
val int128_to_uint128: a:Int128.t -> b:UInt128.t{UInt128.v b == Int128.v a % pow2 128}
//let int128_to_uint128 a = mk_int (v a % pow2 128)

assume
val int64_to_int128: a:Int64.t -> b:Int128.t{Int128.v b == Int64.v a}
//let int64_to_int128 a = Int128.int_to_t (v a)

val uint64_to_int128: a:UInt64.t -> b:Int128.t{Int128.v b == UInt64.v a}
let uint64_to_int128 a = uint128_to_int128 (Int.Cast.Full.uint64_to_uint128 a)

val int64_to_uint128: a:Int64.t -> b:UInt128.t{UInt128.v b == Int64.v a % pow2 128}
let int64_to_uint128 a = int128_to_uint128 (int64_to_int128 a)

val int128_to_uint64: a:Int128.t -> b:UInt64.t{UInt64.v b == Int128.v a % pow2 64}
let int128_to_uint64 a = Int.Cast.Full.uint128_to_uint64 (int128_to_uint128 a)

#push-options "--z3rlimit 1000"

[@(strict_on_arguments [0;2])]
let cast #t #l t' l' u =
  assert_norm (pow2 8 = 2 * pow2 7);
  assert_norm (pow2 16 = 2 * pow2 15);
  assert_norm (pow2 64 * pow2 64 = pow2 128);
  assert_norm (pow2 16 * pow2 48 = pow2 64);
  assert_norm (pow2 8 * pow2 56 = pow2 64);
  assert_norm (pow2 32 * pow2 32 = pow2 64);
  modulo_modulo_lemma (v u) (pow2 32) (pow2 32);
  modulo_modulo_lemma (v u) (pow2 64) (pow2 64);
  modulo_modulo_lemma (v u) (pow2 128) (pow2 64);
  modulo_modulo_lemma (v u) (pow2 16) (pow2 48);
  modulo_modulo_lemma (v u) (pow2 8) (pow2 56);
  let open FStar.Int.Cast in
  let open FStar.Int.Cast.Full in
  match t, t' with
  | U1, U1     -> u
  | U1, U8     -> u
  | U1, U16    -> uint8_to_uint16 u
  | U1, U32    -> uint8_to_uint32 u
  | U1, U64    -> uint8_to_uint64 u
  | U1, U128   -> UInt128.uint64_to_uint128 (uint8_to_uint64 u)
  | U1, S8     -> uint8_to_int8 u
  | U1, S16    -> uint8_to_int16 u
  | U1, S32    -> uint8_to_int32 u
  | U1, S64    -> uint8_to_int64 u
  | U1, S128   -> uint64_to_int128 (uint8_to_uint64 u)

  | U8, U1     -> UInt8.rem u 2uy
  | U8, U8     -> u
  | U8, U16    -> uint8_to_uint16 u
  | U8, U32    -> uint8_to_uint32 u
  | U8, U64    -> uint8_to_uint64 u
  | U8, U128   -> UInt128.uint64_to_uint128 (uint8_to_uint64 u)
  | U8, S8     -> uint8_to_int8 u
  | U8, S16    -> uint8_to_int16 u
  | U8, S32    -> uint8_to_int32 u
  | U8, S64    -> uint8_to_int64 u
  | U8, S128   -> uint64_to_int128 (uint8_to_uint64 u)

  | U16, U1    -> UInt8.rem (uint16_to_uint8 u) 2uy
  | U16, U8    -> uint16_to_uint8 u
  | U16, U16   -> u
  | U16, U32   -> uint16_to_uint32 u
  | U16, U64   -> uint16_to_uint64 u
  | U16, U128  -> UInt128.uint64_to_uint128 (uint16_to_uint64 u)
  | U16, S8    -> uint16_to_int8 u
  | U16, S16   -> uint16_to_int16 u
  | U16, S32   -> uint16_to_int32 u
  | U16, S64   -> uint16_to_int64 u
  | U16, S128  -> uint64_to_int128 (uint16_to_uint64 u)

  | U32, U1    -> UInt8.rem (uint32_to_uint8 u) 2uy
  | U32, U8    -> uint32_to_uint8 u
  | U32, U16   -> uint32_to_uint16 u
  | U32, U32   -> u
  | U32, U64   -> uint32_to_uint64 u
  | U32, U128  -> UInt128.uint64_to_uint128 (uint32_to_uint64 u)
  | U32, S8    -> uint32_to_int8 u
  | U32, S16   -> uint32_to_int16 u
  | U32, S32   -> uint32_to_int32 u
  | U32, S64   -> uint32_to_int64 u
  | U32, S128  -> uint64_to_int128 (uint32_to_uint64 u)

  | U64, U1    -> UInt8.rem (uint64_to_uint8 u) 2uy
  | U64, U8    -> uint64_to_uint8 u
  | U64, U16   -> uint64_to_uint16 u
  | U64, U32   -> uint64_to_uint32 u
  | U64, U64   -> u
  | U64, U128  -> UInt128.uint64_to_uint128 u
  | U64, S8    -> uint64_to_int8 u
  | U64, S16   -> uint64_to_int16 u
  | U64, S32   -> uint64_to_int32 u
  | U64, S64   -> uint64_to_int64 u
  | U64, S128  -> uint64_to_int128 u

  | U128, U1   -> UInt8.rem (uint64_to_uint8 (uint128_to_uint64 u)) 2uy
  | U128, U8   -> uint64_to_uint8 (UInt128.uint128_to_uint64 u)
  | U128, U16  -> uint64_to_uint16 (UInt128.uint128_to_uint64 u)
  | U128, U32  -> uint64_to_uint32 (UInt128.uint128_to_uint64 u)
  | U128, U64  -> UInt128.uint128_to_uint64 u
  | U128, U128 -> u
  | U128, S8   -> uint64_to_int8 (UInt128.uint128_to_uint64 u)
  | U128, S16  -> uint64_to_int16 (UInt128.uint128_to_uint64 u)
  | U128, S32  -> uint64_to_int32 (UInt128.uint128_to_uint64 u)
  | U128, S64  -> uint64_to_int64 (UInt128.uint128_to_uint64 u)
  | U128, S128 -> uint128_to_int128 u

  | S8, U1     -> UInt8.rem (int8_to_uint8 u) 2uy
  | S8, U8     -> int8_to_uint8 u
  | S8, U16    -> int8_to_uint16 u
  | S8, U32    -> int8_to_uint32 u
  | S8, U64    -> int8_to_uint64 u
  | S8, U128   -> int64_to_uint128 (int8_to_int64 u)
  | S8, S8     -> u
  | S8, S16    -> int8_to_int16 u
  | S8, S32    -> int8_to_int32 u
  | S8, S64    -> int8_to_int64 u
  | S8, S128   -> int64_to_int128 (int8_to_int64 u)

  | S16, U1    -> UInt8.rem (int16_to_uint8 u) 2uy
  | S16, U8    -> int16_to_uint8 u
  | S16, U16   -> int16_to_uint16 u
  | S16, U32   -> int16_to_uint32 u
  | S16, U64   -> int16_to_uint64 u
  | S16, U128  -> int64_to_uint128 (int16_to_int64 u)
  | S16, S8    -> int16_to_int8 u
  | S16, S16   -> u
  | S16, S32   -> int16_to_int32 u
  | S16, S64   -> int16_to_int64 u
  | S16, S128  -> int64_to_int128 (int16_to_int64 u)

  | S32, U1    -> UInt8.rem (int32_to_uint8 u) 2uy
  | S32, U8    -> int32_to_uint8 u
  | S32, U16   -> int32_to_uint16 u
  | S32, U32   -> int32_to_uint32 u
  | S32, U64   -> int32_to_uint64 u
  | S32, U128  -> int64_to_uint128 (int32_to_int64 u)
  | S32, S8    -> int32_to_int8 u
  | S32, S16   -> int32_to_int16 u
  | S32, S32   -> u
  | S32, S64   -> int32_to_int64 u
  | S32, S128  -> int64_to_int128 (int32_to_int64 u)

  | S64, U1    -> UInt8.rem (int64_to_uint8 u) 2uy
  | S64, U8    -> int64_to_uint8 u
  | S64, U16   -> int64_to_uint16 u
  | S64, U32   -> int64_to_uint32 u
  | S64, U64   -> int64_to_uint64 u
  | S64, U128  -> int64_to_uint128 u
  | S64, S8    -> int64_to_int8 u
  | S64, S16   -> int64_to_int16 u
  | S64, S32   -> int64_to_int32 u
  | S64, S64   -> u
  | S64, S128  -> int64_to_int128 u

  | S128, U1    -> UInt8.rem (uint64_to_uint8 (int128_to_uint64 u)) 2uy
  | S128, U8    -> uint64_to_uint8 (int128_to_uint64 u)
  | S128, U16   -> uint64_to_uint16 (int128_to_uint64 u)
  | S128, U32   -> uint64_to_uint32 (int128_to_uint64 u)
  | S128, U64   -> int128_to_uint64 u
  | S128, U128  -> int128_to_uint128 u
  | S128, S8    -> uint64_to_int8  (int128_to_uint64 u)
  | S128, S16   -> uint64_to_int16 (int128_to_uint64 u)
  | S128, S32   -> uint64_to_int32 (int128_to_uint64 u)
  | S128, S64   -> uint64_to_int64 (int128_to_uint64 u)
  | S128, S128  -> u

#pop-options

[@(strict_on_arguments [0])]
let ones t l =
  match t with
  | U1  -> 0x1uy
  | U8  -> 0xFFuy
  | U16 -> 0xFFFFus
  | U32 -> 0xFFFFFFFFul
  | U64 -> 0xFFFFFFFFFFFFFFFFuL
  | U128 ->
    let x = UInt128.uint64_to_uint128 0xFFFFFFFFFFFFFFFFuL in
    let y = (UInt128.shift_left x 64ul) `UInt128.add` x in
    assert_norm (UInt128.v y == pow2 128 - 1);
    y
  | _ -> mk_int (-1)
val zeros: t:inttype -> l:secrecy_level -> n:int_t t l{v n = 0}
t: Lib.IntTypes.inttype -> l: Lib.IntTypes.secrecy_level
  -> n: Lib.IntTypes.int_t t l {Lib.IntTypes.v n = 0}