Dev multisig wallet properties

CLAUDE.md

@@ -4,11 +4,12 @@ This file provides guidance to Claude Code (claude.ai/code) when working with co
 
 ## Project Overview
 
-This repository by Trail of Bits provides 168 pre-made Solidity property tests for fuzz testing smart contracts with [Echidna](https://github.com/crytic/echidna) or [Medusa](https://github.com/crytic/medusa). It covers:
+This repository by Trail of Bits provides 200+ pre-made Solidity property tests for fuzz testing smart contracts with [Echidna](https://github.com/crytic/echidna) or [Medusa](https://github.com/crytic/medusa). It covers:
 - ERC20 tokens (25 properties)
 - ERC721 tokens (19 properties)
 - ERC4626 vaults (37 properties)
 - ABDKMath64x64 fixed-point library (106 properties)
+- Uniswap V2 AMM pairs (30+ properties)
 
 ## Build Commands
 
@@ -56,6 +57,7 @@ medusa fuzz --target-contracts CryticERC20InternalHarness --config medusa-config
 ### Directory Structure
 - `contracts/` - Property contracts by standard
   - `ERC20/`, `ERC721/`, `ERC4626/` - Each split into `internal/` and `external/` testing
+  - `UniswapV2/` - Automated Market Maker (AMM) properties for constant product pools
   - `Math/ABDKMath64x64/` - Fixed-point math properties
   - `util/` - Helper functions (PropertiesHelper.sol, Hevm.sol, PropertiesConstants.sol)
 - `tests/` - Example test harnesses for Foundry and Hardhat

PROPERTIES.md

@@ -1,6 +1,6 @@
 # Introduction
 
-This file lists all the currently implemented Echidna property tests for ERC20, ERC721, ERC4626 and ABDKMath64x64. For each property, there is a permalink to the file implementing it in the repository and a small description of the invariant tested.
+This file lists all the currently implemented Echidna property tests for ERC20, ERC721, ERC4626, MultiSig wallets, and ABDKMath64x64. For each property, there is a permalink to the file implementing it in the repository and a small description of the invariant tested.
 
 ## Table of contents
 
@@ -17,6 +17,11 @@ This file lists all the currently implemented Echidna property tests for ERC20,
     - [Tests for burnable tokens](#tests-for-burnable-tokens-1)
     - [Tests for mintable tokens](#tests-for-mintable-tokens-1)
   - [ERC4626](#erc4626)
+  - [MultiSig](#multisig)
+    - [Basic properties](#basic-properties)
+    - [Threshold properties](#threshold-properties)
+    - [Signature and approval properties](#signature-and-approval-properties)
+    - [Nonce properties](#nonce-properties)
   - [ABDKMath64x64](#abdkmath64x64)
 
 ## ERC20
@@ -150,6 +155,55 @@ This file lists all the currently implemented Echidna property tests for ERC20,
 | ERC4626-036 | [verify_redeemRequiresTokenApproval](https://github.com/crytic/properties/blob/main/contracts/ERC4626/properties/RedeemUsingApprovalProps.sol#L73)   | Verifies that `redeem` requires token approval.          |
 | ERC4626-037 | [verify_convertToSharesMustNotRevert](https://github.com/crytic/properties/blob/main/contracts/ERC4626/properties/MustNotRevertProps.sol#L54)        | `convertToShares` must not revert for reasonable values. |
 
+## MultiSig
+
+### Basic properties
+
+| ID                  | Name                                                                                                                                                                      | Invariant tested                                                                 |
+| ------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------------------------------- |
+| MULTISIG-BASIC-001  | [test_MultiSig_onlyOwnersCanApprove](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigBasicProperties.sol#L17)               | Only wallet owners can be valid approvers.                                       |
+| MULTISIG-BASIC-002  | [test_MultiSig_thresholdWithinBounds](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigBasicProperties.sol#L33)              | Threshold must be greater than zero and not exceed owner count.                  |
+| MULTISIG-BASIC-003  | [test_MultiSig_noZeroAddressOwners](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigBasicProperties.sol#L48)                | No owner can be the zero address.                                                |
+| MULTISIG-BASIC-004  | [test_MultiSig_ownerCountMeetsThreshold](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigBasicProperties.sol#L61)           | Owner count must be at least equal to the threshold.                             |
+| MULTISIG-BASIC-005  | [test_MultiSig_ownerListNotEmpty](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigBasicProperties.sol#L73)                  | Owner list must contain at least one owner.                                      |
+| MULTISIG-BASIC-006  | [test_MultiSig_executedTransactionsStayExecuted](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigBasicProperties.sol#L82)   | Once executed, transactions remain in executed state.                            |
+| MULTISIG-BASIC-007  | [test_MultiSig_isOwnerConsistentWithOwnerList](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigBasicProperties.sol#L101)    | `isOwner` function must be consistent with the owner list.                       |
+| MULTISIG-BASIC-008  | [test_MultiSig_noDuplicateOwners](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigBasicProperties.sol#L132)                 | No address should appear more than once in the owner list.                       |
+
+### Threshold properties
+
+| ID                      | Name                                                                                                                                                                           | Invariant tested                                                                        |
+| ----------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | --------------------------------------------------------------------------------------- |
+| MULTISIG-THRESHOLD-001  | [test_MultiSig_cannotExecuteBelowThreshold](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigThresholdProperties.sol#L22)         | Transactions with approvals below threshold cannot be executed.                         |
+| MULTISIG-THRESHOLD-002  | [test_MultiSig_insufficientApprovalsNotExecuted](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigThresholdProperties.sol#L39)   | Transactions with insufficient approvals should not be executed.                        |
+| MULTISIG-THRESHOLD-003  | [test_MultiSig_thresholdNeverZero](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigThresholdProperties.sol#L56)                 | Threshold must always be at least 1.                                                    |
+| MULTISIG-THRESHOLD-004  | [test_MultiSig_thresholdNotAboveOwnerCount](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigThresholdProperties.sol#L66)        | Threshold cannot exceed the number of owners.                                           |
+| MULTISIG-THRESHOLD-005  | [test_MultiSig_thresholdChangeMaintainsOperability](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigThresholdProperties.sol#L77) | Threshold changes must maintain wallet operability (valid bounds).                      |
+| MULTISIG-THRESHOLD-006  | [test_MultiSig_approvalCountWithinBounds](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigThresholdProperties.sol#L94)          | Approval count cannot exceed total number of owners.                                    |
+
+### Signature and approval properties
+
+| ID                      | Name                                                                                                                                                                            | Invariant tested                                                                   |
+| ----------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ---------------------------------------------------------------------------------- |
+| MULTISIG-SIGNATURE-001  | [test_MultiSig_approvalsNotReusedAcrossTransactions](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigSignatureProperties.sol#L24) | Approvals for one transaction do not apply to other transactions.                 |
+| MULTISIG-SIGNATURE-002  | [test_MultiSig_executedTxApprovalsImmutable](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigSignatureProperties.sol#L42)         | Approval state for executed transactions should not change.                        |
+| MULTISIG-SIGNATURE-003  | [test_MultiSig_onlyOwnersCanApprove](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigSignatureProperties.sol#L67)                 | Only owners can have recorded approvals.                                           |
+| MULTISIG-SIGNATURE-004  | [test_MultiSig_approvalCountMatchesApprovals](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigSignatureProperties.sol#L79)        | Reported approval count must match actual number of owner approvals.               |
+| MULTISIG-SIGNATURE-005  | [test_MultiSig_approvalCountNeverDecreases](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigSignatureProperties.sol#L98)          | For pending transactions, approval count can only increase.                        |
+| MULTISIG-SIGNATURE-006  | [test_MultiSig_noDoubleApprovalCounting](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigSignatureProperties.sol#L115)            | Each owner can only approve once per transaction (no double-counting).             |
+| MULTISIG-SIGNATURE-007  | [test_MultiSig_zeroAddressCannotApprove](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigSignatureProperties.sol#L133)            | Zero address should never be recorded as having approved.                          |
+
+### Nonce properties
+
+| ID                  | Name                                                                                                                                                                      | Invariant tested                                                                    |
+| ------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ----------------------------------------------------------------------------------- |
+| MULTISIG-NONCE-001  | [test_MultiSig_nonceMonotonicallyIncreases](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigNonceProperties.sol#L25)        | Nonce strictly increases monotonically (never decreases, increases by 1).          |
+| MULTISIG-NONCE-002  | [test_MultiSig_nonceUsedOnlyOnce](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigNonceProperties.sol#L52)                 | Each nonce can only be used once.                                                   |
+| MULTISIG-NONCE-003  | [test_MultiSig_nonceIncrementsOnlyOnExecution](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigNonceProperties.sol#L72)    | Nonce only increments on successful transaction execution.                          |
+| MULTISIG-NONCE-004  | [test_MultiSig_oldNoncesRejected](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigNonceProperties.sol#L91)                 | Transactions with nonces less than current nonce should be rejected.                |
+| MULTISIG-NONCE-005  | [test_MultiSig_nonceStartsAtExpectedValue](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigNonceProperties.sol#L108)       | Current nonce must always be greater than or equal to initial nonce.                |
+| MULTISIG-NONCE-006  | [test_MultiSig_noNonceGaps](https://github.com/crytic/properties/blob/main/contracts/MultiSig/internal/properties/MultiSigNonceProperties.sol#L120)                      | All nonces from initial to current (exclusive) should be marked as used (no gaps). |
+
 ## ABDKMath64x64
 
 | ID           | Name                                                                                                                                                        | Invariant tested                                                                                       |

contracts/MultiSig/external/echidna.config.yaml

@@ -0,0 +1,7 @@
+coverage: true
+allContracts: true
+corpusDir: "corpus"
+testMode: assertion
+testLimit: 100000
+deployer: "0x10000"
+sender: ["0x10000", "0x20000", "0x30000"]

contracts/MultiSig/external/properties/MultiSigExternalBasicProperties.sol

@@ -0,0 +1,161 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+pragma solidity ^0.8.0;
+
+import "../util/MultiSigExternalTestBase.sol";
+
+/**
+ * @title CryticMultiSigExternalBasicProperties
+ * @notice Basic property tests for MultiSig wallets (external mode)
+ * @dev Contains fundamental invariants that should hold for any MultiSig wallet implementation
+ *      Tests through external interface only, treating the contract as a black box
+ */
+abstract contract CryticMultiSigExternalBasicProperties is CryticMultiSigExternalTestBase {
+    constructor() {}
+
+    ////////////////////////////////////////
+    // Properties
+
+    /**
+     * @notice MULTISIG-EXTERNAL-BASIC-051: Only owners can be valid approvers
+     * @dev Invariant: Any valid approval must come from an address that is an owner
+     */
+    function test_MultiSigExternal_onlyOwnersCanApprove(address addr) public {
+        // If address is not an owner, they should not be able to approve
+        if (!isOwner(addr)) {
+            // This property verifies that non-owners cannot approve
+            // Implementation-specific: MultiSig should revert or ignore non-owner approvals
+            assertWithMsg(
+                !isValidOwner(addr),
+                "Non-owner marked as valid owner"
+            );
+        }
+    }
+
+    /**
+     * @notice MULTISIG-EXTERNAL-BASIC-052: Threshold must be within valid bounds
+     * @dev Invariant: 0 < threshold <= owner count at all times
+     */
+    function test_MultiSigExternal_thresholdWithinBounds() public {
+        uint256 threshold = getThreshold();
+        uint256 ownerCount = getOwnerCount();
+
+        assertGt(threshold, 0, "Threshold must be greater than zero");
+        assertLte(
+            threshold,
+            ownerCount,
+            "Threshold cannot exceed owner count"
+        );
+    }
+
+    /**
+     * @notice MULTISIG-EXTERNAL-BASIC-053: No owner can be the zero address
+     * @dev Invariant: All addresses in the owners list must be non-zero
+     */
+    function test_MultiSigExternal_noZeroAddressOwners() public {
+        address[] memory owners = getOwners();
+
+        for (uint256 i = 0; i < owners.length; i++) {
+            assertWithMsg(
+                owners[i] != address(0),
+                "Owner list contains zero address"
+            );
+        }
+    }
+
+    /**
+     * @notice MULTISIG-EXTERNAL-BASIC-054: Owner count must be at least equal to threshold
+     * @dev Invariant: There must be enough owners to meet the threshold requirement
+     */
+    function test_MultiSigExternal_ownerCountMeetsThreshold() public {
+        uint256 threshold = getThreshold();
+        uint256 ownerCount = getOwnerCount();
+
+        assertGte(
+            ownerCount,
+            threshold,
+            "Owner count below threshold requirement"
+        );
+    }
+
+    /**
+     * @notice MULTISIG-EXTERNAL-BASIC-055: Owner list must not be empty
+     * @dev Invariant: MultiSig must always have at least one owner
+     */
+    function test_MultiSigExternal_ownerListNotEmpty() public {
+        uint256 ownerCount = getOwnerCount();
+
+        assertGt(ownerCount, 0, "Owner list is empty");
+    }
+
+    /**
+     * @notice MULTISIG-EXTERNAL-BASIC-056: Executed transactions cannot be executed again
+     * @dev Invariant: Once a transaction is marked as executed, it should remain executed
+     * @param txHash Transaction identifier
+     */
+    function test_MultiSigExternal_executedTransactionsStayExecuted(bytes32 txHash) public {
+        // If a transaction was previously marked as executed, it must still be executed
+        if (executedTransactions[txHash]) {
+            assertWithMsg(
+                isExecuted(txHash),
+                "Previously executed transaction no longer marked as executed"
+            );
+        }
+
+        // Update our tracking if transaction is newly executed
+        if (isExecuted(txHash)) {
+            executedTransactions[txHash] = true;
+        }
+    }
+
+    /**
+     * @notice MULTISIG-EXTERNAL-BASIC-057: isOwner consistency with owner list
+     * @dev Invariant: If isOwner returns true, address must be in the owners list
+     * @param addr Address to check
+     */
+    function test_MultiSigExternal_isOwnerConsistentWithOwnerList(address addr) public {
+        address[] memory owners = getOwners();
+        bool foundInList = false;
+
+        for (uint256 i = 0; i < owners.length; i++) {
+            if (owners[i] == addr) {
+                foundInList = true;
+                break;
+            }
+        }
+
+        bool isOwnerResult = isOwner(addr);
+
+        // If isOwner returns true, must be in list
+        if (isOwnerResult) {
+            assertWithMsg(
+                foundInList,
+                "isOwner returns true but address not in owner list"
+            );
+        }
+
+        // If in list, isOwner should return true
+        if (foundInList) {
+            assertWithMsg(
+                isOwnerResult,
+                "Address in owner list but isOwner returns false"
+            );
+        }
+    }
+
+    /**
+     * @notice MULTISIG-EXTERNAL-BASIC-058: No duplicate owners in owner list
+     * @dev Invariant: Each address should appear at most once in the owners list
+     */
+    function test_MultiSigExternal_noDuplicateOwners() public {
+        address[] memory owners = getOwners();
+
+        for (uint256 i = 0; i < owners.length; i++) {
+            for (uint256 j = i + 1; j < owners.length; j++) {
+                assertWithMsg(
+                    owners[i] != owners[j],
+                    "Duplicate owner found in owner list"
+                );
+            }
+        }
+    }
+}