val 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 ()))})
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)
val 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 ()))})
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)
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 Prims.bool Prims.squash LowParse.Low.Writers.writer LowParse.Low.Writers.Writer LowParse.Low.Writers.__proj__Writer__item__v FStar.Ghost.erased LowParse.Low.Writers.write LowParse.Low.Writers.wvalue
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)))
val 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 ()))})

    cond: Prims.bool ->
    wtrue: (_: Prims.squash (cond == true) -> LowParse.Low.Writers.writer s h0 sout pout_from0) ->
    wfalse: (_: Prims.squash (cond == false) -> LowParse.Low.Writers.writer s h0 sout pout_from0)
  -> x:
    LowParse.Low.Writers.writer s h0 sout pout_from0
      { LowParse.Low.Writers.wvalue x ==
        (match cond with
          | true -> LowParse.Low.Writers.wvalue (wtrue ())
          | _ -> LowParse.Low.Writers.wvalue (wfalse ())) }