Enable CLI control of equiv checker rewrite passes with --asm-rewriting-pipeline, --asm-rewriting-passes
#1498
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
JasonGross
changed the title
--asm-rewriting-pipeline, --asm-rewriting-passes
JasonGross
force-pushed
the
asm-custom-rules
branch
from
d9f623a
to
3e4894a
Compare
<details><summary>Timing Diff</summary>
<p>
```
After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem)
----------------------------------------------------------------------------------------------------------------------------------------------------------------------
151m22.97s | 4384052 ko | Total Time / Peak Mem | 151m25.18s | 4380836 ko || -0m02.20s || 3216 ko | -0.02% | +0.07%
----------------------------------------------------------------------------------------------------------------------------------------------------------------------
39m12.08s | 364876 ko | fiat-amd64/p434-square.status | 41m17.38s | 359984 ko || -2m05.30s || 4892 ko | -5.05% | +1.35%
43m07.34s | 396684 ko | fiat-amd64/p434-mul.status | 41m14.78s | 385732 ko || +1m52.55s || 10952 ko | +4.54% | +2.83%
4m13.67s | 98344 ko | fiat-amd64/p384-square.status | 4m22.45s | 96620 ko || -0m08.78s || 1724 ko | -3.34% | +1.78%
1m26.71s | 64576 ko | fiat-amd64/p448-mul.status | 1m21.39s | 65472 ko || +0m05.32s || -896 ko | +6.53% | -1.36%
4m14.88s | 2554932 ko | Assembly/WithBedrock/Proofs.vo | 4m11.08s | 2555764 ko || +0m03.79s || -832 ko | +1.51% | -0.03%
1m38.28s | 1521596 ko | Assembly/EquivalenceProofs.vo | 1m35.28s | 1509416 ko || +0m03.00s || 12180 ko | +3.14% | +0.80%
0m29.01s | 49924 ko | fiat-amd64/p448-square.status | 0m32.35s | 50224 ko || -0m03.33s || -300 ko | -10.32% | -0.59%
4m41.93s | 105612 ko | fiat-amd64/p384-mul.status | 4m39.42s | 106152 ko || +0m02.50s || -540 ko | +0.89% | -0.50%
0m57.65s | 57836 ko | fiat-amd64/p521-mul.status | 0m59.01s | 57884 ko || -0m01.35s || -48 ko | -2.30% | -0.08%
0m41.68s | 1451856 ko | Assembly/Symbolic.vo | 0m40.56s | 1402828 ko || +0m01.11s || 49028 ko | +2.76% | +3.49%
0m41.01s | 1785580 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas | 0m39.27s | 1772956 ko || +0m01.73s || 12624 ko | +4.43% | +0.71%
0m40.93s | 2147868 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery | 0m41.98s | 2147808 ko || -0m01.04s || 60 ko | -2.50% | +0.00%
0m40.23s | 2147884 ko | ExtractionOCaml/word_by_word_montgomery | 0m39.13s | 2004364 ko || +0m01.09s || 143520 ko | +2.81% | +7.16%
0m32.45s | 1499668 ko | StandaloneDebuggingExamples.vo | 0m30.71s | 1491140 ko || +0m01.74s || 8528 ko | +5.66% | +0.57%
0m06.28s | 1101420 ko | CLI.vo | 0m04.99s | 1093984 ko || +0m01.29s || 7436 ko | +25.85% | +0.67%
10m08.33s | 2587612 ko | Bedrock/End2End/X25519/GarageDoor.vo | 10m08.47s | 2587172 ko || -0m00.13s || 440 ko | -0.02% | +0.01%
5m33.90s | 2724280 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo | 5m34.57s | 2689860 ko || -0m00.67s || 34420 ko | -0.20% | +1.27%
1m53.00s | 1581340 ko | Bedrock/End2End/X25519/Field25519.vo | 1m53.03s | 1578804 ko || -0m00.03s || 2536 ko | -0.02% | +0.16%
1m49.48s | 2203552 ko | Fancy/Barrett256.vo | 1m49.70s | 2219448 ko || -0m00.22s || -15896 ko | -0.20% | -0.71%
1m29.30s | 2000076 ko | SlowPrimeSynthesisExamples.vo | 1m29.64s | 1996156 ko || -0m00.34s || 3920 ko | -0.37% | +0.19%
1m12.36s | 1433096 ko | Assembly/WithBedrock/SymbolicProofs.vo | 1m11.56s | 1424368 ko || +0m00.79s || 8728 ko | +1.11% | +0.61%
1m02.97s | 4384052 ko | Bedrock/End2End/RupicolaCrypto/Derive.vo | 1m03.27s | 4380836 ko || -0m00.30s || 3216 ko | -0.47% | +0.07%
0m47.63s | 1722840 ko | Fancy/Montgomery256.vo | 0m47.57s | 1722892 ko || +0m00.06s || -52 ko | +0.12% | -0.00%
0m44.01s | 2147928 ko | ExtractionOCaml/bedrock2_solinas_reduction | 0m43.54s | 2147860 ko || +0m00.46s || 68 ko | +1.07% | +0.00%
0m42.33s | 2147748 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery | 0m42.07s | 2147848 ko || +0m00.25s || -100 ko | +0.61% | -0.00%
0m41.29s | 2147864 ko | ExtractionOCaml/solinas_reduction | 0m40.86s | 2147544 ko || +0m00.42s || 320 ko | +1.05% | +0.01%
0m40.09s | 1784984 ko | ExtractionOCaml/bedrock2_unsaturated_solinas | 0m40.08s | 1773536 ko || +0m00.01s || 11448 ko | +0.02% | +0.64%
0m38.12s | 1263824 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m37.83s | 1262776 ko || +0m00.28s || 1048 ko | +0.76% | +0.08%
0m37.64s | 1689044 ko | ExtractionOCaml/unsaturated_solinas | 0m37.21s | 1706524 ko || +0m00.42s || -17480 ko | +1.15% | -1.02%
0m37.39s | 1452272 ko | ExtractionOCaml/bedrock2_saturated_solinas | 0m37.02s | 1453464 ko || +0m00.36s || -1192 ko | +0.99% | -0.08%
0m37.36s | 1442016 ko | ExtractionOCaml/with_bedrock2_saturated_solinas | 0m36.54s | 1464612 ko || +0m00.82s || -22596 ko | +2.24% | -1.54%
0m37.31s | 1441836 ko | ExtractionOCaml/with_bedrock2_solinas_reduction | 0m36.59s | 1464708 ko || +0m00.71s || -22872 ko | +1.96% | -1.56%
0m36.47s | 1440776 ko | ExtractionOCaml/with_bedrock2_base_conversion | 0m36.54s | 1441748 ko || -0m00.07s || -972 ko | -0.19% | -0.06%
0m35.67s | 1438816 ko | ExtractionOCaml/bedrock2_base_conversion | 0m36.48s | 1441844 ko || -0m00.80s || -3028 ko | -2.22% | -0.21%
0m35.41s | 2252448 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml | 0m35.17s | 2235808 ko || +0m00.23s || 16640 ko | +0.68% | +0.74%
0m34.53s | 2218740 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml | 0m34.40s | 2197352 ko || +0m00.13s || 21388 ko | +0.37% | +0.97%
0m34.45s | 2218700 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml | 0m34.35s | 2197268 ko || +0m00.10s || 21432 ko | +0.29% | +0.97%
0m34.17s | 2147684 ko | ExtractionOCaml/solinas_reduction.ml | 0m34.27s | 2116996 ko || -0m00.10s || 30688 ko | -0.29% | +1.44%
0m33.90s | 1415940 ko | ExtractionOCaml/base_conversion | 0m33.69s | 1415780 ko || +0m00.21s || 160 ko | +0.62% | +0.01%
0m33.48s | 1415872 ko | ExtractionOCaml/saturated_solinas | 0m34.46s | 1415848 ko || -0m00.98s || 24 ko | -2.84% | +0.00%
0m33.36s | 2115648 ko | ExtractionOCaml/word_by_word_montgomery.ml | 0m33.21s | 2077176 ko || +0m00.14s || 38472 ko | +0.45% | +1.85%
0m31.66s | 2135620 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml | 0m31.36s | 2104392 ko || +0m00.30s || 31228 ko | +0.95% | +1.48%
0m31.26s | 2135580 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml | 0m31.42s | 2104200 ko || -0m00.16s || 31380 ko | -0.50% | +1.49%
0m30.15s | 2025768 ko | ExtractionOCaml/unsaturated_solinas.ml | 0m29.84s | 2011636 ko || +0m00.30s || 14132 ko | +1.03% | +0.70%
0m28.94s | 1232124 ko | ExtractionOCaml/perf_word_by_word_montgomery | 0m29.08s | 1232268 ko || -0m00.13s || -144 ko | -0.48% | -0.01%
0m28.81s | 1232212 ko | ExtractionOCaml/perf_unsaturated_solinas | 0m28.64s | 1232288 ko || +0m00.16s || -76 ko | +0.59% | -0.00%
0m27.43s | 2042592 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml | 0m27.11s | 2000996 ko || +0m00.32s || 41596 ko | +1.18% | +2.07%
0m27.35s | 2042508 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml | 0m26.59s | 2000880 ko || +0m00.76s || 41628 ko | +2.85% | +2.08%
0m27.23s | 2042508 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml | 0m27.16s | 2000916 ko || +0m00.07s || 41592 ko | +0.25% | +2.07%
0m27.15s | 2017348 ko | ExtractionOCaml/bedrock2_base_conversion.ml | 0m27.32s | 2004784 ko || -0m00.17s || 12564 ko | -0.62% | +0.62%
0m26.58s | 1955212 ko | ExtractionOCaml/base_conversion.ml | 0m25.93s | 1905052 ko || +0m00.64s || 50160 ko | +2.50% | +2.63%
0m26.52s | 2017372 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml | 0m27.11s | 2004944 ko || -0m00.58s || 12428 ko | -2.17% | +0.61%
0m26.32s | 1940208 ko | ExtractionOCaml/saturated_solinas.ml | 0m25.48s | 1891352 ko || +0m00.83s || 48856 ko | +3.29% | +2.58%
0m25.12s | 1150580 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m25.10s | 1147720 ko || +0m00.01s || 2860 ko | +0.07% | +0.24%
0m23.69s | 1353132 ko | Bedrock/End2End/RupicolaCrypto/Low.vo | 0m23.62s | 1358036 ko || +0m00.07s || -4904 ko | +0.29% | -0.36%
0m22.18s | 1121336 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m22.31s | 1117916 ko || -0m00.12s || 3420 ko | -0.58% | +0.30%
0m19.88s | 1786664 ko | ExtractionOCaml/perf_unsaturated_solinas.ml | 0m20.26s | 1780872 ko || -0m00.38s || 5792 ko | -1.87% | +0.32%
0m19.88s | 1857548 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml | 0m19.90s | 1849472 ko || -0m00.01s || 8076 ko | -0.10% | +0.43%
0m19.46s | 1136688 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m19.20s | 1129064 ko || +0m00.26s || 7624 ko | +1.35% | +0.67%
0m19.11s | 1104372 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m18.86s | 1101216 ko || +0m00.25s || 3156 ko | +1.32% | +0.28%
0m18.47s | 43728 ko | fiat-amd64/p224-mul.status | 0m18.95s | 42268 ko || -0m00.48s || 1460 ko | -2.53% | +3.45%
0m18.34s | 42392 ko | fiat-amd64/secp256k1-mul.status | 0m18.11s | 42552 ko || +0m00.23s || -160 ko | +1.27% | -0.37%
0m18.11s | 1178648 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m18.03s | 1175728 ko || +0m00.07s || 2920 ko | +0.44% | +0.24%
0m17.76s | 1106232 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m17.78s | 1103516 ko || -0m00.01s || 2716 ko | -0.11% | +0.24%
0m16.91s | 43376 ko | fiat-amd64/p224-square.status | 0m17.41s | 44016 ko || -0m00.50s || -640 ko | -2.87% | -1.45%
0m16.12s | 42516 ko | fiat-amd64/secp256k1-square.status | 0m16.78s | 43240 ko || -0m00.66s || -724 ko | -3.93% | -1.67%
0m13.03s | 1010964 ko | BoundsPipeline.vo | 0m12.85s | 1008152 ko || +0m00.17s || 2812 ko | +1.40% | +0.27%
0m12.70s | 42424 ko | fiat-amd64/p521-square.status | 0m13.55s | 42228 ko || -0m00.85s || 196 ko | -6.27% | +0.46%
0m11.75s | 1631776 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo | 0m11.49s | 1629496 ko || +0m00.25s || 2280 ko | +2.26% | +0.13%
0m10.86s | 1301816 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo | 0m10.87s | 1297796 ko || -0m00.00s || 4020 ko | -0.09% | +0.30%
0m09.80s | 1008988 ko | PushButtonSynthesis/BaseConversion.vo | 0m09.78s | 1004916 ko || +0m00.02s || 4072 ko | +0.20% | +0.40%
0m08.89s | 1018900 ko | PushButtonSynthesis/Primitives.vo | 0m08.84s | 1017008 ko || +0m00.05s || 1892 ko | +0.56% | +0.18%
0m08.83s | 37568 ko | fiat-amd64/p256-square.status | 0m08.75s | 37640 ko || +0m00.08s || -72 ko | +0.91% | -0.19%
0m08.72s | 979868 ko | PushButtonSynthesis/SmallExamples.vo | 0m08.66s | 976988 ko || +0m00.06s || 2880 ko | +0.69% | +0.29%
0m07.54s | 1012504 ko | PushButtonSynthesis/SolinasReduction.vo | 0m07.41s | 1008696 ko || +0m00.12s || 3808 ko | +1.75% | +0.37%
0m06.58s | 1019768 ko | PushButtonSynthesis/BarrettReduction.vo | 0m06.52s | 1016180 ko || +0m00.06s || 3588 ko | +0.92% | +0.35%
0m06.17s | 1070672 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m06.28s | 1066672 ko || -0m00.11s || 4000 ko | -1.75% | +0.37%
0m04.81s | 1041804 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m04.76s | 1038764 ko || +0m00.04s || 3040 ko | +1.05% | +0.29%
0m04.57s | 1013536 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m04.61s | 1010376 ko || -0m00.04s || 3160 ko | -0.86% | +0.31%
0m04.15s | 1023232 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m04.03s | 1019884 ko || +0m00.12s || 3348 ko | +2.97% | +0.32%
0m03.61s | 935080 ko | Assembly/Equivalence.vo | 0m03.66s | 931548 ko || -0m00.05s || 3532 ko | -1.36% | +0.37%
0m03.27s | 986976 ko | Bedrock/Field/Translation/Cmd.vo | 0m03.28s | 984052 ko || -0m00.00s || 2924 ko | -0.30% | +0.29%
0m03.26s | 1053776 ko | Rewriter/PerfTesting/Core.vo | 0m03.15s | 1051868 ko || +0m00.10s || 1908 ko | +3.49% | +0.18%
0m03.10s | 984352 ko | Bedrock/Field/Translation/Func.vo | 0m03.05s | 981424 ko || +0m00.05s || 2928 ko | +1.63% | +0.29%
0m03.06s | 1033576 ko | Bedrock/Field/Stringification/Stringification.vo | 0m02.88s | 1030400 ko || +0m00.18s || 3176 ko | +6.25% | +0.30%
0m03.00s | 1094052 ko | StandaloneOCamlMain.vo | 0m02.92s | 1090924 ko || +0m00.08s || 3128 ko | +2.73% | +0.28%
0m02.93s | 1101772 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.92s | 1098692 ko || +0m00.01s || 3080 ko | +0.34% | +0.28%
0m02.91s | 1119604 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m02.92s | 1116356 ko || -0m00.00s || 3248 ko | -0.34% | +0.29%
0m02.89s | 1093556 ko | StandaloneHaskellMain.vo | 0m02.73s | 1090128 ko || +0m00.16s || 3428 ko | +5.86% | +0.31%
0m02.84s | 1038616 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m02.82s | 1035400 ko || +0m00.02s || 3216 ko | +0.70% | +0.31%
0m02.83s | 1045360 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m02.81s | 1042460 ko || +0m00.02s || 2900 ko | +0.71% | +0.27%
0m02.76s | 31332 ko | fiat-amd64/curve25519-mul.status | 0m02.67s | 29664 ko || +0m00.08s || 1668 ko | +3.37% | +5.62%
0m02.64s | 1119876 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m02.68s | 1116548 ko || -0m00.04s || 3328 ko | -1.49% | +0.29%
0m02.63s | 1024664 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m02.66s | 1021800 ko || -0m00.03s || 2864 ko | -1.12% | +0.28%
0m02.61s | 1024452 ko | Bedrock/Field/Translation/Parameters/FE310.vo | 0m02.58s | 1021620 ko || +0m00.02s || 2832 ko | +1.16% | +0.27%
0m02.58s | 1024580 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m02.59s | 1021812 ko || -0m00.00s || 2768 ko | -0.38% | +0.27%
0m02.53s | 1020596 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m02.52s | 1017580 ko || +0m00.00s || 3016 ko | +0.39% | +0.29%
0m01.95s | 29080 ko | fiat-amd64/curve25519-square.status | 0m01.85s | 28976 ko || +0m00.09s || 104 ko | +5.40% | +0.35%
0m00.93s | 25328 ko | fiat-amd64/poly1305-mul.status | 0m00.91s | 25408 ko || +0m00.02s || -80 ko | +2.19% | -0.31%
0m00.78s | 24476 ko | fiat-amd64/poly1305-square.status | 0m00.75s | 24620 ko || +0m00.03s || -144 ko | +4.00% | -0.58%
0m00.57s | 121888 ko | ExtractionOCaml/unsaturated_solinas.cmi | 0m00.57s | 120588 ko || +0m00.00s || 1300 ko | +0.00% | +1.07%
0m00.57s | 122972 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi | 0m00.53s | 121192 ko || +0m00.03s || 1780 ko | +7.54% | +1.46%
0m00.57s | 500000 ko | Util/Strings/ParseFlagOptions.vo | 0m00.58s | 500096 ko || -0m00.01s || -96 ko | -1.72% | -0.01%
0m00.55s | 119452 ko | ExtractionOCaml/base_conversion.cmi | 0m00.54s | 119720 ko || +0m00.01s || -268 ko | +1.85% | -0.22%
0m00.55s | 120464 ko | ExtractionOCaml/solinas_reduction.cmi | 0m00.52s | 119420 ko || +0m00.03s || 1044 ko | +5.76% | +0.87%
0m00.54s | 119856 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi | 0m00.56s | 122760 ko || -0m00.02s || -2904 ko | -3.57% | -2.36%
0m00.54s | 122928 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi | 0m00.56s | 121116 ko || -0m00.02s || 1812 ko | -3.57% | +1.49%
0m00.54s | 123428 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi | 0m00.53s | 120500 ko || +0m00.01s || 2928 ko | +1.88% | +2.42%
0m00.53s | 119860 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi | 0m00.53s | 122836 ko || +0m00.00s || -2976 ko | +0.00% | -2.42%
0m00.52s | 122624 ko | ExtractionOCaml/bedrock2_base_conversion.cmi | 0m00.56s | 122872 ko || -0m00.04s || -248 ko | -7.14% | -0.20%
0m00.52s | 122736 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi | 0m00.55s | 123000 ko || -0m00.03s || -264 ko | -5.45% | -0.21%
0m00.52s | 119132 ko | ExtractionOCaml/saturated_solinas.cmi | 0m00.56s | 119320 ko || -0m00.04s || -188 ko | -7.14% | -0.15%
0m00.52s | 122844 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi | 0m00.53s | 122828 ko || -0m00.01s || 16 ko | -1.88% | +0.01%
0m00.52s | 120712 ko | ExtractionOCaml/word_by_word_montgomery.cmi | 0m00.58s | 120176 ko || -0m00.05s || 536 ko | -10.34% | +0.44%
0m00.51s | 123036 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi | 0m00.53s | 121340 ko || -0m00.02s || 1696 ko | -3.77% | +1.39%
0m00.49s | 123356 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi | 0m00.56s | 120700 ko || -0m00.07s || 2656 ko | -12.50% | +2.20%
0m00.18s | 61204 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi | 0m00.15s | 60996 ko || +0m00.03s || 208 ko | +20.00% | +0.34%
0m00.17s | 61144 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi | 0m00.18s | 61152 ko || -0m00.00s || -8 ko | -5.55% | -0.01%
0m00.05s | 21032 ko | fiat-amd64/p224-sub.status | 0m00.07s | 20776 ko || -0m00.02s || 256 ko | -28.57% | +1.23%
```
</p>
</details>
JasonGross
force-pushed
the
asm-custom-rules
branch
from
3e4894a
to
d09a8c7
Compare
OwenConoly
pushed a commit
that referenced
this pull request
Nov 13, 2022
…ing-pipeline`, `--asm-rewriting-passes` (#1498) <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------- 151m22.97s | 4384052 ko | Total Time / Peak Mem | 151m25.18s | 4380836 ko || -0m02.20s || 3216 ko | -0.02% | +0.07% ---------------------------------------------------------------------------------------------------------------------------------------------------------------------- 39m12.08s | 364876 ko | fiat-amd64/p434-square.status | 41m17.38s | 359984 ko || -2m05.30s || 4892 ko | -5.05% | +1.35% 43m07.34s | 396684 ko | fiat-amd64/p434-mul.status | 41m14.78s | 385732 ko || +1m52.55s || 10952 ko | +4.54% | +2.83% 4m13.67s | 98344 ko | fiat-amd64/p384-square.status | 4m22.45s | 96620 ko || -0m08.78s || 1724 ko | -3.34% | +1.78% 1m26.71s | 64576 ko | fiat-amd64/p448-mul.status | 1m21.39s | 65472 ko || +0m05.32s || -896 ko | +6.53% | -1.36% 4m14.88s | 2554932 ko | Assembly/WithBedrock/Proofs.vo | 4m11.08s | 2555764 ko || +0m03.79s || -832 ko | +1.51% | -0.03% 1m38.28s | 1521596 ko | Assembly/EquivalenceProofs.vo | 1m35.28s | 1509416 ko || +0m03.00s || 12180 ko | +3.14% | +0.80% 0m29.01s | 49924 ko | fiat-amd64/p448-square.status | 0m32.35s | 50224 ko || -0m03.33s || -300 ko | -10.32% | -0.59% 4m41.93s | 105612 ko | fiat-amd64/p384-mul.status | 4m39.42s | 106152 ko || +0m02.50s || -540 ko | +0.89% | -0.50% 0m57.65s | 57836 ko | fiat-amd64/p521-mul.status | 0m59.01s | 57884 ko || -0m01.35s || -48 ko | -2.30% | -0.08% 0m41.68s | 1451856 ko | Assembly/Symbolic.vo | 0m40.56s | 1402828 ko || +0m01.11s || 49028 ko | +2.76% | +3.49% 0m41.01s | 1785580 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas | 0m39.27s | 1772956 ko || +0m01.73s || 12624 ko | +4.43% | +0.71% 0m40.93s | 2147868 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery | 0m41.98s | 2147808 ko || -0m01.04s || 60 ko | -2.50% | +0.00% 0m40.23s | 2147884 ko | ExtractionOCaml/word_by_word_montgomery | 0m39.13s | 2004364 ko || +0m01.09s || 143520 ko | +2.81% | +7.16% 0m32.45s | 1499668 ko | StandaloneDebuggingExamples.vo | 0m30.71s | 1491140 ko || +0m01.74s || 8528 ko | +5.66% | +0.57% 0m06.28s | 1101420 ko | CLI.vo | 0m04.99s | 1093984 ko || +0m01.29s || 7436 ko | +25.85% | +0.67% 10m08.33s | 2587612 ko | Bedrock/End2End/X25519/GarageDoor.vo | 10m08.47s | 2587172 ko || -0m00.13s || 440 ko | -0.02% | +0.01% 5m33.90s | 2724280 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo | 5m34.57s | 2689860 ko || -0m00.67s || 34420 ko | -0.20% | +1.27% 1m53.00s | 1581340 ko | Bedrock/End2End/X25519/Field25519.vo | 1m53.03s | 1578804 ko || -0m00.03s || 2536 ko | -0.02% | +0.16% 1m49.48s | 2203552 ko | Fancy/Barrett256.vo | 1m49.70s | 2219448 ko || -0m00.22s || -15896 ko | -0.20% | -0.71% 1m29.30s | 2000076 ko | SlowPrimeSynthesisExamples.vo | 1m29.64s | 1996156 ko || -0m00.34s || 3920 ko | -0.37% | +0.19% 1m12.36s | 1433096 ko | Assembly/WithBedrock/SymbolicProofs.vo | 1m11.56s | 1424368 ko || +0m00.79s || 8728 ko | +1.11% | +0.61% 1m02.97s | 4384052 ko | Bedrock/End2End/RupicolaCrypto/Derive.vo | 1m03.27s | 4380836 ko || -0m00.30s || 3216 ko | -0.47% | +0.07% 0m47.63s | 1722840 ko | Fancy/Montgomery256.vo | 0m47.57s | 1722892 ko || +0m00.06s || -52 ko | +0.12% | -0.00% 0m44.01s | 2147928 ko | ExtractionOCaml/bedrock2_solinas_reduction | 0m43.54s | 2147860 ko || +0m00.46s || 68 ko | +1.07% | +0.00% 0m42.33s | 2147748 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery | 0m42.07s | 2147848 ko || +0m00.25s || -100 ko | +0.61% | -0.00% 0m41.29s | 2147864 ko | ExtractionOCaml/solinas_reduction | 0m40.86s | 2147544 ko || +0m00.42s || 320 ko | +1.05% | +0.01% 0m40.09s | 1784984 ko | ExtractionOCaml/bedrock2_unsaturated_solinas | 0m40.08s | 1773536 ko || +0m00.01s || 11448 ko | +0.02% | +0.64% 0m38.12s | 1263824 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m37.83s | 1262776 ko || +0m00.28s || 1048 ko | +0.76% | +0.08% 0m37.64s | 1689044 ko | ExtractionOCaml/unsaturated_solinas | 0m37.21s | 1706524 ko || +0m00.42s || -17480 ko | +1.15% | -1.02% 0m37.39s | 1452272 ko | ExtractionOCaml/bedrock2_saturated_solinas | 0m37.02s | 1453464 ko || +0m00.36s || -1192 ko | +0.99% | -0.08% 0m37.36s | 1442016 ko | ExtractionOCaml/with_bedrock2_saturated_solinas | 0m36.54s | 1464612 ko || +0m00.82s || -22596 ko | +2.24% | -1.54% 0m37.31s | 1441836 ko | ExtractionOCaml/with_bedrock2_solinas_reduction | 0m36.59s | 1464708 ko || +0m00.71s || -22872 ko | +1.96% | -1.56% 0m36.47s | 1440776 ko | ExtractionOCaml/with_bedrock2_base_conversion | 0m36.54s | 1441748 ko || -0m00.07s || -972 ko | -0.19% | -0.06% 0m35.67s | 1438816 ko | ExtractionOCaml/bedrock2_base_conversion | 0m36.48s | 1441844 ko || -0m00.80s || -3028 ko | -2.22% | -0.21% 0m35.41s | 2252448 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml | 0m35.17s | 2235808 ko || +0m00.23s || 16640 ko | +0.68% | +0.74% 0m34.53s | 2218740 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml | 0m34.40s | 2197352 ko || +0m00.13s || 21388 ko | +0.37% | +0.97% 0m34.45s | 2218700 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml | 0m34.35s | 2197268 ko || +0m00.10s || 21432 ko | +0.29% | +0.97% 0m34.17s | 2147684 ko | ExtractionOCaml/solinas_reduction.ml | 0m34.27s | 2116996 ko || -0m00.10s || 30688 ko | -0.29% | +1.44% 0m33.90s | 1415940 ko | ExtractionOCaml/base_conversion | 0m33.69s | 1415780 ko || +0m00.21s || 160 ko | +0.62% | +0.01% 0m33.48s | 1415872 ko | ExtractionOCaml/saturated_solinas | 0m34.46s | 1415848 ko || -0m00.98s || 24 ko | -2.84% | +0.00% 0m33.36s | 2115648 ko | ExtractionOCaml/word_by_word_montgomery.ml | 0m33.21s | 2077176 ko || +0m00.14s || 38472 ko | +0.45% | +1.85% 0m31.66s | 2135620 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml | 0m31.36s | 2104392 ko || +0m00.30s || 31228 ko | +0.95% | +1.48% 0m31.26s | 2135580 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml | 0m31.42s | 2104200 ko || -0m00.16s || 31380 ko | -0.50% | +1.49% 0m30.15s | 2025768 ko | ExtractionOCaml/unsaturated_solinas.ml | 0m29.84s | 2011636 ko || +0m00.30s || 14132 ko | +1.03% | +0.70% 0m28.94s | 1232124 ko | ExtractionOCaml/perf_word_by_word_montgomery | 0m29.08s | 1232268 ko || -0m00.13s || -144 ko | -0.48% | -0.01% 0m28.81s | 1232212 ko | ExtractionOCaml/perf_unsaturated_solinas | 0m28.64s | 1232288 ko || +0m00.16s || -76 ko | +0.59% | -0.00% 0m27.43s | 2042592 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml | 0m27.11s | 2000996 ko || +0m00.32s || 41596 ko | +1.18% | +2.07% 0m27.35s | 2042508 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml | 0m26.59s | 2000880 ko || +0m00.76s || 41628 ko | +2.85% | +2.08% 0m27.23s | 2042508 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml | 0m27.16s | 2000916 ko || +0m00.07s || 41592 ko | +0.25% | +2.07% 0m27.15s | 2017348 ko | ExtractionOCaml/bedrock2_base_conversion.ml | 0m27.32s | 2004784 ko || -0m00.17s || 12564 ko | -0.62% | +0.62% 0m26.58s | 1955212 ko | ExtractionOCaml/base_conversion.ml | 0m25.93s | 1905052 ko || +0m00.64s || 50160 ko | +2.50% | +2.63% 0m26.52s | 2017372 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml | 0m27.11s | 2004944 ko || -0m00.58s || 12428 ko | -2.17% | +0.61% 0m26.32s | 1940208 ko | ExtractionOCaml/saturated_solinas.ml | 0m25.48s | 1891352 ko || +0m00.83s || 48856 ko | +3.29% | +2.58% 0m25.12s | 1150580 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m25.10s | 1147720 ko || +0m00.01s || 2860 ko | +0.07% | +0.24% 0m23.69s | 1353132 ko | Bedrock/End2End/RupicolaCrypto/Low.vo | 0m23.62s | 1358036 ko || +0m00.07s || -4904 ko | +0.29% | -0.36% 0m22.18s | 1121336 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m22.31s | 1117916 ko || -0m00.12s || 3420 ko | -0.58% | +0.30% 0m19.88s | 1786664 ko | ExtractionOCaml/perf_unsaturated_solinas.ml | 0m20.26s | 1780872 ko || -0m00.38s || 5792 ko | -1.87% | +0.32% 0m19.88s | 1857548 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml | 0m19.90s | 1849472 ko || -0m00.01s || 8076 ko | -0.10% | +0.43% 0m19.46s | 1136688 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m19.20s | 1129064 ko || +0m00.26s || 7624 ko | +1.35% | +0.67% 0m19.11s | 1104372 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m18.86s | 1101216 ko || +0m00.25s || 3156 ko | +1.32% | +0.28% 0m18.47s | 43728 ko | fiat-amd64/p224-mul.status | 0m18.95s | 42268 ko || -0m00.48s || 1460 ko | -2.53% | +3.45% 0m18.34s | 42392 ko | fiat-amd64/secp256k1-mul.status | 0m18.11s | 42552 ko || +0m00.23s || -160 ko | +1.27% | -0.37% 0m18.11s | 1178648 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m18.03s | 1175728 ko || +0m00.07s || 2920 ko | +0.44% | +0.24% 0m17.76s | 1106232 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m17.78s | 1103516 ko || -0m00.01s || 2716 ko | -0.11% | +0.24% 0m16.91s | 43376 ko | fiat-amd64/p224-square.status | 0m17.41s | 44016 ko || -0m00.50s || -640 ko | -2.87% | -1.45% 0m16.12s | 42516 ko | fiat-amd64/secp256k1-square.status | 0m16.78s | 43240 ko || -0m00.66s || -724 ko | -3.93% | -1.67% 0m13.03s | 1010964 ko | BoundsPipeline.vo | 0m12.85s | 1008152 ko || +0m00.17s || 2812 ko | +1.40% | +0.27% 0m12.70s | 42424 ko | fiat-amd64/p521-square.status | 0m13.55s | 42228 ko || -0m00.85s || 196 ko | -6.27% | +0.46% 0m11.75s | 1631776 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo | 0m11.49s | 1629496 ko || +0m00.25s || 2280 ko | +2.26% | +0.13% 0m10.86s | 1301816 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo | 0m10.87s | 1297796 ko || -0m00.00s || 4020 ko | -0.09% | +0.30% 0m09.80s | 1008988 ko | PushButtonSynthesis/BaseConversion.vo | 0m09.78s | 1004916 ko || +0m00.02s || 4072 ko | +0.20% | +0.40% 0m08.89s | 1018900 ko | PushButtonSynthesis/Primitives.vo | 0m08.84s | 1017008 ko || +0m00.05s || 1892 ko | +0.56% | +0.18% 0m08.83s | 37568 ko | fiat-amd64/p256-square.status | 0m08.75s | 37640 ko || +0m00.08s || -72 ko | +0.91% | -0.19% 0m08.72s | 979868 ko | PushButtonSynthesis/SmallExamples.vo | 0m08.66s | 976988 ko || +0m00.06s || 2880 ko | +0.69% | +0.29% 0m07.54s | 1012504 ko | PushButtonSynthesis/SolinasReduction.vo | 0m07.41s | 1008696 ko || +0m00.12s || 3808 ko | +1.75% | +0.37% 0m06.58s | 1019768 ko | PushButtonSynthesis/BarrettReduction.vo | 0m06.52s | 1016180 ko || +0m00.06s || 3588 ko | +0.92% | +0.35% 0m06.17s | 1070672 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m06.28s | 1066672 ko || -0m00.11s || 4000 ko | -1.75% | +0.37% 0m04.81s | 1041804 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m04.76s | 1038764 ko || +0m00.04s || 3040 ko | +1.05% | +0.29% 0m04.57s | 1013536 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m04.61s | 1010376 ko || -0m00.04s || 3160 ko | -0.86% | +0.31% 0m04.15s | 1023232 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m04.03s | 1019884 ko || +0m00.12s || 3348 ko | +2.97% | +0.32% 0m03.61s | 935080 ko | Assembly/Equivalence.vo | 0m03.66s | 931548 ko || -0m00.05s || 3532 ko | -1.36% | +0.37% 0m03.27s | 986976 ko | Bedrock/Field/Translation/Cmd.vo | 0m03.28s | 984052 ko || -0m00.00s || 2924 ko | -0.30% | +0.29% 0m03.26s | 1053776 ko | Rewriter/PerfTesting/Core.vo | 0m03.15s | 1051868 ko || +0m00.10s || 1908 ko | +3.49% | +0.18% 0m03.10s | 984352 ko | Bedrock/Field/Translation/Func.vo | 0m03.05s | 981424 ko || +0m00.05s || 2928 ko | +1.63% | +0.29% 0m03.06s | 1033576 ko | Bedrock/Field/Stringification/Stringification.vo | 0m02.88s | 1030400 ko || +0m00.18s || 3176 ko | +6.25% | +0.30% 0m03.00s | 1094052 ko | StandaloneOCamlMain.vo | 0m02.92s | 1090924 ko || +0m00.08s || 3128 ko | +2.73% | +0.28% 0m02.93s | 1101772 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.92s | 1098692 ko || +0m00.01s || 3080 ko | +0.34% | +0.28% 0m02.91s | 1119604 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m02.92s | 1116356 ko || -0m00.00s || 3248 ko | -0.34% | +0.29% 0m02.89s | 1093556 ko | StandaloneHaskellMain.vo | 0m02.73s | 1090128 ko || +0m00.16s || 3428 ko | +5.86% | +0.31% 0m02.84s | 1038616 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m02.82s | 1035400 ko || +0m00.02s || 3216 ko | +0.70% | +0.31% 0m02.83s | 1045360 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m02.81s | 1042460 ko || +0m00.02s || 2900 ko | +0.71% | +0.27% 0m02.76s | 31332 ko | fiat-amd64/curve25519-mul.status | 0m02.67s | 29664 ko || +0m00.08s || 1668 ko | +3.37% | +5.62% 0m02.64s | 1119876 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m02.68s | 1116548 ko || -0m00.04s || 3328 ko | -1.49% | +0.29% 0m02.63s | 1024664 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m02.66s | 1021800 ko || -0m00.03s || 2864 ko | -1.12% | +0.28% 0m02.61s | 1024452 ko | Bedrock/Field/Translation/Parameters/FE310.vo | 0m02.58s | 1021620 ko || +0m00.02s || 2832 ko | +1.16% | +0.27% 0m02.58s | 1024580 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m02.59s | 1021812 ko || -0m00.00s || 2768 ko | -0.38% | +0.27% 0m02.53s | 1020596 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m02.52s | 1017580 ko || +0m00.00s || 3016 ko | +0.39% | +0.29% 0m01.95s | 29080 ko | fiat-amd64/curve25519-square.status | 0m01.85s | 28976 ko || +0m00.09s || 104 ko | +5.40% | +0.35% 0m00.93s | 25328 ko | fiat-amd64/poly1305-mul.status | 0m00.91s | 25408 ko || +0m00.02s || -80 ko | +2.19% | -0.31% 0m00.78s | 24476 ko | fiat-amd64/poly1305-square.status | 0m00.75s | 24620 ko || +0m00.03s || -144 ko | +4.00% | -0.58% 0m00.57s | 121888 ko | ExtractionOCaml/unsaturated_solinas.cmi | 0m00.57s | 120588 ko || +0m00.00s || 1300 ko | +0.00% | +1.07% 0m00.57s | 122972 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi | 0m00.53s | 121192 ko || +0m00.03s || 1780 ko | +7.54% | +1.46% 0m00.57s | 500000 ko | Util/Strings/ParseFlagOptions.vo | 0m00.58s | 500096 ko || -0m00.01s || -96 ko | -1.72% | -0.01% 0m00.55s | 119452 ko | ExtractionOCaml/base_conversion.cmi | 0m00.54s | 119720 ko || +0m00.01s || -268 ko | +1.85% | -0.22% 0m00.55s | 120464 ko | ExtractionOCaml/solinas_reduction.cmi | 0m00.52s | 119420 ko || +0m00.03s || 1044 ko | +5.76% | +0.87% 0m00.54s | 119856 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi | 0m00.56s | 122760 ko || -0m00.02s || -2904 ko | -3.57% | -2.36% 0m00.54s | 122928 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi | 0m00.56s | 121116 ko || -0m00.02s || 1812 ko | -3.57% | +1.49% 0m00.54s | 123428 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi | 0m00.53s | 120500 ko || +0m00.01s || 2928 ko | +1.88% | +2.42% 0m00.53s | 119860 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi | 0m00.53s | 122836 ko || +0m00.00s || -2976 ko | +0.00% | -2.42% 0m00.52s | 122624 ko | ExtractionOCaml/bedrock2_base_conversion.cmi | 0m00.56s | 122872 ko || -0m00.04s || -248 ko | -7.14% | -0.20% 0m00.52s | 122736 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi | 0m00.55s | 123000 ko || -0m00.03s || -264 ko | -5.45% | -0.21% 0m00.52s | 119132 ko | ExtractionOCaml/saturated_solinas.cmi | 0m00.56s | 119320 ko || -0m00.04s || -188 ko | -7.14% | -0.15% 0m00.52s | 122844 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi | 0m00.53s | 122828 ko || -0m00.01s || 16 ko | -1.88% | +0.01% 0m00.52s | 120712 ko | ExtractionOCaml/word_by_word_montgomery.cmi | 0m00.58s | 120176 ko || -0m00.05s || 536 ko | -10.34% | +0.44% 0m00.51s | 123036 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi | 0m00.53s | 121340 ko || -0m00.02s || 1696 ko | -3.77% | +1.39% 0m00.49s | 123356 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi | 0m00.56s | 120700 ko || -0m00.07s || 2656 ko | -12.50% | +2.20% 0m00.18s | 61204 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi | 0m00.15s | 60996 ko || +0m00.03s || 208 ko | +20.00% | +0.34% 0m00.17s | 61144 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi | 0m00.18s | 61152 ko || -0m00.00s || -8 ko | -5.55% | -0.01% 0m00.05s | 21032 ko | fiat-amd64/p224-sub.status | 0m00.07s | 20776 ko || -0m00.02s || 256 ko | -28.57% | +1.23% ``` </p> </details>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Alternate implementation of the part of #1481 that enables control of which asm passes are enabled. We go for a much more full-featured approach here, allowing the user to fully customize which rules are run, in what order, and how many times. On top of #1495, #1496, #1497.
cc @OwenConoly @andres-erbsen