Repository navigation
Conversation
EIP-8037 refills state gas inside a frame, so gasleft() can grow during a transaction and CHC was wrongly proving assertions safe on paths that need more gas than before. Pass the target EVM version to the SMTChecker and add the monotonicity constraint only for EVM versions where it still holds. SMTChecker tests now compile for the EVM version given on the command line, like the other isoltest suites do, so that a test can be restricted to the versions it applies to. Tests using features newer than the oldest tested EVM version got the matching EVMVersion setting.
Contributor
|
This is premature as the faith of EIP-8037 is not decided yet. Please monitor the discussion at the linked issue #17193. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
Fixes #17193.
SMTEncoder::visitGasLeftassumed every latergasleft()was<=the previous one in the same transaction. That holds through Osaka, but EIP-8037 lets Amsterdam refill state gas inside a frame, sogasleft()can grow. CHC then treated those paths as unreachable and proved failing assertions safe.The target EVM version is now passed through to the SMTChecker, and the monotonicity constraint is only added when
hasMonotonicGasLeft()still holds (< amsterdam).SMTCheckerTestused to compile every SMT test for the default EVM version, ignoring--evm-versionand// EVMVersion:. It now uses the version from the command line, like the other isoltest suites. Tests that need features newer than the oldest tested version got the matchingEVMVersionsetting.Checklist
AI Disclosure
A Cursor cloud agent helped implement the compiler change, the SMTCheckerTest harness update, and the extra tests, and ran the isoltest suite below. I reviewed the diff and the results.
Tests
Release build with g++ 13 / Ninja and z3 4.13.3, using the SMT-LIB2 callback the same way CI does.
Example 1 from #17193: before the fix,
--evm-version amsterdam --experimentalreported the assertion safe; afterwards CHC reports the violation.build/test/tools/isoltest --no-semantic-tests -t "smtCheckerTests/*"at homestead, tangerineWhistle, spuriousDragon, byzantium, constantinople, istanbul, paris, cancun, prague, amsterdam, osaka and@future: 0 FAIL.Each EVM-version-gated SMT test at all 16 versions (832 combinations): 0 FAIL.
build/test/soltest -t '!smtCheckerTests' -- --testpath test --no-semantic-tests --evm-version osaka: no errors.scripts/check_style.sh: exit 0.