diff --git a/.github/workflows/certora-prover-conf.yml b/.github/workflows/certora-prover-conf.yml new file mode 100644 index 000000000..2d362488d --- /dev/null +++ b/.github/workflows/certora-prover-conf.yml @@ -0,0 +1,60 @@ +name: Certora Prover + +on: + push: + branches: + - dev + - payments-spec + pull_request: {} + workflow_dispatch: {} + +jobs: + list-scripts: + runs-on: ubuntu-latest + outputs: + matrix: ${{ steps.set-matrix.outputs.matrix }} + steps: + - uses: actions/checkout@v2 + - id: set-matrix + run: echo ::set-output name=matrix::$(ls certora/config/*.conf | jq -Rsc 'split("\n")[:-1]') + verify: + runs-on: ubuntu-latest + needs: list-scripts + steps: + - uses: actions/checkout@v3 + with: + submodules: recursive + - name: Install Foundry + uses: foundry-rs/foundry-toolchain@v1 + with: + version: nightly + - name: Install forge dependencies + run: forge install + - name: Install python + uses: actions/setup-python@v2 + with: + python-version: '3.10' + cache: 'pip' + - name: Install java + uses: actions/setup-java@v2 + with: + distribution: temurin + java-version: '17' + - name: Install certora + run: pip install certora-cli + - name: Install solc + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.8.12/solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc + chmod +x /usr/local/bin/solc + - name: Verify rule ${{ matrix.params }} + run: | + certoraRun ${{ matrix.params }} + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} + + strategy: + fail-fast: false + max-parallel: 4 + matrix: + params: ${{ fromJson(needs.list-scripts.outputs.matrix) }} \ No newline at end of file diff --git a/certora/config/paymentCoordinator.conf b/certora/config/paymentCoordinator.conf index 2d51d457d..aca1a6b30 100644 --- a/certora/config/paymentCoordinator.conf +++ b/certora/config/paymentCoordinator.conf @@ -1,6 +1,7 @@ { "files": [ "lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol", + "lib/openzeppelin-contracts/contracts/token/ERC20/presets/ERC20PresetFixedSupply.sol", "certora/harnesses/PaymentCoordinatorHarness.sol" ], "verify": "PaymentCoordinatorHarness:certora/specs/core/PaymentCoordinator.spec", @@ -14,5 +15,13 @@ "optimistic_fallback": true, "optimistic_loop": true, "optimistic_hashing": true, - "rule_sanity": "basic" + "rule_sanity": "basic", + "mutations": { + "gambit": [ + { + "filename" : "src/contracts/core/PaymentCoordinator.sol", + "num_mutants": 5 + } + ], + } } diff --git a/certora/specs/core/PaymentCoordinator.spec b/certora/specs/core/PaymentCoordinator.spec index fa021018a..eb40954cf 100644 --- a/certora/specs/core/PaymentCoordinator.spec +++ b/certora/specs/core/PaymentCoordinator.spec @@ -1,5 +1,6 @@ -using ERC20 as token; +using ERC20 as token1; +using ERC20PresetFixedSupply as token2; methods { @@ -17,48 +18,24 @@ methods { function _.submitRoot(bytes32 root, uint32 paymentCalculationEndTimestamp) external => DISPATCHER(true); function _.processClaim(IPaymentCoordinator.PaymentMerkleClaim claim, address recipient) external => DISPATCHER(true); - // function PaymentCoordinator._checkClaim( - // IPaymentCoordinator.PaymentMerkleC laim calldata claim, - // IPaymentCoordinator.DistributionRoot memory root - // ) internal => NONDET; -} - -// Do not need -// paymentCoordinator.submitRoot() adds a merkle root to the contract with a 7 day activationDelay - -// // Check how accept root changes the storage. -// rule acceptRootStorageChange(env e) { -// bytes32 pendingRoot; bytes32 pendingIpfsHash; -// pendingRoot, pendingIpfsHash, _ = pendingRoot(); - -// acceptRoot(e); - -// assert root() == pendingRoot; -// assert ipfsHash() == pendingIpfsHash; -// } - -// // Check an account claimed amount is correctly updated. -// rule updatedClaimedAmount(address account, address reward, uint256 claimable, bytes32[] proof) { -// claim(account, reward, claimable, proof); - -// assert claimable == claimed(account, reward); -// } - -// // Check an account can only claim greater amounts each time. -// rule increasingClaimedAmounts(address account, address reward, uint256 claimable, bytes32[] proof) { -// uint256 claimed = claimed(account, reward); - -// claim(account, reward, claimable, proof); + function _.verifyInclusionKeccak(bytes memory, bytes32, bytes32, uint256) internal => CONSTANT; + function cumulativeClaimed(address, address) external returns(uint256) envfree; -// assert claimable > claimed; -// } + function _.strategyIsWhitelistedForDeposit(address) external => NONDET; + function _.isPauser(address) external => NONDET; + function _.unpauser() external => NONDET; + function _._ external => DISPATCH [ + _.transferFrom(address, address, uint256), + _.transfer(address, uint256) + ] default NONDET; +} -// 2. Given a processClaim passes, second processClaim reverts -// Rule status: FAILS +// Given a processClaim passes, second processClaim reverts // Assumptions // - checkClaim(claim) == true and does not revert // - claim has non-empty tokenLeaves +/// status: pass rule claimWithduplicateTokenLeafs(env e, IPaymentCoordinator.PaymentMerkleClaim claim, address recipient) { require claim.tokenLeaves.length == 1; @@ -82,23 +59,47 @@ rule claimWithduplicateTokenLeafs(env e, IPaymentCoordinator.PaymentMerkleClaim ); } +/// status: pending +rule cumulativeClaimedStrictlyIncreasing(env e, address claimToken, address earner) { + uint256 cumulativeClaimedBefore = cumulativeClaimed(earner, claimToken); + calldataarg args; + method f; + f(e, args); + uint256 cumulativeClaimedAfter = cumulativeClaimed(earner, claimToken); + + assert(cumulativeClaimedAfter >= cumulativeClaimedBefore); +} + -// Check that transfer amount in paymentCoordinator.prcocessClaim() is equal to leaf.cumulativeEarnings - cumulativeClaimed +/// Check that transfer amount in paymentCoordinator.prcocessClaim() is equal to leaf.cumulativeEarnings - cumulativeClaimed /// cumulativeEarnings - cumulativeClaimed == balanceAfter - balanceBefore -/// status: Fail, havoc from token safeTransfer in the calldata +/// Initially failed from havoc from token safeTransfer in the calldata. Fixed by having unresolved catch-all calls defined +/// status: pass rule transferredTokensFromClaim(env e, IPaymentCoordinator.PaymentMerkleClaim claim, address recipient) { - require claim.tokenLeaves.length >= 1; - require token == claim.tokenLeaves[0].token; + require claim.tokenLeaves.length == 2; + require token1 == claim.tokenLeaves[0].token; + require token2 == claim.tokenLeaves[1].token; + // if recipient is the PaymentCoordinator, rule breaks since balanceAfter == balanceBefore + require recipient != currentContract; address earner = claim.earnerLeaf.earner; - uint256 balanceBefore = token.balanceOf(e, recipient); - uint256 cumulativeClaimed = cumulativeClaimed(e, earner, claim.tokenLeaves[0].token); + uint256 token1BalanceBefore = token1.balanceOf(e, recipient); + uint256 token2BalanceBefore = token2.balanceOf(e, recipient); + uint256 token1CumulativeClaimed = cumulativeClaimed(earner, claim.tokenLeaves[0].token); + uint256 token2CumulativeClaimed = cumulativeClaimed(earner, claim.tokenLeaves[1].token); processClaim(e, claim, recipient); - uint256 balanceAfter = token.balanceOf(e, recipient); + uint256 token1BalanceAfter = token1.balanceOf(e, recipient); + uint256 token2BalanceAfter = token2.balanceOf(e, recipient); - assert claim.tokenLeaves[0].cumulativeEarnings - cumulativeClaimed == balanceAfter - balanceBefore; + if (token1 == token2) { + // In practice this shouldn't occur as we will not construct leaves with multiple tokenLeaves with the same token address + assert claim.tokenLeaves[1].cumulativeEarnings - token1CumulativeClaimed == token2BalanceAfter - token2BalanceBefore; + } else { + assert claim.tokenLeaves[0].cumulativeEarnings - token1CumulativeClaimed == token1BalanceAfter - token1BalanceBefore; + assert claim.tokenLeaves[1].cumulativeEarnings - token2CumulativeClaimed == token2BalanceAfter - token2BalanceBefore; + } } /// paymentCoordinator.checkClaim == True => processClaim success