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

Fix dapp---use and solc---use for flakes #977

Draft
wants to merge 76 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from 50 commits
Commits
Show all changes
76 commits
Select commit Hold shift + click to select a range
986d54a
flake: add solc
asymmetric Jan 5, 2023
bc43430
solc: prettyfiy expression
asymmetric Jan 5, 2023
ad47ed6
ci: add flake job
asymmetric Jan 5, 2023
35cceb4
ci: no need to install cachix
asymmetric Jan 5, 2023
30635b9
flake: add solc-static-versions to packages
asymmetric Jan 5, 2023
c2b8059
nixpkgs: 21.11 -> 22.11
asymmetric Jan 7, 2023
2cfc326
ethsign: fix build
asymmetric Jan 8, 2023
64c678b
jays: fix build
asymmetric Jan 8, 2023
17298da
nix: increase log lines
asymmetric Jan 8, 2023
383ceb4
solc-static: fix darwin build
asymmetric Jan 8, 2023
93f16ab
hevm: use ethereum-hevm
asymmetric Jan 13, 2023
2cf129f
flake: remove aarch64-linux support
asymmetric Jan 13, 2023
5330b12
dapp: silence shellcheck SC2309 warning
asymmetric Jan 13, 2023
2f0bbc1
dapp/seth: add support for nix3 profiles
asymmetric Jan 13, 2023
37e3139
dapp/seth: format
asymmetric Jan 13, 2023
230e9ca
flake: add solc-versions to packages
asymmetric Jan 13, 2023
5c823de
remove mention of hevm
d-xo Dec 27, 2022
5ebcfff
wip eth-hevm
asymmetric Jan 13, 2023
2db390e
default: get revs from flake.lock
asymmetric Jan 13, 2023
ef4caf3
ci: remove hevm tests
asymmetric Jan 14, 2023
6114609
default: use fetchTarball
asymmetric Jan 14, 2023
85b9dc6
release: remove ethereum-test-suite
asymmetric Jan 14, 2023
ab7687a
ci: update actions
asymmetric Jan 14, 2023
191dd7c
rename: hevm -> eth-utils
d-xo Dec 27, 2022
d32b0a2
eth-utils: rm unused files
d-xo Dec 27, 2022
da0274f
eth-utils: compiles
d-xo Dec 27, 2022
2664a89
eth-utils: integrate into dapp & seth
d-xo Dec 27, 2022
764d442
eth-utils: rm .envrc
d-xo Dec 27, 2022
c6e46a5
geth: fix nix run invocations
asymmetric Jan 15, 2023
44cff2b
seth/dapp: fix nix run invocations
asymmetric Jan 15, 2023
53252a7
geth-unlimited: get from nixpkgs
asymmetric Jan 21, 2023
7758372
flake: add devShell
asymmetric Jan 21, 2023
3e159ce
dapp/seth: fix docstring
asymmetric Jan 21, 2023
d5e604a
dapp: add geth to PATH
asymmetric Jan 21, 2023
46e5ebe
dapp-testnet: fix invocation
asymmetric Jan 21, 2023
7e78377
dapp-testnet-launch: move into dapp-testnet
asymmetric Jan 21, 2023
9365390
dapp-testnet: fix geth rpc flags
asymmetric Jan 21, 2023
5fb8596
tests: add license to factor.sol
asymmetric Jan 21, 2023
8839a01
dapp/seth: fix nix-run invocations
asymmetric Jan 21, 2023
5125deb
flake: bump etereum-hevm
asymmetric Jan 28, 2023
1489d3c
dapp---use/seth---use: remove obsolete warning
asymmetric Feb 24, 2023
6fc88f6
dapp: use control flow, instead of exit
asymmetric Feb 24, 2023
a99d4c9
seth: stop running seth twice
asymmetric Feb 24, 2023
fbe3480
flake: update hevm
asymmetric Feb 24, 2023
f7cff5a
flake: remove hevm from devshell
asymmetric Feb 24, 2023
553b354
seth---use: cleanup
asymmetric Feb 24, 2023
907812c
flake: cleanup
asymmetric Feb 24, 2023
26d3d04
dapp: update CHANGELOG
asymmetric Feb 24, 2023
a271603
seth: update CHANGELOG
asymmetric Feb 24, 2023
ab2426a
Merge branch 'master' into solc
asymmetric Feb 25, 2023
f06c549
flake: get latest nixpkgs and update lock
asymmetric Mar 3, 2023
36923b0
.github: update cachix/install-nix-action
asymmetric Mar 3, 2023
a91c08a
dapp/seth: add info to changelog
asymmetric Mar 3, 2023
7c8d238
haskell.nix: remove unneeded patching
asymmetric Mar 3, 2023
229ff5e
Revert "haskell.nix: remove unneeded patching"
asymmetric Mar 17, 2023
ceda76e
tests: integration: disable tx_source_fetching pending hevm fix
asymmetric Mar 28, 2023
93cbab4
tests: integration: test dapp---use and seth---use
asymmetric Mar 28, 2023
eea352c
tests: integration: test dapp---nix-run
asymmetric Mar 28, 2023
c15e020
dapp: update CHANGELOG
asymmetric Mar 28, 2023
79d6c11
seth: update CHANGELOG
asymmetric Mar 28, 2023
59afe3a
dapp/seth: fix --use and --nix-use
asymmetric Mar 28, 2023
d03bc47
cvc4 -> cvc5
asymmetric Mar 29, 2023
c99f41e
ci: colored test output
asymmetric Mar 30, 2023
9127798
dapp-tests: try z3
asymmetric Mar 30, 2023
5dcc509
fixup! ci: colored test output
asymmetric Mar 30, 2023
273fb88
ci: randomize test order
asymmetric Apr 12, 2023
5d30782
ci: change test output to TAP
asymmetric Apr 12, 2023
d32ff8b
fixup! ci: change test output to TAP
asymmetric Apr 12, 2023
2d46afd
fixup! fixup! ci: change test output to TAP
asymmetric Apr 12, 2023
829ef2f
wip: debug
asymmetric Apr 13, 2023
399d51d
Revert "wip: debug"
asymmetric Apr 13, 2023
1d076b3
ci: fix nix-run tests
asymmetric Apr 13, 2023
4424353
dapp/seth: fix nix-run example
asymmetric Apr 13, 2023
ac6bd05
Revert "Revert "wip: debug""
asymmetric Apr 14, 2023
8fb01b9
ci: disable block_1 test, due to flakiness
asymmetric Apr 16, 2023
c045866
Revert "Revert "Revert "wip: debug"""
asymmetric Apr 16, 2023
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
8 changes: 3 additions & 5 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -22,20 +22,18 @@ jobs:
fail-fast: false
runs-on: ${{ matrix.os }}
steps:
- uses: actions/checkout@v2
- uses: actions/checkout@v3
# v12
- uses: cachix/install-nix-action@v14.1
- uses: cachix/install-nix-action@v18
with:
# https://discourse.nixos.org/t/understanding-binutils-darwin-wrapper-nix-support-bad-substitution/11475/2
nix_path: nixpkgs=channel:nixos-unstable
# v8
- uses: cachix/cachix-action@v10
- uses: cachix/cachix-action@v12
with:
name: dapp
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
20 changes: 20 additions & 0 deletions .github/workflows/flake.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
name: Flake
on:
pull_request:
push:

concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true

jobs:
build:
strategy:
matrix:
os: [ ubuntu-latest, macos-latest ]
fail-fast: false
runs-on: ${{ matrix.os }}
steps:
- uses: actions/checkout@v3
- uses: cachix/install-nix-action@v18
- run: nix build --accept-flake-config .#{dapp,ethsign,hevm,seth,solc}
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
```
21 changes: 5 additions & 16 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,14 +18,18 @@ 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:

### With flakes

```
nix profile install github:dapphub/dapptools#{dapp,ethsign,hevm,seth}
nix profile install github:dapphub/dapptools#{dapp,ethsign,hevm,seth,solc}
```

Nix will offer to use the dapptools binary cache, which will speed up installs,
Expand All @@ -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
30 changes: 21 additions & 9 deletions default.nix
Original file line number Diff line number Diff line change
@@ -1,16 +1,28 @@
{ system ? builtins.currentSystem , ... }:
{ 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;
};
ethereum-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)];
}
# Now return the Nixpkgs configured to use our overlay.
import nixpkgs {
inherit system;

overlays = [
(import ./overlay.nix)
(final: prev: {
hevm = ethereum-hevm.packages.${system}.hevm;
})
];
}
113 changes: 108 additions & 5 deletions flake.lock

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

Loading