val key_hash_fn (k:F.key_t) : Zeta.Key.leaf_key
val key_hash_fn (k:F.key_t) : Zeta.Key.leaf_key
let key_hash_fn (k:F.key_t) : Zeta.Key.leaf_key =
    let rk : Zeta.Steel.KeyUtils.raw_key = {
    k = ({
      v3 = 0uL;
      v2 = 0uL;
      v1 = 0uL;
      v0 = k;
    });

   significant_digits = 256us;
  } in
  Zeta.Steel.KeyUtils.lift_raw_key rk
module Zeta.KeyValueStore.Spec

open Zeta.App

module P = Zeta.Steel.Parser
module F = Zeta.KeyValueStore.Formats

friend Zeta.Steel.KeyUtils
/
Zeta.Steel.Parser.fst.checked Zeta.Steel.KeyUtils.fst.checked Zeta.KeyValueStore.Formats.fsti.checked Zeta.Key.fsti.checked Zeta.Hash.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.UInt16.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.KeyValueStore.Spec.fst
k: Zeta.KeyValueStore.Formats.Types.key_t -> Zeta.Key.leaf_key
Zeta.KeyValueStore.Formats.Types.key_t Zeta.Steel.KeyUtils.lift_raw_key Zeta.Steel.KeyUtils.raw_key Zeta.Steel.KeyUtils.Mkraw_key Zeta.Steel.KeyUtils.Mku256 FStar.UInt64.__uint_to_t FStar.UInt16.__uint_to_t Zeta.Key.leaf_key
let key_hash_fn (k: F.key_t) : Zeta.Key.leaf_key =
  
let rk:Zeta.Steel.KeyUtils.raw_key =
  { k = ({ v3 = 0uL; v2 = 0uL; v1 = 0uL; v0 = k }); significant_digits = 256us }
in
Zeta.Steel.KeyUtils.lift_raw_key rk