let test1_enccoins =
  List.Tot.map u8_from_UInt8
    [
      0x8duy; 0xf3uy; 0xfauy; 0xe3uy; 0x83uy; 0x27uy; 0xc5uy; 0x3cuy; 0xc1uy; 0xc4uy; 0x8cuy; 0x60uy;
      0xb2uy; 0x52uy; 0x2buy; 0xb5uy
    ]
let test1_enccoins =
List.Tot.map u8_from_UInt8
  [
    0x8duy; 0xf3uy; 0xfauy; 0xe3uy; 0x83uy; 0x27uy; 0xc5uy; 0x3cuy; 0xc1uy; 0xc4uy; 0x8cuy; 0x60uy;
    0xb2uy; 0x52uy; 0x2buy; 0xb5uy
  ]
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
FStar.List.Tot.Base.map FStar.UInt8.t Lib.IntTypes.uint8 Lib.RawIntTypes.u8_from_UInt8 Prims.Cons FStar.UInt8.__uint_to_t Prims.Nil
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})
  (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

//
// Test1. FrodoKEM-64. SHAKE128
//
let test1_keypaircoins =
  List.Tot.map u8_from_UInt8
    [
      0xa6uy; 0x65uy; 0x65uy; 0x9fuy; 0xfbuy; 0xe4uy; 0x06uy; 0x5cuy; 0xcauy; 0x81uy; 0x5auy; 0x45uy;
      0xe4uy; 0x94uy; 0xd8uy; 0x01uy; 0x90uy; 0x30uy; 0x33uy; 0x55uy; 0x33uy; 0x84uy; 0x2euy; 0xe4uy;
      0x4cuy; 0x55uy; 0x8fuy; 0xd8uy; 0xaeuy; 0x4buy; 0x4euy; 0x91uy; 0x62uy; 0xfeuy; 0xc7uy; 0x9auy;
      0xc5uy; 0xcduy; 0x1fuy; 0xe2uy; 0xd2uy; 0x00uy; 0x63uy; 0x39uy; 0xaauy; 0xb1uy; 0xf3uy; 0x17uy
    ]
val test1_enccoins : Prims.list Lib.IntTypes.uint8
Prims.list Lib.IntTypes.uint8