Abstract gas v2 #403
Closed
Abstract gas v2 #403
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
|
All tests pass now, but perf unfortunately seems to be very similar to the V1 attempt, running main: 33.712 s ± 199 ms |
msooseth
reviewed
Oct 16, 2023
src/EVM/Expr.hs
Outdated
| @@ -374,13 +374,13 @@ writeByte offset byte src = WriteByte offset byte src | |||
|
|
|||
| writeWord :: Expr EWord -> Expr EWord -> Expr Buf -> Expr Buf | |||
| writeWord o@(Lit offset) (WAddr (LitAddr val)) b@(ConcreteBuf _) | |||
| | offset + 32 < maxBytes | |||
| | offset < maxBytes | |||
There was a problem hiding this comment.
Is this an accidental change?
msooseth
reviewed
Oct 16, 2023
| @@ -648,8 +648,8 @@ data FrameContext | |||
| | CallContext | |||
| { target :: Expr EAddr | |||
| , context :: Expr EAddr | |||
| , offset :: W256 | |||
| , size :: W256 | |||
| , offset :: Expr EWord | |||
There was a problem hiding this comment.
This is not strictly necessary, right? Or is it? I am just curious.
msooseth
reviewed
Oct 16, 2023
| @@ -681,7 +681,7 @@ data FrameState s = FrameState | |||
| , calldata :: Expr Buf | |||
| , callvalue :: Expr EWord | |||
| , caller :: Expr EAddr | |||
| , gas :: {-# UNPACK #-} !Word64 | |||
| , gas :: !gas | |||
There was a problem hiding this comment.
The change above had
{-# UNPACK #-} !gas
Wouldn't that be faster?
msooseth
approved these changes
Oct 16, 2023
|
Wow! Nice.
…On Fri 24. Nov 2023 at 19:39, dxo ***@***.***> wrote:
added the magic compiler options that @arcz <https://github.com/arcz>
uncovered in #427 <#427> and now
this benchmarks exactly the same as main!
*main*: 37.372 s ± 1.63 s
*here*: 36.147 s ± 1.55 s
—
Reply to this email directly, view it on GitHub
<#403 (comment)>, or
unsubscribe
<https://github.com/notifications/unsubscribe-auth/AXYLY5GTHA5ODQUZW253GNTYGDSVZAVCNFSM6AAAAAA5RKHZ66VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQMRVHE4DSNJRGI>
.
You are receiving this because your review was requested.Message ID:
***@***.***>
|
|
Yay, Abstract Gasv3 has been merged!! See: #427 So I am closing this :) |
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 is a second attempt at implementing a partially abstract gas model, based on top of some experiments from @arcz. Instead of modelling gas as a
Maybe Word64(as in #352), here we add agasparameter to theVMtype and constrain it to be an instance of theGastypeclass.Two instances of this class are provided:
Word64: this exactly matches the previous concrete gas semanticsSymGas: this is a single constructor type and simply acts as a marker that we should ignore all gas accountingThis (combined with a bunch of specilialise and inline pragmas) should keep the overhead for concrete execution relatively low. There are still four failing ethereum tests that need to be fixed before I can confirm this hypothesis for sure, but initial tests by @arcz on an earlier commit seemed promising.
Compared to #352 this is maybe not quite as clean (our type parameters continue to proliferate), and it does allow more invalid vm states (e.g. as implemented here the combination of concrete gas with symbolic VM state will output garbage numbers for gas), but it's probably worth it if it minimizes the impact to concrete perf.
As mentioned, there are still a few failing tests, and I want to make another pass to cleanup / better organise the code here before it's ready to merge. I may also try deleting gas entirely just to get a feel for exactly how much nicer the code would be without it...
Checklist