val defaultServerNegoCBFun: nego_cb_fun
val defaultServerNegoCBFun: nego_cb_fun
let defaultServerNegoCBFun _ pv cext ocookie =
  Nego_accept []
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;
  ]

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

let default_groups : CommonDH.supportedNamedGroups =
  let open MiTLS.CommonDH in
  let groups = [
    Secp521r1;
    Secp384r1;
    X25519;
    Secp256r1;
    Ffdhe4096;
    Ffdhe3072;
    Ffdhe2048;
  ] in
  assert_norm (List.Tot.length groups <= Parsers.NamedGroupList.max_count);
  assert_norm (List.Tot.for_all is_supported_group groups);
  groups

// By default we use an in-memory ticket table
// and the in-memory internal PSK database
val defaultTicketCBFun: ticket_cb_fun
let defaultTicketCBFun _ sni ticket info psk =
  let h0 = get() in
  begin
  match info with
  | TicketInfo_12 (pv, cs, ems) ->
    // 2018.03.10 SZ: The ticket must be fresh
    assume False;
    PSK.s12_extend ticket (pv, cs, ems, psk) // modifies PSK.tregion
  | TicketInfo_13 pskInfo ->
    // 2018.03.10 SZ: Missing refinement in ticket_cb_fun
    assume (exists i.{:pattern index psk i} index psk i <> 0z);
    // 2018.03.10 SZ: The ticket must be fresh
    assume False;
    PSK.coerce_psk ticket pskInfo psk;      // modifies psk_region
    PSK.extend sni ticket                   // modifies PSK.tregion
  end;
  let h1 = HST.get() in
  // 2018.03.10 SZ: [ticket_cb_fun] ensures [modifies_none]
  assume (modifies_none h0 h1)

val defaultTicketCB: ticket_cb
let defaultTicketCB = {
  ticket_context = (FStar.Dyn.mkdyn ());
  new_ticket = defaultTicketCBFun;
}
/
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
MiTLS.TLSConstants.nego_cb_fun
FStar.Dyn.dyn MiTLS.TLSConstants.protocolVersion FStar.Bytes.bytes FStar.Pervasives.Native.option MiTLS.TLSConstants.Nego_accept Prims.Nil MiTLS.TLSConstants.custom_extension MiTLS.TLSConstants.nego_action
let defaultServerNegoCBFun _ pv cext ocookie =
  
Nego_accept []