val print : s: Prims.string -> FStar.HyperStack.ST.ST Prims.unit
let print s = discard (IO.debug_print_string ("RKY| "^s^"\n"))
module MiTLS.KDF.Rekey
open MiTLS

open MiTLS.Mem
open MiTLS.Pkg
open MiTLS.Idx
open MiTLS.Pkg.Tree
//open KDF
//open IV

//include AEAD.Pkg
//include KDF

/// This file illustrates our use of indexes, packages, and KDF on a
/// simple recursive subset of the TLS key-schedule: late rekeying. It
/// also provides a standalone test for verification and extraction.

val discard: bool -> ST unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 -> h0 == h1))
/
prims.fst.checked MiTLS.Random.fst.checked MiTLS.Pkg.Tree.fst.checked MiTLS.Pkg.fst.checked MiTLS.Mem.fst.checked MiTLS.KDF.fst.checked MiTLS.IV.fst.checked MiTLS.Idx.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.Flags.fst.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.String.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.IO.fst.checked FStar.Bytes.fsti.checked C.fst.checked
MiTLS.KDF.Rekey.fst
s: Prims.string -> FStar.HyperStack.ST.ST Prims.unit
Prims.string MiTLS.KDF.Rekey.discard FStar.IO.debug_print_string Prims.op_Hat Prims.unit
let print s =
  
discard (IO.debug_print_string ("RKY| " ^ s ^ "\n"))