val test_frodo
      (a: frodo_alg)
      (gen_a: frodo_gen_a)
      (keypaircoins: list uint8 {List.Tot.length keypaircoins == 2 * crypto_bytes a + bytes_seed_a})
      (enccoins: list uint8 {List.Tot.length enccoins == bytes_mu a})
      (ss_expected: list uint8 {List.Tot.length ss_expected == crypto_bytes a})
      (pk_expected: list uint8 {List.Tot.length pk_expected == crypto_publickeybytes a})
      (ct_expected: list uint8 {List.Tot.length ct_expected == crypto_ciphertextbytes a})
      (sk_expected: list uint8 {List.Tot.length sk_expected == crypto_secretkeybytes a})
    : ML bool
let test_frodo
  (a:frodo_alg)
  (gen_a:frodo_gen_a)
  (keypaircoins: list uint8 {List.Tot.length keypaircoins == 2 * crypto_bytes a + bytes_seed_a})
  (enccoins: list uint8 {List.Tot.length enccoins == bytes_mu a})
  (ss_expected: list uint8 {List.Tot.length ss_expected == crypto_bytes a})
  (pk_expected: list uint8 {List.Tot.length pk_expected == crypto_publickeybytes a})
  (ct_expected: list uint8 {List.Tot.length ct_expected == crypto_ciphertextbytes a})
  (sk_expected: list uint8 {List.Tot.length sk_expected == crypto_secretkeybytes a})
  : ML bool =
  let keypaircoins = createL keypaircoins in
  let enccoins = createL enccoins in
  let ss_expected = createL ss_expected in
  let pk_expected = createL pk_expected in
  let ct_expected = createL ct_expected in
  let sk_expected = createL sk_expected in
  let pk, sk = crypto_kem_keypair_ a gen_a keypaircoins in
  let ct, ss1 = crypto_kem_enc_ a gen_a enccoins pk in
  let ss2 = crypto_kem_dec a gen_a ct sk in
  let r_pk = compare pk_expected pk in
  let r_sk = compare sk_expected sk in
  let r_ct = compare ct_expected ct in
  let r_ss = PS.print_compare true (crypto_bytes a) ss1 ss2 in
  let r_ss1 = PS.print_compare true (crypto_bytes a) ss_expected ss2 in
  r_pk && r_sk && r_ct && r_ss && r_ss1
val test_frodo
      (a: frodo_alg)
      (gen_a: frodo_gen_a)
      (keypaircoins: list uint8 {List.Tot.length keypaircoins == 2 * crypto_bytes a + bytes_seed_a})
      (enccoins: list uint8 {List.Tot.length enccoins == bytes_mu a})
      (ss_expected: list uint8 {List.Tot.length ss_expected == crypto_bytes a})
      (pk_expected: list uint8 {List.Tot.length pk_expected == crypto_publickeybytes a})
      (ct_expected: list uint8 {List.Tot.length ct_expected == crypto_ciphertextbytes a})
      (sk_expected: list uint8 {List.Tot.length sk_expected == crypto_secretkeybytes a})
    : ML bool
let test_frodo
      (a: frodo_alg)
      (gen_a: frodo_gen_a)
      (keypaircoins: list uint8 {List.Tot.length keypaircoins == 2 * crypto_bytes a + bytes_seed_a})
      (enccoins: list uint8 {List.Tot.length enccoins == bytes_mu a})
      (ss_expected: list uint8 {List.Tot.length ss_expected == crypto_bytes a})
      (pk_expected: list uint8 {List.Tot.length pk_expected == crypto_publickeybytes a})
      (ct_expected: list uint8 {List.Tot.length ct_expected == crypto_ciphertextbytes a})
      (sk_expected: list uint8 {List.Tot.length sk_expected == crypto_secretkeybytes a})
    : ML bool =
