val parse32_all_bytes:parser32 parse_all_bytes
let parse32_all_bytes
  : parser32 parse_all_bytes
= fun (input: B32.bytes) ->
    let res = Some (input, B32.len input) in
    (res <: (res: option (bytes32 * U32.t) { parser32_correct parse_all_bytes input res } ))
val parse32_all_bytes:parser32 parse_all_bytes
let parse32_all_bytes:parser32 parse_all_bytes =
fun (input: B32.bytes) ->
  let res = Some (input, B32.len input) in
  (res <: (res: option (bytes32 * U32.t) {parser32_correct parse_all_bytes input res}))
LowParse.SLow.Bytes.fst.checked
prims.fst.checked LowParse.Spec.Bytes.fst.checked LowParse.SLow.VLGen.fst.checked LowParse.SLow.VLData.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked
LowParse.SLow.Bytes.fst
FStar.Bytes.bytes FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 LowParse.SLow.Base.bytes32 FStar.UInt32.t LowParse.SLow.Base.parser32_correct LowParse.Spec.Bytes.parse_all_bytes_kind LowParse.Spec.Bytes.parse_all_bytes FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 FStar.Bytes.len
module LowParse.SLow.Bytes
include LowParse.Spec.Bytes
include LowParse.SLow.VLData
include LowParse.SLow.VLGen

module B32 = FStar.Bytes
module Seq = FStar.Seq
module U32 = FStar.UInt32

inline_for_extraction
let parse32_flbytes_gen
  (sz: nat { sz < 4294967296 } )
  (x: B32.lbytes sz)
: Tot (y: B32.lbytes sz { y == parse_flbytes_gen sz (B32.reveal x) } )
= B32.hide_reveal x;
  x

#set-options "--z3rlimit 32"

inline_for_extraction
let parse32_flbytes
  (sz: nat)
  (sz' : U32.t { U32.v sz' == sz } )
: Tot (
     lt_pow2_32 sz;
     parser32 (parse_flbytes sz)
  )
= lt_pow2_32 sz;
  make_total_constant_size_parser32
    sz
    sz'
    #(B32.lbytes sz)
    (parse_flbytes_gen sz)
    ()
    (parse32_flbytes_gen sz)

inline_for_extraction
let serialize32_flbytes
  (sz: nat { sz < 4294967296 } )
: Tot (serializer32 (serialize_flbytes sz))
= fun (input: B32.lbytes sz) ->
    B32.hide_reveal input;
    (input <: (res: bytes32 { serializer32_correct (serialize_flbytes sz) input res } ))

inline_for_extraction
let parse32_all_bytes
val parse32_all_bytes:parser32 parse_all_bytes
LowParse.SLow.Base.parser32 LowParse.Spec.Bytes.parse_all_bytes