val secret: #t:inttype -> x:int_t t PUB -> y:int_t t SEC{v x == v y}
let secret #t x = x
val secret: #t:inttype -> x:int_t t PUB -> y:int_t t SEC{v x == v y}
let secret #t x =
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.int_t Lib.IntTypes.PUB Lib.IntTypes.SEC Prims.eq2 Lib.IntTypes.range_t 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
val secret: #t:inttype -> x:int_t t PUB -> y:int_t t SEC{v x == v y}
x: Lib.IntTypes.int_t t Lib.IntTypes.PUB
  -> y: Lib.IntTypes.int_t t Lib.IntTypes.SEC {Lib.IntTypes.v x == Lib.IntTypes.v y}