Add Certora specs

.github/workflows/certora.yml

@@ -0,0 +1,46 @@
+name: Certora
+
+on: [push, pull_request]
+
+jobs:
+  certora:
+    name: Certora
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        alm-controller:
+          - rate-limits
+          - mainnet-controller
+          - foreign-controller
+
+    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.21
+        run: solc-select install 0.8.21
+
+      - name: Install Certora
+        run: pip3 install certora-cli-beta
+
+      - name: Verify ${{ matrix.alm-controller }}
+        run: make certora-${{ matrix.alm-controller }} results=1
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}

.gitmodules

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

ForeignController.conf

@@ -0,0 +1,38 @@
+{
+    "files": [
+        "spark-alm-controller/src/ForeignController.sol",
+        "spark-alm-controller/src/ALMProxy.sol",
+        "harness/CctpMock.sol",
+        "harness/Psm3Mock.sol",
+        "spark-alm-controller/src/RateLimits.sol",
+        "harness/UsdcMock.sol",
+        "harness/UsdsMock.sol",
+        "harness/SUsdsMock.sol",
+        "harness/Auxiliar.sol"
+    ],
+    "solc": "solc-0.8.21",
+    "solc_optimize": "200",
+    "packages": [
+        "forge-std/interfaces/=spark-alm-controller/lib/forge-std/src/interfaces",
+        "openzeppelin-contracts/=spark-alm-controller/lib/openzeppelin-contracts",
+        "lib/openzeppelin-contracts/=spark-alm-controller/lib/openzeppelin-contracts",
+        "spark-psm/src/interfaces/=spark-alm-controller/lib/spark-psm/src/interfaces",
+        "erc20-helpers/interfaces/=spark-alm-controller/lib/spark-psm/lib/erc20-helpers/src/interfaces",
+        "src=spark-alm-controller/src"
+    ],
+    "link": [
+        "ForeignController:proxy=ALMProxy",
+        "ForeignController:cctp=CctpMock",
+        "ForeignController:psm=Psm3Mock",
+        "ForeignController:rateLimits=RateLimits",
+        "ForeignController:usdc=UsdcMock"
+    ],
+    "verify": "ForeignController:ForeignController.spec",
+    "rule_sanity": "basic",
+    "multi_assert_check": true,
+    "optimistic_loop": true,
+    "parametric_contracts": ["ForeignController"],
+    "smt_timeout": "7000",
+    "build_cache": true,
+    "msg": "ForeignController"
+}