Enable CLI control of equiv checker rewrite passes

<details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------- 151m22.97s | 4384052 ko | Total Time / Peak Mem | 151m25.18s | 4380836 ko || -0m02.20s || 3216 ko | -0.02% | +0.07% ---------------------------------------------------------------------------------------------------------------------------------------------------------------------- 39m12.08s | 364876 ko | fiat-amd64/p434-square.status | 41m17.38s | 359984 ko || -2m05.30s || 4892 ko | -5.05% | +1.35% 43m07.34s | 396684 ko | fiat-amd64/p434-mul.status | 41m14.78s | 385732 ko || +1m52.55s || 10952 ko | +4.54% | +2.83% 4m13.67s | 98344 ko | fiat-amd64/p384-square.status | 4m22.45s | 96620 ko || -0m08.78s || 1724 ko | -3.34% | +1.78% 1m26.71s | 64576 ko | fiat-amd64/p448-mul.status | 1m21.39s | 65472 ko || +0m05.32s || -896 ko | +6.53% | -1.36% 4m14.88s | 2554932 ko | Assembly/WithBedrock/Proofs.vo | 4m11.08s | 2555764 ko || +0m03.79s || -832 ko | +1.51% | -0.03% 1m38.28s | 1521596 ko | Assembly/EquivalenceProofs.vo | 1m35.28s | 1509416 ko || +0m03.00s || 12180 ko | +3.14% | +0.80% 0m29.01s | 49924 ko | fiat-amd64/p448-square.status | 0m32.35s | 50224 ko || -0m03.33s || -300 ko | -10.32% | -0.59% 4m41.93s | 105612 ko | fiat-amd64/p384-mul.status | 4m39.42s | 106152 ko || +0m02.50s || -540 ko | +0.89% | -0.50% 0m57.65s | 57836 ko | fiat-amd64/p521-mul.status | 0m59.01s | 57884 ko || -0m01.35s || -48 ko | -2.30% | -0.08% 0m41.68s | 1451856 ko | Assembly/Symbolic.vo | 0m40.56s | 1402828 ko || +0m01.11s || 49028 ko | +2.76% | +3.49% 0m41.01s | 1785580 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas | 0m39.27s | 1772956 ko || +0m01.73s || 12624 ko | +4.43% | +0.71% 0m40.93s | 2147868 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery | 0m41.98s | 2147808 ko || -0m01.04s || 60 ko | -2.50% | +0.00% 0m40.23s | 2147884 ko | ExtractionOCaml/word_by_word_montgomery | 0m39.13s | 2004364 ko || +0m01.09s || 143520 ko | +2.81% | +7.16% 0m32.45s | 1499668 ko | StandaloneDebuggingExamples.vo | 0m30.71s | 1491140 ko || +0m01.74s || 8528 ko | +5.66% | +0.57% 0m06.28s | 1101420 ko | CLI.vo | 0m04.99s | 1093984 ko || +0m01.29s || 7436 ko | +25.85% | +0.67% 10m08.33s | 2587612 ko | Bedrock/End2End/X25519/GarageDoor.vo | 10m08.47s | 2587172 ko || -0m00.13s || 440 ko | -0.02% | +0.01% 5m33.90s | 2724280 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo | 5m34.57s | 2689860 ko || -0m00.67s || 34420 ko | -0.20% | +1.27% 1m53.00s | 1581340 ko | Bedrock/End2End/X25519/Field25519.vo | 1m53.03s | 1578804 ko || -0m00.03s || 2536 ko | -0.02% | +0.16% 1m49.48s | 2203552 ko | Fancy/Barrett256.vo | 1m49.70s | 2219448 ko || -0m00.22s || -15896 ko | -0.20% | -0.71% 1m29.30s | 2000076 ko | SlowPrimeSynthesisExamples.vo | 1m29.64s | 1996156 ko || -0m00.34s || 3920 ko | -0.37% | +0.19% 1m12.36s | 1433096 ko | Assembly/WithBedrock/SymbolicProofs.vo | 1m11.56s | 1424368 ko || +0m00.79s || 8728 ko | +1.11% | +0.61% 1m02.97s | 4384052 ko | Bedrock/End2End/RupicolaCrypto/Derive.vo | 1m03.27s | 4380836 ko || -0m00.30s || 3216 ko | -0.47% | +0.07% 0m47.63s | 1722840 ko | Fancy/Montgomery256.vo | 0m47.57s | 1722892 ko || +0m00.06s || -52 ko | +0.12% | -0.00% 0m44.01s | 2147928 ko | ExtractionOCaml/bedrock2_solinas_reduction | 0m43.54s | 2147860 ko || +0m00.46s || 68 ko | +1.07% | +0.00% 0m42.33s | 2147748 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery | 0m42.07s | 2147848 ko || +0m00.25s || -100 ko | +0.61% | -0.00% 0m41.29s | 2147864 ko | ExtractionOCaml/solinas_reduction | 0m40.86s | 2147544 ko || +0m00.42s || 320 ko | +1.05% | +0.01% 0m40.09s | 1784984 ko | ExtractionOCaml/bedrock2_unsaturated_solinas | 0m40.08s | 1773536 ko || +0m00.01s || 11448 ko | +0.02% | +0.64% 0m38.12s | 1263824 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m37.83s | 1262776 ko || +0m00.28s || 1048 ko | +0.76% | +0.08% 0m37.64s | 1689044 ko | ExtractionOCaml/unsaturated_solinas | 0m37.21s | 1706524 ko || +0m00.42s || -17480 ko | +1.15% | -1.02% 0m37.39s | 1452272 ko | ExtractionOCaml/bedrock2_saturated_solinas | 0m37.02s | 1453464 ko || +0m00.36s || -1192 ko | +0.99% | -0.08% 0m37.36s | 1442016 ko | ExtractionOCaml/with_bedrock2_saturated_solinas | 0m36.54s | 1464612 ko || +0m00.82s || -22596 ko | +2.24% | -1.54% 0m37.31s | 1441836 ko | ExtractionOCaml/with_bedrock2_solinas_reduction | 0m36.59s | 1464708 ko || +0m00.71s || -22872 ko | +1.96% | -1.56% 0m36.47s | 1440776 ko | ExtractionOCaml/with_bedrock2_base_conversion | 0m36.54s | 1441748 ko || -0m00.07s || -972 ko | -0.19% | -0.06% 0m35.67s | 1438816 ko | ExtractionOCaml/bedrock2_base_conversion | 0m36.48s | 1441844 ko || -0m00.80s || -3028 ko | -2.22% | -0.21% 0m35.41s | 2252448 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml | 0m35.17s | 2235808 ko || +0m00.23s || 16640 ko | +0.68% | +0.74% 0m34.53s | 2218740 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml | 0m34.40s | 2197352 ko || +0m00.13s || 21388 ko | +0.37% | +0.97% 0m34.45s | 2218700 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml | 0m34.35s | 2197268 ko || +0m00.10s || 21432 ko | +0.29% | +0.97% 0m34.17s | 2147684 ko | ExtractionOCaml/solinas_reduction.ml | 0m34.27s | 2116996 ko || -0m00.10s || 30688 ko | -0.29% | +1.44% 0m33.90s | 1415940 ko | ExtractionOCaml/base_conversion | 0m33.69s | 1415780 ko || +0m00.21s || 160 ko | +0.62% | +0.01% 0m33.48s | 1415872 ko | ExtractionOCaml/saturated_solinas | 0m34.46s | 1415848 ko || -0m00.98s || 24 ko | -2.84% | +0.00% 0m33.36s | 2115648 ko | ExtractionOCaml/word_by_word_montgomery.ml | 0m33.21s | 2077176 ko || +0m00.14s || 38472 ko | +0.45% | +1.85% 0m31.66s | 2135620 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml | 0m31.36s | 2104392 ko || +0m00.30s || 31228 ko | +0.95% | +1.48% 0m31.26s | 2135580 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml | 0m31.42s | 2104200 ko || -0m00.16s || 31380 ko | -0.50% | +1.49% 0m30.15s | 2025768 ko | ExtractionOCaml/unsaturated_solinas.ml | 0m29.84s | 2011636 ko || +0m00.30s || 14132 ko | +1.03% | +0.70% 0m28.94s | 1232124 ko | ExtractionOCaml/perf_word_by_word_montgomery | 0m29.08s | 1232268 ko || -0m00.13s || -144 ko | -0.48% | -0.01% 0m28.81s | 1232212 ko | ExtractionOCaml/perf_unsaturated_solinas | 0m28.64s | 1232288 ko || +0m00.16s || -76 ko | +0.59% | -0.00% 0m27.43s | 2042592 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml | 0m27.11s | 2000996 ko || +0m00.32s || 41596 ko | +1.18% | +2.07% 0m27.35s | 2042508 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml | 0m26.59s | 2000880 ko || +0m00.76s || 41628 ko | +2.85% | +2.08% 0m27.23s | 2042508 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml | 0m27.16s | 2000916 ko || +0m00.07s || 41592 ko | +0.25% | +2.07% 0m27.15s | 2017348 ko | ExtractionOCaml/bedrock2_base_conversion.ml | 0m27.32s | 2004784 ko || -0m00.17s || 12564 ko | -0.62% | +0.62% 0m26.58s | 1955212 ko | ExtractionOCaml/base_conversion.ml | 0m25.93s | 1905052 ko || +0m00.64s || 50160 ko | +2.50% | +2.63% 0m26.52s | 2017372 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml | 0m27.11s | 2004944 ko || -0m00.58s || 12428 ko | -2.17% | +0.61% 0m26.32s | 1940208 ko | ExtractionOCaml/saturated_solinas.ml | 0m25.48s | 1891352 ko || +0m00.83s || 48856 ko | +3.29% | +2.58% 0m25.12s | 1150580 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m25.10s | 1147720 ko || +0m00.01s || 2860 ko | +0.07% | +0.24% 0m23.69s | 1353132 ko | Bedrock/End2End/RupicolaCrypto/Low.vo | 0m23.62s | 1358036 ko || +0m00.07s || -4904 ko | +0.29% | -0.36% 0m22.18s | 1121336 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m22.31s | 1117916 ko || -0m00.12s || 3420 ko | -0.58% | +0.30% 0m19.88s | 1786664 ko | ExtractionOCaml/perf_unsaturated_solinas.ml | 0m20.26s | 1780872 ko || -0m00.38s || 5792 ko | -1.87% | +0.32% 0m19.88s | 1857548 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml | 0m19.90s | 1849472 ko || -0m00.01s || 8076 ko | -0.10% | +0.43% 0m19.46s | 1136688 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m19.20s | 1129064 ko || +0m00.26s || 7624 ko | +1.35% | +0.67% 0m19.11s | 1104372 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m18.86s | 1101216 ko || +0m00.25s || 3156 ko | +1.32% | +0.28% 0m18.47s | 43728 ko | fiat-amd64/p224-mul.status | 0m18.95s | 42268 ko || -0m00.48s || 1460 ko | -2.53% | +3.45% 0m18.34s | 42392 ko | fiat-amd64/secp256k1-mul.status | 0m18.11s | 42552 ko || +0m00.23s || -160 ko | +1.27% | -0.37% 0m18.11s | 1178648 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m18.03s | 1175728 ko || +0m00.07s || 2920 ko | +0.44% | +0.24% 0m17.76s | 1106232 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m17.78s | 1103516 ko || -0m00.01s || 2716 ko | -0.11% | +0.24% 0m16.91s | 43376 ko | fiat-amd64/p224-square.status | 0m17.41s | 44016 ko || -0m00.50s || -640 ko | -2.87% | -1.45% 0m16.12s | 42516 ko | fiat-amd64/secp256k1-square.status | 0m16.78s | 43240 ko || -0m00.66s || -724 ko | -3.93% | -1.67% 0m13.03s | 1010964 ko | BoundsPipeline.vo | 0m12.85s | 1008152 ko || +0m00.17s || 2812 ko | +1.40% | +0.27% 0m12.70s | 42424 ko | fiat-amd64/p521-square.status | 0m13.55s | 42228 ko || -0m00.85s || 196 ko | -6.27% | +0.46% 0m11.75s | 1631776 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo | 0m11.49s | 1629496 ko || +0m00.25s || 2280 ko | +2.26% | +0.13% 0m10.86s | 1301816 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo | 0m10.87s | 1297796 ko || -0m00.00s || 4020 ko | -0.09% | +0.30% 0m09.80s | 1008988 ko | PushButtonSynthesis/BaseConversion.vo | 0m09.78s | 1004916 ko || +0m00.02s || 4072 ko | +0.20% | +0.40% 0m08.89s | 1018900 ko | PushButtonSynthesis/Primitives.vo | 0m08.84s | 1017008 ko || +0m00.05s || 1892 ko | +0.56% | +0.18% 0m08.83s | 37568 ko | fiat-amd64/p256-square.status | 0m08.75s | 37640 ko || +0m00.08s || -72 ko | +0.91% | -0.19% 0m08.72s | 979868 ko | PushButtonSynthesis/SmallExamples.vo | 0m08.66s | 976988 ko || +0m00.06s || 2880 ko | +0.69% | +0.29% 0m07.54s | 1012504 ko | PushButtonSynthesis/SolinasReduction.vo | 0m07.41s | 1008696 ko || +0m00.12s || 3808 ko | +1.75% | +0.37% 0m06.58s | 1019768 ko | PushButtonSynthesis/BarrettReduction.vo | 0m06.52s | 1016180 ko || +0m00.06s || 3588 ko | +0.92% | +0.35% 0m06.17s | 1070672 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m06.28s | 1066672 ko || -0m00.11s || 4000 ko | -1.75% | +0.37% 0m04.81s | 1041804 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m04.76s | 1038764 ko || +0m00.04s || 3040 ko | +1.05% | +0.29% 0m04.57s | 1013536 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m04.61s | 1010376 ko || -0m00.04s || 3160 ko | -0.86% | +0.31% 0m04.15s | 1023232 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m04.03s | 1019884 ko || +0m00.12s || 3348 ko | +2.97% | +0.32% 0m03.61s | 935080 ko | Assembly/Equivalence.vo | 0m03.66s | 931548 ko || -0m00.05s || 3532 ko | -1.36% | +0.37% 0m03.27s | 986976 ko | Bedrock/Field/Translation/Cmd.vo | 0m03.28s | 984052 ko || -0m00.00s || 2924 ko | -0.30% | +0.29% 0m03.26s | 1053776 ko | Rewriter/PerfTesting/Core.vo | 0m03.15s | 1051868 ko || +0m00.10s || 1908 ko | +3.49% | +0.18% 0m03.10s | 984352 ko | Bedrock/Field/Translation/Func.vo | 0m03.05s | 981424 ko || +0m00.05s || 2928 ko | +1.63% | +0.29% 0m03.06s | 1033576 ko | Bedrock/Field/Stringification/Stringification.vo | 0m02.88s | 1030400 ko || +0m00.18s || 3176 ko | +6.25% | +0.30% 0m03.00s | 1094052 ko | StandaloneOCamlMain.vo | 0m02.92s | 1090924 ko || +0m00.08s || 3128 ko | +2.73% | +0.28% 0m02.93s | 1101772 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.92s | 1098692 ko || +0m00.01s || 3080 ko | +0.34% | +0.28% 0m02.91s | 1119604 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m02.92s | 1116356 ko || -0m00.00s || 3248 ko | -0.34% | +0.29% 0m02.89s | 1093556 ko | StandaloneHaskellMain.vo | 0m02.73s | 1090128 ko || +0m00.16s || 3428 ko | +5.86% | +0.31% 0m02.84s | 1038616 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m02.82s | 1035400 ko || +0m00.02s || 3216 ko | +0.70% | +0.31% 0m02.83s | 1045360 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m02.81s | 1042460 ko || +0m00.02s || 2900 ko | +0.71% | +0.27% 0m02.76s | 31332 ko | fiat-amd64/curve25519-mul.status | 0m02.67s | 29664 ko || +0m00.08s || 1668 ko | +3.37% | +5.62% 0m02.64s | 1119876 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m02.68s | 1116548 ko || -0m00.04s || 3328 ko | -1.49% | +0.29% 0m02.63s | 1024664 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m02.66s | 1021800 ko || -0m00.03s || 2864 ko | -1.12% | +0.28% 0m02.61s | 1024452 ko | Bedrock/Field/Translation/Parameters/FE310.vo | 0m02.58s | 1021620 ko || +0m00.02s || 2832 ko | +1.16% | +0.27% 0m02.58s | 1024580 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m02.59s | 1021812 ko || -0m00.00s || 2768 ko | -0.38% | +0.27% 0m02.53s | 1020596 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m02.52s | 1017580 ko || +0m00.00s || 3016 ko | +0.39% | +0.29% 0m01.95s | 29080 ko | fiat-amd64/curve25519-square.status | 0m01.85s | 28976 ko || +0m00.09s || 104 ko | +5.40% | +0.35% 0m00.93s | 25328 ko | fiat-amd64/poly1305-mul.status | 0m00.91s | 25408 ko || +0m00.02s || -80 ko | +2.19% | -0.31% 0m00.78s | 24476 ko | fiat-amd64/poly1305-square.status | 0m00.75s | 24620 ko || +0m00.03s || -144 ko | +4.00% | -0.58% 0m00.57s | 121888 ko | ExtractionOCaml/unsaturated_solinas.cmi | 0m00.57s | 120588 ko || +0m00.00s || 1300 ko | +0.00% | +1.07% 0m00.57s | 122972 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi | 0m00.53s | 121192 ko || +0m00.03s || 1780 ko | +7.54% | +1.46% 0m00.57s | 500000 ko | Util/Strings/ParseFlagOptions.vo | 0m00.58s | 500096 ko || -0m00.01s || -96 ko | -1.72% | -0.01% 0m00.55s | 119452 ko | ExtractionOCaml/base_conversion.cmi | 0m00.54s | 119720 ko || +0m00.01s || -268 ko | +1.85% | -0.22% 0m00.55s | 120464 ko | ExtractionOCaml/solinas_reduction.cmi | 0m00.52s | 119420 ko || +0m00.03s || 1044 ko | +5.76% | +0.87% 0m00.54s | 119856 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi | 0m00.56s | 122760 ko || -0m00.02s || -2904 ko | -3.57% | -2.36% 0m00.54s | 122928 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi | 0m00.56s | 121116 ko || -0m00.02s || 1812 ko | -3.57% | +1.49% 0m00.54s | 123428 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi | 0m00.53s | 120500 ko || +0m00.01s || 2928 ko | +1.88% | +2.42% 0m00.53s | 119860 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi | 0m00.53s | 122836 ko || +0m00.00s || -2976 ko | +0.00% | -2.42% 0m00.52s | 122624 ko | ExtractionOCaml/bedrock2_base_conversion.cmi | 0m00.56s | 122872 ko || -0m00.04s || -248 ko | -7.14% | -0.20% 0m00.52s | 122736 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi | 0m00.55s | 123000 ko || -0m00.03s || -264 ko | -5.45% | -0.21% 0m00.52s | 119132 ko | ExtractionOCaml/saturated_solinas.cmi | 0m00.56s | 119320 ko || -0m00.04s || -188 ko | -7.14% | -0.15% 0m00.52s | 122844 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi | 0m00.53s | 122828 ko || -0m00.01s || 16 ko | -1.88% | +0.01% 0m00.52s | 120712 ko | ExtractionOCaml/word_by_word_montgomery.cmi | 0m00.58s | 120176 ko || -0m00.05s || 536 ko | -10.34% | +0.44% 0m00.51s | 123036 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi | 0m00.53s | 121340 ko || -0m00.02s || 1696 ko | -3.77% | +1.39% 0m00.49s | 123356 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi | 0m00.56s | 120700 ko || -0m00.07s || 2656 ko | -12.50% | +2.20% 0m00.18s | 61204 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi | 0m00.15s | 60996 ko || +0m00.03s || 208 ko | +20.00% | +0.34% 0m00.17s | 61144 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi | 0m00.18s | 61152 ko || -0m00.00s || -8 ko | -5.55% | -0.01% 0m00.05s | 21032 ko | fiat-amd64/p224-sub.status | 0m00.07s | 20776 ko || -0m00.02s || 256 ko | -28.57% | +1.23% ``` </p> </details>
mit-plv · Nov 12, 2022 · 3e4894a · 3e4894a
1 parent bedfdc6
commit 3e4894a
Show file tree

Hide file tree

Showing 8 changed files with 456 additions and 163 deletions.
diff --git a/src/Assembly/Equivalence.v b/src/Assembly/Equivalence.v
@@ -131,23 +131,29 @@ Definition default_assembly_conventions : assembly_conventions_opt
      |}.
 
 Module Export Options.
+  Export Assembly.Symbolic.Options.
   Class equivalence_checker_options_opt :=
     { assembly_conventions_ : assembly_conventions_opt
+    ; symbolic_options_ : symbolic_options_opt
     }.
   Definition default_equivalence_checker_options : equivalence_checker_options_opt
     := {| assembly_conventions_ := default_assembly_conventions
+       ; symbolic_options_ := default_symbolic_options
        |}.
 End Options.
 
 Module Export EquivalenceCheckerHints.
+  Export Assembly.Symbolic.Hints.
   Global Existing Instances
    Build_equivalence_checker_options_opt
    assembly_conventions_
+   symbolic_options_
   .
   #[global]
    Hint Cut [
       ( _ * )
         (assembly_conventions_
+        | symbolic_options_
         ) ( _ * )
         (Build_equivalence_checker_options_opt
         )
@@ -709,7 +715,7 @@ Global Instance show_EquivalenceCheckingError : Show EquivalenceCheckingError
 Definition merge_fresh_symbol {descr:description} : dag.M idx := fun d => merge_node (dag.gensym 64%N d) d.
 Definition merge_literal {descr:description} (l:Z) : dag.M idx := merge_node ((const l, nil)).
 
-Definition SetRegFresh {descr:description} (r : REG) : M idx :=
+Definition SetRegFresh {opts : symbolic_options_computed_opt} {descr:description} (r : REG) : M idx :=
   (idx <- lift_dag merge_fresh_symbol;
   _ <- SetReg r idx;
   Symbolic.ret idx).
@@ -726,7 +732,7 @@ Bind Scope symex_scope with symexM.
 Notation "'slet' x .. y <- X ; B"  := (symex_bind X (fun x => .. (fun y => B%symex) .. )) : symex_scope.
 Notation "A <- X ; B" := (symex_bind X (fun A => B%symex)) : symex_scope.
 (* light alias *)
-Definition App {descr:description} (e : Symbolic.node idx) : symexM idx := fun st => Success (merge (simplify st e) st).
+Definition App {opts : symbolic_options_computed_opt} {descr:description} (e : Symbolic.node idx) : symexM idx := fun st => Success (merge (simplify st e) st).
 Definition RevealConstant (i : idx) : symexM N := fun st =>
   match reveal st 1 i with
   | ExprApp (const n, nil) =>
@@ -803,17 +809,17 @@ Fixpoint build_inputs {descr:description} (types : type_spec) : dag.M (list (idx
      end%dagM.
 
 (* we factor this out so that conversion is not slow when proving things about this *)
-Definition compute_array_address {descr:description} (base : idx) (i : nat)
+Definition compute_array_address {opts : symbolic_options_computed_opt} {descr:description} (base : idx) (i : nat)
   := (offset <- Symbolic.App (zconst 64%N (8 * Z.of_nat i), nil);
       Symbolic.App (add 64%N, [base; offset]))%x86symex.
 
-Definition build_merge_array_addresses {descr:description} (base : idx) (items : list idx) : M (list idx)
+Definition build_merge_array_addresses {opts : symbolic_options_computed_opt} {descr:description} (base : idx) (items : list idx) : M (list idx)
   := mapM (fun '(i, idx) =>
              (addr <- compute_array_address base i;
               (fun s => Success (addr, update_mem_with s (cons (addr,idx)))))
           )%x86symex (List.enumerate items).
 
-Fixpoint build_merge_base_addresses {descr:description} {dereference_scalar:bool} (items : list (idx + list idx)) (reg_available : list REG) : M (list ((REG + idx) + idx))
+Fixpoint build_merge_base_addresses {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool} (items : list (idx + list idx)) (reg_available : list REG) : M (list ((REG + idx) + idx))
   := match items, reg_available with
      | [], _ | _, [] => Symbolic.ret []
      | inr idxs :: xs, r :: reg_available
@@ -1003,7 +1009,7 @@ Fixpoint symex_T_app_curried {t : API.type} : symex_T t -> type.for_each_lhs_of_
 
 Bind Scope symex_scope with symex_T.
 
-Definition symex_ident {descr:description} {t} (idc : ident t) : symex_T t.
+Definition symex_ident {opts : symbolic_options_computed_opt} {descr:description} {t} (idc : ident t) : symex_T t.
 Proof.
   refine (let symex_mod_zrange idx '(ZRange.Build_zrange l u) :=
             let u := Z.succ u in
@@ -1195,7 +1201,7 @@ Proof.
   all: cbn in *.
 Defined.
 
-Fixpoint symex_expr {descr:description} {t} (e : API.expr (var:=var) t) : symex_T t
+Fixpoint symex_expr {opts : symbolic_options_computed_opt} {descr:description} {t} (e : API.expr (var:=var) t) : symex_T t
   := let _ := @Compilers.ToString.PHOAS.expr.partially_show_expr in
      match e in expr.expr t return symex_T t with
      | expr.Ident _ idc => symex_ident idc
@@ -1218,14 +1224,15 @@ Fixpoint symex_expr {descr:description} {t} (e : API.expr (var:=var) t) : symex_
      end.
 
 (* takes and returns PHOAS-style things *)
-Definition symex_PHOAS_PHOAS {t} (expr : API.Expr t) (input_var_data : type.for_each_lhs_of_arrow _ t) (d : dag)
+Definition symex_PHOAS_PHOAS {opts : symbolic_options_computed_opt} {t} (expr : API.Expr t) (input_var_data : type.for_each_lhs_of_arrow _ t) (d : dag)
   : ErrorT EquivalenceCheckingError (base_var (type.final_codomain t) * dag)
   := let ast : API.expr (type.base (type.final_codomain t))
          := invert_expr.smart_App_curried (expr _) input_var_data in
      symex_expr (descr:=no_description) ast d.
 
 (* takes and returns assembly/list style things *)
 Definition symex_PHOAS
+           {opts : symbolic_options_computed_opt}
            {t} (expr : API.Expr t)
            (inputs : list (idx + list idx))
            (d : dag)
@@ -1252,25 +1259,25 @@ Definition init_symbolic_state (d : dag) : symbolic_state
        symbolic_flag_state := Tuple.repeat None 6;
      |}.
 
-Definition compute_stack_base {descr:description} (stack_size : nat) : M idx
+Definition compute_stack_base {opts : symbolic_options_computed_opt} {descr:description} (stack_size : nat) : M idx
   := (rsp_val <- SetRegFresh rsp;
       stack_size <- Symbolic.App (zconst 64 (-8 * Z.of_nat stack_size), []);
       Symbolic.App (add 64%N, [rsp_val; stack_size]))%x86symex.
 
-Definition build_merge_stack_placeholders {descr:description} (stack_size : nat)
+Definition build_merge_stack_placeholders {opts : symbolic_options_computed_opt} {descr:description} (stack_size : nat)
   : M idx
   := (stack_placeholders <- lift_dag (build_inputarray stack_size);
       stack_base <- compute_stack_base stack_size;
       _ <- build_merge_array_addresses stack_base stack_placeholders;
       ret stack_base)%x86symex.
 
-Definition LoadArray {descr:description} (base : idx) (len : nat) : M (list idx)
+Definition LoadArray {opts : symbolic_options_computed_opt} {descr:description} (base : idx) (len : nat) : M (list idx)
   := mapM (fun i =>
              (addr <- compute_array_address base i;
               Remove64 addr)%x86symex)
           (seq 0 len).
 
-Definition LoadOutputs_internal {descr:description} {dereference_scalar:bool} (outputaddrs : list ((REG + idx) + idx)) (output_types : type_spec)
+Definition LoadOutputs_internal {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool} (outputaddrs : list ((REG + idx) + idx)) (output_types : type_spec)
   : M (list (idx + list idx))
   := (mapM (fun '(ocells, spec) =>
             match ocells, spec with
@@ -1289,7 +1296,7 @@ Definition LoadOutputs_internal {descr:description} {dereference_scalar:bool} (o
                   ret (inr v))
             end) (List.combine outputaddrs output_types))%N%x86symex.
 
-Definition LoadOutputs {descr:description} {dereference_scalar:bool} (outputaddrs : list ((REG + idx) + idx)) (output_types : type_spec)
+Definition LoadOutputs {opts : symbolic_options_computed_opt} {descr:description} {dereference_scalar:bool} (outputaddrs : list ((REG + idx) + idx)) (output_types : type_spec)
   : M (ErrorT EquivalenceCheckingError (list (idx + list idx)))
   := (* In the following line, we match on the result so we can emit Internal_error_output_load_failed in the calling function, rather than passing through the placeholder error from LoadOutputs *)
   fun s => if (List.length outputaddrs =? List.length output_types)%nat
@@ -1307,6 +1314,7 @@ Definition LoadOutputs {descr:description} {dereference_scalar:bool} (outputaddr
              Success (Error (Internal_error_LoadOutputs_length_mismatch outputaddrs output_types), s).
 
 Definition symex_asm_func_M
+           {opts : symbolic_options_computed_opt}
            (dereference_input_scalars:=false)
            {dereference_output_scalars:bool}
            (callee_saved_registers : list REG)
@@ -1344,6 +1352,7 @@ Definition symex_asm_func_M
                     s)))%N%x86symex.
 
 Definition symex_asm_func
+           {opts : symbolic_options_computed_opt}
            {dereference_output_scalars:bool}
            (d : dag) (callee_saved_registers : list REG) (output_types : type_spec) (stack_size : nat)
            (inputs : list (idx + list idx)) (reg_available : list REG) (asm : Lines)
@@ -1374,7 +1383,8 @@ Definition symex_asm_func
              end.
 
 Section check_equivalence.
-  Context {assembly_calling_registers' : assembly_calling_registers_opt}
+  Context {symbolic_opts : symbolic_options_computed_opt}
+          {assembly_calling_registers' : assembly_calling_registers_opt}
           {assembly_stack_size' : assembly_stack_size_opt}
           {assembly_output_first : assembly_output_first_opt}
           {assembly_argument_registers_left_to_right : assembly_argument_registers_left_to_right_opt}