Skip to main content

Browse the archive

Revision 90fb00125d71b67a48e2eeb4c554df8f94ea3188 authored by Jay Bosamiya on 31 May 2019, 23:49:31 UTC, committed by Jay Bosamiya on 31 May 2019, 23:49:31 UTC 
It should be up to caller to show equal init_rsp
1 parent df2a6de
Raw File
Spec.SHA2.fsti 
module Spec.SHA2

open Spec.Hash.Definitions

val init: a:sha2_alg -> init_t a

val update: a:sha2_alg -> update_t a

val pad: a:sha2_alg -> pad_t a

val finish: a:sha2_alg -> finish_t a
back to top