val _traffic_secret:list Secret.uint8
val _traffic_secret:list Secret.uint8
let _traffic_secret: list Secret.uint8 = [
  Secret.hide #Secret.U8 0x48uy; Secret.hide #Secret.U8 0xc4uy; Secret.hide #Secret.U8 0x30uy; Secret.hide #Secret.U8 0x9buy; Secret.hide #Secret.U8 0x5fuy; Secret.hide #Secret.U8 0x27uy; Secret.hide #Secret.U8 0x52uy; Secret.hide #Secret.U8 0xe8uy;
  Secret.hide #Secret.U8 0x12uy; Secret.hide #Secret.U8 0x7buy; Secret.hide #Secret.U8 0x1uy;  Secret.hide #Secret.U8 0x66uy; Secret.hide #Secret.U8 0x5uy;  Secret.hide #Secret.U8 0x5auy; Secret.hide #Secret.U8 0x9auy; Secret.hide #Secret.U8 0x56uy;
  Secret.hide #Secret.U8 0xe5uy; Secret.hide #Secret.U8 0xf9uy; Secret.hide #Secret.U8 0x6uy;  Secret.hide #Secret.U8 0x31uy; Secret.hide #Secret.U8 0xe0uy; Secret.hide #Secret.U8 0x84uy; Secret.hide #Secret.U8 0x85uy; Secret.hide #Secret.U8 0xe0uy;
  Secret.hide #Secret.U8 0xf8uy; Secret.hide #Secret.U8 0x9euy; Secret.hide #Secret.U8 0x9cuy; Secret.hide #Secret.U8 0xecuy; Secret.hide #Secret.U8 0x4auy; Secret.hide #Secret.U8 0xdeuy; Secret.hide #Secret.U8 0xb6uy; Secret.hide #Secret.U8 0x50uy;
]
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

let idx = {
  Q.hash_alg = Spec.Hash.Definitions.SHA2_256;
  Q.aead_alg = Spec.Agile.AEAD.CHACHA20_POLY1305;
}

inline_for_extraction
/
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
Prims.list (Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC)
Prims.Cons Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC QUIC.Secret.Int.hide Lib.IntTypes.PUB FStar.UInt8.__uint_to_t Prims.Nil
let _traffic_secret:list Secret.uint8 =
  
[
  Secret.hide #Secret.U8 0x48uy; Secret.hide #Secret.U8 0xc4uy; Secret.hide #Secret.U8 0x30uy;
  Secret.hide #Secret.U8 0x9buy; Secret.hide #Secret.U8 0x5fuy; Secret.hide #Secret.U8 0x27uy;
  Secret.hide #Secret.U8 0x52uy; Secret.hide #Secret.U8 0xe8uy; Secret.hide #Secret.U8 0x12uy;
  Secret.hide #Secret.U8 0x7buy; Secret.hide #Secret.U8 0x1uy; Secret.hide #Secret.U8 0x66uy;
  Secret.hide #Secret.U8 0x5uy; Secret.hide #Secret.U8 0x5auy; Secret.hide #Secret.U8 0x9auy;
  Secret.hide #Secret.U8 0x56uy; Secret.hide #Secret.U8 0xe5uy; Secret.hide #Secret.U8 0xf9uy;
  Secret.hide #Secret.U8 0x6uy; Secret.hide #Secret.U8 0x31uy; Secret.hide #Secret.U8 0xe0uy;
  Secret.hide #Secret.U8 0x84uy; Secret.hide #Secret.U8 0x85uy; Secret.hide #Secret.U8 0xe0uy;
  Secret.hide #Secret.U8 0xf8uy; Secret.hide #Secret.U8 0x9euy; Secret.hide #Secret.U8 0x9cuy;
  Secret.hide #Secret.U8 0xecuy; Secret.hide #Secret.U8 0x4auy; Secret.hide #Secret.U8 0xdeuy;
  Secret.hide #Secret.U8 0xb6uy; Secret.hide #Secret.U8 0x50uy
]