val recv:
  t ->
  input_buffer: FStar.Buffer.buffer UInt8.t -> 
  max_len: size_t -> ST Int32.t
  (requires fun h0 ->
    Buffer.live h0 input_buffer /\
    UInt32.v max_len = Buffer.length input_buffer)
  (ensures fun h0 r h1 -> 
    let v = Int32.v r in 
    Buffer.modifies_1 input_buffer h0 h1 /\ 
    (v = -1 \/ (0 <= v /\ v <= UInt32.v max_len)))
val recv:
  t ->
  input_buffer: FStar.Buffer.buffer UInt8.t -> 
  max_len: size_t -> ST Int32.t
  (requires fun h0 ->
    Buffer.live h0 input_buffer /\
    UInt32.v max_len = Buffer.length input_buffer)
  (ensures fun h0 r h1 -> 
    let v = Int32.v r in 
    Buffer.modifies_1 input_buffer h0 h1 /\ 
    (v = -1 \/ (0 <= v /\ v <= UInt32.v max_len)))
let recv t buffer len = t.rcv t.ptr buffer len
module MiTLS.Transport
open MiTLS
module HS = FStar.HyperStack //Added automatically

// adding an indirection to TCP for applications that prefer to take control of their IOs.

open FStar.HyperStack.All
open FStar.Bytes
open FStar.Error
open MiTLS.TLSError
open MiTLS.Mem

/// 18-01-23 We now have function pointers matching the types used in
/// mitls.h. After hoisting for KaRaMeL extraction, we treat the
/// explicit context as a dyn to avoid climbing in universes.
type pvoid = FStar.Dyn.dyn
type size_t = UInt32.t 
type pfn_send = 
  pvoid -> 
  output_buffer: FStar.Buffer.buffer UInt8.t -> 
  max_len: size_t -> ST Int32.t
  (requires fun h0 -> 
    Buffer.live h0 output_buffer /\ 
    UInt32.v max_len = Buffer.length output_buffer)
  (ensures fun h0 r h1 -> 
    let v = Int32.v r in
    modifies_none h0 h1 /\
    (v = -1 \/ (0 <= v /\ v <= UInt32.v max_len)))

unfold type recv_t = 
  input_buffer: FStar.Buffer.buffer UInt8.t -> 
  max_len: size_t -> ST Int32.t
  (requires fun h0 ->
    Buffer.live h0 input_buffer /\
    UInt32.v max_len = Buffer.length input_buffer)
  (ensures fun h0 r h1 -> 
    let v = Int32.v r in 
    Buffer.modifies_1 input_buffer h0 h1 /\ 
    (v = -1 \/ (0 <= v /\ v <= UInt32.v max_len)))

type pfn_recv = pvoid -> recv_t
    
noeq type t = {
  ptr: pvoid;
  snd: pfn_send;
  rcv: pfn_recv }

let callbacks v send recv: t = { ptr = v; snd = send; rcv = recv }

// following the indirection
let send t buffer len = t.snd t.ptr buffer len 

//18-04-21 apparently requiring an explicit declaration
//val recv: t -> recv_t

val recv:
  t ->
  input_buffer: FStar.Buffer.buffer UInt8.t -> 
  max_len: size_t -> ST Int32.t
  (requires fun h0 ->
    Buffer.live h0 input_buffer /\
    UInt32.v max_len = Buffer.length input_buffer)
  (ensures fun h0 r h1 -> 
    let v = Int32.v r in 
    Buffer.modifies_1 input_buffer h0 h1 /\ 
    (v = -1 \/ (0 <= v /\ v <= UInt32.v max_len)))
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.Mem.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Int32.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Dyn.fsti.checked FStar.Bytes.fsti.checked FStar.Buffer.fst.checked
MiTLS.Transport.fst

    t: MiTLS.Transport.t ->
    input_buffer: FStar.Buffer.buffer FStar.UInt8.t ->
    max_len: MiTLS.Transport.size_t
  -> FStar.HyperStack.ST.ST FStar.Int32.t
MiTLS.Transport.t FStar.Buffer.buffer FStar.UInt8.t MiTLS.Transport.size_t MiTLS.Transport.__proj__Mkt__item__rcv MiTLS.Transport.__proj__Mkt__item__ptr FStar.Int32.t
let recv t buffer len =
  
t.rcv t.ptr buffer len