Extend typechecking for Econstructor/Eglobal

[pgiarrusso-sl]

The purpose of this PR is to make the type checker more complete.

[skylabs-ai-ci]

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/BRiCk/	paolo/typed-econstructor-eglobal	18f1f1d	c7c1309	main	4a8ce6c	#258

Passive Repos

Repo	Job Branch	Job Commit
./	main	f50d261
fmdeps/auto/	main	b933744
fmdeps/auto-docs/	main	f3ece99
bluerock/NOVA/	skylabs-proof	488788c
bluerock/bhv/	skylabs-main	002aa53
fmdeps/brick-libcpp/	main	671ea1d
fmdeps/ci/	main	70edfbf
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
fmdeps/fm-tools/	main	62ce8ba
psi/protos/	main	8fe3e7c
psi/backend/	main	8f2a32f
psi/ide/	main	6b596cf
psi/data/	main	3cffdd9
vendored/rocq/	skylabs-master	bef7df5
fmdeps/rocq-agent-toolkit/	main	53d9eb0
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	707ce3f
vendored/vsrocq/	skylabs-main	ee79e7a

Performance

Relative	Master	MR	Change	Filename
+0.13%	140288.8	140467.7	+178.9	total
-0.02%	33188.7	33182.9	-5.8	├ translation units
+0.17%	107100.1	107284.8	+184.7	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-3.06%	62.0	60.1	-1.9	fmdeps/auto/rocq-skylabs-auto-cpp/tests/micromega/micromega1.v
-2.10%	462.8	453.1	-9.7	bluerock/bhv/apps/vmm/lib/board/include/model/aarch64_board_common_hpp.v
-0.43%	249.4	248.3	-1.1	bluerock/bhv/apps/vswitch/lib/port/proof/port/defs.v
-0.39%	257.7	256.7	-1.0	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/proof.v
-0.34%	378.4	377.1	-1.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/conclude_chain_use.v
-0.29%	476.5	475.1	-1.4	bluerock/bhv/apps/vswitch/lib/port/proof/port/proof.v
-0.23%	856.1	854.1	-2.0	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/proof.v
+0.14%	880.7	881.9	+1.3	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_default_impl.v
+0.15%	961.3	962.8	+1.5	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_cpp_proof.v
+0.19%	872.2	873.8	+1.6	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/reset_cpu.v
+0.22%	522.9	524.0	+1.1	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/spec.v
+0.23%	546.0	547.3	+1.2	bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_sc.v
+0.23%	666.2	667.8	+1.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/copy.v
+0.24%	1806.0	1810.4	+4.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v
+0.25%	493.9	495.1	+1.2	bluerock/bhv/zeta/lib/concurrent/proof/lossy_queue2_hpp_proof.v
+0.26%	466.6	467.8	+1.2	bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/access.v
+0.26%	467.4	468.6	+1.2	bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_private.v
+0.27%	473.1	474.4	+1.3	bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/zynqmp_dma_ver_cpp_proof.v
+0.29%	528.9	530.5	+1.6	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sc.v
+0.31%	454.3	455.7	+1.4	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pd.v
+0.32%	327.6	328.7	+1.0	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/async_copy_cookie.v
+0.33%	722.6	725.0	+2.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/virtual_interface.v
+0.36%	328.3	329.5	+1.2	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/walk.v
+0.38%	471.8	473.6	+1.8	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/msr_framework.v
+0.39%	405.7	407.3	+1.6	bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_cpp_proof/access.v
+0.40%	290.5	291.6	+1.2	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pt.v
+0.41%	338.6	339.9	+1.4	bluerock/NOVA/build-proof/proof/sm_cpp_proof/dn.v
+0.43%	253.9	255.0	+1.1	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/TO_UPSTREAM.v
+0.45%	339.2	340.8	+1.5	bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_pt.v
+0.46%	253.8	254.9	+1.2	bluerock/bhv/apps/vmm/lib/bluerock/proof/aarch64/reg_accessor_hpp_proof.v
+0.51%	1132.3	1138.1	+5.8	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v
+0.51%	226.3	227.5	+1.2	bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/msr_hpp_proof.v
+0.55%	205.2	206.4	+1.1	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/ctor.v
+0.56%	258.7	260.2	+1.4	bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/mmio.v
+0.57%	269.8	271.4	+1.5	bluerock/NOVA/build-proof/proof/pd_cpp_proof/create.v
+0.57%	209.4	210.6	+1.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/conclude_chain_use.v
+0.60%	359.8	361.9	+2.2	bluerock/bhv/apps/vswitch/lib/vsmp/proof/msg_queue_hpp/proof.v
+0.61%	206.4	207.7	+1.3	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/iterator.v
+0.61%	196.4	197.6	+1.2	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_cpp_proof/space_sel.v
+0.62%	193.1	194.3	+1.2	bluerock/bhv/zeta/lib/intrusive/proof/shared_pointer_hpp_proof.v
+0.62%	199.6	200.9	+1.2	bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_public.v
+0.64%	196.4	197.6	+1.3	bluerock/bhv/apps/vswitch/lib/vswitch/proof/create_forwarding_plane.v
+0.64%	167.7	168.8	+1.1	bluerock/NOVA/build-proof/proof/sm_cpp_proof/create.v
+0.66%	183.4	184.6	+1.2	bluerock/bhv/apps/vswitch/lib/vswitch/proof/initialize_dataplane.v
+0.71%	163.3	164.5	+1.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/reset.v
+0.71%	153.8	154.9	+1.1	bluerock/bhv/apps/vmm/vml/devices/vuart/proof/seq_queue_proof.v
+0.72%	220.5	222.1	+1.6	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort_to_vbus.v
+0.73%	148.8	149.9	+1.1	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/compute_gpa_fault_addr.v
+0.74%	143.0	144.1	+1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/walk_chain.v
+0.82%	139.9	141.1	+1.1	bluerock/bhv/zeta/lib/intrusive/proof/refcounted_proof.v
+0.84%	175.4	176.9	+1.5	bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_base_proof.v
+0.86%	133.2	134.4	+1.1	bluerock/bhv/zeta/lib/lang/proof/bits_hpp_proof.v
+0.88%	133.0	134.2	+1.2	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_off.v
+0.88%	196.3	198.0	+1.7	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/queue/misc.v
+0.96%	234.2	236.4	+2.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/flood.v
+0.99%	106.6	107.7	+1.1	bluerock/NOVA/build-proof/proof/sm_cpp_proof/up.v
+1.03%	105.7	106.8	+1.1	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_sc.v
+1.06%	136.1	137.6	+1.4	bluerock/bhv/zeta/lib/concurrent/proof/ticket_lock_cpp_proof.v
+1.08%	111.3	112.5	+1.2	bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_rich_proof.v
+1.12%	102.6	103.8	+1.1	bluerock/bhv/zeta/lib/lang/proof/string_cpp_proof.v
+1.14%	99.7	100.9	+1.1	bluerock/NOVA/build-proof/proof/slab_cpp_proof/free.v
+1.14%	100.3	101.4	+1.1	bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_proof.v
+1.14%	121.7	123.1	+1.4	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/create.v
+1.15%	131.2	132.7	+1.5	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/update.v
+1.18%	96.2	97.3	+1.1	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/start_cpu.v
+1.26%	96.2	97.4	+1.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/spec.v
+1.31%	98.8	100.1	+1.3	bluerock/bhv/lib/vrl/proof/vrl/port_hpp_proof.v
+1.31%	121.4	123.0	+1.6	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/lookup.v
+1.33%	87.0	88.2	+1.2	bluerock/bhv/zeta/lib/cxx/proof/bitset_hpp_proof.v
+1.36%	102.3	103.7	+1.4	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/spec.v
+1.38%	79.2	80.3	+1.1	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/TO_UPSTREAM.v
+1.42%	83.7	84.9	+1.2	bluerock/bhv/zeta/lib/lang/proof/endian16_hpp_proof.v
+1.42%	100.0	101.4	+1.4	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_other.v
+1.56%	101.3	102.8	+1.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/drop.v
+1.57%	73.0	74.2	+1.1	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_finish.v
+1.59%	79.2	80.5	+1.3	bluerock/bhv/zeta/lib/lang/proof/compiler_hpp_proof.v
+1.59%	75.9	77.1	+1.2	fmdeps/auto/rocq-skylabs-auto-cpp/tests/array_string_init/main_cpp_proof.v
+1.70%	65.4	66.5	+1.1	bluerock/bhv/zeta/lib/lang/proof/endian8_hpp_proof.v
+1.79%	61.7	62.8	+1.1	bluerock/bhv/zeta/lib/lang/proof/endian32_hpp_proof.v
+1.79%	61.0	62.1	+1.1	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/ctor.v
+1.81%	60.2	61.2	+1.1	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/linearized_desc.v
+1.87%	60.6	61.8	+1.1	bluerock/NOVA/build-proof/proof/slab_cpp_proof/slab.v
+1.88%	111.2	113.3	+2.1	bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/hints.v
+1.92%	65.9	67.2	+1.3	bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/unblock.v
+1.96%	71.8	73.2	+1.4	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/spec.v
+1.99%	112.0	114.2	+2.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/util.v
+2.00%	123.4	125.9	+2.5	bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/proof.v
+2.01%	82.1	83.7	+1.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/extract_frame_header.v
+2.07%	58.5	59.7	+1.2	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_merge.v
+2.14%	52.0	53.1	+1.1	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/hints.v
+2.21%	74.4	76.1	+1.6	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/base_startup_handler.v
+2.22%	55.5	56.7	+1.2	bluerock/bhv/zeta/lib/lang/proof/endian64_hpp_proof.v
+2.37%	53.3	54.5	+1.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/virtio_net_header_hints.v
+2.38%	62.2	63.7	+1.5	bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/esr_hpp_proof.v
+2.38%	85.4	87.4	+2.0	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/roundup_parallel_proof.v
+2.42%	47.0	48.1	+1.1	bluerock/bhv/apps/vswitch/proof/model/ethernet.v
+2.50%	46.2	47.3	+1.2	bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_cpp_proof/lookup.v
+2.52%	43.8	44.9	+1.1	bluerock/bhv/zeta/lib/bson/proof/bson_hints.v
+2.54%	45.5	46.7	+1.2	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctrl_feature_reset.v
+2.59%	42.7	43.8	+1.1	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/run.v
+2.60%	44.1	45.2	+1.1	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/lec_stack_size.v
+2.63%	42.1	43.2	+1.1	bluerock/bhv/zeta/lib/zeta/proof/signal_hpp_proof.v
+2.68%	42.1	43.2	+1.1	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/ghost.v
+2.87%	50.4	51.8	+1.4	bluerock/NOVA/build-proof/proof/slab_cpp_proof/hints.v
+2.98%	44.4	45.7	+1.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/cpp_hints.v
+3.02%	38.1	39.3	+1.2	bluerock/bhv/lib/vrl/proof/vrl/packet_hpp_proof.v
+3.02%	42.6	43.9	+1.3	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_split_range.v
+3.15%	36.6	37.7	+1.2	bluerock/bhv/lib/vrl/proof/vrl/port_list_hints.v
+3.17%	44.5	45.9	+1.4	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/guest_chunk_repo_hpp_proof.v
+3.21%	35.2	36.3	+1.1	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctrl_feature_on_vcpu.v
+3.45%	41.0	42.4	+1.4	bluerock/bhv/zeta/lib/log/proof/log_hpp_spec.v
+3.60%	32.4	33.6	+1.2	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/countLN.v
+3.69%	31.3	32.5	+1.2	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/init.v
+3.88%	30.2	31.4	+1.2	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_split_sz.v
+3.91%	39.2	40.7	+1.5	bluerock/bhv/apps/vmm/vml/devices/msr/proof/msr_id_hpp_proof.v
+4.05%	34.5	35.9	+1.4	bluerock/NOVA/build-proof/proof/iface/model.v
+4.30%	27.4	28.6	+1.2	bluerock/bhv/zeta/apps/msc/proof/nova_caprange_hpp_proof.v
+4.55%	32.7	34.2	+1.5	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_intersect.v
+4.66%	25.3	26.4	+1.2	bluerock/bhv/zeta/lib/zeta/proof/mutex_hpp_proof.v
+5.07%	55.3	58.1	+2.8	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/flood.v
+5.53%	25.4	26.8	+1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f0_proof.v
+5.65%	19.1	20.2	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f2_proof.v
+6.48%	25.4	27.1	+1.6	bluerock/NOVA/build-proof/proof/space_hpp_proof.v
+6.60%	17.8	19.0	+1.2	bluerock/bhv/zeta/lib/lang/proof/string_gnu_cpp_proof.v
+6.99%	15.4	16.5	+1.1	bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/utils.v
+7.07%	20.9	22.4	+1.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f0_proof.v
+11.86%	16.7	18.7	+2.0	bluerock/bhv/zeta/lib/intrusive/proof/rangemap_hpp_model.v
+14.26%	14.7	16.8	+2.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f1_proof.v
+19.32%	12.7	15.2	+2.5	bluerock/bhv/zeta/lib/intrusive/proof/rangemap_hpp_util.v
+0.13%	140288.8	140467.7	+178.9	total
-0.02%	33188.7	33182.9	-5.8	├ translation units
+0.17%	107100.1	107284.8	+184.7	└ proofs and tests

