val default_cipherSuites : Prims.list MiTLS.Parsers.CipherSuite.cipherSuite
let default_cipherSuites = [
  TLS_AES_128_GCM_SHA256;
  TLS_AES_256_GCM_SHA384;
  TLS_CHACHA20_POLY1305_SHA256;
  TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256;
  TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256;
  TLS_DHE_RSA_WITH_AES_128_GCM_SHA256;
  TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384;
  TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384;
  TLS_DHE_RSA_WITH_AES_256_GCM_SHA384;
  TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256;
  TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256;
  TLS_DHE_RSA_WITH_CHACHA20_POLY1305_SHA256;
  ]
module MiTLS.TLSInfo
open MiTLS

#reset-options "--using_facts_from '* -LowParse.Spec.Base'"

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

(* This module gathers the definitions of
   public datatypes, parameters, and predicates for our TLS API.

   Its interface is used by most TLS modules;
   its implementation is typechecked.
*)

open FStar.Bytes
open MiTLS.Mem
open MiTLS.TLSConstants

module DM = FStar.DependentMap
module MDM = FStar.Monotonic.DependentMap
module HST = FStar.HyperStack.ST
/
prims.fst.checked MiTLS.TLSInfoFlags.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.PSK.fst.checked MiTLS.PMS.fst.checked MiTLS.Parsers.SignatureSchemeList.fsti.checked MiTLS.Parsers.NamedGroupList.fsti.checked MiTLS.Parsers.NamedGroup.fsti.checked MiTLS.Nonce.fsti.checked MiTLS.Mem.fst.checked MiTLS.HMAC.fsti.checked MiTLS.Flags.fst.checked MiTLS.CommonDH.fsti.checked MiTLS.Cert.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.DependentMap.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.Dyn.fsti.checked FStar.DependentMap.fsti.checked FStar.Bytes.fsti.checked
MiTLS.TLSInfo.fst
Prims.list MiTLS.Parsers.CipherSuite.cipherSuite
Prims.Cons MiTLS.Parsers.CipherSuite.cipherSuite MiTLS.Parsers.CipherSuite.TLS_AES_128_GCM_SHA256 MiTLS.Parsers.CipherSuite.TLS_AES_256_GCM_SHA384 MiTLS.Parsers.CipherSuite.TLS_CHACHA20_POLY1305_SHA256 MiTLS.Parsers.CipherSuite.TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256 MiTLS.Parsers.CipherSuite.TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 MiTLS.Parsers.CipherSuite.TLS_DHE_RSA_WITH_AES_128_GCM_SHA256 MiTLS.Parsers.CipherSuite.TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384 MiTLS.Parsers.CipherSuite.TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 MiTLS.Parsers.CipherSuite.TLS_DHE_RSA_WITH_AES_256_GCM_SHA384 MiTLS.Parsers.CipherSuite.TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256 MiTLS.Parsers.CipherSuite.TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256 MiTLS.Parsers.CipherSuite.TLS_DHE_RSA_WITH_CHACHA20_POLY1305_SHA256 Prims.Nil
let default_cipherSuites =
  
[
  TLS_AES_128_GCM_SHA256; TLS_AES_256_GCM_SHA384; TLS_CHACHA20_POLY1305_SHA256;
  TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256; TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256;
  TLS_DHE_RSA_WITH_AES_128_GCM_SHA256; TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384;
  TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384; TLS_DHE_RSA_WITH_AES_256_GCM_SHA384;
  TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256; TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256;
  TLS_DHE_RSA_WITH_CHACHA20_POLY1305_SHA256
]