{-# Language DataKinds #-}
{-# Language QuasiQuotes #-}

{- |
Module: EVM.Dev
Description: Helpers for repl driven hevm hacking
-}
module EVM.Dev where

import Data.ByteString hiding (writeFile, zip)
import Control.Monad.State.Strict hiding (state)
import Data.Maybe (fromJust)
import System.Directory
import Data.Typeable

import Data.String.Here
import qualified Data.Text.IO as T
import qualified Data.Text.Lazy.IO as TL

import EVM
import EVM.SMT
import EVM.Solvers
import EVM.Types
import EVM.Expr (numBranches, simplify)
import EVM.SymExec
import EVM.Solidity
import EVM.UnitTest
import EVM.Format (formatExpr)
import EVM.Dapp (dappInfo)
import GHC.Conc
import System.Exit (exitFailure)
import qualified EVM.Fetch as Fetch
import qualified EVM.FeeSchedule as FeeSchedule

checkEquiv :: (Typeable a) => Expr a -> Expr a -> IO ()
checkEquiv :: forall (a :: EType). Typeable a => Expr a -> Expr a -> IO ()
checkEquiv Expr a
a Expr a
b = forall a.
Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
withSolvers Solver
Z3 Natural
1 forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ \SolverGroup
s -> do
  let smt :: SMT2
smt = [Prop] -> SMT2
assertProps [Expr a
a forall (a :: EType). Typeable a => Expr a -> Expr a -> Prop
./= Expr a
b]
  CheckSatResult
res <- SolverGroup -> SMT2 -> IO CheckSatResult
checkSat SolverGroup
s SMT2
smt
  forall a. Show a => a -> IO ()
print CheckSatResult
res

runDappTest :: FilePath -> IO ()
runDappTest :: String -> IO ()
runDappTest String
root =
  forall a. String -> IO a -> IO a
withCurrentDirectory String
root forall a b. (a -> b) -> a -> b
$ do
    Natural
cores <- forall a b. (Integral a, Num b) => a -> b
num forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO Int
getNumProcessors
    let testFile :: String
testFile = String
root forall a. Semigroup a => a -> a -> a
<> String
"/out/dapp.sol.json"
    forall a.
Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
withSolvers Solver
Z3 Natural
cores forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ \SolverGroup
solvers -> do
      UnitTestOptions
opts <- SolverGroup -> String -> String -> IO UnitTestOptions
testOpts SolverGroup
solvers String
root String
testFile
      Bool
res <- UnitTestOptions -> String -> Maybe String -> IO Bool
dappTest UnitTestOptions
opts String
testFile forall a. Maybe a
Nothing
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
res forall a. IO a
exitFailure

testOpts :: SolverGroup -> FilePath -> FilePath -> IO UnitTestOptions
testOpts :: SolverGroup -> String -> String -> IO UnitTestOptions
testOpts SolverGroup
solvers String
root String
testFile = do
  DappInfo
srcInfo <- String -> IO (Maybe (Map Text SolcContract, SourceCache))
readSolc String
testFile forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe (Map Text SolcContract, SourceCache)
Nothing -> forall a. HasCallStack => String -> a
error String
"Could not read .sol.json file"
    Just (Map Text SolcContract
contractMap, SourceCache
sourceCache) ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ String -> Map Text SolcContract -> SourceCache -> DappInfo
dappInfo String
root Map Text SolcContract
contractMap SourceCache
sourceCache

  TestVMParams
params <- Maybe Text -> IO TestVMParams
getParametersFromEnvironmentVariables forall a. Maybe a
Nothing
  forall (f :: * -> *) a. Applicative f => a -> f a
pure EVM.UnitTest.UnitTestOptions
    { $sel:solvers:UnitTestOptions :: SolverGroup
EVM.UnitTest.solvers = SolverGroup
solvers
    , $sel:rpcInfo:UnitTestOptions :: RpcInfo
EVM.UnitTest.rpcInfo = forall a. Maybe a
Nothing
    , $sel:maxIter:UnitTestOptions :: Maybe Integer
EVM.UnitTest.maxIter = forall a. Maybe a
Nothing
    , $sel:askSmtIters:UnitTestOptions :: Maybe Integer
EVM.UnitTest.askSmtIters = forall a. Maybe a
Nothing
    , $sel:smtTimeout:UnitTestOptions :: Maybe Natural
EVM.UnitTest.smtTimeout = forall a. Maybe a
Nothing
    , $sel:smtDebug:UnitTestOptions :: Bool
EVM.UnitTest.smtDebug = Bool
False
    , $sel:solver:UnitTestOptions :: Maybe Text
EVM.UnitTest.solver = forall a. Maybe a
Nothing
    , $sel:covMatch:UnitTestOptions :: Maybe Text
EVM.UnitTest.covMatch = forall a. Maybe a
Nothing
    , $sel:verbose:UnitTestOptions :: Maybe Int
EVM.UnitTest.verbose = forall a. Maybe a
Nothing
    , $sel:match:UnitTestOptions :: Text
EVM.UnitTest.match = Text
".*"
    , $sel:maxDepth:UnitTestOptions :: Maybe Int
EVM.UnitTest.maxDepth = forall a. Maybe a
Nothing
    , $sel:fuzzRuns:UnitTestOptions :: Int
EVM.UnitTest.fuzzRuns = Int
100
    , $sel:replay:UnitTestOptions :: Maybe (Text, ByteString)
EVM.UnitTest.replay = forall a. Maybe a
Nothing
    , $sel:vmModifier:UnitTestOptions :: VM -> VM
EVM.UnitTest.vmModifier = forall a. a -> a
id
    , $sel:testParams:UnitTestOptions :: TestVMParams
EVM.UnitTest.testParams = TestVMParams
params
    , $sel:dapp:UnitTestOptions :: DappInfo
EVM.UnitTest.dapp = DappInfo
srcInfo
    , $sel:ffiAllowed:UnitTestOptions :: Bool
EVM.UnitTest.ffiAllowed = Bool
True
    }

doTest :: IO ()
doTest :: IO ()
doTest = do
  ByteString
c <- IO ByteString
testContract
  Bool -> ByteString -> IO ()
reachable' Bool
False ByteString
c
  --e <- simplify <$> buildExpr c
  --Prelude.putStrLn (formatExpr e)

analyzeDai :: IO ()
analyzeDai :: IO ()
analyzeDai = do
  ByteString
d <- IO ByteString
dai
  Bool -> ByteString -> IO ()
reachable' Bool
False ByteString
d

daiExpr :: IO (Expr End)
daiExpr :: IO (Expr 'End)
daiExpr = do
  ByteString
d <- IO ByteString
dai
  forall a.
Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
withSolvers Solver
Z3 Natural
1 forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ \SolverGroup
s -> SolverGroup -> ByteString -> IO (Expr 'End)
buildExpr SolverGroup
s ByteString
d

analyzeVat :: IO ()
analyzeVat :: IO ()
analyzeVat = do
  String -> IO ()
putStrLn String
"starting"
  ByteString
v <- IO ByteString
vat
  forall a.
Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
withSolvers Solver
Z3 Natural
1 forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ \SolverGroup
s -> do
    Expr 'End
e <- SolverGroup -> ByteString -> IO (Expr 'End)
buildExpr SolverGroup
s ByteString
v
    String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"done (" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show (Expr 'End -> Int
numBranches Expr 'End
e) forall a. Semigroup a => a -> a -> a
<> String
" branches)"
    Bool -> ByteString -> IO ()
reachable' Bool
False ByteString
v

analyzeDeposit :: IO ()
analyzeDeposit :: IO ()
analyzeDeposit = do
  Just ByteString
c <- Text -> Text -> IO (Maybe ByteString)
solcRuntime Text
"Deposit"
    [i|
    contract Deposit {
      function deposit(uint256 deposit_count) external pure {
        require(deposit_count < 2**32 - 1);
        ++deposit_count;
        bool found = false;
        for (uint height = 0; height < 32; height++) {
          if ((deposit_count & 1) == 1) {
            found = true;
            break;
          }
         deposit_count = deposit_count >> 1;
         }
        assert(found);
      }
     }
    |]
  forall a.
Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
withSolvers Solver
Z3 Natural
1 forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ \SolverGroup
s -> do
    String -> IO ()
putStrLn String
"Exploring Contract"
    Expr 'End
e <- forall (a :: EType). Expr a -> Expr a
simplify forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SolverGroup -> ByteString -> IO (Expr 'End)
buildExpr SolverGroup
s ByteString
c
    String -> IO ()
putStrLn String
"Writing AST"
    String -> Text -> IO ()
T.writeFile String
"full.ast" (forall (a :: EType). Expr a -> Text
formatExpr Expr 'End
e)


reachable' :: Bool -> ByteString -> IO ()
reachable' :: Bool -> ByteString -> IO ()
reachable' Bool
smtdebug ByteString
c = do
  String -> IO ()
putStrLn String
"Exploring contract"
  forall a.
Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
withSolvers Solver
Z3 Natural
4 forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ \SolverGroup
s -> do
    Expr 'End
full <- forall (a :: EType). Expr a -> Expr a
simplify forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SolverGroup -> ByteString -> IO (Expr 'End)
buildExpr SolverGroup
s ByteString
c
    String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Explored contract (" forall a. Semigroup a => a -> a -> a
<> (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Expr 'End -> Int
numBranches Expr 'End
full) forall a. Semigroup a => a -> a -> a
<> String
" branches)"
    --putStrLn $ formatExpr full
    String -> Text -> IO ()
T.writeFile String
"full.ast" forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> Text
formatExpr Expr 'End
full
    String -> IO ()
putStrLn String
"Dumped to full.ast"
    String -> IO ()
putStrLn String
"Checking reachability"
    ([SMT2]
qs, Expr 'End
less) <- SolverGroup -> Expr 'End -> IO ([SMT2], Expr 'End)
reachable SolverGroup
s Expr 'End
full
    String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Checked reachability (" forall a. Semigroup a => a -> a -> a
<> (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Expr 'End -> Int
numBranches Expr 'End
less) forall a. Semigroup a => a -> a -> a
<> String
" reachable branches)"
    String -> Text -> IO ()
T.writeFile String
"reachable.ast" forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> Text
formatExpr Expr 'End
less
    String -> IO ()
putStrLn String
"Dumped to reachable.ast"
    --putStrLn $ formatExpr less
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
smtdebug forall a b. (a -> b) -> a -> b
$ do
      String -> IO ()
putStrLn String
"\n\nQueries\n\n"
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [SMT2]
qs forall a b. (a -> b) -> a -> b
$ \SMT2
q -> do
        String -> IO ()
putStrLn String
"\n\n-- Query --"
        Text -> IO ()
TL.putStrLn forall a b. (a -> b) -> a -> b
$ SMT2 -> Text
formatSMT2 SMT2
q


showExpr :: ByteString -> IO ()
showExpr :: ByteString -> IO ()
showExpr ByteString
c = do
  forall a.
Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a
withSolvers Solver
Z3 Natural
1 forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ \SolverGroup
s -> do
    Expr 'End
e <- SolverGroup -> ByteString -> IO (Expr 'End)
buildExpr SolverGroup
s ByteString
c
    Text -> IO ()
T.putStrLn forall a b. (a -> b) -> a -> b
$ forall (a :: EType). Expr a -> Text
formatExpr (forall (a :: EType). Expr a -> Expr a
simplify Expr 'End
e)

summaryStore :: IO ByteString
summaryStore :: IO ByteString
summaryStore = do
  let src :: Text
src =
        [i|
          contract A {
            uint x;
            function f(uint256 y) public {
               unchecked {
                 x += y;
                 x += y;
               }
            }
          }
        |]
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. HasCallStack => Maybe a -> a
fromJust (Text -> Text -> IO (Maybe ByteString)
solcRuntime Text
"A" Text
src)

safeAdd :: IO ByteString
safeAdd :: IO ByteString
safeAdd = do
  let src :: Text
src =
        [i|
          contract SafeAdd {
            function add(uint x, uint y) public pure returns (uint z) {
                 require((z = x + y) >= x);
            }
          }
        |]
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. HasCallStack => Maybe a -> a
fromJust (Text -> Text -> IO (Maybe ByteString)
solcRuntime Text
"SafeAdd" Text
src)



testContract :: IO ByteString
testContract :: IO ByteString
testContract = do
  let src :: Text
src =
        [i|
          contract C {
            uint x;
            function set(uint v) public {
              x = v + v;
            }
          }
          |]
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. HasCallStack => Maybe a -> a
fromJust (Text -> Text -> IO (Maybe ByteString)
solcRuntime Text
"C" Text
src)

vat :: IO ByteString
vat :: IO ByteString
vat = do
  let src :: Text
src =
        [i|
          /// vat.sol -- Dai CDP database

          // Copyright (C) 2018 Rain <rainbreak@riseup.net>
          //
          // This program is free software: you can redistribute it and/or modify
          // it under the terms of the GNU Affero General Public License as published by
          // the Free Software Foundation, either version 3 of the License, or
          // (at your option) any later version.
          //
          // This program is distributed in the hope that it will be useful,
          // but WITHOUT ANY WARRANTY; without even the implied warranty of
          // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
          // GNU Affero General Public License for more details.
          //
          // You should have received a copy of the GNU Affero General Public License
          // along with this program.  If not, see <https://www.gnu.org/licenses/>.

          // FIXME: This contract was altered compared to the production version.
          // It doesn't use LibNote anymore.
          // New deployments of this contract will need to include custom events (TO DO).

          contract Vat {
              // --- Auth ---
              mapping (address => uint) public wards;
              function rely(address usr) external auth { require(live == 1, "Vat/not-live"); wards[usr] = 1; }
              function deny(address usr) external auth { require(live == 1, "Vat/not-live"); wards[usr] = 0; }
              modifier auth {
                  require(wards[msg.sender] == 1, "Vat/not-authorized");
                  _;
              }

              mapping(address => mapping (address => uint)) public can;
              function hope(address usr) external { can[msg.sender][usr] = 1; }
              function nope(address usr) external { can[msg.sender][usr] = 0; }
              function wish(address bit, address usr) internal view returns (bool) {
                  return either(bit == usr, can[bit][usr] == 1);
              }

              // --- Data ---
              struct Ilk {
                  uint256 Art;   // Total Normalised Debt     [wad]
                  uint256 rate;  // Accumulated Rates         [ray]
                  uint256 spot;  // Price with Safety Margin  [ray]
                  uint256 line;  // Debt Ceiling              [rad]
                  uint256 dust;  // Urn Debt Floor            [rad]
              }
              struct Urn {
                  uint256 ink;   // Locked Collateral  [wad]
                  uint256 art;   // Normalised Debt    [wad]
              }

              mapping (bytes32 => Ilk)                       public ilks;
              mapping (bytes32 => mapping (address => Urn )) public urns;
              mapping (bytes32 => mapping (address => uint)) public gem;  // [wad]
              mapping (address => uint256)                   public dai;  // [rad]
              mapping (address => uint256)                   public sin;  // [rad]

              uint256 public debt;  // Total Dai Issued    [rad]
              uint256 public vice;  // Total Unbacked Dai  [rad]
              uint256 public Line;  // Total Debt Ceiling  [rad]
              uint256 public live;  // Active Flag

              // --- Init ---
              constructor() public {
                  wards[msg.sender] = 1;
                  live = 1;
              }

              // --- Math ---
              function _add(uint x, int y) internal pure returns (uint z) {
                  z = x + uint(y);
                  require(y >= 0 || z <= x);
                  require(y <= 0 || z >= x);
              }
              function _sub(uint x, int y) internal pure returns (uint z) {
                  z = x - uint(y);
                  require(y <= 0 || z <= x);
                  require(y >= 0 || z >= x);
              }
              function _mul(uint x, int y) internal pure returns (int z) {
                  z = int(x) * y;
                  require(int(x) >= 0);
                  require(y == 0 || z / y == int(x));
              }
              function _add(uint x, uint y) internal pure returns (uint z) {
                  require((z = x + y) >= x);
              }
              function _sub(uint x, uint y) internal pure returns (uint z) {
                  require((z = x - y) <= x);
              }
              function _mul(uint x, uint y) internal pure returns (uint z) {
                  require(y == 0 || (z = x * y) / y == x);
              }

              // --- Administration ---
              function init(bytes32 ilk) external auth {
                  require(ilks[ilk].rate == 0, "Vat/ilk-already-init");
                  ilks[ilk].rate = 10 ** 27;
              }
              function file(bytes32 what, uint data) external auth {
                  require(live == 1, "Vat/not-live");
                  if (what == "Line") Line = data;
                  else revert("Vat/file-unrecognized-param");
              }
              function file(bytes32 ilk, bytes32 what, uint data) external auth {
                  require(live == 1, "Vat/not-live");
                  if (what == "spot") ilks[ilk].spot = data;
                  else if (what == "line") ilks[ilk].line = data;
                  else if (what == "dust") ilks[ilk].dust = data;
                  else revert("Vat/file-unrecognized-param");
              }
              function cage() external auth {
                  live = 0;
              }

              // --- Fungibility ---
              function slip(bytes32 ilk, address usr, int256 wad) external auth {
                  gem[ilk][usr] = _add(gem[ilk][usr], wad);
              }
              function flux(bytes32 ilk, address src, address dst, uint256 wad) external {
                  require(wish(src, msg.sender), "Vat/not-allowed");
                  gem[ilk][src] = _sub(gem[ilk][src], wad);
                  gem[ilk][dst] = _add(gem[ilk][dst], wad);
              }
              function move(address src, address dst, uint256 rad) external {
                  require(wish(src, msg.sender), "Vat/not-allowed");
                  dai[src] = _sub(dai[src], rad);
                  dai[dst] = _add(dai[dst], rad);
              }

              function either(bool x, bool y) internal pure returns (bool z) {
                  assembly{ z := or(x, y)}
              }
              function both(bool x, bool y) internal pure returns (bool z) {
                  assembly{ z := and(x, y)}
              }

              // --- CDP Confiscation ---
              function grab(bytes32 i, address u, address v, address w, int dink, int dart) external auth {
                  Urn storage urn = urns[i][u];
                  Ilk storage ilk = ilks[i];

                  urn.ink = _add(urn.ink, dink);
                  urn.art = _add(urn.art, dart);
                  ilk.Art = _add(ilk.Art, dart);

                  int dtab = _mul(ilk.rate, dart);

                  gem[i][v] = _sub(gem[i][v], dink);
                  sin[w]    = _sub(sin[w],    dtab);
                  vice      = _sub(vice,      dtab);
              }
          }
          |]
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. HasCallStack => Maybe a -> a
fromJust (Text -> Text -> IO (Maybe ByteString)
solcRuntime Text
"Vat" Text
src)

initVm :: ByteString -> VM
initVm :: ByteString -> VM
initVm ByteString
bs = VM
vm
  where
    contractCode :: ContractCode
contractCode = RuntimeCode -> ContractCode
RuntimeCode (ByteString -> RuntimeCode
ConcreteRuntimeCode ByteString
bs)
    c :: Contract
c = Contract
      { $sel:_contractcode:Contract :: ContractCode
_contractcode = ContractCode
contractCode
      , $sel:_balance:Contract :: W256
_balance      = W256
0
      , $sel:_nonce:Contract :: W256
_nonce        = W256
0
      , $sel:_codehash:Contract :: Expr 'EWord
_codehash     = Expr 'Buf -> Expr 'EWord
keccak (ByteString -> Expr 'Buf
ConcreteBuf ByteString
bs)
      , $sel:_opIxMap:Contract :: Vector Int
_opIxMap      = ContractCode -> Vector Int
mkOpIxMap ContractCode
contractCode
      , $sel:_codeOps:Contract :: Vector (Int, Op)
_codeOps      = ContractCode -> Vector (Int, Op)
mkCodeOps ContractCode
contractCode
      , $sel:_external:Contract :: Bool
_external     = Bool
False
      }
    vm :: VM
vm = VMOpts -> VM
makeVm forall a b. (a -> b) -> a -> b
$ VMOpts
      { $sel:vmoptContract:VMOpts :: Contract
EVM.vmoptContract      = Contract
c
      , $sel:vmoptCalldata:VMOpts :: (Expr 'Buf, [Prop])
EVM.vmoptCalldata      = (Text -> Expr 'Buf
AbstractBuf Text
"txdata", [])
      , $sel:vmoptValue:VMOpts :: Expr 'EWord
EVM.vmoptValue         = Int -> Expr 'EWord
CallValue Int
0
      , $sel:vmoptAddress:VMOpts :: Addr
EVM.vmoptAddress       = Word160 -> Addr
Addr Word160
0xffffffffffffffff
      , $sel:vmoptCaller:VMOpts :: Expr 'EWord
EVM.vmoptCaller        = W256 -> Expr 'EWord
Lit W256
0
      , $sel:vmoptOrigin:VMOpts :: Addr
EVM.vmoptOrigin        = Word160 -> Addr
Addr Word160
0xffffffffffffffff
      , $sel:vmoptGas:VMOpts :: Word64
EVM.vmoptGas           = Word64
0xffffffffffffffff
      , $sel:vmoptGaslimit:VMOpts :: Word64
EVM.vmoptGaslimit      = Word64
0xffffffffffffffff
      , $sel:vmoptStorageBase:VMOpts :: StorageBase
EVM.vmoptStorageBase   = StorageBase
Symbolic
      , $sel:vmoptBaseFee:VMOpts :: W256
EVM.vmoptBaseFee       = W256
0
      , $sel:vmoptPriorityFee:VMOpts :: W256
EVM.vmoptPriorityFee   = W256
0
      , $sel:vmoptCoinbase:VMOpts :: Addr
EVM.vmoptCoinbase      = Addr
0
      , $sel:vmoptNumber:VMOpts :: W256
EVM.vmoptNumber        = W256
0
      , $sel:vmoptTimestamp:VMOpts :: Expr 'EWord
EVM.vmoptTimestamp     = Text -> Expr 'EWord
Var Text
"timestamp"
      , $sel:vmoptBlockGaslimit:VMOpts :: Word64
EVM.vmoptBlockGaslimit = Word64
0
      , $sel:vmoptGasprice:VMOpts :: W256
EVM.vmoptGasprice      = W256
0
      , $sel:vmoptMaxCodeSize:VMOpts :: W256
EVM.vmoptMaxCodeSize   = W256
0xffffffff
      , $sel:vmoptPrevRandao:VMOpts :: W256
EVM.vmoptPrevRandao    = W256
420
      , $sel:vmoptSchedule:VMOpts :: FeeSchedule Word64
EVM.vmoptSchedule      = forall n. Num n => FeeSchedule n
FeeSchedule.berlin
      , $sel:vmoptChainId:VMOpts :: W256
EVM.vmoptChainId       = W256
1
      , $sel:vmoptCreate:VMOpts :: Bool
EVM.vmoptCreate        = Bool
False
      , $sel:vmoptTxAccessList:VMOpts :: Map Addr [W256]
EVM.vmoptTxAccessList  = forall a. Monoid a => a
mempty
      , $sel:vmoptAllowFFI:VMOpts :: Bool
EVM.vmoptAllowFFI      = Bool
False
      }


-- | Builds the Expr for the given evm bytecode object
buildExpr :: SolverGroup -> ByteString -> IO (Expr End)
buildExpr :: SolverGroup -> ByteString -> IO (Expr 'End)
buildExpr SolverGroup
solvers ByteString
bs = forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Fetcher
-> Maybe Integer
-> Maybe Integer
-> Stepper (Expr 'End)
-> StateT VM IO (Expr 'End)
interpret (SolverGroup -> RpcInfo -> Fetcher
Fetch.oracle SolverGroup
solvers forall a. Maybe a
Nothing) forall a. Maybe a
Nothing forall a. Maybe a
Nothing Stepper (Expr 'End)
runExpr) (ByteString -> VM
initVm ByteString
bs)

dai :: IO ByteString
dai :: IO ByteString
dai = do
  let src :: Text
src =
        [i|
        contract Dai {
            // --- Auth ---
            mapping (address => uint) public wards;
            function rely(address guy) external auth { wards[guy] = 1; }
            function deny(address guy) external auth { wards[guy] = 0; }
            modifier auth {
                require(wards[msg.sender] == 1, "Dai/not-authorized");
                _;
            }

            // --- ERC20 Data ---
            string  public constant name     = "Dai Stablecoin";
            string  public constant symbol   = "DAI";
            string  public constant version  = "1";
            uint8   public constant decimals = 18;
            uint256 public totalSupply;

            mapping (address => uint)                      public balanceOf;
            mapping (address => mapping (address => uint)) public allowance;

            event Approval(address indexed src, address indexed guy, uint wad);
            event Transfer(address indexed src, address indexed dst, uint wad);

            // --- Math ---
            function add(uint x, uint y) internal pure returns (uint z) {
                require((z = x + y) >= x);
            }
            function sub(uint x, uint y) internal pure returns (uint z) {
                require((z = x - y) <= x);
            }

            // --- EIP712 niceties ---
            constructor() public {
                wards[msg.sender] = 1;
            }

            // --- Token ---
            function transfer(address dst, uint wad) external returns (bool) {
                return transferFrom(msg.sender, dst, wad);
            }
            function transferFrom(address src, address dst, uint wad)
                public returns (bool)
            {
                require(balanceOf[src] >= wad, "Dai/insufficient-balance");
                if (src != msg.sender && allowance[src][msg.sender] != type(uint).max) {
                    require(allowance[src][msg.sender] >= wad, "Dai/insufficient-allowance");
                    allowance[src][msg.sender] = sub(allowance[src][msg.sender], wad);
                }
                balanceOf[src] = sub(balanceOf[src], wad);
                balanceOf[dst] = add(balanceOf[dst], wad);
                emit Transfer(src, dst, wad);
                return true;
            }
            function mint(address usr, uint wad) external auth {
                balanceOf[usr] = add(balanceOf[usr], wad);
                totalSupply    = add(totalSupply, wad);
                emit Transfer(address(0), usr, wad);
            }
            function burn(address usr, uint wad) external {
                require(balanceOf[usr] >= wad, "Dai/insufficient-balance");
                if (usr != msg.sender && allowance[usr][msg.sender] != type(uint).max) {
                    require(allowance[usr][msg.sender] >= wad, "Dai/insufficient-allowance");
                    allowance[usr][msg.sender] = sub(allowance[usr][msg.sender], wad);
                }
                balanceOf[usr] = sub(balanceOf[usr], wad);
                totalSupply    = sub(totalSupply, wad);
                emit Transfer(usr, address(0), wad);
            }
            function approve(address usr, uint wad) external returns (bool) {
                allowance[msg.sender][usr] = wad;
                emit Approval(msg.sender, usr, wad);
                return true;
            }

            // --- Alias ---
            function push(address usr, uint wad) external {
                transferFrom(msg.sender, usr, wad);
            }
            function pull(address usr, uint wad) external {
                transferFrom(usr, msg.sender, wad);
            }
            function move(address src, address dst, uint wad) external {
                transferFrom(src, dst, wad);
            }
        }
        |]
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. HasCallStack => Maybe a -> a
fromJust (Text -> Text -> IO (Maybe ByteString)
solcRuntime Text
"Dai" Text
src)