Skip to content

Commit

Permalink
Unobjectionable rewrite rules for saturated arithmetic
Browse files Browse the repository at this point in the history 
For https://github.com/mit-plv/fiat-crypto/pull/1609

We don't yet include the ones that are higher-order-than 3, those need
more debugging.

Co-authored-by: Andres Erbsen <andres-github@andres.systems>

<details><summary>Timing Diff</summary>
<p>

```
     After |   Peak Mem | File Name                                                         |     Before |   Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
119m55.01s | 2852288 ko | Total Time / Peak Mem                                             | 116m54.82s | 2852504 ko || +3m00.19s ||      -216 ko |   +2.56% |         -0.00%
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
  4m23.28s | 1922200 ko | Rewriter/Passes/ArithWithCasts.vo                                 |   3m44.64s | 1804812 ko || +0m38.63s ||    117388 ko |  +17.20% |         +6.50%
  1m56.74s | 1630248 ko | fiat-java/src/FiatP384Scalar.java                                 |   1m37.68s | 1868416 ko || +0m19.06s ||   -238168 ko |  +19.51% |        -12.74%
  1m58.86s | 1834476 ko | fiat-bedrock2/src/p384_32.c                                       |   1m40.20s | 1821748 ko || +0m18.65s ||     12728 ko |  +18.62% |         +0.69%
  1m57.91s | 1645388 ko | fiat-json/src/p384_scalar_32.json                                 |   1m39.64s | 2106288 ko || +0m18.26s ||   -460900 ko |  +18.33% |        -21.88%
  0m55.68s | 1150564 ko | Rewriter/Passes/Arith.vo                                          |   0m40.86s | 1092012 ko || +0m14.82s ||     58552 ko |  +36.27% |         +5.36%
  2m00.58s | 2234976 ko | fiat-bedrock2/src/p384_scalar_32.c                                |   1m47.08s | 2226524 ko || +0m13.50s ||      8452 ko |  +12.60% |         +0.37%
  1m56.68s | 1764652 ko | fiat-java/src/FiatP384.java                                       |   1m44.50s | 1969328 ko || +0m12.18s ||   -204676 ko |  +11.65% |        -10.39%
  1m54.76s | 1908628 ko | fiat-json/src/p384_32.json                                        |   1m43.69s | 2004176 ko || +0m11.06s ||    -95548 ko |  +10.67% |         -4.76%
  1m57.28s | 1615084 ko | fiat-zig/src/p384_scalar_32.zig                                   |   1m46.91s | 1733780 ko || +0m10.37s ||   -118696 ko |   +9.69% |         -6.84%
  1m54.55s | 2074740 ko | fiat-zig/src/p384_32.zig                                          |   1m44.61s | 1626180 ko || +0m09.93s ||    448560 ko |   +9.50% |        +27.58%
  1m55.94s | 2145952 ko | fiat-go/32/p384scalar/p384scalar.go                               |   1m48.27s | 1630928 ko || +0m07.66s ||    515024 ko |   +7.08% |        +31.57%
  1m57.76s | 1764936 ko | fiat-rust/src/p384_scalar_32.rs                                   |   1m51.87s | 1768464 ko || +0m05.88s ||     -3528 ko |   +5.26% |         -0.19%
  1m54.58s | 1597680 ko | fiat-rust/src/p384_32.rs                                          |   1m48.64s | 1718060 ko || +0m05.93s ||   -120380 ko |   +5.46% |         -7.00%
  1m54.56s | 1708700 ko | fiat-c/src/p384_scalar_32.c                                       |   1m49.11s | 1518820 ko || +0m05.45s ||    189880 ko |   +4.99% |        +12.50%
  1m51.99s | 1734444 ko | fiat-c/src/p384_32.c                                              |   1m46.30s | 1630176 ko || +0m05.69s ||    104268 ko |   +5.35% |         +6.39%
  1m45.33s | 1889064 ko | Bedrock/End2End/X25519/AddPrecomputed.vo                          |   1m49.74s | 1889060 ko || -0m04.41s ||         4 ko |   -4.01% |         +0.00%
  5m27.35s | 2852288 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo                   |   5m31.22s | 2852504 ko || -0m03.87s ||      -216 ko |   -1.16% |         -0.00%
  2m33.52s | 1607452 ko | Rewriter/Passes/NBE.vo                                            |   2m37.17s | 1607512 ko || -0m03.65s ||       -60 ko |   -2.32% |         -0.00%
  0m37.77s |  110828 ko | fiat-json/src/p521_32.json                                        |   0m33.99s |  114180 ko || +0m03.78s ||     -3352 ko |  +11.12% |         -2.93%
  0m37.53s |   62756 ko | fiat-java/src/FiatP521.java                                       |   0m33.77s |   62456 ko || +0m03.75s ||       300 ko |  +11.13% |         +0.48%
  1m50.62s | 1393276 ko | Rewriter/Passes/ToFancyWithCasts.vo                               |   1m53.15s | 1392880 ko || -0m02.53s ||       396 ko |   -2.23% |         +0.02%
  0m42.34s | 1859688 ko | ExtractionOCaml/bedrock2_saturated_solinas                        |   0m40.29s | 1851720 ko || +0m02.05s ||      7968 ko |   +5.08% |         +0.43%
  0m39.48s | 1769316 ko | ExtractionOCaml/base_conversion                                   |   0m41.92s | 1624120 ko || -0m02.44s ||    145196 ko |   -5.82% |         +8.93%
  1m49.94s | 2247636 ko | Fancy/Barrett256.vo                                               |   1m51.28s | 2284788 ko || -0m01.34s ||    -37152 ko |   -1.20% |         -1.62%
  1m47.35s | 1832408 ko | fiat-go/32/p384/p384.go                                           |   1m49.23s | 1724040 ko || -0m01.87s ||    108368 ko |   -1.72% |         +6.28%
  1m32.25s | 2164300 ko | SlowPrimeSynthesisExamples.vo                                     |   1m33.38s | 2139896 ko || -0m01.12s ||     24404 ko |   -1.21% |         +1.14%
  0m51.90s | 1016836 ko | Rewriter/Passes/MultiRetSplit.vo                                  |   0m53.14s | 1016808 ko || -0m01.24s ||        28 ko |   -2.33% |         +0.00%
  0m47.25s | 2146984 ko | ExtractionOCaml/solinas_reduction                                 |   0m45.91s | 2147072 ko || +0m01.34s ||       -88 ko |   +2.91% |         -0.00%
  0m45.18s | 2146856 ko | ExtractionOCaml/word_by_word_montgomery                           |   0m46.83s | 2147056 ko || -0m01.64s ||      -200 ko |   -3.52% |         -0.00%
  0m43.40s | 1864240 ko | ExtractionOCaml/bedrock2_dettman_multiplication                   |   0m41.96s | 1870364 ko || +0m01.43s ||     -6124 ko |   +3.43% |         -0.32%
  0m41.82s | 1863680 ko | ExtractionOCaml/unsaturated_solinas                               |   0m43.45s | 1863368 ko || -0m01.63s ||       312 ko |   -3.75% |         +0.01%
  0m29.25s | 1544592 ko | StandaloneDebuggingExamples.vo                                    |   0m30.51s | 1556744 ko || -0m01.26s ||    -12152 ko |   -4.12% |         -0.78%
  0m16.94s |  283032 ko | fiat-go/64/p434/p434.go                                           |   0m18.07s |  247128 ko || -0m01.12s ||     35904 ko |   -6.25% |        +14.52%
  0m16.74s | 2204356 ko | ExtractionHaskell/with_bedrock2_solinas_reduction.hs              |   0m17.83s | 2237008 ko || -0m01.08s ||    -32652 ko |   -6.11% |         -1.45%
  0m16.25s |  253040 ko | fiat-rust/src/p434_64.rs                                          |   0m17.99s |  278560 ko || -0m01.73s ||    -25520 ko |   -9.67% |         -9.16%
  8m28.15s | 2591812 ko | Bedrock/End2End/X25519/GarageDoor.vo                              |   8m27.82s | 2587848 ko || +0m00.32s ||      3964 ko |   +0.06% |         +0.15%
  1m51.16s | 1612836 ko | Bedrock/End2End/X25519/Field25519.vo                              |   1m52.02s | 1604084 ko || -0m00.86s ||      8752 ko |   -0.76% |         +0.54%
  0m56.72s |  707388 ko | Rewriter/RulesProofs.vo                                           |   0m55.84s |  703908 ko || +0m00.87s ||      3480 ko |   +1.57% |         +0.49%
  0m49.15s | 2147776 ko | ExtractionOCaml/bedrock2_solinas_reduction                        |   0m48.43s | 2147920 ko || +0m00.71s ||      -144 ko |   +1.48% |         -0.00%
  0m48.64s | 1869620 ko | Fancy/Montgomery256.vo                                            |   0m48.94s | 1855572 ko || -0m00.29s ||     14048 ko |   -0.61% |         +0.75%
  0m48.41s | 2147988 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery             |   0m48.03s | 2147920 ko || +0m00.37s ||        68 ko |   +0.79% |         +0.00%
  0m48.12s | 2148012 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery                  |   0m47.94s | 2147964 ko || +0m00.17s ||        48 ko |   +0.37% |         +0.00%
  0m47.07s | 2148072 ko | ExtractionOCaml/bedrock2_unsaturated_solinas                      |   0m46.98s | 2147976 ko || +0m00.09s ||        96 ko |   +0.19% |         +0.00%
  0m46.31s | 2148036 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas                 |   0m46.12s | 2147932 ko || +0m00.19s ||       104 ko |   +0.41% |         +0.00%
  0m42.55s | 1864184 ko | ExtractionOCaml/bedrock2_base_conversion                          |   0m41.57s | 1864708 ko || +0m00.97s ||      -524 ko |   +2.35% |         -0.02%
  0m42.07s | 1864464 ko | ExtractionOCaml/with_bedrock2_base_conversion                     |   0m41.20s | 1823744 ko || +0m00.86s ||     40720 ko |   +2.11% |         +2.23%
  0m41.68s | 1858816 ko | ExtractionOCaml/with_bedrock2_saturated_solinas                   |   0m40.96s | 1851212 ko || +0m00.71s ||      7604 ko |   +1.75% |         +0.41%
  0m41.66s | 1859960 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication              |   0m41.21s | 1851288 ko || +0m00.44s ||      8672 ko |   +1.09% |         +0.46%
  0m41.50s | 1857940 ko | ExtractionOCaml/with_bedrock2_solinas_reduction                   |   0m41.06s | 1849540 ko || +0m00.43s ||      8400 ko |   +1.07% |         +0.45%
  0m40.74s |   62064 ko | fiat-go/32/p521/p521.go                                           |   0m41.26s |   68256 ko || -0m00.51s ||     -6192 ko |   -1.26% |         -9.07%
  0m40.14s | 1864708 ko | ExtractionOCaml/dettman_multiplication                            |   0m40.52s | 1786504 ko || -0m00.38s ||     78204 ko |   -0.93% |         +4.37%
  0m38.85s |  149624 ko | fiat-bedrock2/src/p521_32.c                                       |   0m38.98s |  143940 ko || -0m00.12s ||      5684 ko |   -0.33% |         +3.94%
  0m38.54s | 1775188 ko | ExtractionOCaml/saturated_solinas                                 |   0m38.71s | 1764700 ko || -0m00.17s ||     10488 ko |   -0.43% |         +0.59%
  0m37.51s |   62500 ko | fiat-zig/src/p521_32.zig                                          |   0m37.39s |   59332 ko || +0m00.11s ||      3168 ko |   +0.32% |         +5.33%
  0m37.48s | 1294192 ko | Bedrock/End2End/X25519/GarageDoorTop.vo                           |   0m37.27s | 1292880 ko || +0m00.20s ||      1312 ko |   +0.56% |         +0.10%
  0m37.44s |   66780 ko | fiat-c/src/p521_32.c                                              |   0m37.77s |   60280 ko || -0m00.33s ||      6500 ko |   -0.87% |        +10.78%
  0m37.42s |   60608 ko | fiat-rust/src/p521_32.rs                                          |   0m37.83s |   61900 ko || -0m00.40s ||     -1292 ko |   -1.08% |         -2.08%
  0m37.11s | 2378444 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml                     |   0m37.46s | 2364772 ko || -0m00.35s ||     13672 ko |   -0.93% |         +0.57%
  0m36.36s | 2319684 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml          |   0m36.69s | 2362052 ko || -0m00.32s ||    -42368 ko |   -0.89% |         -1.79%
  0m36.34s | 2322608 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml               |   0m36.87s | 2363400 ko || -0m00.52s ||    -40792 ko |   -1.43% |         -1.72%
  0m35.65s | 2239920 ko | ExtractionOCaml/solinas_reduction.ml                              |   0m35.60s | 2244256 ko || +0m00.04s ||     -4336 ko |   +0.14% |         -0.19%
  0m34.94s | 1413516 ko | ExtractionOCaml/perf_word_by_word_montgomery                      |   0m34.37s | 1401160 ko || +0m00.57s ||     12356 ko |   +1.65% |         +0.88%
  0m34.88s | 1413452 ko | ExtractionOCaml/perf_unsaturated_solinas                          |   0m34.36s | 1398860 ko || +0m00.52s ||     14592 ko |   +1.51% |         +1.04%
  0m34.62s | 1284740 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo                        |   0m35.00s | 1284680 ko || -0m00.38s ||        60 ko |   -1.08% |         +0.00%
  0m34.36s | 2237140 ko | ExtractionOCaml/word_by_word_montgomery.ml                        |   0m34.45s | 2220616 ko || -0m00.09s ||     16524 ko |   -0.26% |         +0.74%
  0m34.01s |  915808 ko | Rewriter/Passes/MulSplit.vo                                       |   0m34.72s |  913152 ko || -0m00.71s ||      2656 ko |   -2.04% |         +0.29%
  0m33.79s | 2251096 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml                   |   0m33.50s | 2229256 ko || +0m00.28s ||     21840 ko |   +0.86% |         +0.97%
  0m33.14s | 2251808 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml              |   0m33.28s | 2229952 ko || -0m00.14s ||     21856 ko |   -0.42% |         +0.98%
  0m31.42s | 2149728 ko | ExtractionOCaml/unsaturated_solinas.ml                            |   0m31.33s | 2124628 ko || +0m00.09s ||     25100 ko |   +0.28% |         +1.18%
  0m29.99s | 2166628 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml                |   0m30.23s | 2179988 ko || -0m00.24s ||    -13360 ko |   -0.79% |         -0.61%
  0m29.53s | 2156584 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml                |   0m29.10s | 2125132 ko || +0m00.42s ||     31452 ko |   +1.47% |         +1.48%
  0m29.25s | 2161092 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml                  |   0m28.31s | 2121844 ko || +0m00.94s ||     39248 ko |   +3.32% |         +1.84%
  0m29.19s | 2161336 ko | ExtractionOCaml/bedrock2_base_conversion.ml                       |   0m29.47s | 2121804 ko || -0m00.27s ||     39532 ko |   -0.95% |         +1.86%
  0m29.12s | 2156880 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml                     |   0m29.25s | 2124968 ko || -0m00.12s ||     31912 ko |   -0.44% |         +1.50%
  0m29.07s | 2156996 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml                |   0m28.94s | 2124832 ko || +0m00.12s ||     32164 ko |   +0.44% |         +1.51%
  0m28.90s | 2158288 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml           |   0m29.11s | 2130440 ko || -0m00.21s ||     27848 ko |   -0.72% |         +1.30%
  0m27.93s | 2064324 ko | ExtractionOCaml/dettman_multiplication.ml                         |   0m28.14s | 2081544 ko || -0m00.21s ||    -17220 ko |   -0.74% |         -0.82%
  0m27.37s | 2077984 ko | ExtractionOCaml/saturated_solinas.ml                              |   0m27.45s | 2061340 ko || -0m00.07s ||     16644 ko |   -0.29% |         +0.80%
  0m26.92s | 2069712 ko | ExtractionOCaml/base_conversion.ml                                |   0m27.35s | 2051836 ko || -0m00.42s ||     17876 ko |   -1.57% |         +0.87%
  0m25.19s | 1381372 ko | PerfTesting/PerfTestSearch.vo                                     |   0m25.63s | 1377272 ko || -0m00.43s ||      4100 ko |   -1.71% |         +0.29%
  0m23.10s | 1189876 ko | PushButtonSynthesis/UnsaturatedSolinas.vo                         |   0m23.84s | 1191348 ko || -0m00.73s ||     -1472 ko |   -3.10% |         -0.12%
  0m21.56s | 1967716 ko | ExtractionOCaml/perf_unsaturated_solinas.ml                       |   0m21.50s | 1905172 ko || +0m00.05s ||     62544 ko |   +0.27% |         +3.28%
  0m21.46s | 1954296 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml                   |   0m21.53s | 2007400 ko || -0m00.07s ||    -53104 ko |   -0.32% |         -2.64%
  0m21.42s | 1364020 ko | Bedrock/End2End/RupicolaCrypto/Low.vo                             |   0m21.81s | 1360444 ko || -0m00.38s ||      3576 ko |   -1.78% |         +0.26%
  0m20.10s | 1163460 ko | PushButtonSynthesis/WordByWordMontgomery.vo                       |   0m20.64s | 1164604 ko || -0m00.53s ||     -1144 ko |   -2.61% |         -0.09%
  0m18.30s |  301772 ko | fiat-bedrock2/src/p434_64.c                                       |   0m18.00s |  301336 ko || +0m00.30s ||       436 ko |   +1.66% |         +0.14%
  0m18.28s | 1142612 ko | Bedrock/Field/Translation/Proofs/Func.vo                          |   0m18.75s | 1141560 ko || -0m00.46s ||      1052 ko |   -2.50% |         +0.09%
  0m17.74s |  405312 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_32.c                |   0m17.23s |  404568 ko || +0m00.50s ||       744 ko |   +2.95% |         +0.18%
  0m17.68s |  267560 ko | fiat-json/src/p434_64.json                                        |   0m17.55s |  336912 ko || +0m00.12s ||    -69352 ko |   +0.74% |        -20.58%
  0m17.57s |  432032 ko | fiat-bedrock2/src/p256_scalar_32.c                                |   0m17.05s |  461272 ko || +0m00.51s ||    -29240 ko |   +3.04% |         -6.33%
  0m17.48s | 2202308 ko | ExtractionHaskell/bedrock2_solinas_reduction.hs                   |   0m17.75s | 2235132 ko || -0m00.26s ||    -32824 ko |   -1.52% |         -1.46%
  0m17.46s | 1380556 ko | PerfTesting/PerfTestSearchPattern.vo                              |   0m17.92s | 1380832 ko || -0m00.46s ||      -276 ko |   -2.56% |         -0.01%
  0m17.41s |  230072 ko | fiat-zig/src/p434_64.zig                                          |   0m17.32s |  253724 ko || +0m00.08s ||    -23652 ko |   +0.51% |         -9.32%
  0m17.35s | 1223956 ko | Bedrock/Field/Synthesis/New/Signature.vo                          |   0m17.66s | 1220516 ko || -0m00.30s ||      3440 ko |   -1.75% |         +0.28%
  0m17.35s | 2166060 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs             |   0m17.53s | 2194808 ko || -0m00.17s ||    -28748 ko |   -1.02% |         -1.30%
  0m17.28s | 2164448 ko | ExtractionHaskell/with_bedrock2_word_by_word_montgomery.hs        |   0m17.52s | 2193664 ko || -0m00.23s ||    -29216 ko |   -1.36% |         -1.33%
  0m17.16s |  254416 ko | fiat-c/src/p434_64.c                                              |   0m17.42s |  251820 ko || -0m00.26s ||      2596 ko |   -1.49% |         +1.03%
  0m17.15s |  390476 ko | fiat-bedrock2/src/secp256k1_montgomery_32.c                       |   0m16.69s |  415512 ko || +0m00.45s ||    -25036 ko |   +2.75% |         -6.02%
  0m17.01s |  351572 ko | fiat-java/src/FiatSecp256K1MontgomeryScalar.java                  |   0m16.40s |  455088 ko || +0m00.61s ||   -103516 ko |   +3.71% |        -22.74%
  0m16.90s |  445272 ko | fiat-go/32/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go |   0m17.19s |  360700 ko || -0m00.29s ||     84572 ko |   -1.68% |        +23.44%
  0m16.86s | 1160300 ko | Bedrock/Field/Translation/Proofs/Cmd.vo                           |   0m17.42s | 1157936 ko || -0m00.56s ||      2364 ko |   -3.21% |         +0.20%
  0m16.84s |  456724 ko | fiat-bedrock2/src/curve25519_scalar_32.c                          |   0m16.68s |  405344 ko || +0m00.16s ||     51380 ko |   +0.95% |        +12.67%
  0m16.83s |  454284 ko | fiat-json/src/secp256k1_montgomery_scalar_32.json                 |   0m16.39s |  468528 ko || +0m00.43s ||    -14244 ko |   +2.68% |         -3.04%
  0m16.79s | 2032540 ko | ExtractionHaskell/word_by_word_montgomery.hs                      |   0m16.91s | 2067180 ko || -0m00.12s ||    -34640 ko |   -0.70% |         -1.67%
  0m16.77s | 2093008 ko | ExtractionHaskell/solinas_reduction.hs                            |   0m16.77s | 2051684 ko || +0m00.00s ||     41324 ko |   +0.00% |         +2.01%
  0m16.76s |  371064 ko | fiat-java/src/FiatP256Scalar.java                                 |   0m15.92s |  334232 ko || +0m00.84s ||     36832 ko |   +5.27% |        +11.01%
  0m16.75s | 2144072 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs                 |   0m16.53s | 2074184 ko || +0m00.21s ||     69888 ko |   +1.33% |         +3.36%
  0m16.73s |  406956 ko | fiat-json/src/curve25519_scalar_32.json                           |   0m16.02s |  450328 ko || +0m00.71s ||    -43372 ko |   +4.43% |         -9.63%
  0m16.73s |  347524 ko | fiat-zig/src/secp256k1_montgomery_scalar_32.zig                   |   0m16.35s |  397760 ko || +0m00.37s ||    -50236 ko |   +2.32% |        -12.62%
  0m16.72s |  390380 ko | fiat-zig/src/p256_scalar_32.zig                                   |   0m16.18s |  356296 ko || +0m00.53s ||     34084 ko |   +3.33% |         +9.56%
  0m16.70s |  391092 ko | fiat-go/32/p256scalar/p256scalar.go                               |   0m16.94s |  366900 ko || -0m00.24s ||     24192 ko |   -1.41% |         +6.59%
  0m16.68s |  405796 ko | fiat-java/src/FiatCurve25519Scalar.java                           |   0m16.15s |  370228 ko || +0m00.53s ||     35568 ko |   +3.28% |         +9.60%
  0m16.66s |  378844 ko | fiat-rust/src/p256_scalar_32.rs                                   |   0m15.98s |  411316 ko || +0m00.67s ||    -32472 ko |   +4.25% |         -7.89%
  0m16.61s |  366928 ko | fiat-c/src/secp256k1_montgomery_scalar_32.c                       |   0m16.58s |  426780 ko || +0m00.03s ||    -59852 ko |   +0.18% |        -14.02%
  0m16.59s |  340692 ko | fiat-rust/src/secp256k1_montgomery_32.rs                          |   0m16.47s |  353508 ko || +0m00.12s ||    -12816 ko |   +0.72% |         -3.62%
  0m16.58s |  385436 ko | fiat-json/src/secp256k1_montgomery_32.json                        |   0m16.19s |  407896 ko || +0m00.38s ||    -22460 ko |   +2.40% |         -5.50%
  0m16.55s |  416232 ko | fiat-go/32/curve25519scalar/curve25519scalar.go                   |   0m16.41s |  346260 ko || +0m00.14s ||     69972 ko |   +0.85% |        +20.20%
  0m16.53s |  338172 ko | fiat-java/src/FiatSecp256K1Montgomery.java                        |   0m16.15s |  423920 ko || +0m00.38s ||    -85748 ko |   +2.35% |        -20.22%
  0m16.53s |  396224 ko | fiat-rust/src/secp256k1_montgomery_scalar_32.rs                   |   0m16.61s |  445068 ko || -0m00.07s ||    -48844 ko |   -0.48% |        -10.97%
  0m16.50s | 2144128 ko | ExtractionHaskell/with_bedrock2_unsaturated_solinas.hs            |   0m16.55s | 2072880 ko || -0m00.05s ||     71248 ko |   -0.30% |         +3.43%
  0m16.45s | 1139712 ko | Bedrock/End2End/Poly1305/Field1305.vo                             |   0m17.26s | 1137640 ko || -0m00.81s ||      2072 ko |   -4.69% |         +0.18%
  0m16.45s |  364804 ko | fiat-c/src/p256_scalar_32.c                                       |   0m16.45s |  434352 ko || +0m00.00s ||    -69548 ko |   +0.00% |        -16.01%
  0m16.36s |  436776 ko | fiat-zig/src/secp256k1_montgomery_32.zig                          |   0m16.01s |  437516 ko || +0m00.34s ||      -740 ko |   +2.18% |         -0.16%
  0m16.33s |  359632 ko | fiat-zig/src/curve25519_scalar_32.zig                             |   0m15.80s |  434444 ko || +0m00.52s ||    -74812 ko |   +3.35% |        -17.22%
  0m16.32s |  440340 ko | fiat-go/32/secp256k1montgomery/secp256k1montgomery.go             |   0m16.19s |  415772 ko || +0m00.12s ||     24568 ko |   +0.80% |         +5.90%
  0m16.31s |  431364 ko | fiat-json/src/p256_scalar_32.json                                 |   0m16.54s |  468452 ko || -0m00.23s ||    -37088 ko |   -1.39% |         -7.91%
  0m16.28s |  418340 ko | fiat-c/src/secp256k1_montgomery_32.c                              |   0m16.07s |  354548 ko || +0m00.21s ||     63792 ko |   +1.30% |        +17.99%
  0m16.11s |  323148 ko | fiat-c/src/curve25519_scalar_32.c                                 |   0m15.37s |  376208 ko || +0m00.74s ||    -53060 ko |   +4.81% |        -14.10%
  0m16.09s |  429024 ko | fiat-rust/src/curve25519_scalar_32.rs                             |   0m16.31s |  405604 ko || -0m00.21s ||     23420 ko |   -1.34% |         +5.77%
  0m16.07s |  392824 ko | fiat-bedrock2/src/p256_32.c                                       |   0m15.76s |  418500 ko || +0m00.31s ||    -25676 ko |   +1.96% |         -6.13%
  0m15.73s | 2026232 ko | ExtractionHaskell/unsaturated_solinas.hs                          |   0m15.70s | 1972880 ko || +0m00.03s ||     53352 ko |   +0.19% |         +2.70%
  0m15.67s |  400632 ko | fiat-java/src/FiatP256.java                                       |   0m15.23s |  347976 ko || +0m00.43s ||     52656 ko |   +2.88% |        +15.13%
  0m15.67s |  426864 ko | fiat-rust/src/p256_32.rs                                          |   0m15.43s |  436980 ko || +0m00.24s ||    -10116 ko |   +1.55% |         -2.31%
  0m15.65s |  433612 ko | fiat-go/32/p256/p256.go                                           |   0m15.46s |  363800 ko || +0m00.18s ||     69812 ko |   +1.22% |        +19.18%
  0m15.65s |  332588 ko | fiat-zig/src/p256_32.zig                                          |   0m15.39s |  407124 ko || +0m00.25s ||    -74536 ko |   +1.68% |        -18.30%
  0m15.56s | 2010528 ko | ExtractionHaskell/with_bedrock2_dettman_multiplication.hs         |   0m15.92s | 2039152 ko || -0m00.35s ||    -28624 ko |   -2.26% |         -1.40%
  0m15.53s | 2010444 ko | ExtractionHaskell/bedrock2_dettman_multiplication.hs              |   0m15.68s | 2040720 ko || -0m00.15s ||    -30276 ko |   -0.95% |         -1.48%
  0m15.40s |  332344 ko | fiat-c/src/p256_32.c                                              |   0m15.21s |  376848 ko || +0m00.18s ||    -44504 ko |   +1.24% |        -11.80%
  0m15.29s | 1948284 ko | ExtractionHaskell/with_bedrock2_base_conversion.hs                |   0m15.53s | 2016228 ko || -0m00.24s ||    -67944 ko |   -1.54% |         -3.36%
  0m15.23s | 1959948 ko | ExtractionHaskell/with_bedrock2_saturated_solinas.hs              |   0m15.52s | 2013692 ko || -0m00.28s ||    -53744 ko |   -1.86% |         -2.66%
  0m15.22s | 1958896 ko | ExtractionHaskell/dettman_multiplication.hs                       |   0m15.10s | 1903264 ko || +0m00.12s ||     55632 ko |   +0.79% |         +2.92%
  0m15.15s | 1948672 ko | ExtractionHaskell/bedrock2_base_conversion.hs                     |   0m15.63s | 2015624 ko || -0m00.48s ||    -66952 ko |   -3.07% |         -3.32%
  0m15.12s |  445592 ko | fiat-json/src/p256_32.json                                        |   0m15.46s |  416848 ko || -0m00.34s ||     28744 ko |   -2.19% |         +6.89%
  0m15.11s | 1960852 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs                   |   0m15.44s | 2013416 ko || -0m00.33s ||    -52564 ko |   -2.13% |         -2.61%
  0m14.88s | 1955220 ko | ExtractionHaskell/base_conversion.hs                              |   0m14.93s | 1897380 ko || -0m00.04s ||     57840 ko |   -0.33% |         +3.04%
  0m14.86s | 1921176 ko | ExtractionHaskell/saturated_solinas.hs                            |   0m14.96s | 1916928 ko || -0m00.10s ||      4248 ko |   -0.66% |         +0.22%
  0m11.31s |  199152 ko | fiat-bedrock2/src/p384_scalar_64.c                                |   0m11.18s |  194984 ko || +0m00.13s ||      4168 ko |   +1.16% |         +2.13%
  0m11.21s |  199888 ko | fiat-go/64/p384scalar/p384scalar.go                               |   0m11.15s |  164128 ko || +0m00.06s ||     35760 ko |   +0.53% |        +21.78%
  0m11.17s | 1708132 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo               |   0m11.30s | 1703996 ko || -0m00.13s ||      4136 ko |   -1.15% |         +0.24%
  0m10.92s | 1035420 ko | BoundsPipeline.vo                                                 |   0m11.20s | 1036784 ko || -0m00.27s ||     -1364 ko |   -2.49% |         -0.13%
  0m10.91s |  169592 ko | fiat-json/src/p384_scalar_64.json                                 |   0m10.81s |  184092 ko || +0m00.09s ||    -14500 ko |   +0.92% |         -7.87%
  0m10.87s |  176344 ko | fiat-zig/src/p384_scalar_64.zig                                   |   0m10.57s |  192372 ko || +0m00.29s ||    -16028 ko |   +2.83% |         -8.33%
  0m10.73s |  166616 ko | fiat-rust/src/p384_scalar_64.rs                                   |   0m10.84s |  176032 ko || -0m00.10s ||     -9416 ko |   -1.01% |         -5.34%
  0m10.58s |  154460 ko | fiat-c/src/p384_scalar_64.c                                       |   0m10.71s |  142320 ko || -0m00.13s ||     12140 ko |   -1.21% |         +8.53%
  0m10.15s | 1304732 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo              |   0m10.24s | 1304688 ko || -0m00.08s ||        44 ko |   -0.87% |         +0.00%
  0m09.59s |  195012 ko | fiat-bedrock2/src/p384_64.c                                       |   0m09.53s |  205984 ko || +0m00.06s ||    -10972 ko |   +0.62% |         -5.32%
  0m09.54s |  255304 ko | fiat-bedrock2/src/p224_32.c                                       |   0m09.46s |  246228 ko || +0m00.07s ||      9076 ko |   +0.84% |         +3.68%
  0m09.38s |  235988 ko | fiat-json/src/p224_32.json                                        |   0m09.14s |  243676 ko || +0m00.24s ||     -7688 ko |   +2.62% |         -3.15%
  0m09.29s |  195668 ko | fiat-json/src/p384_64.json                                        |   0m09.24s |  173592 ko || +0m00.04s ||     22076 ko |   +0.54% |        +12.71%
  0m09.26s |  245908 ko | fiat-java/src/FiatP224.java                                       |   0m09.02s |  210104 ko || +0m00.24s ||     35804 ko |   +2.66% |        +17.04%
  0m09.25s |  170924 ko | fiat-go/64/p384/p384.go                                           |   0m09.35s |  160844 ko || -0m00.09s ||     10080 ko |   -1.06% |         +6.26%
  0m09.20s | 1040012 ko | PushButtonSynthesis/BaseConversion.vo                             |   0m09.41s | 1037912 ko || -0m00.21s ||      2100 ko |   -2.23% |         +0.20%
  0m09.14s |  225000 ko | fiat-go/32/p224/p224.go                                           |   0m09.39s |  230444 ko || -0m00.25s ||     -5444 ko |   -2.66% |         -2.36%
  0m09.11s |  253348 ko | fiat-rust/src/p224_32.rs                                          |   0m09.20s |  245628 ko || -0m00.08s ||      7720 ko |   -0.97% |         +3.14%
  0m09.11s |  166552 ko | fiat-zig/src/p384_64.zig                                          |   0m09.31s |  141172 ko || -0m00.20s ||     25380 ko |   -2.14% |        +17.97%
  0m09.10s |  167020 ko | fiat-c/src/p384_64.c                                              |   0m09.28s |  146704 ko || -0m00.17s ||     20316 ko |   -1.93% |        +13.84%
  0m09.09s |  254100 ko | fiat-zig/src/p224_32.zig                                          |   0m08.87s |  222884 ko || +0m00.22s ||     31216 ko |   +2.48% |        +14.00%
  0m08.96s |  232884 ko | fiat-c/src/p224_32.c                                              |   0m08.97s |  240356 ko || -0m00.00s ||     -7472 ko |   -0.11% |         -3.10%
  0m08.73s |  147896 ko | fiat-rust/src/p384_64.rs                                          |   0m09.22s |  165796 ko || -0m00.49s ||    -17900 ko |   -5.31% |        -10.79%
  0m08.26s | 1009244 ko | PushButtonSynthesis/SmallExamples.vo                              |   0m08.45s | 1008344 ko || -0m00.18s ||       900 ko |   -2.24% |         +0.08%
  0m08.26s |  119472 ko | fiat-json/src/p448_solinas_32.json                                |   0m08.29s |  123884 ko || -0m00.02s ||     -4412 ko |   -0.36% |         -3.56%
  0m08.16s | 1050960 ko | PushButtonSynthesis/Primitives.vo                                 |   0m08.27s | 1050876 ko || -0m00.10s ||        84 ko |   -1.33% |         +0.00%
  0m07.93s |  591100 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo                            |   0m08.19s |  591176 ko || -0m00.25s ||       -76 ko |   -3.17% |         -0.01%
  0m07.91s |   61592 ko | fiat-zig/src/p448_solinas_32.zig                                  |   0m07.94s |   61704 ko || -0m00.03s ||      -112 ko |   -0.37% |         -0.18%
  0m07.89s |   59392 ko | fiat-c/src/p448_solinas_32.c                                      |   0m07.94s |   56764 ko || -0m00.05s ||      2628 ko |   -0.62% |         +4.62%
  0m07.88s |   61076 ko | fiat-rust/src/p448_solinas_32.rs                                  |   0m08.00s |   57600 ko || -0m00.12s ||      3476 ko |   -1.50% |         +6.03%
  0m07.12s | 1043600 ko | PushButtonSynthesis/SolinasReduction.vo                           |   0m07.38s | 1043572 ko || -0m00.25s ||        28 ko |   -3.52% |         +0.00%
  0m06.64s |   52476 ko | fiat-go/64/p521/p521.go                                           |   0m06.25s |   49644 ko || +0m00.38s ||      2832 ko |   +6.23% |         +5.70%
  0m06.27s |  574792 ko | Rewriter/Passes/NoSelect.vo                                       |   0m06.41s |  577812 ko || -0m00.14s ||     -3020 ko |   -2.18% |         -0.52%
  0m06.26s | 1048224 ko | PushButtonSynthesis/BarrettReduction.vo                           |   0m06.20s | 1051084 ko || +0m00.05s ||     -2860 ko |   +0.96% |         -0.27%
  0m06.22s | 1132216 ko | CLI.vo                                                            |   0m06.30s | 1130060 ko || -0m00.08s ||      2156 ko |   -1.26% |         +0.19%
  0m05.96s | 1144288 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo                 |   0m06.15s | 1142040 ko || -0m00.19s ||      2248 ko |   -3.08% |         +0.19%
  0m05.54s |   68872 ko | fiat-bedrock2/src/p521_64.c                                       |   0m05.56s |   68208 ko || -0m00.01s ||       664 ko |   -0.35% |         +0.97%
  0m05.42s |   51340 ko | fiat-json/src/p521_64.json                                        |   0m05.43s |   51520 ko || -0m00.00s ||      -180 ko |   -0.18% |         -0.34%
  0m05.30s |   37436 ko | fiat-zig/src/p521_64.zig                                          |   0m04.77s |   37212 ko || +0m00.53s ||       224 ko |  +11.11% |         +0.60%
  0m04.82s |   37880 ko | fiat-rust/src/p521_64.rs                                          |   0m05.45s |   38100 ko || -0m00.62s ||      -220 ko |  -11.55% |         -0.57%
  0m04.76s |   37380 ko | fiat-c/src/p521_64.c                                              |   0m05.37s |   37352 ko || -0m00.61s ||        28 ko |  -11.35% |         +0.07%
  0m04.66s | 1038068 ko | PushButtonSynthesis/DettmanMultiplication.vo                      |   0m04.63s | 1038160 ko || +0m00.03s ||       -92 ko |   +0.64% |         -0.00%
  0m04.51s | 1074152 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo           |   0m04.59s | 1074372 ko || -0m00.08s ||      -220 ko |   -1.74% |         -0.02%
  0m04.24s | 1047736 ko | PushButtonSynthesis/SaturatedSolinas.vo                           |   0m04.41s | 1047768 ko || -0m00.16s ||       -32 ko |   -3.85% |         -0.00%
  0m04.01s | 1501044 ko | Bedrock/Everything.vo                                             |   0m04.01s | 1501100 ko || +0m00.00s ||       -56 ko |   +0.00% |         -0.00%
  0m03.81s | 1051824 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo                   |   0m03.77s | 1050712 ko || +0m00.04s ||      1112 ko |   +1.06% |         +0.10%
  0m03.50s | 1367412 ko | Everything.vo                                                     |   0m03.59s | 1367556 ko || -0m00.08s ||      -144 ko |   -2.50% |         -0.01%
  0m03.06s |  537952 ko | Rewriter/Passes/ArithWithRelaxedCasts.vo                          |   0m03.15s |  539144 ko || -0m00.08s ||     -1192 ko |   -2.85% |         -0.22%
  0m02.98s | 1013864 ko | Bedrock/Field/Translation/Cmd.vo                                  |   0m02.98s | 1014664 ko || +0m00.00s ||      -800 ko |   +0.00% |         -0.07%
  0m02.96s | 1083180 ko | Rewriter/PerfTesting/Core.vo                                      |   0m03.04s | 1083012 ko || -0m00.08s ||       168 ko |   -2.63% |         +0.01%
  0m02.94s |   70004 ko | fiat-go/64/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go |   0m02.80s |   69640 ko || +0m00.14s ||       364 ko |   +5.00% |         +0.52%
  0m02.93s |   69652 ko | fiat-go/64/p256scalar/p256scalar.go                               |   0m02.77s |   69300 ko || +0m00.16s ||       352 ko |   +5.77% |         +0.50%
  0m02.92s |  539268 ko | Rewriter/Passes/AddAssocLeft.vo                                   |   0m02.99s |  537676 ko || -0m00.07s ||      1592 ko |   -2.34% |         +0.29%
  0m02.90s | 1126644 ko | StandaloneHaskellMain.vo                                          |   0m02.85s | 1124644 ko || +0m00.04s ||      2000 ko |   +1.75% |         +0.17%
  0m02.86s | 1355272 ko | PerfTesting/PerfTestPrint.vo                                      |   0m02.97s | 1353376 ko || -0m00.11s ||      1896 ko |   -3.70% |         +0.14%
  0m02.83s |   74888 ko | fiat-json/src/p256_scalar_64.json                                 |   0m02.73s |   69468 ko || +0m00.10s ||      5420 ko |   +3.66% |         +7.80%
  0m02.79s |   84092 ko | fiat-bedrock2/src/p256_scalar_64.c                                |   0m02.79s |   86516 ko || +0m00.00s ||     -2424 ko |   +0.00% |         -2.80%
  0m02.76s |   87368 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_64.c                |   0m02.77s |   86936 ko || -0m00.01s ||       432 ko |   -0.36% |         +0.49%
  0m02.76s |   57416 ko | fiat-go/64/p448solinas/p448solinas.go                             |   0m02.58s |   51820 ko || +0m00.17s ||      5596 ko |   +6.97% |        +10.79%
  0m02.76s |   73888 ko | fiat-json/src/secp256k1_montgomery_scalar_64.json                 |   0m02.73s |   75908 ko || +0m00.02s ||     -2020 ko |   +1.09% |         -2.66%
  0m02.74s | 1077636 ko | Bedrock/Field/Stringification/Stringification.vo                  |   0m02.78s | 1076572 ko || -0m00.03s ||      1064 ko |   -1.43% |         +0.09%
  0m02.73s | 1010148 ko | Bedrock/Field/Translation/Func.vo                                 |   0m02.82s | 1008988 ko || -0m00.08s ||      1160 ko |   -3.19% |         +0.11%
  0m02.72s |   64580 ko | fiat-zig/src/p256_scalar_64.zig                                   |   0m02.71s |   62528 ko || +0m00.01s ||      2052 ko |   +0.36% |         +3.28%
  0m02.69s |   63552 ko | fiat-go/64/secp256k1montgomery/secp256k1montgomery.go             |   0m02.51s |   67572 ko || +0m00.18s ||     -4020 ko |   +7.17% |         -5.94%
  0m02.69s |   61992 ko | fiat-rust/src/p256_scalar_64.rs                                   |   0m02.75s |   66124 ko || -0m00.06s ||     -4132 ko |   -2.18% |         -6.24%
  0m02.69s |   63084 ko | fiat-rust/src/secp256k1_montgomery_scalar_64.rs                   |   0m02.71s |   66576 ko || -0m00.02s ||     -3492 ko |   -0.73% |         -5.24%
  0m02.68s |   59288 ko | fiat-c/src/p256_scalar_64.c                                       |   0m02.70s |   62336 ko || -0m00.02s ||     -3048 ko |   -0.74% |         -4.88%
  0m02.67s | 1068128 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo          |   0m02.80s | 1068044 ko || -0m00.12s ||        84 ko |   -4.64% |         +0.00%
  0m02.67s |   68464 ko | fiat-c/src/secp256k1_montgomery_scalar_64.c                       |   0m02.70s |   61160 ko || -0m00.03s ||      7304 ko |   -1.11% |        +11.94%
  0m02.66s | 1153388 ko | Bedrock/Standalone/StandaloneHaskellMain.vo                       |   0m02.71s | 1151268 ko || -0m00.04s ||      2120 ko |   -1.84% |         +0.18%
  0m02.66s |   64136 ko | fiat-zig/src/secp256k1_montgomery_scalar_64.zig                   |   0m02.65s |   62200 ko || +0m00.01s ||      1936 ko |   +0.37% |         +3.11%
  0m02.65s | 1103644 ko | StandaloneOCamlMain.vo                                            |   0m02.61s | 1103620 ko || +0m00.04s ||        24 ko |   +1.53% |         +0.00%
  0m02.64s | 1151352 ko | Bedrock/Standalone/StandaloneOCamlMain.vo                         |   0m02.71s | 1151372 ko || -0m00.06s ||       -20 ko |   -2.58% |         -0.00%
  0m02.57s |  535856 ko | Rewriter/Passes/FlattenThunkedRects.vo                            |   0m02.66s |  535192 ko || -0m00.09s ||       664 ko |   -3.38% |         +0.12%
  0m02.52s |   84488 ko | fiat-bedrock2/src/secp256k1_montgomery_64.c                       |   0m02.47s |   93372 ko || +0m00.04s ||     -8884 ko |   +2.02% |         -9.51%
  0m02.52s |   68592 ko | fiat-json/src/secp256k1_montgomery_64.json                        |   0m02.46s |   75364 ko || +0m00.06s ||     -6772 ko |   +2.43% |         -8.98%
  0m02.49s | 1073080 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo                         |   0m02.66s | 1071116 ko || -0m00.16s ||      1964 ko |   -6.39% |         +0.18%
  0m02.48s | 1137168 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo                       |   0m02.76s | 1135252 ko || -0m00.27s ||      1916 ko |  -10.14% |         +0.16%
  0m02.46s |   63516 ko | fiat-go/64/curve25519scalar/curve25519scalar.go                   |   0m02.31s |   70228 ko || +0m00.14s ||     -6712 ko |   +6.49% |         -9.55%
  0m02.42s | 1051400 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo                |   0m02.46s | 1051612 ko || -0m00.04s ||      -212 ko |   -1.62% |         -0.02%
  0m02.42s |   60544 ko | fiat-rust/src/secp256k1_montgomery_64.rs                          |   0m02.42s |   60264 ko || +0m00.00s ||       280 ko |   +0.00% |         +0.46%
  0m02.42s |   65732 ko | fiat-zig/src/secp256k1_montgomery_64.zig                          |   0m02.40s |   57992 ko || +0m00.02s ||      7740 ko |   +0.83% |        +13.34%
  0m02.41s |   60148 ko | fiat-c/src/secp256k1_montgomery_64.c                              |   0m02.44s |   60532 ko || -0m00.02s ||      -384 ko |   -1.22% |         -0.63%
  0m02.37s | 1051572 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo                |   0m02.46s | 1051524 ko || -0m00.08s ||        48 ko |   -3.65% |         +0.00%
  0m02.35s | 1050808 ko | Bedrock/Field/Translation/Parameters/FE310.vo                     |   0m02.42s | 1051668 ko || -0m00.06s ||      -860 ko |   -2.89% |         -0.08%
  0m02.35s |   78788 ko | fiat-bedrock2/src/curve25519_scalar_64.c                          |   0m02.35s |   77892 ko || +0m00.00s ||       896 ko |   +0.00% |         +1.15%
  0m02.34s | 1047512 ko | Bedrock/Field/Translation/Parameters/Defaults.vo                  |   0m02.33s | 1047596 ko || +0m00.00s ||       -84 ko |   +0.42% |         -0.00%
  0m02.31s |   69108 ko | fiat-json/src/curve25519_scalar_64.json                           |   0m02.30s |   69200 ko || +0m00.01s ||       -92 ko |   +0.43% |         -0.13%
  0m02.28s |   60412 ko | fiat-rust/src/curve25519_scalar_64.rs                             |   0m02.31s |   64076 ko || -0m00.03s ||     -3664 ko |   -1.29% |         -5.71%
  0m02.25s |   67320 ko | fiat-c/src/curve25519_scalar_64.c                                 |   0m02.29s |   59928 ko || -0m00.04s ||      7392 ko |   -1.74% |        +12.33%
  0m02.25s |   57700 ko | fiat-zig/src/curve25519_scalar_64.zig                             |   0m02.25s |   63136 ko || +0m00.00s ||     -5436 ko |   +0.00% |         -8.60%
  0m02.17s |  541552 ko | Rewriter/Passes/UnfoldValueBarrier.vo                             |   0m02.27s |  541600 ko || -0m00.10s ||       -48 ko |   -4.40% |         -0.00%
  0m02.10s |  540980 ko | Rewriter/Passes/StripLiteralCasts.vo                              |   0m02.20s |  539800 ko || -0m00.10s ||      1180 ko |   -4.54% |         +0.21%
  0m02.10s |   63292 ko | fiat-go/64/p224/p224.go                                           |   0m01.86s |   61856 ko || +0m00.24s ||      1436 ko |  +12.90% |         +2.32%
  0m02.08s |   38528 ko | fiat-go/32/curve25519/curve25519.go                               |   0m02.07s |   36104 ko || +0m00.01s ||      2424 ko |   +0.48% |         +6.71%
  0m02.07s |   68844 ko | fiat-bedrock2/src/p448_solinas_64.c                               |   0m02.13s |   66964 ko || -0m00.06s ||      1880 ko |   -2.81% |         +2.80%
  0m02.05s |   63476 ko | fiat-go/64/p256/p256.go                                           |   0m01.84s |   62612 ko || +0m00.20s ||       864 ko |  +11.41% |         +1.37%
  0m02.02s |   69516 ko | fiat-bedrock2/src/curve25519_32.c                                 |   0m01.99s |   64620 ko || +0m00.03s ||      4896 ko |   +1.50% |         +7.57%
  0m01.97s |  536652 ko | Rewriter/Passes/ToFancy.vo                                        |   0m02.01s |  537484 ko || -0m00.03s ||      -832 ko |   -1.99% |         -0.15%
  0m01.96s |   52072 ko | fiat-json/src/p448_solinas_64.json                                |   0m01.92s |   49556 ko || +0m00.04s ||      2516 ko |   +2.08% |         +5.07%
  0m01.91s |   78628 ko | fiat-bedrock2/src/p224_64.c                                       |   0m01.91s |   79832 ko || +0m00.00s ||     -1204 ko |   +0.00% |         -1.50%
  0m01.90s |   35620 ko | fiat-c/src/p448_solinas_64.c                                      |   0m01.93s |   35532 ko || -0m00.03s ||        88 ko |   -1.55% |         +0.24%
  0m01.90s |   35992 ko | fiat-rust/src/p448_solinas_64.rs                                  |   0m01.93s |   37888 ko || -0m00.03s ||     -1896 ko |   -1.55% |         -5.00%
  0m01.90s |   36340 ko | fiat-zig/src/p448_solinas_64.zig                                  |   0m01.90s |   38132 ko || +0m00.00s ||     -1792 ko |   +0.00% |         -4.69%
  0m01.89s |   68480 ko | fiat-json/src/p224_64.json                                        |   0m01.93s |   76344 ko || -0m00.04s ||     -7864 ko |   -2.07% |        -10.30%
  0m01.85s |   79464 ko | fiat-bedrock2/src/p256_64.c                                       |   0m01.85s |   80384 ko || +0m00.00s ||      -920 ko |   +0.00% |         -1.14%
  0m01.84s |   69732 ko | fiat-json/src/p256_64.json                                        |   0m01.85s |   68332 ko || -0m00.01s ||      1400 ko |   -0.54% |         +2.04%
  0m01.84s |   60888 ko | fiat-zig/src/p224_64.zig                                          |   0m01.87s |   60200 ko || -0m00.03s ||       688 ko |   -1.60% |         +1.14%
  0m01.83s |   51832 ko | fiat-json/src/curve25519_32.json                                  |   0m01.91s |   54384 ko || -0m00.07s ||     -2552 ko |   -4.18% |         -4.69%
  0m01.82s |   57456 ko | fiat-zig/src/p256_64.zig                                          |   0m01.79s |   57520 ko || +0m00.03s ||       -64 ko |   +1.67% |         -0.11%
  0m01.81s |   60544 ko | fiat-rust/src/p224_64.rs                                          |   0m01.87s |   61580 ko || -0m00.06s ||     -1036 ko |   -3.20% |         -1.68%
  0m01.77s |   58112 ko | fiat-c/src/p224_64.c                                              |   0m01.78s |   61864 ko || -0m00.01s ||     -3752 ko |   -0.56% |         -6.06%
  0m01.77s |   60016 ko | fiat-rust/src/p256_64.rs                                          |   0m01.78s |   60884 ko || -0m00.01s ||      -868 ko |   -0.56% |         -1.42%
  0m01.76s |   36740 ko | fiat-java/src/FiatCurve25519.java                                 |   0m01.70s |   35152 ko || +0m00.06s ||      1588 ko |   +3.52% |         +4.51%
  0m01.76s |   35116 ko | fiat-rust/src/curve25519_32.rs                                    |   0m01.76s |   34160 ko || +0m00.00s ||       956 ko |   +0.00% |         +2.79%
  0m01.75s |   35380 ko | fiat-zig/src/curve25519_32.zig                                    |   0m01.75s |   35084 ko || +0m00.00s ||       296 ko |   +0.00% |         +0.84%
  0m01.74s |   35840 ko | fiat-c/src/curve25519_32.c                                        |   0m01.76s |   34260 ko || -0m00.02s ||      1580 ko |   -1.13% |         +4.61%
  0m01.74s |   65196 ko | fiat-c/src/p256_64.c                                              |   0m01.76s |   62724 ko || -0m00.02s ||      2472 ko |   -1.13% |         +3.94%
  0m01.45s |  596340 ko | CompilersTestCases.vo                                             |   0m01.51s |  596224 ko || -0m00.06s ||       116 ko |   -3.97% |         +0.01%
  0m01.44s |   53596 ko | fiat-bedrock2/src/secp256k1_dettman_32.c                          |   0m01.45s |   51196 ko || -0m00.01s ||      2400 ko |   -0.68% |         +4.68%
  0m01.28s |   42572 ko | fiat-json/src/secp256k1_dettman_32.json                           |   0m01.30s |   43796 ko || -0m00.02s ||     -1224 ko |   -1.53% |         -2.79%
  0m01.22s |   25936 ko | fiat-c/src/secp256k1_dettman_32.c                                 |   0m01.23s |   26436 ko || -0m00.01s ||      -500 ko |   -0.81% |         -1.89%
  0m01.22s |   26988 ko | fiat-go/32/secp256k1dettman/secp256k1dettman.go                   |   0m01.26s |   26796 ko || -0m00.04s ||       192 ko |   -3.17% |         +0.71%
  0m01.22s |   27128 ko | fiat-java/src/FiatSecp256K1Dettman.java                           |   0m01.21s |   27648 ko || +0m00.01s ||      -520 ko |   +0.82% |         -1.88%
  0m01.22s |   26456 ko | fiat-rust/src/secp256k1_dettman_32.rs                             |   0m01.24s |   26404 ko || -0m00.02s ||        52 ko |   -1.61% |         +0.19%
  0m01.20s |   26264 ko | fiat-zig/src/secp256k1_dettman_32.zig                             |   0m01.21s |   26620 ko || -0m00.01s ||      -356 ko |   -0.82% |         -1.33%
  0m00.72s |   33336 ko | fiat-go/64/curve25519/curve25519.go                               |   0m00.62s |   33132 ko || +0m00.09s ||       204 ko |  +16.12% |         +0.61%
  0m00.63s |  438660 ko | Rewriter/Rules.vo                                                 |   0m00.63s |  436796 ko || +0m00.00s ||      1864 ko |   +0.00% |         +0.42%
  0m00.58s |  552492 ko | Rewriter/All.vo                                                   |   0m00.60s |  552492 ko || -0m00.02s ||         0 ko |   -3.33% |         +0.00%
  0m00.54s |  123656 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi               |   0m00.54s |  122456 ko || +0m00.00s ||      1200 ko |   +0.00% |         +0.97%
  0m00.54s |  123868 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi               |   0m00.55s |  122976 ko || -0m00.01s ||       892 ko |   -1.81% |         +0.72%
  0m00.54s |  120496 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi         |   0m00.56s |  122432 ko || -0m00.02s ||     -1936 ko |   -3.57% |         -1.58%
  0m00.53s |  120220 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi                    |   0m00.54s |  120352 ko || -0m00.01s ||      -132 ko |   -1.85% |         -0.10%
  0m00.53s |  122856 ko | ExtractionOCaml/unsaturated_solinas.cmi                           |   0m00.52s |  121012 ko || +0m00.01s ||      1844 ko |   +1.92% |         +1.52%
  0m00.53s |  122964 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi             |   0m00.56s |  123648 ko || -0m00.03s ||      -684 ko |   -5.35% |         -0.55%
  0m00.53s |   39636 ko | fiat-bedrock2/src/curve25519_64.c                                 |   0m00.50s |   38928 ko || +0m00.03s ||       708 ko |   +6.00% |         +1.81%
  0m00.52s |  123624 ko | ExtractionOCaml/bedrock2_base_conversion.cmi                      |   0m00.53s |  123936 ko || -0m00.01s ||      -312 ko |   -1.88% |         -0.25%
  0m00.52s |  120356 ko | ExtractionOCaml/dettman_multiplication.cmi                        |   0m00.50s |  120344 ko || +0m00.02s ||        12 ko |   +4.00% |         +0.00%
  0m00.52s |  123888 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi                 |   0m00.52s |  123416 ko || +0m00.00s ||       472 ko |   +0.00% |         +0.38%
  0m00.52s |  121844 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi          |   0m00.52s |  121848 ko || +0m00.00s ||        -4 ko |   +0.00% |         -0.00%
  0m00.51s |  122700 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi                  |   0m00.53s |  123096 ko || -0m00.02s ||      -396 ko |   -3.77% |         -0.32%
  0m00.50s |  120684 ko | ExtractionOCaml/base_conversion.cmi                               |   0m00.50s |  122432 ko || +0m00.00s ||     -1748 ko |   +0.00% |         -1.42%
  0m00.50s |  120748 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi              |   0m00.57s |  120620 ko || -0m00.06s ||       128 ko |  -12.28% |         +0.10%
  0m00.50s |  120344 ko | ExtractionOCaml/saturated_solinas.cmi                             |   0m00.51s |  120300 ko || -0m00.01s ||        44 ko |   -1.96% |         +0.03%
  0m00.50s |   28344 ko | fiat-zig/src/curve25519_64.zig                                    |   0m00.46s |   28560 ko || +0m00.03s ||      -216 ko |   +8.69% |         -0.75%
  0m00.49s |  123236 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi               |   0m00.53s |  122576 ko || -0m00.04s ||       660 ko |   -7.54% |         +0.53%
  0m00.49s |  120500 ko | ExtractionOCaml/word_by_word_montgomery.cmi                       |   0m00.48s |  120356 ko || +0m00.01s ||       144 ko |   +2.08% |         +0.11%
  0m00.49s |   35980 ko | fiat-json/src/curve25519_64.json                                  |   0m00.52s |   34660 ko || -0m00.03s ||      1320 ko |   -5.76% |         +3.80%
  0m00.49s |   28488 ko | fiat-rust/src/curve25519_64.rs                                    |   0m00.47s |   27384 ko || +0m00.02s ||      1104 ko |   +4.25% |         +4.03%
  0m00.48s |  121720 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi                    |   0m00.52s |  122768 ko || -0m00.04s ||     -1048 ko |   -7.69% |         -0.85%
  0m00.47s |  119616 ko | ExtractionOCaml/solinas_reduction.cmi                             |   0m00.49s |  120324 ko || -0m00.02s ||      -708 ko |   -4.08% |         -0.58%
  0m00.47s |   28124 ko | fiat-c/src/curve25519_64.c                                        |   0m00.45s |   28304 ko || +0m00.01s ||      -180 ko |   +4.44% |         -0.63%
  0m00.44s |   37236 ko | fiat-go/64/curve25519solinas/curve25519solinas.go                 |   0m00.40s |   37736 ko || +0m00.03s ||      -500 ko |   +9.99% |         -1.32%
  0m00.43s |   38744 ko | fiat-json/src/curve25519_solinas_64.json                          |   0m00.43s |   40512 ko || +0m00.00s ||     -1768 ko |   +0.00% |         -4.36%
  0m00.43s |   38224 ko | fiat-rust/src/curve25519_solinas_64.rs                            |   0m00.41s |   37192 ko || +0m00.02s ||      1032 ko |   +4.87% |         +2.77%
  0m00.42s |   45732 ko | fiat-bedrock2/src/curve25519_solinas_64.c                         |   0m00.40s |   42468 ko || +0m00.01s ||      3264 ko |   +4.99% |         +7.68%
  0m00.42s |   37052 ko | fiat-zig/src/curve25519_solinas_64.zig                            |   0m00.41s |   36628 ko || +0m00.01s ||       424 ko |   +2.43% |         +1.15%
  0m00.38s |   37156 ko | fiat-c/src/curve25519_solinas_64.c                                |   0m00.42s |   37160 ko || -0m00.03s ||        -4 ko |   -9.52% |         -0.01%
  0m00.29s |   26484 ko | fiat-go/32/poly1305/poly1305.go                                   |   0m00.28s |   26668 ko || +0m00.00s ||      -184 ko |   +3.57% |         -0.68%
  0m00.26s |   33824 ko | fiat-bedrock2/src/poly1305_32.c                                   |   0m00.26s |   33836 ko || +0m00.00s ||       -12 ko |   +0.00% |         -0.03%
  0m00.24s |   26896 ko | fiat-go/64/secp256k1dettman/secp256k1dettman.go                   |   0m00.22s |   26224 ko || +0m00.01s ||       672 ko |   +9.09% |         +2.56%
  0m00.24s |   26316 ko | fiat-java/src/FiatPoly1305.java                                   |   0m00.22s |   25696 ko || +0m00.01s ||       620 ko |   +9.09% |         +2.41%
  0m00.24s |   31548 ko | fiat-json/src/poly1305_32.json                                    |   0m00.24s |   31200 ko || +0m00.00s ||       348 ko |   +0.00% |         +1.11%
  0m00.23s |   26104 ko | fiat-c/src/poly1305_32.c                                          |   0m00.21s |   25912 ko || +0m00.02s ||       192 ko |   +9.52% |         +0.74%
  0m00.23s |   27116 ko | fiat-go/64/poly1305/poly1305.go                                   |   0m00.17s |   27576 ko || +0m00.06s ||      -460 ko |  +35.29% |         -1.66%
  0m00.23s |   26228 ko | fiat-rust/src/poly1305_32.rs                                      |   0m00.22s |   26228 ko || +0m00.01s ||         0 ko |   +4.54% |         +0.00%
  0m00.22s |   31180 ko | fiat-bedrock2/src/secp256k1_dettman_64.c                          |   0m00.23s |   30968 ko || -0m00.01s ||       212 ko |   -4.34% |         +0.68%
  0m00.21s |   25520 ko | fiat-zig/src/poly1305_32.zig                                      |   0m00.21s |   25420 ko || +0m00.00s ||       100 ko |   +0.00% |         +0.39%
  0m00.20s |   25196 ko | fiat-json/src/secp256k1_dettman_64.json                           |   0m00.19s |   24872 ko || +0m00.01s ||       324 ko |   +5.26% |         +1.30%
  0m00.20s |   22184 ko | fiat-zig/src/secp256k1_dettman_64.zig                             |   0m00.18s |   21864 ko || +0m00.02s ||       320 ko |  +11.11% |         +1.46%
  0m00.18s |   21800 ko | fiat-c/src/secp256k1_dettman_64.c                                 |   0m00.18s |   21800 ko || +0m00.00s ||         0 ko |   +0.00% |         +0.00%
  0m00.18s |   22084 ko | fiat-rust/src/secp256k1_dettman_64.rs                             |   0m00.18s |   22376 ko || +0m00.00s ||      -292 ko |   +0.00% |         -1.30%
  0m00.17s |   61932 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi                      |   0m00.19s |   62248 ko || -0m00.01s ||      -316 ko |  -10.52% |         -0.50%
  0m00.16s |   62528 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi                  |   0m00.16s |   61452 ko || +0m00.00s ||      1076 ko |   +0.00% |         +1.75%
  0m00.15s |   28964 ko | fiat-json/src/poly1305_64.json                                    |   0m00.14s |   27736 ko || +0m00.00s ||      1228 ko |   +7.14% |         +4.42%
  0m00.13s |   25196 ko | fiat-rust/src/poly1305_64.rs                                      |   0m00.12s |   24336 ko || +0m00.01s ||       860 ko |   +8.33% |         +3.53%
  0m00.12s |   29576 ko | fiat-bedrock2/src/poly1305_64.c                                   |   0m00.12s |   29648 ko || +0m00.00s ||       -72 ko |   +0.00% |         -0.24%
  0m00.12s |   24992 ko | fiat-c/src/poly1305_64.c                                          |   0m00.12s |   24612 ko || +0m00.00s ||       380 ko |   +0.00% |         +1.54%
  0m00.12s |   24928 ko | fiat-zig/src/poly1305_64.zig                                      |   0m00.13s |   24612 ko || -0m00.01s ||       316 ko |   -7.69% |         +1.28%

```
</p>
</details>
  • Loading branch information
