val execute_transport_messages
      (nc: config)
      (i: nat)
      (one_way: bool)
      (vectors: list (message_test_vector nc))
      (is rs: cipher_states_pair)
    : Tot (tresult (cipher_states_pair & cipher_states_pair)) (decreases vectors)
val execute_transport_messages
      (nc: config)
      (i: nat)
      (one_way: bool)
      (vectors: list (message_test_vector nc))
      (is rs: cipher_states_pair)
    : Tot (tresult (cipher_states_pair & cipher_states_pair)) (decreases vectors)
let rec execute_transport_messages (nc : config) (i : nat) (one_way : bool)
                                   (vectors : list (message_test_vector nc))
                                   (is rs : cipher_states_pair) :
  Tot (tresult (cipher_states_pair & cipher_states_pair))
  (decreases vectors) =
  match vectors with
  | [] -> Res (is, rs)
  | v1 :: vectors1 ->
    match encrypt_with_ad nc Seq.empty v1.payload (fst is) with
    | Fail e ->
      Fail ("transport message #" ^ (string_of_int i) ^ ": encrypt_with_ad failed: "
            ^ (string_of_error e))
    | Res (cipher, ics1) ->
      (* Check the cipher text *)
      if length cipher > max_size_t then Fail ("length cipher > max_size_t")
      else if not (bytes_eq cipher v1.ciphertext)
      then Fail ("transport message #" ^ (string_of_int i) ^ ": encrypt_with_ad: " ^
                 "the ciphertext doesn't match the reference") else
      match decrypt_with_ad nc Seq.empty cipher (fst rs) with
      | Fail e ->
        Fail ("transport message #" ^ (string_of_int i) ^ ": decrypt_with_ad failed: "
              ^ (string_of_error e))
      | Res (plain, rcs1) ->
        if length plain > max_size_t then Fail ("length plain > max_size_t")
        else if not (bytes_eq plain v1.payload)
        then Fail ("transport_message #" ^ (string_of_int i) ^
                   ": the deciphered ciphertext doesn't match the original plaintext")
        else
        let is1 = (ics1, snd is) in
        let rs1 = (rcs1, snd rs) in
        (* Take care of the order of the different states: if it is not one-way,
         * we invert the cipher states AND we invert the pairs *)
        let is2, rs2 = if one_way then is1, rs1 else swap_pair rs1, swap_pair is1 in
        match execute_transport_messages nc (i+1) one_way vectors1 (**) is2 rs2 (**) with
        | Fail e -> Fail e
        | Res (is3, rs3) ->
          (* Re-invert to retrieve the original order *)
          let is4, rs4 = if one_way then is3, rs3 else swap_pair rs3, swap_pair is3 in
          Res (swap_pair is4, swap_pair rs4)
module Spec.Noise.Testing.Base

open Lib.IntTypes
open Lib.RawIntTypes
open Lib.ByteSequence
open Lib.Sequence

open Spec.Noise.CryptoPrimitives
open Spec.Noise.Base
open Spec.Noise.WellFormedness
open Spec.Noise.Patterns

open Spec.Noise.Utils

open FStar.All
module IO = FStar.IO

#set-options "--z3rlimit 15 --fuel 0 --ifuel 1"

/// The following file defines testing utilities for the Noise patterns

