Overeager substitution in dead code elimination? #1604

andres-erbsen · 2023-05-08T21:28:10Z

It looks like "DCE" inlines a let binder that is in fact used, causing synthesis to fail with Invalid identifier in arithmetic expression Z.zselect. @JasonGross do you have a guess for what is going on here?

After rewriting RewriteArith_0:
let x15 := Z.zselect(x13₁, (0, 38)) in

After rewriting DCE after RewriteArith_0:
let x14 := Z.add_with_get_carry((2^64), (0, ((Z.zselect(x12₁, (0, 38))), ((x12₂ << 0x140) + x8₁)))) in

Log: https://gist.github.com/andres-erbsen/bbfb1994c4e8294be35c5ab59966faf2#file-sat_add-log-L249-L281
Source: andres-erbsen@48c3e62#diff-fc27e1c96d797f696a0116daf62647b093f90d5f4cf52eba7896076151990554

The text was updated successfully, but these errors were encountered:

JasonGross · 2023-05-09T03:06:27Z

I do not. I guess the DCE calculation is buggy? Strange that it hasn't shown up before this...

JasonGross · 2023-05-09T03:09:30Z

Hmm, it's possible that the DCE code does not know how to handle lambdas, and the thunked branches of the if statements are messing it up?

JasonGross · 2023-05-09T03:17:22Z

Nope, the code seems to handle lambdas fine. If you can paste valid Coq code that computes to the expression before DCE, such that vm_compute on DCE results in the mis-inlining, I can try single-stepping it and see what's going on

andres-erbsen · 2023-05-10T03:40:37Z

There you go: andres-erbsen@811460b Thank you!

andres-erbsen · 2023-05-18T11:08:27Z

See also #1601 (comment)

JasonGross · 2023-05-18T16:55:09Z

I've tracked down the issue, and indeed it is what I originally suspected: DCE cannot handle code branching that contains lambdas, so it's the if-statements that are causing trouble. The code at

fiat-crypto/src/MiscCompilerPasses.v

Lines 93 to 94 in 1cce238

    
           | expr.Abs s d f 
        
             => (cur_idx, expr.Abs (fun v => snd (@subst0n' _ (f (expr.Var v)) (Pos.succ cur_idx))))

and

fiat-crypto/src/MiscCompilerPasses.v

Lines 58 to 60 in 1cce238

    
           | expr.Abs s d f 
        
             => let '(idx, live) := @compute_live_counts' _ (f cur_idx) (Pos.succ cur_idx) live in 
        
                (cur_idx, live)

does not propagate the index update from underneath the lambda, and so indices end up being incorrectly reused.

I can think of two solutions:

Thread a boolean of "is in head position", so that we recurse under the initial lambdas, but not under lambdas in the arguments to any App, nor under lambdas in the variable-bindings of let-in
Adjust subst0n' to recurse over the PHOAS expression at two different var arguments, one for tracking the current index, and the other for tracking the returned expression.

Thoughts? (And do you feel confident implementing either of these fixes?)

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 mit-plv#1761 and mit-plv#1604 (comment). Fixes mit-plv#1604

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>

OwenConoly mentioned this issue May 18, 2023

Optimize dettman algorithm #1601

Merged

JasonGross mentioned this issue Jan 22, 2024

Fix DCE/Subst01 to work under lambdas #1809

Merged

JasonGross closed this as completed in #1809 Jan 23, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Overeager substitution in dead code elimination? #1604

Overeager substitution in dead code elimination? #1604

andres-erbsen commented May 8, 2023

JasonGross commented May 9, 2023

JasonGross commented May 9, 2023

JasonGross commented May 9, 2023

andres-erbsen commented May 10, 2023

andres-erbsen commented May 18, 2023

JasonGross commented May 18, 2023

Overeager substitution in dead code elimination? #1604

Overeager substitution in dead code elimination? #1604

Comments

andres-erbsen commented May 8, 2023

JasonGross commented May 9, 2023

JasonGross commented May 9, 2023

JasonGross commented May 9, 2023

andres-erbsen commented May 10, 2023

andres-erbsen commented May 18, 2023

JasonGross commented May 18, 2023