Improve discrimination of lambdas in typeclass search

[Janno]

The (bounded) discrimination nets used in TC search currently consider all fun terms to match any term. This is a performance issue for typeclasses that are keyed on fun terms. One example is the Fractional class in iris which even in iris itself has 22 instances of the form Fractional (fun q => ..). All of those instances will always match any Fractional query. (I am ignoring the first parameter of the class which in practice has very little discriminating power).

The reason for the current state of affairs is that the discrimination nets must over-approximate (tactic) unification. This includes eta equivalence of functions. The following cases need to be considered. I am using x ~ y to indicate that x matches y in the discrimination net.

1. (fun x .. z => f x .. z) ~ f when f is Hint Opaque
2. (fun x .. z => f x .. z) ~ _ when f is Hint Transparent

This is easily achieved by the current algorithm which simply translates all fun to _.

To strengthen the discriminating power, we would like refine these two conditions into the following way. We use n to designate the number of binders in fun x .. z and postfix ↓ to indicate a term lifted by -n. (We do not care that the negative lifting can introduce negative Rels but the algorithm could be changed to avoid that if necessary.)

1. (fun x .. z => f _ .. _) ~ f
   a) when f↓ ~/~ _,
   b) f _ .. _ is an application of f to exactly n arguments of any shape.
2. (fun x .. z => t1) ~ (fun x .. z => t2)
   a) when neither t1 nor t2 match _
   b) neither t1↓ nor t1↓ are applications with n or more arguments.
3. (fun x .. z => t) ~ _
   a) when t ~ _.

These rules were developed based on ideas by and in collaboration with @cipher1024. They aim to over-approximate eta in a way that should retain almost all available discriminating power of fun terms. We would ideally like to rely solely on eta contraction in patterns and constrs and use all non-contractible funs for discrimination. However, standard eta contraction (as is used in the current algorithm) is too specific. It misses cases such as fun x => f (id x) which, assuming id is Hint Transparent, will unify with the term f.

Being more clever in the attempt to recognize true eta expansions (reducing arguments, actually calling unification, etc.) seems difficult and likely expensive performance-wise. So we instead opted to be much dumber about it and simply treat all terms of the form fun x => f _ as potential eta expansions of f. This includes examples such as fun x y => f y x (note the swapped order of arguments) and fun _ => @None A (translated to just @None). This is the basis of case 1.

The flip side of this extremely broad over-approximation of eta is that we can be quite sure that fun terms that do not fit this pattern will never be eta equivalent to other terms. In particular, we can use the fun itself as well as the type of its binder(s) for discrimination. This is case 2.

However, we must be careful if the body of the fun is flexible in the sense that it can be unified with arbitrary terms. For example, the term fun _ => ?A must not be treated as a discriminating fun because ?A could well end up being f _, yielding fun _ => f _ which violates our "eta normal" form and would wrongly end up not matching f. This is case 3.

TODO:

• The algorithm in decomp_lambda_(constr|pattern) is bad and the overall translation of a fun term has cubic runtime in the number of binders in fun terms. Some of that can be fixed but the fact that we must return only one node at a time makes it impossible to fully fix it. I don't think this is super important but I hate contributing bad code. 94ce659 has a solution to the issue of only generating one label at a time but @ppedrot did not like last time I introduced it. With more recursive work being performed now maybe the verdict would be different?
• Generating negative Rels when we chop off binders that might still be used could be problematic but works fine in practice because Rels are translated to None (for constrs) and Nothing (for patterns). An alternative suggested by @cipher1024 finds occurrences of dead variables and replaces terms that contain them with _ (or, rather, some term that translates to _). This ends up re-implementing part of the translation so I would like to avoid it.
• The algorithm for constrs is very confusing because of the way that it uses Everything and Nothing to introduce a distinction (almost) without difference. This PR adds to the confusion and interprets Nothing differently from my previous change (which introduced CaseLabel) in Refine approximation of matches in the bnet #18677, where I treat it as an unique label. In this change it is treated the same as Everything, which I think is the correct interpretation. (Out of scope.)
• I think decomp_pat_discr_syntactic (used for Hint Extern) does not have to respect eta (and can thus always discriminate funs) because Constr_matching does not respect eta. It this correct? We must go through the same eta-reduction approximation steps for syntactic patterns so that the resulting dnets match constrs which are always eta-reduced.

