val main : cafile: Prims.string -> cert: Prims.string -> key: Prims.string -> _: Prims.unit
  -> FStar.HyperStack.ST.STATE C.exit_code
let main cafile cert key () = // could try with different client and server configs
//  test ({ defaultConfig with min_version = TLS_1p2; max_version = TLS_1p2; });
//  test ({ defaultConfig with min_version = TLS_1p2; max_version = TLS_1p3; });
  let pki = PKI.init cafile // CA file
     [cert, // Cert file
      key,  // Private key file
      true] in // Universal (use for any SNI)
  test ({ defaultConfig with
    min_version = TLS_1p3;
    max_version = TLS_1p3;
    cert_callbacks = PKI.tls_callbacks pki;
  });
  PKI.free pki;
  if !ok then C.EXIT_SUCCESS else C.EXIT_FAILURE
module MiTLS.Test.Handshake
open MiTLS
// adapted from test/TestHandshake

open FStar.Bytes // for @|
open FStar.Error
open FStar.Printf
open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.TLSInfo
open MiTLS.Range
open MiTLS.HandshakeMessages
open MiTLS.HandshakeLog
open MiTLS.Negotiation
open FStar.HyperStack
open FStar.HyperStack.ST

module StAE = MiTLS.StAE
module Range = MiTLS.Range
module Handshake = MiTLS.Old.Handshake
module PKI = MiTLS.PKI

#set-options "--admit_smt_queries true"

let prefix = "Test.Handshake"
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

let first_bytes b =
  let open FStar.UInt32 in
  let small = 10ul in
  sprintf "%s (%ul bytes)"
    ( if Bytes.len b <=^ (small +^ small)
      then Bytes.hex_of_bytes b
      else (
        Bytes.hex_of_bytes (Bytes.sub b 0ul small) ^
        "..." ^
        Bytes.hex_of_bytes (Bytes.sub b (Bytes.len b -^ small) small)))
    (len b)



// TLS handshake prefix
let test config: St unit =
  let rid = new_region root in
  let i = Test.StAE.id12 in
  let client = Handshake.create rid config Client in
  let out0 = Handshake.next_fragment client i in
  match out0 with
  | Correct(HandshakeLog.Outgoing (Some f) _ _) ->
    let (|rg, ch|) = f in
    nprint ("----client-hello---> "^first_bytes ch);
    let server = Handshake.create rid config Server in
    let _ = Handshake.recv_fragment server rg ch in
    let out1 = Handshake.next_fragment server i in
    (match out1 with
    | Correct(HandshakeLog.Outgoing (Some f) _ _) ->
      let (|rg, sh|) = f in
      nprint ("<---server-hello---- "^first_bytes sh);
      let _ = Handshake.recv_fragment client rg sh in
      let out2 = Handshake.next_fragment server i in
      (match out2 with
      | Correct(HandshakeLog.Outgoing (Some f) _ _) ->
        let (|rg, sf|) = f in
        nprint ("<--server-finished-- "^first_bytes sf);
        let _ = Handshake.recv_fragment client rg sf in
        let out3 = Handshake.next_fragment client i in
        (match out3 with
        | Correct(HandshakeLog.Outgoing (Some f) _ _) ->
          let (|rg, cf|) = f in
          nprint ("--client-finished---> "^first_bytes cf);
          let _ = Handshake.recv_fragment server rg cf in
          let out4 = Handshake.next_fragment server i in
          (match out4 with
          | Correct(HandshakeLog.Outgoing (Some f) _ _) ->
            let (|rg, nst|) = f in
            nprint ("<--session-ticket-- "^first_bytes nst);
            let _ = Handshake.recv_fragment client rg nst in
            nprint "Done"
          | _ -> eprint "client failed to emit session ticket")
        | _ -> eprint "client failed to return finished flight")
      | _ -> eprint "server failed to return end of second flight")
    | Error (_,s) -> eprint ("server failed to build second flight: "^s)
    | _ -> eprint ("server failed to return second flight."))
  | Error (_,s) -> eprint ("client failed to build first flight: "^s)
  | _ -> eprint ("client failed to return first flight.")
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Test.StAE.fst.checked MiTLS.StAE.fst.checked MiTLS.Range.fst.checked MiTLS.PKI.fsti.checked MiTLS.Old.Handshake.fsti.checked MiTLS.Negotiation.fst.checked MiTLS.HandshakeMessages.fsti.checked MiTLS.HandshakeLog.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.Handshake.fst
cafile: Prims.string -> cert: Prims.string -> key: Prims.string -> _: Prims.unit
  -> FStar.HyperStack.ST.STATE C.exit_code
Prims.string Prims.unit C.EXIT_SUCCESS Prims.bool C.EXIT_FAILURE C.exit_code FStar.HyperStack.ST.op_Bang FStar.Heap.trivial_preorder MiTLS.Test.Handshake.ok MiTLS.PKI.free MiTLS.Test.Handshake.test MiTLS.TLSConstants.config MiTLS.TLSConstants.Mkconfig MiTLS.Parsers.ProtocolVersion.TLS_1p3 MiTLS.TLSConstants.__proj__Mkconfig__item__is_quic MiTLS.TLSInfo.defaultConfig MiTLS.TLSConstants.__proj__Mkconfig__item__cipher_suites MiTLS.TLSConstants.__proj__Mkconfig__item__named_groups MiTLS.TLSConstants.__proj__Mkconfig__item__signature_algorithms MiTLS.TLSConstants.__proj__Mkconfig__item__hello_retry MiTLS.TLSConstants.__proj__Mkconfig__item__offer_shares MiTLS.TLSConstants.__proj__Mkconfig__item__custom_extensions MiTLS.TLSConstants.__proj__Mkconfig__item__use_tickets MiTLS.TLSConstants.__proj__Mkconfig__item__send_ticket MiTLS.TLSConstants.__proj__Mkconfig__item__check_client_version_in_pms_for_old_tls MiTLS.TLSConstants.__proj__Mkconfig__item__request_client_certificate MiTLS.TLSConstants.__proj__Mkconfig__item__non_blocking_read MiTLS.TLSConstants.__proj__Mkconfig__item__max_early_data MiTLS.TLSConstants.__proj__Mkconfig__item__max_ticket_age MiTLS.TLSConstants.__proj__Mkconfig__item__safe_renegotiation MiTLS.TLSConstants.__proj__Mkconfig__item__extended_master_secret MiTLS.TLSConstants.__proj__Mkconfig__item__enable_tickets MiTLS.TLSConstants.__proj__Mkconfig__item__ticket_callback MiTLS.TLSConstants.__proj__Mkconfig__item__nego_callback MiTLS.TLSConstants.__proj__Mkconfig__item__alpn MiTLS.TLSConstants.__proj__Mkconfig__item__peer_name MiTLS.TLSConstants.cert_cb MiTLS.PKI.tls_callbacks FStar.Dyn.dyn MiTLS.PKI.init Prims.Cons FStar.Pervasives.Native.tuple3 FStar.Pervasives.Native.Mktuple3 Prims.Nil
let main cafile cert key () =
  
let pki = PKI.init cafile [cert, key, true] in
test ({
      defaultConfig with
      min_version = TLS_1p3;
      max_version = TLS_1p3;
      cert_callbacks = PKI.tls_callbacks pki
    });
PKI.free pki;
if !ok then C.EXIT_SUCCESS else C.EXIT_FAILURE