val print : s: Prims.string -> FStar.HyperStack.ST.ST Prims.unit
let print s = discard (IO.debug_print_string (prefix^": "^s^".\n"))
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))
/
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
s: Prims.string -> FStar.HyperStack.ST.ST Prims.unit
Prims.string MiTLS.Test.StAE.discard FStar.IO.debug_print_string Prims.op_Hat MiTLS.Test.StAE.prefix Prims.unit
let print s =
  
discard (IO.debug_print_string (prefix ^ ": " ^ s ^ ".\n"))