val bindersBytes: bs:binders -> b:bytes{length b >= 35 /\ length b <= 65537}
val bindersBytes: bs:binders -> b:bytes{length b >= 35 /\ length b <= 65537}
let bindersBytes bs =
  let b = binderListBytes bs in
  Parse.vlbytes2 b
(* 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
module Parse = MiTLS.Parse
open MiTLS.Parse

#set-options "--initial_fuel 2 --max_fuel 2 --initial_ifuel 1 --max_ifuel 1 --z3rlimit 10"

//NS: hoisting a convenient function to avoid a closure conversion
let rec existsb2 (f: 'a -> 'b -> bool) (x:'a) (y:list 'b) : bool =
  match y with
  | [] -> false
  | hd::tl -> f x hd || existsb2 f x tl

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

//17-05-01 deprecated---use TLSError.result instead?
// SI: seems to be only used internally by parseServerName. Remove.
(** local, failed-to-parse exc. *)
private type canFail (a:Type) =
| ExFail of error 
| ExOK of list a

let error s = fatal Decode_error ("Extensions parsing: "^s)


(* PRE-SHARED KEYS AND KEY EXCHANGES *)

val pskiBytes: psk_identifier * PSK.obfuscated_ticket_age -> bytes

let pskiBytes (i,ot) =
  lemma_repr_bytes_values (UInt32.v ot);
  (vlbytes2 i @| bytes_of_int32 ot)

private
let pskiListBytes_aux acc pski = 
  let pb = pskiBytes pski in
  assume (UInt.fits (length acc + length pb) 32);
  acc @| pb

//val pskiListBytes: list pskIdentity -> bytes
let pskiListBytes ids =
  List.Tot.fold_left pskiListBytes_aux empty_bytes ids


let rec binderListBytes_aux (bl:list binder)
    : Tot (b:bytes{length b <= op_Multiply (List.Tot.length bl) 256}) =
    match bl with
    | [] -> empty_bytes
    | b::t ->
      let bt = binderListBytes_aux t in
      assert(length bt <= op_Multiply (List.Tot.length bl - 1) 256);
      let b0 = Parse.vlbytes1 b in
      assert(length b0 <= 256);
      let bt = binderListBytes_aux t in
      assume (UInt.fits (length b0 + length bt) 32);
      b0 @| bt

val binderListBytes: binders -> Pure (b:bytes)
  (requires True)
  (ensures fun b -> length b >= 33 /\ length b <= 65535)
let binderListBytes bs =
  match bs with
  | h::t ->
    let b = binderListBytes_aux t in
    let b0 = Parse.vlbytes1 h in
    assert(length b0 >= 33);
    assume (UInt.fits (length b0 + length b) 32);
    b0 @| b
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.PSK.fst.checked MiTLS.Parse.fst.checked MiTLS.List.Helpers.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.CommonDH.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Option.fst.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.Error.fst.checked FStar.Classical.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Extensions.fst
bs: MiTLS.Extensions.binders
  -> b: FStar.Bytes.bytes{FStar.Bytes.length b >= 35 /\ FStar.Bytes.length b <= 65537}
MiTLS.Extensions.binders MiTLS.Parse.vlbytes2 FStar.Bytes.bytes MiTLS.Extensions.binderListBytes Prims.l_and Prims.b2t Prims.op_GreaterThanOrEqual FStar.Bytes.length Prims.op_LessThanOrEqual
let bindersBytes bs =
  
let b = binderListBytes bs in
Parse.vlbytes2 b