[skylabs-ai-ci]

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/BRiCk/	paolo/typed-econstructor-eglobal	c8a521e	51a8f98	main	1a4e474	#258

Passive Repos

Repo	Job Branch	Job Commit
./	main	f50d261
fmdeps/auto/	main	58eae4b
fmdeps/auto-docs/	main	f3ece99
bluerock/NOVA/	skylabs-proof	488788c
bluerock/bhv/	skylabs-main	ee95a75
fmdeps/brick-libcpp/	main	2b9fd6e
fmdeps/ci/	main	555a549
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
fmdeps/fm-tools/	main	70842c3
psi/protos/	main	8fe3e7c
psi/backend/	main	8f2a32f
psi/ide/	main	6b596cf
psi/data/	main	8cd3ea7
vendored/rocq/	skylabs-master	bef7df5
fmdeps/rocq-agent-toolkit/	main	53d9eb0
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	133e53a
vendored/vsrocq/	skylabs-main	ee79e7a

Performance

Relative	Master	MR	Change	Filename
-0.16%	140849.7	140619.1	-230.7	total
+0.01%	33024.2	33026.6	+2.4	├ translation units
-0.22%	107825.5	107592.4	-233.1	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-51.88%	657.5	316.4	-341.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/arith_bug.v
-12.57%	16.2	14.2	-2.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/includes/A_cpp_proof.v
-7.89%	21.4	19.7	-1.7	bluerock/bhv/zeta/lib/alloc/proof/core_proof_utils.v
-5.54%	26.7	25.2	-1.5	bluerock/bhv/zeta/lib/lang/proof/page_hpp_proof.v
-2.97%	41.1	39.9	-1.2	bluerock/bhv/zeta/lib/cxx/proof/sys/lock_guard_hpp_proof.v
-1.47%	108.0	106.4	-1.6	fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/list_cpp_proof.v
-1.45%	122.9	121.1	-1.8	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/misc_hints.v
-1.04%	101.1	100.0	-1.0	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/route.v
-1.00%	167.8	166.1	-1.7	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof.v
-0.84%	189.6	188.0	-1.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/set_virtio_net_header.v
-0.61%	198.1	196.9	-1.2	fmdeps/auto/rocq-skylabs-auto-cpp/tests/elpi/enums/variant_cpp_proof.v
-0.44%	386.0	384.3	-1.7	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/extract_frame_header.v
-0.43%	249.5	248.5	-1.1	bluerock/bhv/apps/vswitch/lib/port/proof/port/defs.v
-0.41%	261.9	260.8	-1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/get_set_byte_requesters.v
-0.39%	258.1	257.1	-1.0	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/proof.v
-0.34%	378.8	377.5	-1.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/conclude_chain_use.v
-0.33%	339.5	338.4	-1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/hints.v
-0.30%	719.2	717.0	-2.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/misc.v
-0.28%	477.4	476.1	-1.4	bluerock/bhv/apps/vswitch/lib/port/proof/port/proof.v
-0.24%	857.1	855.0	-2.1	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/proof.v
-0.17%	674.0	672.8	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist_cpp/forward_list_hpp_proof.v
+0.20%	1808.1	1811.8	+3.7	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v
+0.39%	1669.8	1676.4	+6.6	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/reset.v
+0.40%	1134.2	1138.8	+4.5	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v
+0.77%	143.7	144.8	+1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/walk_chain.v
+0.78%	140.5	141.6	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/destructuring/test_pair.v
+0.92%	149.3	150.7	+1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/splice_cpp_spec.v
+0.95%	115.9	117.0	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/initialization_forms.v
+1.04%	234.6	237.0	+2.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/flood.v
+1.06%	106.4	107.6	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/compound_assignment_increments.v
+1.16%	89.4	90.4	+1.0	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/devq/used_event_notify.v
+1.28%	96.6	97.9	+1.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/spec.v
+1.30%	98.0	99.3	+1.3	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/destructuring_declarations.v
+1.31%	101.9	103.3	+1.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/drop.v
+1.41%	76.0	77.1	+1.1	fmdeps/auto-docs/content/demo/forward_list_v1/test_cpp_proof.v
+1.44%	75.7	76.8	+1.1	fmdeps/auto-docs/content/demo/linked_list/linked_list_cpp_proof.v
+1.47%	74.2	75.3	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/pair_hpp_spec.v
+1.50%	96.4	97.9	+1.4	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/lambda_captures.v
+1.53%	94.9	96.3	+1.5	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_binary_operators.v
+1.53%	94.3	95.8	+1.4	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_relational_operators.v
+1.61%	75.9	77.1	+1.2	fmdeps/auto/rocq-skylabs-auto-cpp/tests/array_string_init/main_cpp_proof.v
+1.75%	63.1	64.2	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/relational_operators.v
+1.87%	76.3	77.7	+1.4	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/primitive_initialization.v
+1.88%	58.6	59.7	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/wp_lval_op_assign_variants.v
+1.94%	57.5	58.7	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/comma_operator.v
+1.97%	72.3	73.7	+1.4	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/spec.v
+2.03%	57.3	58.5	+1.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/flood.v
+2.10%	53.3	54.5	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/arithmetic_operators.v
+2.15%	51.2	52.3	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/if_switch_initializers.v
+2.29%	48.9	50.0	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_unary_operators.v
+2.40%	61.1	62.6	+1.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/read_prim/read_cpp_proof.v
+2.53%	44.4	45.5	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/bitwise_operators.v
+2.59%	45.4	46.6	+1.2	fmdeps/auto/rocq-skylabs-auto-cpp/tests/auto_frac/anyR_proof.v
+2.59%	44.9	46.1	+1.2	fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/utility/test_cpp_proof.v
+2.64%	41.9	43.1	+1.1	bluerock/bhv/zeta/lib/bson/proof/bson.v
+2.68%	44.0	45.2	+1.2	fmdeps/auto/rocq-skylabs-auto-cpp/tests/control_flow/main_cpp_spec.v
+2.69%	53.7	55.1	+1.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/virtio_net_header_hints.v
+2.72%	41.1	42.2	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/integral_casts.v
+2.83%	38.0	39.0	+1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/vqueue_interface.v
+2.92%	38.9	40.0	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_casts.v
+3.11%	36.9	38.0	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/smoke.v
+3.25%	61.7	63.7	+2.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/micromega/micromega1.v
+3.28%	45.2	46.7	+1.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/inits/main_cpp_spec.v
+3.29%	33.2	34.3	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/control_logical_forms.v
+3.30%	34.6	35.7	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/sizeof_alignof.v
+3.31%	44.7	46.2	+1.5	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/cpp_hints.v
+3.34%	41.8	43.2	+1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/int128/test.v
+3.38%	33.8	34.9	+1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/set_virtio_net_header.v
+3.49%	38.9	40.2	+1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/anyR_proof.v
+3.51%	31.1	32.2	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/destructuring/test.v
+3.61%	41.5	43.0	+1.5	bluerock/NOVA/build-proof/proof/kmem_hpp_spec.v
+4.09%	34.6	36.0	+1.4	fmdeps/auto-docs/content/docs/functions/verification.v
+4.14%	34.3	35.7	+1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/sem_const/constructor.v
+4.50%	31.4	32.8	+1.4	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/xval_init_lval.v
+4.61%	22.7	23.7	+1.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/virtual/virtual_cpp_proof.v
+4.76%	24.3	25.4	+1.2	fmdeps/auto-docs/content/docs/class_reps/alt.v
+4.79%	30.6	32.0	+1.5	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/implicit_array_initialization.v
+4.80%	31.6	33.1	+1.5	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/arrays.v
+5.52%	26.2	27.7	+1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/factor.v
+5.64%	19.6	20.7	+1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/normalization/test.v
+5.75%	25.7	27.2	+1.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/constructor.v
+6.06%	18.9	20.0	+1.1	fmdeps/auto-docs/content/docs/control_flow/loop.v
+6.48%	22.7	24.2	+1.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/sub_const.v
+7.22%	22.9	24.5	+1.7	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/allocation_lambda_forms.v
+7.85%	20.7	22.3	+1.6	fmdeps/auto-docs/content/docs/debugging/main.v
+7.87%	18.8	20.2	+1.5	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/assignment_operators_min_bool.v
+13.37%	16.3	18.5	+2.2	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/member_pointer_operators.v
+13.39%	16.3	18.5	+2.2	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/variable_length_arrays.v
-0.16%	140849.7	140619.1	-230.7	total
+0.01%	33024.2	33026.6	+2.4	├ translation units
-0.22%	107825.5	107592.4	-233.1	└ proofs and tests

