val index_info : i: MiTLS.Idx.id{MiTLS.Mem.model} -> MiTLS.KDF.info
let rec index_info (i:id{model}) =
  let i':pre_id = i in
  match i' with
  | Preshared a _ -> Info a None
  | Derive i l (ExpandLog log hv) -> Info (ha_of_id i) (Some (Log log hv))
  | Derive i _ _ -> index_info i
module MiTLS.KDF
open MiTLS

/// We define a KDF parametric in both its usage and ipkg
/// We rely on type abstraction to separate secrets with different indexes
/// For soundness, we must also prevent external calls to create derived secrets.
///
/// We idealize KDF as a random function, with lazy sampling.
/// This holds syntactically only after inlining all calls to
/// pkg.create/coerce.
///
/// This requires memoizing calls, which is a bit tricky when calling
/// stateful allocators.

open MiTLS.Mem
open MiTLS.Pkg
open MiTLS.Idx 
open MiTLS.Pkg.Tree

module MDM = FStar.Monotonic.DependentMap
module HS = FStar.HyperStack

inline_for_extraction
let sample (len:UInt32.t): ST (lbytes32 len)
    (requires fun h0 -> True)
    (ensures fun h0 r h1 -> h0 == h1)
  = assume false; Random.sample32 len

type details (ha:kdfa) =
| Log:
  loginfo: TLSInfo.logInfo ->
  hv: Hashing.Spec.anyTag {digest_info ha loginfo hv} -> details ha

type info =
| Info:
  ha:kdfa ->
  option (details ha) -> info
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.Random.fst.checked MiTLS.Pkg.Tree.fst.checked MiTLS.Pkg.fst.checked MiTLS.Model.fst.checked MiTLS.Mem.fst.checked MiTLS.Idx.fst.checked MiTLS.HKDF.fsti.checked MiTLS.Hashing.Spec.fst.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.Monotonic.DependentMap.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked
MiTLS.KDF.fst
i: MiTLS.Idx.id{MiTLS.Mem.model} -> MiTLS.KDF.info
MiTLS.Idx.id Prims.b2t MiTLS.Mem.model MiTLS.Idx.kdfa MiTLS.Idx.id_psk MiTLS.KDF.Info FStar.Pervasives.Native.None MiTLS.KDF.details MiTLS.Idx.pre_id MiTLS.Idx.label MiTLS.TLSInfo.logInfo MiTLS.Hashing.Spec.anyTag MiTLS.Idx.ha_of_id FStar.Pervasives.Native.Some MiTLS.KDF.Log MiTLS.Idx.context MiTLS.KDF.index_info MiTLS.KDF.info
let rec index_info (i: id{model}) =
  
let i':pre_id = i in
match i' with
| Preshared a _ -> Info a None
| Derive i l (ExpandLog log hv) -> Info (ha_of_id i) (Some (Log log hv))
| Derive i _ _ -> index_info i