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'})
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)
  | [] -> []
(* 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
/
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
l: MiTLS.CipherSuite.valid_cipher_suites
  -> l':
    Prims.list (c: MiTLS.CipherSuite.cipherSuite{MiTLS.CipherSuite.validCipherSuite c})
      {FStar.List.Tot.Base.length l == FStar.List.Tot.Base.length l'}
MiTLS.CipherSuite.valid_cipher_suites MiTLS.CipherSuite.cipherSuite Prims.list Prims.Cons Prims.b2t MiTLS.CipherSuite.validCipherSuite MiTLS.HandshakeMessages.list_valid_to_valid_list Prims.Nil Prims.eq2 Prims.nat FStar.List.Tot.Base.length
let rec list_valid_to_valid_list l =
  
match l with
| hd :: tl -> hd :: (list_valid_to_valid_list tl)
| [] -> []