val certificateRequestBytes13: cr13 -> b:lbytes 4{hs_msg_bytes HT_certificate_request b}
val certificateRequestBytes13: cr13 -> b:lbytes 4{hs_msg_bytes HT_certificate_request b}
let certificateRequestBytes13 cr =
  lemma_repr_bytes_values 0;
  messageBytes HT_certificate_request empty_bytes
(* Copyright (C) 2012--2017 Microsoft Research and INRIA *)
(**
Handshake protocol messages
*)
module MiTLS.HandshakeMessages
open MiTLS

open FStar.Seq
open FStar.Bytes
open FStar.Error

open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.Extensions
open MiTLS.TLSInfo
open MiTLS.CommonDH

#reset-options "--admit_smt_queries true"

(* External functions, locally annotated for speed *)
(*
assume val vlsplit: lSize:nat{lSize <= 4}
  -> vlb:bytes{lSize <= length vlb}
  -> Tot (result (b:(bytes * bytes){
                      repr_bytes (length (fst b)) <= lSize
                  /\  Seq.equal vlb (vlbytes lSize (fst b) @| (snd b))}))

assume val split: b:bytes -> n:nat{length b >= n} -> Tot (x:(bytes*bytes){Seq.equal b ((fst x) @| (snd x)) /\ length (fst x) = n})

assume val split2: b:bytes -> n1:nat -> n2:nat{length b >= n1 + n2} -> Tot (x:(lbytes n1 * lbytes n2 * bytes){forall x1. forall x2. forall x3. x = (x1,x2,x3) ==> Seq.equal b (x1 @| x2 @| x3)})
*)

let split2 abc n1 n2 =
  let a, bc = split abc (FStar.UInt32.uint_to_t n1) in
  let b, c = split bc (FStar.UInt32.uint_to_t n2) in
  a, b, c

val lbyte_eq_lemma: a:byte -> b:byte -> Lemma (requires (True)) (ensures (a <> b ==> abyte a <> abyte b))
  [SMTPat (abyte a); SMTPat (abyte b)]
let lbyte_eq_lemma a b = if a <> b then cut (Bytes.get (abyte a) 0ul <> Bytes.get (abyte b) 0ul) else ()

/// Handshake types

let htBytes t =
  let z =
    match t with
    | HT_hello_request        -> 0z
    | HT_client_hello         -> 1z
    | HT_server_hello         -> 2z
    | HT_session_ticket       -> 4z
    | HT_end_of_early_data    -> 5z
    | HT_encrypted_extensions -> 8z
    | HT_certificate          -> 11z
    | HT_server_key_exchange  -> 12z
    | HT_certificate_request  -> 13z
    | HT_server_hello_done    -> 14z
    | HT_certificate_verify   -> 15z
    | HT_client_key_exchange  -> 16z
    | HT_finished             -> 20z
    | HT_key_update           -> 24z
    | HT_message_hash         -> 254z
    in
  abyte z

// #reset-options "--z3rlimit 100"
let htBytes_is_injective ht1 ht2 = ()

let parseHt b =
  match b.[0ul] with
  |  0z -> Correct HT_hello_request
  |  1z -> Correct HT_client_hello
  |  2z -> Correct HT_server_hello
  |  4z -> Correct HT_session_ticket
  |  5z -> Correct HT_end_of_early_data
//  |  6z -> Correct HT_hello_retry_request
  |  8z -> Correct HT_encrypted_extensions
  | 11z -> Correct HT_certificate
  | 12z -> Correct HT_server_key_exchange
  | 13z -> Correct HT_certificate_request
  | 14z -> Correct HT_server_hello_done
  | 15z -> Correct HT_certificate_verify
  | 16z -> Correct HT_client_key_exchange
  //| 17z -> Correct HT_server_configuration
  | 20z -> Correct HT_finished
  | 24z -> Correct HT_key_update
  | 254z -> Correct HT_message_hash
  //| 67z -> Correct HT_next_protocol
  | _   -> fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "")

//#reset-options "--z3rlimit 600 --initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0"
let inverse_ht x = admit ()
let pinverse_ht x = ()

/// Messages

let ch_is_resumption {ch_sessionID = sid} = length sid > 0

/// Post-Handshake Messages

let error s = fatal Decode_error ("Handshake parser: "^s)


/// Handshake message format

let messageBytes ht data =
  let htb = htBytes ht in
  let vldata = vlbytes 3 data in
  htb @| vldata

let messageBytes_is_injective_strong ht1 data1 s1 ht2 data2 s2 = admit()
  //TODO bytes NS 09/27
  // if messageBytes ht1 data1 @| s1 = messageBytes ht2 data2 @| s2 then
  //   begin
  //     assert(Bytes.equal (messageBytes ht1 data1 @| s1) (messageBytes ht2 data2 @| s2));
  //     append_assoc (htBytes ht1) (vlbytes 3 data1) s1;
  //     append_assoc (htBytes ht2) (vlbytes 3 data2) s2;
  //     lemma_append_inj (htBytes ht1) (vlbytes 3 data1 @| s1) (htBytes ht2) (vlbytes 3 data2 @| s2);
  //     lemma_vlbytes_inj_strong 3 data1 s1 data2 s2
  //   end
  // else ()

#reset-options "--admit_smt_queries true"
let messageBytes_is_injective ht1 data1 ht2 data2 =
  messageBytes_is_injective_strong ht1 data1 empty_bytes ht2 data2 empty_bytes

(*
 Somewhat inefficient implementation:
 - Repeatedly parse the first 4 bytes of the incoming buffer until we have a complete message;
 - Then remove that message from the incoming buffer.
*)
let parseMessage buf =
  if length buf < 4 then
    Correct None // not enough data to start parsing
  else
    let hstypeb,rem = split_ buf 1 in
    match parseHt hstypeb with
    | Error z -> Error z
    | Correct ht ->
      match vlsplit 3 rem with
      | Error z -> Correct None // not enough payload, try next time
      | Correct(x) ->
        let payload,rem' = x in
        //assert (Bytes.equal buf (htBytes ht @| rem));
        //assert (Bytes.equal rem (vlbytes 3 payload @| rem'));
        let to_log = messageBytes ht payload in
        Correct (Some (| rem', ht, payload, to_log |))

#reset-options "--admit_smt_queries true"
(** A.4.1 Hello Messages *)
//#reset-options
val list_valid_to_valid_list: l:valid_cipher_suites -> Tot (l':list (c:cipherSuite{validCipherSuite c}){List.Tot.length l == List.Tot.length l'})
let rec list_valid_to_valid_list l =
  match l with
  | hd::tl -> hd::(list_valid_to_valid_list tl)
  | [] -> []

val valid_list_to_list_valid: l':list (c:cipherSuite{validCipherSuite c}) -> Tot (l:valid_cipher_suites{List.Tot.length l == List.Tot.length l'})
let rec valid_list_to_list_valid l =
  assume false;
  match l with
  | hd::tl -> hd::(valid_list_to_list_valid tl)
  | [] -> []
//#reset-options "--z3rlimit 600 --initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0"

val messageBytes_extra:
  ht:handshakeType ->
  data:bytes ->
  extra:nat{ repr_bytes (length data + extra) <= 3 } ->
  lbytes (4 + length data)
let messageBytes_extra ht data extra =
  let htb = htBytes ht in
  let vldata = vlbytes_trunc 3 data extra in
  htb @| vldata

let messageBytes_extra_injective
  (ht1: handshakeType)
  (data1: bytes)
  (extra1:nat{ repr_bytes (length data1 + extra1) <= 3 } )
  (s1: bytes)
  (ht2: handshakeType)
  (data2: bytes)
  (extra2:nat{ repr_bytes (length data2 + extra2) <= 3 } )
  (s2: bytes)
: Lemma
  (requires (Bytes.equal (messageBytes_extra ht1 data1 extra1 @| s1) (messageBytes_extra ht2 data2 extra2 @| s2)))
  (ensures (ht1 == ht2 /\ length data1 + extra1 == length data2 + extra2 /\ data1 @| s1 == data2 @| s2))
= let hb1 = htBytes ht1 in
  let v1 = vlbytes_trunc 3 data1 extra1 in
  let hb2 = htBytes ht2 in
  let v2 = vlbytes_trunc 3 data2 extra2 in
  //TODO bytes NS 09/27
  // append_assoc hb1 v1 s1;
  // append_assoc hb2 v2 s2;
  // lemma_append_inj hb1 (v1 @| s1) hb2 (v2 @| s2);
  vlbytes_trunc_injective 3 data1 extra1 s1 data2 extra2 s2

// TODO: replace with the corresponding clientHello serializer generated by QD
let cipherSuitesVLBytes (l: list cipherSuiteName { List.Tot.length l < 256 } ) : Tot (b: bytes { length b <= 65536 } ) =
  LowParse.SLow.serialize32_vlarray 2 65534 #_ #_ #_ #Parsers.CipherSuite.cipherSuite_serializer Parsers.CipherSuite.cipherSuite_serializer32 1 255 () l

let clientHelloBytes ch =
  //17-04-26 this will complicate injectivity, now conditional on an extension.
  let legacyVersion = minPV TLS_1p2 ch.ch_protocol_version in
  let verB = versionBytes legacyVersion in
  lemma_repr_bytes_values (length ch.ch_sessionID);
  let sidB = vlbytes 1 ch.ch_sessionID in
  let csB:bytes = cipherSuitesVLBytes ch.ch_cipher_suites in
  lemma_repr_bytes_values (List.Tot.length ch.ch_compressions);
  (* let cmB = match ch.ch_compressions with *)
  (*   | [] -> empty_bytes  *)
  (*   | cl -> vlbytes 1 (compressionMethodsBytes cl) in *)
  let cmB = vlbytes 1 (compressionMethodsBytes ch.ch_compressions) in
  let extB =
    match ch.ch_extensions with
    | Some ext ->
      assume (repr_bytes (length (extensionListBytes ext)) <= 2 /\ length (Extensions.extensionListBytes ext) + bindersLen ext < 65536); // TODO: FIXME
      extensionsBytes ext
    | None -> empty_bytes in
  let data = verB @| (ch.ch_client_random @| (sidB @| (csB @| (cmB @| extB)))) in
  let binders_len = bindersLen_of_ch ch in
  lemma_repr_bytes_values (length data + binders_len);
  let b = messageBytes_extra HT_client_hello data binders_len in
  assume (FStar.Bytes.length b >= 41 /\ hs_msg_bytes HT_client_hello b); // TODO: FIXME
  b

