val lift_timestamp (st: s_timestamp)
  : i_timestamp
val lift_timestamp (st: s_timestamp)
  : i_timestamp
let lift_timestamp (st: s_timestamp)
  : i_timestamp
  = let epoch = st.epoch in
    let ctr = st.counter in
    { e = U32.v epoch; c = U32.v ctr }
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)))
  = ()

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

#push-options "--query_stats --fuel 0"

let lift_desc_hash (sdh: s_desc_hash)
  : GTot (idh: i_desc_hash { related_desc_hash sdh idh })
  = let open T in
    let open Zeta.Steel.BitUtils in
    match sdh with
    | Dh_vnone () -> M.Empty
    | Dh_vsome dhd -> 
      let k = lift_base_key dhd.dhd_key in
      let h = lift_hash_value dhd.dhd_h in
      let b = Vtrue? dhd.evicted_to_blum in
      let idh = M.Desc k h b in
      Zeta.Steel.KeyUtils.lower_lift_inv dhd.dhd_key;
      idh

let lift_mval (smv: s_mval)
  = { left = lift_desc_hash smv.l;
      right = lift_desc_hash smv.r }

let lift_dval (sdv: s_dval)
  = match sdv with
    | None -> Null
    | Some sv -> DValue sv
    
let lift_val (sv: s_val)
  = match sv with
    | T.MValue smv -> Zeta.Record.IntV (lift_mval smv)
    | T.DValue sdv -> Zeta.Record.AppV (lift_dval sdv)

let lift_record (sr: s_record)
  = let k = lift_key (fst sr) in
    lemma_lower_lift_key (fst sr);
    let v = 
      match snd sr with
      | T.MValue mv -> Zeta.Record.IntV (lift_mval mv)
      | T.DValue d -> Zeta.Record.AppV (lift_dval d)
    in
    k, v
/
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
st: Zeta.Steel.Rel.s_timestamp -> Zeta.Steel.Rel.i_timestamp
Zeta.Steel.Rel.s_timestamp Zeta.Time.Mktimestamp FStar.UInt32.v FStar.UInt32.t Zeta.Steel.LogEntry.Types.__proj__Mktimestamp__item__counter Zeta.Steel.LogEntry.Types.__proj__Mktimestamp__item__epoch Zeta.Steel.Rel.i_timestamp
let lift_timestamp (st: s_timestamp) : i_timestamp =
  
let epoch = st.epoch in
let ctr = st.counter in
{ e = U32.v epoch; c = U32.v ctr }