Fixes / closes #????

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

• Opened overlay pull requests.

[Janno]

@coqbot bench

[coqbot-app]

No check suite 31373 for head commit efebfcc.

[SkySkimmer]

@coqbot bench

[coqbot-app]

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│                       coq-fiat-core │   57.48    59.36  -3.17 │   354429025563    354608498833  -0.05 │  474076   474288  -0.04 │
│                            coq-core │    3.02     3.10  -2.58 │    20603303421     20606537396  -0.02 │   91608    91344   0.29 │
│                       coq-equations │    8.11     8.26  -1.82 │    56661044302     56657571294   0.01 │  394012   391844   0.55 │
│                         coq-coqutil │   42.90    43.52  -1.42 │   269996516696    269967104951   0.01 │  560636   560572   0.01 │
│               coq-engine-bench-lite │  129.20   130.79  -1.22 │   967247100006    969795933374  -0.26 │ 1076956  1076940   0.00 │
│                   coq-metacoq-pcuic │  672.58   680.22  -1.12 │  4354973402284   4387725179452  -0.75 │ 2278972  2287192  -0.36 │
│                    coq-math-classes │   85.41    86.37  -1.11 │   528838580945    529226391803  -0.07 │  506536   506172   0.07 │
│                           coq-color │  246.14   248.49  -0.95 │  1563125582420   1563797848830  -0.04 │ 1082620  1082972  -0.03 │
│                 coq-metacoq-erasure │  514.61   519.43  -0.93 │  3559155153512   3576683031969  -0.49 │ 1795908  1858500  -3.37 │
│                   coq-metacoq-utils │   23.24    23.43  -0.81 │   152534014265    152566493595  -0.02 │  602656   603280  -0.10 │
│                       coq-fourcolor │ 1354.81  1364.81  -0.73 │ 12540442972341  12540767857436  -0.00 │  889628   890508  -0.10 │
│          coq-performance-tests-lite │  910.32   916.98  -0.73 │  7304317978558   7306105112773  -0.02 │ 2469588  2469604  -0.00 │
│                        coq-compcert │  304.19   306.17  -0.65 │  2006440405840   2006935685212  -0.02 │ 1161156  1161372  -0.02 │
│            coq-metacoq-translations │   16.83    16.93  -0.59 │   118124601511    118116109563   0.01 │  785872   786464  -0.08 │
│                    coq-fiat-parsers │  276.07   277.68  -0.58 │  2132478709273   2132562927438  -0.00 │ 2265328  2267064  -0.08 │
│                         coq-bignums │   30.14    30.31  -0.56 │   193768010660    193783282891  -0.01 │  479016   477964   0.22 │
│                  coq-metacoq-common │   67.59    67.96  -0.54 │   439663224299    440347374666  -0.16 │ 1069360  1055920   1.27 │
│                          coq-stdlib │  191.36   192.18  -0.43 │  1193024267622   1193731381024  -0.06 │  529848   529740   0.02 │
│                coq-metacoq-template │  147.10   147.70  -0.41 │   991618890534    992812720995  -0.12 │ 1067940  1057040   1.03 │
│                            coq-corn │  678.04   680.61  -0.38 │  4673915682151   4675707083775  -0.04 │  661652   664108  -0.37 │
│                  coq-mathcomp-field │   90.54    90.88  -0.37 │   644364515746    644976462451  -0.09 │ 1266344  1264876   0.12 │
│                   coq-iris-examples │  390.81   392.06  -0.32 │  2618357450288   2621237503588  -0.11 │ 1100396  1110288  -0.89 │
│                            coq-hott │  158.18   158.66  -0.30 │  1104203715951   1104648531104  -0.04 │  462052   461848   0.04 │
│                             coq-vst │  866.09   868.25  -0.25 │  6524731347186   6524989867444  -0.00 │ 2202324  2202384  -0.00 │
│                        rocq-runtime │   73.96    74.09  -0.18 │   536233925030    536046261722   0.04 │  482824   482688   0.03 │
│        coq-fiat-crypto-with-bedrock │ 5849.76  5858.07  -0.14 │ 47350377013960  47358072421838  -0.02 │ 3245392  3245480  -0.00 │
│              coq-mathcomp-character │   74.66    74.75  -0.12 │   510948622460    511099944555  -0.03 │ 1183100  1181056   0.17 │
│             coq-metacoq-safechecker │  347.96   348.35  -0.11 │  2633847131808   2638539540139  -0.18 │ 1662132  1676860  -0.88 │
│              coq-mathcomp-odd-order │  486.29   486.82  -0.11 │  3449943319146   3450669470587  -0.02 │ 1605520  1607440  -0.12 │
│                coq-mathcomp-algebra │  161.13   161.25  -0.07 │  1127187812366   1127273724504  -0.01 │ 1184164  1183076   0.09 │
│                           coq-verdi │   44.45    44.48  -0.07 │   298398620652    298496000085  -0.03 │  529732   529884  -0.03 │
│               coq-mathcomp-solvable │   90.43    90.49  -0.07 │   629328517261    629121921403   0.03 │  949092   959268  -1.06 │
│                           rocq-core │    6.23     6.23   0.00 │    38876157397     38892668247  -0.04 │  437428   433720   0.85 │
│                 coq-category-theory │  602.82   602.81   0.00 │  4461861856016   4464784296492  -0.07 │  997472   987824   0.98 │
│                      coq-verdi-raft │  534.82   534.81   0.00 │  3717560341215   3717746941116  -0.01 │  835484   833852   0.20 │
│                        coq-rewriter │  337.11   336.98   0.04 │  2512122162630   2512209251711  -0.00 │ 1312820  1307072   0.44 │
│                        coq-bedrock2 │  326.81   326.50   0.09 │  2734867866584   2734371349236   0.02 │  889172   889724  -0.06 │
│ coq-neural-net-interp-computed-lite │  234.54   234.17   0.16 │  2253064833315   2253044260936   0.00 │  870348   866156   0.48 │
│              coq-mathcomp-ssreflect │   88.95    88.74   0.24 │   601415317243    601421887782  -0.00 │ 1637780  1638244  -0.03 │
│               coq-mathcomp-analysis │  536.32   535.01   0.24 │  3856901764111   3857423108526  -0.01 │ 1571324  1571236   0.01 │
│                        coq-coqprime │   52.63    52.46   0.32 │   360703009585    360666014371   0.01 │  794276   794472  -0.02 │
│                         coq-unimath │ 2298.05  2287.85   0.45 │ 18100140371635  18100003353607   0.00 │ 1088156  1090440  -0.21 │
│                      coq-coquelicot │   37.68    37.45   0.61 │   226559333156    226554821311   0.00 │  814332   816280  -0.24 │
│               coq-mathcomp-fingroup │   26.06    25.74   1.24 │   169180138302    169168936006   0.01 │  587304   587084   0.04 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-rewriter-perf-SuperFast (in NEW)

