val parse32_flbytes (sz: nat) (sz': U32.t{U32.v sz' == sz})
    : Tot
    (lt_pow2_32 sz;
      parser32 (parse_flbytes sz))
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)
val parse32_flbytes (sz: nat) (sz': U32.t{U32.v sz' == sz})
    : Tot
    (lt_pow2_32 sz;
      parser32 (parse_flbytes sz))
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)
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
Prims.nat FStar.UInt32.t Prims.eq2 Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.b2t Prims.op_GreaterThanOrEqual FStar.UInt32.v LowParse.SLow.Combinators.make_total_constant_size_parser32 FStar.Bytes.lbytes LowParse.Spec.Bytes.parse_flbytes_gen LowParse.SLow.Bytes.parse32_flbytes_gen Prims.unit LowParse.Spec.Bytes.lt_pow2_32 LowParse.SLow.Base.parser32 LowParse.Spec.Base.total_constant_size_parser_kind LowParse.Spec.Bytes.parse_flbytes
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)
val parse32_flbytes (sz: nat) (sz': U32.t{U32.v sz' == sz})
    : Tot
    (lt_pow2_32 sz;
      parser32 (parse_flbytes sz))
sz: Prims.nat -> sz': FStar.UInt32.t{FStar.UInt32.v sz' == sz}
  -> (LowParse.Spec.Bytes.lt_pow2_32 sz;
      LowParse.SLow.Base.parser32 (LowParse.Spec.Bytes.parse_flbytes sz))