val crypto_kem_enc: crypto_kem_enc_st FP.Frodo976 FP.SHAKE128
let crypto_kem_enc ct ss pk =
  crypto_kem_enc FP.Frodo976 FP.SHAKE128 ct ss pk
val crypto_kem_enc: crypto_kem_enc_st FP.Frodo976 FP.SHAKE128
let crypto_kem_enc ct ss pk =
crypto_kem_enc FP.Frodo976 FP.SHAKE128 ct ss pk
Hacl.Frodo976.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.Frodo976.fst
Hacl.Impl.Matrix.lbytes Hacl.Impl.Frodo.Params.crypto_ciphertextbytes Spec.Frodo.Params.Frodo976 Hacl.Impl.Frodo.Params.crypto_bytes Hacl.Impl.Frodo.Params.crypto_publickeybytes Hacl.Frodo.KEM.crypto_kem_enc Spec.Frodo.Params.SHAKE128 Lib.IntTypes.uint32
module Hacl.Frodo976

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.Frodo976} =
  crypto_bytes FP.Frodo976

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

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

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


val crypto_kem_keypair: crypto_kem_keypair_st FP.Frodo976 FP.SHAKE128
let crypto_kem_keypair pk sk =
  crypto_kem_keypair FP.Frodo976 FP.SHAKE128 pk sk

val crypto_kem_enc: crypto_kem_enc_st FP.Frodo976 FP.SHAKE128
val crypto_kem_enc: crypto_kem_enc_st FP.Frodo976 FP.SHAKE128
Hacl.Frodo.KEM.crypto_kem_enc_st Spec.Frodo.Params.Frodo976 Spec.Frodo.Params.SHAKE128