val iv : _: Prims.unit -> FStar.HyperStack.ST.STATE C.exit_code
let iv () = 
  IV.test(); 
  C.EXIT_SUCCESS
module MiTLS.Test.Main
open MiTLS

open FStar.HyperStack.ST
open FStar.HyperStack.IO

#set-options "--admit_smt_queries true"

inline_for_extraction
let check s (f: unit -> St C.exit_code): St unit =
  match f () with
  | C.EXIT_SUCCESS ->
      C.(ignore (fflush stdout); ignore (fflush stderr));
      print_string "✔ ";
      print_string s;
      print_string "\n"
  | C.EXIT_FAILURE ->
      C.(ignore (fflush stdout); ignore (fflush stderr));
      print_string "✘ ";
      print_string s;
      print_string "\n";
      C.exit 255l

let rec iter (xs:list (string * (unit -> St C.exit_code))) : St unit =
  match xs with
  | [] -> ()
  | (s,f) :: xs -> check s f; iter xs

let handshake () =
  Test.Handshake.main "CAFile.pem" "server-ecdsa.crt" "server-ecdsa.key" ()
/
prims.fst.checked MiTLS.Test.TLSConstants.fst.checked MiTLS.Test.StAE.fst.checked MiTLS.Test.Handshake.fst.checked MiTLS.Test.CommonDH.fst.checked MiTLS.Test.BufferBytes.fst.checked MiTLS.Test.AEAD.fst.checked MiTLS.Random.fst.checked MiTLS.KDF.Rekey.fst.checked MiTLS.IV.fst.checked MiTLS.FStar.Test.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Int32.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.IO.fst.checked C.fst.checked
MiTLS.Test.Main.fst
_: Prims.unit -> FStar.HyperStack.ST.STATE C.exit_code
Prims.unit C.EXIT_SUCCESS C.exit_code MiTLS.IV.test
let iv () =
  
IV.test ();
C.EXIT_SUCCESS