let blake2s_128_no_key_alloca =
  F.alloca (blake2s_128 0) () (s Spec.Blake2S M128) (empty_key Spec.Blake2S)
let blake2s_128_no_key_alloca =
F.alloca (blake2s_128 0) () (s Spec.Blake2S M128) (empty_key Spec.Blake2S)
Hacl.Streaming.Blake2s_128.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.Blake2s_128.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Hacl.Streaming.Blake2s_128.fst
Hacl.Streaming.Functor.alloca Prims.unit Hacl.Streaming.Blake2s_128.blake2s_128 Hacl.Streaming.Blake2.s Spec.Blake2.Blake2S Hacl.Impl.Blake2.Core.M128 Hacl.Streaming.Blake2.empty_key
module Hacl.Streaming.Blake2s_128

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

module Spec = Spec.Blake2
open Hacl.Impl.Blake2.Core
open Hacl.Streaming.Blake2
module Blake2s128 = Hacl.Blake2s_128

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

/// The functor
inline_for_extraction noextract
let blake2s_128 kk =
  blake2 Spec.Blake2S M128 kk Blake2s128.blake2s_init Blake2s128.blake2s_update_multi
         Blake2s128.blake2s_update_last Blake2s128.blake2s_finish

/// Type abbreviations
let blake2s_128_block_state = s Spec.Blake2S M128
let blake2s_128_state = F.state_s (blake2s_128 0) () (s Spec.Blake2S M128) (empty_key Spec.Blake2S)

/// No key
inline_for_extraction noextract
val blake2s_128_no_key_alloca : Hacl.Streaming.Functor.alloca_st (Hacl.Streaming.Blake2s_128.blake2s_128 0)
  ()
  (Hacl.Streaming.Blake2.s Spec.Blake2.Blake2S Hacl.Impl.Blake2.Core.M128)
  (Hacl.Streaming.Blake2.empty_key Spec.Blake2.Blake2S)
Hacl.Streaming.Functor.alloca_st (Hacl.Streaming.Blake2s_128.blake2s_128 0)
  ()
  (Hacl.Streaming.Blake2.s Spec.Blake2.Blake2S Hacl.Impl.Blake2.Core.M128)
  (Hacl.Streaming.Blake2.empty_key Spec.Blake2.Blake2S)