val macSize : a: Spec.Hash.Definitions.fixed_len_alg
  -> n: Lib.IntTypes.size_t{Lib.IntTypes.v n = Spec.Hash.Definitions.hash_length a}
let macSize = Hacl.Hash.Definitions.hash_len
module MiTLS.CipherSuite
open MiTLS

open FStar.Seq
open FStar.UInt32
open FStar.Bytes
open FStar.Error
open MiTLS.TLSError

open MiTLS.Mem
module Parse = MiTLS.Parse
//include Parse


/// CIPHERSUITES, with new structure for TLS 1.3
/// 18-02-22 QD fodder, will require a manual translation as we
/// primarily use this structured ADT --- see also cipherSuiteName
/// below, closer to the RFC.

include MiTLS.Parsers.CipherSuite // for TLS_DH_DSS_WITH_3DES_EDE_CBC_SHA

/// Various elements used in ciphersuites

(** Signature algorithms *)
type sigAlg =
 | RSASIG
 | DSA
 | ECDSA
 | RSAPSS

(** Key exchange algorithms **)
type kexAlg =
  | Kex_RSA
  | Kex_DH
  | Kex_PSK
  | Kex_PSK_DHE
  | Kex_PSK_ECDHE
  | Kex_DHE
  | Kex_ECDHE

(** Crypto algorithm names are defined in EverCrypt **)
type blockCipher = EverCrypt.block_cipher_alg
type streamCipher = EverCrypt.stream_cipher_alg
type aeadAlg = EverCrypt.aead_alg

(** Modes for the initialization vectors *)
type ivMode =
  | Fresh
  | Stale

(** Encryption types *)
type encAlg =
  | Block of blockCipher
  | Stream of streamCipher

(** TLS-specific hash and MAC algorithms *)

//18-09-08 eliminate once EverCrypt/Hashing are stable.

type hash_alg = Hashing.Spec.alg
type hashAlg = Hashing.Spec.tls_alg
type macAlg = Hashing.Spec.alg

let hashSize = Hashing.Spec.tls_tagLen
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.Parsers.CipherSuite.fsti.checked MiTLS.Parse.fst.checked MiTLS.Mem.fst.checked MiTLS.LowParseWrappers.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.EverCrypt.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.CipherSuite.fsti
a: Spec.Hash.Definitions.fixed_len_alg
  -> n: Lib.IntTypes.size_t{Lib.IntTypes.v n = Spec.Hash.Definitions.hash_length a}
Hacl.Hash.Definitions.hash_len
let macSize =
  
Hacl.Hash.Definitions.hash_len