🐢 Top 25 slow downs

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                              TOP 25 SLOW DOWNS                                                              │
│                                                                                                                                             │
│   OLD       NEW      DIFF   %DIFF   Ln                     FILE                                                                             │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  64.6490   66.2530  1.6040  2.48%   609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html      │
│ 118.3310  119.5180  1.1870  1.00%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                             │
│  47.7840   48.3800  0.5960  1.25%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                        │
│  46.2620   46.8160  0.5540  1.20%   110  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html       │
│  64.7520   65.2210  0.4690  0.72%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                        │
│  56.4300   56.8970  0.4670  0.83%   731  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                              │
│  12.5160   12.9510  0.4350  3.48%  1555  coq-fiat-crypto-with-bedrock/src/Util/FSets/FMapTrie.v.html                                        │
│  18.1900   18.6030  0.4130  2.27%   459  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialPER.v.html              │
│  31.3600   31.7640  0.4040  1.29%    97  coq-vst/veric/binop_lemmas5.v.html                                                                 │
│  46.2510   46.6490  0.3980  0.86%   110  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                                         │
│  24.4310   24.8210  0.3900  1.60%   558  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html  │
│  20.2810   20.6630  0.3820  1.88%   297  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Universal.v.html             │
│  25.5500   25.9270  0.3770  1.48%   375  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                        │
│  25.5710   25.9290  0.3580  1.40%   374  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                        │
│  24.5370   24.8850  0.3480  1.42%   558  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                    │
│  42.3470   42.6750  0.3280  0.77%   834  coq-vst/veric/binop_lemmas4.v.html                                                                 │
│  38.9720   39.2820  0.3100  0.80%   548  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                   │
│  26.5430   26.8450  0.3020  1.14%    68  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html │
│   5.9660    6.2610  0.2950  4.94%     5  coq-fiat-crypto-with-bedrock/src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.v.html     │
│  18.0770   18.3550  0.2780  1.54%   481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                                  │
│  15.9790   16.2520  0.2730  1.71%   197  coq-fiat-crypto-with-bedrock/src/Demo.v.html                                                       │
│  14.5260   14.7890  0.2630  1.81%  3158  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html                                │
│  39.1480   39.4020  0.2540  0.65%   835  coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html                                             │
│ 199.5870  199.8260  0.2390  0.12%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html      │
│   7.9940    8.2300  0.2360  2.95%   559  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialPER.v.html              │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                  TOP 25 SPEED UPS                                                                   │
│                                                                                                                                                     │
│   OLD       NEW      DIFF     %DIFF    Ln                      FILE                                                                                 │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 177.9460  175.1050  -2.8410   -1.60%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│  38.5450   37.3780  -1.1670   -3.03%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                        │
│  37.0650   36.0950  -0.9700   -2.62%     2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                                 │
│  38.3790   37.4100  -0.9690   -2.52%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html                     │
│ 102.3830  101.7670  -0.6160   -0.60%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│  22.5100   21.9450  -0.5650   -2.51%    49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                                 │
│  29.0010   28.4650  -0.5360   -1.85%    12  coq-fourcolor/theories/proof/job563to588.v.html                                                         │
│  30.2930   29.7570  -0.5360   -1.77%    12  coq-fourcolor/theories/proof/job001to106.v.html                                                         │
│  25.6660   25.1310  -0.5350   -2.08%    12  coq-fourcolor/theories/proof/job535to541.v.html                                                         │
│  23.6770   23.1680  -0.5090   -2.15%    12  coq-fourcolor/theories/proof/job495to498.v.html                                                         │
│  28.7110   28.2270  -0.4840   -1.69%    32  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html                    │
│  29.1200   28.6440  -0.4760   -1.63%   144  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                            │
│ 102.3730  101.9100  -0.4630   -0.45%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│  24.4000   23.9460  -0.4540   -1.86%    12  coq-fourcolor/theories/proof/job486to489.v.html                                                         │
│  33.2810   32.8420  -0.4390   -1.32%    12  coq-fourcolor/theories/proof/job439to465.v.html                                                         │
│  27.1630   26.7400  -0.4230   -1.56%   147  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                            │
│  26.7250   26.3030  -0.4220   -1.58%    35  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html                    │
│  20.9620   20.5650  -0.3970   -1.89%   213  coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html                                        │
│   1.2110    0.8560  -0.3550  -29.31%  2498  coq-metacoq-pcuic/pcuic/theories/PCUICConversion.v.html                                                 │
│   2.1940    1.8410  -0.3530  -16.09%   957  coq-metacoq-safechecker/safechecker/theories/PCUICSafeRetyping.v.html                                   │
│  25.4840   25.1530  -0.3310   -1.30%    12  coq-fourcolor/theories/proof/job517to530.v.html                                                         │
│  27.0320   26.7050  -0.3270   -1.21%    12  coq-fourcolor/theories/proof/job531to534.v.html                                                         │
│   9.2900    8.9740  -0.3160   -3.40%   550  coq-metacoq-erasure/erasure/theories/ErasureFunctionProperties.v.html                                   │
│  26.6190   26.3060  -0.3130   -1.18%    12  coq-fourcolor/theories/proof/job190to206.v.html                                                         │
│  24.7380   24.4380  -0.3000   -1.21%    12  coq-fourcolor/theories/proof/job503to506.v.html                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[Janno]

