ASM Equivalence Checker: Use bounds from the dag

[JasonGross]

This is another part of #1481 ripped out and implemented in a somewhat different way. Here we maintain the abstraction barrier of the dag implementation, and separate out the commits enough to profile the change of using dag bounds on its own.

We pay only a small cost for this, so it seems more than worth it.

Timing Diff

     After |   Peak Mem | File Name                                                 |     Before |   Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
----------------------------------------------------------------------------------------------------------------------------------------------------------------------
158m20.95s | 4393964 ko | Total Time / Peak Mem                                     | 156m15.65s | 4393936 ko || +2m05.29s ||        28 ko |   +1.33% |         +0.00%
----------------------------------------------------------------------------------------------------------------------------------------------------------------------
 41m01.08s |  381660 ko | fiat-amd64/p434-square.status                             |  39m28.73s |  392032 ko || +1m32.34s ||    -10372 ko |   +3.89% |         -2.64%
  4m32.02s |  106160 ko | fiat-amd64/p384-square.status                             |   4m13.46s |  107844 ko || +0m18.55s ||     -1684 ko |   +7.32% |         -1.56%
  5m01.88s |  112276 ko | fiat-amd64/p384-mul.status                                |   4m59.41s |  117724 ko || +0m02.47s ||     -5448 ko |   +0.82% |         -4.62%
  1m49.45s | 2241388 ko | Fancy/Barrett256.vo                                       |   1m51.54s | 2241304 ko || -0m02.08s ||        84 ko |   -1.87% |         +0.00%
  1m02.93s | 4393964 ko | Bedrock/End2End/RupicolaCrypto/Derive.vo                  |   1m00.82s | 4393936 ko || +0m02.10s ||        28 ko |   +3.46% |         +0.00%
  0m32.74s |   55196 ko | fiat-amd64/p448-square.status                             |   0m35.35s |   54524 ko || -0m02.60s ||       672 ko |   -7.38% |         +1.23%
  0m21.12s |   43776 ko | fiat-amd64/secp256k1-mul.status                           |   0m18.18s |   44332 ko || +0m02.94s ||      -556 ko |  +16.17% |         -1.25%
  1m34.95s |   71336 ko | fiat-amd64/p448-mul.status                                |   1m36.14s |   71528 ko || -0m01.18s ||      -192 ko |   -1.23% |         -0.26%
  0m43.46s | 2148100 ko | ExtractionOCaml/bedrock2_solinas_reduction                |   0m41.91s | 2148060 ko || +0m01.55s ||        40 ko |   +3.69% |         +0.00%
  0m31.75s | 1520824 ko | StandaloneDebuggingExamples.vo                            |   0m30.17s | 1520896 ko || +0m01.57s ||       -72 ko |   +5.23% |         -0.00%
  0m20.87s | 1874548 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml           |   0m19.73s | 1874660 ko || +0m01.14s ||      -112 ko |   +5.77% |         -0.00%
  0m19.03s |   45236 ko | fiat-amd64/secp256k1-square.status                        |   0m17.21s |   44724 ko || +0m01.82s ||       512 ko |  +10.57% |         +1.14%
  0m14.65s |   44880 ko | fiat-amd64/p521-square.status                             |   0m13.42s |   45636 ko || +0m01.23s ||      -756 ko |   +9.16% |         -1.65%
 47m04.34s |  403740 ko | fiat-amd64/p434-mul.status                                |  47m03.56s |  415872 ko || +0m00.78s ||    -12132 ko |   +0.02% |         -2.91%
 10m09.41s | 2592812 ko | Bedrock/End2End/X25519/GarageDoor.vo                      |  10m10.08s | 2592672 ko || -0m00.67s ||       140 ko |   -0.10% |         +0.00%
  5m34.52s | 2784892 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo           |   5m34.14s | 2784788 ko || +0m00.37s ||       104 ko |   +0.11% |         +0.00%
  4m12.67s | 2567008 ko | Assembly/WithBedrock/Proofs.vo                            |   4m11.98s | 2566796 ko || +0m00.68s ||       212 ko |   +0.27% |         +0.00%
  1m53.50s | 1596296 ko | Bedrock/End2End/X25519/Field25519.vo                      |   1m53.69s | 1595988 ko || -0m00.18s ||       308 ko |   -0.16% |         +0.01%
  1m39.23s | 1511380 ko | Assembly/EquivalenceProofs.vo                             |   1m39.70s | 1511392 ko || -0m00.47s ||       -12 ko |   -0.47% |         -0.00%
  1m29.49s | 2008892 ko | SlowPrimeSynthesisExamples.vo                             |   1m29.42s | 2008852 ko || +0m00.06s ||        40 ko |   +0.07% |         +0.00%
  1m12.44s | 1428436 ko | Assembly/WithBedrock/SymbolicProofs.vo                    |   1m12.17s | 1428424 ko || +0m00.26s ||        12 ko |   +0.37% |         +0.00%
  1m02.94s |   64012 ko | fiat-amd64/p521-mul.status                                |   1m02.87s |   64192 ko || +0m00.07s ||      -180 ko |   +0.11% |         -0.28%
  0m47.62s | 1746252 ko | Fancy/Montgomery256.vo                                    |   0m47.45s | 1746172 ko || +0m00.16s ||        80 ko |   +0.35% |         +0.00%
  0m46.31s | 1483736 ko | Assembly/Symbolic.vo                                      |   0m46.11s | 1482844 ko || +0m00.20s ||       892 ko |   +0.43% |         +0.06%
  0m42.42s | 2147892 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery     |   0m42.25s | 2147924 ko || +0m00.17s ||       -32 ko |   +0.40% |         -0.00%
  0m41.62s | 2147952 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery          |   0m41.65s | 2147836 ko || -0m00.03s ||       116 ko |   -0.07% |         +0.00%
  0m41.10s | 2147880 ko | ExtractionOCaml/solinas_reduction                         |   0m41.07s | 2147912 ko || +0m00.03s ||       -32 ko |   +0.07% |         -0.00%
  0m40.53s | 1779308 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas         |   0m40.66s | 1780496 ko || -0m00.12s ||     -1188 ko |   -0.31% |         -0.06%
  0m40.12s | 1779684 ko | ExtractionOCaml/bedrock2_unsaturated_solinas              |   0m39.13s | 1779368 ko || +0m00.98s ||       316 ko |   +2.53% |         +0.01%
  0m39.97s | 2147984 ko | ExtractionOCaml/word_by_word_montgomery                   |   0m40.17s | 2147956 ko || -0m00.20s ||        28 ko |   -0.49% |         +0.00%
  0m38.47s | 1286368 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo                |   0m38.09s | 1286304 ko || +0m00.37s ||        64 ko |   +0.99% |         +0.00%
  0m38.35s | 1689328 ko | ExtractionOCaml/unsaturated_solinas                       |   0m38.34s | 1688416 ko || +0m00.00s ||       912 ko |   +0.02% |         +0.05%
  0m37.50s | 1453656 ko | ExtractionOCaml/with_bedrock2_solinas_reduction           |   0m37.25s | 1453924 ko || +0m00.25s ||      -268 ko |   +0.67% |         -0.01%
  0m37.28s | 1453524 ko | ExtractionOCaml/with_bedrock2_saturated_solinas           |   0m37.55s | 1453772 ko || -0m00.26s ||      -248 ko |   -0.71% |         -0.01%
  0m37.18s | 1442572 ko | ExtractionOCaml/bedrock2_saturated_solinas                |   0m37.21s | 1457092 ko || -0m00.03s ||    -14520 ko |   -0.08% |         -0.99%
  0m36.66s | 1450972 ko | ExtractionOCaml/with_bedrock2_base_conversion             |   0m36.41s | 1455392 ko || +0m00.25s ||     -4420 ko |   +0.68% |         -0.30%
  0m36.05s | 1446756 ko | ExtractionOCaml/bedrock2_base_conversion                  |   0m36.44s | 1453460 ko || -0m00.39s ||     -6704 ko |   -1.07% |         -0.46%
  0m35.39s | 2285364 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml             |   0m34.77s | 2285512 ko || +0m00.61s ||      -148 ko |   +1.78% |         -0.00%
  0m34.64s | 2242900 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml  |   0m33.78s | 2243116 ko || +0m00.85s ||      -216 ko |   +2.54% |         -0.00%
  0m34.51s | 2243024 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml       |   0m34.38s | 2242944 ko || +0m00.12s ||        80 ko |   +0.37% |         +0.00%
  0m34.26s | 1415884 ko | ExtractionOCaml/saturated_solinas                         |   0m34.59s | 1415904 ko || -0m00.33s ||       -20 ko |   -0.95% |         -0.00%
  0m34.19s | 2168928 ko | ExtractionOCaml/solinas_reduction.ml                      |   0m33.30s | 2168964 ko || +0m00.89s ||       -36 ko |   +2.67% |         -0.00%
  0m33.90s | 1415988 ko | ExtractionOCaml/base_conversion                           |   0m33.80s | 1415884 ko || +0m00.10s ||       104 ko |   +0.29% |         +0.00%
  0m33.21s | 2132400 ko | ExtractionOCaml/word_by_word_montgomery.ml                |   0m33.29s | 2132328 ko || -0m00.07s ||        72 ko |   -0.24% |         +0.00%
  0m31.51s | 2164380 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml      |   0m31.35s | 2164248 ko || +0m00.16s ||       132 ko |   +0.51% |         +0.00%
  0m30.99s | 2164352 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml           |   0m31.90s | 2164568 ko || -0m00.91s ||      -216 ko |   -2.85% |         -0.00%
  0m29.84s | 2043944 ko | ExtractionOCaml/unsaturated_solinas.ml                    |   0m29.78s | 2043888 ko || +0m00.05s ||        56 ko |   +0.20% |         +0.00%
  0m29.40s | 1232240 ko | ExtractionOCaml/perf_word_by_word_montgomery              |   0m28.54s | 1232264 ko || +0m00.85s ||       -24 ko |   +3.01% |         -0.00%
  0m28.97s | 1232260 ko | ExtractionOCaml/perf_unsaturated_solinas                  |   0m28.70s | 1232424 ko || +0m00.26s ||      -164 ko |   +0.94% |         -0.01%
  0m27.51s | 2053200 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml             |   0m27.43s | 2053140 ko || +0m00.08s ||        60 ko |   +0.29% |         +0.00%
  0m27.34s | 2036072 ko | ExtractionOCaml/bedrock2_base_conversion.ml               |   0m27.47s | 2035968 ko || -0m00.12s ||       104 ko |   -0.47% |         +0.00%
  0m27.34s | 2052988 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml        |   0m27.21s | 2053060 ko || +0m00.12s ||       -72 ko |   +0.47% |         -0.00%
  0m27.30s | 2053260 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml        |   0m27.45s | 2053064 ko || -0m00.14s ||       196 ko |   -0.54% |         +0.00%
  0m26.56s | 2036256 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml          |   0m27.33s | 2036248 ko || -0m00.76s ||         8 ko |   -2.81% |         +0.00%
  0m26.00s | 1988816 ko | ExtractionOCaml/base_conversion.ml                        |   0m25.32s | 1988820 ko || +0m00.67s ||        -4 ko |   +2.68% |         -0.00%
  0m25.75s | 1956940 ko | ExtractionOCaml/saturated_solinas.ml                      |   0m25.70s | 1956860 ko || +0m00.05s ||        80 ko |   +0.19% |         +0.00%
  0m25.19s | 1166872 ko | PushButtonSynthesis/UnsaturatedSolinas.vo                 |   0m25.03s | 1166932 ko || +0m00.16s ||       -60 ko |   +0.63% |         -0.00%
  0m23.77s | 1375040 ko | Bedrock/End2End/RupicolaCrypto/Low.vo                     |   0m23.78s | 1375196 ko || -0m00.01s ||      -156 ko |   -0.04% |         -0.01%
  0m22.42s | 1138632 ko | PushButtonSynthesis/WordByWordMontgomery.vo               |   0m22.39s | 1138516 ko || +0m00.03s ||       116 ko |   +0.13% |         +0.01%
  0m19.45s | 1820840 ko | ExtractionOCaml/perf_unsaturated_solinas.ml               |   0m19.96s | 1820960 ko || -0m00.51s ||      -120 ko |   -2.55% |         -0.00%
  0m19.39s | 1152200 ko | Bedrock/Field/Translation/Proofs/Cmd.vo                   |   0m19.27s | 1152320 ko || +0m00.12s ||      -120 ko |   +0.62% |         -0.01%
  0m19.10s | 1121332 ko | Bedrock/Field/Translation/Proofs/Func.vo                  |   0m19.14s | 1121364 ko || -0m00.03s ||       -32 ko |   -0.20% |         -0.00%
  0m19.07s |   46832 ko | fiat-amd64/p224-mul.status                                |   0m19.32s |   46944 ko || -0m00.25s ||      -112 ko |   -1.29% |         -0.23%
  0m18.34s | 1196504 ko | Bedrock/Field/Synthesis/New/Signature.vo                  |   0m18.22s | 1196540 ko || +0m00.12s ||       -36 ko |   +0.65% |         -0.00%
  0m18.10s |   46980 ko | fiat-amd64/p224-square.status                             |   0m17.17s |   45956 ko || +0m00.92s ||      1024 ko |   +5.41% |         +2.22%
  0m17.85s | 1119980 ko | Bedrock/End2End/Poly1305/Field1305.vo                     |   0m17.94s | 1119912 ko || -0m00.08s ||        68 ko |   -0.50% |         +0.00%
  0m13.11s | 1027008 ko | BoundsPipeline.vo                                         |   0m13.31s | 1027120 ko || -0m00.20s ||      -112 ko |   -1.50% |         -0.01%
  0m11.77s | 1718472 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo       |   0m11.91s | 1718332 ko || -0m00.14s ||       140 ko |   -1.17% |         +0.00%
  0m10.95s | 1317672 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo      |   0m10.84s | 1317672 ko || +0m00.10s ||         0 ko |   +1.01% |         +0.00%
  0m09.81s | 1025496 ko | PushButtonSynthesis/BaseConversion.vo                     |   0m09.82s | 1025432 ko || -0m00.00s ||        64 ko |   -0.10% |         +0.00%
  0m09.01s |   40320 ko | fiat-amd64/p256-square.status                             |   0m08.73s |   38692 ko || +0m00.27s ||      1628 ko |   +3.20% |         +4.20%
  0m08.94s | 1036420 ko | PushButtonSynthesis/Primitives.vo                         |   0m08.86s | 1036424 ko || +0m00.08s ||        -4 ko |   +0.90% |         -0.00%
  0m08.75s |  996628 ko | PushButtonSynthesis/SmallExamples.vo                      |   0m08.76s |  996492 ko || -0m00.00s ||       136 ko |   -0.11% |         +0.01%
  0m07.62s | 1028808 ko | PushButtonSynthesis/SolinasReduction.vo                   |   0m07.65s | 1028920 ko || -0m00.03s ||      -112 ko |   -0.39% |         -0.01%
  0m06.58s | 1036084 ko | PushButtonSynthesis/BarrettReduction.vo                   |   0m06.56s | 1035952 ko || +0m00.02s ||       132 ko |   +0.30% |         +0.01%
  0m06.29s | 1084688 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo         |   0m06.24s | 1084704 ko || +0m00.04s ||       -16 ko |   +0.80% |         -0.00%
  0m06.15s | 1115844 ko | CLI.vo                                                    |   0m06.21s | 1116052 ko || -0m00.05s ||      -208 ko |   -0.96% |         -0.01%
  0m04.83s | 1058816 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo   |   0m04.85s | 1058816 ko || -0m00.01s ||         0 ko |   -0.41% |         +0.00%
  0m04.59s | 1030100 ko | PushButtonSynthesis/SaturatedSolinas.vo                   |   0m04.63s | 1029984 ko || -0m00.04s ||       116 ko |   -0.86% |         +0.01%
  0m03.96s | 1039660 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo           |   0m04.07s | 1039672 ko || -0m00.11s ||       -12 ko |   -2.70% |         -0.00%
  0m03.62s |  949392 ko | Assembly/Equivalence.vo                                   |   0m03.69s |  949320 ko || -0m00.06s ||        72 ko |   -1.89% |         +0.00%
  0m03.25s | 1004124 ko | Bedrock/Field/Translation/Cmd.vo                          |   0m03.32s | 1004056 ko || -0m00.06s ||        68 ko |   -2.10% |         +0.00%
  0m03.19s | 1001624 ko | Bedrock/Field/Translation/Func.vo                         |   0m03.07s | 1001804 ko || +0m00.12s ||      -180 ko |   +3.90% |         -0.01%
  0m03.17s | 1071332 ko | Rewriter/PerfTesting/Core.vo                              |   0m03.18s | 1071324 ko || -0m00.01s ||         8 ko |   -0.31% |         +0.00%
  0m02.94s | 1112208 ko | StandaloneHaskellMain.vo                                  |   0m02.87s | 1112204 ko || +0m00.06s ||         4 ko |   +2.43% |         +0.00%
  0m02.93s | 1138092 ko | Bedrock/Standalone/StandaloneHaskellMain.vo               |   0m02.92s | 1138104 ko || +0m00.01s ||       -12 ko |   +0.34% |         -0.00%
  0m02.92s | 1050604 ko | Bedrock/Field/Stringification/Stringification.vo          |   0m02.96s | 1050496 ko || -0m00.04s ||       108 ko |   -1.35% |         +0.01%
  0m02.90s | 1112868 ko | StandaloneOCamlMain.vo                                    |   0m02.90s | 1112708 ko || +0m00.00s ||       160 ko |   +0.00% |         +0.01%
  0m02.88s | 1119908 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo               |   0m02.64s | 1120020 ko || +0m00.23s ||      -112 ko |   +9.09% |         -0.00%
  0m02.84s | 1055540 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo  |   0m02.81s | 1055568 ko || +0m00.02s ||       -28 ko |   +1.06% |         -0.00%
  0m02.82s | 1138076 ko | Bedrock/Standalone/StandaloneOCamlMain.vo                 |   0m02.71s | 1138148 ko || +0m00.10s ||       -72 ko |   +4.05% |         -0.00%
  0m02.81s |   30932 ko | fiat-amd64/curve25519-mul.status                          |   0m02.76s |   30944 ko || +0m00.05s ||       -12 ko |   +1.81% |         -0.03%
  0m02.73s | 1062448 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo                 |   0m02.89s | 1062560 ko || -0m00.16s ||      -112 ko |   -5.53% |         -0.01%
  0m02.64s | 1042004 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo        |   0m02.61s | 1041752 ko || +0m00.03s ||       252 ko |   +1.14% |         +0.02%
  0m02.61s | 1037976 ko | Bedrock/Field/Translation/Parameters/Defaults.vo          |   0m02.60s | 1038084 ko || +0m00.00s ||      -108 ko |   +0.38% |         -0.01%
  0m02.61s | 1041780 ko | Bedrock/Field/Translation/Parameters/FE310.vo             |   0m02.61s | 1041952 ko || +0m00.00s ||      -172 ko |   +0.00% |         -0.01%
  0m02.59s | 1041976 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo        |   0m02.71s | 1042004 ko || -0m00.12s ||       -28 ko |   -4.42% |         -0.00%
  0m02.00s |   29380 ko | fiat-amd64/curve25519-square.status                       |   0m01.94s |   29828 ko || +0m00.06s ||      -448 ko |   +3.09% |         -1.50%
  0m00.92s |   25544 ko | fiat-amd64/poly1305-mul.status                            |   0m00.92s |   25720 ko || +0m00.00s ||      -176 ko |   +0.00% |         -0.68%
  0m00.81s |   25704 ko | fiat-amd64/poly1305-square.status                         |   0m00.79s |   25496 ko || +0m00.02s ||       208 ko |   +2.53% |         +0.81%
  0m00.58s |  119548 ko | ExtractionOCaml/base_conversion.cmi                       |   0m00.51s |  119480 ko || +0m00.06s ||        68 ko |  +13.72% |         +0.05%
  0m00.57s |  120004 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi          |   0m00.57s |  120036 ko || +0m00.00s ||       -32 ko |   +0.00% |         -0.02%
  0m00.57s |  123072 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi      |   0m00.57s |  123096 ko || +0m00.00s ||       -24 ko |   +0.00% |         -0.01%
  0m00.56s |  123140 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi |   0m00.52s |  123084 ko || +0m00.04s ||        56 ko |   +7.69% |         +0.04%
  0m00.55s |  122368 ko | ExtractionOCaml/bedrock2_base_conversion.cmi              |   0m00.55s |  122304 ko || +0m00.00s ||        64 ko |   +0.00% |         +0.05%
  0m00.54s |  122252 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi         |   0m00.54s |  122292 ko || +0m00.00s ||       -40 ko |   +0.00% |         -0.03%
  0m00.54s |  122424 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi       |   0m00.51s |  122648 ko || +0m00.03s ||      -224 ko |   +5.88% |         -0.18%
  0m00.54s |  119968 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi     |   0m00.54s |  120168 ko || +0m00.00s ||      -200 ko |   +0.00% |         -0.16%
  0m00.54s |  121308 ko | ExtractionOCaml/word_by_word_montgomery.cmi               |   0m00.56s |  121284 ko || -0m00.02s ||        24 ko |   -3.57% |         +0.01%
  0m00.53s |  122188 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi            |   0m00.55s |  122312 ko || -0m00.02s ||      -124 ko |   -3.63% |         -0.10%
  0m00.52s |  122696 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi            |   0m00.53s |  122364 ko || -0m00.01s ||       332 ko |   -1.88% |         +0.27%
  0m00.52s |  122568 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi       |   0m00.54s |  122660 ko || -0m00.02s ||       -92 ko |   -3.70% |         -0.07%
  0m00.51s |  120012 ko | ExtractionOCaml/solinas_reduction.cmi                     |   0m00.55s |  120128 ko || -0m00.04s ||      -116 ko |   -7.27% |         -0.09%
  0m00.51s |  121160 ko | ExtractionOCaml/unsaturated_solinas.cmi                   |   0m00.54s |  121324 ko || -0m00.03s ||      -164 ko |   -5.55% |         -0.13%
  0m00.50s |  120828 ko | ExtractionOCaml/saturated_solinas.cmi                     |   0m00.55s |  120584 ko || -0m00.05s ||       244 ko |   -9.09% |         +0.20%
  0m00.18s |   61076 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi          |   0m00.18s |   61168 ko || +0m00.00s ||       -92 ko |   +0.00% |         -0.15%
  0m00.16s |   61240 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi              |   0m00.19s |   61160 ko || -0m00.03s ||        80 ko |  -15.78% |         +0.13%
  0m00.06s |   20944 ko | fiat-amd64/p224-sub.status                                |   0m00.05s |   21032 ko || +0m00.00s ||       -88 ko |  +19.99% |         -0.41%

cc @OwenConoly

On top of #1508, #1509, #1510

[JasonGross]

This previously passed on the CI, so I am merging