val serialize_header_dtuple (short_dcid_len: short_dcid_len_t) (last: PN.last_packet_number_t)
    : Tot (LP.serializer (parse_header_dtuple short_dcid_len last))
let serialize_header_dtuple
  (short_dcid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
: Tot (LP.serializer (parse_header_dtuple short_dcid_len last))
= 
  LP.serialize_dtuple2
    #_ #(Public.header' short_dcid_len)
    (Public.serialize_header short_dcid_len)
    #_ #(packet_number_opt short_dcid_len last)
    #(parse_packet_number_opt short_dcid_len last)
    (serialize_packet_number_opt short_dcid_len last)
val serialize_header_dtuple (short_dcid_len: short_dcid_len_t) (last: PN.last_packet_number_t)
    : Tot (LP.serializer (parse_header_dtuple short_dcid_len last))
let serialize_header_dtuple (short_dcid_len: short_dcid_len_t) (last: PN.last_packet_number_t)
    : Tot (LP.serializer (parse_header_dtuple short_dcid_len last)) =
LP.serialize_dtuple2 #_
  #(Public.header' short_dcid_len)
  (Public.serialize_header short_dcid_len)
  #_
  #(packet_number_opt short_dcid_len last)
  #(parse_packet_number_opt short_dcid_len last)
  (serialize_packet_number_opt short_dcid_len last)
QUIC.Spec.Header.Parse.fst.checked
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
QUIC.Spec.Base.short_dcid_len_t QUIC.Spec.PacketNumber.Base.last_packet_number_t LowParse.Spec.Combinators.serialize_dtuple2 QUIC.Spec.Header.Public.parse_header_kind QUIC.Spec.Header.Public.header' QUIC.Spec.Header.Public.parse_header QUIC.Spec.Header.Public.serialize_header QUIC.Spec.Header.Parse.parse_packet_number_opt_kind QUIC.Spec.Header.Parse.packet_number_opt QUIC.Spec.Header.Parse.parse_packet_number_opt QUIC.Spec.Header.Parse.serialize_packet_number_opt LowParse.Spec.Base.serializer QUIC.Spec.Header.Parse.parse_header_kind Prims.dtuple2 QUIC.Spec.Header.Parse.parse_header_dtuple
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

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

let synth_header_injective
  (short_dcid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
: Lemma
  (LP.synth_injective #(dtuple2 (Public.header' short_dcid_len) (packet_number_opt short_dcid_len last)) #(header' short_dcid_len last)  (synth_header short_dcid_len last))
  [SMTPat (LP.synth_injective #(dtuple2 (Public.header' short_dcid_len) (packet_number_opt short_dcid_len last)) #(header' short_dcid_len last) (synth_header short_dcid_len last))]
= LP.synth_inverse_intro' (synth_header_recip short_dcid_len last) (synth_header short_dcid_len last) (fun (x: dtuple2 (Public.header' short_dcid_len) (packet_number_opt short_dcid_len last)) ->
    let (| h, pn |) = x in
    match h with
    | Public.PShort protected_bits spin dcid ->
      mk_short_protected_bits_complete protected_bits
    | Public.PLong protected_bits version dcid scid spec ->
      begin match spec with
      | Public.PRetry odcid -> ()
      | _ -> mk_long_protected_bits_complete protected_bits
      end
  );
  LP.synth_inverse_synth_injective (synth_header short_dcid_len last) (synth_header_recip short_dcid_len last)

let synth_header_inverse
  (short_dcid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
: Lemma
  (LP.synth_inverse #(dtuple2 (Public.header' short_dcid_len) (packet_number_opt short_dcid_len last)) #(header' short_dcid_len last) (synth_header short_dcid_len last) (synth_header_recip short_dcid_len last))
  [SMTPat (LP.synth_inverse #(dtuple2 (Public.header' short_dcid_len) (packet_number_opt short_dcid_len last)) #(header' short_dcid_len last) (synth_header short_dcid_len last) (synth_header_recip short_dcid_len last))]
= LP.synth_inverse_intro' (synth_header short_dcid_len last) (synth_header_recip short_dcid_len last) (fun (x: header' short_dcid_len last) ->
    match x with
    | MShort rb spin key_phase dcid pnl pn ->
      mk_short_protected_bits_correct rb key_phase pnl
    | MLong version dcid scid spec ->
      begin match spec with
      | MRetry unused odcid -> ()
      | MInitial rb token payload_and_pn_length pnl pn ->
        mk_long_protected_bits_correct rb pnl
      | MHandshake rb payload_and_pn_length pnl pn ->
        mk_long_protected_bits_correct rb pnl
      | MZeroRTT rb payload_and_pn_length pnl pn ->
        mk_long_protected_bits_correct rb pnl
      end
  )

let parse_header_kind
  (short_dcid_len: short_dcid_len_t)
: Tot (k: LP.parser_kind {
    k.LP.parser_kind_subkind == Some LP.ParserStrong /\
    k.LP.parser_kind_low > 0 /\
    begin match k.LP.parser_kind_high with
    | None -> False
    | Some max -> max < header_len_bound
    end
  })
= LP.parse_filter_kind (Public.parse_header_kind short_dcid_len) `LP.and_then_kind` parse_packet_number_opt_kind

let parse_header_dtuple
  (short_dcid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
: Tot (LP.parser (parse_header_kind short_dcid_len) (dtuple2 (Public.header' short_dcid_len) (packet_number_opt short_dcid_len last)))
= LP.parse_dtuple2
    #_ #(Public.header' short_dcid_len)
    (Public.parse_header short_dcid_len)
    #_ #(packet_number_opt short_dcid_len last)
    (parse_packet_number_opt short_dcid_len last)

let lp_parse_header
  (short_dcid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
: Tot (LP.parser (parse_header_kind short_dcid_len) (header' short_dcid_len last))
=
  LP.parse_synth
    #_
    #(dtuple2 (Public.header' short_dcid_len) (packet_number_opt short_dcid_len last))
    #(header' short_dcid_len last)
    (parse_header_dtuple short_dcid_len last)
    (synth_header short_dcid_len last)

#push-options "--z3rlimit 64"

let parse_header_dtuple_eq_1
  (short_dcid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
  (x: bytes)
: Lemma
  (LP.parse (parse_header_dtuple short_dcid_len last) x ==
    LP.bare_parse_dtuple2
      #_ #(Public.header' short_dcid_len)
      (Public.parse_header short_dcid_len)
      #_ #(packet_number_opt short_dcid_len last)
      (parse_packet_number_opt short_dcid_len last)
      x
  )
= LP.parse_dtuple2_eq'
    #_ #(Public.header' short_dcid_len)
    (Public.parse_header short_dcid_len)
    #_ #(packet_number_opt short_dcid_len last)
    (parse_packet_number_opt short_dcid_len last)
    x

let parse_header_dtuple_eq_2
  (short_dcid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
  (x: bytes)
: Lemma
  (LP.parse (parse_header_dtuple short_dcid_len last) x == (
    match LP.parse (Public.parse_header short_dcid_len) x with
    | None -> None
    | Some (ph, consumed) ->
      begin match LP.parse (parse_packet_number_opt short_dcid_len last ph) (Seq.slice x consumed (Seq.length x)) with
      | None -> None
      | Some (pn, consumed') -> Some ((| ph, pn |), consumed + consumed')
      end
  ))
= parse_header_dtuple_eq_1 short_dcid_len last x

let parse_header_dtuple_eq
  (short_dcid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
  (x: bytes)
: Lemma
  (LP.parse (parse_header_dtuple short_dcid_len last) x == (
    match LP.parse (Public.parse_header short_dcid_len) x with
    | None -> None
    | Some (ph, consumed) ->
      if Public.is_retry ph
      then Some ((| ph, () |), consumed)
      else begin
        match LP.parse (PN.parse_packet_number last (get_pn_length ph)) (Seq.slice x consumed (Seq.length x)) with
        | None -> None
        | Some (pn, consumed') -> Some ((| ph, pn |), consumed + consumed')
      end
  ))
=
  LP.parse_dtuple2_eq'
    #_ #(Public.header' short_dcid_len)
    (Public.parse_header short_dcid_len)
    #_ #(packet_number_opt short_dcid_len last)
    (parse_packet_number_opt short_dcid_len last)
    x

let lp_parse_header_eq
  (short_dcid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
  (x: bytes)
: Lemma
  (LP.parse (lp_parse_header short_dcid_len last) x == (
    match LP.parse (Public.parse_header short_dcid_len) x with
    | None -> None
    | Some (ph, consumed) ->
      if Public.is_retry ph
      then Some (synth_header short_dcid_len last (| ph, () |), consumed)
      else begin
        match LP.parse (PN.parse_packet_number last (get_pn_length ph)) (Seq.slice x consumed (Seq.length x)) with
        | None -> None
        | Some (pn, consumed') -> Some (synth_header short_dcid_len last (| ph, pn |), consumed + consumed')
      end
  ))
= LP.parse_synth_eq
    #_
    #(dtuple2 (Public.header' short_dcid_len) (packet_number_opt short_dcid_len last))
    #(header' short_dcid_len last)
    (parse_header_dtuple short_dcid_len last)
    (synth_header short_dcid_len last)
    x;
  parse_header_dtuple_eq short_dcid_len last x

#pop-options

let serialize_header_dtuple
  (short_dcid_len: short_dcid_len_t)
  (last: PN.last_packet_number_t)
: Tot (LP.serializer (parse_header_dtuple short_dcid_len last))
val serialize_header_dtuple (short_dcid_len: short_dcid_len_t) (last: PN.last_packet_number_t)
    : Tot (LP.serializer (parse_header_dtuple short_dcid_len last))

    short_dcid_len: QUIC.Spec.Base.short_dcid_len_t ->
    last: QUIC.Spec.PacketNumber.Base.last_packet_number_t
  -> LowParse.Spec.Base.serializer (QUIC.Spec.Header.Parse.parse_header_dtuple short_dcid_len last)