val 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))
val 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))
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
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
/
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
      (let rk = Zeta.Steel.LogEntry.Types.root_key in
        let i_rk = Zeta.GenKey.IntK Zeta.BinTree.Root in
        Zeta.Steel.Rel.related_key rk i_rk))
Prims.unit Zeta.Steel.KeyUtils.lower_lift_inv Zeta.Steel.KeyUtils.root_base_key Zeta.Steel.KeyUtils.related_root Prims.l_True Prims.squash Zeta.Steel.Rel.related_key Zeta.GenKey.key Zeta.Steel.Rel.app Zeta.GenKey.IntK Zeta.BinTree.Root Zeta.Steel.LogEntry.Types.key Zeta.Steel.LogEntry.Types.root_key Prims.Nil FStar.Pervasives.pattern
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