val cast_down
  (#t1: inttype { unsigned t1 })
  (t2: inttype { unsigned t2 })
  (#sec: secrecy_level)
  (x: uint_t t1 sec { v x < pow2 (bits t2) } )
: Tot (y: uint_t t2 SEC { v y == v x })
let cast_down
  #t1 t2 #sec x
= cast t2 SEC x
val cast_down
  (#t1: inttype { unsigned t1 })
  (t2: inttype { unsigned t2 })
  (#sec: secrecy_level)
  (x: uint_t t1 sec { v x < pow2 (bits t2) } )
: Tot (y: uint_t t2 SEC { v y == v x })
let cast_down #t1 t2 #sec x =
cast t2 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 Prims.op_LessThan QUIC.Secret.Int.Base.v Prims.pow2 Lib.IntTypes.bits Lib.IntTypes.cast Lib.IntTypes.SEC Prims.eq2 Prims.int Prims.l_or Lib.IntTypes.range
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
val cast_down
  (#t1: inttype { unsigned t1 })
  (t2: inttype { unsigned t2 })
  (#sec: secrecy_level)
  (x: uint_t t1 sec { v x < pow2 (bits t2) } )
: Tot (y: uint_t t2 SEC { v y == v x })

    t2: Lib.IntTypes.inttype{Lib.IntTypes.unsigned t2} ->
    x: Lib.IntTypes.uint_t t1 sec {QUIC.Secret.Int.Base.v x < Prims.pow2 (Lib.IntTypes.bits t2)}
  -> y:
    Lib.IntTypes.uint_t t2 Lib.IntTypes.SEC {QUIC.Secret.Int.Base.v y == QUIC.Secret.Int.Base.v x}