val keysize : i: MiTLS.Old.HMAC.UFCMA.id
  -> n:
    Lib.IntTypes.size_t
      {Lib.IntTypes.v n = Spec.Hash.Definitions.hash_length (MiTLS.Old.HMAC.UFCMA.alg i)}
let keysize (i:id) = Hacl.Hash.Definitions.hash_len (alg i)
(**
Idealizing HMAC for Finished message payloads and binders.
*)
module MiTLS.Old.HMAC.UFCMA
open MiTLS

open FStar.Heap
open FStar.HyperStack
open FStar.HyperStack.All
open FStar.Seq
open FStar.Bytes
open FStar.Error

open MiTLS.Mem
open MiTLS.TLSError
open MiTLS.TLSInfo

module HS = FStar.HyperStack

// idealizing HMAC
// for concreteness; the rest of the module is parametric in a:alg

#set-options "--initial_fuel 1 --max_fuel 1 --initial_ifuel 1 --max_ifuel 1"

type finishedId = i:pre_finishedId{valid (I_FINISHED i)}
type binderId = i:pre_binderId{valid (I_BINDER i)}
type hsId = i:pre_hsId{valid (I_HS i)}
type asId = i:pre_asId{valid (I_AS i)}

type id =
| HMAC_Finished of finishedId
| HMAC_Binder of binderId

let alg (i:id) : HMAC.ha = match i with
| HMAC_Finished i -> TLSInfo.finishedId_hash i
| HMAC_Binder i -> TLSInfo.binderId_hash i

//assume
let authId (_:id) : Tot bool = false  // TODO: move to Flags

type text = bytes
type tag (i:id) = lbytes32 (Hacl.Hash.Definitions.hash_len (alg i))
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.Mem.fst.checked MiTLS.HMAC.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.Old.HMAC.UFCMA.fsti
i: MiTLS.Old.HMAC.UFCMA.id
  -> n:
    Lib.IntTypes.size_t
      {Lib.IntTypes.v n = Spec.Hash.Definitions.hash_length (MiTLS.Old.HMAC.UFCMA.alg i)}
MiTLS.Old.HMAC.UFCMA.id Hacl.Hash.Definitions.hash_len MiTLS.Old.HMAC.UFCMA.alg Lib.IntTypes.size_t Prims.b2t Prims.op_Equality Prims.int Prims.l_or Lib.IntTypes.range Lib.IntTypes.U32 Prims.l_and Prims.op_GreaterThanOrEqual Prims.op_LessThanOrEqual Lib.IntTypes.max_size_t Prims.op_GreaterThan Lib.IntTypes.v Lib.IntTypes.PUB Spec.Hash.Definitions.hash_length
let keysize (i: id) =
  
Hacl.Hash.Definitions.hash_len (alg i)