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

Use ethereum hevm #968

Draft
wants to merge 12 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
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
2 changes: 0 additions & 2 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,5 @@ jobs:
signingKey: '${{ secrets.CACHIX_SIGNING_KEY }}'
- name: run dapp tests
run: nix-shell --pure src/dapp-tests/shell.nix --command 'make ci --directory src/dapp-tests'
- name: run hevm symbolic tests
run: nix-build -j 1 -A hevm-tests
- run: nix-collect-garbage
- run: nix-build release.nix -A dapphub.${{ matrix.os_attr }}.stable
57 changes: 0 additions & 57 deletions ARCHITECTURE.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,60 +15,3 @@ The main entrypoint for any invocation of `seth` or `dapp` is a dispatch script,
`./src/seth/libexec/seth/seth` and `./src/dapp/libexec/dapp/dapp` respectively, which parses any
flags given, setting their values to the appropriate environment variable, and dispatches to the
appropriate subcommand.

# hevm

The core evm semnatics in hevm can be found in `EVM.hs`. EVM state is contained in the `VM` record,
and the `exec1` function executes a single opcode inside the monad `type EVM a = State VM a`.

The core semantics are pure, and should information from the outside world be required to continue
execution (rpc queries, smt queires, user input), execution will halt, and the `result` field of the
VM will be an instance of `VMFailure (Query _)`.

Multiple steps of EVM execution are orchestrated via interpreters for a meta language. Programs in
the meta language are called Steppers. The instructions in the meta language can be found in
`Stepper.hs`.

There are many different interpreters with different
features, e.g. a concrete interpreter, a symbolic interpreter, an interpreter that collects coverage
information, a debug interpreter that can accept user input. Interpreters can handle Queries in
different ways, for example in the symbolic inerpreter, both sides of a branch point will be
explored, while in the symbolic debug interpreter, user input will be requested to determine which
side of the branch point will be taken.

Interpreters are parameterized by a `Fetcher` that can handle rpc and smt queries, and can be
instantiated with fetchers that could have different fetching strategies (e.g. caching).

Interpreters execute Steppers and use their Fetcher to handle any Queries that need to be resolved.

This architecure is very modular and pluggable, and allows the core semantics to be shared between
different interpreters, as well as the reuse of steppers between different interpreters, making it
easy to e.g. replay a failed test in the debug interpreter, or to share the same test execution
strategy between concrete and symbolic interpreters.

```mermaid
graph LR
subgraph meta-language
A[Stepper]
end
subgraph interpreters
A --> B[Concrete]
A --> C[Symbolic]
A --> D[Coverage]
A --> E[Debug]
end
subgraph fetchers
F[Fetch.hs]
B --> F
C --> F
D --> F
E --> F
end
subgraph EVM Semantics
G[EVM.hs]
B --> G
C --> G
D --> G
E --> G
end
```
19 changes: 4 additions & 15 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@ hand-crafted and maintained by DappHub, along with dependency management, courte

- [dapp](./src/dapp) - All you need Ethereum development tool. Build, test, fuzz, formally verify, debug & deploy solidity contracts.
- [seth](./src/seth) - Ethereum CLI. Query contracts, send transactions, follow logs, slice & dice data.
- [hevm](./src/hevm) - Testing oriented EVM implementation. Debug, fuzz, or symbolically execute code against local or mainnet state.
- [ethsign](./src/ethsign) - Sign Ethereum transactions from a local keystore or hardware wallet.

## Development Status
Expand All @@ -19,6 +18,10 @@ dapptools is currently in a stage of clandestine development where support for t
be deprived. The software can now be considered free as in free puppy. Users seeking guidance can
explore using foundry as an alternative

