EXPERIMENTS: shorten cache lookup chains, invalidate cache on new ensures

[jberthold]

Fixes #3982

To avoid situations where the cache contains successive mappings e -> e1 -> e2 -> e3 ... -> e_n (a "lookup chain"), the following modifications are made:

1. When inserting e -> e1, first check whether e1 -> e2 is in the cache, and insert e -> e2 instead in this case.
2. When looking up e and a binding e -> e1 is found, check whether a binding e1 -> e2 is also in the cache. In this case, update the binding for e to e -> e2 and return e2.

This will eventually lead to removing all lookup chains that may exist in a cache (for "interesting" cached values that are being looked up), without the risk of a loop.

Assume the following:

• the cache was initially empty;
• insertions and lookups are performed as described above;
• the cache contains a lookup chain e -> e1 -> e2.

If e1 -> e2 was inserted first, insertion of e -> e1 would have resulted in storing e -> e2. Therefore, e -> e1 must have been inserted first.

A subsequent lookup of e will update the cache to contain e -> e2.

Insertion of e -> e1, then e1 -> e2, then e2 -> e3, will create the lookup chain e -> e1 -> e2 -> e3.

• A lookup of e would leave the cache containing two shorter chains e -> e2 -> e3 and e1 -> e2 -> e3.
• A lookup of e1 would also leave the cache containing one shorter chain e -> e1 -> e3, and e2 -> e3.

Every lookup potentially shortens a lookup chain, possibly to several chains.

Fixes #3993

When a new path condition is added (from an ensures clause), the Equations cache is purged. While some entries may still be valid,

• all entries t -> t (no simplification possible) may be invalid because new equations might be applicable with the new path condition
• even entries t -> t' with t /= t' may be invalid because while they already memoise some applicable simplifications, they may store sub-terms that could now be evaluated or simplified further (new equations may apply)

[jberthold]

Performance for KEVM tests on par with master.

Test	3982-shorten-simplification-cache-lookup-chains time	master-f0b3596f9 time	(3982-shorten-simplification-cache-lookup-chains/master-f0b3596f9) time
kontrol/test-arithmetictest-test_max1_broken-uint256-uint256-0-spec.k	38.76	40.32	0.9613095238095237
mcd/flipper-addu48u48-fail-rough-spec.k	43.28	44.86	0.9647793134195275
benchmarks/ecrecoverloop02-sig0-invalid-spec.k	108.67	112.53	0.9656980360792677
TOTAL	190.71	197.71	0.9645946082646298

[jberthold]

Insignificant changes to kevm and kontrol tests

Test	3982-shorten-simplification-cache-lookup-chains time	master-e4bd3aadc time	(3982-shorten-simplification-cache-lookup-chains/master-e4bd3aadc) time
erc20/ds/transferFrom-failure-1-c-spec.k	83.36	79.95	1.0426516572858036
kontrol/test-expectcalltest-testexpectstaticcall-0-spec.k	41.07	39.03	1.0522674865488086
kontrol/test-expectcalltest-testexpectregularcall-0-spec.k	42.49	39.99	1.0625156289072268
benchmarks/encodepacked-keccak01-spec.k	41.0	38.24	1.0721757322175731
TOTAL	207.92	197.21	1.054307590892957

Test	3982-shorten-simplification-cache-lookup-chains time	master-e4bd3aadc time	(3982-shorten-simplification-cache-lookup-chains/master-e4bd3aadc) time
BlockParamsTest.testFee(uint256)	15.44	16.98	0.9093050647820965
CounterTest.testIncrement()	19.53	21.0	0.93
BlockParamsTest.testChainId(uint256)	15.43	16.57	0.9312009656004828
BytesTypeTest.test_bytes4(bytes4)	15.32	16.42	0.933008526187576
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_remove_node	13.52	14.28	0.9467787114845938
AddrTest.test_notBuiltinAddress_concrete()	11.92	12.51	0.9528377298161471
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_xml_report	30.97	32.22	0.9612042209807573
StartPrankTestMsgSender.test_startprank_msgsender_setup()	31.13	32.28	0.9643742255266419
MockFunctionTest.test_mock_function_all_args()	44.22	42.66	1.0365682137834038
AddrTest.test_builtInAddresses()	12.77	12.23	1.044153720359771
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_auto_abstraction	42.42	40.55	1.0461159062885328
CoinBaseTest.test_coinbase_setup()	28.12	26.2	1.0732824427480916
PlainPrankTest.test_prank_zeroAddress_true()	24.7	22.78	1.0842844600526778
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_show_with_hex_encoding	5.05	4.65	1.086021505376344
BlockParamsTest.testRoll(uint256)	16.82	15.45	1.0886731391585762
CounterTest.testSetNumber(uint256)	23.0	21.07	1.0915994304698624
AssumeTest.test_multi_assume(address,address)	22.38	20.43	1.0954478707782673
BlockParamsTest.testCoinBase()	13.46	12.08	1.1142384105960266
TOTAL	386.2	380.36	1.0153538752760545