feat: formal verification for UbiquityPoolFacet (#926)#1048
feat: formal verification for UbiquityPoolFacet (#926)#1048wbobbynmworley wants to merge 2 commits into
Conversation
Resolves ubiquity#972 Problem: When a new contract is added, the core-contracts-storage-check and diamond-storage-check workflows fail because there's no existing storage snapshot to compare against. Solution: In the provide_contracts job, check if each changed contract has an existing storage snapshot (storage-layouts/*.json). If not, it's a new contract and should be skipped. Changes: - Modified core-contracts-storage-check.yml to filter out new contracts - Modified diamond-storage-check.yml to filter out new libraries - Added persist-credentials: false to checkout steps for security QA: 1) No storage updates, CI passing 2) Storage update, no collision, CI passing 3) Storage update, collision, CI failing 4) New contract/library added, CI passing
Add formal verification harness, spec file, and config for LibUbiquityPool: - UbiquityPoolFacetHarness.sol: exposes internal state getters - pool.spec: 10 invariants covering: - No under-collateralization (dollar supply <= collateral value) - Sufficient collateral for all redemptions - Collateral ratio always positive - Reentrancy protection - Fee bounds - Pause state consistency - Mint maintains collateral ratio - Redeem reduces debt correctly - pool.conf: Certora Prover configuration Ref: ubiquity#926
📝 WalkthroughWalkthroughThis PR introduces Certora formal verification for UbiquityPool and enhances CI workflows. The Certora setup includes a test harness exposing internal functions, a configuration file targeting the Diamond contract with facet extensions, and a comprehensive specification with ten invariants covering collateral backing, redemption safety, reentrancy guards, and operation-specific constraints. Both storage-check workflows (core-contracts and diamond) now disable GitHub token persistence and filter the verification matrix to only include contracts with pre-existing storage snapshots. 🚥 Pre-merge checks | ✅ 3 | ❌ 2❌ Failed checks (2 warnings)
✅ Passed checks (3 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 9
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro
Run ID: 3a4afb96-4939-4060-9380-8c22dd2b5e2d
📒 Files selected for processing (5)
.github/workflows/core-contracts-storage-check.yml.github/workflows/diamond-storage-check.ymlpackages/contracts/test/certora/UbiquityPoolFacetHarness.solpackages/contracts/test/certora/pool.confpackages/contracts/test/certora/pool.spec
| 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 |
There was a problem hiding this comment.
🧩 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"
fiRepository: 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"
fiRepository: 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"
fiRepository: 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_CONTRACTSfromsteps.changed-contracts.outputs.contracts_all_changed_files, but the script usesfor CONTRACT in "$CHANGED_CONTRACTS"; do, so bash treats the whole value as one item (multi-contract changes can generate an incorrectcontracts.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.
| 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" |
| 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 |
There was a problem hiding this comment.
🧩 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:
- 1: https://github.com/tj-actions/changed-files/tree/v5
- 2: https://github.com/tj-actions/changed-files
- 3: https://github.com/tj-actions/changed-files/blob/846166ffa0b31738729d07fe422ddfc9a8ee65d2/action.yml
- 4: https://github.com/tj-actions/changed-files/blob/c07606463672e7c623bc2801b4002bd645aed1f2/action.yml
- 5: https://snyk.io/blog/reconstructing-tj-actions-changed-files-github-actions-compromise/
- 6: https://www.stepsecurity.io/blog/harden-runner-detection-tj-actions-changed-files-action-is-compromised
- 7: https://www.reddit.com/r/programming/comments/1jcfchv/popular_github_action_tjactionschangedfiles_has/
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.
| "Diamond": [ | ||
| { | ||
| "extension": "AccessControlFacet", | ||
| "exclude": [] | ||
| }, | ||
| { | ||
| "extension": "ManagerFacet", | ||
| "exclude": [] | ||
| }, | ||
| { | ||
| "extension": "UbiquityPoolFacet", | ||
| "exclude": [] | ||
| }, | ||
| { | ||
| "extension": "StakingFacetHarness", | ||
| "exclude": [] | ||
| } | ||
| ] |
There was a problem hiding this comment.
🧩 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.confRepository: 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": []
},| // Get current state | ||
| totalDollarSupply = dollarToken.totalSupply(); | ||
| collateralBalanceUsd = exposed_collateralUsdBalance(); | ||
| dollarPrice = getDollarPriceUsd(); | ||
| collateralRatio = exposed_collateralRatio(); | ||
|
|
||
| // If there are dollars minted and collateral exists, verify ratio is maintained | ||
| require totalDollarSupply > 0; | ||
| require collateralBalanceUsd > 0; | ||
| require isCollateralRatioSane(collateralRatio); | ||
|
|
||
| calldataarg args; | ||
| env e; | ||
|
|
||
| // Execute the method | ||
| f(e, args); | ||
|
|
||
| // After execution, re-read state | ||
| uint256 newTotalDollarSupply = dollarToken.totalSupply(); | ||
| uint256 newCollateralBalanceUsd = exposed_collateralUsdBalance(); | ||
|
|
||
| // The value of dollars in circulation should not exceed collateral value * ratio | ||
| // dollar_value = total_supply * price / 1e6 | ||
| // collateral_value = collateral_balance * ratio / RATIO_PRECISION | ||
| // invariant: dollar_value <= collateral_value | ||
| mathint dollarValue = newTotalDollarSupply * dollarPrice / 1000000; | ||
| mathint maxAllowedDebt = newCollateralBalanceUsd * collateralRatio / RATIO_PRECISION; | ||
|
|
||
| assert dollarValue <= maxAllowedDebt, | ||
| "CRITICAL: Dollars minted exceed collateral backing"; |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Locate the exact file and print the relevant section with line numbers
ls -la packages/contracts/test/certora/pool.spec
sed -n '1,140p' packages/contracts/test/certora/pool.spec | cat -n
# Also extract any nearby definitions that may affect the meaning of the snippet
# (expand search a bit around the section)
rg -n "exposed_collateralUsdBalance|getDollarPriceUsd|exposed_collateralRatio|isCollateralRatioSane|calldataarg args|env e|\\bf\\(e, args\\)" packages/contracts/test/certora/pool.spec
# Print further context around the solvency check to ensure no other gating/invariant exists
sed -n '140,260p' packages/contracts/test/certora/pool.spec | cat -n || trueRepository: ubiquity/ubiquity-dollar
Length of output: 12157
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Show where these are defined/used in the spec directory
rg -n "function\s+getDollarPriceUsd|definition\s+getDollarPriceUsd|getDollarPriceUsd\s*\(" packages/contracts/test/certora -S
rg -n "exposed_collateralRatio\s*\(" packages/contracts/test/certora -S
rg -n "exposed_collateralUsdBalance\s*\(" packages/contracts/test/certora -S
# Also search the broader repo in case these helpers are defined elsewhere
rg -n "getDollarPriceUsd\s*\(" -S . --hidden --glob '!**/node_modules/**'
rg -n "exposed_collateralRatio\s*\(" -S . --hidden --glob '!**/node_modules/**'Repository: ubiquity/ubiquity-dollar
Length of output: 4607
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Show the harness getters used by the certora spec
sed -n '1,120p' packages/contracts/test/certora/UbiquityPoolFacetHarness.sol | cat -n
# Show getDollarPriceUsd implementation and collateral ratio/base functions it relies on
sed -n '340,460p' packages/contracts/src/dollar/libraries/LibUbiquityPool.sol | cat -n
sed -n '520,740p' packages/contracts/src/dollar/libraries/LibUbiquityPool.sol | cat -n
# Also check the facet wrapper for getDollarPriceUsd
sed -n '1,130p' packages/contracts/src/dollar/facets/UbiquityPoolFacet.sol | cat -nRepository: ubiquity/ubiquity-dollar
Length of output: 23413
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Pull the definitions of collateralRatio() and collateralUsdBalance() from LibUbiquityPool.sol
rg -n "function\s+collateralRatio\s*\(|function\s+collateralUsdBalance\s*\(" packages/contracts/src/dollar/libraries/LibUbiquityPool.sol
# Print the surrounding implementations (small slices around the matches)
python3 - <<'PY'
import re, pathlib
path = pathlib.Path("packages/contracts/src/dollar/libraries/LibUbiquityPool.sol")
text = path.read_text().splitlines()
matches = []
for i,line in enumerate(text,1):
if re.search(r"function\s+collateralRatio\s*\(", line):
matches.append(i)
if re.search(r"function\s+collateralUsdBalance\s*\(", line):
matches.append(i)
print("matches:", matches)
PY
# Use sed windows around likely line numbers: print 200 lines around each match
# (Compute approximate line numbers by re-running rg with --context would be nicer, but keep output small)
rg -n "function\s+collateralRatio\s*\(" -n packages/contracts/src/dollar/libraries/LibUbiquityPool.sol
rg -n "function\s+collateralUsdBalance\s*\(" -n packages/contracts/src/dollar/libraries/LibUbiquityPool.sol
# We'll print broad but bounded ranges to capture both functions.
sed -n '300,430p' packages/contracts/src/dollar/libraries/LibUbiquityPool.sol | cat -n
sed -n '430,580p' packages/contracts/src/dollar/libraries/LibUbiquityPool.sol | cat -nRepository: ubiquity/ubiquity-dollar
Length of output: 12595
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Find any writes/assignments to collateralRatio in the contracts source
rg -n "collateralRatio\s*=" packages/contracts/src -S
rg -n "\.collateralRatio\s*[\+\-\*\/%]?=" packages/contracts/src -S
rg -n "collateralRatio\s*\(" packages/contracts/src/dollar -S
# Also check for any function named like "setCollateralRatio" or "updateCollateralRatio"
rg -n "setCollateralRatio|updateCollateralRatio|CollateralRatio" packages/contracts/src -S
# Find any writes to collateralPrices[] or unclaimedPoolCollateral that affect collateralUsdBalance
rg -n "collateralPrices\s*\[" packages/contracts/src -S
rg -n "unclaimedPoolCollateral\s*\[" packages/contracts/src -S
rg -n "missingDecimals\s*\[" packages/contracts/src -SRepository: ubiquity/ubiquity-dollar
Length of output: 465
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Re-run the searches with simpler patterns
rg -n "collateralRatio\s*=" packages/contracts/src/dollar -S
rg -n "newCollateralRatio" packages/contracts/src/dollar -S
# Show the exact function around the assignment
sed -n '1020,1120p' packages/contracts/src/dollar/libraries/LibUbiquityPool.sol | cat -n
# Also find any access-control or update function names near there
rg -n "function\s+.*collateralRatio|update.*collateralRatio|set.*collateralRatio" packages/contracts/src/dollar/libraries/LibUbiquityPool.sol -S
# And scan for any other collateralRatio writes outside that file
rg -n "collateralRatio\s*=" packages/contracts/src/dollar -SRepository: ubiquity/ubiquity-dollar
Length of output: 6338
Fix inv_noUnderCollateralization to use post-state price/ratio and avoid vacuous preconditions.
inv_noUnderCollateralizationreadsdollarPrice = getDollarPriceUsd()andcollateralRatio = exposed_collateralRatio()beforef(e, args)(lines 71-73) but uses them in the post-state solvency assertion withnewTotalDollarSupply/newCollateralBalanceUsd(lines 94-95); recomputedollarPrice/collateralRatioafterf, since the price feed inputs are modeled as nondeterministic andcollateralRatiois mutable viasetCollateralRatio.- The pre-gating
require totalDollarSupply > 0;andrequire collateralBalanceUsd > 0;(lines 76-78) can skip the invariant exactly in the “first mint / from-empty collateral” transition where an under-collateralization would be most dangerous; remove/relax these preconditions so the solvency check always runs on the post-state.
| rule inv_stalePriceHandledGracefully(method f) { | ||
| env e; | ||
|
|
||
| // If price feeds return stale data, operations should still be safe | ||
| calldataarg args; | ||
| f(e, args); | ||
|
|
||
| // After any operation, collateral balance should be non-negative | ||
| uint256 collateralUsd = exposed_collateralUsdBalance(); | ||
|
|
||
| assert collateralUsd >= 0, | ||
| "Collateral balance went negative"; | ||
| } |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
file="packages/contracts/test/certora/pool.spec"
echo "== file: $file =="
# show around the reported lines
nl -ba "$file" | sed -n '160,240p'Repository: ubiquity/ubiquity-dollar
Length of output: 183
🏁 Script executed:
#!/bin/bash
set -euo pipefail
file="packages/contracts/test/certora/pool.spec"
echo "== file: $file =="
# Prefer cat -n for line numbers
if command -v cat >/dev/null 2>&1; then
cat -n "$file" | sed -n '160,240p'
else
echo "cat not available"
fiRepository: ubiquity/ubiquity-dollar
Length of output: 3089
inv_stalePriceHandledGracefully is tautological and doesn’t test stale-price safety.
In packages/contracts/test/certora/pool.spec (193–205), collateralUsd is a uint256, so assert collateralUsd >= 0 can never fail. As written, the rule provides no validation that stale price feeds are handled safely.
| rule inv_enabledCollateralAlwaysPriced(method f) { | ||
| env e; | ||
| calldataarg args; | ||
| f(e, args); | ||
|
|
||
| // Check each enabled collateral has a valid price | ||
| address[] collaterals = exposed_allCollaterals(); | ||
|
|
||
| // For each enabled collateral, price should always be > 0 | ||
| // (This requires checking each one individually which Certora handles via loop) | ||
| } | ||
|
|
||
| //======== | ||
| // Invariant 7: Fee bounds | ||
| // | ||
| // Minting and redemption fees must always be within acceptable bounds (0-100%) | ||
| //======== | ||
|
|
||
| rule inv_feesAlwaysWithinBounds(method f) { | ||
| address[] collaterals = exposed_allCollaterals(); | ||
|
|
||
| env e; | ||
| calldataarg args; | ||
| f(e, args); | ||
|
|
||
| // After any operation, check that all collateral fees are within bounds | ||
| // 0 <= fee <= 1_000_000 (where 1_000_000 = 100%) | ||
| // This is verified by checking collateralInformation for each collateral | ||
| } | ||
|
|
||
| //======== | ||
| // Invariant 8: Pause state consistency | ||
| // | ||
| // Pausing the contract should properly suspend all minting and redemption | ||
| //======== | ||
|
|
||
| rule inv_pauseStateConsistency(method f) { | ||
| env e; | ||
|
|
||
| // Check pause-related invariants | ||
| calldataarg args; | ||
| f(e, args); | ||
|
|
||
| // After any operation, we should be able to read pause state | ||
| // without revert (pause getter doesn't revert) | ||
| } |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
FILE="packages/contracts/test/certora/pool.spec"
echo "== File exists? =="
ls -l "$FILE"
echo "== Lines 180-290 =="
nl -ba "$FILE" | sed -n '180,290p'Repository: ubiquity/ubiquity-dollar
Length of output: 260
🏁 Script executed:
#!/bin/bash
set -euo pipefail
FILE="packages/contracts/test/certora/pool.spec"
echo "== File exists? =="
ls -l "$FILE"
echo "== Lines 180-290 =="
nl -ba "$FILE" | sed -n '180,290p'Repository: ubiquity/ubiquity-dollar
Length of output: 260
🏁 Script executed:
#!/bin/bash
set -euo pipefail
FILE="packages/contracts/test/certora/pool.spec"
echo "== Snippet $FILE lines 205-275 =="
awk 'NR>=205 && NR<=275 {printf "%d:%s\n", NR, $0}' "$FILE"
echo
echo "== Find rule declarations =="
rg -n "rule inv_(enabledCollateralAlwaysPriced|feesAlwaysWithinBounds|pauseStateConsistency)\b" "$FILE" || true
echo
echo "== Print full rule bodies (best-effort) =="
# Print from each rule line until the next "rule " line.
for name in inv_enabledCollateralAlwaysPriced inv_feesAlwaysWithinBounds inv_pauseStateConsistency; do
echo "--- $name ---"
start=$(rg -n "rule $name\\b" "$FILE" | head -n1 | cut -d: -f1)
if [[ -z "${start:-}" ]]; then
echo "not found"
continue
fi
awk -v s="$start" '
NR>=s {
if (NR>s && $0 ~ /^rule /) { exit }
print
}
' "$FILE"
doneRepository: ubiquity/ubiquity-dollar
Length of output: 4125
🏁 Script executed:
#!/bin/bash
set -euo pipefail
FILE="packages/contracts/test/certora/pool.spec"
# show any assert-like tokens within each rule region (lightweight checks)
for start in 213 231 249; do
awk -v s="$start" '
NR>=s {
if (NR>s && $0 ~ /^rule /) exit
print
}
' "$FILE" | rg -n "assert|check|invariant|require\b|guarantee|ensures|forall|exists" || true
doneRepository: ubiquity/ubiquity-dollar
Length of output: 356
Fix Certora invariants: these rules currently don’t assert anything
- In
packages/contracts/test/certora/pool.spec(lines 213-258),inv_enabledCollateralAlwaysPriced,inv_feesAlwaysWithinBounds, andinv_pauseStateConsistencyonly callf(e, args)and read helper state—there are no Certoraassert/check/guarantee-style properties—so they provide no formal guarantees.
| // If total supply increased (minting occurred), verify collateral still covers it | ||
| require totalSupplyAfter >= totalSupplyBefore; | ||
| require collateralAfter >= collateralBefore; | ||
| require ratioAfter >= ratioBefore; // ratio should not decrease | ||
|
|
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
FILE="packages/contracts/test/certora/pool.spec"
echo "== Lines around 260-320 =="
nl -ba "$FILE" | sed -n '250,330p'
echo
echo "== Search for minting / mint occurrences in this spec =="
rg -n "mint|minting|totalSupplyAfter|collateralAfter|ratioAfter|collateralBefore|ratioBefore|totalSupplyBefore" "$FILE"Repository: ubiquity/ubiquity-dollar
Length of output: 156
🏁 Script executed:
#!/bin/bash
set -euo pipefail
FILE="packages/contracts/test/certora/pool.spec"
echo "== Lines 250-330 (with line numbers) =="
python3 - <<'PY'
import itertools
path = "packages/contracts/test/certora/pool.spec"
start, end = 250, 330
with open(path, "r", encoding="utf-8") as f:
for i, line in enumerate(f, start=1):
if start <= i <= end:
print(f"{i:4d}\t{line.rstrip()}")
elif i > end:
break
PY
echo
echo "== Search for minting / mint occurrences in this spec =="
rg -n "mint|minting" "$FILE" || true
echo
echo "== Search for key variables around the snippet =="
rg -n "totalSupplyAfter|totalSupplyBefore|collateralAfter|collateralBefore|ratioAfter|ratioBefore" "$FILE" || trueRepository: ubiquity/ubiquity-dollar
Length of output: 4671
🌐 Web query:
Certora Prover rule semantics require vs assert failing require skips execution treated as precondition
💡 Result:
In the Certora Prover, require and assert statements serve distinct roles in defining and verifying rules [1]. Require statements act as preconditions [2][1]. If a require statement evaluates to false for a specific execution trace, that entire trace is ignored and excluded from consideration by the Prover [3][1]. Consequently, execution does not "fail" or trigger a violation in the presence of a failing require; rather, the Prover simply filters out those cases and proceeds to evaluate remaining paths [3][1]. Assert statements define the expected behavior of the contract [2][1]. If an assert statement evaluates to false on any execution path that satisfies all preceding require statements, the Prover reports a violation and provides a counterexample [3][1]. The behavior where failing requirements are treated as preconditions that prune the search space is intentional [3][1]. This allows users to restrict verification to relevant, feasible, or intended scenarios [4][1]. However, this mechanism introduces the risk of vacuity, where a rule may pass simply because all execution paths were filtered out by overly aggressive require statements [5][6]. To mitigate this, the Certora Prover includes tools to detect such cases, such as vacuity checks (e.g., automatically appending assert false to rules to ensure they are reachable) [5].
Citations:
- 1: https://docs.certora.com/en/latest/docs/cvl/statements.html
- 2: https://rareskills.io/post/certora-specification
- 3: https://docs.certora.com/en/latest/docs/cvl/rules.html
- 4: https://docs.certora.com/projects/tutorials/en/latest/lesson2_started/preconditions.html
- 5: https://docs.certora.com/en/latest/docs/user-guide/checking.html
- 6: https://docs.certora.com/en/latest/docs/user-guide/glossary.html
Fix vacuity in inv_mintMaintainsCollateralRatio by removing mint-time monotonicity requires
require failures are treated as preconditions that prune traces; in packages/contracts/test/certora/pool.spec lines 286-288, if a mint operation decreases collateralAfter or ratioAfter, the rule is excluded before reaching assert debtAfter <= backingAfter, hiding the violation. Gate on actual mint occurrence (e.g., totalSupplyAfter > totalSupplyBefore) and then assert backing safety unconditionally for those traces.
| rule inv_redeemReducesDebtCorrectly(method f) { | ||
| env e; | ||
|
|
||
| uint256 totalSupplyBefore = dollarToken.totalSupply(); | ||
|
|
||
| calldataarg args; | ||
| f(e, args); | ||
|
|
||
| uint256 totalSupplyAfter = dollarToken.totalSupply(); | ||
|
|
||
| // After redeem operations, total supply should not increase | ||
| // (redeeming burns dollars, doesn't mint) | ||
| assert totalSupplyAfter <= totalSupplyBefore, | ||
| "Dollar supply increased during what should be a burn operation"; |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Locate the certora spec and show the relevant rule plus surrounding context
FILE="packages/contracts/test/certora/pool.spec"
if [ ! -f "$FILE" ]; then
echo "Missing file: $FILE" >&2
exit 1
fi
# Show around the asserted lines
python3 - <<'PY'
import itertools
path="packages/contracts/test/certora/pool.spec"
start=270
end=360
with open(path,'r',encoding='utf-8') as f:
for i,line in enumerate(f,1):
if start<=i<=end:
print(f"{i:4d}: {line.rstrip()}")
PY
# Also search for the rule name and any other inv_redeem... rules
rg -n "inv_redeemReducesDebtCorrectly|redeemReducesDebtCorrectly" "$FILE" || true
# Search within certora specs for any filter/helper macros like "redeem" method predicates
rg -n "redeem|mint|burn|Dollar|dollarToken" "$FILE" | head -n 80
# Search for other rules using "method f" / calldataarg patterns to see how they filter methods
rg -n "rule .*method f" "$FILE" || trueRepository: ubiquity/ubiquity-dollar
Length of output: 5017
🏁 Script executed:
#!/bin/bash
set -euo pipefail
FILE="packages/contracts/test/certora/pool.spec"
# Header/context (includes DISPATCHER and any method set definitions)
python3 - <<'PY'
path="packages/contracts/test/certora/pool.spec"
with open(path,'r',encoding='utf-8') as f:
for i,line in enumerate(f,1):
if i<=120:
print(f"{i:4d}: {line.rstrip()}")
else:
break
PY
echo "---- filtered blocks ----"
rg -n "filtered\s*\{[^\}]*\}" "$FILE" || true
echo "---- any redeem-specific predicates ----"
rg -n "redeem|burn|mint" "$FILE" | head -n 200Repository: ubiquity/ubiquity-dollar
Length of output: 6742
Restrict inv_redeemReducesDebtCorrectly to redeem/burn methods.
inv_redeemReducesDebtCorrectly(method f) runs f(e, args) over the whole methods { ... } set (which includes mint), yet it asserts dollarToken.totalSupply() never increases—this can fail on mint paths. Add a filtered { ... }/method-set restriction so the rule only applies to the redeem/burn entrypoints.
| * @return status 1 = entered, 2 = not entered | ||
| */ |
There was a problem hiding this comment.
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.
1 participant
Summary
Implements formal verification for LibUbiquityPool as requested in #926.
Files Added
est/certora/UbiquityPoolFacetHarness.sol
A harness contract that exposes internal state for Certora analysis:
est/certora/pool.spec
10 formal verification invariants:
est/certora/pool.conf
Certora Prover configuration for UbiquityPoolFacet.
Invariants Map to Issue Requirements
CI Note
Formal verification tests are NOT included in the standard CI pipeline. Per the issue requirements:
A separate workflow should be added to run Certora on merges to development with a 6-hour timeout.
References