diff --git a/certora/Ngt.spec b/certora/Ngt.spec index 4204551..d330c5e 100644 --- a/certora/Ngt.spec +++ b/certora/Ngt.spec @@ -292,102 +292,6 @@ rule approve_revert(address spender, uint256 value) { assert lastReverted => revert1, "Revert rules are not covering all the cases"; } -// Verify correct storage changes for non reverting increaseAllowance -rule increaseAllowance(address spender, uint256 value) { - env e; - - address anyUsr; - address anyUsr2; address anyUsr3; - require anyUsr2 != e.msg.sender || anyUsr3 != spender; - - mathint wardsBefore = wards(anyUsr); - mathint totalSupplyBefore = totalSupply(); - mathint balanceOfBefore = balanceOf(anyUsr); - mathint allowanceSenderSpenderBefore = allowance(e.msg.sender, spender); - mathint allowanceOtherBefore = allowance(anyUsr2, anyUsr3); - mathint noncesBefore = nonces(anyUsr); - - increaseAllowance(e, spender, value); - - mathint wardsAfter = wards(anyUsr); - mathint totalSupplyAfter = totalSupply(); - mathint balanceOfAfter = balanceOf(anyUsr); - mathint allowanceSenderSpenderAfter = allowance(e.msg.sender, spender); - mathint allowanceOtherAfter = allowance(anyUsr2, anyUsr3); - mathint noncesAfter = nonces(anyUsr); - - assert wardsAfter == wardsBefore, "increaseAllowance did not keep unchanged wards"; - assert totalSupplyAfter == totalSupplyBefore, "increaseAllowance did not keep unchanged totalSupply"; - assert balanceOfAfter == balanceOfBefore, "increaseAllowance did not keep unchanged every balanceOf[x]"; - assert allowanceSenderSpenderAfter == allowanceSenderSpenderBefore + value, "increaseAllowance did not increase allowance[sender][spender] by value"; - assert allowanceOtherAfter == allowanceOtherBefore, "increaseAllowance did not keep unchanged the rest of allowance[x][y]"; - assert noncesAfter == noncesBefore, "increaseAllowance did not keep unchanged every nonces[x]"; -} - -// Verify revert rules on increaseAllowance -rule increaseAllowance_revert(address spender, uint256 value) { - env e; - - mathint allowanceSenderSpender = allowance(e.msg.sender, spender); - - increaseAllowance@withrevert(e, spender, value); - - bool revert1 = e.msg.value > 0; - bool revert2 = allowanceSenderSpender + value > max_uint256; - - assert revert1 => lastReverted, "revert1 failed"; - assert revert2 => lastReverted, "revert2 failed"; - assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases"; -} - -// Verify correct storage changes for non reverting decreaseAllowance -rule decreaseAllowance(address spender, uint256 value) { - env e; - - address anyUsr; - address anyUsr2; address anyUsr3; - require anyUsr2 != e.msg.sender || anyUsr3 != spender; - - mathint wardsBefore = wards(anyUsr); - mathint totalSupplyBefore = totalSupply(); - mathint balanceOfBefore = balanceOf(anyUsr); - mathint allowanceSenderSpenderBefore = allowance(e.msg.sender, spender); - mathint allowanceOtherBefore = allowance(anyUsr2, anyUsr3); - mathint noncesBefore = nonces(anyUsr); - - decreaseAllowance(e, spender, value); - - mathint wardsAfter = wards(anyUsr); - mathint totalSupplyAfter = totalSupply(); - mathint balanceOfAfter = balanceOf(anyUsr); - mathint allowanceSenderSpenderAfter = allowance(e.msg.sender, spender); - mathint allowanceOtherAfter = allowance(anyUsr2, anyUsr3); - mathint noncesAfter = nonces(anyUsr); - - assert wardsAfter == wardsBefore, "decreaseAllowance did not keep unchanged wards"; - assert totalSupplyAfter == totalSupplyBefore, "decreaseAllowance did not keep unchanged totalSupply"; - assert balanceOfAfter == balanceOfBefore, "decreaseAllowance did not keep unchanged every balanceOf[x]"; - assert allowanceSenderSpenderAfter == allowanceSenderSpenderBefore - value, "decreaseAllowance did not decrease allowance[sender][spender] by value"; - assert allowanceOtherAfter == allowanceOtherBefore, "decreaseAllowance did not keep unchanged the rest of allowance[x][y]"; - assert noncesAfter == noncesBefore, "decreaseAllowance did not keep unchanged every nonces[x]"; -} - -// Verify revert rules on decreaseAllowance -rule decreaseAllowance_revert(address spender, uint256 value) { - env e; - - mathint allowanceSenderSpender = allowance(e.msg.sender, spender); - - decreaseAllowance@withrevert(e, spender, value); - - bool revert1 = e.msg.value > 0; - bool revert2 = allowanceSenderSpender - value < 0; - - assert revert1 => lastReverted, "revert1 failed"; - assert revert2 => lastReverted, "revert2 failed"; - assert lastReverted => revert1 || revert2, "Revert rules are not covering all the cases"; -} - // Verify correct storage changes for non reverting mint rule mint(address to, uint256 value) { env e; diff --git a/lib/token-tests b/lib/token-tests index e87772a..cdb99fb 160000 --- a/lib/token-tests +++ b/lib/token-tests @@ -1 +1 @@ -Subproject commit e87772a56b28c806b482c89c03ac02b37de2c428 +Subproject commit cdb99fb503213c02728c1ece010fa54644ea40af diff --git a/src/Ngt.sol b/src/Ngt.sol index f975e14..92d48da 100644 --- a/src/Ngt.sol +++ b/src/Ngt.sol @@ -100,7 +100,7 @@ contract Ngt { unchecked { balanceOf[msg.sender] = balance - value; - balanceOf[to] += value; + balanceOf[to] += value; // note: we don't need an overflow check here b/c sum of all balances == totalSupply } emit Transfer(msg.sender, to, value); @@ -126,7 +126,7 @@ contract Ngt { unchecked { balanceOf[from] = balance - value; - balanceOf[to] += value; + balanceOf[to] += value; // note: we don't need an overflow check here b/c sum of all balances == totalSupply } emit Transfer(from, to, value); @@ -142,28 +142,6 @@ contract Ngt { return true; } - function increaseAllowance(address spender, uint256 addedValue) external returns (bool) { - uint256 newValue = allowance[msg.sender][spender] + addedValue; - allowance[msg.sender][spender] = newValue; - - emit Approval(msg.sender, spender, newValue); - - return true; - } - - function decreaseAllowance(address spender, uint256 subtractedValue) external returns (bool) { - uint256 allowed = allowance[msg.sender][spender]; - require(allowed >= subtractedValue, "Ngt/insufficient-allowance"); - unchecked{ - allowed = allowed - subtractedValue; - } - allowance[msg.sender][spender] = allowed; - - emit Approval(msg.sender, spender, allowed); - - return true; - } - // --- Mint/Burn --- function mint(address to, uint256 value) external auth { require(to != address(0) && to != address(this), "Ngt/invalid-address"); @@ -203,7 +181,7 @@ contract Ngt { address signer, bytes32 digest, bytes memory signature - ) internal view returns (bool) { + ) internal view returns (bool valid) { if (signature.length == 65) { bytes32 r; bytes32 s; @@ -218,12 +196,14 @@ contract Ngt { } } - (bool success, bytes memory result) = signer.staticcall( - abi.encodeWithSelector(IERC1271.isValidSignature.selector, digest, signature) - ); - return (success && - result.length == 32 && - abi.decode(result, (bytes4)) == IERC1271.isValidSignature.selector); + if (signer.code.length > 0) { + (bool success, bytes memory result) = signer.staticcall( + abi.encodeCall(IERC1271.isValidSignature, (digest, signature)) + ); + valid = (success && + result.length == 32 && + abi.decode(result, (bytes4)) == IERC1271.isValidSignature.selector); + } } function permit(