Skip to content

RFC: The path to Futamura 🗻 #784

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.

Sign up for GitHub

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

Draft
gustavo-grieco wants to merge 11 commits into
base: main
Choose a base branch
from
Draft

RFC: The path to Futamura 🗻 #784

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
a14a0c6
started to add some code to produce futamura projections
gustavo-grieco Jun 28, 2025
b84b9f1
removed some compilation errors, but still some others there
gustavo-grieco Jun 29, 2025
30b4e18
compilation works
gustavo-grieco Jun 30, 2025
efa4aee
first opcodes correctly compiled and executed
gustavo-grieco Jul 1, 2025
288423f
more opcodes and better interfaces
gustavo-grieco Jul 2, 2025
ffa3501
basic block production
gustavo-grieco Jul 2, 2025
4969edb
initial handling of basic blocks
gustavo-grieco Jul 2, 2025
231e3ba
added enough opcodes to start benchmarking
gustavo-grieco Jul 2, 2025
615fe95
more opcodes and use st monad a single time
gustavo-grieco Jul 3, 2025
bdaf32a
naive cfg building to generate a complete program in haskell from opc…
gustavo-grieco Jul 5, 2025
4ab3b8b
experimented a bit with opcodes
gustavo-grieco Jul 6, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 8 additions & 1 deletion cli/cli.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,7 @@ import EVM.Types qualified
import EVM.UnitTest
import EVM.Effects
import EVM.Expr (maybeLitWordSimp, maybeLitAddrSimp)
import EVM.Futamura (compileAndRunSpecialized)

data AssertionType = DSTest | Forge
deriving (Eq, Show, Read)
Expand Down Expand Up @@ -137,6 +138,7 @@ data CommonExecOptions = CommonExecOptions
, gaslimit ::Maybe Word64
, gasprice ::Maybe W256
, maxcodesize ::Maybe W256
, useFutamura ::Bool
, prevRandao ::Maybe W256
, chainid ::Maybe W256
, rpc ::Maybe URL
Expand All @@ -159,6 +161,7 @@ commonExecOptions = CommonExecOptions
<*> (optional $ option auto $ long "gaslimit" <> help "Tx: gas limit")
<*> (optional $ option auto $ long "gasprice" <> help "Tx: gas price")
<*> (optional $ option auto $ long "maxcodesize" <> help "Block: max code size")
<*> (switch $ long "use-futamura" <> help "Use Futamura specialization for execution")
<*> (optional $ option auto $ long "prev-randao" <> help "Block: prevRandao")
<*> (optional $ option auto $ long "chainid" <> help "Env: chainId")
<*> rpcParser
Expand Down Expand Up @@ -564,7 +567,11 @@ launchExec cFileOpts execOpts cExecOpts cOpts = do

-- TODO: we shouldn't need solvers to execute this code
withSolvers Z3 0 1 Nothing $ \solvers -> do
vm' <- EVM.Stepper.interpret (Fetch.oracle solvers rpcinfo) vm EVM.Stepper.runFully
vm' <- case cExecOpts.useFutamura of
True -> do f <- liftIO (compileAndRunSpecialized vm)
return $ f vm
False -> EVM.Stepper.interpret (Fetch.oracle solvers rpcinfo) vm EVM.Stepper.runFully

writeTraceDapp dapp vm'
case vm'.result of
Just (VMFailure (Revert msg)) -> liftIO $ do
Expand Down
11 changes: 9 additions & 2 deletions hevm.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ cabal-version: 3.0
name:
hevm
version:
0.54.2
0.54.3
synopsis:
Symbolic EVM Evaluator
description:
Expand Down Expand Up @@ -104,6 +104,8 @@ library
EVM.Format,
EVM.Fetch,
EVM.FeeSchedule,
EVM.Opcodes,
EVM.Futamura,
EVM.Op,
EVM.Precompiled,
EVM.RLP,
Expand Down Expand Up @@ -141,6 +143,11 @@ library
install-includes:
ethjet/tinykeccak.h, ethjet/ethjet.h, ethjet/ethjet-ff.h, ethjet/blake2.h
build-depends:
ghc >= 9.6 && < 10,
ghc-paths >= 0.1,
ghc-boot-th >= 9.6 && < 10,
directory >= 1.3,
temporary >= 1.2.0 && < 1.4,
system-cxx-std-lib >= 1.0 && < 2.0,
QuickCheck >= 2.13.2 && < 2.15,
Decimal >= 0.5.1 && < 0.6,
Expand Down Expand Up @@ -196,7 +203,7 @@ executable hevm
cli
main-is:
cli.hs
ghc-options: -threaded -with-rtsopts=-N
ghc-options: -threaded -with-rtsopts=-N -optl-rdynamic
other-modules:
Paths_hevm
autogen-modules:
Expand Down
Loading
Loading