271 recursive simplification of constraints during evaluation

[jberthold]

• recursive simplification of side conditions in rewrite rules and equations
• restrict recursion depth to a small value (5, not 100)
• modified simplification integration tests, including a description.
  • now executes with booster-dev only
  • added a test that would loop in kore-rpc-booster or kore-rpc-dev

Fixes #271

[jberthold]

KEVM timings vs latest master: a few improvements

Test	271-recursive-simplification-reprise time	master-a673bb5 time	(271-recursive-simplification-reprise/master-a673bb5) time
benchmarks/encode-keccak00-spec.k	43.47	48.37	0.8986975397973951
benchmarks/bytes00-spec.k	67.29	71.64	0.9392797319933
erc20/ds/approve-success-spec.k	55.59	58.38	0.9522096608427544
erc20/hkg/approve-spec.k	46.46	48.13	0.9653023062538957
TOTAL	212.81000000000003	226.51999999999998	0.939475542998411

[geo2a]

Kontrol performance (5 workers): some improvements and some really weird looking regressions, perhaps due to noise? rerunning with 1 worker.

Test	271-recursive-simplification-reprise time	master-a673bb5 time	(271-recursive-simplification-reprise/master-a673bb5) time
AssumeTest.test_multi_assume(address,address)	143.23	197.72	0.7244082540967024
StoreTest.testGasLoadWarmUp()	75.22	98.43	0.7641979071421314
ExpectRevertTest.test_expectRevert_message()	113.35	132.59	0.8548910174221283
SymbolicStorageTest.testEmptyInitialStorage(uint256)	50.98	59.19	0.8612941375232303
SymbolicStorageTest.testFail_SymbolicStorage(uint256)	141.08	161.01	0.8762188683932677
AllowChangesTest.testFailAllowChangesToStorage()	197.52	217.94	0.9063044874736167
BytesTypeTest.test_bytes4(bytes4)	48.9	51.63	0.94712376525276
ArithmeticTest.test_max1(uint256,uint256)	103.38	107.1	0.965266106442577
StoreTest.testStoreLoadNonExistent()	99.69	95.64	1.0423462986198244
LabelTest.testLabel()	37.89	36.04	1.0513318534961156
AddrTest.test_builtInAddresses()	28.35	26.67	1.0629921259842519
ExpectRevertTest.test_ExpectRevert_increasedDepth()	204.28	188.54	1.0834836109048478
BlockParamsTest.testWarp(uint256)	46.82	43.04	1.087825278810409
BlockParamsTest.testChainId(uint256)	54.55	44.42	1.2280504277352542
StoreTest.testGasStoreWarmUp()	98.69	73.2	1.3482240437158468
ArithmeticTest.test_max2(uint256,uint256)	89.86	65.96	1.3623408126137053
src/tests/integration/test_foundry_prove.py::test_foundry_resume_proof	117.51	86.13	1.3643329850226402
AssumeTest.test_assume_false(uint256,uint256)	111.81	80.91	1.381905821282907
StoreTest.testLoadNonExistent()	66.73	46.22	1.443747295543055
BlockParamsTest.testFee(uint256)	62.07	42.6	1.4570422535211267
BlockParamsTest.testBlockNumber()	39.45	25.76	1.531444099378882
BlockParamsTest.testCoinBase()	58.11	37.53	1.5483613109512389
BlockParamsTest.testRoll(uint256)	64.72	40.51	1.5976302147617873
BMCLoopsTest.test_countdown_concrete()	25.32	4.52	5.601769911504426
TOTAL	2079.5099999999998	1963.3000000000004	1.0591911577446134

[geo2a]

I've reran the Kontrol suite with 1 worker and the regression is not there anymore:

