val bindersLen_of_ch : ch: MiTLS.HandshakeMessages.ch -> Prims.int
let bindersLen_of_ch ch =
  match ch.ch_extensions with
  | None -> 0
  | Some el -> Extensions.bindersLen el
(* Copyright (C) 2012--2018 Microsoft Research and INRIA *)
(**
Handshake protocol messages
*)
module MiTLS.HandshakeMessages
open MiTLS
open FStar.Seq
open FStar.Bytes
open FStar.Error
open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.Extensions
open MiTLS.TLSInfo
open MiTLS.Range
open MiTLS.CommonDH
module Parse = MiTLS.Parse
open MiTLS.Parse

// e18-02-21 carved out an interface, far from perfect...
// In particular, it exposes the separate parsing of message headers
// and payloads; I would prefer entirely avoid [handshakeType] or at
// least keep it private

/// Handshake types

type handshakeType =
  | HT_hello_request
  | HT_client_hello
  | HT_server_hello
  | HT_session_ticket
  | HT_end_of_early_data
  | HT_hello_retry_request
  | HT_encrypted_extensions
  | HT_certificate
  | HT_server_key_exchange
  | HT_certificate_request
  | HT_server_hello_done
  | HT_certificate_verify
  | HT_client_key_exchange
  | HT_finished
  | HT_key_update
  | HT_message_hash

#reset-options "--admit_smt_queries true"

val htBytes: handshakeType -> Tot (lbytes 1)
val htBytes_is_injective:
  ht1:handshakeType -> ht2:handshakeType ->
  Lemma (requires (True)) (ensures (htBytes ht1 = htBytes ht2 ==> ht1 = ht2))
  [SMTPat (htBytes ht1); SMTPat (htBytes ht2)]
val parseHt: pinverse_t htBytes
val inverse_ht: x:_ -> Lemma
  (requires True)
  (ensures lemma_inverse_g_f htBytes parseHt x)
  [SMTPat (parseHt (htBytes x))]
val pinverse_ht: x:_ -> Lemma
  (requires True)
  (ensures (lemma_pinverse_f_g equal htBytes parseHt x))
  [SMTPat (htBytes (Correct?._0 (parseHt x)))]


// We follow the structure of the TLS 1.3 RFC,
// but we also include prior TLS messages

/// Key Exchange Messages
/// https://tlswg.github.io/tls13-spec/draft-ietf-tls-tls13.html#rfc.section.4.1

// ClientHello for all protocol versions
noeq type ch = {
  ch_protocol_version: protocolVersion; // max supported version up to TLS_1p2 (TLS 1.3 uses the supported_versions extension)
  ch_client_random: TLSInfo.random;
  ch_sessionID: sessionID;
  ch_cipher_suites: k: list cipherSuiteName{List.Tot.length k < 256};
  ch_compressions: cl:list compression{List.Tot.length cl > 0 /\ List.Tot.length cl < 256};
  ch_extensions: option (ce:list extension{List.Tot.length ce < 256});
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Range.fst.checked MiTLS.Parse.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.Extensions.fsti.checked MiTLS.CommonDH.fsti.checked MiTLS.Cert.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.HandshakeMessages.fsti
ch: MiTLS.HandshakeMessages.ch -> Prims.int
MiTLS.HandshakeMessages.ch MiTLS.HandshakeMessages.__proj__Mkch__item__ch_extensions Prims.list MiTLS.Extensions.extension Prims.b2t Prims.op_LessThan FStar.List.Tot.Base.length MiTLS.Extensions.bindersLen MiTLS.Extensions.unknown Prims.int
let bindersLen_of_ch ch =
  
match ch.ch_extensions with
| None -> 0
| Some el -> Extensions.bindersLen el