val lwriter_nil
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p {k.parser_kind_subkind == Some ParserStrong /\ k.parser_kind_low > 0})
      (h0: HS.mem)
      (sout:
          slice (srel_of_buffer_srel (B.trivial_preorder _))
            (srel_of_buffer_srel (B.trivial_preorder _)))
      (pout_from0: U32.t)
    : Tot (x: lwriter s h0 sout pout_from0 {lwvalue x == []})
let lwriter_nil
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p { k.parser_kind_subkind == Some ParserStrong /\ k.parser_kind_low > 0 } )
  (h0: HS.mem)
  (sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (pout_from0: U32.t)
: Tot (x: lwriter s h0 sout pout_from0 { lwvalue x == [] })
= LWriter (Ghost.hide  [])
  (fun pout_from ->
    let h = HST.get () in
    valid_list_nil p h sout pout_from;
    pout_from
  )
val lwriter_nil
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p {k.parser_kind_subkind == Some ParserStrong /\ k.parser_kind_low > 0})
      (h0: HS.mem)
      (sout:
          slice (srel_of_buffer_srel (B.trivial_preorder _))
            (srel_of_buffer_srel (B.trivial_preorder _)))
      (pout_from0: U32.t)
    : Tot (x: lwriter s h0 sout pout_from0 {lwvalue x == []})
let lwriter_nil
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p {k.parser_kind_subkind == Some ParserStrong /\ k.parser_kind_low > 0})
      (h0: HS.mem)
      (sout:
          slice (srel_of_buffer_srel (B.trivial_preorder _))
            (srel_of_buffer_srel (B.trivial_preorder _)))
      (pout_from0: U32.t)
    : Tot (x: lwriter s h0 sout pout_from0 {lwvalue x == []}) =
LWriter (Ghost.hide [])
  (fun pout_from ->
      let h = HST.get () in
      valid_list_nil p h sout pout_from;
      pout_from)
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.l_and 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 Prims.b2t Prims.op_GreaterThan LowParse.Spec.Base.__proj__Mkparser_kind'__item__parser_kind_low FStar.Monotonic.HyperStack.mem LowParse.Slice.slice LowParse.Slice.srel_of_buffer_srel LowParse.Bytes.byte LowStar.Buffer.trivial_preorder FStar.UInt32.t LowParse.Low.Writers.LWriter FStar.Ghost.hide Prims.list Prims.Nil Prims.unit LowParse.Low.Base.Spec.valid_list_nil FStar.HyperStack.ST.get LowParse.Low.Writers.lwriter LowParse.Low.Writers.lwvalue
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)
: GTot t
= Ghost.reveal w.v

