Slightly less crazy implementation of atom conversion in Firstorder

[ppedrot]

The reification code of the firstorder tactic is completely bonkers, as it strongly normalizes (including δ!) all subterms appearing in a goal or hypothesis. We make it a tad less crazy by at least introducing an indirection so that normalized terms are only compared w.r.t. a unique identifier afterwards.

This should help in metacoq.

[ppedrot]

@coqbot bench

[coqbot-app]

🏁 Bench results:

┌─────────────────────────────────────┬──────────────────────────┬────────────────────────────────────────┬────────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]       │               CPU cycles               │            CPU instructions            │  max resident mem [KB]  │
│                                     │                          │                                        │                                        │                         │
│            package_name             │   NEW      OLD    PDIFF  │      NEW             OLD        PDIFF  │      NEW             OLD        PDIFF  │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼──────────────────────────┼────────────────────────────────────────┼────────────────────────────────────────┼─────────────────────────┤
│                   coq-metacoq-pcuic │  745.29   990.67  -24.77 │  3367022717901   4417488278955  -23.78 │  4990320858393   6475840322151  -22.94 │ 2825100  2676924   5.54 │
│            coq-metacoq-translations │   17.14    17.35   -1.21 │    75285694856     76131175157   -1.11 │   124572481868    124551866533    0.02 │  845252   844188   0.13 │
│                coq-metacoq-template │  149.99   151.35   -0.90 │   659898075137    667495339610   -1.14 │  1034792851908   1045655764840   -1.04 │ 1373108  1508920  -9.00 │
│              coq-mathcomp-ssreflect │  204.66   206.50   -0.89 │   923919935379    932161777669   -0.88 │  1550989628132   1550926375901    0.00 │ 1739152  1739008   0.01 │
│ coq-neural-net-interp-computed-lite │  242.77   244.87   -0.86 │  1105490274969   1116200984985   -0.96 │  2312656018670   2312645249114    0.00 │  850672   850932  -0.03 │
│                         coq-bignums │   29.35    29.56   -0.71 │   133363262640    133165877737    0.15 │   192122117586    192126117971   -0.00 │  472500   472668  -0.04 │
│         coq-rewriter-perf-SuperFast │  789.55   791.60   -0.26 │  3527516326014   3536312942794   -0.25 │  6177922807153   6177448888878    0.01 │ 1576980  1577080  -0.01 │
│                   coq-iris-examples │  469.09   469.77   -0.14 │  2121951202038   2123860763769   -0.09 │  3279903860128   3279964284443   -0.00 │ 1118836  1115376   0.31 │
│               coq-mathcomp-solvable │  120.40   120.56   -0.13 │   547865011400    548601305683   -0.13 │   873430253618    873475280461   -0.01 │  878104   878088   0.00 │
│                 coq-metacoq-erasure │  537.99   538.50   -0.09 │  2435471936146   2438351732182   -0.12 │  3814418412871   3813569418953    0.02 │ 2083472  2084032  -0.03 │
│                    coq-fiat-parsers │  308.41   308.69   -0.09 │  1364132760201   1366024718664   -0.14 │  2392865105120   2395957402232   -0.13 │ 2682832  2680688   0.08 │
│                       coq-equations │   12.07    12.08   -0.08 │    50831552588     50504485459    0.65 │    79870516043     79802335162    0.09 │  425512   427852  -0.55 │
│                          coq-stdlib │  354.50   354.79   -0.08 │  1471441949620   1471259497929    0.01 │  1257967984803   1258311239432   -0.03 │  712476   718668  -0.86 │
│                             coq-vst │  877.28   877.45   -0.02 │  3964671723001   3966466935469   -0.05 │  6717460441886   6718275298113   -0.01 │ 2208244  2208772  -0.02 │
│          coq-performance-tests-lite │  872.44   872.31    0.01 │  3923427507862   3917206875060    0.16 │  6986453208271   6986690321279   -0.00 │ 2274728  2276012  -0.06 │
│                            coq-corn │  720.33   720.13    0.03 │  3255971339117   3254618474315    0.04 │  5069578869341   5072834133290   -0.06 │  785316   787860  -0.32 │
│                        coq-bedrock2 │  366.48   366.29    0.05 │  1654633419166   1653497948917    0.07 │  3106907826904   3107155225375   -0.01 │  878372   876164   0.25 │
│                       coq-fourcolor │ 1386.21  1385.23    0.07 │  6306964562821   6302853841741    0.07 │ 12776973875413  12776942745265    0.00 │  834032   835812  -0.21 │
│                           coq-verdi │   49.21    49.17    0.08 │   220412035155    220753454963   -0.15 │   342175108972    342100238190    0.02 │  529628   532516  -0.54 │
│                        coq-rewriter │  388.23   387.89    0.09 │  1747472719855   1748694183796   -0.07 │  2935288300753   2935374685350   -0.00 │ 1478292  1476136   0.15 │
│                         coq-unimath │ 2580.25  2577.88    0.09 │ 11692535210112  11683438239011    0.08 │ 23080539180417  23082440211242   -0.01 │ 1254172  1254564  -0.03 │
│               coq-engine-bench-lite │  157.23   157.06    0.11 │   659056212681    659185742285   -0.02 │  1222426561522   1223233092315   -0.07 │ 1107736  1109804  -0.19 │
│              coq-mathcomp-odd-order │  809.66   808.75    0.11 │  3697356479190   3693985447417    0.09 │  6135423167385   6135058134800    0.01 │ 1648484  1650376  -0.11 │
│                      coq-verdi-raft │  581.66   580.88    0.13 │  2638453655642   2635624134079    0.11 │  4160263425083   4160467744496   -0.00 │  858480   858436   0.01 │
│        coq-fiat-crypto-with-bedrock │ 5952.05  5943.52    0.14 │ 26942559452057  26900094924579    0.16 │ 48054054206342  48045809589336    0.02 │ 3245860  3246012  -0.00 │
│                        coq-coqprime │   48.48    48.38    0.21 │   216414524538    215759740328    0.30 │   333172677564    333192943801   -0.01 │  785528   789124  -0.46 │
│               coq-mathcomp-fingroup │   30.77    30.70    0.23 │   140033443991    138861729961    0.84 │   210212598237    210195066063    0.01 │  564960   564692   0.05 │
│                            coq-hott │  164.48   164.10    0.23 │   730055905283    728490991296    0.21 │  1158912313394   1158941960257   -0.00 │  470180   470468  -0.06 │
│                            coq-core │  130.88   130.55    0.25 │   497483054521    497869230317   -0.08 │   531847894084    532097482907   -0.05 │  458792   457760   0.23 │
│                 coq-category-theory │  665.67   663.87    0.27 │  3012816212582   3003605771037    0.31 │  4917343707192   4917221296350    0.00 │  988132   988312  -0.02 │
│                coq-mathcomp-algebra │  244.06   243.38    0.28 │  1103933678773   1100551746464    0.31 │  1857737834740   1857630742645    0.01 │ 1319128  1324188  -0.38 │
│             coq-metacoq-safechecker │  420.09   418.31    0.43 │  1914087665998   1906400177393    0.40 │  3174590046024   3175018989719   -0.01 │ 2040248  2039804   0.02 │
│                  coq-mathcomp-field │  139.58   138.93    0.47 │   631393019489    628143191221    0.52 │  1038696196326   1038636740284    0.01 │ 1273500  1271492   0.16 │
│                        coq-compcert │  282.67   281.33    0.48 │  1267446220053   1264189184475    0.26 │  1933137840069   1933235762518   -0.01 │ 1109968  1107516   0.22 │
│                      coq-test-suite │  542.20   539.56    0.49 │  2244868396125   2234372032621    0.47 │  3858928671431   3858159371487    0.02 │ 2461636  2461592   0.00 │
│              coq-mathcomp-character │  109.85   109.20    0.60 │   499996734246    497158300792    0.57 │   790678929870    790654810824    0.00 │ 1116368  1114784   0.14 │
│                           coq-color │  254.64   252.99    0.65 │  1135701727094   1128571272674    0.63 │  1638873674512   1633589818523    0.32 │ 1166108  1170164  -0.35 │
│                       coq-fiat-core │   60.67    60.24    0.71 │   249888837677    249826874988    0.02 │   369502165106    369462010206    0.01 │  482328   484252  -0.40 │
│                    coq-math-classes │   86.80    86.09    0.82 │   387757025463    384794645896    0.77 │   538349489987    537237341346    0.21 │  502228   502396  -0.03 │
│                      coq-coquelicot │   39.80    39.47    0.84 │   175665568520    175043463658    0.36 │   247818834448    247837290558   -0.01 │  808256   807940   0.04 │
│                         coq-coqutil │   43.67    42.66    2.37 │   191054032421    187475209866    1.91 │   274984705346    271406607660    1.32 │  669224   560344  19.43 │
└─────────────────────────────────────┴──────────────────────────┴────────────────────────────────────────┴────────────────────────────────────────┴─────────────────────────┘

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                 TOP 25 SLOW DOWNS                                                                  │
│                                                                                                                                                    │
│   OLD       NEW      DIFF    %DIFF    Ln                      FILE                                                                                 │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 218.2370  220.7360  2.4990    1.15%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                                     │
│ 179.9200  181.1480  1.2280    0.68%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│   1.8830    2.8530  0.9700   51.51%  8134  coq-color/Coccinelle/term_orderings/rpo.v.html                                                          │
│  25.6260   26.4560  0.8300    3.24%   129  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html                                   │
│   1.4590    2.2860  0.8270   56.68%  8145  coq-color/Coccinelle/term_orderings/rpo.v.html                                                          │
│   0.7670    1.5740  0.8070  105.22%   105  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Translation/Proofs/UsedVarnames.v.html                   │
│   0.5990    1.4020  0.8030  134.06%    62  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Properties.v.html          │
│   0.5950    1.3620  0.7670  128.91%    62  coq-coqutil/src/coqutil/Word/Properties.v.html                                                          │
│ 235.4130  236.1040  0.6910    0.29%   141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│   0.7110    1.3970  0.6860   96.48%    98  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Translation/Proofs/UsedVarnames.v.html                   │
│  24.3620   25.0460  0.6840    2.81%    12  coq-fourcolor/theories/job319to322.v.html                                                               │
│ 130.4140  131.0220  0.6080    0.47%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│   0.5890    1.1680  0.5790   98.30%   388  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v.html          │
│  65.0810   65.5880  0.5070    0.78%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│   0.6620    1.1110  0.4490   67.82%   385  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v.html          │
│  48.7540   49.2010  0.4470    0.92%   558  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                         │
│  86.5550   86.9730  0.4180    0.48%   365  coq-mathcomp-odd-order/theories/PFsection4.v.html                                                       │
│ 135.1070  135.5100  0.4030    0.30%   155  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│  23.2590   23.6480  0.3890    1.67%    12  coq-fourcolor/theories/job554to562.v.html                                                               │
│  17.5460   17.8690  0.3230    1.84%    32  coq-performance-tests-lite/src/pattern.v.html                                                           │
│   0.3810    0.6880  0.3070   80.58%  2108  coq-stdlib/FSets/FMapFacts.v.html                                                                       │
│  28.9370   29.2210  0.2840    0.98%    12  coq-fourcolor/theories/job589to610.v.html                                                               │
│  39.4910   39.7660  0.2750    0.70%   835  coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html                                                  │
│  16.3810   16.6370  0.2560    1.56%    81  coq-fiat-crypto-with-bedrock/rupicola/src/Rupicola/Examples/Utf8/Utf8.v.html                            │
│  11.7670   12.0110  0.2440    2.07%   527  coq-fiat-crypto-with-bedrock/src/AbstractInterpretation/Wf.v.html                                       │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                              TOP 25 SPEED UPS                                                               │
│                                                                                                                                             │
│   OLD       NEW       DIFF      %DIFF    Ln                    FILE                                                                         │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 256.2600   15.6940  -240.5660  -93.88%  1629  coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html                                               │
│  64.6910   61.2560    -3.4350   -5.31%   609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │
│ 203.4010  200.9050    -2.4960   -1.23%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│   3.5620    2.6350    -0.9270  -26.02%  3222  coq-metacoq-pcuic/pcuic/theories/PCUICConfluence.v.html                                       │
│   3.5570    2.6700    -0.8870  -24.94%   490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                    │
│   2.2440    1.4020    -0.8420  -37.52%  2995  coq-metacoq-template/common/theories/uGraph.v.html                                            │
│   3.4310    2.7230    -0.7080  -20.64%  3226  coq-metacoq-pcuic/pcuic/theories/PCUICConfluence.v.html                                       │
│   3.1860    2.4930    -0.6930  -21.75%  1295  coq-metacoq-pcuic/pcuic/theories/PCUICConversion.v.html                                       │
│   2.3120    1.6230    -0.6890  -29.80%   196  coq-stdlib/setoid_ring/Ncring_tac.v.html                                                      │
│   3.1380    2.4510    -0.6870  -21.89%  1286  coq-metacoq-pcuic/pcuic/theories/PCUICConversion.v.html                                       │
│   5.4440    4.8220    -0.6220  -11.43%    52  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Common/Util.v.html                             │
│   2.0470    1.4340    -0.6130  -29.95%  2996  coq-metacoq-template/common/theories/uGraph.v.html                                            │
│  82.6720   82.0830    -0.5890   -0.71%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                       │
│   7.6780    7.1510    -0.5270   -6.86%  2813  coq-metacoq-pcuic/pcuic/theories/PCUICConfluence.v.html                                       │
│   3.0060    2.4920    -0.5140  -17.10%  3298  coq-metacoq-pcuic/pcuic/theories/PCUICConfluence.v.html                                       │
│   2.7730    2.2760    -0.4970  -17.92%  3281  coq-metacoq-pcuic/pcuic/theories/PCUICConfluence.v.html                                       │
│   6.7000    6.2730    -0.4270   -6.37%   626  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/LAN9250.v.html   │
│   0.6650    0.2590    -0.4060  -61.05%   525  coq-metacoq-template/common/theories/uGraph.v.html                                            │
│  96.0560   95.6540    -0.4020   -0.42%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│   1.4020    1.0060    -0.3960  -28.25%   854  coq-stdlib/FSets/FMapAVL.v.html                                                               │
│   1.5630    1.1910    -0.3720  -23.80%  1250  coq-metacoq-erasure/erasure/theories/ErasureFunction.v.html                                   │
│  23.6520   23.2850    -0.3670   -1.55%   296  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                    │
│  17.7300   17.3780    -0.3520   -1.99%   607  coq-mathcomp-odd-order/theories/PFsection9.v.html                                             │
│   0.5780    0.2720    -0.3060  -52.94%   319  coq-corn/metric2/FinEnum.v.html                                                               │
│   6.4050    6.1030    -0.3020   -4.72%  2495  coq-iris-examples/theories/logatom/herlihy_wing_queue/hwq.v.html                              │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[ppedrot]

The slowdown of some instances of firstorder is probably due to the fact that this PR fixes a bug, insofar as it uniformly strongly normalizes all atoms. For some reason, the And / Or trivial constructors only performed a weak-head reduction. This should go away in favour of a more reasonable approach anyways.

[SkySkimmer]

I don't know the code but the bench is very convincing.

[SkySkimmer]

@coqbot merge now