Skip to content

Simplifications in logic_monad#22013

Open
SkySkimmer wants to merge 4 commits intorocq-prover:masterfrom
SkySkimmer:logic_simpl
Open

Simplifications in logic_monad#22013
SkySkimmer wants to merge 4 commits intorocq-prover:masterfrom
SkySkimmer:logic_simpl

Conversation

@SkySkimmer
Copy link
Copy Markdown
Contributor

@SkySkimmer SkySkimmer commented May 8, 2026

No description provided.

@SkySkimmer SkySkimmer requested a review from a team as a code owner May 8, 2026 15:05
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label May 8, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label May 8, 2026
@SkySkimmer
Copy link
Copy Markdown
Contributor Author

SkySkimmer commented May 8, 2026

@coqbot bench

@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label May 8, 2026
@SkySkimmer SkySkimmer requested review from a team as code owners May 8, 2026 18:40
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label May 8, 2026
@coqbot-app
Copy link
Copy Markdown
Contributor

coqbot-app Bot commented May 9, 2026

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│          rocq-metarocq-translations │   15.63    15.74  -0.70 │   111110903886    111076269246   0.03 │  783868   780860   0.39 │
│                        rocq-bignums │   25.18    25.34  -0.63 │   160287535020    160128244482   0.10 │  460224   458952   0.28 │
│          coq-performance-tests-lite │  904.79   909.85  -0.56 │  7229157184566   7232817684816  -0.05 │ 1289672  1314320  -1.88 │
│                           rocq-elpi │   16.12    16.21  -0.56 │   116148846019    116141982443   0.01 │  448772   448732   0.01 │
│                 rocq-mathcomp-order │   80.99    81.41  -0.52 │   600239276294    600238111944   0.00 │ 1592372  1589596   0.17 │
│                         coq-unimath │ 1835.10  1841.36  -0.34 │ 15259884814295  15258205062457   0.01 │ 1101852  1095348   0.59 │
│                        coq-bedrock2 │  361.13   362.04  -0.25 │  2993717189097   2991671946003   0.07 │  836776   832048   0.57 │
│                         coq-coqutil │   47.18    47.26  -0.17 │   293263084372    292735955311   0.18 │  563996   563688   0.05 │
│                        rocq-runtime │   76.17    76.27  -0.13 │   550423357343    550442293382  -0.00 │  495428   494312   0.23 │
│         coq-rewriter-perf-SuperFast │  475.02   475.44  -0.09 │  3714321923159   3714507663358  -0.01 │ 1251560  1245280   0.50 │
│                 rocq-metarocq-pcuic │  650.31   650.57  -0.04 │  4127259048661   4124065541546   0.08 │ 2454080  2449200   0.20 │
│                rocq-metarocq-common │   40.91    40.92  -0.02 │   263446119821    263236679375   0.08 │  902476   894232   0.92 │
│                            coq-core │    2.83     2.83  -0.00 │    18566553780     18566384383   0.00 │   91312    90720   0.65 │
│             rocq-mathcomp-ssreflect │    1.11     1.11   0.00 │     7112060854      7111486236   0.01 │  591632   594964  -0.56 │
│                    coq-fiat-parsers │  277.46   277.33   0.05 │  2124431447066   2122006496010   0.11 │ 2271976  2255760   0.72 │
│                  rocq-mathcomp-boot │   39.48    39.46   0.05 │   233260528333    233178050203   0.04 │  659928   657952   0.30 │
│                   coq-iris-examples │  365.43   365.24   0.05 │  2393667455605   2393575685888   0.00 │ 1090404  1089780   0.06 │
│                 coq-category-theory │  556.05   555.75   0.05 │  4052134569447   4052223097827  -0.00 │  867192   924500  -6.20 │
│                    coq-math-classes │   82.97    82.91   0.07 │   502709116664    502301114466   0.08 │  514296   514372  -0.01 │
│        coq-fiat-crypto-with-bedrock │ 7288.46  7282.79   0.08 │ 60094582708008  60054657685462   0.07 │ 2989772  2979880   0.33 │
│                      coq-coquelicot │   39.26    39.22   0.10 │   237670170199    236964956723   0.30 │  828856   830556  -0.20 │
│                      coq-verdi-raft │  497.12   496.61   0.10 │  3430990255702   3427138038677   0.11 │  830348   814368   1.96 │
│                        coq-rewriter │  333.38   332.66   0.22 │  2472931120470   2471643289376   0.05 │ 1475232  1466944   0.56 │
│               rocq-metarocq-erasure │  477.88   476.84   0.22 │  3266413747298   3263223095509   0.10 │ 1805136  1788952   0.90 │
│              rocq-metarocq-template │   83.44    83.23   0.25 │   569937364662    569717697006   0.04 │ 1088628  1088560   0.01 │
│ coq-neural-net-interp-computed-lite │  237.28   236.64   0.27 │  2266812940873   2266583945056   0.01 │  882544   880788   0.20 │
│                            coq-corn │  661.71   659.84   0.28 │  4436754495580   4435633047152   0.03 │  737932   767836  -3.89 │
│                       coq-fiat-core │   55.67    55.51   0.29 │   337926889215    337175486781   0.22 │  483048   480312   0.57 │
│                           coq-color │  232.06   231.36   0.30 │  1469023188171   1467364147911   0.11 │ 1165732  1166028  -0.03 │
│               coq-engine-bench-lite │  129.33   128.81   0.40 │   960768328732    960694812208   0.01 │ 1106324  1006108   9.96 │
│                           coq-verdi │   43.85    43.64   0.48 │   289945083382    289841712096   0.04 │  527936   530724  -0.53 │
│                 rocq-metarocq-utils │   24.38    24.25   0.54 │   157422859629    157314792030   0.07 │  584804   591032  -1.05 │
│                         rocq-stdlib │  439.98   437.61   0.54 │  1556212046343   1554676092207   0.10 │  631904   628160   0.60 │
│           rocq-metarocq-safechecker │  345.38   343.14   0.65 │  2517433551191   2516548788509   0.04 │ 1853212  1851968   0.07 │
│                        coq-coqprime │   53.60    53.25   0.66 │   362885422171    362642283766   0.07 │  824228   824140   0.01 │
│                            coq-hott │  160.04   158.83   0.76 │  1074226142427   1073903326380   0.03 │  470328   468608   0.37 │
│                           rocq-core │    6.89     6.83   0.88 │    41664920747     41650980895   0.03 │  447268   444644   0.59 │
│                      rocq-equations │    8.63     8.51   1.41 │    58709120445     58660296047   0.08 │  400752   400212   0.13 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
rocq-mathcomp-fingroup (in NEW)
coq-compcert (dependency install failed in NEW)

