Test cbn delayed subst#14
Draft
Janno wants to merge 1 commit into
Draft
Conversation
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | 7d2ee30 |
| fmdeps/BRiCk/ | main | e64ccd1 |
| fmdeps/auto/ | main | a3a993e |
| fmdeps/auto-docs/ | main | d4c3641 |
| bluerock/NOVA/ | skylabs-proof | 8d011de |
| bluerock/bhv/ | skylabs-main | 6a61dd6 |
| fmdeps/brick-libcpp/ | main | a20f555 |
| fmdeps/ci/ | main | e54841c |
| vendored/elpi/ | skylabs-master | aa4475f |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| fmdeps/fm-tools/ | main | c1e387f |
| psi/protos/ | main | 8fe3e7c |
| psi/backend/ | main | 0b5fea6 |
| psi/ide/ | main | 6b596cf |
| psi/data/ | main | 42bb988 |
| fmdeps/rocq-agent-toolkit/ | main | 3eed23a |
| vendored/rocq-elpi/ | skylabs-master | 103a742 |
| vendored/rocq-equations/ | skylabs-main | a8c4832 |
| vendored/rocq-ext-lib/ | skylabs-master | 94a6630 |
| vendored/rocq-iris/ | skylabs-master | 3ad4ddd |
| vendored/rocq-lsp/ | skylabs-main | a8b7272 |
| vendored/rocq-stdlib/ | skylabs-master | bc07423 |
| vendored/rocq-stdpp/ | skylabs-master | e01d802 |
| fmdeps/skylabs-fm/ | main | 6ca56d6 |
| vendored/vsrocq/ | skylabs-main | 5b4527e |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.34% | 134466.5 | 134005.2 | -461.4 | total |
| -0.01% | 27548.3 | 27551.8 | -3.5 | ├ translation units |
| -0.43% | 106456.9 | 106914.7 | -457.8 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -45.10% | 17.9 | 9.8 | -8.1 | fmdeps/auto/rocq-skylabs-auto-core/theories/internal/ltac2_dnet.v |
| -18.86% | 56.5 | 45.8 | -10.7 | fmdeps/auto/rocq-skylabs-auto-core/tests/cancelx_tactic.v |
| -8.72% | 50.4 | 46.0 | -4.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep_spec.v |
| -8.63% | 65.4 | 59.8 | -5.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/pair_hpp_spec.v |
| -7.94% | 16.6 | 15.3 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/includes/A_cpp_proof.v |
| -7.82% | 21.8 | 20.1 | -1.7 | bluerock/bhv/zeta/lib/alloc/proof/core_proof_utils.v |
| -7.64% | 46.9 | 43.3 | -3.6 | bluerock/bhv/apps/vswitch/proof/model/ethernet.v |
| -7.29% | 89.7 | 83.2 | -6.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/send.v |
| -6.79% | 27.6 | 25.7 | -1.9 | bluerock/bhv/zeta/lib/lang/proof/page_hpp_proof.v |
| -6.73% | 59.0 | 55.1 | -4.0 | bluerock/bhv/zeta/lib/lang/proof/errno_hpp_proof.v |
| -6.33% | 16.4 | 15.4 | -1.0 | bluerock/bhv/zeta/lib/lang/proof/util.v |
| -5.49% | 145.2 | 137.2 | -8.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/splice_cpp_spec.v |
| -5.29% | 1243.9 | 1178.1 | -65.8 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/sync_impl.v |
| -5.07% | 52.2 | 49.5 | -2.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/initlist_cpp_proof.v |
| -4.92% | 30.2 | 28.7 | -1.5 | bluerock/bhv/zeta/lib/cxx/proof/range_hpp_spec.v |
| -3.61% | 35.2 | 33.9 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/default_specs_1.v |
| -3.56% | 42.4 | 40.9 | -1.5 | bluerock/bhv/zeta/lib/cxx/proof/sys/lock_guard_hpp_proof.v |
| -3.37% | 81.2 | 78.4 | -2.7 | bluerock/bhv/apps/umx/proof/main_cpp_proof/setup_sigs.v |
| -3.27% | 529.5 | 512.1 | -17.3 | bluerock/bhv/lib/drivers/serial/pl011/proof/pl011_cpp_proof.v |
| -3.26% | 85.3 | 82.5 | -2.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/drop.v |
| -3.11% | 138.5 | 134.2 | -4.3 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/proof.v |
| -2.85% | 231.5 | 224.9 | -6.6 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort_to_vbus.v |
| -2.60% | 189.4 | 184.4 | -4.9 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/initialize_dataplane.v |
| -2.57% | 340.9 | 332.2 | -8.8 | bluerock/bhv/apps/umx/proof/main_cpp_proof/setup.v |
| -2.46% | 103.6 | 101.0 | -2.5 | bluerock/bhv/lib/vrl/proof/vrl/port_hpp_proof.v |
| -2.28% | 492.5 | 481.3 | -11.2 | bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/access.v |
| -2.24% | 151.8 | 148.4 | -3.4 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/compute_gpa_fault_addr.v |
| -2.22% | 49.1 | 48.0 | -1.1 | bluerock/bhv/apps/umx/proof/main_cpp_proof/setup_output_loop_thread.v |
| -2.14% | 191.0 | 186.9 | -4.1 | bluerock/bhv/apps/umx/proof/main_cpp_proof/parse_connect_args.v |
| -2.12% | 1701.0 | 1665.0 | -36.1 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_glue.v |
| -2.10% | 99.8 | 97.7 | -2.1 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/start_cpu.v |
| -2.08% | 114.9 | 112.5 | -2.4 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_rich_proof.v |
| -2.08% | 486.4 | 476.3 | -10.1 | bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/zynqmp_dma_ver_cpp_proof.v |
| -2.06% | 862.6 | 844.8 | -17.8 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/proof.v |
| -1.94% | 476.9 | 467.7 | -9.3 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/msr_framework.v |
| -1.89% | 1865.1 | 1829.8 | -35.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v |
| -1.86% | 690.0 | 677.1 | -12.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/virtual_interface.v |
| -1.81% | 90.7 | 89.0 | -1.6 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctor.v |
| -1.69% | 1158.9 | 1139.3 | -19.6 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v |
| -1.67% | 192.2 | 189.0 | -3.2 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/create_forwarding_plane.v |
| -1.62% | 728.5 | 716.7 | -11.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/misc.v |
| -1.56% | 194.1 | 191.1 | -3.0 | bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_cpp_proof/space_sel.v |
| -1.55% | 191.3 | 188.4 | -3.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/set_virtio_net_header.v |
| -1.53% | 361.4 | 355.9 | -5.5 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/handle_data_abort.v |
| -1.52% | 108.9 | 107.2 | -1.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/list_cpp_proof.v |
| -1.51% | 117.0 | 115.3 | -1.8 | bluerock/bhv/lib/socket/proof/socket_defs_hpp_proof.v |
| -1.49% | 82.2 | 81.0 | -1.2 | bluerock/bhv/zeta/lib/cxx/proof/sys/mutex_hpp_proof.v |
| -1.49% | 170.9 | 168.4 | -2.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/fields/test_cpp_proof.v |
| -1.45% | 156.9 | 154.6 | -2.3 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_roundedup.v |
| -1.41% | 104.2 | 102.7 | -1.5 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_proof.v |
| -1.38% | 394.9 | 389.4 | -5.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/extract_frame_header.v |
| -1.30% | 359.4 | 354.7 | -4.7 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort.v |
| -1.29% | 349.9 | 345.4 | -4.5 | bluerock/bhv/apps/vswitch/lib/vsmp/proof/msg_queue_hpp/proof.v |
| -1.29% | 96.1 | 94.9 | -1.2 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/get_fdt_from_uuid.v |
| -1.27% | 178.1 | 175.9 | -2.3 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_base_proof.v |
| -1.20% | 146.9 | 145.1 | -1.8 | bluerock/bhv/zeta/lib/zeta/proof/semaphore_hpp_proof.v |
| -1.08% | 498.3 | 492.9 | -5.4 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/vector/test_cpp_proof.v |
| -0.98% | 277.6 | 274.9 | -2.7 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create.v |
| -0.97% | 261.3 | 258.8 | -2.5 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sm.v |
| -0.93% | 171.0 | 169.4 | -1.6 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_other.v |
| -0.89% | 515.1 | 510.5 | -4.6 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/run_vm.v |
| -0.87% | 202.1 | 200.3 | -1.8 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/elpi/enums/variant_cpp_proof.v |
| -0.85% | 201.8 | 200.1 | -1.7 | bluerock/NOVA/build-proof/proof/sc_cpp_proof/create.v |
| -0.84% | 259.5 | 257.3 | -2.2 | bluerock/bhv/apps/vmm/lib/bluerock/proof/aarch64/reg_accessor_hpp_proof.v |
| -0.82% | 226.5 | 224.7 | -1.9 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_read_console_id.v |
| -0.82% | 1970.9 | 1954.8 | -16.2 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/init_vcpus.v |
| -0.81% | 240.7 | 238.7 | -1.9 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/flood.v |
| -0.80% | 140.9 | 139.7 | -1.1 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_off.v |
| -0.76% | 365.9 | 363.1 | -2.8 | bluerock/bhv/zeta/lib/lang/proof/atomic_hpp_proof.v |
| -0.73% | 1093.2 | 1085.2 | -8.0 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/zeta_main.v |
| -0.71% | 180.8 | 179.5 | -1.3 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/spec.v |
| -0.71% | 179.3 | 178.1 | -1.3 | bluerock/bhv/zeta/lib/msc/proof/sys/rwlock_hpp_proof.v |
| -0.70% | 212.3 | 210.8 | -1.5 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/ctor.v |
| -0.70% | 176.9 | 175.7 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/data_class/class_32_cpp_proof.v |
| -0.69% | 464.7 | 461.5 | -3.2 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pd.v |
| -0.68% | 198.2 | 196.8 | -1.3 | bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_public.v |
| -0.68% | 389.9 | 387.3 | -2.6 | bluerock/bhv/lib/vrl/proof/vrl/dataplane_hpp_proof.v |
| -0.66% | 347.8 | 345.5 | -2.3 | bluerock/bhv/apps/umx/proof/main_cpp_proof/input_loop.v |
| -0.63% | 1530.2 | 1520.6 | -9.6 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/prepare_address_space.v |
| -0.61% | 326.6 | 324.6 | -2.0 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/resume.v |
| -0.59% | 492.6 | 489.7 | -2.9 | bluerock/bhv/apps/vswitch/lib/port/proof/port/proof.v |
| -0.56% | 239.6 | 238.2 | -1.3 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/read_line.v |
| -0.56% | 555.1 | 552.0 | -3.1 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sc.v |
| -0.56% | 196.4 | 195.3 | -1.1 | bluerock/bhv/zeta/lib/intrusive/proof/shared_pointer_hpp_proof.v |
| -0.55% | 1695.8 | 1686.5 | -9.3 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/reset.v |
| -0.53% | 202.2 | 201.1 | -1.1 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/queue/misc.v |
| -0.52% | 196.8 | 195.8 | -1.0 | bluerock/bhv/apps/vswitch/lib/port/include/port/aarch64_port_hpp.v |
| -0.52% | 943.3 | 938.4 | -4.9 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/setup.v |
| -0.51% | 276.5 | 275.0 | -1.4 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_on.v |
| -0.51% | 267.5 | 266.2 | -1.4 | bluerock/bhv/apps/vswitch/lib/vswitch/src/aarch64_vswitch_cpp.v |
| -0.50% | 651.4 | 648.2 | -3.3 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/misc.v |
| -0.49% | 222.6 | 221.5 | -1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/include/forwarding/aarch64_forwarding_plane_hpp.v |
| -0.48% | 977.2 | 972.5 | -4.7 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_cpp_proof.v |
| -0.47% | 465.8 | 463.6 | -2.2 | bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_private.v |
| -0.44% | 231.7 | 230.7 | -1.0 | bluerock/bhv/apps/umx/proof/main_cpp_proof/user_handler.v |
| -0.43% | 306.2 | 304.9 | -1.3 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pt.v |
| -0.42% | 561.3 | 558.9 | -2.4 | bluerock/bhv/apps/vmm/lib/board/src/x86/board_cpp.v |
| -0.41% | 760.4 | 757.3 | -3.1 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/setup.v |
| -0.40% | 632.6 | 630.1 | -2.5 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/vector/test_cpp.v |
| -0.38% | 362.2 | 360.8 | -1.4 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/schedule.v |
| -0.32% | 534.1 | 532.4 | -1.7 | bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/recv.v |
| -0.30% | 782.1 | 779.8 | -2.3 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_proof.v |
| -0.29% | 381.0 | 379.9 | -1.1 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_sm.v |
| -0.26% | 676.1 | 674.3 | -1.8 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist_cpp/forward_list_hpp_proof.v |
| -0.23% | 539.5 | 538.3 | -1.2 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/ready_queues.v |
| -0.17% | 619.9 | 618.8 | -1.1 | bluerock/bhv/apps/umx/proof/main_cpp_proof/scanner_state.v |
| +0.12% | 896.4 | 897.5 | +1.1 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/atomic/test_cpp_proof.v |
| +0.17% | 906.0 | 907.5 | +1.6 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_default_impl.v |
| +0.25% | 669.6 | 671.3 | +1.7 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/copy.v |
| +0.30% | 686.3 | 688.4 | +2.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/call_cpp_proof.v |
| +0.38% | 431.1 | 432.8 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/arith_cpp_proof.v |
| +0.44% | 410.5 | 412.3 | +1.8 | bluerock/bhv/apps/vmm/lib/board/include/model/aarch64_board_common_hpp.v |
| +0.50% | 264.6 | 266.0 | +1.3 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/src/aarch64_vcpu_base_cpp.v |
| +0.65% | 163.0 | 164.0 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_binary_operators.v |
| +0.75% | 281.0 | 283.1 | +2.1 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/delegate.v |
| +0.90% | 127.4 | 128.5 | +1.2 | bluerock/bhv/apps/vmm/vml/devices/vuart/include/vuart/aarch64_vuart_hpp.v |
| +1.01% | 148.4 | 149.9 | +1.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/misc_hints.v |
| +1.02% | 112.6 | 113.8 | +1.2 | bluerock/bhv/apps/vmm/lib/bluerock/include/bluerock/platform/aarch64_memory_hpp.v |
| +1.11% | 170.8 | 172.7 | +1.9 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_rounding_mode.v |
| +1.15% | 88.3 | 89.3 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_main_proof.v |
| +1.25% | 303.7 | 307.5 | +3.8 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_main_proof.v |
| +1.38% | 212.7 | 215.7 | +2.9 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_main_proof.v |
| +1.45% | 81.3 | 82.5 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0099_cpp_main_proof.v |
| +1.70% | 112.7 | 114.6 | +1.9 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_main_proof.v |
| +1.70% | 82.7 | 84.2 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_main_proof.v |
| +1.70% | 156.9 | 159.5 | +2.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_main_proof.v |
| +1.83% | 123.1 | 125.3 | +2.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_main_proof.v |
| +1.84% | 76.2 | 77.6 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_main_proof.v |
| +1.88% | 62.0 | 63.2 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/read_prim/read_cpp_proof.v |
| +1.92% | 144.5 | 147.2 | +2.8 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v |
| +1.98% | 74.9 | 76.3 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0084_cpp_main_proof.v |
| +2.01% | 64.5 | 65.8 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/x86_64/inheritance_arch_hpp_spec.v |
| +2.08% | 117.7 | 120.1 | +2.4 | bluerock/bhv/apps/umx/include/aarch64_umx_hpp.v |
| +2.09% | 141.6 | 144.5 | +3.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v |
| +2.29% | 58.7 | 60.0 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/aarch64/inheritance_arch_hpp_spec.v |
| +2.37% | 59.3 | 60.7 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0088_cpp_main_proof.v |
| +2.38% | 43.0 | 44.1 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/auto_frac/anyR_proof.v |
| +2.38% | 49.0 | 50.1 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/data_class/dataclass_hpp_proof.v |
| +2.82% | 57.7 | 59.4 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f2_proof.v |
| +2.89% | 42.9 | 44.1 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/control_flow/main_cpp_spec.v |
| +2.98% | 44.8 | 46.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/inits/main_cpp_spec.v |
| +2.99% | 34.6 | 35.7 | +1.0 | bluerock/NOVA/build-proof/proof/iface/predicates/ec.v |
| +3.02% | 36.5 | 37.6 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/smoke.v |
| +3.13% | 34.4 | 35.5 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/sizeof_alignof.v |
| +3.37% | 54.8 | 56.7 | +1.8 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_f0_proof.v |
| +3.62% | 37.3 | 38.6 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/anyR_proof.v |
| +3.69% | 30.6 | 31.8 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0099_cpp_f0_proof.v |
| +3.71% | 30.2 | 31.3 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f1_proof.v |
| +3.77% | 43.3 | 44.9 | +1.6 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/utility/test_cpp_proof.v |
| +3.88% | 41.8 | 43.4 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f2_proof.v |
| +3.93% | 32.5 | 33.8 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/sem_const/constructor.v |
| +4.08% | 33.1 | 34.4 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/control_logical_forms.v |
| +4.13% | 34.1 | 35.5 | +1.4 | fmdeps/auto-docs/content/docs/functions/verification.v |
| +4.15% | 24.1 | 25.1 | +1.0 | bluerock/NOVA/build-proof/proof/iface/predicates/dma.v |
| +4.31% | 27.1 | 28.3 | +1.2 | bluerock/NOVA/build-proof/proof/iface/predicates/sc.v |
| +4.38% | 26.5 | 27.7 | +1.2 | bluerock/NOVA/build-proof/proof/iface/predicates/mem.v |
| +4.41% | 30.5 | 31.8 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/implicit_array_initialization.v |
| +4.43% | 31.5 | 32.9 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/arrays.v |
| +4.48% | 31.7 | 33.1 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f3_proof.v |
| +4.48% | 25.7 | 26.9 | +1.2 | bluerock/NOVA/build-proof/proof/iface/predicates/pd.v |
| +4.52% | 26.4 | 27.6 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f0_proof.v |
| +4.63% | 31.7 | 33.1 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_f0_proof.v |
| +5.01% | 33.6 | 35.3 | +1.7 | bluerock/NOVA/build-proof/proof/kmem_hpp_spec.v |
| +5.13% | 21.3 | 22.4 | +1.1 | fmdeps/auto-docs/content/docs/class_reps/alt.v |
| +5.22% | 26.1 | 27.5 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/factor.v |
| +5.26% | 25.8 | 27.2 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f3_proof.v |
| +5.38% | 19.1 | 20.1 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f1_proof.v |
| +5.40% | 19.3 | 20.4 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_f0_proof.v |
| +5.45% | 27.4 | 28.9 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f0_proof.v |
| +5.47% | 19.5 | 20.6 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f2_proof.v |
| +5.48% | 19.3 | 20.4 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f1_proof.v |
| +5.51% | 23.8 | 25.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/constructor.v |
| +5.58% | 26.2 | 27.6 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f0_proof.v |
| +5.66% | 20.2 | 21.4 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/normalization/test.v |
| +5.73% | 18.6 | 19.7 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_f0_proof.v |
| +6.06% | 23.1 | 24.5 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/virtual/virtual_cpp_proof.v |
| +6.22% | 18.4 | 19.5 | +1.1 | fmdeps/auto-docs/content/docs/control_flow/loop.v |
| +6.41% | 18.4 | 19.6 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f1_proof.v |
| +6.54% | 22.3 | 23.7 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/sub_const.v |
| +6.78% | 25.2 | 26.9 | +1.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f0_proof.v |
| +6.85% | 21.4 | 22.8 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f0_proof.v |
| +7.03% | 22.4 | 24.0 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/allocation_lambda_forms.v |
| +7.93% | 20.1 | 21.7 | +1.6 | fmdeps/auto-docs/content/docs/debugging/main.v |
| +7.96% | 18.2 | 19.6 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/assignment_operators_min_bool.v |
| +9.00% | 21.4 | 23.3 | +1.9 | bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/mutex_hpp_proof.v |
| +10.37% | 16.3 | 18.0 | +1.7 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/member_pointer_operators.v |
| +10.38% | 15.6 | 17.3 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f1_proof.v |
| -0.34% | 134466.5 | 134005.2 | -461.4 | total |
| -0.01% | 27548.3 | 27551.8 | -3.5 | ├ translation units |
| -0.43% | 106456.9 | 106914.7 | -457.8 | └ proofs and tests |
8 tasks
rlepigre-skylabs-ai
force-pushed
the
skylabs-master
branch
from
2ede3c9 to
bef7df5
Compare
Janno
force-pushed
the
janno/cbn-delayed-subst
branch
from
ba40a09 to
80056b7
Compare
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | 8fc3ef1 |
| fmdeps/BRiCk/ | main | 9916cb2 |
| fmdeps/auto/ | main | a4725a1 |
| fmdeps/auto-docs/ | main | 2a67550 |
| bluerock/NOVA/ | skylabs-proof | 3b48855 |
| bluerock/bhv/ | skylabs-main | 54e9d1e |
| fmdeps/brick-libcpp/ | main | 8d4d524 |
| fmdeps/ci/ | main | 447a671 |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| fmdeps/fm-tools/ | main | c1e387f |
| psi/protos/ | main | 8fe3e7c |
| psi/backend/ | main | 0b5fea6 |
| psi/ide/ | main | 6b596cf |
| psi/data/ | main | ca817a8 |
| fmdeps/rocq-agent-toolkit/ | main | 186cc3f |
| vendored/rocq-elpi/ | skylabs-master | 49a4a74 |
| vendored/rocq-equations/ | skylabs-main | d1f944a |
| vendored/rocq-ext-lib/ | skylabs-master | a31ad69 |
| vendored/rocq-iris/ | skylabs-master | a7af9f7 |
| vendored/rocq-lsp/ | skylabs-main | 2f4c359 |
| vendored/rocq-stdlib/ | skylabs-master | 00897b3 |
| vendored/rocq-stdpp/ | skylabs-master | 0c5e505 |
| fmdeps/skylabs-fm/ | main | 689db5a |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.64% | 129372.5 | 128542.6 | -829.9 | total |
| -0.00% | 23499.1 | 23497.9 | -1.2 | ├ translation units |
| -0.78% | 105873.4 | 105044.7 | -828.7 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -30.66% | 522.6 | 362.3 | -160.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep_spec.v |
| -18.83% | 56.9 | 46.2 | -10.7 | fmdeps/auto/rocq-skylabs-auto-core/tests/cancelx_tactic.v |
| -11.35% | 47.7 | 42.3 | -5.4 | bluerock/bhv/apps/vswitch/proof/model/ethernet.v |
| -10.12% | 67.7 | 60.8 | -6.9 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/pair_hpp_spec.v |
| -7.80% | 85.3 | 78.7 | -6.7 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/send.v |
| -6.55% | 146.8 | 137.1 | -9.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/splice_cpp_spec.v |
| -5.63% | 51.3 | 48.4 | -2.9 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/initlist_cpp_proof.v |
| -5.41% | 1189.5 | 1125.1 | -64.4 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/sync_impl.v |
| -5.10% | 56.0 | 53.2 | -2.9 | bluerock/bhv/zeta/lib/lang/proof/errno_hpp_proof.v |
| -3.76% | 77.7 | 74.8 | -2.9 | bluerock/bhv/apps/umx/proof/main_cpp_proof/setup_sigs.v |
| -3.69% | 80.8 | 77.8 | -3.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/drop.v |
| -3.60% | 133.6 | 128.8 | -4.8 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/proof.v |
| -3.54% | 522.2 | 503.7 | -18.5 | bluerock/bhv/lib/drivers/serial/pl011/proof/pl011_cpp_proof.v |
| -3.52% | 37.6 | 36.2 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/default_specs_1.v |
| -3.19% | 222.0 | 215.0 | -7.1 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort_to_vbus.v |
| -2.92% | 330.6 | 320.9 | -9.7 | bluerock/bhv/apps/umx/proof/main_cpp_proof/setup.v |
| -2.85% | 182.3 | 177.1 | -5.2 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/initialize_dataplane.v |
| -2.70% | 100.6 | 97.9 | -2.7 | bluerock/bhv/lib/vrl/proof/vrl/port_hpp_proof.v |
| -2.66% | 149.4 | 145.4 | -4.0 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/compute_gpa_fault_addr.v |
| -2.59% | 468.4 | 456.3 | -12.1 | bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/access.v |
| -2.55% | 186.3 | 181.5 | -4.7 | bluerock/bhv/apps/umx/proof/main_cpp_proof/parse_connect_args.v |
| -2.48% | 46.8 | 45.6 | -1.2 | bluerock/bhv/apps/umx/proof/main_cpp_proof/setup_output_loop_thread.v |
| -2.32% | 852.0 | 832.2 | -19.8 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/proof.v |
| -2.32% | 112.0 | 109.4 | -2.6 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_rich_proof.v |
| -2.31% | 475.1 | 464.1 | -11.0 | bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/zynqmp_dma_ver_cpp_proof.v |
| -2.20% | 96.4 | 94.3 | -2.1 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/start_cpu.v |
| -2.18% | 474.4 | 464.1 | -10.3 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/msr_framework.v |
| -2.02% | 88.1 | 86.3 | -1.8 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctor.v |
| -1.98% | 1662.5 | 1629.6 | -32.9 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_glue.v |
| -1.95% | 170.4 | 167.1 | -3.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/fields/test_cpp_proof.v |
| -1.92% | 682.8 | 669.8 | -13.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/virtual_interface.v |
| -1.90% | 1805.7 | 1771.3 | -34.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v |
| -1.85% | 712.9 | 699.7 | -13.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/misc.v |
| -1.85% | 192.4 | 188.8 | -3.6 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/create_forwarding_plane.v |
| -1.77% | 332.9 | 327.0 | -5.9 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/handle_data_abort.v |
| -1.75% | 197.4 | 193.9 | -3.5 | bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_cpp_proof/space_sel.v |
| -1.74% | 185.4 | 182.1 | -3.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/set_virtio_net_header.v |
| -1.60% | 176.7 | 173.9 | -2.8 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_base_proof.v |
| -1.56% | 382.7 | 376.7 | -6.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/extract_frame_header.v |
| -1.55% | 91.5 | 90.1 | -1.4 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/get_fdt_from_uuid.v |
| -1.55% | 349.5 | 344.1 | -5.4 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort.v |
| -1.54% | 80.6 | 79.3 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/primitive_initialization.v |
| -1.52% | 117.0 | 115.2 | -1.8 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/initialization_forms.v |
| -1.44% | 100.9 | 99.4 | -1.5 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_proof.v |
| -1.43% | 358.0 | 352.9 | -5.1 | bluerock/bhv/apps/vswitch/lib/vsmp/proof/msg_queue_hpp/proof.v |
| -1.36% | 144.6 | 142.6 | -2.0 | bluerock/bhv/zeta/lib/zeta/proof/semaphore_hpp_proof.v |
| -1.34% | 99.6 | 98.2 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/destructuring_declarations.v |
| -1.34% | 134.2 | 132.4 | -1.8 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_off.v |
| -1.33% | 250.8 | 247.4 | -3.3 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sm.v |
| -1.29% | 273.2 | 269.7 | -3.5 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create.v |
| -1.26% | 218.4 | 215.6 | -2.7 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_read_console_id.v |
| -1.25% | 1980.6 | 1955.9 | -24.7 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/init_vcpus.v |
| -1.14% | 116.5 | 115.2 | -1.3 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_pt.v |
| -1.14% | 168.2 | 166.3 | -1.9 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_other.v |
| -1.11% | 153.2 | 151.5 | -1.7 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_relational_operators.v |
| -1.08% | 198.7 | 196.6 | -2.1 | bluerock/NOVA/build-proof/proof/sc_cpp_proof/create.v |
| -1.06% | 102.0 | 101.0 | -1.1 | bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_other.v |
| -1.05% | 148.5 | 147.0 | -1.6 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_roundedup.v |
| -1.04% | 343.4 | 339.8 | -3.6 | bluerock/bhv/apps/umx/proof/main_cpp_proof/input_loop.v |
| -1.03% | 500.0 | 494.8 | -5.2 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/vector/test_cpp_proof.v |
| -1.03% | 1527.3 | 1511.5 | -15.8 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/prepare_address_space.v |
| -1.01% | 113.8 | 112.7 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/destructuring/test_pair.v |
| -1.01% | 195.4 | 193.4 | -2.0 | bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_public.v |
| -1.01% | 759.0 | 751.3 | -7.7 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/setup.v |
| -1.00% | 1091.0 | 1080.1 | -11.0 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/zeta_main.v |
| -0.98% | 314.7 | 311.6 | -3.1 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/resume.v |
| -0.97% | 256.4 | 253.9 | -2.5 | bluerock/bhv/apps/vmm/lib/bluerock/proof/aarch64/reg_accessor_hpp_proof.v |
| -0.95% | 109.6 | 108.5 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/compound_assignment_increments.v |
| -0.95% | 206.8 | 204.9 | -2.0 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/ctor.v |
| -0.92% | 391.1 | 387.5 | -3.6 | bluerock/bhv/lib/vrl/proof/vrl/dataplane_hpp_proof.v |
| -0.92% | 457.1 | 452.9 | -4.2 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pd.v |
| -0.91% | 271.1 | 268.6 | -2.5 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_on.v |
| -0.91% | 174.0 | 172.4 | -1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/data_class/class_32_cpp_proof.v |
| -0.91% | 539.5 | 534.6 | -4.9 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/run_vm.v |
| -0.88% | 233.6 | 231.6 | -2.1 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/read_line.v |
| -0.86% | 656.5 | 650.8 | -5.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/call_cpp_proof.v |
| -0.82% | 147.2 | 146.0 | -1.2 | bluerock/NOVA/build-proof/proof/pt_cpp_proof/create.v |
| -0.82% | 128.0 | 127.0 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/val_cat/val_cat_cpp_proof.v |
| -0.81% | 149.4 | 148.2 | -1.2 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command.v |
| -0.80% | 930.7 | 923.2 | -7.4 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/setup.v |
| -0.78% | 198.8 | 197.2 | -1.5 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/queue/misc.v |
| -0.77% | 129.9 | 128.9 | -1.0 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_emulating.v |
| -0.75% | 1680.8 | 1668.2 | -12.6 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/reset.v |
| -0.74% | 468.6 | 465.1 | -3.5 | bluerock/bhv/apps/vswitch/lib/port/proof/port/proof.v |
| -0.72% | 341.6 | 339.1 | -2.5 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/schedule.v |
| -0.72% | 534.5 | 530.7 | -3.8 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_pd.v |
| -0.72% | 185.1 | 183.8 | -1.3 | bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/memory_hpp_proof.v |
| -0.72% | 292.5 | 290.4 | -2.1 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pt.v |
| -0.71% | 194.8 | 193.4 | -1.4 | bluerock/bhv/zeta/lib/intrusive/proof/shared_pointer_hpp_proof.v |
| -0.71% | 162.5 | 161.4 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/floating_binary_operators.v |
| -0.70% | 462.2 | 459.0 | -3.2 | bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_private.v |
| -0.70% | 176.0 | 174.8 | -1.2 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/wait_if_exec_paused.v |
| -0.69% | 168.8 | 167.7 | -1.2 | bluerock/NOVA/build-proof/proof/sm_cpp_proof/create.v |
| -0.69% | 146.1 | 145.1 | -1.0 | bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/msr_cpp_proof.v |
| -0.64% | 161.7 | 160.7 | -1.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof.v |
| -0.64% | 240.9 | 239.4 | -1.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/proof.v |
| -0.63% | 531.5 | 528.2 | -3.3 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sc.v |
| -0.61% | 765.2 | 760.6 | -4.6 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_proof.v |
| -0.60% | 228.6 | 227.3 | -1.4 | bluerock/bhv/apps/vmm/vml/devices/msr/proof/aarch64/msr_hpp_proof.v |
| -0.59% | 965.9 | 960.2 | -5.7 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_cpp_proof.v |
| -0.58% | 361.6 | 359.5 | -2.1 | bluerock/bhv/zeta/lib/lang/proof/atomic_hpp_proof.v |
| -0.57% | 475.3 | 472.6 | -2.7 | bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/recv.v |
| -0.55% | 249.4 | 248.0 | -1.4 | bluerock/bhv/zeta/lib/uuid/proof/uuid_hpp_proof.v |
| -0.53% | 229.4 | 228.2 | -1.2 | bluerock/bhv/apps/umx/proof/main_cpp_proof/user_handler.v |
| -0.53% | 328.9 | 327.2 | -1.7 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_sm.v |
| -0.45% | 546.3 | 543.9 | -2.5 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/ready_queues.v |
| -0.44% | 235.3 | 234.3 | -1.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/flood.v |
| -0.39% | 337.5 | 336.2 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/merge_cpp_proof.v |
| -0.32% | 492.6 | 491.0 | -1.6 | bluerock/bhv/zeta/lib/concurrent/proof/lossy_queue2_hpp_proof.v |
| -0.31% | 612.9 | 611.0 | -1.9 | bluerock/bhv/apps/umx/proof/main_cpp_proof/scanner_state.v |
| -0.29% | 371.5 | 370.5 | -1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/conclude_chain_use.v |
| -0.26% | 515.6 | 514.3 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/test1_proof.v |
| -0.19% | 1131.9 | 1129.7 | -2.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v |
| -0.19% | 546.9 | 545.9 | -1.0 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_sc.v |
| -0.18% | 637.2 | 636.1 | -1.2 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/misc.v |
| +0.39% | 882.1 | 885.5 | +3.4 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_default_impl.v |
| +0.40% | 261.3 | 262.3 | +1.0 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/delegate.v |
| +0.54% | 303.4 | 305.0 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_main_proof.v |
| +4.55% | 23.4 | 24.5 | +1.1 | fmdeps/auto-docs/content/docs/class_reps/alt.v |
| +7.69% | 20.2 | 21.8 | +1.6 | fmdeps/auto-docs/content/docs/debugging/main.v |
| +17.58% | 7.8 | 9.2 | +1.4 | fmdeps/auto/rocq-skylabs-auto-core/tests/warnings.v |
| -0.64% | 129372.5 | 128542.6 | -829.9 | total |
| -0.00% | 23499.1 | 23497.9 | -1.2 | ├ translation units |
| -0.78% | 105873.4 | 105044.7 | -828.7 | └ 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
1 participant
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.
Github won't let me re-open the old PR because I force-pushed to the branch.
Fixes / closes #????
make doc_gram_rsts.