val pre_id : role: MiTLS.TLSConstants.role -> MiTLS.TLSInfo.id
let pre_id (role:role) =
  let cr  = Bytes.create 32ul 0z in
  let sr  = Bytes.create 32ul 0z in
  let kdf = PRF_TLS_1p2 kdf_label Hashing.Spec.SHA2_256 in
  let msid = StandardMS PMS.DummyPMS (cr @| sr) kdf in
  ID12 TLS_1p2 msid kdf (AEAD EverCrypt.AES256_GCM Hashing.Spec.SHA2_256) cr sr role
module MiTLS.Test.StAE
open MiTLS
// adapted from test/TestGCM

open FStar.Bytes // for @|
open FStar.Error
open FStar.Printf
open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.TLSInfo
open MiTLS.Range

module StAE = MiTLS.StAE
module Range = MiTLS.Range
module DH = MiTLS.CommonDH

open FStar.HyperStack
open FStar.HyperStack.ST

let prefix = "Test.StAE"
let ok: ref bool = ralloc root true

val discard: bool -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
let discard _ = ()
let print s = discard (IO.debug_print_string (prefix^": "^s^".\n"))
// let print = C.String,print
// let print = FStar.HyperStack.IO.print_string

let eprint s : St unit = ok := false; print ("ERROR: "^s)
let nprint s : St unit = print s

#set-options "--admit_smt_queries true"
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.StAE.fst.checked MiTLS.Range.fst.checked MiTLS.PMS.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.EverCrypt.fsti.checked MiTLS.DataStream.fst.checked MiTLS.Content.fst.checked MiTLS.CommonDH.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.IO.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked C.fst.checked
MiTLS.Test.StAE.fst
role: MiTLS.TLSConstants.role -> MiTLS.TLSInfo.id
MiTLS.TLSConstants.role MiTLS.TLSInfo.ID12 MiTLS.Parsers.ProtocolVersion.TLS_1p2 MiTLS.CipherSuite.AEAD MiTLS.EverCrypt.AES256_GCM Spec.Hash.Definitions.SHA2_256 MiTLS.TLSInfo.msId MiTLS.TLSInfo.StandardMS MiTLS.PMS.DummyPMS FStar.Bytes.op_At_Bar MiTLS.TLSConstants.prePrfAlg MiTLS.TLSConstants.PRF_TLS_1p2 MiTLS.TLSConstants.kdf_label FStar.Bytes.lbytes FStar.UInt32.v FStar.UInt32.uint_to_t FStar.UInt32.t Prims.l_Forall Prims.b2t FStar.UInt32.lt Prims.eq2 FStar.UInt8.t FStar.Bytes.get FStar.UInt8.uint_to_t FStar.Bytes.create FStar.UInt32.__uint_to_t FStar.UInt8.__uint_to_t MiTLS.TLSInfo.id
let pre_id (role: role) =
  
let cr = Bytes.create 32ul 0uy in
let sr = Bytes.create 32ul 0uy in
let kdf = PRF_TLS_1p2 kdf_label Hashing.Spec.SHA2_256 in
let msid = StandardMS PMS.DummyPMS (cr @| sr) kdf in
ID12 TLS_1p2 msid kdf (AEAD EverCrypt.AES256_GCM Hashing.Spec.SHA2_256) cr sr role