amm experiments

flake.nix

@@ -5,7 +5,7 @@
     flake-utils.url = "github:numtide/flake-utils";
     nixpkgs.url = "github:nixos/nixpkgs";
     hevmUpstream = {
-      url = "github:ethereum/hevm";
+      url = "github:ethereum/hevm/b025ea2162373916953d6bfe3430859222f298f7";
       inputs.nixpkgs.follows = "nixpkgs";
     };
   };

src/Act/HEVM.hs

@@ -315,8 +315,14 @@ returnsToExpr :: ContractMap -> Maybe TypedExp -> ActM (EVM.Expr EVM.Buf)
 returnsToExpr _ Nothing = pure $ EVM.ConcreteBuf ""
 returnsToExpr cmap (Just r) = typedExpToBuf cmap r
 
+writeWord' :: EVM.Expr EVM.EWord -> EVM.Expr EVM.EWord -> EVM.Expr EVM.Buf -> EVM.Expr EVM.Buf
+-- writeWord' i v b = EVM.WriteWord i v b
+writeWord' i v b =
+  trace ("Calling writeWord with i: " <> (show i) <> " v : " <> (show v) <> " b:" <> (show b)) $
+  EVM.CopySlice (EVM.Lit 0) (EVM.Lit 0) (EVM.Lit 64) (EVM.WriteWord i v b) (EVM.ConcreteBuf "")
+
 wordToBuf :: EVM.Expr EVM.EWord -> EVM.Expr EVM.Buf
-wordToBuf w = EVM.WriteWord (EVM.Lit 0) w (EVM.ConcreteBuf "")
+wordToBuf w = trace ("Show call word to buf with w : " <> (show w)) $ EVM.WriteWord (EVM.Lit 0) w (EVM.ConcreteBuf "")
 
 wordToProp :: EVM.Expr EVM.EWord -> EVM.Prop
 wordToProp w = EVM.PNeg (EVM.PEq w (EVM.Lit 0))
@@ -331,10 +337,10 @@ expToBuf cmap styp e = do
   case styp of
     SInteger -> do
       e' <- toExpr cmap e
-      pure $ EVM.WriteWord (EVM.Lit 0) e' (EVM.ConcreteBuf "")
+      pure $ writeWord' (EVM.Lit 0) e' (EVM.ConcreteBuf "")
     SBoolean -> do
       e' <- toExpr cmap e
-      pure $ EVM.WriteWord (EVM.Lit 0) e' (EVM.ConcreteBuf "")
+      pure $ writeWord' (EVM.Lit 0) e' (EVM.ConcreteBuf "")
     SByteStr -> toExpr cmap e
     SContract -> error "Internal error: expecting primitive type"
 
@@ -608,7 +614,7 @@ checkBehaviours solvers (Contract _ behvs) actenv cmap = do
     solbehvs <- removeFails <$> getRuntimeBranches solvers hevmstorage calldata
     showMsg $ "\x1b[1mChecking behavior \x1b[4m" <> name <> "\x1b[m of Act\x1b[m"
     traceM "Act"
-    -- traceM (showBehvs behvs')
+    traceM (showBehvs behvs')
     -- traceM "Solidity"
     -- traceM (showBehvs solbehvs)
     -- equivalence check

tests/hevm/pass/amm/amm.act

@@ -58,7 +58,7 @@ interface swap0(uint256 amt)
 
 iff
     CALLVALUE == 0
-
+    amt > 54
 // iff in range uint256
 
     // token0.balanceOf[CALLER] - amt
@@ -70,8 +70,8 @@ iff
 
 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))

tests/hevm/pass/amm/amm.sol

@@ -31,18 +31,11 @@ contract Amm {
 	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);
+	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); */
-    /* 	token1.transferFrom(amt, msg.sender, address(this)); */
-    /* 	token0.transferFrom((token0.balanceOf(address(this))*amt) / (token1.balanceOf(address(this)) + amt), address(this), msg.sender); */
-    /*     return 1; */
-    /* } */
 }