Store template inductive data abstracted w.r.t. template levels.

[ppedrot]

All accesses to terms and sorts from a template inductive block need first to substitute the bound levels by the default template instance, just like polymorphic inductive types. Thanks to the invariants on template types, there is actually little additional work to do, because template levels can only appear in the type of parameters (not in lets!) or in the conclusion.

Overlays:

• Adapt to rocq-prover/rocq#22070. LPCIC/coq-elpi#1028
• Adapt to rocq-prover/rocq#22070. equations#721
• Adapt to rocq-prover/rocq#22070. rocq-community/paramcoq#156

[ppedrot]

@coqbot run full ci

[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-neural-net-interp-computed-lite │  236.61   241.26  -1.93 │  2265696746076   2262876001261   0.12 │  879024   882884  -0.44 │
│                           rocq-core │    6.69     6.78  -1.33 │    41360103715     41346489953   0.03 │  445284   443876   0.32 │
│                        coq-bedrock2 │  356.55   360.97  -1.22 │  2978840905127   2975904431772   0.10 │  868056   865540   0.29 │
│                         rocq-stdlib │  417.51   420.05  -0.60 │  1511315227927   1510969203830   0.02 │  758672   759540  -0.11 │
│                    coq-math-classes │   81.72    82.03  -0.38 │   499910916410    499015231366   0.18 │  513564   514260  -0.14 │
│          coq-performance-tests-lite │  881.68   884.93  -0.37 │  7124624408844   7119494769636   0.07 │ 1524368  1608896  -5.25 │
│               coq-engine-bench-lite │  127.49   127.90  -0.32 │   947754520051    948627403750  -0.09 │ 1103780  1103668   0.01 │
│                   coq-iris-examples │  363.93   365.10  -0.32 │  2389117346029   2386125200741   0.13 │ 1061628  1072040  -0.97 │
│                        rocq-bignums │   25.09    25.16  -0.28 │   160116789796    159984688619   0.08 │  460780   458892   0.41 │
│                            coq-hott │  156.46   156.82  -0.23 │  1058722786944   1058804117592  -0.01 │  476172   479104  -0.61 │
│                         coq-unimath │ 1878.00  1881.76  -0.20 │ 15739065086795  15721501684490   0.11 │ 1673964  1669468   0.27 │
│                      coq-verdi-raft │  488.80   489.70  -0.18 │  3400563438382   3395417802975   0.15 │  812520   830904  -2.21 │
│        coq-fiat-crypto-with-bedrock │ 7213.79  7219.41  -0.08 │ 59624216995366  59567878965506   0.09 │ 2872128  2869032   0.11 │
│                           coq-color │  229.46   229.48  -0.01 │  1459713271816   1453580005718   0.42 │ 1151008  1153888  -0.25 │
│                        rocq-runtime │   76.13    76.03   0.13 │   551080849153    550937642463   0.03 │  493988   494448  -0.09 │
│                        coq-compcert │  306.12   305.62   0.16 │  2005004443983   2000645655475   0.22 │ 1195544  1204408  -0.74 │
│         coq-rewriter-perf-SuperFast │  465.36   464.15   0.26 │  3656847568659   3648018137786   0.24 │ 1249684  1239824   0.80 │
│                        coq-rewriter │  330.11   329.22   0.27 │  2462006615926   2452348816399   0.39 │ 1477956  1432040   3.21 │
│                        coq-coqprime │   56.55    56.35   0.35 │   392753222298    391524552468   0.31 │  822268   823888  -0.20 │
│                    coq-fiat-parsers │  272.49   270.87   0.60 │  2093686724958   2085693662876   0.38 │ 2036896  2033940   0.15 │
│                            coq-core │    2.77     2.75   0.73 │    18610761601     18661192196  -0.27 │   91124    90884   0.26 │
│                           coq-verdi │   43.48    43.07   0.95 │   288921263280    287189685509   0.60 │  528752   522716   1.15 │
│                       coq-fiat-core │   55.29    54.75   0.99 │   336517784633    333323231934   0.96 │  482228   483028  -0.17 │
│                         coq-coqutil │   47.04    46.35   1.49 │   292616772024    290001410650   0.90 │  567344   568020  -0.12 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
rocq-elpi (in OLD)
rocq-equations (in OLD)
rocq-metarocq-utils (in NEW)
coq-vst (in NEW)

rocq-mathcomp-boot (dependency rocq-elpi failed)
rocq-mathcomp-order (dependency rocq-elpi failed)
rocq-mathcomp-ssreflect (dependency rocq-elpi failed)
rocq-mathcomp-finite-group (dependency rocq-elpi failed)
rocq-mathcomp-algebra (dependency rocq-elpi failed)
rocq-mathcomp-solvable (dependency rocq-elpi failed)
rocq-mathcomp-field (dependency rocq-elpi failed)
rocq-mathcomp-group-representation (dependency rocq-elpi failed)
coq-mathcomp-odd-order (dependency rocq-elpi failed)
coq-mathcomp-analysis (dependency rocq-elpi failed)
coq-corn (dependency rocq-elpi failed)
rocq-metarocq-common (dependency rocq-metarocq-utils failed)
rocq-metarocq-template (dependency rocq-metarocq-utils failed)
rocq-metarocq-pcuic (dependency rocq-metarocq-utils failed)
rocq-metarocq-safechecker (dependency rocq-metarocq-utils failed)
rocq-metarocq-erasure (dependency rocq-metarocq-utils failed)
rocq-metarocq-translations (dependency rocq-metarocq-utils failed)
coq-coquelicot (dependency rocq-elpi failed)
coq-fourcolor (dependency rocq-elpi failed)
coq-category-theory (dependency rocq-equations failed)

🐢 Top 25 slow downs

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                           TOP 25 SLOW DOWNS                                                           │
│                                                                                                                                       │
│  OLD    NEW    DIFF    %DIFF    Ln                     FILE                                                                           │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  39.0   39.7  0.6723    1.72%  1423  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │
│  43.2   43.8  0.5994    1.39%   578  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                 │
│  17.4   17.9  0.4557    2.61%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                        │
│  40.7   41.0  0.3327    0.82%   539  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                       │
│  21.4   21.7  0.3186    1.49%    49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                          │
│  49.6   49.9  0.3050    0.61%   567  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                       │
│  54.3   54.6  0.3039    0.56%   512  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                       │
│ 0.122  0.424  0.3021  247.23%   658  rocq-stdlib/theories/Numbers/DecimalFacts.v.html                                                 │
│ 0.109  0.403  0.2937  268.30%    18  rocq-stdlib/theories/Sorting/Permutation.v.html                                                  │
│ 0.343  0.613  0.2705   78.92%   163  rocq-stdlib/theories/Numbers/HexadecimalPos.v.html                                               │
│ 0.172  0.439  0.2670  154.97%   592  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                        │
│  16.6   16.9  0.2595    1.56%   762  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                             │
│ 0.906   1.15  0.2472   27.29%   572  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                        │
│ 0.344  0.584  0.2400   69.71%    18  rocq-stdlib/theories/ZArith/Zeven.v.html                                                         │
│ 0.289  0.525  0.2360   81.55%   374  rocq-stdlib/theories/Sorting/SetoidList.v.html                                                   │
│ 0.539  0.771  0.2317   42.99%   207  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                               │
│ 0.306  0.537  0.2307   75.40%    11  rocq-stdlib/theories/Sorting/PermutSetoid.v.html                                                 │
│  12.6   12.8  0.2224    1.77%   544  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                       │
│  42.9   43.1  0.2174    0.51%   256  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                    │
│  46.1   46.3  0.2120    0.46%   277  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                    │
│ 0.308  0.518  0.2108   68.50%    10  rocq-stdlib/theories/micromega/ZArith_hints.v.html                                               │
│ 0.313  0.520  0.2074   66.24%    13  rocq-stdlib/theories/ZArith/Zmin.v.html                                                          │
│  36.7   36.9  0.2012    0.55%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                     │
│  31.4   31.6  0.1877    0.60%   331  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord.v.html                                       │
│ 0.462  0.647  0.1853   40.12%  1161  rocq-stdlib/theories/Strings/Byte.v.html                                                         │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SPEED UPS                                                             │
│                                                                                                                                         │
│  OLD    NEW    DIFF     %DIFF   Ln                     FILE                                                                             │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   206    201  -5.1883   -2.52%    8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html      │
│  66.9   63.4  -3.5355   -5.29%  608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                        │
│  64.3   63.4  -0.8226   -1.28%  608  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html      │
│  39.1   38.3  -0.7762   -1.98%  224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                     │
│  31.8   31.0  -0.7560   -2.38%  180  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html               │
│  31.7   31.0  -0.7220   -2.28%  157  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html               │
│  32.9   32.1  -0.7208   -2.19%  121  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html               │
│  31.6   30.9  -0.6887   -2.18%  139  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html               │
│  88.8   88.1  -0.6470   -0.73%  999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                    │
│  89.0   88.3  -0.6418   -0.72%  968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                    │
│  31.6   31.0  -0.6166   -1.95%  166  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html               │
│  80.7   80.1  -0.5697   -0.71%   48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                            │
│  18.0   17.5  -0.5114   -2.85%   32  coq-performance-tests-lite/src/pattern.v.html                                                      │
│  2.07   1.57  -0.5014  -24.24%   42  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                           │
│  31.5   31.0  -0.4909   -1.56%  198  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html               │
│  31.7   31.2  -0.4809   -1.52%  214  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html               │
│  31.7   31.2  -0.4656   -1.47%  148  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html               │
│  24.3   23.9  -0.4564   -1.88%  782  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                               │
│  44.7   44.3  -0.4261   -0.95%    3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html                │
│  27.1   26.7  -0.4202   -1.55%   68  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html │
│  44.7   44.2  -0.4152   -0.93%    3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                   │
│ 0.666  0.273  -0.3935  -59.05%  398  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                                 │
│  25.8   25.4  -0.3742   -1.45%  788  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                               │
│ 0.879  0.517  -0.3623  -41.22%  682  rocq-stdlib/theories/Numbers/DecimalFacts.v.html                                                   │
│  46.1   45.8  -0.3516   -0.76%  115  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html       │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[SkySkimmer]

@coqbot merge now

[coqbot-app]

@SkySkimmer: Please take care of the following overlays:

• 22070-ppedrot-kernel-abstract-univ-inductive.sh