Add some subrelation instances

[JasonGross]

Timing Diff

     After |   Peak Mem | File Name                                                       |     Before |   Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------
138m52.03s | 4072760 ko | Total Time / Peak Mem                                           | 139m15.93s | 4075576 ko || -0m23.90s ||     -2816 ko |   -0.28% |         -0.06%
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------
  7m23.75s | 1061508 ko | fiat-json/src/p384_32.json                                      |   8m10.06s | 1061472 ko || -0m46.31s ||        36 ko |   -9.44% |         +0.00%
  7m56.46s |  959900 ko | fiat-go/32/p384/p384.go                                         |   7m16.49s |  959976 ko || +0m39.96s ||       -76 ko |   +9.15% |         -0.00%
  7m47.27s | 1116112 ko | fiat-zig/src/p384_32.zig                                        |   7m56.60s | 1116192 ko || -0m09.33s ||       -80 ko |   -1.95% |         -0.00%
  7m03.40s | 1057720 ko | fiat-bedrock2/src/p384_32.c                                     |   7m06.96s | 1057648 ko || -0m03.56s ||        72 ko |   -0.83% |         +0.00%
  7m46.39s |  942188 ko | fiat-rust/src/p384_32.rs                                        |   7m44.21s |  942456 ko || +0m02.18s ||      -268 ko |   +0.46% |         -0.02%
  4m20.80s | 1363192 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo     |   4m23.33s | 1395412 ko || -0m02.52s ||    -32220 ko |   -0.96% |         -2.30%
  4m09.60s | 4072760 ko | Curves/EdwardsMontgomery.vo                                     |   4m07.18s | 4075576 ko || +0m02.41s ||     -2816 ko |   +0.97% |         -0.06%
  0m29.71s |  210444 ko | fiat-bedrock2/src/p256_32.c                                     |   0m32.20s |  210136 ko || -0m02.49s ||       308 ko |   -7.73% |         +0.14%
  0m29.07s |  234552 ko | fiat-json/src/secp256k1_32.json                                 |   0m31.23s |  234576 ko || -0m02.16s ||       -24 ko |   -6.91% |         -0.01%
  0m28.92s |  208332 ko | fiat-java/src/FiatSecp256K1.java                                |   0m31.06s |  208352 ko || -0m02.13s ||       -20 ko |   -6.88% |         -0.00%
  0m27.88s |  227384 ko | fiat-zig/src/p256_32.zig                                        |   0m30.74s |  227204 ko || -0m02.85s ||       180 ko |   -9.30% |         +0.07%
  0m27.81s |  195368 ko | fiat-go/32/p256/p256.go                                         |   0m30.04s |  195328 ko || -0m02.23s ||        40 ko |   -7.42% |         +0.02%
  0m23.83s |  144000 ko | fiat-zig/src/p434_64.zig                                        |   0m21.09s |  143836 ko || +0m02.73s ||       164 ko |  +12.99% |         +0.11%
  7m54.35s | 1081840 ko | fiat-c/src/p384_32.c                                            |   7m52.94s | 1082160 ko || +0m01.41s ||      -320 ko |   +0.29% |         -0.02%
  0m35.54s | 1452920 ko | ExtractionOCaml/bedrock2_saturated_solinas                      |   0m33.97s | 1452912 ko || +0m01.57s ||         8 ko |   +4.62% |         +0.00%
  0m29.01s |  954156 ko | PushButtonSynthesis/BYInversionReificationCache.vo              |   0m27.29s |  954532 ko || +0m01.72s ||      -376 ko |   +6.30% |         -0.03%
  0m25.72s | 1233352 ko | ExtractionOCaml/perf_unsaturated_solinas                        |   0m27.33s | 1233140 ko || -0m01.60s ||       212 ko |   -5.89% |         +0.01%
  0m21.56s | 1714120 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml                   |   0m20.54s | 1714084 ko || +0m01.01s ||        36 ko |   +4.96% |         +0.00%
  0m15.27s |  805632 ko | Bedrock/Field/Translation/Proofs/Cmd.vo                         |   0m16.57s |  805796 ko || -0m01.30s ||      -164 ko |   -7.84% |         -0.02%
  0m14.64s |  131216 ko | fiat-json/src/p224_32.json                                      |   0m13.38s |  131012 ko || +0m01.25s ||       204 ko |   +9.41% |         +0.15%
  7m50.59s | 1105652 ko | fiat-java/src/FiatP384.java                                     |   7m51.37s | 1105580 ko || -0m00.77s ||        72 ko |   -0.16% |         +0.00%
  6m53.70s | 2075284 ko | Curves/Weierstrass/AffineProofs.vo                              |   6m52.78s | 2085408 ko || +0m00.92s ||    -10124 ko |   +0.22% |         -0.48%
  5m36.80s | 2100572 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo                 |   5m36.61s | 2100564 ko || +0m00.18s ||         8 ko |   +0.05% |         +0.00%
  2m55.89s | 1447776 ko | Curves/Weierstrass/Projective.vo                                |   2m56.13s | 1448452 ko || -0m00.24s ||      -676 ko |   -0.13% |         -0.04%
  2m42.17s | 1444860 ko | Curves/Montgomery/XZProofs.vo                                   |   2m43.06s | 1446140 ko || -0m00.88s ||     -1280 ko |   -0.54% |         -0.08%
  2m37.11s | 1230880 ko | Curves/Montgomery/AffineProofs.vo                               |   2m37.80s | 1231036 ko || -0m00.68s ||      -156 ko |   -0.43% |         -0.01%
  1m55.88s | 2508148 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo                      |   1m55.81s | 2508244 ko || +0m00.06s ||       -96 ko |   +0.06% |         -0.00%
  1m43.04s | 1466548 ko | Fancy/Barrett256.vo                                             |   1m42.60s | 1465768 ko || +0m00.43s ||       780 ko |   +0.42% |         +0.05%
  1m40.78s | 1060100 ko | Bedrock/Field/Synthesis/Examples/X25519_64.vo                   |   1m41.01s | 1060228 ko || -0m00.22s ||      -128 ko |   -0.22% |         -0.01%
  1m36.13s | 1455828 ko | SlowPrimeSynthesisExamples.vo                                   |   1m36.03s | 1456116 ko || +0m00.09s ||      -288 ko |   +0.10% |         -0.01%
  1m19.69s | 1224556 ko | Bedrock/End2End/X25519/Field25519.vo                            |   1m19.82s | 1224596 ko || -0m00.12s ||       -40 ko |   -0.16% |         -0.00%
  1m17.12s | 1122996 ko | UnsaturatedSolinasHeuristics/Tests.vo                           |   1m17.66s | 1123088 ko || -0m00.53s ||       -92 ko |   -0.69% |         -0.00%
  1m02.71s |  949624 ko | Curves/Weierstrass/Jacobian.vo                                  |   1m02.74s |  944416 ko || -0m00.03s ||      5208 ko |   -0.04% |         +0.55%
  1m01.84s | 1363364 ko | Bedrock/Field/Synthesis/Examples/p224_64.vo                     |   1m02.10s | 1363168 ko || -0m00.25s ||       196 ko |   -0.41% |         +0.01%
  1m00.62s |  974740 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo       |   1m00.11s |  975384 ko || +0m00.50s ||      -644 ko |   +0.84% |         -0.06%
  0m59.14s | 1285812 ko | Bedrock/Field/Synthesis/Examples/p256_64.vo                     |   0m59.37s | 1285760 ko || -0m00.22s ||        52 ko |   -0.38% |         +0.00%
  0m54.71s | 2462140 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery                |   0m54.76s | 2462092 ko || -0m00.04s ||        48 ko |   -0.09% |         +0.00%
  0m49.54s | 2145264 ko | ExtractionOCaml/word_by_word_montgomery                         |   0m49.17s | 2145284 ko || +0m00.36s ||       -20 ko |   +0.75% |         -0.00%
  0m46.89s | 1078348 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo        |   0m47.16s | 1077960 ko || -0m00.26s ||       388 ko |   -0.57% |         +0.03%
  0m44.71s |  579944 ko | Demo.vo                                                         |   0m44.69s |  580072 ko || +0m00.02s ||      -128 ko |   +0.04% |         -0.02%
  0m43.11s | 1334340 ko | Fancy/Montgomery256.vo                                          |   0m43.18s | 1334364 ko || -0m00.07s ||       -24 ko |   -0.16% |         -0.00%
  0m40.00s | 1019384 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo                    |   0m40.05s | 1019192 ko || -0m00.04s ||       192 ko |   -0.12% |         +0.01%
  0m39.83s | 2410116 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml             |   0m40.05s | 2410112 ko || -0m00.21s ||         4 ko |   -0.54% |         +0.00%
  0m39.56s | 1862800 ko | ExtractionOCaml/bedrock2_unsaturated_solinas                    |   0m39.67s | 1863068 ko || -0m00.10s ||      -268 ko |   -0.27% |         -0.01%
  0m38.23s | 2306144 ko | ExtractionOCaml/word_by_word_montgomery.ml                      |   0m38.38s | 2306024 ko || -0m00.15s ||       120 ko |   -0.39% |         +0.00%
  0m36.46s | 1649212 ko | ExtractionOCaml/unsaturated_solinas                             |   0m35.48s | 1649220 ko || +0m00.98s ||        -8 ko |   +2.76% |         -0.00%
  0m34.61s | 1445504 ko | ExtractionOCaml/bedrock2_base_conversion                        |   0m35.14s | 1445584 ko || -0m00.53s ||       -80 ko |   -1.50% |         -0.00%
  0m33.43s |  216724 ko | fiat-bedrock2/src/secp256k1_32.c                                |   0m33.45s |  216548 ko || -0m00.02s ||       176 ko |   -0.05% |         +0.08%
  0m33.04s | 1285244 ko | ExtractionOCaml/base_conversion                                 |   0m32.58s | 1285136 ko || +0m00.46s ||       108 ko |   +1.41% |         +0.00%
  0m31.54s |  195176 ko | fiat-zig/src/secp256k1_32.zig                                   |   0m31.03s |  195168 ko || +0m00.50s ||         8 ko |   +1.64% |         +0.00%
  0m31.47s | 1270516 ko | ExtractionOCaml/saturated_solinas                               |   0m30.80s | 1270528 ko || +0m00.66s ||       -12 ko |   +2.17% |         -0.00%
  0m30.96s |  218700 ko | fiat-go/32/secp256k1/secp256k1.go                               |   0m31.34s |  218604 ko || -0m00.37s ||        96 ko |   -1.21% |         +0.04%
  0m30.90s |  200744 ko | fiat-rust/src/secp256k1_32.rs                                   |   0m30.75s |  201020 ko || +0m00.14s ||      -276 ko |   +0.48% |         -0.13%
  0m30.42s |  201304 ko | fiat-java/src/FiatP256.java                                     |   0m30.16s |  201284 ko || +0m00.26s ||        20 ko |   +0.86% |         +0.00%
  0m29.95s |  248040 ko | fiat-json/src/p256_32.json                                      |   0m29.99s |  247980 ko || -0m00.03s ||        60 ko |   -0.13% |         +0.02%
  0m29.81s |  224604 ko | fiat-rust/src/p256_32.rs                                        |   0m30.03s |  224556 ko || -0m00.22s ||        48 ko |   -0.73% |         +0.02%
  0m29.79s | 1233228 ko | ExtractionOCaml/perf_word_by_word_montgomery                    |   0m29.63s | 1233392 ko || +0m00.16s ||      -164 ko |   +0.53% |         -0.01%
  0m29.76s |  200696 ko | fiat-c/src/secp256k1_32.c                                       |   0m30.05s |  200852 ko || -0m00.28s ||      -156 ko |   -0.96% |         -0.07%
  0m29.33s | 1171608 ko | Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.vo           |   0m30.09s | 1172292 ko || -0m00.76s ||      -684 ko |   -2.52% |         -0.05%
  0m29.25s |  178860 ko | fiat-c/src/p256_32.c                                            |   0m29.61s |  178848 ko || -0m00.35s ||        12 ko |   -1.21% |         +0.00%
  0m28.23s | 1098080 ko | Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.vo         |   0m28.36s | 1096388 ko || -0m00.12s ||      1692 ko |   -0.45% |         +0.15%
  0m27.45s |  914820 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo         |   0m27.35s |  915260 ko || +0m00.09s ||      -440 ko |   +0.36% |         -0.04%
  0m26.60s |  844908 ko | PushButtonSynthesis/UnsaturatedSolinas.vo                       |   0m26.68s |  845056 ko || -0m00.07s ||      -148 ko |   -0.29% |         -0.01%
  0m25.98s |  499960 ko | Arithmetic/Saturated.vo                                         |   0m25.90s |  499960 ko || +0m00.08s ||         0 ko |   +0.30% |         +0.00%
  0m25.83s | 1816800 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml                 |   0m25.89s | 1816916 ko || -0m00.06s ||      -116 ko |   -0.23% |         -0.00%
  0m24.65s |  157136 ko | fiat-bedrock2/src/p434_64.c                                     |   0m24.60s |  157372 ko || +0m00.04s ||      -236 ko |   +0.20% |         -0.14%
  0m24.25s | 1705940 ko | ExtractionOCaml/unsaturated_solinas.ml                          |   0m24.41s | 1705940 ko || -0m00.16s ||         0 ko |   -0.65% |         +0.00%
  0m24.16s |  154696 ko | fiat-go/64/p434/p434.go                                         |   0m23.40s |  154816 ko || +0m00.76s ||      -120 ko |   +3.24% |         -0.07%
  0m23.51s |  161476 ko | fiat-json/src/p434_64.json                                      |   0m23.73s |  161268 ko || -0m00.21s ||       208 ko |   -0.92% |         +0.12%
  0m23.18s |  865764 ko | Bedrock/Field/Synthesis/Examples/LadderStep.vo                  |   0m23.04s |  866356 ko || +0m00.14s ||      -592 ko |   +0.60% |         -0.06%
  0m22.42s |  790944 ko | Bedrock/Field/Translation/Proofs/Expr.vo                        |   0m22.28s |  791304 ko || +0m00.14s ||      -360 ko |   +0.62% |         -0.04%
  0m22.39s |  161208 ko | fiat-c/src/p434_64.c                                            |   0m22.54s |  161128 ko || -0m00.14s ||        80 ko |   -0.66% |         +0.04%
  0m21.52s | 1703968 ko | ExtractionOCaml/bedrock2_base_conversion.ml                     |   0m21.58s | 1704056 ko || -0m00.05s ||       -88 ko |   -0.27% |         -0.00%
  0m21.19s |  821980 ko | PushButtonSynthesis/WordByWordMontgomery.vo                     |   0m21.45s |  821752 ko || -0m00.25s ||       228 ko |   -1.21% |         +0.02%
  0m20.89s |  734160 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo               |   0m20.98s |  734052 ko || -0m00.08s ||       108 ko |   -0.42% |         +0.01%
  0m20.80s |  169984 ko | fiat-rust/src/p434_64.rs                                        |   0m20.71s |  169996 ko || +0m00.08s ||       -12 ko |   +0.43% |         -0.00%
  0m19.84s | 1646164 ko | ExtractionOCaml/base_conversion.ml                              |   0m20.00s | 1646408 ko || -0m00.16s ||      -244 ko |   -0.80% |         -0.01%
  0m19.01s | 1651992 ko | ExtractionOCaml/saturated_solinas.ml                            |   0m19.91s | 1649388 ko || -0m00.89s ||      2604 ko |   -4.52% |         +0.15%
  0m18.29s | 1821048 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml                 |   0m18.38s | 1820724 ko || -0m00.08s ||       324 ko |   -0.48% |         +0.01%
  0m18.14s |  820032 ko | Bedrock/Field/Synthesis/Examples/X1305_32.vo                    |   0m18.11s |  820036 ko || +0m00.03s ||        -4 ko |   +0.16% |         -0.00%
  0m17.93s |  943124 ko | StandaloneDebuggingExamples.vo                                  |   0m18.00s |  943136 ko || -0m00.07s ||       -12 ko |   -0.38% |         -0.00%
  0m17.88s |  847492 ko | Bedrock/End2End/RupicolaCrypto/Low.vo                           |   0m18.04s |  847304 ko || -0m00.16s ||       188 ko |   -0.88% |         +0.02%
  0m17.45s | 1931916 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs           |   0m17.19s | 1931840 ko || +0m00.25s ||        76 ko |   +1.51% |         +0.00%
  0m17.00s | 1778328 ko | ExtractionOCaml/perf_unsaturated_solinas.ml                     |   0m17.14s | 1777956 ko || -0m00.14s ||       372 ko |   -0.81% |         +0.02%
  0m16.71s |  532988 ko | Arithmetic/WordByWordMontgomery.vo                              |   0m16.42s |  533328 ko || +0m00.28s ||      -340 ko |   +1.76% |         -0.06%
  0m16.67s |  754944 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo |   0m16.69s |  755004 ko || -0m00.01s ||       -60 ko |   -0.11% |         -0.00%
  0m16.63s |  831228 ko | Curves/Edwards/XYZT/Basic.vo                                    |   0m16.80s |  831440 ko || -0m00.17s ||      -212 ko |   -1.01% |         -0.02%
  0m16.61s | 1848496 ko | ExtractionHaskell/word_by_word_montgomery.hs                    |   0m16.63s | 1848964 ko || -0m00.01s ||      -468 ko |   -0.12% |         -0.02%
  0m16.54s |  727500 ko | Bedrock/End2End/RupicolaCrypto/Derive.vo                        |   0m16.40s |  727360 ko || +0m00.14s ||       140 ko |   +0.85% |         +0.01%
  0m15.65s |  726436 ko | Curves/Edwards/AffineProofs.vo                                  |   0m15.49s |  726168 ko || +0m00.16s ||       268 ko |   +1.03% |         +0.03%
  0m15.19s |  135368 ko | fiat-bedrock2/src/p224_32.c                                     |   0m15.22s |  134820 ko || -0m00.03s ||       548 ko |   -0.19% |         +0.40%
  0m15.18s |  790840 ko | Bedrock/Field/Translation/Proofs/Func.vo                        |   0m15.98s |  790980 ko || -0m00.80s ||      -140 ko |   -5.00% |         -0.01%
  0m15.07s |  515772 ko | Arithmetic/BarrettReduction.vo                                  |   0m15.03s |  515900 ko || +0m00.04s ||      -128 ko |   +0.26% |         -0.02%
  0m14.75s |  800572 ko | Bedrock/End2End/Poly1305/Field1305.vo                           |   0m14.66s |  800468 ko || +0m00.08s ||       104 ko |   +0.61% |         +0.01%
  0m14.34s |  119540 ko | fiat-zig/src/p224_32.zig                                        |   0m14.40s |  119716 ko || -0m00.06s ||      -176 ko |   -0.41% |         -0.14%
  0m14.15s |  134416 ko | fiat-java/src/FiatP224.java                                     |   0m14.19s |  134372 ko || -0m00.03s ||        44 ko |   -0.28% |         +0.03%
  0m14.11s |  460396 ko | Algebra/Field.vo                                                |   0m14.06s |  460312 ko || +0m00.04s ||        84 ko |   +0.35% |         +0.01%
  0m14.11s |  134736 ko | fiat-go/32/p224/p224.go                                         |   0m13.86s |  134624 ko || +0m00.25s ||       112 ko |   +1.80% |         +0.08%
  0m14.03s |  482592 ko | Arithmetic/Core.vo                                              |   0m14.04s |  482508 ko || -0m00.00s ||        84 ko |   -0.07% |         +0.01%
  0m13.84s |  668096 ko | Bedrock/Group/AdditionChains.vo                                 |   0m13.62s |  667924 ko || +0m00.22s ||       172 ko |   +1.61% |         +0.02%
  0m13.55s |  588324 ko | Bedrock/Field/Common/Util.vo                                    |   0m13.49s |  588840 ko || +0m00.06s ||      -516 ko |   +0.44% |         -0.08%
  0m13.43s |  116236 ko | fiat-c/src/p224_32.c                                            |   0m13.66s |  116720 ko || -0m00.23s ||      -484 ko |   -1.68% |         -0.41%
  0m13.03s | 1549244 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs               |   0m13.15s | 1549436 ko || -0m00.12s ||      -192 ko |   -0.91% |         -0.01%
  0m12.90s |  971168 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo            |   0m13.02s |  971124 ko || -0m00.11s ||        44 ko |   -0.92% |         +0.00%
  0m12.90s |  657996 ko | Bedrock/Group/ScalarMult/LadderStep.vo                          |   0m12.80s |  657880 ko || +0m00.09s ||       116 ko |   +0.78% |         +0.01%
  0m12.72s |  136740 ko | fiat-rust/src/p224_32.rs                                        |   0m13.56s |  136564 ko || -0m00.83s ||       176 ko |   -6.19% |         +0.12%
  0m12.70s |  833352 ko | Bedrock/Field/Synthesis/New/Signature.vo                        |   0m13.10s |  833596 ko || -0m00.40s ||      -244 ko |   -3.05% |         -0.02%
  0m12.59s | 1542716 ko | ExtractionHaskell/unsaturated_solinas.hs                        |   0m12.74s | 1542688 ko || -0m00.15s ||        28 ko |   -1.17% |         +0.00%
  0m12.30s |  841348 ko | PushButtonSynthesis/SmallExamples.vo                            |   0m12.30s |  841420 ko || +0m00.00s ||       -72 ko |   +0.00% |         -0.00%
  0m12.27s |   89364 ko | fiat-bedrock2/src/p384_64.c                                     |   0m12.12s |   89116 ko || +0m00.15s ||       248 ko |   +1.23% |         +0.27%
  0m12.19s | 1488728 ko | ExtractionHaskell/bedrock2_base_conversion.hs                   |   0m11.35s | 1488816 ko || +0m00.83s ||       -88 ko |   +7.40% |         -0.00%
  0m11.26s | 1488656 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs                 |   0m11.33s | 1488936 ko || -0m00.07s ||      -280 ko |   -0.61% |         -0.01%
  0m11.25s | 1378336 ko | ExtractionHaskell/base_conversion.hs                            |   0m10.60s | 1378392 ko || +0m00.65s ||       -56 ko |   +6.13% |         -0.00%
  0m11.01s |  113036 ko | fiat-json/src/p384_64.json                                      |   0m10.96s |  113164 ko || +0m00.04s ||      -128 ko |   +0.45% |         -0.11%
  0m10.97s |   97280 ko | fiat-go/64/p384/p384.go                                         |   0m11.07s |   97208 ko || -0m00.09s ||        72 ko |   -0.90% |         +0.07%
  0m10.92s |  603084 ko | Bedrock/Field/Translation/Proofs/Flatten.vo                     |   0m10.54s |  603676 ko || +0m00.38s ||      -592 ko |   +3.60% |         -0.09%
  0m10.87s |  105140 ko | fiat-zig/src/p384_64.zig                                        |   0m10.87s |  105204 ko || +0m00.00s ||       -64 ko |   +0.00% |         -0.06%
  0m10.82s | 1429068 ko | ExtractionHaskell/saturated_solinas.hs                          |   0m10.75s | 1429292 ko || +0m00.07s ||      -224 ko |   +0.65% |         -0.01%
  0m10.71s |   98680 ko | fiat-rust/src/p384_64.rs                                        |   0m10.58s |   99216 ko || +0m00.13s ||      -536 ko |   +1.22% |         -0.54%
  0m10.29s |  100764 ko | fiat-c/src/p384_64.c                                            |   0m10.53s |  100840 ko || -0m00.24s ||       -76 ko |   -2.27% |         -0.07%
  0m10.27s | 1323388 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo             |   0m10.14s | 1323312 ko || +0m00.12s ||        76 ko |   +1.28% |         +0.00%
  0m10.22s |  472772 ko | Primitives/MxDHRepChange.vo                                     |   0m10.24s |  472628 ko || -0m00.01s ||       144 ko |   -0.19% |         +0.03%
  0m09.54s |  651888 ko | Bedrock/Group/ScalarMult/CSwap.vo                               |   0m09.56s |  651896 ko || -0m00.02s ||        -8 ko |   -0.20% |         -0.00%
  0m09.37s |  450344 ko | Algebra/Ring.vo                                                 |   0m09.45s |  450292 ko || -0m00.08s ||        52 ko |   -0.84% |         +0.01%
  0m08.51s |  107092 ko | fiat-json/src/p448_solinas_32.json                              |   0m08.22s |  106856 ko || +0m00.28s ||       236 ko |   +3.52% |         +0.22%
  0m08.17s |  902368 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo       |   0m08.08s |  901208 ko || +0m00.08s ||      1160 ko |   +1.11% |         +0.12%
  0m08.14s |   49928 ko | fiat-zig/src/p448_solinas_32.zig                                |   0m08.14s |   49960 ko || +0m00.00s ||       -32 ko |   +0.00% |         -0.06%
  0m08.10s |  695232 ko | PushButtonSynthesis/BaseConversion.vo                           |   0m08.07s |  695140 ko || +0m00.02s ||        92 ko |   +0.37% |         +0.01%
  0m08.01s |   49284 ko | fiat-rust/src/p448_solinas_32.rs                                |   0m08.05s |   49028 ko || -0m00.04s ||       256 ko |   -0.49% |         +0.52%
  0m07.95s |   50232 ko | fiat-c/src/p448_solinas_32.c                                    |   0m07.96s |   50288 ko || -0m00.00s ||       -56 ko |   -0.12% |         -0.11%
  0m07.33s |  703396 ko | PushButtonSynthesis/Primitives.vo                               |   0m07.37s |  703532 ko || -0m00.04s ||      -136 ko |   -0.54% |         -0.01%
  0m06.70s |  600556 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo         |   0m06.66s |  600488 ko || +0m00.04s ||        68 ko |   +0.60% |         +0.01%
  0m06.53s |  464132 ko | Arithmetic/FancyMontgomeryReduction.vo                          |   0m06.56s |  464024 ko || -0m00.02s ||       108 ko |   -0.45% |         +0.02%
  0m06.20s |  828840 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo                |   0m06.24s |  829040 ko || -0m00.04s ||      -200 ko |   -0.64% |         -0.02%
  0m05.44s |  500740 ko | Arithmetic/BYInv.vo                                             |   0m05.23s |  500620 ko || +0m00.20s ||       120 ko |   +4.01% |         +0.02%
  0m05.36s |  735980 ko | Bedrock/Field/Synthesis/Examples/EncodeDecode.vo                |   0m05.40s |  735884 ko || -0m00.04s ||        96 ko |   -0.74% |         +0.01%
  0m05.14s |  525612 ko | Fancy/Prod.vo                                                   |   0m05.32s |  525640 ko || -0m00.18s ||       -28 ko |   -3.38% |         -0.00%
  0m05.08s |  490584 ko | COperationSpecifications.vo                                     |   0m04.98s |  490468 ko || +0m00.09s ||       116 ko |   +2.00% |         +0.02%
  0m04.85s |  459368 ko | Util/FsatzAutoLemmas.vo                                         |   0m04.83s |  459464 ko || +0m00.01s ||       -96 ko |   +0.41% |         -0.02%
  0m04.81s |  500640 ko | Curves/Edwards/Pre.vo                                           |   0m04.76s |  500728 ko || +0m00.04s ||       -88 ko |   +1.05% |         -0.01%
  0m04.77s |  686920 ko | PushButtonSynthesis/BarrettReduction.vo                         |   0m04.66s |  686904 ko || +0m00.10s ||        16 ko |   +2.36% |         +0.00%
  0m04.12s |  474680 ko | Algebra/Field_test.vo                                           |   0m04.08s |  474604 ko || +0m00.04s ||        76 ko |   +0.98% |         +0.01%
  0m04.09s |  457004 ko | UnsaturatedSolinasHeuristics.vo                                 |   0m03.94s |  456964 ko || +0m00.14s ||        40 ko |   +3.80% |         +0.00%
  0m04.08s |   34728 ko | fiat-go/64/p521/p521.go                                         |   0m03.69s |   34624 ko || +0m00.39s ||       104 ko |  +10.56% |         +0.30%
  0m03.91s |  483984 ko | Curves/Montgomery/Affine.vo                                     |   0m03.76s |  484132 ko || +0m00.15s ||      -148 ko |   +3.98% |         -0.03%
  0m03.84s |  759328 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo               |   0m03.83s |  759480 ko || +0m00.00s ||      -152 ko |   +0.26% |         -0.02%
  0m03.82s |   44204 ko | fiat-bedrock2/src/p521_64.c                                     |   0m03.79s |   44288 ko || +0m00.02s ||       -84 ko |   +0.79% |         -0.18%
  0m03.75s |  602168 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo                       |   0m03.19s |  601884 ko || +0m00.56s ||       284 ko |  +17.55% |         +0.04%
  0m03.62s |  452916 ko | Arithmetic/UniformWeight.vo                                     |   0m03.59s |  452840 ko || +0m00.03s ||        76 ko |   +0.83% |         +0.01%
  0m03.44s |  669884 ko | Bedrock/Group/ScalarMult/ScalarMult.vo                          |   0m03.85s |  669920 ko || -0m00.41s ||       -36 ko |  -10.64% |         -0.00%
  0m03.31s |  564880 ko | PushButtonSynthesis/BaseConversionReificationCache.vo           |   0m03.37s |  564728 ko || -0m00.06s ||       152 ko |   -1.78% |         +0.02%
  0m03.25s |  723560 ko | Bedrock/Field/Synthesis/Examples/MulTwice.vo                    |   0m03.29s |  723480 ko || -0m00.04s ||        80 ko |   -1.21% |         +0.01%
  0m03.24s |   39160 ko | fiat-json/src/p521_64.json                                      |   0m03.27s |   38948 ko || -0m00.02s ||       212 ko |   -0.91% |         +0.54%
  0m03.18s |   29760 ko | fiat-zig/src/p521_64.zig                                        |   0m03.16s |   30112 ko || +0m00.02s ||      -352 ko |   +0.63% |         -1.16%
  0m03.17s |  696272 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo                 |   0m03.16s |  696292 ko || +0m00.00s ||       -20 ko |   +0.31% |         -0.00%
  0m03.13s |   28368 ko | fiat-c/src/p521_64.c                                            |   0m03.09s |   28348 ko || +0m00.04s ||        20 ko |   +1.29% |         +0.07%
  0m03.13s |   26928 ko | fiat-rust/src/p521_64.rs                                        |   0m03.12s |   26860 ko || +0m00.00s ||        68 ko |   +0.32% |         +0.25%
  0m03.08s |  392784 ko | Algebra/Group.vo                                                |   0m03.04s |  392780 ko || +0m00.04s ||         4 ko |   +1.31% |         +0.00%
  0m03.04s |   46732 ko | fiat-bedrock2/src/secp256k1_64.c                                |   0m03.10s |   46996 ko || -0m00.06s ||      -264 ko |   -1.93% |         -0.56%
  0m02.93s |  709176 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo         |   0m02.96s |  709088 ko || -0m00.02s ||        88 ko |   -1.01% |         +0.01%
  0m02.88s |  614332 ko | Bedrock/Field/Interface/Compilation2.vo                         |   0m02.92s |  614332 ko || -0m00.04s ||         0 ko |   -1.36% |         +0.00%
  0m02.85s |  693400 ko | PushButtonSynthesis/SaturatedSolinas.vo                         |   0m02.94s |  693236 ko || -0m00.08s ||       164 ko |   -3.06% |         +0.02%
  0m02.74s |   44536 ko | fiat-go/64/secp256k1/secp256k1.go                               |   0m02.74s |   44672 ko || +0m00.00s ||      -136 ko |   +0.00% |         -0.30%
  0m02.73s |   53436 ko | fiat-json/src/secp256k1_64.json                                 |   0m02.74s |   53204 ko || -0m00.01s ||       232 ko |   -0.36% |         +0.43%
  0m02.68s |   41180 ko | fiat-bedrock2/src/p448_solinas_64.c                             |   0m02.65s |   41316 ko || +0m00.03s ||      -136 ko |   +1.13% |         -0.32%
  0m02.68s |   37156 ko | fiat-go/64/p448solinas/p448solinas.go                           |   0m02.74s |   37104 ko || -0m00.06s ||        52 ko |   -2.18% |         +0.14%
  0m02.67s |   44656 ko | fiat-zig/src/secp256k1_64.zig                                   |   0m02.69s |   44596 ko || -0m00.02s ||        60 ko |   -0.74% |         +0.13%
  0m02.58s |  723812 ko | CLI.vo                                                          |   0m02.68s |  723980 ko || -0m00.10s ||      -168 ko |   -3.73% |         -0.02%
  0m02.57s |   44360 ko | fiat-rust/src/secp256k1_64.rs                                   |   0m02.61s |   44396 ko || -0m00.04s ||       -36 ko |   -1.53% |         -0.08%
  0m02.54s |   45360 ko | fiat-c/src/secp256k1_64.c                                       |   0m02.53s |   45588 ko || +0m00.01s ||      -228 ko |   +0.39% |         -0.50%
  0m02.52s |   39680 ko | fiat-bedrock2/src/curve25519_32.c                               |   0m02.56s |   39720 ko || -0m00.04s ||       -40 ko |   -1.56% |         -0.10%
  0m02.37s |   46872 ko | fiat-bedrock2/src/p224_64.c                                     |   0m02.41s |   46576 ko || -0m00.04s ||       296 ko |   -1.65% |         +0.63%
  0m02.35s |  460112 ko | Spec/MontgomeryCurve.vo                                         |   0m02.34s |  460088 ko || +0m00.01s ||        24 ko |   +0.42% |         +0.00%
  0m02.28s |   43440 ko | fiat-bedrock2/src/p256_64.c                                     |   0m02.20s |   43528 ko || +0m00.07s ||       -88 ko |   +3.63% |         -0.20%
  0m02.25s |  454396 ko | Arithmetic/Freeze.vo                                            |   0m02.21s |  454772 ko || +0m00.04s ||      -376 ko |   +1.80% |         -0.08%
  0m02.18s |  588096 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo                  |   0m02.29s |  588020 ko || -0m00.10s ||        76 ko |   -4.80% |         +0.01%
  0m02.14s |   40248 ko | fiat-go/64/p224/p224.go                                         |   0m01.99s |   40284 ko || +0m00.15s ||       -36 ko |   +7.53% |         -0.08%
  0m02.09s |   39688 ko | fiat-json/src/p448_solinas_64.json                              |   0m01.96s |   39748 ko || +0m00.12s ||       -60 ko |   +6.63% |         -0.15%
  0m02.06s |  453840 ko | Arithmetic/BaseConversion.vo                                    |   0m02.04s |  453836 ko || +0m00.02s ||         4 ko |   +0.98% |         +0.00%
  0m02.06s |   39184 ko | fiat-go/64/p256/p256.go                                         |   0m02.04s |   39216 ko || +0m00.02s ||       -32 ko |   +0.98% |         -0.08%
  0m02.05s |   26980 ko | fiat-go/32/curve25519/curve25519.go                             |   0m02.07s |   26868 ko || -0m00.02s ||       112 ko |   -0.96% |         +0.41%
  0m02.04s |   49664 ko | fiat-json/src/p224_64.json                                      |   0m02.01s |   49476 ko || +0m00.03s ||       188 ko |   +1.49% |         +0.37%
  0m01.96s |   26676 ko | fiat-zig/src/p448_solinas_64.zig                                |   0m01.97s |   27080 ko || -0m00.01s ||      -404 ko |   -0.50% |         -1.49%
  0m01.94s |   40704 ko | fiat-c/src/p224_64.c                                            |   0m01.93s |   40252 ko || +0m00.01s ||       452 ko |   +0.51% |         +1.12%
  0m01.93s |   49468 ko | fiat-json/src/p256_64.json                                      |   0m01.89s |   49376 ko || +0m00.04s ||        92 ko |   +2.11% |         +0.18%
  0m01.93s |   40740 ko | fiat-rust/src/p224_64.rs                                        |   0m01.92s |   40492 ko || +0m00.01s ||       248 ko |   +0.52% |         +0.61%
  0m01.92s |   26844 ko | fiat-rust/src/p448_solinas_64.rs                                |   0m01.90s |   26956 ko || +0m00.02s ||      -112 ko |   +1.05% |         -0.41%
  0m01.91s |   26608 ko | fiat-c/src/p448_solinas_64.c                                    |   0m01.92s |   26716 ko || -0m00.01s ||      -108 ko |   -0.52% |         -0.40%
  0m01.88s |   44196 ko | fiat-rust/src/p256_64.rs                                        |   0m01.87s |   44064 ko || +0m00.00s ||       132 ko |   +0.53% |         +0.29%
  0m01.86s |   41276 ko | fiat-json/src/curve25519_32.json                                |   0m01.89s |   41216 ko || -0m00.02s ||        60 ko |   -1.58% |         +0.14%
  0m01.85s |   38212 ko | fiat-c/src/p256_64.c                                            |   0m01.83s |   38464 ko || +0m00.02s ||      -252 ko |   +1.09% |         -0.65%
  0m01.85s |   41992 ko | fiat-zig/src/p224_64.zig                                        |   0m01.92s |   41908 ko || -0m00.06s ||        84 ko |   -3.64% |         +0.20%
  0m01.84s |  611976 ko | Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo               |   0m01.89s |  611848 ko || -0m00.04s ||       128 ko |   -2.64% |         +0.02%
  0m01.84s |   42996 ko | fiat-zig/src/p256_64.zig                                        |   0m01.84s |   43260 ko || +0m00.00s ||      -264 ko |   +0.00% |         -0.61%
  0m01.76s |   26732 ko | fiat-java/src/FiatCurve25519.java                               |   0m01.77s |   26512 ko || -0m00.01s ||       220 ko |   -0.56% |         +0.82%
  0m01.73s |   27128 ko | fiat-c/src/curve25519_32.c                                      |   0m01.77s |   26964 ko || -0m00.04s ||       164 ko |   -2.25% |         +0.60%
  0m01.72s |   26188 ko | fiat-zig/src/curve25519_32.zig                                  |   0m01.75s |   26120 ko || -0m00.03s ||        68 ko |   -1.71% |         +0.26%
  0m01.71s |   25576 ko | fiat-rust/src/curve25519_32.rs                                  |   0m01.73s |   25920 ko || -0m00.02s ||      -344 ko |   -1.15% |         -1.32%
  0m01.67s |  452020 ko | Arithmetic/ModOps.vo                                            |   0m01.70s |  451924 ko || -0m00.03s ||        96 ko |   -1.76% |         +0.02%
  0m01.64s |  596532 ko | Bedrock/Field/Common/Names/MakeNames.vo                         |   0m01.78s |  596440 ko || -0m00.14s ||        92 ko |   -7.86% |         +0.01%
  0m01.62s |  442476 ko | Arithmetic/ModularArithmeticTheorems.vo                         |   0m01.61s |  442388 ko || +0m00.01s ||        88 ko |   +0.62% |         +0.01%
  0m01.40s |  723572 ko | Rewriter/PerfTesting/Core.vo                                    |   0m01.38s |  723680 ko || +0m00.02s ||      -108 ko |   +1.44% |         -0.01%
  0m01.38s |  435340 ko | Spec/WeierstrassCurve.vo                                        |   0m01.39s |  435204 ko || -0m00.01s ||       136 ko |   -0.71% |         +0.03%
  0m01.34s |  419196 ko | Algebra/ScalarMult.vo                                           |   0m01.36s |  419012 ko || -0m00.02s ||       184 ko |   -1.47% |         +0.04%
  0m01.34s |  695436 ko | Bedrock/Field/Stringification/Stringification.vo                |   0m01.32s |  695400 ko || +0m00.02s ||        36 ko |   +1.51% |         +0.00%
  0m01.27s |  619712 ko | Bedrock/Specs/Field.vo                                          |   0m01.28s |  619712 ko || -0m00.01s ||         0 ko |   -0.78% |         +0.00%
  0m01.24s |  443528 ko | Arithmetic/Partition.vo                                         |   0m01.17s |  443520 ko || +0m00.07s ||         8 ko |   +5.98% |         +0.00%
  0m01.19s |  466472 ko | Arithmetic/PrimeFieldTheorems.vo                                |   0m01.22s |  466572 ko || -0m00.03s ||      -100 ko |   -2.45% |         -0.02%
  0m01.19s |  729348 ko | Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.vo     |   0m01.16s |  729312 ko || +0m00.03s ||        36 ko |   +2.58% |         +0.00%
  0m01.18s |  717524 ko | Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.vo       |   0m01.16s |  717740 ko || +0m00.02s ||      -216 ko |   +1.72% |         -0.03%
  0m01.18s |  701836 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo        |   0m01.15s |  701820 ko || +0m00.03s ||        16 ko |   +2.60% |         +0.00%
  0m01.14s |  711000 ko | StandaloneOCamlMain.vo                                          |   0m01.09s |  711028 ko || +0m00.04s ||       -28 ko |   +4.58% |         -0.00%
  0m01.09s |  745320 ko | Bedrock/Standalone/StandaloneHaskellMain.vo                     |   0m01.15s |  745348 ko || -0m00.05s ||       -28 ko |   -5.21% |         -0.00%
  0m01.08s |  697528 ko | Bedrock/Field/Synthesis/Generic/Operation.vo                    |   0m01.08s |  697352 ko || +0m00.00s ||       176 ko |   +0.00% |         +0.02%
  0m01.08s |  734036 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo                     |   0m01.11s |  733984 ko || -0m00.03s ||        52 ko |   -2.70% |         +0.00%
  0m01.07s |  597424 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo                        |   0m01.09s |  597216 ko || -0m00.02s ||       208 ko |   -1.83% |         +0.03%
  0m01.06s |  702512 ko | Bedrock/Field/Synthesis/Specialized/ReifiedOperation.vo         |   0m01.04s |  702364 ko || +0m00.02s ||       148 ko |   +1.92% |         +0.02%
  0m01.05s |  695308 ko | Bedrock/Field/Synthesis/Specialized/Tactics.vo                  |   0m01.11s |  695460 ko || -0m00.06s ||      -152 ko |   -5.40% |         -0.02%
  0m01.04s |  693912 ko | Bedrock/Field/Synthesis/Generic/Tactics.vo                      |   0m01.13s |  693824 ko || -0m00.08s ||        88 ko |   -7.96% |         +0.01%
  0m01.03s |  711012 ko | StandaloneHaskellMain.vo                                        |   0m01.01s |  710808 ko || +0m00.02s ||       204 ko |   +1.98% |         +0.02%
  0m01.02s |  713540 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo                       |   0m00.97s |  713532 ko || +0m00.05s ||         8 ko |   +5.15% |         +0.00%
  0m01.01s |  438384 ko | Curves/Edwards/XYZT/Precomputed.vo                              |   0m01.02s |  438288 ko || -0m00.01s ||        96 ko |   -0.98% |         +0.02%
  0m00.99s |  588484 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo                       |   0m00.97s |  588468 ko || +0m00.02s ||        16 ko |   +2.06% |         +0.00%
  0m00.98s |  745588 ko | Bedrock/Standalone/StandaloneOCamlMain.vo                       |   0m01.00s |  745520 ko || -0m00.02s ||        68 ko |   -2.00% |         +0.00%
  0m00.96s |  655460 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo              |   0m00.97s |  655516 ko || -0m00.01s ||       -56 ko |   -1.03% |         -0.00%
  0m00.91s |  650960 ko | Bedrock/Field/Translation/Parameters/Defaults.vo                |   0m00.93s |  650964 ko || -0m00.02s ||        -4 ko |   -2.15% |         -0.00%
  0m00.91s |  655616 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo              |   0m00.95s |  655540 ko || -0m00.03s ||        76 ko |   -4.21% |         +0.01%
  0m00.89s |  610812 ko | Bedrock/Group/Point.vo                                          |   0m00.91s |  610968 ko || -0m00.02s ||      -156 ko |   -2.19% |         -0.02%
  0m00.86s |  608444 ko | Bedrock/Field/Interface/Representation.vo                       |   0m00.93s |  608228 ko || -0m00.07s ||       216 ko |   -7.52% |         +0.03%
  0m00.84s |  424488 ko | Curves/Montgomery/AffineInstances.vo                            |   0m00.86s |  424488 ko || -0m00.02s ||         0 ko |   -2.32% |         +0.00%
  0m00.76s |  580932 ko | Bedrock/Field/Common/Tactics.vo                                 |   0m00.80s |  580944 ko || -0m00.04s ||       -12 ko |   -5.00% |         -0.00%
  0m00.65s |  419948 ko | Algebra/IntegralDomain.vo                                       |   0m00.67s |  419940 ko || -0m00.02s ||         8 ko |   -2.98% |         +0.00%
  0m00.64s |   24856 ko | fiat-go/64/curve25519/curve25519.go                             |   0m00.63s |   24856 ko || +0m00.01s ||         0 ko |   +1.58% |         +0.00%
  0m00.62s |   28032 ko | fiat-bedrock2/src/curve25519_64.c                               |   0m00.61s |   27932 ko || +0m00.01s ||       100 ko |   +1.63% |         +0.35%
  0m00.58s |  417548 ko | Algebra/SubsetoidRing.vo                                        |   0m00.55s |  417472 ko || +0m00.02s ||        76 ko |   +5.45% |         +0.01%
  0m00.58s |  462092 ko | ArithmeticCPS/WordByWordMontgomery.vo                           |   0m00.53s |  462024 ko || +0m00.04s ||        68 ko |   +9.43% |         +0.01%
  0m00.55s |  449476 ko | ArithmeticCPS/Saturated.vo                                      |   0m00.45s |  449424 ko || +0m00.10s ||        52 ko |  +22.22% |         +0.01%
  0m00.51s |  458836 ko | ArithmeticCPS/Freeze.vo                                         |   0m00.47s |  458844 ko || +0m00.04s ||        -8 ko |   +8.51% |         -0.00%
  0m00.51s |  447880 ko | Bedrock/Specs/Group.vo                                          |   0m00.55s |  447720 ko || -0m00.04s ||       160 ko |   -7.27% |         +0.03%
  0m00.50s |  458932 ko | ArithmeticCPS/BaseConversion.vo                                 |   0m00.41s |  458888 ko || +0m00.09s ||        44 ko |  +21.95% |         +0.00%
  0m00.50s |  453764 ko | ArithmeticCPS/ModOps.vo                                         |   0m00.49s |  453232 ko || +0m00.01s ||       532 ko |   +2.04% |         +0.11%
  0m00.50s |   27960 ko | fiat-json/src/curve25519_64.json                                |   0m00.49s |   27740 ko || +0m00.01s ||       220 ko |   +2.04% |         +0.79%
  0m00.48s |  447108 ko | ArithmeticCPS/Core.vo                                           |   0m00.52s |  447184 ko || -0m00.04s ||       -76 ko |   -7.69% |         -0.01%
  0m00.48s |  473680 ko | Bedrock/End2End/RupicolaCrypto/Spec.vo                          |   0m00.51s |  473628 ko || -0m00.03s ||        52 ko |   -5.88% |         +0.01%
  0m00.46s |   22288 ko | fiat-c/src/curve25519_64.c                                      |   0m00.46s |   22288 ko || +0m00.00s ||         0 ko |   +0.00% |         +0.00%
  0m00.45s |   22652 ko | fiat-zig/src/curve25519_64.zig                                  |   0m00.45s |   22564 ko || +0m00.00s ||        88 ko |   +0.00% |         +0.39%
  0m00.44s |  467020 ko | Arithmetic/FLia.vo                                              |   0m00.46s |  467028 ko || -0m00.02s ||        -8 ko |   -4.34% |         -0.00%
  0m00.44s |   22876 ko | fiat-rust/src/curve25519_64.rs                                  |   0m00.44s |   22996 ko || +0m00.00s ||      -120 ko |   +0.00% |         -0.52%
  0m00.35s |  421796 ko | Curves/Weierstrass/Affine.vo                                    |   0m00.37s |  421640 ko || -0m00.02s ||       156 ko |   -5.40% |         +0.03%
  0m00.35s |   26356 ko | fiat-bedrock2/src/poly1305_32.c                                 |   0m00.36s |   26220 ko || -0m00.01s ||       136 ko |   -2.77% |         +0.51%
  0m00.34s |  420588 ko | Spec/CompleteEdwardsCurve.vo                                    |   0m00.38s |  420564 ko || -0m00.03s ||        24 ko |  -10.52% |         +0.00%
  0m00.29s |  363984 ko | Curves/Montgomery/XZ.vo                                         |   0m00.31s |  363988 ko || -0m00.02s ||        -4 ko |   -6.45% |         -0.00%
  0m00.29s |   22212 ko | fiat-go/32/poly1305/poly1305.go                                 |   0m00.29s |   22220 ko || +0m00.00s ||        -8 ko |   +0.00% |         -0.03%
  0m00.25s |  353344 ko | Util/AdditionChainExponentiation.vo                             |   0m00.20s |  353308 ko || +0m00.04s ||        36 ko |  +24.99% |         +0.01%
  0m00.25s |   26260 ko | fiat-json/src/poly1305_32.json                                  |   0m00.24s |   26356 ko || +0m00.01s ||       -96 ko |   +4.16% |         -0.36%
  0m00.22s |   21252 ko | fiat-java/src/FiatPoly1305.java                                 |   0m00.23s |   21660 ko || -0m00.01s ||      -408 ko |   -4.34% |         -1.88%
  0m00.20s |   21536 ko | fiat-c/src/poly1305_32.c                                        |   0m00.20s |   21560 ko || +0m00.00s ||       -24 ko |   +0.00% |         -0.11%
  0m00.20s |   21452 ko | fiat-zig/src/poly1305_32.zig                                    |   0m00.23s |   21532 ko || -0m00.03s ||       -80 ko |  -13.04% |         -0.37%
  0m00.19s |   21272 ko | fiat-rust/src/poly1305_32.rs                                    |   0m00.20s |   21456 ko || -0m00.01s ||      -184 ko |   -5.00% |         -0.85%
  0m00.18s |   22320 ko | fiat-go/64/poly1305/poly1305.go                                 |   0m00.18s |   21924 ko || +0m00.00s ||       396 ko |   +0.00% |         +1.80%
  0m00.16s |   24456 ko | fiat-bedrock2/src/poly1305_64.c                                 |   0m00.15s |   24472 ko || +0m00.01s ||       -16 ko |   +6.66% |         -0.06%
  0m00.14s |   24140 ko | fiat-json/src/poly1305_64.json                                  |   0m00.15s |   24376 ko || -0m00.00s ||      -236 ko |   -6.66% |         -0.96%
  0m00.12s |   20776 ko | fiat-zig/src/poly1305_64.zig                                    |   0m00.11s |   20772 ko || +0m00.00s ||         4 ko |   +9.09% |         +0.01%
  0m00.11s |   20884 ko | fiat-c/src/poly1305_64.c                                        |   0m00.12s |   20752 ko || -0m00.00s ||       132 ko |   -8.33% |         +0.63%
  0m00.11s |   20676 ko | fiat-rust/src/poly1305_64.rs                                    |   0m00.11s |   20828 ko || +0m00.00s ||      -152 ko |   +0.00% |         -0.72%
  0m00.08s |  220884 ko | Util/Relations.vo                                               |   0m00.14s |  189384 ko || -0m00.06s ||     31500 ko |  -42.85% |        +16.63%