ASM Equiv Checker: Include bounds info in dag

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>
mit-plv · Nov 13, 2022 · ab7fab8 · ab7fab8
1 parent 591c682
commit ab7fab8
Showing 1 changed file with 71 additions and 50 deletions.
diff --git a/src/Assembly/Symbolic.v b/src/Assembly/Symbolic.v
@@ -1045,13 +1045,15 @@ Existing Class node_ok.
 Hint Extern 1 (node_ok ?i ?n) => exact (@new_node_ok n I i) : typeclass_instances.
 Module Old.
 Module dag.
-  Definition t : Type := list (node idx * description).
+  Definition t : Type := list (node idx * description * option ZRange.zrange).
   Definition empty : t := nil.
   Definition size (d : t) : N := N.of_nat (List.length d).
   Definition lookup (d : t) (i : idx) : option (node idx)
-    := option_map fst (List.nth_error d (N.to_nat i)).
+    := option_map (fun '(n, _d, _b) => n) (List.nth_error d (N.to_nat i)).
+  Definition lookup_bounds (d : t) (i : idx) : option ZRange.zrange
+    := (n <- List.nth_error d (N.to_nat i); let '(_n, _d, b) := n in b)%option.
   Definition reverse_lookup (d : t) (i : node idx) : option idx
-    := option_map N.of_nat (List.indexof (fun '(n', _) => node_beq N.eqb i n') d).
+    := option_map N.of_nat (List.indexof (fun '(n', _, _) => node_beq N.eqb i n') d).
   Definition size_ok (d : t) : Prop
     := True.
   Definition all_nodes_ok (d : t) : Prop
@@ -1064,7 +1066,7 @@ Module dag.
     := match reverse_lookup d n with
        | Some i => (i, d)
        | None
-         => (size d, d ++ [(n, descr)])
+         => (size d, d ++ [(n, descr, bound_node_idx_via_PHOAS (lookup_bounds d) n)])
        end.
   Definition gensym (s:OperationSize) (d : t) : node idx
     := (old s (size d), []).
@@ -1081,7 +1083,7 @@ Module dag.
   Module eager.
     Definition t := list (idx * node idx * eager_description).
     Definition force (d : dag.t) : eager.t
-      := List.map (fun '(idx, (n, descr)) => (N.of_nat idx, n, force_description descr))
+      := List.map (fun '(idx, (n, descr, _)) => (N.of_nat idx, n, force_description descr))
                   (List.enumerate d).
     Definition description_lookup (d : eager.t) (descr : string) : list idx
       := List.map (fun '(idx, _, _) => idx) (List.filter (fun '(_, _, descr') => match get_eager_description_description descr' with Some descr' => String.eqb descr descr' | _ => false end) d).
@@ -1253,13 +1255,13 @@ Module dag.
     repeat apply conj; cbv [size empty size_ok]; intros *.
     all: rewrite ?lookup_merge_node, ?reverse_lookup_merge_node by assumption.
     all: let tac :=
-           repeat first [ progress cbv [ok size_ok size merge_node lookup reverse_lookup] in *
+           repeat first [ progress cbv [ok size_ok size merge_node lookup reverse_lookup lookup_bounds Crypto.Util.Option.bind] in *
                         | progress destruct_head'_and
                         | progress inversion_option
                         | progress subst
                         | exfalso; assumption
                         | progress inversion_pair
-                        | progress cbn [fst snd List.length] in *
+                        | progress cbn [fst snd List.length List.app] in *
                         | break_innermost_match_step
                         | progress intros
                         | progress destruct_head'_ex
@@ -1276,14 +1278,21 @@ Module dag.
                         | rewrite Nat2N.id in *
                         | rewrite N2Nat.id in *
                         | rewrite app_length
+                        | rewrite nth_error_app in *
                         | progress specialize_under_binders_by reflexivity
                         | progress specialize_under_binders_by rewrite Nat2N.id
                         | progress destruct_head'_prod
+                        | progress inversion_list
                         | match goal with
                           | [ H : forall i n, match nth_error _ (N.to_nat i) with _ => _ end = _ -> _ |- _ ]
                             => specialize (fun i => H (N.of_nat i))
                           | [ H : _ = Some _ |- _ ] => rewrite H in *
                           | [ H : N.of_nat _ = N.of_nat _ |- _ ] => apply (f_equal N.to_nat) in H
+                          | [ H : nth_error (_ :: _) _ = Some _ |- _ ]
+                            => apply nth_error_split in H
+                          | [ H : _ :: _ = ?x ++ _ |- _ ] => is_var x; destruct x
+                          | [ H : ?x ++ _ = nil |- _ ] => is_var x; destruct x
+                          | [ H : _ :: _ = _ :: _ |- _ ] => apply list_leq_to_eq in H; cbn [list_eq] in H
                           end
                         | solve [ exfalso; auto ] ] in
          tac;
@@ -1338,11 +1347,13 @@ Module dag.
   Module IdxMapProperties := FMapFacts.OrdProperties IdxMap <+ OrdProperties_RemoveHints IdxMap.
   Module NodeIdxMapProperties := FMapFacts.OrdProperties NodeIdxMap <+ OrdProperties_RemoveHints NodeIdxMap.
 
-  Definition t : Type := NodeIdxMap.t idx * IdxMap.t (node idx * description) * N (* size *).
+  Definition t : Type := NodeIdxMap.t idx * IdxMap.t (node idx * description * option ZRange.zrange) * N (* size *).
   Definition empty : t := (@NodeIdxMap.empty _, @IdxMap.empty _, 0%N).
   Definition size (d : t) : N := let '(_, _, sz) := d in sz.
   Definition lookup (d : t) (i : idx) : option (node idx)
-    := let '(_, d, _) := d in option_map (@fst _ _) (IdxMap.find i d).
+    := let '(_, d, _) := d in option_map (fun '(n, _, _) => n) (IdxMap.find i d).
+  Definition lookup_bounds (d : t) (i : idx) : option ZRange.zrange
+    := (let '(_, d, _) := d in n <- IdxMap.find i d; let '(_n, _d, b) := n in b)%option.
   Definition reverse_lookup (d : t) (i : node idx) : option idx
     := let '(d, _, _) := d in NodeIdxMap.find i d.
   Definition size_ok (d : t) : Prop
@@ -1359,8 +1370,9 @@ Module dag.
     := match reverse_lookup d n with
        | Some i => (i, d)
        | None
-         => let '(d, d', sz) := d in
-            (sz, (NodeIdxMap.add n sz d, IdxMap.add sz (n, descr) d', N.succ sz))
+         => let lookup_bounds := lookup_bounds d in
+            let '(d, d', sz) := d in
+            (sz, (NodeIdxMap.add n sz d, IdxMap.add sz (n, descr, bound_node_idx_via_PHOAS lookup_bounds n) d', N.succ sz))
        end.
   Definition gensym (s:OperationSize) (d : t) : node idx
     := (old s (size d), []).
@@ -1377,7 +1389,7 @@ Module dag.
   Module eager.
     Definition t := list (idx * node idx * eager_description).
     Definition force (d : dag.t) : eager.t
-      := List.map (fun '(idx, (n, descr)) => (idx, n, force_description descr))
+      := List.map (fun '(idx, (n, descr, _b)) => (idx, n, force_description descr))
                   (IdxMap.elements (let '(_, d, _) := d in d)).
     Definition description_lookup (d : eager.t) (descr : string) : list idx
       := List.map (fun '(idx, _, _) => idx) (List.filter (fun '(_, _, descr') => match get_eager_description_description descr' with Some descr' => String.eqb descr descr' | _ => false end) d).
@@ -1415,18 +1427,26 @@ Module dag.
                                                      else None
                                                 end.
   Proof.
-    cbv [dag.merge_node andb is_None lookup dag.ok size] in *;
-      repeat first [ assumption
-                   | reflexivity
-                   | lia
-                   | congruence
-                   | progress specialize_under_binders_by eassumption
-                   | progress subst
-                   | progress destruct_head'_and
-                   | progress reflect_hyps
-                   | progress cbn [fst snd option_map] in *
-                   | rewrite IdxMap.add_o
-                   | break_innermost_match_step ].
+    cbv [dag.merge_node andb is_None lookup dag.ok size option_map] in *;
+      let tac :=
+        repeat first [ assumption
+                     | reflexivity
+                     | lia
+                     | congruence
+                     | progress specialize_under_binders_by eassumption
+                     | progress subst
+                     | progress destruct_head'_and
+                     | progress destruct_head' iff
+                     | progress split_iff
+                     | progress break_innermost_match_hyps
+                     | progress specialize_by reflexivity
+                     | progress inversion_option
+                     | progress inversion_pair
+                     | progress reflect_hyps
+                     | progress cbn [fst snd option_map] in *
+                     | rewrite IdxMap.add_o
+                     | break_innermost_match_step ] in
+      tac; specialize_all_ways; tac.
   Qed.
 
   Lemma reverse_lookup_merge_node {d : t}
@@ -1536,32 +1556,33 @@ Module dag.
   Proof.
     repeat apply conj; cbv [size empty size_ok]; intros *.
     all: rewrite ?lookup_merge_node, ?reverse_lookup_merge_node by assumption.
-    all: repeat first [ progress cbv [ok size_ok size merge_node lookup reverse_lookup] in *
-                      | progress destruct_head'_and
-                      | progress inversion_option
-                      | progress subst
-                      | exfalso; assumption
-                      | progress inversion_pair
-                      | progress cbn [fst snd] in *
-                      | break_innermost_match_step
-                      | progress intros
-                      | progress reflect_hyps
-                      | progress split_iff
-                      | apply conj
-                      | rewrite NodeIdxMap.cardinal_add, NodeIdxMap.mem_find_b
-                      | rewrite IdxMap.cardinal_add, IdxMap.mem_find_b
-                      | rewrite N2Nat.inj_succ
-                      | lia
-                      | congruence
-                      | solve [ auto ]
-                      | match goal with
-                        | [ H : ?x = Some _ |- _ ] => rewrite H in *
-                        end
-                      | progress specialize_under_binders_by reflexivity
-                      | match goal with
-                        | [ H : _ |- _ ] => progress specialize_all_ways_under_binders_by exact H
-                        | [ H : _ |- _ ] => progress specialize_all_ways_under_binders_by rewrite H
-                        end ].
+    all: let tac :=
+           repeat first [ progress cbv [ok size_ok size merge_node lookup reverse_lookup option_map idx] in *
+                        | progress destruct_head'_and
+                        | progress inversion_option
+                        | progress subst
+                        | exfalso; assumption
+                        | progress inversion_pair
+                        | progress cbn [fst snd] in *
+                        | break_innermost_match_step
+                        | break_innermost_match_hyps_step
+                        | progress intros
+                        | progress reflect_hyps
+                        | progress split_iff
+                        | apply conj
+                        | rewrite NodeIdxMap.cardinal_add, NodeIdxMap.mem_find_b
+                        | rewrite IdxMap.cardinal_add, IdxMap.mem_find_b
+                        | rewrite N2Nat.inj_succ
+                        | lia
+                        | congruence
+                        | solve [ auto ]
+                        | match goal with
+                          | [ H : ?x = Some _ |- _ ] => rewrite H in *
+                          end
+                        | progress specialize_under_binders_by reflexivity ] in
+         tac;
+         specialize_all_ways;
+         tac.
   Qed.
   Global Instance merge_node_all_nodes_ok {descr:description} {n:node idx} {d : t} {dok : ok d} {dnok : all_nodes_ok d} {nok : node_ok (size d) n}
     : all_nodes_ok (snd (merge_node n d)) | 10.