let versionBytes_is_injective pv1 pv2 =
  cut (pv1 <> pv2 ==> (Bytes.get (versionBytes pv1) 0ul <> Bytes.get (versionBytes pv2) 0ul
                   \/ Bytes.get (versionBytes pv1) 1ul <> Bytes.get (versionBytes pv2) 1ul))

(* JK: additional conditions are required on the size of the extensions after serialization *)
//val optionExtensionsBytes: exts:option (ce:list extension{List.Tot.length ce < 256}) -> Tot (b:bytes{length b <= 2 + 65535})
let optionExtensionsBytes exts =
  match exts with
  | Some ext ->
    assume (repr_bytes (length (extensionListBytes ext)) <= 2 /\ length (Extensions.extensionListBytes ext) + bindersLen ext < 65536); // TODO: FIXME
    extensionsBytes ext
  | None -> empty_bytes

//#reset-options
val list_valid_to_valid_list_lemma: cs1:valid_cipher_suites{List.Tot.length cs1 < 256} ->
  cs2:valid_cipher_suites{List.Tot.length cs2 < 256} ->
  Lemma (requires True)
  (ensures (list_valid_to_valid_list cs1 == list_valid_to_valid_list cs2 ==> cs1 == cs2))
let rec list_valid_to_valid_list_lemma cs1 cs2 =
  match cs1, cs2 with
  | [], [] -> ()
  | hd::tl, hd'::tl' -> list_valid_to_valid_list_lemma tl tl'
  | _ -> ()

val compressionMethodsBytes_is_injective: l1:list compression -> l2:list compression ->
  Lemma (requires True)
  (ensures (Bytes.equal (compressionMethodsBytes l1) (compressionMethodsBytes l2) ==> l1 = l2))
let rec compressionMethodsBytes_is_injective l1 l2 =
  match l1, l2 with
  | [], [] -> ()
  | hd::tl, hd'::tl' ->
    if compressionMethodsBytes l1 = compressionMethodsBytes l2 then (
      compressionMethodsBytes_is_injective tl tl';
      //lemma_append_inj (compressionBytes hd) (compressionMethodsBytes tl) (compressionBytes hd') (compressionMethodsBytes tl');   //TODO bytes NS 09/27
      assert (compressionBytes hd = compressionBytes hd' ==> hd = hd'))
  | _ -> ()

val optionExtensionsBytes_is_injective: ext1:option (ce:list extension{List.Tot.length ce < 256}) ->
  ext2:option (ce2:list extension{List.Tot.length ce2 < 256}) ->
  Lemma (requires True)
  (ensures (Bytes.equal (optionExtensionsBytes ext1) (optionExtensionsBytes ext2) ==> ext1 == ext2))
let optionExtensionsBytes_is_injective ext1 ext2 =
  if optionExtensionsBytes ext1 = optionExtensionsBytes ext2
  then begin
    (* JK: TODO: make the assumes part of the specifications *)
    assume (Some? ext1 ==> (let (Some e1) = ext1 in (repr_bytes (length (extensionListBytes e1)) <= 2 /\ length (Extensions.extensionListBytes e1) + bindersLen e1 < 65536))); // TODO: FIXME
    assume (Some? ext2 ==> (let (Some e2) = ext2 in (repr_bytes (length (extensionListBytes e2)) <= 2 /\ length (Extensions.extensionListBytes e2) + bindersLen e2 < 65536))); // TODO: FIXME
    match ext1, ext2 with
    | Some e1, Some e2 ->
      extensionsBytes_is_injective e1 e2
    | _ -> ()
  end else ()

let clientHelloBytes_is_injective_strong msg1 s1 msg2 s2 =
  if clientHelloBytes msg1 @| s1 = clientHelloBytes msg2 @| s2 then begin
    let legacyVersion1 = minPV TLS_1p2 msg1.ch_protocol_version in
    let verB1 = versionBytes legacyVersion1 in
    lemma_repr_bytes_values (length msg1.ch_sessionID);
    let sidB1 = vlbytes 1 msg1.ch_sessionID in
    let csB1 : bytes = cipherSuitesVLBytes msg1.ch_cipher_suites in
    lemma_repr_bytes_values (List.Tot.length msg1.ch_compressions);
    let cmb1 = compressionMethodsBytes msg1.ch_compressions in
    let cmB1 = vlbytes 1 cmb1 in
    let extB1 = match msg1.ch_extensions with
    | Some ext ->
      assume (repr_bytes (length (extensionListBytes ext)) <= 2 /\ length (Extensions.extensionListBytes ext) + bindersLen ext < 65536); // TODO: FIXME
      extensionsBytes ext
    | None -> empty_bytes
    in
    let tail3_1 = cmB1 @| extB1 in
    let tail4_1 = csB1 @| tail3_1 in
    let tail5_1 = sidB1 @| tail4_1 in
    let tail6_1 = msg1.ch_client_random @| tail5_1 in
    let data1 = verB1 @| tail6_1 in
    let binders_len1 = bindersLen_of_ch msg1 in
    lemma_repr_bytes_values (length data1 + binders_len1);
    assert (clientHelloBytes msg1 == messageBytes_extra HT_client_hello data1 binders_len1);
    let legacyVersion2 = minPV TLS_1p2 msg2.ch_protocol_version in
    let verB2 = versionBytes legacyVersion2 in
    lemma_repr_bytes_values (length msg2.ch_sessionID);
    let sidB2 = vlbytes 1 msg2.ch_sessionID in
    let csB2 : bytes = cipherSuitesVLBytes msg2.ch_cipher_suites in
    lemma_repr_bytes_values (List.Tot.length msg2.ch_compressions);
    let cmb2 = compressionMethodsBytes msg2.ch_compressions in
    let cmB2 = vlbytes 1 cmb2 in
    let extB2 = match msg2.ch_extensions with
    | Some ext ->
      assume (repr_bytes (length (extensionListBytes ext)) <= 2 /\ length (Extensions.extensionListBytes ext) + bindersLen ext < 65536); // TODO: FIXME
      extensionsBytes ext
    | None -> empty_bytes
    in
    let tail3_2 = cmB2 @| extB2 in
    let tail4_2 = csB2 @| tail3_2 in
    let tail5_2 = sidB2 @| tail4_2 in
    let tail6_2 = msg2.ch_client_random @| tail5_2 in
    let data2 = verB2 @| tail6_2 in
    let binders_len2 = bindersLen_of_ch msg2 in
    lemma_repr_bytes_values (length data2 + binders_len2);
    assert (clientHelloBytes msg2 == messageBytes_extra HT_client_hello data2 binders_len2);
    messageBytes_extra_injective HT_client_hello data1 binders_len1 s1 HT_client_hello data2 binders_len2 s2;
    //TODO bytes NS 09/27
    // append_assoc verB1 tail6_1 s1;
    // append_assoc verB2 tail6_2 s2;
    // lemma_append_inj verB1 (tail6_1 @| s1) verB2 (tail6_2 @| s2);
    versionBytes_is_injective legacyVersion1 legacyVersion2;
    let f
      ()
    : Lemma (msg1.ch_protocol_version == msg2.ch_protocol_version)
    = assume (~ (msg1.ch_protocol_version == TLS_1p3)); // TODO: FIXME (see comment on ch_protocol_version: should this be formalized as a refinement constraint there?)
      assume (~ (msg2.ch_protocol_version == TLS_1p3)); // TODO: FIXME
      // (those assumes are enclosed in a function so they do not leak into the rest of the proof)
      ()
    in
    f ();
    //TODO bytes NS 09/27
    // append_assoc msg1.ch_client_random tail5_1 s1;
    // append_assoc msg2.ch_client_random tail5_2 s2;
    // lemma_append_inj msg1.ch_client_random (tail5_1 @| s1) msg2.ch_client_random (tail5_2 @| s2);
    // append_assoc sidB1 tail4_1 s1;
    // append_assoc sidB2 tail4_2 s2;
    lemma_vlbytes_inj_strong 1 msg1.ch_sessionID (tail4_1 @| s1) msg2.ch_sessionID (tail4_2 @| s2);
    //TODO bytes NS 09/27
    // append_assoc csB1 tail3_1 s1;
    // append_assoc csB2 tail3_2 s2;
//    lemma_vlbytes_inj_strong 2 csb1 (tail3_1 @| s1) csb2 (tail3_2 @| s2);
    let _ : squash (msg1.ch_cipher_suites == msg2.ch_cipher_suites) =
      assume (msg1.ch_cipher_suites == msg2.ch_cipher_suites) // cipherSuitesBytes_is_injective msg1.ch_cipher_suites msg2.ch_cipher_suites
    in
    //TODO bytes NS 09/27
    // append_assoc cmB1 extB1 s1;
    // append_assoc cmB2 extB2 s2;
    lemma_vlbytes_inj_strong 1 cmb1 (extB1 @| s1) cmb2 (extB2 @| s2);
    let _ : squash (msg1.ch_compressions == msg2.ch_compressions) =
      compressionMethodsBytes_is_injective msg1.ch_compressions msg2.ch_compressions
    in
    assert (length extB1 + binders_len1 == length extB2 + binders_len2);
    match msg1.ch_extensions with
    | None ->
      assert (msg2.ch_extensions == None)
      //TODO bytes NS 09/27
      // lemma_append_inj extB1 s1 extB2 s2
    | Some e1 ->
      let (Some e2) = msg2.ch_extensions in
      assume (repr_bytes (length (extensionListBytes e1)) <= 2 /\ length (Extensions.extensionListBytes e1) + bindersLen e1 < 65536); // TODO: FIXME
      assume (repr_bytes (length (extensionListBytes e2)) <= 2 /\ length (Extensions.extensionListBytes e2) + bindersLen e2 < 65536); // TODO: FIXME
      extensionsBytes_is_injective_strong e1 s1 e2 s2
  end else ()

