val serialize_flbytes_correct (sz: nat{sz < 4294967296})
    : Lemma (serializer_correct (parse_flbytes sz) (serialize_flbytes' sz))
let serialize_flbytes_correct
  (sz: nat { sz < 4294967296 } )
: Lemma
  (serializer_correct (parse_flbytes sz) (serialize_flbytes' sz))
= let prf
    (input: B32.lbytes sz)
  : Lemma
    (
      let ser = serialize_flbytes' sz input in
      Seq.length ser == sz /\
      parse (parse_flbytes sz) ser == Some (input, sz)
    )
  = ()
  in
  Classical.forall_intro prf
val serialize_flbytes_correct (sz: nat{sz < 4294967296})
    : Lemma (serializer_correct (parse_flbytes sz) (serialize_flbytes' sz))
let serialize_flbytes_correct (sz: nat{sz < 4294967296})
    : Lemma (serializer_correct (parse_flbytes sz) (serialize_flbytes' sz)) =
let prf (input: B32.lbytes sz)
    : Lemma
    (let ser = serialize_flbytes' sz input in
      Seq.length ser == sz /\ parse (parse_flbytes sz) ser == Some (input, sz)) =
  ()
in
Classical.forall_intro prf
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.Classical.forall_intro FStar.Bytes.lbytes Prims.l_and Prims.eq2 FStar.Seq.Base.length LowParse.Bytes.byte LowParse.Spec.Bytes.serialize_flbytes' FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.consumed_length LowParse.Spec.Base.parse LowParse.Spec.Bytes.parse_flbytes FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 Prims.unit Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern LowParse.Bytes.bytes LowParse.Spec.Base.serializer_correct LowParse.Spec.Base.total_constant_size_parser_kind
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 } )
: Tot (bare_serializer (B32.lbytes sz))
= fun (x: B32.lbytes sz) -> (
    lt_pow2_32 sz;
    B32.reveal x
  )

let serialize_flbytes_correct
  (sz: nat { sz < 4294967296 } )
: Lemma
val serialize_flbytes_correct (sz: nat{sz < 4294967296})
    : Lemma (serializer_correct (parse_flbytes sz) (serialize_flbytes' sz))
sz: Prims.nat{sz < 4294967296}
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Base.serializer_correct (LowParse.Spec.Bytes.parse_flbytes sz)
        (LowParse.Spec.Bytes.serialize_flbytes' sz))