val read: Transport.t -> s: input_state -> ST read_result
  (requires fun h0 -> input_inv h0 s)
  (ensures fun h0 r h1 -> ReadError? r \/ input_inv h1 s)
val read: Transport.t -> s: input_state -> ST read_result
  (requires fun h0 -> input_inv h0 s)
  (ensures fun h0 r h1 -> ReadError? r \/ input_inv h1 s)
let rec read tcp s =
  let h0 = ST.get() in 
  let header = Buffer.sub s.b 0ul headerLen in 
  let p0 = !s.pos in
  let waiting = waiting_len s in
  let dest = Buffer.sub s.b p0 waiting in
  let res = Transport.recv tcp dest waiting in
  let h1 = ST.get() in
  Buffer.lemma_reveal_modifies_1 dest h0 h1;
  // framing, with two cases depending on the input state.
  //assert(p0 <^ headerLen \/ Buffer.disjoint header dest);
  //assert(p0 <^ headerLen \/ Buffer.as_seq h0 header == Buffer.as_seq h1 header);
  if res = -1l then
    ReadError (fatalAlert Internal_error, "Transport.recv")
  else
  if res = 0l
  then ( trace "WouldBlock"; ReadWouldBlock )
  else
    begin
    let received = Int.Cast.int32_to_uint32 res in
    assert (received <=^ waiting);
    assert (p0 +^ waiting <=^ maxlen);
    let p1 = p0 +^ received in 
    s.pos := p1;
    //let h2 = ST.get() in
    //assert(p0 <^ headerLen \/ Buffer.as_seq h0 header == Buffer.as_seq h2 header);
    if received <^ waiting
    then
      // partial read; we remain in the same logical state
      // we should probably return ReadWouldBlock instead when non-blocking
      read tcp s
    else
      begin
      if p1 = headerLen 
      then
        begin
        // we have just buffered the record header
        match parseHeaderBuffer header with
        | Error e -> ReadError e
        | Correct(ct, pv, length) ->
          if length = 0 then
            begin
            // zero-length packet, a corner case possibly excluded by the RFC
            s.pos := 0ul;
            Received ct pv empty_bytes
            end
          else read tcp s
        end
      else
        begin
        // we have just buffered the whole record
        assert(headerLen <=^ p0); 
        let hdr = parseHeaderBuffer header in 
        match hdr with
        | Correct(ct, pv, length) ->
          begin
          let len = UInt32.uint_to_t length in
          let b = Buffer.sub s.b headerLen len in
          let payload = BufferBytes.to_bytes length b in
          s.pos := 0ul;
          Received ct pv payload
          end
        end
      end
    end
module MiTLS.Record
open MiTLS

(* (optional) encryption and processing of the outer, untrusted record format *)

open FStar.Seq
open FStar.Bytes
open FStar.Error
open FStar.UInt32

open MiTLS.Mem
open MiTLS.TLSError
open MiTLS.TLSInfo
open MiTLS.TLSConstants
open MiTLS.Range
open MiTLS.Content

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

#reset-options "--using_facts_from '* -LowParse.Spec.Base'"

#set-options "--z3rlimit 10" //18-04-20 now required; why?
noeq type input_state = | InputState:
  pos: ref (len:UInt32.t {len <=^ maxlen}) ->
  b: input_buffer {
    Buffer.disjoint_ref_1 b pos /\
    Buffer.frameOf b = Mem.frameOf pos /\ 
    Buffer.length b = v maxlen} -> 
  input_state

let input_inv h0 (s: input_state) = 
  Mem.contains h0 s.pos /\
  Buffer.live h0 s.b /\
  ( let p0 = UInt32.v (sel h0 s.pos) in 
    p0 < headerLength \/ 
    ( let hdr = parseHeader (Bytes.hide (Buffer.as_seq h0 (Buffer.sub s.b 0ul headerLen))) in
      match hdr with  
      | Correct (_,_,length) -> p0 < headerLength + length 
      | _                    -> False ))
// we are waiting either for header bytes or payload bytes

let input_pos s = s.pos
let input_b s = s.b

#reset-options "--max_fuel 0 --max_ifuel 0 --using_facts_from '* -LowParse -Format'"
let waiting_len s =
  if !s.pos <^ headerLen
  then headerLen -^ !s.pos
  else
    let Correct (_,_,length) = parseHeaderBuffer (Buffer.sub s.b 0ul headerLen) in
    headerLen +^ uint_to_t length -^ !s.pos

// TODO later, use a length-field accessor instead of a header parser

let alloc_input_state r = 
  let pos = ralloc r 0ul in
  let b = Buffer.rcreate r 0uy maxlen in
  InputState pos b
/
prims.fst.checked MiTLS.Transport.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Range.fst.checked MiTLS.Mem.fst.checked MiTLS.Content.fst.checked MiTLS.BufferBytes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Int32.fsti.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked FStar.Buffer.fst.checked
MiTLS.Record.fst
tcp: MiTLS.Transport.t -> s: MiTLS.Record.input_state
  -> FStar.HyperStack.ST.ST MiTLS.Record.read_result
MiTLS.Transport.t MiTLS.Record.input_state Prims.op_Equality FStar.Int32.t FStar.Int32.__int_to_t MiTLS.Record.ReadError FStar.Pervasives.Native.Mktuple2 MiTLS.Parsers.Alert.alert Prims.string MiTLS.TLSError.fatalAlert MiTLS.Parsers.AlertDescription.Internal_error MiTLS.Record.read_result Prims.bool MiTLS.Record.ReadWouldBlock Prims.unit MiTLS.Record.trace FStar.UInt32.op_Less_Hat MiTLS.Record.read FStar.UInt32.t MiTLS.Record.headerLen MiTLS.TLSError.error MiTLS.Content.contentType MiTLS.TLSConstants.protocolVersion Prims.nat Prims.b2t Prims.op_LessThanOrEqual MiTLS.TLSConstants.max_TLSCiphertext_fragment_length Prims.int MiTLS.Record.Received FStar.Bytes.empty_bytes FStar.HyperStack.ST.op_Colon_Equals FStar.UInt32.op_Less_Equals_Hat MiTLS.Record.maxlen FStar.Heap.trivial_preorder MiTLS.Record.__proj__InputState__item__pos FStar.UInt32.__uint_to_t MiTLS.Record.parsed_header MiTLS.Record.parseHeaderBuffer FStar.Bytes.bytes Prims.l_or FStar.UInt.size Prims.op_GreaterThanOrEqual FStar.UInt32.v FStar.Bytes.len MiTLS.BufferBytes.to_bytes FStar.Bytes.length FStar.Buffer.buffer FStar.UInt8.t Prims.l_and FStar.Buffer.includes MiTLS.Record.__proj__InputState__item__b Prims.eq2 FStar.Buffer.length FStar.Buffer.sub FStar.UInt32.uint_to_t Prims._assert FStar.UInt32.op_Plus_Hat Prims.op_Modulus FStar.Int32.v Prims.pow2 FStar.Int.Cast.int32_to_uint32 FStar.Buffer.lemma_reveal_modifies_1 FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get MiTLS.Transport.recv MiTLS.Record.waiting_len FStar.UInt32.lte FStar.HyperStack.ST.op_Bang
let rec read tcp s =
  
let h0 = ST.get () in
let header = Buffer.sub s.b 0ul headerLen in
let p0 = !s.pos in
let waiting = waiting_len s in
let dest = Buffer.sub s.b p0 waiting in
let res = Transport.recv tcp dest waiting in
let h1 = ST.get () in
Buffer.lemma_reveal_modifies_1 dest h0 h1;
if res = -1l
then ReadError (fatalAlert Internal_error, "Transport.recv")
else
  if res = 0l
  then
    (trace "WouldBlock";
      ReadWouldBlock)
  else
    let received = Int.Cast.int32_to_uint32 res in
    assert (received <=^ waiting);
    assert (p0 +^ waiting <=^ maxlen);
    let p1 = p0 +^ received in
    s.pos := p1;
    if received <^ waiting
    then read tcp s
    else
      if p1 = headerLen
      then
        match parseHeaderBuffer header with
        | Error e -> ReadError e
        | Correct (ct, pv, length) ->
          if length = 0
          then
            (s.pos := 0ul;
              Received ct pv empty_bytes)
          else read tcp s
      else
        (assert (headerLen <=^ p0);
          let hdr = parseHeaderBuffer header in
          match hdr with
          | Correct (ct, pv, length) ->
            let len = UInt32.uint_to_t length in
            let b = Buffer.sub s.b headerLen len in
            let payload = BufferBytes.to_bytes length b in
            s.pos := 0ul;
            Received ct pv payload)