val clientHelloBytes_is_injective: msg1:ch -> msg2:ch ->
  Lemma (requires True)
  (ensures (Bytes.equal (clientHelloBytes msg1) (clientHelloBytes msg2) ==> (msg1 == msg2)))
  [SMTPat (clientHelloBytes msg1); SMTPat (clientHelloBytes msg2)]
let clientHelloBytes_is_injective msg1 msg2 =
  clientHelloBytes_is_injective_strong msg1 empty_bytes msg2 empty_bytes

(* JK: to work around a subtyping difficulty in parseClientHello *)
val coercion_helper: o:option (list extension){Some? o ==>  List.Tot.length (Some?.v o) < 256}
   -> Tot (option (l:list extension{List.Tot.length l < 256}))
let coercion_helper e =
  match e with
  | None -> None
  | Some li -> cut (List.Tot.length li < 256); Some li

let parseVLCipherSuites (b: bytes) : Tot (option ((l: list cipherSuiteName { 1 <= List.Tot.length l /\ List.Tot.length l <= 255 } ) * bytes)) =
  match LowParse.SLow.parse32_vlarray 2 2ul 65534 65534ul Parsers.CipherSuite.cipherSuite_serializer Parsers.CipherSuite.cipherSuite_parser32 1 255 () b with
  | Some (l, consumed) ->
    let rem = FStar.Bytes.slice b consumed (FStar.Bytes.len b) in
    Some (l, rem)
  | None -> None

let parseClientHello data =
  if length data < 35 then error "ClientHello is too short" else
  let clVerBytes,cr_data = split data 2ul in
  let cr, data = split cr_data 32ul in
  match parseVersion clVerBytes with
  | Error z -> Error z
  | Correct cv ->
    match vlsplit 1 data with
    | Error z -> error "sid length"
    | Correct (x) ->
      let sid,data = x in
      if length sid > 32 || length data < 2 then error "sid" else (
      match parseVLCipherSuites data with
      | None -> error "ciphersuites"
      | Some (clientCipherSuites, data) ->
          (* ADL More relaxed parsing for old ClientHello messages with *)
          (* no compression and no extensions *)
          let compExts =
            if length data < 1 || List.Tot.length clientCipherSuites >= 256 then error "ciphersuites length"
            else (match vlsplit 1 data with
            | Error z -> fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "Failed to parse compression bytes")
            | Correct (x) ->
              let cmBytes, extensions = x in
              let cm = parseCompressions cmBytes in
               (match parseOptExtensions EM_ClientHello extensions with
                | Error z -> Error z
                | Correct (x) ->
                    let exts, obinders = x in
                    if (match exts with
                        | None -> true
                        | Some l -> List.Tot.length l < 256)
                        && List.Tot.length cm < 256 &&  List.Tot.length cm > 0
                    then Correct (cm, (coercion_helper exts, obinders))
                    else error "bad extension lengths"))
            in
            ( match compExts with
              | Error z -> Error z
              | Correct (cm, (exts, obinders)) -> (
                cut (List.Tot.length clientCipherSuites < 256);
                let cCS = clientCipherSuites in
                Correct ({
                  ch_protocol_version = cv;
                  ch_client_random = cr;
                  ch_sessionID = sid;
                  ch_cipher_suites = cCS;
                  ch_compressions = cm;
                  ch_extensions = exts; }, obinders))))

#reset-options "--admit_smt_queries true"
let serverHelloBytes sh =
  // signalling the current draft version
  let pv = match sh.sh_protocol_version with | TLS_1p3 -> TLS_1p2 | v -> v in
  let verB = versionBytes pv in
  lemma_repr_bytes_values (length sh.sh_sessionID);
  let sidB = vlbytes 1 sh.sh_sessionID in
  let csB = cipherSuiteNameBytes sh.sh_cipher_suite in
  let cmB = compressionBytes sh.sh_compression in
  let extB =
    match sh.sh_extensions with
    | Some ext -> extensionsBytes ext
    | None -> empty_bytes in  // JK: in TLS1.3 case should be vlbytes 2 empty_bytes
  let data:bytes = verB @| (sh.sh_server_random @| (sidB @| (csB @| (cmB @| extB)))) in
  lemma_repr_bytes_values (length data);
  messageBytes HT_server_hello data

//#reset-options "--z3rlimit 50"

// 18-02-15 disabling verification attemps (150', 44 errors) till the new parsers.
let serverHelloBytes_is_injective msg1 msg2 =
  if serverHelloBytes msg1 = serverHelloBytes msg2 then
  begin
    let verB1 = versionBytes msg1.sh_protocol_version in
    lemma_repr_bytes_values (length msg1.sh_sessionID);
    let sidB1 = vlbytes 1 msg1.sh_sessionID in
      let csB1 = cipherSuiteNameBytes msg1.sh_cipher_suite in
      let cmB1 =  compressionBytes msg1.sh_compression in
      let extB1 = match msg1.sh_extensions with
      | Some ext -> extensionsBytes ext
      | None -> empty_bytes in
      let data1:bytes = match msg1.sh_protocol_version with
      | TLS_1p3 -> verB1 @| (msg1.sh_server_random @| (csB1 @| extB1))
      | _       -> verB1 @| (msg1.sh_server_random @| (sidB1 @| (csB1 @| (cmB1 @| extB1)))) in
      lemma_repr_bytes_values (length data1);
      let verB2 = versionBytes msg2.sh_protocol_version in
      lemma_repr_bytes_values (length msg2.sh_sessionID);
      let sidB2 = vlbytes 1 msg2.sh_sessionID in
      let csB2 = cipherSuiteNameBytes msg2.sh_cipher_suite in
      let cmB2 = compressionBytes msg2.sh_compression in
      let extB2:bytes = match msg2.sh_extensions with
      | Some ext -> extensionsBytes ext
      | None -> empty_bytes in
      let data2:bytes = match msg2.sh_protocol_version with
      | TLS_1p3 -> verB2 @| (msg2.sh_server_random @| (csB2 @| extB2))
      | _       -> verB2 @| (msg2.sh_server_random @| (sidB2 @| (csB2 @| (cmB2 @| extB2)))) in
      lemma_repr_bytes_values (length data2);
      messageBytes_is_injective HT_server_hello data1 HT_server_hello data2;
      cut(Bytes.equal data1 data2);
      let s1 = split data1 2ul in
      let s2 = split data2 2ul in
      cut(Bytes.equal verB1 (fst s1) /\ Bytes.equal verB2 (fst s2));
      //TODO bytes NS 09/27
      //lemma_append_inj verB1 (snd s1) verB2 (snd s2);
      versionBytes_is_injective msg1.sh_protocol_version msg2.sh_protocol_version;
      cut(msg1.sh_protocol_version = msg2.sh_protocol_version);
      if msg1.sh_protocol_version = TLS_1p3 then (
  cut (Bytes.equal (snd s1) (snd s2));
  cut (Bytes.equal (snd s1) (msg1.sh_server_random @| (csB1 @| extB1)));
  cut (Bytes.equal (snd s2) (msg2.sh_server_random @| (csB2 @| extB2)));
  cut (length msg1.sh_server_random = length msg2.sh_server_random);
  //TODO bytes NS 09/27
  //lemma_append_inj msg1.sh_server_random (csB1 @| extB1) msg2.sh_server_random (csB2 @| extB2);
  assert(msg1.sh_server_random = msg2.sh_server_random);
  let l1 = (csB1 @| extB1) in
  let l2 = (csB2 @| extB2) in
  cut(length csB1 >= 2 /\ length csB2 >= 2);
  cut(Bytes.get csB1 0ul = Bytes.get l1 0ul /\ Bytes.get csB1 1ul = Bytes.get l1 1ul);
  cut(Bytes.get csB2 0ul = Bytes.get l2 0ul /\ Bytes.get csB2 1ul = Bytes.get l2 1ul);
  cut(length (cipherSuiteNameBytes msg1.sh_cipher_suite) = length (cipherSuiteNameBytes msg2.sh_cipher_suite));
  //TODO bytes NS 09/27
  //lemma_append_inj csB1 extB1 csB2 extB2;
//  cipherSuiteBytes_is_injective msg1.sh_cipher_suite msg2.sh_cipher_suite;
  optionExtensionsBytes_is_injective msg1.sh_extensions msg2.sh_extensions;
  ())
      else (
  cut (Bytes.equal (snd s1) (snd s2));
  cut (Bytes.equal (snd s1) (msg1.sh_server_random @| (sidB1 @| (csB1 @| (cmB1 @| extB1)))));
  cut (Bytes.equal (snd s2) (msg2.sh_server_random @| (sidB2 @| (csB2 @| (cmB2 @| extB2)))));
  cut (length msg1.sh_server_random = length msg2.sh_server_random);
  //TODO bytes NS 09/27
  // lemma_append_inj msg1.sh_server_random (sidB1 @| (csB1 @| (cmB1 @| extB1)))
  //      msg2.sh_server_random (sidB2 @| (csB2 @| (cmB2 @| extB2)));
  let l1 = (sidB1 @| (csB1 @| (cmB1 @| extB1))) in
  let l2 = (sidB2 @| (csB2 @| (cmB2 @| extB2))) in
  cut(length sidB1 >= 1);
  cut(length sidB2 >= 1);
  cut(Bytes.equal l1 l2);
  cut(Bytes.get sidB1 0ul = Bytes.get l1 0ul /\ Bytes.get sidB2 0ul = Bytes.get l2 0ul);
  cut(Bytes.get sidB1 0ul = Bytes.get sidB2 0ul);
  vlbytes_length_lemma 1 (msg1.sh_sessionID) (msg2.sh_sessionID);
  cut (length sidB1 = length sidB2);
  //TODO bytes NS 09/27
  //lemma_append_inj sidB1 (csB1 @| (cmB1 @| extB1)) sidB2 (csB2 @| (cmB2 @| extB2));
  cut(length csB1 >= 2 /\ length csB2 >= 2);
  let l1 = (csB1 @| (cmB1 @| extB1)) in
  let l2 = (csB2 @| (cmB2 @| extB2)) in
  cut(Bytes.get csB1 0ul = Bytes.get l1 0ul /\ Bytes.get csB1 1ul = Bytes.get l1 1ul);
  cut(Bytes.get csB2 0ul = Bytes.get l2 0ul /\ Bytes.get csB2 1ul = Bytes.get l2 1ul);
  cut(length (cipherSuiteNameBytes msg1.sh_cipher_suite) = length (cipherSuiteNameBytes msg2.sh_cipher_suite));
  //TODO bytes NS 09/27
  //lemma_append_inj csB1 (cmB1 @| extB1) csB2 (cmB2 @| extB2);
  cut (length cmB1 = length cmB2);
  //TODO bytes NS 09/27
  //lemma_append_inj cmB1 extB1 cmB2 extB2;
//  cipherSuiteBytes_is_injective msg1.sh_cipher_suite msg2.sh_cipher_suite;
  optionExtensionsBytes_is_injective msg1.sh_extensions msg2.sh_extensions;
  cut(msg1.sh_protocol_version = msg2.sh_protocol_version);
  cut(msg1.sh_server_random = msg2.sh_server_random);
  cut(Bytes.equal sidB1 sidB2);
  lemma_vlbytes_inj 1 (msg1.sh_sessionID) (msg2.sh_sessionID);
  ()
      )
    end

