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)
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
125m19.92s | 4337192 ko | Total Time / Peak Mem                                             | 121m02.11s | 3709900 ko || +4m17.81s ||    627292 ko |     +3.55% |        +16.90%
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
  9m42.13s | 4337192 ko | Rewriter/Passes/NBE.vo                                            |   2m34.04s | 3317136 ko || +7m08.09s ||   1020056 ko |   +277.90% |        +30.75%
  5m28.68s | 3201708 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo                   |   0m18.21s | 1196664 ko || +5m10.47s ||   2005044 ko |  +1704.94% |       +167.55%
   N/A     |    N/A     | fiat-bedrock2/src/p384_scalar_32.c                                |   1m56.31s | 2430492 ko || -1m56.31s ||  -2430492 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-bedrock2/src/p384_32.c                                       |   1m50.66s | 2217956 ko || -1m50.65s ||  -2217956 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | ExtractionOCaml/with_bedrock2_word_by_word_montgomery             |   0m44.11s | 2631312 ko || -0m44.10s ||  -2631312 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | ExtractionOCaml/dettman_multiplication                            |   0m36.25s | 1931516 ko || -0m36.25s ||  -1931516 ko |   -100.00% |       -100.00%
  0m34.06s | 1755172 ko | ExtractionOCaml/perf_word_by_word_montgomery                      |   0m00.06s |   27632 ko || +0m34.00s ||   1727540 ko | +56666.66% |      +6251.95%
  0m07.87s | 1154620 ko | ExtractionOCaml/bedrock2_dettman_multiplication                   |   0m38.88s | 2247616 ko || -0m31.01s ||  -1092996 ko |    -79.75% |        -48.62%
  0m15.09s | 1793900 ko | ExtractionOCaml/solinas_reduction                                 |   0m42.14s | 2682524 ko || -0m27.05s ||   -888624 ko |    -64.19% |        -33.12%
  0m20.42s | 2272536 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas                 |   0m41.77s | 2536016 ko || -0m21.35s ||   -263480 ko |    -51.11% |        -10.38%
   N/A     |    N/A     | fiat-bedrock2/src/p434_64.c                                       |   0m17.54s |  395048 ko || -0m17.53s ||   -395048 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-bedrock2/src/p256_scalar_32.c                                |   0m16.44s |  582124 ko || -0m16.44s ||   -582124 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-bedrock2/src/secp256k1_montgomery_scalar_32.c                |   0m16.26s |  549024 ko || -0m16.26s ||   -549024 ko |   -100.00% |       -100.00%
  0m10.51s | 1436260 ko | ExtractionOCaml/dettman_multiplication.ml                         |   0m27.45s | 1986292 ko || -0m16.93s ||   -550032 ko |    -61.71% |        -27.69%
   N/A     |    N/A     | fiat-bedrock2/src/secp256k1_montgomery_32.c                       |   0m15.96s |  545668 ko || -0m15.96s ||   -545668 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-bedrock2/src/curve25519_scalar_32.c                          |   0m15.83s |  561700 ko || -0m15.83s ||   -561700 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-bedrock2/src/p256_32.c                                       |   0m14.52s |  527852 ko || -0m14.51s ||   -527852 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-bedrock2/src/p384_scalar_64.c                                |   0m10.63s |  248348 ko || -0m10.63s ||   -248348 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-bedrock2/src/p384_64.c                                       |   0m08.94s |  247848 ko || -0m08.93s ||   -247848 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-bedrock2/src/p224_32.c                                       |   0m08.81s |  359800 ko || -0m08.81s ||   -359800 ko |   -100.00% |       -100.00%
  0m37.47s | 2612000 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery                  |   0m43.94s | 2632436 ko || -0m06.46s ||    -20436 ko |    -14.72% |         -0.77%
  3m20.10s | 3453808 ko | Rewriter/Passes/ArithWithCasts.vo                                 |   3m24.42s | 3457324 ko || -0m04.32s ||     -3516 ko |     -2.11% |         -0.10%
  2m00.29s | 2196836 ko | fiat-go/32/p384/p384.go                                           |   1m56.07s | 2250852 ko || +0m04.22s ||    -54016 ko |     +3.63% |         -2.39%
  1m53.86s | 2273356 ko | fiat-go/32/p384scalar/p384scalar.go                               |   1m58.07s | 2317828 ko || -0m04.20s ||    -44472 ko |     -3.56% |         -1.91%
  0m04.01s | 1409008 ko | Bedrock/Everything.vo                                             |    N/A     |    N/A     || +0m04.00s ||   1409008 ko |          ∞ |              ∞
  0m37.42s |  138936 ko | fiat-json/src/p521_32.json                                        |   0m33.89s |  133296 ko || +0m03.53s ||      5640 ko |    +10.41% |         +4.23%
  1m52.17s | 2415720 ko | fiat-json/src/p384_32.json                                        |   1m54.90s | 2444672 ko || -0m02.73s ||    -28952 ko |     -2.37% |         -1.18%
  0m59.21s | 3703536 ko | ExtractionOCaml/with_bedrock2_fiat_crypto                         |   0m56.68s | 3709508 ko || +0m02.53s ||     -5972 ko |     +4.46% |         -0.16%
  0m41.38s | 2339900 ko | ExtractionOCaml/unsaturated_solinas                               |   0m39.29s | 2332668 ko || +0m02.09s ||      7232 ko |     +5.31% |         +0.31%
  0m41.08s | 2242080 ko | ExtractionOCaml/with_bedrock2_solinas_reduction                   |   0m38.77s | 2230172 ko || +0m02.30s ||     11908 ko |     +5.95% |         +0.53%
  0m40.80s | 2236980 ko | ExtractionOCaml/with_bedrock2_base_conversion                     |   0m38.63s | 2225172 ko || +0m02.16s ||     11808 ko |     +5.61% |         +0.53%
  0m40.77s | 2241348 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication              |   0m38.56s | 2228548 ko || +0m02.21s ||     12800 ko |     +5.73% |         +0.57%
  0m37.72s | 2045476 ko | ExtractionOCaml/base_conversion                                   |   0m35.37s | 1885096 ko || +0m02.35s ||    160380 ko |     +6.64% |         +8.50%
  0m37.62s | 2056036 ko | ExtractionOCaml/saturated_solinas                                 |   0m35.47s | 1905300 ko || +0m02.14s ||    150736 ko |     +6.06% |         +7.91%
   N/A     |    N/A     | fiat-bedrock2/src/p256_scalar_64.c                                |   0m02.70s |  101456 ko || -0m02.70s ||   -101456 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-bedrock2/src/secp256k1_montgomery_scalar_64.c                |   0m02.68s |   99516 ko || -0m02.68s ||    -99516 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-bedrock2/src/secp256k1_montgomery_64.c                       |   0m02.32s |   98040 ko || -0m02.31s ||    -98040 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-bedrock2/src/curve25519_scalar_64.c                          |   0m02.27s |   93692 ko || -0m02.27s ||    -93692 ko |   -100.00% |       -100.00%
  8m03.76s | 2662632 ko | Bedrock/End2End/X25519/GarageDoor.vo                              |   8m02.07s | 2662176 ko || +0m01.68s ||       456 ko |     +0.35% |         +0.01%
  1m53.86s | 2320964 ko | fiat-zig/src/p384_scalar_32.zig                                   |   1m55.37s | 2195532 ko || -0m01.51s ||    125432 ko |     -1.30% |         +5.71%
  1m52.52s | 2476384 ko | Rewriter/Passes/ToFancyWithCasts.vo                               |   1m53.68s | 2477588 ko || -0m01.15s ||     -1204 ko |     -1.02% |         -0.04%
  1m51.55s | 2290772 ko | fiat-c/src/p384_32.c                                              |   1m52.81s | 2324820 ko || -0m01.26s ||    -34048 ko |     -1.11% |         -1.46%
  0m57.46s | 3704644 ko | ExtractionOCaml/bedrock2_fiat_crypto                              |   0m55.94s | 3709900 ko || +0m01.52s ||     -5256 ko |     +2.71% |         -0.14%
  0m54.38s | 2479396 ko | ExtractionJsOfOCaml/fiat_crypto.ml                                |   0m53.32s | 2488132 ko || +0m01.06s ||     -8736 ko |     +1.98% |         -0.35%
  0m54.30s | 3722216 ko | ExtractionOCaml/fiat_crypto                                       |   0m52.74s | 3709380 ko || +0m01.55s ||     12836 ko |     +2.95% |         +0.34%
  0m45.63s | 2725464 ko | ExtractionOCaml/bedrock2_solinas_reduction                        |   0m43.64s | 2703368 ko || +0m01.99s ||     22096 ko |     +4.56% |         +0.81%
  0m43.43s | 2635148 ko | ExtractionOCaml/word_by_word_montgomery                           |   0m41.62s | 2621852 ko || +0m01.81s ||     13296 ko |     +4.34% |         +0.50%
  0m43.37s | 2543396 ko | ExtractionOCaml/bedrock2_unsaturated_solinas                      |   0m41.39s | 2537124 ko || +0m01.97s ||      6272 ko |     +4.78% |         +0.24%
  0m40.54s | 2242020 ko | ExtractionOCaml/with_bedrock2_saturated_solinas                   |   0m38.65s | 2229328 ko || +0m01.89s ||     12692 ko |     +4.89% |         +0.56%
  0m39.79s | 2234368 ko | ExtractionOCaml/bedrock2_base_conversion                          |   0m38.26s | 2224780 ko || +0m01.53s ||      9588 ko |     +3.99% |         +0.43%
  0m39.08s | 2240544 ko | ExtractionOCaml/bedrock2_saturated_solinas                        |   0m38.06s | 2229884 ko || +0m01.01s ||     10660 ko |     +2.67% |         +0.47%
  0m37.58s | 2252428 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml                     |   0m36.11s | 2263524 ko || +0m01.46s ||    -11096 ko |     +4.07% |         -0.49%
  0m33.68s | 1740208 ko | ExtractionOCaml/perf_unsaturated_solinas                          |   0m31.87s | 1694436 ko || +0m01.80s ||     45772 ko |     +5.67% |         +2.70%
  0m33.59s | 2165180 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml              |   0m31.89s | 2166272 ko || +0m01.70s ||     -1092 ko |     +5.33% |         -0.05%
   N/A     |    N/A     | fiat-bedrock2/src/p224_64.c                                       |   0m01.80s |   95640 ko || -0m01.80s ||    -95640 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-bedrock2/src/p256_64.c                                       |   0m01.78s |   91368 ko || -0m01.78s ||    -91368 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-bedrock2/src/secp256k1_dettman_32.c                          |   0m01.39s |   60176 ko || -0m01.38s ||    -60176 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-json/src/secp256k1_dettman_32.json                           |   0m01.28s |   48844 ko || -0m01.28s ||    -48844 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-go/32/secp256k1dettman/secp256k1dettman.go                   |   0m01.24s |   31380 ko || -0m01.24s ||    -31380 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-java/src/FiatSecp256K1Dettman.java                           |   0m01.21s |   33872 ko || -0m01.20s ||    -33872 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-c/src/secp256k1_dettman_32.c                                 |   0m01.20s |   32624 ko || -0m01.19s ||    -32624 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-zig/src/secp256k1_dettman_32.zig                             |   0m01.20s |   31720 ko || -0m01.19s ||    -31720 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-rust/src/secp256k1_dettman_32.rs                             |   0m01.17s |   31344 ko || -0m01.16s ||    -31344 ko |   -100.00% |       -100.00%
  4m37.50s | 2493852 ko | Bedrock/End2End/X25519/EdwardsXYZT.vo                             |   4m37.35s | 2490572 ko || +0m00.14s ||      3280 ko |     +0.05% |         +0.13%
  2m06.13s | 1391752 ko | Bedrock/End2End/X25519/Field25519.vo                              |   2m06.07s | 1386020 ko || +0m00.06s ||      5732 ko |     +0.04% |         +0.41%
  1m55.72s | 2461384 ko | fiat-json/src/p384_scalar_32.json                                 |   1m56.57s | 2162248 ko || -0m00.84s ||    299136 ko |     -0.72% |        +13.83%
  1m54.09s | 2328976 ko | fiat-rust/src/p384_scalar_32.rs                                   |   1m54.46s | 2298040 ko || -0m00.37s ||     30936 ko |     -0.32% |         +1.34%
  1m53.96s | 2264640 ko | fiat-c/src/p384_scalar_32.c                                       |   1m54.64s | 2315720 ko || -0m00.67s ||    -51080 ko |     -0.59% |         -2.20%
  1m52.88s | 2307516 ko | fiat-java/src/FiatP384.java                                       |   1m53.85s | 2326772 ko || -0m00.96s ||    -19256 ko |     -0.85% |         -0.82%
  1m52.26s | 2289988 ko | fiat-rust/src/p384_32.rs                                          |   1m53.15s | 2291956 ko || -0m00.89s ||     -1968 ko |     -0.78% |         -0.08%
  1m51.99s | 2321356 ko | fiat-zig/src/p384_32.zig                                          |   1m52.56s | 2285520 ko || -0m00.56s ||     35836 ko |     -0.50% |         +1.56%
  1m50.27s | 2142016 ko | fiat-java/src/FiatP384Scalar.java                                 |   1m50.35s | 2237492 ko || -0m00.07s ||    -95476 ko |     -0.07% |         -4.26%
  1m31.28s | 2069580 ko | Fancy/Barrett256.vo                                               |   1m30.31s | 2071284 ko || +0m00.96s ||     -1704 ko |     +1.07% |         -0.08%
  1m30.61s | 1959592 ko | SlowPrimeSynthesisExamples.vo                                     |   1m30.46s | 1949656 ko || +0m00.14s ||      9936 ko |     +0.16% |         +0.50%
  0m56.42s | 2599072 ko | ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.ml                  |   0m55.43s | 2577872 ko || +0m00.99s ||     21200 ko |     +1.78% |         +0.82%
  0m56.24s |  832904 ko | Rewriter/RulesProofs.vo                                           |   0m55.85s |  832184 ko || +0m00.39s ||       720 ko |     +0.69% |         +0.08%
  0m56.01s | 2599020 ko | ExtractionJsOfOCaml/bedrock2_fiat_crypto.ml                       |   0m55.34s | 2577860 ko || +0m00.66s ||     21160 ko |     +1.21% |         +0.82%
  0m55.93s | 2591660 ko | ExtractionOCaml/bedrock2_fiat_crypto.ml                           |   0m55.47s | 2582316 ko || +0m00.46s ||      9344 ko |     +0.82% |         +0.36%
  0m55.71s | 2590632 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.ml                      |   0m56.27s | 2582520 ko || -0m00.56s ||      8112 ko |     -0.99% |         +0.31%
  0m54.11s | 2479772 ko | ExtractionOCaml/fiat_crypto.ml                                    |   0m53.40s | 2488208 ko || +0m00.71s ||     -8436 ko |     +1.32% |         -0.33%
  0m50.54s | 1088688 ko | Rewriter/Passes/MultiRetSplit.vo                                  |   0m51.52s | 1089116 ko || -0m00.98s ||      -428 ko |     -1.90% |         -0.03%
  0m46.64s | 1839612 ko | Fancy/Montgomery256.vo                                            |   0m45.84s | 1884076 ko || +0m00.79s ||    -44464 ko |     +1.74% |         -2.35%
  0m40.72s | 1474472 ko | Rewriter/Passes/Arith.vo                                          |   0m41.24s | 1474564 ko || -0m00.52s ||       -92 ko |     -1.26% |         -0.00%
  0m40.26s |   89412 ko | fiat-go/32/p521/p521.go                                           |   0m40.48s |   89996 ko || -0m00.21s ||      -584 ko |     -0.54% |         -0.64%
  0m38.32s |  192600 ko | fiat-bedrock2/src/p521_32.c                                       |   0m38.14s |  191552 ko || +0m00.17s ||      1048 ko |     +0.47% |         +0.54%
  0m37.43s |   81368 ko | fiat-rust/src/p521_32.rs                                          |   0m37.40s |   82428 ko || +0m00.03s ||     -1060 ko |     +0.08% |         -1.28%
  0m37.26s |   82392 ko | fiat-c/src/p521_32.c                                              |   0m37.43s |   79576 ko || -0m00.17s ||      2816 ko |     -0.45% |         +3.53%
  0m37.21s |   85776 ko | fiat-java/src/FiatP521.java                                       |   0m37.36s |   83200 ko || -0m00.14s ||      2576 ko |     -0.40% |         +3.09%
  0m37.16s |   79880 ko | fiat-zig/src/p521_32.zig                                          |   0m37.01s |   84328 ko || +0m00.14s ||     -4448 ko |     +0.40% |         -5.27%
  0m37.01s | 2254764 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml               |   0m36.23s | 2209256 ko || +0m00.78s ||     45508 ko |     +2.15% |         +2.05%
  0m36.11s | 2223820 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml          |   0m36.20s | 2208892 ko || -0m00.09s ||     14928 ko |     -0.24% |         +0.67%
  0m35.73s | 2174540 ko | ExtractionOCaml/solinas_reduction.ml                              |   0m35.09s | 2145800 ko || +0m00.63s ||     28740 ko |     +1.82% |         +1.33%
  0m34.62s | 2145512 ko | ExtractionOCaml/word_by_word_montgomery.ml                        |   0m34.01s | 2117132 ko || +0m00.60s ||     28380 ko |     +1.79% |         +1.34%
  0m33.86s | 2166000 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml                   |   0m33.09s | 2165020 ko || +0m00.76s ||       980 ko |     +2.32% |         +0.04%
  0m32.98s |  898452 ko | Rewriter/Passes/MulSplit.vo                                       |   0m33.54s |  897384 ko || -0m00.56s ||      1068 ko |     -1.66% |         +0.11%
  0m32.19s | 1222428 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo                        |   0m32.14s | 1220432 ko || +0m00.04s ||      1996 ko |     +0.15% |         +0.16%
  0m31.72s | 2092236 ko | ExtractionOCaml/unsaturated_solinas.ml                            |   0m31.03s | 2033016 ko || +0m00.68s ||     59220 ko |     +2.22% |         +2.91%
  0m31.24s | 1258424 ko | Bedrock/End2End/X25519/GarageDoorTop.vo                           |   0m30.97s | 1256816 ko || +0m00.26s ||      1608 ko |     +0.87% |         +0.12%
  0m30.23s | 2082056 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml                |   0m29.49s | 2034984 ko || +0m00.74s ||     47072 ko |     +2.50% |         +2.31%
  0m29.54s | 2075228 ko | ExtractionOCaml/bedrock2_base_conversion.ml                       |   0m28.81s | 2027284 ko || +0m00.73s ||     47944 ko |     +2.53% |         +2.36%
  0m29.52s | 1481224 ko | StandaloneDebuggingExamples.vo                                    |   0m29.94s | 1478968 ko || -0m00.42s ||      2256 ko |     -1.40% |         +0.15%
  0m29.38s | 2075096 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml                  |   0m28.64s | 2027796 ko || +0m00.73s ||     47300 ko |     +2.58% |         +2.33%
  0m29.34s | 2069888 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml                |   0m28.56s | 2048480 ko || +0m00.78s ||     21408 ko |     +2.73% |         +1.04%
  0m29.30s | 2070080 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml                |   0m28.82s | 2047128 ko || +0m00.48s ||     22952 ko |     +1.66% |         +1.12%
  0m29.28s | 2054288 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml           |   0m28.58s | 2047664 ko || +0m00.70s ||      6624 ko |     +2.44% |         +0.32%
  0m29.16s | 2070516 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml                     |   0m28.51s | 2048116 ko || +0m00.64s ||     22400 ko |     +2.27% |         +1.09%
  0m27.55s | 1945716 ko | ExtractionOCaml/saturated_solinas.ml                              |   0m26.65s | 1912104 ko || +0m00.90s ||     33612 ko |     +3.37% |         +1.75%
  0m27.26s | 1954792 ko | ExtractionOCaml/base_conversion.ml                                |   0m26.63s | 1938284 ko || +0m00.63s ||     16508 ko |     +2.36% |         +0.85%
  0m25.05s | 1299504 ko | PerfTesting/PerfTestSearch.vo                                     |   0m24.95s | 1301992 ko || +0m00.10s ||     -2488 ko |     +0.40% |         -0.19%
  0m21.44s | 1907920 ko | ExtractionOCaml/perf_unsaturated_solinas.ml                       |   0m20.71s | 1833068 ko || +0m00.73s ||     74852 ko |     +3.52% |         +4.08%
  0m21.23s | 2436792 ko | ExtractionHaskell/bedrock2_fiat_crypto.hs                         |   0m21.16s | 2447800 ko || +0m00.07s ||    -11008 ko |     +0.33% |         -0.44%
  0m21.23s | 2435776 ko | ExtractionHaskell/with_bedrock2_fiat_crypto.hs                    |   0m20.95s | 2447456 ko || +0m00.28s ||    -11680 ko |     +1.33% |         -0.47%
  0m21.15s | 1899700 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml                   |   0m20.67s | 1929640 ko || +0m00.47s ||    -29940 ko |     +2.32% |         -1.55%
  0m20.96s | 2370116 ko | ExtractionHaskell/fiat_crypto.hs                                  |   0m20.37s | 2340672 ko || +0m00.58s ||     29444 ko |     +2.89% |         +1.25%
  0m20.62s | 1114588 ko | PushButtonSynthesis/UnsaturatedSolinas.vo                         |   0m20.58s | 1117168 ko || +0m00.04s ||     -2580 ko |     +0.19% |         -0.23%
  0m18.50s | 1115248 ko | PushButtonSynthesis/WordByWordMontgomery.vo                       |   0m18.50s | 1110356 ko || +0m00.00s ||      4892 ko |     +0.00% |         +0.44%
  0m18.44s | 1086396 ko | Bedrock/End2End/Poly1305/Field1305.vo                             |   0m18.46s | 1082940 ko || -0m00.01s ||      3456 ko |     -0.10% |         +0.31%
  0m17.32s | 2161028 ko | ExtractionHaskell/with_bedrock2_solinas_reduction.hs              |   0m16.78s | 2114384 ko || +0m00.53s ||     46644 ko |     +3.21% |         +2.20%
  0m17.30s |  320652 ko | fiat-go/64/p434/p434.go                                           |   0m16.86s |  344744 ko || +0m00.44s ||    -24092 ko |     +2.60% |         -6.98%
  0m17.20s | 2162464 ko | ExtractionHaskell/bedrock2_solinas_reduction.hs                   |   0m16.88s | 2115404 ko || +0m00.32s ||     47060 ko |     +1.89% |         +2.22%
  0m17.15s |  385316 ko | fiat-json/src/p434_64.json                                        |   0m17.12s |  354524 ko || +0m00.02s ||     30792 ko |     +0.17% |         +8.68%
  0m17.06s | 2147492 ko | ExtractionHaskell/with_bedrock2_word_by_word_montgomery.hs        |   0m16.69s | 2095396 ko || +0m00.36s ||     52096 ko |     +2.21% |         +2.48%
  0m17.02s | 2146908 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs             |   0m16.89s | 2095976 ko || +0m00.12s ||     50932 ko |     +0.76% |         +2.42%
  0m16.99s |  332764 ko | fiat-rust/src/p434_64.rs                                          |   0m16.90s |  331544 ko || +0m00.08s ||      1220 ko |     +0.53% |         +0.36%
  0m16.89s | 1292064 ko | PerfTesting/PerfTestSearchPattern.vo                              |   0m16.87s | 1289552 ko || +0m00.01s ||      2512 ko |     +0.11% |         +0.19%
  0m16.82s |  319012 ko | fiat-zig/src/p434_64.zig                                          |   0m16.88s |  332144 ko || -0m00.05s ||    -13132 ko |     -0.35% |         -3.95%
  0m16.81s |  327236 ko | fiat-c/src/p434_64.c                                              |   0m16.87s |  320400 ko || -0m00.06s ||      6836 ko |     -0.35% |         +2.13%
  0m16.26s | 2055032 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs                 |   0m15.72s | 2031520 ko || +0m00.54s ||     23512 ko |     +3.43% |         +1.15%
  0m16.19s | 1096356 ko | Bedrock/Field/Translation/Proofs/Func.vo                          |   0m15.54s | 1092824 ko || +0m00.65s ||      3532 ko |     +4.18% |         +0.32%
  0m16.19s | 2058840 ko | ExtractionHaskell/solinas_reduction.hs                            |   0m16.10s | 2039476 ko || +0m00.08s ||     19364 ko |     +0.55% |         +0.94%
  0m16.17s | 2011948 ko | ExtractionHaskell/word_by_word_montgomery.hs                      |   0m15.98s | 1994732 ko || +0m00.19s ||     17216 ko |     +1.18% |         +0.86%
  0m15.99s | 2055016 ko | ExtractionHaskell/with_bedrock2_unsaturated_solinas.hs            |   0m15.72s | 2032724 ko || +0m00.26s ||     22292 ko |     +1.71% |         +1.09%
  0m15.90s |  506520 ko | fiat-java/src/FiatSecp256K1MontgomeryScalar.java                  |   0m15.95s |  508156 ko || -0m00.04s ||     -1636 ko |     -0.31% |         -0.32%
  0m15.84s |  527800 ko | fiat-json/src/p256_scalar_32.json                                 |   0m15.92s |  550292 ko || -0m00.08s ||    -22492 ko |     -0.50% |         -4.08%
  0m15.74s |  498240 ko | fiat-json/src/secp256k1_montgomery_scalar_32.json                 |   0m15.77s |  567600 ko || -0m00.02s ||    -69360 ko |     -0.19% |        -12.21%
  0m15.73s |  497952 ko | fiat-java/src/FiatP256Scalar.java                                 |   0m15.62s |  465356 ko || +0m00.11s ||     32596 ko |     +0.70% |         +7.00%
  0m15.68s |  480272 ko | fiat-go/32/p256scalar/p256scalar.go                               |   0m15.55s |  443840 ko || +0m00.12s ||     36432 ko |     +0.83% |         +8.20%
  0m15.65s |  490776 ko | fiat-c/src/p256_scalar_32.c                                       |   0m15.55s |  480552 ko || +0m00.09s ||     10224 ko |     +0.64% |         +2.12%
  0m15.64s |  481120 ko | fiat-rust/src/p256_scalar_32.rs                                   |   0m15.60s |  451844 ko || +0m00.04s ||     29276 ko |     +0.25% |         +6.47%
  0m15.61s |  494700 ko | fiat-go/32/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go |   0m15.70s |  436556 ko || -0m00.08s ||     58144 ko |     -0.57% |        +13.31%
  0m15.59s |  495328 ko | fiat-json/src/secp256k1_montgomery_32.json                        |   0m15.64s |  553440 ko || -0m00.05s ||    -58112 ko |     -0.31% |        -10.50%
  0m15.59s |  504192 ko | fiat-rust/src/secp256k1_montgomery_scalar_32.rs                   |   0m15.67s |  439980 ko || -0m00.08s ||     64212 ko |     -0.51% |        +14.59%
  0m15.58s |  489428 ko | fiat-zig/src/p256_scalar_32.zig                                   |   0m15.73s |  439800 ko || -0m00.15s ||     49628 ko |     -0.95% |        +11.28%
  0m15.56s |  476852 ko | fiat-c/src/secp256k1_montgomery_scalar_32.c                       |   0m15.56s |  443348 ko || +0m00.00s ||     33504 ko |     +0.00% |         +7.55%
  0m15.55s |  496920 ko | fiat-zig/src/secp256k1_montgomery_scalar_32.zig                   |   0m15.51s |  501764 ko || +0m00.04s ||     -4844 ko |     +0.25% |         -0.96%
  0m15.47s |  502448 ko | fiat-rust/src/secp256k1_montgomery_32.rs                          |   0m15.43s |  495976 ko || +0m00.04s ||      6472 ko |     +0.25% |         +1.30%
  0m15.45s | 1104192 ko | Bedrock/Field/Translation/Proofs/Cmd.vo                           |   0m15.31s | 1101560 ko || +0m00.13s ||      2632 ko |     +0.91% |         +0.23%
  0m15.38s |  440600 ko | fiat-java/src/FiatSecp256K1Montgomery.java                        |   0m15.48s |  504996 ko || -0m00.09s ||    -64396 ko |     -0.64% |        -12.75%
  0m15.32s |  478516 ko | fiat-zig/src/secp256k1_montgomery_32.zig                          |   0m15.40s |  496520 ko || -0m00.08s ||    -18004 ko |     -0.51% |         -3.62%
  0m15.31s |  494924 ko | fiat-go/32/secp256k1montgomery/secp256k1montgomery.go             |   0m15.40s |  494840 ko || -0m00.08s ||        84 ko |     -0.58% |         +0.01%
  0m15.30s |  486492 ko | fiat-java/src/FiatCurve25519Scalar.java                           |   0m15.32s |  435568 ko || -0m00.01s ||     50924 ko |     -0.13% |        +11.69%
  0m15.29s | 1130412 ko | Bedrock/Field/Synthesis/New/Signature.vo                          |   0m15.34s | 1124752 ko || -0m00.05s ||      5660 ko |     -0.32% |         +0.50%
  0m15.28s | 1972964 ko | ExtractionHaskell/unsaturated_solinas.hs                          |   0m15.11s | 1940108 ko || +0m00.16s ||     32856 ko |     +1.12% |         +1.69%
  0m15.28s |  473416 ko | fiat-zig/src/curve25519_scalar_32.zig                             |   0m15.18s |  491132 ko || +0m00.09s ||    -17716 ko |     +0.65% |         -3.60%
  0m15.27s |  485840 ko | fiat-go/32/curve25519scalar/curve25519scalar.go                   |   0m15.12s |  483372 ko || +0m00.15s ||      2468 ko |     +0.99% |         +0.51%
  0m15.24s |  477328 ko | fiat-c/src/secp256k1_montgomery_32.c                              |   0m15.32s |  494028 ko || -0m00.08s ||    -16700 ko |     -0.52% |         -3.38%
  0m15.22s |  491884 ko | fiat-rust/src/curve25519_scalar_32.rs                             |   0m15.28s |  483372 ko || -0m00.05s ||      8512 ko |     -0.39% |         +1.76%
  0m15.16s | 1979980 ko | ExtractionHaskell/bedrock2_dettman_multiplication.hs              |   0m14.86s | 1951840 ko || +0m00.30s ||     28140 ko |     +2.01% |         +1.44%
  0m15.12s | 1979668 ko | ExtractionHaskell/with_bedrock2_dettman_multiplication.hs         |   0m14.89s | 1950340 ko || +0m00.22s ||     29328 ko |     +1.54% |         +1.50%
  0m15.03s |  485944 ko | fiat-c/src/curve25519_scalar_32.c                                 |   0m15.00s |  450824 ko || +0m00.02s ||     35120 ko |     +0.19% |         +7.79%
  0m14.96s | 1975912 ko | ExtractionHaskell/bedrock2_base_conversion.hs                     |   0m14.62s | 1944152 ko || +0m00.34s ||     31760 ko |     +2.32% |         +1.63%
  0m14.93s | 1975456 ko | ExtractionHaskell/with_bedrock2_base_conversion.hs                |   0m14.72s | 1945892 ko || +0m00.20s ||     29564 ko |     +1.42% |         +1.51%
  0m14.90s | 1940744 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs                   |   0m14.72s | 1945412 ko || +0m00.17s ||     -4668 ko |     +1.22% |         -0.23%
  0m14.82s | 1942936 ko | ExtractionHaskell/with_bedrock2_saturated_solinas.hs              |   0m14.75s | 1946856 ko || +0m00.07s ||     -3920 ko |     +0.47% |         -0.20%
  0m14.77s |  488968 ko | fiat-json/src/curve25519_scalar_32.json                           |   0m15.37s |  542368 ko || -0m00.59s ||    -53400 ko |     -3.90% |         -9.84%
  0m14.74s |  486248 ko | fiat-rust/src/p256_32.rs                                          |   0m14.69s |  480780 ko || +0m00.05s ||      5468 ko |     +0.34% |         +1.13%
  0m14.71s |  476972 ko | fiat-json/src/p256_32.json                                        |   0m14.78s |  516540 ko || -0m00.06s ||    -39568 ko |     -0.47% |         -7.66%
  0m14.57s |  482352 ko | fiat-go/32/p256/p256.go                                           |   0m14.60s |  476800 ko || -0m00.02s ||      5552 ko |     -0.20% |         +1.16%
  0m14.50s |  485760 ko | fiat-zig/src/p256_32.zig                                          |   0m14.58s |  485632 ko || -0m00.08s ||       128 ko |     -0.54% |         +0.02%
  0m14.46s | 1902592 ko | ExtractionHaskell/dettman_multiplication.hs                       |   0m14.18s | 1884012 ko || +0m00.28s ||     18580 ko |     +1.97% |         +0.98%
  0m14.43s |  480256 ko | fiat-c/src/p256_32.c                                              |   0m14.49s |  478808 ko || -0m00.06s ||      1448 ko |     -0.41% |         +0.30%
  0m14.29s | 1894708 ko | ExtractionHaskell/base_conversion.hs                              |   0m13.88s | 1860840 ko || +0m00.40s ||     33868 ko |     +2.95% |         +1.82%
  0m14.27s |  491324 ko | fiat-java/src/FiatP256.java                                       |   0m14.56s |  487596 ko || -0m00.29s ||      3728 ko |     -1.99% |         +0.76%
  0m14.26s | 1882348 ko | ExtractionHaskell/saturated_solinas.hs                            |   0m13.98s | 1872892 ko || +0m00.27s ||      9456 ko |     +2.00% |         +0.50%
  0m12.87s | 1551852 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo               |   0m12.92s | 1551400 ko || -0m00.05s ||       452 ko |     -0.38% |         +0.02%
  0m10.51s |  225240 ko | fiat-json/src/p384_scalar_64.json                                 |   0m10.51s |  251020 ko || +0m00.00s ||    -25780 ko |     +0.00% |        -10.27%
  0m10.42s |  199480 ko | fiat-go/64/p384scalar/p384scalar.go                               |   0m10.43s |  209852 ko || -0m00.00s ||    -10372 ko |     -0.09% |         -4.94%
  0m10.41s |  204396 ko | fiat-c/src/p384_scalar_64.c                                       |   0m10.43s |  194600 ko || -0m00.01s ||      9796 ko |     -0.19% |         +5.03%
  0m10.38s |  206196 ko | fiat-rust/src/p384_scalar_64.rs                                   |   0m10.35s |  206736 ko || +0m00.03s ||      -540 ko |     +0.28% |         -0.26%
  0m10.23s | 1004972 ko | BoundsPipeline.vo                                                 |   0m10.20s | 1000116 ko || +0m00.03s ||      4856 ko |     +0.29% |         +0.48%
  0m10.11s |  204688 ko | fiat-zig/src/p384_scalar_64.zig                                   |   0m10.06s |  181992 ko || +0m00.04s ||     22696 ko |     +0.49% |        +12.47%
  0m09.00s |  238480 ko | fiat-json/src/p384_64.json                                        |   0m09.05s |  231740 ko || -0m00.05s ||      6740 ko |     -0.55% |         +2.90%
  0m08.90s | 1248708 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo              |   0m09.07s | 1246884 ko || -0m00.16s ||      1824 ko |     -1.87% |         +0.14%
  0m08.86s |  212388 ko | fiat-go/64/p384/p384.go                                           |   0m08.92s |  209760 ko || -0m00.06s ||      2628 ko |     -0.67% |         +1.25%
  0m08.75s |  204100 ko | fiat-rust/src/p384_64.rs                                          |   0m08.83s |  193404 ko || -0m00.08s ||     10696 ko |     -0.90% |         +5.53%
  0m08.71s |  190620 ko | fiat-c/src/p384_64.c                                              |   0m08.77s |  192560 ko || -0m00.05s ||     -1940 ko |     -0.68% |         -1.00%
  0m08.55s |  309040 ko | fiat-java/src/FiatP224.java                                       |   0m08.53s |  309016 ko || +0m00.02s ||        24 ko |     +0.23% |         +0.00%
  0m08.50s |  304704 ko | fiat-rust/src/p224_32.rs                                          |   0m08.55s |  295280 ko || -0m00.05s ||      9424 ko |     -0.58% |         +3.19%
  0m08.45s |  298032 ko | fiat-go/32/p224/p224.go                                           |   0m08.37s |  272988 ko || +0m00.08s ||     25044 ko |     +0.95% |         +9.17%
  0m08.45s |  197948 ko | fiat-zig/src/p384_64.zig                                          |   0m08.86s |  194272 ko || -0m00.41s ||      3676 ko |     -4.62% |         +1.89%
  0m08.42s |  281584 ko | fiat-zig/src/p224_32.zig                                          |   0m08.34s |  304508 ko || +0m00.08s ||    -22924 ko |     +0.95% |         -7.52%
  0m08.36s |  292080 ko | fiat-c/src/p224_32.c                                              |   0m08.37s |  294116 ko || -0m00.00s ||     -2036 ko |     -0.11% |         -0.69%
  0m08.34s |  321564 ko | fiat-json/src/p224_32.json                                        |   0m08.65s |  345908 ko || -0m00.31s ||    -24344 ko |     -3.58% |         -7.03%
  0m08.14s |  140200 ko | fiat-json/src/p448_solinas_32.json                                |   0m08.21s |  138688 ko || -0m00.07s ||      1512 ko |     -0.85% |         +1.09%
  0m08.01s |  996516 ko | PushButtonSynthesis/BaseConversion.vo                             |   0m07.95s |  989088 ko || +0m00.05s ||      7428 ko |     +0.75% |         +0.75%
  0m07.97s |  632644 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo                            |   0m08.17s |  630336 ko || -0m00.20s ||      2308 ko |     -2.44% |         +0.36%
  0m07.93s |   79400 ko | fiat-rust/src/p448_solinas_32.rs                                  |   0m07.96s |   81460 ko || -0m00.03s ||     -2060 ko |     -0.37% |         -2.52%
  0m07.83s |   73844 ko | fiat-zig/src/p448_solinas_32.zig                                  |   0m07.79s |   81336 ko || +0m00.04s ||     -7492 ko |     +0.51% |         -9.21%
  0m07.79s |   78732 ko | fiat-c/src/p448_solinas_32.c                                      |   0m07.86s |   79276 ko || -0m00.07s ||      -544 ko |     -0.89% |         -0.68%
  0m07.46s |  971276 ko | PushButtonSynthesis/SmallExamples.vo                              |   0m07.72s |  968540 ko || -0m00.25s ||      2736 ko |     -3.36% |         +0.28%
  0m07.19s | 1016968 ko | PushButtonSynthesis/Primitives.vo                                 |   0m07.14s | 1013600 ko || +0m00.05s ||      3368 ko |     +0.70% |         +0.33%
  0m06.28s |  993068 ko | PushButtonSynthesis/SolinasReduction.vo                           |   0m06.34s |  997904 ko || -0m00.05s ||     -4836 ko |     -0.94% |         -0.48%
  0m06.22s |  616388 ko | Rewriter/Passes/NoSelect.vo                                       |   0m06.31s |  616404 ko || -0m00.08s ||       -16 ko |     -1.42% |         -0.00%
  0m06.12s |   59732 ko | fiat-go/64/p521/p521.go                                           |   0m06.14s |   60028 ko || -0m00.01s ||      -296 ko |     -0.32% |         -0.49%
  0m05.42s |   61860 ko | fiat-json/src/p521_64.json                                        |   0m05.44s |   61936 ko || -0m00.02s ||       -76 ko |     -0.36% |         -0.12%
  0m05.37s | 1135900 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo                 |   0m05.40s | 1127820 ko || -0m00.03s ||      8080 ko |     -0.55% |         +0.71%
  0m05.36s |   75076 ko | fiat-bedrock2/src/p521_64.c                                       |   0m04.85s |   79172 ko || +0m00.51s ||     -4096 ko |    +10.51% |         -5.17%
  0m05.36s |   44612 ko | fiat-c/src/p521_64.c                                              |   0m05.40s |   44276 ko || -0m00.04s ||       336 ko |     -0.74% |         +0.75%
  0m05.31s |   44092 ko | fiat-rust/src/p521_64.rs                                          |   0m05.35s |   43908 ko || -0m00.04s ||       184 ko |     -0.74% |         +0.41%
  0m05.30s |   44932 ko | fiat-zig/src/p521_64.zig                                          |   0m05.30s |   45176 ko || +0m00.00s ||      -244 ko |     +0.00% |         -0.54%
  0m05.23s |  996920 ko | PushButtonSynthesis/BarrettReduction.vo                           |   0m05.23s |  989348 ko || +0m00.00s ||      7572 ko |     +0.00% |         +0.76%
  0m05.11s | 1049968 ko | CLI.vo                                                            |   0m05.12s | 1052144 ko || -0m00.00s ||     -2176 ko |     -0.19% |         -0.20%
  0m04.27s |  975384 ko | PushButtonSynthesis/DettmanMultiplication.vo                      |   0m04.20s |  973544 ko || +0m00.06s ||      1840 ko |     +1.66% |         +0.18%
  0m04.01s | 1004524 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo           |   0m04.04s | 1002656 ko || -0m00.03s ||      1868 ko |     -0.74% |         +0.18%
  0m03.92s |  986288 ko | PushButtonSynthesis/SaturatedSolinas.vo                           |   0m04.00s |  986032 ko || -0m00.08s ||       256 ko |     -2.00% |         +0.02%
  0m03.89s | 1260988 ko | Everything.vo                                                     |   0m03.84s | 1259420 ko || +0m00.05s ||      1568 ko |     +1.30% |         +0.12%
  0m03.65s |  981568 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo                   |   0m03.66s |  985616 ko || -0m00.01s ||     -4048 ko |     -0.27% |         -0.41%
  0m03.45s | 1232876 ko | PerfTesting/PerfTestPrint.vo                                      |   0m03.43s | 1231896 ko || +0m00.02s ||       980 ko |     +0.58% |         +0.07%
  0m03.30s | 1009032 ko | Rewriter/PerfTesting/Core.vo                                      |   0m03.25s |  993788 ko || +0m00.04s ||     15244 ko |     +1.53% |         +1.53%
  0m03.13s |  568440 ko | Rewriter/Passes/ArithWithRelaxedCasts.vo                          |   0m03.12s |  568404 ko || +0m00.00s ||        36 ko |     +0.32% |         +0.00%
  0m03.11s | 1008240 ko | StandaloneMonadicUtils.vo                                         |   0m03.17s | 1006332 ko || -0m00.06s ||      1908 ko |     -1.89% |         +0.18%
  0m03.07s |  938864 ko | Bedrock/Field/Translation/Cmd.vo                                  |   0m03.10s |  942432 ko || -0m00.03s ||     -3568 ko |     -0.96% |         -0.37%
  0m03.04s | 1036936 ko | Bedrock/Standalone/StandaloneHaskellMain.vo                       |   0m03.05s | 1035024 ko || -0m00.00s ||      1912 ko |     -0.32% |         +0.18%
  0m03.04s | 1035364 ko | Bedrock/Standalone/StandaloneJsOfOCamlMain.vo                     |   0m02.91s | 1033368 ko || +0m00.12s ||      1996 ko |     +4.46% |         +0.19%
  0m03.03s | 1037124 ko | Bedrock/Standalone/StandaloneOCamlMain.vo                         |   0m03.05s | 1035300 ko || -0m00.02s ||      1824 ko |     -0.65% |         +0.17%
  0m03.02s | 1005396 ko | StandaloneHaskellMain.vo                                          |   0m03.06s | 1004508 ko || -0m00.04s ||       888 ko |     -1.30% |         +0.08%
  0m02.99s |  996484 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo          |   0m02.97s |  994484 ko || +0m00.02s ||      2000 ko |     +0.67% |         +0.20%
  0m02.97s |  939444 ko | Bedrock/Field/Translation/Func.vo                                 |   0m02.94s |  942808 ko || +0m00.03s ||     -3364 ko |     +1.02% |         -0.35%
  0m02.97s |  575436 ko | Rewriter/Passes/AddAssocLeft.vo                                   |   0m02.96s |  575508 ko || +0m00.01s ||       -72 ko |     +0.33% |         -0.01%
  0m02.96s |  999680 ko | Bedrock/Field/Stringification/Stringification.vo                  |   0m02.94s |  997464 ko || +0m00.02s ||      2216 ko |     +0.68% |         +0.22%
  0m02.93s | 1013008 ko | StandaloneJsOfOCamlMain.vo                                        |   0m02.93s | 1011048 ko || +0m00.00s ||      1960 ko |     +0.00% |         +0.19%
  0m02.89s | 1012680 ko | StandaloneOCamlMain.vo                                            |   0m02.94s | 1010756 ko || -0m00.04s ||      1924 ko |     -1.70% |         +0.19%
  0m02.83s |  971240 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo                |   0m02.85s |  974972 ko || -0m00.02s ||     -3732 ko |     -0.70% |         -0.38%
  0m02.82s |  971312 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo                |   0m02.83s |  974976 ko || -0m00.01s ||     -3664 ko |     -0.35% |         -0.37%
  0m02.80s |  971184 ko | Bedrock/Field/Translation/Parameters/FE310.vo                     |   0m02.88s |  974956 ko || -0m00.08s ||     -3772 ko |     -2.77% |         -0.38%
  0m02.79s |  963668 ko | Bedrock/Field/Translation/Parameters/Defaults.vo                  |   0m02.80s |  967484 ko || -0m00.00s ||     -3816 ko |     -0.35% |         -0.39%
  0m02.77s |  989712 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo                         |   0m02.79s |  993364 ko || -0m00.02s ||     -3652 ko |     -0.71% |         -0.36%
  0m02.72s | 1022452 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo                       |   0m02.92s | 1021420 ko || -0m00.19s ||      1032 ko |     -6.84% |         +0.10%
  0m02.70s |   87024 ko | fiat-json/src/secp256k1_montgomery_scalar_64.json                 |   0m02.69s |   89792 ko || +0m00.01s ||     -2768 ko |     +0.37% |         -3.08%
  0m02.69s |   88536 ko | fiat-json/src/p256_scalar_64.json                                 |   0m02.70s |   87080 ko || -0m00.01s ||      1456 ko |     -0.37% |         +1.67%
  0m02.68s |   78056 ko | fiat-go/64/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go |   0m02.65s |   77448 ko || +0m00.03s ||       608 ko |     +1.13% |         +0.78%
  0m02.64s |  566836 ko | Rewriter/Passes/FlattenThunkedRects.vo                            |   0m02.58s |  566824 ko || +0m00.06s ||        12 ko |     +2.32% |         +0.00%
  0m02.64s |   77940 ko | fiat-go/64/p256scalar/p256scalar.go                               |   0m02.65s |   77108 ko || -0m00.00s ||       832 ko |     -0.37% |         +1.07%
  0m02.64s |   74068 ko | fiat-rust/src/secp256k1_montgomery_scalar_64.rs                   |   0m02.62s |   73192 ko || +0m00.02s ||       876 ko |     +0.76% |         +1.19%
  0m02.63s |   71360 ko | fiat-c/src/p256_scalar_64.c                                       |   0m02.62s |   70824 ko || +0m00.00s ||       536 ko |     +0.38% |         +0.75%
  0m02.63s |   71752 ko | fiat-rust/src/p256_scalar_64.rs                                   |   0m02.66s |   72480 ko || -0m00.03s ||      -728 ko |     -1.12% |         -1.00%
  0m02.62s |   70460 ko | fiat-zig/src/secp256k1_montgomery_scalar_64.zig                   |   0m02.62s |   69520 ko || +0m00.00s ||       940 ko |     +0.00% |         +1.35%
  0m02.61s |   74116 ko | fiat-c/src/secp256k1_montgomery_scalar_64.c                       |   0m02.61s |   73576 ko || +0m00.00s ||       540 ko |     +0.00% |         +0.73%
  0m02.57s |   72276 ko | fiat-zig/src/p256_scalar_64.zig                                   |   0m02.61s |   70560 ko || -0m00.04s ||      1716 ko |     -1.53% |         +2.43%
  0m02.54s |   57268 ko | fiat-go/64/p448solinas/p448solinas.go                             |   0m02.52s |   57916 ko || +0m00.02s ||      -648 ko |     +0.79% |         -1.11%
  0m02.43s |   87696 ko | fiat-json/src/secp256k1_montgomery_64.json                        |   0m02.48s |   89372 ko || -0m00.04s ||     -1676 ko |     -2.01% |         -1.87%
  0m02.40s |   74332 ko | fiat-go/64/secp256k1montgomery/secp256k1montgomery.go             |   0m02.41s |   73928 ko || -0m00.01s ||       404 ko |     -0.41% |         +0.54%
  0m02.38s |   70228 ko | fiat-c/src/secp256k1_montgomery_64.c                              |   0m02.36s |   72916 ko || +0m00.02s ||     -2688 ko |     +0.84% |         -3.68%
  0m02.38s |   72360 ko | fiat-rust/src/secp256k1_montgomery_64.rs                          |   0m02.42s |   72692 ko || -0m00.04s ||      -332 ko |     -1.65% |         -0.45%
  0m02.36s |   71032 ko | fiat-zig/src/secp256k1_montgomery_64.zig                          |   0m02.37s |   70800 ko || -0m00.01s ||       232 ko |     -0.42% |         +0.32%
  0m02.26s |   85160 ko | fiat-json/src/curve25519_scalar_64.json                           |   0m02.26s |   86724 ko || +0m00.00s ||     -1564 ko |     +0.00% |         -1.80%
  0m02.23s |   69924 ko | fiat-c/src/curve25519_scalar_64.c                                 |   0m02.19s |   69180 ko || +0m00.04s ||       744 ko |     +1.82% |         +1.07%
  0m02.22s |   70000 ko | fiat-zig/src/curve25519_scalar_64.zig                             |   0m02.22s |   68600 ko || +0m00.00s ||      1400 ko |     +0.00% |         +2.04%
  0m02.21s |   71756 ko | fiat-rust/src/curve25519_scalar_64.rs                             |   0m02.22s |   71176 ko || -0m00.01s ||       580 ko |     -0.45% |         +0.81%
  0m02.20s |  563992 ko | Rewriter/Passes/StripLiteralCasts.vo                              |   0m02.23s |  563936 ko || -0m00.02s ||        56 ko |     -1.34% |         +0.00%
  0m02.19s |   75236 ko | fiat-go/64/curve25519scalar/curve25519scalar.go                   |   0m02.23s |   72760 ko || -0m00.04s ||      2476 ko |     -1.79% |         +3.40%
  0m02.18s |  566468 ko | Rewriter/Passes/UnfoldValueBarrier.vo                             |   0m02.24s |  566448 ko || -0m00.06s ||        20 ko |     -2.67% |         +0.00%
  0m02.07s |   44876 ko | fiat-go/32/curve25519/curve25519.go                               |   0m02.08s |   43820 ko || -0m00.01s ||      1056 ko |     -0.48% |         +2.40%
  0m02.06s |  567120 ko | Rewriter/Passes/ToFancy.vo                                        |   0m02.11s |  567120 ko || -0m00.04s ||         0 ko |     -2.36% |         +0.00%
  0m02.04s |   77844 ko | fiat-bedrock2/src/p448_solinas_64.c                               |   0m02.04s |   76924 ko || +0m00.00s ||       920 ko |     +0.00% |         +1.19%
  0m01.99s |   60264 ko | fiat-json/src/p448_solinas_64.json                                |   0m01.98s |   59236 ko || +0m00.01s ||      1028 ko |     +0.50% |         +1.73%
  0m01.94s |   42296 ko | fiat-rust/src/p448_solinas_64.rs                                  |   0m01.92s |   43556 ko || +0m00.02s ||     -1260 ko |     +1.04% |         -2.89%
  0m01.89s |   42540 ko | fiat-c/src/p448_solinas_64.c                                      |   0m01.89s |   42128 ko || +0m00.00s ||       412 ko |     +0.00% |         +0.97%
  0m01.88s |   75780 ko | fiat-bedrock2/src/curve25519_32.c                                 |   0m01.89s |   76316 ko || -0m00.01s ||      -536 ko |     -0.52% |         -0.70%
  0m01.87s |   59136 ko | fiat-json/src/curve25519_32.json                                  |   0m01.82s |   60668 ko || +0m00.05s ||     -1532 ko |     +2.74% |         -2.52%
  0m01.85s |   85200 ko | fiat-json/src/p224_64.json                                        |   0m01.76s |   88252 ko || +0m00.09s ||     -3052 ko |     +5.11% |         -3.45%
  0m01.83s |   43660 ko | fiat-zig/src/p448_solinas_64.zig                                  |   0m01.90s |   42244 ko || -0m00.06s ||      1416 ko |     -3.68% |         +3.35%
  0m01.81s |   87256 ko | fiat-json/src/p256_64.json                                        |   0m01.78s |   86468 ko || +0m00.03s ||       788 ko |     +1.68% |         +0.91%
  0m01.78s |   41772 ko | fiat-zig/src/curve25519_32.zig                                    |   0m01.78s |   41288 ko || +0m00.00s ||       484 ko |     +0.00% |         +1.17%
  0m01.77s |   40472 ko | fiat-c/src/curve25519_32.c                                        |   0m01.75s |   40936 ko || +0m00.02s ||      -464 ko |     +1.14% |         -1.13%
  0m01.77s |   73372 ko | fiat-go/64/p256/p256.go                                           |   0m01.72s |   71408 ko || +0m00.05s ||      1964 ko |     +2.90% |         +2.75%
  0m01.76s |   73804 ko | fiat-go/64/p224/p224.go                                           |   0m01.80s |   73552 ko || -0m00.04s ||       252 ko |     -2.22% |         +0.34%
  0m01.76s |   41092 ko | fiat-rust/src/curve25519_32.rs                                    |   0m01.73s |   41988 ko || +0m00.03s ||      -896 ko |     +1.73% |         -2.13%
  0m01.74s |   68544 ko | fiat-c/src/p224_64.c                                              |   0m01.74s |   69316 ko || +0m00.00s ||      -772 ko |     +0.00% |         -1.11%
  0m01.74s |   41964 ko | fiat-java/src/FiatCurve25519.java                                 |   0m01.76s |   42384 ko || -0m00.02s ||      -420 ko |     -1.13% |         -0.99%
  0m01.74s |   69496 ko | fiat-rust/src/p256_64.rs                                          |   0m01.70s |   71088 ko || +0m00.04s ||     -1592 ko |     +2.35% |         -2.23%
  0m01.74s |   69712 ko | fiat-zig/src/p224_64.zig                                          |   0m01.74s |   69472 ko || +0m00.00s ||       240 ko |     +0.00% |         +0.34%
  0m01.73s |   71260 ko | fiat-rust/src/p224_64.rs                                          |   0m01.74s |   68428 ko || -0m00.01s ||      2832 ko |     -0.57% |         +4.13%
  0m01.71s |   69352 ko | fiat-c/src/p256_64.c                                              |   0m01.71s |   68088 ko || +0m00.00s ||      1264 ko |     +0.00% |         +1.85%
  0m01.71s |   69644 ko | fiat-zig/src/p256_64.zig                                          |   0m01.72s |   70072 ko || -0m00.01s ||      -428 ko |     -0.58% |         -0.61%
  0m01.62s |  617916 ko | CompilersTestCases.vo                                             |   0m01.67s |  614276 ko || -0m00.04s ||      3640 ko |     -2.99% |         +0.59%
  0m00.92s |  571620 ko | Rewriter/All.vo                                                   |   0m00.96s |  566648 ko || -0m00.03s ||      4972 ko |     -4.16% |         +0.87%
  0m00.91s |  456024 ko | Rewriter/Rules.vo                                                 |   0m00.84s |  458148 ko || +0m00.07s ||     -2124 ko |     +8.33% |         -0.46%
  0m00.59s |   37240 ko | fiat-go/64/curve25519/curve25519.go                               |   0m00.61s |   36360 ko || -0m00.02s ||       880 ko |     -3.27% |         +2.42%
  0m00.49s |   43716 ko | fiat-bedrock2/src/curve25519_64.c                                 |   0m00.48s |   43712 ko || +0m00.01s ||         4 ko |     +2.08% |         +0.00%
  0m00.49s |   40156 ko | fiat-json/src/curve25519_64.json                                  |   0m00.51s |   39776 ko || -0m00.02s ||       380 ko |     -3.92% |         +0.95%
  0m00.48s |   31880 ko | fiat-c/src/curve25519_64.c                                        |   0m00.47s |   31008 ko || +0m00.01s ||       872 ko |     +2.12% |         +2.81%
  0m00.48s |   31544 ko | fiat-zig/src/curve25519_64.zig                                    |   0m00.46s |   30612 ko || +0m00.01s ||       932 ko |     +4.34% |         +3.04%
  0m00.45s |  109596 ko | ExtractionOCaml/bedrock2_fiat_crypto.cmi                          |   0m00.45s |  109588 ko || +0m00.00s ||         8 ko |     +0.00% |         +0.00%
  0m00.45s |  107072 ko | ExtractionOCaml/fiat_crypto.cmi                                   |   0m00.48s |  107100 ko || -0m00.02s ||       -28 ko |     -6.24% |         -0.02%
  0m00.44s |  106988 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi                    |   0m00.45s |  106772 ko || -0m00.01s ||       216 ko |     -2.22% |         +0.20%
  0m00.44s |  104996 ko | ExtractionOCaml/solinas_reduction.cmi                             |   0m00.39s |  104852 ko || +0m00.04s ||       144 ko |    +12.82% |         +0.13%
  0m00.44s |   31724 ko | fiat-rust/src/curve25519_64.rs                                    |   0m00.45s |   31432 ko || -0m00.01s ||       292 ko |     -2.22% |         +0.92%
  0m00.43s |  108484 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi              |   0m00.44s |  108552 ko || -0m00.01s ||       -68 ko |     -2.27% |         -0.06%
  0m00.42s |  108792 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi                  |   0m00.43s |  108796 ko || -0m00.01s ||        -4 ko |     -2.32% |         -0.00%
  0m00.42s |  106548 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi               |   0m00.41s |  106696 ko || +0m00.01s ||      -148 ko |     +2.43% |         -0.13%
  0m00.42s |  108120 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi             |   0m00.41s |  108344 ko || +0m00.01s ||      -224 ko |     +2.43% |         -0.20%
   N/A     |    N/A     | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi         |   0m00.42s |  108592 ko || -0m00.42s ||   -108592 ko |   -100.00% |       -100.00%
  0m00.41s |  106848 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi                    |   0m00.41s |  106912 ko || +0m00.00s ||       -64 ko |     +0.00% |         -0.05%
  0m00.41s |  105788 ko | ExtractionOCaml/unsaturated_solinas.cmi                           |   0m00.42s |  106072 ko || -0m00.01s ||      -284 ko |     -2.38% |         -0.26%
  0m00.41s |  107060 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi                 |   0m00.44s |  107368 ko || -0m00.03s ||      -308 ko |     -6.81% |         -0.28%
  0m00.41s |  107376 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi          |   0m00.41s |  107572 ko || +0m00.00s ||      -196 ko |     +0.00% |         -0.18%
  0m00.41s |  110628 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.cmi                     |   0m00.47s |  110712 ko || -0m00.06s ||       -84 ko |    -12.76% |         -0.07%
  0m00.41s |  106768 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi               |   0m00.42s |  106780 ko || -0m00.01s ||       -12 ko |     -2.38% |         -0.01%
  0m00.40s |  106936 ko | ExtractionOCaml/bedrock2_base_conversion.cmi                      |   0m00.40s |  107096 ko || +0m00.00s ||      -160 ko |     +0.00% |         -0.14%
  0m00.40s |  104704 ko | ExtractionOCaml/saturated_solinas.cmi                             |   0m00.42s |  104776 ko || -0m00.01s ||       -72 ko |     -4.76% |         -0.06%
  0m00.40s |  105528 ko | ExtractionOCaml/word_by_word_montgomery.cmi                       |   0m00.39s |  105420 ko || +0m00.01s ||       108 ko |     +2.56% |         +0.10%
   N/A     |    N/A     | fiat-json/src/curve25519_solinas_64.json                          |   0m00.40s |   46008 ko || -0m00.40s ||    -46008 ko |   -100.00% |       -100.00%
  0m00.39s |  107648 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi               |   0m00.42s |  107532 ko || -0m00.02s ||       116 ko |     -7.14% |         +0.10%
   N/A     |    N/A     | ExtractionOCaml/dettman_multiplication.cmi                        |   0m00.39s |  104104 ko || -0m00.39s ||   -104104 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-c/src/curve25519_solinas_64.c                                |   0m00.39s |   42048 ko || -0m00.39s ||    -42048 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-go/64/curve25519solinas/curve25519solinas.go                 |   0m00.39s |   42940 ko || -0m00.39s ||    -42940 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-zig/src/curve25519_solinas_64.zig                            |   0m00.39s |   42164 ko || -0m00.39s ||    -42164 ko |   -100.00% |       -100.00%
  0m00.38s |  105176 ko | ExtractionOCaml/base_conversion.cmi                               |   0m00.38s |  105136 ko || +0m00.00s ||        40 ko |     +0.00% |         +0.03%
  0m00.38s |   48488 ko | fiat-bedrock2/src/curve25519_solinas_64.c                         |   0m00.41s |   47512 ko || -0m00.02s ||       976 ko |     -7.31% |         +2.05%
   N/A     |    N/A     | fiat-rust/src/curve25519_solinas_64.rs                            |   0m00.38s |   42472 ko || -0m00.38s ||    -42472 ko |   -100.00% |       -100.00%
  0m00.30s |   29796 ko | fiat-go/32/poly1305/poly1305.go                                   |   0m00.29s |   29576 ko || +0m00.01s ||       220 ko |     +3.44% |         +0.74%
  0m00.26s |   38628 ko | fiat-bedrock2/src/poly1305_32.c                                   |   0m00.24s |   38816 ko || +0m00.02s ||      -188 ko |     +8.33% |         -0.48%
  0m00.24s |   28816 ko | fiat-java/src/FiatPoly1305.java                                   |   0m00.21s |   28308 ko || +0m00.03s ||       508 ko |    +14.28% |         +1.79%
  0m00.24s |   35080 ko | fiat-json/src/poly1305_32.json                                    |   0m00.24s |   34920 ko || +0m00.00s ||       160 ko |     +0.00% |         +0.45%
  0m00.22s |   28316 ko | fiat-c/src/poly1305_32.c                                          |   0m00.25s |   28008 ko || -0m00.03s ||       308 ko |    -12.00% |         +1.09%
   N/A     |    N/A     | fiat-go/64/secp256k1dettman/secp256k1dettman.go                   |   0m00.22s |   28508 ko || -0m00.22s ||    -28508 ko |   -100.00% |       -100.00%
  0m00.22s |   28476 ko | fiat-rust/src/poly1305_32.rs                                      |   0m00.24s |   28484 ko || -0m00.01s ||        -8 ko |     -8.33% |         -0.02%
   N/A     |    N/A     | fiat-bedrock2/src/secp256k1_dettman_64.c                          |   0m00.21s |   33628 ko || -0m00.21s ||    -33628 ko |   -100.00% |       -100.00%
  0m00.21s |   28428 ko | fiat-zig/src/poly1305_32.zig                                      |   0m00.21s |   28344 ko || +0m00.00s ||        84 ko |     +0.00% |         +0.29%
   N/A     |    N/A     | fiat-c/src/secp256k1_dettman_64.c                                 |   0m00.19s |   24484 ko || -0m00.19s ||    -24484 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-json/src/secp256k1_dettman_64.json                           |   0m00.19s |   28256 ko || -0m00.19s ||    -28256 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-rust/src/secp256k1_dettman_64.rs                             |   0m00.18s |   24736 ko || -0m00.18s ||    -24736 ko |   -100.00% |       -100.00%
   N/A     |    N/A     | fiat-zig/src/secp256k1_dettman_64.zig                             |   0m00.18s |   24564 ko || -0m00.18s ||    -24564 ko |   -100.00% |       -100.00%
  0m00.17s |   29876 ko | fiat-go/64/poly1305/poly1305.go                                   |   0m00.18s |   29452 ko || -0m00.00s ||       424 ko |     -5.55% |         +1.43%
  0m00.16s |   61844 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi                      |   0m00.18s |   61920 ko || -0m00.01s ||       -76 ko |    -11.11% |         -0.12%
  0m00.16s |   61640 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi                  |   0m00.18s |   61720 ko || -0m00.01s ||       -80 ko |    -11.11% |         -0.12%
  0m00.13s |   26840 ko | fiat-c/src/poly1305_64.c                                          |   0m00.13s |   26520 ko || +0m00.00s ||       320 ko |     +0.00% |         +1.20%
  0m00.13s |   31516 ko | fiat-json/src/poly1305_64.json                                    |   0m00.12s |   31220 ko || +0m00.01s ||       296 ko |     +8.33% |         +0.94%
  0m00.13s |   27116 ko | fiat-rust/src/poly1305_64.rs                                      |   0m00.13s |   26708 ko || +0m00.00s ||       408 ko |     +0.00% |         +1.52%
  0m00.12s |   26824 ko | fiat-zig/src/poly1305_64.zig                                      |   0m00.12s |   26772 ko || +0m00.00s ||        52 ko |     +0.00% |         +0.19%
  0m00.11s |   31524 ko | fiat-bedrock2/src/poly1305_64.c                                   |   0m00.13s |   31756 ko || -0m00.02s ||      -232 ko |    -15.38% |         -0.73%
  0m00.00s |    4632 ko | ExtractionJsOfOCaml/bedrock2_fiat_crypto.cmi                      |   0m00.00s |    4636 ko || +0m00.00s ||        -4 ko |    N/A     |         -0.08%
  0m00.00s |    4508 ko | ExtractionJsOfOCaml/fiat_crypto.cmi                               |   0m00.00s |    4448 ko || +0m00.00s ||        60 ko |    N/A     |         +1.34%
  0m00.00s |    4496 ko | ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.cmi                 |   0m00.00s |    4368 ko || +0m00.00s ||       128 ko |    N/A     |         +2.93%

