Janno/quadratic tc#12
Closed
Janno wants to merge 6 commits into
Closed
Conversation
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | 7d2ee30 |
| fmdeps/BRiCk/ | main | eda4636 |
| fmdeps/auto/ | main | 9588fca |
| fmdeps/auto-docs/ | main | d4c3641 |
| bluerock/NOVA/ | skylabs-proof | dc3d314 |
| bluerock/bhv/ | skylabs-main | c46f5e3 |
| fmdeps/brick-libcpp/ | main | 2014908 |
| fmdeps/ci/ | main | 9e6e574 |
| vendored/elpi/ | skylabs-master | aa4475f |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| fmdeps/fm-tools/ | main | e5188db |
| psi/protos/ | main | 8fe3e7c |
| psi/backend/ | main | 0b5fea6 |
| psi/ide/ | main | 6b596cf |
| psi/data/ | main | 76acc2f |
| fmdeps/rocq-agent-toolkit/ | main | ac7e4ec |
| 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 | e8b88a7 |
| vendored/vsrocq/ | skylabs-main | 5b4527e |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -1.36% | 126163.5 | 124441.7 | -1721.8 | total |
| -1.29% | 1627.1 | - | -1627.1 | ├ disappeared files (12) |
| -0.08% | 124441.7 | 124536.4 | -94.6 | └ common files |
| -0.00% | 22792.4 | 22792.5 | -0.1 | ├ translation units |
| -0.09% | 101649.3 | 101743.8 | -94.5 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -50.56% | 46.0 | 22.7 | -23.2 | fmdeps/auto/rocq-skylabs-cpp-stdlib/theories/algorithms/spec.v |
| -26.36% | 40.8 | 30.0 | -10.8 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_spec.v |
| -15.90% | 104.1 | 87.6 | -16.6 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_hpp_spec.v |
| -15.22% | 71.3 | 60.5 | -10.9 | bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_hpp_spec.v |
| -12.52% | 58.9 | 51.5 | -7.4 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_spec.v |
| -10.60% | 20.6 | 18.4 | -2.2 | bluerock/bhv/lib/ddk/proof/interrupt_bhv_spec.v |
| -8.34% | 16.7 | 15.3 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f1_proof.v |
| -6.56% | 85.2 | 79.6 | -5.6 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_hpp_spec.v |
| -6.46% | 50.0 | 46.7 | -3.2 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_spec.v |
| -5.89% | 26.3 | 24.8 | -1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f0_proof.v |
| -5.58% | 22.3 | 21.0 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f0_proof.v |
| -4.85% | 27.1 | 25.7 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f0_proof.v |
| -3.48% | 32.6 | 31.4 | -1.1 | bluerock/bhv/lib/vrl/proof/vrl/dataplane_hpp_spec.v |
| -3.29% | 32.7 | 31.6 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f3_proof.v |
| -3.16% | 42.7 | 41.3 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f2_proof.v |
| -2.89% | 98.2 | 95.3 | -2.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/spec.v |
| -2.77% | 55.9 | 54.4 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_f0_proof.v |
| -2.31% | 67.2 | 65.7 | -1.6 | bluerock/NOVA/build-proof/proof/scheduler_hpp_spec/abs_pred.v |
| -2.10% | 82.5 | 80.8 | -1.7 | bluerock/bhv/apps/vswitch/lib/port/proof/port/spec.v |
| -1.57% | 89.1 | 87.7 | -1.4 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/model/cpu_hpp_spec.v |
| -1.50% | 123.0 | 121.2 | -1.8 | bluerock/bhv/apps/vmm/vml/devices/msr/proof/msr_base_hpp_spec.v |
| -1.41% | 149.7 | 147.6 | -2.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/misc_hints.v |
| -1.35% | 194.0 | 191.4 | -2.6 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/create_forwarding_plane.v |
| -1.26% | 119.5 | 118.0 | -1.5 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/hints.v |
| -1.16% | 124.1 | 122.6 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_main_proof.v |
| -1.13% | 1970.9 | 1948.7 | -22.2 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/init_vcpus.v |
| -1.03% | 142.6 | 141.2 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v |
| -0.99% | 180.3 | 178.5 | -1.8 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/spec.v |
| -0.88% | 157.9 | 156.5 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_main_proof.v |
| -0.84% | 192.3 | 190.7 | -1.6 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/set_virtio_net_header.v |
| -0.77% | 145.4 | 144.3 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v |
| -0.76% | 168.1 | 166.8 | -1.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof.v |
| -0.50% | 669.5 | 666.1 | -3.4 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/copy.v |
| -0.35% | 330.8 | 329.7 | -1.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/hints.v |
| -0.29% | 1160.2 | 1156.8 | -3.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v |
| -0.21% | 862.8 | 861.0 | -1.8 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/proof.v |
| -0.12% | 1863.6 | 1861.5 | -2.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v |
| +0.16% | 686.2 | 687.4 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/virtual_interface.v |
| +0.32% | 491.0 | 492.6 | +1.6 | bluerock/bhv/apps/vswitch/lib/port/proof/port/proof.v |
| +0.32% | 363.5 | 364.7 | +1.2 | bluerock/bhv/zeta/lib/lang/proof/atomic_hpp_proof.v |
| +0.35% | 392.8 | 394.2 | +1.4 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/extract_frame_header.v |
| +0.58% | 200.0 | 201.1 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/elpi/enums/variant_cpp_proof.v |
| +0.75% | 250.7 | 252.6 | +1.9 | bluerock/bhv/zeta/lib/uuid/proof/uuid_hpp_proof.v |
| +0.88% | 174.9 | 176.5 | +1.5 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/defs.v |
| +1.03% | 112.8 | 114.0 | +1.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/util.v |
| +1.22% | 102.6 | 103.8 | +1.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/drop.v |
| +1.45% | 87.8 | 89.1 | +1.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/route.v |
| +1.75% | 58.3 | 59.3 | +1.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints.v |
| +2.07% | 83.0 | 84.8 | +1.7 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/drop.v |
| +2.38% | 53.6 | 54.8 | +1.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/flood.v |
| +2.53% | 57.1 | 58.6 | +1.4 | bluerock/bhv/zeta/lib/lang/proof/errno_hpp_proof.v |
| +2.53% | 86.9 | 89.1 | +2.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/send.v |
| +2.68% | 67.4 | 69.2 | +1.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/copy_frame.v |
| +2.68% | 78.3 | 80.4 | +2.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/pkt.v |
| +3.17% | 69.4 | 71.6 | +2.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/extract_frame_header.v |
| +3.78% | 40.4 | 42.0 | +1.5 | bluerock/bhv/zeta/lib/lang/proof/memory_barrier.v |
| +3.90% | 33.8 | 35.1 | +1.3 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/model/virtq/state/descriptor_table.v |
| +3.96% | 38.5 | 40.0 | +1.5 | bluerock/bhv/zeta/lib/bson/proof/bson.v |
| +5.14% | 28.2 | 29.7 | +1.5 | bluerock/bhv/zeta/lib/cxx/proof/range_hpp_spec.v |
| +5.65% | 20.1 | 21.2 | +1.1 | bluerock/bhv/lib/ddk/proof/utils.v |
| +6.90% | 15.0 | 16.0 | +1.0 | bluerock/bhv/zeta/lib/lang/proof/util.v |
| -1.36% | 126163.5 | 124441.7 | -1721.8 | total |
| -1.29% | 1627.1 | - | -1627.1 | ├ disappeared files (12) |
| -0.08% | 124441.7 | 124536.4 | -94.6 | └ common files |
| -0.00% | 22792.4 | 22792.5 | -0.1 | ├ translation units |
| -0.09% | 101649.3 | 101743.8 | -94.5 | └ proofs and tests |
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | 7d2ee30 |
| fmdeps/BRiCk/ | main | 8bffaed |
| fmdeps/auto/ | main | 9588fca |
| fmdeps/auto-docs/ | main | d4c3641 |
| bluerock/NOVA/ | skylabs-proof | dc3d314 |
| bluerock/bhv/ | skylabs-main | c46f5e3 |
| fmdeps/brick-libcpp/ | main | 2014908 |
| fmdeps/ci/ | main | 9e6e574 |
| vendored/elpi/ | skylabs-master | aa4475f |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| fmdeps/fm-tools/ | main | e5188db |
| psi/protos/ | main | 8fe3e7c |
| psi/backend/ | main | 0b5fea6 |
| psi/ide/ | main | 6b596cf |
| psi/data/ | main | 76acc2f |
| fmdeps/rocq-agent-toolkit/ | main | ac7e4ec |
| 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 | e8b88a7 |
| vendored/vsrocq/ | skylabs-main | 5b4527e |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.06% | 126163.5 | 126093.5 | -70.0 | total |
| +0.00% | 22792.9 | 22792.5 | +0.4 | ├ translation units |
| -0.07% | 103300.6 | 103371.0 | -70.4 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -49.37% | 46.0 | 23.3 | -22.7 | fmdeps/auto/rocq-skylabs-cpp-stdlib/theories/algorithms/spec.v |
| -22.13% | 25.7 | 20.0 | -5.7 | bluerock/NOVA/build-proof/proof/ec_hpp_spec.v |
| -20.04% | 40.8 | 32.6 | -8.2 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_spec.v |
| -15.61% | 104.1 | 87.9 | -16.3 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_hpp_spec.v |
| -10.66% | 58.9 | 52.6 | -6.3 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_spec.v |
| -10.60% | 20.6 | 18.4 | -2.2 | bluerock/bhv/lib/ddk/proof/interrupt_bhv_spec.v |
| -8.38% | 16.7 | 15.3 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f1_proof.v |
| -6.45% | 50.0 | 46.7 | -3.2 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_spec.v |
| -6.10% | 71.3 | 67.0 | -4.3 | bluerock/bhv/apps/vmm/vml/devices/vbus/proof/vbus_hpp_spec.v |
| -5.89% | 26.3 | 24.8 | -1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f0_proof.v |
| -5.38% | 22.3 | 21.1 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f0_proof.v |
| -4.84% | 27.1 | 25.7 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_f0_proof.v |
| -4.10% | 85.2 | 81.7 | -3.5 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_hpp_spec.v |
| -3.43% | 32.7 | 31.5 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_f3_proof.v |
| -3.30% | 32.6 | 31.5 | -1.1 | bluerock/bhv/lib/vrl/proof/vrl/dataplane_hpp_spec.v |
| -3.17% | 42.7 | 41.3 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_f2_proof.v |
| -2.32% | 55.9 | 54.6 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0076_cpp_f0_proof.v |
| -2.31% | 67.2 | 65.7 | -1.6 | bluerock/NOVA/build-proof/proof/scheduler_hpp_spec/abs_pred.v |
| -2.27% | 98.2 | 95.9 | -2.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/spec.v |
| -1.46% | 123.0 | 121.2 | -1.8 | bluerock/bhv/apps/vmm/vml/devices/msr/proof/msr_base_hpp_spec.v |
| -1.46% | 82.5 | 81.3 | -1.2 | bluerock/bhv/apps/vswitch/lib/port/proof/port/spec.v |
| -1.41% | 149.7 | 147.6 | -2.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/misc_hints.v |
| -1.35% | 194.0 | 191.4 | -2.6 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/create_forwarding_plane.v |
| -1.17% | 124.1 | 122.6 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0052_cpp_main_proof.v |
| -1.15% | 119.5 | 118.1 | -1.4 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/hints.v |
| -1.03% | 142.6 | 141.2 | -1.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v |
| -0.89% | 180.3 | 178.7 | -1.6 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/spec.v |
| -0.83% | 192.3 | 190.7 | -1.6 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/set_virtio_net_header.v |
| -0.82% | 157.9 | 156.6 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_main_proof.v |
| -0.79% | 1970.9 | 1955.4 | -15.6 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/init_vcpus.v |
| -0.77% | 145.4 | 144.3 | -1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v |
| -0.76% | 168.1 | 166.8 | -1.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof.v |
| -0.50% | 669.5 | 666.2 | -3.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/copy.v |
| -0.40% | 266.5 | 265.4 | -1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/proof.v |
| -0.36% | 330.8 | 329.6 | -1.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/hints.v |
| -0.29% | 1160.2 | 1156.8 | -3.4 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v |
| -0.21% | 862.8 | 861.0 | -1.8 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/proof.v |
| -0.12% | 1863.6 | 1861.5 | -2.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v |
| +0.16% | 686.2 | 687.4 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/virtual_interface.v |
| +0.32% | 491.0 | 492.6 | +1.6 | bluerock/bhv/apps/vswitch/lib/port/proof/port/proof.v |
| +0.32% | 363.5 | 364.7 | +1.2 | bluerock/bhv/zeta/lib/lang/proof/atomic_hpp_proof.v |
| +0.35% | 392.8 | 394.2 | +1.4 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/extract_frame_header.v |
| +0.59% | 200.0 | 201.1 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/elpi/enums/variant_cpp_proof.v |
| +0.75% | 250.7 | 252.6 | +1.9 | bluerock/bhv/zeta/lib/uuid/proof/uuid_hpp_proof.v |
| +0.89% | 174.9 | 176.5 | +1.5 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/defs.v |
| +1.04% | 112.8 | 114.0 | +1.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/util.v |
| +1.21% | 102.6 | 103.8 | +1.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/drop.v |
| +1.45% | 87.8 | 89.1 | +1.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/route.v |
| +1.76% | 58.3 | 59.3 | +1.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints.v |
| +2.08% | 83.0 | 84.8 | +1.7 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/drop.v |
| +2.38% | 53.6 | 54.8 | +1.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/flood.v |
| +2.53% | 57.1 | 58.6 | +1.4 | bluerock/bhv/zeta/lib/lang/proof/errno_hpp_proof.v |
| +2.53% | 86.9 | 89.1 | +2.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/send.v |
| +2.68% | 78.3 | 80.4 | +2.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/pkt.v |
| +2.70% | 67.4 | 69.2 | +1.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/copy_frame.v |
| +3.17% | 69.4 | 71.6 | +2.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/extract_frame_header.v |
| +3.78% | 40.4 | 42.0 | +1.5 | bluerock/bhv/zeta/lib/lang/proof/memory_barrier.v |
| +3.90% | 33.8 | 35.1 | +1.3 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/model/virtq/state/descriptor_table.v |
| +3.96% | 38.5 | 40.0 | +1.5 | bluerock/bhv/zeta/lib/bson/proof/bson.v |
| +5.15% | 28.2 | 29.7 | +1.5 | bluerock/bhv/zeta/lib/cxx/proof/range_hpp_spec.v |
| +5.64% | 20.1 | 21.2 | +1.1 | bluerock/bhv/lib/ddk/proof/utils.v |
| +6.90% | 15.0 | 16.0 | +1.0 | bluerock/bhv/zeta/lib/lang/proof/util.v |
| +40.56% | 10.6 | 14.9 | +4.3 | fmdeps/auto/rocq-skylabs-auto-core/theories/internal/ltac2_dnet.v |
| -0.06% | 126163.5 | 126093.5 | -70.0 | total |
| +0.00% | 22792.9 | 22792.5 | +0.4 | ├ translation units |
| -0.07% | 103300.6 | 103371.0 | -70.4 | └ proofs and tests |
6 tasks
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.
Fixes / closes #????
make doc_gram_rsts.