[Certora][H-02] NFT Withdrawal Price Finalization

[jtfirek]

Motivation

This pr addresses the concerns with the withdrawal flow raised by the certora team during the audit:

• The withdrawal requests claim process is unfair as users are exposed to the ramifications of a negative rebase after their request is finalized
• eETH requested for withdrawal still accrue staking rewards after requests are made. These positive rebase rewards remain in this contract after users claim their withdrawal, but there is currently no accounting or method to withdraw these funds as revenue

Features

• A new mechanism to finalize the value of request when its corresponding batch of withdrawals is processed by the oracle. Note that users are still exposed to negative rebases that occur before finalization
• Logic to query and claim the excess staking rewards mentioned above
• Removal of unnecessary accounting like EthAmountLockedForWithdrawal in the new flow
• Refactor the codebase to consistently use uint32 for withdrawal NFT id values

Migration

• To make the existing unclaimed finalized withdrawals work with the new system, lastFinalizedRequestId will be reset to 0 and the oracle will re-finalize all withdrawals with the new logic. It will be much to expensive to call calculateTotalPendingAmount on 30,000ish withdrawals. We will have to calculate the amount needed to re-finalized all the withdrawals off-chain and pass it on-chain with finalizeRequests(uint256 lastRequestId, uint256 totalAmount). The ability to withdrawal will be temporary paused to maintain correct accounting

[jtfirek]

fyi, The failing unit tests on the last run are from Eigenpod changes from the PEPE upgrade

[vvalecha519]

I think you can get rid of binary search and just use a map, m, of lastFinalizedRequestId -> finalizedPrice
and add lastFinalizedRequestId in WithdrawRequest. This might simplify everything. Let me know what you think and then I will re-review.

Ie. if someone wants to claim we find their WithdrawRequest get the lastFinalizedRequestId and then find the price in the map m to find the finalizedPrice.

[jtfirek]

Here is a situation that breaks this approach:

• Let's say we have request A and request B created during the same oracle report period; they will be created with the same lastFinalizedRequestId value
• Later request A is finalized as the last request in a batch and request B isn't finalized till the next batch
• Both request A and B will incorrectly map to the same finalizedPrice