Reorganize pipeline options to allow for easier additions to them #1448

JasonGross · 2022-10-17T09:32:02Z

Alternative to #1440
Closes #1440

I decided to add some debugging ability to rewriting (in particular some options to let fiat-crypto print out the AST before/after each rewrite pass), and decided in passing to reorganize the options to the pipeline to allow for less invasive future additions. #1440 was too heavy, so I decided to instead base the records on how we use the options (BoundsPipeline to AST, BoundsPipeline to strings, field Pipeline to AST, field pipeline to strings, (the field synthesis does a bit more computation on top of the bounds pipeline, because it knows which operation is being synthesized, whether it's for the fancy machine, etc), or the full field synthesis pipeline (which also does things like assembly equivalence checking)).

Timing check coming soon

This will allow for easier addition to the set of options in the future. <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------- 33m49.65s | 2740072 ko | Total Time / Peak Mem | 33m53.62s | 2710668 ko || -0m03.97s || 29404 ko | -0.19% | +1.08% ---------------------------------------------------------------------------------------------------------------------------------------------------------------------- 0m08.51s | 973148 ko | PushButtonSynthesis/SmallExamples.vo | 0m12.79s | 1046628 ko || -0m04.27s || -73480 ko | -33.46% | -7.02% 1m28.62s | 2008852 ko | SlowPrimeSynthesisExamples.vo | 1m26.14s | 1929460 ko || +0m02.48s || 79392 ko | +2.87% | +4.11% 5m31.43s | 2740072 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo | 5m32.61s | 2710668 ko || -0m01.18s || 29404 ko | -0.35% | +1.08% 0m30.22s | 1158528 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m31.63s | 1173992 ko || -0m01.41s || -15464 ko | -4.45% | -1.31% 0m22.53s | 1131012 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m23.80s | 1144704 ko || -0m01.26s || -13692 ko | -5.33% | -1.19% 9m51.54s | 2579912 ko | Bedrock/End2End/X25519/GarageDoor.vo | 9m52.28s | 2580004 ko || -0m00.74s || -92 ko | -0.12% | -0.00% 1m56.68s | 1395416 ko | Bedrock/Field/Synthesis/Examples/X25519_64.vo | 1m56.48s | 1396204 ko || +0m00.20s || -788 ko | +0.17% | -0.05% 1m53.08s | 1587068 ko | Bedrock/End2End/X25519/Field25519.vo | 1m53.07s | 1574828 ko || +0m00.01s || 12240 ko | +0.00% | +0.77% 1m49.83s | 2199216 ko | Fancy/Barrett256.vo | 1m49.55s | 2199296 ko || +0m00.28s || -80 ko | +0.25% | -0.00% 1m07.38s | 1697320 ko | Bedrock/Field/Synthesis/Examples/p224_64.vo | 1m06.85s | 1697200 ko || +0m00.53s || 120 ko | +0.79% | +0.00% 1m04.92s | 1698128 ko | Bedrock/Field/Synthesis/Examples/p256_64.vo | 1m05.72s | 1698124 ko || -0m00.79s || 4 ko | -1.21% | +0.00% 0m47.30s | 1664320 ko | Fancy/Montgomery256.vo | 0m47.43s | 1664556 ko || -0m00.13s || -236 ko | -0.27% | -0.01% 0m34.79s | 1490760 ko | Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.vo | 0m34.37s | 1491568 ko || +0m00.42s || -808 ko | +1.22% | -0.05% 0m32.97s | 1381196 ko | Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.vo | 0m32.85s | 1380312 ko || +0m00.11s || 884 ko | +0.36% | +0.06% 0m32.88s | 1219288 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m33.13s | 1219984 ko || -0m00.25s || -696 ko | -0.75% | -0.05% 0m26.31s | 1187480 ko | Bedrock/Field/Synthesis/Examples/LadderStep.vo | 0m26.23s | 1188760 ko || +0m00.07s || -1280 ko | +0.30% | -0.10% 0m23.09s | 1328736 ko | Bedrock/End2End/RupicolaCrypto/Low.vo | 0m23.18s | 1333636 ko || -0m00.08s || -4900 ko | -0.38% | -0.36% 0m21.82s | 1225856 ko | StandaloneDebuggingExamples.vo | 0m20.83s | 1225768 ko || +0m00.99s || 88 ko | +4.75% | +0.00% 0m21.36s | 1146468 ko | Bedrock/Field/Synthesis/Examples/X1305_32.vo | 0m21.40s | 1146508 ko || -0m00.03s || -40 ko | -0.18% | -0.00% 0m19.19s | 1168492 ko | Bedrock/End2End/RupicolaCrypto/Derive.vo | 0m19.33s | 1168752 ko || -0m00.13s || -260 ko | -0.72% | -0.02% 0m19.15s | 1101036 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m18.95s | 1102260 ko || +0m00.19s || -1224 ko | +1.05% | -0.11% 0m18.98s | 1129452 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m18.67s | 1130152 ko || +0m00.30s || -700 ko | +1.66% | -0.06% 0m17.51s | 1173576 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m17.41s | 1173112 ko || +0m00.10s || 464 ko | +0.57% | +0.03% 0m17.49s | 1102788 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m17.52s | 1102936 ko || -0m00.03s || -148 ko | -0.17% | -0.01% 0m11.66s | 1641036 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo | 0m11.59s | 1641128 ko || +0m00.07s || -92 ko | +0.60% | -0.00% 0m11.53s | 1285140 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo | 0m11.39s | 1285012 ko || +0m00.13s || 128 ko | +1.22% | +0.00% 0m10.27s | 1004612 ko | PushButtonSynthesis/BaseConversion.vo | 0m10.14s | 1005816 ko || +0m00.12s || -1204 ko | +1.28% | -0.11% 0m09.13s | 1019652 ko | PushButtonSynthesis/Primitives.vo | 0m09.70s | 1021924 ko || -0m00.56s || -2272 ko | -5.87% | -0.22% 0m08.21s | 965680 ko | BoundsPipeline.vo | 0m07.67s | 963168 ko || +0m00.54s || 2512 ko | +7.04% | +0.26% 0m07.56s | 1067820 ko | Bedrock/Field/Synthesis/Examples/EncodeDecode.vo | 0m07.41s | 1067084 ko || +0m00.14s || 736 ko | +2.02% | +0.06% 0m06.53s | 1016400 ko | PushButtonSynthesis/BarrettReduction.vo | 0m06.53s | 1016136 ko || +0m00.00s || 264 ko | +0.00% | +0.02% 0m06.33s | 1068656 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m06.28s | 1069000 ko || +0m00.04s || -344 ko | +0.79% | -0.03% 0m05.27s | 1052184 ko | Bedrock/Field/Synthesis/Examples/MulTwice.vo | 0m05.21s | 1052164 ko || +0m00.05s || 20 ko | +1.15% | +0.00% 0m04.82s | 1037680 ko | CLI.vo | 0m04.61s | 1037748 ko || +0m00.20s || -68 ko | +4.55% | -0.00% 0m04.73s | 1035468 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m04.68s | 1035704 ko || +0m00.05s || -236 ko | +1.06% | -0.02% 0m04.53s | 1002552 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m04.68s | 1000708 ko || -0m00.14s || 1844 ko | -3.20% | +0.18% 0m04.10s | 1019356 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m04.00s | 1020496 ko || +0m00.09s || -1140 ko | +2.49% | -0.11% 0m03.29s | 1049220 ko | Rewriter/PerfTesting/Core.vo | 0m03.23s | 1049196 ko || +0m00.06s || 24 ko | +1.85% | +0.00% 0m03.16s | 980668 ko | Bedrock/Field/Translation/Cmd.vo | 0m03.20s | 980520 ko || -0m00.04s || 148 ko | -1.25% | +0.01% 0m03.06s | 978548 ko | Bedrock/Field/Translation/Func.vo | 0m02.94s | 978528 ko || +0m00.12s || 20 ko | +4.08% | +0.00% 0m02.97s | 1023720 ko | Bedrock/Field/Stringification/Stringification.vo | 0m03.00s | 1023520 ko || -0m00.02s || 200 ko | -0.99% | +0.01% 0m02.96s | 1041996 ko | Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.vo | 0m02.90s | 1041952 ko || +0m00.06s || 44 ko | +2.06% | +0.00% 0m02.88s | 1031980 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m02.94s | 1032036 ko || -0m00.06s || -56 ko | -2.04% | -0.00% 0m02.85s | 1049352 ko | Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.vo | 0m02.96s | 1049448 ko || -0m00.10s || -96 ko | -3.71% | -0.00% 0m02.80s | 1018708 ko | Bedrock/Field/Synthesis/Specialized/ReifiedOperation.vo | 0m02.73s | 1018496 ko || +0m00.06s || 212 ko | +2.56% | +0.02% 0m02.72s | 1045748 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.75s | 1045572 ko || -0m00.02s || 176 ko | -1.09% | +0.01% 0m02.68s | 1039340 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m02.80s | 1039364 ko || -0m00.11s || -24 ko | -4.28% | -0.00% 0m02.67s | 1025984 ko | Bedrock/Field/Synthesis/Generic/Tactics.vo | 0m02.61s | 1025848 ko || +0m00.06s || 136 ko | +2.29% | +0.01% 0m02.59s | 1029012 ko | Bedrock/Field/Synthesis/Generic/Operation.vo | 0m02.73s | 1029056 ko || -0m00.14s || -44 ko | -5.12% | -0.00% 0m02.59s | 1061628 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m02.52s | 1061688 ko || +0m00.06s || -60 ko | +2.77% | -0.00% 0m02.59s | 1035692 ko | StandaloneHaskellMain.vo | 0m02.58s | 1035660 ko || +0m00.00s || 32 ko | +0.38% | +0.00% 0m02.58s | 1036056 ko | StandaloneOCamlMain.vo | 0m02.68s | 1036112 ko || -0m00.10s || -56 ko | -3.73% | -0.00% 0m02.57s | 1061852 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m02.49s | 1061784 ko || +0m00.07s || 68 ko | +3.21% | +0.00% 0m02.54s | 1025600 ko | Bedrock/Field/Synthesis/Specialized/Tactics.vo | 0m02.61s | 1025400 ko || -0m00.06s || 200 ko | -2.68% | +0.01% 0m02.52s | 988112 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m02.46s | 988128 ko || +0m00.06s || -16 ko | +2.43% | -0.00% 0m02.49s | 988260 ko | Bedrock/Field/Translation/Parameters/FE310.vo | 0m02.49s | 988092 ko || +0m00.00s || 168 ko | +0.00% | +0.01% 0m02.45s | 984580 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m02.39s | 984540 ko || +0m00.06s || 40 ko | +2.51% | +0.00% 0m02.44s | 988144 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m02.51s | 988080 ko || -0m00.06s || 64 ko | -2.78% | +0.00% ``` </p> </details>

The timing is a bit messed up because I haven't worked out the kinks in the branch timing script yet, but there's no significant slowdowns on the files that changed. <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------- 32m17.69s | 2706176 ko | Total Time / Peak Mem | 33m49.65s | 2740072 ko || -1m31.95s || -33896 ko | -4.53% | -1.23% ---------------------------------------------------------------------------------------------------------------------------------------------------------------------- N/A | N/A | Bedrock/Field/Translation/Proofs/Func.vo | 0m19.15s | 1101036 ko || -0m19.14s || -1101036 ko | -100.00% | -100.00% N/A | N/A | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m18.98s | 1129452 ko || -0m18.98s || -1129452 ko | -100.00% | -100.00% N/A | N/A | Bedrock/Field/Synthesis/New/Signature.vo | 0m17.51s | 1173576 ko || -0m17.51s || -1173576 ko | -100.00% | -100.00% N/A | N/A | PushButtonSynthesis/SmallExamples.vo | 0m08.51s | 973148 ko || -0m08.50s || -973148 ko | -100.00% | -100.00% N/A | N/A | BoundsPipeline.vo | 0m08.21s | 965680 ko || -0m08.21s || -965680 ko | -100.00% | -100.00% 0m27.71s | 1367708 ko | StandaloneDebuggingExamples.vo | 0m21.82s | 1225856 ko || +0m05.89s || 141852 ko | +26.99% | +11.57% N/A | N/A | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m04.73s | 1035468 ko || -0m04.73s || -1035468 ko | -100.00% | -100.00% 9m48.21s | 2580080 ko | Bedrock/End2End/X25519/GarageDoor.vo | 9m51.54s | 2579912 ko || -0m03.32s || 168 ko | -0.56% | +0.00% N/A | N/A | Bedrock/Field/Translation/Cmd.vo | 0m03.16s | 980668 ko || -0m03.16s || -980668 ko | -100.00% | -100.00% N/A | N/A | Bedrock/Field/Translation/Func.vo | 0m03.06s | 978548 ko || -0m03.06s || -978548 ko | -100.00% | -100.00% N/A | N/A | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m02.88s | 1031980 ko || -0m02.87s || -1031980 ko | -100.00% | -100.00% N/A | N/A | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m02.68s | 1039340 ko || -0m02.68s || -1039340 ko | -100.00% | -100.00% N/A | N/A | Bedrock/Field/Synthesis/Generic/Tactics.vo | 0m02.67s | 1025984 ko || -0m02.67s || -1025984 ko | -100.00% | -100.00% 1m30.32s | 2020800 ko | SlowPrimeSynthesisExamples.vo | 1m28.62s | 2008852 ko || +0m01.69s || 11948 ko | +1.91% | +0.59% 0m28.51s | 1154860 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m30.22s | 1158528 ko || -0m01.70s || -3668 ko | -5.65% | -0.31% 0m08.07s | 1016508 ko | PushButtonSynthesis/Primitives.vo | 0m09.13s | 1019652 ko || -0m01.06s || -3144 ko | -11.61% | -0.30% 5m31.92s | 2706176 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo | 5m31.43s | 2740072 ko || +0m00.49s || -33896 ko | +0.14% | -1.23% 1m56.42s | 1396552 ko | Bedrock/Field/Synthesis/Examples/X25519_64.vo | 1m56.68s | 1395416 ko || -0m00.26s || 1136 ko | -0.22% | +0.08% 1m53.01s | 1574388 ko | Bedrock/End2End/X25519/Field25519.vo | 1m53.08s | 1587068 ko || -0m00.07s || -12680 ko | -0.06% | -0.79% 1m49.21s | 2181856 ko | Fancy/Barrett256.vo | 1m49.83s | 2199216 ko || -0m00.61s || -17360 ko | -0.56% | -0.78% 1m07.01s | 1693072 ko | Bedrock/Field/Synthesis/Examples/p224_64.vo | 1m07.38s | 1697320 ko || -0m00.36s || -4248 ko | -0.54% | -0.25% 1m05.62s | 1697656 ko | Bedrock/Field/Synthesis/Examples/p256_64.vo | 1m04.92s | 1698128 ko || +0m00.70s || -472 ko | +1.07% | -0.02% 0m47.30s | 1665224 ko | Fancy/Montgomery256.vo | 0m47.30s | 1664320 ko || +0m00.00s || 904 ko | +0.00% | +0.05% 0m34.92s | 1476520 ko | Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.vo | 0m34.79s | 1490760 ko || +0m00.13s || -14240 ko | +0.37% | -0.95% 0m33.44s | 1376500 ko | Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.vo | 0m32.97s | 1381196 ko || +0m00.46s || -4696 ko | +1.42% | -0.33% 0m32.40s | 1220036 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m32.88s | 1219288 ko || -0m00.48s || 748 ko | -1.45% | +0.06% 0m26.75s | 1155644 ko | Bedrock/Field/Synthesis/Examples/LadderStep.vo | 0m26.31s | 1187480 ko || +0m00.44s || -31836 ko | +1.67% | -2.68% 0m23.16s | 1331292 ko | Bedrock/End2End/RupicolaCrypto/Low.vo | 0m23.09s | 1328736 ko || +0m00.07s || 2556 ko | +0.30% | +0.19% 0m21.78s | 1122684 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m22.53s | 1131012 ko || -0m00.75s || -8328 ko | -3.32% | -0.73% 0m21.06s | 1143476 ko | Bedrock/Field/Synthesis/Examples/X1305_32.vo | 0m21.36s | 1146468 ko || -0m00.30s || -2992 ko | -1.40% | -0.26% 0m19.18s | 1169028 ko | Bedrock/End2End/RupicolaCrypto/Derive.vo | 0m19.19s | 1168492 ko || -0m00.01s || 536 ko | -0.05% | +0.04% 0m17.28s | 1102796 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m17.49s | 1102788 ko || -0m00.20s || 8 ko | -1.20% | +0.00% 0m11.85s | 1644260 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo | 0m11.66s | 1641036 ko || +0m00.18s || 3224 ko | +1.62% | +0.19% 0m11.33s | 1285028 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo | 0m11.53s | 1285140 ko || -0m00.19s || -112 ko | -1.73% | -0.00% 0m09.68s | 1003716 ko | PushButtonSynthesis/BaseConversion.vo | 0m10.27s | 1004612 ko || -0m00.58s || -896 ko | -5.74% | -0.08% 0m07.30s | 1048624 ko | Bedrock/Field/Synthesis/Examples/EncodeDecode.vo | 0m07.56s | 1067820 ko || -0m00.25s || -19196 ko | -3.43% | -1.79% 0m06.54s | 1016448 ko | PushButtonSynthesis/BarrettReduction.vo | 0m06.53s | 1016400 ko || +0m00.00s || 48 ko | +0.15% | +0.00% 0m06.18s | 1067996 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m06.33s | 1068656 ko || -0m00.15s || -660 ko | -2.36% | -0.06% 0m05.32s | 1051536 ko | Bedrock/Field/Synthesis/Examples/MulTwice.vo | 0m05.27s | 1052184 ko || +0m00.05s || -648 ko | +0.94% | -0.06% 0m04.74s | 1037636 ko | CLI.vo | 0m04.82s | 1037680 ko || -0m00.08s || -44 ko | -1.65% | -0.00% 0m04.24s | 1008188 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m04.53s | 1002552 ko || -0m00.29s || 5636 ko | -6.40% | +0.56% 0m04.07s | 1019308 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m04.10s | 1019356 ko || -0m00.02s || -48 ko | -0.73% | -0.00% 0m03.18s | 1048404 ko | Rewriter/PerfTesting/Core.vo | 0m03.29s | 1049220 ko || -0m00.10s || -816 ko | -3.34% | -0.07% 0m03.06s | 1048904 ko | Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.vo | 0m02.85s | 1049352 ko || +0m00.20s || -448 ko | +7.36% | -0.04% 0m02.94s | 1027304 ko | Bedrock/Field/Stringification/Stringification.vo | 0m02.97s | 1023720 ko || -0m00.03s || 3584 ko | -1.01% | +0.35% 0m02.83s | 1041684 ko | Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.vo | 0m02.96s | 1041996 ko || -0m00.12s || -312 ko | -4.39% | -0.02% 0m02.74s | 1032956 ko | Bedrock/Field/Synthesis/Generic/Operation.vo | 0m02.59s | 1029012 ko || +0m00.15s || 3944 ko | +5.79% | +0.38% 0m02.72s | 1022200 ko | Bedrock/Field/Synthesis/Specialized/ReifiedOperation.vo | 0m02.80s | 1018708 ko || -0m00.07s || 3492 ko | -2.85% | +0.34% 0m02.69s | 1045260 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.72s | 1045748 ko || -0m00.03s || -488 ko | -1.10% | -0.04% 0m02.67s | 1029388 ko | Bedrock/Field/Synthesis/Specialized/Tactics.vo | 0m02.54s | 1025600 ko || +0m00.12s || 3788 ko | +5.11% | +0.36% 0m02.62s | 1019000 ko | Bedrock/Field/Translation/Parameters/FE310.vo | 0m02.49s | 988260 ko || +0m00.12s || 30740 ko | +5.22% | +3.11% 0m02.61s | 1019004 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m02.44s | 988144 ko || +0m00.16s || 30860 ko | +6.96% | +3.12% 0m02.55s | 1019060 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m02.52s | 988112 ko || +0m00.02s || 30948 ko | +1.19% | +3.13% 0m02.55s | 1061232 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m02.59s | 1061628 ko || -0m00.04s || -396 ko | -1.54% | -0.03% 0m02.54s | 1014972 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m02.45s | 984580 ko || +0m00.08s || 30392 ko | +3.67% | +3.08% 0m02.53s | 1061456 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m02.57s | 1061852 ko || -0m00.04s || -396 ko | -1.55% | -0.03% 0m02.47s | 1035368 ko | StandaloneHaskellMain.vo | 0m02.59s | 1035692 ko || -0m00.11s || -324 ko | -4.63% | -0.03% 0m02.47s | 1035864 ko | StandaloneOCamlMain.vo | 0m02.58s | 1036056 ko || -0m00.10s || -192 ko | -4.26% | -0.01% ``` </p> </details>

JasonGross force-pushed the reorganize-opts-conservative branch 2 times, most recently from d42a584 to 6c39393 Compare October 17, 2022 14:12

JasonGross force-pushed the reorganize-opts-conservative branch from 6c39393 to bf3c398 Compare October 17, 2022 15:10

JasonGross added 2 commits October 17, 2022 11:14

Adjust arguments on correctness lemmas

fb89434

JasonGross force-pushed the reorganize-opts-conservative branch from bf3c398 to fb89434 Compare October 17, 2022 15:31

JasonGross enabled auto-merge October 17, 2022 15:31

JasonGross merged commit f2c50e3 into mit-plv:master Oct 17, 2022

JasonGross deleted the reorganize-opts-conservative branch October 17, 2022 23:53

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Reorganize pipeline options to allow for easier additions to them #1448

Reorganize pipeline options to allow for easier additions to them #1448

JasonGross commented Oct 17, 2022

Reorganize pipeline options to allow for easier additions to them #1448

Reorganize pipeline options to allow for easier additions to them #1448

Conversation

JasonGross commented Oct 17, 2022