AMM full spec

ethereum · Feb 23, 2024 · bf913d3 · bf913d3
1 parent b61df21
commit bf913d3
Show file tree

Hide file tree

Showing 3 changed files with 43 additions and 25 deletions.
diff --git a/src/Act/HEVM.hs b/src/Act/HEVM.hs
@@ -615,8 +615,8 @@ checkBehaviours solvers (Contract _ behvs) actenv cmap = do
     -- traceM "Solidity"
     -- traceM (showBehvs solbehvs)
     -- equivalence check
-    -- showMsg $ "\x1b[1mChecking if behaviour is matched by EVM\x1b[m"
-    -- checkResult calldata (Just sig) =<< checkEquiv solvers solbehvs behvs'
+    showMsg $ "\x1b[1mChecking if behaviour is matched by EVM\x1b[m"
+    checkResult calldata (Just sig) =<< checkEquiv solvers solbehvs behvs'
     -- input space exhaustiveness check
     showMsg $ "\x1b[1mChecking if the input spaces are the same\x1b[m"
     checkResult calldata (Just sig) =<< checkInputSpaces solvers solbehvs behvs'

diff --git a/tests/hevm/pass/amm/amm.act b/tests/hevm/pass/amm/amm.act
@@ -27,7 +27,7 @@ iff
   inRange(uint256,balanceOf[from] - value)
 
 case from =/= to:
-  
+
   storage
 
     balanceOf[from]  => balanceOf[from] - value
@@ -57,18 +57,15 @@ behaviour swap0 of Amm
 interface swap0(uint256 amt)
 
 iff
-    CALLVALUE == 0     
-    inRange(uint256,token0.balanceOf[CALLER] - amt)    
+    CALLVALUE == 0
+    inRange(uint256,token0.balanceOf[CALLER] - amt)
     CALLER =/= THIS => inRange(uint256,token0.balanceOf[THIS] + amt)
 
     inRange(uint256,token1.balanceOf[THIS] - ((token1.balanceOf[THIS] * amt) / (token0.balanceOf[THIS] + amt)))
     CALLER =/= THIS => inRange(uint256,token1.balanceOf[CALLER] + ((token1.balanceOf[THIS] * amt) / (token0.balanceOf[THIS] + amt)))
 
-    inRange(uint256, token1.balanceOf[THIS] * amt)
-    inRange(uint256, token0.balanceOf[THIS] + amt)
-
     token0.balanceOf[THIS] + amt =/= 0
-    
+
 case CALLER =/= THIS:
 
 storage
@@ -90,24 +87,35 @@ ensures
     pre(token0.balanceOf[THIS]) * pre(token1.balanceOf[THIS]) <= post(token0.balanceOf[THIS]) * post(token1.balanceOf[THIS])
 
 
-// behaviour swap1 of Amm
-// interface swap1(uint256 amt)
+behaviour swap1 of Amm
+interface swap1(uint256 amt)
 
-// iff in range uint256
+iff
+    CALLVALUE == 0
+    inRange(uint256,token1.balanceOf[CALLER] - amt)
+    CALLER =/= THIS => inRange(uint256,token1.balanceOf[THIS] + amt)
 
-//     token1.balanceOf[CALLER] - amt
-//     token1.balanceOf[THIS] + amt
-//     token0.balanceOf[THIS] - ((token0.balanceOf[THIS] * amt) / (token1.balanceOf[THIS] + amt))
-//     token0.balanceOf[CALLER] +  ((token0.balanceOf[THIS] * amt) / (token1.balanceOf[THIS] + amt))
+    inRange(uint256,token0.balanceOf[THIS] - ((token0.balanceOf[THIS] * amt) / (token1.balanceOf[THIS] + amt)))
+    CALLER =/= THIS => inRange(uint256,token0.balanceOf[CALLER] + ((token0.balanceOf[THIS] * amt) / (token1.balanceOf[THIS] + amt)))
 
-// storage
+    token1.balanceOf[THIS] + amt =/= 0
 
-//     token1.balanceOf[CALLER] => token1.balanceOf[CALLER] - amt
-//     token1.balanceOf[THIS]   => token1.balanceOf[THIS] + amt
+case CALLER =/= THIS:
+
+storage
 
-//     token0.balanceOf[THIS]   => token0.balanceOf[THIS] - ((token0.balanceOf[THIS] * amt) / (token1.balanceOf[THIS] + amt))
-//     token0.balanceOf[CALLER] => token0.balanceOf[CALLER] + ((token0.balanceOf[THIS] * amt) / (token1.balanceOf[THIS] + amt))
+    token1.balanceOf[CALLER] => token1.balanceOf[CALLER] - amt
+    token1.balanceOf[THIS]   => token1.balanceOf[THIS] + amt
 
-// ensures
+    token0.balanceOf[THIS]   => token0.balanceOf[THIS] - ((token0.balanceOf[THIS] * amt) / (token1.balanceOf[THIS] + amt))
+    token0.balanceOf[CALLER] => token0.balanceOf[CALLER] + ((token0.balanceOf[THIS] * amt) / (token1.balanceOf[THIS] + amt))
 
-//     pre(token0.balanceOf[THIS]) * pre(token1.balanceOf[THIS]) <= post(token0.balanceOf[THIS]) * post(token1.balanceOf[THIS])
+returns 1
+
+case CALLER == THIS:
+
+returns 1
+
+ensures
+
+    pre(token0.balanceOf[THIS]) * pre(token1.balanceOf[THIS]) <= post(token0.balanceOf[THIS]) * post(token1.balanceOf[THIS])
diff --git a/tests/hevm/pass/amm/amm.sol b/tests/hevm/pass/amm/amm.sol
@@ -8,7 +8,7 @@ contract Token {
     }
 
 
-    function transferFrom(uint256 value, address from, address to) public returns (uint) {	
+    function transferFrom(uint256 value, address from, address to) public returns (uint) {
 	balanceOf[from] = balanceOf[from] - value;
         balanceOf[to] = balanceOf[to] + value;
         return 1;
@@ -33,7 +33,17 @@ contract Amm {
 
 	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) {
+	uint256 reserve0 = token0.balanceOf(address(this));
+	uint256 reserve1 = token1.balanceOf(address(this));
+
+	token1.transferFrom(amt, msg.sender, address(this));
+	token0.transferFrom((reserve0*amt)/(reserve1+amt), address(this), msg.sender);
+
 	return 1;
     }