Skip to content

Commit

Permalink
More fine-grained bounds analysis (#1769)
Browse files Browse the repository at this point in the history 
Of `if` and `Z.{max,min,ltb,leb,gtb,geb}`

Splitting out a bit of https://github.com/mit-plv/fiat-crypto/pull/1609
that can be merged in isolation

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

```
     After |   Peak Mem | File Name                                                         |     Before |   Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
118m07.69s | 2852656 ko | Total Time / Peak Mem                                             | 120m57.22s | 2852384 ko || -2m49.52s ||       272 ko |   -2.33% |         +0.00%
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
  8m11.53s | 2656284 ko | Bedrock/End2End/X25519/GarageDoor.vo                              |   8m35.13s | 2651116 ko || -0m23.60s ||      5168 ko |   -4.58% |         +0.19%
  1m42.29s | 1598056 ko | fiat-rust/src/p384_32.rs                                          |   1m53.13s | 1711156 ko || -0m10.84s ||   -113100 ko |   -9.58% |         -6.60%
  1m40.37s | 1910616 ko | Bedrock/End2End/X25519/AddPrecomputed.vo                          |   1m50.67s | 1914612 ko || -0m10.29s ||     -3996 ko |   -9.30% |         -0.20%
  1m44.95s | 1868664 ko | fiat-go/32/p384scalar/p384scalar.go                               |   1m53.23s | 1629028 ko || -0m08.27s ||    239636 ko |   -7.31% |        +14.71%
  1m44.01s | 1694084 ko | fiat-json/src/p384_32.json                                        |   1m52.15s | 2062740 ko || -0m08.14s ||   -368656 ko |   -7.25% |        -17.87%
  1m43.70s | 1598448 ko | fiat-go/32/p384/p384.go                                           |   1m51.29s | 2096096 ko || -0m07.58s ||   -497648 ko |   -6.82% |        -23.74%
  1m43.12s | 1970240 ko | fiat-c/src/p384_scalar_32.c                                       |   1m50.95s | 1753688 ko || -0m07.82s ||    216552 ko |   -7.05% |        +12.34%
  1m47.93s | 1777564 ko | fiat-zig/src/p384_scalar_32.zig                                   |   1m54.10s | 1960872 ko || -0m06.16s ||   -183308 ko |   -5.40% |         -9.34%
  1m45.63s | 1859004 ko | fiat-rust/src/p384_scalar_32.rs                                   |   1m52.38s | 1691776 ko || -0m06.75s ||    167228 ko |   -6.00% |         +9.88%
  1m41.00s | 2040020 ko | fiat-c/src/p384_32.c                                              |   1m47.40s | 1613808 ko || -0m06.40s ||    426212 ko |   -5.95% |        +26.41%
  1m49.12s | 1707240 ko | fiat-json/src/p384_scalar_32.json                                 |   1m55.04s | 1915948 ko || -0m05.91s ||   -208708 ko |   -5.14% |        -10.89%
  1m47.23s | 1742608 ko | fiat-zig/src/p384_32.zig                                          |   1m51.91s | 1965108 ko || -0m04.68s ||   -222500 ko |   -4.18% |        -11.32%
  0m34.08s |  108600 ko | fiat-json/src/p521_32.json                                        |   0m38.51s |  110272 ko || -0m04.42s ||     -1672 ko |  -11.50% |         -1.51%
  1m51.33s | 1766248 ko | fiat-java/src/FiatP384Scalar.java                                 |   1m55.23s | 1672896 ko || -0m03.89s ||     93352 ko |   -3.38% |         +5.58%
  1m49.07s | 1677504 ko | fiat-java/src/FiatP384.java                                       |   1m52.11s | 1829396 ko || -0m03.04s ||   -151892 ko |   -2.71% |         -8.30%
  1m48.39s | 2087004 ko | fiat-bedrock2/src/p384_32.c                                       |   1m51.44s | 2002744 ko || -0m03.04s ||     84260 ko |   -2.73% |         +4.20%
  0m41.56s | 2147648 ko | ExtractionOCaml/bedrock2_solinas_reduction                        |   0m43.56s | 2147620 ko || -0m02.00s ||        28 ko |   -4.59% |         +0.00%
  0m16.06s |  305752 ko | fiat-rust/src/p434_64.rs                                          |   0m18.74s |  245968 ko || -0m02.67s ||     59784 ko |  -14.30% |        +24.30%
  5m29.05s | 2852656 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo                   |   5m30.35s | 2852384 ko || -0m01.30s ||       272 ko |   -0.39% |         +0.00%
  1m18.17s | 1527676 ko | Assembly/EquivalenceProofs.vo                                     |   1m19.80s | 1528936 ko || -0m01.62s ||     -1260 ko |   -2.04% |         -0.08%
  0m54.68s |  864844 ko | AbstractInterpretation/ZRangeProofs.vo                            |   0m53.49s |  847940 ko || +0m01.18s ||     16904 ko |   +2.22% |         +1.99%
  0m41.26s | 2147868 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery                  |   0m43.00s | 2147828 ko || -0m01.74s ||        40 ko |   -4.04% |         +0.00%
  0m40.43s | 2147800 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery             |   0m42.31s | 2147868 ko || -0m01.88s ||       -68 ko |   -4.44% |         -0.00%
  0m39.00s | 2148408 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas                 |   0m40.19s | 2148288 ko || -0m01.18s ||       120 ko |   -2.96% |         +0.00%
  0m36.59s | 1642524 ko | ExtractionOCaml/bedrock2_dettman_multiplication                   |   0m38.32s | 1642028 ko || -0m01.72s ||       496 ko |   -4.51% |         +0.03%
  0m36.09s | 1624132 ko | ExtractionOCaml/bedrock2_saturated_solinas                        |   0m37.77s | 1622392 ko || -0m01.67s ||      1740 ko |   -4.44% |         +0.10%
  0m35.64s | 1618740 ko | ExtractionOCaml/bedrock2_base_conversion                          |   0m37.32s | 1620464 ko || -0m01.67s ||     -1724 ko |   -4.50% |         -0.10%
  0m35.51s | 1627416 ko | ExtractionOCaml/with_bedrock2_saturated_solinas                   |   0m36.77s | 1623636 ko || -0m01.26s ||      3780 ko |   -3.42% |         +0.23%
  0m35.32s | 1618208 ko | ExtractionOCaml/with_bedrock2_base_conversion                     |   0m36.78s | 1620312 ko || -0m01.46s ||     -2104 ko |   -3.96% |         -0.12%
  0m35.16s | 1624836 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication              |   0m36.65s | 1624768 ko || -0m01.49s ||        68 ko |   -4.06% |         +0.00%
  0m28.09s | 1232176 ko | ExtractionOCaml/perf_unsaturated_solinas                          |   0m29.26s | 1232192 ko || -0m01.17s ||       -16 ko |   -3.99% |         -0.00%
  0m17.56s |  306028 ko | fiat-go/64/p434/p434.go                                           |   0m18.81s |  312620 ko || -0m01.25s ||     -6592 ko |   -6.64% |         -2.10%
  0m17.14s |  233816 ko | fiat-c/src/p434_64.c                                              |   0m18.20s |  233352 ko || -0m01.05s ||       464 ko |   -5.82% |         +0.19%
  0m15.36s |  426148 ko | fiat-json/src/curve25519_scalar_32.json                           |   0m16.62s |  378608 ko || -0m01.26s ||     47540 ko |   -7.58% |        +12.55%
  4m01.16s | 2561424 ko | Assembly/WithBedrock/Proofs.vo                                    |   4m00.36s | 2560184 ko || +0m00.79s ||      1240 ko |   +0.33% |         +0.04%
  3m13.40s | 2602832 ko | Bedrock/End2End/RupicolaCrypto/ChaCha20.vo                        |   3m13.52s | 2602864 ko || -0m00.12s ||       -32 ko |   -0.06% |         -0.00%
  1m51.86s | 1595228 ko | Bedrock/End2End/X25519/Field25519.vo                              |   1m51.80s | 1594816 ko || +0m00.06s ||       412 ko |   +0.05% |         +0.02%
  1m48.00s | 1749600 ko | fiat-bedrock2/src/p384_scalar_32.c                                |   1m48.76s | 2096800 ko || -0m00.75s ||   -347200 ko |   -0.69% |        -16.55%
  1m47.72s | 2435524 ko | Fancy/Barrett256.vo                                               |   1m47.86s | 2427488 ko || -0m00.14s ||      8036 ko |   -0.12% |         +0.33%
  1m28.12s | 2041012 ko | SlowPrimeSynthesisExamples.vo                                     |   1m28.22s | 2041020 ko || -0m00.09s ||        -8 ko |   -0.11% |         -0.00%
  1m08.85s | 1435264 ko | Assembly/WithBedrock/SymbolicProofs.vo                            |   1m08.65s | 1437236 ko || +0m00.19s ||     -1972 ko |   +0.29% |         -0.13%
  1m01.35s |  875184 ko | AbstractInterpretation/Wf.vo                                      |   1m01.39s |  875564 ko || -0m00.03s ||      -380 ko |   -0.06% |         -0.04%
  0m47.33s | 1517272 ko | Assembly/Symbolic.vo                                              |   0m47.25s | 1517300 ko || +0m00.07s ||       -28 ko |   +0.16% |         -0.00%
  0m45.93s | 1761576 ko | Fancy/Montgomery256.vo                                            |   0m45.85s | 1758788 ko || +0m00.07s ||      2788 ko |   +0.17% |         +0.15%
  0m45.55s | 1106852 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo          |   0m45.30s | 1108620 ko || +0m00.25s ||     -1768 ko |   +0.55% |         -0.15%
  0m41.79s | 2146792 ko | ExtractionOCaml/solinas_reduction                                 |   0m41.41s | 2146912 ko || +0m00.38s ||      -120 ko |   +0.91% |         -0.00%
  0m40.94s |   66976 ko | fiat-go/32/p521/p521.go                                           |   0m41.62s |   62044 ko || -0m00.67s ||      4932 ko |   -1.63% |         +7.94%
  0m40.04s | 2148432 ko | ExtractionOCaml/bedrock2_unsaturated_solinas                      |   0m41.02s | 2148352 ko || -0m00.98s ||        80 ko |   -2.38% |         +0.00%
  0m39.54s | 2146728 ko | ExtractionOCaml/word_by_word_montgomery                           |   0m39.44s | 2146928 ko || +0m00.10s ||      -200 ko |   +0.25% |         -0.00%
  0m38.92s |  143296 ko | fiat-bedrock2/src/p521_32.c                                       |   0m38.94s |  140708 ko || -0m00.01s ||      2588 ko |   -0.05% |         +1.83%
  0m38.60s | 1013256 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo                      |   0m38.76s | 1014568 ko || -0m00.15s ||     -1312 ko |   -0.41% |         -0.12%
  0m38.33s |   64612 ko | fiat-zig/src/p521_32.zig                                          |   0m38.23s |   64104 ko || +0m00.10s ||       508 ko |   +0.26% |         +0.79%
  0m37.84s |   61744 ko | fiat-java/src/FiatP521.java                                       |   0m38.30s |   62888 ko || -0m00.45s ||     -1144 ko |   -1.20% |         -1.81%
  0m37.61s |   63940 ko | fiat-rust/src/p521_32.rs                                          |   0m38.25s |   60432 ko || -0m00.64s ||      3508 ko |   -1.67% |         +5.80%
  0m37.53s |   60244 ko | fiat-c/src/p521_32.c                                              |   0m38.16s |   61116 ko || -0m00.62s ||      -872 ko |   -1.65% |         -1.42%
  0m36.96s | 1652372 ko | ExtractionOCaml/unsaturated_solinas                               |   0m36.97s | 1652860 ko || -0m00.00s ||      -488 ko |   -0.02% |         -0.02%
  0m36.39s | 1319040 ko | Bedrock/End2End/X25519/GarageDoorTop.vo                           |   0m36.96s | 1319208 ko || -0m00.57s ||      -168 ko |   -1.54% |         -0.01%
  0m35.47s | 1626948 ko | ExtractionOCaml/with_bedrock2_solinas_reduction                   |   0m35.91s | 1623640 ko || -0m00.43s ||      3308 ko |   -1.22% |         +0.20%
  0m35.40s | 1532564 ko | ExtractionOCaml/base_conversion                                   |   0m34.76s | 1534804 ko || +0m00.64s ||     -2240 ko |   +1.84% |         -0.14%
  0m34.67s | 1556164 ko | ExtractionOCaml/dettman_multiplication                            |   0m34.66s | 1555920 ko || +0m00.01s ||       244 ko |   +0.02% |         +0.01%
  0m34.04s | 2239244 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml                     |   0m34.06s | 2241716 ko || -0m00.02s ||     -2472 ko |   -0.05% |         -0.11%
  0m33.88s | 1279440 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo                        |   0m34.21s | 1279492 ko || -0m00.32s ||       -52 ko |   -0.96% |         -0.00%
  0m33.55s | 1536436 ko | ExtractionOCaml/saturated_solinas                                 |   0m33.64s | 1537180 ko || -0m00.09s ||      -744 ko |   -0.26% |         -0.04%
  0m33.12s | 2217312 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml               |   0m33.14s | 2203232 ko || -0m00.02s ||     14080 ko |   -0.06% |         +0.63%
  0m33.07s | 2216360 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml          |   0m33.22s | 2203556 ko || -0m00.14s ||     12804 ko |   -0.45% |         +0.58%
  0m32.66s | 2139416 ko | ExtractionOCaml/solinas_reduction.ml                              |   0m32.73s | 2136004 ko || -0m00.07s ||      3412 ko |   -0.21% |         +0.15%
  0m31.59s | 2121628 ko | ExtractionOCaml/word_by_word_montgomery.ml                        |   0m31.75s | 2120436 ko || -0m00.16s ||      1192 ko |   -0.50% |         +0.05%
  0m30.49s | 2124060 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml                   |   0m30.19s | 2135432 ko || +0m00.29s ||    -11372 ko |   +0.99% |         -0.53%
  0m30.12s | 2124092 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml              |   0m30.10s | 2136124 ko || +0m00.01s ||    -12032 ko |   +0.06% |         -0.56%
  0m29.34s |  701176 ko | AbstractInterpretation/Proofs.vo                                  |   0m29.28s |  704144 ko || +0m00.05s ||     -2968 ko |   +0.20% |         -0.42%
  0m29.30s | 1522160 ko | StandaloneDebuggingExamples.vo                                    |   0m29.30s | 1518292 ko || +0m00.00s ||      3868 ko |   +0.00% |         +0.25%
  0m28.80s | 2031644 ko | ExtractionOCaml/unsaturated_solinas.ml                            |   0m28.59s | 2032480 ko || +0m00.21s ||      -836 ko |   +0.73% |         -0.04%
  0m28.79s | 1232252 ko | ExtractionOCaml/perf_word_by_word_montgomery                      |   0m29.69s | 1232280 ko || -0m00.90s ||       -28 ko |   -3.03% |         -0.00%
  0m27.14s | 2070388 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml                |   0m27.14s | 2071988 ko || +0m00.00s ||     -1600 ko |   +0.00% |         -0.07%
  0m26.26s | 2000772 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml                     |   0m26.20s | 1996072 ko || +0m00.06s ||      4700 ko |   +0.22% |         +0.23%
  0m26.18s | 2038572 ko | ExtractionOCaml/bedrock2_base_conversion.ml                       |   0m26.15s | 2039460 ko || +0m00.03s ||      -888 ko |   +0.11% |         -0.04%
  0m26.06s | 2000140 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml                |   0m26.06s | 1997496 ko || +0m00.00s ||      2644 ko |   +0.00% |         +0.13%
  0m26.03s | 2000976 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml                |   0m26.06s | 1997080 ko || -0m00.02s ||      3896 ko |   -0.11% |         +0.19%
  0m25.96s | 2001216 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml           |   0m26.02s | 1997732 ko || -0m00.05s ||      3484 ko |   -0.23% |         +0.17%
  0m25.50s | 2038700 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml                  |   0m26.34s | 2040380 ko || -0m00.83s ||     -1680 ko |   -3.18% |         -0.08%
  0m25.39s | 1943804 ko | ExtractionOCaml/dettman_multiplication.ml                         |   0m25.29s | 1940856 ko || +0m00.10s ||      2948 ko |   +0.39% |         +0.15%
  0m25.29s | 1370488 ko | PerfTesting/PerfTestSearch.vo                                     |   0m25.48s | 1373524 ko || -0m00.19s ||     -3036 ko |   -0.74% |         -0.22%
  0m24.75s | 1921636 ko | ExtractionOCaml/base_conversion.ml                                |   0m24.79s | 1921920 ko || -0m00.03s ||      -284 ko |   -0.16% |         -0.01%
  0m24.52s | 1930464 ko | ExtractionOCaml/saturated_solinas.ml                              |   0m24.58s | 1930692 ko || -0m00.05s ||      -228 ko |   -0.24% |         -0.01%
  0m23.82s | 1184144 ko | PushButtonSynthesis/UnsaturatedSolinas.vo                         |   0m23.87s | 1184016 ko || -0m00.05s ||       128 ko |   -0.20% |         +0.01%
  0m21.72s | 1350932 ko | Bedrock/End2End/RupicolaCrypto/Low.vo                             |   0m21.72s | 1350828 ko || +0m00.00s ||       104 ko |   +0.00% |         +0.00%
  0m20.50s | 1158648 ko | PushButtonSynthesis/WordByWordMontgomery.vo                       |   0m20.70s | 1157940 ko || -0m00.19s ||       708 ko |   -0.96% |         +0.06%
  0m20.43s |  797092 ko | Bedrock/Field/Translation/Proofs/Expr.vo                          |   0m20.43s |  794660 ko || +0m00.00s ||      2432 ko |   +0.00% |         +0.30%
  0m19.00s | 1129620 ko | Bedrock/Field/Translation/Proofs/Func.vo                          |   0m19.03s | 1130752 ko || -0m00.03s ||     -1132 ko |   -0.15% |         -0.10%
  0m18.97s | 1826476 ko | ExtractionOCaml/perf_unsaturated_solinas.ml                       |   0m18.96s | 1826428 ko || +0m00.00s ||        48 ko |   +0.05% |         +0.00%
  0m18.96s | 1869440 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml                   |   0m19.48s | 1869604 ko || -0m00.51s ||      -164 ko |   -2.66% |         -0.00%
  0m18.88s |  742056 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo                 |   0m18.85s |  737320 ko || +0m00.02s ||      4736 ko |   +0.15% |         +0.64%
  0m18.59s |  291896 ko | fiat-bedrock2/src/p434_64.c                                       |   0m18.16s |  352412 ko || +0m00.42s ||    -60516 ko |   +2.36% |        -17.17%
  0m17.88s |  252104 ko | fiat-zig/src/p434_64.zig                                          |   0m17.38s |  250948 ko || +0m00.50s ||      1156 ko |   +2.87% |         +0.46%
  0m17.59s | 1373672 ko | PerfTesting/PerfTestSearchPattern.vo                              |   0m17.59s | 1373380 ko || +0m00.00s ||       292 ko |   +0.00% |         +0.02%
  0m17.56s |  497844 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_32.c                |   0m17.66s |  489084 ko || -0m00.10s ||      8760 ko |   -0.56% |         +1.79%
  0m17.41s |  291724 ko | fiat-json/src/p434_64.json                                        |   0m17.60s |  312988 ko || -0m00.19s ||    -21264 ko |   -1.07% |         -6.79%
  0m17.35s |  404072 ko | fiat-bedrock2/src/p256_scalar_32.c                                |   0m17.40s |  428080 ko || -0m00.04s ||    -24008 ko |   -0.28% |         -5.60%
  0m17.26s | 1206516 ko | Bedrock/Field/Synthesis/New/Signature.vo                          |   0m17.32s | 1208232 ko || -0m00.05s ||     -1716 ko |   -0.34% |         -0.14%
  0m17.20s |  338132 ko | fiat-java/src/FiatSecp256K1MontgomeryScalar.java                  |   0m17.22s |  362240 ko || -0m00.01s ||    -24108 ko |   -0.11% |         -6.65%
  0m17.18s | 1127712 ko | Bedrock/End2End/Poly1305/Field1305.vo                             |   0m17.07s | 1127832 ko || +0m00.10s ||      -120 ko |   +0.64% |         -0.01%
  0m17.11s | 1145988 ko | Bedrock/Field/Translation/Proofs/Cmd.vo                           |   0m17.13s | 1146100 ko || -0m00.01s ||      -112 ko |   -0.11% |         -0.00%
  0m17.06s |  387120 ko | fiat-bedrock2/src/secp256k1_montgomery_32.c                       |   0m16.54s |  443456 ko || +0m00.51s ||    -56336 ko |   +3.14% |        -12.70%
  0m16.96s |  422020 ko | fiat-bedrock2/src/curve25519_scalar_32.c                          |   0m17.02s |  405584 ko || -0m00.05s ||     16436 ko |   -0.35% |         +4.05%
  0m16.81s |  422192 ko | fiat-java/src/FiatP256Scalar.java                                 |   0m16.85s |  342228 ko || -0m00.04s ||     79964 ko |   -0.23% |        +23.36%
  0m16.66s |  442624 ko | fiat-zig/src/p256_scalar_32.zig                                   |   0m16.95s |  409628 ko || -0m00.28s ||     32996 ko |   -1.71% |         +8.05%
  0m16.65s |  438324 ko | fiat-zig/src/secp256k1_montgomery_scalar_32.zig                   |   0m17.11s |  346784 ko || -0m00.46s ||     91540 ko |   -2.68% |        +26.39%
  0m16.64s |  407624 ko | fiat-json/src/p256_scalar_32.json                                 |   0m17.19s |  455400 ko || -0m00.55s ||    -47776 ko |   -3.19% |        -10.49%
  0m16.53s |  345100 ko | fiat-go/32/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go |   0m17.28s |  346872 ko || -0m00.75s ||     -1772 ko |   -4.34% |         -0.51%
  0m16.53s |  396644 ko | fiat-zig/src/secp256k1_montgomery_32.zig                          |   0m16.02s |  435648 ko || +0m00.51s ||    -39004 ko |   +3.18% |         -8.95%
  0m16.51s | 2094100 ko | ExtractionHaskell/with_bedrock2_solinas_reduction.hs              |   0m15.61s | 2095512 ko || +0m00.90s ||     -1412 ko |   +5.76% |         -0.06%
  0m16.49s |  406684 ko | fiat-zig/src/curve25519_scalar_32.zig                             |   0m15.98s |  345112 ko || +0m00.50s ||     61572 ko |   +3.19% |        +17.84%
  0m16.37s | 2093460 ko | ExtractionHaskell/bedrock2_solinas_reduction.hs                   |   0m16.35s | 2093640 ko || +0m00.01s ||      -180 ko |   +0.12% |         -0.00%
  0m16.34s |  355372 ko | fiat-go/32/p256scalar/p256scalar.go                               |   0m17.01s |  336536 ko || -0m00.67s ||     18836 ko |   -3.93% |         +5.59%
  0m16.30s |  406028 ko | fiat-java/src/FiatCurve25519Scalar.java                           |   0m16.86s |  405600 ko || -0m00.55s ||       428 ko |   -3.32% |         +0.10%
  0m16.28s |  398648 ko | fiat-c/src/secp256k1_montgomery_scalar_32.c                       |   0m16.65s |  410752 ko || -0m00.36s ||    -12104 ko |   -2.22% |         -2.94%
  0m16.26s |  392892 ko | fiat-json/src/secp256k1_montgomery_32.json                        |   0m16.20s |  380020 ko || +0m00.06s ||     12872 ko |   +0.37% |         +3.38%
  0m16.21s |  404640 ko | fiat-rust/src/p256_scalar_32.rs                                   |   0m16.94s |  345940 ko || -0m00.73s ||     58700 ko |   -4.30% |        +16.96%
  0m16.13s | 2010332 ko | ExtractionHaskell/with_bedrock2_word_by_word_montgomery.hs        |   0m16.34s | 2010428 ko || -0m00.21s ||       -96 ko |   -1.28% |         -0.00%
  0m16.08s |  423192 ko | fiat-rust/src/secp256k1_montgomery_scalar_32.rs                   |   0m16.70s |  439012 ko || -0m00.62s ||    -15820 ko |   -3.71% |         -3.60%
  0m16.07s |  414412 ko | fiat-java/src/FiatSecp256K1Montgomery.java                        |   0m16.78s |  368320 ko || -0m00.71s ||     46092 ko |   -4.23% |        +12.51%
  0m16.06s |  408448 ko | fiat-bedrock2/src/p256_32.c                                       |   0m15.79s |  364756 ko || +0m00.26s ||     43692 ko |   +1.70% |        +11.97%
  0m16.06s |  335964 ko | fiat-c/src/p256_scalar_32.c                                       |   0m16.56s |  343336 ko || -0m00.50s ||     -7372 ko |   -3.01% |         -2.14%
  0m15.90s |  330100 ko | fiat-rust/src/secp256k1_montgomery_32.rs                          |   0m16.81s |  440356 ko || -0m00.90s ||   -110256 ko |   -5.41% |        -25.03%
  0m15.85s |  428928 ko | fiat-json/src/secp256k1_montgomery_scalar_32.json                 |   0m16.40s |  361916 ko || -0m00.54s ||     67012 ko |   -3.35% |        +18.51%
  0m15.83s |  352752 ko | fiat-go/32/curve25519scalar/curve25519scalar.go                   |   0m15.84s |  439340 ko || -0m00.00s ||    -86588 ko |   -0.06% |        -19.70%
  0m15.81s |  436524 ko | fiat-c/src/secp256k1_montgomery_32.c                              |   0m16.19s |  429096 ko || -0m00.38s ||      7428 ko |   -2.34% |         +1.73%
  0m15.75s |  443548 ko | fiat-go/32/secp256k1montgomery/secp256k1montgomery.go             |   0m16.69s |  436064 ko || -0m00.94s ||      7484 ko |   -5.63% |         +1.71%
  0m15.74s | 2031652 ko | ExtractionHaskell/solinas_reduction.hs                            |   0m15.71s | 2027732 ko || +0m00.02s ||      3920 ko |   +0.19% |         +0.19%
  0m15.72s |  346384 ko | fiat-rust/src/curve25519_scalar_32.rs                             |   0m16.45s |  356200 ko || -0m00.72s ||     -9816 ko |   -4.43% |         -2.75%
  0m15.56s |  387008 ko | fiat-c/src/curve25519_scalar_32.c                                 |   0m16.01s |  416392 ko || -0m00.45s ||    -29384 ko |   -2.81% |         -7.05%
  0m15.50s |  355240 ko | fiat-zig/src/p256_32.zig                                          |   0m15.72s |  414944 ko || -0m00.22s ||    -59704 ko |   -1.39% |        -14.38%
  0m15.42s | 1983776 ko | ExtractionHaskell/word_by_word_montgomery.hs                      |   0m15.41s | 1985996 ko || +0m00.00s ||     -2220 ko |   +0.06% |         -0.11%
  0m15.41s | 2010140 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs             |   0m16.13s | 2007524 ko || -0m00.71s ||      2616 ko |   -4.46% |         +0.13%
  0m15.14s |  387292 ko | fiat-java/src/FiatP256.java                                       |   0m15.80s |  394640 ko || -0m00.66s ||     -7348 ko |   -4.17% |         -1.86%
  0m15.12s | 1950604 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs                 |   0m15.19s | 1950624 ko || -0m00.07s ||       -20 ko |   -0.46% |         -0.00%
  0m15.07s |  354004 ko | fiat-rust/src/p256_32.rs                                          |   0m15.96s |  390952 ko || -0m00.89s ||    -36948 ko |   -5.57% |         -9.45%
  0m14.87s |  415960 ko | fiat-c/src/p256_32.c                                              |   0m15.48s |  320752 ko || -0m00.61s ||     95208 ko |   -3.94% |        +29.68%
  0m14.86s |  360644 ko | fiat-json/src/p256_32.json                                        |   0m15.39s |  446864 ko || -0m00.53s ||    -86220 ko |   -3.44% |        -19.29%
  0m14.62s | 1933488 ko | ExtractionHaskell/unsaturated_solinas.hs                          |   0m14.75s | 1929252 ko || -0m00.13s ||      4236 ko |   -0.88% |         +0.21%
  0m14.53s |  341776 ko | fiat-go/32/p256/p256.go                                           |   0m15.15s |  362036 ko || -0m00.62s ||    -20260 ko |   -4.09% |         -5.59%
  0m14.47s | 1951532 ko | ExtractionHaskell/with_bedrock2_unsaturated_solinas.hs            |   0m15.34s | 1950416 ko || -0m00.86s ||      1116 ko |   -5.67% |         +0.05%
  0m14.40s | 1886356 ko | ExtractionHaskell/with_bedrock2_dettman_multiplication.hs         |   0m14.39s | 1887008 ko || +0m00.00s ||      -652 ko |   +0.06% |         -0.03%
  0m14.35s | 1886684 ko | ExtractionHaskell/bedrock2_dettman_multiplication.hs              |   0m14.27s | 1886136 ko || +0m00.08s ||       548 ko |   +0.56% |         +0.02%
  0m14.31s | 1932196 ko | ExtractionHaskell/with_bedrock2_base_conversion.hs                |   0m14.24s | 1932776 ko || +0m00.07s ||      -580 ko |   +0.49% |         -0.03%
  0m14.21s | 1862464 ko | ExtractionHaskell/with_bedrock2_saturated_solinas.hs              |   0m14.21s | 1862348 ko || +0m00.00s ||       116 ko |   +0.00% |         +0.00%
  0m14.20s | 1932440 ko | ExtractionHaskell/bedrock2_base_conversion.hs                     |   0m13.64s | 1933348 ko || +0m00.55s ||      -908 ko |   +4.10% |         -0.04%
  0m14.09s | 1863000 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs                   |   0m14.17s | 1861768 ko || -0m00.08s ||      1232 ko |   -0.56% |         +0.06%
  0m13.88s | 1858476 ko | ExtractionHaskell/dettman_multiplication.hs                       |   0m13.90s | 1855680 ko || -0m00.01s ||      2796 ko |   -0.14% |         +0.15%
  0m13.70s | 1848820 ko | ExtractionHaskell/saturated_solinas.hs                            |   0m13.69s | 1847424 ko || +0m00.00s ||      1396 ko |   +0.07% |         +0.07%
  0m13.63s |  601740 ko | Bedrock/Field/Common/Util.vo                                      |   0m13.74s |  607744 ko || -0m00.10s ||     -6004 ko |   -0.80% |         -0.98%
  0m13.51s | 1849984 ko | ExtractionHaskell/base_conversion.hs                              |   0m13.43s | 1850900 ko || +0m00.08s ||      -916 ko |   +0.59% |         -0.04%
  0m13.39s |  664432 ko | Bedrock/Group/AdditionChains.vo                                   |   0m13.36s |  664280 ko || +0m00.03s ||       152 ko |   +0.22% |         +0.02%
  0m13.06s |  668412 ko | Bedrock/Group/ScalarMult/LadderStep.vo                            |   0m13.13s |  667172 ko || -0m00.07s ||      1240 ko |   -0.53% |         +0.18%
  0m11.81s | 1031712 ko | BoundsPipeline.vo                                                 |   0m11.79s | 1030480 ko || +0m00.02s ||      1232 ko |   +0.16% |         +0.11%
  0m11.41s | 1698212 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo               |   0m11.35s | 1698080 ko || +0m00.06s ||       132 ko |   +0.52% |         +0.00%
  0m11.02s |  165236 ko | fiat-go/64/p384scalar/p384scalar.go                               |   0m11.23s |  165448 ko || -0m00.21s ||      -212 ko |   -1.86% |         -0.12%
  0m11.01s |  216400 ko | fiat-bedrock2/src/p384_scalar_64.c                                |   0m11.03s |  194560 ko || -0m00.01s ||     21840 ko |   -0.18% |        +11.22%
  0m10.89s |  191528 ko | fiat-zig/src/p384_scalar_64.zig                                   |   0m11.07s |  193528 ko || -0m00.17s ||     -2000 ko |   -1.62% |         -1.03%
  0m10.83s |  202864 ko | fiat-json/src/p384_scalar_64.json                                 |   0m11.00s |  176204 ko || -0m00.16s ||     26660 ko |   -1.54% |        +15.13%
  0m10.72s |  142328 ko | fiat-rust/src/p384_scalar_64.rs                                   |   0m10.83s |  141448 ko || -0m00.10s ||       880 ko |   -1.01% |         +0.62%
  0m10.59s |  140712 ko | fiat-c/src/p384_scalar_64.c                                       |   0m11.00s |  154528 ko || -0m00.41s ||    -13816 ko |   -3.72% |         -8.94%
  0m10.10s | 1296876 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo              |   0m10.21s | 1296864 ko || -0m00.11s ||        12 ko |   -1.07% |         +0.00%
  0m09.85s |  626712 ko | Bedrock/Field/Translation/Proofs/Flatten.vo                       |   0m09.86s |  624056 ko || -0m00.00s ||      2656 ko |   -0.10% |         +0.42%
  0m09.79s |  215236 ko | fiat-bedrock2/src/p384_64.c                                       |   0m09.43s |  215444 ko || +0m00.35s ||      -208 ko |   +3.81% |         -0.09%
  0m09.41s |  597268 ko | Stringification/IR.vo                                             |   0m09.43s |  596100 ko || -0m00.01s ||      1168 ko |   -0.21% |         +0.19%
  0m09.33s |  165208 ko | fiat-zig/src/p384_64.zig                                          |   0m09.60s |  159780 ko || -0m00.26s ||      5428 ko |   -2.81% |         +3.39%
  0m09.32s | 1035796 ko | PushButtonSynthesis/BaseConversion.vo                             |   0m09.26s | 1035900 ko || +0m00.06s ||      -104 ko |   +0.64% |         -0.01%
  0m09.26s |  660684 ko | Bedrock/Group/ScalarMult/CSwap.vo                                 |   0m09.22s |  660736 ko || +0m00.03s ||       -52 ko |   +0.43% |         -0.00%
  0m09.09s |  281340 ko | fiat-bedrock2/src/p224_32.c                                       |   0m09.37s |  256532 ko || -0m00.27s ||     24808 ko |   -2.98% |         +9.67%
  0m09.07s |  253804 ko | fiat-zig/src/p224_32.zig                                          |   0m09.26s |  253128 ko || -0m00.18s ||       676 ko |   -2.05% |         +0.26%
  0m09.06s |  179420 ko | fiat-go/64/p384/p384.go                                           |   0m09.53s |  159216 ko || -0m00.46s ||     20204 ko |   -4.93% |        +12.68%
  0m09.06s |  144912 ko | fiat-rust/src/p384_64.rs                                          |   0m09.38s |  191232 ko || -0m00.32s ||    -46320 ko |   -3.41% |        -24.22%
  0m09.01s |  261152 ko | fiat-json/src/p224_32.json                                        |   0m08.97s |  238644 ko || +0m00.03s ||     22508 ko |   +0.44% |         +9.43%
  0m09.00s |  174204 ko | fiat-c/src/p384_64.c                                              |   0m09.24s |  151968 ko || -0m00.24s ||     22236 ko |   -2.59% |        +14.63%
  0m09.00s |  224252 ko | fiat-go/32/p224/p224.go                                           |   0m09.37s |  252692 ko || -0m00.36s ||    -28440 ko |   -3.94% |        -11.25%
  0m08.95s |  244668 ko | fiat-java/src/FiatP224.java                                       |   0m09.45s |  244680 ko || -0m00.50s ||       -12 ko |   -5.29% |         -0.00%
  0m08.88s |  194884 ko | fiat-json/src/p384_64.json                                        |   0m09.21s |  174104 ko || -0m00.33s ||     20780 ko |   -3.58% |        +11.93%
  0m08.85s |  274884 ko | fiat-rust/src/p224_32.rs                                          |   0m08.84s |  269904 ko || +0m00.00s ||      4980 ko |   +0.11% |         +1.84%
  0m08.77s |  221004 ko | fiat-c/src/p224_32.c                                              |   0m09.15s |  240672 ko || -0m00.38s ||    -19668 ko |   -4.15% |         -8.17%
  0m08.45s | 1042428 ko | PushButtonSynthesis/Primitives.vo                                 |   0m08.48s | 1043676 ko || -0m00.03s ||     -1248 ko |   -0.35% |         -0.11%
  0m08.35s |  124484 ko | fiat-json/src/p448_solinas_32.json                                |   0m08.62s |  117952 ko || -0m00.26s ||      6532 ko |   -3.13% |         +5.53%
  0m08.15s | 1001028 ko | PushButtonSynthesis/SmallExamples.vo                              |   0m08.22s | 1000832 ko || -0m00.07s ||       196 ko |   -0.85% |         +0.01%
  0m08.11s |   59512 ko | fiat-zig/src/p448_solinas_32.zig                                  |   0m07.90s |   57868 ko || +0m00.20s ||      1644 ko |   +2.65% |         +2.84%
  0m07.95s |   57108 ko | fiat-c/src/p448_solinas_32.c                                      |   0m08.13s |   58904 ko || -0m00.18s ||     -1796 ko |   -2.21% |         -3.04%
  0m07.89s |   58248 ko | fiat-rust/src/p448_solinas_32.rs                                  |   0m08.17s |   59288 ko || -0m00.28s ||     -1040 ko |   -3.42% |         -1.75%
  0m07.55s |  912244 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo         |   0m07.51s |  911348 ko || +0m00.04s ||       896 ko |   +0.53% |         +0.09%
  0m07.17s | 1033452 ko | PushButtonSynthesis/SolinasReduction.vo                           |   0m07.22s | 1033556 ko || -0m00.04s ||      -104 ko |   -0.69% |         -0.01%
  0m06.46s | 1041532 ko | PushButtonSynthesis/BarrettReduction.vo                           |   0m06.43s | 1042724 ko || +0m00.03s ||     -1192 ko |   +0.46% |         -0.11%
  0m06.28s | 1121372 ko | CLI.vo                                                            |   0m06.27s | 1121452 ko || +0m00.01s ||       -80 ko |   +0.15% |         -0.00%
  0m06.20s |   50120 ko | fiat-go/64/p521/p521.go                                           |   0m06.31s |   49576 ko || -0m00.10s ||       544 ko |   -1.74% |         +1.09%
  0m06.07s | 1131040 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo                 |   0m06.03s | 1131092 ko || +0m00.04s ||       -52 ko |   +0.66% |         -0.00%
  0m05.91s |  906776 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo                  |   0m05.90s |  905968 ko || +0m00.00s ||       808 ko |   +0.16% |         +0.08%
  0m05.66s |   66172 ko | fiat-bedrock2/src/p521_64.c                                       |   0m05.56s |   63552 ko || +0m00.10s ||      2620 ko |   +1.79% |         +4.12%
  0m05.45s |   36044 ko | fiat-c/src/p521_64.c                                              |   0m05.36s |   36052 ko || +0m00.08s ||        -8 ko |   +1.67% |         -0.02%
  0m05.45s |   35768 ko | fiat-zig/src/p521_64.zig                                          |   0m05.45s |   35820 ko || +0m00.00s ||       -52 ko |   +0.00% |         -0.14%
  0m05.44s |   50680 ko | fiat-json/src/p521_64.json                                        |   0m05.49s |   50400 ko || -0m00.04s ||       280 ko |   -0.91% |         +0.55%
  0m05.41s |   36092 ko | fiat-rust/src/p521_64.rs                                          |   0m05.49s |   36672 ko || -0m00.08s ||      -580 ko |   -1.45% |         -1.58%
  0m05.31s |  616344 ko | Bedrock/End2End/RupicolaCrypto/Broadcast.vo                       |   0m05.26s |  619692 ko || +0m00.04s ||     -3348 ko |   +0.95% |         -0.54%
  0m04.69s | 1030320 ko | PushButtonSynthesis/DettmanMultiplication.vo                      |   0m04.56s | 1030476 ko || +0m00.13s ||      -156 ko |   +2.85% |         -0.01%
  0m04.50s | 1065264 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo           |   0m04.52s | 1065392 ko || -0m00.01s ||      -128 ko |   -0.44% |         -0.01%
  0m04.40s | 1038916 ko | PushButtonSynthesis/SaturatedSolinas.vo                           |   0m04.39s | 1038120 ko || +0m00.01s ||       796 ko |   +0.22% |         +0.07%
  0m04.27s |  525664 ko | AbstractInterpretation/ZRangeCommonProofs.vo                      |   0m04.20s |  526132 ko || +0m00.06s ||      -468 ko |   +1.66% |         -0.08%
  0m04.02s |  955384 ko | Assembly/Equivalence.vo                                           |   0m04.01s |  958996 ko || +0m00.00s ||     -3612 ko |   +0.24% |         -0.37%
  0m03.93s | 1050124 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo                   |   0m03.99s | 1050092 ko || -0m00.06s ||        32 ko |   -1.50% |         +0.00%
  0m03.88s | 1502888 ko | Bedrock/Everything.vo                                             |   0m04.05s | 1502796 ko || -0m00.16s ||        92 ko |   -4.19% |         +0.00%
  0m03.52s | 1365580 ko | Everything.vo                                                     |   0m03.57s | 1365508 ko || -0m00.04s ||        72 ko |   -1.40% |         +0.00%
  0m03.40s |  667052 ko | Bedrock/Group/ScalarMult/ScalarMult.vo                            |   0m03.41s |  668512 ko || -0m00.01s ||     -1460 ko |   -0.29% |         -0.21%
  0m03.09s | 1072420 ko | Rewriter/PerfTesting/Core.vo                                      |   0m03.11s | 1072220 ko || -0m00.02s ||       200 ko |   -0.64% |         +0.01%
  0m03.05s | 1006368 ko | Bedrock/Field/Translation/Cmd.vo                                  |   0m03.04s | 1007684 ko || +0m00.00s ||     -1316 ko |   +0.32% |         -0.13%
  0m03.04s |  614916 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo                         |   0m03.07s |  613648 ko || -0m00.02s ||      1268 ko |   -0.97% |         +0.20%
  0m02.99s | 1348660 ko | PerfTesting/PerfTestPrint.vo                                      |   0m02.98s | 1346496 ko || +0m00.01s ||      2164 ko |   +0.33% |         +0.16%
  0m02.89s | 1068352 ko | Bedrock/Field/Stringification/Stringification.vo                  |   0m02.86s | 1068140 ko || +0m00.03s ||       212 ko |   +1.04% |         +0.01%
  0m02.83s |   86440 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_64.c                |   0m02.78s |   92448 ko || +0m00.05s ||     -6008 ko |   +1.79% |         -6.49%
  0m02.82s |   83512 ko | fiat-bedrock2/src/p256_scalar_64.c                                |   0m02.82s |   83824 ko || +0m00.00s ||      -312 ko |   +0.00% |         -0.37%
  0m02.81s | 1004916 ko | Bedrock/Field/Translation/Func.vo                                 |   0m02.82s | 1004904 ko || -0m00.00s ||        12 ko |   -0.35% |         +0.00%
  0m02.79s |   73300 ko | fiat-json/src/p256_scalar_64.json                                 |   0m02.77s |   72208 ko || +0m00.02s ||      1092 ko |   +0.72% |         +1.51%
  0m02.78s |   74696 ko | fiat-json/src/secp256k1_montgomery_scalar_64.json                 |   0m02.76s |   70564 ko || +0m00.02s ||      4132 ko |   +0.72% |         +5.85%
  0m02.76s | 1061320 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo          |   0m02.69s | 1061296 ko || +0m00.06s ||        24 ko |   +2.60% |         +0.00%
  0m02.76s |   61376 ko | fiat-zig/src/p256_scalar_64.zig                                   |   0m02.74s |   61368 ko || +0m00.01s ||         8 ko |   +0.72% |         +0.01%
  0m02.73s |   59516 ko | fiat-c/src/secp256k1_montgomery_scalar_64.c                       |   0m02.70s |   60860 ko || +0m00.02s ||     -1344 ko |   +1.11% |         -2.20%
  0m02.73s |   62232 ko | fiat-go/64/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go |   0m02.78s |   62084 ko || -0m00.04s ||       148 ko |   -1.79% |         +0.23%
  0m02.73s |   57104 ko | fiat-zig/src/secp256k1_montgomery_scalar_64.zig                   |   0m02.70s |   58912 ko || +0m00.02s ||     -1808 ko |   +1.11% |         -3.06%
  0m02.71s |   64476 ko | fiat-go/64/p256scalar/p256scalar.go                               |   0m02.78s |   71348 ko || -0m00.06s ||     -6872 ko |   -2.51% |         -9.63%
  0m02.70s | 1103800 ko | StandaloneOCamlMain.vo                                            |   0m02.74s | 1103804 ko || -0m00.04s ||        -4 ko |   -1.45% |         -0.00%
  0m02.69s | 1145340 ko | Bedrock/Standalone/StandaloneHaskellMain.vo                       |   0m02.71s | 1145380 ko || -0m00.02s ||       -40 ko |   -0.73% |         -0.00%
  0m02.69s | 1103604 ko | StandaloneHaskellMain.vo                                          |   0m02.69s | 1103632 ko || +0m00.00s ||       -28 ko |   +0.00% |         -0.00%
  0m02.69s |   61060 ko | fiat-c/src/p256_scalar_64.c                                       |   0m02.69s |   61428 ko || +0m00.00s ||      -368 ko |   +0.00% |         -0.59%
  0m02.69s |   60672 ko | fiat-rust/src/secp256k1_montgomery_scalar_64.rs                   |   0m02.76s |   60612 ko || -0m00.06s ||        60 ko |   -2.53% |         +0.09%
  0m02.66s |   58680 ko | fiat-rust/src/p256_scalar_64.rs                                   |   0m02.75s |   58604 ko || -0m00.08s ||        76 ko |   -3.27% |         +0.12%
  0m02.65s | 1045356 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo                |   0m02.58s | 1044768 ko || +0m00.06s ||       588 ko |   +2.71% |         +0.05%
  0m02.65s | 1131240 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo                       |   0m02.64s | 1131204 ko || +0m00.00s ||        36 ko |   +0.37% |         +0.00%
  0m02.64s |  621660 ko | Bedrock/Field/Interface/Compilation2.vo                           |   0m02.59s |  621772 ko || +0m00.05s ||      -112 ko |   +1.93% |         -0.01%
  0m02.64s | 1066352 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo                         |   0m02.65s | 1066344 ko || -0m00.00s ||         8 ko |   -0.37% |         +0.00%
  0m02.64s | 1145296 ko | Bedrock/Standalone/StandaloneOCamlMain.vo                         |   0m02.58s | 1145232 ko || +0m00.06s ||        64 ko |   +2.32% |         +0.00%
  0m02.58s |   81752 ko | fiat-bedrock2/src/secp256k1_montgomery_64.c                       |   0m02.51s |   88460 ko || +0m00.07s ||     -6708 ko |   +2.78% |         -7.58%
  0m02.58s |   50260 ko | fiat-go/64/p448solinas/p448solinas.go                             |   0m02.66s |   50540 ko || -0m00.08s ||      -280 ko |   -3.00% |         -0.55%
  0m02.54s | 1046728 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo                |   0m02.57s | 1045428 ko || -0m00.02s ||      1300 ko |   -1.16% |         +0.12%
  0m02.53s | 1044668 ko | Bedrock/Field/Translation/Parameters/FE310.vo                     |   0m02.53s | 1044656 ko || +0m00.00s ||        12 ko |   +0.00% |         +0.00%
  0m02.53s |   75236 ko | fiat-json/src/secp256k1_montgomery_64.json                        |   0m02.52s |   75144 ko || +0m00.00s ||        92 ko |   +0.39% |         +0.12%
  0m02.47s |   57796 ko | fiat-zig/src/secp256k1_montgomery_64.zig                          |   0m02.46s |   58824 ko || +0m00.01s ||     -1028 ko |   +0.40% |         -1.74%
  0m02.46s | 1042628 ko | Bedrock/Field/Translation/Parameters/Defaults.vo                  |   0m02.46s | 1041412 ko || +0m00.00s ||      1216 ko |   +0.00% |         +0.11%
  0m02.46s |   69376 ko | fiat-go/64/secp256k1montgomery/secp256k1montgomery.go             |   0m02.45s |   69576 ko || +0m00.00s ||      -200 ko |   +0.40% |         -0.28%
  0m02.42s |   60312 ko | fiat-c/src/secp256k1_montgomery_64.c                              |   0m02.45s |   59556 ko || -0m00.03s ||       756 ko |   -1.22% |         +1.26%
  0m02.40s |   78108 ko | fiat-bedrock2/src/curve25519_scalar_64.c                          |   0m02.39s |   76948 ko || +0m00.00s ||      1160 ko |   +0.41% |         +1.50%
  0m02.37s |   64204 ko | fiat-rust/src/secp256k1_montgomery_64.rs                          |   0m02.45s |   63840 ko || -0m00.08s ||       364 ko |   -3.26% |         +0.57%
  0m02.35s |   67972 ko | fiat-json/src/curve25519_scalar_64.json                           |   0m02.44s |   67576 ko || -0m00.08s ||       396 ko |   -3.68% |         +0.58%
  0m02.32s |   55900 ko | fiat-zig/src/curve25519_scalar_64.zig                             |   0m02.32s |   55884 ko || +0m00.00s ||        16 ko |   +0.00% |         +0.02%
  0m02.28s |   67752 ko | fiat-go/64/curve25519scalar/curve25519scalar.go                   |   0m02.33s |   67920 ko || -0m00.05s ||      -168 ko |   -2.14% |         -0.24%
  0m02.22s |   62560 ko | fiat-c/src/curve25519_scalar_64.c                                 |   0m02.27s |   60776 ko || -0m00.04s ||      1784 ko |   -2.20% |         +2.93%
  0m02.21s |   64476 ko | fiat-rust/src/curve25519_scalar_64.rs                             |   0m02.23s |   64472 ko || -0m00.02s ||         4 ko |   -0.89% |         +0.00%
  0m02.11s |   35492 ko | fiat-go/32/curve25519/curve25519.go                               |   0m02.14s |   37076 ko || -0m00.03s ||     -1584 ko |   -1.40% |         -4.27%
  0m02.09s |   67444 ko | fiat-bedrock2/src/p448_solinas_64.c                               |   0m02.09s |   66572 ko || +0m00.00s ||       872 ko |   +0.00% |         +1.30%
  0m02.05s |  616152 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo                    |   0m02.00s |  615540 ko || +0m00.04s ||       612 ko |   +2.49% |         +0.09%
  0m02.01s |   51624 ko | fiat-json/src/p448_solinas_64.json                                |   0m02.05s |   51400 ko || -0m00.04s ||       224 ko |   -1.95% |         +0.43%
  0m01.99s |   65960 ko | fiat-bedrock2/src/curve25519_32.c                                 |   0m02.00s |   64112 ko || -0m00.01s ||      1848 ko |   -0.50% |         +2.88%
  0m01.98s |   34908 ko | fiat-zig/src/p448_solinas_64.zig                                  |   0m01.98s |   35076 ko || +0m00.00s ||      -168 ko |   +0.00% |         -0.47%
  0m01.97s |  544384 ko | Stringification/Language.vo                                       |   0m01.85s |  545284 ko || +0m00.11s ||      -900 ko |   +6.48% |         -0.16%
  0m01.94s |   80484 ko | fiat-bedrock2/src/p224_64.c                                       |   0m01.92s |   80632 ko || +0m00.02s ||      -148 ko |   +1.04% |         -0.18%
  0m01.93s |   36480 ko | fiat-c/src/p448_solinas_64.c                                      |   0m01.97s |   35164 ko || -0m00.04s ||      1316 ko |   -2.03% |         +3.74%
  0m01.91s |   68372 ko | fiat-json/src/p224_64.json                                        |   0m01.88s |   68740 ko || +0m00.03s ||      -368 ko |   +1.59% |         -0.53%
  0m01.90s |   34104 ko | fiat-rust/src/p448_solinas_64.rs                                  |   0m01.97s |   34452 ko || -0m00.07s ||      -348 ko |   -3.55% |         -1.01%
  0m01.89s |   76504 ko | fiat-bedrock2/src/p256_64.c                                       |   0m01.84s |   76436 ko || +0m00.04s ||        68 ko |   +2.71% |         +0.08%
  0m01.85s |  636172 ko | Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo                 |   0m01.83s |  636080 ko || +0m00.02s ||        92 ko |   +1.09% |         +0.01%
  0m01.85s |   62188 ko | fiat-go/64/p224/p224.go                                           |   0m01.91s |   62196 ko || -0m00.05s ||        -8 ko |   -3.14% |         -0.01%
  0m01.84s |   64332 ko | fiat-zig/src/p224_64.zig                                          |   0m01.86s |   62296 ko || -0m00.02s ||      2036 ko |   -1.07% |         +3.26%
  0m01.83s |   67704 ko | fiat-json/src/p256_64.json                                        |   0m01.90s |   67196 ko || -0m00.06s ||       508 ko |   -3.68% |         +0.75%
  0m01.82s |   57896 ko | fiat-zig/src/p256_64.zig                                          |   0m01.83s |   58884 ko || -0m00.01s ||      -988 ko |   -0.54% |         -1.67%
  0m01.81s |   68648 ko | fiat-go/64/p256/p256.go                                           |   0m01.85s |   68732 ko || -0m00.04s ||       -84 ko |   -2.16% |         -0.12%
  0m01.81s |   48104 ko | fiat-json/src/curve25519_32.json                                  |   0m01.89s |   51216 ko || -0m00.07s ||     -3112 ko |   -4.23% |         -6.07%
  0m01.81s |   61896 ko | fiat-rust/src/p224_64.rs                                          |   0m01.84s |   61188 ko || -0m00.03s ||       708 ko |   -1.63% |         +1.15%
  0m01.80s |   34044 ko | fiat-java/src/FiatCurve25519.java                                 |   0m01.85s |   34004 ko || -0m00.05s ||        40 ko |   -2.70% |         +0.11%
  0m01.78s |   33848 ko | fiat-c/src/curve25519_32.c                                        |   0m01.80s |   33848 ko || -0m00.02s ||         0 ko |   -1.11% |         +0.00%
  0m01.78s |   62420 ko | fiat-c/src/p224_64.c                                              |   0m01.78s |   56260 ko || +0m00.00s ||      6160 ko |   +0.00% |        +10.94%
  0m01.78s |   33040 ko | fiat-zig/src/curve25519_32.zig                                    |   0m01.79s |   33284 ko || -0m00.01s ||      -244 ko |   -0.55% |         -0.73%
  0m01.77s |   59716 ko | fiat-rust/src/p256_64.rs                                          |   0m01.80s |   59012 ko || -0m00.03s ||       704 ko |   -1.66% |         +1.19%
  0m01.76s |   61788 ko | fiat-c/src/p256_64.c                                              |   0m01.76s |   61780 ko || +0m00.00s ||         8 ko |   +0.00% |         +0.01%
  0m01.75s |   33880 ko | fiat-rust/src/curve25519_32.rs                                    |   0m01.79s |   34012 ko || -0m00.04s ||      -132 ko |   -2.23% |         -0.38%
  0m01.56s |  606924 ko | Bedrock/Field/Common/Names/MakeNames.vo                           |   0m01.60s |  607788 ko || -0m00.04s ||      -864 ko |   -2.50% |         -0.14%
  0m01.51s |  590192 ko | CompilersTestCases.vo                                             |   0m01.50s |  590212 ko || +0m00.01s ||       -20 ko |   +0.66% |         -0.00%
  0m01.44s |   51944 ko | fiat-bedrock2/src/secp256k1_dettman_32.c                          |   0m01.45s |   51804 ko || -0m00.01s ||       140 ko |   -0.68% |         +0.27%
  0m01.43s |  511832 ko | AbstractInterpretation/AbstractInterpretation.vo                  |   0m01.49s |  511940 ko || -0m00.06s ||      -108 ko |   -4.02% |         -0.02%
  0m01.39s |  522448 ko | AbstractInterpretation/ZRange.vo                                  |   0m01.41s |  522640 ko || -0m00.02s ||      -192 ko |   -1.41% |         -0.03%
  0m01.38s |  543168 ko | Stringification/Go.vo                                             |   0m01.36s |  541976 ko || +0m00.01s ||      1192 ko |   +1.47% |         +0.21%
  0m01.27s |   41988 ko | fiat-json/src/secp256k1_dettman_32.json                           |   0m01.27s |   41052 ko || +0m00.00s ||       936 ko |   +0.00% |         +2.28%
  0m01.24s |   26744 ko | fiat-java/src/FiatSecp256K1Dettman.java                           |   0m01.23s |   26564 ko || +0m00.01s ||       180 ko |   +0.81% |         +0.67%
  0m01.23s |   25760 ko | fiat-zig/src/secp256k1_dettman_32.zig                             |   0m01.22s |   25624 ko || +0m00.01s ||       136 ko |   +0.81% |         +0.53%
  0m01.20s |   25752 ko | fiat-go/32/secp256k1dettman/secp256k1dettman.go                   |   0m01.23s |   25676 ko || -0m00.03s ||        76 ko |   -2.43% |         +0.29%
  0m01.20s |   25744 ko | fiat-rust/src/secp256k1_dettman_32.rs                             |   0m01.22s |   25596 ko || -0m00.02s ||       148 ko |   -1.63% |         +0.57%
  0m01.19s |   25720 ko | fiat-c/src/secp256k1_dettman_32.c                                 |   0m01.21s |   25612 ko || -0m00.02s ||       108 ko |   -1.65% |         +0.42%
  0m01.15s |  628108 ko | Bedrock/Specs/Field.vo                                            |   0m01.25s |  627916 ko || -0m00.10s ||       192 ko |   -8.00% |         +0.03%
  0m01.06s |  609396 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo                          |   0m01.06s |  608640 ko || +0m00.00s ||       756 ko |   +0.00% |         +0.12%
  0m01.02s |  601076 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo                         |   0m01.04s |  601192 ko || -0m00.02s ||      -116 ko |   -1.92% |         -0.01%
  0m00.94s |  539300 ko | Stringification/C.vo                                              |   0m00.94s |  539324 ko || +0m00.00s ||       -24 ko |   +0.00% |         -0.00%
  0m00.92s |  537052 ko | Stringification/JSON.vo                                           |   0m00.89s |  537668 ko || +0m00.03s ||      -616 ko |   +3.37% |         -0.11%
  0m00.87s |  614388 ko | Bedrock/Field/Interface/Representation.vo                         |   0m00.86s |  615708 ko || +0m00.01s ||     -1320 ko |   +1.16% |         -0.21%
  0m00.85s |  617724 ko | Bedrock/Group/Point.vo                                            |   0m00.88s |  617624 ko || -0m00.03s ||       100 ko |   -3.40% |         +0.01%
  0m00.84s |  535920 ko | Stringification/Zig.vo                                            |   0m00.82s |  541188 ko || +0m00.02s ||     -5268 ko |   +2.43% |         -0.97%
  0m00.83s |  535816 ko | Stringification/Java.vo                                           |   0m00.81s |  535704 ko || +0m00.01s ||       112 ko |   +2.46% |         +0.02%
  0m00.81s |  535004 ko | Stringification/Rust.vo                                           |   0m00.81s |  535796 ko || +0m00.00s ||      -792 ko |   +0.00% |         -0.14%
  0m00.77s |  587864 ko | Bedrock/Field/Common/Tactics.vo                                   |   0m00.75s |  587696 ko || +0m00.02s ||       168 ko |   +2.66% |         +0.02%
  0m00.73s |  546720 ko | Bedrock/Field/Stringification/FlattenVarData.vo                   |   0m00.71s |  546700 ko || +0m00.02s ||        20 ko |   +2.81% |         +0.00%
  0m00.67s |  521656 ko | Bedrock/Field/Common/Arrays/MakeListLengths.vo                    |   0m00.72s |  521652 ko || -0m00.04s ||         4 ko |   -6.94% |         +0.00%
  0m00.67s |  541484 ko | Bedrock/Field/Stringification/LoadStoreListVarData.vo             |   0m00.68s |  541716 ko || -0m00.01s ||      -232 ko |   -1.47% |         -0.04%
  0m00.64s |  516760 ko | AbstractInterpretation/WfExtra.vo                                 |   0m00.67s |  515528 ko || -0m00.03s ||      1232 ko |   -4.47% |         +0.23%
  0m00.62s |   32864 ko | fiat-go/64/curve25519/curve25519.go                               |   0m00.63s |   32848 ko || -0m00.01s ||        16 ko |   -1.58% |         +0.04%
  0m00.54s |  120072 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi               |   0m00.52s |  119948 ko || +0m00.02s ||       124 ko |   +3.84% |         +0.10%
  0m00.53s |  120544 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi              |   0m00.53s |  123744 ko || +0m00.00s ||     -3200 ko |   +0.00% |         -2.58%
  0m00.52s |  120996 ko | ExtractionOCaml/bedrock2_base_conversion.cmi                      |   0m00.51s |  120016 ko || +0m00.01s ||       980 ko |   +1.96% |         +0.81%
  0m00.52s |  123028 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi                  |   0m00.52s |  122568 ko || +0m00.00s ||       460 ko |   +0.00% |         +0.37%
  0m00.52s |  120064 ko | ExtractionOCaml/dettman_multiplication.cmi                        |   0m00.51s |  119968 ko || +0m00.01s ||        96 ko |   +1.96% |         +0.08%
  0m00.52s |  119192 ko | ExtractionOCaml/saturated_solinas.cmi                             |   0m00.49s |  117920 ko || +0m00.03s ||      1272 ko |   +6.12% |         +1.07%
  0m00.52s |  119152 ko | ExtractionOCaml/unsaturated_solinas.cmi                           |   0m00.51s |  119976 ko || +0m00.01s ||      -824 ko |   +1.96% |         -0.68%
  0m00.52s |   38008 ko | fiat-bedrock2/src/curve25519_64.c                                 |   0m00.52s |   38160 ko || +0m00.00s ||      -152 ko |   +0.00% |         -0.39%
  0m00.51s |  119300 ko | ExtractionOCaml/base_conversion.cmi                               |   0m00.49s |  119472 ko || +0m00.02s ||      -172 ko |   +4.08% |         -0.14%
  0m00.51s |  120180 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi                    |   0m00.53s |  122568 ko || -0m00.02s ||     -2388 ko |   -3.77% |         -1.94%
  0m00.51s |  121068 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi                 |   0m00.52s |  119812 ko || -0m00.01s ||      1256 ko |   -1.92% |         +1.04%
  0m00.51s |  120416 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi          |   0m00.52s |  121088 ko || -0m00.01s ||      -672 ko |   -1.92% |         -0.55%
  0m00.51s |  120260 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi               |   0m00.50s |  120972 ko || +0m00.01s ||      -712 ko |   +2.00% |         -0.58%
  0m00.51s |  120244 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi               |   0m00.51s |  122452 ko || +0m00.00s ||     -2208 ko |   +0.00% |         -1.80%
  0m00.51s |  123296 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi             |   0m00.51s |  121612 ko || +0m00.00s ||      1684 ko |   +0.00% |         +1.38%
  0m00.51s |  118932 ko | ExtractionOCaml/word_by_word_montgomery.cmi                       |   0m00.51s |  118492 ko || +0m00.00s ||       440 ko |   +0.00% |         +0.37%
  0m00.51s |   32760 ko | fiat-json/src/curve25519_64.json                                  |   0m00.50s |   33336 ko || +0m00.01s ||      -576 ko |   +2.00% |         -1.72%
  0m00.50s |  120092 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi                    |   0m00.51s |  120440 ko || -0m00.01s ||      -348 ko |   -1.96% |         -0.28%
  0m00.50s |  120028 ko | ExtractionOCaml/solinas_reduction.cmi                             |   0m00.50s |  119036 ko || +0m00.00s ||       992 ko |   +0.00% |         +0.83%
  0m00.49s |  120812 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi         |   0m00.51s |  123016 ko || -0m00.02s ||     -2204 ko |   -3.92% |         -1.79%
  0m00.49s |   26340 ko | fiat-zig/src/curve25519_64.zig                                    |   0m00.48s |   26368 ko || +0m00.01s ||       -28 ko |   +2.08% |         -0.10%
  0m00.46s |   27368 ko | fiat-c/src/curve25519_64.c                                        |   0m00.46s |   27064 ko || +0m00.00s ||       304 ko |   +0.00% |         +1.12%
  0m00.46s |   26276 ko | fiat-rust/src/curve25519_64.rs                                    |   0m00.46s |   25892 ko || +0m00.00s ||       384 ko |   +0.00% |         +1.48%
  0m00.43s |   40400 ko | fiat-bedrock2/src/curve25519_solinas_64.c                         |   0m00.42s |   40528 ko || +0m00.01s ||      -128 ko |   +2.38% |         -0.31%
  0m00.42s |   37480 ko | fiat-json/src/curve25519_solinas_64.json                          |   0m00.44s |   37636 ko || -0m00.02s ||      -156 ko |   -4.54% |         -0.41%
  0m00.41s |   36396 ko | fiat-zig/src/curve25519_solinas_64.zig                            |   0m00.41s |   36708 ko || +0m00.00s ||      -312 ko |   +0.00% |         -0.84%
  0m00.40s |   36716 ko | fiat-c/src/curve25519_solinas_64.c                                |   0m00.40s |   35712 ko || +0m00.00s ||      1004 ko |   +0.00% |         +2.81%
  0m00.40s |   36604 ko | fiat-go/64/curve25519solinas/curve25519solinas.go                 |   0m00.40s |   36456 ko || +0m00.00s ||       148 ko |   +0.00% |         +0.40%
  0m00.39s |   36344 ko | fiat-rust/src/curve25519_solinas_64.rs                            |   0m00.41s |   36104 ko || -0m00.01s ||       240 ko |   -4.87% |         +0.66%
  0m00.28s |   25548 ko | fiat-go/32/poly1305/poly1305.go                                   |   0m00.28s |   25516 ko || +0m00.00s ||        32 ko |   +0.00% |         +0.12%
  0m00.26s |   30308 ko | fiat-json/src/poly1305_32.json                                    |   0m00.24s |   30076 ko || +0m00.02s ||       232 ko |   +8.33% |         +0.77%
  0m00.25s |   32436 ko | fiat-bedrock2/src/poly1305_32.c                                   |   0m00.25s |   32300 ko || +0m00.00s ||       136 ko |   +0.00% |         +0.42%
  0m00.24s |   24584 ko | fiat-rust/src/poly1305_32.rs                                      |   0m00.22s |   24716 ko || +0m00.01s ||      -132 ko |   +9.09% |         -0.53%
  0m00.23s |   29680 ko | fiat-bedrock2/src/secp256k1_dettman_64.c                          |   0m00.23s |   29712 ko || +0m00.00s ||       -32 ko |   +0.00% |         -0.10%
  0m00.23s |   24356 ko | fiat-go/64/secp256k1dettman/secp256k1dettman.go                   |   0m00.24s |   24104 ko || -0m00.00s ||       252 ko |   -4.16% |         +1.04%
  0m00.23s |   23996 ko | fiat-zig/src/poly1305_32.zig                                      |   0m00.21s |   24020 ko || +0m00.02s ||       -24 ko |   +9.52% |         -0.09%
  0m00.22s |   25188 ko | fiat-java/src/FiatPoly1305.java                                   |   0m00.23s |   25100 ko || -0m00.01s ||        88 ko |   -4.34% |         +0.35%
  0m00.21s |   24128 ko | fiat-c/src/poly1305_32.c                                          |   0m00.22s |   24272 ko || -0m00.01s ||      -144 ko |   -4.54% |         -0.59%
  0m00.19s |   20896 ko | fiat-rust/src/secp256k1_dettman_64.rs                             |   0m00.18s |   21240 ko || +0m00.01s ||      -344 ko |   +5.55% |         -1.61%
  0m00.18s |   23760 ko | fiat-json/src/secp256k1_dettman_64.json                           |   0m00.20s |   24196 ko || -0m00.02s ||      -436 ko |  -10.00% |         -1.80%
  0m00.18s |   21172 ko | fiat-zig/src/secp256k1_dettman_64.zig                             |   0m00.17s |   20636 ko || +0m00.00s ||       536 ko |   +5.88% |         +2.59%
  0m00.17s |   20852 ko | fiat-c/src/secp256k1_dettman_64.c                                 |   0m00.19s |   20816 ko || -0m00.01s ||        36 ko |  -10.52% |         +0.17%
  0m00.17s |   25992 ko | fiat-go/64/poly1305/poly1305.go                                   |   0m00.17s |   25912 ko || +0m00.00s ||        80 ko |   +0.00% |         +0.30%
  0m00.16s |   58684 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi                      |   0m00.18s |   59896 ko || -0m00.01s ||     -1212 ko |  -11.11% |         -2.02%
  0m00.15s |   59116 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi                  |   0m00.15s |   58856 ko || +0m00.00s ||       260 ko |   +0.00% |         +0.44%
  0m00.13s |   27404 ko | fiat-json/src/poly1305_64.json                                    |   0m00.14s |   27292 ko || -0m00.01s ||       112 ko |   -7.14% |         +0.41%
  0m00.13s |   23064 ko | fiat-zig/src/poly1305_64.zig                                      |   0m00.12s |   23072 ko || +0m00.01s ||        -8 ko |   +8.33% |         -0.03%
  0m00.12s |   23284 ko | fiat-c/src/poly1305_64.c                                          |   0m00.12s |   23028 ko || +0m00.00s ||       256 ko |   +0.00% |         +1.11%
  0m00.11s |   28008 ko | fiat-bedrock2/src/poly1305_64.c                                   |   0m00.13s |   28304 ko || -0m00.02s ||      -296 ko |  -15.38% |         -1.04%
  0m00.11s |   22892 ko | fiat-rust/src/poly1305_64.rs                                      |   0m00.12s |   22952 ko || -0m00.00s ||       -60 ko |   -8.33% |         -0.26%

```
</p>
</details>
  • Loading branch information
@JasonGross
JasonGross authored Dec 5, 2023
1 parent 81220a6 commit 3961c6a
Show file tree
Hide file tree
Showing 2 changed files with 99 additions and 8 deletions.
40 changes: 32 additions & 8 deletions src/AbstractInterpretation/ZRange.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -282,6 +282,29 @@ Module Compilers.
Lemma interp_beq_lb {t x y} : x = y -> @interp_beq t t x y = true.
Proof. apply reflect_to_beq; exact _. Qed.

Fixpoint union {t} : interp t -> interp t -> interp t
:= match t return interp t -> interp t -> interp t with
| base.type.type_base base.type.Z => Option.map2 ZRange.union
| base.type.type_base _ as t
| base.type.unit as t
=> fun x y
=> if @interp_beq t t x y
then x
else None
| base.type.prod A B => fun '(a, b) '(a', b') =>
(@union A a a', @union B b b')
| base.type.list A => fun la lb => Option.bind2 la lb (fun la lb =>
if Nat.eqb (length la) (length lb)
then Datatypes.Some (List.map (uncurry (@union A)) (List.combine la lb))
else Datatypes.None)
| base.type.option A => fun oa ob => Option.bind2 oa ob (fun l r =>
match l, r return option (option (interp A)) with
| Datatypes.Some l, Datatypes.Some r => Datatypes.Some (Datatypes.Some (union l r))
| Datatypes.None, Datatypes.None => Datatypes.Some Datatypes.None
| _, _ => Datatypes.None
end)
end.

Fixpoint is_bounded_by {t} : interp t -> binterp t -> bool
:= match t with
| base.type.type_base base.type.Z as t
Expand Down Expand Up @@ -573,12 +596,6 @@ Module Compilers.
| None => None
end
| ident.Z_eqb as idc
| ident.Z_leb as idc
| ident.Z_ltb as idc
| ident.Z_geb as idc
| ident.Z_gtb as idc
| ident.Z_max as idc
| ident.Z_min as idc
| ident.Z_pow as idc
| ident.Z_lxor as idc
| ident.Z_modulo as idc
Expand Down Expand Up @@ -623,13 +640,13 @@ Module Compilers.
=> fun t f b
=> match b with
| Some b => if b then t tt else f tt
| None => ZRange.type.base.option.None
| None => type.base.option.union (t tt) (f tt)
end
| ident.bool_rect_nodep _
=> fun t f b
=> match b with
| Some b => if b then t else f
| None => ZRange.type.base.option.None
| None => type.base.option.union t f
end
| ident.option_rect _ _
=> fun s n o
Expand Down Expand Up @@ -737,10 +754,17 @@ Module Compilers.
| ident.List_app _
=> fun ls1 ls2 => ls1 <- ls1; ls2 <- ls2; Some (List.app ls1 ls2)
| ident.List_rev _ => option_map (@List.rev _)
| ident.Z_leb as idc
| ident.Z_ltb as idc
| ident.Z_geb as idc
| ident.Z_gtb as idc
=> fun x y => x <- x; y <- y; ZRange.ToConstant.four_corners Bool.eqb (ident.interp idc) x y
| ident.Z_opp as idc
| ident.Z_log2 as idc
| ident.Z_log2_up as idc
=> fun x => x <- x; Some (ZRange.two_corners (ident.interp idc) x)
| ident.Z_max as idc
| ident.Z_min as idc
| ident.Z_add as idc
| ident.Z_mul as idc
| ident.Z_sub as idc
Expand Down
67 changes: 67 additions & 0 deletions src/AbstractInterpretation/ZRangeProofs.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,7 @@ Require Import Crypto.Util.Tactics.SpecializeBy.
Require Import Crypto.Util.Tactics.SpecializeAllWays.
Require Import Crypto.Util.Tactics.Head.
Require Import Crypto.Util.Tactics.PrintGoal.
Require Import Crypto.Util.Tactics.DoWithHyp.
Require Import Crypto.Language.PreExtra.
Require Import Crypto.CastLemmas.
Require Import Crypto.AbstractInterpretation.ZRange.
Expand All @@ -58,6 +59,61 @@ Module Compilers.
Module option.
Lemma is_bounded_by_None t v : ZRange.type.base.option.is_bounded_by (@ZRange.type.base.option.None t) v = true.
Proof. induction t; cbn; cbv [andb]; break_innermost_match; eauto. Qed.

Lemma tighter_than_union t (rx ry : ZRange.type.base.option.interp t) :
ZRange.type.base.option.is_tighter_than rx (ZRange.type.base.option.union rx ry) = true /\
ZRange.type.base.option.is_tighter_than ry (ZRange.type.base.option.union rx ry) = true.
Proof.
induction t; [destruct t|..]; destruct rx, ry;
cbn [
ZRange.type.base.interp
ZRange.type.base.option.interp
ZRange.type.base.option.is_tighter_than
ZRange.type.base.is_tighter_than
ZRange.type.base.option.union
Option.map2
Option.bind2
] in *; auto 2.
all: fold (@ZRange.type.base.option.interp) in *.
all: break_innermost_match; reflect_hyps; inversion_option; subst; auto 2.
all: split_and.
all: cbn [option_beq].
all: rewrite ?Bool.andb_true_iff; auto.
all: try now split; first [ apply ZRange.is_tighter_than_bool_union_l | apply ZRange.is_tighter_than_bool_union_r ].
all: do 2 try (match goal with
| [ |- context[?x = true] ]
=> lazymatch x with true => fail | false => fail | _ => idtac end;
destruct x eqn:?; progress reflect_hyps
end;
cbn [ZRange.type.base.option.None] in *;
auto 2; subst; try congruence).
{ rewrite 2 fold_andb_map_map.
rewrite 2 fold_andb_map_iff.
rewrite List.combine_length.
do_with_hyp' ltac:(fun H => rewrite H).
rewrite Nat.min_id.
repeat split; intros *; destruct_head'_prod; cbn [uncurry fst snd].
all: rewrite In_nth_error_iff.
all: intros [n H']; revert H'.
all: rewrite !nth_error_combine.
all: break_innermost_match; intros; inversion_option; inversion_pair; subst; auto. }
Qed.

Lemma is_bounded_by_union_l t (rx ry : ZRange.type.base.option.interp t) x :
ZRange.type.base.option.is_bounded_by rx x = true ->
ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union rx ry) x = true.
Proof.
eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; try eassumption;
eapply tighter_than_union.
Qed.

Lemma is_bounded_by_union_r t (rx ry : ZRange.type.base.option.interp t) y :
ZRange.type.base.option.is_bounded_by ry y = true ->
ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union rx ry) y = true.
Proof.
eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; try eassumption;
eapply tighter_than_union.
Qed.
End option.
End base.