```
</p>
</details>

src/Rewriter/Rules.v

@@ -183,6 +183,13 @@ Definition nbe_rewrite_rulesT : list (bool * Prop)
                             end)
                         ('n)
                         xs)
+              ; typeof! @unfold1_nat_rect_fbb_b
+              ; typeof! @unfold1_nat_rect_fbb_b_b
+              ; typeof! @unfold1_list_rect_fbb_b
+              ; typeof! @unfold1_list_rect_fbb_b_b
+              ; typeof! @unfold1_list_rect_fbb_b_b_b
+              ; typeof! @unfold1_list_rect_fbb_b_b_b_b
+              ; typeof! @unfold1_list_rect_fbb_b_b_b_b_b
              ]
         ].
 

src/Rewriter/RulesProofs.v

@@ -90,6 +90,13 @@ Local Hint Resolve
       eq_firstn_nat_rect
       eq_skipn_nat_rect
       eq_update_nth_nat_rect
+      unfold1_nat_rect_fbb_b
+      unfold1_nat_rect_fbb_b_b
+      unfold1_list_rect_fbb_b
+      unfold1_list_rect_fbb_b_b
+      unfold1_list_rect_fbb_b_b_b
+      unfold1_list_rect_fbb_b_b_b_b
+      unfold1_list_rect_fbb_b_b_b_b_b
   : core.
 
 (* to catch [prod_rect] and not just [prod_rect_nodep] *)