Avoid bottomify-ing higher order functions

Reworked value type to more closely match the possible spec.

Deduplicated `interp_ident` / `abstract_interp_ident` overlapped state.

The specification of `reify` and `reflect` has been simplified to more
closely match the intuition: `reify`'s spec no longer talks about output
bounds, only interpretation, and a companion lemma
`abstraction_relation_of_related_bounded_value'` shows that the spec of
`reflect` is effectively one direction of an isomorphism between
interpreted-values bounded by abstract state, and `value`s which are in
relationship with the given interpreted-value.  Not really sure how best
to describe this in words yet, probably needs some digesting work.

There's some interesting lemmas where we have an equivalency between two
ways of representing things only for up-to-second-order types, and an
implication for up-to-third-order types, which is currently all the
identifiers.  But this means that if we add fourth-order identifiers,
we'll have to deal with two different sorts of `Proper` abstraction
relations (one used by `Assembly/Symbolic` and one used by bounds
analysis, though it's possible the `Assembly/Symbolic` one can be
adapted).

* Guard exponentially slow bounds analysis with a flag

With `--fancy-and-powerful-but-exponentially-slow-bounds-analysis`

Idk how to implement a non-exponential PHOAS passe for this.

<details><summary>Timing Diff before guarding with flag</summary>
<p>

