val compute_blake2b_256:compute_st Blake2B
let compute_blake2b_256: compute_st Blake2B =
  mk_compute (D.mk_impl Blake2B Hacl.Impl.Blake2.Core.M256)
             hash_blake2b_256 alloca_blake2b_256 init_blake2b_256
             update_multi_blake2b_256 update_last_blake2b_256 finish_blake2b_256
val compute_blake2b_256:compute_st Blake2B
let compute_blake2b_256:compute_st Blake2B =
mk_compute (D.mk_impl Blake2B Hacl.Impl.Blake2.Core.M256)
  hash_blake2b_256
  alloca_blake2b_256
  init_blake2b_256
  update_multi_blake2b_256
  update_last_blake2b_256
  finish_blake2b_256
Hacl.HMAC.Blake2b_256.fst.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked Hacl.Impl.Blake2.Core.fsti.checked Hacl.HMAC.fsti.checked Hacl.Hash.Definitions.fst.checked Hacl.Hash.Blake2.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked EverCrypt.Helpers.fsti.checked
Hacl.HMAC.Blake2b_256.fst
Hacl.HMAC.mk_compute Hacl.Hash.Definitions.mk_impl Spec.Hash.Definitions.Blake2B Hacl.Impl.Blake2.Core.M256 Hacl.Hash.Blake2.hash_blake2b_256 Hacl.Hash.Blake2.alloca_blake2b_256 Hacl.Hash.Blake2.init_blake2b_256 Hacl.Hash.Blake2.update_multi_blake2b_256 Hacl.Hash.Blake2.update_last_blake2b_256 Hacl.Hash.Blake2.finish_blake2b_256
module Hacl.HMAC.Blake2b_256

module B = LowStar.Buffer
module D = Hacl.Hash.Definitions

open Spec.Agile.HMAC
open Spec.Hash.Definitions
open FStar.HyperStack.ST
open Lib.IntTypes

open EverCrypt.Helpers

open Hacl.HMAC
open Hacl.Hash.Blake2

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

[@@ Comment "Write the HMAC-BLAKE2b MAC of a message (`data`) by using a key (`key`) into `dst`.

The key can be any length and will be hashed if it is longer and padded if it is shorter than 128 bytes.
`dst` must point to 64 bytes of memory."]
val compute_blake2b_256:compute_st Blake2B
Hacl.HMAC.compute_st Spec.Hash.Definitions.Blake2B