val legacy_hash: hash_st MD5
let legacy_hash: hash_st MD5 =
  Hacl.Hash.MD.mk_hash MD5 legacy_alloca legacy_update_multi legacy_update_last legacy_finish
val legacy_hash: hash_st MD5
let legacy_hash:hash_st MD5 =
Hacl.Hash.MD.mk_hash MD5 legacy_alloca legacy_update_multi legacy_update_last legacy_finish
Hacl.Hash.MD5.fst.checked
Spec.Hash.Definitions.fst.checked prims.fst.checked Hacl.Hash.MD.fst.checked Hacl.Hash.Definitions.fst.checked Hacl.Hash.Core.MD5.fsti.checked FStar.Pervasives.fsti.checked
Hacl.Hash.MD5.fst
Hacl.Hash.MD.mk_hash Spec.Hash.Definitions.MD5 Hacl.Hash.Core.MD5.legacy_alloca Hacl.Hash.MD5.legacy_update_multi Hacl.Hash.MD5.legacy_update_last Hacl.Hash.Core.MD5.legacy_finish Hacl.Hash.Definitions.hash_st
module Hacl.Hash.MD5

open Hacl.Hash.Definitions
open Spec.Hash.Definitions

include Hacl.Hash.Core.MD5

friend Hacl.Hash.MD

let legacy_update_multi: update_multi_st (|MD5, ()|) =
  Hacl.Hash.MD.mk_update_multi MD5 legacy_update

let legacy_update_last: update_last_st (|MD5, ()|) =
  Hacl.Hash.MD.mk_update_last MD5 legacy_update_multi legacy_pad
val legacy_hash: hash_st MD5
Hacl.Hash.Definitions.hash_st Spec.Hash.Definitions.MD5