val serialize_flbytes' (sz: nat{sz < 4294967296}) : Tot (bare_serializer (B32.lbytes sz))
let serialize_flbytes'
  (sz: nat { sz < 4294967296 } )
: Tot (bare_serializer (B32.lbytes sz))
= fun (x: B32.lbytes sz) -> (
    lt_pow2_32 sz;
    B32.reveal x
  )
val serialize_flbytes' (sz: nat{sz < 4294967296}) : Tot (bare_serializer (B32.lbytes sz))
let serialize_flbytes' (sz: nat{sz < 4294967296}) : Tot (bare_serializer (B32.lbytes sz)) =
fun (x: B32.lbytes sz) ->
  (lt_pow2_32 sz;
    B32.reveal x)
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 FStar.Bytes.lbytes FStar.Bytes.reveal Prims.unit LowParse.Spec.Bytes.lt_pow2_32 LowParse.Bytes.bytes LowParse.Spec.Base.bare_serializer
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 } )
: GTot (B32.lbytes sz)
= lt_pow2_32 sz;
  B32.hide s

let parse_flbytes
  (sz: nat { sz < 4294967296 } )
: Tot (parser (total_constant_size_parser_kind sz) (B32.lbytes sz))
= make_total_constant_size_parser sz (B32.lbytes sz) (parse_flbytes_gen sz)

let serialize_flbytes'
  (sz: nat { sz < 4294967296 } )
val serialize_flbytes' (sz: nat{sz < 4294967296}) : Tot (bare_serializer (B32.lbytes sz))
sz: Prims.nat{sz < 4294967296} -> LowParse.Spec.Base.bare_serializer (FStar.Bytes.lbytes sz)