val pskiBytes: psk_identifier * PSK.obfuscated_ticket_age -> bytes
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)
(* 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
/
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
_: (MiTLS.TLSConstants.psk_identifier * MiTLS.PSK.obfuscated_ticket_age) -> FStar.Bytes.bytes
FStar.Pervasives.Native.tuple2 MiTLS.TLSConstants.psk_identifier MiTLS.PSK.obfuscated_ticket_age FStar.Bytes.op_At_Bar MiTLS.Parse.vlbytes2 FStar.Bytes.bytes_of_int32 Prims.unit FStar.Bytes.lemma_repr_bytes_values FStar.UInt32.v FStar.Bytes.bytes
let pskiBytes (i, ot) =
  
lemma_repr_bytes_values (UInt32.v ot);
(vlbytes2 i @| bytes_of_int32 ot)