@JasonGross
JasonGross committed Dec 8, 2023
1 parent 85194d7 commit b3d80ad
Show file tree
Hide file tree
Showing 2 changed files with 46 additions and 3 deletions.
32 changes: 32 additions & 0 deletions src/Rewriter/Rules.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -288,18 +288,35 @@ Definition arith_rewrite_rulesT (max_const_val : Z) : list (bool * Prop)
; (forall s y x,
Z.add_get_carry_full s (- y) x
= dlet vb := Z.sub_get_borrow_full s x y in (fst vb, - snd vb))
; (forall s y x k,
Z.add_get_carry_full s x (-y * k)
= dlet vb := Z.sub_get_borrow_full s x (y * k) in (fst vb, - snd vb))
; (forall s y x k,
Z.add_get_carry_full s (-y * k) x
= dlet vb := Z.sub_get_borrow_full s x (y * k) in (fst vb, - snd vb))
; (forall s y x,
Z.add_with_get_carry_full s 0 x (- y)
= dlet vb := Z.sub_get_borrow_full s x y in (fst vb, - snd vb))
; (forall s y x,
Z.add_with_get_carry_full s 0 (- y) x
= dlet vb := Z.sub_get_borrow_full s x y in (fst vb, - snd vb))

; (forall s c x,
Z.add_with_get_carry_full s (- c) x 0
= dlet vb := Z.sub_with_get_borrow_full s c x 0 in (fst vb, - snd vb))

