val sendHandshake
      (#c: connection)
      (#i: id)
      (wopt: option (cwriter i c))
      (om: option (HandshakeLog.fragment i))
      (send_ccs: bool)
    : ST (result unit)
      (requires (sendFragment_inv wopt))
      (ensures
        (fun h0 r h1 -> sendFragment_inv wopt h1 /\ sendHandshake_post wopt om send_ccs h0 r h1))
val sendHandshake
      (#c: connection)
      (#i: id)
      (wopt: option (cwriter i c))
      (om: option (HandshakeLog.fragment i))
      (send_ccs: bool)
    : ST (result unit)
      (requires (sendFragment_inv wopt))
      (ensures
        (fun h0 r h1 -> sendFragment_inv wopt h1 /\ sendHandshake_post wopt om send_ccs h0 r h1))
let sendHandshake
  (#c:connection)
  (#i:id)
  (wopt:option (cwriter i c))
  (om:option (HandshakeLog.fragment i))
  (send_ccs:bool) :
  ST (result unit)
     (requires (sendFragment_inv wopt))
     (ensures  (fun h0 r h1 ->
                sendFragment_inv wopt h1 /\
                sendHandshake_post wopt om send_ccs h0 r h1))
  = trace "sendHandshake";
    // first try to send handshake fragment, if any
    // then try to send CCS fragment, if requested
    match om, send_ccs with
    | Some (| rg, f |), false -> sendFragment c wopt (Content.CT_Handshake rg f)
    | Some (| rg, f |), true ->
      let result = sendFragment c wopt (Content.CT_Handshake rg f) in
      begin
      match result with
      | Error _ -> result
      | _       -> sendFragment c wopt (Content.CT_CCS (point 1))
      end
    | _, true  -> sendFragment c wopt (Content.CT_CCS (point 1))
    | _ -> Correct ()
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

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

(* which fragment should we send next? *)
(* we must send this fragment before restoring the connection invariant *)

//* pick & send one pending message from any protocol state, in two modes:
//* when writing for the application code, we may send Some? ghost.
//* when writing while reading, None? ghost.
//* the result ranges over...
//* | WriteDone         when None? ghost, notifying there is nothing left to send
//* | Written when Some? ghost, notifying the appdata fragment was sent
//* | WriteError (unrecoverable \/ after sending alert)
//* | WriteClose
//* | WriteAgain | WriteAgainFinishing | WriteAgainClosing
//* | WriteHSComplete
//* the state changes accordingly.

////////////////////////////////////////////////////////////////////////////////
// Current writers
////////////////////////////////////////////////////////////////////////////////
let trigger_peer (#a:Type) (x:a) = True

let cwriter (i:id) (c:connection) =
  w:StAE.writer i{exists (r:StAE.reader (peerId i)).{:pattern (trigger_peer r)}
		    epoch_region_inv' (Handshake.region_of c.hs) r w}

let current_writer_pre (c:connection) (i:id) (h:HS.mem) : GTot bool =
  let hs = c.hs in
  let ix = Handshake.iT hs Writer h in
  if ix < 0
  then PlaintextID? i
  else
    let epoch_i = Handshake.eT hs Writer h in
    i = epoch_id epoch_i

let current_writer_T (c:connection) (i:id) (h:HS.mem{current_writer_pre c i h})
  : GTot (option (cwriter i c))
=
  let i = Handshake.iT c.hs Writer h in
  if 0 <= i
  then
    let e = Handshake.eT c.hs Writer h in
    let _ = cut (trigger_peer (Epoch?.r e)) in
    Some (Epoch?.w e)
  else None

val current_writer : c:connection -> i:id -> ST (option (cwriter i c))
       (requires (fun h -> current_writer_pre c i h))
       (ensures (fun h0 wo h1 ->
	       current_writer_pre c i h1
	       /\ h0==h1
	       /\ wo==current_writer_T c i h1
	       /\ (None? wo <==> PlaintextID? i)))
let current_writer c i =
  let ix = Handshake.i c.hs Writer in
  if ix < 0
  then None
  else
    let epochs = MS.i_read (Handshake.es_of c.hs) in
    let e = epochs.(ix) in
    let _ = cut (trigger_peer (Epoch?.r e)) in
    Some (Epoch?.w e)

let recall_current_writer (c:connection)
  : ST unit (fun h -> True) (fun h0 _ h1 ->
    let i = currentId_T c Writer h0 in
    let wopt = current_writer_T c i h0 in
    h0 == h1
    /\ (match wopt with
       | None -> True
       | Some wr -> HS.live_region h0 (StAE.region wr)
	         /\ HS.live_region h0 (StAE.log_region wr)))
  = let i = currentId c Writer in
    let wopt = current_writer c i in
    match wopt with
    | None -> ()
    | Some wr ->
      recall_region (StAE.region wr);
      recall_region (StAE.log_region wr)

//16-05-29 duplicating no_seqn_overflow?
private let check_incrementable (#c:connection) (#i:id) (wopt:option (cwriter i c))
  : ST bool
    (requires (fun h -> True))
    (ensures (fun h0 b h1 ->
	      h0 == h1
	      /\ (b <==> (match wopt with
		        | None -> True
			| Some w -> StAE.incrementable w h1))))
  = assume(False); true // admit()

////////////////////////////////////////////////////////////////////////////////
// Sending fragments on a given writer (not necessarily the current one)
////////////////////////////////////////////////////////////////////////////////
let opt_writer_regions (#i:id) (#c:connection) (wopt:option (cwriter i c)) : GTot (FStar.Set.set HS.rid) =
  match wopt with
  | None -> Set.empty
  | Some wr -> Set.singleton (StAE.region wr)

let sendFragment_inv (#c:connection) (#i:id) (wo:option(cwriter i c)) h =
     st_inv c h
  /\ (match wo with
     | None    -> PlaintextID? i
     | Some wr ->  live_region h (StAE.region wr)
	        /\ live_region h (StAE.log_region wr))

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

//16-05-29 note that AD_record_overflow os for oversized incoming records, not seqn overflows! See slack.
// let ad_overflow : result unit = Error (AD_internal_error, "seqn overflow")
let ad_overflow : result unit = fatal Record_overflow "seqn overflow"

let sendFragment_success (mods:FStar.Set.set rid) (c:connection) (i:id) (wo:option (cwriter i c)) (f: Content.fragment i) (h0:HS.mem) (h1:HS.mem) =
      Some? wo ==>
      (let wr = Some?.v wo in
       HS.modifies (Set.union mods (Set.singleton (StAE.region wr))) h0 h1
     /\ StAE.seqnT wr h1 = StAE.seqnT wr h0 + 1
     /\ (authId i ==>
	     //fragment was definitely snoc'd
	     StAE.fragments wr h1 == snoc (StAE.fragments wr h0) f
     	     //delta was maybe snoc'd, if f is not a handshake fragment
	     /\ SD.stream_deltas wr h1 == Seq.append (SD.stream_deltas wr h0) (SD.project_one_frag f)
	     //and the deltas associated with wr will forever more contain deltas1 as a prefix
             /\ ST.witnessed (SD.deltas_prefix wr (SD.stream_deltas wr h1))))

val sendFragment: c:connection -> #i:id -> wo:option (cwriter i c) -> f: Content.fragment i -> ST (result unit)
  (requires (sendFragment_inv wo))
  (ensures (fun h0 r h1 ->
    //we still have st_inv, etc.
    sendFragment_inv wo h1
    //we didn't advance any epochs
    /\ (current_writer_pre c i h0 ==> current_writer_pre c i h1
				   /\ current_writer_T c i h0 == current_writer_T c i h1)
    /\ (currentId_T c Writer h1 = currentId_T c Writer h0)
    //behavior in the erroneous cases
    /\ (None? wo \/ r=ad_overflow ==> modifies Set.empty h0 h1)
    /\ (r=ad_overflow ==> Some? wo /\ not(StAE.incrementable (Some?.v wo) h1))
    //correct behavior, including projections suitable for both the handshake (fragments) and the application (deltas)
    /\ (r<>ad_overflow ==> sendFragment_success Set.empty c i wo f h0 h1)))

#reset-options "--z3rlimit 100 --initial_fuel 0 --max_fuel 0 --initial_ifuel 1 --max_ifuel 1 --admit_smt_queries true"
let sendFragment c #i wo f =
  reveal_epoch_region_inv_all ();
  let ct, rg = Content.ct_rg i f in
  let idt = if ID12? i then "ID12" else if ID13? i then "ID13" else "PlaintextID" in
  trace ("send "^Content.ctToString ct^" fragment with index "^idt);
  if not (check_incrementable wo)
  then ad_overflow
  else begin
       let payload: Content.encrypted f =
           match wo with
	   | None    ->
	     assert (PlaintextID? i);
	     Content.repr i f
	   | Some wr ->
             begin
             (match wr with
              | StAE.Stream _ st ->
                if not (authId i) then
                  let key,salt = StreamAE.leak #i st in
                  trace ("Encrypting with key " ^ (print_bytes key))
              | _ -> ()
             );
	     SD.encrypt wr f
             end
       in
       let pv = Handshake.version_of c.hs in
       lemma_repr_bytes_values (length payload);
       assume (repr_bytes (length payload) <= 2); //NS: How are we supposed to prove this?
       trace ("Sending fragment of length " ^ string_of_int (length payload));
       let r = Record.sendPacket c.tcp ct (PlaintextID? i) pv payload in
       match r with
       | Error x   -> fatal Internal_error x
       | Correct _ -> Correct()
  end

////////////////////////////////////////////////////////////////////////////////
// Sending alerts: this always happens on the current writer
////////////////////////////////////////////////////////////////////////////////
//Cedric says on slack:
//  Functionally, you can only send alerts on the current epoch; so
//  indeed, it is not necessarily the index known at the TLS API level. We
//  have to reflect it in the postconditions of TLS read/write, but we
//  don't have to be fully precise: If we report an error, we can e.g. say
//  that an alert may have been sent on the current epoch.


// 18-10-30 we could statically enforce what alerts are sendable: no warnings etc
#reset-options "--z3rlimit 100 --initial_fuel 0 --max_fuel 0 --initial_ifuel 1 --max_ifuel 1 --admit_smt_queries true"
private let sendAlert (c:connection) (ad:alert) (reason:string)
  :  ST ioresult_w
	(requires (fun h ->
	  let i = currentId_T c Writer h in
	  current_writer_pre c i h
	  /\ sendFragment_inv (current_writer_T c i h) h))
	(ensures (fun h0 r h1 ->
	    let i = currentId_T c Writer h1 in
    	    current_writer_pre c i h1 /\
	    st_inv c h1 /\
	    (match r with
	     | WriteError None _ ->
	       modifies (Set.singleton (C?.region c)) h0 h1
	       //the spec of disconnect is too weak to prove this now
               (* /\ sel h1 c.state = Close *)
	       (* /\ StAE.fragments wr h1 == snoc (StAE.fragments wr h0) f *)
	     | WriteError (Some _) _ ->
	       modifies (Set.singleton (C?.region c)) h0 h1
	       //the spec of disconnect is too weak to prove more than this now
	     | WriteClose ->
	       let wopt = current_writer_T c i h1 in
	       let frag = Content.CT_Alert #i (point 2) ad in
	       let st = sel h0 c.state in
	       sendFragment_success (Set.singleton (C?.region c)) c i wopt frag h0 h1
	       /\ sel h1 c.state = (fst st, Closed)
	     | _ -> False)))
=
    trace ("sendAlert "^TLSError.string_of_error (ad,reason));
    reveal_epoch_region_inv_all ();
    let i = currentId c Writer in
    let wopt = current_writer c i in
    let st = !c.state in
    let res = sendFragment c #i wopt (Content.CT_Alert #i (point 2) ad) in
    match res with
    | Error xy -> unrecoverable c (snd xy) // or reason?
    | Correct _   ->
        if ad.description = Close_notify then
          begin // graceful closure
            c.state := (fst st, Closed);
            WriteClose
          end
        else
          begin
            disconnect c;
            WriteError (Some ad) reason
          end

////////////////////////////////////////////////////////////////////////////////
// Sending handshake messages on a given writer
////////////////////////////////////////////////////////////////////////////////
let sendHandshake_post (#c:connection) (#i:id) (wopt:option (cwriter i c))
		       (om:option (HandshakeLog.fragment i)) (send_ccs:bool) (h0:HS.mem) r (h1:HS.mem) =
      HS.modifies (opt_writer_regions wopt) h0 h1   //didn't modify more than the writer's regions
      /\ (match wopt with
 	 | None -> True
	 | Some wr ->
	   StAE.seqnT wr h0 <= StAE.seqnT wr h1
	   /\ StAE.seqnT wr h1 <= StAE.seqnT wr h0 + 2  //sent at most 2 fragments
	   /\ (authId i ==>
	      (let frags1 = StAE.fragments wr h1 in
 	       let frags0 = StAE.fragments wr h0 in
	       Seq.equal (SD.stream_deltas wr h1) (SD.stream_deltas wr h0) //all the fragments sent are internal to TLS
	       /\ (match r with
		  | Error _ ->
		    //either the handshake message failed or the ccs failed
		    //but we can't really distinguish those cases precisely
		    //Also, the post-condition of sendFragment in the error case is not yet very informative
		    True
		  | _ ->
		    r<>ad_overflow ==>  //if both sends succeeded
		    (match om with
		     | None ->  //if no msg, then we sent at most the CCS
		       if send_ccs
		       then frags1==snoc frags0 (Content.CT_CCS #i (point 1))
		       else frags1==frags0
		     | Some(| rg, f |) -> //we sent the message
		       let frags0' = snoc frags0 (Content.CT_Handshake rg f) in
		       if send_ccs //and the CCS, if requested
		       then frags1==snoc frags0' (Content.CT_CCS #i (point 1))
		       else frags1==frags0')))))

#reset-options "--using_facts_from FStar --using_facts_from Prims --using_facts_from Range --using_facts_from Parse --using_facts_from Connection --using_facts_from Handshake --using_facts_from TLS --using_facts_from TLSError --using_facts_from TLSConstants --using_facts_from 'FStar Prims Range Parse Connection Handshake TLS TLSError TLSConstants'"
#set-options "--z3rlimit 100 --initial_fuel 0 --max_fuel 0 --initial_ifuel 1 --max_ifuel 1 --admit_smt_queries true"
/
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

    wopt: FStar.Pervasives.Native.option (MiTLS.TLS.cwriter i c) ->
    om: FStar.Pervasives.Native.option (MiTLS.HandshakeLog.fragment i) ->
    send_ccs: Prims.bool
  -> FStar.HyperStack.ST.ST (MiTLS.TLSError.result Prims.unit)
MiTLS.Connection.connection MiTLS.TLSInfo.id FStar.Pervasives.Native.option MiTLS.TLS.cwriter MiTLS.HandshakeLog.fragment Prims.bool FStar.Pervasives.Native.Mktuple2 Prims.dtuple2 MiTLS.Range.frange MiTLS.Range.rbytes MiTLS.TLS.sendFragment MiTLS.Content.CT_Handshake MiTLS.TLSError.result Prims.unit MiTLS.TLSError.error FStar.Error.optResult MiTLS.Content.CT_CCS MiTLS.TLS.point FStar.Pervasives.Native.tuple2 FStar.Error.Correct MiTLS.TLS.trace MiTLS.TLS.sendFragment_inv FStar.Monotonic.HyperStack.mem Prims.l_and MiTLS.TLS.sendHandshake_post
let sendHandshake
      (#c: connection)
      (#i: id)
      (wopt: option (cwriter i c))
      (om: option (HandshakeLog.fragment i))
      (send_ccs: bool)
    : ST (result unit)
      (requires (sendFragment_inv wopt))
      (ensures
        (fun h0 r h1 -> sendFragment_inv wopt h1 /\ sendHandshake_post wopt om send_ccs h0 r h1)) =
  
trace "sendHandshake";
match om, send_ccs with
| Some (| rg , f |), false -> sendFragment c wopt (Content.CT_Handshake rg f)
| Some (| rg , f |), true ->
  let result = sendFragment c wopt (Content.CT_Handshake rg f) in
  (match result with
    | Error _ -> result
    | _ -> sendFragment c wopt (Content.CT_CCS (point 1)))
| _, true -> sendFragment c wopt (Content.CT_CCS (point 1))
| _ -> Correct ()