val datafragment
      (i: id{~(PlaintextID? i)})
      (o: option (rg: frange i & DataStream.fragment i rg) {Some? o})
    : DataStream.delta i
val datafragment
      (i: id{~(PlaintextID? i)})
      (o: option (rg: frange i & DataStream.fragment i rg) {Some? o})
    : DataStream.delta i
let datafragment (i:id{~ (PlaintextID? i)}) (o: option (rg:frange i & DataStream.fragment i rg) { Some? o }) : DataStream.delta i =
  match o with
  | Some (| rg, f |) -> let f: DataStream.pre_fragment i = f in //16-05-16 unclear why we now need this step
                       DataStream.Data f
module MiTLS.TLS
open MiTLS
module HS = FStar.HyperStack //Added automatically

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

open MiTLS.Mem
open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.TLSInfo


module Range = MiTLS.Range
let range = Range.range
let point = Range.point
let frange = Range.frange
let valid_clen = Range.valid_clen
let fragment_range = Range.fragment_range

//open Negotiation
open MiTLS.Old.Epochs
open MiTLS.Connection

module ST   = FStar.HyperStack.ST
module HST  = FStar.HyperStack
module MS   = FStar.Monotonic.Seq
module DS   = MiTLS.DataStream
module SD   = MiTLS.StreamDeltas
module Conn = MiTLS.Connection

module Epochs    = MiTLS.Old.Epochs
module Handshake = MiTLS.Old.Handshake

(* A flag for runtime debugging of TLS data.
   The F* normalizer will erase debug prints at extraction
   when this flag is set to false *)
val discard: bool -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
let discard _ = ()
let print s = discard (IO.debug_print_string ("TLS| "^s^"\n"))
unfold val trace: s:string -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
unfold let trace = if DebugFlags.debug_TLS then print else (fun _ -> ())


