val waiting_len:  s: input_state -> ST UInt32.t
  (requires fun h0 -> input_inv h0 s)
  (ensures fun h0 len h1 -> 
    h0 == h1 /\
    ( let pv = UInt32.v (sel h0 (input_pos s)) in 
      let l = UInt32.v len in 
      ( if pv < headerLength 
        then pv + l = headerLength
        else 
        match parseHeader (Bytes.hide (Buffer.as_seq h0 (Buffer.sub (input_b s) 0ul headerLen))) with
        | Correct (_,_,length) -> pv + l == headerLength + length
        | _ -> False)))
val waiting_len:  s: input_state -> ST UInt32.t
  (requires fun h0 -> input_inv h0 s)
  (ensures fun h0 len h1 -> 
    h0 == h1 /\
    ( let pv = UInt32.v (sel h0 (input_pos s)) in 
      let l = UInt32.v len in 
      ( if pv < headerLength 
        then pv + l = headerLength
        else 
        match parseHeader (Bytes.hide (Buffer.as_seq h0 (Buffer.sub (input_b s) 0ul headerLen))) with
        | Correct (_,_,length) -> pv + l == headerLength + length
        | _ -> False)))
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
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
/
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
s: MiTLS.Record.input_state -> FStar.HyperStack.ST.ST FStar.UInt32.t
MiTLS.Record.input_state FStar.UInt32.op_Subtraction_Hat MiTLS.Record.headerLen FStar.UInt32.t FStar.HyperStack.ST.op_Bang Prims.b2t FStar.UInt32.op_Less_Equals_Hat MiTLS.Record.maxlen FStar.Heap.trivial_preorder MiTLS.Record.__proj__InputState__item__pos Prims.bool MiTLS.Content.contentType MiTLS.TLSConstants.protocolVersion Prims.nat Prims.op_LessThanOrEqual MiTLS.TLSConstants.max_TLSCiphertext_fragment_length FStar.UInt32.op_Plus_Hat FStar.UInt32.uint_to_t MiTLS.Record.parsed_header MiTLS.Record.parseHeaderBuffer FStar.Buffer.sub FStar.UInt8.t MiTLS.Record.__proj__InputState__item__b FStar.UInt32.__uint_to_t FStar.UInt32.op_Less_Hat
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