val reduce_pn' (pn_len: nat{pn_len < 4}) (pn: nat) : Tot nat
val reduce_pn' (pn_len: nat{pn_len < 4}) (pn: nat) : Tot nat
let reduce_pn'
  (pn_len: nat { pn_len < 4 })
  (pn: nat)
: Tot nat
= pn % (bound_npn' pn_len)
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
/
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
pn_len: Prims.nat{pn_len < 4} -> pn: Prims.nat -> Prims.nat
Prims.nat Prims.b2t Prims.op_LessThan Prims.op_Modulus QUIC.Spec.PacketNumber.Base.bound_npn'
let reduce_pn' (pn_len: nat{pn_len < 4}) (pn: nat) : Tot nat =
  
pn % (bound_npn' pn_len)