val kvstore_vput_args_parser : P.parser vput_args_spec_parser
val kvstore_vput_args_parser : P.parser vput_args_spec_parser
let kvstore_vput_args_parser =
  P.make_parser
    vput_args_spec_parser
    parse_vput_args
    (LL.validate_synth
      (LL.validate_u64 () `LL.validate_nondep_then` LL.validate_u64 () `LL.validate_nondep_then` LL.validate_u16 ())
      synth_vput_args
      ()
    )
    (LL.read_synth'
      _
      synth_vput_args
      (LL.read_nondep_then
        (LL.jump_nondep_then LL.jump_u64 LL.jump_u64)
        (LL.read_nondep_then LL.jump_u64 LL.read_u64 LL.read_u64)
        LL.read_u16
      )
      ()
    )
module Zeta.KeyValueStore.Formats.LowStar

module LL = LowParse.Low
module B = LowStar.Buffer
module HST = FStar.HyperStack.ST

friend Zeta.KeyValueStore.Formats.Spec

let kvstore_key_parser =
  P.make_parser
    key_spec_parser
    LL.parse_u64
    (LL.validate_u64 ())
    LL.read_u64

let kvstore_key_serializer =
  P.make_serializer
    _
    key_spec_serializer
    _
    LL.serialize_u64
    LL.serialize32_u64

let kvstore_value_parser =
  P.make_parser
    value_spec_parser
    LL.parse_u64
    (LL.validate_u64 ())
    LL.read_u64

let kvstore_value_serializer =
  P.make_serializer
    _
    value_spec_serializer
    _
    LL.serialize_u64
    LL.serialize32_u64

let kvstore_vget_args_parser =
  P.make_parser
    vget_args_spec_parser
    parse_vget_args
    (LL.validate_synth
      (LL.validate_u64 () `LL.validate_nondep_then` LL.validate_u64 () `LL.validate_nondep_then` LL.validate_u16 ())
      synth_vget_args
      ()
    )
    (LL.read_synth'
      _
      synth_vget_args
      (LL.read_nondep_then
        (LL.jump_nondep_then LL.jump_u64 LL.jump_u64)
        (LL.read_nondep_then LL.jump_u64 LL.read_u64 LL.read_u64)
        LL.read_u16
      )
      ()
    )
/
Zeta.KeyValueStore.Formats.Spec.fst.checked prims.fst.checked LowStar.Buffer.fst.checked LowParse.Low.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked
Zeta.KeyValueStore.Formats.LowStar.fst
Zeta.LowStar.Parser.parser Zeta.KeyValueStore.Formats.Spec.vput_args_spec_parser
Zeta.LowStar.Parser.make_parser Zeta.KeyValueStore.Formats.Types.vput_args_t LowParse.Spec.Combinators.and_then_kind LowParse.Spec.Int.parse_u64_kind LowParse.Spec.Int.parse_u16_kind Zeta.KeyValueStore.Formats.Spec.vput_args_spec_parser Zeta.KeyValueStore.Formats.Spec.parse_vput_args LowParse.Low.Combinators.validate_synth FStar.Pervasives.Native.tuple2 FStar.UInt64.t FStar.UInt16.t LowParse.Spec.Combinators.nondep_then LowParse.Spec.Int.parse_u64 LowParse.Spec.Int.parse_u16 LowParse.Low.Combinators.validate_nondep_then LowParse.Low.Int.validate_u64 LowParse.Low.Int.validate_u16 Zeta.KeyValueStore.Formats.Spec.synth_vput_args LowParse.Low.Combinators.read_synth' LowParse.Low.Combinators.read_nondep_then LowParse.Low.Combinators.jump_nondep_then LowParse.Low.Int.jump_u64 LowParse.Low.Int.read_u64 LowParse.Low.Int.read_u16
let kvstore_vput_args_parser =
  
P.make_parser vput_args_spec_parser
  parse_vput_args
  (LL.validate_synth (((LL.validate_u64 ()) `LL.validate_nondep_then` (LL.validate_u64 ()))
        `LL.validate_nondep_then`
        (LL.validate_u16 ()))
      synth_vput_args
      ())
  (LL.read_synth' _
      synth_vput_args
      (LL.read_nondep_then (LL.jump_nondep_then LL.jump_u64 LL.jump_u64)
          (LL.read_nondep_then LL.jump_u64 LL.read_u64 LL.read_u64)
          LL.read_u16)
      ())