### Solidity State Variable Inventory Example

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

An example of how to create an inventory of state variables in Solidity for property testing. This structure helps in systematically tracking and defining properties related to balances, protocol-specific metrics, and configuration parameters.

```solidity
struct StateInventory {
    // Balances
    mapping(address => uint256) balances;
    uint256 totalSupply;

    // Protocol-specific
    uint256 totalBorrowed;
    uint256 totalCollateral;

    // Configuration
    uint256 cap;
    uint256 fee;
}
```

--------------------------------

### Setup Protocol Environment in Solidity

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

Defines the base environment for property-based tests, including actor management, token funding, and protocol deployment. It provides helper functions for actor selection and input bounding.

```Solidity
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

import {BaseSetup} from "@chimera/BaseSetup.sol";

abstract contract Setup is BaseSetup {

    YourProtocol protocol;
    YourToken token;

    address[] internal actors;
    address internal currentActor;

    uint256 constant MIN_AMOUNT = 1e6;
    uint256 constant MAX_AMOUNT = 1e24;
    uint256 constant NUM_ACTORS = 3;

    function setup() internal virtual override {
        protocol = new YourProtocol();
        token = new YourToken();

        for (uint256 i = 0; i < NUM_ACTORS; i++) {
            address actor = address(uint160(0x10000 + i));
            actors.push(actor);
            deal(address(token), actor, 1000 ether);
            vm.prank(actor);
            token.approve(address(protocol), type(uint256).max);
        }
    }

    function _selectActor(uint8 seed) internal returns (address) {
        currentActor = actors[seed % actors.length];
        return currentActor;
    }

    function _bound(uint256 value, uint256 min, uint256 max) internal pure returns (uint256) {
        return min + (value % (max - min + 1));
    }
}
```

--------------------------------

### Quick Start Initialization Commands

Source: https://context7.com/0kn0t/properties_framework/llms.txt

Shell commands to initialize a Chimera-compatible project, set up directory structures, and execute fuzzing tests using Forge, Echidna, and Medusa.

```bash
forge install Recon-Fuzz/chimera
mkdir -p test/recon/{properties,targets,trophies}
cp lib/chimera/templates/* test/recon/
echidna test/recon/CryticTester.sol --contract CryticTester --config echidna.yaml
medusa fuzz --config medusa.json
forge test --match-test invariant
```

--------------------------------

### YAML Collection Format Example

Source: https://github.com/0kn0t/properties_framework/blob/main/02_PROPERTY_SCHEMA.md

An example of a property collection formatted in YAML. This format is often used for configuration files and provides a more human-readable alternative to JSON for defining property suites, categories, and individual property details.

```yaml
collection:
  name: Aave V3 Invariant Suite
  version: 1.0.0
  protocol: Aave
  protocolVersion: "3.3"
  tool: chimera

categories:
  - code: ACC
    name: Accounting
    properties:
      - AAVE_POOL_ACC_01
      - AAVE_POOL_ACC_02

properties:
  - id: AAVE_POOL_ACC_01
    name: aToken Supply-Balance Equality
    category: ACC
    subcategory: SUM
    type: INV
    description: >
      The total supply of aTokens must equal
      the sum of all user balances
    specification: aToken.totalSupply() == Σ balanceOf(user)
    assertion:
      operator: approx_eq
      left: aToken.totalSupply()
      right: sum(aToken.balanceOf(actor) for actor in actors)
      tolerance:
        formula: actors.length * 2
    severity: critical
    tags:
      - accounting
      - erc20
      - supply
    status: implemented
```

--------------------------------

### Configure Chimera Test Setup

Source: https://context7.com/0kn0t/properties_framework/llms.txt

Establishes the foundational environment for Chimera-compatible property testing. It handles protocol deployment, actor initialization, and funding within a Solidity contract.

```solidity
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

import {BaseSetup} from "@chimera/BaseSetup.sol";

abstract contract Setup is BaseSetup {
    YourProtocol protocol;
    YourToken token;

    address[] internal actors;
    address internal currentActor;

    uint256 constant MIN_AMOUNT = 1e6;
    uint256 constant MAX_AMOUNT = 1e24;
    uint256 constant NUM_ACTORS = 3;

    function setup() internal virtual override {
        protocol = new YourProtocol();
        token = new YourToken();

        for (uint256 i = 0; i < NUM_ACTORS; i++) {
            address actor = address(uint160(0x10000 + i));
            actors.push(actor);
            deal(address(token), actor, 1000 ether);
            vm.prank(actor);
            token.approve(address(protocol), type(uint256).max);
        }
    }

    function _selectActor(uint8 seed) internal returns (address) {
        currentActor = actors[seed % actors.length];
        return currentActor;
    }

    function _bound(uint256 value, uint256 min, uint256 max) internal pure returns (uint256) {
        return min + (value % (max - min + 1));
    }
}
```

--------------------------------

### State Transitions Property Example

Source: https://github.com/0kn0t/properties_framework/blob/main/00_MASTER_CAMPAIGN_LIST.md

Shows the State Transitions property, verifying that a smart contract adheres to a valid lifecycle state machine. This ensures predictable and secure contract behavior.

```Solidity
enum State { Created, Active, Paused, Closed }
State public currentState;

function transitionToActive() public {
    require(currentState == State.Created, "Invalid state transition");
    currentState = State.Active;
}

// Invariant check:
// Ensure currentState is always one of the defined enum values.
```

--------------------------------

### Sum Equality Property Example

Source: https://github.com/0kn0t/properties_framework/blob/main/00_MASTER_CAMPAIGN_LIST.md

Demonstrates the Sum Equality property pattern where the total supply of a token is equal to the sum of balances of all users. This is a common invariant in token contracts.

