val impl_long_protected_bits (reserved_bits: secret_bitfield 2) (pnl: PN.packet_number_length_t)
    : Tot
    (x: Secret.uint8{Secret.reveal x == mk_long_protected_bits (Secret.reveal reserved_bits) pnl})
let impl_long_protected_bits
  (reserved_bits: secret_bitfield 2)
  (pnl: PN.packet_number_length_t)
: Tot (x: Secret.uint8 { Secret.reveal x == mk_long_protected_bits (Secret.reveal reserved_bits) pnl })
= // https://github.com/FStarLang/karamel/issues/1024
  let pnl_1 = Secret.to_u8 pnl `Secret.sub` Secret.to_u8 1uy in
  Secret.set_bitfield #Secret.U8 (Secret.set_bitfield #Secret.U8 (Secret.to_u8 0uy) 0ul 2ul (pnl_1)) 2ul 4ul reserved_bits
val impl_long_protected_bits (reserved_bits: secret_bitfield 2) (pnl: PN.packet_number_length_t)
    : Tot
    (x: Secret.uint8{Secret.reveal x == mk_long_protected_bits (Secret.reveal reserved_bits) pnl})
let impl_long_protected_bits (reserved_bits: secret_bitfield 2) (pnl: PN.packet_number_length_t)
    : Tot
    (x: Secret.uint8{Secret.reveal x == mk_long_protected_bits (Secret.reveal reserved_bits) pnl}) =
let pnl_1 = (Secret.to_u8 pnl) `Secret.sub` (Secret.to_u8 1uy) in
Secret.set_bitfield #Secret.U8
  (Secret.set_bitfield #Secret.U8 (Secret.to_u8 0uy) 0ul 2ul (pnl_1))
  2ul
  4ul
  reserved_bits
QUIC.Impl.Header.Parse.fst.checked
QUIC.Spec.Header.Parse.fst.checked QUIC.Spec.Header.Parse.fst.checked QUIC.Secret.Buffer.fsti.checked QUIC.Impl.PacketNumber.fsti.checked QUIC.Impl.Header.Public.fsti.checked QUIC.Impl.Header.Base.fst.checked prims.fst.checked LowParse.Low.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
QUIC.Impl.Header.Parse.fst
QUIC.Spec.Base.secret_bitfield QUIC.Spec.PacketNumber.Base.packet_number_length_t QUIC.Secret.Int.set_bitfield Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.to_u8 Lib.IntTypes.U1 Lib.IntTypes.PUB FStar.UInt8.__uint_to_t FStar.UInt32.__uint_to_t Lib.IntTypes.int_t Lib.IntTypes.sub Lib.IntTypes.U32 Lib.IntTypes.uint8 Prims.eq2 FStar.UInt8.t Prims.l_or Lib.IntTypes.range_t QUIC.Secret.Int.Base.v Prims.b2t Prims.op_LessThan FStar.UInt8.v Prims.pow2 QUIC.Secret.Int.reveal QUIC.Spec.Header.Parse.mk_long_protected_bits
module QUIC.Impl.Header.Parse

open QUIC.Spec.Header.Parse
open QUIC.Impl.Header.Base

friend QUIC.Spec.Header.Parse

module LP = LowParse.Low.Base
module Public = QUIC.Impl.Header.Public
module U8 = FStar.UInt8
module SecretBuffer = QUIC.Secret.Buffer
module Spec = QUIC.Spec.Header.Parse
module PN = QUIC.Impl.PacketNumber

[@"opaque_to_smt"]
let impl_short_protected_bits
  (reserved_bits: secret_bitfield 2)
  (key_phase: secret_bitfield 1)
  (pnl: PN.packet_number_length_t)
: Tot (x: Secret.uint8 { Secret.reveal x == mk_short_protected_bits (Secret.reveal reserved_bits) (Secret.v key_phase = 1) pnl })
= // https://github.com/FStarLang/karamel/issues/1024
  let pnl_1 = Secret.to_u8 pnl `Secret.sub` Secret.to_u8 1uy in
Secret.set_bitfield #Secret.U8 (Secret.set_bitfield #Secret.U8 (Secret.set_bitfield #Secret.U8 (Secret.to_u8 0uy) 0ul 2ul (pnl_1)) 2ul 3ul key_phase) 3ul 5ul reserved_bits

[@"opaque_to_smt"]
let impl_long_protected_bits
  (reserved_bits: secret_bitfield 2)
  (pnl: PN.packet_number_length_t)
val impl_long_protected_bits (reserved_bits: secret_bitfield 2) (pnl: PN.packet_number_length_t)
    : Tot
    (x: Secret.uint8{Secret.reveal x == mk_long_protected_bits (Secret.reveal reserved_bits) pnl})

    reserved_bits: QUIC.Spec.Base.secret_bitfield 2 ->
    pnl: QUIC.Spec.PacketNumber.Base.packet_number_length_t
  -> x:
    Lib.IntTypes.uint8
      { QUIC.Secret.Int.reveal x ==
        QUIC.Spec.Header.Parse.mk_long_protected_bits (QUIC.Secret.Int.reveal reserved_bits) pnl }