val crypto_kem_keypair: crypto_kem_keypair_st FP.Frodo640 FP.SHAKE128
let crypto_kem_keypair pk sk =
  crypto_kem_keypair FP.Frodo640 FP.SHAKE128 pk sk
val crypto_kem_keypair: crypto_kem_keypair_st FP.Frodo640 FP.SHAKE128
let crypto_kem_keypair pk sk =
crypto_kem_keypair FP.Frodo640 FP.SHAKE128 pk sk
Hacl.Frodo640.fst.checked
Spec.Frodo.Params.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.Frodo.Params.fst.checked Hacl.Frodo.KEM.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Frodo640.fst
Hacl.Impl.Matrix.lbytes Hacl.Impl.Frodo.Params.crypto_publickeybytes Spec.Frodo.Params.Frodo640 Hacl.Impl.Frodo.Params.crypto_secretkeybytes Hacl.Frodo.KEM.crypto_kem_keypair Spec.Frodo.Params.SHAKE128 Lib.IntTypes.uint32
module Hacl.Frodo640

open FStar.HyperStack
open FStar.HyperStack.ST

open Lib.IntTypes
open Lib.Buffer

open Hacl.Frodo.KEM
open Hacl.Impl.Frodo.Params

module FP = Spec.Frodo.Params

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

let crypto_bytes :r:size_t{v r == FP.crypto_bytes FP.Frodo640} =
  crypto_bytes FP.Frodo640

let crypto_publickeybytes :r:size_t{v r == FP.crypto_publickeybytes FP.Frodo640} =
  normalize_term (crypto_publickeybytes FP.Frodo640)

let crypto_secretkeybytes :r:size_t{v r == FP.crypto_secretkeybytes FP.Frodo640} =
  normalize_term (crypto_secretkeybytes FP.Frodo640)

let crypto_ciphertextbytes :r:size_t{v r == FP.crypto_ciphertextbytes FP.Frodo640} =
  normalize_term (crypto_ciphertextbytes FP.Frodo640)


val crypto_kem_keypair: crypto_kem_keypair_st FP.Frodo640 FP.SHAKE128
val crypto_kem_keypair: crypto_kem_keypair_st FP.Frodo640 FP.SHAKE128
Hacl.Frodo.KEM.crypto_kem_keypair_st Spec.Frodo.Params.Frodo640 Spec.Frodo.Params.SHAKE128