-
Notifications
You must be signed in to change notification settings - Fork 49
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
Gas fixes #639
Conversation
b623b5c
to
7bca0f9
Compare
src/EVM/SMT.hs
Outdated
consecutivePairs [] = [] | ||
consecutivePairs [_] = [] | ||
consecutivePairs (x:y:xs) = (x, y) : consecutivePairs (y:xs) | ||
names :: [Int] = nubOrd $ concatMap (foldProp go mempty) ps |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I am a bit confused why names
is a list of Ints
. Wouldn't indices
be a better name here?
Also, can you elaborate on why this gives you the gas variables in the right order?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh yes, should be indices! Renamed :)
The nubOrd
orders the variable numbers :) But I didn't even think about it :S Just worked, and I didn't check, oops. But Yeah, nubOrd
should do the trick!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The variable numbers are actually generated in an orderly fashion. freshGasVals
starts at 0:
env = Env
{ chainId = o.chainId
, contracts = Map.fromList ((o.address,o.contract):o.otherContracts)
, freshAddresses = o.freshAddresses
, freshGasVals = 0
}
And is incremented every time it's called:
pushGas = do
modifying (#env % #freshGasVals) (+ 1)
n <- use (#env % #freshGasVals)
pushSym $ Expr.Gas n
It's not perfect... there could be more ordering constraints, but it at least makes it work to some extent. We don't assert that e.g. sub-calls get less gas -- but if they call the Gas
instruction, their remaining gas will be asserted to be less than its caller's, which is sane.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I saw this is a [Int]
, the docs suggest nubInt
is almost always better than nubOrd
https://hackage.haskell.org/package/containers-0.7/docs/Data-Containers-ListUtils.html in case you want to revisit that 😄
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh nice! Thanks, fixed!
Co-authored-by: Martin Blicha <[email protected]>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM!
Description
Gas has been a second-class citizen. We kinda died on it in many cases. This fixes some of the issues related to Gas:
gas_X
to track itGas
decreases the gas so evenGas, Gas, Gas
is strictly monotonically decreasing.I added a test-case for gas as well.
Checklist