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>

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] *)