[skylabs-ai-ci]

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/BRiCk/	paolo/typed-econstructor-eglobal	9ea907b	e4885bb	main	1f77eb9	#258

Passive Repos

Repo	Job Branch	Job Commit
./	main	f50d261
fmdeps/auto/	main	ab40b56
fmdeps/auto-docs/	main	f3ece99
bluerock/NOVA/	skylabs-proof	d802253
bluerock/bhv/	skylabs-main	a727bb3
fmdeps/brick-libcpp/	main	c63ec2f
fmdeps/ci/	main	9bc1d3f
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
fmdeps/fm-tools/	main	70842c3
psi/protos/	main	8fe3e7c
psi/backend/	main	8f2a32f
psi/ide/	main	6b596cf
psi/data/	main	b01668d
vendored/rocq/	skylabs-master	bef7df5
fmdeps/rocq-agent-toolkit/	main	53d9eb0
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	133e53a
vendored/vsrocq/	skylabs-main	ee79e7a

Performance

Relative	Master	MR	Change	Filename
-97.97%	141318.8	2864.3	-138454.5	total
-97.97%	138454.5	-	-138454.5	├ disappeared files (2667)
+0.00%	2864.3	2864.3	+0.0	└ common files
+0.00%	2864.3	2864.3	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-97.97%	141318.8	2864.3	-138454.5	total
-97.97%	138454.5	-	-138454.5	├ disappeared files (2667)
+0.00%	2864.3	2864.3	+0.0	└ common files
+0.00%	2864.3	2864.3	+0.0	└ proofs and tests

