val parse_flbytes_gen (sz: nat{sz < 4294967296}) (s: bytes{Seq.length s == sz})
    : GTot (B32.lbytes sz)
let parse_flbytes_gen
  (sz: nat { sz < 4294967296 } )
  (s: bytes { Seq.length s == sz } )
: GTot (B32.lbytes sz)
= lt_pow2_32 sz;
  B32.hide s
val parse_flbytes_gen (sz: nat{sz < 4294967296}) (s: bytes{Seq.length s == sz})
    : GTot (B32.lbytes sz)
let parse_flbytes_gen (sz: nat{sz < 4294967296}) (s: bytes{Seq.length s == sz})
    : GTot (B32.lbytes sz) =
lt_pow2_32 sz;
B32.hide s
LowParse.Spec.Bytes.fst.checked
prims.fst.checked LowParse.Spec.VLGen.fst.checked LowParse.Bytes32.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.Bytes.fst
Prims.nat Prims.b2t Prims.op_LessThan LowParse.Bytes.bytes Prims.eq2 FStar.Seq.Base.length LowParse.Bytes.byte FStar.Bytes.hide Prims.unit LowParse.Spec.Bytes.lt_pow2_32 FStar.Bytes.lbytes
module LowParse.Spec.Bytes
include LowParse.Spec.VLGen

module B32 = LowParse.Bytes32
module Seq = FStar.Seq
module U32 = FStar.UInt32

#set-options "--z3rlimit 128 --max_fuel 64 --max_ifuel 64"

let lt_pow2_32
  (x: nat)
: Lemma
  (x < 4294967296 <==> x < pow2 32)
= ()

#reset-options

let parse_flbytes_gen
  (sz: nat { sz < 4294967296 } )
  (s: bytes { Seq.length s == sz } )
val parse_flbytes_gen (sz: nat{sz < 4294967296}) (s: bytes{Seq.length s == sz})
    : GTot (B32.lbytes sz)
sz: Prims.nat{sz < 4294967296} -> s: LowParse.Bytes.bytes{FStar.Seq.Base.length s == sz}
  -> Prims.GTot (FStar.Bytes.lbytes sz)