From 2610f854db7edaebafe70c9ee496748b721ce029 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 22 Jan 2024 16:15:08 -0500 Subject: [PATCH] Fix DCE/Subst01 to work under lambdas MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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
Timing Diff

``` 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% ```

--- src/BoundsPipeline.v | 10 +- src/Language/TreeCaching.v | 70 +++++++++++++ src/MiscCompilerPasses.v | 147 +++++++++++++++++----------- src/MiscCompilerPassesProofs.v | 95 +++++++++++------- src/MiscCompilerPassesProofsExtra.v | 8 +- 5 files changed, 226 insertions(+), 104 deletions(-) create mode 100644 src/Language/TreeCaching.v diff --git a/src/BoundsPipeline.v b/src/BoundsPipeline.v index 5666bb1945..de40f32702 100644 --- a/src/BoundsPipeline.v +++ b/src/BoundsPipeline.v @@ -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) @@ -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; @@ -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 diff --git a/src/Language/TreeCaching.v b/src/Language/TreeCaching.v new file mode 100644 index 0000000000..107c4d8f09 --- /dev/null +++ b/src/Language/TreeCaching.v @@ -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)}% + #mit-plv/fiat-crypto##1604 with option (2)# + and + %\href{https://github.com/mit-plv/fiat-crypto/issues/1761}{mit-plv/fiat-crypto\#1761}% + #mit-plv/fiat-crypto##1761#. *) + +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. diff --git a/src/MiscCompilerPasses.v b/src/MiscCompilerPasses.v index a534f59744..b4e7c64e60 100644 --- a/src/MiscCompilerPasses.v +++ b/src/MiscCompilerPasses.v @@ -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. @@ -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 @@ -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. @@ -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. @@ -122,8 +163,13 @@ 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. @@ -131,25 +177,16 @@ Module Compilers. 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. diff --git a/src/MiscCompilerPassesProofs.v b/src/MiscCompilerPassesProofs.v index 0fe5c89638..569bb993a8 100644 --- a/src/MiscCompilerPassesProofs.v +++ b/src/MiscCompilerPassesProofs.v @@ -6,7 +6,10 @@ Require Import Coq.FSets.FMapPositive. Require Import Rewriter.Language.Language. Require Import Rewriter.Language.Inversion. Require Import Rewriter.Language.Wf. +Require Import Crypto.Language.TreeCaching. Require Import Crypto.MiscCompilerPasses. +Require Import Crypto.Util.Bool.Reflect. +Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.SpecializeAllWays. @@ -39,45 +42,42 @@ Module Compilers. 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). + Context {ident : type -> Type}. Local Notation expr := (@expr.expr base_type ident). + Context {base_type_beq : base_type -> base_type -> bool} + {try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type} + {reflect_base_type_beq : reflect_rel (@eq base_type) base_type_beq} + {exprDefault : forall var, @DefaultValue.type.base.DefaultT type (@expr var)} + {try_make_transport_base_type_cps_correct : type.try_make_transport_cps_correctT base_type}. + Context (is_ident_always_live : forall t, ident t -> bool). Section with_var. Context {doing_subst_debug : forall T1 T2, T1 -> (unit -> T2) -> T1} {should_subst : T -> bool} (Hdoing_subst_debug : forall T1 T2 x y, doing_subst_debug T1 T2 x y = x) - {var1 var2 : type -> Type} - (live : PositiveMap.t T). + {var1 var2 : type -> Type}. + Local Notation tree := (@tree_nd.tree (option T * (unit -> positive * list (positive * T)))). Local Notation expr1 := (@expr.expr base_type ident var1). Local Notation expr2 := (@expr.expr base_type ident var2). - Local Notation subst0n'1 := (@subst0n' T base_type ident doing_subst_debug var1 should_subst live). - Local Notation subst0n'2 := (@subst0n' T base_type ident doing_subst_debug var2 should_subst live). - Local Notation subst0n1 := (@subst0n T base_type ident doing_subst_debug var1 should_subst live). - Local Notation subst0n2 := (@subst0n T base_type ident doing_subst_debug var2 should_subst live). + Local Notation subst0n1 := (@subst0n T base_type ident doing_subst_debug var1 should_subst). + Local Notation subst0n2 := (@subst0n T base_type ident doing_subst_debug var2 should_subst). - Lemma wf_subst0n' G1 G2 t e1 e2 p + Lemma wf_subst0n_gen live G1 G2 t e1 e2 (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> expr.wf G2 v1 v2) - : expr.wf G1 (t:=t) e1 e2 -> expr.wf G2 (snd (subst0n'1 e1 p)) (snd (subst0n'2 e2 p)) - /\ fst (subst0n'1 e1 p) = fst (subst0n'2 e2 p). + : expr.wf G1 (t:=t) e1 e2 -> expr.wf G2 (subst0n1 live e1) (subst0n2 live e2). Proof using Hdoing_subst_debug. - intro Hwf; revert dependent G2; revert p; induction Hwf; - cbn [subst0n']; + intro Hwf; revert dependent G2; revert live; induction Hwf; + cbn [subst0n]; repeat first [ progress wf_safe_t | simplifier_t_step - | progress split_and | rewrite Hdoing_subst_debug - | apply conj - | match goal with - | [ H : context[fst _ = fst _] |- _ ] => progress erewrite H by eauto - end | break_innermost_match_step | solve [ wf_t ] ]. Qed. - Lemma wf_subst0n t e1 e2 - : expr.wf nil (t:=t) e1 e2 -> expr.wf nil (subst0n1 e1) (subst0n2 e2). - Proof using Hdoing_subst_debug. clear -Hdoing_subst_debug; intro Hwf; apply wf_subst0n' with (G1:=nil); cbn [In]; eauto with nocore; tauto. Qed. + Lemma wf_subst0n live t e1 e2 + : expr.wf nil (t:=t) e1 e2 -> expr.wf nil (subst0n1 live e1) (subst0n2 live e2). + Proof using Hdoing_subst_debug. intro Hwf; eapply wf_subst0n_gen, Hwf; wf_safe_t. Qed. End with_var. Lemma Wf_Subst0n @@ -86,7 +86,10 @@ Module Compilers. (Hdoing_subst_debug : forall T1 T2 x y, doing_subst_debug T1 T2 x y = x) {t} (e : @expr.Expr base_type ident t) : expr.Wf e -> expr.Wf (Subst0n one incr incr_always_live is_ident_always_live doing_subst_debug should_subst e). - Proof using Type. intros Hwf var1 var2; eapply wf_subst0n, Hwf; assumption. Qed. + Proof using try_make_transport_base_type_cps_correct. + intros Hwf var1 var2; cbv [Subst0n Let_In]. + apply wf_subst0n, GeneralizeVar.Wf_FromFlat_ToFlat, Hwf; assumption. + Qed. Section interp. Context {base_interp : base_type -> Type} @@ -98,13 +101,12 @@ Module Compilers. {should_subst : T -> bool} (Hdoing_subst_debug : forall T1 T2 x y, doing_subst_debug T1 T2 x y = x). - Lemma interp_subst0n'_gen (live : PositiveMap.t T) G t (e1 e2 : expr t) + Lemma interp_subst0n_gen live G t (e1 e2 : expr t) (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> expr.interp interp_ident v1 == v2) (Hwf : expr.wf G e1 e2) - p - : expr.interp interp_ident (snd (subst0n' doing_subst_debug should_subst live e1 p)) == expr.interp interp_ident e2. + : expr.interp interp_ident (subst0n doing_subst_debug should_subst live e1) == expr.interp interp_ident e2. Proof using Hdoing_subst_debug interp_ident_Proper. - revert p; induction Hwf; cbn [subst0n']; cbv [Proper respectful] in *; + revert live; induction Hwf; cbn [subst0n]; cbv [Proper respectful] in *; repeat first [ progress interp_safe_t | simplifier_t_step | rewrite Hdoing_subst_debug @@ -115,11 +117,15 @@ Module Compilers. Lemma interp_subst0n live t (e1 e2 : expr t) (Hwf : expr.wf nil e1 e2) : expr.interp interp_ident (subst0n doing_subst_debug should_subst live e1) == expr.interp interp_ident e2. - Proof using Hdoing_subst_debug interp_ident_Proper. clear -Hwf Hdoing_subst_debug interp_ident_Proper. apply interp_subst0n'_gen with (G:=nil); cbn [In]; eauto with nocore; tauto. Qed. + Proof using Hdoing_subst_debug interp_ident_Proper. clear -Hwf Hdoing_subst_debug interp_ident_Proper. apply interp_subst0n_gen with (G:=nil); cbn [In]; eauto with nocore; tauto. Qed. Lemma Interp_Subst0n {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e) : expr.Interp interp_ident (Subst0n one incr incr_always_live is_ident_always_live doing_subst_debug should_subst e) == expr.Interp interp_ident e. - Proof using Hdoing_subst_debug interp_ident_Proper. apply interp_subst0n, Hwf. Qed. + Proof using Hdoing_subst_debug interp_ident_Proper try_make_transport_base_type_cps_correct. + cbv [Subst0n Let_In expr.Interp]. + etransitivity; [ apply interp_subst0n, GeneralizeVar.Wf_FromFlat_ToFlat, Hwf | ]. + apply GeneralizeVar.Interp_gen1_FromFlat_ToFlat; assumption. + Qed. End with_doing_subst_debug. End interp. End with_ident. @@ -128,13 +134,18 @@ Module Compilers. 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). + Context {ident : type -> Type}. Local Notation expr := (@expr.expr base_type ident). + Context {base_type_beq : base_type -> base_type -> bool} + {try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type} + {reflect_base_type_beq : reflect_rel (@eq base_type) base_type_beq} + {exprDefault : forall var, @DefaultValue.type.base.DefaultT type (@expr var)} + {try_make_transport_base_type_cps_correct : type.try_make_transport_cps_correctT base_type}. + Context (is_ident_always_live : forall t, ident t -> bool). Lemma Wf_Subst01 {t} (e : @expr.Expr base_type ident t) : expr.Wf e -> expr.Wf (Subst01 is_ident_always_live e). - Proof using Type. eapply Wf_Subst0n; reflexivity. Qed. + Proof using try_make_transport_base_type_cps_correct. eapply Wf_Subst0n; try assumption; reflexivity. Qed. Section interp. Context {base_interp : base_type -> Type} @@ -142,9 +153,11 @@ Module Compilers. {interp_ident_Proper : forall t, Proper (eq ==> type.eqv) (interp_ident t)}. Lemma Interp_Subst01 {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e) : expr.Interp interp_ident (Subst01 is_ident_always_live e) == expr.Interp interp_ident e. - Proof using interp_ident_Proper. apply Interp_Subst0n, Hwf; auto. Qed. + Proof using interp_ident_Proper try_make_transport_base_type_cps_correct. eapply Interp_Subst0n, Hwf; auto. Qed. End interp. End with_ident. + + Ltac autorewrite_interp_side_condition_solver := assumption. End Subst01. #[global] @@ -152,7 +165,7 @@ Module Compilers. #[global] Hint Opaque Subst01.Subst01 : wf interp rewrite. #[global] - Hint Rewrite @Subst01.Interp_Subst01 : interp. + Hint Rewrite @Subst01.Interp_Subst01 using Subst01.autorewrite_interp_side_condition_solver : interp. Module DeadCodeElimination. Import MiscCompilerPasses.Compilers.DeadCodeElimination. @@ -169,13 +182,18 @@ Module Compilers. 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). + Context {ident : type -> Type}. Local Notation expr := (@expr.expr base_type ident). + Context {base_type_beq : base_type -> base_type -> bool} + {try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type} + {reflect_base_type_beq : reflect_rel (@eq base_type) base_type_beq} + {exprDefault : forall var, @DefaultValue.type.base.DefaultT type (@expr var)} + {try_make_transport_base_type_cps_correct : type.try_make_transport_cps_correctT base_type}. + Context (is_ident_always_live : forall t, ident t -> bool). Lemma Wf_EliminateDead {t} (e : @expr.Expr base_type ident t) : expr.Wf e -> expr.Wf (EliminateDead is_ident_always_live e). - Proof using Type. apply Subst01.Wf_Subst0n; intros; apply @OUGHT_TO_BE_UNUSED_id. Qed. + Proof using try_make_transport_base_type_cps_correct. eapply Subst01.Wf_Subst0n; auto using @OUGHT_TO_BE_UNUSED_id. Qed. Section interp. Context {base_interp : base_type -> Type} @@ -184,9 +202,10 @@ Module Compilers. Lemma Interp_EliminateDead {t} (e : @expr.Expr base_type ident t) (Hwf : expr.Wf e) : expr.Interp interp_ident (EliminateDead is_ident_always_live e) == expr.Interp interp_ident e. - Proof using interp_ident_Proper. apply Subst01.Interp_Subst0n, Hwf; auto using @OUGHT_TO_BE_UNUSED_id. Qed. + Proof using interp_ident_Proper try_make_transport_base_type_cps_correct. eapply Subst01.Interp_Subst0n, Hwf; auto using @OUGHT_TO_BE_UNUSED_id. Qed. End interp. End with_ident. + Ltac autorewrite_interp_side_condition_solver := Subst01.autorewrite_interp_side_condition_solver. End DeadCodeElimination. #[global] @@ -194,5 +213,5 @@ Module Compilers. #[global] Hint Opaque DeadCodeElimination.EliminateDead : wf interp rewrite. #[global] - Hint Rewrite @DeadCodeElimination.Interp_EliminateDead : interp. + Hint Rewrite @DeadCodeElimination.Interp_EliminateDead using DeadCodeElimination.autorewrite_interp_side_condition_solver : interp. End Compilers. diff --git a/src/MiscCompilerPassesProofsExtra.v b/src/MiscCompilerPassesProofsExtra.v index 6dfe3e82a1..4e8030f9c4 100644 --- a/src/MiscCompilerPassesProofsExtra.v +++ b/src/MiscCompilerPassesProofsExtra.v @@ -26,8 +26,10 @@ Module Compilers. Module Subst01. Import MiscCompilerPassesProofs.Compilers.Subst01. + Definition Wf_Subst01 is_ident_always_live {t} e Hwf + := @Wf_Subst01 _ ident _ _ _ _ _ is_ident_always_live t e Hwf. Definition Interp_Subst01 is_ident_always_live {t} e Hwf - := @Interp_Subst01 _ ident is_ident_always_live _ (@ident.interp) (@ident.interp_Proper) t e Hwf. + := @Interp_Subst01 _ ident _ _ _ _ _ is_ident_always_live _ (@ident.interp) (@ident.interp_Proper) t e Hwf. End Subst01. #[global] @@ -40,8 +42,10 @@ Module Compilers. Module DeadCodeElimination. Import MiscCompilerPassesProofs.Compilers.DeadCodeElimination. + Definition Wf_EliminateDead is_ident_always_live {t} e Hwf + := @Wf_EliminateDead _ ident _ _ _ _ _ is_ident_always_live t e Hwf. Definition Interp_EliminateDead is_ident_always_live {t} e Hwf - := @Interp_EliminateDead _ ident is_ident_always_live _ (@ident.interp) (@ident.interp_Proper) t e Hwf. + := @Interp_EliminateDead _ ident _ _ _ _ _ is_ident_always_live _ (@ident.interp) (@ident.interp_Proper) t e Hwf. End DeadCodeElimination. #[global]