Accelerate Development with AI

---
description: Any task involving assertion writing or testing of assertion writing. This will be all files in the "assertions/" folder
alwaysApply: false
---
# Phylax Credible Layer Assertion Rules

## Project Structure

### Directory Organization

```bash
project/
├── assertions/
│   ├── src/           # Assertion source files (.a.sol)
│   └── test/          # Assertion test files (.t.sol)
├── src/               # Protocol smart contracts
├── test/              # Protocol tests
├── script/            # Deployment scripts
├── foundry.toml       # Foundry configuration with assertions profile
└── remappings.txt     # Import remappings for dependencies
```

### File Naming Conventions

- Assertion files: `{ContractOrFeatureName}Assertion.a.sol`
- Test files: `{ContractOrFeatureName}Assertion.t.sol`
- Use descriptive names that indicate the component or module being protected

### Assertion Function Naming

- Assertion functions must start with `assertion{PropertyOrInvariant}`
- Examples: `assertionOwnershipChange`, `assertionBalanceInvariant`, `assertionHealthFactor`
- Use descriptive names that clearly indicate what property or invariant is being verified

### Foundry Configuration

```toml
[profile.assertions]
# Use assertions profile for pcl commands
# FOUNDRY_PROFILE=assertions pcl test

# Optional: Configure specific settings for assertions
# [profile.assertions]
# src = "assertions/src"
# test = "assertions/test"
# out = "out"
# libs = ["lib"]
# remappings = [
#     "credible-std/=lib/credible-std/src/",
#     "forge-std/=lib/forge-std/src/"
# ]
```

#### Profile Usage

- **Environment Variable**: Set `FOUNDRY_PROFILE=assertions` before running pcl commands
- **Command Line**: Use `FOUNDRY_PROFILE=assertions pcl test` to run tests with assertions profile
- **Purpose**: Ensures pcl commands use the correct configuration for assertion development
- **Separation**: Keeps assertion-specific settings separate from main project configuration

### Dependencies Setup

#### Installing credible-std

```bash
# Using git submodules (recommended)
git submodule add https://github.com/phylaxsystems/credible-std.git lib/credible-std

# Or using forge install
forge install phylaxsystems/credible-std
```

#### Remappings Configuration

Add to `remappings.txt`:

```bash
credible-std/=lib/credible-std/src/
forge-std/=lib/forge-std/src/
```

#### Required Dependencies

- `credible-std`: Core Credible Layer functionality
- `forge-std`: Forge standard library for testing
- `openzeppelin-contracts`: (optional, but recommended during development) For utility functions (Strings, etc.)

## Core Assertion Patterns

### Basic Assertion Structure

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

import {Assertion} from "credible-std/Assertion.sol";
import {AssertionSpec} from "credible-std/SpecRecorder.sol";
import {PhEvm} from "credible-std/PhEvm.sol";

