Standardize all properties

contracts/ERC20/external/properties/ERC20ExternalBurnableProperties.sol

@@ -3,15 +3,50 @@ pragma solidity ^0.8.0;
 
 import "../util/ERC20ExternalTestBase.sol";
 
+/**
+ * @title ERC20 External Burnable Properties
+ * @author Crytic (Trail of Bits)
+ * @notice Properties for ERC20 tokens with burn functionality tested via external interface
+ * @dev Testing Mode: EXTERNAL (test harness interacts with token through external interface)
+ * @dev This contract contains 3 properties that test token burning mechanics via external
+ * @dev interface, including burn(), burnFrom(), and allowance updates during burns.
+ * @dev
+ * @dev Usage Example:
+ * @dev ```solidity
+ * @dev contract TestHarness is CryticERC20ExternalBurnableProperties {
+ * @dev     constructor() {
+ * @dev         // Deploy or reference your burnable ERC20 token
+ * @dev         token = ITokenMock(address(new MyBurnableToken()));
+ * @dev     }
+ * @dev }
+ * @dev ```
+ */
 abstract contract CryticERC20ExternalBurnableProperties is
     CryticERC20ExternalTestBase
 {
     constructor() {}
 
-    ////////////////////////////////////////
-    // Properties
 
-    // Burn should update user balance and total supply
+    /* ================================================================
+
+                        BURN PROPERTIES
+
+       Description: Properties verifying token burning mechanics
+       Testing Mode: EXTERNAL
+       Property Count: 3
+
+       ================================================================ */
+
+    /// @title Burn Updates Balance and Supply Correctly
+    /// @notice Burning tokens should decrease both user balance and total supply
+    /// @dev Testing Mode: EXTERNAL
+    /// @dev Invariant: After `burn(amount)`, `balanceOf(burner)` decreases by `amount`
+    /// @dev and `totalSupply()` decreases by `amount`
+    /// @dev This ensures burned tokens are properly removed from circulation and cannot
+    /// @dev be recovered, maintaining accurate accounting of circulating supply. The burn
+    /// @dev operation permanently destroys tokens, reducing both individual balance and
+    /// @dev the total token supply by exactly the burned amount.
+    /// @custom:property-id ERC20-EXTERNAL-BURN-051
     function test_ERC20external_burn(uint256 amount) public {
         uint256 balance_sender = token.balanceOf(address(this));
         uint256 supply = token.totalSupply();
@@ -31,7 +66,15 @@ abstract contract CryticERC20ExternalBurnableProperties is
         );
     }
 
-    // Burn should update user balance and total supply
+    /// @title BurnFrom Updates Balance and Supply Correctly
+    /// @notice Burning tokens via burnFrom should decrease both owner balance and total supply
+    /// @dev Testing Mode: EXTERNAL
+    /// @dev Invariant: After `burnFrom(owner, amount)`, `balanceOf(owner)` decreases by `amount`
+    /// @dev and `totalSupply()` decreases by `amount`
+    /// @dev Delegated burning must maintain the same accounting guarantees as direct burning,
+    /// @dev ensuring tokens are permanently removed from circulation regardless of burn method.
+    /// @dev The burner must have sufficient allowance from the owner to burn tokens on their behalf.
+    /// @custom:property-id ERC20-EXTERNAL-BURN-052
     function test_ERC20external_burnFrom(uint256 amount) public {
         uint256 balance_sender = token.balanceOf(msg.sender);
         uint256 allowance = token.allowance(msg.sender, address(this));
@@ -52,7 +95,16 @@ abstract contract CryticERC20ExternalBurnableProperties is
         );
     }
 
