Content - 9133971888e407ee0e16fd01769318885ae7a951 - 0cb1060/code/hash/Hacl.Hash.MD.fsti

visit type:

Tip revision: 6c689597d7d7f4e81e9a40481b32f3ff32f33510 authored by Nikhil Swamy on 12 March 2021, 20:17:28 UTC
bump rlimit on lemma that is failing with an F* update

Tip revision: 6c68959

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{is_md a} -> update:update_st (|a, ()|) -> update_multi_st (|a, ()|)

noextract inline_for_extraction
val mk_update_last: a:hash_alg{is_md a} -> update_multi_st (|a, ()|) -> pad_st a -> update_last_st (|a, ()|)

noextract inline_for_extraction
val mk_hash: a:hash_alg{is_md a} ->
  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