Skip to content

feat: formal verification for UbiquityPoolFacet (#926) #1048

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wbobbynmworley wants to merge 2 commits into from
Closed

feat: formal verification for UbiquityPoolFacet (#926) #1048

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b64e25f
fix: skip storage check for new contracts/libraries
wbobbynmworley May 17, 2026
e6dfa2f
feat: add Certora formal verification for UbiquityPoolFacet
May 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 21 additions & 5 deletions .github/workflows/core-contracts-storage-check.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ jobs:
- uses: actions/checkout@v3
with:
submodules: recursive
persist-credentials: false

- name: Install Foundry
uses: foundry-rs/foundry-toolchain@v1
Expand All @@ -33,10 +34,25 @@ jobs:
env:
CHANGED_CONTRACTS: ${{ steps.changed-contracts.outputs.contracts_all_changed_files }}
run: |
# Filter out contracts that are new (no existing storage snapshot)
for CONTRACT in "$CHANGED_CONTRACTS"; do
echo ${CONTRACT} | xargs basename -a | cut -d'.' -f1 | xargs -I{} echo src/dollar/core/{}.sol:{} >> contracts.txt
CONTRACT_NAME=$(echo ${CONTRACT} | xargs basename -a | cut -d'.' -f1)
CONTRACT_PATH="src/dollar/core/${CONTRACT_NAME}.sol"
SNAPSHOT_PATH="storage-layouts/${CONTRACT_NAME}.json"
if [ -f "$SNAPSHOT_PATH" ]; then
echo "Existing contract: ${CONTRACT_PATH}:${CONTRACT_NAME}"
echo "${CONTRACT_PATH}:${CONTRACT_NAME}" >> contracts.txt
else
echo "New contract (skipping storage check): ${CONTRACT_PATH}:${CONTRACT_NAME}"
fi
done
Comment on lines 38 to 49

@coderabbitai coderabbitai Bot May 22, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟠 Major | ⚡ Quick win

🧩 Analysis chain

🏁 Script executed:

#!/bin/bash
set -euo pipefail
FILE=.github/workflows/core-contracts-storage-check.yml

echo "Check loop form and changed-files output wiring:"
rg -n 'CHANGED_CONTRACTS|contracts_all_changed_files|for CONTRACT in "\$CHANGED_CONTRACTS"|while IFS= read -r CONTRACT' "$FILE"

Repository: ubiquity/ubiquity-dollar

Length of output: 270

🏁 Script executed:

#!/bin/bash
set -euo pipefail
FILE=.github/workflows/core-contracts-storage-check.yml

echo "=== Show loop block (lines 25-70) ==="
nl -ba "$FILE" | sed -n '25,75p'

echo
echo "=== Find the step id=changed-contracts and the output name ==="
rg -n "id:\s*changed-contracts|contracts_all_changed_files|outputs:" "$FILE"

echo
echo "=== Print the changed-contracts step content ==="
# crude extraction: from id changed-contracts to next id or end
START=$(rg -n "id:\s*changed-contracts" "$FILE" | cut -d: -f1 | head -n1)
if [ -n "${START:-}" ]; then
  # print next ~120 lines
  nl -ba "$FILE" | sed -n "${START},$((START+140))p"
fi

Repository: ubiquity/ubiquity-dollar

Length of output: 167

🏁 Script executed:

#!/bin/bash
set -euo pipefail
FILE=.github/workflows/core-contracts-storage-check.yml

echo "=== Show loop block (lines 25-70) ==="
nl -ba "$FILE" | sed -n '25,75p'

echo
echo "=== Find the step id=changed-contracts and the output name ==="
rg -n "id:\s*changed-contracts|contracts_all_changed_files|outputs:" "$FILE"

echo
echo "=== Print the changed-contracts step content ==="
START=$(rg -n "id:\s*changed-contracts" "$FILE" | cut -d: -f1 | head -n1)
if [ -n "${START:-}" ]; then
  nl -ba "$FILE" | sed -n "${START},$((START+140))p"
fi

Repository: ubiquity/ubiquity-dollar

Length of output: 167

🏁 Script executed:

#!/bin/bash
set -euo pipefail
FILE=.github/workflows/core-contracts-storage-check.yml

echo "=== Show lines 25-75 ==="
sed -n '25,75p' "$FILE"

echo
echo "=== Lines with changed-contracts id or contracts_all_changed_files ==="
rg -n "id:\s*changed-contracts|contracts_all_changed_files" "$FILE"

echo
echo "=== Show around changed-contracts step (from first occurrence to +140 lines) ==="
START=$(rg -n "id:\s*changed-contracts" "$FILE" | head -n1 | cut -d: -f1)
if [ -n "${START:-}" ]; then
  sed -n "${START},$((START+140))p" "$FILE"
fi

Repository: ubiquity/ubiquity-dollar

Length of output: 4455

Fix contract filtering loop to iterate over each entry in contracts_all_changed_files

  • The workflow sets CHANGED_CONTRACTS from steps.changed-contracts.outputs.contracts_all_changed_files, but the script uses for CONTRACT in "$CHANGED_CONTRACTS"; do, so bash treats the whole value as one item (multi-contract changes can generate an incorrect contracts.txt/matrix).
Suggested fix 
-          for CONTRACT in "$CHANGED_CONTRACTS"; do
-            CONTRACT_NAME=$(echo ${CONTRACT} | xargs basename -a | cut -d'.' -f1)
+          while IFS= read -r CONTRACT; do
+            [ -z "$CONTRACT" ] && continue
+            CONTRACT_NAME="$(basename "$CONTRACT" .sol)"
             CONTRACT_PATH="src/dollar/core/${CONTRACT_NAME}.sol"
             SNAPSHOT_PATH="storage-layouts/${CONTRACT_NAME}.json"
             
             if [ -f "$SNAPSHOT_PATH" ]; then
               echo "Existing contract: ${CONTRACT_PATH}:${CONTRACT_NAME}"
               echo "${CONTRACT_PATH}:${CONTRACT_NAME}" >> contracts.txt
             else
               echo "New contract (skipping storage check): ${CONTRACT_PATH}:${CONTRACT_NAME}"
             fi
-          done
+          done <<< "$CHANGED_CONTRACTS"
📝 Committable suggestion

‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.

Suggested change
for CONTRACT in "$CHANGED_CONTRACTS"; do
echo ${CONTRACT} | xargs basename -a | cut -d'.' -f1 | xargs -I{} echo src/dollar/core/{}.sol:{} >> contracts.txt
CONTRACT_NAME=$(echo ${CONTRACT} | xargs basename -a | cut -d'.' -f1)
CONTRACT_PATH="src/dollar/core/${CONTRACT_NAME}.sol"
SNAPSHOT_PATH="storage-layouts/${CONTRACT_NAME}.json"
if [ -f "$SNAPSHOT_PATH" ]; then
echo "Existing contract: ${CONTRACT_PATH}:${CONTRACT_NAME}"
echo "${CONTRACT_PATH}:${CONTRACT_NAME}" >> contracts.txt
else
echo "New contract (skipping storage check): ${CONTRACT_PATH}:${CONTRACT_NAME}"
fi
done
while IFS= read -r CONTRACT; do
[ -z "$CONTRACT" ] && continue
CONTRACT_NAME="$(basename "$CONTRACT" .sol)"
CONTRACT_PATH="src/dollar/core/${CONTRACT_NAME}.sol"
SNAPSHOT_PATH="storage-layouts/${CONTRACT_NAME}.json"
if [ -f "$SNAPSHOT_PATH" ]; then
echo "Existing contract: ${CONTRACT_PATH}:${CONTRACT_NAME}"
echo "${CONTRACT_PATH}:${CONTRACT_NAME}" >> contracts.txt
else
echo "New contract (skipping storage check): ${CONTRACT_PATH}:${CONTRACT_NAME}"
fi
done <<< "$CHANGED_CONTRACTS"

echo "matrix=$(cat contracts.txt | jq -R -s -c 'split("\n")[:-1]')" >> $GITHUB_OUTPUT
if [ -f contracts.txt ]; then
echo "matrix=$(cat contracts.txt | jq -R -s -c 'split(\"\n\")[:-1]')" >> $GITHUB_OUTPUT
else
echo "matrix=[]" >> $GITHUB_OUTPUT
fi
outputs:
matrix: ${{ steps.set-matrix.outputs.matrix }}
Expand All @@ -54,14 +70,14 @@ jobs:
- uses: actions/checkout@v3
with:
submodules: recursive
persist-credentials: false

- name: Install Foundry
uses: foundry-rs/foundry-toolchain@v1

- name: Check For Core Contracts Storage Changes
uses: Rubilmax/foundry-storage-check@main
with:
workingDirectory: packages/contracts
contract: ${{ matrix.contract }}
failOnRemoval: true

failOnRemoval: true
25 changes: 21 additions & 4 deletions .github/workflows/diamond-storage-check.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ jobs:
- uses: actions/checkout@v3
with:
submodules: recursive
persist-credentials: false

- name: Install Foundry
uses: foundry-rs/foundry-toolchain@v1
Expand All @@ -37,10 +38,25 @@ jobs:
env:
CHANGED_LIBS: ${{ steps.changed-libraries.outputs.libraries_all_changed_files }}
run: |
# Filter out libraries that are new (no existing storage snapshot)
for DIAMOND_LIB in "$CHANGED_LIBS"; do
echo ${DIAMOND_LIB} | xargs basename -a | cut -d'.' -f1 | xargs -I{} echo src/dollar/libraries/{}.sol:{} >> contracts.txt
LIB_NAME=$(echo ${DIAMOND_LIB} | xargs basename -a | cut -d'.' -f1)
LIB_PATH="src/dollar/libraries/${LIB_NAME}.sol"
SNAPSHOT_PATH="storage-layouts/${LIB_NAME}.json"

if [ -f "$SNAPSHOT_PATH" ]; then
echo "Existing library: ${LIB_PATH}:${LIB_NAME}"
echo "${LIB_PATH}:${LIB_NAME}" >> contracts.txt
else
echo "New library (skipping storage check): ${LIB_PATH}:${LIB_NAME}"
fi
done
Comment on lines 42 to 53

@coderabbitai coderabbitai Bot May 22, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟠 Major | ⚡ Quick win

🧩 Analysis chain

🏁 Script executed:

#!/bin/bash
set -euo pipefail
FILE=.github/workflows/diamond-storage-check.yml

echo "Check loop form and changed-files output wiring:"
rg -n 'CHANGED_LIBS|libraries_all_changed_files|for DIAMOND_LIB in "\$CHANGED_LIBS"|while IFS= read -r DIAMOND_LIB' "$FILE"

Repository: ubiquity/ubiquity-dollar

Length of output: 263

🏁 Script executed:

#!/bin/bash
set -euo pipefail

FILE=.github/workflows/diamond-storage-check.yml
echo "== Lines 1-120 =="
nl -ba "$FILE" | sed -n '1,120p'

echo
echo "== Locate changed-libraries step =="
rg -n 'id:\s*changed-libraries|changed-libraries|libraries_all_changed_files' "$FILE"

Repository: ubiquity/ubiquity-dollar

Length of output: 147

🏁 Script executed:

#!/bin/bash
set -euo pipefail
FILE=.github/workflows/diamond-storage-check.yml

echo "== cat -n 1-160 =="
cat -n "$FILE" | sed -n '1,160p'

echo
echo "== Find step/outputs for changed-libraries =="
rg -n 'id:\s*changed-libraries|steps\.changed-libraries|libraries_all_changed_files|changed-libraries' "$FILE"

Repository: ubiquity/ubiquity-dollar

Length of output: 3673

🌐 Web query:

tj-actions/changed-files libraries_all_changed_files output delimiter format newline space

💡 Result:

In the tj-actions/changed-files GitHub Action, the output format for lists of changed files (such as all_changed_files) is controlled by the separator input [1][2]. The default delimiter for these outputs is a single space character (' ') [3][1]. You can customize this by providing a different string to the separator input in your workflow configuration [1][2]. For example, to output file paths separated by a newline, you would configure your step as follows [3][4]: - uses: tj-actions/changed-files@v45 with: separator: ' ' Note that when using shell commands to process these outputs, using a space-based delimiter can sometimes lead to issues if filenames contain spaces. In such cases, configuring the separator to a newline or another character that does not appear in your filenames is recommended [3][4]. Finally, please be aware that historical versions of this action were subject to a supply chain compromise involving secret exfiltration [5][6][7]. It is recommended to ensure you are using a secure, verified version of the action [6].

Citations:

Fix CHANGED_LIBS iteration in diamond-storage-check.yml (space-delimited list)

CHANGED_LIBS comes from tj-actions/changed-files’ libraries_all_changed_files output, which defaults to a single space separator. With for DIAMOND_LIB in "$CHANGED_LIBS"; do, the whole space-delimited list becomes one loop token, leading to incorrect/merged library handling and a broken/incomplete matrix.

Use either: (1) don’t quote the loop expansion (for DIAMOND_LIB in $CHANGED_LIBS; do ...) or (2) set separator on the changed-libraries step to newline and then iterate line-by-line.

echo "matrix=$(cat contracts.txt | jq -R -s -c 'split("\n")[:-1]')" >> $GITHUB_OUTPUT

if [ -f contracts.txt ]; then
echo "matrix=$(cat contracts.txt | jq -R -s -c 'split(\"\n\")[:-1]')" >> $GITHUB_OUTPUT
else
echo "matrix=[]" >> $GITHUB_OUTPUT
fi

outputs:
matrix: ${{ steps.set-matrix.outputs.matrix }}
Expand All @@ -58,14 +74,15 @@ jobs:
- uses: actions/checkout@v3
with:
submodules: recursive
persist-credentials: false

- name: Install Foundry
uses: foundry-rs/foundry-toolchain@v1

- name: Check For Diamond Storage Changes
uses: ubiquity/foundry-storage-check@main
with:
workingDirectory: packages/contracts
contract: ${{ matrix.contract }}
failOnRemoval: true
failOnLabelDiff: true
failOnLabelDiff: true
68 changes: 68 additions & 0 deletions packages/contracts/test/certora/UbiquityPoolFacetHarness.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,68 @@
// SPDX-License-Identifier: MIT
pragma solidity 0.8.19;

import {UbiquityPoolFacet} from "../../../../src/dollar/facets/UbiquityPoolFacet.sol";
import {LibUbiquityPool} from "../../../../src/dollar/libraries/LibUbiquityPool.sol";
import {AppStorage, LibAppStorage} from "../../../../src/dollar/libraries/LibAppStorage.sol";

/**
* @notice Ubiquity pool facet harness for Certora formal verification
* @notice Exposes internal state and critical view functions for invariant checking
*/
contract UbiquityPoolFacetHarness is UbiquityPoolFacet {
/**
* @notice Exposes the reentrancy status for safety verification
* @return status 1 = entered, 2 = not entered
*/
Comment on lines +15 to +16

@coderabbitai coderabbitai Bot May 22, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Fix reentrancy status value mapping in docs.

Line 15 documents the status values opposite to what pool.spec assumes (not entered = 1). Please align the mapping to prevent inverted invariant assumptions.

function exposed_getReentrancyStatus() external view returns (uint256) {
AppStorage storage store = LibAppStorage.appStorage();
return store.reentrancyStatus;
}

/**
* @notice Exposes the collateral ratio for price-bound verification
* @return collateralRatio 1_000_000 = 100%
*/
function exposed_collateralRatio() external view returns (uint256) {
return LibUbiquityPool.collateralRatio();
}

/**
* @notice Exposes the total collateral USD balance
* @return balance Collateral balance in USD terms
*/
function exposed_collateralUsdBalance() external view returns (uint256) {
return LibUbiquityPool.collateralUsdBalance();
}

/**
* @notice Returns whether a collateral token is enabled
* @param collateralAddress The collateral token address
* @return isEnabled True if enabled
*/
function exposed_isCollateralEnabled(address collateralAddress) external view returns (bool) {
LibUbiquityPool.CollateralInformation memory info = LibUbiquityPool.collateralInformation(collateralAddress);
return info.isEnabled;
}

/**
* @notice Returns the collateral information for a given address
* @param collateralAddress The collateral token address
* @return returnData The collateral information struct
*/
function exposed_collateralInformation(address collateralAddress)
external
view
returns (LibUbiquityPool.CollateralInformation memory returnData)
{
return LibUbiquityPool.collateralInformation(collateralAddress);
}

/**
* @notice Returns all collateral addresses
* @return addresses Array of enabled collateral token addresses
*/
function exposed_allCollaterals() external view returns (address[] memory) {
return LibUbiquityPool.allCollaterals();
}
}
46 changes: 46 additions & 0 deletions packages/contracts/test/certora/pool.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
{
"files": [
"src/dollar/Diamond.sol",
"src/dollar/facets/AccessControlFacet.sol",
"src/dollar/facets/ManagerFacet.sol",
"src/dollar/facets/UbiquityPoolFacet.sol",
"src/dollar/libraries/LibUbiquityPool.sol",
"src/dollar/libraries/LibAppStorage.sol",
"src/dollar/core/UbiquityDollarToken.sol",
"src/dollar/core/UbiquityGovernanceToken.sol",
"test/certora/UbiquityPoolFacetHarness.sol",
"test/certora/StakingFacetHarness.sol"
],
"verify": "Diamond:test/certora/pool.spec",
"contract_extensions": {
"Diamond": [
{
"extension": "AccessControlFacet",
"exclude": []
},
{
"extension": "ManagerFacet",
"exclude": []
},
{
"extension": "UbiquityPoolFacet",
"exclude": []
},
{
"extension": "StakingFacetHarness",
"exclude": []
}
]
Comment on lines +16 to +33

@coderabbitai coderabbitai Bot May 22, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟠 Major | ⚡ Quick win

🧩 Analysis chain

🏁 Script executed:

#!/bin/bash
# Verify exposed_* functions are only in the harness and that pool.conf extension list includes it.
rg -n -C2 'function\s+exposed_' packages/contracts/test/certora/UbiquityPoolFacetHarness.sol
rg -n -C3 '"contract_extensions"|"extension"' packages/contracts/test/certora/pool.conf

Repository: ubiquity/ubiquity-dollar

Length of output: 2137

Mount UbiquityPoolFacetHarness in contract_extensions.Diamond (not UbiquityPoolFacet).

pool.spec calls exposed_* selectors, which are implemented in test/certora/UbiquityPoolFacetHarness.sol; however packages/contracts/test/certora/pool.conf currently lists "extension": "UbiquityPoolFacet" under contract_extensions.Diamond, so those exposed_* methods won’t be present on the configured Diamond.

Suggested config change 
             {
-                "extension": "UbiquityPoolFacet",
+                "extension": "UbiquityPoolFacetHarness",
                 "exclude": []
             },

},
"link": [
"UbiquityGovernanceToken:manager=UbiquityAlgorithmicDollarManager",
"UbiquityDollarToken:manager=UbiquityAlgorithmicDollarManager"
],
"parametric_contracts": [
"Diamond",
"UbiquityPoolFacet"
],
"optimistic_loop": true,
"rule_sanity": "basic",
"msg": "pool.conf"
}
Loading
Loading