val valid_crt13 : Type0
let valid_crt13 = c:crt13 {length (Cert.certificateListBytes13 c.crt_chain13) < 16777212}
(* 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 *)
/
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
Type0
MiTLS.HandshakeMessages.crt13 Prims.b2t Prims.op_LessThan FStar.Bytes.length MiTLS.Cert.certificateListBytes13 MiTLS.HandshakeMessages.__proj__Mkcrt13__item__crt_chain13
let valid_crt13 =
  
c: crt13{length (Cert.certificateListBytes13 c.crt_chain13) < 16777212}