The failure in coq-rewriter-perf-SuperFast (in NEW) looks unrelated.

[gares]

One example is the Fractional class in iris which even in iris itself has 22 instances. All of those instances will always match any Fractional query.

@Janno would you mind sharing your analysis. Are the instances something like Fractional f but the goal Fractional [eta f] (or Fractional [eta g]) or the converse? From the PR description it looks like the instances are expanded, but that looks weird to me.
CC @FissoreD

[Janno]

@Janno would you mind sharing your analysis. Are the instances something like Fractional f but the goal Fractional [eta f] (or Fractional [eta g]) or the converse? From the PR description it looks like the instances are expanded, but that looks weird to me.

No, it's simpler than that. All the instances are Fractional (fun q => ...) which is translated to Fractional _ in the dnet and thus matches any query.

[SkySkimmer]

The failure in coq-rewriter-perf-SuperFast (in NEW) looks unrelated.

mit-plv/rewriter#167

[SkySkimmer]

@Janno did you run this on your private bench?

[Janno]

Yes. But we do not currently use classes such as Fractional in interesting ways in our automation—mostly because we didn't know how to do the prefiltering of fun terms efficiently enough for us to rely on it. Now that we know a better approximation we will very likely implement it soon in our prolog-based prefiltering step. But even then we wouldn't get interesting performance results because nothing currently relies on discriminating fun terms, I think.

