val expand_spec:
  #ha:Hashing.alg ->
  prk: Hashing.Spec.tag ha ->
  info: bytes {Bytes.length info < 1024 (* somewhat arbitrary *) } ->
  len: UInt32.t {0 < v len /\ v len <= op_Multiply 255 (hash_length ha)} ->
  GTot (lbytes32 len)
val expand_spec:
  #ha:Hashing.alg ->
  prk: Hashing.Spec.tag ha ->
  info: bytes {Bytes.length info < 1024 (* somewhat arbitrary *) } ->
  len: UInt32.t {0 < v len /\ v len <= op_Multiply 255 (hash_length ha)} ->
  GTot (lbytes32 len)
let expand_spec = expand_spec'
(**
TLS 1.3 HKDF extract and expand constructions, parametrized by their hash algorithm
*)
module MiTLS.HKDF
open MiTLS
open MiTLS.Declassify
friend Lib.IntTypes

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)
*)

(*-------------------------------------------------------------------*)
(*
HKDF-Expand(PRK, info, L) -> OKM
   Options:
      Hash     a hash function; HashLen denotes the length of the
               hash function output in octets
   Inputs:
      PRK      a pseudorandom key of at least HashLen octets
               (usually, the output from the extract step)
      info     optional context and application specific information
               (can be a zero-length string)
      L        length of output keying material in octets (<= 255*HashLen)
   Output:
      OKM      output keying material (of L octets)

   N = ceil(L/HashLen)
   T = T(1) | T(2) | T(3) | ... | T(N)

   OKM = first L octets of T

   where:
   T(0) = empty string
   T(1) = HMAC-Hash(PRK, T(0) | info | 0x01)
   T(2) = HMAC-Hash(PRK, T(1) | info | 0x02)
   ...
*)

assume val expand_spec':
  #ha:Hashing.alg ->
  prk: Hashing.Spec.tag ha ->
  info: bytes {Bytes.length info < 1024 (* somewhat arbitrary *) } ->
  len: UInt32.t {0 < v len /\ v len <= op_Multiply 255 (hash_length ha)} ->
  GTot (lbytes32 len)
/
Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked prims.fst.checked MiTLS.Parsers.HKDF.HkdfLabel.fsti.checked MiTLS.Mem.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.Hashing.fsti.checked MiTLS.Declassify.fsti.checked LowStar.Buffer.fst.checked Lib.IntTypes.fst.checked Hacl.Hash.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.Bytes.fsti.checked EverCrypt.HKDF.fsti.checked
MiTLS.HKDF.fst

    prk: MiTLS.Hashing.Spec.tag ha ->
    info: FStar.Bytes.bytes{FStar.Bytes.length info < 1024} ->
    len:
      FStar.UInt32.t
        {0 < FStar.UInt32.v len /\ FStar.UInt32.v len <= 255 * Spec.Hash.Definitions.hash_length ha}
  -> Prims.GTot (FStar.Bytes.lbytes32 len)
MiTLS.HKDF.expand_spec'
let expand_spec =
  
expand_spec'