inline_for_extraction
noextract
let weaken_swriter
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (#s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
  (#h0: HS.mem)
  (#space_beyond0: 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_beyond0 sout pout_from0)
  (h1: HS.mem)
  (space_beyond1: nat)
  (pout_from1: U32.t)
: Pure (w' : swriter s h1 space_beyond1 sout pout_from1 { swvalue w' == swvalue w } )
  (requires (B.modifies (loc_slice_from sout pout_from0) h0 h1 /\ U32.v pout_from0 <= U32.v pout_from1 /\ space_beyond0 <= space_beyond1))
  (ensures (fun _ -> True))
= SWriter w.v (fun pout_from -> w.w pout_from)

inline_for_extraction
noextract
let swrite
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (#s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
  (#h0: HS.mem)
  (#sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (#pout_from0: U32.t)
  (#space_beyond: nat)  
  (w: swriter s h0 space_beyond sout pout_from0)
: Tot (fswriter s h0 space_beyond sout pout_from0 (swvalue w))
= match w with | SWriter _ f -> f

inline_for_extraction
noextract
let swriter_ifthenelse
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (#s: serializer p { k.parser_kind_subkind == Some ParserStrong /\ k.parser_kind_low > 0 } )
  (#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)
  (cond: bool)
  (wtrue: (squash (cond == true) -> Tot (swriter s h0 space_beyond sout pout_from0)))
  (wfalse: (squash (cond == false) -> Tot (swriter s h0 space_beyond sout pout_from0)))
: Tot (x: swriter s h0 space_beyond sout pout_from0 { swvalue x == (if cond then swvalue (wtrue ()) else swvalue (wfalse ())) } )
= SWriter (if cond then SWriter?.v (wtrue ()) else SWriter?.v (wfalse ()))
  (fun pout_from -> if cond then swrite (wtrue ()) pout_from else swrite (wfalse ()) pout_from)

inline_for_extraction
noextract
let swrite_leaf
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (#s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
  (w: leaf_writer_strong s)
  (h0: HS.mem)
  (sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (pout_from0: U32.t)
  (x: t)
: Tot (y: swriter s h0 0 sout pout_from0 { swvalue y == x } )
= SWriter (Ghost.hide x)
  (fun pout_from -> w x sout pout_from)

inline_for_extraction
noextract
let fwriter
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
  (h0: HS.mem)
  (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 <= U32.v sout.len /\
    U32.v sout.len < U32.v max_uint32
  ))
  (ensures (fun h res h' ->
    B.modifies (loc_slice_from sout pout_from) h h' /\ (
    if res = max_uint32
    then U32.v pout_from + serialized_length s x > U32.v sout.len
    else valid_content_pos p h' sout pout_from x res
)))

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

let wvalue
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (#s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
  (#h0: HS.mem)
  (#sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (#pout_from0: U32.t)
  (w: writer s h0 sout pout_from0)
: GTot t
= Ghost.reveal w.v

inline_for_extraction
noextract
let weaken_writer
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (#s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
  (#h0: HS.mem)
  (#sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (#pout_from0: U32.t)
  (w: writer s h0 sout pout_from0)
  (h1: HS.mem)
  (pout_from1: U32.t)
: Pure (w' : writer s h1 sout pout_from1 { wvalue w' == wvalue w } )
  (requires (B.modifies (loc_slice_from sout pout_from0) h0 h1 /\ U32.v pout_from0 <= U32.v pout_from1))
  (ensures (fun _ -> True))
= Writer w.v (fun pout_from -> w.w pout_from)

inline_for_extraction
noextract
let write
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (#s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
  (#h0: HS.mem)
  (#sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (#pout_from0: U32.t)
  (w: writer s h0 sout pout_from0)
: Tot (fwriter s h0 sout pout_from0 (wvalue w))
= match w with | Writer _ f -> f

inline_for_extraction
noextract
let writer_ifthenelse
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (#s: serializer p { k.parser_kind_subkind == Some ParserStrong /\ k.parser_kind_low > 0 } )
  (#h0: HS.mem)
  (#sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (#pout_from0: U32.t)
  (cond: bool)
  (wtrue: (squash (cond == true) -> Tot (writer s h0 sout pout_from0)))
  (wfalse: (squash (cond == false) -> Tot (writer s h0 sout pout_from0)))
: Tot (x: writer s h0 sout pout_from0 { wvalue x == (if cond then wvalue (wtrue ()) else wvalue (wfalse ())) } )
= Writer (if cond then Writer?.v (wtrue ()) else Writer?.v (wfalse ()))
  (fun pout_from -> if cond then write (wtrue ()) pout_from else write (wfalse ()) pout_from)

inline_for_extraction
noextract
let write_leaf_cs
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (#s: serializer p { k.parser_kind_subkind == Some ParserStrong /\ k.parser_kind_high == Some k.parser_kind_low /\ k.parser_kind_low < 4294967296 } )
  (w: leaf_writer_strong s)
  (h0: HS.mem)
  (sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (pout_from0: U32.t)
  (x: t)
: Tot (y: writer s h0 sout pout_from0 { wvalue y == x } )
= Writer (Ghost.hide x)
  (fun pout_from ->
    if U32.uint_to_t k.parser_kind_low `U32.gt` (sout.len `U32.sub` pout_from)
    then max_uint32
    else w x sout pout_from
  )

inline_for_extraction
noextract
let flwriter
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p { k.parser_kind_subkind == Some ParserStrong /\ k.parser_kind_low > 0 } )
  (h0: HS.mem)
  (sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (pout_from0: U32.t)
  (x: list t)
: Tot Type
= (pout_from: U32.t) ->
  HST.Stack U32.t
  (requires (fun h ->
    live_slice h sout /\
    B.modifies (loc_slice_from sout pout_from0) h0 h /\
    U32.v pout_from0 <= U32.v pout_from /\
    U32.v pout_from <= U32.v sout.len /\
    U32.v sout.len < U32.v max_uint32
  ))
  (ensures (fun h res h' ->
    B.modifies (loc_slice_from sout pout_from) h h' /\ (
    if res = max_uint32
    then U32.v pout_from + serialized_list_length s x > U32.v sout.len
    else
      valid_list p h' sout pout_from res /\
      contents_list p h' sout pout_from res ==  x
  )))

inline_for_extraction
noeq
noextract
type lwriter
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p { k.parser_kind_subkind == Some ParserStrong /\ k.parser_kind_low > 0 } )
  (h0: HS.mem)
  (sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (pout_from0: U32.t)
: Type
= | LWriter:
      (v: Ghost.erased (list t)) ->
      (w: flwriter s h0 sout pout_from0 (Ghost.reveal v)) ->
      lwriter s h0 sout pout_from0

inline_for_extraction
noextract
let lwvalue
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (#s: serializer p { k.parser_kind_subkind == Some ParserStrong /\ k.parser_kind_low > 0 } )
  (#h0: HS.mem)
  (#sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (#pout_from0: U32.t)
  (w: lwriter s h0 sout pout_from0)
: GTot (list t)
= Ghost.reveal w.v

inline_for_extraction
noextract
let weaken_lwriter
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (#s: serializer p { k.parser_kind_subkind == Some ParserStrong /\ k.parser_kind_low > 0 } )
  (#h0: HS.mem)
  (#sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (#pout_from0: U32.t)
  (w: lwriter s h0 sout pout_from0)
  (h1: HS.mem)
  (pout_from1: U32.t)
: Pure (w' : lwriter s h1 sout pout_from1 { lwvalue w' == lwvalue w } )
  (requires (B.modifies (loc_slice_from sout pout_from0) h0 h1 /\ U32.v pout_from0 <= U32.v pout_from1))
  (ensures (fun _ -> True))
= LWriter w.v (fun pout_from -> w.w pout_from)

inline_for_extraction
noextract
let lwrite
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (#s: serializer p { k.parser_kind_subkind == Some ParserStrong /\ k.parser_kind_low > 0 } )
  (#h0: HS.mem)
  (#sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (#pout_from0: U32.t)
  (w: lwriter s h0 sout pout_from0)
: Tot (flwriter s h0 sout pout_from0 (lwvalue w))
= match w with | LWriter _ f -> f

inline_for_extraction
noextract
let lwriter_nil
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p { k.parser_kind_subkind == Some ParserStrong /\ k.parser_kind_low > 0 } )
  (h0: HS.mem)
  (sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (pout_from0: U32.t)
val lwriter_nil
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p {k.parser_kind_subkind == Some ParserStrong /\ k.parser_kind_low > 0})
      (h0: HS.mem)
      (sout:
          slice (srel_of_buffer_srel (B.trivial_preorder _))
            (srel_of_buffer_srel (B.trivial_preorder _)))
      (pout_from0: U32.t)
    : Tot (x: lwriter s h0 sout pout_from0 {lwvalue x == []})

    s:
      LowParse.Spec.Base.serializer p
        { Mkparser_kind'?.parser_kind_subkind k ==
          FStar.Pervasives.Native.Some LowParse.Spec.Base.ParserStrong /\
          Mkparser_kind'?.parser_kind_low k > 0 } ->
    h0: FStar.Monotonic.HyperStack.mem ->
    sout:
      LowParse.Slice.slice (LowParse.Slice.srel_of_buffer_srel (LowStar.Buffer.trivial_preorder LowParse.Bytes.byte
              ))
        (LowParse.Slice.srel_of_buffer_srel (LowStar.Buffer.trivial_preorder LowParse.Bytes.byte)) ->
    pout_from0: FStar.UInt32.t
  -> x: LowParse.Low.Writers.lwriter s h0 sout pout_from0 {LowParse.Low.Writers.lwvalue x == []}