[skylabs-ai-ci]

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/BRiCk/	paolo/typed-econstructor-eglobal	59ac99d	5eb35ee	main	1f77eb9	#258

Passive Repos

Repo	Job Branch	Job Commit
./	main	f50d261
fmdeps/auto/	main	ab40b56
fmdeps/auto-docs/	main	f3ece99
bluerock/NOVA/	skylabs-proof	d802253
bluerock/bhv/	skylabs-main	a727bb3
fmdeps/brick-libcpp/	main	c63ec2f
fmdeps/ci/	main	9bc1d3f
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
fmdeps/fm-tools/	main	70842c3
psi/protos/	main	8fe3e7c
psi/backend/	main	8f2a32f
psi/ide/	main	6b596cf
psi/data/	main	b01668d
vendored/rocq/	skylabs-master	bef7df5
fmdeps/rocq-agent-toolkit/	main	53d9eb0
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	133e53a
vendored/vsrocq/	skylabs-main	ee79e7a

Performance

Relative	Master	MR	Change	Filename
-97.97%	141318.8	2864.3	-138454.5	total
-97.97%	138454.5	-	-138454.5	├ disappeared files (2667)
+0.00%	2864.3	2864.3	+0.0	└ common files
+0.00%	2864.3	2864.3	+0.0	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-97.97%	141318.8	2864.3	-138454.5	total
-97.97%	138454.5	-	-138454.5	├ disappeared files (2667)
+0.00%	2864.3	2864.3	+0.0	└ common files
+0.00%	2864.3	2864.3	+0.0	└ proofs and tests

