https://github.com/project-everest/hacl-star
Raw File
Tip revision: 13e72719479807d4f437dd1424d53dfb80dbbd3b authored by Aymeric Fromherz on 31 July 2019, 08:57:48 UTC
Ed: Finish proving barrett reduction
Tip revision: 13e7271
Hacl.Hash.MD5.fst
module Hacl.Hash.MD5

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

include Hacl.Hash.Core.MD5

friend Hacl.Hash.MD

let update_multi: update_multi_st MD5 = Hacl.Hash.MD.mk_update_multi MD5 update
let update_last: update_last_st MD5 = Hacl.Hash.MD.mk_update_last MD5 update_multi pad
let hash: hash_st MD5 = Hacl.Hash.MD.mk_hash MD5 alloca update_multi update_last finish
back to top