Skip to content

hevm/0.40.0
Compare
Choose a tag to compare
@github-actions github-actions released this 22 Jul 14:28
hevm/0.40.0
8e1980f

This release makes hevm capable of symbolic execution, and exposes the new hevm symbolic or hevm equivalence.

For more details, check out the announcing post https://fv.ethereum.org/2020/07/28/symbolic-hevm-release/ or consult the README for usage options.

Install as always using nix. Check out installation instructions or in brief:

curl -L https://nixos.org/nix/install | sh
. "$HOME/.nix-profile/etc/profile.d/nix.sh"
curl https://dapp.tools/install | sh

Full changelog:

0.40 - 2020-07-22

  • hevm is now capable of symbolic execution!

Changed

As a result, the types of several registers of the EVM have changed to admit symbolic values as well as concrete ones.

  • state.stack: Word -> SymWord.

  • state.memory: ByteString -> [SWord 8].

  • state.callvalue: W256 -> SymWord.

  • state.caller: Addr -> SAddr.

  • state.returndata: ByteString -> [SWord 8].

  • state.calldata: ByteString -> ([SWord 8], (SWord 32)). The first element is a list of symbolic bytes, the second is the length of calldata. We have fst calldata !! i .== 0 for all snd calldata < i.

  • tx.value: W256 -> SymWord.

  • contract.storage: Map Word Word -> Storage, defined as:

data Storage
  = Concrete (Map Word SymWord)
  | Symbolic (SArray (WordN 256) (WordN 256))
  deriving (Show)

Added

New cli commands:

  • hevm symbolic: search for assertion violations, or step through a symbolic execution in debug mode.
  • hevm equivalence: compare two programs for equivalence.

See the README for details on usage.

The new module EVM.SymExec exposes several library functions dealing with symbolic execution.
In particular,

  • SymExec.interpret: implements an operational monad script similar to TTY.interpret and Stepper.interpret, but returns a list of final VM states rather than a single VM.
  • SymExec.verify: takes a prestate and a postcondition, symbolically executes the prestate and checks that all final states matches the postcondition.

Removed

The concrete versions of a lot of arithmetic operations, replaced with their more general symbolic counterpart.

Assets 2
Loading