let swap_pair (#a #b : Type) (p : a & b) : b & a =
  match p with x, y -> y, x

(* TODO: should be moved *)
let bytes_eq (b1 : bytes{length b1 <= max_size_t})
             (b2 : bytes{length b2 <= max_size_t}) :
  b:bool{b <==> b1 == b2} =
  if length b1 <> length b2 then false
  else lbytes_eq #(length b1) b1 b2

let string_of_error (e : error) : string =
  match e with
  | No_key          -> "No_key"
  | Already_key     -> "Already_key"
  | Input_size      -> "Input_size"
  | DH              -> "DH"
  | Decryption      -> "Decryption"
  | Saturated_nonce -> "Saturated_nonce"

type test_error = string

let tresult (a : Type) = result a test_error

noeq type message_test_vector (nc : config) = {
  payload : plain_message nc;
  ciphertext : c:bytes{length c <= max_size_t};
}

noeq type handshake_test_vector = {
  nc : config;
  pattern : wf_handshake_pattern;
  protocol_str : string; // The protocol name
  protocol_name : hashable nc; // The protocol name but interpreted as a sequence of bytes
  prologue : hashable nc;
  is : option (private_key nc);
  ie : option (private_key nc);
  rs : option (private_key nc);
  re : option (private_key nc);
  irs : option (public_key nc); (* initiator remote static - actually not used *)
  rrs : option (public_key nc); (* responder remote static - actually not used *)
  psk : option preshared_key;
  final_hash : hash nc;
  msgs : (msgs:list (message_test_vector nc){List.Tot.length msgs >= List.Tot.length pattern.messages});
}

type handshake_state_pair (nc : config) = handshake_state nc & handshake_state nc

let execute_premessage (nc : config) (hsk : wf_handshake_pattern)
                       (ir : bool) (is rs : handshake_state nc) :
  Tot (tresult (handshake_state_pair nc)) =  
  match (if ir then hsk.premessage_ir else hsk.premessage_ri) with
  | None -> Res (is, rs)
  | Some pre ->
    match csend_premessage nc hsk ir is with
    | Fail _ -> Fail ("send_premessage failed (ir:" ^ (string_of_bool ir) ^ ")")
    | Res (msg1, is1) ->
      if length msg1 > max_size_t then Fail "send_premessage: premessage too long" else
      match creceive_premessage nc hsk ir msg1 rs with
      | Fail _ -> Fail ("receive_premessage failed (ir:" ^ (string_of_bool ir) ^ ")")
      | Res rs1 ->
        Res (is1, rs1)

/// Note that in the case of handshame patterns with only one message, everything
/// goes one way.
/
Spec.Noise.WellFormedness.fsti.checked Spec.Noise.Utils.fst.checked Spec.Noise.Patterns.fst.checked Spec.Noise.CryptoPrimitives.fsti.checked Spec.Noise.Base.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.List.Pure.Properties.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.All.fst.checked
Spec.Noise.Testing.Base.fst

    nc: Spec.Noise.CryptoPrimitives.config ->
    i: Prims.nat ->
    one_way: Prims.bool ->
    vectors: Prims.list (Spec.Noise.Testing.Base.message_test_vector nc) ->
    is: Spec.Noise.Base.Definitions.cipher_states_pair ->
    rs: Spec.Noise.Base.Definitions.cipher_states_pair
  -> Prims.Tot
    (Spec.Noise.Testing.Base.tresult (Spec.Noise.Base.Definitions.cipher_states_pair *
          Spec.Noise.Base.Definitions.cipher_states_pair))
Spec.Noise.CryptoPrimitives.config Prims.nat Prims.bool Prims.list Spec.Noise.Testing.Base.message_test_vector Spec.Noise.Base.Definitions.cipher_states_pair Spec.Noise.Base.Definitions.Res FStar.Pervasives.Native.tuple2 Spec.Noise.Testing.Base.test_error FStar.Pervasives.Native.Mktuple2 Spec.Noise.Base.Definitions.encrypt_with_ad FStar.Seq.Base.empty Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.Noise.Testing.Base.__proj__Mkmessage_test_vector__item__payload FStar.Pervasives.Native.fst Spec.Noise.Base.Definitions.cipher_state Spec.Noise.Base.Definitions.error Spec.Noise.Base.Definitions.Fail Prims.op_Hat Prims.string_of_int Spec.Noise.Testing.Base.string_of_error Lib.ByteSequence.bytes Prims.op_GreaterThan Lib.Sequence.length Lib.IntTypes.max_size_t Prims.op_Negation Spec.Noise.Testing.Base.bytes_eq Spec.Noise.Testing.Base.__proj__Mkmessage_test_vector__item__ciphertext Spec.Noise.Base.Definitions.decrypt_with_ad Prims.precedes Spec.Noise.Testing.Base.execute_transport_messages Prims.op_Addition Spec.Noise.Testing.Base.swap_pair Spec.Noise.Testing.Base.tresult FStar.Pervasives.Native.snd
let rec execute_transport_messages
      (nc: config)
      (i: nat)
      (one_way: bool)
      (vectors: list (message_test_vector nc))
      (is rs: cipher_states_pair)
    : Tot (tresult (cipher_states_pair & cipher_states_pair)) (decreases vectors) =
  
match vectors with
| [] -> Res (is, rs)
| v1 :: vectors1 ->
  match encrypt_with_ad nc Seq.empty v1.payload (fst is) with
  | Fail e ->
    Fail
    ("transport message #" ^ (string_of_int i) ^ ": encrypt_with_ad failed: " ^ (string_of_error e))
  | Res (cipher, ics1) ->
    if length cipher > max_size_t
    then Fail ("length cipher > max_size_t")
    else
      if not (bytes_eq cipher v1.ciphertext)
      then
        Fail
        ("transport message #" ^
          (string_of_int i) ^ ": encrypt_with_ad: " ^ "the ciphertext doesn't match the reference")
      else
        match decrypt_with_ad nc Seq.empty cipher (fst rs) with
        | Fail e ->
          Fail
          ("transport message #" ^
            (string_of_int i) ^ ": decrypt_with_ad failed: " ^ (string_of_error e))
        | Res (plain, rcs1) ->
          if length plain > max_size_t
          then Fail ("length plain > max_size_t")
          else
            if not (bytes_eq plain v1.payload)
            then
              Fail
              ("transport_message #" ^
                (string_of_int i) ^
                ": the deciphered ciphertext doesn't match the original plaintext")
            else
              let is1 = (ics1, snd is) in
              let rs1 = (rcs1, snd rs) in
              let is2, rs2 = if one_way then is1, rs1 else swap_pair rs1, swap_pair is1 in
              match execute_transport_messages nc (i + 1) one_way vectors1 is2 rs2 with
              | Fail e -> Fail e
              | Res (is3, rs3) ->
                let is4, rs4 = if one_way then is3, rs3 else swap_pair rs3, swap_pair is3 in
                Res (swap_pair is4, swap_pair rs4)