contract ProtocolAssertion is Assertion {
    constructor() {
        registerAssertionSpec(AssertionSpec.Reshiram);
    }

    // Required: Register triggers for assertion functions
    function triggers() external view override {
        registerFnCallTrigger(this.assertionFunction.selector, Protocol.functionToMonitor.selector);
    }

    // Assertion function - must be public/external
    function assertionFunction() external view {
        // Get protocol instance
        Protocol protocol = Protocol(ph.getAssertionAdopter());

        // State comparison logic with explicit Reshiram snapshots
        uint256 preValue = uint256(ph.loadStateAt(address(protocol), SOME_VALUE_SLOT, _preTx()));
        uint256 postValue = uint256(ph.loadStateAt(address(protocol), SOME_VALUE_SLOT, _postTx()));

        // Require statements for invariants
        require(postValue >= preValue, "Descriptive error message");
    }
}
```

### Essential Cheatcodes

#### State Management

- `_preTx()` - Snapshot ID for state before the transaction
- `_postTx()` - Snapshot ID for state after the transaction
- `PhEvm.ForkId({forkType: 2, callIndex: callId})` - Snapshot ID for state before a specific call
- `PhEvm.ForkId({forkType: 3, callIndex: callId})` - Snapshot ID for state after a specific call
- `ph.loadStateAt(target, slot, fork)` - Read storage at a snapshot

#### Call Input Tracking

- `ph.getCallInputs(target, selector)` - Get all CALL opcode inputs
- `ph.getStaticCallInputs(target, selector)` - Get STATICCALL inputs
- `ph.getDelegateCallInputs(target, selector)` - Get DELEGATECALL inputs
- `ph.getCallCodeInputs(target, selector)` - Get CALLCODE inputs
- `ph.getAllCallInputs(target, selector)` - Get all call types (avoid double-counting)

#### State Change Tracking

- `ph.getStateChangesUint(target, slot)` - Track uint state changes
- `ph.getStateChangesAddress(target, slot)` - Track address state changes
- `ph.getStateChangesBytes32(target, slot)` - Track bytes32 state changes

#### Protocol Access

- `ph.getAssertionAdopter()` - Get the contract being protected

#### Storage Access

- `ph.loadStateAt(address, bytes32, fork)` - Read storage from an address at a specific snapshot
- **Note**: Use `ph.loadStateAt()` not `vm.load()` - the `vm` cheatcode is not available in assertions
- Useful for reading internal state variables that aren't exposed as public functions

#### Console Logs

- `import { console } from "credible-std/console.sol";` - Import the console library
- `console.log(string memory message)` - Log a string to the console
- You can use a string concatenation library like `Strings.toString` to log complex values

### Constructor Usage

- **Prefer `ph.getAssertionAdopter()` over constructors** for getting the protected contract address
- Constructors run against empty state and cannot read from other contracts
- Use constructors only for additional values your assertion needs (e.g., token addresses)
- If using constructor arguments, append them to creation code: `abi.encodePacked(type(Assertion).creationCode, abi.encode(arguments))`
- Constructor storage persists in the assertion contract

### Trigger Registration Patterns

#### Call Triggers

```solidity
function triggers() external view override {
    // Single function trigger
    registerFnCallTrigger(this.assertionFunction.selector, Protocol.functionToMonitor.selector);

    // Multiple functions trigger same assertion
    registerFnCallTrigger(this.assertionFunction.selector, Protocol.function1.selector);
    registerFnCallTrigger(this.assertionFunction.selector, Protocol.function2.selector);
}
```

#### Transaction End Triggers

```solidity
function triggers() external view override {
    // Trigger after transactions that touch the protected contract
    registerTxEndTrigger(this.assertionFunction.selector);
}
```

### Common Assertion Patterns

#### Pre/Post State Comparison

```solidity
function assertionStateInvariant() external view {
    Protocol protocol = Protocol(ph.getAssertionAdopter());

    uint256 preValue = uint256(ph.loadStateAt(address(protocol), SOME_VALUE_SLOT, _preTx()));
    uint256 postValue = uint256(ph.loadStateAt(address(protocol), SOME_VALUE_SLOT, _postTx()));

    require(postValue >= preValue, "Value cannot decrease");
}
```

#### Call Input Analysis

```solidity
function assertionCallValidation() external {
    Protocol protocol = Protocol(ph.getAssertionAdopter());

    PhEvm.CallInputs[] memory calls = ph.getCallInputs(
        address(protocol),
        protocol.functionToMonitor.selector
    );

    for (uint256 i = 0; i < calls.length; i++) {
        // Decode function parameters
        (uint256 param1, address param2) = abi.decode(calls[i].input, (uint256, address));

        // Validate parameters
        require(param1 > 0, "Parameter must be positive");
        require(param2 != address(0), "Address cannot be zero");
    }
}
```

#### Multi-Layered Validation

```solidity
function assertionComplexInvariant() external view {
    Protocol protocol = Protocol(ph.getAssertionAdopter());

    // Layer 1: Basic state check (cheapest)
    uint256 preBalance = uint256(ph.loadStateAt(address(protocol), BALANCE_SLOT, _preTx()));
    uint256 postBalance = uint256(ph.loadStateAt(address(protocol), BALANCE_SLOT, _postTx()));

    if (postBalance < preBalance) {
        // Layer 2: Detailed analysis only if basic check fails
        PhEvm.CallInputs[] memory calls = ph.getCallInputs(
            address(protocol),
            protocol.withdraw.selector
        );

        uint256 totalWithdrawn = 0;
        for (uint256 i = 0; i < calls.length; i++) {
            uint256 amount = abi.decode(calls[i].input, (uint256));
            totalWithdrawn += amount;
        }

        require(postBalance == preBalance - totalWithdrawn, "Balance mismatch");
    }
}
```

#### Intra-Transaction State Monitoring

```solidity
function assertionIntraTxOracleDeviation() external view {
    IOracle oracle = IOracle(ph.getAssertionAdopter());

    uint256 initialPrice = uint256(ph.loadStateAt(address(oracle), PRICE_SLOT, _preTx()));

    // Calculate allowed deviation thresholds
    uint256 maxAllowedPrice = (initialPrice * 110) / 100; // +10%
    uint256 minAllowedPrice = (initialPrice * 90) / 100;  // -10%

    uint256 finalPrice = uint256(ph.loadStateAt(address(oracle), PRICE_SLOT, _postTx()));
    require(
        finalPrice >= minAllowedPrice && finalPrice <= maxAllowedPrice,
        "Oracle final price deviation exceeds threshold"
    );

    // Get all price update calls in this transaction
    PhEvm.CallInputs[] memory priceUpdates = ph.getCallInputs(
        address(oracle),
        oracle.updatePrice.selector
    );

    // Check each intermediate state after each call
    for (uint256 i = 0; i < priceUpdates.length; i++) {
        uint256 intermediatePrice = uint256(ph.loadStateAt(
            address(oracle),
            PRICE_SLOT,
            PhEvm.ForkId({forkType: 3, callIndex: priceUpdates[i].id})
        ));
        require(
            intermediatePrice >= minAllowedPrice && intermediatePrice <= maxAllowedPrice,
            "Oracle intra-tx price deviation exceeds threshold"
        );
    }
}
```

## Testing Patterns

### Testing vs. Production Execution

Understanding the difference between testing and production is critical for writing effective tests.

**Production (On-Chain):**
- Transactions that fail assertions are dropped (never enter the blockchain)
- The `triggers()` function determines which assertions run based on function calls, storage changes, or balance changes
- All matching assertions for all interacted contracts execute
- Users don't see reverts - invalid transactions simply aren't included

**Testing (`cl.assertion()`):**
- Transactions that fail assertions revert (catchable with `vm.expectRevert()`)
- You specify which assertion function runs via `fnSelector`, but triggers still determine if it runs
- Only the specified assertion runs, only on the next external call
- Reverts simulate the production behavior of dropped transactions
- When an assertion passes, state changes persist for the rest of the test

**Key Mental Model:**

`cl.assertion()` works like `vm.prank()` - it affects only the immediately following external call, then the registration is consumed.

```solidity
// Testing: You specify which assertion function to run
// But the call must still match a registered trigger for that assertion
cl.assertion({
    adopter: address(protocol),
    createData: type(MyAssertion).creationCode,
    fnSelector: MyAssertion.assertDeposit.selector
});
protocol.deposit(100);  // Must match a trigger registered for assertDeposit
```

You must test each assertion function separately by specifying its selector and calling a function that matches its registered trigger.

### Test Structure

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

import {CredibleTest} from "credible-std/CredibleTest.sol";
import {Test} from "forge-std/Test.sol";
import {ProtocolAssertion} from "../src/ProtocolAssertion.a.sol";
import {Protocol} from "../../src/Protocol.sol";

contract TestProtocolAssertion is CredibleTest, Test {
    Protocol public assertionAdopter;
    ProtocolAssertion public assertion;

    function setUp() public {
        assertionAdopter = new Protocol();
        assertion = new ProtocolAssertion();

        // Setup test environment
        vm.deal(address(0xBEEF), 100 ether);
    }

    function testAssertionPasses() public {
        // Register assertion for next transaction
        cl.assertion({
            adopter: address(assertionAdopter),
            createData: type(ProtocolAssertion).creationCode,
            fnSelector: ProtocolAssertion.assertionFunction.selector
        });

        // Execute valid transaction
        vm.prank(address(0xBEEF));
        assertionAdopter.safeFunction();
    }

    function testAssertionFails() public {
        cl.assertion({
            adopter: address(assertionAdopter),
            createData: type(ProtocolAssertion).creationCode,
            fnSelector: ProtocolAssertion.assertionFunction.selector
        });

        // Execute invalid transaction
        vm.prank(address(0xBEEF));
        vm.expectRevert("Descriptive error message");
        assertionAdopter.unsafeFunction();
    }
}
```

