Equivalence fixes #681
Open
Equivalence fixes #681
Conversation
This file contains 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
msooseth
force-pushed
the
equiv-fix-mate
branch
2 times, most recently
from
07c494b to
33b41c7
Compare
Should work this way, cleaner Explain why test is ignored Update changelog Fixing git merge artefact Fixing up git merge Fixing some small bugs
msooseth
force-pushed
the
equiv-fix-mate
branch
2 times, most recently
from
cc374e0 to
90d7155
Compare
msooseth
force-pushed
the
equiv-fix-mate
branch
3 times, most recently
from
9b88719 to
f874dad
Compare
msooseth
force-pushed
the
equiv-fix-mate
branch
from
f874dad to
fa16a9e
Compare
zoep
approved these changes
Mar 17, 2025
| @@ -480,20 +483,23 @@ instance Eq Prop where | |||
| PImpl a b == PImpl c d = a == c && b == d | |||
| _ == _ = False | |||
|
|
|||
| -- Note: we cannot compare via `a <= c || b <= d` because then | |||
| -- when a==c but b > d, we'd return TRUE, when we should be | |||
| -- returning FALSE. | |||
There was a problem hiding this comment.
Is it OK to return TRUE when a > b (and b < d)?
There was a problem hiding this comment.
If not, you can also consider a lexicographic ordering (a <= c || (a == c && b <= d))
| CodeHash a@(LitAddr _) -> pure $ fromLazyText "codehash_" <> formatEAddr a | ||
| Gas prefix var -> pure $ fromLazyText $ "gas-" <> T.pack (TS.unpack prefix) <> T.pack (show var) |
There was a problem hiding this comment.
Is dash instead of underscore here intentional?
|
|
||
| -- If the original check was for create (i.e. undeployed code), then we must also check that the deployed | ||
| -- code is equivalent. The constraints from the undeployed code (aProps,bProps) influence this check. | ||
| checkCreatedDiff aOut bOut aProps bProps = do |
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
This fixes two underlying issues with equivalence checking.
Creation now deploys the code and checks the difference of the deployed code
Firstly, it fixes the issue that we didn't check the deployed contract, as per Zoe's observation. This is because we never deployed the contract that was created and check its difference in behaviour. This is no longer the case, we now distinguish between create/no-create equivalence checking. Some of this code was written by Zoe, and I fixed up the rest.
Equivalence checking no longer assumes overapproximated calls/etc. return the same value
Secondly, during equivalence checking, we actually didn't distinguish the fresh variables added via overapproximation for code A and code B. So the overapproximations were somehow doing the "same thing" which is wrong, they may very well be called with different arguments, at different points of the run, etc. This false equivalence was because the variables were named the same. I now have a function
rewriteFreshthat sticks anA-orB-in front of these fresh variables, therefore making them symbolically different. This also means that we potentially return false positives. This is just the way things are with overapproximation. We could add constraints, such as(initial state + calldata) -> symbolic valueand then these false positives will go away. However, for the moment, these are not added. This is future work.Small Things
Currently, we cannot deal with symbolic code. Hence, the test
constructor-diff-deployis underignoreTest. Maybe we could make it work, actually. The deployed code will NEVER have symbolic opcodes, only symbolic values. Hence, it could be possible to change the interpreter to work on this. Future work.Both
parseBlockCtxandparseTxCtxhave been modified to remove the now very fragilegascontext extraction. This context should pretty much be useless -- code really ought not to depend on gas. We could extract it, but I find that keeping code in that is not tested and not used is just a recipe for later headaches. I'd rather it isn't extracted, and if it really is necessary at a later point, we can extract it.referencedFrameContextis now usingexprToSMT, which makes it a lot more standard and less prone to breaking. It was essentially a bug that it wasn't doing that.The
OrdforPropwas incorrect.POr a b <= POr c dcannot be compared viaa <= c || b <= dbecause in the case tahta == bandb >dit will return True, but it should return False. This has been fixed.Git History etc.
Closes #647.
This is an updated version of #650 -- in a way that all commits by Zoe are preserved.
Checklist