val public_header_len_correct' (h: header) (m: HS.mem) (pn: PN.packet_number_t)
    : Lemma
    (let gh = g_header h m pn in
      let cid_len = dcid_len h in
      let last = last_packet_number gh in
      let (| ph , pn' |) = synth_header_recip cid_len last gh in
      Public.g_header (p_header h) m == ph /\
      U32.v (public_header_len h) == Seq.length (LP.serialize (Public.serialize_header cid_len) ph))
let public_header_len_correct'
  (h: header)
  (m: HS.mem)
  (pn: PN.packet_number_t)
: Lemma (
    let gh = g_header h m pn in
    let cid_len = dcid_len h in
    let last = last_packet_number gh in
    let (| ph, pn' |) = synth_header_recip cid_len last gh in
    Public.g_header (p_header h) m == ph /\
    U32.v (public_header_len h) == Seq.length (LP.serialize (Public.serialize_header cid_len) ph) 
  )
= public_header_len_correct h;
  public_g_header_p_header h m pn;
  Public.header_len_correct (dcid_len h) m (p_header h)
val public_header_len_correct' (h: header) (m: HS.mem) (pn: PN.packet_number_t)
    : Lemma
    (let gh = g_header h m pn in
      let cid_len = dcid_len h in
      let last = last_packet_number gh in
      let (| ph , pn' |) = synth_header_recip cid_len last gh in
      Public.g_header (p_header h) m == ph /\
      U32.v (public_header_len h) == Seq.length (LP.serialize (Public.serialize_header cid_len) ph))
let public_header_len_correct' (h: header) (m: HS.mem) (pn: PN.packet_number_t)
    : Lemma
    (let gh = g_header h m pn in
      let cid_len = dcid_len h in
      let last = last_packet_number gh in
      let (| ph , pn' |) = synth_header_recip cid_len last gh in
      Public.g_header (p_header h) m == ph /\
      U32.v (public_header_len h) == Seq.length (LP.serialize (Public.serialize_header cid_len) ph)) =
public_header_len_correct h;
public_g_header_p_header h m pn;
Public.header_len_correct (dcid_len h) m (p_header h)
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 FStar.Monotonic.HyperStack.mem QUIC.Spec.PacketNumber.Base.packet_number_t QUIC.Impl.Header.Public.header_len_correct QUIC.Impl.Header.Base.dcid_len QUIC.Impl.Header.Parse.p_header Prims.unit QUIC.Impl.Header.Parse.public_g_header_p_header QUIC.Impl.Header.Parse.public_header_len_correct Prims.l_True Prims.squash QUIC.Spec.Header.Public.header' QUIC.Spec.Header.Parse.packet_number_opt Prims.l_and Prims.eq2 QUIC.Spec.Header.Public.header QUIC.Impl.Header.Public.g_header Prims.int Prims.l_or Prims.b2t Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt32.n FStar.UInt32.v QUIC.Impl.Header.Base.public_header_len FStar.Seq.Base.length LowParse.Bytes.byte LowParse.Spec.Base.serialize QUIC.Spec.Header.Public.parse_header_kind QUIC.Spec.Header.Public.parse_header QUIC.Spec.Header.Public.serialize_header Prims.dtuple2 QUIC.Spec.Header.Parse.synth_header_recip QUIC.Spec.PacketNumber.Base.last_packet_number_t QUIC.Spec.Header.Parse.last_packet_number FStar.UInt32.t QUIC.Spec.Header.Base.header QUIC.Impl.Header.Base.g_header Prims.Nil FStar.Pervasives.pattern
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)
: 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

let public_header_len_correct
  (h: header)
: Lemma
  (public_header_len h == Public.header_len (p_header h))
= ()

#push-options "--z3rlimit 1024 --query_stats"

let public_g_header_p_header
  (h: header)
  (m: HS.mem)
  (pn: PN.packet_number_t)
: Lemma (
    let gh = g_header h m pn in
    let cid_len = dcid_len h in
    let last = last_packet_number gh in
    let (| ph, pn' |) = synth_header_recip cid_len last gh in
    Public.g_header (p_header h) m == ph
  )
= ()

let public_header_len_correct'
  (h: header)
  (m: HS.mem)
  (pn: PN.packet_number_t)
: Lemma (
    let gh = g_header h m pn in
    let cid_len = dcid_len h in
    let last = last_packet_number gh in
    let (| ph, pn' |) = synth_header_recip cid_len last gh in
    Public.g_header (p_header h) m == ph /\
    U32.v (public_header_len h) == Seq.length (LP.serialize (Public.serialize_header cid_len) ph)
val public_header_len_correct' (h: header) (m: HS.mem) (pn: PN.packet_number_t)
    : Lemma
    (let gh = g_header h m pn in
      let cid_len = dcid_len h in
      let last = last_packet_number gh in
      let (| ph , pn' |) = synth_header_recip cid_len last gh in
      Public.g_header (p_header h) m == ph /\
      U32.v (public_header_len h) == Seq.length (LP.serialize (Public.serialize_header cid_len) ph))

    h: QUIC.Impl.Header.Base.header ->
    m: FStar.Monotonic.HyperStack.mem ->
    pn: QUIC.Spec.PacketNumber.Base.packet_number_t
  -> FStar.Pervasives.Lemma
    (ensures
      (let gh = QUIC.Impl.Header.Base.g_header h m pn in
        let cid_len = QUIC.Impl.Header.Base.dcid_len h in
        let last = QUIC.Spec.Header.Parse.last_packet_number gh in
        let _ = QUIC.Spec.Header.Parse.synth_header_recip cid_len last gh in
        (let Prims.Mkdtuple2 #_ #_ ph _ = _ in
          QUIC.Impl.Header.Public.g_header (QUIC.Impl.Header.Parse.p_header h) m == ph /\
          FStar.UInt32.v (QUIC.Impl.Header.Base.public_header_len h) ==
          FStar.Seq.Base.length (LowParse.Spec.Base.serialize (QUIC.Spec.Header.Public.serialize_header
                    cid_len)
                ph))
        <:
        Type0))