hevm v0.40.0 Release Notes

Release Date: 2020-07-22 // over 3 years ago
  • ๐Ÿš€ 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.