val swrite_nondep_then'
      (#h0: HS.mem)
      (#sout:
          slice (srel_of_buffer_srel (B.trivial_preorder _))
            (srel_of_buffer_srel (B.trivial_preorder _)))
      (#pout_from0: U32.t)
      (#k1: parser_kind)
      (#t1: Type)
      (#p1: parser k1 t1)
      (#s1: serializer p1 {k1.parser_kind_subkind == Some ParserStrong})
      (#space_beyond: nat)
      (w1: swriter s1 h0 space_beyond sout pout_from0)
      (#k2: parser_kind)
      (#t2: Type)
      (#p2: parser k2 t2)
      (#s2: serializer p2 {k2.parser_kind_subkind == Some ParserStrong})
      (w2: swriter s2 h0 space_beyond sout pout_from0)
    : Tot
    (w:
      swriter (s1 `serialize_nondep_then` s2) h0 space_beyond sout pout_from0
        {swvalue w == (swvalue w1, swvalue w2)})
let swrite_nondep_then'
  (#h0: HS.mem)
  (#sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (#pout_from0: U32.t)
  (#k1: parser_kind)
  (#t1: Type)
  (#p1: parser k1 t1)
  (#s1: serializer p1 { k1.parser_kind_subkind == Some ParserStrong })
  (#space_beyond: nat)
  (w1: swriter s1 h0 space_beyond sout pout_from0)
  (#k2: parser_kind)
  (#t2: Type)
  (#p2: parser k2 t2)
  (#s2: serializer p2 { k2.parser_kind_subkind == Some ParserStrong })
  (w2: swriter s2 h0 space_beyond sout pout_from0)
: Tot (w: swriter (s1 `serialize_nondep_then` s2) h0 space_beyond sout pout_from0 {
    swvalue w == (swvalue w1, swvalue w2)
  })
= SWriter (Ghost.hide (swvalue w1, swvalue w2)) (fun pout_from ->
    serialized_length_eq (s1 `serialize_nondep_then` s2) (swvalue w1, swvalue w2);
    serialize_nondep_then_eq s1 s2 (swvalue w1, swvalue w2);
    serialized_length_eq s1 (swvalue w1);
    serialized_length_eq s2 (swvalue w2);
    let pos1 = swrite w1 pout_from in
    let pos2 = swrite w2 pos1 in
    let h' = HST.get () in
    valid_nondep_then h' p1 p2 sout pout_from;
    pos2
  )
val swrite_nondep_then'
      (#h0: HS.mem)
      (#sout:
          slice (srel_of_buffer_srel (B.trivial_preorder _))
            (srel_of_buffer_srel (B.trivial_preorder _)))
      (#pout_from0: U32.t)
      (#k1: parser_kind)
      (#t1: Type)
      (#p1: parser k1 t1)
      (#s1: serializer p1 {k1.parser_kind_subkind == Some ParserStrong})
      (#space_beyond: nat)
      (w1: swriter s1 h0 space_beyond sout pout_from0)
      (#k2: parser_kind)
      (#t2: Type)
      (#p2: parser k2 t2)
      (#s2: serializer p2 {k2.parser_kind_subkind == Some ParserStrong})
      (w2: swriter s2 h0 space_beyond sout pout_from0)
    : Tot
    (w:
      swriter (s1 `serialize_nondep_then` s2) h0 space_beyond sout pout_from0
        {swvalue w == (swvalue w1, swvalue w2)})
let swrite_nondep_then'
      (#h0: HS.mem)
      (#sout:
          slice (srel_of_buffer_srel (B.trivial_preorder _))
            (srel_of_buffer_srel (B.trivial_preorder _)))
      (#pout_from0: U32.t)
      (#k1: parser_kind)
      (#t1: Type)
      (#p1: parser k1 t1)
      (#s1: serializer p1 {k1.parser_kind_subkind == Some ParserStrong})
      (#space_beyond: nat)
      (w1: swriter s1 h0 space_beyond sout pout_from0)
      (#k2: parser_kind)
      (#t2: Type)
      (#p2: parser k2 t2)
      (#s2: serializer p2 {k2.parser_kind_subkind == Some ParserStrong})
      (w2: swriter s2 h0 space_beyond sout pout_from0)
    : Tot
    (w:
      swriter (s1 `serialize_nondep_then` s2) h0 space_beyond sout pout_from0
        {swvalue w == (swvalue w1, swvalue w2)}) =
SWriter (Ghost.hide (swvalue w1, swvalue w2))
  (fun pout_from ->
      serialized_length_eq (s1 `serialize_nondep_then` s2) (swvalue w1, swvalue w2);
      serialize_nondep_then_eq s1 s2 (swvalue w1, swvalue w2);
      serialized_length_eq s1 (swvalue w1);
      serialized_length_eq s2 (swvalue w2);
      let pos1 = swrite w1 pout_from in
      let pos2 = swrite w2 pos1 in
      let h' = HST.get () in
      valid_nondep_then h' p1 p2 sout pout_from;
      pos2)
LowParse.Low.Writers.Instances.fst.checked
prims.fst.checked LowStar.Endianness.fst.checked LowStar.Buffer.fst.checked LowParse.Low.Writers.fst.checked LowParse.Low.Combinators.fsti.checked LowParse.Low.Bytes.fst.checked LowParse.Low.BitSum.fst.checked LowParse.Endianness.BitFields.fst.checked LowParse.BitFields.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Bytes.fsti.checked
LowParse.Low.Writers.Instances.fst
FStar.Monotonic.HyperStack.mem LowParse.Slice.slice LowParse.Slice.srel_of_buffer_srel LowParse.Bytes.byte LowStar.Buffer.trivial_preorder FStar.UInt32.t 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 Prims.nat LowParse.Low.Writers.swriter LowParse.Low.Writers.SWriter LowParse.Spec.Combinators.and_then_kind FStar.Pervasives.Native.tuple2 LowParse.Spec.Combinators.nondep_then LowParse.Spec.Combinators.serialize_nondep_then FStar.Ghost.hide FStar.Pervasives.Native.Mktuple2 LowParse.Low.Writers.swvalue Prims.unit LowParse.Low.Combinators.valid_nondep_then FStar.HyperStack.ST.get LowParse.Low.Writers.swrite LowParse.Low.Base.Spec.serialized_length_eq LowParse.Spec.Combinators.serialize_nondep_then_eq
module LowParse.Low.Writers.Instances
include LowParse.Low.Writers
include LowParse.Low.Combinators
include LowParse.Low.Bytes
include LowParse.Low.BitSum

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

inline_for_extraction
noextract
let swrite_weaken
  (#h0: HS.mem)
  (#sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (#pout_from0: U32.t)
  (#k1: parser_kind)
  (#t1: Type)
  (#p1: parser k1 t1)
  (#s1: serializer p1 { k1.parser_kind_subkind == Some ParserStrong })
  (#space_beyond: nat)
  (k2: parser_kind)
  (w1: swriter s1 h0 space_beyond sout pout_from0 {
    (k2 `is_weaker_than` k1) /\
    k2.parser_kind_subkind == Some ParserStrong
  })
: Tot (w2: swriter (serialize_weaken k2 s1) h0 space_beyond sout pout_from0 {
    swvalue w2 == swvalue w1
  })
= SWriter (Ghost.hide (swvalue w1)) (fun pout_from ->
    serialized_length_eq s1 (swvalue w1);
    serialized_length_eq (serialize_weaken k2 s1) (swvalue w1);
    let res = swrite w1 pout_from in
    let h = HST.get () in
    valid_weaken k2 p1 h sout pout_from;
    res
  )

inline_for_extraction
noextract
let swrite_nondep_then'
  (#h0: HS.mem)
  (#sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (#pout_from0: U32.t)
  (#k1: parser_kind)
  (#t1: Type)
  (#p1: parser k1 t1)
  (#s1: serializer p1 { k1.parser_kind_subkind == Some ParserStrong })
  (#space_beyond: nat)
  (w1: swriter s1 h0 space_beyond sout pout_from0)
  (#k2: parser_kind)
  (#t2: Type)
  (#p2: parser k2 t2)
  (#s2: serializer p2 { k2.parser_kind_subkind == Some ParserStrong })
  (w2: swriter s2 h0 space_beyond sout pout_from0)
: Tot (w: swriter (s1 `serialize_nondep_then` s2) h0 space_beyond sout pout_from0 {
    swvalue w == (swvalue w1, swvalue w2)
val swrite_nondep_then'
      (#h0: HS.mem)
      (#sout:
          slice (srel_of_buffer_srel (B.trivial_preorder _))
            (srel_of_buffer_srel (B.trivial_preorder _)))
      (#pout_from0: U32.t)
      (#k1: parser_kind)
      (#t1: Type)
      (#p1: parser k1 t1)
      (#s1: serializer p1 {k1.parser_kind_subkind == Some ParserStrong})
      (#space_beyond: nat)
      (w1: swriter s1 h0 space_beyond sout pout_from0)
      (#k2: parser_kind)
      (#t2: Type)
      (#p2: parser k2 t2)
      (#s2: serializer p2 {k2.parser_kind_subkind == Some ParserStrong})
      (w2: swriter s2 h0 space_beyond sout pout_from0)
    : Tot
    (w:
      swriter (s1 `serialize_nondep_then` s2) h0 space_beyond sout pout_from0
        {swvalue w == (swvalue w1, swvalue w2)})

    w1: LowParse.Low.Writers.swriter s1 h0 space_beyond sout pout_from0 ->
    w2: LowParse.Low.Writers.swriter s2 h0 space_beyond sout pout_from0
  -> w:
    LowParse.Low.Writers.swriter (LowParse.Spec.Combinators.serialize_nondep_then s1 s2)
      h0
      space_beyond
      sout
      pout_from0
      { LowParse.Low.Writers.swvalue w ==
        FStar.Pervasives.Native.Mktuple2 (LowParse.Low.Writers.swvalue w1)
          (LowParse.Low.Writers.swvalue w2) }