Add Certora specs

.github/workflows/certora.yml

@@ -0,0 +1,41 @@
+name: Certora
+
+on: [push, pull_request]
+
+jobs:
+  certora:
+    name: Certora
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - uses: actions/setup-java@v2
+        with:
+          distribution: 'zulu'
+          java-version: '11'
+          java-package: jre
+
+      - name: Set up Python 3.8
+        uses: actions/setup-python@v3
+        with:
+          python-version: 3.8
+
+      - name: Install solc-select
+        run: pip3 install solc-select
+
+      - name: Solc Select 0.8.20
+        run: solc-select install 0.8.20
+
+      - name: Install Certora
+        run: pip3 install certora-cli-beta
+
+      - name: Verify Psm3
+        run: make certora-psm3 results=1
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}

.gitignore

@@ -0,0 +1 @@
+.certora_internal

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "spark-psm"]
+	path = spark-psm
+	url = https://github.com/marsfoundation/spark-psm.git

Makefile

@@ -0,0 +1,2 @@
+PATH := ~/.solc-select/artifacts/:~/.solc-select/artifacts/solc-0.8.20:$(PATH)
+certora-psm3 :; PATH=${PATH} certoraRun PSM3.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,)

PSM3.conf

@@ -0,0 +1,35 @@
+{
+    "files": [
+        "spark-psm/src/PSM3.sol",
+        "spark-psm/test/mocks/MockRateProvider.sol",
+        "harness/GemMock.sol", // Adding this one in order the prover also checks with an invalid asset
+        "harness/GemMock.sol:USDCMock",
+        "harness/GemMock.sol:USDSMock",
+        "harness/GemMock.sol:SUSDSMock"
+    ],
+    "solc": "solc-0.8.20",
+    "solc_optimize": "200",
+    "packages": [
+        "erc20-helpers=spark-psm/lib/erc20-helpers/src",
+        "openzeppelin-contracts/=spark-psm/lib/openzeppelin-contracts",
+        "src=spark-psm/src"
+    ],
+    "link": [
+        "PSM3:rateProvider=MockRateProvider",
+        "PSM3:usdc=USDCMock",
+        "PSM3:usds=USDSMock",
+        "PSM3:susds=SUSDSMock",
+    ],
+    "verify": "PSM3:PSM3.spec",
+    "rule_sanity": "basic",
+    "multi_assert_check": true,
+    "parametric_contracts": ["PSM3"],
+    "smt_timeout": "7200",
+    "global_timeout": "7200",
+    "prover_args": [
+        "-depth 0",
+        " -s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]"
+    ],
+    "build_cache": true,
+    "msg": "PSM3"
+}

harness/GemMock.sol

@@ -0,0 +1,106 @@
+// SPDX-License-Identifier: AGPL-3.0-or-later
+
+// Copyright (C) 2024 Dai Foundation
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU Affero General Public License as published by
+// the Free Software Foundation, either version 3 of the License, or
+// (at your option) any later version.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU Affero General Public License for more details.
+//
+// You should have received a copy of the GNU Affero General Public License
+// along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+pragma solidity ^0.8.20;
+
+contract GemMock {
+    mapping (address => uint256)                      public wards;
+    mapping (address => uint256)                      public balanceOf;
+    mapping (address => mapping (address => uint256)) public allowance;
+
+    uint256 public totalSupply;
+
+    uint256 public decimals;
+
+    modifier auth() {
+        require(wards[msg.sender] == 1, "Gem/not-authorized");
+        _;
+    }
+
+    function rely(address usr) external auth { wards[usr] = 1; }
+    function deny(address usr) external auth { wards[usr] = 0; }
+
+    function approve(address spender, uint256 value) external returns (bool) {
+        allowance[msg.sender][spender] = value;
+        return true;
+    }
+
+    function transfer(address to, uint256 value) external returns (bool) {
+        uint256 balance = balanceOf[msg.sender];
+        require(balance >= value, "Gem/insufficient-balance");
+
+        unchecked {
+            balanceOf[msg.sender] = balance - value;
+        }
+        balanceOf[to] += value;
+        return true;
+    }
+
+    function transferFrom(address from, address to, uint256 value) external returns (bool) {
+        uint256 balance = balanceOf[from];
+        require(balance >= value, "Gem/insufficient-balance");
+
+        if (from != msg.sender) {
+            uint256 allowed = allowance[from][msg.sender];
+            if (allowed != type(uint256).max) {
+                require(allowed >= value, "Gem/insufficient-allowance");
+
+                unchecked {
+                    allowance[from][msg.sender] = allowed - value;
+                }
+            }
+        }
+
+        unchecked {
+            balanceOf[from] = balance - value;
+        }
+        balanceOf[to] += value;
+        return true;
+    }
+
+    function mint(address to, uint256 value) public auth {
+        unchecked {
+            balanceOf[to] = balanceOf[to] + value;
+        }
+        totalSupply = totalSupply + value;
+    }
+
+    function burn(address from, uint256 value) external {
+        uint256 balance = balanceOf[from];
+        require(balance >= value, "Gem/insufficient-balance");
+
+        if (from != msg.sender) {
+            uint256 allowed = allowance[from][msg.sender];
+            if (allowed != type(uint256).max) {
+                require(allowed >= value, "Gem/insufficient-allowance");
+
+                unchecked {
+                    allowance[from][msg.sender] = allowed - value;
+                }
+            }
+        }
+
+        unchecked {
+            balanceOf[from] = balance - value;
+            totalSupply     = totalSupply - value;
+        }
+    }
+}
+
+contract USDCMock is GemMock {}
+contract USDSMock is GemMock {}
+contract SUSDSMock is GemMock {}