// TR: the following proof successfully verifies
let serverHelloBytes_is_injective_strong msg1 s1 msg2 s2 =
  let b1 = serverHelloBytes msg1 in
  let b1' = snd (split b1 4ul) in
  let b2 = serverHelloBytes msg2 in
  let b2' = snd (split b2 4ul) in
  messageBytes_is_injective_strong HT_server_hello b1' s1 HT_server_hello b2' s2;
  serverHelloBytes_is_injective msg1 msg2

#reset-options "--admit_smt_queries true"
let parseServerHello data =
  if length data < 34 then
    fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "")
  else
    let (serverVerBytes, serverRandomBytes, data) = split2 data 2 32 in
    match parseVersion serverVerBytes with
    | Error z -> Error z
    | Correct serverVer ->
     if length data >= 1 then
       match vlsplit 1 data with
       | Error z -> Error z
       | Correct (x) ->
         let sid,data = x in
         if length sid <= 32 then
           if length data >= 3 then
             let (csBytes,cmBytes,data) = split2 data 2 1 in
             (let cs = parseCipherSuiteName csBytes in
                 let cm = parseCompression cmBytes in
                 (match cm with
                   | Unknown_compressionMethod _ ->
                     fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "server selected a compression mode")
                   | NullCompression ->
                     let em = // FIXME what can we do about this horrible, atrocious hack?
                       if bytes_of_hex "cf21ad74e59a6111be1d8c021e65b891c2a211167abb8c5e079e09e2c8a8339c" = serverRandomBytes
                       then EM_HelloRetryRequest else EM_ServerHello in
                      (match parseOptExtensions em data with
                       | Error z -> Error z
                       | Correct (x) ->
                         let exts,obinders = x in
                         if (match exts with
                             | None -> true
                             | Some l -> List.Tot.length l < 256)
                         then
                           let exts = coercion_helper exts in
                           correct ({
                             sh_protocol_version = serverVer;
                             sh_server_random = serverRandomBytes;
                             sh_sessionID = sid;
                             sh_cipher_suite = cs;
                             sh_compression = NullCompression;
                             sh_extensions = exts})
                         else fatal Decode_error (perror __SOURCE_FILE__ __LINE__ ""))))
           else fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "")
         else fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "")
     else fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "")

let helloRequestBytes =
  lemma_repr_bytes_values 0;
  messageBytes HT_hello_request empty_bytes

let ccsBytes = abyte 1z

let serverHelloDoneBytes =
  lemma_repr_bytes_values 0;
  messageBytes HT_server_hello_done empty_bytes

(** A.4.2 Server Authentication and Key Exchange Messages *)

let valid_crt = c:crt {length (Cert.certificateListBytes c.crt_chain) < 16777212}
let valid_crt13 = c:crt13 {length (Cert.certificateListBytes13 c.crt_chain13) < 16777212}

val certificateBytes: valid_crt -> b:bytes{hs_msg_bytes HT_certificate b}
let certificateBytes crt =
  let cb = Cert.certificateListBytes crt.crt_chain in
  lemma_repr_bytes_values (length cb);
  lemma_repr_bytes_values (length (vlbytes 3 cb));
  messageBytes HT_certificate (vlbytes 3 cb)

val certificateBytes13: valid_crt13 -> b:bytes{hs_msg_bytes HT_certificate b}
let certificateBytes13 crt =
  let cb = Cert.certificateListBytes13 crt.crt_chain13 in
  lemma_repr_bytes_values (length empty_bytes);
  cut (length ((vlbytes 1 empty_bytes) @| (vlbytes 3 cb)) < 16777216);
  lemma_repr_bytes_values (length ((vlbytes 1 empty_bytes) @| vlbytes 3 cb));
  messageBytes HT_certificate ((vlbytes 1 empty_bytes) @| (vlbytes 3 cb))

val certificateBytes_is_injective: c1:valid_crt -> c2:valid_crt ->
  Lemma (Bytes.equal (certificateBytes c1) (certificateBytes c2) ==> c1 = c2)
let certificateBytes_is_injective c1 c2 =
  if certificateBytes c1 = certificateBytes c2  then (
    let cb1 = Cert.certificateListBytes c1.crt_chain in
    let cb2 = Cert.certificateListBytes c2.crt_chain in
    lemma_repr_bytes_values (length cb1);
    lemma_repr_bytes_values (length cb2);
    lemma_vlbytes_len 3 cb1;
    lemma_vlbytes_len 3 cb2;
    cut (length (vlbytes 3 cb1) < 16777216);
    cut (length (vlbytes 3 cb2) < 16777216);
    lemma_repr_bytes_values (length (vlbytes 3 cb1));
    lemma_repr_bytes_values (length (vlbytes 3 cb2));
    cut (Bytes.equal (certificateBytes c1) (messageBytes HT_certificate ((vlbytes 3 cb1))));
    cut (Bytes.equal (certificateBytes c2) (messageBytes HT_certificate ((vlbytes 3 cb2))));
    messageBytes_is_injective HT_certificate (vlbytes 3 cb1)
            HT_certificate (vlbytes 3 cb2);
    lemma_vlbytes_inj 3 cb1 cb2;
    Cert.certificateListBytes_is_injective c1.crt_chain c2.crt_chain;
    ()
  ) else ()

val certificateBytes13_is_injective: c1:valid_crt13 -> c2:valid_crt13 ->
  Lemma (Bytes.equal (certificateBytes13 c1) (certificateBytes13 c2) ==> c1 = c2)
let certificateBytes13_is_injective c1 c2 =
  if certificateBytes13 c1 = certificateBytes13 c2  then (
    let cb1 = Cert.certificateListBytes13 c1.crt_chain13 in
    let cb2 = Cert.certificateListBytes13 c2.crt_chain13 in
    lemma_repr_bytes_values (length cb1);
    lemma_repr_bytes_values (length cb2);
    lemma_repr_bytes_values (length empty_bytes);
    lemma_vlbytes_len 1 empty_bytes;
    lemma_vlbytes_len 3 cb1;
    lemma_vlbytes_len 3 cb2;
    cut (length ((vlbytes 1 empty_bytes) @| (vlbytes 3 cb1)) < 16777216);
    cut (length ((vlbytes 1 empty_bytes) @| (vlbytes 3 cb2)) < 16777216);
    lemma_repr_bytes_values (length ((vlbytes 1 empty_bytes) @| (vlbytes 3 cb1)));
    lemma_repr_bytes_values (length ((vlbytes 1 empty_bytes) @| (vlbytes 3 cb2)));
    cut (Bytes.equal (certificateBytes13 c1) (messageBytes HT_certificate ((vlbytes 1 empty_bytes) @| (vlbytes 3 cb1))));
    cut (Bytes.equal (certificateBytes13 c2) (messageBytes HT_certificate ((vlbytes 1 empty_bytes) @| (vlbytes 3 cb2))));
    messageBytes_is_injective HT_certificate ((vlbytes 1 empty_bytes) @| vlbytes 3 cb1)
            HT_certificate ((vlbytes 1 empty_bytes) @| vlbytes 3 cb2);
    //TODO bytes NS 09/27
    //lemma_append_inj (vlbytes 1 empty_bytes) (vlbytes 3 cb1) (vlbytes 1 empty_bytes) (vlbytes 3 cb2);
    lemma_vlbytes_inj 3 cb1 cb2;
    Cert.certificateListBytes13_is_injective c1.crt_chain13 c2.crt_chain13;
    ()
  ) else ()

