feat: std::initializer_list

[jhaag-skylabs-ai]

Tip

References:

• https://eel.is/c++draft/dcl.init.list
• https://en.cppreference.com/cpp/utility/initializer_list

Specifications for std::initializer_list, cf. SkyLabsAI/BRiCk#281.

[skylabs-ai-ci]

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/brick-libcpp/	feat/CxxStdInitializerListExpr	dca568d	c30ae4a	main	394e769	#112
fmdeps/BRiCk/	feat/CxxStdInitializerListExpr	392cc6f	86f104e	main	a9c5a18	#281
fmdeps/auto/	feat/CxxStdInitializerListExpr	c0d348f	295af0d	main	bd95ecd	#368

Passive Repos

Repo	Job Branch	Job Commit
./	main	9d4bec2
fmdeps/auto-docs/	main	f3ece99
bluerock/NOVA/	skylabs-proof	d802253
bluerock/bhv/	skylabs-main	bd2be4a
fmdeps/ci/	main	3972352
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
psi/data/	main	b01668d
vendored/rocq/	skylabs-master	bef7df5
fmdeps/rocq-agent-toolkit/	main	a53a09f
vendored/rocq-elpi/	skylabs-master	be1ffc5
vendored/rocq-equations/	skylabs-main	d1f944a
vendored/rocq-ext-lib/	skylabs-master	a31ad69
vendored/rocq-iris/	skylabs-master	a7af9f7
vendored/rocq-lsp/	skylabs-main	64ef78a
vendored/rocq-stdlib/	skylabs-master	00897b3
vendored/rocq-stdpp/	skylabs-master	0c5e505
fmdeps/skylabs-fm/	main	6350e97
vendored/vsrocq/	skylabs-main	ee79e7a

Performance

