val extract (#ha: Hashing.Spec.tls_macAlg) (salt: hkey ha) (ikm: macable ha)
    : ST (hkey ha)
      (requires (fun h0 -> True))
      (ensures (fun h0 t h1 -> FStar.HyperStack.modifies Set.empty h0 h1))
val extract (#ha: Hashing.Spec.tls_macAlg) (salt: hkey ha) (ikm: macable ha)
    : ST (hkey ha)
      (requires (fun h0 -> True))
      (ensures (fun h0 t h1 -> FStar.HyperStack.modifies Set.empty h0 h1))
let extract:
  #ha: Hashing.Spec.tls_macAlg ->
  salt: hkey ha ->
  ikm: macable ha ->
  ST (hkey ha)
  (requires (fun h0 -> True))
  (ensures (fun h0 t h1 -> FStar.HyperStack.modifies Set.empty h0 h1))
  = fun #ha salt ikm -> HMAC.hmac ha salt ikm
(**
TLS 1.3 HKDF extract and expand constructions, parametrized by their hash algorithm
*)
module MiTLS.HKDF
open MiTLS

open MiTLS.Mem

open FStar.UInt32
// open FStar.Integers
// 18-09-24 still triggering extraction error

open MiTLS.Hashing.Spec
open FStar.Bytes

(*-------------------------------------------------------------------*)
(*
From https://tools.ietf.org/html/rfc5869

HKDF-Extract(salt, IKM) -> PRK
   Options:
      Hash     a hash function; HashLen denotes the length of the
               hash function output in octets
   Inputs:
      salt     optional salt value (a non-secret random value);
               if not provided, it is set to a string of HashLen zeros.
      IKM      input keying material
   Output:
      PRK      a pseudorandom key (of HashLen octets)

   PRK = HMAC-Hash(salt, IKM)
*)
/
Spec.Hash.Definitions.fst.checked prims.fst.checked MiTLS.Mem.fst.checked MiTLS.HMAC.fsti.checked MiTLS.Hashing.Spec.fst.checked MiTLS.Hashing.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked
MiTLS.HKDF.fsti
salt: MiTLS.Hashing.Spec.hkey ha -> ikm: MiTLS.Hashing.Spec.macable ha
  -> FStar.HyperStack.ST.ST (MiTLS.Hashing.Spec.hkey ha)
MiTLS.Hashing.Spec.tls_macAlg MiTLS.Hashing.Spec.hkey MiTLS.Hashing.Spec.macable MiTLS.HMAC.hmac MiTLS.Hashing.Spec.tag
let extract: #ha: Hashing.Spec.tls_macAlg -> salt: hkey ha -> ikm: macable ha
  -> ST (hkey ha)
      (requires (fun h0 -> True))
      (ensures (fun h0 t h1 -> FStar.HyperStack.modifies Set.empty h0 h1)) =
  
fun #ha salt ikm -> HMAC.hmac ha salt ikm