// SZ: I think this should be
// val parseCertificate: pv:protocolVersion -> data:bytes{3 <= length data /\ repr_bytes (length data - 3) <= 3}
//  -> Tot (result (r:crt{Bytes.equal (certificateBytes r) (messageBytes HT_certificate data)}))
(* val parseCertificate: pv:protocolVersion -> data:bytes{repr_bytes (length data) <= 3}  *)
(*   -> Tot (result (r:valid_crt{Bytes.equal (certificateBytes pv r) (messageBytes HT_certificate data)})) *)
val parseCertificate: data:bytes{repr_bytes (length data) <= 3} -> Tot (result valid_crt)
let parseCertificate data =
  if length data < 3 then error "not enough certificate-list length bytes" else
  match vlparse 3 data with
  | Error (x,y) -> fatal Bad_certificate y
  | Correct certList -> (
    match Cert.parseCertificateList certList with
    | Error (x,y) -> fatal Bad_certificate y
    | Correct l ->
      if length certList >= 16777212 then error "certificate list is too large" else
      ( Cert.lemma_parseCertificateList_length certList;
        Correct ({crt_chain = l})))

val parseCertificate13: data:bytes{repr_bytes (length data) <= 3} -> Tot (result valid_crt13)
let parseCertificate13 data =
  if length data < 1 then error "not enough bytes (context)" else
  let hdr, data = split data 1ul in
  if not (hdr = abyte 0z) then error "non-empty context" else
  if length data < 3 then error "not enough bytes (certificate list length)" else (
  match vlparse 3 data with
  | Error (x,y) -> fatal Bad_certificate y
  | Correct certList -> (
    match Cert.parseCertificateList13 certList with
    | Error z -> Error z
    | Correct l ->
      if length certList >= 16777212 then error "certificate list is too large" else
      ( //Cert.lemma_parseCertificateList_length13 certList;
        Correct ({crt_request_context = empty_bytes; crt_chain13 = l}))))

(* JK: TODO: rewrite taking the protocol version as an extra parameter, otherwise not injective *)
val certificateRequestBytes: cr -> b:bytes{hs_msg_bytes HT_certificate_request b}
let certificateRequestBytes cr =
  let ctb = certificateTypeListBytes cr.cr_cert_types in
  lemma_repr_bytes_values (length ctb);
  let ctB = vlbytes 1 ctb in
  let saB =
    match cr.cr_sig_algorithms with
    | None -> empty_bytes
    | Some sigAlgs -> signatureSchemeListBytes sigAlgs // includes length header
  in
  let dnb = distinguishedNameListBytes cr.cr_certificate_authorities in
  lemma_repr_bytes_values (length dnb);
  let dnB = vlbytes 2 dnb in
  let data = ctB @| saB @| dnB in
  lemma_repr_bytes_values (length data);
  messageBytes HT_certificate_request data

val certificateTypeListBytes_is_injective: ctl1:list certType -> ctl2:list certType ->
  Lemma (Bytes.equal (certificateTypeListBytes ctl1) (certificateTypeListBytes ctl2) ==> ctl1 = ctl2)
let rec certificateTypeListBytes_is_injective ctl1 ctl2 =
  match ctl1, ctl2 with
  | [], [] -> ()
  | hd::tl, hd'::tl' ->
    if certificateTypeListBytes ctl1 = certificateTypeListBytes ctl2 then (
      cut (Bytes.equal (certTypeBytes hd @| certificateTypeListBytes tl) (certTypeBytes hd' @| certificateTypeListBytes tl'));
      //TODO bytes NS 09/27
      //lemma_append_inj (certTypeBytes hd) (certificateTypeListBytes tl) (certTypeBytes hd') (certificateTypeListBytes tl');
      cut(hd = hd');
      certificateTypeListBytes_is_injective tl tl'
    )
  | _, _ -> ()

//#reset-options

let lemma_distinguishedNameListBytes_def (n:list dn{Cons? n /\ repr_bytes (length (utf8_encode (Cons?.hd n))) <= 2}) : Lemma
  (distinguishedNameListBytes n = (vlbytes 2 (utf8_encode (Cons?.hd n)) @| distinguishedNameListBytes (Cons?.tl n))) = ()

let lemma_distinguishedNameListBytes_def2 (n:list dn{Nil? n}) : Lemma (distinguishedNameListBytes n = empty_bytes) = ()

(* TODO: port to FStar.Bytes *)
assume val utf8_is_injective: s:string -> s':string ->
  Lemma (requires True)
  (ensures (Bytes.equal (utf8_encode s) (utf8_encode s') ==> s = s'))

val distinguishedNameListBytes_is_injective: n1:list dn -> n2:list dn ->
  Lemma (requires True)
  (ensures (Bytes.equal (distinguishedNameListBytes n1) (distinguishedNameListBytes n2) ==> n1 = n2))
let rec distinguishedNameListBytes_is_injective n1 n2 = admit ()
  //this is very stale now
  //TODO bytes NS 09/27
  // match n1, n2 with
  // | [],[] -> ()
  // | hd::tl, hd'::tl' ->
  //     let payload1 = distinguishedNameListBytes n1 in
  //     let payload2 = distinguishedNameListBytes n2 in
  //     if payload1 = payload2 then (
  // lemma_repr_bytes_values (length (utf8_encode hd'));
  // lemma_repr_bytes_values (length (utf8_encode hd));
  // lemma_distinguishedNameListBytes_def n1;
  // lemma_distinguishedNameListBytes_def n2;
  // //cut (forall b b'. {:pattern (b@|b')} (b@|b') = Seq.append b b'); //TODO bytes NS 09/27 redundant?
  // //Seq.lemma_eq_refl payload1 payload2;
  // cut (Bytes.equal ((vlbytes 2 (utf8_encode hd))  @| (distinguishedNameListBytes tl))
  //                  ((vlbytes 2 (utf8_encode hd')) @| (distinguishedNameListBytes tl')));
  // // cut (Bytes.equal (Bytes.append (vlbytes 2 (utf8_encode hd))  (distinguishedNameListBytes tl))
  // //                  (Bytes.append (vlbytes 2 (utf8_encode hd')) (distinguishedNameListBytes tl')));
  //       cut (Bytes.get (vlbytes 2 (utf8_encode hd)) 0 = Bytes.get payload1 0);
  //       cut (Bytes.get (vlbytes 2 (utf8_encode hd)) 1 = Bytes.get payload1 1);
  //       cut (Bytes.get (vlbytes 2 (utf8_encode hd')) 0 = Bytes.get payload2 0);
  //       cut (Bytes.get (vlbytes 2 (utf8_encode hd')) 1 = Bytes.get payload2 1);
  // cut (Bytes.get payload1 0 = Bytes.get payload2 0);
  //       cut (Bytes.get payload1 1 = Bytes.get payload2 1);
  // vlbytes_length_lemma 2 (utf8_encode hd) (utf8_encode hd');
  // lemma_append_inj (vlbytes 2 (utf8_encode hd)) (distinguishedNameListBytes tl) (vlbytes 2 (utf8_encode hd')) (distinguishedNameListBytes tl');
  // distinguishedNameListBytes_is_injective tl tl';
  // lemma_vlbytes_inj 2 (utf8_encode hd) (utf8_encode hd');
  // utf8_is_injective hd hd'
  //     )
  // | [],hd::tl -> (
  //     lemma_repr_bytes_values (length (utf8 hd));
  //     lemma_distinguishedNameListBytes_def n2;
  //     lemma_distinguishedNameListBytes_def2 n1;
  //     cut (forall b b'. {:pattern (b@|b')} (b@|b') = Seq.append b b');
  //     cut (length (distinguishedNameListBytes n2) >= 2);
  //     cut (length (distinguishedNameListBytes n1) = 0)
  //     )
  // | hd::tl,[] -> (
  //     lemma_repr_bytes_values (length (utf8 hd));
  //     lemma_distinguishedNameListBytes_def n1;
  //     lemma_distinguishedNameListBytes_def2 n2;
  //     cut (forall b b'. {:pattern (b@|b')} (b@|b') = Seq.append b b');
  //     cut (length (distinguishedNameListBytes n1) >= 2);
  //     cut (length (distinguishedNameListBytes n2) = 0)
  //     )

//#set-options "--admit_smt_queries true"

val certificateRequestBytes_is_injective: c1:cr -> c2:cr ->
  Lemma (requires True)
  (ensures (Bytes.equal (certificateRequestBytes c1) (certificateRequestBytes c2) ==> c1 = c2))
let certificateRequestBytes_is_injective c1 c2 =
  admit(); // JK: TODO
  if certificateRequestBytes c1 = certificateRequestBytes c2 then (
    let ctb1 = certificateTypeListBytes c1.cr_cert_types in
    lemma_repr_bytes_values (length ctb1);
    let ctB1 = vlbytes 1 ctb1 in
    let saB1 = admit() in //signatureSchemeListBytes c1.cr_sig_algorithms in
    let dnb1 = distinguishedNameListBytes c1.cr_certificate_authorities in
    lemma_repr_bytes_values (length dnb1);
    let dnB1 = vlbytes 2 dnb1 in
    let data1 = ctB1 @| saB1 @| dnB1 in
    let ctb2 = certificateTypeListBytes c2.cr_cert_types in
    lemma_repr_bytes_values (length ctb2);
    let ctB2 = vlbytes 1 ctb2 in
    let saB2 = admit() in // signatureSchemeListBytes c2.cr_sig_algorithms in
    let dnb2 = distinguishedNameListBytes c2.cr_certificate_authorities in
    lemma_repr_bytes_values (length dnb2);
    let dnB2 = vlbytes 2 dnb2 in
    let data2 = ctB2 @| saB2 @| dnB2 in
    lemma_repr_bytes_values (length data2);
    lemma_repr_bytes_values (length data1);
    messageBytes_is_injective HT_certificate_request data1 HT_certificate_request data2;
    assume (Bytes.equal (slice_ data1 0 1) (slice_ data2 0 1));
    assume (Bytes.equal (slice_ data1 0 1) (slice_ ctB1 0 1));
    assume (Bytes.equal (slice_ data2 0 1) (slice_ ctB2 0 1));
    vlbytes_length_lemma 1 ctb1 ctb2
    //TODO bytes NS 09/27
    //lemma_append_inj ctB1 (saB1 @| dnB1) ctB2 (saB2 @| dnB2)
  )

// TODO split on pv
val parseCertificateRequest: pv:protocolVersion -> data:bytes -> result cr
let parseCertificateRequest pv data =
  if length data >= 1 then
    match vlsplit 1 data with
    | Error z -> Error z
    | Correct (x) ->
      let certTypeListBytes, data = x in
      let certTypeList = parseCertificateTypeList certTypeListBytes in
      let n = List.Tot.length certTypeList in
      if 0 < n && n < 256 then // Redundant to check upper bound
        if length data >= 2 then
          begin
          match pv with
          | TLS_1p2 ->
            begin
            match vlsplit 2 data with
            | Error z -> Error z
            | Correct (x) ->
              let signatureAlgorithmsBytes, data = x in
              begin
              lemma_repr_bytes_values (length signatureAlgorithmsBytes);
              match parseSignatureSchemeList (vlbytes 2 signatureAlgorithmsBytes) with
              | Error z -> Error z
              | Correct sigAlgs ->
                if length data >= 2 then
                  match vlparse 2 data with
                  | Error z -> Error z
                  | Correct certificateAuthoritiesBytes ->
                    begin
                    match parseDistinguishedNameList certificateAuthoritiesBytes [] with
                    | Error z -> Error z
                    | Correct distNamesList ->
                      correct (
                        {cr_cert_types = certTypeList;
                         cr_sig_algorithms = Some sigAlgs;
                         cr_certificate_authorities = distNamesList})
                    end
                else fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "Certificate Request message is too short")
              end
            end
          | _ -> // TLS_1p0, TLS_1p1
            match parseDistinguishedNameList data [] with
            | Error z -> Error z
            | Correct distNamesList ->
              correct (
               {cr_cert_types = certTypeList;
                cr_sig_algorithms = None;
                cr_certificate_authorities = distNamesList})
          end // match pv
        else fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "Certificate Request message is too short")
      else fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "empty certificate_types in Certificate Request")
  else fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "Certificate Request message is too short")

