val print_string : s: Prims.string -> FStar.Pervasives.Dv Prims.unit
let print_string s = print_string (prefix ^ ": " ^ s ^ ".\n")
module MiTLS.Test.AEAD
open MiTLS

open FStar.HyperStack.ST
open FStar.HyperStack.IO
module HS = FStar.HyperStack

open MiTLS.TLSConstants
open MiTLS.TLSInfo
open FStar.Bytes
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Hashing.Spec.fst.checked MiTLS.EverCrypt.fsti.checked MiTLS.AEADProvider.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.IO.fst.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked C.fst.checked
MiTLS.Test.AEAD.fst
s: Prims.string -> FStar.Pervasives.Dv Prims.unit
Prims.string FStar.HyperStack.IO.print_string Prims.op_Hat MiTLS.Test.AEAD.prefix Prims.unit
let print_string s =
  
print_string (prefix ^ ": " ^ s ^ ".\n")