test: vUnits deviation accumulator round-trip invariant - #629
Open
AnubisQuantumCipher wants to merge 1 commit into
Open
test: vUnits deviation accumulator round-trip invariant#629AnubisQuantumCipher wants to merge 1 commit into
AnubisQuantumCipher wants to merge 1 commit into
Conversation
Asserts the strong DAO accumulator identity daoTotalEthVUnits == ethDaoValidatorCount * BPS_DENOMINATOR holds after the full lifecycle register -> updateClusterBalance(EB up) -> liquidate -> reactivate -> updateClusterBalance(EB down to baseline) on a single cluster with zero fees (orthogonal to the vUnits-deviation dimension being probed). This is the deviation-only-model endpoint identity: the per-operator deviation MUST net to zero across the cycle, otherwise networkTotalEarnings (ProtocolLib.sol:84-90) under- or over-collects against the cluster owners' real obligations. Complements the existing Echidna property echidna_vunits_deviation_consistent at SSVAccountingEchidna.sol:1023, which asserts the weaker self-consistent identity daoTotalEthVUnits == sum(clusterEB.vUnits) that can mirror a corruption since both sides read from the same storage the SUT writes. This test asserts the stronger endpoint identity on a deterministic state-machine sequence that the Echidna action_* surface does not chain together (updateClusterBalance is not part of SSVAccountingEchidna's action set, and no Echidna harness sequences a full register -> EB up -> liquidate -> reactivate -> EB down cycle). Pin: HEAD 9bb7b21.
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.
Summary
Adds
test/sanity/vunits-cycle-roundtrip-invariant.test.ts— a single deterministic sanity test that asserts the deviation-only model's strong endpoint identity after a full cluster lifecycle cycle:The cycle exercised:
After this sequence, every per-operator stored deviation must have netted to zero; otherwise
ProtocolLib.networkTotalEarnings(contracts/libraries/ProtocolLib.sol:84-90) would over- or under-collect against the cluster owners' real obligations on subsequent updates.Pin: branch
mainHEAD at the time of writing (9bb7b21d4432f34f623bed3e0bb3fa77f1e5d2b9).Why a new sanity test?
The existing Echidna property
echidna_vunits_deviation_consistentattest/echidna/SSVAccountingEchidna.sol:1023asserts the weaker self-consistent identity:That identity can mirror a corruption because both sides read from the same storage the SUT writes. The endpoint identity in this PR is stronger: it requires every per-operator deviation accumulator to have rolled back to zero across the cycle, which an internal-storage-recompute property cannot detect.
Two additional reasons this property is currently uncovered:
updateClusterBalanceis not inSSVAccountingEchidna's action surface (the 22 actions enumerated at the top of that contract do not include anaction_update_cluster_balance_*variant), so the explicit-EB up/down sequence this invariant probes is structurally unreachable for the existing harness.test/echidna/chains the fullregister -> EB up -> liquidate -> reactivate -> EB downcycle through a single stateful sequence.SSVEdgeCasesEchidna'sechidna_reactivation_restores_vunitsat:425covers the reactivation step but not the full cycle and not the post-cycle DAO identity.This test pins the deviation-only model's expected behavior to a runnable artifact and would catch any future regression that introduces drift on this exact cycle.
How it fits the repo
ssvClustersHarnessFixtureand the existingsetupTestContext/registerAndParseCluster/mockEBAndUpdate/parseClusterFromEventhelpers — no new test infrastructure.test/sanity/next to the other regression-style sanity tests (ssv2-frozen-supply-quorum.test.ts,ssv3-stale-vunits-liquidation.test.ts, etc.).Test plan
NO_GAS_ENFORCE=true npx hardhat test test/sanity/vunits-cycle-roundtrip-invariant.test.tspasses locally onmain(1 passing, ~85 ms).test/unit/SSVClusters/ebAutoLiquidation.test.tsfor the EB-update + liquidate flow andtest/sanity/ssv3-stale-vunits-liquidation.test.tsfor the sanity-test shape.Provenance
This test was authored as part of an independent post-v2.0.0 audit pass; the property the test probes was derived from a symbolic walk-through of
OperatorLib.updateSnapshotSt(contracts/libraries/OperatorLib.sol:52-72) and the_executeLiquidationflow (contracts/modules/SSVClusters.sol:555-616). No issue was found at9bb7b21d— the invariant holds, this PR pins it.