Add remaining rewrite rules for saturated arithmetic #1778
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
more-rewrite-complex
branch
6 times, most recently
from
968ddba
to
68a01c7
Compare
JasonGross
force-pushed
the
more-rewrite-complex
branch
from
68a01c7
to
73a5072
Compare
JasonGross
added a commit
to JasonGross/rewriter
that referenced
this pull request
Dec 23, 2023
JasonGross
added a commit
to JasonGross/rewriter
that referenced
this pull request
Dec 23, 2023
JasonGross
added a commit
to mit-plv/rewriter
that referenced
this pull request
Dec 23, 2023
JasonGross
force-pushed
the
more-rewrite-complex
branch
from
73a5072
to
1588b10
Compare
JasonGross
force-pushed
the
more-rewrite-complex
branch
2 times, most recently
from
e6e9362
to
87f239d
Compare
|
The timing does not look promising. Timing Diff
|
JasonGross
added
needs: fixing
and removed
awaiting-merge-of-dependency
awaiting-timing-info
labels
Profiling data |
profile of just the new rewrite rules |
JasonGross
added a commit
to JasonGross/rewriter
that referenced
this pull request
Dec 24, 2023
Seems to be responsible for 23.0% of the cost of rewrite rules in mit-plv/fiat-crypto#1778, with a single call taking 168.429s.
JasonGross
added a commit
to mit-plv/rewriter
that referenced
this pull request
Dec 24, 2023
* Add profiling for cbn Seems to be responsible for 23.0% of the cost of rewrite rules in mit-plv/fiat-crypto#1778, with a single call taking 168.429s. * Drop Coq < 8.17 The Ltac2 support is not good enough.
JasonGross
added a commit
to JasonGross/rewriter
that referenced
this pull request
Dec 24, 2023
This should hopefully speed up reduction significantly. Timing is a bit of a mixed bag (on ArithWithCasts in particular), but overall good, and very good for mit-plv/fiat-crypto#1778. <details><summary>Timing Diff (Only Complex NBE)</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) --------------------------------------------------------------------------------------------------------------------------------- 6m27.38s | 4352640 ko | Total Time / Peak Mem | 10m36.83s | 4349248 ko || -4m09.44s || 3392 ko | -39.16% | +0.07% --------------------------------------------------------------------------------------------------------------------------------- 5m30.19s | 4352640 ko | Rewriter/Passes/NBE.vo | 9m38.79s | 4349248 ko || -4m08.59s || 3392 ko | -42.95% | +0.07% 0m56.36s | 833016 ko | Rewriter/RulesProofs.vo | 0m57.16s | 833032 ko || -0m00.79s || -16 ko | -1.39% | -0.00% 0m00.84s | 457988 ko | Rewriter/Rules.vo | 0m00.89s | 456124 ko || -0m00.05s || 1864 ko | -5.61% | +0.40% ``` </p> </details> <details><summary>Timing Diff (Full Fiat Cryptography)</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 70m31.96s | 3445468 ko | Total Time / Peak Mem | 71m53.60s | 3539572 ko || -1m21.63s || -94104 ko | -1.89% | -2.65% -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 8m05.37s | 2661168 ko | Bedrock/End2End/X25519/GarageDoor.vo | 8m27.50s | 2661956 ko || -0m22.12s || -788 ko | -4.36% | -0.02% 4m36.32s | 2492748 ko | Bedrock/End2End/X25519/EdwardsXYZT.vo | 4m52.33s | 2493256 ko || -0m16.00s || -508 ko | -5.47% | -0.02% 3m31.47s | 3445468 ko | Rewriter/Passes/ArithWithCasts.vo | 3m19.41s | 3539572 ko || +0m12.06s || -94104 ko | +6.04% | -2.65% 2m31.42s | 3335368 ko | Rewriter/Passes/NBE.vo | 2m40.05s | 3327880 ko || -0m08.62s || 7488 ko | -5.39% | +0.22% 3m41.83s | 2295144 ko | Assembly/WithBedrock/Proofs.vo | 3m49.57s | 2298492 ko || -0m07.74s || -3348 ko | -3.37% | -0.14% 5m28.65s | 3181688 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo | 5m34.17s | 3178616 ko || -0m05.52s || 3072 ko | -1.65% | +0.09% 2m53.06s | 2655348 ko | Bedrock/End2End/RupicolaCrypto/ChaCha20.vo | 2m56.57s | 2650952 ko || -0m03.50s || 4396 ko | -1.98% | +0.16% 1m52.75s | 2518796 ko | Rewriter/Passes/ToFancyWithCasts.vo | 1m56.20s | 2474660 ko || -0m03.45s || 44136 ko | -2.96% | +1.78% 1m24.67s | 1532696 ko | Assembly/EquivalenceProofs.vo | 1m28.52s | 1535932 ko || -0m03.84s || -3236 ko | -4.34% | -0.21% 1m00.24s | 1362776 ko | Assembly/WithBedrock/SymbolicProofs.vo | 1m03.25s | 1362872 ko || -0m03.00s || -96 ko | -4.75% | -0.00% 2m05.92s | 1385148 ko | Bedrock/End2End/X25519/Field25519.vo | 2m08.40s | 1392128 ko || -0m02.48s || -6980 ko | -1.93% | -0.50% 1m24.77s | 1103548 ko | Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.vo | 1m22.51s | 1089068 ko || +0m02.25s || 14480 ko | +2.73% | +1.32% 1m00.12s | 1393880 ko | Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.vo | 1m02.89s | 1390884 ko || -0m02.77s || 2996 ko | -4.40% | +0.21% 0m44.20s | 1118240 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo | 0m46.28s | 1118352 ko || -0m02.07s || -112 ko | -4.49% | -0.01% 0m31.16s | 900084 ko | Rewriter/Rewriter/Examples/PrefixSums.vo | 0m28.63s | 907212 ko || +0m02.53s || -7128 ko | +8.83% | -0.78% 2m36.62s | 1100532 ko | Fancy/Compiler.vo | 2m34.73s | 1100132 ko || +0m01.89s || 400 ko | +1.22% | +0.03% 1m34.79s | 1951088 ko | SlowPrimeSynthesisExamples.vo | 1m36.21s | 1951248 ko || -0m01.42s || -160 ko | -1.47% | -0.00% 1m33.18s | 2069588 ko | Fancy/Barrett256.vo | 1m31.93s | 2069544 ko || +0m01.25s || 44 ko | +1.35% | +0.00% 1m18.16s | 838412 ko | PushButtonSynthesis/SolinasReductionReificationCache.vo | 1m19.76s | 838420 ko || -0m01.60s || -8 ko | -2.00% | -0.00% 1m02.83s | 869272 ko | AbstractInterpretation/Wf.vo | 1m04.11s | 869412 ko || -0m01.28s || -140 ko | -1.99% | -0.01% 0m51.65s | 1151212 ko | Rewriter/Rewriter/Examples.vo | 0m49.69s | 1153560 ko || +0m01.96s || -2348 ko | +3.94% | -0.20% 0m51.51s | 1119120 ko | Rewriter/Passes/MultiRetSplit.vo | 0m52.90s | 1095208 ko || -0m01.39s || 23912 ko | -2.62% | +2.18% 0m49.53s | 724296 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 0m48.35s | 724252 ko || +0m01.17s || 44 ko | +2.44% | +0.00% 0m46.34s | 1884328 ko | Fancy/Montgomery256.vo | 0m48.15s | 1882076 ko || -0m01.80s || 2252 ko | -3.75% | +0.11% 0m36.20s | 653060 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m37.53s | 653104 ko || -0m01.32s || -44 ko | -3.54% | -0.00% 0m31.04s | 1254384 ko | Bedrock/End2End/X25519/GarageDoorTop.vo | 0m32.14s | 1255108 ko || -0m01.10s || -724 ko | -3.42% | -0.05% 0m20.97s | 926116 ko | Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo | 0m19.54s | 916216 ko || +0m01.42s || 9900 ko | +7.31% | +1.08% 0m12.52s | 668624 ko | Rewriter/Demo.vo | 0m11.47s | 668456 ko || +0m01.04s || 168 ko | +9.15% | +0.02% 1m09.46s | 942948 ko | AbstractInterpretation/ZRangeProofs.vo | 1m09.57s | 943236 ko || -0m00.10s || -288 ko | -0.15% | -0.03% 0m46.87s | 1348304 ko | Assembly/Symbolic.vo | 0m46.46s | 1350988 ko || +0m00.40s || -2684 ko | +0.88% | -0.19% 0m42.95s | 1485056 ko | Rewriter/Passes/Arith.vo | 0m43.03s | 1464772 ko || -0m00.07s || 20284 ko | -0.18% | +1.38% 0m36.17s | 1023364 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo | 0m35.81s | 1027148 ko || +0m00.35s || -3784 ko | +1.00% | -0.36% 0m33.90s | 895312 ko | Rewriter/Passes/MulSplit.vo | 0m33.73s | 908304 ko || +0m00.17s || -12992 ko | +0.50% | -1.43% 0m32.43s | 1222184 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m33.26s | 1222032 ko || -0m00.82s || 152 ko | -2.49% | +0.01% 0m31.12s | 1481496 ko | StandaloneDebuggingExamples.vo | 0m30.92s | 1479016 ko || +0m00.19s || 2480 ko | +0.64% | +0.16% 0m28.78s | 718080 ko | AbstractInterpretation/Proofs.vo | 0m28.83s | 718216 ko || -0m00.04s || -136 ko | -0.17% | -0.01% 0m26.86s | 901368 ko | Language/IdentifiersGENERATED.vo | 0m27.02s | 904776 ko || -0m00.16s || -3408 ko | -0.59% | -0.37% 0m26.45s | 736040 ko | Language/IdentifiersGENERATEDProofs.vo | 0m26.81s | 736152 ko || -0m00.35s || -112 ko | -1.34% | -0.01% 0m25.12s | 1303196 ko | PerfTesting/PerfTestSearch.vo | 0m25.93s | 1303988 ko || -0m00.80s || -792 ko | -3.12% | -0.06% 0m20.80s | 1113188 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m21.74s | 1116044 ko || -0m00.93s || -2856 ko | -4.32% | -0.25% 0m20.29s | 781780 ko | Bedrock/Field/Translation/Proofs/Expr.vo | 0m20.79s | 783272 ko || -0m00.50s || -1492 ko | -2.40% | -0.19% 0m18.92s | 1081924 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m18.75s | 1084908 ko || +0m00.17s || -2984 ko | +0.90% | -0.27% 0m18.56s | 1117340 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m19.47s | 1110736 ko || -0m00.91s || 6604 ko | -4.67% | +0.59% 0m18.29s | 747768 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo | 0m18.71s | 749356 ko || -0m00.42s || -1588 ko | -2.24% | -0.21% 0m17.01s | 1099360 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m17.29s | 1093828 ko || -0m00.27s || 5532 ko | -1.61% | +0.50% 0m16.83s | 1290904 ko | PerfTesting/PerfTestSearchPattern.vo | 0m17.54s | 1290768 ko || -0m00.71s || 136 ko | -4.04% | +0.01% 0m16.33s | 764628 ko | Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.vo | 0m15.57s | 760204 ko || +0m00.75s || 4424 ko | +4.88% | +0.58% 0m15.49s | 1105204 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m15.94s | 1104348 ko || -0m00.44s || 856 ko | -2.82% | +0.07% 0m15.22s | 1124768 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m16.12s | 1124776 ko || -0m00.90s || -8 ko | -5.58% | -0.00% 0m14.42s | 637688 ko | Bedrock/Field/Common/Util.vo | 0m14.80s | 637624 ko || -0m00.38s || 64 ko | -2.56% | +0.01% 0m13.39s | 1549628 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo | 0m13.39s | 1549680 ko || +0m00.00s || -52 ko | +0.00% | -0.00% 0m12.88s | 581368 ko | PushButtonSynthesis/DettmanMultiplicationReificationCache.vo | 0m13.17s | 579468 ko || -0m00.28s || 1900 ko | -2.20% | +0.32% 0m12.01s | 686764 ko | Bedrock/Group/AdditionChains.vo | 0m12.05s | 686588 ko || -0m00.04s || 176 ko | -0.33% | +0.02% 0m11.53s | 676412 ko | Bedrock/Group/ScalarMult/LadderStep.vo | 0m11.73s | 679628 ko || -0m00.20s || -3216 ko | -1.70% | -0.47% 0m11.14s | 1001828 ko | BoundsPipeline.vo | 0m11.58s | 999900 ko || -0m00.43s || 1928 ko | -3.79% | +0.19% 0m10.51s | 711112 ko | Language/IdentifiersBasicGENERATED.vo | 0m10.71s | 709608 ko || -0m00.20s || 1504 ko | -1.86% | +0.21% 0m10.10s | 576652 ko | AbstractInterpretation/ZRangeCommonProofs.vo | 0m10.06s | 576752 ko || +0m00.03s || -100 ko | +0.39% | -0.01% 0m10.03s | 646752 ko | Bedrock/Field/Translation/Proofs/Flatten.vo | 0m09.98s | 646820 ko || +0m00.04s || -68 ko | +0.50% | -0.01% 0m09.20s | 632816 ko | Stringification/IR.vo | 0m09.15s | 634608 ko || +0m00.04s || -1792 ko | +0.54% | -0.28% 0m09.00s | 576700 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m09.14s | 578324 ko || -0m00.14s || -1624 ko | -1.53% | -0.28% 0m08.92s | 1245456 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo | 0m09.33s | 1247352 ko || -0m00.41s || -1896 ko | -4.39% | -0.15% 0m08.57s | 593856 ko | PushButtonSynthesis/BYInversionReificationCache.vo | 0m08.66s | 593812 ko || -0m00.08s || 44 ko | -1.03% | +0.00% 0m08.29s | 677284 ko | Bedrock/Group/ScalarMult/CSwap.vo | 0m08.63s | 675232 ko || -0m00.34s || 2052 ko | -3.93% | +0.30% 0m07.94s | 964156 ko | PushButtonSynthesis/SmallExamples.vo | 0m08.33s | 963152 ko || -0m00.38s || 1004 ko | -4.68% | +0.10% 0m07.91s | 628192 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo | 0m08.14s | 629576 ko || -0m00.23s || -1384 ko | -2.82% | -0.21% 0m07.89s | 998288 ko | PushButtonSynthesis/BaseConversion.vo | 0m08.26s | 991900 ko || -0m00.37s || 6388 ko | -4.47% | +0.64% 0m07.32s | 1014248 ko | PushButtonSynthesis/Primitives.vo | 0m07.61s | 1011680 ko || -0m00.29s || 2568 ko | -3.81% | +0.25% 0m07.00s | 862996 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo | 0m06.94s | 863080 ko || +0m00.05s || -84 ko | +0.86% | -0.00% 0m06.45s | 991184 ko | PushButtonSynthesis/SolinasReduction.vo | 0m06.63s | 997340 ko || -0m00.17s || -6156 ko | -2.71% | -0.61% 0m05.98s | 571608 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo | 0m06.05s | 569504 ko || -0m00.06s || 2104 ko | -1.15% | +0.36% 0m05.96s | 614768 ko | Rewriter/Passes/NoSelect.vo | 0m06.37s | 617024 ko || -0m00.41s || -2256 ko | -6.43% | -0.36% 0m05.75s | 1133792 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m05.50s | 1134036 ko || +0m00.25s || -244 ko | +4.54% | -0.02% 0m05.57s | 571792 ko | Fancy/Prod.vo | 0m05.97s | 571768 ko || -0m00.39s || 24 ko | -6.70% | +0.00% 0m05.46s | 990152 ko | PushButtonSynthesis/BarrettReduction.vo | 0m05.55s | 990108 ko || -0m00.08s || 44 ko | -1.62% | +0.00% 0m05.38s | 1047844 ko | CLI.vo | 0m05.28s | 1047976 ko || +0m00.09s || -132 ko | +1.89% | -0.01% 0m05.19s | 568668 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m05.53s | 568832 ko || -0m00.33s || -164 ko | -6.14% | -0.02% 0m04.94s | 849712 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo | 0m04.85s | 849640 ko || +0m00.09s || 72 ko | +1.85% | +0.00% 0m04.81s | 648420 ko | Bedrock/End2End/RupicolaCrypto/Broadcast.vo | 0m05.09s | 645428 ko || -0m00.28s || 2992 ko | -5.50% | +0.46% 0m04.52s | 576772 ko | Language/InversionExtra.vo | 0m04.44s | 576668 ko || +0m00.07s || 104 ko | +1.80% | +0.01% 0m04.32s | 979404 ko | PushButtonSynthesis/DettmanMultiplication.vo | 0m04.47s | 974560 ko || -0m00.14s || 4844 ko | -3.35% | +0.49% 0m04.05s | 1002636 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m04.39s | 1003040 ko || -0m00.33s || -404 ko | -7.74% | -0.04% 0m03.99s | 1407072 ko | Bedrock/Everything.vo | 0m04.42s | 1407076 ko || -0m00.42s || -4 ko | -9.72% | -0.00% 0m03.94s | 985864 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m04.26s | 979532 ko || -0m00.31s || 6332 ko | -7.51% | +0.64% 0m03.91s | 980892 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m03.91s | 987028 ko || +0m00.00s || -6136 ko | +0.00% | -0.62% 0m03.83s | 1273392 ko | Everything.vo | 0m03.70s | 1273324 ko || +0m00.12s || 68 ko | +3.51% | +0.00% 0m03.81s | 899312 ko | Assembly/Equivalence.vo | 0m03.88s | 897416 ko || -0m00.06s || 1896 ko | -1.80% | +0.21% 0m03.49s | 993844 ko | Rewriter/PerfTesting/Core.vo | 0m03.52s | 994052 ko || -0m00.02s || -208 ko | -0.85% | -0.02% 0m03.42s | 1231888 ko | PerfTesting/PerfTestPrint.vo | 0m03.33s | 1231988 ko || +0m00.08s || -100 ko | +2.70% | -0.00% 0m03.35s | 567060 ko | Rewriter/Passes/ArithWithRelaxedCasts.vo | 0m03.33s | 566640 ko || +0m00.02s || 420 ko | +0.60% | +0.07% 0m03.18s | 1033496 ko | Bedrock/Standalone/StandaloneJsOfOCamlMain.vo | 0m03.16s | 1033480 ko || +0m00.02s || 16 ko | +0.63% | +0.00% 0m03.16s | 1035128 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m03.35s | 1035156 ko || -0m00.18s || -28 ko | -5.67% | -0.00% 0m03.16s | 1035336 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m03.31s | 1035248 ko || -0m00.14s || 88 ko | -4.53% | +0.00% 0m03.13s | 575568 ko | Rewriter/Passes/AddAssocLeft.vo | 0m03.10s | 575444 ko || +0m00.02s || 124 ko | +0.96% | +0.02% 0m03.13s | 1011080 ko | StandaloneJsOfOCamlMain.vo | 0m03.15s | 1011036 ko || -0m00.02s || 44 ko | -0.63% | +0.00% 0m03.07s | 1021192 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m03.23s | 1021288 ko || -0m00.16s || -96 ko | -4.95% | -0.00% 0m03.06s | 993984 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m03.09s | 994852 ko || -0m00.02s || -868 ko | -0.97% | -0.08% 0m03.05s | 1006432 ko | StandaloneMonadicUtils.vo | 0m03.25s | 1006480 ko || -0m00.20s || -48 ko | -6.15% | -0.00% 0m03.04s | 559232 ko | PushButtonSynthesis/BaseConversionReificationCache.vo | 0m03.30s | 559292 ko || -0m00.25s || -60 ko | -7.87% | -0.01% 0m03.03s | 942252 ko | Bedrock/Field/Translation/Cmd.vo | 0m03.36s | 942320 ko || -0m00.33s || -68 ko | -9.82% | -0.00% 0m03.00s | 997332 ko | Bedrock/Field/Stringification/Stringification.vo | 0m03.20s | 999256 ko || -0m00.20s || -1924 ko | -6.25% | -0.19% 0m02.98s | 942948 ko | Bedrock/Field/Translation/Func.vo | 0m03.08s | 942924 ko || -0m00.10s || 24 ko | -3.24% | +0.00% 0m02.94s | 1010768 ko | StandaloneOCamlMain.vo | 0m03.36s | 1010736 ko || -0m00.41s || 32 ko | -12.49% | +0.00% 0m02.92s | 993280 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m02.94s | 993224 ko || -0m00.02s || 56 ko | -0.68% | +0.00% 0m02.92s | 1002192 ko | StandaloneHaskellMain.vo | 0m03.12s | 1002372 ko || -0m00.20s || -180 ko | -6.41% | -0.01% 0m02.89s | 626628 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo | 0m03.14s | 626628 ko || -0m00.25s || 0 ko | -7.96% | +0.00% 0m02.83s | 975056 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m02.94s | 975012 ko || -0m00.10s || 44 ko | -3.74% | +0.00% 0m02.82s | 565180 ko | Rewriter/Passes/FlattenThunkedRects.vo | 0m02.78s | 565068 ko || +0m00.04s || 112 ko | +1.43% | +0.01% 0m02.80s | 555640 ko | Rewriter/Passes/Test.vo | 0m02.93s | 555308 ko || -0m00.13s || 332 ko | -4.43% | +0.05% 0m02.79s | 975024 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m03.04s | 975076 ko || -0m00.25s || -52 ko | -8.22% | -0.00% 0m02.74s | 967628 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m02.98s | 967552 ko || -0m00.23s || 76 ko | -8.05% | +0.00% 0m02.74s | 974976 ko | Bedrock/Field/Translation/Parameters/FE310.vo | 0m03.02s | 975012 ko || -0m00.27s || -36 ko | -9.27% | -0.00% 0m02.49s | 565220 ko | Bedrock/Field/Translation/Expr.vo | 0m02.63s | 565452 ko || -0m00.13s || -232 ko | -5.32% | -0.04% 0m02.42s | 562132 ko | Rewriter/Passes/StripLiteralCasts.vo | 0m02.35s | 562052 ko || +0m00.06s || 80 ko | +2.97% | +0.01% 0m02.40s | 572572 ko | Stringification/Language.vo | 0m02.30s | 572524 ko || +0m00.10s || 48 ko | +4.34% | +0.00% 0m02.32s | 625468 ko | Bedrock/Field/Interface/Compilation2.vo | 0m02.51s | 625352 ko || -0m00.18s || 116 ko | -7.56% | +0.01% 0m02.26s | 622388 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo | 0m02.28s | 622392 ko || -0m00.02s || -4 ko | -0.87% | -0.00% 0m02.21s | 566480 ko | Rewriter/Passes/UnfoldValueBarrier.vo | 0m02.18s | 566508 ko || +0m00.02s || -28 ko | +1.37% | -0.00% 0m02.01s | 567200 ko | Rewriter/Passes/ToFancy.vo | 0m02.09s | 567212 ko || -0m00.08s || -12 ko | -3.82% | -0.00% 0m01.94s | 638116 ko | Bedrock/Group/ScalarMult/ScalarMult.vo | 0m01.89s | 638124 ko || +0m00.05s || -8 ko | +2.64% | -0.00% 0m01.90s | 638032 ko | Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo | 0m01.83s | 637992 ko || +0m00.06s || 40 ko | +3.82% | +0.00% 0m01.82s | 544192 ko | AbstractInterpretation/ZRange.vo | 0m01.70s | 544268 ko || +0m00.12s || -76 ko | +7.05% | -0.01% 0m01.80s | 614356 ko | CompilersTestCases.vo | 0m01.79s | 614440 ko || +0m00.01s || -84 ko | +0.55% | -0.01% 0m01.79s | 535132 ko | AbstractInterpretation/AbstractInterpretation.vo | 0m01.84s | 535240 ko || -0m00.05s || -108 ko | -2.71% | -0.02% 0m01.66s | 614456 ko | Bedrock/Field/Common/Names/MakeNames.vo | 0m01.90s | 614456 ko || -0m00.24s || 0 ko | -12.63% | +0.00% 0m01.59s | 562240 ko | Stringification/Go.vo | 0m01.75s | 562320 ko || -0m00.15s || -80 ko | -9.14% | -0.01% 0m01.57s | 634032 ko | Bedrock/Specs/Field.vo | 0m01.73s | 633640 ko || -0m00.15s || 392 ko | -9.24% | +0.06% 0m01.44s | 612524 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo | 0m01.51s | 616444 ko || -0m00.07s || -3920 ko | -4.63% | -0.63% 0m01.38s | 604032 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo | 0m01.43s | 604164 ko || -0m00.05s || -132 ko | -3.49% | -0.02% 0m01.32s | 619644 ko | Bedrock/Field/Interface/Representation.vo | 0m01.31s | 619784 ko || +0m00.01s || -140 ko | +0.76% | -0.02% 0m01.23s | 614868 ko | Bedrock/Group/Point.vo | 0m01.33s | 615212 ko || -0m00.10s || -344 ko | -7.51% | -0.05% 0m01.23s | 556884 ko | Stringification/C.vo | 0m01.35s | 556948 ko || -0m00.12s || -64 ko | -8.88% | -0.01% 0m01.21s | 590676 ko | Bedrock/Field/Common/Tactics.vo | 0m01.25s | 590780 ko || -0m00.04s || -104 ko | -3.20% | -0.01% 0m01.20s | 558764 ko | Stringification/JSON.vo | 0m01.37s | 558968 ko || -0m00.17s || -204 ko | -12.40% | -0.03% 0m01.18s | 544620 ko | Bedrock/Field/Common/Types.vo | 0m01.17s | 544536 ko || +0m00.01s || 84 ko | +0.85% | +0.01% 0m01.17s | 544340 ko | Bedrock/Field/Translation/LoadStoreList.vo | 0m01.22s | 544292 ko || -0m00.05s || 48 ko | -4.09% | +0.00% 0m01.17s | 493956 ko | Rewriter/Rewriter/Reify.vo | 0m01.06s | 495316 ko || +0m00.10s || -1360 ko | +10.37% | -0.27% 0m01.15s | 545116 ko | Bedrock/Field/Translation/Proofs/Equivalence.vo | 0m01.20s | 544996 ko || -0m00.05s || 120 ko | -4.16% | +0.02% 0m01.15s | 556092 ko | Stringification/Zig.vo | 0m01.27s | 555992 ko || -0m00.12s || 100 ko | -9.44% | +0.01% 0m01.14s | 555848 ko | Stringification/Rust.vo | 0m01.26s | 555792 ko || -0m00.12s || 56 ko | -9.52% | +0.01% 0m01.09s | 555636 ko | Stringification/Java.vo | 0m01.19s | 555460 ko || -0m00.09s || 176 ko | -8.40% | +0.03% 0m01.07s | 558372 ko | Bedrock/Field/Stringification/LoadStoreListVarData.vo | 0m01.10s | 558404 ko || -0m00.03s || -32 ko | -2.72% | -0.00% 0m01.07s | 530640 ko | Language/APINotations.vo | 0m01.08s | 528384 ko || -0m00.01s || 2256 ko | -0.92% | +0.42% 0m01.06s | 507192 ko | Bedrock/Field/Common/Arrays/MakeListLengths.vo | 0m01.11s | 507160 ko || -0m00.05s || 32 ko | -4.50% | +0.00% 0m01.05s | 568500 ko | Rewriter/All.vo | 0m01.08s | 568492 ko || -0m00.03s || 8 ko | -2.77% | +0.00% 0m01.03s | 562556 ko | Bedrock/Field/Stringification/FlattenVarData.vo | 0m01.13s | 562636 ko || -0m00.09s || -80 ko | -8.84% | -0.01% 0m01.03s | 536868 ko | Bedrock/Field/Translation/Proofs/VarnameSet.vo | 0m01.02s | 536852 ko || +0m00.01s || 16 ko | +0.98% | +0.00% 0m01.02s | 529504 ko | AbstractInterpretation/WfExtra.vo | 0m00.98s | 530316 ko || +0m00.04s || -812 ko | +4.08% | -0.15% 0m01.02s | 503696 ko | Rewriter/Rewriter/AllTactics.vo | 0m00.94s | 503736 ko || +0m00.08s || -40 ko | +8.51% | -0.00% 0m00.98s | 539140 ko | Bedrock/Field/Translation/Flatten.vo | 0m01.02s | 539212 ko || -0m00.04s || -72 ko | -3.92% | -0.01% 0m00.96s | 509700 ko | Language/WfExtra.vo | 0m00.89s | 509180 ko || +0m00.06s || 520 ko | +7.86% | +0.10% 0m00.95s | 519220 ko | PushButtonSynthesis/ReificationCache.vo | 0m00.98s | 521116 ko || -0m00.03s || -1896 ko | -3.06% | -0.36% 0m00.94s | 518908 ko | Language/API.vo | 0m00.90s | 518832 ko || +0m00.03s || 76 ko | +4.44% | +0.01% 0m00.94s | 491660 ko | Language/UnderLetsProofsExtra.vo | 0m00.94s | 491476 ko || +0m00.00s || 184 ko | +0.00% | +0.03% 0m00.94s | 522908 ko | MiscCompilerPassesProofsExtra.vo | 0m00.94s | 522932 ko || +0m00.00s || -24 ko | +0.00% | -0.00% 0m00.82s | 401576 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings.vo | 0m00.73s | 401220 ko || +0m00.08s || 356 ko | +12.32% | +0.08% 0m00.81s | 517016 ko | Rewriter/AllTacticsExtra.vo | 0m00.93s | 517112 ko || -0m00.12s || -96 ko | -12.90% | -0.01% 0m00.79s | 496044 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports.vo | 0m00.70s | 496092 ko || +0m00.09s || -48 ko | +12.85% | -0.00% 0m00.78s | 441520 ko | Rewriter/Util/plugins/RewriterBuild.vo | 0m00.70s | 441072 ko || +0m00.08s || 448 ko | +11.42% | +0.10% 0m00.78s | 440760 ko | Rewriter/Util/plugins/RewriterBuildRegistry.vo | 0m00.70s | 440396 ko || +0m00.08s || 364 ko | +11.42% | +0.08% ``` </p> </details>
|
With mit-plv/rewriter#142, this commit now only makes NBE 2x slower (5m30.19s vs 2m31.42s) instead of 4x slower (9m38.79s vs 2m40.05s). This is a bit better, but probably still not good enough. |
JasonGross
added a commit
to mit-plv/rewriter
that referenced
this pull request
Dec 24, 2023
This should hopefully speed up reduction significantly. Timing is a bit of a mixed bag (on ArithWithCasts in particular), but overall good, and very good for mit-plv/fiat-crypto#1778. <details><summary>Timing Diff (Only Complex NBE)</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) --------------------------------------------------------------------------------------------------------------------------------- 6m27.38s | 4352640 ko | Total Time / Peak Mem | 10m36.83s | 4349248 ko || -4m09.44s || 3392 ko | -39.16% | +0.07% --------------------------------------------------------------------------------------------------------------------------------- 5m30.19s | 4352640 ko | Rewriter/Passes/NBE.vo | 9m38.79s | 4349248 ko || -4m08.59s || 3392 ko | -42.95% | +0.07% 0m56.36s | 833016 ko | Rewriter/RulesProofs.vo | 0m57.16s | 833032 ko || -0m00.79s || -16 ko | -1.39% | -0.00% 0m00.84s | 457988 ko | Rewriter/Rules.vo | 0m00.89s | 456124 ko || -0m00.05s || 1864 ko | -5.61% | +0.40% ``` </p> </details> <details><summary>Timing Diff (Full Fiat Cryptography)</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 70m31.96s | 3445468 ko | Total Time / Peak Mem | 71m53.60s | 3539572 ko || -1m21.63s || -94104 ko | -1.89% | -2.65% -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 8m05.37s | 2661168 ko | Bedrock/End2End/X25519/GarageDoor.vo | 8m27.50s | 2661956 ko || -0m22.12s || -788 ko | -4.36% | -0.02% 4m36.32s | 2492748 ko | Bedrock/End2End/X25519/EdwardsXYZT.vo | 4m52.33s | 2493256 ko || -0m16.00s || -508 ko | -5.47% | -0.02% 3m31.47s | 3445468 ko | Rewriter/Passes/ArithWithCasts.vo | 3m19.41s | 3539572 ko || +0m12.06s || -94104 ko | +6.04% | -2.65% 2m31.42s | 3335368 ko | Rewriter/Passes/NBE.vo | 2m40.05s | 3327880 ko || -0m08.62s || 7488 ko | -5.39% | +0.22% 3m41.83s | 2295144 ko | Assembly/WithBedrock/Proofs.vo | 3m49.57s | 2298492 ko || -0m07.74s || -3348 ko | -3.37% | -0.14% 5m28.65s | 3181688 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo | 5m34.17s | 3178616 ko || -0m05.52s || 3072 ko | -1.65% | +0.09% 2m53.06s | 2655348 ko | Bedrock/End2End/RupicolaCrypto/ChaCha20.vo | 2m56.57s | 2650952 ko || -0m03.50s || 4396 ko | -1.98% | +0.16% 1m52.75s | 2518796 ko | Rewriter/Passes/ToFancyWithCasts.vo | 1m56.20s | 2474660 ko || -0m03.45s || 44136 ko | -2.96% | +1.78% 1m24.67s | 1532696 ko | Assembly/EquivalenceProofs.vo | 1m28.52s | 1535932 ko || -0m03.84s || -3236 ko | -4.34% | -0.21% 1m00.24s | 1362776 ko | Assembly/WithBedrock/SymbolicProofs.vo | 1m03.25s | 1362872 ko || -0m03.00s || -96 ko | -4.75% | -0.00% 2m05.92s | 1385148 ko | Bedrock/End2End/X25519/Field25519.vo | 2m08.40s | 1392128 ko || -0m02.48s || -6980 ko | -1.93% | -0.50% 1m24.77s | 1103548 ko | Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.vo | 1m22.51s | 1089068 ko || +0m02.25s || 14480 ko | +2.73% | +1.32% 1m00.12s | 1393880 ko | Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.vo | 1m02.89s | 1390884 ko || -0m02.77s || 2996 ko | -4.40% | +0.21% 0m44.20s | 1118240 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo | 0m46.28s | 1118352 ko || -0m02.07s || -112 ko | -4.49% | -0.01% 0m31.16s | 900084 ko | Rewriter/Rewriter/Examples/PrefixSums.vo | 0m28.63s | 907212 ko || +0m02.53s || -7128 ko | +8.83% | -0.78% 2m36.62s | 1100532 ko | Fancy/Compiler.vo | 2m34.73s | 1100132 ko || +0m01.89s || 400 ko | +1.22% | +0.03% 1m34.79s | 1951088 ko | SlowPrimeSynthesisExamples.vo | 1m36.21s | 1951248 ko || -0m01.42s || -160 ko | -1.47% | -0.00% 1m33.18s | 2069588 ko | Fancy/Barrett256.vo | 1m31.93s | 2069544 ko || +0m01.25s || 44 ko | +1.35% | +0.00% 1m18.16s | 838412 ko | PushButtonSynthesis/SolinasReductionReificationCache.vo | 1m19.76s | 838420 ko || -0m01.60s || -8 ko | -2.00% | -0.00% 1m02.83s | 869272 ko | AbstractInterpretation/Wf.vo | 1m04.11s | 869412 ko || -0m01.28s || -140 ko | -1.99% | -0.01% 0m51.65s | 1151212 ko | Rewriter/Rewriter/Examples.vo | 0m49.69s | 1153560 ko || +0m01.96s || -2348 ko | +3.94% | -0.20% 0m51.51s | 1119120 ko | Rewriter/Passes/MultiRetSplit.vo | 0m52.90s | 1095208 ko || -0m01.39s || 23912 ko | -2.62% | +2.18% 0m49.53s | 724296 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 0m48.35s | 724252 ko || +0m01.17s || 44 ko | +2.44% | +0.00% 0m46.34s | 1884328 ko | Fancy/Montgomery256.vo | 0m48.15s | 1882076 ko || -0m01.80s || 2252 ko | -3.75% | +0.11% 0m36.20s | 653060 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m37.53s | 653104 ko || -0m01.32s || -44 ko | -3.54% | -0.00% 0m31.04s | 1254384 ko | Bedrock/End2End/X25519/GarageDoorTop.vo | 0m32.14s | 1255108 ko || -0m01.10s || -724 ko | -3.42% | -0.05% 0m20.97s | 926116 ko | Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo | 0m19.54s | 916216 ko || +0m01.42s || 9900 ko | +7.31% | +1.08% 0m12.52s | 668624 ko | Rewriter/Demo.vo | 0m11.47s | 668456 ko || +0m01.04s || 168 ko | +9.15% | +0.02% 1m09.46s | 942948 ko | AbstractInterpretation/ZRangeProofs.vo | 1m09.57s | 943236 ko || -0m00.10s || -288 ko | -0.15% | -0.03% 0m46.87s | 1348304 ko | Assembly/Symbolic.vo | 0m46.46s | 1350988 ko || +0m00.40s || -2684 ko | +0.88% | -0.19% 0m42.95s | 1485056 ko | Rewriter/Passes/Arith.vo | 0m43.03s | 1464772 ko || -0m00.07s || 20284 ko | -0.18% | +1.38% 0m36.17s | 1023364 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo | 0m35.81s | 1027148 ko || +0m00.35s || -3784 ko | +1.00% | -0.36% 0m33.90s | 895312 ko | Rewriter/Passes/MulSplit.vo | 0m33.73s | 908304 ko || +0m00.17s || -12992 ko | +0.50% | -1.43% 0m32.43s | 1222184 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m33.26s | 1222032 ko || -0m00.82s || 152 ko | -2.49% | +0.01% 0m31.12s | 1481496 ko | StandaloneDebuggingExamples.vo | 0m30.92s | 1479016 ko || +0m00.19s || 2480 ko | +0.64% | +0.16% 0m28.78s | 718080 ko | AbstractInterpretation/Proofs.vo | 0m28.83s | 718216 ko || -0m00.04s || -136 ko | -0.17% | -0.01% 0m26.86s | 901368 ko | Language/IdentifiersGENERATED.vo | 0m27.02s | 904776 ko || -0m00.16s || -3408 ko | -0.59% | -0.37% 0m26.45s | 736040 ko | Language/IdentifiersGENERATEDProofs.vo | 0m26.81s | 736152 ko || -0m00.35s || -112 ko | -1.34% | -0.01% 0m25.12s | 1303196 ko | PerfTesting/PerfTestSearch.vo | 0m25.93s | 1303988 ko || -0m00.80s || -792 ko | -3.12% | -0.06% 0m20.80s | 1113188 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m21.74s | 1116044 ko || -0m00.93s || -2856 ko | -4.32% | -0.25% 0m20.29s | 781780 ko | Bedrock/Field/Translation/Proofs/Expr.vo | 0m20.79s | 783272 ko || -0m00.50s || -1492 ko | -2.40% | -0.19% 0m18.92s | 1081924 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m18.75s | 1084908 ko || +0m00.17s || -2984 ko | +0.90% | -0.27% 0m18.56s | 1117340 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m19.47s | 1110736 ko || -0m00.91s || 6604 ko | -4.67% | +0.59% 0m18.29s | 747768 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo | 0m18.71s | 749356 ko || -0m00.42s || -1588 ko | -2.24% | -0.21% 0m17.01s | 1099360 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m17.29s | 1093828 ko || -0m00.27s || 5532 ko | -1.61% | +0.50% 0m16.83s | 1290904 ko | PerfTesting/PerfTestSearchPattern.vo | 0m17.54s | 1290768 ko || -0m00.71s || 136 ko | -4.04% | +0.01% 0m16.33s | 764628 ko | Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.vo | 0m15.57s | 760204 ko || +0m00.75s || 4424 ko | +4.88% | +0.58% 0m15.49s | 1105204 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m15.94s | 1104348 ko || -0m00.44s || 856 ko | -2.82% | +0.07% 0m15.22s | 1124768 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m16.12s | 1124776 ko || -0m00.90s || -8 ko | -5.58% | -0.00% 0m14.42s | 637688 ko | Bedrock/Field/Common/Util.vo | 0m14.80s | 637624 ko || -0m00.38s || 64 ko | -2.56% | +0.01% 0m13.39s | 1549628 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo | 0m13.39s | 1549680 ko || +0m00.00s || -52 ko | +0.00% | -0.00% 0m12.88s | 581368 ko | PushButtonSynthesis/DettmanMultiplicationReificationCache.vo | 0m13.17s | 579468 ko || -0m00.28s || 1900 ko | -2.20% | +0.32% 0m12.01s | 686764 ko | Bedrock/Group/AdditionChains.vo | 0m12.05s | 686588 ko || -0m00.04s || 176 ko | -0.33% | +0.02% 0m11.53s | 676412 ko | Bedrock/Group/ScalarMult/LadderStep.vo | 0m11.73s | 679628 ko || -0m00.20s || -3216 ko | -1.70% | -0.47% 0m11.14s | 1001828 ko | BoundsPipeline.vo | 0m11.58s | 999900 ko || -0m00.43s || 1928 ko | -3.79% | +0.19% 0m10.51s | 711112 ko | Language/IdentifiersBasicGENERATED.vo | 0m10.71s | 709608 ko || -0m00.20s || 1504 ko | -1.86% | +0.21% 0m10.10s | 576652 ko | AbstractInterpretation/ZRangeCommonProofs.vo | 0m10.06s | 576752 ko || +0m00.03s || -100 ko | +0.39% | -0.01% 0m10.03s | 646752 ko | Bedrock/Field/Translation/Proofs/Flatten.vo | 0m09.98s | 646820 ko || +0m00.04s || -68 ko | +0.50% | -0.01% 0m09.20s | 632816 ko | Stringification/IR.vo | 0m09.15s | 634608 ko || +0m00.04s || -1792 ko | +0.54% | -0.28% 0m09.00s | 576700 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m09.14s | 578324 ko || -0m00.14s || -1624 ko | -1.53% | -0.28% 0m08.92s | 1245456 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo | 0m09.33s | 1247352 ko || -0m00.41s || -1896 ko | -4.39% | -0.15% 0m08.57s | 593856 ko | PushButtonSynthesis/BYInversionReificationCache.vo | 0m08.66s | 593812 ko || -0m00.08s || 44 ko | -1.03% | +0.00% 0m08.29s | 677284 ko | Bedrock/Group/ScalarMult/CSwap.vo | 0m08.63s | 675232 ko || -0m00.34s || 2052 ko | -3.93% | +0.30% 0m07.94s | 964156 ko | PushButtonSynthesis/SmallExamples.vo | 0m08.33s | 963152 ko || -0m00.38s || 1004 ko | -4.68% | +0.10% 0m07.91s | 628192 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo | 0m08.14s | 629576 ko || -0m00.23s || -1384 ko | -2.82% | -0.21% 0m07.89s | 998288 ko | PushButtonSynthesis/BaseConversion.vo | 0m08.26s | 991900 ko || -0m00.37s || 6388 ko | -4.47% | +0.64% 0m07.32s | 1014248 ko | PushButtonSynthesis/Primitives.vo | 0m07.61s | 1011680 ko || -0m00.29s || 2568 ko | -3.81% | +0.25% 0m07.00s | 862996 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo | 0m06.94s | 863080 ko || +0m00.05s || -84 ko | +0.86% | -0.00% 0m06.45s | 991184 ko | PushButtonSynthesis/SolinasReduction.vo | 0m06.63s | 997340 ko || -0m00.17s || -6156 ko | -2.71% | -0.61% 0m05.98s | 571608 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo | 0m06.05s | 569504 ko || -0m00.06s || 2104 ko | -1.15% | +0.36% 0m05.96s | 614768 ko | Rewriter/Passes/NoSelect.vo | 0m06.37s | 617024 ko || -0m00.41s || -2256 ko | -6.43% | -0.36% 0m05.75s | 1133792 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m05.50s | 1134036 ko || +0m00.25s || -244 ko | +4.54% | -0.02% 0m05.57s | 571792 ko | Fancy/Prod.vo | 0m05.97s | 571768 ko || -0m00.39s || 24 ko | -6.70% | +0.00% 0m05.46s | 990152 ko | PushButtonSynthesis/BarrettReduction.vo | 0m05.55s | 990108 ko || -0m00.08s || 44 ko | -1.62% | +0.00% 0m05.38s | 1047844 ko | CLI.vo | 0m05.28s | 1047976 ko || +0m00.09s || -132 ko | +1.89% | -0.01% 0m05.19s | 568668 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m05.53s | 568832 ko || -0m00.33s || -164 ko | -6.14% | -0.02% 0m04.94s | 849712 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo | 0m04.85s | 849640 ko || +0m00.09s || 72 ko | +1.85% | +0.00% 0m04.81s | 648420 ko | Bedrock/End2End/RupicolaCrypto/Broadcast.vo | 0m05.09s | 645428 ko || -0m00.28s || 2992 ko | -5.50% | +0.46% 0m04.52s | 576772 ko | Language/InversionExtra.vo | 0m04.44s | 576668 ko || +0m00.07s || 104 ko | +1.80% | +0.01% 0m04.32s | 979404 ko | PushButtonSynthesis/DettmanMultiplication.vo | 0m04.47s | 974560 ko || -0m00.14s || 4844 ko | -3.35% | +0.49% 0m04.05s | 1002636 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m04.39s | 1003040 ko || -0m00.33s || -404 ko | -7.74% | -0.04% 0m03.99s | 1407072 ko | Bedrock/Everything.vo | 0m04.42s | 1407076 ko || -0m00.42s || -4 ko | -9.72% | -0.00% 0m03.94s | 985864 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m04.26s | 979532 ko || -0m00.31s || 6332 ko | -7.51% | +0.64% 0m03.91s | 980892 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m03.91s | 987028 ko || +0m00.00s || -6136 ko | +0.00% | -0.62% 0m03.83s | 1273392 ko | Everything.vo | 0m03.70s | 1273324 ko || +0m00.12s || 68 ko | +3.51% | +0.00% 0m03.81s | 899312 ko | Assembly/Equivalence.vo | 0m03.88s | 897416 ko || -0m00.06s || 1896 ko | -1.80% | +0.21% 0m03.49s | 993844 ko | Rewriter/PerfTesting/Core.vo | 0m03.52s | 994052 ko || -0m00.02s || -208 ko | -0.85% | -0.02% 0m03.42s | 1231888 ko | PerfTesting/PerfTestPrint.vo | 0m03.33s | 1231988 ko || +0m00.08s || -100 ko | +2.70% | -0.00% 0m03.35s | 567060 ko | Rewriter/Passes/ArithWithRelaxedCasts.vo | 0m03.33s | 566640 ko || +0m00.02s || 420 ko | +0.60% | +0.07% 0m03.18s | 1033496 ko | Bedrock/Standalone/StandaloneJsOfOCamlMain.vo | 0m03.16s | 1033480 ko || +0m00.02s || 16 ko | +0.63% | +0.00% 0m03.16s | 1035128 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m03.35s | 1035156 ko || -0m00.18s || -28 ko | -5.67% | -0.00% 0m03.16s | 1035336 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m03.31s | 1035248 ko || -0m00.14s || 88 ko | -4.53% | +0.00% 0m03.13s | 575568 ko | Rewriter/Passes/AddAssocLeft.vo | 0m03.10s | 575444 ko || +0m00.02s || 124 ko | +0.96% | +0.02% 0m03.13s | 1011080 ko | StandaloneJsOfOCamlMain.vo | 0m03.15s | 1011036 ko || -0m00.02s || 44 ko | -0.63% | +0.00% 0m03.07s | 1021192 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m03.23s | 1021288 ko || -0m00.16s || -96 ko | -4.95% | -0.00% 0m03.06s | 993984 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m03.09s | 994852 ko || -0m00.02s || -868 ko | -0.97% | -0.08% 0m03.05s | 1006432 ko | StandaloneMonadicUtils.vo | 0m03.25s | 1006480 ko || -0m00.20s || -48 ko | -6.15% | -0.00% 0m03.04s | 559232 ko | PushButtonSynthesis/BaseConversionReificationCache.vo | 0m03.30s | 559292 ko || -0m00.25s || -60 ko | -7.87% | -0.01% 0m03.03s | 942252 ko | Bedrock/Field/Translation/Cmd.vo | 0m03.36s | 942320 ko || -0m00.33s || -68 ko | -9.82% | -0.00% 0m03.00s | 997332 ko | Bedrock/Field/Stringification/Stringification.vo | 0m03.20s | 999256 ko || -0m00.20s || -1924 ko | -6.25% | -0.19% 0m02.98s | 942948 ko | Bedrock/Field/Translation/Func.vo | 0m03.08s | 942924 ko || -0m00.10s || 24 ko | -3.24% | +0.00% 0m02.94s | 1010768 ko | StandaloneOCamlMain.vo | 0m03.36s | 1010736 ko || -0m00.41s || 32 ko | -12.49% | +0.00% 0m02.92s | 993280 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m02.94s | 993224 ko || -0m00.02s || 56 ko | -0.68% | +0.00% 0m02.92s | 1002192 ko | StandaloneHaskellMain.vo | 0m03.12s | 1002372 ko || -0m00.20s || -180 ko | -6.41% | -0.01% 0m02.89s | 626628 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo | 0m03.14s | 626628 ko || -0m00.25s || 0 ko | -7.96% | +0.00% 0m02.83s | 975056 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m02.94s | 975012 ko || -0m00.10s || 44 ko | -3.74% | +0.00% 0m02.82s | 565180 ko | Rewriter/Passes/FlattenThunkedRects.vo | 0m02.78s | 565068 ko || +0m00.04s || 112 ko | +1.43% | +0.01% 0m02.80s | 555640 ko | Rewriter/Passes/Test.vo | 0m02.93s | 555308 ko || -0m00.13s || 332 ko | -4.43% | +0.05% 0m02.79s | 975024 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m03.04s | 975076 ko || -0m00.25s || -52 ko | -8.22% | -0.00% 0m02.74s | 967628 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m02.98s | 967552 ko || -0m00.23s || 76 ko | -8.05% | +0.00% 0m02.74s | 974976 ko | Bedrock/Field/Translation/Parameters/FE310.vo | 0m03.02s | 975012 ko || -0m00.27s || -36 ko | -9.27% | -0.00% 0m02.49s | 565220 ko | Bedrock/Field/Translation/Expr.vo | 0m02.63s | 565452 ko || -0m00.13s || -232 ko | -5.32% | -0.04% 0m02.42s | 562132 ko | Rewriter/Passes/StripLiteralCasts.vo | 0m02.35s | 562052 ko || +0m00.06s || 80 ko | +2.97% | +0.01% 0m02.40s | 572572 ko | Stringification/Language.vo | 0m02.30s | 572524 ko || +0m00.10s || 48 ko | +4.34% | +0.00% 0m02.32s | 625468 ko | Bedrock/Field/Interface/Compilation2.vo | 0m02.51s | 625352 ko || -0m00.18s || 116 ko | -7.56% | +0.01% 0m02.26s | 622388 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo | 0m02.28s | 622392 ko || -0m00.02s || -4 ko | -0.87% | -0.00% 0m02.21s | 566480 ko | Rewriter/Passes/UnfoldValueBarrier.vo | 0m02.18s | 566508 ko || +0m00.02s || -28 ko | +1.37% | -0.00% 0m02.01s | 567200 ko | Rewriter/Passes/ToFancy.vo | 0m02.09s | 567212 ko || -0m00.08s || -12 ko | -3.82% | -0.00% 0m01.94s | 638116 ko | Bedrock/Group/ScalarMult/ScalarMult.vo | 0m01.89s | 638124 ko || +0m00.05s || -8 ko | +2.64% | -0.00% 0m01.90s | 638032 ko | Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo | 0m01.83s | 637992 ko || +0m00.06s || 40 ko | +3.82% | +0.00% 0m01.82s | 544192 ko | AbstractInterpretation/ZRange.vo | 0m01.70s | 544268 ko || +0m00.12s || -76 ko | +7.05% | -0.01% 0m01.80s | 614356 ko | CompilersTestCases.vo | 0m01.79s | 614440 ko || +0m00.01s || -84 ko | +0.55% | -0.01% 0m01.79s | 535132 ko | AbstractInterpretation/AbstractInterpretation.vo | 0m01.84s | 535240 ko || -0m00.05s || -108 ko | -2.71% | -0.02% 0m01.66s | 614456 ko | Bedrock/Field/Common/Names/MakeNames.vo | 0m01.90s | 614456 ko || -0m00.24s || 0 ko | -12.63% | +0.00% 0m01.59s | 562240 ko | Stringification/Go.vo | 0m01.75s | 562320 ko || -0m00.15s || -80 ko | -9.14% | -0.01% 0m01.57s | 634032 ko | Bedrock/Specs/Field.vo | 0m01.73s | 633640 ko || -0m00.15s || 392 ko | -9.24% | +0.06% 0m01.44s | 612524 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo | 0m01.51s | 616444 ko || -0m00.07s || -3920 ko | -4.63% | -0.63% 0m01.38s | 604032 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo | 0m01.43s | 604164 ko || -0m00.05s || -132 ko | -3.49% | -0.02% 0m01.32s | 619644 ko | Bedrock/Field/Interface/Representation.vo | 0m01.31s | 619784 ko || +0m00.01s || -140 ko | +0.76% | -0.02% 0m01.23s | 614868 ko | Bedrock/Group/Point.vo | 0m01.33s | 615212 ko || -0m00.10s || -344 ko | -7.51% | -0.05% 0m01.23s | 556884 ko | Stringification/C.vo | 0m01.35s | 556948 ko || -0m00.12s || -64 ko | -8.88% | -0.01% 0m01.21s | 590676 ko | Bedrock/Field/Common/Tactics.vo | 0m01.25s | 590780 ko || -0m00.04s || -104 ko | -3.20% | -0.01% 0m01.20s | 558764 ko | Stringification/JSON.vo | 0m01.37s | 558968 ko || -0m00.17s || -204 ko | -12.40% | -0.03% 0m01.18s | 544620 ko | Bedrock/Field/Common/Types.vo | 0m01.17s | 544536 ko || +0m00.01s || 84 ko | +0.85% | +0.01% 0m01.17s | 544340 ko | Bedrock/Field/Translation/LoadStoreList.vo | 0m01.22s | 544292 ko || -0m00.05s || 48 ko | -4.09% | +0.00% 0m01.17s | 493956 ko | Rewriter/Rewriter/Reify.vo | 0m01.06s | 495316 ko || +0m00.10s || -1360 ko | +10.37% | -0.27% 0m01.15s | 545116 ko | Bedrock/Field/Translation/Proofs/Equivalence.vo | 0m01.20s | 544996 ko || -0m00.05s || 120 ko | -4.16% | +0.02% 0m01.15s | 556092 ko | Stringification/Zig.vo | 0m01.27s | 555992 ko || -0m00.12s || 100 ko | -9.44% | +0.01% 0m01.14s | 555848 ko | Stringification/Rust.vo | 0m01.26s | 555792 ko || -0m00.12s || 56 ko | -9.52% | +0.01% 0m01.09s | 555636 ko | Stringification/Java.vo | 0m01.19s | 555460 ko || -0m00.09s || 176 ko | -8.40% | +0.03% 0m01.07s | 558372 ko | Bedrock/Field/Stringification/LoadStoreListVarData.vo | 0m01.10s | 558404 ko || -0m00.03s || -32 ko | -2.72% | -0.00% 0m01.07s | 530640 ko | Language/APINotations.vo | 0m01.08s | 528384 ko || -0m00.01s || 2256 ko | -0.92% | +0.42% 0m01.06s | 507192 ko | Bedrock/Field/Common/Arrays/MakeListLengths.vo | 0m01.11s | 507160 ko || -0m00.05s || 32 ko | -4.50% | +0.00% 0m01.05s | 568500 ko | Rewriter/All.vo | 0m01.08s | 568492 ko || -0m00.03s || 8 ko | -2.77% | +0.00% 0m01.03s | 562556 ko | Bedrock/Field/Stringification/FlattenVarData.vo | 0m01.13s | 562636 ko || -0m00.09s || -80 ko | -8.84% | -0.01% 0m01.03s | 536868 ko | Bedrock/Field/Translation/Proofs/VarnameSet.vo | 0m01.02s | 536852 ko || +0m00.01s || 16 ko | +0.98% | +0.00% 0m01.02s | 529504 ko | AbstractInterpretation/WfExtra.vo | 0m00.98s | 530316 ko || +0m00.04s || -812 ko | +4.08% | -0.15% 0m01.02s | 503696 ko | Rewriter/Rewriter/AllTactics.vo | 0m00.94s | 503736 ko || +0m00.08s || -40 ko | +8.51% | -0.00% 0m00.98s | 539140 ko | Bedrock/Field/Translation/Flatten.vo | 0m01.02s | 539212 ko || -0m00.04s || -72 ko | -3.92% | -0.01% 0m00.96s | 509700 ko | Language/WfExtra.vo | 0m00.89s | 509180 ko || +0m00.06s || 520 ko | +7.86% | +0.10% 0m00.95s | 519220 ko | PushButtonSynthesis/ReificationCache.vo | 0m00.98s | 521116 ko || -0m00.03s || -1896 ko | -3.06% | -0.36% 0m00.94s | 518908 ko | Language/API.vo | 0m00.90s | 518832 ko || +0m00.03s || 76 ko | +4.44% | +0.01% 0m00.94s | 491660 ko | Language/UnderLetsProofsExtra.vo | 0m00.94s | 491476 ko || +0m00.00s || 184 ko | +0.00% | +0.03% 0m00.94s | 522908 ko | MiscCompilerPassesProofsExtra.vo | 0m00.94s | 522932 ko || +0m00.00s || -24 ko | +0.00% | -0.00% 0m00.82s | 401576 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings.vo | 0m00.73s | 401220 ko || +0m00.08s || 356 ko | +12.32% | +0.08% 0m00.81s | 517016 ko | Rewriter/AllTacticsExtra.vo | 0m00.93s | 517112 ko || -0m00.12s || -96 ko | -12.90% | -0.01% 0m00.79s | 496044 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports.vo | 0m00.70s | 496092 ko || +0m00.09s || -48 ko | +12.85% | -0.00% 0m00.78s | 441520 ko | Rewriter/Util/plugins/RewriterBuild.vo | 0m00.70s | 441072 ko || +0m00.08s || 448 ko | +11.42% | +0.10% 0m00.78s | 440760 ko | Rewriter/Util/plugins/RewriterBuildRegistry.vo | 0m00.70s | 440396 ko || +0m00.08s || 364 ko | +11.42% | +0.08% ``` </p> </details>
|
Of the time spent in the new rewrite rule reification, 82.7% is spent in I have asked about speeding this up on Zulip, but at this point I'm inclined to run another timing diff after mit-plv/rewriter#142 and then eat the ~2--3 minute slowdown. (I'm also out of debugging time, @andres-erbsen if you want to debug, consider applying the patch diff --git a/src/Rewriter/Passes/NBE.v b/src/Rewriter/Passes/NBE.v
index 429a6125f..784248943 100644
--- a/src/Rewriter/Passes/NBE.v
+++ b/src/Rewriter/Passes/NBE.v
@@ -16,8 +16,14 @@ Module Compilers.
Module Import RewriteRules.
Section __.
- Definition VerifiedRewriterNBE : VerifiedRewriter_with_args true false true nbe_rewrite_rules_proofs.
+ Set Ltac Profiling.
+ Set Printing Depth 1000000.
+ Ltac2 Set Rewriter.Language.PreCommon.Pre.reify_profile_cbn := Init.true.
+ Ltac2 Set Reify.should_debug_profile := fun () => Init.true.
+ Definition VerifiedRewriterNBE : VerifiedRewriter_with_args false false true nbe_rewrite_rules_proofs.
Proof using All. make_rewriter. Defined.
+ Redirect "profile" Show Ltac Profile.
+ Redirect "profile0" Show Ltac Profile CutOff 0.
Definition default_opts := Eval hnf in @default_opts VerifiedRewriterNBE.
Let optsT := Eval hnf in optsT VerifiedRewriterNBE.
diff --git a/src/Rewriter/Rules.v b/src/Rewriter/Rules.v
index 08d572064..1c4d81e04 100644
--- a/src/Rewriter/Rules.v
+++ b/src/Rewriter/Rules.v
@@ -51,7 +51,7 @@ Definition nbe_rewrite_rulesT : list (bool * Prop)
myflatten
[mymap
dont_do_again
- [(forall A B x y, @fst A B (x, y) = x)
+ [(*(forall A B x y, @fst A B (x, y) = x)
; (forall A B x y, @snd A B (x, y) = y)
; (forall P t f, @Thunked.bool_rect P t f true = t tt)
; (forall P t f, @Thunked.bool_rect P t f false = f tt)
@@ -183,7 +183,7 @@ Definition nbe_rewrite_rulesT : list (bool * Prop)
end)
('n)
xs)
- ; typeof! @unfold1_nat_rect_fbb_b
+ ; *)typeof! @unfold1_nat_rect_fbb_b
; typeof! @unfold1_nat_rect_fbb_b_b
; typeof! @unfold1_list_rect_fbb_b
; typeof! @unfold1_list_rect_fbb_b_bYou might also want to throw a |
|
For future archeologists: locally but not on CI. Very much not sure what to make of it, but I don't think it should block this PR if CI passes. |
JasonGross
force-pushed
the
more-rewrite-complex
branch
2 times, most recently
from
afb40f7
to
0ccc145
Compare
JasonGross
force-pushed
the
more-rewrite-complex
branch
from
0ccc145
to
ea82a69
Compare
For https://github.com/mit-plv/fiat-crypto/pull/1609
<details><summary>Timing Diff</summary>
<p>
```
After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem)
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
133m38.95s | 4370484 ko | Total Time / Peak Mem | 129m38.05s | 3712508 ko || +4m00.90s || 657976 ko | +3.09% | +17.72%
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
5m34.12s | 4370484 ko | Rewriter/Passes/NBE.vo | 2m34.13s | 3330528 ko || +2m59.99s || 1039956 ko | +116.77% | +31.22%
1m59.50s | 2329072 ko | fiat-rust/src/p384_scalar_32.rs | 2m02.66s | 2299112 ko || -0m03.15s || 29960 ko | -2.57% | +1.30%
1m57.95s | 2415624 ko | fiat-json/src/p384_32.json | 1m54.82s | 2444832 ko || +0m03.13s || -29208 ko | +2.72% | -1.19%
0m39.98s | 2234396 ko | ExtractionOCaml/dettman_multiplication | 0m36.98s | 1927716 ko || +0m03.00s || 306680 ko | +8.11% | +15.90%
5m31.05s | 3200456 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo | 5m28.82s | 3175412 ko || +0m02.23s || 25044 ko | +0.67% | +0.78%
2m00.23s | 2461568 ko | fiat-json/src/p384_scalar_32.json | 1m58.15s | 2162244 ko || +0m02.07s || 299324 ko | +1.76% | +13.84%
1m59.33s | 2241456 ko | fiat-bedrock2/src/p384_scalar_32.c | 2m01.48s | 2430500 ko || -0m02.15s || -189044 ko | -1.76% | -7.77%
1m58.75s | 2141892 ko | fiat-java/src/FiatP384Scalar.java | 2m01.05s | 2237348 ko || -0m02.29s || -95456 ko | -1.90% | -4.26%
1m58.44s | 2273192 ko | fiat-go/32/p384scalar/p384scalar.go | 2m00.68s | 2317900 ko || -0m02.24s || -44708 ko | -1.85% | -1.92%
1m57.40s | 2307724 ko | fiat-java/src/FiatP384.java | 1m59.84s | 2327088 ko || -0m02.43s || -19364 ko | -2.03% | -0.83%
1m56.84s | 2321212 ko | fiat-zig/src/p384_32.zig | 1m59.10s | 2285560 ko || -0m02.25s || 35652 ko | -1.89% | +1.55%
1m56.07s | 2290720 ko | fiat-c/src/p384_32.c | 1m58.32s | 2325148 ko || -0m02.25s || -34428 ko | -1.90% | -1.48%
1m02.24s | 3703520 ko | ExtractionOCaml/with_bedrock2_fiat_crypto | 0m59.53s | 3712508 ko || +0m02.71s || -8988 ko | +4.55% | -0.24%
1m01.35s | 3705452 ko | ExtractionOCaml/bedrock2_fiat_crypto | 0m59.03s | 3710668 ko || +0m02.32s || -5216 ko | +3.93% | -0.14%
0m54.91s | 3724428 ko | ExtractionOCaml/fiat_crypto | 0m52.48s | 3710332 ko || +0m02.42s || 14096 ko | +4.63% | +0.37%
0m54.29s | 2480048 ko | ExtractionJsOfOCaml/fiat_crypto.ml | 0m52.17s | 2487376 ko || +0m02.11s || -7328 ko | +4.06% | -0.29%
0m48.09s | 2652116 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery | 0m45.49s | 2632088 ko || +0m02.60s || 20028 ko | +5.71% | +0.76%
0m47.65s | 2657836 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery | 0m44.92s | 2630968 ko || +0m02.72s || 26868 ko | +6.07% | +1.02%
0m47.57s | 2726404 ko | ExtractionOCaml/bedrock2_solinas_reduction | 0m45.01s | 2704500 ko || +0m02.56s || 21904 ko | +5.68% | +0.80%
0m45.77s | 2689372 ko | ExtractionOCaml/solinas_reduction | 0m43.29s | 2683760 ko || +0m02.48s || 5612 ko | +5.72% | +0.20%
0m45.63s | 2633500 ko | ExtractionOCaml/word_by_word_montgomery | 0m43.16s | 2619516 ko || +0m02.47s || 13984 ko | +5.72% | +0.53%
0m45.27s | 2544004 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas | 0m42.87s | 2533792 ko || +0m02.40s || 10212 ko | +5.59% | +0.40%
0m45.08s | 2545148 ko | ExtractionOCaml/bedrock2_unsaturated_solinas | 0m42.40s | 2536564 ko || +0m02.67s || 8584 ko | +6.32% | +0.33%
0m42.60s | 2339896 ko | ExtractionOCaml/unsaturated_solinas | 0m40.15s | 2331728 ko || +0m02.45s || 8168 ko | +6.10% | +0.35%
0m42.14s | 2237132 ko | ExtractionOCaml/with_bedrock2_base_conversion | 0m39.92s | 2230688 ko || +0m02.21s || 6444 ko | +5.56% | +0.28%
0m41.95s | 2258216 ko | ExtractionOCaml/bedrock2_dettman_multiplication | 0m39.79s | 2246108 ko || +0m02.16s || 12108 ko | +5.42% | +0.53%
0m41.92s | 2240944 ko | ExtractionOCaml/with_bedrock2_saturated_solinas | 0m39.70s | 2233448 ko || +0m02.21s || 7496 ko | +5.59% | +0.33%
0m41.86s | 2239092 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication | 0m39.56s | 2234396 ko || +0m02.29s || 4696 ko | +5.81% | +0.21%
0m41.57s | 2240068 ko | ExtractionOCaml/bedrock2_saturated_solinas | 0m39.51s | 2231968 ko || +0m02.06s || 8100 ko | +5.21% | +0.36%
0m41.41s | 2234816 ko | ExtractionOCaml/bedrock2_base_conversion | 0m39.16s | 2224784 ko || +0m02.25s || 10032 ko | +5.74% | +0.45%
0m39.09s | 2045652 ko | ExtractionOCaml/base_conversion | 0m36.77s | 1882572 ko || +0m02.32s || 163080 ko | +6.30% | +8.66%
0m39.06s | 2055248 ko | ExtractionOCaml/saturated_solinas | 0m36.32s | 1900876 ko || +0m02.74s || 154372 ko | +7.54% | +8.12%
0m35.49s | 1741752 ko | ExtractionOCaml/perf_unsaturated_solinas | 0m33.30s | 1696000 ko || +0m02.19s || 45752 ko | +6.57% | +2.69%
2m00.22s | 2401976 ko | fiat-bedrock2/src/p384_32.c | 2m02.18s | 2217824 ko || -0m01.96s || 184152 ko | -1.60% | +8.30%
1m59.91s | 2320940 ko | fiat-zig/src/p384_scalar_32.zig | 2m01.71s | 2195356 ko || -0m01.79s || 125584 ko | -1.47% | +5.72%
1m59.14s | 2264508 ko | fiat-c/src/p384_scalar_32.c | 2m01.04s | 2315428 ko || -0m01.90s || -50920 ko | -1.56% | -2.19%
1m58.08s | 2290144 ko | fiat-rust/src/p384_32.rs | 1m59.31s | 2292024 ko || -0m01.23s || -1880 ko | -1.03% | -0.08%
0m42.55s | 2240500 ko | ExtractionOCaml/with_bedrock2_solinas_reduction | 0m40.66s | 2234592 ko || +0m01.89s || 5908 ko | +4.64% | +0.26%
0m40.28s | 1478504 ko | Rewriter/Passes/Arith.vo | 0m41.98s | 1481228 ko || -0m01.69s || -2724 ko | -4.04% | -0.18%
0m34.72s | 1752580 ko | ExtractionOCaml/perf_word_by_word_montgomery | 0m32.93s | 1718100 ko || +0m01.78s || 34480 ko | +5.43% | +2.00%
0m29.64s | 2053032 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml | 0m28.62s | 2049864 ko || +0m01.01s || 3168 ko | +3.56% | +0.15%
0m28.03s | 1945424 ko | ExtractionOCaml/saturated_solinas.ml | 0m26.78s | 1911944 ko || +0m01.25s || 33480 ko | +4.66% | +1.75%
0m17.56s | 320704 ko | fiat-go/64/p434/p434.go | 0m16.35s | 344808 ko || +0m01.20s || -24104 ko | +7.40% | -6.99%
8m04.87s | 2663916 ko | Bedrock/End2End/X25519/GarageDoor.vo | 8m04.02s | 2661980 ko || +0m00.85s || 1936 ko | +0.17% | +0.07%
4m45.51s | 2494088 ko | Bedrock/End2End/X25519/EdwardsXYZT.vo | 4m46.33s | 2489792 ko || -0m00.81s || 4296 ko | -0.28% | +0.17%
3m21.85s | 3498672 ko | Rewriter/Passes/ArithWithCasts.vo | 3m21.48s | 3497152 ko || +0m00.37s || 1520 ko | +0.18% | +0.04%
2m06.54s | 1391724 ko | Bedrock/End2End/X25519/Field25519.vo | 2m06.68s | 1385108 ko || -0m00.14s || 6616 ko | -0.11% | +0.47%
1m59.46s | 2196900 ko | fiat-go/32/p384/p384.go | 1m58.78s | 2251120 ko || +0m00.68s || -54220 ko | +0.57% | -2.40%
1m53.98s | 2478600 ko | Rewriter/Passes/ToFancyWithCasts.vo | 1m53.96s | 2481272 ko || +0m00.01s || -2672 ko | +0.01% | -0.10%
1m32.90s | 1957336 ko | SlowPrimeSynthesisExamples.vo | 1m32.90s | 1951288 ko || +0m00.00s || 6048 ko | +0.00% | +0.30%
1m32.09s | 2070416 ko | Fancy/Barrett256.vo | 1m31.69s | 2070856 ko || +0m00.40s || -440 ko | +0.43% | -0.02%
0m56.65s | 2591660 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.ml | 0m56.04s | 2587220 ko || +0m00.60s || 4440 ko | +1.08% | +0.17%
0m56.59s | 2591872 ko | ExtractionOCaml/bedrock2_fiat_crypto.ml | 0m55.96s | 2588596 ko || +0m00.63s || 3276 ko | +1.12% | +0.12%
0m56.36s | 2597952 ko | ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.ml | 0m55.83s | 2591080 ko || +0m00.53s || 6872 ko | +0.94% | +0.26%
0m56.26s | 834704 ko | Rewriter/RulesProofs.vo | 0m55.87s | 848780 ko || +0m00.39s || -14076 ko | +0.69% | -1.65%
0m56.16s | 2599000 ko | ExtractionJsOfOCaml/bedrock2_fiat_crypto.ml | 0m55.46s | 2588324 ko || +0m00.69s || 10676 ko | +1.26% | +0.41%
0m54.47s | 2480528 ko | ExtractionOCaml/fiat_crypto.ml | 0m53.50s | 2488780 ko || +0m00.96s || -8252 ko | +1.81% | -0.33%
0m50.01s | 1117432 ko | Rewriter/Passes/MultiRetSplit.vo | 0m50.54s | 1117464 ko || -0m00.53s || -32 ko | -1.04% | -0.00%
0m47.05s | 1843584 ko | Fancy/Montgomery256.vo | 0m46.57s | 1882256 ko || +0m00.47s || -38672 ko | +1.03% | -2.05%
0m41.03s | 89412 ko | fiat-go/32/p521/p521.go | 0m41.29s | 90304 ko || -0m00.25s || -892 ko | -0.62% | -0.98%
0m38.73s | 192288 ko | fiat-bedrock2/src/p521_32.c | 0m38.54s | 191252 ko || +0m00.18s || 1036 ko | +0.49% | +0.54%
0m37.96s | 2250044 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml | 0m37.38s | 2262168 ko || +0m00.57s || -12124 ko | +1.55% | -0.53%
0m37.96s | 139000 ko | fiat-json/src/p521_32.json | 0m37.84s | 133668 ko || +0m00.11s || 5332 ko | +0.31% | +3.98%
0m37.78s | 80004 ko | fiat-zig/src/p521_32.zig | 0m37.75s | 84172 ko || +0m00.03s || -4168 ko | +0.07% | -4.95%
0m37.75s | 81832 ko | fiat-rust/src/p521_32.rs | 0m37.84s | 82404 ko || -0m00.09s || -572 ko | -0.23% | -0.69%
0m37.63s | 85588 ko | fiat-java/src/FiatP521.java | 0m37.81s | 83048 ko || -0m00.17s || 2540 ko | -0.47% | +3.05%
0m37.53s | 82628 ko | fiat-c/src/p521_32.c | 0m37.72s | 79408 ko || -0m00.18s || 3220 ko | -0.50% | +4.05%
0m37.25s | 2254188 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml | 0m36.44s | 2212012 ko || +0m00.81s || 42176 ko | +2.22% | +1.90%
0m37.14s | 2254952 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml | 0m36.41s | 2211712 ko || +0m00.73s || 43240 ko | +2.00% | +1.95%
0m36.21s | 2176032 ko | ExtractionOCaml/solinas_reduction.ml | 0m35.30s | 2146952 ko || +0m00.91s || 29080 ko | +2.57% | +1.35%
0m35.12s | 2145588 ko | ExtractionOCaml/word_by_word_montgomery.ml | 0m34.17s | 2116752 ko || +0m00.94s || 28836 ko | +2.78% | +1.36%
0m33.21s | 899056 ko | Rewriter/Passes/MulSplit.vo | 0m33.18s | 895480 ko || +0m00.03s || 3576 ko | +0.09% | +0.39%
0m32.88s | 2166828 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml | 0m33.41s | 2166516 ko || -0m00.52s || 312 ko | -1.58% | +0.01%
0m32.85s | 2164880 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml | 0m33.57s | 2166408 ko || -0m00.71s || -1528 ko | -2.14% | -0.07%
0m32.49s | 1221984 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m32.64s | 1219996 ko || -0m00.14s || 1988 ko | -0.45% | +0.16%
0m32.10s | 2091560 ko | ExtractionOCaml/unsaturated_solinas.ml | 0m31.31s | 2033016 ko || +0m00.79s || 58544 ko | +2.52% | +2.87%
0m30.93s | 1256232 ko | Bedrock/End2End/X25519/GarageDoorTop.vo | 0m31.18s | 1258200 ko || -0m00.25s || -1968 ko | -0.80% | -0.15%
0m30.58s | 2083824 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml | 0m29.69s | 2035044 ko || +0m00.88s || 48780 ko | +2.99% | +2.39%
0m30.07s | 1481064 ko | StandaloneDebuggingExamples.vo | 0m30.16s | 1479316 ko || -0m00.08s || 1748 ko | -0.29% | +0.11%
0m29.85s | 2075580 ko | ExtractionOCaml/bedrock2_base_conversion.ml | 0m29.01s | 2027820 ko || +0m00.83s || 47760 ko | +2.89% | +2.35%
0m29.71s | 2074580 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml | 0m28.90s | 2028104 ko || +0m00.81s || 46476 ko | +2.80% | +2.29%
0m29.71s | 2070300 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml | 0m28.72s | 2048012 ko || +0m00.99s || 22288 ko | +3.44% | +1.08%
0m29.58s | 2070020 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml | 0m28.98s | 2048204 ko || +0m00.59s || 21816 ko | +2.07% | +1.06%
0m29.57s | 2070812 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml | 0m28.64s | 2048732 ko || +0m00.92s || 22080 ko | +3.24% | +1.07%
0m28.56s | 2011744 ko | ExtractionOCaml/dettman_multiplication.ml | 0m27.77s | 1986400 ko || +0m00.78s || 25344 ko | +2.84% | +1.27%
0m27.60s | 1954988 ko | ExtractionOCaml/base_conversion.ml | 0m27.05s | 1939500 ko || +0m00.55s || 15488 ko | +2.03% | +0.79%
0m25.28s | 1299164 ko | PerfTesting/PerfTestSearch.vo | 0m25.45s | 1302744 ko || -0m00.16s || -3580 ko | -0.66% | -0.27%
0m21.63s | 1909120 ko | ExtractionOCaml/perf_unsaturated_solinas.ml | 0m20.75s | 1832892 ko || +0m00.87s || 76228 ko | +4.24% | +4.15%
0m21.54s | 2437392 ko | ExtractionHaskell/with_bedrock2_fiat_crypto.hs | 0m21.34s | 2441484 ko || +0m00.19s || -4092 ko | +0.93% | -0.16%
0m21.40s | 2436356 ko | ExtractionHaskell/bedrock2_fiat_crypto.hs | 0m21.03s | 2438364 ko || +0m00.36s || -2008 ko | +1.75% | -0.08%
0m21.26s | 1899948 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml | 0m21.00s | 1929736 ko || +0m00.26s || -29788 ko | +1.23% | -1.54%
0m20.89s | 1109836 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m20.89s | 1117536 ko || +0m00.00s || -7700 ko | +0.00% | -0.68%
0m20.78s | 2366272 ko | ExtractionHaskell/fiat_crypto.hs | 0m20.58s | 2338376 ko || +0m00.20s || 27896 ko | +0.97% | +1.19%
0m18.71s | 1115184 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m18.71s | 1116872 ko || +0m00.00s || -1688 ko | +0.00% | -0.15%
0m18.52s | 1088300 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m18.43s | 1082908 ko || +0m00.08s || 5392 ko | +0.48% | +0.49%
0m18.02s | 385368 ko | fiat-bedrock2/src/p434_64.c | 0m18.09s | 395184 ko || -0m00.07s || -9816 ko | -0.38% | -2.48%
0m17.58s | 385232 ko | fiat-json/src/p434_64.json | 0m17.61s | 354440 ko || -0m00.03s || 30792 ko | -0.17% | +8.68%
0m17.55s | 2147688 ko | ExtractionHaskell/with_bedrock2_word_by_word_montgomery.hs | 0m17.01s | 2096248 ko || +0m00.53s || 51440 ko | +3.17% | +2.45%
0m17.53s | 332812 ko | fiat-rust/src/p434_64.rs | 0m17.51s | 331704 ko || +0m00.01s || 1108 ko | +0.11% | +0.33%
0m17.42s | 1291228 ko | PerfTesting/PerfTestSearchPattern.vo | 0m17.36s | 1290596 ko || +0m00.06s || 632 ko | +0.34% | +0.04%
0m17.41s | 2162836 ko | ExtractionHaskell/bedrock2_solinas_reduction.hs | 0m17.05s | 2115740 ko || +0m00.35s || 47096 ko | +2.11% | +2.22%
0m17.34s | 2162424 ko | ExtractionHaskell/with_bedrock2_solinas_reduction.hs | 0m17.01s | 2115484 ko || +0m00.32s || 46940 ko | +1.94% | +2.21%
0m17.32s | 319240 ko | fiat-zig/src/p434_64.zig | 0m17.41s | 332084 ko || -0m00.08s || -12844 ko | -0.51% | -3.86%
0m17.29s | 2148704 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs | 0m16.97s | 2095280 ko || +0m00.32s || 53424 ko | +1.88% | +2.54%
0m17.28s | 327216 ko | fiat-c/src/p434_64.c | 0m17.59s | 320604 ko || -0m00.30s || 6612 ko | -1.76% | +2.06%
0m16.94s | 591992 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_32.c | 0m16.89s | 549204 ko || +0m00.05s || 42788 ko | +0.29% | +7.79%
0m16.88s | 1097764 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m16.94s | 1091044 ko || -0m00.06s || 6720 ko | -0.35% | +0.61%
0m16.64s | 2058508 ko | ExtractionHaskell/solinas_reduction.hs | 0m16.27s | 2040460 ko || +0m00.37s || 18048 ko | +2.27% | +0.88%
0m16.64s | 545948 ko | fiat-bedrock2/src/p256_scalar_32.c | 0m16.81s | 582184 ko || -0m00.16s || -36236 ko | -1.01% | -6.22%
0m16.60s | 497404 ko | fiat-java/src/FiatP256Scalar.java | 0m16.49s | 465532 ko || +0m00.11s || 31872 ko | +0.66% | +6.84%
0m16.48s | 2015788 ko | ExtractionHaskell/word_by_word_montgomery.hs | 0m16.14s | 1994928 ko || +0m00.33s || 20860 ko | +2.10% | +1.04%
0m16.48s | 506704 ko | fiat-java/src/FiatSecp256K1MontgomeryScalar.java | 0m15.89s | 508152 ko || +0m00.58s || -1448 ko | +3.71% | -0.28%
0m16.37s | 532700 ko | fiat-bedrock2/src/curve25519_scalar_32.c | 0m16.47s | 561952 ko || -0m00.09s || -29252 ko | -0.60% | -5.20%
0m16.37s | 527676 ko | fiat-json/src/p256_scalar_32.json | 0m16.55s | 550516 ko || -0m00.17s || -22840 ko | -1.08% | -4.14%
0m16.29s | 2055344 ko | ExtractionHaskell/with_bedrock2_unsaturated_solinas.hs | 0m16.02s | 2032356 ko || +0m00.26s || 22988 ko | +1.68% | +1.13%
0m16.26s | 480716 ko | fiat-rust/src/p256_scalar_32.rs | 0m16.35s | 451796 ko || -0m00.08s || 28920 ko | -0.55% | +6.40%
0m16.19s | 494352 ko | fiat-go/32/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go | 0m16.30s | 436412 ko || -0m00.10s || 57940 ko | -0.67% | +13.27%
0m16.16s | 2056824 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs | 0m15.98s | 2031116 ko || +0m00.17s || 25708 ko | +1.12% | +1.26%
0m16.14s | 503672 ko | fiat-bedrock2/src/secp256k1_montgomery_32.c | 0m16.40s | 545704 ko || -0m00.25s || -42032 ko | -1.58% | -7.70%
0m16.04s | 480428 ko | fiat-go/32/p256scalar/p256scalar.go | 0m16.21s | 443600 ko || -0m00.17s || 36828 ko | -1.04% | +8.30%
0m16.04s | 496756 ko | fiat-zig/src/secp256k1_montgomery_scalar_32.zig | 0m16.10s | 501916 ko || -0m00.06s || -5160 ko | -0.37% | -1.02%
0m16.02s | 489128 ko | fiat-zig/src/p256_scalar_32.zig | 0m16.08s | 439752 ko || -0m00.05s || 49376 ko | -0.37% | +11.22%
0m16.01s | 503984 ko | fiat-rust/src/secp256k1_montgomery_scalar_32.rs | 0m16.08s | 440028 ko || -0m00.06s || 63956 ko | -0.43% | +14.53%
0m15.93s | 490732 ko | fiat-c/src/p256_scalar_32.c | 0m15.93s | 480884 ko || +0m00.00s || 9848 ko | +0.00% | +2.04%
0m15.90s | 486180 ko | fiat-java/src/FiatCurve25519Scalar.java | 0m16.31s | 435648 ko || -0m00.40s || 50532 ko | -2.51% | +11.59%
0m15.79s | 495508 ko | fiat-json/src/secp256k1_montgomery_32.json | 0m15.93s | 553532 ko || -0m00.14s || -58024 ko | -0.87% | -10.48%
0m15.78s | 476920 ko | fiat-c/src/secp256k1_montgomery_scalar_32.c | 0m15.82s | 443512 ko || -0m00.04s || 33408 ko | -0.25% | +7.53%
0m15.76s | 1973368 ko | ExtractionHaskell/unsaturated_solinas.hs | 0m15.46s | 1939424 ko || +0m00.29s || 33944 ko | +1.94% | +1.75%
0m15.76s | 488488 ko | fiat-json/src/curve25519_scalar_32.json | 0m16.04s | 542208 ko || -0m00.27s || -53720 ko | -1.74% | -9.90%
0m15.76s | 478272 ko | fiat-zig/src/secp256k1_montgomery_32.zig | 0m15.94s | 496368 ko || -0m00.17s || -18096 ko | -1.12% | -3.64%
0m15.74s | 502548 ko | fiat-rust/src/secp256k1_montgomery_32.rs | 0m15.76s | 496384 ko || -0m00.01s || 6164 ko | -0.12% | +1.24%
0m15.66s | 494864 ko | fiat-go/32/secp256k1montgomery/secp256k1montgomery.go | 0m15.69s | 494948 ko || -0m00.02s || -84 ko | -0.19% | -0.01%
0m15.66s | 440572 ko | fiat-java/src/FiatSecp256K1Montgomery.java | 0m15.74s | 504796 ko || -0m00.08s || -64224 ko | -0.50% | -12.72%
0m15.65s | 473036 ko | fiat-zig/src/curve25519_scalar_32.zig | 0m15.70s | 491508 ko || -0m00.04s || -18472 ko | -0.31% | -3.75%
0m15.57s | 498380 ko | fiat-json/src/secp256k1_montgomery_scalar_32.json | 0m16.14s | 567328 ko || -0m00.57s || -68948 ko | -3.53% | -12.15%
0m15.54s | 1106180 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m15.58s | 1105256 ko || -0m00.04s || 924 ko | -0.25% | +0.08%
0m15.52s | 485872 ko | fiat-go/32/curve25519scalar/curve25519scalar.go | 0m15.53s | 483400 ko || -0m00.00s || 2472 ko | -0.06% | +0.51%
0m15.49s | 485832 ko | fiat-c/src/curve25519_scalar_32.c | 0m15.43s | 450744 ko || +0m00.06s || 35088 ko | +0.38% | +7.78%
0m15.40s | 1126272 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m15.37s | 1128492 ko || +0m00.03s || -2220 ko | +0.19% | -0.19%
0m15.40s | 1980912 ko | ExtractionHaskell/with_bedrock2_dettman_multiplication.hs | 0m15.01s | 1952584 ko || +0m00.39s || 28328 ko | +2.59% | +1.45%
0m15.38s | 507964 ko | fiat-bedrock2/src/p256_32.c | 0m15.49s | 528008 ko || -0m00.10s || -20044 ko | -0.71% | -3.79%
0m15.37s | 477376 ko | fiat-c/src/secp256k1_montgomery_32.c | 0m15.35s | 494284 ko || +0m00.01s || -16908 ko | +0.13% | -3.42%
0m15.34s | 1980092 ko | ExtractionHaskell/bedrock2_dettman_multiplication.hs | 0m15.05s | 1952380 ko || +0m00.28s || 27712 ko | +1.92% | +1.41%
0m15.19s | 1979336 ko | ExtractionHaskell/with_bedrock2_base_conversion.hs | 0m14.79s | 1947364 ko || +0m00.40s || 31972 ko | +2.70% | +1.64%
0m15.16s | 492160 ko | fiat-rust/src/curve25519_scalar_32.rs | 0m16.08s | 483312 ko || -0m00.91s || 8848 ko | -5.72% | +1.83%
0m15.10s | 1979572 ko | ExtractionHaskell/bedrock2_base_conversion.hs | 0m14.77s | 1944640 ko || +0m00.33s || 34932 ko | +2.23% | +1.79%
0m15.03s | 1941608 ko | ExtractionHaskell/with_bedrock2_saturated_solinas.hs | 0m14.13s | 1944032 ko || +0m00.89s || -2424 ko | +6.36% | -0.12%
0m15.02s | 485556 ko | fiat-zig/src/p256_32.zig | 0m15.19s | 485712 ko || -0m00.16s || -156 ko | -1.11% | -0.03%
0m15.00s | 1941740 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs | 0m14.85s | 1945624 ko || +0m00.15s || -3884 ko | +1.01% | -0.19%
0m14.97s | 486152 ko | fiat-rust/src/p256_32.rs | 0m14.85s | 481172 ko || +0m00.12s || 4980 ko | +0.80% | +1.03%
0m14.95s | 476920 ko | fiat-json/src/p256_32.json | 0m15.11s | 516088 ko || -0m00.16s || -39168 ko | -1.05% | -7.58%
0m14.90s | 482212 ko | fiat-go/32/p256/p256.go | 0m15.07s | 477140 ko || -0m00.16s || 5072 ko | -1.12% | +1.06%
0m14.78s | 1881064 ko | ExtractionHaskell/saturated_solinas.hs | 0m14.38s | 1876668 ko || +0m00.39s || 4396 ko | +2.78% | +0.23%
0m14.72s | 491212 ko | fiat-java/src/FiatP256.java | 0m14.80s | 487264 ko || -0m00.08s || 3948 ko | -0.54% | +0.81%
0m14.41s | 1894732 ko | ExtractionHaskell/base_conversion.hs | 0m14.15s | 1859860 ko || +0m00.25s || 34872 ko | +1.83% | +1.87%
0m14.41s | 480184 ko | fiat-c/src/p256_32.c | 0m14.49s | 478564 ko || -0m00.08s || 1620 ko | -0.55% | +0.33%
0m13.98s | 1903704 ko | ExtractionHaskell/dettman_multiplication.hs | 0m14.51s | 1885976 ko || -0m00.52s || 17728 ko | -3.65% | +0.93%
0m13.15s | 1551964 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo | 0m13.08s | 1549676 ko || +0m00.07s || 2288 ko | +0.53% | +0.14%
0m10.83s | 249924 ko | fiat-bedrock2/src/p384_scalar_64.c | 0m10.84s | 248224 ko || -0m00.00s || 1700 ko | -0.09% | +0.68%
0m10.76s | 225128 ko | fiat-json/src/p384_scalar_64.json | 0m10.90s | 250920 ko || -0m00.14s || -25792 ko | -1.28% | -10.27%
0m10.75s | 206312 ko | fiat-rust/src/p384_scalar_64.rs | 0m10.59s | 206860 ko || +0m00.16s || -548 ko | +1.51% | -0.26%
0m10.69s | 199568 ko | fiat-go/64/p384scalar/p384scalar.go | 0m10.70s | 209512 ko || -0m00.00s || -9944 ko | -0.09% | -4.74%
0m10.60s | 204368 ko | fiat-c/src/p384_scalar_64.c | 0m10.54s | 194796 ko || +0m00.06s || 9572 ko | +0.56% | +4.91%
0m10.60s | 204528 ko | fiat-zig/src/p384_scalar_64.zig | 0m10.54s | 181860 ko || +0m00.06s || 22668 ko | +0.56% | +12.46%
0m10.26s | 1005728 ko | BoundsPipeline.vo | 0m10.25s | 999828 ko || +0m00.00s || 5900 ko | +0.09% | +0.59%
0m09.25s | 1247096 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo | 0m09.24s | 1245416 ko || +0m00.00s || 1680 ko | +0.10% | +0.13%
0m09.12s | 238524 ko | fiat-json/src/p384_64.json | 0m09.13s | 231860 ko || -0m00.01s || 6664 ko | -0.10% | +2.87%
0m09.10s | 255620 ko | fiat-bedrock2/src/p384_64.c | 0m09.08s | 247996 ko || +0m00.01s || 7624 ko | +0.22% | +3.07%
0m09.09s | 198100 ko | fiat-zig/src/p384_64.zig | 0m08.66s | 194384 ko || +0m00.42s || 3716 ko | +4.96% | +1.91%
0m09.01s | 362652 ko | fiat-bedrock2/src/p224_32.c | 0m09.01s | 359804 ko || +0m00.00s || 2848 ko | +0.00% | +0.79%
0m09.01s | 212280 ko | fiat-go/64/p384/p384.go | 0m09.09s | 209752 ko || -0m00.08s || 2528 ko | -0.88% | +1.20%
0m08.92s | 204084 ko | fiat-rust/src/p384_64.rs | 0m08.95s | 193392 ko || -0m00.02s || 10692 ko | -0.33% | +5.52%
0m08.89s | 321540 ko | fiat-json/src/p224_32.json | 0m08.82s | 345768 ko || +0m00.07s || -24228 ko | +0.79% | -7.00%
0m08.84s | 190600 ko | fiat-c/src/p384_64.c | 0m08.77s | 192560 ko || +0m00.07s || -1960 ko | +0.79% | -1.01%
0m08.81s | 304848 ko | fiat-rust/src/p224_32.rs | 0m08.76s | 295376 ko || +0m00.05s || 9472 ko | +0.57% | +3.20%
0m08.69s | 297896 ko | fiat-go/32/p224/p224.go | 0m08.77s | 272772 ko || -0m00.08s || 25124 ko | -0.91% | +9.21%
0m08.69s | 281356 ko | fiat-zig/src/p224_32.zig | 0m08.37s | 304612 ko || +0m00.32s || -23256 ko | +3.82% | -7.63%
0m08.68s | 309088 ko | fiat-java/src/FiatP224.java | 0m08.71s | 309156 ko || -0m00.03s || -68 ko | -0.34% | -0.02%
0m08.49s | 291880 ko | fiat-c/src/p224_32.c | 0m08.54s | 294312 ko || -0m00.04s || -2432 ko | -0.58% | -0.82%
0m08.31s | 140296 ko | fiat-json/src/p448_solinas_32.json | 0m08.31s | 138912 ko || +0m00.00s || 1384 ko | +0.00% | +0.99%
0m08.17s | 628572 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo | 0m08.16s | 628844 ko || +0m00.00s || -272 ko | +0.12% | -0.04%
0m08.08s | 997520 ko | PushButtonSynthesis/BaseConversion.vo | 0m07.98s | 996644 ko || +0m00.09s || 876 ko | +1.25% | +0.08%
0m07.95s | 79240 ko | fiat-rust/src/p448_solinas_32.rs | 0m07.90s | 81472 ko || +0m00.04s || -2232 ko | +0.63% | -2.73%
0m07.91s | 73556 ko | fiat-zig/src/p448_solinas_32.zig | 0m07.94s | 81352 ko || -0m00.03s || -7796 ko | -0.37% | -9.58%
0m07.84s | 971052 ko | PushButtonSynthesis/SmallExamples.vo | 0m07.79s | 964172 ko || +0m00.04s || 6880 ko | +0.64% | +0.71%
0m07.83s | 78696 ko | fiat-c/src/p448_solinas_32.c | 0m07.89s | 79452 ko || -0m00.05s || -756 ko | -0.76% | -0.95%
0m07.15s | 1013368 ko | PushButtonSynthesis/Primitives.vo | 0m07.25s | 1014352 ko || -0m00.09s || -984 ko | -1.37% | -0.09%
0m06.38s | 993404 ko | PushButtonSynthesis/SolinasReduction.vo | 0m06.38s | 991732 ko || +0m00.00s || 1672 ko | +0.00% | +0.16%
0m06.27s | 616792 ko | Rewriter/Passes/NoSelect.vo | 0m06.26s | 615456 ko || +0m00.00s || 1336 ko | +0.15% | +0.21%
0m06.26s | 59768 ko | fiat-go/64/p521/p521.go | 0m06.26s | 59896 ko || +0m00.00s || -128 ko | +0.00% | -0.21%
0m05.56s | 75132 ko | fiat-bedrock2/src/p521_64.c | 0m05.58s | 79276 ko || -0m00.02s || -4144 ko | -0.35% | -5.22%
0m05.43s | 1138132 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m05.18s | 1135688 ko || +0m00.25s || 2444 ko | +4.82% | +0.21%
0m05.42s | 1049972 ko | CLI.vo | 0m05.47s | 1047920 ko || -0m00.04s || 2052 ko | -0.91% | +0.19%
0m05.41s | 44772 ko | fiat-c/src/p521_64.c | 0m04.88s | 44296 ko || +0m00.53s || 476 ko | +10.86% | +1.07%
0m05.38s | 44544 ko | fiat-zig/src/p521_64.zig | 0m04.82s | 45056 ko || +0m00.55s || -512 ko | +11.61% | -1.13%
0m05.36s | 61792 ko | fiat-json/src/p521_64.json | 0m05.41s | 62016 ko || -0m00.04s || -224 ko | -0.92% | -0.36%
0m05.30s | 997084 ko | PushButtonSynthesis/BarrettReduction.vo | 0m05.37s | 989500 ko || -0m00.07s || 7584 ko | -1.30% | +0.76%
0m04.81s | 44036 ko | fiat-rust/src/p521_64.rs | 0m05.37s | 44100 ko || -0m00.56s || -64 ko | -10.42% | -0.14%
0m04.41s | 975388 ko | PushButtonSynthesis/DettmanMultiplication.vo | 0m04.32s | 978264 ko || +0m00.08s || -2876 ko | +2.08% | -0.29%
0m04.11s | 1004444 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m04.15s | 1002344 ko || -0m00.04s || 2100 ko | -0.96% | +0.20%
0m04.06s | 980500 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m04.08s | 986200 ko || -0m00.02s || -5700 ko | -0.49% | -0.57%
0m03.98s | 1409300 ko | Bedrock/Everything.vo | 0m04.11s | 1407144 ko || -0m00.13s || 2156 ko | -3.16% | +0.15%
0m03.84s | 1275180 ko | Everything.vo | 0m03.77s | 1273232 ko || +0m00.06s || 1948 ko | +1.85% | +0.15%
0m03.80s | 982844 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m03.77s | 981160 ko || +0m00.02s || 1684 ko | +0.79% | +0.17%
0m03.58s | 997692 ko | Rewriter/PerfTesting/Core.vo | 0m03.58s | 993660 ko || +0m00.00s || 4032 ko | +0.00% | +0.40%
0m03.52s | 1232872 ko | PerfTesting/PerfTestPrint.vo | 0m03.55s | 1231676 ko || -0m00.02s || 1196 ko | -0.84% | +0.09%
0m03.21s | 1008336 ko | StandaloneMonadicUtils.vo | 0m03.16s | 1006476 ko || +0m00.04s || 1860 ko | +1.58% | +0.18%
0m03.14s | 567764 ko | Rewriter/Passes/ArithWithRelaxedCasts.vo | 0m03.20s | 567876 ko || -0m00.06s || -112 ko | -1.87% | -0.01%
0m03.13s | 996084 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m03.09s | 994320 ko || +0m00.04s || 1764 ko | +1.29% | +0.17%
0m03.13s | 1037072 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m03.15s | 1034988 ko || -0m00.02s || 2084 ko | -0.63% | +0.20%
0m03.10s | 1035384 ko | Bedrock/Standalone/StandaloneJsOfOCamlMain.vo | 0m03.05s | 1033372 ko || +0m00.05s || 2012 ko | +1.63% | +0.19%
0m03.08s | 1005344 ko | StandaloneHaskellMain.vo | 0m03.04s | 1002224 ko || +0m00.04s || 3120 ko | +1.31% | +0.31%
0m03.02s | 1037312 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m03.12s | 1035308 ko || -0m00.10s || 2004 ko | -3.20% | +0.19%
0m03.02s | 575508 ko | Rewriter/Passes/AddAssocLeft.vo | 0m02.92s | 577532 ko || +0m00.10s || -2024 ko | +3.42% | -0.35%
0m03.01s | 999364 ko | Bedrock/Field/Stringification/Stringification.vo | 0m03.07s | 997148 ko || -0m00.06s || 2216 ko | -1.95% | +0.22%
0m03.00s | 938636 ko | Bedrock/Field/Translation/Cmd.vo | 0m03.06s | 942412 ko || -0m00.06s || -3776 ko | -1.96% | -0.40%
0m02.98s | 939264 ko | Bedrock/Field/Translation/Func.vo | 0m02.94s | 942940 ko || +0m00.04s || -3676 ko | +1.36% | -0.38%
0m02.97s | 1012892 ko | StandaloneJsOfOCamlMain.vo | 0m03.03s | 1011080 ko || -0m00.05s || 1812 ko | -1.98% | +0.17%
0m02.96s | 1012548 ko | StandaloneOCamlMain.vo | 0m03.05s | 1010580 ko || -0m00.08s || 1968 ko | -2.95% | +0.19%
0m02.92s | 1022664 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.89s | 1021240 ko || +0m00.02s || 1424 ko | +1.03% | +0.13%
0m02.89s | 971328 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m02.86s | 974964 ko || +0m00.03s || -3636 ko | +1.04% | -0.37%
0m02.88s | 995476 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m02.89s | 993312 ko || -0m00.01s || 2164 ko | -0.34% | +0.21%
0m02.88s | 971372 ko | Bedrock/Field/Translation/Parameters/FE310.vo | 0m02.87s | 975136 ko || +0m00.00s || -3764 ko | +0.34% | -0.38%
0m02.86s | 964220 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m02.84s | 967560 ko || +0m00.02s || -3340 ko | +0.70% | -0.34%
0m02.85s | 971540 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m02.88s | 975024 ko || -0m00.02s || -3484 ko | -1.04% | -0.35%
0m02.79s | 100444 ko | fiat-bedrock2/src/p256_scalar_64.c | 0m02.78s | 101444 ko || +0m00.01s || -1000 ko | +0.35% | -0.98%
0m02.76s | 101104 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_64.c | 0m02.71s | 99348 ko || +0m00.04s || 1756 ko | +1.84% | +1.76%
0m02.76s | 88556 ko | fiat-json/src/p256_scalar_64.json | 0m02.76s | 87104 ko || +0m00.00s || 1452 ko | +0.00% | +1.66%
0m02.74s | 87088 ko | fiat-json/src/secp256k1_montgomery_scalar_64.json | 0m02.68s | 89884 ko || +0m00.06s || -2796 ko | +2.23% | -3.11%
0m02.69s | 565928 ko | Rewriter/Passes/FlattenThunkedRects.vo | 0m02.70s | 566044 ko || -0m00.01s || -116 ko | -0.37% | -0.02%
0m02.67s | 71188 ko | fiat-rust/src/p256_scalar_64.rs | 0m02.70s | 72632 ko || -0m00.03s || -1444 ko | -1.11% | -1.98%
0m02.65s | 71568 ko | fiat-c/src/p256_scalar_64.c | 0m02.67s | 70884 ko || -0m00.02s || 684 ko | -0.74% | +0.96%
0m02.65s | 74164 ko | fiat-c/src/secp256k1_montgomery_scalar_64.c | 0m02.65s | 73872 ko || +0m00.00s || 292 ko | +0.00% | +0.39%
0m02.65s | 77536 ko | fiat-go/64/p256scalar/p256scalar.go | 0m02.70s | 77236 ko || -0m00.05s || 300 ko | -1.85% | +0.38%
0m02.65s | 73976 ko | fiat-rust/src/secp256k1_montgomery_scalar_64.rs | 0m02.65s | 73244 ko || +0m00.00s || 732 ko | +0.00% | +0.99%
0m02.65s | 72064 ko | fiat-zig/src/p256_scalar_64.zig | 0m02.67s | 70600 ko || -0m00.02s || 1464 ko | -0.74% | +2.07%
0m02.64s | 78004 ko | fiat-go/64/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go | 0m02.71s | 77792 ko || -0m00.06s || 212 ko | -2.58% | +0.27%
0m02.63s | 70176 ko | fiat-zig/src/secp256k1_montgomery_scalar_64.zig | 0m02.68s | 69524 ko || -0m00.05s || 652 ko | -1.86% | +0.93%
0m02.58s | 57468 ko | fiat-go/64/p448solinas/p448solinas.go | 0m02.57s | 58220 ko || +0m00.01s || -752 ko | +0.38% | -1.29%
0m02.47s | 87764 ko | fiat-json/src/secp256k1_montgomery_64.json | 0m02.40s | 89584 ko || +0m00.07s || -1820 ko | +2.91% | -2.03%
0m02.44s | 98212 ko | fiat-bedrock2/src/secp256k1_montgomery_64.c | 0m02.37s | 97792 ko || +0m00.06s || 420 ko | +2.95% | +0.42%
0m02.42s | 72468 ko | fiat-rust/src/secp256k1_montgomery_64.rs | 0m02.43s | 72696 ko || -0m00.01s || -228 ko | -0.41% | -0.31%
0m02.40s | 74216 ko | fiat-go/64/secp256k1montgomery/secp256k1montgomery.go | 0m02.36s | 73876 ko || +0m00.04s || 340 ko | +1.69% | +0.46%
0m02.39s | 71156 ko | fiat-zig/src/secp256k1_montgomery_64.zig | 0m02.38s | 70956 ko || +0m00.01s || 200 ko | +0.42% | +0.28%
0m02.35s | 70164 ko | fiat-c/src/secp256k1_montgomery_64.c | 0m02.35s | 72620 ko || +0m00.00s || -2456 ko | +0.00% | -3.38%
0m02.30s | 75052 ko | fiat-go/64/curve25519scalar/curve25519scalar.go | 0m02.28s | 72824 ko || +0m00.02s || 2228 ko | +0.87% | +3.05%
0m02.29s | 93720 ko | fiat-bedrock2/src/curve25519_scalar_64.c | 0m02.30s | 93748 ko || -0m00.00s || -28 ko | -0.43% | -0.02%
0m02.27s | 562884 ko | Rewriter/Passes/StripLiteralCasts.vo | 0m02.27s | 564888 ko || +0m00.00s || -2004 ko | +0.00% | -0.35%
0m02.26s | 71596 ko | fiat-rust/src/curve25519_scalar_64.rs | 0m02.29s | 71196 ko || -0m00.03s || 400 ko | -1.31% | +0.56%
0m02.25s | 85432 ko | fiat-json/src/curve25519_scalar_64.json | 0m02.35s | 86952 ko || -0m00.10s || -1520 ko | -4.25% | -1.74%
0m02.25s | 70124 ko | fiat-zig/src/curve25519_scalar_64.zig | 0m02.25s | 68708 ko || +0m00.00s || 1416 ko | +0.00% | +2.06%
0m02.22s | 566620 ko | Rewriter/Passes/UnfoldValueBarrier.vo | 0m02.28s | 566536 ko || -0m00.05s || 84 ko | -2.63% | +0.01%
0m02.19s | 69788 ko | fiat-c/src/curve25519_scalar_64.c | 0m02.21s | 69340 ko || -0m00.02s || 448 ko | -0.90% | +0.64%
0m02.15s | 567208 ko | Rewriter/Passes/ToFancy.vo | 0m02.20s | 567212 ko || -0m00.05s || -4 ko | -2.27% | -0.00%
0m02.13s | 45116 ko | fiat-go/32/curve25519/curve25519.go | 0m02.13s | 43576 ko || +0m00.00s || 1540 ko | +0.00% | +3.53%
0m02.05s | 77620 ko | fiat-bedrock2/src/p448_solinas_64.c | 0m02.07s | 77308 ko || -0m00.02s || 312 ko | -0.96% | +0.40%
0m02.00s | 75804 ko | fiat-bedrock2/src/curve25519_32.c | 0m01.98s | 76816 ko || +0m00.02s || -1012 ko | +1.01% | -1.31%
0m01.97s | 59824 ko | fiat-json/src/p448_solinas_64.json | 0m01.97s | 59328 ko || +0m00.00s || 496 ko | +0.00% | +0.83%
0m01.94s | 43708 ko | fiat-zig/src/p448_solinas_64.zig | 0m01.90s | 42340 ko || +0m00.04s || 1368 ko | +2.10% | +3.23%
0m01.92s | 42480 ko | fiat-c/src/p448_solinas_64.c | 0m01.89s | 41788 ko || +0m00.03s || 692 ko | +1.58% | +1.65%
0m01.92s | 42196 ko | fiat-rust/src/p448_solinas_64.rs | 0m01.92s | 43676 ko || +0m00.00s || -1480 ko | +0.00% | -3.38%
0m01.83s | 85452 ko | fiat-json/src/p224_64.json | 0m01.80s | 88012 ko || +0m00.03s || -2560 ko | +1.66% | -2.90%
0m01.83s | 87112 ko | fiat-json/src/p256_64.json | 0m01.81s | 86432 ko || +0m00.02s || 680 ko | +1.10% | +0.78%
0m01.82s | 96320 ko | fiat-bedrock2/src/p224_64.c | 0m01.87s | 95588 ko || -0m00.05s || 732 ko | -2.67% | +0.76%
0m01.81s | 41768 ko | fiat-zig/src/curve25519_32.zig | 0m01.79s | 41492 ko || +0m00.02s || 276 ko | +1.11% | +0.66%
0m01.81s | 69796 ko | fiat-zig/src/p224_64.zig | 0m01.79s | 69264 ko || +0m00.02s || 532 ko | +1.11% | +0.76%
0m01.80s | 94100 ko | fiat-bedrock2/src/p256_64.c | 0m01.77s | 91532 ko || +0m00.03s || 2568 ko | +1.69% | +2.80%
0m01.80s | 71228 ko | fiat-rust/src/p224_64.rs | 0m01.80s | 68468 ko || +0m00.00s || 2760 ko | +0.00% | +4.03%
0m01.79s | 41952 ko | fiat-java/src/FiatCurve25519.java | 0m01.74s | 42324 ko || +0m00.05s || -372 ko | +2.87% | -0.87%
0m01.78s | 59180 ko | fiat-json/src/curve25519_32.json | 0m01.89s | 60524 ko || -0m00.10s || -1344 ko | -5.82% | -2.22%
0m01.76s | 40544 ko | fiat-c/src/curve25519_32.c | 0m01.76s | 40876 ko || +0m00.00s || -332 ko | +0.00% | -0.81%
0m01.76s | 73780 ko | fiat-go/64/p224/p224.go | 0m01.75s | 73584 ko || +0m00.01s || 196 ko | +0.57% | +0.26%
0m01.76s | 73468 ko | fiat-go/64/p256/p256.go | 0m01.73s | 71364 ko || +0m00.03s || 2104 ko | +1.73% | +2.94%
0m01.75s | 69560 ko | fiat-zig/src/p256_64.zig | 0m01.74s | 70000 ko || +0m00.01s || -440 ko | +0.57% | -0.62%
0m01.74s | 41016 ko | fiat-rust/src/curve25519_32.rs | 0m01.80s | 41968 ko || -0m00.06s || -952 ko | -3.33% | -2.26%
0m01.72s | 68600 ko | fiat-c/src/p224_64.c | 0m01.74s | 69000 ko || -0m00.02s || -400 ko | -1.14% | -0.57%
0m01.70s | 69300 ko | fiat-c/src/p256_64.c | 0m01.68s | 68352 ko || +0m00.02s || 948 ko | +1.19% | +1.38%
0m01.70s | 69860 ko | fiat-rust/src/p256_64.rs | 0m01.74s | 70856 ko || -0m00.04s || -996 ko | -2.29% | -1.40%
0m01.66s | 617724 ko | CompilersTestCases.vo | 0m01.67s | 614372 ko || -0m00.01s || 3352 ko | -0.59% | +0.54%
0m01.43s | 63256 ko | fiat-bedrock2/src/secp256k1_dettman_32.c | 0m01.42s | 60252 ko || +0m00.01s || 3004 ko | +0.70% | +4.98%
0m01.22s | 32000 ko | fiat-go/32/secp256k1dettman/secp256k1dettman.go | 0m01.22s | 31548 ko || +0m00.00s || 452 ko | +0.00% | +1.43%
0m01.22s | 34668 ko | fiat-java/src/FiatSecp256K1Dettman.java | 0m01.22s | 33688 ko || +0m00.00s || 980 ko | +0.00% | +2.90%
0m01.22s | 49040 ko | fiat-json/src/secp256k1_dettman_32.json | 0m01.27s | 48936 ko || -0m00.05s || 104 ko | -3.93% | +0.21%
0m01.22s | 31852 ko | fiat-rust/src/secp256k1_dettman_32.rs | 0m01.21s | 31532 ko || +0m00.01s || 320 ko | +0.82% | +1.01%
0m01.22s | 32152 ko | fiat-zig/src/secp256k1_dettman_32.zig | 0m01.22s | 31720 ko || +0m00.00s || 432 ko | +0.00% | +1.36%
0m01.20s | 33024 ko | fiat-c/src/secp256k1_dettman_32.c | 0m01.21s | 32708 ko || -0m00.01s || 316 ko | -0.82% | +0.96%
0m00.93s | 571828 ko | Rewriter/All.vo | 0m00.98s | 568380 ko || -0m00.04s || 3448 ko | -5.10% | +0.60%
0m00.85s | 456204 ko | Rewriter/Rules.vo | 0m00.86s | 455820 ko || -0m00.01s || 384 ko | -1.16% | +0.08%
0m00.62s | 37376 ko | fiat-go/64/curve25519/curve25519.go | 0m00.62s | 36976 ko || +0m00.00s || 400 ko | +0.00% | +1.08%
0m00.50s | 43752 ko | fiat-bedrock2/src/curve25519_64.c | 0m00.50s | 43516 ko || +0m00.00s || 236 ko | +0.00% | +0.54%
0m00.50s | 40228 ko | fiat-json/src/curve25519_64.json | 0m00.48s | 39756 ko || +0m00.02s || 472 ko | +4.16% | +1.18%
0m00.48s | 31900 ko | fiat-zig/src/curve25519_64.zig | 0m00.48s | 30460 ko || +0m00.00s || 1440 ko | +0.00% | +4.72%
0m00.47s | 110692 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.cmi | 0m00.44s | 110484 ko || +0m00.02s || 208 ko | +6.81% | +0.18%
0m00.46s | 106976 ko | ExtractionOCaml/fiat_crypto.cmi | 0m00.44s | 106972 ko || +0m00.02s || 4 ko | +4.54% | +0.00%
0m00.46s | 31484 ko | fiat-rust/src/curve25519_64.rs | 0m00.47s | 31292 ko || -0m00.00s || 192 ko | -2.12% | +0.61%
0m00.45s | 105408 ko | ExtractionOCaml/base_conversion.cmi | 0m00.43s | 105420 ko || +0m00.02s || -12 ko | +4.65% | -0.01%
0m00.45s | 108780 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi | 0m00.45s | 108964 ko || +0m00.00s || -184 ko | +0.00% | -0.16%
0m00.45s | 107220 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi | 0m00.41s | 107104 ko || +0m00.04s || 116 ko | +9.75% | +0.10%
0m00.45s | 31516 ko | fiat-c/src/curve25519_64.c | 0m00.45s | 31172 ko || +0m00.00s || 344 ko | +0.00% | +1.10%
0m00.44s | 107500 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi | 0m00.47s | 107408 ko || -0m00.02s || 92 ko | -6.38% | +0.08%
0m00.44s | 109688 ko | ExtractionOCaml/bedrock2_fiat_crypto.cmi | 0m00.45s | 109576 ko || -0m00.01s || 112 ko | -2.22% | +0.10%
0m00.44s | 106768 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi | 0m00.45s | 106852 ko || -0m00.01s || -84 ko | -2.22% | -0.07%
0m00.44s | 108500 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi | 0m00.47s | 108388 ko || -0m00.02s || 112 ko | -6.38% | +0.10%
0m00.44s | 104152 ko | ExtractionOCaml/dettman_multiplication.cmi | 0m00.44s | 104116 ko || +0m00.00s || 36 ko | +0.00% | +0.03%
0m00.44s | 105080 ko | ExtractionOCaml/solinas_reduction.cmi | 0m00.43s | 104852 ko || +0m00.01s || 228 ko | +2.32% | +0.21%
0m00.44s | 105748 ko | ExtractionOCaml/unsaturated_solinas.cmi | 0m00.44s | 105948 ko || +0m00.00s || -200 ko | +0.00% | -0.18%
0m00.44s | 106800 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi | 0m00.44s | 106716 ko || +0m00.00s || 84 ko | +0.00% | +0.07%
0m00.44s | 105460 ko | ExtractionOCaml/word_by_word_montgomery.cmi | 0m00.46s | 105440 ko || -0m00.02s || 20 ko | -4.34% | +0.01%
0m00.43s | 106940 ko | ExtractionOCaml/bedrock2_base_conversion.cmi | 0m00.45s | 107388 ko || -0m00.02s || -448 ko | -4.44% | -0.41%
0m00.43s | 104764 ko | ExtractionOCaml/saturated_solinas.cmi | 0m00.44s | 104952 ko || -0m00.01s || -188 ko | -2.27% | -0.17%
0m00.43s | 106872 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi | 0m00.45s | 106864 ko || -0m00.02s || 8 ko | -4.44% | +0.00%
0m00.43s | 108272 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi | 0m00.45s | 108168 ko || -0m00.02s || 104 ko | -4.44% | +0.09%
0m00.43s | 108648 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi | 0m00.44s | 108860 ko || -0m00.01s || -212 ko | -2.27% | -0.19%
0m00.42s | 106768 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi | 0m00.44s | 106768 ko || -0m00.02s || 0 ko | -4.54% | +0.00%
0m00.42s | 107376 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi | 0m00.41s | 107212 ko || +0m00.01s || 164 ko | +2.43% | +0.15%
0m00.41s | 42764 ko | fiat-rust/src/curve25519_solinas_64.rs | 0m00.41s | 42420 ko || +0m00.00s || 344 ko | +0.00% | +0.81%
0m00.40s | 48292 ko | fiat-bedrock2/src/curve25519_solinas_64.c | 0m00.42s | 47448 ko || -0m00.01s || 844 ko | -4.76% | +1.77%
0m00.40s | 42028 ko | fiat-c/src/curve25519_solinas_64.c | 0m00.39s | 41920 ko || +0m00.01s || 108 ko | +2.56% | +0.25%
0m00.40s | 46448 ko | fiat-json/src/curve25519_solinas_64.json | 0m00.43s | 46028 ko || -0m00.02s || 420 ko | -6.97% | +0.91%
0m00.39s | 43412 ko | fiat-go/64/curve25519solinas/curve25519solinas.go | 0m00.42s | 43260 ko || -0m00.02s || 152 ko | -7.14% | +0.35%
0m00.39s | 42768 ko | fiat-zig/src/curve25519_solinas_64.zig | 0m00.40s | 41992 ko || -0m00.01s || 776 ko | -2.50% | +1.84%
0m00.30s | 29992 ko | fiat-go/32/poly1305/poly1305.go | 0m00.29s | 29464 ko || +0m00.01s || 528 ko | +3.44% | +1.79%
0m00.26s | 38380 ko | fiat-bedrock2/src/poly1305_32.c | 0m00.27s | 38752 ko || -0m00.01s || -372 ko | -3.70% | -0.95%
0m00.24s | 34972 ko | fiat-json/src/poly1305_32.json | 0m00.26s | 34748 ko || -0m00.02s || 224 ko | -7.69% | +0.64%
0m00.23s | 34312 ko | fiat-bedrock2/src/secp256k1_dettman_64.c | 0m00.22s | 33788 ko || +0m00.01s || 524 ko | +4.54% | +1.55%
0m00.23s | 28528 ko | fiat-zig/src/poly1305_32.zig | 0m00.22s | 28356 ko || +0m00.01s || 172 ko | +4.54% | +0.60%
0m00.22s | 28592 ko | fiat-go/64/secp256k1dettman/secp256k1dettman.go | 0m00.23s | 28316 ko || -0m00.01s || 276 ko | -4.34% | +0.97%
0m00.22s | 28756 ko | fiat-java/src/FiatPoly1305.java | 0m00.22s | 28688 ko || +0m00.00s || 68 ko | +0.00% | +0.23%
0m00.22s | 28888 ko | fiat-rust/src/poly1305_32.rs | 0m00.22s | 28596 ko || +0m00.00s || 292 ko | +0.00% | +1.02%
0m00.21s | 28244 ko | fiat-c/src/poly1305_32.c | 0m00.22s | 28308 ko || -0m00.01s || -64 ko | -4.54% | -0.22%
0m00.19s | 28908 ko | fiat-json/src/secp256k1_dettman_64.json | 0m00.19s | 28124 ko || +0m00.00s || 784 ko | +0.00% | +2.78%
0m00.18s | 24828 ko | fiat-rust/src/secp256k1_dettman_64.rs | 0m00.19s | 24608 ko || -0m00.01s || 220 ko | -5.26% | +0.89%
0m00.18s | 24692 ko | fiat-zig/src/secp256k1_dettman_64.zig | 0m00.18s | 24300 ko || +0m00.00s || 392 ko | +0.00% | +1.61%
0m00.17s | 61740 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi | 0m00.15s | 61852 ko || +0m00.02s || -112 ko | +13.33% | -0.18%
0m00.17s | 24668 ko | fiat-c/src/secp256k1_dettman_64.c | 0m00.17s | 24356 ko || +0m00.00s || 312 ko | +0.00% | +1.28%
0m00.17s | 29916 ko | fiat-go/64/poly1305/poly1305.go | 0m00.18s | 29392 ko || -0m00.00s || 524 ko | -5.55% | +1.78%
0m00.15s | 61552 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi | 0m00.17s | 61932 ko || -0m00.02s || -380 ko | -11.76% | -0.61%
0m00.13s | 31476 ko | fiat-json/src/poly1305_64.json | 0m00.13s | 31440 ko || +0m00.00s || 36 ko | +0.00% | +0.11%
0m00.12s | 31576 ko | fiat-bedrock2/src/poly1305_64.c | 0m00.12s | 31240 ko || +0m00.00s || 336 ko | +0.00% | +1.07%
0m00.12s | 26580 ko | fiat-c/src/poly1305_64.c | 0m00.12s | 26524 ko || +0m00.00s || 56 ko | +0.00% | +0.21%
0m00.12s | 27276 ko | fiat-rust/src/poly1305_64.rs | 0m00.12s | 26776 ko || +0m00.00s || 500 ko | +0.00% | +1.86%
0m00.12s | 26968 ko | fiat-zig/src/poly1305_64.zig | 0m00.12s | 26948 ko || +0m00.00s || 20 ko | +0.00% | +0.07%
0m00.00s | 4544 ko | ExtractionJsOfOCaml/bedrock2_fiat_crypto.cmi | 0m00.00s | 4664 ko || +0m00.00s || -120 ko | N/A | -2.57%
0m00.00s | 4508 ko | ExtractionJsOfOCaml/fiat_crypto.cmi | 0m00.00s | 4564 ko || +0m00.00s || -56 ko | N/A | -1.22%
0m00.00s | 4444 ko | ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.cmi | 0m00.00s | 4504 ko || +0m00.00s || -60 ko | N/A | -1.33%
```
</p>
</details>
JasonGross
force-pushed
the
more-rewrite-complex
branch
from
ea82a69
to
fd392ca
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
Notes:
Ltac CacheTerm.allow_debug_in_cache ::= constr:(true).to get access to the leftover goalsrepeat ProofsCommonTactics.Compilers.RewriteRules.InterpTactics.handle_reified_rewrite_rules_interp_step (Build_ExprInfoT Compilers.base IdentifiersBasicGENERATED.Compilers.ident Compilers.base_interp (@Compilers.ident_interp)) (Build_ExprExtraInfoT (Build_ExprInfoT Compilers.base IdentifiersBasicGENERATED.Compilers.ident Compilers.base_interp (@Compilers.ident_interp)) Compilers.base_beq (@Compilers.base_interp_beq) Compilers.try_make_base_transport_cps Compilers.baseHasNat Compilers.buildIdent Compilers.toRestrictedIdent Compilers.buildEagerIdent Compilers.invertIdent Compilers.base_default Compilers.reflect_base_beq (@Compilers.reflect_base_interp_beq) Compilers.try_make_base_transport_cps_correct Compilers.baseHasNatCorrect Compilers.toFromRestrictedIdent Compilers.buildInvertIdentCorrect Compilers.buildInterpIdentCorrect Compilers.buildInterpEagerIdentCorrect (@Compilers.ident_interp_Proper)) Compilers.base_interp @Compilers.ident_interp @Compilers.ident_interp_Proper.to play with the code (discovered with More expressive debugging inhandle_reified_rewrite_rules_interprewriter#132)UnderLetsProofs.Compilers.UnderLets.eqv_of_interp_related.to get appropriate context lemmas forProperproofsTiming Diff