Skip to content
Merged
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
181 changes: 97 additions & 84 deletions test/invariants/HandlerXanV1.t.sol
Original file line number Diff line number Diff line change
Expand Up @@ -2,123 +2,60 @@
pragma solidity ^0.8.30;

import {Test} from "forge-std/Test.sol";
import {ERC1967Proxy} from "@openzeppelin/contracts/proxy/ERC1967/ERC1967Proxy.sol";
import {XanV1} from "src/XanV1.sol";

import {XanV1} from "../../src/XanV1.sol";

contract XanV1Handler is Test {
XanV1 public token;
address public initialHolder;

// ============ GHOST VARIABLES (for invariant tracking) ============
address[] public actors;
mapping(address => bool) internal isActor;
address[] internal _actors;
mapping(address actor => bool isActor) internal _isActor;

// Valid implementation addresses for testing
address[5] public validImpls = [address(0x1111), address(0x2222), address(0x3333), address(0x4444), address(0x5555)];
address[5] internal _validImpls =
[address(0x1111), address(0x2222), address(0x3333), address(0x4444), address(0x5555)];

mapping(address => mapping(address => uint256)) internal previousVotes; // voter => impl => votes
mapping(address => uint256) internal previousLockedBalances;
uint256 internal previousLockedSupply;
mapping(address voter => mapping(address impl => uint256 previousVote)) internal _previousVotes;
mapping(address voter => uint256 previousLockedBalance) internal _previousLockedBalances;
uint256 internal _previousLockedSupply;

constructor(XanV1 _token, address _initialHolder) {
token = _token;
initialHolder = _initialHolder;
_addActor(_initialHolder);
}

// ============ HELPER FUNCTIONS ============

function _addActor(address a) internal {
if (!isActor[a]) {
isActor[a] = true;
actors.push(a);
}
}

function getActors() external view returns (address[] memory) {
return actors;
}

function getValidImpls() external view returns (address[5] memory) {
return validImpls;
}

function getPreviousVotes(address voter, address impl) external view returns (uint256) {
return previousVotes[voter][impl];
}

function getPreviousLockedBalance(address account) external view returns (uint256) {
return previousLockedBalances[account];
}

function getPreviousLockedSupply() external view returns (uint256) {
return previousLockedSupply;
}

function updateStateTracking() public {
// Update previous locked supply
previousLockedSupply = token.lockedSupply();

// Update previous locked balances and votes for all actors
for (uint256 i = 0; i < actors.length; i++) {
address actor = actors[i];
previousLockedBalances[actor] = token.lockedBalanceOf(actor);
// Capture votes across all implementations
for (uint256 j = 0; j < validImpls.length; j++) {
previousVotes[actor][validImpls[j]] = token.getVotes(actor, validImpls[j]);
}
}
}

function updateStateTrackingFor(address account) public {
// Update previous locked supply
previousLockedSupply = token.lockedSupply();

// Update previous locked balance and votes for a specific account
previousLockedBalances[account] = token.lockedBalanceOf(account);
for (uint256 j = 0; j < validImpls.length; j++) {
previousVotes[account][validImpls[j]] = token.getVotes(account, validImpls[j]);
}
}

function updateStateTrackingFor(address account1, address account2) public {
// Update previous locked supply
previousLockedSupply = token.lockedSupply();

// Update state for account1
previousLockedBalances[account1] = token.lockedBalanceOf(account1);
for (uint256 j = 0; j < validImpls.length; j++) {
previousVotes[account1][validImpls[j]] = token.getVotes(account1, validImpls[j]);
}

// Update state for account2
previousLockedBalances[account2] = token.lockedBalanceOf(account2);
for (uint256 j = 0; j < validImpls.length; j++) {
previousVotes[account2][validImpls[j]] = token.getVotes(account2, validImpls[j]);
}
}

// ============ FUZZED BUSINESS LOGIC FUNCTIONS ============

function airdrop(address to, uint256 amount) external {
// bounding to non-zero addresses, to avoid unnecessary reverts
to = address(uint160(bound(uint160(to), 1, type(uint160).max)));

_addActor(to);

uint256 unlocked = token.unlockedBalanceOf(initialHolder);
amount = bound(amount, 0, unlocked);

updateStateTrackingFor(initialHolder, to);

vm.prank(initialHolder);
token.transfer(to, amount);
}

function transfer(address from, address to, uint256 amount) external {
from = address(uint160(bound(uint160(from), 1, type(uint160).max)));
to = address(uint160(bound(uint160(to), 1, type(uint160).max)));

_addActor(from);
_addActor(to);

uint256 unlocked = token.unlockedBalanceOf(from);
amount = bound(amount, 0, unlocked);

updateStateTrackingFor(from, to);

vm.prank(from);
token.transfer(to, amount);
}
Expand All @@ -137,8 +74,10 @@ contract XanV1Handler is Test {
function transferAndLock(address from, address to, uint256 amount) external {
from = address(uint160(bound(uint160(from), 1, type(uint160).max)));
to = address(uint160(bound(uint160(to), 1, type(uint160).max)));

_addActor(from);
_addActor(to);

uint256 unlocked = token.unlockedBalanceOf(from);
amount = bound(amount, 0, unlocked);

Expand All @@ -154,8 +93,8 @@ contract XanV1Handler is Test {
_addActor(who);

// Restrict to only valid implementation addresses
implIndex = bound(implIndex, 0, validImpls.length - 1);
address impl = validImpls[implIndex];
implIndex = bound(implIndex, 0, _validImpls.length - 1);
address impl = _validImpls[implIndex];

updateStateTrackingFor(who);

Expand Down Expand Up @@ -198,8 +137,8 @@ contract XanV1Handler is Test {
// Council-only; prank as council.
address council = token.governanceCouncil();

implIndex = bound(implIndex, 0, validImpls.length - 1);
address impl = validImpls[implIndex];
implIndex = bound(implIndex, 0, _validImpls.length - 1);
address impl = _validImpls[implIndex];

updateStateTracking();

Expand All @@ -223,4 +162,78 @@ contract XanV1Handler is Test {
// Anyone can attempt; requires quorum/min-locked reached or will revert.
token.vetoCouncilUpgrade();
}

// ============ GETTER FUNCTIONS ============

function getActors() external view returns (address[] memory arr) {
arr = _actors;
}

function getValidImpls() external view returns (address[5] memory arr) {
arr = _validImpls;
}

function getPreviousVotes(address voter, address impl) external view returns (uint256 previousVotes) {
previousVotes = _previousVotes[voter][impl];
}

function getPreviousLockedBalance(address account) external view returns (uint256 previousLockedBalance) {
previousLockedBalance = _previousLockedBalances[account];
}

function getPreviousLockedSupply() external view returns (uint256 previousLockedSupply) {
previousLockedSupply = _previousLockedSupply;
}

// ============ HELPER FUNCTIONS ============

function updateStateTracking() public {
// Update previous locked supply
_previousLockedSupply = token.lockedSupply();

// Update previous locked balances and votes for all actors
for (uint256 i = 0; i < _actors.length; ++i) {
address actor = _actors[i];
_previousLockedBalances[actor] = token.lockedBalanceOf(actor);
// Capture votes across all implementations
for (uint256 j = 0; j < _validImpls.length; ++j) {
_previousVotes[actor][_validImpls[j]] = token.getVotes(actor, _validImpls[j]);
}
}
}

function updateStateTrackingFor(address account) public {
// Update previous locked supply
_previousLockedSupply = token.lockedSupply();

// Update previous locked balance and votes for a specific account
_previousLockedBalances[account] = token.lockedBalanceOf(account);
for (uint256 j = 0; j < _validImpls.length; ++j) {
_previousVotes[account][_validImpls[j]] = token.getVotes(account, _validImpls[j]);
}
}

function updateStateTrackingFor(address account1, address account2) public {
// Update previous locked supply
_previousLockedSupply = token.lockedSupply();

// Update state for account1
_previousLockedBalances[account1] = token.lockedBalanceOf(account1);
for (uint256 j = 0; j < _validImpls.length; ++j) {
_previousVotes[account1][_validImpls[j]] = token.getVotes(account1, _validImpls[j]);
}

// Update state for account2
_previousLockedBalances[account2] = token.lockedBalanceOf(account2);
for (uint256 j = 0; j < _validImpls.length; ++j) {
_previousVotes[account2][_validImpls[j]] = token.getVotes(account2, _validImpls[j]);
}
}

function _addActor(address a) internal {
if (!_isActor[a]) {
_isActor[a] = true;
_actors.push(a);
}
}
}
36 changes: 19 additions & 17 deletions test/invariants/InvariantXanV1.t.sol
Original file line number Diff line number Diff line change
@@ -1,42 +1,44 @@
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.30;

import {Test, StdInvariant} from "forge-std/Test.sol";
import {ERC1967Proxy} from "@openzeppelin/contracts/proxy/ERC1967/ERC1967Proxy.sol";
import {XanV1} from "src/XanV1.sol";

import {Test, StdInvariant} from "forge-std/Test.sol";

import {XanV1} from "../../src/XanV1.sol";
import {XanV1Handler} from "./HandlerXanV1.t.sol";

contract XanV1Invariants is StdInvariant, Test {
XanV1 public token;
XanV1Handler public handler;

address internal alice = makeAddr("alice");
address internal council = makeAddr("council");
address internal _alice = makeAddr("alice");
address internal _council = makeAddr("council");

function setUp() public {
// Deploy implementation
XanV1 impl = new XanV1();
// Deploy proxy with initializer
bytes memory init = abi.encodeWithSelector(XanV1.initializeV1.selector, alice, council);
bytes memory init = abi.encodeWithSelector(XanV1.initializeV1.selector, _alice, _council);
ERC1967Proxy proxy = new ERC1967Proxy(address(impl), init);
token = XanV1(payable(address(proxy)));

handler = new XanV1Handler(token, alice);
handler = new XanV1Handler(token, _alice);

// Register the handler for invariant fuzzing
targetContract(address(handler));
}

// PS-1: Locked balances never exceed total balances for any address
// Invariant: for all seen actors:
// - lockedBalance <= balance
// - unlockedBalance == balance - lockedBalance
// - sum(lockedBalances) == lockedSupply

function invariant_lockedAccountingHolds() public view {
function invariant_locked_accounting_holds() public view {
address[] memory actors = handler.getActors();
uint256 sumLocked = 0;

for (uint256 i = 0; i < actors.length; i++) {
for (uint256 i = 0; i < actors.length; ++i) {
uint256 balance = token.balanceOf(actors[i]);
uint256 locked = token.lockedBalanceOf(actors[i]);
uint256 unlocked = token.unlockedBalanceOf(actors[i]);
Expand All @@ -52,10 +54,10 @@ contract XanV1Invariants is StdInvariant, Test {

// PS-2: locked token transfer immutability =>
// Locked balances can never decrease (be transferred) for any address
function invariant_lockedBalanceMonotonicity() public view {
function invariant_locked_balance_monotonicity() public view {
address[] memory actors = handler.getActors();

for (uint256 i = 0; i < actors.length; i++) {
for (uint256 i = 0; i < actors.length; ++i) {
address account = actors[i];
uint256 currentLocked = token.lockedBalanceOf(account);
uint256 previousLocked = handler.getPreviousLockedBalance(account);
Expand All @@ -66,15 +68,15 @@ contract XanV1Invariants is StdInvariant, Test {

// PS-4: Vote monotonicity
// Individual vote counts can only increase (never decrease) for any voter-implementation pair
function invariant_voteMonotonicity() public view {
function invariant_vote_monotonicity() public view {
address[] memory actors = handler.getActors();
address[5] memory validImpls = handler.getValidImpls();

for (uint256 i = 0; i < actors.length; i++) {
for (uint256 i = 0; i < actors.length; ++i) {
address voter = actors[i];

// Check all valid implementation addresses to verify monotonicity
for (uint256 j = 0; j < validImpls.length; j++) {
for (uint256 j = 0; j < validImpls.length; ++j) {
address impl = validImpls[j];
uint256 currentVotes = token.getVotes(voter, impl);
uint256 previousVotes = handler.getPreviousVotes(voter, impl);
Expand All @@ -85,13 +87,13 @@ contract XanV1Invariants is StdInvariant, Test {
}

// PS-5: Upgrade mutual exclusion — never both scheduled at once
function invariant_upgradeMutualExclusion() public view {
function invariant_upgrade_mutual_exclusion() public view {
(address vImpl, uint48 vEnd) = token.scheduledVoterBodyUpgrade();
(address cImpl, uint48 cEnd) = token.scheduledCouncilUpgrade();
bool voterScheduled = (vImpl != address(0) && vEnd != 0);
bool councilScheduled = (cImpl != address(0) && cEnd != 0);
bool _councilScheduled = (cImpl != address(0) && cEnd != 0);

assertTrue(!(voterScheduled && councilScheduled), "both voter and council scheduled");
assertTrue(!(voterScheduled && _councilScheduled), "both voter and _council scheduled");
}

//PS-9 (upgrade cancellation token persistence) is implicitly proved by invariant tests above
Expand Down