val leak: #i:id -> #good: (bytes -> Type) -> k:key i good {~(authId i)} -> Tot (kv:keyrepr i { kv = keyval k })
val leak: #i:id -> #good: (bytes -> Type) -> k:key i good {~(authId i)} -> Tot (kv:keyrepr i { kv = keyval k })
let leak   #i #good k = k.kv
(**
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 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 entry (i:id) (good: bytes -> Type0) : Type0 =
  | Entry: t:tag i -> p:bytes { authId i ==> good p } -> entry i good

#set-options "--initial_fuel 1 --max_fuel 1 --initial_ifuel 1 --max_ifuel 1 --z3rlimit 30"
let gen i good parent =
  gen0 i good parent (Random.sample32 (keysize i))

let coerce i good parent kv = gen0 i good parent kv
/
Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.Random.fst.checked MiTLS.Mem.fst.checked MiTLS.HMAC.fsti.checked MiTLS.Hashing.Spec.fst.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.fst
k: MiTLS.Old.HMAC.UFCMA.key i good {~(MiTLS.Old.HMAC.UFCMA.authId i)}
  -> kv: MiTLS.Old.HMAC.UFCMA.keyrepr i {kv = MiTLS.Old.HMAC.UFCMA.keyval k}
MiTLS.Old.HMAC.UFCMA.id FStar.Bytes.bytes MiTLS.Old.HMAC.UFCMA.key Prims.l_not Prims.b2t MiTLS.Old.HMAC.UFCMA.authId MiTLS.Old.HMAC.UFCMA.__proj__Key__item__kv MiTLS.Old.HMAC.UFCMA.keyrepr Prims.op_Equality MiTLS.Old.HMAC.UFCMA.keyval
let leak #i #good k =
  
k.kv