val tresult : a: Type -> Type
let tresult (a : Type) = result a test_error
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
/
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
a: Type -> Type
Spec.Noise.Base.Definitions.result Spec.Noise.Testing.Base.test_error
let tresult (a: Type) =
  
result a test_error