Add more identifiers for saturated solinas #1773
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
branch
3 times, most recently
from
4972127
to
9d120d3
Compare
JasonGross
force-pushed
the
saturated-solinas-idents
branch
2 times, most recently
from
d73f0b7
to
d8ae2a5
Compare
JasonGross
force-pushed
the
saturated-solinas-idents
branch
6 times, most recently
from
a219b11
to
a8df66a
Compare
For mit-plv#1609 Slow identifiers are commented out. I'll have to figure out a different way to prove the ZRange bounds proof that isn't so slow. Co-authored-by: Andres Erbsen <andres-github@andres.systems> <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 65m48.78s | 2852620 ko | Total Time / Peak Mem | 67m03.79s | 2852280 ko || -1m15.01s || 340 ko | -1.86% | +0.01% -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 8m28.52s | 2657300 ko | Bedrock/End2End/X25519/GarageDoor.vo | 8m49.71s | 2656156 ko || -0m21.19s || 1144 ko | -4.00% | +0.04% 2m27.88s | 1666316 ko | Rewriter/Passes/NBE.vo | 2m15.45s | 1554568 ko || +0m12.43s || 111748 ko | +9.17% | +7.18% 1m42.99s | 1885360 ko | Bedrock/End2End/X25519/AddPrecomputed.vo | 1m55.09s | 1888072 ko || -0m12.09s || -2712 ko | -10.51% | -0.14% 3m02.83s | 2603460 ko | Bedrock/End2End/RupicolaCrypto/ChaCha20.vo | 3m13.15s | 2603344 ko || -0m10.31s || 116 ko | -5.34% | +0.00% 5m25.01s | 2852620 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo | 5m33.56s | 2852280 ko || -0m08.55s || 340 ko | -2.56% | +0.01% 0m11.49s | 542800 ko | AbstractInterpretation/ZRangeCommonProofs.vo | 0m04.40s | 537448 ko || +0m07.08s || 5352 ko | +161.13% | +0.99% 3m31.55s | 1773972 ko | Rewriter/Passes/ArithWithCasts.vo | 3m36.07s | 1682328 ko || -0m04.51s || 91644 ko | -2.09% | +5.44% 0m48.69s | 1127200 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo | 0m44.14s | 1100028 ko || +0m04.54s || 27172 ko | +10.30% | +2.47% 1m50.06s | 1603060 ko | Bedrock/End2End/X25519/Field25519.vo | 1m53.33s | 1600868 ko || -0m03.26s || 2192 ko | -2.88% | +0.13% 0m36.82s | 712856 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m40.41s | 710156 ko || -0m03.58s || 2700 ko | -8.88% | +0.38% 2m26.61s | 1119660 ko | Fancy/Compiler.vo | 2m29.14s | 1127580 ko || -0m02.52s || -7920 ko | -1.69% | -0.70% 1m47.35s | 1418720 ko | Rewriter/Passes/ToFancyWithCasts.vo | 1m49.39s | 1437288 ko || -0m02.04s || -18568 ko | -1.86% | -1.29% 1m46.98s | 2428052 ko | Fancy/Barrett256.vo | 1m49.19s | 2411004 ko || -0m02.21s || 17048 ko | -2.02% | +0.70% 1m22.34s | 945488 ko | AbstractInterpretation/Fancy/Wf.vo | 1m24.45s | 901548 ko || -0m02.10s || 43940 ko | -2.49% | +4.87% 0m29.23s | 1554548 ko | StandaloneDebuggingExamples.vo | 0m31.54s | 1544348 ko || -0m02.30s || 10200 ko | -7.32% | +0.66% 0m59.32s | 876092 ko | AbstractInterpretation/Bottomify/Wf.vo | 1m00.44s | 882844 ko || -0m01.11s || -6752 ko | -1.85% | -0.76% 0m58.11s | 710572 ko | Rewriter/RulesProofs.vo | 0m59.51s | 710680 ko || -0m01.39s || -108 ko | -2.35% | -0.01% 0m46.54s | 773492 ko | AbstractInterpretation/Fancy/Proofs.vo | 0m47.54s | 771488 ko || -0m01.00s || 2004 ko | -2.10% | +0.25% 0m39.38s | 1072512 ko | Rewriter/Passes/Arith.vo | 0m40.40s | 1087364 ko || -0m01.01s || -14852 ko | -2.52% | -1.36% 0m37.80s | 1016072 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo | 0m39.02s | 1016376 ko || -0m01.22s || -304 ko | -3.12% | -0.02% 0m33.76s | 1284448 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m35.26s | 1286640 ko || -0m01.50s || -2192 ko | -4.25% | -0.17% 0m21.18s | 1357384 ko | Bedrock/End2End/RupicolaCrypto/Low.vo | 0m22.28s | 1355956 ko || -0m01.10s || 1428 ko | -4.93% | +0.10% 0m17.74s | 1142436 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m19.06s | 1133464 ko || -0m01.32s || 8972 ko | -6.92% | +0.79% 0m17.34s | 1379920 ko | PerfTesting/PerfTestSearchPattern.vo | 0m18.52s | 1378460 ko || -0m01.17s || 1460 ko | -6.37% | +0.10% 0m16.93s | 792296 ko | Language/IdentifiersGENERATED.vo | 0m15.81s | 765508 ko || +0m01.11s || 26788 ko | +7.08% | +3.49% 3m55.44s | 2545572 ko | Assembly/WithBedrock/Proofs.vo | 3m54.51s | 2541224 ko || +0m00.93s || 4348 ko | +0.39% | +0.17% 1m27.57s | 2144112 ko | SlowPrimeSynthesisExamples.vo | 1m26.76s | 2088940 ko || +0m00.80s || 55172 ko | +0.93% | +2.64% 1m15.72s | 1526800 ko | Assembly/EquivalenceProofs.vo | 1m16.33s | 1522940 ko || -0m00.60s || 3860 ko | -0.79% | +0.25% 1m15.72s | 990208 ko | PushButtonSynthesis/SolinasReductionReificationCache.vo | 1m16.02s | 1010076 ko || -0m00.29s || -19868 ko | -0.39% | -1.96% 1m06.04s | 1437348 ko | Assembly/WithBedrock/SymbolicProofs.vo | 1m06.56s | 1433052 ko || -0m00.51s || 4296 ko | -0.78% | +0.29% 0m55.24s | 866644 ko | AbstractInterpretation/ZRangeProofs.vo | 0m54.79s | 864800 ko || +0m00.45s || 1844 ko | +0.82% | +0.21% 0m50.66s | 836408 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 0m51.33s | 831040 ko || -0m00.67s || 5368 ko | -1.30% | +0.64% 0m49.88s | 1029676 ko | Rewriter/Passes/MultiRetSplit.vo | 0m49.97s | 1027180 ko || -0m00.08s || 2496 ko | -0.18% | +0.24% 0m46.64s | 1780880 ko | Fancy/Montgomery256.vo | 0m47.17s | 1839968 ko || -0m00.53s || -59088 ko | -1.12% | -3.21% 0m45.28s | 1517332 ko | Assembly/Symbolic.vo | 0m45.54s | 1519112 ko || -0m00.25s || -1780 ko | -0.57% | -0.11% 0m38.05s | 1327100 ko | Bedrock/End2End/X25519/GarageDoorTop.vo | 0m38.96s | 1322972 ko || -0m00.91s || 4128 ko | -2.33% | +0.31% 0m32.34s | 913332 ko | Rewriter/Passes/MulSplit.vo | 0m32.16s | 879740 ko || +0m00.18s || 33592 ko | +0.55% | +3.81% 0m28.26s | 702272 ko | AbstractInterpretation/Bottomify/Proofs.vo | 0m28.53s | 707212 ko || -0m00.26s || -4940 ko | -0.94% | -0.69% 0m25.06s | 1380588 ko | PerfTesting/PerfTestSearch.vo | 0m26.01s | 1380864 ko || -0m00.95s || -276 ko | -3.65% | -0.01% 0m22.67s | 1186572 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m22.89s | 1182588 ko || -0m00.21s || 3984 ko | -0.96% | +0.33% 0m19.99s | 813092 ko | Bedrock/Field/Translation/Proofs/Expr.vo | 0m19.87s | 794980 ko || +0m00.11s || 18112 ko | +0.60% | +2.27% 0m19.55s | 1168644 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m19.73s | 1164252 ko || -0m00.17s || 4392 ko | -0.91% | +0.37% 0m18.91s | 748880 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo | 0m19.52s | 739932 ko || -0m00.60s || 8948 ko | -3.12% | +1.20% 0m16.82s | 1222464 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m17.65s | 1218392 ko || -0m00.82s || 4072 ko | -4.70% | +0.33% 0m16.73s | 1137776 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m17.62s | 1133672 ko || -0m00.89s || 4104 ko | -5.05% | +0.36% 0m16.26s | 1161904 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m16.39s | 1153720 ko || -0m00.12s || 8184 ko | -0.79% | +0.70% 0m14.51s | 603548 ko | Language/IdentifiersGENERATEDProofs.vo | 0m13.92s | 598200 ko || +0m00.58s || 5348 ko | +4.23% | +0.89% 0m13.35s | 604016 ko | Bedrock/Field/Common/Util.vo | 0m13.39s | 603924 ko || -0m00.04s || 92 ko | -0.29% | +0.01% 0m13.05s | 682576 ko | Bedrock/Group/AdditionChains.vo | 0m13.57s | 680296 ko || -0m00.51s || 2280 ko | -3.83% | +0.33% 0m12.72s | 667548 ko | Bedrock/Group/ScalarMult/LadderStep.vo | 0m13.15s | 653356 ko || -0m00.42s || 14192 ko | -3.26% | +2.17% 0m12.63s | 576512 ko | PushButtonSynthesis/DettmanMultiplicationReificationCache.vo | 0m13.46s | 579232 ko || -0m00.83s || -2720 ko | -6.16% | -0.46% 0m11.38s | 1034268 ko | BoundsPipeline.vo | 0m11.49s | 1034352 ko || -0m00.10s || -84 ko | -0.95% | -0.00% 0m11.30s | 1705800 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo | 0m11.77s | 1703840 ko || -0m00.46s || 1960 ko | -3.99% | +0.11% 0m10.29s | 602260 ko | Stringification/IR.vo | 0m09.58s | 598276 ko || +0m00.70s || 3984 ko | +7.41% | +0.66% 0m10.02s | 627072 ko | Bedrock/Field/Translation/Proofs/Flatten.vo | 0m09.47s | 625248 ko || +0m00.54s || 1824 ko | +5.80% | +0.29% 0m09.97s | 1303428 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo | 0m10.50s | 1301292 ko || -0m00.52s || 2136 ko | -5.04% | +0.16% 0m08.98s | 1040220 ko | PushButtonSynthesis/BaseConversion.vo | 0m09.14s | 1038228 ko || -0m00.16s || 1992 ko | -1.75% | +0.19% 0m08.89s | 664948 ko | Bedrock/Group/ScalarMult/CSwap.vo | 0m09.35s | 663156 ko || -0m00.45s || 1792 ko | -4.91% | +0.27% 0m08.80s | 610724 ko | Language/IdentifiersBasicGENERATED.vo | 0m08.35s | 600648 ko || +0m00.45s || 10076 ko | +5.38% | +1.67% 0m08.55s | 563324 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m09.11s | 559056 ko || -0m00.55s || 4268 ko | -6.14% | +0.76% 0m08.19s | 583492 ko | PushButtonSynthesis/BYInversionReificationCache.vo | 0m08.78s | 586752 ko || -0m00.58s || -3260 ko | -6.71% | -0.55% 0m08.04s | 1048948 ko | PushButtonSynthesis/Primitives.vo | 0m08.03s | 1046980 ko || +0m00.00s || 1968 ko | +0.12% | +0.18% 0m07.82s | 1006888 ko | PushButtonSynthesis/SmallExamples.vo | 0m07.83s | 1005592 ko || -0m00.00s || 1296 ko | -0.12% | +0.12% 0m07.51s | 913956 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo | 0m07.32s | 911976 ko || +0m00.18s || 1980 ko | +2.59% | +0.21% 0m07.40s | 585988 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo | 0m07.36s | 587760 ko || +0m00.04s || -1772 ko | +0.54% | -0.30% 0m06.92s | 1038440 ko | PushButtonSynthesis/SolinasReduction.vo | 0m06.91s | 1038112 ko || +0m00.00s || 328 ko | +0.14% | +0.03% 0m06.20s | 1129984 ko | CLI.vo | 0m06.05s | 1130104 ko || +0m00.15s || -120 ko | +2.47% | -0.01% 0m06.13s | 1048216 ko | PushButtonSynthesis/BarrettReduction.vo | 0m06.05s | 1045296 ko || +0m00.08s || 2920 ko | +1.32% | +0.27% 0m05.99s | 1142012 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m06.30s | 1140152 ko || -0m00.30s || 1860 ko | -4.92% | +0.16% 0m05.77s | 543492 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m05.72s | 544060 ko || +0m00.04s || -568 ko | +0.87% | -0.10% 0m05.77s | 573064 ko | Rewriter/Passes/NoSelect.vo | 0m05.75s | 574592 ko || +0m00.01s || -1528 ko | +0.34% | -0.26% 0m05.54s | 909144 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo | 0m05.65s | 908360 ko || -0m00.11s || 784 ko | -1.94% | +0.08% 0m05.49s | 551392 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo | 0m06.26s | 549176 ko || -0m00.76s || 2216 ko | -12.30% | +0.40% 0m05.34s | 538884 ko | Fancy/Prod.vo | 0m05.41s | 538800 ko || -0m00.07s || 84 ko | -1.29% | +0.01% 0m05.15s | 618708 ko | Bedrock/End2End/RupicolaCrypto/Broadcast.vo | 0m05.10s | 617832 ko || +0m00.05s || 876 ko | +0.98% | +0.14% 0m04.92s | 552816 ko | Language/InversionExtra.vo | 0m04.68s | 551468 ko || +0m00.24s || 1348 ko | +5.12% | +0.24% 0m04.49s | 1037344 ko | PushButtonSynthesis/DettmanMultiplication.vo | 0m04.60s | 1037096 ko || -0m00.10s || 248 ko | -2.39% | +0.02% 0m04.34s | 1071460 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m04.51s | 1070156 ko || -0m00.16s || 1304 ko | -3.76% | +0.12% 0m04.12s | 1043552 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m04.21s | 1042528 ko || -0m00.08s || 1024 ko | -2.13% | +0.09% 0m04.04s | 1509780 ko | Bedrock/Everything.vo | 0m04.30s | 1507700 ko || -0m00.25s || 2080 ko | -6.04% | +0.13% 0m03.88s | 955608 ko | Assembly/Equivalence.vo | 0m03.85s | 955484 ko || +0m00.02s || 124 ko | +0.77% | +0.01% 0m03.77s | 1058376 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m03.68s | 1056232 ko || +0m00.08s || 2144 ko | +2.44% | +0.20% 0m03.46s | 1367392 ko | Everything.vo | 0m03.83s | 1357220 ko || -0m00.37s || 10172 ko | -9.66% | +0.74% 0m03.42s | 462772 ko | CastLemmas.vo | 0m03.52s | 460708 ko || -0m00.10s || 2064 ko | -2.84% | +0.44% 0m02.95s | 619192 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo | 0m03.21s | 615928 ko || -0m00.25s || 3264 ko | -8.09% | +0.52% 0m02.93s | 547416 ko | PushButtonSynthesis/BaseConversionReificationCache.vo | 0m03.08s | 545340 ko || -0m00.14s || 2076 ko | -4.87% | +0.38% 0m02.86s | 1013968 ko | Bedrock/Field/Translation/Cmd.vo | 0m02.90s | 1011888 ko || -0m00.04s || 2080 ko | -1.37% | +0.20% 0m02.84s | 1351068 ko | PerfTesting/PerfTestPrint.vo | 0m03.07s | 1351172 ko || -0m00.23s || -104 ko | -7.49% | -0.00% 0m02.77s | 538024 ko | Rewriter/Passes/ArithWithRelaxedCasts.vo | 0m02.84s | 535952 ko || -0m00.06s || 2072 ko | -2.46% | +0.38% 0m02.73s | 1074352 ko | Bedrock/Field/Stringification/Stringification.vo | 0m02.91s | 1073232 ko || -0m00.18s || 1120 ko | -6.18% | +0.10% 0m02.69s | 1080972 ko | Rewriter/PerfTesting/Core.vo | 0m02.90s | 1080988 ko || -0m00.20s || -16 ko | -7.24% | -0.00% 0m02.68s | 669512 ko | Bedrock/Group/ScalarMult/ScalarMult.vo | 0m03.67s | 672696 ko || -0m00.98s || -3184 ko | -26.97% | -0.47% 0m02.67s | 1124652 ko | StandaloneHaskellMain.vo | 0m02.85s | 1128712 ko || -0m00.18s || -4060 ko | -6.31% | -0.35% 0m02.66s | 519056 ko | Rewriter/Passes/Test.vo | 0m02.64s | 519224 ko || +0m00.02s || -168 ko | +0.75% | -0.03% 0m02.65s | 1010364 ko | Bedrock/Field/Translation/Func.vo | 0m02.78s | 1009000 ko || -0m00.12s || 1364 ko | -4.67% | +0.13% 0m02.65s | 1137252 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.82s | 1135256 ko || -0m00.16s || 1996 ko | -6.02% | +0.17% 0m02.64s | 1151424 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m02.84s | 1149244 ko || -0m00.19s || 2180 ko | -7.04% | +0.18% 0m02.64s | 536980 ko | Rewriter/Passes/AddAssocLeft.vo | 0m02.73s | 538840 ko || -0m00.08s || -1860 ko | -3.29% | -0.34% 0m02.62s | 1126724 ko | StandaloneOCamlMain.vo | 0m02.81s | 1124820 ko || -0m00.18s || 1904 ko | -6.76% | +0.16% 0m02.60s | 1151328 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m02.82s | 1149340 ko || -0m00.21s || 1988 ko | -7.80% | +0.17% 0m02.57s | 1067372 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m02.83s | 1066028 ko || -0m00.26s || 1344 ko | -9.18% | +0.12% 0m02.51s | 1070256 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m02.69s | 1069024 ko || -0m00.18s || 1232 ko | -6.69% | +0.11% 0m02.46s | 623592 ko | Bedrock/Field/Interface/Compilation2.vo | 0m02.63s | 624284 ko || -0m00.16s || -692 ko | -6.46% | -0.11% 0m02.45s | 548060 ko | Bedrock/Field/Translation/Expr.vo | 0m02.31s | 545488 ko || +0m00.14s || 2572 ko | +6.06% | +0.47% 0m02.34s | 537832 ko | Rewriter/Passes/FlattenThunkedRects.vo | 0m02.28s | 535868 ko || +0m00.06s || 1964 ko | +2.63% | +0.36% 0m02.29s | 1049416 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m02.36s | 1049520 ko || -0m00.06s || -104 ko | -2.96% | -0.00% 0m02.26s | 1046904 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m02.35s | 1046768 ko || -0m00.09s || 136 ko | -3.82% | +0.01% 0m02.26s | 1049440 ko | Bedrock/Field/Translation/Parameters/FE310.vo | 0m02.41s | 1048624 ko || -0m00.15s || 816 ko | -6.22% | +0.07% 0m02.25s | 1049404 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m02.38s | 1049464 ko || -0m00.12s || -60 ko | -5.46% | -0.00% 0m02.03s | 616408 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo | 0m02.14s | 616276 ko || -0m00.11s || 132 ko | -5.14% | +0.02% 0m02.01s | 545060 ko | Stringification/Language.vo | 0m02.01s | 543272 ko || +0m00.00s || 1788 ko | +0.00% | +0.32% 0m01.74s | 539000 ko | Rewriter/Passes/StripLiteralCasts.vo | 0m01.72s | 537668 ko || +0m00.02s || 1332 ko | +1.16% | +0.24% 0m01.71s | 639164 ko | Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo | 0m01.87s | 638432 ko || -0m00.16s || 732 ko | -8.55% | +0.11% 0m01.69s | 536832 ko | Rewriter/Passes/UnfoldValueBarrier.vo | 0m01.77s | 540684 ko || -0m00.08s || -3852 ko | -4.51% | -0.71% 0m01.60s | 514120 ko | AbstractInterpretation/Fancy/AbstractInterpretation.vo | 0m01.64s | 512084 ko || -0m00.03s || 2036 ko | -2.43% | +0.39% 0m01.59s | 540756 ko | Rewriter/Passes/ToFancy.vo | 0m01.59s | 534608 ko || +0m00.00s || 6148 ko | +0.00% | +1.15% 0m01.57s | 522584 ko | AbstractInterpretation/ZRange.vo | 0m01.57s | 520536 ko || +0m00.00s || 2048 ko | +0.00% | +0.39% 0m01.54s | 612044 ko | Bedrock/Field/Common/Names/MakeNames.vo | 0m01.64s | 612792 ko || -0m00.09s || -748 ko | -6.09% | -0.12% 0m01.50s | 511852 ko | AbstractInterpretation/Bottomify/AbstractInterpretation.vo | 0m01.56s | 512044 ko || -0m00.06s || -192 ko | -3.84% | -0.03% 0m01.46s | 593628 ko | CompilersTestCases.vo | 0m01.44s | 592128 ko || +0m00.02s || 1500 ko | +1.38% | +0.25% 0m01.32s | 543916 ko | Stringification/Go.vo | 0m01.30s | 543816 ko || +0m00.02s || 100 ko | +1.53% | +0.01% 0m01.24s | 528640 ko | AbstractInterpretation/Proofs.vo | 0m01.20s | 528576 ko || +0m00.04s || 64 ko | +3.33% | +0.01% 0m01.08s | 633492 ko | Bedrock/Specs/Field.vo | 0m01.23s | 631456 ko || -0m00.14s || 2036 ko | -12.19% | +0.32% 0m01.02s | 610084 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo | 0m01.13s | 610100 ko || -0m00.10s || -16 ko | -9.73% | -0.00% 0m00.98s | 603908 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo | 0m01.01s | 604044 ko || -0m00.03s || -136 ko | -2.97% | -0.02% 0m00.90s | 539712 ko | Bedrock/Field/Translation/LoadStoreList.vo | 0m00.91s | 538964 ko || -0m00.01s || 748 ko | -1.09% | +0.13% 0m00.88s | 541444 ko | Stringification/C.vo | 0m00.89s | 541524 ko || -0m00.01s || -80 ko | -1.12% | -0.01% 0m00.87s | 539148 ko | Stringification/JSON.vo | 0m00.90s | 537108 ko || -0m00.03s || 2040 ko | -3.33% | +0.37% 0m00.84s | 541104 ko | Stringification/Zig.vo | 0m00.81s | 537096 ko || +0m00.02s || 4008 ko | +3.70% | +0.74% 0m00.83s | 616196 ko | Bedrock/Field/Interface/Representation.vo | 0m00.87s | 616296 ko || -0m00.04s || -100 ko | -4.59% | -0.01% 0m00.81s | 536436 ko | Bedrock/Field/Common/Types.vo | 0m00.82s | 535080 ko || -0m00.00s || 1356 ko | -1.21% | +0.25% 0m00.81s | 539924 ko | Bedrock/Field/Translation/Proofs/Equivalence.vo | 0m00.81s | 538976 ko || +0m00.00s || 948 ko | +0.00% | +0.17% 0m00.79s | 620084 ko | Bedrock/Group/Point.vo | 0m00.86s | 621820 ko || -0m00.06s || -1736 ko | -8.13% | -0.27% 0m00.78s | 537940 ko | Stringification/Rust.vo | 0m00.81s | 537864 ko || -0m00.03s || 76 ko | -3.70% | +0.01% 0m00.77s | 537780 ko | Stringification/Java.vo | 0m00.81s | 537972 ko || -0m00.04s || -192 ko | -4.93% | -0.03% 0m00.75s | 590292 ko | Bedrock/Field/Common/Tactics.vo | 0m00.74s | 592228 ko || +0m00.01s || -1936 ko | +1.35% | -0.32% 0m00.72s | 505868 ko | Language/APINotations.vo | 0m00.73s | 505972 ko || -0m00.01s || -104 ko | -1.36% | -0.02% 0m00.69s | 548152 ko | Bedrock/Field/Stringification/FlattenVarData.vo | 0m00.68s | 548924 ko || +0m00.00s || -772 ko | +1.47% | -0.14% 0m00.68s | 541572 ko | Bedrock/Field/Stringification/LoadStoreListVarData.vo | 0m00.70s | 542352 ko || -0m00.01s || -780 ko | -2.85% | -0.14% 0m00.66s | 517348 ko | AbstractInterpretation/Wf.vo | 0m00.61s | 518040 ko || +0m00.05s || -692 ko | +8.19% | -0.13% 0m00.65s | 516864 ko | AbstractInterpretation/Fancy/WfExtra.vo | 0m00.62s | 515400 ko || +0m00.03s || 1464 ko | +4.83% | +0.28% 0m00.65s | 537532 ko | Bedrock/Field/Translation/Flatten.vo | 0m00.64s | 537568 ko || +0m00.01s || -36 ko | +1.56% | -0.00% 0m00.64s | 523068 ko | Bedrock/Field/Common/Arrays/MakeListLengths.vo | 0m00.68s | 523072 ko || -0m00.04s || -4 ko | -5.88% | -0.00% 0m00.64s | 439920 ko | Rewriter/Rules.vo | 0m00.68s | 442548 ko || -0m00.04s || -2628 ko | -5.88% | -0.59% 0m00.63s | 550452 ko | Rewriter/All.vo | 0m00.62s | 548168 ko || +0m00.01s || 2284 ko | +1.61% | +0.41% 0m00.62s | 536664 ko | Bedrock/Field/Translation/Proofs/VarnameSet.vo | 0m00.67s | 537484 ko || -0m00.05s || -820 ko | -7.46% | -0.15% 0m00.62s | 504536 ko | MiscCompilerPassesProofsExtra.vo | 0m00.66s | 505220 ko || -0m00.04s || -684 ko | -6.06% | -0.13% 0m00.61s | 515352 ko | AbstractInterpretation/Bottomify/WfExtra.vo | 0m00.63s | 515384 ko || -0m00.02s || -32 ko | -3.17% | -0.00% 0m00.61s | 502908 ko | Language/WfExtra.vo | 0m00.63s | 502392 ko || -0m00.02s || 516 ko | -3.17% | +0.10% 0m00.60s | 503684 ko | AbstractInterpretation/AbstractInterpretation.vo | 0m00.66s | 503728 ko || -0m00.06s || -44 ko | -9.09% | -0.00% 0m00.60s | 518640 ko | AbstractInterpretation/WfExtra.vo | 0m00.59s | 518248 ko || +0m00.01s || 392 ko | +1.69% | +0.07% 0m00.60s | 513080 ko | Language/API.vo | 0m00.60s | 511192 ko || +0m00.00s || 1888 ko | +0.00% | +0.36% 0m00.60s | 502224 ko | Language/UnderLetsProofsExtra.vo | 0m00.60s | 503052 ko || +0m00.00s || -828 ko | +0.00% | -0.16% 0m00.60s | 511968 ko | PushButtonSynthesis/ReificationCache.vo | 0m00.58s | 512032 ko || +0m00.02s || -64 ko | +3.44% | -0.01% 0m00.55s | 503160 ko | Rewriter/AllTacticsExtra.vo | 0m00.60s | 502504 ko || -0m00.04s || 656 ko | -8.33% | +0.13% 0m00.35s | 405512 ko | Rewriter/TestRules.vo | 0m00.37s | 403052 ko || -0m00.02s || 2460 ko | -5.40% | +0.61% 0m00.34s | 437584 ko | Language/PreExtra.vo | 0m00.31s | 393984 ko || +0m00.03s || 43600 ko | +9.67% | +11.06% 0m00.32s | 415460 ko | Language/IdentifierParameters.vo | 0m00.33s | 413516 ko || -0m00.01s || 1944 ko | -3.03% | +0.47% 0m00.30s | 366268 ko | Rewriter/TestRulesProofs.vo | 0m00.33s | 364416 ko || -0m00.03s || 1852 ko | -9.09% | +0.50% ``` </p> </details>
JasonGross
force-pushed
the
saturated-solinas-idents
branch
from
a8df66a
to
0f395e8
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
Slow identifiers are commented out. I'll have to figure out a different
way to prove the ZRange bounds proof that isn't so slow.
Timing Diff