val ecpfListBytes: l:list point_format{length (ecpfListBytes_aux l) < 256} -> Tot bytes
val ecpfListBytes: l:list point_format{length (ecpfListBytes_aux l) < 256} -> Tot bytes
let ecpfListBytes l =
  let al = ecpfListBytes_aux l in
  lemma_repr_bytes_values (length al);
  let bl:bytes = vlbytes 1 al in
  bl
(* 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

let bindersBytes bs =
  let b = binderListBytes bs in
  Parse.vlbytes2 b

let rec parseBinderList_aux (b:bytes) (binders:list binder)
  : Tot (result (list binder)) (decreases (length b)) =
    if length b > 0 then
      if length b >= 5 then
        match vlsplit 1 b with
        | Error z -> error "parseBinderList failed to parse a binder"
        | Correct (x) ->
          let binder, bytes = x in
          if length binder < 32 then error "parseBinderList: binder too short"
            else (assume (length bytes < length b);
                  parseBinderList_aux bytes (binders @ [binder]))
      else error "parseBinderList: too few bytes"
    else Correct binders

let parseBinderList (b:bytes{2 <= length b}) : result binders =
  if length b < 2 then
    error "pskBinderList not enough bytes to read length header"
  else
    match vlparse 2 b with
    | Correct b ->
      begin
      match parseBinderList_aux b [] with
      | Correct bs ->
        let len = List.Tot.length bs in
        if 0 < len && len < 255 then
          Correct bs
        else
          error "none or too many binders"
      | Error z -> Error z
      end
    | Error z -> error "parseBinderList"

(** REMARK: we don't serialize the binders length; we do it when serializing Binders *)
val pskBytes: psk -> bytes
let pskBytes = function
  | ClientPSK ids len ->
    vlbytes2 (pskiListBytes ids)
  | ServerPSK sid ->
    lemma_repr_bytes_values (UInt16.v sid);
    bytes_of_int 2 (UInt16.v sid)

val parsePskIdentity: b:bytes -> result pskIdentity
let parsePskIdentity b =
  if length b < 2 then
    error "not enough bytes to parse the length of the identity field of PskIdentity"
  else
    match vlsplit 2 b with
    | Error z -> error "malformed PskIdentity"
    | Correct (x) ->
      let id, ota = x in
      if length ota = 4 then
        let ota = uint32_of_bytes ota in
        lemma_repr_bytes_values (length id);
        Correct (id, ota)
      else error "malformed PskIdentity"

#reset-options "--admit_smt_queries true"
let rec parsePskIdentities_aux : b:bytes -> list pskIdentity -> Tot (result (list pskIdentity)) (decreases (length b))
  = fun b psks ->
    if length b > 0 then
      if length b >= 2 then
        match vlsplit 2 b with
        | Error z -> error "parsePskIdentities failed to parse id"
        | Correct (x) ->
          let id, bytes = x in
          lemma_repr_bytes_values (length id);
          if length bytes >= 4 then
            let ot, bytes = split bytes 4ul in
            match parsePskIdentity (vlbytes2 id @| ot) with
            | Correct pski -> parsePskIdentities_aux bytes (psks @ [pski])
            | Error z -> Error z
          else error "parsePSKIdentities too few bytes"
      else error "parsePSKIdentities too few bytes"
    else Correct psks
#reset-options

val parsePskIdentities: b:bytes{length b >= 2} -> result (list pskIdentity)
let parsePskIdentities b =
  match vlparse 2 b with
  | Correct b ->
    if length b >= 7 then parsePskIdentities_aux b []
    else error "parsePskIdentities: too short"
  | Error z -> error "parsePskIdentities: failed to parse"

#reset-options "--admit_smt_queries true"
val client_psk_parse : bytes -> result (psk * option binders)
let client_psk_parse b =
  match vlsplit 2 b with
  | Error z -> error "client_psk_parse failed to parse"
  | Correct(ids,binders_bytes) -> (
    // SI: add ids header back.
    match parsePskIdentities (vlbytes2 ids) with
    | Correct ids -> (
    	match parseBinderList binders_bytes with
    	| Correct bl -> Correct (ClientPSK ids (length binders_bytes), Some bl)
    	| Error z -> error "client_psk_parse_binders")
    | Error z -> error "client_psk_parse_ids")
#reset-options

val server_psk_parse : lbytes 2 -> psk
let server_psk_parse b = ServerPSK (UInt16.uint_to_t (int_of_bytes b))

val parse_psk: ext_msg -> bytes -> result (psk * option binders)
let parse_psk mt b =
  match mt with
  | EM_ClientHello -> client_psk_parse b
  | EM_ServerHello ->
    if length b = 2 then Correct (server_psk_parse b, None)
    else error "Invalid format of server PSK"
  | _ -> error "PSK extension cannot appear in this message type"
#reset-options

// 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

val psk_kex_bytes: psk_kex -> Tot (lbytes 1)
let psk_kex_bytes = function
  | PSK_KE -> abyte 0z
  | PSK_DHE_KE -> abyte 1z
let parse_psk_kex: pinverse_t psk_kex_bytes = fun b -> match b.[0ul] with
  | 0z -> Correct PSK_KE
  | 1z -> Correct PSK_DHE_KE
  | _ -> error  "psk_key"

let client_psk_kexes_bytes (ckxs: client_psk_kexes): b:bytes {length b <= 3} =
  let content: b:bytes {length b = 1 || length b = 2} =
    match ckxs with
    | [x] -> psk_kex_bytes x
    | [x;y] -> psk_kex_bytes x @| psk_kex_bytes y in
  lemma_repr_bytes_values (length content);
  vlbytes 1 content

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

#set-options "--admit_smt_queries true"

let parse_client_psk_kexes: pinverse_t client_psk_kexes_bytes = fun b ->
  if b = client_psk_kexes_bytes [PSK_KE] then Correct [PSK_KE] else
  if b = client_psk_kexes_bytes [PSK_DHE_KE] then Correct [PSK_DHE_KE] else
  if b = client_psk_kexes_bytes [PSK_KE; PSK_DHE_KE] then Correct [PSK_KE; PSK_DHE_KE]  else
  if b = client_psk_kexes_bytes [PSK_DHE_KE; PSK_KE] then Correct [PSK_DHE_KE; PSK_KE]
  else error "PSK KEX payload"
  // redundants lists yield an immediate decoding error.
#reset-options

(* EARLY DATA INDICATION *)

val earlyDataIndicationBytes: edi:earlyDataIndication -> Tot bytes
let earlyDataIndicationBytes = function
  | None -> empty_bytes // ClientHello, EncryptedExtensions
  | Some max_early_data_size -> // NewSessionTicket
    FStar.Bytes.bytes_of_int32 max_early_data_size // avoids overflow in QUIC

val parseEarlyDataIndication: bytes -> result earlyDataIndication
let parseEarlyDataIndication data =
  match length data with
  | 0 -> Correct None
  | 4 ->
      let n = int_of_bytes data in
      lemma_repr_bytes_values n;
      assert_norm (pow2 32 == 4294967296);
      Correct (Some (UInt32.uint_to_t n))
  | _ -> error "early data indication"

(* EC POINT FORMATS *)

let rec ecpfListBytes_aux: list point_format -> bytes = function
  | [] -> empty_bytes
  | ECP_UNCOMPRESSED :: r -> 
    let a = abyte 0z in 
    let b = ecpfListBytes_aux r in
    assume (UInt.fits (length a + length b) 32);
    a @| b
  | ECP_UNKNOWN t :: r -> 
    let a = bytes_of_int 1 t in
    let b = ecpfListBytes_aux r in
    assume (UInt.fits (length a + length b) 32);
    a @| 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

    l:
      Prims.list MiTLS.Extensions.point_format
        {FStar.Bytes.length (MiTLS.Extensions.ecpfListBytes_aux l) < 256}
  -> FStar.Bytes.bytes
Prims.list MiTLS.Extensions.point_format Prims.b2t Prims.op_LessThan FStar.Bytes.length MiTLS.Extensions.ecpfListBytes_aux FStar.Bytes.bytes MiTLS.Parse.vlbytes Prims.unit FStar.Bytes.lemma_repr_bytes_values
let ecpfListBytes l =
  
let al = ecpfListBytes_aux l in
lemma_repr_bytes_values (length al);
let bl:bytes = vlbytes 1 al in
bl