val alg (i: id) : HMAC.ha
val alg (i: id) : HMAC.ha
let alg (i:id) : HMAC.ha = match i with
| HMAC_Finished i -> TLSInfo.finishedId_hash i
| HMAC_Binder i -> TLSInfo.binderId_hash 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
/
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 -> MiTLS.HMAC.ha
MiTLS.Old.HMAC.UFCMA.id MiTLS.Old.HMAC.UFCMA.finishedId MiTLS.TLSInfo.finishedId_hash MiTLS.Old.HMAC.UFCMA.binderId MiTLS.TLSInfo.binderId_hash MiTLS.HMAC.ha
let alg (i: id) : HMAC.ha =
  
match i with
| HMAC_Finished i -> TLSInfo.finishedId_hash i
| HMAC_Binder i -> TLSInfo.binderId_hash i