val mk_short_protected_bits
      (reserved_bits: bitfield 2)
      (key_phase: bool)
      (pnl: PN.packet_number_length_t)
    : GTot (bitfield 5)
let mk_short_protected_bits
  (reserved_bits: bitfield 2)
  (key_phase: bool)
  (pnl: PN.packet_number_length_t)
: GTot (bitfield 5)
= BF.set_bitfield_bound #8 0 5 0 2 (Secret.v pnl - 1);
  BF.set_bitfield_bound #8 (BF.set_bitfield #8 0 0 2 (Secret.v pnl - 1)) 5 2 3 (if key_phase then 1 else 0);
  BF.set_bitfield_bound #8 (BF.set_bitfield #8 (BF.set_bitfield #8 0 0 2 (Secret.v pnl - 1)) 2 3 (if key_phase then 1 else 0)) 5 3 5 (U8.v reserved_bits);
  BF.uint8.BF.set_bitfield (BF.uint8.BF.set_bitfield (BF.uint8.BF.set_bitfield 0uy 0 2 (U8.uint_to_t (Secret.v pnl - 1))) 2 3 (if key_phase then 1uy else 0uy)) 3 5 reserved_bits
val mk_short_protected_bits
      (reserved_bits: bitfield 2)
      (key_phase: bool)
      (pnl: PN.packet_number_length_t)
    : GTot (bitfield 5)
let mk_short_protected_bits
      (reserved_bits: bitfield 2)
      (key_phase: bool)
      (pnl: PN.packet_number_length_t)
    : GTot (bitfield 5) =
BF.set_bitfield_bound #8 0 5 0 2 (Secret.v pnl - 1);
BF.set_bitfield_bound #8
  (BF.set_bitfield #8 0 0 2 (Secret.v pnl - 1))
  5
  2
  3
  (if key_phase then 1 else 0);
BF.set_bitfield_bound #8
  (BF.set_bitfield #8 (BF.set_bitfield #8 0 0 2 (Secret.v pnl - 1)) 2 3 (if key_phase then 1 else 0)
  )
  5
  3
  5
  (U8.v reserved_bits);
BF.uint8.BF.set_bitfield (BF.uint8.BF.set_bitfield (BF.uint8.BF.set_bitfield 0uy
          0
          2
          (U8.uint_to_t (Secret.v pnl - 1)))
      2
      3
      (if key_phase then 1uy else 0uy))
  3
  5
  reserved_bits
QUIC.Spec.Header.Parse.fst.checked
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
QUIC.Spec.Base.bitfield Prims.bool QUIC.Spec.PacketNumber.Base.packet_number_length_t LowParse.BitFields.__proj__Mkuint_t__item__set_bitfield FStar.UInt8.t LowParse.BitFields.uint8 FStar.UInt8.__uint_to_t FStar.UInt8.uint_to_t Prims.op_Subtraction QUIC.Secret.Int.Base.v Lib.IntTypes.U32 Lib.IntTypes.SEC Prims.b2t Prims.op_LessThan LowParse.BitFields.__proj__Mkuint_t__item__v Prims.pow2 Prims.unit LowParse.BitFields.set_bitfield_bound LowParse.BitFields.set_bitfield LowParse.BitFields.ubitfield FStar.UInt8.v
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

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)

let get_pn_length
  (h: Public.header)
: Tot PN.packet_number_length_t 
= protected_bits_pn_length (Public.PShort? h) (Public.get_protected_bits h)

let protected_bits_reserved
  (is_short: bool)
  (pb: bitfield (if is_short then 5 else 4))
: Tot (bitfield 2)
= if is_short
  then BF.uint8.BF.get_bitfield pb 3 5
  else BF.uint8.BF.get_bitfield pb 2 4

let get_reserved_bits
  (h: Public.header)
: Tot (bitfield 2)
= protected_bits_reserved (Public.PShort? h) (Public.get_protected_bits h)

let packet_number_opt
  (cid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
  (h: Public.header' cid_len)
: Tot Type0
= if Public.is_retry h
  then unit
  else PN.packet_number_t' last (get_pn_length h)

let parse_packet_number_opt_kind = LP.strong_parser_kind 0 4 None

let parse_packet_number_opt
  (cid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
  (h: Public.header' cid_len)
: Tot (LP.parser parse_packet_number_opt_kind (packet_number_opt cid_len last h))
= if Public.is_retry h
  then LP.weaken parse_packet_number_opt_kind LP.parse_empty
  else LP.weaken parse_packet_number_opt_kind (PN.parse_packet_number last (get_pn_length h))

let serialize_packet_number_opt
  (cid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
  (h: Public.header' cid_len)
: Tot (LP.serializer (parse_packet_number_opt cid_len last h))
= if Public.is_retry h
  then LP.serialize_weaken parse_packet_number_opt_kind LP.serialize_empty
  else LP.serialize_weaken parse_packet_number_opt_kind (PN.serialize_packet_number last (get_pn_length h))

let packet_number_prop
  (last: PN.last_packet_number_t)
  (h: header)
: GTot bool
= if not (is_retry h)
  then PN.in_window (Secret.v (pn_length h) - 1) (Secret.v last) (Secret.v (packet_number h))
  else true

module U32 = FStar.UInt32

let short_dcid_len_prop
  (short_dcid_len: short_dcid_len_t)
  (h: header)
: Tot bool
= if MShort? h
  then dcid_len h = U32.v short_dcid_len
  else true

unfold
let parse_header_prop
  (short_dcid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
  (m: header)
: GTot bool
= short_dcid_len_prop short_dcid_len m &&
  packet_number_prop last m

inline_for_extraction
type header'
  (short_dcid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
= LP.parse_filter_refine (parse_header_prop short_dcid_len last)

let protected_bits_key_phase
  (x: bitfield 5)
: Tot bool
= BF.uint8.BF.get_bitfield x 2 3 = 1uy

let mk_short_protected_bits
  (reserved_bits: bitfield 2)
  (key_phase: bool)
  (pnl: PN.packet_number_length_t)
val mk_short_protected_bits
      (reserved_bits: bitfield 2)
      (key_phase: bool)
      (pnl: PN.packet_number_length_t)
    : GTot (bitfield 5)

    reserved_bits: QUIC.Spec.Base.bitfield 2 ->
    key_phase: Prims.bool ->
    pnl: QUIC.Spec.PacketNumber.Base.packet_number_length_t
  -> Prims.GTot (QUIC.Spec.Base.bitfield 5)