val swrite_bounded_vlgenbytes
      (h0: HS.mem)
      (sout:
          slice (srel_of_buffer_srel (B.trivial_preorder _))
            (srel_of_buffer_srel (B.trivial_preorder _)))
      (pout_from0: U32.t)
      (min: nat)
      (max: nat{min <= max /\ max > 0 /\ max < 4294967296})
      (#kk: parser_kind)
      (#pk: parser kk (bounded_int32 min max))
      (#sk: serializer pk {kk.parser_kind_subkind == Some ParserStrong})
      (wk: leaf_writer_strong sk)
      (len: U32.t{min <= U32.v len /\ U32.v len <= max})
      (b:
          B.buffer U8.t
            { B.live h0 b /\ B.length b == U32.v len /\
              B.loc_disjoint (B.loc_buffer b) (loc_slice_from sout pout_from0) })
    : Tot
    (w:
      swriter (serialize_bounded_vlgenbytes min max sk) h0 0 sout pout_from0
        {swvalue w == FB.hide (B.as_seq h0 b)})
let swrite_bounded_vlgenbytes
  (h0: HS.mem)
  (sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (pout_from0: U32.t)
  (min: nat)
  (max: nat { min <= max /\ max > 0 /\ max < 4294967296 })
  (#kk: parser_kind)
  (#pk: parser kk (bounded_int32 min max))
  (#sk: serializer pk { kk.parser_kind_subkind == Some ParserStrong })
  (wk: leaf_writer_strong sk)
  (len: U32.t { min <= U32.v len /\ U32.v len <= max })
  (b: B.buffer U8.t {
    B.live h0 b /\
    B.length b == U32.v len /\
    B.loc_disjoint (B.loc_buffer b) (loc_slice_from sout pout_from0)
  })
: Tot (w: swriter (serialize_bounded_vlgenbytes min max sk) h0 0 sout pout_from0 {
    swvalue w == FB.hide (B.as_seq h0 b)
  })
= SWriter (Ghost.hide (FB.hide (B.as_seq h0 b))) (fun pout_from ->
    serialized_length_eq (serialize_bounded_vlgenbytes min max sk) (FB.hide (B.as_seq h0 b));
    length_serialize_bounded_vlgenbytes min max sk (FB.hide (B.as_seq h0 b));
    serialized_length_eq sk len;
    let pout_payload = swrite (swrite_leaf wk h0 sout pout_from0 len) pout_from in
    let payload = B.sub sout.base pout_payload len in
    B.blit b 0ul payload 0ul len;
    let h = HST.get () in
    valid_bounded_vlgenbytes min max pk sout pout_from h;
    pout_payload `U32.add` len
  )
val swrite_bounded_vlgenbytes
      (h0: HS.mem)
      (sout:
          slice (srel_of_buffer_srel (B.trivial_preorder _))
            (srel_of_buffer_srel (B.trivial_preorder _)))
      (pout_from0: U32.t)
      (min: nat)
      (max: nat{min <= max /\ max > 0 /\ max < 4294967296})
      (#kk: parser_kind)
      (#pk: parser kk (bounded_int32 min max))
      (#sk: serializer pk {kk.parser_kind_subkind == Some ParserStrong})
      (wk: leaf_writer_strong sk)
      (len: U32.t{min <= U32.v len /\ U32.v len <= max})
      (b:
          B.buffer U8.t
            { B.live h0 b /\ B.length b == U32.v len /\
              B.loc_disjoint (B.loc_buffer b) (loc_slice_from sout pout_from0) })
    : Tot
    (w:
      swriter (serialize_bounded_vlgenbytes min max sk) h0 0 sout pout_from0
        {swvalue w == FB.hide (B.as_seq h0 b)})
let swrite_bounded_vlgenbytes
      (h0: HS.mem)
      (sout:
          slice (srel_of_buffer_srel (B.trivial_preorder _))
            (srel_of_buffer_srel (B.trivial_preorder _)))
      (pout_from0: U32.t)
      (min: nat)
      (max: nat{min <= max /\ max > 0 /\ max < 4294967296})
      (#kk: parser_kind)
      (#pk: parser kk (bounded_int32 min max))
      (#sk: serializer pk {kk.parser_kind_subkind == Some ParserStrong})
      (wk: leaf_writer_strong sk)
      (len: U32.t{min <= U32.v len /\ U32.v len <= max})
      (b:
          B.buffer U8.t
            { B.live h0 b /\ B.length b == U32.v len /\
              B.loc_disjoint (B.loc_buffer b) (loc_slice_from sout pout_from0) })
    : Tot
    (w:
      swriter (serialize_bounded_vlgenbytes min max sk) h0 0 sout pout_from0
        {swvalue w == FB.hide (B.as_seq h0 b)}) =
SWriter (Ghost.hide (FB.hide (B.as_seq h0 b)))
  (fun pout_from ->
      serialized_length_eq (serialize_bounded_vlgenbytes min max sk) (FB.hide (B.as_seq h0 b));
      length_serialize_bounded_vlgenbytes min max sk (FB.hide (B.as_seq h0 b));
      serialized_length_eq sk len;
      let pout_payload = swrite (swrite_leaf wk h0 sout pout_from0 len) pout_from in
      let payload = B.sub sout.base pout_payload len in
      B.blit b 0ul payload 0ul len;
      let h = HST.get () in
      valid_bounded_vlgenbytes min max pk sout pout_from h;
      pout_payload `U32.add` len)
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 Prims.nat Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.op_GreaterThan Prims.op_LessThan LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.BoundedInt.bounded_int32 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 LowParse.Low.Base.leaf_writer_strong FStar.UInt32.v LowStar.Buffer.buffer FStar.UInt8.t LowStar.Monotonic.Buffer.live Prims.int Prims.l_or Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt32.n LowStar.Monotonic.Buffer.length LowStar.Monotonic.Buffer.loc_disjoint LowStar.Monotonic.Buffer.loc_buffer LowParse.Slice.loc_slice_from LowParse.Low.Writers.SWriter LowParse.Spec.VLGen.parse_bounded_vlgen_kind LowParse.Spec.Bytes.parse_all_bytes_kind LowParse.Spec.Bytes.parse_bounded_vlbytes_t LowParse.Spec.Bytes.parse_bounded_vlgenbytes LowParse.Spec.Bytes.serialize_bounded_vlgenbytes FStar.Ghost.hide FStar.Bytes.hide LowStar.Monotonic.Buffer.as_seq FStar.UInt32.add Prims.unit LowParse.Low.Bytes.valid_bounded_vlgenbytes FStar.HyperStack.ST.get LowStar.Monotonic.Buffer.blit FStar.UInt32.__uint_to_t LowStar.Monotonic.Buffer.mbuffer LowStar.Buffer.sub LowParse.Slice.__proj__Mkslice__item__base LowParse.Low.Writers.swrite LowParse.Low.Writers.swrite_leaf LowParse.Low.Base.Spec.serialized_length_eq LowParse.Spec.Bytes.length_serialize_bounded_vlgenbytes LowParse.Low.Writers.swriter FStar.Bytes.bytes LowParse.Low.Writers.swvalue
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)
  })
= 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
  )

let max (x1 x2: nat) : Tot nat = if x1 > x2 then x1 else x2

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_beyond1: nat)
  (w1: swriter s1 h0 space_beyond1 sout pout_from0)
  (#k2: parser_kind)
  (#t2: Type)
  (#p2: parser k2 t2)
  (#s2: serializer p2 { k2.parser_kind_subkind == Some ParserStrong })
  (#space_beyond2: nat)
  (w2: swriter s2 h0 space_beyond2 sout pout_from0)
: Tot (w: swriter (s1 `serialize_nondep_then` s2) h0 (space_beyond1 `max` space_beyond2) sout pout_from0 {
    swvalue w == (swvalue w1, swvalue w2)
  })
= [@inline_let]
  let sbmax = space_beyond1 `max` space_beyond2 in
  weaken_swriter w1 h0 sbmax pout_from0 `swrite_nondep_then'` weaken_swriter w2 h0 sbmax pout_from0

inline_for_extraction
noextract
let swrite_filter
  (#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)
  (cond: (t1 -> GTot bool)) 
  (w1: swriter s1 h0 space_beyond sout pout_from0 { cond (swvalue w1) } )
: Tot (w2: swriter (serialize_filter s1 cond) h0 space_beyond sout pout_from0 {
    swvalue w2 == swvalue w1
  })
= SWriter (Ghost.hide (swvalue w1)) (fun pout_from ->
    serialized_length_eq (serialize_filter s1 cond) (swvalue w1);
    serialized_length_eq s1 (swvalue w1);
    let res = swrite w1 pout_from in
    let h = HST.get () in
    valid_filter h p1 cond sout pout_from;
    res
  )

inline_for_extraction
noextract
let swrite_synth
  (#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)
  (#t2: Type)
  (f12: (t1 -> GTot t2))
  (f21: (t2 -> GTot t1))
  (prf: squash (
    synth_injective f12 /\
    synth_inverse f12 f21
  ))
: Tot (w2: swriter (serialize_synth p1 f12 s1 f21 ()) h0 space_beyond sout pout_from0 {
    swvalue w2 == f12 (swvalue w1) /\
    swvalue w1 == f21 (swvalue w2)
  })
= [@inline_let] let _ =
    serialize_synth_eq p1 f12 s1 f21 () (f12 (swvalue w1));
    synth_injective_synth_inverse_synth_inverse_recip f12 f21 ()
  in
  SWriter (Ghost.hide (f12 (swvalue w1))) (fun pout_from ->
    serialized_length_eq (serialize_synth p1 f12 s1 f21 ()) (f12 (swvalue w1));
    serialized_length_eq s1 (swvalue w1);
    let res = swrite w1 pout_from in
    let h = HST.get () in
    valid_synth h p1 f12 sout pout_from;
    res
  )

module U8 = FStar.UInt8
module FB = FStar.Bytes

#push-options "--z3rlimit 16"

inline_for_extraction
noextract
let swrite_flbytes
  (h0: HS.mem)
  (sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (pout_from0: U32.t)
  (len: U32.t)
  (b: B.buffer U8.t {
    B.live h0 b /\
    B.length b == U32.v len /\
    B.loc_disjoint (B.loc_buffer b) (loc_slice_from sout pout_from0)
  })
: Tot (w: swriter (serialize_flbytes (U32.v len)) h0 0 sout pout_from0 {
    swvalue w == FB.hide (B.as_seq h0 b)
  })
= SWriter (Ghost.hide (FB.hide (B.as_seq h0 b))) (fun pout_from ->
    serialized_length_eq (serialize_flbytes (U32.v len)) (FB.hide (B.as_seq h0 b));
    let payload = B.sub sout.base pout_from len in
    B.blit b 0ul payload 0ul len;
    let h = HST.get () in
    valid_flbytes_intro h (U32.v len) sout pout_from;
    pout_from `U32.add` len
  )

inline_for_extraction
noextract
let swrite_bounded_vlbytes
  (h0: HS.mem)
  (sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (pout_from0: U32.t)
  (min: nat)
  (max: nat { min <= max /\ max > 0 /\ max < 4294967296 })
  (len: U32.t { min <= U32.v len /\ U32.v len <= max })
  (b: B.buffer U8.t {
    B.length b == U32.v len /\
    B.live h0 b /\
    B.loc_disjoint (B.loc_buffer b) (loc_slice_from sout pout_from0)
  })
: Tot (w: swriter (serialize_bounded_vlbytes min max) h0 0 sout pout_from0 {
    swvalue w == FB.hide (B.as_seq h0 b)
  })
= SWriter (Ghost.hide (FB.hide (B.as_seq h0 b))) (fun pout_from ->
    serialized_length_eq (serialize_bounded_vlbytes min max) (FB.hide (B.as_seq h0 b));
    length_serialize_bounded_vlbytes min max (FB.hide (B.as_seq h0 b));
    let pout_payload = pout_from `U32.add` U32.uint_to_t (log256' max) in
    let payload = B.sub sout.base pout_payload len in
    B.blit b 0ul payload 0ul len;
    finalize_bounded_vlbytes min max sout pout_from len
  )

inline_for_extraction
noextract
let swrite_bounded_vlgenbytes
  (h0: HS.mem)
  (sout: slice (srel_of_buffer_srel (B.trivial_preorder _)) (srel_of_buffer_srel (B.trivial_preorder _)))
  (pout_from0: U32.t)
  (min: nat)
  (max: nat { min <= max /\ max > 0 /\ max < 4294967296 })
  (#kk: parser_kind)
  (#pk: parser kk (bounded_int32 min max))
  (#sk: serializer pk { kk.parser_kind_subkind == Some ParserStrong })
  (wk: leaf_writer_strong sk)
  (len: U32.t { min <= U32.v len /\ U32.v len <= max })
  (b: B.buffer U8.t {
    B.live h0 b /\
    B.length b == U32.v len /\
    B.loc_disjoint (B.loc_buffer b) (loc_slice_from sout pout_from0)
  })
: Tot (w: swriter (serialize_bounded_vlgenbytes min max sk) h0 0 sout pout_from0 {
    swvalue w == FB.hide (B.as_seq h0 b)
val swrite_bounded_vlgenbytes
      (h0: HS.mem)
      (sout:
          slice (srel_of_buffer_srel (B.trivial_preorder _))
            (srel_of_buffer_srel (B.trivial_preorder _)))
      (pout_from0: U32.t)
      (min: nat)
      (max: nat{min <= max /\ max > 0 /\ max < 4294967296})
      (#kk: parser_kind)
      (#pk: parser kk (bounded_int32 min max))
      (#sk: serializer pk {kk.parser_kind_subkind == Some ParserStrong})
      (wk: leaf_writer_strong sk)
      (len: U32.t{min <= U32.v len /\ U32.v len <= max})
      (b:
          B.buffer U8.t
            { B.live h0 b /\ B.length b == U32.v len /\
              B.loc_disjoint (B.loc_buffer b) (loc_slice_from sout pout_from0) })
    : Tot
    (w:
      swriter (serialize_bounded_vlgenbytes min max sk) h0 0 sout pout_from0
        {swvalue w == FB.hide (B.as_seq h0 b)})

    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 ->
    min: Prims.nat ->
    max: Prims.nat{min <= max /\ max > 0 /\ max < 4294967296} ->
    wk: LowParse.Low.Base.leaf_writer_strong sk ->
    len: FStar.UInt32.t{min <= FStar.UInt32.v len /\ FStar.UInt32.v len <= max} ->
    b:
      LowStar.Buffer.buffer FStar.UInt8.t
        { LowStar.Monotonic.Buffer.live h0 b /\
          LowStar.Monotonic.Buffer.length b == FStar.UInt32.v len /\
          LowStar.Monotonic.Buffer.loc_disjoint (LowStar.Monotonic.Buffer.loc_buffer b)
            (LowParse.Slice.loc_slice_from sout pout_from0) }
  -> w:
    LowParse.Low.Writers.swriter (LowParse.Spec.Bytes.serialize_bounded_vlgenbytes min max sk)
      h0
      0
      sout
      pout_from0
      {LowParse.Low.Writers.swvalue w == FStar.Bytes.hide (LowStar.Monotonic.Buffer.as_seq h0 b)}