let crypto_kem_dec_st (a:FP.frodo_alg) (gen_a:FP.frodo_gen_a{is_supported gen_a}) =
    ss:lbytes (crypto_bytes a)
  -> ct:lbytes (crypto_ciphertextbytes a)
  -> sk:lbytes (crypto_secretkeybytes a)
  -> Stack uint32
    (requires fun h ->
      live h ss /\ live h ct /\ live h sk /\
      disjoint ss ct /\ disjoint ss sk /\ disjoint ct sk)
    (ensures  fun h0 r h1 -> modifies (loc ss) h0 h1 /\
      as_seq h1 ss == S.crypto_kem_dec a gen_a (as_seq h0 ct) (as_seq h0 sk))
let crypto_kem_dec_st (a: FP.frodo_alg) (gen_a: FP.frodo_gen_a{is_supported gen_a}) =

    ss: lbytes (crypto_bytes a) ->
    ct: lbytes (crypto_ciphertextbytes a) ->
    sk: lbytes (crypto_secretkeybytes a)
  -> Stack uint32
      (requires
        fun h ->
          live h ss /\ live h ct /\ live h sk /\ disjoint ss ct /\ disjoint ss sk /\ disjoint ct sk)
      (ensures
        fun h0 r h1 ->
          modifies (loc ss) h0 h1 /\
          as_seq h1 ss == S.crypto_kem_dec a gen_a (as_seq h0 ct) (as_seq h0 sk))
Hacl.Frodo.KEM.fst.checked
Spec.Frodo.Params.fst.checked Spec.Frodo.KEM.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.Matrix.fst.checked Hacl.Impl.Frodo.Params.fst.checked Hacl.Impl.Frodo.KEM.KeyGen.fst.checked Hacl.Impl.Frodo.KEM.Encaps.fst.checked Hacl.Impl.Frodo.KEM.Decaps.fst.checked Hacl.Impl.Frodo.KEM.fst.checked Hacl.Frodo.Random.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Frodo.KEM.fst
Spec.Frodo.Params.frodo_alg Spec.Frodo.Params.frodo_gen_a Prims.b2t Hacl.Impl.Frodo.Params.is_supported Hacl.Impl.Matrix.lbytes Hacl.Impl.Frodo.Params.crypto_bytes Hacl.Impl.Frodo.Params.crypto_ciphertextbytes Hacl.Impl.Frodo.Params.crypto_secretkeybytes Lib.IntTypes.uint32 FStar.Monotonic.HyperStack.mem Prims.l_and Lib.Buffer.live Lib.Buffer.MUT Lib.IntTypes.uint8 Lib.Buffer.disjoint Lib.Buffer.modifies Lib.Buffer.loc Prims.eq2 Lib.Sequence.seq Prims.l_or Prims.nat FStar.Seq.Base.length Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.Frodo.Params.crypto_bytes Lib.Buffer.as_seq Spec.Frodo.KEM.crypto_kem_dec
module Hacl.Frodo.KEM

open FStar.HyperStack
open FStar.HyperStack.ST

open Lib.IntTypes
open Lib.Buffer

open Hacl.Impl.Matrix
open Hacl.Impl.Frodo.Params
open Hacl.Impl.Frodo.KEM
open Hacl.Frodo.Random

module S = Spec.Frodo.KEM
module FP = Spec.Frodo.Params

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

inline_for_extraction noextract
let crypto_kem_keypair_st (a:FP.frodo_alg) (gen_a:FP.frodo_gen_a{is_supported gen_a}) =
    pk:lbytes (crypto_publickeybytes a)
  -> sk:lbytes (crypto_secretkeybytes a)
  -> Stack uint32
    (requires fun h ->
      live h pk /\ live h sk /\
      disjoint pk sk /\ disjoint state pk /\ disjoint state sk)
    (ensures  fun h0 r h1 -> modifies (loc state |+| (loc pk |+| loc sk)) h0 h1 /\
      (as_seq h1 pk, as_seq h1 sk) == S.crypto_kem_keypair a gen_a (as_seq h0 state))


inline_for_extraction noextract
val crypto_kem_keypair: a:FP.frodo_alg -> gen_a:FP.frodo_gen_a{is_supported gen_a} -> crypto_kem_keypair_st a gen_a
let crypto_kem_keypair a gen_a pk sk =
  Hacl.Impl.Frodo.KEM.KeyGen.crypto_kem_keypair a gen_a pk sk


inline_for_extraction noextract
let crypto_kem_enc_st (a:FP.frodo_alg) (gen_a:FP.frodo_gen_a{is_supported gen_a}) =
    ct:lbytes (crypto_ciphertextbytes a)
  -> ss:lbytes (crypto_bytes a)
  -> pk:lbytes (crypto_publickeybytes a)
  -> Stack uint32
    (requires fun h ->
      live h ct /\ live h ss /\ live h pk /\
      disjoint ct ss /\ disjoint ct pk /\ disjoint ss pk /\
      disjoint state ct /\ disjoint state ss /\ disjoint state pk)
    (ensures  fun h0 _ h1 -> modifies (loc state |+| (loc ct |+| loc ss)) h0 h1 /\
      (as_seq h1 ct, as_seq h1 ss) == S.crypto_kem_enc a gen_a (as_seq h0 state) (as_seq h0 pk))


inline_for_extraction noextract
val crypto_kem_enc: a:FP.frodo_alg -> gen_a:FP.frodo_gen_a{is_supported gen_a} -> crypto_kem_enc_st a gen_a
let crypto_kem_enc a gen_a ct ss pk =
  Hacl.Impl.Frodo.KEM.Encaps.crypto_kem_enc a gen_a ct ss pk


inline_for_extraction noextract
val crypto_kem_dec_st : a: Spec.Frodo.Params.frodo_alg ->
    gen_a: Spec.Frodo.Params.frodo_gen_a{Hacl.Impl.Frodo.Params.is_supported gen_a}
  -> Type0

    a: Spec.Frodo.Params.frodo_alg ->
    gen_a: Spec.Frodo.Params.frodo_gen_a{Hacl.Impl.Frodo.Params.is_supported gen_a}
  -> Type0