let blake2b_256 kk =
  blake2 Spec.Blake2B M256 kk Blake2b256.blake2b_init Blake2b256.blake2b_update_multi
         Blake2b256.blake2b_update_last Blake2b256.blake2b_finish
let blake2b_256 kk =
blake2 Spec.Blake2B
  M256
  kk
  Blake2b256.blake2b_init
  Blake2b256.blake2b_update_multi
  Blake2b256.blake2b_update_last
  Blake2b256.blake2b_finish
Hacl.Streaming.Blake2b_256.fst.checked
Spec.Blake2.fst.checked prims.fst.checked Hacl.Streaming.Functor.fsti.checked Hacl.Streaming.Blake2.fst.checked Hacl.Impl.Blake2.Core.fsti.checked Hacl.Blake2b_256.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Hacl.Streaming.Blake2b_256.fst
Hacl.Streaming.Blake2.key_size Spec.Blake2.Blake2B Hacl.Streaming.Blake2.blake2 Hacl.Impl.Blake2.Core.M256 Hacl.Blake2b_256.blake2b_init Hacl.Blake2b_256.blake2b_update_multi Hacl.Blake2b_256.blake2b_update_last Hacl.Blake2b_256.blake2b_finish Hacl.Streaming.Interface.block Prims.unit
module Hacl.Streaming.Blake2b_256

module G = FStar.Ghost
module F = Hacl.Streaming.Functor

module Spec = Spec.Blake2
open Hacl.Impl.Blake2.Core
open Hacl.Streaming.Blake2
module Blake2b256 = Hacl.Blake2b_256

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

/// The functor
inline_for_extraction noextract
val blake2b_256 : kk: Hacl.Streaming.Blake2.key_size Spec.Blake2.Blake2B -> Hacl.Streaming.Interface.block Prims.unit
kk: Hacl.Streaming.Blake2.key_size Spec.Blake2.Blake2B -> Hacl.Streaming.Interface.block Prims.unit