val 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})
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)))
val 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})
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)))
QUIC.TotSpec.fst.checked
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
QUIC.Spec.PacketNumber.Base.last_packet_number_t QUIC.Spec.PacketNumber.Base.packet_number_length_t LowParse.Spec.BoundedInt.bounded_integer QUIC.Secret.Int.Base.v Lib.IntTypes.U32 Lib.IntTypes.SEC Lib.IntTypes.to_u64 Lib.IntTypes.U64 Lib.IntTypes.PUB FStar.UInt64.uint_to_t QUIC.Spec.PacketNumber.expand_pn' Prims.op_Subtraction Lib.RawIntTypes.uint_to_nat FStar.UInt32.v QUIC.Spec.PacketNumber.Base.packet_number_t' Prims.eq2 QUIC.Spec.PacketNumber.synth_packet_number
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))
val 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})

    last: QUIC.Spec.PacketNumber.Base.last_packet_number_t ->
    pn_len: QUIC.Spec.PacketNumber.Base.packet_number_length_t ->
    npn: LowParse.Spec.BoundedInt.bounded_integer (QUIC.Secret.Int.Base.v pn_len)
  -> pn:
    QUIC.Spec.PacketNumber.Base.packet_number_t' last pn_len
      {pn == QUIC.Spec.PacketNumber.synth_packet_number last pn_len npn}