val encryptedExtension (ext: extension) : bool
val encryptedExtension (ext: extension) : bool
let encryptedExtension (ext: extension) : bool =
  match ext with
  | E_server_name _
  | E_supported_groups _
  | E_alpn _
  | E_unknown_extension _ _
  | E_early_data _ -> true
  | _ -> false
(* Copyright (C) 2012--2017 Microsoft Research and INRIA *)
(**
This modules defines TLS 1.3 Extensions.

- An AST, and it's associated parsing and formatting functions.
- Nego calls prepareExtensions : config -> list extensions.

@summary: TLS 1.3 Extensions.
*)
module MiTLS.Extensions
open MiTLS

open FStar.Bytes
open FStar.Error
open MiTLS.TLSError
open MiTLS.TLSConstants

(*************************************************
 Define extension.
 *************************************************)

// Extensions may (selectively) appear in the following messages
 type ext_msg =
   | EM_ClientHello
   | EM_ServerHello
   | EM_EncryptedExtensions
   | EM_Certificate
   | EM_NewSessionTicket
   | EM_HelloRetryRequest

(* As a static invariant, we record that any intermediate, parsed
   extension and extension lists can be formatted into bytes without
   overflowing 2^16. This create dependencies on the formatting
   functions, at odd with recursive extensions. *)

(* PRE-SHARED KEYS AND KEY EXCHANGES *)

type pskIdentity = psk_identifier * PSK.obfuscated_ticket_age

// used in a refinement below
val pskiListBytes: list pskIdentity -> bytes

// how to build this type without overflows?? 
noeq type psk =
  | ClientPSK:
    // truncated PSK extension, without the list of binder tags.
    identities: list pskIdentity {let n = length (pskiListBytes identities) in 6 < n /\ n < 65536} ->
    binders_len: nat {binders_len <= 65535} -> psk
  | ServerPSK of UInt16.t
    // index into the client offer's PSK extension

// PSK binders, actually the truncated suffix of TLS 1.3 ClientHello
// We statically enforce length requirements to ensure that formatting is total.

//18-02-20 This should be defined in Hashing 
//18-02-20 We'll need a lemma on HMAC tag lengths. 
type binder = b:bytes {32 <= length b /\ length b <= 255}

(** REMARK: this is more restrictive than in the RFC, which allows up to 2047 binders *)
type binders =
  bs:list binder {1 <= List.Tot.length bs /\ List.Tot.length bs < 255}

// used in HandshakeLog
val bindersBytes: bs:binders -> b:bytes{length b >= 35 /\ length b <= 65537}

// https://tlswg.github.io/tls13-spec/#rfc.section.4.2.8
// restricting both proposed PSKs and future ones sent by the server
// will also be used in the PSK table, and possibly in the configs
type psk_kex =
  | PSK_KE
  | PSK_DHE_KE

type client_psk_kexes = l:list psk_kex
  { l = [PSK_KE] \/ l = [PSK_DHE_KE] \/ l = [PSK_KE; PSK_DHE_KE] \/ l = [PSK_DHE_KE; PSK_KE] }

val client_psk_kexes_length (l:client_psk_kexes): Lemma (List.Tot.length l < 3)

#set-options "--admit_smt_queries true"

(* EARLY DATA INDICATION *)

type earlyDataIndication = option UInt32.t // Some max_early_data_size, only in NewSessionTicket

(* EC POINT FORMATS *)

type point_format =
  | ECP_UNCOMPRESSED
  | ECP_UNKNOWN of (n:nat{repr_bytes n <= 1})

// Move TLSConstants?
val alpnBytes : alpn -> b:bytes{length b < 65536}

// The length exactly reflects the RFC format constraint <2..254>
type protocol_versions =
  | ServerPV of protocolVersion
  | ClientPV of l:list protocolVersion' {0 < List.Tot.length l /\ List.Tot.length l < 128}

// We constrain unknown extensions to have headers different from
// known extensions; we rely on parametricity to avoid recursion
// between the datatype and its formatting property.
type unknownTag = lbytes 2 -> Type0

// ExtensionType and Extension Table in https://tlswg.github.io/tls13-spec/#rfc.section.4.2.
// M=Mandatory, AF=mandatory for Application Features in https://tlswg.github.io/tls13-spec/#rfc.section.8.2.
noeq type extension' (p: unknownTag) =
  | E_server_name of list serverName (* M, AF *) (* RFC 6066 *)
  | E_supported_groups of list CommonDH.namedGroup (* M, AF *) (* RFC 7919 *)
  | E_signature_algorithms of signatureSchemeList (* M, AF *) (* RFC 5246 *)
  | E_signature_algorithms_cert of signatureSchemeList (* TLS 1.3#23 addition; TLS 1.2 should also support it *)
  | E_key_share of CommonDH.keyShare (* M, AF *)
  | E_pre_shared_key of psk (* M, AF *)
  | E_session_ticket of bytes
  | E_early_data of earlyDataIndication
  | E_supported_versions of protocol_versions   (* M, AF *)
  | E_cookie of b:bytes {0 < length b /\ length b < 65536}  (* M *)
  | E_psk_key_exchange_modes of client_psk_kexes (* client-only; mandatory when proposing PSKs *)
  | E_extended_ms
  | E_ec_point_format of list point_format
  | E_alpn of alpn
  | E_unknown_extension: x: lbytes 2 {p x} -> bytes -> extension' p (* header, payload *)
(*
We do not yet support the extensions below (authenticated but ignored)
  | E_max_fragment_length
  | E_status_request
  | E_use_srtp
  | E_heartbeat
  | E_signed_certifcate_timestamp
  | E_client_certificate_type
  | E_server_certificate_type
  | E_certificate_authorities
  | E_oid_filters
  | E_post_handshake_auth
  | E_renegotiation_info of renegotiationInfo
*)



val bindersLen: #p: unknownTag -> el: list (extension' p) -> nat
val string_of_extension: #p: unknownTag -> extension' p -> string
val string_of_extensions: #p: unknownTag -> list (extension' p) -> string

(** shallow equality, comparing just the extension tags *)
val sameExt: #p: unknownTag -> e1: extension' p -> e2: extension' p -> bool

(*************************************************
 extension formatting
 *************************************************)

val unknown: unknownTag
val is_unknown: x: lbytes 2 -> b:bool {b2t b <==> unknown x}
type extension = extension' unknown

// TLSConstants defines the application-level type for custom extensions
val ext_of_custom: custom_extensions -> list extension
val custom_of_ext: list extension -> custom_extensions
val app_ext_filter: option (list extension) -> option (list extension)
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.PSK.fst.checked MiTLS.CommonDH.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt.fsti.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.All.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.Extensions.fsti
ext: MiTLS.Extensions.extension -> Prims.bool
MiTLS.Extensions.extension Prims.list MiTLS.TLSConstants.serverName MiTLS.Parsers.NamedGroup.namedGroup MiTLS.TLSConstants.alpn FStar.Bytes.lbytes MiTLS.Extensions.unknown FStar.Bytes.bytes MiTLS.Extensions.earlyDataIndication MiTLS.Extensions.extension' Prims.bool
let encryptedExtension (ext: extension) : bool =
  
match ext with
| E_server_name _
| E_supported_groups _
| E_alpn _
| E_unknown_extension _ _
| E_early_data _ -> true
| _ -> false