val serialize_packet_number_ext
  (last1 last2: last_packet_number_t)
  (pn_len: packet_number_length_t)
  (pn: packet_number_t)
: Lemma
  (requires (
    in_window (Secret.v pn_len - 1) (Secret.v last1) (Secret.v pn) /\
    in_window (Secret.v pn_len - 1) (Secret.v last2) (Secret.v pn)
  ))
  (ensures (
    serialize (serialize_packet_number last1 pn_len) pn == serialize (serialize_packet_number last2 pn_len) pn
  ))
val serialize_packet_number_ext
  (last1 last2: last_packet_number_t)
  (pn_len: packet_number_length_t)
  (pn: packet_number_t)
: Lemma
  (requires (
    in_window (Secret.v pn_len - 1) (Secret.v last1) (Secret.v pn) /\
    in_window (Secret.v pn_len - 1) (Secret.v last2) (Secret.v pn)
  ))
  (ensures (
    serialize (serialize_packet_number last1 pn_len) pn == serialize (serialize_packet_number last2 pn_len) pn
  ))
let serialize_packet_number_ext
  last1 last2 pn_len pn
= serialize_synth_eq 
    (lift_parser (parse_reduced_pn pn_len))
    (synth_packet_number last1 pn_len)
    (lift_serializer (serialize_reduced_pn pn_len))
    (synth_packet_number_recip last1 pn_len)
    ()
    pn;
  serialize_synth_eq 
    (lift_parser (parse_reduced_pn pn_len))
    (synth_packet_number last2 pn_len)
    (lift_serializer (serialize_reduced_pn pn_len))
    (synth_packet_number_recip last2 pn_len)
    ()
    pn
module QUIC.Spec.PacketNumber
open QUIC.Spec.PacketNumber.Lemmas
open LowParse.Spec.Combinators
open LowParse.Spec.BoundedInt

