val first_bytes : b: FStar.Bytes.bytes -> Prims.string
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)
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
/
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
b: FStar.Bytes.bytes -> Prims.string
FStar.Bytes.bytes FStar.Printf.sprintf FStar.UInt32.op_Less_Equals_Hat FStar.Bytes.len FStar.UInt32.op_Plus_Hat FStar.Bytes.hex_of_bytes Prims.bool Prims.op_Hat FStar.Bytes.sub FStar.UInt32.__uint_to_t FStar.UInt32.op_Subtraction_Hat Prims.string FStar.UInt32.t
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)