```Solidity
function totalSupply() public view returns (uint256) {
    return _totalSupply;
}

function balanceOf(address account) public view returns (uint256) {
    return _balances[account];
}

// Invariant check:
// require(totalSupply() == _balances.values().sum(), "Sum Equality Violation");
```

--------------------------------

### Property Naming and Assertion Helpers

Source: https://context7.com/0kn0t/properties_framework/llms.txt

Guidelines for naming properties using the Chimera convention and examples of using assertion helpers for boolean and comparison checks.

```solidity
// Naming Format: {PROTOCOL}_{MODULE}_{TYPE}_{ID}
t(condition, "PROPERTY_ID");
eq(a, b, "ID");
lt(a, b, "ID");
```

--------------------------------

### Generated Chimera Property Example (Solidity)

Source: https://github.com/0kn0t/properties_framework/blob/main/02_PROPERTY_SCHEMA.md

An example of a Solidity property generated using the Chimera template. This specific property checks for the equality between the total supply of aTokens and the sum of all user balances, with an approximate equality assertion to account for potential minor discrepancies.

```solidity
/// @notice The total supply of aTokens must equal the sum of all user balances
/// @dev Property ID: AAVE_POOL_ACC_01
/// @custom:category ACC
/// @custom:subcategory SUM
/// @custom:severity critical
function property_aave_pool_acc_01() public view returns (bool) {
    // Specification: aToken.totalSupply() == Σ balanceOf(user)
    uint256 sum;
    for (uint256 i = 0; i < actors.length; i++) {
        sum += aToken.balanceOf(actors[i]);
    }
    return _approxEq(aToken.totalSupply(), sum, actors.length * 2);
}
```

--------------------------------

### Balance Consistency Property Example

Source: https://github.com/0kn0t/properties_framework/blob/main/00_MASTER_CAMPAIGN_LIST.md

Illustrates the Balance Consistency property, ensuring that the actual balance of an asset is always greater than or equal to a virtual balance. This is crucial for preventing discrepancies in accounting.

```Solidity
mapping(address => uint256) private _balances;
mapping(address => uint256) private _virtualBalances;

// Invariant check:
// require(_balances[user] >= _virtualBalances[user], "Balance Consistency Violation");
```

--------------------------------

### Solidity Subscription Payment Access Control and Temporal Constraints

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

Tests access control (owner vs. unauthorized) and temporal constraints (payment window, interval) for subscription payments. It relies on Setup and Asserts contracts and interacts with an ISubExecutor interface. Inputs include owner, unauthorized addresses, and subscription parameters. Outputs are boolean success/failure indicators for tests.

```solidity
/// @title Subscription Payment Invariants
/// @notice Access control and temporal constraints for recurring payments

contract SubscriptionProperties is Setup, Asserts {

    ISubExecutor public subExecutor;
    address public owner;
    address public unauthorized;

    // Subscription params
    uint256 constant VALID_AFTER = 100;
    uint256 constant VALID_UNTIL = 1000;
    uint256 constant PAYMENT_INTERVAL = 50;

    /// @notice SUB_ACL_01: Owner can create subscriptions
    function property_SUB_ACL_01_owner_creates() public returns (bool) {
        vm.prank(owner);
        try subExecutor.createSubscription(
            subscriber, token, amount, PAYMENT_INTERVAL, VALID_UNTIL
        ) {
            return true;
        } catch {
            return false; // Owner should always succeed
        }
    }

    /// @notice SUB_ACL_02: Unauthorized cannot create
    function property_SUB_ACL_02_unauthorized_blocked() public returns (bool) {
        vm.prank(unauthorized);
        try subExecutor.createSubscription(
            subscriber, token, amount, PAYMENT_INTERVAL, VALID_UNTIL
        ) {
            return false; // Should have reverted
        } catch {
            return true; // Expected revert
        }
    }

    /// @notice SUB_TMP_01: Payment only valid within window
    function handler_testPaymentWindow(uint256 timestamp) external {
        timestamp = _bound(timestamp, 0, 2000);

        // Create subscription
        vm.prank(owner);
        uint256 subId = subExecutor.createSubscription(
            subscriber, token, amount, PAYMENT_INTERVAL, VALID_UNTIL
        );

        vm.warp(timestamp);

        bool canProcess = subExecutor.canProcessPayment(subId);

        if (timestamp < VALID_AFTER) {
            // Before window - should fail
            t(!canProcess, "SUB_TMP_01_BEFORE");
        } else if (timestamp > VALID_UNTIL) {
            // After expiry - should fail
            t(!canProcess, "SUB_TMP_01_AFTER");
        } else {
            // Within window - check interval
            uint256 lastPayment = subExecutor.lastPaymentTime(subId);
            if (timestamp < lastPayment + PAYMENT_INTERVAL) {
                t(!canProcess, "SUB_TMP_01_INTERVAL");
            }
        }
    }

    /// @notice SUB_TMP_02: Payment interval enforced
    function handler_testPaymentInterval(uint256 timeDelta) external {
        timeDelta = _bound(timeDelta, 1, 200);

        // Setup and first payment
        vm.prank(owner);
        uint256 subId = subExecutor.createSubscription(
            subscriber, token, amount, PAYMENT_INTERVAL, VALID_UNTIL
        );

        vm.warp(VALID_AFTER + 1);
        subExecutor.processPayment(subId);
        uint256 firstPaymentTime = block.timestamp;

        // Try second payment after timeDelta
        vm.warp(firstPaymentTime + timeDelta);

        bool canProcess = subExecutor.canProcessPayment(subId);

        if (timeDelta < PAYMENT_INTERVAL) {
            t(!canProcess, "SUB_TMP_02_TOO_EARLY");
        } else {
            t(canProcess, "SUB_TMP_02_SHOULD_PROCESS");
        }
    }
}

```

--------------------------------

### Monotonicity Property Example

