let compare (#len: size_nat) (test_expected: lbytes len) (test_result: lbytes len) =
  for_all2 (fun a b -> uint_to_nat #U8 a = uint_to_nat #U8 b) test_expected test_result
let compare (#len: size_nat) (test_expected test_result: lbytes len) =
for_all2 (fun a b -> uint_to_nat #U8 a = uint_to_nat #U8 b) test_expected test_result
Spec.Frodo.Test.fst.checked
Spec.Frodo.Params.fst.checked Spec.Frodo.KEM.KeyGen.fst.checked Spec.Frodo.KEM.Encaps.fst.checked Spec.Frodo.KEM.Decaps.fst.checked Spec.Frodo.KEM.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.PrintSequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt8.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.IO.fst.checked FStar.All.fst.checked
Spec.Frodo.Test.fst
Lib.IntTypes.size_nat Lib.ByteSequence.lbytes Lib.Sequence.for_all2 Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Prims.op_Equality Prims.nat Prims.l_or Prims.b2t Prims.int Prims.op_GreaterThanOrEqual Lib.IntTypes.range Lib.IntTypes.uint_v Lib.RawIntTypes.uint_to_nat Prims.bool
module Spec.Frodo.Test

open FStar.Mul

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

open Spec.Frodo.KEM
open Spec.Frodo.KEM.KeyGen
open Spec.Frodo.KEM.Encaps
open Spec.Frodo.KEM.Decaps
open Spec.Frodo.Params

open FStar.All

module PS = Lib.PrintSequence

#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
val compare : test_expected: Lib.ByteSequence.lbytes len -> test_result: Lib.ByteSequence.lbytes len -> Prims.bool
test_expected: Lib.ByteSequence.lbytes len -> test_result: Lib.ByteSequence.lbytes len -> Prims.bool