val concrete_pkg : t: MiTLS.Pkg.Tree.tree (MiTLS.KDF.Rekey.idealKDF (n + 1)) {MiTLS.KDF.Rekey.is_rekey_tree n t} ->
    l: MiTLS.Idx.label
  -> MiTLS.Pkg.local_pkg MiTLS.Idx.ii
let
concrete_pkg (#n:nat) (t:tree (idealKDF (n+1)){is_rekey_tree n t}) (l:label) =
  if model then
    [@inline_let] let t' : tree' (idealKDF (n+1)) = t in
    assert(is_rekey_tree' n t);
    [@inline_let] let Node p u = t' in
    if has_lbl #(idealKDF n) u l then
      match l with
      | "RE" -> KDF.local_kdf_pkg (flagKDF n) u
      | "IV" -> IV.local_raw_pkg ii ivlen
    else _cpkg l
  else
    _cpkg l
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

inline_for_extraction
let is_rekey_tree (n:nat) (x:tree (idealKDF (n+1))) =
  if model then is_rekey_tree' n (KDF.itree x)
  else True

noextract
val mk_rekey' (n:nat)
  : ST (tree' (idealKDF (n+1)))
  (requires fun h0 -> model)
  (ensures fun h0 x h1 ->
    is_rekey_tree' n x
    //tree_invariant x h1
  ) (decreases n)

private noextract
let lift_children' (#p:Type0) (u:children' p)
  : Pure (children p) (requires model) (ensures fun u' -> u' == u) = u

// utf8_encode gives this but not bytes_of_string
assume val lemma_bytes_of_string_length: s:string -> Lemma
  (Bytes.length (Bytes.bytes_of_string s) <= op_Multiply 4 (String.length s))

inline_for_extraction noextract let mklabel (s:string) : Pure label
  (requires normalize (String.length s < 32))
  (ensures fun l -> True) =
  lemma_bytes_of_string_length s; s

#set-options "--z3rlimit 30"
noextract
let rec mk_rekey' n =
  lemma_KDF_depth n;
  if n = 0 then (
    let u : children False = lift_children' [] in
    let p = memoization_ST (KDF.local_kdf_pkg (flagKDF 0) u) in
    Node p u
  ) else (
    let re : tree' (idealKDF n) = mk_rekey' (n-1) in
    let iv = memoization_ST (IV.local_raw_pkg ii ivlen) in
    assume(b2t Flags.flag_Raw ==> idealKDF n);
    let iv_leaf : tree' (idealKDF n) = Leaf iv in
    let u : children (idealKDF n) = lift_children' [mklabel "IV", iv_leaf; mklabel "RE",re] in
    let p = memoization_ST (KDF.local_kdf_pkg (flagKDF n) u) in
    Node p u
  )

inline_for_extraction noextract
let mk_rekey (n:nat)
  : ST (tree (idealKDF (n+1)))
  (requires fun h0 -> True)
  (ensures fun h0 t h1 ->
    is_rekey_tree n t /\
    KDF.tree_invariant t h1)
  =
  if model then
    let t' = mk_rekey' n in
    let h = get () in
    let _ = assume(KDF.tree_invariant' t' h) in
    t'
  else erased_tree

noextract inline_for_extraction let _cpkg (l:label) =
  if l = "RE" then
     [@inline_let] let u : KDF.usage false =
       if model then _mchildren false #False []
       else erased_tree in
     KDF.local_kdf_pkg false u
  else IV.local_raw_pkg ii ivlen
/
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

    t: MiTLS.Pkg.Tree.tree (MiTLS.KDF.Rekey.idealKDF (n + 1)) {MiTLS.KDF.Rekey.is_rekey_tree n t} ->
    l: MiTLS.Idx.label
  -> MiTLS.Pkg.local_pkg MiTLS.Idx.ii
Prims.nat MiTLS.Pkg.Tree.tree MiTLS.KDF.Rekey.idealKDF Prims.op_Addition MiTLS.KDF.Rekey.is_rekey_tree MiTLS.Idx.label MiTLS.Mem.model MiTLS.Pkg.Tree.t Prims.l_imp MiTLS.Pkg.__proj__Pkg__item__ideal MiTLS.Idx.ii Prims.list FStar.Pervasives.Native.tuple2 MiTLS.Pkg.Tree.tree' MiTLS.Pkg.Tree.has_lbl MiTLS.KDF.local_kdf_pkg MiTLS.KDF.Rekey.flagKDF MiTLS.IV.local_raw_pkg MiTLS.KDF.Rekey.ivlen MiTLS.Pkg.local_pkg Prims.bool MiTLS.KDF.Rekey._cpkg Prims.unit Prims._assert MiTLS.KDF.Rekey.is_rekey_tree'
let concrete_pkg (#n: nat) (t: tree (idealKDF (n + 1)) {is_rekey_tree n t}) (l: label) =
  
if model
then
  [@@ inline_let ]let t':tree' (idealKDF (n + 1)) = t in
  assert (is_rekey_tree' n t);
  [@@ inline_let ]let Node p u = t' in
  if has_lbl #(idealKDF n) u l
  then
    match l with
    | "RE" -> KDF.local_kdf_pkg (flagKDF n) u
    | "IV" -> IV.local_raw_pkg ii ivlen
  else _cpkg l
else _cpkg l