From 289f9322edc9c68812eb704c7f5b6deaf12b976e Mon Sep 17 00:00:00 2001 From: Omar Inuwa Date: Wed, 26 Nov 2025 14:26:07 +0100 Subject: [PATCH] Add property documentation standards and standardize ERC20BasicProperties This PR addresses issue #39 by establishing comprehensive documentation standards for all property test functions in the repository. Changes: - Add PROPERTY_STANDARDS.md defining complete documentation standards - NatSpec template with required tags (@title, @notice, @dev, @custom) - 5 testing modes documented (INTERNAL/EXTERNAL/ISOLATED/FUNCTION_OVERRIDE/MODEL) - Property ID format: [STANDARD]-[CATEGORY]-[NUMBER] - Section organization guidelines matching ABDKMath64x64 style - Before/after examples and contribution checklist - Standardize ERC20BasicProperties.sol (17 properties) - Add comprehensive contract-level NatSpec documentation - Organize into 4 logical sections with standardized headers: * Supply Accounting (1 property) * Balance Accounting (3 properties) * Transfer Properties (10 properties) * Allowance Properties (3 properties) - Add full NatSpec to all 17 properties with: * Testing mode specification (INTERNAL) * Plain English invariant descriptions * Unique property IDs (ERC20-SUPPLY-001 through ERC20-ALLOWANCE-003) * Detailed explanations of why each property matters Standardizing ERC20BasicProperties is the first of many files that will be updated to follow these standards. This establishes the foundation and reference implementation for standardizing the remaining 151 properties across ERC20, ERC721, ERC4626, and Math library contracts. Fixes #39 --- PROPERTY_STANDARDS.md | 435 ++++++++++++++++++ .../properties/ERC20BasicProperties.sol | 212 ++++++++- 2 files changed, 627 insertions(+), 20 deletions(-) create mode 100644 PROPERTY_STANDARDS.md diff --git a/PROPERTY_STANDARDS.md b/PROPERTY_STANDARDS.md new file mode 100644 index 0000000..535b1d5 --- /dev/null +++ b/PROPERTY_STANDARDS.md @@ -0,0 +1,435 @@ +# Property Documentation Standards + +This document defines the standardization rules for all property test functions in the Crytic Properties repository. These standards ensure consistency, clarity, and educational value across all 168+ properties. + +## Overview + +All property test functions must follow these standards: +1. **NatSpec Documentation** - Complete structured documentation +2. **Testing Mode** - Clearly specified approach (INTERNAL/EXTERNAL/ISOLATED/FUNCTION_OVERRIDE/MODEL) +3. **Invariant Description** - Plain English explanation of what must always be true +4. **Logical Organization** - Properties grouped into meaningful sections +5. **Unique Identifiers** - Trackable property IDs for reference + +## Testing Modes + +Based on [Echidna's common testing approaches](https://secure-contracts.com/program-analysis/echidna/basic/common-testing-approaches.html#partial-testing), we use five testing modes: + +### INTERNAL +Test harness inherits from the contract under test. Properties have direct access to internal state and functions. + +**When to use:** Testing your own contracts during development. + +**Example:** +```solidity +contract TestHarness is MyToken, CryticERC20BasicProperties { + constructor() { + _mint(USER1, INITIAL_BALANCE); + } +} +``` + +### EXTERNAL +Test harness interacts with the contract through its public interface only. Simulates real-world usage patterns. + +**When to use:** Testing deployed contracts or simulating external user interactions. + +**Example:** +```solidity +contract TestHarness is CryticERC20ExternalBasicProperties { + constructor() { + token = ITokenMock(address(new MyToken())); + } +} +``` + +### ISOLATED +Testing individual components abstracted from the rest of the system. Particularly useful for stateless mathematical operations. + +**When to use:** Testing math libraries, pure functions, or components with no external dependencies. + +**Example:** Testing ABDKMath64x64 arithmetic operations independently. + +### FUNCTION_OVERRIDE +Uses Solidity's override mechanism to mock or disable dependencies that cannot be simulated (e.g., oracles, bridges, signature verification). + +**When to use:** System depends on off-chain components or external systems that cannot be easily mocked. + +**Example:** +```solidity +contract TestHarness is System { + function verifySignature(...) public override returns (bool) { + return true; // Mock: signatures always valid for testing + } +} +``` + +### MODEL +Abstract mathematical model represents expected behavior. Properties compare actual contract behavior against a simplified reference implementation. + +**When to use:** Contract implements complex logic with known mathematical properties that can be expressed as a simpler model. + +**Example:** Comparing vault share calculations against a simplified mathematical formula. + +--- + +## NatSpec Documentation Template + +Every property function **must** include the following NatSpec tags: + +```solidity +/// @title [Human-Readable Property Name] +/// @notice [Brief user-facing description of what this property tests] +/// @dev Testing Mode: [INTERNAL|EXTERNAL|ISOLATED|FUNCTION_OVERRIDE|MODEL] +/// @dev Invariant: [Plain English description of what must always be true] +/// @dev [Optional: Additional context, examples, or preconditions] +/// @custom:property-id [STANDARD]-[CATEGORY]-[NUMBER] +function test_Standard_PropertyName() public { + // Implementation +} +``` + +### Tag Requirements + +| Tag | Required | Purpose | Example | +|-----|----------|---------|---------| +| `@title` | ✅ Yes | Clear, human-readable property name | "User Balance Cannot Exceed Total Supply" | +| `@notice` | ✅ Yes | Brief description for users/auditors | "Ensures individual balances never exceed the total token supply" | +| `@dev Testing Mode:` | ✅ Yes | Specify which testing approach is used | "Testing Mode: INTERNAL" | +| `@dev Invariant:` | ✅ Yes | Plain English invariant description | "For any address `user`, `balanceOf(user) <= totalSupply()` must always hold" | +| `@dev [context]` | ⚠️ Optional | Additional explanations, examples, or preconditions | "This is a fundamental accounting invariant..." | +| `@custom:property-id` | ✅ Yes | Unique identifier for tracking | "ERC20-BALANCE-001" | + +--- + +## Property ID Format + +Property IDs follow the pattern: `[STANDARD]-[CATEGORY]-[NUMBER]` + +### Standard Prefixes +- `ERC20` - ERC20 token properties +- `ERC721` - ERC721 NFT properties +- `ERC4626` - ERC4626 vault properties +- `MATH` - Mathematical library properties + +### Category Guidelines + +Choose categories based on **functionality** being tested: + +**For ERC20:** +- `SUPPLY` - Total supply accounting +- `BALANCE` - Individual balance accounting +- `TRANSFER` - Transfer mechanics and safety +- `ALLOWANCE` - Approve/transferFrom mechanics +- `BURN` - Burning mechanics +- `MINT` - Minting mechanics +- `PAUSE` - Pause functionality + +**For ERC721:** +- `OWNERSHIP` - Token ownership tracking +- `TRANSFER` - Transfer mechanics +- `APPROVAL` - Approval mechanics +- `BURN` - Burning mechanics +- `MINT` - Minting mechanics + +**For ERC4626:** +- `ACCOUNTING` - Share/asset accounting +- `DEPOSIT` - Deposit mechanics +- `WITHDRAW` - Withdrawal mechanics +- `SECURITY` - Security properties (inflation attacks, etc.) +- `ROUNDING` - Rounding direction safety + +**For Math:** +- `[OPERATION]` - Name of the operation (ADD, SUB, MUL, DIV, SQRT, LOG, etc.) + +### Numbering +- Use zero-padded 3-digit numbers: 001, 002, 003, etc. +- Sequential within each category +- No gaps in numbering + +### Examples +- `ERC20-SUPPLY-001` - First supply accounting property +- `ERC20-TRANSFER-005` - Fifth transfer property +- `ERC721-OWNERSHIP-001` - First ownership property +- `ERC4626-SECURITY-002` - Second security property +- `MATH-ADD-001` - First addition property + +--- + +## File Organization + +### File-Level Documentation + +Every property contract must include comprehensive contract-level NatSpec: + +```solidity +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity ^0.8.0; + +import "./PropertiesHelper.sol"; + +/** + * @title [Contract Name] Properties + * @author Crytic (Trail of Bits) + * @notice [High-level description of what this contract tests] + * @dev Testing Mode: [Primary mode used in this contract] + * @dev This contract contains [X] properties testing [brief description] + * @dev + * @dev Usage Example: + * @dev ```solidity + * @dev contract TestHarness is MyToken, CryticERC20BasicProperties { + * @dev constructor() { + * @dev _mint(USER1, INITIAL_BALANCE); + * @dev initialSupply = totalSupply(); + * @dev } + * @dev } + * @dev ``` + */ +contract ContractNameProperties is PropertiesAsserts { + // Contract body +} +``` + +### Section Structure + +Properties should be organized into logical sections based on functionality: + +```solidity +// ================================================================ +// STATE VARIABLES & CONFIGURATION +// ================================================================ + +/// @notice [Description of state variable] +uint256 public someStateVar; + + +/* ================================================================ + + [SECTION NAME IN CAPS] + + Description: [What this section tests] + Testing Mode: [MODE if different from default] + Property Count: [X] + + ================================================================ */ + +// Properties for this section... + + +/* ================================================================ + + [NEXT SECTION NAME] + + Description: [What this section tests] + Property Count: [X] + + ================================================================ */ + +// Properties for next section... +``` + +### Section Header Format + +Must follow this exact format (matching ABDKMath64x64PropertyTests.sol): + +```solidity +/* ================================================================ + + [SECTION TITLE HERE] + + Description: [Brief explanation] + Testing Mode: [MODE] (if different from file default) + Property Count: [X] + + ================================================================ */ +``` + +**Rules:** +- Opening `/*` and closing `*/` on their own lines +- `================================================================` lines (64 equals signs) +- Empty line after opening +- Section title centered (3 blank lines before title) +- Empty line after title +- Description and metadata left-aligned with 3-space indent +- Empty line before closing + +--- + +## Complete Example + +Here's a complete before/after example: + +### Before (Current State) +```solidity +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity ^0.8.13; + +import "../util/ERC20TestBase.sol"; + +abstract contract CryticERC20BasicProperties is CryticERC20Base { + // User balance must not exceed total supply + function test_ERC20_userBalanceNotHigherThanSupply() public { + assertLte( + balanceOf(msg.sender), + totalSupply(), + "User balance higher than total supply" + ); + } + + // Address zero should have zero balance + function test_ERC20_zeroAddressBalance() public { + assertEq( + balanceOf(address(0)), + 0, + "Address zero balance not equal to zero" + ); + } +} +``` + +### After (Standardized) +```solidity +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity ^0.8.13; + +import "../util/ERC20TestBase.sol"; + +/** + * @title ERC20 Basic Properties + * @author Crytic (Trail of Bits) + * @notice Core invariant properties for ERC20 token implementations + * @dev Testing Mode: INTERNAL (can also be used EXTERNALLY via interface) + * @dev This contract contains 17 fundamental properties testing supply accounting, + * @dev balance accounting, transfer mechanics, and allowance operations. + * @dev + * @dev Usage Example: + * @dev ```solidity + * @dev contract TestHarness is MyToken, CryticERC20BasicProperties { + * @dev constructor() { + * @dev _mint(USER1, INITIAL_BALANCE); + * @dev _mint(USER2, INITIAL_BALANCE); + * @dev initialSupply = totalSupply(); + * @dev isMintableOrBurnable = false; // Set based on your token + * @dev } + * @dev } + * @dev ``` + */ +abstract contract CryticERC20BasicProperties is CryticERC20Base { + + // ================================================================ + // STATE VARIABLES + // ================================================================ + + /// @notice Initial total supply recorded at test initialization + /// @dev Used for constant supply checks in non-mintable/burnable tokens + uint256 public initialSupply; + + /// @notice Flag indicating if token supply can change after deployment + /// @dev Set to true for mintable/burnable tokens, false for fixed supply + bool public isMintableOrBurnable; + + + /* ================================================================ + + BALANCE ACCOUNTING PROPERTIES + + Description: Properties verifying individual balance accounting + Testing Mode: INTERNAL + Property Count: 2 + + ================================================================ */ + + /// @title User Balance Cannot Exceed Total Supply + /// @notice Ensures individual user balances never exceed the total token supply + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: For any address `user`, `balanceOf(user) <= totalSupply()` must always hold + /// @dev This is a fundamental accounting invariant - if violated, the token contract + /// @dev has a critical bug allowing token creation from nothing or double-counting + /// @custom:property-id ERC20-BALANCE-001 + function test_ERC20_userBalanceNotHigherThanSupply() public { + assertLte( + balanceOf(msg.sender), + totalSupply(), + "User balance higher than total supply" + ); + } + + /// @title Zero Address Has Zero Balance + /// @notice The zero address should never hold tokens + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: `balanceOf(address(0)) == 0` must always hold + /// @dev The zero address is conventionally used to represent burned tokens. + /// @dev If it holds a non-zero balance, tokens are effectively lost/inaccessible + /// @custom:property-id ERC20-BALANCE-002 + function test_ERC20_zeroAddressBalance() public { + assertEq( + balanceOf(address(0)), + 0, + "Address zero balance not equal to zero" + ); + } +} +``` + +--- + +## Code Style Requirements + +### Assertion Messages +- Must be descriptive and clearly indicate what invariant was violated +- Use present tense ("Balance exceeds supply" not "Balance exceeded supply") +- No abbreviations or unclear technical jargon + +### Formatting +- Property functions should have blank lines between them for readability +- Long assertions should be formatted with one parameter per line +- Consistent indentation (4 spaces) + +### Comments +- Replace inline comments with NatSpec documentation +- Only keep inline comments if they explain non-obvious implementation details +- Avoid redundant comments that simply restate the code + +--- + +## Contribution Checklist + +Before submitting a PR with new or modified properties: + +- [ ] All property functions have complete NatSpec (@title, @notice, @dev tags) +- [ ] Testing mode is clearly documented in @dev tag +- [ ] Invariant is described in plain English in @dev tag +- [ ] Property has a unique ID in @custom:property-id tag +- [ ] Property ID follows the [STANDARD]-[CATEGORY]-[NUMBER] format +- [ ] Property is placed in the appropriate logical section +- [ ] Section headers follow the standardized format +- [ ] File has comprehensive contract-level NatSpec +- [ ] Assertion messages are clear and descriptive +- [ ] Related documentation (PROPERTIES.md, README) is updated + +--- + +## Automated Validation + +Future: A linting script will validate: +- All `test_*` functions have required NatSpec tags +- Testing mode is specified and valid +- Invariant descriptions are present +- Property IDs are unique and properly formatted +- Section headers follow the standard format + +--- + +## Questions? + +For questions about these standards: +1. Review existing standardized files (e.g., ERC20BasicProperties.sol) +2. Check examples in this document +3. Open an issue in the GitHub repository +4. Refer to the [contribution guidelines](./CONTRIBUTING.md) + +## Document History + +- **2025-11**: Initial standardization document created +- Based on issue: "Standardize properties in the repo" +- Reference implementation: ABDKMath64x64PropertyTests.sol section headers diff --git a/contracts/ERC20/internal/properties/ERC20BasicProperties.sol b/contracts/ERC20/internal/properties/ERC20BasicProperties.sol index 9ce039e..5ed7d62 100644 --- a/contracts/ERC20/internal/properties/ERC20BasicProperties.sol +++ b/contracts/ERC20/internal/properties/ERC20BasicProperties.sol @@ -3,19 +3,74 @@ pragma solidity ^0.8.13; import "../util/ERC20TestBase.sol"; +/** + * @title ERC20 Basic Properties + * @author Crytic (Trail of Bits) + * @notice Core invariant properties for ERC20 token implementations + * @dev Testing Mode: INTERNAL (test harness inherits from token and properties) + * @dev This contract contains 17 fundamental properties that test supply accounting, + * @dev balance accounting, transfer mechanics, and allowance operations for ERC20 tokens. + * @dev These properties represent the essential invariants that all ERC20 implementations + * @dev should maintain to ensure correct accounting and safe operations. + * @dev + * @dev Usage Example: + * @dev ```solidity + * @dev contract TestHarness is MyToken, CryticERC20BasicProperties { + * @dev constructor() { + * @dev _mint(USER1, INITIAL_BALANCE); + * @dev _mint(USER2, INITIAL_BALANCE); + * @dev _mint(USER3, INITIAL_BALANCE); + * @dev initialSupply = totalSupply(); + * @dev isMintableOrBurnable = false; // Set based on your token's features + * @dev } + * @dev } + * @dev ``` + */ abstract contract CryticERC20BasicProperties is CryticERC20Base { constructor() {} - //////////////////////////////////////// - // Properties - // Total supply should change only by means of mint or burn + /* ================================================================ + + SUPPLY ACCOUNTING PROPERTIES + + Description: Properties verifying total supply accounting correctness + Testing Mode: INTERNAL + Property Count: 1 + + ================================================================ */ + + /// @title Constant Supply Invariant + /// @notice For non-mintable/burnable tokens, total supply must remain constant + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: If `!isMintableOrBurnable`, then `totalSupply() == initialSupply` must always hold + /// @dev This property only applies to tokens with fixed supply. For mintable or burnable + /// @dev tokens, set `isMintableOrBurnable = true` to skip this check. + /// @dev Preconditions: Only meaningful when isMintableOrBurnable is false + /// @custom:property-id ERC20-SUPPLY-001 function test_ERC20_constantSupply() public virtual { require(!isMintableOrBurnable); assertEq(initialSupply, totalSupply(), "Token supply was modified"); } - // User balance must not exceed total supply + + /* ================================================================ + + BALANCE ACCOUNTING PROPERTIES + + Description: Properties verifying individual balance accounting correctness + Testing Mode: INTERNAL + Property Count: 3 + + ================================================================ */ + + /// @title User Balance Cannot Exceed Total Supply + /// @notice Ensures that any individual user's balance never exceeds the total token supply + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: For any address `user`, `balanceOf(user) <= totalSupply()` must always hold + /// @dev This is a fundamental accounting invariant. If violated, the token contract has + /// @dev a critical bug allowing token creation from nothing, double-counting, or overflow. + /// @custom:property-id ERC20-BALANCE-001 function test_ERC20_userBalanceNotHigherThanSupply() public { assertLte( balanceOf(msg.sender), @@ -24,7 +79,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { ); } - // Sum of users balance must not exceed total supply + /// @title Sum of User Balances Cannot Exceed Total Supply + /// @notice Ensures that the sum of test user balances never exceeds the total supply + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: `balanceOf(USER1) + balanceOf(USER2) + balanceOf(USER3) <= totalSupply()` + /// @dev This checks that the accounting for multiple users remains consistent with total supply. + /// @dev While not exhaustive (doesn't check all addresses), it provides confidence in multi-user scenarios. + /// @custom:property-id ERC20-BALANCE-002 function test_ERC20_usersBalancesNotHigherThanSupply() public { uint256 balance = balanceOf(USER1) + balanceOf(USER2) + @@ -36,7 +97,14 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { ); } - // Address zero should have zero balance + /// @title Zero Address Has Zero Balance + /// @notice The zero address should never hold tokens + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: `balanceOf(address(0)) == 0` must always hold + /// @dev The zero address (0x0) is conventionally used to represent burned tokens or null state. + /// @dev If it holds a non-zero balance, tokens are effectively lost and inaccessible, breaking + /// @dev the accounting assumption that all supply is either held by users or explicitly burned. + /// @custom:property-id ERC20-BALANCE-003 function test_ERC20_zeroAddressBalance() public { assertEq( balanceOf(address(0)), @@ -45,7 +113,24 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { ); } - // Transfers to zero address should not be allowed + + /* ================================================================ + + TRANSFER PROPERTIES + + Description: Properties verifying transfer mechanics and safety guarantees + Testing Mode: INTERNAL + Property Count: 10 + + ================================================================ */ + + /// @title Transfer to Zero Address Must Fail + /// @notice Transfers to the zero address should not be allowed + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: `transfer(address(0), amount)` must return false or revert for any amount > 0 + /// @dev Prevents accidental token burning via transfer. Burning should use explicit burn() + /// @dev functions if supported. This protects users from irreversible mistakes. + /// @custom:property-id ERC20-TRANSFER-001 function test_ERC20_transferToZeroAddress() public { uint256 balance = balanceOf(address(this)); require(balance > 0); @@ -54,7 +139,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { assertWithMsg(r == false, "Successful transfer to address zero"); } - // Transfers to zero address should not be allowed + /// @title TransferFrom to Zero Address Must Fail + /// @notice TransferFrom to the zero address should not be allowed + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: `transferFrom(sender, address(0), amount)` must return false or revert + /// @dev Similar to direct transfers, this prevents accidental burning through delegated transfers. + /// @dev Protects against both user error and potential exploits involving allowances. + /// @custom:property-id ERC20-TRANSFER-002 function test_ERC20_transferFromToZeroAddress(uint256 value) public { uint256 balance_sender = balanceOf(msg.sender); uint256 current_allowance = allowance(msg.sender, address(this)); @@ -67,7 +158,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { assertWithMsg(r == false, "Successful transferFrom to address zero"); } - // Self transfers should not break accounting + /// @title Self TransferFrom Preserves Balance + /// @notice Transferring tokens to oneself via transferFrom should not change balance + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: After `transferFrom(user, user, amount)`, `balanceOf(user)` must remain unchanged + /// @dev Self-transfers are a special case that some implementations handle incorrectly. + /// @dev The balance should remain the same since tokens are both leaving and entering the same account. + /// @custom:property-id ERC20-TRANSFER-003 function test_ERC20_selfTransferFrom(uint256 value) public { uint256 balance_sender = balanceOf(msg.sender); uint256 current_allowance = allowance(msg.sender, address(this)); @@ -85,7 +182,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { ); } - // Self transfers should not break accounting + /// @title Self Transfer Preserves Balance + /// @notice Transferring tokens to oneself should not change balance + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: After `transfer(sender, amount)` where sender == recipient, balance must be unchanged + /// @dev Self-transfers via direct transfer() should behave identically to self transferFrom(). + /// @dev This is a common edge case that can expose accounting bugs in naive implementations. + /// @custom:property-id ERC20-TRANSFER-004 function test_ERC20_selfTransfer(uint256 value) public { uint256 balance_sender = balanceOf(address(this)); require(balance_sender > 0); @@ -99,7 +202,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { ); } - // Transfers for more than available balance should not be allowed + /// @title TransferFrom More Than Balance Must Fail + /// @notice TransferFrom exceeding sender's balance should not be allowed + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: `transferFrom(sender, recipient, amount)` where `amount > balanceOf(sender)` must fail + /// @dev Even with sufficient allowance, transfers cannot exceed the sender's actual balance. + /// @dev Both sender and recipient balances must remain unchanged on failure. + /// @custom:property-id ERC20-TRANSFER-005 function test_ERC20_transferFromMoreThanBalance(address target) public { uint256 balance_sender = balanceOf(msg.sender); uint256 balance_receiver = balanceOf(target); @@ -123,7 +232,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { ); } - // Transfers for more than available balance should not be allowed + /// @title Transfer More Than Balance Must Fail + /// @notice Transfers exceeding sender's balance should not be allowed + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: `transfer(recipient, amount)` where `amount > balanceOf(sender)` must fail + /// @dev Fundamental safety property preventing token creation or negative balances. + /// @dev Both sender and recipient balances must remain unchanged on failure. + /// @custom:property-id ERC20-TRANSFER-006 function test_ERC20_transferMoreThanBalance(address target) public { uint256 balance_sender = balanceOf(address(this)); uint256 balance_receiver = balanceOf(target); @@ -146,7 +261,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { ); } - // Zero amount transfers should not break accounting + /// @title Zero Amount Transfer Succeeds Without Changes + /// @notice Transferring zero tokens should succeed without modifying balances + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: `transfer(recipient, 0)` must succeed and leave all balances unchanged + /// @dev Zero-value transfers should be no-ops. Some contracts incorrectly reject them, + /// @dev which can break composability with other contracts expecting standard behavior. + /// @custom:property-id ERC20-TRANSFER-007 function test_ERC20_transferZeroAmount(address target) public { uint256 balance_sender = balanceOf(address(this)); uint256 balance_receiver = balanceOf(target); @@ -166,7 +287,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { ); } - // Zero amount transfers should not break accounting + /// @title Zero Amount TransferFrom Succeeds Without Changes + /// @notice TransferFrom with zero tokens should succeed without modifying balances + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: `transferFrom(sender, recipient, 0)` must succeed and leave balances unchanged + /// @dev Zero-value delegated transfers should also be no-ops, maintaining consistency + /// @dev with direct transfer behavior and ERC20 standard expectations. + /// @custom:property-id ERC20-TRANSFER-008 function test_ERC20_transferFromZeroAmount(address target) public { uint256 balance_sender = balanceOf(msg.sender); uint256 balance_receiver = balanceOf(target); @@ -187,7 +314,14 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { ); } - // Transfers should update accounting correctly + /// @title Transfer Updates Balances Correctly + /// @notice Regular transfers should update sender and recipient balances correctly + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: After `transfer(recipient, amount)`, sender balance decreases by `amount` + /// @dev and recipient balance increases by `amount` + /// @dev This is the core correctness property for transfers: tokens leaving one account + /// @dev must arrive in the destination account, preserving total supply. + /// @custom:property-id ERC20-TRANSFER-009 function test_ERC20_transfer(address target, uint256 amount) public { require(target != address(this)); uint256 balance_sender = balanceOf(address(this)); @@ -209,7 +343,14 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { ); } - // Transfers should update accounting correctly + /// @title TransferFrom Updates Balances Correctly + /// @notice Delegated transfers should update sender and recipient balances correctly + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: After `transferFrom(sender, recipient, amount)`, sender balance decreases + /// @dev by `amount` and recipient balance increases by `amount` + /// @dev Core correctness property for delegated transfers. Must maintain same accounting + /// @dev guarantees as direct transfers, just with allowance consumption. + /// @custom:property-id ERC20-TRANSFER-010 function test_ERC20_transferFrom(address target, uint256 amount) public { require(target != address(this)); require(target != msg.sender); @@ -233,7 +374,24 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { ); } - // Approve should set correct allowances + + /* ================================================================ + + ALLOWANCE PROPERTIES + + Description: Properties verifying approve/transferFrom allowance mechanics + Testing Mode: INTERNAL + Property Count: 3 + + ================================================================ */ + + /// @title Approve Sets Allowance Correctly + /// @notice Approve should set the allowance to the specified amount + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: After `approve(spender, amount)`, `allowance(owner, spender) == amount` + /// @dev Basic correctness property for the approval mechanism. The allowance value + /// @dev must be set exactly as specified, enabling precise delegation of spending rights. + /// @custom:property-id ERC20-ALLOWANCE-001 function test_ERC20_setAllowance(address target, uint256 amount) public { bool r = this.approve(target, amount); assertWithMsg(r == true, "Failed to set allowance via approve"); @@ -244,7 +402,13 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { ); } - // Approve should set correct allowances + /// @title Approve Can Overwrite Previous Allowance + /// @notice Approve should be able to change existing allowances + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: Sequential `approve()` calls should each set allowance to the new value + /// @dev Allowances must be updateable to allow users to modify or revoke spending permissions. + /// @dev This is essential for security (reducing allowances) and flexibility (increasing them). + /// @custom:property-id ERC20-ALLOWANCE-002 function test_ERC20_setAllowanceTwice( address target, uint256 amount @@ -266,7 +430,15 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { ); } - // TransferFrom should decrease allowance + /// @title TransferFrom Decreases Allowance + /// @notice TransferFrom should decrease the allowance by the transferred amount + /// @dev Testing Mode: INTERNAL + /// @dev Invariant: After `transferFrom(owner, recipient, amount)`, allowance decreases by `amount` + /// @dev Exception: Allowance of `type(uint256).max` is treated as infinite by some implementations + /// @dev This ensures that allowances are consumed correctly, preventing spenders from + /// @dev exceeding their delegated permissions. The infinite allowance exception is a + /// @dev common optimization to avoid storage updates for "unlimited" approvals. + /// @custom:property-id ERC20-ALLOWANCE-003 function test_ERC20_spendAllowanceAfterTransfer( address target, uint256 amount @@ -281,7 +453,7 @@ abstract contract CryticERC20BasicProperties is CryticERC20Base { bool r = this.transferFrom(msg.sender, target, transfer_value); assertWithMsg(r == true, "transferFrom failed"); - // Some implementations take an allowance of 2**256-1 as infinite, and therefore don't update + // Some implementations treat type(uint256).max as infinite allowance if (current_allowance != type(uint256).max) { assertEq( allowance(msg.sender, address(this)),