unfold let op_Array_Access (#a:Type) (s:Seq.seq a) n = Seq.index s n // s.[n]

// using also DataStream, Content, Record
#set-options "--initial_ifuel 0 --max_ifuel 0 --initial_fuel 0 --max_fuel 0 --admit_smt_queries true"


(** misc ***)

// the (now fake) protocol version in the record header
let outerPV (c:connection) : ST protocolVersion
  (requires (Handshake.hs_inv c.hs))
  (ensures (fun h0 pv h1 -> h0 == h1)) =
  match Handshake.version_of c.hs with
  | TLS_1p3 -> TLS_1p0
  | pv      -> pv


(** control API ***)

// subsumes connect, resume, accept_connected, ...
val create: r0:c_rgn -> tcp:Transport.t -> r:role -> cfg:config -> ST connection
  (requires (fun h -> True))
  (ensures (fun h0 c h1 ->
    modifies Set.empty h0 h1 /\
    extends c.region r0 /\
    HS.fresh_region c.region h0 h1 /\
    HS.live_region h1 c.region /\ //NS: may be removeable: we should get it from fresh_region
    st_inv c h1 /\
    c_role c = r /\
//17-04-08 commented out as their access is now stateful
//    c_cfg c == cfg /\
//    c_resume c = resume /\
    c.tcp == tcp  /\
    //17-04-07 went back to static refinements on resumeInfo r
    //(r = Server ==> resume = None) /\ //16-05-28 style: replacing a refinement under the option
    epochs c h1 == Seq.empty /\ // we probably don't care---but we should say nothing written yet
    HS.sel h1 c.state = (Ctrl,Ctrl) ))

#set-options "--z3rlimit 50"
let create parent tcp role cfg =
    let m = new_region parent in
    let hs = Handshake.create m cfg role in
    let recv = Record.alloc_input_state m in
    let state = ralloc m (Ctrl,Ctrl) in
    assume (is_hs_rgn m);
    C #m hs tcp recv state


//TODO upgrade commented-out types imported from TLS.fsti
// type initial (role: role) (ns:Transport.t) (c:config) (resume: option sessionID) (cn:connection) (h: HH.t) =
//     extends (c_rid cn) root /\ // we allocate a fresh, opaque region for the connection
//     c_role cn   = role /\
//     c_tcp cn    = ns /\
//     c_resume cn = resume /\
//     c_cfg cn = c /\
//     HH.sel h (C.reading cn) = Init /\ // assuming Init epoch implicitly have no data sent/received
//     HH.sel h (C.writing cn) = Init

// painful to specify?
//* should we still return ConnectionInfo ?
//* merging connect and resume with an optional sessionID
//val connect: ns:Transport.t -> c:config -> resume: option sessionID -> ST connection
//  (requires (fun h0 -> True))
//  (ensures (fun h0 cn h1 ->
//    modifies Set.empty h0 h1 /\
//    initial Client ns c resume cn h1
//    //TODO: even if the server declines, we authenticate the client's intent to resume from this sid.
//  ))
let connect m0 tcp cfg         = create m0 tcp Client cfg
let resume  m0 tcp cfg tid psk =
  let cfg = {cfg with use_tickets=(tid,psk)::cfg.use_tickets} in
  create m0 tcp Client cfg

//val accept_connected: ns:Transport.t -> c:config -> ST connection
//  (requires (fun h0 -> True))
//  (ensures (fun h0 cn h1 ->
//    modifies Set.empty h0 h1 /\
//    initial Server ns c None cn h1
//  ))
let accept_connected m0 tcp cfg = create m0 tcp Server cfg

//* do we need accept and accept_connected?
//val accept: Tcp.tcpListener -> c:config -> ST connection
//  (requires (fun h0 -> True))
//  (ensures (fun h0 cn h1 ->
//    modifies Set.empty h0 h1 /\
//    (exists ns. initial Server ns c None cn h1)
//  ))

(* NS Jan 30, 2018: Removing this since uses of TCP should be from the application *)
// let accept m0 listener cfg =
//     let tcp = Transport.accept listener in
//     accept_connected m0 tcp cfg

//val rehandshake: cn:connection { c_role cn = Client } -> c:config -> ST unit
//  (requires (fun h0 -> True))
//  (ensures (fun h0 b h1 -> modifies Set.empty h0 h1 // no visible change in cn
//  ))
let rehandshake c ops = Handshake.rehandshake (C?.hs c) ops
// the client can ask for rekeying --- no immediate effect
//val rekey: cn:connection { c_role cn = Client } -> ST unit
//  (requires (fun h0 -> True))
//  (ensures (fun h0 b h1 -> modifies Set.empty h0 h1 // no visible change in cn
//  ))
let rekey c ops       = Handshake.rekey       (C?.hs c) ops
//val request: cn:connection { c_role cn = Server } -> c:config -> ST unit
//  (requires (fun h0 -> True))
//  (ensures (fun h0 b h1 -> modifies Set.empty h0 h1 // no visible change in cn
//  ))
let request c ops     = Handshake.request     (C?.hs c) ops

let get_mode c = (Handshake.get_mode (C?.hs c))
let set_ticket_key (a:aeadAlg) (kv:bytes) = Ticket.set_ticket_key a kv
let set_sealing_key (a:aeadAlg) (kv:bytes) = Ticket.set_sealing_key a kv

(** current epochs ***)

// the index of messages depends on the connection state,
// and may be different for reading and for writing.

#set-options "--initial_ifuel 0 --max_ifuel 1 --initial_fuel 0 --max_fuel 0"
//16-05-28 we need pattern matching!

// to be replaced with check_incrementable (and pushed).
// dynamically checks for overflows
val no_seqn_overflow: c: connection -> rw:rw -> ST bool
  (requires (fun h -> st_inv c h))
  (ensures (fun h0 b h1 ->
    let es = epochs c h1 in
    let j = Handshake.iT c.hs rw h1 in
    j < Seq.length es /\
    h0 == h1 /\
    (b /\ j >= 0) ==> (
    let e = es.(j) in
    match rw with
    | Reader -> StAE.incrementable (reader_epoch e) h0
    | Writer -> StAE.incrementable (writer_epoch e) h0
    )))

let no_seqn_overflow c rw =
  let es = MS.i_read (Handshake.es_of c.hs) in //ST.op_Bang c.hs.log in
  let j = Handshake.i c.hs rw in // -1 <= j < length es
  if j < 0 then //16-05-28 style: ghost constraint prevents using j < 0 || ...
    true
  else ( //indexable es j
    let e = es.(j) in
    let h = get() in
    let _ = match rw with
    | Reader -> assume(StAE.incrementable (reader_epoch e) h)
    | Writer -> assume(StAE.incrementable (writer_epoch e) h) in
    true  )
// JP: placeholder while I fix the int64 problem
    (*
    let n = !(seqn w) + 1 in
    if n >= 72057594037927936 && n < 18446744073709551616
    then (lemma_repr_bytes_values n; true)
    else false *)

#set-options "--initial_ifuel 0 --max_ifuel 0 --initial_fuel 0 --max_fuel 0"


(** outgoing ***)

type ioresult_w =
    // public results returned by TLS.send
    | Written             // the application data was written; the connection remains writable
    | WriteClose          // a final closeNotify was written; the connection is either closed or read-only
    | WriteError: o:option alert -> txt: string -> ioresult_w
                          // The connection is gone, possibly after sending a fata alert
//  | WritePartial of unsent_data // worth restoring?

    // transient internal results returned by auxiliary send functions
    | WrittenHS: newWriter:option bool -> complete:bool -> ioresult_w // the handshake progressed
(*
//  | MustRead            // Nothing written, and the connection is busy completing a handshake
    | WriteDone           // No more data to send in the current state
    | WriteHSComplete     // The handshake is complete [while reading]
    | WriteClose           // a closeNotify was finally written.
    | WriteAgain          // sent something; there may be more to send (loop)
    | WriteAgainFinishing // outgoing epoch changed; there may be more to send to finish the handshake (loop)
    | WriteAgainClosing   // we are tearing down the connection & must still send an alert
*)

#set-options "--initial_ifuel 1 --max_ifuel 1"
let string_of_ioresult_w = function
  | Written -> "Written"
  | WriteClose -> "WriteClose"
  | WriteError (Some a) s -> "WriteError: "^string_of_error (a,s)
  | WriteError None s -> "WriteError: "^s
  | WrittenHS nw c -> "WrittenHS "^(match nw with | Some true -> "new-writable " | Some false -> "new-hanshake-only " | None -> "")^(if c then "complete" else "")
#set-options "--initial_ifuel 0 --max_ifuel 0 --initial_fuel 0 --max_fuel 0"

type ioresult_o = r:ioresult_w { Written? r \/ WriteError? r }


// error-handling

// the connection fails now, and should not be resumed.
val disconnect: c: connection -> ST unit
  (requires (fun h0 -> st_inv c h0 /\ h0 `HS.contains` c.state))
  (ensures (fun h0 _ h1 -> st_inv c h1 /\ modifies (Set.singleton (C?.region c)) h0 h1))

let disconnect c =
    Handshake.invalidateSession c.hs; //changes (HS?.region c.hs)
    c.state := (Closed,Closed);
    let h = get () in
    assume (st_inv c h)

// on some errors, we locally give up the connection
val unrecoverable: c: connection -> r:string -> ST ioresult_w
  (requires (fun h0 -> st_inv c h0 /\ h0 `HS.contains` c.state))
  (ensures (fun h0 i h1 -> st_inv c h1 /\
		        modifies (Set.singleton (C?.region c)) h0 h1 /\
			i = WriteError None r))
let unrecoverable c reason =
  disconnect c;
  WriteError None reason

let currentId_T (c:connection) (rw:rw) (h:HS.mem) : GTot id =
  let j = Handshake.iT c.hs rw h in
  if j < 0
  then PlaintextID (c_nonce c)
  else epoch_id (Handshake.eT c.hs rw h)

let currentId (c:connection) (rw:rw)
  : ST id
      (requires (fun h -> True))
      (ensures (fun h0 r h1 -> h0==h1 /\ r=currentId_T c rw h1))
=
  let j = Handshake.i c.hs rw in
  if j<0 then PlaintextID (c_nonce c)
  else let e = Epochs.get_current_epoch (Handshake.epochs_of c.hs) rw in epoch_id e

let maybe_indexable (es:seq 'a) (i:int) = i=(-1) \/ indexable es i


(*
assume val admit_st_inv: c: connection -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 = h1 /\ st_inv h1 c))
*)


