val reveal
  (#t: inttype { unsigned t })
  (#sec: secrecy_level)
  (x: uint_t t sec)
: GTot (y: uint_t t PUB { v y == v x })
val reveal
  (#t: inttype { unsigned t })
  (#sec: secrecy_level)
  (x: uint_t t sec)
: GTot (y: uint_t t PUB { v y == v x })
let reveal
  #t #sec x
= mk_int #t (v x)
module QUIC.Secret.Int
module Aux = QUIC.Secret.Int.Aux

let usub
  #t #sec x y
= x `sub` y

let cast_up
  #t1 t2 #sec x
= cast t2 SEC x

let cast_down
  #t1 t2 #sec x
= cast t2 SEC x

let hide
  #t #sec x
= cast t SEC x
/
QUIC.Secret.Int.Aux.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked
QUIC.Secret.Int.fst
x: Lib.IntTypes.uint_t t sec
  -> Prims.GTot
    (y:
      Lib.IntTypes.uint_t t Lib.IntTypes.PUB {QUIC.Secret.Int.Base.v y == QUIC.Secret.Int.Base.v x})
Lib.IntTypes.inttype Prims.b2t Lib.IntTypes.unsigned Lib.IntTypes.secrecy_level Lib.IntTypes.uint_t Lib.IntTypes.mk_int Lib.IntTypes.PUB QUIC.Secret.Int.Base.v Prims.eq2 Lib.IntTypes.range_t
let reveal #t #sec x =
  
mk_int #t (v x)