val default_signature_schemes : Prims.list MiTLS.Parsers.SignatureScheme.signatureScheme
let default_signature_schemes =
  let schemes = [
    Ecdsa_secp256r1_sha256; Ecdsa_secp384r1_sha384; Ecdsa_secp521r1_sha512;
    Rsa_pss_rsae_sha256; Rsa_pss_rsae_sha384; Rsa_pss_rsae_sha512;
    Rsa_pkcs1_sha256; Rsa_pkcs1_sha384; Rsa_pkcs1_sha512;
    Ecdsa_sha1; Rsa_pkcs1_sha1
  ] in
  assert_norm (List.Tot.length schemes <= Parsers.SignatureSchemeList.max_count);
  assert_norm (List.Tot.for_all is_supported_signatureScheme schemes);
  schemes
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

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;
  ]
/
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.SignatureScheme.signatureScheme
Prims.unit FStar.Pervasives.assert_norm Prims.b2t FStar.List.Tot.Base.for_all MiTLS.Parsers.SignatureScheme.signatureScheme MiTLS.TLSConstants.is_supported_signatureScheme Prims.op_LessThanOrEqual FStar.List.Tot.Base.length MiTLS.Parsers.SignatureSchemeList.max_count Prims.list Prims.Cons MiTLS.Parsers.SignatureScheme.Ecdsa_secp256r1_sha256 MiTLS.Parsers.SignatureScheme.Ecdsa_secp384r1_sha384 MiTLS.Parsers.SignatureScheme.Ecdsa_secp521r1_sha512 MiTLS.Parsers.SignatureScheme.Rsa_pss_rsae_sha256 MiTLS.Parsers.SignatureScheme.Rsa_pss_rsae_sha384 MiTLS.Parsers.SignatureScheme.Rsa_pss_rsae_sha512 MiTLS.Parsers.SignatureScheme.Rsa_pkcs1_sha256 MiTLS.Parsers.SignatureScheme.Rsa_pkcs1_sha384 MiTLS.Parsers.SignatureScheme.Rsa_pkcs1_sha512 MiTLS.Parsers.SignatureScheme.Ecdsa_sha1 MiTLS.Parsers.SignatureScheme.Rsa_pkcs1_sha1 Prims.Nil
let default_signature_schemes =
  
let schemes =
  [
    Ecdsa_secp256r1_sha256; Ecdsa_secp384r1_sha384; Ecdsa_secp521r1_sha512; Rsa_pss_rsae_sha256;
    Rsa_pss_rsae_sha384; Rsa_pss_rsae_sha512; Rsa_pkcs1_sha256; Rsa_pkcs1_sha384; Rsa_pkcs1_sha512;
    Ecdsa_sha1; Rsa_pkcs1_sha1
  ]
in
assert_norm (List.Tot.length schemes <= Parsers.SignatureSchemeList.max_count);
assert_norm (List.Tot.for_all is_supported_signatureScheme schemes);
schemes