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

Gas fixes #639

Merged
merged 4 commits into from
Jan 30, 2025
Merged

Gas fixes #639

merged 4 commits into from
Jan 30, 2025

Conversation

msooseth
Copy link
Collaborator

@msooseth msooseth commented Jan 27, 2025

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:

  • We use a specific variable, gas_X to track it
  • We can now emit it in SMT
  • We enforce an order on in SMT: gas is monotonically decreasing. This is true because issuing Gas decreases the gas so even Gas, Gas, Gas is strictly monotonically decreasing.

I added a test-case for gas as well.

Checklist

  • tested locally
  • added automated tests
  • updated the docs
  • updated the changelog

@msooseth msooseth force-pushed the gas-fixes branch 2 times, most recently from b623b5c to 7bca0f9 Compare January 27, 2025 12:05
@msooseth msooseth changed the title [DRAFT] Gas fixes Gas fixes Jan 27, 2025
@msooseth msooseth marked this pull request as ready for review January 27, 2025 14:10
@msooseth msooseth requested review from elopez and blishko January 27, 2025 14:10
src/EVM/SMT.hs Outdated Show resolved Hide resolved
src/EVM/SMT.hs Outdated
consecutivePairs [] = []
consecutivePairs [_] = []
consecutivePairs (x:y:xs) = (x, y) : consecutivePairs (y:xs)
names :: [Int] = nubOrd $ concatMap (foldProp go mempty) ps
Copy link
Collaborator

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?

Copy link
Collaborator Author

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!

Copy link
Collaborator Author

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.

Copy link
Collaborator

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 😄

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh nice! Thanks, fixed!

test/test.hs Outdated Show resolved Hide resolved
Copy link
Collaborator

@blishko blishko left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM!

@msooseth msooseth merged commit 51ebe37 into main Jan 30, 2025
9 checks passed
@msooseth msooseth deleted the gas-fixes branch January 30, 2025 10:45
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