Skip to content

Commit

Permalink
Move unfolding of fst and snd earlier
Browse files Browse the repository at this point in the history 
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>
  • Loading branch information
@JasonGross
JasonGross committed Dec 24, 2023
1 parent 1788532 commit 2c58879
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/Rewriter/Rewriter/Reify.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -884,8 +884,8 @@ Module Compilers.
let pident_of_typed_ident := head_reference pident_of_typed_ident in
let pident_type_of_list_arg_types_beq := head_reference pident_type_of_list_arg_types_beq in
let pident_arg_types_of_typed_ident := head_reference pident_arg_types_of_typed_ident in
(eval cbv [expr_to_pattern_and_replacement_unfolded_split $pident_arg_types $pident_of_typed_ident $pident_type_of_list_arg_types_beq $pident_arg_types_of_typed_ident (*reflect_ident_iota*)] in res) in
let res := (debug ("reify_to_pattern_and_replacement_in_context:1") profile eval cbn [fst snd andb pattern.base.relax pattern.base.subst_default pattern.base.subst_default_relax] in res) in
(eval cbv [fst snd expr_to_pattern_and_replacement_unfolded_split $pident_arg_types $pident_of_typed_ident $pident_type_of_list_arg_types_beq $pident_arg_types_of_typed_ident (*reflect_ident_iota*)] in res) in
let res := (debug ("reify_to_pattern_and_replacement_in_context:1") profile eval cbn [andb pattern.base.relax pattern.base.subst_default pattern.base.subst_default_relax] in res) in
let res := change_pattern_base_subst_default_relax res in
let (p, res) := lazy_match! res with
| existT _ ?p ?res => (p, res)
Expand Down

0 comments on commit 2c58879

Please sign in to comment.