rocq-mathcomp-algebra (dependency rocq-mathcomp-fingroup failed)
rocq-mathcomp-solvable (dependency rocq-mathcomp-fingroup failed)
rocq-mathcomp-field (dependency rocq-mathcomp-fingroup failed)
rocq-mathcomp-character (dependency rocq-mathcomp-fingroup failed)
coq-mathcomp-odd-order (dependency rocq-mathcomp-fingroup failed)
coq-mathcomp-analysis (dependency rocq-mathcomp-fingroup failed)
coq-fourcolor (dependency rocq-mathcomp-fingroup failed)
coq-vst (dependency coq-compcert failed)

🐢 Top 25 slow downs 
┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                           TOP 25 SLOW DOWNS                                                            │
│                                                                                                                                        │
│  OLD    NEW    DIFF    %DIFF   Ln                     FILE                                                                             │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  63.3   67.2  3.8769    6.13%  608  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html      │
│  48.6   49.5  0.9205    1.89%  376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                        │
│  50.8   51.6  0.7679    1.51%  571  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                         │
│  44.0   44.7  0.6389    1.45%    3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                   │
│   201    201  0.5521    0.27%    8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html      │
│  44.3   44.8  0.5323    1.20%    3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html                │
│  27.5   28.0  0.5224    1.90%   68  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html │
│   107    107  0.5164    0.48%   22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                             │
│  20.9   21.4  0.4785    2.29%  338  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                        │
│  3.86   4.32  0.4651   12.06%  196  rocq-stdlib/theories/ZArith/ZModOffset.v.html                                                      │
│  18.3   18.7  0.4012    2.19%  481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                                  │
│  23.7   24.1  0.3945    1.67%  129  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html                              │
│  55.8   56.2  0.3603    0.65%  516  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                         │
│  42.5   42.8  0.3529    0.83%    2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                            │
│  95.0   95.4  0.3483    0.37%  999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                    │
│ 0.226  0.527  0.3016  133.51%  484  rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html                                               │
│  41.3   41.6  0.2982    0.72%  543  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                         │
│  36.7   36.9  0.2913    0.79%  835  coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html                                             │
│  20.8   21.1  0.2859    1.37%  479  rocq-metarocq-erasure/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v.html                   │
│  42.2   42.4  0.2684    0.64%  221  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                       │
│ 0.121  0.372  0.2503  206.26%  585  rocq-stdlib/theories/Strings/Byte.v.html                                                           │
│ 0.286  0.534  0.2485   86.94%   12  rocq-stdlib/theories/MSets/MSets.v.html                                                            │
│  9.24   9.48  0.2417    2.62%  577  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/Jacobian.v.html                       │
│  10.0   10.2  0.2354    2.35%  673  coq-rewriter/src/Rewriter/Rewriter/Wf.v.html                                                       │
│ 0.244  0.475  0.2305   94.35%    1  rocq-stdlib/theories/ZArith/Zcong.v.html                                                           │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SPEED UPS                                                            │
│                                                                                                                                        │
│  OLD    NEW    DIFF     %DIFF    Ln                     FILE                                                                           │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  42.4   38.4  -4.0064   -9.45%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                   │
│  41.1   39.6  -1.5213   -3.70%  1423  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │
│  45.3   44.0  -1.2762   -2.82%   578  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                 │
│  65.6   64.4  -1.2058   -1.84%   608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                      │
│  30.9   30.3  -0.5370   -1.74%   305  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html                               │
│  46.7   46.2  -0.5137   -1.10%   115  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                                       │
│  2.55   2.06  -0.4947  -19.37%   212  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                               │
│  59.5   59.0  -0.4412   -0.74%   659  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                            │
│  55.9   55.5  -0.4123   -0.74%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                         │
│  22.4   22.0  -0.3917   -1.75%   651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                        │
│  21.3   20.9  -0.3821   -1.79%    24  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html                            │
│  24.4   24.1  -0.3416   -1.40%   782  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                             │
│  16.2   15.8  -0.3389   -2.10%   632  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html          │
│  14.1   13.8  -0.3297   -2.33%   216  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                         │
│  21.8   21.5  -0.3167   -1.45%    49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                          │
│ 0.998  0.692  -0.3061  -30.67%   214  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                               │
│  83.4   83.1  -0.2972   -0.36%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                          │
│  12.3   12.0  -0.2948   -2.39%   324  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html         │
│ 0.551  0.261  -0.2898  -52.59%   707  rocq-stdlib/theories/MSets/MSetList.v.html                                                       │
│  8.14   7.85  -0.2878   -3.54%   633  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html         │
│ 0.835  0.549  -0.2864  -34.29%   816  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                        │
│ 0.677  0.404  -0.2736  -40.39%   160  rocq-stdlib/theories/Numbers/HexadecimalNat.v.html                                               │
│  14.7   14.4  -0.2711   -1.85%   656  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                             │
│  12.2   11.9  -0.2575   -2.11%   388  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html         │
│  12.2   11.9  -0.2494   -2.05%    14  coq-fiat-crypto-with-bedrock/src/Language/IdentifiersGENERATED.v.html                            │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@coqbot-app
Copy link
Copy Markdown
Contributor