Source: https://github.com/0kn0t/properties_framework/blob/main/00_MASTER_CAMPAIGN_LIST.md

Shows the Monotonicity property, where an accumulator value should always increase or stay the same over time. This is common in tracking cumulative metrics.

```Solidity
uint256 public accumulator;

function updateAccumulator(uint256 amount) public {
    uint256 _accumulator_before = accumulator;
    // ... update logic ...
    accumulator += amount;
    // Invariant check:
    // require(accumulator >= _accumulator_before, "Monotonicity Violation");
}
```

--------------------------------

### Price Direction Property Example

Source: https://github.com/0kn0t/properties_framework/blob/main/00_MASTER_CAMPAIGN_LIST.md

Illustrates the Price Direction property, where a specific condition (e.g., zeroForOne swap) implies a decrease in price. This is relevant in decentralized exchange (DEX) or oracle implementations.

```Solidity
function swap(bool zeroForOne, uint256 amountIn, uint256 amountOut) public {
    // ... swap logic ...
    // Invariant check:
    // if (zeroForOne) {
    //     require(price decreases, "Price Direction Violation");
    // }
}
```

--------------------------------

### Cap Enforcement Property Example

Source: https://github.com/0kn0t/properties_framework/blob/main/00_MASTER_CAMPAIGN_LIST.md

Demonstrates the Cap Enforcement property, ensuring that a specific value does not exceed a predefined cap. This is often used for limits on deposits, withdrawals, or total supply.

```Solidity
uint256 public constant MAX_CAP = 1_000_000 ether;
uint256 public currentValue;

function updateValue(uint256 amount) public {
    currentValue += amount;
    // Invariant check:
    // require(currentValue <= MAX_CAP, "Cap Enforcement Violation");
}
```

--------------------------------

### Roundtrip Loss Property Example

Source: https://github.com/0kn0t/properties_framework/blob/main/00_MASTER_CAMPAIGN_LIST.md

Demonstrates the Roundtrip Loss property, asserting that the result of a deposit followed by a redeem operation should be less than or equal to the initial deposit amount. This helps detect unintended value loss.

```Solidity
function deposit(uint256 amount) public {
    // ... deposit logic ...
}

function redeem(uint256 amount) public {
    // ... redeem logic ...
}

// Invariant check:
// uint256 initialAmount = 100 ether;
// deposit(initialAmount);
// uint256 redeemedAmount = redeem(initialAmount);
// require(redeemedAmount <= initialAmount, "Roundtrip Loss Violation");
```

--------------------------------

### Variable Name Patterns for AI Detection

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

This outlines variable naming conventions and their associated property types for AI detection. It provides a guide for how variable names like 'total*', '*Balance', '*Supply', etc., can indicate specific invariants or properties to check.

```plaintext
total*         → Aggregation property (sum equality)
*Balance       → Balance consistency check
*Supply        → Supply cap or sum equality
*Debt          → Debt accounting
*Rate          → Interest or exchange rate
*Ratio         → Collateralization check
*Cap/*Limit    → Boundary constraint
*Timestamp     → Temporal ordering
*Status/*State → State machine

```

--------------------------------

### Shortcut Composition Patterns in Solidity

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

Demonstrates pre-built action sequences for realistic composite operations, accelerating fuzzer exploration of deeper states. This pattern is implemented in Solidity and includes handlers for initializing a pool with liquidity, performing bidirectional swaps, and targeting overflow boundaries.

```solidity
/// @title Shortcut Composition - Realistic Action Sequences
/// @notice Accelerate fuzzer exploration of deeper states

contract ShortcutHandlers is ActionDispatcher {

    /// @notice Initialize pool + add liquidity in single call
    function handler_shortcut_initializeAndAddLiquidity(
        uint256 sqrtPriceSeed,
        int24 tickLower,
        int24 tickUpper,
        uint256 liquiditySeed
    ) external {
        uint160 sqrtPrice = uint160(_bound(sqrtPriceSeed, MIN_SQRT_PRICE, MAX_SQRT_PRICE));
        int256 liquidityDelta = int256(_bound(liquiditySeed, MIN_LIQUIDITY, MAX_LIQUIDITY));

        tickLower = _boundTick(tickLower);
        tickUpper = _boundTick(tickUpper);
        if (tickLower >= tickUpper) tickUpper = tickLower + TICK_SPACING;

        __before();

        pool.initialize(sqrtPrice);
        pool.modifyLiquidity(tickLower, tickUpper, liquidityDelta);

        __after();

        // HSPOST: Pool initialized with liquidity
        t(_after.liquidity > 0, "POOL_INIT_LIQ");
    }

    /// @notice Bidirectional swap (detect free token extraction)
    function handler_shortcut_swapRoundtrip(
        int256 amountSpecified,
        uint160 sqrtPriceLimitSeed
    ) external {
        amountSpecified = int256(_bound(uint256(amountSpecified), MIN_SWAP, MAX_SWAP));

        __before();
        uint256 token0Before = token0.balanceOf(currentActor);

        // Swap A -> B
        pool.swap(true, amountSpecified, MIN_SQRT_PRICE + 1);

        // Swap B -> A (reverse)
        pool.swap(false, -amountSpecified, MAX_SQRT_PRICE - 1);

        __after();
        uint256 token0After = token0.balanceOf(currentActor);

        // HSPOST: No free tokens from roundtrip
        lte(token0After, token0Before, "CONC_ACC_NO_FREE_TOKENS");
    }

    /// @notice Edge case: Pool at overflow boundary
    function handler_shortcut_targetedOverflowBoundary() external {
        __before();

        pool.initialize(MAX_SQRT_PRICE - 1);
        pool.modifyLiquidity(MAX_TICK - TICK_SPACING, MAX_TICK, type(int128).max);

        __after();

        // HSPOST: Still within bounds
        t(_after.sqrtPriceX96 <= MAX_SQRT_PRICE, "CONC_BND_OVERFLOW");
    }
}
```

