val tagged (m: msg) : bool
val tagged (m: msg) : bool
let tagged (m: msg): bool =
  match m with
  | ClientHello _
  | ServerHello _
  | EndOfEarlyData        // for Client finished
  | Certificate13 _       // for CertVerify payload in TLS 1.3
  | EncryptedExtensions _ // For PSK handshake: [EE; Finished]
  | CertificateVerify _   // for ServerFinish payload in TLS 1.3
  | ClientKeyExchange _   // only for client signing
  | NewSessionTicket _    // for server finished in TLS 1.2
  | Finished _ -> true    // for 2nd Finished
  | _ -> false
module MiTLS.HandshakeLog
open MiTLS

/// Handles incoming and outgoing messages for the TLS handshake,
/// grouping them into flights, hiding their parsing/formatting, and
/// incrementally computing hashes of the whole session transcript.
///
/// Private state is held in a single reference (with a local
/// specification expressed using refinements) so we don't need an
/// external stateful invariant.
///
/// 18-02-28 To support stateless HelloRetryRequests, we will now
///          tolerate updates on the server in the initial "open"
///          state (and hence need a stateful invariant) until the
///          hash algorithm is fixed.
/// 
/// 17-11-11 Partly verified, still missing regions and modifies
///          clauses.  We are planning a rewrite of this interface
///          from lists of messages to constructed flights, to
///          facilitate its low-level extraction.

(* TODO
- add subregion discipline and the corresponding framing conditions
- make prior ghost
- add record-layer calls, keeping track of bytes buffers and their effective lengths
- support abstract plaintexts and multiple epochs
*)

open FStar.Ghost 

open MiTLS.Mem
open MiTLS.HandshakeMessages // for pattern matching on messages

module HS = FStar.HyperStack

open FStar.Error
open MiTLS.TLSError
open MiTLS.Hashing
open MiTLS.Hashing.CRF
open FStar.Bytes

let hash = Hashing.h //18-08-31 
  
type msg = HandshakeMessages.hs_msg

/// Specifies which messages indicate the end of incoming flights and
/// triggers their handshake processing.
let eoflight =
  let open MiTLS.HandshakeMessages in function
  | ClientHello _
  | HelloRetryRequest _
  | EndOfEarlyData
  | ServerHello _
  | ServerHelloDone
  | NewSessionTicket13 _
  | Finished _ -> true
  | _ -> false
// No support for binders yet

/// Specifies which messages require an intermediate transcript hash
/// in incoming flights. In doubt, we hash!
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Range.fst.checked MiTLS.Mem.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.Hashing.CRF.fsti.checked MiTLS.Hashing.fsti.checked MiTLS.HandshakeMessages.fsti.checked MiTLS.CommonDH.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.Set.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.HandshakeLog.fsti
m: MiTLS.HandshakeLog.msg -> Prims.bool
MiTLS.HandshakeLog.msg MiTLS.HandshakeMessages.ch MiTLS.HandshakeMessages.sh MiTLS.HandshakeMessages.crt13 MiTLS.HandshakeMessages.ee MiTLS.HandshakeMessages.cv MiTLS.HandshakeMessages.cke MiTLS.HandshakeMessages.sticket MiTLS.HandshakeMessages.fin MiTLS.HandshakeMessages.hs_msg Prims.bool
let tagged (m: msg) : bool =
  
match m with
| ClientHello _
| ServerHello _
| EndOfEarlyData
| Certificate13 _
| EncryptedExtensions _
| CertificateVerify _
| ClientKeyExchange _
| NewSessionTicket _
| Finished _ -> true
| _ -> false