### Testing Specifics

It is extremely important to understand that `cl.assertion()` runs only on the next function call.
So if you are testing `assertionAdopter.safeFunction`, there should be no other transaction between `cl.assertion` and that function call.
Any function calls that are used to setup the state for the test, should happen before `cl.assertion`.

Do:
```solidity
function testAssertionPasses() public {
    // Setup before cl.assertion
    vm.deal(address(0xBEEF), 100 ether);

    // Register assertion for next transaction
    cl.assertion({
        adopter: address(assertionAdopter),
        createData: type(ProtocolAssertion).creationCode,
        fnSelector: ProtocolAssertion.assertionFunction.selector
    });

    // Execute valid transaction
    vm.prank(address(0xBEEF));
    assertionAdopter.safeFunction(); // <-- Assertion run against this
}
```

Don't:
```solidity
function testAssertionPasses() public {
    // Register assertion for next transaction
    cl.assertion({
        adopter: address(assertionAdopter),
        createData: type(ProtocolAssertion).creationCode,
        fnSelector: ProtocolAssertion.assertionFunction.selector
    });

    // Setup after `cl.assertion`
    vm.deal(address(0xBEEF), 100 ether); // <-- Assertion run against this

    // Execute valid transaction
    vm.prank(address(0xBEEF));
    assertionAdopter.safeFunction();
}
```

