4043 filter smt lemmas use only opaque use equations symmetrically

[jberthold]

Related: #4034

Builds upon prior PR in #4048

Booster SMT bindings change as follows:

• SMT lemmas are held in a lookup table separate from the sort and function declarations. The lookup is by SymbolName, and returns lemmas that (transitively) may relate to the given symbol
• this PR only This lookup table only considers symbols with smt-lib (called opaque symbols). Symbols with smt-hook are left out because no lemmas should be necessary for those symbols (the solver should know all valuable lemmas about its built-in operations)
• When checking predicates or computing a model, only those lemmas are added which relate to an opaque symbol used in one of the predicates

This is hopefully reducing load on the SMT solver to enable solving problems that came up in engagement proofs and led to timeouts.

[jberthold]

Same picture as before for kevm: sum-to-n slowdown

Test	4043-filter-smt-lemmas-use-only-opaque-use-equations-symmetrically time	master-4e95286ea time	(4043-filter-smt-lemmas-use-only-opaque-use-equations-symmetrically/master-4e95286ea) time
benchmarks/ecrecoverloop02-sig1-invalid-spec.k	65.03	67.57	0.9624093532632826
benchmarks/bytes00-spec.k	39.02	40.39	0.9660807130477842
examples/sum-to-n-spec.k	96.61	71.21	1.356691475916304
TOTAL	200.66000000000003	179.17	1.1199419545682874

[jberthold]

kontrol tests, run sequentially (PYTEST_PARALLEL=1) but still too noisy. (and some artefacts of the time comparison script)

Test	4043-filter-smt-lemmas-use-only-opaque-use-equations-symmetrically time	master-4e95286ea time	(4043-filter-smt-lemmas-use-only-opaque-use-equations-symmetrically/master-4e95286ea) time
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_remove_node	5.47	10.65	0.5136150234741783
kontrol/src/tests/integration/test_foundry_prove.py::test_constructor_with_symbolic_args	35.32	56.15	0.6290293855743544
ImmutableVarsTest.test_run_deployment(uint256)	97.5	132.43	0.736238012534924
StoreTest.testGasStoreWarmUp()	14.8	18.59	0.7961269499731038
FreshCheatcodes.test_int128()	11.53	14.14	0.8154172560113153
ExpectRevertTest.test_expectRevert_true()	14.15	16.3	0.8680981595092024
ExpectRevertTest.testFail_expectRevert_false()	16.7	19.13	0.872974385781495
EmitContractTest.testExpectEmitLessTopics()	14.11	16.11	0.8758535071384234
ConstructorTest.run_constructor()	10.63	12.04	0.8828903654485051
SetUpTest.testSetupData()	27.55	30.8	0.8944805194805194
BlockParamsTest.testChainId(uint256)	12.71	14.06	0.9039829302987198
ExpectRevertTest.test_ExpectRevert_increasedDepth()	17.39	19.18	0.9066736183524505
AssertTest.test_failing_branch(uint256)	44.93	49.51	0.9074934356695618
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_show_with_hex_encoding	4.63	4.87	0.9507186858316221
AccountParamsTest.testNonceSymbolic(uint64)	22.33	23.22	0.9616709732988803
BlockParamsTest.testWarp(uint256)-trace_options2	13.93	14.44	0.9646814404432134
AddrTest.test_builtInAddresses()	11.46	10.95	1.0465753424657536
SetUpDeployTest.test_extcodesize()	39.28	37.4	1.0502673796791444
ChainIdTest.test_chainid_setup()	26.8	25.35	1.057199211045365
CoinBaseTest.test_coinbase_setup()	25.48	24.01	1.0612244897959182
])	30.64	28.0	1.0942857142857143
ExpectRevertTest.test_expectRevert_bytes4()	18.1	16.27	1.1124769514443762
AssertTest.test_revert_branch(uint256,uint256)	49.8	44.52	1.118598382749326
ExpectRevertTest.testFail_ExpectRevert_failAndSuccess()	18.83	16.81	1.1201665675193337
ExpectRevertTest.test_expectRevert_returnValue()	21.35	19.02	1.1225026288117772
AssumeTest.test_assume_false(uint256,uint256)	45.97	40.52	1.1345014807502467
EmitContractTest.testExpectEmitDoNotCheckData()	16.25	14.29	1.1371588523442968
StartPrankTestOrigin.test_startprank_origin_setup()	31.81	27.59	1.152953968829286
FreshCheatcodes.test_bool()	13.78	11.74	1.1737649063032367
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_resume_proof	36.17	30.47	1.1870692484410896
],uint256))	27.66	23.3	1.1871244635193132
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_auto_abstraction	39.44	32.3	1.2210526315789474
LabelTest.testLabel()	13.87	11.01	1.259763851044505
AssertTest.testFail_assert_true()	39.92	30.06	1.3280106453759148
StoreTest.testStoreLoadNonExistent()	16.02	11.44	1.4003496503496504
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_merge_loop_heads	85.74	52.86	1.6220204313280362
TOTAL	972.05	959.53	1.0130480547768177

[ehildenb]

Do we have a test merged into Kontrol or KEVM which demonstrates where this causes a performance improvement? We should definitely have that, especially if it is good for a client engagement.

[jberthold]

Do we have a test merged into Kontrol or KEVM which demonstrates where this causes a performance improvement? We should definitely have that, especially if it is good for a client engagement.

Completely agree, especially since we see that slowdown in the sum-to-n. I changed the algorithm for @PetarMax who will hopefully be able to extract some tests from our recent engagement where he saw speed-up with this.