Kernel: physical-equality fast paths in conversion's compare_under#22299
Merged
coqbot-app[bot] merged 1 commit intoJul 24, 2026
Merged
Conversation
`compare_under` is the syntactic pre-check that lets conversion accept two closures without invoking the reduction machine. It walked both terms structurally even when they were physically identical, and treated matching Case/Fix/CoFix nodes as an unconditional failure (an explicit "todo"), forcing identical match-bearing terms through full reduction. Add a physical-equality shortcut (same term pointer under equal, or both trivial, substitutions and universe instances is immediately convertible) and structural comparison of Case/Fix/CoFix nodes. Both only strengthen a sufficient acceptance condition — each new case implies the two sides are literally equal — so they can accept but never reject, preserving the conversion relation. On a telescope-heavy kernel check where 95% of compare_under calls compare a term against itself, this roughly halves the check.
coqbot-app
Bot
added
the
needs: full CI
Contributor
|
@coqbot bench |
Contributor
|
🏁 Bench results: INFO: failed to install rocq-mathcomp-boot (dependency rocq-elpi failed) 🐢 Top 25 slow downs┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 43.7 45.4 1.7399 3.98% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 49.4 50.5 1.1157 2.26% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 1.37 2.38 1.0100 73.82% 574 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 47.1 48.0 0.9475 2.01% 277 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 14.8 15.7 0.8923 6.02% 833 coq-unimath/UniMath/CategoryTheory/ComprehensionCats/CwfFromCompCatWithUniv.v.html │ │ 76.8 77.7 0.8815 1.15% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 24.6 25.3 0.7194 2.92% 550 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 19.4 20.1 0.6382 3.28% 543 coq-unimath/UniMath/CategoryTheory/Presheaves/SigmaTypes.v.html │ │ 89.0 89.5 0.5525 0.62% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 40.1 40.7 0.5351 1.33% 1423 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 26.6 27.1 0.5348 2.01% 34 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │ │ 16.9 17.4 0.5051 2.98% 905 coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html │ │ 27.0 27.5 0.4768 1.77% 794 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 24.8 25.2 0.4741 1.91% 550 coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 89.2 89.6 0.4391 0.49% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 21.2 21.6 0.4231 1.99% 338 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 15.861 16.283 0.4220 2.66% 1515 coq-vst/floyd/VSU.v.html │ │ 4.32 4.73 0.4108 9.52% 526 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 4.71 5.11 0.3999 8.49% 580 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 15.887 16.282 0.3950 2.49% 1223 coq-vst/floyd/Component.v.html │ │ 102 102 0.3784 0.37% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 37.9 38.2 0.3716 0.98% 244 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 28.5 28.9 0.3521 1.23% 31 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │ │ 3.68 3.99 0.3071 8.35% 554 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 16.5 16.8 0.3032 1.84% 669 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 35.353 29.757 -5.5960 -15.83% 147 coq-vst/veric/expr_lemmas4.v.html │ │ 5.681 0.223 -5.4580 -96.07% 1177 coq-vst/veric/expr_lemmas.v.html │ │ 5.61 0.22 -5.3900 -96.08% 2434 coq-vst/veric/semax_call.v.html │ │ 5.732 0.344 -5.3880 -94.00% 2883 coq-vst/veric/semax_call.v.html │ │ 34.27 29.288 -4.9820 -14.54% 194 coq-vst/veric/expr_lemmas4.v.html │ │ 68.2 64.0 -4.2727 -6.26% 608 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 67.3 65.6 -1.7547 -2.61% 608 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 13.8 12.1 -1.7434 -12.62% 216 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 16.7 15.0 -1.6661 -9.97% 6 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeCSR.v.html │ │ 8.19 7.28 -0.9048 -11.05% 571 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 201 200 -0.8462 -0.42% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 1.08 0.250 -0.8337 -76.91% 928 coq-unimath/UniMath/CategoryTheory/ComprehensionCats/CwfFromCompCatWithUniv.v.html │ │ 28.8 28.3 -0.5186 -1.80% 145 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 2.37 1.86 -0.5079 -21.41% 930 coq-neural-net-interp-computed-lite/theories/TransformerLens/HookedTransformer/Module.v.html │ │ 27.0 26.5 -0.5048 -1.87% 148 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 12.0 11.5 -0.5038 -4.20% 118 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 0.543 0.041 -0.5020 -92.45% 74 coq-vst/veric/expr_lemmas2.v.html │ │ 42.7 42.2 -0.4869 -1.14% 539 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 35.7 35.2 -0.4703 -1.32% 898 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 18.7 18.3 -0.4515 -2.41% 32 coq-performance-tests-lite/src/pattern.v.html │ │ 4.36 3.96 -0.4062 -9.31% 190 coq-unimath/UniMath/Algebra/Universal/Examples/Tests.v.html │ │ 20.4 20.0 -0.3902 -1.91% 6 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.v.html │ │ 2.50 2.14 -0.3537 -14.17% 323 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/RecodeProofs.v.html │ │ 0.342 0.018 -0.3240 -94.74% 421 coq-vst/veric/expr_lemmas2.v.html │ │ 10.6 10.3 -0.3178 -3.01% 2300 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
Contributor
|
@coqbot run full ci |
coqbot-app
Bot
removed
the
needs: full CI
Contributor
|
🔴 CI failure at commit c9b523d without any failure in the test-suite ✔️ Corresponding job for the base commit 3403def succeeded ❔ Ask me to try to extract a minimal test case that can be added to the test-suite 🏃
|
Member
|
Note: this PR divides by 2 the time of some very long |
Contributor
Author
Yes, the original motivation for this PR is to improve performance of Rocq on the work-in-progress formalization of extension of the Bonak's semi-simplicial set construction to semi-simplicial groupoids. This change gives a ~2x improvement, a reduction from ~15 min to ~7 min on my laptop, also assuming #22272 change. The exact problematic |
SkySkimmer
added
the
kind: performance
SkySkimmer
approved these changes
Jul 24, 2026
SkySkimmer
left a comment
SkySkimmer
left a comment
Contributor
There was a problem hiding this comment.
seems fine to me
@ppedrot WDYT?
Member
|
Assuming I haven't missed some subtle invariant, the change looks good to me. |
Contributor
|
@coqbot merge now |
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
4 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.
Kernel: physical-equality fast paths in conversion's
compare_underAbout
compare_underis the syntactic pre-check that lets conversion accept two closures without invoking the reduction machine. It walked both terms structurally even when they were physically identical, and treated matchingCase/Fix/CoFixnodes as an unconditional failure (an explicittodo), forcing identical match-bearing terms through full reduction.Overview
Changes introduced in this PR:
c1 == c2) under substitutions and universe instances that are equal — or both trivial — the two closures are immediately convertible, with no structural walk.Case/Fix/CoFixnodes, replacing the old-> false (* todo some other time *)catch-all.