val synth_header_recip
      (short_dcid_len: short_dcid_len_t)
      (last: PN.last_packet_number_t)
      (x: header' short_dcid_len last)
    : GTot (dtuple2 (Public.header' short_dcid_len) (packet_number_opt short_dcid_len last))
val synth_header_recip
      (short_dcid_len: short_dcid_len_t)
      (last: PN.last_packet_number_t)
      (x: header' short_dcid_len last)
    : GTot (dtuple2 (Public.header' short_dcid_len) (packet_number_opt short_dcid_len last))
let synth_header_recip
  (short_dcid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
  (x: header' short_dcid_len last)
: GTot (dtuple2 (Public.header' short_dcid_len) (packet_number_opt short_dcid_len last))
= match x with
  | MShort rb spin key_phase dcid pnl pn ->
    mk_short_protected_bits_correct rb key_phase pnl;
    (| Public.PShort (mk_short_protected_bits rb key_phase pnl) spin dcid, pn |)
  | MLong version dcid scid spec ->
    begin match spec with
    | MRetry unused odcid ->
      (| Public.PLong unused version dcid scid (Public.PRetry odcid), () |)
    | MInitial rb token payload_and_pn_length pnl pn ->
      mk_long_protected_bits_correct rb pnl;
      (| Public.PLong (mk_long_protected_bits rb pnl) version dcid scid (Public.PInitial token payload_and_pn_length), pn |)
    | MHandshake rb payload_and_pn_length pnl pn ->
      mk_long_protected_bits_correct rb pnl;
      (| Public.PLong (mk_long_protected_bits rb pnl) version dcid scid (Public.PHandshake payload_and_pn_length), pn |)
    | MZeroRTT rb payload_and_pn_length pnl pn ->
      mk_long_protected_bits_correct rb pnl;
      (| Public.PLong (mk_long_protected_bits rb pnl) version dcid scid (Public.PZeroRTT payload_and_pn_length), pn |)
    end
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)
: 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

let protected_bits_pn_length_prop
  (is_short: bool)
  (pb: bitfield (if is_short then 5 else 4))
: Lemma
  (Secret.v (protected_bits_pn_length is_short pb) == U8.v (BF.uint8.BF.get_bitfield pb 0 2) + 1)
  [SMTPat (protected_bits_pn_length is_short pb)]
= ()

#push-options "--z3rlimit 16 --max_fuel 2"

let mk_short_protected_bits_correct
  (reserved_bits: bitfield 2)
  (key_phase: bool)
  (pnl: PN.packet_number_length_t)
: Lemma
  (
    let b = mk_short_protected_bits reserved_bits key_phase pnl in
    protected_bits_pn_length true b == pnl /\
    protected_bits_reserved true b == reserved_bits /\
    protected_bits_key_phase b == key_phase /\
    True
  )
= ()

let mk_short_protected_bits_complete
  (pb: bitfield 5)
: Lemma
  (
    mk_short_protected_bits (protected_bits_reserved true pb) (protected_bits_key_phase pb) (protected_bits_pn_length true pb) == pb
  )
= let pb' = mk_short_protected_bits (protected_bits_reserved true pb) (protected_bits_key_phase pb) (protected_bits_pn_length true pb) in
  BF.get_bitfield_full #5 (U8.v pb');
  BF.get_bitfield_full #5 (U8.v pb);
  BF.get_bitfield_size 5 8 (U8.v pb) 0 5;
  BF.get_bitfield_size 5 8 (U8.v pb') 0 5;
  assert_norm (BF.get_bitfield_partition_prop #8 (U8.v pb) (U8.v pb') 0 5 [2; 3] <==> (
    (BF.uint8.BF.v (BF.uint8.BF.get_bitfield pb 0 2) == BF.uint8.BF.v (BF.uint8.BF.get_bitfield pb' 0 2)) /\
    (BF.uint8.BF.v (BF.uint8.BF.get_bitfield pb 2 3) == BF.uint8.BF.v (BF.uint8.BF.get_bitfield pb' 2 3)) /\
    (BF.uint8.BF.v (BF.uint8.BF.get_bitfield pb 3 5) == BF.uint8.BF.v (BF.uint8.BF.get_bitfield pb' 3 5))
  ));
  BF.get_bitfield_partition #8 (U8.v pb) (U8.v pb') 0 5 [2; 3]

#pop-options

let mk_long_protected_bits
  (reserved_bits: bitfield 2)
  (pnl: PN.packet_number_length_t)
: GTot (bitfield 4)
= BF.set_bitfield_bound #8 0 4 0 2 (Secret.v pnl - 1);
  BF.set_bitfield_bound #8 (BF.set_bitfield #8 0 0 2 (Secret.v pnl - 1)) 4 2 4 (U8.v reserved_bits);
  BF.uint8.BF.set_bitfield (BF.uint8.BF.set_bitfield 0uy 0 2 (U8.uint_to_t (Secret.v pnl - 1))) 2 4 reserved_bits

let mk_long_protected_bits_correct
  (reserved_bits: bitfield 2)
  (pnl: PN.packet_number_length_t)
: Lemma
  (
    let b = mk_long_protected_bits reserved_bits pnl in
    protected_bits_pn_length false b == pnl /\
    protected_bits_reserved false b == reserved_bits
  )
= ()

let mk_long_protected_bits_complete
  (pb: bitfield 4)
: Lemma
  (
    mk_long_protected_bits (protected_bits_reserved false pb) (protected_bits_pn_length false pb) == pb
  )
= let pb' = mk_long_protected_bits (protected_bits_reserved false pb) (protected_bits_pn_length false pb) in
  BF.get_bitfield_full #4 (U8.v pb');
  BF.get_bitfield_full #4 (U8.v pb);
  BF.get_bitfield_size 4 8 (U8.v pb) 0 4;
  BF.get_bitfield_size 4 8 (U8.v pb') 0 4;
  assert (
      (BF.uint8.BF.v (BF.uint8.BF.get_bitfield pb 0 2) == BF.uint8.BF.v (BF.uint8.BF.get_bitfield pb' 0 2)) /\
    (BF.uint8.BF.v (BF.uint8.BF.get_bitfield pb 2 4) == BF.uint8.BF.v (BF.uint8.BF.get_bitfield pb' 2 4))
  );
  BF.get_bitfield_partition_2_gen #8 0 2 4 (U8.v pb) (U8.v pb')

let synth_header
  (short_dcid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
  (x: dtuple2 (Public.header' short_dcid_len) (packet_number_opt short_dcid_len last))
: Tot (header' short_dcid_len last)
= let (| h, pn |) = x in
  match h with
  | Public.PShort protected_bits spin dcid ->
    MShort (protected_bits_reserved true protected_bits) spin (protected_bits_key_phase protected_bits) dcid (protected_bits_pn_length true protected_bits) pn
  | Public.PLong protected_bits version dcid scid spec ->
    let pnl = protected_bits_pn_length false protected_bits in
    let rb = protected_bits_reserved false protected_bits in
    MLong version dcid scid
      begin match spec with
      | Public.PRetry odcid ->
        MRetry protected_bits odcid
      | Public.PInitial token payload_and_pn_length ->
        MInitial rb token payload_and_pn_length pnl pn
      | Public.PHandshake payload_and_pn_length ->
        MHandshake rb payload_and_pn_length pnl pn
      | Public.PZeroRTT payload_and_pn_length ->
        MZeroRTT rb payload_and_pn_length pnl pn
      end
/
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

    short_dcid_len: QUIC.Spec.Base.short_dcid_len_t ->
    last: QUIC.Spec.PacketNumber.Base.last_packet_number_t ->
    x: QUIC.Spec.Header.Parse.header' short_dcid_len last
  -> Prims.GTot
    (Prims.dtuple2 (QUIC.Spec.Header.Public.header' short_dcid_len)
        (QUIC.Spec.Header.Parse.packet_number_opt short_dcid_len last))
QUIC.Spec.Base.short_dcid_len_t QUIC.Spec.PacketNumber.Base.last_packet_number_t QUIC.Spec.Header.Parse.header' QUIC.Spec.Base.bitfield Prims.bool QUIC.Spec.Base.vlbytes QUIC.Spec.PacketNumber.Base.packet_number_length_t QUIC.Spec.PacketNumber.Base.packet_number_t Prims.Mkdtuple2 QUIC.Spec.Header.Public.header' QUIC.Spec.Header.Parse.packet_number_opt QUIC.Spec.Header.Public.PShort QUIC.Spec.Header.Parse.mk_short_protected_bits Prims.unit QUIC.Spec.Header.Parse.mk_short_protected_bits_correct FStar.UInt32.t QUIC.Spec.Header.Base.long_header_specifics QUIC.Spec.Header.Public.PLong QUIC.Spec.Header.Public.PRetry QUIC.Spec.Base.token_max_len QUIC.Spec.Base.payload_and_pn_length_t QUIC.Spec.Header.Parse.mk_long_protected_bits QUIC.Spec.Header.Public.PInitial QUIC.Spec.Header.Parse.mk_long_protected_bits_correct QUIC.Spec.Header.Public.PHandshake QUIC.Spec.Header.Public.PZeroRTT Prims.dtuple2
let synth_header_recip
      (short_dcid_len: short_dcid_len_t)
      (last: PN.last_packet_number_t)
      (x: header' short_dcid_len last)
    : GTot (dtuple2 (Public.header' short_dcid_len) (packet_number_opt short_dcid_len last)) =
  
match x with
| MShort rb spin key_phase dcid pnl pn ->
  mk_short_protected_bits_correct rb key_phase pnl;
  (| Public.PShort (mk_short_protected_bits rb key_phase pnl) spin dcid, pn |)
| MLong version dcid scid spec ->
  match spec with
  | MRetry unused odcid -> (| Public.PLong unused version dcid scid (Public.PRetry odcid), () |)
  | MInitial rb token payload_and_pn_length pnl pn ->
    mk_long_protected_bits_correct rb pnl;
    (|
      Public.PLong (mk_long_protected_bits rb pnl)
        version
        dcid
        scid
        (Public.PInitial token payload_and_pn_length),
      pn
    |)
  | MHandshake rb payload_and_pn_length pnl pn ->
    mk_long_protected_bits_correct rb pnl;
    (|
      Public.PLong (mk_long_protected_bits rb pnl)
        version
        dcid
        scid
        (Public.PHandshake payload_and_pn_length),
      pn
    |)
  | MZeroRTT rb payload_and_pn_length pnl pn ->
    mk_long_protected_bits_correct rb pnl;
    (|
      Public.PLong (mk_long_protected_bits rb pnl)
        version
        dcid
        scid
        (Public.PZeroRTT payload_and_pn_length),
      pn
    |)