wip in preconditions for AMM

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

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/tests/hevm/pass/amm/amm.act b/tests/hevm/pass/amm/amm.act
@@ -63,6 +63,9 @@ iff
 
     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
 

diff --git a/tests/hevm/pass/amm/amm.sol b/tests/hevm/pass/amm/amm.sol
@@ -31,7 +31,6 @@ contract Amm {
 	uint256 reserve0 = token0.balanceOf(address(this));
 	uint256 reserve1 = token1.balanceOf(address(this));
 
-	require(msg.sender != address(this));
 	token0.transferFrom(amt, msg.sender, address(this));
 	token1.transferFrom((reserve1*amt)/(reserve0+amt), address(this), msg.sender);