ASM Equiv Checker: Include bounds info in dag #1503
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
We don't currently include any proofs about it, nor make use of it; this
is separated out so we can profile the overhead of including the bounds
info in the dag.
We will later make use of it for better bounds analysis.
<details><summary>Timing Diff</summary>
<p>
```
After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem)
----------------------------------------------------------------------------------------------------------------------------------------------------------------------
156m02.28s | 4384020 ko | Total Time / Peak Mem | 151m16.20s | 4383892 ko || +4m46.07s || 128 ko | +3.15% | +0.00%
----------------------------------------------------------------------------------------------------------------------------------------------------------------------
41m07.87s | 366784 ko | fiat-amd64/p434-square.status | 38m04.65s | 364792 ko || +3m03.21s || 1992 ko | +8.01% | +0.54%
45m27.88s | 386780 ko | fiat-amd64/p434-mul.status | 44m13.60s | 395392 ko || +1m14.28s || -8612 ko | +2.79% | -2.17%
1m35.88s | 71972 ko | fiat-amd64/p448-mul.status | 1m27.77s | 64632 ko || +0m08.10s || 7340 ko | +9.24% | +11.35%
4m16.24s | 108528 ko | fiat-amd64/p384-square.status | 4m10.77s | 98368 ko || +0m05.46s || 10160 ko | +2.18% | +10.32%
1m03.32s | 64012 ko | fiat-amd64/p521-mul.status | 0m57.82s | 57916 ko || +0m05.50s || 6096 ko | +9.51% | +10.52%
5m28.25s | 2724048 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo | 5m33.05s | 2724108 ko || -0m04.80s || -60 ko | -1.44% | -0.00%
0m46.03s | 1481256 ko | Assembly/Symbolic.vo | 0m42.21s | 1443380 ko || +0m03.82s || 37876 ko | +9.04% | +2.62%
0m35.46s | 54608 ko | fiat-amd64/p448-square.status | 0m32.92s | 49908 ko || +0m02.53s || 4700 ko | +7.71% | +9.41%
4m45.08s | 112572 ko | fiat-amd64/p384-mul.status | 4m43.44s | 105504 ko || +0m01.63s || 7068 ko | +0.57% | +6.69%
0m39.23s | 1781844 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas | 0m40.36s | 1785524 ko || -0m01.13s || -3680 ko | -2.79% | -0.20%
0m34.78s | 1415780 ko | ExtractionOCaml/saturated_solinas | 0m33.61s | 1415940 ko || +0m01.17s || -160 ko | +3.48% | -0.01%
0m31.39s | 2139376 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml | 0m30.33s | 2135516 ko || +0m01.06s || 3860 ko | +3.49% | +0.18%
0m14.38s | 44872 ko | fiat-amd64/p521-square.status | 0m12.54s | 42528 ko || +0m01.84s || 2344 ko | +14.67% | +5.51%
10m07.75s | 2587668 ko | Bedrock/End2End/X25519/GarageDoor.vo | 10m07.94s | 2587100 ko || -0m00.19s || 568 ko | -0.03% | +0.02%
4m11.52s | 2547128 ko | Assembly/WithBedrock/Proofs.vo | 4m11.92s | 2549096 ko || -0m00.39s || -1968 ko | -0.15% | -0.07%
1m53.67s | 1581240 ko | Bedrock/End2End/X25519/Field25519.vo | 1m53.63s | 1581240 ko || +0m00.04s || 0 ko | +0.03% | +0.00%
1m49.91s | 2203028 ko | Fancy/Barrett256.vo | 1m50.02s | 2203304 ko || -0m00.11s || -276 ko | -0.09% | -0.01%
1m38.44s | 1522168 ko | Assembly/EquivalenceProofs.vo | 1m38.41s | 1521464 ko || +0m00.03s || 704 ko | +0.03% | +0.04%
1m29.52s | 1999528 ko | SlowPrimeSynthesisExamples.vo | 1m29.35s | 1999408 ko || +0m00.17s || 120 ko | +0.19% | +0.00%
1m12.39s | 1434052 ko | Assembly/WithBedrock/SymbolicProofs.vo | 1m12.50s | 1435576 ko || -0m00.10s || -1524 ko | -0.15% | -0.10%
1m02.90s | 4384020 ko | Bedrock/End2End/RupicolaCrypto/Derive.vo | 1m02.76s | 4383892 ko || +0m00.14s || 128 ko | +0.22% | +0.00%
0m47.56s | 1722948 ko | Fancy/Montgomery256.vo | 0m47.68s | 1722952 ko || -0m00.11s || -4 ko | -0.25% | -0.00%
0m43.43s | 2148104 ko | ExtractionOCaml/bedrock2_solinas_reduction | 0m43.21s | 2147936 ko || +0m00.21s || 168 ko | +0.50% | +0.00%
0m42.68s | 2147880 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery | 0m42.21s | 2147768 ko || +0m00.46s || 112 ko | +1.11% | +0.00%
0m41.76s | 2147924 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery | 0m41.78s | 2147824 ko || -0m00.02s || 100 ko | -0.04% | +0.00%
0m40.91s | 2147792 ko | ExtractionOCaml/solinas_reduction | 0m40.80s | 2147960 ko || +0m00.10s || -168 ko | +0.26% | -0.00%
0m40.19s | 2147976 ko | ExtractionOCaml/word_by_word_montgomery | 0m40.10s | 2148000 ko || +0m00.08s || -24 ko | +0.22% | -0.00%
0m39.29s | 1781212 ko | ExtractionOCaml/bedrock2_unsaturated_solinas | 0m39.87s | 1785192 ko || -0m00.57s || -3980 ko | -1.45% | -0.22%
0m38.63s | 1264060 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m38.00s | 1263932 ko || +0m00.63s || 128 ko | +1.65% | +0.01%
0m38.31s | 1688512 ko | ExtractionOCaml/unsaturated_solinas | 0m38.43s | 1689896 ko || -0m00.11s || -1384 ko | -0.31% | -0.08%
0m37.64s | 1453604 ko | ExtractionOCaml/with_bedrock2_solinas_reduction | 0m37.27s | 1442408 ko || +0m00.36s || 11196 ko | +0.99% | +0.77%
0m37.44s | 1453592 ko | ExtractionOCaml/with_bedrock2_saturated_solinas | 0m37.71s | 1442644 ko || -0m00.27s || 10948 ko | -0.71% | +0.75%
0m37.36s | 1456160 ko | ExtractionOCaml/bedrock2_saturated_solinas | 0m37.16s | 1438460 ko || +0m00.20s || 17700 ko | +0.53% | +1.23%
0m36.76s | 1448492 ko | ExtractionOCaml/with_bedrock2_base_conversion | 0m36.47s | 1441664 ko || +0m00.28s || 6828 ko | +0.79% | +0.47%
0m36.10s | 1440664 ko | ExtractionOCaml/bedrock2_base_conversion | 0m36.04s | 1439332 ko || +0m00.06s || 1332 ko | +0.16% | +0.09%
0m34.57s | 2215472 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml | 0m34.52s | 2218740 ko || +0m00.04s || -3268 ko | +0.14% | -0.14%
0m34.47s | 2265764 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml | 0m35.30s | 2250948 ko || -0m00.82s || 14816 ko | -2.35% | +0.65%
0m34.45s | 2215408 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml | 0m34.22s | 2218680 ko || +0m00.23s || -3272 ko | +0.67% | -0.14%
0m34.17s | 2146396 ko | ExtractionOCaml/solinas_reduction.ml | 0m33.23s | 2147640 ko || +0m00.94s || -1244 ko | +2.82% | -0.05%
0m33.87s | 1415880 ko | ExtractionOCaml/base_conversion | 0m33.69s | 1415876 ko || +0m00.17s || 4 ko | +0.53% | +0.00%
0m33.29s | 2120132 ko | ExtractionOCaml/word_by_word_montgomery.ml | 0m33.21s | 2115884 ko || +0m00.07s || 4248 ko | +0.24% | +0.20%
0m32.20s | 1498896 ko | StandaloneDebuggingExamples.vo | 0m32.09s | 1498868 ko || +0m00.10s || 28 ko | +0.34% | +0.00%
0m31.53s | 2139332 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml | 0m31.58s | 2135512 ko || -0m00.04s || 3820 ko | -0.15% | +0.17%
0m29.89s | 2025700 ko | ExtractionOCaml/unsaturated_solinas.ml | 0m29.87s | 2025640 ko || +0m00.01s || 60 ko | +0.06% | +0.00%
0m29.11s | 1232348 ko | ExtractionOCaml/perf_word_by_word_montgomery | 0m28.90s | 1232180 ko || +0m00.21s || 168 ko | +0.72% | +0.01%
0m29.07s | 1232272 ko | ExtractionOCaml/perf_unsaturated_solinas | 0m28.65s | 1232380 ko || +0m00.42s || -108 ko | +1.46% | -0.00%
0m27.40s | 2022128 ko | ExtractionOCaml/bedrock2_base_conversion.ml | 0m27.20s | 2017236 ko || +0m00.19s || 4892 ko | +0.73% | +0.24%
0m27.28s | 2038088 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml | 0m27.43s | 2042012 ko || -0m00.14s || -3924 ko | -0.54% | -0.19%
0m27.18s | 2038456 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml | 0m27.37s | 2042048 ko || -0m00.19s || -3592 ko | -0.69% | -0.17%
0m26.47s | 2022468 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml | 0m27.44s | 2017308 ko || -0m00.97s || 5160 ko | -3.53% | +0.25%
0m26.33s | 2038284 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml | 0m27.18s | 2041980 ko || -0m00.85s || -3696 ko | -3.12% | -0.18%
0m26.06s | 1960584 ko | ExtractionOCaml/base_conversion.ml | 0m26.22s | 1955884 ko || -0m00.16s || 4700 ko | -0.61% | +0.24%
0m25.80s | 1942608 ko | ExtractionOCaml/saturated_solinas.ml | 0m25.78s | 1940092 ko || +0m00.01s || 2516 ko | +0.07% | +0.12%
0m25.03s | 1152652 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m24.40s | 1152568 ko || +0m00.63s || 84 ko | +2.58% | +0.00%
0m23.46s | 1353196 ko | Bedrock/End2End/RupicolaCrypto/Low.vo | 0m23.54s | 1353020 ko || -0m00.07s || 176 ko | -0.33% | +0.01%
0m22.30s | 1121196 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m22.31s | 1121276 ko || -0m00.00s || -80 ko | -0.04% | -0.00%
0m20.02s | 1787092 ko | ExtractionOCaml/perf_unsaturated_solinas.ml | 0m19.89s | 1787184 ko || +0m00.12s || -92 ko | +0.65% | -0.00%
0m19.89s | 1857136 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml | 0m19.21s | 1856540 ko || +0m00.67s || 596 ko | +3.53% | +0.03%
0m19.34s | 1136400 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m19.36s | 1136536 ko || -0m00.01s || -136 ko | -0.10% | -0.01%
0m19.27s | 44296 ko | fiat-amd64/p224-mul.status | 0m18.77s | 43656 ko || +0m00.50s || 640 ko | +2.66% | +1.46%
0m18.83s | 1104360 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m18.83s | 1104344 ko || +0m00.00s || 16 ko | +0.00% | +0.00%
0m18.18s | 44296 ko | fiat-amd64/secp256k1-mul.status | 0m17.61s | 42472 ko || +0m00.57s || 1824 ko | +3.23% | +4.29%
0m18.10s | 1178664 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m18.05s | 1178644 ko || +0m00.05s || 20 ko | +0.27% | +0.00%
0m17.74s | 1106284 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m17.81s | 1106288 ko || -0m00.07s || -4 ko | -0.39% | -0.00%
0m17.67s | 45268 ko | fiat-amd64/p224-square.status | 0m16.74s | 43408 ko || +0m00.93s || 1860 ko | +5.55% | +4.28%
0m16.47s | 46600 ko | fiat-amd64/secp256k1-square.status | 0m16.43s | 42572 ko || +0m00.03s || 4028 ko | +0.24% | +9.46%
0m13.12s | 1011584 ko | BoundsPipeline.vo | 0m13.16s | 1011664 ko || -0m00.04s || -80 ko | -0.30% | -0.00%
0m11.82s | 1631984 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo | 0m11.48s | 1631832 ko || +0m00.33s || 152 ko | +2.96% | +0.00%
0m10.81s | 1301960 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo | 0m10.81s | 1302004 ko || +0m00.00s || -44 ko | +0.00% | -0.00%
0m09.75s | 1008864 ko | PushButtonSynthesis/BaseConversion.vo | 0m09.83s | 1008872 ko || -0m00.08s || -8 ko | -0.81% | -0.00%
0m08.87s | 1019208 ko | PushButtonSynthesis/Primitives.vo | 0m08.99s | 1019152 ko || -0m00.12s || 56 ko | -1.33% | +0.00%
0m08.74s | 40096 ko | fiat-amd64/p256-square.status | 0m08.73s | 37420 ko || +0m00.00s || 2676 ko | +0.11% | +7.15%
0m08.72s | 979960 ko | PushButtonSynthesis/SmallExamples.vo | 0m08.63s | 980060 ko || +0m00.08s || -100 ko | +1.04% | -0.01%
0m07.57s | 1012444 ko | PushButtonSynthesis/SolinasReduction.vo | 0m07.56s | 1012504 ko || +0m00.01s || -60 ko | +0.13% | -0.00%
0m06.66s | 1019696 ko | PushButtonSynthesis/BarrettReduction.vo | 0m06.57s | 1019736 ko || +0m00.08s || -40 ko | +1.36% | -0.00%
0m06.19s | 1101260 ko | CLI.vo | 0m06.23s | 1101232 ko || -0m00.04s || 28 ko | -0.64% | +0.00%
0m06.13s | 1070748 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m06.20s | 1070756 ko || -0m00.07s || -8 ko | -1.12% | -0.00%
0m04.78s | 1041852 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m04.73s | 1041844 ko || +0m00.04s || 8 ko | +1.05% | +0.00%
0m04.58s | 1013376 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m04.65s | 1013532 ko || -0m00.07s || -156 ko | -1.50% | -0.01%
0m04.06s | 1023272 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m04.12s | 1023304 ko || -0m00.06s || -32 ko | -1.45% | -0.00%
0m03.66s | 934996 ko | Assembly/Equivalence.vo | 0m03.62s | 934952 ko || +0m00.04s || 44 ko | +1.10% | +0.00%
0m03.24s | 986816 ko | Bedrock/Field/Translation/Cmd.vo | 0m03.18s | 986872 ko || +0m00.06s || -56 ko | +1.88% | -0.00%
0m03.08s | 984380 ko | Bedrock/Field/Translation/Func.vo | 0m03.07s | 984444 ko || +0m00.01s || -64 ko | +0.32% | -0.00%
0m03.04s | 1053768 ko | Rewriter/PerfTesting/Core.vo | 0m03.20s | 1053896 ko || -0m00.16s || -128 ko | -5.00% | -0.01%
0m02.95s | 1093448 ko | StandaloneHaskellMain.vo | 0m02.88s | 1093384 ko || +0m00.07s || 64 ko | +2.43% | +0.00%
0m02.92s | 1094072 ko | StandaloneOCamlMain.vo | 0m02.93s | 1094124 ko || -0m00.01s || -52 ko | -0.34% | -0.00%
0m02.89s | 1033576 ko | Bedrock/Field/Stringification/Stringification.vo | 0m03.05s | 1033600 ko || -0m00.15s || -24 ko | -5.24% | -0.00%
0m02.86s | 1038656 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m02.86s | 1038732 ko || +0m00.00s || -76 ko | +0.00% | -0.00%
0m02.85s | 1119740 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m02.86s | 1119644 ko || -0m00.00s || 96 ko | -0.34% | +0.00%
0m02.80s | 1101876 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.72s | 1101856 ko || +0m00.07s || 20 ko | +2.94% | +0.00%
0m02.76s | 30964 ko | fiat-amd64/curve25519-mul.status | 0m02.79s | 31100 ko || -0m00.03s || -136 ko | -1.07% | -0.43%
0m02.73s | 1045276 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m02.84s | 1045332 ko || -0m00.10s || -56 ko | -3.87% | -0.00%
0m02.70s | 1024436 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m02.71s | 1024372 ko || -0m00.00s || 64 ko | -0.36% | +0.00%
0m02.68s | 1024592 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m02.62s | 1024508 ko || +0m00.06s || 84 ko | +2.29% | +0.00%
0m02.66s | 1024640 ko | Bedrock/Field/Translation/Parameters/FE310.vo | 0m02.58s | 1024624 ko || +0m00.08s || 16 ko | +3.10% | +0.00%
0m02.64s | 1119820 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m02.81s | 1119776 ko || -0m00.16s || 44 ko | -6.04% | +0.00%
0m02.50s | 1020652 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m02.55s | 1020528 ko || -0m00.04s || 124 ko | -1.96% | +0.01%
0m02.02s | 29772 ko | fiat-amd64/curve25519-square.status | 0m01.94s | 29392 ko || +0m00.08s || 380 ko | +4.12% | +1.29%
0m00.96s | 25592 ko | fiat-amd64/poly1305-mul.status | 0m00.95s | 25564 ko || +0m00.01s || 28 ko | +1.05% | +0.10%
0m00.76s | 25568 ko | fiat-amd64/poly1305-square.status | 0m00.77s | 24416 ko || -0m00.01s || 1152 ko | -1.29% | +4.71%
0m00.57s | 118752 ko | ExtractionOCaml/base_conversion.cmi | 0m00.56s | 119364 ko || +0m00.00s || -612 ko | +1.78% | -0.51%
0m00.57s | 121884 ko | ExtractionOCaml/unsaturated_solinas.cmi | 0m00.54s | 121824 ko || +0m00.02s || 60 ko | +5.55% | +0.04%
0m00.56s | 122760 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi | 0m00.55s | 122828 ko || +0m00.01s || -68 ko | +1.81% | -0.05%
0m00.56s | 121480 ko | ExtractionOCaml/word_by_word_montgomery.cmi | 0m00.53s | 121696 ko || +0m00.03s || -216 ko | +5.66% | -0.17%
0m00.54s | 123112 ko | ExtractionOCaml/bedrock2_base_conversion.cmi | 0m00.51s | 122620 ko || +0m00.03s || 492 ko | +5.88% | +0.40%
0m00.54s | 122940 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi | 0m00.55s | 123224 ko || -0m00.01s || -284 ko | -1.81% | -0.23%
0m00.54s | 120212 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi | 0m00.52s | 119948 ko || +0m00.02s || 264 ko | +3.84% | +0.22%
0m00.53s | 122796 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi | 0m00.51s | 122960 ko || +0m00.02s || -164 ko | +3.92% | -0.13%
0m00.53s | 120340 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi | 0m00.58s | 119876 ko || -0m00.04s || 464 ko | -8.62% | +0.38%
0m00.52s | 123000 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi | 0m00.55s | 123188 ko || -0m00.03s || -188 ko | -5.45% | -0.15%
0m00.52s | 120444 ko | ExtractionOCaml/saturated_solinas.cmi | 0m00.52s | 118920 ko || +0m00.00s || 1524 ko | +0.00% | +1.28%
0m00.51s | 120484 ko | ExtractionOCaml/solinas_reduction.cmi | 0m00.51s | 120456 ko || +0m00.00s || 28 ko | +0.00% | +0.02%
0m00.51s | 122968 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi | 0m00.54s | 122840 ko || -0m00.03s || 128 ko | -5.55% | +0.10%
0m00.50s | 123048 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi | 0m00.55s | 123248 ko || -0m00.05s || -200 ko | -9.09% | -0.16%
0m00.49s | 122876 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi | 0m00.54s | 123100 ko || -0m00.05s || -224 ko | -9.25% | -0.18%
0m00.18s | 61020 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi | 0m00.14s | 61068 ko || +0m00.03s || -48 ko | +28.57% | -0.07%
0m00.17s | 61228 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi | 0m00.17s | 61068 ko || +0m00.00s || 160 ko | +0.00% | +0.26%
0m00.05s | 21296 ko | fiat-amd64/p224-sub.status | 0m00.05s | 20896 ko || +0m00.00s || 400 ko | +0.00% | +1.91%
```
</p>
</details>
JasonGross
force-pushed
the
asm-bounds-in-dag
branch
from
0f927f0
to
ab7fab8
Compare
|
The timing is a bit unfortunate, but I think it's a price we have to pay. On the upside, this means that optimizing bounds analysis (I'm thinking of special-casing the lower bound of 0 in particular) will pay off even more. |
Rayyy369
reviewed
Nov 14, 2022
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We don't currently include any proofs about it, nor make use of it; this is separated out so we can profile the overhead of including the bounds info in the dag.
We will later make use of it for better bounds analysis.
Timing Diff
(cc @OwenConoly )