Add remaining rewrite rules for saturated arithmetic #1778
Commits on Jan 4, 2024
-
Add remaining rewrite rules for saturated arithmetic
For https://github.com/mit-plv/fiat-crypto/pull/1609 <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ 133m38.95s | 4370484 ko | Total Time / Peak Mem | 129m38.05s | 3712508 ko || +4m00.90s || 657976 ko | +3.09% | +17.72% ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ 5m34.12s | 4370484 ko | Rewriter/Passes/NBE.vo | 2m34.13s | 3330528 ko || +2m59.99s || 1039956 ko | +116.77% | +31.22% 1m59.50s | 2329072 ko | fiat-rust/src/p384_scalar_32.rs | 2m02.66s | 2299112 ko || -0m03.15s || 29960 ko | -2.57% | +1.30% 1m57.95s | 2415624 ko | fiat-json/src/p384_32.json | 1m54.82s | 2444832 ko || +0m03.13s || -29208 ko | +2.72% | -1.19% 0m39.98s | 2234396 ko | ExtractionOCaml/dettman_multiplication | 0m36.98s | 1927716 ko || +0m03.00s || 306680 ko | +8.11% | +15.90% 5m31.05s | 3200456 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo | 5m28.82s | 3175412 ko || +0m02.23s || 25044 ko | +0.67% | +0.78% 2m00.23s | 2461568 ko | fiat-json/src/p384_scalar_32.json | 1m58.15s | 2162244 ko || +0m02.07s || 299324 ko | +1.76% | +13.84% 1m59.33s | 2241456 ko | fiat-bedrock2/src/p384_scalar_32.c | 2m01.48s | 2430500 ko || -0m02.15s || -189044 ko | -1.76% | -7.77% 1m58.75s | 2141892 ko | fiat-java/src/FiatP384Scalar.java | 2m01.05s | 2237348 ko || -0m02.29s || -95456 ko | -1.90% | -4.26% 1m58.44s | 2273192 ko | fiat-go/32/p384scalar/p384scalar.go | 2m00.68s | 2317900 ko || -0m02.24s || -44708 ko | -1.85% | -1.92% 1m57.40s | 2307724 ko | fiat-java/src/FiatP384.java | 1m59.84s | 2327088 ko || -0m02.43s || -19364 ko | -2.03% | -0.83% 1m56.84s | 2321212 ko | fiat-zig/src/p384_32.zig | 1m59.10s | 2285560 ko || -0m02.25s || 35652 ko | -1.89% | +1.55% 1m56.07s | 2290720 ko | fiat-c/src/p384_32.c | 1m58.32s | 2325148 ko || -0m02.25s || -34428 ko | -1.90% | -1.48% 1m02.24s | 3703520 ko | ExtractionOCaml/with_bedrock2_fiat_crypto | 0m59.53s | 3712508 ko || +0m02.71s || -8988 ko | +4.55% | -0.24% 1m01.35s | 3705452 ko | ExtractionOCaml/bedrock2_fiat_crypto | 0m59.03s | 3710668 ko || +0m02.32s || -5216 ko | +3.93% | -0.14% 0m54.91s | 3724428 ko | ExtractionOCaml/fiat_crypto | 0m52.48s | 3710332 ko || +0m02.42s || 14096 ko | +4.63% | +0.37% 0m54.29s | 2480048 ko | ExtractionJsOfOCaml/fiat_crypto.ml | 0m52.17s | 2487376 ko || +0m02.11s || -7328 ko | +4.06% | -0.29% 0m48.09s | 2652116 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery | 0m45.49s | 2632088 ko || +0m02.60s || 20028 ko | +5.71% | +0.76% 0m47.65s | 2657836 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery | 0m44.92s | 2630968 ko || +0m02.72s || 26868 ko | +6.07% | +1.02% 0m47.57s | 2726404 ko | ExtractionOCaml/bedrock2_solinas_reduction | 0m45.01s | 2704500 ko || +0m02.56s || 21904 ko | +5.68% | +0.80% 0m45.77s | 2689372 ko | ExtractionOCaml/solinas_reduction | 0m43.29s | 2683760 ko || +0m02.48s || 5612 ko | +5.72% | +0.20% 0m45.63s | 2633500 ko | ExtractionOCaml/word_by_word_montgomery | 0m43.16s | 2619516 ko || +0m02.47s || 13984 ko | +5.72% | +0.53% 0m45.27s | 2544004 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas | 0m42.87s | 2533792 ko || +0m02.40s || 10212 ko | +5.59% | +0.40% 0m45.08s | 2545148 ko | ExtractionOCaml/bedrock2_unsaturated_solinas | 0m42.40s | 2536564 ko || +0m02.67s || 8584 ko | +6.32% | +0.33% 0m42.60s | 2339896 ko | ExtractionOCaml/unsaturated_solinas | 0m40.15s | 2331728 ko || +0m02.45s || 8168 ko | +6.10% | +0.35% 0m42.14s | 2237132 ko | ExtractionOCaml/with_bedrock2_base_conversion | 0m39.92s | 2230688 ko || +0m02.21s || 6444 ko | +5.56% | +0.28% 0m41.95s | 2258216 ko | ExtractionOCaml/bedrock2_dettman_multiplication | 0m39.79s | 2246108 ko || +0m02.16s || 12108 ko | +5.42% | +0.53% 0m41.92s | 2240944 ko | ExtractionOCaml/with_bedrock2_saturated_solinas | 0m39.70s | 2233448 ko || +0m02.21s || 7496 ko | +5.59% | +0.33% 0m41.86s | 2239092 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication | 0m39.56s | 2234396 ko || +0m02.29s || 4696 ko | +5.81% | +0.21% 0m41.57s | 2240068 ko | ExtractionOCaml/bedrock2_saturated_solinas | 0m39.51s | 2231968 ko || +0m02.06s || 8100 ko | +5.21% | +0.36% 0m41.41s | 2234816 ko | ExtractionOCaml/bedrock2_base_conversion | 0m39.16s | 2224784 ko || +0m02.25s || 10032 ko | +5.74% | +0.45% 0m39.09s | 2045652 ko | ExtractionOCaml/base_conversion | 0m36.77s | 1882572 ko || +0m02.32s || 163080 ko | +6.30% | +8.66% 0m39.06s | 2055248 ko | ExtractionOCaml/saturated_solinas | 0m36.32s | 1900876 ko || +0m02.74s || 154372 ko | +7.54% | +8.12% 0m35.49s | 1741752 ko | ExtractionOCaml/perf_unsaturated_solinas | 0m33.30s | 1696000 ko || +0m02.19s || 45752 ko | +6.57% | +2.69% 2m00.22s | 2401976 ko | fiat-bedrock2/src/p384_32.c | 2m02.18s | 2217824 ko || -0m01.96s || 184152 ko | -1.60% | +8.30% 1m59.91s | 2320940 ko | fiat-zig/src/p384_scalar_32.zig | 2m01.71s | 2195356 ko || -0m01.79s || 125584 ko | -1.47% | +5.72% 1m59.14s | 2264508 ko | fiat-c/src/p384_scalar_32.c | 2m01.04s | 2315428 ko || -0m01.90s || -50920 ko | -1.56% | -2.19% 1m58.08s | 2290144 ko | fiat-rust/src/p384_32.rs | 1m59.31s | 2292024 ko || -0m01.23s || -1880 ko | -1.03% | -0.08% 0m42.55s | 2240500 ko | ExtractionOCaml/with_bedrock2_solinas_reduction | 0m40.66s | 2234592 ko || +0m01.89s || 5908 ko | +4.64% | +0.26% 0m40.28s | 1478504 ko | Rewriter/Passes/Arith.vo | 0m41.98s | 1481228 ko || -0m01.69s || -2724 ko | -4.04% | -0.18% 0m34.72s | 1752580 ko | ExtractionOCaml/perf_word_by_word_montgomery | 0m32.93s | 1718100 ko || +0m01.78s || 34480 ko | +5.43% | +2.00% 0m29.64s | 2053032 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml | 0m28.62s | 2049864 ko || +0m01.01s || 3168 ko | +3.56% | +0.15% 0m28.03s | 1945424 ko | ExtractionOCaml/saturated_solinas.ml | 0m26.78s | 1911944 ko || +0m01.25s || 33480 ko | +4.66% | +1.75% 0m17.56s | 320704 ko | fiat-go/64/p434/p434.go | 0m16.35s | 344808 ko || +0m01.20s || -24104 ko | +7.40% | -6.99% 8m04.87s | 2663916 ko | Bedrock/End2End/X25519/GarageDoor.vo | 8m04.02s | 2661980 ko || +0m00.85s || 1936 ko | +0.17% | +0.07% 4m45.51s | 2494088 ko | Bedrock/End2End/X25519/EdwardsXYZT.vo | 4m46.33s | 2489792 ko || -0m00.81s || 4296 ko | -0.28% | +0.17% 3m21.85s | 3498672 ko | Rewriter/Passes/ArithWithCasts.vo | 3m21.48s | 3497152 ko || +0m00.37s || 1520 ko | +0.18% | +0.04% 2m06.54s | 1391724 ko | Bedrock/End2End/X25519/Field25519.vo | 2m06.68s | 1385108 ko || -0m00.14s || 6616 ko | -0.11% | +0.47% 1m59.46s | 2196900 ko | fiat-go/32/p384/p384.go | 1m58.78s | 2251120 ko || +0m00.68s || -54220 ko | +0.57% | -2.40% 1m53.98s | 2478600 ko | Rewriter/Passes/ToFancyWithCasts.vo | 1m53.96s | 2481272 ko || +0m00.01s || -2672 ko | +0.01% | -0.10% 1m32.90s | 1957336 ko | SlowPrimeSynthesisExamples.vo | 1m32.90s | 1951288 ko || +0m00.00s || 6048 ko | +0.00% | +0.30% 1m32.09s | 2070416 ko | Fancy/Barrett256.vo | 1m31.69s | 2070856 ko || +0m00.40s || -440 ko | +0.43% | -0.02% 0m56.65s | 2591660 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.ml | 0m56.04s | 2587220 ko || +0m00.60s || 4440 ko | +1.08% | +0.17% 0m56.59s | 2591872 ko | ExtractionOCaml/bedrock2_fiat_crypto.ml | 0m55.96s | 2588596 ko || +0m00.63s || 3276 ko | +1.12% | +0.12% 0m56.36s | 2597952 ko | ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.ml | 0m55.83s | 2591080 ko || +0m00.53s || 6872 ko | +0.94% | +0.26% 0m56.26s | 834704 ko | Rewriter/RulesProofs.vo | 0m55.87s | 848780 ko || +0m00.39s || -14076 ko | +0.69% | -1.65% 0m56.16s | 2599000 ko | ExtractionJsOfOCaml/bedrock2_fiat_crypto.ml | 0m55.46s | 2588324 ko || +0m00.69s || 10676 ko | +1.26% | +0.41% 0m54.47s | 2480528 ko | ExtractionOCaml/fiat_crypto.ml | 0m53.50s | 2488780 ko || +0m00.96s || -8252 ko | +1.81% | -0.33% 0m50.01s | 1117432 ko | Rewriter/Passes/MultiRetSplit.vo | 0m50.54s | 1117464 ko || -0m00.53s || -32 ko | -1.04% | -0.00% 0m47.05s | 1843584 ko | Fancy/Montgomery256.vo | 0m46.57s | 1882256 ko || +0m00.47s || -38672 ko | +1.03% | -2.05% 0m41.03s | 89412 ko | fiat-go/32/p521/p521.go | 0m41.29s | 90304 ko || -0m00.25s || -892 ko | -0.62% | -0.98% 0m38.73s | 192288 ko | fiat-bedrock2/src/p521_32.c | 0m38.54s | 191252 ko || +0m00.18s || 1036 ko | +0.49% | +0.54% 0m37.96s | 2250044 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml | 0m37.38s | 2262168 ko || +0m00.57s || -12124 ko | +1.55% | -0.53% 0m37.96s | 139000 ko | fiat-json/src/p521_32.json | 0m37.84s | 133668 ko || +0m00.11s || 5332 ko | +0.31% | +3.98% 0m37.78s | 80004 ko | fiat-zig/src/p521_32.zig | 0m37.75s | 84172 ko || +0m00.03s || -4168 ko | +0.07% | -4.95% 0m37.75s | 81832 ko | fiat-rust/src/p521_32.rs | 0m37.84s | 82404 ko || -0m00.09s || -572 ko | -0.23% | -0.69% 0m37.63s | 85588 ko | fiat-java/src/FiatP521.java | 0m37.81s | 83048 ko || -0m00.17s || 2540 ko | -0.47% | +3.05% 0m37.53s | 82628 ko | fiat-c/src/p521_32.c | 0m37.72s | 79408 ko || -0m00.18s || 3220 ko | -0.50% | +4.05% 0m37.25s | 2254188 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml | 0m36.44s | 2212012 ko || +0m00.81s || 42176 ko | +2.22% | +1.90% 0m37.14s | 2254952 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml | 0m36.41s | 2211712 ko || +0m00.73s || 43240 ko | +2.00% | +1.95% 0m36.21s | 2176032 ko | ExtractionOCaml/solinas_reduction.ml | 0m35.30s | 2146952 ko || +0m00.91s || 29080 ko | +2.57% | +1.35% 0m35.12s | 2145588 ko | ExtractionOCaml/word_by_word_montgomery.ml | 0m34.17s | 2116752 ko || +0m00.94s || 28836 ko | +2.78% | +1.36% 0m33.21s | 899056 ko | Rewriter/Passes/MulSplit.vo | 0m33.18s | 895480 ko || +0m00.03s || 3576 ko | +0.09% | +0.39% 0m32.88s | 2166828 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml | 0m33.41s | 2166516 ko || -0m00.52s || 312 ko | -1.58% | +0.01% 0m32.85s | 2164880 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml | 0m33.57s | 2166408 ko || -0m00.71s || -1528 ko | -2.14% | -0.07% 0m32.49s | 1221984 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m32.64s | 1219996 ko || -0m00.14s || 1988 ko | -0.45% | +0.16% 0m32.10s | 2091560 ko | ExtractionOCaml/unsaturated_solinas.ml | 0m31.31s | 2033016 ko || +0m00.79s || 58544 ko | +2.52% | +2.87% 0m30.93s | 1256232 ko | Bedrock/End2End/X25519/GarageDoorTop.vo | 0m31.18s | 1258200 ko || -0m00.25s || -1968 ko | -0.80% | -0.15% 0m30.58s | 2083824 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml | 0m29.69s | 2035044 ko || +0m00.88s || 48780 ko | +2.99% | +2.39% 0m30.07s | 1481064 ko | StandaloneDebuggingExamples.vo | 0m30.16s | 1479316 ko || -0m00.08s || 1748 ko | -0.29% | +0.11% 0m29.85s | 2075580 ko | ExtractionOCaml/bedrock2_base_conversion.ml | 0m29.01s | 2027820 ko || +0m00.83s || 47760 ko | +2.89% | +2.35% 0m29.71s | 2074580 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml | 0m28.90s | 2028104 ko || +0m00.81s || 46476 ko | +2.80% | +2.29% 0m29.71s | 2070300 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml | 0m28.72s | 2048012 ko || +0m00.99s || 22288 ko | +3.44% | +1.08% 0m29.58s | 2070020 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml | 0m28.98s | 2048204 ko || +0m00.59s || 21816 ko | +2.07% | +1.06% 0m29.57s | 2070812 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml | 0m28.64s | 2048732 ko || +0m00.92s || 22080 ko | +3.24% | +1.07% 0m28.56s | 2011744 ko | ExtractionOCaml/dettman_multiplication.ml | 0m27.77s | 1986400 ko || +0m00.78s || 25344 ko | +2.84% | +1.27% 0m27.60s | 1954988 ko | ExtractionOCaml/base_conversion.ml | 0m27.05s | 1939500 ko || +0m00.55s || 15488 ko | +2.03% | +0.79% 0m25.28s | 1299164 ko | PerfTesting/PerfTestSearch.vo | 0m25.45s | 1302744 ko || -0m00.16s || -3580 ko | -0.66% | -0.27% 0m21.63s | 1909120 ko | ExtractionOCaml/perf_unsaturated_solinas.ml | 0m20.75s | 1832892 ko || +0m00.87s || 76228 ko | +4.24% | +4.15% 0m21.54s | 2437392 ko | ExtractionHaskell/with_bedrock2_fiat_crypto.hs | 0m21.34s | 2441484 ko || +0m00.19s || -4092 ko | +0.93% | -0.16% 0m21.40s | 2436356 ko | ExtractionHaskell/bedrock2_fiat_crypto.hs | 0m21.03s | 2438364 ko || +0m00.36s || -2008 ko | +1.75% | -0.08% 0m21.26s | 1899948 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml | 0m21.00s | 1929736 ko || +0m00.26s || -29788 ko | +1.23% | -1.54% 0m20.89s | 1109836 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m20.89s | 1117536 ko || +0m00.00s || -7700 ko | +0.00% | -0.68% 0m20.78s | 2366272 ko | ExtractionHaskell/fiat_crypto.hs | 0m20.58s | 2338376 ko || +0m00.20s || 27896 ko | +0.97% | +1.19% 0m18.71s | 1115184 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m18.71s | 1116872 ko || +0m00.00s || -1688 ko | +0.00% | -0.15% 0m18.52s | 1088300 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m18.43s | 1082908 ko || +0m00.08s || 5392 ko | +0.48% | +0.49% 0m18.02s | 385368 ko | fiat-bedrock2/src/p434_64.c | 0m18.09s | 395184 ko || -0m00.07s || -9816 ko | -0.38% | -2.48% 0m17.58s | 385232 ko | fiat-json/src/p434_64.json | 0m17.61s | 354440 ko || -0m00.03s || 30792 ko | -0.17% | +8.68% 0m17.55s | 2147688 ko | ExtractionHaskell/with_bedrock2_word_by_word_montgomery.hs | 0m17.01s | 2096248 ko || +0m00.53s || 51440 ko | +3.17% | +2.45% 0m17.53s | 332812 ko | fiat-rust/src/p434_64.rs | 0m17.51s | 331704 ko || +0m00.01s || 1108 ko | +0.11% | +0.33% 0m17.42s | 1291228 ko | PerfTesting/PerfTestSearchPattern.vo | 0m17.36s | 1290596 ko || +0m00.06s || 632 ko | +0.34% | +0.04% 0m17.41s | 2162836 ko | ExtractionHaskell/bedrock2_solinas_reduction.hs | 0m17.05s | 2115740 ko || +0m00.35s || 47096 ko | +2.11% | +2.22% 0m17.34s | 2162424 ko | ExtractionHaskell/with_bedrock2_solinas_reduction.hs | 0m17.01s | 2115484 ko || +0m00.32s || 46940 ko | +1.94% | +2.21% 0m17.32s | 319240 ko | fiat-zig/src/p434_64.zig | 0m17.41s | 332084 ko || -0m00.08s || -12844 ko | -0.51% | -3.86% 0m17.29s | 2148704 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs | 0m16.97s | 2095280 ko || +0m00.32s || 53424 ko | +1.88% | +2.54% 0m17.28s | 327216 ko | fiat-c/src/p434_64.c | 0m17.59s | 320604 ko || -0m00.30s || 6612 ko | -1.76% | +2.06% 0m16.94s | 591992 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_32.c | 0m16.89s | 549204 ko || +0m00.05s || 42788 ko | +0.29% | +7.79% 0m16.88s | 1097764 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m16.94s | 1091044 ko || -0m00.06s || 6720 ko | -0.35% | +0.61% 0m16.64s | 2058508 ko | ExtractionHaskell/solinas_reduction.hs | 0m16.27s | 2040460 ko || +0m00.37s || 18048 ko | +2.27% | +0.88% 0m16.64s | 545948 ko | fiat-bedrock2/src/p256_scalar_32.c | 0m16.81s | 582184 ko || -0m00.16s || -36236 ko | -1.01% | -6.22% 0m16.60s | 497404 ko | fiat-java/src/FiatP256Scalar.java | 0m16.49s | 465532 ko || +0m00.11s || 31872 ko | +0.66% | +6.84% 0m16.48s | 2015788 ko | ExtractionHaskell/word_by_word_montgomery.hs | 0m16.14s | 1994928 ko || +0m00.33s || 20860 ko | +2.10% | +1.04% 0m16.48s | 506704 ko | fiat-java/src/FiatSecp256K1MontgomeryScalar.java | 0m15.89s | 508152 ko || +0m00.58s || -1448 ko | +3.71% | -0.28% 0m16.37s | 532700 ko | fiat-bedrock2/src/curve25519_scalar_32.c | 0m16.47s | 561952 ko || -0m00.09s || -29252 ko | -0.60% | -5.20% 0m16.37s | 527676 ko | fiat-json/src/p256_scalar_32.json | 0m16.55s | 550516 ko || -0m00.17s || -22840 ko | -1.08% | -4.14% 0m16.29s | 2055344 ko | ExtractionHaskell/with_bedrock2_unsaturated_solinas.hs | 0m16.02s | 2032356 ko || +0m00.26s || 22988 ko | +1.68% | +1.13% 0m16.26s | 480716 ko | fiat-rust/src/p256_scalar_32.rs | 0m16.35s | 451796 ko || -0m00.08s || 28920 ko | -0.55% | +6.40% 0m16.19s | 494352 ko | fiat-go/32/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go | 0m16.30s | 436412 ko || -0m00.10s || 57940 ko | -0.67% | +13.27% 0m16.16s | 2056824 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs | 0m15.98s | 2031116 ko || +0m00.17s || 25708 ko | +1.12% | +1.26% 0m16.14s | 503672 ko | fiat-bedrock2/src/secp256k1_montgomery_32.c | 0m16.40s | 545704 ko || -0m00.25s || -42032 ko | -1.58% | -7.70% 0m16.04s | 480428 ko | fiat-go/32/p256scalar/p256scalar.go | 0m16.21s | 443600 ko || -0m00.17s || 36828 ko | -1.04% | +8.30% 0m16.04s | 496756 ko | fiat-zig/src/secp256k1_montgomery_scalar_32.zig | 0m16.10s | 501916 ko || -0m00.06s || -5160 ko | -0.37% | -1.02% 0m16.02s | 489128 ko | fiat-zig/src/p256_scalar_32.zig | 0m16.08s | 439752 ko || -0m00.05s || 49376 ko | -0.37% | +11.22% 0m16.01s | 503984 ko | fiat-rust/src/secp256k1_montgomery_scalar_32.rs | 0m16.08s | 440028 ko || -0m00.06s || 63956 ko | -0.43% | +14.53% 0m15.93s | 490732 ko | fiat-c/src/p256_scalar_32.c | 0m15.93s | 480884 ko || +0m00.00s || 9848 ko | +0.00% | +2.04% 0m15.90s | 486180 ko | fiat-java/src/FiatCurve25519Scalar.java | 0m16.31s | 435648 ko || -0m00.40s || 50532 ko | -2.51% | +11.59% 0m15.79s | 495508 ko | fiat-json/src/secp256k1_montgomery_32.json | 0m15.93s | 553532 ko || -0m00.14s || -58024 ko | -0.87% | -10.48% 0m15.78s | 476920 ko | fiat-c/src/secp256k1_montgomery_scalar_32.c | 0m15.82s | 443512 ko || -0m00.04s || 33408 ko | -0.25% | +7.53% 0m15.76s | 1973368 ko | ExtractionHaskell/unsaturated_solinas.hs | 0m15.46s | 1939424 ko || +0m00.29s || 33944 ko | +1.94% | +1.75% 0m15.76s | 488488 ko | fiat-json/src/curve25519_scalar_32.json | 0m16.04s | 542208 ko || -0m00.27s || -53720 ko | -1.74% | -9.90% 0m15.76s | 478272 ko | fiat-zig/src/secp256k1_montgomery_32.zig | 0m15.94s | 496368 ko || -0m00.17s || -18096 ko | -1.12% | -3.64% 0m15.74s | 502548 ko | fiat-rust/src/secp256k1_montgomery_32.rs | 0m15.76s | 496384 ko || -0m00.01s || 6164 ko | -0.12% | +1.24% 0m15.66s | 494864 ko | fiat-go/32/secp256k1montgomery/secp256k1montgomery.go | 0m15.69s | 494948 ko || -0m00.02s || -84 ko | -0.19% | -0.01% 0m15.66s | 440572 ko | fiat-java/src/FiatSecp256K1Montgomery.java | 0m15.74s | 504796 ko || -0m00.08s || -64224 ko | -0.50% | -12.72% 0m15.65s | 473036 ko | fiat-zig/src/curve25519_scalar_32.zig | 0m15.70s | 491508 ko || -0m00.04s || -18472 ko | -0.31% | -3.75% 0m15.57s | 498380 ko | fiat-json/src/secp256k1_montgomery_scalar_32.json | 0m16.14s | 567328 ko || -0m00.57s || -68948 ko | -3.53% | -12.15% 0m15.54s | 1106180 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m15.58s | 1105256 ko || -0m00.04s || 924 ko | -0.25% | +0.08% 0m15.52s | 485872 ko | fiat-go/32/curve25519scalar/curve25519scalar.go | 0m15.53s | 483400 ko || -0m00.00s || 2472 ko | -0.06% | +0.51% 0m15.49s | 485832 ko | fiat-c/src/curve25519_scalar_32.c | 0m15.43s | 450744 ko || +0m00.06s || 35088 ko | +0.38% | +7.78% 0m15.40s | 1126272 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m15.37s | 1128492 ko || +0m00.03s || -2220 ko | +0.19% | -0.19% 0m15.40s | 1980912 ko | ExtractionHaskell/with_bedrock2_dettman_multiplication.hs | 0m15.01s | 1952584 ko || +0m00.39s || 28328 ko | +2.59% | +1.45% 0m15.38s | 507964 ko | fiat-bedrock2/src/p256_32.c | 0m15.49s | 528008 ko || -0m00.10s || -20044 ko | -0.71% | -3.79% 0m15.37s | 477376 ko | fiat-c/src/secp256k1_montgomery_32.c | 0m15.35s | 494284 ko || +0m00.01s || -16908 ko | +0.13% | -3.42% 0m15.34s | 1980092 ko | ExtractionHaskell/bedrock2_dettman_multiplication.hs | 0m15.05s | 1952380 ko || +0m00.28s || 27712 ko | +1.92% | +1.41% 0m15.19s | 1979336 ko | ExtractionHaskell/with_bedrock2_base_conversion.hs | 0m14.79s | 1947364 ko || +0m00.40s || 31972 ko | +2.70% | +1.64% 0m15.16s | 492160 ko | fiat-rust/src/curve25519_scalar_32.rs | 0m16.08s | 483312 ko || -0m00.91s || 8848 ko | -5.72% | +1.83% 0m15.10s | 1979572 ko | ExtractionHaskell/bedrock2_base_conversion.hs | 0m14.77s | 1944640 ko || +0m00.33s || 34932 ko | +2.23% | +1.79% 0m15.03s | 1941608 ko | ExtractionHaskell/with_bedrock2_saturated_solinas.hs | 0m14.13s | 1944032 ko || +0m00.89s || -2424 ko | +6.36% | -0.12% 0m15.02s | 485556 ko | fiat-zig/src/p256_32.zig | 0m15.19s | 485712 ko || -0m00.16s || -156 ko | -1.11% | -0.03% 0m15.00s | 1941740 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs | 0m14.85s | 1945624 ko || +0m00.15s || -3884 ko | +1.01% | -0.19% 0m14.97s | 486152 ko | fiat-rust/src/p256_32.rs | 0m14.85s | 481172 ko || +0m00.12s || 4980 ko | +0.80% | +1.03% 0m14.95s | 476920 ko | fiat-json/src/p256_32.json | 0m15.11s | 516088 ko || -0m00.16s || -39168 ko | -1.05% | -7.58% 0m14.90s | 482212 ko | fiat-go/32/p256/p256.go | 0m15.07s | 477140 ko || -0m00.16s || 5072 ko | -1.12% | +1.06% 0m14.78s | 1881064 ko | ExtractionHaskell/saturated_solinas.hs | 0m14.38s | 1876668 ko || +0m00.39s || 4396 ko | +2.78% | +0.23% 0m14.72s | 491212 ko | fiat-java/src/FiatP256.java | 0m14.80s | 487264 ko || -0m00.08s || 3948 ko | -0.54% | +0.81% 0m14.41s | 1894732 ko | ExtractionHaskell/base_conversion.hs | 0m14.15s | 1859860 ko || +0m00.25s || 34872 ko | +1.83% | +1.87% 0m14.41s | 480184 ko | fiat-c/src/p256_32.c | 0m14.49s | 478564 ko || -0m00.08s || 1620 ko | -0.55% | +0.33% 0m13.98s | 1903704 ko | ExtractionHaskell/dettman_multiplication.hs | 0m14.51s | 1885976 ko || -0m00.52s || 17728 ko | -3.65% | +0.93% 0m13.15s | 1551964 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo | 0m13.08s | 1549676 ko || +0m00.07s || 2288 ko | +0.53% | +0.14% 0m10.83s | 249924 ko | fiat-bedrock2/src/p384_scalar_64.c | 0m10.84s | 248224 ko || -0m00.00s || 1700 ko | -0.09% | +0.68% 0m10.76s | 225128 ko | fiat-json/src/p384_scalar_64.json | 0m10.90s | 250920 ko || -0m00.14s || -25792 ko | -1.28% | -10.27% 0m10.75s | 206312 ko | fiat-rust/src/p384_scalar_64.rs | 0m10.59s | 206860 ko || +0m00.16s || -548 ko | +1.51% | -0.26% 0m10.69s | 199568 ko | fiat-go/64/p384scalar/p384scalar.go | 0m10.70s | 209512 ko || -0m00.00s || -9944 ko | -0.09% | -4.74% 0m10.60s | 204368 ko | fiat-c/src/p384_scalar_64.c | 0m10.54s | 194796 ko || +0m00.06s || 9572 ko | +0.56% | +4.91% 0m10.60s | 204528 ko | fiat-zig/src/p384_scalar_64.zig | 0m10.54s | 181860 ko || +0m00.06s || 22668 ko | +0.56% | +12.46% 0m10.26s | 1005728 ko | BoundsPipeline.vo | 0m10.25s | 999828 ko || +0m00.00s || 5900 ko | +0.09% | +0.59% 0m09.25s | 1247096 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo | 0m09.24s | 1245416 ko || +0m00.00s || 1680 ko | +0.10% | +0.13% 0m09.12s | 238524 ko | fiat-json/src/p384_64.json | 0m09.13s | 231860 ko || -0m00.01s || 6664 ko | -0.10% | +2.87% 0m09.10s | 255620 ko | fiat-bedrock2/src/p384_64.c | 0m09.08s | 247996 ko || +0m00.01s || 7624 ko | +0.22% | +3.07% 0m09.09s | 198100 ko | fiat-zig/src/p384_64.zig | 0m08.66s | 194384 ko || +0m00.42s || 3716 ko | +4.96% | +1.91% 0m09.01s | 362652 ko | fiat-bedrock2/src/p224_32.c | 0m09.01s | 359804 ko || +0m00.00s || 2848 ko | +0.00% | +0.79% 0m09.01s | 212280 ko | fiat-go/64/p384/p384.go | 0m09.09s | 209752 ko || -0m00.08s || 2528 ko | -0.88% | +1.20% 0m08.92s | 204084 ko | fiat-rust/src/p384_64.rs | 0m08.95s | 193392 ko || -0m00.02s || 10692 ko | -0.33% | +5.52% 0m08.89s | 321540 ko | fiat-json/src/p224_32.json | 0m08.82s | 345768 ko || +0m00.07s || -24228 ko | +0.79% | -7.00% 0m08.84s | 190600 ko | fiat-c/src/p384_64.c | 0m08.77s | 192560 ko || +0m00.07s || -1960 ko | +0.79% | -1.01% 0m08.81s | 304848 ko | fiat-rust/src/p224_32.rs | 0m08.76s | 295376 ko || +0m00.05s || 9472 ko | +0.57% | +3.20% 0m08.69s | 297896 ko | fiat-go/32/p224/p224.go | 0m08.77s | 272772 ko || -0m00.08s || 25124 ko | -0.91% | +9.21% 0m08.69s | 281356 ko | fiat-zig/src/p224_32.zig | 0m08.37s | 304612 ko || +0m00.32s || -23256 ko | +3.82% | -7.63% 0m08.68s | 309088 ko | fiat-java/src/FiatP224.java | 0m08.71s | 309156 ko || -0m00.03s || -68 ko | -0.34% | -0.02% 0m08.49s | 291880 ko | fiat-c/src/p224_32.c | 0m08.54s | 294312 ko || -0m00.04s || -2432 ko | -0.58% | -0.82% 0m08.31s | 140296 ko | fiat-json/src/p448_solinas_32.json | 0m08.31s | 138912 ko || +0m00.00s || 1384 ko | +0.00% | +0.99% 0m08.17s | 628572 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo | 0m08.16s | 628844 ko || +0m00.00s || -272 ko | +0.12% | -0.04% 0m08.08s | 997520 ko | PushButtonSynthesis/BaseConversion.vo | 0m07.98s | 996644 ko || +0m00.09s || 876 ko | +1.25% | +0.08% 0m07.95s | 79240 ko | fiat-rust/src/p448_solinas_32.rs | 0m07.90s | 81472 ko || +0m00.04s || -2232 ko | +0.63% | -2.73% 0m07.91s | 73556 ko | fiat-zig/src/p448_solinas_32.zig | 0m07.94s | 81352 ko || -0m00.03s || -7796 ko | -0.37% | -9.58% 0m07.84s | 971052 ko | PushButtonSynthesis/SmallExamples.vo | 0m07.79s | 964172 ko || +0m00.04s || 6880 ko | +0.64% | +0.71% 0m07.83s | 78696 ko | fiat-c/src/p448_solinas_32.c | 0m07.89s | 79452 ko || -0m00.05s || -756 ko | -0.76% | -0.95% 0m07.15s | 1013368 ko | PushButtonSynthesis/Primitives.vo | 0m07.25s | 1014352 ko || -0m00.09s || -984 ko | -1.37% | -0.09% 0m06.38s | 993404 ko | PushButtonSynthesis/SolinasReduction.vo | 0m06.38s | 991732 ko || +0m00.00s || 1672 ko | +0.00% | +0.16% 0m06.27s | 616792 ko | Rewriter/Passes/NoSelect.vo | 0m06.26s | 615456 ko || +0m00.00s || 1336 ko | +0.15% | +0.21% 0m06.26s | 59768 ko | fiat-go/64/p521/p521.go | 0m06.26s | 59896 ko || +0m00.00s || -128 ko | +0.00% | -0.21% 0m05.56s | 75132 ko | fiat-bedrock2/src/p521_64.c | 0m05.58s | 79276 ko || -0m00.02s || -4144 ko | -0.35% | -5.22% 0m05.43s | 1138132 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m05.18s | 1135688 ko || +0m00.25s || 2444 ko | +4.82% | +0.21% 0m05.42s | 1049972 ko | CLI.vo | 0m05.47s | 1047920 ko || -0m00.04s || 2052 ko | -0.91% | +0.19% 0m05.41s | 44772 ko | fiat-c/src/p521_64.c | 0m04.88s | 44296 ko || +0m00.53s || 476 ko | +10.86% | +1.07% 0m05.38s | 44544 ko | fiat-zig/src/p521_64.zig | 0m04.82s | 45056 ko || +0m00.55s || -512 ko | +11.61% | -1.13% 0m05.36s | 61792 ko | fiat-json/src/p521_64.json | 0m05.41s | 62016 ko || -0m00.04s || -224 ko | -0.92% | -0.36% 0m05.30s | 997084 ko | PushButtonSynthesis/BarrettReduction.vo | 0m05.37s | 989500 ko || -0m00.07s || 7584 ko | -1.30% | +0.76% 0m04.81s | 44036 ko | fiat-rust/src/p521_64.rs | 0m05.37s | 44100 ko || -0m00.56s || -64 ko | -10.42% | -0.14% 0m04.41s | 975388 ko | PushButtonSynthesis/DettmanMultiplication.vo | 0m04.32s | 978264 ko || +0m00.08s || -2876 ko | +2.08% | -0.29% 0m04.11s | 1004444 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m04.15s | 1002344 ko || -0m00.04s || 2100 ko | -0.96% | +0.20% 0m04.06s | 980500 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m04.08s | 986200 ko || -0m00.02s || -5700 ko | -0.49% | -0.57% 0m03.98s | 1409300 ko | Bedrock/Everything.vo | 0m04.11s | 1407144 ko || -0m00.13s || 2156 ko | -3.16% | +0.15% 0m03.84s | 1275180 ko | Everything.vo | 0m03.77s | 1273232 ko || +0m00.06s || 1948 ko | +1.85% | +0.15% 0m03.80s | 982844 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m03.77s | 981160 ko || +0m00.02s || 1684 ko | +0.79% | +0.17% 0m03.58s | 997692 ko | Rewriter/PerfTesting/Core.vo | 0m03.58s | 993660 ko || +0m00.00s || 4032 ko | +0.00% | +0.40% 0m03.52s | 1232872 ko | PerfTesting/PerfTestPrint.vo | 0m03.55s | 1231676 ko || -0m00.02s || 1196 ko | -0.84% | +0.09% 0m03.21s | 1008336 ko | StandaloneMonadicUtils.vo | 0m03.16s | 1006476 ko || +0m00.04s || 1860 ko | +1.58% | +0.18% 0m03.14s | 567764 ko | Rewriter/Passes/ArithWithRelaxedCasts.vo | 0m03.20s | 567876 ko || -0m00.06s || -112 ko | -1.87% | -0.01% 0m03.13s | 996084 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m03.09s | 994320 ko || +0m00.04s || 1764 ko | +1.29% | +0.17% 0m03.13s | 1037072 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m03.15s | 1034988 ko || -0m00.02s || 2084 ko | -0.63% | +0.20% 0m03.10s | 1035384 ko | Bedrock/Standalone/StandaloneJsOfOCamlMain.vo | 0m03.05s | 1033372 ko || +0m00.05s || 2012 ko | +1.63% | +0.19% 0m03.08s | 1005344 ko | StandaloneHaskellMain.vo | 0m03.04s | 1002224 ko || +0m00.04s || 3120 ko | +1.31% | +0.31% 0m03.02s | 1037312 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m03.12s | 1035308 ko || -0m00.10s || 2004 ko | -3.20% | +0.19% 0m03.02s | 575508 ko | Rewriter/Passes/AddAssocLeft.vo | 0m02.92s | 577532 ko || +0m00.10s || -2024 ko | +3.42% | -0.35% 0m03.01s | 999364 ko | Bedrock/Field/Stringification/Stringification.vo | 0m03.07s | 997148 ko || -0m00.06s || 2216 ko | -1.95% | +0.22% 0m03.00s | 938636 ko | Bedrock/Field/Translation/Cmd.vo | 0m03.06s | 942412 ko || -0m00.06s || -3776 ko | -1.96% | -0.40% 0m02.98s | 939264 ko | Bedrock/Field/Translation/Func.vo | 0m02.94s | 942940 ko || +0m00.04s || -3676 ko | +1.36% | -0.38% 0m02.97s | 1012892 ko | StandaloneJsOfOCamlMain.vo | 0m03.03s | 1011080 ko || -0m00.05s || 1812 ko | -1.98% | +0.17% 0m02.96s | 1012548 ko | StandaloneOCamlMain.vo | 0m03.05s | 1010580 ko || -0m00.08s || 1968 ko | -2.95% | +0.19% 0m02.92s | 1022664 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.89s | 1021240 ko || +0m00.02s || 1424 ko | +1.03% | +0.13% 0m02.89s | 971328 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m02.86s | 974964 ko || +0m00.03s || -3636 ko | +1.04% | -0.37% 0m02.88s | 995476 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m02.89s | 993312 ko || -0m00.01s || 2164 ko | -0.34% | +0.21% 0m02.88s | 971372 ko | Bedrock/Field/Translation/Parameters/FE310.vo | 0m02.87s | 975136 ko || +0m00.00s || -3764 ko | +0.34% | -0.38% 0m02.86s | 964220 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m02.84s | 967560 ko || +0m00.02s || -3340 ko | +0.70% | -0.34% 0m02.85s | 971540 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m02.88s | 975024 ko || -0m00.02s || -3484 ko | -1.04% | -0.35% 0m02.79s | 100444 ko | fiat-bedrock2/src/p256_scalar_64.c | 0m02.78s | 101444 ko || +0m00.01s || -1000 ko | +0.35% | -0.98% 0m02.76s | 101104 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_64.c | 0m02.71s | 99348 ko || +0m00.04s || 1756 ko | +1.84% | +1.76% 0m02.76s | 88556 ko | fiat-json/src/p256_scalar_64.json | 0m02.76s | 87104 ko || +0m00.00s || 1452 ko | +0.00% | +1.66% 0m02.74s | 87088 ko | fiat-json/src/secp256k1_montgomery_scalar_64.json | 0m02.68s | 89884 ko || +0m00.06s || -2796 ko | +2.23% | -3.11% 0m02.69s | 565928 ko | Rewriter/Passes/FlattenThunkedRects.vo | 0m02.70s | 566044 ko || -0m00.01s || -116 ko | -0.37% | -0.02% 0m02.67s | 71188 ko | fiat-rust/src/p256_scalar_64.rs | 0m02.70s | 72632 ko || -0m00.03s || -1444 ko | -1.11% | -1.98% 0m02.65s | 71568 ko | fiat-c/src/p256_scalar_64.c | 0m02.67s | 70884 ko || -0m00.02s || 684 ko | -0.74% | +0.96% 0m02.65s | 74164 ko | fiat-c/src/secp256k1_montgomery_scalar_64.c | 0m02.65s | 73872 ko || +0m00.00s || 292 ko | +0.00% | +0.39% 0m02.65s | 77536 ko | fiat-go/64/p256scalar/p256scalar.go | 0m02.70s | 77236 ko || -0m00.05s || 300 ko | -1.85% | +0.38% 0m02.65s | 73976 ko | fiat-rust/src/secp256k1_montgomery_scalar_64.rs | 0m02.65s | 73244 ko || +0m00.00s || 732 ko | +0.00% | +0.99% 0m02.65s | 72064 ko | fiat-zig/src/p256_scalar_64.zig | 0m02.67s | 70600 ko || -0m00.02s || 1464 ko | -0.74% | +2.07% 0m02.64s | 78004 ko | fiat-go/64/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go | 0m02.71s | 77792 ko || -0m00.06s || 212 ko | -2.58% | +0.27% 0m02.63s | 70176 ko | fiat-zig/src/secp256k1_montgomery_scalar_64.zig | 0m02.68s | 69524 ko || -0m00.05s || 652 ko | -1.86% | +0.93% 0m02.58s | 57468 ko | fiat-go/64/p448solinas/p448solinas.go | 0m02.57s | 58220 ko || +0m00.01s || -752 ko | +0.38% | -1.29% 0m02.47s | 87764 ko | fiat-json/src/secp256k1_montgomery_64.json | 0m02.40s | 89584 ko || +0m00.07s || -1820 ko | +2.91% | -2.03% 0m02.44s | 98212 ko | fiat-bedrock2/src/secp256k1_montgomery_64.c | 0m02.37s | 97792 ko || +0m00.06s || 420 ko | +2.95% | +0.42% 0m02.42s | 72468 ko | fiat-rust/src/secp256k1_montgomery_64.rs | 0m02.43s | 72696 ko || -0m00.01s || -228 ko | -0.41% | -0.31% 0m02.40s | 74216 ko | fiat-go/64/secp256k1montgomery/secp256k1montgomery.go | 0m02.36s | 73876 ko || +0m00.04s || 340 ko | +1.69% | +0.46% 0m02.39s | 71156 ko | fiat-zig/src/secp256k1_montgomery_64.zig | 0m02.38s | 70956 ko || +0m00.01s || 200 ko | +0.42% | +0.28% 0m02.35s | 70164 ko | fiat-c/src/secp256k1_montgomery_64.c | 0m02.35s | 72620 ko || +0m00.00s || -2456 ko | +0.00% | -3.38% 0m02.30s | 75052 ko | fiat-go/64/curve25519scalar/curve25519scalar.go | 0m02.28s | 72824 ko || +0m00.02s || 2228 ko | +0.87% | +3.05% 0m02.29s | 93720 ko | fiat-bedrock2/src/curve25519_scalar_64.c | 0m02.30s | 93748 ko || -0m00.00s || -28 ko | -0.43% | -0.02% 0m02.27s | 562884 ko | Rewriter/Passes/StripLiteralCasts.vo | 0m02.27s | 564888 ko || +0m00.00s || -2004 ko | +0.00% | -0.35% 0m02.26s | 71596 ko | fiat-rust/src/curve25519_scalar_64.rs | 0m02.29s | 71196 ko || -0m00.03s || 400 ko | -1.31% | +0.56% 0m02.25s | 85432 ko | fiat-json/src/curve25519_scalar_64.json | 0m02.35s | 86952 ko || -0m00.10s || -1520 ko | -4.25% | -1.74% 0m02.25s | 70124 ko | fiat-zig/src/curve25519_scalar_64.zig | 0m02.25s | 68708 ko || +0m00.00s || 1416 ko | +0.00% | +2.06% 0m02.22s | 566620 ko | Rewriter/Passes/UnfoldValueBarrier.vo | 0m02.28s | 566536 ko || -0m00.05s || 84 ko | -2.63% | +0.01% 0m02.19s | 69788 ko | fiat-c/src/curve25519_scalar_64.c | 0m02.21s | 69340 ko || -0m00.02s || 448 ko | -0.90% | +0.64% 0m02.15s | 567208 ko | Rewriter/Passes/ToFancy.vo | 0m02.20s | 567212 ko || -0m00.05s || -4 ko | -2.27% | -0.00% 0m02.13s | 45116 ko | fiat-go/32/curve25519/curve25519.go | 0m02.13s | 43576 ko || +0m00.00s || 1540 ko | +0.00% | +3.53% 0m02.05s | 77620 ko | fiat-bedrock2/src/p448_solinas_64.c | 0m02.07s | 77308 ko || -0m00.02s || 312 ko | -0.96% | +0.40% 0m02.00s | 75804 ko | fiat-bedrock2/src/curve25519_32.c | 0m01.98s | 76816 ko || +0m00.02s || -1012 ko | +1.01% | -1.31% 0m01.97s | 59824 ko | fiat-json/src/p448_solinas_64.json | 0m01.97s | 59328 ko || +0m00.00s || 496 ko | +0.00% | +0.83% 0m01.94s | 43708 ko | fiat-zig/src/p448_solinas_64.zig | 0m01.90s | 42340 ko || +0m00.04s || 1368 ko | +2.10% | +3.23% 0m01.92s | 42480 ko | fiat-c/src/p448_solinas_64.c | 0m01.89s | 41788 ko || +0m00.03s || 692 ko | +1.58% | +1.65% 0m01.92s | 42196 ko | fiat-rust/src/p448_solinas_64.rs | 0m01.92s | 43676 ko || +0m00.00s || -1480 ko | +0.00% | -3.38% 0m01.83s | 85452 ko | fiat-json/src/p224_64.json | 0m01.80s | 88012 ko || +0m00.03s || -2560 ko | +1.66% | -2.90% 0m01.83s | 87112 ko | fiat-json/src/p256_64.json | 0m01.81s | 86432 ko || +0m00.02s || 680 ko | +1.10% | +0.78% 0m01.82s | 96320 ko | fiat-bedrock2/src/p224_64.c | 0m01.87s | 95588 ko || -0m00.05s || 732 ko | -2.67% | +0.76% 0m01.81s | 41768 ko | fiat-zig/src/curve25519_32.zig | 0m01.79s | 41492 ko || +0m00.02s || 276 ko | +1.11% | +0.66% 0m01.81s | 69796 ko | fiat-zig/src/p224_64.zig | 0m01.79s | 69264 ko || +0m00.02s || 532 ko | +1.11% | +0.76% 0m01.80s | 94100 ko | fiat-bedrock2/src/p256_64.c | 0m01.77s | 91532 ko || +0m00.03s || 2568 ko | +1.69% | +2.80% 0m01.80s | 71228 ko | fiat-rust/src/p224_64.rs | 0m01.80s | 68468 ko || +0m00.00s || 2760 ko | +0.00% | +4.03% 0m01.79s | 41952 ko | fiat-java/src/FiatCurve25519.java | 0m01.74s | 42324 ko || +0m00.05s || -372 ko | +2.87% | -0.87% 0m01.78s | 59180 ko | fiat-json/src/curve25519_32.json | 0m01.89s | 60524 ko || -0m00.10s || -1344 ko | -5.82% | -2.22% 0m01.76s | 40544 ko | fiat-c/src/curve25519_32.c | 0m01.76s | 40876 ko || +0m00.00s || -332 ko | +0.00% | -0.81% 0m01.76s | 73780 ko | fiat-go/64/p224/p224.go | 0m01.75s | 73584 ko || +0m00.01s || 196 ko | +0.57% | +0.26% 0m01.76s | 73468 ko | fiat-go/64/p256/p256.go | 0m01.73s | 71364 ko || +0m00.03s || 2104 ko | +1.73% | +2.94% 0m01.75s | 69560 ko | fiat-zig/src/p256_64.zig | 0m01.74s | 70000 ko || +0m00.01s || -440 ko | +0.57% | -0.62% 0m01.74s | 41016 ko | fiat-rust/src/curve25519_32.rs | 0m01.80s | 41968 ko || -0m00.06s || -952 ko | -3.33% | -2.26% 0m01.72s | 68600 ko | fiat-c/src/p224_64.c | 0m01.74s | 69000 ko || -0m00.02s || -400 ko | -1.14% | -0.57% 0m01.70s | 69300 ko | fiat-c/src/p256_64.c | 0m01.68s | 68352 ko || +0m00.02s || 948 ko | +1.19% | +1.38% 0m01.70s | 69860 ko | fiat-rust/src/p256_64.rs | 0m01.74s | 70856 ko || -0m00.04s || -996 ko | -2.29% | -1.40% 0m01.66s | 617724 ko | CompilersTestCases.vo | 0m01.67s | 614372 ko || -0m00.01s || 3352 ko | -0.59% | +0.54% 0m01.43s | 63256 ko | fiat-bedrock2/src/secp256k1_dettman_32.c | 0m01.42s | 60252 ko || +0m00.01s || 3004 ko | +0.70% | +4.98% 0m01.22s | 32000 ko | fiat-go/32/secp256k1dettman/secp256k1dettman.go | 0m01.22s | 31548 ko || +0m00.00s || 452 ko | +0.00% | +1.43% 0m01.22s | 34668 ko | fiat-java/src/FiatSecp256K1Dettman.java | 0m01.22s | 33688 ko || +0m00.00s || 980 ko | +0.00% | +2.90% 0m01.22s | 49040 ko | fiat-json/src/secp256k1_dettman_32.json | 0m01.27s | 48936 ko || -0m00.05s || 104 ko | -3.93% | +0.21% 0m01.22s | 31852 ko | fiat-rust/src/secp256k1_dettman_32.rs | 0m01.21s | 31532 ko || +0m00.01s || 320 ko | +0.82% | +1.01% 0m01.22s | 32152 ko | fiat-zig/src/secp256k1_dettman_32.zig | 0m01.22s | 31720 ko || +0m00.00s || 432 ko | +0.00% | +1.36% 0m01.20s | 33024 ko | fiat-c/src/secp256k1_dettman_32.c | 0m01.21s | 32708 ko || -0m00.01s || 316 ko | -0.82% | +0.96% 0m00.93s | 571828 ko | Rewriter/All.vo | 0m00.98s | 568380 ko || -0m00.04s || 3448 ko | -5.10% | +0.60% 0m00.85s | 456204 ko | Rewriter/Rules.vo | 0m00.86s | 455820 ko || -0m00.01s || 384 ko | -1.16% | +0.08% 0m00.62s | 37376 ko | fiat-go/64/curve25519/curve25519.go | 0m00.62s | 36976 ko || +0m00.00s || 400 ko | +0.00% | +1.08% 0m00.50s | 43752 ko | fiat-bedrock2/src/curve25519_64.c | 0m00.50s | 43516 ko || +0m00.00s || 236 ko | +0.00% | +0.54% 0m00.50s | 40228 ko | fiat-json/src/curve25519_64.json | 0m00.48s | 39756 ko || +0m00.02s || 472 ko | +4.16% | +1.18% 0m00.48s | 31900 ko | fiat-zig/src/curve25519_64.zig | 0m00.48s | 30460 ko || +0m00.00s || 1440 ko | +0.00% | +4.72% 0m00.47s | 110692 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.cmi | 0m00.44s | 110484 ko || +0m00.02s || 208 ko | +6.81% | +0.18% 0m00.46s | 106976 ko | ExtractionOCaml/fiat_crypto.cmi | 0m00.44s | 106972 ko || +0m00.02s || 4 ko | +4.54% | +0.00% 0m00.46s | 31484 ko | fiat-rust/src/curve25519_64.rs | 0m00.47s | 31292 ko || -0m00.00s || 192 ko | -2.12% | +0.61% 0m00.45s | 105408 ko | ExtractionOCaml/base_conversion.cmi | 0m00.43s | 105420 ko || +0m00.02s || -12 ko | +4.65% | -0.01% 0m00.45s | 108780 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi | 0m00.45s | 108964 ko || +0m00.00s || -184 ko | +0.00% | -0.16% 0m00.45s | 107220 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi | 0m00.41s | 107104 ko || +0m00.04s || 116 ko | +9.75% | +0.10% 0m00.45s | 31516 ko | fiat-c/src/curve25519_64.c | 0m00.45s | 31172 ko || +0m00.00s || 344 ko | +0.00% | +1.10% 0m00.44s | 107500 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi | 0m00.47s | 107408 ko || -0m00.02s || 92 ko | -6.38% | +0.08% 0m00.44s | 109688 ko | ExtractionOCaml/bedrock2_fiat_crypto.cmi | 0m00.45s | 109576 ko || -0m00.01s || 112 ko | -2.22% | +0.10% 0m00.44s | 106768 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi | 0m00.45s | 106852 ko || -0m00.01s || -84 ko | -2.22% | -0.07% 0m00.44s | 108500 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi | 0m00.47s | 108388 ko || -0m00.02s || 112 ko | -6.38% | +0.10% 0m00.44s | 104152 ko | ExtractionOCaml/dettman_multiplication.cmi | 0m00.44s | 104116 ko || +0m00.00s || 36 ko | +0.00% | +0.03% 0m00.44s | 105080 ko | ExtractionOCaml/solinas_reduction.cmi | 0m00.43s | 104852 ko || +0m00.01s || 228 ko | +2.32% | +0.21% 0m00.44s | 105748 ko | ExtractionOCaml/unsaturated_solinas.cmi | 0m00.44s | 105948 ko || +0m00.00s || -200 ko | +0.00% | -0.18% 0m00.44s | 106800 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi | 0m00.44s | 106716 ko || +0m00.00s || 84 ko | +0.00% | +0.07% 0m00.44s | 105460 ko | ExtractionOCaml/word_by_word_montgomery.cmi | 0m00.46s | 105440 ko || -0m00.02s || 20 ko | -4.34% | +0.01% 0m00.43s | 106940 ko | ExtractionOCaml/bedrock2_base_conversion.cmi | 0m00.45s | 107388 ko || -0m00.02s || -448 ko | -4.44% | -0.41% 0m00.43s | 104764 ko | ExtractionOCaml/saturated_solinas.cmi | 0m00.44s | 104952 ko || -0m00.01s || -188 ko | -2.27% | -0.17% 0m00.43s | 106872 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi | 0m00.45s | 106864 ko || -0m00.02s || 8 ko | -4.44% | +0.00% 0m00.43s | 108272 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi | 0m00.45s | 108168 ko || -0m00.02s || 104 ko | -4.44% | +0.09% 0m00.43s | 108648 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi | 0m00.44s | 108860 ko || -0m00.01s || -212 ko | -2.27% | -0.19% 0m00.42s | 106768 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi | 0m00.44s | 106768 ko || -0m00.02s || 0 ko | -4.54% | +0.00% 0m00.42s | 107376 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi | 0m00.41s | 107212 ko || +0m00.01s || 164 ko | +2.43% | +0.15% 0m00.41s | 42764 ko | fiat-rust/src/curve25519_solinas_64.rs | 0m00.41s | 42420 ko || +0m00.00s || 344 ko | +0.00% | +0.81% 0m00.40s | 48292 ko | fiat-bedrock2/src/curve25519_solinas_64.c | 0m00.42s | 47448 ko || -0m00.01s || 844 ko | -4.76% | +1.77% 0m00.40s | 42028 ko | fiat-c/src/curve25519_solinas_64.c | 0m00.39s | 41920 ko || +0m00.01s || 108 ko | +2.56% | +0.25% 0m00.40s | 46448 ko | fiat-json/src/curve25519_solinas_64.json | 0m00.43s | 46028 ko || -0m00.02s || 420 ko | -6.97% | +0.91% 0m00.39s | 43412 ko | fiat-go/64/curve25519solinas/curve25519solinas.go | 0m00.42s | 43260 ko || -0m00.02s || 152 ko | -7.14% | +0.35% 0m00.39s | 42768 ko | fiat-zig/src/curve25519_solinas_64.zig | 0m00.40s | 41992 ko || -0m00.01s || 776 ko | -2.50% | +1.84% 0m00.30s | 29992 ko | fiat-go/32/poly1305/poly1305.go | 0m00.29s | 29464 ko || +0m00.01s || 528 ko | +3.44% | +1.79% 0m00.26s | 38380 ko | fiat-bedrock2/src/poly1305_32.c | 0m00.27s | 38752 ko || -0m00.01s || -372 ko | -3.70% | -0.95% 0m00.24s | 34972 ko | fiat-json/src/poly1305_32.json | 0m00.26s | 34748 ko || -0m00.02s || 224 ko | -7.69% | +0.64% 0m00.23s | 34312 ko | fiat-bedrock2/src/secp256k1_dettman_64.c | 0m00.22s | 33788 ko || +0m00.01s || 524 ko | +4.54% | +1.55% 0m00.23s | 28528 ko | fiat-zig/src/poly1305_32.zig | 0m00.22s | 28356 ko || +0m00.01s || 172 ko | +4.54% | +0.60% 0m00.22s | 28592 ko | fiat-go/64/secp256k1dettman/secp256k1dettman.go | 0m00.23s | 28316 ko || -0m00.01s || 276 ko | -4.34% | +0.97% 0m00.22s | 28756 ko | fiat-java/src/FiatPoly1305.java | 0m00.22s | 28688 ko || +0m00.00s || 68 ko | +0.00% | +0.23% 0m00.22s | 28888 ko | fiat-rust/src/poly1305_32.rs | 0m00.22s | 28596 ko || +0m00.00s || 292 ko | +0.00% | +1.02% 0m00.21s | 28244 ko | fiat-c/src/poly1305_32.c | 0m00.22s | 28308 ko || -0m00.01s || -64 ko | -4.54% | -0.22% 0m00.19s | 28908 ko | fiat-json/src/secp256k1_dettman_64.json | 0m00.19s | 28124 ko || +0m00.00s || 784 ko | +0.00% | +2.78% 0m00.18s | 24828 ko | fiat-rust/src/secp256k1_dettman_64.rs | 0m00.19s | 24608 ko || -0m00.01s || 220 ko | -5.26% | +0.89% 0m00.18s | 24692 ko | fiat-zig/src/secp256k1_dettman_64.zig | 0m00.18s | 24300 ko || +0m00.00s || 392 ko | +0.00% | +1.61% 0m00.17s | 61740 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi | 0m00.15s | 61852 ko || +0m00.02s || -112 ko | +13.33% | -0.18% 0m00.17s | 24668 ko | fiat-c/src/secp256k1_dettman_64.c | 0m00.17s | 24356 ko || +0m00.00s || 312 ko | +0.00% | +1.28% 0m00.17s | 29916 ko | fiat-go/64/poly1305/poly1305.go | 0m00.18s | 29392 ko || -0m00.00s || 524 ko | -5.55% | +1.78% 0m00.15s | 61552 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi | 0m00.17s | 61932 ko || -0m00.02s || -380 ko | -11.76% | -0.61% 0m00.13s | 31476 ko | fiat-json/src/poly1305_64.json | 0m00.13s | 31440 ko || +0m00.00s || 36 ko | +0.00% | +0.11% 0m00.12s | 31576 ko | fiat-bedrock2/src/poly1305_64.c | 0m00.12s | 31240 ko || +0m00.00s || 336 ko | +0.00% | +1.07% 0m00.12s | 26580 ko | fiat-c/src/poly1305_64.c | 0m00.12s | 26524 ko || +0m00.00s || 56 ko | +0.00% | +0.21% 0m00.12s | 27276 ko | fiat-rust/src/poly1305_64.rs | 0m00.12s | 26776 ko || +0m00.00s || 500 ko | +0.00% | +1.86% 0m00.12s | 26968 ko | fiat-zig/src/poly1305_64.zig | 0m00.12s | 26948 ko || +0m00.00s || 20 ko | +0.00% | +0.07% 0m00.00s | 4544 ko | ExtractionJsOfOCaml/bedrock2_fiat_crypto.cmi | 0m00.00s | 4664 ko || +0m00.00s || -120 ko | N/A | -2.57% 0m00.00s | 4508 ko | ExtractionJsOfOCaml/fiat_crypto.cmi | 0m00.00s | 4564 ko || +0m00.00s || -56 ko | N/A | -1.22% 0m00.00s | 4444 ko | ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.cmi | 0m00.00s | 4504 ko || +0m00.00s || -60 ko | N/A | -1.33% ``` </p> </details>
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.