Skip to content

Instantly share code, notes, and snippets.

@devtooligan

devtooligan/CCAFuzzTestERC20.sol

Created January 7, 2026 03:45
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save devtooligan/e41bd158331de9b4a50fad4417b977d9 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save devtooligan/e41bd158331de9b4a50fad4417b977d9 to your computer and use it in GitHub Desktop.
Download ZIP
Echidna Fuzzing Suite for ContinuousClearingAuction
Raw
CCAFuzzTestERC20.sol
// SPDX-License-Identifier: MIT
pragma solidity 0.8.26;
import {ContinuousClearingAuction} from '../../src/ContinuousClearingAuction.sol';
import {AuctionParameters} from '../../src/interfaces/IContinuousClearingAuction.sol';
import {FixedPoint96} from '../../src/libraries/FixedPoint96.sol';
import {Checkpoint} from '../../src/libraries/CheckpointLib.sol';
import {Bid} from '../../src/libraries/BidLib.sol';
/// @notice Simple ERC20 token for auction token
contract AuctionToken {
mapping(address => uint256) public balanceOf;
uint256 public totalSupply;
function mint(address to, uint256 amount) external {
balanceOf[to] += amount;
totalSupply += amount;
}
function transfer(address to, uint256 amount) external returns (bool) {
require(balanceOf[msg.sender] >= amount, "Insufficient balance");
balanceOf[msg.sender] -= amount;
balanceOf[to] += amount;
return true;
}
function approve(address, uint256) external pure returns (bool) {
return true;
}
function transferFrom(address from, address to, uint256 amount) external returns (bool) {
require(balanceOf[from] >= amount, "Insufficient balance");
balanceOf[from] -= amount;
balanceOf[to] += amount;
return true;
}
}
/// @notice ERC20 currency token for payments
contract CurrencyToken {
mapping(address => uint256) public balanceOf;
mapping(address => mapping(address => uint256)) public allowance;
uint256 public totalSupply;
function mint(address to, uint256 amount) external {
balanceOf[to] += amount;
totalSupply += amount;
}
function transfer(address to, uint256 amount) external returns (bool) {
require(balanceOf[msg.sender] >= amount, "Insufficient balance");
balanceOf[msg.sender] -= amount;
balanceOf[to] += amount;
return true;
}
function approve(address spender, uint256 amount) external returns (bool) {
allowance[msg.sender][spender] = amount;
return true;
}
function transferFrom(address from, address to, uint256 amount) external returns (bool) {
require(balanceOf[from] >= amount, "Insufficient balance");
require(allowance[from][msg.sender] >= amount, "Insufficient allowance");
allowance[from][msg.sender] -= amount;
balanceOf[from] -= amount;
balanceOf[to] += amount;
return true;
}
}
/// @title CCAFuzzTestERC20
/// @notice Echidna fuzz test for ContinuousClearingAuction with ERC20 currency
contract CCAFuzzTestERC20 {
// ============================================
// CONSTANTS
// ============================================
uint256 public constant TICK_SPACING = 100 << FixedPoint96.RESOLUTION;
uint256 public constant FLOOR_PRICE = 1000 << FixedPoint96.RESOLUTION;
uint128 public constant TOTAL_SUPPLY = 1000e18;
uint256 public constant AUCTION_DURATION = 100;
uint256 public constant MAX_BIDS = 50;
uint256 public constant NUM_ACTORS = 5;
uint256 public constant CURRENCY_PER_ACTOR = 1e24;
uint256 public constant INITIAL_CURRENCY_SUPPLY = (NUM_ACTORS + 1) * CURRENCY_PER_ACTOR; // actors + test contract
// ============================================
// CONTRACTS
// ============================================
ContinuousClearingAuction public auction;
AuctionToken public auctionToken;
CurrencyToken public currencyToken;
// ============================================
// ACTORS
// ============================================
address[] public actors;
// ============================================
// STATE TRACKING
// ============================================
uint256[] public bidIds;
uint256 public bidCount;
mapping(uint256 => bool) public bidExited;
mapping(uint256 => bool) public bidClaimed;
mapping(uint256 => uint256) public bidOriginalAmount;
mapping(uint256 => uint256) public bidRefundAmount;
// Ghost variables
uint256 public ghost_totalCurrencyDeposited;
uint256 public ghost_totalCurrencyRefunded;
uint256 public ghost_totalTokensClaimed;
// Clearing price tracking
uint256 public lastObservedClearingPrice;
uint24 public lastObservedCumulativeMps;
// Invariant flags
bool public invariant_avgPriceViolation;
bool public invariant_refundViolation;
bool public invariant_tokenFilledViolation;
// ============================================
// CONSTRUCTOR
// ============================================
constructor() {
// Initialize actors
for (uint256 i = 0; i < NUM_ACTORS; i++) {
actors.push(address(uint160(0x10000 + i)));
}
// Deploy tokens
auctionToken = new AuctionToken();
currencyToken = new CurrencyToken();
// Build auction steps data (MPS = 10,000,000 total)
bytes memory auctionStepsData = abi.encodePacked(
uint24(100_000), uint40(50),
uint24(100_000), uint40(50)
);
// Deploy auction with ERC20 currency (NOT address(0))
AuctionParameters memory params = AuctionParameters({
currency: address(currencyToken), // <-- ERC20 currency!
floorPrice: FLOOR_PRICE,
tickSpacing: TICK_SPACING,
validationHook: address(0),
tokensRecipient: address(0xBEEF),
fundsRecipient: address(0xCAFE),
startBlock: 1,
endBlock: 1 + uint64(AUCTION_DURATION),
claimBlock: 1 + uint64(AUCTION_DURATION) + 10,
requiredCurrencyRaised: 0,
auctionStepsData: auctionStepsData
});
auction = new ContinuousClearingAuction(address(auctionToken), TOTAL_SUPPLY, params);
// Mint auction tokens and notify
auctionToken.mint(address(auction), TOTAL_SUPPLY);
auction.onTokensReceived();
// Mint currency tokens to actors and test contract
for (uint256 i = 0; i < NUM_ACTORS; i++) {
currencyToken.mint(actors[i], 1e24);
}
currencyToken.mint(address(this), 1e24);
// Approve auction to spend our currency
currencyToken.approve(address(auction), type(uint256).max);
}
// ============================================
// HELPER FUNCTIONS
// ============================================
function getActor(uint256 seed) public view returns (address) {
return actors[seed % NUM_ACTORS];
}
function isAuctionActive() public view returns (bool) {
return block.number >= auction.startBlock() && block.number < auction.endBlock();
}
function isAuctionEnded() public view returns (bool) {
return block.number >= auction.endBlock();
}
function canClaimTokens() public view returns (bool) {
return block.number >= auction.claimBlock();
}
// ============================================
// HANDLER FUNCTIONS - ACTIVE AUCTION PHASE
// ============================================
/// @notice Handler to call checkpoint
function handler_checkpoint() public {
if (block.number < auction.startBlock()) return;
try auction.checkpoint() {
uint256 currentPrice = auction.clearingPrice();
lastObservedClearingPrice = currentPrice;
Checkpoint memory cp = auction.checkpoints(auction.lastCheckpointedBlock());
lastObservedCumulativeMps = cp.cumulativeMps;
} catch {}
}
/// @notice Handler to submit a bid with ERC20 currency
function handler_submitBid(uint256 actorSeed, uint256 maxPriceSeed, uint256 amountSeed) public {
if (!isAuctionActive()) return;
if (bidCount >= MAX_BIDS) return;
address actor = getActor(actorSeed);
uint256 tickNumber = 1 + (maxPriceSeed % 100);
uint256 maxPrice = FLOOR_PRICE + tickNumber * TICK_SPACING;
if (maxPrice <= auction.clearingPrice()) return;
uint128 amount = uint128(1e15 + (amountSeed % 1e20));
// Check we have enough currency
if (currencyToken.balanceOf(address(this)) < amount) return;
// Submit bid - ERC20 version (no msg.value)
try auction.submitBid(maxPrice, amount, actor, FLOOR_PRICE, bytes('')) returns (uint256 bidId) {
bidIds.push(bidId);
bidCount++;
bidOriginalAmount[bidId] = amount;
ghost_totalCurrencyDeposited += amount;
} catch {}
}
/// @notice Handler to force iterate over ticks
function handler_forceIterateOverTicks(uint256 tickNumberSeed) public {
if (block.number < auction.startBlock()) return;
uint256 tickNumber = 1 + (tickNumberSeed % 100);
uint256 untilTickPrice = FLOOR_PRICE + tickNumber * TICK_SPACING;
try auction.forceIterateOverTicks(untilTickPrice) {} catch {}
}
// ============================================
// HANDLER FUNCTIONS - POST-AUCTION PHASE
// ============================================
/// @notice Handler to exit a fully filled bid
function handler_exitBid(uint256 bidIndexSeed) public {
if (!isAuctionEnded()) return;
if (bidCount == 0) return;
uint256 index = bidIndexSeed % bidCount;
uint256 bidId = bidIds[index];
if (bidExited[bidId]) return;
Bid memory bid = auction.bids(bidId);
if (bid.maxPrice <= auction.clearingPrice()) return;
uint256 ownerBalanceBefore = currencyToken.balanceOf(bid.owner);
uint256 originalAmount = bidOriginalAmount[bidId];
try auction.exitBid(bidId) {
bidExited[bidId] = true;
uint256 refunded = currencyToken.balanceOf(bid.owner) - ownerBalanceBefore;
bidRefundAmount[bidId] = refunded;
ghost_totalCurrencyRefunded += refunded;
Bid memory exitedBid = auction.bids(bidId);
// INVARIANT: Refund cannot exceed original deposit
if (refunded > originalAmount) {
invariant_refundViolation = true;
}
// INVARIANT: Average price <= maxPrice
if (exitedBid.tokensFilled > 0) {
uint256 currencySpent = originalAmount - refunded;
uint256 maxValueAtBidPrice = (exitedBid.tokensFilled * exitedBid.maxPrice) / FixedPoint96.Q96;
if (currencySpent > maxValueAtBidPrice + 1e6) {
invariant_avgPriceViolation = true;
}
}
// INVARIANT: TokensFilled <= maximum possible
uint256 maxTokensPossible = (originalAmount * FixedPoint96.Q96) / auction.floorPrice();
if (exitedBid.tokensFilled > maxTokensPossible) {
invariant_tokenFilledViolation = true;
}
} catch {}
}
/// @notice Handler to exit a partially filled bid
function handler_exitPartiallyFilledBid(uint256 bidIndexSeed) public {
if (!isAuctionEnded()) return;
if (bidCount == 0) return;
try auction.checkpoint() {} catch {}
uint256 index = bidIndexSeed % bidCount;
uint256 bidId = bidIds[index];
if (bidExited[bidId]) return;
Bid memory bid = auction.bids(bidId);
if (bid.maxPrice > auction.clearingPrice()) return;
uint256 ownerBalanceBefore = currencyToken.balanceOf(bid.owner);
uint256 originalAmount = bidOriginalAmount[bidId];
// Use 0, 0 hints - will likely fail but tests the path
try auction.exitPartiallyFilledBid(bidId, 0, 0) {
bidExited[bidId] = true;
uint256 refunded = currencyToken.balanceOf(bid.owner) - ownerBalanceBefore;
bidRefundAmount[bidId] = refunded;
ghost_totalCurrencyRefunded += refunded;
if (refunded > originalAmount) {
invariant_refundViolation = true;
}
} catch {}
}
/// @notice Handler to sweep currency
function handler_sweepCurrency() public {
if (!isAuctionEnded()) return;
try auction.sweepCurrency() {} catch {}
}
/// @notice Handler to sweep unsold tokens
function handler_sweepUnsoldTokens() public {
if (!isAuctionEnded()) return;
try auction.sweepUnsoldTokens() {} catch {}
}
/// @notice Handler to claim tokens
function handler_claimTokens(uint256 bidIndexSeed) public {
if (!canClaimTokens()) return;
if (bidCount == 0) return;
uint256 index = bidIndexSeed % bidCount;
uint256 bidId = bidIds[index];
if (!bidExited[bidId]) return;
if (bidClaimed[bidId]) return;
Bid memory bid = auction.bids(bidId);
try auction.claimTokens(bidId) {
bidClaimed[bidId] = true;
ghost_totalTokensClaimed += bid.tokensFilled;
} catch {}
}
// ============================================
// INVARIANTS
// ============================================
/// @notice INVARIANT: Clearing price must always be >= floor price
function echidna_clearingPriceAboveFloor() public view returns (bool) {
return auction.clearingPrice() >= auction.floorPrice();
}
/// @notice INVARIANT: Total tokens cleared cannot exceed total supply
function echidna_totalClearedNotExceedTotalSupply() public view returns (bool) {
return auction.totalCleared() <= auction.totalSupply();
}
/// @notice INVARIANT: Clearing price should never decrease
function echidna_clearingPriceMonotonic() public returns (bool) {
uint256 currentPrice = auction.clearingPrice();
bool result = currentPrice >= lastObservedClearingPrice;
lastObservedClearingPrice = currentPrice;
return result;
}
/// @notice INVARIANT: CumulativeMps should never decrease
function echidna_cumulativeMpsMonotonic() public returns (bool) {
if (auction.lastCheckpointedBlock() == 0) return true;
Checkpoint memory cp = auction.checkpoints(auction.lastCheckpointedBlock());
bool result = cp.cumulativeMps >= lastObservedCumulativeMps;
lastObservedCumulativeMps = cp.cumulativeMps;
return result;
}
/// @notice INVARIANT: CumulativeMps cannot exceed MPS constant
function echidna_cumulativeMpsNotExceedMax() public view returns (bool) {
if (auction.lastCheckpointedBlock() == 0) return true;
Checkpoint memory cp = auction.checkpoints(auction.lastCheckpointedBlock());
return cp.cumulativeMps <= 10_000_000;
}
/// @notice INVARIANT: Auction token balance valid
function echidna_tokenAccountingValid() public view returns (bool) {
uint256 auctionTokenBalance = auctionToken.balanceOf(address(auction));
return auctionTokenBalance <= TOTAL_SUPPLY;
}
/// @notice INVARIANT: Sum of tokens claimed should not exceed total cleared
function echidna_claimedNotExceedCleared() public view returns (bool) {
return ghost_totalTokensClaimed <= auction.totalCleared();
}
/// @notice INVARIANT: Average price <= maxPrice
function echidna_avgPriceNotExceedMaxPrice() public view returns (bool) {
return !invariant_avgPriceViolation;
}
/// @notice INVARIANT: Refund cannot exceed deposit
function echidna_refundNotExceedDeposit() public view returns (bool) {
return !invariant_refundViolation;
}
/// @notice INVARIANT: TokensFilled cannot exceed maximum
function echidna_tokensFilledNotExceedMax() public view returns (bool) {
return !invariant_tokenFilledViolation;
}
/// @notice INVARIANT: Auction currency balance should be sufficient
function echidna_auctionSolvent() public view returns (bool) {
if (!isAuctionEnded()) return true;
return currencyToken.balanceOf(address(auction)) >= auction.currencyRaised();
}
/// @notice INVARIANT: No ERC20 accounting errors
/// The auction's currency balance should match deposits minus refunds minus sweeps
function echidna_erc20BalanceConsistent() public view returns (bool) {
// This checks that currency isn't being created or destroyed unexpectedly
uint256 auctionCurrencyBalance = currencyToken.balanceOf(address(auction));
// At minimum, balance should be >= currencyRaised (after all exits)
if (isAuctionEnded()) {
return auctionCurrencyBalance >= auction.currencyRaised();
}
return true;
}
// ============================================
// NEW CRYTIC-INSPIRED ERC20 INVARIANTS
// ============================================
/// @notice INVARIANT: Currency token total supply is conserved
/// Sum of all known balances should equal initial supply (no tokens created/destroyed)
function echidna_currencyTotalConserved() public view returns (bool) {
uint256 totalTracked = 0;
// Sum actor balances
for (uint256 i = 0; i < NUM_ACTORS; i++) {
totalTracked += currencyToken.balanceOf(actors[i]);
}
// Add test contract balance
totalTracked += currencyToken.balanceOf(address(this));
// Add auction contract balance
totalTracked += currencyToken.balanceOf(address(auction));
// Add funds recipient balance (receives swept currency)
totalTracked += currencyToken.balanceOf(address(0xCAFE));
// Total should equal initial supply (conservation of currency)
return totalTracked == INITIAL_CURRENCY_SUPPLY;
}
/// @notice INVARIANT: Auction token total supply is conserved
/// Sum of auction balance + tokens recipient + claimed by bidders = TOTAL_SUPPLY
function echidna_auctionTokensConserved() public view returns (bool) {
uint256 totalTracked = 0;
// Auction still holds unclaimed/unsold tokens
totalTracked += auctionToken.balanceOf(address(auction));
// Tokens recipient receives unsold tokens via sweepUnsoldTokens
totalTracked += auctionToken.balanceOf(address(0xBEEF));
// Sum tokens claimed by actors
for (uint256 i = 0; i < NUM_ACTORS; i++) {
totalTracked += auctionToken.balanceOf(actors[i]);
}
// Add test contract's auction tokens (if any)
totalTracked += auctionToken.balanceOf(address(this));
// Total should equal TOTAL_SUPPLY (conservation of auction tokens)
return totalTracked == TOTAL_SUPPLY;
}
/// @notice INVARIANT: No user has currency balance > totalSupply (ERC20-BASE-002)
function echidna_userBalanceNotHigherThanCurrencySupply() public view returns (bool) {
for (uint256 i = 0; i < NUM_ACTORS; i++) {
if (currencyToken.balanceOf(actors[i]) > currencyToken.totalSupply()) {
return false;
}
}
if (currencyToken.balanceOf(address(this)) > currencyToken.totalSupply()) {
return false;
}
if (currencyToken.balanceOf(address(auction)) > currencyToken.totalSupply()) {
return false;
}
return true;
}
/// @notice INVARIANT: No user has auction token balance > totalSupply (ERC20-BASE-002)
function echidna_userBalanceNotHigherThanAuctionSupply() public view returns (bool) {
for (uint256 i = 0; i < NUM_ACTORS; i++) {
if (auctionToken.balanceOf(actors[i]) > auctionToken.totalSupply()) {
return false;
}
}
if (auctionToken.balanceOf(address(auction)) > auctionToken.totalSupply()) {
return false;
}
return true;
}
/// @notice INVARIANT: Zero address should have zero balance for both tokens (ERC20-BASE-004)
function echidna_zeroAddressHasNoBalance() public view returns (bool) {
return currencyToken.balanceOf(address(0)) == 0 &&
auctionToken.balanceOf(address(0)) == 0;
}
/// @notice INVARIANT: Currency token totalSupply should never change (no mint/burn after setup)
function echidna_currencySupplyConstant() public view returns (bool) {
return currencyToken.totalSupply() == INITIAL_CURRENCY_SUPPLY;
}
/// @notice INVARIANT: Auction token totalSupply should never change
function echidna_auctionSupplyConstant() public view returns (bool) {
return auctionToken.totalSupply() == TOTAL_SUPPLY;
}
/// @notice INVARIANT: Tokens distributed should match totalCleared
/// After claims, the auction token balance should decrease by totalCleared
function echidna_tokensDistributedMatchCleared() public view returns (bool) {
if (!canClaimTokens()) return true;
// Auction should have TOTAL_SUPPLY - totalCleared tokens (minus swept unsold)
uint256 auctionBalance = auctionToken.balanceOf(address(auction));
uint256 recipientBalance = auctionToken.balanceOf(address(0xBEEF));
uint256 distributed = TOTAL_SUPPLY - auctionBalance - recipientBalance;
// Distributed tokens should not exceed totalCleared
return distributed <= auction.totalCleared();
}
receive() external payable {}
}
Raw
CCAInvariantTest.sol
// SPDX-License-Identifier: MIT
pragma solidity 0.8.26;
import {ContinuousClearingAuction} from '../../src/ContinuousClearingAuction.sol';
import {AuctionParameters, IContinuousClearingAuction} from '../../src/interfaces/IContinuousClearingAuction.sol';
import {IValidationHook} from '../../src/interfaces/IValidationHook.sol';
import {FixedPoint96} from '../../src/libraries/FixedPoint96.sol';
import {Checkpoint} from '../../src/libraries/CheckpointLib.sol';
import {Bid} from '../../src/libraries/BidLib.sol';
/// @notice Simple ERC20 token for testing
contract TestToken {
mapping(address => uint256) public balanceOf;
mapping(address => mapping(address => uint256)) public allowance;
uint256 public totalSupply;
function mint(address to, uint256 amount) external {
balanceOf[to] += amount;
totalSupply += amount;
}
function transfer(address to, uint256 amount) external returns (bool) {
require(balanceOf[msg.sender] >= amount, "Insufficient");
balanceOf[msg.sender] -= amount;
balanceOf[to] += amount;
return true;
}
function approve(address spender, uint256 amount) external returns (bool) {
allowance[msg.sender][spender] = amount;
return true;
}
function transferFrom(address from, address to, uint256 amount) external returns (bool) {
require(balanceOf[from] >= amount, "Insufficient");
if (allowance[from][msg.sender] != type(uint256).max) {
require(allowance[from][msg.sender] >= amount, "No allowance");
allowance[from][msg.sender] -= amount;
}
balanceOf[from] -= amount;
balanceOf[to] += amount;
return true;
}
}
/// @title UltraMaliciousHook
/// @notice The most aggressive validation hook possible - tries EVERYTHING
contract UltraMaliciousHook is IValidationHook {
ContinuousClearingAuction public auction;
address public testContract;
// ===== ATTACK CONFIGURATION =====
uint256 public attackMode;
uint256 public attackPrice;
uint128 public attackAmount;
uint256 public attackBidId;
uint256 public attackRepetitions; // How many times to repeat the attack
uint256 public repeatInnerMode; // Which mode to repeat (for MODE_REPEATED)
bool public chainAttacks; // Try multiple attack types in sequence
// ===== REENTRANCY STATE =====
bool public reentering;
uint256 public reentrancyDepth;
uint256 public maxReentrancyDepth;
// ===== ATTEMPT TRACKING =====
uint256 public totalAttackAttempts;
uint256 public attemptedForceIterates;
uint256 public attemptedNestedBids;
uint256 public attemptedCheckpoints;
uint256 public attemptedExits;
uint256 public attemptedClaims;
uint256 public attemptedSweeps;
// ===== SUCCESS TRACKING =====
uint256 public successfulForceIterates;
uint256 public successfulNestedBids;
uint256 public successfulCheckpoints;
uint256 public successfulExitBids;
uint256 public successfulExitPartials;
uint256 public successfulSweepCurrency;
uint256 public successfulSweepTokens;
uint256 public successfulClaims;
uint256 public successfulBatchClaims;
// ===== STATE SNAPSHOTS =====
uint256 public clearingPriceSnapshot;
uint256 public totalClearedSnapshot;
uint256 public currencyRaisedSnapshot;
uint256 public auctionBalanceSnapshot;
// ===== ANOMALY DETECTION =====
bool public clearingPriceDecreased;
bool public totalClearedDecreased;
bool public balanceAnomaly;
bool public stateCorruption;
// ===== ATTACK MODE CONSTANTS =====
uint256 constant MODE_NONE = 0;
uint256 constant MODE_FORCE_ITERATE_LOW = 1; // Iterate to low price
uint256 constant MODE_FORCE_ITERATE_HIGH = 2; // Iterate to high price
uint256 constant MODE_FORCE_ITERATE_EXACT = 3; // Iterate to exact clearing
uint256 constant MODE_SUBMIT_SAME_PRICE = 4; // Submit at same price as victim
uint256 constant MODE_SUBMIT_HIGHER = 5; // Submit at higher price (front-run)
uint256 constant MODE_SUBMIT_LOWER = 6; // Submit at lower price
uint256 constant MODE_SUBMIT_AT_CLEARING = 7; // Try to bid at exactly clearing
uint256 constant MODE_CHECKPOINT = 8; // Force checkpoint
uint256 constant MODE_EXIT_OWN_BID = 9; // Exit attacker's own bid
uint256 constant MODE_EXIT_VICTIM_BID = 10; // Try to exit victim's bid (should fail)
uint256 constant MODE_EXIT_PARTIAL = 11; // Exit partially filled bid
uint256 constant MODE_SWEEP_CURRENCY = 12; // Sweep currency
uint256 constant MODE_SWEEP_TOKENS = 13; // Sweep tokens
uint256 constant MODE_CLAIM_TOKENS = 14; // Claim tokens
uint256 constant MODE_BATCH_CLAIM = 15; // Batch claim tokens
uint256 constant MODE_MULTI_BID = 16; // Submit multiple bids
uint256 constant MODE_PRICE_SANDWICH = 17; // Sandwich attack pattern
uint256 constant MODE_DRAIN_ATTEMPT = 18; // Try to drain funds
uint256 constant MODE_STATE_CORRUPTION = 19; // Try to corrupt state
uint256 constant MODE_CHAOS = 20; // Do everything possible
uint256 constant MODE_REPEATED = 21; // Repeat single attack N times
uint256 constant MODE_RECURSIVE_NESTED = 22; // Try recursive nesting
uint256 constant MODE_FLASH_STYLE = 23; // Flash loan style attack
uint256 constant MODE_GRIEFING = 24; // Griefing attacks
uint256 constant MODE_VIEW_MANIPULATION = 25; // Manipulate view functions
uint256 constant MODE_TICK_SPAM = 26; // Spam different ticks
uint256 constant MODE_RAPID_PRICE_CHANGE = 27; // Try to change price rapidly
uint256 constant MODE_EXIT_RACE = 28; // Race condition on exits
uint256 constant MODE_CHECKPOINT_SPAM = 29; // Spam checkpoints
uint256 constant MODE_EXTREME_VALUES = 30; // Use extreme uint values
uint256 constant MODE_REENTRANT_BID_THEN_ITERATE = 31; // Nested bid + forceIterate during validation callback
uint256[] public ownBidIds;
constructor() payable {
maxReentrancyDepth = 3; // Allow some recursion depth
}
function setTestContract(address _test) external {
testContract = _test;
}
function setAuction(address _auction) external {
auction = ContinuousClearingAuction(payable(_auction));
}
function setAttackFull(
uint256 _mode,
uint256 _price,
uint128 _amount,
uint256 _bidId,
uint256 _repetitions,
bool _chain,
uint256 _innerMode
) external {
attackMode = _mode;
attackPrice = _price;
attackAmount = _amount;
attackBidId = _bidId;
attackRepetitions = _repetitions;
chainAttacks = _chain;
repeatInnerMode = _innerMode;
}
function resetStats() external {
totalAttackAttempts = 0;
attemptedForceIterates = 0;
attemptedNestedBids = 0;
attemptedCheckpoints = 0;
attemptedExits = 0;
attemptedClaims = 0;
attemptedSweeps = 0;
successfulForceIterates = 0;
successfulNestedBids = 0;
successfulCheckpoints = 0;
successfulExitBids = 0;
successfulExitPartials = 0;
successfulSweepCurrency = 0;
successfulSweepTokens = 0;
successfulClaims = 0;
successfulBatchClaims = 0;
clearingPriceDecreased = false;
totalClearedDecreased = false;
balanceAnomaly = false;
stateCorruption = false;
}
function validate(uint256 maxPrice, uint128 amount, address owner, address sender, bytes calldata) external override {
// Allow limited recursion for nested attack testing
if (reentrancyDepth >= maxReentrancyDepth) return;
if (address(auction) == address(0)) return;
reentrancyDepth++;
totalAttackAttempts++;
// Snapshot state before attack
_snapshotState();
// Execute attack based on mode
if (chainAttacks) {
_executeChainedAttacks(maxPrice, amount, owner);
} else if (attackMode == MODE_CHAOS) {
_executeChaosMode(maxPrice, amount, owner);
} else if (attackMode == MODE_REPEATED) {
_executeRepeatedAttack();
} else {
_executeSingleAttack(attackMode, maxPrice, amount, owner);
}
// Check for anomalies after attack
_checkStateAnomalies();
reentrancyDepth--;
}
function _snapshotState() internal {
clearingPriceSnapshot = auction.clearingPrice();
totalClearedSnapshot = auction.totalCleared();
currencyRaisedSnapshot = auction.currencyRaised();
auctionBalanceSnapshot = address(auction).balance;
}
function _checkStateAnomalies() internal {
if (auction.clearingPrice() < clearingPriceSnapshot) {
clearingPriceDecreased = true;
}
if (auction.totalCleared() < totalClearedSnapshot) {
totalClearedDecreased = true;
}
// Check for unexpected balance changes
uint256 expectedMin = currencyRaisedSnapshot;
if (address(auction).balance < expectedMin && block.number < auction.endBlock()) {
balanceAnomaly = true;
}
}
function _executeChainedAttacks(uint256 maxPrice, uint128 amount, address owner) internal {
// Try ALL attack modes in sequence
for (uint256 mode = 1; mode <= 20; mode++) {
_executeSingleAttack(mode, maxPrice, amount, owner);
}
}
function _executeChaosMode(uint256 maxPrice, uint128 amount, address owner) internal {
// Chaos mode - try everything with random-ish parameters
_tryForceIterateLow();
_tryForceIterateHigh();
_trySubmitBidAtPrice(maxPrice);
_trySubmitBidAtPrice(attackPrice);
_tryCheckpoint();
_tryExitOwnBids();
_trySweepAll();
_tryClaimAll();
// Try again with different parameters
_trySubmitBidAtPrice(auction.floorPrice() + 100 << FixedPoint96.RESOLUTION);
_tryForceIterateLow();
}
function _executeRepeatedAttack() internal {
// Use repeatInnerMode (not attackMode which is 21/MODE_REPEATED)
uint256 innerMode = repeatInnerMode;
if (innerMode == 0 || innerMode >= MODE_REPEATED) {
innerMode = MODE_FORCE_ITERATE_HIGH; // Default to a real attack mode
}
for (uint256 i = 0; i < attackRepetitions && i < 10; i++) {
_executeSingleAttack(innerMode, attackPrice, attackAmount, address(this));
}
}
function _executeSingleAttack(uint256 mode, uint256 maxPrice, uint128 amount, address owner) internal {
if (mode == MODE_FORCE_ITERATE_LOW) {
_tryForceIterateLow();
} else if (mode == MODE_FORCE_ITERATE_HIGH) {
_tryForceIterateHigh();
} else if (mode == MODE_FORCE_ITERATE_EXACT) {
_tryForceIterateExact();
} else if (mode == MODE_SUBMIT_SAME_PRICE) {
_trySubmitBidAtPrice(maxPrice);
} else if (mode == MODE_SUBMIT_HIGHER) {
_trySubmitBidAtPrice(maxPrice + (100 << FixedPoint96.RESOLUTION));
} else if (mode == MODE_SUBMIT_LOWER) {
if (maxPrice > auction.clearingPrice()) {
_trySubmitBidAtPrice(maxPrice - (100 << FixedPoint96.RESOLUTION));
}
} else if (mode == MODE_SUBMIT_AT_CLEARING) {
_trySubmitBidAtPrice(auction.clearingPrice());
} else if (mode == MODE_CHECKPOINT) {
_tryCheckpoint();
} else if (mode == MODE_EXIT_OWN_BID) {
_tryExitOwnBids();
} else if (mode == MODE_EXIT_VICTIM_BID) {
_tryExitBid(attackBidId);
} else if (mode == MODE_EXIT_PARTIAL) {
_tryExitPartial(attackBidId);
} else if (mode == MODE_SWEEP_CURRENCY) {
_trySweepCurrency();
} else if (mode == MODE_SWEEP_TOKENS) {
_trySweepTokens();
} else if (mode == MODE_CLAIM_TOKENS) {
_tryClaimTokens(attackBidId);
} else if (mode == MODE_BATCH_CLAIM) {
_tryBatchClaim();
} else if (mode == MODE_MULTI_BID) {
_tryMultipleBids(maxPrice, amount);
} else if (mode == MODE_PRICE_SANDWICH) {
_tryPriceSandwich(maxPrice, amount);
} else if (mode == MODE_DRAIN_ATTEMPT) {
_tryDrainFunds();
} else if (mode == MODE_STATE_CORRUPTION) {
_tryStateCorruption(maxPrice, amount);
} else if (mode == MODE_RECURSIVE_NESTED) {
_tryRecursiveNested(maxPrice, amount);
} else if (mode == MODE_FLASH_STYLE) {
_tryFlashStyleAttack(maxPrice, amount);
} else if (mode == MODE_GRIEFING) {
_tryGriefingAttack();
} else if (mode == MODE_VIEW_MANIPULATION) {
_tryViewManipulation();
} else if (mode == MODE_TICK_SPAM) {
_tryTickSpam();
} else if (mode == MODE_RAPID_PRICE_CHANGE) {
_tryRapidPriceChange();
} else if (mode == MODE_EXIT_RACE) {
_tryExitRace();
} else if (mode == MODE_CHECKPOINT_SPAM) {
_tryCheckpointSpam();
} else if (mode == MODE_EXTREME_VALUES) {
_tryExtremeValues(maxPrice);
} else if (mode == MODE_REENTRANT_BID_THEN_ITERATE) {
_tryReentrantBidThenIterate(maxPrice, amount);
}
}
// ===== INDIVIDUAL ATTACK FUNCTIONS =====
function _tryForceIterateLow() internal {
attemptedForceIterates++;
try auction.forceIterateOverTicks(auction.floorPrice()) {
successfulForceIterates++;
} catch {}
}
function _tryForceIterateHigh() internal {
attemptedForceIterates++;
uint256 highPrice = auction.floorPrice() + (10000 << FixedPoint96.RESOLUTION);
try auction.forceIterateOverTicks(highPrice) {
successfulForceIterates++;
} catch {}
}
function _tryForceIterateExact() internal {
attemptedForceIterates++;
try auction.forceIterateOverTicks(auction.clearingPrice()) {
successfulForceIterates++;
} catch {}
}
function _trySubmitBidAtPrice(uint256 price) internal {
if (attackAmount == 0) return;
if (price <= auction.clearingPrice()) return;
if (address(this).balance < attackAmount) return;
attemptedNestedBids++;
try auction.submitBid{value: attackAmount}(
price,
attackAmount,
address(this),
auction.floorPrice(),
bytes('')
) returns (uint256 bidId) {
ownBidIds.push(bidId);
successfulNestedBids++;
} catch {}
}
function _tryCheckpoint() internal {
attemptedCheckpoints++;
try auction.checkpoint() {
successfulCheckpoints++;
} catch {}
}
function _tryExitBid(uint256 bidId) internal {
if (bidId == 0) return;
attemptedExits++;
try auction.exitBid(bidId) {
successfulExitBids++;
} catch {}
}
function _tryExitOwnBids() internal {
for (uint256 i = 0; i < ownBidIds.length && i < 5; i++) {
_tryExitBid(ownBidIds[i]);
}
}
function _tryExitPartial(uint256 bidId) internal {
if (bidId == 0) return;
attemptedExits++;
try auction.exitPartiallyFilledBid(bidId, 0, 0) {
successfulExitPartials++;
} catch {}
}
function _trySweepCurrency() internal {
attemptedSweeps++;
try auction.sweepCurrency() {
successfulSweepCurrency++;
} catch {}
}
function _trySweepTokens() internal {
attemptedSweeps++;
try auction.sweepUnsoldTokens() {
successfulSweepTokens++;
} catch {}
}
function _trySweepAll() internal {
_trySweepCurrency();
_trySweepTokens();
}
function _tryClaimTokens(uint256 bidId) internal {
if (bidId == 0) return;
attemptedClaims++;
try auction.claimTokens(bidId) {
successfulClaims++;
} catch {}
}
function _tryClaimAll() internal {
for (uint256 i = 0; i < ownBidIds.length && i < 5; i++) {
_tryClaimTokens(ownBidIds[i]);
}
}
function _tryBatchClaim() internal {
if (ownBidIds.length == 0) return;
attemptedClaims++;
uint256[] memory bidIds = new uint256[](ownBidIds.length > 5 ? 5 : ownBidIds.length);
for (uint256 i = 0; i < bidIds.length; i++) {
bidIds[i] = ownBidIds[i];
}
try auction.claimTokensBatch(address(this), bidIds) {
successfulBatchClaims++;
} catch {}
}
function _tryMultipleBids(uint256 basePrice, uint128 amount) internal {
// Try to submit multiple bids in quick succession
for (uint256 i = 0; i < 3; i++) {
uint256 price = basePrice + (i * 100 << FixedPoint96.RESOLUTION);
if (price > auction.clearingPrice() && address(this).balance >= amount) {
try auction.submitBid{value: amount}(
price,
amount,
address(this),
auction.floorPrice(),
bytes('')
) returns (uint256 bidId) {
ownBidIds.push(bidId);
successfulNestedBids++;
} catch {}
}
}
}
function _tryPriceSandwich(uint256 victimPrice, uint128 amount) internal {
// Classic sandwich: bid below, victim bids, bid above
// We're in the hook during victim's bid, so we try to manipulate
// First, try to force iterate to raise clearing
_tryForceIterateHigh();
// Then submit our own bid at a higher price
if (address(this).balance >= amount) {
uint256 sandwichPrice = victimPrice + (200 << FixedPoint96.RESOLUTION);
_trySubmitBidAtPrice(sandwichPrice);
}
// Finally, try to checkpoint to lock in state
_tryCheckpoint();
}
/// @notice Reentrant attack: nested bid + forceIterate during validation callback
/// @dev Attack sequence: submit nested bid at high price, then forceIterate to raise clearing
/// 1. Submit nested bid at high price (creates demand at high tick)
/// 2. Call forceIterateOverTicks to advance clearing price
/// 3. Tests reentrancy guards and tick list integrity under adversarial conditions
function _tryReentrantBidThenIterate(uint256 victimMaxPrice, uint128 victimAmount) internal {
// We need ETH to submit our own bid
if (address(this).balance < attackAmount || attackAmount == 0) return;
// Use the attackPrice set by the handler - it's properly aligned with tick spacing
// attackPrice should be significantly above victimMaxPrice
uint256 ourBidPrice = attackPrice;
// Ensure our bid is actually above victim's (skip if not configured correctly)
if (ourBidPrice <= victimMaxPrice) return;
// Step 1: Submit OUR bid FIRST at high price
// This creates demand at the high tick that forceIterate can use
uint256 bidId;
try auction.submitBid{value: attackAmount}(
ourBidPrice,
attackAmount,
address(this),
auction.floorPrice(),
bytes('')
) returns (uint256 _bidId) {
bidId = _bidId;
ownBidIds.push(bidId);
successfulNestedBids++;
} catch {
return; // Can't continue attack without our bid
}
// Step 2: Call forceIterateOverTicks to advance clearing price
// The nested bid creates demand at high tick that forceIterate can use
try auction.forceIterateOverTicks(ourBidPrice) {
successfulForceIterates++;
} catch {}
// Try to finalize state via checkpoint
_tryCheckpoint();
}
function _tryDrainFunds() internal {
// Attempt to drain funds through various means
_trySweepCurrency();
_trySweepTokens();
_tryExitOwnBids();
_tryClaimAll();
}
function _tryStateCorruption(uint256 price, uint128 amount) internal {
// Try to corrupt state through rapid state changes
_tryCheckpoint();
_tryForceIterateLow();
_trySubmitBidAtPrice(price);
_tryForceIterateHigh();
_tryCheckpoint();
_tryExitOwnBids();
_tryCheckpoint();
}
function _tryRecursiveNested(uint256 price, uint128 amount) internal {
// Try to create recursive nested bids
if (address(this).balance < amount * 3) return;
// Submit multiple bids that might trigger nested hooks
for (uint256 i = 0; i < 3; i++) {
uint256 nestedPrice = price + (i * 50 << FixedPoint96.RESOLUTION);
if (nestedPrice > auction.clearingPrice()) {
try auction.submitBid{value: amount}(
nestedPrice,
amount,
address(this),
auction.floorPrice(),
bytes('')
) returns (uint256 bidId) {
ownBidIds.push(bidId);
successfulNestedBids++;
} catch {}
}
}
}
function _tryFlashStyleAttack(uint256 price, uint128 amount) internal {
// Flash loan style: do many operations, try to end up profitable
uint256 balanceBefore = address(this).balance;
// Submit a bid
_trySubmitBidAtPrice(price);
// Immediately try to manipulate clearing price
_tryForceIterateHigh();
_tryCheckpoint();
// Try to exit and reclaim funds
_tryExitOwnBids();
// Try to claim any tokens
_tryClaimAll();
// Check if we ended up with more than we started
if (address(this).balance > balanceBefore) {
// Profit - this could be a bug!
}
}
function _tryGriefingAttack() internal {
// Griefing: try to brick the auction for others
// Spam force iterates to different prices
for (uint256 i = 0; i < 5; i++) {
uint256 price = auction.floorPrice() + ((i * 1000) << FixedPoint96.RESOLUTION);
try auction.forceIterateOverTicks(price) {
successfulForceIterates++;
} catch {}
}
// Spam checkpoints
for (uint256 i = 0; i < 3; i++) {
_tryCheckpoint();
}
}
function _tryViewManipulation() internal {
// Try to manipulate state that affects view functions
// Get current values
uint256 currentClearing = auction.clearingPrice();
uint256 currentTotal = auction.totalCleared();
// Try various state changes
_tryCheckpoint();
_tryForceIterateHigh();
// Check if values changed unexpectedly
if (auction.clearingPrice() < currentClearing) {
clearingPriceDecreased = true;
}
if (auction.totalCleared() < currentTotal) {
totalClearedDecreased = true;
}
}
function _tryTickSpam() internal {
// Spam bids at many different tick levels
uint256 basePrice = auction.clearingPrice();
for (uint256 i = 1; i <= 10; i++) {
uint256 tickPrice = basePrice + (i * 100 << FixedPoint96.RESOLUTION);
if (address(this).balance >= 1e15) {
try auction.submitBid{value: 1e15}(
tickPrice,
1e15,
address(this),
auction.floorPrice(),
bytes('')
) returns (uint256 bidId) {
ownBidIds.push(bidId);
successfulNestedBids++;
} catch {}
}
}
}
function _tryRapidPriceChange() internal {
// Try to change clearing price rapidly
uint256 startPrice = auction.clearingPrice();
// Force iterate to high price
_tryForceIterateHigh();
// Submit high price bid
uint256 highPrice = startPrice + (500 << FixedPoint96.RESOLUTION);
if (address(this).balance >= 1e18 && highPrice > auction.clearingPrice()) {
_trySubmitBidAtPrice(highPrice);
}
// Force iterate again
_tryForceIterateHigh();
// Checkpoint to lock in
_tryCheckpoint();
uint256 endPrice = auction.clearingPrice();
if (endPrice < startPrice) {
clearingPriceDecreased = true;
}
}
function _tryExitRace() internal {
// Try to exit bids in rapid succession (race condition)
for (uint256 i = 0; i < ownBidIds.length && i < 5; i++) {
uint256 bidId = ownBidIds[i];
// Try both exit methods on same bid
try auction.exitBid(bidId) {
successfulExitBids++;
} catch {}
try auction.exitPartiallyFilledBid(bidId, 0, 0) {
successfulExitPartials++;
} catch {}
}
}
function _tryCheckpointSpam() internal {
// Spam checkpoints
for (uint256 i = 0; i < 10; i++) {
try auction.checkpoint() {
successfulCheckpoints++;
} catch {}
}
}
function _tryExtremeValues(uint256 basePrice) internal {
// Try extreme values
// Try with 0 amount (should fail)
try auction.submitBid{value: 0}(
basePrice,
0,
address(this),
auction.floorPrice(),
bytes('')
) {
successfulNestedBids++; // Unexpected success!
} catch {}
// Try with max uint128 amount (limited by balance)
uint128 maxAmount = uint128(address(this).balance);
if (maxAmount > 0 && basePrice > auction.clearingPrice()) {
try auction.submitBid{value: maxAmount}(
basePrice,
maxAmount,
address(this),
auction.floorPrice(),
bytes('')
) returns (uint256 bidId) {
ownBidIds.push(bidId);
successfulNestedBids++;
} catch {}
}
// Try force iterate to max uint
try auction.forceIterateOverTicks(type(uint256).max) {
successfulForceIterates++;
} catch {}
// Try force iterate to 0
try auction.forceIterateOverTicks(0) {
successfulForceIterates++;
} catch {}
}
receive() external payable {}
}
/// @title CCAInvariantTest
/// @notice Comprehensive invariant testing with adversarial hook and tick integrity checks
contract CCAInvariantTest {
// ===== CONSTANTS =====
uint256 public constant TICK_SPACING = 100 << FixedPoint96.RESOLUTION;
uint256 public constant FLOOR_PRICE = 1000 << FixedPoint96.RESOLUTION;
uint128 public constant TOTAL_SUPPLY = 1000e18;
uint256 public constant AUCTION_DURATION = 100;
uint256 public constant MAX_BIDS = 100;
uint256 public constant NUM_ACTORS = 20;
// ===== CONTRACTS =====
ContinuousClearingAuction public auction;
TestToken public token;
UltraMaliciousHook public hook;
// ===== ACTORS =====
// Different actor types with different behaviors
address[] public honestBidders; // 0-4: Normal bidders
address[] public aggressiveBidders; // 5-9: High price bidders
address[] public passiveBidders; // 10-14: Low price bidders
address[] public attackers; // 15-19: Malicious actors
address[] public allActors;
// ===== STATE TRACKING =====
uint256[] public bidIds;
uint256 public bidCount;
mapping(uint256 => bool) public bidExited;
mapping(uint256 => bool) public bidClaimed;
mapping(uint256 => address) public bidOwner;
mapping(uint256 => uint256) public bidOriginalAmount;
mapping(address => uint256[]) public actorBids;
// ===== GHOST VARIABLES =====
uint256 public ghost_totalDeposited;
uint256 public ghost_totalRefunded;
uint256 public ghost_totalTokensClaimed;
uint256 public ghost_sumCurrencyDemandAboveClearing; // Shadow of $sumCurrencyDemandAboveClearingQ96
// ===== STATE HISTORY =====
uint256 public lastClearingPrice;
uint256 public lastTotalCleared;
uint24 public lastCumulativeMps;
uint256 public lastNextActiveTickPrice;
// ===== INVARIANT VIOLATION FLAGS =====
bool public inv_clearingPriceDecreased;
bool public inv_totalClearedDecreased;
bool public inv_bidBelowClearing;
bool public inv_refundExceedsDeposit;
bool public inv_claimedExceedsCleared;
bool public inv_balanceAnomaly;
bool public inv_reentrancyExploit;
bool public inv_hookSucceededIllegally;
bool public inv_sumDemandMismatch; // sumCurrencyDemandAboveClearingQ96 mismatch
bool public inv_nextActiveTickInvalid; // nextActiveTickPrice <= clearingPrice
bool public inv_clearingPriceNotSynced; // clearingPrice != latestCheckpoint.clearingPrice
bool public inv_unreachableDemand; // Global demand > reachable demand (tick list corruption)
bool public inv_tickListCycle; // Tick list has a cycle
bool public inv_tickListUnordered; // Tick list not monotonically increasing
// ===== INSTRUMENTATION COUNTERS =====
uint256 public submitBidAttempts;
uint256 public submitBidSuccesses;
uint256 public exitBidAttempts;
uint256 public exitBidSuccesses;
uint256 public checkpointAttempts;
uint256 public checkpointSuccesses;
// ===== OPERATION COUNTERS =====
uint256 public totalBidsSubmitted;
uint256 public totalBidsExited;
uint256 public totalCheckpoints;
uint256 public totalForceIterates;
uint256 public totalSweeps;
uint256 public totalClaims;
bool private _initialized;
constructor() payable {
// Minimal constructor for Echidna compatibility
// Real initialization happens in _ensureInitialized()
}
modifier initialized() {
_ensureInitialized();
_;
}
function _ensureInitialized() internal {
if (_initialized) return;
_initialized = true;
// Initialize all actors
for (uint256 i = 0; i < 5; i++) {
honestBidders.push(address(uint160(0x10000 + i)));
allActors.push(honestBidders[i]);
}
for (uint256 i = 0; i < 5; i++) {
aggressiveBidders.push(address(uint160(0x20000 + i)));
allActors.push(aggressiveBidders[i]);
}
for (uint256 i = 0; i < 5; i++) {
passiveBidders.push(address(uint160(0x30000 + i)));
allActors.push(passiveBidders[i]);
}
for (uint256 i = 0; i < 5; i++) {
attackers.push(address(uint160(0x40000 + i)));
allActors.push(attackers[i]);
}
// Deploy token
token = new TestToken();
// Deploy malicious hook
hook = new UltraMaliciousHook();
// Build auction steps (MPS = 10,000,000)
bytes memory auctionStepsData = abi.encodePacked(
uint24(100_000), uint40(50),
uint24(100_000), uint40(50)
);
// Deploy auction WITH the malicious hook
AuctionParameters memory params = AuctionParameters({
currency: address(0),
floorPrice: FLOOR_PRICE,
tickSpacing: TICK_SPACING,
validationHook: address(hook),
tokensRecipient: address(0xBEEF),
fundsRecipient: address(0xCAFE),
startBlock: 1,
endBlock: 1 + uint64(AUCTION_DURATION),
claimBlock: 1 + uint64(AUCTION_DURATION) + 10,
requiredCurrencyRaised: 0,
auctionStepsData: auctionStepsData
});
auction = new ContinuousClearingAuction(address(token), TOTAL_SUPPLY, params);
// Complete hook setup
hook.setAuction(address(auction));
hook.setTestContract(address(this));
// Note: Hook needs ETH for reentrant bid attacks but we can't fund it in constructor
// The handler_fundHookForAttack will be called by echidna to fund the hook
// Mint tokens and notify
token.mint(address(auction), TOTAL_SUPPLY);
auction.onTokensReceived();
// Initialize state tracking
lastClearingPrice = auction.clearingPrice();
}
// ===== HELPER FUNCTIONS =====
function getActor(uint256 seed) public view returns (address) {
return allActors[seed % NUM_ACTORS];
}
function getHonestBidder(uint256 seed) public view returns (address) {
return honestBidders[seed % 5];
}
function getAggressiveBidder(uint256 seed) public view returns (address) {
return aggressiveBidders[seed % 5];
}
function getPassiveBidder(uint256 seed) public view returns (address) {
return passiveBidders[seed % 5];
}
function getAttacker(uint256 seed) public view returns (address) {
return attackers[seed % 5];
}
function isAuctionActive() public view returns (bool) {
return block.number >= auction.startBlock() && block.number < auction.endBlock();
}
function isAuctionEnded() public view returns (bool) {
return block.number >= auction.endBlock();
}
function canClaim() public view returns (bool) {
return block.number >= auction.claimBlock();
}
// ===== TICK LIST TRAVERSAL (BOUNDED) =====
uint256 constant MAX_TICK_ITERATIONS = 256;
/// @notice Sum demand reachable from nextActiveTickPrice with bounded iteration
/// @return sum The total demand reachable
/// @return isCycle True if a cycle was detected
/// @return isUnordered True if tick ordering is violated
function _sumReachableDemandBounded() internal view returns (uint256 sum, bool isCycle, bool isUnordered) {
uint256 price = auction.nextActiveTickPrice();
uint256 prevPrice = 0;
uint256 iterations = 0;
while (price != type(uint256).max && iterations < MAX_TICK_ITERATIONS) {
// Check ordering: price should always increase
if (prevPrice != 0 && price <= prevPrice) {
isUnordered = true;
}
sum += auction.ticks(price).currencyDemandQ96;
prevPrice = price;
price = auction.ticks(price).next;
iterations++;
// Simple cycle detection: if we've iterated MAX times and still going, likely a cycle
if (iterations == MAX_TICK_ITERATIONS && price != type(uint256).max) {
isCycle = true;
}
}
}
/// @notice Check for phantom demand (unreachable demand in tick list)
function _checkPhantomDemand() internal {
uint256 globalDemand = auction.sumCurrencyDemandAboveClearingQ96();
(uint256 reachableDemand, bool isCycle, bool isUnordered) = _sumReachableDemandBounded();
if (isCycle) {
inv_tickListCycle = true;
}
if (isUnordered) {
inv_tickListUnordered = true;
}
if (globalDemand > reachableDemand) {
inv_unreachableDemand = true;
}
}
function _checkClearingPriceInvariant() internal {
uint256 current = auction.clearingPrice();
if (current < lastClearingPrice) {
inv_clearingPriceDecreased = true;
}
lastClearingPrice = current;
}
function _checkTotalClearedInvariant() internal {
uint256 current = auction.totalCleared();
if (current < lastTotalCleared) {
inv_totalClearedDecreased = true;
}
lastTotalCleared = current;
}
function _checkNextActiveTickInvariant() internal {
uint256 clearingPrice = auction.clearingPrice();
uint256 nextActiveTick = auction.nextActiveTickPrice();
// nextActiveTickPrice must be > clearingPrice (unless it's MAX_TICK_PTR = type(uint256).max)
// Or clearingPrice is at floor and no bids yet
if (nextActiveTick != type(uint256).max && nextActiveTick <= clearingPrice && nextActiveTick != 0) {
inv_nextActiveTickInvalid = true;
}
lastNextActiveTickPrice = nextActiveTick;
}
function _checkClearingPriceSyncInvariant() internal {
// After checkpoint, clearingPrice() should equal latestCheckpoint().clearingPrice
uint256 storageClearingPrice = auction.clearingPrice();
Checkpoint memory latest = auction.latestCheckpoint();
if (storageClearingPrice != latest.clearingPrice) {
inv_clearingPriceNotSynced = true;
}
}
// ===== HONEST BIDDER HANDLERS =====
function handler_honestBid(uint256 actorSeed, uint256 priceSeed, uint256 amountSeed) public initialized {
if (!isAuctionActive()) return;
if (bidCount >= MAX_BIDS) return;
address actor = getHonestBidder(actorSeed);
uint256 tickNumber = 1 + (priceSeed % 50); // Moderate price range
uint256 maxPrice = FLOOR_PRICE + tickNumber * TICK_SPACING;
if (maxPrice <= auction.clearingPrice()) return;
uint128 amount = uint128(1e16 + (amountSeed % 1e19)); // Moderate amounts
// No attack during honest bids
hook.setAttackFull(0, 0, 0, 0, 0, false, 0);
_submitBid(maxPrice, amount, actor);
}
// ===== AGGRESSIVE BIDDER HANDLERS =====
function handler_aggressiveBid(uint256 actorSeed, uint256 priceSeed, uint256 amountSeed) public initialized {
if (!isAuctionActive()) return;
if (bidCount >= MAX_BIDS) return;
address actor = getAggressiveBidder(actorSeed);
uint256 tickNumber = 50 + (priceSeed % 100); // High price range
uint256 maxPrice = FLOOR_PRICE + tickNumber * TICK_SPACING;
if (maxPrice <= auction.clearingPrice()) return;
uint128 amount = uint128(1e17 + (amountSeed % 1e20)); // Larger amounts
hook.setAttackFull(0, 0, 0, 0, 0, false, 0);
_submitBid(maxPrice, amount, actor);
}
// ===== PASSIVE BIDDER HANDLERS =====
function handler_passiveBid(uint256 actorSeed, uint256 priceSeed, uint256 amountSeed) public initialized {
if (!isAuctionActive()) return;
if (bidCount >= MAX_BIDS) return;
address actor = getPassiveBidder(actorSeed);
uint256 tickNumber = 1 + (priceSeed % 20); // Low price range
uint256 maxPrice = FLOOR_PRICE + tickNumber * TICK_SPACING;
if (maxPrice <= auction.clearingPrice()) return;
uint128 amount = uint128(1e15 + (amountSeed % 1e18)); // Smaller amounts
hook.setAttackFull(0, 0, 0, 0, 0, false, 0);
_submitBid(maxPrice, amount, actor);
}
// ===== ATTACKER HANDLERS =====
function handler_attackerBidWithReentrancy(
uint256 actorSeed,
uint256 priceSeed,
uint256 amountSeed,
uint256 attackModeSeed,
uint256 attackPriceSeed
) public initialized {
if (!isAuctionActive()) return;
if (bidCount >= MAX_BIDS) return;
address actor = getAttacker(actorSeed);
uint256 tickNumber = 1 + (priceSeed % 100);
uint256 maxPrice = FLOOR_PRICE + tickNumber * TICK_SPACING;
if (maxPrice <= auction.clearingPrice()) return;
uint128 amount = uint128(1e15 + (amountSeed % 1e20));
// Configure attack
uint256 attackMode = 1 + (attackModeSeed % 31); // Modes 1-31 (all attack modes)
uint256 attackTickNumber = 1 + (attackPriceSeed % 100);
uint256 attackPrice = FLOOR_PRICE + attackTickNumber * TICK_SPACING;
uint256 attackBidId = bidCount > 0 ? bidIds[attackPriceSeed % bidCount] : 0;
hook.setAttackFull(attackMode, attackPrice, amount, attackBidId, 1, false, 0);
_submitBid(maxPrice, amount, actor);
// Check if hook did anything illegal
_checkHookSuccess();
// Reset hook
hook.setAttackFull(0, 0, 0, 0, 0, false, 0);
}
function handler_chaosAttack(
uint256 actorSeed,
uint256 priceSeed,
uint256 amountSeed,
uint256 attackPriceSeed
) public initialized {
if (!isAuctionActive()) return;
if (bidCount >= MAX_BIDS) return;
address actor = getAttacker(actorSeed);
uint256 tickNumber = 1 + (priceSeed % 100);
uint256 maxPrice = FLOOR_PRICE + tickNumber * TICK_SPACING;
if (maxPrice <= auction.clearingPrice()) return;
uint128 amount = uint128(1e15 + (amountSeed % 1e20));
// CHAOS MODE - try everything
uint256 attackTickNumber = 1 + (attackPriceSeed % 100);
uint256 attackPrice = FLOOR_PRICE + attackTickNumber * TICK_SPACING;
uint256 attackBidId = bidCount > 0 ? bidIds[attackPriceSeed % bidCount] : 0;
hook.setAttackFull(20, attackPrice, amount, attackBidId, 3, false, 0); // MODE_CHAOS
_submitBid(maxPrice, amount, actor);
_checkHookSuccess();
hook.setAttackFull(0, 0, 0, 0, 0, false, 0);
}
function handler_chainedAttack(
uint256 actorSeed,
uint256 priceSeed,
uint256 amountSeed,
uint256 attackPriceSeed
) public initialized {
if (!isAuctionActive()) return;
if (bidCount >= MAX_BIDS) return;
address actor = getAttacker(actorSeed);
uint256 tickNumber = 1 + (priceSeed % 100);
uint256 maxPrice = FLOOR_PRICE + tickNumber * TICK_SPACING;
if (maxPrice <= auction.clearingPrice()) return;
uint128 amount = uint128(1e15 + (amountSeed % 1e20));
// CHAINED ATTACKS - try all modes in sequence
uint256 attackTickNumber = 1 + (attackPriceSeed % 100);
uint256 attackPrice = FLOOR_PRICE + attackTickNumber * TICK_SPACING;
uint256 attackBidId = bidCount > 0 ? bidIds[attackPriceSeed % bidCount] : 0;
hook.setAttackFull(1, attackPrice, amount, attackBidId, 1, true, 0); // chain=true
_submitBid(maxPrice, amount, actor);
_checkHookSuccess();
hook.setAttackFull(0, 0, 0, 0, 0, false, 0);
}
function handler_repeatedAttack(
uint256 actorSeed,
uint256 priceSeed,
uint256 amountSeed,
uint256 attackModeSeed,
uint256 repetitionsSeed
) public initialized {
if (!isAuctionActive()) return;
if (bidCount >= MAX_BIDS) return;
address actor = getAttacker(actorSeed);
uint256 tickNumber = 1 + (priceSeed % 100);
uint256 maxPrice = FLOOR_PRICE + tickNumber * TICK_SPACING;
if (maxPrice <= auction.clearingPrice()) return;
uint128 amount = uint128(1e15 + (amountSeed % 1e20));
// REPEATED ATTACK - same attack N times
uint256 innerMode = 1 + (attackModeSeed % 20); // The actual attack mode to repeat
uint256 repetitions = 1 + (repetitionsSeed % 5);
hook.setAttackFull(21, maxPrice, amount, 0, repetitions, false, innerMode); // MODE_REPEATED with innerMode
_submitBid(maxPrice, amount, actor);
_checkHookSuccess();
hook.setAttackFull(0, 0, 0, 0, 0, false, 0);
}
/// @notice Handler for reentrant bid + iterate attack (nested bid then forceIterate during callback)
/// @dev Tests reentrancy guards by attempting nested bid at high price, then advancing clearing
function handler_reentrantBidThenIterate(
uint256 actorSeed,
uint256 priceSeed,
uint256 amountSeed,
uint256 attackPriceSeed
) public initialized {
if (!isAuctionActive()) return;
if (bidCount >= MAX_BIDS) return;
address actor = getAttacker(actorSeed);
uint256 tickNumber = 1 + (priceSeed % 100);
uint256 maxPrice = FLOOR_PRICE + tickNumber * TICK_SPACING;
if (maxPrice <= auction.clearingPrice()) return;
uint128 amount = uint128(1e15 + (amountSeed % 1e20));
// Fund the hook with ETH via direct transfer (test contract has ETH from balanceContract config)
uint256 hookFunding = 100 ether;
if (address(this).balance >= hookFunding && address(hook).balance < hookFunding) {
(bool sent,) = payable(address(hook)).call{value: hookFunding}("");
// If send fails, hook won't have ETH - attack will skip gracefully
}
// Configure attack: high price nested bid + forceIterate
uint256 attackTickNumber = tickNumber + 5 + (attackPriceSeed % 50); // Attack above victim price
uint256 attackPrice = FLOOR_PRICE + attackTickNumber * TICK_SPACING;
// Set up reentrant bid + iterate attack mode
hook.setAttackFull(31, attackPrice, amount, 0, 1, false, 0); // MODE_REENTRANT_BID_THEN_ITERATE = 31
_submitBid(maxPrice, amount, actor);
_checkHookSuccess();
hook.setAttackFull(0, 0, 0, 0, 0, false, 0);
}
// ===== COMMON BID SUBMISSION =====
function _submitBid(uint256 maxPrice, uint128 amount, address owner) internal {
uint256 clearingBefore = auction.clearingPrice();
submitBidAttempts++;
try auction.submitBid{value: amount}(maxPrice, amount, owner, FLOOR_PRICE, bytes('')) returns (uint256 bidId) {
submitBidSuccesses++;
bidIds.push(bidId);
bidCount++;
bidOwner[bidId] = owner;
bidOriginalAmount[bidId] = amount;
actorBids[owner].push(bidId);
ghost_totalDeposited += amount;
totalBidsSubmitted++;
// Check bid validity
Bid memory bid = auction.bids(bidId);
uint256 clearingAfter = auction.clearingPrice();
if (bid.maxPrice <= clearingAfter && clearingAfter > clearingBefore) {
inv_bidBelowClearing = true;
}
_checkClearingPriceInvariant();
_checkTotalClearedInvariant();
_checkPhantomDemand(); // Check tick list integrity after each successful bid
} catch {}
}
function _checkHookSuccess() internal {
// Check if hook succeeded in doing something it shouldn't have
if (hook.successfulNestedBids() > 0) {
// Nested bids during reentrancy - concerning!
inv_reentrancyExploit = true;
}
if (hook.clearingPriceDecreased()) {
inv_clearingPriceDecreased = true;
}
if (hook.balanceAnomaly()) {
inv_balanceAnomaly = true;
}
}
// ===== CHECKPOINT HANDLERS =====
function handler_checkpoint() public initialized {
if (block.number < auction.startBlock()) return;
try auction.checkpoint() {
totalCheckpoints++;
_checkClearingPriceInvariant();
_checkTotalClearedInvariant();
_checkNextActiveTickInvariant();
_checkClearingPriceSyncInvariant();
} catch {}
}
function handler_forceIterate(uint256 tickSeed) public initialized {
if (block.number < auction.startBlock()) return;
uint256 tickNumber = 1 + (tickSeed % 200);
uint256 price = FLOOR_PRICE + tickNumber * TICK_SPACING;
try auction.forceIterateOverTicks(price) {
totalForceIterates++;
_checkClearingPriceInvariant();
_checkTotalClearedInvariant();
_checkNextActiveTickInvariant();
} catch {}
}
// ===== EXIT HANDLERS =====
function handler_exitBid(uint256 bidIndexSeed) public initialized {
if (!isAuctionEnded()) return;
if (bidCount == 0) return;
uint256 index = bidIndexSeed % bidCount;
uint256 bidId = bidIds[index];
if (bidExited[bidId]) return;
Bid memory bid = auction.bids(bidId);
if (bid.maxPrice <= auction.clearingPrice()) return;
address owner = bidOwner[bidId];
uint256 balanceBefore = owner.balance;
uint256 originalAmount = bidOriginalAmount[bidId];
try auction.exitBid(bidId) {
bidExited[bidId] = true;
totalBidsExited++;
uint256 refund = owner.balance - balanceBefore;
ghost_totalRefunded += refund;
// Check refund invariant
if (refund > originalAmount) {
inv_refundExceedsDeposit = true;
}
} catch {}
}
function handler_exitPartial(uint256 bidIndexSeed) public initialized {
if (!isAuctionEnded()) return;
if (bidCount == 0) return;
try auction.checkpoint() {} catch {}
uint256 index = bidIndexSeed % bidCount;
uint256 bidId = bidIds[index];
if (bidExited[bidId]) return;
Bid memory bid = auction.bids(bidId);
if (bid.maxPrice > auction.clearingPrice()) return;
address owner = bidOwner[bidId];
uint256 balanceBefore = owner.balance;
uint256 originalAmount = bidOriginalAmount[bidId];
try auction.exitPartiallyFilledBid(bidId, 0, 0) {
bidExited[bidId] = true;
totalBidsExited++;
uint256 refund = owner.balance - balanceBefore;
ghost_totalRefunded += refund;
if (refund > originalAmount) {
inv_refundExceedsDeposit = true;
}
} catch {}
}
// ===== SWEEP HANDLERS =====
function handler_sweepCurrency() public initialized {
if (!isAuctionEnded()) return;
try auction.sweepCurrency() {
totalSweeps++;
} catch {}
}
function handler_sweepTokens() public initialized {
if (!isAuctionEnded()) return;
try auction.sweepUnsoldTokens() {
totalSweeps++;
} catch {}
}
// ===== CLAIM HANDLERS =====
function handler_claimTokens(uint256 bidIndexSeed) public initialized {
if (!canClaim()) return;
if (bidCount == 0) return;
uint256 index = bidIndexSeed % bidCount;
uint256 bidId = bidIds[index];
if (!bidExited[bidId]) return;
if (bidClaimed[bidId]) return;
Bid memory bid = auction.bids(bidId);
try auction.claimTokens(bidId) {
bidClaimed[bidId] = true;
ghost_totalTokensClaimed += bid.tokensFilled;
totalClaims++;
} catch {}
}
function handler_batchClaim(uint256 actorSeed) public initialized {
if (!canClaim()) return;
address actor = getActor(actorSeed);
uint256[] storage actorBidList = actorBids[actor];
if (actorBidList.length == 0) return;
uint256 claimCount = 0;
uint256[] memory toClaimIds = new uint256[](actorBidList.length);
uint256 totalTokens = 0;
for (uint256 i = 0; i < actorBidList.length && claimCount < 10; i++) {
uint256 bidId = actorBidList[i];
if (bidExited[bidId] && !bidClaimed[bidId]) {
toClaimIds[claimCount] = bidId;
Bid memory bid = auction.bids(bidId);
totalTokens += bid.tokensFilled;
claimCount++;
}
}
if (claimCount == 0) return;
uint256[] memory claimIds = new uint256[](claimCount);
for (uint256 i = 0; i < claimCount; i++) {
claimIds[i] = toClaimIds[i];
}
try auction.claimTokensBatch(actor, claimIds) {
for (uint256 i = 0; i < claimCount; i++) {
bidClaimed[claimIds[i]] = true;
}
ghost_totalTokensClaimed += totalTokens;
totalClaims++;
} catch {}
}
// ===== EDGE CASE HANDLERS =====
function handler_bidMinAmount(uint256 actorSeed, uint256 priceSeed) public initialized {
if (!isAuctionActive()) return;
if (bidCount >= MAX_BIDS) return;
address actor = getActor(actorSeed);
uint256 tickNumber = 1 + (priceSeed % 100);
uint256 maxPrice = FLOOR_PRICE + tickNumber * TICK_SPACING;
if (maxPrice <= auction.clearingPrice()) return;
hook.setAttackFull(0, 0, 0, 0, 0, false, 0);
_submitBid(maxPrice, 1, actor); // 1 wei
}
function handler_bidMaxAmount(uint256 actorSeed, uint256 priceSeed) public initialized {
if (!isAuctionActive()) return;
if (bidCount >= MAX_BIDS) return;
address actor = getActor(actorSeed);
uint256 tickNumber = 1 + (priceSeed % 100);
uint256 maxPrice = FLOOR_PRICE + tickNumber * TICK_SPACING;
if (maxPrice <= auction.clearingPrice()) return;
uint128 maxAmount = uint128(address(this).balance > 1e22 ? 1e22 : address(this).balance);
if (maxAmount == 0) return;
hook.setAttackFull(0, 0, 0, 0, 0, false, 0);
_submitBid(maxPrice, maxAmount, actor);
}
function handler_bidAtFloorPrice(uint256 actorSeed, uint256 amountSeed) public initialized {
if (!isAuctionActive()) return;
if (bidCount >= MAX_BIDS) return;
address actor = getActor(actorSeed);
uint128 amount = uint128(1e15 + (amountSeed % 1e19));
// This should fail - bidding at floor price
hook.setAttackFull(0, 0, 0, 0, 0, false, 0);
_submitBid(FLOOR_PRICE, amount, actor);
}
function handler_bidJustAboveClearing(uint256 actorSeed, uint256 amountSeed) public initialized {
if (!isAuctionActive()) return;
if (bidCount >= MAX_BIDS) return;
address actor = getActor(actorSeed);
uint128 amount = uint128(1e15 + (amountSeed % 1e19));
uint256 justAbove = auction.clearingPrice() + TICK_SPACING;
hook.setAttackFull(0, 0, 0, 0, 0, false, 0);
_submitBid(justAbove, amount, actor);
}
// ===== INTERLEAVED OPERATION HANDLERS =====
function handler_rapidOperations(
uint256 op1Seed,
uint256 op2Seed,
uint256 op3Seed,
uint256 param1,
uint256 param2
) public initialized {
// Execute 3 operations in rapid succession
_executeOperation(op1Seed % 6, param1, param2);
_executeOperation(op2Seed % 6, param1, param2);
_executeOperation(op3Seed % 6, param1, param2);
}
function _executeOperation(uint256 op, uint256 param1, uint256 param2) internal {
if (op == 0) {
handler_honestBid(param1, param2, param1 + param2);
} else if (op == 1) {
handler_checkpoint();
} else if (op == 2) {
handler_forceIterate(param1);
} else if (op == 3) {
handler_exitBid(param1);
} else if (op == 4) {
handler_sweepCurrency();
} else {
handler_claimTokens(param1);
}
}
// ===== AUCTION BOUNDARY HANDLERS =====
/// @notice Handler specifically for bidding at exact start block
function handler_bidAtStartBlock(uint256 actorSeed, uint256 priceSeed, uint256 amountSeed) public initialized {
// Only run if we're exactly at start block
if (block.number != auction.startBlock()) return;
if (bidCount >= MAX_BIDS) return;
address actor = getActor(actorSeed);
uint256 tickNumber = 1 + (priceSeed % 50);
uint256 maxPrice = FLOOR_PRICE + tickNumber * TICK_SPACING;
if (maxPrice <= auction.clearingPrice()) return;
uint128 amount = uint128(1e16 + (amountSeed % 1e19));
hook.setAttackFull(0, 0, 0, 0, 0, false, 0);
_submitBid(maxPrice, amount, actor);
}
/// @notice Handler specifically for checkpointing at exact end block
function handler_checkpointAtEndBlock() public initialized {
// Only run if we're exactly at end block
if (block.number != auction.endBlock()) return;
try auction.checkpoint() {
totalCheckpoints++;
_checkClearingPriceInvariant();
_checkTotalClearedInvariant();
_checkNextActiveTickInvariant();
_checkClearingPriceSyncInvariant();
} catch {}
}
/// @notice Handler for bidding just before auction ends
function handler_bidBeforeEnd(uint256 actorSeed, uint256 priceSeed, uint256 amountSeed) public initialized {
// Only run if we're 1 block before end
if (block.number + 1 != auction.endBlock()) return;
if (!isAuctionActive()) return;
if (bidCount >= MAX_BIDS) return;
address actor = getActor(actorSeed);
uint256 tickNumber = 1 + (priceSeed % 50);
uint256 maxPrice = FLOOR_PRICE + tickNumber * TICK_SPACING;
if (maxPrice <= auction.clearingPrice()) return;
uint128 amount = uint128(1e16 + (amountSeed % 1e19));
hook.setAttackFull(0, 0, 0, 0, 0, false, 0);
_submitBid(maxPrice, amount, actor);
}
/// @notice Handler to verify sumCurrencyDemandAboveClearingQ96 after operations
function handler_checkSumDemand() public initialized {
// Compare actual sumCurrencyDemandAboveClearingQ96 with our expectations
uint256 actual = auction.sumCurrencyDemandAboveClearingQ96();
// The sum should never be negative (underflow)
// and should never exceed max reasonable value
if (actual >= type(uint256).max / 2) {
inv_sumDemandMismatch = true;
}
ghost_sumCurrencyDemandAboveClearing = actual;
}
// ===== INVARIANTS =====
// All invariants return true if not initialized to avoid false positives
function echidna_clearingPriceNeverDecreases() public view returns (bool) {
if (!_initialized) return true;
return !inv_clearingPriceDecreased;
}
function echidna_totalClearedNeverDecreases() public view returns (bool) {
if (!_initialized) return true;
return !inv_totalClearedDecreased;
}
function echidna_noBidBelowClearing() public view returns (bool) {
if (!_initialized) return true;
return !inv_bidBelowClearing;
}
function echidna_refundNeverExceedsDeposit() public view returns (bool) {
if (!_initialized) return true;
return !inv_refundExceedsDeposit;
}
function echidna_claimedNeverExceedsCleared() public view returns (bool) {
if (!_initialized) return true;
return ghost_totalTokensClaimed <= auction.totalCleared();
}
function echidna_noBalanceAnomaly() public view returns (bool) {
if (!_initialized) return true;
return !inv_balanceAnomaly;
}
function echidna_noReentrancyExploit() public view returns (bool) {
if (!_initialized) return true;
return !inv_reentrancyExploit;
}
function echidna_clearingAboveFloor() public view returns (bool) {
if (!_initialized) return true;
return auction.clearingPrice() >= auction.floorPrice();
}
function echidna_totalClearedNotExceedSupply() public view returns (bool) {
if (!_initialized) return true;
return auction.totalCleared() <= auction.totalSupply();
}
function echidna_auctionSolvent() public view returns (bool) {
if (!_initialized) return true;
if (!isAuctionEnded()) return true;
return address(auction).balance >= auction.currencyRaised();
}
function echidna_hookNoSuccessfulNestedBids() public view returns (bool) {
if (!_initialized) return true;
return hook.successfulNestedBids() == 0;
}
function echidna_hookNoSuccessfulForceIterates() public view returns (bool) {
if (!_initialized) return true;
return hook.successfulForceIterates() == 0;
}
function echidna_hookNoSuccessfulExits() public view returns (bool) {
if (!_initialized) return true;
return hook.successfulExitBids() == 0 && hook.successfulExitPartials() == 0;
}
function echidna_hookNoSuccessfulSweeps() public view returns (bool) {
if (!_initialized) return true;
return hook.successfulSweepCurrency() == 0 && hook.successfulSweepTokens() == 0;
}
function echidna_hookNoSuccessfulClaims() public view returns (bool) {
if (!_initialized) return true;
return hook.successfulClaims() == 0 && hook.successfulBatchClaims() == 0;
}
function echidna_hookNoStateCorruption() public view returns (bool) {
if (!_initialized) return true;
return !hook.stateCorruption();
}
// ===== NEW STATE CONSISTENCY INVARIANTS =====
/// @notice sumCurrencyDemandAboveClearingQ96 should never underflow to extreme values
function echidna_sumDemandConsistent() public view returns (bool) {
if (!_initialized) return true;
return !inv_sumDemandMismatch;
}
/// @notice nextActiveTickPrice must be > clearingPrice (unless max tick)
function echidna_nextActiveTickValid() public view returns (bool) {
if (!_initialized) return true;
return !inv_nextActiveTickInvalid;
}
/// @notice clearingPrice() should match latestCheckpoint().clearingPrice after checkpoint
function echidna_clearingPriceSynced() public view returns (bool) {
if (!_initialized) return true;
return !inv_clearingPriceNotSynced;
}
/// @notice Direct check: nextActiveTickPrice > clearingPrice relationship
function echidna_tickPriceAboveClearing() public view returns (bool) {
if (!_initialized) return true;
uint256 nextTick = auction.nextActiveTickPrice();
uint256 clearing = auction.clearingPrice();
// nextActiveTickPrice should be > clearingPrice unless it's max tick (no more ticks)
// or we're at floor with no bids
if (nextTick == type(uint256).max) return true; // Max tick, no more ticks initialized above
if (nextTick == 0) return true; // No ticks initialized yet
return nextTick > clearing;
}
/// @notice Direct check: sumCurrencyDemand sanity
function echidna_sumDemandSanity() public view returns (bool) {
if (!_initialized) return true;
uint256 sumDemand = auction.sumCurrencyDemandAboveClearingQ96();
// Sum should not be an obviously wrong value (like near max uint from underflow)
return sumDemand < type(uint256).max / 2;
}
// ===== TICK LIST INTEGRITY INVARIANTS =====
/// @notice Global demand counter must equal sum of reachable tick demands
function echidna_globalDemandMatchesReachable() public view returns (bool) {
if (!_initialized) return true;
return !inv_unreachableDemand;
}
/// @notice Tick list must not have cycles
function echidna_noTickListCycle() public view returns (bool) {
if (!_initialized) return true;
return !inv_tickListCycle;
}
/// @notice Tick list must be monotonically increasing
function echidna_tickListOrdered() public view returns (bool) {
if (!_initialized) return true;
return !inv_tickListUnordered;
}
// ===== LIVENESS INVARIANTS =====
/// @notice If many attempts with zero successes, something is wrong
function echidna_bidsAreReaching() public view returns (bool) {
if (!_initialized) return true;
// Only check after significant attempts
if (submitBidAttempts < 100) return true;
// At least 10% of bids should succeed
return submitBidSuccesses * 10 >= submitBidAttempts;
}
receive() external payable {}
}
Raw
echidna-invariant.yaml
# Echidna Configuration for CCAInvariantTest
# IMPORTANT: maxBlockDelay=1 prevents skipping past 100-block auction window
testMode: "property"
testLimit: 1000000
seqLen: 100
shrinkLimit: 10000
workers: 4
# Block/time constraints - CRITICAL for time-bounded auctions
maxBlockDelay: 1
maxTimeDelay: 86400
# Coverage
coverage: true
coverageFormats: ["html", "txt"]
# Give the test contract sufficient ETH for bids and attacks
balanceContract: 0xffffffffffffffffffffff
# Increase code size and gas limits for complex handlers
codeSize: 0xffffffffff
propMaxGas: 100000000
testMaxGas: 100000000
Raw
echidna.yaml
# Echidna Configuration for CCA Auction Fuzzing
# IMPORTANT: maxBlockDelay=1 prevents skipping past 100-block auction window
testMode: "property"
testLimit: 100000
shrinkLimit: 5000
# Corpus management
corpusDir: "echidna-corpus"
# Sequence settings
seqLen: 100
# Block/time constraints - CRITICAL for time-bounded auctions
maxTimeDelay: 86400
maxBlockDelay: 1
# Coverage
coverage: true
coverageFormats: ["html", "txt"]
# Workers
workers: 4
# Contract balance for bids
balanceContract: 100000000000000000000
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment