Content - 890d7ad094c74df00f61e19bd41cd5bd35df571f - c601cc8/code/hash/Hacl.Hash.MD.fsti

visit type:

Tip revision: d1028e9562cad77bdb2376b985a1bea46294116c authored by Aseem Rastogi on 01 April 2019, 09:22:14 UTC
Merge branch 'fstar-master' into _aseem_merkle_tree

Tip revision: d1028e9

Hacl.Hash.MD.fsti

module Hacl.Hash.MD

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

noextract inline_for_extraction
val mk_update_multi: a:hash_alg -> update:update_st a -> update_multi_st a

noextract inline_for_extraction
val mk_update_last: a:hash_alg -> update_multi_st a -> pad_st a -> update_last_st a

noextract inline_for_extraction
val mk_hash: a:hash_alg ->
  alloca:alloca_st a ->
  update_multi:update_multi_st a ->
  update_last:update_last_st a ->
  finish:finish_st a ->
  hash_st a

Browse the archive

https://github.com/project-everest/hacl-star