Content - 213e145d3114e5d04605e5861b68d0af376bef59 - 43b5f09/code/hash/Hacl.Hash.Core.MD5.fsti

visit type:

Tip revision: e00b7b9e4921939271a7816084e6a12b7110757f authored by Christoph M. Wintersteiger on 18 September 2020, 10:45:48 UTC
Enable -O2 for Merkle tree benchmarks in debug mode to enable tail-call optimization (avoids stack exhaustion).

Tip revision: e00b7b9

Hacl.Hash.Core.MD5.fsti

module Hacl.Hash.Core.MD5

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

noextract inline_for_extraction
val legacy_alloca: alloca_st (|MD5, ()|)
val legacy_init: init_st (|MD5, ()|)
val legacy_update: update_st (|MD5, ()|)
val legacy_pad: pad_st MD5
val legacy_finish: finish_st (|MD5, ()|)

Browse the archive

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