Skip to content

Conversation

@Vectorized
Copy link
Owner

@Vectorized Vectorized commented Sep 25, 2024

Description

Confidence level is 99.999%.

  • The boolean conditions are checked against their simple ground truths with Halmos.
  • The transferFrom logic is duplicated in a super left-curved way.

Checklist

Ensure you completed all of the steps below before submitting your pull request:

  • Ran forge fmt?
  • Ran forge test?

Pull requests with an incomplete checklist will be thrown out.

@Vectorized Vectorized merged commit d3a43a9 into main Sep 25, 2024
@Vectorized Vectorized requested a review from atarpara September 25, 2024 22:54
@Vectorized Vectorized deleted the permit2-erc20 branch September 25, 2024 23:28
Comment on lines +262 to +300
let from_ := shl(96, from)
if iszero(eq(caller(), _PERMIT2)) {
// Compute the allowance slot and load its value.
mstore(0x20, caller())
mstore(0x0c, or(from_, _ALLOWANCE_SLOT_SEED))
let allowanceSlot := keccak256(0x0c, 0x34)
let allowance_ := sload(allowanceSlot)
// If the allowance is not the maximum uint256 value.
if not(allowance_) {
// Revert if the amount to be transferred exceeds the allowance.
if gt(amount, allowance_) {
mstore(0x00, 0x13be252b) // `InsufficientAllowance()`.
revert(0x1c, 0x04)
}
// Subtract and store the updated allowance.
sstore(allowanceSlot, sub(allowance_, amount))
}
}
// Compute the balance slot and load its value.
mstore(0x0c, or(from_, _BALANCE_SLOT_SEED))
let fromBalanceSlot := keccak256(0x0c, 0x20)
let fromBalance := sload(fromBalanceSlot)
// Revert if insufficient balance.
if gt(amount, fromBalance) {
mstore(0x00, 0xf4d678b8) // `InsufficientBalance()`.
revert(0x1c, 0x04)
}
// Subtract and store the updated allowance.
sstore(allowanceSlot, sub(allowance_, amount))
// Subtract and store the updated balance.
sstore(fromBalanceSlot, sub(fromBalance, amount))
// Compute the balance slot of `to`.
mstore(0x00, to)
let toBalanceSlot := keccak256(0x0c, 0x20)
// Add and store the updated balance of `to`.
// Will not overflow because the sum of all user balances
// cannot exceed the maximum uint256 value.
sstore(toBalanceSlot, add(sload(toBalanceSlot), amount))
// Emit the {Transfer} event.
mstore(0x20, amount)
log3(0x20, 0x20, _TRANSFER_EVENT_SIGNATURE, shr(96, from_), shr(96, mload(0x0c)))
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This chunk of code is the same for both branches, with the only exception being that for the _givePermit2InfiniteAllowance() branch, if msg.sender == _PERMIT2, the allowance logic will be skipped.

Comment on lines +384 to +388
// If `spender == _PERMIT2 && value != type(uint256).max`.
if iszero(or(xor(shr(96, shl(96, spender)), _PERMIT2), iszero(not(value)))) {
mstore(0x00, 0x3f68539a) // `Permit2AllowanceIsFixedAtInfinity()`.
revert(0x1c, 0x04)
}
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This expression's equivalence has been verified with Halmos.

let allowance_ := sload(allowanceSlot)
// If the allowance is not the maximum uint256 value.
if add(allowance_, 1) {
if not(allowance_) {
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This expression's equivalence has been verified with Halmos.

Comment on lines +189 to +193
// If `spender == _PERMIT2 && amount != type(uint256).max`.
if iszero(or(xor(shr(96, shl(96, spender)), _PERMIT2), iszero(not(amount)))) {
mstore(0x00, 0x3f68539a) // `Permit2AllowanceIsFixedAtInfinity()`.
revert(0x1c, 0x04)
}
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This expression's equivalence has been verified with Halmos.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants