val alloc_input_state: r:_ -> ST input_state 
  (requires (fun h0 -> is_eternal_region r))
  (ensures (fun h0 s h1 ->
    //18-04-20 TODO post-condition for allocating a ref and a buffer?
    Mem.frameOf (input_pos s) = r /\ 
    input_inv h1 s))
val alloc_input_state: r:_ -> ST input_state 
  (requires (fun h0 -> is_eternal_region r))
  (ensures (fun h0 s h1 ->
    //18-04-20 TODO post-condition for allocating a ref and a buffer?
    Mem.frameOf (input_pos s) = r /\ 
    input_inv h1 s))
let alloc_input_state r = 
  let pos = ralloc r 0ul in
  let b = Buffer.rcreate r 0uy maxlen in
  InputState pos b
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
/
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
r: FStar.Monotonic.HyperHeap.rid -> FStar.HyperStack.ST.ST MiTLS.Record.input_state
FStar.Monotonic.HyperHeap.rid MiTLS.Record.InputState MiTLS.Record.input_state FStar.Buffer.buffer FStar.UInt8.t FStar.Buffer.rcreate FStar.UInt8.__uint_to_t MiTLS.Record.maxlen FStar.HyperStack.ST.mref FStar.UInt32.t Prims.b2t FStar.UInt32.lte FStar.Heap.trivial_preorder FStar.HyperStack.ST.ralloc FStar.UInt32.op_Less_Equals_Hat FStar.UInt32.__uint_to_t
let alloc_input_state r =
  
let pos = ralloc r 0ul in
let b = Buffer.rcreate r 0uy maxlen in
InputState pos b