val iter (xs: list (string * (unit -> St C.exit_code))) : St unit
val iter (xs: list (string * (unit -> St C.exit_code))) : St unit
let rec iter (xs:list (string * (unit -> St C.exit_code))) : St unit =
  match xs with
  | [] -> ()
  | (s,f) :: xs -> check s f; iter xs
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
/
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
xs: Prims.list (Prims.string * (_: Prims.unit -> FStar.HyperStack.ST.St C.exit_code))
  -> FStar.HyperStack.ST.St Prims.unit
Prims.list FStar.Pervasives.Native.tuple2 Prims.string Prims.unit C.exit_code MiTLS.Test.Main.iter MiTLS.Test.Main.check
let rec iter (xs: list (string * (unit -> St C.exit_code))) : St unit =
  
match xs with
| [] -> ()
| (s, f) :: xs ->
  check s f;
  iter xs