let mk_certificateRequestBytes sign cs version =
  certificateRequestBytes (
    {cr_cert_types = defaultCertTypes sign cs;
     cr_sig_algorithms =
       (match version with
        | TLS_1p2 -> Some (default_signatureScheme version cs)
        | _ -> None);
     cr_certificate_authorities = []})

let parseCertificateRequest13 (body:bytes): result cr13 = error "Certificate requests not yet implemented"

(** A.4.3 Client Authentication and Key Exchange Messages *)

let kex_c_of_dh_key #g kex =
  if CommonDH.is_ec g then
    KEX_C_ECDHE (CommonDH.serialize_raw #g kex)
  else
    KEX_C_DHE (CommonDH.serialize_raw #g kex)

(* JK: TODO: add the kex as an extra parameter, otherwise not injective *)
val clientKeyExchangeBytes: cke -> Tot (b:bytes{hs_msg_bytes HT_client_key_exchange b})
let clientKeyExchangeBytes cke =
  let kexB =
    match cke.cke_kex_c with
    | KEX_C_DHE b -> (
      lemma_repr_bytes_values (length b);
      lemma_vlbytes_len 2 b;
      lemma_repr_bytes_values (length (vlbytes 2 b));
      vlbytes 2 b )
    | KEX_C_ECDHE b -> (
      lemma_repr_bytes_values (length b);
      lemma_vlbytes_len 1 b;
      lemma_repr_bytes_values (length (vlbytes 1 b));
      vlbytes 1 b)
    // | SSL_3p0,KEX_C_RSA(encpms) -> (lemma_repr_bytes_values (length encpms); encpms)
    | KEX_C_RSA(encpms) -> (
      lemma_repr_bytes_values (length encpms);
      lemma_vlbytes_len 2 encpms;
      lemma_repr_bytes_values (length (vlbytes 2 encpms));
      vlbytes 2 encpms )
    | KEX_C_DH -> (
      lemma_repr_bytes_values (length empty_bytes);
      empty_bytes) in
  lemma_repr_bytes_values (length kexB);
  messageBytes HT_client_key_exchange kexB

val clientKeyExchangeBytes_is_injective: cke1:cke -> cke2:cke ->
  Lemma (Bytes.equal (clientKeyExchangeBytes cke1) (clientKeyExchangeBytes cke2) ==> cke1 = cke2)
let clientKeyExchangeBytes_is_injective cke1 cke2 =
  admit(); // JK: TODO, see comment above
  if clientKeyExchangeBytes cke1 = clientKeyExchangeBytes cke2 then (
    ()
  ) else ()

(* val parseClientKeyExchange: p:protocolVersion -> kex:kexAlg -> b:bytes{repr_bytes(length b) <= 3} ->  *)
(*     Tot (result (cke:cke{Bytes.equal (clientKeyExchangeBytes p cke) (messageBytes HT_client_key_exchange b)})) *)
val parseClientKeyExchange: kex:kexAlg -> b:bytes{repr_bytes(length b) <= 3} -> Tot (result cke)
let parseClientKeyExchange kex data =
  match kex with
  | Kex_DH ->
      if length data = 0
      then Correct({cke_kex_c = KEX_C_DH})
      else fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "")
  | Kex_DHE ->
      if length data >= 2
      then (match vlparse 2 data with
           | Error(z) -> Error(z)
           | Correct(y) -> (lemma_repr_bytes_values (length y); Correct({cke_kex_c = KEX_C_DHE y})))
      else fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "")
  | Kex_ECDHE ->
      if length data >= 1
      then (match vlparse 1 data with
           | Error(z) -> Error(z)
           | Correct(y) -> (lemma_repr_bytes_values (length y); Correct({cke_kex_c = KEX_C_ECDHE y})))
      else fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "")
//  | SSL_3p0,Kex_RSA ->
//      if length data < 4096 then
//         (lemma_repr_bytes_values (length data); Correct({cke_kex_c = KEX_C_RSA data}))
//      else fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "")
  | Kex_RSA  ->
        if length data >= 2 then
            match vlparse 2 data with
            | Correct (encPMS) ->
        if length encPMS < 4096 then (lemma_repr_bytes_values (length encPMS); correct({cke_kex_c = KEX_C_RSA encPMS}))
        else fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "")
            | Error(z) -> Error(z)
        else fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "")

(* Signature *)

val signatureBytes: signature -> b:bytes{length b < 65540}
let signatureBytes sig =
  lemma_repr_bytes_values (length sig.sig_signature);
  let sig_bytes = vlbytes2 sig.sig_signature in
  match sig.sig_algorithm with
  | None -> sig_bytes
  | Some sigalg ->
    let sig_algorithm_bytes = signatureScheme_serializer32 sigalg in
    sig_algorithm_bytes @| sig_bytes

val signatureBytes_is_injective: sig1:signature -> sig2:signature ->
  Lemma (requires (None? sig1.sig_algorithm == None? sig2.sig_algorithm))
  (ensures (Bytes.equal (signatureBytes sig1) (signatureBytes sig2) ==> sig1 == sig2))
let signatureBytes_is_injective sig1 sig2 =
  if signatureBytes sig1 = signatureBytes sig2 then
    begin
    lemma_repr_bytes_values (length sig1.sig_signature);
    lemma_repr_bytes_values (length sig2.sig_signature);
    match sig1.sig_algorithm, sig2.sig_algorithm with
    | None, None -> lemma_vlbytes_inj 2 sig1.sig_signature sig2.sig_signature
    | Some sigalg1, Some sigalg2 ->
      begin
      //TODO bytes NS 09/27
      // lemma_append_inj (signatureSchemeBytes sigalg1)
      //                  (vlbytes2 sig1.sig_signature)
      //                  (signatureSchemeBytes sigalg2)
      //                  (vlbytes2 sig2.sig_signature);
//      signatureSchemeBytes_is_injective sigalg1 sigalg2;
      lemma_vlbytes_inj 2 sig1.sig_signature sig2.sig_signature
      end
    end

val parseSignature: pv:protocolVersion -> data:bytes -> result (sig:signature{Bytes.equal (signatureBytes sig) data})
let parseSignature pv data =
  if pv `geqPV` TLS_1p2 then
    if length data >= 4 then
      let alg, sig = split data 2ul in
      match signatureScheme_parser32 alg with
      | Some (sigalg, _) ->
        begin
        match vlparse 2 sig with
        | Correct sigv ->
          lemma_repr_bytes_values (length sigv);
          Correct ({sig_algorithm = Some sigalg; sig_signature = sigv})
        | _ ->
          fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "Signature: incorrect signature length")
        end
      | None -> fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "Signature: invalid signature scheme")
    else fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "Signature: message too short")
  else
    if length data >= 2 then
      match vlparse 2 data with
      | Correct sigv ->
        lemma_repr_bytes_values (length sigv);
        Correct ({sig_algorithm = None; sig_signature = sigv})
      | _ ->
        fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "Signature: incorrect signature length")
    else fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "Signature: message too short")


(* ServerKeyExchange *)

let kex_s_to_bytes kex =
  admit(); // JK: TODO
  match kex with
  | KEX_S_DHE (|g, k|) -> CommonDH.serialize #g k
  | KEX_S_RSA pk -> (*TODO: Ephemeral RSA*) empty_bytes

(* JK: TODO, or rewrite the functions altogether *)
assume val commonDH_serialize_is_injective: #g:CommonDH.group -> k1:CommonDH.pre_share g -> k2:CommonDH.pre_share g ->
  Lemma (requires True)
  (ensures (Bytes.equal (CommonDH.serialize k1) (CommonDH.serialize k2) ==> k1 == k2))

(* JK: TODO: missing the proper serialization for RSA so not injective for now *)
(* Actually false for now *)
assume val kex_s_to_bytes_is_injective: k1:kex_s -> k2:kex_s ->
  Lemma (requires True)
  (ensures (Bytes.equal (kex_s_to_bytes k1) (kex_s_to_bytes k2) ==> k1 == k2))