--------------------------------

### Configure Scenario-Based Weight Adjustments in Solidity

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

Demonstrates how to configure handler weights for different protocol states. This allows for targeted testing of specific scenarios like normal operations versus default conditions.

```Solidity
contract NormalOperationsScenario is BaseInvariants {
    function setUp() public override {
        super.setUp();
        handler.setSelectorWeight("deposit", 3000);
        handler.setSelectorWeight("withdraw", 2000);
        handler.setSelectorWeight("borrow", 2500);
        handler.setSelectorWeight("triggerDefault", 0);
    }
}

contract DefaultScenario is BaseInvariants {
    function setUp() public override {
        super.setUp();
        handler.setSelectorWeight("deposit", 500);
        handler.setSelectorWeight("triggerDefault", 2000);
    }
}
```

--------------------------------

### Standard Directory Layout

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

The recommended file structure for a Chimera-based property testing project, organizing properties, targets, and test helpers.

```bash
test/recon/
├── properties/
│   ├── AccountingProperties.sol
│   ├── CollateralProperties.sol
│   └── StateProperties.sol
├── targets/
├── trophies/
├── BeforeAfter.sol
├── CryticTester.sol
├── CryticToFoundry.t.sol
├── PROPERTIES.md
├── Properties.sol
├── Setup.sol
└── TargetFunctions.sol
```

--------------------------------

### Implement Fuzzer Entry Points in Solidity

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

Provides a contract template to expose invariant functions to fuzzing tools like Echidna or Medusa. It inherits from the Properties contract and maps specific property functions to fuzzer-accessible entry points.

```solidity
contract CryticTester is Properties, CryticAsserts {
	constructor() {
		setup();
	}

	function echidna_supply_equals_balances() public returns (bool) {
		return property_supply_equals_balances();
	}
}
```

--------------------------------

### Implement CryticTester Entry Point

Source: https://context7.com/0kn0t/properties_framework/llms.txt

A Solidity contract serving as the central entry point for Echidna and Medusa. It inherits from Properties and CryticAsserts to expose specific property functions for the fuzzers.

```solidity
contract CryticTester is Properties, CryticAsserts {

    constructor() {
        setup();
    }

    function echidna_supply_equals_balances() public returns (bool) {
        return property_supply_equals_balances();
    }

    function echidna_solvency() public returns (bool) {
        return property_solvency();
    }

    function echidna_health_maintained() public returns (bool) {
        return property_health_maintained();
    }

    function echidna_supply_cap() public returns (bool) {
        return property_supply_cap();
    }
}
```

--------------------------------

### Health Enforcement Property Example

Source: https://github.com/0kn0t/properties_framework/blob/main/00_MASTER_CAMPAIGN_LIST.md

Illustrates the Health Enforcement property, ensuring that borrowers maintain a health factor greater than or equal to 1.0. This is critical in lending protocols to ensure solvency.

```Solidity
function getHealthFactor(address user) public view returns (uint256) {
    // ... calculation logic ...
}

// Invariant check:
// require(getHealthFactor(borrower) >= 1 ether, "Health Enforcement Violation");
```

--------------------------------

### Implement Dual-Mode Fuzzer Compatibility

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

Demonstrates how to write invariant tests that function simultaneously in Foundry and Echidna. It uses a base contract for logic and a wrapper contract to satisfy Echidna's specific naming requirements.

```Solidity
contract DualModeTests is Test {

    function invariant_supply_equals_balances() external returns (bool) {
        uint256 sum;
        for (uint256 i; i < actors.length; i++) {
            sum += token.balanceOf(actors[i]);
        }
        assertEq(token.totalSupply(), sum, "Supply mismatch");
        return !failed();
    }
}

contract EchidnaWrapper is DualModeTests {
    function echidna_supply_equals_balances() public returns (bool) {
        return invariant_supply_equals_balances();
    }
}
```

--------------------------------

### Callback-Based Action Dispatch in Solidity

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

Implements a system for queuing and executing a series of actions in batches, useful for complex multi-step operations like flash accounting. It defines an enum for action types and allows adding various actions such as SWAP, BURN, and SETTLE before executing them in a handler.

```solidity
/// @title Callback-Based Action Dispatch
/// @notice Queue actions then execute in batch (useful for flash accounting)

enum ActionType {
    MINT,
    BURN,
    SWAP,
    DONATE,
    MODIFY_LIQUIDITY,
    TAKE,
    SETTLE,
    SYNC
}

contract ActionDispatcher is TargetFunctions {

    ActionType[] public queuedActions;
    bytes[] public queuedParams;

    function addSwap(bool zeroForOne, int256 amountSpecified, uint160 sqrtPriceLimit) external {
        queuedActions.push(ActionType.SWAP);
        queuedParams.push(abi.encode(zeroForOne, amountSpecified, sqrtPriceLimit));
    }

    function addModifyLiquidity(int24 tickLower, int24 tickUpper, int256 liquidityDelta) external {
        queuedActions.push(ActionType.MODIFY_LIQUIDITY);
        queuedParams.push(abi.encode(tickLower, tickUpper, liquidityDelta));
    }

    function addSettle() external {
        queuedActions.push(ActionType.SETTLE);
        queuedParams.push("");
    }

    function handler_runActions() external {
        __before();

        for (uint256 i; i < queuedActions.length; i++) {
            _dispatch(queuedActions[i], queuedParams[i]);
        }

        __after();
        _checkPostconditions();

        // Clear queue
        delete queuedActions;
        delete queuedParams;
    }

    function _dispatch(ActionType action, bytes memory params) internal {
        if (action == ActionType.SWAP) {
            (bool zeroForOne, int256 amount, uint160 limit) =
                abi.decode(params, (bool, int256, uint160));
            pool.swap(zeroForOne, amount, limit);
        } else if (action == ActionType.MODIFY_LIQUIDITY) {
            (int24 lower, int24 upper, int256 delta) =
                abi.decode(params, (int24, int24, int256));
            pool.modifyLiquidity(lower, upper, delta);
        } else if (action == ActionType.SETTLE) {
            pool.settle();
        }
        // ... other actions
    }
}
```

