module Hacl.HMAC.SHA2_512
open FStar.Mul
open FStar.Ghost
open FStar.HyperStack
open FStar.HyperStack.All
open FStar.HyperStack.ST
open FStar.Buffer
open FStar.UInt32
module ST = FStar.HyperStack.ST
module Hash = Hacl.Impl.SHA2_512
module Spec = Spec.HMAC.SHA2_512
module HMAC = Hacl.Impl.HMAC.SHA2_512
(* Definition of base types *)
private let uint8_ht = Hacl.UInt8.t
private let uint32_t = FStar.UInt32.t
private let uint8_p = Buffer.buffer uint8_ht
//
// HMAC
//
#reset-options "--max_fuel 0 --z3rlimit 25"
val hmac_core:
mac :uint8_p {length mac = v Hash.size_hash} ->
key :uint8_p {length key = v Hash.size_block /\ disjoint key mac} ->
data :uint8_p {length data + v Hash.size_block < pow2 32 /\ disjoint data mac /\ disjoint data key} ->
len :uint32_t {length data = v len} ->
Stack unit
(requires (fun h -> live h mac /\ live h key /\ live h data))
(ensures (fun h0 _ h1 -> live h1 mac /\ live h0 mac
/\ live h1 key /\ live h0 key
/\ live h1 data /\ live h0 data /\ modifies_1 mac h0 h1
/\ (as_seq h1 mac == Spec.hmac_core (as_seq h0 key) (as_seq h0 data))))
#reset-options "--max_fuel 0 --z3rlimit 10"
let hmac_core mac key data len = HMAC.hmac_core mac key data len
//
//
#reset-options "--max_fuel 0 --z3rlimit 25"
val hmac:
mac :uint8_p {length mac = v Hash.size_hash} ->
key :uint8_p {length key = v Hash.size_block /\ disjoint key mac} ->
keylen :uint32_t {v keylen = length key} ->
data :uint8_p {length data + v Hash.size_block < pow2 32 /\ disjoint data mac /\ disjoint data key} ->
datalen :uint32_t {v datalen = length data} ->
Stack unit
(requires (fun h -> live h mac /\ live h key /\ live h data))
(ensures (fun h0 _ h1 -> live h1 mac /\ live h0 mac
/\ live h1 key /\ live h0 key
/\ live h1 data /\ live h0 data /\ modifies_1 mac h0 h1
/\ (as_seq h1 mac == Spec.hmac (as_seq h0 key) (as_seq h0 data))))
#reset-options "--max_fuel 0 --z3rlimit 10"
let hmac mac key keylen data datalen = HMAC.hmac mac key keylen data datalen