hevm: implement CALLER and THIS

ethereum · Jan 23, 2024 · 567b25d · 567b25d
1 parent cb5b547
commit 567b25d
Show file tree

Hide file tree

Showing 3 changed files with 63 additions and 41 deletions.
diff --git a/src/Act/HEVM.hs b/src/Act/HEVM.hs
@@ -85,6 +85,7 @@ data ActEnv = ActEnv
   , fresh   :: Int
   , layout  :: Layout
   , caddr   :: EVM.Expr EVM.EAddr
+  , caller  :: Maybe (EVM.Expr EVM.EAddr)
   }
 
 type ActM a = State ActEnv a
@@ -120,12 +121,21 @@ localCaddr :: EVM.Expr EVM.EAddr -> ActM a -> ActM a
 localCaddr caddr m = do
   env <- get
   let caddr' = env.caddr
-  put (env { caddr = caddr })
+  let caller' = env.caller
+  put (env { caddr = caddr, caller = Just caddr' })
   res <- m
   env' <- get
-  put (env' { caddr = caddr' })
+  put (env' { caddr = caddr', caller =  caller' })
   pure res
 
+getCaller :: ActM (EVM.Expr EVM.EAddr)
+getCaller = do
+  env <- get
+  case env.caller of
+    Just c -> pure c
+    Nothing -> pure $ EVM.SymAddr "caller" -- Zoe: not sure what to put here
+
+
 -- * Act translation
 
 translateConstructor ::  BS.ByteString -> Constructor -> ActM ([EVM.Expr EVM.End], Calldata, Sig)
@@ -382,17 +392,21 @@ refAddr cmap (SField _ ref c x) = do
     Nothing -> error "Internal error: contract not found"
 refAddr _ (SMapping _ _ _) = error "Internal error: mapping address not suppported"
 
-ethEnvToWord :: EthEnv -> EVM.Expr EVM.EWord
-ethEnvToWord Callvalue = EVM.TxValue
-ethEnvToWord Caller = EVM.WAddr $ EVM.SymAddr "caller"
-ethEnvToWord Origin = EVM.Origin
-ethEnvToWord Blocknumber = EVM.BlockNumber
-ethEnvToWord Blockhash = EVM.BlockHash $ EVM.Lit 0
-ethEnvToWord Chainid = EVM.ChainId
-ethEnvToWord Gaslimit = EVM.GasLimit
-ethEnvToWord Coinbase = EVM.Coinbase
-ethEnvToWord Timestamp = EVM.Timestamp
-ethEnvToWord This = error "TODO"
+ethEnvToWord :: EthEnv -> ActM (EVM.Expr EVM.EWord)
+ethEnvToWord Callvalue = pure $ EVM.TxValue
+ethEnvToWord Caller = do
+  c <- getCaller
+  pure $ EVM.WAddr c
+ethEnvToWord Origin = pure $ EVM.Origin
+ethEnvToWord Blocknumber = pure $ EVM.BlockNumber
+ethEnvToWord Blockhash = pure $ EVM.BlockHash $ EVM.Lit 0
+ethEnvToWord Chainid = pure $ EVM.ChainId
+ethEnvToWord Gaslimit = pure $ EVM.GasLimit
+ethEnvToWord Coinbase = pure $ EVM.Coinbase
+ethEnvToWord Timestamp = pure $ EVM.Timestamp
+ethEnvToWord This = do
+  c <- getCaddr
+  pure $ EVM.WAddr c
 ethEnvToWord Nonce = error "TODO"
 ethEnvToWord Calldepth = error "TODO"
 ethEnvToWord Difficulty = error "TODO"
@@ -465,7 +479,7 @@ toExpr cmap = \case
   (Mod _ e1 e2) -> op2 EVM.Mod e1 e2 -- which mod?
   (Exp _ e1 e2) -> op2 EVM.Exp e1 e2
   (LitInt _ n) -> pure $ EVM.Lit (fromIntegral n)
-  (IntEnv _ env) -> pure $ ethEnvToWord env
+  (IntEnv _ env) -> ethEnvToWord env
   -- bounds
   (IntMin _ n) -> pure $ EVM.Lit (fromIntegral $ intmin n)
   (IntMax _ n) -> pure $ EVM.Lit (fromIntegral $ intmax n)
@@ -567,7 +581,7 @@ checkEquiv solvers l1 l2 = do
 
 checkConstructors :: App m => SolverGroup -> ByteString -> ByteString -> Store -> Contract -> CodeMap -> m (ContractMap, ActEnv)
 checkConstructors solvers initcode runtimecode store (Contract ctor _) codemap = do
-  let actenv = ActEnv codemap 0 (slotMap store) (EVM.SymAddr "entrypoint")
+  let actenv = ActEnv codemap 0 (slotMap store) (EVM.SymAddr "entrypoint") Nothing
   let ((actbehvs, calldata, sig), actenv') = flip runState actenv $ translateConstructor runtimecode ctor
   traceM "Act"
   traceM (showBehvs actbehvs)  

diff --git a/tests/hevm/pass/amm/amm.act b/tests/hevm/pass/amm/amm.act
@@ -31,7 +31,7 @@ case from =/= to:
   storage
 
     balanceOf[from]  => balanceOf[from] - value
-    balanceOf[to]      => balanceOf[to] + value
+    balanceOf[to]    => balanceOf[to] + value
 
   returns 1
 
@@ -41,7 +41,7 @@ case from == to:
 
 
 constructor of Amm
-interface constructor(uint256 amt1)
+interface constructor(uint256 amt1, uint256 amt2)
 
 iff
 
@@ -51,33 +51,36 @@ iff
 creates
 
     Token token0 := create Token(amt1)
-    // Token token1 := create Token(amt2)
+    Token token1 := create Token(amt2)
 
-// behaviour swap0 of Amm
-// interface swap0(uint256 amt)
+behaviour swap0 of Amm
+interface swap0(uint256 amt)
+
+iff
+    CALLVALUE == 0
 
 // iff in range uint256
 
-//     token0.balanceOf[CALLER] - amt
-//     token0.balanceOf[THIS] + amt
+    // token0.balanceOf[CALLER] - amt
+    // token0.balanceOf[THIS] + amt
 //     token0.balanceOf[THIS] * token1.balanceOf[THIS]
 //     (token1.balanceOf[THIS] * amt) / (token0.balanceOf[THIS] + amt)
-//     token1.balanceOf[THIS] - (token1.balanceOf[THIS] * amt) / (token0.balanceOf[THIS] + amt)
-//     token1.balanceOf[CALLER] +  (token1.balanceOf[THIS] * amt) / (token0.balanceOf[THIS] + amt)
+//     token1.balanceOf[THIS] - ((token1.balanceOf[THIS] * amt) / (token0.balanceOf[THIS] + amt))
+//     token1.balanceOf[CALLER] +  ((token1.balanceOf[THIS] * amt) / (token0.balanceOf[THIS] + amt))
 
-// storage
+storage
 
-//     token0.balanceOf[CALLER] => token0.balanceOf[CALLER] - amt
-//     token0.balanceOf[THIS]   => token0.balanceOf[THIS] + amt
+    // token0.balanceOf[CALLER] => token0.balanceOf[CALLER] - amt
+    // token0.balanceOf[THIS]   => token0.balanceOf[THIS] + amt
 
-//     token1.balanceOf[THIS]   => token1.balanceOf[THIS] - ((token1.balanceOf[THIS] * amt) / (token0.balanceOf[THIS] + amt))
-
-//     token1.balanceOf[CALLER] => token1.balanceOf[CALLER] + ((token1.balanceOf[THIS] * amt) / (token0.balanceOf[THIS] + amt))
+    token1.balanceOf[THIS]   => token1.balanceOf[THIS] - ((token1.balanceOf[THIS] * amt) / (token0.balanceOf[THIS] + amt))
+    token1.balanceOf[CALLER] => token1.balanceOf[CALLER] + ((token1.balanceOf[THIS] * amt) / (token0.balanceOf[THIS] + amt))
 
+returns 1
 
-// ensures
+ensures
 
-//     pre(token0.balanceOf[THIS]) * pre(token1.balanceOf[THIS]) <= post(token0.balanceOf[THIS]) * post(token1.balanceOf[THIS])
+    pre(token0.balanceOf[THIS]) * pre(token1.balanceOf[THIS]) <= post(token0.balanceOf[THIS]) * post(token1.balanceOf[THIS])
 
 
 // behaviour swap1 of Amm

diff --git a/tests/hevm/pass/amm/amm.sol b/tests/hevm/pass/amm/amm.sol
@@ -20,19 +20,24 @@ contract Token {
 contract Amm {
 
     Token token0;
-    /* Token token1; */
+    Token token1;
 
-    constructor(uint256 amt1) {
+    constructor(uint256 amt1, uint256 amt2) {
         token0 = new Token(amt1);
-	/* token1 = new Token(amt2); */
+	token1 = new Token(amt2);
     }
 
-    /* function swap0(uint256 amt) public returns (uint) { */
-    /* 	require (token0.balanceOf(msg.sender) >= amt); */
-    /* 	token0.transferFrom(amt, msg.sender, address(this)); */
-    /* 	token1.transferFrom((token1.balanceOf(address(this))*amt) / (token0.balanceOf(address(this)) + amt), address(this), msg.sender); */
-    /*     return 1; */
-    /* } */
+    function swap0(uint256 amt) public returns (uint) {
+	uint256 reserve0 = token0.balanceOf(address(this));
+	uint256 reserve1 = token1.balanceOf(address(this));
+
+	/* require (token0.balanceOf(msg.sender) >= amt); */
+
+	/* token0.transferFrom(amt, msg.sender, address(this)); */
+	token1.transferFrom((reserve1*amt) / (reserve0+amt), address(this), msg.sender);
+
+	return 1;
+    }
 
     /* function swap1(uint256 amt) public returns (uint) { */
     /* 	require (token1.balanceOf(msg.sender) >= amt); */