Skip to content

Commit

Permalink
Move unfolding of fst and snd earlier (#142)
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 95d7ef4
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 95d7ef4

Please sign in to comment.