Revision 1990ae634d0602ff022afc946ef66933e4e4a2dc authored by Santiago Zanella-Beguelin on 09 December 2019, 17:48:55 UTC, committed by Santiago Zanella-Beguelin on 09 December 2019, 17:50:10 UTC
1 parent ae8e182
Spec.Agile.HMAC.fsti
module Spec.Agile.HMAC
open Spec.Hash.Definitions
open Lib.IntTypes
#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 50"
let is_supported_alg = function
| SHA1 | SHA2_256 | SHA2_384 | SHA2_512 -> true
| _ -> false
let lbytes (l:nat) = b:bytes {Seq.length b = l}
let keysized (a:hash_alg) (l:nat) =
l <= max_input_length a /\
l + block_length a < pow2 32
val hmac:
a: hash_alg ->
key: bytes ->
data: bytes ->
Pure (lbytes (hash_length a))
(requires keysized a (Seq.length key) /\
Seq.length data + block_length a <= max_input_length a)
(ensures fun _ -> True)
Computing file changes ...
