val get_mode: hs -> ST Negotiation.mode
  (requires fun h0 -> True)
  (ensures fun h0 _ h1 -> h0 == h1)
val get_mode: hs -> ST Negotiation.mode
  (requires fun h0 -> True)
  (ensures fun h0 _ h1 -> h0 == h1)
let get_mode (s:hs) = Nego.getMode s.nego
module MiTLS.Old.Handshake
open MiTLS

open FStar.String
open FStar.Heap
open FStar.HyperStack
open FStar.Seq
open FStar.Error
open FStar.Bytes

open MiTLS.TLSError
open MiTLS.TLSInfo
open MiTLS.TLSConstants
open MiTLS.Range
open MiTLS.HandshakeMessages // for the message syntax
open MiTLS.HandshakeLog // for Outgoing
open MiTLS.Old.Epochs

module U32 = FStar.UInt32
module MS = FStar.Monotonic.Seq
module Nego = MiTLS.Negotiation
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module Epochs = MiTLS.Old.Epochs
module KeySchedule = MiTLS.Old.KeySchedule
module HMAC_UFCMA = MiTLS.Old.HMAC.UFCMA
// For readabililty, we try to open/abbreviate fewer modules


(* A flag for runtime debugging of Handshake 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 ("HS | "^s^"\n"))
unfold val trace: s:string -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
unfold let trace = if DebugFlags.debug_HS then print else (fun _ -> ())


// TODO : implement resumption
//val getCachedSession: cfg:config -> ch:ch -> ST (option session)
//  (requires (fun h -> True))
//  (ensures (fun h0 i h1 -> True))
//let getCachedSession cfg cg = None


// *** internal stuff: state machine, reader/writer counters, etc.

// some states keep digests (irrespective of their hash algorithm)
type digest = l:bytes{length l <= 32}

private
let finishedId = HMAC_UFCMA.finishedId

#set-options "--admit_smt_queries true"
type machineState =
  | C_Idle
  | C_Wait_ServerHello
  | C_Wait_Finished1           // TLS 1.3
  | C_Sent_EOED:
    digest ->
    option HandshakeMessages.cr13 ->
    i:finishedId & cfk:KeySchedule.fink i -> machineState // TLS 1.3#20 aggravation
  | C_Wait_CCS1 of digest      // TLS resume, digest to be MACed by server
  | C_Wait_R_Finished1 of digest // TLS resume, digest to be MACed by server
  | C_Wait_ServerHelloDone     // TLS classic
  | C_Wait_CCS2 of digest      // TLS classic, digest to be MACed by server
  | C_Wait_Finished2 of digest // TLS classic, digest to be MACed by server
  | C_Complete

  | S_Idle
  | S_Sent_ServerHello         // TLS 1.3, intermediate state to encryption
  | S_Wait_EOED                // Waiting for EOED
  | S_Wait_Finished2 of digest // TLS 1.3, digest to be MACed by client
  | S_Wait_CCS1                   // TLS classic
  | S_Wait_Finished1 of digest // TLS classic, digest to the MACed by client
  | S_Wait_CCS2 of digest      // TLS resume (CCS)
  | S_Wait_CF2 of digest       // TLS resume (CF)
  | S_Complete

//17-03-24 consider using instead "if role = Client then clientState else serverServer"
//17-03-24 but that may break extraction to KaRaMeL and complicate typechecking
//17-03-24 we could also use two refinements.

// Removed error states, consider adding again to ensure the machine is stuck?

noeq type hs' = | HS:
  #region: rgn {is_hs_rgn region} ->
  r: role ->
  nego: Nego.t region r ->
  log: HandshakeLog.t {HandshakeLog.region_of log = region} ->
  ks: KeySchedule.ks (*region*) ->
  epochs: epochs region (Nego.nonce nego) ->
  state: ref machineState {HS.frameOf state = region} -> // state machine; should be opaque and depend on r.
  hs'

let hs = hs' //17-04-08 interface limitation

let nonce (s:hs) = Nego.nonce s.nego
let region_of (s:hs) = s.region
let role_of (s:hs) = s.r
let random_of (s:hs) = nonce s
let config_of (s:hs) = Nego.local_config s.nego
/
prims.fst.checked MiTLS.TLSPRF.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Ticket.fst.checked MiTLS.Range.fst.checked MiTLS.Random.fst.checked MiTLS.PSK.fst.checked MiTLS.Parse.fst.checked MiTLS.Old.KeySchedule.fsti.checked MiTLS.Old.HMAC.UFCMA.fsti.checked MiTLS.Old.Epochs.fsti.checked MiTLS.Negotiation.fst.checked MiTLS.Hashing.fsti.checked MiTLS.HandshakeMessages.fsti.checked MiTLS.HandshakeLog.fsti.checked MiTLS.Extensions.fsti.checked MiTLS.DebugFlags.fst.checked MiTLS.CommonDH.fsti.checked MiTLS.Cert.fsti.checked FStar.UInt32.fsti.checked FStar.String.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.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Error.fst.checked FStar.Date.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Old.Handshake.fst
s: MiTLS.Old.Handshake.hs -> FStar.HyperStack.ST.ST MiTLS.Negotiation.mode
MiTLS.Old.Handshake.hs MiTLS.Negotiation.getMode MiTLS.Old.Handshake.__proj__HS__item__region MiTLS.Old.Handshake.__proj__HS__item__r MiTLS.Old.Handshake.__proj__HS__item__nego MiTLS.Negotiation.mode
let get_mode (s: hs) =
  
Nego.getMode s.nego