Do not create global constraints for applied template polymorphic types

[ppedrot]

This is a partial step towards rocq-prover/rfcs#90.

Backwards compatible overlays:

• Adapt w.r.t. coq/coq#19228. jwiegley/category-theory#147
• Adapt w.r.t. coq/coq#19228. JasonGross/neural-net-coq-interp#62
• Adapt w.r.t. coq/coq#19228. mit-plv/fiat-crypto#1933
• Adapt w.r.t. coq/coq#19228. PrincetonUniversity/VST#787

Depends on #19501

[ppedrot]

@coqbot bench

[SkySkimmer]

@coqbot bench

[ppedrot]

@coqbot bench and hopefully this will not be completely broken this time

[SkySkimmer]

Fixed pretyping 29d1ff5 (not pushed here to allow the bench to run)

The test suite fails on

Module C.
  Parameter A : Type.
  Parameter eq_A : A->A->bool.
  Parameter A_bl : forall x y, eq_A x y = true -> x = y.
  Parameter A_lb : forall x y, x = y -> eq_A x y = true.
  #[export] Hint Resolve A_bl A_lb : core.
  Inductive J := D : list A -> J.
  Set Printing Universes.
  Scheme Equality for J.
End C.

in SchemeEquality.

It wants to apply internal_list_beq to A, but internal_list_beq is univ monomorphic using list.u0 and now we have no preexisting constraint between the universe of A and list.u0.

