val olwriter_append
      (#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)
      (w1 w2: olwriter s h0 sout pout_from0)
    : Tot
    (x:
      olwriter s h0 sout pout_from0
        { olwvalue x ==
          (match olwvalue w1, olwvalue w2 with
            | Some l1, Some l2 -> Some (l1 `List.Tot.append` l2)
            | _ -> None) })
let olwriter_append
  (#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)
  (w1 w2: olwriter s h0 sout pout_from0)
: Tot (x: olwriter s h0 sout pout_from0 { olwvalue x == (match olwvalue w1, olwvalue w2 with | Some l1, Some l2 -> Some (l1 `List.Tot.append` l2) | _ -> None) } )
= OLWriter (Ghost.hide (match olwvalue w1, olwvalue w2 with | Some l1, Some l2 -> Some (l1 `List.Tot.append` l2) | _ -> None)) (fun pout_from ->
    let res1 = olwrite w1 pout_from in
    Classical.forall_intro_2 (serialized_list_length_append s);
    if (max_uint32 `U32.sub` 1ul) `U32.lte` res1
    then
      res1
    else begin
      let res2 = olwrite w2 res1 in
      let h = HST.get () in
      valid_list_serialized_list_length s h sout pout_from res1;
      if res2 `U32.lt` (max_uint32 `U32.sub` 1ul)
      then begin
        valid_list_serialized_list_length s h sout res1 res2;
        valid_list_append p h sout pout_from res1 res2;
        valid_list_serialized_list_length s h sout pout_from res2
      end;
      res2
    end
  )
val olwriter_append
      (#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)
      (w1 w2: olwriter s h0 sout pout_from0)
    : Tot
    (x:
      olwriter s h0 sout pout_from0
        { olwvalue x ==
          (match olwvalue w1, olwvalue w2 with
            | Some l1, Some l2 -> Some (l1 `List.Tot.append` l2)
            | _ -> None) })
let olwriter_append
      (#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)
      (w1 w2: olwriter s h0 sout pout_from0)
    : Tot
    (x:
      olwriter s h0 sout pout_from0
        { olwvalue x ==
          (match olwvalue w1, olwvalue w2 with
            | Some l1, Some l2 -> Some (l1 `List.Tot.append` l2)
            | _ -> None) }) =
OLWriter
  (Ghost.hide (match olwvalue w1, olwvalue w2 with
        | Some l1, Some l2 -> Some (l1 `List.Tot.append` l2)
        | _ -> None))
  (fun pout_from ->
      let res1 = olwrite w1 pout_from in
      Classical.forall_intro_2 (serialized_list_length_append s);
      if (max_uint32 `U32.sub` 1ul) `U32.lte` res1
      then res1
      else
        let res2 = olwrite w2 res1 in
        let h = HST.get () in
        valid_list_serialized_list_length s h sout pout_from res1;
        if res2 `U32.lt` (max_uint32 `U32.sub` 1ul)
        then
          (valid_list_serialized_list_length s h sout res1 res2;
            valid_list_append p h sout pout_from res1 res2;
            valid_list_serialized_list_length s h sout pout_from res2);
        res2)
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.olwriter LowParse.Low.Writers.OLWriter FStar.Ghost.hide Prims.list FStar.Pervasives.Native.Mktuple2 LowParse.Low.Writers.olwvalue FStar.List.Tot.Base.append FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.None FStar.UInt32.lte FStar.UInt32.sub LowParse.Low.ErrorCode.max_uint32 FStar.UInt32.__uint_to_t Prims.bool Prims.unit FStar.UInt32.lt LowParse.Low.Base.Spec.valid_list_serialized_list_length LowParse.Low.Base.Spec.valid_list_append FStar.HyperStack.ST.get LowParse.Low.Writers.olwrite FStar.Classical.forall_intro_2 Prims.int LowParse.Low.Base.Spec.serialized_list_length Prims.op_Addition LowParse.Low.Base.Spec.serialized_list_length_append
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)
: 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
  )

inline_for_extraction
noextract
let lwriter_singleton
  (#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: writer s h0 sout pout_from0)
: Tot (x: lwriter s h0 sout pout_from0 { lwvalue x == [wvalue w] } )
= LWriter (Ghost.hide [wvalue w])
  (fun pout_from ->
    let res = write w pout_from in
    if res `U32.lt` max_uint32
    then begin
      let h = HST.get () in
      valid_list_nil p h sout res;
      valid_list_cons p h sout pout_from res
    end else begin
      [@inline_let]
      let f () : Lemma (ensures (let v = wvalue w in serialized_list_length s [v] == serialized_length s v)) =
        serialized_list_length_cons s (wvalue w) [];
        serialized_list_length_nil s
      in
      f ()
    end;
    res
  )

inline_for_extraction
noextract
let lwriter_append
  (#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)
  (w1 w2: lwriter s h0 sout pout_from0)
: Tot (x: lwriter s h0 sout pout_from0 { lwvalue x == lwvalue w1 `List.Tot.append` lwvalue w2 } )
= LWriter (Ghost.hide (lwvalue w1 `List.Tot.append` lwvalue w2)) (fun pout_from ->
    let res1 = lwrite w1 pout_from in
    Classical.forall_intro_2 (serialized_list_length_append s);
    if res1 = max_uint32
    then
      res1
    else begin
      let res2 = lwrite w2 res1 in
      let h = HST.get () in
      valid_list_serialized_list_length s h sout pout_from res1;
      if res2 `U32.lt` (max_uint32)
      then begin
        valid_list_serialized_list_length s h sout res1 res2;
        valid_list_append p h sout pout_from res1 res2;
        valid_list_serialized_list_length s h sout pout_from res2
      end;
      res2
    end
  )

inline_for_extraction
noextract
let lwriter_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 (lwriter s h0 sout pout_from0)))
  (wfalse: (squash (cond == false) -> Tot (lwriter s h0 sout pout_from0)))
: Tot (x: lwriter s h0 sout pout_from0 { lwvalue x == (if cond then lwvalue (wtrue ()) else lwvalue (wfalse ())) } )
= LWriter (if cond then (wtrue ()).v else (wfalse ()).v)
  (fun pout_from -> if cond then lwrite (wtrue ()) pout_from else lwrite (wfalse ()) pout_from)

inline_for_extraction
noextract
let lwriter_list_map
  (#k1: parser_kind)
  (#t1: Type)
  (#p1: parser k1 t1)
  (j1: jumper p1)
  (#k2: parser_kind)
  (#t2: Type)
  (#p2: parser k2 t2)
  (s2: serializer p2 { k2.parser_kind_subkind == Some ParserStrong /\ k2.parser_kind_low > 0 } )
  (f: t1 -> Tot t2)
  (#rrel #rel: _)
  (sin: slice rrel rel)
  (pin_from pin_to: U32.t)
  (h0: HS.mem)
  (sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (pout_from0: U32.t {
    B.loc_disjoint (loc_slice_from sout pout_from0) (loc_slice_from_to sin pin_from pin_to) /\
    valid_list p1 h0 sin pin_from pin_to
  })
  (f' : (
    (pos: U32.t {
      U32.v pin_from <= U32.v pos /\
      valid p1 h0 sin pos /\
      U32.v pos + content_length p1 h0 sin pos <= U32.v pin_to
    }) ->
    Tot (y: writer s2 h0 sout pout_from0 { wvalue y == f (contents p1 h0 sin pos) })
  ))
: Tot (x: lwriter s2 h0 sout pout_from0 { lwvalue x == List.Tot.map f (contents_list p1 h0 sin pin_from pin_to) } )
= LWriter (Ghost.hide (List.Tot.map f (contents_list p1 h0 sin pin_from pin_to))) (fun pout_from ->
    assert (k1.parser_kind_subkind == Some ParserStrong);
    let h = HST.get () in
    list_map
      j1
      s2
      f
      h
      sin pin_from pin_to
      sout pout_from
      (fun pin_ pout_ ->
        valid_pos_frame_strong p1 h0 sin pin_ (get_valid_pos p1 h sin pin_) (loc_slice_from sout pout_from0) h;
        write (f' pin_) pout_
      )
  )


(* With options (other failures) *)

inline_for_extraction
noextract
let fowriter
  (#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: option 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 - 1
  ))
  (ensures (fun h res h' ->
    B.modifies (loc_slice_from sout pout_from) h h' /\ (
    if res = max_uint32
    then (Some? x ==> U32.v pout_from + serialized_length s (Some?.v x) > U32.v sout.len)
    else if res = max_uint32 `U32.sub` 1ul
    then None? x
    else
    Some? x /\
    valid_content_pos p h' sout pout_from (Some?.v x) res
)))

inline_for_extraction
noextract
noeq
type owriter
  (#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
= | OWriter:
    (v: Ghost.erased (option t)) ->
    (w: fowriter s h0 sout pout_from0 (Ghost.reveal v)) ->
    owriter s h0 sout pout_from0

let owvalue
  (#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: owriter s h0 sout pout_from0)
: GTot (option t)
= Ghost.reveal w.v

inline_for_extraction
noextract
let weaken_owriter
  (#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: owriter s h0 sout pout_from0)
  (h1: HS.mem)
  (pout_from1: U32.t)
: Pure (w' : owriter s h1 sout pout_from1 { owvalue w' == owvalue w } )
  (requires (B.modifies (loc_slice_from sout pout_from0) h0 h1 /\ U32.v pout_from0 <= U32.v pout_from1))
  (ensures (fun _ -> True))
= OWriter w.v (fun pout_from -> w.w pout_from)

inline_for_extraction
noextract
let owrite
  (#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: owriter s h0 sout pout_from0)
: Tot (fowriter s h0 sout pout_from0 (owvalue w))
= match w with | OWriter _ f -> f

inline_for_extraction
noextract
let owriter_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 (owriter s h0 sout pout_from0)))
  (wfalse: (squash (cond == false) -> Tot (owriter s h0 sout pout_from0)))
: Tot (x: owriter s h0 sout pout_from0 { owvalue x == (if cond then owvalue (wtrue ()) else owvalue (wfalse ())) } )
= OWriter (if cond then OWriter?.v (wtrue ()) else OWriter?.v (wfalse ()))
  (fun pout_from -> if cond then owrite (wtrue ()) pout_from else owrite (wfalse ()) pout_from)

inline_for_extraction
noextract
let owrite_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: owriter s h0 sout pout_from0 { owvalue y == Some x } )
= OWriter (Ghost.hide (Some 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 owriter_of_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)
: Tot (x: owriter s h0 sout pout_from0 { owvalue x == Some (wvalue w) })
= OWriter (Ghost.hide (Some (wvalue w))) (fun pout_from -> write w pout_from)

inline_for_extraction
noextract
let folwriter
  (#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: option (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 - 1
  ))
  (ensures (fun h res h' ->
    B.modifies (loc_slice_from sout pout_from) h h' /\ (
    if res = max_uint32
    then (Some? x ==> U32.v pout_from + serialized_list_length s (Some?.v x) > U32.v sout.len)
    else if res = max_uint32 `U32.sub` 1ul
    then None? x
    else
      Some? x /\
      valid_list p h' sout pout_from res /\
      contents_list p h' sout pout_from res ==  (Some?.v x)
  )))

inline_for_extraction
noeq
noextract
type olwriter
  (#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
= | OLWriter:
      (v: Ghost.erased (option (list t))) ->
      (w: folwriter s h0 sout pout_from0 (Ghost.reveal v)) ->
      olwriter s h0 sout pout_from0

inline_for_extraction
noextract
let olwvalue
  (#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: olwriter s h0 sout pout_from0)
: GTot (option (list t))
= Ghost.reveal w.v

inline_for_extraction
noextract
let weaken_olwriter
  (#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: olwriter s h0 sout pout_from0)
  (h1: HS.mem)
  (pout_from1: U32.t)
: Pure (w' : olwriter s h1 sout pout_from1 { olwvalue w' == olwvalue w } )
  (requires (B.modifies (loc_slice_from sout pout_from0) h0 h1 /\ U32.v pout_from0 <= U32.v pout_from1))
  (ensures (fun _ -> True))
= OLWriter w.v (fun pout_from -> w.w pout_from)

inline_for_extraction
noextract
let olwrite
  (#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: olwriter s h0 sout pout_from0)
: Tot (folwriter s h0 sout pout_from0 (olwvalue w))
= match w with | OLWriter _ f -> f

inline_for_extraction
noextract
let olwriter_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: olwriter s h0 sout pout_from0 { olwvalue x == Some [] })
= OLWriter (Ghost.hide (Some []))
  (fun pout_from ->
    let h = HST.get () in
    valid_list_nil p h sout pout_from;
    pout_from
  )

inline_for_extraction
noextract
let olwriter_singleton
  (#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: owriter s h0 sout pout_from0)
: Tot (x: olwriter s h0 sout pout_from0 { olwvalue x == (match owvalue w with None -> None | Some x -> Some [x]) })
= OLWriter (Ghost.hide (match owvalue w with None -> None | Some x -> Some [x]))
  (fun pout_from ->
    let res = owrite w pout_from in
    if res `U32.lt` (max_uint32 `U32.sub` 1ul)
    then begin
      let h = HST.get () in
      valid_list_nil p h sout res;
      valid_list_cons p h sout pout_from res
    end else begin
      [@inline_let]
      let f () : Lemma (requires (Some? (owvalue w))) (ensures (match owvalue w with | None -> False | Some v -> serialized_list_length s [v] == serialized_length s v)) =
        serialized_list_length_cons s (Some?.v (owvalue w)) [];
        serialized_list_length_nil s
      in
      Classical.move_requires f ()
    end;
    res
  )

inline_for_extraction
noextract
let olwriter_append
  (#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)
  (w1 w2: olwriter s h0 sout pout_from0)
val olwriter_append
      (#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)
      (w1 w2: olwriter s h0 sout pout_from0)
    : Tot
    (x:
      olwriter s h0 sout pout_from0
        { olwvalue x ==
          (match olwvalue w1, olwvalue w2 with
            | Some l1, Some l2 -> Some (l1 `List.Tot.append` l2)
            | _ -> None) })

    w1: LowParse.Low.Writers.olwriter s h0 sout pout_from0 ->
    w2: LowParse.Low.Writers.olwriter s h0 sout pout_from0
  -> x:
    LowParse.Low.Writers.olwriter s h0 sout pout_from0
      { LowParse.Low.Writers.olwvalue x ==
        (match LowParse.Low.Writers.olwvalue w1, LowParse.Low.Writers.olwvalue w2 with
          | FStar.Pervasives.Native.Mktuple2
            #_
            #_
            (FStar.Pervasives.Native.Some #_ l1)
            (FStar.Pervasives.Native.Some #_ l2) ->
            FStar.Pervasives.Native.Some (l1 @ l2)
          | _ -> FStar.Pervasives.Native.None) }