Fast path for Reductionops kernel-defined functions.#22143
Draft
ppedrot wants to merge 1 commit into
Draft
Conversation
We do not call normalization when the argument is already in head normal form. Note that for some reason the code still relies on the term being evar-expanded, so we do implement this carefully. This fast path seems to be quite important for VM normalization, as most constructors of inductive types already have a type in head normal form. On a micro-benchmark designed to measure VM reification of big first-order terms, this gives a 20% speedup.
ppedrot
added
request: full CI
coqbot-app
Bot
removed
the
request: full CI
Member
Author
|
@coqbot bench |
SkySkimmer
reviewed
Jun 19, 2026
| | Const _ | Case _ | Fix _ | CoFix _ | Proj _ -> | ||
| Reductionops.clos_whd_flags RedFlags.all env sigma t | ||
| end | ||
| | Rel _ | Evar _ | Cast _ | LetIn _ | Case _ | Proj _ | Const _ | Var _ -> |
Contributor
There was a problem hiding this comment.
isn't Evar in whnf? since it's from EConstr.kind it's undefined
Member
Author
There was a problem hiding this comment.
Technically in vnorm we only ever reduce types whose normal forms are either Π or (applied) inductives, so in practice it doesn't matter.
SkySkimmer
reviewed
Jun 19, 2026
| | Const _ | Case _ | Fix _ | CoFix _ | Proj _ -> | ||
| Reductionops.clos_whd_flags RedFlags.all env sigma t | ||
| end | ||
| | Rel _ | Evar _ | Cast _ | LetIn _ | Case _ | Proj _ | Const _ | Var _ -> |
Contributor
There was a problem hiding this comment.
would it also be worth checking definedness of Rel/Var/Const?
Contributor
|
🏁 Bench results: INFO: failed to install 🐢 Top 25 slow downs┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 236 242 5.4710 2.32% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 133 136 2.7157 2.04% 155 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 202 204 1.8866 0.94% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 80.5 81.8 1.2832 1.59% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 106 107 1.0511 0.99% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 83.0 83.8 0.8795 1.06% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 7.83 8.68 0.8435 10.77% 1331 coq-mathcomp-odd-order/theories/PFsection9.v.html │ │ 20.4 21.0 0.6397 3.14% 24 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html │ │ 16.3 17.0 0.6325 3.87% 762 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 3.62 4.24 0.6219 17.18% 196 rocq-stdlib/theories/ZArith/ZModOffset.v.html │ │ 55.0 55.6 0.6119 1.11% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 89.9 90.4 0.5509 0.61% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 22.3 22.8 0.5459 2.45% 776 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 21.4 21.9 0.5359 2.50% 651 rocq-stdlib/theories/Zmod/ZmodBase.v.html │ │ 23.5 24.0 0.5184 2.20% 782 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 43.1 43.6 0.4981 1.16% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 53.8 54.3 0.4799 0.89% 296 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html │ │ 21.1 21.6 0.4764 2.26% 516 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 9.25 9.71 0.4589 4.96% 435 coq-mathcomp-odd-order/theories/PFsection12.v.html │ │ 54.7 55.2 0.4500 0.82% 512 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 0.761 1.20 0.4438 58.34% 215 rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html │ │ 21.4 21.8 0.4006 1.87% 49 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 44.7 45.1 0.3825 0.86% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html │ │ 0.000083 0.380 0.3804 458325.30% 81 coq-mathcomp-analysis/theories/hoelder.v.html │ │ 22.8 23.1 0.3433 1.51% 85 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/AffineProofs.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 27.9 24.7 -3.2411 -11.61% 129 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ │ 2.45 1.36 -1.0972 -44.73% 574 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 43.9 43.1 -0.8218 -1.87% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 9.78 9.03 -0.7501 -7.67% 87 coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html │ │ 64.6 63.9 -0.6720 -1.04% 608 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 2.48 1.89 -0.5936 -23.91% 32 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 48.1 47.6 -0.5320 -1.11% 277 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 27.7 27.2 -0.4868 -1.76% 34 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │ │ 18.7 18.2 -0.4802 -2.57% 32 coq-performance-tests-lite/src/pattern.v.html │ │ 29.6 29.2 -0.4507 -1.52% 31 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │ │ 26.1 25.6 -0.4505 -1.73% 13 coq-fourcolor/theories/proof/job466to485.v.html │ │ 90.6 90.2 -0.4072 -0.45% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 37.0 36.6 -0.3899 -1.05% 139 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 36.7 36.4 -0.3796 -1.03% 222 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 0.995 0.615 -0.3792 -38.12% 41 rocq-stdlib/theories/ZArith/Zdiv_facts.v.html │ │ 26.8 26.4 -0.3588 -1.34% 374 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 0.561 0.221 -0.3403 -60.61% 4 rocq-stdlib/theories/extraction/ExtrHaskellZInteger.v.html │ │ 0.344 0.00481 -0.3392 -98.60% 112 coq-mathcomp-analysis/theories/esum.v.html │ │ 29.3 29.0 -0.3269 -1.12% 145 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 0.587 0.262 -0.3256 -55.43% 13 rocq-stdlib/theories/ZArith/Zmin.v.html │ │ 30.2 29.9 -0.3250 -1.08% 13 coq-fourcolor/theories/proof/job165to189.v.html │ │ 0.679 0.355 -0.3234 -47.63% 719 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 25.6 25.2 -0.3124 -1.22% 224 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 31.0 30.7 -0.3096 -1.00% 223 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 4.27 3.97 -0.3065 -7.17% 576 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
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.
We do not call normalization when the argument is already in head normal form. Note that for some reason the code still relies on the term being evar-expanded, so we do implement this carefully.
This fast path seems to be quite important for VM normalization, as most constructors of inductive types already have a type in head normal form. On a micro-benchmark designed to measure VM reification of big first-order terms, this gives a 20% speedup.
Here is the code of the micro-benchmark: