val crypto_kem_keypair:
    a:frodo_alg
  -> gen_a:frodo_gen_a
  -> state:Spec.Frodo.Random.state_t
  -> lbytes (crypto_publickeybytes a) & lbytes (crypto_secretkeybytes a)
let crypto_kem_keypair a gen_a state = KeyGen.crypto_kem_keypair a gen_a state
val crypto_kem_keypair:
    a:frodo_alg
  -> gen_a:frodo_gen_a
  -> state:Spec.Frodo.Random.state_t
  -> lbytes (crypto_publickeybytes a) & lbytes (crypto_secretkeybytes a)
let crypto_kem_keypair a gen_a state =
KeyGen.crypto_kem_keypair a gen_a state
Spec.Frodo.KEM.fst.checked
Spec.Frodo.Random.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 prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.Frodo.KEM.fst
Spec.Frodo.Params.frodo_alg Spec.Frodo.Params.frodo_gen_a Spec.Frodo.Random.state_t Spec.Frodo.KEM.KeyGen.crypto_kem_keypair FStar.Pervasives.Native.tuple2 Lib.ByteSequence.lbytes Spec.Frodo.Params.crypto_publickeybytes Spec.Frodo.Params.crypto_secretkeybytes
module Spec.Frodo.KEM

open FStar.Mul

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

open Spec.Frodo.Params

module KeyGen = Spec.Frodo.KEM.KeyGen
module Encaps = Spec.Frodo.KEM.Encaps
module Decaps = Spec.Frodo.KEM.Decaps

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

val crypto_kem_keypair:
    a:frodo_alg
  -> gen_a:frodo_gen_a
  -> state:Spec.Frodo.Random.state_t
  -> lbytes (crypto_publickeybytes a) & lbytes (crypto_secretkeybytes a)
val crypto_kem_keypair:
    a:frodo_alg
  -> gen_a:frodo_gen_a
  -> state:Spec.Frodo.Random.state_t
  -> lbytes (crypto_publickeybytes a) & lbytes (crypto_secretkeybytes a)

    a: Spec.Frodo.Params.frodo_alg ->
    gen_a: Spec.Frodo.Params.frodo_gen_a ->
    state: Spec.Frodo.Random.state_t
  -> Lib.ByteSequence.lbytes (Spec.Frodo.Params.crypto_publickeybytes a) *
    Lib.ByteSequence.lbytes (Spec.Frodo.Params.crypto_secretkeybytes a)