val hmacVerify: a:ha -> k:hkey a -> m:macable a -> t: tag a -> ST (b:bool {b <==> (t == Hashing.Spec.hmac a k m)})
  (requires (fun h0 -> True))
  (ensures (fun h0 t h1 -> FStar.HyperStack.modifies Set.empty h0 h1))
val hmacVerify: a:ha -> k:hkey a -> m:macable a -> t: tag a -> ST (b:bool {b <==> (t == Hashing.Spec.hmac a k m)})
  (requires (fun h0 -> True))
  (ensures (fun h0 t h1 -> FStar.HyperStack.modifies Set.empty h0 h1))
let hmacVerify a k p t =
  let result = hmac a k p in
  result = t
﻿module MiTLS.HMAC

open MiTLS.Hashing.Spec // for the algorithm names, instead of CoreCrypt
open MiTLS.Mem
friend Lib.IntTypes

open FStar.HyperStack.ST

#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 20"

(* Parametric keyed HMAC; could be coded up from two HASH calls. *)

let hmac a k m =
  let h00 = get() in
  push_frame();
  let lt = Hacl.Hash.Definitions.hash_len a in
  let lk = Bytes.len k in
  let bk = LowStar.Buffer.alloca 0uy lk in
  Bytes.store_bytes k bk;
  let bt = LowStar.Buffer.alloca 0uy lt in
  let lm = Bytes.len m in

  if lm = 0ul then (
    let bm = LowStar.Buffer.null in
    let h0 = get() in
    Seq.lemma_eq_intro (Bytes.reveal m) (LowStar.Buffer.as_seq h0 bm);
    EverCrypt.HMAC.compute a bt bk lk bm lm
  )
  else (
    let h0 = get() in
    push_frame();
    let bm = LowStar.Buffer.alloca 0uy lm in
    Bytes.store_bytes m bm;
    EverCrypt.HMAC.compute a bt bk lk bm lm;
    pop_frame();
    let h1 = get() in
    assert(LowStar.Modifies.(modifies (loc_buffer bt) h0 h1))
    );

  let t = Bytes.of_buffer lt bt in
  Hacl.HMAC.key_and_data_fits a;
  assert(Bytes.reveal t == Spec.Agile.HMAC.hmac a (Bytes.reveal k) (Bytes.reveal m));
  assert(t = Hashing.Spec.hmac a k m);
  pop_frame();
  let h11 = HyperStack.ST.get() in
  //18-09-01 todo, as in Hashing.compute
  assert(LowStar.Modifies.(modifies loc_none h00 h11));
  assume(modifies_none h00 h11); //18-09-12 missing compatibility lemma?
  t

//18-09-02 TODO lower code to avoid bytes-allocating the tag.
/
Spec.Agile.HMAC.fsti.checked prims.fst.checked MiTLS.Mem.fst.checked MiTLS.Hashing.Spec.fst.checked LowStar.Modifies.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fst.checked Hacl.HMAC.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.Bytes.fsti.checked EverCrypt.HMAC.fsti.checked
MiTLS.HMAC.fst

    a: MiTLS.HMAC.ha ->
    k: MiTLS.Hashing.Spec.hkey a ->
    m: MiTLS.Hashing.Spec.macable a ->
    t: MiTLS.Hashing.Spec.tag a
  -> FStar.HyperStack.ST.ST (b: Prims.bool{b <==> t == MiTLS.Hashing.Spec.hmac a k m})
MiTLS.HMAC.ha MiTLS.Hashing.Spec.hkey MiTLS.Hashing.Spec.macable MiTLS.Hashing.Spec.tag Prims.op_Equality Prims.bool Prims.l_iff Prims.b2t Prims.eq2 MiTLS.Hashing.Spec.hmac MiTLS.HMAC.hmac
let hmacVerify a k p t =
  
let result = hmac a k p in
result = t