val protected_bits_pn_length (is_short: bool) (pb: bitfield (if is_short then 5 else 4))
    : Tot PN.packet_number_length_t
val protected_bits_pn_length (is_short: bool) (pb: bitfield (if is_short then 5 else 4))
    : Tot PN.packet_number_length_t
let protected_bits_pn_length
  (is_short: bool)
  (pb: bitfield (if is_short then 5 else 4))
: Tot PN.packet_number_length_t
= Secret.to_u32 #Secret.U8 (1uy `Secret.add` Secret.get_bitfield #Secret.U8 pb 0ul 2ul)
module QUIC.Spec.Header.Parse

module PN = QUIC.Spec.PacketNumber
module Public = QUIC.Spec.Header.Public
module LP = LowParse.Spec.Combinators
module Secret = QUIC.Secret.Int
module BF = LowParse.BitFields
module U8 = FStar.UInt8
module Seq = QUIC.Secret.Seq
module U64 = FStar.UInt64
module Cast = FStar.Int.Cast
/
QUIC.Spec.PacketNumber.fsti.checked QUIC.Spec.Header.Public.fsti.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Int.fsti.checked prims.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.BitFields.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Int.Cast.fst.checked
QUIC.Spec.Header.Parse.fst

    is_short: Prims.bool ->
    pb:
      QUIC.Spec.Base.bitfield (match is_short with
          | true -> 5
          | _ -> 4)
  -> QUIC.Spec.PacketNumber.Base.packet_number_length_t
Prims.bool QUIC.Spec.Base.bitfield Prims.nat Prims.b2t Prims.op_LessThanOrEqual Lib.IntTypes.to_u32 Lib.IntTypes.U8 Lib.IntTypes.PUB Lib.IntTypes.add FStar.UInt8.__uint_to_t QUIC.Secret.Int.get_bitfield FStar.UInt32.__uint_to_t QUIC.Spec.PacketNumber.Base.packet_number_length_t
let protected_bits_pn_length (is_short: bool) (pb: bitfield (if is_short then 5 else 4))
    : Tot PN.packet_number_length_t =
  
Secret.to_u32 #Secret.U8 (1uy `Secret.add` (Secret.get_bitfield #Secret.U8 pb 0ul 2ul))