Skip to content

Commit

Permalink
Fix DCE/Subst01 to work under lambdas (#1809)
Browse files Browse the repository at this point in the history 
The naive encoding of PHOAS passes that need to produce both
[expr]-like output and data-like output simultaneously involves
exponential blowup.

This commit adds caching of results (and/or intermediates) of a
data-producing PHOAS pass in a tree structure that mimics the
PHOAS expression so that a subsequent pass can consume this tree
and a PHOAS expression to produce a new expression.

More concretely, suppose we are trying to write a pass that is
`expr var1 * expr var2 -> A * expr var3`. We can define an
`expr`-like-tree-structure that (a) doesn't use higher-order
things for `Abs` nodes, and (b) stores `A` at every node. Then we
can write a pass that is `expr var1 * expr var2 -> A * tree-of-A`
and then `expr var1 * expr var2 * tree-of-A -> expr var3` such
that we incur only linear overhead.

See also #1761 and
https://github.com/mit-plv/fiat-crypto/issues/1604#issuecomment-1553341559.

Fixes #1604

<details><summary>Timing Diff</summary>
<p>

```
     After |   Peak Mem | File Name                                                         |     Before |   Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
119m00.41s | 3712896 ko | Total Time / Peak Mem                                             | 117m55.92s | 3712368 ko || +1m04.49s ||       528 ko |   +0.91% |         +0.01%
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
  4m42.94s | 2490632 ko | Bedrock/End2End/X25519/EdwardsXYZT.vo                             |   4m32.25s | 2489304 ko || +0m10.68s ||      1328 ko |   +3.92% |         +0.05%
  2m03.36s | 1846856 ko | fiat-java/src/FiatP384.java                                       |   1m53.28s | 2326980 ko || +0m10.07s ||   -480124 ko |   +8.89% |        -20.63%
  1m52.25s | 1549488 ko | fiat-go/32/p384/p384.go                                           |   1m59.07s | 2250876 ko || -0m06.81s ||   -701388 ko |   -5.72% |        -31.16%
  1m59.32s | 1691084 ko | fiat-json/src/p384_32.json                                        |   1m53.47s | 2444840 ko || +0m05.84s ||   -753756 ko |   +5.15% |        -30.83%
  0m40.01s |  131676 ko | fiat-bedrock2/src/p521_32.c                                       |   0m34.78s |  190408 ko || +0m05.22s ||    -58732 ko |  +15.03% |        -30.84%
  0m37.83s |  121704 ko | fiat-json/src/p521_32.json                                        |   0m34.11s |  133368 ko || +0m03.71s ||    -11664 ko |  +10.90% |         -8.74%
  0m33.87s |   71128 ko | fiat-java/src/FiatP521.java                                       |   0m37.83s |   83008 ko || -0m03.96s ||    -11880 ko |  -10.46% |        -14.31%
  0m05.44s |  504992 ko | MiscCompilerPassesProofs.vo                                       |   0m02.21s |  486644 ko || +0m03.23s ||     18348 ko | +146.15% |         +3.77%
  2m03.41s | 1477044 ko | fiat-bedrock2/src/p384_scalar_32.c                                |   2m01.31s | 2430696 ko || +0m02.09s ||   -953652 ko |   +1.73% |        -39.23%
  0m18.53s |  353076 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_32.c                |   0m16.23s |  549032 ko || +0m02.30s ||   -195956 ko |  +14.17% |        -35.69%
  8m04.15s | 2660384 ko | Bedrock/End2End/X25519/GarageDoor.vo                              |   8m02.97s | 2661316 ko || +0m01.17s ||      -932 ko |   +0.24% |         -0.03%
  2m03.78s | 1869460 ko | fiat-bedrock2/src/p384_32.c                                       |   2m01.97s | 2218064 ko || +0m01.81s ||   -348604 ko |   +1.48% |        -15.71%
  2m01.22s | 1828112 ko | fiat-rust/src/p384_scalar_32.rs                                   |   2m03.12s | 2298944 ko || -0m01.90s ||   -470832 ko |   -1.54% |        -20.48%
  1m58.45s | 1531664 ko | fiat-zig/src/p384_32.zig                                          |   1m59.59s | 2285948 ko || -0m01.14s ||   -754284 ko |   -0.95% |        -32.99%
  1m58.25s | 1796656 ko | fiat-c/src/p384_32.c                                              |   1m59.78s | 2324760 ko || -0m01.53s ||   -528104 ko |   -1.27% |        -22.71%
  1m31.80s | 1943396 ko | SlowPrimeSynthesisExamples.vo                                     |   1m32.99s | 1951328 ko || -0m01.19s ||     -7932 ko |   -1.27% |         -0.40%
  0m54.81s | 2485352 ko | ExtractionOCaml/fiat_crypto.ml                                    |   0m53.16s | 2488988 ko || +0m01.65s ||     -3636 ko |   +3.10% |         -0.14%
  0m52.58s | 3712896 ko | ExtractionOCaml/fiat_crypto                                       |   0m53.81s | 3710436 ko || -0m01.23s ||      2460 ko |   -2.28% |         +0.06%
  0m37.58s | 2239200 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml                     |   0m36.11s | 2262736 ko || +0m01.46s ||    -23536 ko |   +4.07% |         -1.04%
  0m33.57s | 2139444 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml              |   0m32.50s | 2165752 ko || +0m01.07s ||    -26308 ko |   +3.29% |         -1.21%
  0m19.58s |  275340 ko | fiat-bedrock2/src/p434_64.c                                       |   0m18.00s |  395284 ko || +0m01.57s ||   -119944 ko |   +8.77% |        -30.34%
  0m18.18s |  393308 ko | fiat-bedrock2/src/p256_scalar_32.c                                |   0m16.95s |  582384 ko || +0m01.23s ||   -189076 ko |   +7.25% |        -32.46%
  0m17.84s |  368324 ko | fiat-bedrock2/src/curve25519_scalar_32.c                          |   0m16.43s |  561904 ko || +0m01.41s ||   -193580 ko |   +8.58% |        -34.45%
  0m17.71s |  369704 ko | fiat-bedrock2/src/secp256k1_montgomery_32.c                       |   0m16.36s |  545504 ko || +0m01.35s ||   -175800 ko |   +8.25% |        -32.22%
  0m16.51s |  319708 ko | fiat-bedrock2/src/p256_32.c                                       |   0m14.82s |  528056 ko || +0m01.69s ||   -208348 ko |  +11.40% |        -39.45%
  0m16.18s | 2115400 ko | ExtractionHaskell/bedrock2_solinas_reduction.hs                   |   0m17.19s | 2115136 ko || -0m01.01s ||       264 ko |   -5.87% |         +0.01%
  0m11.82s |  162652 ko | fiat-bedrock2/src/p384_scalar_64.c                                |   0m10.80s |  248280 ko || +0m01.01s ||    -85628 ko |   +9.44% |        -34.48%
  5m31.16s | 3213148 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo                   |   5m31.70s | 3175180 ko || -0m00.53s ||     37968 ko |   -0.16% |         +1.19%
  2m07.13s | 1398244 ko | Bedrock/End2End/X25519/Field25519.vo                              |   2m07.52s | 1385812 ko || -0m00.39s ||     12432 ko |   -0.30% |         +0.89%
  2m01.79s | 1839808 ko | fiat-json/src/p384_scalar_32.json                                 |   2m02.58s | 2162300 ko || -0m00.78s ||   -322492 ko |   -0.64% |        -14.91%
  2m01.40s | 1848688 ko | fiat-zig/src/p384_scalar_32.zig                                   |   2m01.53s | 2195116 ko || -0m00.12s ||   -346428 ko |   -0.10% |        -15.78%
  2m01.15s | 1582380 ko | fiat-go/32/p384scalar/p384scalar.go                               |   2m01.06s | 2317700 ko || +0m00.09s ||   -735320 ko |   +0.07% |        -31.72%
  2m00.71s | 1784024 ko | fiat-c/src/p384_scalar_32.c                                       |   2m01.39s | 2315572 ko || -0m00.68s ||   -531548 ko |   -0.56% |        -22.95%
  2m00.48s | 1747580 ko | fiat-java/src/FiatP384Scalar.java                                 |   2m01.02s | 2237456 ko || -0m00.53s ||   -489876 ko |   -0.44% |        -21.89%
  1m59.42s | 1705344 ko | fiat-rust/src/p384_32.rs                                          |   2m00.18s | 2292932 ko || -0m00.76s ||   -587588 ko |   -0.63% |        -25.62%
  1m31.86s | 2103612 ko | Fancy/Barrett256.vo                                               |   1m31.64s | 2070684 ko || +0m00.21s ||     32928 ko |   +0.24% |         +1.59%
  0m59.38s | 3705200 ko | ExtractionOCaml/with_bedrock2_fiat_crypto                         |   0m59.58s | 3712368 ko || -0m00.19s ||     -7168 ko |   -0.33% |         -0.19%
  0m59.22s | 3709680 ko | ExtractionOCaml/bedrock2_fiat_crypto                              |   0m59.27s | 3710700 ko || -0m00.05s ||     -1020 ko |   -0.08% |         -0.02%
  0m56.17s | 2561860 ko | ExtractionJsOfOCaml/bedrock2_fiat_crypto.ml                       |   0m55.77s | 2588396 ko || +0m00.39s ||    -26536 ko |   +0.71% |         -1.02%
  0m56.17s | 2563040 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.ml                      |   0m55.50s | 2587632 ko || +0m00.67s ||    -24592 ko |   +1.20% |         -0.95%
  0m56.16s | 2566832 ko | ExtractionOCaml/bedrock2_fiat_crypto.ml                           |   0m55.39s | 2587172 ko || +0m00.76s ||    -20340 ko |   +1.39% |         -0.78%
  0m56.09s | 2560764 ko | ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.ml                  |   0m55.63s | 2587748 ko || +0m00.46s ||    -26984 ko |   +0.82% |         -1.04%
  0m54.52s | 2487364 ko | ExtractionJsOfOCaml/fiat_crypto.ml                                |   0m53.72s | 2488452 ko || +0m00.80s ||     -1088 ko |   +1.48% |         -0.04%
  0m46.35s | 1864828 ko | Fancy/Montgomery256.vo                                            |   0m46.53s | 1882324 ko || -0m00.17s ||    -17496 ko |   -0.38% |         -0.92%
  0m45.86s | 2633728 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery             |   0m45.38s | 2631336 ko || +0m00.47s ||      2392 ko |   +1.05% |         +0.09%
  0m45.13s | 2628588 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery                  |   0m44.72s | 2631196 ko || +0m00.41s ||     -2608 ko |   +0.91% |         -0.09%
  0m45.01s | 2704032 ko | ExtractionOCaml/bedrock2_solinas_reduction                        |   0m45.25s | 2704460 ko || -0m00.24s ||      -428 ko |   -0.53% |         -0.01%
  0m43.55s | 2689968 ko | ExtractionOCaml/solinas_reduction                                 |   0m43.03s | 2685092 ko || +0m00.51s ||      4876 ko |   +1.20% |         +0.18%
  0m43.13s | 2616752 ko | ExtractionOCaml/word_by_word_montgomery                           |   0m42.49s | 2619388 ko || +0m00.64s ||     -2636 ko |   +1.50% |         -0.10%
  0m42.94s | 2540252 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas                 |   0m42.98s | 2534848 ko || -0m00.03s ||      5404 ko |   -0.09% |         +0.21%
  0m42.46s | 2540704 ko | ExtractionOCaml/bedrock2_unsaturated_solinas                      |   0m42.31s | 2535612 ko || +0m00.14s ||      5092 ko |   +0.35% |         +0.20%
  0m41.09s |   68036 ko | fiat-go/32/p521/p521.go                                           |   0m41.58s |   89984 ko || -0m00.48s ||    -21948 ko |   -1.17% |        -24.39%
  0m40.27s | 2226764 ko | ExtractionOCaml/with_bedrock2_solinas_reduction                   |   0m39.94s | 2235060 ko || +0m00.33s ||     -8296 ko |   +0.82% |         -0.37%
  0m40.21s | 2342848 ko | ExtractionOCaml/unsaturated_solinas                               |   0m40.22s | 2331788 ko || -0m00.00s ||     11060 ko |   -0.02% |         +0.47%
  0m40.04s | 2222156 ko | ExtractionOCaml/with_bedrock2_base_conversion                     |   0m39.81s | 2230200 ko || +0m00.22s ||     -8044 ko |   +0.57% |         -0.36%
  0m39.77s | 2248012 ko | ExtractionOCaml/bedrock2_dettman_multiplication                   |   0m39.86s | 2246008 ko || -0m00.08s ||      2004 ko |   -0.22% |         +0.08%
  0m39.76s | 2227296 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication              |   0m39.23s | 2235188 ko || +0m00.53s ||     -7892 ko |   +1.35% |         -0.35%
  0m39.69s | 2227220 ko | ExtractionOCaml/with_bedrock2_saturated_solinas                   |   0m39.75s | 2234304 ko || -0m00.06s ||     -7084 ko |   -0.15% |         -0.31%
  0m39.22s | 2222396 ko | ExtractionOCaml/bedrock2_base_conversion                          |   0m39.00s | 2225128 ko || +0m00.21s ||     -2732 ko |   +0.56% |         -0.12%
  0m39.10s | 2225812 ko | ExtractionOCaml/bedrock2_saturated_solinas                        |   0m38.87s | 2230904 ko || +0m00.23s ||     -5092 ko |   +0.59% |         -0.22%
  0m38.08s |   65920 ko | fiat-rust/src/p521_32.rs                                          |   0m37.67s |   82364 ko || +0m00.40s ||    -16444 ko |   +1.08% |        -19.96%
  0m37.69s |   69868 ko | fiat-zig/src/p521_32.zig                                          |   0m37.76s |   84304 ko || -0m00.07s ||    -14436 ko |   -0.18% |        -17.12%
  0m37.58s |   63900 ko | fiat-c/src/p521_32.c                                              |   0m37.78s |   79712 ko || -0m00.20s ||    -15812 ko |   -0.52% |        -19.83%
  0m37.16s | 1927432 ko | ExtractionOCaml/dettman_multiplication                            |   0m36.77s | 1927468 ko || +0m00.38s ||       -36 ko |   +1.06% |         -0.00%
  0m36.68s | 2208344 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml               |   0m36.27s | 2209520 ko || +0m00.40s ||     -1176 ko |   +1.13% |         -0.05%
  0m36.58s | 1889596 ko | ExtractionOCaml/base_conversion                                   |   0m35.96s | 1882400 ko || +0m00.61s ||      7196 ko |   +1.72% |         +0.38%
  0m36.54s | 1901292 ko | ExtractionOCaml/saturated_solinas                                 |   0m36.23s | 1900756 ko || +0m00.31s ||       536 ko |   +0.85% |         +0.02%
  0m36.51s | 2207332 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml          |   0m36.53s | 2209884 ko || -0m00.02s ||     -2552 ko |   -0.05% |         -0.11%
  0m35.76s | 2116004 ko | ExtractionOCaml/solinas_reduction.ml                              |   0m35.10s | 2145732 ko || +0m00.65s ||    -29728 ko |   +1.88% |         -1.38%
  0m34.55s | 2143460 ko | ExtractionOCaml/word_by_word_montgomery.ml                        |   0m34.24s | 2117800 ko || +0m00.30s ||     25660 ko |   +0.90% |         +1.21%
  0m33.49s | 2139300 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml                   |   0m34.27s | 2166160 ko || -0m00.78s ||    -26860 ko |   -2.27% |         -1.23%
  0m32.98s | 1695900 ko | ExtractionOCaml/perf_unsaturated_solinas                          |   0m32.89s | 1695528 ko || +0m00.08s ||       372 ko |   +0.27% |         +0.02%
  0m32.90s | 1714104 ko | ExtractionOCaml/perf_word_by_word_montgomery                      |   0m33.02s | 1718156 ko || -0m00.12s ||     -4052 ko |   -0.36% |         -0.23%
  0m32.54s | 1220348 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo                        |   0m32.68s | 1220032 ko || -0m00.14s ||       316 ko |   -0.42% |         +0.02%
  0m31.67s | 2044364 ko | ExtractionOCaml/unsaturated_solinas.ml                            |   0m31.31s | 2032268 ko || +0m00.36s ||     12096 ko |   +1.14% |         +0.59%
  0m30.89s | 1253684 ko | Bedrock/End2End/X25519/GarageDoorTop.vo                           |   0m31.05s | 1254284 ko || -0m00.16s ||      -600 ko |   -0.51% |         -0.04%
  0m30.19s | 1476196 ko | StandaloneDebuggingExamples.vo                                    |   0m29.94s | 1479252 ko || +0m00.25s ||     -3056 ko |   +0.83% |         -0.20%
  0m29.87s | 2063484 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml                |   0m29.64s | 2035996 ko || +0m00.23s ||     27488 ko |   +0.77% |         +1.35%
  0m29.15s | 2051876 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml                  |   0m28.92s | 2028232 ko || +0m00.22s ||     23644 ko |   +0.79% |         +1.16%
  0m29.09s | 2053704 ko | ExtractionOCaml/bedrock2_base_conversion.ml                       |   0m28.75s | 2027468 ko || +0m00.33s ||     26236 ko |   +1.18% |         +1.29%
  0m28.98s | 2056312 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml                |   0m28.86s | 2047824 ko || +0m00.12s ||      8488 ko |   +0.41% |         +0.41%
  0m28.97s | 2057432 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml                     |   0m28.77s | 2048548 ko || +0m00.19s ||      8884 ko |   +0.69% |         +0.43%
  0m28.90s | 2059464 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml                |   0m28.61s | 2049520 ko || +0m00.28s ||      9944 ko |   +1.01% |         +0.48%
  0m28.77s | 2054636 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml           |   0m28.74s | 2048512 ko || +0m00.03s ||      6124 ko |   +0.10% |         +0.29%
  0m28.00s | 1985508 ko | ExtractionOCaml/dettman_multiplication.ml                         |   0m27.78s | 1986744 ko || +0m00.21s ||     -1236 ko |   +0.79% |         -0.06%
  0m27.05s | 1957812 ko | ExtractionOCaml/saturated_solinas.ml                              |   0m26.89s | 1912860 ko || +0m00.16s ||     44952 ko |   +0.59% |         +2.34%
  0m26.98s | 1949468 ko | ExtractionOCaml/base_conversion.ml                                |   0m26.79s | 1938188 ko || +0m00.19s ||     11280 ko |   +0.70% |         +0.58%
  0m25.51s | 1302468 ko | PerfTesting/PerfTestSearch.vo                                     |   0m25.39s | 1303484 ko || +0m00.12s ||     -1016 ko |   +0.47% |         -0.07%
  0m21.37s | 2440932 ko | ExtractionHaskell/with_bedrock2_fiat_crypto.hs                    |   0m21.23s | 2439220 ko || +0m00.14s ||      1712 ko |   +0.65% |         +0.07%
  0m20.99s | 1843996 ko | ExtractionOCaml/perf_unsaturated_solinas.ml                       |   0m21.09s | 1833016 ko || -0m00.10s ||     10980 ko |   -0.47% |         +0.59%
  0m20.95s | 2439784 ko | ExtractionHaskell/bedrock2_fiat_crypto.hs                         |   0m19.96s | 2438120 ko || +0m00.98s ||      1664 ko |   +4.95% |         +0.06%
  0m20.89s | 1114864 ko | PushButtonSynthesis/UnsaturatedSolinas.vo                         |   0m20.95s | 1114468 ko || -0m00.05s ||       396 ko |   -0.28% |         +0.03%
  0m20.84s | 1899964 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml                   |   0m20.86s | 1929696 ko || -0m00.01s ||    -29732 ko |   -0.09% |         -1.54%
  0m20.51s | 2338044 ko | ExtractionHaskell/fiat_crypto.hs                                  |   0m20.59s | 2338048 ko || -0m00.07s ||        -4 ko |   -0.38% |         -0.00%
  0m18.63s | 1116056 ko | PushButtonSynthesis/WordByWordMontgomery.vo                       |   0m18.24s | 1121068 ko || +0m00.39s ||     -5012 ko |   +2.13% |         -0.44%
  0m18.54s | 1076284 ko | Bedrock/End2End/Poly1305/Field1305.vo                             |   0m18.50s | 1076712 ko || +0m00.03s ||      -428 ko |   +0.21% |         -0.03%
  0m18.24s |  234376 ko | fiat-go/64/p434/p434.go                                           |   0m17.55s |  344796 ko || +0m00.68s ||   -110420 ko |   +3.93% |        -32.02%
  0m17.84s |  266772 ko | fiat-rust/src/p434_64.rs                                          |   0m17.62s |  331464 ko || +0m00.21s ||    -64692 ko |   +1.24% |        -19.51%
  0m17.69s |  258268 ko | fiat-json/src/p434_64.json                                        |   0m17.60s |  354448 ko || +0m00.08s ||    -96180 ko |   +0.51% |        -27.13%
  0m17.55s |  238796 ko | fiat-zig/src/p434_64.zig                                          |   0m17.38s |  332096 ko || +0m00.17s ||    -93300 ko |   +0.97% |        -28.09%
  0m17.49s |  239600 ko | fiat-c/src/p434_64.c                                              |   0m17.15s |  320692 ko || +0m00.33s ||    -81092 ko |   +1.98% |        -25.28%
  0m17.34s | 1288544 ko | PerfTesting/PerfTestSearchPattern.vo                              |   0m17.26s | 1289792 ko || +0m00.07s ||     -1248 ko |   +0.46% |         -0.09%
  0m17.09s | 2115764 ko | ExtractionHaskell/with_bedrock2_solinas_reduction.hs              |   0m17.00s | 2115168 ko || +0m00.08s ||       596 ko |   +0.52% |         +0.02%
  0m17.02s | 2096116 ko | ExtractionHaskell/with_bedrock2_word_by_word_montgomery.hs        |   0m16.93s | 2095144 ko || +0m00.08s ||       972 ko |   +0.53% |         +0.04%
  0m16.92s | 1091012 ko | Bedrock/Field/Translation/Proofs/Func.vo                          |   0m16.84s | 1088956 ko || +0m00.08s ||      2056 ko |   +0.47% |         +0.18%
  0m16.85s | 2095212 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs             |   0m17.03s | 2096432 ko || -0m00.17s ||     -1220 ko |   -1.05% |         -0.05%
  0m16.73s |  389052 ko | fiat-java/src/FiatP256Scalar.java                                 |   0m16.57s |  465392 ko || +0m00.16s ||    -76340 ko |   +0.96% |        -16.40%
  0m16.73s |  381468 ko | fiat-json/src/p256_scalar_32.json                                 |   0m16.72s |  550468 ko || +0m00.01s ||   -169000 ko |   +0.05% |        -30.70%
  0m16.69s |  365096 ko | fiat-go/32/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go |   0m16.22s |  436688 ko || +0m00.47s ||    -71592 ko |   +2.89% |        -16.39%
  0m16.68s |  368308 ko | fiat-java/src/FiatSecp256K1MontgomeryScalar.java                  |   0m16.58s |  508480 ko || +0m00.10s ||   -140172 ko |   +0.60% |        -27.56%
  0m16.58s |  335988 ko | fiat-rust/src/p256_scalar_32.rs                                   |   0m16.32s |  452024 ko || +0m00.25s ||   -116036 ko |   +1.59% |        -25.67%
  0m16.45s |  363824 ko | fiat-go/32/p256scalar/p256scalar.go                               |   0m16.36s |  443652 ko || +0m00.08s ||    -79828 ko |   +0.55% |        -17.99%
  0m16.38s | 2041708 ko | ExtractionHaskell/solinas_reduction.hs                            |   0m16.21s | 2038736 ko || +0m00.16s ||      2972 ko |   +1.04% |         +0.14%
  0m16.35s |  368404 ko | fiat-json/src/secp256k1_montgomery_scalar_32.json                 |   0m16.23s |  567364 ko || +0m00.12s ||   -198960 ko |   +0.73% |        -35.06%
  0m16.30s |  328068 ko | fiat-zig/src/p256_scalar_32.zig                                   |   0m16.21s |  439912 ko || +0m00.08s ||   -111844 ko |   +0.55% |        -25.42%
  0m16.26s | 1997856 ko | ExtractionHaskell/word_by_word_montgomery.hs                      |   0m16.14s | 1999068 ko || +0m00.12s ||     -1212 ko |   +0.74% |         -0.06%
  0m16.26s |  312564 ko | fiat-rust/src/secp256k1_montgomery_scalar_32.rs                   |   0m16.01s |  440048 ko || +0m00.25s ||   -127484 ko |   +1.56% |        -28.97%
  0m16.23s |  405148 ko | fiat-json/src/secp256k1_montgomery_32.json                        |   0m15.92s |  553616 ko || +0m00.31s ||   -148468 ko |   +1.94% |        -26.81%
  0m16.18s |  387012 ko | fiat-rust/src/curve25519_scalar_32.rs                             |   0m15.90s |  483240 ko || +0m00.27s ||    -96228 ko |   +1.76% |        -19.91%
  0m16.13s |  324784 ko | fiat-zig/src/secp256k1_montgomery_scalar_32.zig                   |   0m16.10s |  501740 ko || +0m00.02s ||   -176956 ko |   +0.18% |        -35.26%
  0m16.11s |  364752 ko | fiat-zig/src/secp256k1_montgomery_32.zig                          |   0m16.12s |  496352 ko || -0m00.01s ||   -131600 ko |   -0.06% |        -26.51%
  0m16.10s |  373100 ko | fiat-c/src/secp256k1_montgomery_scalar_32.c                       |   0m15.90s |  443492 ko || +0m00.20s ||    -70392 ko |   +1.25% |        -15.87%
  0m16.08s |  363424 ko | fiat-rust/src/secp256k1_montgomery_32.rs                          |   0m15.90s |  496056 ko || +0m00.17s ||   -132632 ko |   +1.13% |        -26.73%
  0m16.07s |  398244 ko | fiat-json/src/curve25519_scalar_32.json                           |   0m16.05s |  542064 ko || +0m00.01s ||   -143820 ko |   +0.12% |        -26.53%
  0m16.06s |  368996 ko | fiat-go/32/curve25519scalar/curve25519scalar.go                   |   0m15.69s |  483624 ko || +0m00.36s ||   -114628 ko |   +2.35% |        -23.70%
  0m16.02s |  375044 ko | fiat-java/src/FiatSecp256K1Montgomery.java                        |   0m15.75s |  504728 ko || +0m00.26s ||   -129684 ko |   +1.71% |        -25.69%
  0m16.01s | 2039252 ko | ExtractionHaskell/with_bedrock2_unsaturated_solinas.hs            |   0m15.95s | 2032812 ko || +0m00.06s ||      6440 ko |   +0.37% |         +0.31%
  0m16.01s |  364588 ko | fiat-go/32/secp256k1montgomery/secp256k1montgomery.go             |   0m15.84s |  495008 ko || +0m00.17s ||   -130420 ko |   +1.07% |        -26.34%
  0m15.86s | 2037300 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs                 |   0m15.19s | 2031872 ko || +0m00.67s ||      5428 ko |   +4.41% |         +0.26%
  0m15.83s |  366152 ko | fiat-zig/src/curve25519_scalar_32.zig                             |   0m15.71s |  491216 ko || +0m00.11s ||   -125064 ko |   +0.76% |        -25.46%
  0m15.72s |  365060 ko | fiat-c/src/curve25519_scalar_32.c                                 |   0m15.42s |  450720 ko || +0m00.30s ||    -85660 ko |   +1.94% |        -19.00%
  0m15.58s |  341664 ko | fiat-java/src/FiatCurve25519Scalar.java                           |   0m16.16s |  435944 ko || -0m00.58s ||    -94280 ko |   -3.58% |        -21.62%
  0m15.57s |  375192 ko | fiat-c/src/secp256k1_montgomery_32.c                              |   0m15.49s |  494320 ko || +0m00.08s ||   -119128 ko |   +0.51% |        -24.09%
  0m15.53s | 1102596 ko | Bedrock/Field/Translation/Proofs/Cmd.vo                           |   0m15.65s | 1105296 ko || -0m00.12s ||     -2700 ko |   -0.76% |         -0.24%
  0m15.50s | 1939896 ko | ExtractionHaskell/unsaturated_solinas.hs                          |   0m15.57s | 1940196 ko || -0m00.07s ||      -300 ko |   -0.44% |         -0.01%
  0m15.50s |  361108 ko | fiat-c/src/p256_scalar_32.c                                       |   0m16.04s |  480596 ko || -0m00.53s ||   -119488 ko |   -3.36% |        -24.86%
  0m15.37s | 1126812 ko | Bedrock/Field/Synthesis/New/Signature.vo                          |   0m15.35s | 1124668 ko || +0m00.01s ||      2144 ko |   +0.13% |         +0.19%
  0m15.28s |  358408 ko | fiat-json/src/p256_32.json                                        |   0m15.18s |  516016 ko || +0m00.09s ||   -157608 ko |   +0.65% |        -30.54%
  0m15.23s |  380476 ko | fiat-zig/src/p256_32.zig                                          |   0m15.25s |  485876 ko || -0m00.01s ||   -105400 ko |   -0.13% |        -21.69%
  0m15.17s |  391176 ko | fiat-rust/src/p256_32.rs                                          |   0m14.97s |  480552 ko || +0m00.19s ||    -89376 ko |   +1.33% |        -18.59%
  0m15.16s |  327160 ko | fiat-go/32/p256/p256.go                                           |   0m15.06s |  476880 ko || +0m00.09s ||   -149720 ko |   +0.66% |        -31.39%
  0m15.10s | 1951784 ko | ExtractionHaskell/with_bedrock2_dettman_multiplication.hs         |   0m15.13s | 1950212 ko || -0m00.03s ||      1572 ko |   -0.19% |         +0.08%
  0m15.02s | 1954488 ko | ExtractionHaskell/bedrock2_dettman_multiplication.hs              |   0m15.01s | 1950572 ko || +0m00.00s ||      3916 ko |   +0.06% |         +0.20%
  0m14.97s |  386420 ko | fiat-java/src/FiatP256.java                                       |   0m14.94s |  487428 ko || +0m00.03s ||   -101008 ko |   +0.20% |        -20.72%
  0m14.94s | 1942204 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs                   |   0m14.78s | 1946752 ko || +0m00.16s ||     -4548 ko |   +1.08% |         -0.23%
  0m14.92s | 1941392 ko | ExtractionHaskell/with_bedrock2_base_conversion.hs                |   0m14.82s | 1944492 ko || +0m00.09s ||     -3100 ko |   +0.67% |         -0.15%
  0m14.85s | 1943860 ko | ExtractionHaskell/with_bedrock2_saturated_solinas.hs              |   0m14.46s | 1943428 ko || +0m00.38s ||       432 ko |   +2.69% |         +0.02%
  0m14.78s | 1942620 ko | ExtractionHaskell/bedrock2_base_conversion.hs                     |   0m14.85s | 1947088 ko || -0m00.07s ||     -4468 ko |   -0.47% |         -0.22%
  0m14.72s |  294600 ko | fiat-c/src/p256_32.c                                              |   0m14.14s |  478440 ko || +0m00.58s ||   -183840 ko |   +4.10% |        -38.42%
  0m14.46s | 1883616 ko | ExtractionHaskell/dettman_multiplication.hs                       |   0m14.48s | 1885612 ko || -0m00.01s ||     -1996 ko |   -0.13% |         -0.10%
  0m14.41s | 1876800 ko | ExtractionHaskell/saturated_solinas.hs                            |   0m14.42s | 1872284 ko || -0m00.00s ||      4516 ko |   -0.06% |         +0.24%
  0m14.25s | 1861548 ko | ExtractionHaskell/base_conversion.hs                              |   0m14.12s | 1862120 ko || +0m00.13s ||      -572 ko |   +0.92% |         -0.03%
  0m13.00s | 1550136 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo               |   0m13.03s | 1549688 ko || -0m00.02s ||       448 ko |   -0.23% |         +0.02%
  0m11.04s |  157128 ko | fiat-go/64/p384scalar/p384scalar.go                               |   0m10.77s |  209908 ko || +0m00.26s ||    -52780 ko |   +2.50% |        -25.14%
  0m10.88s |  187180 ko | fiat-json/src/p384_scalar_64.json                                 |   0m10.96s |  250972 ko || -0m00.08s ||    -63792 ko |   -0.72% |        -25.41%
  0m10.83s |  165252 ko | fiat-rust/src/p384_scalar_64.rs                                   |   0m10.40s |  207016 ko || +0m00.42s ||    -41764 ko |   +4.13% |        -20.17%
  0m10.74s |  162468 ko | fiat-zig/src/p384_scalar_64.zig                                   |   0m10.55s |  182100 ko || +0m00.18s ||    -19632 ko |   +1.80% |        -10.78%
  0m10.64s |  157828 ko | fiat-c/src/p384_scalar_64.c                                       |   0m10.62s |  194572 ko || +0m00.02s ||    -36744 ko |   +0.18% |        -18.88%
  0m09.95s |  171536 ko | fiat-bedrock2/src/p384_64.c                                       |   0m09.13s |  247964 ko || +0m00.81s ||    -76428 ko |   +8.98% |        -30.82%
  0m09.83s |  241628 ko | fiat-bedrock2/src/p224_32.c                                       |   0m09.04s |  359972 ko || +0m00.79s ||   -118344 ko |   +8.73% |        -32.87%
  0m09.36s |  172540 ko | fiat-go/64/p384/p384.go                                           |   0m09.03s |  209672 ko || +0m00.33s ||    -37132 ko |   +3.65% |        -17.70%
  0m09.30s | 1245696 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo              |   0m09.06s | 1247292 ko || +0m00.24s ||     -1596 ko |   +2.64% |         -0.12%
  0m09.26s |  990120 ko | BoundsPipeline.vo                                                 |   0m10.17s | 1001900 ko || -0m00.91s ||    -11780 ko |   -8.94% |         -1.17%
  0m09.22s |  196596 ko | fiat-json/src/p384_64.json                                        |   0m09.07s |  231996 ko || +0m00.15s ||    -35400 ko |   +1.65% |        -15.25%
  0m09.16s |  168928 ko | fiat-rust/src/p384_64.rs                                          |   0m08.94s |  193548 ko || +0m00.22s ||    -24620 ko |   +2.46% |        -12.72%
  0m09.02s |  148804 ko | fiat-zig/src/p384_64.zig                                          |   0m09.06s |  194724 ko || -0m00.04s ||    -45920 ko |   -0.44% |        -23.58%
  0m08.95s |  221716 ko | fiat-rust/src/p224_32.rs                                          |   0m08.80s |  295280 ko || +0m00.14s ||    -73564 ko |   +1.70% |        -24.91%
  0m08.91s |  270756 ko | fiat-json/src/p224_32.json                                        |   0m08.94s |  345988 ko || -0m00.02s ||    -75232 ko |   -0.33% |        -21.74%
  0m08.90s |  211804 ko | fiat-zig/src/p224_32.zig                                          |   0m08.61s |  304584 ko || +0m00.29s ||    -92780 ko |   +3.36% |        -30.46%
  0m08.89s |  152768 ko | fiat-c/src/p384_64.c                                              |   0m08.89s |  193164 ko || +0m00.00s ||    -40396 ko |   +0.00% |        -20.91%
  0m08.89s |  224580 ko | fiat-java/src/FiatP224.java                                       |   0m08.75s |  308952 ko || +0m00.14s ||    -84372 ko |   +1.60% |        -27.30%
  0m08.87s |  208792 ko | fiat-go/32/p224/p224.go                                           |   0m08.71s |  273008 ko || +0m00.15s ||    -64216 ko |   +1.83% |        -23.52%
  0m08.34s |  216488 ko | fiat-c/src/p224_32.c                                              |   0m08.48s |  294192 ko || -0m00.14s ||    -77704 ko |   -1.65% |        -26.41%
  0m08.30s |  130604 ko | fiat-json/src/p448_solinas_32.json                                |   0m08.28s |  138976 ko || +0m00.02s ||     -8372 ko |   +0.24% |         -6.02%
  0m08.08s |  997024 ko | PushButtonSynthesis/BaseConversion.vo                             |   0m08.01s |  998652 ko || +0m00.07s ||     -1628 ko |   +0.87% |         -0.16%
  0m07.97s |   63136 ko | fiat-rust/src/p448_solinas_32.rs                                  |   0m07.94s |   81796 ko || +0m00.02s ||    -18660 ko |   +0.37% |        -22.81%
  0m07.87s |   63124 ko | fiat-c/src/p448_solinas_32.c                                      |   0m07.89s |   79116 ko || -0m00.01s ||    -15992 ko |   -0.25% |        -20.21%
  0m07.76s |  971804 ko | PushButtonSynthesis/SmallExamples.vo                              |   0m07.72s |  963916 ko || +0m00.04s ||      7888 ko |   +0.51% |         +0.81%
  0m07.66s |   66928 ko | fiat-zig/src/p448_solinas_32.zig                                  |   0m07.94s |   81272 ko || -0m00.28s ||    -14344 ko |   -3.52% |        -17.64%
  0m07.15s | 1014500 ko | PushButtonSynthesis/Primitives.vo                                 |   0m07.14s | 1014268 ko || +0m00.01s ||       232 ko |   +0.14% |         +0.02%
  0m06.44s |  998480 ko | PushButtonSynthesis/SolinasReduction.vo                           |   0m06.41s |  991736 ko || +0m00.03s ||      6744 ko |   +0.46% |         +0.68%
  0m06.41s |   50340 ko | fiat-go/64/p521/p521.go                                           |   0m05.58s |   60156 ko || +0m00.83s ||     -9816 ko |  +14.87% |        -16.31%
  0m05.84s |   64284 ko | fiat-bedrock2/src/p521_64.c                                       |   0m05.52s |   79608 ko || +0m00.32s ||    -15324 ko |   +5.79% |        -19.24%
  0m05.47s |   40672 ko | fiat-rust/src/p521_64.rs                                          |   0m05.41s |   44064 ko || +0m00.05s ||     -3392 ko |   +1.10% |         -7.69%
  0m05.46s |   39792 ko | fiat-zig/src/p521_64.zig                                          |   0m05.39s |   45116 ko || +0m00.07s ||     -5324 ko |   +1.29% |        -11.80%
  0m05.42s |   40516 ko | fiat-c/src/p521_64.c                                              |   0m05.29s |   44236 ko || +0m00.12s ||     -3720 ko |   +2.45% |         -8.40%
  0m05.41s | 1128812 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo                 |   0m05.43s | 1137752 ko || -0m00.01s ||     -8940 ko |   -0.36% |         -0.78%
  0m05.41s |  990868 ko | PushButtonSynthesis/BarrettReduction.vo                           |   0m05.41s |  994048 ko || +0m00.00s ||     -3180 ko |   +0.00% |         -0.31%
  0m05.39s | 1050088 ko | CLI.vo                                                            |   0m05.46s | 1047924 ko || -0m00.07s ||      2164 ko |   -1.28% |         +0.20%
  0m05.38s |   57020 ko | fiat-json/src/p521_64.json                                        |   0m05.37s |   61652 ko || +0m00.00s ||     -4632 ko |   +0.18% |         -7.51%
  0m04.39s |  978576 ko | PushButtonSynthesis/DettmanMultiplication.vo                      |   0m04.42s |  978280 ko || -0m00.03s ||       296 ko |   -0.67% |         +0.03%
  0m04.14s | 1005104 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo           |   0m04.12s | 1002340 ko || +0m00.01s ||      2764 ko |   +0.48% |         +0.27%
  0m04.09s |  986744 ko | PushButtonSynthesis/SaturatedSolinas.vo                           |   0m03.87s |  988116 ko || +0m00.21s ||     -1372 ko |   +5.68% |         -0.13%
  0m04.05s | 1408000 ko | Bedrock/Everything.vo                                             |   0m04.05s | 1407508 ko || +0m00.00s ||       492 ko |   +0.00% |         +0.03%
  0m03.79s |  985896 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo                   |   0m03.79s |  979824 ko || +0m00.00s ||      6072 ko |   +0.00% |         +0.61%
  0m03.62s | 1274284 ko | Everything.vo                                                     |   0m03.80s | 1273676 ko || -0m00.17s ||       608 ko |   -4.73% |         +0.04%
  0m03.56s |  995868 ko | Rewriter/PerfTesting/Core.vo                                      |   0m03.53s |  993696 ko || +0m00.03s ||      2172 ko |   +0.84% |         +0.21%
  0m03.52s | 1232320 ko | PerfTesting/PerfTestPrint.vo                                      |   0m03.54s | 1231900 ko || -0m00.02s ||       420 ko |   -0.56% |         +0.03%
  0m03.19s | 1006604 ko | StandaloneMonadicUtils.vo                                         |   0m03.17s | 1006356 ko || +0m00.02s ||       248 ko |   +0.63% |         +0.02%
  0m03.18s |   71672 ko | fiat-bedrock2/src/p256_scalar_64.c                                |   0m02.76s |  101396 ko || +0m00.42s ||    -29724 ko |  +15.21% |        -29.31%
  0m03.17s | 1033928 ko | Bedrock/Standalone/StandaloneJsOfOCamlMain.vo                     |   0m03.06s | 1033420 ko || +0m00.10s ||       508 ko |   +3.59% |         +0.04%
  0m03.13s |  997304 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo          |   0m03.08s |  994328 ko || +0m00.04s ||      2976 ko |   +1.62% |         +0.29%
  0m03.11s | 1035436 ko | Bedrock/Standalone/StandaloneHaskellMain.vo                       |   0m03.12s | 1035108 ko || -0m00.01s ||       328 ko |   -0.32% |         +0.03%
  0m03.10s |   72376 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_64.c                |   0m02.73s |   99420 ko || +0m00.37s ||    -27044 ko |  +13.55% |        -27.20%
  0m03.07s | 1035720 ko | Bedrock/Standalone/StandaloneOCamlMain.vo                         |   0m03.06s | 1035304 ko || +0m00.00s ||       416 ko |   +0.32% |         +0.04%
  0m03.07s | 1002468 ko | StandaloneHaskellMain.vo                                          |   0m03.03s | 1001988 ko || +0m00.04s ||       480 ko |   +1.32% |         +0.04%
  0m03.06s |  997784 ko | Bedrock/Field/Stringification/Stringification.vo                  |   0m03.09s |  997184 ko || -0m00.02s ||       600 ko |   -0.97% |         +0.06%
  0m03.02s | 1011104 ko | StandaloneOCamlMain.vo                                            |   0m03.03s | 1010576 ko || -0m00.00s ||       528 ko |   -0.33% |         +0.05%
  0m03.01s |  942960 ko | Bedrock/Field/Translation/Cmd.vo                                  |   0m03.01s |  944416 ko || +0m00.00s ||     -1456 ko |   +0.00% |         -0.15%
  0m02.98s |  943312 ko | Bedrock/Field/Translation/Func.vo                                 |   0m02.96s |  942944 ko || +0m00.02s ||       368 ko |   +0.67% |         +0.03%
  0m02.97s | 1011444 ko | StandaloneJsOfOCamlMain.vo                                        |   0m02.99s | 1011032 ko || -0m00.02s ||       412 ko |   -0.66% |         +0.04%
  0m02.94s | 1021728 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo                       |   0m02.97s | 1021312 ko || -0m00.03s ||       416 ko |   -1.01% |         +0.04%
  0m02.91s |  975208 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo                |   0m02.84s |  974984 ko || +0m00.07s ||       224 ko |   +2.46% |         +0.02%
  0m02.91s |  975304 ko | Bedrock/Field/Translation/Parameters/FE310.vo                     |   0m02.93s |  975164 ko || -0m00.02s ||       140 ko |   -0.68% |         +0.01%
  0m02.89s |  967920 ko | Bedrock/Field/Translation/Parameters/Defaults.vo                  |   0m02.84s |  967592 ko || +0m00.05s ||       328 ko |   +1.76% |         +0.03%
  0m02.86s |  975308 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo                |   0m02.91s |  975076 ko || -0m00.05s ||       232 ko |   -1.71% |         +0.02%
  0m02.84s |  993860 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo                         |   0m02.84s |  991728 ko || +0m00.00s ||      2132 ko |   +0.00% |         +0.21%
  0m02.79s |   70364 ko | fiat-bedrock2/src/secp256k1_montgomery_64.c                       |   0m02.47s |   97868 ko || +0m00.31s ||    -27504 ko |  +12.95% |        -28.10%
  0m02.78s |   62840 ko | fiat-go/64/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go |   0m02.65s |   77260 ko || +0m00.12s ||    -14420 ko |   +4.90% |        -18.66%
  0m02.77s |   78500 ko | fiat-json/src/secp256k1_montgomery_scalar_64.json                 |   0m02.82s |   89688 ko || -0m00.04s ||    -11188 ko |   -1.77% |        -12.47%
  0m02.76s |   61360 ko | fiat-go/64/p256scalar/p256scalar.go                               |   0m02.71s |   76844 ko || +0m00.04s ||    -15484 ko |   +1.84% |        -20.14%
  0m02.75s |   48676 ko | fiat-go/64/p448solinas/p448solinas.go                             |   0m02.58s |   58008 ko || +0m00.16s ||     -9332 ko |   +6.58% |        -16.08%
  0m02.75s |   80092 ko | fiat-json/src/p256_scalar_64.json                                 |   0m02.73s |   86968 ko || +0m00.02s ||     -6876 ko |   +0.73% |         -7.90%
  0m02.71s |   61136 ko | fiat-rust/src/p256_scalar_64.rs                                   |   0m02.71s |   72876 ko || +0m00.00s ||    -11740 ko |   +0.00% |        -16.10%
  0m02.71s |   58288 ko | fiat-zig/src/p256_scalar_64.zig                                   |   0m02.67s |   70452 ko || +0m00.04s ||    -12164 ko |   +1.49% |        -17.26%
  0m02.70s |   65392 ko | fiat-rust/src/secp256k1_montgomery_scalar_64.rs                   |   0m02.73s |   73348 ko || -0m00.02s ||     -7956 ko |   -1.09% |        -10.84%
  0m02.68s |   60804 ko | fiat-c/src/p256_scalar_64.c                                       |   0m02.64s |   70656 ko || +0m00.04s ||     -9852 ko |   +1.51% |        -13.94%
  0m02.67s |   61096 ko | fiat-c/src/secp256k1_montgomery_scalar_64.c                       |   0m02.70s |   73624 ko || -0m00.03s ||    -12528 ko |   -1.11% |        -17.01%
  0m02.67s |   59312 ko | fiat-zig/src/secp256k1_montgomery_scalar_64.zig                   |   0m02.66s |   69360 ko || +0m00.00s ||    -10048 ko |   +0.37% |        -14.48%
  0m02.63s |   68304 ko | fiat-bedrock2/src/curve25519_scalar_64.c                          |   0m02.32s |   93616 ko || +0m00.31s ||    -25312 ko |  +13.36% |        -27.03%
  0m02.54s |   59212 ko | fiat-go/64/secp256k1montgomery/secp256k1montgomery.go             |   0m02.44s |   73720 ko || +0m00.10s ||    -14508 ko |   +4.09% |        -19.67%
  0m02.51s |   78528 ko | fiat-json/src/secp256k1_montgomery_64.json                        |   0m02.48s |   89620 ko || +0m00.02s ||    -11092 ko |   +1.20% |        -12.37%
  0m02.44s |   60300 ko | fiat-rust/src/secp256k1_montgomery_64.rs                          |   0m02.41s |   72620 ko || +0m00.02s ||    -12320 ko |   +1.24% |        -16.96%
  0m02.42s |   59944 ko | fiat-zig/src/secp256k1_montgomery_64.zig                          |   0m02.40s |   70968 ko || +0m00.02s ||    -11024 ko |   +0.83% |        -15.53%
  0m02.40s |   61632 ko | fiat-bedrock2/src/p448_solinas_64.c                               |   0m02.08s |   77056 ko || +0m00.31s ||    -15424 ko |  +15.38% |        -20.01%
  0m02.37s |   61400 ko | fiat-c/src/secp256k1_montgomery_64.c                              |   0m02.38s |   72852 ko || -0m00.00s ||    -11452 ko |   -0.42% |        -15.71%
  0m02.34s |   59256 ko | fiat-go/64/curve25519scalar/curve25519scalar.go                   |   0m02.28s |   72580 ko || +0m00.06s ||    -13324 ko |   +2.63% |        -18.35%
  0m02.33s |   59672 ko | fiat-bedrock2/src/curve25519_32.c                                 |   0m01.97s |   76516 ko || +0m00.36s ||    -16844 ko |  +18.27% |        -22.01%
  0m02.29s |   57408 ko | fiat-zig/src/curve25519_scalar_64.zig                             |   0m02.26s |   68600 ko || +0m00.03s ||    -11192 ko |   +1.32% |        -16.31%
  0m02.27s |   76824 ko | fiat-json/src/curve25519_scalar_64.json                           |   0m02.27s |   86484 ko || +0m00.00s ||     -9660 ko |   +0.00% |        -11.16%
  0m02.27s |   59708 ko | fiat-rust/src/curve25519_scalar_64.rs                             |   0m02.27s |   70816 ko || +0m00.00s ||    -11108 ko |   +0.00% |        -15.68%
  0m02.23s |   60616 ko | fiat-c/src/curve25519_scalar_64.c                                 |   0m02.23s |   69008 ko || +0m00.00s ||     -8392 ko |   +0.00% |        -12.16%
  0m02.17s |   69392 ko | fiat-bedrock2/src/p224_64.c                                       |   0m01.85s |   95744 ko || +0m00.31s ||    -26352 ko |  +17.29% |        -27.52%
  0m02.14s |   38524 ko | fiat-go/32/curve25519/curve25519.go                               |   0m02.16s |   43904 ko || -0m00.02s ||     -5380 ko |   -0.92% |        -12.25%
  0m02.08s |   67380 ko | fiat-bedrock2/src/p256_64.c                                       |   0m01.79s |   91572 ko || +0m00.29s ||    -24192 ko |  +16.20% |        -26.41%
  0m01.99s |   55216 ko | fiat-json/src/p448_solinas_64.json                                |   0m01.88s |   59420 ko || +0m00.11s ||     -4204 ko |   +5.85% |         -7.07%
  0m01.94s |   39112 ko | fiat-zig/src/p448_solinas_64.zig                                  |   0m01.94s |   42288 ko || +0m00.00s ||     -3176 ko |   +0.00% |         -7.51%
  0m01.93s |   38224 ko | fiat-c/src/p448_solinas_64.c                                      |   0m01.90s |   42056 ko || +0m00.03s ||     -3832 ko |   +1.57% |         -9.11%
  0m01.92s |   58352 ko | fiat-go/64/p224/p224.go                                           |   0m01.73s |   73288 ko || +0m00.18s ||    -14936 ko |  +10.98% |        -20.37%
  0m01.92s |   38508 ko | fiat-rust/src/p448_solinas_64.rs                                  |   0m01.92s |   43824 ko || +0m00.00s ||     -5316 ko |   +0.00% |        -12.13%
  0m01.90s |   63580 ko | fiat-go/64/p256/p256.go                                           |   0m01.75s |   71360 ko || +0m00.14s ||     -7780 ko |   +8.57% |        -10.90%
  0m01.84s |   77768 ko | fiat-json/src/p224_64.json                                        |   0m01.83s |   87924 ko || +0m00.01s ||    -10156 ko |   +0.54% |        -11.55%
  0m01.84s |   61112 ko | fiat-zig/src/p224_64.zig                                          |   0m01.80s |   69264 ko || +0m00.04s ||     -8152 ko |   +2.22% |        -11.76%
  0m01.82s |   54540 ko | fiat-json/src/curve25519_32.json                                  |   0m01.85s |   60820 ko || -0m00.03s ||     -6280 ko |   -1.62% |        -10.32%
  0m01.81s |   75152 ko | fiat-json/src/p256_64.json                                        |   0m01.80s |   86432 ko || +0m00.01s ||    -11280 ko |   +0.55% |        -13.05%
  0m01.81s |   37200 ko | fiat-rust/src/curve25519_32.rs                                    |   0m01.78s |   42116 ko || +0m00.03s ||     -4916 ko |   +1.68% |        -11.67%
  0m01.80s |   37780 ko | fiat-c/src/curve25519_32.c                                        |   0m01.76s |   40824 ko || +0m00.04s ||     -3044 ko |   +2.27% |         -7.45%
  0m01.80s |   61280 ko | fiat-rust/src/p224_64.rs                                          |   0m01.79s |   68664 ko || +0m00.01s ||     -7384 ko |   +0.55% |        -10.75%
  0m01.80s |   36760 ko | fiat-zig/src/curve25519_32.zig                                    |   0m01.77s |   41496 ko || +0m00.03s ||     -4736 ko |   +1.69% |        -11.41%
  0m01.76s |   59756 ko | fiat-rust/src/p256_64.rs                                          |   0m01.75s |   70532 ko || +0m00.01s ||    -10776 ko |   +0.57% |        -15.27%
  0m01.75s |   59104 ko | fiat-c/src/p224_64.c                                              |   0m01.77s |   69336 ko || -0m00.02s ||    -10232 ko |   -1.12% |        -14.75%
  0m01.75s |   37028 ko | fiat-java/src/FiatCurve25519.java                                 |   0m01.76s |   42592 ko || -0m00.01s ||     -5564 ko |   -0.56% |        -13.06%
  0m01.74s |   58728 ko | fiat-zig/src/p256_64.zig                                          |   0m01.73s |   69820 ko || +0m00.01s ||    -11092 ko |   +0.57% |        -15.88%
  0m01.71s |   53640 ko | fiat-bedrock2/src/secp256k1_dettman_32.c                          |   0m01.43s |   60396 ko || +0m00.28s ||     -6756 ko |  +19.58% |        -11.18%
  0m01.70s |  614616 ko | CompilersTestCases.vo                                             |   0m01.68s |  614336 ko || +0m00.02s ||       280 ko |   +1.19% |         +0.04%
  0m01.68s |   58576 ko | fiat-c/src/p256_64.c                                              |   0m01.69s |   68252 ko || -0m00.01s ||     -9676 ko |   -0.59% |        -14.17%
  0m01.31s |   45844 ko | fiat-json/src/secp256k1_dettman_32.json                           |   0m01.32s |   48572 ko || -0m00.01s ||     -2728 ko |   -0.75% |         -5.61%
  0m01.24s |   30080 ko | fiat-c/src/secp256k1_dettman_32.c                                 |   0m01.21s |   32832 ko || +0m00.03s ||     -2752 ko |   +2.47% |         -8.38%
  0m01.24s |   32540 ko | fiat-java/src/FiatSecp256K1Dettman.java                           |   0m01.25s |   33892 ko || -0m00.01s ||     -1352 ko |   -0.80% |         -3.98%
  0m01.24s |   30760 ko | fiat-rust/src/secp256k1_dettman_32.rs                             |   0m01.22s |   31400 ko || +0m00.02s ||      -640 ko |   +1.63% |         -2.03%
  0m01.23s |   31472 ko | fiat-go/32/secp256k1dettman/secp256k1dettman.go                   |   0m01.22s |   31672 ko || +0m00.01s ||      -200 ko |   +0.81% |         -0.63%
  0m01.23s |   30428 ko | fiat-zig/src/secp256k1_dettman_32.zig                             |   0m01.22s |   31768 ko || +0m00.01s ||     -1340 ko |   +0.81% |         -4.21%
  0m00.81s |  523364 ko | MiscCompilerPassesProofsExtra.vo                                  |   0m00.85s |  522920 ko || -0m00.03s ||       444 ko |   -4.70% |         +0.08%
  0m00.74s |  472868 ko | MiscCompilerPasses.vo                                             |   0m00.74s |  445980 ko || +0m00.00s ||     26888 ko |   +0.00% |         +6.02%
  0m00.67s |   32768 ko | fiat-go/64/curve25519/curve25519.go                               |   0m00.60s |   36860 ko || +0m00.07s ||     -4092 ko |  +11.66% |        -11.10%
  0m00.64s |   39160 ko | fiat-bedrock2/src/curve25519_64.c                                 |   0m00.50s |   43428 ko || +0m00.14s ||     -4268 ko |  +28.00% |         -9.82%
  0m00.53s |   37788 ko | fiat-json/src/curve25519_64.json                                  |   0m00.51s |   39780 ko || +0m00.02s ||     -1992 ko |   +3.92% |         -5.00%
  0m00.50s |   39980 ko | fiat-bedrock2/src/curve25519_solinas_64.c                         |   0m00.42s |   47692 ko || +0m00.08s ||     -7712 ko |  +19.04% |        -16.17%
  0m00.48s |   29052 ko | fiat-zig/src/curve25519_64.zig                                    |   0m00.46s |   30704 ko || +0m00.01s ||     -1652 ko |   +4.34% |         -5.38%
  0m00.47s |  106268 ko | ExtractionOCaml/unsaturated_solinas.cmi                           |   0m00.41s |  105940 ko || +0m00.06s ||       328 ko |  +14.63% |         +0.30%
  0m00.47s |   29480 ko | fiat-rust/src/curve25519_64.rs                                    |   0m00.46s |   31568 ko || +0m00.00s ||     -2088 ko |   +2.17% |         -6.61%
  0m00.46s |  108404 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi                  |   0m00.46s |  108860 ko || +0m00.00s ||      -456 ko |   +0.00% |         -0.41%
  0m00.46s |  107356 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi               |   0m00.42s |  106764 ko || +0m00.04s ||       592 ko |   +9.52% |         +0.55%
  0m00.46s |  108988 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi             |   0m00.44s |  108080 ko || +0m00.02s ||       908 ko |   +4.54% |         +0.84%
  0m00.45s |  107644 ko | ExtractionOCaml/bedrock2_base_conversion.cmi                      |   0m00.42s |  106976 ko || +0m00.03s ||       668 ko |   +7.14% |         +0.62%
  0m00.45s |  106864 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi               |   0m00.43s |  107592 ko || +0m00.02s ||      -728 ko |   +4.65% |         -0.67%
  0m00.45s |  107208 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi                    |   0m00.41s |  106724 ko || +0m00.04s ||       484 ko |   +9.75% |         +0.45%
  0m00.45s |  107600 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi              |   0m00.45s |  108388 ko || +0m00.00s ||      -788 ko |   +0.00% |         -0.72%
  0m00.45s |  105328 ko | ExtractionOCaml/dettman_multiplication.cmi                        |   0m00.40s |  104160 ko || +0m00.04s ||      1168 ko |  +12.49% |         +1.12%
  0m00.45s |  103952 ko | ExtractionOCaml/saturated_solinas.cmi                             |   0m00.42s |  104872 ko || +0m00.03s ||      -920 ko |   +7.14% |         -0.87%
  0m00.45s |  107276 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi               |   0m00.44s |  106912 ko || +0m00.01s ||       364 ko |   +2.27% |         +0.34%
  0m00.45s |  104348 ko | ExtractionOCaml/word_by_word_montgomery.cmi                       |   0m00.42s |  105376 ko || +0m00.03s ||     -1028 ko |   +7.14% |         -0.97%
  0m00.45s |   29520 ko | fiat-c/src/curve25519_64.c                                        |   0m00.45s |   31108 ko || +0m00.00s ||     -1588 ko |   +0.00% |         -5.10%
  0m00.44s |  105044 ko | ExtractionOCaml/base_conversion.cmi                               |   0m00.37s |  105320 ko || +0m00.07s ||      -276 ko |  +18.91% |         -0.26%
  0m00.44s |  103868 ko | ExtractionOCaml/solinas_reduction.cmi                             |   0m00.40s |  104720 ko || +0m00.03s ||      -852 ko |   +9.99% |         -0.81%
  0m00.44s |  107368 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi          |   0m00.43s |  107640 ko || +0m00.01s ||      -272 ko |   +2.32% |         -0.25%
  0m00.44s |  110880 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.cmi                     |   0m00.46s |  110604 ko || -0m00.02s ||       276 ko |   -4.34% |         +0.24%
  0m00.44s |  107632 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi         |   0m00.44s |  108480 ko || +0m00.00s ||      -848 ko |   +0.00% |         -0.78%
  0m00.44s |   37168 ko | fiat-go/64/curve25519solinas/curve25519solinas.go                 |   0m00.41s |   43492 ko || +0m00.03s ||     -6324 ko |   +7.31% |        -14.54%
  0m00.43s |  107460 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi                    |   0m00.42s |  106644 ko || +0m00.01s ||       816 ko |   +2.38% |         +0.76%
  0m00.43s |  107832 ko | ExtractionOCaml/fiat_crypto.cmi                                   |   0m00.49s |  107092 ko || -0m00.06s ||       740 ko |  -12.24% |         +0.69%
  0m00.42s |  110252 ko | ExtractionOCaml/bedrock2_fiat_crypto.cmi                          |   0m00.45s |  109560 ko || -0m00.03s ||       692 ko |   -6.66% |         +0.63%
  0m00.42s |  107596 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi                 |   0m00.41s |  107244 ko || +0m00.01s ||       352 ko |   +2.43% |         +0.32%
  0m00.42s |   36584 ko | fiat-rust/src/curve25519_solinas_64.rs                            |   0m00.41s |   42544 ko || +0m00.01s ||     -5960 ko |   +2.43% |        -14.00%
  0m00.42s |   37132 ko | fiat-zig/src/curve25519_solinas_64.zig                            |   0m00.41s |   42192 ko || +0m00.01s ||     -5060 ko |   +2.43% |        -11.99%
  0m00.41s |   36464 ko | fiat-c/src/curve25519_solinas_64.c                                |   0m00.41s |   41988 ko || +0m00.00s ||     -5524 ko |   +0.00% |        -13.15%
  0m00.39s |   38620 ko | fiat-json/src/curve25519_solinas_64.json                          |   0m00.42s |   45928 ko || -0m00.02s ||     -7308 ko |   -7.14% |        -15.91%
  0m00.38s |  322220 ko | Language/TreeCaching.vo                                           |    N/A     |    N/A     || +0m00.38s ||    322220 ko |        ∞ |              ∞
  0m00.35s |   35256 ko | fiat-bedrock2/src/poly1305_32.c                                   |   0m00.25s |   38708 ko || +0m00.09s ||     -3452 ko |  +39.99% |         -8.91%
  0m00.31s |   32200 ko | fiat-bedrock2/src/secp256k1_dettman_64.c                          |   0m00.23s |   33888 ko || +0m00.07s ||     -1688 ko |  +34.78% |         -4.98%
  0m00.29s |   27912 ko | fiat-go/32/poly1305/poly1305.go                                   |   0m00.29s |   29464 ko || +0m00.00s ||     -1552 ko |   +0.00% |         -5.26%
  0m00.26s |   27348 ko | fiat-go/64/secp256k1dettman/secp256k1dettman.go                   |   0m00.23s |   28376 ko || +0m00.03s ||     -1028 ko |  +13.04% |         -3.62%
  0m00.24s |   33520 ko | fiat-json/src/poly1305_32.json                                    |   0m00.24s |   34772 ko || +0m00.00s ||     -1252 ko |   +0.00% |         -3.60%
  0m00.22s |   26908 ko | fiat-zig/src/poly1305_32.zig                                      |   0m00.23s |   28128 ko || -0m00.01s ||     -1220 ko |   -4.34% |         -4.33%
  0m00.21s |   27332 ko | fiat-c/src/poly1305_32.c                                          |   0m00.21s |   28264 ko || +0m00.00s ||      -932 ko |   +0.00% |         -3.29%
  0m00.21s |   27112 ko | fiat-java/src/FiatPoly1305.java                                   |   0m00.22s |   28688 ko || -0m00.01s ||     -1576 ko |   -4.54% |         -5.49%
  0m00.21s |   27048 ko | fiat-rust/src/poly1305_32.rs                                      |   0m00.22s |   28276 ko || -0m00.01s ||     -1228 ko |   -4.54% |         -4.34%
  0m00.19s |   28456 ko | fiat-go/64/poly1305/poly1305.go                                   |   0m00.17s |   29408 ko || +0m00.01s ||      -952 ko |  +11.76% |         -3.23%
  0m00.18s |   27912 ko | fiat-json/src/secp256k1_dettman_64.json                           |   0m00.19s |   28184 ko || -0m00.01s ||      -272 ko |   -5.26% |         -0.96%
  0m00.18s |   23976 ko | fiat-rust/src/secp256k1_dettman_64.rs                             |   0m00.18s |   24544 ko || +0m00.00s ||      -568 ko |   +0.00% |         -2.31%
  0m00.17s |   62552 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi                      |   0m00.16s |   61744 ko || +0m00.01s ||       808 ko |   +6.25% |         +1.30%
  0m00.17s |   60964 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi                  |   0m00.17s |   61880 ko || +0m00.00s ||      -916 ko |   +0.00% |         -1.48%
  0m00.17s |   24108 ko | fiat-c/src/secp256k1_dettman_64.c                                 |   0m00.17s |   24416 ko || +0m00.00s ||      -308 ko |   +0.00% |         -1.26%
  0m00.17s |   24124 ko | fiat-zig/src/secp256k1_dettman_64.zig                             |   0m00.18s |   24224 ko || -0m00.00s ||      -100 ko |   -5.55% |         -0.41%
  0m00.16s |   31212 ko | fiat-bedrock2/src/poly1305_64.c                                   |   0m00.12s |   31312 ko || +0m00.04s ||      -100 ko |  +33.33% |         -0.31%
  0m00.13s |   30208 ko | fiat-json/src/poly1305_64.json                                    |   0m00.11s |   31244 ko || +0m00.02s ||     -1036 ko |  +18.18% |         -3.31%
  0m00.12s |   25872 ko | fiat-c/src/poly1305_64.c                                          |   0m00.12s |   26464 ko || +0m00.00s ||      -592 ko |   +0.00% |         -2.23%
  0m00.12s |   25840 ko | fiat-rust/src/poly1305_64.rs                                      |   0m00.13s |   26816 ko || -0m00.01s ||      -976 ko |   -7.69% |         -3.63%
  0m00.12s |   25336 ko | fiat-zig/src/poly1305_64.zig                                      |   0m00.12s |   26644 ko || +0m00.00s ||     -1308 ko |   +0.00% |         -4.90%
  0m00.00s |    4500 ko | ExtractionJsOfOCaml/bedrock2_fiat_crypto.cmi                      |   0m00.00s |    4380 ko || +0m00.00s ||       120 ko |   N/A    |         +2.73%
  0m00.00s |    4676 ko | ExtractionJsOfOCaml/fiat_crypto.cmi                               |   0m00.00s |    4440 ko || +0m00.00s ||       236 ko |   N/A    |         +5.31%
  0m00.00s |    4680 ko | ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.cmi                 |   0m00.00s |    4444 ko || +0m00.00s ||       236 ko |   N/A    |         +5.31%

```
</p>
</details>
  • Loading branch information
@JasonGross
JasonGross authored Jan 23, 2024
1 parent 16b3666 commit 922fb56
Show file tree
Hide file tree
Showing 5 changed files with 226 additions and 104 deletions.
10 changes: 1 addition & 9 deletions src/BoundsPipeline.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -660,12 +660,6 @@ Module Pipeline.
(E : Expr t)
: DebugM (Expr t)
:= (E <- DoRewrite E;
(* Note that DCE evaluates the expr with two different [var]
arguments, and so results in a pipeline that is 2x slower
unless we pass through a uniformly concrete [var] type
first *)
dlet_nd e := ToFlat E in
let E := FromFlat e in
E <- if with_subst01 return DebugM (Expr t)
then wrap_debug_rewrite ("subst01 for " ++ descr) (Subst01.Subst01 ident.is_comment) E
else if with_dead_code_elimination return DebugM (Expr t)
Expand All @@ -675,8 +669,6 @@ Module Pipeline.
then wrap_debug_rewrite ("LetBindReturn for " ++ descr) (UnderLets.LetBindReturn (@ident.is_var_like)) E
else Debug.ret E;
E <- DoRewrite E; (* after inlining, see if any new rewrite redexes are available *)
dlet_nd e := ToFlat E in
let E := FromFlat e in
E <- if with_dead_code_elimination
then wrap_debug_rewrite ("DCE after " ++ descr) (DeadCodeElimination.EliminateDead ident.is_comment) E
else Debug.ret E;
Expand Down Expand Up @@ -1150,7 +1142,7 @@ Module Pipeline.
first [ progress destruct_head'_and
| progress cbv [Classes.base Classes.ident Classes.ident_interp Classes.base_interp Classes.exprInfo] in *
| progress intros
| progress rewrite_strat repeat topdown hints interp
| progress rewrite_strat repeat topdown choice (hints interp_extra) (hints interp)
| solve [ typeclasses eauto with nocore interp_extra wf_extra ]
| solve [ typeclasses eauto ]
| break_innermost_match_step
Expand Down
70 changes: 70 additions & 0 deletions src/Language/TreeCaching.v
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
(** * Tree Caching for PHOAS Expressions *)
(** The naive encoding of PHOAS passes that need to produce both
[expr]-like output and data-like output simultaneously involves
exponential blowup.
This file allows caching of results (and/or intermediates) of a
data-producing PHOAS pass in a tree structure that mimics the
PHOAS expression so that a subsequent pass can consume this tree
and a PHOAS expression to produce a new expression.
More concretely, suppose we are trying to write a pass that is
[expr var1 * expr var2 -> A * expr var3]. We can define an
[expr]-like-tree-structure that (a) doesn't use higher-order
things for [Abs] nodes, and (b) stores [A] at every node. Then we
can write a pass that is [expr var1 * expr var2 -> A * tree-of-A]
and then [expr var1 * expr var2 * tree-of-A -> expr var3] such
that we incur only linear overhead.
See also
%\href{https://github.com/mit-plv/fiat-crypto/issues/1604#issuecomment-1553341559}{mit-plv/fiat-crypto\#1604 with option (2)}%
#<a href=https://github.com/mit-plv/fiat-crypto/issues/1604##issuecomment-1553341559">mit-plv/fiat-crypto##1604 with option (2)</a>#
and
%\href{https://github.com/mit-plv/fiat-crypto/issues/1761}{mit-plv/fiat-crypto\#1761}%
#<a href=https://github.com/mit-plv/fiat-crypto/issues/1761#">mit-plv/fiat-crypto##1761</a>#. *)

Require Import Rewriter.Language.Language.

Module Compilers.
Export Language.Compilers.
Local Set Boolean Equality Schemes.
Local Set Decidable Equality Schemes.

Module tree_nd.
Section with_result.
Context {base_type : Type}.
Local Notation type := (type base_type).
Context {ident : type -> Type}
{result : Type}.
Local Notation expr := (@expr.expr base_type ident).

Inductive tree : Type :=
| Ident (r : result) : tree
| Var (r : result) : tree
| Abs (r : result) (f : option tree) : tree
| App (r : result) (f : option tree) (x : option tree) : tree
| LetIn (r : result) (x : option tree) (f : option tree) : tree
.
End with_result.
Global Arguments tree result : clear implicits, assert.
End tree_nd.

Module tree.
Section with_result.
Context {base_type : Type}.
Local Notation type := (type base_type).
Context {ident : type -> Type}
{result : type -> Type}.
Local Notation expr := (@expr.expr base_type ident).

Inductive tree : type -> Type :=
| Ident {t} (r : result t) : tree t
| Var {t} (r : result t) : tree t
| Abs {s d} (r : result (s -> d)) (f : option (tree d)) : tree (s -> d)
| App {s d} (r : result d) (f : option (tree (s -> d))) (x : option (tree s)) : tree d
| LetIn {A B} (r : result B) (x : option (tree A)) (f : option (tree B)) : tree B
.
End with_result.
Global Arguments tree {base_type} {result} t, {base_type} result t : assert.
End tree.
End Compilers.
147 changes: 92 additions & 55 deletions src/MiscCompilerPasses.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,14 @@ Require Import Coq.MSets.MSetPositive.
Require Import Coq.FSets.FMapPositive.
Require Import Crypto.Util.ListUtil Coq.Lists.List.
Require Import Rewriter.Language.Language.
Require Import Crypto.Util.LetIn.
Require Import Crypto.Util.Notations.
Require Import Crypto.Language.TreeCaching.
Import ListNotations. Local Open Scope Z_scope.

Module Compilers.
Export Language.Compilers.
Export Language.TreeCaching.Compilers.
Import invert_expr.

Module Subst01.
Expand All @@ -33,6 +36,8 @@ Module Compilers.
(** some identifiers, like [comment], might always be live *)
(is_ident_always_live : forall t, ident t -> bool).
Local Notation expr := (@expr.expr base_type ident).
(* [option t] is "is the let-in here live?", meaningless elsewhere; the thunk is for debugging *)
Local Notation tree := (@tree_nd.tree (option t * (unit -> positive * list (positive * t)))).
(** N.B. This does not work well when let-binders are not at top-level *)
Fixpoint contains_always_live_ident {var} (dummy : forall t, var t) {t} (e : @expr var t)
: bool
Expand All @@ -46,28 +51,39 @@ Module Compilers.
| expr.LetIn tx tC ex eC
=> contains_always_live_ident dummy ex || contains_always_live_ident dummy (eC (dummy _))
end%bool.
Definition meaningless : option t * (unit -> positive * list (positive * t)) := (None, (fun 'tt => (1%positive, []%list))).
Global Opaque meaningless.
Fixpoint compute_live_counts' {t} (e : @expr (fun _ => positive) t) (cur_idx : positive) (live : PositiveMap.t _)
: positive * PositiveMap.t _
: positive * PositiveMap.t _ * option tree
:= match e with
| expr.Var t v => (cur_idx, PositiveMap_incr v live)
| expr.Ident t idc => (cur_idx, live)
| expr.Var t v
=> let '(idx, live) := (cur_idx, PositiveMap_incr v live) in
(idx, live, Some (tree_nd.Var meaningless))
| expr.Ident t idc
=> let '(idx, live) := (cur_idx, live) in
(idx, live, Some (tree_nd.Ident meaningless))
| expr.App s d f x
=> let '(idx, live) := @compute_live_counts' _ f cur_idx live in
let '(idx, live) := @compute_live_counts' _ x idx live in
(idx, live)
=> let '(idx, live, f_tree) := @compute_live_counts' _ f cur_idx live in
let '(idx, live, x_tree) := @compute_live_counts' _ x idx live in
(idx, live, Some (tree_nd.App meaningless f_tree x_tree))
| expr.Abs s d f
=> let '(idx, live) := @compute_live_counts' _ (f cur_idx) (Pos.succ cur_idx) live in
(cur_idx, live)
=> let '(idx, live, f_tree) := @compute_live_counts' _ (f cur_idx) (Pos.succ cur_idx) live in
(idx, live, Some (tree_nd.Abs meaningless f_tree))
| expr.LetIn tx tC ex eC
=> let '(idx, live) := @compute_live_counts' tC (eC cur_idx) (Pos.succ cur_idx) live in
=> let '(idx, live, C_tree) := @compute_live_counts' tC (eC cur_idx) (Pos.succ cur_idx) live in
let live := if contains_always_live_ident (fun _ => cur_idx (* dummy *)) ex
then PositiveMap_incr_always_live cur_idx live
else live in
if PositiveMap.mem cur_idx live
then @compute_live_counts' tx ex idx live
else (idx, live)
let debug_info := fun 'tt => (Pos.succ cur_idx, PositiveMap.elements live) in
match PositiveMap.find cur_idx live with
| Some x_count
=> let '(x_idx, x_live, x_tree) := @compute_live_counts' tx ex idx live in
(x_idx, x_live, Some (tree_nd.LetIn (Some x_count, debug_info) x_tree C_tree))
| None
=> (idx, live, Some (tree_nd.LetIn (None, debug_info) None C_tree))
end
end%bool.
Definition compute_live_counts {t} e : PositiveMap.t _ := snd (@compute_live_counts' t e 1 (PositiveMap.empty _)).
Definition compute_live_counts {t} e : option tree := snd (@compute_live_counts' t e 1 (PositiveMap.empty _)).
Definition ComputeLiveCounts {t} (e : expr.Expr t) := compute_live_counts (e _).

Section with_var.
Expand All @@ -79,36 +95,61 @@ Module Compilers.
in extraction *)
Context (doing_subst_debug : forall T1 T2, T1 -> (unit -> T2) -> T1)
{var : type -> Type}
(should_subst : t -> bool)
(live : PositiveMap.t t).
Fixpoint subst0n' {t} (e : @expr (@expr var) t) (cur_idx : positive)
: positive * @expr var t
(should_subst : t -> bool).
(** When [live] is [None], we don't inline anything, just
dropping [var]. This is required for preventing blowup
in inlining lets in unused [LetIn]-bound expressions.
*)
Fixpoint subst0n (live : option tree) {t} (e : @expr (@expr var) t)
: @expr var t
:= match e with
| expr.Var t v => (cur_idx, v)
| expr.Ident t idc => (cur_idx, expr.Ident idc)
| expr.Var t v => v
| expr.Ident t idc => expr.Ident idc
| expr.App s d f x
=> let '(idx, f') := @subst0n' _ f cur_idx in
let '(idx, x') := @subst0n' _ x idx in
(idx, expr.App f' x')
=> let '(f_live, x_live)
:= match live with
| Some (tree_nd.App _ f_live x_live) => (f_live, x_live)
| _ => (None, None)
end%core in
let f' := @subst0n f_live _ f in
let x' := @subst0n x_live _ x in
expr.App f' x'
| expr.Abs s d f
=> (cur_idx, expr.Abs (fun v => snd (@subst0n' _ (f (expr.Var v)) (Pos.succ cur_idx))))
=> let f_tree
:= match live with
| Some (tree_nd.Abs _ f_tree) => f_tree
| _ => None
end in
expr.Abs (fun v => @subst0n f_tree _ (f (expr.Var v)))
| expr.LetIn tx tC ex eC
=> let '(idx, ex') := @subst0n' tx ex cur_idx in
let eC' := fun v => snd (@subst0n' tC (eC v) (Pos.succ cur_idx)) in
if match PositiveMap.find cur_idx live with
| Some n => should_subst n
| None => true
end
then (Pos.succ cur_idx, eC' (doing_subst_debug _ _ ex' (fun 'tt => (Pos.succ cur_idx, PositiveMap.elements live))))
else (Pos.succ cur_idx, expr.LetIn ex' (fun v => eC' (expr.Var v)))
=> match live with
| Some (tree_nd.LetIn (x_count, debug_info) x_tree C_tree)
=> let ex' := @subst0n x_tree tx ex in
let eC' := fun v => @subst0n C_tree tC (eC v) in
if match x_count with
| Some n => should_subst n
| None => true
end
then eC' (doing_subst_debug _ _ ex' debug_info)
else expr.LetIn ex' (fun v => eC' (expr.Var v))
| _
=> let ex' := @subst0n None tx ex in
let eC' := fun v => @subst0n None tC (eC v) in
expr.LetIn ex' (fun v => eC' (expr.Var v))
end
end.

Definition subst0n {t} e : expr t
:= snd (@subst0n' t e 1).
End with_var.

Definition Subst0n (doing_subst_debug : forall T1 T2, T1 -> (unit -> T2) -> T1) (should_subst : t -> bool) {t} (e : expr.Expr t) : expr.Expr t
:= fun var => subst0n doing_subst_debug should_subst (ComputeLiveCounts e) (e _).
Section with_transport.
Context {try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type}
{exprDefault : forall var, @DefaultValue.type.base.DefaultT type (@expr var)}.
(** We pass through [Flat] to ensure that the passed in
[Expr] only gets invoked at a single [var] type *)
Definition Subst0n (doing_subst_debug : forall T1 T2, T1 -> (unit -> T2) -> T1) (should_subst : t -> bool) {t} (E : expr.Expr t) : expr.Expr t
:= dlet_nd e := GeneralizeVar.ToFlat E in
let E := GeneralizeVar.FromFlat e in
fun var => subst0n doing_subst_debug should_subst (ComputeLiveCounts E) (E _).
End with_transport.
End with_ident.
End with_counter.

Expand All @@ -122,34 +163,30 @@ Module Compilers.
| more => false
end.

Definition Subst01 {base_type ident} (is_ident_always_live : forall t, ident t -> bool) {t} (e : expr.Expr t) : expr.Expr t
:= @Subst0n _ one incr (fun _ => more) base_type ident is_ident_always_live (fun _ _ x _ => x) should_subst t e.
Definition Subst01
{base_type ident}
{try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type}
{exprDefault : forall var, @DefaultValue.type.base.DefaultT _ _}
(is_ident_always_live : forall t, ident t -> bool)
{t} (e : expr.Expr t) : expr.Expr t
:= @Subst0n _ one incr (fun _ => more) base_type ident is_ident_always_live try_make_transport_base_type_cps exprDefault (fun _ _ x _ => x) should_subst t e.
End for_01.
End Subst01.

Module DeadCodeElimination.
Section with_ident.
Context {base_type : Type}.
Local Notation type := (type.type base_type).
Context {ident : type -> Type}
(is_ident_always_live : forall t, ident t -> bool).
Local Notation expr := (@expr.expr base_type ident).

Definition OUGHT_TO_BE_UNUSED {T1 T2} (v : T1) (v' : T2) := v.
Global Opaque OUGHT_TO_BE_UNUSED.

Definition ComputeLive {t} (e : expr.Expr t) : PositiveMap.t unit
:= @Subst01.ComputeLiveCounts unit tt (fun _ => tt) (fun _ => tt) base_type ident is_ident_always_live _ e.
Definition is_live (map : PositiveMap.t unit) (idx : positive) : bool
:= match PositiveMap.find idx map with
| Some tt => true
| None => false
end.
Definition is_dead (map : PositiveMap.t unit) (idx : positive) : bool
:= negb (is_live map idx).

Definition EliminateDead {t} (e : expr.Expr t) : expr.Expr t
:= @Subst01.Subst0n unit tt (fun _ => tt) (fun _ => tt) base_type ident is_ident_always_live (fun T1 T2 => OUGHT_TO_BE_UNUSED) (fun _ => false) t e.
Definition EliminateDead
{ident : type -> Type}
{try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type}
{exprDefault : forall var, @DefaultValue.type.base.DefaultT _ _}
(is_ident_always_live : forall t, ident t -> bool)
{t} (e : expr.Expr t)
: expr.Expr t
:= @Subst01.Subst0n unit tt (fun _ => tt) (fun _ => tt) base_type ident is_ident_always_live try_make_transport_base_type_cps exprDefault (fun T1 T2 => OUGHT_TO_BE_UNUSED) (fun _ => false) t e.
End with_ident.
End DeadCodeElimination.
End Compilers.
Loading

0 comments on commit 922fb56

Please sign in to comment.