Use Gc.ramp_up on ocaml >= 5.4

[rlepigre-skylabs-ai]

No description provided.

[skylabs-ai-ci]

Performance summary for https://github.com/SkylabsAI/rocq/actions/runs/19634496852

Relative	Master	MR	Change	Filename
-7.88%	132896.5	122422.2	-10474.3	total
-2.73%	24267.3	24949.7	-682.4	├ translation units
-9.07%	98154.8	107946.8	-9791.9	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-38.89%	26.2	16.0	-10.2	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_config_hpp/prelude/ghost.v
-38.88%	26.2	16.0	-10.2	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/prelude/ghost.v
-38.87%	26.2	16.0	-10.2	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/prelude/ghost.v
-38.65%	26.7	16.4	-10.3	bluerock/bhv/apps/vswitch/proof/prelude/ghost.v
-38.46%	24.5	15.1	-9.4	bluerock/NOVA/build-proof/proof/iface/predicates/pred.v
-37.02%	18.1	11.4	-6.7	bluerock/NOVA/build-proof/proof/fpu_hpp_spec.v
-36.95%	25.5	16.1	-9.4	bluerock/NOVA/build-proof/proof/iface/predicates/hip.v
-36.57%	21.5	13.6	-7.8	bluerock/bhv/lib/ddk/proof/dmadev_drv_hpp_spec.v
-36.56%	25.8	16.4	-9.4	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue.v
-36.26%	24.7	15.8	-9.0	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_entry_cpp/portal_flags.v
-35.56%	17.8	11.5	-6.3	bluerock/bhv/lib/ddk/proof/ddk.v
-35.29%	25.4	16.4	-9.0	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/axioms.v
-35.20%	16.6	10.8	-5.8	bluerock/bhv/zeta/lib/zeta/proof/types_hpp_spec.v
-35.07%	28.5	18.5	-10.0	bluerock/NOVA/build-proof/proof/iface/predicates/arch.v
-34.85%	20.3	13.2	-7.1	bluerock/bhv/lib/ddk/proof/chardev_drv_hpp_spec.v
-34.83%	15.4	10.1	-5.4	bluerock/NOVA/build-proof/proof/spinlock_hpp_spec.v
-34.82%	15.4	10.1	-5.4	bluerock/NOVA/build-proof/proof/lock_guard_hpp_spec.v
-34.60%	15.8	10.3	-5.5	bluerock/NOVA/build-proof/proof/cpu_hpp_spec.v
-34.49%	41.6	27.2	-14.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/prelude/spec.v
-34.49%	39.1	25.6	-13.5	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_hpp_spec.v
-34.38%	15.5	10.2	-5.3	bluerock/NOVA/build-proof/proof/start_S_spec.v
-34.38%	15.1	9.9	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/enums.v
-34.38%	19.9	13.1	-6.9	bluerock/bhv/lib/ddk/proof/ptr_mmio_hpp_spec.v
-34.34%	15.7	10.3	-5.4	bluerock/NOVA/build-proof/proof/lock_guard_hpp_proof.v
-34.34%	15.1	9.9	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/lib/trace.v
-34.32%	15.8	10.4	-5.4	bluerock/NOVA/build-proof/proof/aarch64/board_qemu.v
-34.29%	15.1	9.9	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/includes/A_cpp_spec.v
-34.27%	15.1	9.9	-5.2	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/cstdlib/spec.v
-34.25%	15.1	10.0	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/cpp/main.v
-34.21%	15.9	10.4	-5.4	bluerock/NOVA/build-proof/proof/aarch64/arch.v
-34.21%	16.3	10.7	-5.6	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/vector/pred.v
-34.16%	15.2	10.0	-5.2	bluerock/bhv/zeta/lib/cxx/proof/type_traits_hpp_spec.v
-34.15%	22.2	14.6	-7.6	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_cpp_proof/hints.v
-34.14%	15.2	10.0	-5.2	bluerock/bhv/zeta/lib/lang/proof/types_hpp_spec.v
-34.12%	15.4	10.2	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/spec.v
-34.12%	14.5	9.6	-5.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/elpi.v
-34.10%	15.2	10.0	-5.2	bluerock/bhv/apps/vmm/lib/vm_config/proof/vm_config_hpp_spec.v
-34.09%	15.2	10.0	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/spec/example_cpp_spec.v
-34.03%	15.5	10.2	-5.3	bluerock/bhv/zeta/lib/cxx/proof/timer_hpp_spec.v
-34.03%	15.5	10.2	-5.3	bluerock/bhv/zeta/lib/cli/proof/readline_hpp_spec.v
-34.03%	16.2	10.7	-5.5	bluerock/NOVA/build-proof/proof/kobject_hpp_spec.v
-34.02%	15.7	10.4	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/prelude/test.v
-33.99%	15.5	10.2	-5.3	bluerock/bhv/zeta/lib/cxx/proof/vector_hpp_spec.v
-33.97%	15.3	10.1	-5.2	bluerock/bhv/apps/pm/proof/dev_api.v
-33.96%	15.7	10.4	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/prelude.v
-33.93%	15.7	10.4	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/llist/new_hpp_spec.v
-33.92%	42.1	27.8	-14.3	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/prelude/proof.v
-33.86%	15.3	10.1	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/specify/challenge/main_spec.v
-33.86%	15.3	10.2	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/local_scope/local_scope_cpp_spec.v
-33.85%	15.8	10.5	-5.4	bluerock/NOVA/build-proof/proof/queue_hpp_hints.v
-33.85%	15.4	10.2	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/llist_cpp/main_cpp_spec.v
-33.84%	15.8	10.5	-5.3	bluerock/NOVA/build-proof/proof/event_hpp_spec.v
-33.84%	15.4	10.2	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/specify/challenge/identity_hpp_spec.v
-33.83%	15.4	10.2	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/llist_cpp/assert_hpp_spec.v
-33.82%	15.8	10.5	-5.3	bluerock/NOVA/build-proof/proof/cpu_hpp_spec/page.v
-33.82%	15.8	10.5	-5.3	bluerock/NOVA/build-proof/proof/regs_hpp_spec/prelude.v
-33.77%	16.2	10.7	-5.5	bluerock/NOVA/build-proof/proof/cpu_hpp_spec/abs_pred.v
-33.76%	16.2	10.8	-5.5	bluerock/NOVA/build-proof/proof/cpu_hpp_spec/ghosts.v
-33.72%	15.9	10.5	-5.3	bluerock/NOVA/build-proof/proof/timeout_hpp_spec/scheduled.v
-33.72%	15.6	10.3	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/cpp/spec/concepts.v
-33.71%	16.2	10.7	-5.5	bluerock/NOVA/build-proof/proof/queue_hpp_proof.v
-33.70%	15.6	10.3	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/unlocked/test_unlocked.v
-33.70%	15.6	10.3	-5.3	bluerock/bhv/zeta/lib/alloc/proof/spec_utils.v
-33.67%	15.9	10.5	-5.3	bluerock/bhv/zeta/lib/lang/proof/endian128_hpp_proof.v
-33.66%	15.4	10.2	-5.2	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/cassert/spec.v
-33.65%	37.1	24.6	-12.5	bluerock/bhv/apps/vswitch/lib/acl/proof/outcome_hpp_spec.v
-33.63%	16.9	11.2	-5.7	bluerock/NOVA/build-proof/proof/soup/base.v
-33.62%	15.5	10.3	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/io/io_c_spec.v
-33.61%	15.5	10.3	-5.2	bluerock/bhv/zeta/lib/lang/proof/page_hpp_spec.v
-33.59%	35.8	23.8	-12.0	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/prelude/hints.v
-33.57%	16.3	10.8	-5.5	bluerock/NOVA/build-proof/proof/start_S_spec/addr.v
-33.57%	15.5	10.3	-5.2	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/new/spec_exc.v
-33.53%	15.5	10.3	-5.2	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/exception/spec.v
-33.52%	15.5	10.3	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/brick_eval/bad/util.v
-33.51%	40.9	27.2	-13.7	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/prelude/spec.v
-33.48%	16.0	10.6	-5.3	bluerock/bhv/zeta/lib/alloc/proof/bcs_hpp_proof.v
-33.46%	16.0	10.6	-5.3	bluerock/bhv/zeta/lib/alloc/proof/allocator_hpp_proof.v
-33.40%	16.0	10.7	-5.3	bluerock/NOVA/build-proof/proof/cpulocal/abs_pred.v
-33.40%	15.7	10.5	-5.3	bluerock/bhv/apps/vmm/proof/prelude/spec.v
-33.38%	15.8	10.5	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/specify/challenge/challenge_hpp_spec.v
-33.37%	16.0	10.7	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/cpp_spec/term_matcher.v
-33.36%	16.0	10.7	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/llist/listd_cpp_spec.v
-33.35%	17.1	11.4	-5.7	bluerock/NOVA/build-proof/proof/pt_hpp_spec.v
-33.35%	15.6	10.4	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/arch_indep/upstream_specs.v
-33.34%	22.6	15.0	-7.5	bluerock/NOVA/build-proof/proof/iface/predicates/ec_regs.v
-33.32%	16.1	10.7	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/prelude/proof.v
-33.31%	15.8	10.5	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/cpp/spec/concepts/experimental.v
-33.30%	15.8	10.5	-5.3	bluerock/bhv/apps/umx/proof/model.v
-33.27%	16.1	10.7	-5.3	bluerock/NOVA/build-proof/proof/cpulocal/interrupt.v
-33.26%	15.6	10.4	-5.2	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/new/pred.v
-33.24%	23.9	15.9	-7.9	bluerock/NOVA/build-proof/proof/syscall_cpp_spec.v
-33.24%	16.0	10.7	-5.3	bluerock/NOVA/build-proof/proof/scheduler_hpp_spec/prelude.v
-33.23%	16.1	10.7	-5.3	bluerock/NOVA/build-proof/proof/cpulocal/simple_model.v
-33.23%	16.1	10.7	-5.3	bluerock/NOVA/build-proof/proof/cpulocal.v
-33.19%	41.3	27.6	-13.7	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/pkt.v
-33.15%	16.1	10.8	-5.3	bluerock/NOVA/build-proof/proof/bits_hpp_spec.v
-33.13%	16.7	11.1	-5.5	bluerock/NOVA/build-proof/proof/pt_hpp_spec/prelude.v
-33.13%	15.9	10.6	-5.3	bluerock/bhv/apps/vmm/lib/lifecycle_bluerock/proof/lifecycle_hpp_spec.v
-33.09%	16.7	11.2	-5.5	bluerock/bhv/zeta/lib/alloc/proof/range_hpp_spec.v
-33.01%	19.8	13.3	-6.5	fmdeps/auto/coq-bluerock-auto-cpp/tests/llist_cpp/new_hpp_hints.v
-32.98%	16.2	10.9	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/llist/list_cpp_spec.v
-32.97%	17.9	12.0	-5.9	bluerock/NOVA/build-proof/proof/spinlock_hpp_spec/lock.v
-32.97%	15.8	10.6	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/dataclass_demo/dataclass_demo_imports.v
-32.94%	16.2	10.9	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/specify/challenge/link.v
-32.93%	15.8	10.6	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/includes/A_hpp_spec.v
-32.80%	11.1	7.5	-3.6	bluerock/NOVA/build-proof/proof/tests/modules/test.v
-32.78%	16.3	11.0	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/cpp_spec/return_bug.v
-32.71%	16.9	11.3	-5.5	bluerock/NOVA/build-proof/proof/capability_hpp_spec.v
-32.69%	16.4	11.0	-5.3	bluerock/NOVA/build-proof/proof/utcb_arch_hpp_spec.v
-32.68%	16.7	11.2	-5.5	bluerock/NOVA/build-proof/proof/aarch64/timer_hpp_spec.v
-32.68%	19.8	13.3	-6.5	bluerock/bhv/apps/vmm/lib/bluerock/proof/aarch64/vm_types_hpp_spec.v
-32.67%	16.3	11.0	-5.3	bluerock/NOVA/build-proof/proof/space_obj_hpp_spec/sel.v
-32.63%	16.7	11.3	-5.5	bluerock/NOVA/build-proof/proof/rcu_hpp_spec.v
-32.62%	16.5	11.1	-5.4	bluerock/NOVA/build-proof/proof/start_S_spec/abs_pred.v
-32.62%	16.6	11.2	-5.4	bluerock/NOVA/build-proof/proof/aarch64/cos_hpp_spec.v
-32.61%	42.2	28.4	-13.7	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/prelude/hints/drop.v
-32.61%	16.1	10.9	-5.3	bluerock/bhv/zeta/lib/cxx/proof/optional_hpp_spec.v
-32.59%	16.5	11.1	-5.4	bluerock/NOVA/build-proof/proof/kobject_hpp_spec/prelude.v
-32.58%	16.4	11.1	-5.3	bluerock/NOVA/build-proof/proof/globals_static.v
-32.55%	44.9	30.3	-14.6	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/prelude/proof.v
-32.54%	16.4	11.1	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/cpp_spec/test_requires.v
-32.51%	16.2	10.9	-5.3	bluerock/bhv/apps/vmm/lib/vsmmu/proof/pagetable_tracker_cpp_spec.v
-32.50%	12.2	8.2	-4.0	fmdeps/auto/coq-bluerock-auto-core/tests/warnings.v
-32.49%	17.5	11.8	-5.7	bluerock/NOVA/build-proof/proof/sc_hpp_spec/conf.v
-32.48%	16.2	10.9	-5.3	bluerock/bhv/zeta/lib/alloc/proof/bin_info_hpp_specs.v
-32.46%	16.0	10.8	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/simple/main_cpp_spec.v
-32.46%	20.1	13.6	-6.5	bluerock/bhv/apps/umx/proof/umx_hpp_proof.v
-32.40%	16.2	11.0	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0088_cpp_spec.v
-32.40%	16.2	11.0	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0084_cpp_spec.v
-32.37%	17.0	11.5	-5.5	bluerock/NOVA/build-proof/proof/sc_hpp_spec/prelude.v
-32.33%	16.3	11.0	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/specify/copymove/test_hpp_spec.v
-32.33%	16.3	11.0	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0099_cpp_spec.v
-32.32%	16.3	11.0	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0092_cpp_spec.v
-32.32%	20.1	13.6	-6.5	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxshared.v
-32.31%	16.7	11.3	-5.4	bluerock/NOVA/build-proof/proof/spinlock_hpp_spec/lock_guard.v
-32.30%	16.6	11.2	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/upstream/cpp/misc_hints.v
-32.29%	17.1	11.6	-5.5	bluerock/NOVA/build-proof/proof/dc_hpp_spec.v
-32.27%	16.1	10.9	-5.2	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/cctype/spec.v
-32.25%	16.3	11.0	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/validate_spec/test.v
-32.23%	16.3	11.1	-5.3	bluerock/bhv/lib/vrl/proof/lists_in_map.v
-32.23%	16.3	11.1	-5.3	bluerock/bhv/lib/vrl/proof/guardedR.v
-32.22%	16.6	11.2	-5.3	bluerock/NOVA/build-proof/proof/hip_hpp_spec.v
-32.22%	16.6	11.3	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/virtual/virtual_cpp_spec.v
-32.22%	16.8	11.4	-5.4	bluerock/NOVA/build-proof/proof/capability_hpp_spec/cap.v
-32.22%	16.3	11.1	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0076_cpp_spec.v
-32.21%	16.3	11.1	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/proof.v
-32.19%	16.3	11.1	-5.2	bluerock/NOVA/build-proof/proof/basis/spec.v
-32.18%	23.3	15.8	-7.5	bluerock/bhv/apps/vswitch/lib/protocol/proof/virtio_net_hpp/ghost.v
-32.17%	42.8	29.0	-13.8	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/prelude/hints/copy_frame.v
-32.10%	16.3	11.1	-5.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/portal_hpp_spec.v
-32.09%	17.2	11.7	-5.5	bluerock/NOVA/build-proof/proof/spinlock_hpp_spec/lc_lock_guard.v
-32.07%	16.7	11.3	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/theories/upstream/cpp/big_op.v
-32.05%	16.4	11.1	-5.3	bluerock/bhv/zeta/lib/alloc/proof/allocator_hpp_specs.v
-32.05%	22.8	15.5	-7.3	bluerock/bhv/lib/vconnect/proof/vconnect/async_control_hpp/prelude/ghost.v
-32.05%	17.2	11.7	-5.5	bluerock/NOVA/build-proof/proof/space_pio_hpp_spec.v
-32.04%	23.4	15.9	-7.5	bluerock/NOVA/build-proof/proof/iface/predicates.v
-32.04%	17.2	11.7	-5.5	bluerock/NOVA/build-proof/proof/space_msr_hpp_spec.v
-32.04%	11.4	7.7	-3.6	bluerock/NOVA/build-proof/proof/tests/modules/test_part_two.v
-32.04%	22.8	15.5	-7.3	bluerock/bhv/lib/vconnect/proof/vconnect/async_control_hpp/ghost.v
-32.03%	11.4	7.7	-3.6	bluerock/NOVA/build-proof/proof/tests/modules/test_part_one.v
-32.03%	11.4	7.7	-3.6	bluerock/NOVA/build-proof/proof/cpulocal/ghost.v
-32.02%	51.7	35.1	-16.6	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_hpp_spec/hints.v
-31.99%	11.4	7.7	-3.6	bluerock/NOVA/build-proof/proof/tests/modules/test_client.v
-31.95%	16.3	11.1	-5.2	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/cstdlib/atoi.v
-31.94%	17.7	12.0	-5.6	bluerock/NOVA/build-proof/proof/ec_hpp_spec/hazard_pred.v
-31.93%	16.8	11.4	-5.3	fmdeps/auto-docs/content/docs/class_reps/main.v
-31.93%	17.3	11.8	-5.5	bluerock/NOVA/build-proof/proof/sm_hpp_spec/prelude.v
-31.92%	23.4	15.9	-7.5	bluerock/bhv/apps/vswitch/proof/upstream/hyp_tagging.v
-31.92%	11.4	7.8	-3.6	bluerock/NOVA/build-proof/proof/tests/modules/all_in_one.v
-31.91%	16.5	11.2	-5.3	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/allocator/spec.v
-31.91%	17.1	11.6	-5.5	bluerock/NOVA/build-proof/proof/timeout_hpp_spec.v
-31.89%	16.8	11.4	-5.3	bluerock/NOVA/build-proof/proof/start_S_spec/prelude.v
-31.89%	22.7	15.4	-7.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/devq.v
-31.88%	19.9	13.6	-6.4	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxclient.v
-31.88%	22.7	15.4	-7.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/available.v
-31.88%	22.7	15.4	-7.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/queue.v
-31.87%	22.7	15.4	-7.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/descriptor.v
-31.87%	22.7	15.4	-7.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/used.v
-31.87%	11.4	7.8	-3.6	bluerock/NOVA/build-proof/proof/fpu_hpp_spec/prelude.v
-31.86%	16.5	11.2	-5.3	bluerock/bhv/zeta/lib/alloc/proof/bcs_hpp_specs.v
-31.86%	22.7	15.4	-7.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/used_entry.v
-31.85%	23.9	16.3	-7.6	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof.v
-31.84%	23.7	16.1	-7.5	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg.v
-31.82%	17.3	11.8	-5.5	bluerock/NOVA/build-proof/proof/spinlock_hpp_spec/lc_lock.v
-31.81%	22.6	15.4	-7.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/model/iommu_interface_hpp/prelude/spec.v
-31.81%	16.9	11.5	-5.4	bluerock/bhv/zeta/lib/pt/proof/pt_hpp_spec.v
-31.81%	22.6	15.4	-7.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/model/iommu_interface_hpp/spec.v
-31.80%	23.5	16.0	-7.5	bluerock/bhv/apps/vswitch/lib/port/proof/port/prelude/ghost.v
-31.80%	22.7	15.5	-7.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof.v
-31.79%	22.6	15.4	-7.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/model/iommu_interface_hpp/proof.v
-31.79%	22.6	15.4	-7.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/model/iommu_interface_hpp/prelude/hints.v
-31.77%	17.5	12.0	-5.6	bluerock/NOVA/build-proof/proof/space_obj_hpp_spec.v
-31.77%	16.9	11.5	-5.4	bluerock/bhv/zeta/lib/nova/proof/errno_hpp_spec.v
-31.75%	16.9	11.5	-5.4	bluerock/bhv/zeta/lib/cxx/proof/platform_hpp_spec.v
-31.74%	11.5	7.8	-3.6	bluerock/NOVA/build-proof/proof/sm_hpp_spec/count.v
-31.74%	16.4	11.2	-5.2	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/new/spec.v
-31.70%	16.6	11.3	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/upstream/cpp/reg_arrayR.v
-31.67%	43.4	29.7	-13.8	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/prelude/proof/pkt.v
-31.65%	41.7	28.5	-13.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/prelude/proof/copy_frame.v
-31.64%	22.7	15.5	-7.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/model/iommu_interface_hpp/prelude/defs.v
-31.63%	41.5	28.4	-13.1	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_vrl.v
-31.61%	23.2	15.9	-7.3	bluerock/bhv/apps/vmm/proof/guestdram.v
-31.61%	17.3	11.9	-5.5	bluerock/NOVA/build-proof/proof/buddy_hpp_spec.v
-31.61%	52.4	35.8	-16.6	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_entry_cpp_spec.v
-31.58%	16.7	11.4	-5.3	bluerock/bhv/apps/vmm/lib/pagetable/proof/pagetable_cpp_spec.v
-31.57%	16.7	11.4	-5.3	bluerock/bhv/zeta/lib/cxx/proof/cpuset_hpp_spec.v
-31.49%	11.6	7.9	-3.6	bluerock/NOVA/build-proof/proof/aarch64/fpu.v
-31.46%	23.7	16.2	-7.5	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer.v
-31.44%	16.7	11.5	-5.3	bluerock/bhv/zeta/lib/fdt/proof/reserved_mem_hpp_spec.v
-31.44%	16.5	11.3	-5.2	bluerock/bhv/apps/vmm/vml/config/vmm_debug/proof/debug_switches_hpp_spec.v
-31.40%	17.0	11.7	-5.3	bluerock/bhv/zeta/lib/alloc/proof/core_hpp_derived_proof.v
-31.40%	22.9	15.7	-7.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/model/iommu_interface_hpp/defs.v
-31.40%	16.7	11.5	-5.3	bluerock/bhv/lib/pm/pm_bhv/proof/sm_devs_hpp_spec.v
-31.40%	42.3	29.0	-13.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/spec.v
-31.38%	18.1	12.4	-5.7	bluerock/NOVA/build-proof/proof/sm_hpp_spec/queue.v
-31.32%	18.3	12.6	-5.7	bluerock/NOVA/build-proof/proof/ec_hpp_spec/const_triples.v
-31.28%	16.6	11.4	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/val_cat/val_cat_cpp_spec.v
-31.26%	17.3	11.9	-5.4	bluerock/NOVA/build-proof/proof/regs_hpp_spec.v
-31.23%	42.4	29.2	-13.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/prelude/proof/extract_frame_header.v
-31.23%	23.9	16.4	-7.5	bluerock/bhv/apps/vswitch/proof/upstream/gmap_lemmas.v
-31.21%	17.4	12.0	-5.4	bluerock/NOVA/build-proof/proof/aarch64/regs_cpp_proof.v
-31.18%	16.9	11.6	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0004_cpp_spec.v
-31.17%	23.0	15.9	-7.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/model/iommu_interface_hpp/prelude/proof.v
-31.16%	30.9	21.3	-9.6	bluerock/bhv/apps/vmm/lib/board/proof/x86/board_impl_hpp_hints.v
-31.14%	18.7	12.9	-5.8	bluerock/NOVA/build-proof/proof/ec_hpp_hints/status_hints.v
-31.12%	57.5	39.6	-17.9	bluerock/bhv/apps/vmm/proof/initial_setup_hpp_spec.v
-31.12%	42.5	29.3	-13.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp_spec.v
-31.11%	16.9	11.6	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0068_cpp_spec.v
-31.11%	18.3	12.6	-5.7	bluerock/NOVA/build-proof/proof/aarch64/regs_cpp_proof/cpu_regs.v
-31.10%	42.3	29.1	-13.2	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/prelude/spec.v
-31.09%	17.5	12.1	-5.5	bluerock/NOVA/build-proof/proof/start_S_spec/skew.v
-31.07%	16.9	11.7	-5.3	bluerock/bhv/zeta/lib/intrusive/proof/map_hpp_data_spec.v
-31.06%	16.9	11.7	-5.3	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/atomic/pred.v
-31.00%	24.0	16.5	-7.4	bluerock/bhv/apps/vmm/lib/vmi_interface/proof/sail.v
-30.96%	17.6	12.2	-5.5	bluerock/NOVA/build-proof/proof/stc_hpp_spec.v
-30.95%	17.3	11.9	-5.3	bluerock/NOVA/build-proof/proof/queue_hpp_spec.v
-30.94%	17.9	12.4	-5.5	bluerock/NOVA/build-proof/proof/ec_hpp_spec/fpu_pred.v
-30.91%	17.0	11.8	-5.3	bluerock/bhv/lib/pm/pm_bhv/proof/info_hpp_spec.v
-30.91%	17.3	12.0	-5.4	bluerock/bhv/zeta/lib/cxx/proof/sys/lock_guard_hpp_spec.v
-30.87%	37.8	26.2	-11.7	bluerock/bhv/apps/vmm/lib/board/proof/aarch64/board_impl_hpp_spec.v
-30.83%	20.4	14.1	-6.3	bluerock/bhv/apps/umx/proof/admin_cpp_proof.v
-30.79%	20.3	14.0	-6.3	bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers.v
-30.76%	23.9	16.6	-7.4	bluerock/bhv/lib/vconnect/proof/vconnect/async_control_hpp/hints.v
-30.76%	23.9	16.6	-7.4	bluerock/bhv/lib/vconnect/proof/vconnect/async_control_hpp/prelude/hints.v
-30.73%	18.0	12.4	-5.5	bluerock/NOVA/build-proof/proof/space_gst_hpp_spec.v
-30.73%	18.0	12.4	-5.5	bluerock/NOVA/build-proof/proof/space_hst_hpp_spec.v
-30.72%	44.8	31.0	-13.8	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/prelude/proof/flood.v
-30.70%	18.0	12.5	-5.5	bluerock/NOVA/build-proof/proof/space_dma_hpp_spec.v
-30.69%	17.6	12.2	-5.4	bluerock/NOVA/build-proof/proof/counter_hpp_spec.v
-30.69%	17.1	11.9	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/upstream/cpp/nullable_ptr_to_arrayR.v
-30.66%	40.9	28.4	-12.5	bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/spec.v
-30.66%	17.5	12.1	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/cpp_enum/test_cpp_proof.v
-30.64%	18.3	12.7	-5.6	bluerock/NOVA/build-proof/proof/ec_hpp_spec/status.v
-30.62%	43.0	29.9	-13.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/prelude/proof/set_virtio_net_header.v
-30.61%	24.6	17.1	-7.5	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/updaters.v
-30.60%	17.2	11.9	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0052_cpp_spec.v
-30.58%	17.2	11.9	-5.3	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/atomic/spec.v
-30.55%	17.2	12.0	-5.3	bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_cpp_proof/range_spec.v
-30.55%	17.2	11.9	-5.3	bluerock/bhv/lib/vrl/proof/TO_UPSTREAM.v
-30.55%	22.6	15.7	-6.9	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/hints.v
-30.44%	17.6	12.2	-5.4	bluerock/bhv/zeta/lib/lang/proof/compiler_hpp_spec.v
-30.44%	18.0	12.5	-5.5	bluerock/NOVA/build-proof/proof/abi_hpp_spec.v
-30.41%	45.5	31.7	-13.8	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_cpp_proof.v
-30.40%	17.3	12.0	-5.3	bluerock/bhv/zeta/lib/cxx/proof/util.v
-30.34%	17.3	12.1	-5.3	bluerock/bhv/zeta/lib/nova/proof/aarch64/arch_utcb_hpp_spec.v
-30.33%	45.4	31.6	-13.8	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/prelude/proof/misc.v
-30.33%	17.6	12.3	-5.3	bluerock/NOVA/build-proof/proof/basis/proof.v
-30.30%	18.3	12.8	-5.5	bluerock/NOVA/build-proof/proof/fpu_hpp_spec/triples.v
-30.29%	19.3	13.4	-5.8	bluerock/NOVA/build-proof/proof/ec_proof.v
-30.29%	17.3	12.1	-5.2	bluerock/bhv/apps/vswitch/lib/vswitch_config/proof/bson_config_hpp_spec.v
-30.27%	17.7	12.3	-5.3	bluerock/bhv/zeta/lib/msc/proof/sys/user_signal_hpp_proof.v
-30.26%	17.4	12.1	-5.3	bluerock/bhv/zeta/lib/alloc/proof/sels_hpp_spec.v
-30.24%	52.5	36.6	-15.9	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/misc.v
-30.22%	21.4	14.9	-6.5	bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/irq_cpp_proof.v
-30.20%	19.1	13.4	-5.8	bluerock/NOVA/build-proof/proof/aarch64/ec_proof/exc_predicates.v
-30.18%	19.2	13.4	-5.8	bluerock/NOVA/build-proof/proof/ec_hpp_spec/regs_triples.v
-30.18%	17.4	12.2	-5.3	bluerock/bhv/zeta/lib/alloc/proof/vmap_hpp_spec.v
-30.18%	17.4	12.2	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/upstream/cpp/cfractional_utils.v
-30.17%	17.4	12.2	-5.3	bluerock/bhv/zeta/lib/cli/proof/command_handler_hpp_spec.v
-30.15%	17.9	12.5	-5.4	bluerock/NOVA/build-proof/proof/aarch64/regs_cpp_proof/sys_regs.v
-30.14%	17.4	12.2	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0098_cpp_spec.v
-30.14%	41.7	29.1	-12.6	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/hints.v
-30.10%	17.3	12.1	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/elpi/enums/variant_cpp_spec.v
-30.07%	51.2	35.8	-15.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/set_virtio_net_header.v
-30.07%	51.0	35.7	-15.3	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_cpp_spec.v
-30.04%	17.5	12.2	-5.3	bluerock/bhv/zeta/lib/concurrent/proof/lossy_queue2_hpp_spec.v
-30.04%	45.5	31.8	-13.7	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/spec.v
-30.03%	17.8	12.5	-5.3	bluerock/NOVA/build-proof/proof/tests/queue/test_queue_spec.v
-30.02%	19.9	13.9	-6.0	bluerock/NOVA/build-proof/proof/pd_cpp_proof.v
-30.02%	17.5	12.3	-5.3	fmdeps/auto-docs/content/demo/linked_list/linked_list_hpp_spec.v
-29.98%	17.6	12.3	-5.3	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/primatomic_derivedspecs.v
-29.97%	17.9	12.5	-5.4	bluerock/bhv/zeta/apps/msc/proof/pd_hpp_spec.v
-29.97%	19.0	13.3	-5.7	bluerock/bhv/apps/vmm/lib/bluerock/proof/aarch64/nova_reg_utils.v
-29.96%	17.5	12.3	-5.3	bluerock/bhv/zeta/lib/msc/proof/sys/rwlock_hpp_spec.v
-29.93%	17.9	12.5	-5.3	bluerock/NOVA/build-proof/proof/capability_hpp_spec/perm.v
-29.90%	20.2	14.2	-6.0	bluerock/NOVA/build-proof/proof/sm_cpp_proof.v
-29.87%	46.0	32.3	-13.8	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/prelude/proof/route.v
-29.82%	43.4	30.4	-12.9	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/vlan_groups_hints.v
-29.80%	17.6	12.4	-5.3	bluerock/bhv/zeta/lib/bhv/proof/types_hpp_spec.v
-29.79%	17.9	12.6	-5.3	bluerock/NOVA/build-proof/proof/mtd_hpp_spec.v
-29.77%	17.6	12.4	-5.3	bluerock/bhv/zeta/lib/nova/proof/aarch64/exc_hpp_spec.v
-29.76%	17.7	12.4	-5.3	bluerock/bhv/zeta/lib/intrusive/proof/rangemap_hpp_spec.v
-29.75%	38.2	26.8	-11.4	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp_spec.v
-29.72%	19.4	13.7	-5.8	bluerock/NOVA/build-proof/proof/aarch64/ec_proof.v
-29.72%	18.0	12.7	-5.4	bluerock/bhv/zeta/lib/nova/proof/pd_weak_objective.v
-29.72%	17.5	12.3	-5.2	fmdeps/auto-docs/content/demo/aggregate01/Point_hpp_spec.v
-29.72%	17.7	12.5	-5.3	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/model/vcpu_types_hpp_spec.v
-29.70%	18.8	13.2	-5.6	bluerock/NOVA/build-proof/proof/sm_hpp_spec/accessors.v
-29.69%	24.6	17.3	-7.3	bluerock/bhv/lib/vconnect/proof/vconnect/async_control_hpp/prelude/defs.v
-29.67%	57.8	40.6	-17.1	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/wp_vcpu/predicates.v
-29.66%	17.7	12.5	-5.3	bluerock/bhv/zeta/lib/intrusive/proof/list_internal_hpp_spec.v
-29.65%	17.7	12.5	-5.3	bluerock/bhv/lib/pm/pm_client_bhv/proof/dev_client_hpp_spec.v
-29.63%	17.9	12.6	-5.3	bluerock/bhv/apps/sm/smclient/proof/client_hpp_spec.v
-29.62%	17.7	12.5	-5.3	bluerock/bhv/zeta/lib/nova/proof/aarch64/arch_types_hpp_spec.v
-29.61%	17.8	12.5	-5.3	bluerock/bhv/apps/vmm/proof/prelude/proof.v
-29.60%	17.8	12.5	-5.3	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/roundup_vcpu_interface.v
-29.58%	18.7	13.1	-5.5	bluerock/NOVA/build-proof/proof/fpu_hpp_spec/abs_pred.v
-29.58%	19.4	13.7	-5.7	bluerock/NOVA/build-proof/proof/scheduler_hpp_spec.v
-29.54%	18.9	13.3	-5.6	bluerock/bhv/zeta/lib/nova/proof/raw.v
-29.53%	21.9	15.4	-6.5	bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/irq_hpp_spec.v
-29.50%	19.8	14.0	-5.8	bluerock/NOVA/build-proof/proof/ec_hpp_spec/current_triples.v
-29.49%	18.7	13.2	-5.5	bluerock/NOVA/build-proof/proof/ec_hpp_spec/prelude.v
-29.47%	12.4	8.7	-3.7	bluerock/NOVA/build-proof/proof/aarch64/regs.v
-29.45%	19.4	13.7	-5.7	bluerock/NOVA/build-proof/proof/ec_hpp_spec/block_sc_pred.v
-29.45%	62.0	43.8	-18.3	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/run.v
-29.43%	24.9	17.6	-7.3	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg.v
-29.41%	42.2	29.8	-12.4	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_config_hpp/defs.v
-29.40%	18.4	13.0	-5.4	bluerock/NOVA/build-proof/proof/hazard_hpp_spec.v
-29.40%	19.2	13.6	-5.6	bluerock/NOVA/build-proof/proof/timeout_budget_hpp_spec.v
-29.40%	17.9	12.6	-5.3	bluerock/bhv/zeta/apps/msc/proof/bootargs_hpp_spec.v
-29.37%	25.5	18.0	-7.5	bluerock/bhv/apps/vswitch/lib/protocol/proof/virtio_net_hpp/prelude/defs.v
-29.33%	17.9	12.7	-5.3	bluerock/bhv/zeta/lib/alloc/proof/sel_alloc_hpp_spec.v
-29.28%	17.8	12.6	-5.2	bluerock/bhv/zeta/lib/cxx/proof/rangeset_hpp_spec.v
-29.24%	41.7	29.5	-12.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/prelude/proof/virtual_interface.v
-29.24%	18.4	13.0	-5.4	bluerock/NOVA/build-proof/proof/kobject_hpp_spec/subclass.v
-29.19%	25.7	18.2	-7.5	bluerock/NOVA/build-proof/proof/iface/predicates/interrupts.v
-29.15%	52.9	37.5	-15.4	bluerock/bhv/apps/vmm/proof/docs/noimport/aarch64/proof_architecture.v
-29.14%	20.3	14.4	-5.9	bluerock/NOVA/build-proof/proof/ec_hpp_hints.v
-29.11%	18.1	12.8	-5.3	bluerock/bhv/zeta/lib/fdt/proof/base_device_spec.v
-29.10%	17.8	12.6	-5.2	bluerock/bhv/zeta/lib/intrusive/proof/rangemap_hpp_util.v
-29.07%	23.0	16.3	-6.7	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/deps.v
-29.04%	18.1	12.9	-5.3	bluerock/bhv/zeta/lib/msc/proof/sys/user_signal_hpp_spec.v
-29.02%	18.4	13.1	-5.3	bluerock/bhv/zeta/lib/lang/proof/compiler_cpp_proof.v
-29.00%	15.4	11.0	-4.5	bluerock/bhv/lib/pm/pm_client_bhv/proof/device_config.v
-29.00%	33.7	24.0	-9.8	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/devq.v
-28.98%	22.5	16.0	-6.5	bluerock/bhv/apps/umx/proof/main_cpp_proof.v
-28.97%	33.8	24.0	-9.8	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer.v
-28.96%	32.8	23.3	-9.5	bluerock/bhv/apps/vmm/lib/board/proof/aarch64/board_impl_hpp_hints.v
-28.95%	15.7	11.2	-4.5	bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_model.v
-28.95%	44.4	31.5	-12.8	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/defs.v
-28.94%	18.2	12.9	-5.3	bluerock/bhv/zeta/lib/fdt/proof/reglist_hpp_spec.v
-28.90%	33.9	24.1	-9.8	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters.v
-28.87%	18.5	13.2	-5.3	bluerock/NOVA/build-proof/proof/kobject_hpp_spec/type.v
-28.84%	18.2	13.0	-5.3	bluerock/bhv/zeta/lib/cxx/proof/sys/semaphore_hpp_spec.v
-28.82%	36.0	25.6	-10.4	bluerock/bhv/lib/vrl/proof/vrl/port_map_hints.v
-28.81%	18.3	13.0	-5.3	bluerock/bhv/zeta/lib/intrusive/proof/dlist_internal_hpp_proof.v
-28.79%	18.3	13.0	-5.3	bluerock/bhv/zeta/lib/concurrent/proof/ticket_lock_hpp_spec.v
-28.78%	22.5	16.0	-6.5	bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/msr_info_hpp_spec.v
-28.71%	19.8	14.1	-5.7	bluerock/NOVA/build-proof/proof/ec_hpp_spec/fpu_triples.v
-28.64%	19.8	14.2	-5.7	bluerock/NOVA/build-proof/proof/pd_hpp_spec.v
-28.63%	32.8	23.4	-9.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol.v
-28.61%	19.8	14.2	-5.7	bluerock/NOVA/build-proof/proof/soup.v
-28.60%	18.2	13.0	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/brick_eval/bad/uninitialized_memory.v
-28.59%	18.4	13.1	-5.3	bluerock/bhv/zeta/lib/zeta/proof/zeta_hpp_spec.v
-28.56%	18.4	13.1	-5.3	bluerock/bhv/zeta/lib/nova/proof/syscall_hpp_spec.v
-28.54%	12.8	9.1	-3.7	bluerock/NOVA/build-proof/proof/aarch64/vmcb.v
-28.48%	65.3	46.7	-18.6	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/lec_stack_size.v
-28.45%	26.4	18.9	-7.5	bluerock/NOVA/build-proof/proof/iface/predicates/ec_info.v
-28.44%	18.5	13.2	-5.3	bluerock/bhv/apps/umx/proof/channel.v
-28.44%	21.4	15.3	-6.1	bluerock/NOVA/build-proof/proof/slab/slab_cache_alloc.v
-28.43%	18.5	13.2	-5.3	bluerock/bhv/zeta/lib/porter/proof/marshal_hpp_spec.v
-28.42%	18.5	13.2	-5.3	bluerock/bhv/apps/umx/proof/spec_prelude.v
-28.33%	19.7	14.1	-5.6	bluerock/NOVA/build-proof/proof/sc_hpp_spec.v
-28.33%	41.7	29.9	-11.8	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/defs.v
-28.24%	18.9	13.6	-5.4	bluerock/bhv/zeta/lib/lang/proof/verif_hpp_spec.v
-28.24%	18.9	13.6	-5.3	fmdeps/auto-docs/content/docs/simple/test.v
-28.21%	18.6	13.4	-5.3	bluerock/bhv/zeta/lib/fdt/proof/as_hpp_spec.v
-28.19%	18.6	13.4	-5.3	bluerock/bhv/zeta/lib/alloc/proof/malloc_cpp_proof.v
-28.18%	18.4	13.2	-5.2	bluerock/bhv/zeta/lib/msc/proof/sys/signal_hpp_spec.v
-28.17%	19.8	14.2	-5.6	bluerock/NOVA/build-proof/proof/sm_hpp_spec.v
-28.17%	15.6	11.2	-4.4	bluerock/NOVA/build-proof/proof/aarch64/interrupt_hpp_spec.v
-28.12%	47.6	34.2	-13.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/spec.v
-28.11%	23.0	16.5	-6.5	bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_cpp_proof/register.v
-28.11%	23.0	16.5	-6.5	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/model/cpu_affinity_hpp_spec.v
-28.10%	20.1	14.4	-5.6	bluerock/NOVA/build-proof/proof/ec_hpp_spec/abs_pred.v
-28.09%	36.9	26.6	-10.4	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/proof.v
-28.07%	13.0	9.4	-3.7	bluerock/NOVA/build-proof/proof/aarch64/utcb.v
-28.03%	18.8	13.5	-5.3	bluerock/bhv/zeta/lib/porter/proof/server_hpp_spec.v
-28.01%	43.1	31.0	-12.1	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/defs.v
-27.97%	20.6	14.9	-5.8	bluerock/NOVA/build-proof/proof/aarch64/ec_hpp_spec/exc_triples.v
-27.96%	21.0	15.1	-5.9	bluerock/NOVA/build-proof/proof/aarch64/ec_hpp_spec.v
-27.92%	24.5	17.6	-6.8	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/deps.v
-27.91%	19.3	13.9	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/includes/A_o.v
-27.86%	54.7	39.5	-15.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/vqueue_interface.v
-27.82%	25.8	18.6	-7.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/model/iommu_interface_hpp/hints.v
-27.81%	29.4	21.2	-8.2	bluerock/bhv/apps/vswitch/lib/protocol/proof/virtio_net_hpp_proof.v
-27.79%	20.4	14.8	-5.7	bluerock/bhv/apps/vmm/vml/config/vmm_debug/proof/vm_abort_hpp_proof.v
-27.76%	48.6	35.1	-13.5	bluerock/bhv/apps/vmm/lib/board/proof/aarch64/board_cpp_proof.v
-27.72%	29.4	21.2	-8.1	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_config_hpp_spec.v
-27.71%	30.0	21.7	-8.3	bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp_spec.v
-27.71%	29.2	21.1	-8.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/prelude/proof.v
-27.69%	14.2	10.3	-3.9	fmdeps/auto/coq-bluerock-auto-cpp/tests/reps/rep_auto.v
-27.69%	23.7	17.1	-6.6	bluerock/bhv/apps/vmm/vml/devices/msr/proof/msr_id_hpp_spec.v
-27.66%	29.5	21.3	-8.2	bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp_proof.v
-27.66%	21.1	15.3	-5.8	bluerock/NOVA/build-proof/proof/iface.v
-27.64%	14.8	10.7	-4.1	bluerock/NOVA/build-proof/proof/soup/stamp.v
-27.60%	23.1	16.7	-6.4	bluerock/NOVA/build-proof/proof/slab/slab_proof_cmra.v
-27.59%	23.4	16.9	-6.5	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_hpp_spec/space_view_defs.v
-27.58%	19.4	14.0	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/includes/A_cpp_proof.v
-27.57%	19.4	14.1	-5.4	bluerock/bhv/zeta/lib/lang/proof/new_hpp_proof.v
-27.55%	45.0	32.6	-12.4	bluerock/bhv/apps/vswitch/lib/protocol/proof/virtio_net_hpp/hints.v
-27.53%	23.8	17.2	-6.5	bluerock/bhv/lib/ddk/proof/transformers.v
-27.53%	48.1	34.8	-13.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_spec.v
-27.51%	37.1	26.9	-10.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/msr_bus_hpp_spec.v
-27.50%	19.5	14.1	-5.4	bluerock/bhv/zeta/apps/msc/proof/hp_hpp_spec.v
-27.50%	45.5	33.0	-12.5	bluerock/bhv/apps/vmm/lib/board/proof/model/board_hpp_spec.v
-27.47%	14.9	10.8	-4.1	bluerock/NOVA/build-proof/proof/soup/count.v
-27.41%	49.7	36.1	-13.6	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_hpp_spec/space_view.v
-27.39%	47.7	34.6	-13.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/callback_impl.v
-27.39%	27.0	19.6	-7.4	bluerock/bhv/lib/vconnect/proof/vconnect/async_control_hpp/proof.v
-27.31%	19.6	14.2	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0076_cpp_f1_proof.v
-27.28%	15.9	11.6	-4.3	bluerock/NOVA/build-proof/proof/aarch64/mtd_arch_hpp_spec.v
-27.27%	36.3	26.4	-9.9	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/prelude/hints.v
-27.26%	17.3	12.6	-4.7	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/prelude/spec.v
-27.24%	27.0	19.6	-7.3	bluerock/bhv/lib/vconnect/proof/vconnect/async_control_hpp/prelude/spec.v
-27.18%	19.7	14.3	-5.3	bluerock/NOVA/build-proof/proof/globals.v
-27.16%	23.8	17.3	-6.5	bluerock/bhv/apps/vmm/lib/bluerock/proof/fdt_hpp_spec.v
-27.15%	30.1	21.9	-8.2	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_config_hpp/proof.v
-27.15%	27.1	19.8	-7.4	bluerock/bhv/lib/vconnect/proof/vconnect/async_control_hpp/defs.v
-27.12%	20.3	14.8	-5.5	bluerock/NOVA/build-proof/proof/slab_hpp_spec.v
-27.11%	29.9	21.8	-8.1	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_config_hpp/hints.v
-27.11%	19.4	14.1	-5.3	bluerock/bhv/zeta/lib/zeta/proof/timer_hpp_spec.v
-27.09%	67.7	49.4	-18.3	bluerock/bhv/apps/vmm/proof/main_cpp_proof/hints.v
-27.07%	16.5	12.1	-4.5	bluerock/bhv/lib/ddk/proof/mmio.v
-27.07%	29.9	21.8	-8.1	bluerock/bhv/apps/vswitch/lib/acl/proof/match_field_types_hpp_spec.v
-27.06%	21.1	15.4	-5.7	bluerock/NOVA/build-proof/proof/status_hpp_spec.v
-27.05%	30.0	21.8	-8.1	bluerock/bhv/apps/vswitch/lib/acl/proof/match_field_types_hpp_proof.v
-27.00%	30.0	21.9	-8.1	bluerock/bhv/apps/vswitch/lib/acl/proof/flow_entry_hpp_spec.v
-27.00%	19.8	14.5	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/return_void/main_cpp_proof.v
-27.00%	34.4	25.1	-9.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/prelude/hints.v
-26.99%	20.6	15.1	-5.6	bluerock/NOVA/build-proof/proof/cpu_hpp_spec/cpulocal.v
-26.98%	27.4	20.0	-7.4	bluerock/bhv/lib/vconnect/proof/vconnect/async_control_hpp/spec.v
-26.97%	27.7	20.2	-7.5	bluerock/NOVA/build-proof/proof/iface/hypercall/pt.v
-26.97%	57.8	42.2	-15.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/cpp_hints.v
-26.95%	30.0	21.9	-8.1	bluerock/bhv/apps/vswitch/lib/acl/proof/packet_field_hpp_spec.v
-26.94%	19.5	14.3	-5.3	bluerock/bhv/zeta/lib/cxx/proof/bitset_hpp_spec.v
-26.91%	30.1	22.0	-8.1	bluerock/bhv/apps/vswitch/lib/acl/proof/parser_hpp_spec.v
-26.90%	30.1	22.0	-8.1	bluerock/bhv/apps/vswitch/lib/protocol/proof/ipv4_hpp_spec.v
-26.90%	19.9	14.5	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0068_cpp_f2_proof.v
-26.90%	13.8	10.1	-3.7	fmdeps/auto/coq-bluerock-auto-cpp/tests/arch_indep/reg_accessor_combined_model.v
-26.89%	30.1	22.0	-8.1	bluerock/bhv/apps/vswitch/lib/acl/proof/flow_list_hpp_spec.v
-26.87%	27.5	20.1	-7.4	bluerock/bhv/lib/vconnect/proof/vconnect/async_control_hpp/prelude/proof.v
-26.86%	51.7	37.8	-13.9	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_hpp_spec.v
-26.83%	34.8	25.5	-9.3	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/chain_walking_callback.v
-26.82%	30.2	22.1	-8.1	bluerock/bhv/apps/vswitch/lib/protocol/proof/ipv6_hpp_spec.v
-26.82%	20.0	14.7	-5.4	bluerock/NOVA/build-proof/proof/refcnt_hpp_spec.v
-26.82%	34.8	25.5	-9.3	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/bulk_copier.v
-26.81%	29.4	21.5	-7.9	bluerock/bhv/apps/vmm/vml/devices/irq_controller/proof/model/irq_controller_hpp_spec.v
-26.80%	28.7	21.0	-7.7	bluerock/bhv/apps/vswitch/lib/protocol/proof/virtio_net_hpp/defs.v
-26.78%	34.2	25.0	-9.1	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp_spec.v
-26.78%	20.0	14.6	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0036_cpp_f1_proof.v
-26.74%	49.9	36.5	-13.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints.v
-26.71%	19.7	14.4	-5.2	bluerock/bhv/zeta/lib/alloc/proof/unique_sels_hpp_spec.v
-26.67%	19.7	14.5	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/virtual/virtual_destructor_cpp_spec.v
-26.67%	33.5	24.6	-8.9	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/prelude/proof.v
-26.65%	21.2	15.5	-5.6	bluerock/NOVA/build-proof/proof/timeout_budget_cpp_proof.v
-26.64%	33.0	24.2	-8.8	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/hints.v
-26.62%	29.9	21.9	-7.9	bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/signal_hpp_proof.v
-26.61%	33.4	24.5	-8.9	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/prelude/spec.v
-26.61%	30.5	22.4	-8.1	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_config_hpp/prelude/hints.v
-26.61%	30.4	22.3	-8.1	bluerock/bhv/apps/vswitch/lib/acl/proof/acl_config_hpp_spec.v
-26.60%	38.0	27.9	-10.1	bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_hpp_spec.v
-26.59%	30.5	22.4	-8.1	bluerock/bhv/apps/vswitch/proof/prelude/proof.v
-26.56%	14.1	10.3	-3.7	fmdeps/auto/coq-bluerock-auto-cpp/tests/constants/constants_cpp_spec.v
-26.55%	33.5	24.6	-8.9	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/prelude/hints.v
-26.55%	16.9	12.4	-4.5	bluerock/bhv/lib/ddk/proof/init.v
-26.54%	30.8	22.6	-8.2	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_config_hpp/spec.v
-26.53%	21.8	16.0	-5.8	bluerock/NOVA/build-proof/proof/ec_hpp_spec/mode_pred.v
-26.48%	34.1	25.1	-9.0	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/prelude/hints.v
-26.48%	14.9	11.0	-4.0	bluerock/bhv/apps/vswitch/proof/model/vswitch/prelude/lemmas.v
-26.47%	30.6	22.5	-8.1	bluerock/bhv/apps/vswitch/lib/protocol/proof/virtio_net_hpp/spec.v
-26.46%	14.0	10.3	-3.7	fmdeps/auto/coq-bluerock-auto-cpp/tests/arch_indep/proof_imports.v
-26.41%	12.5	9.2	-3.3	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/prelude/model.v
-26.41%	12.5	9.2	-3.3	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/prelude/model.v
-26.41%	12.5	9.2	-3.3	bluerock/bhv/apps/vswitch/lib/port/proof/port/prelude/model.v
-26.40%	12.5	9.2	-3.3	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_config_hpp/prelude/model.v
-26.39%	45.8	33.7	-12.1	bluerock/bhv/apps/vmm/lib/board/proof/model/board_hpp_hints.v
-26.38%	30.7	22.6	-8.1	bluerock/bhv/apps/vswitch/lib/protocol/proof/udp_hpp_spec.v
-26.35%	20.3	14.9	-5.3	fmdeps/auto-docs/content/docs/fractional-sharing/intro.v
-26.33%	30.7	22.6	-8.1	bluerock/bhv/apps/vswitch/lib/protocol/proof/tcp_hpp_spec.v
-26.33%	14.1	10.4	-3.7	fmdeps/auto/coq-bluerock-auto-cpp/tests/arch_indep/spec_imports.v
-26.33%	26.3	19.4	-6.9	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/wp_vcpu/axioms.v
-26.28%	29.0	21.4	-7.6	bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/prelude/defs.v
-26.26%	29.7	21.9	-7.8	bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/prelude/spec.v
-26.25%	14.8	10.9	-3.9	fmdeps/auto/coq-bluerock-auto-cpp/tests/llist_cpp/new_hpp_spec.v
-26.22%	30.9	22.8	-8.1	bluerock/bhv/apps/vswitch/lib/protocol/proof/ip_hpp_spec.v
-26.19%	14.2	10.5	-3.7	fmdeps/auto/coq-bluerock-auto-cpp/tests/arch_indep/reg_accessor_common_model.v
-26.18%	31.0	22.8	-8.1	bluerock/bhv/apps/vswitch/lib/port/proof/port/upstream.v
-26.16%	31.2	23.1	-8.2	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_config_hpp/prelude/proof.v
-26.14%	28.1	20.8	-7.3	bluerock/NOVA/build-proof/proof/syscall_cpp_spec/accessors.v
-26.08%	20.6	15.3	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/includes/A_hpp_proof.v
-26.08%	20.2	14.9	-5.3	bluerock/bhv/zeta/lib/cxx/proof/unique_ptr_hpp_spec.v
-26.07%	21.1	15.6	-5.5	bluerock/NOVA/build-proof/proof/kobject_hpp_spec/triples.v
-26.06%	31.1	23.0	-8.1	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_config_hpp/prelude/spec.v
-26.04%	20.2	15.0	-5.3	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_hpp_spec/upstream.v
-26.03%	15.1	11.2	-3.9	bluerock/bhv/zeta/lib/fdt/proof/fdt.v
-26.02%	21.1	15.6	-5.5	bluerock/bhv/zeta/lib/intrusive/proof/map_hpp_proof.v
-26.02%	39.1	28.9	-10.2	bluerock/bhv/lib/vrl/proof/vrl/dataplane_hpp_spec.v
-26.02%	31.1	23.0	-8.1	bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/prelude/hints.v
-25.98%	31.2	23.1	-8.1	bluerock/bhv/apps/vswitch/lib/protocol/proof/virtio_net_hpp/prelude/proof.v
-25.95%	31.2	23.1	-8.1	bluerock/bhv/apps/vswitch/lib/acl/proof/actions_hpp_spec.v
-25.91%	20.9	15.5	-5.4	bluerock/NOVA/build-proof/proof/regs_hpp_spec/exc_regs.v
-25.89%	31.2	23.2	-8.1	bluerock/bhv/apps/vswitch/lib/acl/proof/acl_hpp_spec.v
-25.86%	28.8	21.3	-7.4	bluerock/bhv/apps/vswitch/proof/prelude/defs.v
-25.85%	20.6	15.3	-5.3	bluerock/bhv/zeta/lib/intrusive/proof/shared_pointer_hpp_spec.v
-25.83%	12.7	9.5	-3.3	bluerock/bhv/apps/vswitch/proof/model/nic.v
-25.82%	20.8	15.4	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/constants/constants_cpp_proof.v
-25.81%	20.1	14.9	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/specify_cmd/specify_cmd_hpp_spec.v
-25.78%	24.6	18.2	-6.3	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/ghost_common.v
-25.74%	21.4	15.9	-5.5	bluerock/NOVA/build-proof/proof/ec_hpp_spec/call_chain.v
-25.70%	31.5	23.4	-8.1	bluerock/bhv/apps/vswitch/lib/acl/proof/matcher_hpp_spec.v
-25.69%	20.9	15.5	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/specify/challenge/main_cpp_proof.v
-25.66%	31.6	23.5	-8.1	bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/prelude/proof.v
-25.65%	21.1	15.7	-5.4	bluerock/NOVA/build-proof/proof/kobject_hpp_spec/abs_pred.v
-25.62%	21.0	15.6	-5.4	bluerock/bhv/zeta/lib/intrusive/proof/map_hpp_spec.v
-25.62%	20.5	15.3	-5.3	bluerock/bhv/apps/umx/proof/admin_hpp_spec.v
-25.61%	16.2	12.0	-4.1	bluerock/bhv/apps/vswitch/proof/model/util.v
-25.59%	39.7	29.5	-10.2	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/guest_as_hpp_spec.v
-25.58%	10.8	8.0	-2.8	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_cpp_proof/hints.v
-25.54%	21.1	15.7	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/const/charptr_spec.v
-25.52%	30.0	22.4	-7.7	bluerock/bhv/apps/vswitch/lib/protocol/proof/virtio_net_hpp/prelude/spec.v
-25.52%	21.1	15.7	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0098_cpp_f1_proof.v
-25.51%	30.0	22.4	-7.7	bluerock/bhv/apps/vswitch/lib/protocol/proof/virtio_net_hpp/prelude/hints.v
-25.51%	33.0	24.6	-8.4	bluerock/bhv/apps/vswitch/proof/upstream/lts_inv.v
-25.50%	15.6	11.6	-4.0	bluerock/bhv/apps/vswitch/lib/protocol/proof/virtio_net_hpp/model.v
-25.50%	10.8	8.0	-2.8	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/specialize_wand.v
-25.47%	14.6	10.9	-3.7	fmdeps/auto/coq-bluerock-auto-cpp/tests/arch_indep/x86_64/reg_accessor_model.v
-25.47%	20.6	15.4	-5.3	bluerock/bhv/zeta/lib/intrusive/proof/list_hpp_spec.v
-25.45%	14.6	10.9	-3.7	fmdeps/auto/coq-bluerock-auto-cpp/tests/arch_indep/aarch64/reg_accessor_model.v
-25.43%	13.5	10.0	-3.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/arch_indep/model_imports.v
-25.42%	11.4	8.5	-2.9	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/upstream.v
-25.40%	36.0	26.9	-9.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/prelude/defs.v
-25.39%	31.9	23.8	-8.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/forwarding_table_private_hints.v
-25.39%	10.9	8.1	-2.8	fmdeps/auto/coq-bluerock-auto-cpp/theories/cpp/nullR.v
-25.34%	54.6	40.8	-13.9	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/as_layout_hpp_spec.v
-25.34%	21.7	16.2	-5.5	bluerock/NOVA/build-proof/proof/utcb_hpp_spec.v
-25.34%	20.8	15.5	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0036_cpp_spec.v
-25.33%	24.8	18.5	-6.3	bluerock/NOVA/build-proof/proof/cpu_cpp_proof/cls.v
-25.32%	22.2	16.6	-5.6	bluerock/NOVA/build-proof/proof/soup/base_pred.v
-25.31%	19.3	14.4	-4.9	bluerock/bhv/zeta/lib/lang/proof/util.v
-25.30%	10.9	8.1	-2.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/params/params_tests.v
-25.28%	15.4	11.5	-3.9	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/prelude/hints.v
-25.27%	21.2	15.8	-5.4	bluerock/bhv/zeta/lib/uuid/proof/uuid_hpp_spec.v
-25.27%	30.2	22.5	-7.6	bluerock/bhv/apps/vswitch/proof/prelude/hints.v
-25.26%	20.8	15.5	-5.3	bluerock/bhv/lib/vrl/proof/vrl/typeclasses.v
-25.22%	21.4	16.0	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/anonymous_union/test_cpp_proof.v
-25.20%	10.9	8.2	-2.8	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/upstream.v
-25.20%	10.9	8.2	-2.7	bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_cpp_proof/prelude.v
-25.20%	20.9	15.6	-5.3	bluerock/bhv/zeta/lib/fdt/proof/uart_hpp_spec.v
-25.17%	25.0	18.7	-6.3	bluerock/NOVA/build-proof/proof/sc_hpp_spec/hints.v
-25.16%	20.9	15.6	-5.3	bluerock/bhv/zeta/lib/alloc/proof/core_hpp_specs.v
-25.13%	30.3	22.7	-7.6	bluerock/bhv/apps/vswitch/proof/prelude/spec.v
-25.13%	26.1	19.5	-6.6	bluerock/NOVA/build-proof/proof/ec_hpp_spec/utcb_pred.v
-25.13%	21.5	16.1	-5.4	bluerock/NOVA/build-proof/proof/regs_hpp_spec/sys_regs.v
-25.12%	43.4	32.5	-10.9	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/init.v
-25.12%	15.8	11.8	-4.0	bluerock/bhv/apps/vswitch/proof/model/vswitch/model.v
-25.10%	37.2	27.9	-9.3	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/chain_accessor.v
-25.06%	32.3	24.2	-8.1	bluerock/bhv/apps/vswitch/lib/port/proof/port/prelude/hints.v
-25.02%	17.9	13.4	-4.5	bluerock/bhv/zeta/lib/nova/proof/hints.v
-25.01%	21.0	15.8	-5.3	bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/rwlock_spec.v
-24.98%	22.1	16.6	-5.5	bluerock/NOVA/build-proof/proof/space_hpp_spec.v
-24.98%	30.2	22.7	-7.5	bluerock/NOVA/build-proof/proof/iface/predicates/dma.v
-24.96%	15.6	11.7	-3.9	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/prelude/spec.v
-24.95%	14.8	11.1	-3.7	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_entry_hpp/portal_flags.v
-24.93%	21.0	15.7	-5.2	bluerock/bhv/zeta/apps/msc/proof/multiboot2_hpp_spec.v
-24.91%	70.4	52.8	-17.5	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_hpp_spec.v
-24.86%	21.2	15.9	-5.3	bluerock/bhv/zeta/lib/nova/proof/utcb_hpp_spec.v
-24.80%	23.2	17.4	-5.7	bluerock/bhv/lib/ddk/proof/mmio_bhv_hpp_spec.v
-24.79%	23.5	17.7	-5.8	bluerock/NOVA/build-proof/proof/syscall_cpp_spec/sys_finish_status.v
-24.78%	25.4	19.1	-6.3	bluerock/NOVA/build-proof/proof/iface/predicates/ec_regs_aarch64.v
-24.75%	32.8	24.7	-8.1	bluerock/bhv/apps/umx/proof/toplevel.v
-24.72%	23.2	17.4	-5.7	bluerock/NOVA/build-proof/proof/ec_hpp_spec/scheduler.v
-24.70%	23.9	18.0	-5.9	bluerock/NOVA/build-proof/proof/soup/hints.v
-24.67%	23.2	17.5	-5.7	bluerock/NOVA/build-proof/proof/ec_hpp_spec/status_triples.v
-24.63%	30.2	22.8	-7.4	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_config_hpp/prelude/defs.v
-24.62%	21.3	16.1	-5.3	bluerock/bhv/zeta/lib/lang/proof/vbytes.v
-24.60%	36.9	27.8	-9.1	bluerock/bhv/apps/vmm/lib/board/proof/model/board_common_hpp_spec.v
-24.58%	66.0	49.8	-16.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_spec.v
-24.58%	41.0	30.9	-10.1	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/roundup_parallel_specs.v
-24.57%	21.6	16.3	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/arch_indep/inheritance_hpp_base_spec.v
-24.55%	21.9	16.5	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/ast/span_cpp_proof.v
-24.53%	26.8	20.2	-6.6	bluerock/NOVA/build-proof/proof/timeout_cpp_proof/ctor.v
-24.52%	21.4	16.2	-5.3	bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/semaphore_hpp_spec.v
-24.52%	21.8	16.5	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/cpp_spec/test_default.v
-24.51%	21.4	16.1	-5.2	bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/utils.v
-24.48%	33.0	24.9	-8.1	bluerock/bhv/apps/vswitch/lib/port/proof/port/prelude/spec.v
-24.47%	52.5	39.6	-12.8	bluerock/bhv/apps/vmm/lib/board/proof/x86/board_cpp_proof.v
-24.45%	16.0	12.1	-3.9	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/prelude/proof.v
-24.42%	21.7	16.4	-5.3	bluerock/bhv/zeta/lib/lang/proof/bits_hpp_spec.v
-24.39%	30.5	23.1	-7.4	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/prelude/defs.v
-24.38%	55.0	41.6	-13.4	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/guest_chunk_repo_hpp_spec.v
-24.34%	21.6	16.3	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0096_cpp_spec.v
-24.31%	36.4	27.6	-8.9	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/used_entry/misc.v
-24.30%	21.9	16.6	-5.3	bluerock/NOVA/build-proof/proof/atomic_hpp_spec.v
-24.28%	32.7	24.8	-7.9	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/predicates.v
-24.26%	46.3	35.1	-11.2	bluerock/bhv/apps/vmm/vml/devices/simple_as/proof/simple_as_hpp_spec.v
-24.23%	22.2	16.8	-5.4	fmdeps/auto-docs/content/docs/common_errors/missing_type_instances.v
-24.20%	25.7	19.5	-6.2	bluerock/bhv/lib/ddk/proof/utils.v
-24.19%	31.6	24.0	-7.7	bluerock/bhv/apps/umx/proof/admin_cpp_spec.v
-24.18%	33.2	25.2	-8.0	bluerock/bhv/apps/vmm/lib/outpost_dummy/proof/outpost_hpp_spec.v
-24.16%	22.3	16.9	-5.4	bluerock/bhv/zeta/lib/intrusive/proof/list_internal_hpp_proof.v
-24.15%	21.8	16.5	-5.3	bluerock/bhv/lib/socket/proof/socket_defs_hpp_spec.v
-24.13%	21.8	16.5	-5.3	bluerock/bhv/zeta/lib/porter/proof/as_resource_hpp_spec.v
-24.08%	22.4	17.0	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0094_cpp_f2_proof.v
-24.07%	31.0	23.5	-7.5	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxclient/dtor.v
-24.04%	27.2	20.7	-6.5	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/model/vcpu_types_hpp_proof.v
-24.00%	31.7	24.1	-7.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/prelude/defs.v
-24.00%	31.7	24.1	-7.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/prelude/defs.v
-24.00%	9.2	7.0	-2.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/constants.v
-23.99%	33.5	25.5	-8.0	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/prelude/defs.v
-23.97%	16.7	12.7	-4.0	bluerock/bhv/apps/vmm/vml/config/vmm_debug/proof/vm_abort_hpp_spec.v
-23.96%	28.8	21.9	-6.9	bluerock/bhv/apps/vmm/vml/devices/msr/proof/msr_access_hpp_spec.v
-23.94%	36.8	28.0	-8.8	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/is_size_valid.v
-23.93%	22.0	16.7	-5.3	bluerock/bhv/zeta/lib/intrusive/proof/dlist_internal_hpp_spec.v
-23.90%	22.4	17.1	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/union/main_cpp_proof.v
-23.90%	22.7	17.3	-5.4	bluerock/bhv/zeta/lib/lang/proof/string_gnu_cpp_proof.v
-23.87%	37.7	28.7	-9.0	bluerock/bhv/apps/umx/proof/main_cpp_proof/publish.v
-23.87%	22.5	17.1	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/lambda/test_cpp_proof.v
-23.85%	26.4	20.1	-6.3	bluerock/bhv/lib/ddk/proof/atomic_updates.v
-23.84%	27.1	20.6	-6.5	bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/mutex_hpp_proof.v
-23.82%	52.6	40.1	-12.5	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/data_portsP_hints.v
-23.80%	9.3	7.1	-2.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/fractional.v
-23.78%	22.1	16.9	-5.3	bluerock/bhv/zeta/lib/intrusive/proof/dlist_hpp_spec.v
-23.76%	22.8	17.4	-5.4	bluerock/NOVA/build-proof/proof/aarch64/regs_cpp_proof/exc_regs.v
-23.76%	23.6	18.0	-5.6	bluerock/NOVA/build-proof/proof/ec_hpp_spec/timeout_triples.v
-23.75%	31.7	24.2	-7.5	bluerock/NOVA/build-proof/proof/iface/predicates/pd.v
-23.74%	33.6	25.6	-8.0	bluerock/bhv/apps/vmm/lib/board/proof/x86/board_impl_hpp_spec.v
-23.73%	29.0	22.1	-6.9	bluerock/bhv/apps/vmm/proof/bm_cpu.v
-23.73%	32.4	24.7	-7.7	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/prelude/hints.v
-23.69%	22.6	17.2	-5.3	fmdeps/auto-docs/content/docs/control_flow/loop.v
-23.69%	22.2	16.9	-5.3	bluerock/bhv/zeta/lib/zeta/proof/semaphore_hpp_spec.v
-23.67%	23.0	17.5	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/cpp_spec/template.v
-23.65%	22.7	17.3	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0059_cpp_f1_proof.v
-23.60%	27.3	20.8	-6.4	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/msr_bus_hpp_proof.v
-23.58%	41.8	32.0	-9.9	bluerock/bhv/apps/vmm/lib/vmi_interface/proof/vmi_interface_hpp_spec.v
-23.57%	22.3	17.0	-5.3	bluerock/bhv/zeta/lib/concurrent/proof/lock_hpp_spec.v
-23.57%	22.3	17.0	-5.3	bluerock/bhv/apps/vmm/vml/devices/vuart/proof/vuart/vuart_hpp_spec.v
-23.54%	34.4	26.3	-8.1	bluerock/bhv/apps/vswitch/lib/port/proof/port/prelude/proof.v
-23.53%	32.4	24.8	-7.6	bluerock/bhv/apps/vswitch/lib/port/proof/port/prelude/defs.v
-23.53%	33.2	25.4	-7.8	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxshared/switch_to_admin.v
-23.52%	22.3	17.1	-5.3	bluerock/bhv/apps/umx/proof/uart_hpp_spec.v
-23.49%	30.8	23.5	-7.2	bluerock/NOVA/build-proof/proof/ec_hpp_spec/ghosts.v
-23.45%	24.4	18.6	-5.7	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/triples.v
-23.44%	11.3	8.6	-2.6	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/elpi/derive/learn.v
-23.44%	27.1	20.7	-6.3	bluerock/NOVA/build-proof/proof/soup/info.v
-23.42%	23.0	17.6	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0092_cpp_f0_proof.v
-23.42%	31.7	24.3	-7.4	bluerock/NOVA/build-proof/proof/sm_hpp_spec/triples.v
-23.41%	14.0	10.8	-3.3	bluerock/bhv/apps/vswitch/proof/model/vswitch/prelude/defs.v
-23.40%	32.4	24.8	-7.6	bluerock/bhv/apps/umx/proof/admin_cpp_proof/beep.v
-23.40%	23.1	17.7	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/specify/challenge/identity_cpp_proof.v
-23.39%	9.4	7.2	-2.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/eval.v
-23.37%	69.9	53.6	-16.3	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/init.v
-23.34%	24.5	18.8	-5.7	bluerock/NOVA/build-proof/proof/space_obj_hpp_spec/triples.v
-23.30%	9.7	7.5	-2.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/templates/hints/wp_discard.v
-23.27%	23.5	18.0	-5.5	bluerock/bhv/zeta/lib/intrusive/proof/rangemap_hpp_proof.v
-23.23%	34.8	26.7	-8.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/prelude/spec.v
-23.23%	12.5	9.6	-2.9	bluerock/bhv/apps/vswitch/proof/prelude/model.v
-23.23%	23.5	18.1	-5.5	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0059_cpp_spec.v
-23.21%	32.5	25.0	-7.5	bluerock/NOVA/build-proof/proof/iface/predicates/mem.v
-23.21%	22.6	17.4	-5.3	bluerock/bhv/zeta/lib/zeta/proof/signal_hpp_spec.v
-23.12%	23.3	17.9	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0068_cpp_f1_proof.v
-23.11%	14.2	10.9	-3.3	bluerock/bhv/apps/vswitch/lib/protocol/proof/virtio_net_hpp/prelude/model.v
-23.09%	22.5	17.3	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/brick_eval/bad/out_of_bound.v
-23.06%	35.0	27.0	-8.1	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/foreign_ptr_spec.v
-23.05%	24.7	19.0	-5.7	fmdeps/auto/coq-bluerock-auto-cpp/tests/normalization/test.v
-23.05%	67.7	52.1	-15.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/virtio_net_header_hints.v
-23.04%	33.3	25.6	-7.7	bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/mutex_hpp_spec.v
-23.02%	14.3	11.0	-3.3	bluerock/bhv/apps/vswitch/proof/model/vswitch/prelude/model.v
-23.02%	27.7	21.3	-6.4	bluerock/bhv/apps/vswitch/lib/protocol/proof/virtio_net_hpp_spec.v
-22.98%	8.0	6.2	-1.8	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/big_sep/coercion.v
-22.98%	20.5	15.8	-4.7	bluerock/NOVA/build-proof/proof/basis/tls.v
-22.97%	58.0	44.7	-13.3	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/guest_chunk_repo_hpp_proof.v
-22.96%	8.1	6.2	-1.9	fmdeps/auto/coq-bluerock-auto-core/tests/modes.v
-22.95%	21.8	16.8	-5.0	bluerock/bhv/zeta/lib/intrusive/proof/rangemap_hpp_model.v
-22.94%	23.4	18.0	-5.4	fmdeps/auto-docs/content/docs/rep_hints/main.v
-22.93%	28.4	21.9	-6.5	bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_hints.v
-22.93%	27.5	21.2	-6.3	bluerock/bhv/zeta/lib/zeta/proof/mutex_hpp_spec.v
-22.92%	8.1	6.3	-1.9	fmdeps/auto/coq-bluerock-auto-core/tests/refine_lib.v
-22.91%	33.2	25.6	-7.6	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/as_layout_hpp_spec/defs.v
-22.91%	23.4	18.0	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0052_cpp_f1_proof.v
-22.88%	30.1	23.2	-6.9	bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/zynqmp_dma_ver_hpp_spec.v
-22.87%	58.2	44.9	-13.3	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp_spec2.v
-22.86%	11.6	9.0	-2.7	fmdeps/auto/coq-bluerock-auto-core/tests/disjunction.v
-22.86%	25.2	19.5	-5.8	bluerock/bhv/zeta/lib/bson/proof/bson_hpp_spec.v
-22.74%	23.1	17.9	-5.3	bluerock/bhv/zeta/lib/umx/proof/umx_hpp_spec.v
-22.71%	23.7	18.3	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0004_cpp_f0_proof.v
-22.71%	13.2	10.2	-3.0	fmdeps/auto/coq-bluerock-auto-cpp/tests/default_spec/argr.v
-22.68%	32.8	25.4	-7.4	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/prelude/defs.v
-22.67%	8.2	6.3	-1.9	fmdeps/auto/coq-bluerock-auto-core/tests/learn/fupd.v
-22.65%	8.2	6.3	-1.8	fmdeps/auto/coq-bluerock-auto-core/tests/sep.v
-22.59%	33.7	26.1	-7.6	bluerock/bhv/apps/vmm/vml/devices/msr/proof/msr_base_hpp_proof.v
-22.52%	23.5	18.2	-5.3	bluerock/bhv/lib/vrl/proof/vrl/port_list_payload.v
-22.48%	23.9	18.6	-5.4	bluerock/bhv/zeta/lib/lang/proof/string_cpp_hints.v
-22.48%	23.8	18.5	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0036_cpp_f2_proof.v
-22.42%	25.7	19.9	-5.8	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/vector/spec.v
-22.36%	28.0	21.7	-6.3	bluerock/NOVA/build-proof/proof/capability_hpp_spec/abs_pred.v
-22.36%	24.4	18.9	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0094_cpp_spec.v
-22.35%	17.9	13.9	-4.0	bluerock/NOVA/build-proof/proof/ec_hpp_spec/exc_pred.v
-22.34%	28.4	22.1	-6.4	bluerock/NOVA/build-proof/proof/timeout_hpp_spec/trigger.v
-22.29%	8.3	6.5	-1.9	fmdeps/auto/coq-bluerock-auto-core/tests/observe/test.v
-22.29%	9.9	7.7	-2.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/interp.v
-22.25%	24.2	18.8	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0094_cpp_f1_proof.v
-22.24%	8.8	6.9	-2.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/weakly_local_with.v
-22.22%	34.7	27.0	-7.7	bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/memory_hpp_spec.v
-22.21%	8.4	6.5	-1.9	fmdeps/auto/coq-bluerock-auto-core/tests/multimatch.v
-22.20%	24.3	18.9	-5.4	bluerock/bhv/zeta/lib/alloc/proof/core_proof_utils.v
-22.17%	29.1	22.7	-6.5	bluerock/bhv/zeta/lib/zeta/proof/helpers_hpp_spec.v
-22.16%	23.7	18.5	-5.3	bluerock/bhv/apps/vmm/proof/resource_hpp_spec.v
-22.14%	67.3	52.4	-14.9	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/recall.v
-22.14%	8.4	6.5	-1.9	fmdeps/auto/coq-bluerock-auto-core/tests/cancelx/bi_abd.v
-22.11%	10.2	8.0	-2.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/templates/hints/read_decl.v
-22.11%	10.5	8.2	-2.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/lazy_unfold/demo.v
-22.10%	69.0	53.7	-15.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/flood.v
-22.09%	34.2	26.6	-7.5	bluerock/NOVA/build-proof/proof/iface/predicates/sc.v
-22.04%	18.0	14.0	-4.0	bluerock/bhv/apps/vswitch/proof/model/vswitch/defs.v
-22.03%	23.9	18.6	-5.3	bluerock/bhv/lib/ddk/proof/chardev_hpp_spec.v
-22.03%	10.4	8.1	-2.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/templates/hints/normalize_type.v
-22.01%	26.7	20.8	-5.9	bluerock/NOVA/build-proof/proof/ec_hpp_spec.v
-22.00%	9.0	7.0	-2.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/proofmode/cpp/_at_eq_cinv.v
-21.87%	24.4	19.1	-5.3	fmdeps/auto-docs/content/docs/debugging/main.v
-21.87%	26.1	20.4	-5.7	bluerock/bhv/zeta/lib/fdt/proof/fdt_hpp_spec.v
-21.84%	24.6	19.2	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/data_class/dataclass_const_hpp_spec.v
-21.78%	10.1	7.9	-2.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/heap_pred.v
-21.77%	33.6	26.3	-7.3	bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/esr_hpp_spec.v
-21.73%	54.7	42.8	-11.9	bluerock/bhv/apps/vswitch/proof/upstream/hints.v
-21.68%	8.8	6.9	-1.9	fmdeps/auto/coq-bluerock-auto-cpp/tests/elpi/enums/golden_variant.v
-21.68%	35.4	27.7	-7.7	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_hpp_spec/space_sel.v
-21.64%	24.2	19.0	-5.2	bluerock/bhv/lib/drivers/serial/pl011/proof/utils.v
-21.64%	17.2	13.5	-3.7	bluerock/bhv/zeta/lib/cxx/proof/sys/mutex_hpp_spec.v
-21.54%	9.9	7.8	-2.1	fmdeps/auto/coq-bluerock-auto-cpp/tests/micromega/micromega2.v
-21.52%	24.7	19.3	-5.3	bluerock/bhv/zeta/lib/lang/proof/atomic_hpp_spec.v
-21.52%	13.8	10.8	-3.0	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/prelude/defs.v
-21.46%	24.4	19.2	-5.2	bluerock/bhv/lib/vrl/proof/vrl/control_plane_spec.v
-21.46%	24.5	19.2	-5.3	bluerock/bhv/zeta/lib/porter/proof/shareable_hpp_spec.v
-21.43%	10.7	8.4	-2.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/templates/hints/wp_expr.v
-21.40%	47.0	37.0	-10.1	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctrl_feature_on_vcpu.v
-21.36%	8.7	6.8	-1.9	fmdeps/auto/coq-bluerock-auto-core/tests/boxes.v
-21.26%	24.7	19.5	-5.3	bluerock/bhv/apps/vmm/proof/model.v
-21.22%	51.0	40.2	-10.8	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_spec.v
-21.17%	32.5	25.6	-6.9	bluerock/bhv/apps/vmm/lib/bluerock/proof/aarch64/reg_accessor_hpp_spec.v
-21.12%	24.9	19.6	-5.3	bluerock/bhv/lib/ddk/proof/interrupt_bhv_spec.v
-21.11%	24.9	19.6	-5.3	bluerock/bhv/apps/vmm/lib/board/proof/model/common.v
-21.10%	21.2	16.7	-4.5	bluerock/bhv/apps/vmm/proof/bm.v
-21.06%	27.4	21.6	-5.8	bluerock/NOVA/build-proof/proof/syscall_cpp_spec/syscall.v
-21.03%	26.7	21.1	-5.6	bluerock/bhv/zeta/lib/fdt/proof/fdt_hpp_dataclass_spec.v
-21.01%	40.1	31.7	-8.4	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/hints.v
-21.00%	25.3	20.0	-5.3	bluerock/bhv/apps/vmm/proof/guestpt.v
-20.99%	25.5	20.1	-5.3	fmdeps/auto-docs/content/docs/class_reps/alt.v
-20.95%	15.2	12.0	-3.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/has_type.v
-20.93%	13.3	10.5	-2.8	bluerock/bhv/zeta/lib/lang/proof/endian_hpp_util.v
-20.91%	14.3	11.3	-3.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/vc_rw_defs.v
-20.85%	40.5	32.1	-8.5	bluerock/bhv/apps/vswitch/lib/util/proof/profiler_hpp_spec.v
-20.78%	62.5	49.5	-13.0	bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/defs.v
-20.77%	25.5	20.2	-5.3	bluerock/bhv/zeta/lib/lang/proof/errno_hpp_spec.v
-20.76%	34.4	27.3	-7.1	bluerock/bhv/apps/vswitch/lib/vsmp/proof/msg_queue_hpp/spec.v
-20.76%	13.3	10.5	-2.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/operator_auto/test_cpp_proof.v
-20.73%	28.5	22.6	-5.9	bluerock/bhv/lib/vrl/proof/vrl/port_hpp_hint.v
-20.73%	37.0	29.4	-7.7	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxshared/active_client.v
-20.72%	48.7	38.6	-10.1	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/cpu_feature_hpp_derived_specs.v
-20.70%	39.0	30.9	-8.1	bluerock/NOVA/build-proof/proof/iface/hypercall/sm.v
-20.65%	8.3	6.6	-1.7	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/to_bool.v
-20.62%	26.1	20.7	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0036_cpp_f0_proof.v
-20.60%	29.1	23.1	-6.0	bluerock/bhv/apps/vmm/vml/devices/vuart/proof/seq_queue_spec.v
-20.59%	25.5	20.3	-5.3	bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/signal_hpp_spec.v
-20.58%	7.1	5.6	-1.5	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/templates/semantics/report_me.v
-20.58%	30.4	24.1	-6.3	bluerock/NOVA/build-proof/proof/cpp/restrict.v
-20.53%	37.3	29.7	-7.7	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_hpp_spec/spaces_config.v
-20.51%	34.0	27.1	-7.0	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/wp_vcpu/memory1.v
-20.49%	15.0	11.9	-3.1	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/ptrs/valid_type_ptr.v
-20.46%	9.9	7.9	-2.0	fmdeps/auto/coq-bluerock-auto-cpp/tests/deps/deps_test.v
-20.45%	32.1	25.5	-6.6	bluerock/bhv/zeta/lib/zeta/proof/mutex_hpp_proof.v
-20.43%	18.6	14.8	-3.8	bluerock/bhv/apps/vswitch/lib/vsmp/proof/msg_queue_hpp/prelude.v
-20.37%	41.0	32.7	-8.4	bluerock/NOVA/build-proof/proof/iface/predicates/ec.v
-20.36%	29.4	23.4	-6.0	bluerock/bhv/lib/ddk/proof/compatible.v
-20.34%	27.6	22.0	-5.6	bluerock/NOVA/build-proof/proof/spinlock_hpp_proof/lc_lock.v
-20.32%	28.3	22.6	-5.8	bluerock/bhv/zeta/lib/fdt/proof/property_hpp_spec.v
-20.21%	9.8	7.8	-2.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/proofmode/cpp/_at_pureR.v
-20.21%	9.8	7.9	-2.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/borrowR.v
-20.17%	36.5	29.1	-7.4	bluerock/NOVA/build-proof/proof/soup/shared.v
-20.17%	25.9	20.7	-5.2	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/model/cpu_feature_hpp_derived_specs.v
-20.14%	25.8	20.6	-5.2	bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/util.v
-20.10%	39.8	31.8	-8.0	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_hpp_spec/reg_simulation.v
-20.08%	31.8	25.4	-6.4	bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_spec.v
-20.08%	73.4	58.6	-14.7	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints.v
-20.03%	40.4	32.3	-8.1	bluerock/NOVA/build-proof/proof/iface/hypercall/spc.v
-20.01%	14.8	11.8	-3.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/auto_frac/base.v
-19.99%	9.3	7.4	-1.9	fmdeps/auto/coq-bluerock-auto-core/tests/fwd/test.v
-19.99%	29.9	24.0	-6.0	bluerock/NOVA/build-proof/proof/space_hpp_proof.v
-19.96%	13.8	11.1	-2.8	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/lift_at_seps_fwd.v
-19.92%	29.2	23.4	-5.8	bluerock/bhv/lib/vrl/proof/vrl/shared_hpp_hints.v
-19.89%	60.7	48.6	-12.1	bluerock/bhv/apps/vswitch/lib/vsmp/proof/msg_queue_hpp/hints.v
-19.89%	7.7	6.2	-1.5	bluerock/bhv/lib/ddk/include/ddk/aarch64_chardev_drv_hpp.v
-19.88%	26.9	21.5	-5.3	bluerock/bhv/zeta/lib/concurrent/proof/ring_buffer.v
-19.88%	70.7	56.6	-14.0	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_cpp_proof/space_view.v
-19.83%	13.9	11.1	-2.7	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/patterns.v
-19.81%	9.4	7.5	-1.9	fmdeps/auto/coq-bluerock-auto-core/tests/existential.v
-19.79%	20.0	16.0	-4.0	bluerock/bhv/apps/vswitch/lib/protocol/proof/virtio_net_hpp/prelude/ghost.v
-19.77%	27.2	21.9	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/data_class/class_4_cpp_proof.v
-19.75%	10.5	8.4	-2.1	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/anyR.v
-19.75%	26.4	21.2	-5.2	bluerock/bhv/zeta/lib/lang/proof/string_hpp_spec.v
-19.71%	11.3	9.0	-2.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/big_sep/lemmas.v
-19.71%	30.7	24.7	-6.1	bluerock/NOVA/build-proof/proof/pt_hpp_spec/abs_pred.v
-19.71%	27.1	21.7	-5.3	bluerock/bhv/lib/vrl/proof/vrl/route_hpp_proof.v
-19.70%	32.8	26.3	-6.5	bluerock/NOVA/build-proof/proof/ec_hpp_spec/call_chain_pred.v
-19.67%	15.3	12.3	-3.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/base_logic/lib/darray.v
-19.64%	6.0	4.9	-1.2	bluerock/NOVA/build-proof/proof/cpp/bi_prelude.v
-19.63%	34.2	27.5	-6.7	bluerock/NOVA/build-proof/proof/sc_hpp_spec/abs_pred.v
-19.55%	14.2	11.4	-2.8	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/templates/upstream/brick/learn.v
-19.55%	26.9	21.6	-5.3	bluerock/bhv/apps/vmm/vml/devices/timer/proof/aa64_timer_hpp_spec.v
-19.50%	27.4	22.0	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/virtual/virtual_cpp_proof.v
-19.48%	71.2	57.3	-13.9	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/packet_ctor.v
-19.47%	63.8	51.4	-12.4	bluerock/bhv/apps/vswitch/lib/protocol/proof/virtio_net_hpp/proof.v
-19.46%	32.8	26.4	-6.4	bluerock/NOVA/build-proof/proof/timeout_cpp_proof/sync.v
-19.43%	32.0	25.8	-6.2	bluerock/NOVA/build-proof/proof/timeout_hypercall_hpp_spec.v
-19.37%	24.3	19.6	-4.7	fmdeps/auto/coq-bluerock-auto-cpp/tests/llist_cpp/forward_list_hpp_hints.v
-19.30%	12.0	9.7	-2.3	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/model/virtq/step/device.v
-19.23%	27.1	21.9	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/lib_alloc/alloc_hpp_spec.v
-19.18%	14.5	11.7	-2.8	bluerock/bhv/zeta/lib/intrusive/proof/map_hpp_data_proof.v
-19.17%	28.3	22.9	-5.4	bluerock/NOVA/build-proof/proof/bits_hpp_proof.v
-19.10%	21.0	17.0	-4.0	fmdeps/auto/coq-bluerock-auto-cpp/tests/spec/example_cpp_proof.v
-19.09%	19.0	15.4	-3.6	fmdeps/auto/coq-bluerock-auto-cpp/theories/cpp/unaligned.v
-19.09%	33.5	27.1	-6.4	bluerock/bhv/zeta/lib/nova/proof/types_hpp_spec.v
-19.08%	6.3	5.1	-1.2	fmdeps/auto/coq-bluerock-auto-core/theories/internal/lib/gather_all.v
-19.05%	11.1	9.0	-2.1	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/elpi/cpp_const.v
-19.05%	10.9	8.8	-2.1	bluerock/bhv/zeta/lib/nova/proof/model.v
-19.04%	28.1	22.7	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/static_methods/main_cpp_proof.v
-19.04%	64.9	52.5	-12.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/ghost_hints.v
-18.99%	35.4	28.7	-6.7	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/prelude.v
-18.98%	40.1	32.5	-7.6	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxshared/atomic_switch_to.v
-18.98%	36.4	29.5	-6.9	bluerock/bhv/lib/vrl/proof/vrl/route_hpp_spec.v
-18.98%	21.1	17.1	-4.0	fmdeps/auto/coq-bluerock-auto-cpp/tests/local_scope/local_scope_cpp_proof.v
-18.97%	14.6	11.8	-2.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/derive/bi_derive.v
-18.96%	26.7	21.7	-5.1	bluerock/bhv/zeta/lib/nova/proof/safe.v
-18.93%	10.6	8.6	-2.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/templates/logic/wp.v
-18.79%	12.9	10.5	-2.4	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/base.v
-18.76%	8.1	6.6	-1.5	bluerock/bhv/zeta/lib/lang/src/aarch64_string_cpp.v
-18.75%	6.6	5.3	-1.2	fmdeps/auto/coq-bluerock-auto-core/theories/internal/syntactic_bi/forced/simplify_sepT.v
-18.70%	44.6	36.2	-8.3	bluerock/bhv/lib/vconnect/proof/vconnect/guest_as_hpp_spec.v
-18.70%	39.0	31.7	-7.3	bluerock/bhv/apps/umx/proof/main_cpp_proof/umxservice.v
-18.70%	17.0	13.9	-3.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/tactics4/test_cancelx.v
-18.68%	8.1	6.6	-1.5	bluerock/bhv/zeta/lib/lang/include/aarch64_bits_hpp.v
-18.65%	14.4	11.8	-2.7	bluerock/bhv/zeta/lib/nova/proof/x86_64/exc_hpp_spec.v
-18.65%	38.8	31.5	-7.2	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxclient/uninit_ctor.v
-18.58%	35.7	29.1	-6.6	bluerock/NOVA/build-proof/proof/scheduler_hpp_spec/triples.v
-18.57%	35.7	29.1	-6.6	bluerock/NOVA/build-proof/proof/ec_hpp_spec/regs_pred.v
-18.55%	10.7	8.7	-2.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/pretty/work_pretty.v
-18.53%	9.8	8.0	-1.8	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/breakpoints.v
-18.50%	28.6	23.3	-5.3	bluerock/bhv/zeta/lib/lang/proof/new_hpp_spec.v
-18.48%	9.8	8.0	-1.8	fmdeps/auto/coq-bluerock-auto-cpp/theories/base_logic/lib/ghost_frac.v
-18.47%	30.4	24.8	-5.6	bluerock/NOVA/build-proof/proof/abi_hpp_proof.v
-18.44%	48.5	39.6	-8.9	bluerock/bhv/apps/umx/proof/main_cpp_spec.v
-18.42%	40.5	33.0	-7.5	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/model/cpu_feature_hpp_spec.v
-18.41%	15.3	12.5	-2.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/tactics4/custom_tactics.v
-18.40%	10.3	8.4	-1.9	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/elpi/cpp_spec.v
-18.38%	9.9	8.1	-1.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/brick_eval/bad/goal_doctor.v
-18.36%	14.3	11.7	-2.6	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/model/reset_flag.v
-18.33%	29.4	24.0	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/data_class/dataclass_hpp_spec.v
-18.31%	10.7	8.7	-2.0	fmdeps/auto/coq-bluerock-auto-core/theories/internal/instr/FwdSplit.v
-18.25%	8.3	6.8	-1.5	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/model/phase.v
-18.19%	81.8	66.9	-14.9	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/ctor.v
-18.16%	9.9	8.1	-1.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/synth_names/test.v
-18.15%	9.1	7.4	-1.6	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/hints/decidable.v
-18.09%	102.9	84.3	-18.6	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/recall.v
-18.09%	9.4	7.7	-1.7	fmdeps/auto/coq-bluerock-auto-core/theories/internal/syntactic_bi/forced/simplify_exT.v
-18.05%	8.3	6.8	-1.5	bluerock/bhv/zeta/lib/log/include/log/aarch64_log_hpp.v
-18.03%	30.1	24.7	-5.4	bluerock/bhv/zeta/lib/lang/proof/page_hpp_proof.v
-18.02%	46.0	37.7	-8.3	bluerock/NOVA/build-proof/proof/sc_hpp_spec/triples.v
-18.01%	9.9	8.1	-1.8	fmdeps/auto/coq-bluerock-auto-core/theories/internal/instr/Observe.v
-18.00%	8.4	6.9	-1.5	bluerock/bhv/zeta/lib/alloc/include/alloc/aarch64_bin_info_hpp.v
-17.98%	15.7	12.9	-2.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/derive/test.v
-17.97%	36.9	30.3	-6.6	bluerock/bhv/zeta/lib/bhv/proof/bhv_hpp_spec.v
-17.92%	27.5	22.5	-4.9	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_util.v
-17.92%	22.4	18.4	-4.0	fmdeps/auto/coq-bluerock-auto-cpp/tests/llist/list_hpp_spec.v
-17.89%	47.0	38.6	-8.4	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/descriptor/misc.v
-17.89%	41.0	33.6	-7.3	bluerock/NOVA/build-proof/proof/ec_hpp_spec/active_triples.v
-17.89%	8.2	6.7	-1.5	fmdeps/auto/coq-bluerock-auto-cpp/theories/base_logic/lib/monpred_invariants.v
-17.87%	30.1	24.7	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0052_cpp_f0_proof.v
-17.87%	29.9	24.5	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/upstream/cpp/bi_choice.v
-17.83%	8.4	6.9	-1.5	bluerock/bhv/apps/vmm/vml/config/vmm_debug/include/aarch64_vm_abort_hpp.v
-17.79%	30.1	24.7	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0059_cpp_f3_proof.v
-17.76%	7.9	6.5	-1.4	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/type.v
-17.73%	47.2	38.8	-8.4	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/available/misc.v
-17.73%	8.5	7.0	-1.5	bluerock/bhv/apps/vswitch/lib/util/include/util/aarch64_trace_hpp.v
-17.72%	47.2	38.8	-8.4	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/used/misc.v
-17.71%	43.1	35.5	-7.6	bluerock/bhv/apps/vswitch/proof/model/vswitch/nodirect.v
-17.68%	8.5	7.0	-1.5	bluerock/bhv/zeta/lib/uuid/include/uuid/aarch64_uuid_hpp.v
-17.63%	8.5	7.0	-1.5	bluerock/bhv/zeta/lib/cxx/include/aarch64_tagged_ptr_hpp.v
-17.61%	31.5	25.9	-5.5	bluerock/NOVA/build-proof/proof/spinlock_hpp_proof/lock_guard.v
-17.61%	57.1	47.0	-10.0	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctrl_feature_reset.v
-17.60%	34.4	28.4	-6.1	bluerock/NOVA/build-proof/proof/iface/model.v
-17.58%	32.9	27.1	-5.8	bluerock/bhv/zeta/apps/msc/proof/nova_caprange_hpp_proof.v
-17.55%	30.6	25.2	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0096_cpp_f0_proof.v
-17.53%	105.5	87.0	-18.5	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/wp_vcpu/hints.v
-17.47%	13.2	10.9	-2.3	bluerock/NOVA/build-proof/proof/cpp/const_ptr.v
-17.47%	48.7	40.2	-8.5	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/spec.v
-17.47%	35.5	29.3	-6.2	bluerock/NOVA/build-proof/proof/timeout_cpp_proof/check.v
-17.47%	9.5	7.9	-1.7	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/sizeof.v
-17.47%	13.9	11.5	-2.4	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/tactics.v
-17.45%	7.9	6.5	-1.4	bluerock/bhv/apps/vmm/lib/board/include/model/board_common_hpp_names.v
-17.43%	30.8	25.5	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0068_cpp_f0_proof.v
-17.40%	32.5	26.9	-5.7	bluerock/NOVA/build-proof/proof/spinlock_hpp_proof/lc_lock_guard.v
-17.38%	37.5	30.9	-6.5	bluerock/NOVA/build-proof/proof/regs_hpp_spec/cpu_regs.v
-17.38%	58.0	47.9	-10.1	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_cpp_proof/end_roundup.v
-17.35%	50.9	42.1	-8.8	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/bulk_copier_default.v
-17.30%	8.7	7.2	-1.5	bluerock/bhv/zeta/lib/nova/include/aarch64/nova/arch_utcb_hpp.v
-17.27%	7.0	5.8	-1.2	fmdeps/auto/coq-bluerock-auto-core/theories/internal/syntactic_bi/forced/forceT.v
-17.26%	10.8	8.9	-1.9	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/ptrs/nullptr.v
-17.25%	10.9	9.0	-1.9	fmdeps/auto/coq-bluerock-auto-core/examples/classes/playground.v
-17.21%	13.1	10.8	-2.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/base_logic/lib/bound.v
-17.20%	44.9	37.2	-7.7	bluerock/NOVA/build-proof/proof/sm_cpp_proof/private_prelude.v
-17.19%	10.4	8.6	-1.8	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/templates/hints/log_subst.v
-17.16%	64.8	53.7	-11.1	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/guest_as_hpp_proof.v
-17.14%	13.1	10.9	-2.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/cpp/spec/test.v
-17.13%	30.6	25.4	-5.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_timer_hpp_spec.v
-17.08%	22.8	18.9	-3.9	bluerock/bhv/apps/vswitch/proof/typeclasses.v
-17.05%	35.5	29.5	-6.1	bluerock/bhv/apps/umx/proof/umx_hpp_spec.v
-17.03%	83.2	69.0	-14.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/copy_frame.v
-17.00%	7.9	6.5	-1.3	fmdeps/auto/coq-bluerock-auto-core/tests/test_orient.v
-16.98%	36.5	30.3	-6.2	bluerock/bhv/apps/umx/proof/umx_hints.v
-16.97%	10.0	8.3	-1.7	fmdeps/auto/coq-bluerock-auto-cpp/tests/tactics4/learn.v
-16.93%	34.8	28.9	-5.9	bluerock/bhv/apps/vmm/vml/devices/timer/proof/timer_hpp_spec.v
-16.89%	31.9	26.5	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0059_cpp_f0_proof.v
-16.85%	8.9	7.4	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_amlogic_sm1_hpp.v
-16.85%	8.9	7.4	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_allwinner_a64_hpp.v
-16.85%	8.9	7.4	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_nxp_imx8m_hpp.v
-16.84%	8.9	7.4	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_nvidia_tegrax1_hpp.v
-16.84%	8.9	7.4	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_qemu_hpp.v
-16.84%	8.9	7.4	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_rockchip_rk3399_hpp.v
-16.83%	8.9	7.4	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_broadcom_bcm2711_hpp.v
-16.83%	8.9	7.4	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_amlogic_g12b_hpp.v
-16.83%	8.9	7.4	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_ti_am62x_hpp.v
-16.82%	8.9	7.4	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_hisilicon_hi3660_hpp.v
-16.82%	8.9	7.4	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_renesas_rcar3_hpp.v
-16.79%	46.5	38.7	-7.8	bluerock/bhv/lib/vrl/proof/vrl/port_list_hints.v
-16.79%	8.9	7.4	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_ti_j721e_hpp.v
-16.76%	31.9	26.6	-5.3	bluerock/bhv/zeta/lib/cxx/proof/tagged_ptr_hpp_spec.v
-16.75%	84.8	70.6	-14.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/extract_frame_header.v
-16.68%	8.9	7.5	-1.5	bluerock/bhv/apps/vmm/vml/devices/msr/include/msr/aarch64_msr_access_hpp.v
-16.68%	32.4	27.0	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/virtual/mdc_noimpl/BD.v
-16.67%	30.2	25.1	-5.0	fmdeps/auto/coq-bluerock-auto-cpp/tests/arch_indep/simple_base_hpp_spec.v
-16.67%	31.1	25.9	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/brick_eval/bad/overflow.v
-16.65%	11.7	9.8	-1.9	fmdeps/auto/coq-bluerock-auto-core/theories/internal/instr/Later.v
-16.65%	35.2	29.4	-5.9	bluerock/bhv/lib/drivers/serial/pl011/proof/pl011_hpp_spec.v
-16.65%	9.0	7.5	-1.5	bluerock/NOVA/build-proof/proof/aarch64/mtd_hpp.v
-16.63%	54.5	45.4	-9.1	bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_cpp_proof/hints.v
-16.61%	40.5	33.7	-6.7	bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/inversion.v
-16.58%	9.0	7.5	-1.5	bluerock/bhv/lib/vrl/include/vrl/aarch64_shared_hpp_names.v
-16.54%	9.1	7.6	-1.5	bluerock/NOVA/build-proof/proof/aarch64/kmem_hpp.v
-16.53%	32.3	26.9	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/const/backwards_cpp_spec.v
-16.52%	11.0	9.2	-1.8	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/default_spec/logical.v
-16.46%	16.2	13.5	-2.7	fmdeps/auto/coq-bluerock-auto-cpp/tests/llist_cpp/forward_list_hpp_spec.v
-16.45%	31.9	26.6	-5.2	bluerock/bhv/lib/vrl/proof/vrl/packet_hpp_spec.v
-16.42%	41.1	34.3	-6.7	bluerock/NOVA/build-proof/proof/ec_hpp_spec/current_pred.v
-16.30%	16.0	13.4	-2.6	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/tactics.v
-16.28%	115.8	97.0	-18.9	bluerock/bhv/apps/vmm/proof/main_cpp_proof/get_fdt_from_uuid.v
-16.28%	10.0	8.4	-1.6	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/interp.v
-16.25%	45.6	38.2	-7.4	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/ghost.v
-16.24%	14.4	12.1	-2.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/auto_frac/tmp_classy_reify.v
-16.21%	11.6	9.8	-1.9	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/perm_func.v
-16.21%	11.6	9.8	-1.9	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/perm.v
-16.21%	12.1	10.1	-2.0	fmdeps/auto/coq-bluerock-auto-core/theories/internal/instr/Learn.v
-16.21%	37.0	31.0	-6.0	bluerock/NOVA/build-proof/proof/refcnt_hpp_proof.v
-16.20%	40.1	33.6	-6.5	bluerock/NOVA/build-proof/proof/pd_hpp_spec/abs_pred.v
-16.20%	18.8	15.8	-3.1	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/plogic.v
-16.18%	33.5	28.1	-5.4	fmdeps/auto-docs/content/demo/aggregate01/Point_hpp_proof.v
-16.14%	9.3	7.8	-1.5	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/fancy_module_tests.v
-16.13%	62.7	52.6	-10.1	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/roundup_proofs_combined.v
-16.13%	24.6	20.6	-4.0	fmdeps/auto/coq-bluerock-auto-cpp/tests/const/derive.v
-16.10%	9.3	7.8	-1.5	bluerock/bhv/zeta/lib/zeta/include/bluerock/zeta/aarch64_ec_hpp_names.v
-16.10%	9.3	7.8	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_xilinx_zynq_cg_hpp.v
-16.09%	19.3	16.2	-3.1	bluerock/bhv/lib/vconnect/proof/vconnect/common_hpp_spec.v
-16.09%	9.3	7.8	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_xilinx_zynq_zcu102_hpp.v
-16.08%	9.3	7.8	-1.5	bluerock/NOVA/build-proof/proof/aarch64/timer_hpp.v
-16.08%	9.3	7.8	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_xilinx_zynq_u96_hpp.v
-16.03%	9.3	7.8	-1.5	bluerock/NOVA/build-proof/proof/aarch64/mtd_arch_hpp.v
-16.01%	9.3	7.8	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_nvidia_tegrax2_hpp.v
-16.01%	41.2	34.6	-6.6	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/captable.v
-16.00%	84.7	71.1	-13.6	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_hpp_spec/space_view_invs.v
-15.99%	11.9	10.0	-1.9	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/default_spec/ltac2.v
-15.99%	9.3	7.9	-1.5	bluerock/bhv/apps/vmm/lib/bluerock/include/bluerock/platform/aarch64_semaphore_hpp_names.v
-15.97%	18.0	15.1	-2.9	fmdeps/auto/coq-bluerock-auto-cpp/tests/arith/cpp_tests.v
-15.96%	14.9	12.5	-2.4	bluerock/NOVA/build-proof/proof/basis/word.v
-15.96%	9.4	7.9	-1.5	bluerock/bhv/apps/vmm/lib/bluerock/include/bluerock/platform/aarch64_mutex_hpp_names.v
-15.94%	89.7	75.4	-14.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/vrl_hints.v
-15.93%	9.4	7.9	-1.5	bluerock/bhv/apps/vmm/lib/bluerock/include/bluerock/platform/aarch64_memory_hpp_names.v
-15.90%	9.4	7.9	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_nvidia_xavier_hpp.v
-15.88%	10.8	9.1	-1.7	fmdeps/auto/coq-bluerock-auto-core/theories/internal/syntactic_bi/forced/simplify_wandT.v
-15.87%	9.9	8.3	-1.6	bluerock/NOVA/build-proof/proof/aarch64/sdid_hpp.v
-15.87%	9.9	8.3	-1.6	bluerock/NOVA/build-proof/proof/aarch64/vmid_hpp.v
-15.81%	9.5	8.0	-1.5	bluerock/bhv/apps/umx/include/aarch64_admin_hpp_names.v
-15.81%	9.4	8.0	-1.5	bluerock/bhv/apps/vmm/lib/bluerock/include/bluerock/platform/aarch64_rwlock_hpp_names.v
-15.81%	9.5	8.0	-1.5	bluerock/bhv/apps/umx/src/aarch64_admin_cpp_names.v
-15.81%	9.5	8.0	-1.5	bluerock/bhv/apps/umx/include/aarch64_umx_hpp_names.v
-15.78%	9.4	7.9	-1.5	bluerock/NOVA/build-proof/proof/aarch64/wait_hpp.v
-15.73%	10.0	8.4	-1.6	bluerock/NOVA/build-proof/proof/aarch64/hazard_hpp.v
-15.72%	9.4	7.9	-1.5	bluerock/NOVA/build-proof/proof/aarch64/console_hpp.v
-15.72%	34.1	28.7	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0096_cpp_f1_proof.v
-15.71%	9.4	8.0	-1.5	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_hpp.v
-15.71%	9.4	7.9	-1.5	bluerock/bhv/zeta/lib/nova/include/aarch64/nova/arch_types_hpp.v
-15.70%	41.7	35.1	-6.5	bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/triples.v
-15.70%	9.8	8.3	-1.5	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/alignment.v
-15.66%	34.2	28.9	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/io/io_c_proof.v
-15.65%	45.2	38.2	-7.1	bluerock/NOVA/build-proof/proof/ec_hpp_spec/global_pred.v
-15.65%	38.2	32.2	-6.0	bluerock/bhv/zeta/lib/cxx/proof/unique_ptr_cpp_proof.v
-15.61%	12.4	10.5	-1.9	fmdeps/auto/coq-bluerock-auto-core/theories/internal/syntactic_bi/syntactic_bi_def.v
-15.60%	21.4	18.1	-3.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/upstream/cpp/misc_tactics.v
-15.59%	9.6	8.1	-1.5	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/include/model/aarch64_cpu_hpp_names.v
-15.56%	68.0	57.4	-10.6	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_spec.v
-15.56%	21.5	18.2	-3.3	bluerock/bhv/apps/vmm/proof/tactics.v
-15.56%	94.7	79.9	-14.7	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/base_startup_handler.v
-15.54%	49.7	42.0	-7.7	bluerock/bhv/lib/vrl/proof/vrl/packet_hpp_proof.v
-15.53%	9.7	8.2	-1.5	bluerock/bhv/zeta/lib/porter/include/porter/aarch64_server_hpp_names.v
-15.52%	16.6	14.0	-2.6	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/ptrs/valid_tests.v
-15.49%	11.0	9.3	-1.7	fmdeps/auto/coq-bluerock-auto-cpp/theories/base_logic/lib/reusable.v
-15.49%	39.1	33.0	-6.1	bluerock/NOVA/build-proof/proof/ec_hpp_spec/continuation.v
-15.48%	9.7	8.2	-1.5	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/src/aarch64_vcpu_roundup_cpp_names.v
-15.47%	70.4	59.5	-10.9	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/roundup_all.v
-15.47%	9.6	8.1	-1.5	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_xsdt_hpp.v
-15.45%	48.8	41.3	-7.5	bluerock/NOVA/build-proof/proof/iface/predicates/sm.v
-15.44%	9.7	8.2	-1.5	bluerock/bhv/lib/vrl/src/aarch64_dataplane_cpp_names.v
-15.42%	34.7	29.4	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/aggregate_arrays/proof.v
-15.40%	34.9	29.5	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0099_cpp_f0_proof.v
-15.40%	11.1	9.4	-1.7	fmdeps/auto/coq-bluerock-auto-core/theories/internal/syntactic_bi/forced.v
-15.36%	9.8	8.3	-1.5	bluerock/bhv/apps/vmm/vml/devices/vbus/include/vbus/aarch64_vbus_hpp_names.v
-15.36%	34.1	28.9	-5.2	bluerock/bhv/apps/umx/proof/main_hints.v
-15.36%	10.1	8.6	-1.6	bluerock/bhv/zeta/lib/lang/include/aarch64_atomic_hpp.v
-15.34%	18.7	15.8	-2.9	fmdeps/auto/coq-bluerock-auto-core/theories/internal/tactic/Dnet.v
-15.33%	43.6	36.9	-6.7	bluerock/NOVA/build-proof/proof/timeout_hpp_spec/abs_pred.v
-15.33%	9.7	8.2	-1.5	bluerock/NOVA/build-proof/proof/aarch64/board_qualcomm_sdm670_hpp.v
-15.33%	39.9	33.8	-6.1	bluerock/NOVA/build-proof/proof/syscall_hpp_spec.v
-15.32%	10.2	8.6	-1.6	bluerock/NOVA/build-proof/proof/aarch64/smc_psci_hpp.v
-15.31%	9.9	8.4	-1.5	bluerock/NOVA/build-proof/proof/basis/types.v
-15.30%	9.8	8.3	-1.5	bluerock/bhv/apps/vmm/vml/devices/vuart/include/vuart/aarch64_vuart_hpp_names.v
-15.30%	15.8	13.4	-2.4	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/join.v
-15.25%	36.6	31.0	-5.6	bluerock/NOVA/build-proof/proof/kmem_hpp_spec.v
-15.23%	10.2	8.6	-1.5	bluerock/bhv/zeta/lib/intrusive/include/intrusive/aarch64_map_hpp.v
-15.23%	38.0	32.2	-5.8	bluerock/NOVA/build-proof/proof/kobject_hpp_proof.v
-15.22%	38.3	32.5	-5.8	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/countLN.v
-15.21%	9.7	8.2	-1.5	bluerock/NOVA/build-proof/proof/aarch64/dev_hpp.v
-15.20%	9.7	8.2	-1.5	bluerock/NOVA/build-proof/proof/aarch64/dev_cpp.v
-15.17%	9.9	8.4	-1.5	bluerock/bhv/apps/vmm/vml/devices/irq_controller/include/model/aarch64_irq_controller_hpp_names.v
-15.17%	9.9	8.4	-1.5	bluerock/bhv/apps/vmm/vml/devices/simple_as/include/model/aarch64_simple_as_hpp_names.v
-15.16%	8.9	7.5	-1.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/base_logic/lib/scontender.v
-15.15%	9.9	8.4	-1.5	bluerock/bhv/apps/vswitch/lib/acl/include/acl/aarch64_acl_hpp_names.v
-15.13%	7.3	6.2	-1.1	fmdeps/auto/coq-bluerock-auto-core/theories/internal/instr/Persist.v
-15.12%	9.9	8.4	-1.5	bluerock/bhv/apps/vmm/lib/dynamic_as/include/model/aarch64_guest_as_hpp_names.v
-15.11%	64.3	54.6	-9.7	bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_cpp_proof.v
-15.10%	9.9	8.4	-1.5	bluerock/bhv/apps/vmm/vml/devices/vpl011/include/pl011/aarch64_pl011_hpp_names.v
-15.10%	10.3	8.7	-1.6	bluerock/bhv/zeta/lib/concurrent/include/concurrent/aarch64_ticket_lock_hpp.v
-15.09%	132.7	112.6	-20.0	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/startup.v
-15.09%	37.2	31.6	-5.6	bluerock/bhv/zeta/lib/bson/proof/bson.v
-15.07%	84.3	71.6	-12.7	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/private_hints3.v
-15.07%	9.9	8.4	-1.5	bluerock/bhv/apps/vmm/vml/devices/timer/include/model/aarch64_timer_hpp_names.v
-15.07%	94.7	80.5	-14.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/pkt.v
-15.06%	10.0	8.5	-1.5	bluerock/bhv/apps/vmm/vml/devices/timer/include/model/aarch64_aa64_timer_hpp_names.v
-15.04%	73.2	62.2	-11.0	bluerock/bhv/apps/vmm/vml/devices/simple_as/proof/simple_as_hpp_proof.v
-15.04%	10.3	8.8	-1.6	bluerock/NOVA/build-proof/proof/aarch64/hip_hpp.v
-15.01%	15.2	12.9	-2.3	bluerock/NOVA/build-proof/proof/cpp/const_global.v
-15.01%	10.0	8.5	-1.5	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/include/vcpu/aarch64_vcpu_timer_hpp_names.v
-15.00%	10.0	8.5	-1.5	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/include/aarch64_portal_hpp_names.v
-14.99%	67.1	57.0	-10.1	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/hints.v
-14.96%	10.0	8.5	-1.5	bluerock/bhv/apps/vmm/lib/outpost_dummy/include/outpost/aarch64_outpost_hpp_names.v
-14.96%	10.0	8.5	-1.5	bluerock/bhv/apps/vmm/lib/vmi_interface/include/vmi_interface/aarch64_vmi_interface_hpp_names.v
-14.95%	43.0	36.6	-6.4	bluerock/bhv/zeta/lib/nova/proof/types_hpp_proof.v
-14.94%	47.6	40.5	-7.1	bluerock/bhv/apps/vmm/vml/devices/msr/proof/msr_id_hpp_proof.v
-14.94%	50.6	43.1	-7.6	bluerock/NOVA/build-proof/proof/sc_cpp_proof/proof.v
-14.94%	10.4	8.8	-1.5	bluerock/bhv/zeta/lib/concurrent/src/aarch64_ticket_lock_cpp.v
-14.94%	9.8	8.4	-1.5	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_xsdt_cpp.v
-14.91%	10.1	8.6	-1.5	bluerock/bhv/apps/vmm/vml/devices/vpl011/src/aarch64_pl011_cpp_names.v
-14.91%	41.1	35.0	-6.1	bluerock/bhv/zeta/lib/msc/proof/bhv_defs.v
-14.91%	10.1	8.6	-1.5	bluerock/bhv/apps/vmm/vml/devices/msr/include/msr/aarch64_msr_base_hpp_names.v
-14.89%	36.1	30.7	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0098_cpp_f0_proof.v
-14.88%	32.4	27.6	-4.8	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_spec.v
-14.87%	10.1	8.6	-1.5	bluerock/bhv/apps/vmm/vml/devices/msr/src/aarch64_msr_base_cpp_names.v
-14.87%	10.4	8.8	-1.5	bluerock/bhv/zeta/lib/concurrent/include/concurrent/aarch64_lossy_queue_hpp.v
-14.85%	10.1	8.6	-1.5	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/src/aarch64_cpu_model_cpp_names.v
-14.85%	9.9	8.4	-1.5	bluerock/bhv/zeta/lib/nova/include/nova/aarch64_utcb_hpp.v
-14.84%	10.5	8.9	-1.6	bluerock/NOVA/build-proof/proof/aarch64/bitmap_hpp.v
-14.78%	117.1	99.8	-17.3	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_hpp_spec.v
-14.77%	15.2	13.0	-2.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/base_logic/tls_modalities.v
-14.76%	10.0	8.5	-1.5	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_tpm2_hpp.v
-14.70%	9.6	8.2	-1.4	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/elpi/synth.v
-14.66%	36.7	31.3	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0036_cpp_f3_proof.v
-14.64%	10.3	8.8	-1.5	bluerock/bhv/apps/vmm/lib/bluerock/include/bluerock/aarch64_fdt_hpp_names.v
-14.63%	86.7	74.0	-12.7	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/spec.v
-14.63%	51.6	44.1	-7.5	bluerock/NOVA/build-proof/proof/iface/predicates/pt.v
-14.62%	10.0	8.5	-1.5	bluerock/NOVA/build-proof/proof/aarch64/console_cpp.v
-14.61%	67.6	57.7	-9.9	bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/defs.v
-14.59%	10.6	9.0	-1.5	bluerock/bhv/apps/vswitch/lib/acl/include/acl/aarch64_matcher_hpp.v
-14.57%	11.6	9.9	-1.7	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/modules.v
-14.56%	18.9	16.1	-2.7	bluerock/bhv/apps/vmm/vml/arch/arch_api/proof/barrier_common_hpp_spec.v
-14.56%	51.3	43.8	-7.5	bluerock/bhv/apps/vmm/proof/bm_dram.v
-14.55%	19.3	16.5	-2.8	fmdeps/auto/coq-bluerock-auto-cpp/theories/cpp/spec/specify.v
-14.55%	36.9	31.5	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/default_spec/test_cpp_proof.v
-14.53%	14.2	12.1	-2.1	fmdeps/auto-docs/content/docs/functions/specification.v
-14.52%	10.4	8.9	-1.5	bluerock/bhv/zeta/apps/msc/include/msc/nova/aarch64_pd_hpp_names.v
-14.52%	11.7	10.0	-1.7	fmdeps/auto/coq-bluerock-auto-core/theories/internal/syntactic_bi/forced/apply.v
-14.48%	9.4	8.0	-1.4	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/deps.v
-14.48%	10.1	8.7	-1.5	bluerock/NOVA/build-proof/proof/aarch64/uefi_hpp.v
-14.47%	10.6	9.0	-1.5	bluerock/bhv/lib/vrl/include/vrl/aarch64_stats_hpp.v
-14.47%	10.5	9.0	-1.5	bluerock/bhv/zeta/lib/concurrent/include/concurrent/aarch64_lossy_queue2_hpp.v
-14.45%	7.0	6.0	-1.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/lemmas/util.v
-14.41%	10.8	9.3	-1.6	bluerock/NOVA/build-proof/proof/aarch64/hash_hpp.v
-14.40%	7.6	6.5	-1.1	fmdeps/auto/coq-bluerock-auto-core/theories/internal/instr/PersistBoxed.v
-14.40%	10.4	8.9	-1.5	bluerock/bhv/lib/vconnect/include/vconnect/aarch64_guest_as_hpp_names.v
-14.36%	7.0	6.0	-1.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/case_split.v
-14.36%	10.5	9.0	-1.5	bluerock/bhv/apps/vmm/vml/devices/gic/include/model/aarch64_gic_hpp_names.v
-14.36%	37.2	31.9	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/var_args/main_cpp_spec.v
-14.36%	10.7	9.2	-1.5	bluerock/bhv/zeta/lib/lang/include/aarch64_endian_hpp.v
-14.33%	10.7	9.1	-1.5	bluerock/bhv/zeta/lib/cxx/include/aarch64_range_hpp.v
-14.33%	100.2	85.8	-14.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/send.v
-14.28%	11.2	9.6	-1.6	fmdeps/auto/coq-bluerock-auto-core/theories/hints/hint_adapters.v
-14.24%	10.6	9.1	-1.5	bluerock/bhv/apps/sm/smclient/include/sm/aarch64_client_hpp_names.v
-14.24%	10.2	8.8	-1.5	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_gtdt_hpp.v
-14.22%	10.8	9.3	-1.5	bluerock/bhv/apps/vswitch/lib/acl/include/acl/aarch64_flow_entry_hpp.v
-14.20%	38.0	32.6	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/data_class/class_8_cpp_proof.v
-14.19%	10.3	8.8	-1.5	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_rsdp_hpp.v
-14.19%	10.6	9.1	-1.5	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/include/aarch64/vcpu/msr_bus_hpp_names.v
-14.19%	10.6	9.1	-1.5	bluerock/bhv/apps/vmm/vml/devices/msr/include/aarch64/msr/msr_hpp_names.v
-14.18%	10.3	8.8	-1.5	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_facs_hpp.v
-14.17%	16.6	14.2	-2.3	bluerock/bhv/apps/vswitch/lib/util/proof/trace_hpp_spec.v
-14.14%	44.3	38.1	-6.3	bluerock/bhv/lib/ddk/proof/iris_device_wp.v
-14.14%	10.3	8.8	-1.5	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_mcfg_hpp.v
-14.13%	10.8	9.3	-1.5	bluerock/bhv/apps/vswitch/lib/util/include/util/aarch64_profiler_hpp.v
-14.09%	12.4	10.7	-1.7	fmdeps/auto/coq-bluerock-auto-cpp/theories/base_logic/lib/ghost_map.v
-14.08%	57.5	49.4	-8.1	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/hints.v
-14.08%	11.1	9.5	-1.6	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/new/inc_new_cpp.v
-14.07%	10.9	9.4	-1.5	bluerock/NOVA/build-proof/proof/aarch64/rcu_hpp.v
-14.07%	58.3	50.1	-8.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/requesters.v
-14.05%	7.9	6.8	-1.1	fmdeps/auto/coq-bluerock-auto-core/theories/internal/instr/ID.v
-14.03%	11.1	9.6	-1.6	bluerock/NOVA/build-proof/proof/aarch64/integrity_hpp.v
-14.02%	77.5	66.6	-10.9	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/resume_all.v
-14.01%	18.9	16.2	-2.6	bluerock/bhv/apps/vmm/proof/prelude/bhv.v
-14.01%	10.1	8.7	-1.4	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/delayed_case_tactics.v
-14.00%	45.8	39.4	-6.4	bluerock/bhv/zeta/lib/log/proof/log_hpp_spec.v
-13.97%	13.3	11.4	-1.9	fmdeps/auto/coq-bluerock-auto-cpp/theories/lib/ghost.v
-13.96%	54.3	46.7	-7.6	bluerock/bhv/apps/umx/proof/main_cpp_proof/zeta_main.v
-13.93%	10.8	9.3	-1.5	bluerock/bhv/apps/vmm/lib/dynamic_as/include/model/aarch64_space_view_hpp_names.v
-13.92%	38.3	33.0	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/cpp_proof/test_cpp_proof.v
-13.92%	7.8	6.7	-1.1	fmdeps/auto/coq-bluerock-auto-core/theories/internal/instr/cmd.v
-13.90%	9.2	7.9	-1.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/persistent.v
-13.90%	11.0	9.4	-1.5	bluerock/bhv/apps/vmm/vml/devices/msr/include/aarch64/msr/msr_info_hpp.v
-13.89%	10.4	9.0	-1.4	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_dbg2_hpp.v
-13.88%	10.8	9.3	-1.5	bluerock/bhv/apps/umx/src/aarch64_main_cpp_names.v
-13.85%	10.8	9.3	-1.5	bluerock/bhv/apps/vmm/lib/dynamic_as/include/model/aarch64_as_layout_hpp_names.v
-13.83%	38.4	33.1	-5.3	fmdeps/auto-docs/content/docs/functions/verification.v
-13.81%	38.5	33.2	-5.3	bluerock/NOVA/build-proof/proof/basis/na_invariants.v
-13.81%	23.3	20.1	-3.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/ptrs/valid.v
-13.79%	96.3	83.0	-13.3	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_hpp_spec.v
-13.76%	41.8	36.1	-5.8	bluerock/bhv/lib/vrl/proof/vrl/shared_hpp_spec.v
-13.73%	23.4	20.2	-3.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/unroll_loops.v
-13.70%	138.2	119.3	-18.9	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/hints.v
-13.69%	11.0	9.5	-1.5	bluerock/bhv/zeta/lib/concurrent/src/aarch64_lossy_queue2_cpp.v
-13.65%	39.5	34.1	-5.4	fmdeps/auto-docs/content/docs/control_flow/if.v
-13.65%	103.6	89.4	-14.1	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/route.v
-13.64%	46.2	39.9	-6.3	bluerock/bhv/zeta/lib/cxx/proof/sys/lock_guard_hpp_proof.v
-13.61%	40.3	34.8	-5.5	bluerock/NOVA/build-proof/proof/cpu_hpp_spec/count.v
-13.61%	11.1	9.6	-1.5	bluerock/bhv/zeta/lib/concurrent/include/concurrent/aarch64_client_lock_hpp.v
-13.59%	39.3	34.0	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/control_flow/main_cpp_spec.v
-13.57%	10.6	9.2	-1.4	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_spcr_hpp.v
-13.55%	10.7	9.2	-1.4	bluerock/NOVA/build-proof/proof/aarch64/uefi_cpp.v
-13.52%	19.0	16.4	-2.6	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/builtins.v
-13.52%	39.9	34.5	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/cpp_spec/test.v
-13.51%	11.2	9.7	-1.5	bluerock/bhv/apps/vswitch/lib/protocol/include/protocol/aarch64_udp_hpp.v
-13.50%	53.6	46.4	-7.2	bluerock/bhv/apps/umx/proof/main_cpp_proof/setup_output_loop_thread.v
-13.49%	11.2	9.7	-1.5	bluerock/bhv/apps/vswitch/lib/protocol/include/protocol/aarch64_tcp_hpp.v
-13.47%	11.5	9.9	-1.5	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_srat_hpp.v
-13.45%	60.6	52.4	-8.2	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxclient/io.v
-13.39%	40.2	34.8	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0094_cpp_f0_proof.v
-13.39%	89.2	77.3	-11.9	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/setup.v
-13.39%	10.0	8.6	-1.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/elpi/dataclass.v
-13.35%	11.5	10.0	-1.5	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_iort_hpp.v
-13.32%	7.9	6.9	-1.1	bluerock/NOVA/build-proof/proof/basis/duplicable.v
-13.28%	96.0	83.2	-12.7	bluerock/bhv/apps/vswitch/lib/port/proof/port/spec.v
-13.26%	45.6	39.6	-6.1	bluerock/bhv/zeta/lib/lang/proof/memory_barrier.v
-13.24%	23.0	19.9	-3.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/elpi/cpp_enum.v
-13.16%	18.2	15.8	-2.4	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/identity.v
-13.14%	34.9	30.3	-4.6	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_split_sz.v
-13.14%	10.6	9.2	-1.4	bluerock/NOVA/build-proof/proof/cpp/when.v
-13.10%	50.0	43.5	-6.6	bluerock/NOVA/build-proof/proof/sm_hpp_spec/abs_pred.v
-13.08%	37.0	32.1	-4.8	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof.v
-13.06%	11.5	10.0	-1.5	bluerock/bhv/apps/vswitch/lib/protocol/include/protocol/aarch64_virtio_net_hpp.v
-13.02%	37.1	32.3	-4.8	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_intersect.v
-12.98%	52.7	45.9	-6.8	bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_cpp_proof/lookup.v
-12.97%	11.6	10.1	-1.5	bluerock/bhv/apps/vmm/lib/dynamic_as/include/model/aarch64_guest_chunk_repo_hpp_names.v
-12.97%	41.2	35.8	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/big_sep/anyR_proof.v
-12.96%	11.6	10.1	-1.5	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/include/vcpu/aarch64_vcpu_base_hpp_names.v
-12.93%	11.7	10.2	-1.5	bluerock/bhv/lib/pm/pm_client_bhv/include/aarch64_dev_client_hpp_names.v
-12.90%	11.5	10.0	-1.5	bluerock/bhv/apps/vmm/vml/devices/msr/include/aarch64/msr/esr_hpp.v
-12.90%	11.7	10.2	-1.5	bluerock/bhv/lib/vconnect/include/vconnect/aarch64_async_control_hpp_names.v
-12.88%	41.4	36.1	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/specify/copymove/test_hpp_proof.v
-12.87%	52.0	45.3	-6.7	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ipc_call.v
-12.85%	9.6	8.4	-1.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/sep_core.v
-12.85%	15.2	13.2	-1.9	fmdeps/auto/coq-bluerock-auto-core/theories/internal/instr/Fwd.v
-12.84%	11.7	10.2	-1.5	bluerock/bhv/lib/ddk/include/ddk/aarch64_mmio_bhv_hpp_names.v
-12.83%	51.8	45.2	-6.6	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/hints.v
-12.81%	11.6	10.1	-1.5	bluerock/bhv/zeta/lib/alloc/include/alloc/aarch64_core_hpp.v
-12.77%	55.0	48.0	-7.0	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxshared/client_io_done.v
-12.77%	41.7	36.4	-5.3	fmdeps/auto-docs/content/demo/data_class/main_proof.v
-12.75%	11.8	10.3	-1.5	bluerock/bhv/lib/drivers/serial/pl011/include/pl011/aarch64_pl011_hpp_names.v
-12.71%	42.6	37.2	-5.4	bluerock/bhv/zeta/lib/lang/proof/new_hpp_hints.v
-12.67%	43.9	38.3	-5.6	fmdeps/auto/coq-bluerock-auto-cpp/tests/inits/main_cpp_spec.v
-12.67%	9.8	8.5	-1.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/templates/pre_c11_swap_client_cpp_proof.v
-12.65%	18.6	16.3	-2.4	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/virtual.v
-12.65%	65.5	57.2	-8.3	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/used/setters.v
-12.63%	47.8	41.8	-6.0	bluerock/NOVA/build-proof/proof/space_obj_hpp_spec/abs_pred.v
-12.63%	11.9	10.4	-1.5	bluerock/bhv/apps/vmm/lib/board/include/model/aarch64_board_hpp_names.v
-12.62%	11.8	10.3	-1.5	bluerock/bhv/apps/vswitch/lib/protocol/include/protocol/aarch64_ethernet_hpp.v
-12.62%	161.4	141.0	-20.4	bluerock/bhv/apps/vmm/proof/main_cpp_proof/proof.v
-12.57%	105.0	91.8	-13.2	bluerock/bhv/apps/vswitch/lib/port/proof/port/hints.v
-12.53%	11.9	10.4	-1.5	bluerock/bhv/zeta/lib/cxx/include/aarch64_optional_hpp.v
-12.53%	12.0	10.5	-1.5	bluerock/bhv/apps/vmm/include/aarch64_initial_setup_hpp_names.v
-12.52%	20.6	18.1	-2.6	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/wp_derived.v
-12.49%	11.9	10.4	-1.5	bluerock/NOVA/build-proof/proof/aarch64/utcb_arch_hpp.v
-12.48%	46.3	40.5	-5.8	bluerock/bhv/apps/umx/proof/admin_hints.v
-12.48%	45.2	39.5	-5.6	bluerock/bhv/zeta/lib/bson/proof/bson_hints.v
-12.48%	17.0	14.9	-2.1	fmdeps/auto/coq-bluerock-auto-cpp/theories/base_logic/lib/qftickets.v
-12.47%	15.5	13.6	-1.9	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/prim.v
-12.42%	23.2	20.4	-2.9	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/const.v
-12.42%	19.0	16.7	-2.4	fmdeps/auto/coq-bluerock-auto-core/theories/hints/orient.v
-12.39%	43.9	38.5	-5.4	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/new/hints.v
-12.38%	8.9	7.8	-1.1	fmdeps/auto/coq-bluerock-auto-core/theories/internal/instr/Bwd.v
-12.36%	22.0	19.3	-2.7	fmdeps/auto/coq-bluerock-auto-cpp/tests/arith/bitsize_tests.v
-12.33%	50.6	44.4	-6.2	bluerock/NOVA/build-proof/proof/cpu_hpp_spec/cls.v
-12.28%	9.0	7.9	-1.1	fmdeps/auto/coq-bluerock-auto-core/theories/internal/instr/Forget.v
-12.28%	12.3	10.8	-1.5	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_fadt_hpp.v
-12.27%	12.0	10.5	-1.5	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_hest_cpp.v
-12.26%	12.0	10.5	-1.5	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_hest_hpp.v
-12.21%	17.4	15.2	-2.1	bluerock/bhv/zeta/apps/msc/include/msc/aarch64_hp_hpp_names.v
-12.16%	71.4	62.7	-8.7	bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/esr_hpp_proof.v
-12.10%	44.1	38.8	-5.3	fmdeps/auto-docs/content/demo/inline/inline_hpp_spec.v
-12.08%	16.3	14.3	-2.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/map_solver.v
-12.08%	15.8	13.9	-1.9	fmdeps/auto/coq-bluerock-auto-core/tests/cancelx/fupd.v
-12.08%	27.6	24.3	-3.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/lazy_unfold/test_case.v
-12.07%	12.1	10.6	-1.5	bluerock/bhv/zeta/lib/cxx/include/aarch64_bitset_hpp.v
-12.00%	27.6	24.3	-3.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/specify/templates.v
-12.00%	119.1	104.9	-14.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/drop.v
-11.99%	69.5	61.1	-8.3	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/chain_walking_nop.v
-11.97%	8.5	7.5	-1.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/perm_func_lazy.v
-11.96%	12.6	11.1	-1.5	bluerock/bhv/apps/vswitch/lib/port/include/port/aarch64_port_hpp_names.v
-11.95%	169.2	149.0	-20.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/compute_gpa_fault_addr.v
-11.93%	49.3	43.5	-5.9	bluerock/bhv/zeta/lib/zeta/proof/signal_hpp_proof.v
-11.90%	11.7	10.3	-1.4	fmdeps/auto/coq-bluerock-auto-cpp/theories/base_logic/lib/mono_rel.v
-11.87%	109.2	96.2	-13.0	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/devq/used_event_notify.v
-11.85%	23.0	20.2	-2.7	fmdeps/auto/coq-bluerock-auto-cpp/tests/auto_frac/basic.v
-11.84%	57.1	50.3	-6.8	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxshared/switch_to_client.v
-11.84%	12.8	11.3	-1.5	bluerock/bhv/apps/vswitch/lib/forwarding/include/forwarding/aarch64_forwarding_table_hpp_names.v
-11.83%	43.8	38.7	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/inc/increment_cpp_proof.v
-11.82%	37.3	32.9	-4.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/simple/main_cpp_proof.v
-11.82%	11.8	10.4	-1.4	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/model/mono_rel.v
-11.76%	12.5	11.0	-1.5	bluerock/NOVA/build-proof/proof/aarch64/gicc_hpp.v
-11.74%	21.5	19.0	-2.5	fmdeps/auto/coq-bluerock-auto-cpp/tests/arith/mod_tests.v
-11.73%	60.3	53.2	-7.1	bluerock/bhv/apps/vmm/vml/devices/msr/proof/msr_access_hpp_proof.v
-11.73%	12.8	11.3	-1.5	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/include/aarch64/vcpu/vcpu_hpp_names.v
-11.71%	10.3	9.1	-1.2	bluerock/bhv/apps/vswitch/proof/prelude/common.v
-11.65%	97.3	86.0	-11.3	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/roundup_parallel_proof.v
-11.63%	46.2	40.8	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/specify/challenge/challenge_cpp_proof.v
-11.62%	12.7	11.2	-1.5	bluerock/NOVA/build-proof/proof/aarch64/counter_cpp.v
-11.61%	22.6	20.0	-2.6	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/destroy.v
-11.61%	19.6	17.3	-2.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/array.v
-11.61%	12.7	11.2	-1.5	bluerock/NOVA/build-proof/proof/aarch64/counter_hpp.v
-11.60%	53.8	47.5	-6.2	bluerock/NOVA/build-proof/proof/slab/slab_inst.v
-11.60%	12.9	11.4	-1.5	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/src/aarch64_portal_cpp_names.v
-11.59%	50.1	44.3	-5.8	bluerock/bhv/apps/vswitch/proof/model/virtionet_header.v
-11.58%	11.9	10.5	-1.4	fmdeps/auto/coq-bluerock-auto-cpp/theories/lib/frac.v
-11.56%	40.7	36.0	-4.7	fmdeps/auto/coq-bluerock-auto-cpp/tests/arch_indep/aarch64/simple_arch_hpp_spec.v
-11.54%	57.7	51.0	-6.7	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxclient/helpers.v
-11.52%	50.1	44.3	-5.8	bluerock/bhv/zeta/lib/zeta/proof/ec_hpp_proof.v
-11.50%	100.2	88.7	-11.5	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctor.v
-11.49%	15.5	13.7	-1.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/arith/arith_tests.v
-11.48%	12.7	11.2	-1.5	bluerock/bhv/apps/vswitch/lib/acl/include/acl/aarch64_flow_list_hpp.v
-11.44%	12.7	11.3	-1.5	bluerock/bhv/apps/vswitch/lib/protocol/include/protocol/aarch64_ipv6_hpp.v
-11.44%	18.4	16.3	-2.1	bluerock/bhv/apps/vmm/lib/dynamic_as/src/aarch64_space_view_cpp_names.v
-11.40%	74.2	65.8	-8.5	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/used_entry/setters.v
-11.36%	23.6	20.9	-2.7	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/resolve/mtu_find.v
-11.34%	17.7	15.7	-2.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/base_logic/lib/local_invariants.v
-11.33%	47.1	41.8	-5.3	fmdeps/auto-docs/content/demo/loops/main_cpp_proof.v
-11.33%	13.3	11.8	-1.5	bluerock/bhv/apps/vswitch/lib/vswitch/include/vswitch/aarch64_vswitch_hpp_names.v
-11.33%	18.6	16.5	-2.1	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/src/aarch64/vmexit_cpp_names.v
-11.32%	111.7	99.1	-12.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/spec.v
-11.32%	13.3	11.8	-1.5	bluerock/bhv/apps/vswitch/lib/vswitch_config/include/vswitch_config/aarch64_bson_config_hpp_names.v
-11.31%	63.1	56.0	-7.1	bluerock/NOVA/build-proof/proof/ec_hpp_spec/timeout_pred.v
-11.30%	16.5	14.7	-1.9	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/big_sep/hints.v
-11.30%	97.6	86.5	-11.0	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_cpp_proof/proof.v
-11.28%	19.4	17.2	-2.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/pretty/my_pretty.v
-11.28%	12.8	11.4	-1.4	bluerock/bhv/apps/vswitch/lib/protocol/include/protocol/aarch64_ipv4_hpp.v
-11.28%	17.5	15.5	-2.0	bluerock/NOVA/build-proof/proof/cpp/rep.v
-11.14%	13.6	12.0	-1.5	bluerock/bhv/apps/vswitch/lib/forwarding/include/forwarding/aarch64_forwarding_plane_hpp_names.v
-11.12%	48.0	42.7	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/auto_frac/anyR_proof.v
-11.11%	13.6	12.1	-1.5	bluerock/bhv/apps/vswitch/lib/forwarding/src/aarch64_forwarding_plane_cpp_names.v
-11.10%	48.1	42.8	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/control_flow/if_expr_proof.v
-11.07%	12.9	11.5	-1.4	bluerock/bhv/zeta/lib/intrusive/include/intrusive/aarch64_shared_pointer_hpp.v
-11.02%	48.5	43.2	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/control_flow/array_loops_proof.v
-11.02%	54.6	48.6	-6.0	bluerock/NOVA/build-proof/proof/slab/slab_proof_metadata.v
-10.94%	13.1	11.7	-1.4	bluerock/bhv/zeta/lib/nova/include/nova/aarch64_types_hpp.v
-10.92%	104.9	93.5	-11.5	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctrl_feature_off.v
-10.90%	65.9	58.7	-7.2	bluerock/bhv/apps/umx/proof/main_cpp_proof/copy_bytes_and_flush.v
-10.89%	179.0	159.5	-19.5	bluerock/bhv/apps/vmm/proof/main_cpp_spec.v
-10.86%	28.4	25.3	-3.1	fmdeps/auto/coq-bluerock-auto-cpp/theories/lib/protocol.v
-10.85%	52.2	46.6	-5.7	bluerock/bhv/zeta/lib/zeta/proof/ec_hpp_spec.v
-10.81%	108.8	97.1	-11.8	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/start_cpu.v
-10.80%	28.1	25.1	-3.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/base_logic/lib/refinement_binary.v
-10.80%	50.8	45.3	-5.5	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/algorithms/spec.v
-10.70%	13.4	12.0	-1.4	bluerock/bhv/apps/vswitch/lib/vswitch/include/vswitch/aarch64_vswitch_config_hpp.v
-10.67%	27.1	24.2	-2.9	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/set_solver.v
-10.64%	13.5	12.1	-1.4	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/cstdlib/inc_cstdlib_cpp.v
-10.62%	59.6	53.3	-6.3	bluerock/bhv/zeta/lib/nova/proof/safe_proof/hypercall_au_lemmas.v
-10.61%	75.6	67.6	-8.0	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/ghost.v
-10.60%	137.4	122.8	-14.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtual_interface.v
-10.59%	13.3	11.9	-1.4	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_madt_hpp.v
-10.56%	26.2	23.4	-2.8	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/mvcg.v
-10.56%	13.5	12.1	-1.4	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_gtdt_cpp.v
-10.55%	25.4	22.7	-2.7	fmdeps/auto/coq-bluerock-auto-cpp/theories/cpp/virtual.v
-10.53%	18.5	16.5	-1.9	fmdeps/auto/coq-bluerock-auto-cpp/theories/cpp/oprimR.v
-10.53%	123.6	110.6	-13.0	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/util.v
-10.52%	100.4	89.9	-10.6	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/model/cpu_hpp_spec.v
-10.51%	13.4	12.0	-1.4	bluerock/bhv/zeta/lib/nova/include/nova/aarch64_syscall_common_hpp.v
-10.50%	105.1	94.0	-11.0	bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/msr_hpp_spec.v
-10.48%	14.4	12.9	-1.5	bluerock/bhv/apps/vswitch/lib/vswitch/src/aarch64_vswitch_cpp_names.v
-10.44%	68.9	61.7	-7.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/linearized_desc.v
-10.43%	13.6	12.2	-1.4	bluerock/NOVA/build-proof/proof/aarch64/pci_hpp.v
-10.43%	13.5	12.1	-1.4	bluerock/bhv/zeta/lib/nova/include/nova/aarch64_errno_hpp.v
-10.40%	13.7	12.3	-1.4	bluerock/NOVA/build-proof/proof/aarch64/acpi_fixed_hpp.v
-10.39%	14.5	13.0	-1.5	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/src/aarch64/vcpu_cpp_names.v
-10.38%	72.3	64.8	-7.5	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/desc_metadata.v
-10.34%	47.4	42.5	-4.9	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_split_range.v
-10.32%	14.5	13.0	-1.5	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/templates/upstream/bi/learn.v
-10.27%	19.9	17.9	-2.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/linking_proof.v
-10.24%	13.8	12.4	-1.4	bluerock/NOVA/build-proof/proof/aarch64/gicd_hpp.v
-10.20%	13.8	12.4	-1.4	bluerock/bhv/apps/vswitch/lib/acl/include/acl/aarch64_parser_hpp.v
-10.18%	14.8	13.3	-1.5	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/src/aarch64_vcpu_base_cpp_names.v
-10.18%	64.6	58.0	-6.6	bluerock/NOVA/build-proof/proof/timeout_cpp_proof/hints.v
-10.16%	25.1	22.6	-2.6	fmdeps/auto/coq-bluerock-auto-core/theories/hints/cancelx_notation.v
-10.15%	63.7	57.2	-6.5	bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/requeue.v
-10.14%	19.4	17.4	-2.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/templates/logic/wp_expr.v
-10.13%	53.3	47.9	-5.4	bluerock/bhv/zeta/lib/lang/proof/endian_hpp_spec.v
-10.12%	53.0	47.7	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/data_class/dataclass_hpp_proof.v
-10.10%	52.8	47.5	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/casts/cast_cpp_proof.v
-10.09%	66.0	59.4	-6.7	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxshared/nth_client.v
-10.07%	18.1	16.2	-1.8	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/templates/upstream/prelude/parse.v
-10.07%	46.1	41.5	-4.6	fmdeps/auto/coq-bluerock-auto-cpp/tests/arch_indep/x86_64/simple_arch_hpp_spec.v
-10.04%	29.0	26.1	-2.9	fmdeps/auto/coq-bluerock-auto-cpp/theories/upstream/cpp/countLN.v
-10.04%	14.1	12.6	-1.4	bluerock/NOVA/build-proof/proof/aarch64/cpu_hpp.v
-9.99%	123.7	111.4	-12.4	bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/hints.v
-9.96%	66.1	59.5	-6.6	bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/hints.v
-9.93%	78.6	70.8	-7.8	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/devq/misc.v
-9.92%	83.1	74.8	-8.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/hints.v
-9.86%	31.7	28.6	-3.1	fmdeps/auto/coq-bluerock-auto-cpp/theories/lib/fracQ.v
-9.83%	62.9	56.7	-6.2	bluerock/NOVA/build-proof/proof/ec_hpp_spec/status_pred.v
-9.78%	16.8	15.2	-1.6	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/templates/semantics/subst_build.v
-9.75%	23.3	21.1	-2.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/wapply.v
-9.75%	164.5	148.5	-16.0	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/handle_msr_exit.v
-9.74%	68.9	62.2	-6.7	bluerock/NOVA/build-proof/proof/pd_cpp_proof/hints.v
-9.71%	26.6	24.0	-2.6	fmdeps/auto/coq-bluerock-auto-cpp/theories/base_logic/lib/saved_mpred.v
-9.71%	66.4	60.0	-6.4	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxclient/signaling.v
-9.66%	55.4	50.1	-5.4	bluerock/bhv/apps/umx/proof/queue.v
-9.65%	14.6	13.2	-1.4	bluerock/bhv/apps/vmm/vml/devices/virtio_base/include/model/aarch64_virtqueue_hpp.v
-9.64%	11.1	10.0	-1.1	fmdeps/auto/coq-bluerock-auto-cpp/tests/lazy_unfold/as_Rep.v
-9.64%	14.5	13.1	-1.4	bluerock/NOVA/build-proof/proof/aarch64/gich_hpp.v
-9.63%	51.6	46.6	-5.0	bluerock/NOVA/build-proof/proof/slab/slab_proof_slab.v
-9.62%	84.1	76.0	-8.1	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/TO_UPSTREAM.v
-9.62%	14.7	13.3	-1.4	bluerock/bhv/lib/pm/pm_bhv/include/aarch64_info_hpp.v
-9.62%	55.5	50.2	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/array/initlist_cpp_proof.v
-9.55%	104.9	94.9	-10.0	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/spec.v
-9.54%	82.8	74.9	-7.9	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_finish.v
-9.44%	14.7	13.3	-1.4	bluerock/bhv/zeta/lib/intrusive/include/intrusive/aarch64_rangemap_hpp.v
-9.40%	18.9	17.1	-1.8	fmdeps/auto/coq-bluerock-auto-core/tests/test.v
-9.37%	14.6	13.2	-1.4	bluerock/bhv/zeta/lib/cxx/src/aarch64_rangeset_cpp.v
-9.32%	28.7	26.1	-2.7	fmdeps/auto/coq-bluerock-auto-cpp/tests/new_delete/test_cpp_proof.v
-9.31%	70.7	64.2	-6.6	bluerock/bhv/apps/umx/proof/admin_cpp_proof/admin_console.v
-9.26%	58.1	52.7	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0076_cpp_f0_proof.v
-9.24%	121.5	110.3	-11.2	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/init_info.v
-9.24%	66.8	60.6	-6.2	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/insert.v
-9.21%	25.2	22.8	-2.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/invariants.v
-9.18%	14.9	13.5	-1.4	bluerock/bhv/zeta/lib/cxx/include/aarch64_cpuset_hpp.v
-9.15%	71.6	65.1	-6.6	bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/unblock.v
-9.14%	75.2	68.3	-6.9	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/invoke.v
-9.10%	89.2	81.0	-8.1	bluerock/NOVA/build-proof/proof/soup/abs_pred.v
-9.08%	58.3	53.0	-5.3	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/iterator/spec.v
-9.00%	64.2	58.5	-5.8	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_merge.v
-8.96%	24.6	22.4	-2.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/inline_invoke.v
-8.96%	69.4	63.1	-6.2	bluerock/bhv/apps/vswitch/lib/vsmp/proof/msg_queue_hpp/defs.v
-8.95%	77.6	70.7	-6.9	bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_hpp_spec.v
-8.94%	75.5	68.7	-6.7	bluerock/bhv/apps/umx/proof/admin_cpp_proof/read_escape.v
-8.94%	61.0	55.6	-5.5	bluerock/bhv/zeta/lib/lang/proof/endian64_hpp_proof.v
-8.89%	229.7	209.3	-20.4	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/ctor.v
-8.88%	15.4	14.0	-1.4	bluerock/NOVA/build-proof/proof/aarch64/fpu_hpp.v
-8.78%	15.1	13.8	-1.3	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/include/model/aarch64_cpu_feature_hpp.v
-8.78%	86.3	78.7	-7.6	bluerock/NOVA/build-proof/proof/ec_proof/status_accessors.v
-8.78%	12.8	11.7	-1.1	fmdeps/auto/coq-bluerock-auto-cpp/theories/lib/suffix.v
-8.77%	62.1	56.6	-5.4	bluerock/NOVA/build-proof/proof/tests/queue/test_queue_proof.v
-8.77%	131.8	120.2	-11.6	bluerock/bhv/apps/vmm/vml/devices/msr/proof/msr_base_hpp_spec.v
-8.77%	61.7	56.3	-5.4	bluerock/bhv/zeta/lib/lang/proof/errno_hpp_proof.v
-8.69%	12.2	11.1	-1.1	fmdeps/auto/coq-bluerock-auto-cpp/tests/data_class/dataclass_tests.v
-8.67%	15.0	13.7	-1.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/templates/upstream/bi/runI.v
-8.66%	90.6	82.8	-7.8	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/spec.v
-8.64%	160.5	146.6	-13.9	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/misc_hints.v
-8.49%	134.5	123.1	-11.4	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/emulation.v
-8.48%	83.8	76.6	-7.1	bluerock/bhv/apps/umx/proof/main_cpp_proof/setup_sigs.v
-8.48%	15.7	14.3	-1.3	bluerock/bhv/zeta/lib/alloc/include/alloc/aarch64_range_hpp.v
-8.44%	63.4	58.0	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0059_cpp_f2_proof.v
-8.33%	15.9	14.6	-1.3	bluerock/bhv/zeta/lib/intrusive/include/intrusive/aarch64_shared_pointer_instantiations_hpp.v
-8.32%	20.1	18.4	-1.7	fmdeps/auto/coq-bluerock-auto-core/tests/forward.v
-8.30%	64.4	59.1	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0088_cpp_main_proof.v
-8.27%	137.1	125.8	-11.3	bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/proof.v
-8.26%	45.0	41.3	-3.7	fmdeps/auto/coq-bluerock-auto-cpp/tests/templates/inc_twice_hpp_proof.v
-8.25%	179.1	164.3	-14.8	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/reset.v
-8.23%	59.0	54.1	-4.9	fmdeps/auto/coq-bluerock-auto-cpp/tests/lib_alloc/alloc_hpp_proof.v
-8.17%	16.1	14.8	-1.3	bluerock/bhv/apps/vmm/vml/devices/virtio_base/src/aarch64_virtqueue_cpp.v
-8.16%	31.0	28.4	-2.5	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/wp_path.v
-8.14%	199.3	183.0	-16.2	bluerock/bhv/apps/vswitch/lib/vswitch/proof/initialize_dataplane.v
-8.12%	247.9	227.8	-20.1	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort_to_vbus.v
-8.11%	72.2	66.3	-5.9	bluerock/NOVA/build-proof/proof/scheduler_hpp_spec/abs_pred.v
-8.08%	205.4	188.8	-16.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/set_virtio_net_header.v
-8.06%	22.7	20.8	-1.8	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/name_pattern.v
-8.05%	16.5	15.2	-1.3	bluerock/NOVA/build-proof/proof/aarch64/stdio_hpp.v
-8.04%	16.5	15.2	-1.3	bluerock/NOVA/build-proof/proof/aarch64/assert_hpp.v
-8.04%	16.5	15.2	-1.3	bluerock/NOVA/build-proof/proof/aarch64/queue_hpp.v
-8.04%	67.5	62.1	-5.4	bluerock/bhv/zeta/lib/lang/proof/endian32_hpp_proof.v
-8.02%	66.0	60.7	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/read_prim/read_cpp_proof.v
-8.02%	36.4	33.5	-2.9	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/delayed_case.v
-8.00%	69.8	64.2	-5.6	fmdeps/auto/coq-bluerock-auto-cpp/tests/templates/pair_hpp_spec.v
-8.00%	80.4	74.0	-6.4	bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/release_queue.v
-7.94%	59.2	54.5	-4.7	bluerock/NOVA/build-proof/proof/slab/slab_proof_lemmata.v
-7.94%	18.2	16.8	-1.4	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/templates/semantics/subst.v
-7.92%	83.6	76.9	-6.6	bluerock/NOVA/build-proof/proof/slab/slab_proof_metadata_sideline.v
-7.91%	16.8	15.4	-1.3	bluerock/NOVA/build-proof/proof/aarch64/timeout_budget_cpp.v
-7.90%	255.2	235.0	-20.2	bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/msr_hpp_proof.v
-7.90%	202.3	186.3	-16.0	bluerock/bhv/apps/vswitch/lib/vswitch/proof/create_forwarding_plane.v
-7.89%	16.8	15.5	-1.3	bluerock/bhv/lib/vrl/include/vrl/aarch64_port_hpp.v
-7.87%	25.9	23.9	-2.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/base_logic/lib/qtickets.v
-7.87%	22.1	20.4	-1.7	fmdeps/auto/coq-bluerock-auto-core/tests/learn/test.v
-7.85%	95.6	88.1	-7.5	bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_sm.v
-7.83%	87.4	80.5	-6.8	bluerock/bhv/apps/vmm/lib/vm_config/proof/bson_config_hpp_spec.v
-7.80%	17.0	15.7	-1.3	bluerock/bhv/lib/vrl/include/vrl/aarch64_route_hpp.v
-7.79%	149.6	137.9	-11.6	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_off.v
-7.77%	68.9	63.5	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/data_class/class_16_cpp_proof.v
-7.76%	62.4	57.6	-4.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/derive/cpp_test.v
-7.73%	17.1	15.8	-1.3	bluerock/NOVA/build-proof/proof/aarch64/scheduler_hpp.v
-7.73%	146.8	135.5	-11.4	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_emulating.v
-7.72%	78.5	72.4	-6.1	bluerock/NOVA/build-proof/proof/pt_cpp_proof/proof.v
-7.70%	17.2	15.9	-1.3	bluerock/NOVA/build-proof/proof/aarch64/refcnt_hpp.v
-7.67%	153.4	141.7	-11.8	bluerock/bhv/apps/vmm/vml/devices/gic/proof/model/gic_hpp_spec.v
-7.67%	85.0	78.5	-6.5	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxshared/ctor.v
-7.67%	27.3	25.2	-2.1	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/Arith.v
-7.66%	115.8	106.9	-8.9	bluerock/bhv/apps/umx/proof/main_cpp_proof/output_loop.v
-7.65%	82.3	76.0	-6.3	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxclient/init_ctor.v
-7.65%	115.8	106.9	-8.9	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/requesters.v
-7.62%	177.8	164.3	-13.5	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof.v
-7.61%	39.8	36.7	-3.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/layout.v
-7.60%	17.4	16.1	-1.3	bluerock/NOVA/build-proof/proof/aarch64/test_queue_cpp.v
-7.59%	71.3	65.9	-5.4	bluerock/bhv/zeta/lib/lang/proof/endian8_hpp_proof.v
-7.58%	114.9	106.2	-8.7	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/defs.v
-7.58%	17.4	16.1	-1.3	bluerock/NOVA/build-proof/proof/aarch64/smc_arch_cpp.v
-7.57%	167.3	154.7	-12.7	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/walk_chain.v
-7.56%	17.5	16.1	-1.3	bluerock/NOVA/build-proof/proof/aarch64/timeout_cpp.v
-7.52%	17.5	16.2	-1.3	bluerock/NOVA/build-proof/proof/aarch64/kobject_hpp.v
-7.45%	17.7	16.4	-1.3	bluerock/bhv/zeta/lib/bson/include/bson/aarch64_bson_hpp.v
-7.44%	138.6	128.3	-10.3	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/model/cpu_hpp_properties.v
-7.44%	24.7	22.8	-1.8	fmdeps/auto/rocq-bluerock-cpp-stdlib/tests/cctype/test_cpp.v
-7.38%	17.9	16.6	-1.3	bluerock/bhv/zeta/lib/concurrent/include/concurrent/aarch64_lock_hpp.v
-7.38%	30.4	28.2	-2.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/initialize.v
-7.34%	18.0	16.6	-1.3	bluerock/NOVA/build-proof/proof/aarch64/buddy_hpp.v
-7.30%	109.2	101.2	-8.0	bluerock/bhv/apps/vswitch/proof/ghost.v
-7.28%	94.1	87.3	-6.9	bluerock/NOVA/build-proof/proof/iface/predicates/core.v
-7.23%	163.0	151.2	-11.8	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_roundedup.v
-7.23%	14.5	13.4	-1.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/lib/prefix.v
-7.22%	79.0	73.3	-5.7	bluerock/NOVA/build-proof/proof/timeout_cpp_proof/client_dequeue.v
-7.21%	18.4	17.1	-1.3	bluerock/NOVA/build-proof/proof/aarch64/smc_psci_cpp.v
-7.19%	98.9	91.8	-7.1	bluerock/bhv/lib/vrl/proof/vrl/port_hpp_spec.v
-7.16%	74.8	69.4	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0052_cpp_f2_proof.v
-7.16%	18.5	17.2	-1.3	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_tpm2_cpp.v
-7.15%	18.9	17.6	-1.4	fmdeps/auto/rocq-bluerock-cpp-stdlib/tests/cstdlib/test_cpp.v
-7.12%	84.7	78.7	-6.0	bluerock/bhv/lib/drivers/serial/pl011/proof/compatible.v
-7.10%	115.2	107.1	-8.2	bluerock/NOVA/build-proof/proof/iface/hypercall/pd.v
-7.09%	140.7	130.8	-10.0	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_sc.v
-7.08%	18.7	17.4	-1.3	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_facs_cpp.v
-7.08%	212.7	197.6	-15.1	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/check_reset.v
-7.07%	92.4	85.9	-6.5	bluerock/NOVA/build-proof/proof/ec_hpp_spec/const_pred.v
-7.07%	229.8	213.5	-16.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/drop.v
-7.06%	18.6	17.3	-1.3	bluerock/NOVA/build-proof/proof/aarch64/capability_hpp.v
-6.95%	41.4	38.5	-2.9	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/multiborrow.v
-6.94%	15.1	14.0	-1.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/lib/append.v
-6.93%	18.9	17.6	-1.3	bluerock/bhv/zeta/lib/alloc/include/alloc/aarch64_sels_hpp.v
-6.92%	356.6	331.9	-24.7	bluerock/bhv/apps/vmm/proof/main_cpp_proof.v
-6.89%	26.4	24.5	-1.8	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/templates/upstream/brick/materialize.v
-6.89%	19.1	17.8	-1.3	bluerock/NOVA/build-proof/proof/aarch64/buddy_cpp.v
-6.86%	42.7	39.8	-2.9	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/auto_frac/hints.v
-6.83%	81.2	75.7	-5.5	bluerock/bhv/zeta/lib/lang/proof/compiler_hpp_proof.v
-6.81%	156.7	146.0	-10.7	bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/msr_cpp_proof.v
-6.80%	107.9	100.5	-7.3	bluerock/bhv/lib/vrl/proof/vrl/port_hpp_proof.v
-6.80%	19.3	18.0	-1.3	bluerock/NOVA/build-proof/proof/aarch64/ptab_hpp.v
-6.78%	19.3	18.0	-1.3	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_spcr_cpp.v
-6.77%	78.3	73.0	-5.3	fmdeps/auto-docs/content/demo/linked_list/linked_list_cpp_proof.v
-6.77%	19.3	18.0	-1.3	bluerock/bhv/zeta/lib/cxx/include/sys/aarch64_semaphore_hpp.v
-6.76%	19.4	18.1	-1.3	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_dbg2_cpp.v
-6.76%	79.1	73.8	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/data_class/dataclass_hpp_spec2.v
-6.75%	19.4	18.1	-1.3	bluerock/NOVA/build-proof/proof/aarch64/slab_cpp.v
-6.70%	79.3	74.0	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/array_string_init/main_cpp_proof.v
-6.70%	78.1	72.9	-5.2	fmdeps/auto-docs/content/demo/forward_list_v1/test_cpp_proof.v
-6.69%	61.2	57.1	-4.1	fmdeps/auto/coq-bluerock-auto-cpp/tests/arch_indep/aarch64/inheritance_arch_hpp_spec.v
-6.69%	19.4	18.1	-1.3	bluerock/bhv/apps/vmm/vml/devices/virtio_base/include/model/aarch64_virtio_sg_hpp.v
-6.68%	19.6	18.3	-1.3	bluerock/NOVA/build-proof/proof/aarch64/ptab_pte_hpp.v
-6.67%	19.6	18.3	-1.3	bluerock/bhv/zeta/lib/cxx/include/bluerock/sys/aarch64_mutex_hpp.v
-6.66%	19.6	18.3	-1.3	bluerock/bhv/zeta/lib/cxx/include/sys/aarch64_lock_guard_hpp.v
-6.64%	84.2	78.6	-5.6	bluerock/bhv/zeta/lib/cxx/proof/sys/mutex_hpp_proof.v
-6.64%	19.5	18.2	-1.3	bluerock/bhv/zeta/apps/msc/include/msc/aarch64_bootargs_hpp.v
-6.63%	96.3	89.9	-6.4	bluerock/NOVA/build-proof/proof/ec_hpp_spec/active_pred.v
-6.61%	100.0	93.4	-6.6	bluerock/NOVA/build-proof/proof/sm_cpp_proof/create.v
-6.60%	19.7	18.4	-1.3	bluerock/NOVA/build-proof/proof/aarch64/console_mbuf_hpp.v
-6.60%	80.5	75.2	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0076_cpp_main_proof.v
-6.58%	123.4	115.3	-8.1	bluerock/NOVA/build-proof/proof/pd_cpp_proof/create.v
-6.56%	19.9	18.6	-1.3	bluerock/NOVA/build-proof/proof/aarch64/rcu_cpp.v
-6.56%	19.9	18.6	-1.3	bluerock/bhv/zeta/apps/msc/include/msc/aarch64_multiboot2_hpp.v
-6.53%	81.8	76.5	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0084_cpp_main_proof.v
-6.53%	20.1	18.7	-1.3	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_srat_cpp.v
-6.51%	329.6	308.2	-21.4	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/wp_vcpu_lemmas.v
-6.51%	20.0	18.7	-1.3	bluerock/NOVA/build-proof/proof/aarch64/pd_hpp.v
-6.49%	114.2	106.8	-7.4	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/defs.v
-6.47%	88.4	82.6	-5.7	bluerock/NOVA/build-proof/proof/timeout_cpp_proof/private_dequeue.v
-6.41%	84.3	78.9	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/virtual/virtual_destructor_cpp_proof.v
-6.39%	49.3	46.2	-3.1	bluerock/bhv/apps/vswitch/proof/model/ethernet.v
-6.38%	20.5	19.2	-1.3	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/exception/inc_exception_cpp.v
-6.37%	20.4	19.1	-1.3	bluerock/NOVA/build-proof/proof/aarch64/space_hpp.v
-6.35%	20.4	19.1	-1.3	bluerock/bhv/zeta/lib/cli/include/cli/aarch64_command_handler_hpp.v
-6.34%	20.5	19.2	-1.3	bluerock/NOVA/build-proof/proof/aarch64/space_msr_hpp.v
-6.34%	20.5	19.2	-1.3	bluerock/NOVA/build-proof/proof/aarch64/space_pio_hpp.v
-6.34%	43.5	40.7	-2.8	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/genv_tu.v
-6.33%	40.7	38.1	-2.6	fmdeps/auto/coq-bluerock-auto-cpp/theories/lib/pred_utils.v
-6.32%	155.7	145.9	-9.8	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_pt.v
-6.31%	20.8	19.5	-1.3	bluerock/bhv/zeta/lib/pt/include/pt/aarch64_pt_hpp.v
-6.30%	20.9	19.6	-1.3	bluerock/bhv/zeta/lib/bhv/include/bhv/aarch64_types_hpp.v
-6.28%	32.0	30.0	-2.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/lazy_unfold.v
-6.22%	133.1	124.9	-8.3	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxclient/move_assignment.v
-6.16%	21.4	20.1	-1.3	bluerock/NOVA/build-proof/proof/aarch64/space_mem_hpp.v
-6.16%	106.3	99.7	-6.5	bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxshared/signals.v
-6.16%	189.2	177.5	-11.6	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/wait_if_exec_paused.v
-6.15%	33.5	31.5	-2.1	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/cast.v
-6.15%	87.7	82.3	-5.4	bluerock/bhv/zeta/lib/cxx/proof/bitset_hpp_proof.v
-6.14%	21.2	19.9	-1.3	bluerock/NOVA/build-proof/proof/aarch64/ptab_dpt_hpp.v
-6.14%	253.9	238.3	-15.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/flood.v
-6.12%	21.5	20.2	-1.3	bluerock/NOVA/build-proof/proof/aarch64/ptab_hpt_hpp.v
-6.12%	21.4	20.1	-1.3	bluerock/NOVA/build-proof/proof/aarch64/utcb_hpp.v
-6.11%	22.0	20.6	-1.3	bluerock/bhv/lib/vrl/include/vrl/aarch64_packet_hpp.v
-6.10%	87.2	81.9	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0059_cpp_main_proof.v
-6.10%	87.1	81.8	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0099_cpp_main_proof.v
-6.09%	212.4	199.4	-12.9	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/hints.v
-6.08%	31.3	29.4	-1.9	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/big_sep/normalize.v
-6.08%	22.4	21.0	-1.4	bluerock/bhv/zeta/lib/bson/src/aarch64_bson_cpp.v
-6.07%	43.6	41.0	-2.6	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/operators.v
-6.07%	22.0	20.7	-1.3	bluerock/NOVA/build-proof/proof/aarch64/ptab_hpt_cpp.v
-6.06%	22.1	20.7	-1.3	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_mcfg_cpp.v
-6.06%	22.3	20.9	-1.3	bluerock/NOVA/build-proof/proof/aarch64/ptab_npt_cpp.v
-6.06%	22.5	21.1	-1.4	bluerock/bhv/lib/ddk/include/ddk/aarch64_dmadev_drv_hpp.v
-6.06%	22.1	20.8	-1.3	bluerock/NOVA/build-proof/proof/aarch64/ptab_npt_hpp.v
-6.05%	24.0	22.6	-1.5	bluerock/bhv/apps/vmm/vml/devices/virtio_base/src/aarch64_virtio_sg_cpp.v
-6.03%	66.9	62.9	-4.0	fmdeps/auto/coq-bluerock-auto-cpp/tests/arch_indep/x86_64/inheritance_arch_hpp_spec.v
-6.03%	22.3	21.0	-1.3	bluerock/NOVA/build-proof/proof/aarch64/cmdline_cpp.v
-6.02%	22.5	21.1	-1.4	bluerock/bhv/zeta/lib/fdt/include/fdt/aarch64_fdt_hpp.v
-5.98%	22.6	21.2	-1.3	bluerock/NOVA/build-proof/proof/aarch64/gicr_hpp.v
-5.97%	92.4	86.9	-5.5	fmdeps/auto/coq-bluerock-auto-cpp/tests/big_sep/basic.v
-5.97%	30.5	28.7	-1.8	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/big_sep/lemmas.v
-5.96%	188.5	177.2	-11.2	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/defs.v
-5.95%	98.8	92.9	-5.9	bluerock/NOVA/build-proof/proof/aarch64/slab_hpp_proof.v
-5.94%	219.1	206.1	-13.0	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/roundup_impl.v
-5.94%	110.4	103.8	-6.6	bluerock/NOVA/build-proof/proof/sm_cpp_proof/up.v
-5.93%	25.6	24.1	-1.5	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/templates/semantics/subst_ap.v
-5.93%	90.1	84.8	-5.3	bluerock/bhv/zeta/lib/lang/proof/endian16_hpp_proof.v
-5.91%	24.8	23.3	-1.5	bluerock/bhv/zeta/lib/alloc/include/alloc/aarch64_vmap_hpp.v
-5.91%	23.9	22.5	-1.4	bluerock/NOVA/build-proof/proof/aarch64/space_obj_hpp.v
-5.87%	25.3	23.8	-1.5	bluerock/bhv/zeta/lib/alloc/include/alloc/aarch64_allocator_hpp.v
-5.87%	24.3	22.9	-1.4	bluerock/NOVA/build-proof/proof/aarch64/space_obj_cpp.v
-5.86%	30.9	29.1	-1.8	bluerock/bhv/zeta/lib/fdt/src/aarch64_fdt_cpp.v
-5.84%	70.2	66.1	-4.1	fmdeps/auto/coq-bluerock-auto-cpp/tests/arch_indep/simple_if_style_hpp_spec.v
-5.84%	88.8	83.6	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/dataclass_demo/dataclass_demo.v
-5.81%	120.1	113.1	-7.0	bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_pd.v
-5.79%	196.0	184.6	-11.3	bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_cpp_proof/space_sel.v
-5.78%	102.2	96.3	-5.9	bluerock/NOVA/build-proof/proof/pd_hpp_spec/triples.v
-5.78%	97.6	92.0	-5.6	bluerock/NOVA/build-proof/proof/timeout_cpp_proof/enqueue.v
-5.77%	25.1	23.7	-1.5	bluerock/bhv/lib/drivers/dma/zynqmp_dma/include/zynqmp_dma/aarch64_zynqmp_dma_ver_hpp.v
-5.76%	25.6	24.1	-1.5	bluerock/NOVA/build-proof/proof/aarch64/pci_cpp.v
-5.74%	374.0	352.5	-21.5	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort.v
-5.74%	32.0	30.1	-1.8	bluerock/NOVA/build-proof/proof/aarch64/regs_hpp.v
-5.72%	25.9	24.4	-1.5	bluerock/bhv/zeta/lib/fdt/include/fdt/aarch64_property_hpp.v
-5.72%	93.5	88.2	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0094_cpp_main_proof.v
-5.70%	28.7	27.1	-1.6	bluerock/bhv/apps/vmm/lib/bluerock/include/aarch64/platform/reg_accessor_hpp.v
-5.70%	26.0	24.6	-1.5	bluerock/bhv/zeta/lib/fdt/src/aarch64_property_cpp.v
-5.69%	26.2	24.7	-1.5	bluerock/bhv/apps/vmm/lib/bluerock/include/platform/aarch64_irq_hpp.v
-5.69%	105.7	99.7	-6.0	bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_other.v
-5.68%	26.2	24.7	-1.5	bluerock/bhv/zeta/lib/alloc/include/bhv/aarch64_sel_alloc_hpp.v
-5.67%	108.3	102.2	-6.1	bluerock/NOVA/build-proof/proof/slab/slab_cache_free.v
-5.67%	26.6	25.1	-1.5	bluerock/bhv/zeta/lib/fdt/include/fdt/aarch64_base_device_hpp.v
-5.65%	26.6	25.1	-1.5	bluerock/bhv/zeta/lib/fdt/include/fdt/aarch64_as_hpp.v
-5.63%	26.4	24.9	-1.5	bluerock/NOVA/build-proof/proof/aarch64/acpi_arch_hpp.v
-5.63%	27.1	25.6	-1.5	bluerock/bhv/zeta/lib/fdt/include/fdt/aarch64_reglist_hpp.v
-5.61%	27.3	25.7	-1.5	bluerock/bhv/zeta/lib/fdt/include/fdt/aarch64_reserved_mem_hpp.v
-5.60%	26.0	24.5	-1.5	bluerock/NOVA/build-proof/proof/aarch64/console_uart_hpp.v
-5.60%	26.4	24.9	-1.5	bluerock/NOVA/build-proof/proof/aarch64/console_uart_mini_hpp.v
-5.60%	115.5	109.0	-6.5	bluerock/NOVA/build-proof/proof/ec_hpp_spec/cont_pred.v
-5.60%	26.4	24.9	-1.5	bluerock/NOVA/build-proof/proof/aarch64/console_uart_mini_cpp.v
-5.60%	26.3	24.9	-1.5	bluerock/NOVA/build-proof/proof/aarch64/console_uart_cdns_hpp.v
-5.59%	26.3	24.9	-1.5	bluerock/NOVA/build-proof/proof/aarch64/console_uart_meson_cpp.v
-5.59%	26.4	24.9	-1.5	bluerock/NOVA/build-proof/proof/aarch64/console_uart_cdns_cpp.v
-5.59%	26.3	24.8	-1.5	bluerock/NOVA/build-proof/proof/aarch64/console_uart_meson_hpp.v
-5.59%	26.7	25.2	-1.5	bluerock/NOVA/build-proof/proof/aarch64/space_gst_hpp.v
-5.58%	26.6	25.1	-1.5	bluerock/NOVA/build-proof/proof/aarch64/console_uart_imx_hpp.v
-5.58%	26.4	24.9	-1.5	bluerock/NOVA/build-proof/proof/aarch64/console_uart_pl011_hpp.v
-5.58%	26.4	25.0	-1.5	bluerock/NOVA/build-proof/proof/aarch64/console_uart_pl011_cpp.v
-5.58%	26.5	25.0	-1.5	bluerock/NOVA/build-proof/proof/aarch64/console_uart_ns16550_hpp.v
-5.58%	26.5	25.0	-1.5	bluerock/NOVA/build-proof/proof/aarch64/console_uart_ns16550_cpp.v
-5.57%	26.5	25.0	-1.5	bluerock/NOVA/build-proof/proof/aarch64/console_uart_scif_hpp.v
-5.57%	26.6	25.1	-1.5	bluerock/NOVA/build-proof/proof/aarch64/console_uart_imx_cpp.v
-5.55%	26.5	25.0	-1.5	bluerock/NOVA/build-proof/proof/aarch64/console_uart_scif_cpp.v
-5.55%	26.8	25.3	-1.5	bluerock/NOVA/build-proof/proof/aarch64/space_hst_hpp.v
-5.54%	22.6	21.3	-1.3	bluerock/bhv/apps/vmm/lib/board/include/model/aarch64_board_common_hpp_names.v
-5.54%	28.9	27.3	-1.6	bluerock/bhv/zeta/lib/fdt/include/fdt/aarch64_uart_hpp.v
-5.54%	28.8	27.2	-1.6	bluerock/bhv/apps/vmm/lib/vm_config/include/aarch64_bson_config_hpp.v
-5.49%	112.3	106.1	-6.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/llist/list_cpp_proof.v
-5.48%	29.8	28.1	-1.6	bluerock/bhv/zeta/lib/msc/include/bluerock/sys/aarch64_signal_hpp.v
-5.48%	28.9	27.4	-1.6	bluerock/NOVA/build-proof/proof/aarch64/space_hst_cpp.v
-5.46%	116.9	110.5	-6.4	bluerock/bhv/zeta/lib/cxx/proof/tagged_ptr_hpp_proof.v
-5.45%	28.0	26.5	-1.5	bluerock/NOVA/build-proof/proof/aarch64/ptab_cpp.v
-5.44%	126.6	119.7	-6.9	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/lookup.v
-5.43%	29.2	27.6	-1.6	bluerock/NOVA/build-proof/proof/aarch64/mmio_hpp.v
-5.43%	33.6	31.8	-1.8	bluerock/bhv/apps/vmm/lib/bluerock/include/bluerock/platform/aarch64_signal_hpp.v
-5.43%	30.1	28.5	-1.6	bluerock/bhv/zeta/lib/zeta/include/zeta/aarch64_signal_hpp.v
-5.42%	35.5	33.6	-1.9	bluerock/bhv/zeta/lib/alloc/src/aarch64_malloc_cpp.v
-5.41%	236.6	223.8	-12.8	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/defs.v
-5.40%	106.2	100.5	-5.7	bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_proof.v
-5.37%	35.9	34.0	-1.9	bluerock/bhv/zeta/lib/msc/include/sys/aarch64_rwlock_hpp.v
-5.36%	99.1	93.8	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0094_cpp_f3_proof.v
-5.36%	33.1	31.3	-1.8	bluerock/bhv/zeta/lib/msc/include/bluerock/sys/aarch64_user_signal_hpp.v
-5.36%	32.6	30.9	-1.7	bluerock/bhv/zeta/lib/umx/include/umx/aarch64_umx_hpp.v
-5.35%	137.8	130.4	-7.4	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/update.v
-5.35%	37.0	35.0	-2.0	bluerock/bhv/zeta/apps/msc/include/msc/bhv/aarch64_nova_caprange_hpp.v
-5.34%	153.5	145.3	-8.2	bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command.v
-5.33%	99.7	94.4	-5.3	fmdeps/auto-docs/content/demo/basic/main_cpp_proof.v
-5.32%	108.3	102.5	-5.8	bluerock/NOVA/build-proof/proof/syscall_hpp_proof.v
-5.32%	31.9	30.2	-1.7	bluerock/NOVA/build-proof/proof/aarch64/abi_hpp.v
-5.32%	33.4	31.6	-1.8	bluerock/bhv/zeta/lib/alloc/include/alloc/aarch64_unique_sels_hpp.v
-5.32%	108.8	103.0	-5.8	bluerock/NOVA/build-proof/proof/pt_cpp_proof/create.v
-5.30%	32.0	30.3	-1.7	bluerock/NOVA/build-proof/proof/aarch64/smmu_hpp.v
-5.29%	34.8	32.9	-1.8	bluerock/NOVA/build-proof/proof/aarch64/syscall_hpp.v
-5.27%	36.4	34.5	-1.9	bluerock/NOVA/build-proof/proof/aarch64/sc_hpp.v
-5.27%	37.1	35.1	-2.0	bluerock/NOVA/build-proof/proof/aarch64/timeout_hypercall_cpp.v
-5.26%	37.5	35.5	-2.0	bluerock/bhv/lib/pm/pm_bhv/include/dev/aarch64_sm_devs_hpp.v
-5.26%	36.4	34.5	-1.9	bluerock/NOVA/build-proof/proof/aarch64/ec_hpp.v
-5.25%	37.0	35.1	-1.9	bluerock/NOVA/build-proof/proof/aarch64/sm_hpp.v
-5.25%	36.9	35.0	-1.9	bluerock/NOVA/build-proof/proof/aarch64/fpu_cpp.v
-5.24%	37.2	35.3	-1.9	bluerock/NOVA/build-proof/proof/aarch64/sm_cpp.v
-5.23%	78.6	74.5	-4.1	fmdeps/auto/coq-bluerock-auto-cpp/tests/arch_indep/inheritance_if_style_hpp_spec.v
-5.23%	33.8	32.0	-1.8	bluerock/NOVA/build-proof/proof/aarch64/smmu_v2_hpp.v
-5.22%	37.1	35.1	-1.9	bluerock/NOVA/build-proof/proof/aarch64/sc_cpp.v
-5.22%	36.9	34.9	-1.9	bluerock/NOVA/build-proof/proof/aarch64/dc_cpp.v
-5.21%	36.6	34.7	-1.9	bluerock/NOVA/build-proof/proof/aarch64/dc_state_hpp.v
-5.21%	43.8	41.6	-2.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/new_delete.v
-5.21%	37.6	35.6	-2.0	bluerock/NOVA/build-proof/proof/aarch64/smmu_v3_hpp.v
-5.21%	37.8	35.8	-2.0	bluerock/NOVA/build-proof/proof/aarch64/pt_hpp.v
-5.20%	36.8	34.9	-1.9	bluerock/NOVA/build-proof/proof/aarch64/dc_hpp.v
-5.20%	34.4	32.6	-1.8	bluerock/NOVA/build-proof/proof/aarch64/gits_hpp.v
-5.20%	154.5	146.5	-8.0	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/devq/send.v
-5.20%	34.4	32.6	-1.8	bluerock/NOVA/build-proof/proof/aarch64/space_dma_hpp.v
-5.19%	38.1	36.1	-2.0	bluerock/NOVA/build-proof/proof/aarch64/pt_cpp.v
-5.17%	37.0	35.1	-1.9	bluerock/NOVA/build-proof/proof/aarch64/gits_cpp.v
-5.16%	38.7	36.7	-2.0	bluerock/NOVA/build-proof/proof/aarch64/console_mbuf_cpp.v
-5.16%	35.5	33.7	-1.8	bluerock/NOVA/build-proof/proof/aarch64/space_mem_cpp.v
-5.13%	23.9	22.6	-1.2	fmdeps/auto/coq-bluerock-auto-core/theories/internal/instr/split_propT.v
-5.12%	42.1	40.0	-2.2	bluerock/bhv/zeta/lib/zeta/include/zeta/aarch64_helpers_hpp.v
-5.12%	40.8	38.7	-2.1	bluerock/NOVA/build-proof/proof/aarch64/ec_arch_hpp.v
-5.12%	276.9	262.7	-14.2	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/proof.v
-5.09%	41.2	39.1	-2.1	bluerock/bhv/apps/vmm/lib/bluerock/src/aarch64_irq_cpp.v
-5.08%	147.0	139.6	-7.5	bluerock/bhv/zeta/lib/zeta/proof/semaphore_hpp_proof.v
-5.07%	42.0	39.8	-2.1	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_iort_cpp.v
-5.04%	125.9	119.6	-6.4	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/create.v
-5.02%	174.6	165.8	-8.8	bluerock/NOVA/build-proof/proof/sc_cpp_proof/create.v
-4.99%	230.9	219.4	-11.5	bluerock/bhv/apps/vswitch/lib/port/proof/port/defs.v
-4.97%	369.2	350.8	-18.4	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/handle_data_abort.v
-4.97%	30.4	28.9	-1.5	bluerock/NOVA/build-proof/proof/aarch64/integrity_cpp.v
-4.96%	134.1	127.4	-6.7	bluerock/bhv/zeta/lib/msc/proof/sys/signal_hpp_proof.v
-4.95%	51.1	48.6	-2.5	fmdeps/auto/coq-bluerock-auto-cpp/tests/pretty/tests.v
-4.95%	233.3	221.8	-11.5	bluerock/bhv/apps/umx/proof/main_cpp_proof/user_handler.v
-4.89%	123.0	116.9	-6.0	bluerock/NOVA/build-proof/proof/ec_hpp_spec/sched_pred.v
-4.89%	108.6	103.3	-5.3	bluerock/bhv/zeta/lib/lang/proof/string_cpp_proof.v
-4.80%	53.6	51.0	-2.6	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/specifications.v
-4.77%	42.8	40.7	-2.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/big_sep/classes.v
-4.73%	322.9	307.6	-15.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp_proof.v
-4.69%	148.6	141.6	-7.0	bluerock/bhv/lib/drivers/serial/pl011/proof/mmio.v
-4.69%	118.2	112.6	-5.5	bluerock/bhv/zeta/lib/concurrent/proof/lock_hpp_proof.v
-4.66%	110.9	105.7	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/fupd/inc_twice_hpp_spec.v
-4.64%	117.1	111.7	-5.4	bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_rich_proof.v
-4.59%	34.6	33.0	-1.6	bluerock/bhv/apps/vmm/src/aarch64_main_cpp_names.v
-4.59%	29.4	28.1	-1.4	bluerock/bhv/apps/vmm/lib/board/src/x86/board_cpp_names.v
-4.58%	49.8	47.5	-2.3	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/pretty/my_pretty_internals.v
-4.58%	57.4	54.7	-2.6	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/big_sep/array.v
-4.54%	182.5	174.2	-8.3	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/spec.v
-4.53%	490.9	468.7	-22.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/msr_framework.v
-4.50%	27.0	25.7	-1.2	bluerock/bhv/apps/vmm/lib/board/include/x86/board_impl_hpp_names.v
-4.49%	30.3	28.9	-1.4	bluerock/bhv/apps/vmm/lib/board/src/aarch64/board_cpp_names.v
-4.49%	27.1	25.8	-1.2	bluerock/bhv/apps/vmm/lib/board/include/aarch64/board_impl_hpp_names.v
-4.49%	98.1	93.7	-4.4	bluerock/bhv/apps/vswitch/proof/model/vswitch/lemmas.v
-4.45%	120.1	114.7	-5.3	bluerock/bhv/lib/socket/proof/socket_defs_hpp_proof.v
-4.45%	180.4	172.4	-8.0	bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_other.v
-4.43%	44.4	42.5	-2.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/templates/verif/pattern.v
-4.41%	192.3	183.8	-8.5	bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/memory_hpp_proof.v
-4.40%	292.9	280.0	-12.9	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/get_set_byte_requesters.v
-4.40%	283.4	270.9	-12.5	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_on.v
-4.35%	122.3	116.9	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0092_cpp_main_proof.v
-4.30%	138.3	132.3	-5.9	bluerock/bhv/zeta/lib/concurrent/proof/ticket_lock_cpp_proof.v
-4.25%	338.9	324.5	-14.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/hints.v
-4.23%	207.5	198.7	-8.8	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/queue/misc.v
-4.20%	153.1	146.7	-6.4	bluerock/bhv/apps/vmm/vml/devices/vuart/proof/seq_queue_proof.v
-4.17%	127.4	122.1	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/const/const_cpp_spec.v
-4.12%	35.1	33.7	-1.4	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/model/virtq/state/descriptor_table.v
-4.09%	159.5	153.0	-6.5	bluerock/bhv/apps/umx/proof/umx_hpp_proof/abspred_instantiations.v
-4.09%	62.6	60.0	-2.6	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/wp.v
-4.09%	62.9	60.3	-2.6	fmdeps/auto/coq-bluerock-auto-core/tests/cancelx/test.v
-4.09%	53.3	51.1	-2.2	fmdeps/auto/coq-bluerock-auto-cpp/theories/bi/monpred_flip.v
-4.08%	41.4	39.8	-1.7	fmdeps/auto/coq-bluerock-auto-core/tests/dnet.v
-4.07%	131.8	126.5	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0052_cpp_main_proof.v
-4.04%	132.6	127.2	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/val_cat/val_cat_cpp_proof.v
-3.99%	43.9	42.1	-1.7	bluerock/NOVA/build-proof/proof/aarch64/interrupt_hpp.v
-3.99%	44.0	42.2	-1.8	bluerock/NOVA/build-proof/proof/aarch64/hip_arch_cpp.v
-3.97%	67.4	64.7	-2.7	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/prepost_loops.v
-3.95%	219.2	210.6	-8.7	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/conclude_chain_use.v
-3.92%	137.5	132.1	-5.4	bluerock/bhv/zeta/lib/lang/proof/bits_hpp_proof.v
-3.90%	62.4	59.9	-2.4	fmdeps/auto/coq-bluerock-auto-cpp/theories/cpp/blockR.v
-3.82%	142.3	136.8	-5.4	bluerock/bhv/zeta/lib/nova/proof/safe_proof/safe_proof.v
-3.77%	523.3	503.6	-19.7	bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/recv.v
-3.75%	44.5	42.9	-1.7	bluerock/NOVA/build-proof/proof/aarch64/smmu_v2_cpp.v
-3.72%	216.1	208.0	-8.0	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/iterator.v
-3.71%	147.5	142.0	-5.5	bluerock/bhv/zeta/lib/alloc/proof/core_hpp_general_proof.v
-3.70%	143.4	138.1	-5.3	bluerock/bhv/zeta/lib/intrusive/proof/refcounted_proof.v
-3.67%	71.4	68.8	-2.6	fmdeps/auto/coq-bluerock-auto-cpp/theories/bi/tls_modalities_rep.v
-3.67%	65.6	63.2	-2.4	fmdeps/auto/coq-bluerock-auto-cpp/theories/bi/tls_modalities.v
-3.64%	45.6	44.0	-1.7	bluerock/NOVA/build-proof/proof/aarch64/scheduler_cpp.v
-3.59%	149.1	143.8	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v
-3.57%	78.8	76.0	-2.8	fmdeps/auto/coq-bluerock-auto-cpp/theories/cpp/slice.v
-3.55%	529.1	510.4	-18.8	bluerock/bhv/apps/vmm/proof/main_cpp_proof/run_vm.v
-3.49%	149.0	143.8	-5.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/templates/splice_cpp_spec.v
-3.48%	154.1	148.7	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v
-3.46%	228.6	220.7	-7.9	bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_read_console_id.v
-3.43%	180.0	173.8	-6.2	bluerock/bhv/zeta/lib/msc/proof/sys/rwlock_hpp_proof.v
-3.41%	251.5	242.9	-8.6	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/TO_UPSTREAM.v
-3.40%	66.8	64.5	-2.3	bluerock/bhv/apps/umx/include/aarch64_uart_hpp.v
-3.39%	66.7	64.5	-2.3	bluerock/bhv/zeta/lib/bhv/include/bhv/aarch64_bhv_hpp.v
-3.37%	357.6	345.6	-12.1	bluerock/bhv/apps/vswitch/lib/vsmp/proof/msg_queue_hpp/proof.v
-3.36%	72.9	70.4	-2.5	fmdeps/auto/coq-bluerock-auto-cpp/theories/base_logic/lib/rinv.v
-3.35%	69.2	66.9	-2.3	bluerock/NOVA/build-proof/proof/aarch64/hip_cpp.v
-3.34%	46.0	44.5	-1.5	bluerock/NOVA/build-proof/proof/aarch64/vmcb_hpp.v
-3.34%	179.2	173.2	-6.0	bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_base_proof.v
-3.33%	333.3	322.2	-11.1	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/resume.v
-3.27%	409.5	396.1	-13.4	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/conclude_chain_use.v
-3.26%	187.1	181.0	-6.1	bluerock/bhv/apps/umx/proof/main_cpp_proof/parse_connect_args.v
-3.24%	199.7	193.2	-6.5	bluerock/bhv/zeta/lib/intrusive/proof/shared_pointer_hpp_proof.v
-3.23%	61.8	59.8	-2.0	fmdeps/auto/coq-bluerock-auto-cpp/tests/micromega/micromega1.v
-3.21%	405.8	392.8	-13.0	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/extract_frame_header.v
-3.19%	338.7	327.9	-10.8	bluerock/bhv/apps/umx/proof/main_cpp_proof/setup.v
-3.17%	75.0	72.6	-2.4	bluerock/NOVA/build-proof/proof/aarch64/gicr_cpp.v
-3.15%	74.7	72.4	-2.4	bluerock/bhv/apps/vmm/include/aarch64_resource_hpp.v
-3.15%	74.7	72.3	-2.3	bluerock/bhv/zeta/lib/porter/include/porter/aarch64_as_resource_hpp.v
-3.15%	87.2	84.4	-2.7	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/switch.v
-3.13%	171.5	166.2	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0068_cpp_main_proof.v
-3.11%	238.0	230.6	-7.4	bluerock/bhv/apps/umx/proof/admin_cpp_proof/read_line.v
-3.10%	46.0	44.6	-1.4	bluerock/NOVA/build-proof/proof/aarch64/acpi_hpp.v
-3.08%	72.3	70.0	-2.2	bluerock/bhv/zeta/lib/zeta/include/zeta/aarch64_zeta_hpp.v
-3.06%	46.1	44.7	-1.4	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_fadt_cpp.v
-3.04%	46.2	44.8	-1.4	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_cpp.v
-3.04%	72.8	70.6	-2.2	bluerock/NOVA/build-proof/proof/aarch64/gicd_cpp.v
-2.99%	79.3	77.0	-2.4	bluerock/NOVA/build-proof/proof/aarch64/interrupt_cpp.v
-2.98%	79.3	76.9	-2.4	bluerock/bhv/zeta/lib/zeta/include/bluerock/zeta/aarch64_semaphore_hpp.v
-2.98%	179.8	174.4	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/data_class/class_32_cpp_proof.v
-2.96%	71.8	69.7	-2.1	bluerock/NOVA/build-proof/proof/aarch64/bootstrap_cpp.v
-2.90%	171.5	166.5	-5.0	fmdeps/auto/coq-bluerock-auto-cpp/tests/fields/test_cpp_proof.v
-2.89%	80.0	77.7	-2.3	bluerock/bhv/zeta/lib/zeta/include/bluerock/zeta/aarch64_mutex_hpp.v
-2.86%	200.8	195.0	-5.7	bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_public.v
-2.84%	83.0	80.6	-2.4	bluerock/NOVA/build-proof/proof/aarch64/cpu_cpp.v
-2.84%	204.6	198.8	-5.8	fmdeps/auto/coq-bluerock-auto-cpp/tests/elpi/enums/variant_cpp_proof.v
-2.83%	395.1	383.9	-11.2	bluerock/bhv/lib/vrl/proof/vrl/dataplane_hpp_proof.v
-2.80%	115.9	112.7	-3.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/big_sep/demo_proof.v
-2.80%	59.3	57.6	-1.7	fmdeps/auto/coq-bluerock-auto-core/tests/cancelx_tactic.v
-2.76%	288.3	280.3	-8.0	bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_pt.v
-2.75%	85.4	83.0	-2.3	bluerock/bhv/lib/drivers/dma/zynqmp_dma/src/aarch64_zynqmp_dma_ver_cpp.v
-2.69%	253.3	246.5	-6.8	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sm.v
-2.68%	47.8	46.5	-1.3	bluerock/NOVA/build-proof/proof/aarch64/init_cpp.v
-2.66%	50.7	49.4	-1.3	bluerock/NOVA/build-proof/proof/aarch64/vmcb_cpp.v
-2.61%	50.7	49.4	-1.3	bluerock/NOVA/build-proof/proof/aarch64/timer_cpp.v
-2.60%	64.9	63.3	-1.7	fmdeps/auto/coq-bluerock-auto-core/theories/internal/instr/paths.v
-2.57%	51.9	50.6	-1.3	bluerock/NOVA/build-proof/proof/aarch64/ec_exc_cpp.v
-2.54%	352.6	343.6	-9.0	bluerock/bhv/apps/umx/proof/main_cpp_proof/input_loop.v
-2.51%	121.2	118.2	-3.0	fmdeps/auto/coq-bluerock-auto-cpp/theories/cpp/array.v
-2.50%	454.3	442.9	-11.3	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sc.v
-2.49%	51.9	50.7	-1.3	bluerock/NOVA/build-proof/proof/aarch64/fdt_cpp.v
-2.47%	49.0	47.8	-1.2	bluerock/NOVA/build-proof/proof/aarch64/acpi_table_madt_cpp.v
-2.46%	261.3	254.9	-6.4	bluerock/bhv/apps/vmm/lib/bluerock/proof/aarch64/reg_accessor_hpp_proof.v
-2.43%	86.2	84.1	-2.1	bluerock/bhv/lib/vrl/include/vrl/aarch64_shared_hpp.v
-2.41%	87.7	85.6	-2.1	bluerock/bhv/apps/vswitch/lib/vsmp/include/vsmp/aarch64_msg_queue_hpp.v
-2.39%	73.0	71.2	-1.7	bluerock/bhv/zeta/lib/porter/include/porter/aarch64_marshal_hpp.v
-2.37%	315.1	307.7	-7.5	bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/mmio.v
-2.37%	975.6	952.5	-23.1	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_cpp_proof.v
-2.36%	88.2	86.1	-2.1	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/atomic/inc_int_cpp.v
-2.36%	76.0	74.2	-1.8	fmdeps/auto/coq-bluerock-auto-core/theories/internal/instr/CancelX.v
-2.35%	678.3	662.4	-15.9	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/copy.v
-2.34%	48.0	46.9	-1.1	bluerock/NOVA/build-proof/proof/aarch64/smmu_v3_cpp.v
-2.33%	75.3	73.6	-1.8	fmdeps/auto-docs/content/demo/forward_list_v1/test_cpp.v
-2.33%	54.4	53.1	-1.3	bluerock/NOVA/build-proof/proof/aarch64/ec_arch_cpp.v
-2.32%	247.3	241.5	-5.7	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/delegate.v
-2.31%	230.1	224.8	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0098_cpp_main_proof.v
-2.30%	47.5	46.4	-1.1	fmdeps/auto/coq-bluerock-auto-core/theories/internal/syntactic_bi/forced/simplify_liftT.v
-2.30%	137.6	134.5	-3.2	fmdeps/auto/coq-bluerock-auto-cpp/tests/lazy_unfold/test1_proof.v
-2.30%	50.7	49.5	-1.2	bluerock/NOVA/build-proof/proof/aarch64/acpi_cpp.v
-2.26%	361.5	353.3	-8.2	bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/schedule.v
-2.15%	92.1	90.1	-2.0	fmdeps/auto/rocq-bluerock-cpp-stdlib/tests/atomic/test_cpp.v
-2.13%	495.5	485.0	-10.5	bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/access.v
-2.12%	249.5	244.2	-5.3	bluerock/bhv/zeta/lib/uuid/proof/uuid_hpp_proof.v
-2.07%	54.3	53.2	-1.1	bluerock/NOVA/build-proof/proof/aarch64/utcb_arch_cpp.v
-2.06%	304.6	298.4	-6.3	bluerock/bhv/lib/drivers/serial/pl011/proof/inversion.v
-2.05%	130.8	128.1	-2.7	fmdeps/auto/coq-bluerock-auto-cpp/theories/auto/cpp/hints/inc_dec.v
-2.03%	191.9	188.0	-3.9	fmdeps/auto/coq-bluerock-auto-cpp/tests/inheritence/demo_cpp_proof.v
-2.01%	763.3	748.0	-15.3	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/setup.v
-2.01%	498.0	488.0	-10.0	bluerock/bhv/apps/vswitch/lib/port/proof/port/proof.v
-2.01%	333.6	326.9	-6.7	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/async_copy_cookie.v
-2.00%	1096.1	1074.2	-21.9	bluerock/bhv/apps/vmm/proof/main_cpp_proof/zeta_main.v
-2.00%	682.6	669.0	-13.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/virtual_interface.v
-1.99%	328.6	322.1	-6.5	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pt.v
-1.99%	55.7	54.6	-1.1	bluerock/NOVA/build-proof/proof/aarch64/pd_cpp.v
-1.99%	188.0	184.2	-3.7	fmdeps/auto/coq-bluerock-auto-cpp/theories/cpp/string.v
-1.98%	55.3	54.2	-1.1	bluerock/NOVA/build-proof/proof/aarch64/gicc_cpp.v
-1.98%	56.1	55.0	-1.1	bluerock/NOVA/build-proof/proof/aarch64/ec_cpp.v
-1.98%	326.3	319.8	-6.5	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pd.v
-1.97%	96.2	94.3	-1.9	bluerock/bhv/apps/vmm/lib/bluerock/include/bluerock/platform/aarch64_rwlock_hpp.v
-1.95%	66.7	65.4	-1.3	fmdeps/auto/coq-bluerock-auto-core/theories/internal/syntactic_bi/forced/lift_exT.v
-1.95%	734.1	719.8	-14.3	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/misc.v
-1.94%	92.5	90.7	-1.8	bluerock/bhv/apps/vmm/lib/bluerock/include/bluerock/platform/aarch64_mutex_hpp.v
-1.93%	92.4	90.6	-1.8	bluerock/bhv/apps/vmm/lib/bluerock/include/bluerock/platform/aarch64_semaphore_hpp.v
-1.93%	91.7	90.0	-1.8	bluerock/bhv/zeta/lib/zeta/include/bluerock/zeta/aarch64_ec_hpp.v
-1.92%	338.8	332.3	-6.5	bluerock/NOVA/build-proof/proof/sm_cpp_proof/dn.v
-1.91%	57.4	56.3	-1.1	bluerock/NOVA/build-proof/proof/aarch64/gich_cpp.v
-1.91%	92.6	90.9	-1.8	bluerock/bhv/zeta/lib/zeta/include/bluerock/zeta/aarch64_timer_hpp.v
-1.91%	92.6	90.8	-1.8	bluerock/bhv/apps/vmm/lib/bluerock/include/bluerock/platform/aarch64_memory_hpp.v
-1.90%	93.4	91.6	-1.8	bluerock/bhv/lib/vconnect/include/vconnect/aarch64_common_hpp.v
-1.89%	96.8	94.9	-1.8	bluerock/bhv/apps/umx/include/aarch64_umx_hpp.v
-1.89%	863.5	847.2	-16.3	bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/proof.v
-1.89%	84.9	83.3	-1.6	bluerock/bhv/zeta/lib/porter/include/porter/aarch64_shareable_hpp.v
-1.88%	96.8	95.0	-1.8	bluerock/bhv/apps/umx/include/aarch64_admin_hpp.v
-1.85%	97.7	95.9	-1.8	bluerock/bhv/apps/umx/src/aarch64_admin_cpp.v
-1.82%	98.0	96.2	-1.8	bluerock/bhv/lib/vrl/include/vrl/aarch64_dataplane_hpp.v
-1.81%	324.4	318.5	-5.9	bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/walk.v
-1.79%	211.7	207.9	-3.8	bluerock/bhv/apps/vswitch/proof/upstream/lemmata.v
-1.79%	378.6	371.8	-6.8	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_sm.v
-1.76%	98.8	97.0	-1.7	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/include/model/aarch64_cpu_hpp.v
-1.75%	426.7	419.2	-7.5	bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_cpp_proof/access.v
-1.74%	100.0	98.3	-1.7	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/src/aarch64_vcpu_roundup_cpp.v
-1.74%	143.2	140.7	-2.5	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/include/vcpu/aarch64_vcpu_base_hpp.v
-1.72%	309.2	303.9	-5.3	fmdeps/auto/coq-bluerock-auto-cpp/tests/hammer_test/tests/test0096_cpp_main_proof.v
-1.70%	499.3	490.8	-8.5	bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_sc.v
-1.69%	146.7	144.3	-2.5	bluerock/bhv/apps/vmm/lib/dynamic_as/include/model/aarch64_guest_chunk_repo_hpp.v
-1.69%	139.8	137.4	-2.4	bluerock/bhv/apps/umx/src/aarch64_main_cpp.v
-1.68%	432.4	425.1	-7.2	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/hints.v
-1.68%	486.2	478.1	-8.1	bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/zynqmp_dma_ver_cpp_proof.v
-1.66%	99.5	97.8	-1.7	bluerock/bhv/lib/vrl/src/aarch64_dataplane_cpp.v
-1.64%	1538.8	1513.5	-25.3	bluerock/bhv/apps/vmm/proof/main_cpp_proof/prepare_address_space.v
-1.61%	337.2	331.7	-5.4	fmdeps/auto/coq-bluerock-auto-cpp/tests/llist/merge_cpp_proof.v
-1.61%	141.2	139.0	-2.3	bluerock/bhv/lib/pm/pm_client_bhv/include/aarch64_dev_client_hpp.v
-1.60%	143.1	140.8	-2.3	bluerock/bhv/lib/ddk/include/ddk/aarch64_mmio_bhv_hpp.v
-1.60%	143.1	140.8	-2.3	bluerock/bhv/lib/ddk/include/ddk/aarch64_interrupt_bhv_hpp.v
-1.58%	333.3	328.0	-5.3	bluerock/bhv/zeta/lib/cxx/proof/sys/semaphore_hpp_proof.v
-1.57%	316.6	311.6	-5.0	fmdeps/auto/coq-bluerock-auto-cpp/tests/perf/read_write_proof.v
-1.53%	780.1	768.1	-11.9	bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_proof.v
-1.50%	379.6	373.9	-5.7	bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_private.v
-1.49%	947.3	933.1	-14.1	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/setup.v
-1.48%	162.6	160.2	-2.4	bluerock/bhv/apps/vswitch/lib/port/include/port/aarch64_port_hpp.v
-1.47%	537.8	529.9	-7.9	bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/ready_queues.v
-1.45%	363.5	358.2	-5.3	bluerock/bhv/zeta/lib/lang/proof/atomic_hpp_proof.v
-1.45%	575.1	566.7	-8.4	bluerock/bhv/apps/umx/proof/main_cpp_proof/scanner_state.v
-1.43%	372.6	367.3	-5.3	fmdeps/auto/rocq-bluerock-cpp-stdlib/tests/cctype/proof.v
-1.39%	166.6	164.2	-2.3	bluerock/bhv/apps/vswitch/lib/forwarding/include/forwarding/aarch64_forwarding_table_hpp.v
-1.38%	476.1	469.5	-6.6	bluerock/bhv/zeta/lib/concurrent/proof/lossy_queue2_hpp_proof.v
-1.36%	1962.1	1935.4	-26.8	bluerock/bhv/apps/vmm/proof/main_cpp_proof/init_vcpus.v
-1.36%	115.7	114.1	-1.6	bluerock/bhv/apps/vmm/lib/bluerock/include/bluerock/aarch64_fdt_hpp.v
-1.36%	118.3	116.7	-1.6	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/include/aarch64/vcpu/msr_bus_hpp.v
-1.35%	118.3	116.7	-1.6	bluerock/bhv/apps/vmm/vml/devices/msr/include/aarch64/msr/msr_hpp.v
-1.34%	145.9	144.0	-2.0	bluerock/bhv/lib/drivers/serial/pl011/src/aarch64_pl011_cpp.v
-1.33%	147.2	145.2	-2.0	bluerock/bhv/lib/vconnect/include/vconnect/aarch64_async_control_hpp.v
-1.33%	154.1	152.0	-2.1	bluerock/bhv/apps/vmm/include/aarch64_initial_setup_hpp.v
-1.33%	91.2	89.9	-1.2	bluerock/NOVA/build-proof/proof/aarch64/syscall_cpp.v
-1.32%	116.1	114.6	-1.5	bluerock/bhv/apps/vmm/vml/devices/gic/include/model/aarch64_gic_hpp.v
-1.31%	144.9	143.0	-1.9	bluerock/bhv/lib/drivers/serial/pl011/include/pl011/aarch64_pl011_hpp.v
-1.31%	103.1	101.7	-1.3	bluerock/bhv/apps/vmm/vml/devices/vbus/include/vbus/aarch64_vbus_hpp.v
-1.29%	528.3	521.5	-6.8	fmdeps/auto/rocq-bluerock-cpp-stdlib/tests/vector/test_cpp_proof.v
-1.27%	104.6	103.3	-1.3	bluerock/bhv/apps/vmm/vml/devices/irq_controller/include/model/aarch64_irq_controller_hpp.v
-1.26%	1153.5	1138.9	-14.6	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v
-1.25%	106.8	105.5	-1.3	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/include/vcpu/aarch64_vcpu_timer_hpp.v
-1.25%	104.2	102.9	-1.3	bluerock/bhv/apps/vmm/vml/devices/vuart/include/vuart/aarch64_vuart_hpp.v
-1.24%	897.9	886.7	-11.2	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_default_impl.v
-1.22%	124.5	123.0	-1.5	bluerock/bhv/apps/sm/smclient/include/sm/aarch64_client_hpp.v
-1.22%	105.4	104.1	-1.3	bluerock/bhv/apps/vmm/vml/devices/timer/include/model/aarch64_timer_hpp.v
-1.21%	101.1	99.8	-1.2	bluerock/bhv/apps/vswitch/lib/acl/include/acl/aarch64_acl_hpp.v
-1.20%	1694.5	1674.1	-20.4	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/reset.v
-1.20%	105.5	104.2	-1.3	bluerock/bhv/zeta/lib/porter/include/porter/aarch64_server_hpp.v
-1.19%	105.9	104.7	-1.3	bluerock/bhv/apps/vmm/vml/devices/timer/include/model/aarch64_aa64_timer_hpp.v
-1.17%	424.4	419.4	-5.0	fmdeps/auto/coq-bluerock-auto-cpp/tests/perf/arith_cpp_proof.v
-1.17%	106.6	105.3	-1.2	bluerock/bhv/apps/vmm/vml/devices/vpl011/include/pl011/aarch64_pl011_hpp.v
-1.16%	106.1	104.8	-1.2	bluerock/bhv/apps/vmm/vml/devices/vbus/src/aarch64_vbus_cpp.v
-1.15%	554.9	548.6	-6.4	bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_pd.v
-1.13%	522.5	516.6	-5.9	bluerock/bhv/lib/drivers/serial/pl011/proof/pl011_cpp_proof.v
-1.11%	106.0	104.9	-1.2	bluerock/bhv/apps/vmm/vml/devices/simple_as/include/model/aarch64_simple_as_hpp.v
-1.11%	106.0	104.8	-1.2	bluerock/bhv/apps/vmm/vml/devices/msr/include/msr/aarch64_msr_base_hpp.v
-1.11%	113.7	112.5	-1.3	bluerock/bhv/apps/vmm/lib/pagetable/src/aarch64_pagetable_cpp.v
-1.10%	108.2	107.0	-1.2	bluerock/bhv/apps/vmm/lib/vmi_interface/include/vmi_interface/aarch64_vmi_interface_hpp.v
-1.10%	106.3	105.1	-1.2	bluerock/bhv/apps/vmm/lib/dynamic_as/include/model/aarch64_guest_as_hpp.v
-1.10%	108.5	107.3	-1.2	bluerock/bhv/apps/vmm/lib/outpost_dummy/include/outpost/aarch64_outpost_hpp.v
-1.10%	108.2	107.0	-1.2	bluerock/bhv/apps/vmm/vml/devices/msr/src/aarch64_msr_base_cpp.v
-1.10%	582.9	576.5	-6.4	bluerock/bhv/apps/vmm/src/aarch64_main_cpp.v
-1.09%	648.3	641.2	-7.1	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/misc.v
-1.06%	100.1	99.0	-1.1	fmdeps/auto/coq-bluerock-auto-core/theories/internal/syntactic_bi/forced/resolve_liftT.v
-1.03%	109.5	108.4	-1.1	bluerock/bhv/apps/vmm/vml/devices/vpl011/src/aarch64_pl011_cpp.v
-1.03%	154.3	152.7	-1.6	bluerock/bhv/apps/vmm/lib/board/include/model/aarch64_board_hpp.v
-1.01%	113.1	112.0	-1.1	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/include/aarch64_portal_hpp.v
-1.00%	113.7	112.6	-1.1	bluerock/bhv/lib/ddk/include/ddk/aarch64_chardev_hpp.v
-0.99%	1160.7	1149.2	-11.5	bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/reset_cpu.v
-0.96%	258.7	256.2	-2.5	bluerock/bhv/apps/vmm/lib/dynamic_as/src/aarch64_space_view_cpp.v
-0.96%	116.7	115.6	-1.1	bluerock/bhv/lib/vconnect/include/vconnect/aarch64_guest_as_hpp.v
-0.91%	1950.0	1932.3	-17.8	bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v
-0.89%	1197.7	1187.1	-10.6	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/sync_impl.v
-0.80%	440.9	437.3	-3.5	fmdeps/auto/coq-bluerock-auto-cpp/tests/big_sep/test1_proof.v
-0.78%	280.5	278.3	-2.2	bluerock/bhv/apps/vmm/lib/vcpu_bluerock/src/aarch64/vmexit_cpp.v
-0.74%	201.3	199.8	-1.5	fmdeps/auto/coq-bluerock-auto-core/tests/subgoals.v
-0.72%	685.5	680.5	-5.0	fmdeps/auto/coq-bluerock-auto-cpp/tests/perf/call_cpp_proof.v
-0.68%	679.4	674.8	-4.6	fmdeps/auto/coq-bluerock-auto-cpp/tests/llist_cpp/forward_list_hpp_proof.v
-0.56%	191.7	190.6	-1.1	bluerock/bhv/zeta/apps/msc/include/msc/aarch64_hp_hpp.v
-0.53%	969.9	964.7	-5.2	fmdeps/auto/rocq-bluerock-cpp-stdlib/tests/atomic/test_cpp_proof.v
-0.41%	371.0	369.5	-1.5	fmdeps/auto/rocq-bluerock-cpp-stdlib/theories/vector/inc_vector_cpp.v
-0.40%	519.2	517.2	-2.1	bluerock/bhv/apps/vmm/lib/board/src/aarch64/board_cpp.v
-0.36%	1678.2	1672.2	-6.0	bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_glue.v
+14.30%	10.1	11.5	+1.4	fmdeps/auto/coq-bluerock-auto-core/theories/internal/ltac2_dnet.v
-7.88%	132896.5	122422.2	-10474.3	total
-2.73%	24267.3	24949.7	-682.4	├ translation units
-9.07%	98154.8	107946.8	-9791.9	└ proofs and tests