-    // burnFrom should update allowance
+    /// @title BurnFrom Decreases Allowance Correctly
+    /// @notice BurnFrom should consume the burner's allowance
+    /// @dev Testing Mode: EXTERNAL
+    /// @dev Invariant: After `burnFrom(owner, amount)`, `allowance(owner, burner)` decreases by `amount`
+    /// @dev Exception: Allowance of `type(uint256).max` is treated as infinite by some implementations
+    /// @dev This prevents unauthorized burning beyond granted allowances. The burner must have
+    /// @dev sufficient allowance to burn tokens on behalf of the owner, and that allowance is
+    /// @dev consumed during the burn operation (unless infinite allowance is used). This ensures
+    /// @dev burn permissions are properly enforced through the allowance mechanism.
+    /// @custom:property-id ERC20-EXTERNAL-BURN-053
     function test_ERC20external_burnFromUpdateAllowance(uint256 amount) public {
         uint256 balance_sender = token.balanceOf(msg.sender);
         uint256 current_allowance = token.allowance(msg.sender, address(this));

contracts/ERC20/external/properties/ERC20ExternalIncreaseAllowanceProperties.sol

@@ -3,15 +3,52 @@ pragma solidity ^0.8.0;
 
 import "../util/ERC20ExternalTestBase.sol";
 
+/**
+ * @title ERC20 External Increase/Decrease Allowance Properties
+ * @author Crytic (Trail of Bits)
+ * @notice Properties for ERC20 tokens with increaseAllowance and decreaseAllowance functions tested via external interface
+ * @dev Testing Mode: EXTERNAL (test harness interacts with token through external interface)
+ * @dev This contract contains 2 properties that test increaseAllowance() and decreaseAllowance()
+ * @dev functions via external interface. These functions provide safer alternatives to approve()
+ * @dev by modifying existing allowances rather than setting absolute values.
+ * @dev
+ * @dev Usage Example:
+ * @dev ```solidity
+ * @dev contract TestHarness is CryticERC20ExternalIncreaseAllowanceProperties {
+ * @dev     constructor() {
+ * @dev         // Deploy or reference your ERC20 token with increase/decrease allowance
+ * @dev         token = ITokenMock(address(new MyToken()));
+ * @dev     }
+ * @dev }
+ * @dev ```
+ */
 abstract contract CryticERC20ExternalIncreaseAllowanceProperties is
     CryticERC20ExternalTestBase
 {
     constructor() {}
 
-    ////////////////////////////////////////
-    // Properties
 
-    // Allowance should be modified correctly via increase/decrease
+    /* ================================================================
+
+                    ALLOWANCE MODIFICATION PROPERTIES
+
+       Description: Properties verifying increaseAllowance/decreaseAllowance
+       Testing Mode: EXTERNAL
+       Property Count: 2
+
+       ================================================================ */
+
+    /// @title IncreaseAllowance Updates Allowance Correctly
+    /// @notice Increasing allowance should add to the existing allowance value
+    /// @dev Testing Mode: EXTERNAL
+    /// @dev Invariant: After `increaseAllowance(spender, amount)`, the allowance becomes
+    /// @dev `previousAllowance + amount`
+    /// @dev The increaseAllowance() function provides a safer alternative to approve() by
+    /// @dev incrementing the existing allowance rather than setting an absolute value. This
+    /// @dev prevents certain race conditions where a spender could potentially spend both the
+    /// @dev old and new allowance if approve() is called twice in quick succession. This property
+    /// @dev verifies the arithmetic correctness of the increase operation.
+    /// @custom:property-id ERC20-EXTERNAL-ALLOWANCE-MODIFY-051
     function test_ERC20external_setAndIncreaseAllowance(
         address target,
         uint256 initialAmount,
@@ -34,7 +71,16 @@ abstract contract CryticERC20ExternalIncreaseAllowanceProperties is
         );
     }
 
-    // Allowance should be modified correctly via increase/decrease
+    /// @title DecreaseAllowance Updates Allowance Correctly
+    /// @notice Decreasing allowance should subtract from the existing allowance value
+    /// @dev Testing Mode: EXTERNAL
+    /// @dev Invariant: After `decreaseAllowance(spender, amount)`, the allowance becomes
+    /// @dev `previousAllowance - amount`
+    /// @dev The decreaseAllowance() function provides a safer way to reduce allowances by
+    /// @dev decrementing the existing value rather than setting a new absolute value. This
+    /// @dev avoids race conditions and provides clearer intent when reducing permissions. This
+    /// @dev property verifies the arithmetic correctness of the decrease operation.
+    /// @custom:property-id ERC20-EXTERNAL-ALLOWANCE-MODIFY-052
     function test_ERC20external_setAndDecreaseAllowance(
         address target,
         uint256 initialAmount,

contracts/ERC20/external/properties/ERC20ExternalMintableProperties.sol

@@ -3,15 +3,52 @@ pragma solidity ^0.8.0;
 
 import "../util/ERC20ExternalTestBase.sol";
 
+/**
+ * @title ERC20 External Mintable Properties
+ * @author Crytic (Trail of Bits)
+ * @notice Properties for ERC20 tokens with mint functionality tested via external interface
+ * @dev Testing Mode: EXTERNAL (test harness interacts with token through external interface)
+ * @dev This contract contains 1 property that tests token minting mechanics via external
+ * @dev interface. The token's mint() function is called externally to verify proper balance
+ * @dev and supply updates.
+ * @dev
+ * @dev Usage Example:
+ * @dev ```solidity
+ * @dev contract TestHarness is CryticERC20ExternalMintableProperties {
+ * @dev     constructor() {
+ * @dev         // Deploy or reference your mintable ERC20 token
+ * @dev         token = ITokenMock(address(new MyMintableToken()));
+ * @dev     }
+ * @dev }
+ * @dev ```
+ */
 abstract contract CryticERC20ExternalMintableProperties is
     CryticERC20ExternalTestBase
 {
     constructor() {}
 
-    ////////////////////////////////////////
-    // Properties
 
-    // Minting tokens should update user balance and total supply
+    /* ================================================================
+
+                        MINT PROPERTIES
+
+       Description: Properties verifying token minting mechanics
+       Testing Mode: EXTERNAL
+       Property Count: 1
+
+       ================================================================ */
+
+    /// @title Mint Updates Balance and Supply Correctly
+    /// @notice Minting tokens should increase both recipient balance and total supply
+    /// @dev Testing Mode: EXTERNAL
+    /// @dev Invariant: After `mint(target, amount)`, `balanceOf(target)` increases by `amount`
+    /// @dev and `totalSupply()` increases by `amount`
+    /// @dev This ensures minted tokens are properly added to circulation and credited to the
+    /// @dev recipient, maintaining accurate accounting of total supply. The relationship between
+    /// @dev individual balances and total supply must be preserved during minting. New tokens
+    /// @dev are created from nothing and must be reflected in both the recipient's balance and
+    /// @dev the total circulating supply.
+    /// @custom:property-id ERC20-EXTERNAL-MINT-051
     function test_ERC20external_mintTokens(
         address target,
         uint256 amount

contracts/ERC20/external/properties/ERC20ExternalPausableProperties.sol

@@ -4,15 +4,51 @@ pragma solidity ^0.8.0;
 import "../util/ERC20ExternalTestBase.sol";
 import "../../../util/IHevm.sol";
 
+/**
+ * @title ERC20 External Pausable Properties
+ * @author Crytic (Trail of Bits)
+ * @notice Properties for ERC20 tokens with pause functionality tested via external interface
+ * @dev Testing Mode: EXTERNAL (test harness interacts with token through external interface)
+ * @dev This contract contains 2 properties that test pause/unpause mechanics via external
+ * @dev interface, ensuring transfers are blocked when the contract is paused. Uses hevm cheatcodes
+ * @dev to prank as the token owner for pause/unpause operations.
+ * @dev
+ * @dev Usage Example:
+ * @dev ```solidity
+ * @dev contract TestHarness is CryticERC20ExternalPausableProperties {
+ * @dev     constructor() {
+ * @dev         // Deploy or reference your pausable ERC20 token
+ * @dev         token = ITokenMock(address(new MyPausableToken()));
+ * @dev     }
+ * @dev }
+ * @dev ```
+ */
 abstract contract CryticERC20ExternalPausableProperties is
     CryticERC20ExternalTestBase
 {
     constructor() {}
 
-    ////////////////////////////////////////
-    // Properties
 
-    // Transfers should not be possible during paused state
+    /* ================================================================
+
+                        PAUSE PROPERTIES
+
+       Description: Properties verifying pause/unpause mechanics
+       Testing Mode: EXTERNAL
+       Property Count: 2
+
+       ================================================================ */
+
+    /// @title Transfer Must Fail When Paused
+    /// @notice Direct transfers should be blocked when contract is paused
+    /// @dev Testing Mode: EXTERNAL
+    /// @dev Invariant: When paused, `transfer(recipient, amount)` must return false or revert,
+    /// @dev and balances must remain unchanged
+    /// @dev The pause mechanism is a critical safety feature allowing contract administrators
+    /// @dev to halt all token transfers in emergency situations. This property ensures the pause
+    /// @dev works correctly by preventing any balance changes while paused. After testing, the
+    /// @dev contract is unpaused to restore normal operations.
+    /// @custom:property-id ERC20-EXTERNAL-PAUSE-051
     function test_ERC20external_pausedTransfer(
         address target,
         uint256 amount
@@ -42,7 +78,16 @@ abstract contract CryticERC20ExternalPausableProperties is
         token.unpause();
     }
 
-    // Transfers should not be possible during paused state
+    /// @title TransferFrom Must Fail When Paused
+    /// @notice Delegated transfers should be blocked when contract is paused
+    /// @dev Testing Mode: EXTERNAL
+    /// @dev Invariant: When paused, `transferFrom(owner, recipient, amount)` must return false
+    /// @dev or revert, and balances must remain unchanged
+    /// @dev Like direct transfers, delegated transfers via transferFrom must also be blocked
+    /// @dev during pause. This ensures complete halt of all token movements regardless of
+    /// @dev transfer method, maintaining pause integrity across all transfer mechanisms. After
+    /// @dev testing, the contract is unpaused to restore normal operations.
+    /// @custom:property-id ERC20-EXTERNAL-PAUSE-052
     function test_ERC20external_pausedTransferFrom(
         address target,
         uint256 amount

contracts/ERC20/internal/properties/ERC20BurnableProperties.sol

@@ -4,6 +4,26 @@ pragma solidity ^0.8.13;
 import "../util/ERC20TestBase.sol";
 import "@openzeppelin/contracts/token/ERC20/extensions/ERC20Burnable.sol";
 
+/**
+ * @title ERC20 Burnable Properties
+ * @author Crytic (Trail of Bits)
+ * @notice Properties for ERC20 tokens with burn functionality
+ * @dev Testing Mode: INTERNAL (test harness inherits from token and properties)
+ * @dev This contract contains 3 properties that test token burning mechanics,
+ * @dev including burn(), burnFrom(), and allowance updates during burns.
+ * @dev
+ * @dev Usage Example:
+ * @dev ```solidity
+ * @dev contract TestHarness is MyBurnableToken, CryticERC20BurnableProperties {
+ * @dev     constructor() {
+ * @dev         _mint(USER1, INITIAL_BALANCE);
+ * @dev         _mint(USER2, INITIAL_BALANCE);
+ * @dev         _mint(USER3, INITIAL_BALANCE);
+ * @dev         isMintableOrBurnable = true; // Must be true for burnable tokens
+ * @dev     }
+ * @dev }
+ * @dev ```
+ */
 abstract contract CryticERC20BurnableProperties is
     CryticERC20Base,
     ERC20Burnable
@@ -12,10 +32,25 @@ abstract contract CryticERC20BurnableProperties is
         isMintableOrBurnable = true;
     }
 
-    ////////////////////////////////////////
-    // Properties
 
-    // Burn should update user balance and total supply
+    /* ================================================================
+
+                        BURN PROPERTIES
+
+       Description: Properties verifying token burning mechanics
+       Testing Mode: INTERNAL
+       Property Count: 3
+
+       ================================================================ */
+
+    /// @title Burn Updates Balance and Supply Correctly
+    /// @notice Burning tokens should decrease both user balance and total supply
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: After `burn(amount)`, `balanceOf(burner)` decreases by `amount`
+    /// @dev and `totalSupply()` decreases by `amount`
+    /// @dev This ensures burned tokens are properly removed from circulation and cannot
+    /// @dev be recovered, maintaining accurate accounting of circulating supply.
+    /// @custom:property-id ERC20-BURN-001
     function test_ERC20_burn(uint256 amount) public {
         uint256 balance_sender = balanceOf(address(this));
         uint256 supply = totalSupply();
@@ -35,7 +70,14 @@ abstract contract CryticERC20BurnableProperties is
         );
     }
 
-    // Burn should update user balance and total supply
+    /// @title BurnFrom Updates Balance and Supply Correctly
+    /// @notice Burning tokens via burnFrom should decrease both owner balance and total supply
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: After `burnFrom(owner, amount)`, `balanceOf(owner)` decreases by `amount`
+    /// @dev and `totalSupply()` decreases by `amount`
+    /// @dev Delegated burning must maintain the same accounting guarantees as direct burning,
+    /// @dev ensuring tokens are permanently removed from circulation regardless of burn method.
+    /// @custom:property-id ERC20-BURN-002
     function test_ERC20_burnFrom(uint256 amount) public {
         uint256 balance_sender = balanceOf(msg.sender);
         uint256 allowance = allowance(msg.sender, address(this));
@@ -56,7 +98,15 @@ abstract contract CryticERC20BurnableProperties is
         );
     }
 
-    // burnFrom should update allowance
+    /// @title BurnFrom Decreases Allowance Correctly
+    /// @notice BurnFrom should consume the burner's allowance
+    /// @dev Testing Mode: INTERNAL
+    /// @dev Invariant: After `burnFrom(owner, amount)`, `allowance(owner, burner)` decreases by `amount`
+    /// @dev Exception: Allowance of `type(uint256).max` is treated as infinite by some implementations
+    /// @dev This prevents unauthorized burning beyond granted allowances. The burner must have
+    /// @dev sufficient allowance to burn tokens on behalf of the owner, and that allowance is
+    /// @dev consumed during the burn operation (unless infinite allowance is used).
+    /// @custom:property-id ERC20-BURN-003
     function test_ERC20_burnFromUpdateAllowance(uint256 amount) public {
         uint256 balance_sender = balanceOf(msg.sender);
         uint256 current_allowance = allowance(msg.sender, address(this));
@@ -65,7 +115,7 @@ abstract contract CryticERC20BurnableProperties is
 
         this.burnFrom(msg.sender, burn_amount);
 
-        // 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)),