```
      After |   Peak Mem | File Name                                                         |     Before |   Peak Mem ||       Change || Change (mem) |   % Change | % Change (mem)
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
5494m57.81s | 2858552 ko | Total Time / Peak Mem                                             | 120m21.13s | 2852328 ko || +5374m36.68s ||      6224 ko |  +4465.73% |         +0.21%
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
 352m04.93s | 1781524 ko | fiat-rust/src/p384_scalar_32.rs                                   |   1m53.74s | 1628856 ko ||  +350m11.18s ||    152668 ko | +18472.99% |         +9.37%
 351m13.49s | 1916288 ko | fiat-java/src/FiatP384Scalar.java                                 |   1m53.23s | 1620248 ko ||  +349m20.26s ||    296040 ko | +18511.22% |        +18.27%
 344m52.23s | 1666100 ko | fiat-go/32/p384scalar/p384scalar.go                               |   1m53.04s | 1734424 ko ||  +342m59.18s ||    -68324 ko | +18205.22% |         -3.93%
 343m32.96s | 1898556 ko | fiat-c/src/p384_scalar_32.c                                       |   1m51.27s | 1627512 ko ||  +341m41.68s ||    271044 ko | +18425.17% |        +16.65%
 341m26.05s | 1834040 ko | fiat-json/src/p384_scalar_32.json                                 |   1m46.90s | 1802484 ko ||  +339m39.14s ||     31556 ko | +19063.75% |         +1.75%
 336m05.54s | 1870632 ko | fiat-rust/src/p384_32.rs                                          |   1m50.16s | 1709428 ko ||  +334m15.38s ||    161204 ko | +18205.68% |         +9.43%
 334m29.07s | 1989180 ko | fiat-java/src/FiatP384.java                                       |   1m52.50s | 1817848 ko ||  +332m36.56s ||    171332 ko | +17739.17% |         +9.42%
 333m35.10s | 1806688 ko | fiat-json/src/p384_32.json                                        |   1m53.94s | 1629284 ko ||  +331m41.15s ||    177404 ko | +17466.35% |        +10.88%
 328m36.71s | 1779836 ko | fiat-bedrock2/src/p384_scalar_32.c                                |   1m48.68s | 1758232 ko ||  +326m48.02s ||     21604 ko | +18041.98% |         +1.22%
 328m39.19s | 1662676 ko | fiat-go/32/p384/p384.go                                           |   1m53.01s | 1625684 ko ||  +326m46.18s ||     36992 ko | +17349.06% |         +2.27%
 321m01.71s | 1709592 ko | fiat-c/src/p384_32.c                                              |   1m49.66s | 2029588 ko ||  +319m12.04s ||   -319996 ko | +17464.93% |        -15.76%
 320m33.13s | 1872256 ko | fiat-bedrock2/src/p384_32.c                                       |   1m48.69s | 1687840 ko ||  +318m44.44s ||    184416 ko | +17595.39% |        +10.92%
 318m14.38s | 2079716 ko | fiat-zig/src/p384_scalar_32.zig                                   |   1m54.15s | 1960684 ko ||  +316m20.22s ||    119032 ko | +16627.44% |         +6.07%
 308m20.28s | 1645516 ko | fiat-zig/src/p384_32.zig                                          |   1m52.66s | 1948020 ko ||  +306m27.61s ||   -302504 ko | +16321.33% |        -15.52%
 140m13.96s | 2858552 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo                   |   5m29.46s | 2852328 ko ||  +134m44.49s ||      6224 ko |  +2453.86% |         +0.21%
  15m08.73s |  412980 ko | fiat-zig/src/secp256k1_montgomery_scalar_32.zig                   |   0m17.06s |  365400 ko ||   +14m51.67s ||     47580 ko |  +5226.67% |        +13.02%
  15m07.92s |  444232 ko | fiat-rust/src/secp256k1_montgomery_scalar_32.rs                   |   0m16.58s |  413372 ko ||   +14m51.33s ||     30860 ko |  +5375.99% |         +7.46%
  15m07.44s |  447232 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_32.c                |   0m17.59s |  396628 ko ||   +14m49.85s ||     50604 ko |  +5058.84% |        +12.75%
  15m05.89s |  413980 ko | fiat-zig/src/p256_scalar_32.zig                                   |   0m17.13s |  404448 ko ||   +14m48.75s ||      9532 ko |  +5188.32% |         +2.35%
  15m00.09s |  462000 ko | fiat-json/src/secp256k1_montgomery_scalar_32.json                 |   0m17.14s |  372928 ko ||   +14m42.95s ||     89072 ko |  +5151.40% |        +23.88%
  14m59.00s |  383440 ko | fiat-go/32/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go |   0m16.75s |  439368 ko ||   +14m42.25s ||    -55928 ko |  +5267.16% |        -12.72%
  14m58.83s |  417168 ko | fiat-java/src/FiatSecp256K1MontgomeryScalar.java                  |   0m17.43s |  335352 ko ||   +14m41.40s ||     81816 ko |  +5056.79% |        +24.39%
  14m57.88s |  378000 ko | fiat-go/32/p256scalar/p256scalar.go                               |   0m16.89s |  362996 ko ||   +14m40.99s ||     15004 ko |  +5216.04% |         +4.13%
  14m43.11s |  453008 ko | fiat-bedrock2/src/curve25519_scalar_32.c                          |   0m16.87s |  404488 ko ||   +14m26.24s ||     48520 ko |  +5134.79% |        +11.99%
  14m42.26s |  423172 ko | fiat-zig/src/curve25519_scalar_32.zig                             |   0m16.75s |  338768 ko ||   +14m25.50s ||     84404 ko |  +5167.22% |        +24.91%
  14m34.97s |  386392 ko | fiat-java/src/FiatSecp256K1Montgomery.java                        |   0m16.92s |  375048 ko ||   +14m18.05s ||     11344 ko |  +5071.21% |         +3.02%
  14m35.14s |  439764 ko | fiat-bedrock2/src/p256_scalar_32.c                                |   0m17.47s |  466176 ko ||   +14m17.66s ||    -26412 ko |  +4909.38% |         -5.66%
  14m33.96s |  418052 ko | fiat-c/src/p256_scalar_32.c                                       |   0m16.30s |  433696 ko ||   +14m17.66s ||    -15644 ko |  +5261.71% |         -3.60%
  14m32.17s |  379176 ko | fiat-zig/src/secp256k1_montgomery_32.zig                          |   0m16.64s |  440088 ko ||   +14m15.52s ||    -60912 ko |  +5141.40% |        -13.84%
  14m32.26s |  386104 ko | fiat-java/src/FiatP256Scalar.java                                 |   0m17.60s |  395220 ko ||   +14m14.65s ||     -9116 ko |  +4856.02% |         -2.30%
  14m20.14s |  476544 ko | fiat-json/src/secp256k1_montgomery_32.json                        |   0m16.80s |  384668 ko ||   +14m03.34s ||     91876 ko |  +5019.88% |        +23.88%
  14m18.94s |  380196 ko | fiat-java/src/FiatCurve25519Scalar.java                           |   0m16.99s |  369068 ko ||   +14m01.95s ||     11128 ko |  +4955.56% |         +3.01%
  14m14.20s |  438032 ko | fiat-bedrock2/src/secp256k1_montgomery_32.c                       |   0m16.55s |  414072 ko ||   +13m57.65s ||     23960 ko |  +5061.32% |         +5.78%
  14m10.18s |  382024 ko | fiat-c/src/secp256k1_montgomery_scalar_32.c                       |   0m16.48s |  349956 ko ||   +13m53.69s ||     32068 ko |  +5058.85% |         +9.16%
  14m07.30s |  380804 ko | fiat-go/32/secp256k1montgomery/secp256k1montgomery.go             |   0m15.85s |  343344 ko ||   +13m51.44s ||     37460 ko |  +5245.74% |        +10.91%
  14m05.83s |  384216 ko | fiat-rust/src/p256_scalar_32.rs                                   |   0m16.99s |  347112 ko ||   +13m48.84s ||     37104 ko |  +4878.39% |        +10.68%
  14m02.24s |  421196 ko | fiat-rust/src/secp256k1_montgomery_32.rs                          |   0m16.59s |  342720 ko ||   +13m45.64s ||     78476 ko |  +4976.79% |        +22.89%
  13m55.86s |  416884 ko | fiat-bedrock2/src/p256_32.c                                       |   0m15.76s |  363984 ko ||   +13m40.10s ||     52900 ko |  +5203.68% |        +14.53%
  13m49.51s |  435140 ko | fiat-zig/src/p256_32.zig                                          |   0m15.90s |  375036 ko ||   +13m33.61s ||     60104 ko |  +5117.04% |        +16.02%
  13m48.55s |  402868 ko | fiat-json/src/curve25519_scalar_32.json                           |   0m16.09s |  444636 ko ||   +13m32.45s ||    -41768 ko |  +5049.47% |         -9.39%
  13m47.62s |  374572 ko | fiat-c/src/curve25519_scalar_32.c                                 |   0m15.90s |  352232 ko ||   +13m31.72s ||     22340 ko |  +5105.15% |         +6.34%
  13m40.58s |  411000 ko | fiat-c/src/secp256k1_montgomery_32.c                              |   0m15.54s |  361600 ko ||   +13m25.04s ||     49400 ko |  +5180.43% |        +13.66%
  13m38.90s |  391764 ko | fiat-java/src/FiatP256.java                                       |   0m15.69s |  392176 ko ||   +13m23.20s ||      -412 ko |  +5119.24% |         -0.10%
  13m28.98s |  382116 ko | fiat-go/32/p256/p256.go                                           |   0m15.69s |  361040 ko ||   +13m13.28s ||     21076 ko |  +5056.02% |         +5.83%
  13m24.91s |  408552 ko | fiat-rust/src/p256_32.rs                                          |   0m15.57s |  405540 ko ||   +13m09.33s ||      3012 ko |  +5069.62% |         +0.74%
  13m25.05s |  424812 ko | fiat-rust/src/curve25519_scalar_32.rs                             |   0m16.29s |  429536 ko ||   +13m08.75s ||     -4724 ko |  +4841.98% |         -1.09%
  13m23.56s |  408716 ko | fiat-json/src/p256_scalar_32.json                                 |   0m17.19s |  433976 ko ||   +13m06.36s ||    -25260 ko |  +4574.57% |         -5.82%
  13m06.66s |  379524 ko | fiat-go/32/curve25519scalar/curve25519scalar.go                   |   0m16.39s |  325156 ko ||   +12m50.26s ||     54368 ko |  +4699.63% |        +16.72%
  13m01.92s |  376048 ko | fiat-c/src/p256_32.c                                              |   0m15.20s |  359812 ko ||   +12m46.71s ||     16236 ko |  +5044.21% |         +4.51%
  12m49.57s |  423456 ko | fiat-json/src/p256_32.json                                        |   0m15.99s |  429740 ko ||   +12m33.58s ||     -6284 ko |  +4712.82% |         -1.46%
   7m46.98s |  284096 ko | fiat-zig/src/p434_64.zig                                          |   0m18.66s |  250696 ko ||    +7m28.31s ||     33400 ko |  +2402.57% |        +13.32%
   7m42.79s |  333916 ko | fiat-json/src/p434_64.json                                        |   0m18.88s |  286668 ko ||    +7m23.91s ||     47248 ko |  +2351.21% |        +16.48%
   7m42.28s |  277712 ko | fiat-go/64/p434/p434.go                                           |   0m18.69s |  239700 ko ||    +7m23.58s ||     38012 ko |  +2373.40% |        +15.85%
   7m34.48s |  367696 ko | fiat-bedrock2/src/p434_64.c                                       |   0m18.03s |  373868 ko ||    +7m16.45s ||     -6172 ko |  +2420.68% |         -1.65%
   7m30.04s |  281384 ko | fiat-c/src/p434_64.c                                              |   0m18.12s |  237136 ko ||    +7m11.92s ||     44248 ko |  +2383.66% |        +18.65%
   7m24.16s |  273604 ko | fiat-rust/src/p434_64.rs                                          |   0m18.41s |  246432 ko ||    +7m05.75s ||     27172 ko |  +2312.60% |        +11.02%
   5m07.03s |  256280 ko | fiat-java/src/FiatP224.java                                       |   0m09.02s |  261688 ko ||    +4m58.00s ||     -5408 ko |  +3303.88% |         -2.06%
   5m00.31s |  238104 ko | fiat-go/32/p224/p224.go                                           |   0m09.01s |  223612 ko ||    +4m51.30s ||     14492 ko |  +3233.07% |         +6.48%
   4m59.60s |  240328 ko | fiat-zig/src/p224_32.zig                                          |   0m09.37s |  225308 ko ||    +4m50.23s ||     15020 ko |  +3097.43% |         +6.66%
   4m57.44s |  288372 ko | fiat-json/src/p224_32.json                                        |   0m09.08s |  283848 ko ||    +4m48.36s ||      4524 ko |  +3175.77% |         +1.59%
   4m57.40s |  239760 ko | fiat-rust/src/p224_32.rs                                          |   0m09.10s |  269448 ko ||    +4m48.29s ||    -29688 ko |  +3168.13% |        -11.01%
   4m48.57s |  310468 ko | fiat-bedrock2/src/p224_32.c                                       |   0m08.99s |  282600 ko ||    +4m39.57s ||     27868 ko |  +3109.89% |         +9.86%
   4m48.27s |  239228 ko | fiat-c/src/p224_32.c                                              |   0m08.96s |  230412 ko ||    +4m39.31s ||      8816 ko |  +3117.29% |         +3.82%
   2m48.44s |  184568 ko | fiat-json/src/p384_scalar_64.json                                 |   0m11.23s |  168860 ko ||    +2m37.21s ||     15708 ko |  +1399.91% |         +9.30%
   2m48.14s |  167980 ko | fiat-zig/src/p384_scalar_64.zig                                   |   0m11.15s |  193456 ko ||    +2m36.98s ||    -25476 ko |  +1407.98% |        -13.16%
   2m43.61s |  213748 ko | fiat-bedrock2/src/p384_scalar_64.c                                |   0m11.14s |  192024 ko ||    +2m32.47s ||     21724 ko |  +1368.67% |        +11.31%
   2m43.36s |  167968 ko | fiat-rust/src/p384_scalar_64.rs                                   |   0m11.11s |  148400 ko ||    +2m32.25s ||     19568 ko |  +1370.38% |        +13.18%
   2m41.95s |  184636 ko | fiat-c/src/p384_scalar_64.c                                       |   0m10.86s |  154744 ko ||    +2m31.08s ||     29892 ko |  +1391.25% |        +19.31%
   2m37.83s |  178156 ko | fiat-go/64/p384scalar/p384scalar.go                               |   0m11.15s |  193256 ko ||    +2m26.67s ||    -15100 ko |  +1315.51% |         -7.81%
   2m29.44s |  166896 ko | fiat-zig/src/p384_64.zig                                          |   0m09.52s |  154632 ko ||    +2m19.91s ||     12264 ko |  +1469.74% |         +7.93%
   2m28.98s |  184900 ko | fiat-json/src/p384_64.json                                        |   0m09.31s |  171972 ko ||    +2m19.66s ||     12928 ko |  +1500.21% |         +7.51%
   2m26.58s |  176112 ko | fiat-go/64/p384/p384.go                                           |   0m09.47s |  181568 ko ||    +2m17.10s ||     -5456 ko |  +1447.83% |         -3.00%
   2m25.35s |  175320 ko | fiat-c/src/p384_64.c                                              |   0m09.21s |  151936 ko ||    +2m16.13s ||     23384 ko |  +1478.17% |        +15.39%
   2m23.86s |  189000 ko | fiat-rust/src/p384_64.rs                                          |   0m09.49s |  145760 ko ||    +2m14.37s ||     43240 ko |  +1415.91% |        +29.66%
   2m23.35s |  211804 ko | fiat-bedrock2/src/p384_64.c                                       |   0m09.35s |  189388 ko ||    +2m14.00s ||     22416 ko |  +1433.15% |        +11.83%
   2m29.46s | 2135192 ko | SlowPrimeSynthesisExamples.vo                                     |   1m28.36s | 2041032 ko ||    +1m01.10s ||     94160 ko |    +69.14% |         +4.61%
   8m55.13s | 2650896 ko | Bedrock/End2End/X25519/GarageDoor.vo                              |   8m25.15s | 2656564 ko ||    +0m29.98s ||     -5668 ko |     +5.93% |         -0.21%
    N/A     |    N/A     | PerfTesting/PerfTestSearch.vo                                     |   0m25.13s | 1373644 ko ||    -0m25.12s ||  -1373644 ko |   -100.00% |       -100.00%
   1m22.31s |  941440 ko | AbstractInterpretation/Wf.vo                                      |   1m00.63s |  875644 ko ||    +0m21.67s ||     65796 ko |    +35.75% |         +7.51%
   0m48.67s |  773988 ko | AbstractInterpretation/Proofs.vo                                  |   0m29.24s |  702092 ko ||    +0m19.43s ||     71896 ko |    +66.45% |        +10.24%
    N/A     |    N/A     | PerfTesting/PerfTestSearchPattern.vo                              |   0m17.89s | 1373708 ko ||    -0m17.89s ||  -1373708 ko |   -100.00% |       -100.00%
   2m05.77s | 1631168 ko | Bedrock/End2End/X25519/Field25519.vo                              |   1m51.28s | 1594648 ko ||    +0m14.48s ||     36520 ko |    +13.02% |         +2.29%
   0m14.59s |   64448 ko | fiat-rust/src/secp256k1_montgomery_scalar_64.rs                   |   0m02.67s |   60756 ko ||    +0m11.92s ||      3692 ko |   +446.44% |         +6.07%
   0m14.52s |   62432 ko | fiat-zig/src/secp256k1_montgomery_scalar_64.zig                   |   0m02.76s |   58520 ko ||    +0m11.75s ||      3912 ko |   +426.08% |         +6.68%
   0m14.45s |   67272 ko | fiat-zig/src/p256_scalar_64.zig                                   |   0m02.73s |   61128 ko ||    +0m11.71s ||      6144 ko |   +429.30% |        +10.05%
   0m14.25s |   62036 ko | fiat-rust/src/p256_scalar_64.rs                                   |   0m02.73s |   59396 ko ||    +0m11.51s ||      2640 ko |   +421.97% |         +4.44%
   0m14.21s |   72352 ko | fiat-json/src/secp256k1_montgomery_scalar_64.json                 |   0m02.82s |   70904 ko ||    +0m11.39s ||      1448 ko |   +403.90% |         +2.04%
   0m14.16s |   62316 ko | fiat-c/src/secp256k1_montgomery_scalar_64.c                       |   0m02.69s |   61008 ko ||    +0m11.47s ||      1308 ko |   +426.39% |         +2.14%
   0m14.02s |   72660 ko | fiat-json/src/p256_scalar_64.json                                 |   0m02.79s |   73116 ko ||    +0m11.23s ||      -456 ko |   +402.50% |         -0.62%
   0m14.01s |   61848 ko | fiat-c/src/p256_scalar_64.c                                       |   0m02.67s |   61148 ko ||    +0m11.33s ||       700 ko |   +424.71% |         +1.14%
   0m13.61s |   67516 ko | fiat-go/64/p256scalar/p256scalar.go                               |   0m02.75s |   71172 ko ||    +0m10.85s ||     -3656 ko |   +394.90% |         -5.13%
   0m13.51s |   85796 ko | fiat-bedrock2/src/p256_scalar_64.c                                |   0m02.80s |   84480 ko ||    +0m10.71s ||      1316 ko |   +382.50% |         +1.55%
   0m13.33s |   66312 ko | fiat-go/64/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go |   0m02.77s |   62180 ko ||    +0m10.56s ||      4132 ko |   +381.22% |         +6.64%
   0m13.20s |   88340 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_64.c                |   0m02.79s |   84980 ko ||    +0m10.41s ||      3360 ko |   +373.11% |         +3.95%
   0m13.16s |   70728 ko | fiat-json/src/secp256k1_montgomery_64.json                        |   0m02.49s |   75256 ko ||    +0m10.67s ||     -4528 ko |   +428.51% |         -6.01%
   0m12.74s |   65292 ko | fiat-zig/src/secp256k1_montgomery_64.zig                          |   0m02.42s |   59724 ko ||    +0m10.32s ||      5568 ko |   +426.44% |         +9.32%
   0m12.72s |   60072 ko | fiat-zig/src/curve25519_scalar_64.zig                             |   0m02.33s |   55908 ko ||    +0m10.39s ||      4164 ko |   +445.92% |         +7.44%
   0m12.66s |   61844 ko | fiat-rust/src/secp256k1_montgomery_64.rs                          |   0m02.44s |   64784 ko ||    +0m10.22s ||     -2940 ko |   +418.85% |         -4.53%
   0m44.36s |   60596 ko | fiat-zig/src/p521_32.zig                                          |   0m34.44s |   60684 ko ||    +0m09.92s ||       -88 ko |    +28.80% |         -0.14%
   0m44.26s |  112564 ko | fiat-json/src/p521_32.json                                        |   0m34.64s |  106924 ko ||    +0m09.61s ||      5640 ko |    +27.77% |         +5.27%
   0m44.00s |   64936 ko | fiat-java/src/FiatP521.java                                       |   0m34.40s |   59656 ko ||    +0m09.60s ||      5280 ko |    +27.90% |         +8.85%
   0m12.18s |   66900 ko | fiat-rust/src/curve25519_scalar_64.rs                             |   0m02.32s |   60304 ko ||    +0m09.85s ||      6596 ko |   +425.00% |        +10.93%
   0m12.07s |   67140 ko | fiat-c/src/secp256k1_montgomery_64.c                              |   0m02.43s |   59524 ko ||    +0m09.64s ||      7616 ko |   +396.70% |        +12.79%
   0m12.06s |   60364 ko | fiat-c/src/curve25519_scalar_64.c                                 |   0m02.27s |   60644 ko ||    +0m09.79s ||      -280 ko |   +431.27% |         -0.46%
   0m12.03s |   68432 ko | fiat-json/src/curve25519_scalar_64.json                           |   0m02.36s |   67732 ko ||    +0m09.67s ||       700 ko |   +409.74% |         +1.03%
   0m11.92s |   84348 ko | fiat-bedrock2/src/secp256k1_montgomery_64.c                       |   0m02.45s |   88860 ko ||    +0m09.46s ||     -4512 ko |   +386.53% |         -5.07%
   0m11.92s |   67724 ko | fiat-go/64/secp256k1montgomery/secp256k1montgomery.go             |   0m02.52s |   71412 ko ||    +0m09.40s ||     -3688 ko |   +373.01% |         -5.16%
   0m11.58s |   64176 ko | fiat-go/64/curve25519scalar/curve25519scalar.go                   |   0m02.32s |   67952 ko ||    +0m09.25s ||     -3776 ko |   +399.13% |         -5.55%
   0m11.37s |   84500 ko | fiat-bedrock2/src/curve25519_scalar_64.c                          |   0m02.28s |   80992 ko ||    +0m09.08s ||      3508 ko |   +398.68% |         +4.33%
   0m10.91s |   60548 ko | fiat-c/src/p224_64.c                                              |   0m01.82s |   61764 ko ||    +0m09.08s ||     -1216 ko |   +499.45% |         -1.96%
   0m10.82s |   65748 ko | fiat-zig/src/p224_64.zig                                          |   0m01.84s |   62532 ko ||    +0m08.98s ||      3216 ko |   +488.04% |         +5.14%
   0m10.55s |   60692 ko | fiat-rust/src/p224_64.rs                                          |   0m01.84s |   61180 ko ||    +0m08.71s ||      -488 ko |   +473.36% |         -0.79%
   0m10.52s |   73812 ko | fiat-json/src/p224_64.json                                        |   0m01.88s |   70604 ko ||    +0m08.64s ||      3208 ko |   +459.57% |         +4.54%
   0m10.37s |   64696 ko | fiat-go/64/p224/p224.go                                           |   0m01.92s |   62144 ko ||    +0m08.44s ||      2552 ko |   +440.10% |         +4.10%
   0m10.11s |   83476 ko | fiat-bedrock2/src/p224_64.c                                       |   0m01.91s |   80568 ko ||    +0m08.19s ||      2908 ko |   +429.31% |         +3.60%
   0m15.25s |  124888 ko | fiat-json/src/p448_solinas_32.json                                |   0m08.23s |  116848 ko ||    +0m07.01s ||      8040 ko |    +85.29% |         +6.88%
   0m09.70s |   75056 ko | fiat-json/src/p256_64.json                                        |   0m01.88s |   66596 ko ||    +0m07.81s ||      8460 ko |   +415.95% |        +12.70%
   0m09.59s |   61964 ko | fiat-zig/src/p256_64.zig                                          |   0m01.79s |   58052 ko ||    +0m07.79s ||      3912 ko |   +435.75% |         +6.73%
   0m09.50s |   82532 ko | fiat-bedrock2/src/p256_64.c                                       |   0m01.84s |   77096 ko ||    +0m07.66s ||      5436 ko |   +416.30% |         +7.05%
   0m09.43s |   61676 ko | fiat-rust/src/p256_64.rs                                          |   0m01.80s |   59200 ko ||    +0m07.62s ||      2476 ko |   +423.88% |         +4.18%
   0m09.40s |   65020 ko | fiat-go/64/p256/p256.go                                           |   0m01.84s |   68656 ko ||    +0m07.56s ||     -3636 ko |   +410.86% |         -5.29%
   0m08.91s |   65360 ko | fiat-c/src/p256_64.c                                              |   0m01.74s |   61792 ko ||    +0m07.16s ||      3568 ko |   +412.06% |         +5.77%
   0m14.66s |   59488 ko | fiat-zig/src/p448_solinas_32.zig                                  |   0m08.21s |   58580 ko ||    +0m06.44s ||       908 ko |    +78.56% |         +1.55%
   0m14.42s |   60808 ko | fiat-rust/src/p448_solinas_32.rs                                  |   0m08.12s |   57972 ko ||    +0m06.30s ||      2836 ko |    +77.58% |         +4.89%
   0m43.35s |   62524 ko | fiat-rust/src/p521_32.rs                                          |   0m38.15s |   60356 ko ||    +0m05.20s ||      2168 ko |    +13.63% |         +3.59%
   0m42.96s |  148852 ko | fiat-bedrock2/src/p521_32.c                                       |   0m38.63s |  145628 ko ||    +0m04.32s ||      3224 ko |    +11.20% |         +2.21%
   0m42.44s |   63004 ko | fiat-c/src/p521_32.c                                              |   0m37.82s |   59428 ko ||    +0m04.61s ||      3576 ko |    +12.21% |         +6.01%
   0m12.71s |   60360 ko | fiat-c/src/p448_solinas_32.c                                      |   0m08.16s |   58932 ko ||    +0m04.55s ||      1428 ko |    +55.75% |         +2.42%
   1m51.21s | 2339376 ko | Fancy/Barrett256.vo                                               |   1m48.02s | 2417076 ko ||    +0m03.18s ||    -77700 ko |     +2.95% |         -3.21%
   0m49.17s | 1960112 ko | Fancy/Montgomery256.vo                                            |   0m46.03s | 1758768 ko ||    +0m03.14s ||    201344 ko |     +6.82% |        +11.44%
   0m39.42s | 1319164 ko | Bedrock/End2End/X25519/GarageDoorTop.vo                           |   0m36.42s | 1319624 ko ||    +0m03.00s ||      -460 ko |     +8.23% |         -0.03%
    N/A     |    N/A     | Bedrock/Everything.vo                                             |   0m03.96s | 1502884 ko ||    -0m03.96s ||  -1502884 ko |   -100.00% |       -100.00%
    N/A     |    N/A     | Everything.vo                                                     |   0m03.45s | 1363476 ko ||    -0m03.45s ||  -1363476 ko |   -100.00% |       -100.00%
    N/A     |    N/A     | PerfTesting/PerfTestPrint.vo                                      |   0m02.94s | 1346788 ko ||    -0m02.94s ||  -1346788 ko |   -100.00% |       -100.00%
   3m59.87s | 2553740 ko | Assembly/WithBedrock/Proofs.vo                                    |   4m01.45s | 2553452 ko ||    -0m01.57s ||       288 ko |     -0.65% |         +0.01%
   1m54.05s | 1916900 ko | Bedrock/End2End/X25519/AddPrecomputed.vo                          |   1m52.31s | 1916820 ko ||    +0m01.73s ||        80 ko |     +1.54% |         +0.00%
   0m43.02s |   64392 ko | fiat-go/32/p521/p521.go                                           |   0m41.64s |   61532 ko ||    +0m01.38s ||      2860 ko |     +3.31% |         +4.64%
   0m38.48s | 2146800 ko | ExtractionOCaml/word_by_word_montgomery                           |   0m40.27s | 2146720 ko ||    -0m01.79s ||        80 ko |     -4.44% |         +0.00%
   0m37.41s | 1617480 ko | ExtractionOCaml/bedrock2_base_conversion                          |   0m36.32s | 1620388 ko ||    +0m01.08s ||     -2908 ko |     +3.00% |         -0.17%
   0m34.27s | 1554400 ko | ExtractionOCaml/dettman_multiplication                            |   0m35.58s | 1556408 ko ||    -0m01.30s ||     -2008 ko |     -3.68% |         -0.12%
   0m33.95s | 1537192 ko | ExtractionOCaml/saturated_solinas                                 |   0m35.03s | 1536764 ko ||    -0m01.07s ||       428 ko |     -3.08% |         +0.02%
   0m33.09s | 1531652 ko | ExtractionOCaml/base_conversion                                   |   0m34.83s | 1534488 ko ||    -0m01.73s ||     -2836 ko |     -4.99% |         -0.18%
   0m18.85s | 1135808 ko | Bedrock/End2End/Poly1305/Field1305.vo                             |   0m17.21s | 1129728 ko ||    +0m01.64s ||      6080 ko |     +9.52% |         +0.53%
   0m06.04s |   52332 ko | fiat-json/src/p521_64.json                                        |   0m04.95s |   50248 ko ||    +0m01.08s ||      2084 ko |    +22.02% |         +4.14%
   0m05.99s |   37064 ko | fiat-zig/src/p521_64.zig                                          |   0m04.90s |   36028 ko ||    +0m01.08s ||      1036 ko |    +22.24% |         +2.87%
   3m13.72s | 2603328 ko | Bedrock/End2End/RupicolaCrypto/ChaCha20.vo                        |   3m12.79s | 2602764 ko ||    +0m00.93s ||       564 ko |     +0.48% |         +0.02%
   1m20.21s | 1524980 ko | Assembly/EquivalenceProofs.vo                                     |   1m19.93s | 1530348 ko ||    +0m00.28s ||     -5368 ko |     +0.35% |         -0.35%
   1m08.96s | 1437312 ko | Assembly/WithBedrock/SymbolicProofs.vo                            |   1m09.05s | 1433128 ko ||    -0m00.08s ||      4184 ko |     -0.13% |         +0.29%
   0m52.36s |  849360 ko | AbstractInterpretation/ZRangeProofs.vo                            |   0m52.56s |  848576 ko ||    -0m00.20s ||       784 ko |     -0.38% |         +0.09%
   0m47.18s | 1522816 ko | Assembly/Symbolic.vo                                              |   0m46.85s | 1519280 ko ||    +0m00.32s ||      3536 ko |     +0.70% |         +0.23%
   0m45.33s | 1104720 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo          |   0m45.27s | 1102688 ko ||    +0m00.05s ||      2032 ko |     +0.13% |         +0.18%
   0m44.21s | 2147564 ko | ExtractionOCaml/bedrock2_solinas_reduction                        |   0m43.87s | 2147536 ko ||    +0m00.34s ||        28 ko |     +0.77% |         +0.00%
   0m43.12s | 2147892 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery             |   0m42.35s | 2147764 ko ||    +0m00.76s ||       128 ko |     +1.81% |         +0.00%
   0m42.80s | 2147776 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery                  |   0m42.72s | 2147720 ko ||    +0m00.07s ||        56 ko |     +0.18% |         +0.00%
   0m41.90s | 2146676 ko | ExtractionOCaml/solinas_reduction                                 |   0m40.99s | 2146676 ko ||    +0m00.90s ||         0 ko |     +2.22% |         +0.00%
   0m41.07s | 2148200 ko | ExtractionOCaml/bedrock2_unsaturated_solinas                      |   0m41.03s | 2148284 ko ||    +0m00.03s ||       -84 ko |     +0.09% |         -0.00%
   0m41.02s | 2148244 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas                 |   0m40.67s | 2148388 ko ||    +0m00.35s ||      -144 ko |     +0.86% |         -0.00%
   0m38.93s | 1016196 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo                      |   0m38.63s | 1016156 ko ||    +0m00.29s ||        40 ko |     +0.77% |         +0.00%
   0m38.12s | 1640756 ko | ExtractionOCaml/bedrock2_dettman_multiplication                   |   0m38.27s | 1642204 ko ||    -0m00.15s ||     -1448 ko |     -0.39% |         -0.08%
   0m37.73s | 1623836 ko | ExtractionOCaml/unsaturated_solinas                               |   0m36.98s | 1653884 ko ||    +0m00.75s ||    -30048 ko |     +2.02% |         -1.81%
   0m37.59s | 1621000 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication              |   0m37.00s | 1623732 ko ||    +0m00.59s ||     -2732 ko |     +1.59% |         -0.16%
   0m37.56s | 1622616 ko | ExtractionOCaml/bedrock2_saturated_solinas                        |   0m37.36s | 1622804 ko ||    +0m00.20s ||      -188 ko |     +0.53% |         -0.01%
   0m37.50s | 1621644 ko | ExtractionOCaml/with_bedrock2_solinas_reduction                   |   0m36.64s | 1624384 ko ||    +0m00.85s ||     -2740 ko |     +2.34% |         -0.16%
   0m37.48s | 1621204 ko | ExtractionOCaml/with_bedrock2_saturated_solinas                   |   0m36.73s | 1622828 ko ||    +0m00.75s ||     -1624 ko |     +2.04% |         -0.10%
   0m37.41s | 1617420 ko | ExtractionOCaml/with_bedrock2_base_conversion                     |   0m36.52s | 1618732 ko ||    +0m00.88s ||     -1312 ko |     +2.43% |         -0.08%
   0m34.91s | 1279244 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo                        |   0m34.52s | 1284212 ko ||    +0m00.38s ||     -4968 ko |     +1.12% |         -0.38%
   0m34.14s | 2240972 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml                     |   0m34.09s | 2237916 ko ||    +0m00.04s ||      3056 ko |     +0.14% |         +0.13%
   0m33.11s | 2212924 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml          |   0m33.05s | 2204728 ko ||    +0m00.06s ||      8196 ko |     +0.18% |         +0.37%
   0m33.01s | 2213528 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml               |   0m33.12s | 2204912 ko ||    -0m00.10s ||      8616 ko |     -0.33% |         +0.39%
   0m32.68s | 2150644 ko | ExtractionOCaml/solinas_reduction.ml                              |   0m32.56s | 2139728 ko ||    +0m00.11s ||     10916 ko |     +0.36% |         +0.51%
   0m31.47s | 2122940 ko | ExtractionOCaml/word_by_word_montgomery.ml                        |   0m31.58s | 2120080 ko ||    -0m00.10s ||      2860 ko |     -0.34% |         +0.13%
   0m30.56s | 2114916 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml                   |   0m30.25s | 2134076 ko ||    +0m00.30s ||    -19160 ko |     +1.02% |         -0.89%
   0m30.28s | 1232236 ko | ExtractionOCaml/perf_word_by_word_montgomery                      |   0m29.68s | 1232100 ko ||    +0m00.60s ||       136 ko |     +2.02% |         +0.01%
   0m30.23s | 1232188 ko | ExtractionOCaml/perf_unsaturated_solinas                          |   0m29.28s | 1232224 ko ||    +0m00.94s ||       -36 ko |     +3.24% |         -0.00%
   0m30.11s | 2114248 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml              |   0m30.11s | 2132752 ko ||    +0m00.00s ||    -18504 ko |     +0.00% |         -0.86%
   0m29.92s | 1526264 ko | StandaloneDebuggingExamples.vo                                    |   0m30.25s | 1518384 ko ||    -0m00.32s ||      7880 ko |     -1.09% |         +0.51%
   0m28.53s | 2051912 ko | ExtractionOCaml/unsaturated_solinas.ml                            |   0m28.57s | 2032036 ko ||    -0m00.03s ||     19876 ko |     -0.14% |         +0.97%
   0m27.17s | 2040956 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml                |   0m27.20s | 2071528 ko ||    -0m00.02s ||    -30572 ko |     -0.11% |         -1.47%
   0m26.36s | 2009348 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml                  |   0m26.30s | 2038044 ko ||    +0m00.05s ||    -28696 ko |     +0.22% |         -1.40%
   0m26.34s | 2019688 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml                |   0m26.08s | 1996180 ko ||    +0m00.26s ||     23508 ko |     +0.99% |         +1.17%
   0m26.32s | 2018796 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml                     |   0m26.30s | 1997428 ko ||    +0m00.01s ||     21368 ko |     +0.07% |         +1.06%
   0m26.18s | 2009056 ko | ExtractionOCaml/bedrock2_base_conversion.ml                       |   0m26.28s | 2037624 ko ||    -0m00.10s ||    -28568 ko |     -0.38% |         -1.40%
   0m26.13s | 2019564 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml                |   0m26.06s | 1996408 ko ||    +0m00.07s ||     23156 ko |     +0.26% |         +1.15%
   0m26.05s | 2016864 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml           |   0m25.95s | 1997412 ko ||    +0m00.10s ||     19452 ko |     +0.38% |         +0.97%
   0m25.24s | 1952220 ko | ExtractionOCaml/dettman_multiplication.ml                         |   0m25.47s | 1939744 ko ||    -0m00.23s ||     12476 ko |     -0.90% |         +0.64%
   0m24.71s | 1944464 ko | ExtractionOCaml/saturated_solinas.ml                              |   0m24.58s | 1934196 ko ||    +0m00.13s ||     10268 ko |     +0.52% |         +0.53%
   0m24.68s | 1914120 ko | ExtractionOCaml/base_conversion.ml                                |   0m25.18s | 1922504 ko ||    -0m00.50s ||     -8384 ko |     -1.98% |         -0.43%
   0m23.73s | 1184052 ko | PushButtonSynthesis/UnsaturatedSolinas.vo                         |   0m23.70s | 1185516 ko ||    +0m00.03s ||     -1464 ko |     +0.12% |         -0.12%
   0m21.52s | 1354084 ko | Bedrock/End2End/RupicolaCrypto/Low.vo                             |   0m21.31s | 1350968 ko ||    +0m00.21s ||      3116 ko |     +0.98% |         +0.23%
   0m20.49s | 1158932 ko | PushButtonSynthesis/WordByWordMontgomery.vo                       |   0m20.38s | 1160828 ko ||    +0m00.10s ||     -1896 ko |     +0.53% |         -0.16%
   0m20.15s |  794468 ko | Bedrock/Field/Translation/Proofs/Expr.vo                          |   0m20.23s |  794720 ko ||    -0m00.08s ||      -252 ko |     -0.39% |         -0.03%
   0m18.98s | 1821220 ko | ExtractionOCaml/perf_unsaturated_solinas.ml                       |   0m18.91s | 1826352 ko ||    +0m00.07s ||     -5132 ko |     +0.37% |         -0.28%
   0m18.80s | 1843872 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml                   |   0m18.84s | 1867344 ko ||    -0m00.03s ||    -23472 ko |     -0.21% |         -1.25%
   0m18.64s |  737284 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo                 |   0m18.64s |  740312 ko ||    +0m00.00s ||     -3028 ko |     +0.00% |         -0.40%
   0m18.55s | 1128568 ko | Bedrock/Field/Translation/Proofs/Func.vo                          |   0m18.89s | 1129264 ko ||    -0m00.33s ||      -696 ko |     -1.79% |         -0.06%
   0m17.93s | 1207216 ko | Bedrock/Field/Synthesis/New/Signature.vo                          |   0m17.32s | 1210248 ko ||    +0m00.60s ||     -3032 ko |     +3.52% |         -0.25%
   0m16.37s | 1144804 ko | Bedrock/Field/Translation/Proofs/Cmd.vo                           |   0m17.11s | 1146536 ko ||    -0m00.73s ||     -1732 ko |     -4.32% |         -0.15%
   0m16.36s | 2063348 ko | ExtractionHaskell/with_bedrock2_solinas_reduction.hs              |   0m16.35s | 2096996 ko ||    +0m00.00s ||    -33648 ko |     +0.06% |         -1.60%
   0m16.26s | 2063264 ko | ExtractionHaskell/bedrock2_solinas_reduction.hs                   |   0m16.52s | 2095492 ko ||    -0m00.25s ||    -32228 ko |     -1.57% |         -1.53%
   0m16.16s | 2023412 ko | ExtractionHaskell/with_bedrock2_word_by_word_montgomery.hs        |   0m16.00s | 2007884 ko ||    +0m00.16s ||     15528 ko |     +1.00% |         +0.77%
   0m16.12s | 2021956 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs             |   0m16.13s | 2010240 ko ||    -0m00.00s ||     11716 ko |     -0.06% |         +0.58%
   0m16.08s | 2028764 ko | ExtractionHaskell/solinas_reduction.hs                            |   0m15.49s | 1949544 ko ||    +0m00.58s ||     79220 ko |     +3.80% |         +4.06%
   0m15.71s | 1962892 ko | ExtractionHaskell/word_by_word_montgomery.hs                      |   0m15.47s | 1985472 ko ||    +0m00.24s ||    -22580 ko |     +1.55% |         -1.13%
   0m15.59s | 2009872 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs                 |   0m15.14s | 1950900 ko ||    +0m00.44s ||     58972 ko |     +2.97% |         +3.02%
   0m15.21s | 2008904 ko | ExtractionHaskell/with_bedrock2_unsaturated_solinas.hs            |   0m15.24s | 1949824 ko ||    -0m00.02s ||     59080 ko |     -0.19% |         +3.03%
   0m14.63s | 1934444 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs                   |   0m14.22s | 1862544 ko ||    +0m00.41s ||     71900 ko |     +2.88% |         +3.86%
   0m14.47s | 1879068 ko | ExtractionHaskell/bedrock2_dettman_multiplication.hs              |   0m14.36s | 1889216 ko ||    +0m00.11s ||    -10148 ko |     +0.76% |         -0.53%
   0m14.38s | 1879364 ko | ExtractionHaskell/with_bedrock2_dettman_multiplication.hs         |   0m14.28s | 1886884 ko ||    +0m00.10s ||     -7520 ko |     +0.70% |         -0.39%
   0m14.37s | 1927472 ko | ExtractionHaskell/unsaturated_solinas.hs                          |   0m14.53s | 1928704 ko ||    -0m00.16s ||     -1232 ko |     -1.10% |         -0.06%
   0m14.32s | 1917200 ko | ExtractionHaskell/with_bedrock2_base_conversion.hs                |   0m14.11s | 1932764 ko ||    +0m00.21s ||    -15564 ko |     +1.48% |         -0.80%
   0m14.30s | 1935052 ko | ExtractionHaskell/with_bedrock2_saturated_solinas.hs              |   0m14.12s | 1861568 ko ||    +0m00.18s ||     73484 ko |     +1.27% |         +3.94%
   0m14.20s | 1917124 ko | ExtractionHaskell/bedrock2_base_conversion.hs                     |   0m14.22s | 1911084 ko ||    -0m00.02s ||      6040 ko |     -0.14% |         +0.31%
   0m14.06s | 1864296 ko | ExtractionHaskell/dettman_multiplication.hs                       |   0m13.20s | 1856724 ko ||    +0m00.86s ||      7572 ko |     +6.51% |         +0.40%
   0m13.78s | 1840872 ko | ExtractionHaskell/saturated_solinas.hs                            |   0m13.71s | 1846748 ko ||    +0m00.06s ||     -5876 ko |     +0.51% |         -0.31%
   0m13.68s |  602488 ko | Bedrock/Field/Common/Util.vo                                      |   0m13.68s |  602420 ko ||    +0m00.00s ||        68 ko |     +0.00% |         +0.01%
   0m13.36s |  663048 ko | Bedrock/Group/AdditionChains.vo                                   |   0m13.42s |  662928 ko ||    -0m00.06s ||       120 ko |     -0.44% |         +0.01%
   0m13.12s |  667092 ko | Bedrock/Group/ScalarMult/LadderStep.vo                            |   0m13.04s |  667048 ko ||    +0m00.08s ||        44 ko |     +0.61% |         +0.00%
   0m13.11s | 1845960 ko | ExtractionHaskell/base_conversion.hs                              |   0m13.55s | 1851580 ko ||    -0m00.44s ||     -5620 ko |     -3.24% |         -0.30%
   0m11.84s | 1029560 ko | BoundsPipeline.vo                                                 |   0m11.88s | 1028872 ko ||    -0m00.04s ||       688 ko |     -0.33% |         +0.06%
   0m11.31s | 1699940 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo               |   0m11.11s | 1698268 ko ||    +0m00.20s ||      1672 ko |     +1.80% |         +0.09%
   0m10.27s | 1297740 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo              |   0m10.36s | 1296660 ko ||    -0m00.08s ||      1080 ko |     -0.86% |         +0.08%
   0m09.88s |  600056 ko | Stringification/IR.vo                                             |   0m09.90s |  601448 ko ||    -0m00.01s ||     -1392 ko |     -0.20% |         -0.23%
   0m09.74s |  624024 ko | Bedrock/Field/Translation/Proofs/Flatten.vo                       |   0m09.73s |  624068 ko ||    +0m00.00s ||       -44 ko |     +0.10% |         -0.00%
   0m09.34s | 1032068 ko | PushButtonSynthesis/BaseConversion.vo                             |   0m09.37s | 1035460 ko ||    -0m00.02s ||     -3392 ko |     -0.32% |         -0.32%
   0m09.19s |  661364 ko | Bedrock/Group/ScalarMult/CSwap.vo                                 |   0m08.96s |  661296 ko ||    +0m00.22s ||        68 ko |     +2.56% |         +0.01%
   0m08.41s | 1044384 ko | PushButtonSynthesis/Primitives.vo                                 |   0m08.56s | 1045468 ko ||    -0m00.15s ||     -1084 ko |     -1.75% |         -0.10%
   0m08.33s | 1000952 ko | PushButtonSynthesis/SmallExamples.vo                              |   0m08.13s | 1001028 ko ||    +0m00.19s ||       -76 ko |     +2.46% |         -0.00%
   0m07.39s |  911356 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo         |   0m07.43s |  912204 ko ||    -0m00.04s ||      -848 ko |     -0.53% |         -0.09%
   0m07.17s | 1033520 ko | PushButtonSynthesis/SolinasReduction.vo                           |   0m07.24s | 1033476 ko ||    -0m00.07s ||        44 ko |     -0.96% |         +0.00%
   0m06.67s |   51208 ko | fiat-go/64/p521/p521.go                                           |   0m06.32s |   49224 ko ||    +0m00.34s ||      1984 ko |     +5.53% |         +4.03%
   0m06.40s | 1040660 ko | PushButtonSynthesis/BarrettReduction.vo                           |   0m06.42s | 1041508 ko ||    -0m00.01s ||      -848 ko |     -0.31% |         -0.08%
   0m06.27s | 1121320 ko | CLI.vo                                                            |   0m06.40s | 1121288 ko ||    -0m00.13s ||        32 ko |     -2.03% |         +0.00%
   0m05.98s | 1130956 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo                 |   0m06.11s | 1130988 ko ||    -0m00.12s ||       -32 ko |     -2.12% |         -0.00%
   0m05.92s |   68612 ko | fiat-bedrock2/src/p521_64.c                                       |   0m04.98s |   66368 ko ||    +0m00.93s ||      2244 ko |    +18.87% |         +3.38%
   0m05.90s |   37028 ko | fiat-rust/src/p521_64.rs                                          |   0m05.46s |   36076 ko ||    +0m00.44s ||       952 ko |     +8.05% |         +2.63%
   0m05.87s |   37052 ko | fiat-c/src/p521_64.c                                              |   0m05.41s |   36076 ko ||    +0m00.46s ||       976 ko |     +8.50% |         +2.70%
   0m05.84s |  906864 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo                  |   0m05.81s |  906744 ko ||    +0m00.03s ||       120 ko |     +0.51% |         +0.01%
   0m05.25s |  616380 ko | Bedrock/End2End/RupicolaCrypto/Broadcast.vo                       |   0m05.24s |  616216 ko ||    +0m00.00s ||       164 ko |     +0.19% |         +0.02%
   0m04.73s | 1030392 ko | PushButtonSynthesis/DettmanMultiplication.vo                      |   0m04.78s | 1030456 ko ||    -0m00.04s ||       -64 ko |     -1.04% |         -0.00%
   0m04.41s | 1065452 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo           |   0m04.56s | 1065272 ko ||    -0m00.14s ||       180 ko |     -3.28% |         +0.01%
   0m04.39s | 1038800 ko | PushButtonSynthesis/SaturatedSolinas.vo                           |   0m04.43s | 1038816 ko ||    -0m00.04s ||       -16 ko |     -0.90% |         -0.00%
   0m03.94s |  957224 ko | Assembly/Equivalence.vo                                           |   0m03.88s |  955376 ko ||    +0m00.06s ||      1848 ko |     +1.54% |         +0.19%
   0m03.84s | 1051032 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo                   |   0m03.94s | 1051128 ko ||    -0m00.10s ||       -96 ko |     -2.53% |         -0.00%
   0m03.66s |  666368 ko | Bedrock/Group/ScalarMult/ScalarMult.vo                            |   0m03.97s |  667152 ko ||    -0m00.31s ||      -784 ko |     -7.80% |         -0.11%
   0m03.12s | 1072356 ko | Rewriter/PerfTesting/Core.vo                                      |   0m03.09s | 1072420 ko ||    +0m00.03s ||       -64 ko |     +0.97% |         -0.00%
   0m03.06s |  617024 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo                         |   0m03.02s |  613720 ko ||    +0m00.04s ||      3304 ko |     +1.32% |         +0.53%
   0m03.05s | 1006464 ko | Bedrock/Field/Translation/Cmd.vo                                  |   0m03.08s | 1009700 ko ||    -0m00.03s ||     -3236 ko |     -0.97% |         -0.32%
   0m02.98s |   50852 ko | fiat-go/64/p448solinas/p448solinas.go                             |   0m02.67s |   50500 ko ||    +0m00.31s ||       352 ko |    +11.61% |         +0.69%
   0m02.88s | 1068264 ko | Bedrock/Field/Stringification/Stringification.vo                  |   0m02.87s | 1068932 ko ||    +0m00.00s ||      -668 ko |     +0.34% |         -0.06%
   0m02.84s | 1061220 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo          |   0m02.73s | 1059288 ko ||    +0m00.10s ||      1932 ko |     +4.02% |         +0.18%
   0m02.80s | 1004228 ko | Bedrock/Field/Translation/Func.vo                                 |   0m02.79s | 1004848 ko ||    +0m00.00s ||      -620 ko |     +0.35% |         -0.06%
   0m02.80s | 1103608 ko | StandaloneHaskellMain.vo                                          |   0m02.72s | 1103504 ko ||    +0m00.07s ||       104 ko |     +2.94% |         +0.00%
   0m02.78s | 1145260 ko | Bedrock/Standalone/StandaloneHaskellMain.vo                       |   0m02.77s | 1145216 ko ||    +0m00.00s ||        44 ko |     +0.36% |         +0.00%
   0m02.76s | 1145200 ko | Bedrock/Standalone/StandaloneOCamlMain.vo                         |   0m02.72s | 1145392 ko ||    +0m00.03s ||      -192 ko |     +1.47% |         -0.01%
   0m02.76s | 1131284 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo                       |   0m02.73s | 1131224 ko ||    +0m00.02s ||        60 ko |     +1.09% |         +0.00%
   0m02.66s | 1103772 ko | StandaloneOCamlMain.vo                                            |   0m02.68s | 1103860 ko ||    -0m00.02s ||       -88 ko |     -0.74% |         -0.00%
   0m02.60s |  620876 ko | Bedrock/Field/Interface/Compilation2.vo                           |   0m02.60s |  621772 ko ||    +0m00.00s ||      -896 ko |     +0.00% |         -0.14%
   0m02.54s | 1064964 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo                         |   0m02.59s | 1065008 ko ||    -0m00.04s ||       -44 ko |     -1.93% |         -0.00%
   0m02.53s |   65044 ko | fiat-bedrock2/src/p448_solinas_64.c                               |   0m02.07s |   66308 ko ||    +0m00.46s ||     -1264 ko |    +22.22% |         -1.90%
   0m02.52s |   35764 ko | fiat-zig/src/p448_solinas_64.zig                                  |   0m01.90s |   35084 ko ||    +0m00.62s ||       680 ko |    +32.63% |         +1.93%
   0m02.51s |   37100 ko | fiat-go/32/curve25519/curve25519.go                               |   0m02.15s |   35348 ko ||    +0m00.35s ||      1752 ko |    +16.74% |         +4.95%
   0m02.51s |   36324 ko | fiat-rust/src/p448_solinas_64.rs                                  |   0m01.97s |   34328 ko ||    +0m00.53s ||      1996 ko |    +27.41% |         +5.81%
   0m02.50s | 1044712 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo                |   0m02.53s | 1045368 ko ||    -0m00.02s ||      -656 ko |     -1.18% |         -0.06%
   0m02.48s | 1041488 ko | Bedrock/Field/Translation/Parameters/Defaults.vo                  |   0m02.40s | 1040684 ko ||    +0m00.08s ||       804 ko |     +3.33% |         +0.07%
   0m02.48s | 1045392 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo                |   0m02.56s | 1044600 ko ||    -0m00.08s ||       792 ko |     -3.12% |         +0.07%
   0m02.47s |   51164 ko | fiat-json/src/p448_solinas_64.json                                |   0m02.06s |   51416 ko ||    +0m00.41s ||      -252 ko |    +19.90% |         -0.49%
   0m02.45s |   36696 ko | fiat-c/src/p448_solinas_64.c                                      |   0m01.98s |   35380 ko ||    +0m00.47s ||      1316 ko |    +23.73% |         +3.71%
   0m02.44s | 1045352 ko | Bedrock/Field/Translation/Parameters/FE310.vo                     |   0m02.50s | 1045320 ko ||    -0m00.06s ||        32 ko |     -2.40% |         +0.00%
   0m02.24s |   63200 ko | fiat-bedrock2/src/curve25519_32.c                                 |   0m01.98s |   63640 ko ||    +0m00.26s ||      -440 ko |    +13.13% |         -0.69%
   0m02.18s |   35508 ko | fiat-java/src/FiatCurve25519.java                                 |   0m01.82s |   36520 ko ||    +0m00.36s ||     -1012 ko |    +19.78% |         -2.77%
   0m02.16s |   50436 ko | fiat-json/src/curve25519_32.json                                  |   0m01.89s |   49708 ko ||    +0m00.27s ||       728 ko |    +14.28% |         +1.46%
   0m02.15s |   34348 ko | fiat-zig/src/curve25519_32.zig                                    |   0m01.82s |   33388 ko ||    +0m00.32s ||       960 ko |    +18.13% |         +2.87%
   0m02.12s |   34960 ko | fiat-rust/src/curve25519_32.rs                                    |   0m01.79s |   34088 ko ||    +0m00.33s ||       872 ko |    +18.43% |         +2.55%
   0m02.10s |   35016 ko | fiat-c/src/curve25519_32.c                                        |   0m01.76s |   33112 ko ||    +0m00.34s ||      1904 ko |    +19.31% |         +5.75%
   0m01.96s |  616180 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo                    |   0m02.00s |  614096 ko ||    -0m00.04s ||      2084 ko |     -2.00% |         +0.33%
   0m01.78s |  636112 ko | Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo                 |   0m01.82s |  636072 ko ||    -0m00.04s ||        40 ko |     -2.19% |         +0.00%
   0m01.62s |   52504 ko | fiat-bedrock2/src/secp256k1_dettman_32.c                          |   0m01.46s |   51924 ko ||    +0m00.16s ||       580 ko |    +10.95% |         +1.11%
   0m01.61s |  607916 ko | Bedrock/Field/Common/Names/MakeNames.vo                           |   0m01.62s |  607756 ko ||    -0m00.01s ||       160 ko |     -0.61% |         +0.02%
   0m01.53s |  590192 ko | CompilersTestCases.vo                                             |   0m01.48s |  590236 ko ||    +0m00.05s ||       -44 ko |     +3.37% |         -0.00%
   0m01.50s |  512068 ko | AbstractInterpretation/AbstractInterpretation.vo                  |   0m01.39s |  512000 ko ||    +0m00.11s ||        68 ko |     +7.91% |         +0.01%
   0m01.46s |   26680 ko | fiat-java/src/FiatSecp256K1Dettman.java                           |   0m01.24s |   26336 ko ||    +0m00.21s ||       344 ko |    +17.74% |         +1.30%
   0m01.46s |   42060 ko | fiat-json/src/secp256k1_dettman_32.json                           |   0m01.24s |   41136 ko ||    +0m00.21s ||       924 ko |    +17.74% |         +2.24%
   0m01.44s |   26260 ko | fiat-c/src/secp256k1_dettman_32.c                                 |   0m01.21s |   25744 ko ||    +0m00.23s ||       516 ko |    +19.00% |         +2.00%
   0m01.44s |   27956 ko | fiat-go/32/secp256k1dettman/secp256k1dettman.go                   |   0m01.21s |   25860 ko ||    +0m00.23s ||      2096 ko |    +19.00% |         +8.10%
   0m01.44s |   27096 ko | fiat-rust/src/secp256k1_dettman_32.rs                             |   0m01.22s |   25440 ko ||    +0m00.21s ||      1656 ko |    +18.03% |         +6.50%
   0m01.42s |   27060 ko | fiat-zig/src/secp256k1_dettman_32.zig                             |   0m01.23s |   25656 ko ||    +0m00.18s ||      1404 ko |    +15.44% |         +5.47%
   0m01.35s |  543324 ko | Stringification/Go.vo                                             |   0m01.35s |  541960 ko ||    +0m00.00s ||      1364 ko |     +0.00% |         +0.25%
   0m01.11s |  628136 ko | Bedrock/Specs/Field.vo                                            |   0m01.18s |  628700 ko ||    -0m00.06s ||      -564 ko |     -5.93% |         -0.08%
   0m01.07s |  609304 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo                          |   0m01.03s |  607272 ko ||    +0m00.04s ||      2032 ko |     +3.88% |         +0.33%
   0m01.06s |  601084 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo                         |   0m01.00s |  602440 ko ||    +0m00.06s ||     -1356 ko |     +6.00% |         -0.22%
   0m00.94s |  538600 ko | Stringification/C.vo                                              |   0m00.91s |  538560 ko ||    +0m00.02s ||        40 ko |     +3.29% |         +0.00%
   0m00.91s |  535844 ko | Stringification/JSON.vo                                           |   0m00.94s |  537144 ko ||    -0m00.02s ||     -1300 ko |     -3.19% |         -0.24%
   0m00.88s |  535936 ko | Stringification/Zig.vo                                            |   0m00.88s |  539224 ko ||    +0m00.00s ||     -3288 ko |     +0.00% |         -0.60%
   0m00.87s |  618888 ko | Bedrock/Group/Point.vo                                            |   0m00.89s |  617632 ko ||    -0m00.02s ||      1256 ko |     -2.24% |         +0.20%
   0m00.86s |  615616 ko | Bedrock/Field/Interface/Representation.vo                         |   0m00.84s |  615736 ko ||    +0m00.02s ||      -120 ko |     +2.38% |         -0.01%
   0m00.86s |  534896 ko | Stringification/Java.vo                                           |   0m00.84s |  538936 ko ||    +0m00.02s ||     -4040 ko |     +2.38% |         -0.74%
   0m00.80s |  535916 ko | Stringification/Rust.vo                                           |   0m00.83s |  535824 ko ||    -0m00.02s ||        92 ko |     -3.61% |         +0.01%
   0m00.79s |  587772 ko | Bedrock/Field/Common/Tactics.vo                                   |   0m00.78s |  587592 ko ||    +0m00.01s ||       180 ko |     +1.28% |         +0.03%
   0m00.72s |  521776 ko | Bedrock/Field/Common/Arrays/MakeListLengths.vo                    |   0m00.68s |  523076 ko ||    +0m00.03s ||     -1300 ko |     +5.88% |         -0.24%
   0m00.72s |  546832 ko | Bedrock/Field/Stringification/FlattenVarData.vo                   |   0m00.72s |  546004 ko ||    +0m00.00s ||       828 ko |     +0.00% |         +0.15%
   0m00.70s |   32124 ko | fiat-go/64/curve25519/curve25519.go                               |   0m00.63s |   32976 ko ||    +0m00.06s ||      -852 ko |    +11.11% |         -2.58%
   0m00.68s |  515488 ko | AbstractInterpretation/WfExtra.vo                                 |   0m00.63s |  515492 ko ||    +0m00.05s ||        -4 ko |     +7.93% |         -0.00%
   0m00.68s |   38372 ko | fiat-json/src/curve25519_solinas_64.json                          |   0m00.41s |   39308 ko ||    +0m00.27s ||      -936 ko |    +65.85% |         -2.38%
   0m00.67s |   38908 ko | fiat-c/src/curve25519_solinas_64.c                                |   0m00.41s |   36728 ko ||    +0m00.26s ||      2180 ko |    +63.41% |         +5.93%
   0m00.66s |   37132 ko | fiat-rust/src/curve25519_solinas_64.rs                            |   0m00.39s |   36260 ko ||    +0m00.27s ||       872 ko |    +69.23% |         +2.40%
   0m00.66s |   36892 ko | fiat-zig/src/curve25519_solinas_64.zig                            |   0m00.42s |   36336 ko ||    +0m00.24s ||       556 ko |    +57.14% |         +1.53%
   0m00.60s |   34160 ko | fiat-json/src/curve25519_64.json                                  |   0m00.52s |   32588 ko ||    +0m00.07s ||      1572 ko |    +15.38% |         +4.82%
   0m00.59s |   38236 ko | fiat-go/64/curve25519solinas/curve25519solinas.go                 |   0m00.43s |   36420 ko ||    +0m00.15s ||      1816 ko |    +37.20% |         +4.98%
   0m00.58s |   38448 ko | fiat-bedrock2/src/curve25519_64.c                                 |   0m00.51s |   38216 ko ||    +0m00.06s ||       232 ko |    +13.72% |         +0.60%
   0m00.58s |   42568 ko | fiat-bedrock2/src/curve25519_solinas_64.c                         |   0m00.42s |   40596 ko ||    +0m00.15s ||      1972 ko |    +38.09% |         +4.85%
   0m00.56s |   26892 ko | fiat-c/src/curve25519_64.c                                        |   0m00.45s |   27132 ko ||    +0m00.11s ||      -240 ko |    +24.44% |         -0.88%
   0m00.56s |   26560 ko | fiat-rust/src/curve25519_64.rs                                    |   0m00.46s |   26040 ko ||    +0m00.10s ||       520 ko |    +21.73% |         +1.99%
   0m00.56s |   27152 ko | fiat-zig/src/curve25519_64.zig                                    |   0m00.48s |   26252 ko ||    +0m00.08s ||       900 ko |    +16.66% |         +3.42%
   0m00.54s |  120576 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi                 |   0m00.50s |  119948 ko ||    +0m00.04s ||       628 ko |     +8.00% |         +0.52%
   0m00.53s |  120076 ko | ExtractionOCaml/unsaturated_solinas.cmi                           |   0m00.50s |  119836 ko ||    +0m00.03s ||       240 ko |     +6.00% |         +0.20%
   0m00.52s |  124368 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi              |   0m00.52s |  123300 ko ||    +0m00.00s ||      1068 ko |     +0.00% |         +0.86%
   0m00.52s |  118308 ko | ExtractionOCaml/solinas_reduction.cmi                             |   0m00.51s |  118636 ko ||    +0m00.01s ||      -328 ko |     +1.96% |         -0.27%
   0m00.52s |  121724 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi          |   0m00.50s |  121156 ko ||    +0m00.02s ||       568 ko |     +4.00% |         +0.46%
   0m00.52s |  123672 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi               |   0m00.51s |  120980 ko ||    +0m00.01s ||      2692 ko |     +1.96% |         +2.22%
   0m00.52s |  123072 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi               |   0m00.50s |  122784 ko ||    +0m00.02s ||       288 ko |     +4.00% |         +0.23%
   0m00.52s |  123132 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi             |   0m00.50s |  123700 ko ||    +0m00.02s ||      -568 ko |     +4.00% |         -0.45%
   0m00.51s |  120332 ko | ExtractionOCaml/bedrock2_base_conversion.cmi                      |   0m00.51s |  119972 ko ||    +0m00.00s ||       360 ko |     +0.00% |         +0.30%
   0m00.51s |  120184 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi                  |   0m00.53s |  123596 ko ||    -0m00.02s ||     -3412 ko |     -3.77% |         -2.76%
   0m00.51s |  118088 ko | ExtractionOCaml/saturated_solinas.cmi                             |   0m00.48s |  117928 ko ||    +0m00.03s ||       160 ko |     +6.25% |         +0.13%
   0m00.51s |  124416 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi         |   0m00.51s |  123124 ko ||    +0m00.00s ||      1292 ko |     +0.00% |         +1.04%
   0m00.50s |  120256 ko | ExtractionOCaml/base_conversion.cmi                               |   0m00.51s |  118684 ko ||    -0m00.01s ||      1572 ko |     -1.96% |         +1.32%
   0m00.50s |  123568 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi                    |   0m00.54s |  122468 ko ||    -0m00.04s ||      1100 ko |     -7.40% |         +0.89%
   0m00.50s |  123660 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi                    |   0m00.50s |  120332 ko ||    +0m00.00s ||      3328 ko |     +0.00% |         +2.76%
   0m00.50s |  119964 ko | ExtractionOCaml/dettman_multiplication.cmi                        |   0m00.51s |  120092 ko ||    -0m00.01s ||      -128 ko |     -1.96% |         -0.10%
   0m00.50s |  120424 ko | ExtractionOCaml/word_by_word_montgomery.cmi                       |   0m00.49s |  119588 ko ||    +0m00.01s ||       836 ko |     +2.04% |         +0.69%
   0m00.49s |  120784 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi               |   0m00.53s |  120180 ko ||    -0m00.04s ||       604 ko |     -7.54% |         +0.50%
   0m00.34s |   25480 ko | fiat-go/32/poly1305/poly1305.go                                   |   0m00.30s |   24960 ko ||    +0m00.04s ||       520 ko |    +13.33% |         +2.08%
   0m00.31s |   25196 ko | fiat-go/64/secp256k1dettman/secp256k1dettman.go                   |   0m00.25s |   24476 ko ||    +0m00.06s ||       720 ko |    +24.00% |         +2.94%
   0m00.30s |   33676 ko | fiat-bedrock2/src/poly1305_32.c                                   |   0m00.25s |   32372 ko ||    +0m00.04s ||      1304 ko |    +19.99% |         +4.02%
   0m00.30s |   29656 ko | fiat-json/src/poly1305_32.json                                    |   0m00.25s |   30252 ko ||    +0m00.04s ||      -596 ko |    +19.99% |         -1.97%
   0m00.29s |   29300 ko | fiat-bedrock2/src/secp256k1_dettman_64.c                          |   0m00.22s |   29724 ko ||    +0m00.06s ||      -424 ko |    +31.81% |         -1.42%
   0m00.28s |   23932 ko | fiat-json/src/secp256k1_dettman_64.json                           |   0m00.20s |   23928 ko ||    +0m00.08s ||         4 ko |    +40.00% |         +0.01%
   0m00.27s |   25000 ko | fiat-c/src/poly1305_32.c                                          |   0m00.21s |   24124 ko ||    +0m00.06s ||       876 ko |    +28.57% |         +3.63%
   0m00.27s |   21060 ko | fiat-c/src/secp256k1_dettman_64.c                                 |   0m00.18s |   20924 ko ||    +0m00.09s ||       136 ko |    +50.00% |         +0.64%
   0m00.27s |   25404 ko | fiat-java/src/FiatPoly1305.java                                   |   0m00.22s |   25272 ko ||    +0m00.05s ||       132 ko |    +22.72% |         +0.52%
   0m00.27s |   20960 ko | fiat-rust/src/secp256k1_dettman_64.rs                             |   0m00.18s |   21372 ko ||    +0m00.09s ||      -412 ko |    +50.00% |         -1.92%
   0m00.27s |   24624 ko | fiat-zig/src/poly1305_32.zig                                      |   0m00.21s |   23860 ko ||    +0m00.06s ||       764 ko |    +28.57% |         +3.20%
   0m00.27s |   21176 ko | fiat-zig/src/secp256k1_dettman_64.zig                             |   0m00.18s |   20508 ko ||    +0m00.09s ||       668 ko |    +50.00% |         +3.25%
   0m00.26s |   24636 ko | fiat-rust/src/poly1305_32.rs                                      |   0m00.21s |   24504 ko ||    +0m00.05s ||       132 ko |    +23.80% |         +0.53%
   0m00.18s |   26440 ko | fiat-go/64/poly1305/poly1305.go                                   |   0m00.18s |   26096 ko ||    +0m00.00s ||       344 ko |     +0.00% |         +1.31%
   0m00.17s |   26980 ko | fiat-json/src/poly1305_64.json                                    |   0m00.13s |   27492 ko ||    +0m00.04s ||      -512 ko |    +30.76% |         -1.86%
   0m00.16s |   61504 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi                      |   0m00.16s |   61784 ko ||    +0m00.00s ||      -280 ko |     +0.00% |         -0.45%
   0m00.16s |   23780 ko | fiat-rust/src/poly1305_64.rs                                      |   0m00.13s |   22996 ko ||    +0m00.03s ||       784 ko |    +23.07% |         +3.40%
   0m00.16s |   23284 ko | fiat-zig/src/poly1305_64.zig                                      |   0m00.13s |   23176 ko ||    +0m00.03s ||       108 ko |    +23.07% |         +0.46%
   0m00.15s |   58712 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi                  |   0m00.15s |   58904 ko ||    +0m00.00s ||      -192 ko |     +0.00% |…

src/AbstractInterpretation/AbstractInterpretation.v

@@ -0,0 +1,62 @@
+Require Import Crypto.Util.ZRange.
+Require Import Rewriter.Language.Language.
+Require Import Crypto.Language.API.
+Require Import Crypto.AbstractInterpretation.ZRange.
+Require Crypto.AbstractInterpretation.Fancy.AbstractInterpretation.
+Require Crypto.AbstractInterpretation.Bottomify.AbstractInterpretation.
+
+Module Compilers.
+  Export Language.Compilers.
+  Export UnderLets.Compilers.
+  Export Language.API.Compilers.
+  Export AbstractInterpretation.ZRange.Compilers.
+  Export Fancy.AbstractInterpretation.Compilers.
+  Export Bottomify.AbstractInterpretation.Compilers.
+
+  Module partial.
+    Definition Extract {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow _ t)
+    := if fancy_and_powerful_but_exponentially_slow_bounds_analysis
+       then     Fancy.AbstractInterpretation.Compilers.partial.Extract assume_cast_truncates e bound
+       else Bottomify.AbstractInterpretation.Compilers.partial.Extract assume_cast_truncates e bound.
+  End partial.
+
+  Import API.
+  Definition PartialEvaluateWithBounds
+    {fancy_and_powerful_but_exponentially_slow_bounds_analysis : fancy_and_powerful_but_exponentially_slow_bounds_analysis_opt}
+    {shiftr_avoid_uint1 : shiftr_avoid_uint1_opt}
+    (relax_zrange : zrange -> option zrange)
+    (assume_cast_truncates : bool)
+    (skip_annotations_under : forall t, ident t -> bool)
+    (strip_preexisting_annotations : bool)
+    {t} (e : Expr t)
+    (bound : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
+    : Expr t
+    := if fancy_and_powerful_but_exponentially_slow_bounds_analysis
+       then     Fancy.AbstractInterpretation.Compilers.PartialEvaluateWithBounds relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e bound
+       else Bottomify.AbstractInterpretation.Compilers.PartialEvaluateWithBounds relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e bound.
+
+  Definition PartialEvaluateWithListInfoFromBounds
+    {fancy_and_powerful_but_exponentially_slow_bounds_analysis : fancy_and_powerful_but_exponentially_slow_bounds_analysis_opt}
+    {shiftr_avoid_uint1 : shiftr_avoid_uint1_opt}
+    {t} (e : Expr t)
+    (bound : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
+    : Expr t
+    := if fancy_and_powerful_but_exponentially_slow_bounds_analysis
+       then     Fancy.AbstractInterpretation.Compilers.PartialEvaluateWithListInfoFromBounds e bound
+       else Bottomify.AbstractInterpretation.Compilers.PartialEvaluateWithListInfoFromBounds e bound.
+
+  Definition CheckedPartialEvaluateWithBounds
+    {fancy_and_powerful_but_exponentially_slow_bounds_analysis : fancy_and_powerful_but_exponentially_slow_bounds_analysis_opt}
+    {shiftr_avoid_uint1 : shiftr_avoid_uint1_opt}
+    (relax_zrange : zrange -> option zrange)
+    (assume_cast_truncates : bool)
+    (skip_annotations_under : forall t, ident t -> bool)
+    (strip_preexisting_annotations : bool)
+    {t} (E : Expr t)
+    (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
+    (b_out : ZRange.type.base.option.interp (type.final_codomain t))
+    : Expr t + (ZRange.type.base.option.interp (type.final_codomain t) * Expr t + list { t : _ & forall var, @expr var t })
+    := if fancy_and_powerful_but_exponentially_slow_bounds_analysis
+       then     Fancy.AbstractInterpretation.Compilers.CheckedPartialEvaluateWithBounds relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations E b_in b_out
+       else Bottomify.AbstractInterpretation.Compilers.CheckedPartialEvaluateWithBounds relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations E b_in b_out.
+End Compilers.

src/AbstractInterpretation/Bottomify/AbstractInterpretation.v

@@ -493,6 +493,7 @@ Module Compilers.
         Definition eta_expand_with_bound {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t
           := let assume_cast_truncates := false in
              let shiftr_avoid_uint1 : shiftr_avoid_uint1_opt := false (* this doesn't actually matter for [eta_expand_with_bound], which only invokes [abstract_interp_ident] on things like [fst], [snd], etc *) in
+             let fancy_and_powerful_but_exponentially_slow_bounds_analysis : fancy_and_powerful_but_exponentially_slow_bounds_analysis_opt := false in
              (@partial.ident.eta_expand_with_bound)
                var abstract_domain' annotate_expr bottom' (abstract_interp_ident assume_cast_truncates) extract_list_state extract_option_state is_annotated_for t e bound.
 
@@ -551,7 +552,7 @@ Module Compilers.
   End CheckCasts.
 
   Definition PartialEvaluateWithBounds
-             {shiftr_avoid_uint1 : shiftr_avoid_uint1_opt}
+             {opts : AbstractInterpretation.Options}
              (relax_zrange : zrange -> option zrange)
              (assume_cast_truncates : bool)
              (skip_annotations_under : forall t, ident t -> bool)
@@ -561,14 +562,14 @@ Module Compilers.
     : Expr t
     := partial.EvalWithBound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations (GeneralizeVar.GeneralizeVar (e _)) bound.
   Definition PartialEvaluateWithListInfoFromBounds
-             {shiftr_avoid_uint1 : shiftr_avoid_uint1_opt}
+             {opts : AbstractInterpretation.Options}
              {t} (e : Expr t)
              (bound : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
     : Expr t
     := partial.EtaExpandWithListInfoFromBound (GeneralizeVar.GeneralizeVar (e _)) bound.
 
   Definition CheckedPartialEvaluateWithBounds
-             {shiftr_avoid_uint1 : shiftr_avoid_uint1_opt}
+             {opts : AbstractInterpretation.Options}
              (relax_zrange : zrange -> option zrange)
              (assume_cast_truncates : bool)
              (skip_annotations_under : forall t, ident t -> bool)