Repository navigation
Adapt for the stdpp/iris bump. - #236
Merged
Merged
Conversation
rlepigre-skylabs-ai
force-pushed
the
rodolphe/bump-stdpp-and-iris
branch
from
October 27, 2026 14:02
c20d0c3 to
0688abb
Compare
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | 781c507 |
| fmdeps/auto-docs/ | main | 918aa33 |
| fmdeps/brick-libgtest/ | main | 495b855 |
| fmdeps/ci/ | main | b480641 |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| vendored/rocq/ | skylabs-master | 7c6eef8 |
| vendored/rocq-elpi/ | skylabs-master | 7dee592 |
| vendored/rocq-equations/ | skylabs-main | 9cf8471 |
| vendored/rocq-stdlib/ | skylabs-master | 00897b3 |
| vendored/vsrocq/ | skylabs-main | 03db19e |
Changes in Warnings or Errors
| Before | New | Fixed | After | |
|---|---|---|---|---|
| Errors | 0 | 0 | 1 | |
| Warnings | 77 | 76 |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.82% | 197274.4 | 198901.7 | +1627.3 | total |
| -0.17% | 327.0 | - | -327.0 | ├ disappeared files (1) |
| +0.00% | - | 4.9 | +4.9 | ├ newly appeared files (1) |
| +0.99% | 196947.4 | 198896.8 | +1949.3 | └ common files |
| +0.03% | 49381.4 | 49396.3 | +14.9 | ├ translation units |
| +1.31% | 147566.1 | 149500.5 | +1934.4 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -45.12% | 18.2 | 10.0 | -8.2 | fmdeps/auto/rocq-skylabs-auto-core/theories/internal/ltac2_dnet.v |
| -8.96% | 375.2 | 341.6 | -33.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arith_bug.v |
| -8.42% | 13.8 | 12.6 | -1.2 | bluerock/bhv/apps/vmm/lib/bluerock/proof/aarch64/nova_reg_utils.v |
| -3.08% | 148.0 | 143.5 | -4.6 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/invoke.v |
| -1.70% | 424.8 | 417.6 | -7.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/iostream/inc_iostream_cpp_templates.v |
| -0.85% | 339.9 | 337.0 | -2.9 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/string/erase_out_of_range_cpp.v |
| -0.22% | 506.1 | 505.0 | -1.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/memory/inc_hpp.v |
| -0.18% | 600.0 | 598.9 | -1.1 | fmdeps/auto/rocq-skylabs-cpp-stdlib/theories/vector/inc_vector_cpp.v |
| +0.17% | 1830.4 | 1833.5 | +3.1 | fmdeps/brick-libgtest/proof/gtest/inc_gtest_cpp.v |
| +0.31% | 1737.9 | 1743.3 | +5.4 | bluerock/NOVA/build-proof/proof/arch/ptab_hpt_cpp_proof/update_tmp.v |
| +0.34% | 1067.6 | 1071.3 | +3.6 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/iostream_trace/extract.v |
| +0.34% | 1079.1 | 1082.9 | +3.7 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/iostream/two_ints.v |
| +0.42% | 286.5 | 287.6 | +1.2 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/hints.v |
| +0.46% | 323.3 | 324.8 | +1.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp_proof.v |
| +0.47% | 726.9 | 730.3 | +3.4 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/cctype/proof.v |
| +0.47% | 232.7 | 233.8 | +1.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays.v |
| +0.47% | 758.1 | 761.7 | +3.6 | fmdeps/brick-libgtest/test/gtest/proof/proof/bounds.v |
| +0.48% | 434.5 | 436.6 | +2.1 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/iter_bounds.v |
| +0.48% | 268.1 | 269.4 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_main_proof.v |
| +0.48% | 681.1 | 684.4 | +3.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/call_cpp_proof.v |
| +0.49% | 514.4 | 517.0 | +2.5 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_sc.v |
| +0.50% | 222.0 | 223.1 | +1.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/AddArrays_WhileTrueWithBreak.v |
| +0.53% | 857.7 | 862.3 | +4.6 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/reset_cpu.v |
| +0.56% | 380.7 | 382.9 | +2.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/arith_cpp_proof.v |
| +0.58% | 782.7 | 787.2 | +4.5 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/setup.v |
| +0.58% | 303.8 | 305.5 | +1.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/read_write_proof.v |
| +0.59% | 1381.4 | 1389.5 | +8.1 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/reset.v |
| +0.60% | 371.6 | 373.8 | +2.2 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_obj.v |
| +0.63% | 301.7 | 303.6 | +1.9 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_dma.v |
| +0.64% | 599.3 | 603.1 | +3.8 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/data_class/dataclass_hpp_spec.v |
| +0.67% | 561.9 | 565.6 | +3.7 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/spec.v |
| +0.67% | 153.9 | 155.0 | +1.0 | fmdeps/brick-libgtest/test/gtest/proof/proof/arith.v |
| +0.68% | 328.6 | 330.8 | +2.2 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_pt.v |
| +0.68% | 234.2 | 235.8 | +1.6 | bluerock/bhv/apps/vmm/proof/main_cpp_spec.v |
| +0.69% | 271.6 | 273.5 | +1.9 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_sm.v |
| +0.71% | 270.7 | 272.6 | +1.9 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_gst.v |
| +0.72% | 387.9 | 390.8 | +2.8 | fmdeps/auto/brick_groundtruth/examples/loopsynth/downward_loop.v |
| +0.73% | 172.9 | 174.2 | +1.3 | bluerock/NOVA/build-proof/proof/arch/ptab_hpt_hpp_spec.v |
| +0.74% | 1366.0 | 1376.1 | +10.1 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/prepare_address_space.v |
| +0.74% | 138.1 | 139.2 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v |
| +0.74% | 244.7 | 246.5 | +1.8 | fmdeps/brick-libgtest/test/gtest/proof/proof/fatal.v |
| +0.75% | 1515.3 | 1526.7 | +11.4 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_glue.v |
| +0.77% | 327.1 | 329.6 | +2.5 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pt.v |
| +0.77% | 447.3 | 450.8 | +3.5 | bluerock/NOVA/build-proof/proof/arch/syscall_cpp_proof/sys_create_pd.v |
| +0.78% | 328.3 | 330.9 | +2.6 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_sm.v |
| +0.79% | 242.7 | 244.6 | +1.9 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/delegate.v |
| +0.81% | 240.9 | 242.8 | +1.9 | fmdeps/auto/brick_groundtruth/examples/loopsynth/qtest_5_failure.v |
| +0.81% | 221.7 | 223.5 | +1.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/hints.v |
| +0.83% | 319.0 | 321.7 | +2.7 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/handle_data_abort.v |
| +0.85% | 130.7 | 131.8 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/defs.v |
| +0.85% | 159.4 | 160.7 | +1.4 | fmdeps/brick-libgtest/test/gtest/proof/proof/order.v |
| +0.85% | 155.0 | 156.4 | +1.3 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/check_reset.v |
| +0.85% | 205.7 | 207.4 | +1.8 | fmdeps/brick-libgtest/test/gtest/proof/proof/canon.v |
| +0.86% | 121.6 | 122.7 | +1.0 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_pt.v |
| +0.86% | 458.6 | 462.6 | +3.9 | bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/recv.v |
| +0.86% | 462.2 | 466.1 | +4.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/test1_proof.v |
| +0.87% | 130.3 | 131.4 | +1.1 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command.v |
| +0.87% | 133.2 | 134.4 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/destructuring/test_pair.v |
| +0.87% | 324.6 | 327.4 | +2.8 | bluerock/NOVA/build-proof/proof/sm_cpp_proof/dn.v |
| +0.88% | 144.6 | 145.9 | +1.3 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/mutex/test_cpp_proof.v |
| +0.89% | 213.3 | 215.2 | +1.9 | bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/msr_hpp_proof.v |
| +0.90% | 886.8 | 894.7 | +7.9 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/zeta_main.v |
| +0.91% | 529.7 | 534.5 | +4.8 | bluerock/NOVA/build-proof/proof/arch/syscall_cpp_proof/sys_create_sc.v |
| +0.91% | 295.0 | 297.7 | +2.7 | bluerock/bhv/apps/umx/proof/main_cpp_proof/input_loop.v |
| +0.92% | 162.2 | 163.7 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/splice_cpp_spec.v |
| +0.92% | 797.8 | 805.1 | +7.3 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/compare/test_cpp_proof.v |
| +0.92% | 302.2 | 305.0 | +2.8 | bluerock/bhv/apps/umx/proof/main_cpp_proof/setup.v |
| +0.92% | 149.9 | 151.3 | +1.4 | fmdeps/auto/rocq-skylabs-auto-core/tests/subgoals.v |
| +0.92% | 371.9 | 375.4 | +3.4 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_hst.v |
| +0.93% | 347.8 | 351.0 | +3.2 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/schedule.v |
| +0.93% | 181.4 | 183.1 | +1.7 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/ctor.v |
| +0.95% | 181.0 | 182.7 | +1.7 | fmdeps/brick-libgtest/test/gtest/proof/proof/versions.v |
| +0.96% | 386.4 | 390.1 | +3.7 | bluerock/NOVA/build-proof/proof/arch/space_hst_cpp_proof/create.v |
| +0.96% | 1249.3 | 1261.3 | +12.0 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/MultipleLoops.v |
| +0.96% | 172.6 | 174.3 | +1.7 | bluerock/bhv/apps/umx/proof/main_cpp_proof/parse_connect_args.v |
| +0.96% | 126.3 | 127.5 | +1.2 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/proof.v |
| +0.97% | 133.8 | 135.1 | +1.3 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_roundedup.v |
| +0.98% | 776.0 | 783.6 | +7.6 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/compare/test_cpp_proof.v |
| +0.98% | 302.3 | 305.3 | +3.0 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/resume.v |
| +0.98% | 196.0 | 197.9 | +1.9 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_main_proof.v |
| +0.99% | 164.4 | 166.1 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/new_delete.v |
| +1.00% | 1524.9 | 1540.1 | +15.2 | bluerock/NOVA/build-proof/proof/arch/ptab_hpt_cpp_proof/walk_tmp.v |
| +1.00% | 122.5 | 123.7 | +1.2 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_off.v |
| +1.00% | 173.4 | 175.2 | +1.7 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/set_virtio_net_header.v |
| +1.01% | 684.9 | 691.8 | +6.9 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_pd.v |
| +1.01% | 396.5 | 400.5 | +4.0 | bluerock/NOVA/build-proof/proof/arch/space_gst_cpp_proof/create.v |
| +1.01% | 99.4 | 100.5 | +1.0 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/emulation.v |
| +1.02% | 144.3 | 145.8 | +1.5 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_other.v |
| +1.02% | 100.1 | 101.1 | +1.0 | bluerock/bhv/apps/vswitch/proof/ghost.v |
| +1.02% | 200.6 | 202.7 | +2.0 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort_to_vbus.v |
| +1.02% | 145.7 | 147.2 | +1.5 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/devq/send.v |
| +1.03% | 789.4 | 797.5 | +8.1 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_cpp_proof.v |
| +1.03% | 135.0 | 136.3 | +1.4 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/defs.v |
| +1.04% | 110.6 | 111.8 | +1.1 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_sc.v |
| +1.05% | 1148.5 | 1160.6 | +12.0 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/sync_impl.v |
| +1.05% | 752.4 | 760.3 | +7.9 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/array/test_cpp_proof.v |
| +1.06% | 238.2 | 240.7 | +2.5 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_on.v |
| +1.06% | 288.0 | 291.1 | +3.1 | bluerock/NOVA/build-proof/proof/arch/syscall_cpp_proof/sys_create_sm.v |
| +1.06% | 130.3 | 131.7 | +1.4 | bluerock/bhv/apps/vmm/vml/devices/msr/proof/msr_base_hpp_spec.v |
| +1.07% | 122.8 | 124.1 | +1.3 | bluerock/bhv/zeta/lib/zeta/proof/semaphore_hpp_proof.v |
| +1.07% | 114.6 | 115.8 | +1.2 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_emulating.v |
| +1.08% | 587.5 | 593.8 | +6.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist_cpp/forward_list_hpp_proof.v |
| +1.08% | 153.6 | 155.2 | +1.7 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/wait_if_exec_paused.v |
| +1.08% | 210.3 | 212.6 | +2.3 | bluerock/NOVA/build-proof/proof/sc_cpp_proof/create.v |
| +1.09% | 99.8 | 100.8 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/route.v |
| +1.09% | 120.4 | 121.7 | +1.3 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/atomic/test_cpp_proof.v |
| +1.09% | 188.1 | 190.2 | +2.1 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/roundup_impl.v |
| +1.09% | 98.9 | 100.0 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/compound_assignment_increments.v |
| +1.10% | 454.4 | 459.4 | +5.0 | bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_private.v |
| +1.10% | 476.3 | 481.6 | +5.3 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/vector/test_cpp_proof.v |
| +1.12% | 272.3 | 275.3 | +3.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/proof.v |
| +1.12% | 164.6 | 166.5 | +1.8 | bluerock/NOVA/build-proof/proof/pt_cpp_proof/create.v |
| +1.14% | 204.8 | 207.1 | +2.3 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/read_line.v |
| +1.14% | 117.3 | 118.6 | +1.3 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/string/test_cpp_proof.v |
| +1.14% | 671.1 | 678.8 | +7.7 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v |
| +1.15% | 144.0 | 145.7 | +1.7 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/reset.v |
| +1.15% | 118.4 | 119.7 | +1.4 | fmdeps/brick-libgtest/test/gtest/proof/proof/colors.v |
| +1.15% | 188.6 | 190.8 | +2.2 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_read_console_id.v |
| +1.16% | 99.3 | 100.5 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/demo_proof.v |
| +1.17% | 87.1 | 88.1 | +1.0 | fmdeps/BRiCk/rocq-skylabs-brick/theories/lang/cpp/logic/func.v |
| +1.17% | 116.6 | 117.9 | +1.4 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/model/cpu_hpp_spec.v |
| +1.17% | 273.3 | 276.5 | +3.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/fixed_regression_tests/atomic_exchange_void/atomic_exchange_void.v |
| +1.18% | 112.3 | 113.6 | +1.3 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/atomic/test_cpp_proof.v |
| +1.19% | 210.5 | 213.0 | +2.5 | bluerock/NOVA/build-proof/proof/arch/ptab_hpt_cpp_proof/hpt_tmp.v |
| +1.19% | 684.6 | 692.7 | +8.1 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/setup.v |
| +1.19% | 115.6 | 117.0 | +1.4 | fmdeps/brick-libgtest/test/gtest/proof/proof/levels.v |
| +1.21% | 483.5 | 489.3 | +5.8 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/run_vm.v |
| +1.21% | 171.6 | 173.7 | +2.1 | bluerock/NOVA/build-proof/proof/sm_cpp_proof/create.v |
| +1.22% | 182.6 | 184.8 | +2.2 | bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_cpp_proof/space_sel.v |
| +1.22% | 141.3 | 143.0 | +1.7 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/compute_gpa_fault_addr.v |
| +1.23% | 357.8 | 362.2 | +4.4 | bluerock/bhv/lib/vrl/proof/vrl/dataplane_hpp_proof.v |
| +1.23% | 175.4 | 177.6 | +2.2 | bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/memory_hpp_proof.v |
| +1.24% | 341.6 | 345.9 | +4.2 | bluerock/NOVA/build-proof/proof/slab_cpp_proof/free.v |
| +1.24% | 109.6 | 110.9 | +1.4 | bluerock/NOVA/build-proof/proof/sm_cpp_proof/up.v |
| +1.25% | 104.1 | 105.4 | +1.3 | bluerock/NOVA/build-proof/proof/ptab_hpp_spec/cmra.v |
| +1.26% | 111.0 | 112.4 | +1.4 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/CountPositives_DoWhile.v |
| +1.26% | 347.1 | 351.4 | +4.4 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/extract_frame_header.v |
| +1.26% | 88.1 | 89.2 | +1.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/FindMax.v |
| +1.27% | 429.9 | 435.4 | +5.5 | bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/access.v |
| +1.27% | 293.9 | 297.6 | +3.7 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create.v |
| +1.28% | 89.7 | 90.9 | +1.1 | bluerock/bhv/zeta/lib/cxx/proof/bitset_hpp_proof.v |
| +1.28% | 193.3 | 195.8 | +2.5 | bluerock/NOVA/build-proof/proof/slab_cpp_proof/alloc.v |
| +1.28% | 106.0 | 107.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/dataclass_demo/dataclass_demo.v |
| +1.30% | 184.4 | 186.8 | +2.4 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/create_forwarding_plane.v |
| +1.30% | 80.0 | 81.1 | +1.0 | bluerock/NOVA/build-proof/proof/scheduler_hpp_spec/abs_pred.v |
| +1.30% | 175.3 | 177.6 | +2.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/inheritence/demo_cpp_proof.v |
| +1.32% | 82.2 | 83.3 | +1.1 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/wp_vcpu/hints.v |
| +1.32% | 86.0 | 87.1 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/data_class/dataclass_hpp_spec2.v |
| +1.35% | 1897.0 | 1922.6 | +25.6 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/cstring/proof.v |
| +1.35% | 1833.4 | 1858.2 | +24.8 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/init_vcpus.v |
| +1.35% | 309.4 | 313.6 | +4.2 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort.v |
| +1.35% | 422.2 | 427.9 | +5.7 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/msr_framework.v |
| +1.36% | 166.3 | 168.6 | +2.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/data_class/class_32_cpp_proof.v |
| +1.36% | 87.4 | 88.6 | +1.2 | bluerock/NOVA/build-proof/proof/soup/abs_pred.v |
| +1.36% | 213.3 | 216.2 | +2.9 | bluerock/bhv/zeta/lib/uuid/proof/uuid_hpp_proof.v |
| +1.37% | 576.2 | 584.1 | +7.9 | bluerock/bhv/apps/umx/proof/main_cpp_proof/scanner_state.v |
| +1.38% | 200.9 | 203.7 | +2.8 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/create.v |
| +1.39% | 130.1 | 131.9 | +1.8 | bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/msr_cpp_proof.v |
| +1.39% | 247.5 | 250.9 | +3.4 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/wp_path.v |
| +1.40% | 74.5 | 75.6 | +1.0 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/TO_UPSTREAM.v |
| +1.40% | 120.2 | 121.9 | +1.7 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/arguments.v |
| +1.40% | 690.0 | 699.7 | +9.7 | fmdeps/auto/brick_groundtruth/examples/loopsynth/za18_2.v |
| +1.40% | 83.8 | 85.0 | +1.2 | bluerock/bhv/apps/vswitch/lib/port/proof/port/hints.v |
| +1.42% | 78.8 | 79.9 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/virtual/virtual_destructor_cpp_proof.v |
| +1.42% | 364.1 | 369.3 | +5.2 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_pd.v |
| +1.43% | 194.1 | 196.8 | +2.8 | bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_public.v |
| +1.44% | 72.7 | 73.7 | +1.0 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/FindFirst_EarlyExitFromWhile.v |
| +1.44% | 78.2 | 79.3 | +1.1 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/release_queue.v |
| +1.44% | 209.4 | 212.5 | +3.0 | bluerock/NOVA/build-proof/proof/pt_cpp_proof/proof.v |
| +1.45% | 228.2 | 231.5 | +3.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/flood.v |
| +1.46% | 529.0 | 536.7 | +7.7 | fmdeps/auto/brick_groundtruth/examples/loopsynth/Exp1_0_failure.v |
| +1.46% | 234.4 | 237.8 | +3.4 | bluerock/bhv/apps/vmm/lib/bluerock/proof/aarch64/reg_accessor_hpp_proof.v |
| +1.46% | 109.7 | 111.3 | +1.6 | fmdeps/brick-libgtest/test/gtest/proof/proof/signs.v |
| +1.47% | 70.5 | 71.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/pure_virtual_dispatch/pure_virtual_dispatch.v |
| +1.48% | 77.6 | 78.7 | +1.1 | bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_hpp_spec/space_view_invs.v |
| +1.49% | 131.5 | 133.5 | +2.0 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/handle_msr_exit.v |
| +1.49% | 75.8 | 76.9 | +1.1 | fmdeps/brick-libgtest/test/gtest/proof/proof/nullptr.v |
| +1.50% | 75.7 | 76.9 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/pkt.v |
| +1.51% | 84.3 | 85.6 | +1.3 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/initializer_list/test_cpp_proof.v |
| +1.52% | 155.9 | 158.3 | +2.4 | bluerock/NOVA/build-proof/proof/iface/hypercall/pd.v |
| +1.53% | 276.4 | 280.7 | +4.2 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/wp_vcpu_lemmas.v |
| +1.54% | 66.6 | 67.6 | +1.0 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/hints.v |
| +1.54% | 119.6 | 121.5 | +1.8 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/init_info.v |
| +1.55% | 125.7 | 127.7 | +1.9 | bluerock/bhv/zeta/lib/lang/proof/bits_hpp_proof.v |
| +1.55% | 66.2 | 67.2 | +1.0 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/create_hints.v |
| +1.56% | 72.4 | 73.6 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/conditional/bit_cast_nan/bit_cast_nan.v |
| +1.57% | 692.6 | 703.4 | +10.9 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/identityloop.v |
| +1.57% | 134.5 | 136.6 | +2.1 | bluerock/bhv/zeta/lib/alloc/proof/core_hpp_general_proof.v |
| +1.57% | 132.9 | 135.0 | +2.1 | fmdeps/auto/brick_groundtruth/examples/loopsynth/replicate_example_0.v |
| +1.57% | 277.0 | 281.4 | +4.4 | bluerock/bhv/lib/drivers/serial/pl011/proof/pl011_cpp_proof.v |
| +1.58% | 164.2 | 166.8 | +2.6 | bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/proof.v |
| +1.59% | 1026.5 | 1042.8 | +16.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v |
| +1.60% | 79.3 | 80.5 | +1.3 | bluerock/bhv/lib/drivers/serial/pl011/proof/compatible.v |
| +1.60% | 724.1 | 735.7 | +11.6 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/proof.v |
| +1.61% | 80.2 | 81.5 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/inheritance_if_style_hpp_spec.v |
| +1.61% | 120.1 | 122.0 | +1.9 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/spec.v |
| +1.63% | 73.5 | 74.7 | +1.2 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_finish.v |
| +1.63% | 84.5 | 85.9 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/pair_hpp_spec.v |
| +1.64% | 91.2 | 92.7 | +1.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/drop.v |
| +1.64% | 164.7 | 167.4 | +2.7 | bluerock/NOVA/build-proof/proof/slab_cpp_proof/slab.v |
| +1.64% | 326.3 | 331.6 | +5.3 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/joinpoint_tests.v |
| +1.64% | 155.5 | 158.0 | +2.6 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof.v |
| +1.65% | 117.6 | 119.6 | +1.9 | bluerock/NOVA/build-proof/proof/pd_hpp_spec/hints.v |
| +1.65% | 280.7 | 285.3 | +4.6 | bluerock/NOVA/build-proof/proof/ptab_cpp_proof/walk.v |
| +1.65% | 106.7 | 108.5 | +1.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/util.v |
| +1.66% | 97.4 | 99.0 | +1.6 | bluerock/NOVA/build-proof/proof/iface/predicates/core.v |
| +1.67% | 94.5 | 96.1 | +1.6 | bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_other.v |
| +1.68% | 91.8 | 93.4 | +1.5 | bluerock/NOVA/build-proof/proof/ec_hpp_spec/active_pred.v |
| +1.68% | 174.2 | 177.1 | +2.9 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/elpi/enums/variant_cpp_proof.v |
| +1.68% | 84.3 | 85.7 | +1.4 | bluerock/NOVA/build-proof/proof/slab_cpp_proof/hints.v |
| +1.69% | 84.4 | 85.8 | +1.4 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/roundup_parallel_proof.v |
| +1.69% | 799.1 | 812.6 | +13.5 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_default_impl.v |
| +1.70% | 514.5 | 523.2 | +8.7 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/ready_queues.v |
| +1.70% | 85.1 | 86.6 | +1.4 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayCopy_WhileTrueWithBreak.v |
| +1.70% | 180.0 | 183.0 | +3.1 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/conclude_chain_use.v |
| +1.70% | 111.2 | 113.1 | +1.9 | bluerock/NOVA/build-proof/proof/slab_cpp_proof/metadata.v |
| +1.70% | 239.5 | 243.6 | +4.1 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/TO_UPSTREAM.v |
| +1.70% | 147.8 | 150.3 | +2.5 | bluerock/bhv/apps/vmm/vml/devices/vuart/proof/seq_queue_proof.v |
| +1.71% | 359.2 | 365.3 | +6.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/conclude_chain_use.v |
| +1.71% | 188.5 | 191.7 | +3.2 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/iterator.v |
| +1.71% | 112.0 | 113.9 | +1.9 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/model/cpu_hpp_properties.v |
| +1.72% | 88.3 | 89.9 | +1.5 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctrl_feature_off.v |
| +1.73% | 427.4 | 434.8 | +7.4 | bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/zynqmp_dma_ver_cpp_proof.v |
| +1.75% | 60.6 | 61.7 | +1.1 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/hints.v |
| +1.76% | 78.5 | 79.9 | +1.4 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_cpp_proof/proof.v |
| +1.76% | 258.5 | 263.1 | +4.5 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/new/demo_cpp_proof.v |
| +1.77% | 138.1 | 140.6 | +2.4 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/walk_chain.v |
| +1.77% | 106.3 | 108.2 | +1.9 | bluerock/bhv/lib/vrl/proof/vrl/port_hpp_spec.v |
| +1.77% | 105.8 | 107.6 | +1.9 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayReverseCopy.v |
| +1.78% | 118.7 | 120.8 | +2.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/const/const_cpp_spec.v |
| +1.78% | 324.9 | 330.7 | +5.8 | bluerock/bhv/apps/vmm/proof/main_cpp_proof.v |
| +1.78% | 129.0 | 131.3 | +2.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtual_interface.v |
| +1.79% | 70.1 | 71.4 | +1.3 | bluerock/NOVA/build-proof/proof/timeout_cpp_proof/client_dequeue.v |
| +1.79% | 72.5 | 73.8 | +1.3 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/FindFirst_EarlyExit.v |
| +1.79% | 146.9 | 149.6 | +2.6 | bluerock/NOVA/build-proof/proof/arch/intid_hpp_proof.v |
| +1.79% | 76.9 | 78.3 | +1.4 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/ghost.v |
| +1.80% | 128.9 | 131.2 | +2.3 | bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxclient/move_assignment.v |
| +1.80% | 318.3 | 324.0 | +5.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/merge_cpp_proof.v |
| +1.80% | 104.8 | 106.7 | +1.9 | bluerock/bhv/zeta/lib/cxx/proof/tagged_ptr_hpp_proof.v |
| +1.81% | 96.0 | 97.8 | +1.7 | bluerock/bhv/lib/vrl/proof/vrl/port_hpp_proof.v |
| +1.81% | 250.5 | 255.1 | +4.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/get_set_byte_requesters.v |
| +1.83% | 92.7 | 94.4 | +1.7 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/destructuring_declarations.v |
| +1.83% | 542.0 | 552.0 | +9.9 | bluerock/NOVA/build-proof/proof/syscall_hpp_proof.v |
| +1.83% | 137.1 | 139.7 | +2.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/lazy_unfold/test1_proof.v |
| +1.84% | 59.0 | 60.0 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/packet_ctor.v |
| +1.84% | 113.2 | 115.3 | +2.1 | bluerock/NOVA/build-proof/proof/timeout_cpp_proof/enqueue.v |
| +1.85% | 72.2 | 73.6 | +1.3 | fmdeps/BRiCk/rocq-skylabs-iris/theories/bi/monpred_na_invariants.v |
| +1.85% | 134.7 | 137.2 | +2.5 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/inc_dec.v |
| +1.87% | 85.5 | 87.1 | +1.6 | bluerock/bhv/apps/vmm/lib/vm_config/proof/bson_config_hpp_spec.v |
| +1.88% | 177.5 | 180.8 | +3.3 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/update.v |
| +1.88% | 136.0 | 138.6 | +2.6 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/defs.v |
| +1.89% | 62.8 | 64.0 | +1.2 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/mutex/spec/recursive_mutex.v |
| +1.90% | 130.6 | 133.1 | +2.5 | bluerock/bhv/zeta/lib/nova/proof/safe_proof/safe_proof.v |
| +1.91% | 469.6 | 478.6 | +9.0 | bluerock/bhv/zeta/lib/concurrent/proof/lossy_queue2_hpp_proof.v |
| +1.92% | 92.5 | 94.3 | +1.8 | fmdeps/auto-docs/content/demo/basic/main_cpp_proof.v |
| +1.94% | 53.7 | 54.7 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/base_tail_padding/witness.v |
| +1.95% | 104.4 | 106.4 | +2.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/fupd/inc_twice_hpp_spec.v |
| +1.95% | 112.2 | 114.4 | +2.2 | fmdeps/skylabs-fm/rocq-brick-status/tests/basic.v |
| +1.95% | 107.8 | 109.9 | +2.1 | bluerock/bhv/zeta/lib/concurrent/proof/ticket_lock_cpp_proof.v |
| +1.95% | 162.2 | 165.3 | +3.2 | bluerock/bhv/zeta/lib/msc/proof/sys/rwlock_hpp_proof.v |
| +1.95% | 673.2 | 686.4 | +13.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/misc.v |
| +1.96% | 82.5 | 84.1 | +1.6 | bluerock/NOVA/build-proof/proof/sc_hpp_spec/triples.v |
| +1.96% | 106.7 | 108.8 | +2.1 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayReverseCopy_WhileTrueWithBreak.v |
| +1.97% | 462.4 | 471.6 | +9.1 | bluerock/bhv/apps/vswitch/lib/port/proof/port/proof.v |
| +1.97% | 65.7 | 67.0 | +1.3 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/devq/misc.v |
| +1.97% | 77.4 | 79.0 | +1.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/vrl_hints.v |
| +2.00% | 115.7 | 118.1 | +2.3 | bluerock/bhv/zeta/lib/msc/proof/sys/signal_hpp_proof.v |
| +2.00% | 50.3 | 51.3 | +1.0 | bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxclient/helpers.v |
| +2.00% | 69.7 | 71.1 | +1.4 | fmdeps/auto-docs/content/demo/linked_list/linked_list_cpp_proof.v |
| +2.01% | 75.9 | 77.4 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/nrvo_elision/nrvo_elision.v |
| +2.01% | 195.1 | 199.1 | +3.9 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/defs.v |
| +2.03% | 79.3 | 80.9 | +1.6 | bluerock/bhv/zeta/lib/lang/proof/endian16_hpp_proof.v |
| +2.03% | 58.2 | 59.4 | +1.2 | bluerock/bhv/zeta/lib/lang/proof/endian32_hpp_proof.v |
| +2.04% | 62.1 | 63.4 | +1.3 | bluerock/bhv/zeta/lib/lang/proof/endian8_hpp_proof.v |
| +2.06% | 740.1 | 755.3 | +15.2 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_proof.v |
| +2.06% | 86.6 | 88.4 | +1.8 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/hints.v |
| +2.06% | 304.7 | 310.9 | +6.3 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/string/inc_string_cpp_templates.v |
| +2.07% | 313.5 | 319.9 | +6.5 | bluerock/bhv/zeta/lib/cxx/proof/sys/semaphore_hpp_proof.v |
| +2.07% | 60.1 | 61.4 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/data_class/class_16_cpp_proof.v |
| +2.10% | 99.7 | 101.8 | +2.1 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/insert.v |
| +2.11% | 72.8 | 74.4 | +1.5 | fmdeps/auto/rocq-skylabs-auto-core/theories/internal/instr/CancelX.v |
| +2.15% | 731.5 | 747.2 | +15.7 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/misc.v |
| +2.16% | 180.2 | 184.1 | +3.9 | bluerock/NOVA/build-proof/proof/ec_proof/status_accessors.v |
| +2.16% | 329.9 | 337.1 | +7.1 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/walk.v |
| +2.17% | 179.5 | 183.4 | +3.9 | bluerock/bhv/zeta/lib/intrusive/proof/shared_pointer_hpp_proof.v |
| +2.17% | 80.9 | 82.7 | +1.8 | bluerock/NOVA/build-proof/proof/timeout_cpp_proof/private_dequeue.v |
| +2.18% | 83.0 | 84.8 | +1.8 | fmdeps/BRiCk/rocq-skylabs-brick/theories/lang/cpp/logic/initializers.v |
| +2.19% | 120.7 | 123.3 | +2.6 | fmdeps/brick-libgtest/test/client/client_cpp_proof.v |
| +2.20% | 140.4 | 143.4 | +3.1 | bluerock/bhv/lib/drivers/serial/pl011/proof/mmio.v |
| +2.21% | 106.6 | 108.9 | +2.4 | bluerock/bhv/lib/socket/proof/socket_defs_hpp_proof.v |
| +2.21% | 51.4 | 52.5 | +1.1 | bluerock/bhv/zeta/lib/nova/proof/safe_proof/hypercall_au_lemmas.v |
| +2.22% | 75.1 | 76.7 | +1.7 | bluerock/NOVA/build-proof/proof/sc_cpp_proof/proof.v |
| +2.23% | 335.7 | 343.2 | +7.5 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/string/test_cpp.v |
| +2.23% | 116.0 | 118.6 | +2.6 | bluerock/NOVA/build-proof/proof/ec_hpp_spec/cont_pred.v |
| +2.24% | 57.4 | 58.7 | +1.3 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/desc_metadata.v |
| +2.27% | 292.8 | 299.5 | +6.6 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/hints.v |
| +2.28% | 111.4 | 114.0 | +2.5 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/requesters.v |
| +2.30% | 155.6 | 159.2 | +3.6 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/lookup.v |
| +2.32% | 58.3 | 59.7 | +1.4 | bluerock/NOVA/build-proof/proof/timeout_cpp_proof/hints.v |
| +2.32% | 105.2 | 107.7 | +2.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/list_cpp_proof.v |
| +2.33% | 88.0 | 90.1 | +2.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/devq/used_event_notify.v |
| +2.33% | 50.5 | 51.7 | +1.2 | fmdeps/auto/brick_groundtruth/examples/ownership_disciplines/field_sharing_protocol_cpp_proof.v |
| +2.34% | 520.9 | 533.1 | +12.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/virtual_interface.v |
| +2.34% | 53.1 | 54.3 | +1.2 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/roundup_proofs_combined.v |
| +2.36% | 181.3 | 185.6 | +4.3 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/queue/misc.v |
| +2.37% | 64.7 | 66.2 | +1.5 | bluerock/NOVA/build-proof/proof/ptab_cpp_proof/update.v |
| +2.40% | 52.1 | 53.4 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/specifications.v |
| +2.42% | 150.7 | 154.3 | +3.7 | bluerock/bhv/apps/umx/proof/umx_hpp_proof/abspred_instantiations.v |
| +2.45% | 108.5 | 111.2 | +2.7 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/spec.v |
| +2.45% | 44.6 | 45.7 | +1.1 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctrl_feature_reset.v |
| +2.45% | 624.6 | 639.9 | +15.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/copy.v |
| +2.45% | 125.2 | 128.3 | +3.1 | bluerock/NOVA/build-proof/proof/ptab_cpp_proof/table.v |
| +2.47% | 72.4 | 74.2 | +1.8 | fmdeps/auto/rocq-skylabs-auto-core/theories/internal/syntactic_bi/forced/resolve_liftT.v |
| +2.48% | 164.4 | 168.5 | +4.1 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_base_proof.v |
| +2.49% | 41.4 | 42.5 | +1.0 | bluerock/bhv/zeta/lib/lang/proof/memory_barrier.v |
| +2.49% | 97.9 | 100.3 | +2.4 | bluerock/bhv/zeta/lib/lang/proof/string_cpp_proof.v |
| +2.51% | 107.8 | 110.5 | +2.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/unit_tests.v |
| +2.52% | 94.6 | 97.0 | +2.4 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_proof.v |
| +2.53% | 246.3 | 252.5 | +6.2 | bluerock/bhv/apps/vswitch/lib/port/proof/port/defs.v |
| +2.54% | 309.9 | 317.8 | +7.9 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/async_copy_cookie.v |
| +2.55% | 85.9 | 88.1 | +2.2 | bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxshared/signals.v |
| +2.59% | 89.5 | 91.8 | +2.3 | fmdeps/BRiCk/rocq-skylabs-brick/theories/lang/cpp/logic/destroy.v |
| +2.61% | 99.3 | 101.9 | +2.6 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/cast.v |
| +2.61% | 101.1 | 103.7 | +2.6 | bluerock/NOVA/build-proof/proof/ec_hpp_spec/const_pred.v |
| +2.63% | 53.1 | 54.5 | +1.4 | fmdeps/BRiCk/rocq-skylabs-brick/theories/lang/cpp/logic/wp.v |
| +2.66% | 135.8 | 139.4 | +3.6 | bluerock/bhv/zeta/lib/intrusive/proof/refcounted_proof.v |
| +2.70% | 51.6 | 53.0 | +1.4 | bluerock/bhv/apps/umx/proof/queue.v |
| +2.70% | 112.8 | 115.8 | +3.1 | bluerock/NOVA/build-proof/proof/arch/regs_hpp_proof.v |
| +2.74% | 50.2 | 51.5 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/lazy/big_sep/instances.v |
| +2.75% | 136.3 | 140.0 | +3.8 | bluerock/bhv/zeta/lib/concurrent/proof/lock_hpp_proof.v |
| +2.76% | 55.1 | 56.6 | +1.5 | bluerock/NOVA/build-proof/proof/cpu_hpp_spec/cls.v |
| +2.78% | 210.0 | 215.8 | +5.8 | bluerock/bhv/apps/vswitch/proof/upstream/lemmata.v |
| +2.80% | 329.3 | 338.6 | +9.2 | bluerock/bhv/zeta/lib/lang/proof/atomic_hpp_proof.v |
| +2.82% | 141.8 | 145.8 | +4.0 | bluerock/bhv/apps/vmm/vml/devices/gic/proof/model/gic_hpp_spec.v |
| +2.84% | 255.8 | 263.0 | +7.3 | bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/mmio.v |
| +2.85% | 37.9 | 39.0 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/delayed_case.v |
| +2.89% | 71.2 | 73.2 | +2.1 | fmdeps/BRiCk/rocq-skylabs-brick/theories/lang/cpp/model/simple_pred.v |
| +2.89% | 77.9 | 80.1 | +2.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/basic.v |
| +2.93% | 39.9 | 41.1 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/lazy/big_sep/lemmas.v |
| +2.93% | 73.1 | 75.3 | +2.1 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/base_logic/lib/rinv.v |
| +2.98% | 127.9 | 131.7 | +3.8 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/val_cat/val_cat_cpp_proof.v |
| +3.00% | 100.1 | 103.1 | +3.0 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_rich_proof.v |
| +3.01% | 45.7 | 47.1 | +1.4 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/model/cpu_feature_hpp_spec.v |
| +3.05% | 43.1 | 44.4 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/bi/monpred_flip.v |
| +3.07% | 61.1 | 63.0 | +1.9 | fmdeps/auto/rocq-skylabs-cpp-stdlib/theories/iterator/spec.v |
| +3.08% | 61.1 | 63.0 | +1.9 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/iterator/spec.v |
| +3.11% | 85.7 | 88.4 | +2.7 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayCopy_DownwardForLoop.v |
| +3.14% | 58.8 | 60.6 | +1.8 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/prepost_loops.v |
| +3.18% | 32.8 | 33.9 | +1.0 | bluerock/NOVA/build-proof/proof/cpp/rep.v |
| +3.27% | 87.0 | 89.9 | +2.8 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/switch.v |
| +3.33% | 85.0 | 87.9 | +2.8 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/ArrayCopy_While.v |
| +3.55% | 1832.2 | 1897.2 | +65.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v |
| +3.70% | 52.7 | 54.6 | +1.9 | fmdeps/BRiCk/rocq-skylabs-brick/theories/lang/cpp/logic/heap_pred/everywhere.v |
| +3.70% | 29.3 | 30.4 | +1.1 | bluerock/bhv/lib/vrl/proof/vrl/port_map_hints.v |
| +3.74% | 397.6 | 412.5 | +14.9 | bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_cpp_proof/access.v |
| +3.76% | 29.2 | 30.3 | +1.1 | fmdeps/BRiCk/rocq-skylabs-brick/theories/lang/cpp/logic/heap_pred/any.v |
| +3.80% | 64.4 | 66.9 | +2.4 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/wp.v |
| +3.92% | 77.9 | 81.0 | +3.1 | fmdeps/BRiCk/rocq-skylabs-iris/theories/base_logic/lib/spectra.v |
| +3.97% | 63.4 | 65.9 | +2.5 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/bi/tls_modalities_rep.v |
| +4.01% | 54.4 | 56.6 | +2.2 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/pretty/my_pretty_internals.v |
| +4.05% | 189.4 | 197.1 | +7.7 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/cpp/string.v |
| +4.06% | 55.3 | 57.5 | +2.2 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/lib/pred_utils.v |
| +4.20% | 125.1 | 130.3 | +5.2 | bluerock/NOVA/build-proof/proof/ec_hpp_spec/sched_pred.v |
| +4.23% | 42.2 | 44.0 | +1.8 | fmdeps/BRiCk/rocq-skylabs-brick/theories/lang/cpp/logic/zstring.v |
| +4.24% | 85.6 | 89.2 | +3.6 | fmdeps/BRiCk/rocq-skylabs-brick/theories/lang/cpp/logic/object_repr.v |
| +4.38% | 64.3 | 67.2 | +2.8 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/cpp/blockR.v |
| +4.44% | 73.1 | 76.4 | +3.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/unsound/global_delete_virtual/global_delete_virtual.v |
| +4.45% | 32.0 | 33.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/lazy/lazy_unfold.v |
| +4.58% | 128.5 | 134.3 | +5.9 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/cpp/array.v |
| +4.62% | 106.3 | 111.2 | +4.9 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/cpp/slice.v |
| +4.63% | 41.4 | 43.4 | +1.9 | fmdeps/BRiCk/rocq-skylabs-brick/theories/lang/cpp/logic/rep.v |
| +4.67% | 39.5 | 41.3 | +1.8 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/multiborrow.v |
| +4.76% | 34.6 | 36.2 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/initialize.v |
| +4.90% | 31.3 | 32.8 | +1.5 | bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/spec.v |
| +4.90% | 40.7 | 42.7 | +2.0 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/lazy/auto_frac/hints.v |
| +4.92% | 78.1 | 82.0 | +3.8 | fmdeps/BRiCk/rocq-skylabs-brick/theories/lang/cpp/logic/arr.v |
| +5.03% | 51.7 | 54.3 | +2.6 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/operators.v |
| +5.15% | 41.2 | 43.4 | +2.1 | fmdeps/BRiCk/rocq-skylabs-brick/tests/array_block_layout.v |
| +5.18% | 38.4 | 40.4 | +2.0 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/layout.v |
| +5.22% | 38.9 | 40.9 | +2.0 | fmdeps/BRiCk/rocq-skylabs-brick/theories/lang/cpp/logic/rep_proofmode.v |
| +5.36% | 61.5 | 64.8 | +3.3 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/lazy/big_sep/array.v |
| +5.40% | 19.6 | 20.7 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/tactics/wapply.v |
| +5.53% | 57.1 | 60.3 | +3.2 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/bi/tls_modalities.v |
| +5.60% | 20.7 | 21.8 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arith/mod_tests.v |
| +5.91% | 68.8 | 72.9 | +4.1 | fmdeps/auto/rocq-skylabs-auto-core/theories/internal/instr/paths.v |
| +6.08% | 24.1 | 25.6 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/ptrs/valid.v |
| +6.76% | 41.0 | 43.8 | +2.8 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/inc_twice_hpp_proof.v |
| +6.76% | 14.8 | 15.8 | +1.0 | fmdeps/auto/rocq-skylabs-auto-core/theories/internal/instr/cmd.v |
| +8.20% | 14.2 | 15.4 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/base_logic/lib/darray.v |
| +8.62% | 12.6 | 13.7 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/hints/kont.v |
| +8.66% | 38.9 | 42.2 | +3.4 | bluerock/bhv/lib/ddk/proof/iris_device_wp.v |
| +10.00% | 12.2 | 13.5 | +1.2 | fmdeps/BRiCk/rocq-skylabs-brick/theories/lang/cpp/model/operator.v |
| +10.23% | 32.9 | 36.3 | +3.4 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/spec.v |
| +10.43% | 17.3 | 19.1 | +1.8 | bluerock/NOVA/build-proof/proof/iface/predicates/ec_regs_aarch64.v |
| +10.57% | 17.2 | 19.0 | +1.8 | bluerock/NOVA/build-proof/proof/iface/predicates/ec_regs_x86_64.v |
| +10.71% | 9.9 | 10.9 | +1.1 | fmdeps/BRiCk/rocq-skylabs-iris/theories/bi/invariants.v |
| +10.82% | 24.8 | 27.5 | +2.7 | fmdeps/BRiCk/rocq-skylabs-iris/theories/bi/atomic_update_properties.v |
| +11.63% | 13.7 | 15.3 | +1.6 | bluerock/bhv/lib/pm/pm_bhv/proof/info_hpp_spec.v |
| +11.93% | 19.1 | 21.4 | +2.3 | bluerock/NOVA/build-proof/proof/mtd_arch_hpp_spec.v |
| +12.03% | 20.0 | 22.4 | +2.4 | bluerock/NOVA/build-proof/proof/space_pio_hpp_spec/triples.v |
| +12.25% | 13.7 | 15.4 | +1.7 | bluerock/bhv/zeta/lib/alloc/proof/sels_hpp_spec.v |
| +12.74% | 12.6 | 14.2 | +1.6 | fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/atomic/spec.v |
| +12.86% | 14.0 | 15.8 | +1.8 | fmdeps/BRiCk/rocq-skylabs-iris/theories/wp_io/refinement/wp_io.v |
| +13.24% | 19.4 | 22.0 | +2.6 | bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/signal_hpp_proof.v |
| +13.57% | 18.4 | 20.9 | +2.5 | bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/msr_info_hpp_spec.v |
| +13.61% | 9.3 | 10.6 | +1.3 | fmdeps/BRiCk/rocq-skylabs-brick/theories/lang/cpp/bi/cfractional.v |
| +13.66% | 14.4 | 16.4 | +2.0 | bluerock/NOVA/build-proof/proof/ec_hpp_spec/regs_triples.v |
| +14.46% | 47.7 | 54.6 | +6.9 | fmdeps/BRiCk/rocq-skylabs-iris/theories/wp_io/wp_io_compose.v |
| +16.09% | 15.6 | 18.1 | +2.5 | bluerock/bhv/lib/vconnect/proof/vconnect/async_control_hpp/prelude/defs.v |
| +19.32% | 12.5 | 14.9 | +2.4 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/auto/cpp/hints/ptrs/valid_type_ptr.v |
| +39.57% | 14.7 | 20.5 | +5.8 | fmdeps/auto/rocq-skylabs-auto-core/theories/internal/instr/Fwd.v |
| +52.87% | 33.7 | 51.5 | +17.8 | fmdeps/auto/brick_groundtruth/examples/loopcorpus/IntegerDivide_WhileTrueWithBreak.v |
| +95.49% | 169.6 | 331.5 | +161.9 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/initialize_dataplane.v |
| +0.82% | 197274.4 | 198901.7 | +1627.3 | total |
| -0.17% | 327.0 | - | -327.0 | ├ disappeared files (1) |
| +0.00% | - | 4.9 | +4.9 | ├ newly appeared files (1) |
| +0.99% | 196947.4 | 198896.8 | +1949.3 | └ common files |
| +0.03% | 49381.4 | 49396.3 | +14.9 | ├ translation units |
| +1.31% | 147566.1 | 149500.5 | +1934.4 | └ proofs and tests |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.