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