Feat: certora prover#1734
Draft
tamtamchik wants to merge 34 commits intodevelopfrom
Draft
Conversation
Lido V3 (3.0.1)
fix: fix timeout on vaultHub.conf pendingHasNoShares
Certora Formal Verification: Staking Vaults
|
Hardhat Unit Tests Coverage SummaryDetailsDiff against masterResults for commit: f976cf3 Minimum allowed coverage is ♻️ This comment has been updated with latest results |
tamtamchik
force-pushed
the
feat/certora-prover
branch
from
d4d526f to
f976cf3
Compare
Contributor
There was a problem hiding this comment.
Pull request overview
Adds a Certora Prover verification suite and CI integration for the VaultHub/VaultFactory/Lido components, plus several Solidity harnesses/mocks to support invariant/fuzz and formal verification runs.
Changes:
- Introduces Certora specs/summaries, harnesses, mocks, and configuration files for verifying key protocol properties.
- Adds GitHub Actions workflows for running Certora CI and Foundry fuzz/invariant tests on PRs.
- Adds test-only Solidity harness/wrapper contracts for VaultFactory/LazyOracle/Dashboard used by the verification setup.
Reviewed changes
Copilot reviewed 126 out of 126 changed files in this pull request and generated 7 comments.
Show a summary per file
| File | Description |
|---|---|
| test/0.8.25/vaults/vaulthub/contracts/VaultFactory__HarnessForVaultHub.sol | Test harness to augment VaultFactory vault registration checks. |
| test/0.8.25/vaults/vaulthub/contracts/VaultFactoryWrapper.sol | IVaultFactory wrapper to intercept deployedVaults in tests. |
| test/0.8.25/vaults/vaulthub/contracts/MinimalDashboard.sol | Minimal Dashboard stub to satisfy VaultFactory construction/flows in tests. |
| test/0.8.25/vaults/vaulthub/contracts/LazyOracle__HarnessForVaultHub.sol | LazyOracle harness to control/report timestamps in tests. |
| certora/specs/vaults/vaults-array.spec | VaultHub vaults array set/indexing invariants and helpers. |
| certora/specs/vaults/shortfall.spec | Shortfall-related spec scaffolding and method summaries. |
| certora/specs/vaults/predeposit.spec | PredepositGuarantee validator-status transition rules and summaries. |
| certora/specs/vaults/lido-mock.spec | CVL summaries/ghosts for an ILidoMock model. |
| certora/specs/vaults/VaultHub_health.spec | Vault health-related rules plus withdrawable-value summary equivalence check. |
| certora/specs/setup/snippet_withdrawals.spec | Snippet summarizing withdrawal-request related calls. |
| certora/specs/setup/snippet_proof.spec | Snippet summarizing CLProofVerifier calls via wildcard. |
| certora/specs/setup/snippet_memutils.spec | Snippet summarizing memory utils behavior for verification. |
| certora/specs/setup/snippet_lidomock.spec | Snippet summarizing ILidoMock ERC20/share conversion calls. |
| certora/specs/setup/snippet_beacon.spec | Snippet summarizing IBeacon implementation selection as constant. |
| certora/specs/setup/snippet_StakingVault.spec | Snippet dispatching key StakingVault calls for verification. |
| certora/specs/setup/snippet_IHashConsensusMock.spec | Snippet summarizing IHashConsensusMock methods as NONDET. |
| certora/specs/setup/sanity_VaultHub.spec | Sanity spec wrapper for VaultHub dispatching setup. |
| certora/specs/setup/sanity_VaultFactory.spec | Sanity spec wrapper for VaultFactory dispatching setup. |
| certora/specs/setup/sanity_StakingVault.spec | Sanity spec wrapper for StakingVault dispatching setup. |
| certora/specs/setup/sanity_PredepositGuarantee.spec | Sanity spec wrapper for PredepositGuarantee dispatching setup. |
| certora/specs/setup/sanity_OperatorGrid.spec | Sanity spec wrapper for OperatorGrid dispatching setup. |
| certora/specs/setup/sanity_LazyOracle.spec | Sanity spec wrapper for LazyOracle dispatching setup. |
| certora/specs/setup/sanity_Dashboard.spec | Sanity spec wrapper for Dashboard dispatching setup. |
| certora/specs/setup/dispatching_VaultHub.spec | Dispatching/spec composition for VaultHub setup. |
| certora/specs/setup/dispatching_VaultFactory.spec | Dispatching/spec composition for VaultFactory setup. |
| certora/specs/setup/dispatching_StakingVault.spec | Dispatching/spec composition for StakingVault setup. |
| certora/specs/setup/dispatching_PredepositGuarantee.spec | Dispatching/spec composition for PredepositGuarantee setup. |
| certora/specs/setup/dispatching_OperatorGrid.spec | Dispatching/spec composition for OperatorGrid setup. |
| certora/specs/setup/dispatching_LazyOracle.spec | Dispatching/spec composition for LazyOracle setup. |
| certora/specs/setup/dispatching_Dashboard.spec | Dispatching/spec composition for Dashboard setup. |
| certora/specs/misc/node_operators.spec | NodeOperatorsRegistry monotonicity rule/spec. |
| certora/specs/misc/burner.spec | Burner invariants/rules around allowances and share burning behavior. |
| certora/specs/core/Lido_and_VaultHub.spec | Joint Lido/VaultHub properties with ghosts and hooks. |
| certora/specs/core/Accounting-summarized.spec | Accounting spec variant summarizing smoothenTokenRebase. |
| certora/specs/core/Accounting-fees-as-frac.spec | Rule checking fee shares approximate designated fraction of rewards. |
| certora/specs/core/Accounting-burnlimit.spec | Spec checking shares-to-burn limiter correctness (PositiveTokenRebaseLimiter). |
| certora/specs/common/lido-summaries.spec | Common CVL summaries for Lido share conversion functions and getters. |
| certora/specs/common/lido-storage-ghost.spec | Ghost-based modeling of key Lido storage slots/setters/getters. |
| certora/specs/common/erc20-summary.spec | Generic ERC20 behavioral summary layer for specs. |
| certora/specs/common/WithdrawalQueue-summary.spec | Common WithdrawalQueue summaries (e.g., prefinalize). |
| certora/specs/common/StakingRouter-summary.spec | Common StakingRouter summaries with constrained constants/ghosts. |
| certora/specs/common/ERC20Storage.spec | ERC20 ghost storage definitions and basic constraints. |
| certora/specs/common/ERC20Standard.spec | Standardized ERC20 transfer/allowance semantics atop ERC20 ghosts. |
| certora/specs/common/ERC20Params.spec | Shared ERC20 parameter definitions (MAX_SUPPLY, NATIVE, precisions). |
| certora/scripts/patch.sh | Helper script to apply Certora-required source patches. |
| certora/scripts/patch-undo.sh | Helper script to revert Certora-required source patches. |
| certora/patches/patch-total-shares-access.patch | Patch to expose and route _setTotalShares for Certora analysis. |
| certora/patches/patch-strategy-lib.patch | Patch to adjust allocation strategy function visibility for verification. |
| certora/patches/Makefile | Convenience Makefile for applying/unapplying all patch files. |
| certora/mocks/WithdrawalQueueMock.sol | Minimal WithdrawalQueueBase subclass used in verification configs. |
| certora/mocks/WithdrawableRequestMock.sol | Mock contract for withdrawal request calls (fallback). |
| certora/mocks/StorageExtensionVaultHub.sol | Storage extension harness for VaultHub storage linking. |
| certora/mocks/StorageExtensionStakingVault.sol | Storage extension harness for StakingVault storage linking. |
| certora/mocks/StorageExtensionPredepositGuarantee.sol | Storage extension harness for PredepositGuarantee storage linking. |
| certora/mocks/StorageExtensionOperatorGrid.sol | Storage extension harness for OperatorGrid storage linking. |
| certora/mocks/StorageExtensionNodeOperatorsRegistry.sol | Storage extension harness for NodeOperatorsRegistry linking. |
| certora/mocks/StorageExtensionLazyOracle.sol | Storage extension harness for LazyOracle storage linking. |
| certora/mocks/StorageExtension.sol | Combined storage extension harness holding multiple storage layouts. |
| certora/mocks/PayableMock.sol | Simple payable fallback mock used in configs. |
| certora/mocks/OldBurnerMock.sol | Burner wrapper mock used in older verification setups. |
| certora/mocks/ILidoMock.sol | Solidity mock implementing ILido used by verification configs. |
| certora/mocks/IHashConsensusMock.sol | Solidity mock implementing IHashConsensus used by configs. |
| certora/mocks/IDepositContractMock.sol | Solidity mock implementing IDepositContract used by configs. |
| certora/mocks/ERC721RecipientMock.sol | ERC721 receiver mock used for Dashboard-related verification. |
| certora/harness/VaultHubHarness.sol | VaultHub harness exposing internal state for CVL access. |
| certora/harness/NativeTransferFuncs.sol | Harness for native transfer flows (EL rewards/withdrawals). |
| certora/harness/LidoHarness.sol | Lido harness exposing additional view helpers for specs. |
| certora/harness/LazyOracleHarness.sol | LazyOracle harness exposing sanity-check path for specs. |
| certora/harness/BurnerHarness.sol | Burner harness exposing excess-share getter. |
| certora/harness/AccountingHarness.sol | Accounting harness exposing protocol-fee share calculation. |
| certora/confs/vaults/shortfall.conf | Certora config intended to run the shortfall spec. |
| certora/confs/vaults/predeposit.conf | Certora config for PredepositGuarantee spec. |
| certora/confs/vaults/lazy-oracle.conf | Certora config for LazyOracleHarness spec. |
| certora/confs/vaults/immutable-ratio.conf | Certora config for immutable ratio-related VaultHub rules. |
| certora/confs/vaults/approximated-VaultHub.conf | Certora config for approximated conversion VaultHub spec. |
| certora/confs/vaults/VaultHub_health_part6.conf | Split config for VaultHub health rule coverage (part 6). |
| certora/confs/vaults/VaultHub_health_part5.conf | Split config for VaultHub health rule coverage (part 5). |
| certora/confs/vaults/VaultHub_health_part4.conf | Split config for VaultHub health rule coverage (part 4). |
| certora/confs/vaults/VaultHub_health_part3.conf | Split config for VaultHub health rule coverage (part 3). |
| certora/confs/vaults/VaultHub_health_part2.conf | Split config for VaultHub health rule coverage (part 2). |
| certora/confs/vaults/VaultHub_health_part1.conf | Split config for VaultHub health rule coverage (part 1). |
| certora/confs/vaults/VaultHub_health.conf | Aggregate config for VaultHub health spec. |
| certora/confs/vaults/VaultHub.conf | Base config for VaultHub verification runs. |
| certora/confs/vaults/VaultHub-obligatedVaultIsConnected.conf | Dedicated config for obligated-vault connectivity rule. |
| certora/confs/setup/sanity_VaultHub.conf | Certora sanity config for VaultHub compilation/mutation setup. |
| certora/confs/setup/sanity_VaultFactory.conf | Certora sanity config for VaultFactory compilation/mutation setup. |
| certora/confs/setup/sanity_StakingVault.conf | Certora sanity config for StakingVault compilation/mutation setup. |
| certora/confs/setup/sanity_PredepositGuarantee.conf | Certora sanity config for PredepositGuarantee compilation/mutation setup. |
| certora/confs/setup/sanity_OperatorGrid.conf | Certora sanity config for OperatorGrid compilation/mutation setup. |
| certora/confs/setup/sanity_LazyOracle.conf | Certora sanity config for LazyOracle compilation/mutation setup. |
| certora/confs/setup/sanity_Dashboard.conf | Certora sanity config for Dashboard compilation/mutation setup. |
| certora/confs/setup/autocvl_Accounting.conf | AutoCVL config for Accounting verification. |
| certora/confs/old-Steth.conf | Legacy StETH-related Certora configuration. |
| certora/confs/old-Lido.conf | Legacy Lido-related Certora configuration. |
| certora/confs/misc/node_operators.conf | Certora config for NodeOperatorsRegistry spec. |
| certora/confs/misc/burner.conf | Certora config for Burner spec. |
| certora/confs/lido/Lido_staking.conf | Certora config for Lido staking limits rules. |
| certora/confs/lido/Lido_shares.conf | Certora config for Lido shares rules. |
| certora/confs/lido/Lido_eth.conf | Certora config for Lido buffered ETH rules. |
| certora/confs/lido/Base.conf | Base Certora config for Lido rules/spec. |
| certora/confs/core/comprehensive-setup.conf | Comprehensive multi-contract setup config for core specs. |
| certora/confs/core/Lido_and_VaultHub.conf | Core joint Lido/VaultHub verification config. |
| certora/confs/core/Accounting.conf | Core Accounting verification config. |
| certora/confs/core/Accounting-unsummarized.conf | Accounting config variant without certain summaries. |
| certora/confs/core/Accounting-summarized.conf | Accounting config variant with additional summaries. |
| certora/confs/core/Accounting-fees-as-frac.conf | Accounting config focused on protocol-fee share fraction rule. |
| certora/confs/core/Accounting-burnlimit.conf | Accounting config focused on burn-limit rule. |
| .prettierignore | Excludes /certora from Prettier formatting. |
| .github/workflows/foundry-fuzz-tests.yml | New PR workflow running selected Foundry fuzz/invariant tests. |
| .github/workflows/certora.yml | New PR workflow running multiple Certora configurations. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+160
to
+162
| /// @title Intergrity of `commitSharesToBurn` | ||
| rule commitBurnIntergrity(uint256 sharesToBurn) { | ||
| uint256 totalSharesPre = _Lido.getTotalShares(); |
There was a problem hiding this comment.
Spelling: "Intergrity" should be "Integrity" in both the doc comment and rule name, to improve readability and searchability.
Comment on lines
+22
to
+25
| function VaultHubHarness.obligationsShares(address) external returns (uint256) envfree; | ||
| function VaultHubHarness.unsettledLidoFees(address) external returns (uint256) envfree; | ||
| function VaultHubHarness.totalValue(address) external returns (uint256) envfree; | ||
| function VaultHubHarness.healthShortfallShares(address) external returns (uint256) envfree; |
There was a problem hiding this comment.
VaultHubHarness.totalValue(address) is declared twice in the methods block (lines 8 and 24). Duplicate method declarations can cause spec parsing/compilation issues and should be removed so there is a single authoritative summary/signature.
Comment on lines
+44
to
+48
| /// and therefore another becomes disconnected. | ||
| /// @notice Assumes `initialize` is called immediately after constructor (verified with Lido) | ||
| function applyVaultReportRquirements(address _other) { | ||
| require( | ||
| isInitialized(), |
There was a problem hiding this comment.
Typo in helper function name applyVaultReportRquirements (missing 'e' in "Requirements"). Since this helper is used across invariants, consider renaming to applyVaultReportRequirements to improve clarity and avoid propagating the typo into other specs/configs.
Comment on lines
+1
to
+17
| import "./VaultHub.spec"; | ||
|
|
||
|
|
||
| methods { | ||
| function OperatorGrid.onBurnedShares(address, uint256) external => NONDET; | ||
| function OperatorGrid.onMintedShares(address, uint256, bool) external => NONDET; | ||
|
|
||
| // Ignore side-effects of rebalancing on internal-ETH to internal-shares ratio. | ||
| // Without this, rebalancing increases _internalEth which increases share price, | ||
| // causing remaining liability shares to convert to more ETH, potentially making | ||
| // the vault unhealthy again. This is the approach used in approximated-VaultHub.spec. | ||
| function ILidoMock.rebalanceExternalEtherToInternal(uint256) external => NONDET; | ||
|
|
||
| // Simplify external calls that don't affect the core property | ||
| function _.pauseBeaconChainDeposits() external => NONDET; | ||
| function _.resumeBeaconChainDeposits() external => NONDET; | ||
| } |
There was a problem hiding this comment.
This spec currently defines only methods summaries; all rules/invariants are commented out. The corresponding config (certora/confs/vaults/shortfall.conf) will therefore not verify any shortfall property and may pass vacuously. Either add at least one active rule/invariant here or remove this spec from CI until it contains checks.
Comment on lines
+21
to
+32
| contract NativeTransferFuncs { | ||
|
|
||
| ILido public LIDO; | ||
|
|
||
| function withdrawRewards(uint256 amount) external returns (uint256) { | ||
| LIDO.receiveELRewards{value: amount}(); | ||
| return amount; | ||
| } | ||
|
|
||
| function withdrawWithdrawals(uint256 amount) public { | ||
| LIDO.receiveWithdrawals{value: amount}(); | ||
| } |
There was a problem hiding this comment.
LIDO is a storage variable that is never initialized (no constructor or setter). As written, withdrawRewards/withdrawWithdrawals will call receiveELRewards/receiveWithdrawals on address(0), which will revert if these functions are ever executed in a spec. To match the real vault contracts, make LIDO immutable and set it in a constructor, or add an explicit initializer/setter used by the verification setup.
Comment on lines
+1
to
+2
| git apply ./certora/patches/patch-strategy-lib.patch | ||
| git apply ./certora/patches/patch-total-shares-access.patch |
There was a problem hiding this comment.
Consider making this script fail fast and portable by adding a shell shebang and set -e (or set -euo pipefail). As-is, a failed git apply may be easier to miss in local runs and CI logs.
Comment on lines
+32
to
+33
| with: | ||
| version: nightly |
There was a problem hiding this comment.
This workflow pins Foundry to nightly. In this repo’s existing CI (.github/workflows/tests-unit.yml) the Foundry version is intentionally left unpinned (with guidance to pin only if nightly breaks). Using nightly here may introduce avoidable CI flakiness; consider aligning with the existing approach (omit version or pin to a known-good revision).
Suggested change
| with: | |
| version: nightly |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.