val key_cmp_fn : Zeta.MultiSet.cmp (app_key adm)
val key_cmp_fn : Zeta.MultiSet.cmp (app_key adm)
let key_cmp_fn = fun n1 n2 -> FStar.UInt64.(n1 <=^ n2)
module Zeta.KeyValueStore.Spec

open Zeta.App

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

friend Zeta.Steel.KeyUtils

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.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
Zeta.MultiSet.cmp (Zeta.App.app_key Zeta.KeyValueStore.Spec.adm)
Zeta.App.app_key Zeta.KeyValueStore.Spec.adm FStar.UInt64.op_Less_Equals_Hat Prims.bool
let key_cmp_fn =
  
fun n1 n2 -> let open FStar.UInt64 in n1 <=^ n2