.

Author: liav-certora

DEFI/ConstantProductPool/README.md

@@ -28,7 +28,7 @@ Refer to `certora/conf/runBroken.conf` and `certora/conf/runFixed.conf` for more
 To check this version, run: 
 ```certoraRun runBroken.conf```
 
-[The report of the run](https://prover.certora.com/output/15800/fa11484d63054f79a199c8620af33bdb?anonymousKey=1cdcdf2c4cf2cd17157ecb1290dc726e15ba8de4)
+[The report of the run](https://prover.certora.com/output/15800/2987524d197447f4944e13ed519390f9?anonymousKey=d09bc4f46c5bab5a51296938fbffeb9fcac03252)
 
 ## Correct Code
 
@@ -37,4 +37,4 @@ To check this version, run:
 This contract can be verified by running: 
 ```certoraRun runFixed.conf```
 
-[The report of the run](https://prover.certora.com/output/15800/1fe898be7fc242909c043bac5b8c67e7?anonymousKey=ca1719a1a7ee64b224160d5ebf0b02fa69b20e28)
+[The report of the run](https://prover.certora.com/output/15800/b1ed0c02f9d0409fbaed4485f5b23a56?anonymousKey=a48319976eedda3ebf0e7c3eabe1ead2e02c809f)

DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec

@@ -6,6 +6,7 @@ See https://docs.certora.com for a complete guide.
 // reference from the spec to additional contracts used in the verification 
 using DummyERC20A as _token0;
 using DummyERC20B as _token1;
+using ConstantProductPool as _pool;
 
 
 /*
@@ -25,6 +26,8 @@ methods{
     //calls to external contracts  
     function _token0.balanceOf(address account) external returns (uint256) envfree;
     function _token1.balanceOf(address account) external returns (uint256) envfree;
+    function _token0.allowance(address owner, address spender) external returns (uint256) envfree;
+    function _token1.allowance(address owner, address spender) external returns (uint256) envfree;
     function _token0.transfer(address, uint) external;
     function _token1.transfer(address, uint) external;
 
@@ -127,17 +130,32 @@ invariant balanceGreaterThanReserve()
 
         // This preserved is safe because transferFrom is called from the currentContract whose code is known and
         // it is not msg.sender. It would not be safe to do if the call was to a function of an unresolved contract.
-        preserved transferFrom(address sender, address recipient,uint256 amount) with (env e1) {
+        preserved _.transferFrom(address sender, address recipient,uint256 amount) with (env e1) {
+            requireInvariant allowanceOfPoolAlwaysZero(e1.msg.sender);
             require e1.msg.sender != currentContract;
         }
 
-       // This preserved is safe because transfer is called from the currentContract whose code is known and
+        // This preserved is safe because transfer is called from the currentContract whose code is known and
         // it is not msg.sender.
-        preserved transfer(address recipient, uint256 amount) with (env e2) {
+        preserved _.transfer(address recipient, uint256 amount) with (env e2) {
             require e2.msg.sender != currentContract;
         }
     }
 
+invariant allowanceOfPoolAlwaysZero(address a)
+    _token0.allowance(_pool, a) == 0 && _token1.allowance(_pool, a) == 0
+    {
+        // This preserved is safe because we know the code in the pool contract.
+        preserved _.approve(address spender, uint256 amount) with (env e1) {
+            require e1.msg.sender != _pool;
+        }
+
+        // This preserved is safe because we know the code in the pool contract.
+        preserved _.increaseAllowance(address spender, uint256 addedValue) with (env e2) {
+            require e2.msg.sender != _pool;
+        }
+    }
+
 
 /*
 Property: Integrity of totalSupply with respect to the amount of reserves.