let incrementable (#i: index) (s: state i) (h: HS.mem { invariant h s }) =
  Secret.v (g_next_packet_number s h) + 1 < pow2 62
let incrementable (#i: index) (s: state i) (h: HS.mem{invariant h s}) =
Secret.v (g_next_packet_number s h) + 1 < pow2 62
QUIC.fsti.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.Cipher.fsti.checked Spec.Agile.AEAD.fsti.checked QUIC.Spec.PacketNumber.Base.fst.checked QUIC.Spec.Header.Parse.fsti.checked QUIC.Spec.fsti.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Int.fsti.checked QUIC.Impl.Header.Base.fst.checked QUIC.Impl.fsti.checked prims.fst.checked Model.QUIC.fsti.checked Model.Indexing.fsti.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lib.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverCrypt.Helpers.fsti.checked EverCrypt.Error.fsti.checked
QUIC.fsti
QUIC.index QUIC.state FStar.Monotonic.HyperStack.mem QUIC.invariant Prims.op_LessThan Prims.op_Addition QUIC.Secret.Int.Base.v Lib.IntTypes.U64 Lib.IntTypes.SEC QUIC.g_next_packet_number Prims.pow2 Prims.bool
module QUIC

module QSpec = QUIC.Spec
module QImpl = QUIC.Impl
module QImplBase = QUIC.Impl.Header.Base
module QModel = Model.QUIC
module PN = QUIC.Spec.PacketNumber.Base

module Secret = QUIC.Secret.Int

module I = Model.Indexing
module G = FStar.Ghost
module B = LowStar.Buffer
module S = FStar.Seq
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST

module U64 = FStar.UInt64
module U32 = FStar.UInt32
module U8 = FStar.UInt8

open FStar.HyperStack
open FStar.HyperStack.ST

open EverCrypt.Helpers
open EverCrypt.Error

#set-options "--fuel 0 --ifuel 0"

type nat62 = n:nat{n < pow2 62}

let cipher_keysize (a:QSpec.ea) =
  Spec.Agile.Cipher.key_length (Spec.Agile.AEAD.cipher_alg_of_supported_alg a)

/// Low-level types used in this API
/// --------------------------------

let u2 = QImpl.u2
let u4 = QImpl.u4
let u62 = QImpl.u62

val index:eqtype

val alg: index -> GTot QSpec.ea
val halg: index -> GTot QSpec.ha

let traffic_secret i =
  Spec.Hash.Definitions.bytes_hash (halg i)

// Switch state: either QModel or QImpl
val state: index -> Type u#1

val footprint: #i:index -> HS.mem -> state i -> GTot B.loc
val invariant: #i:index -> HS.mem -> state i -> Type0

val g_traffic_secret: #i:index -> state i -> HS.mem -> GTot (traffic_secret i)
val g_initial_packet_number: #i:index -> (s: state i) -> (h: HS.mem) -> GTot PN.packet_number_t
val g_last_packet_number: #i:index -> (s:state i) -> (h: HS.mem { invariant h s }) ->
  GTot (pn: PN.packet_number_t {
    let open Lib.IntTypes in
    Secret.v pn >= Secret.v #U64 #SEC (g_initial_packet_number s h)
  })
val g_next_packet_number: #i:index -> (s:state i) -> (h: HS.mem { invariant h s }) ->
  GTot (pn: PN.packet_number_t {
    let open Lib.IntTypes in
    Secret.v pn >= Secret.v #U64 #SEC (g_initial_packet_number s h)
  })
val incrementable : s: QUIC.state i -> h: FStar.Monotonic.HyperStack.mem{QUIC.invariant h s} -> Prims.GTot Prims.bool
s: QUIC.state i -> h: FStar.Monotonic.HyperStack.mem{QUIC.invariant h s} -> Prims.GTot Prims.bool