ethereum / hevm

symbolic EVM evaluator
https://hevm.dev
GNU Affero General Public License v3.0
227 stars 46 forks source link

Abstract gas v3 #427

Closed arcz closed 8 months ago

arcz commented 10 months ago

Description

Another try for abstract gas (see https://github.com/ethereum/hevm/pull/403, https://github.com/ethereum/hevm/pull/404).

I introduced two types of VMs that we can specialize execution for: VM Symbolic and VM Concrete. The behavior can be specialized in instances of VMOps class and data structures with type families similar to Gas (t :: VMType) introduced here. Thanks to -fspecialize-aggressively -fexpose-all-unfoldings this version is only slightly (~2%) slower than main as all the VMOps-dependent functions should be picked at compile time. This opens a whole world of possibilities for optimizing the concrete version of the VM without introducing too many changes.

For instance, having branch specialized to branch (Lit cond) continue = continue (cond > 0) in concrete VM speeds up ethereum-tests over 10% which puts way ahead compared to the current main. I didn't include further optimizations to limit the scope of this PR to gas.

Checklist

arcz commented 8 months ago

@d-xo it's ready

d-xo commented 8 months ago

Merged. Thanks <3