val swvalue
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (#s: serializer p {k.parser_kind_subkind == Some ParserStrong})
      (#h0: HS.mem)
      (#space_beyond: nat)
      (#sout:
          slice (srel_of_buffer_srel (B.trivial_preorder _))
            (srel_of_buffer_srel (B.trivial_preorder _)))
      (#pout_from0: U32.t)
      (w: swriter s h0 space_beyond sout pout_from0)
    : GTot t
let swvalue
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (#s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
  (#h0: HS.mem)
  (#space_beyond: nat)
  (#sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (#pout_from0: U32.t)
  (w: swriter s h0 space_beyond sout pout_from0)
: GTot t
= Ghost.reveal w.v
val swvalue
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (#s: serializer p {k.parser_kind_subkind == Some ParserStrong})
      (#h0: HS.mem)
      (#space_beyond: nat)
      (#sout:
          slice (srel_of_buffer_srel (B.trivial_preorder _))
            (srel_of_buffer_srel (B.trivial_preorder _)))
      (#pout_from0: U32.t)
      (w: swriter s h0 space_beyond sout pout_from0)
    : GTot t
let swvalue
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (#s: serializer p {k.parser_kind_subkind == Some ParserStrong})
      (#h0: HS.mem)
      (#space_beyond: nat)
      (#sout:
          slice (srel_of_buffer_srel (B.trivial_preorder _))
            (srel_of_buffer_srel (B.trivial_preorder _)))
      (#pout_from0: U32.t)
      (w: swriter s h0 space_beyond sout pout_from0)
    : GTot t =
Ghost.reveal w.v
LowParse.Low.Writers.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Low.Base.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
LowParse.Low.Writers.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Base.serializer Prims.eq2 FStar.Pervasives.Native.option LowParse.Spec.Base.parser_subkind LowParse.Spec.Base.__proj__Mkparser_kind'__item__parser_kind_subkind FStar.Pervasives.Native.Some LowParse.Spec.Base.ParserStrong FStar.Monotonic.HyperStack.mem Prims.nat LowParse.Slice.slice LowParse.Slice.srel_of_buffer_srel LowParse.Bytes.byte LowStar.Buffer.trivial_preorder FStar.UInt32.t LowParse.Low.Writers.swriter FStar.Ghost.reveal LowParse.Low.Writers.__proj__SWriter__item__v
module LowParse.Low.Writers
include LowParse.Low.Base

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module B = LowStar.Buffer
module U32 = FStar.UInt32
module L = FStar.List.Tot

inline_for_extraction
noextract
let fswriter
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
  (h0: HS.mem)
  (space_beyond: nat)
  (sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (pout_from0: U32.t)
  (x: t)
: Tot Type
= (pout_from: U32.t) ->
  HST.Stack U32.t
  (requires (fun h ->
    B.modifies (loc_slice_from sout pout_from0) h0 h /\
    U32.v pout_from0 <= U32.v pout_from /\
    live_slice h sout /\
    U32.v pout_from + serialized_length s x + space_beyond <= U32.v sout.len
  ))
  (ensures (fun h res h' ->
    B.modifies (loc_slice_from sout pout_from) h h' /\
    valid_content_pos p h' sout pout_from x res
))

inline_for_extraction
noextract
noeq
type swriter
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
  (h0: HS.mem)
  (space_beyond: nat)
  (sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (pout_from0: U32.t)
: Type
= | SWriter:
    (v: Ghost.erased t) ->
    (w: fswriter s h0 space_beyond sout pout_from0 (Ghost.reveal v)) ->
    swriter s h0 space_beyond sout pout_from0

let swvalue
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (#s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
  (#h0: HS.mem)
  (#space_beyond: nat)
  (#sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (#pout_from0: U32.t)
  (w: swriter s h0 space_beyond sout pout_from0)
val swvalue
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (#s: serializer p {k.parser_kind_subkind == Some ParserStrong})
      (#h0: HS.mem)
      (#space_beyond: nat)
      (#sout:
          slice (srel_of_buffer_srel (B.trivial_preorder _))
            (srel_of_buffer_srel (B.trivial_preorder _)))
      (#pout_from0: U32.t)
      (w: swriter s h0 space_beyond sout pout_from0)
    : GTot t
w: LowParse.Low.Writers.swriter s h0 space_beyond sout pout_from0 -> Prims.GTot t