coqbot-app Bot commented May 9, 2026

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│                           rocq-core │    6.80     6.88  -1.16 │    41674713957     41647353617   0.07 │  443508   443700  -0.04 │
│                        rocq-runtime │   75.49    76.25  -1.00 │   550498982874    550457692972   0.01 │  495264   494712   0.11 │
│             rocq-mathcomp-ssreflect │    1.08     1.09  -0.92 │     7109551901      7107185610   0.03 │  591544   591600  -0.01 │
│                            coq-core │    2.69     2.71  -0.74 │    18563056916     18565363470  -0.01 │   91064    90832   0.26 │
│                         coq-unimath │ 1838.57  1844.63  -0.33 │ 15260032867270  15258361394099   0.01 │ 1111992  1098484   1.23 │
│                      coq-verdi-raft │  495.14   496.62  -0.30 │  3430944279985   3426975028518   0.12 │  830192   814280   1.95 │
│         coq-rewriter-perf-SuperFast │  474.91   476.15  -0.26 │  3714726621915   3714391366177   0.01 │ 1267196  1245452   1.75 │
│                 coq-category-theory │  555.53   556.74  -0.22 │  4052232571531   4052614320709  -0.01 │  867260   922576  -6.00 │
│                         rocq-stdlib │  443.44   444.12  -0.15 │  1556259459816   1554701816799   0.10 │  631816   630528   0.20 │
│                           rocq-elpi │   16.25    16.27  -0.12 │   116161770474    116140916576   0.02 │  450256   450044   0.05 │
│                        rocq-bignums │   25.35    25.38  -0.12 │   160297299455    160141032791   0.10 │  458512   458440   0.02 │
│                        coq-bedrock2 │  360.42   360.84  -0.12 │  2993524717576   2991590607064   0.06 │  833048   836492  -0.41 │
│                  rocq-mathcomp-boot │   39.56    39.60  -0.10 │   233277695882    233207542939   0.03 │  660236   659912   0.05 │
│                         coq-coqutil │   47.38    47.39  -0.02 │   293247921668    292707644076   0.18 │  567836   567960  -0.02 │
│                 rocq-metarocq-pcuic │  650.29   649.95   0.05 │  4127262140239   4123982874093   0.08 │ 2455348  2448804   0.27 │
│                    coq-math-classes │   82.87    82.81   0.07 │   502655134462    502311628129   0.07 │  513728   514116  -0.08 │
│                      rocq-equations │    8.51     8.50   0.12 │    58687095889     58652006381   0.06 │  400460   400816  -0.09 │
│                        coq-rewriter │  333.64   333.23   0.12 │  2472960369673   2471752028030   0.05 │ 1475772  1466912   0.60 │
│               coq-engine-bench-lite │  129.25   129.05   0.15 │   959037882145    959765332254  -0.08 │ 1106524  1110056  -0.32 │
│                 rocq-mathcomp-order │   81.41    81.22   0.23 │   600246858140    600246955099  -0.00 │ 1590744  1590380   0.02 │
│                           coq-verdi │   43.78    43.66   0.27 │   289938432082    289812588407   0.04 │  527620   526720   0.17 │
│          coq-performance-tests-lite │  904.89   902.40   0.28 │  7227908138194   7232083070462  -0.06 │ 1302928  1295696   0.56 │
│                    coq-fiat-parsers │  278.61   277.82   0.28 │  2124430123928   2121988661360   0.12 │ 2272288  2256644   0.69 │
│                   coq-iris-examples │  366.37   365.23   0.31 │  2393690514690   2393565546333   0.01 │ 1088272  1089860  -0.15 │
│                            coq-corn │  661.87   659.51   0.36 │  4436500684487   4435571841997   0.02 │  737820   770028  -4.18 │
│              rocq-metarocq-template │   83.27    82.94   0.40 │   569947042906    569718366755   0.04 │ 1086288  1086552  -0.02 │
│                           coq-color │  232.25   231.31   0.41 │  1469001887861   1467262885520   0.12 │ 1168300  1168108   0.02 │
│        coq-fiat-crypto-with-bedrock │ 7320.57  7288.41   0.44 │ 60094544124348  60054787722721   0.07 │ 2992536  2993908  -0.05 │
│ coq-neural-net-interp-computed-lite │  238.66   237.57   0.46 │  2266811482428   2266629405842   0.01 │  884988   880624   0.50 │
│                        coq-coqprime │   53.32    53.04   0.53 │   362870099350    362610925104   0.07 │  823992   823952   0.00 │
│                      coq-coquelicot │   39.43    39.22   0.54 │   237754386556    236952977462   0.34 │  829444   829480  -0.00 │
│                rocq-metarocq-common │   41.17    40.92   0.61 │   263442900930    263245983212   0.07 │  898712   896148   0.29 │
│                            coq-hott │  160.21   159.12   0.69 │  1074213350596   1073874526961   0.03 │  467492   468100  -0.13 │
│               rocq-metarocq-erasure │  479.49   476.22   0.69 │  3266435839260   3263041389303   0.10 │ 1804476  1784908   1.10 │
│                 rocq-metarocq-utils │   24.47    24.26   0.87 │   157405958812    157301929187   0.07 │  587572   590852  -0.56 │
│           rocq-metarocq-safechecker │  346.30   343.12   0.93 │  2517544578753   2516552079033   0.04 │ 1846912  1852996  -0.33 │
│                       coq-fiat-core │   56.06    55.30   1.37 │   337896386199    337170601318   0.22 │  482908   481944   0.20 │
│          rocq-metarocq-translations │   15.86    15.64   1.41 │   111102540370    111110770152  -0.01 │  782208   779832   0.30 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
rocq-mathcomp-fingroup (in NEW)
coq-compcert (dependency install failed in NEW)

