fix compiler errors

evm/open-games-hevm.cabal

@@ -1,6 +1,6 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.36.0.
+-- This file has been generated from package.yaml by hpack version 0.37.0.
 --
 -- see: https://github.com/sol/hpack
 

evm/src/EVM/TH.hs

@@ -9,7 +9,8 @@
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE TypeFamilies #-}
 
-module EVM.TH (sendAndRun, sendAndRunAll, sendAndRun', makeTxCall, balance, loadAll, ContractInfo (..), AbiValue (..), Expr (..), stToIO, setupAddresses, getAllContracts) where
+module EVM.TH (sendAndRun, sendAndRunAll, sendAndRun', makeTxCall, balance, loadAll
+              , ContractFileInfo(..), ContractInfo (..), AbiValue (..), Expr (..), stToIO, setupAddresses, getAllContracts) where
 
 import Control.Monad.ST
 import Control.Monad.Trans.State.Strict
@@ -18,6 +19,7 @@ import Data.ByteString (ByteString)
 import Data.Map as Map
 import Data.Text (Text, intercalate, pack, toLower, unpack)
 import Data.Text.IO (readFile)
+import Data.Maybe (fromJust)
 import qualified Data.Tree.Zipper as Zipper
 import Data.Vector as Vector (fromList)
 import EVM (blankState, emptyContract, exec1, initialContract, loadContract, resetState)
@@ -26,7 +28,7 @@ import EVM.Expr
 import EVM.FeeSchedule
 import EVM.Fetch
 import EVM.Prelude
-import EVM.Solidity (Contracts (..), Method (..), SolcContract (..), readStdJSON, solcRuntime, solidity')
+import EVM.Solidity (Contracts (..), Method (..), SolcContract (..), readStdJSON, solcRuntime, solidity, solc, Language(..))
 import EVM.Stepper
 import EVM.Transaction (initTx)
 import EVM.Types
@@ -46,7 +48,7 @@ makeCallData :: EthTransaction -> Expr Buf
 makeCallData (EthTransaction _ caller method args _ _) =
   ConcreteBuf $ abiMethod method (AbiTuple (Vector.fromList args))
 
-makeTxCall :: EthTransaction -> EVM s ()
+makeTxCall :: EthTransaction -> EVM Concrete s ()
 makeTxCall tx@(EthTransaction addr caller meth args amt gas) = do
   resetState
   assign (#tx % #isCreate) False
@@ -57,7 +59,7 @@ makeTxCall tx@(EthTransaction addr caller meth args amt gas) = do
   assign (#state % #gas) gas
   modify initTx
 
-loadIntoVM :: [(Expr EAddr, ByteString)] -> ST s (VM s)
+loadIntoVM :: [(Expr EAddr, ByteString)] -> ST s (VM Concrete s)
 loadIntoVM contracts = do
   blankSt <- blankState
   pure $
@@ -74,11 +76,11 @@ loadIntoVM contracts = do
         burned = 0,
         iterations = mempty,
         constraints = [],
-        keccakEqs = [],
         config =
           RuntimeConfig
             True
             Nothing
+            False
             EmptyBase
       }
   where
@@ -104,7 +106,7 @@ loadIntoVM contracts = do
           origin = LitAddr 0,
           toAddr = LitAddr 0,
           value = Lit 0,
-          substate = emptySubState,
+          subState = emptySubState,
           isCreate = True,
           txReversion = mempty
         }
@@ -146,16 +148,18 @@ constructorExprForType (AbiArrayType size ty) = error "arrays unsuppported"
 constructorExprForType (AbiTupleType types) = error "tuples unsupported" -- ConE (mkName "AbiTuple") [] [VarP (mkName name)]
 constructorExprForType (AbiFunctionType) = error "functions unsupported"
 
-data ContractInfo = ContractInfo
+data ContractInfo = ContractInfo { name :: Text, boundName :: Text }
+
+
+data ContractFileInfo = ContractFileInfo
   { file :: Text,
-    name :: Text,
-    boundName :: Text
+    modules :: [ContractInfo]
   }
 
 pat = VarP . mkName
 
 generateTxFactory :: Method -> Integer -> Text -> Q Dec
-generateTxFactory (Method _ args name sig _) addr boundName = do
+generateTxFactory (Method _ args name sig _) addr contractName = do
   runIO $ print ("arguments for method " <> name <> ":" <> pack (show args))
   let signatureString :: Q Exp = pure $ LitE $ StringL $ unpack sig
   let argExp :: Q Exp = pure $ ListE $ fmap (\(nm, ty) -> constructorExprForType ty (mkName $ unpack nm)) args
@@ -173,7 +177,7 @@ generateTxFactory (Method _ args name sig _) addr boundName = do
       |]
   pure $
     FunD
-      (mkName (unpack (toLower boundName <> "_" <> name)))
+      (mkName (unpack (toLower contractName <> "_" <> name)))
       [ Clause
           ( [pat "src", pat "amt", pat "gas"]
               ++ patterns
@@ -188,74 +192,84 @@ instance Lift (Addr) where
 instance Lift (Expr 'EAddr) where
   lift (LitAddr a) = [e|LitAddr (fromInteger a)|]
 
-loadAll :: [ContractInfo] -> Q [Dec]
+instance Num (Expr 'EAddr) where
+  fromInteger i = LitAddr (fromInteger i)
+
+loadAll :: [ContractFileInfo] -> Q [Dec]
 loadAll contracts = do
   cs <- runIO $ traverse loadSolcInfo contracts
-  let indexed = zip [0x1000 ..] cs
-  methods <- traverse (\(ix, (_, bn, _, m)) -> traverse (\m' -> generateTxFactory m' ix bn) m) indexed
-  let allMethods = concat methods
-  let contractMap = fmap (\(ix, (_, _, b, _)) -> (LitAddr (fromInteger ix), b)) indexed
-  contractNames <- traverse (\(ix, ContractInfo _ _ nm) -> contractName nm ix) (zip [0x1000 ..] contracts)
+  let allContracts = Map.unions cs
+  let allContractsHash = zip [ 0x1000.. ] (Map.toList allContracts)
+  methods <- generateDefsForMethods allContractsHash
+  let contractMap = generateContractMap allContractsHash
+  contractNames <- traverse (\(addr, (nm, (bn, con))) -> contractName bn addr) allContractsHash -- traverse (\(ix, ContractFileInfo _ nm) -> contractName nm ix) (zip [0x1000 ..] contracts)
   init <-
     [d|
-      initial :: ST s (VM s)
+      initial :: ST s (VM Concrete s)
       initial = loadIntoVM contractMap
       |]
-  pure (init ++ allMethods ++ contractNames)
+  pure (init ++ methods ++ contractNames)
   where
+                        -- Address, Contract name, Bound name
+    generateContractMap :: [(Integer, (Text, (Text, SolcContract)))] -> [(Integer, ByteString)]
+    generateContractMap = fmap (\(i, (nm, (bn, con))) -> (i, con.runtimeCode))
+                        -- Address, Contract name, Bound name
+    generateDefsForMethods :: [(Integer, (Text, (Text, SolcContract)))] -> Q [Dec]
+    generateDefsForMethods [] = pure []
+    generateDefsForMethods ((hash, (name, (boundName, contract))) : xs) = do
+      let methods = Map.elems contract.abiMap
+      traverse (\x -> generateTxFactory x hash name) methods
+
     contractName :: Text -> Integer -> Q Dec
     contractName binder value = do
       let nm = mkName (unpack (binder <> "_contract"))
       let value' = LitAddr (fromInteger value)
       addr <- [e|value'|]
       pure (ValD (VarP nm) (NormalB addr) [])
 
-loadSolcInfo :: ContractInfo -> IO (Text, Text, ByteString, [Method])
-loadSolcInfo (ContractInfo contractFilename contractName boundName) = do
+loadSolcInfo :: ContractFileInfo -> IO (Map Text (Text, SolcContract))
+loadSolcInfo (ContractFileInfo contractFilename modules) = do
   file <- readFile (unpack contractFilename)
-  solRes <- solidity' file
-  let (bytecode, methods) = getSolcResults solRes
-  pure (contractName, boundName, bytecode, methods)
+  json <- solc Solidity file
+  let (Contracts sol, _, _) = fromJust $ readStdJSON json
+  let retrievedMap = fmap (\mod -> (mod.name, (mod.boundName, Map.lookup ("hevm.sol:" <> mod.name) sol))) (modules)
+  contractmap <- emitMissing retrievedMap
+  pure $ Map.fromList contractmap
   where
-    getSolcResults :: (Text, Text) -> (ByteString, [Method])
-    getSolcResults (json, path) = case readStdJSON json of
-      Nothing -> error ("could not read json file: " <> show json)
-      Just (Contracts sol, a, b) ->
-        case Map.lookup (path <> ":" <> contractName) sol of
-          Nothing -> error "failed looking up contract"
-          Just contract ->
-            let methods = Map.elems $ contract.abiMap
-             in (contract.runtimeCode, methods)
+    emitMissing :: Show a => [(Text, (b, Maybe a))] -> IO [(Text, (b, a))]
+    emitMissing [] = pure []
+    emitMissing ((t, (s, Nothing)) : xs) = putStrLn ("contract " ++ show t ++ "is missing") >> emitMissing xs
+    emitMissing ((t, (s, Just x)) : xs) = ((t, (s, x)) :) <$> emitMissing xs
 
-run' :: EVM s (VM s)
+run' :: EVM Concrete s (VM Concrete s)
 run' = do
   vm <- get
   case vm.result of
     Nothing -> exec1 >> run'
     Just (HandleEffect (Query (PleaseAskSMT (Lit c) _ cont))) ->
-      cont (Case (c > 0)) >> run'
+      undefined -- cont (Case (c > 0)) >> run'
     Just (VMFailure y) -> pure vm
     Just (VMSuccess y) -> pure vm
 
--- send and run a transaction on the EVM state
-sendAndRun' :: EthTransaction -> EVM RealWorld (VM RealWorld)
+-- send and run a transaction on the EVM Concrete state
+sendAndRun' :: EthTransaction -> EVM Concrete RealWorld (VM Concrete RealWorld)
 sendAndRun' tx = do
   EVM.TH.makeTxCall tx
   vm <- run'
   pure vm
 
-sendAndRunAll :: [EthTransaction] -> EVM RealWorld (VM RealWorld)
+sendAndRunAll :: [EthTransaction] -> EVM Concrete RealWorld (VM Concrete RealWorld)
 sendAndRunAll [transaction] = sendAndRun' transaction
 sendAndRunAll (tx : ts) = do
   EVM.TH.makeTxCall tx
   vm <- run'
   sendAndRunAll ts
 
--- exectute the EVM state in IO
+-- exectute the EVM Concrete state in IO
 sendAndRun ::
   EthTransaction ->
-  VM RealWorld ->
-  EVM RealWorld (VM RealWorld)
+  VM Concrete RealWorld ->
+  EVM Concrete RealWorld (VM Concrete RealWorld)
 sendAndRun tx st = do
   put st
   sendAndRun' tx
@@ -264,7 +278,7 @@ sendAndRun tx st = do
 adjustOrAdd :: (Ord k) => (v -> v) -> v -> k -> Map.Map k v -> Map.Map k v
 adjustOrAdd f def = alter (Just . maybe def f)
 
-setupAddresses :: [(Expr EAddr, Expr EWord)] -> VM s -> VM s
+setupAddresses :: [(Expr EAddr, Expr EWord)] -> VM Concrete s -> VM Concrete s
 setupAddresses amounts =
   over (#env % #contracts) (updateContractMap amounts)
   where
@@ -279,16 +293,16 @@ setupAddresses amounts =
 
     createNew (addr, amount) = (addr, set #balance amount emptyContract)
 
-    updateContractState :: (Expr EAddr, Contract) -> VM s -> VM s
+    updateContractState :: (Expr EAddr, Contract) -> VM Concrete s -> VM Concrete s
     updateContractState (addr, contract) = set (#env % #contracts % at addr) (Just contract)
 
-getAllContracts :: VM s -> [(Expr EAddr, Expr EWord)]
+getAllContracts :: VM Concrete s -> [(Expr EAddr, Expr EWord)]
 getAllContracts vm =
   let contracts = Map.toList $ view (#env % #contracts) vm
       contractsAmounts = fmap (fmap (view #balance)) contracts
    in contractsAmounts
 
-balance :: VM s -> Expr EAddr -> W256
+balance :: VM Concrete s -> Expr EAddr -> W256
 balance st addr =
   let contract = Map.lookup addr st.env.contracts
       Just balance = fmap (view #balance) contract
@@ -297,7 +311,7 @@ balance st addr =
 
 -- TODO: use foundry
 -- thatOneMethod =
---   let st = loadContracts [ContractInfo "solidity/Simple.sol" "Neg" "test"]
+--   let st = loadContracts [ContractFileInfo "solidity/Simple.sol" "Neg" "test"]
 --       ourTransaction =
 --         EthTransaction
 --           (LitAddr 0xabcd)

evm/src/Examples/Components.hs

@@ -88,7 +88,7 @@ addPrivateValueDirectEndogenous name payoffFunctionDirect =
   [opengame|
 
     inputs    : dec, privateValueDirect ;
-    feedback  :     ;
+    feedback  :   ;
 
     :---------------------------:
 

evm/src/Examples/HEVM.hs

@@ -37,7 +37,7 @@ import OpenGames.Engine.HEVMGames
 import OpenGames.Preprocessor hiding (Lit)
 import Optics.Core (at, over, preview, set, view, (%), (%?), (&), (.~))
 
-$(loadAll [ContractInfo "solidity/Withdraw.sol" "Piggybank" "store"])
+$(loadAll [ContractFileInfo "solidity/Withdraw.sol" [ContractInfo "Piggybank" "store"]])
 
 deposit :: EthTransaction
 deposit = store_deposit userContractAddress 1000 10_000_000

evm/src/Examples/Lido.hs

@@ -6,8 +6,11 @@ module Examples.Lido where
 
 import EVM.TH
 
+-- lido = loadContracts [("EmergencyProtectedTimelockModel", "solidity/EmergencyProtectedTimelockModel.sol")]
+-- lido = [loadContract| file : solidity/LidoReward.sol, contract : LidoExecutionLayerRewardsVault, name : lido]
+
 -- lido = loadContracts [("LidoExecutionLayerRewardsVault", "solidity/LidoReward.sol")]
 -- lido = [loadContract| file : solidity/LidoReward.sol, contract : LidoExecutionLayerRewardsVault, name : lido]
 --
 
--- $(loadABI "solidity/LidoReward.sol" "LidoExecutionLayerRewardsVault")
+-- $(loadAll [ContractInfo "solidity/EmergencyProtectedTimelockModel.sol" "TimelockModel" "model"])

evm/src/Examples/Prisoner.hs

@@ -19,11 +19,12 @@ import EVM.Fetch (zero)
 import EVM.Prelude
 import EVM.Stepper (evm, interpret, runFully)
 import EVM.TH
+import EVM.Types
 import OpenGames hiding (dependentDecision, fromFunctions, fromLens)
 import OpenGames.Engine.HEVMGames
 import OpenGames.Preprocessor hiding (Lit)
 
-$(loadAll [ContractInfo "solidity/Prisonner.sol" "Prison" "prison"])
+$(loadAll [ContractFileInfo "solidity/Prisonner.sol" [ContractInfo "Prison" "prison"]])
 
 player1 = LitAddr 0x1234
 

evm/src/OpenGames/Engine/Copy.hs

@@ -1,6 +1,8 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE OverloadedLabels #-}
 {-# LANGUAGE NoFieldSelectors #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
 
 module OpenGames.Engine.Copy where
 
@@ -18,7 +20,7 @@ class Copy (a :: Type -> Type) where
 class Restore (a :: Type -> Type) where
   restore :: a s -> StateT (a s) (ST s) ()
 
-instance Copy VM where
+instance Copy (VM Concrete) where
   copy = do
     state <- get
     let st = state ^. #state
@@ -28,16 +30,16 @@ instance Copy VM where
     let newState =
           state
             & #state
-              .~ st'
+            .~ st'
             & #frames
-              .~ fr'
+            .~ fr'
             & #result
-              .~ Nothing
+            .~ Nothing
     pure newState
     where
-      copyFrame :: Frame s -> StateT (VM s) (ST s) (Frame s)
+      copyFrame :: Frame Concrete s -> StateT (VM Concrete s) (ST s) (Frame Concrete s)
       copyFrame (Frame ctx state) = Frame ctx <$> copyFrameState state
-      copyFrameState :: FrameState s -> StateT (VM s) (ST s) (FrameState s)
+      copyFrameState :: FrameState Concrete s -> StateT (VM Concrete s) (ST s) (FrameState Concrete s)
       copyFrameState oldFrame = do
         let mem = oldFrame ^. #memory
         mem' <- case mem of
@@ -46,5 +48,5 @@ instance Copy VM where
 
         pure (oldFrame & #memory .~ mem')
 
-instance Restore VM where
+instance Restore (VM Concrete) where
   restore = put

evm/src/OpenGames/Engine/HEVMGames.hs

@@ -13,7 +13,7 @@ import Data.HashMap as HM hiding (map, mapMaybe, null)
 import Data.Maybe (fromJust)
 import Data.Ord (comparing)
 import Data.Utils
-import EVM.Types (VM, W256, toInt)
+import EVM.Types (VM, W256, VMType(..))
 import GHC.Float (int2Double)
 import GHC.ST
 import OpenGames.Engine.Copy
@@ -24,13 +24,13 @@ import OpenGames.Engine.TLL
 
 type OpenGameM m a b x s y r = OpenGame (MonadOpticM m W256) (MonadContextM m W256) a b x s y r
 
-type HEVMState = StateT (VM RealWorld) (ST RealWorld)
+type HEVMState = StateT (VM Concrete RealWorld) (ST RealWorld)
 
 type HEVMGame a b x s y r = OpenGameM HEVMState a b x s y r
 
 -- converting words to double for diagnostic reasons
 word2Double :: W256 -> Double
-word2Double x = int2Double (fromJust $ toInt x)
+word2Double x = fromInteger (fromIntegral x)
 
 hevmDecision ::
   forall x y.