; (forall s c y x,
Z.add_with_get_carry_full s (- c) (- y) x
= dlet vb := Z.sub_with_get_borrow_full s c x y in (fst vb, - snd vb))
; (forall s c y x,
Z.add_with_get_carry_full s (- c) x (- y)
= dlet vb := Z.sub_with_get_borrow_full s c x y in (fst vb, - snd vb))
; (forall s c y x k,
Z.add_with_get_carry_full s c x (-y * k)
= dlet vb := Z.sub_with_get_borrow_full s (-c) x (y * k) in (fst vb, - snd vb))
; (forall s c y x k,
Z.add_with_get_carry_full s c (-y * k) x
= dlet vb := Z.sub_with_get_borrow_full s (-c) x (y * k) in (fst vb, - snd vb))
; (forall b x, (* inline negation when the rewriter wouldn't already inline it *)
ident.gets_inlined b x = false
-> -x = dlet v := x in -v)
Expand Down Expand Up @@ -395,6 +412,16 @@ Definition arith_with_casts_rewrite_rulesT (adc_no_carry_to_add : bool) : list (
y ∈ ry -> y = Z.ones (Z.succ (Z.log2 y))
-> cstZ rv (cstZ ry ('y) &' cstZ rx x) = cstZ rx x)
]%Z%zrange
; mymap
do_again
[ (forall x y, cstZ r[0~>1] x * y = Z.zselect (cstZ r[0~>1] x) (cstZ r[0~>0] (' 0)) y)
; (forall x y, y * cstZ r[0~>1] x = Z.zselect (cstZ r[0~>1] x) (cstZ r[0~>0] (' 0)) y)
; (forall c M rv r0 rM, 0 ∈ r0 -> M ∈ rM -> M ∈ rv -> 2^Z.log2 (M+1) = M + 1 -> 1 <= M ->
cstZ rv (Z.zselect (cstZ r[0~>1] c) (cstZ r0 ('0)) (cstZ rM ('M)))
= (dlet vc := cstZZ rv r[0~>1] (Z.sub_with_get_borrow_full ('(M+1)) (cstZ r[0~>1] c) 0 0) in
cstZ rv (fst vc)))
; (forall rv c x y, cstZ rv (Z.zselect c x y) = dlet v := cstZ rv (Z.zselect c x y) in cstZ rv v)
]
; mymap
do_again
[ (* [do_again], so that we can trigger add/sub rules on the output *)
Expand All @@ -415,6 +442,11 @@ Definition arith_with_casts_rewrite_rulesT (adc_no_carry_to_add : bool) : list (
adc_no_carry_to_add = true -> s ∈ rs -> (n rx - n ry - n rc <= r[0~>s-1])%zrange
-> cstZZ rv r[0~>0] (Z.sub_with_get_borrow_full (cstZ rs ('s)) (cstZ rc c) (cstZ rx x) (cstZ ry y))
= (cstZ rv (cstZ rx x - cstZ ry y - cstZ rc c), (cstZ r[0~>0] ('0))))
(* 0-0-c passes through the carry *)
; (forall rv rs s c rx ry,
s ∈ rs -> 0 ∈ rx -> 0 ∈ ry -> -1 / s = -1
-> cstZZ rv r[0~>1] (Z.sub_with_get_borrow_full (cstZ rs ('s)) (cstZ r[0~>1] c) (cstZ rx ('0)) (cstZ ry ('0)))
= (cstZ rv (-(cstZ r[0~>1]c) mod 's), (cstZ r[0~>1] c)))
]%Z%zrange
; mymap
dont_do_again
Expand Down
17 changes: 14 additions & 3 deletions src/Rewriter/RulesProofs.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -258,6 +258,13 @@ Local Ltac interp_good_t_step_arith :=
=> cbv [Z.ltz];
apply unfold_is_bounded_by_bool in Hx;
apply unfold_is_bounded_by_bool in Hy
| [ H : is_bounded_by_bool _ (ZRange.normalize r[0 ~> 1]) = true |- _ ]
=> change (ZRange.normalize r[0 ~> 1]) with r[0 ~> 1]%zrange in *;
cbv [is_bounded_by_bool] in H; cbn [upper lower] in H
| [ H : ?x <> ?a, H' : ?a <= ?x |- _ ] => assert (a < x) by lia; clear H H'
| [ H : 0 < ?x, H' : ?x <= 1 |- _ ] => assert (x = 1) by lia; clear H H'
| [ H : ?x <= 1, H' : 0 <= ?x |- _ ] => assert (x = 0 \/ x = 1) by lia; clear H H'
| [ H : ?x = Z.neg _ |- context[?x] ] => rewrite H
| [ |- context[ident.cast r[0~>0] ?v] ]
=> rewrite (ident.platform_specific_cast_0_is_mod 0 v) by reflexivity
| [ H : ?x = Z.ones _ |- context [Z.land _ ?x] ] => rewrite H
Expand All @@ -283,6 +290,7 @@ Local Ltac interp_good_t_step_arith :=
| progress destruct_head'_and
| progress Z.ltb_to_lt
| progress split_andb
| progress change (0 - 1) with (-1) in *
| match goal with
| [ |- ?a mod ?b = ?a' mod ?b ] => apply f_equal2; lia
| [ |- ?a / ?b = ?a' / ?b ] => apply f_equal2; lia
Expand Down Expand Up @@ -394,6 +402,9 @@ Local Ltac interp_good_t_step_arith :=
=> tryif constr_eq x x' then fail else replace x with x' by lia
| [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_fast
end
| match goal with
| [ |- context[(- _) mod _] ] => rewrite Z.mod_opp_small by lia
end
| saturate_add_sub_bounds_step ].

Local Ltac remove_casts :=
Expand Down Expand Up @@ -598,17 +609,17 @@ Proof.
-- rewrite <- Z.mod_divide_full. assumption.
+ rewrite H2. apply Ones.Z.ones_nonneg. remember (Z.log2_nonneg (upper)). lia.
+ lia.
+ rewrite H2. apply Ones.Z.ones_nonneg. remember (Z.log2_nonneg (upper)). lia.
+ rewrite H2. apply Ones.Z.ones_nonneg. remember (Z.log2_nonneg (upper)). lia.
Qed.

Lemma arith_with_relaxed_casts_rewrite_rules_proofs
: PrimitiveHList.hlist (@snd bool Prop) arith_with_relaxed_casts_rewrite_rulesT.
Proof using Type.
start_proof; auto; intros; try lia.
- apply relaxed_rules_work; assumption.
- rewrite Z.land_comm. apply relaxed_rules_work; assumption.
Qed.

Lemma strip_literal_casts_rewrite_rules_proofs
: PrimitiveHList.hlist (@snd bool Prop) strip_literal_casts_rewrite_rulesT.
Proof using Type.
Expand Down

0 comments on commit b3d80ad

Please sign in to comment.