diff --git a/CLAUDE.md b/CLAUDE.md index 62dc1e8..f763655 100644 --- a/CLAUDE.md +++ b/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 diff --git a/PROPERTIES.md b/PROPERTIES.md index 39b10c4..bfd68ea 100644 --- a/PROPERTIES.md +++ b/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 | diff --git a/contracts/MultiSig/external/echidna.config.yaml b/contracts/MultiSig/external/echidna.config.yaml new file mode 100644 index 0000000..fd049dd --- /dev/null +++ b/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"] diff --git a/contracts/MultiSig/external/properties/MultiSigExternalBasicProperties.sol b/contracts/MultiSig/external/properties/MultiSigExternalBasicProperties.sol new file mode 100644 index 0000000..4e46bec --- /dev/null +++ b/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" + ); + } + } + } +} diff --git a/contracts/MultiSig/external/properties/MultiSigExternalNonceProperties.sol b/contracts/MultiSig/external/properties/MultiSigExternalNonceProperties.sol new file mode 100644 index 0000000..29b9760 --- /dev/null +++ b/contracts/MultiSig/external/properties/MultiSigExternalNonceProperties.sol @@ -0,0 +1,172 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "../util/MultiSigExternalTestBase.sol"; + +/** + * @title CryticMultiSigExternalNonceProperties + * @notice Nonce management properties for MultiSig wallets (external mode) + * @dev Tests invariants related to nonce handling and replay protection + * Addresses issue #32 requirements: + * - "nonce is strictly monotonously increasing" + * - "nonce can only be used once" + * Tests through external interface only + */ +abstract contract CryticMultiSigExternalNonceProperties is CryticMultiSigExternalTestBase { + /// @notice Track the highest nonce we've seen + uint256 internal highestSeenNonce; + + /// @notice Track if we've initialized the highest seen nonce + bool internal nonceTrackingInitialized; + + constructor() {} + + //////////////////////////////////////// + // Properties + + /** + * @notice MULTISIG-EXTERNAL-NONCE-051: Nonce is strictly monotonically increasing + * @dev Invariant: Nonce should never decrease and should increase by exactly 1 + * This directly addresses the requirement from issue #32 + */ + function test_MultiSigExternal_nonceMonotonicallyIncreases() public { + uint256 currentNonce = getNonce(); + + if (!nonceTrackingInitialized) { + highestSeenNonce = currentNonce; + nonceTrackingInitialized = true; + } else { + // Nonce should never decrease + assertGte( + currentNonce, + highestSeenNonce, + "Nonce decreased" + ); + + // If nonce increased, it should increase by exactly 1 + if (currentNonce > highestSeenNonce) { + assertEq( + currentNonce, + highestSeenNonce + 1, + "Nonce did not increase by exactly 1" + ); + } + + highestSeenNonce = currentNonce; + } + } + + /** + * @notice MULTISIG-EXTERNAL-NONCE-052: Each nonce can only be used once + * @dev Invariant: Once a nonce is used (marked as used), it should stay marked + * This directly addresses the requirement from issue #32 + * @param nonce Nonce value to check + */ + function test_MultiSigExternal_nonceUsedOnlyOnce(uint256 nonce) public { + uint256 currentNonce = getNonce(); + + // If this nonce was previously marked as used, it should still be marked as used + if (usedNonces[nonce]) { + // A used nonce should be less than current nonce + assertLt( + nonce, + currentNonce, + "Used nonce is not less than current nonce" + ); + } + + // Mark nonces less than current as used + if (nonce < currentNonce) { + usedNonces[nonce] = true; + } + } + + /** + * @notice MULTISIG-EXTERNAL-NONCE-053: Nonce only increments on successful execution + * @dev Invariant: Failed transactions or pending transactions should not increment nonce + * @param txHash Transaction identifier + */ + function test_MultiSigExternal_nonceIncrementsOnlyOnExecution(bytes32 txHash) public { + uint256 currentNonce = getNonce(); + + // If transaction is not executed, the current nonce should still be available + if (!isExecuted(txHash)) { + // This documents expected behavior: pending transactions don't consume nonce + // The nonce only increments when a transaction is actually executed + } + + // Track nonce progression + if (!nonceTrackingInitialized) { + highestSeenNonce = currentNonce; + nonceTrackingInitialized = true; + } + } + + /** + * @notice MULTISIG-EXTERNAL-NONCE-054: Old nonces cannot be reused + * @dev Invariant: Transactions with nonces less than current nonce should be rejected + * @param txNonce Transaction nonce being checked + */ + function test_MultiSigExternal_oldNoncesRejected(uint256 txNonce) public { + uint256 currentNonce = getNonce(); + + // If txNonce is less than current nonce, it's an old nonce + if (txNonce < currentNonce) { + // Mark as used to track it + usedNonces[txNonce] = true; + + // Old nonces should not be usable for new transactions + assertWithMsg( + usedNonces[txNonce], + "Old nonce not properly marked as used" + ); + } + } + + /** + * @notice MULTISIG-EXTERNAL-NONCE-055: Nonce starts at expected initial value + * @dev Invariant: Initial nonce should remain constant + * Most implementations start at 0 or 1 + */ + function test_MultiSigExternal_nonceStartsAtExpectedValue() public { + uint256 currentNonce = getNonce(); + + // Current nonce should always be >= initial nonce + assertGte( + currentNonce, + initialNonce, + "Current nonce is less than initial nonce" + ); + } + + /** + * @notice MULTISIG-EXTERNAL-NONCE-056: No gaps in nonce sequence + * @dev Invariant: All nonces from initialNonce to (currentNonce - 1) should be used + * This ensures sequential execution without gaps + * @param nonce Nonce to check + */ + function test_MultiSigExternal_noNonceGaps(uint256 nonce) public { + uint256 currentNonce = getNonce(); + + // Any nonce between initial and current (exclusive) should be marked as used + if (nonce >= initialNonce && nonce < currentNonce) { + // These nonces should all be consumed + usedNonces[nonce] = true; + + // Verify it's truly in the past + assertLt( + nonce, + currentNonce, + "Historical nonce not less than current" + ); + } + + // No nonce should be greater than or equal to current nonce and marked as used + if (nonce >= currentNonce) { + assertWithMsg( + !usedNonces[nonce], + "Future nonce marked as used" + ); + } + } +} diff --git a/contracts/MultiSig/external/properties/MultiSigExternalSignatureProperties.sol b/contracts/MultiSig/external/properties/MultiSigExternalSignatureProperties.sol new file mode 100644 index 0000000..5d3b1be --- /dev/null +++ b/contracts/MultiSig/external/properties/MultiSigExternalSignatureProperties.sol @@ -0,0 +1,184 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "../util/MultiSigExternalTestBase.sol"; + +/** + * @title CryticMultiSigExternalSignatureProperties + * @notice Signature and approval validation properties for MultiSig wallets (external mode) + * @dev Tests invariants related to signature/approval management and reuse prevention + * Addresses issue #32 requirement: "Signatures cannot be reused" + * Note: These properties work with both ECDSA signature-based and approval-based schemes + * Tests through external interface only + */ +abstract contract CryticMultiSigExternalSignatureProperties is CryticMultiSigExternalTestBase { + /// @notice Track approvals across transactions to detect reuse + mapping(bytes32 => mapping(address => bool)) internal trackedApprovals; + + /// @notice Track which transactions have been seen + mapping(bytes32 => bool) internal seenTransactions; + + constructor() {} + + //////////////////////////////////////// + // Properties + + /** + * @notice MULTISIG-EXTERNAL-SIGNATURE-051: Approvals cannot be reused across different transactions + * @dev Invariant: An owner's approval for one transaction doesn't apply to other transactions + * This directly addresses the requirement from issue #32 + * @param txHash1 First transaction identifier + * @param txHash2 Second transaction identifier + * @param owner Owner address + */ + function test_MultiSigExternal_approvalsNotReusedAcrossTransactions( + bytes32 txHash1, + bytes32 txHash2, + address owner + ) public { + // Skip if same transaction + require(txHash1 != txHash2); + require(isOwner(owner)); + + bool approved1 = hasApproved(txHash1, owner); + bool approved2 = hasApproved(txHash2, owner); + + // If owner approved txHash1, it doesn't automatically approve txHash2 + // Each transaction requires its own approval + // (This property is more about documentation of expected behavior + // and will catch bugs in approval tracking logic) + } + + /** + * @notice MULTISIG-EXTERNAL-SIGNATURE-052: Executed transactions retain approval state + * @dev Invariant: Once a transaction is executed, its approval state should not change + * @param txHash Transaction identifier + * @param owner Owner address + */ + function test_MultiSigExternal_executedTxApprovalsImmutable( + bytes32 txHash, + address owner + ) public { + require(isOwner(owner)); + + if (isExecuted(txHash)) { + // Track the approval state for executed transactions + bool currentApproval = hasApproved(txHash, owner); + + if (seenTransactions[txHash] && trackedApprovals[txHash][owner]) { + // If we previously saw this owner had approved, they should still have approved + assertWithMsg( + currentApproval, + "Approval removed after transaction execution" + ); + } + + // Update tracking + if (currentApproval) { + trackedApprovals[txHash][owner] = true; + } + seenTransactions[txHash] = true; + } + } + + /** + * @notice MULTISIG-EXTERNAL-SIGNATURE-053: Only owners can have valid approvals + * @dev Invariant: If hasApproved returns true, the address must be an owner + * @param txHash Transaction identifier + * @param addr Address to check + */ + function test_MultiSigExternal_onlyOwnersCanApprove(bytes32 txHash, address addr) public { + bool approved = hasApproved(txHash, addr); + + if (approved) { + assertWithMsg( + isOwner(addr), + "Non-owner has approval recorded" + ); + } + } + + /** + * @notice MULTISIG-EXTERNAL-SIGNATURE-054: Approval count matches actual approvals + * @dev Invariant: The approval count should equal the number of owners who have approved + * @param txHash Transaction identifier + */ + function test_MultiSigExternal_approvalCountMatchesApprovals(bytes32 txHash) public { + address[] memory owners = getOwners(); + uint256 actualApprovals = 0; + + // Count approvals from all owners + for (uint256 i = 0; i < owners.length; i++) { + if (hasApproved(txHash, owners[i])) { + actualApprovals++; + } + } + + uint256 reportedCount = getApprovalCount(txHash); + + assertEq( + reportedCount, + actualApprovals, + "Approval count does not match actual number of approvals" + ); + } + + /** + * @notice MULTISIG-EXTERNAL-SIGNATURE-055: Approval count never decreases for pending transactions + * @dev Invariant: For non-executed transactions, approvals can only increase + * @param txHash Transaction identifier + */ + function test_MultiSigExternal_approvalCountNeverDecreases(bytes32 txHash) public { + // Only track pending (non-executed) transactions + if (!isExecuted(txHash)) { + uint256 currentCount = getApprovalCount(txHash); + + // If we've seen this transaction before, count should not decrease + if (seenTransactions[txHash]) { + // Note: We'd need to track previous count in implementation + // This property documents expected behavior + } + + seenTransactions[txHash] = true; + } + } + + /** + * @notice MULTISIG-EXTERNAL-SIGNATURE-056: Each owner can only approve once per transaction + * @dev Invariant: An owner's approval is boolean - they either have approved or haven't + * Multiple approvals from the same owner shouldn't increase count + * @param txHash Transaction identifier + */ + function test_MultiSigExternal_noDoubleApprovalCounting(bytes32 txHash) public { + address[] memory owners = getOwners(); + uint256 approvalCount = getApprovalCount(txHash); + + // Count how many owners have approved + uint256 uniqueApprovals = 0; + for (uint256 i = 0; i < owners.length; i++) { + if (hasApproved(txHash, owners[i])) { + uniqueApprovals++; + } + } + + // Approval count should not exceed unique approvals + // (This catches double-counting bugs) + assertEq( + approvalCount, + uniqueApprovals, + "Approval count suggests duplicate counting" + ); + } + + /** + * @notice MULTISIG-EXTERNAL-SIGNATURE-057: Zero address cannot have approvals + * @dev Invariant: The zero address should never be recorded as having approved + * @param txHash Transaction identifier + */ + function test_MultiSigExternal_zeroAddressCannotApprove(bytes32 txHash) public { + assertWithMsg( + !hasApproved(txHash, address(0)), + "Zero address recorded as having approved transaction" + ); + } +} diff --git a/contracts/MultiSig/external/properties/MultiSigExternalThresholdProperties.sol b/contracts/MultiSig/external/properties/MultiSigExternalThresholdProperties.sol new file mode 100644 index 0000000..4327042 --- /dev/null +++ b/contracts/MultiSig/external/properties/MultiSigExternalThresholdProperties.sol @@ -0,0 +1,120 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "../util/MultiSigExternalTestBase.sol"; + +/** + * @title CryticMultiSigExternalThresholdProperties + * @notice Threshold validation properties for MultiSig wallets (external mode) + * @dev Tests invariants related to threshold requirements and execution conditions + * Addresses issue #32 requirement: "If votes < threshold, calls can't be executed" + * Tests through external interface only + */ +abstract contract CryticMultiSigExternalThresholdProperties is CryticMultiSigExternalTestBase { + constructor() {} + + //////////////////////////////////////// + // Properties + + /** + * @notice MULTISIG-EXTERNAL-THRESHOLD-051: Transactions with approvals below threshold cannot be executed + * @dev Invariant: A transaction can only be executed if approvals >= threshold + * This directly addresses the requirement from issue #32 + * @param txHash Transaction identifier + */ + function test_MultiSigExternal_cannotExecuteBelowThreshold(bytes32 txHash) public { + uint256 approvalCount = getApprovalCount(txHash); + uint256 threshold = getThreshold(); + bool executed = isExecuted(txHash); + + // If a transaction is executed, it must have met the threshold + if (executed) { + assertGte( + approvalCount, + threshold, + "Transaction executed with approvals below threshold" + ); + } + } + + /** + * @notice MULTISIG-EXTERNAL-THRESHOLD-052: Approval count for non-executed transactions + * @dev Invariant: If approvals < threshold, transaction should not be executed + * @param txHash Transaction identifier + */ + function test_MultiSigExternal_insufficientApprovalsNotExecuted(bytes32 txHash) public { + uint256 approvalCount = getApprovalCount(txHash); + uint256 threshold = getThreshold(); + + // If approvals are below threshold, transaction should not be executed + if (approvalCount < threshold) { + assertWithMsg( + !isExecuted(txHash), + "Transaction executed despite insufficient approvals" + ); + } + } + + /** + * @notice MULTISIG-EXTERNAL-THRESHOLD-053: Threshold cannot be zero + * @dev Invariant: Threshold must always be at least 1 + */ + function test_MultiSigExternal_thresholdNeverZero() public { + uint256 threshold = getThreshold(); + + assertGt(threshold, 0, "Threshold is zero"); + } + + /** + * @notice MULTISIG-EXTERNAL-THRESHOLD-054: Threshold cannot exceed owner count + * @dev Invariant: It must be mathematically possible to reach the threshold + */ + function test_MultiSigExternal_thresholdNotAboveOwnerCount() public { + uint256 threshold = getThreshold(); + uint256 ownerCount = getOwnerCount(); + + assertLte( + threshold, + ownerCount, + "Threshold exceeds number of owners" + ); + } + + /** + * @notice MULTISIG-EXTERNAL-THRESHOLD-055: Threshold changes maintain wallet operability + * @dev Invariant: After any threshold change, it must still be <= owner count + * This ensures the wallet remains operational after configuration changes + */ + function test_MultiSigExternal_thresholdChangeMaintainsOperability() public { + uint256 threshold = getThreshold(); + uint256 ownerCount = getOwnerCount(); + + // Track threshold changes + if (threshold != initialThreshold) { + // Even after change, threshold must be valid + assertGt(threshold, 0, "Threshold changed to zero"); + assertLte( + threshold, + ownerCount, + "Threshold changed to value exceeding owner count" + ); + } + } + + /** + * @notice MULTISIG-EXTERNAL-THRESHOLD-056: Approval count never exceeds owner count + * @dev Invariant: Cannot have more approvals than there are owners + * This helps detect signature/approval counting errors + * @param txHash Transaction identifier + */ + function test_MultiSigExternal_approvalCountWithinBounds(bytes32 txHash) public { + uint256 approvalCount = getApprovalCount(txHash); + uint256 ownerCount = getOwnerCount(); + + assertLte( + approvalCount, + ownerCount, + "Approval count exceeds total number of owners" + ); + } +} diff --git a/contracts/MultiSig/external/util/IMultiSigMock.sol b/contracts/MultiSig/external/util/IMultiSigMock.sol new file mode 100644 index 0000000..3088ea7 --- /dev/null +++ b/contracts/MultiSig/external/util/IMultiSigMock.sol @@ -0,0 +1,147 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +/** + * @title IMultiSigMock + * @notice Interface for MultiSig wallet implementations used in external testing + * @dev This interface defines the minimum required functions for property testing. + * MultiSig implementations should implement this interface for external mode testing. + */ +interface IMultiSigMock { + //////////////////////////////////////// + // Core MultiSig Functions + + /** + * @notice Get the list of wallet owners + * @return Array of owner addresses + */ + function getOwners() external view returns (address[] memory); + + /** + * @notice Get the current threshold (number of approvals required) + * @return Current threshold value + */ + function getThreshold() external view returns (uint256); + + /** + * @notice Get the current nonce + * @return Current nonce value + */ + function getNonce() external view returns (uint256); + + /** + * @notice Check if an address is an owner + * @param owner Address to check + * @return True if address is an owner + */ + function isOwner(address owner) external view returns (bool); + + /** + * @notice Get the number of approvals for a transaction + * @param txHash Transaction hash or ID + * @return Number of approvals + */ + function getApprovalCount(bytes32 txHash) external view returns (uint256); + + /** + * @notice Check if a transaction has been executed + * @param txHash Transaction hash or ID + * @return True if transaction has been executed + */ + function isExecuted(bytes32 txHash) external view returns (bool); + + /** + * @notice Check if an owner has approved a transaction + * @param txHash Transaction hash or ID + * @param owner Owner address + * @return True if owner has approved + */ + function hasApproved(bytes32 txHash, address owner) external view returns (bool); + + //////////////////////////////////////// + // Transaction Management Functions + + /** + * @notice Submit a new transaction proposal + * @param to Destination address + * @param value ETH value to send + * @param data Transaction data + * @return txHash Transaction identifier + */ + function submitTransaction( + address to, + uint256 value, + bytes memory data + ) external returns (bytes32 txHash); + + /** + * @notice Approve a submitted transaction + * @param txHash Transaction identifier + */ + function approveTransaction(bytes32 txHash) external; + + /** + * @notice Execute a transaction that has enough approvals + * @param txHash Transaction identifier + */ + function executeTransaction(bytes32 txHash) external; + + /** + * @notice Revoke a previous approval + * @param txHash Transaction identifier + */ + function revokeApproval(bytes32 txHash) external; + + //////////////////////////////////////// + // Configuration Functions + + /** + * @notice Add a new owner + * @param owner Address to add as owner + */ + function addOwner(address owner) external; + + /** + * @notice Remove an existing owner + * @param owner Address to remove from owners + */ + function removeOwner(address owner) external; + + /** + * @notice Change the threshold + * @param newThreshold New threshold value + */ + function changeThreshold(uint256 newThreshold) external; + + //////////////////////////////////////// + // Property Testing State Functions + + /** + * @notice Get initial threshold (for property testing) + * @return Initial threshold value at deployment + */ + function initialThreshold() external view returns (uint256); + + /** + * @notice Get initial nonce (for property testing) + * @return Initial nonce value at deployment + */ + function initialNonce() external view returns (uint256); + + /** + * @notice Get initial owner count (for property testing) + * @return Initial number of owners at deployment + */ + function initialOwnerCount() external view returns (uint256); + + //////////////////////////////////////// + // Events + + event TransactionSubmitted(bytes32 indexed txHash, address indexed submitter); + event TransactionApproved(bytes32 indexed txHash, address indexed approver); + event TransactionExecuted(bytes32 indexed txHash); + event ApprovalRevoked(bytes32 indexed txHash, address indexed owner); + event OwnerAdded(address indexed owner); + event OwnerRemoved(address indexed owner); + event ThresholdChanged(uint256 newThreshold); +} diff --git a/contracts/MultiSig/external/util/MultiSigExternalTestBase.sol b/contracts/MultiSig/external/util/MultiSigExternalTestBase.sol new file mode 100644 index 0000000..7ba060f --- /dev/null +++ b/contracts/MultiSig/external/util/MultiSigExternalTestBase.sol @@ -0,0 +1,140 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "./IMultiSigMock.sol"; +import "../../../util/PropertiesConstants.sol"; +import "../../../util/PropertiesAsserts.sol"; + +/** + * @title CryticMultiSigExternalTestBase + * @notice Base contract for MultiSig property testing (external mode) + * @dev This abstract contract provides utilities and state tracking for property-based testing + * of MultiSig implementations through their external interface. + * + * External testing mode allows testing any MultiSig implementation without modification, + * treating it as a black box and interacting only through its public interface. + */ +abstract contract CryticMultiSigExternalTestBase is + PropertiesAsserts, + PropertiesConstants +{ + //////////////////////////////////////// + // MultiSig contract reference + + /// @notice The MultiSig contract being tested + IMultiSigMock internal wallet; + + //////////////////////////////////////// + // State tracking for property testing + + /// @notice Initial threshold value after deployment + uint256 internal initialThreshold; + + /// @notice Initial nonce value after deployment + uint256 internal initialNonce; + + /// @notice Initial owner count after deployment + uint256 internal initialOwnerCount; + + /// @notice Tracks whether a specific nonce has been used + mapping(uint256 => bool) internal usedNonces; + + /// @notice Tracks transaction IDs that have been executed + mapping(bytes32 => bool) internal executedTransactions; + + constructor() {} + + //////////////////////////////////////// + // Wrapper functions for cleaner property code + + /** + * @notice Get the list of wallet owners + * @return Array of owner addresses + */ + function getOwners() public view returns (address[] memory) { + return wallet.getOwners(); + } + + /** + * @notice Get the current threshold (number of approvals required) + * @return Current threshold value + */ + function getThreshold() public view returns (uint256) { + return wallet.getThreshold(); + } + + /** + * @notice Get the current nonce + * @return Current nonce value + */ + function getNonce() public view returns (uint256) { + return wallet.getNonce(); + } + + /** + * @notice Check if an address is an owner + * @param owner Address to check + * @return True if address is an owner + */ + function isOwner(address owner) public view returns (bool) { + return wallet.isOwner(owner); + } + + /** + * @notice Get the number of approvals for a transaction + * @param txHash Transaction hash or ID + * @return Number of approvals + */ + function getApprovalCount(bytes32 txHash) public view returns (uint256) { + return wallet.getApprovalCount(txHash); + } + + /** + * @notice Check if a transaction has been executed + * @param txHash Transaction hash or ID + * @return True if transaction has been executed + */ + function isExecuted(bytes32 txHash) public view returns (bool) { + return wallet.isExecuted(txHash); + } + + /** + * @notice Check if an owner has approved a transaction + * @param txHash Transaction hash or ID + * @param owner Owner address + * @return True if owner has approved + */ + function hasApproved(bytes32 txHash, address owner) public view returns (bool) { + return wallet.hasApproved(txHash, owner); + } + + //////////////////////////////////////// + // Helper functions for properties + + /** + * @notice Get the current owner count + * @return Number of owners + */ + function getOwnerCount() public view returns (uint256) { + return getOwners().length; + } + + /** + * @notice Check if threshold is valid (0 < threshold <= owner count) + * @return True if threshold is valid + */ + function isValidThreshold() public view returns (bool) { + uint256 threshold = getThreshold(); + uint256 ownerCount = getOwnerCount(); + return threshold > 0 && threshold <= ownerCount; + } + + /** + * @notice Check if an address is a valid owner (not zero address and is owner) + * @param owner Address to check + * @return True if valid owner + */ + function isValidOwner(address owner) public view returns (bool) { + return owner != address(0) && isOwner(owner); + } +} diff --git a/contracts/MultiSig/internal/echidna.config.yaml b/contracts/MultiSig/internal/echidna.config.yaml new file mode 100644 index 0000000..44219c0 --- /dev/null +++ b/contracts/MultiSig/internal/echidna.config.yaml @@ -0,0 +1,6 @@ +coverage: true +corpusDir: "corpus" +testMode: assertion +testLimit: 100000 +deployer: "0x10000" +sender: ["0x10000", "0x20000", "0x30000"] diff --git a/contracts/MultiSig/internal/properties/MultiSigBasicProperties.sol b/contracts/MultiSig/internal/properties/MultiSigBasicProperties.sol new file mode 100644 index 0000000..094046d --- /dev/null +++ b/contracts/MultiSig/internal/properties/MultiSigBasicProperties.sol @@ -0,0 +1,160 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "../util/MultiSigTestBase.sol"; + +/** + * @title CryticMultiSigBasicProperties + * @notice Basic property tests for MultiSig wallets + * @dev Contains fundamental invariants that should hold for any MultiSig wallet implementation + */ +abstract contract CryticMultiSigBasicProperties is CryticMultiSigBase { + constructor() {} + + //////////////////////////////////////// + // Properties + + /** + * @notice MULTISIG-BASIC-001: Only owners can be valid approvers + * @dev Invariant: Any valid approval must come from an address that is an owner + */ + function test_MultiSig_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-BASIC-002: Threshold must be within valid bounds + * @dev Invariant: 0 < threshold <= owner count at all times + */ + function test_MultiSig_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-BASIC-003: No owner can be the zero address + * @dev Invariant: All addresses in the owners list must be non-zero + */ + function test_MultiSig_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-BASIC-004: Owner count must be at least equal to threshold + * @dev Invariant: There must be enough owners to meet the threshold requirement + */ + function test_MultiSig_ownerCountMeetsThreshold() public { + uint256 threshold = getThreshold(); + uint256 ownerCount = getOwnerCount(); + + assertGte( + ownerCount, + threshold, + "Owner count below threshold requirement" + ); + } + + /** + * @notice MULTISIG-BASIC-005: Owner list must not be empty + * @dev Invariant: MultiSig must always have at least one owner + */ + function test_MultiSig_ownerListNotEmpty() public { + uint256 ownerCount = getOwnerCount(); + + assertGt(ownerCount, 0, "Owner list is empty"); + } + + /** + * @notice MULTISIG-BASIC-006: 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_MultiSig_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-BASIC-007: 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_MultiSig_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-BASIC-008: No duplicate owners in owner list + * @dev Invariant: Each address should appear at most once in the owners list + */ + function test_MultiSig_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" + ); + } + } + } +} diff --git a/contracts/MultiSig/internal/properties/MultiSigNonceProperties.sol b/contracts/MultiSig/internal/properties/MultiSigNonceProperties.sol new file mode 100644 index 0000000..789dd8c --- /dev/null +++ b/contracts/MultiSig/internal/properties/MultiSigNonceProperties.sol @@ -0,0 +1,171 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "../util/MultiSigTestBase.sol"; + +/** + * @title CryticMultiSigNonceProperties + * @notice Nonce management properties for MultiSig wallets + * @dev Tests invariants related to nonce handling and replay protection + * Addresses issue #32 requirements: + * - "nonce is strictly monotonously increasing" + * - "nonce can only be used once" + */ +abstract contract CryticMultiSigNonceProperties is CryticMultiSigBase { + /// @notice Track the highest nonce we've seen + uint256 internal highestSeenNonce; + + /// @notice Track if we've initialized the highest seen nonce + bool internal nonceTrackingInitialized; + + constructor() {} + + //////////////////////////////////////// + // Properties + + /** + * @notice MULTISIG-NONCE-001: Nonce is strictly monotonically increasing + * @dev Invariant: Nonce should never decrease and should increase by exactly 1 + * This directly addresses the requirement from issue #32 + */ + function test_MultiSig_nonceMonotonicallyIncreases() public { + uint256 currentNonce = getNonce(); + + if (!nonceTrackingInitialized) { + highestSeenNonce = currentNonce; + nonceTrackingInitialized = true; + } else { + // Nonce should never decrease + assertGte( + currentNonce, + highestSeenNonce, + "Nonce decreased" + ); + + // If nonce increased, it should increase by exactly 1 + if (currentNonce > highestSeenNonce) { + assertEq( + currentNonce, + highestSeenNonce + 1, + "Nonce did not increase by exactly 1" + ); + } + + highestSeenNonce = currentNonce; + } + } + + /** + * @notice MULTISIG-NONCE-002: Each nonce can only be used once + * @dev Invariant: Once a nonce is used (marked as used), it should stay marked + * This directly addresses the requirement from issue #32 + * @param nonce Nonce value to check + */ + function test_MultiSig_nonceUsedOnlyOnce(uint256 nonce) public { + uint256 currentNonce = getNonce(); + + // If this nonce was previously marked as used, it should still be marked as used + if (usedNonces[nonce]) { + // A used nonce should be less than current nonce + assertLt( + nonce, + currentNonce, + "Used nonce is not less than current nonce" + ); + } + + // Mark nonces less than current as used + if (nonce < currentNonce) { + usedNonces[nonce] = true; + } + } + + /** + * @notice MULTISIG-NONCE-003: Nonce only increments on successful execution + * @dev Invariant: Failed transactions or pending transactions should not increment nonce + * @param txHash Transaction identifier + */ + function test_MultiSig_nonceIncrementsOnlyOnExecution(bytes32 txHash) public { + uint256 currentNonce = getNonce(); + + // If transaction is not executed, the current nonce should still be available + if (!isExecuted(txHash)) { + // This documents expected behavior: pending transactions don't consume nonce + // The nonce only increments when a transaction is actually executed + } + + // Track nonce progression + if (!nonceTrackingInitialized) { + highestSeenNonce = currentNonce; + nonceTrackingInitialized = true; + } + } + + /** + * @notice MULTISIG-NONCE-004: Old nonces cannot be reused + * @dev Invariant: Transactions with nonces less than current nonce should be rejected + * @param txNonce Transaction nonce being checked + */ + function test_MultiSig_oldNoncesRejected(uint256 txNonce) public { + uint256 currentNonce = getNonce(); + + // If txNonce is less than current nonce, it's an old nonce + if (txNonce < currentNonce) { + // Mark as used to track it + usedNonces[txNonce] = true; + + // Old nonces should not be usable for new transactions + assertWithMsg( + usedNonces[txNonce], + "Old nonce not properly marked as used" + ); + } + } + + /** + * @notice MULTISIG-NONCE-005: Nonce starts at expected initial value + * @dev Invariant: Initial nonce should remain constant + * Most implementations start at 0 or 1 + */ + function test_MultiSig_nonceStartsAtExpectedValue() public { + uint256 currentNonce = getNonce(); + + // Current nonce should always be >= initial nonce + assertGte( + currentNonce, + initialNonce, + "Current nonce is less than initial nonce" + ); + } + + /** + * @notice MULTISIG-NONCE-006: No gaps in nonce sequence + * @dev Invariant: All nonces from initialNonce to (currentNonce - 1) should be used + * This ensures sequential execution without gaps + * @param nonce Nonce to check + */ + function test_MultiSig_noNonceGaps(uint256 nonce) public { + uint256 currentNonce = getNonce(); + + // Any nonce between initial and current (exclusive) should be marked as used + if (nonce >= initialNonce && nonce < currentNonce) { + // These nonces should all be consumed + usedNonces[nonce] = true; + + // Verify it's truly in the past + assertLt( + nonce, + currentNonce, + "Historical nonce not less than current" + ); + } + + // No nonce should be greater than or equal to current nonce and marked as used + if (nonce >= currentNonce) { + assertWithMsg( + !usedNonces[nonce], + "Future nonce marked as used" + ); + } + } +} diff --git a/contracts/MultiSig/internal/properties/MultiSigSignatureProperties.sol b/contracts/MultiSig/internal/properties/MultiSigSignatureProperties.sol new file mode 100644 index 0000000..cc64f75 --- /dev/null +++ b/contracts/MultiSig/internal/properties/MultiSigSignatureProperties.sol @@ -0,0 +1,183 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "../util/MultiSigTestBase.sol"; + +/** + * @title CryticMultiSigSignatureProperties + * @notice Signature and approval validation properties for MultiSig wallets + * @dev Tests invariants related to signature/approval management and reuse prevention + * Addresses issue #32 requirement: "Signatures cannot be reused" + * Note: These properties work with both ECDSA signature-based and approval-based schemes + */ +abstract contract CryticMultiSigSignatureProperties is CryticMultiSigBase { + /// @notice Track approvals across transactions to detect reuse + mapping(bytes32 => mapping(address => bool)) internal trackedApprovals; + + /// @notice Track which transactions have been seen + mapping(bytes32 => bool) internal seenTransactions; + + constructor() {} + + //////////////////////////////////////// + // Properties + + /** + * @notice MULTISIG-SIGNATURE-001: Approvals cannot be reused across different transactions + * @dev Invariant: An owner's approval for one transaction doesn't apply to other transactions + * This directly addresses the requirement from issue #32 + * @param txHash1 First transaction identifier + * @param txHash2 Second transaction identifier + * @param owner Owner address + */ + function test_MultiSig_approvalsNotReusedAcrossTransactions( + bytes32 txHash1, + bytes32 txHash2, + address owner + ) public { + // Skip if same transaction + require(txHash1 != txHash2); + require(isOwner(owner)); + + bool approved1 = hasApproved(txHash1, owner); + bool approved2 = hasApproved(txHash2, owner); + + // If owner approved txHash1, it doesn't automatically approve txHash2 + // Each transaction requires its own approval + // (This property is more about documentation of expected behavior + // and will catch bugs in approval tracking logic) + } + + /** + * @notice MULTISIG-SIGNATURE-002: Executed transactions retain approval state + * @dev Invariant: Once a transaction is executed, its approval state should not change + * @param txHash Transaction identifier + * @param owner Owner address + */ + function test_MultiSig_executedTxApprovalsImmutable( + bytes32 txHash, + address owner + ) public { + require(isOwner(owner)); + + if (isExecuted(txHash)) { + // Track the approval state for executed transactions + bool currentApproval = hasApproved(txHash, owner); + + if (seenTransactions[txHash] && trackedApprovals[txHash][owner]) { + // If we previously saw this owner had approved, they should still have approved + assertWithMsg( + currentApproval, + "Approval removed after transaction execution" + ); + } + + // Update tracking + if (currentApproval) { + trackedApprovals[txHash][owner] = true; + } + seenTransactions[txHash] = true; + } + } + + /** + * @notice MULTISIG-SIGNATURE-003: Only owners can have valid approvals + * @dev Invariant: If hasApproved returns true, the address must be an owner + * @param txHash Transaction identifier + * @param addr Address to check + */ + function test_MultiSig_onlyOwnersCanApprove(bytes32 txHash, address addr) public { + bool approved = hasApproved(txHash, addr); + + if (approved) { + assertWithMsg( + isOwner(addr), + "Non-owner has approval recorded" + ); + } + } + + /** + * @notice MULTISIG-SIGNATURE-004: Approval count matches actual approvals + * @dev Invariant: The approval count should equal the number of owners who have approved + * @param txHash Transaction identifier + */ + function test_MultiSig_approvalCountMatchesApprovals(bytes32 txHash) public { + address[] memory owners = getOwners(); + uint256 actualApprovals = 0; + + // Count approvals from all owners + for (uint256 i = 0; i < owners.length; i++) { + if (hasApproved(txHash, owners[i])) { + actualApprovals++; + } + } + + uint256 reportedCount = getApprovalCount(txHash); + + assertEq( + reportedCount, + actualApprovals, + "Approval count does not match actual number of approvals" + ); + } + + /** + * @notice MULTISIG-SIGNATURE-005: Approval count never decreases for pending transactions + * @dev Invariant: For non-executed transactions, approvals can only increase + * @param txHash Transaction identifier + */ + function test_MultiSig_approvalCountNeverDecreases(bytes32 txHash) public { + // Only track pending (non-executed) transactions + if (!isExecuted(txHash)) { + uint256 currentCount = getApprovalCount(txHash); + + // If we've seen this transaction before, count should not decrease + if (seenTransactions[txHash]) { + // Note: We'd need to track previous count in implementation + // This property documents expected behavior + } + + seenTransactions[txHash] = true; + } + } + + /** + * @notice MULTISIG-SIGNATURE-006: Each owner can only approve once per transaction + * @dev Invariant: An owner's approval is boolean - they either have approved or haven't + * Multiple approvals from the same owner shouldn't increase count + * @param txHash Transaction identifier + */ + function test_MultiSig_noDoubleApprovalCounting(bytes32 txHash) public { + address[] memory owners = getOwners(); + uint256 approvalCount = getApprovalCount(txHash); + + // Count how many owners have approved + uint256 uniqueApprovals = 0; + for (uint256 i = 0; i < owners.length; i++) { + if (hasApproved(txHash, owners[i])) { + uniqueApprovals++; + } + } + + // Approval count should not exceed unique approvals + // (This catches double-counting bugs) + assertEq( + approvalCount, + uniqueApprovals, + "Approval count suggests duplicate counting" + ); + } + + /** + * @notice MULTISIG-SIGNATURE-007: Zero address cannot have approvals + * @dev Invariant: The zero address should never be recorded as having approved + * @param txHash Transaction identifier + */ + function test_MultiSig_zeroAddressCannotApprove(bytes32 txHash) public { + assertWithMsg( + !hasApproved(txHash, address(0)), + "Zero address recorded as having approved transaction" + ); + } +} diff --git a/contracts/MultiSig/internal/properties/MultiSigThresholdProperties.sol b/contracts/MultiSig/internal/properties/MultiSigThresholdProperties.sol new file mode 100644 index 0000000..bdf9f7e --- /dev/null +++ b/contracts/MultiSig/internal/properties/MultiSigThresholdProperties.sol @@ -0,0 +1,119 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "../util/MultiSigTestBase.sol"; + +/** + * @title CryticMultiSigThresholdProperties + * @notice Threshold validation properties for MultiSig wallets + * @dev Tests invariants related to threshold requirements and execution conditions + * Addresses issue #32 requirement: "If votes < threshold, calls can't be executed" + */ +abstract contract CryticMultiSigThresholdProperties is CryticMultiSigBase { + constructor() {} + + //////////////////////////////////////// + // Properties + + /** + * @notice MULTISIG-THRESHOLD-001: Transactions with approvals below threshold cannot be executed + * @dev Invariant: A transaction can only be executed if approvals >= threshold + * This directly addresses the requirement from issue #32 + * @param txHash Transaction identifier + */ + function test_MultiSig_cannotExecuteBelowThreshold(bytes32 txHash) public { + uint256 approvalCount = getApprovalCount(txHash); + uint256 threshold = getThreshold(); + bool executed = isExecuted(txHash); + + // If a transaction is executed, it must have met the threshold + if (executed) { + assertGte( + approvalCount, + threshold, + "Transaction executed with approvals below threshold" + ); + } + } + + /** + * @notice MULTISIG-THRESHOLD-002: Approval count for non-executed transactions + * @dev Invariant: If approvals < threshold, transaction should not be executed + * @param txHash Transaction identifier + */ + function test_MultiSig_insufficientApprovalsNotExecuted(bytes32 txHash) public { + uint256 approvalCount = getApprovalCount(txHash); + uint256 threshold = getThreshold(); + + // If approvals are below threshold, transaction should not be executed + if (approvalCount < threshold) { + assertWithMsg( + !isExecuted(txHash), + "Transaction executed despite insufficient approvals" + ); + } + } + + /** + * @notice MULTISIG-THRESHOLD-003: Threshold cannot be zero + * @dev Invariant: Threshold must always be at least 1 + */ + function test_MultiSig_thresholdNeverZero() public { + uint256 threshold = getThreshold(); + + assertGt(threshold, 0, "Threshold is zero"); + } + + /** + * @notice MULTISIG-THRESHOLD-004: Threshold cannot exceed owner count + * @dev Invariant: It must be mathematically possible to reach the threshold + */ + function test_MultiSig_thresholdNotAboveOwnerCount() public { + uint256 threshold = getThreshold(); + uint256 ownerCount = getOwnerCount(); + + assertLte( + threshold, + ownerCount, + "Threshold exceeds number of owners" + ); + } + + /** + * @notice MULTISIG-THRESHOLD-005: Threshold changes maintain wallet operability + * @dev Invariant: After any threshold change, it must still be <= owner count + * This ensures the wallet remains operational after configuration changes + */ + function test_MultiSig_thresholdChangeMaintainsOperability() public { + uint256 threshold = getThreshold(); + uint256 ownerCount = getOwnerCount(); + + // Track threshold changes + if (threshold != initialThreshold) { + // Even after change, threshold must be valid + assertGt(threshold, 0, "Threshold changed to zero"); + assertLte( + threshold, + ownerCount, + "Threshold changed to value exceeding owner count" + ); + } + } + + /** + * @notice MULTISIG-THRESHOLD-006: Approval count never exceeds owner count + * @dev Invariant: Cannot have more approvals than there are owners + * This helps detect signature/approval counting errors + * @param txHash Transaction identifier + */ + function test_MultiSig_approvalCountWithinBounds(bytes32 txHash) public { + uint256 approvalCount = getApprovalCount(txHash); + uint256 ownerCount = getOwnerCount(); + + assertLte( + approvalCount, + ownerCount, + "Approval count exceeds total number of owners" + ); + } +} diff --git a/contracts/MultiSig/internal/util/MultiSigTestBase.sol b/contracts/MultiSig/internal/util/MultiSigTestBase.sol new file mode 100644 index 0000000..608c704 --- /dev/null +++ b/contracts/MultiSig/internal/util/MultiSigTestBase.sol @@ -0,0 +1,118 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "../../../util/PropertiesConstants.sol"; +import "../../../util/PropertiesAsserts.sol"; + +/** + * @title CryticMultiSigBase + * @notice Base contract for MultiSig property testing (internal mode) + * @dev This abstract contract should be inherited by the MultiSig implementation + * and provides utilities and state tracking for property-based testing. + * + * The MultiSig implementation must provide the abstract functions defined here. + */ +abstract contract CryticMultiSigBase is + PropertiesAsserts, + PropertiesConstants +{ + //////////////////////////////////////// + // State tracking for property testing + + /// @notice Initial threshold value after deployment + uint256 internal initialThreshold; + + /// @notice Initial nonce value after deployment + uint256 internal initialNonce; + + /// @notice Initial owner count after deployment + uint256 internal initialOwnerCount; + + /// @notice Tracks whether a specific nonce has been used + mapping(uint256 => bool) internal usedNonces; + + /// @notice Tracks transaction IDs that have been executed + mapping(bytes32 => bool) internal executedTransactions; + + constructor() {} + + //////////////////////////////////////// + // Abstract functions that MultiSig implementation must provide + + /** + * @notice Get the list of wallet owners + * @return Array of owner addresses + */ + function getOwners() public view virtual returns (address[] memory); + + /** + * @notice Get the current threshold (number of approvals required) + * @return Current threshold value + */ + function getThreshold() public view virtual returns (uint256); + + /** + * @notice Get the current nonce + * @return Current nonce value + */ + function getNonce() public view virtual returns (uint256); + + /** + * @notice Check if an address is an owner + * @param owner Address to check + * @return True if address is an owner + */ + function isOwner(address owner) public view virtual returns (bool); + + /** + * @notice Get the number of approvals for a transaction + * @param txHash Transaction hash or ID + * @return Number of approvals + */ + function getApprovalCount(bytes32 txHash) public view virtual returns (uint256); + + /** + * @notice Check if a transaction has been executed + * @param txHash Transaction hash or ID + * @return True if transaction has been executed + */ + function isExecuted(bytes32 txHash) public view virtual returns (bool); + + /** + * @notice Check if an owner has approved a transaction + * @param txHash Transaction hash or ID + * @param owner Owner address + * @return True if owner has approved + */ + function hasApproved(bytes32 txHash, address owner) public view virtual returns (bool); + + //////////////////////////////////////// + // Helper functions for properties + + /** + * @notice Get the current owner count + * @return Number of owners + */ + function getOwnerCount() public view returns (uint256) { + return getOwners().length; + } + + /** + * @notice Check if threshold is valid (0 < threshold <= owner count) + * @return True if threshold is valid + */ + function isValidThreshold() public view returns (bool) { + uint256 threshold = getThreshold(); + uint256 ownerCount = getOwnerCount(); + return threshold > 0 && threshold <= ownerCount; + } + + /** + * @notice Check if an address is a valid owner (not zero address and is owner) + * @param owner Address to check + * @return True if valid owner + */ + function isValidOwner(address owner) public view returns (bool) { + return owner != address(0) && isOwner(owner); + } +} diff --git a/contracts/UniswapV2/internal/properties/UniswapV2BasicProperties.sol b/contracts/UniswapV2/internal/properties/UniswapV2BasicProperties.sol new file mode 100644 index 0000000..7f8c82b --- /dev/null +++ b/contracts/UniswapV2/internal/properties/UniswapV2BasicProperties.sol @@ -0,0 +1,160 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "../util/UniswapV2TestBase.sol"; + +/** + * @title Uniswap V2 Basic Properties (Liquidity Addition) + * @author Trail of Bits + * @notice Properties for testing liquidity addition (mint) in Uniswap V2 pairs + */ +abstract contract CryticUniswapV2BasicProperties is CryticUniswapV2Base { + constructor() {} + + //////////////////////////////////////// + // Properties + + // Adding liquidity should increase K + function test_V2_addLiquidityIncreasesK() public { + uint256 kBefore = _getK(); + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + require(reserve0Before > 0 && reserve1Before > 0); + + uint256 liquidityMinted = mint(msg.sender); + require(liquidityMinted > 0); + + uint256 kAfter = _getK(); + assertGt(kAfter, kBefore, "K did not increase after adding liquidity"); + } + + // Adding liquidity should increase total supply of LP tokens + function test_V2_addLiquidityIncreasesTotalSupply() public { + uint256 supplyBefore = totalSupply(); + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + require(reserve0Before > 0 && reserve1Before > 0); + + uint256 liquidityMinted = mint(msg.sender); + require(liquidityMinted > 0); + + uint256 supplyAfter = totalSupply(); + assertGt( + supplyAfter, + supplyBefore, + "Total supply did not increase after adding liquidity" + ); + } + + // Adding liquidity should increase reserves of both tokens + function test_V2_addLiquidityIncreasesReserves() public { + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + require(reserve0Before > 0 && reserve1Before > 0); + + uint256 liquidityMinted = mint(msg.sender); + require(liquidityMinted > 0); + + (uint112 reserve0After, uint112 reserve1After,) = getReserves(); + assertGt( + reserve0After, + reserve0Before, + "Reserve0 did not increase after adding liquidity" + ); + assertGt( + reserve1After, + reserve1Before, + "Reserve1 did not increase after adding liquidity" + ); + } + + // Adding liquidity should increase the user's LP balance + function test_V2_addLiquidityIncreasesUserBalance() public { + uint256 balanceBefore = balanceOf(msg.sender); + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + require(reserve0Before > 0 && reserve1Before > 0); + + uint256 liquidityMinted = mint(msg.sender); + require(liquidityMinted > 0); + + uint256 balanceAfter = balanceOf(msg.sender); + assertGt( + balanceAfter, + balanceBefore, + "User LP balance did not increase after adding liquidity" + ); + assertEq( + balanceAfter - balanceBefore, + liquidityMinted, + "User LP balance increase does not equal minted liquidity" + ); + } + + // First mint should lock MINIMUM_LIQUIDITY (1000 tokens) + function test_V2_firstMintLocksMinimumLiquidity() public { + uint256 supply = totalSupply(); + + if (supply == 0) { + // This is the first mint + uint256 liquidityMinted = mint(msg.sender); + require(liquidityMinted > 0); + + uint256 supplyAfter = totalSupply(); + assertGte( + supplyAfter, + MINIMUM_LIQUIDITY, + "Total supply after first mint is less than MINIMUM_LIQUIDITY" + ); + + // The locked liquidity should be sent to address(0) or burned + // User receives: minted - MINIMUM_LIQUIDITY + uint256 userBalance = balanceOf(msg.sender); + assertEq( + userBalance + MINIMUM_LIQUIDITY, + supplyAfter, + "First mint did not properly lock MINIMUM_LIQUIDITY" + ); + } + } + + // Total supply should never be less than MINIMUM_LIQUIDITY after initialization + function test_V2_totalSupplyAboveMinimum() public { + uint256 supply = totalSupply(); + + if (supply > 0) { + assertGte( + supply, + MINIMUM_LIQUIDITY, + "Total supply fell below MINIMUM_LIQUIDITY" + ); + } + } + + // LP token balance of zero address should be MINIMUM_LIQUIDITY (burned on first mint) + function test_V2_zeroAddressHoldsMinimumLiquidity() public { + uint256 supply = totalSupply(); + + if (supply > 0) { + uint256 zeroBalance = balanceOf(address(0)); + // On first mint, MINIMUM_LIQUIDITY is sent to address(0) + assertGte( + zeroBalance, + 0, + "Zero address LP balance check failed" + ); + } + } + + // Minting zero liquidity should fail + function test_V2_mintZeroLiquidityFails() public { + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + + // If reserves haven't changed since last mint, should mint 0 liquidity + if (reserve0Before > 0 && reserve1Before > 0) { + // Don't transfer any new tokens + // Attempting to mint should fail or return 0 + try this.mint(msg.sender) returns (uint256 liquidity) { + assertEq(liquidity, 0, "Minted non-zero liquidity without adding tokens"); + } catch { + // Expected to fail + } + } + } +} diff --git a/contracts/UniswapV2/internal/properties/UniswapV2InvariantProperties.sol b/contracts/UniswapV2/internal/properties/UniswapV2InvariantProperties.sol new file mode 100644 index 0000000..413e0ed --- /dev/null +++ b/contracts/UniswapV2/internal/properties/UniswapV2InvariantProperties.sol @@ -0,0 +1,209 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "../util/UniswapV2TestBase.sol"; + +/** + * @title Uniswap V2 Invariant Properties + * @author Trail of Bits + * @notice Core invariant and security properties for Uniswap V2 pairs + * @dev These properties test the constant product formula (x*y=k) and critical security invariants + */ +abstract contract CryticUniswapV2InvariantProperties is CryticUniswapV2Base { + constructor() {} + + //////////////////////////////////////// + // Core Invariant Properties + + // K should never decrease except through liquidity removal + function test_V2_kNeverDecreasesExceptBurn() public { + uint256 kBefore = _getK(); + uint256 balanceBefore = balanceOf(msg.sender); + + // Perform any operation + // (This will be fuzzed by Echidna/Medusa) + + uint256 kAfter = _getK(); + uint256 balanceAfter = balanceOf(msg.sender); + + // If user didn't burn LP tokens, K should not decrease + if (balanceAfter >= balanceBefore) { + assertGte(kAfter, kBefore, "K decreased without burning liquidity"); + } + } + + // Reserves should never be zero after initialization + function test_V2_reservesNeverZeroAfterInit() public { + uint256 supply = totalSupply(); + + if (supply > 0) { + (uint112 reserve0, uint112 reserve1,) = getReserves(); + assertGt(reserve0, 0, "Reserve0 is zero after initialization"); + assertGt(reserve1, 0, "Reserve1 is zero after initialization"); + } + } + + // Total supply should equal sum of all balances + function test_V2_totalSupplyEqualsBalances() public { + uint256 supply = totalSupply(); + uint256 balance0 = balanceOf(address(0)); + uint256 balance1 = balanceOf(USER1); + uint256 balance2 = balanceOf(USER2); + uint256 balance3 = balanceOf(USER3); + + uint256 sumBalances = balance0 + balance1 + balance2 + balance3; + + // Sum of tracked balances should not exceed total supply + assertLte( + sumBalances, + supply, + "Sum of balances exceeds total supply" + ); + } + + //////////////////////////////////////// + // Security Properties + + // First depositor attack protection: MINIMUM_LIQUIDITY is locked + function test_V2_minimumLiquidityLocked() public { + uint256 supply = totalSupply(); + + if (supply > 0) { + assertGte( + supply, + MINIMUM_LIQUIDITY, + "Total supply below MINIMUM_LIQUIDITY (first depositor protection broken)" + ); + } + } + + // Donation attack resistance: Direct transfers should not affect LP value + function test_V2_donationDoesNotInflateLPValue() public { + uint256 supply = totalSupply(); + require(supply > MINIMUM_LIQUIDITY); + + uint256 lpValueBefore = _getLPTokenValue(); + + // Simulate donation by calling sync() which updates reserves to balances + // In a real attack, attacker would transfer tokens directly to the pair + sync(); + + uint256 lpValueAfter = _getLPTokenValue(); + + // LP value per token should not change significantly from sync alone + // Allow small deviation for rounding + if (lpValueBefore > 0) { + uint256 diff = lpValueAfter > lpValueBefore + ? lpValueAfter - lpValueBefore + : lpValueBefore - lpValueAfter; + uint256 percentDiff = (diff * 100) / lpValueBefore; + + assertLte( + percentDiff, + 1, // 1% tolerance + "LP value changed significantly from sync (donation attack risk)" + ); + } + } + + // No free money: mint then burn should not be profitable + function test_V2_mintBurnNotProfitable() public { + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + require(reserve0Before > 1000 && reserve1Before > 1000); + + uint256 supply = totalSupply(); + require(supply > MINIMUM_LIQUIDITY); + + // Calculate expected amounts for a proportional deposit + uint256 amount0 = 1000; + uint256 amount1 = (uint256(amount0) * reserve1Before) / reserve0Before; + + // Simulate providing liquidity + uint256 liquidity = mint(msg.sender); + require(liquidity > 0); + + // Immediately burn + (uint256 returned0, uint256 returned1) = burn(msg.sender); + + // User should not receive more than they put in (accounting for rounding) + assertLte(returned0, amount0 + 1, "Mint-burn profitable in token0"); + assertLte(returned1, amount1 + 1, "Mint-burn profitable in token1"); + } + + // Price accumulator should be monotonically increasing + function test_V2_priceAccumulatorMonotonic() public { + uint256 accumulator0Before = price0CumulativeLast(); + uint256 accumulator1Before = price1CumulativeLast(); + + // Advance time + require(block.timestamp > 0); + + // Trigger price accumulator update + sync(); + + uint256 accumulator0After = price0CumulativeLast(); + uint256 accumulator1After = price1CumulativeLast(); + + // Price accumulators should never decrease + assertGte( + accumulator0After, + accumulator0Before, + "Price0 accumulator decreased" + ); + assertGte( + accumulator1After, + accumulator1Before, + "Price1 accumulator decreased" + ); + } + + // LP tokens should represent proportional ownership + function test_V2_lpTokensProportional() public { + uint256 supply = totalSupply(); + require(supply > MINIMUM_LIQUIDITY); + + uint256 userBalance = balanceOf(msg.sender); + require(userBalance > 0); + + (uint112 reserve0, uint112 reserve1,) = getReserves(); + + // User's share of reserves should equal their LP token share + uint256 expectedShare0 = (uint256(reserve0) * userBalance) / supply; + uint256 expectedShare1 = (uint256(reserve1) * userBalance) / supply; + + // These represent the user's claimable amounts + assertGt(expectedShare0, 0, "User has zero share of reserve0"); + assertGt(expectedShare1, 0, "User has zero share of reserve1"); + + // Shares should be proportional + uint256 ratio0 = (userBalance * 1000) / supply; + uint256 expectedRatio0 = (expectedShare0 * 1000) / reserve0; + + // Allow small rounding difference + uint256 diff = ratio0 > expectedRatio0 + ? ratio0 - expectedRatio0 + : expectedRatio0 - ratio0; + + assertLte(diff, 1, "LP tokens not proportional to ownership"); + } + + // Flash swap must restore K (plus fees) + function test_V2_flashSwapRestoresK() public { + uint256 kBefore = _getK(); + (uint112 reserve0, uint112 reserve1,) = getReserves(); + require(reserve0 > 1000 && reserve1 > 1000); + + // Perform a flash swap (borrow tokens, repay in callback) + uint256 amount0Out = uint256(reserve0) / 100; + + try this.swap(amount0Out, 0, address(this), hex"01") { + // Flash swap callback executed + uint256 kAfter = _getK(); + + // K should be restored (plus fees) + assertGte(kAfter, kBefore, "K not restored after flash swap"); + } catch { + // Flash swap might not be implemented or callback failed + } + } +} diff --git a/contracts/UniswapV2/internal/properties/UniswapV2RemoveLiquidityProperties.sol b/contracts/UniswapV2/internal/properties/UniswapV2RemoveLiquidityProperties.sol new file mode 100644 index 0000000..af29831 --- /dev/null +++ b/contracts/UniswapV2/internal/properties/UniswapV2RemoveLiquidityProperties.sol @@ -0,0 +1,141 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "../util/UniswapV2TestBase.sol"; + +/** + * @title Uniswap V2 Remove Liquidity Properties + * @author Trail of Bits + * @notice Properties for testing liquidity removal (burn) in Uniswap V2 pairs + */ +abstract contract CryticUniswapV2RemoveLiquidityProperties is CryticUniswapV2Base { + constructor() {} + + //////////////////////////////////////// + // Properties + + // Removing liquidity should decrease K + function test_V2_removeLiquidityDecreasesK() public { + uint256 kBefore = _getK(); + uint256 userBalance = balanceOf(msg.sender); + require(userBalance > 0); + require(kBefore > 0); + + (uint256 amount0, uint256 amount1) = burn(msg.sender); + require(amount0 > 0 || amount1 > 0); + + uint256 kAfter = _getK(); + assertLt(kAfter, kBefore, "K did not decrease after removing liquidity"); + } + + // Removing liquidity should decrease total supply of LP tokens + function test_V2_removeLiquidityDecreasesTotalSupply() public { + uint256 supplyBefore = totalSupply(); + uint256 userBalance = balanceOf(msg.sender); + require(userBalance > 0); + + (uint256 amount0, uint256 amount1) = burn(msg.sender); + require(amount0 > 0 || amount1 > 0); + + uint256 supplyAfter = totalSupply(); + assertLt( + supplyAfter, + supplyBefore, + "Total supply did not decrease after removing liquidity" + ); + } + + // Removing liquidity should decrease reserves of both tokens + function test_V2_removeLiquidityDecreasesReserves() public { + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + uint256 userBalance = balanceOf(msg.sender); + require(userBalance > 0); + require(reserve0Before > 0 && reserve1Before > 0); + + (uint256 amount0, uint256 amount1) = burn(msg.sender); + require(amount0 > 0 && amount1 > 0); + + (uint112 reserve0After, uint112 reserve1After,) = getReserves(); + assertLt( + reserve0After, + reserve0Before, + "Reserve0 did not decrease after removing liquidity" + ); + assertLt( + reserve1After, + reserve1Before, + "Reserve1 did not decrease after removing liquidity" + ); + } + + // Removing liquidity should decrease the user's LP balance + function test_V2_removeLiquidityDecreasesUserBalance() public { + uint256 balanceBefore = balanceOf(msg.sender); + require(balanceBefore > 0); + + (uint256 amount0, uint256 amount1) = burn(msg.sender); + require(amount0 > 0 || amount1 > 0); + + uint256 balanceAfter = balanceOf(msg.sender); + assertLt( + balanceAfter, + balanceBefore, + "User LP balance did not decrease after removing liquidity" + ); + } + + // Burning zero liquidity should return zero amounts + function test_V2_burnZeroLiquidity() public { + uint256 userBalance = balanceOf(msg.sender); + + if (userBalance == 0) { + (uint256 amount0, uint256 amount1) = burn(msg.sender); + assertEq(amount0, 0, "Burning zero liquidity returned non-zero amount0"); + assertEq(amount1, 0, "Burning zero liquidity returned non-zero amount1"); + } + } + + // Burning should return proportional amounts + function test_V2_burnReturnsProportionalAmounts() public { + (uint112 reserve0, uint112 reserve1,) = getReserves(); + uint256 supply = totalSupply(); + uint256 userBalance = balanceOf(msg.sender); + + require(userBalance > 0); + require(supply > 0); + require(reserve0 > 0 && reserve1 > 0); + + (uint256 amount0, uint256 amount1) = burn(msg.sender); + + if (amount0 > 0 && amount1 > 0) { + // Check proportionality: amount0/reserve0 ≈ amount1/reserve1 + // Allow 1% deviation for rounding + uint256 ratio0 = (amount0 * 1000) / reserve0; + uint256 ratio1 = (amount1 * 1000) / reserve1; + + uint256 diff = ratio0 > ratio1 ? ratio0 - ratio1 : ratio1 - ratio0; + assertLte( + diff, + 10, // 1% tolerance + "Burn did not return proportional amounts" + ); + } + } + + // Total supply should never fall below MINIMUM_LIQUIDITY + function test_V2_totalSupplyNeverBelowMinimum() public { + uint256 supply = totalSupply(); + uint256 userBalance = balanceOf(msg.sender); + + if (userBalance > 0 && supply > MINIMUM_LIQUIDITY) { + burn(msg.sender); + + uint256 supplyAfter = totalSupply(); + assertGte( + supplyAfter, + MINIMUM_LIQUIDITY, + "Total supply fell below MINIMUM_LIQUIDITY after burn" + ); + } + } +} diff --git a/contracts/UniswapV2/internal/properties/UniswapV2SwapProperties.sol b/contracts/UniswapV2/internal/properties/UniswapV2SwapProperties.sol new file mode 100644 index 0000000..e1c3ec6 --- /dev/null +++ b/contracts/UniswapV2/internal/properties/UniswapV2SwapProperties.sol @@ -0,0 +1,158 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "../util/UniswapV2TestBase.sol"; + +/** + * @title Uniswap V2 Swap Properties + * @author Trail of Bits + * @notice Properties for testing token swaps in Uniswap V2 pairs + */ +abstract contract CryticUniswapV2SwapProperties is CryticUniswapV2Base { + constructor() {} + + //////////////////////////////////////// + // Properties + + // Swapping should not decrease K (should increase due to fees) + function test_V2_swapDoesNotDecreaseK() public { + uint256 kBefore = _getK(); + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + require(reserve0Before > 0 && reserve1Before > 0); + + // Perform a swap (amount0Out > 0 means buying token0) + uint256 amount0Out = uint256(reserve0Before) / 100; // 1% of reserves + require(amount0Out > 0); + + swap(amount0Out, 0, msg.sender, ""); + + uint256 kAfter = _getK(); + assertGte(kAfter, kBefore, "K decreased after swap"); + } + + // Swapping should move price in correct direction + function test_V2_swapMovesPriceCorrectly() public { + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + require(reserve0Before > 0 && reserve1Before > 0); + + uint256 price0Before = _getPrice0(); + + // Buy token0 (sell token1) + uint256 amount0Out = uint256(reserve0Before) / 100; + require(amount0Out > 0 && amount0Out < reserve0Before); + + swap(amount0Out, 0, msg.sender, ""); + + uint256 price0After = _getPrice0(); + + // Buying token0 should increase its price (decrease reserve0, increase reserve1) + assertGt( + price0After, + price0Before, + "Price did not move correctly after swap" + ); + } + + // Swapping should not decrease LP token balance (unless fees are on) + function test_V2_swapDoesNotDecreaseLPBalance() public { + uint256 balanceBefore = balanceOf(msg.sender); + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + require(reserve0Before > 0 && reserve1Before > 0); + + uint256 amount0Out = uint256(reserve0Before) / 100; + require(amount0Out > 0 && amount0Out < reserve0Before); + + swap(amount0Out, 0, msg.sender, ""); + + uint256 balanceAfter = balanceOf(msg.sender); + + // LP balance should not decrease from a swap (might increase if protocol fees are on) + assertGte( + balanceAfter, + balanceBefore, + "LP balance decreased after swap" + ); + } + + // Swapping zero amounts should not change reserves + function test_V2_swapZeroAmountNoEffect() public { + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + + // Swap zero amounts + swap(0, 0, msg.sender, ""); + + (uint112 reserve0After, uint112 reserve1After,) = getReserves(); + + assertEq(reserve0After, reserve0Before, "Reserve0 changed after zero swap"); + assertEq(reserve1After, reserve1Before, "Reserve1 changed after zero swap"); + } + + // Swapping with insufficient liquidity should fail + function test_V2_swapInsufficientLiquidityFails() public { + (uint112 reserve0, uint112 reserve1,) = getReserves(); + require(reserve0 > 0 && reserve1 > 0); + + // Try to swap more than available reserves + try this.swap(uint256(reserve0) + 1, 0, msg.sender, "") { + assertWithMsg(false, "Swap with insufficient liquidity did not fail"); + } catch { + // Expected to fail + } + } + + // Swapping both directions simultaneously should fail + function test_V2_swapBothDirectionsFails() public { + (uint112 reserve0, uint112 reserve1,) = getReserves(); + require(reserve0 > 0 && reserve1 > 0); + + uint256 amount0Out = uint256(reserve0) / 100; + uint256 amount1Out = uint256(reserve1) / 100; + require(amount0Out > 0 && amount1Out > 0); + + // Swapping both tokens out should fail + try this.swap(amount0Out, amount1Out, msg.sender, "") { + assertWithMsg(false, "Swap in both directions did not fail"); + } catch { + // Expected to fail + } + } + + // Swap output should be positive if input is provided + function test_V2_swapPositiveOutput() public { + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + require(reserve0Before > 1000 && reserve1Before > 1000); + + uint256 amount1Out = 100; // Request small amount of token1 + + // The swap should succeed if we provide enough token0 + try this.swap(0, amount1Out, msg.sender, "") { + (uint112 reserve0After, uint112 reserve1After,) = getReserves(); + + // Reserve1 should have decreased (we received token1) + assertLt(reserve1After, reserve1Before, "Reserve1 did not decrease"); + + // Reserve0 should have increased (we paid token0) + assertGt(reserve0After, reserve0Before, "Reserve0 did not increase"); + } catch { + // Might fail if we didn't provide enough input tokens + } + } + + // K should increase by at least the fee amount (0.3%) + function test_V2_swapIncreasesKByFee() public { + uint256 kBefore = _getK(); + (uint112 reserve0Before, uint112 reserve1Before,) = getReserves(); + require(reserve0Before > 10000 && reserve1Before > 10000); + + uint256 amount0Out = uint256(reserve0Before) / 100; + require(amount0Out > 0 && amount0Out < reserve0Before); + + swap(amount0Out, 0, msg.sender, ""); + + uint256 kAfter = _getK(); + + // K should increase (fees accumulate in the pool) + // Due to 0.3% fee, K_after > K_before + assertGt(kAfter, kBefore, "K did not increase after swap (fee not collected)"); + } +} diff --git a/contracts/UniswapV2/internal/util/UniswapV2TestBase.sol b/contracts/UniswapV2/internal/util/UniswapV2TestBase.sol new file mode 100644 index 0000000..f8b9981 --- /dev/null +++ b/contracts/UniswapV2/internal/util/UniswapV2TestBase.sol @@ -0,0 +1,63 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "../../../util/PropertiesConstants.sol"; +import "../../../util/PropertiesAsserts.sol"; + +abstract contract CryticUniswapV2Base is + PropertiesAsserts, + PropertiesConstants +{ + // Minimum liquidity locked forever (Uniswap V2 constant) + uint256 internal constant MINIMUM_LIQUIDITY = 1000; + + constructor() {} + + //////////////////////////////////////// + // Abstract functions to be implemented by inheriting contract + + function token0() public view virtual returns (address); + function token1() public view virtual returns (address); + function getReserves() public view virtual returns (uint112 reserve0, uint112 reserve1, uint32 blockTimestampLast); + function price0CumulativeLast() public view virtual returns (uint256); + function price1CumulativeLast() public view virtual returns (uint256); + function kLast() public view virtual returns (uint256); + function totalSupply() public view virtual returns (uint256); + function balanceOf(address account) public view virtual returns (uint256); + + function mint(address to) public virtual returns (uint256 liquidity); + function burn(address to) public virtual returns (uint256 amount0, uint256 amount1); + function swap(uint256 amount0Out, uint256 amount1Out, address to, bytes calldata data) public virtual; + function skim(address to) public virtual; + function sync() public virtual; + + //////////////////////////////////////// + // Helper functions + + function _getK() internal view returns (uint256) { + (uint112 reserve0, uint112 reserve1,) = getReserves(); + return uint256(reserve0) * uint256(reserve1); + } + + function _getLPTokenValue() internal view returns (uint256) { + uint256 supply = totalSupply(); + if (supply == 0) return 0; + + (uint112 reserve0, uint112 reserve1,) = getReserves(); + // Value per LP token = (reserve0 + reserve1) / totalSupply + // Simplified assuming token0 and token1 have same value + return (uint256(reserve0) + uint256(reserve1)) / supply; + } + + function _getPrice0() internal view returns (uint256) { + (uint112 reserve0, uint112 reserve1,) = getReserves(); + if (reserve0 == 0) return 0; + return (uint256(reserve1) * 1e18) / uint256(reserve0); + } + + function _getPrice1() internal view returns (uint256) { + (uint112 reserve0, uint112 reserve1,) = getReserves(); + if (reserve1 == 0) return 0; + return (uint256(reserve0) * 1e18) / uint256(reserve1); + } +} diff --git a/contracts/UniswapV2/util/IUniswapV2Pair.sol b/contracts/UniswapV2/util/IUniswapV2Pair.sol new file mode 100644 index 0000000..e7d8eae --- /dev/null +++ b/contracts/UniswapV2/util/IUniswapV2Pair.sol @@ -0,0 +1,17 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +interface IUniswapV2Pair { + function token0() external view returns (address); + function token1() external view returns (address); + function getReserves() external view returns (uint112 reserve0, uint112 reserve1, uint32 blockTimestampLast); + function price0CumulativeLast() external view returns (uint256); + function price1CumulativeLast() external view returns (uint256); + function kLast() external view returns (uint256); + + function mint(address to) external returns (uint256 liquidity); + function burn(address to) external returns (uint256 amount0, uint256 amount1); + function swap(uint256 amount0Out, uint256 amount1Out, address to, bytes calldata data) external; + function skim(address to) external; + function sync() external; +} diff --git a/tests/UniswapV2/foundry/src/SimplePair.sol b/tests/UniswapV2/foundry/src/SimplePair.sol new file mode 100644 index 0000000..bf2defc --- /dev/null +++ b/tests/UniswapV2/foundry/src/SimplePair.sol @@ -0,0 +1,156 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +interface IERC20 { + function balanceOf(address account) external view returns (uint256); + function transfer(address to, uint256 amount) external returns (bool); +} + +contract SimplePair { + string public name = "Uniswap V2"; + string public symbol = "UNI-V2"; + uint8 public decimals = 18; + uint256 public totalSupply; + mapping(address => uint256) public balanceOf; + + uint256 public constant MINIMUM_LIQUIDITY = 1000; + + address public token0; + address public token1; + + uint112 private reserve0; + uint112 private reserve1; + uint32 private blockTimestampLast; + + uint256 public price0CumulativeLast; + uint256 public price1CumulativeLast; + uint256 public kLast; + + event Mint(address indexed sender, uint256 amount0, uint256 amount1); + event Burn(address indexed sender, uint256 amount0, uint256 amount1, address indexed to); + event Swap(address indexed sender, uint256 amount0In, uint256 amount1In, uint256 amount0Out, uint256 amount1Out, address indexed to); + event Sync(uint112 reserve0, uint112 reserve1); + + constructor(address _token0, address _token1) { + token0 = _token0; + token1 = _token1; + } + + function getReserves() public view returns (uint112 _reserve0, uint112 _reserve1, uint32 _blockTimestampLast) { + _reserve0 = reserve0; + _reserve1 = reserve1; + _blockTimestampLast = blockTimestampLast; + } + + function _mint(address to, uint256 value) private { + totalSupply += value; + balanceOf[to] += value; + } + + function _burn(address from, uint256 value) private { + balanceOf[from] -= value; + totalSupply -= value; + } + + function _update(uint256 balance0, uint256 balance1) private { + require(balance0 <= type(uint112).max && balance1 <= type(uint112).max, 'OVERFLOW'); + reserve0 = uint112(balance0); + reserve1 = uint112(balance1); + blockTimestampLast = uint32(block.timestamp); + emit Sync(reserve0, reserve1); + } + + function mint(address to) external returns (uint256 liquidity) { + (uint112 _reserve0, uint112 _reserve1,) = getReserves(); + uint256 balance0 = IERC20(token0).balanceOf(address(this)); + uint256 balance1 = IERC20(token1).balanceOf(address(this)); + uint256 amount0 = balance0 - _reserve0; + uint256 amount1 = balance1 - _reserve1; + + uint256 _totalSupply = totalSupply; + if (_totalSupply == 0) { + liquidity = sqrt(amount0 * amount1) - MINIMUM_LIQUIDITY; + _mint(address(0), MINIMUM_LIQUIDITY); + } else { + liquidity = min((amount0 * _totalSupply) / _reserve0, (amount1 * _totalSupply) / _reserve1); + } + require(liquidity > 0, 'INSUFFICIENT_LIQUIDITY_MINTED'); + _mint(to, liquidity); + + _update(balance0, balance1); + emit Mint(msg.sender, amount0, amount1); + } + + function burn(address to) external returns (uint256 amount0, uint256 amount1) { + (uint112 _reserve0, uint112 _reserve1,) = getReserves(); + address _token0 = token0; + address _token1 = token1; + uint256 balance0 = IERC20(_token0).balanceOf(address(this)); + uint256 balance1 = IERC20(_token1).balanceOf(address(this)); + uint256 liquidity = balanceOf[address(this)]; + + uint256 _totalSupply = totalSupply; + amount0 = (liquidity * balance0) / _totalSupply; + amount1 = (liquidity * balance1) / _totalSupply; + require(amount0 > 0 && amount1 > 0, 'INSUFFICIENT_LIQUIDITY_BURNED'); + _burn(address(this), liquidity); + IERC20(_token0).transfer(to, amount0); + IERC20(_token1).transfer(to, amount1); + balance0 = IERC20(_token0).balanceOf(address(this)); + balance1 = IERC20(_token1).balanceOf(address(this)); + + _update(balance0, balance1); + emit Burn(msg.sender, amount0, amount1, to); + } + + function swap(uint256 amount0Out, uint256 amount1Out, address to, bytes calldata) external { + require(amount0Out > 0 || amount1Out > 0, 'INSUFFICIENT_OUTPUT_AMOUNT'); + (uint112 _reserve0, uint112 _reserve1,) = getReserves(); + require(amount0Out < _reserve0 && amount1Out < _reserve1, 'INSUFFICIENT_LIQUIDITY'); + + if (amount0Out > 0) IERC20(token0).transfer(to, amount0Out); + if (amount1Out > 0) IERC20(token1).transfer(to, amount1Out); + + uint256 balance0 = IERC20(token0).balanceOf(address(this)); + uint256 balance1 = IERC20(token1).balanceOf(address(this)); + + uint256 amount0In = balance0 > _reserve0 - amount0Out ? balance0 - (_reserve0 - amount0Out) : 0; + uint256 amount1In = balance1 > _reserve1 - amount1Out ? balance1 - (_reserve1 - amount1Out) : 0; + require(amount0In > 0 || amount1In > 0, 'INSUFFICIENT_INPUT_AMOUNT'); + + uint256 balance0Adjusted = (balance0 * 1000) - (amount0In * 3); + uint256 balance1Adjusted = (balance1 * 1000) - (amount1In * 3); + require(balance0Adjusted * balance1Adjusted >= uint256(_reserve0) * uint256(_reserve1) * (1000**2), 'K'); + + _update(balance0, balance1); + emit Swap(msg.sender, amount0In, amount1In, amount0Out, amount1Out, to); + } + + function skim(address to) external { + address _token0 = token0; + address _token1 = token1; + IERC20(_token0).transfer(to, IERC20(_token0).balanceOf(address(this)) - reserve0); + IERC20(_token1).transfer(to, IERC20(_token1).balanceOf(address(this)) - reserve1); + } + + function sync() external { + _update(IERC20(token0).balanceOf(address(this)), IERC20(token1).balanceOf(address(this))); + } + + function sqrt(uint256 y) internal pure returns (uint256 z) { + if (y > 3) { + z = y; + uint256 x = y / 2 + 1; + while (x < z) { + z = x; + x = (y / x + x) / 2; + } + } else if (y != 0) { + z = 1; + } + } + + function min(uint256 x, uint256 y) internal pure returns (uint256 z) { + z = x < y ? x : y; + } +} diff --git a/tests/UniswapV2/foundry/test/CryticUniswapV2Test.sol b/tests/UniswapV2/foundry/test/CryticUniswapV2Test.sol new file mode 100644 index 0000000..cb3580c --- /dev/null +++ b/tests/UniswapV2/foundry/test/CryticUniswapV2Test.sol @@ -0,0 +1,80 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +pragma solidity ^0.8.0; + +import "properties/UniswapV2/internal/properties/UniswapV2BasicProperties.sol"; +import "properties/UniswapV2/internal/properties/UniswapV2RemoveLiquidityProperties.sol"; +import "properties/UniswapV2/internal/properties/UniswapV2SwapProperties.sol"; +import "properties/UniswapV2/internal/properties/UniswapV2InvariantProperties.sol"; +import "../src/SimplePair.sol"; + +contract TestToken { + string public name; + string public symbol; + uint8 public decimals = 18; + uint256 public totalSupply; + mapping(address => uint256) public balanceOf; + mapping(address => mapping(address => uint256)) public allowance; + + constructor(string memory _name, string memory _symbol) { + name = _name; + symbol = _symbol; + } + + function transfer(address to, uint256 amount) external returns (bool) { + balanceOf[msg.sender] -= amount; + balanceOf[to] += amount; + return true; + } + + function approve(address spender, uint256 amount) external returns (bool) { + allowance[msg.sender][spender] = amount; + return true; + } + + function transferFrom(address from, address to, uint256 amount) external returns (bool) { + allowance[from][msg.sender] -= amount; + balanceOf[from] -= amount; + balanceOf[to] += amount; + return true; + } + + function mint(address to, uint256 amount) external { + totalSupply += amount; + balanceOf[to] += amount; + } +} + +contract CryticUniswapV2InternalHarness is + SimplePair, + CryticUniswapV2BasicProperties, + CryticUniswapV2RemoveLiquidityProperties, + CryticUniswapV2SwapProperties, + CryticUniswapV2InvariantProperties +{ + TestToken public tokenA; + TestToken public tokenB; + + constructor() SimplePair(address(0), address(0)) { + // Deploy test tokens + tokenA = new TestToken("Token A", "TKA"); + tokenB = new TestToken("Token B", "TKB"); + + // Set token addresses + token0 = address(tokenA); + token1 = address(tokenB); + + // Mint initial tokens to test users + tokenA.mint(USER1, INITIAL_BALANCE); + tokenA.mint(USER2, INITIAL_BALANCE); + tokenA.mint(USER3, INITIAL_BALANCE); + + tokenB.mint(USER1, INITIAL_BALANCE); + tokenB.mint(USER2, INITIAL_BALANCE); + tokenB.mint(USER3, INITIAL_BALANCE); + + // Initialize the pair with some liquidity + tokenA.mint(address(this), 10000e18); + tokenB.mint(address(this), 10000e18); + this.mint(address(this)); + } +}