val tls_mac (a: tls_macAlg) (k: hkey a) (msg: macable)
    : ST (tag a)
      (requires fun h0 -> True)
      (ensures fun h0 t h1 -> FStar.HyperStack.modifies Set.empty h0 h1)
val tls_mac (a: tls_macAlg) (k: hkey a) (msg: macable)
    : ST (tag a)
      (requires fun h0 -> True)
      (ensures fun h0 t h1 -> FStar.HyperStack.modifies Set.empty h0 h1)
let tls_mac: a:
  tls_macAlg ->
  k: hkey a  ->
  msg:macable ->
  ST (tag a)
  (requires fun h0 -> True)
  (ensures fun h0 t h1 -> FStar.HyperStack.modifies Set.empty h0 h1) =
  hmac
module MiTLS.HMAC

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

open FStar.HyperStack.ST

let ha = a:EverCrypt.HMAC.supported_alg{Spec.Hash.Definitions.is_md a}

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

val hmac:
  a:ha ->
  k:hkey a ->
  m:macable a ->
  Stack (tag a)
  (requires fun h0 -> True)
  (ensures fun h0 t h1 ->
    modifies_none h0 h1 /\
    t = Hashing.Spec.hmac a k m)

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))

(*** Old TLS 1.2 HMAC ***)

/// Agile bytes-friendly MAC function

type macable = b:Bytes.bytes {Bytes.length b + 128 < pow2 32} // [==> pre of hmac for all algorithms]
/
Spec.Hash.Definitions.fst.checked prims.fst.checked MiTLS.Mem.fst.checked MiTLS.Hashing.Spec.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked EverCrypt.HMAC.fsti.checked
MiTLS.HMAC.fsti
a: MiTLS.Hashing.Spec.tls_macAlg -> k: MiTLS.Hashing.Spec.hkey a -> msg: MiTLS.HMAC.macable
  -> FStar.HyperStack.ST.ST (MiTLS.Hashing.Spec.tag a)
MiTLS.HMAC.hmac
let tls_mac: a: tls_macAlg -> k: hkey a -> msg: macable
  -> ST (tag a)
      (requires fun h0 -> True)
      (ensures fun h0 t h1 -> FStar.HyperStack.modifies Set.empty h0 h1) =
  
hmac