For now, the results are mildly positive. There are some files that see bigger speedups because of typeclasses that interact with Fractional and friends in some way. I see at least one places where apply _ takes 0.01s instead of 1s.

Relative	Master	MR	Change	Filename
-0.01%	30815.4	30812.5	-3.0	cpp2v-generated
-0.10%	87326.9	87239.4	-87.5	other
-0.08%	118142.3	118051.9	-90.5	total

[Janno]

@coqbot bench

[coqbot-app]

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│            coq-metacoq-translations │   16.55    16.75  -1.19 │   118120286691    118129370986  -0.01 │  786208   787568  -0.17 │
│                 coq-metacoq-erasure │  512.84   516.85  -0.78 │  3560657138876   3576570423325  -0.44 │ 1827680  1857160  -1.59 │
│                       coq-equations │    8.34     8.40  -0.71 │    56676301726     56671657968   0.01 │  389720   389560   0.04 │
│             coq-metacoq-safechecker │  345.97   348.41  -0.70 │  2633661763952   2638223056917  -0.17 │ 1666980  1673676  -0.40 │
│                  coq-mathcomp-field │   90.26    90.69  -0.47 │   644828842520    644928267099  -0.02 │ 1264384  1264388  -0.00 │
│                      coq-coquelicot │   37.40    37.56  -0.43 │   226288191650    226319580830  -0.01 │  811340   813216  -0.23 │
│               coq-mathcomp-solvable │   90.56    90.93  -0.41 │   628694681486    629261193180  -0.09 │  944996   948968  -0.42 │
│          coq-performance-tests-lite │  911.08   914.06  -0.33 │  7307398076105   7304688084519   0.04 │ 2471460  2469448   0.08 │
│              coq-mathcomp-ssreflect │   87.71    87.94  -0.26 │   601478966539    601373885915   0.02 │ 1638568  1638124   0.03 │
│                    coq-fiat-parsers │  275.32   276.04  -0.26 │  2133173411734   2132628618412   0.03 │ 2265568  2264092   0.07 │
│                coq-metacoq-template │  147.62   147.96  -0.23 │   991985980031    992812597625  -0.08 │ 1058284  1057056   0.12 │
│                       coq-fourcolor │ 1353.92  1356.83  -0.21 │ 12540464808894  12540812753792  -0.00 │  890312   889940   0.04 │
│              coq-mathcomp-odd-order │  486.89   487.77  -0.18 │  3450588618812   3450635125645  -0.00 │ 1610520  1607236   0.20 │
│                  coq-metacoq-common │   67.48    67.60  -0.18 │   439885628009    440399046430  -0.12 │ 1058500  1056864   0.15 │
│                   coq-metacoq-pcuic │  674.81   675.88  -0.16 │  4355979420258   4387940868129  -0.73 │ 2266608  2286600  -0.87 │
│               coq-engine-bench-lite │  129.68   129.84  -0.12 │   970495430286    969673340759   0.08 │ 1076648  1076760  -0.01 │
│               coq-mathcomp-fingroup │   25.86    25.89  -0.12 │   169105030154    169202012041  -0.06 │  587276   589008  -0.29 │
│                coq-mathcomp-algebra │  160.32   160.48  -0.10 │  1126908939665   1127271869617  -0.03 │ 1188836  1183648   0.44 │
│        coq-fiat-crypto-with-bedrock │ 5833.66  5837.94  -0.07 │ 47364853324760  47361768218693   0.01 │ 3245344  3245408  -0.00 │
│                        rocq-runtime │   73.95    74.00  -0.07 │   536543172406    536038537680   0.09 │  482736   482816  -0.02 │
│              coq-mathcomp-character │   74.43    74.48  -0.07 │   511095993346    511005060297   0.02 │ 1180920  1181152  -0.02 │
│                           coq-color │  248.16   248.31  -0.06 │  1565589011236   1564598766418   0.06 │ 1082192  1082700  -0.05 │
│                        coq-rewriter │  334.89   335.01  -0.04 │  2512836089361   2512477048058   0.01 │ 1305164  1308808  -0.28 │
│                    coq-math-classes │   86.37    86.38  -0.01 │   529545400917    529454669480   0.02 │  505384   505536  -0.03 │
│ coq-neural-net-interp-computed-lite │  235.38   235.39  -0.00 │  2253042822244   2253000171281   0.00 │  870280   868544   0.20 │
│                            coq-core │    3.03     3.03   0.00 │    20607462949     20602762666   0.02 │   91524    91792  -0.29 │
│                            coq-hott │  159.24   159.24   0.00 │  1110147732079   1110053449390   0.01 │  460244   460212   0.01 │
│                           coq-verdi │   44.70    44.70   0.00 │   298501333876    298442399045   0.02 │  530772   531232  -0.09 │
│                          coq-stdlib │  192.35   192.33   0.01 │  1193334840217   1193755607084  -0.04 │  528992   529620  -0.12 │
│               coq-mathcomp-analysis │  533.57   533.44   0.02 │  3856525995438   3857134931826  -0.02 │ 1574036  1571844   0.14 │
│                        coq-coqprime │   52.22    52.18   0.08 │   360767924098    360697842443   0.02 │  796204   794164   0.26 │
│                      coq-verdi-raft │  533.49   532.88   0.11 │  3718491902648   3717690315700   0.02 │  833664   834508  -0.10 │
│                             coq-vst │  865.20   863.52   0.19 │  6525456186744   6525113447915   0.01 │ 2214856  2206032   0.40 │
│                         coq-bignums │   30.18    30.11   0.23 │   193799793395    193814200679  -0.01 │  478872   478856   0.00 │
│                            coq-corn │  679.27   677.57   0.25 │  4675751952976   4675165987591   0.01 │  660908   662476  -0.24 │
│                           rocq-core │    6.29     6.27   0.32 │    38905540017     38908069068  -0.01 │  437456   437052   0.09 │
│                   coq-iris-examples │  392.69   391.00   0.43 │  2619667593906   2621122302454  -0.06 │ 1105580  1108336  -0.25 │
│                        coq-bedrock2 │  326.79   325.32   0.45 │  2734816646557   2734715464721   0.00 │  888804   887872   0.10 │
│                         coq-unimath │ 2294.95  2284.00   0.48 │ 18099725401649  18099754903428  -0.00 │ 1090224  1090688  -0.04 │
│                        coq-compcert │  305.95   304.41   0.51 │  2008359663582   2006898133805   0.07 │ 1159332  1159320   0.00 │
│                   coq-metacoq-utils │   23.34    23.20   0.60 │   152536418818    152582615370  -0.03 │  604168   604744  -0.10 │
│                       coq-fiat-core │   59.19    58.80   0.66 │   354694357896    354580414069   0.03 │  473712   474112  -0.08 │
│                 coq-category-theory │  603.10   598.91   0.70 │  4463953843052   4463519108283   0.01 │  992180   988660   0.36 │
│                         coq-coqutil │   43.22    42.90   0.75 │   270111429220    270027805211   0.03 │  560488   557692   0.50 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-rewriter-perf-SuperFast (in NEW)

