val impl_protected_bits_pn_length (is_short: bool) (pb: secret_bitfield (if is_short then 5 else 4))
    : Tot (y: PN.packet_number_length_t{y == protected_bits_pn_length is_short (Secret.reveal pb)})
let impl_protected_bits_pn_length
  (is_short: bool)
  (pb: secret_bitfield (if is_short then 5 else 4))
: Tot (y: PN.packet_number_length_t { y == protected_bits_pn_length is_short (Secret.reveal pb) })
= // https://github.com/FStarLang/karamel/issues/102
  let bf = Secret.get_bitfield #Secret.U8 pb 0ul 2ul in
  Secret.to_u32 #Secret.U8 (Secret.to_u8 1uy `Secret.add` bf)
val impl_protected_bits_pn_length (is_short: bool) (pb: secret_bitfield (if is_short then 5 else 4))
    : Tot (y: PN.packet_number_length_t{y == protected_bits_pn_length is_short (Secret.reveal pb)})
let impl_protected_bits_pn_length (is_short: bool) (pb: secret_bitfield (if is_short then 5 else 4))
    : Tot (y: PN.packet_number_length_t{y == protected_bits_pn_length is_short (Secret.reveal pb)}) =
let bf = Secret.get_bitfield #Secret.U8 pb 0ul 2ul in
Secret.to_u32 #Secret.U8 ((Secret.to_u8 1uy) `Secret.add` bf)
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
Prims.bool QUIC.Spec.Base.secret_bitfield Prims.nat Prims.b2t Prims.op_LessThanOrEqual Lib.IntTypes.to_u32 Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.add Lib.IntTypes.to_u8 Lib.IntTypes.U1 Lib.IntTypes.PUB FStar.UInt8.__uint_to_t Lib.IntTypes.int_t Prims.eq2 Prims.int Prims.l_or Lib.IntTypes.range Prims.l_and FStar.UInt.size Prims.op_LessThan Prims.pow2 Prims.op_Subtraction FStar.UInt32.v FStar.UInt32.uint_to_t FStar.UInt32.t Lib.IntTypes.v LowParse.BitFields.get_bitfield QUIC.Secret.Int.get_bitfield FStar.UInt32.__uint_to_t QUIC.Spec.PacketNumber.Base.packet_number_length_t QUIC.Spec.Header.Parse.protected_bits_pn_length QUIC.Secret.Int.reveal
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) 
  )
= public_header_len_correct h;
  public_g_header_p_header h m pn;
  Public.header_len_correct (dcid_len h) m (p_header h)

#restart-solver

let public_header_len_is_pn_offset
  h m pn
= public_header_len_correct' h m pn

#pop-options

#push-options "--z3rlimit 16 --query_stats --z3cliopt smt.arith.nl=false"

#restart-solver

let header_len_correct
  h m pn
=
  allow_inversion header;
  allow_inversion long_header_specifics;
  let gh = g_header h m pn in
  let cid_len = dcid_len h in
  let last = last_packet_number gh in
  in_window_last_packet_number gh;
  let (| ph, pn' |) = synth_header_recip cid_len last gh in
  public_g_header_p_header h m pn;
  assert (Public.g_header (p_header h) m == ph);
  serialize_header_eq cid_len last gh;
  Public.header_len_correct cid_len m (p_header h);
  public_header_len_correct h;
  public_header_len_correct' h m pn;
  assert (Seq.length (LP.serialize (Public.serialize_header cid_len) ph) == U32.v (public_header_len h));
  if is_retry h
  then begin
    header_len_is_retry h;
    assert (Secret.v (header_len h) == Spec.header_len (g_header h m pn))
  end else begin
    header_len_not_is_retry h;
    assert (pn_offset gh + Secret.v (Spec.pn_length gh) == Spec.header_len gh);
    assert (pn_offset gh == Seq.length (LP.serialize (Public.serialize_header cid_len) ph));
    assert (Secret.v (header_len h) == Spec.header_len (g_header h m pn))
  end

#pop-options

let last_pn
  (is_retry: bool)
  (pn: PN.packet_number_t)
: Tot PN.last_packet_number_t
= if is_retry
  then Secret.to_u64 0uL
  else
    let cond = Secret.lognot_one_bit (pn `Secret.secrets_are_equal_62` Secret.to_u64 0uL) in
    pn `Secret.sub` cond

#push-options "--z3rlimit 64 --query_stats"

let last_pn_correct
  (h: header)
  (m: HS.mem)
  (pn: PN.packet_number_t)
: Lemma
  (last_packet_number (g_header h m pn) == last_pn (is_retry h) pn)
= ()

#pop-options

#push-options "--z3rlimit 128 --query_stats"

#restart-solver

let write_header
  h pn out out_len
= let m = HST.get () in
  header_len_correct h m pn;
  public_header_len_correct' h m pn;
  let cid_len = dcid_len h in
  let last = last_pn (is_retry h) pn in
  last_pn_correct h m pn;
  let ph = p_header h in
  in_window_last_packet_number (g_header h m pn);
  serialize_header_eq cid_len last (g_header h m pn);
  let len = Public.write_header cid_len ph out out_len in
  if is_retry h
  then ()
  else begin
    assert (len == Public.header_len ph);
    let pn_len = pn_length h in
    let m1 = HST.get () in
    SecretBuffer.with_buffer_hide
      #unit
      out
      len
      (len `U32.add` 4ul)
      m1
      B.loc_none
      B.loc_none
      1ul 0ul 0ul 4ul 1ul 0ul
      (fun _ contl cont _ _ ->
        contl == LP.serialize (Public.serialize_header cid_len) (Public.g_header ph m) /\
        Seq.slice cont 0 (Secret.v pn_len) `Seq.equal` LP.serialize (PN.serialize_packet_number last pn_len) pn
      )
      (fun _ _ bs _ ->
        PN.write_packet_number last pn_len pn bs
      )
  end
  
#pop-options

#push-options "--z3rlimit 64"

#restart-solver

let putative_pn_offset
  cid_len b b_len
=
  let h = HST.get () in
  let input = LP.make_slice b b_len in
  assert (LP.bytes_of_slice_from h input 0ul `Seq.equal` B.as_seq h b);
  LP.valid_facts (Public.parse_header cid_len) h input 0ul;
  let res = Public.validate_header cid_len input 0uL in
  if LP.is_error res
  then None
  else Some (LP.uint64_to_uint32 res)

#pop-options

let impl_protected_bits_pn_length
  (is_short: bool)
  (pb: secret_bitfield (if is_short then 5 else 4))
val impl_protected_bits_pn_length (is_short: bool) (pb: secret_bitfield (if is_short then 5 else 4))
    : Tot (y: PN.packet_number_length_t{y == protected_bits_pn_length is_short (Secret.reveal pb)})

    is_short: Prims.bool ->
    pb:
      QUIC.Spec.Base.secret_bitfield (match is_short with
          | true -> 5
          | _ -> 4)
  -> y:
    QUIC.Spec.PacketNumber.Base.packet_number_length_t
      {y == QUIC.Spec.Header.Parse.protected_bits_pn_length is_short (QUIC.Secret.Int.reveal pb)}