Skip to content

Commit

Permalink
Remove a needless GeneralizeVar.GeneralizeVar
Browse files Browse the repository at this point in the history
Maybe this is responsible for the performance issue???

<details><summary>Timing Diff</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% |         -0.32%
   0m00.15s |   28228 ko | fiat-bedrock2/src/poly1305_64.c                                   |   0m00.11s |   28056 ko ||    +0m00.03s ||       172 ko |    +36.36% |         +0.61%
   0m00.15s |   23928 ko | fiat-c/src/poly1305_64.c                                          |   0m00.12s |   22980 ko ||    +0m00.03s ||       948 ko |    +25.00% |         +4.12%

```
</p>
</details>
  • Loading branch information
JasonGross committed Dec 6, 2023
1 parent cd9fe36 commit 72600ed
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 10 deletions.
2 changes: 1 addition & 1 deletion src/AbstractInterpretation/AbstractInterpretation.v
Original file line number Diff line number Diff line change
Expand Up @@ -577,7 +577,7 @@ Module Compilers.
{t} (e : Expr t)
(bound : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
: Expr t
:= partial.EvalWithBound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations (GeneralizeVar.GeneralizeVar (e _)) bound.
:= partial.EvalWithBound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e bound.
Definition PartialEvaluateWithListInfoFromBounds
{shiftr_avoid_uint1 : shiftr_avoid_uint1_opt}
{t} (e : Expr t)
Expand Down
10 changes: 1 addition & 9 deletions src/AbstractInterpretation/Proofs.v
Original file line number Diff line number Diff line change
Expand Up @@ -1507,7 +1507,6 @@ Module Compilers.
by (hnf; etransitivity; [ eassumption | symmetry; eassumption ]).
assert (arg2_Proper : Proper (type.and_for_each_lhs_of_arrow (@type.related base.type base.interp (fun _ => eq))) arg2)
by (hnf; etransitivity; [ symmetry; eassumption | eassumption ]).
rewrite <- (GeneralizeVar.Interp_gen1_GeneralizeVar E) by auto with wf.
eapply Interp_EvalWithBound; eauto with wf typeclass_instances.
Qed.

Expand All @@ -1530,14 +1529,7 @@ Module Compilers.
Proof.
cbv [PartialEvaluateWithBounds].
intros arg1 Harg11 Harg1.
rewrite <- Extract_GeneralizeVar; auto with wf typeclass_instances.
{ eapply @Interp_EvalWithBound; eauto with wf typeclass_instances. }
{ cbv [Proper] in *.
eapply type.and_for_each_lhs_of_arrow_Proper_impl_hetero1;
[ | eapply type.andb_bool_impl_and_for_each_lhs_of_arrow; [ | eassumption ] ];
[ | refine (fun t x y H => H) ];
cbv beta.
intros *; eapply ZRange.type.option.is_bounded_by_impl_eqv_refl. }
eapply @Interp_EvalWithBound; eauto with wf typeclass_instances.
Qed.

Lemma Interp_PartialEvaluateWithListInfoFromBounds
Expand Down

0 comments on commit 72600ed

Please sign in to comment.