- **One `cl.assertion()` can only trigger one assertion function per test**
- Each `cl.assertion()` call registers the assertion to run on the very next transaction only
- Create separate test functions for each assertion function that can be triggered
- Test each assertion function in isolation to ensure proper coverage
- Use different test scenarios for different assertion functions
- If you need to test multiple calls in one test, re-register the assertion before each call:

```solidity
function testMultipleOperations() public {
    // First assertion
    cl.assertion({...});
    protocol.operation1();
    
    // Re-register for second operation
    cl.assertion({...});
    protocol.operation2();
}
```

#### Inline Function Calls Consuming `vm.prank()`

**CRITICAL**: When you pass a function call as a parameter to another function, that inner call executes FIRST and consumes the `vm.prank()`.

```solidity
// ❌ WRONG - getBalance() executes first, consuming the prank
vm.prank(user);
protocol.withdraw(protocol.getBalance(user));
// Error: test contract (not user) tries to call withdraw

// ✅ CORRECT - Store result before prank
uint256 balance = protocol.getBalance(user);
vm.prank(user);
protocol.withdraw(balance);
```

**Why This Happens:**
- Solidity evaluates function parameters before executing the outer function
- `vm.prank()` only affects the NEXT external call
- The inner function call (e.g., `protocol.getBalance()`) is that "next call"
- By the time the outer function executes, the prank is already consumed

**Rule of Thumb:**
- Never inline view/pure function calls as parameters after `vm.prank()`
- Always store view function results in variables BEFORE calling `vm.prank()`
- This also applies to `cl.assertion()` - store any needed values first

