val value_cmp_fn : Zeta.MultiSet.cmp (app_value_nullable adm)
val value_cmp_fn : Zeta.MultiSet.cmp (app_value_nullable adm)
let value_cmp_fn =
  fun v1 v2 ->
  match v1, v2 with
  | Null, _ -> true
  | DValue v1, DValue v2 -> FStar.UInt64.(v1 <=^ v2)
  | _, _ -> false
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.KeyUtils.lift_raw_key rk
let key_cmp_fn = fun n1 n2 -> FStar.UInt64.(n1 <=^ n2)
/
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_value_nullable Zeta.KeyValueStore.Spec.adm)
Zeta.App.app_value_nullable Zeta.KeyValueStore.Spec.adm FStar.Pervasives.Native.Mktuple2 Zeta.App.app_value FStar.UInt64.op_Less_Equals_Hat Prims.bool
let value_cmp_fn =
  
fun v1 v2 ->
  match v1, v2 with
  | Null, _ -> true
  | DValue v1, DValue v2 -> let open FStar.UInt64 in v1 <=^ v2
  | _, _ -> false