(* From https://tools.ietf.org/html/draft-ietf-quic-transport-22#appendix-A *)

module Cast = FStar.Int.Cast
module U64 = FStar.UInt64
module U32 = FStar.UInt32
module U16 = FStar.UInt16
module U8 = FStar.UInt8

module Secret = QUIC.Secret.Int

let reduce_pn'
  (pn_len: nat { pn_len < 4 })
  (pn: nat)
: Tot nat
= pn % (bound_npn' pn_len)

let in_window_self (pn_len: nat { pn_len < 4 }) (pn:nat) : Lemma
  (in_window pn_len pn (if pn = 0 then 0 else pn - 1))
= ()

#push-options "--max_fuel 2 --initial_fuel 2 --max_ifuel 1 --initial_ifuel 1"
let expand_pn'
  (pn_len: nat { pn_len < 4 })
  (last: nat { last + 1 < pow2 62})
  (npn: nat { npn < bound_npn' pn_len })
: Tot (pn: nat { pn < pow2 62 /\ in_window pn_len last pn /\ pn % bound_npn' pn_len == npn })
=
  let open FStar.Mul in
  let open FStar.Math.Lemmas in
  let expected = last + 1 in
  let bound = bound_npn' pn_len in
  let candidate = replace_modulo' expected bound npn in
  lemma_replace_modulo_bound expected (8*(pn_len+1)) npn 62;
  if candidate <= last + 1 - bound/2
     && candidate < pow2 62 - bound then // the test for overflow (candidate < pow2 62 - bound) is not present in draft 22.
    let _ = lemma_mod_plus candidate 1 bound in
    candidate + bound
  else if candidate > last + 1 + bound/2
          && candidate >= bound then // in draft 22 the test for underflow (candidate >= bound) uses a strict inequality, which makes it impossible to expand npn to 0
    let _ = lemma_mod_plus candidate (-1) bound in
    candidate - bound
  else candidate
#pop-options

let max (a b:int) : Tot (n:int{n >= a /\ n >= b}) =
  if a > b then a else b // this must exist somewhere...

let lemma_uniqueness_in_window (pn_len: nat { pn_len < 4 }) (last: nat { last < pow2 62 }) (x: nat {x < pow2 62}) (y:nat {y < pow2 62}) : Lemma
  (requires (
    let h = bound_npn' pn_len in
    in_window pn_len last x /\
    in_window pn_len last y /\
    x%h = y%h))
  (ensures x = y) =
  let open FStar.Math.Lemmas in
  pow2_lt_compat 62 (8 `op_Multiply` (pn_len+1));
  let h = bound_npn' pn_len in
  if last+1 < h/2 && x < h then
    lemma_mod_plus_injective h 0 x y
  else if last+1 >= pow2 62 - h/2 && x >= pow2 62 - h then
    let low = pow2 62 - h in
    lemma_mod_plus_injective h low (x-low) (y-low)
  else
    let low = max (last+2-h/2) 0 in
    lemma_mod_plus_injective h low (x-low) (y-low)

val lemma_parse_pn_correct : (pn_len: nat { pn_len < 4 }) -> last:nat{last+1 < pow2 62} -> (pn: nat { pn < U64.v U62.bound }) -> Lemma
  (requires in_window pn_len last pn)
  (ensures expand_pn' pn_len last (reduce_pn' pn_len pn) = pn)

let lemma_parse_pn_correct pn_len last pn =
  lemma_uniqueness_in_window pn_len last pn (expand_pn' pn_len last (reduce_pn' pn_len pn))

#push-options "--z3rlimit 16"

inline_for_extraction
let synth_packet_number
  (last: last_packet_number_t)
  (pn_len: packet_number_length_t)
  (npn: bounded_integer (Secret.v pn_len))
: GTot (packet_number_t' last pn_len)
= Secret.to_u64 (U64.uint_to_t (expand_pn' (Secret.v pn_len - 1) (Secret.v last) (U32.v npn)))

#pop-options

let synth_packet_number_recip
  (last: last_packet_number_t)
  (pn_len: packet_number_length_t)
  (pn: packet_number_t' last pn_len)
: GTot  (bounded_integer (Secret.v pn_len))
= U32.uint_to_t (reduce_pn' (Secret.v pn_len - 1) (Secret.v pn))

#push-options "--z3rlimit 512"

let synth_packet_number_injective
  (last: last_packet_number_t)
  (pn_len: packet_number_length_t)
: Lemma
  (synth_injective #(bounded_integer (Secret.v pn_len)) #(packet_number_t' last pn_len) (synth_packet_number last pn_len))
  [SMTPat 
    (synth_injective #(bounded_integer (Secret.v pn_len)) #(packet_number_t' last pn_len) (synth_packet_number last pn_len))
  ]
= synth_inverse_intro' #(packet_number_t' last pn_len) #(bounded_integer (Secret.v pn_len)) (synth_packet_number_recip last pn_len) (synth_packet_number last pn_len) (fun pn -> ());
  synth_inverse_synth_injective #(bounded_integer (Secret.v pn_len)) #(packet_number_t' last pn_len) (synth_packet_number last pn_len) (synth_packet_number_recip last pn_len)

let synth_packet_number_recip_inverse
  (last: last_packet_number_t)
  (pn_len: packet_number_length_t)
: Lemma
  (synth_inverse #(bounded_integer (Secret.v pn_len)) #(packet_number_t' last pn_len) (synth_packet_number last pn_len) (synth_packet_number_recip last pn_len))
  [SMTPat (synth_inverse #(bounded_integer (Secret.v pn_len)) #(packet_number_t' last pn_len) (synth_packet_number last pn_len) (synth_packet_number_recip last pn_len))]
= synth_inverse_intro' #(bounded_integer (Secret.v pn_len)) #(packet_number_t' last pn_len) (synth_packet_number last pn_len) (synth_packet_number_recip last pn_len) (fun pn ->
    lemma_parse_pn_correct (Secret.v pn_len - 1) (Secret.v last) (Secret.v pn)
  )

#pop-options


let parse_reduced_pn
  (pn_len: packet_number_length_t)
  ()
: GTot (parser parse_packet_number_kind (bounded_integer (Secret.v pn_len)))
= weaken parse_packet_number_kind (parse_bounded_integer (Secret.v pn_len))

let parse_packet_number
  (last: last_packet_number_t)
  (pn_len: packet_number_length_t)
: Tot (parser parse_packet_number_kind (packet_number_t' last pn_len) )
= lift_parser (parse_reduced_pn pn_len) `parse_synth` synth_packet_number last pn_len

let parse_packet_number_kind'_correct
  last pn_len
= let p = parse_bounded_integer (Secret.v pn_len) `parse_synth` synth_packet_number last pn_len in
  let f
    (input: bytes)
  : Lemma
    (parse (parse_packet_number last pn_len) input == parse p input)
  = parse_synth_eq
      (lift_parser (parse_reduced_pn pn_len))
      (synth_packet_number last pn_len)
      input;
    parse_synth_eq
      (parse_bounded_integer (Secret.v pn_len))
      (synth_packet_number last pn_len)
      input
  in
  Classical.forall_intro f;
  parser_kind_prop_ext (total_constant_size_parser_kind (Secret.v pn_len)) (parse_packet_number last pn_len) p

let serialize_reduced_pn
  (pn_len: packet_number_length_t)
  (x: unit)
: GTot (serializer (parse_reduced_pn pn_len ()))
= serialize_weaken parse_packet_number_kind (serialize_bounded_integer (Secret.v pn_len))

let serialize_packet_number
  (last: last_packet_number_t)
  (pn_len: packet_number_length_t)
: Tot (serializer (parse_packet_number last pn_len))
= serialize_synth
    (lift_parser (parse_reduced_pn pn_len))
    (synth_packet_number last pn_len)
    (lift_serializer (serialize_reduced_pn pn_len))
    (synth_packet_number_recip last pn_len)
    ()
/
QUIC.Spec.PacketNumber.Lemmas.fst.checked QUIC.Secret.Int.fsti.checked prims.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.BoundedInt.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Int.Cast.fst.checked FStar.Classical.fsti.checked
QUIC.Spec.PacketNumber.fst

    last1: QUIC.Spec.PacketNumber.Base.last_packet_number_t ->
    last2: QUIC.Spec.PacketNumber.Base.last_packet_number_t ->
    pn_len: QUIC.Spec.PacketNumber.Base.packet_number_length_t ->
    pn: QUIC.Spec.PacketNumber.Base.packet_number_t
  -> FStar.Pervasives.Lemma
      (requires
        QUIC.Spec.PacketNumber.Base.in_window (QUIC.Secret.Int.Base.v pn_len - 1)
          (QUIC.Secret.Int.Base.v last1)
          (QUIC.Secret.Int.Base.v pn) /\
        QUIC.Spec.PacketNumber.Base.in_window (QUIC.Secret.Int.Base.v pn_len - 1)
          (QUIC.Secret.Int.Base.v last2)
          (QUIC.Secret.Int.Base.v pn))
      (ensures
        LowParse.Spec.Base.serialize (QUIC.Spec.PacketNumber.serialize_packet_number last1 pn_len)
          pn ==
        LowParse.Spec.Base.serialize (QUIC.Spec.PacketNumber.serialize_packet_number last2 pn_len)
          pn)
QUIC.Spec.PacketNumber.Base.last_packet_number_t QUIC.Spec.PacketNumber.Base.packet_number_length_t QUIC.Spec.PacketNumber.Base.packet_number_t LowParse.Spec.Combinators.serialize_synth_eq QUIC.Spec.PacketNumber.parse_packet_number_kind LowParse.Spec.BoundedInt.bounded_integer QUIC.Secret.Int.Base.v Lib.IntTypes.U32 Lib.IntTypes.SEC QUIC.Spec.PacketNumber.Base.packet_number_t' LowParse.Spec.Combinators.lift_parser QUIC.Spec.PacketNumber.parse_reduced_pn QUIC.Spec.PacketNumber.synth_packet_number LowParse.Spec.Combinators.lift_serializer QUIC.Spec.PacketNumber.serialize_reduced_pn QUIC.Spec.PacketNumber.synth_packet_number_recip Prims.unit
let serialize_packet_number_ext last1 last2 pn_len pn =
  
serialize_synth_eq (lift_parser (parse_reduced_pn pn_len))
  (synth_packet_number last1 pn_len)
  (lift_serializer (serialize_reduced_pn pn_len))
  (synth_packet_number_recip last1 pn_len)
  ()
  pn;
serialize_synth_eq (lift_parser (parse_reduced_pn pn_len))
  (synth_packet_number last2 pn_len)
  (lift_serializer (serialize_reduced_pn pn_len))
  (synth_packet_number_recip last2 pn_len)
  ()
  pn