#reset-options "--admit_smt_queries true"

val serverKeyExchangeBytes: ske -> Tot (b:bytes{hs_msg_bytes HT_server_key_exchange b})
let serverKeyExchangeBytes ske =
  let kexB = kex_s_to_bytes ske.ske_kex_s in
  let sigB = signatureBytes ske.ske_signed_params in
  let payload = kexB @| sigB in
  lemma_repr_bytes_values (length payload);
  (messageBytes HT_server_key_exchange payload <: bytes)

(* JK: TODO, currently not injective and missing an extra argument compared to the
   parsing function: the kex algorithm *)
assume val serverKeyExchangeBytes_is_injective: s1:ske -> s2:ske ->
  Lemma (requires True)
  (ensures (Bytes.equal (serverKeyExchangeBytes s1) (serverKeyExchangeBytes s2) ==> s1 == s2))
(* let serverKeyExchangeBytes_is_injective s1 s2 =  *)
  (* if serverKeyExchangeBytes s1 = serverKeyExchangeBytes s2 then ( *)
  (*   let kexB1 = kex_s_to_bytes s1.ske_kex_s in *)
  (*   let payload1 = kexB1 @| s1.ske_sig in *)
  (*   lemma_repr_bytes_values (length payload1); *)
  (*   let kexB2 = kex_s_to_bytes s2.ske_kex_s in *)
  (*   let payload2 = kexB2 @| s2.ske_sig in *)
  (*   lemma_repr_bytes_values (length payload2); *)
  (*   messageBytes_is_injective HT_server_key_exchange payload1 HT_server_key_exchange payload2; *)
  (*   kex_s_to_bytes_is_injective s1.ske_kex_s s2.ske_kex_s; *)
  (* ) *)

(* val parseServerKeyExchange: kex:kexAlg -> b:bytes{repr_bytes(length b) <= 3} ->  *)
(*     Tot (result (s:ske{Bytes.equal (serverKeyExchangeBytes s) (messageBytes HT_server_key_exchange b)})) *)
val parseServerKeyExchange: pv:protocolVersion -> kex:kexAlg -> b:bytes{repr_bytes(length b) <= 3} -> result ske
let parseServerKeyExchange pv kex payload =
  match kex with
  | Kex_DHE ->
    begin
    match CommonDH.parse_partial false payload with
    | Correct (k, sigv) ->
      begin
      match parseSignature pv sigv with
      | Correct sig ->
        Correct ({ske_kex_s = KEX_S_DHE k; ske_signed_params = sig})
      | Error z -> Error z
      end
    | Error z -> Error z
    end
  | Kex_ECDHE ->
    begin
    match CommonDH.parse_partial true payload with
    | Correct (k, sigv) ->
      begin
      match parseSignature pv sigv with
      | Correct sig ->
        Correct ({ske_kex_s = KEX_S_DHE k; ske_signed_params = sig})
      | Error z -> Error z
      end
    | Error z -> Error z
    end
  | _ -> fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "ServerKeyExchange: Unexpected Key Exchange")


(* Certificate Verify *)

val certificateVerifyBytes: cv -> b:bytes{hs_msg_bytes HT_certificate_verify b}
let certificateVerifyBytes cv =
  let sigB = signatureBytes cv in
  lemma_repr_bytes_values (length sigB);
  messageBytes HT_certificate_verify sigB

val certificateVerifyBytes_is_injective: c1:cv -> c2:cv ->
  Lemma (requires (None? c1.sig_algorithm == None? c2.sig_algorithm))
  (ensures (Bytes.equal (certificateVerifyBytes c1) (certificateVerifyBytes c2) ==> c1 == c2))
let certificateVerifyBytes_is_injective c1 c2 =
  if certificateVerifyBytes c1 = certificateVerifyBytes c2 then
    begin
    let sig1 = signatureBytes c1 in
    let sig2 = signatureBytes c2 in
    lemma_repr_bytes_values (length sig1);
    lemma_repr_bytes_values (length sig2);
    signatureBytes_is_injective c1 c2;
    messageBytes_is_injective HT_certificate_verify sig1 HT_certificate_verify sig2
    end

val parseCertificateVerify: pv:protocolVersion -> data:bytes{repr_bytes(length data) <= 3} ->
  result (c:cv{Bytes.equal (certificateVerifyBytes c) (messageBytes HT_certificate_verify data)})
let parseCertificateVerify pv data =
  match parseSignature pv data with
  | Correct sig -> Correct sig
  | Error z -> Error z

val finishedBytes: fin -> Tot (b:bytes{hs_msg_bytes HT_finished b})
let finishedBytes fin =
  lemma_repr_bytes_values (length fin.fin_vd);
  messageBytes HT_finished fin.fin_vd

val finishedBytes_is_injective: f1:fin -> f2:fin ->
  Lemma (requires True)
  (ensures (Bytes.equal (finishedBytes f1) (finishedBytes f2) ==> f1 == f2))
let finishedBytes_is_injective f1 f2 =
  if finishedBytes f1 = finishedBytes f2 then (
    lemma_repr_bytes_values (length f1.fin_vd);
    lemma_repr_bytes_values (length f2.fin_vd);
    messageBytes_is_injective HT_finished f1.fin_vd HT_finished f2.fin_vd
  )

//#reset-options

val parseFinished: data:bytes{repr_bytes(length data) <= 3} ->
  result(f:fin{Bytes.equal (finishedBytes f) (messageBytes HT_finished data)})
let parseFinished data =
  if length data < 65536 then Correct ({fin_vd = data}) else error "Finished too large"


(* Session ticket *)

val sessionTicketBytes: sticket -> Tot (b:bytes{hs_msg_bytes HT_session_ticket b})
let sessionTicketBytes t =
  let payload =
    bytes_of_int 4 (UInt32.v t.sticket_lifetime) @|
    (vlbytes 2 t.sticket_ticket) in
  lemma_repr_bytes_values (length payload);
  messageBytes HT_session_ticket payload

val sessionTicketBytes13: sticket13 -> Tot (b:bytes{hs_msg_bytes HT_session_ticket b})
let sessionTicketBytes13 t =
  let payload =
    bytes_of_int32 t.ticket13_lifetime @|
    bytes_of_int32 t.ticket13_age_add @|
    vlbytes 1 t.ticket13_nonce @|
    vlbytes 2 t.ticket13_ticket @|
    extensionsBytes t.ticket13_extensions in
  lemma_repr_bytes_values (length payload);
  messageBytes HT_session_ticket payload

(* TODO generalize, with adequate condition of s1 and s2:
val sessionTicketBytes_is_injective: p:protocolVersion -> s1:sticket -> s2:sticket ->
  Lemma (requires (p <> TLS_1p3))
  (ensures (Bytes.equal (sessionTicketBytes p s1) (sessionTicketBytes p s2) ==> s1 = s2))
let sessionTicketBytes_is_injective p s1 s2 =
  if sessionTicketBytes p s1 = sessionTicketBytes p s2 then (
    let payload1 = s1.sticket_lifetime @| s1.sticket_ticket in
    let payload2 = s2.sticket_lifetime @| s2.sticket_ticket in
    lemma_repr_bytes_values (length payload1);
    lemma_repr_bytes_values (length payload2);
    messageBytes_is_injective HT_session_ticket payload1 HT_session_ticket payload2;
    lemma_append_inj s1.sticket_lifetime s1.sticket_ticket s2.sticket_lifetime s2.sticket_ticket
  )
*)

val parseSessionTicket: b:bytes{repr_bytes(length b) <= 3} ->
  result (s:sticket {Bytes.equal (sessionTicketBytes s) (messageBytes HT_session_ticket b)})
let parseSessionTicket b =
  if length b < 6 then
    fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "NewSessionTicket: too short")
  else
    begin
    let lifetimeB, ticketB = split b 4ul in
    let lifetime = int_of_bytes lifetimeB in
    lemma_repr_bytes_values lifetime;
    let lifetime = UInt32.uint_to_t lifetime in
    match vlparse 2 ticketB with
    | Correct ticket ->
      Correct ({ sticket_lifetime = lifetime; sticket_ticket = ticket })
    | Error _ ->
      fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "NewSessionTicket: incorrect length")
    end

val parseSessionTicket13: b:bytes{repr_bytes(length b) <= 3} ->
  result (s:sticket13 {Bytes.equal (sessionTicketBytes13 s) (messageBytes HT_session_ticket b)})
let parseSessionTicket13 b =
  if length b < 12 then
    fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "NewSessionTicket13: too short")
  else
    begin
    let lifetimeB, rest = split b 4ul in
    let lifetime = int_of_bytes lifetimeB in
    lemma_repr_bytes_values lifetime;
    let lifetime = UInt32.uint_to_t lifetime in
    let ageB, rest = split rest 4ul in
    let age = int_of_bytes ageB in
    lemma_repr_bytes_values age;
    let age = UInt32.uint_to_t age in
    match vlsplit 1 rest with
    | Error _ -> fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "NewSessionTicket13: invalid nonce (check draft version 21 or greater)")
    | Correct(x) ->
      let nonce, rest = x in
      begin
        match vlsplit 2 rest with
        | Correct (x) ->
          let ticket, rest = x in
          begin
          match vlsplit 2 rest with
          | Correct (x) ->
            let exts, eof = x in
            if length eof > 0 then
              fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "NewSessionTicket13: dangling bytes")
            else
              begin
              match parseExtensions EM_NewSessionTicket (vlbytes 2 exts) with
              | Correct (exts,None) ->
                Correct ({ ticket13_lifetime = lifetime;
                           ticket13_age_add = age;
                           ticket13_nonce = nonce;
                           ticket13_ticket = ticket;
                           ticket13_extensions = exts})
              | Error _ -> fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "NewSessionTicket13: invalid extensions")
              end
          | Error _ -> fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "NewSessionTicket13: incorrect length")
          end
        | Error _ -> fatal Decode_error (perror __SOURCE_FILE__ __LINE__ "NewSessionTicket13: incorrect length")
        end
      end


