val rpn_of_nat (j: nat{j < max_ctr}) : rpn
let rpn_of_nat (j:nat{j < max_ctr}) : rpn = U64.uint_to_t j
val rpn_of_nat (j: nat{j < max_ctr}) : rpn
let rpn_of_nat (j: nat{j < max_ctr}) : rpn =
U64.uint_to_t j
Model.QUIC.fsti.checked
Spec.Agile.Cipher.fsti.checked Spec.Agile.AEAD.fsti.checked QUIC.UInt62.fst.checked QUIC.Spec.PacketNumber.Base.fst.checked QUIC.Spec.Header.Parse.fsti.checked QUIC.Spec.Header.Base.fst.checked QUIC.Spec.Header.fsti.checked QUIC.Spec.fsti.checked QUIC.Secret.Int.fsti.checked prims.fst.checked Model.PNE.fsti.checked Model.Indexing.fsti.checked Model.Helpers.fsti.checked Model.AEAD.fsti.checked Mem.fst.checked LowStar.Modifies.fst.checked LowParse.BitFields.fsti.checked Lib.RawIntTypes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt128.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.fst.checked
Model.QUIC.fsti
Prims.nat Prims.b2t Prims.op_LessThan Model.QUIC.max_ctr FStar.UInt64.uint_to_t Model.QUIC.rpn
module Model.QUIC

module HS = FStar.HyperStack
module I = Model.Indexing
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module U128 = FStar.UInt128
module M = LowStar.Modifies

module Spec = QUIC.Spec
module QH = QUIC.Spec.Header
module AE = Model.AEAD
module SAE = Spec.Agile.AEAD
module PNE = Model.PNE
module SPNE = Spec.Agile.Cipher
module BF = LowParse.BitFields
module U62 = QUIC.UInt62
module Secret = QUIC.Secret.Int

open FStar.UInt32
open Mem

type id = i:AE.id & j:PNE.id{PNE.is_safe j <==> AEAD.is_safe i}

let safe (i:id) = AEAD.is_safe (dfst i)
let safe_id = i:id{safe i}
let unsafe (i:id) = not (safe i)
let unsafe_id = i:id{unsafe i}

/// Package for QUIC plaintexts
/// (i.e. the payload of QUIC packets)
/// This would be implemented as a serializable list of frames
/// (using EverParse refined lists)

type qplain_len = n:AEAD.plain_length_at_least 3{n < Spec.max_plain_length}
let pnl = PNE.pne_plain_length

val pne_pkg: PNE.pne_plain_pkg

noeq type info = {
  region: r:subq{r `HS.disjoint` q_ae_region};
}

let max_ctr = pow2 62 - 1
type epn (nl:pnl) = Spec.lbytes nl
type pn = n:nat{n <= max_ctr}
val rpn_of_nat (j: nat{j < max_ctr}) : rpn
j: Prims.nat{j < Model.QUIC.max_ctr} -> Model.QUIC.rpn