[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-safechecker │  393.82   411.22  -4.23 │  1794136890120   1874057624411  -4.26 │  2975498287630   3097120969293  -3.93 │ 2044832  2043816   0.05 │
│                           coq-verdi │   48.73    49.56  -1.67 │   218346123104    221981066709  -1.64 │   339480109536    342444147017  -0.87 │  524292   528460  -0.79 │
│                       coq-equations │   11.63    11.78  -1.27 │    48897589654     49160203570  -0.53 │    77529370737     77315041060   0.28 │  415168   414528   0.15 │
│                 coq-metacoq-erasure │  539.01   543.87  -0.89 │  2440197520125   2463987955942  -0.97 │  3815536057085   3843809116011  -0.74 │ 1971124  1976156  -0.25 │
│                       coq-fiat-core │   57.46    57.97  -0.88 │   235740652724    238345816867  -1.09 │   350287749456    349574811538   0.20 │  469376   471588  -0.47 │
│                        coq-rewriter │  388.18   391.51  -0.85 │  1746240983697   1763664729268  -0.99 │  2919587952806   2940569988300  -0.71 │ 1503404  1511856  -0.56 │
│                         coq-bignums │   29.60    29.85  -0.84 │   134199974286    134380488674  -0.13 │   193445199411    192988250773   0.24 │  468372   469148  -0.17 │
│                            coq-core │  130.67   131.75  -0.82 │   498867984387    494482634924   0.89 │   532925205320    532792854534   0.02 │  458112   457960   0.03 │
│                            coq-hott │  161.71   162.95  -0.76 │   717263900544    720197026727  -0.41 │  1145216464310   1144727827688   0.04 │  464712   465124  -0.09 │
│               coq-engine-bench-lite │  157.09   158.29  -0.76 │   658842565876    664109090805  -0.79 │  1217011678970   1208948352764   0.67 │ 1060480  1061224  -0.07 │
│                    coq-fiat-parsers │  301.99   303.57  -0.52 │  1335614907903   1344498152098  -0.66 │  2359449117606   2356041954079   0.14 │ 2411356  2618980  -7.93 │
│                          coq-stdlib │  361.76   363.61  -0.51 │  1514374590418   1518256373217  -0.26 │  1278757716987   1275065583107   0.29 │  692784   682492   1.51 │
│                   coq-iris-examples │  465.35   467.67  -0.50 │  2107383974411   2115945619488  -0.40 │  3264829622409   3262102489220   0.08 │ 1080960  1075044   0.55 │
│                    coq-math-classes │   87.06    87.47  -0.47 │   388697794464    391824420354  -0.80 │   543405826297    542800984400   0.11 │  504008   503884   0.02 │
│                            coq-corn │  721.38   724.55  -0.44 │  3262371740625   3276159010534  -0.42 │  5090806404973   5085144422339   0.11 │  782992   783416  -0.05 │
│                        coq-bedrock2 │  366.23   367.77  -0.42 │  1651167590031   1658018217472  -0.41 │  3115837943754   3105745511905   0.32 │  899408   891040   0.94 │
│                 coq-category-theory │  651.92   654.53  -0.40 │  2951451485752   2960975209100  -0.32 │  4851372758326   4847536914105   0.08 │  964048   989568  -2.58 │
│                      coq-verdi-raft │  581.26   583.54  -0.39 │  2637833293054   2647500461564  -0.37 │  4141608907516   4154524155119  -0.31 │  841148   841304  -0.02 │
│                         coq-coqutil │   42.88    43.04  -0.37 │   187467196677    188482560669  -0.54 │   271416067786    270712840533   0.26 │  681316   681588  -0.04 │
│                   coq-metacoq-pcuic │  732.04   734.75  -0.37 │  3308808021352   3320750707133  -0.36 │  4875709178241   4901954203335  -0.54 │ 3213660  3230944  -0.53 │
│                           coq-color │  252.24   253.14  -0.36 │  1124782894798   1129881770634  -0.45 │  1626069292045   1623994515584   0.13 │ 1211220  1215748  -0.37 │
│         coq-rewriter-perf-SuperFast │  794.05   796.19  -0.27 │  3543976345870   3558641121552  -0.41 │  6151540001869   6209344134624  -0.93 │ 1570824  1598436  -1.73 │
│                        coq-compcert │  280.99   281.05  -0.02 │  1261021251701   1262590322936  -0.12 │  1920843255188   1915354522109   0.29 │ 1104228  1104468  -0.02 │
│                         coq-unimath │ 2579.39  2579.21   0.01 │ 11691397109695  11690826731228   0.00 │ 23123536830786  23115479464832   0.03 │ 1307792  1304268   0.27 │
│                coq-metacoq-template │  154.03   154.01   0.01 │   678372361889    679163041771  -0.12 │  1063964668106   1064581328854  -0.06 │ 1260320  1263436  -0.25 │
│                        coq-coqprime │   48.61    48.60   0.02 │   217147921344    217171588501  -0.01 │   335372789800    334276427168   0.33 │  774980   772816   0.28 │
│ coq-neural-net-interp-computed-lite │  241.28   240.94   0.14 │  1099375960856   1098231044435   0.10 │  2310276337761   2309195992629   0.05 │  836740   831168   0.67 │
│        coq-fiat-crypto-with-bedrock │ 5751.77  5742.04   0.17 │ 26019380481605  25958088999875   0.24 │ 46839493171458  46660668695630   0.38 │ 3246000  3245840   0.00 │
│          coq-performance-tests-lite │  903.72   891.08   1.42 │  4063536786582   4006938360655   1.41 │  7335749000280   7240886252187   1.31 │ 2444784  1523140  60.51 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-test-suite
coq-mathcomp-ssreflect
coq-metacoq-translations
coq-vst

coq-mathcomp-fingroup (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-algebra (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-solvable (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-field (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-character (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-odd-order (dependency coq-mathcomp-ssreflect failed)
coq-coquelicot (dependency coq-mathcomp-ssreflect failed)
coq-fourcolor (dependency coq-mathcomp-ssreflect failed)

🐢 Top 25 slow downs

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                 TOP 25 SLOW DOWNS                                                                 │
│                                                                                                                                                   │
│   OLD       NEW      DIFF   %DIFF    Ln                      FILE                                                                                 │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 130.9070  134.7520  3.8450   2.94%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│ 179.6770  182.5830  2.9060   1.62%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│ 101.6390  103.3950  1.7560   1.73%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                             │
│  16.7970   17.8530  1.0560   6.29%    32  coq-performance-tests-lite/src/pattern.v.html                                                           │
│   3.9070    4.9380  1.0310  26.39%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│  37.9830   38.8250  0.8420   2.22%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                        │
│  21.6530   22.4900  0.8370   3.87%    40  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/SolinasReductionReificationCache.v.html            │
│ 153.8050  154.6410  0.8360   0.54%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                           │
│  50.6370   51.4080  0.7710   1.52%   558  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html       │
│   2.6200    3.3380  0.7180  27.40%    34  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│  38.0590   38.7220  0.6630   1.74%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v.html                   │
│   2.3970    3.0360  0.6390  26.66%  1001  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│   3.5960    4.2070  0.6110  16.99%    35  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/SolinasReductionReificationCache.v.html            │
│  97.5650   98.1750  0.6100   0.63%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                             │
│  47.5940   48.1700  0.5760   1.21%   926  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                               │
│   7.9700    8.5460  0.5760   7.23%   860  coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html                                                  │
│  12.1800   12.7360  0.5560   4.56%   194  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                                │
│   1.9370    2.4860  0.5490  28.34%  3281  coq-metacoq-pcuic/pcuic/theories/PCUICConfluence.v.html                                                 │
│  28.6260   29.1580  0.5320   1.86%   144  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                            │
│  39.7430   40.2640  0.5210   1.31%   835  coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html                                                  │
│  29.2160   29.7020  0.4860   1.66%    79  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html       │
│  72.4620   72.9300  0.4680   0.65%   905  coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html                                    │
│   4.3350    4.7950  0.4600  10.61%  4414  coq-unimath/UniMath/HomologicalAlgebra/MappingCone.v.html                                               │
│   1.0470    1.4680  0.4210  40.21%   854  coq-stdlib/FSets/FMapAVL.v.html                                                                         │
│  46.4650   46.8750  0.4100   0.88%   110  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html            │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                TOP 25 SPEED UPS                                                                 │
│                                                                                                                                                 │
│   OLD      NEW     DIFF     %DIFF    Ln                      FILE                                                                               │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 23.0410  20.3770  -2.6640  -11.56%  1073  coq-metacoq-safechecker/safechecker/theories/PCUICSafeReduce.v.html                                   │
│ 12.0800  10.1670  -1.9130  -15.84%  1408  coq-rewriter-perf-SuperFast/src/Rewriter/Language/Wf.v.html                                           │
│ 20.3800  18.6750  -1.7050   -8.37%  2734  coq-metacoq-safechecker/safechecker/theories/PCUICTypeChecker.v.html                                  │
│ 65.0240  63.6170  -1.4070   -2.16%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                           │
│ 12.5930  11.2230  -1.3700  -10.88%     6  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.v.html   │
│ 11.3430  10.3060  -1.0370   -9.14%   789  coq-metacoq-safechecker/safechecker/theories/PCUICSafeRetyping.v.html                                 │
│ 64.1400  63.1350  -1.0050   -1.57%   609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html         │
│  4.1820   3.2320  -0.9500  -22.72%   157  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/Field25519.v.html                             │
│  3.9200   3.0300  -0.8900  -22.70%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                              │
│ 15.3180  14.4510  -0.8670   -5.66%  1382  coq-rewriter/src/Rewriter/Language/Wf.v.html                                                          │
│ 84.2380  83.3900  -0.8480   -1.01%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                               │
│ 27.8610  27.0240  -0.8370   -3.00%    68  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html    │
│ 12.0630  11.2850  -0.7780   -6.45%  1408  coq-rewriter/src/Rewriter/Language/Wf.v.html                                                          │
│ 15.2030  14.5040  -0.6990   -4.60%  1382  coq-rewriter-perf-SuperFast/src/Rewriter/Language/Wf.v.html                                           │
│ 35.0240  34.3460  -0.6780   -1.94%  1333  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html      │
│  2.8770   2.2060  -0.6710  -23.32%  3279  coq-metacoq-pcuic/pcuic/theories/PCUICConfluence.v.html                                               │
│  5.6860   5.0160  -0.6700  -11.78%     6  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeCSR.v.html │
│  8.4970   7.8500  -0.6470   -7.61%  1435  coq-metacoq-safechecker/safechecker/theories/PCUICTypeChecker.v.html                                  │
│  5.9260   5.2840  -0.6420  -10.83%   823  coq-metacoq-erasure/erasure/theories/ErasureFunction.v.html                                           │
│ 37.7980  37.2670  -0.5310   -1.40%   548  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                      │
│  5.5700   5.1140  -0.4560   -8.19%  1099  coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/StrictTwoSidedDispCat.v.html                │
│ 20.6300  20.1830  -0.4470   -2.17%   214  coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html                                  │
│ 18.6470  18.2070  -0.4400   -2.36%   957  coq-unimath/UniMath/CategoryTheory/Monoidal/Examples/DisplayedCartesianMonoidal.v.html                │
│  4.7240   4.2910  -0.4330   -9.17%   733  coq-category-theory/Construction/Comma/Adjunction.v.html                                              │
│ 20.4390  20.0260  -0.4130   -2.02%   325  coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[ppedrot]

@coqbot ci minimize

[ppedrot]

I think that the first commit of this PR can go early, it's a small restriction of the current way we do things in the kernel and cannot really affect backwards compatibility in practice. Likewise we could easily fix #19230 before making progress on this PR.

[SkySkimmer]

I think that the first commit of this PR can go early, it's a small restriction of the current way we do things in the kernel

It needs a corresponding upper layer change otherwise I think the kernel will error because we send incorrect entries.

[ppedrot]

The upper layer actually already checks that the universes do not appear in constructors.

[SkySkimmer]

Simplest fix for scheme equality d8aed29

[SkySkimmer]

@coqbot ci minimize

[ppedrot]

Why is CI minimization not working now?

[SkySkimmer]

The corresponding master pipeline got cancelled by a more recent push

[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-core │  132.01   132.61  -0.45 │   537645770275    537247353012   0.07 │  464428   463588   0.18 │
│ coq-fiat-crypto-with-bedrock │ 5240.70  5252.38  -0.22 │ 42417250684892  42480782238772  -0.15 │ 3245392  3245424  -0.00 │
│                   coq-stdlib │  346.42   343.10   0.97 │  1208030267577   1205406704660   0.22 │  635076   632976   0.33 │
└──────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-test-suite

🐢 Top 25 slow downs

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                               TOP 25 SLOW DOWNS                                                               │
│                                                                                                                                               │
│   OLD       NEW      DIFF     %DIFF     Ln                     FILE                                                                           │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  77.4270   79.1960  1.7690      2.28%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                          │
│   3.8120    5.0350  1.2230     32.08%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                           │
│   8.1540    9.2400  1.0860     13.32%   165  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                               │
│   2.5470    3.3290  0.7820     30.70%    34  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                           │
│   8.9900    9.5420  0.5520      6.14%   345  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                       │
│  17.6330   18.1110  0.4780      2.71%   708  coq-fiat-crypto-with-bedrock/src/Rewriter/RulesProofs.v.html                                     │
│   3.2020    3.5900  0.3880     12.12%   490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                       │
│  15.1650   15.5510  0.3860      2.55%   196  coq-fiat-crypto-with-bedrock/src/Demo.v.html                                                     │
│  26.3670   26.7360  0.3690      1.40%   147  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                     │
│  38.1920   38.5510  0.3590      0.94%  1350  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │
│ 235.2030  235.5300  0.3270      0.14%   141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                       │
│  28.2040   28.4970  0.2930      1.04%   144  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                     │
│  14.8860   15.1500  0.2640      1.77%   617  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html          │
│  14.6530   14.9120  0.2590      1.77%   615  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html          │
│   2.9460    3.1800  0.2340      7.94%    53  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                       │
│   9.2900    9.5200  0.2300      2.48%     7  coq-fiat-crypto-with-bedrock/src/PerfTesting/PerfTestSearchPattern.v.html                        │
│  16.5930   16.8090  0.2160      1.30%    81  coq-fiat-crypto-with-bedrock/rupicola/src/Rupicola/Examples/Utf8/Utf8.v.html                     │
│  21.0590   21.2730  0.2140      1.02%    40  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/SolinasReductionReificationCache.v.html     │
│   0.0020    0.2110  0.2090  10450.00%   531  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.v.html           │
│   0.0490    0.2490  0.2000    408.16%   606  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html                              │
│   0.6510    0.8480  0.1970     30.26%    35  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/Arith.v.html                                    │
│   0.0380    0.2340  0.1960    515.79%   175  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.v.html     │
│   0.2180    0.4110  0.1930     88.53%   747  coq-stdlib/MSets/MSetRBT.v.html                                                                  │
│   0.0490    0.2390  0.1900    387.76%  1072  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/Primitives.v.html                           │
│   0.0110    0.1950  0.1840   1672.73%  1146  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/Primitives.v.html                           │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                  TOP 25 SPEED UPS                                                                  │
│                                                                                                                                                    │
│   OLD       NEW      DIFF     %DIFF   Ln                      FILE                                                                                 │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   7.2680    5.6570  -1.6110  -22.17%  196  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│ 123.0110  121.4430  -1.5680   -1.27%   22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│  95.9000   94.5910  -1.3090   -1.36%   20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                             │
│  61.4290   60.2510  -1.1780   -1.92%   27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│  24.7340   23.6360  -1.0980   -4.44%   49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                                 │
│   3.9220    2.9810  -0.9410  -23.99%   24  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html                                   │
│  39.9870   39.1070  -0.8800   -2.20%  835  coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html                                                  │
│   3.9430    3.0650  -0.8780  -22.27%   27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│  66.0260   65.1660  -0.8600   -1.30%  609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html           │
│   9.7850    9.1120  -0.6730   -6.88%  849  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html                                 │
│   3.9440    3.3250  -0.6190  -15.69%  551  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                               │
│ 180.8460  180.3270  -0.5190   -0.29%  233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│  12.7040   12.1920  -0.5120   -4.03%   14  coq-fiat-crypto-with-bedrock/src/Language/IdentifiersGENERATED.v.html                                   │
│  38.1390   37.6500  -0.4890   -1.28%  548  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                        │
│   2.0890    1.6160  -0.4730  -22.64%   42  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│  20.2100   19.8800  -0.3300   -1.63%  213  coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html                                        │
│  22.2270   21.9010  -0.3260   -1.47%   24  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html                                   │
│   6.0340    5.7430  -0.2910   -4.82%  841  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html                                 │
│   5.9650    5.6910  -0.2740   -4.59%  840  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html                                 │
│   5.0030    4.7330  -0.2700   -5.40%  227  coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html                                        │
│  42.5210   42.2550  -0.2660   -0.63%   50  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│  21.8480   21.5830  -0.2650   -1.21%   23  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/Arith.v.html                                           │
│   1.1220    0.8570  -0.2650  -23.62%  572  coq-stdlib/MSets/MSetAVL.v.html                                                                         │
│  36.5060   36.2470  -0.2590   -0.71%    2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                                 │
│   3.3900    3.1350  -0.2550   -7.52%  256  coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html                                        │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[SkySkimmer]

Looks ok

[ppedrot]

I believe this to be ready.

[mattam82]

Looks good, will merge when CI passes.

[mattam82]

@ppedrot Hmm, could the failure in fcsl be a merge glitch?

[SkySkimmer]

cc @aleksnanevski, @clayrat

[ppedrot]

CI was green before, this was just a rebase on master after the merge of #19501. Maybe it's transient, let's @coqbot run full ci

[clayrat]

cc @aleksnanevski, @clayrat

We pushed a new version of FCSL-PCM on Friday that requires Mathcomp2 + Hierarchy Builder, the CI errors seem to imply that HB is not found.

[mattam82]

Ok, indeed all full pipelines fail on FCSL-PCM now, so this is orthogonal to the current change, I'll merge.

[mattam82]

sudo @coqbot merge now

[coqbot-app]

@mattam82: You cannot merge this PR because:

• You are not among the assignees.

[mattam82]

sudo @coqbot merge now

[proux01]

FYI, the commit "pretyping doesn't generate extra template poly constraints" breaks CoqEAL.
Here is a minimized example, depending only on paramcoq

From Coq Require Import ssreflect ssrfun ssrbool.
From Param Require Import Param.

Parametricity bool.
Parametricity simpl_fun.
Parametricity SimplRel.

Probably a bug that was already lingering in paramcoq and was made visible by this.

[proux01]

Here is a further reduced example (without ssr dependency):

From Param Require Import Param.

Inductive bool : Set :=  true : bool | false : bool.
Variant simpl_fun (aT rT : Type) : Type :=
  SimplFun : (aT -> rT) -> @simpl_fun aT rT.
Definition simpl_pred T := simpl_fun T bool.

Print Universes Subgraph (simpl_pred.u0 simpl_fun.u0).
(* 8.20.0: simpl_pred.u0 <= simpl_fun.u0 *)
(* master: no constraint *)

Definition SimplPred (p : bool -> bool) : simpl_pred bool :=
  SimplFun _ _ p.

Parametricity bool.
Parametricity simpl_fun.
Parametricity SimplPred.
(* 8.20.0: SimplPred_R is defined *)
(* master: Error: Unsatisfied constraints: simpl_pred.u0 <= simpl_fun.u0 (maybe a bugged tactic). *)

I have not much intuition about what's happening @SkySkimmer @ppedrot do you confirm that the removal of the constraint is the expected result of this PR and I must somehow adapt paramcoq to work without the constraint?

[SkySkimmer]

do you confirm that the removal of the constraint is the expected result of this PR

yes

I must somehow adapt paramcoq to work without the constraint?

paramcoq needs updating, it doesn't have to be you who does it (but @ppedrot is busy for the next few days IIUC)

[proux01]

No hurry, I'll try to have a look at paramcoq but I'll indeed likely ask for some help.

[proux01]

@ppedrot looks like you finally managed to kill paramcoq: #20114 ;-)
Congrats!