val n_threads : n:U32.t{ 0 < U32.v n /\ U32.v n < FStar.UInt.max_int 16 }
val n_threads : n:U32.t{ 0 < U32.v n /\ U32.v n < FStar.UInt.max_int 16 }
let n_threads = 16ul
module Zeta.Steel.ApplicationTypes

module S = Zeta.KeyValueStore.Spec
module F = Zeta.KeyValueStore.Formats

/// Implementation of the steel/Zeta.Steel.ApplicationsTypes interface
///   for the key value store app

type key_type = F.key_t

let spec_parser_key = F.key_spec_parser
let parse_key = F.kvstore_key_parser
let spec_serializer_key = F.key_spec_serializer
let serialize_key = F.kvstore_key_serializer

let spec_parser_key_injective b1 b2 = F.key_spec_parser_injective b1 b2

let spec_parser_key_strong_prefix b1 b2 = F.key_spec_parser_strong_prefix b1 b2

let serialized_key_length v = F.serialized_key_length v

type value_type = F.value_t

let eq_value_type v0 v1 = v0 = v1

let spec_parser_value = F.value_spec_parser
let parse_value = F.kvstore_value_parser

let spec_serializer_value = F.value_spec_serializer
let serialize_value = F.kvstore_value_serializer

let spec_parser_value_injective b1 b2 = F.value_spec_parser_injective b1 b2

let spec_parser_value_strong_prefix b1 b2 = F.value_spec_parser_strong_prefix b1 b2

let serialized_value_length v = F.serialized_value_length v

let aprm = S.kv_params
/
Zeta.KeyValueStore.Spec.fsti.checked Zeta.KeyValueStore.Formats.fsti.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.Steel.ApplicationTypes.fst
n: FStar.UInt32.t{0 < FStar.UInt32.v n /\ FStar.UInt32.v n < FStar.UInt.max_int 16}
FStar.UInt32.__uint_to_t
let n_threads =
  
16ul