[skylabs-ai-ci]

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/BRiCk/	paolo/typed-econstructor-eglobal	3f90abc	c8e943c	main	1f77eb9	#258
fmdeps/auto/	paolo/typed-econstructor-eglobal	1d8ac3b	1d8ac3b	main	83a895e	-

Passive Repos

Repo	Job Branch	Job Commit
./	main	f50d261
fmdeps/auto-docs/	main	f3ece99
bluerock/NOVA/	skylabs-proof	d802253
bluerock/bhv/	skylabs-main	a727bb3
fmdeps/brick-libcpp/	main	c63ec2f
fmdeps/ci/	main	9bc1d3f
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
fmdeps/fm-tools/	main	70842c3
psi/protos/	main	8fe3e7c
psi/backend/	main	8f2a32f
psi/ide/	main	6b596cf
psi/data/	main	b01668d
vendored/rocq/	skylabs-master	bef7df5
fmdeps/rocq-agent-toolkit/	main	53d9eb0
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	133e53a
vendored/vsrocq/	skylabs-main	ee79e7a

Performance

Relative	Master	MR	Change	Filename
+0.03%	141314.0	141356.8	+42.7	total
+0.01%	-	20.3	+20.3	├ newly appeared files (1)
+0.02%	141314.0	141336.4	+22.4	└ common files
+0.01%	33026.5	33030.7	+4.2	├ translation units
+0.02%	108287.6	108305.8	+18.2	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-12.39%	16.8	14.7	-2.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f1_proof.v
-11.67%	18.6	16.4	-2.2	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/member_pointer_operators.v
-11.62%	18.6	16.4	-2.2	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/variable_length_arrays.v
-7.19%	22.3	20.7	-1.6	fmdeps/auto-docs/content/docs/debugging/main.v
-7.16%	20.3	18.8	-1.5	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/assignment_operators_min_bool.v
-6.48%	22.4	20.9	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f0_proof.v
-5.98%	24.4	22.9	-1.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/sub_const.v
-5.76%	23.6	22.3	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/virtual/virtual_cpp_proof.v
-5.72%	24.5	23.1	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/allocation_lambda_forms.v
-5.57%	20.1	19.0	-1.1	fmdeps/auto-docs/content/docs/control_flow/loop.v
-5.45%	27.7	26.2	-1.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/factor.v
-5.33%	19.0	18.0	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f1_proof.v
-5.29%	19.6	18.6	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f1_proof.v
-5.27%	20.7	19.6	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/normalization/test.v
-5.18%	20.1	19.1	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f2_proof.v
-5.17%	19.9	18.9	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_f0_proof.v
-5.10%	26.8	25.4	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f0_proof.v
-5.05%	27.2	25.8	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/constructor.v
-4.54%	28.1	26.8	-1.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f0_proof.v
-4.47%	33.2	31.7	-1.5	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/arrays.v
-4.46%	32.1	30.7	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/implicit_array_initialization.v
-4.43%	32.4	31.0	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f3_proof.v
-4.41%	25.4	24.3	-1.1	fmdeps/auto-docs/content/docs/class_reps/alt.v
-4.32%	23.5	22.5	-1.0	fmdeps/auto/rocq-skylabs-cpp-stdlib/theories/vector/spec.v
-4.23%	28.6	27.3	-1.2	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f0_proof.v
-4.11%	33.0	31.6	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/xval_init_lval.v
-3.95%	26.7	25.7	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f3_proof.v
-3.91%	35.7	34.3	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/sem_const/constructor.v
-3.77%	36.7	35.4	-1.4	fmdeps/auto-docs/content/docs/functions/verification.v
-3.32%	43.9	42.4	-1.5	bluerock/NOVA/build-proof/proof/kmem_hpp_spec.v
-3.28%	32.3	31.2	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/destructuring/test.v
-3.07%	35.8	34.7	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/sizeof_alignof.v
-3.07%	44.2	42.9	-1.4	bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_cpp_proof/hints.v
-3.06%	34.4	33.3	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/control_logical_forms.v
-3.05%	43.3	42.0	-1.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/int128/test.v
-2.97%	339.9	329.8	-10.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/arith_bug.v
-2.97%	43.8	42.5	-1.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f2_proof.v
-2.96%	41.0	39.8	-1.2	fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/anyR_proof.v
-2.90%	38.1	37.0	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/smoke.v
-2.83%	46.9	45.5	-1.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/inits/main_cpp_spec.v
-2.62%	40.1	39.0	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_casts.v
-2.52%	42.2	41.2	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/integral_casts.v
-2.52%	45.4	44.2	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/control_flow/main_cpp_spec.v
-2.37%	47.5	46.4	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/auto_frac/anyR_proof.v
-2.37%	46.2	45.2	-1.1	fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/utility/test_cpp_proof.v
-2.35%	45.6	44.5	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/bitwise_operators.v
-2.10%	50.1	49.1	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_unary_operators.v
-1.99%	52.6	51.6	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/if_switch_initializers.v
-1.90%	54.5	53.5	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/arithmetic_operators.v
-1.78%	58.7	57.7	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/comma_operator.v
-1.76%	60.9	59.8	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/aarch64/inheritance_arch_hpp_spec.v
-1.76%	59.9	58.8	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/wp_lval_op_assign_variants.v
-1.68%	77.8	76.5	-1.3	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/primitive_initialization.v
-1.60%	64.2	63.2	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/relational_operators.v
-1.58%	66.4	65.4	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/x86_64/inheritance_arch_hpp_spec.v
-1.53%	77.2	76.0	-1.2	fmdeps/auto/rocq-skylabs-auto-cpp/tests/array_string_init/main_cpp_proof.v
-1.48%	122.9	121.1	-1.8	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/misc_hints.v
-1.41%	96.4	95.1	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_binary_operators.v
-1.37%	95.9	94.5	-1.3	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_relational_operators.v
-1.36%	97.9	96.6	-1.3	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/lambda_captures.v
-1.32%	76.8	75.8	-1.0	fmdeps/auto-docs/content/demo/linked_list/linked_list_cpp_proof.v
-1.22%	122.7	121.2	-1.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_main_proof.v
-1.19%	99.6	98.5	-1.2	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/destructuring_declarations.v
-1.08%	101.1	100.0	-1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/route.v
-0.94%	107.7	106.7	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/compound_assignment_increments.v
-0.94%	146.9	145.5	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v
-0.92%	167.8	166.3	-1.5	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof.v
-0.79%	132.8	131.7	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v
-0.73%	189.6	188.3	-1.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/set_virtio_net_header.v
-0.49%	261.9	260.6	-1.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/get_set_byte_requesters.v
-0.42%	249.5	248.5	-1.1	bluerock/bhv/apps/vswitch/lib/port/proof/port/defs.v
-0.34%	339.5	338.4	-1.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/hints.v
-0.33%	378.7	377.5	-1.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/conclude_chain_use.v
-0.21%	959.4	957.4	-2.0	fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/vector/test_cpp.v
-0.16%	719.3	718.2	-1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/misc.v
+0.12%	882.4	883.4	+1.1	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_default_impl.v
+0.14%	927.3	928.6	+1.3	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/setup.v
+0.16%	759.7	760.9	+1.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/setup.v
+0.23%	673.0	674.5	+1.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist_cpp/forward_list_hpp_proof.v
+0.24%	1526.0	1529.7	+3.6	bluerock/bhv/apps/vmm/proof/main_cpp_proof/prepare_address_space.v
+0.26%	1090.5	1093.3	+2.8	bluerock/bhv/apps/vmm/proof/main_cpp_proof/zeta_main.v
+0.29%	1808.2	1813.5	+5.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v
+0.34%	362.5	363.7	+1.2	bluerock/bhv/apps/vswitch/lib/vsmp/proof/msg_queue_hpp/proof.v
+0.38%	360.2	361.6	+1.4	bluerock/bhv/zeta/lib/lang/proof/atomic_hpp_proof.v
+0.48%	1134.9	1140.4	+5.5	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v
+0.68%	229.9	231.4	+1.6	bluerock/bhv/apps/umx/proof/main_cpp_proof/user_handler.v
+0.69%	196.8	198.2	+1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/elpi/enums/variant_cpp_proof.v
+0.76%	342.4	345.0	+2.6	bluerock/bhv/apps/umx/proof/main_cpp_proof/input_loop.v
+0.77%	143.7	144.8	+1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/walk_chain.v
+1.08%	115.1	116.3	+1.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/spec.v
+1.10%	234.7	237.3	+2.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/flood.v
+1.16%	89.4	90.4	+1.0	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/devq/used_event_notify.v
+1.19%	147.6	149.3	+1.8	bluerock/bhv/zeta/lib/alloc/proof/core_hpp_general_proof.v
+1.21%	177.2	179.3	+2.1	bluerock/bhv/zeta/lib/msc/proof/sys/rwlock_hpp_proof.v
+1.33%	101.9	103.3	+1.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/drop.v
+1.52%	113.5	115.3	+1.7	bluerock/bhv/lib/socket/proof/socket_defs_hpp_proof.v
+1.55%	67.0	68.0	+1.0	bluerock/bhv/zeta/lib/lang/proof/endian_hpp_spec.v
+1.58%	100.0	101.6	+1.6	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_other.v
+1.58%	106.4	108.1	+1.7	fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/list_cpp_proof.v
+1.60%	78.1	79.4	+1.3	bluerock/bhv/zeta/lib/cxx/proof/sys/mutex_hpp_proof.v
+1.64%	85.7	87.1	+1.4	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/spec.v
+1.97%	56.4	57.5	+1.1	bluerock/bhv/zeta/lib/lang/proof/errno_hpp_proof.v
+1.98%	57.3	58.4	+1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/flood.v
+2.23%	58.5	59.8	+1.3	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_merge.v
+2.60%	46.9	48.1	+1.2	bluerock/bhv/apps/vswitch/proof/model/ethernet.v
+2.70%	53.7	55.2	+1.5	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/virtio_net_header_hints.v
+2.83%	38.0	39.0	+1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/vqueue_interface.v
+3.09%	42.6	43.9	+1.3	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_split_range.v
+3.11%	74.4	76.7	+2.3	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/invoke.v
+3.27%	39.9	41.2	+1.3	bluerock/bhv/zeta/lib/cxx/proof/sys/lock_guard_hpp_proof.v
+3.32%	44.8	46.3	+1.5	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/cpp_hints.v
+3.42%	40.8	42.2	+1.4	bluerock/bhv/zeta/lib/lang/proof/memory_barrier.v
+3.42%	33.8	34.9	+1.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/set_virtio_net_header.v
+3.92%	30.2	31.4	+1.2	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_split_sz.v
+4.50%	34.2	35.7	+1.5	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_spec.v
+4.58%	32.7	34.2	+1.5	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_intersect.v
+5.64%	24.7	26.1	+1.4	bluerock/bhv/zeta/lib/lang/proof/string_hpp_spec.v
+6.15%	25.2	26.7	+1.5	bluerock/bhv/zeta/lib/lang/proof/page_hpp_proof.v
+6.20%	20.1	21.3	+1.2	bluerock/bhv/zeta/lib/lang/proof/bits_hpp_spec.v
+6.65%	22.9	24.4	+1.5	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_util.v
+7.13%	21.4	23.0	+1.5	bluerock/bhv/zeta/lib/lang/proof/string_cpp_hints.v
+7.45%	14.6	15.7	+1.1	bluerock/bhv/zeta/lib/lang/proof/util.v
+8.88%	19.7	21.5	+1.8	bluerock/bhv/zeta/lib/alloc/proof/core_proof_utils.v
+10.31%	24.2	26.7	+2.5	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/inline_invoke.v
+11.77%	16.7	18.7	+2.0	bluerock/bhv/zeta/lib/intrusive/proof/rangemap_hpp_model.v
+13.81%	15.5	17.6	+2.1	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/axioms.v
+14.66%	14.2	16.3	+2.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/includes/A_cpp_proof.v
+0.03%	141314.0	141356.8	+42.7	total
+0.01%	-	20.3	+20.3	├ newly appeared files (1)
+0.02%	141314.0	141336.4	+22.4	└ common files
+0.01%	33026.5	33030.7	+4.2	├ translation units
+0.02%	108287.6	108305.8	+18.2	└ proofs and tests