hevm was previously maintained as a part of this repository, but has since been forked out by the
formal methods team at the ethereum foundation, and is now developed at
[ethereum/hevm](https://github.com/ethereum/hevm).

## Installation

Install Nix if you haven't already ([instructions](https://nixos.org/download.html)). Then install dapptools:
Expand Down Expand Up @@ -52,20 +55,12 @@ nix-env -iA <tool> -f $(curl -sS https://api.github.com/repos/dapphub/dapptools/

If you instead want to build from `master`, change the url to `https://github.com/dapphub/dapptools/archive/master.tar.gz`.

### Prebuilt hevm binary

Static binaries for linux and macos of hevm are available for each release at https://github.com/dapphub/dapptools/releases.

Most functionality is available out of the box, but for symbolic execution you will need
[`solc`](https://github.com/ethereum/solidity) and ([`z3`](https://github.com/Z3Prover/z3/) or [`cvc4`](https://github.com/CVC4/CVC4) (or both)).

## Getting started

For more information about the tools, consult the individual README pages:

- [seth](./src/seth/README.md)
- [dapp](./src/dapp/README.md)
- [hevm](./src/hevm/README.md)
- [ethsign](./src/ethsign/README.md)

or use the `--help` flag for any tool.
Expand Down Expand Up @@ -95,12 +90,6 @@ export ETH_RPC_URL=https://mainnet.infura.io/v3/$YOUR_API_KEY
dapp address 0xab5801a7d398351b8be11c439e05c5b3259aec9b $(seth nonce 0xab5801a7d398351b8be11c439e05c5b3259aec9b)
```

Symbolically explore the possible execution paths of a call to `dai.transfer(address,uint)`:
```sh
seth bundle-source 0x6b175474e89094c44da98b954eedeac495271d0f > daisrc.json && \
hevm symbolic --address 0x6b175474e89094c44da98b954eedeac495271d0f --rpc $ETH_RPC_URL --debug --sig "transfer(address,uint256)" --json-file daisrc.json
```

## Contributing

Contributions are always welcome! You may be interested in the
Expand Down
14 changes: 10 additions & 4 deletions default.nix
Original file line number Diff line number Diff line change
@@ -1,16 +1,22 @@
{ system ? builtins.currentSystem , ... }:

let
rev = "aa576357673d609e618d87db43210e49d4bb1789";
lock = builtins.fromJSON (builtins.readFile ./flake.lock);

nixpkgs = builtins.fetchTarball {
name = "nixpkgs-release-21.05";
url = "https://github.com/nixos/nixpkgs/tarball/${rev}";
sha256 = "1868s3mp0lwg1jpxsgmgijzddr90bjkncf6k6zhdjqihf0i1n2np";
url = "https://github.com/nixos/nixpkgs/tarball/${lock.nodes.nixpkgs_2.locked.rev}";
sha256 = lock.nodes.nixpkgs_2.locked.narHash;
};
hevm = import (builtins.fetchTarball {
name = "ethereum-hevm";
url = "https://github.com/ethereum/hevm/tarball/${lock.nodes.ethereum-hevm.locked.rev}";
sha256 = lock.nodes.ethereum-hevm.locked.narHash;
});
in
# Now return the Nixpkgs configured to use our overlay.
import nixpkgs {
inherit system;

overlays = [(import ./overlay.nix)];
overlays = [ (import ./overlay.nix) ];
}
105 changes: 104 additions & 1 deletion flake.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

9 changes: 3 additions & 6 deletions flake.nix
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,6 @@
};

nixConfig = {
# required to build hevm
allow-import-from-derivation = true;
extra-substituters = [ "https://dapp.cachix.org" ];
extra-substituters-public-keys = [ "dapp.cachix.org-1:9GJt9Ja8IQwR7YW/aF0QvCa6OmjGmsKoZIist0dG+Rs=" ];
};
Expand All @@ -33,14 +31,13 @@
forAllSystems (system:
let
pkgs = nixpkgsFor.${system};

dapptoolsSrc = pkgs.callPackage (import ./nix/dapptools-src.nix) { };
in
rec {
dapp = pkgs.callPackage (import ./src/dapp) { inherit dapptoolsSrc hevm seth; };
ethsign = pkgs.callPackage (import ./src/ethsign) { };
hevm = pkgs.hevm;
seth = pkgs.callPackage (import ./src/seth) { inherit dapptoolsSrc hevm ethsign; };
dapp = pkgs.callPackage (import ./src/dapp) { inherit dapptoolsSrc seth; };
ethsign = pkgs.callPackage (import ./src/ethsign) { };
seth = pkgs.callPackage (import ./src/seth) { inherit dapptoolsSrc ethsign; };
});

apps =
Expand Down
70 changes: 30 additions & 40 deletions haskell.nix
Original file line number Diff line number Diff line change
Expand Up @@ -2,52 +2,42 @@
# to our Haskell package extensions from other overlays, bypassing the
# rest of our overlay. This was necessary for rather obscure reasons.

{ pkgs, lib, wrapped ? true, shared ? false }:
{ pkgs, lib }:

let
stdenv = pkgs.stdenv;

in self-hs: super-hs:
let
dontCheck = x: y:
pkgs.haskell.lib.dontCheck
(self-hs.callCabal2nix x y {});
# FIXME: hevm is broken in our current nixpkgs pin, so we pull a newer one
# here and then use that to build hevm-0.50.0. This should be removed once
# we migrate the main nixpkgs pin to a newer version.
pkgs-2022-11 = import (pkgs.fetchFromGitHub {
owner = "nixos";
repo = "nixpkgs";
rev = "dac57a4eccf1442e8bf4030df6fcbb55883cb682";
sha256 = "sha256-C15oAtyupmLB3coZY7qzEHXjhtUx/+77olVdqVMruAg=";
}) { system = pkgs.system; };

in {
restless-git = dontCheck "restless-git" (./src/restless-git);

hevm = pkgs.haskell.lib.dontHaddock ((
self-hs.callCabal2nix "hevm" (./src/hevm) {
# Haskell libs with the same names as C libs...
# Depend on the C libs, not the Haskell libs.
# These are system deps, not Cabal deps.
inherit (pkgs) secp256k1;
}
).overrideAttrs (attrs: {
postInstall =
if wrapped
then
''
wrapProgram $out/bin/hevm --prefix PATH \
: "${lib.makeBinPath (with pkgs; [bash coreutils git solc])}"
''
else "";
myHaskell = pkgs-2022-11.haskellPackages.override {
overrides = self: super: {
hevm = pkgs.haskell.lib.dontCheck (self.callHackageDirect {
pkg = "hevm";
ver = "0.50.0";
sha256 = "sha256-ju/ZuacGneQR6tJLv7gwyMj7+u8GGQ5JcYm/XXi53yI=";
} {});
secp256k1 = pkgs.secp256k1;
# FIXME: cut a new restless-git release...
restless-git = pkgs.haskell.lib.dontCheck
(self.callCabal2nix "restless-git" (./src/restless-git) {});
eth-utils = pkgs.haskell.lib.dontHaddock (
self.callCabal2nix "eth-utils" (./src/eth-utils) {}
);
};
};

enableSeparateDataOutput = true;
buildInputs = attrs.buildInputs ++ [pkgs.solc] ++ (if wrapped then [] else [pkgs.z3 pkgs.cvc4]);
nativeBuildInputs = attrs.nativeBuildInputs ++ [pkgs.makeWrapper];
configureFlags = attrs.configureFlags ++ [
"--ghc-option=-O2"
] ++
(if stdenv.isDarwin then [] else
if shared then [] else [
"--enable-executable-static"
"--extra-lib-dirs=${pkgs.gmp.override { withStatic = true; }}/lib"
"--extra-lib-dirs=${pkgs.glibc.static}/lib"
"--extra-lib-dirs=${pkgs.libff.override { enableStatic = true; }}/lib"
"--extra-lib-dirs=${pkgs.ncurses.override {enableStatic = true; }}/lib"
"--extra-lib-dirs=${pkgs.zlib.static}/lib"
"--extra-lib-dirs=${pkgs.libffi.overrideAttrs (old: { dontDisableStatic = true; })}/lib"
]);
}));
in {
hevm = myHaskell.hevm;
eth-utils = myHaskell.eth-utils;
restless-git = myHaskell.restless-git;
}
19 changes: 0 additions & 19 deletions nix/hevm-tests/default.nix

This file was deleted.

Loading