Janno/cbn delayed subst#11
Closed
Janno wants to merge 26 commits into
Closed
Conversation
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | 7d2ee30 |
| fmdeps/BRiCk/ | main | 9d3083c |
| fmdeps/auto/ | main | 003f68d |
| fmdeps/auto-docs/ | main | 624d55f |
| bluerock/NOVA/ | skylabs-proof | 6cbef03 |
| bluerock/bhv/ | skylabs-main | b7085c3 |
| fmdeps/brick-libcpp/ | main | 2014908 |
| fmdeps/ci/ | main | 9e6e574 |
| vendored/elpi/ | skylabs-master | aa4475f |
| vendored/flocq/ | skylabs-master | cf9cc84 |
| fmdeps/fm-tools/ | main | fb160a9 |
| 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 |
|---|---|---|---|---|
| -33.68% | 126110.8 | 83640.5 | -42470.3 | total |
| -33.58% | 42350.7 | - | -42350.7 | ├ disappeared files (291) |
| -0.14% | 83640.5 | 83760.1 | -119.6 | └ common files |
| -0.02% | 22783.9 | 22788.6 | -4.7 | ├ translation units |
| -0.19% | 60856.6 | 60971.5 | -114.9 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -36.10% | 12.1 | 7.8 | -4.4 | fmdeps/auto/rocq-skylabs-auto-core/tests/warnings.v |
| -18.88% | 56.5 | 45.8 | -10.7 | fmdeps/auto/rocq-skylabs-auto-core/tests/cancelx_tactic.v |
| -10.05% | 64.6 | 58.1 | -6.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/pair_hpp_spec.v |
| -8.94% | 50.0 | 45.5 | -4.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep_spec.v |
| -8.74% | 47.7 | 43.5 | -4.2 | bluerock/bhv/apps/vswitch/proof/model/ethernet.v |
| -6.37% | 144.3 | 135.1 | -9.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/splice_cpp_spec.v |
| -5.40% | 50.6 | 47.8 | -2.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/initlist_cpp_proof.v |
| -4.35% | 57.2 | 54.7 | -2.5 | bluerock/bhv/zeta/lib/lang/proof/errno_hpp_proof.v |
| -4.10% | 202.0 | 193.7 | -8.3 | fmdeps/auto/rocq-skylabs-auto-core/tests/subgoals.v |
| -3.75% | 34.6 | 33.3 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/default_specs_1.v |
| -2.01% | 491.6 | 481.7 | -9.9 | bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/access.v |
| -1.64% | 167.8 | 165.0 | -2.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/fields/test_cpp_proof.v |
| -1.58% | 90.0 | 88.6 | -1.4 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctor.v |
| -1.36% | 99.1 | 97.8 | -1.3 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/start_cpu.v |
| -1.14% | 497.7 | 492.0 | -5.7 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/vector/test_cpp_proof.v |
| -1.03% | 277.0 | 274.1 | -2.8 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create.v |
| -0.94% | 169.7 | 168.1 | -1.6 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_other.v |
| -0.86% | 260.9 | 258.7 | -2.2 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sm.v |
| -0.85% | 201.6 | 199.8 | -1.7 | bluerock/NOVA/build-proof/proof/sc_cpp_proof/create.v |
| -0.82% | 258.8 | 256.7 | -2.1 | bluerock/bhv/apps/vmm/lib/bluerock/proof/aarch64/reg_accessor_hpp_proof.v |
| -0.81% | 347.0 | 344.2 | -2.8 | bluerock/bhv/apps/umx/proof/main_cpp_proof/input_loop.v |
| -0.80% | 225.3 | 223.5 | -1.8 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_read_console_id.v |
| -0.78% | 464.0 | 460.4 | -3.6 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pd.v |
| -0.73% | 176.3 | 175.0 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/data_class/class_32_cpp_proof.v |
| -0.72% | 149.1 | 148.0 | -1.1 | bluerock/NOVA/build-proof/proof/pt_cpp_proof/create.v |
| -0.70% | 197.7 | 196.4 | -1.4 | bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_public.v |
| -0.62% | 554.9 | 551.5 | -3.4 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sc.v |
| -0.61% | 171.7 | 170.6 | -1.1 | bluerock/NOVA/build-proof/proof/sm_cpp_proof/create.v |
| -0.50% | 683.8 | 680.4 | -3.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/call_cpp_proof.v |
| -0.48% | 485.0 | 482.7 | -2.3 | bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/zynqmp_dma_ver_cpp_proof.v |
| -0.45% | 363.7 | 362.1 | -1.6 | bluerock/bhv/zeta/lib/lang/proof/atomic_hpp_proof.v |
| -0.44% | 238.7 | 237.7 | -1.0 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/read_line.v |
| -0.41% | 464.5 | 462.6 | -1.9 | bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_private.v |
| -0.40% | 305.8 | 304.5 | -1.2 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pt.v |
| -0.37% | 361.3 | 359.9 | -1.3 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/schedule.v |
| -0.34% | 380.3 | 379.1 | -1.3 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_sm.v |
| -0.30% | 339.3 | 338.3 | -1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/llist/merge_cpp_proof.v |
| -0.29% | 538.2 | 536.7 | -1.6 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/ready_queues.v |
| +0.27% | 527.0 | 528.4 | +1.4 | bluerock/bhv/lib/drivers/serial/pl011/proof/pl011_cpp_proof.v |
| +0.31% | 895.0 | 897.8 | +2.8 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/atomic/test_cpp_proof.v |
| +0.39% | 424.2 | 425.8 | +1.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/arith_cpp_proof.v |
| +0.57% | 177.5 | 178.5 | +1.0 | bluerock/bhv/zeta/lib/msc/proof/sys/rwlock_hpp_proof.v |
| +0.67% | 213.4 | 214.8 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_main_proof.v |
| +0.67% | 280.3 | 282.2 | +1.9 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/delegate.v |
| +0.76% | 303.8 | 306.2 | +2.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_main_proof.v |
| +0.80% | 145.4 | 146.6 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v |
| +0.87% | 142.6 | 143.9 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v |
| +1.14% | 177.1 | 179.2 | +2.0 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_base_proof.v |
| +1.58% | 79.8 | 81.0 | +1.3 | bluerock/bhv/zeta/lib/cxx/proof/sys/mutex_hpp_proof.v |
| +1.88% | 103.6 | 105.5 | +2.0 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_proof.v |
| +1.89% | 114.2 | 116.4 | +2.2 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_rich_proof.v |
| +3.74% | 33.8 | 35.1 | +1.3 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/model/virtq/state/descriptor_table.v |
| +3.84% | 40.4 | 42.0 | +1.6 | bluerock/bhv/zeta/lib/lang/proof/memory_barrier.v |
| +5.68% | 20.1 | 21.2 | +1.1 | bluerock/bhv/lib/ddk/proof/utils.v |
| +7.50% | 59.3 | 63.8 | +4.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/micromega/micromega1.v |
| +9.01% | 20.9 | 22.8 | +1.9 | bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/mutex_hpp_proof.v |
| +10.79% | 10.8 | 12.0 | +1.2 | fmdeps/auto/rocq-skylabs-auto-core/theories/internal/ltac2_dnet.v |
| -33.68% | 126110.8 | 83640.5 | -42470.3 | total |
| -33.58% | 42350.7 | - | -42350.7 | ├ disappeared files (291) |
| -0.14% | 83640.5 | 83760.1 | -119.6 | └ common files |
| -0.02% | 22783.9 | 22788.6 | -4.7 | ├ translation units |
| -0.19% | 60856.6 | 60971.5 | -114.9 | └ proofs and tests |
Janno
force-pushed
the
janno/cbn-delayed-subst
branch
from
25c1be4 to
23c7507
Compare
GPT-5.5 comment: Root cause: norm_cbn was normalizing suspended Fix/Case/Cst stack bodies before trying constant-stack refolding. For HexString.v/OctalString.v, that expanded stuck fixpoint bodies and then unfolded ascii_dec on variables, causing the apparent divergence.
The LLM says: - Cached CbnClos.force for non-identity delayed substitutions. - Added closure-level application reconstruction to avoid internal stack_zip forcing in recursive/refolding continuations. - Delayed local Rel unfolding lift via CbnClos.lift instead of eager lift. - Made fix/cofix self-refolding keep parameter closures instead of forcing params. - Avoided computing refold references for non-mutual fix/cofixes. - Added Stack.best_state_opt so strong norm_cbn no longer builds fully forced raw case/fix/proj terms just to discover refolding failed. - Made rewrite-rule matching avoid upfront forcing for ignored holes / rigid patterns.
The LLM says: What was wrong: - perf showed the bad run spending time in Cbn.norm_zip / Array.map, with repeated Cbn.kind / Esubst.expand_rel. - The new norm_cbn was recursively normalizing delayed stack application arguments before surrounding Case/Fix/constant frames could refold or discard them. - On cbn_hott.v, that turned large delayed closures into repeated full traversals. Fix: - Restored the master-style strong-normalization control flow: first call whd_cbn, which zips/refolds the weak-head state, then recurse with Termops.map_constr_with_full_binders. - Added a comment documenting why refolding must happen before recursive descent. - Removed the now-unused Stack.best_state_opt export from the module signature.
Janno
force-pushed
the
janno/cbn-delayed-subst
branch
from
23c7507 to
c398a60
Compare
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 |
|---|---|---|---|---|
| -98.63% | 126163.5 | 1727.4 | -124436.0 | total |
| -98.63% | 124440.9 | - | -124440.9 | ├ disappeared files (2627) |
| +0.28% | 1727.4 | 1722.6 | +4.9 | └ common files |
| +0.28% | 1727.4 | 1722.6 | +4.9 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| +39.67% | 10.6 | 14.8 | +4.2 | fmdeps/auto/rocq-skylabs-auto-core/theories/internal/ltac2_dnet.v |
| -98.63% | 126163.5 | 1727.4 | -124436.0 | total |
| -98.63% | 124440.9 | - | -124440.9 | ├ disappeared files (2627) |
| +0.28% | 1727.4 | 1722.6 | +4.9 | └ common files |
| +0.28% | 1727.4 | 1722.6 | +4.9 | └ 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.12% | 126163.5 | 126015.4 | -148.1 | total |
| +0.05% | 22802.9 | 22792.5 | +10.4 | ├ translation units |
| -0.15% | 103212.5 | 103371.0 | -158.5 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -18.86% | 56.5 | 45.8 | -10.7 | fmdeps/auto/rocq-skylabs-auto-core/tests/cancelx_tactic.v |
| -13.43% | 10.6 | 9.2 | -1.4 | fmdeps/auto/rocq-skylabs-auto-core/theories/internal/ltac2_dnet.v |
| -10.05% | 64.7 | 58.2 | -6.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/pair_hpp_spec.v |
| -8.68% | 50.0 | 45.7 | -4.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep_spec.v |
| -8.35% | 47.7 | 43.7 | -4.0 | bluerock/bhv/apps/vswitch/proof/model/ethernet.v |
| -6.87% | 63.8 | 59.4 | -4.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/micromega/micromega1.v |
| -6.29% | 144.3 | 135.2 | -9.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/splice_cpp_spec.v |
| -5.14% | 50.6 | 48.0 | -2.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/initlist_cpp_proof.v |
| -4.21% | 57.1 | 54.7 | -2.4 | bluerock/bhv/zeta/lib/lang/proof/errno_hpp_proof.v |
| -3.50% | 34.6 | 33.4 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/default_specs_1.v |
| -2.78% | 137.8 | 134.0 | -3.8 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/proof.v |
| -2.77% | 230.6 | 224.2 | -6.4 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort_to_vbus.v |
| -2.36% | 46.6 | 45.5 | -1.1 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ipc_call.v |
| -2.13% | 151.0 | 147.8 | -3.2 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/compute_gpa_fault_addr.v |
| -2.02% | 491.6 | 481.7 | -9.9 | bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/access.v |
| -1.87% | 475.2 | 466.3 | -8.9 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/msr_framework.v |
| -1.84% | 1160.2 | 1138.8 | -21.4 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v |
| -1.74% | 99.2 | 97.5 | -1.7 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/start_cpu.v |
| -1.74% | 70.1 | 68.9 | -1.2 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/unblock.v |
| -1.56% | 167.8 | 165.2 | -2.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/fields/test_cpp_proof.v |
| -1.47% | 78.1 | 77.0 | -1.2 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/release_queue.v |
| -1.44% | 194.0 | 191.2 | -2.8 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/create_forwarding_plane.v |
| -1.42% | 90.0 | 88.8 | -1.3 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctor.v |
| -1.41% | 72.9 | 71.9 | -1.0 | bluerock/NOVA/build-proof/proof/pt_cpp_proof/proof.v |
| -1.32% | 360.7 | 356.0 | -4.8 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/handle_data_abort.v |
| -1.30% | 357.9 | 353.2 | -4.6 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort.v |
| -1.26% | 156.3 | 154.4 | -2.0 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_roundedup.v |
| -1.24% | 83.0 | 82.0 | -1.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/drop.v |
| -1.19% | 95.6 | 94.4 | -1.1 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/get_fdt_from_uuid.v |
| -1.13% | 726.4 | 718.2 | -8.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/misc.v |
| -1.12% | 168.1 | 166.2 | -1.9 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof.v |
| -1.11% | 497.7 | 492.2 | -5.5 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/vector/test_cpp_proof.v |
| -0.96% | 276.9 | 274.3 | -2.7 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create.v |
| -0.86% | 169.7 | 168.2 | -1.5 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_other.v |
| -0.86% | 514.6 | 510.2 | -4.4 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/run_vm.v |
| -0.82% | 1970.9 | 1954.7 | -16.2 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/init_vcpus.v |
| -0.80% | 862.8 | 855.9 | -6.9 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/proof.v |
| -0.75% | 225.2 | 223.5 | -1.7 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_read_console_id.v |
| -0.75% | 266.5 | 264.5 | -2.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/proof.v |
| -0.74% | 347.0 | 344.4 | -2.6 | bluerock/bhv/apps/umx/proof/main_cpp_proof/input_loop.v |
| -0.73% | 240.8 | 239.1 | -1.7 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/flood.v |
| -0.71% | 176.3 | 175.1 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/data_class/class_32_cpp_proof.v |
| -0.69% | 258.8 | 257.0 | -1.8 | bluerock/bhv/apps/vmm/lib/bluerock/proof/aarch64/reg_accessor_hpp_proof.v |
| -0.68% | 202.1 | 200.7 | -1.4 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/queue/misc.v |
| -0.68% | 192.3 | 191.0 | -1.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/set_virtio_net_header.v |
| -0.68% | 1530.0 | 1519.7 | -10.4 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/prepare_address_space.v |
| -0.62% | 211.7 | 210.4 | -1.3 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/ctor.v |
| -0.61% | 686.2 | 682.1 | -4.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/virtual_interface.v |
| -0.60% | 197.7 | 196.5 | -1.2 | bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_public.v |
| -0.60% | 1863.6 | 1852.6 | -11.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v |
| -0.59% | 1092.6 | 1086.1 | -6.5 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/zeta_main.v |
| -0.58% | 464.0 | 461.3 | -2.7 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pd.v |
| -0.57% | 1693.0 | 1683.4 | -9.6 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/reset.v |
| -0.54% | 189.6 | 188.5 | -1.0 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/initialize_dataplane.v |
| -0.51% | 260.9 | 259.5 | -1.3 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sm.v |
| -0.48% | 305.8 | 304.3 | -1.5 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pt.v |
| -0.47% | 485.1 | 482.8 | -2.3 | bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/zynqmp_dma_ver_cpp_proof.v |
| -0.47% | 380.4 | 378.6 | -1.8 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_sm.v |
| -0.46% | 972.6 | 968.2 | -4.4 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_cpp_proof.v |
| -0.44% | 330.8 | 329.4 | -1.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/transaction_protocol/hints.v |
| -0.42% | 683.8 | 681.0 | -2.9 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/call_cpp_proof.v |
| -0.42% | 363.5 | 362.0 | -1.5 | bluerock/bhv/zeta/lib/lang/proof/atomic_hpp_proof.v |
| -0.41% | 275.8 | 274.7 | -1.1 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_on.v |
| -0.38% | 650.0 | 647.5 | -2.5 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/misc.v |
| -0.37% | 325.9 | 324.7 | -1.2 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/resume.v |
| -0.37% | 464.3 | 462.6 | -1.7 | bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_private.v |
| -0.34% | 361.4 | 360.2 | -1.2 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/schedule.v |
| -0.32% | 554.8 | 553.0 | -1.8 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sc.v |
| -0.31% | 508.9 | 507.3 | -1.6 | bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/recv.v |
| -0.31% | 335.9 | 334.9 | -1.0 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/walk.v |
| -0.26% | 491.0 | 489.7 | -1.3 | bluerock/bhv/apps/vswitch/lib/port/proof/port/proof.v |
| -0.25% | 538.3 | 537.0 | -1.3 | bluerock/NOVA/build-proof/proof/scheduler_cpp_proof/ready_queues.v |
| -0.24% | 780.8 | 778.9 | -1.9 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_proof.v |
| -0.15% | 942.1 | 940.7 | -1.4 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/setup.v |
| +0.12% | 894.9 | 896.0 | +1.0 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/atomic/test_cpp_proof.v |
| +0.30% | 527.0 | 528.6 | +1.6 | bluerock/bhv/lib/drivers/serial/pl011/proof/pl011_cpp_proof.v |
| +0.32% | 759.5 | 761.9 | +2.5 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/setup.v |
| +0.33% | 315.4 | 316.4 | +1.0 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/read_write_proof.v |
| +0.52% | 424.2 | 426.4 | +2.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/arith_cpp_proof.v |
| +0.65% | 180.3 | 181.4 | +1.2 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/spec.v |
| +0.73% | 280.3 | 282.4 | +2.1 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/delegate.v |
| +0.76% | 213.4 | 215.0 | +1.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_main_proof.v |
| +0.79% | 904.9 | 912.0 | +7.2 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_default_impl.v |
| +0.81% | 303.8 | 306.3 | +2.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_main_proof.v |
| +0.85% | 174.9 | 176.4 | +1.5 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/defs.v |
| +0.85% | 1699.1 | 1713.6 | +14.5 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_glue.v |
| +0.91% | 145.4 | 146.8 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v |
| +0.94% | 142.6 | 144.0 | +1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v |
| +1.00% | 112.8 | 113.9 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/util.v |
| +1.01% | 392.8 | 396.8 | +4.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/extract_frame_header.v |
| +1.04% | 102.6 | 103.7 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/drop.v |
| +1.60% | 1243.4 | 1263.3 | +19.9 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/sync_impl.v |
| +1.77% | 58.3 | 59.3 | +1.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints.v |
| +2.27% | 87.8 | 89.8 | +2.0 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/route.v |
| +2.28% | 78.3 | 80.1 | +1.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/pkt.v |
| +2.63% | 53.6 | 55.0 | +1.4 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/flood.v |
| +2.73% | 67.4 | 69.2 | +1.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/copy_frame.v |
| +3.30% | 34.2 | 35.3 | +1.1 | bluerock/NOVA/build-proof/proof/iface/predicates/ec.v |
| +3.35% | 69.4 | 71.7 | +2.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/extract_frame_header.v |
| +4.11% | 40.4 | 42.1 | +1.7 | bluerock/bhv/zeta/lib/lang/proof/memory_barrier.v |
| +4.70% | 26.7 | 27.9 | +1.3 | bluerock/NOVA/build-proof/proof/iface/predicates/sc.v |
| +4.75% | 26.1 | 27.3 | +1.2 | bluerock/NOVA/build-proof/proof/iface/predicates/mem.v |
| +4.83% | 23.7 | 24.8 | +1.1 | bluerock/NOVA/build-proof/proof/iface/predicates/dma.v |
| +4.91% | 25.3 | 26.5 | +1.2 | bluerock/NOVA/build-proof/proof/iface/predicates/pd.v |
| +15.59% | 7.7 | 8.8 | +1.2 | fmdeps/auto/rocq-skylabs-auto-core/tests/warnings.v |
| -0.12% | 126163.5 | 126015.4 | -148.1 | total |
| +0.05% | 22802.9 | 22792.5 | +10.4 | ├ translation units |
| -0.15% | 103212.5 | 103371.0 | -158.5 | └ proofs and tests |
CI summary (Details)Active Repos
|
| Repo | Job Branch | Job Commit |
|---|---|---|
| ./ | main | 7d2ee30 |
| fmdeps/BRiCk/ | main | b96cddc |
| fmdeps/auto/ | main | ee152ab |
| 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 | 82cb305 |
| 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 | 6a99b06 |
| vendored/vsrocq/ | skylabs-main | 5b4527e |
Performance
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -0.29% | 127291.9 | 126920.8 | -371.1 | total |
| -0.00% | 22688.9 | 22689.7 | -0.8 | ├ translation units |
| -0.35% | 104231.9 | 104602.2 | -370.3 | └ proofs and tests |
Full Results
| Relative | Master | MR | Change | Filename |
|---|---|---|---|---|
| -18.87% | 56.5 | 45.8 | -10.7 | fmdeps/auto/rocq-skylabs-auto-core/tests/cancelx_tactic.v |
| -10.20% | 64.7 | 58.1 | -6.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/pair_hpp_spec.v |
| -10.11% | 47.7 | 42.9 | -4.8 | bluerock/bhv/apps/vswitch/proof/model/ethernet.v |
| -8.84% | 50.0 | 45.6 | -4.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/big_sep_spec.v |
| -6.35% | 144.3 | 135.1 | -9.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/templates/splice_cpp_spec.v |
| -5.24% | 51.6 | 48.9 | -2.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/array/initlist_cpp_proof.v |
| -5.21% | 1241.9 | 1177.2 | -64.7 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/sync_impl.v |
| -4.20% | 58.5 | 56.1 | -2.5 | bluerock/bhv/zeta/lib/lang/proof/errno_hpp_proof.v |
| -3.83% | 34.7 | 33.3 | -1.3 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/default_specs_1.v |
| -3.73% | 85.7 | 82.5 | -3.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/send.v |
| -3.41% | 80.5 | 77.8 | -2.7 | bluerock/bhv/apps/umx/proof/main_cpp_proof/setup_sigs.v |
| -3.02% | 525.6 | 509.7 | -15.9 | bluerock/bhv/lib/drivers/serial/pl011/proof/pl011_cpp_proof.v |
| -2.55% | 340.4 | 331.7 | -8.7 | bluerock/bhv/apps/umx/proof/main_cpp_proof/setup.v |
| -2.48% | 103.0 | 100.5 | -2.6 | bluerock/bhv/lib/vrl/proof/vrl/port_hpp_proof.v |
| -2.41% | 188.3 | 183.7 | -4.5 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/initialize_dataplane.v |
| -2.37% | 192.7 | 188.2 | -4.6 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/create_forwarding_plane.v |
| -2.30% | 491.7 | 480.4 | -11.3 | bluerock/bhv/apps/vmm/vml/devices/vpl011/proof/pl011_proof/access.v |
| -2.27% | 136.7 | 133.6 | -3.1 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/proof.v |
| -2.27% | 48.6 | 47.5 | -1.1 | bluerock/bhv/apps/umx/proof/main_cpp_proof/setup_output_loop_thread.v |
| -2.24% | 229.2 | 224.0 | -5.1 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort_to_vbus.v |
| -2.14% | 190.3 | 186.2 | -4.1 | bluerock/bhv/apps/umx/proof/main_cpp_proof/parse_connect_args.v |
| -2.09% | 861.3 | 843.2 | -18.0 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_cpp/proof.v |
| -2.07% | 485.2 | 475.2 | -10.0 | bluerock/bhv/lib/drivers/dma/zynqmp_dma/proof/zynqmp_dma_ver_cpp_proof.v |
| -2.05% | 1698.3 | 1663.5 | -34.8 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_glue.v |
| -2.02% | 114.2 | 111.9 | -2.3 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_rich_proof.v |
| -1.94% | 1863.8 | 1827.7 | -36.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/copy_frame.v |
| -1.88% | 1158.8 | 1137.0 | -21.8 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/route.v |
| -1.77% | 90.3 | 88.7 | -1.6 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/ctor.v |
| -1.75% | 191.0 | 187.7 | -3.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/set_virtio_net_header.v |
| -1.62% | 99.4 | 97.8 | -1.6 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/start_cpu.v |
| -1.58% | 473.5 | 466.0 | -7.5 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/msr_framework.v |
| -1.57% | 193.5 | 190.5 | -3.0 | bluerock/bhv/apps/vmm/lib/dynamic_as/proof/space_view_cpp_proof/space_sel.v |
| -1.53% | 684.9 | 674.5 | -10.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/virtual_interface.v |
| -1.52% | 170.3 | 167.8 | -2.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/fields/test_cpp_proof.v |
| -1.51% | 149.9 | 147.6 | -2.3 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/compute_gpa_fault_addr.v |
| -1.36% | 103.6 | 102.2 | -1.4 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_proof.v |
| -1.34% | 725.2 | 715.5 | -9.7 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/misc.v |
| -1.26% | 177.2 | 175.0 | -2.2 | bluerock/bhv/zeta/lib/concurrent/proof/client_lock_hpp_base_proof.v |
| -1.22% | 146.3 | 144.5 | -1.8 | bluerock/bhv/zeta/lib/zeta/proof/semaphore_hpp_proof.v |
| -1.22% | 116.9 | 115.5 | -1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/initialization_forms.v |
| -1.10% | 496.9 | 491.5 | -5.5 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/vector/test_cpp_proof.v |
| -1.05% | 534.9 | 529.3 | -5.6 | fmdeps/auto/rocq-skylabs-auto-cpp/coverage-tests/assignment_operators.v |
| -1.03% | 359.2 | 355.5 | -3.7 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/handle_data_abort.v |
| -0.95% | 356.6 | 353.2 | -3.4 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vmexit_cpp_proof/data_abort.v |
| -0.90% | 169.7 | 168.2 | -1.5 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_other.v |
| -0.89% | 225.2 | 223.2 | -2.0 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/process_command_helpers_read_console_id.v |
| -0.84% | 258.8 | 256.6 | -2.2 | bluerock/bhv/apps/vmm/lib/bluerock/proof/aarch64/reg_accessor_hpp_proof.v |
| -0.82% | 346.7 | 343.9 | -2.8 | bluerock/bhv/apps/vswitch/lib/vsmp/proof/msg_queue_hpp/proof.v |
| -0.81% | 140.3 | 139.2 | -1.1 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_off.v |
| -0.78% | 1969.5 | 1954.1 | -15.3 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/init_vcpus.v |
| -0.74% | 156.4 | 155.2 | -1.2 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_roundedup.v |
| -0.70% | 197.7 | 196.4 | -1.4 | bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_public.v |
| -0.68% | 346.9 | 344.5 | -2.4 | bluerock/bhv/apps/umx/proof/main_cpp_proof/input_loop.v |
| -0.68% | 176.4 | 175.2 | -1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/data_class/class_32_cpp_proof.v |
| -0.65% | 391.2 | 388.6 | -2.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/extract_frame_header.v |
| -0.60% | 513.0 | 509.9 | -3.1 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/run_vm.v |
| -0.58% | 1091.3 | 1085.0 | -6.3 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/zeta_main.v |
| -0.58% | 238.8 | 237.4 | -1.4 | bluerock/bhv/apps/umx/proof/admin_cpp_proof/read_line.v |
| -0.54% | 239.6 | 238.3 | -1.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/flood.v |
| -0.54% | 1528.6 | 1520.3 | -8.2 | bluerock/bhv/apps/vmm/proof/main_cpp_proof/prepare_address_space.v |
| -0.53% | 325.9 | 324.2 | -1.7 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/resume.v |
| -0.52% | 195.9 | 194.9 | -1.0 | bluerock/bhv/zeta/lib/intrusive/proof/shared_pointer_hpp_proof.v |
| -0.52% | 275.9 | 274.4 | -1.4 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/switch_state_to_on.v |
| -0.50% | 275.6 | 274.2 | -1.4 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create.v |
| -0.47% | 464.6 | 462.4 | -2.2 | bluerock/bhv/zeta/lib/bson/proof/bson_cpp_proof_private.v |
| -0.45% | 1691.8 | 1684.2 | -7.6 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/reset.v |
| -0.45% | 229.4 | 228.4 | -1.0 | bluerock/bhv/apps/umx/proof/main_cpp_proof/user_handler.v |
| -0.44% | 757.5 | 754.2 | -3.3 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/setup.v |
| -0.43% | 462.8 | 460.8 | -2.0 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_pd.v |
| -0.43% | 364.7 | 363.2 | -1.6 | bluerock/bhv/zeta/lib/lang/proof/atomic_hpp_proof.v |
| -0.40% | 684.2 | 681.5 | -2.7 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/call_cpp_proof.v |
| -0.37% | 940.8 | 937.3 | -3.5 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/setup.v |
| -0.36% | 971.4 | 967.9 | -3.5 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/portal_cpp_proof.v |
| -0.31% | 648.9 | 646.9 | -2.0 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/misc.v |
| -0.30% | 553.3 | 551.6 | -1.7 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_create_sc.v |
| -0.30% | 396.7 | 395.6 | -1.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/conclude_chain_use.v |
| -0.17% | 779.6 | 778.2 | -1.3 | bluerock/bhv/apps/vmm/vml/vcpu/vcpu_roundup/proof/vcpu_roundup_proof.v |
| +0.11% | 894.8 | 895.8 | +1.0 | fmdeps/auto/rocq-skylabs-cpp-stdlib/tests/atomic/test_cpp_proof.v |
| +0.13% | 1149.8 | 1151.3 | +1.5 | bluerock/bhv/apps/vmm/vml/vcpu/cpu_model/proof/cpu_model_cpp_proof/reset_cpu.v |
| +0.19% | 547.8 | 548.8 | +1.0 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_sc.v |
| +0.20% | 668.3 | 669.7 | +1.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/copy.v |
| +0.28% | 377.6 | 378.6 | +1.0 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_pd.v |
| +0.35% | 318.9 | 320.0 | +1.1 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_obj.v |
| +0.41% | 903.4 | 907.1 | +3.7 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/copy/to_sg/async_default_impl.v |
| +0.43% | 424.6 | 426.4 | +1.8 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/perf/arith_cpp_proof.v |
| +0.47% | 287.0 | 288.3 | +1.3 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_sm.v |
| +0.58% | 194.9 | 196.1 | +1.1 | fmdeps/auto/rocq-skylabs-auto-core/tests/subgoals.v |
| +0.59% | 308.6 | 310.5 | +1.8 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/wp_vcpu_lemmas.v |
| +0.63% | 209.4 | 210.7 | +1.3 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/iterator.v |
| +0.67% | 281.1 | 283.0 | +1.9 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/buffer/get_set_byte_requesters.v |
| +0.68% | 151.0 | 152.0 | +1.0 | bluerock/bhv/apps/vmm/proof/main_cpp_spec.v |
| +0.71% | 147.8 | 148.8 | +1.1 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/handle_msr_exit.v |
| +0.75% | 156.4 | 157.6 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0068_cpp_main_proof.v |
| +0.77% | 211.9 | 213.5 | +1.6 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/buffer/conclude_chain_use.v |
| +0.77% | 199.9 | 201.5 | +1.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_table_hpp/hints.v |
| +0.79% | 147.6 | 148.8 | +1.2 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtqueue/proof/devq/send.v |
| +0.84% | 144.0 | 145.2 | +1.2 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0036_cpp_main_proof.v |
| +0.86% | 123.9 | 124.9 | +1.1 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/create.v |
| +0.94% | 112.1 | 113.2 | +1.1 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0092_cpp_main_proof.v |
| +0.99% | 125.0 | 126.2 | +1.2 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/lookup.v |
| +1.00% | 146.8 | 148.3 | +1.5 | bluerock/NOVA/build-proof/proof/iface/hypercall/pd.v |
| +1.00% | 141.1 | 142.5 | +1.4 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0004_cpp_main_proof.v |
| +1.04% | 120.8 | 122.0 | +1.3 | bluerock/NOVA/build-proof/proof/syscall_cpp_proof/sys_ctrl_pt.v |
| +1.06% | 110.5 | 111.7 | +1.2 | bluerock/NOVA/build-proof/proof/sm_cpp_proof/up.v |
| +1.08% | 113.3 | 114.5 | +1.2 | bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/hints.v |
| +1.09% | 102.6 | 103.7 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/drop.v |
| +1.17% | 303.0 | 306.6 | +3.6 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0096_cpp_main_proof.v |
| +1.18% | 212.1 | 214.6 | +2.5 | fmdeps/auto/rocq-skylabs-auto-cpp/tests/hammer_test/tests/test0098_cpp_main_proof.v |
| +1.20% | 279.1 | 282.5 | +3.3 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/delegate.v |
| +1.63% | 78.3 | 79.6 | +1.3 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/pkt.v |
| +1.66% | 62.5 | 63.6 | +1.0 | bluerock/bhv/apps/vmm/vml/devices/virtio_base/proof/virtio_sg/proof/linearized_desc.v |
| +1.78% | 121.7 | 123.8 | +2.2 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtual_interface.v |
| +1.81% | 125.8 | 128.1 | +2.3 | bluerock/bhv/apps/vswitch/lib/protocol/proof/ethernet_hpp/proof.v |
| +1.83% | 58.3 | 59.4 | +1.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints.v |
| +1.90% | 111.5 | 113.6 | +2.1 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/virtio_requesters/util.v |
| +1.93% | 173.1 | 176.4 | +3.3 | bluerock/bhv/apps/vswitch/lib/vswitch/proof/vswitch_hpp/defs.v |
| +2.20% | 52.4 | 53.6 | +1.2 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/recall.v |
| +2.38% | 44.0 | 45.0 | +1.0 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/vcpu_base_cpp_proof/run.v |
| +2.41% | 46.5 | 47.7 | +1.1 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/create_pio.v |
| +2.51% | 46.0 | 47.2 | +1.2 | bluerock/bhv/apps/vmm/lib/vcpu_bluerock/proof/aarch64/vcpu_cpp_proof/lec_stack_size.v |
| +2.64% | 56.7 | 58.2 | +1.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/proof/packet_ctor.v |
| +2.69% | 47.7 | 49.0 | +1.3 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/hints.v |
| +2.99% | 53.0 | 54.5 | +1.6 | bluerock/NOVA/build-proof/proof/pd_cpp_proof/hints.v |
| +3.01% | 43.5 | 44.8 | +1.3 | bluerock/bhv/apps/vswitch/proof/upstream/hints.v |
| +4.09% | 66.4 | 69.2 | +2.7 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/copy_frame.v |
| +4.18% | 86.2 | 89.8 | +3.6 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/route.v |
| +4.41% | 36.0 | 37.6 | +1.6 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/captable.v |
| +4.78% | 52.3 | 54.8 | +2.5 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_cpp/hints/flood.v |
| +5.04% | 68.2 | 71.6 | +3.4 | bluerock/bhv/apps/vswitch/lib/forwarding/proof/forwarding_plane_hpp/hints/extract_frame_header.v |
| +5.89% | 29.4 | 31.1 | +1.7 | bluerock/NOVA/build-proof/proof/space_obj_cpp_proof/prelude.v |
| +9.01% | 20.9 | 22.8 | +1.9 | bluerock/bhv/apps/vmm/lib/bluerock/proof/platform/mutex_hpp_proof.v |
| +70.94% | 9.3 | 15.9 | +6.6 | fmdeps/auto/rocq-skylabs-auto-core/theories/internal/ltac2_dnet.v |
| -0.29% | 127291.9 | 126920.8 | -371.1 | total |
| -0.00% | 22688.9 | 22689.7 | -0.8 | ├ translation units |
| -0.35% | 104231.9 | 104602.2 | -370.3 | └ 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.
Fixes / closes #????
make doc_gram_rsts.