🐢 Top 25 slow downs

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                   TOP 25 SLOW DOWNS                                                                   │
│                                                                                                                                                       │
│   OLD       NEW      DIFF   %DIFF   Ln                       FILE                                                                                     │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  62.3990   66.1870  3.7880   6.07%  609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                │
│  64.2080   65.5940  1.3860   2.16%  609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                                  │
│  91.2320   92.6120  1.3800   1.51%   20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                                  │
│ 117.1230  117.9170  0.7940   0.68%   22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                       │
│  17.7910   18.2660  0.4750   2.67%  481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                                            │
│  38.1040   38.5340  0.4300   1.13%    3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html                          │
│  46.1420   46.5560  0.4140   0.90%  110  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                                                   │
│  11.7680   12.1790  0.4110   3.49%  521  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/PERCategory.v.html                           │
│   4.8370    5.2010  0.3640   7.53%   19  coq-fiat-crypto-with-bedrock/src/Language/IdentifiersBasicGENERATED.v.html                                   │
│  47.7000   48.0640  0.3640   0.76%  376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                                  │
│  31.0020   31.3420  0.3400   1.10%   12  coq-fourcolor/theories/proof/job254to270.v.html                                                              │
│  10.5900   10.9300  0.3400   3.21%  551  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/PERCategory.v.html                           │
│  13.6630   13.9760  0.3130   2.29%  249  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/memory_mapped_ext_calls_compiler.v.html │
│  59.0570   59.3430  0.2860   0.48%   27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                     │
│  29.0550   29.3360  0.2810   0.97%   12  coq-fourcolor/theories/proof/job589to610.v.html                                                              │
│  18.3300   18.6080  0.2780   1.52%   12  coq-fourcolor/theories/proof/job311to314.v.html                                                              │
│  20.7500   21.0280  0.2780   1.34%   23  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/Arith.v.html                                                │
│   9.1990    9.4370  0.2380   2.59%  403  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialLam.v.html                        │
│   0.0000    0.2340  0.2340    inf%  574  coq-mathcomp-analysis/theories/sequences.v.html                                                              │
│  29.2760   29.5070  0.2310   0.79%   12  coq-fourcolor/theories/proof/job323to383.v.html                                                              │
│  38.3780   38.6080  0.2300   0.60%    3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                             │
│   0.0000    0.2250  0.2250    inf%  130  coq-metacoq-erasure/erasure/theories/Typed/ExtractionCorrectness.v.html                                      │
│  14.9080   15.1270  0.2190   1.47%  615  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html                      │
│   0.2400    0.4540  0.2140  89.17%  273  coq-metacoq-erasure/erasure/theories/Typed/Erasure.v.html                                                    │
│   0.0000    0.2120  0.2120    inf%  201  coq-mathcomp-analysis/theories/derive.v.html                                                                 │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                  TOP 25 SPEED UPS                                                                   │
│                                                                                                                                                     │
│   OLD       NEW      DIFF     %DIFF    Ln                      FILE                                                                                 │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 180.2190  177.1830  -3.0360   -1.68%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│  79.2920   78.1780  -1.1140   -1.40%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                                 │
│  56.3320   55.4420  -0.8900   -1.58%   731  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                                   │
│ 102.5120  101.8190  -0.6930   -0.68%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│   2.4520    1.9130  -0.5390  -21.98%    32  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                             │
│ 102.4330  101.9090  -0.5240   -0.51%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│  42.6130   42.1300  -0.4830   -1.13%   834  coq-vst/veric/binop_lemmas4.v.html                                                                      │
│   9.3550    8.8940  -0.4610   -4.93%   550  coq-metacoq-erasure/erasure/theories/ErasureFunctionProperties.v.html                                   │
│  24.4610   24.0530  -0.4080   -1.67%    12  coq-fourcolor/theories/proof/job231to234.v.html                                                         │
│  30.4160   30.0100  -0.4060   -1.33%   607  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                                   │
│  21.6220   21.2320  -0.3900   -1.80%    12  coq-fourcolor/theories/proof/job511to516.v.html                                                         │
│   2.2030    1.8150  -0.3880  -17.61%   957  coq-metacoq-safechecker/safechecker/theories/PCUICSafeRetyping.v.html                                   │
│   1.9480    1.5610  -0.3870  -19.87%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                             │
│  23.3580   23.0030  -0.3550   -1.52%   373  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html                                      │
│   1.1640    0.8150  -0.3490  -29.98%  2498  coq-metacoq-pcuic/pcuic/theories/PCUICConversion.v.html                                                 │
│  25.4130   25.0750  -0.3380   -1.33%    12  coq-fourcolor/theories/proof/job618to622.v.html                                                         │
│  21.2340   20.9030  -0.3310   -1.56%   213  coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html                                        │
│   9.6490    9.3200  -0.3290   -3.41%   434  coq-mathcomp-odd-order/theories/PFsection12.v.html                                                      │
│   4.1540    3.8330  -0.3210   -7.73%  1127  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/PERSubobjectClassifier.v.html           │
│  28.9670   28.6550  -0.3120   -1.08%   144  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                            │
│ 200.7630  200.4660  -0.2970   -0.15%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html           │
│   9.0040    8.7100  -0.2940   -3.27%   199  coq-mathcomp-odd-order/theories/PFsection12.v.html                                                      │
│  21.3940   21.1060  -0.2880   -1.35%    40  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/SolinasReductionReificationCache.v.html            │
│  26.6320   26.3570  -0.2750   -1.03%    35  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html                    │
│  22.2780   22.0150  -0.2630   -1.18%    12  coq-fourcolor/theories/proof/job384to398.v.html                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[Janno]

I cherry-picked the change that keeps results from recursive decomp code and applied it to the new decomp_lambda functions (in a separate commit). It doesn't seem to improve performance but at least the new code is much nicer (and also the old code, in my opinion.)

I suppose I won't touch the Everything/Nothing distinction in this PR to avoid scope creep. And if my previous change around match turns out to be wrong I will fix it in another PR.