### Testing Commands

- Use `pcl test` instead of `forge test` for assertion testing
- Use `FOUNDRY_PROFILE=assertions pcl test` to ensure correct profile
- Use `pcl build` to compile assertions
- **pcl test supports all forge test commands** for debugging:
  - `pcl test --match-test testFunctionName` - Run specific test function
  - `pcl test --match-contract TestContractName` - Run specific test contract
  - `pcl test path/to/test/file.t.sol` - Run specific test file
  - `pcl test -vvv` - Verbose output for debugging
  - Use these commands to isolate and debug specific test cases

### Testing Best Practices

- Test both positive (should pass) and negative (should fail) cases
- Use descriptive test function names
- Test edge cases and boundary conditions
- Use `vm.expectRevert()` with exact error messages
- Test with realistic data and scenarios
- **Utilize forge-std cheatcodes** for testing scenarios:
  - `vm.deal()` for minting ETH to addresses
  - `vm.prank()` for impersonating addresses
  - `vm.roll()` for manipulating block numbers
  - `vm.warp()` for manipulating timestamps
  - `vm.mockCall()` for mocking external calls
  - Use these tools to create comprehensive test scenarios

#### Avoid Helper Functions That Hide `vm.prank()`

Helper functions that internally call `vm.prank()` make it unclear when assertions actually execute and can accidentally consume the assertion trigger.

```solidity
// ❌ WRONG - Helper abstracts vm.prank
function updateState(uint256 value) internal {
    vm.prank(protocol.admin());
    protocol.updateState(value);
}

// In test - unclear what's happening
cl.assertion({...});
updateState(newValue); // Unclear when assertion executes

// ✅ CORRECT - Explicit vm.prank in test
cl.assertion({...});
vm.prank(protocol.admin());
protocol.updateState(newValue); // Crystal clear
```

**Rationale:**
- Explicit `vm.prank()` makes it obvious who is calling what
- No confusion about whether the assertion runs on the right transaction
- Tests are self-documenting and easier to debug

### Testing with Mock Protocols

- **It may not be possible to simulate failing assertion for well-implemented protocols** - this is expected behavior
- **Create mock protocols** that simulate vulnerable behavior to test assertion failure cases
- Use mock contracts that intentionally violate invariants to verify assertions catch violations
- Test assertion logic by temporarily removing safety checks in mock protocols
- This ensures assertions are working correctly even when the real protocol is secure

## Common Pitfalls and Anti-Patterns

### "Expected 1 assertion to be executed, but 0 were executed"

This error means the assertion never ran on the target transaction. Common causes:

1. **External call between `cl.assertion()` and target call** - Any external call after `cl.assertion()` consumes the assertion registration, even setup calls like `token.mint()` or `token.approve()`.

2. **Target transaction reverts before assertion runs** - The protocol function itself fails. Debug by removing `cl.assertion()` and testing the protocol function in isolation.

3. **Wrong adopter address** - The `adopter` parameter doesn't match the contract being called.

```solidity
// ❌ WRONG - token.approve() consumes the assertion
cl.assertion({...});
token.approve(address(protocol), amount);  // Assertion runs here!
protocol.deposit(amount);  // No assertion runs here

// ✅ CORRECT - All setup before cl.assertion()
token.approve(address(protocol), amount);
cl.assertion({...});
protocol.deposit(amount);  // Assertion runs here
```

### Gas Limit Issues

- Avoid expensive operations in loops
- Use early returns for basic checks
- Monitor gas usage with `pcl test`
- Be aware that the logs show the evm gas usage and the assertion gas usage, but they are not the same.
- Assertion gas limit is 300k.
- If assertion gas limit is exceeded, the assertion will revert with OutOfGas error.

### Call Input Double-Counting

```solidity
// ❌ WRONG: May include duplicate calls from proxy contracts
PhEvm.CallInputs[] memory calls = ph.getAllCallInputs(target, selector);

// ✅ CORRECT: Use specific call type
PhEvm.CallInputs[] memory calls = ph.getCallInputs(target, selector);
```

### Incorrect Function Selectors

```solidity
// ❌ WRONG: Using wrong selector or bytes signature
registerFnCallTrigger(this.assertionFunction.selector, bytes4(0x12345678));

// ✅ CORRECT: Use actual name of function selector
registerFnCallTrigger(this.assertionFunction.selector, Protocol.targetFunction.selector);
```

### Missing Error Messages

```solidity
// ❌ WRONG: No error message
require(condition);

// ✅ CORRECT: Descriptive error message
require(condition, "Specific invariant violation description");
```

### State Persistence in Tests

When an assertion **passes** (doesn't revert), the transaction's state changes persist for the rest of the test:

```solidity
function testStatePersistence() public {
    // First operation with assertion
    cl.assertion({
        adopter: address(protocol),
        createData: type(MyAssertion).creationCode,
        fnSelector: MyAssertion.assertDeposit.selector
    });
    vm.prank(user);
    protocol.deposit(100);
    
    // State persists - deposit is reflected
    assertEq(protocol.balance(user), 100);
    
    // Can register another assertion for the next operation
    cl.assertion({
        adopter: address(protocol),
        createData: type(MyAssertion).creationCode,
        fnSelector: MyAssertion.assertWithdraw.selector
    });
    vm.prank(user);
    protocol.withdraw(50);
    
    // Both operations' effects are visible
    assertEq(protocol.balance(user), 50);
}
```

When an assertion **fails** (reverts), the call is rolled back as with any Solidity revert.

## Best Practices

### General Solidity Practices

- **Regular Solidity best practices apply** to assertion contracts
- Follow standard coding conventions and patterns
- Use proper error handling and validation
- Implement clean, readable, and maintainable code
- Follow security best practices for smart contract development

### Single Responsibility

- Each assertion should verify one specific property
- Split complex assertions into multiple focused functions
- Use descriptive function names starting with "assertion" (see Assertion Function Naming section)

### Gas Optimization

- Assertions have 300k gas limit per assertion function
- Check basic invariants first (fail fast)
- Use early returns for simple checks
- Avoid expensive operations in loops
- Monitor gas usage during development

### Error Handling

- Use descriptive error messages
- Include context in error messages
- Test error conditions thoroughly

### Documentation

- Comment complex logic
- Follow best practice Solidity style for comments
- Explain the invariant being protected
- Document any assumptions or limitations
- Keep documentation in the code files, unless specified otherwise

Make sure to add comments to the assertion functions that explain the invaraint it's checking for as well as explaining how it works.
The same goes for the tests, make it clear which scenario a given test covers.

### Testing Coverage

- Test both valid and invalid scenarios
- Test edge cases and boundary conditions
- Test with realistic data
- Use fuzz testing for parameter validation
- Create separate tests for each assertion function (see Testing Specifics)

## Debugging Tips

### Console Logging

Use `console.log` to log debug information to the console during testing with `pcl test`.

### Gas Monitoring

- Use `pcl test -vvv` for detailed gas usage
- Monitor gas consumption in loops
- Optimize expensive operations

### Common Debugging Patterns

- Add intermediate state checks
- Use console.log for debugging
- Test with minimal examples
- Verify function selectors match expected signatures
- Write a test that doesn't use `cl.assertion` to mimic test behavior to verify if a problem is caused by the protocol function or the assertion function. Currently there is no good way to know if a revert happens because of the protocol function or the assertion function.

## Integration Guidelines

### Protocol Integration

- Use `ph.getAssertionAdopter()` instead of constructor parameters
- Ensure proper interface definitions
- Handle protocol-specific edge cases

### Deployment Workflow

1. Write and test assertions locally with `pcl test`
2. Deploy protocol contracts
3. Configure `credible.toml` with contract addresses and assertion mappings
4. Create a release on the Credible Layer with `pcl apply` (builds automatically)
5. Review your release and deploy it in the platform to activate assertions