val fold_string (#a: Type) (f: (a -> string)) (accum sep: string) (al: list a)
    : Tot string (decreases al)
val fold_string (#a: Type) (f: (a -> string)) (accum sep: string) (al: list a)
    : Tot string (decreases al)
let rec fold_string (#a:Type)
                    (f: a -> string)
                    (accum:string)
                    (sep:string)
                    (al:list a) : Tot string (decreases al) =
    match al with
    | [] -> accum
    | a::al -> let accum = accum ^ sep ^ f a in
             fold_string f accum sep al
(**
This file implements type representations and parsing functions
for the different values negotiated during the TLS
handshake. For instance protocol version, key exchange mechanism,
hash algorithm etc.

@summary Module for main constants
*)
module MiTLS.TLSConstants
open MiTLS

/// 18-09-08 contents & triage (beware of scopes)
/// - crypto ==> EverCrypt
/// - datatypes ==> QD
///    7% for signatures
///   53% for ciphersuites!
///   10% for certificates
/// - prf details ==> KeySchedule
/// - parsed extension contents ==> Extensions
/// - split Config (defaults are defined much later); align to EverCrypt
/// - callbacks + ad hoc string conversions ==> FFI ?

//18-02-27 not a reasonable default?
//#set-options "--max_fuel 0 --initial_fuel 0 --max_ifuel 1 --initial_ifuel 1"

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

open MiTLS.Mem
module Parse = MiTLS.Parse
open MiTLS.Parse
//include Parse
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.Parsers.SignatureSchemeList.fsti.checked MiTLS.Parsers.SignatureScheme.fsti.checked MiTLS.Parsers.ProtocolVersion.fsti.checked MiTLS.Parsers.CompressionMethod.fsti.checked MiTLS.Parse.fst.checked MiTLS.Mem.fst.checked MiTLS.LowParseWrappers.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.FFICallbacks.fst.checked MiTLS.EverCrypt.fsti.checked MiTLS.CommonDH.fsti.checked MiTLS.CipherSuite.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.String.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.HyperStack.All.fst.checked FStar.Error.fst.checked FStar.Dyn.fsti.checked FStar.Bytes.fsti.checked
MiTLS.TLSConstants.fsti
f: (_: a -> Prims.string) -> accum: Prims.string -> sep: Prims.string -> al: Prims.list a
  -> Prims.Tot Prims.string
Prims.string Prims.list MiTLS.TLSConstants.fold_string Prims.op_Hat
let rec fold_string (#a: Type) (f: (a -> string)) (accum sep: string) (al: list a)
    : Tot string (decreases al) =
  
match al with
| [] -> accum
| a :: al ->
  let accum = accum ^ sep ^ f a in
  fold_string f accum sep al