Expand Down Expand Up @@ -484,6 +540,16 @@ Module Compilers.
| [ H : (forall a b, ?R0 a b = true -> forall c d, ?R1 c d = true -> forall e f, (forall g h, ?R3 g h = true -> ?R4 (e g) (f h) = true) -> forall i j, ?R5 i j = true -> ?R6 (?F _ _ _ _) (?G _ _ _ _) = true)
|- ?R6 (?F _ _ _ _) (?G _ _ _ _) = true ]
=> apply H; clear H
end
| match goal with
| [ |- ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union _ _) (Bool.Thunked.bool_rect _ _ _ true) = true ]
=> apply ZRange.type.base.option.is_bounded_by_union_l
| [ |- ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union _ _) (Bool.Thunked.bool_rect _ _ _ false) = true ]
=> apply ZRange.type.base.option.is_bounded_by_union_r
| [ |- ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union _ _) (Bool.bool_rect_nodep _ _ true) = true ]
=> apply ZRange.type.base.option.is_bounded_by_union_l
| [ |- ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union _ _) (Bool.bool_rect_nodep _ _ false) = true ]
=> apply ZRange.type.base.option.is_bounded_by_union_r
end ].

Local Lemma mul_by_halves_bounds x y n :
Expand Down Expand Up @@ -751,6 +817,7 @@ Module Compilers.
end
| intros; mul_by_halves_t ].
all: try solve [ non_arith_t; Z.ltb_to_lt; reflexivity ].
all: try solve [ cbv [ZRange.ToConstant.four_corners ZRange.ToConstant.Option.four_corners ZRange.ToConstant.Option.apply_to_range ZRange.ToConstant.Option.two_corners ZRange.ToConstant.Option.union option_beq Bool.eqb] in *; non_arith_t; Z.ltb_to_lt; lia ].
(** For command-line debugging, we display goals that should not remain *)
all: [ > idtac "WARNING: Remaining goal:"; print_context_and_goal () .. ].
Qed.
Expand Down

0 comments on commit 3961c6a

Please sign in to comment.