hevm 0.24 → 0.41.0

raw patch · 41 files changed

+7989/−3424 lines, 41 filesdep +cborgdep +freedep +sbvdep −base64-bytestringdep −ghci-prettydep −readlinedep ~QuickCheckdep ~abstract-pardep ~aesonnew-uploaderPVP ok

version bump matches the API change (PVP)

Dependencies added: cborg, free, sbv, semver-range, witherable

Dependencies removed: base64-bytestring, ghci-pretty, readline

Dependency ranges changed: QuickCheck, abstract-par, aeson, ansi-wl-pprint, async, base, base16-bytestring, binary, brick, bytestring, cereal, containers, cryptonite, data-dword, deepseq, directory, fgl, filepath, haskeline, here, lens, lens-aeson, megaparsec, memory, monad-par, mtl, multiset, operational, optparse-generic, process, quickcheck-text, regex-tdfa, restless-git, rosezipper, s-cargot, scientific, temporary, text, text-format, time, transformers, unordered-containers, vector, vty, wreq

API changes (from Hackage documentation)

Files

• CHANGELOG.md +158/−0
• ethjet/blake2.cc +65/−0
• ethjet/blake2.h +17/−0
• ethjet/ethjet-ff.cc +278/−0
• ethjet/ethjet-ff.h +18/−0
• ethjet/ethjet.c +34/−0
• ethjet/ethjet.h +4/−0
• hevm-cli/hevm-cli.hs +642/−143
• hevm.cabal +121/−99
• run-blockchain-tests +136/−0
• run-consensus-tests +75/−47
• src/EVM.hs +2603/−1713
• src/EVM/ABI.hs +191/−58
• src/EVM/Concrete.hs +48/−77
• src/EVM/Dapp.hs +16/−17
• src/EVM/Debug.hs +4/−6
• src/EVM/Demand.hs +13/−0
• src/EVM/Dev.hs +32/−3
• src/EVM/Emacs.hs +111/−34
• src/EVM/Exec.hs +20/−8
• src/EVM/Facts.hs +16/−12
• src/EVM/Facts/Git.hs +3/−5
• src/EVM/FeeSchedule.hs +63/−6
• src/EVM/Fetch.hs +93/−21
• src/EVM/Flatten.hs +32/−14
• src/EVM/Format.hs +92/−89
• src/EVM/Keccak.hs +3/−67
• src/EVM/Op.hs +94/−1
• src/EVM/Patricia.hs +232/−0
• src/EVM/RLP.hs +79/−0
• src/EVM/Solidity.hs +154/−54
• src/EVM/Stepper.hs +68/−44
• src/EVM/StorageLayout.hs +6/−37
• src/EVM/SymExec.hs +317/−0
• src/EVM/Symbolic.hs +300/−0
• src/EVM/TTY.hs +515/−482
• src/EVM/Transaction.hs +92/−0
• src/EVM/Types.hs +130/−16
• src/EVM/UnitTest.hs +252/−223
• src/EVM/VMTest.hs +405/−94
• test/test.hs +457/−54

@@ -1,5 +1,163 @@ # hevm changelog +## 0.41.0 - 2020-08-19++### Changed++- Switched to [PVP](https://github.com/haskell/pvp/blob/master/pvp-faq.md) for version control, starting now at `0.41.0` (MAJOR.MAJOR.MINOR).+- z3 updated to 4.8.7+- Generate more interesting values in property based testing, + and implement proper shrinking for all abi values.+- Fixed soundness bug when using KECCAK or SHA256 opcode/precompile+- Fixed an issue in debug mode where backstepping could cause path information to be forgotten+- Ensure that pathconditions are consistent when branching, and end the execution with VMFailure: DeadPath if this is not the case+- Fixed a soundness bug where nonzero jumpconditions  were assumed to equal one.+- default `--smttimeout` changed from unlimited to 20 seconds+- `hevm symbolic --debug` now respects `--max-iterations`++### Added++- `hevm exec --trace` flag to dump a trace+- Faster backstepping in interactive mode by saving multiple snapshot states.+- Support for symbolic storage for multiple contracts++## 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:+```hs+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.+++## 0.39 - 2020-07-13+ - Exposes abi encoding to cli+ - Added cheat code `hevm.store(address a, bytes32 location, bytes32 value)`+ - Removes `ExecMode`, always running as `ExecuteAsBlockchainTest`. This means that `hevm exec` now finalizes transactions as well.+ - `--code` is now entirely optional. Not supplying it returns an empty contract, or whatever is stored in `--state`.++## 0.38 - 2020-04-23+ - Exposes metadata stripping of bytecode to the cli: `hevm strip-metadata --code X`. [357](https://github.com/dapphub/dapptools/pull/357).+ - Fixes a bug in the srcmap parsing introduced in 0.37 [356](https://github.com/dapphub/dapptools/pull/356).+ - Fixes a bug in the abi-encoding of `bytes` with size > 32[358](https://github.com/dapphub/dapptools/pull/358).++## 0.37 - 2020-03-24+ - Sourcemap parser now admits `solc-0.6.0` compiled `.sol.json` files.++## 0.36 - 2020-01-07+ - Implement Istanbul support [318](https://github.com/dapphub/dapptools/pull/318)+ - Fix a bug introduced in [280](https://github.com/dapphub/dapptools/pull/280) of rlp encoding of transactions and sender address [320](https://github.com/dapphub/dapptools/pull/320/).+ - Make InvalidTx a fatal error for vm tests and ci.+ - Suport property based testing in unit tests. [313](https://github.com/dapphub/dapptools/pull/313) Arguments to test functions are randomly generated based on the function abi. Fuzz tests are not present in the graphical debugger.+ - Added flags `--replay` and `--fuzz-run` to `hevm dapp-test`, allowing for particular fuzz run cases to be rerun, or for configuration of how many fuzz tests are run.+ - Correct gas readouts for unit tests+ - Prevent crash when trying to jump to next source code point if source code is missing++## 0.35 - 2019-11-02+ - Merkle Patricia trie support [280](https://github.com/dapphub/dapptools/pull/280)+ - RLP encoding and decoding functions [280](https://github.com/dapphub/dapptools/pull/280)+ - Extended support for Solidity ABI encoding [259](https://github.com/dapphub/dapptools/pull/259)+ - Bug fixes surrounding unit tests and gas accounting (https://github.com/dapphub/dapptools/commit/574ef401d3e744f2dcf994da056810cf69ef84fe, https://github.com/dapphub/dapptools/commit/5257574dd9df14edc29410786b75e9fb9c59069f)++## 0.34 - 2019-08-28+ - handle new solc bzzr metadata in codehash for source map+ - show VM hex outputs as hexadecimal+ - rpc defaults to latest block+ - `hevm interactive`:+  - fix rpc fetch+  - scrollable memory pane+ - Fix regression in VMTest compliance.+ - `hevm exec` ergonomics:+  - Allow code/calldata prefixed with 0x+  - create transactions with specific caller nonce+  - interactive help pane+  - memory pane scrolling++## 0.33 - 2019-08-06+ - Full compliance with the [General State Tests][245] (with the+   BlockchainTest format), using the Yellow and Jello papers as+   reference, for Constantinople Fix (aka Petersburg). Including:+  - full precompile support+  - correct substate accounting, including touched accounts,+    selfdestructs and refunds+  - memory read/write semantics+  - many gas cost corrections+ - Show more information for non solc bytecode in interactive view+   (trace and storage)+ - Help text for all cli options+ - Enable `--debug` flag in `hevm dapp-test`++[245]: https://github.com/dapphub/dapptools/pull/245++## 0.32 - 2019-06-14+ - Fix dapp-test [nonce initialisation bug][224]++[224]: https://github.com/dapphub/dapptools/pull/224++## 0.31 - 2019-05-29+ - Precompiles: SHA256, RIPEMD, IDENTITY, MODEXP, ECADD, ECMUL,+   ECPAIRING, MODEXP+ - Show the hevm version with `hevm version`+ - Interactive mode:+  - no longer exits on reaching halt+  - new shortcuts: 'a' / 'e' for start / end+  - allow returning to test picker screen+ - Exact integer formatting in dapp-test and tty++## 0.30 - 2019-05-09+ - Adjustable verbosity level for `dapp-test` with `--verbose={0,1,2}`+ - Working stack build++## 0.29 - 2019-04-03+ - Significant jump in compliance with client tests+ - Add support for running GeneralStateTests++## 0.28 - 2019-03-22+ - Fix delegatecall gas metering, as reported in+   https://github.com/dapphub/dapptools/issues/34++## 0.27 - 2019-02-06+ - Fix [hevm flatten issue](https://github.com/dapphub/dapptools/issues/127)+   related to SemVer ranges in Solidity version pragmas++## 0.26 - 2019-02-05+ - Format Solidity Error(string) messages in trace++## 0.25 - 2019-02-04+ - Add SHL, SHR and SAR opcodes+ ## 0.24 - 2019-01-23  - Fix STATICCALL for precompiled contracts  - Assume Solidity 0.5.2 in tests

@@ -0,0 +1,65 @@+#include <cstdint>+#include "blake2.h"++#define ROTR64(x, y) (((x) >> (y)) ^ ((x) << (64 - (y))))++#define B2B_G(a, b, c, d, x, y)   \+  v[a] = v[a] + v[b] + x;         \+  v[d] = ROTR64(v[d] ^ v[a], 32); \+  v[c] = v[c] + v[d];             \+  v[b] = ROTR64(v[b] ^ v[c], 24); \+  v[a] = v[a] + v[b] + y;         \+  v[d] = ROTR64(v[d] ^ v[a], 16); \+  v[c] = v[c] + v[d];             \+  v[b] = ROTR64(v[b] ^ v[c], 63);++static const uint64_t blake2b_iv[8] = {+  0x6A09E667F3BCC908, 0xBB67AE8584CAA73B,+  0x3C6EF372FE94F82B, 0xA54FF53A5F1D36F1,+  0x510E527FADE682D1, 0x9B05688C2B3E6C1F,+  0x1F83D9ABFB41BD6B, 0x5BE0CD19137E2179+};++static const uint8_t sigma[10][16] = {+  { 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 },+  { 14, 10, 4, 8, 9, 15, 13, 6, 1, 12, 0, 2, 11, 7, 5, 3 },+  { 11, 8, 12, 0, 5, 2, 15, 13, 10, 14, 3, 6, 7, 1, 9, 4 },+  { 7, 9, 3, 1, 13, 12, 11, 14, 2, 6, 5, 10, 4, 0, 15, 8 },+  { 9, 0, 5, 7, 2, 4, 10, 15, 14, 1, 11, 12, 6, 8, 3, 13 },+  { 2, 12, 6, 10, 0, 11, 8, 3, 4, 13, 7, 5, 15, 14, 1, 9 },+  { 12, 5, 1, 15, 14, 13, 4, 10, 0, 7, 6, 3, 9, 2, 8, 11 },+  { 13, 11, 7, 14, 12, 1, 3, 9, 5, 0, 15, 4, 8, 6, 2, 10 },+  { 6, 15, 14, 9, 11, 3, 0, 8, 12, 2, 13, 7, 1, 4, 10, 5 },+  { 10, 2, 8, 4, 7, 6, 1, 5, 15, 11, 9, 14, 3, 12, 13, 0 }+};++void blake2b_compress(uint64_t *h, uint64_t *m, uint64_t *t, char f, uint32_t rounds) {+  uint32_t i;+  uint64_t v[16];++  for (i = 0; i < 8; i++) {+    v[i] = h[i];+    v[i+8] = blake2b_iv[i];+  }++  v[12] ^= t[0];+  v[13] ^= t[1];++  if (f) v[14] = ~v[14];++  int index;+  for (i = 0; i < rounds; i++) {+    index = i % 10;+    B2B_G( 0, 4,  8, 12, m[sigma[index][ 0]], m[sigma[index][ 1]]);+    B2B_G( 1, 5,  9, 13, m[sigma[index][ 2]], m[sigma[index][ 3]]);+    B2B_G( 2, 6, 10, 14, m[sigma[index][ 4]], m[sigma[index][ 5]]);+    B2B_G( 3, 7, 11, 15, m[sigma[index][ 6]], m[sigma[index][ 7]]);+    B2B_G( 0, 5, 10, 15, m[sigma[index][ 8]], m[sigma[index][ 9]]);+    B2B_G( 1, 6, 11, 12, m[sigma[index][10]], m[sigma[index][11]]);+    B2B_G( 2, 7,  8, 13, m[sigma[index][12]], m[sigma[index][13]]);+    B2B_G( 3, 4,  9, 14, m[sigma[index][14]], m[sigma[index][15]]);+  }++  for (i = 0; i < 8; ++i)+    h[i] ^= v[i] ^ v[i+8];+}

@@ -0,0 +1,17 @@+#ifndef BLAKE2_H+#define BLAKE2_H++#include <stdint.h>++#ifdef __cplusplus+extern "C" {+#endif++void+blake2b_compress(uint64_t *h, uint64_t *m, uint64_t *t, char f, uint32_t rounds);++#ifdef __cplusplus+}+#endif++#endif

@@ -0,0 +1,278 @@+#include "ethjet.h"++#include <gmp.h>+#include <stdio.h>++#include <libff/algebra/fields/bigint.hpp>+#include <libff/algebra/curves/alt_bn128/alt_bn128_init.hpp>+#include <libff/algebra/curves/alt_bn128/alt_bn128_g1.hpp>+#include <libff/algebra/curves/alt_bn128/alt_bn128_g2.hpp>+#include <libff/algebra/curves/alt_bn128/alt_bn128_pairing.hpp>+#include <libff/common/profiling.hpp>++using namespace libff;++namespace ethjet_ff {+  void init() {+    libff::inhibit_profiling_info     = true;+    libff::inhibit_profiling_counters = true;+    init_alt_bn128_params();+  }++  // for loading an element of F_q (a coordinate of G_1)+  // consumes 32 bytes+  alt_bn128_Fq read_Fq_element (uint8_t *in) {+    mpz_t x_data;+    mpz_init(x_data);+    mpz_import(x_data, 32, 1, sizeof(in[0]), 1, 0, in);++    mpz_t q;+    mpz_init(q);+    alt_bn128_modulus_q.to_mpz(q);+    const mp_size_t limbs = alt_bn128_q_limbs;++    if (mpz_cmp(x_data, q) >= 0)+      throw 0;++    return Fp_model<limbs, alt_bn128_modulus_q>(bigint<limbs>(x_data));+  }++  // for loading an element of F_{q^2} (a coordinate of G_2)+  // consumes 64 bytes+  alt_bn128_Fq2 read_Fq2_element (uint8_t *in) {+    // suprising "big-endian" encoding+    alt_bn128_Fq x0 = read_Fq_element(in+32);+    alt_bn128_Fq x1 = read_Fq_element(in);++    mpz_t q;+    mpz_init(q);+    alt_bn128_modulus_q.to_mpz(q);++    return Fp2_model<alt_bn128_q_limbs, alt_bn128_modulus_q>(x0, x1);+  }++  // for loading an element of F_r (a scalar for G_1)+  // consumes 32 bytes+  alt_bn128_Fr read_Fr_element (uint8_t *in) {+    mpz_t x_data;+    mpz_init(x_data);+    mpz_import(x_data, 32, 1, sizeof(in[0]), 1, 0, in);++    mpz_t r;+    mpz_init(r);+    alt_bn128_modulus_r.to_mpz(r);+    const mp_size_t limbs = alt_bn128_r_limbs;++    return Fp_model<limbs, alt_bn128_modulus_r>(bigint<limbs>(x_data));+  }++  // for loading a point in G_1+  // consumes 64 bytes+  alt_bn128_G1 read_G1_point (uint8_t *in) {+    alt_bn128_Fq ax = read_Fq_element(in);+    alt_bn128_Fq ay = read_Fq_element(in+32);+    alt_bn128_G1 a;+    // create curve point from affine coordinates+    // the point at infinity (0,0) is a special case+    if (ax.is_zero() && ay.is_zero()) {+      a = alt_bn128_G1::G1_zero;+    }+    else {+      a = alt_bn128_G1(ax, ay, alt_bn128_Fq::one());+    }+    if (! a.is_well_formed()) {+      throw 0;+    }+    return a;+  }++  // for loading a point in G_2+  // consumes 128 bytes+  alt_bn128_G2 read_G2_point (uint8_t *in) {+    alt_bn128_Fq2 ax = read_Fq2_element(in);+    alt_bn128_Fq2 ay = read_Fq2_element(in+64);+    alt_bn128_G2  a;+    // create curve point from affine coordinates+    // the point at infinity (0,0) is a special case+    if (ax.is_zero() && ay.is_zero()) {+      a = alt_bn128_G2::G2_zero;+      return a;+    }+    a = alt_bn128_G2(ax, ay, alt_bn128_Fq2::one());+    if (! a.is_well_formed()) {+      throw 0;+    }+    // additionally check that the element has the right order+    if (-alt_bn128_Fr::one() * a + a != alt_bn128_G2::G2_zero) {+      throw 0;+    }+    return a;+  }++  // writes an element of Fq+  // produces 32 bytes+  void write_Fq_element(uint8_t *out, alt_bn128_Fq x) {+    mpz_t x_data;+    size_t x_size;+    mpz_init(x_data);++    x.as_bigint().to_mpz(x_data);+    uint8_t *x_arr = (uint8_t *)mpz_export(NULL, &x_size, 1, 1, 1, 0, x_data);+    if (x_size > 32) {+      throw 0;+    }+    // copy the result to the output buffer+    // with padding+    for (int i = 1; i <= 32; i++) {+      if (i <= x_size)+        out[32-i] = x_arr[x_size-i];+      else+        out[32-i] = 0;+    }+    return;+  }++  // writes an element of F_{q^2}+  // produces 64 bytes+  void write_Fq2_element(uint8_t *out, alt_bn128_Fq2 x) {+    // surprising "big-endian" encoding+    write_Fq_element(out+32, x.c0);+    write_Fq_element(out,    x.c1);+    return;+  }++  // writes a point of G1+  // produces 64 bytes+  void write_G1_point(uint8_t *out, alt_bn128_G1 a) {+    // point at infinity is represented as (0,0)+    // so treat it as a special case+    if (a.is_zero()) {+      write_Fq_element(out,    alt_bn128_Fq::zero());+      write_Fq_element(out+32, alt_bn128_Fq::zero());+      return;+    }+    a.to_affine_coordinates();+    write_Fq_element(out,    a.X);+    write_Fq_element(out+32, a.Y);+    return;+  }++  // writes a point of G2+  // produces 128 bytes+  void write_G2_point(uint8_t *out, alt_bn128_G2 a) {+    // point at infinity is represented as (0,0)+    // so treat it as a special case+    if (a.is_zero()) {+      write_Fq2_element(out,    alt_bn128_Fq2::zero());+      write_Fq2_element(out+64, alt_bn128_Fq2::zero());+      return;+    }+    a.to_affine_coordinates();+    write_Fq2_element(out,    a.X);+    write_Fq2_element(out+64, a.Y);+    return;+  }++  // writes a bool+  // produces 32 bytes+  void write_bool(uint8_t *out, bool p) {+    out[31] = (int)(p);+    for (int i = 2; i <= 32; i++) {+      out[32-i] = 0;+    }+  }+}++extern "C" {+  using namespace ethjet_ff;++  int+  ethjet_ecadd (uint8_t *in, size_t in_size,+                uint8_t *out, size_t out_size) {++    if (in_size != 128) {+      return 0;+    }+    if (out_size != 64) {+      return 0;+    }++    init();++    try {+      alt_bn128_G1 a = read_G1_point(in);+      alt_bn128_G1 b = read_G1_point(in+64);+      alt_bn128_G1 sum = (a + b);++      write_G1_point(out, sum);+    }+    catch (int e) {+      return 0;+    }++    return 1;+  }++  int+  ethjet_ecmul (uint8_t *in, size_t in_size,+                uint8_t *out, size_t out_size) {++    if (in_size != 96) {+      return 0;+    }+    if (out_size != 64) {+      return 0;+    }++    init();++    try {+      alt_bn128_G1 a = read_G1_point(in);+      alt_bn128_Fr n = read_Fr_element(in+64);+      alt_bn128_G1 na = n * a;++      write_G1_point(out, na);+    }+    catch (int e) {+      return 0;+    }++    return 1;+  }++  int+  ethjet_ecpairing (uint8_t *in, size_t in_size,+                    uint8_t *out, size_t out_size) {++    if (in_size % 192 != 0)+      return 0;++    if (out_size != 32)+      return 0;++    init();+    int pairs = in_size / 192;++    try {+      alt_bn128_Fq12 x = libff::alt_bn128_Fq12::one();+      for (int i = 0; i < pairs; i++) {+        alt_bn128_G1 a = read_G1_point(in + i*192);+        alt_bn128_G2 b = read_G2_point(in + i*192 + 64);+        if (a.is_zero() || b.is_zero())+          continue;+        x = x * alt_bn128_miller_loop(alt_bn128_precompute_G1(a), alt_bn128_precompute_G2(b));+      }+      bool result;+      if (pairs == 0)+        result = true;+      else+        result = (alt_bn128_final_exponentiation(x) == alt_bn128_GT::one());+      write_bool(out, result);+    }+    catch (int e) {+      return 0;+    }++    return 1;+  }+}

@@ -0,0 +1,18 @@+#ifndef ETHJET_FF_H+#define ETHJET_FF_H++#include <stdint.h>++int+ethjet_ecadd (uint8_t *in, size_t in_size,+              uint8_t *out, size_t out_size);++int+ethjet_ecmul (uint8_t *in, size_t in_size,+              uint8_t *out, size_t out_size);++int+ethjet_ecpairing (uint8_t *in, size_t in_size,+                  uint8_t *out, size_t out_size);++#endif

@@ -1,5 +1,7 @@ #include "ethjet.h"+#include "ethjet-ff.h" #include "tinykeccak.h"+#include "blake2.h"  #include <secp256k1_recovery.h> @@ -68,6 +70,11 @@   input64 = in + 64;   recid = in[63] - 27; +  /* higher bytes of V should be zero  */+  static const char z31 [31];+  if (memcmp (z31, in + 32, 31))+    return 0;+   if (recid < 0 || recid > 3)     return 0; @@ -90,6 +97,21 @@   return 1; } +int ethjet_blake2(uint8_t *in, size_t in_size,+                  uint8_t *out, size_t out_size) {+  uint32_t rounds = in[0] << 24 | in[1] << 16 | in[2] << 8 | in[3];+  unsigned char f = in[212];+  uint64_t *h = (uint64_t *)&in[4];+  uint64_t *m = (uint64_t *)&in[68];+  uint64_t *t = (uint64_t *)&in[196];++  blake2b_compress(h, m, t, f, rounds);++  memcpy(out, h, out_size);++  return 1;+}+ int ethjet (struct ethjet_context *ctx,         enum ethjet_operation op,@@ -103,6 +125,18 @@    case ETHJET_EXAMPLE:     return ethjet_example (ctx, in, in_size, out, out_size);++  case ETHJET_ECADD:+    return ethjet_ecadd (in, in_size, out, out_size);++  case ETHJET_ECMUL:+    return ethjet_ecmul (in, in_size, out, out_size);++  case ETHJET_ECPAIRING:+    return ethjet_ecpairing (in, in_size, out, out_size);++  case ETHJET_BLAKE2:+    return ethjet_blake2 (in, in_size, out, out_size);    default:     return 0;

@@ -13,6 +13,10 @@ enum ethjet_operation   {     ETHJET_ECRECOVER = 1,+    ETHJET_ECADD = 6,+    ETHJET_ECMUL = 7,+    ETHJET_ECPAIRING = 8,+    ETHJET_BLAKE2 = 9,     ETHJET_EXAMPLE = 0xdeadbeef,   }; 