--------------------------------

### Lending Handler Implementation - Solidity

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

Concrete implementation of the PAPHandler for a lending protocol's deposit function. It demonstrates how to implement preconditions, state snapshots, the deposit action, and postcondition checks, including ghost state updates. It inherits from PAPHandler and overrides its virtual functions.

```solidity
// Concrete implementation example
contract LendingHandler is PAPHandler {

    function handler_deposit(uint256 amount, uint8 actorSeed) external {
        // PHASE 1: Preconditions
        address actor = _selectActor(actorSeed);
        amount = _bound(amount, MIN_DEPOSIT, MAX_DEPOSIT);

        if (token.balanceOf(actor) < amount) return;
        if (pool.isPaused()) return;

        // PHASE 2: Snapshot
        __before();

        // PHASE 3: Action
        vm.prank(actor);
        try pool.deposit(amount, actor) returns (uint256 shares) {
            // PHASE 4: Postconditions
            __after();

            // HSPOST: Balance increased
            gte(_after.userBalance, _before.userBalance, "LEND_DIR_DEPOSIT_BAL");

            // HSPOST: Shares received
            gt(shares, 0, "LEND_ACC_DEPOSIT_SHARES");

            // HSPOST: Supply increased
            eq(_after.totalSupply, _before.totalSupply + shares, "LEND_ACC_DEPOSIT_SUPPLY");

            // Update ghost state
            ghost_totalDeposits[actor] += amount;
            ghost_totalShares[actor] += shares;

        } catch (bytes memory reason) {
            _handleRevert(reason);
        }
    }

    function _meetsPreconditions(address actor, uint256 param) internal view override returns (bool) {
        return token.balanceOf(actor) >= param && !pool.isPaused();
    }

    function _checkHandlerPostconditions(uint256 param) internal override {
        // Implemented inline in handler
    }

    function _updateGhostState(address actor, uint256 param) internal override {
        // Implemented inline in handler
    }

    function _handleExpectedFailure(bytes memory reason) internal override {
        _handleRevert(reason);
    }
}

```

--------------------------------

### Foundry Fuzzing and Invariant Testing Configuration

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

This TOML configuration file outlines settings for Foundry, a smart contract development toolkit. It includes default project settings, parameters for invariant testing such as runs and depth, and fuzzing parameters like runs and maximum test rejections.

```toml
# foundry.toml
[profile.default]
src = "src"
out = "out"
libs = ["lib"]
solc = "0.8.19"

[invariant]
runs = 256
depth = 100
fail_on_revert = false
shrink_run_limit = 5000

[fuzz]
runs = 10000
max_test_rejects = 65536

```

--------------------------------

### Implement Ghost Variable Tracking in Solidity

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

Demonstrates the use of ghost variables to track protocol state that is not explicitly stored on-chain. This pattern allows for the creation of invariants that compare internal ghost state against actual protocol state.

```solidity
abstract contract GhostTracking is Setup {
	uint256 public ghost_totalDeposited;

	function _updateGhostDeposit(address user, uint256 amount) internal {
		ghost_totalDeposited += amount;
		ghost_userDeposits[user] += amount;
	}

	function property_ghost_matches_protocol() public view returns (bool) {
		return ghost_totalDeposited - ghost_totalWithdrawn == protocol.totalAssets();
	}
}
```

--------------------------------

### Implement Property Verification Types in Solidity

Source: https://context7.com/0kn0t/properties_framework/llms.txt

Demonstrates the implementation of different property verification scopes, including Invariants checked between actions, Global Postconditions, and Handler-Specific Postconditions.

```solidity
// INVARIANT - Checked between every action
function property_supply_equals_balances() public view returns (bool) {
    uint256 sum;
    for (uint256 i = 0; i < actors.length; i++) {
        sum += token.balanceOf(actors[i]);
    }
    sum += token.balanceOf(address(protocol));
    return token.totalSupply() == sum;
}

// GLOBAL POSTCONDITION - Checked in __after() hook
function _checkGlobalPostconditions() internal override {
    gte(_after.liquidityIndex, _before.liquidityIndex, "GPOST_01_LIQ_INDEX");
    gte(_after.borrowIndex, _before.borrowIndex, "GPOST_01_BORROW_INDEX");
}

// HANDLER-SPECIFIC POSTCONDITION - Checked after specific handler
function handler_deposit(uint256 amount, uint8 actorSeed) external {
    __before();
    vm.prank(actor);
    try protocol.deposit(amount, actor) {
        __after();
        // HSPOST: Balance increased after deposit
        gte(_after.userBalance, _before.userBalance, "DEPOSIT_HSPOST_01");
    } catch {}
}
```

--------------------------------

### Implement Before/After State Snapshots

Source: https://context7.com/0kn0t/properties_framework/llms.txt

Provides a pattern for capturing contract state before and after function execution. This enables comparison-based assertions for verifying global postconditions.

