val 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}
    )
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
  )
val 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}
    )
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)
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 Prims.l_and LowParse.Spec.Base.is_weaker_than LowParse.Low.Writers.SWriter LowParse.Spec.Base.weaken LowParse.Spec.Combinators.serialize_weaken FStar.Ghost.hide LowParse.Low.Writers.swvalue Prims.unit LowParse.Low.Base.valid_weaken FStar.HyperStack.ST.get LowParse.Low.Writers.swrite LowParse.Low.Base.Spec.serialized_length_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
val 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}
    )

    k2: LowParse.Spec.Base.parser_kind ->
    w1:
      LowParse.Low.Writers.swriter s1 h0 space_beyond sout pout_from0
        { LowParse.Spec.Base.is_weaker_than k2 k1 /\
          Mkparser_kind'?.parser_kind_subkind k2 ==
          FStar.Pervasives.Native.Some LowParse.Spec.Base.ParserStrong }
  -> w2:
    LowParse.Low.Writers.swriter (LowParse.Spec.Combinators.serialize_weaken k2 s1)
      h0
      space_beyond
      sout
      pout_from0 {LowParse.Low.Writers.swvalue w2 == LowParse.Low.Writers.swvalue w1}