val blake2b_update_blocks:Impl.blake2_update_blocks_st Spec.Blake2B Core.M256
let blake2b_update_blocks : Impl.blake2_update_blocks_st Spec.Blake2B Core.M256 =
  Impl.blake2_update_blocks #Spec.Blake2B #Core.M256 blake2b_update_multi blake2b_update_last
val blake2b_update_blocks:Impl.blake2_update_blocks_st Spec.Blake2B Core.M256
let blake2b_update_blocks:Impl.blake2_update_blocks_st Spec.Blake2B Core.M256 =
Impl.blake2_update_blocks #Spec.Blake2B #Core.M256 blake2b_update_multi blake2b_update_last
Hacl.Blake2b_256.fst.checked
Spec.Blake2.fst.checked prims.fst.checked Hacl.Impl.Blake2.Generic.fst.checked Hacl.Impl.Blake2.Core.fsti.checked FStar.Pervasives.fsti.checked
Hacl.Blake2b_256.fst
Hacl.Impl.Blake2.Generic.blake2_update_blocks Spec.Blake2.Blake2B Hacl.Impl.Blake2.Core.M256 Hacl.Blake2b_256.blake2b_update_multi Hacl.Blake2b_256.blake2b_update_last
module Hacl.Blake2b_256

module Spec = Spec.Blake2
module Impl = Hacl.Impl.Blake2.Generic
module Core = Hacl.Impl.Blake2.Core

(* Some specialized components of blake2 *)
[@CInline]
private
let blake2b_update_block : Impl.blake2_update_block_st Spec.Blake2B Core.M256 =
  Impl.blake2_update_block #Spec.Blake2B #Core.M256

let blake2b_init : Impl.blake2_init_st Spec.Blake2B Core.M256 =
  Impl.blake2_init #Spec.Blake2B #Core.M256

let blake2b_update_key : Impl.blake2_update_key_st Spec.Blake2B Core.M256 =
  Impl.blake2_update_key #Spec.Blake2B #Core.M256 blake2b_update_block

let blake2b_update_multi : Impl.blake2_update_multi_st Spec.Blake2B Core.M256 =
  Impl.blake2_update_multi #Spec.Blake2B #Core.M256 blake2b_update_block

let blake2b_update_last : Impl.blake2_update_last_st Spec.Blake2B Core.M256 =
  Impl.blake2_update_last #Spec.Blake2B #Core.M256 blake2b_update_block

[@CInline]
private
val blake2b_update_blocks:Impl.blake2_update_blocks_st Spec.Blake2B Core.M256
Hacl.Impl.Blake2.Generic.blake2_update_blocks_st Spec.Blake2.Blake2B Hacl.Impl.Blake2.Core.M256