add postconditon to AMM

ethereum · May 26, 2024 · 24ebf2e · 24ebf2e
1 parent 712b424
commit 24ebf2e
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/tests/hevm/pass/amm/amm.act b/tests/hevm/pass/amm/amm.act
@@ -85,6 +85,8 @@ returns 1
 ensures
 
     pre(token0.balanceOf[THIS]) * pre(token1.balanceOf[THIS]) <= post(token0.balanceOf[THIS]) * post(token1.balanceOf[THIS])
+    post(token0.balanceOf[THIS]) * post(token1.balanceOf[THIS]) <= pre(token0.balanceOf[THIS]) * pre(token1.balanceOf[THIS]) + pre(token0.balanceOf[THIS]) + amt
+
 
 
 behaviour swap1 of Amm
@@ -118,4 +120,5 @@ returns 1
 
 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])
+    post(token0.balanceOf[THIS]) * post(token1.balanceOf[THIS]) <= pre(token0.balanceOf[THIS]) * pre(token1.balanceOf[THIS]) + pre(token1.balanceOf[THIS]) + amt