Fixes mit-plv#1004 <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 167m47.39s | 2506548 ko | Total Time / Peak Mem | 168m57.12s | 2510796 ko || -1m09.73s || -4248 ko | -0.68% | -0.16% ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 1m30.42s | 1030880 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 1m09.57s | 1015932 ko || +0m20.85s || 14948 ko | +29.96% | +1.47% 10m46.03s | 994560 ko | fiat-rust/src/p384_32.rs | 10m59.00s | 994020 ko || -0m12.97s || 540 ko | -1.96% | +0.05% 13m18.11s | 989832 ko | fiat-json/src/p384_32.json | 13m28.59s | 990012 ko || -0m10.48s || -180 ko | -1.29% | -0.01% 10m55.45s | 1060096 ko | fiat-java/src/FiatP384.java | 11m04.32s | 1059280 ko || -0m08.87s || 816 ko | -1.33% | +0.07% 10m42.30s | 991092 ko | fiat-c/src/p384_32.c | 10m49.78s | 991592 ko || -0m07.48s || -500 ko | -1.15% | -0.05% 1m53.19s | 1504652 ko | Bedrock/Field/Synthesis/Examples/p256_64.vo | 1m59.30s | 1505920 ko || -0m06.10s || -1268 ko | -5.12% | -0.08% 6m36.70s | 1476820 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 6m42.52s | 1491412 ko || -0m05.81s || -14592 ko | -1.44% | -0.97% 2m21.71s | 1164144 ko | Bedrock/Field/Synthesis/Examples/X25519_64.vo | 2m27.35s | 1160964 ko || -0m05.63s || 3180 ko | -3.82% | +0.27% 0m50.66s | 1008892 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m44.96s | 973696 ko || +0m05.69s || 35196 ko | +12.67% | +3.61% 1m56.74s | 1533540 ko | Bedrock/Field/Synthesis/Examples/p224_64.vo | 2m00.84s | 1532848 ko || -0m04.09s || 692 ko | -3.39% | +0.04% 0m47.75s | 212516 ko | fiat-c/src/p256_32.c | 0m52.08s | 212096 ko || -0m04.32s || 420 ko | -8.31% | +0.19% 0m47.59s | 213768 ko | fiat-c/src/secp256k1_32.c | 0m52.53s | 213644 ko || -0m04.93s || 124 ko | -9.40% | +0.05% 0m21.05s | 97812 ko | fiat-go/64/p384/p384.go | 0m17.07s | 98044 ko || +0m03.98s || -232 ko | +23.31% | -0.23% 0m17.98s | 95308 ko | fiat-c/src/p384_64.c | 0m21.53s | 95376 ko || -0m03.55s || -68 ko | -16.48% | -0.07% 8m14.08s | 959044 ko | fiat-bedrock2/src/p384_32.c | 8m11.81s | 959584 ko || +0m02.26s || -540 ko | +0.46% | -0.05% 2m50.71s | 1664332 ko | Fancy/Barrett256.vo | 2m53.19s | 1665344 ko || -0m02.47s || -1012 ko | -1.43% | -0.06% 2m26.05s | 1802504 ko | SlowPrimeSynthesisExamples.vo | 2m28.53s | 1799396 ko || -0m02.47s || 3108 ko | -1.66% | +0.17% 1m47.61s | 1601200 ko | Fancy/Montgomery256.vo | 1m49.90s | 1600664 ko || -0m02.29s || 536 ko | -2.08% | +0.03% 1m37.01s | 1277412 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo | 1m39.84s | 1278916 ko || -0m02.83s || -1504 ko | -2.83% | -0.11% 1m11.35s | 213492 ko | fiat-json/src/secp256k1_32.json | 1m13.81s | 213536 ko || -0m02.46s || -44 ko | -3.33% | -0.02% 0m52.32s | 1646516 ko | ExtractionOCaml/bedrock2_unsaturated_solinas | 0m49.97s | 1639016 ko || +0m02.35s || 7500 ko | +4.70% | +0.45% 0m45.26s | 1237392 ko | ExtractionOCaml/perf_unsaturated_solinas | 0m43.09s | 1116852 ko || +0m02.16s || 120540 ko | +5.03% | +10.79% 0m45.18s | 213352 ko | fiat-java/src/FiatSecp256K1.java | 0m47.25s | 213644 ko || -0m02.07s || -292 ko | -4.38% | -0.13% 0m37.50s | 2017036 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml | 0m40.15s | 2010712 ko || -0m02.64s || 6324 ko | -6.60% | +0.31% 0m35.93s | 1739748 ko | ExtractionOCaml/base_conversion.ml | 0m38.18s | 1738396 ko || -0m02.25s || 1352 ko | -5.89% | +0.07% 0m32.61s | 155632 ko | fiat-c/src/p434_64.c | 0m34.61s | 155640 ko || -0m02.00s || -8 ko | -5.77% | -0.00% 0m32.14s | 945032 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m30.08s | 945716 ko || +0m02.06s || -684 ko | +6.84% | -0.07% 0m29.44s | 1673072 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs | 0m27.10s | 1655044 ko || +0m02.33s || 18028 ko | +8.63% | +1.08% 0m18.56s | 870988 ko | PushButtonSynthesis/Primitives.vo | 0m16.52s | 869256 ko || +0m02.03s || 1732 ko | +12.34% | +0.19% 11m00.87s | 1068324 ko | fiat-go/32/p384/p384.go | 11m02.17s | 1068328 ko || -0m01.29s || -4 ko | -0.19% | -0.00% 11m00.78s | 1078940 ko | fiat-zig/src/p384_32.zig | 11m01.99s | 1079008 ko || -0m01.21s || -68 ko | -0.18% | -0.00% 1m21.90s | 501912 ko | UnsaturatedSolinasHeuristics/Tests.vo | 1m23.05s | 501660 ko || -0m01.14s || 252 ko | -1.38% | +0.05% 1m12.01s | 2506548 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml | 1m13.56s | 2510796 ko || -0m01.54s || -4248 ko | -2.10% | -0.16% 1m11.58s | 2422688 ko | ExtractionOCaml/word_by_word_montgomery.ml | 1m09.81s | 2410400 ko || +0m01.76s || 12288 ko | +2.53% | +0.50% 1m05.36s | 190464 ko | fiat-json/src/p256_32.json | 1m06.77s | 190620 ko || -0m01.40s || -156 ko | -2.11% | -0.08% 0m49.88s | 1431908 ko | ExtractionOCaml/bedrock2_base_conversion | 0m48.81s | 1428348 ko || +0m01.07s || 3560 ko | +2.19% | +0.24% 0m47.32s | 1280600 ko | ExtractionOCaml/perf_word_by_word_montgomery | 0m48.33s | 1280924 ko || -0m01.00s || -324 ko | -2.08% | -0.02% 0m44.26s | 200112 ko | fiat-go/32/secp256k1/secp256k1.go | 0m45.86s | 200300 ko || -0m01.60s || -188 ko | -3.48% | -0.09% 0m43.78s | 1289712 ko | ExtractionOCaml/saturated_solinas | 0m45.23s | 1285976 ko || -0m01.44s || 3736 ko | -3.20% | +0.29% 0m43.36s | 192100 ko | fiat-go/32/p256/p256.go | 0m44.40s | 192236 ko || -0m01.03s || -136 ko | -2.34% | -0.07% 0m40.40s | 941208 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m41.81s | 940652 ko || -0m01.41s || 556 ko | -3.37% | +0.05% 0m39.91s | 1842276 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml | 0m41.05s | 1842884 ko || -0m01.14s || -608 ko | -2.77% | -0.03% 0m39.49s | 1014048 ko | Bedrock/Field/Synthesis/Examples/X1305_32.vo | 0m40.89s | 1010788 ko || -0m01.39s || 3260 ko | -3.42% | +0.32% 0m34.80s | 1934900 ko | ExtractionHaskell/word_by_word_montgomery.hs | 0m36.26s | 1933020 ko || -0m01.46s || 1880 ko | -4.02% | +0.09% 0m33.86s | 875176 ko | Bedrock/Field/Translation/Proofs/Expr.vo | 0m35.02s | 878144 ko || -0m01.16s || -2968 ko | -3.31% | -0.33% 0m33.66s | 156100 ko | fiat-go/64/p434/p434.go | 0m34.66s | 155964 ko || -0m01.00s || 136 ko | -2.88% | +0.08% 0m29.51s | 862420 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m31.12s | 856832 ko || -0m01.60s || 5588 ko | -5.17% | +0.65% 0m29.33s | 1054196 ko | StandaloneDebuggingExamples.vo | 0m28.30s | 1047808 ko || +0m01.02s || 6388 ko | +3.63% | +0.60% 0m28.02s | 703388 ko | Bedrock/Field/Common/Util.vo | 0m26.20s | 704208 ko || +0m01.82s || -820 ko | +6.94% | -0.11% 0m26.53s | 1586796 ko | ExtractionHaskell/unsaturated_solinas.hs | 0m25.21s | 1596536 ko || +0m01.32s || -9740 ko | +5.23% | -0.61% 0m24.39s | 1513040 ko | ExtractionHaskell/base_conversion.hs | 0m23.34s | 1515276 ko || +0m01.05s || -2236 ko | +4.49% | -0.14% 0m23.64s | 1500764 ko | ExtractionHaskell/saturated_solinas.hs | 0m25.49s | 1502900 ko || -0m01.84s || -2136 ko | -7.25% | -0.14% 0m13.27s | 45232 ko | fiat-c/src/p448_solinas_32.c | 0m14.66s | 45120 ko || -0m01.39s || 112 ko | -9.48% | +0.24% 0m12.30s | 868500 ko | Bedrock/Field/Synthesis/Specialized/Tactics.vo | 0m13.43s | 868568 ko || -0m01.12s || -68 ko | -8.41% | -0.00% 0m12.11s | 44420 ko | fiat-rust/src/p448_solinas_32.rs | 0m13.41s | 44432 ko || -0m01.30s || -12 ko | -9.69% | -0.02% 0m10.74s | 888228 ko | CLI.vo | 0m11.79s | 890172 ko || -0m01.04s || -1944 ko | -8.90% | -0.21% 2m17.58s | 1597528 ko | Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.vo | 2m16.79s | 1625328 ko || +0m00.78s || -27800 ko | +0.57% | -1.71% 2m14.64s | 1574264 ko | Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.vo | 2m15.48s | 1575564 ko || -0m00.84s || -1300 ko | -0.62% | -0.08% 1m23.63s | 2142696 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery | 1m23.29s | 2142172 ko || +0m00.34s || 524 ko | +0.40% | +0.02% 1m14.75s | 2142308 ko | ExtractionOCaml/word_by_word_montgomery | 1m14.90s | 2142076 ko || -0m00.15s || 232 ko | -0.20% | +0.01% 1m05.05s | 1062476 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 1m04.45s | 1061312 ko || +0m00.59s || 1164 ko | +0.93% | +0.10% 0m57.30s | 55872 ko | fiat-json/src/p448_solinas_32.json | 0m57.99s | 55500 ko || -0m00.69s || 372 ko | -1.18% | +0.67% 0m56.07s | 189636 ko | fiat-bedrock2/src/secp256k1_32.c | 0m55.24s | 189584 ko || +0m00.82s || 52 ko | +1.50% | +0.02% 0m55.17s | 129328 ko | fiat-json/src/p434_64.json | 0m55.16s | 128808 ko || +0m00.01s || 520 ko | +0.01% | +0.40% 0m53.02s | 1020924 ko | PushButtonSynthesis/BYInversionReificationCache.vo | 0m52.85s | 1020440 ko || +0m00.17s || 484 ko | +0.32% | +0.04% 0m50.57s | 1488592 ko | ExtractionOCaml/unsaturated_solinas | 0m50.39s | 1478260 ko || +0m00.17s || 10332 ko | +0.35% | +0.69% 0m49.52s | 202396 ko | fiat-bedrock2/src/p256_32.c | 0m49.86s | 202240 ko || -0m00.33s || 156 ko | -0.68% | +0.07% 0m47.82s | 1961712 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml | 0m47.34s | 1933588 ko || +0m00.47s || 28124 ko | +1.01% | +1.45% 0m47.20s | 999872 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m47.31s | 1000344 ko || -0m00.10s || -472 ko | -0.23% | -0.04% 0m47.12s | 1446184 ko | ExtractionOCaml/bedrock2_saturated_solinas | 0m47.85s | 1448096 ko || -0m00.73s || -1912 ko | -1.52% | -0.13% 0m45.67s | 229728 ko | fiat-zig/src/secp256k1_32.zig | 0m45.63s | 229692 ko || +0m00.03s || 36 ko | +0.08% | +0.01% 0m45.44s | 213668 ko | fiat-rust/src/secp256k1_32.rs | 0m45.46s | 213660 ko || -0m00.02s || 8 ko | -0.04% | +0.00% 0m44.73s | 229720 ko | fiat-zig/src/p256_32.zig | 0m44.54s | 229820 ko || +0m00.18s || -100 ko | +0.42% | -0.04% 0m44.51s | 1290244 ko | ExtractionOCaml/base_conversion | 0m44.98s | 1290756 ko || -0m00.46s || -512 ko | -1.04% | -0.03% 0m44.34s | 226668 ko | fiat-java/src/FiatP256.java | 0m44.82s | 226604 ko || -0m00.47s || 64 ko | -1.07% | +0.02% 0m43.87s | 187124 ko | fiat-rust/src/p256_32.rs | 0m44.29s | 187064 ko || -0m00.42s || 60 ko | -0.94% | +0.03% 0m43.50s | 1842872 ko | ExtractionOCaml/unsaturated_solinas.ml | 0m42.84s | 1834384 ko || +0m00.65s || 8488 ko | +1.54% | +0.46% 0m42.59s | 1833004 ko | ExtractionOCaml/bedrock2_base_conversion.ml | 0m42.35s | 1831124 ko || +0m00.24s || 1880 ko | +0.56% | +0.10% 0m37.64s | 1726124 ko | ExtractionOCaml/saturated_solinas.ml | 0m38.07s | 1726176 ko || -0m00.42s || -52 ko | -1.12% | -0.00% 0m37.38s | 158496 ko | fiat-bedrock2/src/p434_64.c | 0m36.54s | 158548 ko || +0m00.84s || -52 ko | +2.29% | -0.03% 0m37.22s | 2027984 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs | 0m36.56s | 2029736 ko || +0m00.65s || -1752 ko | +1.80% | -0.08% 0m37.18s | 1960904 ko | ExtractionOCaml/perf_unsaturated_solinas.ml | 0m37.18s | 1910908 ko || +0m00.00s || 49996 ko | +0.00% | +2.61% 0m33.84s | 155768 ko | fiat-zig/src/p434_64.zig | 0m33.90s | 155748 ko || -0m00.05s || 20 ko | -0.17% | +0.01% 0m33.58s | 138288 ko | fiat-rust/src/p434_64.rs | 0m34.11s | 138480 ko || -0m00.53s || -192 ko | -1.55% | -0.13% 0m33.53s | 123488 ko | fiat-json/src/p224_32.json | 0m34.18s | 123204 ko || -0m00.64s || 284 ko | -1.90% | +0.23% 0m30.40s | 945248 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m30.57s | 944644 ko || -0m00.17s || 604 ko | -0.55% | +0.06% 0m28.38s | 785036 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo | 0m28.55s | 785580 ko || -0m00.17s || -544 ko | -0.59% | -0.06% 0m27.64s | 95780 ko | fiat-json/src/p384_64.json | 0m27.93s | 95448 ko || -0m00.28s || 332 ko | -1.03% | +0.34% 0m27.55s | 1599472 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs | 0m26.88s | 1601520 ko || +0m00.67s || -2048 ko | +2.49% | -0.12% 0m27.43s | 1585616 ko | ExtractionHaskell/bedrock2_base_conversion.hs | 0m27.08s | 1583460 ko || +0m00.35s || 2156 ko | +1.29% | +0.13% 0m27.09s | 584716 ko | Arithmetic/BarrettReduction.vo | 0m27.54s | 583212 ko || -0m00.44s || 1504 ko | -1.63% | +0.25% 0m26.42s | 619252 ko | Arithmetic/WordByWordMontgomery.vo | 0m26.51s | 619116 ko || -0m00.08s || 136 ko | -0.33% | +0.02% 0m24.59s | 147200 ko | fiat-bedrock2/src/p224_32.c | 0m24.72s | 147140 ko || -0m00.12s || 60 ko | -0.52% | +0.04% 0m24.34s | 881208 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo | 0m24.57s | 879672 ko || -0m00.23s || 1536 ko | -0.93% | +0.17% 0m23.15s | 918500 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m23.78s | 918272 ko || -0m00.63s || 228 ko | -2.64% | +0.02% 0m21.37s | 131776 ko | fiat-go/32/p224/p224.go | 0m21.20s | 131808 ko || +0m00.17s || -32 ko | +0.80% | -0.02% 0m20.99s | 131016 ko | fiat-zig/src/p224_32.zig | 0m20.95s | 131244 ko || +0m00.03s || -228 ko | +0.19% | -0.17% 0m20.79s | 144964 ko | fiat-java/src/FiatP224.java | 0m20.89s | 144612 ko || -0m00.10s || 352 ko | -0.47% | +0.24% 0m20.27s | 138672 ko | fiat-c/src/p224_32.c | 0m20.45s | 138464 ko || -0m00.17s || 208 ko | -0.88% | +0.15% 0m20.23s | 128876 ko | fiat-rust/src/p224_32.rs | 0m20.55s | 128892 ko || -0m00.32s || -16 ko | -1.55% | -0.01% 0m19.82s | 89568 ko | fiat-bedrock2/src/p384_64.c | 0m20.05s | 89856 ko || -0m00.23s || -288 ko | -1.14% | -0.32% 0m18.49s | 932768 ko | PushButtonSynthesis/SmallExamples.vo | 0m18.07s | 932752 ko || +0m00.41s || 16 ko | +2.32% | +0.00% 0m18.02s | 861364 ko | PushButtonSynthesis/BaseConversion.vo | 0m17.82s | 862028 ko || +0m00.19s || -664 ko | +1.12% | -0.07% 0m16.45s | 97556 ko | fiat-rust/src/p384_64.rs | 0m16.78s | 97676 ko || -0m00.33s || -120 ko | -1.96% | -0.12% 0m16.45s | 94124 ko | fiat-zig/src/p384_64.zig | 0m16.68s | 94064 ko || -0m00.23s || 60 ko | -1.37% | +0.06% 0m14.87s | 541528 ko | Arithmetic/FancyMontgomeryReduction.vo | 0m14.73s | 540200 ko || +0m00.13s || 1328 ko | +0.95% | +0.24% 0m14.27s | 706648 ko | Bedrock/Field/Translation/Proofs/Flatten.vo | 0m14.15s | 707140 ko || +0m00.11s || -492 ko | +0.84% | -0.06% 0m14.02s | 906284 ko | Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.vo | 0m14.22s | 905868 ko || -0m00.20s || 416 ko | -1.40% | +0.04% 0m13.66s | 874980 ko | Bedrock/Field/Stringification/Stringification.vo | 0m13.00s | 875944 ko || +0m00.66s || -964 ko | +5.07% | -0.11% 0m13.60s | 994272 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo | 0m12.93s | 992536 ko || +0m00.67s || 1736 ko | +5.18% | +0.17% 0m13.27s | 866928 ko | PushButtonSynthesis/BarrettReduction.vo | 0m13.92s | 867048 ko || -0m00.65s || -120 ko | -4.66% | -0.01% 0m12.88s | 904616 ko | Rewriter/PerfTesting/Core.vo | 0m12.93s | 908364 ko || -0m00.04s || -3748 ko | -0.38% | -0.41% 0m12.87s | 874284 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m12.20s | 872340 ko || +0m00.67s || 1944 ko | +5.49% | +0.22% 0m12.63s | 40776 ko | fiat-zig/src/p448_solinas_32.zig | 0m13.19s | 44708 ko || -0m00.55s || -3932 ko | -4.24% | -8.79% 0m12.61s | 860568 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m12.15s | 858472 ko || +0m00.45s || 2096 ko | +3.78% | +0.24% 0m12.42s | 871420 ko | Bedrock/Field/Synthesis/Generic/Operation.vo | 0m12.71s | 871316 ko || -0m00.29s || 104 ko | -2.28% | +0.01% 0m12.40s | 865560 ko | Bedrock/Field/Synthesis/Generic/Tactics.vo | 0m12.83s | 866284 ko || -0m00.42s || -724 ko | -3.35% | -0.08% 0m11.71s | 885492 ko | Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.vo | 0m11.52s | 885384 ko || +0m00.19s || 108 ko | +1.64% | +0.01% 0m11.18s | 854544 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m10.94s | 851440 ko || +0m00.24s || 3104 ko | +2.19% | +0.36% 0m10.92s | 1007456 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo | 0m10.20s | 1006556 ko || +0m00.72s || 900 ko | +7.05% | +0.08% 0m10.66s | 670268 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m10.17s | 670920 ko || +0m00.49s || -652 ko | +4.81% | -0.09% 0m10.07s | 869884 ko | Bedrock/Field/Synthesis/Specialized/ReifiedOperation.vo | 0m09.87s | 872184 ko || +0m00.20s || -2300 ko | +2.02% | -0.26% 0m09.82s | 930236 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m09.98s | 927456 ko || -0m00.16s || 2780 ko | -1.60% | +0.29% 0m09.50s | 928584 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m10.00s | 927012 ko || -0m00.50s || 1572 ko | -5.00% | +0.16% 0m09.26s | 30208 ko | fiat-json/src/p521_64.json | 0m09.16s | 29768 ko || +0m00.09s || 440 ko | +1.09% | +1.47% 0m09.25s | 863460 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m09.99s | 862928 ko || -0m00.74s || 532 ko | -7.40% | +0.06% 0m09.22s | 593212 ko | Arithmetic/BYInv.vo | 0m08.85s | 595080 ko || +0m00.37s || -1868 ko | +4.18% | -0.31% 0m08.90s | 903492 ko | StandaloneHaskellMain.vo | 0m08.87s | 904560 ko || +0m00.03s || -1068 ko | +0.33% | -0.11% 0m08.68s | 808904 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m07.92s | 808884 ko || +0m00.75s || 20 ko | +9.59% | +0.00% 0m08.65s | 914244 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m08.76s | 914536 ko || -0m00.10s || -292 ko | -1.25% | -0.03% 0m08.59s | 805620 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m08.19s | 805380 ko || +0m00.40s || 240 ko | +4.88% | +0.02% 0m08.58s | 575980 ko | COperationSpecifications.vo | 0m09.15s | 573332 ko || -0m00.57s || 2648 ko | -6.22% | +0.46% 0m08.53s | 904568 ko | StandaloneOCamlMain.vo | 0m08.77s | 904936 ko || -0m00.24s || -368 ko | -2.73% | -0.04% 0m08.51s | 808504 ko | Bedrock/Field/Translation/Parameters/SelectParameters.vo | 0m09.28s | 807728 ko || -0m00.76s || 776 ko | -8.29% | +0.09% 0m07.80s | 809340 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m08.30s | 809704 ko || -0m00.50s || -364 ko | -6.02% | -0.04% 0m07.61s | 29316 ko | fiat-json/src/curve25519_32.json | 0m07.68s | 27416 ko || -0m00.06s || 1900 ko | -0.91% | +6.93% 0m07.29s | 531528 ko | UnsaturatedSolinasHeuristics.vo | 0m06.97s | 533744 ko || +0m00.32s || -2216 ko | +4.59% | -0.41% 0m06.99s | 29352 ko | fiat-json/src/p448_solinas_64.json | 0m06.98s | 27404 ko || +0m00.00s || 1948 ko | +0.14% | +7.10% 0m06.92s | 614460 ko | PushButtonSynthesis/BaseConversionReificationCache.vo | 0m06.59s | 614748 ko || +0m00.33s || -288 ko | +5.00% | -0.04% 0m06.79s | 39456 ko | fiat-json/src/secp256k1_64.json | 0m07.32s | 39588 ko || -0m00.53s || -132 ko | -7.24% | -0.33% 0m06.33s | 37148 ko | fiat-bedrock2/src/p521_64.c | 0m06.46s | 39404 ko || -0m00.12s || -2256 ko | -2.01% | -5.72% 0m06.13s | 25748 ko | fiat-c/src/p521_64.c | 0m05.99s | 25516 ko || +0m00.13s || 232 ko | +2.33% | +0.90% 0m06.10s | 30712 ko | fiat-go/64/p521/p521.go | 0m05.30s | 27000 ko || +0m00.79s || 3712 ko | +15.09% | +13.74% 0m05.87s | 520336 ko | Arithmetic/UniformWeight.vo | 0m05.77s | 522028 ko || +0m00.10s || -1692 ko | +1.73% | -0.32% 0m05.81s | 39400 ko | fiat-json/src/p256_64.json | 0m05.83s | 39348 ko || -0m00.02s || 52 ko | -0.34% | +0.13% 0m05.68s | 700472 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo | 0m05.71s | 700576 ko || -0m00.03s || -104 ko | -0.52% | -0.01% 0m05.67s | 704688 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo | 0m05.32s | 704464 ko || +0m00.34s || 224 ko | +6.57% | +0.03% 0m05.55s | 26064 ko | fiat-rust/src/p521_64.rs | 0m05.90s | 26796 ko || -0m00.35s || -732 ko | -5.93% | -2.73% 0m05.53s | 44912 ko | fiat-json/src/p224_64.json | 0m05.71s | 44964 ko || -0m00.17s || -52 ko | -3.15% | -0.11% 0m05.39s | 38548 ko | fiat-c/src/secp256k1_64.c | 0m05.52s | 38556 ko || -0m00.12s || -8 ko | -2.35% | -0.02% 0m05.25s | 705680 ko | Bedrock/Field/Common/Names/MakeNames.vo | 0m04.57s | 705772 ko || +0m00.67s || -92 ko | +14.87% | -0.01% 0m05.21s | 695372 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo | 0m04.54s | 695100 ko || +0m00.67s || 272 ko | +14.75% | +0.03% 0m05.12s | 43556 ko | fiat-bedrock2/src/secp256k1_64.c | 0m05.13s | 43488 ko || -0m00.00s || 68 ko | -0.19% | +0.15% 0m04.94s | 721376 ko | Bedrock/Field/Interface/Representation.vo | 0m05.37s | 719908 ko || -0m00.42s || 1468 ko | -8.00% | +0.20% 0m04.80s | 24340 ko | fiat-zig/src/p521_64.zig | 0m04.88s | 24188 ko || -0m00.08s || 152 ko | -1.63% | +0.62% 0m04.73s | 44108 ko | fiat-bedrock2/src/p224_64.c | 0m04.10s | 44228 ko || +0m00.63s || -120 ko | +15.36% | -0.27% 0m04.70s | 39556 ko | fiat-bedrock2/src/p448_solinas_64.c | 0m04.88s | 39364 ko || -0m00.17s || 192 ko | -3.68% | +0.48% 0m04.64s | 42072 ko | fiat-go/64/secp256k1/secp256k1.go | 0m04.53s | 42116 ko || +0m00.10s || -44 ko | +2.42% | -0.10% 0m04.60s | 40200 ko | fiat-bedrock2/src/curve25519_32.c | 0m04.61s | 36832 ko || -0m00.01s || 3368 ko | -0.21% | +9.14% 0m04.53s | 690024 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo | 0m04.27s | 694848 ko || +0m00.26s || -4824 ko | +6.08% | -0.69% 0m04.37s | 24192 ko | fiat-c/src/p448_solinas_64.c | 0m04.06s | 24472 ko || +0m00.31s || -280 ko | +7.63% | -1.14% 0m04.32s | 39292 ko | fiat-rust/src/secp256k1_64.rs | 0m04.40s | 39212 ko || -0m00.08s || 80 ko | -1.81% | +0.20% 0m04.26s | 28968 ko | fiat-go/64/p448solinas/p448solinas.go | 0m03.52s | 30600 ko || +0m00.73s || -1632 ko | +21.02% | -5.33% 0m04.17s | 39940 ko | fiat-zig/src/secp256k1_64.zig | 0m04.38s | 39692 ko || -0m00.20s || 248 ko | -4.79% | +0.62% 0m04.12s | 523336 ko | Arithmetic/Freeze.vo | 0m04.36s | 524432 ko || -0m00.24s || -1096 ko | -5.50% | -0.20% 0m03.93s | 41860 ko | fiat-go/64/p224/p224.go | 0m03.33s | 41720 ko || +0m00.60s || 140 ko | +18.01% | +0.33% 0m03.75s | 39824 ko | fiat-c/src/p256_64.c | 0m03.88s | 39868 ko || -0m00.12s || -44 ko | -3.35% | -0.11% 0m03.72s | 24412 ko | fiat-c/src/curve25519_32.c | 0m03.48s | 24200 ko || +0m00.24s || 212 ko | +6.89% | +0.87% 0m03.65s | 43108 ko | fiat-bedrock2/src/p256_64.c | 0m03.73s | 43624 ko || -0m00.08s || -516 ko | -2.14% | -1.18% 0m03.64s | 25724 ko | fiat-rust/src/curve25519_32.rs | 0m02.90s | 25220 ko || +0m00.74s || 504 ko | +25.51% | +1.99% 0m03.60s | 661292 ko | Bedrock/Field/Common/Tactics.vo | 0m03.56s | 661600 ko || +0m00.04s || -308 ko | +1.12% | -0.04% 0m03.36s | 24204 ko | fiat-rust/src/p448_solinas_64.rs | 0m04.13s | 24288 ko || -0m00.77s || -84 ko | -18.64% | -0.34% 0m03.27s | 24560 ko | fiat-go/32/curve25519/curve25519.go | 0m03.21s | 23108 ko || +0m00.06s || 1452 ko | +1.86% | +6.28% 0m03.24s | 41616 ko | fiat-zig/src/p224_64.zig | 0m03.27s | 41312 ko || -0m00.02s || 304 ko | -0.91% | +0.73% 0m03.16s | 39308 ko | fiat-go/64/p256/p256.go | 0m03.32s | 39536 ko || -0m00.15s || -228 ko | -4.81% | -0.57% 0m03.15s | 519688 ko | Arithmetic/BaseConversion.vo | 0m03.30s | 522428 ko || -0m00.14s || -2740 ko | -4.54% | -0.52% 0m03.15s | 24148 ko | fiat-zig/src/p448_solinas_64.zig | 0m03.15s | 25316 ko || +0m00.00s || -1168 ko | +0.00% | -4.61% 0m03.09s | 41412 ko | fiat-rust/src/p224_64.rs | 0m03.18s | 41588 ko || -0m00.09s || -176 ko | -2.83% | -0.42% 0m03.07s | 42884 ko | fiat-zig/src/p256_64.zig | 0m03.19s | 42884 ko || -0m00.12s || 0 ko | -3.76% | +0.00% 0m03.06s | 41604 ko | fiat-c/src/p224_64.c | 0m03.20s | 41932 ko || -0m00.14s || -328 ko | -4.37% | -0.78% 0m02.94s | 39984 ko | fiat-rust/src/p256_64.rs | 0m03.47s | 39768 ko || -0m00.53s || 216 ko | -15.27% | +0.54% 0m02.94s | 24576 ko | fiat-zig/src/curve25519_32.zig | 0m02.84s | 24292 ko || +0m00.10s || 284 ko | +3.52% | +1.16% 0m02.93s | 24428 ko | fiat-java/src/FiatCurve25519.java | 0m03.00s | 25500 ko || -0m00.06s || -1072 ko | -2.33% | -4.20% 0m02.07s | 525320 ko | Arithmetic/ModOps.vo | 0m01.99s | 528532 ko || +0m00.07s || -3212 ko | +4.02% | -0.60% 0m01.76s | 499044 ko | ArithmeticCPS/WordByWordMontgomery.vo | 0m01.71s | 497556 ko || +0m00.05s || 1488 ko | +2.92% | +0.29% 0m01.66s | 22912 ko | fiat-json/src/curve25519_64.json | 0m01.75s | 22772 ko || -0m00.09s || 140 ko | -5.14% | +0.61% 0m01.16s | 20388 ko | fiat-rust/src/curve25519_64.rs | 0m00.97s | 20364 ko || +0m00.18s || 24 ko | +19.58% | +0.11% 0m01.12s | 25064 ko | fiat-bedrock2/src/curve25519_64.c | 0m01.32s | 25772 ko || -0m00.19s || -708 ko | -15.15% | -2.74% 0m01.05s | 23080 ko | fiat-go/64/curve25519/curve25519.go | 0m00.91s | 22052 ko || +0m00.14s || 1028 ko | +15.38% | +4.66% 0m01.00s | 21268 ko | fiat-c/src/curve25519_64.c | 0m00.89s | 20848 ko || +0m00.10s || 420 ko | +12.35% | +2.01% 0m00.84s | 20644 ko | fiat-zig/src/curve25519_64.zig | 0m00.79s | 20284 ko || +0m00.04s || 360 ko | +6.32% | +1.77% 0m00.80s | 22032 ko | fiat-json/src/poly1305_32.json | 0m00.84s | 21132 ko || -0m00.03s || 900 ko | -4.76% | +4.25% 0m00.62s | 24056 ko | fiat-bedrock2/src/poly1305_32.c | 0m00.62s | 24072 ko || +0m00.00s || -16 ko | +0.00% | -0.06% 0m00.48s | 19292 ko | fiat-c/src/poly1305_32.c | 0m00.39s | 19160 ko || +0m00.08s || 132 ko | +23.07% | +0.68% 0m00.48s | 19940 ko | fiat-go/32/poly1305/poly1305.go | 0m00.45s | 19392 ko || +0m00.02s || 548 ko | +6.66% | +2.82% 0m00.47s | 19448 ko | fiat-rust/src/poly1305_32.rs | 0m00.40s | 19340 ko || +0m00.06s || 108 ko | +17.49% | +0.55% 0m00.46s | 20024 ko | fiat-json/src/poly1305_64.json | 0m00.46s | 19976 ko || +0m00.00s || 48 ko | +0.00% | +0.24% 0m00.44s | 19476 ko | fiat-zig/src/poly1305_32.zig | 0m00.37s | 19668 ko || +0m00.07s || -192 ko | +18.91% | -0.97% 0m00.41s | 20032 ko | fiat-java/src/FiatPoly1305.java | 0m00.36s | 19992 ko || +0m00.04s || 40 ko | +13.88% | +0.20% 0m00.30s | 21616 ko | fiat-bedrock2/src/poly1305_64.c | 0m00.30s | 21792 ko || +0m00.00s || -176 ko | +0.00% | -0.80% 0m00.30s | 19928 ko | fiat-go/64/poly1305/poly1305.go | 0m00.26s | 19232 ko || +0m00.03s || 696 ko | +15.38% | +3.61% 0m00.28s | 19028 ko | fiat-rust/src/poly1305_64.rs | 0m00.25s | 18924 ko || +0m00.03s || 104 ko | +12.00% | +0.54% 0m00.26s | 18936 ko | fiat-c/src/poly1305_64.c | 0m00.20s | 18896 ko || +0m00.06s || 40 ko | +30.00% | +0.21% 0m00.21s | 18976 ko | fiat-zig/src/poly1305_64.zig | 0m00.22s | 19016 ko || -0m00.01s || -40 ko | -4.54% | -0.21% ``` </p> </details>

Commits

Commits on Aug 4, 2021

Add carry_{add,sub,opp} operations to Go code