val size32_option
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (#s: serializer p)
      (s32: size32 s)
      (u: squash (k.parser_kind_low > 0))
    : Tot (size32 (serialize_option s u))
let size32_option (#k: parser_kind) (#t: Type) (#p: parser k t) (#s: serializer p) (s32: size32 s) (u: squash (k.parser_kind_low > 0)) : Tot (size32 (serialize_option s u)) =
  fun input -> ((match input with
  | None -> 0ul
  | Some y -> s32 y) <: (y: U32.t { size32_postcond (serialize_option s u) input y } ))
val size32_option
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (#s: serializer p)
      (s32: size32 s)
      (u: squash (k.parser_kind_low > 0))
    : Tot (size32 (serialize_option s u))
let size32_option
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (#s: serializer p)
      (s32: size32 s)
      (u: squash (k.parser_kind_low > 0))
    : Tot (size32 (serialize_option s u)) =
fun input ->
  ((match input with
      | None -> 0ul
      | Some y -> s32 y)
    <:
    (y: U32.t{size32_postcond (serialize_option s u) input y}))
LowParse.SLow.Option.fst.checked
prims.fst.checked LowParse.Spec.Option.fst.checked LowParse.SLow.Base.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked
LowParse.SLow.Option.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Base.serializer LowParse.SLow.Base.size32 Prims.squash Prims.b2t Prims.op_GreaterThan LowParse.Spec.Base.__proj__Mkparser_kind'__item__parser_kind_low FStar.Pervasives.Native.option FStar.UInt32.__uint_to_t FStar.UInt32.t LowParse.SLow.Base.size32_postcond LowParse.Spec.Option.parse_option_kind LowParse.Spec.Option.parse_option LowParse.Spec.Option.serialize_option
module LowParse.SLow.Option
include LowParse.Spec.Option
include LowParse.SLow.Base

module U32 = FStar.UInt32
module B32 = FStar.Bytes

inline_for_extraction
let parse32_option (#k: parser_kind) (#t: Type) (#p: parser k t) (p32: parser32 p) : Tot (parser32 (parse_option p)) =
  fun input -> ((match p32 input with
  | Some (x, consumed) -> Some (Some x, consumed)
  | _ -> Some (None, 0ul)) <: (y: option (option t * U32.t) { parser32_correct (parse_option p) input y } ))

inline_for_extraction
let serialize32_option (#k: parser_kind) (#t: Type) (#p: parser k t) (#s: serializer p) (s32: serializer32 s) (u: squash (k.parser_kind_low > 0)) : Tot (serializer32 (serialize_option s u)) =
  fun input -> ((match input with
  | None ->
    [@inline_let]
    let res = B32.empty_bytes in
    assert (B32.reveal res `Seq.equal` Seq.empty);
    res
  | Some y -> s32 y) <: (y: B32.bytes { serializer32_correct (serialize_option s u) input y } ))

inline_for_extraction
val size32_option
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (#s: serializer p)
      (s32: size32 s)
      (u: squash (k.parser_kind_low > 0))
    : Tot (size32 (serialize_option s u))
s32: LowParse.SLow.Base.size32 s -> u21: Prims.squash (Mkparser_kind'?.parser_kind_low k > 0)
  -> LowParse.SLow.Base.size32 (LowParse.Spec.Option.serialize_option s u21)