val find_supported_versions : o: MiTLS.HandshakeMessages.ch -> FStar.Pervasives.Native.option MiTLS.Extensions.protocol_versions
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
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
/
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
o: MiTLS.HandshakeMessages.ch -> FStar.Pervasives.Native.option MiTLS.Extensions.protocol_versions
MiTLS.HandshakeMessages.ch MiTLS.Negotiation.find_client_extension MiTLS.Extensions.uu___is_E_supported_versions MiTLS.Extensions.unknown FStar.Pervasives.Native.None MiTLS.Extensions.protocol_versions FStar.Pervasives.Native.Some FStar.Pervasives.Native.option
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