Remove [untemplate_goal] - #87
Merged
gmalecha-at-skylabs merged 1 commit intoJun 19, 2026
Merged
Conversation
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | b25979c |
| fmdeps/BRiCk/ | main | 1e1012e |
| fmdeps/auto-docs/ | main | f3ece99 |
| bluerock/NOVA/ | skylabs-proof | 488788c |
| bluerock/bhv/ | skylabs-main | 59068bc |
| fmdeps/ci/ | main | 2f1940b |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| fmdeps/fm-tools/ | main | 18d9d0a |
| psi/protos/ | main | 8fe3e7c |
| psi/backend/ | main | 2be21b2 |
| psi/ide/ | main | 6b596cf |
| psi/data/ | main | 5a4c61e |
| vendored/rocq/ | skylabs-master | bef7df5 |
| fmdeps/rocq-agent-toolkit/ | main | 51ae58b |
| vendored/rocq-elpi/ | skylabs-master | be1ffc5 |
| vendored/rocq-equations/ | skylabs-main | d1f944a |
| vendored/rocq-ext-lib/ | skylabs-master | a31ad69 |
| vendored/rocq-iris/ | skylabs-master | a7af9f7 |
| vendored/rocq-lsp/ | skylabs-main | 64ef78a |
| vendored/rocq-stdlib/ | skylabs-master | 00897b3 |
| vendored/rocq-stdpp/ | skylabs-master | 0c5e505 |
| fmdeps/skylabs-fm/ | main | 148b1ba |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.36% | 129865.2 | 129394.9 | -470.2 | total |
| -0.57% | 737.0 | - | -737.0 | ├ disappeared files (4) |
| +0.34% | - | 439.6 | +439.6 | ├ newly appeared files (100) |
| -0.13% | 129128.2 | 128955.3 | -172.8 | └ common files |
| -0.00% | 23462.8 | 23462.8 | -0.0 | ├ translation units |
| -0.16% | 105665.4 | 105492.5 | -172.8 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -12.46% | 21.9 | 19.2 | -2.7 | bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/mutex_hpp_proof.v |
| -3.35% | 44.7 | 43.2 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/control_flow/main_cpp_spec.v |
| -1.33% | 115.0 | 113.5 | -1.5 | bluerock/bhv/lib/socket/proof/socket_defs_hpp_proof.v |
| -1.28% | 85.9 | 84.8 | -1.1 | bluerock/bhv/zeta/lib/lang/proof/endian16_hpp_proof.v |
| -1.09% | 125.2 | 123.9 | -1.4 | bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/proof.v |
| -1.06% | 101.1 | 100.0 | -1.1 | bluerock/bhv/lib/vrl/proof/vrl/port_hpp_proof.v |
| -1.01% | 111.8 | 110.7 | -1.1 | bluerock/NOVA/build-proof/proof/syscall_hpp_proof.v |
| -0.74% | 195.6 | 194.2 | -1.4 | bluerock/bhv/zeta/lib/intrusive/proof/shared_pointer_hpp_proof.v |
| -0.71% | 199.1 | 197.7 | -1.4 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/queue/misc.v |
| -0.69% | 362.7 | 360.2 | -2.5 | bluerock/bhv/zeta/lib/lang/proof/atomic_hpp_proof.v |
| -0.64% | 476.0 | 473.0 | -3.0 | bluerock/bhv/apps/vswitch/lib/port/proof/port/proof.v |
| -0.62% | 358.3 | 356.1 | -2.2 | bluerock/bhv/apps/vswitch/lib/vsmp/proof/msg_queue_hpp/proof.v |
| -0.54% | 273.7 | 272.2 | -1.5 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create.v |
| -0.45% | 329.7 | 328.2 | -1.5 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/async_copy_cookie.v |
| -0.45% | 391.9 | 390.1 | -1.8 | bluerock/bhv/lib/vrl/proof/vrl/dataplane_hpp_proof.v |
| -0.43% | 257.3 | 256.2 | -1.1 | bluerock/bhv/apps/vmm/lib/bluerock/proof/aarch64/reg_accessor_hpp_proof.v |
| -0.40% | 344.8 | 343.4 | -1.4 | bluerock/bhv/apps/umx/proof/main_cpp_proof/input_loop.v |
| -0.39% | 639.7 | 637.3 | -2.5 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/misc.v |
| -0.38% | 476.1 | 474.3 | -1.8 | bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/zynqmp_dma_ver_cpp_proof.v |
| -0.33% | 716.8 | 714.4 | -2.4 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/misc.v |
| -0.33% | 331.7 | 330.6 | -1.1 | bluerock/bhv/apps/umx/proof/main_cpp_proof/setup.v |
| -0.26% | 463.4 | 462.2 | -1.2 | bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_private.v |
| -0.26% | 524.0 | 522.6 | -1.4 | bluerock/bhv/lib/drivers/serial/pl011/proof/pl011_cpp_proof.v |
| -0.25% | 854.5 | 852.3 | -2.2 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/proof.v |
| -0.25% | 536.1 | 534.7 | -1.3 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_pd.v |
| -0.25% | 475.4 | 474.2 | -1.2 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/msr_framework.v |
| -0.23% | 547.3 | 546.1 | -1.3 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/ready_queues.v |
| -0.23% | 761.7 | 760.0 | -1.7 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/setup.v |
| -0.20% | 1531.8 | 1528.7 | -3.1 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/prepare_address_space.v |
| -0.19% | 533.0 | 532.0 | -1.0 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sc.v |
| -0.18% | 653.0 | 651.9 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/call_cpp_proof.v |
| -0.18% | 933.9 | 932.3 | -1.7 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/setup.v |
| -0.18% | 613.7 | 612.6 | -1.1 | bluerock/bhv/apps/umx/proof/main_cpp_proof/scanner_state.v |
| -0.15% | 672.8 | 671.8 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist_cpp/forward_list_hpp_proof.v |
| -0.15% | 1137.5 | 1135.8 | -1.7 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v |
| -0.14% | 1812.6 | 1810.0 | -2.6 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v |
| -0.13% | 892.7 | 891.5 | -1.2 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/atomic/test_cpp_proof.v |
| -0.12% | 1094.5 | 1093.2 | -1.3 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/zeta_main.v |
| -0.12% | 884.0 | 883.0 | -1.0 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_default_impl.v |
| -0.12% | 1683.1 | 1681.2 | -1.9 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/reset.v |
| -0.11% | 966.7 | 965.6 | -1.1 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_cpp_proof.v |
| -0.11% | 1985.7 | 1983.5 | -2.2 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/init_vcpus.v |
| +1.96% | 60.1 | 61.2 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/micromega/micromega1.v |
| +6.45% | 16.1 | 17.2 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/cpp/spec/specify.v |
| -0.36% | 129865.2 | 129394.9 | -470.2 | total |
| -0.57% | 737.0 | - | -737.0 | ├ disappeared files (4) |
| +0.34% | - | 439.6 | +439.6 | ├ newly appeared files (100) |
| -0.13% | 129128.2 | 128955.3 | -172.8 | └ common files |
| -0.00% | 23462.8 | 23462.8 | -0.0 | ├ translation units |
| -0.16% | 105665.4 | 105492.5 | -172.8 | └ proofs and tests |
gmalecha-at-skylabs
force-pushed
the
gmalecha/verify-template-specialization
branch
from
June 18, 2026 19:16
20759c7 to
151adf0
Compare
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | b25979c |
| fmdeps/BRiCk/ | main | 2286628 |
| fmdeps/auto-docs/ | main | f3ece99 |
| bluerock/NOVA/ | skylabs-proof | 488788c |
| bluerock/bhv/ | skylabs-main | 59068bc |
| fmdeps/ci/ | main | 2f1940b |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| fmdeps/fm-tools/ | main | 18d9d0a |
| psi/protos/ | main | 8fe3e7c |
| psi/backend/ | main | 2be21b2 |
| psi/ide/ | main | 6b596cf |
| psi/data/ | main | 3cffdd9 |
| vendored/rocq/ | skylabs-master | bef7df5 |
| fmdeps/rocq-agent-toolkit/ | main | 51ae58b |
| vendored/rocq-elpi/ | skylabs-master | be1ffc5 |
| vendored/rocq-equations/ | skylabs-main | d1f944a |
| vendored/rocq-ext-lib/ | skylabs-master | a31ad69 |
| vendored/rocq-iris/ | skylabs-master | a7af9f7 |
| vendored/rocq-lsp/ | skylabs-main | 64ef78a |
| vendored/rocq-stdlib/ | skylabs-master | 00897b3 |
| vendored/rocq-stdpp/ | skylabs-master | 0c5e505 |
| fmdeps/skylabs-fm/ | main | 7b9e793 |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.00% | 129383.1 | 129378.7 | -4.5 | total |
| -0.56% | 733.1 | - | -733.1 | ├ disappeared files (4) |
| +0.34% | - | 439.4 | +439.4 | ├ newly appeared files (100) |
| +0.22% | 128650.0 | 128939.3 | +289.3 | └ common files |
| -0.00% | 23471.1 | 23471.1 | -0.0 | ├ translation units |
| +0.28% | 105178.9 | 105468.2 | +289.3 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -12.46% | 21.9 | 19.2 | -2.7 | bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/mutex_hpp_proof.v |
| -2.64% | 42.5 | 41.4 | -1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/cpp_hints.v |
| -2.15% | 51.4 | 50.3 | -1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/virtio_net_header_hints.v |
| -1.84% | 61.7 | 60.6 | -1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints.v |
| -1.58% | 71.7 | 70.6 | -1.1 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/spec.v |
| -1.56% | 100.6 | 99.1 | -1.6 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/drop.v |
| -1.51% | 76.1 | 74.9 | -1.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/pkt.v |
| -1.34% | 115.0 | 113.5 | -1.5 | bluerock/bhv/lib/socket/proof/socket_defs_hpp_proof.v |
| -1.17% | 95.7 | 94.6 | -1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/spec.v |
| -0.73% | 139.9 | 138.9 | -1.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/walk_chain.v |
| -0.70% | 362.1 | 359.6 | -2.5 | bluerock/bhv/zeta/lib/lang/proof/atomic_hpp_proof.v |
| -0.55% | 234.2 | 232.9 | -1.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/flood.v |
| -0.42% | 357.6 | 356.1 | -1.5 | bluerock/bhv/apps/vswitch/lib/vsmp/proof/msg_queue_hpp/proof.v |
| -0.33% | 1139.6 | 1135.8 | -3.7 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v |
| -0.26% | 638.6 | 636.9 | -1.7 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/misc.v |
| -0.26% | 474.3 | 473.0 | -1.2 | bluerock/bhv/apps/vswitch/lib/port/proof/port/proof.v |
| -0.19% | 653.4 | 652.2 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/call_cpp_proof.v |
| -0.14% | 1812.5 | 1810.0 | -2.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v |
| -0.12% | 1530.7 | 1528.8 | -1.9 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/prepare_address_space.v |
| +0.14% | 872.1 | 873.4 | +1.2 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/reset_cpu.v |
| +0.19% | 713.1 | 714.5 | +1.4 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/misc.v |
| +0.27% | 376.2 | 377.2 | +1.0 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_pd.v |
| +0.30% | 372.0 | 373.1 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/conclude_chain_use.v |
| +0.37% | 317.2 | 318.4 | +1.2 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_obj.v |
| +0.37% | 324.3 | 325.5 | +1.2 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_hst.v |
| +0.38% | 321.2 | 322.4 | +1.2 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_dma.v |
| +0.38% | 339.4 | 340.7 | +1.3 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_pt.v |
| +0.40% | 298.0 | 299.1 | +1.2 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/wp_vcpu_lemmas.v |
| +0.41% | 250.3 | 251.3 | +1.0 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sm.v |
| +0.42% | 269.3 | 270.5 | +1.1 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_on.v |
| +0.42% | 252.8 | 253.9 | +1.1 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/TO_UPSTREAM.v |
| +0.44% | 284.2 | 285.5 | +1.3 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_sm.v |
| +0.47% | 302.7 | 304.2 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_main_proof.v |
| +0.47% | 267.3 | 268.5 | +1.3 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_gst.v |
| +0.52% | 240.4 | 241.7 | +1.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/proof.v |
| +0.53% | 190.1 | 191.1 | +1.0 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/defs.v |
| +0.55% | 382.7 | 384.8 | +2.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/extract_frame_header.v |
| +0.55% | 191.4 | 192.5 | +1.1 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/create_forwarding_plane.v |
| +0.58% | 258.5 | 260.0 | +1.5 | bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/mmio.v |
| +0.60% | 181.4 | 182.5 | +1.1 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/initialize_dataplane.v |
| +0.64% | 333.4 | 335.5 | +2.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/hints.v |
| +0.68% | 167.1 | 168.2 | +1.1 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_other.v |
| +0.70% | 181.8 | 183.0 | +1.3 | bluerock/bhv/apps/umx/proof/main_cpp_proof/parse_connect_args.v |
| +0.73% | 148.4 | 149.5 | +1.1 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command.v |
| +0.74% | 147.8 | 148.9 | +1.1 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_roundedup.v |
| +0.75% | 152.8 | 153.9 | +1.2 | bluerock/bhv/zeta/lib/nova/proof/safe_proof/safe_proof.v |
| +0.76% | 141.2 | 142.3 | +1.1 | bluerock/bhv/apps/vmm/vml/devices/gic/proof/model/gic_hpp_spec.v |
| +0.78% | 138.6 | 139.7 | +1.1 | bluerock/bhv/zeta/lib/concurrent/proof/lock_hpp_proof.v |
| +0.81% | 145.8 | 147.0 | +1.2 | bluerock/bhv/lib/drivers/serial/pl011/proof/mmio.v |
| +0.84% | 139.0 | 140.2 | +1.2 | bluerock/NOVA/build-proof/proof/iface/hypercall/pd.v |
| +0.85% | 145.6 | 146.8 | +1.2 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/devq/send.v |
| +0.85% | 257.8 | 260.0 | +2.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/get_set_byte_requesters.v |
| +0.86% | 157.5 | 158.8 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_main_proof.v |
| +0.87% | 141.0 | 142.3 | +1.2 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/defs.v |
| +0.90% | 121.9 | 123.0 | +1.1 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/create.v |
| +0.92% | 110.5 | 111.5 | +1.0 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/startup.v |
| +0.94% | 140.9 | 142.2 | +1.3 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/defs.v |
| +0.94% | 109.7 | 110.7 | +1.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/util.v |
| +0.95% | 131.3 | 132.6 | +1.3 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/update.v |
| +0.97% | 106.7 | 107.7 | +1.0 | bluerock/NOVA/build-proof/proof/sm_cpp_proof/up.v |
| +0.98% | 108.3 | 109.4 | +1.1 | bluerock/bhv/apps/umx/proof/main_cpp_proof/output_loop.v |
| +1.00% | 184.8 | 186.6 | +1.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/set_virtio_net_header.v |
| +1.00% | 122.9 | 124.1 | +1.2 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/init_info.v |
| +1.01% | 227.1 | 229.4 | +2.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/hints.v |
| +1.04% | 141.7 | 143.2 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v |
| +1.04% | 111.1 | 112.2 | +1.2 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_rich_proof.v |
| +1.06% | 144.3 | 145.8 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v |
| +1.11% | 121.7 | 123.1 | +1.3 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/lookup.v |
| +1.12% | 161.0 | 162.8 | +1.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof.v |
| +1.13% | 100.1 | 101.2 | +1.1 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_proof.v |
| +1.13% | 95.5 | 96.6 | +1.1 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/start_cpu.v |
| +1.13% | 125.8 | 127.3 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/unit_tests.v |
| +1.16% | 123.0 | 124.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_main_proof.v |
| +1.22% | 93.0 | 94.1 | +1.1 | bluerock/bhv/apps/vswitch/proof/model/vswitch/lemmas.v |
| +1.22% | 86.7 | 87.8 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/route.v |
| +1.24% | 101.1 | 102.3 | +1.2 | bluerock/bhv/apps/vswitch/proof/ghost.v |
| +1.25% | 81.4 | 82.5 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_main_proof.v |
| +1.26% | 120.6 | 122.1 | +1.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtual_interface.v |
| +1.27% | 98.7 | 100.0 | +1.3 | bluerock/NOVA/build-proof/proof/timeout_cpp_proof/enqueue.v |
| +1.30% | 111.6 | 113.1 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_main_proof.v |
| +1.36% | 79.6 | 80.7 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/primitive_initialization.v |
| +1.36% | 73.6 | 74.6 | +1.0 | bluerock/NOVA/build-proof/proof/timeout_cpp_proof/client_dequeue.v |
| +1.39% | 80.0 | 81.1 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/drop.v |
| +1.43% | 101.8 | 103.3 | +1.5 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/spec.v |
| +1.45% | 73.3 | 74.4 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0084_cpp_main_proof.v |
| +1.47% | 77.0 | 78.1 | +1.1 | bluerock/bhv/apps/umx/proof/main_cpp_proof/setup_sigs.v |
| +1.49% | 68.0 | 69.0 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f3_proof.v |
| +1.49% | 79.2 | 80.4 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0099_cpp_main_proof.v |
| +1.52% | 66.1 | 67.1 | +1.0 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/unblock.v |
| +1.53% | 86.9 | 88.2 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_main_proof.v |
| +1.57% | 78.0 | 79.3 | +1.2 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_spec.v |
| +1.58% | 63.5 | 64.5 | +1.0 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/insert.v |
| +1.67% | 85.7 | 87.1 | +1.4 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/roundup_parallel_proof.v |
| +1.77% | 74.2 | 75.5 | +1.3 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/base_startup_handler.v |
| +1.80% | 57.6 | 58.6 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0088_cpp_main_proof.v |
| +1.87% | 74.5 | 75.8 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_main_proof.v |
| +1.93% | 57.6 | 58.7 | +1.1 | bluerock/bhv/apps/umx/proof/umx_hpp_proof/umxshared/nth_client.v |
| +1.95% | 61.5 | 62.7 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/read_prim/read_cpp_proof.v |
| +1.97% | 54.3 | 55.3 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_f0_proof.v |
| +1.98% | 152.0 | 155.0 | +3.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/misc_hints.v |
| +2.00% | 57.1 | 58.3 | +1.1 | bluerock/bhv/apps/umx/proof/main_cpp_proof/copy_bytes_and_flush.v |
| +2.03% | 54.6 | 55.7 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/packet_ctor.v |
| +2.04% | 57.4 | 58.6 | +1.2 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/requesters.v |
| +2.06% | 56.3 | 57.5 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f2_proof.v |
| +2.10% | 51.6 | 52.7 | +1.1 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/hints.v |
| +2.14% | 64.0 | 65.4 | +1.4 | bluerock/NOVA/build-proof/proof/syscall_hpp_spec.v |
| +2.20% | 65.5 | 66.9 | +1.4 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/resume_all.v |
| +2.29% | 45.3 | 46.3 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/auto_frac/anyR_proof.v |
| +2.30% | 45.9 | 47.0 | +1.1 | bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_cpp_proof/lookup.v |
| +2.32% | 53.0 | 54.2 | +1.2 | bluerock/bhv/apps/vmm/lib/dynamic_as/proof/guest_as_hpp_proof.v |
| +2.35% | 45.1 | 46.2 | +1.1 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/utility/test_cpp_proof.v |
| +2.36% | 45.3 | 46.4 | +1.1 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctrl_feature_reset.v |
| +2.39% | 43.7 | 44.8 | +1.0 | bluerock/bhv/zeta/lib/bson/proof/bson_hints.v |
| +2.40% | 46.9 | 48.0 | +1.1 | bluerock/bhv/apps/vswitch/proof/model/ethernet.v |
| +2.42% | 43.4 | 44.5 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/x86_64/simple_arch_hpp_spec.v |
| +2.47% | 40.9 | 41.9 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/integral_casts.v |
| +2.47% | 43.3 | 44.4 | +1.1 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/lec_stack_size.v |
| +2.49% | 48.0 | 49.2 | +1.2 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/hints.v |
| +2.58% | 44.1 | 45.3 | +1.1 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_pio.v |
| +2.60% | 42.7 | 43.8 | +1.1 | bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_split_range.v |
| +2.61% | 41.9 | 43.0 | +1.1 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/run.v |
| +2.63% | 45.2 | 46.4 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/inits/main_cpp_spec.v |
| +2.70% | 41.7 | 42.8 | +1.1 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/ghost.v |
| +2.74% | 45.9 | 47.2 | +1.3 | bluerock/bhv/apps/umx/proof/main_cpp_proof/setup_output_loop_thread.v |
| +2.78% | 37.8 | 38.9 | +1.1 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/used/misc.v |
| +2.80% | 37.8 | 38.9 | +1.1 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/available/misc.v |
| +2.80% | 37.6 | 38.6 | +1.1 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/descriptor/misc.v |
| +2.81% | 40.7 | 41.9 | +1.1 | bluerock/bhv/apps/vswitch/proof/upstream/hints.v |
| +2.83% | 58.8 | 60.4 | +1.7 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/roundup_all.v |
| +2.84% | 50.2 | 51.7 | +1.4 | bluerock/NOVA/build-proof/proof/slab_cpp_proof/hints.v |
| +2.89% | 36.7 | 37.7 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/smoke.v |
| +2.90% | 44.0 | 45.2 | +1.3 | bluerock/bhv/apps/vmm/lib/dynamic_as/proof/guest_chunk_repo_hpp_proof.v |
| +2.94% | 39.5 | 40.6 | +1.2 | bluerock/bhv/apps/vmm/vml/devices/msr/proof/msr_id_hpp_proof.v |
| +2.96% | 41.8 | 43.0 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/int128/test.v |
| +2.97% | 34.9 | 36.0 | +1.0 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctrl_feature_on_vcpu.v |
| +3.00% | 34.4 | 35.5 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/sizeof_alignof.v |
| +3.00% | 38.9 | 40.0 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep/anyR_proof.v |
| +3.03% | 37.5 | 38.6 | +1.1 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/cpu_feature_hpp_derived_specs.v |
| +3.06% | 41.0 | 42.3 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f2_proof.v |
| +3.09% | 38.8 | 40.0 | +1.2 | bluerock/bhv/apps/umx/proof/admin_hints.v |
| +3.13% | 40.9 | 42.2 | +1.3 | bluerock/bhv/zeta/lib/log/proof/log_hpp_spec.v |
| +3.17% | 35.9 | 37.0 | +1.1 | bluerock/bhv/lib/vrl/proof/vrl/port_list_hints.v |
| +3.21% | 46.7 | 48.2 | +1.5 | bluerock/bhv/apps/vmm/vml/devices/simple_as/proof/simple_as_hpp_spec.v |
| +3.22% | 41.2 | 42.5 | +1.3 | bluerock/NOVA/build-proof/proof/kmem_hpp_spec.v |
| +3.25% | 37.8 | 39.0 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/arch_indep/aarch64/simple_arch_hpp_spec.v |
| +3.29% | 43.2 | 44.6 | +1.4 | bluerock/bhv/apps/vmm/proof/bm_dram.v |
| +3.29% | 44.0 | 45.5 | +1.4 | bluerock/NOVA/build-proof/proof/slab_hpp_spec/partial_big_sep.v |
| +3.41% | 30.3 | 31.3 | +1.0 | bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_split_sz.v |
| +3.49% | 31.0 | 32.1 | +1.1 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/init.v |
| +3.51% | 34.4 | 35.6 | +1.2 | fmdeps/auto-docs/content/docs/functions/verification.v |
| +3.59% | 32.2 | 33.4 | +1.2 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/countLN.v |
| +3.71% | 34.1 | 35.4 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f0_proof.v |
| +3.81% | 32.8 | 34.0 | +1.2 | bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof_intersect.v |
| +3.81% | 27.4 | 28.4 | +1.0 | bluerock/bhv/zeta/apps/msc/proof/nova_caprange_hpp_proof.v |
| +3.89% | 30.0 | 31.2 | +1.2 | bluerock/NOVA/build-proof/proof/timeout_cpp_proof/check.v |
| +3.92% | 30.3 | 31.5 | +1.2 | bluerock/NOVA/build-proof/proof/slab_cpp_proof/alloc.v |
| +3.96% | 34.2 | 35.5 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/sem_const/constructor.v |
| +4.07% | 34.3 | 35.7 | +1.4 | bluerock/NOVA/build-proof/proof/iface/model.v |
| +4.07% | 30.1 | 31.3 | +1.2 | bluerock/bhv/apps/umx/proof/main_cpp_proof/umxservice.v |
| +4.17% | 31.9 | 33.2 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/arrays.v |
| +4.18% | 25.2 | 26.3 | +1.1 | bluerock/bhv/zeta/lib/zeta/proof/mutex_hpp_proof.v |
| +4.23% | 32.5 | 33.8 | +1.4 | bluerock/bhv/zeta/lib/cxx/proof/range_hpp_proof.v |
| +4.25% | 23.8 | 24.8 | +1.0 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/beep.v |
| +4.26% | 29.4 | 30.6 | +1.3 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/prelude.v |
| +4.30% | 30.8 | 32.1 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/implicit_array_initialization.v |
| +4.45% | 25.1 | 26.2 | +1.1 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/wp_vcpu/memory1.v |
| +4.46% | 22.8 | 23.8 | +1.0 | fmdeps/auto/rocq-skylabs-cpp-stdlib/theories/vector/spec.v |
| +4.50% | 27.3 | 28.6 | +1.2 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/is_size_valid.v |
| +4.60% | 41.2 | 43.1 | +1.9 | bluerock/bhv/zeta/lib/bson/proof/bson.v |
| +4.86% | 30.7 | 32.2 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_f0_proof.v |
| +4.87% | 29.8 | 31.2 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0099_cpp_f0_proof.v |
| +4.95% | 30.8 | 32.3 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f3_proof.v |
| +5.00% | 22.8 | 23.9 | +1.1 | bluerock/bhv/zeta/lib/cxx/proof/range_hpp_util.v |
| +5.29% | 25.6 | 27.0 | +1.4 | bluerock/NOVA/build-proof/proof/abi_hpp_proof.v |
| +5.30% | 26.1 | 27.4 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/factor.v |
| +5.37% | 20.7 | 21.8 | +1.1 | bluerock/NOVA/build-proof/proof/timeout_cpp_proof/ctor.v |
| +5.43% | 21.2 | 22.4 | +1.2 | bluerock/bhv/zeta/lib/lang/proof/string_cpp_hints.v |
| +5.51% | 25.4 | 26.8 | +1.4 | bluerock/NOVA/build-proof/proof/space_hpp_proof.v |
| +5.53% | 25.4 | 26.8 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/constructor.v |
| +5.73% | 19.1 | 20.2 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0094_cpp_f1_proof.v |
| +5.75% | 18.9 | 20.0 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f2_proof.v |
| +5.79% | 18.7 | 19.7 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_f0_proof.v |
| +5.81% | 18.7 | 19.8 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f1_proof.v |
| +5.83% | 25.5 | 27.0 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f0_proof.v |
| +5.84% | 26.4 | 27.9 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f0_proof.v |
| +5.85% | 28.7 | 30.4 | +1.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f1_proof.v |
| +5.86% | 18.6 | 19.7 | +1.1 | fmdeps/auto-docs/content/docs/control_flow/loop.v |
| +5.89% | 18.4 | 19.5 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f1_proof.v |
| +5.93% | 19.5 | 20.6 | +1.2 | bluerock/NOVA/build-proof/proof/slab_cpp_proof/utils.v |
| +5.95% | 25.3 | 26.8 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_f0_proof.v |
| +5.98% | 23.5 | 24.9 | +1.4 | bluerock/NOVA/build-proof/proof/bits_hpp_proof.v |
| +5.98% | 22.2 | 23.6 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/virtual/virtual_cpp_proof.v |
| +6.01% | 25.1 | 26.6 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f3_proof.v |
| +6.07% | 17.7 | 18.8 | +1.1 | bluerock/bhv/zeta/lib/lang/proof/string_gnu_cpp_proof.v |
| +6.12% | 17.9 | 19.0 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_f0_proof.v |
| +6.13% | 24.0 | 25.5 | +1.5 | bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/zynqmp_dma_ver_hpp_spec.v |
| +6.35% | 22.4 | 23.8 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/sub_const.v |
| +6.36% | 22.8 | 24.2 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/allocation_lambda_forms.v |
| +6.47% | 16.1 | 17.2 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/theories/cpp/spec/specify.v |
| +6.70% | 19.1 | 20.4 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/normalization/test.v |
| +6.84% | 17.7 | 18.9 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0059_cpp_f1_proof.v |
| +7.01% | 24.6 | 26.3 | +1.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f0_proof.v |
| +7.02% | 15.2 | 16.3 | +1.1 | bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/utils.v |
| +7.31% | 20.7 | 22.2 | +1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f0_proof.v |
| +7.44% | 20.4 | 21.9 | +1.5 | fmdeps/auto-docs/content/docs/debugging/main.v |
| +7.77% | 18.4 | 19.9 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/assignment_operators_min_bool.v |
| +11.49% | 16.6 | 18.5 | +1.9 | bluerock/bhv/zeta/lib/intrusive/proof/rangemap_hpp_model.v |
| +13.19% | 16.0 | 18.2 | +2.1 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/member_pointer_operators.v |
| +14.65% | 14.5 | 16.6 | +2.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f1_proof.v |
| +19.47% | 12.6 | 15.0 | +2.4 | bluerock/bhv/zeta/lib/intrusive/proof/rangemap_hpp_util.v |
| -0.00% | 129383.1 | 129378.7 | -4.5 | total |
| -0.56% | 733.1 | - | -733.1 | ├ disappeared files (4) |
| +0.34% | - | 439.4 | +439.4 | ├ newly appeared files (100) |
| +0.22% | 128650.0 | 128939.3 | +289.3 | └ common files |
| -0.00% | 23471.1 | 23471.1 | -0.0 | ├ translation units |
| +0.28% | 105178.9 | 105468.2 | +289.3 | └ proofs and tests |
gmalecha-at-skylabs
force-pushed
the
gmalecha/verify-template-specialization
branch
from
June 19, 2026 12:40
151adf0 to
c1c1503
Compare
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | b25979c |
| fmdeps/BRiCk/ | main | 6bc3cc1 |
| fmdeps/auto-docs/ | main | f3ece99 |
| bluerock/NOVA/ | skylabs-proof | 488788c |
| bluerock/bhv/ | skylabs-main | 59068bc |
| fmdeps/ci/ | main | 2f1940b |
| vendored/elpi/ | skylabs-master | c0b9653 |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| fmdeps/fm-tools/ | main | 18d9d0a |
| psi/protos/ | main | 8fe3e7c |
| psi/backend/ | main | 2be21b2 |
| psi/ide/ | main | 6b596cf |
| psi/data/ | main | 3cffdd9 |
| vendored/rocq/ | skylabs-master | bef7df5 |
| fmdeps/rocq-agent-toolkit/ | main | 51ae58b |
| vendored/rocq-elpi/ | skylabs-master | be1ffc5 |
| vendored/rocq-equations/ | skylabs-main | d1f944a |
| vendored/rocq-ext-lib/ | skylabs-master | a31ad69 |
| vendored/rocq-iris/ | skylabs-master | a7af9f7 |
| vendored/rocq-lsp/ | skylabs-main | 64ef78a |
| vendored/rocq-stdlib/ | skylabs-master | 00897b3 |
| vendored/rocq-stdpp/ | skylabs-master | 0c5e505 |
| fmdeps/skylabs-fm/ | main | 7b9e793 |
| vendored/vsrocq/ | skylabs-main | ee79e7a |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +0.22% | 129527.0 | 129807.3 | +280.3 | total |
| +0.36% | - | 464.0 | +464.0 | ├ newly appeared files (101) |
| -0.14% | 129527.0 | 129343.3 | -183.8 | └ common files |
| -0.00% | 23471.1 | 23471.1 | -0.0 | ├ translation units |
| -0.17% | 106055.9 | 105872.2 | -183.8 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -12.46% | 21.9 | 19.2 | -2.7 | bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/mutex_hpp_proof.v |
| -6.72% | 24.2 | 22.5 | -1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/allocation_lambda_forms.v |
| -6.19% | 22.0 | 20.6 | -1.4 | fmdeps/auto-docs/content/docs/debugging/main.v |
| -4.66% | 24.8 | 23.6 | -1.2 | fmdeps/auto-docs/content/docs/class_reps/alt.v |
| -4.34% | 23.8 | 22.8 | -1.0 | fmdeps/auto/rocq-skylabs-cpp-stdlib/theories/vector/spec.v |
| -2.64% | 42.3 | 41.2 | -1.1 | bluerock/bhv/zeta/lib/bson/proof/bson.v |
| -1.91% | 112.6 | 110.5 | -2.2 | bluerock/bhv/zeta/lib/cxx/proof/tagged_ptr_hpp_proof.v |
| -1.33% | 114.6 | 113.1 | -1.5 | bluerock/bhv/lib/socket/proof/socket_defs_hpp_proof.v |
| -1.26% | 85.7 | 84.6 | -1.1 | bluerock/bhv/zeta/lib/lang/proof/endian16_hpp_proof.v |
| -1.20% | 147.3 | 145.6 | -1.8 | bluerock/bhv/zeta/lib/alloc/proof/core_hpp_general_proof.v |
| -1.12% | 125.0 | 123.6 | -1.4 | bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/proof.v |
| -1.06% | 100.8 | 99.8 | -1.1 | bluerock/bhv/lib/vrl/proof/vrl/port_hpp_proof.v |
| -1.00% | 111.6 | 110.5 | -1.1 | bluerock/NOVA/build-proof/proof/syscall_hpp_proof.v |
| -0.73% | 195.1 | 193.7 | -1.4 | bluerock/bhv/zeta/lib/intrusive/proof/shared_pointer_hpp_proof.v |
| -0.71% | 248.9 | 247.1 | -1.8 | bluerock/bhv/zeta/lib/uuid/proof/uuid_hpp_proof.v |
| -0.68% | 198.5 | 197.1 | -1.3 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/queue/misc.v |
| -0.68% | 361.5 | 359.1 | -2.5 | bluerock/bhv/zeta/lib/lang/proof/atomic_hpp_proof.v |
| -0.66% | 474.8 | 471.7 | -3.1 | bluerock/bhv/apps/vswitch/lib/port/proof/port/proof.v |
| -0.64% | 357.4 | 355.1 | -2.3 | bluerock/bhv/apps/vswitch/lib/vsmp/proof/msg_queue_hpp/proof.v |
| -0.59% | 272.2 | 270.6 | -1.6 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create.v |
| -0.54% | 185.1 | 184.1 | -1.0 | bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/memory_hpp_proof.v |
| -0.54% | 499.6 | 496.9 | -2.7 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/vector/test_cpp_proof.v |
| -0.53% | 195.3 | 194.3 | -1.0 | bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_public.v |
| -0.46% | 328.4 | 326.9 | -1.5 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/async_copy_cookie.v |
| -0.46% | 389.2 | 387.5 | -1.8 | bluerock/bhv/lib/vrl/proof/vrl/dataplane_hpp_proof.v |
| -0.42% | 255.5 | 254.5 | -1.1 | bluerock/bhv/apps/vmm/lib/bluerock/proof/aarch64/reg_accessor_hpp_proof.v |
| -0.41% | 636.0 | 633.4 | -2.6 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/misc.v |
| -0.38% | 342.3 | 341.0 | -1.3 | bluerock/bhv/apps/umx/proof/main_cpp_proof/input_loop.v |
| -0.33% | 474.8 | 473.2 | -1.5 | bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/zynqmp_dma_ver_cpp_proof.v |
| -0.28% | 712.9 | 710.9 | -2.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/misc.v |
| -0.27% | 521.2 | 519.8 | -1.4 | bluerock/bhv/lib/drivers/serial/pl011/proof/pl011_cpp_proof.v |
| -0.26% | 850.0 | 847.8 | -2.2 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/proof.v |
| -0.25% | 756.5 | 754.6 | -1.9 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/setup.v |
| -0.23% | 472.3 | 471.2 | -1.1 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/msr_framework.v |
| -0.21% | 922.9 | 921.0 | -1.9 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/setup.v |
| -0.20% | 1519.3 | 1516.2 | -3.1 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/prepare_address_space.v |
| -0.20% | 611.9 | 610.7 | -1.2 | bluerock/bhv/apps/umx/proof/main_cpp_proof/scanner_state.v |
| -0.18% | 640.6 | 639.5 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/call_cpp_proof.v |
| -0.16% | 1803.2 | 1800.3 | -2.9 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v |
| -0.16% | 891.6 | 890.2 | -1.4 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/atomic/test_cpp_proof.v |
| -0.16% | 1129.2 | 1127.4 | -1.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v |
| -0.15% | 1087.6 | 1086.0 | -1.7 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/zeta_main.v |
| -0.12% | 1973.6 | 1971.1 | -2.5 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/init_vcpus.v |
| -0.12% | 1666.2 | 1664.2 | -1.9 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/reset.v |
| -0.12% | 880.4 | 879.4 | -1.0 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_default_impl.v |
| +2.47% | 146.4 | 150.0 | +3.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/splice_cpp_spec.v |
| +7.47% | 59.3 | 63.7 | +4.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/micromega/micromega1.v |
| +9.95% | 67.9 | 74.7 | +6.8 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/pair_hpp_spec.v |
| +0.22% | 129527.0 | 129807.3 | +280.3 | total |
| +0.36% | - | 464.0 | +464.0 | ├ newly appeared files (101) |
| -0.14% | 129527.0 | 129343.3 | -183.8 | └ common files |
| -0.00% | 23471.1 | 23471.1 | -0.0 | ├ translation units |
| -0.17% | 106055.9 | 105872.2 | -183.8 | └ proofs and tests |
pgiarrusso-sl
approved these changes
Jun 19, 2026
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
2 participants
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.
Downstream of https://github.com/SkyLabsAI/auto/pull/296