// auxiliary functions for projections; floating.
let appfragment (i:id{~ (PlaintextID? i)}) (o: option (rg:frange i & DataStream.fragment i rg) { Some? o }) : Content.fragment i =
  match o with
  | Some (| rg, f |) -> Content.CT_Data rg f
/
prims.fst.checked MiTLS.Transport.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Ticket.fst.checked MiTLS.StreamDeltas.fst.checked MiTLS.StreamAE.fst.checked MiTLS.StAE.fst.checked MiTLS.Record.fsti.checked MiTLS.Range.fst.checked MiTLS.Old.Handshake.fsti.checked MiTLS.Old.Epochs.fsti.checked MiTLS.Mem.fst.checked MiTLS.HandshakeLog.fsti.checked MiTLS.DebugFlags.fst.checked MiTLS.DataStream.fst.checked MiTLS.Content.fst.checked MiTLS.Connection.fst.checked MiTLS.Cert.fsti.checked FStar.UInt8.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Seq.fst.checked FStar.IO.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.TLS.fst

    i: MiTLS.TLSInfo.id{~(PlaintextID? i)} ->
    o:
      FStar.Pervasives.Native.option (Prims.dtuple2 (MiTLS.TLS.frange i)
            (fun rg -> MiTLS.DataStream.fragment i rg)) {Some? o}
  -> MiTLS.DataStream.delta i
MiTLS.TLSInfo.id Prims.l_not Prims.b2t MiTLS.TLSInfo.uu___is_PlaintextID FStar.Pervasives.Native.option Prims.dtuple2 MiTLS.TLS.frange MiTLS.DataStream.fragment FStar.Pervasives.Native.uu___is_Some MiTLS.DataStream.Data MiTLS.DataStream.pre_fragment MiTLS.DataStream.delta
let datafragment
      (i: id{~(PlaintextID? i)})
      (o: option (rg: frange i & DataStream.fragment i rg) {Some? o})
    : DataStream.delta i =
  
match o with
| Some (| rg , f |) ->
  let f:DataStream.pre_fragment i = f in
  DataStream.Data f