Skip to content

Support for HEVM equivalence of Vyper Contracts and multiple source files. #205

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

Open
wants to merge 8 commits into
base: main
Choose a base branch
from
Open

Support for HEVM equivalence of Vyper Contracts and multiple source files. #205

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
11f05b6
WIP partial vyper compatibility
lefterislazar Sep 13, 2025
b3ee18f
WIP vyper compatibility occasionally functional
lefterislazar Sep 18, 2025
b952148
Working Vyper HEVM equivalence, multiple source file interface
lefterislazar Sep 28, 2025
2005721
minor restoration
lefterislazar Sep 29, 2025
28db59c
minor restoration 2
lefterislazar Sep 29, 2025
564bc2e
Merge branch 'main' into vyper
lefterislazar Sep 29, 2025
003c0ed
Code review corrections and test restructuring
lefterislazar Oct 2, 2025
c7aea38
Added simple tests
lefterislazar Oct 11, 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
23 changes: 17 additions & 6 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,15 +42,19 @@ postcondition_pass=$(wildcard tests/postconditions/pass/*.act) $(typing_pass)
postcondition_fail=$(wildcard tests/postconditions/fail/*.act)

# supposed to pass, but timeout
hevm_buggy=tests/hevm/pass/transfer/transfer.act
hevm_buggy=tests/hevm/pass/transfer/transfer.act tests/hevm/pass/multisource/amm/sol_vyper.json tests/hevm/pass/multisource/amm/vyper_sol.json
# supposed to pass
hevm_pass=$(filter-out $(hevm_buggy), $(wildcard tests/hevm/pass/*/*.act))
hevm_vy_pass=$(wildcard tests/hevm/pass/vyper/*/*.act)
hevm_multi_pass=$(filter-out $(hevm_buggy), $(wildcard tests/hevm/pass/multisource/*/*.json))
# supposed to fail
hevm_fail=$(wildcard tests/hevm/fail/*/*.act)
# supposed to pass
hevm_slow=tests/hevm/pass/amm/amm.act tests/hevm/pass/amm-2/amm-2.act
hevm_multi_slow=$(wildcard tests/hevm/pass/multisource/amm/*.json) $(wildcard tests/hevm/pass/multisource/erc20/*.json)
# supposed to pass, no slow tests
hevm_fast=$(filter-out $(hevm_slow), $(hevm_pass))
hevm_multi_fast=$(filter-out $(hevm_multi_slow), $(hevm_multi_pass))

# supposed to pass
failing_typing=tests/frontend/pass/dss/vat.act tests/frontend/pass/creation/createMultiple.act tests/frontend/pass/staticstore/staticstore.act
Expand All @@ -68,8 +72,8 @@ test-parse: parser compiler $(parser_pass:=.parse.pass) $(parser_fail:=.parse.fa
test-type: parser compiler $(typing_pass:=.type.pass) $(typing_fail:=.type.fail)
test-invariant: parser compiler $(invariant_pass:=.invariant.pass) $(invariant_fail:=.invariant.fail)
test-postcondition: parser compiler $(postcondition_pass:=.postcondition.pass) $(postcondition_fail:=.postcondition.fail)
test-hevm: parser compiler $(hevm_pass:=.hevm.pass) $(hevm_fail:=.hevm.fail)
test-hevm-fast: parser compiler $(hevm_fast:=.hevm.pass.fast) $(hevm_fail:=.hevm.fail)
test-hevm: parser compiler $(hevm_pass:=.hevm.pass) $(hevm_vy_pass:=.hevm.vy.pass) $(hevm_multi_pass:=.hevm.multi.pass) $(hevm_fail:=.hevm.fail)
test-hevm-fast: parser compiler $(hevm_fast:=.hevm.pass.fast) $(hevm_vy_pass:=.hevm.vy.pass) $(hevm_multi_fast:=.hevm.multi.pass) $(hevm_fail:=.hevm.fail)
test-cabal: src/*.hs
cabal v2-run test

Expand Down Expand Up @@ -108,15 +112,22 @@ tests/%.postcondition.fail:

tests/hevm/pass/%.act.hevm.pass:
$(eval CONTRACT := $(shell awk '/contract/{ print $$2 }' tests/hevm/pass/$*.sol))
./bin/act hevm --spec tests/hevm/pass/$*.act --sol tests/hevm/pass/$*.sol --smttimeout 100000000
./bin/act hevm --spec tests/hevm/pass/$*.act --sol tests/hevm/pass/$*.sol --solver bitwuzla --smttimeout 100000000

tests/hevm/pass/%.act.hevm.vy.pass:
$(eval CONTRACT := $(shell awk '/contract/{ print $$2 }' tests/hevm/pass/$*.vy))
./bin/act hevm --spec tests/hevm/pass/$*.act --vy tests/hevm/pass/$*.vy --solver bitwuzla --smttimeout 100000000

tests/hevm/pass/%.json.hevm.multi.pass:
./bin/act hevm --sources tests/hevm/pass/$*.json --solver bitwuzla --smttimeout 100000000

tests/hevm/fail/%.act.hevm.fail:
$(eval CONTRACT := $(shell awk '/contract/{ print $$2 }' tests/hevm/fail/$*.sol))
./bin/act hevm --spec tests/hevm/fail/$*.act --sol tests/hevm/fail/$*.sol && exit 1 || echo 0
./bin/act hevm --spec tests/hevm/fail/$*.act --sol tests/hevm/fail/$*.sol --solver bitwuzla && exit 1 || echo 0

tests/hevm/pass/%.act.hevm.pass.fast:
$(eval CONTRACT := $(shell awk '/contract/{ print $$2 }' tests/hevm/pass/$*.sol))
./bin/act hevm --spec tests/hevm/pass/$*.act --sol tests/hevm/pass/$*.sol --smttimeout 100000000
./bin/act hevm --spec tests/hevm/pass/$*.act --sol tests/hevm/pass/$*.sol --solver bitwuzla --smttimeout 100000000

test-ci: test-parse test-type test-invariant test-postcondition test-coq test-hevm
test: test-ci test-cabal
2 changes: 2 additions & 0 deletions act.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,8 @@ common common
data-dword >= 0.3.2.1,
prettyprinter,
prettyprinter-ansi-terminal,
base16,
filepath
if flag(ci)
ghc-options: -O2 -Wall -Werror -Wno-orphans -Wno-unticked-promoted-constructors
else
Expand Down
2 changes: 2 additions & 0 deletions flake.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@
pkgs.cvc5
pkgs.solc
pkgs.vyper
pkgs.bitwuzla
];
});
in rec {
Expand Down Expand Up @@ -55,6 +56,7 @@
pkgs.secp256k1
pkgs.libff
pkgs.vyper
pkgs.bitwuzla
];
withHoogle = true;
shellHook = ''
Expand Down
13 changes: 7 additions & 6 deletions src/Act/Bounds.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}

module Act.Bounds (addBounds) where
module Act.Bounds (addBounds, mkLocationBounds) where

import Data.Maybe
import Data.List (nub, partition)
Expand Down Expand Up @@ -45,14 +45,14 @@ addBoundsConstructor ctor@(Constructor _ (Interface _ decls) _ pre post invs sta
invs' = addBoundsInvariant ctor <$> invs
post' = post <> mkStorageBounds stateUpdates Post

locs = concatMap locsFromExp (pre <> post)
locs = nub $ concatMap locsFromExp (pre <> post)
<> concatMap locsFromInvariant invs
<> concatMap locsFromUpdate stateUpdates
nonlocalLocs = filter (not . isLocalLoc) locs

-- | Adds type bounds for calldata, environment vars, and storage vars as preconditions
addBoundsBehaviour :: Behaviour -> Behaviour
addBoundsBehaviour behv@(Behaviour _ _ (Interface _ decls) _ pre cases post stateUpdates _) =
addBoundsBehaviour behv@(Behaviour _ _ (Interface _ decls) _ pre cases post stateUpdates ret) =
behv { _preconditions = pre', _postconditions = post' }
where
pre' = pre
Expand All @@ -63,8 +63,9 @@ addBoundsBehaviour behv@(Behaviour _ _ (Interface _ decls) _ pre cases post stat
post' = post
<> mkStorageBounds stateUpdates Post

locs = concatMap locsFromExp (pre <> post <> cases)
locs = nub $ concatMap locsFromExp (pre <> post <> cases)
<> concatMap locsFromUpdate stateUpdates
<> (maybe [] locsFromTypedExp ret)

-- | Adds type bounds for calldata, environment vars, and storage vars
addBoundsInvariant :: Constructor -> Invariant -> Invariant
Expand Down Expand Up @@ -112,7 +113,7 @@ mkStorageBounds refs t = concatMap mkBound refs
where
mkBound :: StorageUpdate -> [Exp ABoolean]
mkBound (Update SInteger item _) = [mkSItemBounds t item]
mkBound (Update typ item@(Item _ (PrimitiveType at) _) _) | isNothing $ flattenArrayAbiType at =
mkBound (Update typ item@(Item _ (PrimitiveType at) _) _) | isJust $ flattenArrayAbiType at =
maybe [] (\Refl -> mkSItemBounds t <$> expandItem item) $ testEquality (flattenSType typ) SInteger
mkBound _ = []

Expand All @@ -129,7 +130,7 @@ mkLocationBounds refs = concatMap mkBound refs
where
mkBound :: Location -> [Exp ABoolean]
mkBound (Loc SInteger rk item) = [mkItemBounds rk item]
mkBound (Loc typ rk item@(Item _ (PrimitiveType at) _)) | isNothing $ flattenArrayAbiType at =
mkBound (Loc typ rk item@(Item _ (PrimitiveType at) _)) | isJust $ flattenArrayAbiType at =
maybe [] (\Refl -> mkItemBounds rk <$> expandItem item) $ testEquality (flattenSType typ) SInteger
mkBound _ = []

Expand Down
Loading