val secret_len (a: info) : keylen
val secret_len (a: info) : keylen
let secret_len (a:info) : keylen = Hacl.Hash.Definitions.hash_len a.ha
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

noextract
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

let valid_info (i0:id) (v:info) =
  if model then v == index_info i0 else True

type info0 (i:id) = u:info{valid_info i u}
type iflag = b:bool{b ==> model}
type usage (ideal:iflag) = children (b2t ideal)

unfold type regid = i:(Idx?.t ii){(Idx?.registered ii) i}

let derived_key
  (#ideal:iflag)
  (u: usage ideal)
  (i: regid)
  (lbl: label {u `has_lbl` lbl})
  (ctx: context)
  : Pure Type0
  (requires wellformed_derive i lbl ctx /\
    registered (derive i lbl ctx) /\ model)
//    (model ==> Pkg?.key (child u lbl) == ktype))
  (ensures fun t -> True)
  =
  Pkg?.key (child u lbl) (Derive i lbl ctx)
//  (Pkg?.key (child u lbl)) (Derive i lbl ctx)

let kdf_tables_region : tls_rgn = new_region Mem.tls_tables_region

/// key-derivation table (memoizing create/coerce)
noextract
type domain (#ideal:iflag) (u:usage ideal) (i:regid) : eqtype =
| Domain:
  lbl: label {u `has_lbl` lbl} ->
  ctx: context {wellformed_derive i lbl ctx /\ registered (derive i lbl ctx)} ->
  domain u i

noextract
let kdf_range (#ideal:iflag) (u:usage ideal) (i:regid{model}) (d:domain u i) =
  (let Domain lbl ctx = d in derived_key u i lbl ctx)

noextract
noeq private type table (#ideal:iflag) (u:usage ideal) (i:regid) (s:squash model) =
  | KDF_table:
    r:subrgn kdf_tables_region ->
    t:MDM.t r (domain u i) (kdf_range u i) (fun _ -> True) ->
    table u i s
/
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
a: MiTLS.KDF.info -> MiTLS.Pkg.keylen
MiTLS.KDF.info Hacl.Hash.Definitions.hash_len MiTLS.KDF.__proj__Info__item__ha MiTLS.Pkg.keylen
let secret_len (a: info) : keylen =
  
Hacl.Hash.Definitions.hash_len a.ha