Function: batchedFinalizeWithdrawals(byte[32][] messages)

This function can be used to finalize a batch of pending withdrawals, transferring the owed USDC amounts.

Inputs

• messages

  • Control: Arbitrary.

  • Constraints: Each message must not be already finalized and correspond to a withdrawal for which the dispute period has elapsed.

  • Impact: Hashes identifying the withdrawals to be finalized.

Branches and code coverage (including function calls)

Intended branches

• For each withdrawal message, it checks the dispute period and ensures the withdrawal was not already processed, then transfers the tokens.

  Test coverage

Negative behavior

• Reverts if the withdrawal was already processed.

  Negative test

• Reverts if the dispute period has not elapsed.

  Negative test

Function call analysis

• rootFunction -> finalizeWithdrawal(messages[idx])

  • What is controllable? messages[idx].

  • If return value controllable, how is it used and how can it go wrong? N/A.

  • What happens if it reverts, reenters, or does other unusual control flow? Reverts bubble up; reentrancy is not a concern (USDC makes no external calls).

• finalizeWithdrawal -> checkDisputePeriod(withdrawal.requestedTime, withdrawal.requestedBlockNumber)

  • What is controllable? Nothing directly.

  • If return value controllable, how is it used and how can it go wrong? N/A.

  • What happens if it reverts, reenters, or does other unusual control flow? Reverts bubble up; reentrancy cannot happen (no external calls).

• finalizeWithdrawal -> usdcToken.transfer(withdrawal.user, withdrawal.usdc)

  • What is controllable? Nothing directly.

  • If return value controllable, how is it used and how can it go wrong? N/A.

  • What happens if it reverts, reenters, or does other unusual control flow? Reverts bubble up; reentrancy is not a concern (USDC makes no external calls).