val hide
  (#t: inttype { unsigned t })
  (#sec: secrecy_level)
  (x: uint_t t sec)
: Tot (y: uint_t t SEC { v y == v x })
let hide
  #t #sec x
= cast t SEC x
val hide
  (#t: inttype { unsigned t })
  (#sec: secrecy_level)
  (x: uint_t t sec)
: Tot (y: uint_t t SEC { v y == v x })
let hide #t #sec x =
cast t SEC x
QUIC.Secret.Int.fst.checked
QUIC.Secret.Int.Aux.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked
QUIC.Secret.Int.fst
Lib.IntTypes.inttype Prims.b2t Lib.IntTypes.unsigned Lib.IntTypes.secrecy_level Lib.IntTypes.uint_t Lib.IntTypes.cast Lib.IntTypes.SEC Prims.eq2 Lib.IntTypes.range_t QUIC.Secret.Int.Base.v
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
val hide
  (#t: inttype { unsigned t })
  (#sec: secrecy_level)
  (x: uint_t t sec)
: Tot (y: uint_t t SEC { v y == v x })
x: Lib.IntTypes.uint_t t sec
  -> y:
    Lib.IntTypes.uint_t t Lib.IntTypes.SEC {QUIC.Secret.Int.Base.v y == QUIC.Secret.Int.Base.v x}