Add PermitERC721 Certora Specs (#802)

* add erc721-permit certora specs

* cleanup

.gitignore

@@ -15,4 +15,10 @@ coverage/
 report/
 keystore/
 broadcast/
-logFile.txt
+logFile.txt
+
+# Certora
+.certora_internal/
+.certora_recent_jobs.json
+.zip-output-url.txt
+*.zip

Makefile

@@ -32,6 +32,9 @@ test-invariant-erc721-precision :; ./tests/forge/invariants/test-invariant-erc72
 test-invariant-erc20-buckets    :; ./tests/forge/invariants/test-invariant-erc20-buckets.sh
 test-invariant-erc721-buckets   :; ./tests/forge/invariants/test-invariant-erc721-buckets.sh
 
+# Certora
+certora-erc721-permit          :; $(if $(CERTORAKEY),, @echo "set certora key"; exit 1;) PATH=~/.solc-select/artifacts/solc-0.8.14:~/.solc-select/artifacts:${PATH} certoraRun --solc_map PermitERC721Harness=solc-0.8.14,Auxiliar=solc-0.8.14,SignerMock=solc-0.8.14 --optimize_map PermitERC721Harness=500,Auxiliar=0,SignerMock=0 --rule_sanity basic certora/harness/PermitERC721Harness.sol certora/Auxiliar.sol certora/SignerMock.sol --verify PermitERC721Harness:certora/PermitERC721.spec --multi_assert_check $(if $(short), --short_output,)
+
 # Generate Gas Snapshots
 snapshot :; forge clean && forge snapshot
 

certora/Auxiliar.sol

@@ -0,0 +1,50 @@
+pragma solidity 0.8.14;
+
+contract Auxiliar {    
+    function computeDigest(
+        bytes32 domain_separator,
+        bytes32 permit_typehash,
+        address spender,
+        uint256 tokenId,
+        uint256 nonce,
+        uint256 deadline
+    ) public pure returns (bytes32 digest){
+        digest =
+        keccak256(
+            abi.encodePacked(
+                "\x19\x01",
+                domain_separator,
+                keccak256(
+                    abi.encode(
+                        permit_typehash,
+                        spender,
+                        tokenId,
+                        nonce,
+                        deadline
+                ))
+        ));
+    }
+
+    function call_ecrecover(
+        bytes32 digest,
+        uint8 v,
+        bytes32 r,
+        bytes32 s
+    ) public pure returns (address signer) {
+        signer = ecrecover(digest, v, r, s);
+    }
+
+    function signatureToVRS(bytes memory signature) public returns (uint8 v, bytes32 r, bytes32 s) {
+        if (signature.length == 65) {
+            assembly {
+                r := mload(add(signature, 0x20))
+                s := mload(add(signature, 0x40))
+                v := byte(0, mload(add(signature, 0x60)))
+            }
+        }
+    }
+
+    function isContract(address owner) public returns (bool) {
+        return owner.code.length > 0;
+    }
+}

certora/PermitERC721.spec

@@ -0,0 +1,77 @@
+// PermitERC721.spec
+
+using Auxiliar as aux
+using SignerMock as signer
+
+methods {
+    getApproved(uint256) returns (address) envfree
+    ownerOf(uint256) returns (address) envfree
+    nonces(uint256) returns (uint96) envfree
+    DOMAIN_SEPARATOR() returns (bytes32) envfree
+    PERMIT_TYPEHASH() returns (bytes32) envfree
+    aux.call_ecrecover(bytes32, uint8, bytes32, bytes32) returns (address) envfree
+    aux.computeDigest(bytes32, bytes32, address, uint256, uint256, uint256) returns (bytes32) envfree
+    aux.signatureToVRS(bytes) returns (uint8, bytes32, bytes32) envfree
+    aux.isContract(address) returns (bool) envfree
+    isValidSignature(bytes32, bytes) returns (bytes4) => DISPATCHER(true)
+}
+
+// Verify that allowance behaves correctly on permit
+rule permit(address spender, address tokenId, uint256 deadline, bytes signature) {
+    env e;
+
+    uint8 v; bytes32 r; bytes32 s;
+    v, r, s = aux.signatureToVRS(signature);
+
+    permit(e, spender, tokenId, deadline, v, r, s);
+
+    assert(getApproved(tokenId) == spender, "assert1 failed");
+}
+
+// Verify revert rules on permit
+rule permit_revert(address spender, uint256 tokenId, uint256 deadline, bytes signature) {
+    env e;
+
+    uint8 v; bytes32 r; bytes32 s;
+    v, r, s = aux.signatureToVRS(signature);
+
+    uint256 tokenIdNonce = nonces(tokenId);
+    address owner = ownerOf(tokenId);
+
+    bytes32 digest = aux.computeDigest(
+                        DOMAIN_SEPARATOR(),
+                        PERMIT_TYPEHASH(),
+                        spender,
+                        tokenId,
+                        tokenIdNonce,
+                        deadline
+                    );
+
+    address ownerRecover = aux.call_ecrecover(digest, v, r, s);
+    bytes32 returnedSig = signer.isValidSignature(e, digest, signature);
+    bool isContract = aux.isContract(owner);
+
+    permit@withrevert(e, spender, tokenId, deadline, v, r, s);
+
+    bool revert1 = e.msg.value > 0;
+    bool revert2 = e.block.timestamp > deadline;
+    bool revert3 = owner == 0;
+    bool revert4 = owner == spender;
+    bool revert5 = isContract  && returnedSig  != 0x1626ba7e00000000000000000000000000000000000000000000000000000000;
+    bool revert6 = !isContract && ownerRecover == 0;
+    bool revert7 = !isContract && ownerRecover != owner;
+    bool revert8 = tokenIdNonce == max_uint96;
+
+    assert(revert1 => lastReverted, "revert1 failed");
+    assert(revert2 => lastReverted, "revert2 failed");
+    assert(revert3 => lastReverted, "revert3 failed");
+    assert(revert4 => lastReverted, "revert4 failed");
+    assert(revert5 => lastReverted, "revert5 failed");
+    assert(revert6 => lastReverted, "revert6 failed");
+    assert(revert7 => lastReverted, "revert7 failed");
+    assert(revert8 => lastReverted, "revert8 failed");
+
+    assert(lastReverted => revert1 || revert2 || revert3 ||
+                           revert4 || revert5 || revert6 ||
+                           revert7 || revert8, "Revert rules are not covering all the cases");
+}

certora/SignerMock.sol

@@ -0,0 +1,11 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+
+pragma solidity ^0.8.14;
+
+contract SignerMock {
+    bytes32 sig;
+
+    function isValidSignature(bytes32, bytes memory) external view returns (bytes32) {
+        return sig;
+    }
+}

certora/harness/PermitERC721Harness.sol

@@ -0,0 +1,18 @@
+pragma solidity 0.8.14;
+
+import { PermitERC721 } from '../../src/base/PermitERC721.sol';
+
+contract PermitERC721Harness is PermitERC721 { 
+
+    // overrides internal nonces
+    mapping(uint256 => uint96) public nonces;
+
+    constructor() PermitERC721("Ajna Positions NFT-V1", "AJNA-V1-POS", "1") public {}
+
+    // PostionManager.sol
+    function _getAndIncrementNonce(
+        uint256 tokenId_
+    ) internal override returns (uint256) {
+        return uint256(nonces[tokenId_]++);
+    }
+}