val hmac:
  a:alg ->
  k:hkey a ->
  text:macable a ->
  GTot (t:tag a{
    let text = Bytes.reveal text in
    (Seq.length text + block_length a) `less_than_max_input_length` a /\
    Bytes.reveal t = Spec.Agile.HMAC.hmac a (Bytes.reveal k) text})
val hmac:
  a:alg ->
  k:hkey a ->
  text:macable a ->
  GTot (t:tag a{
    let text = Bytes.reveal text in
    (Seq.length text + block_length a) `less_than_max_input_length` a /\
    Bytes.reveal t = Spec.Agile.HMAC.hmac a (Bytes.reveal k) text})
let hmac a k text =
  let k = Bytes.reveal k in
  let text = Bytes.reveal text in
  assert_norm (pow2 32 < pow2 61);
  assert_norm (pow2 61 < pow2 125);
  //assert (Seq.length text + block_length a <= max_input_length a);
  let t: bytes_hash a = Spec.Agile.HMAC.hmac a k text in
  Bytes.hide t
﻿(** hash algorithms and providers

 * provides bytes-friendly API before idealization
 * no dependency on TLS: could go to EverCrypt or SecureAPI.

*)
module MiTLS.Hashing.Spec
open MiTLS

include EverCrypt.Hash
include Spec.Hash.Definitions

open FStar.Bytes

open MiTLS.Declassify

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

let alg = a:alg { is_md a }

let hash_len (a:alg)
  : n:UInt32.t{UInt32.v n == hash_length a}
  = Hacl.Hash.Definitions.hash_len a

type tag (a:alg) = Bytes.lbytes (hash_length a)

let max_hash_length = 64
let max_hash_len = 64ul
type anyTag = lbytes max_hash_length

let max_block_length = 128
let max_block_len = 128ul

private let lemma_tagLen (a:alg)
  : Lemma (hash_length a <= max_hash_length)
  [SMTPat (hash_length a)]
  = ()

private let lemma_blockLength (a:alg)
  : Lemma (block_length a <= max_block_length)
  [SMTPat (block_length a)]
  = ()

let macable a = b:bytes {length b + block_length a < pow2 32}
// 32-bit implementation restriction

// Adapting EverCrypt's HMAC specification to TLS. In contrast with
// RFC 2104 (which take any key length), in TLS, the HMAC key has the
// same length as the hash [TLS1.3, 4.4.3]

type hkey (a:alg) = b:bytes{
  // 18-09-12 this usage restriction is dubious, but always met in
  // miTLS; it avoids a null-pointer case in the wrapper below.
  length b > 0 /\
  Spec.Agile.HMAC.keysized a (length b)}

val hmac:
  a:alg ->
  k:hkey a ->
  text:macable a ->
  GTot (t:tag a{
    let text = Bytes.reveal text in
    (Seq.length text + block_length a) `less_than_max_input_length` a /\
    Bytes.reveal t = Spec.Agile.HMAC.hmac a (Bytes.reveal k) text})
/
Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked prims.fst.checked MiTLS.Declassify.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked EverCrypt.HMAC.fsti.checked EverCrypt.Hash.fsti.checked
MiTLS.Hashing.Spec.fst
a: MiTLS.Hashing.Spec.alg -> k: MiTLS.Hashing.Spec.hkey a -> text: MiTLS.Hashing.Spec.macable a
  -> Prims.GTot
    (t:
      MiTLS.Hashing.Spec.tag a
        { let text = FStar.Bytes.reveal text in
          Spec.Hash.Definitions.less_than_max_input_length (FStar.Seq.Base.length text +
              Spec.Hash.Definitions.block_length a)
            a /\ FStar.Bytes.reveal t = Spec.Agile.HMAC.hmac a (FStar.Bytes.reveal k) text })
MiTLS.Hashing.Spec.alg MiTLS.Hashing.Spec.hkey MiTLS.Hashing.Spec.macable FStar.Bytes.hide Spec.Hash.Definitions.bytes_hash Spec.Agile.HMAC.hmac Prims.unit FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThan Prims.pow2 FStar.Seq.Base.seq FStar.UInt8.t FStar.Bytes.reveal MiTLS.Hashing.Spec.tag Prims.l_and Spec.Hash.Definitions.less_than_max_input_length Prims.op_Addition FStar.Seq.Base.length FStar.Bytes.byte Spec.Hash.Definitions.block_length Prims.op_Equality Lib.IntTypes.uint8
let hmac a k text =
  
let k = Bytes.reveal k in
let text = Bytes.reveal text in
assert_norm (pow2 32 < pow2 61);
assert_norm (pow2 61 < pow2 125);
let t:bytes_hash a = Spec.Agile.HMAC.hmac a k text in
Bytes.hide t