val receivable : s: QUIC.state i -> h: FStar.Monotonic.HyperStack.mem{QUIC.invariant h s} -> Prims.GTot Prims.bool
let receivable (#i: index) (s: state i) (h: HS.mem { invariant h s }) =
  Secret.v (g_last_packet_number s h) + 1 < pow2 62
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)
  })

let incrementable (#i: index) (s: state i) (h: HS.mem { invariant h s }) =
  Secret.v (g_next_packet_number s h) + 1 < pow2 62
/
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
s: QUIC.state i -> h: FStar.Monotonic.HyperStack.mem{QUIC.invariant h s} -> Prims.GTot Prims.bool
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_last_packet_number Prims.pow2 Prims.bool
let receivable (#i: index) (s: state i) (h: HS.mem{invariant h s}) =
  
Secret.v (g_last_packet_number s h) + 1 < pow2 62