val execute_premessage
      (nc: config)
      (hsk: wf_handshake_pattern)
      (ir: bool)
      (is rs: handshake_state nc)
    : Tot (tresult (handshake_state_pair nc))
val execute_premessage
      (nc: config)
      (hsk: wf_handshake_pattern)
      (ir: bool)
      (is rs: handshake_state nc)
    : Tot (tresult (handshake_state_pair 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)
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
/
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 ->
    hsk: Spec.Noise.WellFormedness.wf_handshake_pattern ->
    ir: Prims.bool ->
    is: Spec.Noise.Base.Definitions.handshake_state nc ->
    rs: Spec.Noise.Base.Definitions.handshake_state nc
  -> Spec.Noise.Testing.Base.tresult (Spec.Noise.Testing.Base.handshake_state_pair nc)
Spec.Noise.CryptoPrimitives.config Spec.Noise.WellFormedness.wf_handshake_pattern Prims.bool Spec.Noise.Base.Definitions.handshake_state Spec.Noise.Base.Definitions.__proj__Mkhandshake_pattern__item__premessage_ir Spec.Noise.Base.Definitions.__proj__Mkhandshake_pattern__item__premessage_ri Spec.Noise.Base.Definitions.Res Spec.Noise.Testing.Base.handshake_state_pair Spec.Noise.Testing.Base.test_error FStar.Pervasives.Native.Mktuple2 Prims.list Spec.Noise.Base.Definitions.premessage_token Spec.Noise.Base.Definitions.csend_premessage Spec.Noise.Base.Definitions.pre_error Spec.Noise.Base.Definitions.Fail Prims.op_Hat Prims.string_of_bool Lib.ByteSequence.bytes Prims.op_GreaterThan Lib.Sequence.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.max_size_t Spec.Noise.Base.Definitions.creceive_premessage Spec.Noise.Testing.Base.tresult
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)