rocq-mathcomp-algebra (dependency rocq-mathcomp-fingroup failed)
rocq-mathcomp-solvable (dependency rocq-mathcomp-fingroup failed)
rocq-mathcomp-field (dependency rocq-mathcomp-fingroup failed)
rocq-mathcomp-character (dependency rocq-mathcomp-fingroup failed)
coq-mathcomp-odd-order (dependency rocq-mathcomp-fingroup failed)
coq-mathcomp-analysis (dependency rocq-mathcomp-fingroup failed)
coq-fourcolor (dependency rocq-mathcomp-fingroup failed)
coq-vst (dependency coq-compcert failed)

🐢 Top 25 slow downs 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                          TOP 25 SLOW DOWNS                                                          │
│                                                                                                                                     │
│ OLD   NEW    DIFF   %DIFF   Ln                     FILE                                                                             │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 62.7  64.8  2.0897   3.33%  608  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html      │
│ 25.0  26.6  1.6193   6.48%  788  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                               │
│ 43.9  45.2  1.2987   2.96%    3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html                │
│ 27.1  28.4  1.2917   4.77%  794  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                               │
│  202   203  1.1182   0.55%    8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html      │
│ 16.8  17.8  1.0419   6.21%  762  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                               │
│ 24.3  25.2  0.9329   3.84%  782  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                               │
│ 48.7  49.6  0.8469   1.74%  376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                        │
│ 22.9  23.7  0.8349   3.65%  776  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                               │
│  107   108  0.6836   0.64%   22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                             │
│ 83.0  83.7  0.6781   0.82%   48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                            │
│ 14.6  15.2  0.6342   4.35%  656  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                               │
│ 50.9  51.5  0.6302   1.24%  571  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                         │
│ 21.7  22.3  0.6262   2.89%   49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                            │
│ 10.3  10.9  0.5995   5.82%  743  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                               │
│ 6.88  7.47  0.5852   8.50%  604  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │
│ 9.18  9.71  0.5316   5.79%  722  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                               │
│ 7.19  7.69  0.5054   7.03%  602  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html     │
│ 1.56  2.07  0.5050  32.36%   42  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                           │
│ 36.0  36.5  0.4580   1.27%  195  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                      │
│ 10.5  10.9  0.4349   4.14%  672  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                               │
│ 59.1  59.5  0.4323   0.73%  659  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                              │
│ 63.8  64.2  0.4303   0.67%  608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                        │
│ 42.9  43.3  0.4126   0.96%    2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                            │
│ 44.6  45.0  0.4095   0.92%    3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                   │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SPEED UPS                                                             │
│                                                                                                                                         │
│  OLD    NEW    DIFF     %DIFF    Ln                     FILE                                                                            │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  41.4   40.1  -1.2181   -2.94%  1423  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html  │
│  25.3   24.1  -1.1988   -4.74%   550  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                   │
│  45.2   44.2  -0.9878   -2.19%   578  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                  │
│  31.0   30.2  -0.8744   -2.82%   305  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html                                │
│  47.0   46.3  -0.7099   -1.51%   115  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html      │
│  2.29   1.67  -0.6211  -27.09%   313  rocq-stdlib/theories/Strings/Byte.v.html                                                          │
│  12.6   12.1  -0.5930   -4.69%   324  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html          │
│  4.13   3.59  -0.5385  -13.04%   492  rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                              │
│  12.5   12.0  -0.5291   -4.23%   388  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html          │
│  8.24   7.80  -0.4400   -5.34%   633  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html          │
│ 0.772  0.348  -0.4235  -54.87%  1161  rocq-stdlib/theories/Strings/Byte.v.html                                                          │
│  7.58   7.27  -0.3057   -4.03%   663  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html             │
│  1.03  0.729  -0.2987  -29.07%   816  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                         │
│ 0.884  0.590  -0.2942  -33.29%   484  rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html                                              │
│  46.5   46.2  -0.2882   -0.62%   278  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                     │
│  2.55   2.27  -0.2803  -11.00%   212  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                                │
│  12.8   12.6  -0.2750   -2.14%   930  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html             │
│ 0.608  0.334  -0.2744  -45.11%    14  rocq-stdlib/theories/setoid_ring/Ring_polynom.v.html                                              │
│ 0.582  0.313  -0.2693  -46.24%    14  rocq-stdlib/theories/Numbers/Integer/Binary/ZBinary.v.html                                        │
│  6.55   6.29  -0.2605   -3.98%  1933  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v.html                   │
│  24.3   24.1  -0.2526   -1.04%   550  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │
│  36.8   36.6  -0.2511   -0.68%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                      │
│ 0.565  0.320  -0.2447  -43.30%    11  rocq-stdlib/theories/ZArith/Zdiv_facts.v.html                                                     │
│ 0.543  0.304  -0.2393  -44.05%    13  rocq-stdlib/theories/ZArith/Zmax.v.html                                                           │
│  18.4   18.2  -0.2344   -1.27%    32  coq-performance-tests-lite/src/pattern.v.html                                                     │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@SkySkimmer