val spec_parser_value_injective (b1 b2: bytes) : Lemma
  (requires (match spec_parser_value b1, spec_parser_value b2 with
  | Some (v1, n1), Some (v2, n2) -> v1 == v2
  | _ -> False
  ))
  (ensures (match spec_parser_value b1, spec_parser_value b2 with
  | Some (v1, n1), Some (v2, n2) -> (n1 <: nat) == n2 /\ Seq.slice b1 0 n1 == Seq.slice b2 0 n2
  | _ -> True
  ))
val spec_parser_value_injective (b1 b2: bytes) : Lemma
  (requires (match spec_parser_value b1, spec_parser_value b2 with
  | Some (v1, n1), Some (v2, n2) -> v1 == v2
  | _ -> False
  ))
  (ensures (match spec_parser_value b1, spec_parser_value b2 with
  | Some (v1, n1), Some (v2, n2) -> (n1 <: nat) == n2 /\ Seq.slice b1 0 n1 == Seq.slice b2 0 n2
  | _ -> True
  ))
let spec_parser_value_injective b1 b2 = F.value_spec_parser_injective b1 b2
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
/
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
b1: Zeta.Steel.ApplicationTypes.bytes -> b2: Zeta.Steel.ApplicationTypes.bytes
  -> FStar.Pervasives.Lemma
      (requires
        ((match
              Zeta.Steel.ApplicationTypes.spec_parser_value b1,
              Zeta.Steel.ApplicationTypes.spec_parser_value b2
            with
            | FStar.Pervasives.Native.Mktuple2
              #_
              #_
              (FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ v1 _))
              (FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ v2 _)) ->
              v1 == v2
            | _ -> Prims.l_False)
          <:
          Type0))
      (ensures
        ((match
              Zeta.Steel.ApplicationTypes.spec_parser_value b1,
              Zeta.Steel.ApplicationTypes.spec_parser_value b2
            with
            | FStar.Pervasives.Native.Mktuple2
              #_
              #_
              (FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ _ n1))
              (FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ _ n2)) ->
              n1 == n2 /\ FStar.Seq.Base.slice b1 0 n1 == FStar.Seq.Base.slice b2 0 n2
            | _ -> Prims.l_True)
          <:
          Type0))
Zeta.Steel.ApplicationTypes.bytes Zeta.KeyValueStore.Formats.Spec.value_spec_parser_injective Prims.unit
let spec_parser_value_injective b1 b2 =
  
F.value_spec_parser_injective b1 b2