Revision 3bedacece9b9474403d3bf7b329f30fe291fcea8 authored by Benjamin Beurdouche on 15 April 2018, 09:25:43 UTC, committed by Benjamin Beurdouche on 15 April 2018, 09:25:43 UTC
1 parent 6b6ba23
Spec.SHA512.fst
module Spec.SHA512
module ST = FStar.HyperStack.ST
open Spec.SHA2_512
#reset-options "--max_fuel 0 --z3rlimit 20"
let k = k
let h_0 = h_0
let update h b = update h b
let update_multi h b = update_multi h b
let update_last h l i = update_last h l i
let finish h = finish h
let hash s = hash s
Computing file changes ...