Merge pull request #1005 from ryzhak/ci/formal-verification

Author: 0x4007

.github/workflows/formal-verification.yml

@@ -0,0 +1,64 @@
+name: Formal Verification
+
+on:
+  workflow_dispatch:
+  push:
+    branches:
+      - main
+      - development
+    paths:
+      - '**.sol'
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout Repository
+        uses: actions/checkout@v5
+        with:
+          submodules: recursive
+
+      # ====================
+      # Project Dependencies
+      # ====================
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+
+      - name: Install Project Dependencies
+        run: |
+          yarn install
+          yarn workspace @ubiquity/contracts forge:install
+
+      # ====================
+      # Certora Dependencies
+      # ====================
+
+      - name: Install python
+        uses: actions/setup-python@v6
+        with: { 
+          python-version: 3.13 
+        }
+
+      - name: Install java
+        uses: actions/setup-java@v5
+        with: { 
+          java-version: "11", 
+          java-package: jre,
+          distribution: temurin
+        }
+
+      # It's recommended to pin the latest certora-cli version available in https://pypi.org/project/certora-cli/
+      - name: Install certora cli
+        run: pip install certora-cli==8.1.1
+
+      - name: Install solc
+        run: |
+          pip install solc-select
+          solc-select install 0.8.19
+          solc-select use 0.8.19
+      - name: Verify
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+        working-directory: ./packages/contracts
+        run: certoraRun test/certora/staking.conf

.gitignore

@@ -2,6 +2,7 @@ _.log
 _.pid
 _.seed
 .cache
+.certora_internal
 .DS_Store
 .dynamodb
 .env

packages/contracts/test/certora/StakingFacetHarness.sol

@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: MIT
+pragma solidity 0.8.19;
+
+import {StakingFacet} from "../../src/dollar/facets/StakingFacet.sol";
+import {AppStorage, LibAppStorage} from "../../src/dollar/libraries/LibAppStorage.sol";
+
+/**
+ * @notice Ubiquity staking facet harness
+ */
+contract StakingFacetHarness is StakingFacet {
+    /**
+     * @notice Returns reentrancy status, 1 - entered, 2 - not entered
+     * @return Reentrancy status
+     */
+    function exposed_getReentrancyStatus() external view returns (uint256) {
+        AppStorage storage store = LibAppStorage.appStorage();
+        return store.reentrancyStatus;
+    }
+}

packages/contracts/test/certora/staking.conf

@@ -0,0 +1,42 @@
+{
+    "files": [
+        "src/dollar/Diamond.sol",
+        "src/dollar/facets/AccessControlFacet.sol",
+        "src/dollar/facets/ManagerFacet.sol",
+        "src/dollar/facets/UbiquityPoolFacet.sol",
+        "src/dollar/libraries/LibStaking.sol",
+        "src/deprecated/UbiquityGovernance.sol",
+        "src/deprecated/UbiquityAlgorithmicDollarManager.sol",
+        "test/certora/StakingFacetHarness.sol",
+    ],
+    "verify": "Diamond:test/certora/staking.spec",
+    "contract_extensions": {
+        "Diamond": [
+            {
+                "extension": "AccessControlFacet",
+                "exclude": [],
+            },
+            {
+                "extension": "ManagerFacet",
+                "exclude": [],
+            },
+            {
+                "extension": "StakingFacetHarness",
+                "exclude": [],
+            },
+            {
+                "extension": "UbiquityPoolFacet",
+                "exclude": [],
+            }
+        ]
+    },
+    "link": [
+        "UbiquityGovernance:manager=UbiquityAlgorithmicDollarManager",
+    ],
+    "parametric_contracts": [
+        "Diamond",
+    ],
+    "optimistic_loop": true,
+    "rule_sanity": "basic",
+    "msg": "staking.conf",
+}