@@ -1,132 +1,238 @@ -- Main file of the hevm CLI program -{-# Language BangPatterns #-} {-# Language CPP #-}+{-# Language DataKinds #-}+{-# Language FlexibleInstances #-} {-# Language DeriveGeneric #-}-{-# Language GeneralizedNewtypeDeriving #-}+{-# Language GADTs #-} {-# Language LambdaCase #-} {-# Language NumDecimals #-} {-# Language OverloadedStrings #-}-{-# Language TemplateHaskell #-}+{-# Language TypeOperators #-} -import EVM.Concrete (w256)+module Main where -import qualified EVM as EVM+import EVM (StorageModel(..))+import qualified EVM+import EVM.Concrete (createAddress, w256)+import EVM.Symbolic (forceLitBytes, litBytes, litAddr, w256lit, sw256, SymWord(..), Buffer(..), len) import qualified EVM.FeeSchedule as FeeSchedule import qualified EVM.Fetch import qualified EVM.Flatten import qualified EVM.Stepper-import qualified EVM.TTY as EVM.TTY-import qualified EVM.Emacs as EVM.Emacs+import qualified EVM.TTY+import qualified EVM.Emacs  #if MIN_VERSION_aeson(1, 0, 0) import qualified EVM.VMTest as VMTest #endif +import EVM.SymExec import EVM.Debug-import EVM.Exec+import EVM.ABI import EVM.Solidity import EVM.Types hiding (word) import EVM.UnitTest (UnitTestOptions, coverageReport, coverageForUnitTestContract) import EVM.UnitTest (runUnitTestContract) import EVM.UnitTest (getParametersFromEnvironmentVariables, testNumber)-import EVM.Dapp (findUnitTests, dappInfo)--import qualified EVM.UnitTest as EVM.UnitTest+import EVM.Dapp (findUnitTests, dappInfo, DappInfo)+import EVM.Format (showTraceTree)+import EVM.RLP (rlpdecode)+import qualified EVM.Patricia as Patricia+import Data.Map (Map) -import qualified Paths_hevm as Paths+import qualified EVM.Facts     as Facts+import qualified EVM.Facts.Git as Git+import qualified EVM.UnitTest  import Control.Concurrent.Async   (async, waitCatch)-import Control.Exception          (evaluate)-import Control.Lens-import Control.Monad              (void, when, forM_)-import Control.Monad.State.Strict (execState)+import Control.Lens hiding (pre)+import Control.Monad              (void, when, forM_, unless)+import Control.Monad.State.Strict (execStateT) import Data.ByteString            (ByteString) import Data.List                  (intercalate, isSuffixOf) import Data.Text                  (Text, unpack, pack)-import Data.Maybe                 (fromMaybe)+import Data.Text.Encoding         (encodeUtf8)+import Data.Text.IO               (hPutStr)+import Data.Maybe                 (fromMaybe, fromJust)+import Data.Version               (showVersion)+import Data.SBV hiding (Word, solver, verbose, name)+import Data.SBV.Control hiding (Version, timeout, create)+import System.IO                  (hFlush, hPrint, stdout, stderr) import System.Directory           (withCurrentDirectory, listDirectory)-import System.Exit                (die, exitFailure)-import System.IO                  (hFlush, stdout)+import System.Exit                (die, exitFailure, exitWith, ExitCode(..))+import System.Environment         (setEnv) import System.Process             (callProcess)-import System.Timeout             (timeout)+import qualified Data.Aeson        as JSON+import qualified Data.Aeson.Types  as JSON+import Data.Aeson (FromJSON (..), (.:))+import Data.Aeson.Lens hiding (values)+import qualified Data.Vector as V+import qualified Data.ByteString.Lazy  as Lazy  import qualified Data.ByteString        as ByteString-import qualified Data.ByteString.Base16 as BS16 import qualified Data.ByteString.Char8  as Char8 import qualified Data.ByteString.Lazy   as LazyByteString import qualified Data.Map               as Map-import qualified Options.Generic        as Options--import qualified EVM.Facts     as Facts-import qualified EVM.Facts.Git as Git+import qualified Data.Sequence          as Seq+import qualified System.Timeout         as Timeout +import qualified Paths_hevm      as Paths import qualified Text.Regex.TDFA as Regex-import qualified Data.Sequence as Seq +import Options.Generic as Options+ -- This record defines the program's command-line options -- automatically via the `optparse-generic` package.-data Command-  = Exec-      { code       :: ByteString-      , calldata   :: Maybe ByteString-      , address    :: Maybe Addr-      , caller     :: Maybe Addr-      , origin     :: Maybe Addr-      , coinbase   :: Maybe Addr-      , value      :: Maybe W256-      , gas        :: Maybe W256-      , number     :: Maybe W256-      , timestamp  :: Maybe W256-      , gaslimit   :: Maybe W256-      , gasprice   :: Maybe W256-      , difficulty :: Maybe W256-      , debug      :: Bool-      , state      :: Maybe String+data Command w+  = Symbolic -- Symbolically explore an abstract program, or specialized with specified env & calldata+  -- vm opts+      { code          :: w ::: Maybe ByteString <?> "Program bytecode"+      , calldata      :: w ::: Maybe ByteString <?> "Tx: calldata"+      , address       :: w ::: Maybe Addr       <?> "Tx: address"+      , caller        :: w ::: Maybe Addr       <?> "Tx: caller"+      , origin        :: w ::: Maybe Addr       <?> "Tx: origin"+      , coinbase      :: w ::: Maybe Addr       <?> "Block: coinbase"+      , value         :: w ::: Maybe W256       <?> "Tx: Eth amount"+      , nonce         :: w ::: Maybe W256       <?> "Nonce of origin"+      , gas           :: w ::: Maybe W256       <?> "Tx: gas amount"+      , number        :: w ::: Maybe W256       <?> "Block: number"+      , timestamp     :: w ::: Maybe W256       <?> "Block: timestamp"+      , gaslimit      :: w ::: Maybe W256       <?> "Tx: gas limit"+      , gasprice      :: w ::: Maybe W256       <?> "Tx: gas price"+      , create        :: w ::: Bool             <?> "Tx: creation"+      , maxcodesize   :: w ::: Maybe W256       <?> "Block: max code size"+      , difficulty    :: w ::: Maybe W256       <?> "Block: difficulty"+      , chainid       :: w ::: Maybe W256       <?> "Env: chainId"+  -- remote state opts+      , rpc         :: w ::: Maybe URL        <?> "Fetch state from a remote node"+      , block       :: w ::: Maybe W256       <?> "Block state is be fetched from"++  -- symbolic execution opts+      , jsonFile      :: w ::: Maybe String       <?> "Filename or path to dapp build output (default: out/*.solc.json)"+      , dappRoot      :: w ::: Maybe String       <?> "Path to dapp project root directory (default: . )"+      , storageModel  :: w ::: Maybe StorageModel <?> "Select storage model: ConcreteS, SymbolicS (default) or InitialS"+      , sig           :: w ::: Maybe Text         <?> "Signature of types to decode / encode"+      , arg           :: w ::: [String]           <?> "Values to encode"+      , debug         :: w ::: Bool               <?> "Run interactively"+      , getModels     :: w ::: Bool               <?> "Print example testcase for each execution path"+      , smttimeout    :: w ::: Maybe Integer      <?> "Timeout given to SMT solver in milliseconds (default: 20000)"+      , maxIterations :: w ::: Maybe Integer      <?> "Number of times we may revisit a particular branching point"+      , solver        :: w ::: Maybe Text         <?> "Used SMT solver: z3 (default) or cvc4"       }-  | DappTest-      { jsonFile           :: Maybe String-      , dappRoot           :: Maybe String-      , debug              :: Bool-      , rpc                :: Maybe URL-      , verbose            :: Bool-      , coverage           :: Bool-      , state              :: Maybe String-      , match              :: Maybe String+  | Equivalence -- prove equivalence between two programs+      { codeA         :: w ::: ByteString    <?> "Bytecode of the first program"+      , codeB         :: w ::: ByteString    <?> "Bytecode of the second program"+      , sig           :: w ::: Maybe Text    <?> "Signature of types to decode / encode"+      , smttimeout    :: w ::: Maybe Integer <?> "Timeout given to SMT solver in milliseconds (default: 20000)"+      , maxIterations :: w ::: Maybe Integer <?> "Number of times we may revisit a particular branching point"+      , solver        :: w ::: Maybe Text    <?> "Used SMT solver: z3 (default) or cvc4"       }-  | Interactive-      { jsonFile           :: Maybe String-      , dappRoot           :: Maybe String-      , rpc                :: Maybe URL-      , state              :: Maybe String+  | Exec -- Execute a given program with specified env & calldata+      { code        :: w ::: Maybe ByteString <?> "Program bytecode"+      , calldata    :: w ::: Maybe ByteString <?> "Tx: calldata"+      , address     :: w ::: Maybe Addr       <?> "Tx: address"+      , caller      :: w ::: Maybe Addr       <?> "Tx: caller"+      , origin      :: w ::: Maybe Addr       <?> "Tx: origin"+      , coinbase    :: w ::: Maybe Addr       <?> "Block: coinbase"+      , value       :: w ::: Maybe W256       <?> "Tx: Eth amount"+      , nonce       :: w ::: Maybe W256       <?> "Nonce of origin"+      , gas         :: w ::: Maybe W256       <?> "Tx: gas amount"+      , number      :: w ::: Maybe W256       <?> "Block: number"+      , timestamp   :: w ::: Maybe W256       <?> "Block: timestamp"+      , gaslimit    :: w ::: Maybe W256       <?> "Tx: gas limit"+      , gasprice    :: w ::: Maybe W256       <?> "Tx: gas price"+      , create      :: w ::: Bool             <?> "Tx: creation"+      , maxcodesize :: w ::: Maybe W256       <?> "Block: max code size"+      , difficulty  :: w ::: Maybe W256       <?> "Block: difficulty"+      , chainid     :: w ::: Maybe W256       <?> "Env: chainId"+      , debug       :: w ::: Bool             <?> "Run interactively"+      , trace       :: w ::: Bool             <?> "Dump trace"+      , state       :: w ::: Maybe String     <?> "Path to state repository"+      , rpc         :: w ::: Maybe URL        <?> "Fetch state from a remote node"+      , block       :: w ::: Maybe W256       <?> "Block state is be fetched from"+      , jsonFile    :: w ::: Maybe String     <?> "Filename or path to dapp build output (default: out/*.solc.json)"+      , dappRoot    :: w ::: Maybe String     <?> "Path to dapp project root directory (default: . )"       }-  | VmTest-      { file  :: String-      , test  :: [String]-      , debug :: Bool+  | DappTest -- Run DSTest unit tests+      { jsonFile    :: w ::: Maybe String             <?> "Filename or path to dapp build output (default: out/*.solc.json)"+      , dappRoot    :: w ::: Maybe String             <?> "Path to dapp project root directory (default: . )"+      , debug       :: w ::: Bool                     <?> "Run interactively"+      , fuzzRuns    :: w ::: Maybe Int                <?> "Number of times to run fuzz tests"+      , replay      :: w ::: Maybe (Text, ByteString) <?> "Custom fuzz case to run/debug"+      , rpc         :: w ::: Maybe URL                <?> "Fetch state from a remote node"+      , verbose     :: w ::: Maybe Int                <?> "Append call trace: {1} failures {2} all"+      , coverage    :: w ::: Bool                     <?> "Coverage analysis"+      , state       :: w ::: Maybe String             <?> "Path to state repository"+      , match       :: w ::: Maybe String             <?> "Test case filter - only run methods matching regex"       }-  | VmTestReport-      { tests :: String+  | Interactive -- Browse & run unit tests interactively+      { jsonFile :: w ::: Maybe String <?> "Filename or path to dapp build output (default: out/*.solc.json)"+      , dappRoot :: w ::: Maybe String <?> "Path to dapp project root directory (default: . )"+      , rpc      :: w ::: Maybe URL    <?> "Fetch state from a remote node"+      , state    :: w ::: Maybe String <?> "Path to state repository"+      , replay   :: w ::: Maybe (Text, ByteString) <?> "Custom fuzz case to run/debug"       }-  | Flatten-    { sourceFile :: String-    , jsonFile   :: Maybe String-    , dappRoot   :: Maybe String+  | BcTest -- Run an Ethereum Blockhain/GeneralState test+      { file    :: w ::: String    <?> "Path to .json test file"+      , test    :: w ::: [String]  <?> "Test case filter - only run specified test method(s)"+      , debug   :: w ::: Bool      <?> "Run interactively"+      , diff    :: w ::: Bool      <?> "Print expected vs. actual state on failure"+      , timeout :: w ::: Maybe Int <?> "Execution timeout (default: 10 sec.)"+      }+  | Compliance -- Run Ethereum Blockhain compliance report+      { tests   :: w ::: String       <?> "Path to Ethereum Tests directory"+      , group   :: w ::: Maybe String <?> "Report group to run: VM or Blockchain (default: Blockchain)"+      , match   :: w ::: Maybe String <?> "Test case filter - only run methods matching regex"+      , skip    :: w ::: Maybe String <?> "Test case filter - skip tests containing string"+      , html    :: w ::: Bool         <?> "Output html report"+      , timeout :: w ::: Maybe Int    <?> "Execution timeout (default: 10 sec.)"+      }+  | Flatten -- Concat all dependencies for a given source file+    { sourceFile :: w ::: String       <?> "Path to solidity source file e.g. src/contract.sol"+    , jsonFile   :: w ::: Maybe String <?> "Filename or path to dapp build output (default: out/*.solc.json)"+    , dappRoot   :: w ::: Maybe String <?> "Path to dapp project root directory (default: . )"     }   | Emacs-  deriving (Show, Options.Generic, Eq)+  | Version+  | Rlp  -- RLP decode a string and print the result+  { decode :: w ::: ByteString <?> "RLP encoded hexstring"+  }+  | Abiencode+  { abi  :: w ::: Maybe String <?> "Signature of types to decode / encode"+  , arg  :: w ::: [String]     <?> "Values to encode"+  }+  | MerkleTest -- Insert a set of key values and check against the given root+  { file :: w ::: String <?> "Path to .json test file"+  }+  | StripMetadata -- Remove metadata from contract bytecode+  { code        :: w ::: Maybe ByteString       <?> "Program bytecode"+  } +  deriving (Options.Generic)+ type URL = Text -instance Options.ParseRecord Command where++-- For some reason haskell can't derive a+-- parseField instance for (Text, ByteString)+instance Options.ParseField (Text, ByteString)++instance Options.ParseRecord (Command Options.Wrapped) where   parseRecord =     Options.parseRecordWithModifiers Options.lispCaseModifiers -optsMode :: Command -> Mode+optsMode :: Command Options.Unwrapped -> Mode optsMode x = if debug x then Debug else Run -unitTestOptions :: Command -> IO UnitTestOptions-unitTestOptions cmd = do+unitTestOptions :: Command Options.Unwrapped -> String -> IO UnitTestOptions+unitTestOptions cmd testFile = do+  let root = fromMaybe "." (dappRoot cmd)+  srcInfo <- readSolc testFile >>= \case+    Nothing -> error "Could not read .sol.json file"+    Just (contractMap, sourceCache) ->+      pure $ dappInfo root contractMap sourceCache+   vmModifier <-     case state cmd of       Nothing ->@@ -137,45 +243,64 @@    params <- getParametersFromEnvironmentVariables +  let+    testn = testNumber params+    block' = if 0 == testn+       then EVM.Fetch.Latest+       else EVM.Fetch.BlockNumber testn+   pure EVM.UnitTest.UnitTestOptions     { EVM.UnitTest.oracle =         case rpc cmd of-         Just url -> EVM.Fetch.http (EVM.Fetch.BlockNumber (testNumber params)) url+         Just url -> EVM.Fetch.http block' url          Nothing  -> EVM.Fetch.zero     , EVM.UnitTest.verbose = verbose cmd     , EVM.UnitTest.match   = pack $ fromMaybe "^test" (match cmd)+    , EVM.UnitTest.fuzzRuns = fromMaybe 100 (fuzzRuns cmd)+    , EVM.UnitTest.replay   = do+        arg' <- replay cmd+        return (fst arg', LazyByteString.fromStrict (hexByteString "--replay" $ strip0x $ snd arg'))     , EVM.UnitTest.vmModifier = vmModifier     , EVM.UnitTest.testParams = params+    , EVM.UnitTest.dapp = srcInfo     }  main :: IO () main = do-  cmd <- Options.getRecord "hevm -- Ethereum evaluator"+  cmd <- Options.unwrapRecord "hevm -- Ethereum evaluator"   let     root = fromMaybe "." (dappRoot cmd)   case cmd of+    Version {} -> putStrLn (showVersion Paths.version)+    Symbolic {} -> assert cmd+    Equivalence {} -> equivalence cmd     Exec {} ->       launchExec cmd-    VmTest {} ->-      launchVMTest cmd+    Abiencode {} ->+      print . ByteStringS $ abiencode (abi cmd) (arg cmd)+    BcTest {} ->+      launchTest cmd     DappTest {} ->       withCurrentDirectory root $ do         testFile <- findJsonFile (jsonFile cmd)-        testOpts <- unitTestOptions cmd-        case coverage cmd of-          False ->+        testOpts <- unitTestOptions cmd testFile+        case (coverage cmd, optsMode cmd) of+          (False, Run) ->             dappTest testOpts (optsMode cmd) testFile-          True ->+          (False, Debug) ->+            EVM.TTY.main testOpts root testFile+          (True, _) ->             dappCoverage testOpts (optsMode cmd) testFile     Interactive {} ->       withCurrentDirectory root $ do         testFile <- findJsonFile (jsonFile cmd)-        testOpts <- unitTestOptions cmd+        testOpts <- unitTestOptions cmd testFile         EVM.TTY.main testOpts root testFile-    VmTestReport {} ->-      withCurrentDirectory (tests cmd) $ do-        dataDir <- Paths.getDataDir-        callProcess "bash" [dataDir ++ "/run-consensus-tests", "."]+    Compliance {} ->+      case (group cmd) of+        Just "Blockchain" -> launchScript "/run-blockchain-tests" cmd+        Just "VM" -> launchScript "/run-consensus-tests" cmd+        _ -> launchScript "/run-blockchain-tests" cmd     Flatten {} ->       withCurrentDirectory root $ do         theJson <- findJsonFile (jsonFile cmd)@@ -188,7 +313,27 @@               error ("Failed to read Solidity JSON for `" ++ theJson ++ "'")     Emacs ->       EVM.Emacs.main+    Rlp {} ->+      case rlpdecode $ hexByteString "--decode" $ strip0x $ decode cmd of+        Nothing -> error "Malformed RLP string"+        Just c -> print c+    MerkleTest {} -> merkleTest cmd+    StripMetadata {} -> print .+      ByteStringS . stripBytecodeMetadata . hexByteString "bytecode" . strip0x $ fromJust $ code cmd +launchScript :: String -> Command Options.Unwrapped -> IO ()+launchScript script cmd =+  withCurrentDirectory (tests cmd) $ do+    dataDir <- Paths.getDataDir+    callProcess "bash"+      [ dataDir ++ script+      , "."+      , show (html cmd)+      , fromMaybe "" (match cmd)+      , fromMaybe "" (skip cmd)+      , show $ fromMaybe 10 (timeout cmd)+      ]+ findJsonFile :: Maybe String -> IO String findJsonFile (Just s) = pure s findJsonFile Nothing = do@@ -210,12 +355,12 @@         ]  dappTest :: UnitTestOptions -> Mode -> String -> IO ()-dappTest opts _ solcFile = do+dappTest opts _ solcFile =   readSolc solcFile >>=     \case       Just (contractMap, cache) -> do         let matcher = regexMatches (EVM.UnitTest.match opts)-        let unitTests = (findUnitTests matcher) (Map.elems contractMap)+            unitTests = (findUnitTests matcher) (Map.elems contractMap)         results <- mapM (runUnitTestContract opts contractMap cache) unitTests         when (any (== False) results) exitFailure       Nothing ->@@ -232,8 +377,154 @@   in     Regex.matchTest regex . Seq.fromList . unpack +equivalence :: Command Options.Unwrapped -> IO ()+equivalence cmd =+  do let bytecodeA = hexByteString "--code" . strip0x $ codeA cmd+         bytecodeB = hexByteString "--code" . strip0x $ codeB cmd+     maybeSignature <- case sig cmd of+       Nothing -> return Nothing+       Just sig' -> do method' <- functionAbi sig'+                       return $ Just (view methodSignature method', snd <$> view methodInputs method')++     void . runSMTWithTimeOut (solver cmd) (smttimeout cmd) . query $+       equivalenceCheck bytecodeA bytecodeB (maxIterations cmd) maybeSignature >>= \case+         Right vm -> do io $ putStrLn "Not equal!"+                        io $ putStrLn "Counterexample:"+                        showCounterexample vm maybeSignature+                        io $ exitFailure+         Left (postAs, postBs) -> io $ do+           putStrLn $ "Explored: " <> show (length postAs)+                       <> " execution paths of A and: "+                       <> show (length postBs) <> " paths of B."+           putStrLn $ "No discrepancies found."+++-- cvc4 sets timeout via a commandline option instead of smtlib `(set-option)`+runSMTWithTimeOut :: Maybe Text -> Maybe Integer -> Symbolic a -> IO a+runSMTWithTimeOut solver maybeTimeout sym+  | solver == Just "cvc4" = do+      setEnv "SBV_CVC4_OPTIONS" ("--lang=smt --incremental --interactive --no-interactive-prompt --model-witness-value --tlimit-per=" <> show timeout)+      a <- runSMTWith cvc4 sym+      setEnv "SBV_CVC4_OPTIONS" ""+      return a+  | solver == Just "z3" = runwithz3+  | solver == Nothing = runwithz3+  | otherwise = error "Unknown solver. Currently supported solvers; z3, cvc4"+ where timeout = fromMaybe 20000 maybeTimeout+       runwithz3 = runSMTWith z3 $ (setTimeOut timeout) >> sym+++checkForVMErrors :: [EVM.VM] -> [String]+checkForVMErrors [] = []+checkForVMErrors (vm:vms) =+  case view EVM.result vm of+    Just (EVM.VMFailure EVM.UnexpectedSymbolicArg) ->+      ("Unexpected symbolic argument at opcode: "+      <> maybe "??" show (EVM.vmOp vm)+      <> ". Not supported (yet!)"+      ) : checkForVMErrors vms+    _ ->+      checkForVMErrors vms++emptyDapp :: DappInfo+emptyDapp = dappInfo "" mempty (SourceCache mempty mempty mempty mempty)++getSrcInfo :: Command Options.Unwrapped -> IO DappInfo+getSrcInfo cmd =+  let root = fromMaybe "." (dappRoot cmd)+  in case (jsonFile cmd) of+    Nothing ->+      pure $ emptyDapp+    Just json -> readSolc json >>= \case+      Nothing ->+        pure $ emptyDapp+      Just (contractMap, sourceCache) ->+        pure $ dappInfo root contractMap sourceCache++-- Although it is tempting to fully abstract calldata and give any hints about+-- the nature of the signature doing so results in significant time spent in+-- consulting z3 about rather trivial matters. But with cvc4 it is quite+-- pleasant!++-- If function signatures are known, they should always be given for best results.+assert :: Command Options.Unwrapped -> IO ()+assert cmd = do+  let block'  = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd)+      rpcinfo = (,) block' <$> rpc cmd+      model = fromMaybe (if create cmd then InitialS else SymbolicS) (storageModel cmd)+  srcInfo <- getSrcInfo cmd+  maybesig <- case sig cmd of+    Nothing ->+      return Nothing+    Just sig' -> do+      method' <- functionAbi sig'+      let typ = snd <$> view methodInputs method'+          name = view methodSignature method'+      return $ Just (name,typ)+  if debug cmd then+    runSMTWithTimeOut (solver cmd) (smttimeout cmd) $ query $ do+      preState <- symvmFromCommand cmd+      smtState <- queryState+      io $ void $ EVM.TTY.runFromVM+        (maxIterations cmd)+        srcInfo+        (EVM.Fetch.oracle smtState rpcinfo model)+        preState++  else+    runSMTWithTimeOut (solver cmd) (smttimeout cmd) $ query $ do+      preState <- symvmFromCommand cmd+      verify preState (maxIterations cmd) rpcinfo (Just checkAssertions) >>= \case+        Right _ -> do+          io $ putStrLn "Assertion violation found."+          showCounterexample preState maybesig+          io $ exitWith (ExitFailure 1)+        Left (pre, posts) -> do+          io $ putStrLn $ "Explored: " <> show (length posts)+                       <> " branches without assertion violations"+          let vmErrs = checkForVMErrors posts+          unless (null vmErrs) $ io $ do+            putStrLn $+              "However, "+              <> show (length vmErrs)+              <> " branch(es) errored while exploring:"+            print vmErrs+          -- When `--get-models` is passed, we print example vm info for each path+          when (getModels cmd) $+            forM_ (zip [1..] posts) $ \(i, postVM) -> do+              resetAssertions+              constrain (sAnd (view EVM.pathConditions postVM))+              io $ putStrLn $+                "-- Branch (" <> show i <> "/" <> show (length posts) <> ") --"+              checkSat >>= \case+                Unk -> io $ do putStrLn "Timed out"+                               print $ view EVM.result postVM+                Unsat -> io $ do putStrLn "Inconsistent path conditions: dead path"+                                 print $ view EVM.result postVM+                Sat -> do+                  showCounterexample pre maybesig+                  case view EVM.result postVM of+                    Nothing ->+                      error "internal error; no EVM result"+                    Just (EVM.VMFailure (EVM.Revert "")) -> io . putStrLn $+                      "Reverted"+                    Just (EVM.VMFailure (EVM.Revert msg)) -> io . putStrLn $+                      "Reverted: " <> show (ByteStringS msg)+                    Just (EVM.VMFailure err) -> io . putStrLn $+                      "Failed: " <> show err+                    Just (EVM.VMSuccess (ConcreteBuffer msg)) ->+                      if ByteString.null msg+                      then io $ putStrLn+                        "Stopped"+                      else io $ putStrLn $+                        "Returned: " <> show (ByteStringS msg)+                    Just (EVM.VMSuccess (SymbolicBuffer msg)) -> do+                      out <- mapM (getValue.fromSized) msg+                      io . putStrLn $+                        "Returned: " <> show (ByteStringS (ByteString.pack out))+ dappCoverage :: UnitTestOptions -> Mode -> String -> IO ()-dappCoverage opts _ solcFile = do+dappCoverage opts _ solcFile =   readSolc solcFile >>=     \case       Just (contractMap, cache) -> do@@ -262,9 +553,11 @@       Nothing ->         error ("Failed to read Solidity JSON for `" ++ solcFile ++ "'") -launchExec :: Command -> IO ()+launchExec :: Command Options.Unwrapped -> IO () launchExec cmd = do-  let vm = vmFromCommand cmd+  dapp <- getSrcInfo cmd++  vm <- vmFromCommand cmd   vm1 <- case state cmd of     Nothing -> pure vm     Just path ->@@ -274,57 +567,248 @@       Facts.apply vm <$> Git.loadFacts (Git.RepoAt path)    case optsMode cmd of-    Run ->-      let vm' = execState exec vm1-      in case view EVM.result vm' of+    Run -> do+      vm' <- execStateT (interpret fetcher Nothing . void $ EVM.Stepper.execFully) vm1+      when (trace cmd) $ hPutStr stderr (showTraceTree dapp vm')+      case view EVM.result vm' of         Nothing ->           error "internal error; no EVM result"-        Just (EVM.VMFailure e) -> do-          die (show e)-        Just (EVM.VMSuccess x) -> do-          let hex = BS16.encode x-          if ByteString.null hex then pure ()-            else do-              ByteString.putStr hex-              putStrLn ""+        Just (EVM.VMFailure (EVM.Revert msg)) -> do+          print $ ByteStringS msg+          exitWith (ExitFailure 2)+        Just (EVM.VMFailure err) -> do+          print err+          exitWith (ExitFailure 2)+        Just (EVM.VMSuccess buf) -> do+          let msg = case buf of+                SymbolicBuffer msg' -> forceLitBytes msg'+                ConcreteBuffer msg' -> msg'+          print $ ByteStringS msg           case state cmd of             Nothing -> pure ()             Just path ->               Git.saveFacts (Git.RepoAt path) (Facts.vmFacts vm')-    Debug ->-      void (EVM.TTY.runFromVM vm1)+    Debug -> void $ EVM.TTY.runFromVM Nothing dapp fetcher vm1+   where fetcher = maybe EVM.Fetch.zero (EVM.Fetch.http block') (rpc cmd)+         block'  = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd) -vmFromCommand :: Command -> EVM.VM-vmFromCommand cmd =-  vm1 & EVM.env . EVM.contracts . ix address' . EVM.balance +~ (w256 value')+data Testcase = Testcase {+  _entries :: [(Text, Maybe Text)],+  _root :: Text+} deriving Show++parseTups :: JSON.Value -> JSON.Parser [(Text, Maybe Text)]+parseTups (JSON.Array arr) = do+  tupList <- mapM parseJSON (V.toList arr)+  mapM (\[k, v] -> do+                  rhs <- parseJSON v+                  lhs <- parseJSON k+                  return (lhs, rhs))+         tupList+parseTups invalid = JSON.typeMismatch "Malformed array" invalid+++parseTrieTest :: JSON.Object -> JSON.Parser Testcase+parseTrieTest p = do+  kvlist <- p .: "in"+  entries <- parseTups kvlist+  root <- p .: "root"+  return $ Testcase entries root++instance FromJSON Testcase where+  parseJSON (JSON.Object p) = parseTrieTest p+  parseJSON invalid = JSON.typeMismatch "Merkle test case" invalid++parseTrieTests :: Lazy.ByteString -> Either String (Map String Testcase)+parseTrieTests = JSON.eitherDecode'++merkleTest :: Command Options.Unwrapped -> IO ()+merkleTest cmd = do+  parsed <- parseTrieTests <$> LazyByteString.readFile (file cmd)+  case parsed of+    Left err -> print err+    Right testcases -> mapM_ runMerkleTest testcases++runMerkleTest :: Testcase -> IO ()+runMerkleTest (Testcase entries root) =+  case Patricia.calcRoot entries' of+    Nothing ->+      error "Test case failed"+    Just n ->+      case n == strip0x (hexText root) of+        True ->+          putStrLn "Test case success"+        False ->+          error ("Test case failure; expected " <> show root+                 <> " but got " <> show (ByteStringS n))+  where entries' = fmap (\(k, v) ->+                           (tohexOrText k,+                            tohexOrText (fromMaybe mempty v)))+                   entries++tohexOrText :: Text -> ByteString+tohexOrText s = case "0x" `Char8.isPrefixOf` encodeUtf8 s of+                  True -> hexText s+                  False -> encodeUtf8 s++-- | Creates a (concrete) VM from command line options+vmFromCommand :: Command Options.Unwrapped -> IO EVM.VM+vmFromCommand cmd = do+  vm <- case (rpc cmd, address cmd) of+    (Just url, Just addr') -> do+      EVM.Fetch.fetchContractFrom block' url addr' >>= \case+        Nothing -> error $ "contract not found: " <> show address'+        Just contract' -> case code cmd of+          Nothing -> return (vm1 contract')+          -- if both code and url is given,+          -- fetch the contract and overwrite the code+          Just c -> return . vm1 $+            EVM.initialContract  (codeType $ hexByteString "--code" $ strip0x c)+              & set EVM.storage  (view EVM.storage  contract')+              & set EVM.balance  (view EVM.balance  contract')+              & set EVM.nonce    (view EVM.nonce    contract')+              & set EVM.external (view EVM.external contract')++    _ -> return . vm1 . EVM.initialContract . codeType $ bytes code ""++  return $ vm & EVM.env . EVM.contracts . ix address' . EVM.balance +~ (w256 value')+      where+        decipher = hexByteString "bytes" . strip0x+        block'   = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd)+        value'   = word value 0+        caller'  = addr caller 0+        origin'  = addr origin 0+        calldata' = ConcreteBuffer $ bytes calldata ""+        codeType = if create cmd then EVM.InitCode else EVM.RuntimeCode+        address' = if create cmd+              then createAddress origin' (word nonce 0)+              else addr address 0xacab++        vm1 c = EVM.makeVm $ EVM.VMOpts+          { EVM.vmoptContract      = c+          , EVM.vmoptCalldata      = (calldata', literal . num $ len calldata')+          , EVM.vmoptValue         = w256lit value'+          , EVM.vmoptAddress       = address'+          , EVM.vmoptCaller        = litAddr caller'+          , EVM.vmoptOrigin        = origin'+          , EVM.vmoptGas           = word gas 0+          , EVM.vmoptGaslimit      = word gas 0+          , EVM.vmoptCoinbase      = addr coinbase 0+          , EVM.vmoptNumber        = word number 0+          , EVM.vmoptTimestamp     = word timestamp 0+          , EVM.vmoptBlockGaslimit = word gaslimit 0+          , EVM.vmoptGasprice      = word gasprice 0+          , EVM.vmoptMaxCodeSize   = word maxcodesize 0xffffffff+          , EVM.vmoptDifficulty    = word difficulty 0+          , EVM.vmoptSchedule      = FeeSchedule.istanbul+          , EVM.vmoptChainId       = word chainid 1+          , EVM.vmoptCreate        = create cmd+          , EVM.vmoptStorageModel  = ConcreteS+          }+        word f def = fromMaybe def (f cmd)+        addr f def = fromMaybe def (f cmd)+        bytes f def = maybe def decipher (f cmd)++symvmFromCommand :: Command Options.Unwrapped -> Query EVM.VM+symvmFromCommand cmd = do+  caller' <- maybe (SAddr <$> freshVar_) (return . litAddr) (caller cmd)+  callvalue' <- maybe (sw256 <$> freshVar_) (return . w256lit) (value cmd)+  (calldata', cdlen, pathCond) <- case (calldata cmd, sig cmd) of+    -- fully abstract calldata (up to 1024 bytes)+    (Nothing, Nothing) -> do+      cd <- sbytes256+      len <- freshVar_+      return (SymbolicBuffer cd, len, len .<= 256)+    -- fully concrete calldata+    (Just c, Nothing) ->+      let cd = ConcreteBuffer $ decipher c+      in return (cd, num (len cd), sTrue)+    -- calldata according to given abi with possible specializations from the `arg` list+    (Nothing, Just sig') -> do+      method' <- io $ functionAbi sig'+      let typs = snd <$> view methodInputs method'+      (cd, cdlen) <- symCalldata (view methodSignature method') typs (arg cmd)+      return (SymbolicBuffer cd, cdlen, sTrue)++    _ -> error "incompatible options: calldata and abi"++  store <- case storageModel cmd of+    -- InitialS and SymbolicS can read and write to symbolic locations+    -- ConcreteS cannot (instead values can be fetched from rpc!)+    -- Initial defaults to 0 for uninitialized storage slots,+    -- whereas the values of SymbolicS are unconstrained.+    Just InitialS  -> EVM.Symbolic <$> freshArray_ (Just 0)+    Just ConcreteS -> return (EVM.Concrete mempty)+    Just SymbolicS -> EVM.Symbolic <$> freshArray_ Nothing+    Nothing -> EVM.Symbolic <$> freshArray_ (if create cmd then (Just 0) else Nothing)++  vm <- case (rpc cmd, address cmd, code cmd) of+    (Just url, Just addr', _) ->+      io (EVM.Fetch.fetchContractFrom block' url addr') >>= \case+        Nothing ->+          error $ "contract not found."+        Just contract' ->+          return $+            vm1 cdlen calldata' callvalue' caller' (contract'' & set EVM.storage store)+          where+            contract'' = case code cmd of+              Nothing -> contract'+              -- if both code and url is given,+              -- fetch the contract and overwrite the code+              Just c -> EVM.initialContract (codeType $ decipher c)+                        & set EVM.storage     (view EVM.storage contract')+                        & set EVM.origStorage (view EVM.origStorage contract')+                        & set EVM.balance     (view EVM.balance contract')+                        & set EVM.nonce       (view EVM.nonce contract')+                        & set EVM.external    (view EVM.external contract')++    (_, _, Just c)  ->+      return $+        vm1 cdlen calldata' callvalue' caller' $+          (EVM.initialContract . codeType $ decipher c) & set EVM.storage store+    (_, _, Nothing) ->+      error $ "must provide at least (rpc + address) or code"++  return $ vm & over EVM.pathConditions (<> [pathCond])+   where-    value'   = word value 0-    address' = addr address 1-    vm1 = EVM.makeVm $ EVM.VMOpts-      { EVM.vmoptCode       = hexByteString "--code" (code cmd)-      , EVM.vmoptCalldata   = maybe "" (hexByteString "--calldata")-                                (calldata cmd)-      , EVM.vmoptValue      = value'-      , EVM.vmoptAddress    = address'-      , EVM.vmoptCaller     = addr caller 2-      , EVM.vmoptOrigin     = addr origin 3-      , EVM.vmoptGas        = word gas 0-      , EVM.vmoptCoinbase   = addr coinbase 0-      , EVM.vmoptNumber     = word number 0-      , EVM.vmoptTimestamp  = word timestamp 0-      , EVM.vmoptGaslimit   = word gaslimit 0-      , EVM.vmoptGasprice   = word gasprice 0-      , EVM.vmoptDifficulty = word difficulty 0-      , EVM.vmoptSchedule   = FeeSchedule.metropolis+    decipher = hexByteString "bytes" . strip0x+    block'   = maybe EVM.Fetch.Latest EVM.Fetch.BlockNumber (block cmd)+    origin'  = addr origin 0+    codeType = if create cmd then EVM.InitCode else EVM.RuntimeCode+    address' = if create cmd+          then createAddress origin' (word nonce 0)+          else addr address 0xacab+    vm1 cdlen calldata' callvalue' caller' c = EVM.makeVm $ EVM.VMOpts+      { EVM.vmoptContract      = c+      , EVM.vmoptCalldata      = (calldata', cdlen)+      , EVM.vmoptValue         = callvalue'+      , EVM.vmoptAddress       = address'+      , EVM.vmoptCaller        = caller'+      , EVM.vmoptOrigin        = origin'+      , EVM.vmoptGas           = word gas 0xffffffffffffffff+      , EVM.vmoptGaslimit      = word gas 0xffffffffffffffff+      , EVM.vmoptCoinbase      = addr coinbase 0+      , EVM.vmoptNumber        = word number 0+      , EVM.vmoptTimestamp     = word timestamp 0+      , EVM.vmoptBlockGaslimit = word gaslimit 0+      , EVM.vmoptGasprice      = word gasprice 0+      , EVM.vmoptMaxCodeSize   = word maxcodesize 0xffffffff+      , EVM.vmoptDifficulty    = word difficulty 0+      , EVM.vmoptSchedule      = FeeSchedule.istanbul+      , EVM.vmoptChainId       = word chainid 1+      , EVM.vmoptCreate        = create cmd+      , EVM.vmoptStorageModel  = fromMaybe SymbolicS (storageModel cmd)       }-    word f def = maybe def id (f cmd)-    addr f def = maybe def id (f cmd)+    word f def = fromMaybe def (f cmd)+    addr f def = fromMaybe def (f cmd) -launchVMTest :: Command -> IO ()-launchVMTest cmd =+launchTest :: Command Options.Unwrapped ->  IO ()+launchTest cmd = do #if MIN_VERSION_aeson(1, 0, 0)-  VMTest.parseSuite <$> LazyByteString.readFile (file cmd) >>=-   \case+  parsed <- VMTest.parseBCSuite <$> LazyByteString.readFile (file cmd)+  case parsed of+     Left "No cases to check." -> putStrLn "no-cases ok"      Left err -> print err      Right allTests ->        let testFilter =@@ -332,40 +816,55 @@              then id              else filter (\(x, _) -> elem x (test cmd))        in-         mapM_ (runVMTest (optsMode cmd)) $+         mapM_ (runVMTest (diff cmd) (optsMode cmd) (timeout cmd)) $            testFilter (Map.toList allTests) #else   putStrLn "Not supported" #endif  #if MIN_VERSION_aeson(1, 0, 0)-runVMTest :: Mode -> (String, VMTest.Case) -> IO Bool-runVMTest mode (name, x) = do-  let-    vm0 = VMTest.vmForCase x-    m = void EVM.Stepper.execFully >> EVM.Stepper.evm EVM.finalize-+runVMTest :: Bool -> Mode -> Maybe Int -> (String, VMTest.Case) -> IO Bool+runVMTest diffmode mode timelimit (name, x) =+ do+  let vm0 = VMTest.vmForCase x   putStr (name ++ " ")   hFlush stdout   result <- do     action <- async $       case mode of         Run ->-          timeout (1e6) . evaluate $ do-            execState (VMTest.interpret m) vm0+          Timeout.timeout (1e6 * (fromMaybe 10 timelimit)) $+            execStateT (EVM.Stepper.interpret EVM.Fetch.zero . void $ EVM.Stepper.execFully) vm0         Debug ->-          Just <$> EVM.TTY.runFromVM vm0+          Just <$> EVM.TTY.runFromVM Nothing emptyDapp EVM.Fetch.zero vm0     waitCatch action   case result of     Right (Just vm1) -> do-      ok <- VMTest.checkExpectation x vm1+      ok <- VMTest.checkExpectation diffmode x vm1       putStrLn (if ok then "ok" else "")       return ok     Right Nothing -> do       putStrLn "timeout"       return False-    Left _ -> do-      putStrLn "error"+    Left e -> do+      putStrLn $ "error: " ++ if diffmode+        then show e+        else (head . lines . show) e       return False  #endif++parseAbi :: (AsValue s) => s -> (Text, [AbiType])+parseAbi abijson =+  (signature abijson, snd+    <$> parseMethodInput+    <$> V.toList+      (fromMaybe (error "Malformed function abi") (abijson ^? key "inputs" . _Array)))++abiencode :: (AsValue s) => Maybe s -> [String] -> ByteString+abiencode Nothing _ = error "missing required argument: abi"+abiencode (Just abijson) args =+  let (sig', declarations) = parseAbi abijson+  in if length declarations == length args+     then abiMethod sig' $ AbiTuple . V.fromList $ zipWith makeAbiValue declarations args+     else error $ "wrong number of arguments:" <> show (length args) <> ": " <> show args

@@ -1,7 +1,8 @@+cabal-version: 2.2 name:   hevm version:-  0.24+  0.41.0 synopsis:   Ethereum virtual machine evaluator description:@@ -12,20 +13,19 @@ homepage:   https://github.com/dapphub/dapptools license:-  AGPL-3+  AGPL-3.0-only license-file:   COPYING author:-  Mikael Brockman+  Mikael Brockman, Martin Lundfall maintainer:-  mikael@brockman.se+  mikael@brockman.se, martin.lundfall@gmail.com category:   Ethereum build-type:   Simple-cabal-version:-  >=1.10 data-files:+  run-blockchain-tests   run-consensus-tests extra-source-files:   CHANGELOG.md@@ -38,6 +38,7 @@     EVM.Dapp,     EVM.Dev,     EVM.Debug,+    EVM.Demand,     EVM.Emacs,     EVM.Exec,     EVM.Facts,@@ -47,73 +48,88 @@     EVM.Fetch,     EVM.FeeSchedule,     EVM.Hexdump,+    EVM.Keccak,     EVM.Op,+    EVM.Patricia,     EVM.Precompiled,-    EVM.Keccak,+    EVM.RLP,     EVM.Solidity,     EVM.Stepper,     EVM.StorageLayout,+    EVM.Symbolic,+    EVM.SymExec+    EVM.Transaction,     EVM.TTY,     EVM.TTYCenteredList,     EVM.Types,     EVM.UnitTest,-    EVM.VMTest,+    EVM.VMTest+  other-modules:     Paths_hevm+  autogen-modules:+    Paths_hevm   ghc-options:     -Wall -Wno-deprecations   extra-libraries:-    secp256k1+    secp256k1, ff   c-sources:-    ethjet/ethjet.c, ethjet/tinykeccak.c+    ethjet/tinykeccak.c, ethjet/ethjet.c+  cxx-sources:+    ethjet/ethjet-ff.cc, ethjet/blake2.cc+  cxx-options:+    -std=c++0x   install-includes:-    ethjet/ethjet.h, ethjet/tinykeccak.h+    ethjet/tinykeccak.h, ethjet/ethjet.h, ethjet/ethjet-ff.h, ethjet/blake2.h   build-depends:-    QuickCheck                        >= 2.9,-    abstract-par                      >= 0.3,-    aeson                             >= 1.0,-    ansi-wl-pprint                    >= 0.6,-    base                              >= 4.9 && < 5,-    base16-bytestring                 >= 0.1,-    base64-bytestring                 >= 1.0,-    binary                            >= 0.8,-    brick                             >= 0.18,-    bytestring                        >= 0.10,-    cereal                            >= 0.5,-    containers                        >= 0.5,-    cryptonite                        >= 0.21,-    data-dword                        >= 0.3,-    deepseq                           >= 1.4,-    directory                         >= 1.3,-    filepath                          >= 1.4,-    fgl                               >= 5.0,-    ghci-pretty                       >= 0.0,-    haskeline                         >= 0.7,-    time                              >= 1.8,-    transformers                      >= 0.5,-    lens                              >= 4.15,-    lens-aeson                        >= 1.0,-    megaparsec                        >= 6.0,-    memory                            >= 0.14,-    monad-par                         >= 0.3,-    mtl                               >= 2.2,-    multiset                          >= 0.3,-    operational                       >= 0.2,-    optparse-generic                  >= 1.1,-    process                           >= 1.4,-    quickcheck-text                   >= 0.1,-    readline                          >= 1.0,-    restless-git                      >= 0.7,-    rosezipper                        >= 0.2,-    scientific                        >= 0.3,-    s-cargot                          >= 0.1,-    temporary                         >= 1.2,-    text                              >= 1.2,-    text-format                       >= 0.3,+    QuickCheck                        >= 2.13.2 && < 2.14,+    containers                        >= 0.6.0 && < 0.7,+    deepseq                           >= 1.4.4 && < 1.5,+    time                              >= 1.8.0 && < 1.9,+    transformers                      >= 0.5.6 && < 0.6,     tree-view                         == 0.5,-    unordered-containers              >= 0.2,-    vector                            >= 0.11,-    vty                               >= 5.15,-    wreq                              >= 0.5+    abstract-par                      >= 0.3.3 && < 0.4,+    aeson                             >= 1.4.6 && < 1.5,+    bytestring                        >= 0.10.8 && < 0.11,+    scientific                        >= 0.3.6 && < 0.4,+    binary                            >= 0.8.6 && < 0.9,+    text                              >= 1.2.3 && < 1.3,+    unordered-containers              >= 0.2.10 && < 0.3,+    vector                            >= 0.12.1 && < 0.13,+    ansi-wl-pprint                    >= 0.6.9 && < 0.7,+    base16-bytestring                 >= 0.1.1 && < 0.2,+    brick                             >= 0.47.1 && < 0.48,+    megaparsec                        >= 7.0.5 && < 7.1,+    mtl                               >= 2.2.2 && < 2.3,+    directory                         >= 1.3.3 && < 1.4,+    filepath                          >= 1.4.2 && < 1.5,+    vty                               >= 5.25.1 && < 5.26,+    cborg                             >= 0.2.2 && < 0.3,+    cereal                            >= 0.5.8 && < 0.6,+    cryptonite                        >= 0.25 && < 0.26,+    memory                            >= 0.14.18 && < 0.15,+    data-dword                        >= 0.3.1 && < 0.4,+    fgl                               >= 5.7.0 && < 5.8,+    free                              >= 5.1.3 && < 5.2,+    haskeline                         >= 0.7.4 && < 0.8,+    process                           >= 1.6.5 && < 1.7,+    lens                              >= 4.17.1 && < 4.18,+    lens-aeson                        >= 1.0.2 && < 1.1,+    monad-par                         >= 0.3.5 && < 0.4,+    multiset                          >= 0.3.4 && < 0.4,+    operational                       >= 0.2.3 && < 0.3,+    optparse-generic                  >= 1.3.1 && < 1.4,+    quickcheck-text                   >= 0.1.2 && < 0.2,+    restless-git                      >= 0.7 && < 0.8,+    rosezipper                        >= 0.2 && < 0.3,+    s-cargot                          >= 0.1.4 && < 0.2,+    sbv                               >= 8.7.5 && < 8.8,+    semver-range                      >= 0.2.7 && < 0.3,+    temporary                         >= 1.3 && < 1.4,+    text-format                       >= 0.3.2 && < 0.4,+    witherable                        >= 0.3.5 && < 0.4,+    wreq                              >= 0.5.3 && < 0.6,+    regex-tdfa                        >= 1.2.3 && < 1.3,+    base                              >= 4.9 && < 5   hs-source-dirs:     src   default-language:@@ -140,40 +156,44 @@     hevm-cli.hs   ghc-options:     -Wall -threaded -with-rtsopts=-N+  other-modules:+    Paths_hevm+  if os(darwin)+    ld-options: -Wl,-keep_dwarf_unwind   build-depends:-    QuickCheck                        >= 2.9,-    aeson                             >= 1.0,-    ansi-wl-pprint                    >= 0.6,-    async                             == 2.*,-    base                              >= 4.9 && < 5,-    base16-bytestring                 >= 0.1,-    base64-bytestring                 >= 1.0,-    binary                            >= 0.8,-    brick                             >= 0.18,-    bytestring                        >= 0.10,-    containers                        >= 0.5,-    cryptonite                        >= 0.21,-    data-dword                        >= 0.3,-    deepseq                           >= 1.4,-    directory                         >= 1.3,-    filepath                          >= 1.4,-    ghci-pretty                       >= 0.0,+    QuickCheck,+    aeson,+    ansi-wl-pprint,+    async,+    base,+    base16-bytestring,+    binary,+    brick,+    bytestring,+    containers,+    cryptonite,+    data-dword,+    deepseq,+    directory,+    filepath,+    free,     hevm,-    lens                              >= 4.15,-    lens-aeson                        >= 1.0,-    memory                            >= 0.14,-    mtl                               >= 2.2,-    optparse-generic                  >= 1.1,-    process                           >= 1.4,-    quickcheck-text                   >= 0.1,-    readline                          >= 1.0,-    regex-tdfa                        >= 1.2,-    temporary                         >= 1.2,-    text                              >= 1.2,-    text-format                       >= 0.3,-    unordered-containers              >= 0.2,-    vector                            >= 0.11,-    vty                               >= 5.15+    lens,+    lens-aeson,+    memory,+    mtl,+    optparse-generic,+    operational,+    process,+    quickcheck-text,+    regex-tdfa,+    sbv,+    temporary,+    text,+    text-format,+    unordered-containers,+    vector,+    vty  test-suite test   default-language:@@ -190,18 +210,20 @@     secp256k1   build-depends:     HUnit >= 1.6,-    QuickCheck >= 2.9,-    base >= 4.9 && < 5,-    base16-bytestring >= 0.1,-    ghci-pretty >= 0.0.2,+    QuickCheck,+    base,+    base16-bytestring,+    binary,+    containers,+    bytestring,+    free,+    here,     hevm,+    lens,+    mtl,     tasty >= 1.0,     tasty-hunit >= 0.10,     tasty-quickcheck >= 0.9,-    mtl >= 2.2,-    lens >= 4.16,-    text >= 1.2,-    here >= 1.2,-    bytestring >= 0.10,-    vector >= 0.12,-    binary >= 0.8+    text,+    vector,+    sbv

@@ -0,0 +1,136 @@+#!/usr/bin/env bash+set -e++# Invoke with hevm e.g.+# hevm compliance --tests ~/ethereum-tests --skip modexp --timeout 20 --html++HEVM=${HEVM:-hevm}++if [[ "$#" -lt 1 ]]; then+  echo >&2 "usage: $(basename "$0") <tests-dir>"+  exit 1+fi++tests=$1+html=$2+match=$3+skip=$4+timeout=${5:-10}++_html () {+cat <<.+<!doctype html>+<title>hevm test results</title>+<style>+* { font-family:+"latin modern mono", "fantasque sans mono",+inconsolata, menlo, monospace;+font-size: 22px;+line-height: 26px; }+body { margin: 2rem; }+header { text-align: center; margin: 4rem 0; }+table { border-collapse: collapse; width: 100%; }+tr:nth-child(even) { background: rgba(0, 0, 0, 0.05); }+td:not(:first-child):not(:last-child) { padding: 0 1rem; }+.category { opacity: 0.6; text-align: right }+a { color: darkblue; text-decoration: none; }+h1, h2 { text-align: center; margin-top: 2rem  }+.testcase { font-weight: bold }+#failed .testcase { color: rgb(200, 0, 0) }+#balancefailed .testcase { color: rgb(200, 200, 0) }+#passed .testcase { color: rgb(0, 150, 0) }+#skipped .testcase { color: rgb(0, 100, 250) }+#timeout .testcase { color: rgb(0, 0, 250) }+</style>+<header>+<h1>hevm consensus test report</h1>+<p>$(date +%Y-%m-%d)</p>+<p>$(echo "$npass passed, $nbal bad-balance, $nnon bad-nonce, $nstr bad-storage, $nfail failed, $nskip skipped, $ntime timeout")</p>+(Test suite: <span class=GeneralStateTests</span>GeneralStateTests</span> for Istanbul)+</header>+<h2>Failed tests</h2>+<table id=failed>+<tbody>+$(echo $noncefailed)+$(echo $storagefailed)+$(echo $failed)+</table>+<h2>Failed tests (due to balance only)</h2>+<table id=balancefailed>+<tbody>+$(echo $balancefailed)+</table>+<h2>Timeout tests</h2>+<table id=timeout>+<tbody>+$(echo $timeouts)+</table>+<h2>Skipped tests</h2>+<table id=skipped>+<tbody>+$(echo $skipped)+</table>+<h2>Passed tests</h2>+<table id=passed>+<tbody>+$(echo $passed)+</table>+.+}++shopt -s nocasematch+{+  cd "$tests"+  for x in BlockchainTests/GeneralStateTests/*/*; do+    if [[ $x =~ .*$match.* ]] && [[ -n $skip && $x =~ .*$skip.* ]]; then+      for job in $(<$x jq '.|keys[]' -r); do+        echo -n "$job " ; echo "skip"+      done+    elif [[ $x =~ .*$match.* ]]; then+      set +e+      "$HEVM" bc-test --file $x --timeout $timeout 2>&1+      set -e+    fi+  done+} | {+  while read test outcome; do+    echo >&2 "$test $outcome"+    row="<tr><td class=testcase>$test<td>$outcome"+    row+=$'\n'+    case $outcome in+      ok)          passed+=$row ;;+      bad-balance) balancefailed+=$row ;;+      bad-nonce)   noncefailed+=$row ;;+      bad-storage) storagefailed+=$row ;;+      timeout)     timeouts+=$row ;;+      skip)        skipped+=$row ;;+      *)           failed+=$row ;;+    esac+  done++  sum () { echo -ne "$1" | wc -l | awk '{print $1}'; }++  npass=$(sum "$passed")+  nbal=$(sum "$balancefailed")+  nnon=$(sum "$noncefailed")+  nstr=$(sum "$storagefailed")+  nfail=$(sum "$failed")+  ntime=$(sum "$timeouts")+  nskip=$(sum "$skipped")++  echo >&2 "passed: $npass"+  echo >&2 "bad-balance: $nbal"+  echo >&2 "bad-nonce: $nnon"+  echo >&2 "bad-storage: $nstr"+  echo >&2 "failed: $nfail"+  echo >&2 "timeout: $ntime"+  echo >&2 "skipped: $nskip"++  if [[ $html == "True" ]]; then+    _html+  fi++  nbad=$(($nbal + $nnon + $nstr + $nfail))++  [[ $nbad -gt 0 ]] && exit 1 || exit 0+}

@@ -1,41 +1,32 @@ #!/usr/bin/env bash set -e -if [[ $# != 1 ]]; then+# Invoke with hevm e.g.+# hevm compliance --tests ~/ethereum-tests --group VM --skip quadratic --html++HEVM=${HEVM:-hevm}++if [[ "$#" -lt 1 ]]; then   echo >&2 "usage: $(basename "$0") <tests-dir>"   exit 1 fi -{-  cd "$1"-  for x in VMTests/*/*; do-    echo >&2 "$x"-    echo -n "$x " ; hevm vm-test --file $x-  done-} | {-  while read path test outcome; do-    category=$(dirname "$path")-    testcase=$(basename "${path%.json}")-    row="<tr><td class=testcase>$testcase<td>$outcome<td class=category>$category"-    row+=$'\n'-    case $outcome in-      ok) passed+=$row ;;-      *)  failed+=$row ;;-    esac-  done-  -  cat <<.+tests=$1+html=$2+match=$3+skip=$4+timeout=${5:-10}++_html() {+cat <<. <!doctype html> <title>hevm test results</title> <style>-* {-  font-family:-    "latin modern mono", "fantasque sans mono",-    inconsolata, menlo, monospace;-  font-size: 22px;-  line-height: 26px;-}-+* { font-family:+"latin modern mono", "fantasque sans mono",+inconsolata, menlo, monospace;+font-size: 22px;+line-height: 26px; } body { margin: 2rem; } header { text-align: center; margin: 4rem 0; } table { border-collapse: collapse; width: 100%; }@@ -47,36 +38,73 @@ .testcase { font-weight: bold } #failed .testcase { color: rgb(200, 0, 0) } #passed .testcase { color: rgb(0, 150, 0) }+#skipped .testcase { color: rgb(0, 100, 250) } </style> <header> <h1>hevm consensus test report</h1>-<p>-$(date +%Y-%m-%d)-<p>-.--  wc -l <<<"$passed"-  echo "passed, "-  wc -l <<<"$failed"-  echo "failed"-  -  cat <<.-<p>-(Test suite: <span class=VMTests</span>VMTests</span> for Homestead)+<p>$(date +%Y-%m-%d)</p>+<p>$(echo "$npass passed, $nfail failed, $nskip skipped")</p>+(Test suite: <span class=VMTests</span>VMTests</span> for ConstantinopleFix) </header> <h2>Failed tests</h2> <table id=failed> <tbody>-.-  echo "$failed"-  cat <<.+$(echo $failed) </table>+<h2>Skipped tests</h2>+<table id=skipped>+<tbody>+$(echo $skipped)+</table> <h2>Passed tests</h2> <table id=passed> <tbody>-.-  echo "$passed"-  cat <<.+$(echo $passed) </table> .+}++{+  cd "$tests"+  for x in VMTests/*/*; do+    if [[ $x =~ .*$match.* ]] && [[ -n $skip && $x =~ .*$skip.* ]]; then+      for job in $(<$x jq '.|keys[]' -r); do+        echo "$x $job skip"+      done+    elif [[ $x =~ .*$match.* ]]; then+      echo -n "$x " ; "$HEVM" vm-test --file $x --timeout $timeout 2>&1+    fi+  done+} | {+  while read path test outcome; do+    echo >&2 "$path $test $outcome"+    category=$(dirname "$path")+    testcase=$(basename "${path%.json}")+    row="<tr><td class=testcase>$testcase<td>$outcome<td class=category>$category"+    row+=$'\n'+    case $outcome in+      ok)      passed+=$row ;;+      skip)    skipped+=$row ;;+      timeout) timouts+=row ;;+      *)       failed+=$row ;;+    esac+  done++  sum () { echo -ne "$1" | wc -l | awk '{print $1}'; }++  nfail=$(sum "$failed")+  npass=$(sum "$passed")+  nskip=$(sum "$skipped")+  ntime=$(sum "$timeouts")++  echo >&2 "passed: $npass"+  echo >&2 "failed: $nfail"+  echo >&2 "timeout: $ntime"+  echo >&2 "skipped: $nskip"++  if [[ $html == "True" ]]; then+    _html+  fi++  [[ $nfail -gt 0 ]] && exit 1 || exit 0 }

@@ -1,1719 +1,2609 @@ {-# Language ImplicitParams #-} {-# Language ConstraintKinds #-} {-# Language FlexibleInstances #-}-{-# Language GADTs #-}-{-# Language RecordWildCards #-}-{-# Language ScopedTypeVariables #-}-{-# Language StandaloneDeriving #-}-{-# Language StrictData #-}-{-# Language TemplateHaskell #-}-{-# Language TypeOperators #-}-{-# Language ViewPatterns #-}--module EVM where--import Prelude hiding ((^), log, Word, exponent)--import EVM.ABI-import EVM.Types-import EVM.Solidity-import EVM.Keccak-import EVM.Concrete-import EVM.Op-import EVM.FeeSchedule (FeeSchedule (..))--import qualified EVM.Precompiled--import Data.Binary.Get (runGetOrFail)-import Data.Bits (bit, testBit, complement)-import Data.Bits (xor, shiftR, (.&.), (.|.), FiniteBits (..))-import Data.Text (Text)-import Data.Word (Word8, Word32)--import Control.Lens hiding (op, (:<), (|>))-import Control.Monad.State.Strict hiding (state)--import Data.ByteString              (ByteString)-import Data.ByteString.Lazy         (fromStrict)-import Data.Map.Strict              (Map)-import Data.Maybe                   (fromMaybe, isNothing)-import Data.Semigroup               (Semigroup (..))-import Data.Sequence                (Seq)-import Data.Vector.Storable         (Vector)-import Data.Foldable                (toList)--import Data.Tree--import qualified Data.ByteString      as BS-import qualified Data.ByteString.Char8 as Char8-import qualified Data.Map.Strict      as Map-import qualified Data.Sequence        as Seq-import qualified Data.Tree.Zipper     as Zipper-import qualified Data.Vector.Storable as Vector-import qualified Data.Vector.Storable.Mutable as Vector--import qualified Data.Vector as RegularVector---- * Data types--data Error-  = BalanceTooLow Word Word-  | UnrecognizedOpcode Word8-  | SelfDestruction-  | StackUnderrun-  | BadJumpDestination-  | Revert ByteString-  | NoSuchContract Addr-  | OutOfGas Word Word-  | BadCheatCode Word32-  | StackLimitExceeded-  | IllegalOverflow-  | Query Query-  | PrecompiledContractError Int-  | StateChangeWhileStatic--deriving instance Show Error---- | The possible result states of a VM-data VMResult-  = VMFailure Error -- ^ An operation failed-  | VMSuccess ByteString -- ^ Reached STOP, RETURN, or end-of-code--deriving instance Show VMResult---- | The state of a stepwise EVM execution-data VM = VM-  { _result        :: Maybe VMResult-  , _state         :: FrameState-  , _frames        :: [Frame]-  , _env           :: Env-  , _block         :: Block-  , _tx            :: TxState-  , _logs          :: Seq Log-  , _traces        :: Zipper.TreePos Zipper.Empty Trace-  , _cache         :: Cache-  , _execMode      :: ExecMode-  , _burned        :: Word-  }--data Trace = Trace-  { _traceCodehash :: W256-  , _traceOpIx     :: Int-  , _traceData     :: TraceData-  }--data TraceData-  = EventTrace Log-  | FrameTrace FrameContext-  | QueryTrace Query-  | ErrorTrace Error-  | EntryTrace Text-  | ReturnTrace ByteString FrameContext--data ExecMode = ExecuteNormally | ExecuteAsVMTest--data Query where-  PleaseFetchContract :: Addr         -> (Contract -> EVM ()) -> Query-  PleaseFetchSlot     :: Addr -> Word -> (Word     -> EVM ()) -> Query--instance Show Query where-  showsPrec _ = \case-    PleaseFetchContract addr _ ->-      (("<EVM.Query: fetch contract " ++ show addr ++ ">") ++)-    PleaseFetchSlot addr slot _ ->-      (("<EVM.Query: fetch slot "-        ++ show slot ++ " for "-        ++ show addr ++ ">") ++)---- | Alias for the type of e.g. @exec1@.-type EVM a = State VM a---- | The cache is data that can be persisted for efficiency:--- any expensive query that is constant at least within a block.-data Cache = Cache-  { _fetched :: Map Addr Contract-  }---- | A way to specify an initial VM state-data VMOpts = VMOpts-  { vmoptCode :: ByteString-  , vmoptCalldata :: ByteString-  , vmoptValue :: W256-  , vmoptAddress :: Addr-  , vmoptCaller :: Addr-  , vmoptOrigin :: Addr-  , vmoptGas :: W256-  , vmoptNumber :: W256-  , vmoptTimestamp :: W256-  , vmoptCoinbase :: Addr-  , vmoptDifficulty :: W256-  , vmoptGaslimit :: W256-  , vmoptGasprice :: W256-  , vmoptSchedule :: FeeSchedule Word-  } deriving Show---- | A log entry-data Log = Log Addr ByteString [Word]---- | An entry in the VM's "call/create stack"-data Frame = Frame-  { _frameContext   :: FrameContext-  , _frameState     :: FrameState-  }---- | Call/create info-data FrameContext-  = CreationContext-    { creationContextCodehash :: W256 }-  | CallContext-    { callContextOffset   :: Word-    , callContextSize     :: Word-    , callContextCodehash :: W256-    , callContextAbi      :: Maybe Word-    , callContextData     :: ByteString-    , callContextReversion :: Map Addr Contract-    }---- | The "registers" of the VM along with memory and data stack-data FrameState = FrameState-  { _contract     :: Addr-  , _codeContract :: Addr-  , _code         :: ByteString-  , _pc           :: Int-  , _stack        :: [Word]-  , _memory       :: ByteString-  , _memorySize   :: Int-  , _calldata     :: ByteString-  , _callvalue    :: Word-  , _caller       :: Addr-  , _gas          :: Word-  , _returndata   :: ByteString-  , _static       :: Bool-  }---- | The state that spans a whole transaction-data TxState = TxState-  { _selfdestructs :: [Addr]-  , _refunds       :: [(Addr, Word)]-  }---- | The state of a contract-data Contract = Contract-  { _bytecode :: ByteString-  , _storage  :: Map Word Word-  , _balance  :: Word-  , _nonce    :: Word-  , _codehash :: W256-  , _codesize :: Int -- (redundant?)-  , _opIxMap  :: Vector Int-  , _codeOps  :: RegularVector.Vector (Int, Op)-  , _external :: Bool-  }--deriving instance Show Contract-deriving instance Eq Contract---- | Various environmental data-data Env = Env-  { _contracts :: Map Addr Contract-  , _sha3Crack :: Map Word ByteString-  , _origin    :: Addr-  }----- | Data about the block-data Block = Block-  { _coinbase   :: Addr-  , _timestamp  :: Word-  , _number     :: Word-  , _difficulty :: Word-  , _gaslimit   :: Word-  , _gasprice   :: Word-  , _schedule   :: FeeSchedule Word-  }--blankState :: FrameState-blankState = FrameState-  { _contract     = 0-  , _codeContract = 0-  , _code         = mempty-  , _pc           = 0-  , _stack        = mempty-  , _memory       = mempty-  , _memorySize   = 0-  , _calldata     = mempty-  , _callvalue    = 0-  , _caller       = 0-  , _gas          = 0-  , _returndata   = mempty-  , _static       = False-  }--makeLenses ''FrameState-makeLenses ''Frame-makeLenses ''Block-makeLenses ''TxState-makeLenses ''Contract-makeLenses ''Env-makeLenses ''Cache-makeLenses ''Trace-makeLenses ''VM--instance Semigroup Cache where-  a <> b = Cache-    { _fetched = mappend (view fetched a) (view fetched b) }--instance Monoid Cache where-  mempty = Cache { _fetched = mempty }---- * Data accessors--currentContract :: VM -> Maybe Contract-currentContract vm =-  view (env . contracts . at (view (state . codeContract) vm)) vm---- * Data constructors--makeVm :: VMOpts -> VM-makeVm o = VM-  { _result = Nothing-  , _frames = mempty-  , _tx = TxState-    { _selfdestructs = mempty-    , _refunds = mempty-    }-  , _logs = mempty-  , _traces = Zipper.fromForest []-  , _block = Block-    { _coinbase = vmoptCoinbase o-    , _timestamp = w256 $ vmoptTimestamp o-    , _number = w256 $ vmoptNumber o-    , _difficulty = w256 $ vmoptDifficulty o-    , _gaslimit = w256 $ vmoptGaslimit o-    , _gasprice = w256 $ vmoptGasprice o-    , _schedule = vmoptSchedule o-    }-  , _state = FrameState-    { _pc = 0-    , _stack = mempty-    , _memory = mempty-    , _memorySize = 0-    , _code = vmoptCode o-    , _contract = vmoptAddress o-    , _codeContract = vmoptAddress o-    , _calldata = vmoptCalldata o-    , _callvalue = w256 $ vmoptValue o-    , _caller = vmoptCaller o-    , _gas = w256 $ vmoptGas o-    , _returndata = mempty-    , _static = False-    }-  , _env = Env-    { _sha3Crack = mempty-    , _origin = vmoptOrigin o-    , _contracts = Map.fromList-      [(vmoptAddress o, initialContract (vmoptCode o))]-    }-  , _cache = mempty-  , _execMode = ExecuteNormally-  , _burned = 0-  }--initialContract :: ByteString -> Contract-initialContract theCode = Contract-  { _bytecode = theCode-  , _codesize = BS.length theCode-  , _codehash =-    if BS.null theCode then 0 else-      keccak (stripBytecodeMetadata theCode)-  , _storage  = mempty-  , _balance  = 0-  , _nonce    = 0-  , _opIxMap  = mkOpIxMap theCode-  , _codeOps  = mkCodeOps theCode-  , _external = False-  }---- * Opcode dispatch (exec1)--next :: (?op :: Word8) => EVM ()-next = modifying (state . pc) (+ (opSize ?op))--exec1 :: EVM ()-exec1 = do-  vm <- get--  let-    -- Convenience function to access parts of the current VM state.-    -- Arcane type signature needed to avoid monomorphism restriction.-    the :: (b -> VM -> Const a VM) -> ((a -> Const a a) -> b) -> a-    the f g = view (f . g) vm--    -- Convenient aliases-    mem  = the state memory-    stk  = the state stack-    self = the state contract-    this = fromMaybe (error "internal error: state contract") (preview (ix (the state contract)) (the env contracts))--    fees@(FeeSchedule {..}) = the block schedule--    doStop = finishFrame (FrameReturned "")--  if the state pc >= num (BS.length (the state code))-    then-      doStop--    else do-      let ?op = BS.index (the state code) (the state pc)--      case ?op of--        -- op: PUSH-        x | x >= 0x60 && x <= 0x7f -> do-          let !n = num x - 0x60 + 1-              !xs = BS.take n (BS.drop (1 + the state pc)-                                       (the state code))-          limitStack 1 $-            burn g_verylow $ do-              next-              push (w256 (word xs))--        -- op: DUP-        x | x >= 0x80 && x <= 0x8f -> do-          let !i = x - 0x80 + 1-          case preview (ix (num i - 1)) stk of-            Nothing -> underrun-            Just y -> do-              limitStack 1 $-                burn g_verylow $ do-                  next-                  push y--        -- op: SWAP-        x | x >= 0x90 && x <= 0x9f -> do-          let i = num (x - 0x90 + 1)-          if length stk < i + 1-            then underrun-            else-              burn g_verylow $ do-                next-                zoom (state . stack) $ do-                  assign (ix 0) (stk ^?! ix i)-                  assign (ix i) (stk ^?! ix 0)--        -- op: LOG-        x | x >= 0xa0 && x <= 0xa4 ->-          notStatic $-          let n = (num x - 0xa0) in-          case stk of-            (xOffset:xSize:xs) ->-              if length xs < n-              then underrun-              else do-                let (topics, xs') = splitAt n xs-                    bytes         = readMemory (num xOffset) (num xSize) vm-                    log           = Log self bytes topics--                burn (g_log + g_logdata * xSize + num n * g_logtopic) $ do-                  accessMemoryRange fees xOffset xSize $ do-                    traceLog log-                    next-                    assign (state . stack) xs'-                    pushToSequence logs log-            _ ->-              underrun--        -- op: STOP-        0x00 -> doStop--        -- op: ADD-        0x01 -> stackOp2 (const g_verylow) (uncurry (+))-        -- op: MUL-        0x02 -> stackOp2 (const g_low) (uncurry (*))-        -- op: SUB-        0x03 -> stackOp2 (const g_verylow) (uncurry (-))--        -- op: DIV-        0x04 -> stackOp2 (const g_low) $-          \case (_, 0) -> 0-                (x, y) -> div x y--        -- op: SDIV-        0x05 ->-          stackOp2 (const g_low) (uncurry (sdiv))--        -- op: MOD-        0x06 -> stackOp2 (const g_low) $ \case-          (_, 0) -> 0-          (x, y) -> mod x y--        -- op: SMOD-        0x07 -> stackOp2 (const g_low) $ uncurry smod-        -- op: ADDMOD-        0x08 -> stackOp3 (const g_mid) $ (\(x, y, z) -> addmod x y z)-        -- op: MULMOD-        0x09 -> stackOp3 (const g_mid) $ (\(x, y, z) -> mulmod x y z)--        -- op: LT-        0x10 -> stackOp2 (const g_verylow) $ \(x, y) -> if x < y then 1 else 0-        -- op: GT-        0x11 -> stackOp2 (const g_verylow) $ \(x, y) -> if x > y then 1 else 0-        -- op: SLT-        0x12 -> stackOp2 (const g_verylow) $ uncurry slt-        -- op: SGT-        0x13 -> stackOp2 (const g_verylow) $ uncurry sgt--        -- op: EQ-        0x14 -> stackOp2 (const g_verylow) $ \(x, y) -> if x == y then 1 else 0-        -- op: ISZERO-        0x15 -> stackOp1 (const g_verylow) $ \case 0 -> 1; _ -> 0--        -- op: AND-        0x16 -> stackOp2 (const g_verylow) $ uncurry (.&.)-        -- op: OR-        0x17 -> stackOp2 (const g_verylow) $ uncurry (.|.)-        -- op: XOR-        0x18 -> stackOp2 (const g_verylow) $ uncurry xor-        -- op: NOT-        0x19 -> stackOp1 (const g_verylow) complement--        -- op: BYTE-        0x1a -> stackOp2 (const g_verylow) $ \case-          (n, _) | n >= 32 ->-            0-          (n, x) ->-            0xff .&. shiftR x (8 * (31 - num n))--        -- op: SHA3-        0x20 ->-          case stk of-            ((num -> xOffset) : (num -> xSize) : xs) -> do-              let bytes = readMemory xOffset xSize vm-                  hash  = keccakBlob bytes-              burn (g_sha3 + g_sha3word * ceilDiv (num xSize) 32) $-                accessMemoryRange fees xOffset xSize $ do-                  next-                  assign (state . stack) (hash : xs)-                  assign (env . sha3Crack . at hash) (Just bytes)-            _ -> underrun--        -- op: ADDRESS-        0x30 ->-          limitStack 1 $-            burn g_base (next >> push (num (the state contract)))--        -- op: BALANCE-        0x31 ->-          case stk of-            (x:xs) -> do-              burn g_balance $ do-                touchAccount (num x) $ \c -> do-                  next-                  assign (state . stack) xs-                  push (view balance c)-            [] ->-              underrun--        -- op: ORIGIN-        0x32 ->-          limitStack 1 . burn g_base $-            next >> push (num (the env origin))--        -- op: CALLER-        0x33 ->-          limitStack 1 . burn g_base $-            next >> push (num (the state caller))--        -- op: CALLVALUE-        0x34 ->-          limitStack 1 . burn g_base $-            next >> push (the state callvalue)--        -- op: CALLDATALOAD-        0x35 -> stackOp1 (const g_verylow) $-          \x -> readBlobWord x (the state calldata)--        -- op: CALLDATASIZE-        0x36 ->-          limitStack 1 . burn g_base $-            next >> push (blobSize (the state calldata))--        -- op: CALLDATACOPY-        0x37 ->-          case stk of-            ((num -> xTo) : (num -> xFrom) : (num -> xSize) :xs) -> do-              burn (g_verylow + g_copy * ceilDiv xSize 32) $ do-                accessMemoryRange fees xTo xSize $ do-                  next-                  assign (state . stack) xs-                  copyBytesToMemory (the state calldata) xSize xFrom xTo-            _ -> underrun--        -- op: CODESIZE-        0x38 ->-          limitStack 1 . burn g_base $-            next >> push (num (BS.length (the state code)))--        -- op: CODECOPY-        0x39 ->-          case stk of-            ((num -> memOffset) : (num -> codeOffset) : (num -> n) : xs) -> do-              burn (g_verylow + g_copy * ceilDiv (num n) 32) $ do-                accessMemoryRange fees memOffset n $ do-                  next-                  assign (state . stack) xs-                  copyBytesToMemory (view bytecode this)-                    n codeOffset memOffset-            _ -> underrun--        -- op: GASPRICE-        0x3a ->-          limitStack 1 . burn g_base $-            next >> push (the block gasprice)--        -- op: EXTCODESIZE-        0x3b ->-          case stk of-            (x:xs) -> do-              if x == num cheatCode-                then do-                  next-                  assign (state . stack) xs-                  push (w256 1)-                else-                  burn g_extcode $ do-                    touchAccount (num x) $ \c -> do-                      next-                      assign (state . stack) xs-                      push (num (view codesize c))-            [] ->-              underrun--        -- op: EXTCODECOPY-        0x3c ->-          case stk of-            ( extAccount-              : (num -> memOffset)-              : (num -> codeOffset)-              : (num -> codeSize)-              : xs ) -> do-              burn (g_extcode + g_copy * ceilDiv (num codeSize) 32) $-                accessMemoryRange fees memOffset codeSize $ do-                  touchAccount (num extAccount) $ \c -> do-                    next-                    assign (state . stack) xs-                    copyBytesToMemory (view bytecode c)-                      codeSize codeOffset memOffset-            _ -> underrun--        -- op: RETURNDATASIZE-        0x3d ->-          limitStack 1 . burn g_base $-            next >> push (blobSize (the state returndata))--        -- op: RETURNDATACOPY-        0x3e ->-          case stk of-            ((num -> xTo) : (num -> xFrom) : (num -> xSize) :xs) -> do-              burn (g_verylow + g_copy * ceilDiv xSize 32) $ do-                accessMemoryRange fees xTo xSize $ do-                  next-                  assign (state . stack) xs-                  copyBytesToMemory (the state returndata) xSize xFrom xTo-            _ -> underrun--        -- op: BLOCKHASH-        0x40 -> do-          -- We adopt the fake block hash scheme of the VMTests,-          -- so that blockhash(i) is the hash of i as decimal ASCII.-          stackOp1 (const g_blockhash) $-            \i ->-              if i + 256 < the block number || i >= the block number-              then 0-              else-                (num i :: Integer)-                  & show & Char8.pack & keccak & num--        -- op: COINBASE-        0x41 ->-          limitStack 1 . burn g_base $-            next >> push (num (the block coinbase))--        -- op: TIMESTAMP-        0x42 ->-          limitStack 1 . burn g_base $-            next >> push (the block timestamp)--        -- op: NUMBER-        0x43 ->-          limitStack 1 . burn g_base $-            next >> push (the block number)--        -- op: DIFFICULTY-        0x44 ->-          limitStack 1 . burn g_base $-            next >> push (the block difficulty)--        -- op: GASLIMIT-        0x45 ->-          limitStack 1 . burn g_base $-            next >> push (the block gaslimit)--        -- op: POP-        0x50 ->-          case stk of-            (_:xs) -> burn g_base (next >> assign (state . stack) xs)-            _      -> underrun--        -- op: MLOAD-        0x51 ->-          case stk of-            (x:xs) -> do-              burn g_verylow $-                accessMemoryWord fees x $ do-                  next-                  assign (state . stack) (view (word256At (num x)) mem : xs)-            _ -> underrun--        -- op: MSTORE-        0x52 ->-          case stk of-            (x:y:xs) -> do-              burn g_verylow $-                accessMemoryWord fees x $ do-                  next-                  assign (state . memory . word256At (num x)) y-                  assign (state . stack) xs-            _ -> underrun--        -- op: MSTORE8-        0x53 ->-          case stk of-            (x:y:xs) -> do-              burn g_verylow $-                accessMemoryRange fees x 1 $ do-                  next-                  modifying (state . memory) (setMemoryByte x (wordToByte y))-                  assign (state . stack) xs-            _ -> underrun--        -- op: SLOAD-        0x54 ->-          case stk of-            (x:xs) ->-              burn g_sload $-                accessStorage self x $ \y -> do-                  next-                  assign (state . stack) (y:xs)-            _ -> underrun--        -- op: SSTORE-        0x55 ->-          notStatic $-          case stk of-            (x:new:xs) -> do-              accessStorage self x $ \old -> do-                -- Gas cost is higher when changing from zero to nonzero.-                let cost = if old == 0 && new /= 0 then g_sset else g_sreset--                burn cost $ do-                  next-                  assign (state . stack) xs-                  assign (env . contracts . ix (the state contract) . storage . at x)-                    (Just new)--                  -- Give gas refund if clearing the storage slot.-                  if old /= 0 && new == 0 then refund r_sclear else noop--            _ -> underrun--        -- op: JUMP-        0x56 ->-          case stk of-            (x:xs) -> do-              burn g_mid $ do-                checkJump x xs-            _ -> underrun--        -- op: JUMPI-        0x57 -> do-          case stk of-            (x:y:xs) -> do-              burn g_high $ do-                if y == 0-                  then assign (state . stack) xs >> next-                  else checkJump x xs-            _ -> underrun--        -- op: PC-        0x58 ->-          limitStack 1 . burn g_base $-            next >> push (num (the state pc))--        -- op: MSIZE-        0x59 ->-          limitStack 1 . burn g_base $-            next >> push (num (the state memorySize))--        -- op: GAS-        0x5a ->-          limitStack 1 . burn g_base $-            next >> push (the state gas - g_base)--        -- op: JUMPDEST-        0x5b -> burn g_jumpdest next--        -- op: EXP-        0x0a ->-          let cost (_, exponent) =-                if exponent == 0-                then g_exp-                else g_exp + g_expbyte * num (ceilDiv (1 + log2 exponent) 8)-          in stackOp2 cost (uncurry exponentiate)--        -- op: SIGNEXTEND-        0x0b ->-          stackOp2 (const g_low) $ \(bytes, x) ->-            if bytes >= 32 then x-            else let n = num bytes * 8 + 7 in-              if testBit x n-              then x .|. complement (bit n - 1)-              else x .&. (bit n - 1)--        -- op: CREATE-        0xf0 ->-          notStatic $-          case stk of-            (xValue:xOffset:xSize:xs) ->-              burn g_create $ do-                accessMemoryRange fees xOffset xSize $ do-                  if xValue > view balance this-                    then do-                      assign (state . stack) (0 : xs)-                      next-                    else do-                      let-                        newAddr =-                          newContractAddress self (wordValue (view nonce this))-                      case view execMode vm of-                        ExecuteAsVMTest -> do-                          assign (state . stack) (num newAddr : xs)-                          next--                        ExecuteNormally -> do-                          let-                            newCode =-                              readMemory (num xOffset) (num xSize) vm-                            newContract =-                              initialContract newCode-                            newContext  =-                              CreationContext (view codehash newContract)--                          zoom (env . contracts) $ do-                            assign (at newAddr) (Just newContract)-                            assign (ix newAddr . balance) xValue-                            modifying (ix self . balance) (flip (-) xValue)-                            modifying (ix self . nonce) succ--                          pushTrace (FrameTrace newContext)-                          next-                          vm' <- get-                          pushTo frames $ Frame-                            { _frameContext = newContext-                            , _frameState   = (set stack xs) (view state vm')-                            }--                          assign state $-                            blankState-                              & set contract   newAddr-                              & set codeContract newAddr-                              & set code       newCode-                              & set callvalue  xValue-                              & set caller     self-                              & set gas        (view (state . gas) vm')--            _ -> underrun--        -- op: CALL-        0xf1 ->-          case stk of-            ( xGas-              : (num -> xTo)-              : xValue-              : xInOffset-              : xInSize-              : xOutOffset-              : xOutSize-              : xs-             ) ->-              case xTo of-                n | n > 0 && n <= 8 -> precompiledContract-                n | num n == cheatCode ->-                  do-                    assign (state . stack) xs-                    cheat (xInOffset, xInSize) (xOutOffset, xOutSize)-                _ ->-                  let-                    availableGas = the state gas-                    recipient    = view (env . contracts . at xTo) vm-                    (cost, gas') = costOfCall fees recipient xValue availableGas xGas-                  in burn (cost - gas') $-                    (if xValue > 0 then notStatic else id) $-                    if xValue > view balance this-                    then do-                      assign (state . stack) (0 : xs)-                      next-                    else-                      case view execMode vm of-                        ExecuteAsVMTest -> do-                          assign (state . stack) (1 : xs)-                          next-                        ExecuteNormally -> do-                          delegateCall fees gas' xTo xInOffset xInSize xOutOffset xOutSize xs $ do-                            zoom state $ do-                              assign callvalue xValue-                              assign caller (the state contract)-                              assign contract xTo-                              assign memorySize 0-                            zoom (env . contracts) $ do-                              ix self . balance -= xValue-                              ix xTo  . balance += xValue-            _ ->-              underrun--        -- op: CALLCODE-        0xf2 ->-          error "CALLCODE not supported (use DELEGATECALL)"--        -- op: RETURN-        0xf3 ->-          case stk of-            (xOffset:xSize:_) ->-              accessMemoryRange fees xOffset xSize $ do-                let output = readMemory (num xOffset) (num xSize) vm-                finishFrame (FrameReturned output)-            _ -> underrun--        -- op: DELEGATECALL-        0xf4 ->-          case stk of-            (xGas:xTo:xInOffset:xInSize:xOutOffset:xOutSize:xs) ->-              if num xTo == cheatCode-              then do-                assign (state . stack) xs-                cheat (xInOffset, xInSize) (xOutOffset, xOutSize)-              else-                burn (num g_call) $ do-                  delegateCall fees xGas (num xTo) xInOffset xInSize xOutOffset xOutSize xs-                    (return ())-            _ -> underrun--        -- op: STATICCALL-        0xfa ->-          case stk of-            (xGas : (num -> xTo) : xInOffset : xInSize : xOutOffset : xOutSize : xs) ->-              case xTo of-                n | n > 0 && n <= 8 -> precompiledContract-                _ ->-                  let-                    availableGas = the state gas-                    recipient    = view (env . contracts . at xTo) vm-                    (cost, gas') = costOfCall fees recipient 0 availableGas xGas-                  in burn (cost - gas') $-                    case view execMode vm of-                      ExecuteAsVMTest -> do-                        assign (state . stack) (1 : xs)-                        next-                      ExecuteNormally -> do-                        delegateCall fees gas' xTo xInOffset xInSize xOutOffset xOutSize xs $ do-                          zoom state $ do-                            assign callvalue 0-                            assign caller (the state contract)-                            assign contract xTo-                            assign memorySize 0-                            assign static True-            _ ->-              underrun--        -- op: SELFDESTRUCT-        0xff ->-          notStatic $-          case stk of-            [] -> underrun-            (x:_) -> do-              touchAccount (num x) $ \_ -> do-                pushTo (tx . selfdestructs) self-                assign (env . contracts . ix self . balance) 0-                modifying-                  (env . contracts . ix (num x) . balance)-                  (+ (vm ^?! env . contracts . ix self . balance))-                doStop--        -- op: REVERT-        0xfd ->-          case stk of-            (xOffset:xSize:_) ->-              accessMemoryRange fees xOffset xSize $ do-                let output = readMemory (num xOffset) (num xSize) vm-                finishFrame (FrameReverted output)-            _ -> underrun--        xxx ->-          vmError (UnrecognizedOpcode xxx)--precompiledContract :: (?op :: Word8) => EVM ()-precompiledContract = do-  vm <- get-  fees <- use (block . schedule)-  stk <- use (state . stack)--  case (?op, stk) of-    -- CALL (includes value)-    (0xf1, (_:(num -> op):_:inOffset:inSize:outOffset:outSize:xs)) ->-      doIt vm fees op inOffset inSize outOffset outSize xs-    -- STATICCALL (does not include value)-    (0xfa, (_:(num -> op):inOffset:inSize:outOffset:outSize:xs)) ->-      doIt vm fees op inOffset inSize outOffset outSize xs-    _ ->-      underrun--  where-    doIt vm fees op inOffset inSize outOffset outSize xs =-      let-        input = readMemory (num inOffset) (num inSize) vm-      in-        case EVM.Precompiled.execute op input (num outSize) of-          Nothing -> do-            assign (state . stack) (0 : xs)-            vmError (PrecompiledContractError op)-          Just output -> do-            let-              cost =-                case op of-                  1 -> 3000-                  _ -> error ("unimplemented precompiled contract " ++ show op)-            accessMemoryRange fees inOffset inSize $-              accessMemoryRange fees outOffset outSize $-                burn cost $ do-                  assign (state . stack) (1 : xs)-                  modifying (state . memory)-                    (writeMemory output outSize 0 outOffset)-                  next---- * Opcode helper actions--noop :: Monad m => m ()-noop = pure ()--pushTo :: MonadState s m => ASetter s s [a] [a] -> a -> m ()-pushTo f x = f %= (x :)--pushToSequence :: MonadState s m => ASetter s s (Seq a) (Seq a) -> a -> m ()-pushToSequence f x = f %= (Seq.|> x)--touchAccount :: Addr -> (Contract -> EVM ()) -> EVM ()-touchAccount addr continue = do-  use (env . contracts . at addr) >>= \case-    Just c -> continue c-    Nothing ->-      use (cache . fetched . at addr) >>= \case-        Just c -> do-          assign (env . contracts . at addr) (Just c)-          continue c-        Nothing ->-          assign result . Just . VMFailure . Query $-            PleaseFetchContract addr-              (\c -> do assign (cache . fetched . at addr) (Just c)-                        assign (env . contracts . at addr) (Just c)-                        assign result Nothing-                        continue c)--accessStorage-  :: Addr             -- ^ Contract address-  -> Word             -- ^ Storage slot key-  -> (Word -> EVM ()) -- ^ Continuation-  -> EVM ()-accessStorage addr slot continue =-  use (env . contracts . at addr) >>= \case-    Just c ->-      case view (storage . at slot) c of-        Just value ->-          continue value-        Nothing ->-          if view external c-          then-            assign result . Just . VMFailure . Query $-              PleaseFetchSlot addr slot-                (\x -> do-                    assign (cache . fetched . ix addr . storage . at slot) (Just x)-                    assign (env . contracts . ix addr . storage . at slot) (Just x)-                    assign result Nothing-                    continue x)-          else do-            assign (env . contracts . ix addr . storage . at slot) (Just 0)-            continue 0-    Nothing ->-      touchAccount addr $ \_ ->-        accessStorage addr slot continue---- | Replace a contract's code, like when CREATE returns--- from the constructor code.-replaceCode :: Addr -> ByteString -> EVM ()-replaceCode target newCode = do-  zoom (env . contracts . at target) $ do-    if BS.null newCode-      then put Nothing-      else do-        Just now <- get-        put . Just $-          initialContract newCode-            & set storage (view storage now)-            & set balance (view balance now)-            & set nonce   (view nonce now)--replaceCodeOfSelf :: ByteString -> EVM ()-replaceCodeOfSelf newCode = do-  vm <- get-  replaceCode (view (state . contract) vm) newCode--resetState :: EVM ()-resetState = do-  assign result     Nothing-  assign frames     []-  assign state      blankState--finalize :: EVM ()-finalize = do-  destroyedAddresses <- use (tx . selfdestructs)-  modifying (env . contracts)-    (Map.filterWithKey (\k _ -> not (elem k destroyedAddresses)))--loadContract :: Addr -> EVM ()-loadContract target =-  preuse (env . contracts . ix target . bytecode) >>=-    \case-      Nothing ->-        error "Call target doesn't exist"-      Just targetCode -> do-        assign (state . contract) target-        assign (state . code)     targetCode-        assign (state . codeContract) target--limitStack :: Int -> EVM () -> EVM ()-limitStack n continue = do-  stk <- use (state . stack)-  if length stk + n > 1024-    then vmError StackLimitExceeded-    else continue--notStatic :: EVM () -> EVM ()-notStatic continue = do-  bad <- use (state . static)-  if bad-    then vmError StateChangeWhileStatic-    else continue--burn :: Word -> EVM () -> EVM ()-burn n continue = do-  available <- use (state . gas)-  if n <= available-    then do-      state . gas -= n-      burned += n-      continue-    else-      vmError (OutOfGas available n)--refund :: Word -> EVM ()-refund n = do-  self <- use (state . contract)-  pushTo (tx . refunds) (self, n)----- * Cheat codes---- The cheat code is 7109709ecfa91a80626ff3989d68f67f5b1dd12d.--- Call this address using one of the cheatActions below to do--- special things, e.g. changing the block timestamp. Beware that--- these are necessarily hevm specific.-cheatCode :: Addr-cheatCode = num (keccak "hevm cheat code")--cheat-  :: (?op :: Word8)-  => (Word, Word) -> (Word, Word)-  -> EVM ()-cheat (inOffset, inSize) (outOffset, outSize) = do-  mem <- use (state . memory)-  let-    abi =-      num (wordValue (readMemoryWord32 inOffset mem))-    input =-      sliceMemory (inOffset + 4) (inSize - 4) mem-  case Map.lookup abi cheatActions of-    Nothing ->-      vmError (BadCheatCode abi)-    Just (argTypes, action) -> do-      case runGetOrFail-             (getAbiSeq (length argTypes) argTypes)-             (fromStrict input) of-        Right ("", _, args) -> do-          action (toList args) >>= \case-            Nothing -> do-              next-              push 1-            Just (encodeAbiValue -> bs) -> do-              next-              modifying (state . memory)-                (writeMemory bs outSize 0 outOffset)-              push 1-        Left _ ->-          vmError (BadCheatCode abi)-        Right _ ->-          vmError (BadCheatCode abi)--type CheatAction = ([AbiType], [AbiValue] -> EVM (Maybe AbiValue))--cheatActions :: Map Word32 CheatAction-cheatActions =-  Map.fromList-    [ action "warp(uint256)" [AbiUIntType 256] $-        \[AbiUInt 256 x] -> do-          assign (block . timestamp) (w256 (W256 x))-          return Nothing-    ]-  where-    action s ts f = (abiKeccak s, (ts, f))----- * General call implementation ("delegateCall")--delegateCall-  :: (?op :: Word8)-  => FeeSchedule Word-  -> Word -> Addr -> Word -> Word -> Word -> Word -> [Word]-  -> EVM ()-  -> EVM ()-delegateCall fees xGas xTo xInOffset xInSize xOutOffset xOutSize xs continue =-  touchAccount xTo . const $-    preuse (env . contracts . ix xTo) >>=-      \case-        Nothing -> vmError (NoSuchContract xTo)-        Just target ->-          accessMemoryRange fees xInOffset xInSize $ do-            accessMemoryRange fees xOutOffset xOutSize $ do-              burn xGas $ do-                vm0 <- get--                let newContext = CallContext-                      { callContextOffset = xOutOffset-                      , callContextSize = xOutSize-                      , callContextCodehash = view codehash target-                      , callContextReversion = view (env . contracts) vm0-                      , callContextAbi =-                          if xInSize >= 4-                          then-                            let-                              w = wordValue-                                    (readMemoryWord32 xInOffset (view (state . memory) vm0))-                            in Just $! num w-                          else Nothing-                      , callContextData = (readMemory (num xInOffset) (num xInSize) vm0)-                      }--                pushTrace (FrameTrace newContext)-                next-                vm1 <- get--                pushTo frames $ Frame-                  { _frameState = (set stack xs) (view state vm1)-                  , _frameContext = newContext-                  }--                zoom state $ do-                  assign gas xGas-                  assign pc 0-                  assign code (view bytecode target)-                  assign codeContract xTo-                  assign stack mempty-                  assign memory mempty-                  assign calldata (readMemory (num xInOffset) (num xInSize) vm0)--                continue----- * VM error implementation--underrun :: EVM ()-underrun = vmError StackUnderrun---- | A stack frame can be popped in three ways.-data FrameResult-  = FrameReturned ByteString -- ^ STOP, RETURN, or no more code-  | FrameReverted ByteString -- ^ REVERT-  | FrameErrored Error -- ^ Any other error-  deriving Show---- | This function defines how to pop the current stack frame in either of--- the ways specified by 'FrameResult'.------ It also handles the case when the current stack frame is the only one;--- in this case, we set the final '_result' of the VM execution.-finishFrame :: FrameResult -> EVM ()-finishFrame how = do-  oldVm <- get--  case view frames oldVm of-    -- Is the current frame the only one?-    [] ->-      assign result . Just $-        case how of-          FrameReturned output -> VMSuccess output-          FrameReverted output -> VMFailure (Revert output)-          FrameErrored e       -> VMFailure e--    -- Are there some remaining frames?-    nextFrame : remainingFrames -> do--      -- Pop the top frame.-      assign frames remainingFrames-      -- Install the state of the frame to which we shall return.-      assign state (view frameState nextFrame)-      -- Insert a debug trace.-      insertTrace $-        case how of-          FrameErrored e ->-            ErrorTrace e-          FrameReverted output ->-            ErrorTrace (Revert output)-          FrameReturned output ->-            ReturnTrace output (view frameContext nextFrame)-      -- Pop to the previous level of the debug trace stack.-      popTrace--      let remainingGas = view (state . gas) oldVm--      -- Now dispatch on whether we were creating or calling,-      -- and whether we shall return, revert, or error (six cases).-      case view frameContext nextFrame of--        -- Were we calling?-        CallContext (num -> outOffset) (num -> outSize) _ _ _ reversion -> do--          let-            -- When entering a call, the gas allowance is counted as burned-            -- in advance; this unburns the remainder and adds it to the-            -- parent frame.-            reclaimRemainingGasAllowance = do-              modifying burned (subtract remainingGas)-              modifying (state . gas) (+ remainingGas)--            revertContracts = assign (env . contracts) reversion--          case how of-            -- Case 1: Returning from a call?-            FrameReturned output -> do-              assign (state . returndata) output-              copyBytesToMemory output outSize 0 outOffset-              reclaimRemainingGasAllowance-              push 1--            -- Case 2: Reverting during a call?-            FrameReverted output -> do-              revertContracts-              assign (state . returndata) output-              reclaimRemainingGasAllowance-              push 0--            -- Case 3: Error during a call?-            FrameErrored _ -> do-              revertContracts-              push 0--        -- Or were we creating?-        CreationContext _ -> do-          let-            createe = view (state . contract) oldVm-            destroy = assign (env . contracts . at createe) Nothing--          case how of-            -- Case 4: Returning during a creation?-            FrameReturned output -> do-              replaceCode createe output-              assign (state . gas) remainingGas-              push (num createe)--            -- Case 5: Reverting during a creation?-            FrameReverted output -> do-              destroy-              assign (state . returndata) output-              assign (state . gas) remainingGas-              push 0--            -- Case 6: Error during a creation?-            FrameErrored _ -> do-              destroy-              assign (state . gas) 0-              push 0---vmError :: Error -> EVM ()-vmError e = finishFrame (FrameErrored e)---- * Memory helpers--accessMemoryRange-  :: FeeSchedule Word-  -> Word-  -> Word-  -> EVM ()-  -> EVM ()-accessMemoryRange _ _ 0 continue = continue-accessMemoryRange fees f l continue = do-  m0 <- num <$> use (state . memorySize)-  if f + l < l-    then vmError IllegalOverflow-    else do-      let m1 = 32 * ceilDiv (max m0 (f + l)) 32-      burn (memoryCost fees m1 - memoryCost fees m0) $ do-        assign (state . memorySize) (num m1)-        continue--accessMemoryWord-  :: FeeSchedule Word -> Word -> EVM () -> EVM ()-accessMemoryWord fees x continue = accessMemoryRange fees x 32 continue--copyBytesToMemory-  :: ByteString -> Word -> Word -> Word -> EVM ()-copyBytesToMemory bs size xOffset yOffset =-  if size == 0 then noop-  else do-    mem <- use (state . memory)-    assign (state . memory) $-      writeMemory bs size xOffset yOffset mem--readMemory :: Word -> Word -> VM -> ByteString-readMemory offset size vm = sliceMemory offset size (view (state . memory) vm)--word256At-  :: Functor f-  => Word -> (Word -> f Word)-  -> ByteString -> f ByteString-word256At i = lens getter setter where-  getter m = readMemoryWord i m-  setter m x = setMemoryWord i x m---- * Tracing--withTraceLocation-  :: (MonadState VM m) => TraceData -> m Trace-withTraceLocation x = do-  vm <- get-  let-    Just this =-      preview (env . contracts . ix (view (state . codeContract) vm)) vm-  pure Trace-    { _traceData = x-    , _traceCodehash = view codehash this-    , _traceOpIx = (view opIxMap this) Vector.! (view (state . pc) vm)-    }--pushTrace :: TraceData -> EVM ()-pushTrace x = do-  trace <- withTraceLocation x-  modifying traces $-    \t -> Zipper.children $ Zipper.insert (Node trace []) t--insertTrace :: TraceData -> EVM ()-insertTrace x = do-  trace <- withTraceLocation x-  modifying traces $-    \t -> Zipper.nextSpace $ Zipper.insert (Node trace []) t--popTrace :: EVM ()-popTrace =-  modifying traces $-    \t -> case Zipper.parent t of-            Nothing -> error "internal error (trace root)"-            Just t' -> Zipper.nextSpace t'--zipperRootForest :: Zipper.TreePos Zipper.Empty a -> Forest a-zipperRootForest z =-  case Zipper.parent z of-    Nothing -> Zipper.toForest z-    Just z' -> zipperRootForest (Zipper.nextSpace z')--traceForest :: VM -> Forest Trace-traceForest vm =-  view (traces . to zipperRootForest) vm--traceLog :: (MonadState VM m) => Log -> m ()-traceLog log = do-  trace <- withTraceLocation (EventTrace log)-  modifying traces $-    \t -> Zipper.nextSpace (Zipper.insert (Node trace []) t)---- * Stack manipulation--push :: Word -> EVM ()-push x = state . stack %= (x :)--stackOp1-  :: (?op :: Word8)-  => (Word -> Word)-  -> (Word -> Word)-  -> EVM ()-stackOp1 cost f =-  use (state . stack) >>= \case-    (x:xs) ->-      burn (cost x) $ do-        next-        let !y = f x-        state . stack .= y : xs-    _ ->-      underrun--stackOp2-  :: (?op :: Word8)-  => ((Word, Word) -> Word)-  -> ((Word, Word) -> Word)-  -> EVM ()-stackOp2 cost f =-  use (state . stack) >>= \case-    (x:y:xs) ->-      burn (cost (x, y)) $ do-        next-        state . stack .= f (x, y) : xs-    _ ->-      underrun--stackOp3-  :: (?op :: Word8)-  => ((Word, Word, Word) -> Word)-  -> ((Word, Word, Word) -> Word)-  -> EVM ()-stackOp3 cost f =-  use (state . stack) >>= \case-    (x:y:z:xs) ->-      burn (cost (x, y, z)) $ do-        next-        state . stack .= f (x, y, z) : xs-    _ ->-      underrun---- * Bytecode data functions--checkJump :: (Integral n) => n -> [Word] -> EVM ()-checkJump x xs = do-  theCode <- use (state . code)-  if x < num (BS.length theCode) && BS.index theCode (num x) == 0x5b-    then-      insidePushData (num x) >>=-        \case-          True ->-            vmError BadJumpDestination-          _ -> do-            state . stack .= xs-            state . pc .= num x-    else vmError BadJumpDestination--insidePushData :: Int -> EVM Bool-insidePushData i =-  -- If the operation index for the code pointer is the same-  -- as for the previous code pointer, then it's inside push data.-  if i == 0-    then pure False-    else do-      self <- use (state . codeContract)-      Just x <- preuse (env . contracts . ix self . opIxMap)-      pure ((x Vector.! i) == (x Vector.! (i - 1)))--opSize :: Word8 -> Int-opSize x | x >= 0x60 && x <= 0x7f = num x - 0x60 + 2-opSize _                          = 1---- Index i of the resulting vector contains the operation index for--- the program counter value i.  This is needed because source map--- entries are per operation, not per byte.-mkOpIxMap :: ByteString -> Vector Int-mkOpIxMap xs = Vector.create $ Vector.new (BS.length xs) >>= \v ->-  -- Loop over the byte string accumulating a vector-mutating action.-  -- This is somewhat obfuscated, but should be fast.-  let (_, _, _, m) =-        BS.foldl' (go v) (0 :: Word8, 0, 0, return ()) xs-  in m >> return v-  where-    go v (0, !i, !j, !m) x | x >= 0x60 && x <= 0x7f =-      {- Start of PUSH op. -} (x - 0x60 + 1, i + 1, j,     m >> Vector.write v i j)-    go v (1, !i, !j, !m) _ =-      {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> Vector.write v i j)-    go v (0, !i, !j, !m) _ =-      {- Other op. -}         (0,            i + 1, j + 1, m >> Vector.write v i j)-    go v (n, !i, !j, !m) _ =-      {- PUSH data. -}        (n - 1,        i + 1, j,     m >> Vector.write v i j)--vmOp :: VM -> Maybe Op-vmOp vm =-  let i  = vm ^. state . pc-      xs = BS.drop i (vm ^. state . code)-      op = BS.index xs 0-  in if BS.null xs-     then Nothing-     else Just (readOp op (BS.drop 1 xs))--vmOpIx :: VM -> Maybe Int-vmOpIx vm =-  do self <- currentContract vm-     (view opIxMap self) Vector.!? (view (state . pc) vm)--opParams :: VM -> Map String Word-opParams vm =-  case vmOp vm of-    Just OpCreate ->-      params $ words "value offset size"-    Just OpCall ->-      params $ words "gas to value in-offset in-size out-offset out-size"-    Just OpSstore ->-      params $ words "index value"-    Just OpCodecopy ->-      params $ words "mem-offset code-offset code-size"-    Just OpSha3 ->-      params $ words "offset size"-    Just OpCalldatacopy ->-      params $ words "to from size"-    Just OpExtcodecopy ->-      params $ words "account mem-offset code-offset code-size"-    Just OpReturn ->-      params $ words "offset size"-    Just OpJumpi ->-      params $ words "destination condition"-    _ -> mempty-  where-    params xs =-      if length (vm ^. state . stack) >= length xs-      then Map.fromList (zip xs (vm ^. state . stack))-      else mempty--readOp :: Word8 -> ByteString -> Op-readOp x _  | x >= 0x80 && x <= 0x8f = OpDup (x - 0x80 + 1)-readOp x _  | x >= 0x90 && x <= 0x9f = OpSwap (x - 0x90 + 1)-readOp x _  | x >= 0xa0 && x <= 0xa4 = OpLog (x - 0xa0)-readOp x xs | x >= 0x60 && x <= 0x7f =-  let n   = x - 0x60 + 1-      xs' = BS.take (num n) xs-  in OpPush (word xs')-readOp x _ = case x of-  0x00 -> OpStop-  0x01 -> OpAdd-  0x02 -> OpMul-  0x03 -> OpSub-  0x04 -> OpDiv-  0x05 -> OpSdiv-  0x06 -> OpMod-  0x07 -> OpSmod-  0x08 -> OpAddmod-  0x09 -> OpMulmod-  0x0a -> OpExp-  0x0b -> OpSignextend-  0x10 -> OpLt-  0x11 -> OpGt-  0x12 -> OpSlt-  0x13 -> OpSgt-  0x14 -> OpEq-  0x15 -> OpIszero-  0x16 -> OpAnd-  0x17 -> OpOr-  0x18 -> OpXor-  0x19 -> OpNot-  0x1a -> OpByte-  0x20 -> OpSha3-  0x30 -> OpAddress-  0x31 -> OpBalance-  0x32 -> OpOrigin-  0x33 -> OpCaller-  0x34 -> OpCallvalue-  0x35 -> OpCalldataload-  0x36 -> OpCalldatasize-  0x37 -> OpCalldatacopy-  0x38 -> OpCodesize-  0x39 -> OpCodecopy-  0x3a -> OpGasprice-  0x3b -> OpExtcodesize-  0x3c -> OpExtcodecopy-  0x3d -> OpReturndatasize-  0x3e -> OpReturndatacopy-  0x40 -> OpBlockhash-  0x41 -> OpCoinbase-  0x42 -> OpTimestamp-  0x43 -> OpNumber-  0x44 -> OpDifficulty-  0x45 -> OpGaslimit-  0x50 -> OpPop-  0x51 -> OpMload-  0x52 -> OpMstore-  0x53 -> OpMstore8-  0x54 -> OpSload-  0x55 -> OpSstore-  0x56 -> OpJump-  0x57 -> OpJumpi-  0x58 -> OpPc-  0x59 -> OpMsize-  0x5a -> OpGas-  0x5b -> OpJumpdest-  0xf0 -> OpCreate-  0xf1 -> OpCall-  0xf2 -> OpCallcode-  0xf3 -> OpReturn-  0xf4 -> OpDelegatecall-  0xfd -> OpRevert-  0xfa -> OpStaticcall-  0xff -> OpSelfdestruct-  _    -> (OpUnknown x)--mkCodeOps :: ByteString -> RegularVector.Vector (Int, Op)-mkCodeOps bytes = RegularVector.fromList . toList $ go 0 bytes-  where-    go !i !xs =-      case BS.uncons xs of-        Nothing ->-          mempty-        Just (x, xs') ->-          let j = opSize x-          in (i, readOp x xs') Seq.<| go (i + j) (BS.drop j xs)---- * Gas cost calculation helpers---- Gas cost function for CALL, transliterated from the Yellow Paper.-costOfCall-  :: FeeSchedule Word-  -> Maybe a -> Word -> Word -> Word-  -> (Word, Word)-costOfCall (FeeSchedule {..}) recipient xValue availableGas xGas =-  (c_gascap + c_extra, c_callgas)-  where-    c_extra =-      num g_call + c_xfer + c_new-    c_xfer =-      if xValue /= 0          then num g_callvalue              else 0-    c_new =-      if isNothing recipient  then num g_newaccount             else 0-    c_callgas =-      if xValue /= 0          then c_gascap + num g_callstipend else c_gascap-    c_gascap =-      if availableGas >= c_extra-      then min xGas (allButOne64th (availableGas - c_extra))-      else xGas--memoryCost :: FeeSchedule Word -> Word -> Word-memoryCost FeeSchedule{..} byteCount =-  let-    wordCount = ceilDiv byteCount 32-    linearCost = g_memory * wordCount-    quadraticCost = div (wordCount * wordCount) 512-  in-    if byteCount > exponentiate 2 32-    then maxBound-    else linearCost + quadraticCost+{-# Language DataKinds #-}+{-# Language GADTs #-}+{-# Language RecordWildCards #-}+{-# Language ScopedTypeVariables #-}+{-# Language StandaloneDeriving #-}+{-# Language StrictData #-}+{-# Language TemplateHaskell #-}+{-# Language TypeOperators #-}+{-# Language ViewPatterns #-}++module EVM where++import Prelude hiding (log, Word, exponent)++import Data.SBV hiding (Word, output, Unknown)+import Data.Proxy (Proxy(..))+import EVM.ABI+import EVM.Types+import EVM.Solidity+import EVM.Keccak+import EVM.Concrete (Word(..), w256, createAddress, wordValue, keccakBlob, create2Address)+import EVM.Symbolic+import EVM.Op+import EVM.FeeSchedule (FeeSchedule (..))+import Options.Generic as Options+import qualified EVM.Precompiled++import Data.Binary.Get (runGetOrFail)+import Data.Text (Text)+import Data.Word (Word8, Word32)+import Control.Lens hiding (op, (:<), (|>), (.>))+import Control.Monad.State.Strict hiding (state)++import Data.ByteString              (ByteString)+import Data.ByteString.Lazy         (fromStrict)+import Data.Map.Strict              (Map)+import Data.Maybe                   (fromMaybe)+import Data.Semigroup               (Semigroup (..))+import Data.Sequence                (Seq)+import Data.Vector.Storable         (Vector)+import Data.Foldable                (toList)++import Data.Tree++import qualified Data.ByteString      as BS+import qualified Data.ByteString.Lazy as LS+import qualified Data.ByteString.Char8 as Char8+import qualified Data.ByteArray       as BA+import qualified Data.Map.Strict      as Map+import qualified Data.Sequence        as Seq+import qualified Data.Tree.Zipper     as Zipper+import qualified Data.Vector.Storable as Vector+import qualified Data.Vector.Storable.Mutable as Vector++import qualified Data.Vector as RegularVector++import Crypto.Number.ModArithmetic (expFast)+import Crypto.Hash (Digest, SHA256, RIPEMD160)+import qualified Crypto.Hash as Crypto++-- * Data types++-- | EVM failure modes+data Error+  = BalanceTooLow Word Word+  | UnrecognizedOpcode Word8+  | SelfDestruction+  | StackUnderrun+  | BadJumpDestination+  | Revert ByteString+  | NoSuchContract Addr+  | OutOfGas Word Word+  | BadCheatCode (Maybe Word32)+  | StackLimitExceeded+  | IllegalOverflow+  | Query Query+  | Choose Choose+  | StateChangeWhileStatic+  | InvalidMemoryAccess+  | CallDepthLimitReached+  | MaxCodeSizeExceeded Word Word+  | PrecompileFailure+  | UnexpectedSymbolicArg+  | DeadPath+deriving instance Show Error++-- | The possible result states of a VM+data VMResult+  = VMFailure Error -- ^ An operation failed+  | VMSuccess Buffer -- ^ Reached STOP, RETURN, or end-of-code++deriving instance Show VMResult++-- | The state of a stepwise EVM execution+data VM = VM+  { _result         :: Maybe VMResult+  , _state          :: FrameState+  , _frames         :: [Frame]+  , _env            :: Env+  , _block          :: Block+  , _tx             :: TxState+  , _logs           :: Seq Log+  , _traces         :: Zipper.TreePos Zipper.Empty Trace+  , _cache          :: Cache+  , _burned         :: Word+  , _pathConditions :: [SBool]+  , _iterations     :: Map CodeLocation Int+  }++data Trace = Trace+  { _traceCodehash :: W256+  , _traceOpIx     :: Int+  , _traceData     :: TraceData+  }++data TraceData+  = EventTrace Log+  | FrameTrace FrameContext+  | QueryTrace Query+  | ErrorTrace Error+  | EntryTrace Text+  | ReturnTrace Buffer FrameContext++-- | Queries halt execution until resolved through RPC calls or SMT queries+data Query where+  PleaseFetchContract :: Addr         -> (Contract   -> EVM ()) -> Query+  PleaseFetchSlot     :: Addr -> Word -> (Word       -> EVM ()) -> Query+  PleaseAskSMT        :: SymWord -> [SBool] -> (JumpCondition -> EVM ()) -> Query++data Choose where+  PleaseChoosePath    :: (Bool -> EVM ()) -> Choose++instance Show Query where+  showsPrec _ = \case+    PleaseFetchContract addr _ ->+      (("<EVM.Query: fetch contract " ++ show addr ++ ">") ++)+    PleaseFetchSlot addr slot _ ->+      (("<EVM.Query: fetch slot "+        ++ show slot ++ " for "+        ++ show addr ++ ">") ++)+    PleaseAskSMT condition pathConditions _ ->+      (("<EVM.Query: ask SMT about "+        ++ show condition ++ " in context "+        ++ show pathConditions ++ ">") ++)++instance Show Choose where+  showsPrec _ = \case+    PleaseChoosePath _ ->+      (("<EVM.Choice: waiting for user to select path (0,1)") ++)++-- | Alias for the type of e.g. @exec1@.+type EVM a = State VM a++type CodeLocation = (Addr, Int)++-- | The possible return values of a SMT query regarding JUMPI+data JumpCondition = Iszero Bool | Unknown | Inconsistent+  deriving (Show)++-- | The cache is data that can be persisted for efficiency:+-- any expensive query that is constant at least within a block.+data Cache = Cache+  { _fetched :: Map Addr Contract,+    _path :: Map (CodeLocation, Int) Bool+  } deriving Show++-- | A way to specify an initial VM state+data VMOpts = VMOpts+  { vmoptContract :: Contract+  , vmoptCalldata :: (Buffer, (SWord 32)) -- maximum size of uint32 as per eip 1985+  , vmoptValue :: SymWord+  , vmoptAddress :: Addr+  , vmoptCaller :: SAddr+  , vmoptOrigin :: Addr+  , vmoptGas :: W256+  , vmoptGaslimit :: W256+  , vmoptNumber :: W256+  , vmoptTimestamp :: W256+  , vmoptCoinbase :: Addr+  , vmoptDifficulty :: W256+  , vmoptMaxCodeSize :: W256+  , vmoptBlockGaslimit :: W256+  , vmoptGasprice :: W256+  , vmoptSchedule :: FeeSchedule Word+  , vmoptChainId :: W256+  , vmoptCreate :: Bool+  , vmoptStorageModel :: StorageModel+  } deriving Show++-- | A log entry+data Log = Log Addr Buffer [SymWord]++-- | An entry in the VM's "call/create stack"+data Frame = Frame+  { _frameContext   :: FrameContext+  , _frameState     :: FrameState+  }++-- | Call/create info+data FrameContext+  = CreationContext+    { creationContextCodehash  :: W256+    , creationContextReversion :: Map Addr Contract+    , creationContextSubstate  :: SubState+    }+  | CallContext+    { callContextOffset    :: Word+    , callContextSize      :: Word+    , callContextCodehash  :: W256+    , callContextAbi       :: Maybe Word+    , callContextData      :: Buffer+    , callContextReversion :: Map Addr Contract+    , callContextSubState  :: SubState+    }++-- | The "registers" of the VM along with memory and data stack+data FrameState = FrameState+  { _contract     :: Addr+  , _codeContract :: Addr+  , _code         :: ByteString+  , _pc           :: Int+  , _stack        :: [SymWord]+  , _memory       :: Buffer+  , _memorySize   :: Int+  , _calldata     :: (Buffer, (SWord 32))+  , _callvalue    :: SymWord+  , _caller       :: SAddr+  , _gas          :: Word+  , _returndata   :: Buffer+  , _static       :: Bool+  }++-- | The state that spans a whole transaction+data TxState = TxState+  { _gasprice        :: Word+  , _txgaslimit      :: Word+  , _origin          :: Addr+  , _toAddr          :: Addr+  , _value           :: SymWord+  , _substate        :: SubState+  , _isCreate        :: Bool+  , _txReversion     :: Map Addr Contract+  }++-- | The "accrued substate" across a transaction+data SubState = SubState+  { _selfdestructs   :: [Addr]+  , _touchedAccounts :: [Addr]+  , _refunds         :: [(Addr, Word)]+  -- in principle we should include logs here, but do not for now+  }++-- | A contract is either in creation (running its "constructor") or+-- post-creation, and code in these two modes is treated differently+-- by instructions like @EXTCODEHASH@, so we distinguish these two+-- code types.+data ContractCode+  = InitCode ByteString     -- ^ "Constructor" code, during contract creation+  | RuntimeCode ByteString  -- ^ "Instance" code, after contract creation+  deriving (Show, Eq)++-- | A contract can either have concrete or symbolic storage+-- depending on what type of execution we are doing+data Storage+  = Concrete (Map Word SymWord)+  | Symbolic (SArray (WordN 256) (WordN 256))+  deriving (Show)++-- to allow for Eq Contract (which useful for debugging vmtests)+-- we mock an instance of Eq for symbolic storage.+-- It should not (cannot) be used though.+instance Eq Storage where+  (==) (Concrete a) (Concrete b) = fmap forceLit a == fmap forceLit b+  (==) (Symbolic _) (Concrete _) = False+  (==) (Concrete _) (Symbolic _) = False+  (==) _ _ = error "do not compare two symbolic arrays like this!"++-- | The state of a contract+data Contract = Contract+  { _contractcode :: ContractCode+  , _storage      :: Storage+  , _balance      :: Word+  , _nonce        :: Word+  , _codehash     :: W256+  , _opIxMap      :: Vector Int+  , _codeOps      :: RegularVector.Vector (Int, Op)+  , _external     :: Bool+  , _origStorage  :: Map Word Word+  }++deriving instance Show Contract+deriving instance Eq Contract++-- | When doing symbolic execution, we have three different+-- ways to model the storage of contracts. This determines+-- not only the initial contract storage model but also how+-- RPC or state fetched contracts will be modeled.+data StorageModel+  = ConcreteS    -- ^ Uses `Concrete` Storage. Reading / Writing from abstract+                 -- locations causes a runtime failure. Can be nicely combined with RPC.++  | SymbolicS    -- ^ Uses `Symbolic` Storage. Reading / Writing never reaches RPC,+                 -- but always done using an SMT array with no default value.++  | InitialS     -- ^ Uses `Symbolic` Storage. Reading / Writing never reaches RPC,+                 -- but always done using an SMT array with 0 as the default value.++  deriving (Read, Show)++instance ParseField StorageModel++-- | Various environmental data+data Env = Env+  { _contracts    :: Map Addr Contract+  , _chainId      :: Word+  , _storageModel :: StorageModel+  , _sha3Crack    :: Map Word ByteString+  , _keccakUsed   :: [([SWord 8], SWord 256)]+  }+++-- | Data about the block+data Block = Block+  { _coinbase    :: Addr+  , _timestamp   :: Word+  , _number      :: Word+  , _difficulty  :: Word+  , _gaslimit    :: Word+  , _maxCodeSize :: Word+  , _schedule    :: FeeSchedule Word+  }++blankState :: FrameState+blankState = FrameState+  { _contract     = 0+  , _codeContract = 0+  , _code         = mempty+  , _pc           = 0+  , _stack        = mempty+  , _memory       = mempty+  , _memorySize   = 0+  , _calldata     = (mempty, 0)+  , _callvalue    = 0+  , _caller       = 0+  , _gas          = 0+  , _returndata   = mempty+  , _static       = False+  }++makeLenses ''FrameState+makeLenses ''Frame+makeLenses ''Block+makeLenses ''TxState+makeLenses ''SubState+makeLenses ''Contract+makeLenses ''Env+makeLenses ''Cache+makeLenses ''Trace+makeLenses ''VM++-- | An "external" view of a contract's bytecode, appropriate for+-- e.g. @EXTCODEHASH@.+bytecode :: Getter Contract ByteString+bytecode = contractcode . to f+  where f (InitCode _)    = BS.empty+        f (RuntimeCode b) = b++instance Semigroup Cache where+  a <> b = Cache+    { _fetched = mappend (view fetched a) (view fetched b),+      _path = mappend (view path a) (view path b)+    }++instance Monoid Cache where+  mempty = Cache { _fetched = mempty,+                   _path = mempty+                 }++-- * Data accessors++currentContract :: VM -> Maybe Contract+currentContract vm =+  view (env . contracts . at (view (state . codeContract) vm)) vm++-- * Data constructors++makeVm :: VMOpts -> VM+makeVm o = VM+  { _result = Nothing+  , _frames = mempty+  , _tx = TxState+    { _gasprice = w256 $ vmoptGasprice o+    , _txgaslimit = w256 $ vmoptGaslimit o+    , _origin = vmoptOrigin o+    , _toAddr = vmoptAddress o+    , _value = vmoptValue o+    , _substate = SubState mempty mempty mempty+    , _isCreate = vmoptCreate o+    , _txReversion = Map.fromList+      [(vmoptAddress o, vmoptContract o)]+    }+  , _logs = mempty+  , _traces = Zipper.fromForest []+  , _block = Block+    { _coinbase = vmoptCoinbase o+    , _timestamp = w256 $ vmoptTimestamp o+    , _number = w256 $ vmoptNumber o+    , _difficulty = w256 $ vmoptDifficulty o+    , _maxCodeSize = w256 $ vmoptMaxCodeSize o+    , _gaslimit = w256 $ vmoptBlockGaslimit o+    , _schedule = vmoptSchedule o+    }+  , _state = FrameState+    { _pc = 0+    , _stack = mempty+    , _memory = mempty+    , _memorySize = 0+    , _code = theCode+    , _contract = vmoptAddress o+    , _codeContract = vmoptAddress o+    , _calldata = vmoptCalldata o+    , _callvalue = vmoptValue o+    , _caller = vmoptCaller o+    , _gas = w256 $ vmoptGas o+    , _returndata = mempty+    , _static = False+    }+  , _env = Env+    { _sha3Crack = mempty+    , _chainId = w256 $ vmoptChainId o+    , _contracts = Map.fromList+      [(vmoptAddress o, vmoptContract o)]+    , _keccakUsed = mempty+    , _storageModel = vmoptStorageModel o+    }+  , _cache = Cache (Map.fromList+    [(vmoptAddress o, vmoptContract o)])+    mempty+  , _burned = 0+  , _pathConditions = []+  , _iterations = mempty+  } where theCode = case _contractcode (vmoptContract o) of+            InitCode b    -> b+            RuntimeCode b -> b++-- | Initialize empty contract with given code+initialContract :: ContractCode -> Contract+initialContract theContractCode = Contract+  { _contractcode = theContractCode+  , _codehash =+    if BS.null theCode then 0 else+      keccak (stripBytecodeMetadata theCode)+  , _storage  = Concrete mempty+  , _balance  = 0+  , _nonce    = 0+  , _opIxMap  = mkOpIxMap theCode+  , _codeOps  = mkCodeOps theCode+  , _external = False+  , _origStorage = mempty+  } where theCode = case theContractCode of+            InitCode b    -> b+            RuntimeCode b -> b++contractWithStore :: ContractCode -> Storage -> Contract+contractWithStore theContractCode store =+  initialContract theContractCode & set storage store++-- * Opcode dispatch (exec1)++-- | Update program counter+next :: (?op :: Word8) => EVM ()+next = modifying (state . pc) (+ (opSize ?op))++-- | Executes the EVM one step+exec1 :: EVM ()+exec1 = do+  vm <- get++  let+    -- Convenience function to access parts of the current VM state.+    -- Arcane type signature needed to avoid monomorphism restriction.+    the :: (b -> VM -> Const a VM) -> ((a -> Const a a) -> b) -> a+    the f g = view (f . g) vm++    -- Convenient aliases+    mem  = the state memory+    stk  = the state stack+    self = the state contract+    this = fromMaybe (error "internal error: state contract") (preview (ix self) (the env contracts))++    fees@FeeSchedule {..} = the block schedule++    doStop = finishFrame (FrameReturned mempty)++  if self > 0x0 && self <= 0x9 then do+    -- call to precompile+    let ?op = 0x00 -- dummy value+    let+      calldatasize = snd (the state calldata)+    case unliteral calldatasize of+        Nothing -> vmError UnexpectedSymbolicArg+        Just calldatasize' -> do+          copyBytesToMemory (fst $ the state calldata) (num calldatasize') 0 0+          executePrecompile self (the state gas) 0 (num calldatasize') 0 0 []+          vmx <- get+          case view (state.stack) vmx of+            (x:_) -> case maybeLitWord x of+              Just 0 -> do+                fetchAccount self $ \_ -> do+                  touchAccount self+                  vmError PrecompileFailure+              Just _ ->+                fetchAccount self $ \_ -> do+                  touchAccount self+                  out <- use (state . returndata)+                  finishFrame (FrameReturned out)+              Nothing -> vmError UnexpectedSymbolicArg+            _ ->+              underrun++  else if the state pc >= num (BS.length (the state code))+    then doStop++    else do+      let ?op = BS.index (the state code) (the state pc)++      case ?op of++        -- op: PUSH+        x | x >= 0x60 && x <= 0x7f -> do+          let !n = num x - 0x60 + 1+              !xs = BS.take n (BS.drop (1 + the state pc)+                                       (the state code))+          limitStack 1 $+            burn g_verylow $ do+              next+              push (w256 (word xs))++        -- op: DUP+        x | x >= 0x80 && x <= 0x8f -> do+          let !i = x - 0x80 + 1+          case preview (ix (num i - 1)) stk of+            Nothing -> underrun+            Just y ->+              limitStack 1 $+                burn g_verylow $ do+                  next+                  pushSym y++        -- op: SWAP+        x | x >= 0x90 && x <= 0x9f -> do+          let i = num (x - 0x90 + 1)+          if length stk < i + 1+            then underrun+            else+              burn g_verylow $ do+                next+                zoom (state . stack) $ do+                  assign (ix 0) (stk ^?! ix i)+                  assign (ix i) (stk ^?! ix 0)++        -- op: LOG+        x | x >= 0xa0 && x <= 0xa4 ->+          notStatic $+          let n = (num x - 0xa0) in+          case stk of+            (xOffset':xSize':xs) ->+              if length xs < n+              then underrun+              else+                forceConcrete2 (xOffset', xSize') $ \(xOffset, xSize) -> do+                    let (topics, xs') = splitAt n xs+                        bytes         = readMemory (num xOffset) (num xSize) vm+                        log           = Log self bytes topics++                    burn (g_log + g_logdata * xSize + num n * g_logtopic) $+                      accessMemoryRange fees xOffset xSize $ do+                        traceLog log+                        next+                        assign (state . stack) xs'+                        pushToSequence logs log+            _ ->+              underrun++        -- op: STOP+        0x00 -> doStop++        -- op: ADD+        0x01 -> stackOp2 (const g_verylow) (uncurry (+))+        -- op: MUL+        0x02 -> stackOp2 (const g_low) (uncurry (*))+        -- op: SUB+        0x03 -> stackOp2 (const g_verylow) (uncurry (-))++        -- op: DIV+        0x04 -> stackOp2 (const g_low) (uncurry (sDiv))++        -- op: SDIV+        0x05 ->+          stackOp2 (const g_low) (uncurry sdiv)++        -- op: MOD+        0x06 -> stackOp2 (const g_low) $ \(x, y) -> ite (y .== 0) 0 (x `sMod` y)++        -- op: SMOD+        0x07 -> stackOp2 (const g_low) $ uncurry smod+        -- op: ADDMOD+        0x08 -> stackOp3 (const g_mid) (\(x, y, z) -> addmod x y z)+        -- op: MULMOD+        0x09 -> stackOp3 (const g_mid) (\(x, y, z) -> mulmod x y z)++        -- op: LT+        0x10 -> stackOp2 (const g_verylow) $ \(x, y) -> ite (x .< y) 1 0+        -- op: GT+        0x11 -> stackOp2 (const g_verylow) $ \(x, y) -> ite (x .> y) 1 0+        -- op: SLT+        0x12 -> stackOp2 (const g_verylow) $ uncurry slt+        -- op: SGT+        0x13 -> stackOp2 (const g_verylow) $ uncurry sgt++        -- op: EQ+        0x14 -> stackOp2 (const g_verylow) $ \(x, y) -> ite (x .== y) 1 0+        -- op: ISZERO+        0x15 -> stackOp1 (const g_verylow) $ \x -> ite (x .== 0) 1 0++        -- op: AND+        0x16 -> stackOp2 (const g_verylow) $ uncurry (.&.)+        -- op: OR+        0x17 -> stackOp2 (const g_verylow) $ uncurry (.|.)+        -- op: XOR+        0x18 -> stackOp2 (const g_verylow) $ uncurry xor+        -- op: NOT+        0x19 -> stackOp1 (const g_verylow) complement++        -- op: BYTE+        0x1a -> stackOp2 (const g_verylow) $ \case+          (n, _) | (forceLit n) >= 32 -> 0+          (n, x) | otherwise          -> 0xff .&. shiftR x (8 * (31 - num (forceLit n)))++        -- op: SHL+        0x1b -> stackOp2 (const g_verylow) $ \((S _ n), (S _ x)) -> sw256 $ sShiftLeft x n+        -- op: SHR+        0x1c -> stackOp2 (const g_verylow) $ \((S _ n), (S _ x)) -> sw256 $ sShiftRight x n+        -- op: SAR+        0x1d -> stackOp2 (const g_verylow) $ \((S _ n), (S _ x)) -> sw256 $ sSignedShiftArithRight x n++        -- op: SHA3+        -- more accurately refered to as KECCAK+        0x20 ->+          case stk of+            (xOffset' : xSize' : xs) ->+              forceConcrete xOffset' $+                \xOffset -> forceConcrete xSize' $ \xSize -> do+                  (hash, invMap) <- case readMemory xOffset xSize vm of+                                     ConcreteBuffer bs -> pure (litWord $ keccakBlob bs, Map.singleton (keccakBlob bs) bs)++                                     -- Although we would like to simply assert that the uninterpreted function symkeccak'+                                     -- is injective, this proves to cause a lot of concern for our smt solvers, probably+                                     -- due to the introduction of universal quantifiers into the queries.++                                     -- Instead, we keep track of all of the particular invocations of symkeccak' we see+                                     -- (similarly to sha3Crack), and simply assert that injectivity holds for these+                                     -- particular invocations.++                                     SymbolicBuffer bs -> do+                                                   let hash' = symkeccak' bs+                                                       previousUsed = view (env . keccakUsed) vm+                                                   env . keccakUsed <>= [(bs, hash')]+                                                   pathConditions <>= fmap (\(preimage, image) ->+                                                                               image .== hash' .=> preimage .== bs)+                                                                           previousUsed+                                                   return (sw256 hash', mempty)++                  burn (g_sha3 + g_sha3word * ceilDiv (num xSize) 32) $+                    accessMemoryRange fees xOffset xSize $ do+                      next+                      assign (state . stack) (hash : xs)+                      (env . sha3Crack) <>= invMap+            _ -> underrun++        -- op: ADDRESS+        0x30 ->+          limitStack 1 $+            burn g_base (next >> push (num self))++        -- op: BALANCE+        0x31 ->+          case stk of+            (x':xs) -> forceConcrete x' $ \x ->+              burn g_balance $+                fetchAccount (num x) $ \c -> do+                  next+                  assign (state . stack) xs+                  push (view balance c)+            [] ->+              underrun++        -- op: ORIGIN+        0x32 ->+          limitStack 1 . burn g_base $+            next >> push (num (the tx origin))++        -- op: CALLER+        0x33 ->+          limitStack 1 . burn g_base $+            let toSymWord = sw256 . sFromIntegral . saddressWord160+            in next >> pushSym (toSymWord (the state caller))++        -- op: CALLVALUE+        0x34 ->+          limitStack 1 . burn g_base $+            next >> pushSym (the state callvalue)++        -- op: CALLDATALOAD+        0x35 -> stackOp1 (const g_verylow) $+          \(S _ x) -> uncurry (readSWordWithBound (sFromIntegral x)) (the state calldata)++        -- op: CALLDATASIZE+        0x36 ->+          limitStack 1 . burn g_base $+            next >> pushSym (sw256 . zeroExtend . snd $ (the state calldata))++        -- op: CALLDATACOPY+        0x37 ->+          case stk of+            (xTo' : xFrom' : xSize' : xs) -> forceConcrete3 (xTo',xFrom',xSize') $ \(xTo,xFrom,xSize) ->+              burn (g_verylow + g_copy * ceilDiv xSize 32) $+                accessUnboundedMemoryRange fees xTo xSize $ do+                  next+                  assign (state . stack) xs+                  case the state calldata of+                    (SymbolicBuffer cd, cdlen) -> copyBytesToMemory (SymbolicBuffer [ite (i .<= cdlen) x 0 | (x, i) <- zip cd [1..]]) xSize xFrom xTo+                    -- when calldata is concrete,+                    -- the bound should always be equal to the bytestring length+                    (cd, _) -> copyBytesToMemory cd xSize xFrom xTo+            _ -> underrun++        -- op: CODESIZE+        0x38 ->+          limitStack 1 . burn g_base $+            next >> push (num (BS.length (the state code)))++        -- op: CODECOPY+        0x39 ->+          case stk of+            (memOffset' : codeOffset' : n' : xs) -> forceConcrete3 (memOffset',codeOffset',n') $ \(memOffset,codeOffset,n) -> do+              burn (g_verylow + g_copy * ceilDiv (num n) 32) $+                accessUnboundedMemoryRange fees memOffset n $ do+                  next+                  assign (state . stack) xs+                  copyBytesToMemory (ConcreteBuffer (the state code))+                    n codeOffset memOffset+            _ -> underrun++        -- op: GASPRICE+        0x3a ->+          limitStack 1 . burn g_base $+            next >> push (the tx gasprice)++        -- op: EXTCODESIZE+        0x3b ->+          case stk of+            (x':xs) -> forceConcrete x' $ \x ->+              if x == num cheatCode+                then do+                  next+                  assign (state . stack) xs+                  push (w256 1)+                else+                  burn g_extcode $+                    fetchAccount (num x) $ \c -> do+                      next+                      assign (state . stack) xs+                      push (num (BS.length (view bytecode c)))+            [] ->+              underrun++        -- op: EXTCODECOPY+        0x3c ->+          case stk of+            ( extAccount'+              : memOffset'+              : codeOffset'+              : codeSize'+              : xs ) ->+              forceConcrete4 (extAccount', memOffset', codeOffset', codeSize') $+                \(extAccount, memOffset, codeOffset, codeSize) ->+                  burn (g_extcode + g_copy * ceilDiv (num codeSize) 32) $+                    accessUnboundedMemoryRange fees memOffset codeSize $+                      fetchAccount (num extAccount) $ \c -> do+                        next+                        assign (state . stack) xs+                        copyBytesToMemory (ConcreteBuffer (view bytecode c))+                          codeSize codeOffset memOffset+            _ -> underrun++        -- op: RETURNDATASIZE+        0x3d ->+          limitStack 1 . burn g_base $+            next >> push (num $ len (the state returndata))++        -- op: RETURNDATACOPY+        0x3e ->+          case stk of+            (xTo' : xFrom' : xSize' :xs) -> forceConcrete3 (xTo', xFrom', xSize') $+              \(xTo, xFrom, xSize) ->+                burn (g_verylow + g_copy * ceilDiv xSize 32) $+                  accessUnboundedMemoryRange fees xTo xSize $ do+                    next+                    assign (state . stack) xs+                    if len (the state returndata) < num xFrom + num xSize+                    then vmError InvalidMemoryAccess+                    else copyBytesToMemory (the state returndata) xSize xFrom xTo+            _ -> underrun++        -- op: EXTCODEHASH+        0x3f ->+          case stk of+            (x':xs) -> forceConcrete x' $ \x ->+              burn g_extcodehash $ do+                next+                assign (state . stack) xs+                fetchAccount (num x) $ \c ->+                   if accountEmpty c+                     then push (num (0 :: Int))+                     else push (num (keccak (view bytecode c)))+            [] ->+              underrun++        -- op: BLOCKHASH+        0x40 -> do+          -- We adopt the fake block hash scheme of the VMTests,+          -- so that blockhash(i) is the hash of i as decimal ASCII.+          stackOp1 (const g_blockhash) $+            \(forceLit -> i) ->+              if i + 256 < the block number || i >= the block number+              then 0+              else+                (num i :: Integer)+                  & show & Char8.pack & keccak & num++        -- op: COINBASE+        0x41 ->+          limitStack 1 . burn g_base $+            next >> push (num (the block coinbase))++        -- op: TIMESTAMP+        0x42 ->+          limitStack 1 . burn g_base $+            next >> push (the block timestamp)++        -- op: NUMBER+        0x43 ->+          limitStack 1 . burn g_base $+            next >> push (the block number)++        -- op: DIFFICULTY+        0x44 ->+          limitStack 1 . burn g_base $+            next >> push (the block difficulty)++        -- op: GASLIMIT+        0x45 ->+          limitStack 1 . burn g_base $+            next >> push (the block gaslimit)++        -- op: CHAINID+        0x46 ->+          limitStack 1 . burn g_base $+            next >> push (the env chainId)++        -- op: SELFBALANCE+        0x47 ->+          limitStack 1 . burn g_low $+            next >> push (view balance this)++        -- op: POP+        0x50 ->+          case stk of+            (_:xs) -> burn g_base (next >> assign (state . stack) xs)+            _      -> underrun++        -- op: MLOAD+        0x51 ->+          case stk of+            (x':xs) -> forceConcrete x' $ \x ->+              burn g_verylow $+                accessMemoryWord fees x $ do+                  next+                  assign (state . stack) (view (word256At (num x)) mem : xs)+            _ -> underrun++        -- op: MSTORE+        0x52 ->+          case stk of+            (x':y:xs) -> forceConcrete x' $ \x ->+              burn g_verylow $+                accessMemoryWord fees x $ do+                  next+                  assign (state . memory . word256At (num x)) y+                  assign (state . stack) xs+            _ -> underrun++        -- op: MSTORE8+        0x53 ->+          case stk of+            (x':(S _ y):xs) -> forceConcrete x' $ \x ->+              burn g_verylow $+                accessMemoryRange fees x 1 $ do+                  let yByte = bvExtract (Proxy :: Proxy 7) (Proxy :: Proxy 0) y+                  next+                  modifying (state . memory) (setMemoryByte x yByte)+                  assign (state . stack) xs+            _ -> underrun++        -- op: SLOAD+        0x54 ->+          case stk of+            (x:xs) ->+              burn g_sload $+                accessStorage self x $ \y -> do+                  next+                  assign (state . stack) (y:xs)+            _ -> underrun++        -- op: SSTORE+        0x55 ->+          notStatic $+          case stk of+            (x:new:xs) ->+              accessStorage self x $ \current -> do+                availableGas <- use (state . gas)++                if availableGas <= g_callstipend+                  then finishFrame (FrameErrored (OutOfGas availableGas g_callstipend))+                  else do+                    let original = case view storage this of+                                  Concrete _ -> fromMaybe 0 (Map.lookup (forceLit x) (view origStorage this))+                                  Symbolic _ -> 0 -- we don't use this value anywhere anyway+                        cost = case (maybeLitWord current, maybeLitWord new) of+                                 (Just current', Just new') ->+                                    if (current' == new') then g_sload+                                    else if (current' == original) && (original == 0) then g_sset+                                    else if (current' == original) then g_sreset+                                    else g_sload++                                 -- if any of the arguments are symbolic,+                                 -- assume worst case scenario+                                 _ -> g_sset++                    burn cost $ do+                      next+                      assign (state . stack) xs+                      modifying (env . contracts . ix self . storage)+                        (writeStorage x new)++                      case (maybeLitWord current, maybeLitWord new) of+                         (Just current', Just new') ->+                            unless (current' == new') $+                              if current' == original+                              then when (original /= 0 && new' == 0) $+                                      refund r_sclear+                              else do+                                      when (original /= 0) $+                                        if new' == 0+                                        then refund r_sclear+                                        else unRefund r_sclear+                                      when (original == new') $+                                        if original == 0+                                        then refund (g_sset - g_sload)+                                        else refund (g_sreset - g_sload)+                         -- if any of the arguments are symbolic,+                         -- don't change the refund counter+                         _ -> noop+            _ -> underrun++        -- op: JUMP+        0x56 ->+          case stk of+            (x:xs) ->+              burn g_mid $ forceConcrete x $ \x' ->+                checkJump x' xs+            _ -> underrun++        -- op: JUMPI+        0x57 -> do+          case stk of+            (x:y:xs) -> forceConcrete x $ \x' ->+                burn g_high $+                  let jump :: Bool -> EVM ()+                      jump True = assign (state . stack) xs >> next+                      jump _    = checkJump x' xs+                  in case maybeLitWord y of+                      Just y' -> jump (0 == y')+                      -- if the jump condition is symbolic, an smt query has to be made.+                      Nothing -> askSMT (self, the state pc) y jump+            _ -> underrun++        -- op: PC+        0x58 ->+          limitStack 1 . burn g_base $+            next >> push (num (the state pc))++        -- op: MSIZE+        0x59 ->+          limitStack 1 . burn g_base $+            next >> push (num (the state memorySize))++        -- op: GAS+        0x5a ->+          limitStack 1 . burn g_base $+            next >> push (the state gas - g_base)++        -- op: JUMPDEST+        0x5b -> burn g_jumpdest next++        -- op: EXP+        0x0a ->+          let cost (_ ,(forceLit -> exponent)) =+                if exponent == 0+                then g_exp+                else g_exp + g_expbyte * num (ceilDiv (1 + log2 exponent) 8)+          in stackOp2 cost $ \((S _ x),(S _ y)) -> sw256 $ x .^ y++        -- op: SIGNEXTEND+        0x0b ->+          stackOp2 (const g_low) $ \((forceLit -> bytes), w@(S _ x)) ->+            if bytes >= 32 then w+            else let n = num bytes * 8 + 7 in+              sw256 $ ite (sTestBit x n)+                      (x .|. complement (bit n - 1))+                      (x .&. (bit n - 1))++        -- op: CREATE+        0xf0 ->+          notStatic $+          case stk of+            (xValue' : xOffset' : xSize' : xs) -> forceConcrete3 (xValue', xOffset', xSize') $+              \(xValue, xOffset, xSize) -> do+                accessMemoryRange fees xOffset xSize $ do+                  availableGas <- use (state . gas)+                  let+                    newAddr = createAddress self (wordValue (view nonce this))+                    (cost, gas') = costOfCreate fees availableGas 0+                  burn (cost - gas') $ forceConcreteBuffer (readMemory (num xOffset) (num xSize) vm) $ \initCode ->+                    create self this gas' xValue xs newAddr initCode+            _ -> underrun++        -- op: CALL+        0xf1 ->+          case stk of+            ( xGas'+              : xTo'+              : (forceLit -> xValue)+              : xInOffset'+              : xInSize'+              : xOutOffset'+              : xOutSize'+              : xs+             ) -> forceConcrete6 (xGas', xTo', xInOffset', xInSize', xOutOffset', xOutSize') $+              \(xGas, (num -> xTo), xInOffset, xInSize, xOutOffset, xOutSize) ->+              (if xValue > 0 then notStatic else id) $+                case xTo of+                  n | n > 0 && n <= 9 ->+                    precompiledContract this xGas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs+                  n | num n == cheatCode ->+                    do+                      assign (state . stack) xs+                      cheat (xInOffset, xInSize) (xOutOffset, xOutSize)+                  _ -> delegateCall this xGas xTo xTo xValue xInOffset xInSize xOutOffset xOutSize xs $ do+                            zoom state $ do+                              assign callvalue (litWord xValue)+                              assign caller (litAddr self)+                              assign contract xTo+                            zoom (env . contracts) $ do+                              ix self . balance -= xValue+                              ix xTo  . balance += xValue+                            touchAccount self+                            touchAccount xTo+            _ ->+              underrun++        -- op: CALLCODE+        0xf2 ->+          case stk of+            ( xGas'+              : xTo'+              : (forceLit -> xValue)+              : xInOffset'+              : xInSize'+              : xOutOffset'+              : xOutSize'+              : xs+              ) -> forceConcrete6 (xGas', xTo', xInOffset', xInSize', xOutOffset', xOutSize') $+              \(xGas, (num -> xTo), xInOffset, xInSize, xOutOffset, xOutSize) ->+                case xTo of+                  n | n > 0 && n <= 9 ->+                    precompiledContract this xGas xTo self xValue xInOffset xInSize xOutOffset xOutSize xs+                  _ -> delegateCall this xGas xTo self xValue xInOffset xInSize xOutOffset xOutSize xs $ do+                         zoom state $ do+                           assign callvalue (litWord xValue)+                           assign caller (litAddr self)+                         touchAccount self+            _ ->+              underrun++        -- op: RETURN+        0xf3 ->+          case stk of+            (xOffset' : xSize' :_) -> forceConcrete2 (xOffset', xSize') $ \(xOffset, xSize) ->+              accessMemoryRange fees xOffset xSize $ do+                let+                  output = readMemory xOffset xSize vm+                  codesize = num (len output)+                  maxsize = the block maxCodeSize+                case view frames vm of+                  [] ->+                    case (the tx isCreate) of+                      True ->+                        if codesize > maxsize+                        then+                          finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))+                        else+                          burn (g_codedeposit * codesize) $+                            finishFrame (FrameReturned output)+                      False ->+                        finishFrame (FrameReturned output)+                  (frame: _) -> do+                    let+                      context = view frameContext frame+                    case context of+                      CreationContext {} ->+                        if codesize > maxsize+                        then+                          finishFrame (FrameErrored (MaxCodeSizeExceeded maxsize codesize))+                        else+                          burn (g_codedeposit * codesize) $+                            finishFrame (FrameReturned output)+                      CallContext {} ->+                          finishFrame (FrameReturned output)+            _ -> underrun++        -- op: DELEGATECALL+        0xf4 ->+          case stk of+            (xGas'+             :xTo'+             :xInOffset'+             :xInSize'+             :xOutOffset'+             :xOutSize'+             :xs) -> forceConcrete6 (xGas', xTo', xInOffset', xInSize', xOutOffset', xOutSize') $+              \(xGas, (num -> xTo), xInOffset, xInSize, xOutOffset, xOutSize) ->+                case xTo of+                  n | n > 0 && n <= 9 ->+                    precompiledContract this xGas xTo self 0 xInOffset xInSize xOutOffset xOutSize xs+                  n | num n == cheatCode -> do+                        assign (state . stack) xs+                        cheat (xInOffset, xInSize) (xOutOffset, xOutSize)+                  _ -> do+                        delegateCall this xGas xTo self 0 xInOffset xInSize xOutOffset xOutSize xs $ do+                          touchAccount self+            _ -> underrun++        -- op: CREATE2+        0xf5 -> notStatic $+          case stk of+            (xValue'+             :xOffset'+             :xSize'+             :xSalt'+             :xs) -> forceConcrete4 (xValue', xOffset', xSize', xSalt') $+              \(xValue, xOffset, xSize, xSalt) ->+                accessMemoryRange fees xOffset xSize $ do+                  availableGas <- use (state . gas)+                  forceConcreteBuffer (readMemory (num xOffset) (num xSize) vm) $ \initCode ->+                   let+                    newAddr  = create2Address self (num xSalt) initCode+                    (cost, gas') = costOfCreate fees availableGas xSize+                   in burn (cost - gas') $+                    create self this gas' xValue xs newAddr initCode+            _ -> underrun++        -- op: STATICCALL+        0xfa ->+          case stk of+            (xGas'+             :xTo'+             :xInOffset'+             :xInSize'+             :xOutOffset'+             :xOutSize'+             :xs) -> forceConcrete6 (xGas', xTo', xInOffset', xInSize', xOutOffset', xOutSize') $+              \(xGas, (num -> xTo), xInOffset, xInSize, xOutOffset, xOutSize) ->+                case xTo of+                  n | n > 0 && n <= 9 ->+                    precompiledContract this xGas xTo xTo 0 xInOffset xInSize xOutOffset xOutSize xs+                  _ -> delegateCall this xGas xTo xTo 0 xInOffset xInSize xOutOffset xOutSize xs $ do+                            zoom state $ do+                              assign callvalue 0+                              assign caller (litAddr self)+                              assign contract xTo+                              assign static True+                            touchAccount self+                            touchAccount xTo+            _ ->+              underrun++        -- op: SELFDESTRUCT+        0xff ->+          notStatic $+          case stk of+            [] -> underrun+            (xTo':_) -> forceConcrete xTo' $ \(num -> xTo) ->+              let+                funds = view balance this+                recipientExists = accountExists xTo vm+                c_new = if not recipientExists && funds /= 0+                        then num g_selfdestruct_newaccount+                        else 0+              in burn (g_selfdestruct + c_new) $ do+                   destructs <- use (tx . substate . selfdestructs)+                   unless (elem self destructs) $ refund r_selfdestruct+                   selfdestruct self+                   touchAccount xTo++                   if funds /= 0+                   then fetchAccount xTo $ \_ -> do+                          env . contracts . ix xTo . balance += funds+                          assign (env . contracts . ix self . balance) 0+                          doStop+                   else doStop++        -- op: REVERT+        0xfd ->+          case stk of+            (xOffset':xSize':_) -> forceConcrete2 (xOffset', xSize') $ \(xOffset, xSize) ->+              accessMemoryRange fees xOffset xSize $ do+                let output = readMemory xOffset xSize vm+                finishFrame (FrameReverted output)+            _ -> underrun++        xxx ->+          vmError (UnrecognizedOpcode xxx)++-- | Checks a *CALL for failure; OOG, too many callframes, memory access etc.+callChecks+  :: (?op :: Word8)+  => Contract -> Word -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord]+   -- continuation with gas avail for call+  -> (Word -> EVM ())+  -> EVM ()+callChecks this xGas xContext xValue xInOffset xInSize xOutOffset xOutSize xs continue = do+  vm <- get+  let fees = view (block . schedule) vm+  accessMemoryRange fees xInOffset xInSize $+    accessMemoryRange fees xOutOffset xOutSize $ do+      availableGas <- use (state . gas)+      let recipientExists = accountExists xContext vm+          (cost, gas') = costOfCall fees recipientExists xValue availableGas xGas+      burn (cost - gas') $ do+        if xValue > view balance this+        then do+          assign (state . stack) (0 : xs)+          assign (state . returndata) mempty+          pushTrace $ ErrorTrace $ BalanceTooLow xValue (view balance this)+          next+        else if length (view frames vm) >= 1024+             then do+               assign (state . stack) (0 : xs)+               assign (state . returndata) mempty+               pushTrace $ ErrorTrace $ CallDepthLimitReached+               next+             else continue gas'++precompiledContract+  :: (?op :: Word8)+  => Contract+  -> Word+  -> Addr+  -> Addr+  -> Word+  -> Word -> Word -> Word -> Word+  -> [SymWord]+  -> EVM ()+precompiledContract this xGas precompileAddr recipient xValue inOffset inSize outOffset outSize xs =+  callChecks this xGas recipient xValue inOffset inSize outOffset outSize xs $ \gas' ->+  do+    executePrecompile precompileAddr gas' inOffset inSize outOffset outSize xs+    self <- use (state . contract)+    stk <- use (state . stack)+    case stk of+      (x:_) -> case maybeLitWord x of+        Just 0 ->+          return ()+        Just 1 ->+          fetchAccount recipient $ \_ -> do++          zoom (env . contracts) $ do+            ix self . balance -= xValue+            ix recipient  . balance += xValue+          touchAccount self+          touchAccount recipient+          touchAccount precompileAddr+        _ -> vmError UnexpectedSymbolicArg+      _ -> underrun++executePrecompile+  :: (?op :: Word8)+  => Addr+  -> Word -> Word -> Word -> Word -> Word -> [SymWord]+  -> EVM ()+executePrecompile preCompileAddr gasCap inOffset inSize outOffset outSize xs  = do+  vm <- get+  let input = readMemory (num inOffset) (num inSize) vm+      fees = view (block . schedule) vm+      cost = costOfPrecompile fees preCompileAddr input+      notImplemented = error $ "precompile at address " <> show preCompileAddr <> " not yet implemented"+      precompileFail = burn (gasCap - cost) $ do+                         assign (state . stack) (0 : xs)+                         pushTrace $ ErrorTrace $ PrecompileFailure+                         next+  if cost > gasCap then+    burn gasCap $ do+      assign (state . stack) (0 : xs)+      next+  else+    burn cost $+      case preCompileAddr of+        -- ECRECOVER+        0x1 ->+         -- TODO: support symbolic variant+         forceConcreteBuffer input $ \input' ->+          case EVM.Precompiled.execute 0x1 (truncpadlit 128 input') 32 of+            Nothing -> do+              -- return no output for invalid signature+              assign (state . stack) (1 : xs)+              assign (state . returndata) mempty+              next+            Just output -> do+              assign (state . stack) (1 : xs)+              assign (state . returndata) (ConcreteBuffer output)+              copyBytesToMemory (ConcreteBuffer output) outSize 0 outOffset+              next++        -- SHA2-256+        0x2 ->+          let+            hash = case input of+                     ConcreteBuffer input' -> ConcreteBuffer $ BS.pack $ BA.unpack $ (Crypto.hash input' :: Digest SHA256)+                     SymbolicBuffer input' -> SymbolicBuffer $ symSHA256 input'+          in do+            assign (state . stack) (1 : xs)+            assign (state . returndata) hash+            copyBytesToMemory hash outSize 0 outOffset+            next++        -- RIPEMD-160+        0x3 ->+         -- TODO: support symbolic variant+         forceConcreteBuffer input $ \input' ->++          let+            padding = BS.pack $ replicate 12 0+            hash' = BS.pack $ BA.unpack (Crypto.hash input' :: Digest RIPEMD160)+            hash  = ConcreteBuffer $ padding <> hash'+          in do+            assign (state . stack) (1 : xs)+            assign (state . returndata) hash+            copyBytesToMemory hash outSize 0 outOffset+            next++        -- IDENTITY+        0x4 -> do+            assign (state . stack) (1 : xs)+            assign (state . returndata) input+            copyCallBytesToMemory input outSize 0 outOffset+            next++        -- MODEXP+        0x5 ->+         -- TODO: support symbolic variant+         forceConcreteBuffer input $ \input' ->++          let+            (lenb, lene, lenm) = parseModexpLength input'++            output = ConcreteBuffer $+              case (isZero (96 + lenb + lene) lenm input') of+                 True ->+                   truncpadlit (num lenm) (asBE (0 :: Int))+                 False ->+                   let+                     b = asInteger $ lazySlice 96 lenb $ input'+                     e = asInteger $ lazySlice (96 + lenb) lene $ input'+                     m = asInteger $ lazySlice (96 + lenb + lene) lenm $ input'+                   in+                     padLeft (num lenm) (asBE (expFast b e m))+          in do+            assign (state . stack) (1 : xs)+            assign (state . returndata) output+            copyBytesToMemory output outSize 0 outOffset+            next++        -- ECADD+        0x6 ->+         -- TODO: support symbolic variant+         forceConcreteBuffer input $ \input' ->+           case EVM.Precompiled.execute 0x6 (truncpadlit 128 input') 64 of+          Nothing -> precompileFail+          Just output -> do+            let truncpaddedOutput = ConcreteBuffer $ truncpadlit 64 output+            assign (state . stack) (1 : xs)+            assign (state . returndata) truncpaddedOutput+            copyBytesToMemory truncpaddedOutput outSize 0 outOffset+            next++        -- ECMUL+        0x7 ->+         -- TODO: support symbolic variant+         forceConcreteBuffer input $ \input' ->++          case EVM.Precompiled.execute 0x7 (truncpadlit 96 input') 64 of+          Nothing -> precompileFail+          Just output -> do+            let truncpaddedOutput = ConcreteBuffer $ truncpadlit 64 output+            assign (state . stack) (1 : xs)+            assign (state . returndata) truncpaddedOutput+            copyBytesToMemory truncpaddedOutput outSize 0 outOffset+            next++        -- ECPAIRING+        0x8 ->+         -- TODO: support symbolic variant+         forceConcreteBuffer input $ \input' ->++          case EVM.Precompiled.execute 0x8 input' 32 of+          Nothing -> precompileFail+          Just output -> do+            let truncpaddedOutput = ConcreteBuffer $ truncpadlit 32 output+            assign (state . stack) (1 : xs)+            assign (state . returndata) truncpaddedOutput+            copyBytesToMemory truncpaddedOutput outSize 0 outOffset+            next++        -- BLAKE2+        0x9 ->+         -- TODO: support symbolic variant+         forceConcreteBuffer input $ \input' -> do++          case (BS.length input', 1 >= BS.last input') of+            (213, True) -> case EVM.Precompiled.execute 0x9 input' 64 of+              Just output -> do+                let truncpaddedOutput = ConcreteBuffer $ truncpadlit 64 output+                assign (state . stack) (1 : xs)+                assign (state . returndata) truncpaddedOutput+                copyBytesToMemory truncpaddedOutput outSize 0 outOffset+                next+              Nothing -> precompileFail+            _ -> precompileFail+++        _   -> notImplemented++truncpadlit :: Int -> ByteString -> ByteString+truncpadlit n xs = if m > n then BS.take n xs+                   else BS.append xs (BS.replicate (n - m) 0)+  where m = BS.length xs++lazySlice :: Word -> Word -> ByteString -> LS.ByteString+lazySlice offset size bs =+  let bs' = LS.take (num size) (LS.drop (num offset) (fromStrict bs))+  in bs' <> LS.replicate ((num size) - LS.length bs') 0++parseModexpLength :: ByteString -> (Word, Word, Word)+parseModexpLength input =+  let lenb = w256 $ word $ LS.toStrict $ lazySlice  0 32 input+      lene = w256 $ word $ LS.toStrict $ lazySlice 32 64 input+      lenm = w256 $ word $ LS.toStrict $ lazySlice 64 96 input+  in (lenb, lene, lenm)++isZero :: Word -> Word -> ByteString -> Bool+isZero offset size bs =+  LS.all (== 0) $+    LS.take (num size) $+      LS.drop (num offset) $+        fromStrict bs++asInteger :: LS.ByteString -> Integer+asInteger xs = if xs == mempty then 0+  else 256 * asInteger (LS.init xs)+      + num (LS.last xs)++-- * Opcode helper actions++noop :: Monad m => m ()+noop = pure ()++pushTo :: MonadState s m => ASetter s s [a] [a] -> a -> m ()+pushTo f x = f %= (x :)++pushToSequence :: MonadState s m => ASetter s s (Seq a) (Seq a) -> a -> m ()+pushToSequence f x = f %= (Seq.|> x)++getCodeLocation :: VM -> CodeLocation+getCodeLocation vm = (view (state . contract) vm, view (state . pc) vm)++-- | Construct SMT Query and halt execution until resolved+askSMT :: CodeLocation -> SymWord -> (Bool -> EVM ()) -> EVM ()+askSMT codeloc jumpcondition continue = do+  -- We keep track of how many times we have come across this particular+  -- (contract, pc) combination in the `iteration` mapping.+  iteration <- use (iterations . at codeloc . non 0)++  -- If we are backstepping, the result of this query should be cached+  -- already. So we first check the cache to see if the result is known+  use (cache . path . at (codeloc, iteration)) >>= \case+     -- If the query has been done already, select path or select the only available+     Just w -> choosePath (Iszero w)+     -- If this is a new query, run the query, cache the result+     -- increment the iterations and select appropriate path+     Nothing -> do pathconds <- use pathConditions+                   assign result . Just . VMFailure . Query $ PleaseAskSMT+                     jumpcondition pathconds choosePath++   where -- Only one path is possible+         choosePath :: JumpCondition -> EVM ()+         choosePath (Iszero v) = do assign result Nothing+                                    pathConditions <>= if v then [litWord 0 .== jumpcondition] else [litWord 0 ./= jumpcondition]+                                    iteration <- use (iterations . at codeloc . non 0)+                                    assign (cache . path . at (codeloc, iteration)) (Just v)+                                    assign (iterations . at codeloc) (Just (iteration + 1))+                                    continue v+         -- Both paths are possible; we ask for more input+         choosePath Unknown = assign result . Just . VMFailure . Choose . PleaseChoosePath $ choosePath . Iszero+         -- None of the paths are possible; fail this branch+         choosePath Inconsistent = vmError DeadPath++-- | Construct RPC Query and halt execution until resolved+fetchAccount :: Addr -> (Contract -> EVM ()) -> EVM ()+fetchAccount addr continue =+  use (env . contracts . at addr) >>= \case+    Just c -> continue c+    Nothing ->+      use (cache . fetched . at addr) >>= \case+        Just c -> do+          assign (env . contracts . at addr) (Just c)+          continue c+        Nothing ->+          assign result . Just . VMFailure . Query $+            PleaseFetchContract addr+              (\c -> do assign (cache . fetched . at addr) (Just c)+                        assign (env . contracts . at addr) (Just c)+                        assign result Nothing+                        tryContinue c)+  where+    tryContinue c =+      if (view external c) && (accountEmpty c)+        then vmError . NoSuchContract $ addr+        else continue c++readStorage :: Storage -> SymWord -> Maybe (SymWord)+readStorage (Symbolic s) (S _ loc) = Just . sw256 $ readArray s loc+readStorage (Concrete s) loc = Map.lookup (forceLit loc) s++writeStorage :: SymWord -> SymWord -> Storage -> Storage+writeStorage (S _ loc) (S _ val) (Symbolic s) = Symbolic (writeArray s loc val)+writeStorage loc val (Concrete s) = Concrete (Map.insert (forceLit loc) val s)++accessStorage+  :: Addr                -- ^ Contract address+  -> SymWord             -- ^ Storage slot key+  -> (SymWord -> EVM ()) -- ^ Continuation+  -> EVM ()+accessStorage addr slot continue =+  use (env . contracts . at addr) >>= \case+    Just c ->+      case readStorage (view storage c) slot of+        -- Notice that if storage is symbolic, we always continue straight away+        Just x ->+          continue x+        Nothing ->+          if view external c+          then+            -- check if the slot is cached+            use (cache . fetched . at addr) >>= \case+              Nothing -> mkQuery+              Just cachedContract ->+                maybe mkQuery continue (readStorage (view storage cachedContract) slot)+          else do+            modifying (env . contracts . ix addr . storage) (writeStorage slot 0)+            continue 0+    Nothing ->+      fetchAccount addr $ \_ ->+        accessStorage addr slot continue+  where+      mkQuery = assign result . Just . VMFailure . Query $+                  PleaseFetchSlot addr (forceLit slot)+                    (\(litWord -> x) -> do+                        modifying (cache . fetched . ix addr . storage) (writeStorage slot x)+                        modifying (env . contracts . ix addr . storage) (writeStorage slot x)+                        assign result Nothing+                        continue x)++accountExists :: Addr -> VM -> Bool+accountExists addr vm =+  case view (env . contracts . at addr) vm of+    Just c -> not (accountEmpty c)+    Nothing -> False++-- EIP 161+accountEmpty :: Contract -> Bool+accountEmpty c =+  (view contractcode c == RuntimeCode mempty)+  && (view nonce c == 0)+  && (view balance c == 0)++-- * How to finalize a transaction+finalize :: EVM ()+finalize = do+  let+    burnRemainingGas = use (state . gas) >>= flip burn noop+    revertContracts  = use (tx . txReversion) >>= assign (env . contracts)+    revertSubstate   = assign (tx . substate) (SubState mempty mempty mempty)++  use result >>= \case+    Nothing ->+      error "Finalising an unfinished tx."+    Just (VMFailure (Revert _)) -> do+      revertContracts+      revertSubstate+    Just (VMFailure _) -> do+      burnRemainingGas+      revertContracts+      revertSubstate+    Just (VMSuccess output) -> do+      -- deposit the code from a creation tx+      creation <- use (tx . isCreate)+      createe  <- use (state . contract)+      createeExists <- (Map.member createe) <$> use (env . contracts)++      when (creation && createeExists) $ forceConcreteBuffer output $ \code' -> replaceCode createe (RuntimeCode code')++  -- compute and pay the refund to the caller and the+  -- corresponding payment to the miner+  txOrigin     <- use (tx . origin)+  sumRefunds   <- (sum . (snd <$>)) <$> (use (tx . substate . refunds))+  miner        <- use (block . coinbase)+  blockReward  <- r_block <$> (use (block . schedule))+  gasPrice     <- use (tx . gasprice)+  gasLimit     <- use (tx . txgaslimit)+  gasRemaining <- use (state . gas)++  let+    gasUsed      = gasLimit - gasRemaining+    cappedRefund = min (quot gasUsed 2) sumRefunds+    originPay    = (gasRemaining + cappedRefund) * gasPrice+    minerPay     = gasPrice * (gasUsed - cappedRefund)++  modifying (env . contracts)+     (Map.adjust (over balance (+ originPay)) txOrigin)+  modifying (env . contracts)+     (Map.adjust (over balance (+ minerPay)) miner)+  touchAccount miner++  -- pay out the block reward, recreating the miner if necessary+  preuse (env . contracts . ix miner) >>= \case+    Nothing -> modifying (env . contracts)+      (Map.insert miner (initialContract (EVM.RuntimeCode mempty)))+    Just _  -> noop+  modifying (env . contracts)+    (Map.adjust (over balance (+ blockReward)) miner)++  -- perform state trie clearing (EIP 161), of selfdestructs+  -- and touched accounts. addresses are cleared if they have+  --    a) selfdestructed, or+  --    b) been touched and+  --    c) are empty.+  -- (see Yellow Paper "Accrued Substate")+  --+  -- remove any destructed addresses+  destroyedAddresses <- use (tx . substate . selfdestructs)+  modifying (env . contracts)+    (Map.filterWithKey (\k _ -> (notElem k destroyedAddresses)))+  -- then, clear any remaining empty and touched addresses+  touchedAddresses <- use (tx . substate . touchedAccounts)+  modifying (env . contracts)+    (Map.filterWithKey+      (\k a -> not ((elem k touchedAddresses) && accountEmpty a)))++-- | Loads the selected contract as the current contract to execute+loadContract :: Addr -> EVM ()+loadContract target =+  preuse (env . contracts . ix target . contractcode) >>=+    \case+      Nothing ->+        error "Call target doesn't exist"+      Just (InitCode targetCode) -> do+        assign (state . contract) target+        assign (state . code)     targetCode+        assign (state . codeContract) target+      Just (RuntimeCode targetCode) -> do+        assign (state . contract) target+        assign (state . code)     targetCode+        assign (state . codeContract) target++limitStack :: Int -> EVM () -> EVM ()+limitStack n continue = do+  stk <- use (state . stack)+  if length stk + n > 1024+    then vmError StackLimitExceeded+    else continue++notStatic :: EVM () -> EVM ()+notStatic continue = do+  bad <- use (state . static)+  if bad+    then vmError StateChangeWhileStatic+    else continue++-- | Burn gas, failing if insufficient gas is available+burn :: Word -> EVM () -> EVM ()+burn n continue = do+  available <- use (state . gas)+  if n <= available+    then do+      state . gas -= n+      burned += n+      continue+    else+      vmError (OutOfGas available n)++forceConcreteAddr :: SAddr -> (Addr -> EVM ()) -> EVM ()+forceConcreteAddr n continue = case maybeLitAddr n of+  Nothing -> vmError UnexpectedSymbolicArg+  Just c -> continue c++forceConcrete :: SymWord -> (Word -> EVM ()) -> EVM ()+forceConcrete n continue = case maybeLitWord n of+  Nothing -> vmError UnexpectedSymbolicArg+  Just c -> continue c++forceConcrete2 :: (SymWord, SymWord) -> ((Word, Word) -> EVM ()) -> EVM ()+forceConcrete2 (n,m) continue = case (maybeLitWord n, maybeLitWord m) of+  (Just c, Just d) -> continue (c, d)+  _ -> vmError UnexpectedSymbolicArg++forceConcrete3 :: (SymWord, SymWord, SymWord) -> ((Word, Word, Word) -> EVM ()) -> EVM ()+forceConcrete3 (k,n,m) continue = case (maybeLitWord k, maybeLitWord n, maybeLitWord m) of+  (Just c, Just d, Just f) -> continue (c, d, f)+  _ -> vmError UnexpectedSymbolicArg++forceConcrete4 :: (SymWord, SymWord, SymWord, SymWord) -> ((Word, Word, Word, Word) -> EVM ()) -> EVM ()+forceConcrete4 (k,l,n,m) continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord n, maybeLitWord m) of+  (Just b, Just c, Just d, Just f) -> continue (b, c, d, f)+  _ -> vmError UnexpectedSymbolicArg++forceConcrete5 :: (SymWord, SymWord, SymWord, SymWord, SymWord) -> ((Word, Word, Word, Word, Word) -> EVM ()) -> EVM ()+forceConcrete5 (k,l,m,n,o) continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord m, maybeLitWord n, maybeLitWord o) of+  (Just a, Just b, Just c, Just d, Just e) -> continue (a, b, c, d, e)+  _ -> vmError UnexpectedSymbolicArg++forceConcrete6 :: (SymWord, SymWord, SymWord, SymWord, SymWord, SymWord) -> ((Word, Word, Word, Word, Word, Word) -> EVM ()) -> EVM ()+forceConcrete6 (k,l,m,n,o,p) continue = case (maybeLitWord k, maybeLitWord l, maybeLitWord m, maybeLitWord n, maybeLitWord o, maybeLitWord p) of+  (Just a, Just b, Just c, Just d, Just e, Just f) -> continue (a, b, c, d, e, f)+  _ -> vmError UnexpectedSymbolicArg++forceConcreteBuffer :: Buffer -> (ByteString -> EVM ()) -> EVM ()+forceConcreteBuffer (SymbolicBuffer b) continue = case maybeLitBytes b of+  Nothing -> vmError UnexpectedSymbolicArg+  Just bs -> continue bs+forceConcreteBuffer (ConcreteBuffer b) continue = continue b++-- * Substate manipulation+refund :: Word -> EVM ()+refund n = do+  self <- use (state . contract)+  pushTo (tx . substate . refunds) (self, n)++unRefund :: Word -> EVM ()+unRefund n = do+  self <- use (state . contract)+  refs <- use (tx . substate . refunds)+  assign (tx . substate . refunds)+    (filter (\(a,b) -> not (a == self && b == n)) refs)++touchAccount :: Addr -> EVM()+touchAccount = pushTo ((tx . substate) . touchedAccounts)++selfdestruct :: Addr -> EVM()+selfdestruct = pushTo ((tx . substate) . selfdestructs)++-- * Cheat codes++-- The cheat code is 7109709ecfa91a80626ff3989d68f67f5b1dd12d.+-- Call this address using one of the cheatActions below to do+-- special things, e.g. changing the block timestamp. Beware that+-- these are necessarily hevm specific.+cheatCode :: Addr+cheatCode = num (keccak "hevm cheat code")++cheat+  :: (?op :: Word8)+  => (Word, Word) -> (Word, Word)+  -> EVM ()+cheat (inOffset, inSize) (outOffset, outSize) = do+  mem <- use (state . memory)+  vm <- get+  let+    abi = readMemoryWord32 inOffset mem+    input = readMemory (inOffset + 4) (inSize - 4) vm+  case fromSized <$> unliteral abi of+    Nothing -> vmError UnexpectedSymbolicArg+    Just abi ->+              case Map.lookup abi cheatActions of+                Nothing ->+                  vmError (BadCheatCode (Just abi))+                Just (argTypes, action) ->+                  case input of+                    SymbolicBuffer _ -> vmError UnexpectedSymbolicArg+                    ConcreteBuffer input' ->+                      case runGetOrFail+                             (getAbiSeq (length argTypes) argTypes)+                             (LS.fromStrict input') of+                        Right ("", _, args) ->+                          action (toList args) >>= \case+                            Nothing -> do+                              next+                              push 1+                            Just (encodeAbiValue -> bs) -> do+                              next+                              modifying (state . memory)+                                (writeMemory (ConcreteBuffer bs) outSize 0 outOffset)+                              push 1+                        _ ->+                          vmError (BadCheatCode (Just abi))++type CheatAction = ([AbiType], [AbiValue] -> EVM (Maybe AbiValue))++cheatActions :: Map Word32 CheatAction+cheatActions =+  Map.fromList+    [ action "warp(uint256)" [AbiUIntType 256] $+        \[AbiUInt 256 x] -> do+          assign (block . timestamp) (w256 (W256 x))+          return Nothing,+      action "store(address,bytes32,bytes32)" [AbiAddressType, AbiBytesType 32, AbiBytesType 32] $+        \[AbiAddress a, AbiBytes 32 x, AbiBytes 32 y] -> do+          let slot = w256lit $ word x+              new  = w256lit $ word y+          fetchAccount a $ \_ -> do+            modifying (env . contracts . ix a . storage) (writeStorage slot new)+          return Nothing+    ]+  where+    action s ts f = (abiKeccak s, (ts, f))++-- * General call implementation ("delegateCall")+delegateCall+  :: (?op :: Word8)+  => Contract -> Word -> Addr -> Addr -> Word -> Word -> Word -> Word -> Word -> [SymWord]+  -> EVM ()+  -> EVM ()+delegateCall this gasGiven xTo xContext xValue xInOffset xInSize xOutOffset xOutSize xs continue =+  callChecks this gasGiven xContext xValue xInOffset xInSize xOutOffset xOutSize xs $+  \xGas -> do+    vm0 <- get+    fetchAccount xTo . const $+      preuse (env . contracts . ix xTo) >>= \case+        Nothing ->+          vmError (NoSuchContract xTo)+        Just target ->+          burn xGas $ do+            let newContext = CallContext+                  { callContextOffset = xOutOffset+                  , callContextSize = xOutSize+                  , callContextCodehash = view codehash target+                  , callContextReversion = view (env . contracts) vm0+                  , callContextSubState = view (tx . substate) vm0+                  , callContextAbi =+                      if xInSize >= 4+                      then case unliteral $ readMemoryWord32 xInOffset (view (state . memory) vm0)+                           of Nothing -> Nothing+                              Just abi -> Just . w256 $ num abi+                      else Nothing+                  , callContextData = (readMemory (num xInOffset) (num xInSize) vm0)+                  }++            pushTrace (FrameTrace newContext)+            next+            vm1 <- get++            pushTo frames $ Frame+              { _frameState = (set stack xs) (view state vm1)+              , _frameContext = newContext+              }++            zoom state $ do+              assign gas xGas+              assign pc 0+              assign code (view bytecode target)+              assign codeContract xTo+              assign stack mempty+              assign memory mempty+              assign memorySize 0+              assign returndata mempty+              assign calldata (readMemory (num xInOffset) (num xInSize) vm0, literal (num xInSize))++            continue++-- -- * Contract creation++-- EIP 684+collision :: Maybe Contract -> Bool+collision c' = case c' of+  Just c -> (view contractcode c /= RuntimeCode mempty) || (view nonce c /= 0)+  Nothing -> False++create :: (?op :: Word8)+  => Addr -> Contract+  -> Word -> Word -> [SymWord] -> Addr -> ByteString -> EVM ()+create self this xGas xValue xs newAddr initCode = do+  vm0 <- get+  if xValue > view balance this+  then do+    assign (state . stack) (0 : xs)+    assign (state . returndata) mempty+    pushTrace $ ErrorTrace $ BalanceTooLow xValue (view balance this)+    next+  else if length (view frames vm0) >= 1024+  then do+    assign (state . stack) (0 : xs)+    assign (state . returndata) mempty+    pushTrace $ ErrorTrace $ CallDepthLimitReached+    next+  else if collision $ view (env . contracts . at newAddr) vm0+  then burn xGas $ do+    assign (state . stack) (0 : xs)+    modifying (env . contracts . ix self . nonce) succ+    next+  else burn xGas $ do+        touchAccount self+        touchAccount newAddr+        let+          store = case view (env . storageModel) vm0 of+            ConcreteS -> Concrete mempty+            SymbolicS -> Symbolic $ sListArray 0 []+            InitialS -> Symbolic $ sListArray 0 []+          newContract =+            initialContract (InitCode initCode) & set storage store+          newContext  =+            CreationContext { creationContextCodehash  = view codehash newContract+                            , creationContextReversion = view (env . contracts) vm0+                            , creationContextSubstate = view (tx . substate) vm0+                            }++        zoom (env . contracts) $ do+          oldAcc <- use (at newAddr)+          let oldBal = case oldAcc of+                Nothing -> 0+                Just c  -> view balance c+          assign (at newAddr) (Just newContract)+          assign (ix newAddr . balance) (oldBal + xValue)+          assign (ix newAddr . nonce) 1+          modifying (ix self . balance) (flip (-) xValue)+          modifying (ix self . nonce) succ++        pushTrace (FrameTrace newContext)+        next+        vm1 <- get+        pushTo frames $ Frame+          { _frameContext = newContext+          , _frameState   = (set stack xs) (view state vm1)+          }++        assign state $+          blankState+            & set contract   newAddr+            & set codeContract newAddr+            & set code       initCode+            & set callvalue  (litWord xValue)+            & set caller     (litAddr self)+            & set gas        xGas++-- | Replace a contract's code, like when CREATE returns+-- from the constructor code.+replaceCode :: Addr -> ContractCode -> EVM ()+replaceCode target newCode =+  zoom (env . contracts . at target) $+    get >>= \case+      Just now -> case (view contractcode now) of+        InitCode _ ->+          put . Just $+          initialContract newCode+          & set storage (view storage now)+          & set balance (view balance now)+          & set nonce   (view nonce now)+        RuntimeCode _ ->+          error "internal error: can't replace code of deployed contract"+      Nothing ->+        error "internal error: can't replace code of nonexistent contract"++replaceCodeOfSelf :: ContractCode -> EVM ()+replaceCodeOfSelf newCode = do+  vm <- get+  replaceCode (view (state . contract) vm) newCode++resetState :: EVM ()+resetState = do+  assign result Nothing+  assign frames []+  assign state  blankState+++-- * VM error implementation++vmError :: Error -> EVM ()+vmError e = finishFrame (FrameErrored e)++underrun :: EVM ()+underrun = vmError StackUnderrun++-- | A stack frame can be popped in three ways.+data FrameResult+  = FrameReturned Buffer -- ^ STOP, RETURN, or no more code+  | FrameReverted Buffer -- ^ REVERT+  | FrameErrored Error -- ^ Any other error+  deriving Show++-- | This function defines how to pop the current stack frame in either of+-- the ways specified by 'FrameResult'.+--+-- It also handles the case when the current stack frame is the only one;+-- in this case, we set the final '_result' of the VM execution.+finishFrame :: FrameResult -> EVM ()+finishFrame how = do+  oldVm <- get++  case view frames oldVm of+    -- Is the current frame the only one?+    [] -> do+      case how of+          FrameReturned output -> assign result . Just $ VMSuccess output+          FrameReverted buffer -> forceConcreteBuffer buffer $ \out -> assign result . Just $ VMFailure (Revert out)+          FrameErrored e       -> assign result . Just $ VMFailure e+      finalize++    -- Are there some remaining frames?+    nextFrame : remainingFrames -> do++      -- Pop the top frame.+      assign frames remainingFrames+      -- Install the state of the frame to which we shall return.+      assign state (view frameState nextFrame)+      -- Insert a debug trace.+      insertTrace $+        case how of+          FrameErrored e ->+            ErrorTrace e+          FrameReverted (ConcreteBuffer output) ->+            ErrorTrace (Revert output)+          FrameReverted (SymbolicBuffer output) ->+            ErrorTrace (Revert (forceLitBytes output))+          FrameReturned output ->+            ReturnTrace output (view frameContext nextFrame)+      -- Pop to the previous level of the debug trace stack.+      popTrace++      -- When entering a call, the gas allowance is counted as burned+      -- in advance; this unburns the remainder and adds it to the+      -- parent frame.+      let remainingGas = view (state . gas) oldVm+          reclaimRemainingGasAllowance = do+            modifying burned (subtract remainingGas)+            modifying (state . gas) (+ remainingGas)++          FeeSchedule {..} = view ( block . schedule ) oldVm++      -- Now dispatch on whether we were creating or calling,+      -- and whether we shall return, revert, or error (six cases).+      case view frameContext nextFrame of++        -- Were we calling?+        CallContext (num -> outOffset) (num -> outSize) _ _ _ reversion substate' -> do++          let+            revertContracts = assign (env . contracts) reversion+            revertSubstate  = assign (tx . substate) substate'++          case how of+            -- Case 1: Returning from a call?+            FrameReturned output -> do+              assign (state . returndata) output+              copyCallBytesToMemory output outSize 0 outOffset+              reclaimRemainingGasAllowance+              push 1++            -- Case 2: Reverting during a call?+            FrameReverted output -> do+              revertContracts+              revertSubstate+              assign (state . returndata) output+              copyCallBytesToMemory output outSize 0 outOffset+              reclaimRemainingGasAllowance+              push 0++            -- Case 3: Error during a call?+            FrameErrored _ -> do+              revertContracts+              revertSubstate+              assign (state . returndata) mempty+              push 0++        -- Or were we creating?+        CreationContext _ reversion substate' -> do+          creator <- use (state . contract)+          let+            createe = view (state . contract) oldVm+            revertContracts = assign (env . contracts) reversion'+            revertSubstate  = assign (tx . substate) substate'++            -- persist the nonce through the reversion+            reversion' = (Map.adjust (over nonce (+ 1)) creator) reversion++          case how of+            -- Case 4: Returning during a creation?+            FrameReturned output ->+              forceConcreteBuffer output $ \output' -> do+                replaceCode createe (RuntimeCode output')+                assign (state . returndata) mempty+                reclaimRemainingGasAllowance+                push (num createe)++            -- Case 5: Reverting during a creation?+            FrameReverted output -> do+              revertContracts+              revertSubstate+              assign (state . returndata) output+              reclaimRemainingGasAllowance+              push 0++            -- Case 6: Error during a creation?+            FrameErrored _ -> do+              revertContracts+              revertSubstate+              assign (state . returndata) mempty+              push 0+++-- * Memory helpers++accessUnboundedMemoryRange+  :: FeeSchedule Word+  -> Word+  -> Word+  -> EVM ()+  -> EVM ()+accessUnboundedMemoryRange _ _ 0 continue = continue+accessUnboundedMemoryRange fees f l continue = do+  m0 <- num <$> use (state . memorySize)+  do+    let m1 = 32 * ceilDiv (max m0 (num f + num l)) 32+    burn (memoryCost fees m1 - memoryCost fees m0) $ do+      assign (state . memorySize) (num m1)+      continue++accessMemoryRange+  :: FeeSchedule Word+  -> Word+  -> Word+  -> EVM ()+  -> EVM ()+accessMemoryRange _ _ 0 continue = continue+accessMemoryRange fees f l continue =+  if f + l < l+    then vmError IllegalOverflow+    else accessUnboundedMemoryRange fees f l continue++accessMemoryWord+  :: FeeSchedule Word -> Word -> EVM () -> EVM ()+accessMemoryWord fees x = accessMemoryRange fees x 32++copyBytesToMemory+  :: Buffer -> Word -> Word -> Word -> EVM ()+copyBytesToMemory bs size xOffset yOffset =+  if size == 0 then noop+  else do+    mem <- use (state . memory)+    assign (state . memory) $+      writeMemory bs size xOffset yOffset mem++copyCallBytesToMemory+  :: Buffer -> Word -> Word -> Word -> EVM ()+copyCallBytesToMemory bs size xOffset yOffset =+  if size == 0 then noop+  else do+    mem <- use (state . memory)+    assign (state . memory) $+      writeMemory bs (min size (num (len bs))) xOffset yOffset mem++readMemory :: Word -> Word -> VM -> Buffer+readMemory offset size vm = sliceWithZero (num offset) (num size) (view (state . memory) vm)++word256At+  :: Functor f+  => Word -> (SymWord -> f (SymWord))+  -> Buffer -> f Buffer+word256At i = lens getter setter where+  getter = readMemoryWord i+  setter m x = setMemoryWord i x m++-- * Tracing++withTraceLocation+  :: (MonadState VM m) => TraceData -> m Trace+withTraceLocation x = do+  vm <- get+  let+    Just this =+      preview (env . contracts . ix (view (state . codeContract) vm)) vm+  pure Trace+    { _traceData = x+    , _traceCodehash = view codehash this+    , _traceOpIx = (view opIxMap this) Vector.! (view (state . pc) vm)+    }++pushTrace :: TraceData -> EVM ()+pushTrace x = do+  trace <- withTraceLocation x+  modifying traces $+    \t -> Zipper.children $ Zipper.insert (Node trace []) t++insertTrace :: TraceData -> EVM ()+insertTrace x = do+  trace <- withTraceLocation x+  modifying traces $+    \t -> Zipper.nextSpace $ Zipper.insert (Node trace []) t++popTrace :: EVM ()+popTrace =+  modifying traces $+    \t -> case Zipper.parent t of+            Nothing -> error "internal error (trace root)"+            Just t' -> Zipper.nextSpace t'++zipperRootForest :: Zipper.TreePos Zipper.Empty a -> Forest a+zipperRootForest z =+  case Zipper.parent z of+    Nothing -> Zipper.toForest z+    Just z' -> zipperRootForest (Zipper.nextSpace z')++traceForest :: VM -> Forest Trace+traceForest = view (traces . to zipperRootForest)++traceLog :: (MonadState VM m) => Log -> m ()+traceLog log = do+  trace <- withTraceLocation (EventTrace log)+  modifying traces $+    \t -> Zipper.nextSpace (Zipper.insert (Node trace []) t)++-- * Stack manipulation++push :: Word -> EVM ()+push = pushSym . w256lit . num++pushSym :: SymWord -> EVM ()+pushSym x = state . stack %= (x :)+++stackOp1+  :: (?op :: Word8)+  => ((SymWord) -> Word)+  -> ((SymWord) -> (SymWord))+  -> EVM ()+stackOp1 cost f =+  use (state . stack) >>= \case+    (x:xs) ->+      burn (cost x) $ do+        next+        let !y = f x+        state . stack .= y : xs+    _ ->+      underrun++stackOp2+  :: (?op :: Word8)+  => (((SymWord), (SymWord)) -> Word)+  -> (((SymWord), (SymWord)) -> (SymWord))+  -> EVM ()+stackOp2 cost f =+  use (state . stack) >>= \case+    (x:y:xs) ->+      burn (cost (x, y)) $ do+        next+        state . stack .= f (x, y) : xs+    _ ->+      underrun++stackOp3+  :: (?op :: Word8)+  => (((SymWord), (SymWord), (SymWord)) -> Word)+  -> (((SymWord), (SymWord), (SymWord)) -> (SymWord))+  -> EVM ()+stackOp3 cost f =+  use (state . stack) >>= \case+    (x:y:z:xs) ->+      burn (cost (x, y, z)) $ do+        next+        state . stack .= f (x, y, z) : xs+    _ ->+      underrun++-- * Bytecode data functions++checkJump :: (Integral n) => n -> [SymWord] -> EVM ()+checkJump x xs = do+  theCode <- use (state . code)+  self <- use (state . codeContract)+  theCodeOps <- use (env . contracts . ix self . codeOps)+  if x < num (BS.length theCode) && BS.index theCode (num x) == 0x5b+    then+      case RegularVector.find (\(i, op) -> i == num x && op == OpJumpdest) theCodeOps of+        Nothing ->  vmError BadJumpDestination+        _ -> do+             state . stack .= xs+             state . pc .= num x+    else vmError BadJumpDestination++opSize :: Word8 -> Int+opSize x | x >= 0x60 && x <= 0x7f = num x - 0x60 + 2+opSize _                          = 1++-- Index i of the resulting vector contains the operation index for+-- the program counter value i.  This is needed because source map+-- entries are per operation, not per byte.+mkOpIxMap :: ByteString -> Vector Int+mkOpIxMap xs = Vector.create $ Vector.new (BS.length xs) >>= \v ->+  -- Loop over the byte string accumulating a vector-mutating action.+  -- This is somewhat obfuscated, but should be fast.+  let (_, _, _, m) =+        BS.foldl' (go v) (0 :: Word8, 0, 0, return ()) xs+  in m >> return v+  where+    go v (0, !i, !j, !m) x | x >= 0x60 && x <= 0x7f =+      {- Start of PUSH op. -} (x - 0x60 + 1, i + 1, j,     m >> Vector.write v i j)+    go v (1, !i, !j, !m) _ =+      {- End of PUSH op. -}   (0,            i + 1, j + 1, m >> Vector.write v i j)+    go v (0, !i, !j, !m) _ =+      {- Other op. -}         (0,            i + 1, j + 1, m >> Vector.write v i j)+    go v (n, !i, !j, !m) _ =+      {- PUSH data. -}        (n - 1,        i + 1, j,     m >> Vector.write v i j)++vmOp :: VM -> Maybe Op+vmOp vm =+  let i  = vm ^. state . pc+      xs = BS.drop i (vm ^. state . code)+      op = BS.index xs 0+  in if BS.null xs+     then Nothing+     else Just (readOp op (BS.drop 1 xs))++vmOpIx :: VM -> Maybe Int+vmOpIx vm =+  do self <- currentContract vm+     (view opIxMap self) Vector.!? (view (state . pc) vm)++opParams :: VM -> Map String (SymWord)+opParams vm =+  case vmOp vm of+    Just OpCreate ->+      params $ words "value offset size"+    Just OpCall ->+      params $ words "gas to value in-offset in-size out-offset out-size"+    Just OpSstore ->+      params $ words "index value"+    Just OpCodecopy ->+      params $ words "mem-offset code-offset code-size"+    Just OpSha3 ->+      params $ words "offset size"+    Just OpCalldatacopy ->+      params $ words "to from size"+    Just OpExtcodecopy ->+      params $ words "account mem-offset code-offset code-size"+    Just OpReturn ->+      params $ words "offset size"+    Just OpJumpi ->+      params $ words "destination condition"+    _ -> mempty+  where+    params xs =+      if length (vm ^. state . stack) >= length xs+      then Map.fromList (zip xs (vm ^. state . stack))+      else mempty++readOp :: Word8 -> ByteString -> Op+readOp x _  | x >= 0x80 && x <= 0x8f = OpDup (x - 0x80 + 1)+readOp x _  | x >= 0x90 && x <= 0x9f = OpSwap (x - 0x90 + 1)+readOp x _  | x >= 0xa0 && x <= 0xa4 = OpLog (x - 0xa0)+readOp x xs | x >= 0x60 && x <= 0x7f =+  let n   = x - 0x60 + 1+      xs' = BS.take (num n) xs+  in OpPush (word xs')+readOp x _ = case x of+  0x00 -> OpStop+  0x01 -> OpAdd+  0x02 -> OpMul+  0x03 -> OpSub+  0x04 -> OpDiv+  0x05 -> OpSdiv+  0x06 -> OpMod+  0x07 -> OpSmod+  0x08 -> OpAddmod+  0x09 -> OpMulmod+  0x0a -> OpExp+  0x0b -> OpSignextend+  0x10 -> OpLt+  0x11 -> OpGt+  0x12 -> OpSlt+  0x13 -> OpSgt+  0x14 -> OpEq+  0x15 -> OpIszero+  0x16 -> OpAnd+  0x17 -> OpOr+  0x18 -> OpXor+  0x19 -> OpNot+  0x1a -> OpByte+  0x1b -> OpShl+  0x1c -> OpShr+  0x1d -> OpSar+  0x20 -> OpSha3+  0x30 -> OpAddress+  0x31 -> OpBalance+  0x32 -> OpOrigin+  0x33 -> OpCaller+  0x34 -> OpCallvalue+  0x35 -> OpCalldataload+  0x36 -> OpCalldatasize+  0x37 -> OpCalldatacopy+  0x38 -> OpCodesize+  0x39 -> OpCodecopy+  0x3a -> OpGasprice+  0x3b -> OpExtcodesize+  0x3c -> OpExtcodecopy+  0x3d -> OpReturndatasize+  0x3e -> OpReturndatacopy+  0x3f -> OpExtcodehash+  0x40 -> OpBlockhash+  0x41 -> OpCoinbase+  0x42 -> OpTimestamp+  0x43 -> OpNumber+  0x44 -> OpDifficulty+  0x45 -> OpGaslimit+  0x46 -> OpChainid+  0x47 -> OpSelfbalance+  0x50 -> OpPop+  0x51 -> OpMload+  0x52 -> OpMstore+  0x53 -> OpMstore8+  0x54 -> OpSload+  0x55 -> OpSstore+  0x56 -> OpJump+  0x57 -> OpJumpi+  0x58 -> OpPc+  0x59 -> OpMsize+  0x5a -> OpGas+  0x5b -> OpJumpdest+  0xf0 -> OpCreate+  0xf1 -> OpCall+  0xf2 -> OpCallcode+  0xf3 -> OpReturn+  0xf4 -> OpDelegatecall+  0xf5 -> OpCreate2+  0xfd -> OpRevert+  0xfa -> OpStaticcall+  0xff -> OpSelfdestruct+  _    -> OpUnknown x++mkCodeOps :: ByteString -> RegularVector.Vector (Int, Op)+mkCodeOps bytes = RegularVector.fromList . toList $ go 0 bytes+  where+    go !i !xs =+      case BS.uncons xs of+        Nothing ->+          mempty+        Just (x, xs') ->+          let j = opSize x+          in (i, readOp x xs') Seq.<| go (i + j) (BS.drop j xs)++-- * Gas cost calculation helpers++-- Gas cost function for CALL, transliterated from the Yellow Paper.+costOfCall+  :: FeeSchedule Word+  -> Bool -> Word -> Word -> Word+  -> (Word, Word)+costOfCall (FeeSchedule {..}) recipientExists xValue availableGas xGas =+  (c_gascap + c_extra, c_callgas)+  where+    c_extra =+      num g_call + c_xfer + c_new+    c_xfer =+      if xValue /= 0  then num g_callvalue              else 0+    c_callgas =+      if xValue /= 0  then c_gascap + num g_callstipend else c_gascap+    c_new =+      if not recipientExists && xValue /= 0+      then num g_newaccount+      else 0+    c_gascap =+      if availableGas >= c_extra+      then min xGas (allButOne64th (availableGas - c_extra))+      else xGas++-- Gas cost of create, including hash cost if needed+costOfCreate+  :: FeeSchedule Word+  -> Word -> Word -> (Word, Word)+costOfCreate (FeeSchedule {..}) availableGas hashSize =+  (createCost + initGas, initGas)+  where+    createCost = g_create + hashCost+    hashCost   = g_sha3word * ceilDiv (hashSize) 32+    initGas    = allButOne64th (availableGas - createCost)++-- Gas cost of precompiles+costOfPrecompile :: FeeSchedule Word -> Addr -> Buffer -> Word+costOfPrecompile (FeeSchedule {..}) precompileAddr input =+  case precompileAddr of+    -- ECRECOVER+    0x1 -> 3000+    -- SHA2-256+    0x2 -> num $ (((len input + 31) `div` 32) * 12) + 60+    -- RIPEMD-160+    0x3 -> num $ (((len input + 31) `div` 32) * 120) + 600+    -- IDENTITY+    0x4 -> num $ (((len input + 31) `div` 32) * 3) + 15+    -- MODEXP+    0x5 -> num $ (f (num (max lenm lenb)) * num (max lene' 1)) `div` (num g_quaddivisor)+      where input' = case input of+              SymbolicBuffer _ -> error "unsupported: symbolic MODEXP gas cost calc"+              ConcreteBuffer b -> b+            (lenb, lene, lenm) = parseModexpLength input'+            lene' | lene <= 32 && ez = 0+                  | lene <= 32 = num (log2 e')+                  | e' == 0 = 8 * (lene - 32)+                  | otherwise = num (log2 e') + 8 * (lene - 32)++            ez = isZero (96 + lenb) lene input'+            e' = w256 $ word $ LS.toStrict $+                   lazySlice (96 + lenb) (min 32 lene) input'++            f :: Integer -> Integer+            f x | x <= 64 = x * x+                | x <= 1024 = (x * x) `div` 4 + 96 * x - 3072+                | otherwise = (x * x) `div` 16 + 480 * x - 199680+    -- ECADD+    0x6 -> g_ecadd+    -- ECMUL+    0x7 -> g_ecmul+    -- ECPAIRING+    0x8 -> num $ ((len input) `div` 192) * (num g_pairing_point) + (num g_pairing_base)+    -- BLAKE2+    0x9 -> let input' = case input of+                         SymbolicBuffer _ -> error "unsupported: symbolic BLAKE2B gas cost calc"+                         ConcreteBuffer b -> b+           in g_fround * (num $ asInteger $ lazySlice 0 4 input')+    _ -> error ("unimplemented precompiled contract " ++ show precompileAddr)++-- Gas cost of memory expansion+memoryCost :: FeeSchedule Word -> Word -> Word+memoryCost FeeSchedule{..} byteCount =+  let+    wordCount = ceilDiv byteCount 32+    linearCost = g_memory * wordCount+    quadraticCost = div (wordCount * wordCount) 512+  in+    linearCost + quadraticCost++-- * Uninterpreted functions++symSHA256N :: SInteger -> SInteger -> SWord 256+symSHA256N = uninterpret "sha256"++symkeccakN :: SInteger -> SInteger -> SWord 256+symkeccakN = uninterpret "keccak"++toSInt :: [SWord 8] -> SInteger+toSInt bs = sum $ zipWith (\a i -> sFromIntegral a * 256 ^ i) bs [0..]++-- | Although we'd like to define this directly as an uninterpreted function,+-- we cannot because [a] is not a symbolic type. We must convert the list into a suitable+-- symbolic type first. The only important property of this conversion is that it is injective.+-- We embedd the bytestring as a pair of symbolic integers, this is a fairly easy solution.+symkeccak' :: [SWord 8] -> SWord 256+symkeccak' bytes = case length bytes of+  0 -> literal $ toSizzle $ keccak ""+  n -> symkeccakN (num n) (toSInt bytes)++symSHA256 :: [SWord 8] -> [SWord 8]+symSHA256 bytes = case length bytes of+  0 -> litBytes $ BS.pack $ BA.unpack $ (Crypto.hash BS.empty :: Digest SHA256)+  n -> toBytes $ symSHA256N (num n) (toSInt bytes)+  -- * Arithmetic 

@@ -25,9 +25,7 @@  -} -{-# Language DeriveAnyClass #-} {-# Language StrictData #-}-{-# Language TemplateHaskell #-}  module EVM.ABI   ( AbiValue (..)@@ -38,35 +36,47 @@   , putAbi   , getAbi   , getAbiSeq+  , genAbiValue   , abiValueType   , abiTypeSolidity   , abiCalldata+  , abiMethod+  , emptyAbi   , encodeAbiValue+  , decodeAbiValue   , parseTypeName+  , makeAbiValue+  , parseAbiValue+  , selector   ) where  import EVM.Keccak (abiKeccak)-import EVM.Types ()+import EVM.Types  import Control.Monad      (replicateM, replicateM_, forM_, void)-import Data.Binary.Get    (Get, label, getWord8, getWord32be, skip)+import Data.Binary.Get    (Get, runGet, label, getWord8, getWord32be, skip) import Data.Binary.Put    (Put, runPut, putWord8, putWord32be) import Data.Bits          (shiftL, shiftR, (.&.)) import Data.ByteString    (ByteString)-import Data.DoubleWord    (Word256, Int256, Word160, signedWord)+import Data.DoubleWord    (Word256, Int256, signedWord)+import Data.Functor       (($>)) import Data.Monoid        ((<>)) import Data.Text          (Text, pack) import Data.Text.Encoding (encodeUtf8) import Data.Vector        (Vector)-import Data.Word          (Word32, Word8)+import Data.Word          (Word32)+import Data.List          (intercalate) import GHC.Generics  import Test.QuickCheck hiding ((.&.), label)+import Text.ParserCombinators.ReadP+import Control.Applicative -import qualified Data.ByteString      as BS-import qualified Data.ByteString.Lazy as BSLazy-import qualified Data.Text            as Text-import qualified Data.Vector          as Vector+import qualified Data.ByteString       as BS+import qualified Data.ByteString.Char8 as Char8+import qualified Data.ByteString.Lazy  as BSLazy+import qualified Data.Text             as Text+import qualified Data.Vector           as Vector  import qualified Text.Megaparsec      as P import qualified Text.Megaparsec.Char as P@@ -74,15 +84,32 @@ data AbiValue   = AbiUInt         Int Word256   | AbiInt          Int Int256-  | AbiAddress      Word160+  | AbiAddress      Addr   | AbiBool         Bool   | AbiBytes        Int BS.ByteString   | AbiBytesDynamic BS.ByteString   | AbiString       BS.ByteString   | AbiArrayDynamic AbiType (Vector AbiValue)   | AbiArray        Int AbiType (Vector AbiValue)-  deriving (Show, Read, Eq, Ord, Generic)+  | AbiTuple        (Vector AbiValue)+  deriving (Read, Eq, Ord, Generic) +-- | Pretty-print some 'AbiValue'.+instance Show AbiValue where+  show (AbiUInt _ n)         = show n+  show (AbiInt  _ n)         = show n+  show (AbiAddress n)        = show n+  show (AbiBool b)           = if b then "true" else "false"+  show (AbiBytes      _ b)   = show (ByteStringS b)+  show (AbiBytesDynamic b)   = show (ByteStringS b)+  show (AbiString       s)   = show s+  show (AbiArrayDynamic _ v) =+    "[" ++ intercalate ", " (show <$> Vector.toList v) ++ "]"+  show (AbiArray      _ _ v) =+    "[" ++ intercalate ", " (show <$> Vector.toList v) ++ "]"+  show (AbiTuple v) =+    "(" ++ intercalate ", " (show <$> Vector.toList v) ++ ")"+ data AbiType   = AbiUIntType         Int   | AbiIntType          Int@@ -93,8 +120,12 @@   | AbiStringType   | AbiArrayDynamicType AbiType   | AbiArrayType        Int AbiType-  deriving (Show, Read, Eq, Ord, Generic)+  | AbiTupleType        (Vector AbiType)+  deriving (Read, Eq, Ord, Generic) +instance Show AbiType where+  show = Text.unpack . abiTypeSolidity+ data AbiKind = Dynamic | Static   deriving (Show, Read, Eq, Ord, Generic) @@ -111,6 +142,7 @@   AbiStringType         -> Dynamic   AbiArrayDynamicType _ -> Dynamic   AbiArrayType _ t      -> abiKind t+  AbiTupleType ts       -> if Dynamic `elem` (abiKind <$> ts) then Dynamic else Static   _                     -> Static  abiValueType :: AbiValue -> AbiType@@ -124,6 +156,7 @@   AbiString _         -> AbiStringType   AbiArrayDynamic t _ -> AbiArrayDynamicType t   AbiArray n t _      -> AbiArrayType n t+  AbiTuple v          -> AbiTupleType (abiValueType <$> v)  abiTypeSolidity :: AbiType -> Text abiTypeSolidity = \case@@ -136,6 +169,7 @@   AbiStringType         -> "string"   AbiArrayDynamicType t -> abiTypeSolidity t <> "[]"   AbiArrayType n t      -> abiTypeSolidity t <> "[" <> pack (show n) <> "]"+  AbiTupleType ts       -> "(" <> (Text.intercalate "," . Vector.toList $ abiTypeSolidity <$> ts) <> ")"  getAbi :: AbiType -> Get AbiValue getAbi t = label (Text.unpack (abiTypeSolidity t)) $@@ -169,11 +203,13 @@       AbiArrayDynamic t' <$>         label "array body" (getAbiSeq (fromIntegral n) (repeat t')) +    AbiTupleType ts ->+      AbiTuple <$> getAbiSeq (Vector.length ts) (Vector.toList ts)+ putAbi :: AbiValue -> Put putAbi = \case-  AbiUInt n x -> do-    let word32Count = div (roundTo256Bits n) 4-    forM_ (reverse [0 .. word32Count - 1]) $ \i ->+  AbiUInt _ x ->+    forM_ (reverse [0 .. 7]) $ \i ->       putWord32be (fromIntegral (shiftR x (i * 32) .&. 0xffffffff))    AbiInt n x   -> putAbi (AbiUInt n (fromIntegral x))@@ -182,7 +218,7 @@    AbiBytes n xs -> do     forM_ [0 .. n-1] (putWord8 . BS.index xs)-    replicateM_ (roundTo256Bits n - n) (putWord8 0)+    replicateM_ (roundTo32Bytes n - n) (putWord8 0)    AbiBytesDynamic xs -> do     let n = BS.length xs@@ -199,6 +235,9 @@     putAbi (AbiUInt 256 (fromIntegral (Vector.length xs)))     putAbiSeq xs +  AbiTuple v ->+    putAbiSeq v+ getAbiSeq :: Int -> [AbiType] -> Get (Vector AbiValue) getAbiSeq n ts = label "sequence" $ do   hs <- label "sequence head" (getAbiHead n ts)@@ -209,7 +248,7 @@   -> Get [Either AbiType AbiValue] getAbiHead 0 _      = pure [] getAbiHead _ []     = fail "ran out of types"-getAbiHead n (t:ts) = do+getAbiHead n (t:ts) =   case abiKind t of     Dynamic ->       (Left t :) <$> (skip 32 *> getAbiHead (n - 1) ts)@@ -227,17 +266,18 @@ abiValueSize :: AbiValue -> Int abiValueSize x =   case x of-    AbiUInt n _  -> roundTo256Bits n-    AbiInt  n _  -> roundTo256Bits n-    AbiBytes n _ -> roundTo256Bits n+    AbiUInt _ _  -> 32+    AbiInt  _ _  -> 32+    AbiBytes n _ -> roundTo32Bytes n     AbiAddress _ -> 32     AbiBool _    -> 32     AbiArray _ _ xs -> Vector.sum (Vector.map abiHeadSize xs) +                        Vector.sum (Vector.map abiTailSize xs)-    AbiBytesDynamic xs -> 32 + roundTo256Bits (BS.length xs)+    AbiBytesDynamic xs -> 32 + roundTo32Bytes (BS.length xs)     AbiArrayDynamic _ xs -> 32 + Vector.sum (Vector.map abiHeadSize xs) +                                 Vector.sum (Vector.map abiTailSize xs)-    AbiString s -> 32 + roundTo256Bits (BS.length s)+    AbiString s -> 32 + roundTo32Bytes (BS.length s)+    AbiTuple v  -> sum (abiValueSize <$> v)  abiTailSize :: AbiValue -> Int abiTailSize x =@@ -245,11 +285,15 @@     Static -> 0     Dynamic ->       case x of-        AbiString s -> 32 + roundTo256Bits (BS.length s)-        AbiBytesDynamic s -> 32 + roundTo256Bits (BS.length s)+        AbiString s -> 32 + roundTo32Bytes (BS.length s)+        AbiBytesDynamic s -> 32 + roundTo32Bytes (BS.length s)         AbiArrayDynamic _ xs -> 32 + Vector.sum (Vector.map abiValueSize xs)         AbiArray _ _ xs -> Vector.sum (Vector.map abiValueSize xs)+        AbiTuple v -> sum (headSize <$> v) + sum (abiTailSize <$> v)         _ -> error "impossible"+  where headSize y = if abiKind (abiValueType y) == Static+                     then abiValueSize y+                     else 32  abiHeadSize :: AbiValue -> Int abiHeadSize x =@@ -257,9 +301,9 @@     Dynamic -> 32     Static ->       case x of-        AbiUInt n _  -> roundTo256Bits n-        AbiInt  n _  -> roundTo256Bits n-        AbiBytes n _ -> roundTo256Bits n+        AbiUInt _ _  -> 32+        AbiInt  _ _  -> 32+        AbiBytes n _ -> roundTo32Bytes n         AbiAddress _ -> 32         AbiBool _    -> 32         AbiArray _ _ xs -> Vector.sum (Vector.map abiHeadSize xs) +@@ -267,6 +311,8 @@         AbiBytesDynamic _ -> 32         AbiArrayDynamic _ _ -> 32         AbiString _       -> 32+        AbiTuple v   -> sum (abiHeadSize <$> v) ++                        sum (abiTailSize <$> v)  putAbiSeq :: Vector AbiValue -> Put putAbiSeq xs =@@ -283,17 +329,28 @@ encodeAbiValue :: AbiValue -> BS.ByteString encodeAbiValue = BSLazy.toStrict . runPut . putAbi +decodeAbiValue :: AbiType -> BSLazy.ByteString -> AbiValue+decodeAbiValue = runGet . getAbi++selector :: Text -> BS.ByteString+selector s = BSLazy.toStrict . runPut $ putWord32be (abiKeccak (encodeUtf8 s))++abiMethod :: Text -> AbiValue -> BS.ByteString+abiMethod s args = BSLazy.toStrict . runPut $ do+  putWord32be (abiKeccak (encodeUtf8 s))+  putAbi args+ abiCalldata :: Text -> Vector AbiValue -> BS.ByteString abiCalldata s xs = BSLazy.toStrict . runPut $ do   putWord32be (abiKeccak (encodeUtf8 s))   putAbiSeq xs -parseTypeName :: Text -> Maybe AbiType-parseTypeName = P.parseMaybe typeWithArraySuffix+parseTypeName :: Vector AbiType -> Text -> Maybe AbiType+parseTypeName = P.parseMaybe . typeWithArraySuffix -typeWithArraySuffix :: P.Parsec () Text AbiType-typeWithArraySuffix = do-  base <- basicType+typeWithArraySuffix :: Vector AbiType -> P.Parsec () Text AbiType+typeWithArraySuffix v = do+  base <- basicType v   sizes <-     P.many $       P.between@@ -301,24 +358,25 @@         (P.many P.digitChar)    let-    parseSize :: AbiType -> [Char] -> AbiType+    parseSize :: AbiType -> String -> AbiType     parseSize t "" = AbiArrayDynamicType t     parseSize t s  = AbiArrayType (read s) t    pure (foldl parseSize base sizes) -basicType :: P.Parsec () Text AbiType-basicType =+basicType :: Vector AbiType -> P.Parsec () Text AbiType+basicType v =   P.choice-    [ P.string "address" *> pure AbiAddressType-    , P.string "bool"    *> pure AbiBoolType-    , P.string "string"  *> pure AbiStringType+    [ P.string "address" $> AbiAddressType+    , P.string "bool"    $> AbiBoolType+    , P.string "string"  $> AbiStringType      , sizedType "uint" AbiUIntType     , sizedType "int"  AbiIntType     , sizedType "bytes" AbiBytesType -    , P.string "bytes" *> pure AbiBytesDynamicType+    , P.string "bytes" $> AbiBytesDynamicType+    , P.string "tuple" $> AbiTupleType v     ]    where@@ -332,24 +390,22 @@   sum [ shiftL x ((n - i) * 32)       | (x, i) <- zip (map fromIntegral xs) [1..] ] -pack8 :: Int -> [Word8] -> Word256-pack8 n xs =-  sum [ shiftL x ((n - i) * 8)-      | (x, i) <- zip (map fromIntegral xs) [1..] ]- asUInt :: Integral i => Int -> (i -> a) -> Get a asUInt n f = (\(AbiUInt _ x) -> f (fromIntegral x)) <$> getAbi (AbiUIntType n)  getWord256 :: Get Word256 getWord256 = pack32 8 <$> replicateM 8 getWord32be -roundTo256Bits :: Integral a => a -> a-roundTo256Bits n = 32 * div (n + 255) 256+roundTo32Bytes :: Integral a => a -> a+roundTo32Bytes n = 32 * div (n + 31) 32 +emptyAbi :: AbiValue+emptyAbi = AbiTuple mempty+ getBytesWith256BitPadding :: Integral a => a -> Get ByteString getBytesWith256BitPadding i =   (BS.pack <$> replicateM n getWord8)-    <* skip ((roundTo256Bits n) - n)+    <* skip ((roundTo32Bytes n) - n)   where n = fromIntegral i  -- QuickCheck instances@@ -358,9 +414,9 @@ genAbiValue = \case    AbiUIntType n -> genUInt n    AbiIntType n ->-     do AbiUInt _ x <- genUInt n-        b <- arbitrary-        pure $ AbiInt n (signedWord x * if b then 1 else -1)+     do a <- genUInt n+        let AbiUInt _ x = a+        pure $ AbiInt n (signedWord x)    AbiAddressType ->      (\(AbiUInt _ x) -> AbiAddress (fromIntegral x)) <$> genUInt 20    AbiBoolType ->@@ -378,14 +434,13 @@    AbiArrayType n t ->      AbiArray n t . Vector.fromList <$>        replicateM n (scale (`div` 2) (genAbiValue t))+   AbiTupleType ts ->+     AbiTuple <$> mapM genAbiValue ts   where-    genUInt n =-       do x <- pack8 (div n 8) <$> replicateM n arbitrary-          pure . AbiUInt n $-            if n == 256 then x else mod x (2 ^ n)+    genUInt n = AbiUInt n <$> arbitraryIntegralWithMax n  instance Arbitrary AbiType where-  arbitrary = oneof+  arbitrary = sized $ \n -> oneof $ -- prevent empty tuples     [ (AbiUIntType . (* 8)) <$> choose (1, 32)     , (AbiIntType . (* 8)) <$> choose (1, 32)     , pure AbiAddressType@@ -397,7 +452,10 @@     , AbiArrayType         <$> (getPositive <$> arbitrary)         <*> scale (`div` 2) arbitrary-    ]+    ] <>+    [AbiTupleType+        <$> scale (`div` 2) (Vector.fromList <$> arbitrary)+        | n /= 0]  instance Arbitrary AbiValue where   arbitrary = arbitrary >>= genAbiValue@@ -406,8 +464,83 @@       Vector.toList v ++         map (AbiArrayDynamic t . Vector.fromList)             (shrinkList shrink (Vector.toList v))+    AbiBytesDynamic b -> AbiBytesDynamic . BS.pack <$> shrinkList shrinkIntegral (BS.unpack b)+    AbiString b -> AbiString . BS.pack <$> shrinkList shrinkIntegral (BS.unpack b)+    AbiBytes n a | n <= 32 -> shrink $ AbiUInt (n * 8) (word256 a)+    --bytesN for N > 32 don't really exist right now anyway..+    AbiBytes _ _ | otherwise -> []     AbiArray _ t v ->       Vector.toList v ++         map (\x -> AbiArray (length x) t (Vector.fromList x))             (shrinkList shrink (Vector.toList v))-    _ -> []+    AbiTuple v -> Vector.toList $ AbiTuple . Vector.fromList . shrink <$> v+    AbiUInt n a -> AbiUInt n <$> (shrinkIntegral a)+    AbiInt n a -> AbiInt n <$> (shrinkIntegral a)+    AbiBool b -> AbiBool <$> shrink b+    AbiAddress a -> [AbiAddress 0xacab, AbiAddress 0xdeadbeef, AbiAddress 0xbabeface]+      <> (AbiAddress <$> shrinkIntegral a)+++-- Bool synonym with custom read instance+-- to be able to parse lower case 'false' and 'true'+data Boolz = Boolz Bool++instance Read Boolz where+  readsPrec _ ('T':'r':'u':'e':x) = [(Boolz True, x)]+  readsPrec _ ('t':'r':'u':'e':x) = [(Boolz True, x)]+  readsPrec _ ('f':'a':'l':'s':'e':x) = [(Boolz False, x)]+  readsPrec _ ('F':'a':'l':'s':'e':x) = [(Boolz False, x)]+  readsPrec _ [] = []+  readsPrec n (_:t) = readsPrec n t++makeAbiValue :: AbiType -> String -> AbiValue+makeAbiValue typ str = case readP_to_S (parseAbiValue typ) str of+  [] -> error "could not parse abi arguments"+  ((val,_):_) -> val++parseAbiValue :: AbiType -> ReadP AbiValue+parseAbiValue (AbiUIntType n) = do W256 w256 <- readS_to_P reads+                                   return $ AbiUInt n w256+parseAbiValue (AbiIntType n) = do W256 w256 <- readS_to_P reads+                                  return $ AbiInt n (num w256)+parseAbiValue AbiAddressType = AbiAddress <$> readS_to_P reads+parseAbiValue AbiBoolType = (do W256 w256 <- readS_to_P reads+                                return $ AbiBool (w256 /= 0))+                            <|> (do Boolz b <- readS_to_P reads+                                    return $ AbiBool b)+parseAbiValue (AbiBytesType n) = AbiBytes n <$> do ByteStringS bytes <- readS_to_P reads+                                                   return bytes+parseAbiValue AbiBytesDynamicType = AbiBytesDynamic <$> do ByteStringS bytes <- readS_to_P reads+                                                           return bytes+parseAbiValue AbiStringType = AbiString <$> do Char8.pack <$> readS_to_P reads+parseAbiValue (AbiArrayDynamicType typ) =+  AbiArrayDynamic typ <$> do a <- listP (parseAbiValue typ)+                             return $ Vector.fromList a+parseAbiValue (AbiArrayType n typ) =+  AbiArray n typ <$> do a <- listP (parseAbiValue typ)+                        return $ Vector.fromList a+parseAbiValue (AbiTupleType _) = error "tuple types not supported"++listP :: ReadP a -> ReadP [a]+listP parser = between (char '[') (char ']') ((do skipSpaces+                                                  a <- parser+                                                  skipSpaces+                                                  return a) `sepBy` (char ','))+++-- A modification of 'arbitrarySizedBoundedIntegral' quickcheck library+-- which takes the maxbound explicitly rather than relying on a Bounded instance.+-- Essentially a mix between three types of generators:+-- one that strongly prefers values close to 0, one that prefers values close to max+-- and one that chooses uniformly.+arbitraryIntegralWithMax :: (Integral a) => Int -> Gen a+arbitraryIntegralWithMax maxbound =+  sized $ \s ->+    do let mn = 0 :: Int+           mx = maxbound+           bits n | n `quot` 2 == 0 = 0+                  | otherwise = 1 + bits (n `quot` 2)+           k  = 2^(s*(bits mn `max` bits mx `max` 40) `div` 100)+       smol <- choose (toInteger mn `max` (-k), toInteger mx `min` k)+       mid <- choose (0, maxbound)+       elements [fromIntegral smol, fromIntegral mid, fromIntegral (maxbound - (fromIntegral smol))]