val is_rekey_tree : n: Prims.nat -> x: MiTLS.Pkg.Tree.tree (MiTLS.KDF.Rekey.idealKDF (n + 1)) -> Type0
let is_rekey_tree (n:nat) (x:tree (idealKDF (n+1))) =
  if model then is_rekey_tree' n (KDF.itree x)
  else True
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))
let discard _ = ()
let print s = discard (IO.debug_print_string ("RKY| "^s^"\n"))

(*
//17-11-15 for testing; rename to aeadAlg_of_id ?
assume val get_aeadAlg: i:id -> aeadAlg
let derive_aea
  (lbl:label) (i:id)
  (a:info{wellformed_id (Derive i lbl Expand)}):
  (a':aeadAlg{a' == get_aeadAlg (Derive i lbl Expand)})
=
  //fixme! should be extracted from a
  get_aeadAlg (Derive i lbl Expand)

let is_ae_p (p: pkg ii) =
//  let ioi = get_aeadAlg in
  let (ioi:pkg ii -> Crypto.Indexing.id) = magic() in
  let q = local_ae_pkg ii get_aeadAlg ioi in
  Pkg?.key p == key ii ioi /\ p == memoization q p.define_table
let is_kdf_p (p: pkg ii) d children = // same as ksd_subtree
  Pkg?.key p == secret d children /\ p == memoization (local_kdf_pkg d children) p.define_table
*)

//let test_rekey(): St C.exit_code = C.EXIT_SUCCESS

inline_for_extraction noextract
let ivlen (i:id) : keylen = Hacl.Hash.Definitions.hash_len Hashing.Spec.SHA2_256

let is_iv_p (p:pkg ii) =
  Pkg?.key p == IV.raw ii ivlen /\
  p == memoization (IV.local_raw_pkg ii ivlen) (p.define_table)

assume noextract val flagKDF': d:nat -> b:KDF.iflag{d=0 ==> b = false}
inline_for_extraction noextract let flagKDF d = if model then flagKDF' d else false
noextract let idealKDF d = b2t (flagKDF d)

assume noextract val lemma_KDF_depth: d:nat -> Lemma
  (idealKDF d == b2t (flagKDF d) /\ (match d with 0 -> idealKDF 0 == False | d -> idealKDF d ==> idealKDF (d+1)))

type is_kdf_p (p:pkg ii) (#ideal:KDF.iflag) (u:KDF.usage ideal) =
  Pkg?.key p == KDF.secret u /\
  p == memoization (KDF.local_kdf_pkg ideal u) p.define_table

private noextract let _mchildren (f:KDF.iflag) (#p:Type0) (c:children' p)
  : Pure (KDF.usage f)
  (requires model /\ b2t f == p) (ensures fun _ -> True) = c

#set-options "--z3rlimit 30"
noextract
let rec is_rekey_tree' (n:nat) (x:tree' (idealKDF (n+1)))
  : Pure Type0 (requires model) (ensures fun _ -> True) (decreases n) =
  lemma_KDF_depth n;
  if n = 0 then
    match x with
    | Node p [] ->
      Pkg?.ideal p == idealKDF 0 /\
      is_kdf_p p (_mchildren false (Node?.children x))
    | _ -> False
  else
    match x with
    | Node p ["IV", Leaf iv; "RE", re ] ->
      Pkg?.ideal p == idealKDF n /\
      is_kdf_p p (_mchildren (flagKDF n) (Node?.children x)) /\
      is_iv_p iv /\
      is_rekey_tree' (n-1) re
    | _ -> False
#reset-options
/
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
n: Prims.nat -> x: MiTLS.Pkg.Tree.tree (MiTLS.KDF.Rekey.idealKDF (n + 1)) -> Type0
Prims.nat MiTLS.Pkg.Tree.tree MiTLS.KDF.Rekey.idealKDF Prims.op_Addition MiTLS.Mem.model MiTLS.KDF.Rekey.is_rekey_tree' MiTLS.KDF.itree Prims.bool Prims.l_True
let is_rekey_tree (n: nat) (x: tree (idealKDF (n + 1))) =
  
if model then is_rekey_tree' n (KDF.itree x) else True