val mk_int: #t:inttype -> #l:secrecy_level -> n:range_t t -> u:int_t t l{v u == n}
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 mk_int: #t:inttype -> #l:secrecy_level -> n:range_t t -> u:int_t t l{v u == n}
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
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.range_t FStar.UInt8.uint_to_t FStar.UInt16.uint_to_t FStar.UInt32.uint_to_t FStar.UInt64.uint_to_t FStar.UInt128.uint_to_t FStar.Int8.int_to_t FStar.Int16.int_to_t FStar.Int32.int_to_t FStar.Int64.int_to_t FStar.Int128.int_to_t Lib.IntTypes.int_t Prims.eq2 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])]
val mk_int: #t:inttype -> #l:secrecy_level -> n:range_t t -> u:int_t t l{v u == n}
n: Lib.IntTypes.range_t t -> u62: Lib.IntTypes.int_t t l {Lib.IntTypes.v u62 == n}