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
Raw File
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
back to top