add mutations

certora/confs/setup/PoolManagerTest.conf

@@ -2,7 +2,7 @@
 // The verified properties can be assumed in the PoolManager mock spec 
 // (specs/setup/PoolManager.spec)
 {
-    "assert_autofinder_success": "true",
+    "assert_autofinder_success": true,
     "files": [
         "certora/harnesses/Conversions.sol",
         "certora/harnesses/PoolGetters.sol",
@@ -27,8 +27,7 @@
     "process": "emv",
 	"solc_evm_version": "cancun",
     "server":"production",
-    "solc":"solc8.26",
     "solc_via_ir": true,
-    "verify": "PoolManager:certora/specs/PoolManagerTest.spec",
+    "verify": "PoolManager:certora/specs/setup/PoolManagerTest.spec",
     "msg": "PoolManager mock test",
 }

certora/harnesses/PoolGetters.sol

@@ -0,0 +1,62 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.20;
+
+import { PoolId } from "@uniswap/v4-core/src/types/PoolId.sol";
+import { StateLibrary } from "@uniswap/v4-core/src/libraries/StateLibrary.sol";
+import { Position } from "@uniswap/v4-core/src/libraries/Position.sol";
+import { TransientStateLibrary } from "@uniswap/v4-core/src/libraries/TransientStateLibrary.sol";
+import { Slot0Library, Slot0 } from "@uniswap/v4-core/src/types/Slot0.sol";
+import { IPoolManager } from "@uniswap/v4-core/src/interfaces/IPoolManager.sol";
+import { Currency } from "@uniswap/v4-core/src/types/Currency.sol";
+
+contract PoolGetters {
+    using StateLibrary for IPoolManager;
+    using TransientStateLibrary for IPoolManager;
+
+    IPoolManager private immutable manager;
+
+    constructor(address _manager) {
+        manager = IPoolManager(_manager);
+    }
+
+    function _getSlot0(PoolId poolId) internal view returns (bytes32) {
+        bytes32 stateSlot = StateLibrary._getPoolStateSlot(poolId);
+        return manager.extsload(stateSlot);
+    }
+
+    function getSqrtPriceX96(PoolId poolId) external view returns (uint160) {
+        Slot0 packed = Slot0.wrap(_getSlot0(poolId));
+        return Slot0Library.sqrtPriceX96(packed);
+    }
+
+    function getTick(PoolId poolId) external view returns (int24 _tick) {
+        Slot0 packed = Slot0.wrap(_getSlot0(poolId));
+        return Slot0Library.tick(packed);
+    }
+
+    function getProtocolFee(PoolId poolId) external view returns (uint24 _protocolFee) {
+        Slot0 packed = Slot0.wrap(_getSlot0(poolId));
+        return Slot0Library.protocolFee(packed);
+    }
+
+    function getLpFee(PoolId poolId) external view returns (uint24 _lpFee) {
+        Slot0 packed = Slot0.wrap(_getSlot0(poolId));
+        return Slot0Library.lpFee(packed);
+    }
+
+    function isUnlocked() external view returns (bool) {
+        return manager.isUnlocked();
+    }
+
+    function getNonzeroDeltaCount() external view returns (uint256) {
+        return manager.getNonzeroDeltaCount();
+    }
+
+    function getSyncedCurrency() external view returns (Currency) {
+        return manager.getSyncedCurrency();
+    }
+
+    function getSyncedReserves() external view returns (uint256) {
+        return manager.getSyncedReserves();
+    }
+}

certora/mutations/DeltaResolver/DeltaResolver_0.sol

@@ -0,0 +1,91 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.24;
+
+import {Currency} from "@uniswap/v4-core/src/types/Currency.sol";
+import {TransientStateLibrary} from "@uniswap/v4-core/src/libraries/TransientStateLibrary.sol";
+import {IPoolManager} from "@uniswap/v4-core/src/interfaces/IPoolManager.sol";
+import {ImmutableState} from "./ImmutableState.sol";
+import {ActionConstants} from "../libraries/ActionConstants.sol";
+
+/// @notice Abstract contract used to sync, send, and settle funds to the pool manager
+/// @dev Note that sync() is called before any erc-20 transfer in `settle`.
+abstract contract DeltaResolver is ImmutableState {
+    using TransientStateLibrary for IPoolManager;
+
+    /// @notice Emitted trying to settle a positive delta.
+    error DeltaNotPositive(Currency currency);
+    /// @notice Emitted trying to take a negative delta.
+    error DeltaNotNegative(Currency currency);
+
+    /// @notice Take an amount of currency out of the PoolManager
+    /// @param currency Currency to take
+    /// @param recipient Address to receive the currency
+    /// @param amount Amount to take
+    function _take(Currency currency, address recipient, uint256 amount) internal {
+        poolManager.take(currency, recipient, amount);
+    }
+
+    /// @notice Pay and settle a currency to the PoolManager
+    /// @dev The implementing contract must ensure that the `payer` is a secure address
+    /// @param currency Currency to settle
+    /// @param payer Address of the payer
+    /// @param amount Amount to send
+    function _settle(Currency currency, address payer, uint256 amount) internal {
+        if (currency.isAddressZero()) {
+            poolManager.settle{value: amount}();
+        } else {
+            poolManager.sync(currency);
+            _pay(currency, payer, amount);
+            poolManager.settle();
+        }
+    }
+
+    /// @notice Abstract function for contracts to implement paying tokens to the poolManager
+    /// @dev The recipient of the payment should be the poolManager
+    /// @param token The token to settle. This is known not to be the native currency
+    /// @param payer The address who should pay tokens
+    /// @param amount The number of tokens to send
+    function _pay(Currency token, address payer, uint256 amount) internal virtual;
+
+    /// @notice Obtain the full amount owed by this contract (negative delta)
+    /// @param currency Currency to get the delta for
+    /// @return amount The amount owed by this contract as a uint256
+    function _getFullDebt(Currency currency) internal view returns (uint256 amount) {
+        int256 _amount = poolManager.currencyDelta(address(this), currency);
+        // If the amount is positive, it should be taken not settled.
+        if (_amount > 0) revert DeltaNotNegative(currency);
+        // Casting is safe due to limits on the total supply of a pool
+        // mutation: remove "-" before `_amount`
+        amount = uint256(_amount);
+    }
+
+    /// @notice Obtain the full credit owed to this contract (positive delta)
+    /// @param currency Currency to get the delta for
+    /// @return amount The amount owed to this contract as a uint256
+    function _getFullCredit(Currency currency) internal view returns (uint256 amount) {
+        int256 _amount = poolManager.currencyDelta(address(this), currency);
+        // If the amount is negative, it should be settled not taken.
+        if (_amount < 0) revert DeltaNotPositive(currency);
+        amount = uint256(_amount);
+    }
+
+    /// @notice Calculates the amount for a settle action
+    function _mapSettleAmount(uint256 amount, Currency currency) internal view returns (uint256) {
+        if (amount == ActionConstants.CONTRACT_BALANCE) {
+            return currency.balanceOfSelf();
+        } else if (amount == ActionConstants.OPEN_DELTA) {
+            return _getFullDebt(currency);
+        } else {
+            return amount;
+        }
+    }
+
+    /// @notice Calculates the amount for a take action
+    function _mapTakeAmount(uint256 amount, Currency currency) internal view returns (uint256) {
+        if (amount == ActionConstants.OPEN_DELTA) {
+            return _getFullCredit(currency);
+        } else {
+            return amount;
+        }
+    }
+}

certora/mutations/DeltaResolver/DeltaResolver_1.sol

@@ -0,0 +1,91 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.24;
+
+import {Currency} from "@uniswap/v4-core/src/types/Currency.sol";
+import {TransientStateLibrary} from "@uniswap/v4-core/src/libraries/TransientStateLibrary.sol";
+import {IPoolManager} from "@uniswap/v4-core/src/interfaces/IPoolManager.sol";
+import {ImmutableState} from "./ImmutableState.sol";
+import {ActionConstants} from "../libraries/ActionConstants.sol";
+
+/// @notice Abstract contract used to sync, send, and settle funds to the pool manager
+/// @dev Note that sync() is called before any erc-20 transfer in `settle`.
+abstract contract DeltaResolver is ImmutableState {
+    using TransientStateLibrary for IPoolManager;
+
+    /// @notice Emitted trying to settle a positive delta.
+    error DeltaNotPositive(Currency currency);
+    /// @notice Emitted trying to take a negative delta.
+    error DeltaNotNegative(Currency currency);
+
+    /// @notice Take an amount of currency out of the PoolManager
+    /// @param currency Currency to take
+    /// @param recipient Address to receive the currency
+    /// @param amount Amount to take
+    function _take(Currency currency, address recipient, uint256 amount) internal {
+        poolManager.take(currency, recipient, amount);
+    }
+
+    /// @notice Pay and settle a currency to the PoolManager
+    /// @dev The implementing contract must ensure that the `payer` is a secure address
+    /// @param currency Currency to settle
+    /// @param payer Address of the payer
+    /// @param amount Amount to send
+    function _settle(Currency currency, address payer, uint256 amount) internal {
+        if (currency.isAddressZero()) {
+            poolManager.settle{value: amount}();
+        } else {
+            // mutation: fail to call "sync"
+            // poolManager.sync(currency);
+            _pay(currency, payer, amount);
+            poolManager.settle();
+        }
+    }
+
+    /// @notice Abstract function for contracts to implement paying tokens to the poolManager
+    /// @dev The recipient of the payment should be the poolManager
+    /// @param token The token to settle. This is known not to be the native currency
+    /// @param payer The address who should pay tokens
+    /// @param amount The number of tokens to send
+    function _pay(Currency token, address payer, uint256 amount) internal virtual;
+
+    /// @notice Obtain the full amount owed by this contract (negative delta)
+    /// @param currency Currency to get the delta for
+    /// @return amount The amount owed by this contract as a uint256
+    function _getFullDebt(Currency currency) internal view returns (uint256 amount) {
+        int256 _amount = poolManager.currencyDelta(address(this), currency);
+        // If the amount is positive, it should be taken not settled.
+        if (_amount > 0) revert DeltaNotNegative(currency);
+        // Casting is safe due to limits on the total supply of a pool
+        amount = uint256(-_amount);
+    }
+
+    /// @notice Obtain the full credit owed to this contract (positive delta)
+    /// @param currency Currency to get the delta for
+    /// @return amount The amount owed to this contract as a uint256
+    function _getFullCredit(Currency currency) internal view returns (uint256 amount) {
+        int256 _amount = poolManager.currencyDelta(address(this), currency);
+        // If the amount is negative, it should be settled not taken.
+        if (_amount < 0) revert DeltaNotPositive(currency);
+        amount = uint256(_amount);
+    }
+
+    /// @notice Calculates the amount for a settle action
+    function _mapSettleAmount(uint256 amount, Currency currency) internal view returns (uint256) {
+        if (amount == ActionConstants.CONTRACT_BALANCE) {
+            return currency.balanceOfSelf();
+        } else if (amount == ActionConstants.OPEN_DELTA) {
+            return _getFullDebt(currency);
+        } else {
+            return amount;
+        }
+    }
+
+    /// @notice Calculates the amount for a take action
+    function _mapTakeAmount(uint256 amount, Currency currency) internal view returns (uint256) {
+        if (amount == ActionConstants.OPEN_DELTA) {
+            return _getFullCredit(currency);
+        } else {
+            return amount;
+        }
+    }
+}