val input_b (s:input_state)
: Tot (b: input_buffer{
          Buffer.disjoint_ref_1 b (input_pos s) /\
          Buffer.frameOf b = Mem.frameOf (input_pos s) /\ 
          Buffer.length b = v maxlen})
val input_b (s:input_state)
: Tot (b: input_buffer{
          Buffer.disjoint_ref_1 b (input_pos s) /\
          Buffer.frameOf b = Mem.frameOf (input_pos s) /\ 
          Buffer.length b = v maxlen})
let input_b s = s.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
/
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
  -> b:
    MiTLS.Record.input_buffer
      { FStar.Buffer.disjoint_ref_1 b (MiTLS.Record.input_pos s) /\
        FStar.Buffer.frameOf b = FStar.Monotonic.HyperStack.frameOf (MiTLS.Record.input_pos s) /\
        FStar.Buffer.length b = FStar.UInt32.v MiTLS.Record.maxlen }
MiTLS.Record.input_state MiTLS.Record.__proj__InputState__item__b MiTLS.Record.input_buffer Prims.l_and FStar.Buffer.disjoint_ref_1 FStar.UInt8.t FStar.UInt32.t Prims.b2t FStar.UInt32.op_Less_Equals_Hat MiTLS.Record.maxlen MiTLS.Record.input_pos Prims.op_Equality FStar.Monotonic.HyperHeap.rid FStar.Buffer.frameOf FStar.Monotonic.HyperStack.frameOf FStar.Heap.trivial_preorder Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.op_GreaterThanOrEqual FStar.Buffer.length FStar.UInt32.v
let input_b s =
  
s.b