Revision 5b2fbf3c4989a9b0587a00578f69f3041df3f957 authored by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC, committed by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC
1 parent d4ca892
Spec.Agile.Hash.fsti
module Spec.Agile.Hash
module S = FStar.Seq
include Spec.Hash.Definitions
open Spec.Hash.PadFinish
val init (a:hash_alg): init_t a
val update (a:hash_alg): update_t a
val update_multi (a:hash_alg) (hash:words_state a) (blocks:bytes_blocks a):
Tot (words_state a) (decreases (S.length blocks))
val hash (a:hash_alg) (input:bytes{S.length input <= max_input_length a}):
Tot (Lib.ByteSequence.lbytes (hash_length a))
Computing file changes ...