Test	271-recursive-simplification-reprise time	master-a673bb5 time	(271-recursive-simplification-reprise/master-a673bb5) time
src/tests/integration/test_foundry_prove.py::test_foundry_remove_node	26.35	54.06	0.48742138364779874
BytesTypeTest.test_bytes4(bytes4)	29.58	51.63	0.5729227193492155
StoreTest.testStoreLoadNonExistent()	60.69	95.64	0.6345671267252195
UintTypeTest.test_uint256(uint256)	32.37	50.2	0.644820717131474
AssertTest.test_assert_false()	41.42	62.32	0.6646341463414634
StoreTest.testGasStoreColdVM()	45.95	68.8	0.6678779069767442
AssertTest.test_assert_true()	55.38	80.57	0.6873526126349759
AllowChangesTest.testFailAllowChangesToStorage()	151.04	217.94	0.693034780214738
AssumeTest.test_multi_assume(address,address)	139.94	197.72	0.7077685616022659
ArithmeticTest.test_max1(uint256,uint256)	77.63	107.1	0.7248366013071895
StoreTest.testGasLoadWarmUp()	71.53	98.43	0.7267093365843746
StoreTest.testStoreLoad()	89.86	122.38	0.7342703056054911
LoopsTest.test_sum_10()	62.23	83.58	0.7445561139028476
AssertTest.test_assert_true_branch(uint256)	81.02	106.46	0.7610370092053353
Storage.sol	65.26	82.77	0.7884499214691314
SymbolicStorageTest.testEmptyInitialStorage(uint256)	46.67	59.19	0.7884777834093597
ERC20.sol	60.96	76.84	0.7933368037480478
ERC721.sol	61.76	76.58	0.8064768869156438
Empty.sol	61.02	75.5	0.8082119205298014
ExpectRevertTest.test_expectRevert_message()	110.18	132.59	0.8309827287125726
SymbolicStorageTest.testFail_SymbolicStorage(uint256)	140.26	161.01	0.8711260170175765
AssumeTest.testFail_assume_true(uint256,uint256)	100.22	109.36	0.9164228237015362
AssumeTest.test_assume_true(uint256,uint256)	42.39	45.54	0.9308300395256918
BlockParamsTest.testChainId(uint256)	41.52	44.42	0.9347140927510131
PlainPrankTest.testFail_startPrank_internalCall()	54.21	57.63	0.9406559083810515
AccountParamsTest.testEtchConcrete()	75.43	80.03	0.9425215544170936
InitCodeTest.testFail_init()	138.11	145.52	0.9490791643760308
AddrTest.test_notBuiltinAddress_symbolic(address)	66.72	70.23	0.9500213583938487
AccountParamsTest.test_getNonce_unknownSymbolic(address)	116.34	122.12	0.9526695054045201
LoopsTest.sum_N(uint256)	124.39	130.42	0.9537647600061341
AccountParamsTest.testDealConcrete()	63.85	66.77	0.9562677849333534
ExpectRevertTest.test_expectRevert_true()	107.95	112.5	0.9595555555555556
BlockParamsTest.testBlockNumber()	24.78	25.76	0.9619565217391304
ExpectRevertTest.test_ExpectRevert_increasedDepth()	181.44	188.54	0.9623422085499098
CounterTest.testIncrement()	155.41	161.31	0.9634244622156096
EmitContractTest.testExpectEmitDoNotCheckData()	97.58	101.26	0.9636579103298439
ExpectRevertTest.test_expectRevert_returnValue()	153.51	159.11	0.9648042234931806
BMCLoopsTest.test_countdown_symbolic(uint256)	142.74	137.84	1.03554846198491
BMCLoopsTest.test_countdown_concrete()	4.71	4.52	1.0420353982300885
MethodDisambiguateTest.test_method_call()	25.95	24.88	1.0430064308681672
src/tests/integration/test_foundry_prove.py::test_foundry_resume_proof	110.81	86.13	1.2865435968884247
AssumeTest.test_assume_false(uint256,uint256)	107.22	80.91	1.3251761216166111
TOTAL	3446.379999999999	4016.1100000000006	0.858138845798546

[geo2a]

nice!

[ehildenb]

Do we have any examples where this allows execution to continue where it couldn't before? If we don't see significant performance improvements, then we should at least check that we are indeed falling back less. Can we post fallback statistics here?

The worry I have is that recursive constraint simplification has always caused problems in the past and been tricky to implement, usually with creating potentially infinite looping code. Do we have any protections against infinite looping? Is the depth-limit of 5 mentioned above doing that? Is that user-configurable?

[jberthold]

Do we have any examples where this allows execution to continue where it couldn't before? If we don't see significant performance improvements, then we should at least check that we are indeed falling back less. Can we post fallback statistics here?

The code change enables jump condition simplifications when combined with the evm-semantics change to add preserves-definedness attributes to some key simplifications.

The worry I have is that recursive constraint simplification has always caused problems in the past and been tricky to implement, usually with creating potentially infinite looping code. Do we have any protections against infinite looping? Is the depth-limit of 5 mentioned above doing that? Is that user-configurable?

The limit of 5 is currently not configurable but we can add an option to adjust that limit. There is one test with two mutually-recursive simplifications, which indeed loops forever in the legacy backend but is caught by the new code.

[geo2a]

Kontrol performance with 3 workers

Test	271-recursive-simplification-reprise time	master-a673bb5 time	(271-recursive-simplification-reprise/master-a673bb5) time
Setup2Test.test_setup()	42.73	57.1	0.7483362521891418
BytesTypeTest.test_bytes4(bytes4)	29.17	33.64	0.8671224732461356
AllowChangesTest.testFailAllowChangesToStorage()	183.9	196.82	0.9343562646072554
ArithmeticTest.test_max1(uint256,uint256)	96.85	93.47	1.0361613351877608
BMCLoopsTest.test_countdown_concrete()	25.04	24.04	1.0415973377703827
AccountParamsTest.test_Nonce_NonExistentAddress()	63.54	60.89	1.0435211036294958
BlockParamsTest.testWarp(uint256)	42.04	40.25	1.044472049689441
AssumeTest.test_assume_staticCall(bool)	54.68	52.09	1.0497216356306391
Empty.sol	68.16	64.72	1.0531520395550062
MethodDisambiguateTest.test_method_call()	26.11	23.95	1.090187891440501
ArithmeticTest.test_max2(uint256,uint256)	80.1	61.82	1.2956971853769006
StoreTest.testGasLoadWarmUp()	92.41	71.05	1.3006333567909922
src/tests/integration/test_foundry_prove.py::test_foundry_resume_proof	111.21	80.36	1.3838974614235937
AssumeTest.test_assume_false(uint256,uint256)	105.81	75.11	1.4087338570097192
AssumeTest.testFail_assume_true(uint256,uint256)	99.32	68.66	1.4465482085639383
TOTAL	1121.07	1003.97	1.1166369513033256