(* Hello retry request *)
// val helloRetryRequestBytes: hrr -> Tot (b:bytes{hs_msg_bytes HT_server_hello b})
let helloRetryRequestBytes hrr =
  serverHelloBytes ({
    sh_protocol_version = TLS_1p2;
    sh_server_random = bytes_of_hex "cf21ad74e59a6111be1d8c021e65b891c2a211167abb8c5e079e09e2c8a8339c";
    sh_sessionID = hrr.hrr_sessionID;
    sh_cipher_suite = hrr.hrr_cipher_suite;
    sh_compression = NullCompression;
    sh_extensions = Some hrr.hrr_extensions
  })
  (*
  let pvb = versionBytes hrr.hrr_protocol_version in
  let csb = cipherSuiteBytes hrr.hrr_cipher_suite in
  let extb = extensionsBytes hrr.hrr_extensions in
  let data = pvb @| csb @| extb in
  lemma_repr_bytes_values (length data);
  messageBytes HT_hello_retry_request data
  *)

val helloRetryRequestBytes_is_injective: h1:hrr -> h2:hrr ->
  Lemma (requires True)
  (ensures (Bytes.equal (helloRetryRequestBytes h1) (helloRetryRequestBytes h2) ==> h1 == h2))
let helloRetryRequestBytes_is_injective h1 h2 = admit()
(*
  if helloRetryRequestBytes h1 = helloRetryRequestBytes h2 then (
    let pv1 = versionBytes h1.hrr_protocol_version in
    let cs_bytes1 = cipherSuiteBytes h1.hrr_cipher_suite in
    let exts1 = extensionsBytes h1.hrr_extensions in
    let pv2 = versionBytes h2.hrr_protocol_version in
    let cs_bytes2 = cipherSuiteBytes h2.hrr_cipher_suite in
    let exts2 = extensionsBytes h2.hrr_extensions in
    let data1 = pv1 @| cs_bytes1 @| exts1 in
    lemma_repr_bytes_values (length data1);
    let data2 = pv2 @| cs_bytes2 @| exts2 in
    lemma_repr_bytes_values (length data2);
    messageBytes_is_injective HT_hello_retry_request data1 HT_hello_retry_request data2;
    //TODO bytes NS 09/27
    // lemma_append_inj pv1 (cs_bytes1 @| exts1) pv2 (cs_bytes2 @| exts2);
    // lemma_append_inj cs_bytes1 exts1 cs_bytes2 exts2;
    versionBytes_is_injective h1.hrr_protocol_version h2.hrr_protocol_version;
    cipherSuiteBytes_is_injective h1.hrr_cipher_suite h2.hrr_cipher_suite;
    extensionsBytes_is_injective h1.hrr_extensions h2.hrr_extensions
  )
*)

(* Encrypted_extensions *)
let valid_ee : Type0 = msg:ee{repr_bytes (length (extensionsBytes msg)) <= 3}

val encryptedExtensionsBytes: e:valid_ee -> Tot (b:bytes{hs_msg_bytes HT_encrypted_extensions b})
let encryptedExtensionsBytes ee =
    let payload = extensionsBytes ee in
    messageBytes HT_encrypted_extensions payload

val encryptedExtensionsBytes_is_injective: e1:valid_ee -> e2:valid_ee ->
  Lemma (requires True)
  (ensures (Bytes.equal (encryptedExtensionsBytes e1) (encryptedExtensionsBytes e2) ==> e1 == e2))
let encryptedExtensionsBytes_is_injective e1 e2 =
  let payload1 = extensionsBytes e1 in
  let payload2 = extensionsBytes e2 in
  messageBytes_is_injective HT_encrypted_extensions payload1 HT_encrypted_extensions payload2;
  extensionsBytes_is_injective e1 e2

(* JK : TODO *)
assume val lemma_extensionsBytes_length: mt:ext_msg -> b:bytes ->
  Lemma (requires True)
  (ensures (
    match parseExtensions mt b with
    | Error _ -> True
    | Correct (ee, obinders) ->
    let len = match obinders with
      | Some binders -> length (bindersBytes binders)
      | _ -> 0 in
    length (extensionsBytes ee) + len == length b))

(* val parseEncryptedExtensions: b:bytes{repr_bytes(length b) <= 3} ->  *)
(*     Tot (result (s:valid_ee{Bytes.equal (encryptedExtensionsBytes s) (messageBytes HT_encrypted_extensions b)})) *)
val parseEncryptedExtensions: b:bytes{repr_bytes(length b) <= 3} ->
    Tot (result valid_ee)
let parseEncryptedExtensions payload  =
  match parseExtensions EM_EncryptedExtensions payload with
  | Error z -> Error z
  | Correct (exts,None) ->
    if List.Tot.length exts >= 256 then  error "too many extensions" else
    ( lemma_extensionsBytes_length EM_EncryptedExtensions payload;
      Correct exts)

(*
(* Next protocol message *)
val nextProtocolBytes: np -> Tot (b:bytes{hs_msg_bytes HT_next_protocol b})
let nextProtocolBytes np =
  lemma_repr_bytes_values (length (np.np_selected_protocol));
  lemma_repr_bytes_values (length (np.np_padding));
  let selected_protocol = vlbytes 1 np.np_selected_protocol in
  let padding = vlbytes 1 np.np_padding in
  lemma_repr_bytes_values (length (selected_protocol @| padding));
  messageBytes HT_next_protocol (selected_protocol @| padding)

val nextProtocolBytes_is_injective: np1:np -> np2:np ->
  Lemma (requires True)
  (ensures (Bytes.equal (nextProtocolBytes np1) (nextProtocolBytes np2) ==> np1 = np2))
let nextProtocolBytes_is_injective np1 np2 =
  if nextProtocolBytes np1 = nextProtocolBytes np2 then (
    lemma_repr_bytes_values (length (np1.np_selected_protocol));
    lemma_repr_bytes_values (length (np1.np_padding));
    lemma_repr_bytes_values (length (np2.np_selected_protocol));
    lemma_repr_bytes_values (length (np2.np_padding));
    let selected_protocol1 = vlbytes 1 np1.np_selected_protocol in
    let padding1 = vlbytes 1 np1.np_padding in
    let selected_protocol2 = vlbytes 1 np2.np_selected_protocol in
    let padding2 = vlbytes 1 np2.np_padding in
    let data1 = (selected_protocol1 @| padding1) in
    let data2 = (selected_protocol2 @| padding2) in
    lemma_repr_bytes_values (length data1);
    lemma_repr_bytes_values (length data2);
    messageBytes_is_injective HT_next_protocol data1 HT_next_protocol data2;
    cut (Bytes.equal (Seq.slice selected_protocol1 0 1) (Seq.slice data1 0 1));
    cut (Bytes.equal (Seq.slice selected_protocol2 0 1) (Seq.slice data2 0 1));
    cut (Bytes.equal (Seq.slice selected_protocol2 0 1) (Seq.slice selected_protocol1 0 1));
    vlbytes_length_lemma 1 np1.np_selected_protocol np2.np_selected_protocol;
    lemma_append_inj selected_protocol1 padding1 selected_protocol2 padding2;
    lemma_vlbytes_inj 1 np1.np_selected_protocol np2.np_selected_protocol;
    lemma_vlbytes_inj 1 np1.np_padding np2.np_padding
  )

(* val parseNextProtocol: b:bytes{repr_bytes (length b) <= 3} ->  *)
(*     Tot (result (s:np{Bytes.equal (nextProtocolBytes s) (messageBytes HT_next_protocol b)})) *)
val parseNextProtocol: b:bytes{repr_bytes (length b) <= 3} ->Tot (result np)
let parseNextProtocol payload =
  if length payload >= 1 then
  match vlsplit 1 payload with
  | Error(z) -> Error(z)
  | Correct(selected_protocol, data) ->
  if length data >= 1 then
    match vlparse 1 data with
    | Error(z) -> Error(z)
    | Correct(padding) ->
  Correct( { np_selected_protocol = selected_protocol;
       np_padding = padding;})
  else Error (AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
  else Error (AD_decode_error, perror __SOURCE_FILE__ __LINE__ "")
*)

val endOfEarlyDataBytes: b:lbytes 4{hs_msg_bytes HT_end_of_early_data b}
let endOfEarlyDataBytes =
  lemma_repr_bytes_values 0;
  messageBytes HT_end_of_early_data empty_bytes

val keyUpdateBytes: u:bool -> b:lbytes 5{hs_msg_bytes HT_key_update b}
let keyUpdateBytes u =
  lemma_repr_bytes_values 1;
  messageBytes HT_key_update (abyte (if u then 1z else 0z))

//FIXME: Implement CertificateRequest in TLS 1.3
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Parsers.CipherSuite.fsti.checked MiTLS.Extensions.fsti.checked MiTLS.CommonDH.fsti.checked MiTLS.Cert.fsti.checked LowParse.SLow.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.HandshakeMessages.fst
cr: MiTLS.HandshakeMessages.cr13
  -> b:
    FStar.Bytes.lbytes 4
      {MiTLS.HandshakeMessages.hs_msg_bytes MiTLS.HandshakeMessages.HT_certificate_request b}
MiTLS.HandshakeMessages.cr13 MiTLS.HandshakeMessages.messageBytes MiTLS.HandshakeMessages.HT_certificate_request FStar.Bytes.empty_bytes Prims.unit FStar.Bytes.lemma_repr_bytes_values FStar.Bytes.lbytes MiTLS.HandshakeMessages.hs_msg_bytes
let certificateRequestBytes13 cr =
  
lemma_repr_bytes_values 0;
messageBytes HT_certificate_request empty_bytes