val related_zero (_:unit)
  : Lemma (ensures (related_hash_value TSM.zero Zeta.Hash.zero))
val related_zero (_:unit)
  : Lemma (ensures (related_hash_value TSM.zero Zeta.Hash.zero))
let related_zero (_:unit)
  : Lemma (ensures (related_hash_value TSM.zero Zeta.Hash.zero))
  = Zeta.Steel.BitUtils.related_zero()
module Zeta.Steel.Rel

module GK = Zeta.GenKey
module T = Zeta.Steel.FormatsManual
module KU = Zeta.Steel.KeyUtils

let lift_key (k: s_key)
  : GTot i_key
  = let open T in
    let open GK in
    match k with
    | InternalKey k -> 
      KU.lift_internal_key k;
      IntK (lift_base_key k)
    | ApplicationKey k -> AppK k

let lower_key (k: i_key)
  = let open T in
    let open GK in
    match k with
    | IntK k -> 
      KU.lower_merkle_key k;
      lift_lower_inv k;
      InternalKey (lower_base_key k)
    | AppK k -> ApplicationKey k

let lemma_lower_lift_key (k: s_key)
  : Lemma (ensures (lower_key (lift_key k) == k))
  = match k with
    | T.InternalKey k ->
      lower_lift_inv k
    | _ -> ()

let related_root (sk: s_key) (ik: i_key)
  : Lemma (requires (related_key sk ik))
          (ensures (TSM.is_root_key sk <==> ik = GK.IntK Zeta.BinTree.Root))
  = match sk with
    | T.ApplicationKey _ -> ()
    | T.InternalKey k ->
      KU.is_root_spec k;
      T.related_root();
      T.lower_lift_inv root_base_key

let related_root_inv (_:unit)
  : Lemma (ensures (let rk = T.root_key in
                    let i_rk = GK.IntK Zeta.BinTree.Root in
                    related_key rk i_rk))
  = T.related_root();
    T.lower_lift_inv root_base_key

let lemma_related_key_proper_descendent (sk0 sk1: s_base_key) (ik0 ik1: i_base_key)
  : Lemma (requires (related_base_key sk0 ik0 /\ related_base_key sk1 ik1))
          (ensures (is_proper_descendent sk0 sk1 <==> Zeta.BinTree.is_proper_desc ik0 ik1) /\
                   (is_proper_descendent sk0 sk1 ==>
                    (related_desc_dir (desc_dir sk0 sk1) (Zeta.BinTree.desc_dir ik0 ik1))))
  = Zeta.Steel.KeyUtils.related_proper_descendent sk0 sk1 ik0 ik1;
    if is_proper_descendent sk0 sk1
    then Zeta.Steel.KeyUtils.related_desc_dir sk0 sk1 ik0 ik1

let lemma_related_base_key (sk: s_key) (ik: i_key)
  : Lemma (requires (related_key sk ik))
          (ensures (let s = TSM.to_base_key sk in
                    let i = GK.to_base_key ik in
                    related_base_key s i))
  = ()

let related_app_key (sk: s_key) (ik: i_key)
  : Lemma (requires (related_key sk ik /\
                     T.ApplicationKey? sk))
          (ensures (GK.AppK? ik /\
                    (let T.ApplicationKey ak = sk in
                     let GK.AppK i_ak = ik in
                     ak = i_ak)))
  = ()
/
Zeta.Time.fsti.checked Zeta.Steel.KeyUtils.fsti.checked Zeta.Steel.FormatsManual.fsti.checked Zeta.Steel.BitUtils.fsti.checked Zeta.Record.fsti.checked Zeta.Hash.fsti.checked Zeta.GenKey.fsti.checked Zeta.BinTree.fsti.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.Steel.Rel.fst
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures Zeta.Steel.Rel.related_hash_value Zeta.Steel.ThreadStateModel.zero Zeta.Hash.zero)
Prims.unit Zeta.Steel.BitUtils.related_zero Prims.l_True Prims.squash Zeta.Steel.Rel.related_hash_value Zeta.Steel.ThreadStateModel.zero Zeta.Hash.zero Prims.Nil FStar.Pervasives.pattern
let related_zero (_: unit) : Lemma (ensures (related_hash_value TSM.zero Zeta.Hash.zero)) =
  
Zeta.Steel.BitUtils.related_zero ()