val list_of_ClientKeyShare (ks: list CommonDH.keyShareEntry) : Tot (list pre_share)
val list_of_ClientKeyShare (ks: list CommonDH.keyShareEntry) : Tot (list pre_share)
let rec list_of_ClientKeyShare (ks:list CommonDH.keyShareEntry)
  : Tot (list pre_share) =
  match ks with
  | [] -> []
  | (CommonDH.UnknownShare _ _) :: tl -> list_of_ClientKeyShare tl
  | (CommonDH.Share g s) :: tl -> (|g, s|) :: list_of_ClientKeyShare tl
module MiTLS.Negotiation
open MiTLS

open FStar.Error
open FStar.Bytes

open MiTLS.Mem
open MiTLS.TLSError
open MiTLS.TLSInfo
open MiTLS.TLSConstants
open MiTLS.HandshakeMessages

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

//16-05-31 these opens are implementation-only; overall we should open less
open MiTLS.Extensions

(**
  Debugging flag.
  F* normalizer will erase debug prints at extraction when set to false.
*)
val discard: bool -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
let discard _ = ()
let print s = discard (IO.debug_print_string ("NGO| "^s^"\n"))
unfold val trace: s:string -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
unfold let trace = if DebugFlags.debug_NGO then print else (fun _ -> ())


//17-05-01 relocate these printing functions?!
//18-09-09
let string_of_option_extensions (o: option extensions) = match o with
  | None -> "None"
  | Some es -> "[ "^Extensions.string_of_extensions es^"]"

let string_of_ciphersuite (cs:cipherSuite) =
  string_of_cipherSuite (name_of_cipherSuite cs)

private
let accum_string_of_signatureSchemes s sa =
    s^(string_of_signatureScheme sa)^" "
let string_of_signatureSchemes sal =
  List.Tot.fold_left accum_string_of_signatureSchemes "" sal

private
let accum_string_of_ciphersuite s cs =
    s ^ "; " ^ string_of_ciphersuite cs
let string_of_ciphersuites csl =
  List.Tot.fold_left accum_string_of_ciphersuite "" csl

private
let accum_string_of_namedGroups s ng =
    s ^ "; " ^ (Parsers.NamedGroup.string_of_namedGroup ng)
let string_of_namedGroups ngl =
  List.Tot.fold_left accum_string_of_namedGroups "" ngl

private
let accum_string_of_ciphersuitename s cs =
    s ^ "; " ^ string_of_cipherSuite cs
let string_of_ciphersuitenames csl =
  List.Tot.fold_left accum_string_of_ciphersuitename "" csl

(* Negotiation: HELLO sub-module *)
type ri = cVerifyData * sVerifyData

type resumption_offer_12 = // part of resumeInfo
  | OfferNothing
  | OfferTicket of b:bytes{ length b <> 0 }
  | OfferSid of b:bytes { length b <> 0 }
// type resumption_mode_12 (o: resumption_offer_12) = b:bool { OfferNothing? o ==> b = false }

let valid_offer ch =
  True
// There is a pure function computing a ClientHello from an offer (minus the PSK binders)
type offer = ch:HandshakeMessages.ch { valid_offer ch }


// boilerplate code for accessing individual extensions
// 18-09-09 TODO use lowparse readers (simpler datatypes)

let find_client_extension (filter:Extensions.extension -> bool) o
  : option (e:Extensions.extension{filter e}) =
  match o.ch_extensions with
  | None -> None
  | Some es -> List.Tot.find filter es

let find_client_extension_aux env filter o =
  match o.ch_extensions with
  | None -> None
  | Some es -> List.Helpers.find_aux env filter es

let find_supported_versions o =
  match find_client_extension Extensions.E_supported_versions? o with
  | None -> None
  | Some (Extensions.E_supported_versions vs) -> Some vs

let find_signature_algorithms o : option signatureSchemeList =
  match find_client_extension Extensions.E_signature_algorithms? o with
  | None -> None
  | Some (Extensions.E_signature_algorithms algs) -> Some algs

let find_signature_algorithms_cert o : option signatureSchemeList =
  match find_client_extension Extensions.E_signature_algorithms_cert? o with
  | None -> None
  | Some (Extensions.E_signature_algorithms_cert algs) -> Some algs

