val print : s: Prims.string -> FStar.HyperStack.ST.ST Prims.unit
let print s = discard (IO.debug_print_string ("FFI| "^s^"\n"))
module MiTLS.FFI
open MiTLS


// A thin layer on top of TLS, adapting a bit our main API:
// - for TCP send & receive, we use callbacks provided by the application
// - for output traffic, we send fragment and send the whole message at once
// - for client connects, we block until the connection is sucessfully established
//
// We rely on higher-order; to be reconsidered once we compile to C/C++.

// TODO: guarantee (by typing) that we don't do stdio, and don't throw
//       exceptions, notably for incomplete pattern matching

open FStar.Bytes
open FStar.Error

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

open MiTLS.TLSConstants
open MiTLS.TLSInfo
module Range = MiTLS.Range
open MiTLS.Range
module Parse = MiTLS.Parse

open MiTLS.Mem
open MiTLS.DataStream
open MiTLS.TLS
//open FFICallbacks

open FStar.HyperStack.All
type cbytes = string
#set-options "--admit_smt_queries true"

let pair_of_ints = int & int

(* A flag for runtime debugging of ffi data.
   The F* normalizer will erase debug prints at extraction
   when this flag is set to false. *)
val discard: bool -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
/
prims.fst.checked MiTLS.Transport.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.TLS.fst.checked MiTLS.Ticket.fst.checked MiTLS.Range.fst.checked MiTLS.Parse.fst.checked MiTLS.Old.Handshake.fsti.checked MiTLS.Negotiation.fst.checked MiTLS.Mem.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.Extensions.fsti.checked MiTLS.EverCrypt.fsti.checked MiTLS.DebugFlags.fst.checked MiTLS.DataStream.fst.checked MiTLS.Connection.fst.checked MiTLS.CommonDH.fsti.checked MiTLS.Cert.fsti.checked MiTLS.Alert.fst.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.String.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.IO.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Dyn.fsti.checked FStar.Char.fsti.checked FStar.Bytes.fsti.checked C.Loops.fst.checked
MiTLS.FFI.fst
s: Prims.string -> FStar.HyperStack.ST.ST Prims.unit
Prims.string MiTLS.FFI.discard FStar.IO.debug_print_string Prims.op_Hat Prims.unit
let print s =
  
discard (IO.debug_print_string ("FFI| " ^ s ^ "\n"))