Add remaining identifiers for saturated solinas #1774
Merged
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
force-pushed
the
saturated-solinas-idents-more
branch
5 times, most recently
from
35f5cc2
to
d1f3730
Compare
This reverts commit 697a6988f1175688ca0dfda3e01712467b136595.
This adds back the remaining identifiers we need for improved saturated
solinas.
<details><summary>Timing Diff</summary>
<p>
```
After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem)
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------
76m08.32s | 2852356 ko | Total Time / Peak Mem | 66m44.53s | 2852348 ko || +9m23.79s || 8 ko | +14.07% | +0.00%
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------
9m17.84s | 1919280 ko | AbstractInterpretation/ZRangeProofs.vo | 0m55.71s | 870072 ko || +8m22.13s || 1049208 ko | +901.32% | +120.58%
0m26.70s | 752688 ko | Language/IdentifiersGENERATEDProofs.vo | 0m14.52s | 602668 ko || +0m12.17s || 150020 ko | +83.88% | +24.89%
0m25.97s | 898820 ko | Language/IdentifiersGENERATED.vo | 0m17.16s | 792348 ko || +0m08.80s || 106472 ko | +51.34% | +13.43%
3m42.96s | 1806652 ko | Rewriter/Passes/ArithWithCasts.vo | 3m35.69s | 1774188 ko || +0m07.27s || 32464 ko | +3.37% | +1.82%
1m21.77s | 1013952 ko | PushButtonSynthesis/SolinasReductionReificationCache.vo | 1m15.69s | 993216 ko || +0m06.07s || 20736 ko | +8.03% | +2.08%
3m58.49s | 2546620 ko | Assembly/WithBedrock/Proofs.vo | 4m04.05s | 2545412 ko || -0m05.56s || 1208 ko | -2.27% | +0.04%
3m09.30s | 2604680 ko | Bedrock/End2End/RupicolaCrypto/ChaCha20.vo | 3m15.25s | 2604708 ko || -0m05.94s || -28 ko | -3.04% | -0.00%
1m24.58s | 1681676 ko | Assembly/EquivalenceProofs.vo | 1m18.97s | 1522968 ko || +0m05.60s || 158708 ko | +7.10% | +10.42%
8m44.80s | 2593976 ko | Bedrock/End2End/X25519/GarageDoor.vo | 8m39.98s | 2652060 ko || +0m04.81s || -58084 ko | +0.92% | -2.19%
2m34.41s | 1638752 ko | Rewriter/Passes/NBE.vo | 2m30.90s | 1667212 ko || +0m03.50s || -28460 ko | +2.32% | -1.70%
2m30.24s | 1127108 ko | Fancy/Compiler.vo | 2m26.31s | 1118692 ko || +0m03.93s || 8416 ko | +2.68% | +0.75%
1m53.36s | 1431992 ko | Rewriter/Passes/ToFancyWithCasts.vo | 1m49.41s | 1416792 ko || +0m03.95s || 15200 ko | +3.61% | +1.07%
1m03.32s | 896792 ko | AbstractInterpretation/Bottomify/Wf.vo | 1m01.20s | 875848 ko || +0m02.11s || 20944 ko | +3.46% | +2.39%
0m52.81s | 1067140 ko | Rewriter/Passes/MultiRetSplit.vo | 0m50.71s | 1032240 ko || +0m02.10s || 34900 ko | +4.14% | +3.38%
0m29.72s | 1559056 ko | StandaloneDebuggingExamples.vo | 0m32.37s | 1554516 ko || -0m02.64s || 4540 ko | -8.18% | +0.29%
0m13.50s | 551360 ko | AbstractInterpretation/ZRangeCommonProofs.vo | 0m11.12s | 540720 ko || +0m02.38s || 10640 ko | +21.40% | +1.96%
5m30.60s | 2852356 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo | 5m32.21s | 2852348 ko || -0m01.60s || 8 ko | -0.48% | +0.00%
1m24.41s | 910104 ko | AbstractInterpretation/Fancy/Wf.vo | 1m22.60s | 951160 ko || +0m01.81s || -41056 ko | +2.19% | -4.31%
0m52.47s | 833064 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 0m50.89s | 837144 ko || +0m01.57s || -4080 ko | +3.10% | -0.48%
0m51.41s | 1122476 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo | 0m50.26s | 1126764 ko || +0m01.14s || -4288 ko | +2.28% | -0.38%
0m49.94s | 1838856 ko | Fancy/Montgomery256.vo | 0m48.68s | 1781840 ko || +0m01.25s || 57016 ko | +2.58% | +3.19%
0m41.25s | 1071284 ko | Rewriter/Passes/Arith.vo | 0m40.06s | 1064176 ko || +0m01.18s || 7108 ko | +2.97% | +0.66%
0m37.92s | 715400 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m36.47s | 713460 ko || +0m01.45s || 1940 ko | +3.97% | +0.27%
0m34.12s | 903056 ko | Rewriter/Passes/MulSplit.vo | 0m32.84s | 913248 ko || +0m01.27s || -10192 ko | +3.89% | -1.11%
0m10.23s | 654492 ko | Language/IdentifiersBasicGENERATED.vo | 0m08.46s | 607544 ko || +0m01.76s || 46948 ko | +20.92% | +7.72%
0m09.72s | 583292 ko | PushButtonSynthesis/BYInversionReificationCache.vo | 0m08.60s | 585636 ko || +0m01.12s || -2344 ko | +13.02% | -0.40%
1m52.56s | 1896276 ko | Bedrock/End2End/X25519/AddPrecomputed.vo | 1m52.99s | 1883952 ko || -0m00.43s || 12324 ko | -0.38% | +0.65%
1m52.14s | 1607068 ko | Bedrock/End2End/X25519/Field25519.vo | 1m51.98s | 1602880 ko || +0m00.16s || 4188 ko | +0.14% | +0.26%
1m51.46s | 2291012 ko | Fancy/Barrett256.vo | 1m51.48s | 2425960 ko || -0m00.01s || -134948 ko | -0.01% | -5.56%
1m31.46s | 2188740 ko | SlowPrimeSynthesisExamples.vo | 1m31.82s | 2146844 ko || -0m00.35s || 41896 ko | -0.39% | +1.95%
1m07.73s | 1441800 ko | Assembly/WithBedrock/SymbolicProofs.vo | 1m07.29s | 1438732 ko || +0m00.43s || 3068 ko | +0.65% | +0.21%
0m48.56s | 777524 ko | AbstractInterpretation/Fancy/Proofs.vo | 0m48.49s | 775252 ko || +0m00.07s || 2272 ko | +0.14% | +0.29%
0m46.63s | 1513204 ko | Assembly/Symbolic.vo | 0m46.50s | 1519132 ko || +0m00.13s || -5928 ko | +0.27% | -0.39%
0m38.93s | 1296004 ko | Bedrock/End2End/X25519/GarageDoorTop.vo | 0m39.27s | 1329020 ko || -0m00.34s || -33016 ko | -0.86% | -2.48%
0m38.25s | 1019348 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo | 0m39.01s | 1015424 ko || -0m00.75s || 3924 ko | -1.94% | +0.38%
0m35.36s | 1286728 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m35.45s | 1287440 ko || -0m00.09s || -712 ko | -0.25% | -0.05%
0m29.56s | 707536 ko | AbstractInterpretation/Bottomify/Proofs.vo | 0m29.20s | 702064 ko || +0m00.35s || 5472 ko | +1.23% | +0.77%
0m25.67s | 1364344 ko | PerfTesting/PerfTestSearch.vo | 0m26.34s | 1380620 ko || -0m00.66s || -16276 ko | -2.54% | -1.17%
0m23.20s | 1190664 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m23.68s | 1186712 ko || -0m00.48s || 3952 ko | -2.02% | +0.33%
0m21.28s | 1363584 ko | Bedrock/End2End/RupicolaCrypto/Low.vo | 0m22.10s | 1357416 ko || -0m00.82s || 6168 ko | -3.71% | +0.45%
0m21.12s | 819132 ko | Bedrock/Field/Translation/Proofs/Expr.vo | 0m20.23s | 813100 ko || +0m00.89s || 6032 ko | +4.39% | +0.74%
0m20.10s | 1169484 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m20.42s | 1169604 ko || -0m00.32s || -120 ko | -1.56% | -0.01%
0m19.90s | 750740 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo | 0m19.13s | 751788 ko || +0m00.76s || -1048 ko | +4.02% | -0.13%
0m18.22s | 1149556 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m18.81s | 1141612 ko || -0m00.58s || 7944 ko | -3.13% | +0.69%
0m17.80s | 1363884 ko | PerfTesting/PerfTestSearchPattern.vo | 0m18.52s | 1380264 ko || -0m00.71s || -16380 ko | -3.88% | -1.18%
0m17.13s | 1139848 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m17.76s | 1137596 ko || -0m00.63s || 2252 ko | -3.54% | +0.19%
0m17.06s | 1163884 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m17.28s | 1162092 ko || -0m00.22s || 1792 ko | -1.27% | +0.15%
0m16.91s | 1224600 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m17.54s | 1222556 ko || -0m00.62s || 2044 ko | -3.59% | +0.16%
0m14.61s | 575824 ko | PushButtonSynthesis/DettmanMultiplicationReificationCache.vo | 0m13.72s | 578380 ko || +0m00.88s || -2556 ko | +6.48% | -0.44%
0m13.94s | 603948 ko | Bedrock/Field/Common/Util.vo | 0m13.57s | 604028 ko || +0m00.36s || -80 ko | +2.72% | -0.01%
0m13.37s | 682464 ko | Bedrock/Group/AdditionChains.vo | 0m13.43s | 681756 ko || -0m00.06s || 708 ko | -0.44% | +0.10%
0m12.99s | 651956 ko | Bedrock/Group/ScalarMult/LadderStep.vo | 0m12.96s | 667512 ko || +0m00.02s || -15556 ko | +0.23% | -2.33%
0m11.85s | 1039564 ko | BoundsPipeline.vo | 0m11.63s | 1034336 ko || +0m00.21s || 5228 ko | +1.89% | +0.50%
0m11.63s | 608456 ko | Stringification/IR.vo | 0m10.69s | 605692 ko || +0m00.94s || 2764 ko | +8.79% | +0.45%
0m11.29s | 1708044 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo | 0m11.84s | 1704028 ko || -0m00.55s || 4016 ko | -4.64% | +0.23%
0m10.32s | 627304 ko | Bedrock/Field/Translation/Proofs/Flatten.vo | 0m09.70s | 625132 ko || +0m00.62s || 2172 ko | +6.39% | +0.34%
0m10.24s | 1309500 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo | 0m10.43s | 1302452 ko || -0m00.18s || 7048 ko | -1.82% | +0.54%
0m09.66s | 560724 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m09.30s | 564352 ko || +0m00.35s || -3628 ko | +3.87% | -0.64%
0m09.23s | 1042308 ko | PushButtonSynthesis/BaseConversion.vo | 0m09.35s | 1039684 ko || -0m00.11s || 2624 ko | -1.28% | +0.25%
0m09.21s | 667088 ko | Bedrock/Group/ScalarMult/CSwap.vo | 0m09.30s | 663944 ko || -0m00.08s || 3144 ko | -0.96% | +0.47%
0m08.43s | 1010664 ko | PushButtonSynthesis/SmallExamples.vo | 0m08.17s | 1006976 ko || +0m00.25s || 3688 ko | +3.18% | +0.36%
0m08.37s | 1055836 ko | PushButtonSynthesis/Primitives.vo | 0m08.44s | 1048984 ko || -0m00.07s || 6852 ko | -0.82% | +0.65%
0m08.02s | 915988 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo | 0m07.81s | 914048 ko || +0m00.20s || 1940 ko | +2.68% | +0.21%
0m07.81s | 599108 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo | 0m07.53s | 588088 ko || +0m00.27s || 11020 ko | +3.71% | +1.87%
0m06.99s | 1046728 ko | PushButtonSynthesis/SolinasReduction.vo | 0m07.35s | 1041620 ko || -0m00.35s || 5108 ko | -4.89% | +0.49%
0m06.45s | 548204 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo | 0m06.09s | 551660 ko || +0m00.36s || -3456 ko | +5.91% | -0.62%
0m06.36s | 1134228 ko | CLI.vo | 0m06.55s | 1130032 ko || -0m00.18s || 4196 ko | -2.90% | +0.37%
0m06.28s | 1053920 ko | PushButtonSynthesis/BarrettReduction.vo | 0m06.48s | 1048200 ko || -0m00.20s || 5720 ko | -3.08% | +0.54%
0m06.19s | 582548 ko | Rewriter/Passes/NoSelect.vo | 0m05.88s | 575040 ko || +0m00.31s || 7508 ko | +5.27% | +1.30%
0m06.08s | 1144788 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m06.36s | 1142048 ko || -0m00.28s || 2740 ko | -4.40% | +0.23%
0m06.08s | 545032 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m05.97s | 544184 ko || +0m00.11s || 848 ko | +1.84% | +0.15%
0m05.98s | 909120 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo | 0m05.84s | 909032 ko || +0m00.14s || 88 ko | +2.39% | +0.00%
0m05.54s | 540876 ko | Fancy/Prod.vo | 0m05.43s | 540052 ko || +0m00.11s || 824 ko | +2.02% | +0.15%
0m05.37s | 619716 ko | Bedrock/End2End/RupicolaCrypto/Broadcast.vo | 0m05.25s | 618532 ko || +0m00.12s || 1184 ko | +2.28% | +0.19%
0m05.11s | 553984 ko | Language/InversionExtra.vo | 0m04.82s | 552876 ko || +0m00.29s || 1108 ko | +6.01% | +0.20%
0m04.65s | 1044416 ko | PushButtonSynthesis/DettmanMultiplication.vo | 0m04.78s | 1038664 ko || -0m00.12s || 5752 ko | -2.71% | +0.55%
0m04.56s | 1076332 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m04.58s | 1070084 ko || -0m00.02s || 6248 ko | -0.43% | +0.58%
0m04.29s | 1051768 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m04.38s | 1044832 ko || -0m00.08s || 6936 ko | -2.05% | +0.66%
0m04.24s | 1513692 ko | Bedrock/Everything.vo | 0m04.17s | 1509600 ko || +0m00.07s || 4092 ko | +1.67% | +0.27%
0m03.89s | 1054876 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m03.95s | 1059392 ko || -0m00.06s || -4516 ko | -1.51% | -0.42%
0m03.87s | 957956 ko | Assembly/Equivalence.vo | 0m03.80s | 955500 ko || +0m00.07s || 2456 ko | +1.84% | +0.25%
0m03.72s | 1371368 ko | Everything.vo | 0m03.66s | 1367476 ko || +0m00.06s || 3892 ko | +1.63% | +0.28%
0m03.39s | 671368 ko | Bedrock/Group/ScalarMult/ScalarMult.vo | 0m03.42s | 669444 ko || -0m00.02s || 1924 ko | -0.87% | +0.28%
0m03.22s | 540716 ko | Rewriter/Passes/ArithWithRelaxedCasts.vo | 0m02.86s | 537260 ko || +0m00.36s || 3456 ko | +12.58% | +0.64%
0m03.08s | 546696 ko | PushButtonSynthesis/BaseConversionReificationCache.vo | 0m03.00s | 547388 ko || +0m00.08s || -692 ko | +2.66% | -0.12%
0m03.05s | 616084 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo | 0m03.07s | 615220 ko || -0m00.02s || 864 ko | -0.65% | +0.14%
0m03.04s | 1024028 ko | Bedrock/Field/Translation/Cmd.vo | 0m03.09s | 1014548 ko || -0m00.04s || 9480 ko | -1.61% | +0.93%
0m03.02s | 1085216 ko | Rewriter/PerfTesting/Core.vo | 0m03.10s | 1083032 ko || -0m00.08s || 2184 ko | -2.58% | +0.20%
0m02.99s | 1355228 ko | PerfTesting/PerfTestPrint.vo | 0m03.19s | 1351204 ko || -0m00.19s || 4024 ko | -6.26% | +0.29%
0m02.97s | 543912 ko | Rewriter/Passes/AddAssocLeft.vo | 0m02.69s | 537868 ko || +0m00.28s || 6044 ko | +10.40% | +1.12%
0m02.85s | 528668 ko | Rewriter/Passes/Test.vo | 0m02.60s | 519376 ko || +0m00.25s || 9292 ko | +9.61% | +1.78%
0m02.83s | 1078936 ko | Bedrock/Field/Stringification/Stringification.vo | 0m02.95s | 1074420 ko || -0m00.12s || 4516 ko | -4.06% | +0.42%
0m02.78s | 1015124 ko | Bedrock/Field/Translation/Func.vo | 0m02.85s | 1010968 ko || -0m00.07s || 4156 ko | -2.45% | +0.41%
0m02.75s | 1155412 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m02.78s | 1151352 ko || -0m00.02s || 4060 ko | -1.07% | +0.35%
0m02.73s | 550964 ko | Bedrock/Field/Translation/Expr.vo | 0m02.46s | 547204 ko || +0m00.27s || 3760 ko | +10.97% | +0.68%
0m02.70s | 1141332 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.89s | 1137240 ko || -0m00.18s || 4092 ko | -6.57% | +0.35%
0m02.70s | 1128612 ko | StandaloneHaskellMain.vo | 0m02.73s | 1124468 ko || -0m00.02s || 4144 ko | -1.09% | +0.36%
0m02.68s | 1103360 ko | StandaloneOCamlMain.vo | 0m02.76s | 1126632 ko || -0m00.07s || -23272 ko | -2.89% | -2.06%
0m02.66s | 1155528 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m02.75s | 1151392 ko || -0m00.08s || 4136 ko | -3.27% | +0.35%
0m02.65s | 538272 ko | Rewriter/Passes/FlattenThunkedRects.vo | 0m02.30s | 539232 ko || +0m00.35s || -960 ko | +15.21% | -0.17%
0m02.64s | 1070016 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m02.79s | 1068048 ko || -0m00.14s || 1968 ko | -5.37% | +0.18%
0m02.56s | 626724 ko | Bedrock/Field/Interface/Compilation2.vo | 0m02.57s | 624252 ko || -0m00.00s || 2472 ko | -0.38% | +0.39%
0m02.52s | 1075116 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m02.75s | 1070284 ko || -0m00.23s || 4832 ko | -8.36% | +0.45%
0m02.48s | 1052724 ko | Bedrock/Field/Translation/Parameters/FE310.vo | 0m02.58s | 1050740 ko || -0m00.10s || 1984 ko | -3.87% | +0.18%
0m02.46s | 1054036 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m02.52s | 1050836 ko || -0m00.06s || 3200 ko | -2.38% | +0.30%
0m02.43s | 1051584 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m02.49s | 1047564 ko || -0m00.06s || 4020 ko | -2.40% | +0.38%
0m02.41s | 1054648 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m02.56s | 1050792 ko || -0m00.14s || 3856 ko | -5.85% | +0.36%
0m02.20s | 542064 ko | Rewriter/Passes/StripLiteralCasts.vo | 0m01.75s | 537888 ko || +0m00.45s || 4176 ko | +25.71% | +0.77%
0m02.20s | 548260 ko | Stringification/Language.vo | 0m01.98s | 545108 ko || +0m00.22s || 3152 ko | +11.11% | +0.57%
0m02.14s | 542796 ko | Rewriter/Passes/UnfoldValueBarrier.vo | 0m01.80s | 536716 ko || +0m00.34s || 6080 ko | +18.88% | +1.13%
0m02.10s | 621412 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo | 0m02.12s | 616400 ko || -0m00.02s || 5012 ko | -0.94% | +0.81%
0m01.96s | 542816 ko | Rewriter/Passes/ToFancy.vo | 0m01.60s | 535480 ko || +0m00.35s || 7336 ko | +22.49% | +1.36%
0m01.86s | 515192 ko | AbstractInterpretation/Fancy/AbstractInterpretation.vo | 0m01.61s | 513448 ko || +0m00.25s || 1744 ko | +15.52% | +0.33%
0m01.74s | 640408 ko | Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo | 0m01.78s | 639184 ko || -0m00.04s || 1224 ko | -2.24% | +0.19%
0m01.69s | 519248 ko | AbstractInterpretation/Bottomify/AbstractInterpretation.vo | 0m01.53s | 511940 ko || +0m00.15s || 7308 ko | +10.45% | +1.42%
0m01.65s | 612764 ko | Bedrock/Field/Common/Names/MakeNames.vo | 0m01.62s | 612900 ko || +0m00.02s || -136 ko | +1.85% | -0.02%
0m01.64s | 527992 ko | AbstractInterpretation/ZRange.vo | 0m01.50s | 522552 ko || +0m00.13s || 5440 ko | +9.33% | +1.04%
0m01.56s | 597148 ko | CompilersTestCases.vo | 0m01.51s | 593760 ko || +0m00.05s || 3388 ko | +3.31% | +0.57%
0m01.40s | 545956 ko | Stringification/Go.vo | 0m01.38s | 545232 ko || +0m00.02s || 724 ko | +1.44% | +0.13%
0m01.33s | 528596 ko | AbstractInterpretation/Proofs.vo | 0m01.31s | 528596 ko || +0m00.02s || 0 ko | +1.52% | +0.00%
0m01.19s | 634224 ko | Bedrock/Specs/Field.vo | 0m01.24s | 633592 ko || -0m00.05s || 632 ko | -4.03% | +0.09%
0m01.08s | 606020 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo | 0m00.99s | 603968 ko || +0m00.09s || 2052 ko | +9.09% | +0.33%
0m01.07s | 611500 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo | 0m01.08s | 613420 ko || -0m00.01s || -1920 ko | -0.92% | -0.31%
0m01.00s | 545716 ko | Stringification/C.vo | 0m00.86s | 541544 ko || +0m00.14s || 4172 ko | +16.27% | +0.77%
0m00.99s | 539992 ko | Stringification/JSON.vo | 0m00.89s | 539204 ko || +0m00.09s || 788 ko | +11.23% | +0.14%
0m00.97s | 540996 ko | Bedrock/Field/Translation/LoadStoreList.vo | 0m00.91s | 539648 ko || +0m00.05s || 1348 ko | +6.59% | +0.24%
0m00.90s | 541904 ko | Stringification/Zig.vo | 0m00.83s | 539880 ko || +0m00.07s || 2024 ko | +8.43% | +0.37%
0m00.89s | 537956 ko | Stringification/Rust.vo | 0m00.80s | 537880 ko || +0m00.08s || 76 ko | +11.24% | +0.01%
0m00.88s | 539836 ko | Bedrock/Field/Translation/Proofs/Equivalence.vo | 0m00.86s | 539792 ko || +0m00.02s || 44 ko | +2.32% | +0.00%
0m00.87s | 617604 ko | Bedrock/Field/Interface/Representation.vo | 0m00.88s | 616092 ko || -0m00.01s || 1512 ko | -1.13% | +0.24%
0m00.86s | 623164 ko | Bedrock/Group/Point.vo | 0m00.84s | 620064 ko || +0m00.02s || 3100 ko | +2.38% | +0.49%
0m00.85s | 539220 ko | Stringification/Java.vo | 0m00.80s | 537952 ko || +0m00.04s || 1268 ko | +6.24% | +0.23%
0m00.82s | 537040 ko | Bedrock/Field/Common/Types.vo | 0m00.80s | 538432 ko || +0m00.01s || -1392 ko | +2.49% | -0.25%
0m00.81s | 592996 ko | Bedrock/Field/Common/Tactics.vo | 0m00.73s | 590956 ko || +0m00.08s || 2040 ko | +10.95% | +0.34%
0m00.76s | 525612 ko | Bedrock/Field/Common/Arrays/MakeListLengths.vo | 0m00.70s | 523724 ko || +0m00.06s || 1888 ko | +8.57% | +0.36%
0m00.75s | 552108 ko | Bedrock/Field/Stringification/FlattenVarData.vo | 0m00.66s | 548104 ko || +0m00.08s || 4004 ko | +13.63% | +0.73%
0m00.75s | 506512 ko | Language/APINotations.vo | 0m00.70s | 505660 ko || +0m00.05s || 852 ko | +7.14% | +0.16%
0m00.74s | 538784 ko | Bedrock/Field/Translation/Flatten.vo | 0m00.67s | 536724 ko || +0m00.06s || 2060 ko | +10.44% | +0.38%
0m00.72s | 543720 ko | Bedrock/Field/Stringification/LoadStoreListVarData.vo | 0m00.71s | 541640 ko || +0m00.01s || 2080 ko | +1.40% | +0.38%
0m00.71s | 537548 ko | Bedrock/Field/Translation/Proofs/VarnameSet.vo | 0m00.68s | 537560 ko || +0m00.02s || -12 ko | +4.41% | -0.00%
0m00.70s | 519324 ko | AbstractInterpretation/Wf.vo | 0m00.66s | 518048 ko || +0m00.03s || 1276 ko | +6.06% | +0.24%
0m00.69s | 516912 ko | AbstractInterpretation/Fancy/WfExtra.vo | 0m00.66s | 515532 ko || +0m00.02s || 1380 ko | +4.54% | +0.26%
0m00.68s | 556520 ko | Rewriter/All.vo | 0m00.65s | 550540 ko || +0m00.03s || 5980 ko | +4.61% | +1.08%
0m00.66s | 504404 ko | AbstractInterpretation/AbstractInterpretation.vo | 0m00.63s | 503808 ko || +0m00.03s || 596 ko | +4.76% | +0.11%
0m00.66s | 516844 ko | AbstractInterpretation/Bottomify/WfExtra.vo | 0m00.67s | 515484 ko || -0m00.01s || 1360 ko | -1.49% | +0.26%
0m00.66s | 505260 ko | MiscCompilerPassesProofsExtra.vo | 0m00.69s | 505296 ko || -0m00.02s || -36 ko | -4.34% | -0.00%
0m00.65s | 503072 ko | Language/WfExtra.vo | 0m00.64s | 502932 ko || +0m00.01s || 140 ko | +1.56% | +0.02%
0m00.65s | 513968 ko | PushButtonSynthesis/ReificationCache.vo | 0m00.62s | 512044 ko || +0m00.03s || 1924 ko | +4.83% | +0.37%
0m00.64s | 521332 ko | AbstractInterpretation/WfExtra.vo | 0m00.68s | 518696 ko || -0m00.04s || 2636 ko | -5.88% | +0.50%
0m00.64s | 504440 ko | Language/UnderLetsProofsExtra.vo | 0m00.63s | 503120 ko || +0m00.01s || 1320 ko | +1.58% | +0.26%
0m00.62s | 513292 ko | Language/API.vo | 0m00.63s | 513116 ko || -0m00.01s || 176 ko | -1.58% | +0.03%
0m00.60s | 506788 ko | Rewriter/AllTacticsExtra.vo | 0m00.56s | 503132 ko || +0m00.03s || 3656 ko | +7.14% | +0.72%
0m00.32s | 418188 ko | Language/IdentifierParameters.vo | 0m00.33s | 413864 ko || -0m00.01s || 4324 ko | -3.03% | +1.04%
```
</p>
</details>
<details><summary>Timing Diff</summary>
<p>
```
After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem)
-------------------------------------------------------------------------------------------------------------------------------------------------------------------
38m49.72s | 2852140 ko | Total Time / Peak Mem | 46m18.15s | 2852004 ko || -7m28.43s || 136 ko | -16.14% | +0.00%
-------------------------------------------------------------------------------------------------------------------------------------------------------------------
1m01.16s | 970108 ko | AbstractInterpretation/ZRangeProofs.vo | 8m27.89s | 1924896 ko || -7m26.73s || -954788 ko | -87.95% | -49.60%
3m59.87s | 2549792 ko | Assembly/WithBedrock/Proofs.vo | 3m58.18s | 2549652 ko || +0m01.68s || 140 ko | +0.70% | +0.00%
1m51.19s | 2299312 ko | Fancy/Barrett256.vo | 1m52.37s | 2288172 ko || -0m01.18s || 11140 ko | -1.05% | +0.48%
0m49.17s | 1844880 ko | Fancy/Montgomery256.vo | 0m50.51s | 1841780 ko || -0m01.33s || 3100 ko | -2.65% | +0.16%
8m27.11s | 2587840 ko | Bedrock/End2End/X25519/GarageDoor.vo | 8m27.35s | 2594716 ko || -0m00.24s || -6876 ko | -0.04% | -0.26%
5m26.94s | 2852140 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo | 5m26.97s | 2852004 ko || -0m00.03s || 136 ko | -0.00% | +0.00%
1m51.50s | 1607724 ko | Bedrock/End2End/X25519/Field25519.vo | 1m51.33s | 1609940 ko || +0m00.17s || -2216 ko | +0.15% | -0.13%
1m46.95s | 1894264 ko | Bedrock/End2End/X25519/AddPrecomputed.vo | 1m46.65s | 1895588 ko || +0m00.29s || -1324 ko | +0.28% | -0.06%
1m33.18s | 2190992 ko | SlowPrimeSynthesisExamples.vo | 1m33.40s | 2188784 ko || -0m00.21s || 2208 ko | -0.23% | +0.10%
1m25.68s | 1684352 ko | Assembly/EquivalenceProofs.vo | 1m25.73s | 1682328 ko || -0m00.04s || 2024 ko | -0.05% | +0.12%
1m08.02s | 1436136 ko | Assembly/WithBedrock/SymbolicProofs.vo | 1m08.45s | 1441924 ko || -0m00.43s || -5788 ko | -0.62% | -0.40%
0m47.13s | 779276 ko | AbstractInterpretation/Fancy/Proofs.vo | 0m47.29s | 778260 ko || -0m00.15s || 1016 ko | -0.33% | +0.13%
0m45.50s | 1513088 ko | Assembly/Symbolic.vo | 0m45.25s | 1516408 ko || +0m00.25s || -3320 ko | +0.55% | -0.21%
0m37.47s | 1292460 ko | Bedrock/End2End/X25519/GarageDoorTop.vo | 0m37.53s | 1292424 ko || -0m00.06s || 36 ko | -0.15% | +0.00%
0m34.59s | 1286768 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m34.59s | 1291524 ko || +0m00.00s || -4756 ko | +0.00% | -0.36%
0m32.33s | 1558900 ko | StandaloneDebuggingExamples.vo | 0m32.32s | 1559080 ko || +0m00.00s || -180 ko | +0.03% | -0.01%
0m28.84s | 708060 ko | AbstractInterpretation/Bottomify/Proofs.vo | 0m28.93s | 708216 ko || -0m00.08s || -156 ko | -0.31% | -0.02%
0m25.80s | 1362152 ko | PerfTesting/PerfTestSearch.vo | 0m25.75s | 1363608 ko || +0m00.05s || -1456 ko | +0.19% | -0.10%
0m23.68s | 1190740 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m23.70s | 1190668 ko || -0m00.01s || 72 ko | -0.08% | +0.00%
0m22.25s | 1363668 ko | Bedrock/End2End/RupicolaCrypto/Low.vo | 0m22.16s | 1363652 ko || +0m00.08s || 16 ko | +0.40% | +0.00%
0m20.66s | 1170596 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m20.65s | 1169612 ko || +0m00.01s || 984 ko | +0.04% | +0.08%
0m18.51s | 1149660 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m18.53s | 1152312 ko || -0m00.01s || -2652 ko | -0.10% | -0.23%
0m17.99s | 1363616 ko | PerfTesting/PerfTestSearchPattern.vo | 0m17.92s | 1363820 ko || +0m00.06s || -204 ko | +0.39% | -0.01%
0m17.62s | 1224592 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m17.94s | 1224468 ko || -0m00.32s || 124 ko | -1.78% | +0.01%
0m17.61s | 1139740 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m17.78s | 1139848 ko || -0m00.17s || -108 ko | -0.95% | -0.00%
0m17.41s | 1165228 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m17.41s | 1163888 ko || +0m00.00s || 1340 ko | +0.00% | +0.11%
0m11.93s | 1708212 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo | 0m11.91s | 1713748 ko || +0m00.01s || -5536 ko | +0.16% | -0.32%
0m11.45s | 1039396 ko | BoundsPipeline.vo | 0m11.41s | 1039604 ko || +0m00.03s || -208 ko | +0.35% | -0.02%
0m10.25s | 1306464 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo | 0m10.16s | 1306496 ko || +0m00.08s || -32 ko | +0.88% | -0.00%
0m09.44s | 1042380 ko | PushButtonSynthesis/BaseConversion.vo | 0m09.38s | 1042428 ko || +0m00.05s || -48 ko | +0.63% | -0.00%
0m08.57s | 1010972 ko | PushButtonSynthesis/SmallExamples.vo | 0m08.66s | 1011000 ko || -0m00.08s || -28 ko | -1.03% | -0.00%
0m08.41s | 1054296 ko | PushButtonSynthesis/Primitives.vo | 0m08.51s | 1054412 ko || -0m00.09s || -116 ko | -1.17% | -0.01%
0m07.29s | 1045396 ko | PushButtonSynthesis/SolinasReduction.vo | 0m07.32s | 1046564 ko || -0m00.03s || -1168 ko | -0.40% | -0.11%
0m06.46s | 1138216 ko | CLI.vo | 0m06.50s | 1138192 ko || -0m00.04s || 24 ko | -0.61% | +0.00%
0m06.38s | 1053884 ko | PushButtonSynthesis/BarrettReduction.vo | 0m06.41s | 1055024 ko || -0m00.03s || -1140 ko | -0.46% | -0.10%
0m06.37s | 1144708 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m06.41s | 1144588 ko || -0m00.04s || 120 ko | -0.62% | +0.01%
0m04.74s | 1043692 ko | PushButtonSynthesis/DettmanMultiplication.vo | 0m04.73s | 1044428 ko || +0m00.00s || -736 ko | +0.21% | -0.07%
0m04.67s | 1076308 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m04.68s | 1077472 ko || -0m00.00s || -1164 ko | -0.21% | -0.10%
0m04.41s | 1048588 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m04.39s | 1048700 ko || +0m00.02s || -112 ko | +0.45% | -0.01%
0m04.01s | 1514004 ko | Bedrock/Everything.vo | 0m04.02s | 1513892 ko || -0m00.00s || 112 ko | -0.24% | +0.00%
0m03.93s | 1053880 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m03.93s | 1054916 ko || +0m00.00s || -1036 ko | +0.00% | -0.09%
0m03.76s | 957948 ko | Assembly/Equivalence.vo | 0m03.84s | 957944 ko || -0m00.08s || 4 ko | -2.08% | +0.00%
0m03.55s | 1371536 ko | Everything.vo | 0m03.53s | 1371356 ko || +0m00.02s || 180 ko | +0.56% | +0.01%
0m03.13s | 1085180 ko | Rewriter/PerfTesting/Core.vo | 0m03.08s | 1084968 ko || +0m00.04s || 212 ko | +1.62% | +0.01%
0m03.11s | 1020792 ko | Bedrock/Field/Translation/Cmd.vo | 0m03.15s | 1020912 ko || -0m00.04s || -120 ko | -1.26% | -0.01%
0m03.03s | 1355188 ko | PerfTesting/PerfTestPrint.vo | 0m02.99s | 1355440 ko || +0m00.03s || -252 ko | +1.33% | -0.01%
0m02.93s | 1078716 ko | Bedrock/Field/Stringification/Stringification.vo | 0m02.91s | 1078860 ko || +0m00.02s || -144 ko | +0.68% | -0.01%
0m02.84s | 1015124 ko | Bedrock/Field/Translation/Func.vo | 0m02.80s | 1014456 ko || +0m00.04s || 668 ko | +1.42% | +0.06%
0m02.84s | 1069980 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m02.88s | 1071444 ko || -0m00.04s || -1464 ko | -1.38% | -0.13%
0m02.84s | 1141364 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.84s | 1141408 ko || +0m00.00s || -44 ko | +0.00% | -0.00%
0m02.84s | 1103528 ko | StandaloneOCamlMain.vo | 0m02.80s | 1103560 ko || +0m00.04s || -32 ko | +1.42% | -0.00%
0m02.81s | 1155224 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m02.81s | 1155500 ko || +0m00.00s || -276 ko | +0.00% | -0.02%
0m02.79s | 1074396 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m02.74s | 1075284 ko || +0m00.04s || -888 ko | +1.82% | -0.08%
0m02.78s | 1155352 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m02.72s | 1155508 ko || +0m00.05s || -156 ko | +2.20% | -0.01%
0m02.77s | 1128796 ko | StandaloneHaskellMain.vo | 0m02.72s | 1128716 ko || +0m00.04s || 80 ko | +1.83% | +0.00%
0m02.51s | 1054848 ko | Bedrock/Field/Translation/Parameters/FE310.vo | 0m02.53s | 1052604 ko || -0m00.02s || 2244 ko | -0.79% | +0.21%
0m02.49s | 1054620 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m02.56s | 1054768 ko || -0m00.06s || -148 ko | -2.73% | -0.01%
0m02.48s | 1051804 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m02.49s | 1050928 ko || -0m00.01s || 876 ko | -0.40% | +0.08%
0m02.48s | 1054180 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m02.51s | 1054080 ko || -0m00.02s || 100 ko | -1.19% | +0.00%
0m01.27s | 530000 ko | AbstractInterpretation/Proofs.vo | 0m01.26s | 530032 ko || +0m00.01s || -32 ko | +0.79% | -0.00%
```
</p>
</details>
JasonGross
force-pushed
the
saturated-solinas-idents-more
branch
from
d1f3730
to
02afb84
Compare
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.
For #1609
Still working on proofs of remaining idents for which
type.is_not_higher_order_than 3 t = false.