val coerce: i:id -> good: (bytes -> Type) -> parent: rgn -> kv:keyrepr i -> ST(key i good)
  (requires (fun _ -> ~(authId i)))
  (ensures (fun h0 k h1 ->
    modifies Set.empty h0 h1 /\
    fresh_subregion (region #i #good k) parent h0 h1 ))
val coerce: i:id -> good: (bytes -> Type) -> parent: rgn -> kv:keyrepr i -> ST(key i good)
  (requires (fun _ -> ~(authId i)))
  (ensures (fun h0 k h1 ->
    modifies Set.empty h0 h1 /\
    fresh_subregion (region #i #good k) parent h0 h1 ))
let coerce i good parent kv = gen0 i good parent 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))
/
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

    i: MiTLS.Old.HMAC.UFCMA.id ->
    good: (_: FStar.Bytes.bytes -> Type0) ->
    parent: MiTLS.Mem.rgn ->
    kv: MiTLS.Old.HMAC.UFCMA.keyrepr i
  -> FStar.HyperStack.ST.ST (MiTLS.Old.HMAC.UFCMA.key i good)
MiTLS.Old.HMAC.UFCMA.id FStar.Bytes.bytes MiTLS.Mem.rgn MiTLS.Old.HMAC.UFCMA.keyrepr MiTLS.Old.HMAC.UFCMA.gen0 MiTLS.Old.HMAC.UFCMA.key
let coerce i good parent kv =
  
gen0 i good parent kv