```solidity
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

import {Setup} from "./Setup.sol";

abstract contract BeforeAfter is Setup {
    struct Vars {
        uint256 totalSupply;
        uint256 totalBorrowed;
        uint256 userBalance;
        uint256 userDebt;
        uint256 healthFactor;
        uint256 tcr;
        uint256 liquidityIndex;
        uint256 borrowIndex;
        uint256 timestamp;
        uint256 lastUpdate;
    }

    Vars internal _before;
    Vars internal _after;

    function __before() internal {
        _before = _captureState();
    }

    function __after() internal {
        _after = _captureState();
        _checkGlobalPostconditions();
    }

    function _captureState() internal view returns (Vars memory v) {
        v.totalSupply = token.totalSupply();
        v.totalBorrowed = protocol.totalBorrowed();
        v.userBalance = token.balanceOf(currentActor);
        v.userDebt = protocol.debtOf(currentActor);
        v.healthFactor = protocol.healthFactor(currentActor);
        v.liquidityIndex = protocol.liquidityIndex();
        v.borrowIndex = protocol.borrowIndex();
        v.timestamp = block.timestamp;
        v.lastUpdate = protocol.lastUpdate();
    }

    function _checkGlobalPostconditions() internal virtual;
}
```

--------------------------------

### Capture State Before and After Execution in Solidity

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

Implements a state-tracking mechanism to compare protocol variables before and after a transaction. It uses a custom struct to store protocol metrics and enforces global postconditions.

```Solidity
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

import {Setup} from "./Setup.sol";

abstract contract BeforeAfter is Setup {

    struct Vars {
        uint256 totalSupply;
        uint256 totalBorrowed;
        uint256 userBalance;
        uint256 userDebt;
        uint256 healthFactor;
        uint256 tcr;
        uint256 liquidityIndex;
        uint256 borrowIndex;
        uint256 timestamp;
        uint256 lastUpdate;
    }

    Vars internal _before;
    Vars internal _after;

    function __before() internal {
        _before = _captureState();
    }

    function __after() internal {
        _after = _captureState();
        _checkGlobalPostconditions();
    }

    function _captureState() internal view returns (Vars memory v) {
        v.totalSupply = token.totalSupply();
        v.totalBorrowed = protocol.totalBorrowed();
        v.userBalance = token.balanceOf(currentActor);
        v.userDebt = protocol.debtOf(currentActor);
        v.healthFactor = protocol.healthFactor(currentActor);
        v.liquidityIndex = protocol.liquidityIndex();
        v.borrowIndex = protocol.borrowIndex();
        v.timestamp = block.timestamp;
        v.lastUpdate = protocol.lastUpdate();
    }

    function _checkGlobalPostconditions() internal virtual;
}
```

--------------------------------

### Verify Price Movement Bounds and Consumption in Solidity

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

A collection of property-based tests for the Algebra Protocol's price movement logic. These functions validate that price updates move in the correct direction, remain stationary when at the target, and fully consume input amounts when the target is not reached.

```solidity
contract PriceMovementProperties is Asserts {

    /// @notice PRICE_DIR_01: Price movement direction matches swap direction
    function property_PRICE_DIR_01_movement_direction(
        uint160 sqrtPriceStart,
        uint160 sqrtPriceTarget,
        uint128 liquidity,
        int256 amountSpecified,
        uint24 feePips
    ) public pure returns (bool) {
        if (sqrtPriceStart == 0 || sqrtPriceTarget == 0) return true;
        if (feePips >= 1e6) return true; // Fee must be < 100%

        (uint160 sqrtPriceResult,,,) = PriceMovementMath.movePriceTowardsTarget(
            sqrtPriceStart, sqrtPriceTarget, liquidity, amountSpecified, feePips
        );

        // Price must move toward target (or stay if at target)
        if (sqrtPriceTarget <= sqrtPriceStart) {
            return sqrtPriceResult <= sqrtPriceStart && sqrtPriceResult >= sqrtPriceTarget;
        } else {
            return sqrtPriceResult >= sqrtPriceStart && sqrtPriceResult <= sqrtPriceTarget;
        }
    }

    /// @notice PRICE_BND_01: No movement when already at target
    function property_PRICE_BND_01_no_move_at_target(
        uint160 sqrtPrice,
        uint128 liquidity,
        int256 amountSpecified,
        uint24 feePips
    ) public pure returns (bool) {
        if (sqrtPrice == 0 || feePips >= 1e6) return true;

        (uint160 sqrtPriceResult, uint256 amountIn, uint256 amountOut, uint256 feeAmount) =
            PriceMovementMath.movePriceTowardsTarget(
                sqrtPrice, sqrtPrice, liquidity, amountSpecified, feePips
            );

        return sqrtPriceResult == sqrtPrice &&
               amountIn == 0 &&
               amountOut == 0 &&
               feeAmount == 0;
    }

    /// @notice PRICE_ACC_01: Full amount consumed when not reaching target
    function property_PRICE_ACC_01_full_consumption(
        uint160 sqrtPriceStart,
        uint160 sqrtPriceTarget,
        uint128 liquidity,
        int256 amountSpecified,
        uint24 feePips
    ) public pure returns (bool) {
        if (sqrtPriceStart == 0 || sqrtPriceTarget == 0) return true;
        if (sqrtPriceStart == sqrtPriceTarget) return true;
        if (feePips >= 1e6) return true;

        (uint160 sqrtPriceResult, uint256 amountIn, uint256 amountOut, uint256 feeAmount) =
            PriceMovementMath.movePriceTowardsTarget(
                sqrtPriceStart, sqrtPriceTarget, liquidity, amountSpecified, feePips
            );

        // If didn't reach target, must have consumed all input
        if (sqrtPriceResult != sqrtPriceTarget) {
            if (amountSpecified < 0) {
                return amountOut == uint256(-amountSpecified);
            } else {
                return amountIn + feeAmount == uint256(amountSpecified);
            }
        }

        return true;
    }
}
```

--------------------------------

### Implement Solidity Fuzzing Harness for Vyper Contracts

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

A Solidity contract that inherits from a Properties base to test Vyper-deployed tokens. It uses a VyperDeployer to instantiate contracts and defines invariant properties to verify ERC20 behavior.

