val serialize32_long_initial_body:LP.serializer32 Public.serialize_long_initial_body
val serialize32_long_initial_body:LP.serializer32 Public.serialize_long_initial_body
let serialize32_long_initial_body : LP.serializer32 Public.serialize_long_initial_body =
    serialize32_common_long `LP.serialize32_nondep_then` (
      LP.serialize32_bounded_vlgenbytes 0 token_max_len (serialize32_bounded_varint 0 (token_max_len)) `LP.serialize32_nondep_then`
      serialize32_payload_and_pn_length
    )
module QUIC.TotSpec

friend QUIC.Spec
friend QUIC.Spec.Header
friend QUIC.Spec.Header.Parse
friend QUIC.Spec.Header.Public
friend QUIC.Spec.PacketNumber
friend QUIC.Spec.VarInt

module PN = QUIC.Spec.PacketNumber
module VI = QUIC.Spec.VarInt
module Public = QUIC.Spec.Header.Public
module Parse = QUIC.Spec.Header.Parse
module Header = QUIC.Spec.Header
module Lemmas = QUIC.Spec.Lemmas
module Spec = QUIC.Spec

module LP = LowParse.SLow
module LPB = LowParse.SLow.BitSum

module U8 = FStar.UInt8
module U62 = QUIC.UInt62
module U64 = FStar.UInt64
module BF = LowParse.BitFields
module B32 = LowParse.Bytes32
module Cast = FStar.Int.Cast
module U32 = FStar.UInt32
module Seq = QUIC.Secret.Seq

#push-options "--z3rlimit 128"

let parse32_varint'
  (b: B32.bytes)
