let blake2b_256_no_key_create_in =
  F.create_in (blake2b_256 0) () (s Spec.Blake2B M256) (empty_key Spec.Blake2B)
let blake2b_256_no_key_create_in =
F.create_in (blake2b_256 0) () (s Spec.Blake2B M256) (empty_key Spec.Blake2B)
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.Functor.create_in Prims.unit Hacl.Streaming.Blake2b_256.blake2b_256 Hacl.Streaming.Blake2.s Spec.Blake2.Blake2B Hacl.Impl.Blake2.Core.M256 Hacl.Streaming.Blake2.empty_key
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
let blake2b_256 kk =
  blake2 Spec.Blake2B M256 kk Blake2b256.blake2b_init Blake2b256.blake2b_update_multi
         Blake2b256.blake2b_update_last Blake2b256.blake2b_finish

/// Type abbreviations
let blake2b_256_block_state = s Spec.Blake2B M256
let blake2b_256_state = F.state_s (blake2b_256 0) () (s Spec.Blake2B M256) (empty_key Spec.Blake2B)

/// No key
inline_for_extraction noextract
let blake2b_256_no_key_alloca =
  F.alloca (blake2b_256 0) () (s Spec.Blake2B M256) (empty_key Spec.Blake2B)

[@ (Comment "  State allocation function when there is no key")]
val blake2b_256_no_key_create_in : Hacl.Streaming.Functor.create_in_st (Hacl.Streaming.Blake2b_256.blake2b_256 0)
  ()
  (Hacl.Streaming.Blake2.s Spec.Blake2.Blake2B Hacl.Impl.Blake2.Core.M256)
  (Hacl.Streaming.Blake2.empty_key Spec.Blake2.Blake2B)
Hacl.Streaming.Functor.create_in_st (Hacl.Streaming.Blake2b_256.blake2b_256 0)
  ()
  (Hacl.Streaming.Blake2.s Spec.Blake2.Blake2B Hacl.Impl.Blake2.Core.M256)
  (Hacl.Streaming.Blake2.empty_key Spec.Blake2.Blake2B)