val macAlg_of_aeAlg (pv: protocolVersion) (a: aeAlg{pv <> TLS_1p3 /\ ~(AEAD? a)}) : Tot macAlg
val macAlg_of_aeAlg (pv: protocolVersion) (a: aeAlg{pv <> TLS_1p3 /\ ~(AEAD? a)}) : Tot macAlg
let macAlg_of_aeAlg: (pv:protocolVersion) -> (a:aeAlg { pv <> TLS_1p3 /\ ~(AEAD? a) }) -> Tot macAlg =
  fun pv ae ->
  match pv,ae with
  // 17-02-02 dropping support for weak ciphersuites. To be discussed!
  //  | SSL_3p0,MACOnly alg -> SSLKHash alg (* dropped pattern on the left to simplify refinements *)
  //  | SSL_3p0,MtE _ alg   -> SSLKHash alg
  //  | _      ,MACOnly alg -> SSLKHash alg
  | _      ,MACOnly alg
  | _      ,MtE _ alg   -> alg
(**
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

(* Relocate? *)
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

/// HIGH-LEVEL DECLARATIONS

(** Role of the connection endpoints *)
type role =
  | Client
  | Server
let dualRole = function
  | Client -> Server
  | Server -> Client

(** Polarity for reading and writing on a connection *)
type rw =
  | Reader
  | Writer

/// PROTOCOL VERSION

include MiTLS.Parsers.ProtocolVersion // for TLS_1p3, etc.

inline_for_extraction
type protocolVersion' = Parsers.ProtocolVersion.protocolVersion
inline_for_extraction
type protocolVersion = (p: protocolVersion' { not (Unknown_protocolVersion? p) } )

// aka TLS_1p3
let is_pv_13 = function
  | TLS_1p3 -> true
  | _       -> false

(** Serializing function for the protocol version *)
let versionBytes : protocolVersion' -> Tot (lbytes 2) =
  LowParseWrappers.wrap_serializer32_constant_length protocolVersion_serializer32 2 ()

inline_for_extraction
let parse_protocolVersion_error_msg : string =
  FStar.Error.perror __SOURCE_FILE__ __LINE__ ""

let parseVersion : pinverse_t versionBytes = fun x ->
  LowParseWrappers.wrap_parser32_constant_length protocolVersion_serializer32 2 () protocolVersion_parser32 parse_protocolVersion_error_msg x

(** Determine the oldest protocol versions for TLS *)
let minPV (a:protocolVersion) (b:protocolVersion) =
  match a,b with
  | SSL_3p0, _  | _, SSL_3p0 -> SSL_3p0
  | TLS_1p0, _  | _, TLS_1p0 -> TLS_1p0
  | TLS_1p1, _  | _, TLS_1p1 -> TLS_1p1
  | TLS_1p2, _  | _, TLS_1p2 -> TLS_1p2
  | TLS_1p3, _  | _, TLS_1p3 -> TLS_1p3

let geqPV a b = (b = minPV a b)

// TODO, remove alias
inline_for_extraction noextract let string_of_pv = string_of_protocolVersion 

/// CIPHER SUITES

include MiTLS.CipherSuite

let aeAlg_hash = function
  | MACOnly ha -> ha
  | MtE _ ha -> ha
  | AEAD _ ha -> ha

#set-options "--z3rlimit 100"
(** Determine if this algorithm provide padding support with TLS 1.2 *)
let lhae = function
  | MtE (Block _) _                         -> true
  | MACOnly _ | AEAD _ _ | MtE (Stream _) _ -> false

(** Sequence numbers for StreamAE/StatefulLHAE *)
let is_seqn (n:nat) = repr_bytes n <= 8
type seqn_t = n:nat { is_seqn n }

(** Predicates for Strong Authentication *)
// MtE: ``The AE algorithms are CPA and INT-CTXT''
// MtE: ``The MAC algorithm of id is INT-CMA.''

val strongAuthAlg: protocolVersion -> aeAlg -> Tot bool
//  | MtE _ m | MACOnly m   -> int_cma (macAlg_of_id i)
//  | AEAD e m -> strongAEADalg

let strongAEAlg (_:protocolVersion) (_:aeAlg) : Tot bool= false
// let strongAEAlg pv ae = match ae with
//    | AEAD e m -> true
//    | MtE _ -> false

val strongAuthAE: pv:protocolVersion -> ae:aeAlg -> Lemma(strongAEAlg pv ae ==> strongAuthAlg pv ae)

// we leave these functions abstract for verification purposes
// we may need to be more negative on weak algorithms (so that we don't try to verify their use)
// and more precise/positive on algorithms we implement (so that we reflect lower assumptions)

(** Encryption key sizes *)
let encKeySize = function
  | Stream EverCrypt.RC4_128 -> 16
  | Block a                  -> UInt32.v (EverCrypt.block_cipher_keyLen a)

(** AEAD salt sizes *)
let aeadSaltSize =
  let open MiTLS.EverCrypt in function // TLS 1.3 IV salt.
  | AES128_GCM       -> 4
  | AES256_GCM       -> 4
  | CHACHA20_POLY1305 -> 12
  | _                 -> 4 //recheck

(** AEAD *)
let aeadRecordIVSize =
  let open MiTLS.EverCrypt in function // TLS 1.2 explicit IVs
  | AES128_GCM       -> 8
  | AES256_GCM       -> 8
  | CHACHA20_POLY1305 -> 0
  | _                 -> 8 //recheck


// -----------------------------------------------------------------------
// record-layer length constants [5.2.1]
// note that TLS 1.3 lowers a bit the upper bound of cipher lengths (Ok in principle)
// but still enables padding beyond plausible plaintext lengths.

(** Constants for API and protocol-level fragments are in [0..2^14] *)
let max_TLSPlaintext_fragment_length     = 16384
let max_TLSCompressed_fragment_length    = max_TLSPlaintext_fragment_length + 1024
let max_TLSCiphertext_fragment_length    = max_TLSPlaintext_fragment_length + 2048
let max_TLSCiphertext_fragment_length_13 = max_TLSPlaintext_fragment_length + 256

/// SIGNATURE SCHEME
 
// signatureScheme enum
include MiTLS.Parsers.SignatureScheme

let is_handshake13_signatureScheme = function
  | Ecdsa_secp256r1_sha256
  | Ecdsa_secp384r1_sha384
  | Ecdsa_secp521r1_sha512
  | Ed25519
  | Ed448
  | Rsa_pss_rsae_sha256
  | Rsa_pss_rsae_sha384
  | Rsa_pss_rsae_sha512
  | Rsa_pss_pss_sha256
  | Rsa_pss_pss_sha384
  | Rsa_pss_pss_sha512 -> true
  | _ -> false

let is_supported_signatureScheme = function
  | Rsa_pkcs1_sha1
  | Ecdsa_sha1
  | Rsa_pkcs1_sha256
  | Rsa_pkcs1_sha384
  | Rsa_pkcs1_sha512
  | Ecdsa_secp256r1_sha256
  | Ecdsa_secp384r1_sha384
  | Ecdsa_secp521r1_sha512
  | Rsa_pss_rsae_sha256
  | Rsa_pss_rsae_sha384
  | Rsa_pss_rsae_sha512
  | Rsa_pss_pss_sha256
  | Rsa_pss_pss_sha384
  | Rsa_pss_pss_sha512 -> true
  | _ -> false

type supported_signatureScheme = s:signatureScheme{is_supported_signatureScheme s}

let sigHashAlg_of_signatureScheme (s:supported_signatureScheme) : (sigAlg * hashAlg) =
  let open MiTLS.Hashing.Spec in
  match s with
  | Rsa_pkcs1_sha1 -> (RSASIG, Hash SHA1)
  | Ecdsa_sha1 -> (ECDSA, Hash SHA1)
  | Rsa_pkcs1_sha256 -> (RSASIG, Hash SHA2_256)
  | Rsa_pkcs1_sha384 -> (RSASIG, Hash SHA2_384)
  | Rsa_pkcs1_sha512 -> (RSASIG, Hash SHA2_512)
  | Ecdsa_secp256r1_sha256 -> (ECDSA, Hash SHA2_256)
  | Ecdsa_secp384r1_sha384 -> (ECDSA, Hash SHA2_384)
  | Ecdsa_secp521r1_sha512 -> (ECDSA, Hash SHA2_512)
  | Rsa_pss_rsae_sha256 -> (RSAPSS, Hash SHA2_256)
  | Rsa_pss_rsae_sha384 -> (RSAPSS, Hash SHA2_384)
  | Rsa_pss_rsae_sha512 -> (RSAPSS, Hash SHA2_512)
  | Rsa_pss_pss_sha256 -> (RSAPSS, Hash SHA2_256)
  | Rsa_pss_pss_sha384 -> (RSAPSS, Hash SHA2_384)
  | Rsa_pss_pss_sha512 -> (RSAPSS, Hash SHA2_512)

let signatureScheme_of_sigHashAlg (sa:sigAlg) (ha:hashAlg) : signatureScheme =
  let open MiTLS.Hashing.Spec in
  match sa, ha with
  | (RSASIG, Hash MD5) -> Rsa_pkcs1_md5
  | (RSASIG, Hash SHA1) -> Rsa_pkcs1_sha1
  | (RSASIG, Hash SHA2_256) -> Rsa_pkcs1_sha256
  | (RSASIG, Hash SHA2_384) -> Rsa_pkcs1_sha384
  | (RSASIG, Hash SHA2_512) -> Rsa_pkcs1_sha512
  | (ECDSA,  Hash MD5) -> Ecdsa_md5
  | (ECDSA,  Hash SHA1) -> Ecdsa_sha1
  | (ECDSA,  Hash SHA2_256) -> Ecdsa_secp256r1_sha256
  | (ECDSA,  Hash SHA2_384) -> Ecdsa_secp384r1_sha384
  | (ECDSA,  Hash SHA2_512) -> Ecdsa_secp521r1_sha512
  | (RSAPSS, Hash SHA2_256) -> Rsa_pss_rsae_sha256
  | (RSAPSS, Hash SHA2_384) -> Rsa_pss_rsae_sha384
  | (RSAPSS, Hash SHA2_512) -> Rsa_pss_rsae_sha512
  | _ -> Unknown_signatureScheme 0us

include MiTLS.Parsers.SignatureSchemeList

let signatureSchemeListBytes (algs:signatureSchemeList)
: Tot (b:bytes{4 <= length b /\ length b < 65538}) =
  signatureSchemeList_serializer32 algs

let parseSignatureSchemeList: pinverse_t signatureSchemeListBytes = fun b ->
  let emsg = perror __SOURCE_FILE__ __LINE__ "Failed to parse signature scheme list" in
  LowParseWrappers.wrap_parser32 signatureSchemeList_parser32 emsg b

/// COMPRESSION (LARGELY DEPRECATED IN TLS 1.3)

(** Compression definition *)

include MiTLS.Parsers.CompressionMethod // for NullCompression

inline_for_extraction
type compression = compressionMethod

(** Serializing function for compression algorithms *)
let compressionBytes: compression -> Tot (lbytes 1) =
  LowParseWrappers.wrap_serializer32_constant_length compressionMethod_serializer32 1 ()

// Not pinverse_t compressionBytes, because it never fails.

(** Parsing function for compression algorithm *)
let parseCompression: b:lbytes 1
  -> Tot (cm:compression{compressionBytes cm == b}) =
  LowParseWrappers.wrap_parser32_total_constant_length compressionMethod_serializer32 compressionMethod_parser32 1 ()

// We ignore compression methods we don't understand. This is a departure
// from usual parsing, where we fail on unknown values, but that's how TLS
// handles compression method lists.

type compressions = cms: list compression {List.length cms <= 254}

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

(** Parsing function for compression algorithm lists *)
let rec parseCompressions (b:bytes {length b <= 254})
: Tot (cms: compressions {List.length cms = length b}) (decreases (length b)) =
  if length b = 0
  then
    let cms: list compression = [] in
    assert_norm (List.length cms = 0); //libraries?
    cms
  else (
    let cmB,b' = split b 1ul in
    let cm = parseCompression cmB in
    let cms' = parseCompressions b' in
    let cms = cm :: cms' in
    assert_norm(List.length cms = 1 + List.length cms'); //library?
    cms )

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

(** Serializing function for lists of compression algorithms *)
let rec compressionMethodsBytes
  (cms: compressions) : Tot (lbytes (List.Tot.length cms)) =
  match cms with
  | c::cs -> compressionBytes c @| compressionMethodsBytes cs
  | []   -> empty_bytes

#reset-options

#reset-options "--admit_smt_queries true"

// Some of these could be hidden in Handshake.Secret

(** Definition for the PRF label type *)
type prflabel = bytes

(** Key schedule labels *)
let extract_label          = utf8_encode "master secret"
let extended_extract_label = utf8_encode "extended master secret"
let kdf_label              = utf8_encode "key expansion"

(** PRF definitions based on the protocol version *)
type prePrfAlg =
  | PRF_SSL3_nested         // MD5(SHA1(...)) for extraction and keygen
  | PRF_SSL3_concat         // MD5 @| SHA1    for VerifyData tags
  | PRF_TLS_1p01 of prflabel                       // MD5 xor SHA1
  | PRF_TLS_1p2 : prflabel -> macAlg -> prePrfAlg  // typically SHA2_256 but may depend on CS
  | PRF_TLS_1p3 // TBC

(** PRF associations *)
//BB.TODO: Documentation ?
type kefAlg_t = prePrfAlg
type kdfAlg_t = prePrfAlg
type vdAlg_t = protocolVersion * cipherSuite

// Only to be invoked with TLS 1.2 (hardcoded in previous versions)
// BB.TODO: Documentation ? Confirm that it is used with TLS 1.3 ! CF: no, for TLS 1.3 use hash_len a, e.g. 32 or 64
// let verifyDataLen_of_ciphersuite (cs:cipherSuite) = 12

// Only to be invoked with TLS 1.2 (hardcoded in previous versions)
let prfMacAlg_of_ciphersuite_aux: cipherSuite -> Tot (option macAlg) =
  let open MiTLS.Hashing.Spec in function
  | CipherSuite  _ _  (MtE  _ _ )   -> Some SHA2_256
  | CipherSuite  _ _  (AEAD _ hAlg) -> Some hAlg
  | CipherSuite  _ _  (MACOnly _)   -> Some SHA2_256 //MK was (MACOnly hAlg) should it also be be (HMAC hAlg)?
  | _                               -> None

(** Determine if the tuple PV and CS is the correct association with PRF *)
let pvcs (pv:protocolVersion) (cs:cipherSuite) =
  match pv, cs with
  | TLS_1p3, CipherSuite13 _ _ -> true
  | TLS_1p3, CipherSuite _ _ _ -> false
  | pv, CipherSuite _ _ _ -> Some? (prfMacAlg_of_ciphersuite_aux cs)
  | _                 -> false

unfold type require_some (#a:Type) (#b:Type) ($f:(a -> Tot (option b))) =
  x:a{Some? (f x)} -> Tot b

let prfMacAlg_of_ciphersuite : require_some prfMacAlg_of_ciphersuite_aux =
  fun x -> Some?.v (prfMacAlg_of_ciphersuite_aux x)

// PRF and verifyData hash algorithms are potentially independent in TLS 1.2,
// so we use two distinct functions. However, all currently defined ciphersuites
// use the same hash algorithm, so the current implementation of the two functions
// is the same.

// Only to be invoked with TLS 1.2 (hardcoded in previous versions
// BB.TODO: Documentation ? Confirm that it is used with TLS 1.3 !
private
let verifyDataHashAlg_of_ciphersuite_aux =
  let open MiTLS.Hashing.Spec in function
  | CipherSuite _ _ (MtE  _ _) -> Some SHA2_256
  | CipherSuite _ _ (AEAD _ hAlg) -> Some hAlg
  | CipherSuite _ _ (MACOnly hAlg) -> Some SHA2_256
  | CipherSuite13 _ hAlg -> Some hAlg
  | _ -> None

// BB.TODO: Documentation ?
let verifyDataHashAlg_of_ciphersuite : require_some verifyDataHashAlg_of_ciphersuite_aux =
  fun x -> Some?.v (verifyDataHashAlg_of_ciphersuite_aux x)

let verifyDataHashAlg_of_ciphersuitename (n: cipherSuiteName) =
  match cipherSuite_of_name n with
  | None -> None
  | Some c -> verifyDataHashAlg_of_ciphersuite_aux c

(** Determine which session hash algorithm is to be used with the protocol version and ciphersuite *)
let sessionHashAlg: pv:protocolVersion -> cs:cipherSuite{pvcs pv cs} -> Tot hashAlg =
  fun pv cs ->
  let open MiTLS.Hashing.Spec in
  match pv with
  | TLS_1p3 -> let CipherSuite13 _ h = cs in Hash h
  | SSL_3p0 | TLS_1p0 | TLS_1p1 -> MD5SHA1 // FIXME: DSA uses only SHA1
  | TLS_1p2 -> Hash (verifyDataHashAlg_of_ciphersuite cs)

// TODO recheck this is the right hash for HKDF
// SZ: Right. The TLS 1.3 draft says "Where HMAC [RFC2104] uses
// the Hash algorithm for the handshake"

(** Determine the Authenticated Encryption algorithm associated with a ciphersuite *)
let get_aeAlg: cs:cipherSuite{ CipherSuite? cs \/ CipherSuite13? cs } -> Tot aeAlg =
  fun cs ->
  match cs with
  | CipherSuite _ _ ae -> ae
  | CipherSuite13 a h -> AEAD a h

//(** Define the null authenticated encryption algorithm *)
// BB: Why does this default to MD5 ?
//let null_aeAlg = MACOnly MD5

(** Determine Encryption type to be used with a chosen PV and AE algorithm *)
let encAlg_of_aeAlg: (pv:protocolVersion) -> (a:aeAlg { MtE? a }) -> Tot (encAlg * ivMode) =
  fun pv ae ->
  match pv,ae with
  | SSL_3p0, MtE (Block e) m -> (Block e),Stale
  | TLS_1p0, MtE (Block e) m -> (Block e),Stale
  | _, MtE e m -> e,Fresh
/
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

    pv: MiTLS.TLSConstants.protocolVersion ->
    a: MiTLS.CipherSuite.aeAlg{pv <> MiTLS.Parsers.ProtocolVersion.TLS_1p3 /\ ~(AEAD? a)}
  -> MiTLS.CipherSuite.macAlg
MiTLS.TLSConstants.protocolVersion MiTLS.CipherSuite.aeAlg Prims.l_and Prims.b2t Prims.op_disEquality MiTLS.Parsers.ProtocolVersion.protocolVersion MiTLS.Parsers.ProtocolVersion.TLS_1p3 Prims.l_not MiTLS.CipherSuite.uu___is_AEAD FStar.Pervasives.Native.Mktuple2 MiTLS.CipherSuite.hash_alg MiTLS.CipherSuite.encAlg MiTLS.CipherSuite.macAlg
let macAlg_of_aeAlg: pv: protocolVersion -> a: aeAlg{pv <> TLS_1p3 /\ ~(AEAD? a)} -> Tot macAlg =
  
fun pv ae -> match pv, ae with | _, MACOnly alg | _, MtE _ alg -> alg