[skylabs-ai-ci]

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/BRiCk/	paolo/typed-econstructor-eglobal	3f90abc	c8e943c	main	1f77eb9 ( ⚠️ needs rebase)	#258
fmdeps/auto/	paolo/typed-econstructor-eglobal	c886c60	1d8ac3b	main	83a895e	#353

Passive Repos

Repo	Job Branch	Job Commit
./	main	f50d261
fmdeps/auto-docs/	main	f3ece99
bluerock/NOVA/	skylabs-proof	d802253
bluerock/bhv/	skylabs-main	a727bb3
fmdeps/brick-libcpp/	main	d89b37c
fmdeps/ci/	main	9bc1d3f
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
fmdeps/fm-tools/	main	70842c3
psi/protos/	main	8fe3e7c
psi/backend/	main	8f2a32f
psi/ide/	main	6b596cf
psi/data/	main	b01668d
vendored/rocq/	skylabs-master	bef7df5
fmdeps/rocq-agent-toolkit/	main	53d9eb0
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	133e53a
vendored/vsrocq/	skylabs-main	ee79e7a

Performance

Relative	Master	MR	Change	Filename
+0.03%	141312.4	141356.7	+44.3	total
+0.01%	-	20.3	+20.3	├ newly appeared files (1)
+0.02%	141312.4	141336.4	+24.0	└ common files
+0.01%	33026.5	33030.7	+4.2	├ translation units
+0.02%	108285.9	108305.7	+19.8	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-12.39%	16.8	14.7	-2.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f1_proof.v
-11.67%	18.6	16.4	-2.2	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/member_pointer_operators.v
-11.62%	18.6	16.4	-2.2	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/variable_length_arrays.v
-7.19%	22.3	20.7	-1.6	fmdeps/auto-docs/content/docs/debugging/main.v
-7.16%	20.3	18.8	-1.5	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/assignment_operators_min_bool.v
-6.48%	22.4	20.9	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f0_proof.v
-5.98%	24.4	22.9	-1.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/sub_const.v
-5.76%	23.6	22.3	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/virtual/virtual_cpp_proof.v
-5.72%	24.5	23.1	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/allocation_lambda_forms.v
-5.57%	20.1	19.0	-1.1	fmdeps/auto-docs/content/docs/control_flow/loop.v
-5.33%	19.0	18.0	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f1_proof.v
-5.29%	19.6	18.6	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f1_proof.v
-5.27%	20.7	19.6	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/normalization/test.v
-5.18%	20.1	19.1	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f2_proof.v
-5.17%	19.9	18.9	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_f0_proof.v
-5.10%	26.8	25.4	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f0_proof.v
-5.05%	27.2	25.8	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/constructor.v
-4.54%	28.1	26.8	-1.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f0_proof.v
-4.47%	33.2	31.7	-1.5	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/arrays.v
-4.46%	32.1	30.7	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/implicit_array_initialization.v
-4.43%	32.4	31.0	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f3_proof.v
-4.41%	25.4	24.3	-1.1	fmdeps/auto-docs/content/docs/class_reps/alt.v
-4.32%	23.5	22.5	-1.0	fmdeps/auto/rocq-skylabs-cpp-stdlib/theories/vector/spec.v
-4.23%	28.6	27.3	-1.2	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f0_proof.v
-4.11%	33.0	31.6	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/xval_init_lval.v
-3.95%	26.7	25.7	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f3_proof.v
-3.91%	35.7	34.3	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/sem_const/constructor.v
-3.77%	36.7	35.4	-1.4	fmdeps/auto-docs/content/docs/functions/verification.v
-3.32%	43.9	42.4	-1.5	bluerock/NOVA/build-proof/proof/kmem_hpp_spec.v
-3.28%	32.3	31.2	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/destructuring/test.v
-3.07%	35.8	34.7	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/sizeof_alignof.v
-3.07%	44.2	42.9	-1.4	bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_cpp_proof/hints.v
-3.06%	34.4	33.3	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/control_logical_forms.v
-3.05%	43.3	42.0	-1.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/int128/test.v
-2.97%	339.9	329.8	-10.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/arith_bug.v
-2.97%	43.8	42.5	-1.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f2_proof.v
-2.96%	41.0	39.8	-1.2	fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/anyR_proof.v
-2.90%	38.1	37.0	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/smoke.v
-2.83%	46.9	45.5	-1.3	fmdeps/auto/rocq-skylabs-auto-cpp/tests/inits/main_cpp_spec.v
-2.62%	40.1	39.0	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_casts.v
-2.52%	42.2	41.2	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/integral_casts.v
-2.52%	45.4	44.2	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/control_flow/main_cpp_spec.v
-2.37%	47.5	46.4	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/auto_frac/anyR_proof.v
-2.37%	46.2	45.2	-1.1	fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/utility/test_cpp_proof.v
-2.35%	45.6	44.5	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/bitwise_operators.v
-2.10%	50.1	49.1	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_unary_operators.v
-1.99%	52.6	51.6	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/if_switch_initializers.v
-1.90%	54.5	53.5	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/arithmetic_operators.v
-1.78%	58.7	57.7	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/comma_operator.v
-1.76%	60.9	59.8	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/aarch64/inheritance_arch_hpp_spec.v
-1.76%	59.9	58.8	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/wp_lval_op_assign_variants.v
-1.68%	77.8	76.5	-1.3	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/primitive_initialization.v
-1.60%	64.2	63.2	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/relational_operators.v
-1.58%	66.4	65.4	-1.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/x86_64/inheritance_arch_hpp_spec.v
-1.53%	77.2	76.0	-1.2	fmdeps/auto/rocq-skylabs-auto-cpp/tests/array_string_init/main_cpp_proof.v
-1.48%	122.9	121.1	-1.8	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/misc_hints.v
-1.41%	96.4	95.1	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_binary_operators.v
-1.37%	95.9	94.5	-1.3	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_relational_operators.v
-1.36%	97.9	96.6	-1.3	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/lambda_captures.v
-1.32%	76.8	75.8	-1.0	fmdeps/auto-docs/content/demo/linked_list/linked_list_cpp_proof.v
-1.22%	122.7	121.2	-1.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_main_proof.v
-1.19%	99.6	98.5	-1.2	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/destructuring_declarations.v
-1.08%	101.1	100.0	-1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/route.v
-0.94%	107.7	106.7	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/compound_assignment_increments.v
-0.94%	146.9	145.5	-1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v
-0.92%	167.8	166.3	-1.5	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof.v
-0.79%	132.8	131.7	-1.0	fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v
-0.73%	189.6	188.3	-1.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/set_virtio_net_header.v
-0.49%	261.9	260.6	-1.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/get_set_byte_requesters.v
-0.42%	249.5	248.5	-1.1	bluerock/bhv/apps/vswitch/lib/port/proof/port/defs.v
-0.34%	339.5	338.4	-1.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/hints.v
-0.33%	378.7	377.5	-1.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/conclude_chain_use.v
-0.21%	959.4	957.4	-2.0	fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/vector/test_cpp.v
-0.16%	719.3	718.2	-1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/misc.v
+0.12%	882.4	883.4	+1.1	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_default_impl.v
+0.14%	927.3	928.6	+1.3	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/setup.v
+0.16%	759.7	760.9	+1.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/setup.v
+0.23%	673.0	674.5	+1.5	fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist_cpp/forward_list_hpp_proof.v
+0.24%	1526.0	1529.7	+3.6	bluerock/bhv/apps/vmm/proof/main_cpp_proof/prepare_address_space.v
+0.26%	1090.5	1093.3	+2.8	bluerock/bhv/apps/vmm/proof/main_cpp_proof/zeta_main.v
+0.29%	1808.2	1813.5	+5.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v
+0.34%	362.5	363.7	+1.2	bluerock/bhv/apps/vswitch/lib/vsmp/proof/msg_queue_hpp/proof.v
+0.38%	360.2	361.6	+1.4	bluerock/bhv/zeta/lib/lang/proof/atomic_hpp_proof.v
+0.48%	1134.9	1140.4	+5.5	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v
+0.68%	229.9	231.4	+1.6	bluerock/bhv/apps/umx/proof/main_cpp_proof/user_handler.v
+0.69%	196.8	198.2	+1.4	fmdeps/auto/rocq-skylabs-auto-cpp/tests/elpi/enums/variant_cpp_proof.v
+0.76%	342.4	345.0	+2.6	bluerock/bhv/apps/umx/proof/main_cpp_proof/input_loop.v
+0.77%	143.7	144.8	+1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/walk_chain.v
+1.08%	115.1	116.3	+1.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/spec.v
+1.10%	234.7	237.3	+2.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/flood.v
+1.16%	89.4	90.4	+1.0	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/devq/used_event_notify.v
+1.19%	147.6	149.3	+1.8	bluerock/bhv/zeta/lib/alloc/proof/core_hpp_general_proof.v
+1.21%	177.2	179.3	+2.1	bluerock/bhv/zeta/lib/msc/proof/sys/rwlock_hpp_proof.v
+1.33%	101.9	103.3	+1.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/drop.v
+1.52%	113.5	115.3	+1.7	bluerock/bhv/lib/socket/proof/socket_defs_hpp_proof.v
+1.55%	67.0	68.0	+1.0	bluerock/bhv/zeta/lib/lang/proof/endian_hpp_spec.v
+1.58%	100.0	101.6	+1.6	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_other.v
+1.58%	106.4	108.1	+1.7	fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/list_cpp_proof.v
+1.60%	78.1	79.4	+1.3	bluerock/bhv/zeta/lib/cxx/proof/sys/mutex_hpp_proof.v
+1.64%	85.7	87.1	+1.4	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/spec.v
+1.97%	56.4	57.5	+1.1	bluerock/bhv/zeta/lib/lang/proof/errno_hpp_proof.v
+1.98%	57.3	58.4	+1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/flood.v
+2.23%	58.5	59.8	+1.3	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_merge.v
+2.60%	46.9	48.1	+1.2	bluerock/bhv/apps/vswitch/proof/model/ethernet.v
+2.70%	53.7	55.2	+1.5	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/virtio_net_header_hints.v
+2.83%	38.0	39.0	+1.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/vqueue_interface.v
+3.09%	42.6	43.9	+1.3	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_split_range.v
+3.11%	74.4	76.7	+2.3	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/invoke.v
+3.27%	39.9	41.2	+1.3	bluerock/bhv/zeta/lib/cxx/proof/sys/lock_guard_hpp_proof.v
+3.32%	44.8	46.3	+1.5	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/cpp_hints.v
+3.42%	40.8	42.2	+1.4	bluerock/bhv/zeta/lib/lang/proof/memory_barrier.v
+3.42%	33.8	34.9	+1.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/set_virtio_net_header.v
+3.92%	30.2	31.4	+1.2	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_split_sz.v
+4.50%	34.2	35.7	+1.5	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_spec.v
+4.58%	32.7	34.2	+1.5	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_intersect.v
+5.64%	24.7	26.1	+1.4	bluerock/bhv/zeta/lib/lang/proof/string_hpp_spec.v
+6.15%	25.2	26.7	+1.5	bluerock/bhv/zeta/lib/lang/proof/page_hpp_proof.v
+6.20%	20.1	21.3	+1.2	bluerock/bhv/zeta/lib/lang/proof/bits_hpp_spec.v
+6.65%	22.9	24.4	+1.5	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_util.v
+7.13%	21.4	23.0	+1.5	bluerock/bhv/zeta/lib/lang/proof/string_cpp_hints.v
+7.45%	14.6	15.7	+1.1	bluerock/bhv/zeta/lib/lang/proof/util.v
+8.88%	19.7	21.5	+1.8	bluerock/bhv/zeta/lib/alloc/proof/core_proof_utils.v
+10.31%	24.2	26.7	+2.5	fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/inline_invoke.v
+11.77%	16.7	18.7	+2.0	bluerock/bhv/zeta/lib/intrusive/proof/rangemap_hpp_model.v
+13.81%	15.5	17.6	+2.1	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/axioms.v
+14.66%	14.2	16.3	+2.1	fmdeps/auto/rocq-skylabs-auto-cpp/tests/includes/A_cpp_proof.v
+0.03%	141312.4	141356.7	+44.3	total
+0.01%	-	20.3	+20.3	├ newly appeared files (1)
+0.02%	141312.4	141336.4	+24.0	└ common files
+0.01%	33026.5	33030.7	+4.2	├ translation units
+0.02%	108285.9	108305.7	+19.8	└ proofs and tests

[pgiarrusso-sl]

LGTM, I'd approve your changes and they passed CI.

I fixed the issues.

[gmalecha-at-skylabs]

Mostly my code. Someone else should review as well.