```solidity
import {VyperDeployer} from "./utils/VyperDeployer.sol";
import {ITokenMock} from "./interfaces/ITokenMock.sol";

contract VyperERC20Properties is Properties {
    VyperDeployer constant VYPER_DEPLOYER = VyperDeployer(address(0x1234));
    ITokenMock public token;

    function setup() internal override {
        super.setup();
        bytes memory args = abi.encode("TestToken", "TT", 18, 1_000_000e18, "TestToken", "1");
        token = ITokenMock(VYPER_DEPLOYER.deployContract("src/tokens/", "ERC20", args));
    }

    function property_ERC20_ACC_01_supply_sum() public view returns (bool) {
        uint256 sum;
        for (uint256 i; i < actors.length; i++) {
            sum += token.balanceOf(actors[i]);
        }
        return token.totalSupply() == sum;
    }
}
```

--------------------------------

### Function Signature Patterns for AI Detection

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

This lists common function signatures and their corresponding property implications for AI analysis. It helps in understanding the expected behavior and invariants associated with functions like deposit, withdraw, borrow, repay, transfer, swap, and liquidate.

```plaintext
deposit(uint256 amount)     → Balance increase, supply increase
withdraw(uint256 amount)    → Balance decrease, supply decrease
borrow(uint256 amount)      → Debt increase, health decrease
repay(uint256 amount)       → Debt decrease, health increase
transfer(address, uint256)  → Conservation of value
swap(...)                   → Price movement direction
liquidate(...)              → Only if unhealthy

```

--------------------------------

### Implement Two-Level Weighted Distribution in Solidity

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

Provides fine-grained control over action probability at the handler and action level. It uses a weighted mapping system to dispatch actions based on a provided seed, ensuring total weights sum to a predefined range.

```solidity
abstract contract WeightedDistribution is Setup {

    uint256 constant HANDLER_WEIGHTS_RANGE = 100;
    uint256 constant ACTION_WEIGHTS_RANGE = 10_000;

    mapping(bytes4 => uint256) public actionWeights;
    uint256 public totalActionWeight;

    function setSelectorWeight(string memory sig, uint256 weight) external {
        bytes4 selector = bytes4(keccak256(bytes(sig)));
        totalActionWeight = totalActionWeight - actionWeights[selector] + weight;
        actionWeights[selector] = weight;
    }

    function _dispatchWeighted(uint256 seed) internal {
        require(totalActionWeight == ACTION_WEIGHTS_RANGE, "Weights must sum to 10000");

        uint256 roll = seed % ACTION_WEIGHTS_RANGE;
        uint256 cumulative;

        for (uint256 i; i < registeredSelectors.length; i++) {
            cumulative += actionWeights[registeredSelectors[i]];
            if (roll < cumulative) {
                _executeAction(registeredSelectors[i], seed);
                return;
            }
        }
    }
}
```

--------------------------------

### Pure Math Library Testing in Solidity

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

Tests mathematical libraries in isolation to verify specific properties and invariants. It includes checks for rounding direction and signed delta sign consistency with liquidity. Dependencies include the Asserts contract and the TokenDeltaMath library.

```solidity
/// @title Pure Math Library Testing Pattern
/// @notice Isolated math testing before full system integration

contract MathLibraryProperties is Asserts {

    /// @notice MATH_DIR_01: Rounding - roundUp >= roundDown always
    function property_MATH_DIR_01_rounding_direction(
        uint160 sqrtP,
        uint160 sqrtQ,
        uint128 liquidity
    ) public pure returns (bool) {
        if (sqrtP == 0 || sqrtQ == 0) return true;
        if (sqrtP < sqrtQ) (sqrtP, sqrtQ) = (sqrtQ, sqrtP);

        uint256 amountDown = TokenDeltaMath.getToken0Delta(sqrtQ, sqrtP, liquidity, false);
        uint256 amountUp = TokenDeltaMath.getToken0Delta(sqrtQ, sqrtP, liquidity, true);

        return amountDown <= amountUp && (amountUp - amountDown) < 2;
    }

    /// @notice MATH_DIR_02: Signed delta sign matches liquidity direction
    function property_MATH_DIR_02_signed_delta_direction(
        uint160 sqrtP,
        uint160 sqrtQ,
        int128 liquidity
    ) public pure returns (bool) {
        if (sqrtP == 0 || sqrtQ == 0) return true;

        int256 amount0 = TokenDeltaMath.getToken0Delta(sqrtQ, sqrtP, liquidity);

        if (liquidity < 0) return amount0 <= 0;
        if (liquidity > 0 && sqrtP != sqrtQ) return amount0 > 0;
        if (liquidity == 0) return amount0 == 0;

        return true;
    }

    /// @notice MATH_ACC_01: In-range positions need at least one token
    function property_MATH_ACC_01_inrange_requires_tokens(
        uint160 sqrtLower,
        uint160 sqrtCurrent,
        uint160 sqrtUpper,
        int128 liquidity
    ) public pure returns (bool) {
        if (sqrtLower == 0 || sqrtLower >= sqrtUpper) return true;
        if (sqrtCurrent < sqrtLower || sqrtCurrent > sqrtUpper) return true;
        if (liquidity <= 0) return true;

        int256 amount0 = TokenDeltaMath.getToken0Delta(sqrtCurrent, sqrtUpper, liquidity);
        int256 amount1 = TokenDeltaMath.getToken1Delta(sqrtLower, sqrtCurrent, liquidity);

        return amount0 > 0 || amount1 > 0;
    }
}
```

--------------------------------

### Solidity Code Patterns to Property Mapping for AI Detection

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

This section maps common Solidity code patterns to suggested properties for AI-driven detection. It covers patterns related to accounting, collateralization, boundary conditions, state machines, temporal ordering, access control, and oracle reliability.

