cbn: use delayed substitution#22035
Open
Janno wants to merge 1 commit into
Open
Conversation
coqbot-app
Bot
added
the
needs: full CI
Contributor
Author
|
@coqbot bench |
Contributor
Author
|
I guess this bench job also got lost. Let's try again. @coqbot bench |
Contributor
|
🏁 Bench results: INFO: failed to install rocq-metarocq-utils (dependency rocq-equations failed) 🐢 Top 25 slow downs┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 51.1 54.9 3.7564 7.35% 567 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 59.4 62.8 3.3994 5.72% 659 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 56.0 59.3 3.2906 5.88% 512 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 41.2 44.1 2.9665 7.21% 539 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 43.7 46.4 2.7597 6.32% 256 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 54.6 56.8 2.1751 3.98% 296 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html │ │ 7.84 9.67 1.8298 23.33% 1831 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 203 205 1.8162 0.89% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 42.2 44.0 1.7457 4.13% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 31.0 32.7 1.7114 5.53% 596 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 38.5 39.8 1.2972 3.37% 1423 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 21.6 22.7 1.1335 5.25% 616 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 44.1 45.1 1.0434 2.37% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html │ │ 21.2 22.2 1.0377 4.90% 49 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 9.11 10.0 0.8983 9.86% 435 coq-mathcomp-odd-order/theories/PFsection12.v.html │ │ 44.0 44.9 0.8341 1.89% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html │ │ 42.7 43.4 0.7614 1.78% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 15.5 16.2 0.7187 4.64% 326 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord.v.html │ │ 27.1 27.8 0.7048 2.60% 794 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 31.4 32.1 0.7012 2.23% 331 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord.v.html │ │ 13.4 14.1 0.6670 4.98% 216 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 22.7 23.4 0.6333 2.79% 776 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 42.8 43.5 0.6241 1.46% 244 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 7.78 8.39 0.6118 7.86% 484 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 13.1 13.7 0.6101 4.67% 572 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 │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 7.56 0.848 -6.7156 -88.79% 602 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 7.29 0.858 -6.4316 -88.23% 604 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 36.7 32.1 -4.6666 -12.70% 835 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 109 104 -4.2948 -3.95% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 55.6 51.6 -4.0119 -7.22% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 81.3 78.5 -2.7559 -3.39% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 4.30 1.89 -2.4157 -56.15% 905 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 3.47 1.27 -2.2034 -63.48% 112 coq-bedrock2/bedrock2/src/bedrock2Examples/cswap.v.html │ │ 3.44 1.26 -2.1813 -63.39% 112 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/cswap.v.html │ │ 66.2 64.1 -2.0966 -3.17% 608 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 238 236 -1.8036 -0.76% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 1.75 0.120 -1.6314 -93.14% 216 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Constructions/Product.v.html │ │ 1.58 0.0397 -1.5445 -97.50% 731 coq-fiat-crypto-with-bedrock/src/AbstractInterpretation/ZRangeProofs.v.html │ │ 4.74 3.25 -1.4838 -31.34% 19 coq-fiat-crypto-with-bedrock/src/Language/IdentifiersBasicGENERATED.v.html │ │ 6.87 5.48 -1.3958 -20.30% 35 coq-fiat-crypto-with-bedrock/rupicola/src/Rupicola/Examples/Net/IPChecksum/IPChecksum.v.html │ │ 1.36 0.00474 -1.3600 -99.65% 368 coq-unimath/UniMath/CategoryTheory/Monoidal/Examples/LiftPoset.v.html │ │ 20.9 19.6 -1.2945 -6.18% 24 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html │ │ 1.53 0.278 -1.2522 -81.84% 1325 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 14.3 13.1 -1.2481 -8.72% 24 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MulSplit.v.html │ │ 19.1 18.0 -1.1198 -5.87% 23 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/Arith.v.html │ │ 65.2 64.1 -1.1108 -1.70% 608 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 134 133 -0.9998 -0.74% 155 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 0.924 0.00480 -0.9197 -99.48% 64 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/Cartesian.v.html │ │ 1.06 0.184 -0.8808 -82.72% 833 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 1.07 0.186 -0.8807 -82.60% 835 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
Contributor
Author
|
@coqbot bench |
Contributor
|
🏁 Bench results: INFO: failed to install rocq-metarocq-utils (dependency rocq-equations failed) 🐢 Top 25 slow downs┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 56.0 60.0 3.9828 7.11% 512 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 51.2 55.1 3.8801 7.58% 567 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 59.4 63.0 3.5985 6.06% 659 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 43.8 47.4 3.5700 8.15% 256 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 41.3 44.5 3.2407 7.85% 539 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 54.7 56.9 2.1464 3.92% 296 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html │ │ 63.8 65.6 1.8616 2.92% 608 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 7.84 9.69 1.8471 23.56% 1831 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 30.9 32.7 1.8439 5.97% 596 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 42.4 44.0 1.5954 3.76% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 21.5 22.8 1.2174 5.65% 616 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 21.1 22.2 1.1421 5.41% 49 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 42.3 43.5 1.1416 2.70% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 38.4 39.5 1.1136 2.90% 1423 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 7.04 8.14 1.1071 15.73% 571 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 93.6 94.4 0.8365 0.89% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 44.2 45.0 0.8300 1.88% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html │ │ 44.2 45.1 0.8065 1.82% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html │ │ 7.80 8.53 0.7334 9.40% 484 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 12.9 13.7 0.7123 5.50% 572 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 93.4 94.1 0.6823 0.73% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 5.54 6.21 0.6730 12.16% 549 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 7.79 8.38 0.5855 7.51% 214 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 7.92 8.50 0.5744 7.25% 1331 coq-mathcomp-odd-order/theories/PFsection9.v.html │ │ 26.6 27.1 0.5707 2.15% 34 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 11.6 4.89 -6.7595 -58.04% 194 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 7.52 0.884 -6.6310 -88.24% 602 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 7.37 0.933 -6.4355 -87.34% 604 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 36.9 31.8 -5.0181 -13.61% 835 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 55.7 51.2 -4.4413 -7.98% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 108 104 -3.8912 -3.61% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 81.4 78.5 -2.9421 -3.61% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 4.24 1.74 -2.4937 -58.84% 199 coq-fiat-crypto-with-bedrock/src/Fancy/Montgomery256.v.html │ │ 203 200 -2.4435 -1.20% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 4.28 1.86 -2.4117 -56.41% 905 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 3.49 1.30 -2.1991 -62.92% 112 coq-bedrock2/bedrock2/src/bedrock2Examples/cswap.v.html │ │ 3.50 1.33 -2.1654 -61.87% 112 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/cswap.v.html │ │ 1.73 0.118 -1.6152 -93.19% 216 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Constructions/Product.v.html │ │ 2.99 1.40 -1.5899 -53.24% 256 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 4.72 3.25 -1.4727 -31.20% 19 coq-fiat-crypto-with-bedrock/src/Language/IdentifiersBasicGENERATED.v.html │ │ 6.86 5.45 -1.4030 -20.46% 35 coq-fiat-crypto-with-bedrock/rupicola/src/Rupicola/Examples/Net/IPChecksum/IPChecksum.v.html │ │ 1.36 0.00441 -1.3596 -99.68% 368 coq-unimath/UniMath/CategoryTheory/Monoidal/Examples/LiftPoset.v.html │ │ 1.53 0.278 -1.2551 -81.87% 1325 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 14.3 13.1 -1.2233 -8.55% 24 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MulSplit.v.html │ │ 20.9 19.7 -1.2147 -5.81% 24 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html │ │ 1.21 0.0424 -1.1641 -96.49% 731 coq-fiat-crypto-with-bedrock/src/AbstractInterpretation/ZRangeProofs.v.html │ │ 18.9 17.9 -0.9940 -5.26% 23 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/Arith.v.html │ │ 0.920 0.00476 -0.9156 -99.48% 64 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/Cartesian.v.html │ │ 1.08 0.191 -0.8859 -82.26% 835 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 1.08 0.192 -0.8859 -82.21% 833 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
SkySkimmer
reviewed
May 29, 2026
| let equal sigma a b = | ||
| a == b || (a.term == b.term && a.subst == b.subst) || | ||
| (* TODO: add fast path that returns false on non-Rel terms whose head is not of the same shape. | ||
| Alternatively, fuse the equality check and the substitution *) |
Contributor
There was a problem hiding this comment.
the fusing should be relatively simple using kind below no?
Contributor
Author
There was a problem hiding this comment.
I am not sure I know how to resolve the resulting type puzzle now that kind no longer returns a Constr shaped thing.
SkySkimmer
reviewed
May 29, 2026
| let b = force sigma b in | ||
| a == b || EConstr.eq_constr sigma a b | ||
|
|
||
| let equal_under sigma n a b = equal sigma (liftn n a) (liftn n b) |
Contributor
There was a problem hiding this comment.
is it possible that equal_under is not equivalent to equal? I don't see how lifting by the same amount can change equality. (it will certainly break the physical equality fast path though)
Contributor
Author
There was a problem hiding this comment.
I think you are right. I won't push a fix now to not interrupt the new bench job.
SkySkimmer
reviewed
May 29, 2026
| val best_state : Evd.evar_map -> constr * constr t -> Cst_stack.t -> constr * constr t | ||
| val zip : ?refold:bool -> Evd.evar_map -> constr * constr t -> constr | ||
| val best_state : inject:(constr -> 'a) -> equal:('a -> 'a -> bool) -> 'a * 'a t -> 'a Cst_stack.t -> 'a * 'a t | ||
| val zip : ?refold:bool -> Evd.evar_map -> |
Contributor
There was a problem hiding this comment.
does this stuff actually need to be polymorphic? seems like we should monomorphize
Contributor
Author
There was a problem hiding this comment.
It seems it can be monomorphized. I pushed a commit.
SkySkimmer
reviewed
May 29, 2026
| [CbnClos.kind] view of the array; building that view allocates a closure | ||
| for every element even when [array_get]/[array_length] will discard most | ||
| of them. *) | ||
| let early_array_primitive = match Stack.strip_app stack with |
Contributor
There was a problem hiding this comment.
having to do an extra strip_app at every step may be not great, but I think we can merge array_view and kind (by returning a wrapper around Constr.kind from CbnClos.kind)
incoming commit
Contributor
Author
There was a problem hiding this comment.
That seems like it helped a whole lot with the overhead on some array examples I have locally:
| Master | HEAD~ | HEAD |
|---|---|---|
| 4395962 | 3347798 | 3054980 |
| 15078524 | 11840342 | 10474563 |
| 56989652 | 45893889 | 40186233 |
| 69334 | 77151 | 71117 |
| 67199 | 83959 | 78945 |
| 69314 | 119648 | 70787 |
| 59248 | 55811 | 55575 |
| 59249 | 55822 | 55587 |
| 57083 | 61929 | 55574 |
| 8020239 | 6161145 | 5498511 |
| 29056622 | 23084271 | 20279234 |
| 4401443 | 3365103 |
3067474 |
| 8010337 | 6150323 |
5510858 |
| 15044076 | 11813227 | 10453421 |
| 29046469 | 23126957 | 20317893 |
| 57002056 | 45890300 | 40192347 |
| 21414032 | 14187242 | 12449045 |
(I had to turn two numbers into code because they happen to be valid SHA prefixes of existing commits 🤦 )
Contributor
|
@coqbot bench |
SkySkimmer
reviewed
May 29, 2026
| | Evar (ev, args) -> notarray @@ Evar (ev, SList.Skip.map (mk_clos c.subst) args) | ||
| | Sort s -> notarray @@ Sort s | ||
| | Cast (b, k, t) -> notarray @@ Cast (mk_clos c.subst b, k, mk_clos c.subst t) | ||
| | Prod (na, t, b) -> notarray @@ Prod (na, mk_clos c.subst t, mk_clos c.subst b) |
Contributor
There was a problem hiding this comment.
further looking at this, is it really correct to not apply a lift to the subst under binders?
Contributor
Author
There was a problem hiding this comment.
I was also very surprised by this when I was playing around with the equality thing earlier. I did expect a lift here. The fact that nothing breaks probably means this bug is counteracted by another bug somewhere?
Contributor
There was a problem hiding this comment.
It will lift / cons in other places, eg https://github.com/Janno/coq/blob/9a772ab008e32fcd1addde32f63a6a7e1820fac4/tactics/cbn.ml#L740
Contributor
There was a problem hiding this comment.
I think we can be smarter by returning the substitution to the side instead of in the kind subterms, but it doesn't quite work 0fc36c7 (eg test suite prerequisite/list fails with Not_found)
I think because I didn't handle putting Fix/Case in the stack correctly but getting tired of this for today (also stack being polymorphic doesn't help with modifying this code)
Contributor
Author
There was a problem hiding this comment.
Just for my own notes: This is an example of a term that produces ill-scoped/ill-typed terms at least in debug output.
Goal forall (b : bool) (n : nat), True.
Proof.
intros b n.
Set Debug "RAKAM".
Eval cbn in
((fun b : bool => match n return bool with O => true | S _ => b end) b).
(* ...
Debug: [RAKAM] <<n||ZCase(true| _UNBOUND_REL_1)>>
... *)
Contributor
There was a problem hiding this comment.
I think I got it, let's see how it does
SkySkimmer
reviewed
May 29, 2026
| let n = Array.length elems in | ||
| let term = mkArray (u, Array.init n (fun i -> mkRel (i + 1)), mkRel (n + 1), mkRel (n + 2)) in | ||
| let subst = List.fold_right Esubst.subs_cons (Array.to_list elems @ [def; ty]) id_subst in | ||
| mk_clos subst term |
Contributor
There was a problem hiding this comment.
this looks pretty messy, not sure how much we care about arrays though
Miivaan
approved these changes
May 29, 2026
Contributor
|
🏁 Bench results: INFO: failed to install rocq-mathcomp-solvable (dependency rocq-mathcomp-algebra failed) 🐢 Top 25 slow downs┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 50.9 54.3 3.4507 6.78% 567 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 59.3 62.4 3.1062 5.24% 659 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 55.9 58.9 3.0517 5.46% 512 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 41.1 43.5 2.4179 5.88% 539 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 43.6 46.0 2.3304 5.34% 256 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 63.0 65.2 2.2170 3.52% 608 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 54.2 56.4 2.1698 4.00% 296 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html │ │ 200 202 2.1112 1.06% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 7.81 9.64 1.8321 23.45% 1831 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 30.9 32.6 1.7060 5.52% 596 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 0.831 2.20 1.3736 165.27% 931 coq-unimath/UniMath/CategoryTheory/ComprehensionCats/CwfFromCompCatWithUniv.v.html │ │ 21.6 22.7 1.1029 5.11% 616 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 42.4 43.5 1.0919 2.57% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 38.5 39.3 0.7520 1.95% 1423 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 7.76 8.51 0.7517 9.69% 484 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 2.47 3.21 0.7389 29.88% 34 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 22.7 23.4 0.6739 2.96% 776 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 13.0 13.6 0.6233 4.80% 572 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 82.7 83.3 0.6106 0.74% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 5.57 6.10 0.5336 9.58% 549 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 7.73 8.26 0.5329 6.90% 214 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 1.58 2.06 0.4834 30.67% 42 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 28.5 29.0 0.4610 1.62% 31 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │ │ 38.1 38.6 0.4516 1.18% 224 coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html │ │ 0.189 0.630 0.4405 232.78% 458 coq-unimath/UniMath/Combinatorics/FLists.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 11.6 4.91 -6.6911 -57.66% 194 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 7.42 0.842 -6.5755 -88.64% 602 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 7.10 0.872 -6.2276 -87.71% 604 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 55.4 50.2 -5.1847 -9.36% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 36.5 31.6 -4.9337 -13.51% 835 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 81.1 77.4 -3.7844 -4.66% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 108 104 -3.3511 -3.11% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 4.24 1.76 -2.4714 -58.35% 199 coq-fiat-crypto-with-bedrock/src/Fancy/Montgomery256.v.html │ │ 4.22 1.83 -2.3910 -56.61% 905 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 3.45 1.25 -2.1958 -63.65% 112 coq-bedrock2/bedrock2/src/bedrock2Examples/cswap.v.html │ │ 3.45 1.26 -2.1913 -63.52% 112 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/cswap.v.html │ │ 17.8 16.2 -1.6240 -9.13% 833 coq-unimath/UniMath/CategoryTheory/ComprehensionCats/CwfFromCompCatWithUniv.v.html │ │ 1.74 0.120 -1.6157 -93.10% 216 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Constructions/Product.v.html │ │ 3.00 1.41 -1.5857 -52.93% 256 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 4.71 3.22 -1.4876 -31.59% 19 coq-fiat-crypto-with-bedrock/src/Language/IdentifiersBasicGENERATED.v.html │ │ 6.80 5.43 -1.3701 -20.14% 35 coq-fiat-crypto-with-bedrock/rupicola/src/Rupicola/Examples/Net/IPChecksum/IPChecksum.v.html │ │ 1.36 0.00432 -1.3585 -99.68% 368 coq-unimath/UniMath/CategoryTheory/Monoidal/Examples/LiftPoset.v.html │ │ 20.8 19.5 -1.3080 -6.28% 24 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html │ │ 1.52 0.245 -1.2781 -83.91% 1325 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 14.4 13.2 -1.2420 -8.61% 24 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MulSplit.v.html │ │ 31.8 30.5 -1.2260 -3.86% 157 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 1.22 0.0421 -1.1744 -96.54% 731 coq-fiat-crypto-with-bedrock/src/AbstractInterpretation/ZRangeProofs.v.html │ │ 32.9 31.7 -1.1606 -3.53% 121 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 31.6 30.5 -1.0620 -3.37% 198 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 18.8 17.8 -1.0455 -5.56% 23 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/Arith.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
Contributor
|
now with the equal change |
Contributor
|
🏁 Bench results: INFO: failed to install rocq-metarocq-utils (dependency rocq-equations failed) 🐢 Top 25 slow downs┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 0.235 3773 3773.0919 1604383.08% 225 coq-unimath/UniMath/CategoryTheory/Monads/KleisliCategory.v.html │ │ 0.0112 55.1 55.1096 492137.95% 338 coq-unimath/UniMath/Combinatorics/FLists.v.html │ │ 0.0233 27.9 27.9209 119708.86% 108 coq-hott/theories/Colimits/Colimit_Flattening.v.html │ │ 0.237 21.3 21.0139 8860.71% 373 coq-unimath/UniMath/Combinatorics/FLists.v.html │ │ 0.00221 20.6 20.5560 928875.96% 267 coq-hott/theories/Homotopy/CayleyDickson.v.html │ │ 0.189 17.0 16.7652 8857.21% 458 coq-unimath/UniMath/Combinatorics/FLists.v.html │ │ 0.150 13.6 13.4429 8958.15% 495 coq-unimath/UniMath/Combinatorics/FLists.v.html │ │ 0.130 12.1 11.9692 9193.07% 475 coq-unimath/UniMath/Combinatorics/FLists.v.html │ │ 0.0146 6.83 6.8156 46602.50% 116 coq-unimath/UniMath/CategoryTheory/MarkovCategories/RelativeProduct.v.html │ │ 0.0146 6.75 6.7374 46080.59% 128 coq-unimath/UniMath/CategoryTheory/MarkovCategories/RelativeProduct.v.html │ │ 200 204 4.3273 2.16% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 0.0531 4.10 4.0515 7627.94% 374 coq-unimath/UniMath/Combinatorics/FLists.v.html │ │ 0.226 2.88 2.6562 1174.22% 444 coq-unimath/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/DispCatOnTwoSidedDispCat.v.html │ │ 0.227 2.88 2.6562 1172.05% 456 coq-unimath/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/DispCatOnTwoSidedDispCat.v.html │ │ 0.0355 2.43 2.3993 6762.10% 472 coq-unimath/UniMath/CategoryTheory/PseudoElements.v.html │ │ 0.583 2.63 2.0494 351.60% 347 coq-unimath/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/DispCatOnTwoSidedDispCat.v.html │ │ 0.613 2.63 2.0193 329.48% 334 coq-unimath/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/DispCatOnTwoSidedDispCat.v.html │ │ 0.105 1.91 1.8057 1720.67% 124 coq-hott/theories/Algebra/Universal/Algebra.v.html │ │ 48.4 50.2 1.7587 3.63% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 0.000925 1.50 1.5001 162177.19% 180 coq-hott/theories/Colimits/Colimit.v.html │ │ 0.0201 1.16 1.1426 5687.40% 263 coq-unimath/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/DispCatOnTwoSidedDispCat.v.html │ │ 0.0119 1.04 1.0314 8679.31% 229 coq-unimath/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/DispCatOnTwoSidedDispCat.v.html │ │ 0.0120 1.00 0.9918 8244.68% 246 coq-unimath/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/DispCatOnTwoSidedDispCat.v.html │ │ 40.087 40.937 0.8500 2.12% 834 coq-vst/veric/binop_lemmas4.v.html │ │ 0.413 1.24 0.8322 201.61% 816 coq-unimath/UniMath/HomologicalAlgebra/CohomologyComplex.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 7.38 0.834 -6.5416 -88.69% 602 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 7.24 0.867 -6.3710 -88.02% 604 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 1.74 0.0210 -1.7213 -98.80% 216 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Constructions/Product.v.html │ │ 1.37 0.00431 -1.3647 -99.69% 368 coq-unimath/UniMath/CategoryTheory/Monoidal/Examples/LiftPoset.v.html │ │ 0.932 0.0195 -0.9122 -97.91% 64 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/Cartesian.v.html │ │ 1.07 0.204 -0.8615 -80.83% 835 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 1.07 0.212 -0.8564 -80.17% 833 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 18.4 17.6 -0.7319 -3.98% 32 coq-performance-tests-lite/src/pattern.v.html │ │ 0.740 0.0303 -0.7096 -95.90% 990 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 0.678 0.0273 -0.6509 -95.97% 992 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 94.2 93.5 -0.6456 -0.69% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 0.542 0.000530 -0.5419 -99.90% 454 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/PointedPosetStrict.v.html │ │ 2.14 1.65 -0.4918 -22.95% 313 rocq-stdlib/theories/Strings/Byte.v.html │ │ 0.434 0.00770 -0.4261 -98.23% 174 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/Cartesian.v.html │ │ 1.29 0.873 -0.4205 -32.51% 200 rocq-stdlib/theories/Numbers/HexadecimalNat.v.html │ │ 2.61 2.19 -0.4163 -15.97% 213 rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html │ │ 0.416 0.00115 -0.4150 -99.72% 409 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/PointedPosetStrict.v.html │ │ 0.595 0.196 -0.3998 -67.14% 940 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 27.1 26.8 -0.3815 -1.41% 13 coq-fourcolor/theories/proof/job531to534.v.html │ │ 0.447 0.0672 -0.3796 -84.95% 625 coq-unimath/UniMath/CategoryTheory/LeftKanExtension.v.html │ │ 1.24 0.871 -0.3665 -29.62% 215 rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html │ │ 3.07 2.74 -0.3208 -10.46% 597 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/SetGroupoidComprehension.v.html │ │ 0.492 0.180 -0.3125 -63.51% 141 rocq-stdlib/theories/Numbers/DecimalNat.v.html │ │ 3.85 3.54 -0.3117 -8.09% 492 rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 0.359 0.0573 -0.3022 -84.06% 955 coq-unimath/UniMath/CategoryTheory/ComprehensionCats/CwfFromCompCatWithUniv.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
Contributor
|
conclusion: 9a772ab bad |
SkySkimmer
force-pushed
the
janno/cbn-delayed-subst
branch
from
9a772ab to
6edd61e
Compare
Contributor
|
@coqbot bench |
SkySkimmer
force-pushed
the
janno/cbn-delayed-subst
branch
from
65f0650 to
0b61286
Compare
Contributor
|
rebased to avoid overlay problems @coqbot bench |
Contributor
|
🏁 Bench results: INFO: failed to install rocq-metarocq-safechecker (dependency rocq-metarocq-pcuic failed) 🐢 Top 25 slow downs┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 23.4 26.8 3.4139 14.62% 129 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ │ 58.0 60.5 2.4624 4.24% 659 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 55.0 56.9 1.8272 3.32% 512 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 50.7 52.5 1.7198 3.39% 567 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 40.7 42.3 1.5163 3.72% 235 coq-category-theory/Construction/DecoratedCospan/Category.v.html │ │ 43.2 44.7 1.4626 3.39% 256 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 54.0 55.4 1.4005 2.59% 296 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html │ │ 41.2 42.5 1.3790 3.35% 539 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 202 204 1.1821 0.58% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 87.7 88.8 1.0934 1.25% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 87.9 89.0 1.0928 1.24% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 30.3 31.3 0.9954 3.28% 596 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 2.46 3.27 0.8059 32.72% 34 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 6.44 7.19 0.7433 11.54% 1831 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 21.0 21.7 0.6860 3.26% 616 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 0.236 0.713 0.4775 202.40% 586 rocq-stdlib/theories/Strings/Byte.v.html │ │ 12.6 13.1 0.4104 3.25% 572 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 0.210 0.612 0.4021 191.85% 458 coq-unimath/UniMath/Combinatorics/FLists.v.html │ │ 18.4 18.7 0.3768 2.05% 481 coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html │ │ 79.7 80.1 0.3708 0.47% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 0.0848 0.434 0.3489 411.67% 45 coq-mathcomp-analysis/theories/gauss_integral.v.html │ │ 30.9 31.2 0.3452 1.12% 139 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 46.4 46.7 0.3289 0.71% 115 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 11.2 11.5 0.3204 2.87% 675 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 6.95 7.26 0.3093 4.45% 484 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 7.76 0.757 -7.0062 -90.25% 602 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 7.41 0.776 -6.6388 -89.53% 604 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 11.0 4.46 -6.5456 -59.45% 194 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 55.5 49.6 -5.9754 -10.76% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 35.3 29.5 -5.7760 -16.36% 835 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 242 236 -5.4129 -2.24% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 107 102 -4.7003 -4.40% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 80.6 77.4 -3.2654 -4.05% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 136 133 -2.8410 -2.09% 155 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 4.00 1.54 -2.4633 -61.55% 199 coq-fiat-crypto-with-bedrock/src/Fancy/Montgomery256.v.html │ │ 4.30 1.83 -2.4618 -57.31% 905 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 3.49 1.11 -2.3735 -68.07% 112 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/cswap.v.html │ │ 20.5 18.7 -1.8220 -8.88% 24 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html │ │ 1.93 0.119 -1.8066 -93.82% 216 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Constructions/Product.v.html │ │ 4.87 3.12 -1.7524 -35.99% 19 coq-fiat-crypto-with-bedrock/src/Language/IdentifiersBasicGENERATED.v.html │ │ 2.80 1.20 -1.5971 -57.04% 256 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 1.53 0.00404 -1.5264 -99.74% 368 coq-unimath/UniMath/CategoryTheory/Monoidal/Examples/LiftPoset.v.html │ │ 14.2 12.8 -1.4198 -10.00% 24 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MulSplit.v.html │ │ 6.24 4.85 -1.3907 -22.27% 35 coq-fiat-crypto-with-bedrock/rupicola/src/Rupicola/Examples/Net/IPChecksum/IPChecksum.v.html │ │ 1.54 0.189 -1.3509 -87.71% 1325 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 1.35 0.0319 -1.3168 -97.64% 731 coq-fiat-crypto-with-bedrock/src/AbstractInterpretation/ZRangeProofs.v.html │ │ 18.9 17.6 -1.2709 -6.73% 23 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/Arith.v.html │ │ 22.4 21.2 -1.2412 -5.54% 49 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 1.03 0.0572 -0.9759 -94.46% 343 coq-fiat-crypto-with-bedrock/src/Assembly/EquivalenceProofs.v.html │ │ 0.951 0.00427 -0.9470 -99.55% 64 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/Cartesian.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
Contributor
|
I think that's a bit faster. @Janno can you test that last commit on your stuff? |
Contributor
Author
|
Are the bench failures related to missing overlays or do I need to go in and investigate? |
Contributor
|
vst is probably https://rocq-prover.zulipchat.com/#narrow/channel/237656-Rocq-devs-.26-plugin-devs/topic/vst.20broken.20in.20CI/with/599536996 but the others may be real failures |
coqbot-app
Bot
removed
the
needs: full CI
Contributor
Author
SkySkimmer
reviewed
Jun 3, 2026
| let v := eval cbn in (@difference set set_difference (exist _ 0 I) y) in | ||
| lazymatch v with | ||
| | difference (exist _ 0 I) y => exact I | ||
| | _ => fail "difference was not refolded" |
Contributor
There was a problem hiding this comment.
what's going on in this test? in master it fails (cbn produces let (t2, _) := y in exist (fun _ : nat => True) 0 I)
Contributor
Author
There was a problem hiding this comment.
These tests were extracted from failures on skylabs code where the refolding happens and is required. We are using something closer to 9.1. I will try to find out where the discrepancy comes from.
Contributor
Author
There was a problem hiding this comment.
Okay, I know what happened. difference needs simpl nomatch and I lost that while minimizing the example. I pushed a commit to add the missing Arguments lines.
Contributor
There was a problem hiding this comment.
does that mean we should add a test without the Arguments?
is a542012 still needed with the Arguments?
Contributor
Author
There was a problem hiding this comment.
does that mean we should add a test without the Arguments?
I guess we could keep a version of the tests without Arguments to be thorough. I don't really know how to decide. I generally do not like to assert that some ugly term is not being refolded (particularly because cbn can be very, very aggressive about refolding and that seems to be why people like using it)
is a542012 still needed with the Arguments?
Everything seems to work if I locally revert just the changes to cbn.ml from that commit.
SkySkimmer
added
the
request: full CI
coqbot-app
Bot
removed
the
request: full CI
Contributor
|
new commit: expand rel in mk_clos This dramatically speeds up the tests in success/cbn2.v For some reason it restores the master behaviour for some tests in success/cbn.v. @coqbot bench |
Contributor
|
seems like subst_value doesn't like the eager expansion of rels |
coqbot-app
Bot
added
the
needs: full CI
Contributor
|
@coqbot run full ci |
coqbot-app
Bot
removed
the
needs: full CI
Contributor
|
🏁 Bench results: INFO: failed to install rocq-metarocq-utils (dependency rocq-equations failed) 🐢 Top 25 slow downs┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 62.6 66.5 3.9663 6.34% 608 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 50.6 52.1 1.4791 2.92% 567 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 201 202 1.3903 0.69% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 58.5 59.7 1.2483 2.13% 659 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 88.4 89.5 1.1074 1.25% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 88.2 89.3 1.0172 1.15% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 55.2 56.1 0.9503 1.72% 512 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 54.3 55.2 0.9499 1.75% 296 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html │ │ 41.3 42.2 0.9418 2.28% 539 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 43.6 44.5 0.8909 2.04% 256 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 6.48 7.22 0.7412 11.44% 1831 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 26.7 27.3 0.6140 2.30% 68 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html │ │ 34.2 34.8 0.5535 1.62% 194 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 28.5 29.1 0.5427 1.90% 305 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html │ │ 30.6 31.1 0.5405 1.77% 596 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 0.816 1.34 0.5264 64.52% 200 rocq-stdlib/theories/Numbers/HexadecimalNat.v.html │ │ 21.1 21.6 0.4340 2.05% 616 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 48.8 49.2 0.4024 0.82% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 32.1 32.5 0.3942 1.23% 121 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 0.00297 0.395 0.3925 13196.87% 96 coq-mathcomp-analysis/theories/hoelder.v.html │ │ 0.00439 0.365 0.3609 8222.62% 254 coq-mathcomp-analysis/theories/measure_theory/measure_negligible.v.html │ │ 33.7 34.1 0.3209 0.95% 898 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 31.0 31.3 0.3160 1.02% 214 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 0.186 0.475 0.2890 155.06% 16 rocq-stdlib/theories/Numbers/DecimalPos.v.html │ │ 0.367 0.651 0.2842 77.44% 59 rocq-stdlib/theories/ZArith/Zeuclid.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 7.71 0.768 -6.9445 -90.05% 602 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 11.2 4.41 -6.8078 -60.71% 194 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 7.49 0.767 -6.7197 -89.75% 604 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 35.2 29.4 -5.7941 -16.44% 835 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 55.1 49.8 -5.2441 -9.52% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 107 103 -4.4546 -4.16% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 80.9 77.3 -3.6311 -4.49% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 3.99 1.53 -2.4584 -61.68% 199 coq-fiat-crypto-with-bedrock/src/Fancy/Montgomery256.v.html │ │ 4.28 1.83 -2.4477 -57.21% 905 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 3.50 1.08 -2.4204 -69.08% 112 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/cswap.v.html │ │ 1.93 0.0789 -1.8468 -95.90% 216 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Constructions/Product.v.html │ │ 20.6 18.8 -1.8423 -8.93% 24 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html │ │ 4.89 3.12 -1.7718 -36.24% 19 coq-fiat-crypto-with-bedrock/src/Language/IdentifiersBasicGENERATED.v.html │ │ 6.38 4.73 -1.6452 -25.79% 35 coq-fiat-crypto-with-bedrock/rupicola/src/Rupicola/Examples/Net/IPChecksum/IPChecksum.v.html │ │ 2.83 1.23 -1.6013 -56.62% 256 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 1.54 0.00404 -1.5324 -99.74% 368 coq-unimath/UniMath/CategoryTheory/Monoidal/Examples/LiftPoset.v.html │ │ 14.2 12.7 -1.5202 -10.70% 24 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MulSplit.v.html │ │ 1.55 0.162 -1.3880 -89.53% 1325 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 18.8 17.4 -1.3708 -7.30% 23 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/Arith.v.html │ │ 1.35 0.0333 -1.3190 -97.54% 731 coq-fiat-crypto-with-bedrock/src/AbstractInterpretation/ZRangeProofs.v.html │ │ 26.7 25.7 -1.0203 -3.82% 13 coq-fourcolor/theories/proof/job466to485.v.html │ │ 6.34 5.36 -0.9878 -15.57% 20 coq-fiat-crypto-with-bedrock/src/Language/IdentifiersGENERATEDProofs.v.html │ │ 1.03 0.0578 -0.9768 -94.41% 343 coq-fiat-crypto-with-bedrock/src/Assembly/EquivalenceProofs.v.html │ │ 0.947 0.00406 -0.9430 -99.57% 64 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/Cartesian.v.html │ │ 1.12 0.190 -0.9329 -83.08% 833 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
coqbot-app
Bot
added
the
needs: full CI
Janno
commented
Jun 4, 2026
| let v := eval cbn in (@difference set set_difference (exist _ 0 I) y) in | ||
| lazymatch v with | ||
| | difference (exist _ 0 I) y => exact I | ||
| | _ => fail "difference was not refolded" |
Contributor
Author
There was a problem hiding this comment.
Okay, I know what happened. difference needs simpl nomatch and I lost that while minimizing the example. I pushed a commit to add the missing Arguments lines.
SkySkimmer
added
the
kind: performance
SkySkimmer
added
the
request: full CI
coqbot-app
Bot
removed
request: full CI
Contributor
|
@Janno can you check if what I pushed causes regressions? |
Contributor
Author
|
We just completed a bump to 9.2 so the results are not comparable to the previous results on 9.1. Still, |
coqbot-app
Bot
added
the
needs: full CI
github-actions
Bot
added
the
needs: rebase
SkySkimmer
added
the
request: full CI
Contributor
|
for less painful rebase I squashed |
SkySkimmer
force-pushed
the
janno/cbn-delayed-subst
branch
from
8aae8f9 to
291a8e5
Compare
coqbot-app
Bot
removed
needs: rebase
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
3 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.
The code in tactics/cbn.ml was written exclusively by GPT-5.5. It was prompted to implement delayed substitution and then to optimize the performance of examples collected from bugs, from #19309, and from bench regressions that appeared in earlier iterations.
The changes fix several catastrophic examples of
cbnslowness and generally improve its performance but they are not strictly an improvement over master. There are examples in the bench and in some of the added test cases on which the new code is a bit slower.SkyLabs code (which uses cbn almost exclusively but doesn't have (m)any catastrophic examples left) shows a 0.35% speedup as of 50eba77
TODO:
Instructionsand outdated instruction counts in comments, as well as some duplicate tests. I will sort through the tests to keep only those that document cbn behavior and, if possible, someTimeouttests to prevent regressions on catastrophic examples.Fixes / closes #????
make doc_gram_rsts.