Feat: add Certora specs

.gitattributes

@@ -0,0 +1,3 @@
+*.spec linguist-language=Solidity
+*.conf linguist-detectable
+*.conf linguist-language=JSON5

.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
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+
+      - uses: actions/setup-java@v3
+        with:
+          distribution: 'zulu'
+          java-version: '11'
+          java-package: jre
+
+      - name: Set up Python 3.13
+        uses: actions/setup-python@v4
+        with:
+          python-version: 3.13
+
+      - name: Install solc-select
+        run: pip3 install solc-select
+
+      - name: Solc Select 0.8.24
+        run: solc-select install 0.8.24
+
+      - name: Solc Select 0.8.21
+        run: solc-select install 0.8.21
+
+      - name: Solc Select 0.5.12
+        run: solc-select install 0.5.12
+
+      - name: Install Certora
+        run: pip3 install certora-cli-beta
+
+      - name: Certora verify SPBEAM
+        run: make certora-spbeam
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+

.gitignore

@@ -16,4 +16,7 @@ docs/
 # Ignores script config
 /script/input/**/*.json
 !/script/input/**/template-*.json
-/script/output/**/*.json
+/script/output/**/*.json
+
+# Certora
+.certora_internal/

Makefile

@@ -0,0 +1,3 @@
+PATH := ~/.solc-select/artifacts/solc-0.8.24:~/.solc-select/artifacts/solc-0.8.21:~/.solc-select/artifacts/solc-0.5.12:~/.solc-select/artifacts:$(PATH)
+certora-spbeam:; PATH=${PATH} certoraRun certora/SPBEAM.conf$(if $(rule), --rule $(rule),)
+

certora/SPBEAM.conf

@@ -0,0 +1,57 @@
+{
+  "files": [
+    "src/SPBEAM.sol",
+    "certora/mocks/Conv.sol",
+    "certora/mocks/Jug.sol",
+    "certora/mocks/Pot.sol",
+    "certora/mocks/SUsds.sol",
+    "certora/mocks/Usds.sol",
+    "certora/mocks/UsdsJoin.sol",
+    "certora/mocks/Vat.sol"
+  ],
+  "link": [
+    "Jug:vat=Vat",
+    "Pot:vat=Vat",
+    "SUsds:vat=Vat",
+    "UsdsJoin:usds=Usds",
+    "UsdsJoin:vat=Vat",
+    "SPBEAM:jug=Jug",
+    "SPBEAM:pot=Pot",
+    "SPBEAM:susds=SUsds",
+    "SPBEAM:conv=Conv"
+  ],
+  "solc_map": {
+    "Conv": "solc-0.8.24",
+    "SPBEAM": "solc-0.8.24",
+    "Jug": "solc-0.5.12",
+    "Pot": "solc-0.5.12",
+    "SUsds": "solc-0.8.21",
+    "Usds": "solc-0.8.21",
+    "UsdsJoin": "solc-0.8.21",
+    "Vat": "solc-0.5.12"
+  },
+  "solc_optimize_map": {
+    "Conv": "200",
+    "SPBEAM": "200",
+    "Jug": "0",
+    "Pot": "0",
+    "SUsds": "200",
+    "Usds": "200",
+    "UsdsJoin": "200",
+    "Vat": "0"
+  },
+  "verify": "SPBEAM:certora/SPBEAM.spec",
+  "parametric_contracts": [
+    "SPBEAM"
+  ],
+  "build_cache": true,
+  "loop_iter": "3",
+  "multi_assert_check": true,
+  "optimistic_loop": true,
+  "process": "emv",
+  "prover_args": [
+    " -rewriteMSizeAllocations true"
+  ],
+  "rule_sanity": "basic",
+  "wait_for_results": "all"
+}