```markdown
| Code Pattern | Suggested Property | Category |
|--------------|-------------------|----------|
| `mapping(address => uint256) balances` | Sum equality with totalSupply | Accounting |
| `uint256 public totalSupply` | Sum of balances check | Accounting |
| `require(healthFactor >= MIN)` | Health maintenance invariant | Collateralization |
| `uint256 public cap` | Cap enforcement | Boundary |
| `enum Status { A, B, C }` | State machine transitions | State Machine |
| `uint256 public lastUpdate` | Timestamp ordering | Temporal |
| `onlyOwner` modifier | Access control | Permissions |
| `price` or `oracle` | Price feed reliability | Oracle |

```

--------------------------------

### JSON Completeness Score Configuration

Source: https://github.com/0kn0t/properties_framework/blob/main/02_PROPERTY_SCHEMA.md

Configuration for calculating the completeness score of a property, outlining required fields, optional recommended fields, and the scoring logic based on field inclusion.

```json
{
  "completeness": {
    "required_fields": 6,
    "optional_recommended": [
      "specification",
      "variables",
      "scope",
      "severity",
      "implementation",
      "tags"
    ],
    "scoring": {
      "all_required": 60,
      "plus_specification": 70,
      "plus_variables": 75,
      "plus_scope": 80,
      "plus_severity": 85,
      "plus_implementation": 95,
      "plus_tags": 100
    }
  }
}
```

--------------------------------

### Verify Streaming Payment Invariants in Solidity

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

A collection of property-based testing functions and handlers designed to verify that net flow rates sum to zero and that total supply remains consistent during token upgrades or downgrades. It includes state-tracking mechanisms to detect failed liquidations and ensure system liveness.

```Solidity
contract StreamingFlowProperties is Properties {

    ISuperToken public superToken;
    address[] public streamAccounts;

    bool public liquidationFailed;
    uint256 public expectedTotalSupply;

    function property_STRM_ACC_01_net_flow_zero() public view returns (bool) {
        int96 netFlowSum;

        for (uint256 i; i < streamAccounts.length; i++) {
            netFlowSum += superToken.getNetFlowRate(streamAccounts[i]);
        }

        return netFlowSum == 0;
    }

    function property_STRM_ACC_02_supply_conservation() public view returns (bool) {
        return superToken.totalSupply() == expectedTotalSupply;
    }

    function property_STRM_ORC_01_liquidation_liveness() public view returns (bool) {
        return !liquidationFailed;
    }

    function handler_createFlow(uint8 senderSeed, uint8 receiverSeed, int96 flowRate) external {
        address sender = streamAccounts[senderSeed % streamAccounts.length];
        address receiver = streamAccounts[receiverSeed % streamAccounts.length];
        if (sender == receiver) return;

        flowRate = int96(_bound(uint256(uint96(flowRate)), MIN_FLOW, MAX_FLOW));

        __before();

        vm.prank(sender);
        try superToken.createFlow(receiver, flowRate) {
            __after();
        } catch {}
    }

    function handler_liquidate(uint8 senderSeed, uint8 receiverSeed) external {
        address sender = streamAccounts[senderSeed % streamAccounts.length];
        address receiver = streamAccounts[receiverSeed % streamAccounts.length];

        int96 flowRate = superToken.getFlowRate(sender, receiver);
        bool flowExists = flowRate > 0;

        (int256 availableBalance,,,) = superToken.realtimeBalanceOfNow(sender);
        bool isCritical = availableBalance < 0;

        bool shouldSucceed = flowExists && isCritical;

        __before();

        try superToken.liquidate(sender, receiver) {
            __after();
        } catch {
            if (shouldSucceed) {
                liquidationFailed = true;
            }
        }
    }
}
```

--------------------------------

### Perform Tolerance-Based Assertions in Solidity

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

Provides utilities for handling precision loss in fixed-point arithmetic. Includes relative, absolute, and combined tolerance checks to validate approximate equality.

```Solidity
abstract contract ToleranceAsserts is Asserts {
    function assertApproxEqRel(uint256 a, uint256 b, uint256 maxPercentDelta, string memory id) internal {
        if (b == 0) { t(a == 0, id); return; }
        uint256 delta = a > b ? a - b : b - a;
        uint256 percentDelta = (delta * 1e18) / b;
        t(percentDelta <= maxPercentDelta, id);
    }

    function assertApproxEqAbs(uint256 a, uint256 b, uint256 maxDelta, string memory id) internal {
        uint256 delta = a > b ? a - b : b - a;
        t(delta <= maxDelta, id);
    }

    function assertWithinDiff(uint256 a, uint256 b, uint256 scale, string memory id) internal {
        uint256 delta = a > b ? a - b : b - a;
        uint256 relativeComponent = (a + b) / 1e9;
        uint256 absoluteComponent = scale > 1e12 ? scale : 1e12;
        t(delta <= relativeComponent + absoluteComponent, id);
    }
}
```

--------------------------------

### Implement Shadow Accounting Pattern in Solidity

Source: https://github.com/0kn0t/properties_framework/blob/main/03_COMPREHENSIVE_FRAMEWORK.md

A pattern for detecting exploitation in gas-optimized indirect accounting by maintaining a parallel shadow state. It verifies that shadow deltas match the protocol's actual accounting state.

```Solidity
abstract contract ShadowAccounting is Setup {
    mapping(address => mapping(address => int256)) public shadowDeltas;
    mapping(bytes32 => uint256) public shadowPoolLiquidity;

    function _updateShadowState(address actor, address currency, int256 delta) internal {
        shadowDeltas[actor][currency] += delta;
    }

    function _verifyShadowVsActual() internal view {
        for (uint256 i = 0; i < actors.length; i++) {
            int256 shadowDelta = shadowDeltas[actors[i]][currency];
            int256 actualDelta = protocol.currencyDelta(actors[i], currency);
            assert(shadowDelta == actualDelta);
        }
    }
}
```