Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Filter SMT lemmas for predicate checks and get-model #4048

Draft
wants to merge 4 commits into
base: master
Choose a base branch
from

Conversation

jberthold
Copy link
Member

Related: #4034

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
  • When checking predicates or computing a model, only those lemmas are added which relate to a 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
Copy link
Member Author

evm-semantics tests with a regression in sum-to-n-spec.k

Test 4043-filter-smt-lemmas-for-predicate-checks time master-960328a51 time (4043-filter-smt-lemmas-for-predicate-checks/master-960328a51) time
examples/sum-to-n-spec.k 96.15 70.09 1.3718076758453417
TOTAL 96.15 70.09 1.3718076758453417

@jberthold
Copy link
Member Author

More mixed results for kontrol

Test 4043-filter-smt-lemmas-for-predicate-checks time master-960328a51 time (4043-filter-smt-lemmas-for-predicate-checks/master-960328a51) time
SymbolicStorageTest.testEmptyInitialStorage(uint256) 17.6 24.51 0.7180742554059568
ExpectRevertTest.testFail_expectRevert_empty() 12.13 14.59 0.8313913639479096
HevmTests.prove_require_assert_false 37.61 44.7 0.841387024608501
ExpectCallTest.testExpectStaticCall() 17.01 19.32 0.8804347826086957
EmitContractTest.testExpectEmitDoNotCheckData() 15.25 17.28 0.8825231481481481
ExpectRevertTest.test_expectRevert_returnValue() 20.35 22.85 0.8905908096280087
StoreTest.testStoreLoadNonExistent() 12.26 13.76 0.8909883720930233
FeeTest.test_fee_setup() 25.83 28.66 0.9012561060711792
AssertTest.prove_assert_true() 14.25 15.31 0.9307642064010451
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_show_with_hex_encoding 4.5 4.82 0.933609958506224
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_auto_abstraction 29.57 31.13 0.9498875682621266
SetUpDeployTest.test_extcodesize() 42.23 44.14 0.956728590847304
UintTypeTest.test_uint256(uint256) 15.62 15.04 1.038563829787234
]) 31.15 29.95 1.0400667779632722
AssertTest.test_assert_true_branch(uint256) 28.56 27.4 1.0423357664233577
Setup2Test.testFail_setup() 30.51 28.44 1.0727848101265822
kontrol/src/tests/integration/test_foundry_prove.py::test_constructor_with_symbolic_args 82.98 76.6 1.0832898172323762
ExpectCallTest.testExpectRegularCall() 18.93 17.12 1.1057242990654206
EmitContractTest.testExpectEmitCheckEmitter() 17.09 15.38 1.1111833550065018
ExpectRevertTest.test_expectRevert_message() 20.23 18.1 1.1176795580110497
ExpectRevertTest.testFail_expectRevert_bytes4() 22.82 20.41 1.1180793728564429
ExpectRevertTest.testFail_expectRevert_multipleReverts() 19.66 17.05 1.1530791788856305
SymbolicStorageTest.testFail_SymbolicStorage1(uint256) 51.31 44.48 1.1535521582733814
SymbolicStorageTest.testFail_SymbolicStorage(uint256) 70.55 57.23 1.232745063777739
],uint256)) 59.22 42.09 1.4069850320741268
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_merge_loop_heads 87.89 58.7 1.497274275979557
HevmTests.prove_revert 20.49 13.68 1.4978070175438596
FreshCheatcodes.test_address() 21.72 13.17 1.6492027334851935
TOTAL 847.32 775.91 1.0920338699075924

@geo2a
Copy link
Collaborator

geo2a commented Sep 26, 2024

KEVM performance at 4e78fe8

Test 4043-filter-smt-lemmas-for-predicate-checks time master-79caf8c55 time (4043-filter-smt-lemmas-for-predicate-checks/master-79caf8c55) time
mcd/dsvalue-read-pass-spec.k 60.21 62.7 0.9602870813397129
benchmarks/storagevar01-spec.k 49.31 47.19 1.0449247721974995
mcd-structured/pot-join-pass-rough-spec.k 201.05 182.56 1.1012817703768625
examples/erc20-spec.md 171.51 154.13 1.112761954194511
benchmarks/ecrecoverloop02-sig1-invalid-spec.k 118.25 99.96 1.1829731892757103
erc20/ds/transfer-success-1-spec.k 75.74 58.13 1.3029416824359192
examples/sum-to-n-spec.k 134.98 100.83 1.3386888822771
TOTAL 811.0500000000001 705.5 1.1496102055279944

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants