Skip to content

Re routing example #180

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: cli-beta
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions CVLByExample/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@
| **override** | [`override`](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L1), [`definition`](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L8), [`function`](https://github.com/Certora/Examples/blob/master/CVLByExample/Import/certora/specs/sub.spec#L38) |
| **require** | [`require`](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L41) |
| **require_uint256**| [`require_uint256`](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Broken.spec#L156) |
| **rerouting summaries** | [Storage pointer rerouting](https://github.com/Certora/Examples/blob/master/CVLByExample/ReroutingSummaries/StoragePointerExample.spec#L8), [Internal function summarization](https://github.com/Certora/Examples/blob/master/CVLByExample/ReroutingSummaries/README.md) |
| **rule** | [Simple Rule](https://github.com/Certora/Examples/blob/master/DEFI/LiquidityPool/certora/specs/pool_havoc.spec#L27), parameterized [Simple Parameters](https://github.com/Certora/Examples/blob/master/DEFI/LiquidityPool/certora/specs/Full.spec#L78), [Method Parameter](https://github.com/Certora/Examples/blob/master/CVLByExample/Structs/BankAccounts/certora/specs/structs.spec#L95) |
| **satisfy** | [`satisfy`](https://github.com/Certora/Examples/blob/master/DEFI/ConstantProductPool/certora/spec/ConstantProductPool.spec#L252) |
| **selector** | [`selector`](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L92) |
Expand Down
95 changes: 95 additions & 0 deletions CVLByExample/ReroutingSummaries/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,95 @@
# Rerouting Summaries for Storage Pointers

## Overview

This example demonstrates **rerouting summaries**, a CVL feature that allows summarizing internal functions that take storage pointers as parameters. This is particularly useful when dealing with complex storage structures like mappings and arrays that cannot be easily converted between EVM and CVL representations.

## Problem Statement

In traditional CVL specifications, internal functions that accept storage pointers (especially mappings) are difficult to summarize because:
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
In traditional CVL specifications, internal functions that accept storage pointers (especially mappings) are difficult to summarize because:
Internal functions that accept storage pointers (especially mappings) can not be summarized to a CVL function that uses the arguments


1. **Storage pointers are not supported** for EVM → CVL conversions
2. **Mapping enumeration is impossible** - there's no way to systematically translate all key-value pairs
3. **Complex conversion code** would be needed to handle all possible splitting/unpacking scenarios

## Solution: Rerouting Summaries

Rerouting summaries solve this by allowing CVL specs to redirect internal function calls to external library methods:

```cvl
function Contract.internalFunction(...) internal => SomeLibrary.externalMethod(...)
```

The internal call is automatically rewritten to make an external delegate call to the library method, where storage pointers can be freely accessed and will correctly read/write the caller's storage.

## Files

- **`StoragePointerExample.sol`** - Contract with internal functions using storage pointers
- **`StoragePointerExample.spec`** - CVL specification with rerouting summaries
- **`StoragePointerExample.conf`** - Verification configuration

## Contract Structure

### Main Contract: `StoragePointerExample`

- **Storage**: `mapping(address => uint256[]) userDataArrays` - Main storage mapping
- **Internal Function**: `updateStorageInternal()` - Takes storage pointer and updates data
- **External Function**: `updateUserData()` - Public interface that calls internal function

### Library: `ReroutingLibrary`

- **Reroute Target**: `rerouteStorageUpdate()` - External function that handles the actual storage operations

## Key CVL Features Demonstrated

### 1. Rerouting Summary Syntax

```cvl
methods {
function StoragePointerExample.updateStorageInternal(
mapping(address => uint256[]) storage storageRef,
address user,
uint256[] memory newData
) internal returns (uint256[] memory) => ReroutingLibrary.rerouteStorageUpdate(storageRef, user, newData);
}
```

### 2. Storage Pointer Handling

The rerouting allows the library function to:
- Accept storage references as parameters
- Read from and write to the original contract's storage
- Maintain storage consistency across the rerouted call

### 3. Verification Rules

- **`testReroutingSummary`** - Verifies the rerouting works correctly
- **`testDataIntegrity`** - Ensures data isolation between different users
- **`testArrayBounds`** - Validates array length consistency

## Running the Verification

```bash
certoraRun StoragePointerExample.conf
```

## Expected Results

The verification should demonstrate that:

1. ✅ Internal function calls are successfully rerouted to the library
2. ✅ Storage operations work correctly through the rerouting
3. ✅ Data integrity is maintained across different storage locations
4. ✅ Array bounds and lengths are handled properly

## Benefits of Rerouting Summaries

1. **Handles Complex Storage** - Works with mappings and nested structures
2. **Maintains Storage Semantics** - Proper read/write access to original storage
3. **Simplifies Verification** - No need for complex EVM↔CVL conversions
4. **Flexible Summarization** - Can model complex internal logic externally

## Related Documentation

For more information on CVL and verification techniques, see:
- [Certora Documentation](https://docs.certora.com)
17 changes: 17 additions & 0 deletions CVLByExample/ReroutingSummaries/StoragePointerExample.conf
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
{
"files": [
"./StoragePointerExample.sol:StoragePointerExample",
"./StoragePointerExample.sol:ReroutingLibrary"
],
"loop_iter": "3",
"optimistic_loop": true,
"process": "emv",
"rule": [
"testReroutingSummary",
"testDataIntegrity",
"testArrayBounds"
],
"solc": "solc8.28",
"solc_via_ir": true,
"verify": "StoragePointerExample:./StoragePointerExample.spec"
}
85 changes: 85 additions & 0 deletions CVLByExample/ReroutingSummaries/StoragePointerExample.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,85 @@
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

/**
* @title Storage Pointer Rerouting Example
* @notice This contract demonstrates the use of rerouting summaries for internal functions
* that take storage pointers as parameters.
*/

// Library to handle rerouting of internal function calls
library ReroutingLibrary {
/**
* @notice Reroutes the internal storage update operation
* @param data Storage mapping reference
* @param user Address key for the mapping
* @param newValues New values to set
* @return The previous values before update
*/
function rerouteStorageUpdate(
mapping(address => uint256[]) storage data,
address user,
uint256[] memory newValues
) external returns (uint256[] memory) {
uint256[] memory previousValues = data[user];
data[user] = newValues;
return previousValues;
}
}

contract StoragePointerExample {
// Main storage mapping
mapping(address => uint256[]) public userDataArrays;

// Counter for tracking operations
uint256 public operationCounter;

/**
* @notice Internal function that updates storage using storage pointers
* @param storageRef Reference to the storage mapping
* @param user Address of the user
* @param newData New data to store
* @return Previous data before the update
*/
function updateStorageInternal(
mapping(address => uint256[]) storage storageRef,
address user,
uint256[] memory newData
) internal returns (uint256[] memory) {
uint256[] memory oldData = storageRef[user];
storageRef[user] = newData;
operationCounter++;
return oldData;
}

/**
* @notice External function that calls the internal storage update
* @param user Address of the user
* @param newData New data to store
* @return Previous data before the update
*/
function updateUserData(
address user,
uint256[] memory newData
) external returns (uint256[] memory) {
return updateStorageInternal(userDataArrays, user, newData);
}

/**
* @notice Get user data array
* @param user Address of the user
* @return User's data array
*/
function getUserData(address user) external view returns (uint256[] memory) {
return userDataArrays[user];
}

/**
* @notice Get the length of user's data array
* @param user Address of the user
* @return Length of the array
*/
function getUserDataLength(address user) external view returns (uint256) {
return userDataArrays[user].length;
}
}
108 changes: 108 additions & 0 deletions CVLByExample/ReroutingSummaries/StoragePointerExample.spec
Original file line number Diff line number Diff line change
@@ -0,0 +1,108 @@
// Storage Pointer Rerouting Specification
// CVL specification demonstrating rerouting summaries for internal functions
// that accept storage pointers as parameters.

methods {
// Rerouting summary: internal function calls are redirected to library methods
function StoragePointerExample.updateStorageInternal(
mapping(address => uint256[]) storage storageRef,
address user,
uint256[] memory newData
) internal returns (uint256[] memory) => ReroutingLibrary.rerouteStorageUpdate(storageRef, user, newData);

// External function declarations
function updateUserData(address, uint256[] memory) external returns (uint256[] memory);
function getUserData(address) external returns (uint256[] memory) envfree;
function getUserDataLength(address) external returns (uint256) envfree;
function operationCounter() external returns (uint256) envfree;
}

/**
* @notice Rule to verify that rerouting summary correctly handles storage updates
* @dev Tests that the internal function call is properly rerouted through the library
*/
rule testReroutingSummary(env e) {
address user;
uint256[] newData;

// Get initial state
uint256[] initialData = getUserData(user);
uint256 initialCounter = operationCounter();

// Call the external function that internally uses storage pointers
uint256[] returnedData = updateUserData(e, user, newData);

// Verify that the returned data matches the initial data
assert returnedData.length == initialData.length,
"Returned data length should match initial data length";

// Verify that the storage was updated with new data
uint256[] currentData = getUserData(user);
assert currentData.length == newData.length,
"Current data length should match new data length";

// Verify operation counter was incremented
assert operationCounter() == initialCounter + 1,
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

so this will fail, right?

"Operation counter should be incremented by 1";
}

/**
* @notice Rule to verify data integrity during storage pointer operations
*/
rule testDataIntegrity(env e) {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

what's interesting in this rule?

address user1;
address user2;
uint256[] data1;
uint256[] data2;

// Require different users
require user1 != user2;

// Get initial states
uint256[] initial1 = getUserData(user1);
uint256[] initial2 = getUserData(user2);

// Update user1's data
updateUserData(e, user1, data1);

// Verify user2's data wasn't affected
uint256[] afterUpdate2 = getUserData(user2);
assert afterUpdate2.length == initial2.length,
"User2 data should not be affected by user1 update";
}

/**
* @notice Rule to verify array bounds and length consistency
*/
rule testArrayBounds(env e) {
address user;
uint256[] newData;
uint256 index;

// Require valid index
require index < newData.length;
require newData.length > 0;

// Update user data
updateUserData(e, user, newData);

// Verify length consistency
uint256 storedLength = getUserDataLength(user);
uint256[] retrievedData = getUserData(user);

assert storedLength == retrievedData.length,
"Stored length should match retrieved array length";
assert storedLength == newData.length,
"Stored length should match input data length";
}

/**
* @notice Invariant to ensure operation counter only increases
*/
invariant operationCounterMonotonic()
operationCounter() >= 0
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

so with the summary it will not increase, right?

{
preserved {
require operationCounter() <= max_uint256 - 1;
}
}