let keypaircoins = createL keypaircoins in
let enccoins = createL enccoins in
let ss_expected = createL ss_expected in
let pk_expected = createL pk_expected in
let ct_expected = createL ct_expected in
let sk_expected = createL sk_expected in
let pk, sk = crypto_kem_keypair_ a gen_a keypaircoins in
let ct, ss1 = crypto_kem_enc_ a gen_a enccoins pk in
let ss2 = crypto_kem_dec a gen_a ct sk in
let r_pk = compare pk_expected pk in
let r_sk = compare sk_expected sk in
let r_ct = compare ct_expected ct in
let r_ss = PS.print_compare true (crypto_bytes a) ss1 ss2 in
let r_ss1 = PS.print_compare true (crypto_bytes a) ss_expected ss2 in
r_pk && r_sk && r_ct && r_ss && r_ss1
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
Spec.Frodo.Params.frodo_alg Spec.Frodo.Params.frodo_gen_a Prims.list Lib.IntTypes.uint8 Prims.eq2 Prims.int FStar.List.Tot.Base.length Prims.op_Addition FStar.Mul.op_Star Spec.Frodo.Params.crypto_bytes Spec.Frodo.Params.bytes_seed_a Prims.l_or Prims.b2t Prims.op_GreaterThanOrEqual Prims.l_and Prims.op_GreaterThan Prims.op_LessThanOrEqual Lib.IntTypes.max_size_t Spec.Frodo.Params.bytes_mu Spec.Frodo.Params.crypto_publickeybytes Spec.Frodo.Params.crypto_ciphertextbytes Spec.Frodo.Params.crypto_secretkeybytes Lib.ByteSequence.lbytes Prims.op_AmpAmp Prims.bool Lib.PrintSequence.print_compare Spec.Frodo.Test.compare Lib.Sequence.lseq Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.Frodo.KEM.Decaps.crypto_kem_dec FStar.Pervasives.Native.tuple2 Spec.Frodo.KEM.Encaps.crypto_kem_enc_ Spec.Frodo.KEM.KeyGen.crypto_kem_keypair_ FStar.Seq.Base.seq Lib.Sequence.to_seq FStar.Seq.Properties.seq_of_list Lib.Sequence.createL
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"

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 test_frodo
  (a:frodo_alg)
  (gen_a:frodo_gen_a)
  (keypaircoins: list uint8 {List.Tot.length keypaircoins == 2 * crypto_bytes a + bytes_seed_a})
  (enccoins: list uint8 {List.Tot.length enccoins == bytes_mu a})
  (ss_expected: list uint8 {List.Tot.length ss_expected == crypto_bytes a})
  (pk_expected: list uint8 {List.Tot.length pk_expected == crypto_publickeybytes a})
  (ct_expected: list uint8 {List.Tot.length ct_expected == crypto_ciphertextbytes a})
val test_frodo
      (a: frodo_alg)
      (gen_a: frodo_gen_a)
      (keypaircoins: list uint8 {List.Tot.length keypaircoins == 2 * crypto_bytes a + bytes_seed_a})
      (enccoins: list uint8 {List.Tot.length enccoins == bytes_mu a})
      (ss_expected: list uint8 {List.Tot.length ss_expected == crypto_bytes a})
      (pk_expected: list uint8 {List.Tot.length pk_expected == crypto_publickeybytes a})
      (ct_expected: list uint8 {List.Tot.length ct_expected == crypto_ciphertextbytes a})
      (sk_expected: list uint8 {List.Tot.length sk_expected == crypto_secretkeybytes a})
    : ML bool

    a: Spec.Frodo.Params.frodo_alg ->
    gen_a: Spec.Frodo.Params.frodo_gen_a ->
    keypaircoins:
      Prims.list Lib.IntTypes.uint8
        { FStar.List.Tot.Base.length keypaircoins ==
          2 * Spec.Frodo.Params.crypto_bytes a + Spec.Frodo.Params.bytes_seed_a } ->
    enccoins:
      Prims.list Lib.IntTypes.uint8
        {FStar.List.Tot.Base.length enccoins == Spec.Frodo.Params.bytes_mu a} ->
    ss_expected:
      Prims.list Lib.IntTypes.uint8
        {FStar.List.Tot.Base.length ss_expected == Spec.Frodo.Params.crypto_bytes a} ->
    pk_expected:
      Prims.list Lib.IntTypes.uint8
        {FStar.List.Tot.Base.length pk_expected == Spec.Frodo.Params.crypto_publickeybytes a} ->
    ct_expected:
      Prims.list Lib.IntTypes.uint8
        {FStar.List.Tot.Base.length ct_expected == Spec.Frodo.Params.crypto_ciphertextbytes a} ->
    sk_expected:
      Prims.list Lib.IntTypes.uint8
        {FStar.List.Tot.Base.length sk_expected == Spec.Frodo.Params.crypto_secretkeybytes a}
  -> FStar.All.ML Prims.bool