: Tot (option (U62.t & U32.t))
= assert_norm (pow2 8 == 256);
  assert_norm (pow2 6 == 64);
  assert (pow2 62 == U64.v U62.bound);
  assert_norm (pow2 24 == 16777216);
  assert_norm (pow2 32 == 4294967296);
  match LP.parse32_u8 b with
  | None -> None
  | Some (hd, consumed) ->
    let tag = BF.uint8.BF.get_bitfield hd 6 8 in
    let msb = Cast.uint8_to_uint64 (BF.uint8.BF.get_bitfield hd 0 6) in
    let b' = B32.slice b consumed (B32.len b) in
    if tag = 0uy
    then
      Some ((msb <: U62.t), consumed)
    else if tag = 1uy
    then begin match LP.parse32_u8 b' with
    | None -> None
    | Some (lsb, consumed') ->
      let v : U62.t = (msb `U64.mul` 256uL) `U64.add` Cast.uint8_to_uint64 lsb in
      if 64uL `U64.lte` v
      then Some (v, consumed `U32.add` consumed')
      else None
      end
    else if tag = 2uy
    then begin match (LP.parse32_bounded_integer 3) b' with
    | None -> None
    | Some (lsb, consumed') ->
      let v : U62.t =
        (msb `U64.mul` 16777216uL) `U64.add` Cast.uint32_to_uint64 lsb
      in
      if 16384uL `U64.lte` v
      then Some (v, consumed `U32.add` consumed')
      else None
    end else begin match (LP.parse32_u32 `LP.parse32_nondep_then` LP.parse32_bounded_integer 3) b' with
    | None -> None
    | Some ((hi, lo), consumed') ->
      let v : U62.t =
        Cast.uint32_to_uint64 lo `U64.add` (16777216uL `U64.mul` (Cast.uint32_to_uint64 hi `U64.add` (4294967296uL `U64.mul` msb)))
      in
      if 1073741824uL `U64.lte` v
      then Some (v, consumed `U32.add` consumed')
      else None
    end

let parse32_varint'_correct
  (input: B32.bytes)
: Lemma
  (LP.parser32_correct VI.parse_varint input (parse32_varint' input))
= VI.parse_varint_eq (B32.reveal input)

#pop-options

let parse32_varint
: LP.parser32 VI.parse_varint
= fun input ->
    parse32_varint'_correct input; 
    parse32_varint' input

let parse32_bounded_varint
  (min: U32.t)
  (max: U32.t { U32.v min <= U32.v max })
: Tot (LP.parser32 (VI.parse_bounded_varint (U32.v min) (U32.v max)))
= LP.parse32_synth'
   (VI.parse_varint `LP.parse_filter` VI.varint_in_bounds (U32.v min) (U32.v max))
   (VI.synth_bounded_varint (U32.v min) (U32.v max))
   (LP.parse32_filter
     parse32_varint
     (VI.varint_in_bounds (U32.v min) (U32.v max))
     (fun x -> Cast.uint32_to_uint64 min `U64.lte` x && x `U64.lte` Cast.uint32_to_uint64 max)
   )
   ()

let serialize32_varint_payload
  (x: U62.t)
: Tot B32.bytes
=
  assert_norm (pow2 8 == 256);
  assert_norm (pow2 6 == 64);
  assert (pow2 62 == U64.v U62.bound);
  assert_norm (pow2 24 == 16777216);
  assert_norm (pow2 32 == 4294967296);
  if x `U64.lt` 64uL
  then B32.empty_bytes
  else if x `U64.lt` 16384uL
  then LP.serialize32_u8 (Cast.uint64_to_uint8 x)
  else if x `U64.lt` 1073741824uL
  then (LP.serialize32_bounded_integer 3) (Cast.uint64_to_uint32 (x `U64.rem` 16777216uL))
  else (LP.serialize32_u32 `LP.serialize32_nondep_then` LP.serialize32_bounded_integer 3) (Cast.uint64_to_uint32 (x `U64.div` 16777216uL), Cast.uint64_to_uint32 (x `U64.rem` 16777216uL))

#push-options "--z3rlimit 16"

let serialize32_varint
  : LP.serializer32 VI.serialize_varint
= fun x ->
  LP.serialize32_u8 (VI.get_first_byte x) `B32.append` serialize32_varint_payload x

let serialize32_bounded_varint
  (min: nat)
  (max: nat { min <= max /\ max < 4294967296 })
: Tot (LP.serializer32 (VI.serialize_bounded_varint min max))
= LP.serialize32_synth
   (VI.parse_varint `LP.parse_filter` VI.varint_in_bounds (min) (max))
   (VI.synth_bounded_varint (min) (max))
   (VI.serialize_varint `LP.serialize_filter` VI.varint_in_bounds min max)
   (serialize32_varint `LP.serialize32_filter` VI.varint_in_bounds min max)
   (VI.synth_bounded_varint_recip min max)
   (fun x -> VI.synth_bounded_varint_recip min max x)
   ()

#pop-options
    
(* Packet number. *)

module Declassify = Lib.RawIntTypes (* this spec is only for proof purposes, so we do not care about preserving secrets/constant-time execution *)

#push-options "--z3rlimit 16"

let synth_packet_number'
  (last: PN.last_packet_number_t)
  (pn_len: PN.packet_number_length_t)
  (npn: LP.bounded_integer (Secret.v pn_len))
: Tot (pn: PN.packet_number_t' last pn_len { pn == PN.synth_packet_number last pn_len npn })
= Secret.to_u64 (U64.uint_to_t (PN.expand_pn' (Declassify.uint_to_nat pn_len - 1) (Declassify.uint_to_nat last) (U32.v npn)))

#pop-options

let parse32_reduced_pn
  (pn_len: PN.packet_number_length_t)
: Tot (LP.parser32 (PN.parse_reduced_pn pn_len ()))
= LP.parse32_weaken
    PN.parse_packet_number_kind
    (LP.parse32_bounded_integer (Declassify.uint_to_nat pn_len))

let parse32_packet_number
  (last: PN.last_packet_number_t)
  (pn_len: PN.packet_number_length_t)
: Tot (LP.parser32 (PN.parse_packet_number last pn_len))
= LP.parse32_synth
    _
    (PN.synth_packet_number last pn_len)
    (synth_packet_number' last pn_len)
    (LP.lift_parser32 (PN.parse_reduced_pn pn_len) (parse32_reduced_pn pn_len))
    ()

let serialize32_reduced_pn
  (pn_len: PN.packet_number_length_t)
: Tot (LP.serializer32 (PN.serialize_reduced_pn pn_len ()))
= LP.serialize32_weaken
    PN.parse_packet_number_kind
    (LP.serialize32_bounded_integer (Declassify.uint_to_nat pn_len))

#push-options "--z3rlimit 16"
let synth_packet_number_recip'
  (last: PN.last_packet_number_t)
  (pn_len: PN.packet_number_length_t)
  (pn: PN.packet_number_t' last pn_len)
: Tot (npn: LP.bounded_integer (Secret.v pn_len)  { npn == PN.synth_packet_number_recip last pn_len pn })
= U32.uint_to_t (PN.reduce_pn' (Declassify.uint_to_nat pn_len - 1) (Declassify.uint_to_nat pn))
#pop-options

let serialize32_packet_number
  (last: PN.last_packet_number_t)
  (pn_len: PN.packet_number_length_t)
: Tot (LP.serializer32 (PN.serialize_packet_number last pn_len))
= LP.serialize32_synth
    (LP.lift_parser (PN.parse_reduced_pn pn_len))
    (PN.synth_packet_number last pn_len)
    (LP.lift_serializer #_ #_ #(PN.parse_reduced_pn pn_len) (PN.serialize_reduced_pn pn_len))
    (LP.lift_serializer32 #PN.parse_packet_number_kind #(LP.bounded_integer (Declassify.uint_to_nat pn_len)) (PN.parse_reduced_pn pn_len) (PN.serialize_reduced_pn pn_len) (serialize32_reduced_pn pn_len))
    (PN.synth_packet_number_recip last pn_len)
    (synth_packet_number_recip' last pn_len)
    ()

(* Parsing the public header *)

let parse32_common_long : LP.parser32 Public.parse_common_long =
  LP.parse32_u32 `LP.parse32_nondep_then` (
    LP.parse32_bounded_vlbytes 0 0ul 20 20ul `LP.parse32_nondep_then`
    LP.parse32_bounded_vlbytes 0 0ul 20 20ul
  )

let parse32_payload_and_pn_length : LP.parser32 Public.parse_payload_and_pn_length =
  LP.parse32_filter
    parse32_varint
    Public.payload_and_pn_length_prop
    (fun x -> Public.payload_and_pn_length_prop x)

let parse32_long_zero_rtt_body : LP.parser32 Public.parse_long_zero_rtt_body =
  parse32_common_long `LP.parse32_nondep_then` parse32_payload_and_pn_length

let parse32_long_handshake_body : LP.parser32 Public.parse_long_handshake_body =
  parse32_common_long `LP.parse32_nondep_then` parse32_payload_and_pn_length

let parse32_long_initial_body : LP.parser32 Public.parse_long_initial_body =
    parse32_common_long `LP.parse32_nondep_then` (
      LP.parse32_bounded_vlgenbytes 0 0ul token_max_len (U32.uint_to_t token_max_len) (parse32_bounded_varint 0ul (U32.uint_to_t token_max_len)) `LP.parse32_nondep_then`
      parse32_payload_and_pn_length
    )

let parse32_long_retry_body : LP.parser32 Public.parse_long_retry_body =
  parse32_common_long `LP.parse32_nondep_then` LP.parse32_bounded_vlbytes 0 0ul 20 20ul  

#push-options "--z3rlimit 32 --max_fuel 8 --max_ifuel 8 --initial_fuel 8 --initial_ifuel 8"

let parse32_header_body
  (short_dcid_len: short_dcid_len_t)
  (x: LPB.bitsum'_key_type Public.first_byte)
: Tot (LP.parser32 (dsnd (Public.parse_header_body short_dcid_len x)))
= match x with
  | (| Public.Short, (| (), () |) |) ->
    LP.parse32_weaken (LP.strong_parser_kind 0 20 None) (LP.parse32_flbytes (U32.v short_dcid_len) short_dcid_len)
  | (| Public.Long, (| (), (| Public.Initial, () |) |) |) ->
    parse32_long_initial_body
  | (| Public.Long, (| (), (| Public.ZeroRTT, () |) |) |) ->
    parse32_long_zero_rtt_body
  | (| Public.Long, (| (), (| Public.Handshake, () |) |) |) ->
    parse32_long_handshake_body
  | (| Public.Long, (| (), (| Public.Retry, () |) |) |) ->
    parse32_long_retry_body

#pop-options

let parse32_public_header
  (short_dcid_len: short_dcid_len_t)
: Tot (LP.parser32 (Public.parse_header short_dcid_len))
= LPB.parse32_bitsum
    Public.first_byte
    (Public.first_byte_of_header short_dcid_len)
    (Public.header_body_type short_dcid_len)
    (Public.header_synth short_dcid_len)
    LP.parse32_u8
    (Public.parse_header_body short_dcid_len)
    (parse32_header_body short_dcid_len)

let serialize32_common_long : LP.serializer32 Public.serialize_common_long =
  LP.serialize32_u32 `LP.serialize32_nondep_then` (
    LP.serialize32_bounded_vlbytes 0 20 `LP.serialize32_nondep_then`
    LP.serialize32_bounded_vlbytes 0 20
  )

let serialize32_payload_and_pn_length : LP.serializer32 Public.serialize_payload_and_pn_length =
  LP.serialize32_filter
    serialize32_varint
    Public.payload_and_pn_length_prop

let serialize32_long_zero_rtt_body : LP.serializer32 Public.serialize_long_zero_rtt_body =
  serialize32_common_long `LP.serialize32_nondep_then` serialize32_payload_and_pn_length

let serialize32_long_handshake_body : LP.serializer32 Public.serialize_long_handshake_body =
  serialize32_common_long `LP.serialize32_nondep_then` serialize32_payload_and_pn_length
/
QUIC.UInt62.fst.checked QUIC.Spec.VarInt.fst.checked QUIC.Spec.PacketNumber.fst.checked QUIC.Spec.Lemmas.fst.checked QUIC.Spec.Header.Public.fst.checked QUIC.Spec.Header.Parse.fst.checked QUIC.Spec.Header.fst.checked QUIC.Spec.fst.checked QUIC.Secret.Seq.fsti.checked prims.fst.checked LowParse.SLow.BitSum.fst.checked LowParse.SLow.fst.checked LowParse.Bytes32.fst.checked LowParse.BitFields.fsti.checked Lib.RawIntTypes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Int.Cast.fst.checked FStar.Endianness.fsti.checked
QUIC.TotSpec.fst
LowParse.SLow.Base.serializer32 QUIC.Spec.Header.Public.serialize_long_initial_body
LowParse.SLow.Combinators.serialize32_nondep_then LowParse.Spec.Combinators.and_then_kind LowParse.Spec.Int.parse_u32_kind LowParse.Spec.VLData.parse_bounded_vldata_strong_kind LowParse.Spec.BoundedInt.log256' LowParse.Spec.Bytes.parse_all_bytes_kind QUIC.Spec.Header.Public.common_long_t QUIC.Spec.Header.Public.parse_common_long QUIC.Spec.Header.Public.serialize_common_long QUIC.TotSpec.serialize32_common_long LowParse.Spec.VLGen.parse_bounded_vlgen_kind QUIC.Spec.VarInt.parse_varint_kind QUIC.Spec.Base.token_max_len LowParse.Spec.Combinators.parse_filter_kind FStar.Pervasives.Native.tuple2 LowParse.Spec.Bytes.parse_bounded_vlbytes_t QUIC.Spec.Header.Public.payload_and_pn_length_t' LowParse.Spec.Combinators.nondep_then LowParse.Spec.Bytes.parse_bounded_vlgenbytes QUIC.Spec.VarInt.parse_bounded_varint QUIC.Spec.Header.Public.parse_payload_and_pn_length LowParse.Spec.Combinators.serialize_nondep_then LowParse.Spec.Bytes.serialize_bounded_vlgenbytes QUIC.Spec.VarInt.serialize_bounded_varint QUIC.Spec.Header.Public.serialize_payload_and_pn_length LowParse.SLow.Bytes.serialize32_bounded_vlgenbytes QUIC.TotSpec.serialize32_bounded_varint QUIC.TotSpec.serialize32_payload_and_pn_length
let serialize32_long_initial_body:LP.serializer32 Public.serialize_long_initial_body =
  
serialize32_common_long
`LP.serialize32_nondep_then`
((LP.serialize32_bounded_vlgenbytes 0 token_max_len (serialize32_bounded_varint 0 (token_max_len)))
  `LP.serialize32_nondep_then`
  serialize32_payload_and_pn_length)