Relative	Master	MR	Change	Filename
+0.22%	141896.9	142203.5	+306.6	total
-0.00%	32798.5	32798.4	-0.2	├ translation units
+0.28%	109098.4	109405.1	+306.7	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-6.69%	22.4	20.9	-1.5	fmdeps/auto-docs/content/docs/debugging/main.v
-5.56%	24.6	23.3	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/allocation_lambda_forms.v
-5.37%	20.2	19.1	-1.1	fmdeps/auto-docs/content/docs/control_flow/loop.v
-4.21%	25.6	24.5	-1.1	fmdeps/auto-docs/content/docs/class_reps/alt.v
-3.76%	36.9	35.5	-1.4	fmdeps/auto-docs/content/docs/functions/verification.v
-0.74%	302.2	299.9	-2.2	fmdeps/auto/rocq-skylabs-auto-cpp/tests/arith_bug.v
-0.43%	249.0	247.9	-1.1	bluerock/bhv/apps/vswitch/lib/port/proof/port/defs.v
-0.31%	378.1	376.9	-1.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/conclude_chain_use.v
+0.10%	1180.1	1181.3	+1.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/sync_impl.v
+0.12%	1067.5	1068.8	+1.3	bluerock/bhv/apps/vmm/proof/main_cpp_proof/zeta_main.v
+0.13%	951.8	953.1	+1.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_cpp_proof.v
+0.14%	739.2	740.3	+1.1	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/setup.v
+0.17%	606.1	607.1	+1.0	bluerock/bhv/apps/umx/proof/main_cpp_proof/scanner_state.v
+0.18%	1800.4	1803.6	+3.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v
+0.18%	867.6	869.1	+1.5	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_default_impl.v
+0.18%	903.5	905.2	+1.6	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/setup.v
+0.18%	763.0	764.4	+1.4	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_proof.v
+0.18%	871.5	873.1	+1.6	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/reset_cpu.v
+0.21%	627.0	628.3	+1.3	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/misc.v
+0.22%	666.1	667.5	+1.5	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/copy.v
+0.25%	491.0	492.3	+1.2	bluerock/bhv/zeta/lib/concurrent/proof/lossy_queue2_hpp_proof.v
+0.26%	475.5	476.8	+1.2	bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/recv.v
+0.28%	534.5	535.9	+1.5	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/spec.v
+0.28%	467.6	468.9	+1.3	bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_private.v
+0.31%	530.6	532.2	+1.6	bluerock/bhv/apps/vmm/proof/main_cpp_proof/run_vm.v
+0.31%	340.7	341.8	+1.1	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort.v
+0.32%	517.3	518.9	+1.7	bluerock/bhv/lib/drivers/serial/pl011/proof/pl011_cpp_proof.v
+0.34%	326.7	327.8	+1.1	bluerock/bhv/apps/umx/proof/main_cpp_proof/setup.v
+0.34%	466.7	468.3	+1.6	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/msr_framework.v
+0.35%	398.9	400.3	+1.4	bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_cpp_proof/access.v
+0.36%	383.1	384.4	+1.4	bluerock/bhv/lib/vrl/proof/vrl/dataplane_hpp_proof.v
+0.36%	458.4	460.1	+1.7	bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/access.v
+0.37%	324.3	325.5	+1.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/async_copy_cookie.v
+0.39%	329.3	330.6	+1.3	bluerock/bhv/zeta/lib/cxx/proof/sys/semaphore_hpp_proof.v
+0.44%	472.2	474.3	+2.1	bluerock/bhv/apps/vswitch/lib/port/proof/port/proof.v
+0.45%	297.4	298.8	+1.4	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/wp_vcpu_lemmas.v
+0.46%	253.9	255.1	+1.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/TO_UPSTREAM.v
+0.47%	312.4	313.8	+1.5	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/resume.v
+0.48%	230.4	231.5	+1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/flood.v
+0.50%	255.0	256.3	+1.3	bluerock/bhv/apps/vmm/lib/bluerock/proof/aarch64/reg_accessor_hpp_proof.v
+0.51%	719.9	723.6	+3.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/virtual_interface.v
+0.51%	464.6	467.0	+2.4	bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/zynqmp_dma_ver_cpp_proof.v
+0.51%	233.5	234.7	+1.2	bluerock/bhv/apps/vmm/proof/main_cpp_spec.v
+0.53%	334.9	336.7	+1.8	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/handle_data_abort.v
+0.54%	230.9	232.2	+1.2	bluerock/bhv/apps/umx/proof/admin_cpp_proof/read_line.v
+0.55%	218.4	219.6	+1.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort_to_vbus.v
+0.55%	226.1	227.4	+1.2	bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/msr_hpp_proof.v
+0.56%	839.8	844.5	+4.7	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/proof.v
+0.60%	206.6	207.8	+1.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/ctor.v
+0.61%	265.1	266.8	+1.6	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_on.v
+0.62%	182.3	183.5	+1.1	bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/memory_hpp_proof.v
+0.64%	179.8	180.9	+1.1	bluerock/bhv/apps/umx/proof/main_cpp_proof/parse_connect_args.v
+0.65%	203.3	204.7	+1.3	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/check_reset.v
+0.68%	258.0	259.8	+1.8	bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/mmio.v
+0.70%	196.5	197.9	+1.4	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/defs.v
+0.70%	711.0	716.0	+5.0	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/misc.v
+0.75%	143.4	144.5	+1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/walk_chain.v
+0.75%	193.2	194.7	+1.4	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/queue/misc.v
+0.75%	163.1	164.3	+1.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/reset.v
+0.76%	149.4	150.6	+1.1	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/compute_gpa_fault_addr.v
+0.77%	356.2	358.9	+2.7	bluerock/bhv/apps/vswitch/lib/vsmp/proof/msg_queue_hpp/proof.v
+0.79%	201.6	203.2	+1.6	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/iterator.v
+0.80%	205.0	206.7	+1.6	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/conclude_chain_use.v
+0.81%	153.4	154.7	+1.2	bluerock/bhv/apps/vmm/vml/devices/vuart/proof/seq_queue_proof.v
+0.81%	193.0	194.5	+1.6	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_cpp_proof/space_sel.v
+0.81%	197.3	198.9	+1.6	bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_public.v
+0.81%	213.9	215.7	+1.7	bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_read_console_id.v
+0.82%	152.8	154.1	+1.2	bluerock/bhv/zeta/lib/nova/proof/safe_proof/safe_proof.v
+0.83%	146.6	147.8	+1.2	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_roundedup.v
+0.85%	130.6	131.8	+1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtual_interface.v
+0.86%	146.3	147.5	+1.3	bluerock/bhv/lib/drivers/serial/pl011/proof/mmio.v
+0.87%	141.8	143.0	+1.2	bluerock/bhv/apps/vmm/vml/devices/gic/proof/model/gic_hpp_spec.v
+0.89%	138.6	139.9	+1.2	bluerock/bhv/zeta/lib/concurrent/proof/lock_hpp_proof.v
+0.90%	139.1	140.4	+1.3	bluerock/bhv/zeta/lib/intrusive/proof/refcounted_proof.v
+0.90%	143.6	144.9	+1.3	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/handle_msr_exit.v
+0.91%	174.0	175.6	+1.6	bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_base_proof.v
+0.92%	375.0	378.4	+3.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/extract_frame_header.v
+0.92%	132.0	133.2	+1.2	bluerock/bhv/apps/vmm/proof/main_cpp_proof/proof.v
+0.92%	192.8	194.6	+1.8	bluerock/bhv/zeta/lib/intrusive/proof/shared_pointer_hpp_proof.v
+0.93%	146.4	147.7	+1.4	bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command.v
+0.95%	143.1	144.5	+1.4	bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/msr_cpp_proof.v
+0.95%	134.1	135.4	+1.3	bluerock/bhv/zeta/lib/concurrent/proof/ticket_lock_cpp_proof.v
+0.96%	132.8	134.1	+1.3	bluerock/bhv/zeta/lib/lang/proof/bits_hpp_proof.v
+0.98%	128.3	129.6	+1.3	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_emulating.v
+0.98%	147.6	149.1	+1.5	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/devq/send.v
+0.99%	131.8	133.1	+1.3	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_off.v
+0.99%	101.7	102.7	+1.0	bluerock/bhv/apps/vswitch/proof/ghost.v
+1.01%	125.7	126.9	+1.3	bluerock/bhv/zeta/lib/msc/proof/sys/signal_hpp_proof.v
+1.06%	164.6	166.4	+1.8	bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_other.v
+1.07%	120.9	122.2	+1.3	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/lookup.v
+1.07%	121.0	122.3	+1.3	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/create.v
+1.08%	115.2	116.5	+1.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/spec.v
+1.13%	111.0	112.2	+1.3	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/startup.v
+1.14%	115.5	116.8	+1.3	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/spec.v
+1.14%	89.2	90.2	+1.0	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/devq/used_event_notify.v
+1.15%	100.2	101.4	+1.2	bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_proof.v
+1.16%	106.7	107.9	+1.2	bluerock/bhv/apps/umx/proof/main_cpp_proof/output_loop.v
+1.20%	103.0	104.2	+1.2	bluerock/bhv/zeta/lib/lang/proof/string_cpp_proof.v
+1.23%	111.1	112.4	+1.4	bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_rich_proof.v
+1.24%	98.2	99.4	+1.2	bluerock/bhv/lib/vrl/proof/vrl/port_hpp_proof.v
+1.25%	143.2	145.0	+1.8	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/defs.v
+1.29%	88.0	89.1	+1.1	bluerock/bhv/zeta/lib/cxx/proof/bitset_hpp_proof.v
+1.30%	93.2	94.4	+1.2	bluerock/bhv/apps/vswitch/proof/model/vswitch/lemmas.v
+1.31%	76.6	77.6	+1.0	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/pkt.v
+1.33%	134.3	136.0	+1.8	bluerock/bhv/zeta/lib/zeta/proof/semaphore_hpp_proof.v
+1.37%	122.2	123.8	+1.7	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/init_info.v
+1.37%	76.6	77.7	+1.1	bluerock/bhv/apps/umx/proof/main_cpp_proof/setup_sigs.v
+1.39%	91.3	92.6	+1.3	bluerock/bhv/apps/vmm/proof/main_cpp_proof/get_fdt_from_uuid.v
+1.45%	80.2	81.4	+1.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/TO_UPSTREAM.v
+1.47%	101.5	103.0	+1.5	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/drop.v
+1.47%	83.4	84.6	+1.2	bluerock/bhv/zeta/lib/lang/proof/endian16_hpp_proof.v
+1.48%	98.8	100.3	+1.5	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_other.v
+1.61%	76.8	78.0	+1.2	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxshared/ctor.v
+1.65%	79.1	80.4	+1.3	bluerock/bhv/zeta/lib/lang/proof/compiler_hpp_proof.v
+1.65%	85.8	87.2	+1.4	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/spec.v
+1.71%	69.1	70.3	+1.2	bluerock/bhv/apps/umx/proof/admin_cpp_proof/read_escape.v
+1.71%	73.7	74.9	+1.3	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxclient/init_ctor.v
+1.78%	65.2	66.3	+1.2	bluerock/bhv/zeta/lib/lang/proof/endian8_hpp_proof.v
+1.81%	62.5	63.7	+1.1	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/desc_metadata.v
+1.83%	94.6	96.3	+1.7	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/start_cpu.v
+1.83%	85.0	86.5	+1.6	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_cpp_proof/proof.v
+1.86%	57.4	58.4	+1.1	bluerock/bhv/apps/umx/proof/main_cpp_proof/copy_bytes_and_flush.v
+1.91%	61.4	62.6	+1.2	bluerock/bhv/zeta/lib/lang/proof/endian32_hpp_proof.v
+1.92%	84.5	86.1	+1.6	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_spec.v
+1.93%	63.4	64.6	+1.2	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/insert.v
+1.93%	61.1	62.3	+1.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/ctor.v
+1.94%	63.4	64.6	+1.2	bluerock/bhv/apps/umx/proof/admin_cpp_proof/admin_console.v
+1.97%	67.1	68.4	+1.3	bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/defs.v
+1.99%	59.6	60.8	+1.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/linearized_desc.v
+2.03%	111.2	113.5	+2.3	bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/hints.v
+2.06%	75.2	76.7	+1.6	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/base_startup_handler.v
+2.08%	122.8	125.4	+2.6	bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/proof.v
+2.09%	112.1	114.5	+2.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/util.v
+2.10%	84.5	86.3	+1.8	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctor.v
+2.10%	57.8	59.0	+1.2	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxshared/nth_client.v
+2.12%	58.1	59.4	+1.2	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_merge.v
+2.32%	55.3	56.6	+1.3	bluerock/bhv/zeta/lib/lang/proof/endian64_hpp_proof.v
+2.32%	84.8	86.8	+2.0	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/roundup_parallel_proof.v
+2.36%	53.4	54.7	+1.3	bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_cpp_proof.v
+2.36%	46.3	47.4	+1.1	bluerock/bhv/apps/umx/proof/main_cpp_proof/setup_output_loop_thread.v
+2.37%	52.2	53.4	+1.2	bluerock/bhv/apps/vswitch/lib/protocol/proof/virtio_net_hpp/proof.v
+2.38%	51.9	53.1	+1.2	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/hints.v
+2.41%	52.1	53.3	+1.3	bluerock/bhv/apps/vmm/vml/devices/msr/proof/msr_access_hpp_proof.v
+2.44%	81.9	83.9	+2.0	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/extract_frame_header.v
+2.52%	65.4	67.1	+1.7	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/resume_all.v
+2.56%	44.4	45.5	+1.1	bluerock/bhv/zeta/lib/bson/proof/bson_hints.v
+2.62%	48.1	49.4	+1.3	bluerock/NOVA/build-proof/proof/pd_cpp_proof/hints.v
+2.65%	57.2	58.7	+1.5	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/requesters.v
+2.66%	46.1	47.3	+1.2	bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_cpp_proof/lookup.v
+2.69%	43.8	44.9	+1.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/run.v
+2.71%	53.6	55.1	+1.5	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/virtio_net_header_hints.v
+2.72%	45.6	46.9	+1.2	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctrl_feature_reset.v
+2.73%	61.1	62.8	+1.7	bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/esr_hpp_proof.v
+2.80%	42.2	43.4	+1.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/ghost.v
+2.81%	37.8	38.9	+1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/vqueue_interface.v
+2.81%	41.8	43.0	+1.2	bluerock/bhv/zeta/lib/zeta/proof/signal_hpp_proof.v
+2.89%	42.0	43.2	+1.2	bluerock/bhv/apps/vswitch/proof/upstream/hints.v
+2.93%	45.6	46.9	+1.3	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/guest_chunk_repo_hpp_proof.v
+2.98%	49.7	51.2	+1.5	bluerock/bhv/apps/vmm/vml/devices/simple_as/proof/simple_as_hpp_spec.v
+3.02%	42.4	43.7	+1.3	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_split_range.v
+3.06%	85.0	87.6	+2.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/send.v
+3.07%	52.9	54.5	+1.6	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/guest_as_hpp_proof.v
+3.13%	80.3	82.8	+2.5	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/drop.v
+3.15%	58.5	60.3	+1.8	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/roundup_all.v
+3.18%	38.0	39.2	+1.2	bluerock/bhv/lib/vrl/proof/vrl/port_list_hints.v
+3.22%	37.7	38.9	+1.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/available/misc.v
+3.23%	38.0	39.2	+1.2	bluerock/bhv/lib/vrl/proof/vrl/packet_hpp_proof.v
+3.25%	37.7	38.9	+1.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/used/misc.v
+3.26%	39.2	40.5	+1.3	bluerock/bhv/apps/umx/proof/admin_hints.v
+3.28%	44.6	46.1	+1.5	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/cpp_hints.v
+3.28%	37.9	39.2	+1.2	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/cpu_feature_hpp_derived_specs.v
+3.33%	37.4	38.7	+1.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/descriptor/misc.v
+3.34%	44.8	46.3	+1.5	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/lec_stack_size.v
+3.40%	69.2	71.5	+2.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/copy_frame.v
+3.40%	33.7	34.9	+1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/set_virtio_net_header.v
+3.43%	35.2	36.4	+1.2	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctrl_feature_on_vcpu.v
+3.59%	41.0	42.4	+1.5	bluerock/bhv/zeta/lib/log/proof/log_hpp_spec.v
+3.63%	30.5	31.6	+1.1	bluerock/bhv/apps/umx/proof/main_cpp_proof/umxservice.v
+3.67%	39.0	40.4	+1.4	bluerock/bhv/apps/vmm/vml/devices/msr/proof/msr_id_hpp_proof.v
+3.68%	56.5	58.6	+2.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/packet_ctor.v
+3.71%	32.7	33.9	+1.2	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/roundup_parallel_specs.v
+3.72%	43.3	44.9	+1.6	bluerock/bhv/apps/vmm/proof/bm_dram.v
+3.85%	32.3	33.5	+1.2	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/countLN.v
+3.90%	30.1	31.3	+1.2	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_split_sz.v
+3.91%	31.4	32.6	+1.2	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/init.v
+4.29%	27.7	28.9	+1.2	bluerock/bhv/zeta/apps/msc/proof/nova_caprange_hpp_proof.v
+4.65%	32.4	33.9	+1.5	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_intersect.v
+4.68%	25.4	26.5	+1.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/wp_vcpu/memory1.v
+4.78%	24.0	25.1	+1.1	bluerock/bhv/apps/umx/proof/admin_cpp_proof/beep.v
+4.86%	25.2	26.5	+1.2	bluerock/bhv/zeta/lib/zeta/proof/mutex_hpp_proof.v
+4.97%	32.2	33.8	+1.6	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof.v
+5.33%	30.4	32.0	+1.6	bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/zynqmp_dma_ver_hpp_spec.v
+5.43%	55.4	58.4	+3.0	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/flood.v
+5.74%	27.4	28.9	+1.6	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/is_size_valid.v
+5.90%	60.0	63.5	+3.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/micromega/micromega1.v
+6.55%	17.8	19.0	+1.2	bluerock/bhv/zeta/lib/lang/proof/string_gnu_cpp_proof.v
+7.47%	15.3	16.5	+1.1	bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/utils.v
+11.83%	16.7	18.7	+2.0	bluerock/bhv/zeta/lib/intrusive/proof/rangemap_hpp_model.v
+19.59%	12.7	15.2	+2.5	bluerock/bhv/zeta/lib/intrusive/proof/rangemap_hpp_util.v
+0.22%	141896.9	142203.5	+306.6	total
-0.00%	32798.5	32798.4	-0.2	├ translation units
+0.28%	109098.4	109405.1	+306.7	└ proofs and tests

[pgiarrusso-sl]

pred.v is odd and should be fixed, but I won't request changes this late. Approving.