val p_header (h: header) : Tot Public.header
let p_header
  (h: header)
: Tot Public.header
= match h with
  | BShort rb spin phase cid cid_len pnl ->
    Public.PShort (impl_short_protected_bits rb phase pnl) spin cid cid_len
  | BLong version dcid dcil scid scil spec ->
    begin match spec with
    | BInitial rb payload_and_pn_length pnl token token_length ->
      let spec' = (Public.PInitial payload_and_pn_length token token_length) in
      Public.PLong (impl_long_protected_bits rb pnl) version dcid dcil scid scil spec'
    | BZeroRTT rb payload_and_pn_length pnl ->
      let spec' = (Public.PZeroRTT payload_and_pn_length) in
      Public.PLong (impl_long_protected_bits rb pnl) version dcid dcil scid scil spec'
    | BHandshake rb payload_and_pn_length pnl ->
      let spec' = (Public.PHandshake payload_and_pn_length) in
      Public.PLong (impl_long_protected_bits rb pnl) version dcid dcil scid scil spec'
    | BRetry unused odcid odcil ->
      let spec' = (Public.PRetry odcid odcil) in
      Public.PLong unused version dcid dcil scid scil spec'
    end
val p_header (h: header) : Tot Public.header
let p_header (h: header) : Tot Public.header =
match h with
| BShort rb spin phase cid cid_len pnl ->
  Public.PShort (impl_short_protected_bits rb phase pnl) spin cid cid_len
| BLong version dcid dcil scid scil spec ->
  match spec with
  | BInitial rb payload_and_pn_length pnl token token_length ->
    let spec' = (Public.PInitial payload_and_pn_length token token_length) in
    Public.PLong (impl_long_protected_bits rb pnl) version dcid dcil scid scil spec'
  | BZeroRTT rb payload_and_pn_length pnl ->
    let spec' = (Public.PZeroRTT payload_and_pn_length) in
    Public.PLong (impl_long_protected_bits rb pnl) version dcid dcil scid scil spec'
  | BHandshake rb payload_and_pn_length pnl ->
    let spec' = (Public.PHandshake payload_and_pn_length) in
    Public.PLong (impl_long_protected_bits rb pnl) version dcid dcil scid scil spec'
  | BRetry unused odcid odcil ->
    let spec' = (Public.PRetry odcid odcil) in
    Public.PLong unused version dcid dcil scid scil spec'
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.Impl.Header.Base.header QUIC.Spec.Base.secret_bitfield Prims.bool LowStar.Buffer.buffer FStar.UInt8.t FStar.UInt32.t Prims.l_and Prims.eq2 Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.b2t Prims.op_GreaterThanOrEqual LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder Prims.op_LessThanOrEqual FStar.UInt.uint_t FStar.UInt32.v QUIC.Spec.PacketNumber.Base.packet_number_length_t QUIC.Impl.Header.Public.PShort QUIC.Impl.Header.Parse.impl_short_protected_bits QUIC.Impl.Header.Base.long_header_specifics QUIC.Spec.Base.payload_and_pn_length_t QUIC.Spec.Base.token_max_len QUIC.Impl.Header.Public.PLong QUIC.Impl.Header.Parse.impl_long_protected_bits QUIC.Impl.Header.Public.long_header_specifics QUIC.Impl.Header.Public.PInitial QUIC.Impl.Header.Public.PZeroRTT QUIC.Impl.Header.Public.PHandshake Prims.op_Equality QUIC.Impl.Header.Public.PRetry QUIC.Impl.Header.Public.header
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)
: 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

let p_header
  (h: header)
val p_header (h: header) : Tot Public.header
h: QUIC.Impl.Header.Base.header -> QUIC.Impl.Header.Public.header