let find_cookie o =
  match find_client_extension Extensions.E_cookie? o with
  | None -> None
  | Some (Extensions.E_cookie c) -> Some c

// finding the pre-shared keys in ClientHello
let find_pske o =
  match find_client_extension Extensions.E_pre_shared_key? o with
  | Some (Extensions.E_pre_shared_key (Extensions.ClientPSK psks _)) -> Some psks
  | _ -> None

let find_psk_key_exchange_modes o =
  match find_client_extension Extensions.E_psk_key_exchange_modes? o with
  | Some (Extensions.E_psk_key_exchange_modes l) -> l
  | _ -> []

let find_sessionTicket o =
  match find_client_extension Extensions.E_session_ticket? o with
  | None -> None
  | Some (Extensions.E_session_ticket b) -> Some b

let find_clientPske o =
  match find_client_extension Extensions.E_pre_shared_key? o with
  | Some (Extensions.E_pre_shared_key psk) ->
    (match psk with
    | ServerPSK _ -> None
    | ClientPSK ids tlen -> Some (ids,tlen))
  | _ -> None

let find_serverPske sh =
  match sh.sh_extensions with
  | None -> None
  | Some exts ->
    match List.Tot.find E_pre_shared_key? exts with
    | Some (E_pre_shared_key (ServerPSK idx)) -> Some (UInt16.v idx)
    | _ -> None

let find_serverKeyShare sh =
  match sh.sh_extensions with
  | None -> None
  | Some exts ->
    match List.Tot.find E_key_share? exts with
    | Some (E_key_share (CommonDH.ServerKeyShare ks)) -> Some ks
    | _ -> None

// index in the list of PSKs offered by the client
type pski (o:offer) = n:nat {
  o.ch_protocol_version = TLS_1p3 /\
  (match find_clientPske o with
  | Some (ids,_) -> n < List.length ids
  | _ -> False) }

let find_supported_groups o =
  match find_client_extension Extensions.E_supported_groups? o with
  | None -> None
  | Some (Extensions.E_supported_groups gns) -> Some gns

type share = g:CommonDH.group & CommonDH.share g
type pre_share = g:CommonDH.group & CommonDH.pre_share g

let find_key_shares (o:offer)
  : Tot (option (CommonDH.clientKeyShare))
  =
  match find_client_extension Extensions.E_key_share? o with
  | Some (Extensions.E_key_share (CommonDH.ClientKeyShare ks)) -> Some ks
  | _ -> None
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Ticket.fst.checked MiTLS.Random.fst.checked MiTLS.PSK.fst.checked MiTLS.Parsers.NamedGroup.fsti.checked MiTLS.Mem.fst.checked MiTLS.List.Helpers.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.HandshakeMessages.fsti.checked MiTLS.HandshakeLog.fsti.checked MiTLS.Extensions.fsti.checked MiTLS.DebugFlags.fst.checked MiTLS.CommonDH.fsti.checked MiTLS.Cert.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Option.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Error.fst.checked FStar.Date.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Negotiation.fst
ks: Prims.list MiTLS.CommonDH.keyShareEntry -> Prims.list MiTLS.Negotiation.pre_share
Prims.list MiTLS.CommonDH.keyShareEntry Prims.Nil MiTLS.Negotiation.pre_share MiTLS.Parsers.NamedGroup.namedGroup Prims.b2t FStar.Pervasives.Native.uu___is_None MiTLS.CommonDH.group MiTLS.CommonDH.group_of_namedGroup FStar.Bytes.bytes Prims.l_and Prims.op_LessThanOrEqual FStar.Bytes.repr_bytes FStar.Bytes.length Prims.op_GreaterThan MiTLS.Negotiation.list_of_ClientKeyShare FStar.Pervasives.Native.uu___is_Some MiTLS.CommonDH.namedGroup_of_group MiTLS.CommonDH.pre_share Prims.Cons Prims.Mkdtuple2
let rec list_of_ClientKeyShare (ks: list CommonDH.keyShareEntry) : Tot (list pre_share) =
  
match ks with
| [] -> []
| CommonDH.UnknownShare _ _ :: tl -> list_of_ClientKeyShare tl
| CommonDH.Share g s :: tl -> (| g, s |) :: list_of_ClientKeyShare tl