val region (#i: id) (#good: (bytes -> Type)) (k: key i good) : GTot rid
val region (#i: id) (#good: (bytes -> Type)) (k: key i good) : GTot rid
let region (#i:id) (#good:(bytes -> Type)) (k:key i good) : GTot rid = k.region
(**
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))

let keysize (i:id) = Hacl.Hash.Definitions.hash_len (alg i)
type keyrepr (i:id) = lbytes32 (keysize i)

type fresh_subregion rg parent h0 h1 = HS.fresh_region rg h0 h1 /\ extends rg parent

// We keep the tag in case we later want to enforce tag authentication
val entry (i:id) (good: bytes -> Type0) : Type0

// readers and writers share the same private state: a log of MACed messages
// TODO make it abstract
(*
 * AR: two changes: region is of type rgn.
 * log is a hyperstack ref with refinement capturing its rid.
 *)
noeq type key (i:id) (good: bytes -> Type) =
  | Key:
    #region: rgn -> // intuitively, the writer's region
    kv: keyrepr i ->
    log: ref (seq (entry i good)){HS.frameOf log = region} ->
    key i good
/
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
k: MiTLS.Old.HMAC.UFCMA.key i good -> Prims.GTot FStar.Monotonic.HyperHeap.rid
MiTLS.Old.HMAC.UFCMA.id FStar.Bytes.bytes MiTLS.Old.HMAC.UFCMA.key MiTLS.Old.HMAC.UFCMA.__proj__Key__item__region FStar.Monotonic.HyperHeap.rid
let region (#i: id) (#good: (bytes -> Type)) (k: key i good) : GTot rid =
  
k.region