let idx = {
  Q.hash_alg = Spec.Hash.Definitions.SHA2_256;
  Q.aead_alg = Spec.Agile.AEAD.CHACHA20_POLY1305;
}
let idx =
{ Q.hash_alg = Spec.Hash.Definitions.SHA2_256; Q.aead_alg = Spec.Agile.AEAD.CHACHA20_POLY1305 }
QUICTest.fst.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.AEAD.fsti.checked QUIC.UInt62.fst.checked QUIC.State.fsti.checked QUIC.Spec.PacketNumber.Base.fst.checked QUIC.Spec.fsti.checked QUIC.Secret.Seq.fsti.checked QUIC.Secret.Int.fsti.checked prims.fst.checked LowStar.Printf.fst.checked LowStar.Buffer.fst.checked Lib.RawIntTypes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverCrypt.Error.fsti.checked C.fst.checked
QUICTest.fst
QUIC.State.Mkindex Spec.Hash.Definitions.SHA2_256 Spec.Agile.AEAD.CHACHA20_POLY1305
module QUICTest
module B = LowStar.Buffer
module U62 = QUIC.UInt62
module U32 = FStar.UInt32
module U8 = FStar.UInt8
module HST = FStar.HyperStack.ST
module HS = FStar.HyperStack
module L = FStar.List.Tot
module Secret = QUIC.Secret.Int
module PN = QUIC.Spec.PacketNumber.Base
module Seq = QUIC.Secret.Seq
module Q = QUIC.State
module QS = QUIC.Spec

(* declassification for post tests *)
module ADMITDeclassify = Lib.RawIntTypes
val idx : QUIC.State.index
QUIC.State.index