val bytes_eq (b1: bytes{length b1 <= max_size_t}) (b2: bytes{length b2 <= max_size_t})
    : b: bool{b <==> b1 == b2}
val bytes_eq (b1: bytes{length b1 <= max_size_t}) (b2: bytes{length b2 <= max_size_t})
    : b: bool{b <==> b1 == b2}
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
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
/
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

    b1: Lib.ByteSequence.bytes{Lib.Sequence.length b1 <= Lib.IntTypes.max_size_t} ->
    b2: Lib.ByteSequence.bytes{Lib.Sequence.length b2 <= Lib.IntTypes.max_size_t}
  -> b: Prims.bool{b <==> b1 == b2}
Lib.ByteSequence.bytes Prims.b2t Prims.op_LessThanOrEqual Lib.Sequence.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.max_size_t Prims.op_disEquality Prims.nat Prims.bool Lib.ByteSequence.lbytes_eq Prims.l_iff Prims.eq2 Prims.l_or
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