Invariant testing campaign

[clement-ux]

Goal

This PR aims to bring invariant testing to ensure a better test coverage of LidoARM.sol contract.

What is Invariant testing

In stateless fuzzing test that are already implemented (in swap), a single function is tested with multiple random inputs. But after each call the state is reverted.

In contract, invariant testing can be seen as stateful fuzzing test as it evaluates a group of unchanging conditions against randomized sequences of predefined contract functions.

The system checks these invariant conditions after each function call.This method is particularly effective at uncovering flaws in protocol logic. By using randomized function sequences and fuzzy inputs, invariant testing can reveal faulty assumptions and errors in complex protocol states and edge cases that might otherwise go unnoticed.

Technical description

List of called functions:

During the invariant tests, multiple random function will be called, here is the list of function that can be called:

• deposit()
• requestRedeem()
• claimRedeem()
• swapExactTokensForTokens()
• swapTokensForExactTokens()
• setPrices()
• setCrossPrice()
• collectFees()
• setFees()
• requestStETHWithdrawalForETH()
• claimStETHWithdrawalForWETH()

External functions

• donateStETH()
• donateWETH()

Custom probability distribution

During invariant testing process, by default Foundry will call randomly functions, with the same exact probability.

However, sometime this doesn't make sense and it doesn't represent what will happen once contract will be deployed.
For example deposit() or swapExactTokensForTokens() will be called way more often than setFees(). To overcome this problem, we introduce Custom Probability Distribution.

Instead of Foundry directly calling random function, Foundry will be forced to call DistributionHandler.sol which only have a single function distributorEntryPoint(). Which will in turn call entryPoint() of the underlying handler with a custom probability. This entryPoint() will in turn one of the function implemented in the handler with a custom probability. This gives us much greater granularity!

Mocks

Invariant testing performs a lot of call, so in order to make it faster, mocks are implemented instead of forking mainnet.
Mocks are used for:

• WETH
• STETH
• Lido Withdraw

To simulate STETH rounding issue on transfer, the mock randomly transfer -0 or -1 wei.

arm-oeth/test/invariants/mocks/MockSTETH.sol

Lines 35 to 46 in 257468e

	function brutalizeAmount(uint256 amount) public returns (uint256) {
	// Only brutalize the sender doesn't sent all of their balance
	if (balanceOf[msg.sender] != amount && amount > 0) {
	// Get a random number between 0 and 1
	uint256 randomUint = vm.randomUint(0, 1);
	// If the amount is greater than the random number, subtract the random number from the amount
	if (amount > randomUint) {
	amount -= randomUint;
	sum_of_errors += randomUint;
	}
	}
	return amount;

To simulate Lido Withdraw and make it easier to work with, there is no finalization process, i.e. as soon as the request is done, the ARM can withdraw it and will receive ETH.

arm-oeth/test/invariants/mocks/MockLidoWithdraw.sol

Lines 80 to 82 in 257468e

	// Send sum of eth
	vm.deal(address(msg.sender), address(msg.sender).balance + sum);
	}

Invariants assertions

At the end of each call, all the invariants will be asserted. Here is a non-exhaustive list of invariants used:

# Swap functionalities (swap)
   * Invariant A: weth balance == ∑deposit + ∑wethIn + ∑wethRedeem + ∑wethDonated - ∑withdraw - ∑wethOut - ∑feesCollected
   * Invariant B: steth balance >= ∑stethIn + ∑stethDonated - ∑stethOut - ∑stethRedeem
    
# Liquidity provider functionalities (lp)
  # Shares:
    * Invariant A: ∑shares > 0 due to initial deposit
    * Invariant B: totalShares == ∑userShares + deadShares
    * Invariant C: previewRedeem(∑shares) == totalAssets
    * Invariant D: previewRedeem(shares) == (, uint256 assets) = previewRedeem(shares) Not really invariant, but tested on handler
    * Invariant E: previewDeposit(amount) == uint256 shares = previewDeposit(amount) Not really invariant, but tested on handler
    * Invariant L: ∀ user, user.weth + previewRedeem(user.shares) >=~ initialBalance , approxGe, to handle rounding error on deposit.

  # Withdraw Queue:
    * Invariant F: nextWithdrawalIndex == requestRedeem call count
    * Invariant G: withdrawsQueued == ∑requestRedeem.amount
    * Invariant H: withdrawsQueued > withdrawsClaimed
    * Invariant I: withdrawsQueued == ∑request.assets
    * Invariant J: withdrawsClaimed == ∑claimRedeem.amount
    * Invariant K: ∀ requestId, request.queued >= request.assets

  # Fees:
    * Invariant M: ∑feesCollected == feeCollector.balance

# Lido Liquidity Manager functionalities
    * Invariant A: outstandingEther == ∑lidoRequestRedeem.assets
    * Invariant B: address(arm).balance == 0
    * Invariant C: All slots allow for gap to be empty

# After invariants
    * Ensure all user can withdraw their funds.

[naddison36]

wow, this is amazing